Initial typingHEADmain

5 files changed, 86 insertions, 22 deletions

diff --git a/src/Language/Mili/Analyzer.hs b/src/Language/Mili/Analyzer.hs
index d4996ee..37c4437 100644
--- a/src/Language/Mili/Analyzer.hs
+++ b/src/Language/Mili/Analyzer.hs
@@ -37,10 +37,10 @@ traceAbs = go 0 [Root]
   go n t (Abs _ m) =
     M.unionWith (++) (go (n + 1) (AbsD : t) m) (M.singleton n [t])
   go n t (App a b) = M.unionWith (++) (go n (AppL : t) a) (go n (AppR : t) b)
-  go _ _ (Lvl _             ) = M.empty
-  go _ _ (Num Z             ) = M.empty
-  go n t (Num (S i)         ) = go n (NumS : t) i
-  go n t (Rec (t1, t2) u v w) = foldl1
+  go _ _ (Lvl _          ) = M.empty
+  go _ _ (Num Z          ) = M.empty
+  go n t (Num (S i)      ) = go n (NumS : t) i
+  go n t (Rec t1 t2 u v w) = foldl1
     (M.unionWith (++))
     [ go n (RecT1 : t) t1
     , go n (RecT2 : t) t2
@@ -56,12 +56,12 @@ traceAbs = go 0 [Root]
 traceLvl :: Term -> HashMap Int [Trace]
 traceLvl = go [Root]
  where
-  go t (Abs _ m           ) = go (AbsD : t) m
-  go t (App a b) = M.unionWith (++) (go (AppL : t) a) (go (AppR : t) b)
-  go t (Lvl l             ) = M.singleton l [t]
-  go _ (Num Z             ) = M.empty
-  go t (Num (S i)         ) = go (NumS : t) i
-  go t (Rec (t1, t2) u v w) = foldl1
+  go t (Abs _ m        ) = go (AbsD : t) m
+  go t (App a b        ) = M.unionWith (++) (go (AppL : t) a) (go (AppR : t) b)
+  go t (Lvl l          ) = M.singleton l [t]
+  go _ (Num Z          ) = M.empty
+  go t (Num (S i)      ) = go (NumS : t) i
+  go t (Rec t1 t2 u v w) = foldl1
     (M.unionWith (++))
     [ go (RecT1 : t) t1
     , go (RecT2 : t) t2
diff --git a/src/Language/Mili/Compiler.hs b/src/Language/Mili/Compiler.hs
new file mode 100644
index 0000000..ab23767
--- /dev/null
+++ b/src/Language/Mili/Compiler.hs
@@ -0,0 +1,19 @@
+-- MIT License, Copyright (c) 2024 Marvin Borner
+
+module Language.Mili.Compiler
+  ( compile
+  ) where
+
+import           Data.Mili                      ( Nat(..)
+                                                , Term(..)
+                                                , shift
+                                                )
+
+data Comp = CAbs String Comp                  -- | Abstraction with pointer
+              | CApp Comp Comp                -- | Application
+              | CVar                          -- | Namless variable
+              | CNum Nat                      -- | Peano numeral
+              | CRec Comp Comp Comp Comp Comp -- | Unbounded iteration
+
+compile :: Term -> Comp
+compile t = CVar
diff --git a/src/Language/Mili/Parser.hs b/src/Language/Mili/Parser.hs
index b9f7881..0854ab1 100644
--- a/src/Language/Mili/Parser.hs
+++ b/src/Language/Mili/Parser.hs
@@ -115,7 +115,7 @@ rec = do
   _  <- spaces
   _  <- startSymbol ","
   w  <- term
-  pure $ Rec (t1, t2) u v w
+  pure $ Rec t1 t2 u v w
 
 -- | single identifier, directly parsed to corresponding term
 def :: Parser Term
diff --git a/src/Language/Mili/Reducer.hs b/src/Language/Mili/Reducer.hs
index dc8c9bd..27ac029 100644
--- a/src/Language/Mili/Reducer.hs
+++ b/src/Language/Mili/Reducer.hs
@@ -13,25 +13,28 @@ data Singleton = TermTag Term | RecTag Term Term Term Term
 
 -- TODO: There will only ever be one substitution, so don't iterate the entire tree!
 -- WARNING: This function also shifts the substituted term and the levels of the parent!
+-- TODO: replace with foldM?
+-- In compilation this won't be necessary since Abs can have a direct pointer to the variable
 subst :: Int -> Int -> Term -> Term -> Term
 subst c l (Abs d m) s = Abs (d - 1) $ subst (c + 1) l m s
 subst c l (App a b) s = App (subst c l a s) (subst c l b s)
 subst c l (Lvl i) s | l == i    = shift c s
                     | otherwise = Lvl $ i - 1
-subst _ _ (Num Z             ) _ = Num Z
-subst c l (Num (S m)         ) s = Num $ S $ subst c l m s
-subst c l (Rec (t1, t2) u v w) s = Rec (subst c l t1 s, subst c l t2 s)
-                                       (subst c l u s)
-                                       (subst c l v s)
-                                       (subst c l w s)
+subst _ _ (Num Z          ) _ = Num Z
+subst c l (Num (S m)      ) s = Num $ S $ subst c l m s
+subst c l (Rec t1 t2 u v w) s = Rec (subst c l t1 s)
+                                    (subst c l t2 s)
+                                    (subst c l u s)
+                                    (subst c l v s)
+                                    (subst c l w s)
 
 machine :: Term -> [Singleton] -> Term
-machine (App a b           ) s                    = machine a (TermTag b : s)
-machine (Abs l u           ) (TermTag t : s)      = machine (subst 0 l u t) s
-machine (Rec (t1, t2) u v w) s = machine t1 (RecTag t2 u v w : s)
-machine (Num Z             ) (RecTag _ u _ _ : s) = machine u s
+machine (App a b        ) s                    = machine a (TermTag b : s)
+machine (Abs l u        ) (TermTag t : s)      = machine (subst 0 l u t) s
+machine (Rec t1 t2 u v w) s = machine t1 (RecTag t2 u v w : s)
+machine (Num Z          ) (RecTag _ u _ _ : s) = machine u s
 machine (Num (S t1)) ((RecTag t2 u v w) : s) =
-  machine v (TermTag (Rec (App w t1, App w t2) u v w) : s)
+  machine v (TermTag (Rec (App w t1) (App w t2) u v w) : s)
 machine (Num (S t)) s = Num $ S $ machine t s -- TODO: ??
 machine t           _ = t
 
diff --git a/src/Language/Mili/Typer.hs b/src/Language/Mili/Typer.hs
new file mode 100644
index 0000000..d6b453b
--- /dev/null
+++ b/src/Language/Mili/Typer.hs
@@ -0,0 +1,42 @@
+-- MIT License, Copyright (c) 2024 Marvin Borner
+
+module Language.Mili.Typer
+  ( typeCheck
+  ) where
+
+import           Control.Monad.State
+import           Data.HashMap.Strict            ( HashMap )
+import qualified Data.HashMap.Strict           as M
+import           Data.Mili                      ( Nat(..)
+                                                , Term(..)
+                                                )
+
+data Type = Number | Lolli Type Type
+  deriving (Show, Eq)
+type Context = HashMap Int Type
+
+-- | Convert de Bruijn levels to unique variables
+annotate :: Term -> State (Int, [Int]) Term
+annotate (Abs _ m) = do
+  (s, ls) <- get
+  put (s + 1, s : ls)
+  an <- annotate m
+  modify $ \(s', _) -> (s', ls)
+  pure $ Abs s an
+annotate (App a b) = (App <$> annotate a) <*> annotate b
+annotate (Lvl i  ) = do
+  (_, ls) <- get
+  pure $ Lvl $ ls !! (length ls - i - 1)
+annotate (Num Z    ) = pure $ Num Z
+annotate (Num (S m)) = Num . S <$> annotate m
+annotate (Rec t1 t2 u v w) =
+  Rec
+    <$> annotate t1
+    <*> annotate t2
+    <*> annotate u
+    <*> annotate v
+    <*> annotate w
+
+typeCheck :: Term -> Either String Term
+typeCheck t =
+  Left $ show (inferGamma M.empty M.empty $ evalState (annotate t) (0, []))