diff --git a/README.org b/README.org index 691e73f..24a4a96 100644 --- a/README.org +++ b/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]]. diff --git a/docs/error-codes.org b/docs/error-codes.org index a7cae2b..2920d17 100644 --- a/docs/error-codes.org +++ b/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. diff --git a/examples/demo.stt b/examples/demo.stt index d6fddf7..e82d225 100644 --- a/examples/demo.stt +++ b/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 diff --git a/lib/core/Data.ml b/lib/core/Data.ml index 3403fd5..49d68c7 100644 --- a/lib/core/Data.ml +++ b/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 diff --git a/lib/core/Domain.ml b/lib/core/Domain.ml index c3450d0..eb5a569 100644 --- a/lib/core/Domain.ml +++ b/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 -> diff --git a/lib/core/Domain.mli b/lib/core/Domain.mli index 8b7278d..d6150e8 100644 --- a/lib/core/Domain.mli +++ b/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} *) diff --git a/lib/core/Inner.ml b/lib/core/Inner.ml index 98aa391..b22376b 100644 --- a/lib/core/Inner.ml +++ b/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 diff --git a/lib/core/Inner.mli b/lib/core/Inner.mli index df89a53..05f69df 100644 --- a/lib/core/Inner.mli +++ b/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 diff --git a/lib/core/Syntax.ml b/lib/core/Syntax.ml index 7ea487d..86d7e99 100644 --- a/lib/core/Syntax.ml +++ b/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 diff --git a/lib/core/Syntax.mli b/lib/core/Syntax.mli index e219593..cbc4079 100644 --- a/lib/core/Syntax.mli +++ b/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 diff --git a/lib/eff/Doctor.ml b/lib/eff/Doctor.ml new file mode 100644 index 0000000..5f88404 --- /dev/null +++ b/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 + diff --git a/lib/eff/Doctor.mli b/lib/eff/Doctor.mli new file mode 100644 index 0000000..210678c --- /dev/null +++ b/lib/eff/Doctor.mli @@ -0,0 +1,17 @@ +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 diagnostic : Diagnostic.t -> unit +val fatal : Diagnostic.t -> '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 + diff --git a/lib/eff/Staging.ml b/lib/eff/Staging.ml index f74f0c8..ddaa148 100644 --- a/lib/eff/Staging.ml +++ b/lib/eff/Staging.ml @@ -1,5 +1,3 @@ -open Prelude - type mode = | Inner | Outer diff --git a/lib/elaborator/Refiner.ml b/lib/elaborator/Refiner.ml index 30b6389..aa200ae 100644 --- a/lib/elaborator/Refiner.ml +++ b/lib/elaborator/Refiner.ml @@ -1,4 +1,5 @@ open Prelude +open Eff module Ctx = OrderedHashTbl.Make(Ident) @@ -19,12 +20,15 @@ open struct type env = { names : cell Ctx.t; - values : D.env } + values : D.env; + has_holes : bool; + strict_mode : bool + } - let create_env size = + let create_env ?(strict_mode = false) size = let names = Ctx.create size in let values = D.Env.empty in - { names; values } + { names; values; strict_mode; has_holes = false } module Eff = Algaeff.Reader.Make (struct type nonrec env = env end) @@ -76,66 +80,93 @@ 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 = - Format.asprintf "Tried to quote an expression to level 0." - in - let diag = Diagnostic.error ~code:"E0008" msg in - raise @@ Diagnostic.Fatal diag + let msg = "Staging Error" in + let note = + Format.asprintf "Tried to go below stage 0." + 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 Type Holes} *) + let hole ~stage nm tp = + let tp = quote_tp tp in + let env = Eff.read () in + if env.strict_mode then + let msg = "Encountered Hole in Strict Mode." in + let note = + Format.asprintf "Encountered a hole of type '%a'" + S.dump_tp tp + in Doctor.error ~note ~code:"E0010" msg + else if stage <> 0 then + let msg = "Encountered Hole in a metaprogram." in + let note = + Format.asprintf "Encountered a hole of type '%a' while in stage %d" + S.dump_tp tp + stage + in Doctor.error ~note ~code:"E0011" msg + else + let msg = "Type Hole" in + let note = + Format.asprintf "Encountered a hole of type '%a'" + S.dump_tp tp + in + Doctor.warning ~note ~code:"W0002" msg; + S.Hole nm + + let check_stage ~expected ~actual = + if expected = actual then + () + else + Error.staging_mismatch expected actual + (** {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 @@ -143,7 +174,8 @@ open struct 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 @@ -158,37 +190,122 @@ open struct | _ -> Error.staging_not_inferrable tm + and check_code_pi ~stage base x fam = + let base = check base ~stage (D.Univ stage) in + let base_tp = NbE.do_el ~stage @@ eval ~stage base in + let fam = bind_var x stage base_tp @@ fun _ -> + check fam ~stage (D.Univ stage) + in + S.CodePi (base, S.Lam (x, fam)) + + and check_code_expr ~stage tm = + if stage <> 0 then + let tm = check ~stage:(stage - 1) tm (D.Univ (stage - 1)) in + S.CodeExpr tm + else + Error.cant_stage_zero () + + and check_args stage tp tms = + match tp, tms with + | tp, [] -> [], tp + | (D.Pi (base, _, fam)), (tm :: tms) -> + let tm = check tm ~stage base in + let vtm = eval ~stage tm in + let fib = inst_tp_clo ~stage fam vtm in + let tms, ret = check_args stage fib tms in + (tm :: tms, ret) + | _ -> + Error.expected_connective "a pi type" tp + (** {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) - | 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 - let fam = bind_var x stage base_tp @@ fun _ -> - check fam ~stage (D.Univ stage) + 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 - S.CodePi (base, S.Lam (x, fam)) + check_lams names tp + | CS.Pi (base, x, fam), D.Univ _ -> + check_code_pi ~stage base x fam + | CS.Expr tm, D.Univ _ -> + check_code_expr ~stage tm | CS.Quote tm, D.Expr tp -> if stage > 0 then S.Quote (check tm ~stage:(stage - 1) tp) else Error.cant_stage_zero () + | CS.Hole nm, tp -> + hole ~stage nm tp | _ -> let tm', _, tp' = infer tm in try NbE.equate_tp ~size:0 tp tp'; tm' with | NbE.NotConvertible -> Error.type_error tp tp' - (* [TODO: Reed M, 02/05/2022] Should I return the stage here? *) + and infer_with_stage ~(stage : int) (tm : CS.t) : S.t * D.tp = + Doctor.locate tm.info @@ fun () -> + match tm.node with + | CS.Ann {tm;tp} -> + let tp = check_tp ~stage tp in + let vtp = eval_tp ~stage tp in + check ~stage tm vtp, vtp + | CS.Var nm -> + begin + match resolve_local nm with + | Some ix -> + let cell = get_local ix in + check_stage ~expected:stage ~actual:cell.stage; + S.Local ix, cell.tp + | None -> + let (gbl, stage, tp) = resolve_global nm in + check_stage ~expected:stage ~actual:stage; + S.Global gbl, tp + end + | CS.Hole _ -> + Error.type_not_inferrable tm + | CS.Pi (base, x, fam) -> + let tm = check_code_pi ~stage base x fam in + tm, D.Univ stage + | CS.Lam (_, _) -> + Error.type_not_inferrable tm + | CS.Ap (t, ts) -> + let f_tm, f_tp = infer_with_stage ~stage t in + let tms, tp = check_args stage f_tp ts in + S.apps f_tm tms, tp + | CS.Expr t -> + check_code_expr ~stage t, D.Univ stage + | CS.Quote t -> + if stage <> 0 then + let tm, tp = infer_with_stage ~stage:(stage - 1) t in + S.Quote tm, D.Expr tp + else + Error.cant_stage_zero () + | CS.Splice t -> + let tm, tp = infer_with_stage ~stage:(stage + 1) t in + begin + match tp with + | D.Expr tp -> + S.Splice tm, tp + | _ -> + Error.expected_connective "an expression type" tp + end + | CS.Univ {stage = ustage} -> + if stage = ustage then + S.CodeUniv stage, D.Univ stage + else + Error.staging_mismatch stage ustage + + 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 @@ -200,18 +317,6 @@ open struct S.Global gbl, stage, tp end | CS.Ap (t, ts) -> - let rec check_args stage tp tms = - match tp, tms with - | tp, [] -> [], tp - | (D.Pi (base, _, fam)), (tm :: tms) -> - let tm = check tm ~stage base in - let vtm = eval ~stage tm in - let fib = inst_tp_clo ~stage fam vtm in - let tms, ret = check_args stage fib tms in - (tm :: tms, ret) - | _ -> - Error.expected_connective "a pi type" tp - in let f_tm, f_stage, f_tp = infer t in let tms, tp = check_args f_stage f_tp ts in S.apps f_tm tms, f_stage, tp @@ -248,6 +353,11 @@ let check tm ~stage tp = let env = create_env 128 in Eff.run ~env @@ fun () -> check tm ~stage tp +let infer_with_stage ~stage tm = + let env = create_env 128 in + Eff.run ~env @@ fun () -> infer_with_stage ~stage tm + let infer tm = let env = create_env 128 in Eff.run ~env @@ fun () -> infer tm + diff --git a/lib/elaborator/Refiner.mli b/lib/elaborator/Refiner.mli index 7dceffa..d30e7a0 100644 --- a/lib/elaborator/Refiner.mli +++ b/lib/elaborator/Refiner.mli @@ -1,5 +1,3 @@ -open Prelude - module S := Core.Syntax module D := Core.Domain module O := Core.Outer @@ -16,4 +14,5 @@ val check_tp : CS.t -> stage:int -> S.tp val infer_tp : CS.t -> S.tp * int val check : CS.t -> stage:int -> D.tp -> S.t +val infer_with_stage : stage:int -> CS.t -> S.t * D.tp val infer : CS.t -> S.t * int * D.tp diff --git a/lib/elaborator/Syntax.ml b/lib/elaborator/Syntax.ml index 4730eeb..39bcb94 100644 --- a/lib/elaborator/Syntax.ml +++ b/lib/elaborator/Syntax.ml @@ -1,19 +1,30 @@ 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 @@ -21,6 +32,9 @@ let rec dump fmt = | 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 diff --git a/lib/frontend/Command.ml b/lib/frontend/Command.ml index 1cc8225..85f6e5f 100644 --- a/lib/frontend/Command.ml +++ b/lib/frontend/Command.ml @@ -2,7 +2,8 @@ open Prelude module CS = Elaborator.Syntax type command = - | Declare of { ident : Ident.t; tp : CS.t option; tm : CS.t } + | Def of { ident : Ident.t; tp : CS.t option; tm : CS.t } + | DefStaged of { ident : Ident.t; tp : CS.t option; tm : CS.t } | Fail of { message : string; tp : CS.t option; tm : CS.t } | Normalize of { tm : CS.t } | Stage of Ident.path diff --git a/lib/frontend/Execute.ml b/lib/frontend/Execute.ml index 69d9d88..c41fd36 100644 --- a/lib/frontend/Execute.ml +++ b/lib/frontend/Execute.ml @@ -1,7 +1,9 @@ open Prelude +open Core +open Eff + open Command open Elaborator -open Core module CS = Elaborator.Syntax @@ -41,14 +43,31 @@ let not_implemented string = Diagnostic.pp Format.err_formatter diag; Continue +let expected_staged () = + let message = Format.asprintf "The 'def!' construct requires the term to be of stage > 0, but it wasn't." in + let diag = Diagnostic.warning ~code:"E0012" message in + Diagnostic.pp Format.err_formatter diag + let elab tp tm = match tp with | Some tp -> - Debug.print "Elaborating type %a@." CS.dump tp; + Debug.print ~file:"Execute.ml" "Elaborating type %a@." CS.dump tp; + let tp = Refiner.check_tp ~stage:0 tp in + Debug.print ~file:"Execute.ml" "Evaluating type %a@." S.dump_tp tp; + let vtp = NbE.eval_tp ~stage:0 ~env:D.Env.empty tp in + Debug.print ~file:"Execute.ml" "Checking term %a@." CS.dump tm; + let tm = Refiner.check tm ~stage:0 vtp in + (tm, vtp) + | None -> + Refiner.infer_with_stage ~stage:0 tm + +let elab_staged tp tm = + match tp with + | Some tp -> let (tp, stage) = Refiner.infer_tp tp in - Debug.print "Evaluating type %a@." S.dump_tp tp; + Debug.print ~file:"Execute.ml" "Evaluating type %a@." S.dump_tp tp; let vtp = NbE.eval_tp ~stage ~env:D.Env.empty tp in - Debug.print "Checking term %a@." CS.dump tm; + Debug.print ~file:"Execute.ml" "Checking term %a@." CS.dump tm; let tm = Refiner.check tm ~stage vtp in (tm, stage, vtp) | None -> @@ -68,40 +87,39 @@ let resolve_inner path = let exec_command : command -> status = function - | Declare {ident = User path; tp; tm} -> - let (tm, stage, vtp) = elab tp tm in - let vtm = - lazy begin - NbE.eval ~stage ~env:D.Env.empty tm - end in - let itm = - lazy begin - Stage.eval_inner ~stage tm - end - in - let expand = - Stage.eval_outer ~stage tm - in - let gbl : S.global = - if stage = 0 then - `Unstaged (path, vtm, itm) - else - `Staged (path, vtm, itm, expand) - in - Namespace.define path gbl stage vtp; + | Def {ident = User path; tp; tm} -> + let (tm, vtp) = elab tp tm in + let vtm = lazy (NbE.eval ~stage:0 ~env:D.Env.empty tm) in + let itm = lazy (Stage.eval_inner ~stage:0 tm) in + Namespace.define path (`Unstaged (path, vtm, itm)) 0 vtp; + Continue + | Def {ident = Anon; tp; tm} -> + let _ = elab tp tm in Continue - | Declare {ident = Anon; tp; tm} -> - let (_, _, _) = elab tp tm in + | DefStaged { ident = User path; tp; tm } -> + let (tm, stage, vtp) = elab_staged tp tm in + let vtm = lazy (NbE.eval ~stage ~env:D.Env.empty tm) in + let itm = lazy (Stage.eval_inner ~stage tm) in + let otm = Stage.eval_outer ~stage tm in + if stage = 0 then + expected_staged () + else + Namespace.define path (`Staged (path, vtm, itm, otm)) 0 vtp; + Continue + | DefStaged { ident = Anon; tp; tm } -> + let (_, stage, _) = elab_staged tp tm in + if stage = 0 then + expected_staged (); Continue | Fail {message; tp; tm} -> begin try - let (_, _, _) = elab tp tm in + let _ = elab tp tm in Diagnostic.pp Format.err_formatter @@ 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@.@[%a@]" @@ -151,12 +169,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 diff --git a/lib/frontend/Grammar.mly b/lib/frontend/Grammar.mly index bda246b..7944403 100644 --- a/lib/frontend/Grammar.mly +++ b/lib/frontend/Grammar.mly @@ -3,16 +3,20 @@ open Prelude open Command open CS +let locate (start, stop) node = + {node; info = Some {start; stop}} + let ap_or_atomic = function | [] -> failwith "Impossible Internal Error" - | [f] -> f + | [f] -> f.node | f :: args -> Ap (f, args) %} %token NUMERAL %token ATOM +%token HOLE %token FLAG %token COLON COLON_COLON COLON_EQUALS RIGHT_ARROW UNDERSCORE (* Symbols *) @@ -22,14 +26,17 @@ let ap_or_atomic = (* Keywords *) %token TYPE THE (* Commands *) -%token DEF NORMALIZE STAGE PRINT FAIL DEBUG QUIT +%token DEF DEF_BANG NORMALIZE STAGE PRINT FAIL DEBUG QUIT %token EOF %start commands %type - arrow atomic_term term +%type + plain_arrow + plain_atomic_term + plain_term %type path %type @@ -39,6 +46,17 @@ let ap_or_atomic = %% +%inline +located(X): + | e = X + { locate $loc e } + +term: t = located(plain_term) + { t } + +atomic_term: t = located(plain_atomic_term) + { t } + path: | path = separated_nonempty_list(COLON_COLON, ATOM) { path } @@ -57,9 +75,11 @@ commands: command: | DEF; ident = name; COLON; tp = term; COLON_EQUALS tm = term - { Declare {ident; tp = Some tp; tm} } - | FAIL; ident = name; tp = term; COLON_EQUALS tm = term - { Declare {ident; tp = Some tp; tm} } + { Def {ident; tp = Some tp; tm} } + | DEF_BANG; ident = name; COLON; tp = term; COLON_EQUALS tm = term + { DefStaged {ident; tp = Some tp; tm} } + | FAIL; message = ATOM; tp = term; COLON_EQUALS tm = term + { Fail {message; tp = Some tp; tm} } | NORMALIZE; tm = term; { Normalize {tm} } | STAGE; path = path @@ -71,13 +91,13 @@ command: | QUIT { Quit } -term: +plain_term: | tms = nonempty_list(atomic_term) { ap_or_atomic tms } - | tm = arrow + | tm = plain_arrow { tm } -arrow: +plain_arrow: | LAMBDA; nms = list(name); RIGHT_ARROW; tm = term { Lam (nms, tm) } | LPR; ident = name; COLON; base = term; RPR; RIGHT_ARROW; fam = term @@ -85,8 +105,8 @@ arrow: | base = term; RIGHT_ARROW; fam = term { Pi (base, Anon, fam) } -atomic_term: - | LPR; tm = term; RPR +plain_atomic_term: + | LPR; tm = plain_term; RPR { tm } | DOUBLE_UP_LSQ; tm = term; RSQ { Expr tm } @@ -96,6 +116,8 @@ atomic_term: { Splice tm } | path = path { Var path } + | name = HOLE + { Hole name } | TYPE; stage = NUMERAL { Univ { stage } } | THE; tp = atomic_term; tm = atomic_term diff --git a/lib/frontend/Lex.mll b/lib/frontend/Lex.mll index 830e740..4423575 100644 --- a/lib/frontend/Lex.mll +++ b/lib/frontend/Lex.mll @@ -1,4 +1,6 @@ { +open Prelude +open Span open Lexing open Grammar @@ -30,15 +32,12 @@ let commands = let keywords = make_table 0 [ ("def", DEF); + ("def!", DEF_BANG); ("type", TYPE); ("the", THE) ] (* Some Lexing Utilities *) -type span = - {start : position; - stop : position} - let last_token lexbuf = let tok = lexeme lexbuf in if tok = "" then None else Some tok @@ -60,8 +59,12 @@ let atom_initial = let atom_subsequent = [^ '(' ')' '[' ']' '{' '}' '<' '>' '.' '#' '\\' '@' '*' '^' ':' ',' ';' '|' '=' '"' ' ' '\t' '\n' '\r'] + let atom = atom_initial atom_subsequent* +let hole = '?' atom_subsequent* + + let number = ['0'-'9']+ @@ -129,6 +132,18 @@ and real_token = parse | tok -> tok | exception Not_found -> Printf.eprintf "Unknown Command: %s\n" (lexeme lexbuf); token lexbuf } + | "?" + { HOLE None } + | hole + { + let str = lexeme lexbuf in + let len = String.length str in + if len = 1 then + HOLE None + else + let hole_name = String.sub str 1 (String.length str - 1) in + HOLE (Some hole_name) + } | atom { (* [TODO: Reed M, 02/05/2022] Actually disallow subscripts *) diff --git a/lib/frontend/Loader.ml b/lib/frontend/Loader.ml index ef763a1..92ee9ba 100644 --- a/lib/frontend/Loader.ml +++ b/lib/frontend/Loader.ml @@ -1,6 +1,6 @@ open Prelude -let error_cause (span : Lex.span) ~note = +let error_cause (span : Span.t) ~note = let filename = span.start.pos_fname in let row = span.start.pos_lnum in let column = span.start.pos_cnum - span.start.pos_bol in @@ -17,7 +17,7 @@ let error_cause (span : Lex.span) ~note = In_channel.input_line chan in Diagnostic.cause ~filename ~row ~column - |> Diagnostic.note ~source_code ~row ~start_col:column ~end_col ~note + |> Diagnostic.with_note ~source_code ~row ~start_col:column ~end_col ~msg:note let lex_error token span = Diagnostic.error @@ -55,3 +55,4 @@ let load input = let cmds = try_parse Grammar.commands lexbuf in close_in chan; cmds + |> Result.map @@ fun cmds -> (cmds, lexbuf) diff --git a/lib/frontend/Loader.mli b/lib/frontend/Loader.mli index 920d11b..bc6f292 100644 --- a/lib/frontend/Loader.mli +++ b/lib/frontend/Loader.mli @@ -1,4 +1,4 @@ open Prelude open Command -val load : [`Stdin | `File of string] -> (command list, Diagnostic.t) result +val load : [`Stdin | `File of string] -> (command list * Lexing.lexbuf, Diagnostic.t) result diff --git a/lib/frontend/Namespace.ml b/lib/frontend/Namespace.ml index 36b4723..a7e17be 100644 --- a/lib/frontend/Namespace.ml +++ b/lib/frontend/Namespace.ml @@ -1,7 +1,8 @@ open Algaeff.StdlibShim +open Yuujinchou open Prelude -open Yuujinchou +open Eff open Elaborator module S = Core.Syntax @@ -26,9 +27,9 @@ let run f = match NS.resolve path with | Some data -> continue k data | None -> - let msg = Format.asprintf "Identifier '%a' is not in scope." Ident.pp_path path in - let diag = Diagnostic.error ~code:"E0001" msg - in discontinue k @@ Diagnostic.Fatal diag + let msg = "Scope Error" in + let note = Format.asprintf "Identifier '%a' is not in scope." Ident.pp_path path in + Doctor.error ~note ~code:"E0001" msg in try handle_resolve_global () with | [%effect? NS.Act.BindingNotFound _, k] -> continue k () diff --git a/lib/frontend/dune b/lib/frontend/dune index 2b39eca..d3134d5 100644 --- a/lib/frontend/dune +++ b/lib/frontend/dune @@ -1,5 +1,5 @@ (menhir - (flags --strict --explain --table) + (flags --strict --explain --table --unused-tokens) (modules Grammar)) (ocamllex Lex) diff --git a/lib/nbe/Eval.ml b/lib/nbe/Eval.ml index 5f1cda4..74770f4 100644 --- a/lib/nbe/Eval.ml +++ b/lib/nbe/Eval.ml @@ -38,6 +38,8 @@ open struct D.global path v inner | S.Global (`Staged (path, v, inner, _)) -> D.global path v inner + | S.Hole nm -> + D.hole nm | S.Lam (x, body) -> D.Lam (x, clo body) | S.Ap (f, a) -> @@ -48,6 +50,8 @@ open struct do_splice (eval t) | S.CodePi (base, fam) -> D.Code (D.CodePi (eval base, eval fam)) + | S.CodeExpr tm -> + D.Code (D.CodeExpr (eval tm)) | S.CodeUniv stage -> D.Code (D.CodeUniv stage) @@ -110,6 +114,8 @@ open struct Graft.value fam @@ fun fam -> Graft.build @@ TB.pi (TB.el base) @@ fun x -> TB.el (TB.ap fam x) + | D.CodeExpr tm -> + D.Expr (do_el tm) | D.CodeUniv stage -> D.Univ stage (** {1 Closure Instantiation} *) diff --git a/lib/nbe/Quote.ml b/lib/nbe/Quote.ml index 0aed9ce..0aae9d9 100644 --- a/lib/nbe/Quote.ml +++ b/lib/nbe/Quote.ml @@ -45,6 +45,8 @@ and quote_code : D.code -> S.t = function | D.CodePi (base, fam) -> S.CodePi (quote base, quote fam) + | D.CodeExpr tm -> + S.CodeExpr (quote tm) | D.CodeUniv stage -> S.CodeUniv stage @@ -59,6 +61,7 @@ and quote_hd : D.hd -> S.t = function | D.Local lvl -> S.Local (Quoting.level_to_index lvl) | D.Global gbl -> S.Global (gbl :> S.global) + | D.Hole nm -> S.Hole nm and quote_spine (tm : S.t) : D.frm list -> S.t = function diff --git a/lib/prelude/Debug.ml b/lib/prelude/Debug.ml index a060c16..3f499a0 100644 --- a/lib/prelude/Debug.ml +++ b/lib/prelude/Debug.ml @@ -21,6 +21,6 @@ let debug_formatter = let flush () = Stdlib.flush Stdlib.stderr in Format.make_formatter out flush -let print (fmt : ('a, Format.formatter, unit) format) = - Format.fprintf debug_formatter "[DEBUG] "; +let print ~file (fmt : ('a, Format.formatter, unit) format) = + Format.fprintf debug_formatter "DEBUG[%s] " file; Format.fprintf debug_formatter fmt diff --git a/lib/prelude/Debug.mli b/lib/prelude/Debug.mli index b966df4..06171b0 100644 --- a/lib/prelude/Debug.mli +++ b/lib/prelude/Debug.mli @@ -1,4 +1,4 @@ val dump_callstack : ?depth:int -> string -> unit val debug_mode : bool -> unit val is_debug_mode : unit -> bool -val print : ('a, Format.formatter, unit) format -> 'a +val print : file:string -> ('a, Format.formatter, unit) format -> 'a diff --git a/lib/prelude/Diagnostic.ml b/lib/prelude/Diagnostic.ml index adc3ffc..978b90d 100644 --- a/lib/prelude/Diagnostic.ml +++ b/lib/prelude/Diagnostic.ml @@ -12,7 +12,7 @@ type note = row : int; start_col : int; end_col : int; - note : string } + msg : string } | HelpNote of string type cause = @@ -27,24 +27,28 @@ type t = message : string; cause : cause option; } -exception Fatal of t - -let fatal diag = - (* [TODO: Reed M, 11/05/2022] Remove this frame from the callstack *) - raise (Fatal diag) +let severity diag = + diag.severity let cause ~filename ~row ~column = { filename; row; column; notes = Emp } -let note ~source_code ?row ?(start_col = 0) ?end_col ~note cause = +let note ~source_code ~row ?(start_col = 0) ?end_col msg = let end_col = Option.value end_col ~default:(String.length source_code) in + SourceNote { source_code; row; start_col; end_col; msg } + +let add_note note cause = + { cause with notes = Snoc(cause.notes, note) } + +let with_note ~source_code ?row ?start_col ?end_col ~msg cause = let row = Option.value row ~default:cause.row in - { cause with notes = Snoc(cause.notes, SourceNote { source_code; row; start_col; end_col; note }) } + add_note (note ~source_code ~row ?start_col ?end_col msg) cause let help str cause = { cause with notes = Snoc(cause.notes, HelpNote str) } + let info ?cause ~code message = { code; severity = Info; message; cause } @@ -66,7 +70,7 @@ let pp_severity fmt = let pp_note fmt = function - | SourceNote {source_code; row; start_col; end_col; note} -> + | SourceNote {source_code; row; start_col; end_col; msg} -> let row_digits = 1 + (int_of_float @@ Float.log10 (float_of_int row)) in (* NOTE: The formatting here is complicated enough that it warrants using the Format.pp_print family of functions *) @@ -84,7 +88,7 @@ let pp_note fmt = Format.pp_print_string fmt (String.make start_col ' '); Format.pp_print_string fmt (String.make (end_col - start_col) '^'); Format.pp_print_char fmt ' '; - Format.pp_print_string fmt note + Format.pp_print_string fmt msg | HelpNote help -> (* [TODO: Reed M, 02/05/2022] When we have the nicer alignment, update this *) Format.fprintf fmt "Help:@. @[@ %s]" help diff --git a/lib/prelude/Diagnostic.mli b/lib/prelude/Diagnostic.mli index 531aaac..d95596c 100644 --- a/lib/prelude/Diagnostic.mli +++ b/lib/prelude/Diagnostic.mli @@ -1,18 +1,25 @@ -type note +type severity = + | Info + | Warning + | Error + | Impossible +type note type cause type t val cause : filename:string -> row:int -> column:int -> cause -val note : source_code:string -> ?row:int -> ?start_col:int -> ?end_col:int -> note:string -> cause -> cause +val note : source_code:string -> row:int -> ?start_col:int -> ?end_col:int -> string -> note + +val with_note : source_code:string -> ?row:int -> ?start_col:int -> ?end_col:int -> msg:string -> cause -> cause val help : string -> cause -> cause +val add_note : note -> cause -> cause val info : ?cause:cause -> code:string -> string -> t val warning : ?cause:cause -> code:string -> string -> t val error : ?cause:cause -> code:string -> string -> t val impossible : ?cause:cause -> code:string -> string -> t -val pp : Format.formatter -> t -> unit +val severity : t -> severity -exception Fatal of t -val fatal : t -> 'a +val pp : Format.formatter -> t -> unit diff --git a/lib/prelude/Prelude.ml b/lib/prelude/Prelude.ml index f28c002..352e3ef 100644 --- a/lib/prelude/Prelude.ml +++ b/lib/prelude/Prelude.ml @@ -4,3 +4,4 @@ module Ident = Ident module Diagnostic = Diagnostic module OrderedHashTbl = OrderedHashTbl module Debug = Debug +module Span = Span diff --git a/lib/prelude/Span.ml b/lib/prelude/Span.ml new file mode 100644 index 0000000..dd83ba5 --- /dev/null +++ b/lib/prelude/Span.ml @@ -0,0 +1,20 @@ +open Lexing + +type t = + { start : position; + stop : position } + +let filename span = + span.start.pos_fname + +let start_row span = + span.start.pos_lnum + +let start_column span = + span.start.pos_cnum - span.start.pos_bol + +let stop_column span = + span.stop.pos_cnum - span.stop.pos_bol + +let span_size span = + span.stop.pos_cnum - span.start.pos_cnum diff --git a/lib/stage/Eval.ml b/lib/stage/Eval.ml index 62b887b..63513c1 100644 --- a/lib/stage/Eval.ml +++ b/lib/stage/Eval.ml @@ -1,4 +1,3 @@ -open Prelude open Core open Eff @@ -14,11 +13,6 @@ open struct module Reader = Algaeff.Reader.Make (struct type nonrec env = env end) - let impossible msg = - Format.asprintf msg - |> Diagnostic.impossible ~code:"XSTAGE" - |> Diagnostic.fatal - let get_locals () = (Reader.read()).locals @@ -27,14 +21,14 @@ open struct match O.Env.lookup_lvl env ix with | O.Outer otm -> otm | O.Inner _ -> - impossible "Expected an outer variable in 'get_outer_local'" + Doctor.impossible "Expected an outer variable in 'get_outer_local'" let get_inner_local ix = let env = get_locals () in match O.Env.lookup_lvl env ix with | O.Inner itm -> itm | O.Outer _ -> - impossible "Expected an inner variable in 'get_inner_local'" + Doctor.impossible "Expected an inner variable in 'get_inner_local'" let incr_stage k = let stage = (Reader.read ()).stage in @@ -55,7 +49,7 @@ open struct let expand_outer_global (gbl : S.global) = match gbl with | `Unstaged _ -> - impossible "Encountered a global variable of stage 0 when evaluating outer syntax." + Doctor.impossible "Encountered a global variable of stage 0 when evaluating outer syntax." | `Staged (_, _, _, expand) -> let stage = (Reader.read ()).stage in expand stage @@ -73,6 +67,8 @@ open struct get_outer_local ix | S.Global gbl -> expand_outer_global gbl + | S.Hole _ -> + Doctor.impossible "Cannot have holes in metaprograms!" | S.Lam (x, body) -> O.Lam (x, clo body) | S.Ap (f, a) -> @@ -88,6 +84,8 @@ open struct incr_stage @@ fun _ -> eval_outer tm | S.CodePi _ -> O.Irrelevant + | S.CodeExpr _ -> + O.Irrelevant | S.CodeUniv _ -> O.Irrelevant @@ -97,6 +95,8 @@ open struct get_inner_local ix | S.Global gbl -> I.Global gbl + | S.Hole nm -> + I.Hole nm | S.Lam (x, body) -> I.Lam (x, bind_inner @@ fun () -> eval_inner body) | S.Ap (fn, a) -> @@ -112,18 +112,20 @@ open struct end | S.CodePi (base, fam) -> I.CodePi (eval_inner base, eval_inner fam) + | S.CodeExpr tm -> + I.CodeExpr (eval_inner tm) | S.CodeUniv stage -> I.CodeUniv stage and do_outer_ap fn a = match fn with | O.Lam (_, clo) -> inst_tm_clo clo a | _ -> - impossible "Expected a function in do_outer_ap" + Doctor.impossible "Expected a function in do_outer_ap" and do_splice (otm : O.t) = match otm with | O.Quote tm -> tm - | _ -> impossible "Expected a quoted inner value in do_splice" + | _ -> Doctor.impossible "Expected a quoted inner value in do_splice" and inst_tm_clo clo v = match clo with @@ -133,9 +135,7 @@ open struct end let eval_inner tm = - Debug.print "Evaluating Inner@."; let stage = Staging.get_stage () in - Debug.print "Handled Stage Effect!@."; let env = { locals = O.Env.empty; stage } in Reader.run ~env @@ fun () -> eval_inner tm diff --git a/lib/stage/Quote.ml b/lib/stage/Quote.ml index 522604d..984e78f 100644 --- a/lib/stage/Quote.ml +++ b/lib/stage/Quote.ml @@ -11,6 +11,8 @@ let rec quote_inner tm = S.Local (Quoting.level_to_index lvl) | I.Global gbl -> S.Global gbl + | I.Hole nm -> + S.Hole nm | I.Lam (x, body) -> S.Lam (x, Quoting.bind_var @@ fun _ -> quote_inner body) | I.Ap (fn, arg) -> @@ -21,5 +23,7 @@ let rec quote_inner tm = S.Splice (quote_inner tm) | I.CodePi (base, fam) -> S.CodePi (quote_inner base, quote_inner fam) + | I.CodeExpr tm -> + S.CodeExpr (quote_inner tm) | I.CodeUniv stage -> S.CodeUniv stage diff --git a/lib/unfold/Unfold.ml b/lib/unfold/Unfold.ml index 892720d..e26aca9 100644 --- a/lib/unfold/Unfold.ml +++ b/lib/unfold/Unfold.ml @@ -57,6 +57,8 @@ open struct match code with | D.CodePi (base, fam) -> D.CodePi (unfold base, unfold fam) + | D.CodeExpr tm -> + D.CodeExpr (unfold tm) | D.CodeUniv i -> D.CodeUniv i @@ -78,6 +80,8 @@ open struct | `Unstaged (_, _, syn) -> Lazy.force syn | `Staged (_, _, syn, _) -> Lazy.force syn end + | I.Hole nm -> + I.Hole nm | I.Lam (x, body) -> I.Lam (x, unfold_inner body) | I.Ap (fn, arg) -> @@ -88,6 +92,8 @@ open struct I.Splice (unfold_inner tm) | I.CodePi (base, fam) -> I.CodePi (unfold_inner base, unfold_inner fam) + | I.CodeExpr tm -> + I.CodeExpr (unfold_inner tm) | I.CodeUniv stage -> I.CodeUniv stage end