Added η-expander module and removed EAdd from grammar.

Grammar.cf

@@ -63,7 +63,7 @@ internal EVar.  Exp4 ::= LIdent;
          EInj.  Exp4 ::= UIdent;
          ELit.  Exp4 ::= Lit;
          EApp.  Exp3 ::= Exp3 Exp4;
-         EAdd.  Exp2 ::= Exp2 "+" Exp3;
+internal EAdd.  Exp2 ::= Exp2 "+" Exp3;
          ELet.  Exp1  ::= "let" Bind "in" Exp1; 
 --         EAbsS. Exp1  ::= "\\" Pattern "." Exp1;
          EAbs.  Exp1  ::= "\\" LIdent "." Exp1;

language.cabal

@@ -35,6 +35,7 @@ executable language
       Auxiliary
       Renamer.Renamer
       TypeChecker.TypeChecker
+      Expander
       AnnForall
       OrderDefs
       TypeChecker.TypeCheckerHm

sample-programs/Quicksort.crf

@@ -22,23 +22,20 @@ filter p xs = case xs of
         True => Cons x (filter p xs)
         False => filter p xs
 
-.++ as bs = case as of
+(++) as bs = case as of
     Nil => bs
     Cons x xs => Cons x (xs ++ bs)
 
-.:: a as = Cons a as
-
 quicksort : List Int -> List Int
 quicksort xs = case xs of
     Nil => Nil
     Cons a as => let smaller = quicksort (filter (\y. y < a) xs)
                   in let bigger = quicksort (filter (\y. a < y) xs)
-                      in smaller ++ (a :: bigger)
+                      in smaller ++ (Cons a bigger)
 
 descList : Int -> Int -> List Int
 descList from to = case to < from of
    False => Cons to (descList from (to - 1)) 
    True => Nil
 
-main = let list = (5 :: (2 :: (8 :: (9 :: (6 :: (0 :: (1 :: Nil)))))))
-        in printStr (toStr (quicksort list))
+-- main = let list = (5 :: (2 :: (8 :: (9 :: (6 :: (0 :: (1 :: Nil))))))) in printStr (toStr (quicksort list))

sample-programs/eta_test1.crf

@@ -0,0 +1,4 @@
+id x = x
+f = id
+
+main = f 1

sample-programs/eta_test2.crf

@@ -0,0 +1,19 @@
+data List a where
+    Nil : List a
+    Cons : a -> List a -> List a
+
+map : (a -> b) -> List a -> List b
+map f xs = case xs of
+    Nil => Nil
+    Cons a as => Cons (f a) (map f as)
+
+add : Int -> Int -> Int
+add x y = x + y
+
+sum : List Int -> Int
+sum xs = case xs of
+    Nil => 0
+    Cons a as => a + (sum xs)
+
+main : Int
+main = sum (map (add 1) (Cons 1 Nil))

src/Codegen/Emits.hs

@@ -369,6 +369,7 @@ preludeFuns def (Ident xs) arg1 arg2
   | "$langle$$langle$" `isPrefixOf` xs = pure $ Icmp LLSlt I8 arg1 arg2
   | "$langle$" `isPrefixOf` xs =  pure $ Icmp LLSlt I64 arg1 arg2
   | "$minus$" `isPrefixOf` xs = pure $ Sub I64 arg1 arg2
+  | "$plus$" `isPrefixOf` xs = pure $ Add I64 arg1 arg2
   | "printChar$" `isPrefixOf` xs = do
         pure . UnsafeRaw $
             "add i16 0,0\n    call void (ptr, ...) @printf(ptr noundef @.char_print_no_nl, i8 noundef " <> toIr arg1 <> ")\n"

src/Expander.hs

