diff --git a/index.html b/index.html index 919bac7..e3afda7 100644 --- a/index.html +++ b/index.html @@ -80,6 +80,8 @@ input[type="text"] { if (term !== null) { const query = `type(empty, ${term}, ?tau)`; app.ports.receiveConverted.send({ input: string, query }); + } else { + app.ports.receiveConverted.send({ input: string, query: null }); } }); diff --git a/src/Main.elm b/src/Main.elm index 77c777d..a8e8af9 100644 --- a/src/Main.elm +++ b/src/Main.elm @@ -37,6 +37,11 @@ type ResultMode = Conclusion | Tree +type DesugaringState + = Requested + | Succeeded String + | Failed + resultModeEq : ResultMode -> ResultMode -> Bool resultModeEq rm1 rm2 = case (rm1, rm2) of @@ -53,9 +58,8 @@ type alias Model = -- ^ 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. + , 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 @@ -77,7 +81,7 @@ type Msg | SetTab Tab | SetInputMode Int | SetResultMode ResultMode - | SetDesugaredQuery { input: String, query: String } + | SetDesugaredQuery { input: String, query: Maybe String } decodeInputModes: Json.Decode.Value -> List (String, EditMode) decodeInputModes val = @@ -102,10 +106,10 @@ decodeInputModes val = 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 +port receiveConverted : ({ input : String, query : Maybe String } -> msg) -> Sub msg -convertInputCmd : Int -> List (String, EditMode) -> String -> Cmd Msg -convertInputCmd inputMode inputModes input = +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 } @@ -120,13 +124,13 @@ init fs = ( { program = fs.rules , renderProgram = fs.renderRules , input = fs.input - , desugaredQuery = Nothing + , desugaredQuery = Failed , tab = Rendered , inputModes = inputModes , inputMode = 0 , resultMode = Conclusion } - , convertInputCmd inputMode inputModes fs.input + , requestDesugaring inputMode inputModes fs.input ) viewSection : String -> Html Msg -> Html Msg @@ -236,7 +240,7 @@ getEditMode i l = ((_, editMode) :: xs) -> if i == 0 then Ok editMode else getEditMode (i - 1) xs -proofGoal : EditMode -> String -> Maybe String -> Result Error (Term Metavariable) +proofGoal : EditMode -> String -> DesugaringState -> Result Error (Term Metavariable) proofGoal editMode input desugaredQuery = if input == "" then Err Silent @@ -248,11 +252,12 @@ proofGoal editMode input desugaredQuery = Just query -> Ok query Custom _ -> case desugaredQuery of - Just querys -> + Requested -> Err Silent + Succeeded querys -> case run topLevelTerm querys of Nothing -> Err BadQuery Just query -> Ok query - Nothing -> Err Silent + Failed -> Err BadObjectTerm progAndRenderProg : String -> String -> Result Error (RuleEnv, RuleEnv) progAndRenderProg progs renderProgs = @@ -317,18 +322,21 @@ update msg m = SetRenderProgram prog -> ({ m | renderProgram = prog }, Cmd.none) SetInput input -> ( { m | input = input } - , convertInputCmd m.inputMode m.inputModes input + , requestDesugaring m.inputMode m.inputModes input ) SetTab tab -> ({ m | tab = tab }, Cmd.none) SetInputMode mode -> ( { m | inputMode = mode } - , convertInputCmd mode m.inputModes m.input + , requestDesugaring 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 + then + case data.query of + Just q -> Succeeded q + Nothing -> Failed else m.desugaredQuery } , Cmd.none