7 changed files with 70 additions and 265 deletions
--- a/demorules.bergamot
+++ b/demorules.bergamot
@ -1,28 +0,0 @@
-section "" {
-    TNumber @ type(?Gamma, lit(?n), number) <- num(?n);
-    TString @ type(?Gamma, lit(?s), string) <- str(?s);
-    TVar @ type(?Gamma, var(?x), ?tau) <- inenv(?x, ?tau, ?Gamma);
-    TPlusI @ type(?Gamma, plus(?e_1, ?e_2), number) <-
-        type(?Gamma, ?e_1, number), type(?Gamma, ?e_2, number);
-    TPlusS @ type(?Gamma, plus(?e_1, ?e_2), string) <-
-        type(?Gamma, ?e_1, string), type(?Gamma, ?e_2, string);
-}
-section "" {
-    TPair @ type(?Gamma, pair(?e_1, ?e_2), tpair(?tau_1, ?tau_2)) <-
-        type(?Gamma, ?e_1, ?tau_1), type(?Gamma, ?e_2, ?tau_2);
-    TFst @ type(?Gamma, fst(?e), ?tau_1) <-
-        type(?Gamma, ?e, tpair(?tau_1, ?tau_2));
-    TSnd @ type(?Gamma, snd(?e), ?tau_2) <-
-        type(?Gamma, ?e, tpair(?tau_1, ?tau_2));
-}
-section "" {
-    TAbs @ type(?Gamma, abs(?x, ?tau_1, ?e), tarr(?tau_1, ?tau_2)) <-
-        type(extend(?Gamma, ?x, ?tau_1), ?e, ?tau_2);
-    TApp @ type(?Gamma, app(?e_1, ?e_2), ?tau_2) <-
-        type(?Gamma, ?e_1, tarr(?tau_1, ?tau_2)), type(?Gamma, ?e_2, ?tau_1);
-}
-
-section "" {
-    GammaTake @ inenv(?x, ?tau_1, extend(?Gamma, ?x, ?tau_1)) <-;
-    GammaSkip @ inenv(?x, ?tau_1, extend(?Gamma, ?y, ?tau_2)) <- inenv(?x, ?tau_1, ?Gamma);
-}
--- a/elm.nix
+++ b/elm.nix
@ -42,7 +42,7 @@ in mkDerivation {
  name = "bergamot-elm";
  srcs = ./elm-dependencies.nix;
  src = ./.;
-  targets = ["Main" "Bergamot.ObjectLanguage"];
+  targets = ["Main"];
  srcdir = "./src";
  outputJavaScript = true;
 }
