Add syntax for holes, track spans, improve errors

lib/eff/Doctor.ml

@@ -0,0 +1,82 @@
+open Prelude
+
+type _ Effect.t +=
+  | Survivable : Diagnostic.t -> unit Effect.t
+  | Fatal : Diagnostic.t -> 'a Effect.t
+
+type env =
+  { lexbuf : Lexing.lexbuf;
+    span   : Span.t option
+  }
+
+module Reader = Algaeff.Reader.Make (struct type nonrec env = env end)
+
+let run lexbuf k =
+  Reader.run ~env:{ lexbuf; span = None } k
+
+let locate span k =
+  Reader.scope (fun env -> { env with span = span }) k
+
+let with_cause k =
+  let env = Reader.read () in
+  let cause =
+    env.span
+    |> Option.map @@ fun span ->
+    Diagnostic.cause
+      ~filename:(Span.filename span)
+      ~row:(Span.start_row span)
+      ~column:(Span.start_column span)
+  in k cause
+
+let with_note ?note cause =
+  let env = Reader.read () in
+  match note, cause, env.span with
+  | Some note, Some cause, Some span ->
+    let size = (span.stop.pos_cnum - span.start.pos_bol) in
+    let buff = Bytes.create size in
+    Bytes.blit env.lexbuf.lex_buffer span.start.pos_bol buff 0 size; 
+    let source_code = Bytes.to_string buff in
+    Option.some @@
+    Diagnostic.with_note
+      ~source_code
+      ~row:(Span.start_row span)
+      ~start_col:(Span.start_column span)
+      ~end_col:(Span.stop_column span)
+      ~msg:note
+      cause
+  | _ -> None
+
+
+let info ?note ~code msg =
+  let diag =
+    with_cause @@ fun cause ->
+    Diagnostic.error ?cause:(with_note ?note cause) ~code msg
+  in Effect.perform (Survivable diag)
+
+let warning ?note ~code msg =
+  let diag =
+    with_cause @@ fun cause ->
+    Diagnostic.error ?cause:(with_note ?note cause) ~code msg
+  in Effect.perform (Survivable diag)
+
+let error ?note ~code msg =
+  let diag =
+    with_cause @@ fun cause ->
+    Diagnostic.error ?cause:(with_note ?note cause) ~code msg
+  in Effect.perform (Fatal diag)
+
+let impossible ?note msg =
+  let callstack =
+    Format.asprintf "Callstack:@.%s@." @@ 
+    Printexc.raw_backtrace_to_string @@
+    Printexc.get_callstack 1000
+  in
+  let diag =
+    with_cause @@ fun cause ->
+    let cause =
+      cause
+      |> with_note ?note
+      |> Option.map (Diagnostic.help callstack)
+    in 
+    Diagnostic.impossible ?cause:(with_note ?note cause) ~code:"XXXXX" msg
+  in Effect.perform (Fatal diag)

lib/eff/Doctor.mli

