bergamot-elm/src/Bergamot/Latex.elm

45 lines
2.4 KiB
Elm
Raw Normal View History

2023-11-26 14:34:52 -08:00
module Bergamot.Latex exposing (..)
import Bergamot.Syntax exposing (..)
import Bergamot.Rules exposing (..)
termToLatex : (a -> String) -> Term a -> String
termToLatex f t =
case t of
Call "intlit" [t1] -> termToLatex f t1
Call "strlit" [t1] -> termToLatex f t1
Call "var" [t1] -> termToLatex f t1
2023-11-26 14:34:52 -08:00
Call "plus" [t1, t2] -> termToLatex f t1 ++ " + " ++ termToLatex f t2
Call "pair" [t1, t2] -> "(" ++ termToLatex f t1 ++ ", " ++ termToLatex f t2 ++ ")"
Call "abs" [t1, t2, t3] -> "\\lambda " ++ termToLatex f t1 ++ " : " ++ termToLatex f t2 ++ ".\\ " ++ termToLatex f t3
Call "app" [t1, t2] -> termToLatex f t1 ++ "\\ " ++ termToLatex f t2
Call "type" [t1, t2] -> termToLatex f t1 ++ " : " ++ termToLatex f t2
Call "type" [t1, t2, t3] -> termToLatex f t1 ++ "\\vdash " ++ termToLatex f t2 ++ " : " ++ termToLatex f t3
Call "tpair" [t1, t2] -> termToLatex f t1 ++ "\\times" ++ termToLatex f t2
Call "tarr" [t1, t2] -> termToLatex f t1 ++ "\\to" ++ termToLatex f t2
Call "extend" [t1, t2, t3] -> termToLatex f t1 ++ ",\\ " ++ termToLatex f t2 ++ " : " ++ termToLatex f t3
Call "inenv" [t1, t2, t3] -> termToLatex f t1 ++ " : " ++ termToLatex f t2 ++ " \\in " ++ termToLatex f t3
Call "empty" [] -> "\\varnothing"
2023-11-26 14:34:52 -08:00
Call s [] -> "\\text{" ++ s ++ "}"
Call s ts -> "\\text{" ++ s ++ "}(" ++ String.join "," (List.map (termToLatex f) ts) ++ ")"
Var x -> f x
IntLit i -> String.fromInt i
StringLit s -> "\\texttt{" ++ "\"" ++ s ++ "\"" ++ "}"
2023-11-26 14:34:52 -08:00
metavariableToLatex : Metavariable -> String
metavariableToLatex (MkMetavariable s) =
let
noQuestion = String.dropLeft 1 s
in
if String.startsWith "tau" noQuestion then "\\" ++ noQuestion else
if String.startsWith "Gamma" noQuestion then "\\" ++ noQuestion else noQuestion
2023-11-26 14:34:52 -08:00
ruleToLatex : Rule -> String
ruleToLatex r = "\\cfrac{" ++ String.join "\\quad " (List.map (termToLatex metavariableToLatex) r.premises) ++ "}{" ++ termToLatex metavariableToLatex r.conclusion ++ "}\\ \\texttt{" ++ r.name ++ "}"
unificationVarToLatex : UnificationVar -> String
unificationVarToLatex (MkUnificationVar s) = s
proofTreeToLatex : ProofTree -> String
2023-11-26 15:54:01 -08:00
proofTreeToLatex (MkProofTree node) = "\\cfrac{" ++ String.join "\\quad \\quad " (List.map proofTreeToLatex node.premises) ++ "}{" ++ termToLatex unificationVarToLatex node.conclusion ++ "}\\ \\texttt{" ++ node.name ++ "}"