Unbounded iteration

3 files changed, 101 insertions, 31 deletions

diff --git a/src/Language/Mili/Analyzer.hs b/src/Language/Mili/Analyzer.hs
index 0e1118a..8befe0b 100644
--- a/src/Language/Mili/Analyzer.hs
+++ b/src/Language/Mili/Analyzer.hs
@@ -1,3 +1,5 @@
+-- MIT License, Copyright (c) 2024 Marvin Borner
+
 module Language.Mili.Analyzer
   ( linearity
   ) where
@@ -7,7 +9,10 @@ import qualified Data.HashMap.Strict           as M
 import           Data.List                      ( intercalate
                                                 , isSuffixOf
                                                 )
-import           Data.Mili                      ( Term(..) )
+import           Data.Mili                      ( Nat(..)
+                                                , Term(..)
+                                                )
+import           Debug.Trace
 
 -- | A trace specifies the exact path to any subterm
 type Trace = [Breadcrumb]
@@ -15,38 +20,48 @@ type Trace = [Breadcrumb]
 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
+                | 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
   deriving (Eq, Show)
 
 -- | Map abstractions to a hashmap such that de Bruijn levels correspond to traces
 -- | of abstractions at that level
 traceAbs :: Term -> HashMap Int [Trace]
-traceAbs = go 0 []
+traceAbs = go 0 [Root]
  where
   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 _    ) = 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)
+  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
+    (M.unionWith (++))
+    [ go n (RecT : t) t1
+    , go n (RecU : t) u
+    , go n (RecV : t) v
+    , go n (RecW : t) w
+    ]
 
 -- 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 []
+traceLvl = go [Root]
  where
-  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)
+  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
+    (M.unionWith (++))
+    [go (RecT : t) t1, 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
@@ -67,9 +82,9 @@ linearityError
   :: HashMap Int [Trace] -> HashMap Int [Trace] -> HashMap Int [Bool] -> String
 linearityError absTrace lvlTrace = pretty . filter (any not . snd) . M.toList
  where
-  pretty = intercalate "\n" . map
+  pretty = intercalate "\n\n" . map
     (\(depth, _) ->
-      "Linearity divergence in depth "
+      "Linearity divergence at depth "
         <> show depth
         <> "\n\t"
         <> show (M.lookupDefault [[]] depth absTrace)
@@ -85,4 +100,5 @@ linearity t =
       isLinear = all (all id) unified
   in  if isLinear
         then Right t
-        else Left $ linearityError absTrace lvlTrace unified
+        else trace (show t <> "\n" <> show absTrace <> "\n" <> show lvlTrace)
+                   (Left $ linearityError absTrace lvlTrace unified)
diff --git a/src/Language/Mili/Parser.hs b/src/Language/Mili/Parser.hs
index f9c52f3..a733ade 100644
--- a/src/Language/Mili/Parser.hs
+++ b/src/Language/Mili/Parser.hs
@@ -1,3 +1,5 @@
+-- MIT License, Copyright (c) 2024 Marvin Borner
+
 {-# LANGUAGE OverloadedStrings #-}
 
 module Language.Mili.Parser
@@ -6,15 +8,19 @@ module Language.Mili.Parser
 
 import           Control.Monad                  ( void )
 import           Control.Monad.State
+import           Data.Functor                   ( ($>) )
 import           Data.HashMap.Strict            ( HashMap )
 import qualified Data.HashMap.Strict           as M
-import           Data.Mili                      ( Term(..)
+import           Data.Mili                      ( Nat(..)
+                                                , Term(..)
                                                 , shift
                                                 )
 import           Data.Text                      ( Text )
 import qualified Data.Text                     as T
 import           Data.Void
-import           Prelude                 hiding ( abs )
+import           Prelude                 hiding ( abs
+                                                , min
+                                                )
 import           Text.Megaparsec         hiding ( State )
 import           Text.Megaparsec.Char
 import qualified Text.Megaparsec.Char.Lexer    as L
@@ -56,6 +62,19 @@ symbol = string
 startSymbol :: Text -> Parser Text
 startSymbol t = symbol t <* anySpaces
 
+-- | natural number
+nat :: Parser Nat
+nat = natify <$> between (startSymbol "<") (symbol ">") L.decimal
+ where
+  natify 0 = Z
+  natify n = S $ Num $ natify (n - 1 :: Integer)
+
+-- | convert de Bruijn indices to levels
+toLevel :: Int -> Parser Term
+toLevel n = do
+  PS { _depth = d } <- get
+  pure $ Lvl $ d - n - 1
+
 -- | abstraction, entering increases the abstraction depth
 abs :: Parser Term
 abs = between (startSymbol "[") (symbol "]") (Abs <$> (inc *> block <* dec))
@@ -65,10 +84,42 @@ abs = between (startSymbol "[") (symbol "]") (Abs <$> (inc *> block <* dec))
 
 -- | de Bruijn index, parsed to de Bruijn level
 idx :: Parser Term
-idx = do
-  n                 <- L.decimal
-  PS { _depth = d } <- get
-  pure $ Lvl $ d - n - 1
+idx = L.decimal >>= toLevel
+
+-- | single number: <n> | S <term> | Z
+num :: Parser Term
+num =
+  (Num <$> nat)
+    <|> (Num <$> ((string "S" *> spaces $> S) <*> term))
+    <|> (Num <$> (string "Z" $> Z))
+
+-- | unbounded iterator: REC (<term>, <nat>), <term>, <term>, <term>
+rec :: Parser Term
+rec = do
+  _  <- symbol "REC"
+  _  <- spaces
+  _  <- symbol "("
+  _  <- spaces
+  t  <- term
+  _  <- spaces
+  _  <- symbol ","
+  _  <- spaces
+  t' <- nat
+  _  <- spaces
+  _  <- symbol ")"
+  _  <- spaces
+  _  <- symbol ","
+  _  <- spaces
+  u  <- term
+  _  <- spaces
+  _  <- symbol ","
+  _  <- spaces
+  v  <- term
+  _  <- spaces
+  _  <- symbol ","
+  _  <- spaces
+  w  <- term
+  pure $ Rec (t, t') u v w -- TODO
 
 -- | single identifier, directly parsed to corresponding term
 def :: Parser Term
@@ -83,7 +134,7 @@ def = do
 term :: Parser Term
 term = try chain <|> once
  where
-  once  = abs <|> idx <|> def <|> parens block
+  once  = abs <|> idx <|> num <|> rec <|> def <|> parens block
   chain = foldl1 App <$> sepEndBy1 (try once) (char ' ')
 
 -- | single identifier, a-z
diff --git a/src/Language/Mili/Reducer.hs b/src/Language/Mili/Reducer.hs
index a65e018..8074bdf 100644
--- a/src/Language/Mili/Reducer.hs
+++ b/src/Language/Mili/Reducer.hs
@@ -1,9 +1,12 @@
+-- MIT License, Copyright (c) 2024 Marvin Borner
+
 module Language.Mili.Reducer
   ( nf
   ) where
 
-import           Data.Mili                      ( Term(..) )
-
+import           Data.Mili                      ( Nat(..)
+                                                , Term(..)
+                                                )
 -- | Reduce term to normal form
 nf :: Term -> Term
-nf m = m
+nf t = t