diff options
Diffstat (limited to 'src/Language')
| -rw-r--r-- | src/Language/Mili/Analyzer.hs | 58 | ||||
| -rw-r--r-- | src/Language/Mili/Parser.hs | 65 | ||||
| -rw-r--r-- | src/Language/Mili/Reducer.hs | 9 |
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 |