From 12fa4dc1fd8341c86c9782dd774f47a3896b6bea Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 1 Dec 2023 23:31:43 -0800 Subject: [PATCH] WIP: Use bergamot to render inference rules. Not the proof trees yet, but it should be about the same. --- src/Bergamot/Latex.elm | 45 +++++++++++++++++++++++++++++++++++++++-- src/Bergamot/Rules.elm | 8 +++++++- src/Bergamot/Syntax.elm | 18 ++++++++++++++++- src/Bergamot/Utils.elm | 6 ++++++ src/Main.elm | 9 +++++---- 5 files changed, 78 insertions(+), 8 deletions(-) diff --git a/src/Bergamot/Latex.elm b/src/Bergamot/Latex.elm index bdf7c13..fdf3652 100644 --- a/src/Bergamot/Latex.elm +++ b/src/Bergamot/Latex.elm @@ -1,9 +1,50 @@ module Bergamot.Latex exposing (..) -import Bergamot.Syntax exposing (..) -import Bergamot.Rules exposing (..) +import Bergamot.Syntax as Syntax exposing (..) +import Bergamot.Rules as Rules exposing (..) import Bergamot.Utils exposing (..) +import Debug + +type Void = Void Void + +absurd : Void -> a +absurd (Void v) = absurd v + +renderTermViaRules : RuleEnv -> Term Void -> Maybe String +renderTermViaRules env t = + Call "latex" [Syntax.map absurd t, Var (MkMetavariable "s")] + |> prove + |> Rules.andThen reifyProofTree + |> single env + |> Maybe.andThen (\(MkProofTree node) -> + case node.conclusion of + Call "latex" [_, StringLit s] -> Just s + _ -> Nothing) + +renderRuleViaRules : RuleEnv -> Rule -> Maybe String +renderRuleViaRules env r = + let + quotedPrems = List.map (Syntax.andThen quoteMetavariable) r.premises + quotedConc = Syntax.andThen quoteMetavariable r.conclusion + buildStr conc prems = String.concat + [ "\\cfrac{" + , String.join "\\quad " prems + , "}{" + , conc + , "}\\ \\texttt{" + , r.name + , "}" + ] + in + renderTermViaRules env quotedConc + |> Maybe.andThen (\conc -> + sequenceMaybes (List.map (renderTermViaRules env) quotedPrems) + |> Maybe.map (\prems -> buildStr conc prems)) + +quoteMetavariable : Metavariable -> Term Void +quoteMetavariable (MkMetavariable s) = Call "metavariable" [StringLit <| String.dropLeft 1 s] + termToLatex : (a -> String) -> Term a -> String termToLatex f t = case t of diff --git a/src/Bergamot/Rules.elm b/src/Bergamot/Rules.elm index e1cac9d..f7c2785 100644 --- a/src/Bergamot/Rules.elm +++ b/src/Bergamot/Rules.elm @@ -2,7 +2,7 @@ module Bergamot.Rules exposing (..) import Bergamot.Syntax exposing (Term(..), Metavariable, UnificationVar, unify, emptyUnificationState, instantiate, instantiateList, emptyInstantiationState, resetVars, InstantiationState, UnificationState, reify) import Bergamot.Search as Search exposing (Search) -import Bergamot.Utils exposing (encodeStr) +import Bergamot.Utils exposing (encodeStr, encodeLatex) import Debug @@ -148,6 +148,12 @@ builtinRules t = Call "tostring" [Call s [], Var output] -> liftUnification unify (Var output) (StringLit <| encodeStr s) |> map (\_ -> MkProofTree { name = "BuiltinToString", conclusion = t, premises = []}) + Call "escapestring" [StringLit s, Var output] -> + liftUnification unify (Var output) (StringLit (encodeStr s)) + |> map (\_ -> MkProofTree { name = "BuiltinEscapeString", conclusion = t, premises = []}) + Call "latexifystring" [StringLit s, Var output] -> + liftUnification unify (Var output) (StringLit (encodeLatex s)) + |> map (\_ -> MkProofTree { name = "BuiltinLatexifyeString", conclusion = t, premises = []}) _ -> fail provePremises : List (Term UnificationVar) -> Prover (List ProofTree) diff --git a/src/Bergamot/Syntax.elm b/src/Bergamot/Syntax.elm index ca0f4de..bed306d 100644 --- a/src/Bergamot/Syntax.elm +++ b/src/Bergamot/Syntax.elm @@ -1,5 +1,5 @@ module Bergamot.Syntax exposing - ( Term(..), Metavariable(..), UnificationVar(..) + ( Term(..), map, andThen, Metavariable(..), UnificationVar(..) , instantiate, instantiateList, InstantiationState, emptyInstantiationState, resetVars , unify, unifyList, UnificationState, emptyUnificationState , reify @@ -27,6 +27,22 @@ type Term a | Call Name (List (Term a)) | Var a +map : (a -> b) -> Term a -> Term b +map f t = + case t of + IntLit i -> IntLit i + StringLit s -> StringLit s + Call n ts -> Call n (List.map (map f) ts) + Var a -> Var (f a) + +andThen : (a -> Term b) -> Term a -> Term b +andThen f t = + case t of + IntLit i -> IntLit i + StringLit s -> StringLit s + Call n ts -> Call n (List.map (andThen f) ts) + Var a -> f a + type alias InstantiationState = { counter : Int , vars : Dict String UnificationVar diff --git a/src/Bergamot/Utils.elm b/src/Bergamot/Utils.elm index b1aaa5e..cd17030 100644 --- a/src/Bergamot/Utils.elm +++ b/src/Bergamot/Utils.elm @@ -38,3 +38,9 @@ encodeLatex s = in String.fromList (go (String.toList s)) +sequenceMaybes : List (Maybe a) -> Maybe (List a) +sequenceMaybes l = + case l of + [] -> Just [] + (Just x :: mxs) -> sequenceMaybes mxs |> Maybe.map (\xs -> x :: xs) + _ -> Nothing diff --git a/src/Main.elm b/src/Main.elm index aae0104..bca5693 100644 --- a/src/Main.elm +++ b/src/Main.elm @@ -50,7 +50,7 @@ type Msg | SetEditMode EditMode init : Flags -> (Model, Cmd Msg) -init fs = ({ program = fs.rules, query = fs.query, tab = Editor, editMode = Syntax }, Cmd.none) +init fs = ({ program = fs.rules, query = fs.query, tab = Editor, editMode = Query }, Cmd.none) viewSection : String -> Html Msg -> Html Msg viewSection name content = @@ -77,14 +77,15 @@ viewTabSelector = viewSelector tabEq SetTab viewEditModeSelector : EditMode -> List (EditMode, String) -> Html Msg viewEditModeSelector = viewSelector modeEq SetEditMode -viewRule : Rule -> Html Msg -viewRule = latex << ruleToLatex +viewRule : RuleEnv -> Rule -> Maybe (Html Msg) +viewRule env r = renderRuleViaRules env r + |> Maybe.map latex viewRules : String -> Html Msg viewRules progs = viewSection "Rendered Rules" <| Html.div [ class "bergamot-rule-list" ] <| case run program progs of - Just prog -> List.map viewRule prog.rules + Just prog -> List.filterMap (viewRule prog) prog.rules Nothing -> [] proofGoal : EditMode -> String -> Maybe (Term Metavariable)