From 3ab3126bbf766865d7a9735faf9b22a2a8688150 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 11 Mar 2023 16:41:52 -0800
Subject: [PATCH] Extract latex generation to a typeclass

---
 src/Language/Bergamot/Latex.purs | 34 ++++++++++++++++++++++++++++++++
 test/Main.purs                   | 34 ++------------------------------
 2 files changed, 36 insertions(+), 32 deletions(-)
 create mode 100644 src/Language/Bergamot/Latex.purs

diff --git a/src/Language/Bergamot/Latex.purs b/src/Language/Bergamot/Latex.purs
new file mode 100644
index 0000000..ec018a4
--- /dev/null
+++ b/src/Language/Bergamot/Latex.purs
@@ -0,0 +1,34 @@
+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 s xs) = "\\text{" <> s <> "}(" <> intercalate ", " (toLatex <$> xs) <> ")"
+    toLatex (Var x) = toLatex x
+
+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}) = "\\cfrac{" <> intercalate "\\quad " (toLatex <$> witnesses) <> "}{" <> toLatex claim <> "}"
diff --git a/test/Main.purs b/test/Main.purs
index e0ceeca..d713858 100644
--- a/test/Main.purs
+++ b/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")