diff --git a/spago.dhall b/spago.dhall index d953bde..f3dbe10 100644 --- a/spago.dhall +++ b/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" diff --git a/src/Language/Bergamot/Parser.purs b/src/Language/Bergamot/Parser.purs new file mode 100644 index 0000000..b18d4fe --- /dev/null +++ b/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) diff --git a/src/Language/Bergamot/Rules.purs b/src/Language/Bergamot/Rules.purs index de5b087..9883464 100644 --- a/src/Language/Bergamot/Rules.purs +++ b/src/Language/Bergamot/Rules.purs @@ -16,7 +16,7 @@ import Data.Tuple (fst) import Data.Newtype (class Newtype) import Data.Maybe (Maybe(..)) -newtype Rule k = MkRule { name :: String, head :: Expr k, tail :: List (Expr k) } +newtype Rule k = MkRule { head :: Expr k, tail :: List (Expr k) } derive instance Newtype (Rule k) _ derive instance Functor Rule derive instance Foldable Rule @@ -26,6 +26,7 @@ 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 diff --git a/test/Main.purs b/test/Main.purs index b208b33..e0ceeca 100644 --- a/test/Main.purs +++ b/test/Main.purs @@ -4,37 +4,17 @@ 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 @@ -46,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 @@ -58,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")