Accumulate and report multiple errors when possible

bin/narya.ml

@@ -100,9 +100,9 @@ let rec repl terminal history buf =
         let* () = Lwt_io.flush Lwt_io.stdout in
         (* In interactive mode, we display all messages verbosely, and don't quit on fatal errors except for the Quit command. *)
         Reporter.try_with
-          ~emit:(fun d -> Terminal.display ~output:stdout d)
+          ~emit:(fun d -> Reporter.display ~output:stdout d)
           ~fatal:(fun d ->
-            Terminal.display ~output:stdout d;
+            Reporter.display ~output:stdout d;
             match d.message with
             | Quit _ -> exit 0
             | _ -> ())
@@ -153,8 +153,8 @@ let rec interact_pg () : unit =
         ~emit:(fun d ->
           match d.message with
           | Hole _ -> holes := Snoc (!holes, d.message)
-          | _ -> Terminal.display ~use_ansi:true ~output:stdout d)
-        ~fatal:(fun d -> Terminal.display ~use_ansi:true ~output:stdout d)
+          | _ -> Reporter.display ~use_ansi:true ~output:stdout d)
+        ~fatal:(fun d -> Reporter.display ~use_ansi:true ~output:stdout d)
         (fun () ->
           try
             do_command (Command.parse_single cmd);
@@ -177,8 +177,8 @@ let () =
   Mbwd.miter
     (fun [ file ] ->
       let p, src = Parser.Command.Parse.start_parse (`File file) in
-      Reporter.try_with ~emit:(Terminal.display ~output:stdout)
-        ~fatal:(Terminal.display ~output:stdout) (fun () -> Execute.batch true [] p src))
+      Reporter.try_with ~emit:(Reporter.display ~output:stdout)
+        ~fatal:(Reporter.display ~output:stdout) (fun () -> Execute.batch true [] p src))
     [ !fake_interacts ];
   if !interactive then Lwt_main.run (interact ())
   else if !proofgeneral then (

js/jsnarya.ml

@@ -26,8 +26,8 @@ let rec interact_js : string -> result =
   let buf = Buffer.create 70 in
   Sys_js.set_channel_flusher stdout (fun str -> Buffer.add_string buf str);
   Reporter.try_with
-    ~emit:(fun d -> Terminal.display ~use_ansi:true ~output:stdout d)
-    ~fatal:(fun d -> Terminal.display ~use_ansi:true ~output:stdout d)
+    ~emit:(fun d -> Reporter.display ~use_ansi:true ~output:stdout d)
+    ~fatal:(fun d -> Reporter.display ~use_ansi:true ~output:stdout d)
     (fun () -> do_command (Command.parse_single cmd));
   Out_channel.flush stdout;
   (* Now we perform the "Next" effect, which returns control to the browser until the user enters another command.  At that point execution resumes here with a return value of the next command to execute, which we then pass off to ourselves recursively. *)

lib/core/ctx.ml

@@ -39,8 +39,16 @@ module Binding : sig
   (* A known but not-yet-available value is created by delaying it, and can be made available by forcing it. *)
   val delay : t -> t
   val force : t -> unit
+
+  (* An error value raises an exception when accessed. *)
+  val error : Reporter.Code.t -> t
 end = struct
-  type state = Known of level option * normal | Unknown | Delayed of level option * normal
+  type state =
+    | Known of level option * normal
+    | Unknown
+    | Delayed of level option * normal
+    | Error of Reporter.Code.t
+
   type t = state ref
 
   let make i x = ref (Known (i, x))
@@ -49,20 +57,24 @@ end = struct
     match !b with
     | Known (i, _) -> i
     | Unknown | Delayed _ -> None
+    | Error e -> fatal e
 
   let value b =
     match !b with
     | Known (_, x) -> x
     | Unknown | Delayed _ -> fatal (Anomaly "Undetermined context variable")
+    | Error e -> fatal e
 
   let unknown () = ref Unknown
   let specify b i x = b := Known (i, x)
   let delay b = ref (Delayed (level b, value b))
+  let error e = ref (Error e)
 
   let force b =
     match !b with
     | Known _ | Unknown -> ()
     | Delayed (i, x) -> b := Known (i, x)
+    | Error e -> fatal e
 end
 
 (* Test whether all the variables in a cube of bindings are free (none are let-bound). *)

lib/core/domvars.ml

@@ -67,5 +67,6 @@ let rec ext_tel :
         | Some x -> Some x
         | None -> x' in
       let ctx, env, vars, nfs =
-        ext_tel (Ctx.cube_vis ctx x newnfs) (Ext (env, D.plus_zero m, newvars)) xs rest ac ec in
+        ext_tel (Ctx.cube_vis ctx x newnfs) (Ext (env, D.plus_zero m, Ok newvars)) xs rest ac ec
+      in
       (ctx, env, newvars :: vars, newnfs :: nfs)

lib/core/equal.ml

@@ -45,7 +45,7 @@ module Equal = struct
         (* Now we take the projections and compare them at appropriate types.  It suffices to use the fields of x when computing the types of the fields, since we proceed to check the fields for equality *in order* and thus by the time we are checking equality of any particular field of x and y, the previous fields of x and y are already known to be equal, and the type of the current field can only depend on these.  (This latter is a semantic constraint on the kinds of generalized records that can sensibly admit eta-conversion.) *)
         BwdM.miterM
           (fun [ (fld, _) ] ->
-            equal_at ctx (field_term x fld) (field_term y fld) (tyof_field x ty fld))
+            equal_at ctx (field_term x fld) (field_term y fld) (tyof_field (Ok x) ty fld))
           [ fields ]
     (* At a codatatype without eta, there are no kinetic structs, only comatches, and those are not compared componentwise, only as neutrals, since they are generative, so we don't need a clause for it. *)
     (* At a higher-dimensional version of a discrete datatype, any two terms are equal.  Note that we do not check here whether discreteness is on: that affects datatypes when they are *defined*, not when they are used. *)
@@ -264,7 +264,7 @@ module Equal = struct
           (Ext
              ( env,
                D.plus_zero (TubeOf.inst tyarg),
-               TubeOf.plus_cube (val_of_norm_tube tyarg) (CubeOf.singleton x) ))
+               Ok (TubeOf.plus_cube (val_of_norm_tube tyarg) (CubeOf.singleton x)) ))
           xs ys tys tyargs
     | _ -> fatal (Anomaly "length mismatch in equal_at_tel")
 

lib/core/global.ml

@@ -13,9 +13,9 @@ open Status
 (* Each global constant either is an axiom or has a definition (a case tree).  The latter includes canonical types.  An axiom can be either parametric, which means it is always accessible, or nonparametric, which means it is not accessible behind context locks for external parametricity.  (In the future, this should be customizable on a per-direction basis.) *)
 type definition = Axiom of [ `Parametric | `Nonparametric ] | Defined of (emp, potential) term
 
-(* Global metavariables have only a definition. *)
+(* Global metavariables have only a definition (or an error indicating that they can't be correctly accessed, such as if typechecking failed earlier). *)
 module Metamap = Meta.Map.Make (struct
-  type ('x, 'a, 'b, 's) t = ('a, 'b, 's) Metadef.t
+  type ('x, 'a, 'b, 's) t = (('a, 'b, 's) Metadef.t, Code.t) Result.t
 end)
 
 type metamap = unit Metamap.t
@@ -84,10 +84,13 @@ let find_meta m =
   | None -> (
       let data = S.get () in
       match Metamap.find_opt m data.current_metas with
-      | Some d -> d
+      | Some (Ok d) -> d
+      (* If we find an error, we immediately raise it. *)
+      | Some (Error e) -> fatal e
       | None -> (
           match Metamap.find_opt m data.metas with
-          | Some d -> d
+          | Some (Ok d) -> d
+          | Some (Error e) -> fatal e
           | None -> fatal (Anomaly "undefined metavariable")))
 
 (* Marshal and unmarshal the constants and metavariables pertaining to a single compilation unit.  We ignore the "current" data because that is only relevant during typechecking commands, whereas this comes at the end of typechecking a whole file. *)
@@ -108,7 +111,9 @@ let from_channel_unit f chan i =
     Constant.Map.from_channel_unit chan
       (Result.map (fun (tm, df) -> (Link.term f tm, link_definition f df)))
       i d.constants in
-  let metas = Metamap.from_channel_unit chan { map = (fun _ df -> Link.metadef f df) } i d.metas in
+  let metas =
+    Metamap.from_channel_unit chan { map = (fun _ df -> Result.map (Link.metadef f) df) } i d.metas
+  in
   S.set { d with constants; metas }
 
 (* Add a new constant. *)
@@ -135,17 +140,17 @@ let add_error c e =
 let add_meta m ~termctx ~ty ~tm ~energy =
   let tm = (tm :> [ `Defined of ('b, 's) term | `Axiom | `Undefined ]) in
   S.modify @@ fun d ->
-  { d with current_metas = d.current_metas |> Metamap.add m { tm; termctx; ty; energy } }
+  { d with current_metas = d.current_metas |> Metamap.add m (Ok { tm; termctx; ty; energy }) }
 
-(* Set the definition of a Global metavariable, required to already exist. *)
+(* Set the definition of a Global metavariable, required to already exist but not be defined. *)
 let set_meta m ~tm =
   S.modify @@ fun d ->
   {
     d with
     current_metas =
       d.current_metas
       |> Metamap.update m (function
-           | Some d -> Some { d with tm = `Defined tm }
+           | Some (Ok d) -> Some (Ok { d with tm = `Defined tm })
            | _ -> raise (Failure "set_meta"));
   }
 
