Avoid checking for out-of-gas on each 'andThen'

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

renderrules.bergamot

@@ -0,0 +1,32 @@
+LatexListNil @ latexlist(nil, nil) <-;
+LatexListCons @ latexlist(cons(?x, ?xs), cons(?l_x, ?l_s)) <- latex(?x, ?l_x), latexlist(?xs, ?l_s);
+
+IntercalateNil @ intercalate(?sep, nil, nil) <-;
+IntercalateConsCons @ intercalate(?sep, cons(?x_1, cons(?x_2, ?xs)), cons(?x_1, cons(?sep, ?ys))) <- intercalate(?sep, cons(?x_2, ?xs), ?ys);
+IntercalateConsNil @ intercalate(?sep, cons(?x, nil), cons(?x, nil)) <-;
+
+NonEmpty @ nonempty(cons(?x, ?xs)) <-;
+
+LatexInt @ latex(?i, ?l) <- int(?i), tostring(?i, ?l);
+LatexStr @ latex(?s, ?l) <- str(?s), escapestring(?s, ?l_1), latexifystring(?s, ?l_2), join(["\\texttt{\"", ?l_2, "\"}"], ?l);
+LatexMeta @ latex(metavariable(?l), ?l) <-;
+LatexSym @ latex(?s, ?l) <- sym(?s), tostring(?s, ?l_1), join(["\\text{", ?l_1,"}"], ?l);
+LatexCall @ latex(?c, ?l) <- call(?c, ?n, ?ts), nonempty(?ts), latexlist(?ts, ?lts_1), intercalate(", ", ?lts_1, ?lts_2), join(?lts_2, ?lts_3), join(["\\text{", ?n, "}", "(", ?lts_3, ")"], ?l);
+LatexIntLit @ latex(intlit(?i), ?l) <- latex(?i, ?l);
+LatexStrLit @ latex(strlit(?s), ?l) <- latex(?s, ?l);
+LatexPlus @ latex(plus(?e_1, ?e_2), ?l) <- latex(?e_1, ?l_1), latex(?e_2, ?l_2), join([?l_1, " + ", ?l_2], ?l);
+LatexPair @ latex(pair(?e_1, ?e_2), ?l) <- latex(?e_1, ?l_1), latex(?e_2, ?l_2), join(["(", ?l_1, ",  ", ?l_2, ")"], ?l);
+LatexAbs @ latex(abs(?x, ?t, ?e), ?l) <- latex(?e, ?l_e), latex(?t, ?l_t), latex(?x, ?l_x), join(["\\lambda ", ?l_x, " : ", ?l_t, " . ", ?l_e], ?l);
+LatexApp @ latex(app(?e_1, ?e_2), ?l) <- latex(?e_1, ?l_1), latex(?e_2, ?l_2), join([?l_1, " \\enspace ", ?l_2], ?l);
+
+LatexTInt @ latex(tint, "\\text{tint}") <-;
+LatexTStr @ latex(tstr, "\\text{tstr}") <-;
+LatexTArr @ latex(tarr(?t_1, ?t_2), ?l) <- latex(?t_1, ?l_1), latex(?t_2, ?l_2), join([?l_1, " \\to ", ?l_2], ?l);
+LatexTPair @ latex(tpair(?t_1, ?t_2), ?l) <- latex(?t_1, ?l_1), latex(?t_2, ?l_2), join([?l_1, " \\times ", ?l_2], ?l);
+
+LatexTypeEmpty @ latex(empty, "\\varnothing") <-;
+LatexTypeExtend @ latex(extend(?a, ?b, ?c), ?l) <- latex(?a, ?l_a), latex(?b, ?l_b), latex(?c, ?l_c), join([?l_a, " , ", ?l_b, " : ", ?l_c], ?l);
+LatexTypeInenv @ latex(inenv(?x, ?t, ?G), ?l) <-latex(?x, ?l_x), latex(?t, ?l_t), latex(?G, ?l_G), join([?l_x, " : ", ?l_t, " \\in ", ?l_G], ?l);
+
+LatexTypeBin @ latex(type(?e, ?t), ?l) <- latex(?e, ?l_e), latex(?t, ?l_t), join([?l_e, " : ", ?l_t], ?l);
+LatexTypeTer @ latex(type(?G, ?e, ?t), ?l) <- latex(?G, ?l_G), latex(?e, ?l_e), latex(?t, ?l_t), join([?l_G, " \\vdash ", ?l_e, " : ", ?l_t], ?l);

