From 6ed4e70af76bf29297dc872dc7501e70e20ad230 Mon Sep 17 00:00:00 2001
From: Marvin Borner
Date: Wed, 13 Nov 2024 22:49:41 +0100
Subject: Initial bounded iteration and unbounded minimization
---
src/Language/Mili/Analyzer.hs | 30 +++++++++++++++++++++---------
src/Language/Mili/Parser.hs | 9 +++++----
2 files changed, 26 insertions(+), 13 deletions(-)
(limited to 'src/Language/Mili')
diff --git a/src/Language/Mili/Analyzer.hs b/src/Language/Mili/Analyzer.hs
index a85e990..0e1118a 100644
--- a/src/Language/Mili/Analyzer.hs
+++ b/src/Language/Mili/Analyzer.hs
@@ -12,9 +12,13 @@ import Data.Mili ( Term(..) )
-- | A trace specifies the exact path to any subterm
type Trace = [Breadcrumb]
-data Breadcrumb = South -- | Down into abstraction
- | West -- | Left hand side of application
- | East -- | Right hand side of application
+data Breadcrumb = AbsD -- | Down into abstraction
+ | AppL -- | Left side of application
+ | AppR -- | Right side of application
+ | MinE -- | End case of Min
+ | MinF -- | Function of Min
+ | ItrE -- | End case of Iter
+ | ItrF -- | Function of Iter
deriving (Eq, Show)
-- | Map abstractions to a hashmap such that de Bruijn levels correspond to traces
@@ -23,18 +27,26 @@ traceAbs :: Term -> HashMap Int [Trace]
traceAbs = go 0 []
where
go n t (Abs m) =
- M.unionWith (++) (go (n + 1) (South : t) m) (M.singleton n [t])
- go n t (App a b) = M.unionWith (++) (go n (West : t) a) (go n (East : t) b)
- go _ _ (Lvl _ ) = M.empty
+ 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 _ ) = M.empty
+ go n t (Min _ u f) = M.unionWith (++) (go n (MinE : t) u) (go n (MinF : t) f)
+ go n t (Itr _ u v) = M.unionWith (++) (go n (ItrE : t) u) (go n (ItrF : t) v)
+
+-- TODO: Merge these two v^
-- | Map de Bruijn levels to a hashmap such that de Bruijn levels correspond to
-- | traces of de Bruijn levels at that level
traceLvl :: Term -> HashMap Int [Trace]
traceLvl = go []
where
- go t (Abs m ) = go (South : t) m
- go t (App a b) = M.unionWith (++) (go (West : t) a) (go (East : t) b)
- go t (Lvl l ) = M.singleton l [t]
+ 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 _ ) = M.empty
+ go t (Min _ u f) = M.unionWith (++) (go (MinE : t) u) (go (MinF : t) f)
+ go t (Itr _ u v) = M.unionWith (++) (go (ItrE : t) u) (go (ItrF : t) v)
-- | 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 fccd0f1..f9c52f3 100644
--- a/src/Language/Mili/Parser.hs
+++ b/src/Language/Mili/Parser.hs
@@ -21,7 +21,7 @@ import qualified Text.Megaparsec.Char.Lexer as L
type Parser = ParsecT Void Text (State ParserState)
data ParserState = PS
- { _map :: HashMap Text Term
+ { _map :: HashMap Text (Int, Term)
, _depth :: Int
}
@@ -73,8 +73,8 @@ idx = do
-- | single identifier, directly parsed to corresponding term
def :: Parser Term
def = do
- name <- identifier
- PS { _map = names } <- get
+ name <- identifier
+ PS { _map = names, _depth = d1 } <- get
case M.lookup name names of
Just (d2, t) -> pure $ shift (d1 - d2) t
Nothing -> fail $ T.unpack name <> " is not in scope"
@@ -98,7 +98,8 @@ definition = do
_ <- startSymbol "="
_ <- spaces
body <- term
- modify $ \r@(PS { _map = m }) -> r { _map = M.insert name body m }
+ modify $ \r@(PS { _map = m, _depth = d }) ->
+ r { _map = M.insert name (d, body) m }
-- | many definitions, seperated by newline or semicolon
definitions :: Parser [()]
--
cgit v1.2.3