diff options
Diffstat (limited to 'kernel')
49 files changed, 1080 insertions, 1496 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index fe9ec5794c..8bd4b5bfe1 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -540,7 +540,16 @@ let mk_clos e t = | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) -> {norm = Red; term = FCLOS(t,e)} -let mk_clos_vect env v = CArray.Fun1.map mk_clos env v +(** Hand-unrolling of the map function to bypass the call to the generic array + allocation *) +let mk_clos_vect env v = match v with +| [||] -> [||] +| [|v0|] -> [|mk_clos env v0|] +| [|v0; v1|] -> [|mk_clos env v0; mk_clos env v1|] +| [|v0; v1; v2|] -> [|mk_clos env v0; mk_clos env v1; mk_clos env v2|] +| [|v0; v1; v2; v3|] -> + [|mk_clos env v0; mk_clos env v1; mk_clos env v2; mk_clos env v3|] +| v -> CArray.Fun1.map mk_clos env v (* Translate the head constructor of t from constr to fconstr. This function is parameterized by the function to apply on the direct @@ -785,7 +794,7 @@ let drop_parameters depth n argstk = try try_drop_parameters depth n argstk with Not_found -> (* we know that n < stack_args_size(argstk) (if well-typed term) *) - anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor") + anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor.") (** [eta_expand_ind_stack env ind c s t] computes stacks corresponding to the conversion of the eta expansion of t, considered as an inhabitant @@ -991,7 +1000,7 @@ let rec kl info m = if is_val m then (incr prune; term_of_fconstr m) else let (nm,s) = kni info m [] in - let _ = fapp_stack(nm,s) in (* to unlock Zupdates! *) + let () = if !share then ignore (fapp_stack (nm, s)) in (* to unlock Zupdates! *) zip_term (kl info) (norm_head info nm) s (* no redex: go up for atoms and already normalized terms, go down @@ -1041,7 +1050,7 @@ let inject c = mk_clos (subs_id 0) c let whd_stack infos m stk = let k = kni infos m stk in - let _ = fapp_stack k in (* to unlock Zupdates! *) + let () = if !share then ignore (fapp_stack k) in (* to unlock Zupdates! *) k (* cache of constants: the body is computed only when needed. *) diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 810c346990..94ca4c72dd 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -299,7 +299,7 @@ and pp_bytecodes c = | Ksequence (l1, l2) :: c -> pp_bytecodes l1 ++ pp_bytecodes l2 ++ pp_bytecodes c | i :: c -> - tab () ++ pp_instr i ++ fnl () ++ pp_bytecodes c + pp_instr i ++ fnl () ++ pp_bytecodes c (*spiwack: moved this type in this file because I needed it for retroknowledge which can't depend from cbytegen *) diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index b1fc0c85de..57b397e6f8 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -979,7 +979,7 @@ let compile fail_on_error ?universes:(universes=0) env c = Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ; Some (init_code,!fun_code, Array.of_list fv) with TooLargeInductive tname -> - let fn = if fail_on_error then CErrors.errorlabstrm "compile" else + let fn = if fail_on_error then CErrors.user_err ?loc:None ~hdr:"compile" else (fun x -> Feedback.msg_warning x) in (Pp.(fn (str "Cannot compile code for virtual machine as it uses inductive " ++ diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index f13620e101..40c1e027d4 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -24,33 +24,45 @@ type reloc_info = type patch = reloc_info * int let patch_char4 buff pos c1 c2 c3 c4 = - String.unsafe_set buff pos c1; - String.unsafe_set buff (pos + 1) c2; - String.unsafe_set buff (pos + 2) c3; - String.unsafe_set buff (pos + 3) c4 + Bytes.unsafe_set buff pos c1; + Bytes.unsafe_set buff (pos + 1) c2; + Bytes.unsafe_set buff (pos + 2) c3; + Bytes.unsafe_set buff (pos + 3) c4 let patch buff (pos, n) = patch_char4 buff pos (Char.unsafe_chr n) (Char.unsafe_chr (n asr 8)) (Char.unsafe_chr (n asr 16)) (Char.unsafe_chr (n asr 24)) +(* val patch_int : emitcodes -> ((\*pos*\)int * int) list -> emitcodes *) let patch_int buff patches = (* copy code *before* patching because of nested evaluations: the code we are patching might be called (and thus "concurrently" patched) and results in wrong results. Side-effects... *) - let buff = String.copy buff in + let buff = Bytes.of_string buff in let () = List.iter (fun p -> patch buff p) patches in - buff + (* Note: we follow the apporach suggested by Gabriel Scherer in + PR#136 here, and use unsafe as we own buff. + + The crux of the question that avoids defining emitcodes just as a + Byte.t is the call to hcons in to_memory below. Even if disabling + this optimization has no visible time impact, test data shows + that the optimization is indeed triggered quite often so we + choose ugliness over altering the semantics. + + Handle with care. + *) + Bytes.unsafe_to_string buff (* Buffering of bytecode *) -let out_buffer = ref(String.create 1024) +let out_buffer = ref(Bytes.create 1024) and out_position = ref 0 let out_word b1 b2 b3 b4 = let p = !out_position in - if p >= String.length !out_buffer then begin - let len = String.length !out_buffer in + if p >= Bytes.length !out_buffer then begin + let len = Bytes.length !out_buffer in let new_len = if len <= Sys.max_string_length / 2 then 2 * len @@ -58,8 +70,8 @@ let out_word b1 b2 b3 b4 = if len = Sys.max_string_length then invalid_arg "String.create" (* Pas la bonne exception .... *) else Sys.max_string_length in - let new_buffer = String.create new_len in - String.blit !out_buffer 0 new_buffer 0 len; + let new_buffer = Bytes.create new_len in + Bytes.blit !out_buffer 0 new_buffer 0 len; out_buffer := new_buffer end; patch_char4 !out_buffer p (Char.unsafe_chr b1) @@ -94,10 +106,10 @@ let extend_label_table needed = let backpatch (pos, orig) = let displ = (!out_position - orig) asr 2 in - !out_buffer.[pos] <- Char.unsafe_chr displ; - !out_buffer.[pos+1] <- Char.unsafe_chr (displ asr 8); - !out_buffer.[pos+2] <- Char.unsafe_chr (displ asr 16); - !out_buffer.[pos+3] <- Char.unsafe_chr (displ asr 24) + Bytes.set !out_buffer pos @@ Char.unsafe_chr displ; + Bytes.set !out_buffer (pos+1) @@ Char.unsafe_chr (displ asr 8); + Bytes.set !out_buffer (pos+2) @@ Char.unsafe_chr (displ asr 16); + Bytes.set !out_buffer (pos+3) @@ Char.unsafe_chr (displ asr 24) let define_label lbl = if lbl >= Array.length !label_table then extend_label_table lbl; @@ -308,7 +320,7 @@ let init () = label_table := Array.make 16 (Label_undefined []); reloc_info := [] -type emitcodes = string +type emitcodes = String.t let length = String.length @@ -372,9 +384,8 @@ let to_memory (init_code, fun_code, fv) = init(); emit init_code []; emit fun_code []; - let code = String.create !out_position in - String.unsafe_blit !out_buffer 0 code 0 !out_position; (** Later uses of this string are all purely functional *) + let code = Bytes.sub_string !out_buffer 0 !out_position in let code = CString.hcons code in let reloc = List.rev !reloc_info in Array.iter (fun lbl -> diff --git a/kernel/constr.ml b/kernel/constr.ml index ce20751abc..eecceb32a7 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -81,33 +81,42 @@ type pconstructor = constructor puniverses (* [Var] is used for named variables and [Rel] for variables as de Bruijn indices. *) -type ('constr, 'types) kind_of_term = +type ('constr, 'types, 'sort, 'univs) kind_of_term = | Rel of int | Var of Id.t | Meta of metavariable | Evar of 'constr pexistential - | Sort of Sorts.t + | Sort of 'sort | Cast of 'constr * cast_kind * 'types | Prod of Name.t * 'types * 'types | Lambda of Name.t * 'types * 'constr | LetIn of Name.t * 'constr * 'types * 'constr | App of 'constr * 'constr array - | Const of pconstant - | Ind of pinductive - | Construct of pconstructor + | Const of (constant * 'univs) + | Ind of (inductive * 'univs) + | Construct of (constructor * 'univs) | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint | Proj of projection * 'constr (* constr is the fixpoint of the previous type. Requires option -rectypes of the Caml compiler to be set *) -type t = (t,t) kind_of_term +type t = (t, t, Sorts.t, Instance.t) kind_of_term type constr = t type existential = existential_key * constr array type rec_declaration = Name.t array * constr array * constr array type fixpoint = (int array * int) * rec_declaration + (* The array of [int]'s tells for each component of the array of + mutual fixpoints the number of lambdas to skip before finding the + recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B) + (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is + the recursive argument); + The second component [int] tells which component of the block is + returned *) type cofixpoint = int * rec_declaration + (* The component [int] tells which component of the block of + cofixpoint is returned *) type types = constr @@ -115,7 +124,7 @@ type types = constr (* Term constructors *) (*********************) -(* Constructs a DeBrujin index with number n *) +(* Constructs a de Bruijn index with number n *) let rels = [|Rel 1;Rel 2;Rel 3;Rel 4;Rel 5;Rel 6;Rel 7; Rel 8; Rel 9;Rel 10;Rel 11;Rel 12;Rel 13;Rel 14;Rel 15; Rel 16|] @@ -235,6 +244,12 @@ let mkVar id = Var id let kind c = c +(* The other way around. We treat specifically smart constructors *) +let of_kind = function +| App (f, a) -> mkApp (f, a) +| Cast (c, knd, t) -> mkCast (c, knd, t) +| k -> k + (****************************************************************************) (* Functions to recur through subterms *) (****************************************************************************) @@ -972,28 +987,6 @@ module Hcaseinfo = Hashcons.Make(CaseinfoHash) let case_info_hash = CaseinfoHash.hash -module Hsorts = - Hashcons.Make( - struct - open Sorts - - type t = Sorts.t - type u = universe -> universe - let hashcons huniv = function - Prop c -> Prop c - | Type u -> Type (huniv u) - let eq s1 s2 = - s1 == s2 || - match (s1,s2) with - (Prop c1, Prop c2) -> c1 == c2 - | (Type u1, Type u2) -> u1 == u2 - |_ -> false - let hash = function - | Prop Null -> 0 | Prop Pos -> 1 - | Type u -> 2 + Universe.hash u - end) - -(* let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ *) let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate Hcaseinfo.hcons hcons_ind let hcons = diff --git a/kernel/constr.mli b/kernel/constr.mli index 42d298e3b9..e0954160f9 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -70,7 +70,7 @@ type types = constr (** {6 Term constructors. } *) -(** Constructs a DeBrujin index (DB indices begin at 1) *) +(** Constructs a de Bruijn index (DB indices begin at 1) *) val mkRel : int -> constr (** Constructs a Variable *) @@ -188,23 +188,31 @@ type ('constr, 'types) pfixpoint = type ('constr, 'types) pcofixpoint = int * ('constr, 'types) prec_declaration -type ('constr, 'types) kind_of_term = - | Rel of int - | Var of Id.t +type ('constr, 'types, 'sort, 'univs) kind_of_term = + | Rel of int (** Gallina-variable introduced by [forall], [fun], [let-in], [fix], or [cofix]. *) + + | Var of Id.t (** Gallina-variable that was introduced by Vernacular-command that extends + the local context of the currently open section + (i.e. [Variable] or [Let]). *) + | Meta of metavariable | Evar of 'constr pexistential - | Sort of Sorts.t + | Sort of 'sort | Cast of 'constr * cast_kind * 'types | Prod of Name.t * 'types * 'types (** Concrete syntax ["forall A:B,C"] is represented as [Prod (A,B,C)]. *) | Lambda of Name.t * 'types * 'constr (** Concrete syntax ["fun A:B => C"] is represented as [Lambda (A,B,C)]. *) | LetIn of Name.t * 'constr * 'types * 'constr (** Concrete syntax ["let A:B := C in D"] is represented as [LetIn (A,B,C,D)]. *) | App of 'constr * 'constr array (** Concrete syntax ["(F P1 P2 ... Pn)"] is represented as [App (F, [|P1; P2; ...; Pn|])]. + The {!mkApp} constructor also enforces the following invariant: - [F] itself is not {!App} - and [[|P1;..;Pn|]] is not empty. *) - | Const of constant puniverses - | Ind of inductive puniverses - | Construct of constructor puniverses + + | Const of (constant * 'univs) (** Gallina-variable that was introduced by Vernacular-command that extends the global environment + (i.e. [Parameter], or [Axiom], or [Definition], or [Theorem] etc.) *) + + | Ind of (inductive * 'univs) (** A name of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) + | Construct of (constructor * 'univs) (** A constructor of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint @@ -214,7 +222,8 @@ type ('constr, 'types) kind_of_term = least one argument and the function is not itself an applicative term *) -val kind : constr -> (constr, types) kind_of_term +val kind : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term +val of_kind : (constr, types, Sorts.t, Univ.Instance.t) kind_of_term -> constr (** [equal a b] is true if [a] equals [b] modulo alpha, casts, and application grouping *) @@ -302,13 +311,22 @@ val compare_head_gen : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> (constr -> constr -> bool) -> constr -> constr -> bool +val compare_head_gen_leq_with : + (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> + (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> + (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> + (Sorts.t -> Sorts.t -> bool) -> + (constr -> constr -> bool) -> + (constr -> constr -> bool) -> + constr -> constr -> bool + (** [compare_head_gen_with k1 k2 u s f c1 c2] compares [c1] and [c2] like [compare_head_gen u s f c1 c2], except that [k1] (resp. [k2]) is used,rather than {!kind}, to expose the immediate subterms of [c1] (resp. [c2]). *) val compare_head_gen_with : - (constr -> (constr,types) kind_of_term) -> - (constr -> (constr,types) kind_of_term) -> + (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> + (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> (Sorts.t -> Sorts.t -> bool) -> (constr -> constr -> bool) -> diff --git a/kernel/context.ml b/kernel/context.ml index 4e53b73a28..abb284f226 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -37,9 +37,11 @@ struct module Declaration = struct (* local declaration *) - type t = - | LocalAssum of Name.t * Constr.t (** name, type *) - | LocalDef of Name.t * Constr.t * Constr.t (** name, value, type *) + type ('constr, 'types) pt = + | LocalAssum of Name.t * 'types (** name, type *) + | LocalDef of Name.t * 'constr * 'types (** name, value, type *) + + type t = (Constr.constr, Constr.types) pt (** Return the name bound by a given declaration. *) let get_name = function @@ -87,12 +89,12 @@ struct | LocalDef (_, v, ty) -> f v && f ty (** Check whether the two given declarations are equal. *) - let equal decl1 decl2 = + let equal eq decl1 decl2 = match decl1, decl2 with | LocalAssum (n1,ty1), LocalAssum (n2, ty2) -> - Name.equal n1 n2 && Constr.equal ty1 ty2 + Name.equal n1 n2 && eq ty1 ty2 | LocalDef (n1,v1,ty1), LocalDef (n2,v2,ty2) -> - Name.equal n1 n2 && Constr.equal v1 v2 && Constr.equal ty1 ty2 + Name.equal n1 n2 && eq v1 v2 && eq ty1 ty2 | _ -> false @@ -138,7 +140,7 @@ struct | LocalDef (_,v,ty) -> f v; f ty (** Reduce all terms in a given declaration to a single value. *) - let fold f decl acc = + let fold_constr f decl acc = match decl with | LocalAssum (n,ty) -> f ty acc | LocalDef (n,v,ty) -> f ty (f v acc) @@ -147,14 +149,12 @@ struct | LocalAssum (na, ty) -> na, None, ty | LocalDef (na, v, ty) -> na, Some v, ty - let of_tuple = function - | n, None, ty -> LocalAssum (n,ty) - | n, Some v, ty -> LocalDef (n,v,ty) end (** Rel-context is represented as a list of declarations. Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list. *) + type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list type t = Declaration.t list (** empty rel-context *) @@ -169,14 +169,14 @@ struct (** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] with n = |Δ| and with the local definitions of [Γ] skipped in [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *) - let nhyps = + let nhyps ctx = let open Declaration in let rec nhyps acc = function | [] -> acc | LocalAssum _ :: hyps -> nhyps (succ acc) hyps | LocalDef _ :: hyps -> nhyps acc hyps in - nhyps 0 + nhyps 0 ctx (** Return a declaration designated by a given de Bruijn index. @raise Not_found if the designated de Bruijn index is not present in the designated rel-context. *) @@ -187,7 +187,7 @@ struct | _, [] -> raise Not_found (** Check whether given two rel-contexts are equal. *) - let equal = List.equal Declaration.equal + let equal eq l = List.equal (fun c -> Declaration.equal eq c) l (** Map all terms in a given rel-context. *) let map f = List.smartmap (Declaration.map_constr f) @@ -205,26 +205,26 @@ struct (** Map a given rel-context to a list where each {e local assumption} is mapped to [true] and each {e local definition} is mapped to [false]. *) - let to_tags = + let to_tags l = let rec aux l = function | [] -> l | Declaration.LocalDef _ :: ctx -> aux (true::l) ctx | Declaration.LocalAssum _ :: ctx -> aux (false::l) ctx - in aux [] + in aux [] l (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] with n = |Δ| and with the {e local definitions} of [Γ] skipped in [args]. Example: for [x:T, y:=c, z:U] and [n]=2, it gives [Rel 5, Rel 3]. *) - let to_extended_list n = + let to_extended_list mk n l = let rec reln l p = function - | Declaration.LocalAssum _ :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps + | Declaration.LocalAssum _ :: hyps -> reln (mk (n+p) :: l) (p+1) hyps | Declaration.LocalDef _ :: hyps -> reln l (p+1) hyps | [] -> l in - reln [] 1 + reln [] 1 l (** [extended_vect n Γ] does the same, returning instead an array. *) - let to_extended_vect n hyps = Array.of_list (to_extended_list n hyps) + let to_extended_vect mk n hyps = Array.of_list (to_extended_list mk n hyps) end (** This module represents contexts that can capture non-anonymous variables. @@ -235,9 +235,11 @@ struct module Declaration = struct (** local declaration *) - type t = - | LocalAssum of Id.t * Constr.t (** identifier, type *) - | LocalDef of Id.t * Constr.t * Constr.t (** identifier, value, type *) + type ('constr, 'types) pt = + | LocalAssum of Id.t * 'types (** identifier, type *) + | LocalDef of Id.t * 'constr * 'types (** identifier, value, type *) + + type t = (Constr.constr, Constr.types) pt (** Return the identifier bound by a given declaration. *) let get_id = function @@ -285,12 +287,12 @@ struct | LocalDef (_, v, ty) -> f v && f ty (** Check whether the two given declarations are equal. *) - let equal decl1 decl2 = + let equal eq decl1 decl2 = match decl1, decl2 with | LocalAssum (id1, ty1), LocalAssum (id2, ty2) -> - Id.equal id1 id2 && Constr.equal ty1 ty2 + Id.equal id1 id2 && eq ty1 ty2 | LocalDef (id1, v1, ty1), LocalDef (id2, v2, ty2) -> - Id.equal id1 id2 && Constr.equal v1 v2 && Constr.equal ty1 ty2 + Id.equal id1 id2 && eq v1 v2 && eq ty1 ty2 | _ -> false @@ -336,7 +338,7 @@ struct | LocalDef (_, v, ty) -> f v; f ty (** Reduce all terms in a given declaration to a single value. *) - let fold f decl a = + let fold_constr f decl a = match decl with | LocalAssum (_, ty) -> f ty a | LocalDef (_, v, ty) -> a |> f v |> f ty @@ -348,11 +350,24 @@ struct let of_tuple = function | id, None, ty -> LocalAssum (id, ty) | id, Some v, ty -> LocalDef (id, v, ty) + + let of_rel_decl f = function + | Rel.Declaration.LocalAssum (na,t) -> + LocalAssum (f na, t) + | Rel.Declaration.LocalDef (na,v,t) -> + LocalDef (f na, v, t) + + let to_rel_decl = function + | LocalAssum (id,t) -> + Rel.Declaration.LocalAssum (Name id, t) + | LocalDef (id,v,t) -> + Rel.Declaration.LocalDef (Name id,v,t) end (** Named-context is represented as a list of declarations. Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list. *) + type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list type t = Declaration.t list (** empty named-context *) @@ -371,7 +386,7 @@ struct | [] -> raise Not_found (** Check whether given two named-contexts are equal. *) - let equal = List.equal Declaration.equal + let equal eq l = List.equal (fun c -> Declaration.equal eq c) l (** Map all terms in a given named-context. *) let map f = List.smartmap (Declaration.map_constr f) @@ -388,36 +403,55 @@ struct let fold_outside f l ~init = List.fold_right f l init (** Return the set of all identifiers bound in a given named-context. *) - let to_vars = - List.fold_left (fun accu decl -> Id.Set.add (Declaration.get_id decl) accu) Id.Set.empty + let to_vars l = + List.fold_left (fun accu decl -> Id.Set.add (Declaration.get_id decl) accu) Id.Set.empty l (** [instance_from_named_context Ω] builds an instance [args] such that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it gives [Var id1, Var id3]. All [idj] are supposed distinct. *) - let to_instance = + let to_instance mk l = let filter = function - | Declaration.LocalAssum (id, _) -> Some (Constr.mkVar id) + | Declaration.LocalAssum (id, _) -> Some (mk id) | _ -> None in - List.map_filter filter - end + List.map_filter filter l +end -module NamedList = +module Compacted = struct module Declaration = struct - type t = Id.t list * Constr.t option * Constr.t - - let map_constr f (ids, copt, ty as decl) = - let copt' = Option.map f copt in - let ty' = f ty in - if copt == copt' && ty == ty' then decl else (ids, copt', ty') + type ('constr, 'types) pt = + | LocalAssum of Id.t list * 'types + | LocalDef of Id.t list * 'constr * 'types + + type t = (Constr.constr, Constr.types) pt + + let map_constr f = function + | LocalAssum (ids, ty) as decl -> + let ty' = f ty in + if ty == ty' then decl else LocalAssum (ids, ty') + | LocalDef (ids, c, ty) as decl -> + let ty' = f ty in + let c' = f c in + if c == c' && ty == ty' then decl else LocalDef (ids,c',ty') + + let of_named_decl = function + | Named.Declaration.LocalAssum (id,t) -> + LocalAssum ([id],t) + | Named.Declaration.LocalDef (id,v,t) -> + LocalDef ([id],v,t) + + let to_named_context = function + | LocalAssum (ids, t) -> + List.map (fun id -> Named.Declaration.LocalAssum (id,t)) ids + | LocalDef (ids, v, t) -> + List.map (fun id -> Named.Declaration.LocalDef (id,v,t)) ids end + type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list type t = Declaration.t list let fold f l ~init = List.fold_right f l init end - -type section_context = Named.t diff --git a/kernel/context.mli b/kernel/context.mli index b5f3904d22..24e69ebd6e 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -29,111 +29,115 @@ sig module Declaration : sig (* local declaration *) - type t = LocalAssum of Name.t * Constr.t (** name, type *) - | LocalDef of Name.t * Constr.t * Constr.t (** name, value, type *) + type ('constr, 'types) pt = + | LocalAssum of Name.t * 'types (** name, type *) + | LocalDef of Name.t * 'constr * 'types (** name, value, type *) + + type t = (Constr.constr, Constr.types) pt (** Return the name bound by a given declaration. *) - val get_name : t -> Name.t + val get_name : ('c, 't) pt -> Name.t (** Return [Some value] for local-declarations and [None] for local-assumptions. *) - val get_value : t -> Constr.t option + val get_value : ('c, 't) pt -> 'c option (** Return the type of the name bound by a given declaration. *) - val get_type : t -> Constr.t + val get_type : ('c, 't) pt -> 't (** Set the name that is bound by a given declaration. *) - val set_name : Name.t -> t -> t + val set_name : Name.t -> ('c, 't) pt -> ('c, 't) pt (** Set the type of the bound variable in a given declaration. *) - val set_type : Constr.t -> t -> t + val set_type : 't -> ('c, 't) pt -> ('c, 't) pt (** Return [true] iff a given declaration is a local assumption. *) - val is_local_assum : t -> bool + val is_local_assum : ('c, 't) pt -> bool (** Return [true] iff a given declaration is a local definition. *) - val is_local_def : t -> bool + val is_local_def : ('c, 't) pt -> bool (** Check whether any term in a given declaration satisfies a given predicate. *) - val exists : (Constr.t -> bool) -> t -> bool + val exists : ('c -> bool) -> ('c, 'c) pt -> bool (** Check whether all terms in a given declaration satisfy a given predicate. *) - val for_all : (Constr.t -> bool) -> t -> bool + val for_all : ('c -> bool) -> ('c, 'c) pt -> bool (** Check whether the two given declarations are equal. *) - val equal : t -> t -> bool + val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool (** Map the name bound by a given declaration. *) - val map_name : (Name.t -> Name.t) -> t -> t + val map_name : (Name.t -> Name.t) -> ('c, 't) pt -> ('c, 't) pt (** For local assumptions, this function returns the original local assumptions. For local definitions, this function maps the value in the local definition. *) - val map_value : (Constr.t -> Constr.t) -> t -> t + val map_value : ('c -> 'c) -> ('c, 't) pt -> ('c, 't) pt (** Map the type of the name bound by a given declaration. *) - val map_type : (Constr.t -> Constr.t) -> t -> t + val map_type : ('t -> 't) -> ('c, 't) pt -> ('c, 't) pt (** Map all terms in a given declaration. *) - val map_constr : (Constr.t -> Constr.t) -> t -> t + val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt (** Perform a given action on all terms in a given declaration. *) - val iter_constr : (Constr.t -> unit) -> t -> unit + val iter_constr : ('c -> unit) -> ('c, 'c) pt -> unit (** Reduce all terms in a given declaration to a single value. *) - val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a + val fold_constr : ('c -> 'a -> 'a) -> ('c, 'c) pt -> 'a -> 'a - val to_tuple : t -> Name.t * Constr.t option * Constr.t - val of_tuple : Name.t * Constr.t option * Constr.t -> t + val to_tuple : ('c, 't) pt -> Name.t * 'c option * 't end (** Rel-context is represented as a list of declarations. Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list. *) + type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list type t = Declaration.t list (** empty rel-context *) - val empty : t + val empty : ('c, 't) pt (** Return a new rel-context enriched by with a given inner-most declaration. *) - val add : Declaration.t -> t -> t + val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt (** Return the number of {e local declarations} in a given context. *) - val length : t -> int + val length : ('c, 't) pt -> int (** Check whether given two rel-contexts are equal. *) - val equal : t -> t -> bool + val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool (** Return the number of {e local assumptions} in a given rel-context. *) - val nhyps : t -> int + val nhyps : ('c, 't) pt -> int (** Return a declaration designated by a given de Bruijn index. @raise Not_found if the designated de Bruijn index outside the range. *) - val lookup : int -> t -> Declaration.t + val lookup : int -> ('c, 't) pt -> ('c, 't) Declaration.pt (** Map all terms in a given rel-context. *) - val map : (Constr.t -> Constr.t) -> t -> t + val map : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt (** Perform a given action on every declaration in a given rel-context. *) - val iter : (Constr.t -> unit) -> t -> unit + val iter : ('c -> unit) -> ('c, 'c) pt -> unit (** Reduce all terms in a given rel-context to a single value. Innermost declarations are processed first. *) - val fold_inside : ('a -> Declaration.t -> 'a) -> init:'a -> t -> 'a + val fold_inside : ('a -> ('c, 't) Declaration.pt -> 'a) -> init:'a -> ('c, 't) pt -> 'a (** Reduce all terms in a given rel-context to a single value. Outermost declarations are processed first. *) - val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a + val fold_outside : (('c, 't) Declaration.pt -> 'a -> 'a) -> ('c, 't) pt -> init:'a -> 'a (** Map a given rel-context to a list where each {e local assumption} is mapped to [true] and each {e local definition} is mapped to [false]. *) - val to_tags : t -> bool list + val to_tags : ('c, 't) pt -> bool list - (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] + (** [extended_list mk n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] with n = |Δ| and with the {e local definitions} of [Γ] skipped in - [args]. Example: for [x:T, y:=c, z:U] and [n]=2, it gives [Rel 5, Rel 3]. *) - val to_extended_list : int -> t -> Constr.t list + [args] where [mk] is used to build the corresponding variables. + Example: for [x:T, y:=c, z:U] and [n]=2, it gives [mk 5, mk 3]. *) + val to_extended_list : (int -> 'r) -> int -> ('c, 't) pt -> 'r list (** [extended_vect n Γ] does the same, returning instead an array. *) - val to_extended_vect : int -> t -> Constr.t array + val to_extended_vect : (int -> 'r) -> int -> ('c, 't) pt -> 'r array end (** This module represents contexts that can capture non-anonymous variables. @@ -143,118 +147,136 @@ sig (** Representation of {e local declarations}. *) module Declaration : sig - type t = LocalAssum of Id.t * Constr.t (** identifier, type *) - | LocalDef of Id.t * Constr.t * Constr.t (** identifier, value, type *) + type ('constr, 'types) pt = + | LocalAssum of Id.t * 'types (** identifier, type *) + | LocalDef of Id.t * 'constr * 'types (** identifier, value, type *) + + type t = (Constr.constr, Constr.types) pt (** Return the identifier bound by a given declaration. *) - val get_id : t -> Id.t + val get_id : ('c, 't) pt -> Id.t (** Return [Some value] for local-declarations and [None] for local-assumptions. *) - val get_value : t -> Constr.t option + val get_value : ('c, 't) pt -> 'c option (** Return the type of the name bound by a given declaration. *) - val get_type : t -> Constr.t + val get_type : ('c, 't) pt -> 't (** Set the identifier that is bound by a given declaration. *) - val set_id : Id.t -> t -> t + val set_id : Id.t -> ('c, 't) pt -> ('c, 't) pt (** Set the type of the bound variable in a given declaration. *) - val set_type : Constr.t -> t -> t + val set_type : 't -> ('c, 't) pt -> ('c, 't) pt (** Return [true] iff a given declaration is a local assumption. *) - val is_local_assum : t -> bool + val is_local_assum : ('c, 't) pt -> bool (** Return [true] iff a given declaration is a local definition. *) - val is_local_def : t -> bool + val is_local_def : ('c, 't) pt -> bool (** Check whether any term in a given declaration satisfies a given predicate. *) - val exists : (Constr.t -> bool) -> t -> bool + val exists : ('c -> bool) -> ('c, 'c) pt -> bool (** Check whether all terms in a given declaration satisfy a given predicate. *) - val for_all : (Constr.t -> bool) -> t -> bool + val for_all : ('c -> bool) -> ('c, 'c) pt -> bool (** Check whether the two given declarations are equal. *) - val equal : t -> t -> bool + val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool (** Map the identifier bound by a given declaration. *) - val map_id : (Id.t -> Id.t) -> t -> t + val map_id : (Id.t -> Id.t) -> ('c, 't) pt -> ('c, 't) pt (** For local assumptions, this function returns the original local assumptions. For local definitions, this function maps the value in the local definition. *) - val map_value : (Constr.t -> Constr.t) -> t -> t + val map_value : ('c -> 'c) -> ('c, 't) pt -> ('c, 't) pt (** Map the type of the name bound by a given declaration. *) - val map_type : (Constr.t -> Constr.t) -> t -> t + val map_type : ('t -> 't) -> ('c, 't) pt -> ('c, 't) pt (** Map all terms in a given declaration. *) - val map_constr : (Constr.t -> Constr.t) -> t -> t + val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt (** Perform a given action on all terms in a given declaration. *) - val iter_constr : (Constr.t -> unit) -> t -> unit + val iter_constr : ('c -> unit) -> ('c, 'c) pt -> unit (** Reduce all terms in a given declaration to a single value. *) - val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a + val fold_constr : ('c -> 'a -> 'a) -> ('c, 'c) pt -> 'a -> 'a + + val to_tuple : ('c, 't) pt -> Id.t * 'c option * 't + val of_tuple : Id.t * 'c option * 't -> ('c, 't) pt - val to_tuple : t -> Id.t * Constr.t option * Constr.t - val of_tuple : Id.t * Constr.t option * Constr.t -> t + (** Convert [Rel.Declaration.t] value to the corresponding [Named.Declaration.t] value. + The function provided as the first parameter determines how to translate "names" to "ids". *) + val of_rel_decl : (Name.t -> Id.t) -> ('c, 't) Rel.Declaration.pt -> ('c, 't) pt + + (** Convert [Named.Declaration.t] value to the corresponding [Rel.Declaration.t] value. *) + (* TODO: Move this function to [Rel.Declaration] module and rename it to [of_named]. *) + val to_rel_decl : ('c, 't) pt -> ('c, 't) Rel.Declaration.pt end - (** Rel-context is represented as a list of declarations. + (** Named-context is represented as a list of declarations. Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list. *) + type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list type t = Declaration.t list (** empty named-context *) - val empty : t + val empty : ('c, 't) pt - (** Return a new rel-context enriched by with a given inner-most declaration. *) - val add : Declaration.t -> t -> t + (** Return a new named-context enriched by with a given inner-most declaration. *) + val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt (** Return the number of {e local declarations} in a given named-context. *) - val length : t -> int + val length : ('c, 't) pt -> int (** Return a declaration designated by an identifier of the variable bound in that declaration. @raise Not_found if the designated identifier is not bound in a given named-context. *) - val lookup : Id.t -> t -> Declaration.t + val lookup : Id.t -> ('c, 't) pt -> ('c, 't) Declaration.pt - (** Check whether given two rel-contexts are equal. *) - val equal : t -> t -> bool + (** Check whether given two named-contexts are equal. *) + val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool (** Map all terms in a given named-context. *) - val map : (Constr.t -> Constr.t) -> t -> t + val map : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt (** Perform a given action on every declaration in a given named-context. *) - val iter : (Constr.t -> unit) -> t -> unit + val iter : ('c -> unit) -> ('c, 'c) pt -> unit (** Reduce all terms in a given named-context to a single value. Innermost declarations are processed first. *) - val fold_inside : ('a -> Declaration.t -> 'a) -> init:'a -> t -> 'a + val fold_inside : ('a -> ('c, 't) Declaration.pt -> 'a) -> init:'a -> ('c, 't) pt -> 'a (** Reduce all terms in a given named-context to a single value. Outermost declarations are processed first. *) - val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a + val fold_outside : (('c, 't) Declaration.pt -> 'a -> 'a) -> ('c, 't) pt -> init:'a -> 'a (** Return the set of all identifiers bound in a given named-context. *) - val to_vars : t -> Id.Set.t + val to_vars : ('c, 't) pt -> Id.Set.t - (** [instance_from_named_context Ω] builds an instance [args] such - that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local + (** [to_instance Ω] builds an instance [args] such + that [Ω ⊢ args:Ω] where [Ω] is a named-context and with the local definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it gives [Var id1, Var id3]. All [idj] are supposed distinct. *) - val to_instance : t -> Constr.t list + val to_instance : (Id.t -> 'r) -> ('c, 't) pt -> 'r list end -module NamedList : +module Compacted : sig module Declaration : sig - type t = Id.t list * Constr.t option * Constr.t - val map_constr : (Constr.t -> Constr.t) -> t -> t + type ('constr, 'types) pt = + | LocalAssum of Id.t list * 'types + | LocalDef of Id.t list * 'constr * 'types + + type t = (Constr.constr, Constr.types) pt + + val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt + val of_named_decl : ('c, 't) Named.Declaration.pt -> ('c, 't) pt + val to_named_context : ('c, 't) pt -> ('c, 't) Named.pt end + type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list type t = Declaration.t list - val fold : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a + val fold : (('c, 't) Declaration.pt -> 'a -> 'a) -> ('c, 't) pt -> init:'a -> 'a end - -type section_context = Named.t diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 3f1cf92487..4533169804 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -71,7 +71,7 @@ let set_strategy ({ var_opacity; cst_opacity } as oracle) k l = | _ -> Cpred.add c oracle.cst_trstate in { oracle with cst_opacity; cst_trstate; } - | RelKey _ -> CErrors.error "set_strategy: RelKey" + | RelKey _ -> CErrors.user_err Pp.(str "set_strategy: RelKey") let fold_strategy f { var_opacity; cst_opacity; } accu = let fvar id lvl accu = f (VarKey id) lvl accu in diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 1345991503..4deadff0a7 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -21,10 +21,12 @@ open Declarations open Environ open Univ +module NamedDecl = Context.Named.Declaration + (*s Cooking the constants. *) let pop_dirpath p = match DirPath.repr p with - | [] -> anomaly ~label:"dirpath_prefix" (Pp.str "empty dirpath") + | [] -> anomaly ~label:"dirpath_prefix" (Pp.str "empty dirpath.") | _::l -> DirPath.make l let pop_mind kn = @@ -152,7 +154,7 @@ type inline = bool type result = constant_def * constant_type * projection_body option * bool * constant_universes * inline - * Context.section_context option + * Context.Named.t option let on_body ml hy f = function | Undef _ as x -> x @@ -189,21 +191,24 @@ let lift_univs cb subst = subst, Univ.UContext.make (inst,cstrs') else subst, cb.const_universes -let cook_constant env { from = cb; info } = +let cook_constant ~hcons env { from = cb; info } = let { Opaqueproof.modlist; abstract } = info in let cache = RefTable.create 13 in let abstract, usubst, abs_ctx = abstract in let usubst, univs = lift_univs cb usubst in let expmod = expmod_constr_subst cache modlist usubst in let hyps = Context.Named.map expmod abstract in + let map c = + let c = abstract_constant_body (expmod c) hyps in + if hcons then hcons_constr c else c + in let body = on_body modlist (hyps, usubst, abs_ctx) - (fun c -> abstract_constant_body (expmod c) hyps) + map cb.const_body in let const_hyps = Context.Named.fold_outside (fun decl hyps -> - let open Context.Named.Declaration in - List.filter (fun decl' -> not (Id.equal (get_id decl) (get_id decl'))) + List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl'))) hyps) hyps ~init:cb.const_hyps in let typ = match cb.const_type with diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 327e697d23..7d47eba23e 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -19,9 +19,9 @@ type inline = bool type result = constant_def * constant_type * projection_body option * bool * constant_universes * inline - * Context.section_context option + * Context.Named.t option -val cook_constant : env -> recipe -> result +val cook_constant : hcons:bool -> env -> recipe -> result val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr (** {6 Utility functions used in module [Discharge]. } *) diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index c27cb04870..40595f944c 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -22,6 +22,8 @@ open Declarations open Pre_env open Cbytegen +module NamedDecl = Context.Named.Declaration +module RelDecl = Context.Rel.Declaration external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code" external eval_tcode : tcode -> values array -> values = "coq_eval_tcode" @@ -189,18 +191,14 @@ and slot_for_fv env fv = let nv = Pre_env.lookup_named_val id env in begin match force_lazy_val nv with | None -> - let open Context.Named in - let open Declaration in - env |> Pre_env.lookup_named id |> get_value |> fill_fv_cache nv id val_of_named idfun + env |> Pre_env.lookup_named id |> NamedDecl.get_value |> fill_fv_cache nv id val_of_named idfun | Some (v, _) -> v end | FVrel i -> let rv = Pre_env.lookup_rel_val i env in begin match force_lazy_val rv with | None -> - let open Context.Rel in - let open Declaration in - env.env_rel_context |> lookup i |> get_value |> fill_fv_cache rv i val_of_rel env_of_rel + env.env_rel_context |> Context.Rel.lookup i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel | Some (v, _) -> v end | FVuniv_var idu -> diff --git a/kernel/declarations.mli b/kernel/declarations.ml index f89773fcc5..71e228b19c 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.ml @@ -58,10 +58,11 @@ type projection_body = { proj_body : constr; (* For compatibility with VMs only, the match version *) } +(* Global declarations (i.e. constants) can be either: *) type constant_def = - | Undef of inline - | Def of constr Mod_subst.substituted - | OpaqueDef of Opaqueproof.opaque + | Undef of inline (** a global assumption *) + | Def of constr Mod_subst.substituted (** or a transparent global definition *) + | OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *) type constant_universes = Univ.universe_context @@ -76,9 +77,9 @@ type typing_flags = { } (* some contraints are in constant_constraints, some other may be in - * the OpaueDef *) + * the OpaqueDef *) type constant_body = { - const_hyps : Context.section_context; (** New: younger hyp at top *) + const_hyps : Context.Named.t; (** New: younger hyp at top *) const_body : constant_def; const_type : constant_type; const_body_code : Cemitcodes.to_patch_substituted option; @@ -177,7 +178,7 @@ type mutual_inductive_body = { mind_ntypes : int; (** Number of types in the block *) - mind_hyps : Context.section_context; (** Section hypotheses on which the block depends *) + mind_hyps : Context.Named.t; (** Section hypotheses on which the block depends *) mind_nparams : int; (** Number of expected parameters including non-uniform ones (i.e. length of mind_params_ctxt w/o let-in) *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 211e5e062a..0a822d6fad 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -9,7 +9,8 @@ open Declarations open Mod_subst open Util -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration (** Operations concernings types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) @@ -94,7 +95,7 @@ let is_opaque cb = match cb.const_body with (** {7 Constant substitutions } *) let subst_rel_declaration sub = - map_constr (subst_mps sub) + RelDecl.map_constr (subst_mps sub) let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) @@ -146,7 +147,7 @@ let subst_const_body sub cb = themselves. But would it really bring substantial gains ? *) let hcons_rel_decl = - map_type Term.hcons_types % map_value Term.hcons_constr % map_name Names.Name.hcons + RelDecl.map_name Names.Name.hcons %> RelDecl.map_value Term.hcons_constr %> RelDecl.map_type Term.hcons_types let hcons_rel_context l = List.smartmap hcons_rel_decl l diff --git a/kernel/entries.mli b/kernel/entries.mli index 5287a009e5..1e07c96909 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -61,7 +61,7 @@ type 'a const_entry_body = 'a proof_output Future.computation type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) - const_entry_secctx : Context.section_context option; + const_entry_secctx : Context.Named.t option; (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : types option; @@ -73,7 +73,7 @@ type 'a definition_entry = { type inline = int option (* inlining level, None for no inlining *) type parameter_entry = - Context.section_context option * bool * types Univ.in_universe_context * inline + Context.Named.t option * bool * types Univ.in_universe_context * inline type projection_entry = { proj_entry_ind : mutual_inductive; diff --git a/kernel/environ.ml b/kernel/environ.ml index 16ddfac64b..5727bf2ea1 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -120,7 +120,7 @@ let lookup_named = lookup_named let lookup_named_val id ctxt = fst (Id.Map.find id ctxt.env_named_map) let eq_named_context_val c1 c2 = - c1 == c2 || Context.Named.equal (named_context_of_val c1) (named_context_of_val c2) + c1 == c2 || Context.Named.equal Constr.equal (named_context_of_val c1) (named_context_of_val c2) (* A local const is evaluable if it is defined *) @@ -342,7 +342,7 @@ let template_polymorphic_pconstant (cst,u) env = let lookup_projection cst env = match (lookup_constant (Projection.constant cst) env).const_proj with | Some pb -> pb - | None -> anomaly (Pp.str "lookup_projection: constant is not a projection") + | None -> anomaly (Pp.str "lookup_projection: constant is not a projection.") let is_projection cst env = match (lookup_constant cst env).const_proj with @@ -413,7 +413,7 @@ let global_vars_set env constr = Id.Set.union (vars_of_global env c) acc | _ -> acc in - fold_constr filtrec acc c + Term.fold_constr filtrec acc c in filtrec Id.Set.empty constr @@ -469,9 +469,11 @@ let lookup_modtype mp env = (*s Judgments. *) -type unsafe_judgment = { - uj_val : constr; - uj_type : types } +type ('constr, 'types) punsafe_judgment = { + uj_val : 'constr; + uj_type : 'types } + +type unsafe_judgment = (constr, types) punsafe_judgment let make_judge v tj = { uj_val = v; @@ -480,10 +482,12 @@ let make_judge v tj = let j_val j = j.uj_val let j_type j = j.uj_type -type unsafe_type_judgment = { - utj_val : constr; +type 'types punsafe_type_judgment = { + utj_val : 'types; utj_type : sorts } +type unsafe_type_judgment = types punsafe_type_judgment + (*s Compilation of global declaration *) let compile_constant_body = Cbytegen.compile_constant_body false @@ -542,7 +546,7 @@ let register env field entry = | KInt31 (grp, Int31Type) -> let i31c = match kind_of_term entry with | Ind i31t -> mkConstructUi (i31t, 1) - | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type") + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.") in register_one (register_one env (KInt31 (grp,Int31Constructor)) i31c) field entry | field -> register_one env field entry @@ -588,7 +592,7 @@ fun rk value field -> let int31_op_from_const n op prim = match kind_of_term value with | Const kn -> int31_op n op prim kn - | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant") + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant.") in let int31_binop_from_const op prim = int31_op_from_const 2 op prim in let int31_unop_from_const op prim = int31_op_from_const 1 op prim in @@ -600,20 +604,20 @@ fun rk value field -> match field with | KInt31 (grp, Int31Type) -> Retroknowledge.find rk (KInt31 (grp,Int31Bits)) | _ -> anomaly ~label:"Environ.register" - (Pp.str "add_int31_decompilation_from_type called with an abnormal field") + (Pp.str "add_int31_decompilation_from_type called with an abnormal field.") in let i31bit_type = match kind_of_term int31bit with | Ind (i31bit_type,_) -> i31bit_type | _ -> anomaly ~label:"Environ.register" - (Pp.str "Int31Bits should be an inductive type") + (Pp.str "Int31Bits should be an inductive type.") in let int31_decompilation = match kind_of_term value with | Ind (i31t,_) -> constr_of_int31 i31t i31bit_type | _ -> anomaly ~label:"Environ.register" - (Pp.str "should be an inductive type") + (Pp.str "should be an inductive type.") in { empty_reactive_info with vm_decompile_const = Some int31_decompilation; diff --git a/kernel/environ.mli b/kernel/environ.mli index 6ac00088b3..b7431dbe5f 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -231,25 +231,28 @@ val vars_of_global : env -> constr -> Id.Set.t val really_needed : env -> Id.Set.t -> Id.Set.t (** like [really_needed] but computes a well ordered named context *) -val keep_hyps : env -> Id.Set.t -> Context.section_context +val keep_hyps : env -> Id.Set.t -> Context.Named.t (** {5 Unsafe judgments. } We introduce here the pre-type of judgments, which is actually only a datatype to store a term with its type and the type of its type. *) -type unsafe_judgment = { - uj_val : constr; - uj_type : types } +type ('constr, 'types) punsafe_judgment = { + uj_val : 'constr; + uj_type : 'types } -val make_judge : constr -> types -> unsafe_judgment -val j_val : unsafe_judgment -> constr -val j_type : unsafe_judgment -> types +type unsafe_judgment = (constr, types) punsafe_judgment -type unsafe_type_judgment = { - utj_val : constr; +val make_judge : 'constr -> 'types -> ('constr, 'types) punsafe_judgment +val j_val : ('constr, 'types) punsafe_judgment -> 'constr +val j_type : ('constr, 'types) punsafe_judgment -> 'types + +type 'types punsafe_type_judgment = { + utj_val : 'types; utj_type : sorts } +type unsafe_type_judgment = types punsafe_type_judgment (** {6 Compilation of global declaration } *) diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml deleted file mode 100644 index bd91c689d2..0000000000 --- a/kernel/fast_typeops.ml +++ /dev/null @@ -1,463 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open CErrors -open Util -open Names -open Univ -open Term -open Vars -open Declarations -open Environ -open Reduction -open Inductive -open Type_errors - -let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y - -let conv_leq_vecti env v1 v2 = - Array.fold_left2_i - (fun i _ t1 t2 -> - try conv_leq false env t1 t2 - with NotConvertible -> raise (NotConvertibleVect i)) - () - v1 - v2 - -let check_constraints cst env = - if Environ.check_constraints cst env then () - else error_unsatisfied_constraints env cst - -(* This should be a type (a priori without intention to be an assumption) *) -let type_judgment env c t = - match kind_of_term(whd_all env t) with - | Sort s -> {utj_val = c; utj_type = s } - | _ -> error_not_type env (make_judge c t) - -let check_type env c t = - match kind_of_term(whd_all env t) with - | Sort s -> s - | _ -> error_not_type env (make_judge c t) - -(* This should be a type intended to be assumed. The error message is *) -(* not as useful as for [type_judgment]. *) -let assumption_of_judgment env t ty = - try let _ = check_type env t ty in t - with TypeError _ -> - error_assumption env (make_judge t ty) - -(************************************************) -(* Incremental typing rules: builds a typing judgment given the *) -(* judgments for the subterms. *) - -(*s Type of sorts *) - -(* Prop and Set *) - -let judge_of_prop = mkSort type1_sort - -let judge_of_prop_contents _ = judge_of_prop - -(* Type of Type(i). *) - -let judge_of_type u = - let uu = Universe.super u in - mkType uu - -(*s Type of a de Bruijn index. *) - -let judge_of_relative env n = - try - let open Context.Rel.Declaration in - env |> lookup_rel n |> get_type |> lift n - with Not_found -> - error_unbound_rel env n - -(* Type of variables *) -let judge_of_variable env id = - try named_type id env - with Not_found -> - error_unbound_var env id - -(* Management of context of variables. *) - -(* Checks if a context of variables can be instantiated by the - variables of the current env *) -(* TODO: check order? *) -let check_hyps_inclusion env f c sign = - Context.Named.fold_outside - (fun decl () -> - let open Context.Named.Declaration in - let id = get_id decl in - let ty1 = get_type decl in - try - let ty2 = named_type id env in - if not (eq_constr ty2 ty1) then raise Exit - with Not_found | Exit -> - error_reference_variables env id (f c)) - sign - ~init:() - -(* Instantiation of terms on real arguments. *) - -(* Make a type polymorphic if an arity *) - -(* Type of constants *) - - -let type_of_constant_knowing_parameters_arity env t paramtyps = - match t with - | RegularArity t -> t - | TemplateArity (sign,ar) -> - let ctx = List.rev sign in - let ctx,s = instantiate_universes env ctx ar paramtyps in - mkArity (List.rev ctx,s) - -let type_of_constant_knowing_parameters env cst paramtyps = - let ty, cu = constant_type env cst in - type_of_constant_knowing_parameters_arity env ty paramtyps, cu - -let judge_of_constant_knowing_parameters env (kn,u as cst) args = - let cb = lookup_constant kn env in - let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in - let ty, cu = type_of_constant_knowing_parameters env cst args in - let () = check_constraints cu env in - ty - -let judge_of_constant env cst = - judge_of_constant_knowing_parameters env cst [||] - -(* Type of a lambda-abstraction. *) - -(* [judge_of_abstraction env name var j] implements the rule - - env, name:typ |- j.uj_val:j.uj_type env, |- (name:typ)j.uj_type : s - ----------------------------------------------------------------------- - env |- [name:typ]j.uj_val : (name:typ)j.uj_type - - Since all products are defined in the Calculus of Inductive Constructions - and no upper constraint exists on the sort $s$, we don't need to compute $s$ -*) - -let judge_of_abstraction env name var ty = - mkProd (name, var, ty) - -(* Type of an application. *) - -let make_judgev c t = - Array.map2 make_judge c t - -let judge_of_apply env func funt argsv argstv = - let len = Array.length argsv in - let rec apply_rec i typ = - if Int.equal i len then typ - else - (match kind_of_term (whd_all env typ) with - | Prod (_,c1,c2) -> - let arg = argsv.(i) and argt = argstv.(i) in - (try - let () = conv_leq false env argt c1 in - apply_rec (i+1) (subst1 arg c2) - with NotConvertible -> - error_cant_apply_bad_type env - (i+1,c1,argt) - (make_judge func funt) - (make_judgev argsv argstv)) - - | _ -> - error_cant_apply_not_functional env - (make_judge func funt) - (make_judgev argsv argstv)) - in apply_rec 0 funt - -(* Type of product *) - -let sort_of_product env domsort rangsort = - match (domsort, rangsort) with - (* Product rule (s,Prop,Prop) *) - | (_, Prop Null) -> rangsort - (* Product rule (Prop/Set,Set,Set) *) - | (Prop _, Prop Pos) -> rangsort - (* Product rule (Type,Set,?) *) - | (Type u1, Prop Pos) -> - if is_impredicative_set env then - (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) - rangsort - else - (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) - Type (Universe.sup Universe.type0 u1) - (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Pos, Type u2) -> Type (Universe.sup Universe.type0 u2) - (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Null, Type _) -> rangsort - (* Product rule (Type_i,Type_i,Type_i) *) - | (Type u1, Type u2) -> Type (Universe.sup u1 u2) - -(* [judge_of_product env name (typ1,s1) (typ2,s2)] implements the rule - - env |- typ1:s1 env, name:typ1 |- typ2 : s2 - ------------------------------------------------------------------------- - s' >= (s1,s2), env |- (name:typ)j.uj_val : s' - - where j.uj_type is convertible to a sort s2 -*) -let judge_of_product env name s1 s2 = - let s = sort_of_product env s1 s2 in - mkSort s - -(* Type of a type cast *) - -(* [judge_of_cast env (c,typ1) (typ2,s)] implements the rule - - env |- c:typ1 env |- typ2:s env |- typ1 <= typ2 - --------------------------------------------------------------------- - env |- c:typ2 -*) - -let judge_of_cast env c ct k expected_type = - try - match k with - | VMcast -> - vm_conv CUMUL env ct expected_type - | DEFAULTcast -> - default_conv ~l2r:false CUMUL env ct expected_type - | REVERTcast -> - default_conv ~l2r:true CUMUL env ct expected_type - | NATIVEcast -> - let sigma = Nativelambda.empty_evars in - Nativeconv.native_conv CUMUL sigma env ct expected_type - with NotConvertible -> - error_actual_type env (make_judge c ct) expected_type - -(* Inductive types. *) - -(* The type is parametric over the uniform parameters whose conclusion - is in Type; to enforce the internal constraints between the - parameters and the instances of Type occurring in the type of the - constructors, we use the level variables _statically_ assigned to - the conclusions of the parameters as mediators: e.g. if a parameter - has conclusion Type(alpha), static constraints of the form alpha<=v - exist between alpha and the Type's occurring in the constructor - types; when the parameters is finally instantiated by a term of - conclusion Type(u), then the constraints u<=alpha is computed in - the App case of execute; from this constraints, the expected - dynamic constraints of the form u<=v are enforced *) - -let judge_of_inductive_knowing_parameters env (ind,u as indu) args = - let (mib,mip) as spec = lookup_mind_specif env ind in - check_hyps_inclusion env mkIndU indu mib.mind_hyps; - let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters - env (spec,u) args - in - check_constraints cst env; - t - -let judge_of_inductive env (ind,u as indu) = - let (mib,mip) = lookup_mind_specif env ind in - check_hyps_inclusion env mkIndU indu mib.mind_hyps; - let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in - check_constraints cst env; - t - -(* Constructors. *) - -let judge_of_constructor env (c,u as cu) = - let _ = - let ((kn,_),_) = c in - let mib = lookup_mind kn env in - check_hyps_inclusion env mkConstructU cu mib.mind_hyps in - let specif = lookup_mind_specif env (inductive_of_constructor c) in - let t,cst = constrained_type_of_constructor cu specif in - let () = check_constraints cst env in - t - -(* Case. *) - -let check_branch_types env (ind,u) c ct lft explft = - try conv_leq_vecti env lft explft - with - NotConvertibleVect i -> - error_ill_formed_branch env c ((ind,i+1),u) lft.(i) explft.(i) - | Invalid_argument _ -> - error_number_branches env (make_judge c ct) (Array.length explft) - -let judge_of_case env ci p pt c ct lf lft = - let (pind, _ as indspec) = - try find_rectype env ct - with Not_found -> error_case_not_inductive env (make_judge c ct) in - let _ = check_case_info env pind ci in - let (bty,rslty) = - type_case_branches env indspec (make_judge p pt) c in - let () = check_branch_types env pind c ct lft bty in - rslty - -let judge_of_projection env p c ct = - let pb = lookup_projection p env in - let (ind,u), args = - try find_rectype env ct - with Not_found -> error_case_not_inductive env (make_judge c ct) - in - assert(eq_mind pb.proj_ind (fst ind)); - let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in - substl (c :: List.rev args) ty - - -(* Fixpoints. *) - -(* Checks the type of a general (co)fixpoint, i.e. without checking *) -(* the specific guard condition. *) - -let type_fixpoint env lna lar vdef vdeft = - let lt = Array.length vdeft in - assert (Int.equal (Array.length lar) lt); - try - conv_leq_vecti env vdeft (Array.map (fun ty -> lift lt ty) lar) - with NotConvertibleVect i -> - error_ill_typed_rec_body env i lna (make_judgev vdef vdeft) lar - -(************************************************************************) -(************************************************************************) - -(* The typing machine. *) - (* ATTENTION : faudra faire le typage du contexte des Const, - Ind et Constructsi un jour cela devient des constructions - arbitraires et non plus des variables *) -let rec execute env cstr = - let open Context.Rel.Declaration in - match kind_of_term cstr with - (* Atomic terms *) - | Sort (Prop c) -> - judge_of_prop_contents c - - | Sort (Type u) -> - judge_of_type u - - | Rel n -> - judge_of_relative env n - - | Var id -> - judge_of_variable env id - - | Const c -> - judge_of_constant env c - - | Proj (p, c) -> - let ct = execute env c in - judge_of_projection env p c ct - - (* Lambda calculus operators *) - | App (f,args) -> - let argst = execute_array env args in - let ft = - match kind_of_term f with - | Ind ind when Environ.template_polymorphic_pind ind env -> - (* Template sort-polymorphism of inductive types *) - let args = Array.map (fun t -> lazy t) argst in - judge_of_inductive_knowing_parameters env ind args - | Const cst when Environ.template_polymorphic_pconstant cst env -> - (* Template sort-polymorphism of constants *) - let args = Array.map (fun t -> lazy t) argst in - judge_of_constant_knowing_parameters env cst args - | _ -> - (* Full or no sort-polymorphism *) - execute env f - in - - judge_of_apply env f ft args argst - - | Lambda (name,c1,c2) -> - let _ = execute_is_type env c1 in - let env1 = push_rel (LocalAssum (name,c1)) env in - let c2t = execute env1 c2 in - judge_of_abstraction env name c1 c2t - - | Prod (name,c1,c2) -> - let vars = execute_is_type env c1 in - let env1 = push_rel (LocalAssum (name,c1)) env in - let vars' = execute_is_type env1 c2 in - judge_of_product env name vars vars' - - | LetIn (name,c1,c2,c3) -> - let c1t = execute env c1 in - let _c2s = execute_is_type env c2 in - let _ = judge_of_cast env c1 c1t DEFAULTcast c2 in - let env1 = push_rel (LocalDef (name,c1,c2)) env in - let c3t = execute env1 c3 in - subst1 c1 c3t - - | Cast (c,k,t) -> - let ct = execute env c in - let _ts = execute_type env t in - let _ = judge_of_cast env c ct k t in - t - - (* Inductive types *) - | Ind ind -> - judge_of_inductive env ind - - | Construct c -> - judge_of_constructor env c - - | Case (ci,p,c,lf) -> - let ct = execute env c in - let pt = execute env p in - let lft = execute_array env lf in - judge_of_case env ci p pt c ct lf lft - - | Fix ((vn,i as vni),recdef) -> - let (fix_ty,recdef') = execute_recdef env recdef i in - let fix = (vni,recdef') in - check_fix env fix; fix_ty - - | CoFix (i,recdef) -> - let (fix_ty,recdef') = execute_recdef env recdef i in - let cofix = (i,recdef') in - check_cofix env cofix; fix_ty - - (* Partial proofs: unsupported by the kernel *) - | Meta _ -> - anomaly (Pp.str "the kernel does not support metavariables") - - | Evar _ -> - anomaly (Pp.str "the kernel does not support existential variables") - -and execute_is_type env constr = - let t = execute env constr in - check_type env constr t - -and execute_type env constr = - let t = execute env constr in - type_judgment env constr t - -and execute_recdef env (names,lar,vdef) i = - let lart = execute_array env lar in - let lara = Array.map2 (assumption_of_judgment env) lar lart in - let env1 = push_rec_types (names,lara,vdef) env in - let vdeft = execute_array env1 vdef in - let () = type_fixpoint env1 names lara vdef vdeft in - (lara.(i),(names,lara,vdef)) - -and execute_array env = Array.map (execute env) - -(* Derived functions *) -let infer env constr = - let t = execute env constr in - make_judge constr t - -let infer = - if Flags.profile then - let infer_key = Profile.declare_profile "Fast_infer" in - Profile.profile2 infer_key (fun b c -> infer b c) - else (fun b c -> infer b c) - -let infer_type env constr = - execute_type env constr - -let infer_v env cv = - let jv = execute_array env cv in - make_judgev cv jv diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli deleted file mode 100644 index 41cff607e7..0000000000 --- a/kernel/fast_typeops.mli +++ /dev/null @@ -1,24 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Term -open Environ -open Declarations - -(** {6 Typing functions (not yet tagged as safe) } - - They return unsafe judgments that are "in context" of a set of - (local) universe variables (the ones that appear in the term) - and associated constraints. In case of polymorphic definitions, - these variables and constraints will be generalized. - *) - - -val infer : env -> constr -> unsafe_judgment -val infer_v : env -> constr array -> unsafe_judgment array -val infer_type : env -> types -> unsafe_type_judgment diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index de97268b37..1e13239bfc 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -214,7 +214,7 @@ let param_ccls paramsctxt = *) let typecheck_inductive env mie = let () = match mie.mind_entry_inds with - | [] -> anomaly (Pp.str "empty inductive types declaration") + | [] -> anomaly (Pp.str "empty inductive types declaration.") | _ -> () in (* Check unicity of names *) @@ -313,7 +313,7 @@ let typecheck_inductive env mie = anomaly ~label:"check_inductive" (Pp.str"Incorrect universe " ++ Universe.pr defu ++ Pp.str " declared for inductive type, inferred level is " - ++ Universe.pr infu) + ++ Universe.pr infu ++ Pp.str ".") in RegularArity (not is_natural,full_arity,defu) in @@ -333,7 +333,7 @@ let typecheck_inductive env mie = anomaly ~label:"check_inductive" (Pp.str"Incorrect universe " ++ Universe.pr u ++ Pp.str " declared for inductive type, inferred level is " - ++ Universe.pr clev) + ++ Universe.pr clev ++ Pp.str ".") else TemplateArity (param_ccls paramsctxt, infu) | _ (* Not an explicit occurrence of Type *) -> @@ -389,11 +389,11 @@ let failwith_non_pos n ntypes c = let failwith_non_pos_vect n ntypes v = Array.iter (failwith_non_pos n ntypes) v; - anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur") + anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur.") let failwith_non_pos_list n ntypes l = List.iter (failwith_non_pos n ntypes) l; - anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur") + anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur.") (* Check the inductive type is called with the expected parameters *) (* [n] is the index of the last inductive type in [env] *) @@ -734,7 +734,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params matching with a parameter context. *) let indty, paramsletsubst = (* [ty] = [Ind inst] is typed in context [params] *) - let inst = Context.Rel.to_extended_vect 0 paramslet in + let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in let ty = mkApp (mkIndU indu, inst) in (* [Ind inst] is typed in context [params-wo-let] *) let inst' = rel_list 0 nparamargs in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 3c4c2796ee..f3b03252db 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -25,7 +25,7 @@ type mind_specif = mutual_inductive_body * one_inductive_body let lookup_mind_specif env (kn,tyi) = let mib = Environ.lookup_mind kn env in if tyi >= Array.length mib.mind_packets then - error "Inductive.lookup_mind_specif: invalid inductive index"; + user_err Pp.(str "Inductive.lookup_mind_specif: invalid inductive index"); (mib, mib.mind_packets.(tyi)) let find_rectype env c = @@ -75,7 +75,7 @@ let constructor_instantiate mind u mib c = let instantiate_params full t u args sign = let fail () = - anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in + anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch.") in let (rem_args, subs, ty) = Context.Rel.fold_outside (fun decl (largs,subs,ty) -> @@ -247,7 +247,7 @@ let type_of_constructor (cstr, u) (mib,mip) = let specif = mip.mind_user_lc in let i = index_of_constructor cstr in let nconstr = Array.length mip.mind_consnames in - if i > nconstr then error "Not enough constructors in the type."; + if i > nconstr then user_err Pp.(str "Not enough constructors in the type."); constructor_instantiate (fst ind) u mib specif.(i-1) let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) = @@ -297,7 +297,7 @@ let build_dependent_inductive ind (_,mip) params = applist (mkIndU ind, List.map (lift mip.mind_nrealdecls) params - @ Context.Rel.to_extended_list 0 realargs) + @ Context.Rel.to_extended_list mkRel 0 realargs) (* This exception is local *) exception LocalArity of (sorts_family * sorts_family * arity_error) option @@ -355,7 +355,7 @@ let build_branches_type (ind,u) (_,mip as specif) params p = let (lparams,vargs) = List.chop (inductive_params specif) allargs in let cargs = let cstr = ith_constructor_of_inductive ind (i+1) in - let dep_cstr = applist (mkConstructU (cstr,u),lparams@(Context.Rel.to_extended_list 0 cstrsign)) in + let dep_cstr = applist (mkConstructU (cstr,u),lparams@(Context.Rel.to_extended_list mkRel 0 cstrsign)) in vargs @ [dep_cstr] in let base = lambda_appvect_assum (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in it_mkProd_or_LetIn base cstrsign in @@ -1023,7 +1023,7 @@ let check_one_fix renv recpos trees def = check_rec_call renv [] a; let renv' = push_var_renv renv (x,a) in check_nested_fix_body renv' (decr-1) recArgsDecrArg b - | _ -> anomaly (Pp.str "Not enough abstractions in fix body") + | _ -> anomaly (Pp.str "Not enough abstractions in fix body.") in check_rec_call renv [] def @@ -1039,7 +1039,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = || not (Int.equal (Array.length names) nbfix) || bodynum < 0 || bodynum >= nbfix - then anomaly (Pp.str "Ill-formed fix term"); + then anomaly (Pp.str "Ill-formed fix term."); let fixenv = push_rec_types recdef env in let vdefj = judgment_of_fixpoint recdef in let raise_err env i err = @@ -1061,7 +1061,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = raise_err env i (RecursionNotOnInductiveType a) in (mind, (env', b)) else check_occur env' (n+1) b - else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call") + else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.") | _ -> raise_err env i NotEnoughAbstractionInFixBody in check_occur fixenv 1 def in (* Do it on every fixpoint *) @@ -1100,7 +1100,7 @@ let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; exception CoFixGuardError of env * guard_error let anomaly_ill_typed () = - anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor") + anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor.") let rec codomain_is_coind env c = let b = whd_all env c in diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 15f213ce9c..2f49982ce2 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -32,7 +32,6 @@ Type_errors Modops Inductive Typeops -Fast_typeops Indtypes Cooking Term_typing @@ -43,3 +42,4 @@ Safe_typing Vm Csymtable Vconv +Declarations diff --git a/kernel/modops.ml b/kernel/modops.ml index 0f0056ed43..1f8b97ae6a 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -265,7 +265,7 @@ let add_retroknowledge mp = Environ.register env f e |_ -> CErrors.anomaly ~label:"Modops.add_retroknowledge" - (Pp.str "had to import an unsupported kind of term") + (Pp.str "had to import an unsupported kind of term.") in fun lclrk env -> (* The order of the declaration matters, for instance (and it's at the diff --git a/kernel/names.ml b/kernel/names.ml index 1eb9a31751..d7c0a5e980 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -34,33 +34,28 @@ struct let hash = String.hash - let warn_invalid_identifier = - CWarnings.create ~name:"invalid-identifier" ~category:"parsing" - ~default:CWarnings.Disabled - (fun s -> str s) - - let check_soft ?(warn = true) x = - let iter (fatal, x) = - if fatal then CErrors.error x else - if warn then warn_invalid_identifier x - in + let check_valid ?(strict=true) x = + let iter (fatal, x) = if fatal || strict then CErrors.user_err Pp.(str x) in Option.iter iter (Unicode.ident_refutation x) let is_valid s = match Unicode.ident_refutation s with | None -> true | Some _ -> false + let of_bytes s = + let s = Bytes.to_string s in + check_valid s; + String.hcons s + let of_string s = - let () = check_soft s in - let s = String.copy s in + let () = check_valid s in String.hcons s let of_string_soft s = - let () = check_soft ~warn:false s in - let s = String.copy s in + let () = check_valid ~strict:false s in String.hcons s - let to_string id = String.copy id + let to_string id = id let print id = str id @@ -88,11 +83,14 @@ struct type t = Anonymous (** anonymous identifier *) | Name of Id.t (** non-anonymous identifier *) + let mk_name id = + Name id + let is_anonymous = function | Anonymous -> true | Name _ -> false - let is_name = not % is_anonymous + let is_name = is_anonymous %> not let compare n1 n2 = match n1, n2 with | Anonymous, Anonymous -> 0 @@ -106,8 +104,12 @@ struct | _ -> false let hash = function - | Anonymous -> 0 - | Name id -> Id.hash id + | Anonymous -> 0 + | Name id -> Id.hash id + + let print = function + | Anonymous -> str "_" + | Name id -> Id.print id module Self_Hashcons = struct @@ -156,21 +158,8 @@ module DirPath = struct type t = module_ident list - let rec compare (p1 : t) (p2 : t) = - if p1 == p2 then 0 - else begin match p1, p2 with - | [], [] -> 0 - | [], _ -> -1 - | _, [] -> 1 - | id1 :: p1, id2 :: p2 -> - let c = Id.compare id1 id2 in - if Int.equal c 0 then compare p1 p2 else c - end - - let rec equal p1 p2 = p1 == p2 || match p1, p2 with - | [], [] -> true - | id1 :: p1, id2 :: p2 -> Id.equal id1 id2 && equal p1 p2 - | _ -> false + let compare = List.compare Id.compare + let equal = List.equal Id.equal let rec hash accu = function | [] -> accu @@ -185,7 +174,7 @@ struct let empty = [] - let is_empty d = match d with [] -> true | _ -> false + let is_empty = List.is_empty let to_string = function | [] -> "<>" @@ -549,7 +538,6 @@ module KerPair = struct end module SyntacticOrd = struct - type t = kernel_pair let compare x y = match x, y with | Same knx, Same kny -> KerName.compare knx kny | Dual (knux,kncx), Dual (knuy,kncy) -> @@ -601,7 +589,13 @@ end module Constant = KerPair module Cmap = HMap.Make(Constant.CanOrd) +(** A map whose keys are constants (values of the {!Constant.t} type). + Keys are ordered wrt. "canonical form" of the constant. *) + module Cmap_env = HMap.Make(Constant.UserOrd) +(** A map whose keys are constants (values of the {!Constant.t} type). + Keys are ordered wrt. "user form" of the constant. *) + module Cpred = Predicate.Make(Constant.CanOrd) module Cset = Cmap.Set module Cset_env = Cmap_env.Set @@ -866,7 +860,6 @@ struct let hash (c, b) = (if b then 0 else 1) + Constant.hash c module SyntacticOrd = struct - type t = constant * bool let compare (c, b) (c', b') = if b = b' then Constant.SyntacticOrd.compare c c' else -1 let equal (c, b as x) (c', b' as x') = diff --git a/kernel/names.mli b/kernel/names.mli index feaedc775c..004d52d4b3 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -43,13 +43,15 @@ sig (** Check that a string may be converted to an identifier. @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *) + val of_bytes : bytes -> t val of_string : string -> t (** Converts a string into an identifier. - @raise UserError if the string is not valid, or echo a warning if it contains invalid identifier characters. + @raise UserError if the string is invalid as an identifier. @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *) val of_string_soft : string -> t - (** Same as {!of_string} except that no warning is ever issued. + (** Same as {!of_string} except that any string made of supported UTF-8 characters is accepted. + @raise UserError if the string is invalid as an UTF-8 string. @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *) val to_string : t -> string @@ -82,6 +84,9 @@ sig type t = Anonymous (** anonymous identifier *) | Name of Id.t (** non-anonymous identifier *) + val mk_name : Id.t -> t + (** constructor *) + val is_anonymous : t -> bool (** Return [true] iff a given name is [Anonymous]. *) @@ -100,6 +105,9 @@ sig val hcons : t -> t (** Hashconsing over names. *) + val print : t -> Pp.std_ppcmds + (** Pretty-printer (print "_" for [Anonymous]. *) + end (** {6 Type aliases} *) @@ -368,8 +376,14 @@ end module Cpred : Predicate.S with type elt = Constant.t module Cset : CSig.SetS with type elt = Constant.t module Cset_env : CSig.SetS with type elt = Constant.t + module Cmap : Map.ExtS with type key = Constant.t and module Set := Cset -module Cmap_env : Map.ExtS with type key = Constant.t and module Set := Cset_env +(** A map whose keys are constants (values of the {!Constant.t} type). + Keys are ordered wrt. "canonical form" of the constant. *) + +module Cmap_env : Map.ExtS with type key = Constant.t and module Set := Cset_env +(** A map whose keys are constants (values of the {!Constant.t} type). + Keys are ordered wrt. "user form" of the constant. *) (** {6 Inductive names} *) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index b17715a8ff..d3cd6b62a5 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -16,6 +16,8 @@ open Nativeinstr open Nativelambda open Pre_env +[@@@ocaml.warning "-32-37"] + (** This file defines the mllambda code generation phase of the native compiler. mllambda represents a fragment of ML, and can easily be printed to OCaml code. *) @@ -40,8 +42,6 @@ module LNset = Set.Make(LNord) let lname_ctr = ref (-1) -let reset_lname = lname_ctr := -1 - let fresh_lname n = incr lname_ctr; { lname = n; luid = !lname_ctr } @@ -110,40 +110,30 @@ let gname_hash gn = match gn with let case_ctr = ref (-1) -let reset_gcase () = case_ctr := -1 - let fresh_gcase l = incr case_ctr; Gcase (l,!case_ctr) let pred_ctr = ref (-1) -let reset_gpred () = pred_ctr := -1 - let fresh_gpred l = incr pred_ctr; Gpred (l,!pred_ctr) let fixtype_ctr = ref (-1) -let reset_gfixtype () = fixtype_ctr := -1 - let fresh_gfixtype l = incr fixtype_ctr; Gfixtype (l,!fixtype_ctr) let norm_ctr = ref (-1) -let reset_norm () = norm_ctr := -1 - let fresh_gnorm l = incr norm_ctr; Gnorm (l,!norm_ctr) let normtbl_ctr = ref (-1) -let reset_normtbl () = normtbl_ctr := -1 - let fresh_gnormtbl l = incr normtbl_ctr; Gnormtbl (l,!normtbl_ctr) @@ -211,47 +201,47 @@ let empty_symbols = [||] let get_value tbl i = match tbl.(i) with | SymbValue v -> v - | _ -> anomaly (Pp.str "get_value failed") + | _ -> anomaly (Pp.str "get_value failed.") let get_sort tbl i = match tbl.(i) with | SymbSort s -> s - | _ -> anomaly (Pp.str "get_sort failed") + | _ -> anomaly (Pp.str "get_sort failed.") let get_name tbl i = match tbl.(i) with | SymbName id -> id - | _ -> anomaly (Pp.str "get_name failed") + | _ -> anomaly (Pp.str "get_name failed.") let get_const tbl i = match tbl.(i) with | SymbConst kn -> kn - | _ -> anomaly (Pp.str "get_const failed") + | _ -> anomaly (Pp.str "get_const failed.") let get_match tbl i = match tbl.(i) with | SymbMatch case_info -> case_info - | _ -> anomaly (Pp.str "get_match failed") + | _ -> anomaly (Pp.str "get_match failed.") let get_ind tbl i = match tbl.(i) with | SymbInd ind -> ind - | _ -> anomaly (Pp.str "get_ind failed") + | _ -> anomaly (Pp.str "get_ind failed.") let get_meta tbl i = match tbl.(i) with | SymbMeta m -> m - | _ -> anomaly (Pp.str "get_meta failed") + | _ -> anomaly (Pp.str "get_meta failed.") let get_evar tbl i = match tbl.(i) with | SymbEvar ev -> ev - | _ -> anomaly (Pp.str "get_evar failed") + | _ -> anomaly (Pp.str "get_evar failed.") let get_level tbl i = match tbl.(i) with | SymbLevel u -> u - | _ -> anomaly (Pp.str "get_level failed") + | _ -> anomaly (Pp.str "get_level failed.") let push_symbol x = try HashtblSymbol.find symb_tbl x @@ -1848,10 +1838,9 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = auxdefs, MLlet(aux_name, ml, mkMLapp (MLlocal aux_name) (Array.of_list (fv_rel@fv_named))) and compile_rel env sigma univ auxdefs n = - let open Context.Rel in - let open Declaration in - let decl = lookup n env.env_rel_context in - let n = length env.env_rel_context - n in + let open Context.Rel.Declaration in + let decl = Context.Rel.lookup n env.env_rel_context in + let n = Context.Rel.length env.env_rel_context - n in match decl with | LocalDef (_,t,_) -> let code = lambda_of_constr env sigma t in diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 3c0afe3805..fe9f393f63 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -141,10 +141,10 @@ let native_conv_gen pb sigma env univs t1 t2 = let t1 = Sys.time () in let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in if !Flags.debug then Feedback.msg_debug (Pp.str time_info); - (* TODO change 0 when we can have deBruijn *) + (* TODO change 0 when we can have de Bruijn *) fst (conv_val env pb 0 !rt1 !rt2 univs) end - | _ -> anomaly (Pp.str "Compilation failure") + | _ -> anomaly (Pp.str "Compilation failure.") let warn_no_native_compiler = let open Pp in diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 91b40be7e9..72d9c48513 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -14,7 +14,8 @@ open Pre_env open Nativevalues open Nativeinstr -(** This file defines the lambda code generation phase of the native compiler *) +module RelDecl = Context.Rel.Declaration + exception NotClosed @@ -159,10 +160,6 @@ let rec lam_exsubst subst lam = | Lrel(id,i) -> lam_subst_rel lam id i subst | _ -> map_lam_with_binders liftn lam_exsubst subst lam -let lam_subst subst lam = - if is_subs_id subst then lam - else lam_exsubst subst lam - let lam_subst_args subst args = if is_subs_id subst then args else Array.smartmap (lam_exsubst subst) args @@ -276,71 +273,6 @@ and reduce_lapp substf lids body substa largs = Llam(Array.of_list lids, simplify (liftn (List.length lids) substf) body) | [], _::_ -> simplify_app substf body substa (Array.of_list largs) - -(* [occurrence kind k lam]: - If [kind] is [true] return [true] if the variable [k] does not appear in - [lam], return [false] if the variable appear one time and not - under a lambda, a fixpoint, a cofixpoint; else raise Not_found. - If [kind] is [false] return [false] if the variable does not appear in [lam] - else raise [Not_found] -*) - -let rec occurrence k kind lam = - match lam with - | Lrel (_,n) -> - if Int.equal n k then - if kind then false else raise Not_found - else kind - | Lvar _ | Lconst _ | Lproj _ | Luint _ | Lval _ | Lsort _ | Lind _ - | Lconstruct _ | Llazy | Lforce | Lmeta _ | Levar _ -> kind - | Lprod(dom, codom) -> - occurrence k (occurrence k kind dom) codom - | Llam(ids,body) -> - let _ = occurrence (k+Array.length ids) false body in kind - | Llet(_,def,body) -> - occurrence (k+1) (occurrence k kind def) body - | Lapp(f, args) -> - occurrence_args k (occurrence k kind f) args - | Lprim(_,_,_,args) | Lmakeblock(_,_,_,args) -> - occurrence_args k kind args - | Lcase(_,t,a,br) -> - let kind = occurrence k (occurrence k kind t) a in - let r = ref kind in - Array.iter (fun (_,ids,c) -> - r := occurrence (k+Array.length ids) kind c && !r) br; - !r - | Lif (t, bt, bf) -> - let kind = occurrence k kind t in - kind && occurrence k kind bt && occurrence k kind bf - | Lfix(_,(ids,ltypes,lbodies)) - | Lcofix(_,(ids,ltypes,lbodies)) -> - let kind = occurrence_args k kind ltypes in - let _ = occurrence_args (k+Array.length ids) false lbodies in - kind - -and occurrence_args k kind args = - Array.fold_left (occurrence k) kind args - -let occur_once lam = - try let _ = occurrence 1 true lam in true - with Not_found -> false - -(* [remove_let lam] remove let expression in [lam] if the variable is *) -(* used at most once time in the body, and does not appear under *) -(* a lambda or a fix or a cofix *) - -let rec remove_let subst lam = - match lam with - | Lrel(id,i) -> lam_subst_rel lam id i subst - | Llet(id,def,body) -> - let def' = remove_let subst def in - if occur_once body then remove_let (cons def' subst) body - else - let body' = remove_let (lift subst) body in - if def == def' && body == body' then lam else Llet(id,def',body') - | _ -> map_lam_with_binders liftn remove_let subst lam - - (*s Translation from [constr] to [lambda] *) (* Translation of constructor *) @@ -405,8 +337,6 @@ module Vect = size = 0; } - let length v = v.size - let extend v = if Int.equal v.size (Array.length v.elems) then let new_size = min (2*v.size) Sys.max_array_length in @@ -420,33 +350,15 @@ module Vect = v.elems.(v.size) <- a; v.size <- v.size + 1 - let push_pos v a = - let pos = v.size in - push v a; - pos - let popn v n = v.size <- max 0 (v.size - n) let pop v = popn v 1 - let get v n = - if v.size <= n then invalid_arg "Vect.get:index out of bounds"; - v.elems.(n) - let get_last v n = if v.size <= n then invalid_arg "Vect.get:index out of bounds"; v.elems.(v.size - n - 1) - - let last v = - if Int.equal v.size 0 then invalid_arg "Vect.last:index out of bounds"; - v.elems.(v.size - 1) - - let clear v = v.size <- 0 - - let to_array v = Array.sub v.elems 0 v.size - end let empty_args = [||] @@ -727,8 +639,7 @@ let optimize lam = let lambda_of_constr env sigma c = set_global_env env; let env = Renv.make () in - let open Context.Rel.Declaration in - let ids = List.rev_map get_name !global_env.env_rel_context in + let ids = List.rev_map RelDecl.get_name !global_env.env_rel_context in Renv.push_rels env (Array.of_list ids); let lam = lambda_of_constr env sigma c in (* if Flags.vm_draw_opt () then begin diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 1c58c7445c..f6c94158f8 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -15,7 +15,7 @@ open Envars used by the native compiler. *) let get_load_paths = - ref (fun _ -> anomaly (Pp.str "get_load_paths not initialized") : unit -> string list) + ref (fun _ -> anomaly (Pp.str "get_load_paths not initialized.") : unit -> string list) let open_header = ["Nativevalues"; "Nativecode"; @@ -35,7 +35,7 @@ let ( / ) = Filename.concat (* We have to delay evaluation of include_dirs because coqlib cannot be guessed until flags have been properly initialized *) let include_dirs () = - [Filename.temp_dir_name; coqlib () / "kernel"; coqlib () / "library"] + [Filename.get_temp_dir_name (); coqlib () / "kernel"; coqlib () / "library"] (* Pointer to the function linking an ML object into coq's toplevel *) let load_obj = ref (fun x -> () : string -> unit) @@ -125,7 +125,7 @@ let call_linker ?(fatal=true) prefix f upds = if not (Sys.file_exists f) then begin let msg = "Cannot find native compiler file " ^ f in - if fatal then CErrors.error msg + if fatal then CErrors.user_err Pp.(str msg) else if !Flags.debug then Feedback.msg_debug (Pp.str msg) end else diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 8093df3044..7ffb48221b 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -200,7 +200,7 @@ let mk_block tag args = (* Two instances of dummy_value should not be pointer equal, otherwise comparing them as terms would succeed *) let dummy_value : unit -> t = - fun () _ -> anomaly ~label:"native" (Pp.str "Evaluation failed") + fun () _ -> anomaly ~label:"native" (Pp.str "Evaluation failed.") let cast_accu v = (Obj.magic v:accumulator) @@ -334,6 +334,7 @@ let l_or accu x y = if is_int x && is_int y then no_check_l_or x y else accu x y +[@@@ocaml.warning "-37"] type coq_carry = | Caccu of t | C0 of t @@ -430,7 +431,7 @@ let addmuldiv accu x y z = if is_int x && is_int y && is_int z then no_check_addmuldiv x y z else accu x y z - +[@@@ocaml.warning "-34"] type coq_bool = | Baccu of t | Btrue @@ -491,12 +492,12 @@ let str_encode expr = let str_decode s = let mshl_expr_len = String.length s / 2 in let mshl_expr = Buffer.create mshl_expr_len in - let buf = String.create 2 in + let buf = Bytes.create 2 in for i = 0 to mshl_expr_len - 1 do - String.blit s (2*i) buf 0 2; - Buffer.add_char mshl_expr (bin_of_hex buf) + Bytes.blit_string s (2*i) buf 0 2; + Buffer.add_char mshl_expr (bin_of_hex (Bytes.to_string buf)) done; - Marshal.from_string (Buffer.contents mshl_expr) 0 + Marshal.from_bytes (Buffer.to_bytes mshl_expr) 0 (** Retroknowledge, to be removed when we switch to primitive integers *) diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 130f1eb039..59e90ca2e9 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -21,17 +21,26 @@ type proofterm = (constr * Univ.universe_context_set) Future.computation type opaque = | Indirect of substitution list * DirPath.t * int (* subst, lib, index *) | Direct of cooking_info list * proofterm -type opaquetab = (cooking_info list * proofterm) Int.Map.t * DirPath.t -let empty_opaquetab = Int.Map.empty, DirPath.initial +type opaquetab = { + opaque_val : (cooking_info list * proofterm) Int.Map.t; + (** Actual proof terms *) + opaque_len : int; + (** Size of the above map *) + opaque_dir : DirPath.t; +} +let empty_opaquetab = { + opaque_val = Int.Map.empty; + opaque_len = 0; + opaque_dir = DirPath.initial; +} (* hooks *) let default_get_opaque dp _ = - CErrors.error - ("Cannot access opaque proofs in library " ^ DirPath.to_string dp) + CErrors.user_err Pp.(pr_sequence str ["Cannot access opaque proofs in library"; DirPath.to_string dp]) let default_get_univ dp _ = - CErrors.error - ("Cannot access universe constraints of opaque proofs in library " ^ - DirPath.to_string dp) + CErrors.user_err (Pp.pr_sequence Pp.str [ + "Cannot access universe constraints of opaque proofs in library "; + DirPath.to_string dp]) let get_opaque = ref default_get_opaque let get_univ = ref default_get_univ @@ -42,51 +51,55 @@ let set_indirect_univ_accessor f = (get_univ := f) let create cu = Direct ([],cu) -let turn_indirect dp o (prfs,odp) = match o with +let turn_indirect dp o tab = match o with | Indirect (_,_,i) -> - if not (Int.Map.mem i prfs) - then CErrors.anomaly (Pp.str "Indirect in a different table") - else CErrors.anomaly (Pp.str "Already an indirect opaque") + if not (Int.Map.mem i tab.opaque_val) + then CErrors.anomaly (Pp.str "Indirect in a different table.") + else CErrors.anomaly (Pp.str "Already an indirect opaque.") | Direct (d,cu) -> - let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in - let id = Int.Map.cardinal prfs in - let prfs = Int.Map.add id (d,cu) prfs in - let ndp = - if DirPath.equal dp odp then odp - else if DirPath.equal odp DirPath.initial then dp + (** Uncomment to check dynamically that all terms turned into + indirections are hashconsed. *) +(* let check_hcons c = let c' = hcons_constr c in assert (c' == c); c in *) +(* let cu = Future.chain ~pure:true cu (fun (c, u) -> check_hcons c; c, u) in *) + let id = tab.opaque_len in + let opaque_val = Int.Map.add id (d,cu) tab.opaque_val in + let opaque_dir = + if DirPath.equal dp tab.opaque_dir then tab.opaque_dir + else if DirPath.equal tab.opaque_dir DirPath.initial then dp else CErrors.anomaly - (Pp.str "Using the same opaque table for multiple dirpaths") in - Indirect ([],dp,id), (prfs, ndp) + (Pp.str "Using the same opaque table for multiple dirpaths.") in + let ntab = { opaque_val; opaque_dir; opaque_len = id + 1 } in + Indirect ([],dp,id), ntab let subst_opaque sub = function | Indirect (s,dp,i) -> Indirect (sub::s,dp,i) - | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque") + | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.") let iter_direct_opaque f = function - | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque") + | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") | Direct (d,cu) -> Direct (d,Future.chain ~pure:true cu (fun (c, u) -> f c; c, u)) let discharge_direct_opaque ~cook_constr ci = function - | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque") + | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") | Direct (d,cu) -> Direct (ci::d,Future.chain ~pure:true cu (fun (c, u) -> cook_constr c, u)) -let join_opaque (prfs,odp) = function +let join_opaque { opaque_val = prfs; opaque_dir = odp } = function | Direct (_,cu) -> ignore(Future.join cu) | Indirect (_,dp,i) -> if DirPath.equal dp odp then let fp = snd (Int.Map.find i prfs) in ignore(Future.join fp) -let uuid_opaque (prfs,odp) = function +let uuid_opaque { opaque_val = prfs; opaque_dir = odp } = function | Direct (_,cu) -> Some (Future.uuid cu) | Indirect (_,dp,i) -> if DirPath.equal dp odp then Some (Future.uuid (snd (Int.Map.find i prfs))) else None -let force_proof (prfs,odp) = function +let force_proof { opaque_val = prfs; opaque_dir = odp } = function | Direct (_,cu) -> fst(Future.force cu) | Indirect (l,dp,i) -> @@ -97,7 +110,7 @@ let force_proof (prfs,odp) = function let c = Future.force pt in force_constr (List.fold_right subst_substituted l (from_val c)) -let force_constraints (prfs,odp) = function +let force_constraints { opaque_val = prfs; opaque_dir = odp } = function | Direct (_,cu) -> snd(Future.force cu) | Indirect (_,dp,i) -> if DirPath.equal dp odp @@ -106,14 +119,14 @@ let force_constraints (prfs,odp) = function | None -> Univ.ContextSet.empty | Some u -> Future.force u -let get_constraints (prfs,odp) = function +let get_constraints { opaque_val = prfs; opaque_dir = odp } = function | Direct (_,cu) -> Some(Future.chain ~pure:true cu snd) | Indirect (_,dp,i) -> if DirPath.equal dp odp then Some(Future.chain ~pure:true (snd (Int.Map.find i prfs)) snd) else !get_univ dp i -let get_proof (prfs,odp) = function +let get_proof { opaque_val = prfs; opaque_dir = odp } = function | Direct (_,cu) -> Future.chain ~pure:true cu fst | Indirect (l,dp,i) -> let pt = @@ -129,14 +142,13 @@ let a_constr = Future.from_val (Term.mkRel 1) let a_univ = Future.from_val Univ.ContextSet.empty let a_discharge : cooking_info list = [] -let dump (otab,_) = - let n = Int.Map.cardinal otab in +let dump { opaque_val = otab; opaque_len = n } = let opaque_table = Array.make n a_constr in let univ_table = Array.make n a_univ in let disch_table = Array.make n a_discharge in let f2t_map = ref FMap.empty in Int.Map.iter (fun n (d,cu) -> - let c, u = Future.split2 ~greedy:true cu in + let c, u = Future.split2 cu in Future.sink u; Future.sink c; opaque_table.(n) <- c; diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 5139cf0512..3897d5e51e 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -28,8 +28,9 @@ val empty_opaquetab : opaquetab (** From a [proofterm] to some [opaque]. *) val create : proofterm -> opaque -(** Turn a direct [opaque] into an indirect one, also hashconses constr. - * The integer is an hint of the maximum id used so far *) +(** Turn a direct [opaque] into an indirect one. It is your responsibility to + hashcons the inner term beforehand. The integer is an hint of the maximum id + used so far *) val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab (** From a [opaque] back to a [constr]. This might use the diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index f211583e06..48d7ee9ec3 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -17,7 +17,8 @@ open Util open Names open Term open Declarations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (* The type of environments. *) @@ -67,8 +68,8 @@ type named_context_val = { } type env = { - env_globals : globals; - env_named_context : named_context_val; + env_globals : globals; (* globals = constants + inductive types + modules + module-types *) + env_named_context : named_context_val; (* section variables *) env_rel_context : Context.Rel.t; env_rel_val : lazy_val list; env_nb_rel : int; @@ -128,10 +129,10 @@ let env_of_rel n env = (* Named context *) let push_named_context_val_val d rval ctxt = -(* assert (not (Id.Map.mem (get_id d) ctxt.env_named_map)); *) +(* assert (not (Id.Map.mem (NamedDecl.get_id d) ctxt.env_named_map)); *) { env_named_ctx = Context.Named.add d ctxt.env_named_ctx; - env_named_map = Id.Map.add (get_id d) (d, rval) ctxt.env_named_map; + env_named_map = Id.Map.add (NamedDecl.get_id d) (d, rval) ctxt.env_named_map; } let push_named_context_val d ctxt = @@ -140,8 +141,8 @@ let push_named_context_val d ctxt = let match_named_context_val c = match c.env_named_ctx with | [] -> None | decl :: ctx -> - let (_, v) = Id.Map.find (get_id decl) c.env_named_map in - let map = Id.Map.remove (get_id decl) c.env_named_map in + let (_, v) = Id.Map.find (NamedDecl.get_id decl) c.env_named_map in + let map = Id.Map.remove (NamedDecl.get_id decl) c.env_named_map in let cval = { env_named_ctx = ctx; env_named_map = map } in Some (decl, v, cval) @@ -160,19 +161,7 @@ let map_named_val f ctxt = else { env_named_ctx = ctx; env_named_map = map } let push_named d env = -(* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context); - assert (env.env_rel_context = []); *) - { env_globals = env.env_globals; - env_named_context = push_named_context_val d env.env_named_context; - env_rel_context = env.env_rel_context; - env_rel_val = env.env_rel_val; - env_nb_rel = env.env_nb_rel; - env_stratification = env.env_stratification; - env_typing_flags = env.env_typing_flags; - env_conv_oracle = env.env_conv_oracle; - retroknowledge = env.retroknowledge; - indirect_pterms = env.indirect_pterms; - } + {env with env_named_context = push_named_context_val d env.env_named_context} let lookup_named id env = fst (Id.Map.find id env.env_named_context.env_named_map) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 1ae89347ad..427ce04c55 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -71,6 +71,17 @@ let rec zlapp v = function Zlapp v2 :: s -> zlapp (Array.append v v2) s | s -> Zlapp v :: s +(** Hand-unrolling of the map function to bypass the call to the generic array + allocation. Type annotation is required to tell OCaml that the array does + not contain floats. *) +let map_lift (l : lift) (v : fconstr array) = match v with +| [||] -> assert false +| [|c0|] -> [|(l, c0)|] +| [|c0; c1|] -> [|(l, c0); (l, c1)|] +| [|c0; c1; c2|] -> [|(l, c0); (l, c1); (l, c2)|] +| [|c0; c1; c2; c3|] -> [|(l, c0); (l, c1); (l, c2); (l, c3)|] +| v -> CArray.Fun1.map (fun l t -> (l, t)) l v + let pure_stack lfts stk = let rec pure_rec lfts stk = match stk with @@ -80,7 +91,7 @@ let pure_stack lfts stk = (Zupdate _,lpstk) -> lpstk | (Zshift n,(l,pstk)) -> (el_shft n l, pstk) | (Zapp a, (l,pstk)) -> - (l,zlapp (Array.map (fun t -> (l,t)) a) pstk) + (l,zlapp (map_lift l a) pstk) | (Zproj (n,m,c), (l,pstk)) -> (l, Zlproj (c,l)::pstk) | (Zfix(fx,a),(l,pstk)) -> @@ -96,7 +107,15 @@ let pure_stack lfts stk = (****************************************************************************) let whd_betaiota env t = - whd_val (create_clos_infos betaiota env) (inject t) + match kind_of_term t with + | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _| + Prod _|Lambda _|Fix _|CoFix _) -> t + | App (c, _) -> + begin match kind_of_term c with + | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | LetIn _ -> t + | _ -> whd_val (create_clos_infos betaiota env) (inject t) + end + | _ -> whd_val (create_clos_infos betaiota env) (inject t) let nf_betaiota env t = norm_val (create_clos_infos betaiota env) (inject t) @@ -105,18 +124,33 @@ let whd_betaiotazeta env x = match kind_of_term x with | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> x + | App (c, _) -> + begin match kind_of_term c with + | Ind _ | Construct _ | Evar _ | Meta _ | Const _ -> x + | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x) + end | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x) let whd_all env t = match kind_of_term t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> t + | App (c, _) -> + begin match kind_of_term c with + | Ind _ | Construct _ | Evar _ | Meta _ -> t + | _ -> whd_val (create_clos_infos all env) (inject t) + end | _ -> whd_val (create_clos_infos all env) (inject t) let whd_allnolet env t = match kind_of_term t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t + | App (c, _) -> + begin match kind_of_term c with + | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ -> t + | _ -> whd_val (create_clos_infos allnolet env) (inject t) + end | _ -> whd_val (create_clos_infos allnolet env) (inject t) (********************************************************************) @@ -290,7 +324,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (match kind_of_term a1, kind_of_term a2 with | (Sort s1, Sort s2) -> if not (is_empty_stack v1 && is_empty_stack v2) then - anomaly (Pp.str "conversion was given ill-typed terms (Sort)"); + anomaly (Pp.str "conversion was given ill-typed terms (Sort)."); sort_cmp_universes (env_of_infos infos) cv_pb s1 s2 cuniv | (Meta n, Meta m) -> if Int.equal n m @@ -387,7 +421,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* Inconsistency: we tolerate that v1, v2 contain shift and update but we throw them away *) if not (is_empty_stack v1 && is_empty_stack v2) then - anomaly (Pp.str "conversion was given ill-typed terms (FLambda)"); + anomaly (Pp.str "conversion was given ill-typed terms (FLambda)."); let (_,ty1,bd1) = destFLambda mk_clos hd1 in let (_,ty2,bd2) = destFLambda mk_clos hd2 in let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in @@ -395,7 +429,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (FProd (_,c1,c2), FProd (_,c'1,c'2)) -> if not (is_empty_stack v1 && is_empty_stack v2) then - anomaly (Pp.str "conversion was given ill-typed terms (FProd)"); + anomaly (Pp.str "conversion was given ill-typed terms (FProd)."); (* Luo's system *) let cuniv = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv @@ -405,7 +439,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let () = match v1 with | [] -> () | _ -> - anomaly (Pp.str "conversion was given unreduced term (FLambda)") + anomaly (Pp.str "conversion was given unreduced term (FLambda).") in let (_,_ty1,bd1) = destFLambda mk_clos hd1 in eqappr CONV l2r infos @@ -414,7 +448,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let () = match v2 with | [] -> () | _ -> - anomaly (Pp.str "conversion was given unreduced term (FLambda)") + anomaly (Pp.str "conversion was given unreduced term (FLambda).") in let (_,_ty2,bd2) = destFLambda mk_clos hd2 in eqappr CONV l2r infos @@ -453,14 +487,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (FInd (ind1,u1), FInd (ind2,u2)) -> if eq_ind ind1 ind2 then - (let cuniv = convert_instances false u1 u2 cuniv in + (let cuniv = convert_instances ~flex:false u1 u2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv) else raise NotConvertible | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) -> if Int.equal j1 j2 && eq_ind ind1 ind2 then - (let cuniv = convert_instances false u1 u2 cuniv in + (let cuniv = convert_instances ~flex:false u1 u2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv) else raise NotConvertible @@ -733,7 +767,7 @@ let betazeta_appvect = lambda_appvect_assum let hnf_prod_app env t n = match kind_of_term (whd_all env t) with | Prod (_,_,b) -> subst1 n b - | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") + | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product.") let hnf_prod_applist env t nl = List.fold_left (hnf_prod_app env) t nl diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index e3b87bbe1a..f5e8e86530 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -62,6 +62,8 @@ open Names open Declarations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + (** {6 Safe environments } Fields of [safe_environment] : @@ -69,7 +71,7 @@ open Context.Named.Declaration - [env] : the underlying environment (cf Environ) - [modpath] : the current module name - [modvariant] : - * NONE before coqtop initialization (or when -notop is used) + * NONE before coqtop initialization * LIBRARY at toplevel of a compilation or a regular coqtop session * STRUCT (params,oldsenv) : inside a local module, with module parameters [params] and earlier environment [oldsenv] @@ -190,7 +192,7 @@ let check_engagement env expected_impredicative_set = begin match impredicative_set, expected_impredicative_set with | PredicativeSet, ImpredicativeSet -> - CErrors.error "Needs option -impredicative-set." + CErrors.user_err Pp.(str "Needs option -impredicative-set.") | _ -> () end @@ -344,10 +346,10 @@ let check_required current_libs needed = try let actual = DPMap.find id current_libs in if not(digest_match ~actual ~required) then - CErrors.error - ("Inconsistent assumptions over module "^(DirPath.to_string id)^".") + CErrors.user_err Pp.(pr_sequence str + ["Inconsistent assumptions over module"; DirPath.to_string id; "."]) with Not_found -> - CErrors.error ("Reference to unknown module "^(DirPath.to_string id)^".") + CErrors.user_err Pp.(pr_sequence str ["Reference to unknown module"; DirPath.to_string id; "."]) in Array.iter check needed @@ -361,11 +363,11 @@ let check_required current_libs needed = cost too much. *) let safe_push_named d env = - let id = get_id d in + let id = NamedDecl.get_id d in let _ = try let _ = Environ.lookup_named id env in - CErrors.error ("Identifier "^Id.to_string id^" already defined.") + CErrors.user_err Pp.(pr_sequence str ["Identifier"; Id.to_string id; "already defined."]) with Not_found -> () in Environ.push_named d env @@ -795,7 +797,7 @@ type native_library = Nativecode.global list let get_library_native_symbols senv dir = try DPMap.find dir senv.native_symbols - with Not_found -> CErrors.errorlabstrm "get_library_native_symbols" + with Not_found -> CErrors.user_err ~hdr:"get_library_native_symbols" Pp.((str "Linker error in the native compiler. Are you using Require inside a nested Module declaration?") ++ fnl () ++ (str "This use case is not supported, but disabling the native compiler may help.")) @@ -819,7 +821,7 @@ let export ?except senv dir = try join_safe_environment ?except senv with e -> let e = CErrors.push e in - CErrors.errorlabstrm "export" (CErrors.iprint e) + CErrors.user_err ~hdr:"export" (CErrors.iprint e) in assert(senv.future_cst = []); let () = check_current_library dir senv in @@ -855,7 +857,7 @@ let import lib cst vodigest senv = check_required senv.required lib.comp_deps; check_engagement senv.env lib.comp_enga; if DirPath.equal (ModPath.dp senv.modpath) lib.comp_name then - CErrors.errorlabstrm "Safe_typing.import" + CErrors.user_err ~hdr:"Safe_typing.import" (Pp.strbrk "Cannot load a library with the same name as the current one."); let mp = MPfile lib.comp_name in let mb = lib.comp_mod in @@ -906,7 +908,7 @@ let register_inline kn senv = let open Environ in let open Pre_env in if not (evaluable_constant kn senv.env) then - CErrors.error "Register inline: an evaluable constant is expected"; + CErrors.user_err Pp.(str "Register inline: an evaluable constant is expected"); let env = pre_env senv.env in let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in let cb = {cb with const_inline_code = true} in diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index c8ceb064d5..f779f68be4 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -110,14 +110,13 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 in let u = if poly then - CErrors.error ("Checking of subtyping of polymorphic" ^ - " inductive types not implemented") + CErrors.user_err Pp.(str "Checking of subtyping of polymorphic inductive types not implemented") else Instance.empty in let mib2 = Declareops.subst_mind_body subst2 mib2 in let check_inductive_type cst name env t1 t2 = - (* Due to sort-polymorphism in inductive types, the conclusions of + (* Due to template polymorphism, the conclusions of t1 and t2, if in Type, are generated as the least upper bounds of the types of the constructors. @@ -347,7 +346,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let c2 = Mod_subst.force_constr lc2 in check_conv NotConvertibleBodyField cst poly u infer_conv env' c1 c2)) | IndType ((kn,i),mind1) -> - ignore (CErrors.error ( + ignore (CErrors.user_err Pp.(str @@ "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ @@ -364,7 +363,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let error = NotConvertibleTypeField (env, arity1, typ2) in check_conv error cst false Univ.Instance.empty infer_conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> - ignore (CErrors.error ( + ignore (CErrors.user_err Pp.(str @@ "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ diff --git a/kernel/term.ml b/kernel/term.ml index 15f187e5c4..07a85329ef 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -71,20 +71,21 @@ type pconstant = constant puniverses type pinductive = inductive puniverses type pconstructor = constructor puniverses -type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term = +type ('constr, 'types, 'sort, 'univs) kind_of_term = + ('constr, 'types, 'sort, 'univs) Constr.kind_of_term = | Rel of int | Var of Id.t | Meta of metavariable | Evar of 'constr pexistential - | Sort of sorts + | Sort of 'sort | Cast of 'constr * cast_kind * 'types | Prod of Name.t * 'types * 'types | Lambda of Name.t * 'types * 'constr | LetIn of Name.t * 'constr * 'types * 'constr | App of 'constr * 'constr array - | Const of pconstant - | Ind of pinductive - | Construct of pconstructor + | Const of (constant * 'univs) + | Ind of (inductive * 'univs) + | Construct of (constructor * 'univs) | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint @@ -168,7 +169,7 @@ let hcons_types = Constr.hcons exception DestKO -(* Destructs a DeBrujin index *) +(* Destructs a de Bruijn index *) let destRel c = match kind_of_term c with | Rel n -> n | _ -> raise DestKO @@ -179,8 +180,6 @@ let destMeta c = match kind_of_term c with | _ -> raise DestKO let isMeta c = match kind_of_term c with Meta _ -> true | _ -> false -let isMetaOf mv c = - match kind_of_term c with Meta mv' -> Int.equal mv mv' | _ -> false (* Destructs a variable *) let destVar c = match kind_of_term c with @@ -328,38 +327,9 @@ let destCoFix c = match kind_of_term c with let isCoFix c = match kind_of_term c with CoFix _ -> true | _ -> false (******************************************************************) -(* Cast management *) -(******************************************************************) - -let rec strip_outer_cast c = match kind_of_term c with - | Cast (c,_,_) -> strip_outer_cast c - | _ -> c - -(* Fonction spéciale qui laisse les cast clés sous les Fix ou les Case *) - -let under_outer_cast f c = match kind_of_term c with - | Cast (b,k,t) -> mkCast (f b, k, f t) - | _ -> f c - -let rec under_casts f c = match kind_of_term c with - | Cast (c,k,t) -> mkCast (under_casts f c, k, t) - | _ -> f c - -(******************************************************************) (* Flattening and unflattening of embedded applications and casts *) (******************************************************************) -(* flattens application lists throwing casts in-between *) -let collapse_appl c = match kind_of_term c with - | App (f,cl) -> - let rec collapse_rec f cl2 = - match kind_of_term (strip_outer_cast f) with - | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) - | _ -> mkApp (f,cl2) - in - collapse_rec f cl - | _ -> c - let decompose_app c = match kind_of_term c with | App (f,cl) -> (f, Array.to_list cl) @@ -465,7 +435,7 @@ let rec to_lambda n prod = match kind_of_term prod with | Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda (n-1) bd) | Cast (c,_,_) -> to_lambda n c - | _ -> errorlabstrm "to_lambda" (mt ()) + | _ -> user_err ~hdr:"to_lambda" (mt ()) let rec to_prod n lam = if Int.equal n 0 then @@ -474,7 +444,7 @@ let rec to_prod n lam = match kind_of_term lam with | Lambda (na,ty,bd) -> mkProd (na,ty,to_prod (n-1) bd) | Cast (c,_,_) -> to_prod n c - | _ -> errorlabstrm "to_prod" (mt ()) + | _ -> user_err ~hdr:"to_prod" (mt ()) let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c) let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c) @@ -486,7 +456,7 @@ let lambda_applist c l = match kind_of_term c, l with | Lambda(_,_,c), arg::l -> app (arg::subst) c l | _, [] -> substl subst c - | _ -> anomaly (Pp.str "Not enough lambda's") in + | _ -> anomaly (Pp.str "Not enough lambda's.") in app [] c l let lambda_appvect c v = lambda_applist c (Array.to_list v) @@ -495,11 +465,11 @@ let lambda_applist_assum n c l = let rec app n subst t l = if Int.equal n 0 then if l == [] then substl subst t - else anomaly (Pp.str "Not enough arguments") + else anomaly (Pp.str "Not enough arguments.") else match kind_of_term t, l with | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l - | _ -> anomaly (Pp.str "Not enough lambda/let's") in + | _ -> anomaly (Pp.str "Not enough lambda/let's.") in app n [] c l let lambda_appvect_assum n c v = lambda_applist_assum n c (Array.to_list v) @@ -510,7 +480,7 @@ let prod_applist c l = match kind_of_term c, l with | Prod(_,_,c), arg::l -> app (arg::subst) c l | _, [] -> substl subst c - | _ -> anomaly (Pp.str "Not enough prod's") in + | _ -> anomaly (Pp.str "Not enough prod's.") in app [] c l (* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) @@ -520,11 +490,11 @@ let prod_applist_assum n c l = let rec app n subst t l = if Int.equal n 0 then if l == [] then substl subst t - else anomaly (Pp.str "Not enough arguments") + else anomaly (Pp.str "Not enough arguments.") else match kind_of_term t, l with | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l - | _ -> anomaly (Pp.str "Not enough prod/let's") in + | _ -> anomaly (Pp.str "Not enough prod/let's.") in app n [] c l let prod_appvect_assum n c v = prod_applist_assum n c (Array.to_list v) @@ -556,26 +526,26 @@ let decompose_lam = (* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T into the pair ([(xn,Tn);...;(x1,T1)],T) *) let decompose_prod_n n = - if n < 0 then error "decompose_prod_n: integer parameter must be positive"; + if n < 0 then user_err (str "decompose_prod_n: integer parameter must be positive"); let rec prodec_rec l n c = if Int.equal n 0 then l,c else match kind_of_term c with | Prod (x,t,c) -> prodec_rec ((x,t)::l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c - | _ -> error "decompose_prod_n: not enough products" + | _ -> user_err (str "decompose_prod_n: not enough products") in prodec_rec [] n (* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T into the pair ([(xn,Tn);...;(x1,T1)],T) *) let decompose_lam_n n = - if n < 0 then error "decompose_lam_n: integer parameter must be positive"; + if n < 0 then user_err (str "decompose_lam_n: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else match kind_of_term c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c - | _ -> error "decompose_lam_n: not enough abstractions" + | _ -> user_err (str "decompose_lam_n: not enough abstractions") in lamdec_rec [] n @@ -611,7 +581,7 @@ let decompose_lam_assum = ci,Ti);..;(x1,None,T1)] and of the inner type [T]) *) let decompose_prod_n_assum n = if n < 0 then - error "decompose_prod_n_assum: integer parameter must be positive"; + user_err (str "decompose_prod_n_assum: integer parameter must be positive"); let rec prodec_rec l n c = if Int.equal n 0 then l,c else @@ -620,7 +590,7 @@ let decompose_prod_n_assum n = | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c - | c -> error "decompose_prod_n_assum: not enough assumptions" + | c -> user_err (str "decompose_prod_n_assum: not enough assumptions") in prodec_rec Context.Rel.empty n @@ -632,7 +602,7 @@ let decompose_prod_n_assum n = but n is the actual number of destructurated lambdas. *) let decompose_lam_n_assum n = if n < 0 then - error "decompose_lam_n_assum: integer parameter must be positive"; + user_err (str "decompose_lam_n_assum: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else @@ -641,14 +611,14 @@ let decompose_lam_n_assum n = | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c | Cast (c,_,_) -> lamdec_rec l n c - | c -> error "decompose_lam_n_assum: not enough abstractions" + | c -> user_err (str "decompose_lam_n_assum: not enough abstractions") in lamdec_rec Context.Rel.empty n (* Same, counting let-in *) let decompose_lam_n_decls n = if n < 0 then - error "decompose_lam_n_decls: integer parameter must be positive"; + user_err (str "decompose_lam_n_decls: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else @@ -657,7 +627,7 @@ let decompose_lam_n_decls n = | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c - | c -> error "decompose_lam_n_decls: not enough abstractions" + | c -> user_err (str "decompose_lam_n_decls: not enough abstractions") in lamdec_rec Context.Rel.empty n @@ -690,7 +660,7 @@ let destArity = | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c | Cast (c,_,_) -> prodec_rec l c | Sort s -> l,s - | _ -> anomaly ~label:"destArity" (Pp.str "not an arity") + | _ -> anomaly ~label:"destArity" (Pp.str "not an arity.") in prodec_rec [] diff --git a/kernel/term.mli b/kernel/term.mli index 60a3c77154..241ef322fa 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -68,20 +68,21 @@ type ('constr, 'types) prec_declaration = type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint -type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term = +type ('constr, 'types, 'sort, 'univs) kind_of_term = + ('constr, 'types, 'sort, 'univs) Constr.kind_of_term = | Rel of int | Var of Id.t | Meta of metavariable | Evar of 'constr pexistential - | Sort of sorts + | Sort of 'sort | Cast of 'constr * cast_kind * 'types | Prod of Name.t * 'types * 'types | Lambda of Name.t * 'types * 'constr | LetIn of Name.t * 'constr * 'types * 'constr | App of 'constr * 'constr array - | Const of constant puniverses - | Ind of inductive puniverses - | Construct of constructor puniverses + | Const of (constant * 'univs) + | Ind of (inductive * 'univs) + | Construct of (constructor * 'univs) | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint @@ -98,7 +99,6 @@ val isVarId : Id.t -> constr -> bool val isInd : constr -> bool val isEvar : constr -> bool val isMeta : constr -> bool -val isMetaOf : metavariable -> constr -> bool val isEvar_or_Meta : constr -> bool val isSort : constr -> bool val isCast : constr -> bool @@ -127,7 +127,7 @@ val is_small : sorts -> bool exception DestKO -(** Destructs a DeBrujin index *) +(** Destructs a de Bruijn index *) val destRel : constr -> int (** Destructs an existential variable *) @@ -349,20 +349,6 @@ val strip_lam_n : int -> constr -> constr val strip_prod_assum : types -> types val strip_lam_assum : constr -> constr -(** Flattens application lists *) -val collapse_appl : constr -> constr - - -(** Remove recursively the casts around a term i.e. - [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *) -val strip_outer_cast : constr -> constr - -(** Apply a function letting Casted types in place *) -val under_casts : (constr -> constr) -> constr -> constr - -(** Apply a function under components of Cast if any *) -val under_outer_cast : (constr -> constr) -> constr -> constr - (** {5 ... } *) (** An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort. Such a term can canonically be seen as the pair of a context of types @@ -458,7 +444,7 @@ val leq_constr_univs : constr UGraph.check_function application grouping and ignoring universe instances. *) val eq_constr_nounivs : constr -> constr -> bool -val kind_of_term : constr -> (constr, types) kind_of_term +val kind_of_term : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term (** Alias for [Constr.kind] *) val constr_ord : constr -> constr -> int diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 6ce14c853d..eeb9c421a1 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -20,7 +20,9 @@ open Declarations open Environ open Entries open Typeops -open Fast_typeops + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration (* Insertion of constants and parameters in environment. *) @@ -85,58 +87,92 @@ let concat_seff = SideEffects.concat let mk_pure_proof c = (c, Univ.ContextSet.empty), empty_seff let inline_side_effects env body ctx side_eff = - let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } = + (** First step: remove the constants that are still in the environment *) + let filter { eff = se; from_env = mb } = let cbl = match se with - | SEsubproof (c,cb,b) -> [c,cb,b] - | SEscheme (cl,_) -> List.map (fun (_,c,cb,b) -> c,cb,b) cl in + | SEsubproof (c, cb, b) -> [c, cb, b] + | SEscheme (cl,_) -> + List.map (fun (_, c, cb, b) -> c, cb, b) cl + in let not_exists (c,_,_) = try ignore(Environ.lookup_constant c env); false with Not_found -> true in let cbl = List.filter not_exists cbl in - let cname c = - let name = string_of_con c in - for i = 0 to String.length name - 1 do - if name.[i] == '.' || name.[i] == '#' then name.[i] <- '_' done; - Name (id_of_string name) in - let rec sub c i x = match kind_of_term x with - | Const (c', _) when eq_constant c c' -> mkRel i - | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub c i x) i x in - let rec sub_body c u b i x = match kind_of_term x with - | Const (c',u') when eq_constant c c' -> - Vars.subst_instance_constr u' b - | _ -> map_constr_with_binders ((+) 1) (sub_body c u b) i x in - let fix_body (c,cb,b) (t,ctx) = - match cb.const_body, b with - | Def b, _ -> - let b = Mod_subst.force_constr b in - let poly = cb.const_polymorphic in - if not poly then - let b_ty = Typeops.type_of_constant_type env cb.const_type in - let t = sub c 1 (Vars.lift 1 t) in - mkLetIn (cname c, b, b_ty, t), - Univ.ContextSet.union ctx - (Univ.ContextSet.of_context cb.const_universes) - else - let univs = cb.const_universes in - sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx - | OpaqueDef _, `Opaque (b,_) -> - let poly = cb.const_polymorphic in - if not poly then - let b_ty = Typeops.type_of_constant_type env cb.const_type in - let t = sub c 1 (Vars.lift 1 t) in - mkApp (mkLambda (cname c, b_ty, t), [|b|]), - Univ.ContextSet.union ctx - (Univ.ContextSet.of_context cb.const_universes) - else - let univs = cb.const_universes in - sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx + (cbl, mb) + in + (* CAVEAT: we assure that most recent effects come first *) + let side_eff = List.map filter (uniq_seff_rev side_eff) in + let sigs = List.rev_map (fun (cbl, mb) -> mb, List.length cbl) side_eff in + let side_eff = List.fold_left (fun accu (cbl, _) -> cbl @ accu) [] side_eff in + let side_eff = List.rev side_eff in + (** Most recent side-effects first in side_eff *) + if List.is_empty side_eff then (body, ctx, sigs) + else + (** Second step: compute the lifts and substitutions to apply *) + let cname c = + let name = Constant.to_string c in + let map c = if c == '.' || c == '#' then '_' else c in + let name = String.map map name in + Name (Id.of_string name) + in + let fold (subst, var, ctx, args) (c, cb, b) = + let (b, opaque) = match cb.const_body, b with + | Def b, _ -> (Mod_subst.force_constr b, false) + | OpaqueDef _, `Opaque (b,_) -> (b, true) | _ -> assert false + in + if cb.const_polymorphic then + (** Inline the term to emulate universe polymorphism *) + let data = (Univ.UContext.instance cb.const_universes, b) in + let subst = Cmap_env.add c (Inl data) subst in + (subst, var, ctx, args) + else + (** Abstract over the term at the top of the proof *) + let ty = Typeops.type_of_constant_type env cb.const_type in + let subst = Cmap_env.add c (Inr var) subst in + let univs = Univ.ContextSet.of_context cb.const_universes in + let ctx = Univ.ContextSet.union ctx univs in + (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args) in - let t, ctx = List.fold_right fix_body cbl (t,ctx) in - t, ctx, (mb,List.length cbl) :: sl - in - (* CAVEAT: we assure a proper order *) - List.fold_left handle_sideff (body,ctx,[]) (uniq_seff_rev side_eff) + let (subst, len, ctx, args) = List.fold_left fold (Cmap_env.empty, 1, ctx, []) side_eff in + (** Third step: inline the definitions *) + let rec subst_const i k t = match Constr.kind t with + | Const (c, u) -> + let data = try Some (Cmap_env.find c subst) with Not_found -> None in + begin match data with + | None -> t + | Some (Inl (inst, b)) -> + (** [b] is closed but may refer to other constants *) + subst_const i k (Vars.subst_instance_constr u b) + | Some (Inr n) -> + mkRel (k + n - i) + end + | Rel n -> + (** Lift free rel variables *) + if n <= k then t + else mkRel (n + len - i - 1) + | _ -> map_constr_with_binders ((+) 1) (fun k t -> subst_const i k t) k t + in + let map_args i (na, b, ty, opaque) = + (** Both the type and the body may mention other constants *) + let ty = subst_const (len - i - 1) 0 ty in + let b = subst_const (len - i - 1) 0 b in + (na, b, ty, opaque) + in + let args = List.mapi map_args args in + let body = subst_const 0 0 body in + let fold_arg (na, b, ty, opaque) accu = + if opaque then mkApp (mkLambda (na, ty, accu), [|b|]) + else mkLetIn (na, b, ty, accu) + in + let body = List.fold_right fold_arg args body in + (body, ctx, sigs) + +let rec is_nth_suffix n l suf = + if Int.equal n 0 then l == suf + else match l with + | [] -> false + | _ :: l -> is_nth_suffix (pred n) l suf (* Given the list of signatures of side effects, checks if they match. * I.e. if they are ordered descendants of the current revstruct *) @@ -150,7 +186,7 @@ let check_signatures curmb sl = match sl with | None -> sl, None | Some n -> - if List.length mb >= how_many && CList.skipn how_many mb == curmb + if is_nth_suffix how_many mb curmb then Some (n + how_many), Some mb else None, None with CEphemeron.InvalidKey -> None, None in @@ -184,13 +220,10 @@ let rec unzip ctx j = | `Cut (n,ty,arg) :: ctx -> unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) } -let hcons_j j = - { uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type} - let feedback_completion_typecheck = let open Feedback in Option.iter (fun state_id -> - feedback ~id:(State state_id) Feedback.Complete) + feedback ~id:state_id Feedback.Complete) let infer_declaration ~trust env kn dcl = match dcl with @@ -214,7 +247,7 @@ let infer_declaration ~trust env kn dcl = let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let tyj = infer_type env typ in let proofterm = - Future.chain ~greedy:true ~pure:true body (fun ((body,uctx),side_eff) -> + Future.chain ~pure:true body (fun ((body,uctx),side_eff) -> let body, uctx, signatures = inline_side_effects env body uctx side_eff in let valid_signatures = check_signatures trust signatures in @@ -223,13 +256,13 @@ let infer_declaration ~trust env kn dcl = let body,env,ectx = skip_trusted_seff valid_signatures body env in let j = infer env body in unzip ectx j in - let j = hcons_j j in let subst = Univ.LMap.empty in let _ = judge_of_cast env j DEFAULTcast tyj in assert (eq_constr typ tyj.utj_val); + let c = hcons_constr j.uj_val in let _typ = RegularArity (Vars.subst_univs_level_constr subst typ) in feedback_completion_typecheck feedback_id; - j.uj_val, uctx) in + c, uctx) in let def = OpaqueDef (Opaqueproof.create proofterm) in def, RegularArity typ, None, c.const_entry_polymorphic, c.const_entry_universes, @@ -286,18 +319,17 @@ let global_vars_set_constant_type env = function | RegularArity t -> global_vars_set env t | TemplateArity (ctx,_) -> Context.Rel.fold_outside - (Context.Rel.Declaration.fold + (RelDecl.fold_constr (fun t c -> Id.Set.union (global_vars_set env t) c)) ctx ~init:Id.Set.empty let record_aux env s_ty s_bo suggested_expr = - let open Context.Named.Declaration in let in_ty = keep_hyps env s_ty in let v = String.concat " " (CList.map_filter (fun decl -> - let id = get_id decl in - if List.exists (Id.equal id % get_id) in_ty then None + let id = NamedDecl.get_id decl in + if List.exists (NamedDecl.get_id %> Id.equal id) in_ty then None else Some (Id.to_string id)) (keep_hyps env s_bo)) in Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr) @@ -306,26 +338,25 @@ let suggest_proof_using = ref (fun _ _ _ _ _ -> "") let set_suggest_proof_using f = suggest_proof_using := f let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) = - let open Context.Named.Declaration in let check declared inferred = - let mk_set l = List.fold_right Id.Set.add (List.map get_id l) Id.Set.empty in + let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in let inferred_set, declared_set = mk_set inferred, mk_set declared in if not (Id.Set.subset inferred_set declared_set) then let l = Id.Set.elements (Idset.diff inferred_set declared_set) in let n = List.length l in - errorlabstrm "" (Pp.(str "The following section " ++ + user_err (Pp.(str "The following section " ++ str (String.plural n "variable") ++ str " " ++ str (String.conjugate_verb_to_be n) ++ str " used but not declared:" ++ fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in let sort evn l = List.filter (fun decl -> - let id = get_id decl in - List.exists (Names.Id.equal id % get_id) l) + let id = NamedDecl.get_id decl in + List.exists (NamedDecl.get_id %> Names.Id.equal id) l) (named_context env) in (* We try to postpone the computation of used section variables *) let hyps, def = - let context_ids = List.map get_id (named_context env) in + let context_ids = List.map NamedDecl.get_id (named_context env) in match ctx with | None when not (List.is_empty context_ids) -> (* No declared section vars, and non-empty section context: @@ -453,7 +484,7 @@ let export_side_effects mb env ce = let { const_entry_body = body } = c in let _, eff = Future.force body in let ce = DefinitionEntry { c with - const_entry_body = Future.chain ~greedy:true ~pure:true body + const_entry_body = Future.chain ~pure:true body (fun (b_ctx, _) -> b_ctx, empty_seff) } in let not_exists (c,_,_,_) = try ignore(Environ.lookup_constant c env); false @@ -508,7 +539,11 @@ let translate_local_assum env t = t let translate_recipe env kn r = - build_constant_declaration kn env (Cooking.cook_constant env r) + (** We only hashcons the term when outside of a section, otherwise this would + be useless. It is detected by the dirpath of the constant being empty. *) + let (_, dir, _) = Constant.repr3 kn in + let hcons = DirPath.is_empty dir in + build_constant_declaration kn env (Cooking.cook_constant ~hcons env r) let translate_local_def mb env id centry = let def,typ,proj,poly,univs,inline_code,ctx = @@ -519,8 +554,7 @@ let translate_local_def mb env id centry = | Undef _ -> () | Def _ -> () | OpaqueDef lc -> - let open Context.Named.Declaration in - let context_ids = List.map get_id (named_context env) in + let context_ids = List.map NamedDecl.get_id (named_context env) in let ids_typ = global_vars_set env typ in let ids_def = global_vars_set env (Opaqueproof.force_proof (opaque_tables env) lc) in @@ -536,7 +570,7 @@ let translate_local_def mb env id centry = let translate_mind env kn mie = Indtypes.check_inductive env kn mie let inline_entry_side_effects env ce = { ce with - const_entry_body = Future.chain ~greedy:true ~pure:true + const_entry_body = Future.chain ~pure:true ce.const_entry_body (fun ((body, ctx), side_eff) -> let body, ctx',_ = inline_side_effects env body ctx side_eff in (body, ctx'), empty_seff); diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 5071f0ad5d..5e17638152 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -13,52 +13,56 @@ open Reduction (* Type errors. *) -type guard_error = +type 'constr pguard_error = (* Fixpoints *) | NotEnoughAbstractionInFixBody - | RecursionNotOnInductiveType of constr - | RecursionOnIllegalTerm of int * (env * constr) * int list * int list + | RecursionNotOnInductiveType of 'constr + | RecursionOnIllegalTerm of int * (env * 'constr) * int list * int list | NotEnoughArgumentsForFixCall of int (* CoFixpoints *) - | CodomainNotInductiveType of constr + | CodomainNotInductiveType of 'constr | NestedRecursiveOccurrences - | UnguardedRecursiveCall of constr - | RecCallInTypeOfAbstraction of constr - | RecCallInNonRecArgOfConstructor of constr - | RecCallInTypeOfDef of constr - | RecCallInCaseFun of constr - | RecCallInCaseArg of constr - | RecCallInCasePred of constr - | NotGuardedForm of constr - | ReturnPredicateNotCoInductive of constr + | UnguardedRecursiveCall of 'constr + | RecCallInTypeOfAbstraction of 'constr + | RecCallInNonRecArgOfConstructor of 'constr + | RecCallInTypeOfDef of 'constr + | RecCallInCaseFun of 'constr + | RecCallInCaseArg of 'constr + | RecCallInCasePred of 'constr + | NotGuardedForm of 'constr + | ReturnPredicateNotCoInductive of 'constr + +type guard_error = constr pguard_error type arity_error = | NonInformativeToInformative | StrongEliminationOnNonSmallType | WrongArity -type type_error = +type ('constr, 'types) ptype_error = | UnboundRel of int | UnboundVar of variable - | NotAType of unsafe_judgment - | BadAssumption of unsafe_judgment - | ReferenceVariables of identifier * constr - | ElimArity of pinductive * sorts_family list * constr * unsafe_judgment + | NotAType of ('constr, 'types) punsafe_judgment + | BadAssumption of ('constr, 'types) punsafe_judgment + | ReferenceVariables of identifier * 'constr + | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment * (sorts_family * sorts_family * arity_error) option - | CaseNotInductive of unsafe_judgment + | CaseNotInductive of ('constr, 'types) punsafe_judgment | WrongCaseInfo of pinductive * case_info - | NumberBranches of unsafe_judgment * int - | IllFormedBranch of constr * pconstructor * constr * constr - | Generalization of (Name.t * types) * unsafe_judgment - | ActualType of unsafe_judgment * types + | NumberBranches of ('constr, 'types) punsafe_judgment * int + | IllFormedBranch of 'constr * pconstructor * 'constr * 'constr + | Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment + | ActualType of ('constr, 'types) punsafe_judgment * 'types | CantApplyBadType of - (int * constr * constr) * unsafe_judgment * unsafe_judgment array - | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array - | IllFormedRecBody of guard_error * Name.t array * int * env * unsafe_judgment array + (int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array + | CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array + | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array | IllTypedRecBody of - int * Name.t array * unsafe_judgment array * types array + int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array | UnsatisfiedConstraints of Univ.constraints +type type_error = (constr, types) ptype_error + exception TypeError of env * type_error let nfj env {uj_val=c;uj_type=ct} = diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 0c3a952b8d..bd6032716f 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -14,52 +14,56 @@ open Environ (*i Rem: NotEnoughAbstractionInFixBody should only occur with "/i" Fix notation i*) -type guard_error = +type 'constr pguard_error = (** Fixpoints *) | NotEnoughAbstractionInFixBody - | RecursionNotOnInductiveType of constr - | RecursionOnIllegalTerm of int * (env * constr) * int list * int list + | RecursionNotOnInductiveType of 'constr + | RecursionOnIllegalTerm of int * (env * 'constr) * int list * int list | NotEnoughArgumentsForFixCall of int (** CoFixpoints *) - | CodomainNotInductiveType of constr + | CodomainNotInductiveType of 'constr | NestedRecursiveOccurrences - | UnguardedRecursiveCall of constr - | RecCallInTypeOfAbstraction of constr - | RecCallInNonRecArgOfConstructor of constr - | RecCallInTypeOfDef of constr - | RecCallInCaseFun of constr - | RecCallInCaseArg of constr - | RecCallInCasePred of constr - | NotGuardedForm of constr - | ReturnPredicateNotCoInductive of constr + | UnguardedRecursiveCall of 'constr + | RecCallInTypeOfAbstraction of 'constr + | RecCallInNonRecArgOfConstructor of 'constr + | RecCallInTypeOfDef of 'constr + | RecCallInCaseFun of 'constr + | RecCallInCaseArg of 'constr + | RecCallInCasePred of 'constr + | NotGuardedForm of 'constr + | ReturnPredicateNotCoInductive of 'constr + +type guard_error = constr pguard_error type arity_error = | NonInformativeToInformative | StrongEliminationOnNonSmallType | WrongArity -type type_error = +type ('constr, 'types) ptype_error = | UnboundRel of int | UnboundVar of variable - | NotAType of unsafe_judgment - | BadAssumption of unsafe_judgment - | ReferenceVariables of identifier * constr - | ElimArity of pinductive * sorts_family list * constr * unsafe_judgment + | NotAType of ('constr, 'types) punsafe_judgment + | BadAssumption of ('constr, 'types) punsafe_judgment + | ReferenceVariables of identifier * 'constr + | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment * (sorts_family * sorts_family * arity_error) option - | CaseNotInductive of unsafe_judgment + | CaseNotInductive of ('constr, 'types) punsafe_judgment | WrongCaseInfo of pinductive * case_info - | NumberBranches of unsafe_judgment * int - | IllFormedBranch of constr * pconstructor * constr * constr - | Generalization of (Name.t * types) * unsafe_judgment - | ActualType of unsafe_judgment * types + | NumberBranches of ('constr, 'types) punsafe_judgment * int + | IllFormedBranch of 'constr * pconstructor * 'constr * 'constr + | Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment + | ActualType of ('constr, 'types) punsafe_judgment * 'types | CantApplyBadType of - (int * constr * constr) * unsafe_judgment * unsafe_judgment array - | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array - | IllFormedRecBody of guard_error * Name.t array * int * env * unsafe_judgment array + (int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array + | CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array + | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array | IllTypedRecBody of - int * Name.t array * unsafe_judgment array * types array + int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array | UnsatisfiedConstraints of Univ.constraints +type type_error = (constr, types) ptype_error + exception TypeError of env * type_error val error_unbound_rel : env -> int -> 'a diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 0059111c09..1a07bb2fc6 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -14,11 +14,12 @@ open Term open Vars open Declarations open Environ -open Entries open Reduction open Inductive open Type_errors -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y @@ -35,61 +36,46 @@ let check_constraints cst env = if Environ.check_constraints cst env then () else error_unsatisfied_constraints env cst -(* This should be a type (a priori without intension to be an assumption) *) -let type_judgment env j = - match kind_of_term(whd_all env j.uj_type) with - | Sort s -> {utj_val = j.uj_val; utj_type = s } - | _ -> error_not_type env j +(* This should be a type (a priori without intention to be an assumption) *) +let check_type env c t = + match kind_of_term(whd_all env t) with + | Sort s -> s + | _ -> error_not_type env (make_judge c t) -(* This should be a type intended to be assumed. The error message is *) -(* not as useful as for [type_judgment]. *) -let assumption_of_judgment env j = - try (type_judgment env j).utj_val +(* This should be a type intended to be assumed. The error message is + not as useful as for [type_judgment]. *) +let check_assumption env t ty = + try let _ = check_type env t ty in t with TypeError _ -> - error_assumption env j + error_assumption env (make_judge t ty) (************************************************) -(* Incremental typing rules: builds a typing judgement given the *) -(* judgements for the subterms. *) +(* Incremental typing rules: builds a typing judgment given the *) +(* judgments for the subterms. *) (*s Type of sorts *) (* Prop and Set *) -let judge_of_prop = - { uj_val = mkProp; - uj_type = mkSort type1_sort } - -let judge_of_set = - { uj_val = mkSet; - uj_type = mkSort type1_sort } - -let judge_of_prop_contents = function - | Null -> judge_of_prop - | Pos -> judge_of_set +let type1 = mkSort type1_sort (* Type of Type(i). *) -let judge_of_type u = +let type_of_type u = let uu = Universe.super u in - { uj_val = mkType u; - uj_type = mkType uu } + mkType uu (*s Type of a de Bruijn index. *) -let judge_of_relative env n = +let type_of_relative env n = try - let typ = get_type (lookup_rel n env) in - { uj_val = mkRel n; - uj_type = lift n typ } + env |> lookup_rel n |> RelDecl.get_type |> lift n with Not_found -> error_unbound_rel env n (* Type of variables *) -let judge_of_variable env id = - try - let ty = named_type id env in - make_judge (mkVar id) ty +let type_of_variable env id = + try named_type id env with Not_found -> error_unbound_var env id @@ -98,11 +84,11 @@ let judge_of_variable env id = (* Checks if a context of variables can be instantiated by the variables of the current env. Order does not have to be checked assuming that all names are distinct *) -let check_hyps_inclusion env c sign = +let check_hyps_inclusion env f c sign = Context.Named.fold_outside (fun d1 () -> let open Context.Named.Declaration in - let id = get_id d1 in + let id = NamedDecl.get_id d1 in try let d2 = lookup_named id env in conv env (get_type d2) (get_type d1); @@ -114,7 +100,7 @@ let check_hyps_inclusion env c sign = | LocalDef _, LocalAssum _ -> raise NotConvertible | LocalDef (_,b2,_), LocalDef (_,b1,_) -> conv env b2 b1); with Not_found | NotConvertible | Option.Heterogeneous -> - error_reference_variables env id c) + error_reference_variables env id (f c)) sign ~init:() @@ -122,35 +108,9 @@ let check_hyps_inclusion env c sign = (* Make a type polymorphic if an arity *) -let extract_level env p = - let _,c = dest_prod_assum env p in - match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None - -let extract_context_levels env l = - let fold l = function - | LocalAssum (_,p) -> extract_level env p :: l - | LocalDef _ -> l - in - List.fold_left fold [] l - -let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} = - let params, ccl = dest_prod_assum env t in - match kind_of_term ccl with - | Sort (Type u) -> - let ind, l = decompose_app (whd_all env c) in - if isInd ind && List.is_empty l then - let mis = lookup_mind_specif env (fst (destInd ind)) in - let nparams = Inductive.inductive_params mis in - let paramsl = CList.lastn nparams params in - let param_ccls = extract_context_levels env paramsl in - let s = { template_param_levels = param_ccls; template_level = u} in - TemplateArity (params,s) - else RegularArity t - | _ -> - RegularArity t - (* Type of constants *) + let type_of_constant_type_knowing_parameters env t paramtyps = match t with | RegularArity t -> t @@ -159,49 +119,28 @@ let type_of_constant_type_knowing_parameters env t paramtyps = let ctx,s = instantiate_universes env ctx ar paramtyps in mkArity (List.rev ctx,s) -let type_of_constant_knowing_parameters env cst paramtyps = - let cb = lookup_constant (fst cst) env in - let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in +let type_of_constant_knowing_parameters env (kn,u as cst) args = + let cb = lookup_constant kn env in + let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in let ty, cu = constant_type env cst in - type_of_constant_type_knowing_parameters env ty paramtyps, cu + let ty = type_of_constant_type_knowing_parameters env ty args in + let () = check_constraints cu env in + ty -let type_of_constant_knowing_parameters_in env cst paramtyps = - let cb = lookup_constant (fst cst) env in - let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in +let type_of_constant_knowing_parameters_in env (kn,u as cst) args = + let cb = lookup_constant kn env in + let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in let ty = constant_type_in env cst in - type_of_constant_type_knowing_parameters env ty paramtyps - -let type_of_constant_type env t = - type_of_constant_type_knowing_parameters env t [||] + type_of_constant_type_knowing_parameters env ty args let type_of_constant env cst = type_of_constant_knowing_parameters env cst [||] let type_of_constant_in env cst = - let cb = lookup_constant (fst cst) env in - let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in - let ar = constant_type_in env cst in - type_of_constant_type_knowing_parameters env ar [||] - -let judge_of_constant_knowing_parameters env (kn,u as cst) args = - let c = mkConstU cst in - let ty, cu = type_of_constant_knowing_parameters env cst args in - let () = check_constraints cu env in - make_judge c ty - -let judge_of_constant env cst = - judge_of_constant_knowing_parameters env cst [||] - -let type_of_projection env (p,u) = - let cst = Projection.constant p in - let cb = lookup_constant cst env in - match cb.const_proj with - | Some pb -> - if cb.const_polymorphic then - Vars.subst_instance_constr u pb.proj_type - else pb.proj_type - | None -> raise (Invalid_argument "type_of_projection: not a projection") + type_of_constant_knowing_parameters_in env cst [||] +let type_of_constant_type env t = + type_of_constant_type_knowing_parameters env t [||] (* Type of a lambda-abstraction. *) @@ -215,40 +154,36 @@ let type_of_projection env (p,u) = and no upper constraint exists on the sort $s$, we don't need to compute $s$ *) -let judge_of_abstraction env name var j = - { uj_val = mkLambda (name, var.utj_val, j.uj_val); - uj_type = mkProd (name, var.utj_val, j.uj_type) } - -(* Type of let-in. *) - -let judge_of_letin env name defj typj j = - { uj_val = mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val) ; - uj_type = subst1 defj.uj_val j.uj_type } +let type_of_abstraction env name var ty = + mkProd (name, var, ty) (* Type of an application. *) -let judge_of_apply env funj argjv = - let rec apply_rec n typ = function - | [] -> - { uj_val = mkApp (j_val funj, Array.map j_val argjv); - uj_type = typ } - | hj::restjl -> - (match kind_of_term (whd_all env typ) with - | Prod (_,c1,c2) -> - (try - let () = conv_leq false env hj.uj_type c1 in - apply_rec (n+1) (subst1 hj.uj_val c2) restjl - with NotConvertible -> - error_cant_apply_bad_type env - (n,c1, hj.uj_type) - funj argjv) - - | _ -> - error_cant_apply_not_functional env funj argjv) - in - apply_rec 1 - funj.uj_type - (Array.to_list argjv) +let make_judgev c t = + Array.map2 make_judge c t + +let type_of_apply env func funt argsv argstv = + let len = Array.length argsv in + let rec apply_rec i typ = + if Int.equal i len then typ + else + (match kind_of_term (whd_all env typ) with + | Prod (_,c1,c2) -> + let arg = argsv.(i) and argt = argstv.(i) in + (try + let () = conv_leq false env argt c1 in + apply_rec (i+1) (subst1 arg c2) + with NotConvertible -> + error_cant_apply_bad_type env + (i+1,c1,argt) + (make_judge func funt) + (make_judgev argsv argstv)) + + | _ -> + error_cant_apply_not_functional env + (make_judge func funt) + (make_judgev argsv argstv)) + in apply_rec 0 funt (* Type of product *) @@ -281,10 +216,9 @@ let sort_of_product env domsort rangsort = where j.uj_type is convertible to a sort s2 *) -let judge_of_product env name t1 t2 = - let s = sort_of_product env t1.utj_type t2.utj_type in - { uj_val = mkProd (name, t1.utj_val, t2.utj_val); - uj_type = mkSort s } +let type_of_product env name s1 s2 = + let s = sort_of_product env s1 s2 in + mkSort s (* Type of a type cast *) @@ -295,29 +229,20 @@ let judge_of_product env name t1 t2 = env |- c:typ2 *) -let judge_of_cast env cj k tj = - let expected_type = tj.utj_val in +let check_cast env c ct k expected_type = try - let c, cst = - match k with - | VMcast -> - mkCast (cj.uj_val, k, expected_type), - Reduction.vm_conv CUMUL env cj.uj_type expected_type - | DEFAULTcast -> - mkCast (cj.uj_val, k, expected_type), - default_conv ~l2r:false CUMUL env cj.uj_type expected_type - | REVERTcast -> - cj.uj_val, - default_conv ~l2r:true CUMUL env cj.uj_type expected_type - | NATIVEcast -> - let sigma = Nativelambda.empty_evars in - mkCast (cj.uj_val, k, expected_type), - Nativeconv.native_conv CUMUL sigma env cj.uj_type expected_type - in - { uj_val = c; - uj_type = expected_type } + match k with + | VMcast -> + vm_conv CUMUL env ct expected_type + | DEFAULTcast -> + default_conv ~l2r:false CUMUL env ct expected_type + | REVERTcast -> + default_conv ~l2r:true CUMUL env ct expected_type + | NATIVEcast -> + let sigma = Nativelambda.empty_evars in + Nativeconv.native_conv CUMUL sigma env ct expected_type with NotConvertible -> - error_actual_type env cj expected_type + error_actual_type env (make_judge c ct) expected_type (* Inductive types. *) @@ -333,83 +258,78 @@ let judge_of_cast env cj k tj = the App case of execute; from this constraints, the expected dynamic constraints of the form u<=v are enforced *) -let judge_of_inductive_knowing_parameters env (ind,u as indu) args = - let c = mkIndU indu in +let type_of_inductive_knowing_parameters env (ind,u as indu) args = let (mib,mip) as spec = lookup_mind_specif env ind in - check_hyps_inclusion env c mib.mind_hyps; + check_hyps_inclusion env mkIndU indu mib.mind_hyps; let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters env (spec,u) args in - check_constraints cst env; - make_judge c t + check_constraints cst env; + t -let judge_of_inductive env (ind,u as indu) = - let c = mkIndU indu in - let (mib,mip) as spec = lookup_mind_specif env ind in - check_hyps_inclusion env c mib.mind_hyps; - let t,cst = Inductive.constrained_type_of_inductive env (spec,u) in - check_constraints cst env; - (make_judge c t) +let type_of_inductive env (ind,u as indu) = + let (mib,mip) = lookup_mind_specif env ind in + check_hyps_inclusion env mkIndU indu mib.mind_hyps; + let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in + check_constraints cst env; + t (* Constructors. *) -let judge_of_constructor env (c,u as cu) = - let constr = mkConstructU cu in - let _ = +let type_of_constructor env (c,u as cu) = + let () = let ((kn,_),_) = c in let mib = lookup_mind kn env in - check_hyps_inclusion env constr mib.mind_hyps in + check_hyps_inclusion env mkConstructU cu mib.mind_hyps + in let specif = lookup_mind_specif env (inductive_of_constructor c) in let t,cst = constrained_type_of_constructor cu specif in let () = check_constraints cst env in - (make_judge constr t) + t (* Case. *) -let check_branch_types env (ind,u) cj (lfj,explft) = - try conv_leq_vecti env (Array.map j_type lfj) explft +let check_branch_types env (ind,u) c ct lft explft = + try conv_leq_vecti env lft explft with NotConvertibleVect i -> - error_ill_formed_branch env cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i) + error_ill_formed_branch env c ((ind,i+1),u) lft.(i) explft.(i) | Invalid_argument _ -> - error_number_branches env cj (Array.length explft) + error_number_branches env (make_judge c ct) (Array.length explft) -let judge_of_case env ci pj cj lfj = +let type_of_case env ci p pt c ct lf lft = let (pind, _ as indspec) = - try find_rectype env cj.uj_type - with Not_found -> error_case_not_inductive env cj in + try find_rectype env ct + with Not_found -> error_case_not_inductive env (make_judge c ct) in let () = check_case_info env pind ci in let (bty,rslty) = - type_case_branches env indspec pj cj.uj_val in - let () = check_branch_types env pind cj (lfj,bty) in - ({ uj_val = mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, - Array.map j_val lfj); - uj_type = rslty }) + type_case_branches env indspec (make_judge p pt) c in + let () = check_branch_types env pind c ct lft bty in + rslty -let judge_of_projection env p cj = +let type_of_projection env p c ct = let pb = lookup_projection p env in let (ind,u), args = - try find_rectype env cj.uj_type - with Not_found -> error_case_not_inductive env cj + try find_rectype env ct + with Not_found -> error_case_not_inductive env (make_judge c ct) in - assert(eq_mind pb.proj_ind (fst ind)); - let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in - let ty = substl (cj.uj_val :: List.rev args) ty in - {uj_val = mkProj (p,cj.uj_val); - uj_type = ty} + assert(eq_mind pb.proj_ind (fst ind)); + let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in + substl (c :: List.rev args) ty + (* Fixpoints. *) (* Checks the type of a general (co)fixpoint, i.e. without checking *) (* the specific guard condition. *) -let type_fixpoint env lna lar vdefj = - let lt = Array.length vdefj in +let check_fixpoint env lna lar vdef vdeft = + let lt = Array.length vdeft in assert (Int.equal (Array.length lar) lt); try - conv_leq_vecti env (Array.map j_type vdefj) (Array.map (fun ty -> lift lt ty) lar) + conv_leq_vecti env vdeft (Array.map (fun ty -> lift lt ty) lar) with NotConvertibleVect i -> - error_ill_typed_rec_body env i lna vdefj lar + error_ill_typed_rec_body env i lna (make_judgev vdef vdeft) lar (************************************************************************) (************************************************************************) @@ -419,150 +339,254 @@ let type_fixpoint env lna lar vdefj = Ind et Constructsi un jour cela devient des constructions arbitraires et non plus des variables *) let rec execute env cstr = + let open Context.Rel.Declaration in match kind_of_term cstr with (* Atomic terms *) | Sort (Prop c) -> - judge_of_prop_contents c + type1 | Sort (Type u) -> - judge_of_type u + type_of_type u | Rel n -> - judge_of_relative env n + type_of_relative env n | Var id -> - judge_of_variable env id + type_of_variable env id | Const c -> - judge_of_constant env c + type_of_constant env c | Proj (p, c) -> - let cj = execute env c in - judge_of_projection env p cj + let ct = execute env c in + type_of_projection env p c ct (* Lambda calculus operators *) | App (f,args) -> - let jl = execute_array env args in - let j = + let argst = execute_array env args in + let ft = match kind_of_term f with - | Ind ind when Environ.template_polymorphic_pind ind env -> - (* Sort-polymorphism of inductive types *) - let args = Array.map (fun j -> lazy j.uj_type) jl in - judge_of_inductive_knowing_parameters env ind args - | Const cst when Environ.template_polymorphic_pconstant cst env -> - (* Sort-polymorphism of constant *) - let args = Array.map (fun j -> lazy j.uj_type) jl in - judge_of_constant_knowing_parameters env cst args - | _ -> - (* No sort-polymorphism *) - execute env f + | Ind ind when Environ.template_polymorphic_pind ind env -> + let args = Array.map (fun t -> lazy t) argst in + type_of_inductive_knowing_parameters env ind args + | Const cst when Environ.template_polymorphic_pconstant cst env -> + let args = Array.map (fun t -> lazy t) argst in + type_of_constant_knowing_parameters env cst args + | _ -> + (* No template polymorphism *) + execute env f in - judge_of_apply env j jl + + type_of_apply env f ft args argst | Lambda (name,c1,c2) -> - let varj = execute_type env c1 in - let env1 = push_rel (LocalAssum (name,varj.utj_val)) env in - let j' = execute env1 c2 in - judge_of_abstraction env name varj j' + let _ = execute_is_type env c1 in + let env1 = push_rel (LocalAssum (name,c1)) env in + let c2t = execute env1 c2 in + type_of_abstraction env name c1 c2t | Prod (name,c1,c2) -> - let varj = execute_type env c1 in - let env1 = push_rel (LocalAssum (name,varj.utj_val)) env in - let varj' = execute_type env1 c2 in - judge_of_product env name varj varj' + let vars = execute_is_type env c1 in + let env1 = push_rel (LocalAssum (name,c1)) env in + let vars' = execute_is_type env1 c2 in + type_of_product env name vars vars' | LetIn (name,c1,c2,c3) -> - let j1 = execute env c1 in - let j2 = execute_type env c2 in - let _ = judge_of_cast env j1 DEFAULTcast j2 in - let env1 = push_rel (LocalDef (name,j1.uj_val,j2.utj_val)) env in - let j' = execute env1 c3 in - judge_of_letin env name j1 j2 j' + let c1t = execute env c1 in + let _c2s = execute_is_type env c2 in + let () = check_cast env c1 c1t DEFAULTcast c2 in + let env1 = push_rel (LocalDef (name,c1,c2)) env in + let c3t = execute env1 c3 in + subst1 c1 c3t | Cast (c,k,t) -> - let cj = execute env c in - let tj = execute_type env t in - judge_of_cast env cj k tj + let ct = execute env c in + let _ts = (check_type env t (execute env t)) in + let () = check_cast env c ct k t in + t (* Inductive types *) | Ind ind -> - judge_of_inductive env ind + type_of_inductive env ind | Construct c -> - judge_of_constructor env c + type_of_constructor env c | Case (ci,p,c,lf) -> - let cj = execute env c in - let pj = execute env p in - let lfj = execute_array env lf in - judge_of_case env ci pj cj lfj + let ct = execute env c in + let pt = execute env p in + let lft = execute_array env lf in + type_of_case env ci p pt c ct lf lft | Fix ((vn,i as vni),recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let fix = (vni,recdef') in - check_fix env fix; - make_judge (mkFix fix) fix_ty + check_fix env fix; fix_ty | CoFix (i,recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let cofix = (i,recdef') in - check_cofix env cofix; - (make_judge (mkCoFix cofix) fix_ty) + check_cofix env cofix; fix_ty (* Partial proofs: unsupported by the kernel *) | Meta _ -> - anomaly (Pp.str "the kernel does not support metavariables") + anomaly (Pp.str "the kernel does not support metavariables.") | Evar _ -> - anomaly (Pp.str "the kernel does not support existential variables") + anomaly (Pp.str "the kernel does not support existential variables.") -and execute_type env constr = - let j = execute env constr in - type_judgment env j +and execute_is_type env constr = + let t = execute env constr in + check_type env constr t and execute_recdef env (names,lar,vdef) i = - let larj = execute_array env lar in - let lara = Array.map (assumption_of_judgment env) larj in + let lart = execute_array env lar in + let lara = Array.map2 (check_assumption env) lar lart in let env1 = push_rec_types (names,lara,vdef) env in - let vdefj = execute_array env1 vdef in - let vdefv = Array.map j_val vdefj in - let () = type_fixpoint env1 names lara vdefj in - (lara.(i),(names,lara,vdefv)) + let vdeft = execute_array env1 vdef in + let () = check_fixpoint env1 names lara vdef vdeft in + (lara.(i),(names,lara,vdef)) and execute_array env = Array.map (execute env) (* Derived functions *) let infer env constr = - let j = execute env constr in - assert (eq_constr j.uj_val constr); - j + let t = execute env constr in + make_judge constr t + +let infer = + if Flags.profile then + let infer_key = Profile.declare_profile "Fast_infer" in + Profile.profile2 infer_key (fun b c -> infer b c) + else (fun b c -> infer b c) + +let assumption_of_judgment env {uj_val=c; uj_type=t} = + check_assumption env c t -(* let infer_key = Profile.declare_profile "infer" *) -(* let infer = Profile.profile2 infer_key infer *) +let type_judgment env {uj_val=c; uj_type=t} = + let s = check_type env c t in + {utj_val = c; utj_type = s } let infer_type env constr = - let j = execute_type env constr in - j + let t = execute env constr in + let s = check_type env constr t in + {utj_val = constr; utj_type = s} let infer_v env cv = let jv = execute_array env cv in - jv + make_judgev cv jv (* Typing of several terms. *) let infer_local_decl env id = function - | LocalDefEntry c -> - let j = infer env c in - LocalDef (Name id, j.uj_val, j.uj_type) - | LocalAssumEntry c -> - let j = infer env c in - LocalAssum (Name id, assumption_of_judgment env j) + | Entries.LocalDefEntry c -> + let t = execute env c in + RelDecl.LocalDef (Name id, c, t) + | Entries.LocalAssumEntry c -> + let t = execute env c in + RelDecl.LocalAssum (Name id, check_assumption env c t) let infer_local_decls env decls = let rec inferec env = function | (id, d) :: l -> let (env, l) = inferec env l in let d = infer_local_decl env id d in - (push_rel d env, Context.Rel.add d l) - | [] -> (env, Context.Rel.empty) in + (push_rel d env, Context.Rel.add d l) + | [] -> (env, Context.Rel.empty) + in inferec env decls + +let judge_of_prop = make_judge mkProp type1 +let judge_of_set = make_judge mkSet type1 +let judge_of_type u = make_judge (mkType u) (type_of_type u) + +let judge_of_prop_contents = function + | Null -> judge_of_prop + | Pos -> judge_of_set + +let judge_of_relative env k = make_judge (mkRel k) (type_of_relative env k) + +let judge_of_variable env x = make_judge (mkVar x) (type_of_variable env x) + +let judge_of_constant env cst = make_judge (mkConstU cst) (type_of_constant env cst) +let judge_of_constant_knowing_parameters env cst args = + make_judge (mkConstU cst) (type_of_constant_knowing_parameters env cst args) + +let judge_of_projection env p cj = + make_judge (mkProj (p,cj.uj_val)) (type_of_projection env p cj.uj_val cj.uj_type) + +let dest_judgev v = + Array.map j_val v, Array.map j_type v + +let judge_of_apply env funj argjv = + let args, argtys = dest_judgev argjv in + make_judge (mkApp (funj.uj_val, args)) (type_of_apply env funj.uj_val funj.uj_type args argtys) + +let judge_of_abstraction env x varj bodyj = + make_judge (mkLambda (x, varj.utj_val, bodyj.uj_val)) + (type_of_abstraction env x varj.utj_val bodyj.uj_type) + +let judge_of_product env x varj outj = + make_judge (mkProd (x, varj.utj_val, outj.utj_val)) + (mkSort (sort_of_product env varj.utj_type outj.utj_type)) + +let judge_of_letin env name defj typj j = + make_judge (mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val)) + (subst1 defj.uj_val j.uj_type) + +let judge_of_cast env cj k tj = + let () = check_cast env cj.uj_val cj.uj_type k tj.utj_val in + let c = match k with | REVERTcast -> cj.uj_val | _ -> mkCast (cj.uj_val, k, tj.utj_val) in + make_judge c tj.utj_val + +let judge_of_inductive env indu = + make_judge (mkIndU indu) (type_of_inductive env indu) + +let judge_of_constructor env cu = + make_judge (mkConstructU cu) (type_of_constructor env cu) + +let judge_of_case env ci pj cj lfj = + let lf, lft = dest_judgev lfj in + make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) + (type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft) + +let type_of_projection_constant env (p,u) = + let cst = Projection.constant p in + let cb = lookup_constant cst env in + match cb.const_proj with + | Some pb -> + if cb.const_polymorphic then + Vars.subst_instance_constr u pb.proj_type + else pb.proj_type + | None -> raise (Invalid_argument "type_of_projection: not a projection") + +(* Instantiation of terms on real arguments. *) + +(* Make a type polymorphic if an arity *) + +let extract_level env p = + let _,c = dest_prod_assum env p in + match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None + +let extract_context_levels env l = + let fold l = function + | RelDecl.LocalAssum (_,p) -> extract_level env p :: l + | RelDecl.LocalDef _ -> l + in + List.fold_left fold [] l + +let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} = + let params, ccl = dest_prod_assum env t in + match kind_of_term ccl with + | Sort (Type u) -> + let ind, l = decompose_app (whd_all env c) in + if isInd ind && List.is_empty l then + let mis = lookup_mind_specif env (fst (destInd ind)) in + let nparams = Inductive.inductive_params mis in + let paramsl = CList.lastn nparams params in + let param_ccls = extract_context_levels env paramsl in + let s = { template_param_levels = param_ccls; template_level = u} in + TemplateArity (params,s) + else RegularArity t + | _ -> + RegularArity t diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 2112284ea6..007acae604 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -15,7 +15,7 @@ open Declarations (** {6 Typing functions (not yet tagged as safe) } - They return unsafe judgments that are "in context" of a set of + They return unsafe judgments that are "in context" of a set of (local) universe variables (the ones that appear in the term) and associated constraints. In case of polymorphic definitions, these variables and constraints will be generalized. @@ -91,9 +91,6 @@ val judge_of_cast : val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment -(* val judge_of_inductive_knowing_parameters : *) -(* env -> inductive -> unsafe_judgment array -> unsafe_judgment *) - val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment (** {6 Type of Cases. } *) @@ -101,24 +98,15 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -(** Typecheck general fixpoint (not checking guard conditions) *) -val type_fixpoint : env -> Name.t array -> types array - -> unsafe_judgment array -> unit - -val type_of_constant : env -> pconstant -> types constrained - val type_of_constant_type : env -> constant_type -> types -val type_of_projection : env -> Names.projection puniverses -> types +val type_of_projection_constant : env -> Names.projection puniverses -> types val type_of_constant_in : env -> pconstant -> types val type_of_constant_type_knowing_parameters : env -> constant_type -> types Lazy.t array -> types -val type_of_constant_knowing_parameters : - env -> pconstant -> types Lazy.t array -> types constrained - val type_of_constant_knowing_parameters_in : env -> pconstant -> types Lazy.t array -> types @@ -127,4 +115,4 @@ val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment -> constant_type (** Check that hyps are included in env and fails with error otherwise *) -val check_hyps_inclusion : env -> constr -> Context.section_context -> unit +val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Context.Named.t -> unit diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 4884d0deb1..487257a776 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -132,7 +132,7 @@ let rec repr g u = let a = try UMap.find u g.entries with Not_found -> CErrors.anomaly ~label:"Univ.repr" - (str"Universe " ++ Level.pr u ++ str" undefined") + (str"Universe " ++ Level.pr u ++ str" undefined.") in match a with | Equiv v -> repr g v @@ -354,13 +354,15 @@ let get_new_edges g to_merge = UMap.empty to_merge in let ltle = - UMap.fold (fun _ n acc -> - UMap.merge (fun _ strict1 strict2 -> - match strict1, strict2 with - | Some true, _ | _, Some true -> Some true - | _, _ -> Some false) - acc n.ltle) - to_merge_lvl UMap.empty + let fold _ n acc = + let fold u strict acc = + if strict then UMap.add u strict acc + else if UMap.mem u acc then acc + else UMap.add u false acc + in + UMap.fold fold n.ltle acc + in + UMap.fold fold to_merge_lvl UMap.empty in let ltle, _ = clean_ltle g ltle in let ltle = diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index e95cf4d1cb..935a3cab4a 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -17,6 +17,7 @@ type universes = t type 'a check_function = universes -> 'a -> 'a -> bool val check_leq : universe check_function val check_eq : universe check_function +val check_eq_level : universe_level check_function (** The empty graph of universes *) val empty_universes : universes @@ -61,3 +62,6 @@ val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds val dump_universes : (constraint_type -> string -> string -> unit) -> universes -> unit + +(** {6 Debugging} *) +val check_universes_invariants : universes -> unit diff --git a/kernel/univ.ml b/kernel/univ.ml index 09f884ecd0..d53dd8e733 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -440,10 +440,6 @@ struct let set = make Level.set let type1 = hcons (Level.set, 1) - let is_prop = function - | (l,0) -> Level.is_prop l - | _ -> false - let is_small = function | (l,0) -> Level.is_small l | _ -> false @@ -785,7 +781,7 @@ let enforce_eq_level u v c = let enforce_eq u v c = match Universe.level u, Universe.level v with | Some u, Some v -> enforce_eq_level u v c - | _ -> anomaly (Pp.str "A universe comparison can only happen between variables") + | _ -> anomaly (Pp.str "A universe comparison can only happen between variables.") let check_univ_eq u v = Universe.equal u v @@ -805,13 +801,13 @@ let constraint_add_leq v u c = else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then if Level.equal x y then (* u+(k+1) <= u *) raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u, None)) - else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints") + else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints.") else if j = 0 then Constraint.add (x,Le,y) c else (* j >= 1 *) (* m = n + k, u <= v+k *) if Level.equal x y then c (* u <= u+k, trivial *) else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *) - else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints") + else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints.") let check_univ_leq_one u v = Universe.exists (Expr.leq u) v @@ -986,7 +982,7 @@ let enforce_eq_instances x y = let ax = Instance.to_array x and ay = Instance.to_array y in if Array.length ax != Array.length ay then anomaly (Pp.(++) (Pp.str "Invalid argument: enforce_eq_instances called with") - (Pp.str " instances of different lengths")); + (Pp.str " instances of different lengths.")); CArray.fold_right2 enforce_eq_level ax ay type universe_instance = Instance.t diff --git a/kernel/vars.ml b/kernel/vars.ml index 2ca749d505..629de80f7c 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -8,7 +8,8 @@ open Names open Esubst -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration (*********************) (* Occurring *) @@ -26,7 +27,7 @@ let closedn n c = in try closed_rec n c; true with LocalOccur -> false -(* [closed0 M] is true iff [M] is a (deBruijn) closed term *) +(* [closed0 M] is true iff [M] is a (de Bruijn) closed term *) let closed0 c = closedn 0 c @@ -160,25 +161,35 @@ let substnl laml n c = substn_many (make_subst laml) n c let substl laml c = substn_many (make_subst laml) 0 c let subst1 lam c = substn_many [|make_substituend lam|] 0 c -let substnl_decl laml k r = map_constr (fun c -> substnl laml k c) r -let substl_decl laml r = map_constr (fun c -> substnl laml 0 c) r -let subst1_decl lam r = map_constr (fun c -> subst1 lam c) r +let substnl_decl laml k r = RelDecl.map_constr (fun c -> substnl laml k c) r +let substl_decl laml r = RelDecl.map_constr (fun c -> substnl laml 0 c) r +let subst1_decl lam r = RelDecl.map_constr (fun c -> subst1 lam c) r (* Build a substitution from an instance, inserting missing let-ins *) let subst_of_rel_context_instance sign l = let rec aux subst sign l = + let open RelDecl in match sign, l with | LocalAssum _ :: sign', a::args' -> aux (a::subst) sign' args' | LocalDef (_,c,_)::sign', args' -> aux (substl subst c :: subst) sign' args' | [], [] -> subst - | _ -> CErrors.anomaly (Pp.str "Instance and signature do not match") + | _ -> CErrors.anomaly (Pp.str "Instance and signature do not match.") in aux [] (List.rev sign) l let adjust_subst_to_rel_context sign l = List.rev (subst_of_rel_context_instance sign l) +let adjust_rel_to_rel_context sign n = + let rec aux sign = + let open RelDecl in + match sign with + | LocalAssum _ :: sign' -> let (n',p) = aux sign' in (n'+1,p) + | LocalDef (_,c,_)::sign' -> let (n',p) = aux sign' in (n'+1,if n'<n then p+1 else p) + | [] -> (0,n) + in snd (aux sign) + (* (thin_val sigma) removes identity substitutions from sigma *) let rec thin_val = function diff --git a/kernel/vars.mli b/kernel/vars.mli index 574d50eccb..df5c55118f 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -11,10 +11,10 @@ open Constr (** {6 Occur checks } *) -(** [closedn n M] is true iff [M] is a (deBruijn) closed term under n binders *) +(** [closedn n M] is true iff [M] is a (de Bruijn) closed term under n binders *) val closedn : int -> constr -> bool -(** [closed0 M] is true iff [M] is a (deBruijn) closed term *) +(** [closed0 M] is true iff [M] is a (de Bruijn) closed term *) val closed0 : constr -> bool (** [noccurn n M] returns true iff [Rel n] does NOT occur in term [M] *) @@ -73,6 +73,10 @@ val subst_of_rel_context_instance : Context.Rel.t -> constr list -> substl (** For compatibility: returns the substitution reversed *) val adjust_subst_to_rel_context : Context.Rel.t -> constr list -> constr list +(** Take an index in an instance of a context and returns its index wrt to + the full context (e.g. 2 in [x:A;y:=b;z:C] is 3, i.e. a reference to z) *) +val adjust_rel_to_rel_context : ('a, 'b) Context.Rel.pt -> int -> int + (** [substnl [a₁;...;an] k c] substitutes in parallel [a₁],...,[an] for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates accordingly indexes in [an],...,[a1] and [c]. In terms of typing, if diff --git a/kernel/vm.ml b/kernel/vm.ml index 53483a2220..21c1225cc4 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -236,7 +236,7 @@ let uni_lvl_val (v : values) : Univ.universe_level = in CErrors.anomaly Pp.( strbrk "Parsing virtual machine value expected universe level, got " - ++ pr) + ++ pr ++ str ".") let rec whd_accu a stk = let stk = @@ -285,7 +285,7 @@ let rec whd_accu a stk = end | tg -> CErrors.anomaly - Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg) + Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg ++ str ".") external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" @@ -308,7 +308,7 @@ let whd_val : values -> whd = | 1 -> Vfix(Obj.obj o, None) | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) - | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work")) + | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work.")) else Vconstr_block(Obj.obj o) |