diff options
| -rw-r--r-- | notes | 4 | ||||
| -rw-r--r-- | readme.md | 18 | ||||
| -rw-r--r-- | samples/math.mili | 3 | ||||
| -rw-r--r-- | samples/test.lil | 11 | ||||
| -rw-r--r-- | samples/test.mili | 8 | ||||
| -rw-r--r-- | src/Data/Mili.hs | 10 | ||||
| -rw-r--r-- | src/Language/Mili/Analyzer.hs | 4 | ||||
| -rw-r--r-- | src/Language/Mili/Parser.hs | 24 | ||||
| -rw-r--r-- | src/Language/Mili/Reducer.hs | 33 |
9 files changed, 76 insertions, 39 deletions
@@ -1,4 +0,0 @@ -<+0> <-0> -<<-0>| |<+0>> -<|<+0>>| |<<-0>|> -<|<<-0>|>| |<|<+0>>|> @@ -16,14 +16,28 @@ while still benefitting from the advantages of syntactic linearity. Mili's core syntactic representation consists of only five constructs: ``` haskell -data Term = Abs Term -- | Abstraction +data Term = Abs Int Term -- | Abstraction at level | App Term Term -- | Application | Lvl Int -- | de Bruijn level | Num Nat -- | Peano numeral | Rec (Term, Nat) Term Term Term -- | Unbounded iteration ``` -This allows us to use a minimal abstract reduction machine. +Lets and Pairs are only used in the higher-level syntax. This allows us +to use a minimal abstract reduction machine. + +## roadmap + +- [x] basic syntax +- [x] linearity check +- [x] basic reduction +- [ ] type syntax +- [ ] type checking +- [ ] reduction shortcut +- [ ] preprocessor + - [ ] `:test` + - [ ] `:import` +- [ ] more examples ## references diff --git a/samples/math.mili b/samples/math.mili new file mode 100644 index 0000000..6fff8d2 --- /dev/null +++ b/samples/math.mili @@ -0,0 +1,3 @@ +add = [[REC (1, <0>), 0, [S 0], [[[0 2 1]]]]] +mul = [[REC (1, <0>), <0>, (add 0), [[[0 2 1]]]]] +add <0> <2> diff --git a/samples/test.lil b/samples/test.lil deleted file mode 100644 index e0ed6fd..0000000 --- a/samples/test.lil +++ /dev/null @@ -1,11 +0,0 @@ -foo = [ - huh = [[[0 1 2]]] - huh 0 -] - -bar = [ - huh = ([[[0 2 1]]] 0) - huh 0 -] - -foo bar diff --git a/samples/test.mili b/samples/test.mili new file mode 100644 index 0000000..d12b525 --- /dev/null +++ b/samples/test.mili @@ -0,0 +1,8 @@ +foo = [ + huh = [[[0 1 2]]] + abc = [[huh 0 1]] + def = [abc 0 huh] + def [0 1] +] + +[foo 0] diff --git a/src/Data/Mili.hs b/src/Data/Mili.hs index ac6703a..9ba832b 100644 --- a/src/Data/Mili.hs +++ b/src/Data/Mili.hs @@ -13,7 +13,7 @@ import Prelude hiding ( abs data Nat = Z | S Term -data Term = Abs Term -- | Abstraction +data Term = Abs Int Term -- | Abstraction with level | App Term Term -- | Application | Lvl Int -- | de Bruijn level | Num Nat -- | Peano numeral @@ -21,10 +21,10 @@ data Term = Abs Term -- | Abstraction instance Show Nat where show Z = "Z" - show (S t) = "S " <> show t + show (S t) = "S(" <> show t <> ")" instance Show Term where - showsPrec _ (Abs m) = showString "[" . shows m . showString "]" + showsPrec _ (Abs _ m) = showString "[" . shows m . showString "]" showsPrec _ (App m n) = showString "(" . shows m . showString " " . shows n . showString ")" showsPrec _ (Lvl i) = shows i @@ -42,14 +42,14 @@ instance Show Term where . shows w fold - :: (Term -> Term) + :: (Int -> Term -> Term) -> (Term -> Term -> Term) -> (Int -> Term) -> (Nat -> Term) -> ((Term, Nat) -> Term -> Term -> Term -> Term) -> Term -> Term -fold abs app lvl num rec (Abs m) = abs $ fold abs app lvl num rec m +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 diff --git a/src/Language/Mili/Analyzer.hs b/src/Language/Mili/Analyzer.hs index 8befe0b..e0d94b7 100644 --- a/src/Language/Mili/Analyzer.hs +++ b/src/Language/Mili/Analyzer.hs @@ -33,7 +33,7 @@ data Breadcrumb = AbsD -- | Down into abstraction traceAbs :: Term -> HashMap Int [Trace] traceAbs = go 0 [Root] where - go n t (Abs m) = + 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 @@ -54,7 +54,7 @@ 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 diff --git a/src/Language/Mili/Parser.hs b/src/Language/Mili/Parser.hs index a733ade..958c0a8 100644 --- a/src/Language/Mili/Parser.hs +++ b/src/Language/Mili/Parser.hs @@ -77,7 +77,9 @@ toLevel n = do -- | abstraction, entering increases the abstraction depth abs :: Parser Term -abs = between (startSymbol "[") (symbol "]") (Abs <$> (inc *> block <* dec)) +abs = between (startSymbol "[") + (symbol "]") + (gets (Abs <$> _depth) <*> (inc *> block <* dec)) where inc = modify $ \r@(PS { _depth = d }) -> r { _depth = d + 1 } dec = modify $ \r@(PS { _depth = d }) -> r { _depth = d - 1 } @@ -98,28 +100,22 @@ rec :: Parser Term rec = do _ <- symbol "REC" _ <- spaces - _ <- symbol "(" - _ <- spaces + _ <- startSymbol "(" t <- term _ <- spaces - _ <- symbol "," - _ <- spaces + _ <- startSymbol "," t' <- nat _ <- spaces - _ <- symbol ")" - _ <- spaces - _ <- symbol "," - _ <- spaces + _ <- startSymbol ")" + _ <- startSymbol "," u <- term _ <- spaces - _ <- symbol "," - _ <- spaces + _ <- startSymbol "," v <- term _ <- spaces - _ <- symbol "," - _ <- spaces + _ <- startSymbol "," w <- term - pure $ Rec (t, t') u v w -- TODO + pure $ Rec (t, t') 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 8074bdf..c10828e 100644 --- a/src/Language/Mili/Reducer.hs +++ b/src/Language/Mili/Reducer.hs @@ -6,7 +6,38 @@ module Language.Mili.Reducer import Data.Mili ( Nat(..) , Term(..) + , shift ) + +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) + +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 (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' + -- | Reduce term to normal form nf :: Term -> Term -nf t = t +nf = runMachine [] |