src/Bergamot/Latex.elm

@@ -1,7 +1,49 @@
 module Bergamot.Latex exposing (..)
 
-import Bergamot.Syntax exposing (..)
-import Bergamot.Rules exposing (..)
+import Bergamot.Syntax as Syntax exposing (..)
+import Bergamot.Rules as Rules 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 v = Call "metavariable" [StringLit <| metavariableToLatex v]
 
 termToLatex : (a -> String) -> Term a -> String
 termToLatex f t =
@@ -24,7 +66,7 @@ termToLatex f t =
         Call s ts -> "\\text{" ++ s ++ "}(" ++ String.join "," (List.map (termToLatex f) ts) ++ ")"
         Var x -> f x
         IntLit i -> String.fromInt i
-        StringLit s -> "\"" ++ s ++ "\""
+        StringLit s -> "\\texttt{" ++ "\"" ++ encodeLatex (encodeStr s) ++ "\"" ++ "}"
 
 metavariableToLatex : Metavariable -> String
 metavariableToLatex (MkMetavariable s) =

src/Bergamot/ObjectLanguage.elm

@@ -0,0 +1,144 @@
+module Bergamot.ObjectLanguage exposing (..)
+
+import Bergamot.Syntax as Syntax exposing (Metavariable)
+
+import Parser exposing (Parser, Trailing(..), (|.), (|=))
+import Set
+
+type Type
+    = TInt
+    | TStr
+    | TPair Type Type
+    | TArr Type Type
+
+type Expr
+    = IntLit Int
+    | StrLit String
+    | Plus Expr Expr
+    | Pair Expr Expr
+    | Fst Expr
+    | Snd Expr
+    | Abs String Type Expr
+    | App Expr Expr
+    | Ref String
+
+parseParenthed : Parser a -> Parser a
+parseParenthed val = Parser.succeed (\x -> x)
+    |. Parser.symbol "("
+    |. Parser.spaces
+    |= val
+    |. Parser.spaces
+    |. Parser.symbol ")"
+
+parsePair : Parser a -> Parser (a, a)
+parsePair elem = parseParenthed <|
+    Parser.succeed Tuple.pair
+    |= elem
+    |. Parser.spaces
+    |. Parser.symbol ","
+    |. Parser.spaces
+    |= elem
+
+parseType : Parser Type
+parseType = Parser.lazy <| \() -> Parser.oneOf
+    [ Parser.backtrackable <| Parser.succeed TArr
+        |= parseTypeBasic
+        |. Parser.spaces
+        |. Parser.symbol "->"
+        |. Parser.spaces
+        |= parseType
+    , parseTypeBasic
+    ]
+
+parseTypeBasic : Parser Type
+parseTypeBasic = Parser.lazy <| \() -> Parser.oneOf
+    [ Parser.succeed TInt |. Parser.keyword "tint"
+    , Parser.succeed TStr |. Parser.keyword "tstr"
+    , Parser.backtrackable <| Parser.map (\(a, b) -> TPair a b) <| parsePair parseType
+    , parseParenthed parseType
+    ]
+
+parseVariable : Parser String
+parseVariable = Parser.variable
+    { start = Char.isAlphaNum
+    , inner = Char.isAlphaNum
+    , reserved = Set.fromList ["fst", "snd", "let", "in"]
+    }
+
+parseExpr : Parser Expr
+parseExpr = Parser.lazy <| \() -> Parser.oneOf
+    [ Parser.backtrackable <| Parser.succeed Plus
+        |= parseExprBasic
+        |. Parser.spaces
+        |. Parser.symbol "+"
+        |. Parser.spaces
+        |= parseExpr
+    , parseExprApps
+    ]
+
+parseExprApps : Parser Expr
+parseExprApps =
+    let
+        handle l =
+            case l of
+                [] -> Parser.problem "no applications found"
+                x :: xs -> Parser.succeed <| List.foldl (\a b -> App b a) x xs
+    in
+        Parser.sequence
+            { start = ""
+            , separator = " "
+            , end = ""
+            , spaces = Parser.succeed ()
+            , item = parseExprBasic
+            , trailing = Optional
+            }
+        |> Parser.andThen handle
+
+parseExprBasic : Parser Expr
+parseExprBasic = Parser.lazy <| \() -> Parser.oneOf
+    [ Parser.backtrackable (Parser.succeed IntLit |= Parser.int)
+    , Parser.backtrackable <| Parser.map (\(a, b) -> Pair a b) <| parsePair parseExpr
+    , Parser.succeed Fst
+        |. Parser.keyword "fst"
+        |. Parser.spaces
+        |= parseParenthed parseExpr
+    , Parser.succeed Snd
+        |. Parser.keyword "snd"
+        |. Parser.spaces
+        |= parseParenthed parseExpr
+    , Parser.succeed Abs
+        |. Parser.symbol "\\"
+        |. Parser.spaces
+        |= parseVariable
+        |. Parser.spaces
+        |. Parser.symbol ":"
+        |. Parser.spaces
+        |= parseType
+        |. Parser.spaces
+        |. Parser.symbol "."
+        |. Parser.spaces
+        |= parseExpr
+    , Parser.succeed Ref |= parseVariable
+    , parseParenthed parseExpr
+    ]
+
+typeToTerm : Type -> Syntax.Term Metavariable
+typeToTerm t =
+    case t of
+        TInt -> Syntax.Call "tint" []
+        TStr -> Syntax.Call "tstr" []
+        TPair t1 t2 -> Syntax.Call "tpair" [ typeToTerm t1, typeToTerm t2 ]
+        TArr t1 t2 -> Syntax.Call "tarr" [ typeToTerm t1, typeToTerm t2 ]
+
+exprToTerm : Expr -> Syntax.Term Metavariable
+exprToTerm e =
+    case e of
+        IntLit i -> Syntax.Call "intlit" [Syntax.IntLit i]
+        StrLit s -> Syntax.Call "strlit" [Syntax.StringLit s]
+        Plus e1 e2 -> Syntax.Call "plus" [exprToTerm e1, exprToTerm e2]
+        Pair e1 e2 -> Syntax.Call "pair" [exprToTerm e1, exprToTerm e2]
+        Fst ep -> Syntax.Call "fst" [exprToTerm ep]
+        Snd ep -> Syntax.Call "snd" [exprToTerm ep]
+        Abs s t ep -> Syntax.Call "abs" [Syntax.Call s [], typeToTerm t, exprToTerm ep]
+        App e1 e2 -> Syntax.Call "app" [exprToTerm e1, exprToTerm e2]
+        Ref x -> Syntax.Call "var" [Syntax.Call x []]

