Add support for custom modes
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
d1fb4bfdc1
commit
bfc21c2928
|
|
@ -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 )` });
|
||||
});
|
||||
})();
|
||||
</script>
|
||||
</body>
|
||||
|
|
|
|||
111
src/Main.elm
111
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
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user