Compare commits

..

3 Commits

Author SHA1 Message Date
9fd60b4013 Reorganize the UI somewhat and add conclusion-only view
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-22 15:22:46 -08:00
aa7fd44a6d Slightly tweak code for proving a term
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-22 14:39:52 -08:00
da470f5caa Add an occurss check to avoid infinite terms
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-12-22 14:39:35 -08:00
3 changed files with 95 additions and 37 deletions

View File

@ -169,7 +169,8 @@ provePremises = mapM proveTerm
proveTerm : Term UnificationVar -> Prover ProofTree
proveTerm t =
map (reify t) getUnificationState
getUnificationState
|> map (\us -> reify t us)
|> andThen (\tp ->
burn (
getRules

View File

@ -109,12 +109,21 @@ merge v1 v2 us =
in
case (ui1.term, ui2.term) of
(Just t1, Just t2) ->
unify t1 t2 us
|> Maybe.map (\(t, usp) -> reconcile newEq (Just t) usp)
if occurs ui1.equivalence us t2 || occurs ui2.equivalence us t1
then Nothing
else
unify t1 t2 us
|> Maybe.map (\(t, usp) -> reconcile newEq (Just t) usp)
(Just t1, Nothing) ->
Just (reconcile newEq (Just t1) us)
if occurs ui2.equivalence us t1
then Nothing
else
Just (reconcile newEq (Just t1) us)
(Nothing, Just t2) ->
Just (reconcile newEq (Just t2) us)
if occurs ui1.equivalence us t2
then Nothing
else
Just (reconcile newEq (Just t2) us)
(Nothing, Nothing) ->
Just (reconcile newEq Nothing us)
(Just ui1, Nothing) -> Just (reconcile (Set.insert v2s ui1.equivalence) ui1.term us)
@ -128,13 +137,34 @@ set v t us =
in
case Dict.get vs us of
Just ui ->
case ui.term of
Just tp ->
unify t tp us
|> Maybe.map (\(tpp, usp) -> (tpp, reconcile ui.equivalence (Just tpp) usp))
Nothing ->
Just (t, reconcile ui.equivalence (Just t) us)
Nothing -> Just (t, Dict.insert vs { equivalence = Set.singleton vs, term = Just t } us)
if occurs ui.equivalence us t
then Nothing
else
case ui.term of
Just tp ->
unify t tp us
|> Maybe.map (\(tpp, usp) -> (tpp, reconcile ui.equivalence (Just tpp) usp))
Nothing ->
Just (t, reconcile ui.equivalence (Just t) us)
Nothing ->
if occurs (Set.singleton vs) us t
then Nothing
else
Just (t, Dict.insert vs { equivalence = Set.singleton vs, term = Just t } us)
occurs : Set String -> UnificationState -> Term UnificationVar -> Bool
occurs vars us t =
case t of
IntLit _ -> False
StringLit _ -> False
Call n ts -> List.any (occurs vars us) ts
Var (MkUnificationVar v) -> if Set.member v vars then True else
case Dict.get v us of
Just { term } ->
case term of
Just tp -> occurs vars us tp
Nothing -> False
_ -> False
unifyList : List (Term UnificationVar) -> List (Term UnificationVar) -> UnificationState -> Maybe (List (Term UnificationVar), UnificationState)
unifyList l1 l2 us =

View File

@ -33,19 +33,31 @@ type EditMode
= Query
| Syntax
modeEq : EditMode -> EditMode -> Bool
modeEq m1 m2 =
editModeEq : EditMode -> EditMode -> Bool
editModeEq m1 m2 =
case (m1, m2) of
(Query, Query) -> True
(Syntax, Syntax) -> True
_ -> False
type ResultMode
= Conclusion
| Tree
resultModeEq : ResultMode -> ResultMode -> Bool
resultModeEq rm1 rm2 =
case (rm1, rm2) of
(Conclusion, Conclusion) -> True
(Tree, Tree) -> True
_ -> False
type alias Model =
{ program : String
, renderProgram: String
, query : String
, tab : Tab
, query : String
, editMode : EditMode
, resultMode : ResultMode
}
type alias Flags = { renderRules: String, rules: String, query: String }
type Msg
@ -54,9 +66,10 @@ type Msg
| SetQuery String
| SetTab Tab
| SetEditMode EditMode
| SetResultMode ResultMode
init : Flags -> (Model, Cmd Msg)
init fs = ({ program = fs.rules, renderProgram = fs.renderRules, query = fs.query, tab = Editor, editMode = Query }, Cmd.none)
init fs = ({ program = fs.rules, renderProgram = fs.renderRules, query = fs.query, tab = Rendered, editMode = Syntax, resultMode = Conclusion }, Cmd.none)
viewSection : String -> Html Msg -> Html Msg
viewSection name content =
@ -82,7 +95,10 @@ viewTabSelector : Tab -> List (Tab, String) -> Html Msg
viewTabSelector = viewSelector tabEq SetTab
viewEditModeSelector : EditMode -> List (EditMode, String) -> Html Msg
viewEditModeSelector = viewSelector modeEq SetEditMode
viewEditModeSelector = viewSelector editModeEq SetEditMode
viewResultModeSelector : ResultMode -> List (ResultMode, String) -> Html Msg
viewResultModeSelector = viewSelector resultModeEq SetResultMode
viewRule : RuleEnv -> Rule -> Maybe (Html Msg)
viewRule env r = renderRuleViaRules env r
@ -99,48 +115,58 @@ viewRuleSection env sec =
])
viewRules : String -> String -> Html Msg
viewRules renderProgs progs = viewSection "Rendered Rules" <|
viewRules renderProgs progs =
Html.div [ class "bergamot-section-list" ] <|
case (run program renderProgs, run program progs) of
(Just renderProg, Just prog) -> List.filterMap (viewRuleSection renderProg) prog.sections
_ -> []
proofGoal : EditMode -> String -> Maybe (Term Metavariable)
proofGoal mode querys =
case mode of
proofGoal editMode querys =
case editMode of
Query -> run term querys
Syntax -> Maybe.map (\e -> Call "type" [Call "empty" [], exprToTerm e, Var (MkMetavariable "tau")]) <| run parseExpr querys
tryProve : EditMode -> String -> String -> Maybe ProofTree
tryProve mode progs querys =
case (run program progs, proofGoal mode querys) of
tryProve editMode progs querys =
case (run program progs, proofGoal editMode querys) of
(Just prog, Just query) -> single prog (prove query |> Bergamot.Rules.andThen reifyProofTree)
_ -> Nothing
viewProofTree : EditMode -> String -> String -> String -> Html Msg
viewProofTree mode renderProgs progs querys = viewSection "Proof Tree" <|
viewProofTree : EditMode -> ResultMode -> String -> String -> String -> Html Msg
viewProofTree editMode resultMode renderProgs progs querys =
Html.div [ class "bergamot-proof-tree" ] <|
case tryProve mode progs querys of
Just tree ->
case tryProve editMode progs querys of
Just (MkProofTree tree) ->
case run program renderProgs of
Just renderProg ->
List.map latex
<| List.filterMap (renderTreeViaRules renderProg)
<| [ tree ]
let
maybeLatexString =
case resultMode of
Conclusion -> renderTermViaRules renderProg (quoteVariables tree.conclusion)
Tree -> renderTreeViaRules renderProg (MkProofTree tree)
in List.filterMap (Maybe.map latex) [maybeLatexString]
Nothing -> []
Nothing -> []
view : Model -> Html Msg
view m = Html.div [ class "bergamot-root" ]
[ viewTabSelector m.tab [(Editor, "Rule Editor"), (MetaEditor, "Meta Rule Editor"), (Rendered, "Rendered Rules")]
, viewEditModeSelector m.editMode [(Query, "Query"), (Syntax, "Language Term")]
, viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery, value m.query ] []
, viewProofTree m.editMode m.renderProgram m.program m.query
, viewTab m.tab
(viewSection "Rules" <| Html.textarea [ onInput SetProgram ] [ Html.text m.program ])
(viewSection "Meta Rules" <| Html.textarea [ onInput SetRenderProgram ] [ Html.text m.renderProgram ])
(Html.Lazy.lazy2 viewRules m.renderProgram m.program)
[ viewSection "Input" <| Html.div []
[ viewEditModeSelector m.editMode [(Query, "Query"), (Syntax, "Language Term")]
, Html.input [ type_ "text", onInput SetQuery, value m.query ] []
]
, 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
]
, viewSection "Rules" <| Html.div []
[ viewTabSelector m.tab [(Rendered, "Rendered"), (Editor, "Editor"), (MetaEditor, "Presentation Rules")]
, viewTab m.tab
(Html.textarea [ onInput SetProgram ] [ Html.text m.program ])
(Html.textarea [ onInput SetRenderProgram ] [ Html.text m.renderProgram ])
(Html.Lazy.lazy2 viewRules m.renderProgram m.program)
]
]
update : Msg -> Model -> (Model, Cmd Msg)
@ -151,6 +177,7 @@ update msg m =
SetQuery query -> ({ m | query = query }, Cmd.none)
SetTab tab -> ({ m | tab = tab }, Cmd.none)
SetEditMode mode -> ({ m | editMode = mode }, Cmd.none)
SetResultMode mode -> ({ m | resultMode = mode }, Cmd.none)
subscriptions : Model -> Sub Msg
subscriptions _ = Sub.none