src/Bergamot/Parser.elm

@@ -2,6 +2,7 @@ module Bergamot.Parser exposing (..)
 
 import Bergamot.Syntax exposing (Term(..), Metavariable(..))
 import Bergamot.Rules exposing (Rule, RuleEnv)
+import Bergamot.Utils exposing (decodeStr)
 
 import Parser exposing (Parser, Trailing(..), (|.), (|=))
 import Set
@@ -9,9 +10,30 @@ import Set
 intLit : Parser Int
 intLit = Parser.int
 
+strLit : Parser String
+strLit =
+    let
+        char = Parser.map decodeStr <| Parser.getChompedString <|
+            Parser.oneOf
+                [ Parser.backtrackable <|
+                    Parser.chompIf (\c -> c == '\\')
+                    |. Parser.chompIf (\c -> True)
+                , Parser.backtrackable <| Parser.chompIf (\c -> c /= '"')
+                ]
+    in
+        Parser.map (String.join "") <| Parser.sequence
+            { start = "\""
+            , separator = ""
+            , end = "\""
+            , spaces = Parser.succeed ()
+            , item = char
+            , trailing = Optional
+            }
+
+
 name : Parser String
 name = Parser.variable
-    { start = \c -> Char.isAlphaNum c || c == '_'
+    { start = \c -> Char.isAlpha c || c == '_'
     , inner = \c -> Char.isAlphaNum c || c == '_'
     , reserved = Set.empty
     }
@@ -38,12 +60,23 @@ term = Parser.lazy (\() -> Parser.oneOf
             , item = term
             , trailing = Forbidden
             }
+    , Parser.backtrackable
+        <| Parser.map (List.foldr (\x xs -> Call "cons" [x, xs]) (Call "nil" []))
+        <| Parser.sequence
+            { start = "["
+            , separator = ","
+            , end = "]"
+            , spaces = Parser.spaces
+            , item = term
+            , trailing = Forbidden
+            }
     , Parser.backtrackable <|
       Parser.succeed (\n -> Call n [])
         |= name
     , Parser.backtrackable <|
       Parser.succeed Var |= variable
     , Parser.succeed IntLit |= intLit
+    , Parser.succeed StringLit |= strLit
     ])
 
 rule : Parser Rule

