src/Bergamot/Rules.elm

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

src/Bergamot/Syntax.elm

@@ -109,21 +109,12 @@ merge v1 v2 us =
                 in
                     case (ui1.term, ui2.term) of
                         (Just t1, Just t2) ->
-                            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)
+                            unify t1 t2 us
+                            |> Maybe.map (\(t, usp) -> reconcile newEq (Just t) usp)
                         (Just t1, Nothing) ->
-                            if occurs ui2.equivalence us t1
-                            then Nothing
-                            else
-                                Just (reconcile newEq (Just t1) us)
+                            Just (reconcile newEq (Just t1) us)
                         (Nothing, Just t2) ->
-                            if occurs ui1.equivalence us t2
-                            then Nothing
-                            else
-                                Just (reconcile newEq (Just t2) us)
+                            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)
@@ -137,34 +128,13 @@ set v t us =
     in
         case Dict.get vs us of
             Just ui ->
-                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
+                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)
 
 unifyList : List (Term UnificationVar) -> List (Term UnificationVar) -> UnificationState -> Maybe (List (Term UnificationVar), UnificationState)
 unifyList l1 l2 us =

src/Main.elm

@@ -33,31 +33,19 @@ type EditMode
     = Query
     | Syntax
 
-editModeEq : EditMode -> EditMode -> Bool
-editModeEq m1 m2 =
+modeEq : EditMode -> EditMode -> Bool
+modeEq 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
-    , tab : Tab
     , query : String
+    , tab : Tab
     , editMode : EditMode
-    , resultMode : ResultMode
     }
 type alias Flags = { renderRules: String, rules: String, query: String }
 type Msg
@@ -66,10 +54,9 @@ 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 = Rendered, editMode = Syntax, resultMode = Conclusion }, Cmd.none)
+init fs = ({ program = fs.rules, renderProgram = fs.renderRules, query = fs.query, tab = Editor, editMode = Query }, Cmd.none)
 
 viewSection : String -> Html Msg -> Html Msg
 viewSection name content =
@@ -95,10 +82,7 @@ viewTabSelector : Tab -> List (Tab, String) -> Html Msg
 viewTabSelector = viewSelector tabEq SetTab
 
 viewEditModeSelector : EditMode -> List (EditMode, String) -> Html Msg
-viewEditModeSelector = viewSelector editModeEq SetEditMode
-
-viewResultModeSelector : ResultMode -> List (ResultMode, String) -> Html Msg
-viewResultModeSelector = viewSelector resultModeEq SetResultMode
+viewEditModeSelector = viewSelector modeEq SetEditMode
 
 viewRule : RuleEnv -> Rule -> Maybe (Html Msg)
 viewRule env r = renderRuleViaRules env r
@@ -115,58 +99,48 @@ viewRuleSection env sec =
         ])
 
 viewRules : String -> String -> Html Msg
-viewRules renderProgs progs =
+viewRules renderProgs progs = viewSection "Rendered Rules" <|
     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 editMode querys =
-    case editMode of
+proofGoal mode querys =
+    case mode 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 editMode progs querys =
-    case (run program progs, proofGoal editMode querys) of
+tryProve mode progs querys =
+    case (run program progs, proofGoal mode 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 -> String -> String -> String -> Html Msg
+viewProofTree mode renderProgs progs querys = viewSection "Proof Tree" <|
     Html.div [ class "bergamot-proof-tree" ] <|
-        case tryProve editMode progs querys of
-            Just (MkProofTree tree) ->
+        case tryProve mode progs querys of
+            Just tree ->
                 case run program renderProgs of
                     Just renderProg ->
-                        let
-                            maybeLatexString =
-                                case resultMode of
-                                    Conclusion -> renderTermViaRules renderProg (quoteVariables tree.conclusion)
-                                    Tree -> renderTreeViaRules renderProg (MkProofTree tree)
-                        in List.filterMap (Maybe.map latex) [maybeLatexString]
+                        List.map latex
+                            <| List.filterMap (renderTreeViaRules renderProg)
+                            <| [ tree ]
                     Nothing -> []
             Nothing -> []
 
 
 view : Model -> Html Msg
 view m = Html.div [ class "bergamot-root" ]
-    [ 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)
-        ]
+    [ 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)
     ]
 
 update : Msg -> Model -> (Model, Cmd Msg)
@@ -177,7 +151,6 @@ 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