Add an isInt primitive predicate

packages.dhall

@@ -104,7 +104,7 @@ let upstream =
 
 in  upstream
     with logict.repo = "https://dev.danilafe.com/Everything-I-Know-About-Types/logict.git"
-    with logict.version = "a2d2b10e86beb2769245502e7f5dec4592bb2a2a"
+    with logict.version = "e19721af5e5fe172e93ebed1777e4718981516ef"
     with logict.dependencies = [ "control", "lists", "maybe", "prelude", "transformers", "tuples" ]
     with unifyt.repo = "https://dev.danilafe.com/Everything-I-Know-About-Types/unifyt.git"
     with unifyt.version = "590306964c59b8828b66b8d020283c8efaf2170b"

spago.dhall

@@ -17,6 +17,7 @@ to generate this file without the comments in this block.
   , "control"
   , "either"
   , "foldable-traversable"
+  , "integers"
   , "lazy"
   , "lists"
   , "logict"

src/Language/Bergamot/Latex.purs

@@ -0,0 +1,38 @@
+module Language.Bergamot.Latex where
+
+import Prelude
+
+import Language.Bergamot.Syntax (Expr(..))
+import Language.Bergamot.Rules (Rule(..), ProofTree(..))
+import Data.Foldable (intercalate)
+import Data.List (List(..), (:))
+
+class ToLatex a where
+    toLatex :: a -> String
+
+instance toLatexString :: ToLatex String where
+    toLatex s = s
+
+instance toLatexExpr :: ToLatex k => ToLatex (Expr k) where
+    toLatex (Atom "type" (t1 : t2 : Nil)) = toLatex t1 <> " : " <> toLatex t2
+    toLatex (Atom "int" Nil) = "\\text{int}"
+    toLatex (Atom "string" Nil) = "\\text{string}"
+    toLatex (Atom "prod" (t1 : t2 : Nil)) = toLatex t1 <> "\\times " <> toLatex t2
+    toLatex (Atom "n" Nil) = "n"
+    toLatex (Atom "s" Nil) = "s"
+    toLatex (Atom "plus" (t1 : t2 : Nil)) = toLatex t1 <> " + " <> toLatex t2
+    toLatex (Atom "pair" (t1 : t2 : Nil)) = "(" <> toLatex t1 <> ", " <> toLatex t2 <> ")"
+    toLatex (Atom "fst" (t : Nil)) = "\\text{fst}\\ " <> toLatex t
+    toLatex (Atom "snd" (t : Nil)) = "\\text{snd}\\ " <> toLatex t
+    toLatex (Atom "isInt" (t : Nil)) = toLatex t <> " \\in \\mathbb{Z}"
+    toLatex (Atom s xs) = "\\text{" <> s <> "}(" <> intercalate ", " (toLatex <$> xs) <> ")"
+    toLatex (Var x) = toLatex x
+    toLatex (IntLit i) = show i
+    toLatex (StringLit s) = "\"" <> s <> "\""
+
+instance toLatexRule :: ToLatex k => ToLatex (Rule k) where
+    toLatex (MkRule {head, tail}) = "\\cfrac{" <> intercalate "\\quad " (toLatex <$> tail) <> "}{" <> toLatex head <> "}"
+
+instance toLatexTree :: ToLatex k => ToLatex (ProofTree k) where
+    toLatex (MkProofTree {claim, witnesses: Nil}) = toLatex claim
+    toLatex (MkProofTree {claim, witnesses}) = "\\cfrac{" <> intercalate "\\quad " (toLatex <$> witnesses) <> "}{" <> toLatex claim <> "}"

src/Language/Bergamot/Parser.purs

@@ -14,9 +14,10 @@ import Parsing.String.Basic (digit, letter, space)
 import Parsing.Combinators (many, many1, sepBy, (<|>))
 import Data.Array (fromFoldable)
 import Data.Either (hush)
+import Data.Int (fromString)
 import Data.List (List(..))
 import Data.List.NonEmpty (NonEmptyList)
-import Data.Maybe (Maybe)
+import Data.Maybe (Maybe, fromMaybe)
 import Data.String (codePointFromChar, fromCodePointArray)
 
 charsToString :: NonEmptyList Char -> String
@@ -26,10 +27,13 @@ whitespace :: Parser String Unit
 whitespace = void $ many space
 
 identifier :: Parser String String
-identifier = (charsToString <$> many1 (letter <|> digit <|> char '_')) <* whitespace
+identifier = (charsToString <$> many1 (letter <|> digit <|> char '_' <|> char '\\')) <* whitespace
 
 expr :: Parser String (Expr Metavariable)
-expr = (defer $ \_ -> atom) <|> (defer $ \_ -> metavariable)
+expr = (defer $ \_ -> intLit) <|> (defer $ \_ -> atom) <|> (defer $ \_ -> metavariable)
+
+intLit :: Parser String (Expr Metavariable)
+intLit = (IntLit <<< fromMaybe 0 <<< fromString <<< charsToString) <$> many1 digit
 
 atom :: Parser String (Expr Metavariable)
 atom = lift2 Atom (identifier <* whitespace) (args <|> pure Nil)

src/Language/Bergamot/Syntax.purs

@@ -10,6 +10,8 @@ import Data.List (List(..), (:))
 
 data Expr v
     = Var v
+    | IntLit Int
+    | StringLit String
     | Atom String (List (Expr v))
 
 derive instance Eq v => Eq (Expr v)
@@ -28,10 +30,14 @@ instance UnificationVariable IntVar where
 instance UnificationVariable k => Unifiable k Expr where
     variable = Var
     squash (Var f) = f