--- a/index.html
+++ b/index.html
@ -53,42 +53,11 @@ input[type="text"] {
 <body>
    <div id="elm"></div>
    <script src="index.js"></script>
-    <script src="language.js"></script>
    <script>
-        const objectLang = Elm.Bergamot.ObjectLanguage.init({});
-
-        (async () => {
-            var rulesResponse = await fetch("./demorules.bergamot");
-            var rules = await rulesResponse.text();
-            var renderRulesResponse = await fetch("./renderrules.bergamot");
-            var renderRules = await renderRulesResponse.text();
-            console.log(rules);
-            var app = Elm.Main.init({
-                node: document.getElementById('elm'),
-                flags: {
-                    inputModes: {
-                        "Language Term": { "custom": "langterm" },
-                        "Query": "query",
-                    },
-                    inputRules: "PromptConverter @ prompt(type(empty, ?term, ?t)) <- input(?term);",
-                    input: "type(empty, app(abs(x, number, var(x)), lit(1)), ?tau)",
-                    renderRules: renderRules, rules: rules
-                }
-            });
-
-            objectLang.ports.parsedString.subscribe(({ string, term }) => {
-                if (term !== null) {
-                    const query = `type(empty, ${term}, ?tau)`;
-                    app.ports.receiveConverted.send({ input: string, result: { query } });
-                } else {
-                    app.ports.receiveConverted.send({ input: string, result: { error: "Unable to parse object language term" } });
-                }
-            });
-
-            app.ports.convertInput.subscribe(({ mode, input }) => {
-                objectLang.ports.parseString.send(input);
-            });
-        })();
+        var app = Elm.Main.init({
+          node: document.getElementById('elm'),
+          flags: { rules: "TInt @ type(?Gamma, intlit(?n), tint) <-;\nTString @ type(?Gamma, strlit(?s), tstr) <-;\nTVar @ type(?Gamma, var(?x), ?tau) <- inenv(?x, ?tau, ?Gamma);\nTPlusI @ type(?Gamma, plus(?e_1, ?e_2), tint) <- type(?Gamma, ?e_1, tint), type(?Gamma, ?e_2, tint);\nTPlusS @ type(?Gamma, plus(?e_1, ?e_2), tstr) <- type(?Gamma, ?e_1, tstr), type(?Gamma, ?e_2, tstr);\nTPair @ type(?Gamma, pair(?e_1, ?e_2), tpair(?tau_1, ?tau_2)) <- type(?Gamma, ?e_1, ?tau_1), type(?Gamma, ?e_2, ?tau_2);\nTFst @ type(?Gamma, fst(?e), ?tau_1) <- type(?Gamma, ?e, tpair(?tau_1, ?tau_2));\nTSnd @ type(?Gamma, snd(?e), ?tau_2) <- type(?Gamma, ?e, tpair(?tau_1, ?tau_2));\nTAbs @ type(?Gamma, abs(?x, ?tau_1, ?e), tarr(?tau_1, ?tau_2)) <- type(extend(?Gamma, ?x, ?tau_1), ?e, ?tau_2);\nTApp @ type(?Gamma, app(?e_1, ?e_2), ?tau_2) <- type(?Gamma, ?e_1, tarr(?tau_1, ?tau_2)), type(?Gamma, ?e_2, ?tau_1);\n\nGammaTake @ inenv(?x, ?tau_1, extend(?Gamma, ?x, ?tau_1)) <-;\nGammaSkip @ inenv(?x, ?tau_1, extend(?Gamma, ?y, ?tau_2)) <- inenv(?x, ?tau_1, ?Gamma);", query: "type(empty, app(abs(x, tint, var(x)), intlit(1)), ?tau)" }
+        });
    </script>
 </body>
 </html>
--- a/renderrules.bergamot
+++ b/renderrules.bergamot
@ -28,10 +28,10 @@ IntercalateConsNil @ intercalate(?sep, cons(?x, nil), cons(?x, nil)) <-;
 NonEmpty @ nonempty(cons(?x, ?xs)) <-;

 LatexInt @ latex(?i, ?l) <- int(?i), tostring(?i, ?l);
-LatexFloat @ latex(?f, ?l) <- float(?f), tostring(?f, ?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) <-;
-LatexLit @ latex(lit(?i), ?l) <- latex(?i, ?l);
+LatexIntLit @ latex(intlit(?i), ?l) <- latex(?i, ?l);
+LatexStrLit @ latex(strlit(?s), ?l) <- latex(?s, ?l);
 LatexVar @ latex(var(?s), ?l) <- latex(?s, ?l);
 LatexPlus @ latex(plus(?e_1, ?e_2), ?l) <-
    latex(?e_1, ?l_1), latex(?e_2, ?l_2),
@ -62,11 +62,7 @@ LatexTypeInenv @ latex(inenv(?x, ?t, ?G), ?l) <-latex(?x, ?l_x), latex(?t, ?l_t)
 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);