src/Bergamot/Rules.elm

@@ -1,7 +1,8 @@
 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.Utils exposing (encodeStr, encodeLatex)
 
 import Debug
 
@@ -32,7 +33,7 @@ type alias Prover a = RuleEnv -> ProveState -> Search (a, ProveState)
 andThen : (a -> Prover b) -> Prover a -> Prover b
 andThen f p env ps =
     p env ps
-    |> Search.andThen (\(a, psp) -> if psp.gas > 0 then (f a) env psp else Search.fail)
+    |> Search.andThen (\(a, psp) -> (f a) env psp)
 
 join : Prover (Prover a) -> Prover a
 join p = andThen (\x -> x) p
@@ -74,7 +75,7 @@ getUnificationState : Prover UnificationState
 getUnificationState env ps = Search.pure (ps.unificationState, ps)
 
 burn : Prover ()
-burn env ps = Search.pure ((), { ps | gas = ps.gas - 1})
+burn env ps = if ps.gas > 0 then Search.pure ((), { ps | gas = ps.gas - 1}) else Search.fail
 
 liftInstantiation : (a -> InstantiationState -> (b, InstantiationState)) -> a -> Prover b
 liftInstantiation f a env ps =
@@ -104,25 +105,71 @@ reifyProofTree (MkProofTree node) =
 rule : Term UnificationVar -> Rule -> Prover ProofTree
 rule t r =
         withVars (pure Tuple.pair
-            |> apply (liftInstantiation instantiate r.conclusion)
+            |> apply (liftInstantiation instantiate r.conclusion
+                |> andThen (\conc -> liftUnification unify t conc))
             |> apply (liftInstantiation instantiateList r.premises))
         |> andThen (\(conc, prems) ->
-            pure (\tp trees -> MkProofTree { name = r.name, conclusion = tp, premises = trees })
-            |> apply (liftUnification unify t conc)
-            |> apply (provePremises prems))
+            provePremises prems)
+            |> map (\trees -> MkProofTree { name = r.name, conclusion = t, premises = trees })
+
+collectStrings : Term UnificationVar -> Prover (List String)
+collectStrings t =
+    case t of
+        Call "cons" [StringLit s, rest] -> map (\ss -> s :: ss) <| collectStrings rest
+        Call "nil" [] -> pure []
+        _ -> fail
+
+builtinRules : Term UnificationVar -> Prover ProofTree
+builtinRules t =
+    case t of
+        Call "concat" [StringLit s1, StringLit s2, Var output] ->
+            liftUnification unify (Var output) (StringLit (s1 ++ s2))
+            |> map (\_ -> MkProofTree { name = "BuiltinConcat", conclusion = t, premises = []})
+        Call "join" [tp, Var output] ->
+            collectStrings tp
+            |> andThen (\ss -> liftUnification unify (Var output) (StringLit (String.concat ss)))
+            |> map (\_ -> MkProofTree { name = "BuiltinJoin", conclusion = t, premises = []})
+        Call "int" [IntLit i] ->
+            MkProofTree { name = "BuiltinInt", conclusion = t, premises = [] }
+            |> pure
+        Call "str" [StringLit s] ->
+            MkProofTree { name = "BuiltinStr", conclusion = t, premises = [] }
+            |> pure
+        Call "sym" [Call s []] ->
+            MkProofTree { name = "BuiltinSym", conclusion = t, premises = [] }
+            |> pure
+        Call "call" [Call s ts, Var name, Var args] ->
+            pure (\_ _ -> MkProofTree { name = "BuiltinCall", conclusion = t, premises = [] })
+            |> apply (liftUnification unify (Var name) (StringLit <| encodeStr s))
+            |> apply (liftUnification unify (Var args) (List.foldr (\x xs -> Call "cons" [x, xs]) (Call "nil" []) ts))
+        Call "tostring" [IntLit i, Var output] ->
+            liftUnification unify (Var output) (StringLit (String.fromInt i))
+            |> map (\_ -> MkProofTree { name = "BuiltinToString", conclusion = t, premises = []})
+        Call "tostring" [Call s [], Var output] ->
+            liftUnification unify (Var output) (StringLit <| encodeStr s)
+            |> 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
 
 provePremises : List (Term UnificationVar) -> Prover (List ProofTree)
 provePremises = mapM proveTerm
 
 proveTerm : Term UnificationVar -> Prover ProofTree
 proveTerm t =
