diff options
Diffstat (limited to 'src/Language/Mili/Analyzer.hs')
| -rw-r--r-- | src/Language/Mili/Analyzer.hs | 58 |
1 files changed, 37 insertions, 21 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) |