From 3aebd998055caf98d1d9f640012e67d244275b07 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 12 Mar 2023 00:40:46 -0800
Subject: [PATCH] Add an isInt primitive predicate

---
 packages.dhall                     |  2 +-
 src/Language/Bergamot/Latex.purs   |  2 ++
 src/Language/Bergamot/Unifier.purs | 34 +++++++++++++++++++++++++-----
 3 files changed, 32 insertions(+), 6 deletions(-)

diff --git a/packages.dhall b/packages.dhall
index eefbced..85fecd1 100644
--- a/packages.dhall
+++ b/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"
diff --git a/src/Language/Bergamot/Latex.purs b/src/Language/Bergamot/Latex.purs
index c50e95d..5d9c8b5 100644
--- a/src/Language/Bergamot/Latex.purs
+++ b/src/Language/Bergamot/Latex.purs
@@ -24,6 +24,7 @@ instance toLatexExpr :: ToLatex k => ToLatex (Expr k) where
     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
@@ -33,4 +34,5 @@ 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 <> "}"
diff --git a/src/Language/Bergamot/Unifier.purs b/src/Language/Bergamot/Unifier.purs
index c0112f2..ca99d8f 100644
--- a/src/Language/Bergamot/Unifier.purs
+++ b/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