diff options
Diffstat (limited to 'kernel')
99 files changed, 815 insertions, 704 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 1b348ae777..4b45608ae5 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -97,7 +97,8 @@ if (sp - num_args < coq_stack_threshold) { \ several architectures. */ -#if defined(__GNUC__) && !defined(DEBUG) +#if defined(__GNUC__) && !defined(DEBUG) && !defined(__INTEL_COMPILER) \ + && !defined(__llvm__) #ifdef __mips__ #define PC_REG asm("$16") #define SP_REG asm("$17") @@ -126,7 +127,7 @@ if (sp - num_args < coq_stack_threshold) { \ #define SP_REG asm("%edi") #define ACCU_REG #endif -#if defined(PPC) || defined(_POWER) || defined(_IBMR2) +#if defined(__ppc__) || defined(__ppc64__) #define PC_REG asm("26") #define SP_REG asm("27") #define ACCU_REG asm("28") @@ -141,8 +142,9 @@ if (sp - num_args < coq_stack_threshold) { \ #define SP_REG asm("a4") #define ACCU_REG asm("d7") #endif -#if defined(__arm__) && !defined(__thumb2__) -#define PC_REG asm("r9") +/* OCaml PR#4953: these specific registers not available in Thumb mode */ +#if defined(__arm__) && !defined(__thumb__) +#define PC_REG asm("r6") #define SP_REG asm("r8") #define ACCU_REG asm("r7") #endif @@ -152,6 +154,17 @@ if (sp - num_args < coq_stack_threshold) { \ #define ACCU_REG asm("38") #define JUMPTBL_BASE_REG asm("39") #endif +#ifdef __x86_64__ +#define PC_REG asm("%r15") +#define SP_REG asm("%r14") +#define ACCU_REG asm("%r13") +#endif +#ifdef __aarch64__ +#define PC_REG asm("%x19") +#define SP_REG asm("%x20") +#define ACCU_REG asm("%x21") +#define JUMPTBL_BASE_REG asm("%x22") +#endif #endif #define CheckInt1() do{ \ diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 542a05fd25..a1c49bee95 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -105,7 +105,7 @@ value init_coq_vm(value unit) /* ML */ init_coq_interpreter(); /* Some predefined pointer code. - * It is typically contained in accumlator blocks whose tag is 0 and thus + * It is typically contained in accumulator blocks whose tag is 0 and thus * scanned by the GC, so make it look like an OCaml block. */ value accu_block = (value) coq_stat_alloc(2 * sizeof(value)); Hd_hp (accu_block) = Make_header (1, Abstract_tag, Caml_black); \ diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 412637c4b6..6be8a59aeb 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -226,7 +226,7 @@ let unfold_red kn = * this constant or abstraction. * * i_tab is the cache table of the results * - * ref_value_cache searchs in the tab, otherwise uses i_repr to + * ref_value_cache searches in the tab, otherwise uses i_repr to * compute the result and store it in the table. If the constant can't * be unfolded, returns None, but does not store this failure. * This * doesn't take the RESET into account. You mustn't keep such a table @@ -389,7 +389,7 @@ type clos_infos = { i_flags : reds; i_cache : infos_cache } -type clos_tab = fconstr constant_def KeyTable.t +type clos_tab = (fconstr, Empty.t) constant_def KeyTable.t let info_flags info = info.i_flags let info_env info = info.i_cache.i_env @@ -645,7 +645,7 @@ and subst_constr subst c = match [@ocaml.warning "-4"] Constr.kind c with and comp_subs el s = Esubst.lift_subst (fun el c -> lazy (to_constr el c)) el s -(* This function defines the correspondance between constr and +(* This function defines the correspondence between constr and fconstr. When we find a closure whose substitution is the identity, then we directly return the constr to avoid possibly huge reallocation. *) diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index b1b69dded8..027d5245c9 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -200,7 +200,7 @@ val whd_val : clos_infos -> clos_tab -> fconstr -> constr val whd_stack : clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack -(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding +(** [eta_expand_ind_stack env ind c s t] computes stacks corresponding to the conversion of the eta expansion of t, considered as an inhabitant of ind, and the Constructor c of this inductive type applied to arguments s. @@ -215,7 +215,7 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> (** Conversion auxiliary functions to do step by step normalisation *) (** [unfold_reference] unfolds references in a [fconstr] *) -val unfold_reference : clos_infos -> clos_tab -> table_key -> fconstr constant_def +val unfold_reference : clos_infos -> clos_tab -> table_key -> (fconstr, Util.Empty.t) constant_def (*********************************************************************** i This is for lazy debug *) diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index fdc93cfa89..d854cadd15 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 3f8174bd7b..6913371caf 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 7570004fe5..009db05ea2 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 423e7bbe65..06b380ef89 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 69f004307d..83d2a58d83 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -386,7 +386,7 @@ let rec is_tailcall = function | Klabel _ :: c -> is_tailcall c | _ -> None -(* Extention of the continuation *) +(* Extension of the continuation *) (* Add a Kpop n instruction in front of a continuation *) let rec add_pop n = function diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index 6a9550342c..814902a554 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -20,7 +20,7 @@ val compile : fail_on_error:bool -> (** init, fun, fv *) val compile_constant_body : fail_on_error:bool -> - env -> universes -> Constr.t Mod_subst.substituted constant_def -> + env -> universes -> (Constr.t Mod_subst.substituted, 'opaque) constant_def -> body_code option (** Shortcut of the previous function used during module strengthening *) diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index a84a7c0cf9..76e2515ea7 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index 41cc641dc8..9184164504 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names open Vmvalues diff --git a/kernel/constr.ml b/kernel/constr.ml index d74c96af84..8375316003 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/constr.mli b/kernel/constr.mli index 7fc57cdb8a..45ec8a7e64 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -141,7 +141,7 @@ val mkRef : GlobRef.t Univ.puniverses -> constr [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] presented as describe in [ci]. - [p] stucture is [fun args x -> "return clause"] + [p] structure is [fun args x -> "return clause"] [ac]{^ ith} element is ith constructor case presented as {e lambda construct_args (without params). case_term } *) diff --git a/kernel/context.ml b/kernel/context.ml index 290e85294b..2ef750ad69 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/context.mli b/kernel/context.mli index 7b67e54ba4..8f233613da 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index fe82353b70..7ce320381c 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index bc06cc21b6..918dc8c928 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 9b974c4ecc..0951b07d49 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -152,38 +152,45 @@ let abstract_constant_body c (hyps, subst) = let c = Vars.subst_vars subst c in it_mkLambda_or_LetIn c hyps -type recipe = { from : constant_body; info : Opaqueproof.cooking_info } +type recipe = { from : Opaqueproof.opaque constant_body; info : Opaqueproof.cooking_info } type inline = bool -type result = { - cook_body : constr Mod_subst.substituted constant_def; +type 'opaque result = { + cook_body : (constr Mod_subst.substituted, 'opaque) constant_def; cook_type : types; cook_universes : universes; - cook_private_univs : Univ.ContextSet.t option; cook_relevance : Sorts.relevance; cook_inline : inline; cook_context : Constr.named_context option; } -let on_body ml hy f = function - | Undef _ as x -> x - | Def cs -> Def (Mod_subst.from_val (f (Mod_subst.force_constr cs))) - | OpaqueDef o -> - OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f - { Opaqueproof.modlist = ml; abstract = hy } o) - | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked") - let expmod_constr_subst cache modlist subst c = let subst = Univ.make_instance_subst subst in let c = expmod_constr cache modlist c in Vars.subst_univs_level_constr subst c -let cook_constr { Opaqueproof.modlist ; abstract = (vars, subst, _) } c = - let cache = RefTable.create 13 in - let expmod = expmod_constr_subst cache modlist subst in - let hyps = Context.Named.map expmod vars in - let hyps = abstract_context hyps in - abstract_constant_body (expmod c) hyps +let discharge_abstract_universe_context subst abs_ctx auctx = + (** Given a named instance [subst := u₀ ... uₙ₋₁] together with an abstract + context [auctx0 := 0 ... n - 1 |= C{0, ..., n - 1}] of the same length, + and another abstract context relative to the former context + [auctx := 0 ... m - 1 |= C'{u₀, ..., uₙ₋₁, 0, ..., m - 1}], + construct the lifted abstract universe context + [0 ... n - 1 n ... n + m - 1 |= + C{0, ... n - 1} ∪ + C'{0, ..., n - 1, n, ..., n + m - 1} ] + together with the instance + [u₀ ... uₙ₋₁ Var(0) ... Var (m - 1)]. + *) + if (Univ.Instance.is_empty subst) then + (** Still need to take the union for the constraints between globals *) + subst, (AUContext.union abs_ctx auctx) + else + let open Univ in + let ainst = make_abstract_instance auctx in + let subst = Instance.append subst ainst in + let substf = make_instance_subst subst in + let auctx = Univ.subst_univs_level_abstract_universe_context substf auctx in + subst, (AUContext.union abs_ctx auctx) let lift_univs cb subst auctx0 = match cb.const_universes with @@ -191,28 +198,35 @@ let lift_univs cb subst auctx0 = assert (AUContext.is_empty auctx0); subst, (Monomorphic ctx) | Polymorphic auctx -> - (** Given a named instance [subst := u₀ ... uₙ₋₁] together with an abstract - context [auctx0 := 0 ... n - 1 |= C{0, ..., n - 1}] of the same length, - and another abstract context relative to the former context - [auctx := 0 ... m - 1 |= C'{u₀, ..., uₙ₋₁, 0, ..., m - 1}], - construct the lifted abstract universe context - [0 ... n - 1 n ... n + m - 1 |= - C{0, ... n - 1} ∪ - C'{0, ..., n - 1, n, ..., n + m - 1} ] - together with the instance - [u₀ ... uₙ₋₁ Var(0) ... Var (m - 1)]. - *) - if (Univ.Instance.is_empty subst) then - (** Still need to take the union for the constraints between globals *) - subst, (Polymorphic (AUContext.union auctx0 auctx)) - else - let ainst = Univ.make_abstract_instance auctx in - let subst = Instance.append subst ainst in - let substf = Univ.make_instance_subst subst in - let auctx' = Univ.subst_univs_level_abstract_universe_context substf auctx in - subst, (Polymorphic (AUContext.union auctx0 auctx')) - -let cook_constant ~hcons { from = cb; info } = + let subst, auctx = discharge_abstract_universe_context subst auctx0 auctx in + subst, (Polymorphic auctx) + +let cook_constr { Opaqueproof.modlist ; abstract } (c, priv) = + let cache = RefTable.create 13 in + let abstract, usubst, abs_ctx = abstract in + let usubst, priv = match priv with + | Opaqueproof.PrivateMonomorphic () -> + let () = assert (AUContext.is_empty abs_ctx) in + let () = assert (Instance.is_empty usubst) in + usubst, priv + | Opaqueproof.PrivatePolymorphic (univs, ctx) -> + let ainst = Instance.of_array (Array.init univs Level.var) in + let usubst = Instance.append usubst ainst in + let ctx = on_snd (Univ.subst_univs_level_constraints (Univ.make_instance_subst usubst)) ctx in + let univs = univs + AUContext.size abs_ctx in + usubst, Opaqueproof.PrivatePolymorphic (univs, ctx) + in + let expmod = expmod_constr_subst cache modlist usubst in + let hyps = Context.Named.map expmod abstract in + let hyps = abstract_context hyps in + let c = abstract_constant_body (expmod c) hyps in + (c, priv) + +let cook_constr infos c = + let fold info c = cook_constr info c in + List.fold_right fold infos c + +let cook_constant { from = cb; info } = let { Opaqueproof.modlist; abstract } = info in let cache = RefTable.create 13 in let abstract, usubst, abs_ctx = abstract in @@ -220,13 +234,13 @@ let cook_constant ~hcons { from = cb; info } = let expmod = expmod_constr_subst cache modlist usubst in let hyps0 = Context.Named.map expmod abstract in let hyps = abstract_context hyps0 in - let map c = - let c = abstract_constant_body (expmod c) hyps in - if hcons then Constr.hcons c else c - in - let body = on_body modlist (hyps0, usubst, abs_ctx) - map - cb.const_body + let map c = abstract_constant_body (expmod c) hyps in + let body = match cb.const_body with + | Undef _ as x -> x + | Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs))) + | OpaqueDef o -> + OpaqueDef (Opaqueproof.discharge_direct_opaque info o) + | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked") in let const_hyps = Context.Named.fold_outside (fun decl hyps -> @@ -234,15 +248,10 @@ let cook_constant ~hcons { from = cb; info } = hyps) hyps0 ~init:cb.const_hyps in let typ = abstract_constant_type (expmod cb.const_type) hyps in - let private_univs = Option.map (on_snd (Univ.subst_univs_level_constraints - (Univ.make_instance_subst usubst))) - cb.const_private_poly_univs - in { cook_body = body; cook_type = typ; cook_universes = univs; - cook_private_univs = private_univs; cook_relevance = cb.const_relevance; cook_inline = cb.const_inline_code; cook_context = Some const_hyps; @@ -251,4 +260,115 @@ let cook_constant ~hcons { from = cb; info } = (* let cook_constant_key = CProfile.declare_profile "cook_constant" *) (* let cook_constant = CProfile.profile2 cook_constant_key cook_constant *) +(********************************) +(* Discharging mutual inductive *) + +(* Replace + + Var(y1)..Var(yq):C1..Cq |- Ij:Bj + Var(y1)..Var(yq):C1..Cq; I1..Ip:B1..Bp |- ci : Ti + + by + + |- Ij: (y1..yq:C1..Cq)Bj + I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)] +*) + +let it_mkNamedProd_wo_LetIn b d = + List.fold_left (fun c d -> mkNamedProd_wo_LetIn d c) b d + +let abstract_inductive decls nparamdecls inds = + let open Entries in + let ntyp = List.length inds in + let ndecls = Context.Named.length decls in + let args = Context.Named.to_instance mkVar (List.rev decls) in + let args = Array.of_list args in + let subs = List.init ntyp (fun k -> lift ndecls (mkApp(mkRel (k+1),args))) in + let inds' = + List.map + (function (tname,arity,template,cnames,lc) -> + let lc' = List.map (Vars.substl subs) lc in + let lc'' = List.map (fun b -> it_mkNamedProd_wo_LetIn b decls) lc' in + let arity' = it_mkNamedProd_wo_LetIn arity decls in + (tname,arity',template,cnames,lc'')) + inds in + let nparamdecls' = nparamdecls + Array.length args in +(* To be sure to be the same as before, should probably be moved to cook_inductive *) + let params' = let (_,arity,_,_,_) = List.hd inds' in + let (params,_) = decompose_prod_n_assum nparamdecls' arity in + params + in + let ind'' = + List.map + (fun (a,arity,template,c,lc) -> + let _, short_arity = decompose_prod_n_assum nparamdecls' arity in + let shortlc = + List.map (fun c -> snd (decompose_prod_n_assum nparamdecls' c)) lc in + { mind_entry_typename = a; + mind_entry_arity = short_arity; + mind_entry_template = template; + mind_entry_consnames = c; + mind_entry_lc = shortlc }) + inds' + in (params',ind'') + +let refresh_polymorphic_type_of_inductive (_,mip) = + match mip.mind_arity with + | RegularArity s -> s.mind_user_arity, false + | TemplateArity ar -> + let ctx = List.rev mip.mind_arity_ctxt in + mkArity (List.rev ctx, Sorts.sort_of_univ ar.template_level), true + +let dummy_variance = let open Entries in function + | Monomorphic_entry _ -> assert false + | Polymorphic_entry (_,uctx) -> Array.make (Univ.UContext.size uctx) Univ.Variance.Irrelevant + +let cook_inductive { Opaqueproof.modlist; abstract } mib = + let open Entries in + let (section_decls, subst, abs_uctx) = abstract in + let nparamdecls = Context.Rel.length mib.mind_params_ctxt in + let subst, ind_univs = + match mib.mind_universes with + | Monomorphic ctx -> Univ.empty_level_subst, Monomorphic_entry ctx + | Polymorphic auctx -> + let subst, auctx = discharge_abstract_universe_context subst abs_uctx auctx in + let subst = Univ.make_instance_subst subst in + let nas = Univ.AUContext.names auctx in + let auctx = Univ.AUContext.repr auctx in + subst, Polymorphic_entry (nas, auctx) + in + let variance = match mib.mind_variance with + | None -> None + | Some _ -> Some (dummy_variance ind_univs) + in + let cache = RefTable.create 13 in + let discharge c = Vars.subst_univs_level_constr subst (expmod_constr cache modlist c) in + let inds = + Array.map_to_list + (fun mip -> + let ty, template = refresh_polymorphic_type_of_inductive (mib,mip) in + let arity = discharge ty in + let lc = Array.map discharge mip.mind_user_lc in + (mip.mind_typename, + arity, template, + Array.to_list mip.mind_consnames, + Array.to_list lc)) + mib.mind_packets in + let section_decls' = Context.Named.map discharge section_decls in + let (params',inds') = abstract_inductive section_decls' nparamdecls inds in + let record = match mib.mind_record with + | PrimRecord info -> + Some (Some (Array.map (fun (x,_,_,_) -> x) info)) + | FakeRecord -> Some None + | NotRecord -> None + in + { mind_entry_record = record; + mind_entry_finite = mib.mind_finite; + mind_entry_params = params'; + mind_entry_inds = inds'; + mind_entry_private = mib.mind_private; + mind_entry_variance = variance; + mind_entry_universes = ind_univs + } + let expmod_constr modlist c = expmod_constr (RefTable.create 13) modlist c diff --git a/kernel/cooking.mli b/kernel/cooking.mli index b0f143c47d..671cdf51fe 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -13,22 +13,25 @@ open Declarations (** {6 Cooking the constants. } *) -type recipe = { from : constant_body; info : Opaqueproof.cooking_info } +type recipe = { from : Opaqueproof.opaque constant_body; info : Opaqueproof.cooking_info } type inline = bool -type result = { - cook_body : constr Mod_subst.substituted constant_def; +type 'opaque result = { + cook_body : (constr Mod_subst.substituted, 'opaque) constant_def; cook_type : types; cook_universes : universes; - cook_private_univs : Univ.ContextSet.t option; cook_relevance : Sorts.relevance; cook_inline : inline; cook_context : Constr.named_context option; } -val cook_constant : hcons:bool -> recipe -> result -val cook_constr : Opaqueproof.cooking_info -> constr -> constr +val cook_constant : recipe -> Opaqueproof.opaque result +val cook_constr : Opaqueproof.cooking_info list -> + (constr * unit Opaqueproof.delayed_universes) -> (constr * unit Opaqueproof.delayed_universes) + +val cook_inductive : + Opaqueproof.cooking_info -> mutual_inductive_body -> Entries.mutual_inductive_entry (** {6 Utility functions used in module [Discharge]. } *) diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 8bef6aec42..6c9e73b50d 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli index 72c96b0b9f..3322c89aa9 100644 --- a/kernel/csymtable.mli +++ b/kernel/csymtable.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 5551742c02..dff19dee5e 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -22,11 +22,11 @@ type engagement = set_predicativity (** {6 Representation of constants (Definition/Axiom) } *) (** Non-universe polymorphic mode polymorphism (Coq 8.2+): inductives - and constants hiding inductives are implicitely polymorphic when + and constants hiding inductives are implicitly polymorphic when applied to parameters, on the universes appearing in the whnf of their parameters and their conclusion, in a template style. - In truely universe polymorphic mode, we always use RegularArity. + In truly universe polymorphic mode, we always use RegularArity. *) type template_arity = { @@ -47,10 +47,10 @@ type inline = int option transparent body, or an opaque one *) (* Global declarations (i.e. constants) can be either: *) -type 'a constant_def = +type ('a, 'opaque) constant_def = | Undef of inline (** a global assumption *) | Def of 'a (** or a transparent global definition *) - | OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *) + | OpaqueDef of 'opaque (** or an opaque global definition *) | Primitive of CPrimitives.t (** or a primitive operation *) type universes = @@ -87,14 +87,13 @@ type typing_flags = { (* some contraints are in constant_constraints, some other may be in * the OpaqueDef *) -type constant_body = { +type 'opaque constant_body = { const_hyps : Constr.named_context; (** New: younger hyp at top *) - const_body : Constr.t Mod_subst.substituted constant_def; + const_body : (Constr.t Mod_subst.substituted, 'opaque) constant_def; const_type : types; const_relevance : Sorts.relevance; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : universes; - const_private_poly_univs : Univ.ContextSet.t option; const_inline_code : bool; const_typing_flags : typing_flags; (** The typing options which were used for @@ -165,7 +164,7 @@ type one_inductive_body = { mind_nrealdecls : int; (** Length of realargs context (with let, no params) *) - mind_kelim : Sorts.family list; (** List of allowed elimination sorts *) + mind_kelim : Sorts.family; (** Highest allowed elimination sort *) mind_nf_lc : (rel_context * types) array; (** Head normalized constructor types so that their conclusion exposes the inductive type *) @@ -246,7 +245,7 @@ type module_alg_expr = (** A component of a module structure *) type structure_field_body = - | SFBconst of constant_body + | SFBconst of Opaqueproof.opaque constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body | SFBmodtype of module_type_body diff --git a/kernel/declareops.ml b/kernel/declareops.ml index de9a052096..7a553700e8 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -113,7 +113,6 @@ let subst_const_body sub cb = const_body_code = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_universes = cb.const_universes; - const_private_poly_univs = cb.const_private_poly_univs; const_relevance = cb.const_relevance; const_inline_code = cb.const_inline_code; const_typing_flags = cb.const_typing_flags } @@ -144,16 +143,11 @@ let hcons_universes cbu = | Polymorphic ctx -> Polymorphic (Univ.hcons_abstract_universe_context ctx) -let hcons_const_private_univs = function - | None -> None - | Some univs -> Some (Univ.hcons_universe_context_set univs) - let hcons_const_body cb = { cb with const_body = hcons_const_def cb.const_body; const_type = Constr.hcons cb.const_type; const_universes = hcons_universes cb.const_universes; - const_private_poly_univs = hcons_const_private_univs cb.const_private_poly_univs; } (** {6 Inductive types } *) diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 54a853fc81..5a1331afa9 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -26,21 +26,21 @@ val map_decl_arity : ('a -> 'c) -> ('b -> 'd) -> (** {6 Constants} *) -val subst_const_body : substitution -> constant_body -> constant_body +val subst_const_body : substitution -> Opaqueproof.opaque constant_body -> Opaqueproof.opaque constant_body (** Is there a actual body in const_body ? *) -val constant_has_body : constant_body -> bool +val constant_has_body : 'a constant_body -> bool -val constant_polymorphic_context : constant_body -> AUContext.t +val constant_polymorphic_context : 'a constant_body -> AUContext.t (** Is the constant polymorphic? *) -val constant_is_polymorphic : constant_body -> bool +val constant_is_polymorphic : 'a constant_body -> bool (** Return the universe context, in case the definition is polymorphic, otherwise the context is empty. *) -val is_opaque : constant_body -> bool +val is_opaque : 'a constant_body -> bool (** {6 Inductive types} *) @@ -83,7 +83,7 @@ val safe_flags : Conv_oracle.oracle -> typing_flags of the structure, but simply hash-cons all inner constr and other known elements *) -val hcons_const_body : constant_body -> constant_body +val hcons_const_body : 'a constant_body -> 'a constant_body val hcons_mind : mutual_inductive_body -> mutual_inductive_body val hcons_module_body : module_body -> module_body val hcons_module_type : module_type_body -> module_type_body diff --git a/kernel/dune b/kernel/dune index 5b23a705ae..4038bf5638 100644 --- a/kernel/dune +++ b/kernel/dune @@ -3,7 +3,7 @@ (synopsis "The Coq Kernel") (public_name coq.kernel) (wrapped false) - (modules (:standard \ genOpcodeFiles uint63_x86 uint63_amd64 write_uint63)) + (modules (:standard \ genOpcodeFiles uint63_i386_31 uint63_amd64_63 write_uint63)) (libraries lib byterun dynlink)) (executable @@ -14,15 +14,10 @@ (targets copcodes.ml) (action (with-stdout-to %{targets} (run ./genOpcodeFiles.exe copml)))) -(executable - (name write_uint63) - (modules write_uint63) - (libraries unix)) - (rule (targets uint63.ml) - (deps (:gen ./write_uint63.exe) uint63_x86.ml uint63_amd64.ml) - (action (run %{gen}))) + (deps (:gen-file uint63_%{ocaml-config:architecture}_%{ocaml-config:int_size}.ml)) + (action (copy# %{gen-file} %{targets}))) (documentation (package coq)) diff --git a/kernel/entries.ml b/kernel/entries.ml index a3d32267a7..2d29c3ee19 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -60,15 +60,14 @@ type mutual_inductive_entry = { type 'a proof_output = constr Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation -type 'a definition_entry = { - const_entry_body : 'a const_entry_body; +type definition_entry = { + const_entry_body : constr Univ.in_universe_context_set; (* List of section variables *) const_entry_secctx : Constr.named_context option; (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : types option; const_entry_universes : universes_entry; - const_entry_opaque : bool; const_entry_inline_code : bool } type section_def_entry = { @@ -78,6 +77,16 @@ type section_def_entry = { secdef_type : types option; } +type 'a opaque_entry = { + opaque_entry_body : 'a; + (* List of section variables *) + opaque_entry_secctx : Constr.named_context option; + (* State id on which the completion of type checking is reported *) + opaque_entry_feedback : Stateid.t option; + opaque_entry_type : types; + opaque_entry_universes : universes_entry; +} + type inline = int option (* inlining level, None for no inlining *) type parameter_entry = @@ -90,7 +99,8 @@ type primitive_entry = { } type 'a constant_entry = - | DefinitionEntry of 'a definition_entry + | DefinitionEntry of definition_entry + | OpaqueEntry of 'a const_entry_body opaque_entry | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry @@ -107,22 +117,3 @@ type module_entry = | MType of module_params_entry * module_struct_entry | MExpr of module_params_entry * module_struct_entry * module_struct_entry option - - -type seff_env = - [ `Nothing - (* The proof term and its universes. - Same as the constant_body's but not in an ephemeron *) - | `Opaque of Constr.t * Univ.ContextSet.t ] - -(** Not used by the kernel. *) -type side_effect_role = - | Subproof - | Schema of inductive * string - -type side_eff = { - seff_constant : Constant.t; - seff_body : Declarations.constant_body; - seff_env : seff_env; - seff_role : side_effect_role; -} diff --git a/kernel/environ.ml b/kernel/environ.ml index 97c9f8654a..32f9069747 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -46,7 +46,7 @@ type link_info = | LinkedInteractive of string | NotLinked -type constant_key = constant_body * (link_info ref * key) +type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key) type mind_key = mutual_inductive_body * link_info ref @@ -187,7 +187,7 @@ let match_named_context_val c = match c.env_named_ctx with let map_named_val f ctxt = let open Context.Named.Declaration in let fold accu d = - let d' = map_constr f d in + let d' = f d in let accu = if d == d' then accu else Id.Map.modify (get_id d) (fun _ (_, v) -> (d', v)) accu @@ -483,16 +483,6 @@ let constant_value_and_type env (kn, u) = in b', subst_instance_constr u cb.const_type, cst -let body_of_constant_body env cb = - let otab = opaque_tables env in - match cb.const_body with - | Undef _ | Primitive _ -> - None - | Def c -> - Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb) - | OpaqueDef o -> - Some (Opaqueproof.force_proof otab o, Declareops.constant_polymorphic_context cb) - (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant application. *) diff --git a/kernel/environ.mli b/kernel/environ.mli index 8c6bc105c7..a4cd576bcc 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -42,7 +42,7 @@ type link_info = type key = int CEphemeron.key option ref -type constant_key = constant_body * (link_info ref * key) +type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key) type mind_key = mutual_inductive_body * link_info ref @@ -134,9 +134,9 @@ val ids_of_named_context_val : named_context_val -> Id.Set.t (** [map_named_val f ctxt] apply [f] to the body and the type of each declarations. - *** /!\ *** [f t] should be convertible with t *) + *** /!\ *** [f t] should be convertible with t, and preserve the name *) val map_named_val : - (constr -> constr) -> named_context_val -> named_context_val + (named_declaration -> named_declaration) -> named_context_val -> named_context_val val push_named : Constr.named_declaration -> env -> env val push_named_context : Constr.named_context -> env -> env @@ -174,19 +174,19 @@ val reset_with_named_context : named_context_val -> env -> env val pop_rel_context : int -> env -> env (** Useful for printing *) -val fold_constants : (Constant.t -> constant_body -> 'a -> 'a) -> env -> 'a -> 'a +val fold_constants : (Constant.t -> Opaqueproof.opaque constant_body -> 'a -> 'a) -> env -> 'a -> 'a (** {5 Global constants } {6 Add entries to global environment } *) -val add_constant : Constant.t -> constant_body -> env -> env -val add_constant_key : Constant.t -> constant_body -> link_info -> +val add_constant : Constant.t -> Opaqueproof.opaque constant_body -> env -> env +val add_constant_key : Constant.t -> Opaqueproof.opaque constant_body -> link_info -> env -> env val lookup_constant_key : Constant.t -> env -> constant_key (** Looks up in the context of global constant names raises [Not_found] if the required path is not found *) -val lookup_constant : Constant.t -> env -> constant_body +val lookup_constant : Constant.t -> env -> Opaqueproof.opaque constant_body val evaluable_constant : Constant.t -> env -> bool (** New-style polymorphism *) @@ -215,12 +215,6 @@ val constant_value_and_type : env -> Constant.t puniverses -> polymorphic *) val constant_context : env -> Constant.t -> Univ.AUContext.t -(** Returns the body of the constant if it has any, and the polymorphic context - it lives in. For monomorphic constant, the latter is empty, and for - polymorphic constants, the term contains De Bruijn universe variables that - need to be instantiated. *) -val body_of_constant_body : env -> constant_body -> (Constr.constr * Univ.AUContext.t) option - (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant application. *) diff --git a/kernel/esubst.ml b/kernel/esubst.ml index 9fc3b11d78..f10cf20b42 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/esubst.mli b/kernel/esubst.mli index 475b64f472..400f91d302 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/evar.ml b/kernel/evar.ml index bbe143092b..a0bed31f68 100644 --- a/kernel/evar.ml +++ b/kernel/evar.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/evar.mli b/kernel/evar.mli index d14cdce27a..25a92d3e1d 100644 --- a/kernel/evar.mli +++ b/kernel/evar.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index 6564954dfd..a8a4ffce9c 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 4e6e595331..c8e04b9fee 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -232,18 +232,9 @@ let check_record data = (* - all_sorts in case of small, unitary Prop (not smashed) *) (* - logical_sorts in case of large, unitary Prop (smashed) *) -let all_sorts = [InSProp;InProp;InSet;InType] -let small_sorts = [InSProp;InProp;InSet] -let logical_sorts = [InSProp;InProp] -let sprop_sorts = [InSProp] - let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_} = - if not ind_squashed then all_sorts - else match Sorts.family (Sorts.sort_of_univ ind_univ) with - | InType -> assert false - | InSet -> small_sorts - | InProp -> logical_sorts - | InSProp -> sprop_sorts + if not ind_squashed then InType + else Sorts.family (Sorts.sort_of_univ ind_univ) (* Returns the list [x_1, ..., x_n] of levels contributing to template polymorphism. The elements x_k is None if the k-th parameter (starting diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index ad51af66a2..aaa0d6a149 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -22,7 +22,7 @@ open Declarations - for each inductive, (arity * constructors) (with params) * (indices * splayed constructor types) (both without params) - * allowed eliminations + * top allowed elimination *) val typecheck_inductive : env -> mutual_inductive_entry -> env @@ -31,5 +31,5 @@ val typecheck_inductive : env -> mutual_inductive_entry -> * Constr.rel_context * ((inductive_arity * Constr.types array) * (Constr.rel_context * (Constr.rel_context * Constr.types) array) * - Sorts.family list) + Sorts.family) array diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index bb3b0a538e..b0366d6ec0 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 1b8e4208ff..240ba4e2bb 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index d9335d39b5..cd969ea457 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -166,7 +166,7 @@ let make_subst env = (* template, it is identity substitution otherwise (ie. when u is *) (* already in the domain of the substitution) [remember_subst] will *) (* update its image [x] by [sup x u] in order not to forget the *) - (* dependency in [u] that remains to be fullfilled. *) + (* dependency in [u] that remains to be fulfilled. *) make (remember_subst u subst) (sign, exp, []) | _sign, [], _ -> (* Uniform parameters are exhausted *) @@ -289,7 +289,7 @@ let get_instantiated_arity (_ind,u) (mib,mip) params = let sign, s = mind_arity mip in full_inductive_instantiate mib u params sign, s -let elim_sorts (_,mip) = mip.mind_kelim +let elim_sort (_,mip) = mip.mind_kelim let is_private (mib,_) = mib.mind_private = Some true let is_primitive_record (mib,_) = @@ -305,12 +305,12 @@ let build_dependent_inductive ind (_,mip) params = @ Context.Rel.to_extended_list mkRel 0 realargs) (* This exception is local *) -exception LocalArity of (Sorts.family list * Sorts.family * Sorts.family * arity_error) option +exception LocalArity of (Sorts.family * Sorts.family * Sorts.family * arity_error) option let check_allowed_sort ksort specif = - if not (CList.exists (Sorts.family_equal ksort) (elim_sorts specif)) then + if not (Sorts.family_leq ksort (elim_sort specif)) then let s = inductive_sort_family (snd specif) in - raise (LocalArity (Some(elim_sorts specif, ksort,s,error_elim_explain ksort s))) + raise (LocalArity (Some(elim_sort specif, ksort,s,error_elim_explain ksort s))) let is_correct_arity env c pj ind specif params = let arsign,_ = get_instantiated_arity ind specif params in diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 997a620742..8c40c318c5 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -52,7 +52,7 @@ val type_of_inductive : env -> mind_specif puniverses -> types val type_of_inductive_knowing_parameters : env -> ?polyprop:bool -> mind_specif puniverses -> types Lazy.t array -> types -val elim_sorts : mind_specif -> Sorts.family list +val elim_sort : mind_specif -> Sorts.family val is_private : mind_specif -> bool val is_primitive_record : mind_specif -> bool diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 9397772415..c5ea32e157 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 8ab3d04402..b69e62b8a6 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 2de5faa6df..9305a91731 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -188,7 +188,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv = in let new_equiv = add_delta_resolver equiv new_mb.mod_delta in (* we propagate the new equality in the rest of the signature - with the identity substitution accompagned by the new resolver*) + with the identity substitution accompanied by the new resolver*) let id_subst = map_mp mp' mp' new_mb.mod_delta in let new_after = subst_structure id_subst after in before@(lab,SFBmodule new_mb')::new_after, new_equiv, cst diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index e74f455efe..aa8aa96746 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/modops.ml b/kernel/modops.ml index 4f992d3972..4808ed14e4 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -329,7 +329,6 @@ let strengthen_const mp_from l cb resolver = let u = Univ.make_abstract_instance (Declareops.constant_polymorphic_context cb) in { cb with const_body = Def (Mod_subst.from_val (mkConstU (con,u))); - const_private_poly_univs = None; const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) } let rec strengthen_mod mp_from mp_to mb = @@ -515,7 +514,7 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso = "Module M:=P." or "Module M. Include P. End M." We need to perform two operations to compute the body of M. - The first one is applying the substitution {P <- M} on the type of P - - The second one is strenghtening. *) + - The second one is strengthening. *) let strengthen_and_subst_mb mb mp include_b = match mb.mod_type with |NoFunctor struc -> @@ -608,11 +607,7 @@ let clean_bounded_mod_expr sign = (** {6 Stm machinery } *) let join_constant_body except otab cb = match cb.const_body with - | OpaqueDef o -> - (match Opaqueproof.uuid_opaque otab o with - | Some uuid when not(Future.UUIDSet.mem uuid except) -> - Opaqueproof.join_opaque otab o - | _ -> ()) + | OpaqueDef o -> Opaqueproof.join_opaque ~except otab o | _ -> () let join_structure except otab s = diff --git a/kernel/modops.mli b/kernel/modops.mli index 119ce2b359..badbd973ae 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/names.ml b/kernel/names.ml index 047a1d6525..85dc8267bb 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -671,6 +671,7 @@ module InductiveOrdered_env = struct let compare = ind_user_ord end +module Indset = Set.Make(InductiveOrdered) module Indmap = Map.Make(InductiveOrdered) module Indmap_env = Map.Make(InductiveOrdered_env) diff --git a/kernel/names.mli b/kernel/names.mli index 2238e932b0..65c5d6c139 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -481,6 +481,7 @@ type constructor = inductive (* designates the inductive type *) * int (* the index of the constructor BEWARE: indexing starts from 1. *) +module Indset : CSig.SetS with type elt = inductive module Indmap : CSig.MapS with type key = inductive module Constrmap : CSig.MapS with type key = constructor module Indmap_env : CSig.MapS with type key = inductive diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 3f791dfc22..fc9e69d9e3 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 96efa7faa5..955c4ad899 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -65,7 +65,7 @@ val empty_updates : code_location_updates val register_native_file : string -> unit val compile_constant_field : env -> string -> Constant.t -> - global list -> constant_body -> global list + global list -> 'a constant_body -> global list val compile_mind_field : ModPath.t -> Label.t -> global list -> mutual_inductive_body -> global list diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index d153f84e9c..a98523ba66 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli index 2111739d5e..9cacf0f4ef 100644 --- a/kernel/nativeconv.mli +++ b/kernel/nativeconv.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 62afd9df68..70b3beb2dc 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 446df1a1ea..f17339f84d 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 43c9676f05..94a8b1310a 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index e113350368..194efecd9a 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index 5d1b882361..1dbab6c690 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli index 31e5255fc4..168bf646af 100644 --- a/kernel/nativelibrary.mli +++ b/kernel/nativelibrary.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 3eb51ffc59..b3ad3949dc 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 58cb6e2c30..b5b4569a24 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 303cb06c55..e256466112 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -16,10 +16,27 @@ open Mod_subst type work_list = (Instance.t * Id.t array) Cmap.t * (Instance.t * Id.t array) Mindmap.t -type cooking_info = { - modlist : work_list; +type cooking_info = { + modlist : work_list; abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t } -type proofterm = (constr * Univ.ContextSet.t) Future.computation + +type 'a delayed_universes = +| PrivateMonomorphic of 'a +| PrivatePolymorphic of int * Univ.ContextSet.t + +type opaque_proofterm = cooking_info list * (Constr.t * unit delayed_universes) option + +type indirect_accessor = { + access_proof : DirPath.t -> int -> opaque_proofterm; + access_discharge : cooking_info list -> (Constr.t * unit delayed_universes) -> (Constr.t * unit delayed_universes); +} + +let drop_mono = function +| PrivateMonomorphic _ -> PrivateMonomorphic () +| PrivatePolymorphic _ as ctx -> ctx + +type proofterm = (constr * Univ.ContextSet.t delayed_universes) Future.computation + type opaque = | Indirect of substitution list * DirPath.t * int (* subst, lib, index *) | Direct of cooking_info list * proofterm @@ -36,20 +53,8 @@ let empty_opaquetab = { opaque_dir = DirPath.initial; } -(* hooks *) -let default_get_opaque dp _ = - CErrors.user_err Pp.(pr_sequence str ["Cannot access opaque proofs in library"; DirPath.to_string dp]) -let default_get_univ dp _ = - CErrors.user_err (Pp.pr_sequence Pp.str [ - "Cannot access universe constraints of opaque proofs in library "; - DirPath.to_string dp]) - -let get_opaque = ref default_get_opaque -let get_univ = ref default_get_univ - -let set_indirect_opaque_accessor f = (get_opaque := f) -let set_indirect_univ_accessor f = (get_univ := f) -(* /hooks *) +let not_here () = + CErrors.user_err Pp.(str "Cannot access opaque delayed proof") let create cu = Direct ([],cu) @@ -58,11 +63,19 @@ let turn_indirect dp o tab = match o with 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) -> - (** 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 *) + | Direct (d, cu) -> + (* Invariant: direct opaques only exist inside sections, we turn them + indirect as soon as we are at toplevel. At this moment, we perform + hashconsing of their contents, potentially as a future. *) + let hcons (c, u) = + let c = Constr.hcons c in + let u = match u with + | PrivateMonomorphic u -> PrivateMonomorphic (Univ.hcons_universe_context_set u) + | PrivatePolymorphic (n, u) -> PrivatePolymorphic (n, Univ.hcons_universe_context_set u) + in + (c, u) + in + let cu = Future.chain cu hcons in let id = tab.opaque_len in let opaque_val = Int.Map.add id (d,cu) tab.opaque_val in let opaque_dir = @@ -77,85 +90,82 @@ let subst_opaque sub = function | Indirect (s,dp,i) -> Indirect (sub::s,dp,i) | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.") -let iter_direct_opaque f = function +let discharge_direct_opaque ci = function | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") - | Direct (d,cu) -> - Direct (d,Future.chain cu (fun (c, u) -> f c; c, u)) + | Direct (d, cu) -> + Direct (ci :: d, cu) -let discharge_direct_opaque ~cook_constr ci = function - | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") - | Direct (d,cu) -> - Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u)) +let join except cu = match except with +| None -> ignore (Future.join cu) +| Some except -> + if Future.UUIDSet.mem (Future.uuid cu) except then () + else ignore (Future.join cu) -let join_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,cu) -> ignore(Future.join cu) +let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function + | Direct (_,cu) -> join except cu | Indirect (_,dp,i) -> if DirPath.equal dp odp then - let fp = snd (Int.Map.find i prfs) in - ignore(Future.join fp) + let (_, fp) = Int.Map.find i prfs in + join except fp -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 { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,cu) -> - fst(Future.force cu) +let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function + | Direct (d, cu) -> + let (c, u) = Future.force cu in + access.access_discharge d (c, drop_mono u) | Indirect (l,dp,i) -> - let pt = + let c, u = if DirPath.equal dp odp - then Future.chain (snd (Int.Map.find i prfs)) fst - else !get_opaque dp i in - let c = Future.force pt in - force_constr (List.fold_right subst_substituted l (from_val c)) - -let force_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,cu) -> snd(Future.force cu) + then + let (d, cu) = Int.Map.find i prfs in + let (c, u) = Future.force cu in + access.access_discharge d (c, drop_mono u) + else + let (d, cu) = access.access_proof dp i in + match cu with + | None -> not_here () + | Some (c, u) -> access.access_discharge d (c, u) + in + let c = force_constr (List.fold_right subst_substituted l (from_val c)) in + (c, u) + +let get_mono (_, u) = match u with +| PrivateMonomorphic ctx -> ctx +| PrivatePolymorphic _ -> Univ.ContextSet.empty + +let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function + | Direct (_,cu) -> + get_mono (Future.force cu) | Indirect (_,dp,i) -> if DirPath.equal dp odp - then snd (Future.force (snd (Int.Map.find i prfs))) - else match !get_univ dp i with - | None -> Univ.ContextSet.empty - | Some u -> Future.force u + then + let ( _, cu) = Int.Map.find i prfs in + get_mono (Future.force cu) + else Univ.ContextSet.empty -let get_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,cu) -> Some(Future.chain cu snd) - | Indirect (_,dp,i) -> - if DirPath.equal dp odp - then Some(Future.chain (snd (Int.Map.find i prfs)) snd) - else !get_univ dp i +let get_direct_constraints = function +| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") +| Direct (_, cu) -> + Future.chain cu get_mono -let get_proof { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,cu) -> Future.chain cu fst - | Indirect (l,dp,i) -> - let pt = - if DirPath.equal dp odp - then Future.chain (snd (Int.Map.find i prfs)) fst - else !get_opaque dp i in - Future.chain pt (fun c -> - force_constr (List.fold_right subst_substituted l (from_val c))) - module FMap = Future.UUIDMap -let a_constr = Future.from_val (mkRel 1) -let a_univ = Future.from_val Univ.ContextSet.empty -let a_discharge : cooking_info list = [] - -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 dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } = + let opaque_table = Array.make n ([], None) in let f2t_map = ref FMap.empty in - Int.Map.iter (fun n (d,cu) -> - let c, u = Future.split2 cu in - Future.sink u; - Future.sink c; - opaque_table.(n) <- c; - univ_table.(n) <- u; - disch_table.(n) <- d; - f2t_map := FMap.add (Future.uuid cu) n !f2t_map) - otab; - opaque_table, univ_table, disch_table, !f2t_map + let iter n (d, cu) = + let uid = Future.uuid cu in + let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in + let c = + if Future.is_val cu then + let (c, priv) = Future.force cu in + let priv = drop_mono priv in + Some (c, priv) + else if Future.UUIDSet.mem uid except then None + else + CErrors.anomaly + Pp.(str"Proof object "++int n++str" is not checked nor to be checked") + in + opaque_table.(n) <- (d, c) + in + let () = Int.Map.iter iter otab in + opaque_table, !f2t_map diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 5ea6da649b..7c53656c3c 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -21,7 +21,12 @@ open Mod_subst When it is [turn_indirect] the data is relocated to an opaque table and the [opaque] is turned into an index. *) -type proofterm = (constr * Univ.ContextSet.t) Future.computation +type 'a delayed_universes = +| PrivateMonomorphic of 'a +| PrivatePolymorphic of int * Univ.ContextSet.t + (** Number of surrounding bound universes + local constraints *) + +type proofterm = (constr * Univ.ContextSet.t delayed_universes) Future.computation type opaquetab type opaque @@ -35,49 +40,38 @@ val create : proofterm -> opaque used so far *) val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab -(** From a [opaque] back to a [constr]. This might use the - indirect opaque accessor configured below. *) -val force_proof : opaquetab -> opaque -> constr -val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t -val get_proof : opaquetab -> opaque -> constr Future.computation -val get_constraints : - opaquetab -> opaque -> Univ.ContextSet.t Future.computation option - -val subst_opaque : substitution -> opaque -> opaque -val iter_direct_opaque : (constr -> unit) -> opaque -> opaque - -type work_list = (Univ.Instance.t * Id.t array) Cmap.t * +type work_list = (Univ.Instance.t * Id.t array) Cmap.t * (Univ.Instance.t * Id.t array) Mindmap.t -type cooking_info = { - modlist : work_list; +type cooking_info = { + modlist : work_list; abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t } -(* The type has two caveats: - 1) cook_constr is defined after - 2) we have to store the input in the [opaque] in order to be able to - discharge it when turning a .vi into a .vo *) -val discharge_direct_opaque : - cook_constr:(constr -> constr) -> cooking_info -> opaque -> opaque - -val uuid_opaque : opaquetab -> opaque -> Future.UUID.t option -val join_opaque : opaquetab -> opaque -> unit - -val dump : opaquetab -> - Constr.t Future.computation array * - Univ.ContextSet.t Future.computation array * - cooking_info list array * - int Future.UUIDMap.t +type opaque_proofterm = cooking_info list * (Constr.t * unit delayed_universes) option +type indirect_accessor = { + access_proof : DirPath.t -> int -> opaque_proofterm; + access_discharge : cooking_info list -> + (Constr.t * unit delayed_universes) -> (Constr.t * unit delayed_universes); +} (** When stored indirectly, opaque terms are indexed by their library - dirpath and an integer index. The following two functions activate - this indirect storage, by telling how to store and retrieve terms. - Default creator always returns [None], preventing the creation of - any indirect link, and default accessor always raises an error. + dirpath and an integer index. The two functions above activate + this indirect storage, by telling how to retrieve terms. *) -val set_indirect_opaque_accessor : - (DirPath.t -> int -> constr Future.computation) -> unit -val set_indirect_univ_accessor : - (DirPath.t -> int -> Univ.ContextSet.t Future.computation option) -> unit +(** From a [opaque] back to a [constr]. This might use the + indirect opaque accessor given as an argument. *) +val force_proof : indirect_accessor -> opaquetab -> opaque -> constr * unit delayed_universes +val force_constraints : indirect_accessor -> opaquetab -> opaque -> Univ.ContextSet.t +val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation + +val subst_opaque : substitution -> opaque -> opaque + +val discharge_direct_opaque : + cooking_info -> opaque -> opaque + +val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit +val dump : ?except:Future.UUIDSet.t -> opaquetab -> + opaque_proofterm array * + int Future.UUIDMap.t diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 11ece78fe0..53f228c618 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 7dcafb7d7b..ab34d3a6dc 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index e1c4cec5b5..873c6af93d 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 09e8140308..2a7b390951 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/retypeops.ml b/kernel/retypeops.ml index 204dec3eda..a51b762f95 100644 --- a/kernel/retypeops.ml +++ b/kernel/retypeops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util diff --git a/kernel/retypeops.mli b/kernel/retypeops.mli index f30c541c3f..f4497be44b 100644 --- a/kernel/retypeops.mli +++ b/kernel/retypeops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** We can take advantage of non-cumulativity of SProp to avoid fully diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 673f025c75..a0cc2974d9 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -228,19 +228,10 @@ let check_engagement env expected_impredicative_set = (** {6 Stm machinery } *) -let get_opaque_body env cbo = - match cbo.const_body with - | Undef _ -> assert false - | Primitive _ -> assert false - | Def _ -> `Nothing - | OpaqueDef opaque -> - `Opaque - (Opaqueproof.force_proof (Environ.opaque_tables env) opaque, - Opaqueproof.force_constraints (Environ.opaque_tables env) opaque) - type side_effect = { from_env : Declarations.structure_body CEphemeron.key; - eff : Entries.side_eff list; + seff_constant : Constant.t; + seff_body : Constr.t Declarations.constant_body; } module SideEffects : @@ -254,11 +245,9 @@ end = struct module SeffOrd = struct -open Entries type t = side_effect let compare e1 e2 = - let cmp e1 e2 = Constant.CanOrd.compare e1.seff_constant e2.seff_constant in - List.compare cmp e1.eff e2.eff + Constant.CanOrd.compare e1.seff_constant e2.seff_constant end module SeffSet = Set.Make(SeffOrd) @@ -279,42 +268,36 @@ end type private_constants = SideEffects.t let side_effects_of_private_constants l = - let ans = List.rev (SideEffects.repr l) in - List.map_append (fun { eff; _ } -> eff) ans + List.rev (SideEffects.repr l) -let empty_private_constants = SideEffects.empty -let add_private mb eff effs = - let from_env = CEphemeron.create mb in - SideEffects.add { eff; from_env } effs -let concat_private = SideEffects.concat +(* Only used to push in an Environ.env. *) +let lift_constant c = + let body = match c.const_body with + | OpaqueDef _ -> Undef None + | Def _ | Undef _ | Primitive _ as body -> body + in + { c with const_body = body } -let make_eff env cst r = - let open Entries in - let cbo = Environ.lookup_constant cst env.env in - { - seff_constant = cst; - seff_body = cbo; - seff_env = get_opaque_body env.env cbo; - seff_role = r; - } +let map_constant f c = + let body = match c.const_body with + | OpaqueDef o -> OpaqueDef (f o) + | Def _ | Undef _ | Primitive _ as body -> body + in + { c with const_body = body } -let private_con_of_con env c = - let open Entries in - let eff = [make_eff env c Subproof] in - add_private env.revstruct eff empty_private_constants +let push_private_constants env eff = + let eff = side_effects_of_private_constants eff in + let add_if_undefined env eff = + try ignore(Environ.lookup_constant eff.seff_constant env); env + with Not_found -> Environ.add_constant eff.seff_constant (lift_constant eff.seff_body) env + in + List.fold_left add_if_undefined env eff -let private_con_of_scheme ~kind env cl = - let open Entries in - let eff = List.map (fun (i, c) -> make_eff env c (Schema (i, kind))) cl in - add_private env.revstruct eff empty_private_constants +let empty_private_constants = SideEffects.empty +let concat_private = SideEffects.concat let universes_of_private eff = - let open Entries in let fold acc eff = - let acc = match eff.seff_env with - | `Nothing -> acc - | `Opaque (_, ctx) -> ctx :: acc - in match eff.seff_body.const_universes with | Monomorphic ctx -> ctx :: acc | Polymorphic _ -> acc @@ -325,23 +308,24 @@ let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env type constraints_addition = - | Now of bool * Univ.ContextSet.t + | Now of Univ.ContextSet.t | Later of Univ.ContextSet.t Future.computation +let push_context_set poly cst senv = + { senv with + env = Environ.push_context_set ~strict:(not poly) cst senv.env; + univ = Univ.ContextSet.union cst senv.univ } + let add_constraints cst senv = match cst with | Later fc -> {senv with future_cst = fc :: senv.future_cst} - | Now (poly,cst) -> - { senv with - env = Environ.push_context_set ~strict:(not poly) cst senv.env; - univ = Univ.ContextSet.union cst senv.univ } + | Now cst -> + push_context_set false cst senv let add_constraints_list cst senv = List.fold_left (fun acc c -> add_constraints c acc) senv cst -let push_context_set poly ctx = add_constraints (Now (poly,ctx)) - let is_curmod_library senv = match senv.modvariant with LIBRARY -> true | _ -> false @@ -350,7 +334,7 @@ let join_safe_environment ?(except=Future.UUIDSet.empty) e = List.fold_left (fun e fc -> if Future.UUIDSet.mem (Future.uuid fc) except then e - else add_constraints (Now (false, Future.join fc)) e) + else add_constraints (Now (Future.join fc)) e) {e with future_cst = []} e.future_cst let is_joined_environment e = List.is_empty e.future_cst @@ -469,34 +453,26 @@ let labels_of_mib mib = Array.iter visit_mip mib.mind_packets; get () -let globalize_constant_universes env cb = +let globalize_constant_universes cb = match cb.const_universes with | Monomorphic cstrs -> - Now (false, cstrs) :: - (match cb.const_body with - | (Undef _ | Def _ | Primitive _) -> [] - | OpaqueDef lc -> - match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with - | None -> [] - | Some fc -> - match Future.peek_val fc with - | None -> [Later fc] - | Some c -> [Now (false, c)]) + (* Constraints hidden in the opaque body are added by [add_constant_aux] *) + [cstrs] | Polymorphic _ -> - [Now (true, Univ.ContextSet.empty)] + [] let globalize_mind_universes mb = match mb.mind_universes with | Monomorphic ctx -> - [Now (false, ctx)] - | Polymorphic _ -> [Now (true, Univ.ContextSet.empty)] + [ctx] + | Polymorphic _ -> [] -let constraints_of_sfb env sfb = +let constraints_of_sfb sfb = match sfb with - | SFBconst cb -> globalize_constant_universes env cb + | SFBconst cb -> globalize_constant_universes cb | SFBmind mib -> globalize_mind_universes mib - | SFBmodtype mtb -> [Now (false, mtb.mod_constraints)] - | SFBmodule mb -> [Now (false, mb.mod_constraints)] + | SFBmodtype mtb -> [mtb.mod_constraints] + | SFBmodule mb -> [mb.mod_constraints] let add_retroknowledge pttc senv = { senv with @@ -531,8 +507,9 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv = separately. *) senv else - let cst = constraints_of_sfb senv.env sfb in - add_constraints_list cst senv + (* Delayed constraints from opaque body are added by [add_constant_aux] *) + let cst = constraints_of_sfb sfb in + List.fold_left (fun senv cst -> push_context_set false cst senv) senv cst in let env' = match sfb, gn with | SFBconst cb, C con -> Environ.add_constant con cb senv.env @@ -558,13 +535,22 @@ type 'a effect_entry = type global_declaration = | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration - | GlobalRecipe of Cooking.recipe -type exported_private_constant = - Constant.t * Entries.side_effect_role +type exported_private_constant = Constant.t let add_constant_aux ~in_section senv (kn, cb) = let l = Constant.label kn in + let delayed_cst = match cb.const_body with + | OpaqueDef o when not (Declareops.constant_is_polymorphic cb) -> + let fc = Opaqueproof.get_direct_constraints o in + begin match Future.peek_val fc with + | None -> [Later fc] + | Some c -> [Now c] + end + | Undef _ | Def _ | Primitive _ | OpaqueDef _ -> [] + in + (* This is the only place where we hashcons the contents of a constant body *) + let cb = if in_section then cb else Declareops.hcons_const_body cb in let cb, otab = match cb.const_body with | OpaqueDef lc when not in_section -> (* In coqc, opaque constants outside sections will be stored @@ -577,6 +563,7 @@ let add_constant_aux ~in_section senv (kn, cb) = in let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in let senv' = add_field (l,SFBconst cb) (C kn) senv in + let senv' = add_constraints_list delayed_cst senv' in let senv'' = match cb.const_body with | Undef (Some lev) -> update_resolver @@ -588,32 +575,27 @@ let add_constant_aux ~in_section senv (kn, cb) = let mk_pure_proof c = (c, Univ.ContextSet.empty), SideEffects.empty let inline_side_effects env body side_eff = - let open Entries in let open Constr in (** First step: remove the constants that are still in the environment *) - let filter { eff = se; from_env = mb } = - let map e = (e.seff_constant, e.seff_body, e.seff_env) in - let cbl = List.map map se 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 - (cbl, mb) + let filter e = + let cb = (e.seff_constant, e.seff_body) in + try ignore (Environ.lookup_constant e.seff_constant env); None + with Not_found -> Some (cb, e.from_env) in (* CAVEAT: we assure that most recent effects come first *) - let side_eff = List.map filter (SideEffects.repr 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.map_filter filter (SideEffects.repr side_eff) in + let sigs = List.rev_map (fun (_, mb) -> mb) side_eff in + let side_eff = List.fold_left (fun accu (cb, _) -> cb :: 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, Univ.ContextSet.empty, sigs) else (** Second step: compute the lifts and substitutions to apply *) let cname c r = Context.make_annot (Name (Label.to_id (Constant.label c))) r 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) + let fold (subst, var, ctx, args) (c, cb) = + let (b, opaque) = match cb.const_body with + | Def b -> (Mod_subst.force_constr b, false) + | OpaqueDef b -> (b, true) | _ -> assert false in match cb.const_universes with @@ -662,37 +644,27 @@ let inline_side_effects env body side_eff = let body = List.fold_right fold_arg args body in (body, ctx, sigs) -let inline_private_constants_in_definition_entry env ce = - let open Entries in - { ce with - const_entry_body = Future.chain - ce.const_entry_body (fun ((body, ctx), side_eff) -> - let body, ctx',_ = inline_side_effects env body side_eff in - let ctx' = Univ.ContextSet.union ctx ctx' in - (body, ctx'), ()); - } - -let inline_private_constants_in_constr env body side_eff = - pi1 (inline_side_effects env body side_eff) +let inline_private_constants env ((body, ctx), side_eff) = + let body, ctx',_ = inline_side_effects env body side_eff in + let ctx' = Univ.ContextSet.union ctx ctx' in + (body, ctx') -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 +let is_suffix l suf = match l with +| [] -> false +| _ :: l -> 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. Returns the number of effects that can be trusted. *) let check_signatures curmb sl = - let is_direct_ancestor accu (mb, how_many) = + let is_direct_ancestor accu mb = match accu with | None -> None | Some (n, curmb) -> try let mb = CEphemeron.get mb in - if is_nth_suffix how_many mb curmb - then Some (n + how_many, mb) + if is_suffix mb curmb + then Some (n + 1, mb) else None with CEphemeron.InvalidKey -> None in let sl = List.fold_left is_direct_ancestor (Some (0, curmb)) sl in @@ -701,7 +673,8 @@ let check_signatures curmb sl = | Some (n, _) -> n -let constant_entry_of_side_effect cb u = +let constant_entry_of_side_effect eff = + let cb = eff.seff_body in let open Entries in let univs = match cb.const_universes with @@ -710,101 +683,101 @@ let constant_entry_of_side_effect cb u = | Polymorphic auctx -> Polymorphic_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx) in - let pt = - match cb.const_body, u with - | OpaqueDef _, `Opaque (b, c) -> b, c - | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty + let p = + match cb.const_body with + | OpaqueDef b -> b + | Def b -> Mod_subst.force_constr b | _ -> assert false in + if Declareops.is_opaque cb then + OpaqueEntry { + opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); + opaque_entry_secctx = None; + opaque_entry_feedback = None; + opaque_entry_type = cb.const_type; + opaque_entry_universes = univs; + } + else DefinitionEntry { - const_entry_body = Future.from_val (pt, ()); + const_entry_body = (p, Univ.ContextSet.empty); const_entry_secctx = None; const_entry_feedback = None; const_entry_type = Some cb.const_type; const_entry_universes = univs; - const_entry_opaque = Declareops.is_opaque cb; const_entry_inline_code = cb.const_inline_code } -let turn_direct orig = - let open Entries in - let cb = orig.seff_body in - if Declareops.is_opaque cb then - let p = match orig.seff_env with - | `Opaque (b, c) -> (b, c) - | _ -> assert false - in - let const_body = OpaqueDef (Opaqueproof.create (Future.from_val p)) in - let cb = { cb with const_body } in - { orig with seff_body = cb } - else orig - let export_eff eff = - let open Entries in - (eff.seff_constant, eff.seff_body, eff.seff_role) + (eff.seff_constant, eff.seff_body) -let export_side_effects mb env c = - let open Entries in - let body = c.const_entry_body in - let _, eff = Future.force body in - let ce = { c with - Entries.const_entry_body = Future.chain body - (fun (b_ctx, _) -> b_ctx, ()) } in +let export_side_effects mb env (b_ctx, eff) = let not_exists e = try ignore(Environ.lookup_constant e.seff_constant env); false with Not_found -> true in - let aux (acc,sl) { eff = se; from_env = mb } = - let cbl = List.filter not_exists se in - if List.is_empty cbl then acc, sl - else cbl :: acc, (mb,List.length cbl) :: sl in + let aux (acc,sl) e = + if not (not_exists e) then acc, sl + else e :: acc, e.from_env :: sl in let seff, signatures = List.fold_left aux ([],[]) (SideEffects.repr eff) in let trusted = check_signatures mb signatures in let push_seff env eff = let { seff_constant = kn; seff_body = cb ; _ } = eff in - let env = Environ.add_constant kn cb env in + let env = Environ.add_constant kn (lift_constant cb) env in match cb.const_universes with | Polymorphic _ -> env | Monomorphic ctx -> - let ctx = match eff.seff_env with - | `Nothing -> ctx - | `Opaque(_, ctx') -> Univ.ContextSet.union ctx' ctx - in Environ.push_context_set ~strict:true ctx env in let rec translate_seff sl seff acc env = match seff with - | [] -> List.rev acc, ce - | cbs :: rest -> + | [] -> List.rev acc, b_ctx + | eff :: rest -> if Int.equal sl 0 then - let env, cbs = - List.fold_left (fun (env,cbs) eff -> - let { seff_constant = kn; seff_body = ocb; seff_env = u ; _ } = eff in - let ce = constant_entry_of_side_effect ocb u in + let env, cb = + let kn = eff.seff_constant in + let ce = constant_entry_of_side_effect eff in let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in - let eff = { eff with - seff_body = cb; - seff_env = `Nothing; - } in - (push_seff env eff, export_eff eff :: cbs)) - (env,[]) cbs in - translate_seff 0 rest (cbs @ acc) env + let map cu = + let (c, u) = Future.force cu in + let () = match u with + | Opaqueproof.PrivateMonomorphic ctx + | Opaqueproof.PrivatePolymorphic (_, ctx) -> + assert (Univ.ContextSet.is_empty ctx) + in + c + in + let cb = map_constant map cb in + let eff = { eff with seff_body = cb } in + (push_seff env eff, export_eff eff) + in + translate_seff 0 rest (cb :: acc) env else - let cbs_len = List.length cbs in - let cbs = List.map turn_direct cbs in - let env = List.fold_left push_seff env cbs in - let ecbs = List.map export_eff cbs in - translate_seff (sl - cbs_len) rest (ecbs @ acc) env + let env = push_seff env eff in + let ecb = export_eff eff in + translate_seff (sl - 1) rest (ecb :: acc) env in translate_seff trusted seff [] env let export_private_constants ~in_section ce senv = let exported, ce = export_side_effects senv.revstruct senv.env ce in - let bodies = List.map (fun (kn, cb, _) -> (kn, cb)) exported in - let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in + let map univs p = + let local = match univs with + | Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty + | Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty) + in + Opaqueproof.create (Future.from_val (p, local)) + in + let map (kn, cb) = (kn, map_constant (fun c -> map cb.const_universes c) cb) in + let bodies = List.map map exported in + let exported = List.map (fun (kn, _) -> kn) exported in let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in (ce, exported), senv -let add_constant ~in_section l decl senv = +let add_recipe ~in_section l r senv = + let kn = Constant.make2 senv.modpath l in + let cb = Term_typing.translate_recipe senv.env kn r in + let senv = add_constant_aux ~in_section senv (kn, cb) in + kn, senv + +let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl senv : (Constant.t * a) * safe_environment = let kn = Constant.make2 senv.modpath l in - let senv = let cb = match decl with | ConstantEntry (EffectEntry, ce) -> @@ -816,9 +789,9 @@ let add_constant ~in_section l decl senv = Term_typing.translate_constant (Term_typing.SideEffects handle) senv.env kn ce | ConstantEntry (PureEntry, ce) -> Term_typing.translate_constant Term_typing.Pure senv.env kn ce - | GlobalRecipe r -> - let cb = Term_typing.translate_recipe ~hcons:(not in_section) senv.env kn r in - if in_section then cb else Declareops.hcons_const_body cb in + in + let senv = + let cb = map_constant (fun c -> Opaqueproof.create c) cb in add_constant_aux ~in_section senv (kn, cb) in let senv = match decl with @@ -827,7 +800,34 @@ let add_constant ~in_section l decl senv = add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv | _ -> senv in - kn, senv + let eff : a = match side_effect with + | PureEntry -> () + | EffectEntry -> + let body, univs = match cb.const_body with + | (Primitive _ | Undef _) -> assert false + | Def c -> (Def c, cb.const_universes) + | OpaqueDef o -> + let (b, delayed) = Future.force o in + match cb.const_universes, delayed with + | Monomorphic ctx', Opaqueproof.PrivateMonomorphic ctx -> + OpaqueDef b, Monomorphic (Univ.ContextSet.union ctx ctx') + | Polymorphic auctx, Opaqueproof.PrivatePolymorphic (_, ctx) -> + (* Upper layers enforce that there are no internal constraints *) + let () = assert (Univ.ContextSet.is_empty ctx) in + OpaqueDef b, Polymorphic auctx + | (Monomorphic _ | Polymorphic _), (Opaqueproof.PrivateMonomorphic _ | Opaqueproof.PrivatePolymorphic _) -> + assert false + in + let cb = { cb with const_body = body; const_universes = univs } in + let from_env = CEphemeron.create senv.revstruct in + let eff = { + from_env = from_env; + seff_constant = kn; + seff_body = cb; + } in + SideEffects.add eff empty_private_constants + in + (kn, eff), senv (** Insertion of inductive types *) @@ -860,13 +860,13 @@ let add_modtype l params_mte inl senv = (** full_add_module adds module with universes and constraints *) let full_add_module mb senv = - let senv = add_constraints (Now (false, mb.mod_constraints)) senv in + let senv = add_constraints (Now mb.mod_constraints) senv in let dp = ModPath.dp mb.mod_mp in let linkinfo = Nativecode.link_info_of_dirpath dp in { senv with env = Modops.add_linked_module mb linkinfo senv.env } let full_add_module_type mp mt senv = - let senv = add_constraints (Now (false, mt.mod_constraints)) senv in + let senv = add_constraints (Now mt.mod_constraints) senv in { senv with env = Modops.add_module_type mp mt senv.env } (** Insertion of modules *) @@ -1046,7 +1046,7 @@ let add_include me is_module inl senv = let sign,(),resolver,cst = translate_mse_incl is_module senv.env mp_sup inl me in - let senv = add_constraints (Now (false, cst)) senv in + let senv = add_constraints (Now cst) senv in (* Include Self support *) let rec compute_sign sign mb resolver senv = match sign with @@ -1054,7 +1054,7 @@ let add_include me is_module inl senv = let cst_sub = Subtyping.check_subtypes senv.env mb mtb in let senv = add_constraints - (Now (false, Univ.ContextSet.add_constraints cst_sub Univ.ContextSet.empty)) + (Now (Univ.ContextSet.add_constraints cst_sub Univ.ContextSet.empty)) senv in let mpsup_delta = Modops.inline_delta_resolver senv.env inl mp_sup mbid mtb mb.mod_delta @@ -1284,7 +1284,7 @@ let register_inductive ind prim senv = let add_constraints c = add_constraints - (Now (false, Univ.ContextSet.add_constraints c Univ.ContextSet.empty)) + (Now (Univ.ContextSet.add_constraints c Univ.ContextSet.empty)) (* NB: The next old comment probably refers to [propagate_loads] above. diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 46c97c1fb8..885becc40a 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -43,24 +43,17 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment type private_constants -val side_effects_of_private_constants : - private_constants -> Entries.side_eff list -(** Return the list of individual side-effects in the order of their - creation. *) - val empty_private_constants : private_constants val concat_private : private_constants -> private_constants -> private_constants (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in [e1] must be more recent than those of [e2]. *) -val private_con_of_con : safe_environment -> Constant.t -> private_constants -val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constants - val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output -val inline_private_constants_in_constr : - Environ.env -> Constr.constr -> private_constants -> Constr.constr -val inline_private_constants_in_definition_entry : - Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry +val inline_private_constants : + Environ.env -> private_constants Entries.proof_output -> Constr.constr Univ.in_universe_context_set + +val push_private_constants : Environ.env -> private_constants -> Environ.env +(** Push the constants in the environment if not already there. *) val universes_of_private : private_constants -> Univ.ContextSet.t list @@ -93,20 +86,20 @@ type 'a effect_entry = type global_declaration = | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration - | GlobalRecipe of Cooking.recipe -type exported_private_constant = - Constant.t * Entries.side_effect_role +type exported_private_constant = Constant.t val export_private_constants : in_section:bool -> - private_constants Entries.definition_entry -> - (unit Entries.definition_entry * exported_private_constant list) safe_transformer + private_constants Entries.proof_output -> + (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer -(** returns the main constant plus a list of auxiliary constants (empty - unless one requires the side effects to be exported) *) +(** returns the main constant plus a certificate of its validity *) val add_constant : - in_section:bool -> Label.t -> global_declaration -> - Constant.t safe_transformer + side_effect:'a effect_entry -> in_section:bool -> Label.t -> global_declaration -> + (Constant.t * 'a) safe_transformer + +val add_recipe : + in_section:bool -> Label.t -> Cooking.recipe -> Constant.t safe_transformer (** Adding an inductive type *) diff --git a/kernel/sorts.ml b/kernel/sorts.ml index 09c98ca1bc..b8bebb659b 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -91,6 +91,8 @@ let family_compare a b = match a,b with let family_equal = (==) +let family_leq a b = family_compare a b <= 0 + open Hashset.Combine let hash = function @@ -101,11 +103,6 @@ let hash = function let h = Univ.Universe.hash u in combinesmall 2 h -module List = struct - let mem = List.memq - let intersect l l' = CList.intersect family_equal l l' -end - module Hsorts = Hashcons.Make( struct diff --git a/kernel/sorts.mli b/kernel/sorts.mli index c49728b146..fa129d10fb 100644 --- a/kernel/sorts.mli +++ b/kernel/sorts.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -37,11 +37,7 @@ val hcons : t -> t val family_compare : family -> family -> int val family_equal : family -> family -> bool - -module List : sig - val mem : family -> family list -> bool - val intersect : family list -> family list -> family list -end +val family_leq : family -> family -> bool val univ_of_sort : t -> Univ.Universe.t val sort_of_univ : Univ.Universe.t -> t diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 1857ea3329..d47dc0c6e1 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -31,7 +31,7 @@ open Mod_subst an inductive type. It can also be useful to allow reorderings in inductive types *) type namedobject = - | Constant of constant_body + | Constant of Opaqueproof.opaque constant_body | IndType of inductive * mutual_inductive_body | IndConstr of constructor * mutual_inductive_body diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli index 4e755e42ff..9aa48bf6b4 100644 --- a/kernel/subtyping.mli +++ b/kernel/subtyping.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/term.ml b/kernel/term.ml index f09c45715f..38c0d043cf 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/term.mli b/kernel/term.mli index 4265324693..d2de4177ce 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index faa4411e92..eca22869d2 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -74,12 +74,11 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let j = Typeops.infer env t in let usubst, univs = Declareops.abstract_universes uctx in let r = Typeops.assumption_of_judgment env j in - let t = Constr.hcons (Vars.subst_univs_level_constr usubst j.uj_val) in + let t = Vars.subst_univs_level_constr usubst j.uj_val in { Cooking.cook_body = Undef nl; cook_type = t; cook_universes = univs; - cook_private_univs = None; cook_relevance = r; cook_inline = false; cook_context = ctx; @@ -95,7 +94,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = | Some typ -> let typ = Typeops.infer_type env typ in Typeops.check_primitive_type env op_t typ.utj_val; - Constr.hcons typ.utj_val + typ.utj_val | None -> match op_t with | CPrimitives.OT_op op -> Typeops.type_of_prim env op @@ -108,31 +107,21 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = cd; cook_type = ty; cook_universes = Monomorphic uctxt; - cook_private_univs = None; cook_inline = false; cook_context = None; cook_relevance = Sorts.Relevant; } (** Definition [c] is opaque (Qed), non polymorphic and with a specified type, - so we delay the typing and hash consing of its body. - Remark: when the universe quantification is given explicitly, we could - delay even in the polymorphic case. *) + so we delay the typing and hash consing of its body. *) -(** Definition is opaque (Qed) and non polymorphic with known type, so we delay -the typing and hash consing of its body. - -TODO: if the universe quantification is given explicitly, we could delay even in -the polymorphic case - *) - | DefinitionEntry ({ const_entry_type = Some typ; - const_entry_opaque = true; - const_entry_universes = Monomorphic_entry univs; _ } as c) -> + | OpaqueEntry ({ opaque_entry_type = typ; + opaque_entry_universes = Monomorphic_entry univs; _ } as c) -> let env = push_context_set ~strict:true univs env in - let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in + let { opaque_entry_body = body; opaque_entry_feedback = feedback_id; _ } = c in let tyj = Typeops.infer_type env typ in let proofterm = - Future.chain body (fun ((body,uctx),side_eff) -> + Future.chain body begin fun ((body,uctx),side_eff) -> (* don't redeclare universes which are declared for the type *) let uctx = Univ.ContextSet.diff uctx univs in let j, uctx = match trust with @@ -151,50 +140,81 @@ the polymorphic case let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in j, uctx in - let c = Constr.hcons j.uj_val in + let c = j.uj_val in feedback_completion_typecheck feedback_id; - c, uctx) in - let def = OpaqueDef (Opaqueproof.create proofterm) in + c, Opaqueproof.PrivateMonomorphic uctx + end in + let def = OpaqueDef proofterm in { Cooking.cook_body = def; cook_type = tyj.utj_val; cook_universes = Monomorphic univs; - cook_private_univs = None; cook_relevance = Sorts.relevance_of_sort tyj.utj_type; - cook_inline = c.const_entry_inline_code; - cook_context = c.const_entry_secctx; + cook_inline = false; + cook_context = c.opaque_entry_secctx; + } + + (** Similar case for polymorphic entries. *) + + | OpaqueEntry ({ opaque_entry_type = typ; + opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) -> + let { opaque_entry_body = body; opaque_entry_feedback = feedback_id; _ } = c in + let env = push_context ~strict:false uctx env in + let tj = Typeops.infer_type env typ in + let sbst, auctx = Univ.abstract_universes nas uctx in + let usubst = Univ.make_instance_subst sbst in + let proofterm = Future.chain body begin fun ((body, ctx), side_eff) -> + let body, ctx = match trust with + | Pure -> body, ctx + | SideEffects handle -> + let body, ctx', _ = handle env body side_eff in + body, Univ.ContextSet.union ctx ctx' + in + (** [ctx] must contain local universes, such that it has no impact + on the rest of the graph (up to transitivity). *) + let env = push_subgraph ctx env in + let private_univs = on_snd (Univ.subst_univs_level_constraints usubst) ctx in + let j = Typeops.infer env body in + let _ = Typeops.judge_of_cast env j DEFAULTcast tj in + let def = Vars.subst_univs_level_constr usubst j.uj_val in + let () = feedback_completion_typecheck feedback_id in + def, Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, private_univs) + end in + let def = OpaqueDef proofterm in + let typ = Vars.subst_univs_level_constr usubst tj.utj_val in + { + Cooking.cook_body = def; + cook_type = typ; + cook_universes = Polymorphic auctx; + cook_relevance = Sorts.relevance_of_sort tj.utj_type; + cook_inline = false; + cook_context = c.opaque_entry_secctx; } (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> - let { const_entry_type = typ; const_entry_opaque = opaque ; _ } = c in - let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in - let (body, ctx), side_eff = Future.join body in - let body, ctx = match trust with - | Pure -> body, ctx - | SideEffects handle -> - let body, ctx', _ = handle env body side_eff in - body, Univ.ContextSet.union ctx ctx' + let { const_entry_type = typ; _ } = c in + let { const_entry_body = (body, ctx); const_entry_feedback = feedback_id; _ } = c in + let () = match trust with + | Pure -> () + | SideEffects _ -> assert false in - let env, usubst, univs, private_univs = match c.const_entry_universes with + let env, usubst, univs = match c.const_entry_universes with | Monomorphic_entry univs -> let ctx = Univ.ContextSet.union univs ctx in let env = push_context_set ~strict:true ctx env in - env, Univ.empty_level_subst, Monomorphic ctx, None + env, Univ.empty_level_subst, Monomorphic ctx | Polymorphic_entry (nas, uctx) -> (** [ctx] must contain local universes, such that it has no impact on the rest of the graph (up to transitivity). *) let env = push_context ~strict:false uctx env in let sbst, auctx = Univ.abstract_universes nas uctx in let sbst = Univ.make_instance_subst sbst in - let env, local = - if opaque then - push_subgraph ctx env, Some (on_snd (Univ.subst_univs_level_constraints sbst) ctx) - else - if Univ.ContextSet.is_empty ctx then env, None - else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.") + let () = + if not (Univ.ContextSet.is_empty ctx) then + CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.") in - env, sbst, Polymorphic auctx, local + env, sbst, Polymorphic auctx in let j = Typeops.infer env body in let typ = match typ with @@ -205,17 +225,13 @@ the polymorphic case let _ = Typeops.judge_of_cast env j DEFAULTcast tj in Vars.subst_univs_level_constr usubst tj.utj_val in - let def = Constr.hcons (Vars.subst_univs_level_constr usubst j.uj_val) in - let def = - if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty))) - else Def (Mod_subst.from_val def) - in + let def = Vars.subst_univs_level_constr usubst j.uj_val in + let def = Def (Mod_subst.from_val def) in feedback_completion_typecheck feedback_id; { Cooking.cook_body = def; cook_type = typ; cook_universes = univs; - cook_private_univs = private_univs; cook_relevance = Retypeops.relevance_of_term env j.uj_val; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; @@ -232,7 +248,7 @@ let record_aux env s_ty s_bo = (keep_hyps env s_bo)) in Aux_file.record_in_aux "context_used" v -let build_constant_declaration _kn env result = +let build_constant_declaration env result = let open Cooking in let typ = result.cook_type in let check declared inferred = @@ -271,11 +287,8 @@ let build_constant_declaration _kn env result = | Undef _ | Primitive _ -> Id.Set.empty | Def cs -> global_vars_set env (Mod_subst.force_constr cs) | OpaqueDef lc -> - let vars = - global_vars_set env - (Opaqueproof.force_proof (opaque_tables env) lc) in - (* we force so that cst are added to the env immediately after *) - ignore(Opaqueproof.force_constraints (opaque_tables env) lc); + let (lc, _) = Future.force lc in + let vars = global_vars_set env lc in if !Flags.record_aux_file then record_aux env ids_typ vars; vars in @@ -296,11 +309,15 @@ let build_constant_declaration _kn env result = check declared inferred; x | OpaqueDef lc -> (* In this case we can postpone the check *) - OpaqueDef (Opaqueproof.iter_direct_opaque (fun c -> - let ids_typ = global_vars_set env typ in - let ids_def = global_vars_set env c in - let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in - check declared inferred) lc) in + let iter k cu = Future.chain cu (fun (c, _ as p) -> k c; p) in + let kont c = + let ids_typ = global_vars_set env typ in + let ids_def = global_vars_set env c in + let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in + check declared inferred + in + OpaqueDef (iter kont lc) + in let univs = result.cook_universes in let tps = let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in @@ -311,15 +328,14 @@ let build_constant_declaration _kn env result = const_type = typ; const_body_code = tps; const_universes = univs; - const_private_poly_univs = result.cook_private_univs; const_relevance = result.cook_relevance; const_inline_code = result.cook_inline; const_typing_flags = Environ.typing_flags env } (*s Global and local constant declaration. *) -let translate_constant mb env kn ce = - build_constant_declaration kn env +let translate_constant mb env _kn ce = + build_constant_declaration env (infer_declaration ~trust:mb env ce) let translate_local_assum env t = @@ -327,19 +343,30 @@ let translate_local_assum env t = let t = Typeops.assumption_of_judgment env j in j.uj_val, t -let translate_recipe ~hcons env kn r = - build_constant_declaration kn env (Cooking.cook_constant ~hcons r) +let translate_recipe env _kn r = + let open Cooking in + let result = Cooking.cook_constant r in + let univs = result.cook_universes in + let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in + let tps = Option.map Cemitcodes.from_val res in + { const_hyps = Option.get result.cook_context; + const_body = result.cook_body; + const_type = result.cook_type; + const_body_code = tps; + const_universes = univs; + const_relevance = result.cook_relevance; + const_inline_code = result.cook_inline; + const_typing_flags = Environ.typing_flags env } let translate_local_def env _id centry = let open Cooking in - let body = Future.from_val ((centry.secdef_body, Univ.ContextSet.empty), ()) in + let body = (centry.secdef_body, Univ.ContextSet.empty) in let centry = { const_entry_body = body; const_entry_secctx = centry.secdef_secctx; const_entry_feedback = centry.secdef_feedback; const_entry_type = centry.secdef_type; const_entry_universes = Monomorphic_entry Univ.ContextSet.empty; - const_entry_opaque = false; const_entry_inline_code = false; } in let decl = infer_declaration ~trust:Pure env (DefinitionEntry centry) in @@ -351,8 +378,7 @@ let translate_local_def env _id centry = | Def _ -> () | OpaqueDef lc -> let ids_typ = global_vars_set env typ in - let ids_def = global_vars_set env - (Opaqueproof.force_proof (opaque_tables env) lc) in + let ids_def = global_vars_set env (fst (Future.force lc)) in record_aux env ids_typ ids_def end; let () = match decl.cook_universes with @@ -362,11 +388,13 @@ let translate_local_def env _id centry = let c = match decl.cook_body with | Def c -> Mod_subst.force_constr c | OpaqueDef o -> - let p = Opaqueproof.force_proof (Environ.opaque_tables env) o in - let cst = Opaqueproof.force_constraints (Environ.opaque_tables env) o in + let (p, cst) = Future.force o in (** Let definitions are ensured to have no extra constraints coming from the body by virtue of the typing of [Entries.section_def_entry]. *) - let () = assert (Univ.ContextSet.is_empty cst) in + let () = match cst with + | Opaqueproof.PrivateMonomorphic ctx -> assert (Univ.ContextSet.is_empty ctx) + | Opaqueproof.PrivatePolymorphic (_, ctx) -> assert (Univ.ContextSet.is_empty ctx) + in p | Undef _ | Primitive _ -> assert false in diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 1fa5eca2e3..225abd60f8 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -33,14 +33,14 @@ val translate_local_assum : env -> types -> types * Sorts.relevance val translate_constant : 'a trust -> env -> Constant.t -> 'a constant_entry -> - constant_body + Opaqueproof.proofterm constant_body -val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> constant_body +val translate_recipe : env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body (** Internal functions, mentioned here for debug purpose only *) val infer_declaration : trust:'a trust -> env -> - 'a constant_entry -> Cooking.result + 'a constant_entry -> Opaqueproof.proofterm Cooking.result val build_constant_declaration : - Constant.t -> env -> Cooking.result -> constant_body + env -> Opaqueproof.proofterm Cooking.result -> Opaqueproof.proofterm constant_body diff --git a/kernel/transparentState.ml b/kernel/transparentState.ml index 9661dace6a..372e021c39 100644 --- a/kernel/transparentState.ml +++ b/kernel/transparentState.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/transparentState.mli b/kernel/transparentState.mli index f2999c6869..db6d147280 100644 --- a/kernel/transparentState.mli +++ b/kernel/transparentState.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index c45fe1cf00..f221ac7a4f 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -49,7 +49,7 @@ type ('constr, 'types) ptype_error = | BadAssumption of ('constr, 'types) punsafe_judgment | ReferenceVariables of Id.t * 'constr | ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment - * (Sorts.family list * Sorts.family * Sorts.family * arity_error) option + * (Sorts.family * Sorts.family * Sorts.family * arity_error) option | CaseNotInductive of ('constr, 'types) punsafe_judgment | WrongCaseInfo of pinductive * case_info | NumberBranches of ('constr, 'types) punsafe_judgment * int diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 88165a4f07..ae6fd31762 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -50,7 +50,7 @@ type ('constr, 'types) ptype_error = | BadAssumption of ('constr, 'types) punsafe_judgment | ReferenceVariables of Id.t * 'constr | ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment - * (Sorts.family list * Sorts.family * Sorts.family * arity_error) option + * (Sorts.family * Sorts.family * Sorts.family * arity_error) option | CaseNotInductive of ('constr, 'types) punsafe_judgment | WrongCaseInfo of pinductive * case_info | NumberBranches of ('constr, 'types) punsafe_judgment * int @@ -104,7 +104,7 @@ val error_reference_variables : env -> Id.t -> constr -> 'a val error_elim_arity : env -> pinductive -> constr -> unsafe_judgment -> - (Sorts.family list * Sorts.family * Sorts.family * arity_error) option -> 'a + (Sorts.family * Sorts.family * Sorts.family * arity_error) option -> 'a val error_case_not_inductive : env -> unsafe_judgment -> 'a diff --git a/kernel/typeops.ml b/kernel/typeops.ml index af710e7822..b87384d228 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index c8f3e506e6..c71a0e0ca4 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 0d5b55ca1b..6fde6e9c5f 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index 17d6c6e6d3..e1b5868d55 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/uint63.mli b/kernel/uint63.mli index f25f24512d..93632da110 100644 --- a/kernel/uint63.mli +++ b/kernel/uint63.mli @@ -13,7 +13,7 @@ val of_uint : int -> t val hash : t -> int - (* convertion to a string *) + (* conversion to a string *) val to_string : t -> string val of_string : string -> t diff --git a/kernel/uint63_amd64.ml b/kernel/uint63_amd64_63.ml index 2d4d685775..20b2f58496 100644 --- a/kernel/uint63_amd64.ml +++ b/kernel/uint63_amd64_63.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/uint63_x86.ml b/kernel/uint63_i386_31.ml index fa45c90241..c3279779e1 100644 --- a/kernel/uint63_x86.ml +++ b/kernel/uint63_i386_31.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/univ.ml b/kernel/univ.ml index b1bbc25fe6..14d6bfabf1 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -726,7 +726,7 @@ let univ_level_rem u v min = | Some u' -> if Level.equal u u' then min else v | None -> List.filter (fun (l, n) -> not (Int.equal n 0 && Level.equal u l)) v -(* Is u mentionned in v (or equals to v) ? *) +(* Is u mentioned in v (or equals to v) ? *) (**********************************************************************) diff --git a/kernel/univ.mli b/kernel/univ.mli index db178c4bb0..ccb5c80cbf 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -163,7 +163,7 @@ val super : Universe.t -> Universe.t val universe_level : Universe.t -> Level.t option -(** [univ_level_mem l u] Is l is mentionned in u ? *) +(** [univ_level_mem l u] Is l is mentioned in u ? *) val univ_level_mem : Level.t -> Universe.t -> bool diff --git a/kernel/vars.ml b/kernel/vars.ml index bd56d60053..dd187387d4 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/vars.mli b/kernel/vars.mli index f2c32b3625..6a1815619f 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 1a31848989..0a85498c40 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/vm.ml b/kernel/vm.ml index 83312a8530..319a26d824 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/vm.mli b/kernel/vm.mli index 50ebc90626..5637f7e1cd 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 777a207013..c8f5020d71 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -11,10 +11,10 @@ open Names open Univ open Constr -(*******************************************) -(* Initalization of the abstract machine ***) -(* Necessary for [relaccu_tbl] *) -(*******************************************) +(********************************************) +(* Initialization of the abstract machine ***) +(* Necessary for [relaccu_tbl] *) +(********************************************) external init_vm : unit -> unit = "init_coq_vm" diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index 6d984d5f49..d289e7db9a 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/kernel/write_uint63.ml b/kernel/write_uint63.ml index beb59ce205..57a170c8f5 100644 --- a/kernel/write_uint63.ml +++ b/kernel/write_uint63.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -31,8 +31,8 @@ let ml_file_copy input output = let write_uint63 () = ml_file_copy - (if max_int = 1073741823 (* 32-bits *) then "uint63_x86.ml" - else (* 64 bits *) "uint63_amd64.ml") + (if max_int = 1073741823 (* 32-bits *) then "uint63_i386_31.ml" + else (* 64 bits *) "uint63_amd64_63.ml") "uint63.ml" let () = write_uint63 () |