@@ -0,0 +1,13 @@
+open Prelude
+
+type _ Effect.t +=
+  | Survivable : Diagnostic.t -> unit Effect.t
+  | Fatal : Diagnostic.t -> 'a Effect.t
+
+val run : Lexing.lexbuf -> (unit -> 'a) -> 'a
+val locate : Span.t option -> (unit -> 'a) -> 'a
+
+val info : ?note:string -> code:string -> string -> unit
+val warning : ?note:string -> code:string -> string -> unit
+val error : ?note:string -> code:string -> string -> 'a
+val impossible : ?note:string -> string -> 'a

lib/elaborator/Refiner.ml

@@ -1,4 +1,5 @@
 open Prelude
+open Eff
 
 module Ctx = OrderedHashTbl.Make(Ident)
 
@@ -76,74 +77,70 @@ open struct
   module Error =
   struct
     let type_error expected actual =
-      let msg = Format.asprintf "Expected '%a' = '%a'@."
+      let msg = "Type Error" in
+      let note = Format.asprintf "Expected '%a' = '%a'@."
           (D.pp_tp Pp.init) expected
           (D.pp_tp Pp.init) actual
-      in
-      let diag = Diagnostic.error ~code:"E0004" msg in
-      raise @@ Diagnostic.Fatal diag
+      in Doctor.error ~note ~code:"E0004" msg
 
     let staging_mismatch expected actual =
-      let msg =
+      let msg = "Staging Mismatch" in
+      let note =
         Format.asprintf "Expected staging level '%d' but got '%d'"
           expected
           actual
-      in
-      let diag = Diagnostic.error ~code:"E0005" msg in
-      raise @@ Diagnostic.Fatal diag
+      in Doctor.error ~note ~code:"E0005" msg
 
     let staging_not_inferrable tp =
-      let msg =
+      let msg = "Inference failure" in
+      let note =
         Format.asprintf "Could not infer staging level of type '%a'"
           CS.dump tp
-      in
-      let diag = Diagnostic.error ~code:"E0006" msg in
-      raise @@ Diagnostic.Fatal diag
+      in Doctor.error ~note ~code:"E0006" msg
 
     let expected_connective conn actual =
-      let msg =
+      let msg = "Connective Mismatch" in
+      let note =
         Format.asprintf "Expected a %s but got '%a'"
           conn
           (D.pp_tp Pp.init) actual
-      in
-      let diag = Diagnostic.error ~code:"E0007" msg in
-      raise @@ Diagnostic.Fatal diag
+      in Doctor.error ~note ~code:"E0007" msg
 
     let cant_stage_zero () =
-      let msg =
+      let msg = "Staging Error" in
+      let note =
         Format.asprintf "Tried to quote an expression to level 0."
-      in
-      let diag = Diagnostic.error ~code:"E0008" msg in
-      raise @@ Diagnostic.Fatal diag
+      in Doctor.error ~note ~code:"E0008" msg
 
     let type_not_inferrable tp =
-      let msg =
+      let msg = "Inference Error" in
+      let note =
         Format.asprintf "Could not infer type of '%a'"
           CS.dump tp
-      in
-      let diag = Diagnostic.error ~code:"E0009" msg in
-      raise @@ Diagnostic.Fatal diag
+      in Doctor.error ~note ~code:"E0009" msg
   end
 
   (** {1 Elaborating Types} *)
 
   let rec check_tp (tm : CS.t) ~(stage : int) : S.tp =
-    match tm with
+    Doctor.locate tm.info @@ fun () ->
+    match tm.node with
     | CS.Pi (base, name, fam) ->
       let base = check_tp ~stage base in
       let vbase = eval_tp ~stage base in
       let fam = bind_var name stage vbase @@ fun _ ->
         check_tp fam ~stage
       in S.Pi (base, name, fam)
-    | tm ->
+    | _ ->
       let (tp, inferred_stage) = infer_tp tm in
       if stage = inferred_stage then
         tp
       else
         Error.staging_mismatch stage inferred_stage
 
   and infer_tp (tm : CS.t) : (S.tp * int) =
-    match tm with
+    Doctor.locate tm.info @@ fun () ->
+    match tm.node with
     | CS.Pi (base, ident, fam) ->
       let base, base_stage = infer_tp base in
       let vbase = eval_tp ~stage:base_stage base in
@@ -160,14 +157,19 @@ open struct
 
   (** {1 Elaborating Terms} *)
   and check (tm : CS.t) ~(stage : int) (tp : D.tp) : S.t =
-    match tm, tp with
-    | CS.Lam ([], body), tp ->
-      check body ~stage tp
-    | CS.Lam (name :: names, body), D.Pi (base, _, fam) ->
-      bind_var name stage base @@ fun arg ->
-      let fib = inst_tp_clo ~stage fam arg in
-      let body = check (CS.Lam (names, body)) ~stage fib in
-      S.Lam(name, body)
+    Doctor.locate tm.info @@ fun () ->
+    match tm.node, tp with
+    | CS.Lam (names, body), D.Pi (base, _, fam) ->
+      let rec check_lams names tp =
+        match names with
+        | [] -> check ~stage body tp
+        | name :: names ->
+          bind_var name stage base @@ fun arg ->
+          let fib = inst_tp_clo ~stage fam arg in
+          let body = check_lams names fib in
+          S.Lam(name, body)
+      in
+      check_lams names tp
     | CS.Pi (base, x, fam), D.Univ stage ->
       let base = check base ~stage (D.Univ stage) in
       let base_tp = NbE.do_el ~stage @@ eval ~stage base in
@@ -186,9 +188,9 @@ open struct
       | NbE.NotConvertible ->
         Error.type_error tp tp'
 
-  (* [TODO: Reed M, 02/05/2022] Should I return the stage here? *)
   and infer (tm : CS.t) : S.t * int * D.tp =
-    match tm with
+    Doctor.locate tm.info @@ fun () ->
+    match tm.node with
     | CS.Var nm ->
       begin
         match resolve_local nm with

lib/elaborator/Syntax.ml

@@ -1,26 +1,40 @@
 open Prelude
 
-(* [TODO: Reed M, 02/05/2022] Update to use cells *)
-type t =
+type info = Span.t option
+
+type 'a node =
+  {node : 'a;
+   info : info}
+
+type t = t_ node
+and t_ =
   | Ann of { tm : t; tp : t }
   | Var of Ident.path 
+  | Hole of string option
+
   | Pi of t * Ident.t * t
   | Lam of Ident.t list * t
   | Ap of t * t list
+
+
   | Expr of t
   | Quote of t
   | Splice of t
+
   | Univ of { stage : int }
 
-let rec dump fmt =
-  function
+let rec dump fmt tm =
+  match tm.node with
   | Ann {tm; tp} ->
     Format.fprintf fmt "ann[%a, %a]"
       dump tm
       dump tp
   | Var ident ->
     Format.fprintf fmt "var[%a]"
       Ident.pp_path ident
+  | Hole nm ->
+    Format.fprintf fmt "hole[%a]"
+      (Format.pp_print_option Format.pp_print_string) nm
   | Pi (base, ident, fam) ->
     Format.fprintf fmt "pi[%a, %a, %a]"
       Ident.pp ident

lib/frontend/Execute.ml

@@ -1,7 +1,9 @@
 open Prelude
+open Core
+open Eff
+
 open Command
 open Elaborator
-open Core
 
 
 module CS = Elaborator.Syntax
@@ -101,7 +103,7 @@ let exec_command : command -> status =
         Diagnostic.error ~code:"E0003" @@
         Format.asprintf "Expected failure '%s'." message
       with
-      | Diagnostic.Fatal diag ->
+      | [%effect? Doctor.Fatal diag, _] ->
         Diagnostic.pp Format.std_formatter @@
         Diagnostic.info ~code:"I0003" @@
         Format.asprintf "Encountered expected failure@.@[<v 2>%a@]"
@@ -151,12 +153,17 @@ let rec exec : command list -> unit =
 
 let load input =
   match Loader.load input with
-  | Ok cmds ->
+  | Ok (cmds, lexbuf) ->
     begin
       try
+        Doctor.run lexbuf @@ fun () ->
         Namespace.run @@ fun () ->
         exec cmds
-      with Diagnostic.Fatal diag ->
-        Diagnostic.pp Format.err_formatter diag
+      with
+      | [%effect? Doctor.Fatal diag, _] ->
+        Diagnostic.pp Format.err_formatter diag;
+      | [%effect? Doctor.Survivable diag, k] ->
+        Diagnostic.pp Format.std_formatter diag;
+        Effect.Deep.continue k ()
     end
   | Error diagnostic -> Diagnostic.pp Format.err_formatter diagnostic