diff --git a/src/Main.elm b/src/Main.elm index 0468319..92898f2 100644 --- a/src/Main.elm +++ b/src/Main.elm @@ -13,6 +13,7 @@ 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 @@ -32,13 +33,7 @@ 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 @@ -57,20 +52,57 @@ type alias Model = , inputProgram : String , tab : Tab , query : String - , editMode : EditMode + , inputModes : List (String, EditMode) + , inputMode : Int , resultMode : ResultMode } -type alias Flags = { renderRules: String, inputRules: String, rules: String, query: String } +type alias Flags = + { renderRules : String + , inputRules : String + , rules : String + , query : String + , inputModes : Json.Decode.Value + } type Msg = SetProgram String | SetRenderProgram String | SetQuery String | SetTab Tab - | SetEditMode EditMode + | SetInputMode Int | SetResultMode ResultMode +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 + , exactString "syntax" Syntax + , 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), ("Language Term", Syntax)] + 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 = + ( { program = fs.rules + , renderProgram = fs.renderRules + , inputProgram = fs.inputRules + , query = fs.query + , tab = Rendered + , inputModes = decodeInputModes fs.inputModes + , inputMode = 0 + , resultMode = Conclusion + } + , Cmd.none + ) viewSection : String -> Html Msg -> Html Msg viewSection name content = @@ -83,23 +115,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 @@ -130,6 +162,7 @@ type Error | BadProg | BadRenderProg | FailedRender + | InvalidInputMode | Silent combineTwoResults : (a -> b -> Result Error c) -> Result Error a -> Result Error b -> Result Error c @@ -151,6 +184,7 @@ errorToString err = BadProg -> "Unable to parse rules" BadRenderProg -> "Unable to parse rendering rules" FailedRender -> "Unable to render terms using provided rendering rules" + InvalidInputMode -> "Invalid edit mode specified" Silent -> "" viewError : Error -> Html Msg @@ -170,6 +204,13 @@ 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 -> String -> Result Error (Term Metavariable) proofGoal editMode inputProgs querys = if querys == "" @@ -196,6 +237,7 @@ proofGoal editMode inputProgs querys = _ -> Err NoConversionResults (_, Nothing) -> Err BadObjectTerm (Nothing, _) -> Err BadInputProg + Custom _ -> Err BadInputProg progAndRenderProg : String -> String -> Result Error (RuleEnv, RuleEnv) progAndRenderProg progs renderProgs = @@ -227,13 +269,15 @@ 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.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 [] <| - [ viewEditModeSelector m.editMode [(Query, "Query"), (Syntax, "Language Term")] + [ viewInputModeSelector m.inputMode <| + List.map (\(a, b) -> (b, a)) m.inputModes , Html.input [ type_ "text", onInput SetQuery, value m.query ] [] ] ++ viewIfError termOrErr @@ -258,7 +302,7 @@ update msg m = SetRenderProgram prog -> ({ m | renderProgram = prog }, Cmd.none) SetQuery query -> ({ m | query = query }, Cmd.none) SetTab tab -> ({ m | tab = tab }, Cmd.none) - SetEditMode mode -> ({ m | editMode = mode }, Cmd.none) + SetInputMode mode -> ({ m | inputMode = mode }, Cmd.none) SetResultMode mode -> ({ m | resultMode = mode }, Cmd.none) subscriptions : Model -> Sub Msg