From 671bb03263e2ecdc4749781b0df88b9d208ffa0e Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Thu, 13 Jan 2022 15:01:41 -0800 Subject: [PATCH 1/5] [WIP] Define the internal theory of inductive types --- src/core/Conversion.ml | 48 +++++++ src/core/Domain.ml | 28 +++- src/core/Domain.mli | 4 +- src/core/DomainData.ml | 33 ++++- src/core/Ident.ml | 16 +-- src/core/Ident.mli | 9 +- src/core/Quote.ml | 64 ++++++++- src/core/RefineError.ml | 10 +- src/core/RefineErrorData.ml | 8 +- src/core/RefineMonad.ml | 7 + src/core/RefineMonad.mli | 5 +- src/core/Refiner.ml | 158 ++++++++++++++++++++-- src/core/Refiner.mli | 31 ++++- src/core/Semantics.ml | 83 +++++++++++- src/core/Semantics.mli | 4 +- src/core/Serialize.ml | 202 ++++++++++++++--------------- src/core/Syntax.ml | 47 ++++++- src/core/SyntaxData.ml | 22 +++- src/core/TermBuilder.ml | 13 +- src/core/TermBuilder.mli | 14 +- src/frontend/ConcreteSyntaxData.ml | 5 +- src/frontend/Elaborator.ml | 58 ++++++++- src/frontend/Grammar.mly | 8 +- src/frontend/Lex.mll | 1 + 24 files changed, 688 insertions(+), 190 deletions(-) diff --git a/src/core/Conversion.ml b/src/core/Conversion.ml index 4c248ac01..9918210f0 100644 --- a/src/core/Conversion.ml +++ b/src/core/Conversion.ml @@ -96,6 +96,13 @@ let rec equate_tp (tp0 : D.tp) (tp1 : D.tp) = let* fib1 = lift_cmp @@ inst_tp_clo fam1 x in equate_tp fib0 fib1 | D.Signature sign1, D.Signature sign2 -> equate_sign sign1 sign2 + | D.Desc, D.Desc -> + ret () + | D.Ctx, D.Ctx -> + ret () + | D.Tm (ctx0, desc0), D.Tm (ctx1, desc1) -> + let* () = equate_con D.Ctx ctx0 ctx1 in + equate_con D.Desc desc0 desc1 | D.Sub (tp0, phi0, clo0), D.Sub (tp1, phi1, clo1) -> let* () = equate_tp tp0 tp1 in let* () = equate_cof phi0 phi1 in @@ -228,6 +235,47 @@ and equate_con tp con0 con1 = equate_con fib snd0 snd1 | D.Signature sign, _, _ -> equate_struct sign con0 con1 + | _, D.DescEnd, D.DescEnd -> + ret () + | _, D.DescArg (a0, desc0), D.DescArg (a1, desc1) -> + let* () = equate_con D.Univ a0 a1 in + let* famtp = + lift_cmp @@ + Sem.splice_tp @@ + Splice.con a0 @@ fun arg -> + Splice.term @@ TB.pi (TB.el arg) (fun _ -> TB.desc) + in + equate_con famtp desc0 desc1 + | _, D.DescRec desc0, DescRec desc1 -> + equate_con D.Desc desc0 desc1 + | _, D.CtxNil, D.CtxNil -> + ret () + | _, D.CtxSnoc (ctx0, ident0, desc0), D.CtxSnoc (ctx1, ident1, desc1) when Ident.equal ident0 ident1 -> + let* () = equate_con D.Ctx ctx0 ctx1 in + equate_con D.Desc desc0 desc1 + | _, D.TmVar x, D.TmVar y when Ident.equal x y -> + ret () + | D.Tm (ctx, _), D.TmAppArg (base0, fam0, fn0, arg0), D.TmAppArg (base1, fam1, fn1, arg1) -> + let* () = equate_con D.Univ base0 base1 in + let* basetp = + lift_cmp @@ + Sem.splice_tp @@ + Splice.con base0 @@ fun base0 -> + Splice.term @@ TB.el base0 + in + let* famtp = + lift_cmp @@ + Sem.splice_tp @@ + Splice.con base0 @@ fun base0 -> + Splice.term @@ TB.pi (TB.el base0) (fun _ -> TB.desc) + in + let* () = equate_con famtp fam0 fam1 in + let* () = equate_con (D.Tm (ctx, D.DescArg (base0, fam0))) fn0 fn1 in + equate_con basetp arg0 arg1 + | D.Tm (ctx, _) ,D.TmAppRec (desc0, fn0, arg0), D.TmAppRec (desc1, fn1, arg1) -> + let* () = equate_con D.Desc desc0 desc1 in + let* () = equate_con (D.Tm (ctx, D.DescRec desc0)) fn0 fn1 in + equate_con (D.Tm (ctx, D.DescEnd)) arg0 arg1 | D.Sub (tp, _phi, _), _, _ -> let* out0 = lift_cmp @@ do_sub_out con0 in let* out1 = lift_cmp @@ do_sub_out con1 in diff --git a/src/core/Domain.ml b/src/core/Domain.ml index fa13afa35..c80ffaaff 100644 --- a/src/core/Domain.ml +++ b/src/core/Domain.ml @@ -102,7 +102,7 @@ struct | KAp (_, con) -> Format.fprintf fmt "ap[%a]" pp_con con | KFst -> Format.fprintf fmt "fst" | KSnd -> Format.fprintf fmt "snd" - | KProj lbl -> Format.fprintf fmt "proj[%a]" Ident.pp_user lbl + | KProj lbl -> Format.fprintf fmt "proj[%a]" Ident.pp lbl | KNatElim _ -> Format.fprintf fmt "" | KCircleElim _ -> Format.fprintf fmt "" | KElOut -> Uuseg_string.pp_utf_8 fmt "⭝ₑₗ" @@ -156,7 +156,23 @@ struct Format.fprintf fmt "pair[%a,%a]" pp_con con0 pp_con con1 | Struct fields -> Format.fprintf fmt "struct[%a]" - (Pp.pp_sep_list (fun fmt (lbl, tp) -> Format.fprintf fmt "%a : %a" Ident.pp_user lbl pp_con tp)) fields + (Pp.pp_sep_list (fun fmt (lbl, tp) -> Format.fprintf fmt "%a : %a" Ident.pp lbl pp_con tp)) fields + | DescEnd -> + Format.fprintf fmt "desc-end" + | DescArg (arg, desc) -> + Format.fprintf fmt "desc-arg[%a, %a]" pp_con arg pp_con desc + | DescRec desc -> + Format.fprintf fmt "desc-rec[%a]" pp_con desc + | CtxNil -> + Format.fprintf fmt "ctx-nil" + | CtxSnoc(ctx, ident, desc) -> + Format.fprintf fmt "ctx-snoc[%a, %a, %a]" pp_con ctx Ident.pp ident pp_con desc + | TmVar v -> + Format.fprintf fmt "tm-var[%a]" Ident.pp v + | TmAppArg (base, fam, f, a) -> + Format.fprintf fmt "tm-app-arg[%a, %a, %a, %a]" pp_con base pp_con fam pp_con f pp_con a + | TmAppRec (desc, f, a) -> + Format.fprintf fmt "tm-app-rec[%a, %a, %a]" pp_con desc pp_con f pp_con a | Prf -> Format.fprintf fmt "*" | Cof (Cof.Join phis) -> @@ -203,7 +219,7 @@ struct and pp_sign fmt = function - | Field (ident, tp, clo) -> Format.fprintf fmt "sig/field[%a,%a,%a]" Ident.pp_user ident pp_tp tp pp_sign_clo clo + | Field (ident, tp, clo) -> Format.fprintf fmt "sig/field[%a,%a,%a]" Ident.pp ident pp_tp tp pp_sign_clo clo | Empty -> Format.fprintf fmt "sig/empty" and pp_tp fmt = @@ -222,6 +238,12 @@ struct Format.fprintf fmt "" | TpDim -> Format.fprintf fmt "" + | Desc -> + Format.fprintf fmt "" + | Ctx -> + Format.fprintf fmt "" + | Tm (ctx, desc) -> + Format.fprintf fmt "tm[%a, %a]" pp_con ctx pp_con desc | Univ -> Format.fprintf fmt "" | Nat -> diff --git a/src/core/Domain.mli b/src/core/Domain.mli index ea53d28e0..6a74efb97 100644 --- a/src/core/Domain.mli +++ b/src/core/Domain.mli @@ -22,13 +22,13 @@ module Make : functor (Symbol : Symbol.S) -> sig val fst : con val snd : con - val proj : Ident.user -> con + val proj : Ident.t -> con val el_out : con val tm_abort : con val tp_abort : tp - val sign_lbls : sign -> Ident.user list + val sign_lbls : sign -> Ident.t list (** {1 Pretty-printers } diff --git a/src/core/DomainData.ml b/src/core/DomainData.ml index d2ce93cf0..0125e3f70 100644 --- a/src/core/DomainData.ml +++ b/src/core/DomainData.ml @@ -17,7 +17,7 @@ struct | `Sg of 'a * 'a (** Dependent sum type *) - | `Signature of (Ident.user * 'a) list + | `Signature of (Ident.t * 'a) list (** First-Class Record types *) | `Ext of int * 'a * [`Global of 'a] * 'a @@ -68,7 +68,29 @@ struct | Base | Loop of dim | Pair of con * con - | Struct of (Ident.user * con) list + | Struct of (Ident.t * con) list + + (** Descriptions. These can be thought of as the types of a simple type theory. *) + | DescEnd + (** Something of sort [□] *) + | DescArg of con * con + (** A dependent function type [(x : A) → B x], where [A] comes from the outer type theory. *) + | DescRec of con + (** A non-dependent function type [□ → B]. *) + + (** Contexts of descriptions. *) + | CtxNil + | CtxSnoc of con * Ident.t * con + + (** Formal expressions involving elements of a context. We can think of these as embedded terms + from the simple type theory of inductive types. *) + | TmVar of Ident.t + (** A variable from the context [Γ] *) + | TmAppArg of con * con * con * con + (** Application to a dependent function type [(x : A) → B x], where [A] comes from the outer type theory. *) + | TmAppRec of con * con * con + (** Application to a function type [□ → B] *) + | SubIn of con | ElIn of con @@ -108,12 +130,15 @@ struct | Pi of tp * Ident.t * tp_clo | Sg of tp * Ident.t * tp_clo | Signature of sign + | Desc + | Ctx + | Tm of con * con | Nat | Circle | TpLockedPrf of cof and sign = - | Field of Ident.user * tp * S.sign clo + | Field of Ident.t * tp * S.sign clo | Empty (** A head is a variable (e.g. {!constructor:Global}, {!constructor:Var}), or it is some kind of unstable elimination form ({!constructor:Coe}, {!constructor:UnstableCut}). The geometry of {!type:cut}, {!type:hd}, {!type:unstable_frm} enables a very direct way to re-reduce a complex cut to whnf by following the unstable nodes to the root. *) @@ -135,7 +160,7 @@ struct | KAp of tp * con | KFst | KSnd - | KProj of Ident.user + | KProj of Ident.t | KNatElim of con * con * con | KCircleElim of con * con * con diff --git a/src/core/Ident.ml b/src/core/Ident.ml index f4190fd54..028a98165 100644 --- a/src/core/Ident.ml +++ b/src/core/Ident.ml @@ -1,22 +1,14 @@ type t = [`Anon | `User of string list | `Machine of string] -type 'a some = 'a constraint 'a = [< t ] -type user = [ `User of string list ] - -let user parts = `User parts let qual_to_string = function | [] -> "(root)" | parts -> String.concat "." parts -let pp_user fmt = - function - | `User parts -> Uuseg_string.pp_utf_8 fmt (qual_to_string parts) - let pp fmt = function | `Anon -> Format.fprintf fmt "" - | `User _ as u -> pp_user fmt u + | `User parts -> Uuseg_string.pp_utf_8 fmt (qual_to_string parts) | `Machine str -> Uuseg_string.pp_utf_8 fmt str let to_string = @@ -31,11 +23,7 @@ let to_string_opt = | `Machine nm -> Some nm | `Anon -> None -let user_to_string_opt = - function - | `User [] -> None - | `User parts -> Some (String.concat "." parts) - let equal i0 i1 = match (i0, i1) with | `User p0, `User p1 -> List.equal String.equal p0 p1 + | _, _ -> false diff --git a/src/core/Ident.mli b/src/core/Ident.mli index fd1cd209f..94683b3c7 100644 --- a/src/core/Ident.mli +++ b/src/core/Ident.mli @@ -1,16 +1,9 @@ open Basis type t = [`Anon | `User of string list | `Machine of string] -type 'a some = 'a constraint 'a = [< t ] -type user = [ `User of string list ] - -val user : string list -> t val pp : t Pp.printer -val pp_user : user Pp.printer val to_string : t -> string val to_string_opt : t -> string option -val user_to_string_opt : user -> string option - -val equal : user -> user -> bool +val equal : t -> t -> bool diff --git a/src/core/Quote.ml b/src/core/Quote.ml index 1bb4a059f..1906c301c 100644 --- a/src/core/Quote.ml +++ b/src/core/Quote.ml @@ -108,6 +108,60 @@ let rec quote_con (tp : D.tp) con = let+ tfields = quote_fields sign con in S.Struct tfields + | _, D.DescEnd -> + ret S.DescEnd + + | _, D.DescArg (arg, desc) -> + let* famtp = + lift_cmp @@ + Sem.splice_tp @@ + Splice.con arg @@ fun arg -> + Splice.term @@ TB.pi (TB.el arg) (fun _ -> TB.desc) + in + let+ arg = quote_con D.Univ arg + and+ desc = quote_con famtp desc in + S.DescArg (arg, desc) + + | _, D.DescRec desc -> + let+ desc = quote_con D.Desc desc in + S.DescRec desc + + | _, D.CtxNil -> + ret S.CtxNil + + | _, D.CtxSnoc (ctx, ident, desc) -> + let+ ctx = quote_con D.Ctx ctx + and+ desc = quote_con D.Desc desc in + S.CtxSnoc (ctx, ident, desc) + + | _, D.TmVar x -> + ret @@ S.TmVar x + + | D.Tm (ctx, _), D.TmAppArg (base, fam, fn, arg) -> + let* basetp = + lift_cmp @@ + Sem.splice_tp @@ + Splice.con base @@ fun base -> + Splice.term @@ TB.el base + in + let* famtp = + lift_cmp @@ + Sem.splice_tp @@ + Splice.con base @@ fun base -> + Splice.term @@ TB.pi (TB.el base) (fun _ -> TB.desc) + in + let+ base = quote_con D.Univ base + and+ fam = quote_con famtp fam + and+ fn = quote_con (D.Tm (ctx, D.DescArg (base, fam))) fn + and+ arg = quote_con basetp arg in + S.TmAppArg (base, fam, fn, arg) + + | D.Tm (ctx, _), D.TmAppRec (desc, fn, arg) -> + let+ desc = quote_con D.Desc desc + and+ fn = quote_con (D.Tm (ctx, D.DescRec desc)) fn + and+ arg = quote_con (D.Tm (ctx, D.DescEnd)) arg in + S.TmAppRec (desc, fn, arg) + | D.Sub (tp, _phi, _clo), _ -> let+ tout = let* out = lift_cmp @@ do_sub_out con in @@ -280,7 +334,7 @@ let rec quote_con (tp : D.tp) con = Format.eprintf "bad: %a / %a@." D.pp_tp tp D.pp_con con; throw @@ QuotationError (Error.IllTypedQuotationProblem (tp, con)) -and quote_fields (sign : D.sign) con : (Ident.user * S.t) list m = +and quote_fields (sign : D.sign) con : (Ident.t * S.t) list m = match sign with | D.Field (lbl, tp, sign_clo) -> let* fcon = lift_cmp @@ do_proj con lbl in @@ -433,6 +487,14 @@ and quote_tp (tp : D.tp) = | D.Signature sign -> let+ sign = quote_sign sign in S.Signature sign + | D.Desc -> + ret S.Desc + | D.Ctx -> + ret S.Ctx + | D.Tm (ctx, desc) -> + let+ ctx = quote_con D.Ctx ctx + and+ desc = quote_con D.Desc desc in + S .Tm (ctx, desc) | D.Univ -> ret S.Univ | D.ElStable code -> diff --git a/src/core/RefineError.ml b/src/core/RefineError.ml index ca31f4ea7..355d5ca8f 100644 --- a/src/core/RefineError.ml +++ b/src/core/RefineError.ml @@ -20,6 +20,12 @@ let pp_connective fmt = Format.fprintf fmt "sg" | `Signature -> Format.fprintf fmt "sig" + | `Desc -> + Format.fprintf fmt "desc" + | `Ctx -> + Format.fprintf fmt "ctx" + | `Tm -> + Format.fprintf fmt "tm" | `Univ -> Format.fprintf fmt "univ" | `Nat -> @@ -67,9 +73,9 @@ let pp fmt = "Expected true cofibration: %a" (S.pp ppenv) cof | ExpectedField (ppenv, sign, tm, lbl) -> - Fmt.fprintf fmt "Expected (%a : sig %a) to have field %a" (S.pp ppenv) tm (S.pp_sign ppenv) sign Ident.pp_user lbl + Fmt.fprintf fmt "Expected (%a : sig %a) to have field %a" (S.pp ppenv) tm (S.pp_sign ppenv) sign Ident.pp lbl | FieldNameMismatches (expected, actual) -> - Fmt.fprintf fmt "Field names mismatch, expected [%a] but got [%a]" (Pp.pp_sep_list Ident.pp_user) expected (Pp.pp_sep_list Ident.pp_user) actual + Fmt.fprintf fmt "Field names mismatch, expected [%a] but got [%a]" (Pp.pp_sep_list Ident.pp) expected (Pp.pp_sep_list Ident.pp) actual | VirtualType -> Fmt.fprintf fmt "Virtual type (dim, cof, etc.) cannot appear in this position" | HoleNotPermitted (ppenv, tp) -> diff --git a/src/core/RefineErrorData.ml b/src/core/RefineErrorData.ml index 157a85d2f..331e0daf5 100644 --- a/src/core/RefineErrorData.ml +++ b/src/core/RefineErrorData.ml @@ -11,6 +11,9 @@ struct [ `Pi | `Sg | `Signature + | `Desc + | `Ctx + | `Tm | `Nat | `Circle | `Univ @@ -26,8 +29,9 @@ struct type t = | UnboundVariable of Ident.t - | FieldNameMismatches of Ident.user list * Ident.user list - | ExpectedField of Pp.env * S.sign * S.t * Ident.user + | NotFoundInCtx of Pp.env * S.t * Ident.t + | FieldNameMismatches of Ident.t list * Ident.t list + | ExpectedField of Pp.env * S.sign * S.t * 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 | ExpectedConnective of connective * Pp.env * S.tp diff --git a/src/core/RefineMonad.ml b/src/core/RefineMonad.ml index 71ad65880..c0d5d8dea 100644 --- a/src/core/RefineMonad.ml +++ b/src/core/RefineMonad.ml @@ -142,6 +142,13 @@ let expected_connective conn tp = let* ttp = quote_tp tp in refine_err @@ Err.ExpectedConnective (conn, ppenv, ttp) +let not_found_in_ctx ctx ident = + with_pp @@ fun ppenv -> + let* qctx = quote_con D.Ctx ctx in + refine_err @@ Err.NotFoundInCtx (ppenv, qctx, ident) + + + let expected_field sign con lbl = with_pp @@ fun ppenv -> let* tsign = quote_sign sign in diff --git a/src/core/RefineMonad.mli b/src/core/RefineMonad.mli index dd69b72eb..7ea4c26fe 100644 --- a/src/core/RefineMonad.mli +++ b/src/core/RefineMonad.mli @@ -42,5 +42,6 @@ val equate : D.tp -> D.con -> D.con -> unit m val with_pp : (Pp.env -> 'a m) -> 'a m val expected_connective : RefineError.connective -> D.tp -> 'a m -val expected_field : D.sign -> S.t -> Ident.user -> 'a m -val field_names_mismatch : expected:Ident.user list -> actual:Ident.user list -> 'a m +val not_found_in_ctx : D.con -> Ident.t -> 'a m +val expected_field : D.sign -> S.t -> Ident.t -> 'a m +val field_names_mismatch : expected:Ident.t list -> actual:Ident.t list -> 'a m diff --git a/src/core/Refiner.ml b/src/core/Refiner.ml index 87e3b556e..e203033ba 100644 --- a/src/core/Refiner.ml +++ b/src/core/Refiner.ml @@ -26,7 +26,7 @@ exception CJHM type ('a, 'b) quantifier = 'a -> Ident.t * (T.var -> 'b) -> 'b type 'a telescope = - | Bind of Ident.user * 'a * (T.var -> 'a telescope) + | Bind of Ident.t * 'a * (T.var -> 'a telescope) | Done module GlobalUtil : sig @@ -534,7 +534,7 @@ struct | Done -> RM.ret @@ S.Signature (Bwd.to_list tele) in T.Tp.rule ~name:"Signature.formation" @@ form_fields Emp tacs - let rec find_field_tac (fields : (Ident.user * T.Chk.tac) list) (lbl : Ident.user) : T.Chk.tac option = + let rec find_field_tac (fields : (Ident.t * T.Chk.tac) list) (lbl : Ident.t) : T.Chk.tac option = match fields with | (lbl', tac) :: _ when Ident.equal lbl lbl' -> Some tac @@ -544,12 +544,12 @@ struct None - let rec intro_fields phi phi_clo (sign : D.sign) (tacs : Ident.user -> T.Chk.tac option) : (Ident.user * S.t) list m = + let rec intro_fields phi phi_clo (sign : D.sign) (tacs : Ident.t -> T.Chk.tac option) : (Ident.t * S.t) list m = match sign with | D.Field (lbl, tp, sign_clo) -> let tac = match tacs lbl with | Some tac -> tac - | None -> Hole.unleash_hole (Ident.user_to_string_opt lbl) + | None -> Hole.unleash_hole (Ident.to_string_opt lbl) in let* tfield = T.Chk.brun tac (tp, phi, D.un_lam @@ D.compose (D.proj lbl) @@ D.Lam (`Anon, phi_clo)) in let* vfield = RM.lift_ev @@ Sem.eval tfield in @@ -559,7 +559,7 @@ struct | D.Empty -> RM.ret [] - let intro (tacs : Ident.user -> T.Chk.tac option) : T.Chk.tac = + let intro (tacs : Ident.t -> T.Chk.tac option) : T.Chk.tac = T.Chk.brule ~name:"Signature.intro" @@ function | (D.Signature sign, phi, phi_clo) -> @@ -567,7 +567,7 @@ struct S.Struct fields | (tp, _, _) -> RM.expected_connective `Signature tp - let proj_tp (sign : D.sign) (tstruct : S.t) (lbl : Ident.user) : D.tp m = + let proj_tp (sign : D.sign) (tstruct : S.t) (lbl : Ident.t) : D.tp m = let rec go = function | D.Field (flbl, tp, _) when Ident.equal flbl lbl -> RM.ret tp @@ -588,6 +588,140 @@ struct | _ -> RM.expected_connective `Signature tp end +module Desc = +struct + let formation : T.Tp.tac = + T.Tp.rule ~name:"Desc.formation" @@ + RM.ret S.Desc + + let desc_tac ~(name:string) (k : D.tp -> S.t RM.m) : T.Chk.tac = + T.Chk.rule ~name @@ + function + | D.Desc -> k D.Desc + | tp -> RM.expected_connective `Desc tp + + let end_ : T.Chk.tac = + desc_tac ~name:"Desc.end" @@ fun _ -> + RM.ret S.DescEnd + + let arg (arg_tac : T.Chk.tac) (fam_tac : T.Chk.tac) : T.Chk.tac = + desc_tac ~name:"Desc.arg" @@ fun desc -> + let* arg = T.Chk.run arg_tac D.Univ in + let* varg = RM.lift_ev @@ Sem.eval arg in + let* famtp = + RM.lift_cmp @@ + Sem.splice_tp @@ + Splice.con varg @@ fun arg -> + Splice.tp desc @@ fun desc -> + Splice.term @@ TB.pi (TB.el arg) (fun _ -> desc) + in + let+ fam = T.Chk.run fam_tac famtp in + S.DescArg (arg, fam) + + let rec_ (rest_tac : T.Chk.tac) : T.Chk.tac = + desc_tac ~name:"Desc.rec" @@ fun desc -> + let+ rest = T.Chk.run rest_tac desc in + S.DescRec rest +end + +module Ctx = +struct + let formation : T.Tp.tac = + T.Tp.rule ~name:"Ctx.formation" @@ + RM.ret S.Ctx + + let ctx_tac ~(name : string) (k : D.tp -> S.t RM.m) : T.Chk.tac = + T.Chk.rule ~name @@ + function + | D.Ctx -> k D.Ctx + | tp -> RM.expected_connective `Ctx tp + + let nil : T.Chk.tac = + ctx_tac ~name:"Ctx.nil" @@ fun _ -> + RM.ret S.CtxNil + + let snoc (rest_tac : T.Chk.tac) (ident : Ident.t) (desc_tac : T.Chk.tac) : T.Chk.tac = + ctx_tac ~name:"Ctx.nil" @@ fun ctx -> + let* rest = T.Chk.run rest_tac ctx in + let+ desc = T.Chk.run desc_tac D.Desc in + S.CtxSnoc (rest, ident, desc) +end + +module Tm = +struct + let formation (ctx_tac : T.Chk.tac) (desc_tac : T.Chk.tac) : T.Tp.tac = + T.Tp.rule ~name:"Tm.formation" @@ + let+ ctx = T.Chk.run ctx_tac D.Ctx + and+ desc = T.Chk.run desc_tac D.Desc in + S.Tm (ctx, desc) + + (* [TODO: Reed M, 13/01/2022] This is probably the wrong way to do this + We should internalize this to require a proof that A ∈ Γ... *) + let var (ident : Ident.t) : T.Chk.tac = + T.Chk.rule ~name:"Tm.var" @@ + function + | D.Tm (ctx, desc0) -> + begin + match Sem.ctx_lookup ctx ident with + | Some desc1 -> + let+ _ = RM.equate D.Desc desc0 desc1 in + S.TmVar ident + | None -> RM.not_found_in_ctx ctx ident + end + | tp -> RM.expected_connective `Tm tp + + (* Do I just make this whole thing chk? *) + let app (f_tac : T.Syn.tac) (arg_tac : T.Chk.tac) : T.Syn.tac = + T.Syn.rule ~name:"Tm.app_arg" @@ + let* (ftm, ftp) = T.Syn.run f_tac in + match ftp with + | D.Tm (ctx, D.DescArg (base, fam)) -> + let* qbase = RM.quote_con D.Univ base in + let* famtp = + RM.lift_cmp @@ + Sem.splice_tp @@ + Splice.con base @@ fun base -> + Splice.term @@ TB.pi (TB.el base) (fun _ -> TB.desc) + in + let* qfam = RM.quote_con famtp fam in + let* argtp = + RM.lift_cmp @@ + Sem.splice_tp @@ + Splice.con base @@ fun base -> + Splice.term @@ TB.el base + in + let* arg = T.Chk.run arg_tac argtp in + let* varg = RM.lift_ev @@ Sem.eval arg in + let+ apptp = + RM.lift_cmp @@ + Sem.splice_tp @@ + Splice.con ctx @@ fun ctx -> + Splice.con fam @@ fun fam -> + Splice.con varg @@ fun arg -> + Splice.term @@ TB.tm ctx (TB.ap fam [arg]) + in + S.TmAppArg (qbase, qfam, ftm, arg), apptp + | D.Tm (ctx, D.DescRec desc) -> + let* qdesc = RM.quote_con D.Desc desc in + let* argtp = + RM.lift_cmp @@ + Sem.splice_tp @@ + Splice.con ctx @@ fun ctx -> + Splice.term @@ TB.tm ctx TB.desc_end + in + let* arg = T.Chk.run arg_tac argtp in + let+ apptp = + RM.lift_cmp @@ + Sem.splice_tp @@ + Splice.con ctx @@ fun ctx -> + Splice.con desc @@ fun desc -> + Splice.term @@ TB.tm ctx desc + in + S.TmAppRec (qdesc, ftm, arg), apptp + (* [TODO: Reed M, 13/01/2022] Print a better error when we don't have a DescArg/DescApp index. *) + | tp -> RM.expected_connective `Tm tp +end + module Univ = struct let formation : T.Tp.tac = @@ -627,7 +761,7 @@ struct let+ fam = T.Chk.run tac_fam famtp in base, fam - let quantifiers (mk_fields : ('a Ident.some * (D.tp -> S.t m)) list) (univ : D.tp) : ('a Ident.some * S.t) list m = + let quantifiers (mk_fields : (Ident.t * (D.tp -> S.t m)) list) (univ : D.tp) : (Ident.t * S.t) list m = let (idents, ks) = List.split mk_fields in let rec mk_fams fams vfams = function @@ -646,7 +780,7 @@ struct let+ fams = mk_fams [] [] ks in List.combine idents fams - let quote_sign_codes (vsign : (Ident.user * D.con) list) (univ : D.tp) : (Ident.user * S.t) list m = + let quote_sign_codes (vsign : (Ident.t * D.con) list) (univ : D.tp) : (Ident.t * S.t) list m = quantifiers (List.map (fun (lbl, vcode) -> (lbl, fun tp -> RM.quote_con tp vcode)) vsign) univ let pi tac_base tac_fam : T.Chk.tac = @@ -677,7 +811,7 @@ struct (y : x => (arg : x) -> type) (z : x => y => (arg1 : x) -> (arg2 : y) -> type) *) - let signature (tacs : (Ident.user * T.Chk.tac) list) : T.Chk.tac = + let signature (tacs : (Ident.t * T.Chk.tac) list) : T.Chk.tac = univ_tac "Univ.signature" @@ fun univ -> let+ fields = quantifiers (List.map (fun (lbl, tac) -> (lbl, T.Chk.run tac)) tacs) univ in S.CodeSignature fields @@ -698,8 +832,8 @@ struct when we construct the final codes. Most notably, we need to make sure to properly eliminate the 'ext' types introduced by previous patches. *) - let patch_fields (sign : (Ident.user * D.con) list) (tacs : Ident.user -> T.Chk.tac option) (univ : D.tp) : S.t m = - let rec go (field_names : Ident.user list) (codes : D.con list) (elim_conns : (S.t TB.m -> S.t TB.m) list) sign = + let patch_fields (sign : (Ident.t * D.con) list) (tacs : Ident.t -> T.Chk.tac option) (univ : D.tp) : S.t m = + let rec go (field_names : Ident.t list) (codes : D.con list) (elim_conns : (S.t TB.m -> S.t TB.m) list) sign = match sign with | (field_name, vfield_tp) :: sign -> let* (code, elim_conn) = @@ -736,7 +870,7 @@ struct RM.ret @@ S.CodeSignature qsign in go [] [] [] sign - let patch (sig_tac : T.Chk.tac) (tacs : Ident.user -> T.Chk.tac option) : T.Chk.tac = + let patch (sig_tac : T.Chk.tac) (tacs : Ident.t -> T.Chk.tac option) : T.Chk.tac = univ_tac "Univ.patch" @@ fun univ -> let* code = T.Chk.run sig_tac univ in let* vcode = RM.lift_ev @@ Sem.eval code in diff --git a/src/core/Refiner.mli b/src/core/Refiner.mli index 8a9af8743..af24984e9 100644 --- a/src/core/Refiner.mli +++ b/src/core/Refiner.mli @@ -10,7 +10,7 @@ open Tactic type ('a, 'b) quantifier = 'a -> Ident.t * (var -> 'b) -> 'b type 'a telescope = - | Bind of Ident.user * 'a * (var -> 'a telescope) + | Bind of Ident.t * 'a * (var -> 'a telescope) | Done module Hole : sig @@ -54,6 +54,25 @@ module LockedPrf : sig val unlock : Syn.tac -> Chk.tac -> Chk.tac end +module Desc : sig + val formation : Tp.tac + val end_ : Chk.tac + val arg : Chk.tac -> Chk.tac -> Chk.tac + val rec_ : Chk.tac -> Chk.tac +end + +module Ctx : sig + val formation : Tp.tac + val nil : Chk.tac + val snoc : Chk.tac -> Ident.t -> Chk.tac -> Chk.tac +end + +module Tm : sig + val formation : Chk.tac -> Chk.tac -> Tp.tac + val var : Ident.t -> Chk.tac + val app : Syn.tac -> Chk.tac -> Syn.tac +end + module Univ : sig val formation : Tp.tac val univ : Chk.tac @@ -61,8 +80,8 @@ module Univ : sig val circle : Chk.tac val pi : Chk.tac -> Chk.tac -> Chk.tac val sg : Chk.tac -> Chk.tac -> Chk.tac - val signature : (Ident.user * Chk.tac) list -> Chk.tac - val patch : Chk.tac -> (Ident.user -> Chk.tac option) -> Chk.tac + val signature : (Ident.t * Chk.tac) list -> Chk.tac + val patch : Chk.tac -> (Ident.t -> Chk.tac option) -> Chk.tac val total : Syn.tac -> Chk.tac val ext : int -> Chk.tac -> Chk.tac -> Chk.tac -> Chk.tac val code_v : Chk.tac -> Chk.tac -> Chk.tac -> Chk.tac -> Chk.tac @@ -103,10 +122,10 @@ end module Signature : sig val formation : Tp.tac telescope -> Tp.tac - val intro : (Ident.user -> Chk.tac option) -> Chk.tac - val proj : Syn.tac -> Ident.user -> Syn.tac + val intro : (Ident.t -> Chk.tac option) -> Chk.tac + val proj : Syn.tac -> Ident.t -> Syn.tac - val find_field_tac : (Ident.user * Chk.tac) list -> Ident.user -> Chk.tac option + val find_field_tac : (Ident.t * Chk.tac) list -> Ident.t -> Chk.tac option end module Sub : sig diff --git a/src/core/Semantics.ml b/src/core/Semantics.ml index a1e099c6c..dc8669760 100644 --- a/src/core/Semantics.ml +++ b/src/core/Semantics.ml @@ -176,7 +176,7 @@ and push_subst_con : D.dim -> DimProbe.t -> D.con -> D.con CM.m = fun r x -> let open CM in function - | D.Dim0 | D.Dim1 | D.Prf | D.Zero | D.Base | D.StableCode (`Nat | `Circle | `Univ) as con -> ret con + | D.Dim0 | D.Dim1 | D.Prf | D.Zero | D.Base | D.StableCode (`Nat | `Circle | `Univ) | D.DescEnd | D.CtxNil as con -> ret con | D.LetSym (s, y, con) -> push_subst_con r x @<< push_subst_con s y con | D.Suc con -> @@ -205,6 +205,30 @@ and push_subst_con : D.dim -> DimProbe.t -> D.con -> D.con CM.m = | D.Struct fields -> let+ fields = MU.map (MU.second (subst_con r x)) fields in D.Struct fields + | D.DescArg (arg, desc) -> + let+ arg = subst_con r x arg + and+ desc = subst_con r x desc in + D.DescArg (arg, desc) + | D.DescRec desc -> + let+ desc = subst_con r x desc in + D.DescRec desc + | CtxSnoc (ctx, ident, desc) -> + let+ ctx = subst_con r x ctx + and+ desc = subst_con r x desc in + D.CtxSnoc (ctx, ident, desc) + | D.TmVar x -> + ret @@ D.TmVar x + | D.TmAppArg (base, fam, fn, arg) -> + let+ base = push_subst_con r x base + and+ fam = push_subst_con r x fam + and+ fn = push_subst_con r x fn + and+ arg = push_subst_con r x arg in + D.TmAppArg (base, fam, fn, arg) + | D.TmAppRec (desc, fn, arg) -> + let+ desc = push_subst_con r x desc + and+ fn = push_subst_con r x fn + and+ arg = push_subst_con r x arg in + D.TmAppRec (desc, fn, arg) | D.StableCode code -> let+ code = subst_stable_code r x code in D.StableCode code @@ -345,7 +369,11 @@ and subst_tp : D.dim -> DimProbe.t -> D.tp -> D.tp CM.m = and+ phi = subst_cof r x phi and+ clo = subst_clo r x clo in D.Sub (base, phi, clo) - | D.Univ | D.Nat | D.Circle | D.TpDim | D.TpCof as con -> ret con + | D.Desc | D.Ctx | D.Univ | D.Nat | D.Circle | D.TpDim | D.TpCof as con -> ret con + | D.Tm (ctx, desc) -> + let+ ctx = subst_con r x ctx + and+ desc = subst_con r x desc in + D.Tm (ctx, desc) | D.TpPrf phi -> let+ phi = subst_cof r x phi in D.TpPrf phi @@ -507,6 +535,14 @@ and eval_tp : S.tp -> D.tp EvM.m = | S.Signature sign -> let+ vsign = eval_sign sign in D.Signature vsign + | S.Desc -> + ret D.Desc + | S.Ctx -> + ret D.Ctx + | S.Tm (ctx, desc) -> + let+ ctx = eval ctx + and+ desc = eval desc in + D.Tm (ctx, desc) | S.Univ -> ret D.Univ | S.El tm -> @@ -605,6 +641,34 @@ and eval : S.t -> D.con EvM.m = | S.Proj (t, lbl) -> let* con = eval t in lift_cmp @@ do_proj con lbl + | S.DescEnd -> + ret D.DescEnd + | S.DescArg (arg, desc) -> + let+ arg = eval arg + and+ desc = eval desc in + D.DescArg (arg, desc) + | S.DescRec desc -> + let+ desc = eval desc in + D.DescRec desc + | S.CtxNil -> + ret D.CtxNil + | S.CtxSnoc (rest, ident, desc) -> + let+ rest = eval rest + and+ desc = eval desc in + D.CtxSnoc (rest, ident, desc) + | S.TmVar v -> + ret @@ D.TmVar v + | S.TmAppArg (base, fam, fn, arg) -> + let+ base = eval base + and+ fam = eval fam + and+ fn = eval fn + and+ arg = eval arg + in D.TmAppArg (base, fam, fn, arg) + | S.TmAppRec (desc, fn, arg) -> + let+ desc = eval desc + and+ fn = eval fn + and+ arg = eval arg + in D.TmAppRec (desc, fn, arg) | S.Coe (tpcode, tr, tr', tm) -> let* r = eval_dim tr in let* r' = eval_dim tr' in @@ -811,7 +875,9 @@ and eval_cof tphi = and whnf_con ~style : D.con -> D.con whnf CM.m = let open CM in function - | D.Lam _ | D.BindSym _ | D.Zero | D.Suc _ | D.Base | D.Pair _ | D.Struct _ | D.SubIn _ | D.ElIn _ | D.LockedPrfIn _ + | D.Lam _ | D.BindSym _ | D.Zero | D.Suc _ | D.Base | D.Pair _ | D.Struct _ + | D.DescEnd | D.DescArg _ | D.DescRec _ | D.CtxNil | D.CtxSnoc _ | D.TmVar _ | D.TmAppArg _ | D.TmAppRec _ + | D.SubIn _ | D.ElIn _ | D.LockedPrfIn _ | D.Cof _ | D.Dim0 | D.Dim1 | D.Prf | D.StableCode _ | D.DimProbe _ -> ret `Done | D.LetSym (r, x, con) -> @@ -1189,7 +1255,7 @@ and do_snd con : D.con CM.m = throw @@ NbeFailed ("Couldn't snd argument in do_snd") end -and cut_frm_sign (cut : D.cut) (sign : D.sign) (lbl : Ident.user) = +and cut_frm_sign (cut : D.cut) (sign : D.sign) (lbl : Ident.t) = let open CM in match sign with | D.Field (flbl, tp, _) when Ident.equal flbl lbl -> ret @@ cut_frm ~tp ~cut (D.KProj lbl) @@ -1201,7 +1267,7 @@ and cut_frm_sign (cut : D.cut) (sign : D.sign) (lbl : Ident.user) = | D.Empty -> throw @@ NbeFailed ("Couldn't find field label in cut_frm_sign") -and do_proj (con : D.con) (lbl : Ident.user) : D.con CM.m = +and do_proj (con : D.con) (lbl : Ident.t) : D.con CM.m = let open CM in abort_if_inconsistent (ret D.tm_abort) @@ let splitter con phis = splice_tm @@ Splice.Macro.commute_split con phis (fun tm -> TB.proj tm lbl) in @@ -1792,7 +1858,6 @@ and do_spine con = let* con' = do_frm con k in do_spine con' sp - and splice_tm t = let env, tm = Splice.compile t in CM.lift_ev env @@ eval tm @@ -1800,3 +1865,9 @@ and splice_tm t = and splice_tp t = let env, tp = Splice.compile t in CM.lift_ev env @@ eval_tp tp + +let rec ctx_lookup con ident = + match con with + | D.CtxSnoc (_, ident', desc) when Ident.equal ident ident' -> Some desc + | D.CtxSnoc (rest, _, _) -> ctx_lookup rest ident + | _ -> None diff --git a/src/core/Semantics.mli b/src/core/Semantics.mli index 0d9306118..88b089d91 100644 --- a/src/core/Semantics.mli +++ b/src/core/Semantics.mli @@ -32,7 +32,7 @@ val do_ap2 : D.con -> D.con -> D.con -> D.con compute val do_aps : D.con -> D.con list -> D.con compute val do_fst : D.con -> D.con compute val do_snd : D.con -> D.con compute -val do_proj : D.con -> Ident.user -> D.con compute +val do_proj : D.con -> Ident.t -> D.con compute val do_sub_out : D.con -> D.con compute val do_el_out : D.con -> D.con compute val unfold_el : D.con D.stable_code -> D.tp compute @@ -51,3 +51,5 @@ val splice_tp : S.tp Splice.t -> D.tp compute val subst_con : D.dim -> DimProbe.t -> D.con -> D.con compute val push_subst_con : D.dim -> DimProbe.t -> D.con -> D.con compute + +val ctx_lookup : D.con -> Ident.t -> D.con option diff --git a/src/core/Serialize.ml b/src/core/Serialize.ml index 09f907848..8faa0b02e 100644 --- a/src/core/Serialize.ml +++ b/src/core/Serialize.ml @@ -42,25 +42,16 @@ let json_to_bwd json_to_el : J.value -> 'a bwd = let labeled lbl v = `A (`String lbl :: v) (* Identitifers *) -let json_of_user = - function - | `User path -> `A (List.map J.string path) - -let json_to_user : J.value -> [> `User of string list] = - function - | `A path -> `User (List.map J.get_string path) - | j -> J.parse_error j "json_to_path" - let json_of_ident : Ident.t -> J.value = function | `Anon -> `String "anon" - | `User _ as u -> `O [("user", json_of_user u)] + | `User path -> `O [("user", `A (List.map J.string path))] | `Machine str -> `O [("machine", `String str)] let json_to_ident : J.value -> Ident.t = function | `String "anon" -> `Anon - | `O [("user", parts)] -> json_to_user parts + | `O [("user", `A path)] -> `User (List.map J.get_string path) | `O [("machine", `String str)] -> `Machine str | j -> J.parse_error j "json_to_ident" @@ -106,53 +97,54 @@ end module Syntax = struct - let rec json_of_tm = - function - | S.Var n -> labeled "var" [json_of_int n] - | S.Global sym -> labeled "global" [Global.serialize sym] - | S.Let (tm, nm, body) -> labeled "let" [json_of_tm tm; json_of_ident nm; json_of_tm body] - | S.Ann (tm, tp) -> labeled "ann" [json_of_tm tm; json_of_tp tp] - | S.Zero -> `String "zero" - | S.Suc tm -> labeled "suc" [json_of_tm tm] - | S.NatElim (mot, zero, suc, scrut) -> labeled "nat_elim" [json_of_tm mot; json_of_tm zero; json_of_tm suc; json_of_tm scrut] - | S.Base -> `String "base" - | S.Loop tm -> labeled "loop" [json_of_tm tm] - | S.CircleElim (mot, base, loop, scrut) -> labeled "circle_elim" [json_of_tm mot; json_of_tm base; json_of_tm loop; json_of_tm scrut] - | S.Lam (nm, body) -> labeled "lam" [json_of_ident nm; json_of_tm body] - | S.Ap (tm0, tm1) -> labeled "ap" [json_of_tm tm0; json_of_tm tm1] - | S.Pair (tm0, tm1) -> labeled "pair" [json_of_tm tm0; json_of_tm tm1] - | S.Fst tm -> labeled "fst" [json_of_tm tm] - | S.Snd tm -> labeled "snd" [json_of_tm tm] - | S.Struct strct -> labeled "struct" [json_of_labeled json_of_tm strct] - | S.Proj (tm, path) -> labeled "proj" [json_of_tm tm; json_of_user path] - | S.Coe (fam, src, trg, tm) -> labeled "coe" [json_of_tm fam; json_of_tm src; json_of_tm trg; json_of_tm tm] - | S.HCom (code, src, trg, cof, tm) -> labeled "hcom" [json_of_tm code; json_of_tm src; json_of_tm trg; json_of_tm cof; json_of_tm tm] - | S.Com (fam, src, trg, cof, tm) -> labeled "com" [json_of_tm fam; json_of_tm src; json_of_tm trg; json_of_tm cof; json_of_tm tm] - | S.SubIn tm -> labeled "sub_in" [json_of_tm tm] - | S.SubOut tm -> labeled "sub_out" [json_of_tm tm] - | S.Dim0 -> `String "dim0" - | S.Dim1 -> `String "dim1" - | S.Cof cof -> labeled "cof" [Cof.json_of_cof_f json_of_tm json_of_tm cof] - | S.ForallCof cof -> labeled "forall" [json_of_tm cof] - | S.CofSplit branches -> labeled "split" @@ List.map (fun (tphi, tm) -> json_of_pair (json_of_tm tphi) (json_of_tm tm)) branches - | S.Prf -> `String "prf" - | S.ElIn tm -> labeled "el_in" [json_of_tm tm] - | S.ElOut tm -> labeled "el_out" [json_of_tm tm] - | S.Box (r, s, phi, sides, cap) -> labeled "box" [json_of_tm r; json_of_tm s; json_of_tm phi; json_of_tm sides; json_of_tm cap] - | S.Cap (r, s, phi, code, box) -> labeled "cap" [json_of_tm r; json_of_tm s; json_of_tm phi; json_of_tm code; json_of_tm box] - | S.VIn (r, pequiv, pivot, base) -> labeled "v_in" [json_of_tm r; json_of_tm pequiv; json_of_tm pivot; json_of_tm base] - | S.VProj (r, pcode, code, pequiv, v) -> labeled "v_proj" [json_of_tm r; json_of_tm pcode; json_of_tm code; json_of_tm pequiv; json_of_tm v] - | S.CodeExt (n, fam, `Global phi, tbdry) -> labeled "code_ext" [json_of_int n; json_of_tm fam; json_of_tm phi; json_of_tm tbdry] - | S.CodePi (tbase, tfam) -> labeled "code_pi" [json_of_tm tbase; json_of_tm tfam] - | S.CodeSg (tbase, tfam) -> labeled "code_sg" [json_of_tm tbase; json_of_tm tfam] - | S.CodeSignature sign -> labeled "code_sign" [json_of_labeled json_of_tm sign] - | S.CodeNat -> `String "code_nat" - | S.CodeUniv -> `String "code_univ" - | S.CodeV (r, pcode, code, pequiv) -> labeled "code_v" [json_of_tm r; json_of_tm pcode; json_of_tm code; json_of_tm pequiv] - | S.CodeCircle -> `String "code_circle" - | S.ESub (sb, tm) -> labeled "sub" [json_of_sub sb; json_of_tm tm] - | S.LockedPrfIn tm -> labeled "prf_in" [json_of_tm tm] - | S.LockedPrfUnlock {tp; cof; prf; bdy} -> labeled "prf_unlock" [json_of_tp tp; json_of_tm cof; json_of_tm prf; json_of_tm bdy] + let rec json_of_tm = failwith "[FIXME] json_of_tm.json_of_tm.json_of_tm: " + + (* function *) + (* | S.Var n -> labeled "var" [json_of_int n] *) + (* | S.Global sym -> labeled "global" [Global.serialize sym] *) + (* | S.Let (tm, nm, body) -> labeled "let" [json_of_tm tm; json_of_ident nm; json_of_tm body] *) + (* | S.Ann (tm, tp) -> labeled "ann" [json_of_tm tm; json_of_tp tp] *) + (* | S.Zero -> `String "zero" *) + (* | S.Suc tm -> labeled "suc" [json_of_tm tm] *) + (* | S.NatElim (mot, zero, suc, scrut) -> labeled "nat_elim" [json_of_tm mot; json_of_tm zero; json_of_tm suc; json_of_tm scrut] *) + (* | S.Base -> `String "base" *) + (* | S.Loop tm -> labeled "loop" [json_of_tm tm] *) + (* | S.CircleElim (mot, base, loop, scrut) -> labeled "circle_elim" [json_of_tm mot; json_of_tm base; json_of_tm loop; json_of_tm scrut] *) + (* | S.Lam (nm, body) -> labeled "lam" [json_of_ident nm; json_of_tm body] *) + (* | S.Ap (tm0, tm1) -> labeled "ap" [json_of_tm tm0; json_of_tm tm1] *) + (* | S.Pair (tm0, tm1) -> labeled "pair" [json_of_tm tm0; json_of_tm tm1] *) + (* | S.Fst tm -> labeled "fst" [json_of_tm tm] *) + (* | S.Snd tm -> labeled "snd" [json_of_tm tm] *) + (* | S.Struct strct -> labeled "struct" [json_of_labeled json_of_tm strct] *) + (* | S.Proj (tm, path) -> labeled "proj" [json_of_tm tm; json_of_ident path] *) + (* | S.Coe (fam, src, trg, tm) -> labeled "coe" [json_of_tm fam; json_of_tm src; json_of_tm trg; json_of_tm tm] *) + (* | S.HCom (code, src, trg, cof, tm) -> labeled "hcom" [json_of_tm code; json_of_tm src; json_of_tm trg; json_of_tm cof; json_of_tm tm] *) + (* | S.Com (fam, src, trg, cof, tm) -> labeled "com" [json_of_tm fam; json_of_tm src; json_of_tm trg; json_of_tm cof; json_of_tm tm] *) + (* | S.SubIn tm -> labeled "sub_in" [json_of_tm tm] *) + (* | S.SubOut tm -> labeled "sub_out" [json_of_tm tm] *) + (* | S.Dim0 -> `String "dim0" *) + (* | S.Dim1 -> `String "dim1" *) + (* | S.Cof cof -> labeled "cof" [Cof.json_of_cof_f json_of_tm json_of_tm cof] *) + (* | S.ForallCof cof -> labeled "forall" [json_of_tm cof] *) + (* | S.CofSplit branches -> labeled "split" @@ List.map (fun (tphi, tm) -> json_of_pair (json_of_tm tphi) (json_of_tm tm)) branches *) + (* | S.Prf -> `String "prf" *) + (* | S.ElIn tm -> labeled "el_in" [json_of_tm tm] *) + (* | S.ElOut tm -> labeled "el_out" [json_of_tm tm] *) + (* | S.Box (r, s, phi, sides, cap) -> labeled "box" [json_of_tm r; json_of_tm s; json_of_tm phi; json_of_tm sides; json_of_tm cap] *) + (* | S.Cap (r, s, phi, code, box) -> labeled "cap" [json_of_tm r; json_of_tm s; json_of_tm phi; json_of_tm code; json_of_tm box] *) + (* | S.VIn (r, pequiv, pivot, base) -> labeled "v_in" [json_of_tm r; json_of_tm pequiv; json_of_tm pivot; json_of_tm base] *) + (* | S.VProj (r, pcode, code, pequiv, v) -> labeled "v_proj" [json_of_tm r; json_of_tm pcode; json_of_tm code; json_of_tm pequiv; json_of_tm v] *) + (* | S.CodeExt (n, fam, `Global phi, tbdry) -> labeled "code_ext" [json_of_int n; json_of_tm fam; json_of_tm phi; json_of_tm tbdry] *) + (* | S.CodePi (tbase, tfam) -> labeled "code_pi" [json_of_tm tbase; json_of_tm tfam] *) + (* | S.CodeSg (tbase, tfam) -> labeled "code_sg" [json_of_tm tbase; json_of_tm tfam] *) + (* | S.CodeSignature sign -> labeled "code_sign" [json_of_labeled json_of_tm sign] *) + (* | S.CodeNat -> `String "code_nat" *) + (* | S.CodeUniv -> `String "code_univ" *) + (* | S.CodeV (r, pcode, code, pequiv) -> labeled "code_v" [json_of_tm r; json_of_tm pcode; json_of_tm code; json_of_tm pequiv] *) + (* | S.CodeCircle -> `String "code_circle" *) + (* | S.ESub (sb, tm) -> labeled "sub" [json_of_sub sb; json_of_tm tm] *) + (* | S.LockedPrfIn tm -> labeled "prf_in" [json_of_tm tm] *) + (* | S.LockedPrfUnlock {tp; cof; prf; bdy} -> labeled "prf_unlock" [json_of_tp tp; json_of_tm cof; json_of_tm prf; json_of_tm bdy] *) and json_of_sub : S.sub -> J.value = function @@ -180,8 +172,9 @@ struct | S.TpESub (sub, tp) -> labeled "subst" [json_of_sub sub; json_of_tp tp ] | S.TpLockedPrf tm -> labeled "locked" [json_of_tm tm] - and json_of_sign : S.sign -> J.value = - fun sign -> json_of_labeled json_of_tp sign + and json_of_sign : S.sign -> J.value = failwith "[FIXME] Basis.Syntax.json_of_sign: " + + (* fun sign -> json_of_labeled json_of_tp sign *) let json_of_ctx ctx : J.value = `A (List.map (fun (nm, tp) -> json_of_pair (json_of_ident nm) (json_of_tp tp)) ctx) @@ -244,7 +237,7 @@ struct S.Struct strct | `A [`String "proj"; j_tm; j_path] -> let tm = json_to_tm j_tm in - let path = json_to_user j_path in + let path = json_to_ident j_path in S.Proj (tm, path) | `A [`String "coe"; j_fam; j_src; j_trg; j_tm] -> let fam = json_to_tm j_fam in @@ -431,32 +424,33 @@ end module Domain = struct - let rec json_of_con : D.con -> J.value = - function - | Lam (ident, clo) -> labeled "lam" [json_of_ident ident; json_of_tm_clo clo] - | BindSym (dim_probe, con) -> labeled "bind_sym" [DimProbe.serialize dim_probe; json_of_con con] - | LetSym (dim, dim_probe, con) -> labeled "let_sym" [json_of_dim dim; DimProbe.serialize dim_probe; json_of_con con] - | Cut {tp; cut} -> labeled "cut" [json_of_tp tp; json_of_cut cut] - | Zero -> `String "zero" - | Suc con -> labeled "suc" [json_of_con con] - | Base -> `String "base" - | Loop dim -> labeled "loop" [json_of_dim dim] - | Pair (con0, con1) -> labeled "pair" [json_of_con con0; json_of_con con1] - | Struct fields -> labeled "struct" [json_of_labeled json_of_con fields] - | SubIn con -> labeled "sub_in" [json_of_con con] - | ElIn con -> labeled "el_in" [json_of_con con] - | Dim0 -> `String "dim0" - | Dim1 -> `String "dim1" - | DimProbe dim_probe -> labeled "dim_probe" [DimProbe.serialize dim_probe] - | Cof cof -> labeled "cof" [Cof.json_of_cof_f json_of_con json_of_con cof] - | Prf -> `String "prf" - | FHCom (tag, src, trg, cof, con) -> labeled "fhcom" [json_of_fhcom_tag tag; json_of_dim src; json_of_dim trg; json_of_cof cof; json_of_con con] - | StableCode code -> labeled "stable_code" [json_of_stable_code code] - | UnstableCode code -> labeled "unstable_code" [json_of_unstable_code code] - | Box (src, trg, cof, sides, cap) -> labeled "box" [json_of_dim src; json_of_dim trg; json_of_cof cof; json_of_con sides; json_of_con cap] - | VIn (s, eq, pivot, base) -> labeled "v_in" [json_of_dim s; json_of_con eq; json_of_con pivot; json_of_con base] - | Split branches -> labeled "split" (json_of_alist json_of_cof json_of_tm_clo branches) - | LockedPrfIn con -> labeled "locked_prf_in" [json_of_con con] + let rec json_of_con : D.con -> J.value = failwith "[FIXME] json_of_con.json_of_con.json_of_con: " + + (* function *) + (* | Lam (ident, clo) -> labeled "lam" [json_of_ident ident; json_of_tm_clo clo] *) + (* | BindSym (dim_probe, con) -> labeled "bind_sym" [DimProbe.serialize dim_probe; json_of_con con] *) + (* | LetSym (dim, dim_probe, con) -> labeled "let_sym" [json_of_dim dim; DimProbe.serialize dim_probe; json_of_con con] *) + (* | Cut {tp; cut} -> labeled "cut" [json_of_tp tp; json_of_cut cut] *) + (* | Zero -> `String "zero" *) + (* | Suc con -> labeled "suc" [json_of_con con] *) + (* | Base -> `String "base" *) + (* | Loop dim -> labeled "loop" [json_of_dim dim] *) + (* | Pair (con0, con1) -> labeled "pair" [json_of_con con0; json_of_con con1] *) + (* | Struct fields -> labeled "struct" [json_of_labeled json_of_con fields] *) + (* | SubIn con -> labeled "sub_in" [json_of_con con] *) + (* | ElIn con -> labeled "el_in" [json_of_con con] *) + (* | Dim0 -> `String "dim0" *) + (* | Dim1 -> `String "dim1" *) + (* | DimProbe dim_probe -> labeled "dim_probe" [DimProbe.serialize dim_probe] *) + (* | Cof cof -> labeled "cof" [Cof.json_of_cof_f json_of_con json_of_con cof] *) + (* | Prf -> `String "prf" *) + (* | FHCom (tag, src, trg, cof, con) -> labeled "fhcom" [json_of_fhcom_tag tag; json_of_dim src; json_of_dim trg; json_of_cof cof; json_of_con con] *) + (* | StableCode code -> labeled "stable_code" [json_of_stable_code code] *) + (* | UnstableCode code -> labeled "unstable_code" [json_of_unstable_code code] *) + (* | Box (src, trg, cof, sides, cap) -> labeled "box" [json_of_dim src; json_of_dim trg; json_of_cof cof; json_of_con sides; json_of_con cap] *) + (* | VIn (s, eq, pivot, base) -> labeled "v_in" [json_of_dim s; json_of_con eq; json_of_con pivot; json_of_con base] *) + (* | Split branches -> labeled "split" (json_of_alist json_of_cof json_of_tm_clo branches) *) + (* | LockedPrfIn con -> labeled "locked_prf_in" [json_of_con con] *) and json_of_tm_clo : D.tm_clo -> J.value = function @@ -501,10 +495,11 @@ struct | Circle -> `String "circle" | TpLockedPrf cof -> labeled "tp_locked_prf" [json_of_cof cof] - and json_of_sign : D.sign -> J.value = - function - | D.Empty -> `String "empty" - | D.Field (lbl, tp, clo) -> labeled "field" [json_of_user lbl; json_of_tp tp; json_of_sign_clo clo] + and json_of_sign : D.sign -> J.value = failwith "[FIXME] Basis.Domain.json_of_sign: " + + (* function *) + (* | D.Empty -> `String "empty" *) + (* | D.Field (lbl, tp, clo) -> labeled "field" [json_of_ident lbl; json_of_tp tp; json_of_sign_clo clo] *) and json_of_hd : D.hd -> J.value = function @@ -518,7 +513,7 @@ struct | D.KAp (tp, con) -> labeled "k_ap" [json_of_tp tp; json_of_con con] | D.KFst -> `String "k_fst" | D.KSnd -> `String "k_snd" - | D.KProj lbl -> labeled "k_proj" [json_of_user lbl] + | D.KProj lbl -> labeled "k_proj" [json_of_ident lbl] | D.KNatElim (mot, z, s) -> labeled "k_nat_elim" [json_of_con mot; json_of_con z; json_of_con s] | D.KCircleElim (mot, b, l) -> labeled "k_circle_elim" [json_of_con mot; json_of_con b; json_of_con l] | D.KElOut -> `String "k_el_out" @@ -534,15 +529,16 @@ struct and json_of_cut : D.cut -> J.value = fun (hd, frm) -> labeled "cut" (json_of_hd hd :: List.map json_of_frm frm) - and json_of_stable_code : D.con D.stable_code -> J.value = - function - | `Pi (base, fam) -> labeled "pi" [json_of_con base; json_of_con fam] - | `Sg (base, fam) -> labeled "sg" [json_of_con base; json_of_con fam] - | `Signature sign -> labeled "signature" [json_of_labeled json_of_con sign] - | `Ext (n, code, `Global phi, fam) -> labeled "ext" [json_of_int n; json_of_con code; json_of_con phi; json_of_con fam] - | `Nat -> `String "nat" - | `Circle -> `String "circle" - | `Univ -> `String "univ" + and json_of_stable_code : D.con D.stable_code -> J.value = failwith "[FIXME] Basis.Domain.json_of_stable_code: " + + (* function *) + (* | `Pi (base, fam) -> labeled "pi" [json_of_con base; json_of_con fam] *) + (* | `Sg (base, fam) -> labeled "sg" [json_of_con base; json_of_con fam] *) + (* | `Signature sign -> labeled "signature" [json_of_labeled json_of_con sign] *) + (* | `Ext (n, code, `Global phi, fam) -> labeled "ext" [json_of_int n; json_of_con code; json_of_con phi; json_of_con fam] *) + (* | `Nat -> `String "nat" *) + (* | `Circle -> `String "circle" *) + (* | `Univ -> `String "univ" *) and json_of_unstable_code : D.con D.unstable_code -> J.value = function @@ -636,7 +632,7 @@ struct and json_to_sign : J.value -> D.sign = function | `String "empty" -> Empty - | `A [`String "field"; j_lbl; j_tp; j_clo] -> Field (json_to_user j_lbl, json_to_tp j_tp, json_to_sign_clo j_clo) + | `A [`String "field"; j_lbl; j_tp; j_clo] -> Field (json_to_ident j_lbl, json_to_tp j_tp, json_to_sign_clo j_clo) | j -> J.parse_error j "Domain.json_to_sign" and json_to_hd : J.value -> D.hd = @@ -652,7 +648,7 @@ struct | `A [`String "k_ap"; j_tp; j_con] -> KAp (json_to_tp j_tp, json_to_con j_con) | `String "k_fst" -> KFst | `String "k_snd" -> KSnd - | `A [`String "k_proj"; j_lbl] -> KProj (json_to_user j_lbl) + | `A [`String "k_proj"; j_lbl] -> KProj (json_to_ident j_lbl) | `A [`String "k_nat_elim"; j_mot; j_z; j_s] -> KNatElim (json_to_con j_mot, json_to_con j_z, json_to_con j_s) | `A [`String "k_circle_elim"; j_mot; j_b; j_l] -> KCircleElim (json_to_con j_mot, json_to_con j_b, json_to_con j_l) | `String "k-el_out" -> KElOut diff --git a/src/core/Syntax.ml b/src/core/Syntax.ml index a9d0d5488..acc4e15e3 100644 --- a/src/core/Syntax.ml +++ b/src/core/Syntax.ml @@ -43,7 +43,7 @@ struct | Struct fields -> Format.fprintf fmt "struct[%a]" dump_struct fields - | Proj (tm, lbl) -> Format.fprintf fmt "proj[%a, %a]" dump tm Ident.pp_user lbl + | Proj (tm, lbl) -> Format.fprintf fmt "proj[%a, %a]" dump tm Ident.pp lbl | Coe _ -> Format.fprintf fmt "" | HCom _ -> Format.fprintf fmt "" | Com _ -> Format.fprintf fmt "" @@ -72,7 +72,7 @@ struct | CodeSg _ -> Format.fprintf fmt "" | CodeSignature fields -> Format.fprintf fmt "sig[%a]" - (Pp.pp_sep_list (fun fmt (lbl, tp) -> Format.fprintf fmt "%a : %a" Ident.pp_user lbl dump tp)) + (Pp.pp_sep_list (fun fmt (lbl, tp) -> Format.fprintf fmt "%a : %a" Ident.pp lbl dump tp)) fields | CodeNat -> Format.fprintf fmt "nat" | CodeUniv -> Format.fprintf fmt "univ" @@ -85,10 +85,10 @@ struct | LockedPrfUnlock _ -> Format.fprintf fmt "" and dump_struct fmt fields = - Format.fprintf fmt "%a" (Pp.pp_sep_list (fun fmt (lbl, tp) -> Format.fprintf fmt "%a : %a" Ident.pp_user lbl dump tp)) fields + Format.fprintf fmt "%a" (Pp.pp_sep_list (fun fmt (lbl, tp) -> Format.fprintf fmt "%a : %a" Ident.pp lbl dump tp)) fields and dump_sign fmt sign = - Format.fprintf fmt "%a" (Pp.pp_sep_list (fun fmt (lbl, tp) -> Format.fprintf fmt "%a : %a" Ident.pp_user lbl dump_tp tp)) sign + Format.fprintf fmt "%a" (Pp.pp_sep_list (fun fmt (lbl, tp) -> Format.fprintf fmt "%a : %a" Ident.pp lbl dump_tp tp)) sign and dump_tp fmt = function @@ -149,6 +149,14 @@ struct | Ap _ -> juxtaposition | Pair _ -> tuple | Struct _ -> juxtaposition + | DescEnd -> atom + | DescArg _ -> juxtaposition + | DescRec _ -> juxtaposition + | CtxNil -> atom + | CtxSnoc _ -> juxtaposition + | TmVar _ -> juxtaposition + | TmAppArg _ -> juxtaposition + | TmAppRec _ -> juxtaposition | Proj _ -> proj | CofSplit _ -> tuple | Cof (Cof.Eq _) -> cof_eq @@ -190,7 +198,8 @@ struct let classify_tp : tp -> t = function - | Univ | TpDim | TpCof | Nat | Circle -> atom + | Univ | TpDim | TpCof | Nat | Circle | Desc | Ctx -> atom + | Tm _ -> juxtaposition | El _ -> passed | TpVar _ -> atom | TpPrf _ -> delimited @@ -235,7 +244,7 @@ struct | [] -> () | ((lbl, tp) :: fields) -> Format.fprintf fmt "(%a : %a)@ @,%a" - Ident.pp_user lbl + Ident.pp lbl (pp_field env P.(right_of colon)) tp (pp_fields pp_field env) fields @@ -253,7 +262,23 @@ struct | Struct fields -> Format.fprintf fmt "@[struct %a@]" (pp_fields pp env) fields | Proj (tm, lbl) -> - Format.fprintf fmt "@[%a %@ %a@]" (pp env P.(left_of proj)) tm Ident.pp_user lbl + Format.fprintf fmt "@[%a %@ %a@]" (pp env P.(left_of proj)) tm Ident.pp lbl + | DescEnd -> + Format.fprintf fmt "end" + | DescArg (arg, desc) -> + Format.fprintf fmt "%a -> %a" (pp env penv) arg (pp env penv) desc + | DescRec desc -> + Format.fprintf fmt "□ -> %a" (pp env penv) desc + | CtxNil -> + Format.fprintf fmt "∙" + | CtxSnoc (rest, ident, desc) -> + Format.fprintf fmt "%a ▷ (%a : %a)" (pp env penv) rest Ident.pp ident (pp env penv) desc + | TmVar v -> + Format.fprintf fmt "%a" Ident.pp v + | TmAppArg (_, _, f, a) -> + Format.fprintf fmt "%a %a" (pp env penv) f (pp env penv) a + | TmAppRec (_, f, a) -> + Format.fprintf fmt "%a %a" (pp env penv) f (pp env penv) a | CofSplit branches -> let pp_sep fmt () = Format.fprintf fmt "@ | " in pp_bracketed_list ~pp_sep (pp_cof_split_branch env) fmt branches @@ -515,6 +540,14 @@ struct (pp_tp envx P.(right_of times)) fam | Signature fields -> Format.fprintf fmt "sig %a" (pp_sign env) fields + | Desc -> + Format.fprintf fmt "desc" + | Ctx -> + Format.fprintf fmt "ctx" + | Tm (ctx, DescEnd) -> + Format.fprintf fmt "data %a" (pp env P.(right_of juxtaposition)) ctx + | Tm (ctx, desc) -> + Format.fprintf fmt "tm %a %a" (pp env P.(right_of juxtaposition)) ctx (pp env P.(right_of juxtaposition)) desc | Sub (tp, phi, tm) -> let _x, envx = ppenv_bind env `Anon in Format.fprintf fmt "@[sub %a %a@ %a@]" diff --git a/src/core/SyntaxData.ml b/src/core/SyntaxData.ml index bba146002..179cf81e5 100644 --- a/src/core/SyntaxData.ml +++ b/src/core/SyntaxData.ml @@ -24,8 +24,19 @@ struct | Fst of t | Snd of t - | Struct of (Ident.user * t) list - | Proj of t * Ident.user + | Struct of (Ident.t * t) list + | Proj of t * Ident.t + + | DescEnd + | DescArg of t * t + | DescRec of t + + | CtxNil + | CtxSnoc of t * Ident.t * t + + | TmVar of Ident.t + | TmAppArg of t * t * t * t + | TmAppRec of t * t * t | Coe of t * t * t * t | HCom of t * t * t * t * t @@ -53,7 +64,7 @@ struct | CodeExt of int * t * [`Global of t] * t | CodePi of t * t | CodeSg of t * t - | CodeSignature of (Ident.user * t) list + | CodeSignature of (Ident.t * t) list | CodeNat | CodeUniv | CodeV of t * t * t * t @@ -77,12 +88,15 @@ struct | Pi of tp * Ident.t * tp | Sg of tp * Ident.t * tp | Signature of sign + | Desc + | Ctx + | Tm of t * t | Nat | Circle | TpESub of sub * tp | TpLockedPrf of t - and sign = (Ident.user * tp) list + and sign = (Ident.t * tp) list (** The language of substitions from {{:https://arxiv.org/abs/1102.2405} Abel, Coquand, and Pagano}. *) and sub = diff --git a/src/core/TermBuilder.ml b/src/core/TermBuilder.ml index 287336d0d..9483e49af 100644 --- a/src/core/TermBuilder.ml +++ b/src/core/TermBuilder.ml @@ -161,6 +161,17 @@ let proj m lbl = let+ x = m in S.Proj (x, lbl) +let desc = + ret S.Desc + +let desc_end = + ret S.DescEnd + +let tm mctx mdesc = + let+ ctx = mctx + and+ desc = mdesc in + S.Tm (ctx, desc) + let tm_abort = ret @@ S.tm_abort @@ -242,7 +253,7 @@ let sg ?(ident = `Anon) mbase mfam : _ m = and+ fam = scope mfam in S.Sg (base, ident, fam) -let signature (mfields : (Ident.user * (S.t m list -> S.tp m)) list) : _ m = +let signature (mfields : (Ident.t * (S.t m list -> S.tp m)) list) : _ m = let rec scope_fields bound = function | [] -> ret [] diff --git a/src/core/TermBuilder.mli b/src/core/TermBuilder.mli index d10011513..1d5402f66 100644 --- a/src/core/TermBuilder.mli +++ b/src/core/TermBuilder.mli @@ -30,8 +30,12 @@ val snd : t m -> t m val lams : Ident.t list -> (t m list -> t m) -> t m -val struct_ : (Ident.user * t m) list -> t m -val proj : t m -> Ident.user -> t m +val struct_ : (Ident.t * t m) list -> t m +val proj : t m -> Ident.t -> t m + +val desc : tp m +val desc_end : t m +val tm : t m -> t m -> tp m val zero : t m val suc : t m -> t m @@ -64,7 +68,7 @@ val circle_elim : t m -> t m -> t m -> t m -> t m val pi : ?ident:Ident.t -> tp m -> tp b -> tp m val sg : ?ident:Ident.t -> tp m -> tp b -> tp m -val signature : (Ident.user * (t m list -> tp m)) list -> tp m +val signature : (Ident.t * (t m list -> tp m)) list -> tp m val sub : tp m -> t m -> t b -> tp m val tp_prf : t m -> tp m val tp_dim : tp m @@ -119,8 +123,8 @@ module Kan : sig val coe_sg : base_line:t m -> fam_line:t m -> coe val hcom_sg : base:t m -> fam:t m -> hcom - val coe_sign : field_lines:(Ident.user * t m) list -> coe - val hcom_sign : fields:(Ident.user * t m) list -> hcom + val coe_sign : field_lines:(Ident.t * t m) list -> coe + val hcom_sign : fields:(Ident.t * t m) list -> hcom val hcom_ext : n:int -> cof:t m -> fam:t m -> bdry:t m -> hcom val coe_ext : n:int -> cof:t m -> fam_line:t m -> bdry_line:t m -> coe diff --git a/src/frontend/ConcreteSyntaxData.ml b/src/frontend/ConcreteSyntaxData.ml index 01bf0788d..bba5735ef 100644 --- a/src/frontend/ConcreteSyntaxData.ml +++ b/src/frontend/ConcreteSyntaxData.ml @@ -36,7 +36,8 @@ and con_ = | Sg of cell list * con | Signature of field list | Struct of field list - | Proj of con * Ident.user + | Data of Ident.t * ((Ident.t * cell list) list) + | Proj of con * Ident.t | Patch of con * field list | Total of con * field list | Sub of con * con * con @@ -86,7 +87,7 @@ and con_ = and case = pat * con [@@deriving show] -and field = Field of { lbl : Ident.user; tp : con } +and field = Field of { lbl : Ident.t; tp : con } [@@deriving show] and pat = Pat of {lbl : string list; args : pat_arg list} diff --git a/src/frontend/Elaborator.ml b/src/frontend/Elaborator.ml index 68b2e2f5c..33782bc8d 100644 --- a/src/frontend/Elaborator.ml +++ b/src/frontend/Elaborator.ml @@ -34,9 +34,9 @@ let rec unfold idents k = (* Account for the lambda-bound signature field dependencies. See [NOTE: Sig Code Quantifiers] for more info. *) -let bind_sig_tacs (tacs : ('a Ident.some * T.Chk.tac) list) : ('a Ident.some * T.Chk.tac) list = +let bind_sig_tacs (tacs : (Ident.t * T.Chk.tac) list) : (Ident.t * T.Chk.tac) list = let bind_tac lbls (lbl, tac) = - let tac = Bwd.fold_right (fun lbl tac -> R.Pi.intro ~ident:(lbl :> Ident.t) (fun _ -> tac)) lbls tac in + let tac = Bwd.fold_right (fun lbl tac -> R.Pi.intro ~ident:lbl (fun _ -> tac)) lbls tac in Snoc (lbls, lbl) , (lbl, tac) in snd @@ ListUtil.map_accum_left bind_tac Emp tacs @@ -48,7 +48,8 @@ sig val as_tp : tac -> T.Tp.tac val pi : tac -> Ident.t -> tac -> tac val sg : tac -> Ident.t -> tac -> tac - val signature : (Ident.user * tac) list -> tac + val signature : (Ident.t * tac) list -> tac + val data : T.Chk.tac -> tac val sub : tac -> T.Chk.tac -> T.Chk.tac -> tac val ext : int -> T.Chk.tac -> T.Chk.tac -> T.Chk.tac -> tac val nat : tac @@ -109,7 +110,7 @@ struct let tac = R.Sg.formation tac_base (ident, fun _ -> tac_fam) in Tp tac - let signature (tacs : (Ident.user * tac) list) : tac = + let signature (tacs : (Ident.t * tac) list) : tac = match (as_codes tacs) with | Some tacs -> let tac = R.Univ.signature (bind_sig_tacs tacs) in @@ -119,6 +120,9 @@ struct let tac = R.Signature.formation tele in Tp tac + let data (ctx_tac : T.Chk.tac) : tac = + Tp (R.Tm.formation ctx_tac R.Desc.end_) + let sub tac_tp tac_phi tac_pel : tac = let tac = R.Sub.formation (as_tp tac_tp) tac_phi (fun _ -> tac_pel) in Tp tac @@ -154,6 +158,8 @@ let rec cool_chk_tp : CS.con -> CoolTp.tac = | CS.Signature cells -> let tacs = List.map (fun (CS.Field field) -> (field.lbl, cool_chk_tp field.tp)) cells in CoolTp.signature tacs + | CS.Data (self, ctors) -> + CoolTp.data (chk_ctx self ctors) | CS.Dim -> CoolTp.dim | CS.Cof -> CoolTp.cof | CS.Prf phi -> CoolTp.prf @@ chk_tm phi @@ -302,6 +308,7 @@ and chk_tm : CS.con -> T.Chk.tac = let tacs = bind_sig_tacs @@ List.map (fun (CS.Field field) -> field.lbl, chk_tm field.tp) fields in R.Univ.signature tacs + | CS.Patch (tp, patches) -> let tacs = bind_sig_tacs @@ List.map (fun (CS.Field field) -> field.lbl, chk_tm field.tp) patches in R.Univ.patch (chk_tm tp) (R.Signature.find_field_tac tacs) @@ -352,6 +359,8 @@ and chk_tm : CS.con -> T.Chk.tac = | D.Signature _ -> let field_tac lbl = Option.some @@ chk_tm @@ CS.{node = CS.Proj (con, lbl); info = None} in RM.ret @@ R.Signature.intro field_tac + | D.Tm (ctx, _) -> + RM.ret @@ chk_data ctx con | _ -> RM.ret @@ T.Chk.syn @@ syn_tm con @@ -434,6 +443,47 @@ and chk_cases cases = and chk_case (pat, c) = pat, chk_tm c +and chk_desc (self : Ident.t) (cells : CS.cell list) = + match cells with + | [] -> R.Desc.end_ + | (CS.Cell cell :: cells) -> + match cell.tp.node with + | CS.Var id when Ident.equal self id -> R.Desc.rec_ (chk_desc self cells) + (* [TODO: Reed M, 13/01/2022] This is a hack, handle multiple names properly *) + | _ -> R.Desc.arg (chk_tm cell.tp) (R.Pi.intro ~ident:(List.hd cell.names) (fun _ -> chk_desc self cells)) + +and chk_ctx (self : Ident.t) (cells : (Ident.t * CS.cell list) list) = + List.fold_left (fun tac (ident, args) -> R.Ctx.snoc tac ident (chk_desc self args)) R.Ctx.nil cells + +and chk_data (ctx : D.con) (con : CS.con) = + match con.node with + | CS.Var x -> + begin + match Sem.ctx_lookup ctx x with + | Some _ -> R.Tm.var x + | None -> T.Chk.syn @@ R.Structural.lookup_var x + end + | CS.Ap (c, cs) -> T.Chk.syn @@ List.fold_left (fun tac con -> R.Tm.app tac (chk_data ctx con)) (syn_data ctx c) cs + | _ -> chk_tm con + +and syn_data (ctx : D.con) (con : CS.con) = + match con.node with + | CS.Var x -> + begin + match Sem.ctx_lookup ctx x with + | Some desc -> + let tp = T.Tp.rule @@ + let+ qctx = RM.quote_con D.Ctx ctx + and+ qdesc = RM.quote_con D.Desc desc in + S.Tm (qctx, qdesc) + in + T.Syn.ann (R.Tm.var x) tp + | None -> R.Structural.lookup_var x + end + | CS.Ap (c, cs) -> List.fold_left (fun tac con -> R.Tm.app tac (chk_data ctx con)) (syn_data ctx c) cs + | _ -> syn_tm con + + let rec modifier_ (con : CS.con) = let open Yuujinchou.Pattern in RM.update_span con.info @@ diff --git a/src/frontend/Grammar.mly b/src/frontend/Grammar.mly index 2f58eb155..bd78687ac 100644 --- a/src/frontend/Grammar.mly +++ b/src/frontend/Grammar.mly @@ -43,6 +43,7 @@ %token SUC NAT ZERO UNFOLD GENERALIZE WITH %token CIRCLE BASE LOOP %token SIG STRUCT PROJ AS +%token DATA %token EXT %token COE COM HCOM HFILL %token QUIT NORMALIZE PRINT DEF AXIOM FAIL @@ -319,6 +320,8 @@ plain_term_except_cof_case: { Signature tele } | STRUCT; tele = list(field); { Struct tele } + | DATA; AS; self = plain_name; LSQ; ctors = separated_list(PIPE, ctor); RSQ; + { Data (self, ctors) } | dom = term; RIGHT_ARROW; cod = term { Pi ([Cell {names = [`Anon]; tp = dom}], cod) } | dom = term; TIMES; cod = term @@ -382,7 +385,6 @@ pat_lbl: | lbl = path { lbl } - pat: | lbl = pat_lbl args = list(pat_arg) { Pat {lbl; args} } @@ -397,6 +399,10 @@ field: | LPR lbl = user; COLON tp = term; RPR { Field {lbl; tp} } +ctor: + | lbl = plain_name; args = list(tele_cell) + { (lbl, args) } + patch: | lbl = user; DOT_EQUALS; tp = term { Field {lbl; tp} } diff --git a/src/frontend/Lex.mll b/src/frontend/Lex.mll index c3d59e98d..9ef85a855 100644 --- a/src/frontend/Lex.mll +++ b/src/frontend/Lex.mll @@ -37,6 +37,7 @@ let keywords = ("circle", CIRCLE); ("sig", SIG); ("struct", STRUCT); + ("data", DATA); ("as", AS); ("🍪", CIRCLE); ("let", LET); From a835be949c345fcf9633daf21842ec0ce4618be0 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Thu, 13 Jan 2022 16:56:53 -0800 Subject: [PATCH 2/5] [WIP] Add codes for desc, ctx, and tm --- src/core/Conversion.ml | 5 ++++- src/core/Domain.ml | 3 +++ src/core/DomainData.ml | 9 +++++++++ src/core/Quote.ml | 12 ++++++++++++ src/core/Refiner.ml | 7 +++++++ src/core/Refiner.mli | 1 + src/core/Semantics.ml | 39 ++++++++++++++++++++++++++++++++++++-- src/core/Syntax.ml | 39 +++++++++++++++++++++++++++++++++++--- src/core/SyntaxData.ml | 5 +++++ src/frontend/Elaborator.ml | 6 +++++- 10 files changed, 119 insertions(+), 7 deletions(-) diff --git a/src/core/Conversion.ml b/src/core/Conversion.ml index 9918210f0..5a8c1d7ef 100644 --- a/src/core/Conversion.ml +++ b/src/core/Conversion.ml @@ -151,7 +151,7 @@ and equate_sign sign0 sign1 = and equate_stable_code univ code0 code1 = match code0, code1 with - | `Nat, `Nat | `Circle, `Circle | `Univ, `Univ -> ret () + | `Nat, `Nat | `Circle, `Circle | `Univ, `Univ | `Desc, `Desc | `Ctx, `Ctx -> ret () | `Pi (base0, fam0), `Pi (base1, fam1) | `Sg (base0, fam0), `Sg (base1, fam1) -> let* _ = equate_con univ base0 base1 in @@ -186,6 +186,9 @@ and equate_stable_code univ code0 code1 = | `Signature sign0, `Signature sign1 -> equate_sign_code univ sign0 sign1 + | `Tm (ctx0, desc0), `Tm (ctx1, desc1) -> + let* () = equate_con D.Ctx ctx0 ctx1 in + equate_con D.Desc desc0 desc1 | code0, code1 -> conv_err @@ ExpectedConEq (univ, D.StableCode code0, D.StableCode code1) diff --git a/src/core/Domain.ml b/src/core/Domain.ml index c80ffaaff..51907a279 100644 --- a/src/core/Domain.ml +++ b/src/core/Domain.ml @@ -269,6 +269,9 @@ struct | `Pi _ -> Format.fprintf fmt "" | `Sg _ -> Format.fprintf fmt "" | `Signature _ -> Format.fprintf fmt "" + | `Desc -> Format.fprintf fmt "" + | `Ctx -> Format.fprintf fmt "" + | `Tm (ctx, desc) -> Format.fprintf fmt "ctx[%a, %a]" pp_con ctx pp_con desc | `Nat -> Format.fprintf fmt "" | `Circle -> Format.fprintf fmt "" | `Univ -> Format.fprintf fmt "" diff --git a/src/core/DomainData.ml b/src/core/DomainData.ml index 0125e3f70..e7dc10380 100644 --- a/src/core/DomainData.ml +++ b/src/core/DomainData.ml @@ -20,6 +20,15 @@ struct | `Signature of (Ident.t * 'a) list (** First-Class Record types *) + | `Desc + (** Descriptions *) + + | `Ctx + (** Contexts of Descriptions *) + + | `Tm of 'a * 'a + (** Terms in the language of inductive types. *) + | `Ext of int * 'a * [`Global of 'a] * 'a (** Extension type *) diff --git a/src/core/Quote.ml b/src/core/Quote.ml index 1906c301c..c974dd55d 100644 --- a/src/core/Quote.ml +++ b/src/core/Quote.ml @@ -390,11 +390,23 @@ and quote_stable_code univ = lift_cmp @@ do_ap fam var in S.CodeSg (tbase, tfam) + | `Signature fields -> let+ tfields = MU.map_accum_left_m (quote_stable_field_code univ) fields in S.CodeSignature tfields + | `Desc -> + ret S.CodeDesc + + | `Ctx -> + ret S.CodeCtx + + | `Tm (ctx, desc) -> + let+ ctx = quote_con D.Ctx ctx + and+ desc = quote_con D.Desc desc in + S.CodeTm (ctx, desc) + | `Ext (n, code, `Global phi, bdry) -> let+ tphi = let* tp_cof_fam = lift_cmp @@ splice_tp @@ Splice.term @@ TB.cube n @@ fun _ -> TB.tp_cof in diff --git a/src/core/Refiner.ml b/src/core/Refiner.ml index e203033ba..512feffef 100644 --- a/src/core/Refiner.ml +++ b/src/core/Refiner.ml @@ -882,6 +882,7 @@ struct | _ -> RM.expected_connective `Signature whnf_tp + let total (fam_tac : T.Syn.tac) : T.Chk.tac = univ_tac "Univ.total" @@ fun univ -> let* (tm, tp) = T.Syn.run fam_tac in @@ -922,6 +923,12 @@ struct | D.Pi (base, _, _) -> RM.expected_connective `Signature base | _ -> RM.expected_connective `Pi tp + let tm (ctx_tac : T.Chk.tac) (desc_tac : T.Chk.tac) : T.Chk.tac = + univ_tac "Univ.tm" @@ fun univ -> + let* ctx = T.Chk.run ctx_tac D.Ctx in + let+ desc = T.Chk.run desc_tac D.Desc in + S.CodeTm (ctx, desc) + let ext (n : int) (tac_fam : T.Chk.tac) (tac_cof : T.Chk.tac) (tac_bdry : T.Chk.tac) : T.Chk.tac = univ_tac "Univ.ext" @@ fun univ -> let* tcof = diff --git a/src/core/Refiner.mli b/src/core/Refiner.mli index af24984e9..7b4da951e 100644 --- a/src/core/Refiner.mli +++ b/src/core/Refiner.mli @@ -83,6 +83,7 @@ module Univ : sig val signature : (Ident.t * Chk.tac) list -> Chk.tac val patch : Chk.tac -> (Ident.t -> Chk.tac option) -> Chk.tac val total : Syn.tac -> Chk.tac + val tm : Chk.tac -> Chk.tac -> Chk.tac val ext : int -> Chk.tac -> Chk.tac -> Chk.tac -> Chk.tac val code_v : Chk.tac -> Chk.tac -> Chk.tac -> Chk.tac -> Chk.tac val coe : Chk.tac -> Chk.tac -> Chk.tac -> Chk.tac -> Syn.tac diff --git a/src/core/Semantics.ml b/src/core/Semantics.ml index dc8669760..a7979bec6 100644 --- a/src/core/Semantics.ml +++ b/src/core/Semantics.ml @@ -422,11 +422,15 @@ and subst_stable_code : D.dim -> DimProbe.t -> D.con D.stable_code -> D.con D.st | `Signature fields -> let+ fields = MU.map (MU.second (subst_con r x)) fields in `Signature fields + | `Tm (ctx, desc) -> + let+ ctx = subst_con r x ctx + and+ desc = subst_con r x desc in + `Tm (ctx, desc) | `Ext (n, code, `Global cof, con) -> let+ code = subst_con r x code and+ con = subst_con r x con in `Ext (n, code, `Global cof, con) - | `Nat | `Circle | `Univ as code -> + | `Nat | `Circle | `Univ | `Desc | `Ctx as code -> ret code and subst_cut : D.dim -> DimProbe.t -> D.cut -> D.cut CM.m = @@ -764,12 +768,25 @@ and eval : S.t -> D.con EvM.m = let+ vbase = eval base and+ vfam = eval fam in D.StableCode (`Sg (vbase, vfam)) + | S.CodeSignature fields -> let+ vfields = fields |> MU.map @@ fun (ident, tp) -> let+ vtp = eval tp in (ident, vtp) in D.StableCode (`Signature vfields) + + | S.CodeDesc -> + ret @@ D.StableCode `Desc + + | S.CodeCtx -> + ret @@ D.StableCode `Ctx + + | S.CodeTm (ctx, desc) -> + let+ ctx = eval ctx + and+ desc = eval desc in + D.StableCode (`Tm (ctx, desc)) + | S.CodeNat -> ret @@ D.StableCode `Nat @@ -1531,12 +1548,22 @@ and unfold_el : D.con D.stable_code -> D.tp CM.m = Splice.term @@ TB.sg (TB.el base) @@ fun x -> TB.el @@ TB.ap fam [x] + | `Signature fields -> let (lbls, field_cons) = ListUtil.unzip fields in splice_tp @@ Splice.cons field_cons @@ fun fields -> Splice.term @@ TB.signature @@ List.map2 (fun ident fam -> (ident, fun args -> TB.el @@ TB.ap fam args)) lbls fields + | `Desc -> + ret D.Desc + + | `Ctx -> + ret D.Ctx + + | `Tm (ctx, desc) -> + ret @@ D.Tm (ctx, desc) + | `Ext (n, fam, `Global phi, bdry) -> splice_tp @@ Splice.con phi @@ fun phi -> @@ -1611,7 +1638,7 @@ and enact_rigid_coe line r r' con tag = | `Stable (x, code) -> begin match code with - | `Nat | `Circle | `Univ -> ret con + | `Nat | `Circle | `Univ | `Desc | `Ctx -> ret con | `Pi (basex, famx) -> splice_tm @@ Splice.con (D.BindSym (x, basex)) @@ fun base_line -> @@ -1636,6 +1663,8 @@ and enact_rigid_coe line r r' con tag = Splice.dim r' @@ fun r' -> Splice.con con @@ fun bdy -> Splice.term @@ TB.Kan.coe_sign ~field_lines:(ListUtil.zip lbls fam_lines) ~r ~r' ~bdy + | `Tm (ctxx, descx) -> + failwith "[FIXME] Basis.Basis.enact_rigid_coe: Coercions in terms." | `Ext (n, famx, `Global cof, bdryx) -> splice_tm @@ Splice.con cof @@ fun cof -> @@ -1719,6 +1748,12 @@ and enact_rigid_hcom code r r' phi bdy tag = Splice.con bdy @@ fun bdy -> Splice.term @@ TB.Kan.hcom_sign ~fields:(ListUtil.zip lbls fams) ~r ~r' ~phi ~bdy + | `Desc -> + failwith "[FIXME] Basis.Basis.enact_rigid_hcom: HCom in desc." + | `Ctx -> + failwith "[FIXME] Basis.Basis.enact_rigid_hcom: HCom in ctx." + | `Tm (ctx, desc) -> + failwith "[FIXME] Basis.Basis.enact_rigid_hcom: HCom in terms." | `Ext (n, fam, `Global cof, bdry) -> splice_tm @@ Splice.con cof @@ fun cof -> diff --git a/src/core/Syntax.ml b/src/core/Syntax.ml index acc4e15e3..dedc46a31 100644 --- a/src/core/Syntax.ml +++ b/src/core/Syntax.ml @@ -42,8 +42,19 @@ struct | Snd tm -> Format.fprintf fmt "snd[%a]" dump tm | Struct fields -> Format.fprintf fmt "struct[%a]" dump_struct fields - | Proj (tm, lbl) -> Format.fprintf fmt "proj[%a, %a]" dump tm Ident.pp lbl + + | DescEnd -> Format.fprintf fmt "desc/end" + | DescArg (base, fam) -> Format.fprintf fmt "desc/arg[%a, %a]" dump base dump fam + | DescRec desc -> Format.fprintf fmt "desc/rec[%a]" dump desc + + | CtxNil -> Format.fprintf fmt "ctx/nil" + | CtxSnoc (ctx, ident, desc) -> Format.fprintf fmt "ctx/snoc[%a, %a, %a]" dump ctx Ident.pp ident dump desc + + | TmVar x -> Format.fprintf fmt "tm/var[%a]" Ident.pp x + | TmAppArg (base, fam, fn, arg) -> Format.fprintf fmt "tm/app/arg[%a, %a, %a, %a]" dump base dump fam dump fn dump arg + | TmAppRec (desc, fn, arg) -> Format.fprintf fmt "tm/app/rec[%a, %a, %a]" dump desc dump fn dump arg + | Coe _ -> Format.fprintf fmt "" | HCom _ -> Format.fprintf fmt "" | Com _ -> Format.fprintf fmt "" @@ -74,6 +85,9 @@ struct Format.fprintf fmt "sig[%a]" (Pp.pp_sep_list (fun fmt (lbl, tp) -> Format.fprintf fmt "%a : %a" Ident.pp lbl dump tp)) fields + | CodeDesc -> Format.fprintf fmt "desc" + | CodeCtx -> Format.fprintf fmt "ctx" + | CodeTm (ctx, desc) -> Format.fprintf fmt "tm[%a, %a]" dump ctx dump desc | CodeNat -> Format.fprintf fmt "nat" | CodeUniv -> Format.fprintf fmt "univ" | CodeV _ -> Format.fprintf fmt "" @@ -103,6 +117,9 @@ struct | Pi (base, ident, fam) -> Format.fprintf fmt "pi[%a, %a, %a]" dump_tp base Ident.pp ident dump_tp fam | Sg _ -> Format.fprintf fmt "" | Signature fields -> Format.fprintf fmt "tp/sig[%a]" dump_sign fields + | Desc -> Format.fprintf fmt "tp/desc" + | Ctx -> Format.fprintf fmt "tp/ctx" + | Tm (ctx, desc) -> Format.fprintf fmt "tp/tm[%a, %a]" dump ctx dump desc | Nat -> Format.fprintf fmt "nat" | Circle -> Format.fprintf fmt "circle" | TpESub _ -> Format.fprintf fmt "" @@ -165,7 +182,7 @@ struct | Cof (Cof.Meet _) -> cof_meet | ForallCof _ -> dual juxtaposition arrow - | Zero | Base | CodeNat | CodeCircle | CodeUniv | Dim0 | Dim1 | Prf -> atom + | Zero | Base | CodeNat | CodeCircle | CodeDesc | CodeCtx | CodeUniv | Dim0 | Dim1 | Prf -> atom | Suc _ as tm -> if Option.is_some (to_numeral tm) then atom else juxtaposition | HCom _ | Com _ | Coe _ | Fst _ | Snd _ @@ -176,6 +193,7 @@ struct | CodePi _ -> arrow | CodeSg _ -> times | CodeSignature _ -> juxtaposition + | CodeTm _ -> juxtaposition | CodeExt _ -> juxtaposition | Ann _ -> passed @@ -403,12 +421,27 @@ struct (pp_atomic env) tm | CodeSignature fields -> Format.fprintf fmt "@[sig %a@]" (pp_fields pp_binders env) fields + | CodeDesc when Debug.is_debug_mode () -> + Format.fprintf fmt "`desc" + | CodeDesc -> + Format.fprintf fmt "desc" + | CodeCtx when Debug.is_debug_mode () -> + Format.fprintf fmt "`ctx" + | CodeCtx -> + Format.fprintf fmt "ctx" + | CodeTm (desc, ctx) when Debug.is_debug_mode () -> + Format.fprintf fmt "@[ %a %a@]" + (pp_atomic env) desc + (pp_atomic env) ctx + | CodeTm (desc, ctx) -> + Format.fprintf fmt "@[tm %a %a@]" + (pp_atomic env) desc + (pp_atomic env) ctx | CodeExt (_, fam, `Global phi, bdry) -> Format.fprintf fmt "@[ext %a %a %a@]" (pp_atomic env) fam (pp_atomic Pp.Env.emp) phi (pp_atomic env) bdry - | CodeNat when Debug.is_debug_mode () -> Format.fprintf fmt "`nat" | CodeCircle when Debug.is_debug_mode () -> diff --git a/src/core/SyntaxData.ml b/src/core/SyntaxData.ml index 179cf81e5..f550f3601 100644 --- a/src/core/SyntaxData.ml +++ b/src/core/SyntaxData.ml @@ -38,6 +38,8 @@ struct | TmAppArg of t * t * t * t | TmAppRec of t * t * t + | TmElim of t * t * t + | Coe of t * t * t * t | HCom of t * t * t * t * t | Com of t * t * t * t * t @@ -65,6 +67,9 @@ struct | CodePi of t * t | CodeSg of t * t | CodeSignature of (Ident.t * t) list + | CodeDesc + | CodeCtx + | CodeTm of t * t | CodeNat | CodeUniv | CodeV of t * t * t * t diff --git a/src/frontend/Elaborator.ml b/src/frontend/Elaborator.ml index 33782bc8d..7424da5ca 100644 --- a/src/frontend/Elaborator.ml +++ b/src/frontend/Elaborator.ml @@ -308,13 +308,17 @@ and chk_tm : CS.con -> T.Chk.tac = let tacs = bind_sig_tacs @@ List.map (fun (CS.Field field) -> field.lbl, chk_tm field.tp) fields in R.Univ.signature tacs - | CS.Patch (tp, patches) -> let tacs = bind_sig_tacs @@ List.map (fun (CS.Field field) -> field.lbl, chk_tm field.tp) patches in R.Univ.patch (chk_tm tp) (R.Signature.find_field_tac tacs) + | CS.Total (tp, patches) -> let tacs = bind_sig_tacs @@ List.map (fun (CS.Field field) -> field.lbl, chk_tm field.tp) patches in R.Univ.patch (R.Univ.total (syn_tm tp)) (R.Signature.find_field_tac tacs) + + | CS.Data (self, ctors) -> + R.Univ.tm (chk_ctx self ctors) R.Desc.end_ + | CS.V (r, pcode, code, pequiv) -> R.Univ.code_v (chk_tm r) (chk_tm pcode) (chk_tm code) (chk_tm pequiv) From e015e6a90c7ccceeb7230999d1ebe8f933aa7ecf Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 18 Jan 2022 07:38:30 -0800 Subject: [PATCH 3/5] [WIP] Computing elimination methods --- src/core/Domain.ml | 6 ++++ src/core/DomainData.ml | 1 + src/core/RefineError.ml | 5 ++++ src/core/Refiner.ml | 25 +++++++++++++++++ src/core/Refiner.mli | 1 + src/core/Semantics.ml | 44 +++++++++++++++++++++++++++++- src/core/Syntax.ml | 18 ++++++++++-- src/core/SyntaxData.ml | 4 +-- src/core/TermBuilder.ml | 28 +++++++++++++++++++ src/core/TermBuilder.mli | 7 +++++ src/frontend/ConcreteSyntaxData.ml | 6 +++- src/frontend/Elaborator.ml | 4 +++ src/frontend/Grammar.mly | 10 ++++++- src/frontend/Lex.mll | 4 +++ 14 files changed, 156 insertions(+), 7 deletions(-) diff --git a/src/core/Domain.ml b/src/core/Domain.ml index 51907a279..5ad3260de 100644 --- a/src/core/Domain.ml +++ b/src/core/Domain.ml @@ -103,6 +103,12 @@ struct | KFst -> Format.fprintf fmt "fst" | KSnd -> Format.fprintf fmt "snd" | KProj lbl -> Format.fprintf fmt "proj[%a]" Ident.pp lbl + | KDescMethod (mot, ctx, tm) -> + Format.fprintf fmt + "desc/method[%a, %a, %a]" + pp_con mot + pp_con ctx + pp_con tm | KNatElim _ -> Format.fprintf fmt "" | KCircleElim _ -> Format.fprintf fmt "" | KElOut -> Uuseg_string.pp_utf_8 fmt "⭝ₑₗ" diff --git a/src/core/DomainData.ml b/src/core/DomainData.ml index e7dc10380..3bfabb1f9 100644 --- a/src/core/DomainData.ml +++ b/src/core/DomainData.ml @@ -170,6 +170,7 @@ struct | KFst | KSnd | KProj of Ident.t + | KDescMethod of con * con * con | KNatElim of con * con * con | KCircleElim of con * con * con diff --git a/src/core/RefineError.ml b/src/core/RefineError.ml index 355d5ca8f..d72ce46b5 100644 --- a/src/core/RefineError.ml +++ b/src/core/RefineError.ml @@ -49,6 +49,11 @@ let pp fmt = function | UnboundVariable id -> Fmt.fprintf fmt "Unbound variable %a" Ident.pp id + | NotFoundInCtx (ppenv, ctx, id) -> + Format.fprintf fmt + "Unbound identifier %a in context @[%a@]." + Ident.pp id + (S.pp ppenv) ctx | ExpectedEqual (ppenv, tp, tm0, tm1, _) -> Fmt.fprintf fmt "Expected @[%a =@;%a@;: %a@]" diff --git a/src/core/Refiner.ml b/src/core/Refiner.ml index 512feffef..29d58f85b 100644 --- a/src/core/Refiner.ml +++ b/src/core/Refiner.ml @@ -720,6 +720,31 @@ struct S.TmAppRec (qdesc, ftm, arg), apptp (* [TODO: Reed M, 13/01/2022] Print a better error when we don't have a DescArg/DescApp index. *) | tp -> RM.expected_connective `Tm tp + + let elim_method (tac_mot : T.Chk.tac) (tac_tm : T.Syn.tac) : T.Chk.tac = + T.Chk.rule ~name:"Tm.elim_method" @@ + function + | D.Univ -> + let* (tm, tm_tp) = T.Syn.run tac_tm in + begin + match tm_tp with + | D.Tm (ctx, desc) -> + let* mot_tp = + RM.lift_cmp @@ + Sem.splice_tp @@ + Splice.con ctx @@ fun ctx -> + Splice.term @@ TB.pi (TB.data ctx) (fun _ -> TB.univ) + in + Debug.print "Running Motive Tactic against goal %a@." D.pp_tp mot_tp; + let* mot = T.Chk.run tac_mot mot_tp in + Debug.print "Quoting Context@."; + let* tctx = RM.quote_con D.Ctx ctx in + Debug.print "Quoting Description@."; + let+ tdesc = RM.quote_con D.Desc desc in + S.DescMethod (mot, tctx, tdesc, tm) + | _ -> RM.expected_connective `Tm tm_tp + end + | tp -> RM.expected_connective `Univ tp end module Univ = diff --git a/src/core/Refiner.mli b/src/core/Refiner.mli index 7b4da951e..1b5dcba8b 100644 --- a/src/core/Refiner.mli +++ b/src/core/Refiner.mli @@ -71,6 +71,7 @@ module Tm : sig val formation : Chk.tac -> Chk.tac -> Tp.tac val var : Ident.t -> Chk.tac val app : Syn.tac -> Chk.tac -> Syn.tac + val elim_method : Chk.tac -> Syn.tac -> Chk.tac end module Univ : sig diff --git a/src/core/Semantics.ml b/src/core/Semantics.ml index a7979bec6..5400481a7 100644 --- a/src/core/Semantics.ml +++ b/src/core/Semantics.ml @@ -654,6 +654,12 @@ and eval : S.t -> D.con EvM.m = | S.DescRec desc -> let+ desc = eval desc in D.DescRec desc + | S.DescMethod (mot, ctx, desc, tm) -> + let* mot = eval mot in + let* ctx = eval ctx in + let* desc = eval desc in + let* tm = eval tm in + lift_cmp @@ do_desc_method mot ctx desc tm | S.CtxNil -> ret D.CtxNil | S.CtxSnoc (rest, ident, desc) -> @@ -1316,7 +1322,6 @@ and do_ap2 f a b = let* fa = do_ap f a in do_ap fa b - and do_ap con arg = let open CM in abort_if_inconsistent (ret D.tm_abort) @@ @@ -1356,6 +1361,42 @@ and do_ap con arg = throw @@ NbeFailed "Not a function in do_ap" end +and do_desc_method mot ctx desc tm : D.con CM.m = + let open CM in + abort_if_inconsistent (ret D.tm_abort) @@ + match desc with + | D.DescEnd -> do_ap mot tm + | D.DescArg (base, fam) -> + splice_tm @@ + Splice.con mot @@ fun mot -> + Splice.con ctx @@ fun ctx -> + Splice.con base @@ fun base -> + Splice.con fam @@ fun fam -> + Splice.con tm @@ fun tm -> + Splice.term @@ + TB.code_pi base @@ TB.lam @@ fun x -> + TB.desc_method mot ctx (TB.ap fam [x]) (TB.tm_ap base fam tm x) + | D.DescRec desc -> + splice_tm @@ + Splice.con mot @@ fun mot -> + Splice.con ctx @@ fun ctx -> + Splice.con desc @@ fun desc -> + Splice.con tm @@ fun tm -> + Splice.term @@ + TB.code_pi (TB.code_data ctx) @@ TB.lam @@ fun x -> + TB.code_pi (TB.ap mot [x]) @@ TB.lam @@ fun _ -> + TB.desc_method mot ctx desc (TB.tm_rec desc tm x) + | D.Cut { cut; _ } -> + ret @@ cut_frm ~tp:D.Univ ~cut @@ D.KDescMethod (mot, ctx, tm) + | D.Split branches as con -> + splice_tm @@ + Splice.con mot @@ fun mot -> + Splice.con ctx @@ fun ctx -> + Splice.con tm @@ fun tm -> + Splice.Macro.commute_split con (List.map fst branches) @@ fun desc -> TB.desc_method mot ctx desc tm + | con -> + Format.eprintf "bad desc-method: %a@." D.pp_con con; + CM.throw @@ NbeFailed "Not a description" and do_sub_out con = let open CM in @@ -1881,6 +1922,7 @@ and do_frm con = | D.KFst -> do_fst con | D.KSnd -> do_snd con | D.KProj lbl -> do_proj con lbl + | D.KDescMethod (mot, ctx, tm) -> do_desc_method mot ctx con tm | D.KNatElim (mot, case_zero, case_suc) -> do_nat_elim mot case_zero case_suc con | D.KCircleElim (mot, case_base, case_loop) -> do_circle_elim mot case_base case_loop con | D.KElOut -> do_el_out con diff --git a/src/core/Syntax.ml b/src/core/Syntax.ml index dedc46a31..9ab1ab124 100644 --- a/src/core/Syntax.ml +++ b/src/core/Syntax.ml @@ -47,7 +47,13 @@ struct | DescEnd -> Format.fprintf fmt "desc/end" | DescArg (base, fam) -> Format.fprintf fmt "desc/arg[%a, %a]" dump base dump fam | DescRec desc -> Format.fprintf fmt "desc/rec[%a]" dump desc - + | DescMethod (mot, ctx, desc, tm) -> + Format.fprintf fmt + "desc/method[%a, %a, %a, %a]" + dump mot + dump ctx + dump desc + dump tm | CtxNil -> Format.fprintf fmt "ctx/nil" | CtxSnoc (ctx, ident, desc) -> Format.fprintf fmt "ctx/snoc[%a, %a, %a]" dump ctx Ident.pp ident dump desc @@ -169,6 +175,7 @@ struct | DescEnd -> atom | DescArg _ -> juxtaposition | DescRec _ -> juxtaposition + | DescMethod _ -> juxtaposition | CtxNil -> atom | CtxSnoc _ -> juxtaposition | TmVar _ -> juxtaposition @@ -282,11 +289,18 @@ struct | Proj (tm, lbl) -> Format.fprintf fmt "@[%a %@ %a@]" (pp env P.(left_of proj)) tm Ident.pp lbl | DescEnd -> - Format.fprintf fmt "end" + Format.fprintf fmt "□" | DescArg (arg, desc) -> Format.fprintf fmt "%a -> %a" (pp env penv) arg (pp env penv) desc | DescRec desc -> Format.fprintf fmt "□ -> %a" (pp env penv) desc + | DescMethod (mot, ctx,fam, desc) -> + Format.fprintf fmt + "@[method %a %a %a %a@]" + (pp env penv) mot + (pp env penv) ctx + (pp env penv) fam + (pp env penv) desc | CtxNil -> Format.fprintf fmt "∙" | CtxSnoc (rest, ident, desc) -> diff --git a/src/core/SyntaxData.ml b/src/core/SyntaxData.ml index f550f3601..e4038cc8f 100644 --- a/src/core/SyntaxData.ml +++ b/src/core/SyntaxData.ml @@ -31,6 +31,8 @@ struct | DescArg of t * t | DescRec of t + | DescMethod of t * t * t * t + | CtxNil | CtxSnoc of t * Ident.t * t @@ -38,8 +40,6 @@ struct | TmAppArg of t * t * t * t | TmAppRec of t * t * t - | TmElim of t * t * t - | Coe of t * t * t * t | HCom of t * t * t * t * t | Com of t * t * t * t * t diff --git a/src/core/TermBuilder.ml b/src/core/TermBuilder.ml index 9483e49af..d9b5feed7 100644 --- a/src/core/TermBuilder.ml +++ b/src/core/TermBuilder.ml @@ -172,6 +172,34 @@ let tm mctx mdesc = and+ desc = mdesc in S.Tm (ctx, desc) +let tm_ap mbase mfam mf ma = + let+ base = mbase + and+ fam = mfam + and+ f = mf + and+ a = ma in + S.TmAppArg (base, fam, f, a) + +let desc_method mmot mctx mdesc mtm = + let+ mot = mmot + and+ ctx = mctx + and+ desc = mdesc + and+ tm = mtm in + S.DescMethod (mot, ctx, desc, tm) + +let tm_rec mdesc mf ma = + let+ desc = mdesc + and+ f = mf + and+ a = ma in + S.TmAppRec (desc, f, a) + +let data mctx = + let+ ctx = mctx in + S.Tm (ctx, S.DescEnd) + +let code_data mctx = + let+ ctx = mctx in + S.CodeTm (ctx, S.DescEnd) + let tm_abort = ret @@ S.tm_abort diff --git a/src/core/TermBuilder.mli b/src/core/TermBuilder.mli index 1d5402f66..2595019d9 100644 --- a/src/core/TermBuilder.mli +++ b/src/core/TermBuilder.mli @@ -37,6 +37,13 @@ val desc : tp m val desc_end : t m val tm : t m -> t m -> tp m +val tm_ap : t m -> t m -> t m -> t m -> t m +val tm_rec : t m -> t m -> t m -> t m +val desc_method : t m -> t m -> t m -> t m -> t m + +val data : t m -> tp m +val code_data : t m -> t m + val zero : t m val suc : t m -> t m diff --git a/src/frontend/ConcreteSyntaxData.ml b/src/frontend/ConcreteSyntaxData.ml index bba5735ef..8889ba611 100644 --- a/src/frontend/ConcreteSyntaxData.ml +++ b/src/frontend/ConcreteSyntaxData.ml @@ -36,10 +36,14 @@ and con_ = | Sg of cell list * con | Signature of field list | Struct of field list - | Data of Ident.t * ((Ident.t * cell list) list) | Proj of con * Ident.t | Patch of con * field list | Total of con * field list + | Data of Ident.t * ((Ident.t * cell list) list) + | Desc + | Ctx + | Tm of con * con + | Method of con * con | Sub of con * con * con | Pair of con * con | Fst of con diff --git a/src/frontend/Elaborator.ml b/src/frontend/Elaborator.ml index 7424da5ca..657ef68e6 100644 --- a/src/frontend/Elaborator.ml +++ b/src/frontend/Elaborator.ml @@ -316,6 +316,9 @@ and chk_tm : CS.con -> T.Chk.tac = let tacs = bind_sig_tacs @@ List.map (fun (CS.Field field) -> field.lbl, chk_tm field.tp) patches in R.Univ.patch (R.Univ.total (syn_tm tp)) (R.Signature.find_field_tac tacs) + | CS.Method (mot, tm) -> + R.Tm.elim_method (chk_tm mot) (syn_tm tm) + | CS.Data (self, ctors) -> R.Univ.tm (chk_ctx self ctors) R.Desc.end_ @@ -364,6 +367,7 @@ and chk_tm : CS.con -> T.Chk.tac = let field_tac lbl = Option.some @@ chk_tm @@ CS.{node = CS.Proj (con, lbl); info = None} in RM.ret @@ R.Signature.intro field_tac | D.Tm (ctx, _) -> + Debug.print "Elaborating as data...@."; RM.ret @@ chk_data ctx con | _ -> RM.ret @@ T.Chk.syn @@ syn_tm con diff --git a/src/frontend/Grammar.mly b/src/frontend/Grammar.mly index bd78687ac..9559e6849 100644 --- a/src/frontend/Grammar.mly +++ b/src/frontend/Grammar.mly @@ -43,7 +43,7 @@ %token SUC NAT ZERO UNFOLD GENERALIZE WITH %token CIRCLE BASE LOOP %token SIG STRUCT PROJ AS -%token DATA +%token DESC CTX TERM METHOD DATA %token EXT %token COE COM HCOM HFILL %token QUIT NORMALIZE PRINT DEF AXIOM FAIL @@ -240,6 +240,10 @@ plain_atomic_term_except_name: { Circle } | TYPE { Type } + | DESC + { Desc } + | CTX + { Ctx } | name = HOLE_NAME { Hole (name, None) } | DIM @@ -320,6 +324,10 @@ plain_term_except_cof_case: { Signature tele } | STRUCT; tele = list(field); { Struct tele } + | TERM; ctx = atomic_term; desc = atomic_term + { Tm (ctx, desc) } + | METHOD; mot = atomic_term; tm = atomic_term + { Method (mot, tm) } | DATA; AS; self = plain_name; LSQ; ctors = separated_list(PIPE, ctor); RSQ; { Data (self, ctors) } | dom = term; RIGHT_ARROW; cod = term diff --git a/src/frontend/Lex.mll b/src/frontend/Lex.mll index 9ef85a855..80ffd685e 100644 --- a/src/frontend/Lex.mll +++ b/src/frontend/Lex.mll @@ -37,6 +37,10 @@ let keywords = ("circle", CIRCLE); ("sig", SIG); ("struct", STRUCT); + ("desc", DESC); + ("ctx", CTX); + ("term", TERM); + ("method", METHOD); ("data", DATA); ("as", AS); ("🍪", CIRCLE); From 7e8a3a23becb5a3bbc5c44775254047c4e4d05b0 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 18 Jan 2022 11:40:32 -0800 Subject: [PATCH 4/5] Add unit tests for inductive types --- cooltt.opam | 1 + src/core/Syntax.ml | 2 +- src/core/TermBuilder.ml | 7 ++ src/core/TermBuilder.mli | 2 + unit-test/Inductives.ml | 142 +++++++++++++++++++++++++++++++++++++++ unit-test/cooltt-lib | 1 + unit-test/dune | 7 ++ 7 files changed, 161 insertions(+), 1 deletion(-) create mode 100644 unit-test/Inductives.ml create mode 100644 unit-test/cooltt-lib create mode 100644 unit-test/dune diff --git a/cooltt.opam b/cooltt.opam index 124a27199..74144c6ac 100644 --- a/cooltt.opam +++ b/cooltt.opam @@ -18,6 +18,7 @@ depends: [ "menhir" {>= "20180703"} "uuseg" {>= "12.0.0"} "uutf" {>= "1.0.2"} + "alcotest" {>= "1.5.0"} {with-test} "odoc" {with-doc} "bantorra" "yuujinchou" diff --git a/src/core/Syntax.ml b/src/core/Syntax.ml index 9ab1ab124..2c42b9530 100644 --- a/src/core/Syntax.ml +++ b/src/core/Syntax.ml @@ -444,7 +444,7 @@ struct | CodeCtx -> Format.fprintf fmt "ctx" | CodeTm (desc, ctx) when Debug.is_debug_mode () -> - Format.fprintf fmt "@[ %a %a@]" + Format.fprintf fmt "@[tm %a %a@]" (pp_atomic env) desc (pp_atomic env) ctx | CodeTm (desc, ctx) -> diff --git a/src/core/TermBuilder.ml b/src/core/TermBuilder.ml index d9b5feed7..e496b02e7 100644 --- a/src/core/TermBuilder.ml +++ b/src/core/TermBuilder.ml @@ -167,11 +167,18 @@ let desc = let desc_end = ret S.DescEnd +let desc_rec mdesc = + let+ desc = mdesc in + S.DescRec desc + let tm mctx mdesc = let+ ctx = mctx and+ desc = mdesc in S.Tm (ctx, desc) +let tm_var id = + ret @@ S.TmVar id + let tm_ap mbase mfam mf ma = let+ base = mbase and+ fam = mfam diff --git a/src/core/TermBuilder.mli b/src/core/TermBuilder.mli index 2595019d9..575b3db14 100644 --- a/src/core/TermBuilder.mli +++ b/src/core/TermBuilder.mli @@ -35,8 +35,10 @@ val proj : t m -> Ident.t -> t m val desc : tp m val desc_end : t m +val desc_rec : t m -> t m val tm : t m -> t m -> tp m +val tm_var : Ident.t -> t m val tm_ap : t m -> t m -> t m -> t m -> t m val tm_rec : t m -> t m -> t m -> t m val desc_method : t m -> t m -> t m -> t m -> t m diff --git a/unit-test/Inductives.ml b/unit-test/Inductives.ml new file mode 100644 index 000000000..67e2ae57e --- /dev/null +++ b/unit-test/Inductives.ml @@ -0,0 +1,142 @@ +open Core +open Basis + +open CodeUnit + +module S = Syntax +module D = Domain + +module Sem = Semantics +module TB = TermBuilder + +module Env = RefineEnv +module RM = RefineMonad +open Monad.Notation (RM) +module RMU = Monad.Util (RM) + +(** Testing Utilities *) +let library_manager = + match Bantorra.Manager.init ~anchor:"cooltt-lib" ~routers:[] with + | Ok ans -> ans + | Error (`InvalidRouter msg) -> failwith msg (* this should not happen! *) + +let current_lib = + match Bantorra.Manager.load_library_from_cwd library_manager with + | Error (`InvalidLibrary err) -> failwith err + | Ok (lib, _) -> lib + +let bind_axiom (id : string) (tp : S.tp) : S.t RM.m = + let* vtp = RM.lift_ev @@ Sem.eval_tp tp in + let+ sym = RM.add_global (`User [id]) vtp None in + S.Global sym + +(** Check that two terms of type {mtp} are convertible in under a list of {axioms}. *) +let check_tm (axioms : (string * S.tp) list) (mtp : D.tp RM.m) : (S.t list -> D.con RM.m) Alcotest.testable = + let state = RefineState.init_unit CodeUnitID.top_level @@ RefineState.init in + let env = RefineEnv.init current_lib in + let pp fmt m = + let tm = RM.run state env @@ + let* tp = mtp in + let* globals = RMU.map (fun (str, tp) -> bind_axiom str tp) axioms in + let* v = m globals in + RM.quote_con tp v + in + match tm with + | Ok tm -> S.pp Pp.Env.emp fmt tm + | Error err -> Format.fprintf fmt "Error: %s" (Printexc.to_string err) + in + Alcotest.testable pp @@ fun m0 m1 -> + let res = + RM.run state env @@ + let* tp = mtp in + let* globals = RMU.map (fun (str, tp) -> bind_axiom str tp) axioms in + let* v0 = m0 globals in + let* v1 = m1 globals in + RM.lift_conv_ @@ Conversion.equate_con tp v0 v1 + in + match res with + | Ok _ -> true + | Error (Conversion.ConversionError err) -> + (* [TODO: Reed M, 18/01/2022] Register some exception printers instead. *) + Format.printf "Conversion Failed: %a@." Conversion.Error.pp err; + false + | Error _ -> false + +module Desc = +struct + (** Construct an nary operation. *) + let rec nary n = + if n = 0 then S.DescEnd else S.DescRec (nary @@ n - 1) + + let data ctx = + S.Tm (ctx, S.DescEnd) + + let code_data ctx = + S.CodeTm (ctx, S.DescEnd) +end + +module Signature = +struct + (** Construct a signature from a list of constructors. *) + let of_list xs = + List.fold_left (fun sign (lbl, t) -> S.CtxSnoc (sign, `User [lbl], t)) S.CtxNil xs +end + +(** The signature of the 'nat' datatype. *) +let nat_signature : S.t = + Signature.of_list [("z", Desc.nary 0); ("s", Desc.nary 1)] + +let tree_signature : S.t = + Signature.of_list [("leaf", Desc.nary 0); ("node", Desc.nary 2)] + +let nat_suc_method () = + let tp = RM.ret D.Univ in + let mot = (S.Pi (Desc.data nat_signature, `Machine "x", S.Univ)) in + let mthd [mot] = + RM.lift_ev @@ Sem.eval @@ S.DescMethod (mot, nat_signature, Desc.nary 1, S.TmVar (`User ["s"])) + in + let expected [mot] = + let* vmot = RM.lift_ev @@ Sem.eval mot in + let* nat_sig = RM.lift_ev @@ Sem.eval nat_signature in + RM.lift_cmp @@ + Sem.splice_tm @@ + Splice.con nat_sig @@ fun nat_sig -> + Splice.con vmot @@ fun mot -> + Splice.term @@ + TB.code_pi (TB.code_data nat_sig) @@ TB.lam @@ fun n -> + TB.code_pi (TB.ap mot [n]) @@ TB.lam @@ fun _ -> + TB.ap mot [TB.tm_rec TB.desc_end (TB.tm_var (`User ["s"])) n] + in + Alcotest.check (check_tm ["mot", mot] tp) "method of induction for nat/suc" mthd expected + +let tree_node_method () = + let tp = RM.ret D.Univ in + let mot = S.Pi (Desc.data tree_signature, `Machine "x", S.Univ) in + let mthd [mot] = + RM.lift_ev @@ Sem.eval @@ S.DescMethod (mot, tree_signature, Desc.nary 2, S.TmVar (`User ["node"])) + in + let expected [mot] = + let* vmot = RM.lift_ev @@ Sem.eval mot in + let* tree_sig = RM.lift_ev @@ Sem.eval tree_signature in + RM.lift_cmp @@ + Sem.splice_tm @@ + Splice.con tree_sig @@ fun tree_sig -> + Splice.con vmot @@ fun mot -> + Splice.term @@ + TB.code_pi (TB.code_data tree_sig) @@ TB.lam @@ fun t0 -> + TB.code_pi (TB.ap mot [t0]) @@ TB.lam @@ fun _ -> + TB.code_pi (TB.code_data tree_sig) @@ TB.lam @@ fun t1 -> + TB.code_pi (TB.ap mot [t1]) @@ TB.lam @@ fun _ -> + TB.ap mot [TB.tm_rec TB.desc_end (TB.tm_rec (TB.desc_rec TB.desc_end) (TB.tm_var (`User ["node"])) t0) t1] + in + Alcotest.check (check_tm ["mot", mot] tp) "method of induction for tree/node" mthd expected + +let () = + let open Alcotest in + Debug.debug_mode true; + run "Inductives" [ + "Methods of Induction", [ + test_case "nat/suc" `Quick nat_suc_method; + test_case "tree/node" `Quick tree_node_method; + ] + ] diff --git a/unit-test/cooltt-lib b/unit-test/cooltt-lib new file mode 100644 index 000000000..30e36ec40 --- /dev/null +++ b/unit-test/cooltt-lib @@ -0,0 +1 @@ +{ "format": "1.0.0" } \ No newline at end of file diff --git a/unit-test/dune b/unit-test/dune new file mode 100644 index 000000000..6f56b251f --- /dev/null +++ b/unit-test/dune @@ -0,0 +1,7 @@ +(tests + (names inductives) + (libraries cooltt.frontend alcotest) + (flags + (:standard -w -8)) + (deps + (glob_files ./cooltt-lib))) \ No newline at end of file From 32f9e4c7d1b2f7e4b1ee1dca7de1a7e7a3a27e3f Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 18 Jan 2022 16:31:39 -0800 Subject: [PATCH 5/5] [WIP] Rework 'DescMethod', start adding in 'Elem' machinery --- src/core/Domain.ml | 14 ++++-- src/core/DomainData.ml | 12 +++++- src/core/Quote.ml | 49 +++++++++++++++++---- src/core/RefineError.ml | 2 + src/core/RefineErrorData.ml | 1 + src/core/Refiner.ml | 46 +++++++++++++++++++- src/core/Refiner.mli | 6 +++ src/core/Semantics.ml | 86 +++++++++++++++++++++++++++++-------- src/core/Semantics.mli | 2 + src/core/Syntax.ml | 49 +++++++++++++++------ src/core/SyntaxData.ml | 7 ++- src/core/TermBuilder.ml | 8 ++-- unit-test/Inductives.ml | 65 +++++++++++++++++++++------- 13 files changed, 281 insertions(+), 66 deletions(-) diff --git a/src/core/Domain.ml b/src/core/Domain.ml index 5ad3260de..b60f295bc 100644 --- a/src/core/Domain.ml +++ b/src/core/Domain.ml @@ -103,12 +103,11 @@ struct | KFst -> Format.fprintf fmt "fst" | KSnd -> Format.fprintf fmt "snd" | KProj lbl -> Format.fprintf fmt "proj[%a]" Ident.pp lbl - | KDescMethod (mot, ctx, tm) -> + | KDescMethod (ctx, mot) -> Format.fprintf fmt - "desc/method[%a, %a, %a]" - pp_con mot + "desc/method[%a, %a]" pp_con ctx - pp_con tm + pp_con mot | KNatElim _ -> Format.fprintf fmt "" | KCircleElim _ -> Format.fprintf fmt "" | KElOut -> Uuseg_string.pp_utf_8 fmt "⭝ₑₗ" @@ -173,6 +172,10 @@ struct Format.fprintf fmt "ctx-nil" | CtxSnoc(ctx, ident, desc) -> Format.fprintf fmt "ctx-snoc[%a, %a, %a]" pp_con ctx Ident.pp ident pp_con desc + | ElemHere (ctx, desc) -> + Format.fprintf fmt "elem-here[%a, %a]" pp_con ctx pp_con desc + | ElemThere (ctx, desc0, desc1, elem) -> + Format.fprintf fmt "elem-here[%a, %a, %a, %a]" pp_con ctx pp_con desc0 pp_con desc1 pp_con elem | TmVar v -> Format.fprintf fmt "tm-var[%a]" Ident.pp v | TmAppArg (base, fam, f, a) -> @@ -248,6 +251,8 @@ struct Format.fprintf fmt "" | Ctx -> Format.fprintf fmt "" + | Elem (ctx, desc) -> + Format.fprintf fmt "elem[%a, %a]" pp_con ctx pp_con desc | Tm (ctx, desc) -> Format.fprintf fmt "tm[%a, %a]" pp_con ctx pp_con desc | Univ -> @@ -277,6 +282,7 @@ struct | `Signature _ -> Format.fprintf fmt "" | `Desc -> Format.fprintf fmt "" | `Ctx -> Format.fprintf fmt "" + | `Elem (ctx, desc) -> Format.fprintf fmt "elem[%a, %a]" pp_con ctx pp_con desc | `Tm (ctx, desc) -> Format.fprintf fmt "ctx[%a, %a]" pp_con ctx pp_con desc | `Nat -> Format.fprintf fmt "" | `Circle -> Format.fprintf fmt "" diff --git a/src/core/DomainData.ml b/src/core/DomainData.ml index 3bfabb1f9..374beab1a 100644 --- a/src/core/DomainData.ml +++ b/src/core/DomainData.ml @@ -26,6 +26,9 @@ struct | `Ctx (** Contexts of Descriptions *) + | `Elem of 'a * 'a + (** A proof that [A ∈ Γ] *) + | `Tm of 'a * 'a (** Terms in the language of inductive types. *) @@ -91,6 +94,12 @@ struct | CtxNil | CtxSnoc of con * Ident.t * con + (** Proofs that [A ∈ Γ] *) + | ElemHere of con * con + (** [∀ Γ A → A ∈ (Γ, A) ] *) + | ElemThere of con * con * con * con + (** [∀ Γ A B → A ∈ Γ → A ∈ (Γ, B) ] *) + (** Formal expressions involving elements of a context. We can think of these as embedded terms from the simple type theory of inductive types. *) | TmVar of Ident.t @@ -141,6 +150,7 @@ struct | Signature of sign | Desc | Ctx + | Elem of con * con | Tm of con * con | Nat | Circle @@ -170,7 +180,7 @@ struct | KFst | KSnd | KProj of Ident.t - | KDescMethod of con * con * con + | KDescMethod of con * con | KNatElim of con * con * con | KCircleElim of con * con * con diff --git a/src/core/Quote.ml b/src/core/Quote.ml index c974dd55d..140532f08 100644 --- a/src/core/Quote.ml +++ b/src/core/Quote.ml @@ -134,6 +134,18 @@ let rec quote_con (tp : D.tp) con = and+ desc = quote_con D.Desc desc in S.CtxSnoc (ctx, ident, desc) + | _, D.ElemHere (ctx, desc) -> + let+ ctx = quote_con D.Ctx ctx + and+ desc = quote_con D.Desc desc in + S.ElemHere (ctx, desc) + + | _, D.ElemThere (ctx, desc0, desc1, elem) -> + let+ ctx = quote_con D.Ctx ctx + and+ desc0 = quote_con D.Desc desc0 + and+ desc1 = quote_con D.Desc desc1 + and+ elem = quote_con (D.Elem (ctx, desc0)) elem in + S.ElemThere (ctx, desc0, desc1, elem) + | _, D.TmVar x -> ret @@ S.TmVar x @@ -402,6 +414,11 @@ and quote_stable_code univ = | `Ctx -> ret S.CodeCtx + | `Elem (ctx, desc) -> + let+ ctx = quote_con D.Ctx ctx + and+ desc = quote_con D.Desc desc in + S.CodeElem (ctx, desc) + | `Tm (ctx, desc) -> let+ ctx = quote_con D.Ctx ctx and+ desc = quote_con D.Desc desc in @@ -503,10 +520,14 @@ and quote_tp (tp : D.tp) = ret S.Desc | D.Ctx -> ret S.Ctx + | D.Elem (ctx, desc) -> + let+ ctx = quote_con D.Ctx ctx + and+ desc = quote_con D.Desc desc in + S.Elem (ctx, desc) | D.Tm (ctx, desc) -> let+ ctx = quote_con D.Ctx ctx and+ desc = quote_con D.Desc desc in - S .Tm (ctx, desc) + S.Tm (ctx, desc) | D.Univ -> ret S.Univ | D.ElStable code -> @@ -672,8 +693,18 @@ and quote_spine tm = let* tm' = quote_frm tm k in quote_spine tm' spine -and quote_frm tm = +and quote_frm hd = function + | D.KDescMethod (ctx, mot) -> + let* tctx = quote_con D.Ctx ctx in + let* mot_tp = + lift_cmp @@ + Sem.splice_tp @@ + Splice.con ctx @@ fun ctx -> + Splice.term @@ TB.pi (TB.data ctx) @@ fun _ -> TB.univ + in + let+ tmot = quote_con mot_tp mot in + S.DescMethod (tctx, tmot, hd) | D.KNatElim (mot, zero_case, suc_case) -> let* mot_tp = lift_cmp @@ Sem.splice_tp @@ Splice.term @@ @@ -694,7 +725,7 @@ and quote_frm tm = TB.el @@ TB.ap mot [TB.suc x] in let* tsuc_case = quote_con suc_tp suc_case in - ret @@ S.NatElim (tmot, tzero_case, tsuc_case, tm) + ret @@ S.NatElim (tmot, tzero_case, tsuc_case, hd) | D.KCircleElim (mot, base_case, loop_case) -> let* mot_tp = lift_cmp @@ Sem.splice_tp @@ Splice.term @@ @@ -714,15 +745,15 @@ and quote_frm tm = TB.el @@ TB.ap mot [TB.loop x] in let* tloop_case = quote_con loop_tp loop_case in - ret @@ S.CircleElim (tmot, tbase_case, tloop_case, tm) + ret @@ S.CircleElim (tmot, tbase_case, tloop_case, hd) | D.KFst -> - ret @@ S.Fst tm + ret @@ S.Fst hd | D.KSnd -> - ret @@ S.Snd tm + ret @@ S.Snd hd | D.KProj lbl -> - ret @@ S.Proj (tm, lbl) + ret @@ S.Proj (hd, lbl) | D.KAp (tp, con) -> let+ targ = quote_con tp con in - S.Ap (tm, targ) + S.Ap (hd, targ) | D.KElOut -> - ret @@ S.ElOut tm + ret @@ S.ElOut hd diff --git a/src/core/RefineError.ml b/src/core/RefineError.ml index d72ce46b5..0944e1ee3 100644 --- a/src/core/RefineError.ml +++ b/src/core/RefineError.ml @@ -24,6 +24,8 @@ let pp_connective fmt = Format.fprintf fmt "desc" | `Ctx -> Format.fprintf fmt "ctx" + | `Elem -> + Format.fprintf fmt "elem" | `Tm -> Format.fprintf fmt "tm" | `Univ -> diff --git a/src/core/RefineErrorData.ml b/src/core/RefineErrorData.ml index 331e0daf5..85705b89b 100644 --- a/src/core/RefineErrorData.ml +++ b/src/core/RefineErrorData.ml @@ -13,6 +13,7 @@ struct | `Signature | `Desc | `Ctx + | `Elem | `Tm | `Nat | `Circle diff --git a/src/core/Refiner.ml b/src/core/Refiner.ml index 29d58f85b..45beb33b8 100644 --- a/src/core/Refiner.ml +++ b/src/core/Refiner.ml @@ -647,6 +647,47 @@ struct S.CtxSnoc (rest, ident, desc) end +module Elem = +struct + let formation (ctx_tac : T.Chk.tac) (desc_tac : T.Chk.tac) : T.Tp.tac = + T.Tp.rule ~name:"Elem.formation" @@ + let+ ctx = T.Chk.run ctx_tac D.Ctx + and+ desc = T.Chk.run desc_tac D.Desc in + S.Elem (ctx, desc) + + let here : T.Chk.tac = + T.Chk.rule ~name:"Elem.here" @@ + function + | D.Elem (ctx, desc0) -> + begin + match ctx with + | D.CtxSnoc (_, _, desc1) -> + let* _ = RM.equate D.Desc desc0 desc1 in + let* tctx = RM.quote_con D.Ctx ctx in + let+ tdesc = RM.quote_con D.Desc desc0 in + S.ElemHere (tctx, tdesc) + | _ -> failwith "[FIXME] Containers.Elem.here: Better error handling for index mismatches" + end + | tp -> RM.expected_connective `Elem tp + + let there (elem_tac : T.Chk.tac) : T.Chk.tac = + T.Chk.rule ~name:"Elem.there" @@ + function + | D.Elem (ctx, desc0) -> + begin + match ctx with + | D.CtxSnoc (ctx, _, desc1) -> + let* elem = T.Chk.run elem_tac (D.Elem (ctx, desc0)) in + let* tctx = RM.quote_con D.Ctx ctx in + let* tdesc0 = RM.quote_con D.Desc desc0 in + let+ tdesc1 = RM.quote_con D.Desc desc1 in + S.ElemThere (tctx, tdesc0, tdesc1, elem) + | _ -> failwith "[FIXME] Containers.Elem.there: Better error handling for index mismatches" + end + | tp -> RM.expected_connective `Elem tp + +end + module Tm = struct let formation (ctx_tac : T.Chk.tac) (desc_tac : T.Chk.tac) : T.Tp.tac = @@ -741,7 +782,8 @@ struct let* tctx = RM.quote_con D.Ctx ctx in Debug.print "Quoting Description@."; let+ tdesc = RM.quote_con D.Desc desc in - S.DescMethod (mot, tctx, tdesc, tm) + (* [TODO: Reed M, 18/01/2022] Does this make sense? Or should I expand this out to something with a function type... *) + S.Ap (S.DescMethod (mot, tctx, tdesc), tm) | _ -> RM.expected_connective `Tm tm_tp end | tp -> RM.expected_connective `Univ tp @@ -949,7 +991,7 @@ struct | _ -> RM.expected_connective `Pi tp let tm (ctx_tac : T.Chk.tac) (desc_tac : T.Chk.tac) : T.Chk.tac = - univ_tac "Univ.tm" @@ fun univ -> + univ_tac "Univ.tm" @@ fun _ -> let* ctx = T.Chk.run ctx_tac D.Ctx in let+ desc = T.Chk.run desc_tac D.Desc in S.CodeTm (ctx, desc) diff --git a/src/core/Refiner.mli b/src/core/Refiner.mli index 1b5dcba8b..3cbfecd8a 100644 --- a/src/core/Refiner.mli +++ b/src/core/Refiner.mli @@ -67,6 +67,12 @@ module Ctx : sig val snoc : Chk.tac -> Ident.t -> Chk.tac -> Chk.tac end +module Elem : sig + val formation : Chk.tac -> Chk.tac -> Tp.tac + val here : Chk.tac + val there : Chk.tac -> Chk.tac +end + module Tm : sig val formation : Chk.tac -> Chk.tac -> Tp.tac val var : Ident.t -> Chk.tac diff --git a/src/core/Semantics.ml b/src/core/Semantics.ml index 5400481a7..9fa47e246 100644 --- a/src/core/Semantics.ml +++ b/src/core/Semantics.ml @@ -212,10 +212,20 @@ and push_subst_con : D.dim -> DimProbe.t -> D.con -> D.con CM.m = | D.DescRec desc -> let+ desc = subst_con r x desc in D.DescRec desc - | CtxSnoc (ctx, ident, desc) -> + | D.CtxSnoc (ctx, ident, desc) -> let+ ctx = subst_con r x ctx and+ desc = subst_con r x desc in D.CtxSnoc (ctx, ident, desc) + | D.ElemHere (ctx, desc) -> + let+ ctx = subst_con r x ctx + and+ desc = subst_con r x desc in + D.ElemHere (ctx, desc) + | D.ElemThere (ctx, desc0, desc1, elem) -> + let+ ctx = subst_con r x ctx + and+ desc0 = subst_con r x desc0 + and+ desc1 = subst_con r x desc1 + and+ elem = subst_con r x elem in + D.ElemThere (ctx, desc0, desc1, elem) | D.TmVar x -> ret @@ D.TmVar x | D.TmAppArg (base, fam, fn, arg) -> @@ -370,6 +380,10 @@ and subst_tp : D.dim -> DimProbe.t -> D.tp -> D.tp CM.m = and+ clo = subst_clo r x clo in D.Sub (base, phi, clo) | D.Desc | D.Ctx | D.Univ | D.Nat | D.Circle | D.TpDim | D.TpCof as con -> ret con + | D.Elem (ctx, desc) -> + let+ ctx = subst_con r x ctx + and+ desc = subst_con r x desc in + D.Elem (ctx, desc) | D.Tm (ctx, desc) -> let+ ctx = subst_con r x ctx and+ desc = subst_con r x desc in @@ -422,6 +436,10 @@ and subst_stable_code : D.dim -> DimProbe.t -> D.con D.stable_code -> D.con D.st | `Signature fields -> let+ fields = MU.map (MU.second (subst_con r x)) fields in `Signature fields + | `Elem (ctx, desc) -> + let+ ctx = subst_con r x ctx + and+ desc = subst_con r x desc in + `Elem (ctx, desc) | `Tm (ctx, desc) -> let+ ctx = subst_con r x ctx and+ desc = subst_con r x desc in @@ -498,6 +516,10 @@ and subst_frm : D.dim -> DimProbe.t -> D.frm -> D.frm CM.m = let+ tp = subst_tp r x tp and+ arg = subst_con r x arg in D.KAp (tp, arg) + | D.KDescMethod (ctx, mot) -> + let+ ctx = subst_con r x ctx + and+ mot = subst_con r x mot in + D.KDescMethod (ctx, mot) | D.KNatElim (con0, con1, con2) -> let+ con0 = subst_con r x con0 and+ con1 = subst_con r x con1 @@ -543,6 +565,10 @@ and eval_tp : S.tp -> D.tp EvM.m = ret D.Desc | S.Ctx -> ret D.Ctx + | S.Elem (ctx, desc) -> + let+ ctx = eval ctx + and+ desc = eval desc in + D.Elem (ctx, desc) | S.Tm (ctx, desc) -> let+ ctx = eval ctx and+ desc = eval desc in @@ -654,18 +680,27 @@ and eval : S.t -> D.con EvM.m = | S.DescRec desc -> let+ desc = eval desc in D.DescRec desc - | S.DescMethod (mot, ctx, desc, tm) -> - let* mot = eval mot in + | S.DescMethod (ctx, mot, desc) -> let* ctx = eval ctx in + let* mot = eval mot in let* desc = eval desc in - let* tm = eval tm in - lift_cmp @@ do_desc_method mot ctx desc tm + lift_cmp @@ do_desc_method ctx mot desc | S.CtxNil -> ret D.CtxNil | S.CtxSnoc (rest, ident, desc) -> let+ rest = eval rest and+ desc = eval desc in D.CtxSnoc (rest, ident, desc) + | S.ElemHere (ctx, desc) -> + let+ ctx = eval ctx + and+ desc = eval desc in + D.ElemHere (ctx, desc) + | S.ElemThere (ctx, desc0, desc1, elem) -> + let+ ctx = eval ctx + and+ desc0 = eval desc0 + and+ desc1 = eval desc1 + and+ elem = eval elem in + D.ElemThere (ctx, desc0, desc1, elem) | S.TmVar v -> ret @@ D.TmVar v | S.TmAppArg (base, fam, fn, arg) -> @@ -788,6 +823,11 @@ and eval : S.t -> D.con EvM.m = | S.CodeCtx -> ret @@ D.StableCode `Ctx + | S.CodeElem (ctx, desc) -> + let+ ctx = eval ctx + and+ desc = eval desc in + D.StableCode (`Elem (ctx, desc)) + | S.CodeTm (ctx, desc) -> let+ ctx = eval ctx and+ desc = eval desc in @@ -899,7 +939,9 @@ and whnf_con ~style : D.con -> D.con whnf CM.m = let open CM in function | D.Lam _ | D.BindSym _ | D.Zero | D.Suc _ | D.Base | D.Pair _ | D.Struct _ - | D.DescEnd | D.DescArg _ | D.DescRec _ | D.CtxNil | D.CtxSnoc _ | D.TmVar _ | D.TmAppArg _ | D.TmAppRec _ + | D.DescEnd | D.DescArg _ | D.DescRec _ | D.CtxNil | D.CtxSnoc _ + | D.ElemHere _ | D.ElemThere _ + | D.TmVar _ | D.TmAppArg _ | D.TmAppRec _ | D.SubIn _ | D.ElIn _ | D.LockedPrfIn _ | D.Cof _ | D.Dim0 | D.Dim1 | D.Prf | D.StableCode _ | D.DimProbe _ -> ret `Done @@ -1361,39 +1403,40 @@ and do_ap con arg = throw @@ NbeFailed "Not a function in do_ap" end -and do_desc_method mot ctx desc tm : D.con CM.m = +and do_desc_method ctx mot desc : D.con CM.m = let open CM in abort_if_inconsistent (ret D.tm_abort) @@ match desc with - | D.DescEnd -> do_ap mot tm + | D.DescEnd -> + (* NOTE: This has been eta-contracted *) + ret mot | D.DescArg (base, fam) -> splice_tm @@ - Splice.con mot @@ fun mot -> Splice.con ctx @@ fun ctx -> + Splice.con mot @@ fun mot -> Splice.con base @@ fun base -> Splice.con fam @@ fun fam -> - Splice.con tm @@ fun tm -> Splice.term @@ + TB.lam @@ fun tm -> TB.code_pi base @@ TB.lam @@ fun x -> - TB.desc_method mot ctx (TB.ap fam [x]) (TB.tm_ap base fam tm x) + TB.desc_method ctx mot (TB.ap fam [x]) (TB.tm_ap base fam tm x) | D.DescRec desc -> splice_tm @@ - Splice.con mot @@ fun mot -> Splice.con ctx @@ fun ctx -> + Splice.con mot @@ fun mot -> Splice.con desc @@ fun desc -> - Splice.con tm @@ fun tm -> Splice.term @@ + TB.lam @@ fun tm -> TB.code_pi (TB.code_data ctx) @@ TB.lam @@ fun x -> TB.code_pi (TB.ap mot [x]) @@ TB.lam @@ fun _ -> - TB.desc_method mot ctx desc (TB.tm_rec desc tm x) + TB.desc_method ctx mot desc (TB.tm_rec desc tm x) | D.Cut { cut; _ } -> - ret @@ cut_frm ~tp:D.Univ ~cut @@ D.KDescMethod (mot, ctx, tm) + ret @@ cut_frm ~tp:D.Univ ~cut @@ D.KDescMethod (ctx, mot) | D.Split branches as con -> splice_tm @@ Splice.con mot @@ fun mot -> Splice.con ctx @@ fun ctx -> - Splice.con tm @@ fun tm -> - Splice.Macro.commute_split con (List.map fst branches) @@ fun desc -> TB.desc_method mot ctx desc tm + Splice.Macro.commute_split con (List.map fst branches) @@ fun desc -> TB.lam @@ fun tm -> TB.desc_method mot ctx desc tm | con -> Format.eprintf "bad desc-method: %a@." D.pp_con con; CM.throw @@ NbeFailed "Not a description" @@ -1602,6 +1645,9 @@ and unfold_el : D.con D.stable_code -> D.tp CM.m = | `Ctx -> ret D.Ctx + | `Elem (ctx, desc) -> + ret @@ D.Elem (ctx, desc) + | `Tm (ctx, desc) -> ret @@ D.Tm (ctx, desc) @@ -1704,6 +1750,8 @@ and enact_rigid_coe line r r' con tag = Splice.dim r' @@ fun r' -> Splice.con con @@ fun bdy -> Splice.term @@ TB.Kan.coe_sign ~field_lines:(ListUtil.zip lbls fam_lines) ~r ~r' ~bdy + | `Elem (ctxx, descx) -> + failwith "[FIXME] Basis.Basis.enact_rigid_coe: Coercions in elem." | `Tm (ctxx, descx) -> failwith "[FIXME] Basis.Basis.enact_rigid_coe: Coercions in terms." | `Ext (n, famx, `Global cof, bdryx) -> @@ -1793,6 +1841,8 @@ and enact_rigid_hcom code r r' phi bdy tag = failwith "[FIXME] Basis.Basis.enact_rigid_hcom: HCom in desc." | `Ctx -> failwith "[FIXME] Basis.Basis.enact_rigid_hcom: HCom in ctx." + | `Elem (ctx, desc) -> + failwith "[FIXME] Basis.Basis.enact_rigid_hcom: HCom in elem." | `Tm (ctx, desc) -> failwith "[FIXME] Basis.Basis.enact_rigid_hcom: HCom in terms." | `Ext (n, fam, `Global cof, bdry) -> @@ -1922,7 +1972,7 @@ and do_frm con = | D.KFst -> do_fst con | D.KSnd -> do_snd con | D.KProj lbl -> do_proj con lbl - | D.KDescMethod (mot, ctx, tm) -> do_desc_method mot ctx con tm + | D.KDescMethod (ctx, mot) -> do_desc_method ctx mot con | D.KNatElim (mot, case_zero, case_suc) -> do_nat_elim mot case_zero case_suc con | D.KCircleElim (mot, case_base, case_loop) -> do_circle_elim mot case_base case_loop con | D.KElOut -> do_el_out con diff --git a/src/core/Semantics.mli b/src/core/Semantics.mli index 88b089d91..74df053d2 100644 --- a/src/core/Semantics.mli +++ b/src/core/Semantics.mli @@ -53,3 +53,5 @@ val subst_con : D.dim -> DimProbe.t -> D.con -> D.con compute val push_subst_con : D.dim -> DimProbe.t -> D.con -> D.con compute val ctx_lookup : D.con -> Ident.t -> D.con option + +exception NbeFailed of string diff --git a/src/core/Syntax.ml b/src/core/Syntax.ml index 2c42b9530..a08ac70a3 100644 --- a/src/core/Syntax.ml +++ b/src/core/Syntax.ml @@ -47,16 +47,18 @@ struct | DescEnd -> Format.fprintf fmt "desc/end" | DescArg (base, fam) -> Format.fprintf fmt "desc/arg[%a, %a]" dump base dump fam | DescRec desc -> Format.fprintf fmt "desc/rec[%a]" dump desc - | DescMethod (mot, ctx, desc, tm) -> + | DescMethod (ctx, mot, desc) -> Format.fprintf fmt - "desc/method[%a, %a, %a, %a]" - dump mot + "desc/method[%a, %a, %a]" dump ctx + dump mot dump desc - dump tm | CtxNil -> Format.fprintf fmt "ctx/nil" | CtxSnoc (ctx, ident, desc) -> Format.fprintf fmt "ctx/snoc[%a, %a, %a]" dump ctx Ident.pp ident dump desc + | ElemHere (ctx, desc) -> Format.fprintf fmt "elem/here[%a, %a]" dump ctx dump desc + | ElemThere (ctx, desc0, desc1, elem) -> Format.fprintf fmt "elem/there[%a, %a, %a, %a]" dump ctx dump desc0 dump desc1 dump elem + | TmVar x -> Format.fprintf fmt "tm/var[%a]" Ident.pp x | TmAppArg (base, fam, fn, arg) -> Format.fprintf fmt "tm/app/arg[%a, %a, %a, %a]" dump base dump fam dump fn dump arg | TmAppRec (desc, fn, arg) -> Format.fprintf fmt "tm/app/rec[%a, %a, %a]" dump desc dump fn dump arg @@ -93,6 +95,7 @@ struct fields | CodeDesc -> Format.fprintf fmt "desc" | CodeCtx -> Format.fprintf fmt "ctx" + | CodeElem (ctx, desc) -> Format.fprintf fmt "elem[%a, %a]" dump ctx dump desc | CodeTm (ctx, desc) -> Format.fprintf fmt "tm[%a, %a]" dump ctx dump desc | CodeNat -> Format.fprintf fmt "nat" | CodeUniv -> Format.fprintf fmt "univ" @@ -125,6 +128,7 @@ struct | Signature fields -> Format.fprintf fmt "tp/sig[%a]" dump_sign fields | Desc -> Format.fprintf fmt "tp/desc" | Ctx -> Format.fprintf fmt "tp/ctx" + | Elem (ctx, desc) -> Format.fprintf fmt "tp/elem[%a, %a]" dump ctx dump desc | Tm (ctx, desc) -> Format.fprintf fmt "tp/tm[%a, %a]" dump ctx dump desc | Nat -> Format.fprintf fmt "nat" | Circle -> Format.fprintf fmt "circle" @@ -178,6 +182,8 @@ struct | DescMethod _ -> juxtaposition | CtxNil -> atom | CtxSnoc _ -> juxtaposition + | ElemHere _ -> juxtaposition + | ElemThere _ -> juxtaposition | TmVar _ -> juxtaposition | TmAppArg _ -> juxtaposition | TmAppRec _ -> juxtaposition @@ -200,6 +206,7 @@ struct | CodePi _ -> arrow | CodeSg _ -> times | CodeSignature _ -> juxtaposition + | CodeElem _ -> juxtaposition | CodeTm _ -> juxtaposition | CodeExt _ -> juxtaposition @@ -233,6 +240,7 @@ struct | Pi _ -> arrow | Sg _ -> times | Signature _ -> juxtaposition + | Elem _ -> juxtaposition | TpESub _ -> substitution | TpLockedPrf _ -> juxtaposition end @@ -294,17 +302,25 @@ struct Format.fprintf fmt "%a -> %a" (pp env penv) arg (pp env penv) desc | DescRec desc -> Format.fprintf fmt "□ -> %a" (pp env penv) desc - | DescMethod (mot, ctx,fam, desc) -> + | DescMethod (ctx, mot, desc) -> Format.fprintf fmt - "@[method %a %a %a %a@]" - (pp env penv) mot + "@[method %a %a %a@]" (pp env penv) ctx - (pp env penv) fam + (pp env penv) mot (pp env penv) desc | CtxNil -> Format.fprintf fmt "∙" | CtxSnoc (rest, ident, desc) -> Format.fprintf fmt "%a ▷ (%a : %a)" (pp env penv) rest Ident.pp ident (pp env penv) desc + | ElemHere (ctx, desc) -> + Format.fprintf fmt "@[here %a %a@]" (pp env penv) ctx (pp env penv) desc + | ElemThere (ctx, desc0, desc1, elem) -> + Format.fprintf fmt + "@[there %a %a %a %a@]" + (pp env penv) ctx + (pp env penv) desc0 + (pp env penv) desc1 + (pp env penv) elem | TmVar v -> Format.fprintf fmt "%a" Ident.pp v | TmAppArg (_, _, f, a) -> @@ -433,8 +449,10 @@ struct Uuseg_string.pp_utf_8 "Σ" (pp_atomic env) base (pp_atomic env) tm + | CodeSignature fields -> Format.fprintf fmt "@[sig %a@]" (pp_fields pp_binders env) fields + | CodeDesc when Debug.is_debug_mode () -> Format.fprintf fmt "`desc" | CodeDesc -> @@ -443,14 +461,17 @@ struct Format.fprintf fmt "`ctx" | CodeCtx -> Format.fprintf fmt "ctx" - | CodeTm (desc, ctx) when Debug.is_debug_mode () -> - Format.fprintf fmt "@[tm %a %a@]" + | CodeElem (ctx, desc) -> + Format.fprintf fmt "@[%a ∋ %a@]" + (pp_atomic env) ctx (pp_atomic env) desc + | CodeTm (ctx, DescEnd) -> + Format.fprintf fmt "@[data %a@]" (pp_atomic env) ctx - | CodeTm (desc, ctx) -> + | CodeTm (ctx, desc) -> Format.fprintf fmt "@[tm %a %a@]" - (pp_atomic env) desc (pp_atomic env) ctx + (pp_atomic env) desc | CodeExt (_, fam, `Global phi, bdry) -> Format.fprintf fmt "@[ext %a %a %a@]" (pp_atomic env) fam @@ -593,6 +614,10 @@ struct Format.fprintf fmt "ctx" | Tm (ctx, DescEnd) -> Format.fprintf fmt "data %a" (pp env P.(right_of juxtaposition)) ctx + | Elem (ctx, desc) -> + Format.fprintf fmt "@[%a ∋ %a@]" + (pp_atomic env) ctx + (pp_atomic env) desc | Tm (ctx, desc) -> Format.fprintf fmt "tm %a %a" (pp env P.(right_of juxtaposition)) ctx (pp env P.(right_of juxtaposition)) desc | Sub (tp, phi, tm) -> diff --git a/src/core/SyntaxData.ml b/src/core/SyntaxData.ml index e4038cc8f..59a3bbdf7 100644 --- a/src/core/SyntaxData.ml +++ b/src/core/SyntaxData.ml @@ -31,11 +31,14 @@ struct | DescArg of t * t | DescRec of t - | DescMethod of t * t * t * t + | DescMethod of t * t * t | CtxNil | CtxSnoc of t * Ident.t * t + | ElemHere of t * t + | ElemThere of t * t * t * t + | TmVar of Ident.t | TmAppArg of t * t * t * t | TmAppRec of t * t * t @@ -69,6 +72,7 @@ struct | CodeSignature of (Ident.t * t) list | CodeDesc | CodeCtx + | CodeElem of t * t | CodeTm of t * t | CodeNat | CodeUniv @@ -95,6 +99,7 @@ struct | Signature of sign | Desc | Ctx + | Elem of t * t | Tm of t * t | Nat | Circle diff --git a/src/core/TermBuilder.ml b/src/core/TermBuilder.ml index e496b02e7..bff44abf5 100644 --- a/src/core/TermBuilder.ml +++ b/src/core/TermBuilder.ml @@ -186,12 +186,12 @@ let tm_ap mbase mfam mf ma = and+ a = ma in S.TmAppArg (base, fam, f, a) -let desc_method mmot mctx mdesc mtm = - let+ mot = mmot - and+ ctx = mctx +let desc_method mctx mmot mdesc mtm = + let+ ctx = mctx + and+ mot = mmot and+ desc = mdesc and+ tm = mtm in - S.DescMethod (mot, ctx, desc, tm) + S.Ap (S.DescMethod (ctx, mot, desc), tm) let tm_rec mdesc mf ma = let+ desc = mdesc diff --git a/unit-test/Inductives.ml b/unit-test/Inductives.ml index 67e2ae57e..c3399e79b 100644 --- a/unit-test/Inductives.ml +++ b/unit-test/Inductives.ml @@ -60,7 +60,8 @@ let check_tm (axioms : (string * S.tp) list) (mtp : D.tp RM.m) : (S.t list -> D. (* [TODO: Reed M, 18/01/2022] Register some exception printers instead. *) Format.printf "Conversion Failed: %a@." Conversion.Error.pp err; false - | Error _ -> false + | Error _ -> + false module Desc = struct @@ -82,18 +83,39 @@ struct List.fold_left (fun sign (lbl, t) -> S.CtxSnoc (sign, `User [lbl], t)) S.CtxNil xs end -(** The signature of the 'nat' datatype. *) +(** Nat Tests *) let nat_signature : S.t = Signature.of_list [("z", Desc.nary 0); ("s", Desc.nary 1)] -let tree_signature : S.t = - Signature.of_list [("leaf", Desc.nary 0); ("node", Desc.nary 2)] +let nat_method_tp = + let* vnat_sig = RM.lift_ev @@ Sem.eval nat_signature in + RM.lift_cmp @@ + Sem.splice_tp @@ + Splice.con vnat_sig @@ fun nat_sig -> + Splice.term @@ + TB.pi (TB.tm nat_sig (TB.desc_rec TB.desc_end)) @@ fun _ -> TB.univ + +let nat_mot = + S.Pi (Desc.data nat_signature, `Machine "x", S.Univ) + +let nat_zero_method () = + let mthd [mot] = + RM.lift_ev @@ Sem.eval @@ S.DescMethod (nat_signature, mot, Desc.nary 0) + in + let expected [mot] = + let* vmot = RM.lift_ev @@ Sem.eval mot in + RM.lift_cmp @@ + Sem.splice_tm @@ + Splice.con vmot @@ fun mot -> + Splice.term @@ + TB.lam @@ fun z -> + TB.ap mot [z] + in + Alcotest.check (check_tm ["mot", nat_mot] nat_method_tp) "method of induction for nat/zero" expected mthd let nat_suc_method () = - let tp = RM.ret D.Univ in - let mot = (S.Pi (Desc.data nat_signature, `Machine "x", S.Univ)) in let mthd [mot] = - RM.lift_ev @@ Sem.eval @@ S.DescMethod (mot, nat_signature, Desc.nary 1, S.TmVar (`User ["s"])) + RM.lift_ev @@ Sem.eval @@ S.DescMethod (nat_signature, mot, Desc.nary 1) in let expected [mot] = let* vmot = RM.lift_ev @@ Sem.eval mot in @@ -103,17 +125,29 @@ let nat_suc_method () = Splice.con nat_sig @@ fun nat_sig -> Splice.con vmot @@ fun mot -> Splice.term @@ - TB.code_pi (TB.code_data nat_sig) @@ TB.lam @@ fun n -> + TB.lam ~ident:(`User ["s"]) @@ fun s -> + TB.code_pi (TB.code_data nat_sig) @@ TB.lam ~ident:(`User ["n"]) @@ fun n -> TB.code_pi (TB.ap mot [n]) @@ TB.lam @@ fun _ -> - TB.ap mot [TB.tm_rec TB.desc_end (TB.tm_var (`User ["s"])) n] + TB.ap mot [TB.tm_rec TB.desc_end s n] in - Alcotest.check (check_tm ["mot", mot] tp) "method of induction for nat/suc" mthd expected + Alcotest.check (check_tm ["mot", nat_mot] nat_method_tp) "method of induction for nat/suc" expected mthd + +(** Tree Tests *) +let tree_signature : S.t = + Signature.of_list [("leaf", Desc.nary 0); ("node", Desc.nary 2)] + +let tree_method_tp = + let* vtree_sig = RM.lift_ev @@ Sem.eval tree_signature in + RM.lift_cmp @@ + Sem.splice_tp @@ + Splice.con vtree_sig @@ fun tree_sig -> + Splice.term @@ + TB.pi (TB.tm tree_sig (TB.desc_rec @@ TB.desc_rec TB.desc_end)) @@ fun _ -> TB.univ let tree_node_method () = - let tp = RM.ret D.Univ in let mot = S.Pi (Desc.data tree_signature, `Machine "x", S.Univ) in let mthd [mot] = - RM.lift_ev @@ Sem.eval @@ S.DescMethod (mot, tree_signature, Desc.nary 2, S.TmVar (`User ["node"])) + RM.lift_ev @@ Sem.eval @@ S.DescMethod (tree_signature, mot, Desc.nary 2) in let expected [mot] = let* vmot = RM.lift_ev @@ Sem.eval mot in @@ -123,19 +157,20 @@ let tree_node_method () = Splice.con tree_sig @@ fun tree_sig -> Splice.con vmot @@ fun mot -> Splice.term @@ + TB.lam @@ fun node -> TB.code_pi (TB.code_data tree_sig) @@ TB.lam @@ fun t0 -> TB.code_pi (TB.ap mot [t0]) @@ TB.lam @@ fun _ -> TB.code_pi (TB.code_data tree_sig) @@ TB.lam @@ fun t1 -> TB.code_pi (TB.ap mot [t1]) @@ TB.lam @@ fun _ -> - TB.ap mot [TB.tm_rec TB.desc_end (TB.tm_rec (TB.desc_rec TB.desc_end) (TB.tm_var (`User ["node"])) t0) t1] + TB.ap mot [TB.tm_rec TB.desc_end (TB.tm_rec (TB.desc_rec TB.desc_end) node t0) t1] in - Alcotest.check (check_tm ["mot", mot] tp) "method of induction for tree/node" mthd expected + Alcotest.check (check_tm ["mot", mot] tree_method_tp) "method of induction for tree/node" expected mthd let () = let open Alcotest in - Debug.debug_mode true; run "Inductives" [ "Methods of Induction", [ + test_case "nat/zero" `Quick nat_zero_method; test_case "nat/suc" `Quick nat_suc_method; test_case "tree/node" `Quick tree_node_method; ]