+    squash (IntLit i) = IntLit i
+    squash (StringLit s) = StringLit s
     squash (Atom name args) = Atom name $ squash <$> args
     alongside (Var k1) (Var k2) = Var (Merge k1 k2)
     alongside (Var k) f = Var (Store k f)
     alongside f (Var k) = Var (Store k f)
+    alongside (IntLit i1) (IntLit i2) | i1 == i2 = IntLit i1
+    alongside (StringLit s1) (StringLit s2) | s1 == s2 = StringLit s1
     alongside (Atom n1 _) (Atom n2 _) | n1 /= n2 = Var Fail
     alongside (Atom n1 args1) (Atom _ args2) = Atom n1 $ combine args1 args2
         where
@@ -39,3 +45,4 @@ 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
+    alongside _ _ = Var Fail

src/Language/Bergamot/Unifier.purs

@@ -3,22 +3,24 @@ module Language.Bergamot.Unifier where
 import Prelude
 
 import Language.Bergamot.Rules (Metavariable, ProofTree(..), Rule(..), instantiate)
-import Language.Bergamot.Syntax (Expr, IntVar)
+import Language.Bergamot.Syntax (Expr(..), IntVar)
 
 import Control.Plus (class Plus, empty)
 import Control.Apply (lift2)
-import Control.Alt (class Alt)
+import Control.Alt (class Alt, alt, (<|>))
 import Control.Alternative (class Alternative)
+import Control.Lazy (class Lazy, defer)
 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.Reader.Trans (ReaderT(..), runReaderT)
 import Control.Monad.Unify.Trans (UnifyT(..), runUnifyT)
-import Control.Monad.Logic.Trans (SFKT, runSFKTOnce)
+import Control.Monad.Logic.Trans (SFKT(..), runSFKTOnce, unSFKT)
 import Control.Monad.State.Trans (StateT(..), runStateT)
 import Data.Traversable (traverse, oneOf)
 import Data.Tuple (fst)
+import Data.List (List(..), (:))
 import Data.Newtype (class Newtype, un, over2)
 import Data.Maybe (Maybe)
 import Data.Bifunctor (rmap)
@@ -51,13 +53,35 @@ 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)
 
+instance Lazy (Unifier a) where
+    defer f = MkUnifier $ MkUnifyT $ StateT $ \s -> ReaderT $ \r -> SFKT (\sk fk -> unSFKT (runReaderT (runStateT (un MkUnifyT $ un MkUnifier $ f unit) s) r) sk fk)
+
 spend :: forall a. Unifier a -> Unifier a
 spend m = do
     n <- asks _.fuel
     if n > 0 then local (_ { fuel = n - 1}) m else empty
 
+ints :: forall m. MonadLogic m => Lazy (m Int) => m Int
+ints = impl 0
+    where
+      impl n = pure n <|> defer (\_ -> impl $ n+1)
+
+matchBuiltin :: Expr IntVar -> Unifier (ProofTree IntVar)
+matchBuiltin e@(Atom "isInt" (t : Nil)) =
+    case t of
+        IntLit i -> pure $ isIntProof i
+        Var _ -> do
+           i <- ints
+           _ <- unify t (IntLit i)
+           pure $ isIntProof i
+        _ -> empty
+    where
+        isIntRule i = MkRule { head: Atom "isInt" (IntLit i : Nil), tail: Nil }
+        isIntProof i = MkProofTree { claim: e, rule: isIntRule i, witnesses: Nil }
+matchBuiltin _ = empty
+
 match :: Array (Rule Metavariable) -> Expr IntVar -> Unifier (ProofTree IntVar)
-match rs e = oneOf $ map (matchSingle e) rs
+match rs e = interleave (reify e >>= matchBuiltin) $ oneOf $ map (matchSingle e) rs
     where
       matchSingle e' rule = spend $ do
          MkRule {head, tail} <- instantiate rule

test/Main.purs

@@ -5,6 +5,7 @@ import Language.Bergamot.Syntax
 import Language.Bergamot.Rules
 import Language.Bergamot.Unifier
 import Language.Bergamot.Parser
+import Language.Bergamot.Latex
 import Control.Apply
 import Control.Monad.Logic.Trans
 import Control.Monad.Logic.Class
@@ -15,37 +16,6 @@ import Data.Array (fromFoldable)
 import Data.Foldable
 import Data.Maybe
 
-tType et tt = Atom "type" $ et : tt : Nil
-tInt = Atom "int" Nil                                      
-tString = Atom "string" Nil                                
-tProd t1 t2 = Atom "prod" $ t1 : t2 : Nil
-tIntExpr = Atom "n" Nil                                    
-tStringExpr = Atom "s" Nil
-tPlusExpr et1 et2 = Atom "plus" $ et1 : et2 : Nil
-tProdExpr et1 et2 = Atom "pair" $ et1 : et2 : Nil
-tFstExpr et = Atom "fst" $ et : Nil
-tSndExpr et = Atom "snd" $ et : Nil
-
-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 "n" Nil) = "n"
-toLatexExpr (Atom "s" Nil) = "s"
-toLatexExpr (Atom "plus" (t1 : t2 : Nil)) = toLatexExpr t1 <> " + " <> toLatexExpr t2
-toLatexExpr (Atom "pair" (t1 : t2 : Nil)) = "(" <> toLatexExpr t1 <> ", " <> toLatexExpr t2 <> ")"
-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 x) = x
-
-toLatexRule :: Rule String -> String
-toLatexRule (MkRule {head, tail}) = "\\cfrac{" <> intercalate "\\quad " (toLatexExpr <$> tail) <> "}{" <> toLatexExpr head <> "}"
-
-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 rs q = map (toLatex <<< 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")