-LatexConverts @ latex(converts(?f, ?t), ?l) <- latex(?f, ?l_f), latex(?t, ?l_t), join([?l_f, " \\preceq ", ?l_t], ?l);
-
-LatexIsInt @ latex(int(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Int}"], ?l);
-LatexIsFloat @ latex(float(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Float}"], ?l);
-LatexIsNum @ latex(num(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Num}"], ?l);
-LatexIsStr @ latex(str(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Str}"], ?l);
+LatexIsInt @ latex(int(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\mathbb{Z}"], ?l);
+LatexIsStr @ latex(str(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\mathbb{S}"], ?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);
--- a/src/Bergamot/ObjectLanguage.elm
+++ b/src/Bergamot/ObjectLanguage.elm
@ -1,10 +1,9 @@
-port module Bergamot.ObjectLanguage exposing (..)
+module Bergamot.ObjectLanguage exposing (..)

-import Bergamot.Syntax as Syntax exposing (toString)
+import Bergamot.Syntax as Syntax exposing (Metavariable)
 import Bergamot.Parser exposing (strLit)

-import Platform exposing (worker)
-import Parser exposing (Parser, Trailing(..), (|.), (|=), run)
+import Parser exposing (Parser, Trailing(..), (|.), (|=))
 import Set

 type Type
@ -136,7 +135,7 @@ exprBasic = Parser.lazy <| \() -> Parser.oneOf
    , parenthed expr
    ]

-typeToTerm : Type -> Syntax.Term ()
+typeToTerm : Type -> Syntax.Term Metavariable
 typeToTerm t =
    case t of
        TInt -> Syntax.Call "number" []
@ -144,7 +143,7 @@ typeToTerm t =
        TPair t1 t2 -> Syntax.Call "tpair" [ typeToTerm t1, typeToTerm t2 ]
        TArr t1 t2 -> Syntax.Call "tarr" [ typeToTerm t1, typeToTerm t2 ]

-exprToTerm : Expr -> Syntax.Term ()
+exprToTerm : Expr -> Syntax.Term Metavariable
 exprToTerm e =
    case e of
        IntLit i -> Syntax.Call "lit" [Syntax.IntLit i]
@ -157,36 +156,3 @@ exprToTerm e =
        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 []]
-
-- Receives requests from JS code to apply the parser
-port parseString : (String -> msg) -> Sub msg
-
-- Used to send the result of parsing back to JS
-port parsedString : { string : String, term : Maybe String } -> Cmd msg
-
-type Msg = ParseString String
-type alias Model = ()
-type alias Flags = ()
-
-init : Flags -> (Model, Cmd Msg)
-init _ = ((), Cmd.none)
-
-update : Msg -> Model -> (Model, Cmd Msg)
-update (ParseString s) _ =
-    case run topLevelExpr s of
-        Ok e ->
-            ( ()
-            , parsedString
-                { string = s
-                , term =
-                    exprToTerm e
-                    |> toString (\_ -> "")
-                    |> Just
-                }
-            )
-        Err _ -> ((), parsedString { string = s, term = Nothing })
-
-subscriptions : Model -> Sub Msg
-subscriptions _ = parseString ParseString
-
-main = worker { init = init, update = update, subscriptions = subscriptions }
--- a/src/Bergamot/Syntax.elm
+++ b/src/Bergamot/Syntax.elm
@ -1,5 +1,5 @@
 module Bergamot.Syntax exposing
-    ( Term(..), toString, map, andThen, Metavariable(..), UnificationVar(..)
+    ( Term(..), map, andThen, Metavariable(..), UnificationVar(..)
    , unMetavariable, unUnificationVar
    , instantiate, instantiateList, InstantiationState, emptyInstantiationState, resetVars
    , unify, unifyList, UnificationState, emptyUnificationState
@ -29,15 +29,6 @@ type Term a
    | Call Name (List (Term a))
    | Var a

-toString : (a -> String) -> Term a -> String
-toString fn t =
-    case t of
-        IntLit i -> String.fromInt i
-        FloatLit f -> String.fromFloat f
-        StringLit s -> "\"" ++ s ++ "\"" -- TODO: insufficient, need to escape
-        Call n ts -> n ++ "(" ++ String.join ", " (List.map (toString fn) ts) ++ ")"
-        Var a -> fn a
-
 map : (a -> b) -> Term a -> Term b
 map f t =
    case t of
--- a/src/Main.elm
+++ b/src/Main.elm
@ -1,4 +1,4 @@
-port module Main exposing (main)
+module Main exposing (main)

 import Browser
 import Html exposing (Html)
@ -10,9 +10,9 @@ import Bergamot.Search exposing (..)
 import Bergamot.Rules exposing (..)
 import Bergamot.Parser exposing (..)
 import Bergamot.Latex exposing (..)
+import Bergamot.ObjectLanguage exposing (topLevelExpr, exprToTerm)
 import Bergamot.Utils exposing (..)
 import Json.Encode
-import Json.Decode exposing (string, field, list, oneOf, succeed, fail)
 import Maybe
 import Tuple

@ -31,17 +31,19 @@ tabEq t1 t2 =

 type EditMode
    = Query
-    | Custom String
+    | Syntax
+
+editModeEq : EditMode -> EditMode -> Bool
+editModeEq m1 m2 =
+    case (m1, m2) of
+        (Query, Query) -> True
+        (Syntax, Syntax) -> True
+        _ -> False

 type ResultMode
    = Conclusion
    | Tree

-type DesugaringState
-    = Requested
-    | Succeeded String
-    | Failed String
-
 resultModeEq : ResultMode -> ResultMode -> Bool
 resultModeEq rm1 rm2 =
    case (rm1, rm2) of
@ -51,97 +53,24 @@ resultModeEq rm1 rm2 =

 type alias Model =
    { program : String
-      -- ^ The Bergamot rules to execute a search against
    , renderProgram: String
-      -- ^ The Bergamot render rules to apply when generating LaTeX
+    , inputProgram : String
    , tab : Tab
-      -- ^ The current tab (editor, redner rule editor, rendered)
-    , input : String
-      -- ^ The string the user has in the input box
-    , desugaredQuery : DesugaringState
-      -- ^ The Bergamot query corresponding to input, if we're in custom mode.
-    , inputModes : List (String, EditMode)
-      -- ^ A List of input modes that can be used with the input box.
-    , inputMode : Int
-      -- ^ The index of the currently selected input mode.
+    , query : String
+    , editMode : EditMode
    , resultMode : ResultMode
-      -- ^ How the result should be displayed (judgement or proof tree)
-    }
-type alias Flags =
-    { renderRules : String
-    , rules : String
-    , input : String
-    , inputModes : Json.Decode.Value
    }
+type alias Flags = { renderRules: String, inputRules: String, rules: String, query: String }
 type Msg
    = SetProgram String
    | SetRenderProgram String
-    | SetInput String
+    | SetQuery String
    | SetTab Tab
-    | SetInputMode Int
+    | SetEditMode EditMode
    | SetResultMode ResultMode
-    | SetDesugaredQuery { input: String, result: Json.Decode.Value }
-
-decodeRenderResult : Json.Decode.Value -> Result String String
-decodeRenderResult val =
-    let
-        succeedDecoder = field "query" string |> Json.Decode.map Ok
-        failDecoder = field "error" string |> Json.Decode.map Err
-        decoder = Json.Decode.oneOf [ succeedDecoder, failDecoder ]
-    in
-        case Json.Decode.decodeValue decoder val of
-            Ok v -> v
-            Err _ -> Err "Unable to convert input into query"
-
-decodeInputModes : Json.Decode.Value -> List (String, EditMode)
-decodeInputModes val =
-    let
-        exactString s1 v =
-            string
-            |> Json.Decode.andThen (\s2 ->
-                if s1 == s2
-                then succeed v
-                else Json.Decode.fail "did not match expected string")
-        editModeDecoder = oneOf
-            [ exactString "query" Query
-            , field "custom" string |> Json.Decode.map Custom
-            ]
-        decoder = Json.Decode.keyValuePairs editModeDecoder
-    in
-        case Json.Decode.decodeValue decoder val of
-            Ok l -> l
-            Err _ -> [("Query", Query)]
-
-- Convert the user-entered string 'input' using custom query mode 'mode'
-port convertInput : { mode : String, input : String } -> Cmd msg
-
-- Invoked when user code finishes converting 'input' into a Bergamot query
-port receiveConverted : ({ input : String, result : Json.Decode.Value } -> msg) -> Sub msg
-
-requestDesugaring : Int -> List (String, EditMode) -> String -> Cmd Msg
-requestDesugaring inputMode inputModes input =
-    case getEditMode inputMode inputModes of
-        Ok (Custom modeType) ->
-            convertInput { mode = modeType, input = input }
-        _ -> Cmd.none

 init : Flags -> (Model, Cmd Msg)
-init fs =
-    let
-        inputModes = decodeInputModes fs.inputModes
-        inputMode = 0
-    in
-        ( { program = fs.rules
-          , renderProgram = fs.renderRules
-          , input = fs.input
-          , desugaredQuery = Requested
-          , tab = Rendered
-          , inputModes = inputModes
-          , inputMode = 0
-          , resultMode = Conclusion
-          }
-        , requestDesugaring inputMode inputModes fs.input
-        )
+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 =
@ -154,23 +83,23 @@ viewTab tab editor metaEditor rendered =
        MetaEditor -> metaEditor
        Rendered -> rendered

-viewSelector : (Int -> a -> b -> Bool) -> (Int -> a -> Msg) -> b -> List (a, String) -> Html Msg
+viewSelector : (a -> a -> Bool) -> (a -> Msg) -> a -> List (a, String) -> Html Msg
 viewSelector eq mkMsg mode modeNames =
    Html.div [ class "bergamot-selector" ] <|
-        List.indexedMap (\idx (modep, name) ->
+        List.map (\(modep, name) ->
            Html.button
-                [ classList [("active", eq idx modep mode)]
-                , onClick (mkMsg idx modep)
+                [ classList [("active", eq mode modep)]
+                , onClick (mkMsg modep)
                ] [ Html.text name ]) modeNames

 viewTabSelector : Tab -> List (Tab, String) -> Html Msg
-viewTabSelector = viewSelector (\_ -> tabEq) (\_ -> SetTab)
+viewTabSelector = viewSelector tabEq SetTab

-viewInputModeSelector : Int -> List (EditMode, String) -> Html Msg
-viewInputModeSelector = viewSelector (\i _ idx -> i == idx) (\idx _ -> SetInputMode idx)
+viewEditModeSelector : EditMode -> List (EditMode, String) -> Html Msg
+viewEditModeSelector = viewSelector editModeEq SetEditMode

 viewResultModeSelector : ResultMode -> List (ResultMode, String) -> Html Msg
-viewResultModeSelector = viewSelector (\_ -> resultModeEq) (\_ -> SetResultMode)
+viewResultModeSelector = viewSelector resultModeEq SetResultMode

 viewRule : RuleEnv -> Rule -> Maybe (Html Msg)
 viewRule env r = renderRuleViaRules env r
@ -195,12 +124,12 @@ viewRules renderProgs progs =

 type Error
    = BadQuery
+    | BadObjectTerm
    | NoConversionResults
    | BadInputProg
    | BadProg
    | BadRenderProg
-    | FailedRender String
-    | InvalidInputMode
+    | FailedRender
    | Silent

 combineTwoResults : (a -> b -> Result Error c) -> Result Error a -> Result Error b -> Result Error c
@ -216,12 +145,12 @@ errorToString : Error -> String
 errorToString err =
    case err of
        BadQuery -> "Unable to parse input query"
+        BadObjectTerm -> "Unable to parse input object language term"
        NoConversionResults -> "Failed to convert object language term to proof goal"
        BadInputProg -> "Unable to parse conversion rules from object language to proof goals"
        BadProg -> "Unable to parse rules"
        BadRenderProg -> "Unable to parse rendering rules"
-        FailedRender s -> s
-        InvalidInputMode -> "Invalid edit mode specified"
+        FailedRender -> "Unable to render terms using provided rendering rules"
        Silent -> ""

 viewError : Error -> Html Msg
@ -241,31 +170,32 @@ viewOrError r =
        Err e -> Html.div [] [ viewError e ] -- The div wrapper is needed because Elm has a bug?
        Ok html -> html

-getEditMode : Int -> List (String, EditMode) -> Result Error EditMode
-getEditMode i l =
-    case l of
-        [] -> Err InvalidInputMode
-        ((_, editMode) :: xs) ->
-            if i == 0 then Ok editMode else getEditMode (i - 1) xs
-
-proofGoal : EditMode -> String -> DesugaringState -> Result Error (Term Metavariable)
-proofGoal editMode input desugaredQuery =
-    if input == ""
+proofGoal : EditMode -> String -> String -> Result Error (Term Metavariable)
+proofGoal editMode inputProgs querys =
+    if querys == ""
    then Err Silent
    else
        case editMode of
            Query ->
-                case run topLevelTerm input of
+                case run topLevelTerm querys of
                    Nothing -> Err BadQuery
                    Just query -> Ok query
-            Custom _ ->
-                case desugaredQuery of
-                    Requested -> Err Silent
-                    Succeeded querys ->
-                        case run topLevelTerm querys of
-                            Nothing -> Err BadQuery
-                            Just query -> Ok query
-                    Failed s -> Err (FailedRender s)
+            Syntax ->
+                case (run program inputProgs, run topLevelExpr 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] -> Ok <| Bergamot.Syntax.map (MkMetavariable << unUnificationVar) t
+                                        _ -> Err NoConversionResults
+                                _ -> Err NoConversionResults
+                    (_, Nothing) -> Err BadObjectTerm
+                    (Nothing, _) -> Err BadInputProg

 progAndRenderProg : String -> String -> Result Error (RuleEnv, RuleEnv)
 progAndRenderProg progs renderProgs =
@ -297,16 +227,14 @@ viewProofTree resultMode query (prog, renderProg) =
 view : Model -> Html Msg
 view m =
    let
-        mode = getEditMode m.inputMode m.inputModes
-        termOrErr = mode |> Result.andThen (\editMode -> proofGoal editMode m.input m.desugaredQuery)
+        termOrErr = proofGoal m.editMode m.inputProgram m.query
        progsOrErr = progAndRenderProg m.program m.renderProgram
        proofTreeOrErr = combineTwoResults (viewProofTree m.resultMode) termOrErr progsOrErr
    in
        Html.div [ class "bergamot-root" ]
        [ viewSection "Input" <| Html.div [] <|
-            [ viewInputModeSelector m.inputMode <|
-                List.map (\(a, b) -> (b, a)) m.inputModes
-            , Html.input [ type_ "text", onInput SetInput, value m.input ] []
+            [ viewEditModeSelector m.editMode [(Query, "Query"), (Syntax, "Language Term")]
+            , Html.input [ type_ "text", onInput SetQuery, value m.query ] []
            ] ++
            viewIfError termOrErr
        , viewSection "Result" <| Html.div[]
@ -328,30 +256,13 @@ update msg m =
    case msg of
        SetProgram prog -> ({ m | program = prog }, Cmd.none)
        SetRenderProgram prog -> ({ m | renderProgram = prog }, Cmd.none)
-        SetInput input ->
-            ( { m | input = input, desugaredQuery = Requested }
-            , requestDesugaring m.inputMode m.inputModes input
-            )
+        SetQuery query -> ({ m | query = query }, Cmd.none)
        SetTab tab -> ({ m | tab = tab }, Cmd.none)
-        SetInputMode mode ->
-            ( { m | inputMode = mode, desugaredQuery = Requested }
-            , requestDesugaring mode m.inputModes m.input
-            )
+        SetEditMode mode -> ({ m | editMode = mode }, Cmd.none)
        SetResultMode mode -> ({ m | resultMode = mode }, Cmd.none)
-        SetDesugaredQuery data ->
-            ({ m | desugaredQuery =
-                if m.input == data.input
-                then
-                    case decodeRenderResult data.result of
-                        Ok q -> Succeeded q
-                        Err e -> Failed e
-                else m.desugaredQuery
-             }
-            , Cmd.none
-            )

 subscriptions : Model -> Sub Msg
-subscriptions _ = receiveConverted SetDesugaredQuery
+subscriptions _ = Sub.none

 main =
    Browser.element