🕳️ ⛳ Type Holes

README.org

@@ -67,7 +67,7 @@ may have different requirements, but the process should be similar.
 
 First, we will need to add some pins for some merlin deps.
 #+BEGIN_SRC shell
-  opam switch add dot-merlin-reader git+https://github.com/ocaml/merlin#500
+  opam pin add dot-merlin-reader git+https://github.com/ocaml/merlin#500
 #+END_SRC
 
 
@@ -76,6 +76,12 @@ Then, we can install merlin as per usual.
 #+BEGIN_SRC shell
   opam install merlin 
 #+END_SRC
+
+We should also install [[https://github.com/OCamlPro/ocp-indent][ocp-indent]], which is our preferred code
+formatter for the codebase.
+#+BEGIN_SRC shell
+  opam install ocp-indent
+#+END_SRC
 * References
 This work is inspired by some of the work by András Kovács, namely
 [[https://github.com/AndrasKovacs/smalltt][smalltt]] and [[https://github.com/AndrasKovacs/staged][staged]].

docs/error-codes.org

@@ -16,9 +16,17 @@ There was a connective mismatch
 We tried to quote a value to level 0.
 ** E0009
 Couldn't infer type
+** E0010
+Encountered a type hole while in strict mode.
+** E0011
+Encountered a hole while elaborating a metaprogram.
+** E0012
+The ~def!~ construct expects a term with stage > 0.
 * Warnings 
 ** W0001
 =stagedtt= encountered a feature that is under construction.
+** W0002
+Type holes.
 * Info
 ** I0001
 =stagedtt= encountered a ~#print~ directive.

examples/demo.stt

@@ -1,10 +1,10 @@
 def id : type 0 -> type 0 := (\ x → x)
 
 def wow : type 0 := ↓[ the (⇑[ type 0 ]) ↑[ (the (type 0 → type 0) (λ x → x)) type 0 ] ]
-def hmmm : ⇑[ type 0 ] := ↑[ type 0 → wow ]
+def! hmmm : ⇑[ type 0 ] := ↑[ type 0 → wow ]
 def test : type 0 := ↓[ hmmm ]
 
-#debug on
+def test_hole : type 0 := ?
 
 #stage test
 #print test

lib/core/Data.ml

@@ -13,6 +13,7 @@ type global =
 and syntax =
   | Local of int
   | Global of global
+  | Hole of string option
 
   | Lam of Ident.t * syntax
   | Ap of syntax * syntax
@@ -22,6 +23,7 @@ and syntax =
 
   | CodePi of syntax * syntax
   | CodeUniv of int
+  | CodeExpr of syntax
 
 and syntax_tp =
   | TpVar of int
@@ -43,6 +45,7 @@ and value =
 and code =
   | CodePi of value * value
   | CodeUniv of int
+  | CodeExpr of value
 
 and value_tp =
   | Pi of value_tp * Ident.t * tp_vclo
@@ -56,6 +59,7 @@ and neu = { hd : hd; spine : frm list }
 and hd =
   | Local of int
   | Global of [ `Unstaged of Ident.path * value Lazy.t * inner Lazy.t ]
+  | Hole of string option
 
 
 and frm =
@@ -84,6 +88,7 @@ and outer =
 and inner =
   | Local of int
   | Global of global
+  | Hole of string option
 
   | Lam of Ident.t * inner
   | Ap of inner * inner
@@ -93,6 +98,7 @@ and inner =
 
   | CodePi of inner * inner
   | CodeUniv of int
+  | CodeExpr of inner
 
 and staged =
   | Inner of inner

lib/core/Domain.ml

@@ -31,12 +31,14 @@ and tp = D.value_tp =
 and code = D.code = 
   | CodePi of t * t
   | CodeUniv of int
+  | CodeExpr of t
 
 and neu = D.neu = { hd : hd; spine : frm list } 
 
 and hd = D.hd = 
   | Local of int
   | Global of global
+  | Hole of string option
 
 and global =
   [ `Unstaged of Ident.path * D.value Lazy.t * D.inner Lazy.t ]
@@ -51,6 +53,9 @@ let local lvl =
 let global nm v inner =
   Neu { hd = Global (`Unstaged (nm, v, inner)); spine = [] }
 
+let hole nm =
+  Neu { hd = Hole nm; spine = [] }
+
 let push_frm (neu : neu) (frm : frm) ~(unfold : t -> t) ~(stage : D.inner -> D.inner) : neu =
   match neu.hd with
   | Global (`Unstaged (nm, v, inner)) ->
@@ -70,8 +75,6 @@ struct
   let proj = right 4
   let arrow = right 3
   (* [TODO: Reed M, 02/05/2022] Figure out these *)
-  let quote = right 3
-  let splice = right 3
   let colon = nonassoc 2
   let arrow = right 1
   let in_ = nonassoc 0
@@ -145,6 +148,9 @@ and pp_hd env fmt  =
   | Global (`Unstaged (path, _, _)) ->
     let x, _ = Pp.bind_var (User path) env in
     Format.pp_print_string fmt x
+  | Hole nm ->
+    Format.fprintf fmt "?%a"
+      (Format.pp_print_option Format.pp_print_string) nm
 
 and pp_frm env fmt =
   function
@@ -162,6 +168,9 @@ and pp_code env fmt =
       (pp env) fam
   | CodeUniv stage ->
     Format.fprintf fmt "type %d" stage
+  | CodeExpr tm ->
+    Format.fprintf fmt "⇑[ %a ]"
+      (pp env) tm
 
 let rec pp_tp env =
   Pp.parens classify_tp env @@ fun fmt ->

lib/core/Domain.mli

@@ -26,12 +26,14 @@ and tp = D.value_tp =
 and code = D.code = 
   | CodePi of t * t
   | CodeUniv of int
+  | CodeExpr of t
 
 and neu = D.neu = { hd : hd; spine : frm list } 
 
 and hd = D.hd = 
   | Local of int
   | Global of global
+  | Hole of string option
 
 and global =
   [ `Unstaged of Ident.path * D.value Lazy.t * D.inner Lazy.t ]
@@ -43,6 +45,7 @@ and frm = D.frm =
 
 val local : int -> t
 val global : Ident.path -> t Lazy.t -> D.inner Lazy.t -> t 
+val hole : string option -> t
 val push_frm : neu -> frm -> unfold:(t -> t) -> stage:(D.inner -> D.inner)-> neu
 
 (** {1 Pretty Printing} *)

lib/core/Inner.ml

@@ -4,6 +4,7 @@ module D = Data
 type t = D.inner =
   | Local of int
   | Global of global
+  | Hole of string option
 
   | Lam of Ident.t * t
   | Ap of t * t
@@ -13,6 +14,7 @@ type t = D.inner =
 
   | CodePi of t * t
   | CodeUniv of int
+  | CodeExpr of t
 
 and global =
   [ `Unstaged of Ident.path * D.value Lazy.t * D.inner Lazy.t

lib/core/Inner.mli

@@ -7,6 +7,7 @@ module D := Data
 type t = D.inner =
   | Local of int
   | Global of global
+  | Hole of string option
 
   | Lam of Ident.t * t
   | Ap of t * t
@@ -16,6 +17,7 @@ type t = D.inner =
 
   | CodePi of t * t
   | CodeUniv of int
+  | CodeExpr of t
 
 and global =
   [ `Unstaged of Ident.path * D.value Lazy.t * D.inner Lazy.t

lib/core/Syntax.ml

@@ -11,6 +11,7 @@ type global =
 and t = D.syntax =
   | Local of int
   | Global of global
+  | Hole of string option
 
   | Lam of Ident.t * t
   | Ap of t * t
@@ -20,6 +21,7 @@ and t = D.syntax =
 
   | CodePi of t * t
   | CodeUniv of int
+  | CodeExpr of t
 
 type tp = D.syntax_tp =
   | TpVar of int
@@ -44,8 +46,6 @@ struct
   let proj = right 4
   let arrow = right 3
   (* [TODO: Reed M, 02/05/2022] Figure out these *)
-  let quote = right 3
-  let splice = right 3
   let colon = nonassoc 2
   let arrow = right 1
   let in_ = nonassoc 0
@@ -55,12 +55,14 @@ let classify_tm =
   function
   | Local _ -> Prec.atom
   | Global _ -> Prec.atom
+  | Hole _ -> Prec.atom
   | Lam _ -> Prec.arrow
   | Ap _ -> Prec.juxtaposition
-  | Quote _ -> Prec.quote
-  | Splice _ -> Prec.splice
+  | Quote _ -> Prec.delimited
+  | Splice _ -> Prec.delimited
   | CodePi _ -> Prec.arrow
   | CodeUniv _ -> Prec.atom
+  | CodeExpr _ -> Prec.delimited
 
 let classify_tp =
   function
@@ -78,6 +80,9 @@ let rec pp env =
   | Global (`Unstaged (name, _, _))
   | Global (`Staged (name, _, _, _)) ->
     Ident.pp_path fmt name
+  |  Hole nm ->
+    Format.fprintf fmt "?%a"
+      (Format.pp_print_option Format.pp_print_string) nm
   | Lam (x, body) ->
     let x, env = Pp.bind_var x env in
     Format.fprintf fmt "λ %s → %a"
@@ -98,7 +103,11 @@ let rec pp env =
       (pp (Pp.right_of Prec.juxtaposition env)) base
       (pp (Pp.right_of Prec.juxtaposition env)) fam
   | CodeUniv stage ->
-    Format.fprintf fmt "type %d" stage
+    Format.fprintf fmt "type %d"
+      stage
+  | CodeExpr tm ->
+    Format.fprintf fmt "⇑[ %a ]"
+      (pp env) tm
 
 let rec pp_tp env =
   Pp.parens classify_tp env @@ fun fmt ->
@@ -134,6 +143,9 @@ let rec dump fmt : t -> unit =
     Format.fprintf fmt "staged[%a]"
       Ident.pp_path
       nm
+  |  Hole nm ->
+    Format.fprintf fmt "hole[%a]"
+      (Format.pp_print_option Format.pp_print_string) nm
   | Lam (_, body) ->
     Format.fprintf fmt "lam[%a]"
       dump body
@@ -154,6 +166,9 @@ let rec dump fmt : t -> unit =
   | CodeUniv stage ->
     Format.fprintf fmt "type[%d]"
       stage
+  | CodeExpr tm ->
+    Format.fprintf fmt "expr[%a]"
+      dump tm
 
 and dump_tp fmt : tp -> unit =
   function

lib/core/Syntax.mli

@@ -9,6 +9,7 @@ type global =
 and t = D.syntax =
   | Local of int
   | Global of global
+  | Hole of string option
 
   | Lam of Ident.t * t
   | Ap of t * t
@@ -18,6 +19,7 @@ and t = D.syntax =
 
   | CodePi of t * t
   | CodeUniv of int
+  | CodeExpr of t
 
 type tp = D.syntax_tp =
   | TpVar of int

lib/eff/Doctor.ml

@@ -0,0 +1,86 @@
+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 diagnostic diag =
+  Effect.perform (Survivable diag)
+
+let fatal diag =
+  Effect.perform (Fatal diag)
+
+let info ?note ~code msg =
+  with_cause @@ fun cause ->
+  Diagnostic.info ?cause:(with_note ?note cause) ~code msg
+  |> diagnostic
+
+let warning ?note ~code msg =
+  (* let diag = *)
+  with_cause @@ fun cause ->
+  Diagnostic.warning ?cause:(with_note ?note cause) ~code msg
+  |> diagnostic
+(* in Effect.perform (Survivable diag) *)
+
+let error ?note ~code msg =
+  with_cause @@ fun cause ->
+  Diagnostic.error ?cause:(with_note ?note cause) ~code msg
+  |> fatal
+
+let impossible ?note msg =
+  let callstack =
+    Format.asprintf "Callstack:@.%s@." @@ 
+    Printexc.raw_backtrace_to_string @@
+    Printexc.get_callstack 1000
+  in
+  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
+  |> fatal
+