From e7d3e840b37c8dd8f716cc6617e5d0370211d9f1 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 15 Sep 2024 10:21:38 -0700
Subject: [PATCH] Allow input mode code to provide custom error messages

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 index.html   |  4 ++--
 src/Main.elm | 35 ++++++++++++++++++++++-------------
 2 files changed, 24 insertions(+), 15 deletions(-)

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