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

Fix the parser and add more syntax pretty printing

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-11-26 20:44:27 -08:00
parent ff1ea05784
commit e0532fb581
2 changed files with 18 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
src/Bergamot/Latex.elm
View File

@ -6,12 +6,20 @@ import Bergamot.Rules exposing (..)
termToLatex : (a -> String) -> Term a -> String
termToLatex f t =
case t of
Call "type" [t1, t2] -> termToLatex f t1 ++ " : " ++ termToLatex f t2
Call "intlit" [t1] -> termToLatex f t1
Call "strlit" [t1] -> termToLatex f t1
Call "tpair" [t1, t2] -> termToLatex f t1 ++ "\\times" ++ termToLatex f t2
Call "var" [t1] -> termToLatex f t1
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"
Call s [] -> "\\text{" ++ s ++ "}"
Call s ts -> "\\text{" ++ s ++ "}(" ++ String.join "," (List.map (termToLatex f) ts) ++ ")"
Var x -> f x
@ -23,7 +31,8 @@ metavariableToLatex (MkMetavariable s) =
let
noQuestion = String.dropLeft 1 s
in
if String.startsWith "tau" noQuestion then "\\" ++ noQuestion else noQuestion
if String.startsWith "tau" noQuestion then "\\" ++ noQuestion else
if String.startsWith "Gamma" noQuestion then "\\" ++ noQuestion else noQuestion
ruleToLatex : Rule -> String
ruleToLatex r = "\\cfrac{" ++ String.join "\\quad " (List.map (termToLatex metavariableToLatex) r.premises) ++ "}{" ++ termToLatex metavariableToLatex r.conclusion ++ "}\\ \\texttt{" ++ r.name ++ "}"

10
src/Bergamot/Parser.elm
View File

@ -27,8 +27,7 @@ variable =
term : Parser (Term Metavariable)
term = Parser.lazy (\() -> Parser.oneOf
[ Parser.succeed IntLit |= intLit
, Parser.backtrackable <|
[ Parser.backtrackable <|
Parser.succeed Call
|= name
|= Parser.sequence
@ -39,9 +38,12 @@ term = Parser.lazy (\() -> Parser.oneOf
, item = term
, trailing = Forbidden
}
, Parser.succeed (\n -> Call n [])
, Parser.backtrackable <|
Parser.succeed (\n -> Call n [])
|= name
, Parser.succeed Var |= variable
, Parser.backtrackable <|
Parser.succeed Var |= variable
, Parser.succeed IntLit |= intLit
])
rule : Parser Rule