aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorMarvin Borner2024-11-14 15:49:48 +0100
committerMarvin Borner2024-11-14 15:49:48 +0100
commitd7bbded8b0aa3086692b2363076be48c2fbb5a33 (patch)
tree467dcfce4fab61ffdf8840e5eea10ec675356ee4 /src
parent6ed4e70af76bf29297dc872dc7501e70e20ad230 (diff)
Unbounded iteration
Diffstat (limited to 'src')
-rw-r--r--src/Data/Mili.hs74
-rw-r--r--src/Language/Mili/Analyzer.hs58
-rw-r--r--src/Language/Mili/Parser.hs65
-rw-r--r--src/Language/Mili/Reducer.hs9
4 files changed, 138 insertions, 68 deletions
diff --git a/src/Data/Mili.hs b/src/Data/Mili.hs
index f05a606..ac6703a 100644
--- a/src/Data/Mili.hs
+++ b/src/Data/Mili.hs
@@ -1,5 +1,8 @@
+-- MIT License, Copyright (c) 2024 Marvin Borner
+
module Data.Mili
( Term(..)
+ , Nat(..)
, fold
, shift
) where
@@ -8,18 +11,17 @@ import Prelude hiding ( abs
, min
)
-data Nat = Z | S Nat
+data Nat = Z | S Term
-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
+data Term = Abs Term -- | Abstraction
+ | App Term Term -- | Application
+ | Lvl Int -- | de Bruijn level
+ | Num Nat -- | Peano numeral
+ | Rec (Term, Nat) Term Term Term -- | Unbounded iteration
instance Show Nat where
- show Z = "0"
- show (S n) = show (read (show n) + 1 :: Integer)
+ show Z = "Z"
+ show (S t) = "S " <> show t
instance Show Term where
showsPrec _ (Abs m) = showString "[" . shows m . showString "]"
@@ -27,40 +29,38 @@ instance Show Term where
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
- showsPrec _ (Itr n u v) =
- showString "iter "
+ showsPrec _ (Rec (n, t) u v w) =
+ showString "REC ("
. shows n
- . showString " "
+ . showString ", "
+ . shows t
+ . showString "), "
. shows u
- . showString " "
+ . showString ", "
. shows v
+ . showString ", "
+ . shows w
fold
- :: (t -> t)
- -> (t -> t -> t)
- -> (Int -> t)
- -> (Nat -> t)
- -> (Nat -> t -> t -> t)
- -> (Nat -> t -> t -> t)
+ :: (Term -> Term)
+ -> (Term -> Term -> Term)
+ -> (Int -> Term)
+ -> (Nat -> Term)
+ -> ((Term, Nat) -> Term -> Term -> Term -> Term)
+ -> Term
-> Term
- -> t
-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)
+fold abs app lvl num rec (Abs m) = abs $ 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
+fold _ _ _ num _ (Num Z ) = num Z
+fold abs app lvl num rec (Num (S t)) = num $ S $ fold abs app lvl num rec t
+fold abs app lvl num rec (Rec (t, n) u v w) = rec
+ (fold abs app lvl num rec t, n) -- TODO: t'
+ (fold abs app lvl num rec u)
+ (fold abs app lvl num rec v)
+ (fold abs app lvl num rec w)
shift :: Int -> Term -> Term
shift 0 = id
-shift n = fold Abs App (\l -> Lvl $ l + n) Num Min Itr
+shift n = fold Abs App (\l -> Lvl $ l + n) Num Rec
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