From bfc21c2928b3daae71d38cef64b8a7cb367ccf5c Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 7 Sep 2024 21:43:02 -0700 Subject: [PATCH] Add support for custom modes Signed-off-by: Danila Fedorin --- index.html | 9 ++++- src/Main.elm | 111 +++++++++++++++++++++++++++++++++++++-------------- 2 files changed, 88 insertions(+), 32 deletions(-) diff --git a/index.html b/index.html index 00f58c1..3b36b77 100644 --- a/index.html +++ b/index.html @@ -64,15 +64,20 @@ input[type="text"] { node: document.getElementById('elm'), flags: { inputModes: { + "My Mode": { "custom": "mymode" }, "Query": "query", "Language Term": "syntax", - "My Mode": { "custom": "mymode" }, }, inputRules: "PromptConverter @ prompt(type(empty, ?term, ?t)) <- input(?term);", - query: "type(empty, app(abs(x, number, var(x)), lit(1)), ?tau)", + input: "type(empty, app(abs(x, number, var(x)), lit(1)), ?tau)", renderRules: renderRules, rules: rules } }); + + app.ports.convertInput.subscribe(({ mode, input }) => { + console.log(input); + app.ports.receiveConverted.send({ input, query: `type(empty, lit(${input}), ?tau )` }); + }); })(); diff --git a/src/Main.elm b/src/Main.elm index 92898f2..57adbde 100644 --- 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) @@ -48,37 +48,50 @@ 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 + -- ^ The Bergamot rules to apply to convert a Syntax term into a query , tab : Tab - , query : String + -- ^ The current tab (editor, redner rule editor, rendered) + , input : String + -- ^ The string the user has in the input box + , desugaredQuery : Maybe String + -- ^ The Bergamot query corresponding to input. May be Nothing while waiting for + -- Custom mode, which has user JS convert input to a query. , 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 , inputRules : String , rules : String - , query : String + , input : String , inputModes : Json.Decode.Value } type Msg = SetProgram String | SetRenderProgram String - | SetQuery String + | SetInput String | SetTab Tab | SetInputMode Int | SetResultMode ResultMode + | SetDesugaredQuery { input: String, query: String } 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") + |> Json.Decode.andThen (\s2 -> + if s1 == s2 + then succeed v + else Json.Decode.fail "did not match expected string") editModeDecoder = oneOf [ exactString "query" Query , exactString "syntax" Syntax @@ -88,21 +101,39 @@ decodeInputModes val = in case Json.Decode.decodeValue decoder val of Ok l -> l - Err _ -> [("Query", Query), ("Language Term", Syntax)] + Err _ -> [("Language Term", Syntax), ("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, query : String } -> msg) -> Sub msg + +convertInputCmd : Int -> List (String, EditMode) -> String -> Cmd Msg +convertInputCmd 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 - , inputModes = decodeInputModes fs.inputModes - , inputMode = 0 - , resultMode = Conclusion - } - , Cmd.none - ) + let + inputModes = decodeInputModes fs.inputModes + inputMode = 0 + in + ( { program = fs.rules + , renderProgram = fs.renderRules + , inputProgram = fs.inputRules + , input = fs.input + , desugaredQuery = Nothing + , tab = Rendered + , inputModes = inputModes + , inputMode = 0 + , resultMode = Conclusion + } + , convertInputCmd inputMode inputModes fs.input + ) viewSection : String -> Html Msg -> Html Msg viewSection name content = @@ -211,18 +242,18 @@ getEditMode i l = ((_, editMode) :: xs) -> if i == 0 then Ok editMode else getEditMode (i - 1) xs -proofGoal : EditMode -> String -> String -> Result Error (Term Metavariable) -proofGoal editMode inputProgs querys = - if querys == "" +proofGoal : EditMode -> String -> String -> Maybe String -> Result Error (Term Metavariable) +proofGoal editMode inputProgs 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 + case (run program inputProgs, run topLevelExpr input) of (Just inputProg, Just e) -> let inputRule = { name = "UserInput", premises = [], conclusion = Call "input" [exprToTerm e] } @@ -237,7 +268,13 @@ proofGoal editMode inputProgs querys = _ -> Err NoConversionResults (_, Nothing) -> Err BadObjectTerm (Nothing, _) -> Err BadInputProg - Custom _ -> Err BadInputProg + Custom _ -> + case desugaredQuery of + Just querys -> + case run topLevelTerm querys of + Nothing -> Err BadQuery + Just query -> Ok query + Nothing -> Err Silent progAndRenderProg : String -> String -> Result Error (RuleEnv, RuleEnv) progAndRenderProg progs renderProgs = @@ -270,7 +307,7 @@ view : Model -> Html Msg view m = let mode = getEditMode m.inputMode m.inputModes - termOrErr = mode |> Result.andThen (\editMode -> proofGoal editMode m.inputProgram m.query) + termOrErr = mode |> Result.andThen (\editMode -> proofGoal editMode m.inputProgram m.input m.desugaredQuery) progsOrErr = progAndRenderProg m.program m.renderProgram proofTreeOrErr = combineTwoResults (viewProofTree m.resultMode) termOrErr progsOrErr in @@ -278,7 +315,7 @@ view m = [ viewSection "Input" <| Html.div [] <| [ viewInputModeSelector m.inputMode <| List.map (\(a, b) -> (b, a)) m.inputModes - , Html.input [ type_ "text", onInput SetQuery, value m.query ] [] + , Html.input [ type_ "text", onInput SetInput, value m.input ] [] ] ++ viewIfError termOrErr , viewSection "Result" <| Html.div[] @@ -300,13 +337,27 @@ 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 } + , convertInputCmd m.inputMode m.inputModes input + ) SetTab tab -> ({ m | tab = tab }, Cmd.none) - SetInputMode mode -> ({ m | inputMode = mode }, Cmd.none) + SetInputMode mode -> + ( { m | inputMode = mode } + , convertInputCmd mode m.inputModes m.input + ) SetResultMode mode -> ({ m | resultMode = mode }, Cmd.none) + SetDesugaredQuery data -> + ({ m | desugaredQuery = + if m.input == data.input + then Just data.query + else m.desugaredQuery + } + , Cmd.none + ) subscriptions : Model -> Sub Msg -subscriptions _ = Sub.none +subscriptions _ = receiveConverted SetDesugaredQuery main = Browser.element