diff options
Diffstat (limited to 'kernel')
41 files changed, 925 insertions, 1201 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index fe9ec5794..b1dd26119 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 diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 810c34699..94ca4c72d 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 b1fc0c85d..57b397e6f 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 f13620e10..40c1e027d 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 ce20751ab..5a7561bf5 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -81,27 +81,27 @@ 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 @@ -235,6 +235,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 *) (****************************************************************************) diff --git a/kernel/constr.mli b/kernel/constr.mli index 42d298e3b..700c235e6 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -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 4e53b73a2..abb284f22 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 b5f3904d2..0c666a25d 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 + + (** 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 - val to_tuple : t -> Id.t * Constr.t option * Constr.t - val of_tuple : Id.t * Constr.t option * Constr.t -> t + (** 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. 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 + 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 + 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 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/cooking.ml b/kernel/cooking.ml index 134599150..a9f212393 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -21,6 +21,8 @@ open Declarations open Environ open Univ +module NamedDecl = Context.Named.Declaration + (*s Cooking the constants. *) let pop_dirpath p = match DirPath.repr p with @@ -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 327e697d2..7d47eba23 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 c27cb0487..40595f944 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.mli index f89773fcc..7821ea20f 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -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 @@ -78,7 +79,7 @@ type typing_flags = { (* some contraints are in constant_constraints, some other may be in * the OpaueDef *) 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 211e5e062..0a822d6fa 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 5287a009e..1e07c9690 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 16ddfac64..9986f439a 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 *) @@ -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 diff --git a/kernel/environ.mli b/kernel/environ.mli index 6ac00088b..b7431dbe5 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 bd91c689d..000000000 --- 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 41cff607e..000000000 --- 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 de97268b3..2ff419338 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -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 3c4c2796e..d8d365c34 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -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 diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 15f213ce9..4c540a6d7 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -32,7 +32,6 @@ Type_errors Modops Inductive Typeops -Fast_typeops Indtypes Cooking Term_typing diff --git a/kernel/names.ml b/kernel/names.ml index 1eb9a3175..ee8d838da 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -50,17 +50,20 @@ struct | None -> true | Some _ -> false + let of_bytes s = + let s = Bytes.to_string s in + check_soft s; + String.hcons s + let of_string s = let () = check_soft s in - let s = String.copy s in String.hcons s let of_string_soft s = let () = check_soft ~warn:false s in - let s = String.copy s in String.hcons s - let to_string id = String.copy id + let to_string id = id let print id = str id @@ -88,11 +91,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 @@ -601,7 +607,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. "cannonical 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 diff --git a/kernel/names.mli b/kernel/names.mli index feaedc775..be9b9422b 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -43,6 +43,7 @@ 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. @@ -82,6 +83,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]. *) @@ -368,8 +372,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 +(** A map whose keys are constants (values of the {!Constant.t} type). + Keys are ordered wrt. "cannonical 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 b17715a8f..d9659d681 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1848,10 +1848,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/nativelambda.ml b/kernel/nativelambda.ml index 91b40be7e..366f9a0a6 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -14,6 +14,8 @@ open Pre_env open Nativevalues open Nativeinstr +module RelDecl = Context.Rel.Declaration + (** This file defines the lambda code generation phase of the native compiler *) exception NotClosed @@ -727,8 +729,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 1c58c7445..6bd82170e 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -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) diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 8093df304..965ed67b0 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -491,12 +491,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 130f1eb03..d0593c0e0 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -21,8 +21,18 @@ 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 _ = @@ -42,21 +52,25 @@ 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) + 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) + 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) @@ -72,21 +86,21 @@ let discharge_direct_opaque ~cook_constr ci = function | 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 +111,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 +120,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 +143,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 5139cf051..3897d5e51 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 f211583e0..d14a254d3 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. *) @@ -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) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 1ae89347a..cd975ee9a 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) (********************************************************************) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index e3b87bbe1..caaaff1b8 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] @@ -361,7 +363,7 @@ 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 @@ -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 diff --git a/kernel/term.ml b/kernel/term.ml index 15f187e5c..e5a681375 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 @@ -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) diff --git a/kernel/term.mli b/kernel/term.mli index 60a3c7715..a9bb67705 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 @@ -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 6ce14c853..eeb9c421a 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 5071f0ad5..5e1763815 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 0c3a952b8..bd6032716 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 0059111c0..7d9a2aac0 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,95 +339,96 @@ 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 -> + (* Template sort-polymorphism of inductive types *) + 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 -> + (* Template sort-polymorphism of constants *) + let args = Array.map (fun t -> lazy t) argst in + type_of_constant_knowing_parameters env cst args + | _ -> + (* Full or no sort-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 _ -> @@ -516,53 +437,158 @@ let rec execute env cstr = | Evar _ -> 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 2112284ea..007acae60 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/vars.ml b/kernel/vars.ml index 2ca749d50..4affb5f9f 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 *) @@ -160,14 +161,15 @@ 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' -> @@ -179,6 +181,15 @@ let subst_of_rel_context_instance 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 574d50ecc..adeac422e 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -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 |