aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorMarvin Borner2024-11-27 16:18:16 +0100
committerMarvin Borner2024-11-27 16:18:16 +0100
commit02ff39d0ab6488fa8cedb31030130b352e10b3e2 (patch)
tree2fef90f83699831d13dea768e144430e1f60a7a2 /src
parent91d52159a5ac32165dca0edfaf75a19845156551 (diff)
Initial typingHEADmain
Diffstat (limited to 'src')
-rw-r--r--src/Data/Mili.hs45
-rw-r--r--src/Language/Mili/Analyzer.hs20
-rw-r--r--src/Language/Mili/Compiler.hs19
-rw-r--r--src/Language/Mili/Parser.hs2
-rw-r--r--src/Language/Mili/Reducer.hs25
-rw-r--r--src/Language/Mili/Typer.hs42
6 files changed, 98 insertions, 55 deletions
diff --git a/src/Data/Mili.hs b/src/Data/Mili.hs
index c10b24f..de709f1 100644
--- a/src/Data/Mili.hs
+++ b/src/Data/Mili.hs
@@ -3,7 +3,6 @@
module Data.Mili
( Term(..)
, Nat(..)
- , foldM
, fold
, shift
) where
@@ -44,31 +43,6 @@ instance Show Term where
. showString ", "
. shows w
-foldM
- :: Monad m
- => (Int -> Term -> m Term)
- -> (Term -> Term -> m Term)
- -> (Int -> m Term)
- -> (Nat -> m Term)
- -> (Term -> Term -> Term -> Term -> Term -> m Term)
- -> Term
- -> m Term
-foldM abs app lvl num rec (Abs d m) = foldM abs app lvl num rec m >>= abs d
-foldM abs app lvl num rec (App a b) = do
- a' <- foldM abs app lvl num rec a
- b' <- foldM abs app lvl num rec b
- app a' b'
-foldM _ _ lvl _ _ (Lvl i ) = pure i >>= lvl
-foldM _ _ _ num _ (Num Z ) = pure Z >>= num
-foldM abs app lvl num rec (Num (S m)) = foldM abs app lvl num rec m >>= num . S
-foldM abs app lvl num rec (Rec t1 t2 u v w) = do
- t1' <- foldM abs app lvl num rec t1
- t2' <- foldM abs app lvl num rec t2
- u' <- foldM abs app lvl num rec u
- v' <- foldM abs app lvl num rec v
- w' <- foldM abs app lvl num rec w
- rec t1' t2' u' v' w'
-
fold
:: (Int -> Term -> Term)
-> (Term -> Term -> Term)
@@ -77,13 +51,18 @@ fold
-> (Term -> Term -> Term -> Term -> Term -> Term)
-> Term
-> Term
-fold abs app lvl num rec term = runIdentity $ foldM
- (\d m -> pure $ abs d m)
- (\a b -> pure $ app a b)
- (pure . lvl)
- (pure . num)
- (\t1 t2 u v w -> pure $ rec t1 t2 u v w)
- term
+fold abs app lvl num rec (Abs l m) = abs l $ fold abs app lvl num rec m
+fold abs app lvl num rec (App a b) =
+ app (fold abs app lvl num rec a) (fold abs app lvl num rec b)
+fold _ _ lvl _ _ (Lvl n ) = lvl n
+fold _ _ _ num _ (Num Z ) = num Z
+fold abs app lvl num rec (Num (S t)) = num $ S $ fold abs app lvl num rec t
+fold abs app lvl num rec (Rec t1 t2 u v w) = rec
+ (fold abs app lvl num rec t1)
+ (fold abs app lvl num rec t2)
+ (fold abs app lvl num rec u)
+ (fold abs app lvl num rec v)
+ (fold abs app lvl num rec w)
shift :: Int -> Term -> Term
shift 0 = id
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, []))