diff --git a/index.html b/index.html
index e3afda7..ded285c 100644
--- a/index.html
+++ b/index.html
@@ -79,9 +79,9 @@ input[type="text"] {
objectLang.ports.parsedString.subscribe(({ string, term }) => {
if (term !== null) {
const query = `type(empty, ${term}, ?tau)`;
- app.ports.receiveConverted.send({ input: string, query });
+ app.ports.receiveConverted.send({ input: string, result: { query } });
} else {
- app.ports.receiveConverted.send({ input: string, query: null });
+ app.ports.receiveConverted.send({ input: string, result: { error: "Unable to parse object language term" } });
}
});
diff --git a/src/Main.elm b/src/Main.elm
index d981790..3dc383a 100644
--- a/src/Main.elm
+++ b/src/Main.elm
@@ -40,7 +40,7 @@ type ResultMode
type DesugaringState
= Requested
| Succeeded String
- | Failed
+ | Failed String
resultModeEq : ResultMode -> ResultMode -> Bool
resultModeEq rm1 rm2 =
@@ -80,9 +80,20 @@ type Msg
| SetTab Tab
| SetInputMode Int
| SetResultMode ResultMode
- | SetDesugaredQuery { input: String, query: Maybe String }
+ | SetDesugaredQuery { input: String, result: Json.Decode.Value }
-decodeInputModes: Json.Decode.Value -> List (String, EditMode)
+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 =
@@ -105,7 +116,7 @@ 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 : Maybe String } -> msg) -> Sub msg
+port receiveConverted : ({ input : String, result : Json.Decode.Value } -> msg) -> Sub msg
requestDesugaring : Int -> List (String, EditMode) -> String -> Cmd Msg
requestDesugaring inputMode inputModes input =
@@ -123,7 +134,7 @@ init fs =
( { program = fs.rules
, renderProgram = fs.renderRules
, input = fs.input
- , desugaredQuery = Failed
+ , desugaredQuery = Requested
, tab = Rendered
, inputModes = inputModes
, inputMode = 0
@@ -184,12 +195,11 @@ viewRules renderProgs progs =
type Error
= BadQuery
- | BadObjectTerm
| NoConversionResults
| BadInputProg
| BadProg
| BadRenderProg
- | FailedRender
+ | FailedRender String
| InvalidInputMode
| Silent
@@ -206,12 +216,11 @@ 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 -> ""
@@ -256,7 +265,7 @@ proofGoal editMode input desugaredQuery =
case run topLevelTerm querys of
Nothing -> Err BadQuery
Just query -> Ok query
- Failed -> Err BadObjectTerm
+ Failed s -> Err (FailedRender s)
progAndRenderProg : String -> String -> Result Error (RuleEnv, RuleEnv)
progAndRenderProg progs renderProgs =
@@ -333,9 +342,9 @@ update msg m =
({ m | desugaredQuery =
if m.input == data.input
then
- case data.query of
- Just q -> Succeeded q
- Nothing -> Failed
+ case decodeRenderResult data.result of
+ Ok q -> Succeeded q
+ Err e -> Failed e
else m.desugaredQuery
}
, Cmd.none