Add a parser and use it for reading rules and queries

spago.dhall

@@ -12,8 +12,10 @@ to generate this file without the comments in this block.
 -}
 { name = "bergamot"
 , dependencies =
-  [ "bifunctors"
+  [ "arrays"
+  , "bifunctors"
   , "control"
+  , "either"
   , "foldable-traversable"
   , "lazy"
   , "lists"
@@ -21,7 +23,9 @@ to generate this file without the comments in this block.
   , "maybe"
   , "newtype"
   , "ordered-collections"
+  , "parsing"
   , "prelude"
+  , "strings"
   , "transformers"
   , "tuples"
   , "unifyt"

src/Language/Bergamot/Parser.purs

@@ -0,0 +1,57 @@
+module Language.Bergamot.Parser where
+
+import Prelude
+
+
+import Language.Bergamot.Syntax (Expr(..))
+import Language.Bergamot.Rules (Rule(..), Metavariable)
+
+import Control.Apply (lift2)
+import Control.Lazy (defer)
+import Parsing (Parser, runParser)
+import Parsing.String (char, eof, string)
+import Parsing.String.Basic (digit, letter, space)
+import Parsing.Combinators (many, many1, sepBy, (<|>))
+import Data.Array (fromFoldable)
+import Data.Either (hush)
+import Data.List (List(..))
+import Data.List.NonEmpty (NonEmptyList)
+import Data.Maybe (Maybe)
+import Data.String (codePointFromChar, fromCodePointArray)
+
+charsToString :: NonEmptyList Char -> String
+charsToString = fromCodePointArray <<< fromFoldable <<< map codePointFromChar
+
+whitespace :: Parser String Unit
+whitespace = void $ many space
+
+identifier :: Parser String String
+identifier = (charsToString <$> many1 (letter <|> digit <|> char '_')) <* whitespace
+
+expr :: Parser String (Expr Metavariable)
+expr = (defer $ \_ -> atom) <|> (defer $ \_ -> metavariable)
+
+atom :: Parser String (Expr Metavariable)
+atom = lift2 Atom (identifier <* whitespace) (args <|> pure Nil)
+    where args = char '(' *> sepBy (defer $ \_ -> expr) (char ',' *> whitespace) <* char ')' <* whitespace
+
+metavariable :: Parser String (Expr Metavariable)
+metavariable = Var <$> (char '?' *> identifier <* whitespace)
+
+rule :: Parser String (Rule Metavariable)
+rule = map MkRule $ pure { head: _, tail: _ } <*> expr <*> (args <|> pure Nil) <* char ';' <* whitespace
+    where
+        arrow = (void (char '←') <|> void (string "<-")) <* whitespace
+        args = arrow *> sepBy expr (char ',' *> whitespace) <* whitespace
+
+rules :: Parser String (List (Rule Metavariable))
+rules = many rule
+
+parseRule :: String -> Maybe (Rule Metavariable)
+parseRule s = hush $ runParser s (rule <* eof)
+
+parseRules :: String -> Maybe (List (Rule Metavariable))
+parseRules s = hush $ runParser s (rules <* eof)
+
+parseQuery :: String -> Maybe (Expr Metavariable)
+parseQuery s = hush $ runParser s (expr <* eof)

src/Language/Bergamot/Rules.purs

@@ -0,0 +1,43 @@
+module Language.Bergamot.Rules where
+
+import Prelude
+
+import Language.Bergamot.Syntax (Expr)
+
+import Control.Monad.State.Trans (runStateT)
+import Control.Monad.State.Class (class MonadState, gets, modify)
+import Control.Monad.Unify.Class (class MonadUnify, fresh)
+import Data.List (List)
+import Data.Traversable (class Traversable, traverse)
+import Data.Foldable (class Foldable)
+import Data.Map (Map, lookup, insert)
+import Data.Map as Map
+import Data.Tuple (fst)
+import Data.Newtype (class Newtype)
+import Data.Maybe (Maybe(..))
+
+newtype Rule k = MkRule { head :: Expr k, tail :: List (Expr k) }
+derive instance Newtype (Rule k) _
+derive instance Functor Rule
+derive instance Foldable Rule
+derive instance Traversable Rule
+
+type Metavariable = String
+type Metavariables k = Map Metavariable k
+
+newtype ProofTree k = MkProofTree { claim :: Expr k, rule :: Rule Metavariable, witnesses :: List (ProofTree k) }
+derive instance Functor ProofTree
+
+metavariable :: forall k f m. MonadState (Metavariables k) m => MonadUnify k f m => Metavariable -> m k
+metavariable s = do
+    r <- gets (lookup s)
+    case r of
+        Just v -> pure v
+        Nothing -> do
+           v <- fresh
+           modify (insert s v) *> pure v
+
+-- note: unification expression ef not the same as functor-to-instantiate f, this way we can instantiate
+-- things that contain expression etc.
+instantiate :: forall k f ef m. Traversable f => MonadUnify k ef m => f Metavariable -> m (f k)
+instantiate f = map fst $ runStateT (traverse metavariable f) Map.empty

src/Language/Bergamot/Syntax.purs

@@ -2,39 +2,11 @@ module Language.Bergamot.Syntax where
 
 import Prelude
 
-import Control.Plus (class Plus, empty)
-import Control.Monad (class Monad)
-import Control.Monad.State.Trans (StateT, runStateT)
-import Control.Monad.State.Class (class MonadState, gets, modify)
-import Control.Apply (class Apply, apply, lift2)
-import Control.Alt (class Alt, alt)
-import Control.Alternative (class Alternative)
-import Control.Applicative (class Applicative, pure, (*>))
-import Control.Bind (class Bind, bind, join, (>>=))
-import Control.MonadPlus (class MonadPlus)
-import Control.Monad.Reader.Class (class MonadReader, class MonadAsk, local, ask, asks)
-import Control.Monad.Logic.Class (class MonadLogic, msplit, interleave)
-import Control.Monad.Unify.Class (class MonadUnify, class Unifiable, class UnificationVariable, Stream(..), squash, alongside, ComparisonAction(..), fresh, unify, reify)
-import Control.Monad.Reader.Trans (ReaderT, runReaderT)
-import Control.Monad.Unify.Trans (UnifyT(..), runUnifyT)
-import Control.Monad.Logic.Trans (SFKT(..), runSFKTOnce)
-import Control.Monad.State.Trans (StateT(..), runStateT)
-import Data.List (List(..), (:), fromFoldable)
-import Data.Functor (class Functor, (<$>), map)
-import Data.Eq (class Eq)
-import Data.Ord (class Ord)
-import Data.Traversable (class Traversable, sequence, traverse, oneOf)
-import Data.Foldable (class Foldable, foldr, foldl, foldMap, any, intercalate)
-import Data.Monoid ((<>), mempty)
-import Data.Map (Map, lookup, insert)
-import Data.Map as Map
-import Data.Set (Set, singleton, union)
-import Data.Tuple (Tuple(..), fst)
-import Data.Tuple.Nested ((/\))
-import Data.Lazy (Lazy, defer, force)
-import Data.Newtype (class Newtype, un, over2)
-import Data.Maybe (Maybe(..), fromMaybe, isJust)
-import Data.Bifunctor (rmap)
+import Control.Monad.Unify.Class (class Unifiable, class UnificationVariable, Stream(..), squash, alongside, ComparisonAction(..))
+import Data.Foldable (class Foldable)
+import Data.Traversable (class Traversable)
+import Data.Lazy (defer)
+import Data.List (List(..), (:))
 
 data Expr v
     = Var v
@@ -67,83 +39,3 @@ instance UnificationVariable k => Unifiable k Expr where
           combine (_:_) Nil = (Var Fail) : Nil
           combine Nil (_:_) = (Var Fail) : Nil
           combine (x:xs) (y:ys) = alongside x y : combine xs ys
-
--- note: unification expression ef not the same as functor-to-instantiate f, this way we can instantiate
--- things that contain expression etc.
-instantiate :: forall k f ef m. Traversable f => MonadUnify k ef m => f Metavariable -> m (f k)
-instantiate f = map fst $ runStateT (traverse metavariable f) Map.empty
-
-newtype Rule k = MkRule { name :: String, head :: Expr k, tail :: List (Expr k) }
-derive instance Newtype (Rule k) _
-derive instance Functor Rule
-derive instance Foldable Rule
-derive instance Traversable Rule
-
-type UnifierEnv = { rules :: Array (Rule Metavariable), fuel :: Int }
-newtype Unifier a = MkUnifier (UnifyT IntVar Expr (ReaderT UnifierEnv (SFKT Maybe)) a)
-
-derive instance Newtype (Unifier a) _
-derive newtype instance Functor Unifier
-derive newtype instance Apply Unifier
-derive newtype instance Applicative Unifier
-derive newtype instance Alt Unifier
-derive newtype instance Plus Unifier
-derive newtype instance Alternative Unifier
-derive newtype instance Bind Unifier
-derive newtype instance Monad Unifier
-derive newtype instance MonadPlus Unifier
-derive newtype instance MonadUnify IntVar Expr Unifier
-
--- >:(
-instance MonadAsk UnifierEnv Unifier where
-    ask = MkUnifier $ MkUnifyT ask
-
--- >:(
-instance MonadReader UnifierEnv Unifier where
-    local f m = MkUnifier $ MkUnifyT $ StateT $ \s -> local f (runStateT (un MkUnifyT $ un MkUnifier m) s)
-
--- >:(
-instance MonadLogic Unifier where
-    msplit m = MkUnifier $ MkUnifyT $ map (map (rmap (MkUnifier <<< MkUnifyT))) $ msplit $ un MkUnifyT $ un MkUnifier m
-    interleave = over2 MkUnifier (over2 MkUnifyT interleave)
-
-spend :: forall a. Unifier a -> Unifier a
-spend m = do
-    n <- asks _.fuel
-    if n > 0 then local (_ { fuel = n - 1}) m else empty
-
-type Metavariable = String
-type Metavariables k = Map Metavariable k
-
-metavariable :: forall k f m. MonadState (Metavariables k) m => MonadUnify k f m => Metavariable -> m k
-metavariable s = do
-    r <- gets (lookup s)
-    case r of
-        Just v -> pure v
-        Nothing -> do
-           v <- fresh
-           modify (insert s v) *> pure v
-
-
-newtype ProofTree k = MkProofTree { claim :: Expr k, rule :: Rule Metavariable, witnesses :: List (ProofTree k) }
-
-match :: Array (Rule Metavariable) -> Expr IntVar -> Unifier (ProofTree IntVar)
-match rs e = oneOf $ map (matchSingle e) rs
-    where
-      matchSingle e' rule = spend $ do
-         MkRule {head, tail} <- instantiate rule
-         _ <- unify e' head
-         witnesses <- traverse (match rs) tail
-         pure $ MkProofTree { claim: e, rule: rule, witnesses: witnesses }
-
-reifyProofTree :: ProofTree IntVar -> Unifier (ProofTree IntVar)
-reifyProofTree (MkProofTree {claim, rule, witnesses}) = do
-    claim' <- reify claim
-    witnesses' <- traverse reifyProofTree witnesses
-    pure $ MkProofTree $ { claim: claim', rule: rule, witnesses: witnesses' }
-
-query :: Expr Metavariable -> Unifier (ProofTree IntVar)
-query e = (join $ lift2 match (asks _.rules) (instantiate e)) >>= reifyProofTree
-
-runUnifier :: forall a. Array (Rule Metavariable) -> Unifier a -> Maybe a
-runUnifier rs m = runSFKTOnce (fst <$> (runReaderT (runUnifyT $ un MkUnifier m) { rules: rs, fuel: 10 }))

src/Language/Bergamot/Unifier.purs

@@ -0,0 +1,78 @@
+module Language.Bergamot.Unifier where
+
+import Prelude
+
+import Language.Bergamot.Rules (Metavariable, ProofTree(..), Rule(..), instantiate)
+import Language.Bergamot.Syntax (Expr, IntVar)
+
+import Control.Plus (class Plus, empty)
+import Control.Apply (lift2)
+import Control.Alt (class Alt)
+import Control.Alternative (class Alternative)
+import Control.MonadPlus (class MonadPlus)
+import Control.Monad.Reader.Class (class MonadReader, class MonadAsk, local, ask, asks)
+import Control.Monad.Logic.Class (class MonadLogic, msplit, interleave)
+import Control.Monad.Unify.Class (class MonadUnify, unify, reify)
+import Control.Monad.Reader.Trans (ReaderT, runReaderT)
+import Control.Monad.Unify.Trans (UnifyT(..), runUnifyT)
+import Control.Monad.Logic.Trans (SFKT, runSFKTOnce)
+import Control.Monad.State.Trans (StateT(..), runStateT)
+import Data.Traversable (traverse, oneOf)
+import Data.Tuple (fst)
+import Data.Newtype (class Newtype, un, over2)
+import Data.Maybe (Maybe)
+import Data.Bifunctor (rmap)
+
+type UnifierEnv = { rules :: Array (Rule Metavariable), fuel :: Int }
+newtype Unifier a = MkUnifier (UnifyT IntVar Expr (ReaderT UnifierEnv (SFKT Maybe)) a)
+
+derive instance Newtype (Unifier a) _
+derive newtype instance Functor Unifier
+derive newtype instance Apply Unifier
+derive newtype instance Applicative Unifier
+derive newtype instance Alt Unifier
+derive newtype instance Plus Unifier
+derive newtype instance Alternative Unifier
+derive newtype instance Bind Unifier
+derive newtype instance Monad Unifier
+derive newtype instance MonadPlus Unifier
+derive newtype instance MonadUnify IntVar Expr Unifier
+
+-- >:(
+instance MonadAsk UnifierEnv Unifier where
+    ask = MkUnifier $ MkUnifyT ask
+
+-- >:(
+instance MonadReader UnifierEnv Unifier where
+    local f m = MkUnifier $ MkUnifyT $ StateT $ \s -> local f (runStateT (un MkUnifyT $ un MkUnifier m) s)
+
+-- >:(
+instance MonadLogic Unifier where
+    msplit m = MkUnifier $ MkUnifyT $ map (map (rmap (MkUnifier <<< MkUnifyT))) $ msplit $ un MkUnifyT $ un MkUnifier m
+    interleave = over2 MkUnifier (over2 MkUnifyT interleave)
+
+spend :: forall a. Unifier a -> Unifier a
+spend m = do
+    n <- asks _.fuel
+    if n > 0 then local (_ { fuel = n - 1}) m else empty
+
+match :: Array (Rule Metavariable) -> Expr IntVar -> Unifier (ProofTree IntVar)
+match rs e = oneOf $ map (matchSingle e) rs
+    where
+      matchSingle e' rule = spend $ do
+         MkRule {head, tail} <- instantiate rule
+         _ <- unify e' head
+         witnesses <- traverse (match rs) tail
+         pure $ MkProofTree { claim: e, rule: rule, witnesses: witnesses }
+
+reifyProofTree :: ProofTree IntVar -> Unifier (ProofTree IntVar)
+reifyProofTree (MkProofTree {claim, rule, witnesses}) = do
+    claim' <- reify claim
+    witnesses' <- traverse reifyProofTree witnesses
+    pure $ MkProofTree $ { claim: claim', rule: rule, witnesses: witnesses' }
+
+query :: Expr Metavariable -> Unifier (ProofTree IntVar)
+query e = (join $ lift2 match (asks _.rules) (instantiate e)) >>= reifyProofTree
+
+runUnifier :: forall a. Array (Rule Metavariable) -> Unifier a -> Maybe a
+runUnifier rs m = runSFKTOnce (fst <$> (runReaderT (runUnifyT $ un MkUnifier m) { rules: rs, fuel: 10 }))

test/Main.purs

@@ -2,37 +2,19 @@ module Test.Main where
 
 import Prelude
 import Language.Bergamot.Syntax
+import Language.Bergamot.Rules
+import Language.Bergamot.Unifier
+import Language.Bergamot.Parser
+import Control.Apply
 import Control.Monad.Logic.Trans
 import Control.Monad.Logic.Class
 import Control.Monad.Unify.Trans
 import Control.Monad.Unify.Class
-import Data.List
+import Data.List (List(..), (:))
+import Data.Array (fromFoldable)
+import Data.Foldable
 import Data.Maybe
 
-rules :: Array (Rule Metavariable)
-rules =
-    [ MkRule { name: "TInt", head: tType tIntExpr tInt, tail: Nil }
-    , MkRule { name: "TString", head: tType tStringExpr tString, tail: Nil }
-    , MkRule { name: "TPlusInt", head: tType (tPlusExpr (Var "e1") (Var "e2")) tInt, tail: fromFoldable
-        [ tType (Var "e1") tInt
-        , tType (Var "e2") tInt
-        ] }
-    , MkRule { name: "TPlusString", head: tType (tPlusExpr (Var "e1") (Var "e2")) tString, tail: fromFoldable
-        [ tType (Var "e1") tString
-        , tType (Var "e2") tString
-        ] }
-    , MkRule { name: "TPair", head: tType (tProdExpr (Var "e1") (Var "e2")) (tProd (Var "t1") (Var "t2")), tail: fromFoldable
-        [ tType (Var "e1") (Var "t1")
-        , tType (Var "e2") (Var "t2")
-        ] }
-    , MkRule { name: "TFst", head: tType (tFstExpr (Var "e")) (Var "t1"), tail: fromFoldable
-        [ tType (Var "e") (tProd (Var "t1") (Var "t2"))
-        ] }
-    , MkRule { name: "TSnd", head: tType (tSndExpr (Var "e")) (Var "t2"), tail: fromFoldable
-        [ tType (Var "e") (tProd (Var "t1") (Var "t2"))
-        ] }
-    ]
-          
 tType et tt = Atom "type" $ et : tt : Nil
 tInt = Atom "int" Nil                                      
 tString = Atom "string" Nil                                
@@ -44,11 +26,11 @@ tProdExpr et1 et2 = Atom "pair" $ et1 : et2 : Nil
 tFstExpr et = Atom "fst" $ et : Nil
 tSndExpr et = Atom "snd" $ et : Nil
 
-toLatexExpr :: Expr IntVar -> String
+toLatexExpr :: Expr String -> String
 toLatexExpr (Atom "type" (t1 : t2 : Nil)) = toLatexExpr t1 <> " : " <> toLatexExpr t2
 toLatexExpr (Atom "int" Nil) = "\\text{int}"
 toLatexExpr (Atom "string" Nil) = "\\text{string}"
-toLatexExpr (Atom "prod" (t1 : t2 : Nil)) = toLatexExpr t1 <> "\\times" <> toLatexExpr t2
+toLatexExpr (Atom "prod" (t1 : t2 : Nil)) = toLatexExpr t1 <> "\\times " <> toLatexExpr t2
 toLatexExpr (Atom "n" Nil) = "n"
 toLatexExpr (Atom "s" Nil) = "s"
 toLatexExpr (Atom "plus" (t1 : t2 : Nil)) = toLatexExpr t1 <> " + " <> toLatexExpr t2
@@ -56,11 +38,14 @@ toLatexExpr (Atom "pair" (t1 : t2 : Nil)) = "(" <> toLatexExpr t1 <> ", " <> toL
 toLatexExpr (Atom "fst" (t : Nil)) = "\\text{fst}\\ " <> toLatexExpr t
 toLatexExpr (Atom "snd" (t : Nil)) = "\\text{snd}\\ " <> toLatexExpr t
 toLatexExpr (Atom s xs) = "\\text{" <> s <> "}(" <> intercalate ", " (toLatexExpr <$> xs) <> ")"
-toLatexExpr (Var _) = "?"
+toLatexExpr (Var x) = x
 
-toLatexProofTree :: ProofTree IntVar -> String
-toLatexProofTree (MkProofTree {claim, witnesses}) = "\\cfrac{" <> intercalate "\\quad" (toLatexProofTree <$> witnesses) <> "}{" <> toLatexExpr claim <> "}"
+toLatexRule :: Rule String -> String
+toLatexRule (MkRule {head, tail}) = "\\cfrac{" <> intercalate "\\quad " (toLatexExpr <$> tail) <> "}{" <> toLatexExpr head <> "}"
 
-main :: Maybe String
-main = map toLatexProofTree $ runUnifier rules $ query $ tType (Var "e") (tProd tInt (tProd tInt tString))
+toLatexProofTree :: ProofTree String -> String
+toLatexProofTree (MkProofTree {claim, witnesses}) = "\\cfrac{" <> intercalate "\\quad " (toLatexProofTree <$> witnesses) <> "}{" <> toLatexExpr claim <> "}"
+
+main :: String -> String -> Maybe String
+main rs q = map (toLatexProofTree <<< map (const "?")) $ join $ lift2 runUnifier (fromFoldable <$> parseRules rs) (query <$> parseQuery q)
 -- main = map toLatexProofTree $ runUnifier rules $ query $ tType (tSndExpr (tProdExpr tStringExpr (tPlusExpr tIntExpr tIntExpr))) (Var "T")