-    burn
-    |> andThen (\() -> getEnv)
-    |> andThen (\env -> List.foldl (\r -> interleave (yield (rule t r))) fail env.rules)
+    map (reify t) getUnificationState
+    |> andThen (\tp ->
+        burn
+        |> andThen (\() -> getEnv)
+        |> andThen (\env -> List.foldl (\r -> interleave (yield (rule tp r))) (builtinRules tp) env.rules))
 
 prove : Term Metavariable -> Prover ProofTree
 prove mt =
-    liftInstantiation instantiate mt
+    withVars (liftInstantiation instantiate mt)
     |> andThen proveTerm
 
 single : RuleEnv -> Prover a -> Maybe a

src/Bergamot/Syntax.elm

@@ -1,5 +1,5 @@
 module Bergamot.Syntax exposing
-    ( Term(..), Metavariable(..), UnificationVar(..)
+    ( Term(..), map, andThen, Metavariable(..), UnificationVar(..)
     , instantiate, instantiateList, InstantiationState, emptyInstantiationState, resetVars
     , unify, unifyList, UnificationState, emptyUnificationState
     , reify
@@ -27,6 +27,22 @@ type Term a
     | Call Name (List (Term 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 =
     { counter : Int
     , vars : Dict String UnificationVar

src/Bergamot/Utils.elm

@@ -0,0 +1,46 @@
+module Bergamot.Utils exposing (..)
+
+decodeStr : String -> String
+decodeStr str =
+    let
+        go l =
+            case l of
+                '\\' :: '"' :: rest -> '"' :: go rest
+                '\\' :: c :: rest -> c :: go rest
+                c :: rest -> c :: go rest
+                [] -> []
+        noQuotes = String.dropLeft 1 <| String.dropRight 1 <| str
+    in
+        String.fromList (go (String.toList str))
+
+encodeStr : String -> String
+encodeStr s =
+    let
+        go l =
+            case l of
+                '\\' :: xs -> '\\' :: '\\' :: go xs
+                '"' :: xs -> '\\' :: '"' :: go xs
+                x :: xs -> x :: go xs
+                [] -> []
+    in
+        String.fromList (go (String.toList s))
+
+encodeLatex : String -> String
+encodeLatex s =
+    let
+        go l =
+            case l of
+                '\\' :: xs -> String.toList "\\textbackslash " ++ go xs
+                '{' :: xs -> '\\' :: '{' :: go xs
+                '}' :: xs -> '\\' :: '}' :: go xs
+                x :: xs -> x :: go xs
+                [] -> []
+    in
+        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

src/Main.elm

@@ -2,64 +2,123 @@ module Main exposing (main)
 
 import Browser
 import Html exposing (Html)
-import Html.Events exposing (onInput)
-import Html.Attributes exposing (type_, class, value)
+import Html.Events exposing (onInput, onClick)
+import Html.Attributes exposing (type_, class, classList, value)
+import Html.Lazy
 import Bergamot.Syntax exposing (..)
 import Bergamot.Search exposing (..)
 import Bergamot.Rules exposing (..)
 import Bergamot.Parser exposing (..)
 import Bergamot.Latex exposing (..)
+import Bergamot.ObjectLanguage exposing (..)
 import Json.Encode
 import Maybe
 import Tuple
-import Debug
+
+type Tab
+    = Editor
+    | Rendered
+
+tabEq : Tab -> Tab -> Bool
+tabEq t1 t2 =
+    case (t1, t2) of
+        (Editor, Editor) -> True
+        (Rendered, Rendered) -> True
+        _ -> False
+
+type EditMode
+    = Query
+    | Syntax
+
+modeEq : EditMode -> EditMode -> Bool
+modeEq m1 m2 =
+    case (m1, m2) of
+        (Query, Query) -> True
+        (Syntax, Syntax) -> True
+        _ -> False
 
 type alias Model =
     { program : String
+    , renderProgram: String
     , query : String
+    , tab : Tab
+    , editMode : EditMode
     }
-type alias Flags = { rules: String, query: String }
+type alias Flags = { renderRules: String, rules: String, query: String }
 type Msg
     = SetProgram String
     | SetQuery String
+    | SetTab Tab
+    | SetEditMode EditMode
 
 init : Flags -> (Model, Cmd Msg)
-init fs = ({ program = fs.rules, query = fs.query }, 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 =
     Html.div [ class "bergamot-section" ] [ Html.em [ class "bergamot-section-heading" ] [ Html.text name ], content ]
 
-viewRule : Rule -> Html Msg
-viewRule = latex << ruleToLatex
+viewTab : Tab -> Html Msg -> Html Msg -> Html Msg
+viewTab tab editor rendered =
+    case tab of
+        Editor -> editor
+        Rendered -> rendered
 
-viewRules : String -> Html Msg
-viewRules progs = viewSection "Rendered Rules" <|
+viewSelector : (a -> a -> Bool) -> (a -> Msg) -> a -> List (a, String) -> Html Msg
+viewSelector eq mkMsg mode modeNames =
+    Html.div [ class "bergamot-selector" ] <|
+        List.map (\(modep, name) ->
+            Html.button
+                [ classList [("active", eq mode modep)]
+                , onClick (mkMsg modep)
+                ] [ Html.text name ]) modeNames
+
+viewTabSelector : Tab -> List (Tab, String) -> Html Msg
+viewTabSelector = viewSelector tabEq SetTab
+
+viewEditModeSelector : EditMode -> List (EditMode, String) -> Html Msg
+viewEditModeSelector = viewSelector modeEq SetEditMode
+
+viewRule : RuleEnv -> Rule -> Maybe (Html Msg)
+viewRule env r = renderRuleViaRules env r
+    |> Maybe.map latex
+
+viewRules : String -> String -> Html Msg
+viewRules renderProgs progs = viewSection "Rendered Rules" <|
     Html.div [ class "bergamot-rule-list" ] <|
-        case run program progs of
-            Just prog -> List.map viewRule prog.rules
-            Nothing -> []
+        case (run program renderProgs, run program progs) of
+            (Just renderProg, Just prog) -> List.filterMap (viewRule renderProg) prog.rules
+            _ -> []
 
-tryProve : String -> String -> Maybe ProofTree
-tryProve progs querys =
-    case (run program progs, run term querys) of
+proofGoal : EditMode -> String -> Maybe (Term Metavariable)
+proofGoal mode querys =
+    case mode of
+        Query -> run term querys
+        Syntax -> Maybe.map (\e -> Call "type" [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
         (Just prog, Just query) -> single prog (prove query |> Bergamot.Rules.andThen reifyProofTree)
         _ -> Nothing
 
-viewProofTree : String -> String -> Html Msg
-viewProofTree progs querys = viewSection "Proof Tree" <|
+viewProofTree : EditMode -> String -> String -> Html Msg
+viewProofTree mode progs querys = viewSection "Proof Tree" <|
     Html.div [ class "bergamot-proof-tree" ] <|
-      case tryProve progs querys of
+      case tryProve mode progs querys of
           Just tree -> [ latex (proofTreeToLatex tree) ]
           Nothing -> []
 
 
 view : Model -> Html Msg
 view m = Html.div [ class "bergamot-root" ]
-    [ viewSection "Rules" <| Html.textarea [ onInput SetProgram ] [ Html.text m.program ]
+    [ viewTabSelector m.tab [(Editor, "Rule Editor"), (Rendered, "Rendered Rules")]
+    , viewEditModeSelector m.editMode [(Query, "Query"), (Syntax, "Language Term")]
+    , viewTab m.tab
+        (viewSection "Rules" <| Html.textarea [ onInput SetProgram ] [ Html.text m.program ])
+        (Html.Lazy.lazy2 viewRules m.renderProgram m.program)
     , viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery, value m.query ] []
-    , viewRules m.program
-    , viewProofTree m.program m.query
+    , viewProofTree m.editMode m.program m.query
     ]
 
 update : Msg -> Model -> (Model, Cmd Msg)
@@ -67,6 +126,8 @@ update msg m =
     case msg of
         SetProgram prog -> ({ m | program = prog }, Cmd.none)
         SetQuery query -> ({ m | query = query }, Cmd.none)
+        SetTab tab -> ({ m | tab = tab }, Cmd.none)
+        SetEditMode mode -> ({ m | editMode = mode }, Cmd.none)
 
 subscriptions : Model -> Sub Msg
 subscriptions _ = Sub.none