diff --git a/src/PostProcess.hs b/src/PostProcess.hs index f2afb14..15fbc13 100644 --- a/src/PostProcess.hs +++ b/src/PostProcess.hs @@ -30,10 +30,11 @@ runProcess = (fst <$>) .: runStateT postprocess :: [H.Def] -> Process [TL] postprocess defs = addDef <~> defs >> defToTL <~> defs +-- just adds types for processing type signatures addDef :: H.Def -> Process () addDef = \case - H.VarDef _ i t _ -> lift . addEnv i =<< typeSigToPolyT t -- the type checker will check this matches the exp H.TypeDef _ t _ -> insertType =<< fst <$> typeSigToIdParams t + H.VarDef _ i t _ -> pure () -- add type before typesig to id params defToTL :: H.Def -> Process TL @@ -92,12 +93,7 @@ expToExp :: H.Exp -> Process Exp expToExp = \case H.ExpLet p as e -> Let p <$> assignTo2pl <~> as <*> expToExp e H.ExpAbs p is e -> Abs p is <$> expToExp e - H.ExpApp p e1 (e2:es) -> do - e1' <- expToExp e1 - e2' <- expToExp e2 - es' <- traverse expToExp es - pure (foldl (App p) (App p e1' e2') es') - H.ExpApp p e [] -> throwError Oop + H.ExpApp p e es -> App p <$> expToExp e <*> expToExp <~> es H.ExpVar p i -> pure (Var p i) declTo2pl :: H.Decl -> Process (Id, MonoT) diff --git a/src/TC.hs b/src/TC.hs index e96e408..6eaafd0 100644 --- a/src/TC.hs +++ b/src/TC.hs @@ -149,29 +149,50 @@ constructs _ _ = False infer :: Exp -> Check (Subst, MonoT) infer = setPos >=> \case - Let _ [] e -> infer e - Let p ((i,e1):ies) e2 -> do - (s1, t1) <- infer e1 - apply s1 <$> getEnv >>= \e -> localEnv e $ do - t1g <- generalize t1 - addEnv i t1g - (s2, t2) <- infer (Let p ies e2) - pure (s2 <&> s1, t2) - Abs _ [] e -> infer e - Abs p (i:is) e -> localEnv' $ do - tv <- fresh - addEnv i (Forall S.empty tv) - (s, t) <- infer (Abs p is e) - pure (s, apply s tv `TArr` t) + Var _ i -> (emptySubst,) <$> lookupType i - App p e1 e2 -> localEnv' $ do - tv <- fresh - (s1, t1) <- infer e1 - applyEnv s1 - (s2, t2) <- infer e2 - s3 <- unify (apply s2 t1) (TArr t2 tv) - return (s3 <&> s2 <&> s1, apply s3 tv) - App _ _ _ -> throwError Oop + Let _ [] e -> infer e + Let p ((i,e1):ies) e2 -> do + (s1, t1) <- infer e1 + apply s1 <$> getEnv >>= \e -> localEnv e $ do + t1g <- generalize t1 + addEnv i t1g + (s2, t2) <- infer (Let p ies e2) + pure (s2 <&> s1, t2) - Var _ i -> (emptySubst,) <$> lookupType i + Abs _ [] e -> infer e + Abs p (i:is) e -> localEnv' $ do + tv <- fresh + addEnv i (Forall S.empty tv) + (s, t) <- infer (Abs p is e) + pure (s, apply s tv `TArr` t) + + App _ e es -> go e (reverse es) + where + go :: Exp -> [Exp] -> Check (Subst, MonoT) + go _ [] = throwError Oop + go e1 [e2] = localEnv' $ do + + (s1, t1) <- infer e1 + applyEnv s1 + + (s2, t2) <- infer e2 + + tv <- fresh + + s3 <- unify (apply s2 t1) (t2 `TArr` tv) + pure (s3 <&> s2 <&> s1, apply s3 tv) + + go e1 (e2:es) = localEnv' $ do + + (s1, t1) <- go e1 es + applyEnv s1 + + (s2, t2) <- infer e2 + + tv <- fresh + + s3 <- unify (apply s2 t1) (t2 `TArr` tv) + + pure (s3 <&> s2 <&> s1, apply s3 tv) diff --git a/src/Type.hs b/src/Type.hs index c9d141b..3ef2ff6 100644 --- a/src/Type.hs +++ b/src/Type.hs @@ -41,7 +41,7 @@ type Exp = Exp' Pos data Exp' a = Let a [(Id,Exp)] Exp | Abs a [Id] Exp - | App a Exp Exp + | App a Exp [Exp] | Var a Id deriving Show diff --git a/tst b/tst new file mode 100644 index 0000000..aa19a4e --- /dev/null +++ b/tst @@ -0,0 +1 @@ +λf g x y z w. f w (g x y z)