Allow input mode code to provide custom error messages

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
Clear 'Failed' flag when input changes
2024-09-15 10:21:38 -07:00 · 2024-09-07 22:56:42 -07:00 · 2024-09-07 22:54:13 -07:00 · 2024-09-07 22:29:32 -07:00 · 2024-09-07 22:24:29 -07:00 · 2024-09-07 21:43:02 -07:00
7 changed files with 265 additions and 70 deletions
--- a/demorules.bergamot
+++ b/demorules.bergamot
@ -0,0 +1,28 @@
+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"];
+  targets = ["Main" "Bergamot.ObjectLanguage"];
  srcdir = "./src";
  outputJavaScript = true;
 }
--- a/index.html
+++ b/index.html
@ -53,11 +53,42 @@ input[type="text"] {
 <body>
    <div id="elm"></div>
    <script src="index.js"></script>
+    <script src="language.js"></script>
    <script>
-        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)" }
-        });
+        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);
+            });
+        })();
    </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) <-;
-LatexIntLit @ latex(intlit(?i), ?l) <- latex(?i, ?l);
-LatexStrLit @ latex(strlit(?s), ?l) <- latex(?s, ?l);
+LatexLit @ latex(lit(?i), ?l) <- latex(?i, ?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,7 +62,11 @@ 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);

-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);
+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);
 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,9 +1,10 @@
-module Bergamot.ObjectLanguage exposing (..)
+port module Bergamot.ObjectLanguage exposing (..)

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

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

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

-typeToTerm : Type -> Syntax.Term Metavariable
+typeToTerm : Type -> Syntax.Term ()
 typeToTerm t =
    case t of
        TInt -> Syntax.Call "number" []
@ -143,7 +144,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 Metavariable
+exprToTerm : Expr -> Syntax.Term ()
 exprToTerm e =
    case e of
        IntLit i -> Syntax.Call "lit" [Syntax.IntLit i]
@ -156,3 +157,36 @@ 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(..), map, andThen, Metavariable(..), UnificationVar(..)
+    ( Term(..), toString, map, andThen, Metavariable(..), UnificationVar(..)
    , unMetavariable, unUnificationVar
    , instantiate, instantiateList, InstantiationState, emptyInstantiationState, resetVars
    , unify, unifyList, UnificationState, emptyUnificationState
@ -29,6 +29,15 @@ 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 @@
-module Main exposing (main)
+port 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,19 +31,17 @@ tabEq t1 t2 =

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

 type ResultMode
    = Conclusion
    | Tree

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

 type alias Model =
    { program : String
+      -- ^ The Bergamot rules to execute a search against
    , renderProgram: String
-    , inputProgram : String
+      -- ^ The Bergamot render rules to apply when generating LaTeX
    , tab : Tab
-    , query : String
-    , editMode : EditMode
+      -- ^ 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.
    , 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
-    | SetQuery String
+    | SetInput String
    | SetTab Tab
-    | SetEditMode EditMode
+    | SetInputMode Int
    | 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 = ({ program = fs.rules, renderProgram = fs.renderRules, inputProgram = fs.inputRules, query = fs.query, tab = Rendered, editMode = Syntax, resultMode = Conclusion }, Cmd.none)
+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
+        )

 viewSection : String -> Html Msg -> Html Msg
 viewSection name content =
@ -83,23 +154,23 @@ viewTab tab editor metaEditor rendered =
        MetaEditor -> metaEditor
        Rendered -> rendered

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

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

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

 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
@ -124,12 +195,12 @@ viewRules renderProgs progs =

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

 combineTwoResults : (a -> b -> Result Error c) -> Result Error a -> Result Error b -> Result Error c
@ -145,12 +216,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 -> "Unable to render terms using provided rendering rules"
+        FailedRender s -> s
+        InvalidInputMode -> "Invalid edit mode specified"
        Silent -> ""

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

-proofGoal : EditMode -> String -> String -> Result Error (Term Metavariable)
-proofGoal editMode inputProgs querys =
-    if querys == ""
+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 == ""
    then Err Silent
    else
        case editMode of
            Query ->
-                case run topLevelTerm querys of
+                case run topLevelTerm input of
                    Nothing -> Err BadQuery
                    Just query -> Ok query
-            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
+            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)

 progAndRenderProg : String -> String -> Result Error (RuleEnv, RuleEnv)
 progAndRenderProg progs renderProgs =
@ -227,14 +297,16 @@ viewProofTree resultMode query (prog, renderProg) =
 view : Model -> Html Msg
 view m =
    let
-        termOrErr = proofGoal m.editMode m.inputProgram m.query
+        mode = getEditMode m.inputMode m.inputModes
+        termOrErr = mode |> Result.andThen (\editMode -> proofGoal editMode m.input m.desugaredQuery)
        progsOrErr = progAndRenderProg m.program m.renderProgram
        proofTreeOrErr = combineTwoResults (viewProofTree m.resultMode) termOrErr progsOrErr
    in
        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 ] []
+            [ viewInputModeSelector m.inputMode <|
+                List.map (\(a, b) -> (b, a)) m.inputModes
+            , Html.input [ type_ "text", onInput SetInput, value m.input ] []
            ] ++
            viewIfError termOrErr
        , viewSection "Result" <| Html.div[]
@ -256,13 +328,30 @@ update msg m =
    case msg of
        SetProgram prog -> ({ m | program = prog }, Cmd.none)
        SetRenderProgram prog -> ({ m | renderProgram = prog }, Cmd.none)
-        SetQuery query -> ({ m | query = query }, Cmd.none)
+        SetInput input ->
+            ( { m | input = input, desugaredQuery = Requested }
+            , requestDesugaring m.inputMode m.inputModes input
+            )
        SetTab tab -> ({ m | tab = tab }, Cmd.none)
-        SetEditMode mode -> ({ m | editMode = mode }, Cmd.none)
+        SetInputMode mode ->
+            ( { m | inputMode = mode, desugaredQuery = Requested }
+            , requestDesugaring mode m.inputModes m.input
+            )
        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 _ = Sub.none
+subscriptions _ = receiveConverted SetDesugaredQuery

 main =
    Browser.element
Author	SHA1	Message	Date
Danila Fedorin	e7d3e840b3	Allow input mode code to provide custom error messages Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-09-15 10:21:38 -07:00
Danila Fedorin	a17ea205c7	Clear 'Failed' flag when input changes Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-09-07 22:56:42 -07:00
Danila Fedorin	2a0db676bc	Remove useless inputRules flag Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-09-07 22:54:13 -07:00
Danila Fedorin	a7b3efe56c	Tweak API to support syntax errors in custom parsing Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-09-07 22:29:32 -07:00
Danila Fedorin	ec0b05ab51	Make 'language term' just a custom mode Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-09-07 22:24:29 -07:00
Danila Fedorin	bfc21c2928	Add support for custom modes Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-09-07 21:43:02 -07:00
Danila Fedorin	d1fb4bfdc1	Update index.html to work with new setup Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-09-07 21:06:57 -07:00
Danila Fedorin	b6569d8ca0	Allow for customizing the "input mode" toolbar Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-09-07 21:02:15 -07:00