@@ -192,23 +197,70 @@ let with_definition c df f =
       (* Note that f could change the state in other ways, so we can't just reset the whole state to d.  *)
       S.modify (fun d -> { d with constants = d.constants |> Constant.Map.add c old });
       result
+  | Some (Error _ as old) ->
+      (* If the constant is currently unusable, we just retain that state. *)
+      let result = f () in
+      S.modify (fun d -> { d with constants = d.constants |> Constant.Map.add c old });
+      result
   | _ -> fatal (Anomaly "missing definition in with_definition")
 
 (* Similarly, temporarily set the value of a global metavariable, which could be either permanent or current. *)
 let with_meta_definition m tm f =
+  let d = S.get () in
+  match Metamap.find_opt m d.metas with
+  | Some (Ok olddf) ->
+      S.set { d with metas = d.metas |> Metamap.add m (Ok (Metadef.define tm olddf)) };
+      let result = f () in
+      (* Note that f could change the state in other ways, so we can't just reset the whole state to d.  *)
+      S.modify (fun d -> { d with metas = d.metas |> Metamap.add m (Ok olddf) });
+      result
+  | Some (Error _ as old) ->
+      (* If the metavariable is currently unusable, we just retain that state. *)
+      let result = f () in
+      S.modify (fun d -> { d with metas = d.metas |> Metamap.add m old });
+      result
+  | _ -> (
+      match Metamap.find_opt m d.current_metas with
+      | Some (Ok olddf) ->
+          S.set
+            {
+              d with
+              current_metas = d.current_metas |> Metamap.add m (Ok (Metadef.define tm olddf));
+            };
+          let result = f () in
+          (* Note that f could change the state in other ways, so we can't just reset the whole state to d.  *)
+          S.modify (fun d -> { d with metas = d.metas |> Metamap.add m (Ok olddf) });
+          result
+      | _ ->
+          (* If the metavariable isn't found, that means that when we created it we didn't have a type for it.  That, in turn, means that the user doesn't have a name for it, since the metavariable is only bound to a user name in a "let rec".  So we don't need to do anything. *)
+          f ())
+
+(* Temporarily set the value of a constant to produce an error, and restore it afterwards. *)
+let without_definition c err f =
+  let d = S.get () in
+  match Constant.Map.find_opt c d.constants with
+  | Some old ->
+      S.set { d with constants = d.constants |> Constant.Map.add c (Error err) };
+      let result = f () in
+      (* Note that f could change the state in other ways, so we can't just reset the whole state to d.  *)
+      S.modify (fun d -> { d with constants = d.constants |> Constant.Map.add c old });
+      result
+  | _ -> fatal (Anomaly "missing definition in without_definition")
+
+(* Similarly, temporarily set the value of a global metavariable to produce an error. *)
+let without_meta_definition m err f =
   let d = S.get () in
   match Metamap.find_opt m d.metas with
   | Some olddf ->
-      S.set { d with metas = d.metas |> Metamap.add m (Metadef.define tm olddf) };
+      S.set { d with metas = d.metas |> Metamap.add m (Error err) };
       let result = f () in
       (* Note that f could change the state in other ways, so we can't just reset the whole state to d.  *)
       S.modify (fun d -> { d with metas = d.metas |> Metamap.add m olddf });
       result
   | _ -> (
       match Metamap.find_opt m d.current_metas with
       | Some olddf ->
-          S.set
-            { d with current_metas = d.current_metas |> Metamap.add m (Metadef.define tm olddf) };
+          S.set { d with current_metas = d.current_metas |> Metamap.add m (Error err) };
           let result = f () in
           (* Note that f could change the state in other ways, so we can't just reset the whole state to d.  *)
           S.modify (fun d -> { d with metas = d.metas |> Metamap.add m olddf });

lib/core/global.mli

@@ -39,6 +39,8 @@ val add_hole :
 val hole_exists : ('a, 'b, 's) Meta.t -> bool
 val with_definition : Constant.t -> definition -> (unit -> 'a) -> 'a
 val with_meta_definition : ('a, 'b, 's) Meta.t -> ('b, 's) term -> (unit -> 'x) -> 'x
+val without_definition : Constant.t -> Reporter.Code.t -> (unit -> 'a) -> 'a
+val without_meta_definition : ('a, 'b, 's) Meta.t -> Reporter.Code.t -> (unit -> 'x) -> 'x
 
 type data
 

lib/core/metadef.ml

@@ -6,7 +6,7 @@ open Term
 type ('a, 'b, 's) t = {
   energy : 's energy;
   tm : [ `Defined of ('b, 's) term | `Axiom | `Undefined ];
-  (* If a metavariable were "lifted" to top level with pi-types, then its type would be composed of its context and the type in that context.  We instead store them separately without doing the lifting. *)
+  (* If a metavariable were "lifted" to top level with pi-types, then its type would be the pi-type over its context of the type in that context.  We instead store them separately without doing the lifting. *)
   termctx : ('a, 'b) Termctx.t;
   ty : ('b, kinetic) term;
 }

lib/core/norm.ml

@@ -32,7 +32,7 @@ let rec take_args :
  fun env mn dargs plus ->
   match (dargs, plus) with
   | [], Zero -> env
-  | arg :: args, Suc plus -> take_args (Ext (env, mn, arg)) mn args plus
+  | arg :: args, Suc plus -> take_args (Ext (env, mn, Ok arg)) mn args plus
   | _ -> fatal (Anomaly "wrong number of arguments in argument list")
 
 (* A "view" is the aspect of a type or term that we match against to determine its behavior.  A view of a term is just another term, but in WHNF.  A view of a type is either a universe, a pi-type, another canonical type (data or codata), or a neutral.  The non-neutral sorts come with their instantiations that have been checked to have the correct dimension. *)
@@ -554,9 +554,9 @@ and field_term : type n. kinetic value -> Field.t -> kinetic value =
   let (Val v) = field x fld in
   v
 
-(* Given a term and its record type, compute the type and dimension of a field projection.  The caller can control the severity of errors, depending on whether we're typechecking (Error) or normalizing (Bug, the default). *)
-and tyof_field_withname ?severity (tm : kinetic value) (ty : kinetic value) (fld : Field.or_index) :
-    Field.t * dim_wrapped * kinetic value =
+(* Given a term and its record type, compute the type and dimension of a field projection.  The caller can control the severity of errors, depending on whether we're typechecking (Error) or normalizing (Bug, the default).  We allow the term to be an error, in case typechecking failed earlier but we are continuing on; this can nevertheless succeed (or fail in more interesting ways) if the type doesn't actually depend on that value. *)
+and tyof_field_withname ?severity (tm : (kinetic value, Code.t) Result.t) (ty : kinetic value)
+    (fld : Field.or_index) : Field.t * dim_wrapped * kinetic value =
   match view_type ?severity ty "tyof_field" with
   | Canonical (head, Codata { env; ins; fields; opacity = _; eta = _ }, tyargs) -> (
       (* The type cannot have a nonidentity degeneracy applied to it (though it can be at a higher dimension). *)
@@ -571,8 +571,12 @@ and tyof_field_withname ?severity (tm : kinetic value) (ty : kinetic value) (fld
       | Eq -> (
           (* The type of the field projection comes from the type associated to that field name in general, evaluated at the stored environment extended by the term itself and its boundaries. *)
           let env =
-            Value.Ext (env, mn, TubeOf.plus_cube (val_of_norm_tube tyargs) (CubeOf.singleton tm))
-          in
+            Value.Ext
+              ( env,
+                mn,
+                Result.map
+                  (fun tm -> TubeOf.plus_cube (val_of_norm_tube tyargs) (CubeOf.singleton tm))
+                  tm ) in
           match Field.find fields fld with
           | Some (fldname, fldty) ->
               ( fldname,
@@ -583,20 +587,22 @@ and tyof_field_withname ?severity (tm : kinetic value) (ty : kinetic value) (fld
                      {
                        map =
                          (fun _ [ arg ] ->
-                           let (Val tm) = field arg.tm fldname in
-                           let _, _, ty = tyof_field_withname arg.tm arg.ty fld in
-                           { tm; ty });
+                           let (Val subtm) = field arg.tm fldname in
+                           let _, _, ty =
+                             tyof_field_withname (Result.map (fun _ -> arg.tm) tm) arg.ty fld in
+                           { tm = subtm; ty });
                      }
                      [ TubeOf.middle (D.zero_plus m) mn tyargs ]) )
           | None -> fatal ?severity (No_such_field (`Record (phead head), fld))))
   | _ -> fatal ?severity (No_such_field (`Other, fld))
 
 and tyof_field_withdim ?severity (tm : kinetic value) (ty : kinetic value) (fld : Field.t) :
     dim_wrapped * kinetic value =
-  let _, n, ty = tyof_field_withname ?severity tm ty (`Name fld) in
+  let _, n, ty = tyof_field_withname ?severity (Ok tm) ty (`Name fld) in
   (n, ty)
 
-and tyof_field ?severity (tm : kinetic value) (ty : kinetic value) (fld : Field.t) : kinetic value =
+and tyof_field ?severity (tm : (kinetic value, Code.t) Result.t) (ty : kinetic value)
+    (fld : Field.t) : kinetic value =
   let _, _, ty = tyof_field_withname ?severity tm ty (`Name fld) in
   ty
 
@@ -749,7 +755,9 @@ and lookup_cube :
   | Ext (env, _, _), Later v -> lookup_cube env mk v op
   | LazyExt (env, _, _), Later v -> lookup_cube env mk v op
   (* Finally, when we find our variable, we decompose the accumulated operator into a strict face and degeneracy, use the face as an index lookup, and act by the degeneracy.  The forcing function is the identity if the entry is not lazy, and force_eval_term if it is lazy. *)
-  | Ext (_, nk, entry), Now -> Looked_up { act = act_value; op = op_plus op nk mk; entry }
+  | Ext (_, nk, Ok entry), Now -> Looked_up { act = act_value; op = op_plus op nk mk; entry }
+  (* Looking up a variable that's bound to an error immediately fails with that error.  (In particular, this sort of failure can't currently happen "deeper" inside a term.) *)
+  | Ext (_, _, Error e), Now -> fatal e
   | LazyExt (_, nk, entry), Now ->
       Looked_up
         { act = (fun x s -> force_eval_term (act_lazy_eval x s)); op = op_plus op nk mk; entry }