Everything-I-Know-About-Types/bergamot
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Extract latex generation to a typeclass

Browse Source
This commit is contained in:
Danila Fedorin 2023-03-11 16:41:52 -08:00
parent 930a05c951
commit 3ab3126bbf
2 changed files with 36 additions and 32 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
src/Language/Bergamot/Latex.purs Normal file
View File

@ -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 <> "}"

34
test/Main.purs
View File

@ -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")