Try using tail recursion to reduce stack pressure

packages.dhall

@@ -104,9 +104,9 @@ 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 = "880ade17dc5129975c16d211dc6ed3bddf2821c8"
     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"
+    with unifyt.version = "ef3dabfa22a92b3983fc7f5c81614143c58972be"
     with unifyt.dependencies = [ "control", "foldable-traversable", "lazy", "maybe", "newtype", "ordered-collections", "prelude", "transformers", "tuples" ]
 

spago.dhall

@@ -12,16 +12,22 @@ to generate this file without the comments in this block.
 -}
 { name = "bergamot"
 , dependencies =
-  [ "bifunctors"
+  [ "arrays"
+  , "bifunctors"
   , "control"
+  , "either"
   , "foldable-traversable"
+  , "integers"
   , "lazy"
   , "lists"
   , "logict"
   , "maybe"
   , "newtype"
   , "ordered-collections"
+  , "parsing"
   , "prelude"
+  , "strings"
+  , "tailrec"
   , "transformers"
   , "tuples"
   , "unifyt"

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

@@ -0,0 +1,61 @@
+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.Int (fromString)
+import Data.List (List(..))
+import Data.List.NonEmpty (NonEmptyList)
+import Data.Maybe (Maybe, fromMaybe)
+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 '_' <|> char '\\')) <* whitespace
+
+expr :: Parser String (Expr 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)
+    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,42 +2,16 @@ 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
+    | IntLit Int
+    | StringLit String
     | Atom String (List (Expr v))
 
 derive instance Eq v => Eq (Expr v)
@@ -56,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
@@ -67,83 +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
-
--- 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 }))
+    alongside _ _ = Var Fail

src/Language/Bergamot/Unifier.purs

@@ -0,0 +1,158 @@
+module Language.Bergamot.Unifier where
+
+import Prelude
+
+import Language.Bergamot.Rules (Metavariable, ProofTree(..), Rule(..), instantiate)
+import Language.Bergamot.Syntax (Expr(..), IntVar)
+import Language.Bergamot.Latex
+
+import Control.Plus (class Plus, empty)
+import Control.Apply (lift2)
+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.Unify.Trans (UnifyT(..), runUnifyT)
+import Control.Monad.Logic.Trans (SFKT(..), runSFKTOnce, unSFKT)
+import Control.Monad.State.Trans (StateT(..), runStateT)
+import Control.Monad.Rec.Class (class MonadRec, Step(..), tailRecM)
+import Data.Traversable (traverse, oneOf)
+import Data.Foldable (oneOfMap)
+import Data.Tuple (fst)
+import Data.List (List(..), (:), reverse)
+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
+derive newtype instance MonadRec 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)
+
+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
+
+type StackElement =
+    { done :: List (ProofTree IntVar)
+    , todo :: List (Expr IntVar)
+    , claim :: Expr IntVar
+    , rule :: Rule Metavariable
+    }
+
+type Stack = List StackElement
+
+type Acc =
+    { stack :: Stack
+    , rules :: Array (Rule Metavariable)
+    }
+
+rule :: Expr IntVar -> Rule Metavariable -> Unifier StackElement
+rule e r = do
+    MkRule {head, tail} <- instantiate r
+    _ <- unify e head
+    pure $ { done: Nil, todo: tail, claim: e, rule: r }
+
+rules :: Expr IntVar -> Array (Rule Metavariable) -> Unifier StackElement
+rules e rs = oneOfMap (rule e) rs
+
+step :: Acc -> Unifier (Step Acc (ProofTree IntVar))
+step {stack: Nil} = empty
+step acc@{stack: {done, todo: Nil, claim, rule: r} : xs} =
+    pure $ case xs of
+        Nil -> Done tree
+        Cons se xs' -> Loop acc {stack = se { done = tree : se.done } : xs'}
+    where
+        tree = MkProofTree { claim, rule: r, witnesses: reverse done }
+step acc@{stack: se@{todo: (e:es)} : xs} =
+    do
+        e' <- reify e
+        interleave (builtin e') (given e')
+    where
+        builtin e' = do
+            t <- matchBuiltin e'
+            pure $ Loop acc { stack = se { todo = es, done = t : se.done } : xs }
+        given e' = do
+            se' <- rules e' acc.rules
+            pure $ Loop acc { stack = se' : se { todo = es } : xs }
+
+
+-- Note: maybe it's the list / rule operations that are the problem, rather
+-- than the stack itself? In particular, could the oneOf be the issue?
+
+match' :: Array (Rule Metavariable) -> Expr IntVar -> Unifier (ProofTree IntVar)
+match' rs e = interleave (matchBuiltin e) do
+    firstElem <- rules e rs
+    tailRecM step { rules: rs, stack: firstElem : Nil }
+
+match :: Array (Rule Metavariable) -> Expr IntVar -> Unifier (ProofTree IntVar)
+match rs e = interleave (reify e >>= matchBuiltin) $ oneOfMap (matchSingle e) rs
+    where
+      matchSingle e' r = spend $ do
+         MkRule {head, tail} <- instantiate r
+         _ <- unify e' head
+         witnesses <- traverse (match rs) tail
+         pure $ MkProofTree { claim: e, rule: r, witnesses: witnesses }
+
+reifyProofTree :: ProofTree IntVar -> Unifier (ProofTree IntVar)
+reifyProofTree (MkProofTree {claim, rule: r, witnesses}) = do
+    claim' <- reify claim
+    witnesses' <- traverse reifyProofTree witnesses
+    pure $ MkProofTree $ { claim: claim', rule: r, 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,65 +2,20 @@ module Test.Main where
 
 import Prelude
 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
 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                                
-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 IntVar -> 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 _) = "?"
-
-toLatexProofTree :: ProofTree IntVar -> String
-toLatexProofTree (MkProofTree {claim, witnesses}) = "\\cfrac{" <> intercalate "\\quad" (toLatexProofTree <$> witnesses) <> "}{" <> toLatexExpr claim <> "}"
-
-main :: Maybe String
-main = map toLatexProofTree $ runUnifier rules $ query $ tType (Var "e") (tProd tInt (tProd tInt tString))
+main :: String -> String -> Maybe String
+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")