Initial bounded iteration and unbounded minimization

3 files changed, 60 insertions, 24 deletions

diff --git a/src/Data/Mili.hs b/src/Data/Mili.hs
index 1fdaa40..f05a606 100644
--- a/src/Data/Mili.hs
+++ b/src/Data/Mili.hs
@@ -4,9 +4,22 @@ module Data.Mili
   , shift
   ) where
 
-data Term = Abs Term      -- | Abstraction
-          | App Term Term -- | Application
-          | Lvl Int       -- | de Bruijn level
+import           Prelude                 hiding ( abs
+                                                , min
+                                                )
+
+data Nat = Z | S Nat
+
+data Term = Abs Term          -- | Abstraction
+          | App Term Term     -- | Application
+          | Lvl Int           -- | de Bruijn level
+          | Num Nat           -- | Peano numeral
+          | Min Nat Term Term -- | Unbounded minimizer
+          | Itr Nat Term Term -- | Bounded iterator
+
+instance Show Nat where
+  show Z     = "0"
+  show (S n) = show (read (show n) + 1 :: Integer)
 
 instance Show Term where
   showsPrec _ (Abs m) = showString "[" . shows m . showString "]"
@@ -21,6 +34,13 @@ instance Show Term where
       . shows u
       . showString " "
       . shows f
+  showsPrec _ (Itr n u v) =
+    showString "iter "
+      . shows n
+      . showString " "
+      . shows u
+      . showString " "
+      . shows v
 
 fold
   :: (t -> t)
@@ -28,16 +48,19 @@ fold
   -> (Int -> t)
   -> (Nat -> t)
   -> (Nat -> t -> t -> 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)
+fold abs app lvl num min itr (Abs m) = abs (fold abs app lvl num min itr m)
+fold abs app lvl num min itr (App a b) =
+  app (fold abs app lvl num min itr a) (fold abs app lvl num min itr b)
+fold _ _ lvl _   _ _ (Lvl n) = lvl n
+fold _ _ _   num _ _ (Num n) = num n
+fold abs app lvl num min itr (Min n u f) =
+  min n (fold abs app lvl num min itr u) (fold abs app lvl num min itr f)
+fold abs app lvl num min itr (Itr n u v) =
+  min n (fold abs app lvl num min itr u) (fold abs app lvl num min itr v)
 
 shift :: Int -> Term -> Term
 shift 0 = id
-shift n = fold Abs App (\l -> Lvl $ l + n) Num Min
+shift n = fold Abs App (\l -> Lvl $ l + n) Num Min Itr
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 [()]