diff options
| -rw-r--r-- | src/Data/Mili.hs | 30 | ||||
| -rw-r--r-- | src/Language/Mili/Parser.hs | 13 |
2 files changed, 36 insertions, 7 deletions
diff --git a/src/Data/Mili.hs b/src/Data/Mili.hs index b407d00..1fdaa40 100644 --- a/src/Data/Mili.hs +++ b/src/Data/Mili.hs @@ -1,5 +1,7 @@ module Data.Mili ( Term(..) + , fold + , shift ) where data Term = Abs Term -- | Abstraction @@ -11,3 +13,31 @@ instance Show Term where showsPrec _ (App m n) = showString "(" . shows m . showString " " . shows n . showString ")" showsPrec _ (Lvl i) = shows i + showsPrec _ (Num n) = shows n + showsPrec _ (Min n u f) = + showString "μ" + . shows n + . showString " " + . shows u + . showString " " + . shows f + +fold + :: (t -> t) + -> (t -> t -> t) + -> (Int -> t) + -> (Nat -> t) + -> (Nat -> t -> t -> t) + -> Term + -> t +fold abs app lvl num min (Abs m) = abs (fold abs app lvl num min m) +fold abs app lvl num min (App a b) = + app (fold abs app lvl num min a) (fold abs app lvl num min b) +fold _ _ lvl _ _ (Lvl n) = lvl n +fold _ _ _ num _ (Num n) = num n +fold abs app lvl num min (Min n u f) = + min n (fold abs app lvl num min u) (fold abs app lvl num min f) + +shift :: Int -> Term -> Term +shift 0 = id +shift n = fold Abs App (\l -> Lvl $ l + n) Num Min diff --git a/src/Language/Mili/Parser.hs b/src/Language/Mili/Parser.hs index bd61254..fccd0f1 100644 --- a/src/Language/Mili/Parser.hs +++ b/src/Language/Mili/Parser.hs @@ -8,7 +8,9 @@ import Control.Monad ( void ) import Control.Monad.State import Data.HashMap.Strict ( HashMap ) import qualified Data.HashMap.Strict as M -import Data.Mili ( Term(..) ) +import Data.Mili ( Term(..) + , shift + ) import Data.Text ( Text ) import qualified Data.Text as T import Data.Void @@ -55,7 +57,6 @@ startSymbol :: Text -> Parser Text startSymbol t = symbol t <* anySpaces -- | abstraction, entering increases the abstraction depth --- TODO: There's a bug in here with open terms backtracking to increment lol abs :: Parser Term abs = between (startSymbol "[") (symbol "]") (Abs <$> (inc *> block <* dec)) where @@ -67,9 +68,7 @@ idx :: Parser Term idx = do n <- L.decimal PS { _depth = d } <- get - case d - n - 1 of - i | i < 0 -> fail "open term" - | otherwise -> pure $ Lvl i + pure $ Lvl $ d - n - 1 -- | single identifier, directly parsed to corresponding term def :: Parser Term @@ -77,8 +76,8 @@ def = do name <- identifier PS { _map = names } <- get case M.lookup name names of - Just t -> pure t - Nothing -> fail $ T.unpack name <> " is not in scope" + Just (d2, t) -> pure $ shift (d1 - d2) t + Nothing -> fail $ T.unpack name <> " is not in scope" -- | single lambda term, potentially a left application fold of many term :: Parser Term |