disentangle refiner errors from elaborator errors

src/core/ElabBasics.ml

@@ -13,7 +13,7 @@ open Monad.Notation (Monads.ElabM)
 
 let refine_err err =
   let* env = read in
-  throw @@ Err.ElabError (err, Env.location env)
+  throw @@ Err.RefineError (err, Env.location env)
 
 let resolve id =
   let* env = read in

src/core/RefineError.ml

@@ -1,4 +1,3 @@
-module CS = ConcreteSyntax
 module D = Domain
 module S = Syntax
 open Basis
@@ -54,24 +53,6 @@ let pp fmt =
       "Head connective mismatch, expected %a but got %a"
       pp_connective conn
       (S.pp_tp ppenv) tp
-  | ExpectedSynthesizableTerm orig ->
-    Format.fprintf fmt
-      "@[Type annotation required for@,@[<hv> %a@]@]"
-      CS.pp_con_ orig
-  | InvalidTypeExpression cs ->
-    Fmt.fprintf fmt
-      "Invalid type expression: %a"
-      CS.pp_con cs
-  | MalformedCase ->
-    Fmt.fprintf fmt "Malformed case"
-  | CannotEliminate (ppenv, tp) ->
-    Fmt.fprintf fmt
-      "Cannot eliminate element of type %a"
-      (S.pp_tp ppenv) tp
-  | ExpectedSimpleInductive (ppenv, tp) ->
-    Fmt.fprintf fmt
-      "Expected simple inductive type but found %a"
-      (S.pp_tp ppenv) tp
   | ExpectedDimensionLiteral n ->
     Fmt.fprintf fmt
       "Expected dimension literal 0 or 1, but got %i" n
@@ -87,12 +68,12 @@ let pp fmt =
       (S.pp_tp ppenv) tp
 
 
-exception ElabError of t * LexingUtil.span option
+exception RefineError of t * LexingUtil.span option
 
 let _ =
   PpExn.install_printer @@ fun fmt ->
   function
-  | ElabError (err, _loc) ->
+  | RefineError (err, _loc) ->
     pp fmt err
   | _ ->
     raise PpExn.Unrecognized

src/core/RefineError.mli

@@ -3,4 +3,4 @@ open Basis
 include module type of RefineErrorData.Data
 val pp : Format.formatter -> t -> unit
 
-exception ElabError of t * LexingUtil.span option
+exception RefineError of t * LexingUtil.span option

src/core/RefineErrorData.ml

@@ -1,4 +1,3 @@
-module CS = ConcreteSyntax
 module S = Syntax
 module D = Domain
 open Basis
@@ -24,15 +23,9 @@ struct
     | UnboundVariable of Ident.t
     | ExpectedEqual of Pp.env * S.tp * S.t * S.t * Conversion.Error.t
     | ExpectedEqualTypes of Pp.env * S.tp * S.tp * Conversion.Error.t
-    | InvalidTypeExpression of CS.con
     | ExpectedConnective of connective * Pp.env * S.tp
-    | ExpectedSynthesizableTerm of CS.con_
-    | MalformedCase
-    | CannotEliminate of Pp.env * S.tp
-    | ExpectedSimpleInductive of Pp.env * S.tp
     | ExpectedDimensionLiteral of int
     | ExpectedTrue of Pp.env * S.t
     | VirtualType
     | HoleNotPermitted of Pp.env * S.tp
-
 end

src/frontend/Driver.ml

@@ -59,7 +59,7 @@ let execute_decl : CS.decl -> [`Continue | `Quit] EM.m =
         let+ () = EM.emit ident.info pp_message @@ (OutputMessage (Definition {ident = ident.node; tp; tm})) in
         `Continue
       | _ ->
-        EM.throw @@ Err.ElabError (Err.UnboundVariable ident.node, ident.info)
+        EM.throw @@ Err.RefineError (Err.UnboundVariable ident.node, ident.info)
     end
   | CS.Quit ->
     EM.ret `Quit
@@ -70,7 +70,7 @@ let protect m =
   EM.trap m |>> function
   | Ok return ->
     EM.ret @@ Ok return
