From 133cc31e77d67677ae0454e6dff528f2da9eb1d7 Mon Sep 17 00:00:00 2001 From: Martin Fredin Date: Tue, 28 Mar 2023 14:36:43 +0200 Subject: [PATCH] Fix lambda lifter --- sample-programs/basic-0 | 4 +- sample-programs/basic-6.crf | 8 +-- src/TypeChecker/TypeCheckerBidir.hs | 78 +++++++++++++---------------- 3 files changed, 42 insertions(+), 48 deletions(-) diff --git a/sample-programs/basic-0 b/sample-programs/basic-0 index 4738fb6..5084527 100644 --- a/sample-programs/basic-0 +++ b/sample-programs/basic-0 @@ -5,7 +5,7 @@ data forall a. List (a) where { length : forall c. List (c) -> Int; length = \list. case list of { - Nil => 0; Cons x xs => 1 + length xs; - Cons x (Cons y Nil) => 2; +-- Nil => 0; +-- Cons x (Cons y Nil) => 2; }; diff --git a/sample-programs/basic-6.crf b/sample-programs/basic-6.crf index 3ed64a0..082cc6b 100644 --- a/sample-programs/basic-6.crf +++ b/sample-programs/basic-6.crf @@ -3,8 +3,8 @@ data Bool () where { False : Bool () }; -main : Bool () -> Int ; +main : Bool () -> a -> Int ; main b = case b of { - False => 0; - True => 0 -} + False => (\x. 1); + True => \x. 0; +}; diff --git a/src/TypeChecker/TypeCheckerBidir.hs b/src/TypeChecker/TypeCheckerBidir.hs index 5ad5021..78afe7c 100644 --- a/src/TypeChecker/TypeCheckerBidir.hs +++ b/src/TypeChecker/TypeCheckerBidir.hs @@ -46,12 +46,12 @@ type Env = Seq EnvElem -- | Ordered context -- Γ ::= ・| Γ, α | Γ, ά | Γ, ▶ ά | Γ, x:A data Cxt = Cxt - { env :: Env -- ^ Local scope context Γ - , sig :: Map LIdent Type -- ^ Top-level signatures x : A - , binds :: Map LIdent Exp -- ^ Top-level binds x : e - , next_tevar :: Int -- ^ Counter to distinguish ά - , data_injs :: Map UIdent Type -- ^ Data injections (constructors) K/inj : A - , data_types :: Map UIdent [(UIdent, Type)] -- ^ Data types D : (K₁:A₁ + ‥ + Kₙ:Aₙ) + { env :: Env -- ^ Local scope context Γ + , sig :: Map LIdent Type -- ^ Top-level signatures x : A + , binds :: Map LIdent Exp -- ^ Top-level binds x : e + , next_tevar :: Int -- ^ Counter to distinguish ά + , data_injs :: Map UIdent Type -- ^ Data injections (constructors) K/inj : A + , data_types :: Map UIdent (Type, [(UIdent, Type)]) -- ^ Data types (∀α. D (α), K₁:A₁ + ‥ + Kₙ:Aₙ) } deriving (Show, Eq) newtype Tc a = Tc { runTc :: ExceptT String (State Cxt) a } @@ -79,7 +79,7 @@ typecheck (Program defs) = do TData name _ = getTData typ kts = [(k,t) | Inj k t <- injs ] in - (name, kts) + (name, (typ, kts)) | Data typ injs <- datatypes ] } @@ -574,45 +574,39 @@ checkPattern patt t_patt = (, t_patt) <$> case patt of -- Γ ⊢ B₁ → ‥ → Bₘ₊₁ <: A₁ + ‥ + Aₙ ⊣ Θ₁ Θₘ ⊢ pₘ ↑ [Θₘ₋₁]Bₘ ⊣ Δ -- -------------------------------------------------------------- -- Γ ⊢ injₖ xₖ. p₁ ‥ pₘ ↑ A₁ + ‥ + Aₙ ⊣ Δ - PInj name ps -> do - t <- maybeToRightM ("Unknown constructor " ++ show name) - =<< lookupInj name - subtype t t_patt + PInj name ps -> undefined + -- injs <- maybeToRightM err1 =<< lookupDataType name_d + -- tinj <- liftEither . maybeToRight err2 $ lookup name injs + -- trace (show $ length foralls) pure () + -- (tinj', tdata) <- substituteTVars foralls tinj tdata + -- traceT "tinj'" tinj' + -- traceT "tdata" tdata + -- subtype (getTData $ getReturn tinj') tdata + -- t_inj'' <- applyEnv tinj' + -- tdata' <- applyEnv tdata + -- pure $ T.PInj (coerce name) [] + where + substituteTVars fas t1 t2 = case fas of + [] -> pure (t1, t2) + fa:fas' -> do + (t1', t2') <- go fa (t1, t2) + substituteTVars fas' t1' t2' + where + go fa (t1, t2) = let TAll tvar _ = fa dummy in do + tevar <- fresh + insertEnv (EnvTEVar tevar) + traceT "tevar:" (TEVar tevar) + pure $ on (,) (substitute tvar tevar) t1 t2 + (foralls, tdata@(TData name_d _)) = partitionData t_patt + err1 = unwords ["Unknown data type", show name_d] + err2 = unwords ["No", show name, "constructor for data type", show name_d] - let (t_ps, t_return) = partitionTypeWithForall t - unless (length ps == length t_ps) $ - throwError "Wrong number of variables" -- §ps' <- zipWithM (\p t -> checkPattern p =<< applyEnv t) ps t_ps -- let ps'' = map fst ps' -- TODO - pure $ T.PInj (coerce name) [] + -- pure $ T.PInj (coerce name) [] -subtypeData :: UIdent -> Type -> Tc () -subtypeData name_inj typ = do - injs <- maybeToRightM err1 =<< lookupDataType name_d - t_inj <- liftEither . maybeToRight err2 $ lookup name_k injs - (t_inj', typs')<- substituteTVars foralls t_inj data_t - subtype () - - undefined - where - substituteTVars fas t1 t2 = case fas of - [] -> pure (t1, t2) - fa:fas' -> do - (t1', t2') <- go fa (t1, t2) - substituteTVars fas' t1' t2' - where - go fa (t1, t2) = let TAll tvar _ = fa dummy in do - tevar <- fresh - insertEnv (EnvTEVar tevar) - pure $ on (,) (substitute tvar tevar) t1 t2 - - - - (foralls, data_t@(TData name_d typs)) = partitionData typ - err1 = unwords ["Unknown data type", show name_d] - err2 = unwords ["No", show name_k, "constructor for data type", show name_d] -- TAll tvar t -> do -- tevar <- fresh @@ -875,7 +869,7 @@ insertEnv x = modifyEnv (:|> x) lookupBind :: LIdent -> Tc (Maybe Exp) lookupBind x = gets (Map.lookup x . binds) -lookupDataType :: UIdent -> Tc (Maybe [(UIdent, Type)]) +lookupDataType :: UIdent -> Tc (Maybe (Type, [(UIdent, Type)])) lookupDataType x = gets (Map.lookup x . data_types) lookupSig :: LIdent -> Tc (Maybe Type) @@ -897,7 +891,7 @@ putEnv = modifyEnv . const modifyEnv :: (Env -> Env) -> Tc () modifyEnv f = - modify $ \cxt -> {- trace (ppEnv (f cxt.env)) -} cxt { env = f cxt.env } + modify $ \cxt -> trace (ppEnv (f cxt.env)) cxt { env = f cxt.env } pattern DBind' name vars exp = DBind (Bind name vars exp) pattern DSig' name typ = DSig (Sig name typ)