diff options
Diffstat (limited to 'kernel')
33 files changed, 303 insertions, 399 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 2293ae9dfd..4b45608ae5 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -29,13 +29,6 @@ #include "coq_uint63_emul.h" #endif -/* spiwack: I append here a few macros for value/number manipulation */ -#define uint32_of_value(val) (((uint32_t)(val)) >> 1) -#define value_of_uint32(i) ((value)((((uint32_t)(i)) << 1) | 1)) -#define UI64_of_uint32(lo) ((uint64_t)((uint32_t)(lo))) -#define UI64_of_value(val) (UI64_of_uint32(uint32_of_value(val))) -/* /spiwack */ - /* Registers for the abstract machine: @@ -104,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") @@ -133,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") @@ -148,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 @@ -159,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{ \ @@ -1298,12 +1304,6 @@ value coq_interprete /*returns the multiplication on a pair */ print_instr("MULCINT63"); CheckInt2(); - /*accu = 2v+1, *sp=2w+1 ==> p = 2v*w */ - /* TODO: implement - p = I64_mul (UI64_of_value (accu), UI64_of_uint32 ((*sp++)^1)); - AllocPair(); */ - /* Field(accu, 0) = (value)(I64_lsr(p,31)|1) ; */ /*higher part*/ - /* Field(accu, 1) = (value)(I64_to_int32(p)|1); */ /*lower part*/ Uint63_mulc(accu, *sp, sp); *--sp = accu; AllocPair(); @@ -1374,40 +1374,11 @@ value coq_interprete Instruct (CHECKDIV21INT63) { print_instr("DIV21INT63"); CheckInt3(); - /* spiwack: takes three int31 (the two first ones represent an - int62) and performs the euclidian division of the - int62 by the int31 */ - /* TODO: implement this - bigint = UI64_of_value(accu); - bigint = I64_or(I64_lsl(bigint, 31),UI64_of_value(*sp++)); - uint64 divisor; - divisor = UI64_of_value(*sp++); - Alloc_small(accu, 2, 1); */ /* ( _ , arity, tag ) */ - /* if (I64_is_zero (divisor)) { - Field(accu, 0) = 1; */ /* 2*0+1 */ - /* Field(accu, 1) = 1; */ /* 2*0+1 */ - /* } - else { - uint64 quo, mod; - I64_udivmod(bigint, divisor, &quo, &mod); - Field(accu, 0) = value_of_uint32(I64_to_int32(quo)); - Field(accu, 1) = value_of_uint32(I64_to_int32(mod)); - } */ - int b; - Uint63_eq0(b, sp[1]); - if (b) { - AllocPair(); - Field(accu, 0) = sp[1]; - Field(accu, 1) = sp[1]; - } - else { - Uint63_div21(accu, sp[0], sp[1], sp); - sp[1] = sp[0]; - Swap_accu_sp; - AllocPair(); - Field(accu, 0) = sp[1]; - Field(accu, 1) = sp[0]; - } + Uint63_div21(accu, sp[0], sp[1], &(sp[1])); + Swap_accu_sp; + AllocPair(); + Field(accu, 0) = sp[1]; + Field(accu, 1) = sp[0]; sp += 2; Next; } @@ -1616,7 +1587,7 @@ value coq_push_vstack(value stk, value max_stack_size) { print_instr("push_vstack");print_int(len); for(i = 0; i < len; i++) coq_sp[i] = Field(stk,i); sp = coq_sp; - CHECK_STACK(uint32_of_value(max_stack_size)); + CHECK_STACK(uint_of_value(max_stack_size)); return Val_unit; } diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h index d982f67566..528cc6fc1f 100644 --- a/kernel/byterun/coq_uint63_emul.h +++ b/kernel/byterun/coq_uint63_emul.h @@ -6,6 +6,8 @@ #define Is_uint63(v) (Tag_val(v) == Custom_tag) +#define uint_of_value(val) (((uint32_t)(val)) >> 1) + # define DECLARE_NULLOP(name) \ value uint63_##name() { \ static value* cb = 0; \ diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h index d431dc1e5c..1fdafc9d8f 100644 --- a/kernel/byterun/coq_uint63_native.h +++ b/kernel/byterun/coq_uint63_native.h @@ -1,5 +1,6 @@ #define Is_uint63(v) (Is_long(v)) +#define uint_of_value(val) (((uint64_t)(val)) >> 1) #define uint63_of_value(val) ((uint64_t)(val) >> 1) /* 2^63 * y + x as a value */ @@ -109,37 +110,56 @@ value uint63_mulc(value x, value y, value* h) { #define lt128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_lt(xl,yl))) #define le128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_leq(xl,yl))) -value uint63_div21(value xh, value xl, value y, value* q) { - xh = (uint64_t)xh >> 1; - xl = ((uint64_t)xl >> 1) | ((uint64_t)xh << 63); - xh = (uint64_t)xh >> 1; +#define maxuint63 ((uint64_t)0x7FFFFFFFFFFFFFFF) +/* precondition: y <> 0 */ +/* outputs r and sets ql to q % 2^63 s.t. x = q * y + r, r < y */ +static value uint63_div21_aux(value xh, value xl, value y, value* ql) { + xh = uint63_of_value(xh); + xl = uint63_of_value(xl); + y = uint63_of_value(y); uint64_t maskh = 0; uint64_t maskl = 1; uint64_t dh = 0; - uint64_t dl = (uint64_t)y >> 1; + uint64_t dl = y; int cmp = 1; - while (dh >= 0 && cmp) { + /* int n = 0 */ + /* loop invariant: mask = 2^n, d = mask * y, (2 * d <= x -> cmp), n >= 0, d < 2^(2*63) */ + while (!(dh >> (63 - 1)) && cmp) { + dh = (dh << 1) | (dl >> (63 - 1)); + dl = (dl << 1) & maxuint63; + maskh = (maskh << 1) | (maskl >> (63 - 1)); + maskl = (maskl << 1) & maxuint63; + /* ++n */ cmp = lt128(dh,dl,xh,xl); - dh = (dh << 1) | (dl >> 63); - dl = dl << 1; - maskh = (maskh << 1) | (maskl >> 63); - maskl = maskl << 1; } uint64_t remh = xh; uint64_t reml = xl; - uint64_t quotient = 0; + /* uint64_t quotienth = 0; */ + uint64_t quotientl = 0; + /* loop invariant: x = quotient * y + rem, y * 2^(n+1) > r, + mask = floor(2^n), d = mask * y, n >= -1 */ while (maskh | maskl) { - if (le128(dh,dl,remh,reml)) { - quotient = quotient | maskl; - if (uint63_lt(reml,dl)) {remh = remh - dh - 1;} else {remh = remh - dh;} + if (le128(dh,dl,remh,reml)) { /* if rem >= d, add one bit and subtract d */ + /* quotienth = quotienth | maskh */ + quotientl = quotientl | maskl; + remh = (uint63_lt(reml,dl)) ? (remh - dh - 1) : (remh - dh); reml = reml - dl; } - maskl = (maskl >> 1) | (maskh << 63); + maskl = (maskl >> 1) | ((maskh << (63 - 1)) & maxuint63); maskh = maskh >> 1; - dl = (dl >> 1) | (dh << 63); + dl = (dl >> 1) | ((dh << (63 - 1)) & maxuint63); dh = dh >> 1; + /* decr n */ } - *q = Val_int(quotient); + *ql = Val_int(quotientl); return Val_int(reml); } +value uint63_div21(value xh, value xl, value y, value* ql) { + if (uint63_of_value(y) == 0) { + *ql = Val_int(0); + return Val_int(0); + } else { + return uint63_div21_aux(xh, xl, y, ql); + } +} #define Uint63_div21(xh, xl, y, q) (accu = uint63_div21(xh, xl, y, q)) diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 412637c4b6..95f88c0306 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -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 diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index b1b69dded8..1a790eaed6 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -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/cbytegen.mli b/kernel/cbytegen.mli index 6a9550342c..bdaf5fe422 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -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/cooking.ml b/kernel/cooking.ml index 9b974c4ecc..9b6e37251f 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -152,11 +152,11 @@ 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; diff --git a/kernel/cooking.mli b/kernel/cooking.mli index b0f143c47d..b022e2ac09 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -13,12 +13,12 @@ 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; @@ -27,7 +27,7 @@ type result = { cook_context : Constr.named_context option; } -val cook_constant : hcons:bool -> recipe -> result +val cook_constant : hcons:bool -> recipe -> Opaqueproof.opaque result val cook_constr : Opaqueproof.cooking_info -> constr -> constr (** {6 Utility functions used in module [Discharge]. } *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 5551742c02..36ee952099 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -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,9 +87,9 @@ 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; @@ -246,7 +246,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.mli b/kernel/declareops.mli index 54a853fc81..fb02c6a029 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -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/entries.ml b/kernel/entries.ml index a3d32267a7..adb3f6bd29 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -108,21 +108,7 @@ type module_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..05f342a82a 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -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 diff --git a/kernel/environ.mli b/kernel/environ.mli index 8c6bc105c7..f6cd41861e 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -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 *) @@ -219,7 +219,7 @@ val constant_context : env -> Constant.t -> Univ.AUContext.t 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 +val body_of_constant_body : env -> Opaqueproof.opaque 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 diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 009eb3da38..bb3b0a538e 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -49,20 +49,6 @@ let weaker_noccur_between env x nvars t = (************************************************************************) (* Various well-formedness check for inductive declarations *) -(* Errors related to inductive constructions *) -type inductive_error = Type_errors.inductive_error = - | NonPos of env * constr * constr - | NotEnoughArgs of env * constr * constr - | NotConstructor of env * Id.t * constr * constr * int * int - | NonPar of env * constr * int * constr * constr - | SameNamesTypes of Id.t - | SameNamesConstructors of Id.t - | SameNamesOverlap of Id.t list - | NotAnArity of env * constr - | BadEntry - | LargeNonPropInductiveNotInType - | BadUnivs - exception InductiveError = Type_errors.InductiveError (************************************************************************) @@ -84,6 +70,7 @@ exception IllFormedInd of ill_formed_ind let mind_extract_params = decompose_prod_n_assum let explain_ind_err id ntyp env nparamsctxt c err = + let open Type_errors in let (_lparams,c') = mind_extract_params nparamsctxt c in match err with | LocalNonPos kt -> @@ -329,7 +316,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( | Prod (na,b,d) -> let () = assert (List.is_empty largs) in if not recursive && not (noccur_between n ntypes b) then - raise (InductiveError BadEntry); + raise (InductiveError Type_errors.BadEntry); let nmr',recarg = check_pos ienv nmr b in let ienv' = ienv_push_var ienv (na,b,mk_norec) in check_constr_rec ienv' nmr' (recarg::lrec) d diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 7810c1723e..1b8e4208ff 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -9,28 +9,9 @@ (************************************************************************) open Names -open Constr open Declarations open Environ open Entries (** Check an inductive. *) val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body - -(** Deprecated *) -type inductive_error = - | NonPos of env * constr * constr - | NotEnoughArgs of env * constr * constr - | NotConstructor of env * Id.t * constr * constr * int * int - | NonPar of env * constr * int * constr * constr - | SameNamesTypes of Id.t - | SameNamesConstructors of Id.t - | SameNamesOverlap of Id.t list - | NotAnArity of env * constr - | BadEntry - | LargeNonPropInductiveNotInType - | BadUnivs -[@@ocaml.deprecated "Use [Type_errors.inductive_error]"] - -exception InductiveError of Type_errors.inductive_error -[@@ocaml.deprecated "Use [Type_errors.InductiveError]"] diff --git a/kernel/modops.ml b/kernel/modops.ml index 4f992d3972..4fdd7ab334 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -608,11 +608,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/names.ml b/kernel/names.ml index 9f27212967..047a1d6525 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -376,9 +376,6 @@ module KerName = struct { modpath; knlabel; refhash = -1; } let repr kn = (kn.modpath, kn.knlabel) - let make2 = make - [@@ocaml.deprecated "Please use [KerName.make]"] - let modpath kn = kn.modpath let label kn = kn.knlabel diff --git a/kernel/names.mli b/kernel/names.mli index 61df3bad0e..2238e932b0 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -278,9 +278,6 @@ sig val make : ModPath.t -> Label.t -> t val repr : t -> ModPath.t * Label.t - val make2 : ModPath.t -> Label.t -> t - [@@ocaml.deprecated "Please use [KerName.make]"] - (** Projections *) val modpath : t -> ModPath.t val label : t -> Label.t diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 96efa7faa5..b5c03b6ca3 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -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/opaqueproof.ml b/kernel/opaqueproof.ml index 303cb06c55..18c1bcc0f8 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -77,29 +77,23 @@ 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 - | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") - | Direct (d,cu) -> - Direct (d,Future.chain cu (fun (c, u) -> f c; c, u)) - let discharge_direct_opaque ~cook_constr ci = function | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") | Direct (d,cu) -> Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u)) -let join_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,cu) -> ignore(Future.join cu) +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 ?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 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 + join except fp let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> @@ -128,16 +122,6 @@ let get_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function then Some(Future.chain (snd (Int.Map.find i prfs)) snd) else !get_univ dp i -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) diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 5ea6da649b..4e8956af06 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -39,12 +39,10 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab 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 * (Univ.Instance.t * Id.t array) Mindmap.t @@ -60,8 +58,7 @@ type cooking_info = { 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 join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit val dump : opaquetab -> Constr.t Future.computation array * diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 673f025c75..a5d8a480ee 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -228,19 +228,11 @@ 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 * Univ.ContextSet.t) Declarations.constant_body; + seff_role : Entries.side_effect_role; } module SideEffects : @@ -254,11 +246,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,41 +269,40 @@ 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 + let acc = match eff.seff_body.const_body with + | Def _ -> acc + | OpaqueDef (_, ctx) -> ctx :: acc + | Primitive _ | Undef _ -> assert false in match eff.seff_body.const_universes with | Monomorphic ctx -> ctx :: acc @@ -558,7 +547,6 @@ 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 @@ -588,32 +576,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 @@ -675,24 +658,22 @@ let inline_private_constants_in_definition_entry env ce = let inline_private_constants_in_constr env body side_eff = pi1 (inline_side_effects env body side_eff) -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 +682,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 @@ -711,9 +693,9 @@ let constant_entry_of_side_effect cb u = 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 + match cb.const_body with + | OpaqueDef (b, c) -> b, c + | Def b -> Mod_subst.force_constr b, Univ.ContextSet.empty | _ -> assert false in DefinitionEntry { const_entry_body = Future.from_val (pt, ()); @@ -724,21 +706,7 @@ let constant_entry_of_side_effect cb u = 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) let export_side_effects mb env c = @@ -751,60 +719,62 @@ let export_side_effects mb env c = 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 + let ctx = match eff.seff_body.const_body with + | Def _ -> ctx + | OpaqueDef (_, ctx') -> Univ.ContextSet.union ctx' ctx + | Undef _ | Primitive _ -> assert false 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 -> + | 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 cb = map_constant Future.force 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 map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create (Future.from_val p)) cb) in + let bodies = List.map map exported in let exported = List.map (fun (kn, _, r) -> (kn, r)) 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 ~hcons:(not in_section) senv.env kn r in + let cb = if in_section then cb else Declareops.hcons_const_body cb in + let senv = add_constant_aux ~in_section senv (kn, cb) in + kn, senv + +let add_constant ?role ~in_section l decl senv = let kn = Constant.make2 senv.modpath l in - let senv = let cb = match decl with | ConstantEntry (EffectEntry, ce) -> @@ -816,9 +786,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 Opaqueproof.create cb in add_constant_aux ~in_section senv (kn, cb) in let senv = match decl with @@ -827,7 +797,20 @@ let add_constant ~in_section l decl senv = add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv | _ -> senv in - kn, senv + let eff = match role with + | None -> empty_private_constants + | Some role -> + let cb = map_constant Future.force cb in + let from_env = CEphemeron.create senv.revstruct in + let eff = { + from_env = from_env; + seff_constant = kn; + seff_body = cb; + seff_role = role; + } in + SideEffects.add eff empty_private_constants + in + (kn, eff), senv (** Insertion of inductive types *) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 46c97c1fb8..36ca3d8c47 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -43,25 +43,20 @@ 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 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 val is_curmod_library : safe_environment -> bool @@ -93,7 +88,6 @@ 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 @@ -105,8 +99,11 @@ val export_private_constants : in_section:bool -> (** returns the main constant plus a list of auxiliary constants (empty unless one requires the side effects to be exported) *) val add_constant : - in_section:bool -> Label.t -> global_declaration -> - Constant.t safe_transformer + ?role:Entries.side_effect_role -> in_section:bool -> Label.t -> global_declaration -> + (Constant.t * private_constants) safe_transformer + +val add_recipe : + in_section:bool -> Label.t -> Cooking.recipe -> Constant.t safe_transformer (** Adding an inductive type *) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 1857ea3329..24845ce459 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -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/term_typing.ml b/kernel/term_typing.ml index faa4411e92..74c6189a65 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -154,7 +154,7 @@ the polymorphic case let c = Constr.hcons j.uj_val in feedback_completion_typecheck feedback_id; c, uctx) in - let def = OpaqueDef (Opaqueproof.create proofterm) in + let def = OpaqueDef proofterm in { Cooking.cook_body = def; cook_type = tyj.utj_val; @@ -207,7 +207,7 @@ the polymorphic case 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))) + if opaque then OpaqueDef (Future.from_val (def, Univ.ContextSet.empty)) else Def (Mod_subst.from_val def) in feedback_completion_typecheck feedback_id; @@ -232,7 +232,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 +271,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 +293,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 @@ -318,8 +319,8 @@ let build_constant_declaration _kn env result = (*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,8 +328,21 @@ 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 ~hcons env _kn r = + let open Cooking in + let result = Cooking.cook_constant ~hcons 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_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 } let translate_local_def env _id centry = let open Cooking in @@ -351,8 +365,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,8 +375,7 @@ 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 diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 1fa5eca2e3..592a97e132 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -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 : hcons:bool -> 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/typeops.ml b/kernel/typeops.ml index 12ffbf4357..af710e7822 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -462,28 +462,6 @@ let type_of_global_in_context env r = let inst = Univ.make_abstract_instance univs in Inductive.type_of_constructor (cstr,inst) specif, univs -(* Build a fresh instance for a given context, its associated substitution and - the instantiated constraints. *) - -let constr_of_global_in_context env r = - let open GlobRef in - match r with - | VarRef id -> mkVar id, Univ.AUContext.empty - | ConstRef c -> - let cb = lookup_constant c env in - let univs = Declareops.constant_polymorphic_context cb in - mkConstU (c, Univ.make_abstract_instance univs), univs - | IndRef ind -> - let (mib,_) = Inductive.lookup_mind_specif env ind in - let univs = Declareops.inductive_polymorphic_context mib in - mkIndU (ind, Univ.make_abstract_instance univs), univs - | ConstructRef cstr -> - let (mib,_) = - Inductive.lookup_mind_specif env (inductive_of_constructor cstr) - in - let univs = Declareops.inductive_polymorphic_context mib in - mkConstructU (cstr, Univ.make_abstract_instance univs), univs - (************************************************************************) (************************************************************************) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index cc1885f42d..c8f3e506e6 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -107,14 +107,6 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t usage. For non-universe-polymorphic constants, it does not matter. *) -(** {6 Building a term from a global reference *) - -(** Map a global reference to a term in its local universe - context. The term should not be used without pushing it's universe - context in the environmnent of usage. For non-universe-polymorphic - constants, it does not matter. *) -val constr_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t - (** {6 Miscellaneous. } *) (** Check that hyps are included in env and fails with error otherwise *) diff --git a/kernel/uint63.mli b/kernel/uint63.mli index b5f40ca804..f25f24512d 100644 --- a/kernel/uint63.mli +++ b/kernel/uint63.mli @@ -40,6 +40,10 @@ val rem : t -> t -> t (* Specific arithmetic operations *) val mulc : t -> t -> t * t val addmuldiv : t -> t -> t -> t + +(** [div21 xh xl y] returns [q % 2^63, r] + s.t. [xh * 2^63 + xl = q * y + r] and [r < y]. + When [y] is [0], returns [0, 0]. *) val div21 : t -> t -> t -> t * t (* comparison *) diff --git a/kernel/uint63_amd64.ml b/kernel/uint63_amd64.ml index 010b594de8..2d4d685775 100644 --- a/kernel/uint63_amd64.ml +++ b/kernel/uint63_amd64.ml @@ -102,26 +102,35 @@ let le128 xh xl yh yl = lt xh yh || (xh = yh && le xl yl) (* division of two numbers by one *) +(* precondition: y <> 0 *) +(* outputs: q % 2^63, r s.t. x = q * y + r, r < y *) let div21 xh xl y = let maskh = ref 0 in let maskl = ref 1 in let dh = ref 0 in let dl = ref y in let cmp = ref true in - while !dh >= 0 && !cmp do - cmp := lt128 !dh !dl xh xl; + (* n = ref 0 *) + (* loop invariant: mask = 2^n, d = mask * y, (2 * d <= x -> cmp), n >= 0 *) + while !dh >= 0 && !cmp do (* dh >= 0 tests that dh highest bit is zero *) (* We don't use addmuldiv below to avoid checks on 1 *) dh := (!dh lsl 1) lor (!dl lsr (uint_size - 1)); dl := !dl lsl 1; maskh := (!maskh lsl 1) lor (!maskl lsr (uint_size - 1)); - maskl := !maskl lsl 1 - done; (* mask = 2^N, d = 2^N * d, d >= x *) + maskl := !maskl lsl 1; + (* incr n *) + cmp := lt128 !dh !dl xh xl; + done; (* mask = 2^n, d = 2^n * y, 2 * d > x *) let remh = ref xh in let reml = ref xl in - let quotient = ref 0 in + (* quotienth = ref 0 *) + let quotientl = ref 0 in + (* loop invariant: x = quotient * y + rem, y * 2^(n+1) > r, + mask = floor(2^n), d = mask * y, n >= -1 *) while !maskh lor !maskl <> 0 do if le128 !dh !dl !remh !reml then begin (* if rem >= d, add one bit and subtract d *) - quotient := !quotient lor !maskl; + (* quotienth := !quotienth lor !maskh *) + quotientl := !quotientl lor !maskl; remh := if lt !reml !dl then !remh - !dh - 1 else !remh - !dh; reml := !reml - !dl; end; @@ -129,8 +138,11 @@ let div21 xh xl y = maskh := !maskh lsr 1; dl := (!dl lsr 1) lor (!dh lsl (uint_size - 1)); dh := !dh lsr 1; + (* decr n *) done; - !quotient, !reml + !quotientl, !reml + +let div21 xh xl y = if y = 0 then 0, 0 else div21 xh xl y (* exact multiplication *) (* TODO: check that none of these additions could be a logical or *) diff --git a/kernel/uint63_x86.ml b/kernel/uint63_x86.ml index 461184c432..fa45c90241 100644 --- a/kernel/uint63_x86.ml +++ b/kernel/uint63_x86.ml @@ -94,26 +94,35 @@ let le128 xh xl yh yl = lt xh yh || (xh = yh && le xl yl) (* division of two numbers by one *) +(* precondition: y <> 0 *) +(* outputs: q % 2^63, r s.t. x = q * y + r, r < y *) let div21 xh xl y = let maskh = ref zero in let maskl = ref one in let dh = ref zero in let dl = ref y in let cmp = ref true in - while le zero !dh && !cmp do - cmp := lt128 !dh !dl xh xl; + (* n = ref 0 *) + (* loop invariant: mask = 2^n, d = mask * y, (2 * d <= x -> cmp), n >= 0 *) + while Int64.equal (l_sr !dh (of_int (uint_size - 1))) zero && !cmp do (* We don't use addmuldiv below to avoid checks on 1 *) dh := l_or (l_sl !dh one) (l_sr !dl (of_int (uint_size - 1))); dl := l_sl !dl one; maskh := l_or (l_sl !maskh one) (l_sr !maskl (of_int (uint_size - 1))); - maskl := l_sl !maskl one - done; (* mask = 2^N, d = 2^N * d, d >= x *) + maskl := l_sl !maskl one; + (* incr n *) + cmp := lt128 !dh !dl xh xl; + done; (* mask = 2^n, d = 2^n * d, 2 * d > x *) let remh = ref xh in let reml = ref xl in - let quotient = ref zero in + (* quotienth = ref 0 *) + let quotientl = ref zero in + (* loop invariant: x = quotient * y + rem, y * 2^(n+1) > r, + mask = floor(2^n), d = mask * y, n >= -1 *) while not (Int64.equal (l_or !maskh !maskl) zero) do if le128 !dh !dl !remh !reml then begin (* if rem >= d, add one bit and subtract d *) - quotient := l_or !quotient !maskl; + (* quotienth := !quotienth lor !maskh *) + quotientl := l_or !quotientl !maskl; remh := if lt !reml !dl then sub (sub !remh !dh) one else sub !remh !dh; reml := sub !reml !dl end; @@ -121,9 +130,11 @@ let div21 xh xl y = maskh := l_sr !maskh one; dl := l_or (l_sr !dl one) (l_sl !dh (of_int (uint_size - 1))); dh := l_sr !dh one + (* decr n *) done; - !quotient, !reml + !quotientl, !reml +let div21 xh xl y = if Int64.equal y zero then zero, zero else div21 xh xl y (* exact multiplication *) let mulc x y = diff --git a/kernel/univ.ml b/kernel/univ.ml index 8263c68bf5..b1bbc25fe6 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -231,18 +231,15 @@ module LMap = struct module M = HMap.Make (Level) include M - let union l r = - merge (fun _k l r -> - match l, r with - | Some _, _ -> l - | _, _ -> r) l r + let lunion l r = + union (fun _k l _r -> Some l) l r - let subst_union l r = - merge (fun _k l r -> + let subst_union l r = + union (fun _k l r -> match l, r with - | Some (Some _), _ -> l - | Some None, None -> l - | _, _ -> r) l r + | Some _, _ -> Some l + | None, None -> Some l + | _, _ -> Some r) l r let diff ext orig = fold (fun u v acc -> diff --git a/kernel/univ.mli b/kernel/univ.mli index 5543c35741..db178c4bb0 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -223,8 +223,8 @@ module LMap : sig include CMap.ExtS with type key = Level.t and module Set := LSet - val union : 'a t -> 'a t -> 'a t - (** [union x y] favors the bindings in the first map. *) + val lunion : 'a t -> 'a t -> 'a t + (** [lunion x y] favors the bindings in the first map. *) val diff : 'a t -> 'a t -> 'a t (** [diff x y] removes bindings from x that appear in y (whatever the value). *) |