-  | Error (Err.ElabError (err, info)) ->
+  | Error (Err.RefineError (err, info)) ->
     let+ () = EM.emit ~lvl:`Error info RefineError.pp err in
     Error ()
   | Error exn ->

src/frontend/ElabError.ml

@@ -0,0 +1,44 @@
+open Basis
+open Core
+
+module CS = ConcreteSyntax
+module S = Syntax
+
+type t =
+  | MalformedCase
+  | InvalidTypeExpression of CS.con
+  | ExpectedSynthesizableTerm of CS.con_
+  | CannotEliminate of Pp.env * S.tp
+  | ExpectedSimpleInductive of Pp.env * S.tp
+
+
+let pp fmt =
+  function
+  | ExpectedSynthesizableTerm orig ->
+    Format.fprintf fmt
+      "@[Type annotation required for@,@[<hv> %a@]@]"
+      CS.pp_con_ orig
+  | InvalidTypeExpression cs ->
+    Format.fprintf fmt
+      "Invalid type expression: %a"
+      CS.pp_con cs
+  | MalformedCase ->
+    Format.fprintf fmt "Malformed case"
+  | CannotEliminate (ppenv, tp) ->
+    Format.fprintf fmt
+      "Cannot eliminate element of type %a"
+      (S.pp_tp ppenv) tp
+  | ExpectedSimpleInductive (ppenv, tp) ->
+    Format.fprintf fmt
+      "Expected simple inductive type but found %a"
+      (S.pp_tp ppenv) tp
+
+exception ElabError of t * LexingUtil.span option
+
+let _ =
+  PpExn.install_printer @@ fun fmt ->
+  function
+  | ElabError (err, _loc) ->
+    pp fmt err
+  | _ ->
+    raise PpExn.Unrecognized

src/frontend/ElabError.mli

@@ -0,0 +1,15 @@
+open Basis 
+open Core
+module CS := ConcreteSyntax
+module S := Syntax
+
+type t =
+  | MalformedCase
+  | InvalidTypeExpression of CS.con
+  | ExpectedSynthesizableTerm of CS.con_
+  | CannotEliminate of Pp.env * S.tp
+  | ExpectedSimpleInductive of Pp.env * S.tp
+
+val pp : Format.formatter -> t -> unit
+
+exception ElabError of t * LexingUtil.span option

src/frontend/Elaborator.ml

@@ -26,7 +26,7 @@ let rec unfold idents k =
     | _ ->
       let* env = EM.read in
       let span = Env.location env in
-      EM.throw @@ Err.ElabError (Err.UnboundVariable ident, span)
+      EM.throw @@ Err.RefineError (Err.UnboundVariable ident, span)
 
 module CoolTp :
 sig
@@ -356,7 +356,7 @@ and syn_tm : CS.con -> T.Syn.tac =
       R.Univ.com (chk_tm fam) (chk_tm src) (chk_tm trg) (chk_tm cof) (chk_tm tm)
     | _ ->
       T.Syn.rule @@
-      EM.throw @@ Err.ElabError (Err.ExpectedSynthesizableTerm con.node, con.info)
+      EM.throw @@ ElabError.ElabError (ElabError.ExpectedSynthesizableTerm con.node, con.info)
 
 and chk_cases cases =
   List.map chk_case cases

src/frontend/Tactics.ml

@@ -6,11 +6,15 @@ module D = Domain
 module S = Syntax
 module R = Refiner
 module CS = ConcreteSyntax
-module Err = RefineError
 module Sem = Semantics
 
 open Monad.Notation (EM)
 
+let elab_err err =
+  let* env = EM.read in
+  EM.throw @@ ElabError.ElabError (err, ElabEnv.location env)
+
+
 let match_goal (tac : _ -> T.Chk.tac EM.m) : T.Chk.tac =
   T.Chk.brule @@
   fun goal ->
@@ -78,7 +82,7 @@ struct
       let* tac_zero : T.Chk.tac =
         match find_case "zero" cases with
         | Some ([], tac) -> EM.ret tac
-        | Some _ -> EM.refine_err Err.MalformedCase
+        | Some _ -> elab_err ElabError.MalformedCase
         | None -> EM.ret @@ R.Hole.unleash_hole @@ Some "zero"
       in
       let* tac_suc =
@@ -87,29 +91,29 @@ struct
           EM.ret @@ R.Pi.intro ~ident:nm_z @@ fun _ -> R.Pi.intro @@ fun _ -> tac
         | Some ([`Inductive (nm_z, nm_ih)], tac) ->
           EM.ret @@ R.Pi.intro ~ident:nm_z @@ fun _ -> R.Pi.intro ~ident:nm_ih @@ fun _ -> tac
-        | Some _ -> EM.refine_err Err.MalformedCase
+        | Some _ -> elab_err ElabError.MalformedCase
         | None -> EM.ret @@ R.Hole.unleash_hole @@ Some "suc"
       in
       T.Syn.run @@ R.Nat.elim mot tac_zero tac_suc scrut
     | D.Circle, mot ->
       let* tac_base : T.Chk.tac =
         match find_case "base" cases with
         | Some ([], tac) -> EM.ret tac
-        | Some _ -> EM.refine_err Err.MalformedCase
+        | Some _ -> elab_err ElabError.MalformedCase
         | None -> EM.ret @@ R.Hole.unleash_hole @@ Some "base"
       in
       let* tac_loop =
         match find_case "loop" cases with
         | Some ([`Simple nm_x], tac) ->
           EM.ret @@ R.Pi.intro ~ident:nm_x @@ fun _ -> tac
-        | Some _ -> EM.refine_err Err.MalformedCase
+        | Some _ -> elab_err ElabError.MalformedCase
         | None -> EM.ret @@ R.Hole.unleash_hole @@ Some "loop"
       in
       T.Syn.run @@ R.Circle.elim mot tac_base tac_loop scrut
     | _ ->
       EM.with_pp @@ fun ppenv ->
       let* tp = EM.quote_tp ind_tp in
-      EM.refine_err @@ Err.CannotEliminate (ppenv, tp)
+      elab_err @@ ElabError.CannotEliminate (ppenv, tp)
 
   let assert_simple_inductive =
     function
@@ -120,7 +124,7 @@ struct
     | tp ->
       EM.with_pp @@ fun ppenv ->
       let* tp = EM.quote_tp tp in
-      EM.refine_err @@ Err.ExpectedSimpleInductive (ppenv, tp)
+      elab_err @@ ElabError.ExpectedSimpleInductive (ppenv, tp)
 
   let lam_elim cases : T.Chk.tac =
     match_goal @@ fun (tp, _, _) ->