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

Configure prommpts via a Bergamot program, too.

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-12-22 15:58:52 -08:00
parent 9fd60b4013
commit 12d823e944
2 changed files with 28 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/Bergamot/Syntax.elm
View File

@ -1,5 +1,6 @@
module Bergamot.Syntax exposing
( Term(..), map, andThen, Metavariable(..), UnificationVar(..)
, unMetavariable, unUnificationVar
, instantiate, instantiateList, InstantiationState, emptyInstantiationState, resetVars
, unify, unifyList, UnificationState, emptyUnificationState
, reify

39
src/Main.elm
View File

@ -54,12 +54,13 @@ resultModeEq rm1 rm2 =
type alias Model =
{ program : String
, renderProgram: String
, inputProgram : String
, tab : Tab
, query : String
, editMode : EditMode
, resultMode : ResultMode
}
type alias Flags = { renderRules: String, rules: String, query: String }
type alias Flags = { renderRules: String, inputRules: String, rules: String, query: String }
type Msg
= SetProgram String
| SetRenderProgram String
@ -69,7 +70,7 @@ type Msg
| SetResultMode ResultMode
init : Flags -> (Model, Cmd Msg)
init fs = ({ program = fs.rules, renderProgram = fs.renderRules, query = fs.query, tab = Rendered, editMode = Syntax, resultMode = Conclusion }, Cmd.none)
init fs = ({ program = fs.rules, renderProgram = fs.renderRules, inputProgram = fs.inputRules, query = fs.query, tab = Rendered, editMode = Syntax, resultMode = Conclusion }, Cmd.none)
viewSection : String -> Html Msg -> Html Msg
viewSection name content =
@ -121,22 +122,36 @@ viewRules renderProgs progs =
(Just renderProg, Just prog) -> List.filterMap (viewRuleSection renderProg) prog.sections
_ -> []
proofGoal : EditMode -> String -> Maybe (Term Metavariable)
proofGoal editMode querys =
proofGoal : EditMode -> String -> String -> Maybe (Term Metavariable)
proofGoal editMode inputProgs querys =
case editMode of
Query -> run term querys
Syntax -> Maybe.map (\e -> Call "type" [Call "empty" [], exprToTerm e, Var (MkMetavariable "tau")]) <| run parseExpr querys
Syntax ->
case (run program inputProgs, run parseExpr querys) of
(Just inputProg, Just e) ->
let
inputRule = { name = "UserInput", premises = [], conclusion = Call "input" [exprToTerm e] }
fullProgram = { sections = { name = "", rules = [inputRule] } :: inputProg.sections }
query = Call "prompt" [Var (MkMetavariable "?p")]
in
case single fullProgram (prove query |> Bergamot.Rules.andThen reifyProofTree) of
Just (MkProofTree node) ->
case node.conclusion of
Call "prompt" [t] -> Just <| Bergamot.Syntax.map (MkMetavariable << unUnificationVar) t
_ -> Nothing
_ -> Nothing
_ -> Nothing
tryProve : EditMode -> String -> String -> Maybe ProofTree
tryProve editMode progs querys =
case (run program progs, proofGoal editMode querys) of
tryProve : EditMode -> String -> String -> String -> Maybe ProofTree
tryProve editMode inputProgs progs querys =
case (run program progs, proofGoal editMode inputProgs querys) of
(Just prog, Just query) -> single prog (prove query |> Bergamot.Rules.andThen reifyProofTree)
_ -> Nothing
viewProofTree : EditMode -> ResultMode -> String -> String -> String -> Html Msg
viewProofTree editMode resultMode renderProgs progs querys =
viewProofTree : EditMode -> ResultMode -> String -> String -> String -> String -> Html Msg
viewProofTree editMode resultMode renderProgs inputProgs progs querys =
Html.div [ class "bergamot-proof-tree" ] <|
case tryProve editMode progs querys of
case tryProve editMode inputProgs progs querys of
Just (MkProofTree tree) ->
case run program renderProgs of
Just renderProg ->
@ -158,7 +173,7 @@ view m = Html.div [ class "bergamot-root" ]
]
, viewSection "Result" <| Html.div[]
[ viewResultModeSelector m.resultMode [(Conclusion, "Conclusion Only"), (Tree, "Full Proof Tree")]
, viewProofTree m.editMode m.resultMode m.renderProgram m.program m.query
, viewProofTree m.editMode m.resultMode m.renderProgram m.inputProgram m.program m.query
]
, viewSection "Rules" <| Html.div []
[ viewTabSelector m.tab [(Rendered, "Rendered"), (Editor, "Editor"), (MetaEditor, "Presentation Rules")]