@@ -0,0 +1,64 @@
+module Expander where
+
+import TypeChecker.TypeCheckerIr
+import Control.Monad.State
+
+type TExp = T' Exp' Type
+
+type M = State Int
+
+expand :: Program -> Program
+expand (Program defs) = Program (map expandDef defs)
+
+expandDef :: Def -> Def
+expandDef (DBind bind) = DBind $ expandBind bind
+expandDef d            = d
+
+initialState = 0
+
+expandBind :: Bind' Type -> Bind' Type
+expandBind (Bind name args e)
+    = Bind name args $ evalState (expandExp e) initialState
+
+expandExp :: TExp -> M TExp
+expandExp e = do
+    case e of
+        (EApp e1@(e_, _) e2@(_, _), t) -> do
+            let sizeType = arrows t
+            let sizeExp = apps e_
+            let diff = sizeType - sizeExp
+            e1' <- expandExp e1
+            e2' <- expandExp e2
+            apply diff (EApp e1' e2', t)
+        (EVar _, t) -> do
+            let sizeType = arrows t
+            apply sizeType e
+        e -> pure e
+
+apply :: Int -> TExp -> M TExp
+apply n (e, t)
+  | n < 1 = pure (e, t)
+  | otherwise = do
+    fr <- fresh
+    let (TFun t1 t2) = t
+    e' <- apply (n - 1) (EApp (e,t) (EVar fr, t1), t2)
+    pure (EAbs fr e', t)
+
+-- Eerily similar functions
+apps :: Exp -> Int
+apps (EApp _ (e2, _)) = 1 + apps e2
+apps _ = 0
+
+arrows :: Type -> Int
+arrows (TFun _ t2) = 1 + arrows t2
+arrows _ = 0
+
+fresh :: M Ident
+fresh = do
+   n <- get 
+   put (n + 1)
+   return (letters !! n)
+  where
+    letters :: [Ident]
+    letters =
+        map (Ident . ("eta$" ++)) $ [1 ..] >>= flip replicateM ['a' .. 'z']

src/Main.hs

@@ -9,6 +9,7 @@ import           Control.Monad               (when, (<=<))
 import           Data.List.Extra             (isSuffixOf)
 import           Data.Maybe                  (fromJust, isNothing)
 import           Desugar.Desugar             (desugar)
+import           Expander                    (expand)
 import           GHC.IO.Handle.Text          (hPutStrLn)
 import           Grammar.ErrM                (Err)
 import           Grammar.Layout              (resolveLayout)
@@ -117,7 +118,7 @@ main' opts s =
             file <- readFile s
 
            
-            let file' = if opts.preludeOpt then file else file ++ prelude
+            let file' = if opts.preludeOpt then file ++ primitives else file ++ primitives ++ prelude
             parsed <- fromErr . pProgram . resolveLayout True $ myLexer file'
             when opts.logIL (printToErr "-- Parse Tree -- " >> log parsed)
 
@@ -135,7 +136,11 @@ main' opts s =
             when opts.logIL (printToErr "\n-- TypeChecker --" >> log typechecked)
 
 
-            let lifted = lambdaLift typechecked
+            let etaexpanded = expand typechecked
+            when opts.logIL (printToErr "\n-- Eta expander --" >> log etaexpanded)
+
+            
+            let lifted = lambdaLift etaexpanded
             when opts.logIL (printToErr "\n-- Lambda Lifter --" >> log lifted)
 
             
@@ -182,29 +187,33 @@ printToErr = hPutStrLn stderr
 fromErr :: Err a -> IO a
 fromErr = either (\s -> printToErr s >> exitFailure) pure
 
-prelude :: String
-prelude =
+primitives =
     unlines
-        [ "\n"
+        [ ""
         , "data Bool where"
         , "    False : Bool"
         , "    True  : Bool"
-        , -- The function body of lt is replaced during code gen. It exists here for type checking purposes.
-          ".< : Int -> Int -> Bool"
+        , "\n"
+        , ".< : Int -> Int -> Bool"
         , ".< x y = case x of"
         , "    _ => True"
         , "    _ => False"
-        , "\n"
-        , -- The function body of - is replaced during code gen. It exists here for type checking purposes.
-          ".- : Int -> Int -> Int"
+        , ".- : Int -> Int -> Int"
         , ".- x y = 0"
-        , "\n"
+        , ".+ : Int -> Int -> Int"
+        , ".+ x y = 0"
         , ".== : Int -> Int -> Bool"
         , ".== a b = case a < b of"
         , "    False => case b < a of"
         , "        False => True"
         , "        _ => False"
         , "    False => False"
+        ]
+
+prelude :: String
+prelude =
+    unlines
+        [ "\n"
         , "data Unit where"
         , "  Unit : Unit"
         , "\n"