WIP: Use bergamot to render inference rules.
Not the proof trees yet, but it should be about the same.
This commit is contained in:
parent
549527d0cc
commit
12fa4dc1fd
|
@ -1,9 +1,50 @@
|
||||||
module Bergamot.Latex exposing (..)
|
module Bergamot.Latex exposing (..)
|
||||||
|
|
||||||
import Bergamot.Syntax exposing (..)
|
import Bergamot.Syntax as Syntax exposing (..)
|
||||||
import Bergamot.Rules exposing (..)
|
import Bergamot.Rules as Rules exposing (..)
|
||||||
import Bergamot.Utils 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 : (a -> String) -> Term a -> String
|
||||||
termToLatex f t =
|
termToLatex f t =
|
||||||
case t of
|
case t of
|
||||||
|
|
|
@ -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.Syntax exposing (Term(..), Metavariable, UnificationVar, unify, emptyUnificationState, instantiate, instantiateList, emptyInstantiationState, resetVars, InstantiationState, UnificationState, reify)
|
||||||
import Bergamot.Search as Search exposing (Search)
|
import Bergamot.Search as Search exposing (Search)
|
||||||
import Bergamot.Utils exposing (encodeStr)
|
import Bergamot.Utils exposing (encodeStr, encodeLatex)
|
||||||
|
|
||||||
import Debug
|
import Debug
|
||||||
|
|
||||||
|
@ -148,6 +148,12 @@ builtinRules t =
|
||||||
Call "tostring" [Call s [], Var output] ->
|
Call "tostring" [Call s [], Var output] ->
|
||||||
liftUnification unify (Var output) (StringLit <| encodeStr s)
|
liftUnification unify (Var output) (StringLit <| encodeStr s)
|
||||||
|> map (\_ -> MkProofTree { name = "BuiltinToString", conclusion = t, premises = []})
|
|> 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
|
_ -> fail
|
||||||
|
|
||||||
provePremises : List (Term UnificationVar) -> Prover (List ProofTree)
|
provePremises : List (Term UnificationVar) -> Prover (List ProofTree)
|
||||||
|
|
|
@ -1,5 +1,5 @@
|
||||||
module Bergamot.Syntax exposing
|
module Bergamot.Syntax exposing
|
||||||
( Term(..), Metavariable(..), UnificationVar(..)
|
( Term(..), map, andThen, Metavariable(..), UnificationVar(..)
|
||||||
, instantiate, instantiateList, InstantiationState, emptyInstantiationState, resetVars
|
, instantiate, instantiateList, InstantiationState, emptyInstantiationState, resetVars
|
||||||
, unify, unifyList, UnificationState, emptyUnificationState
|
, unify, unifyList, UnificationState, emptyUnificationState
|
||||||
, reify
|
, reify
|
||||||
|
@ -27,6 +27,22 @@ type Term a
|
||||||
| Call Name (List (Term a))
|
| Call Name (List (Term a))
|
||||||
| Var 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 =
|
type alias InstantiationState =
|
||||||
{ counter : Int
|
{ counter : Int
|
||||||
, vars : Dict String UnificationVar
|
, vars : Dict String UnificationVar
|
||||||
|
|
|
@ -38,3 +38,9 @@ encodeLatex s =
|
||||||
in
|
in
|
||||||
String.fromList (go (String.toList s))
|
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
|
||||||
|
|
|
@ -50,7 +50,7 @@ type Msg
|
||||||
| SetEditMode EditMode
|
| SetEditMode EditMode
|
||||||
|
|
||||||
init : Flags -> (Model, Cmd Msg)
|
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 : String -> Html Msg -> Html Msg
|
||||||
viewSection name content =
|
viewSection name content =
|
||||||
|
@ -77,14 +77,15 @@ viewTabSelector = viewSelector tabEq SetTab
|
||||||
viewEditModeSelector : EditMode -> List (EditMode, String) -> Html Msg
|
viewEditModeSelector : EditMode -> List (EditMode, String) -> Html Msg
|
||||||
viewEditModeSelector = viewSelector modeEq SetEditMode
|
viewEditModeSelector = viewSelector modeEq SetEditMode
|
||||||
|
|
||||||
viewRule : Rule -> Html Msg
|
viewRule : RuleEnv -> Rule -> Maybe (Html Msg)
|
||||||
viewRule = latex << ruleToLatex
|
viewRule env r = renderRuleViaRules env r
|
||||||
|
|> Maybe.map latex
|
||||||
|
|
||||||
viewRules : String -> Html Msg
|
viewRules : String -> Html Msg
|
||||||
viewRules progs = viewSection "Rendered Rules" <|
|
viewRules progs = viewSection "Rendered Rules" <|
|
||||||
Html.div [ class "bergamot-rule-list" ] <|
|
Html.div [ class "bergamot-rule-list" ] <|
|
||||||
case run program progs of
|
case run program progs of
|
||||||
Just prog -> List.map viewRule prog.rules
|
Just prog -> List.filterMap (viewRule prog) prog.rules
|
||||||
Nothing -> []
|
Nothing -> []
|
||||||
|
|
||||||
proofGoal : EditMode -> String -> Maybe (Term Metavariable)
|
proofGoal : EditMode -> String -> Maybe (Term Metavariable)
|
||||||
|
|
Loading…
Reference in New Issue
Block a user