Reorganize the UI somewhat and add conclusion-only view

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

src/Bergamot/Rules.elm

@@ -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

src/Bergamot/Syntax.elm

@@ -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 =

src/Main.elm

@@ -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