Initial structure

3 files changed, 212 insertions, 0 deletions

diff --git a/src/Language/Mili/Analyzer.hs b/src/Language/Mili/Analyzer.hs
new file mode 100644
index 0000000..a85e990
--- /dev/null
+++ b/src/Language/Mili/Analyzer.hs
@@ -0,0 +1,76 @@
+module Language.Mili.Analyzer
+  ( linearity
+  ) where
+
+import           Data.HashMap.Strict            ( HashMap )
+import qualified Data.HashMap.Strict           as M
+import           Data.List                      ( intercalate
+                                                , isSuffixOf
+                                                )
+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
+  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 []
+ 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
+
+-- | 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]
+
+-- | 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
+-- TODO: Proof?
+unifyTraces :: HashMap Int [Trace] -> HashMap Int [Trace] -> HashMap Int [Bool]
+unifyTraces traceA traceB = M.fromList $ map zipMap allKeys
+ where
+  allKeys = M.keys (traceA `M.union` traceB)
+  left key = M.lookupDefault [[]] key traceA
+  right key = M.lookupDefault [[]] key traceB
+  zipMap key
+    | length (left key) == length (right key)
+    = (key, zipWith isSuffixOf (left key) (right key))
+    | otherwise
+    = (key, [False])
+
+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
+    (\(depth, _) ->
+      "Linearity divergence in depth "
+        <> show depth
+        <> "\n\t"
+        <> show (M.lookupDefault [[]] depth absTrace)
+        <> "\nvs\n\t"
+        <> show (M.lookupDefault [[]] depth lvlTrace)
+    )
+
+linearity :: Term -> Either String Term
+linearity t =
+  let absTrace = traceAbs t
+      lvlTrace = traceLvl t
+      unified  = unifyTraces absTrace lvlTrace
+      isLinear = all (all id) unified
+  in  if isLinear
+        then Right t
+        else Left $ linearityError absTrace lvlTrace unified
diff --git a/src/Language/Mili/Parser.hs b/src/Language/Mili/Parser.hs
new file mode 100644
index 0000000..bd61254
--- /dev/null
+++ b/src/Language/Mili/Parser.hs
@@ -0,0 +1,127 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Language.Mili.Parser
+  ( parseProgram
+  ) where
+
+import           Control.Monad                  ( void )
+import           Control.Monad.State
+import           Data.HashMap.Strict            ( HashMap )
+import qualified Data.HashMap.Strict           as M
+import           Data.Mili                      ( Term(..) )
+import           Data.Text                      ( Text )
+import qualified Data.Text                     as T
+import           Data.Void
+import           Prelude                 hiding ( abs )
+import           Text.Megaparsec         hiding ( State )
+import           Text.Megaparsec.Char
+import qualified Text.Megaparsec.Char.Lexer    as L
+
+type Parser = ParsecT Void Text (State ParserState)
+data ParserState = PS
+  { _map   :: HashMap Text Term
+  , _depth :: Int
+  }
+
+-- | single line comment
+lineComment :: Parser ()
+lineComment = L.skipLineComment "--"
+
+-- | multiline comment
+blockComment :: Parser ()
+blockComment = L.skipBlockComment "{-" "-}"
+
+parens :: Parser a -> Parser a
+parens = between (symbol "(") (symbol ")")
+
+-- | space consumer including comments
+spaceConsumer :: String -> Parser ()
+spaceConsumer s = L.space (void $ oneOf s) lineComment blockComment
+
+-- | multiple spaces with comments
+spaces :: Parser ()
+spaces = spaceConsumer (" \t" :: String)
+
+-- | multiple spaces and newlines with comments
+anySpaces :: Parser ()
+anySpaces = spaceConsumer (" \t\r\n" :: String)
+
+-- | arbitrary symbol consumer
+symbol :: Text -> Parser Text
+symbol = string
+
+-- | symbol consumer with arbitrary spaces behind
+startSymbol :: Text -> Parser Text
+startSymbol t = symbol t <* anySpaces
+
+-- | abstraction, entering increases the abstraction depth
+-- TODO: There's a bug in here with open terms backtracking to increment lol
+abs :: Parser Term
+abs = between (startSymbol "[") (symbol "]") (Abs <$> (inc *> block <* dec))
+ where
+  inc = modify $ \r@(PS { _depth = d }) -> r { _depth = d + 1 }
+  dec = modify $ \r@(PS { _depth = d }) -> r { _depth = d - 1 }
+
+-- | de Bruijn index, parsed to de Bruijn level
+idx :: Parser Term
+idx = do
+  n                 <- L.decimal
+  PS { _depth = d } <- get
+  case d - n - 1 of
+    i | i < 0     -> fail "open term"
+      | otherwise -> pure $ Lvl i
+
+-- | single identifier, directly parsed to corresponding term
+def :: Parser Term
+def = do
+  name                <- identifier
+  PS { _map = names } <- get
+  case M.lookup name names of
+    Just t  -> pure t
+    Nothing -> fail $ T.unpack name <> " is not in scope"
+
+-- | single lambda term, potentially a left application fold of many
+term :: Parser Term
+term = try chain <|> once
+ where
+  once  = abs <|> idx <|> def <|> parens block
+  chain = foldl1 App <$> sepEndBy1 (try once) (char ' ')
+
+-- | single identifier, a-z
+identifier :: Parser Text
+identifier = T.pack <$> some lowerChar
+
+-- | single definition, <identifier> = <term>
+definition :: Parser ()
+definition = do
+  name <- identifier
+  _    <- spaces
+  _    <- startSymbol "="
+  _    <- spaces
+  body <- term
+  modify $ \r@(PS { _map = m }) -> r { _map = M.insert name body m }
+
+-- | many definitions, seperated by newline or semicolon
+definitions :: Parser [()]
+definitions = endBy (try definition) (oneOf (";\n" :: String) <* anySpaces)
+
+-- | single "let..in" block: many definitions before a single term
+block :: Parser Term
+block = do
+  (PS { _map = m }) <- get -- backup
+  b                 <- definitions *> term
+  _                 <- anySpaces
+  modify $ \r -> r { _map = m } -- restore
+  pure b
+
+-- TODO: add preprocessor commands?
+program :: Parser Term
+program = block
+
+parseProgram :: Text -> Either String Term
+parseProgram s = prettify $ evalState
+  (runParserT (anySpaces *> program <* anySpaces <* eof) "" s)
+  PS { _map = M.empty, _depth = 0 }
+ where
+  prettify (Right t  ) = Right t
+  prettify (Left  err) = Left $ errorBundlePretty err
diff --git a/src/Language/Mili/Reducer.hs b/src/Language/Mili/Reducer.hs
new file mode 100644
index 0000000..a65e018
--- /dev/null
+++ b/src/Language/Mili/Reducer.hs
@@ -0,0 +1,9 @@
+module Language.Mili.Reducer
+  ( nf
+  ) where
+
+import           Data.Mili                      ( Term(..) )
+
+-- | Reduce term to normal form
+nf :: Term -> Term
+nf m = m