From 413f7d3a21ca69bb58b55a8de77ce3e6dedb7754 Mon Sep 17 00:00:00 2001
From: depsterr <depsterr@protonmail.com>
Date: Wed, 26 Jan 2022 19:05:15 +0100
Subject: [PATCH] handle application as list

---
 src/PostProcess.hs | 10 +++----
 src/TC.hs          | 67 ++++++++++++++++++++++++++++++----------------
 src/Type.hs        |  2 +-
 tst                |  1 +
 4 files changed, 49 insertions(+), 31 deletions(-)
 create mode 100644 tst

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)