aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Data/Mili.hs28
-rw-r--r--src/Language/Mili/Analyzer.hs53
-rw-r--r--src/Language/Mili/Parser.hs6
-rw-r--r--src/Language/Mili/Reducer.hs45
4 files changed, 68 insertions, 64 deletions
diff --git a/src/Data/Mili.hs b/src/Data/Mili.hs
index 9ba832b..e5609ad 100644
--- a/src/Data/Mili.hs
+++ b/src/Data/Mili.hs
@@ -13,11 +13,11 @@ import Prelude hiding ( abs
data Nat = Z | S Term
-data Term = Abs Int Term -- | Abstraction with level
- | App Term Term -- | Application
- | Lvl Int -- | de Bruijn level
- | Num Nat -- | Peano numeral
- | Rec (Term, Nat) Term Term Term -- | Unbounded iteration
+data Term = Abs Int Term -- | Abstraction with level
+ | App Term Term -- | Application
+ | Lvl Int -- | de Bruijn level
+ | Num Nat -- | Peano numeral
+ | Rec (Term, Term) Term Term Term -- | Unbounded iteration
instance Show Nat where
show Z = "Z"
@@ -29,11 +29,11 @@ instance Show Term where
showString "(" . shows m . showString " " . shows n . showString ")"
showsPrec _ (Lvl i) = shows i
showsPrec _ (Num n) = shows n
- showsPrec _ (Rec (n, t) u v w) =
+ showsPrec _ (Rec (t1, t2) u v w) =
showString "REC ("
- . shows n
+ . shows t1
. showString ", "
- . shows t
+ . shows t2
. showString "), "
. shows u
. showString ", "
@@ -46,21 +46,21 @@ fold
-> (Term -> Term -> Term)
-> (Int -> Term)
-> (Nat -> Term)
- -> ((Term, Nat) -> Term -> Term -> Term -> Term)
+ -> ((Term, Term) -> Term -> Term -> Term -> Term)
-> Term
-> 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 _ _ 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 (t, n) u v w) = rec
- (fold abs app lvl num rec t, n) -- TODO: 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
-shift n = fold Abs App (\l -> Lvl $ l + n) Num Rec
+shift n = fold (\l m -> Abs (l + n) m) App (\l -> Lvl $ l + n) Num Rec
diff --git a/src/Language/Mili/Analyzer.hs b/src/Language/Mili/Analyzer.hs
index e0d94b7..d4996ee 100644
--- a/src/Language/Mili/Analyzer.hs
+++ b/src/Language/Mili/Analyzer.hs
@@ -17,15 +17,16 @@ import Debug.Trace
-- | A trace specifies the exact path to any subterm
type Trace = [Breadcrumb]
-data Breadcrumb = AbsD -- | Down into abstraction
- | AppL -- | Left side of application
- | AppR -- | Right side of application
- | NumS -- | Successor of number
- | RecT -- | Term of rec -- TODO: RecT2??
- | RecU -- | End of rec
- | RecV -- | Function 1 of rec
- | RecW -- | Function 2 of rec
- | Root -- | Root
+data Breadcrumb = AbsD -- | Down into abstraction
+ | AppL -- | Left side of application
+ | AppR -- | Right side of application
+ | NumS -- | Successor of number
+ | RecT1 -- | Term 1 of rec
+ | RecT2 -- | Term 2 of rec
+ | RecU -- | End of rec
+ | RecV -- | Function 1 of rec
+ | RecW -- | Function 2 of rec
+ | Root -- | Root
deriving (Eq, Show)
-- | Map abstractions to a hashmap such that de Bruijn levels correspond to traces
@@ -36,15 +37,16 @@ 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, _) 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 (RecT : t) t1
- , go n (RecU : t) u
- , go n (RecV : t) v
- , go n (RecW : t) w
+ [ go n (RecT1 : t) t1
+ , go n (RecT2 : t) t2
+ , go n (RecU : t) u
+ , go n (RecV : t) v
+ , go n (RecW : t) w
]
-- TODO: Merge these two v^
@@ -54,14 +56,19 @@ traceAbs = go 0 [Root]
traceLvl :: Term -> HashMap Int [Trace]
traceLvl = go [Root]
where
- go t (Abs _ m ) = go (AbsD : t) m
+ 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, _) u v w) = foldl1
+ 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 (RecT : t) t1, go (RecU : t) u, go (RecV : t) v, go (RecW : t) w]
+ [ go (RecT1 : t) t1
+ , go (RecT2 : t) t2
+ , go (RecU : t) u
+ , go (RecV : t) v
+ , go (RecW : t) w
+ ]
-- | Unify two two mapped traces to find levels at which the traces are no suffixes
-- | Level traces not being a suffix of abstraction traces implies nonlinearity
diff --git a/src/Language/Mili/Parser.hs b/src/Language/Mili/Parser.hs
index 958c0a8..b9f7881 100644
--- a/src/Language/Mili/Parser.hs
+++ b/src/Language/Mili/Parser.hs
@@ -101,10 +101,10 @@ rec = do
_ <- symbol "REC"
_ <- spaces
_ <- startSymbol "("
- t <- term
+ t1 <- term
_ <- spaces
_ <- startSymbol ","
- t' <- nat
+ t2 <- term
_ <- spaces
_ <- startSymbol ")"
_ <- startSymbol ","
@@ -115,7 +115,7 @@ rec = do
_ <- spaces
_ <- startSymbol ","
w <- term
- pure $ Rec (t, t') 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 c10828e..dc8c9bd 100644
--- a/src/Language/Mili/Reducer.hs
+++ b/src/Language/Mili/Reducer.hs
@@ -10,34 +10,31 @@ import Data.Mili ( Nat(..)
)
data Singleton = TermTag Term | RecTag Term Term Term Term
- deriving Show
-- TODO: There will only ever be one substitution, so don't iterate the entire tree!
--- Otherwise replace with fold
-subst :: Int -> Term -> Term -> Term
-subst l (Abs d m) s = Abs d $ subst l m s
-subst l (App a b) s = App (subst l a s) (subst l b s)
-subst l (Lvl i) s | l == i = s
- | otherwise = (Lvl i)
-subst _ (Num Z ) _ = Num Z
-subst l (Num (S m)) s = Num $ S $ subst l m s
-subst l (Rec (t1, t2) u v w) s =
- Rec (subst l t1 s, t2) (subst l u s) (subst l v s) (subst l w s)
+-- WARNING: This function also shifts the substituted term and the levels of the parent!
+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)
-machine :: Term -> [Singleton] -> (Term, [Singleton])
-machine (App a b) s = (a, TermTag b : s)
-machine (Abs l u) (TermTag t : s) = (shift (-1) (subst l u t), s)
-machine (Rec (t1, t2) u v w) s = (t1, RecTag (Num t2) u v w : s)
-machine (Num Z) (RecTag _ u _ _ : s) = (u, 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 (Num (S t1)) ((RecTag t2 u v w) : s) =
- (v, RecTag (App (App w t1) t2) u v w : s)
-machine t s = error $ show t <> show s
-
-runMachine :: [Singleton] -> Term -> Term
-runMachine s t = case machine t s of
- (t', []) -> t'
- (t', s') -> runMachine s' t'
+ 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
-- | Reduce term to normal form
nf :: Term -> Term
-nf = runMachine []
+nf t = machine t []