diff options
42 files changed, 473 insertions, 580 deletions
@@ -53,6 +53,10 @@ Coq binaries and process model Changes from 8.8.0 to 8.8.1 =========================== +Kernel + +- Fix a critical bug with cofixpoints and vm_compute/native_compute (#7333). + Notations - Fixed unexpected collision between only-parsing and only-printing diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 129f171b2..10a7a4158 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -232,7 +232,7 @@ let ppenv e = pp let ppenvwithcst e = pp (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++ str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++ - str "{" ++ Cmap_env.fold (fun a _ s -> Constant.print a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}") + str "{" ++ Cmap_env.fold (fun a _ s -> Constant.print a ++ spc () ++ s) (Obj.magic e).env_globals.env_constants (mt ()) ++ str "}") let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x)) diff --git a/engine/eConstr.ml b/engine/eConstr.ml index f1530b2d1..6810626ad 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -783,7 +783,7 @@ let of_existential : Constr.existential -> existential = let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e) let lookup_named n e = cast_named_decl (sym unsafe_eq) (lookup_named n e) -let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_val n e) +let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_ctxt n e) let map_rel_context_in_env f env sign = let rec aux env acc = function diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 38ceed569..afedfe180 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -13,7 +13,6 @@ open Util open Names open Term open Constr -open Pre_env open Environ open Evd open Termops diff --git a/engine/termops.ml b/engine/termops.ml index bd07555a5..c52f96079 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1379,7 +1379,7 @@ let smash_rel_context sign = let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init let mem_named_context_val id ctxt = - try ignore(Environ.lookup_named_val id ctxt); true with Not_found -> false + try ignore(Environ.lookup_named_ctxt id ctxt); true with Not_found -> false let map_rel_decl f = function | RelDecl.LocalAssum (id, t) -> RelDecl.LocalAssum (id, f t) diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 8ac1ecc79..a944dbb06 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1032,7 +1032,7 @@ value coq_interprete CHECK_STACK(nargs+1); sp -= nargs; for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2); - *--sp = accu; // Last argument is the pointer to the suspension + *--sp = accu; // Leftmost argument is the pointer to the suspension print_lint(nargs); coq_extra_args = nargs; pc = Code_val(coq_env); // Trigger evaluation diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 435cf0a79..4da5f0f38 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -265,7 +265,7 @@ type 'a infos_cache = { i_repr : 'a infos -> 'a infos_tab -> constr -> 'a; i_env : env; i_sigma : existential -> constr option; - i_rels : (Context.Rel.Declaration.t * Pre_env.lazy_val) Range.t; + i_rels : (Context.Rel.Declaration.t * lazy_val) Range.t; } and 'a infos = { @@ -314,12 +314,11 @@ let evar_value cache ev = cache.i_sigma ev let create mk_cl flgs env evars = - let open Pre_env in let cache = { i_repr = mk_cl; i_env = env; i_sigma = evars; - i_rels = (Environ.pre_env env).env_rel_context.env_rel_map; + i_rels = env.env_rel_context.env_rel_map; } in { i_flags = flgs; i_cache = cache } diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 5ed9b6c67..599856b64 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -309,7 +309,7 @@ let rec pp_instr i = prlist_with_sep spc pp_lbl (Array.to_list lblb)) | Kpushfields n -> str "pushfields " ++ int n | Kfield n -> str "field " ++ int n - | Ksetfield n -> str "set field" ++ int n + | Ksetfield n -> str "setfield " ++ int n | Kstop -> str "stop" diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index a771945dd..df5b17da3 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -20,7 +20,7 @@ open Cinstr open Clambda open Constr open Declarations -open Pre_env +open Environ (* Compilation of variables + computing free variables *) @@ -77,6 +77,7 @@ open Pre_env (* ai' = [A_t | accumulate | [Cfx_t | fcofixi] | arg1 | ... | argp ] *) (* If such a block is matched against, we have to force evaluation, *) (* function [fcofixi] is then applied to [ai'] [arg1] ... [argp] *) +(* (note that [ai'] is a pointer to the closure, passed as argument) *) (* Once evaluation is completed [ai'] is updated with the result: *) (* ai' <-- *) (* [A_t | accumulate | [Cfxe_t |fcofixi|result] | arg1 | ... | argp ] *) diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index 1c4cdcbeb..57d3e6fc2 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -12,7 +12,7 @@ open Cbytecodes open Cemitcodes open Constr open Declarations -open Pre_env +open Environ (** Should only be used for monomorphic terms *) val compile : fail_on_error:bool -> diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli index 4a3c03d85..f42c46175 100644 --- a/kernel/cinstr.mli +++ b/kernel/cinstr.mli @@ -31,7 +31,7 @@ and lambda = | Lprim of pconstant * int (* arity *) * instruction * lambda array | Lcase of case_info * reloc_table * lambda * lambda * lam_branches | Lfix of (int array * int) * fix_decl - | Lcofix of int * fix_decl + | Lcofix of int * fix_decl (* must be in eta-expanded form *) | Lmakeblock of int * lambda array | Lval of structured_constant | Lsort of Sorts.t @@ -39,6 +39,10 @@ and lambda = | Lproj of int * Constant.t * lambda | Luint of uint +(* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation +to be correct. Otherwise, memoization of previous evaluations will be applied +again to extra arguments (see #7333). *) + and lam_branches = { constant_branches : lambda array; nonconstant_branches : (Name.t array * lambda) array } diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 0727eaeac..8389dd326 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -6,7 +6,7 @@ open Constr open Declarations open Cbytecodes open Cinstr -open Pre_env +open Environ open Pp let pr_con sp = str(Names.Label.to_string (Constant.label sp)) @@ -700,6 +700,7 @@ let rec lambda_of_constr env c = Lfix(rec_init, (names, ltypes, lbodies)) | CoFix(init,(names,type_bodies,rec_bodies)) -> + let rec_bodies = Array.map2 (Reduction.eta_expand env.global_env) rec_bodies type_bodies in let ltypes = lambda_of_args env 0 type_bodies in Renv.push_rels env names; let lbodies = lambda_of_args env 0 rec_bodies in diff --git a/kernel/clambda.mli b/kernel/clambda.mli index 6cf46163e..8ff10b454 100644 --- a/kernel/clambda.mli +++ b/kernel/clambda.mli @@ -1,13 +1,14 @@ open Names open Cinstr +open Environ exception TooLargeInductive of Pp.t -val lambda_of_constr : optimize:bool -> Pre_env.env -> Constr.t -> lambda +val lambda_of_constr : optimize:bool -> env -> Constr.t -> lambda val decompose_Llam : lambda -> Name.t array * lambda -val get_alias : Pre_env.env -> Constant.t -> Constant.t +val get_alias : env -> Constant.t -> Constant.t val compile_prim : int -> Cbytecodes.instruction -> Constr.pconstant -> bool -> lambda array -> lambda diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 4f3cbf289..9bacdb65f 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -20,7 +20,7 @@ open Vmvalues open Cemitcodes open Cbytecodes open Declarations -open Pre_env +open Environ open Cbytegen module NamedDecl = Context.Named.Declaration @@ -142,23 +142,23 @@ and slot_for_fv env fv = | None -> v_of_id id, Id.Set.empty | Some c -> val_of_constr (env_of_id id env) c, - Environ.global_vars_set (Environ.env_of_pre_env env) c in + Environ.global_vars_set env c in build_lazy_val cache (v, d); v in let val_of_rel i = val_of_rel (nb_rel env - i) in let idfun _ x = x in match fv with | FVnamed id -> - let nv = Pre_env.lookup_named_val id env in + let nv = lookup_named_val id env in begin match force_lazy_val nv with | None -> - env |> Pre_env.lookup_named id |> NamedDecl.get_value |> fill_fv_cache nv id val_of_named idfun + env |> lookup_named id |> NamedDecl.get_value |> fill_fv_cache nv id val_of_named idfun | Some (v, _) -> v end | FVrel i -> - let rv = Pre_env.lookup_rel_val i env in + let rv = lookup_rel_val i env in begin match force_lazy_val rv with | None -> - env |> Pre_env.lookup_rel i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel + env |> lookup_rel i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel | Some (v, _) -> v end | FVevar evk -> val_of_evar evk diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli index d32cfba36..72c96b0b9 100644 --- a/kernel/csymtable.mli +++ b/kernel/csymtable.mli @@ -12,7 +12,7 @@ open Names open Constr -open Pre_env +open Environ val val_of_constr : env -> constr -> Vmvalues.values diff --git a/kernel/environ.ml b/kernel/environ.ml index 9d4063e43..c3e7cec75 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -28,26 +28,204 @@ open Names open Constr open Vars open Declarations -open Pre_env open Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + (* The type of environments. *) -type named_context_val = Pre_env.named_context_val +(* The key attached to each constant is used by the VM to retrieve previous *) +(* evaluations of the constant. It is essentially an index in the symbols table *) +(* used by the VM. *) +type key = int CEphemeron.key option ref + +(** Linking information for the native compiler. *) + +type link_info = + | Linked of string + | LinkedInteractive of string + | NotLinked + +type constant_key = constant_body * (link_info ref * key) + +type mind_key = mutual_inductive_body * link_info ref + +type globals = { + env_constants : constant_key Cmap_env.t; + env_inductives : mind_key Mindmap_env.t; + env_modules : module_body MPmap.t; + env_modtypes : module_type_body MPmap.t} + +type stratification = { + env_universes : UGraph.t; + env_engagement : engagement +} + +type val_kind = + | VKvalue of (Vmvalues.values * Id.Set.t) CEphemeron.key + | VKnone + +type lazy_val = val_kind ref + +let force_lazy_val vk = match !vk with +| VKnone -> None +| VKvalue v -> try Some (CEphemeron.get v) with CEphemeron.InvalidKey -> None + +let dummy_lazy_val () = ref VKnone +let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key) + +type named_context_val = { + env_named_ctx : Context.Named.t; + env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; +} + +type rel_context_val = { + env_rel_ctx : Context.Rel.t; + env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t; +} + +type env = { + env_globals : globals; (* globals = constants + inductive types + modules + module-types *) + env_named_context : named_context_val; (* section variables *) + env_rel_context : rel_context_val; + env_nb_rel : int; + env_stratification : stratification; + env_typing_flags : typing_flags; + retroknowledge : Retroknowledge.retroknowledge; + indirect_pterms : Opaqueproof.opaquetab; +} + +let empty_named_context_val = { + env_named_ctx = []; + env_named_map = Id.Map.empty; +} + +let empty_rel_context_val = { + env_rel_ctx = []; + env_rel_map = Range.empty; +} + +let empty_env = { + env_globals = { + env_constants = Cmap_env.empty; + env_inductives = Mindmap_env.empty; + env_modules = MPmap.empty; + env_modtypes = MPmap.empty}; + env_named_context = empty_named_context_val; + env_rel_context = empty_rel_context_val; + env_nb_rel = 0; + env_stratification = { + env_universes = UGraph.initial_universes; + env_engagement = PredicativeSet }; + env_typing_flags = Declareops.safe_flags Conv_oracle.empty; + retroknowledge = Retroknowledge.initial_retroknowledge; + indirect_pterms = Opaqueproof.empty_opaquetab } + + +(* Rel context *) + +let push_rel_context_val d ctx = { + env_rel_ctx = Context.Rel.add d ctx.env_rel_ctx; + env_rel_map = Range.cons (d, ref VKnone) ctx.env_rel_map; +} + +let match_rel_context_val ctx = match ctx.env_rel_ctx with +| [] -> None +| decl :: rem -> + let (_, lval) = Range.hd ctx.env_rel_map in + let ctx = { env_rel_ctx = rem; env_rel_map = Range.tl ctx.env_rel_map } in + Some (decl, lval, ctx) + +let push_rel d env = + { env with + env_rel_context = push_rel_context_val d env.env_rel_context; + env_nb_rel = env.env_nb_rel + 1 } + +let lookup_rel n env = + try fst (Range.get env.env_rel_context.env_rel_map (n - 1)) + with Invalid_argument _ -> raise Not_found + +let lookup_rel_val n env = + try snd (Range.get env.env_rel_context.env_rel_map (n - 1)) + with Invalid_argument _ -> raise Not_found + +let rel_skipn n ctx = { + env_rel_ctx = Util.List.skipn n ctx.env_rel_ctx; + env_rel_map = Range.skipn n ctx.env_rel_map; +} + +let env_of_rel n env = + { env with + env_rel_context = rel_skipn n env.env_rel_context; + env_nb_rel = env.env_nb_rel - n + } + +(* Named context *) + +let push_named_context_val_val d rval ctxt = +(* assert (not (Id.Map.mem (NamedDecl.get_id d) ctxt.env_named_map)); *) + { + env_named_ctx = Context.Named.add d ctxt.env_named_ctx; + env_named_map = Id.Map.add (NamedDecl.get_id d) (d, rval) ctxt.env_named_map; + } + +let push_named_context_val d ctxt = + push_named_context_val_val d (ref VKnone) ctxt + +let match_named_context_val c = match c.env_named_ctx with +| [] -> None +| decl :: ctx -> + let (_, v) = Id.Map.find (NamedDecl.get_id decl) c.env_named_map in + let map = Id.Map.remove (NamedDecl.get_id decl) c.env_named_map in + let cval = { env_named_ctx = ctx; env_named_map = map } in + Some (decl, v, cval) + +let map_named_val f ctxt = + let open Context.Named.Declaration in + let fold accu d = + let d' = map_constr f d in + let accu = + if d == d' then accu + else Id.Map.modify (get_id d) (fun _ (_, v) -> (d', v)) accu + in + (accu, d') + in + let map, ctx = List.fold_left_map fold ctxt.env_named_map ctxt.env_named_ctx in + if map == ctxt.env_named_map then ctxt + else { env_named_ctx = ctx; env_named_map = map } + +let push_named d env = + {env with env_named_context = push_named_context_val d env.env_named_context} + +let lookup_named id env = + fst (Id.Map.find id env.env_named_context.env_named_map) + +let lookup_named_val id env = + snd(Id.Map.find id env.env_named_context.env_named_map) + +let lookup_named_ctxt id ctxt = + fst (Id.Map.find id ctxt.env_named_map) + +(* Global constants *) -type env = Pre_env.env +let lookup_constant_key kn env = + Cmap_env.find kn env.env_globals.env_constants + +let lookup_constant kn env = + fst (Cmap_env.find kn env.env_globals.env_constants) + +(* Mutual Inductives *) +let lookup_mind kn env = + fst (Mindmap_env.find kn env.env_globals.env_inductives) + +let lookup_mind_key kn env = + Mindmap_env.find kn env.env_globals.env_inductives -let pre_env env = env -let env_of_pre_env env = env let oracle env = env.env_typing_flags.conv_oracle let set_oracle env o = let env_typing_flags = { env.env_typing_flags with conv_oracle = o } in { env with env_typing_flags } -let empty_named_context_val = empty_named_context_val - -let empty_env = empty_env - let engagement env = env.env_stratification.env_engagement let typing_flags env = env.env_typing_flags @@ -72,15 +250,11 @@ let empty_context env = | _ -> false (* Rel context *) -let lookup_rel = lookup_rel - let evaluable_rel n env = is_local_def (lookup_rel n env) let nb_rel env = env.env_nb_rel -let push_rel = push_rel - let push_rel_context ctxt x = Context.Rel.fold_outside push_rel ctxt ~init:x let push_rec_types (lna,typarray,_) env = @@ -105,24 +279,14 @@ let named_context_of_val c = c.env_named_ctx let ids_of_named_context_val c = Id.Map.domain c.env_named_map -(* [map_named_val f ctxt] apply [f] to the body and the type of - each declarations. - *** /!\ *** [f t] should be convertible with t *) -let map_named_val = map_named_val - let empty_named_context = Context.Named.empty -let push_named = push_named let push_named_context = List.fold_right push_named -let push_named_context_val = push_named_context_val let val_of_named_context ctxt = List.fold_right push_named_context_val ctxt empty_named_context_val -let lookup_named = lookup_named -let lookup_named_val id ctxt = fst (Id.Map.find id ctxt.env_named_map) - let eq_named_context_val c1 c2 = c1 == c2 || Context.Named.equal Constr.equal (named_context_of_val c1) (named_context_of_val c2) @@ -181,7 +345,10 @@ let map_universes f env = let s = env.env_stratification in { env with env_stratification = { s with env_universes = f s.env_universes } } - + +let set_universes env u = + { env with env_stratification = { env.env_stratification with env_universes = u } } + let add_constraints c env = if Univ.Constraint.is_empty c then env else map_universes (UGraph.merge_constraints c) env @@ -221,8 +388,6 @@ let set_typing_flags c env = (* Unsafe *) (* Global constants *) -let lookup_constant = lookup_constant - let no_link_info = NotLinked let add_constant_key kn cb linkinfo env = @@ -330,8 +495,6 @@ let is_projection cst env = | None -> false (* Mutual Inductives *) -let lookup_mind = lookup_mind - let polymorphic_ind (mind,i) env = Declareops.inductive_is_polymorphic (lookup_mind mind env) @@ -468,10 +631,6 @@ type 'types punsafe_type_judgment = { type unsafe_type_judgment = types punsafe_type_judgment -(*s Compilation of global declaration *) - -let compile_constant_body = Cbytegen.compile_constant_body ~fail_on_error:false - exception Hyp_not_found let apply_to_hyp ctxt id f = @@ -530,121 +689,3 @@ let register env field entry = in register_one (register_one env (KInt31 (grp,Int31Constructor)) i31c) field entry | field -> register_one env field entry - -(* the Environ.register function syncrhonizes the proactive and reactive - retroknowledge. *) -let dispatch = - - (* subfunction used for static decompilation of int31 (after a vm_compute, - see pretyping/vnorm.ml for more information) *) - let constr_of_int31 = - let nth_digit_plus_one i n = (* calculates the nth (starting with 0) - digit of i and adds 1 to it - (nth_digit_plus_one 1 3 = 2) *) - if Int.equal (i land (1 lsl n)) 0 then - 1 - else - 2 - in - fun ind -> fun digit_ind -> fun tag -> - let array_of_int i = - Array.init 31 (fun n -> mkConstruct - (digit_ind, nth_digit_plus_one i (30-n))) - in - (* We check that no bit above 31 is set to one. This assertion used to - fail in the VM, and led to conversion tests failing at Qed. *) - assert (Int.equal (tag lsr 31) 0); - mkApp(mkConstruct(ind, 1), array_of_int tag) - in - - (* subfunction which dispatches the compiling information of an - int31 operation which has a specific vm instruction (associates - it to the name of the coq definition in the reactive retroknowledge) *) - let int31_op n op prim kn = - { empty_reactive_info with - vm_compiling = Some (Clambda.compile_prim n op kn); - native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn)); - } - in - -fun rk value field -> - (* subfunction which shortens the (very common) dispatch of operations *) - let int31_op_from_const n op prim = - match kind value with - | Const kn -> int31_op n op prim kn - | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant.") - in - let int31_binop_from_const op prim = int31_op_from_const 2 op prim in - let int31_unop_from_const op prim = int31_op_from_const 1 op prim in - match field with - | KInt31 (grp, Int31Type) -> - let int31bit = - (* invariant : the type of bits is registered, otherwise the function - would raise Not_found. The invariant is enforced in safe_typing.ml *) - match field with - | KInt31 (grp, Int31Type) -> Retroknowledge.find rk (KInt31 (grp,Int31Bits)) - | _ -> anomaly ~label:"Environ.register" - (Pp.str "add_int31_decompilation_from_type called with an abnormal field.") - in - let i31bit_type = - match kind int31bit with - | Ind (i31bit_type,_) -> i31bit_type - | _ -> anomaly ~label:"Environ.register" - (Pp.str "Int31Bits should be an inductive type.") - in - let int31_decompilation = - match kind value with - | Ind (i31t,_) -> - constr_of_int31 i31t i31bit_type - | _ -> anomaly ~label:"Environ.register" - (Pp.str "should be an inductive type.") - in - { empty_reactive_info with - vm_decompile_const = Some int31_decompilation; - vm_before_match = Some Clambda.int31_escape_before_match; - native_before_match = Some (Nativelambda.before_match_int31 i31bit_type); - } - | KInt31 (_, Int31Constructor) -> - { empty_reactive_info with - vm_constant_static = Some Clambda.compile_structured_int31; - vm_constant_dynamic = Some Clambda.dynamic_int31_compilation; - native_constant_static = Some Nativelambda.compile_static_int31; - native_constant_dynamic = Some Nativelambda.compile_dynamic_int31; - } - | KInt31 (_, Int31Plus) -> int31_binop_from_const Cbytecodes.Kaddint31 - CPrimitives.Int31add - | KInt31 (_, Int31PlusC) -> int31_binop_from_const Cbytecodes.Kaddcint31 - CPrimitives.Int31addc - | KInt31 (_, Int31PlusCarryC) -> int31_binop_from_const Cbytecodes.Kaddcarrycint31 - CPrimitives.Int31addcarryc - | KInt31 (_, Int31Minus) -> int31_binop_from_const Cbytecodes.Ksubint31 - CPrimitives.Int31sub - | KInt31 (_, Int31MinusC) -> int31_binop_from_const Cbytecodes.Ksubcint31 - CPrimitives.Int31subc - | KInt31 (_, Int31MinusCarryC) -> int31_binop_from_const - Cbytecodes.Ksubcarrycint31 CPrimitives.Int31subcarryc - | KInt31 (_, Int31Times) -> int31_binop_from_const Cbytecodes.Kmulint31 - CPrimitives.Int31mul - | KInt31 (_, Int31TimesC) -> int31_binop_from_const Cbytecodes.Kmulcint31 - CPrimitives.Int31mulc - | KInt31 (_, Int31Div21) -> int31_op_from_const 3 Cbytecodes.Kdiv21int31 - CPrimitives.Int31div21 - | KInt31 (_, Int31Diveucl) -> int31_binop_from_const Cbytecodes.Kdivint31 - CPrimitives.Int31diveucl - | KInt31 (_, Int31AddMulDiv) -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31 - CPrimitives.Int31addmuldiv - | KInt31 (_, Int31Compare) -> int31_binop_from_const Cbytecodes.Kcompareint31 - CPrimitives.Int31compare - | KInt31 (_, Int31Head0) -> int31_unop_from_const Cbytecodes.Khead0int31 - CPrimitives.Int31head0 - | KInt31 (_, Int31Tail0) -> int31_unop_from_const Cbytecodes.Ktail0int31 - CPrimitives.Int31tail0 - | KInt31 (_, Int31Lor) -> int31_binop_from_const Cbytecodes.Klorint31 - CPrimitives.Int31lor - | KInt31 (_, Int31Land) -> int31_binop_from_const Cbytecodes.Klandint31 - CPrimitives.Int31land - | KInt31 (_, Int31Lxor) -> int31_binop_from_const Cbytecodes.Klxorint31 - CPrimitives.Int31lxor - | _ -> empty_reactive_info - -let _ = Hook.set Retroknowledge.dispatch_hook dispatch diff --git a/kernel/environ.mli b/kernel/environ.mli index fdd84b25b..fc45ce0e3 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -28,16 +28,60 @@ open Declarations - a set of universe constraints - a flag telling if Set is, can be, or cannot be set impredicative *) +type lazy_val + +val build_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) -> unit +val force_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) option +val dummy_lazy_val : unit -> lazy_val + +(** Linking information for the native compiler *) +type link_info = + | Linked of string + | LinkedInteractive of string + | NotLinked + +type key = int CEphemeron.key option ref + +type constant_key = constant_body * (link_info ref * key) + +type mind_key = mutual_inductive_body * link_info ref + +type globals = { + env_constants : constant_key Cmap_env.t; + env_inductives : mind_key Mindmap_env.t; + env_modules : module_body MPmap.t; + env_modtypes : module_type_body MPmap.t +} + +type stratification = { + env_universes : UGraph.t; + env_engagement : engagement +} + +type named_context_val = private { + env_named_ctx : Context.Named.t; + env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; +} + +type rel_context_val = private { + env_rel_ctx : Context.Rel.t; + env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t; +} + +type env = private { + env_globals : globals; (* globals = constants + inductive types + modules + module-types *) + env_named_context : named_context_val; (* section variables *) + env_rel_context : rel_context_val; + env_nb_rel : int; + env_stratification : stratification; + env_typing_flags : typing_flags; + retroknowledge : Retroknowledge.retroknowledge; + indirect_pterms : Opaqueproof.opaquetab; +} - - -type env -val pre_env : env -> Pre_env.env -val env_of_pre_env : Pre_env.env -> env val oracle : env -> Conv_oracle.oracle val set_oracle : env -> Conv_oracle.oracle -> env -type named_context_val val eq_named_context_val : named_context_val -> named_context_val -> bool val empty_env : env @@ -70,7 +114,9 @@ val push_rec_types : rec_declaration -> env -> env (** Looks up in the context of local vars referred by indice ([rel_context]) raises [Not_found] if the index points out of the context *) val lookup_rel : int -> env -> Context.Rel.Declaration.t +val lookup_rel_val : int -> env -> lazy_val val evaluable_rel : int -> env -> bool +val env_of_rel : int -> env -> env (** {6 Recurrence on [rel_context] } *) @@ -102,7 +148,8 @@ val push_named_context_val : raises [Not_found] if the Id.t is not found *) val lookup_named : variable -> env -> Context.Named.Declaration.t -val lookup_named_val : variable -> named_context_val -> Context.Named.Declaration.t +val lookup_named_val : variable -> env -> lazy_val +val lookup_named_ctxt : variable -> named_context_val -> Context.Named.Declaration.t val evaluable_named : variable -> env -> bool val named_type : variable -> env -> types val named_body : variable -> env -> constr option @@ -112,6 +159,8 @@ val named_body : variable -> env -> constr option val fold_named_context : (env -> Context.Named.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a +val set_universes : env -> UGraph.t -> env + (** Recurrence on [named_context] starting from younger decl *) val fold_named_context_reverse : ('a -> Context.Named.Declaration.t -> 'a) -> init:'a -> env -> 'a @@ -129,8 +178,9 @@ val pop_rel_context : int -> env -> env {6 Add entries to global environment } *) val add_constant : Constant.t -> constant_body -> env -> env -val add_constant_key : Constant.t -> constant_body -> Pre_env.link_info -> +val add_constant_key : Constant.t -> 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 *) @@ -172,7 +222,8 @@ val lookup_projection : Names.Projection.t -> env -> projection_body val is_projection : Constant.t -> env -> bool (** {5 Inductive types } *) -val add_mind_key : MutInd.t -> Pre_env.mind_key -> env -> env +val lookup_mind_key : MutInd.t -> env -> mind_key +val add_mind_key : MutInd.t -> mind_key -> env -> env val add_mind : MutInd.t -> mutual_inductive_body -> env -> env (** Looks up in the context of global inductive names @@ -251,10 +302,6 @@ type 'types punsafe_type_judgment = { type unsafe_type_judgment = types punsafe_type_judgment -(** {6 Compilation of global declaration } *) - -val compile_constant_body : env -> constant_universes -> constant_def -> Cemitcodes.body_code option - exception Hyp_not_found (** [apply_to_hyp sign id f] split [sign] into [tail::(id,_,_)::head] and @@ -264,7 +311,7 @@ val apply_to_hyp : named_context_val -> variable -> (Context.Named.t -> Context.Named.Declaration.t -> Context.Named.t -> Context.Named.Declaration.t) -> named_context_val -val remove_hyps : Id.Set.t -> (Context.Named.Declaration.t -> Context.Named.Declaration.t) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val +val remove_hyps : Id.Set.t -> (Context.Named.Declaration.t -> Context.Named.Declaration.t) -> (lazy_val -> lazy_val) -> named_context_val -> named_context_val @@ -278,4 +325,4 @@ val registered : env -> field -> bool val register : env -> field -> Retroknowledge.entry -> env (** Native compiler *) -val no_link_info : Pre_env.link_info +val no_link_info : link_info diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 5d270125a..50713b957 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -22,15 +22,17 @@ CPrimitives Declareops Retroknowledge Conv_oracle -Pre_env +Environ +CClosure +Reduction Clambda Nativelambda Cbytegen Nativecode Nativelib -Environ -CClosure -Reduction +Csymtable +Vm +Vconv Nativeconv Type_errors Modops @@ -43,6 +45,3 @@ Subtyping Mod_typing Nativelibrary Safe_typing -Csymtable -Vm -Vconv diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 1baab7c98..d63dc057b 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -120,7 +120,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = const_body = def; const_universes = univs ; const_body_code = Option.map Cemitcodes.from_val - (compile_constant_body env' cb.const_universes def) } + (Cbytegen.compile_constant_body ~fail_on_error:false env' cb.const_universes def) } in before@(lab,SFBconst(cb'))::after, c', ctx' else diff --git a/kernel/modops.mli b/kernel/modops.mli index cb41a5123..ac76d28cf 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -52,7 +52,7 @@ val add_module : module_body -> env -> env (** same as add_module, but for a module whose native code has been linked by the native compiler. The linking information is updated. *) -val add_linked_module : module_body -> Pre_env.link_info -> env -> env +val add_linked_module : module_body -> link_info -> env -> env (** same, for a module type *) val add_module_type : ModPath.t -> module_type_body -> env -> env diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index c82d982b4..0cd0ad46c 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -16,7 +16,7 @@ open Util open Nativevalues open Nativeinstr open Nativelambda -open Pre_env +open Environ [@@@ocaml.warning "-32-37"] @@ -1837,7 +1837,7 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = and compile_rel env sigma univ auxdefs n = let open Context.Rel.Declaration in - let decl = Pre_env.lookup_rel n env in + let decl = lookup_rel n env in let n = List.length env.env_rel_context.env_rel_ctx - n in match decl with | LocalDef (_,t,_) -> diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 4b23cc5f8..42f2cbc2e 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -10,7 +10,7 @@ open Names open Constr open Declarations -open Pre_env +open Environ open Nativelambda (** This file defines the mllambda code generation phase of the native diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index c71f746be..c07025660 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -136,9 +136,8 @@ and conv_fix env lvl t1 f1 t2 f2 cu = aux 0 cu let native_conv_gen pb sigma env univs t1 t2 = - let penv = Environ.pre_env env in let ml_filename, prefix = get_ml_filename () in - let code, upds = mk_conv_code penv sigma prefix t1 t2 in + let code, upds = mk_conv_code env sigma prefix t1 t2 in match compile ml_filename code ~profile:false with | (true, fn) -> begin @@ -163,7 +162,7 @@ let warn_no_native_compiler = let native_conv cv_pb sigma env t1 t2 = if not Coq_config.native_compiler then begin warn_no_native_compiler (); - vm_conv cv_pb env t1 t2 + Vconv.vm_conv cv_pb env t1 t2 end else let univs = Environ.universes env in diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index 9c17cc2b5..c319be32d 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -37,7 +37,7 @@ and lambda = (* annotations, term being matched, accu, branches *) | Lif of lambda * lambda * lambda | Lfix of (int array * int) * fix_decl - | Lcofix of int * fix_decl + | Lcofix of int * fix_decl (* must be in eta-expanded form *) | Lmakeblock of prefix * pconstructor * int * lambda array (* prefix, constructor name, constructor tag, arguments *) (* A fully applied constructor *) @@ -50,6 +50,10 @@ and lambda = | Llazy | Lforce +(* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation +to be correct. Otherwise, memoization of previous evaluations will be applied +again to extra arguments (see #7333). *) + and lam_branches = (constructor * Name.t array * lambda) array and fix_decl = Name.t array * lambda array * lambda array diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 12cd5fe83..8b61ed0c5 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -12,7 +12,7 @@ open Names open Esubst open Constr open Declarations -open Pre_env +open Environ open Nativevalues open Nativeinstr @@ -570,6 +570,7 @@ let rec lambda_of_constr env sigma c = Lfix(rec_init, (names, ltypes, lbodies)) | CoFix(init,(names,type_bodies,rec_bodies)) -> + let rec_bodies = Array.map2 (Reduction.eta_expand !global_env) rec_bodies type_bodies in let ltypes = lambda_of_args env sigma 0 type_bodies in Renv.push_rels env names; let lbodies = lambda_of_args env sigma 0 rec_bodies in diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 9a1e19b3c..26bfeb7e0 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -9,7 +9,7 @@ (************************************************************************) open Names open Constr -open Pre_env +open Environ open Nativeinstr (** This file defines the lambda code generation phase of the native compiler *) diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index c69cf722b..8bff43632 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -10,7 +10,6 @@ open Names open Declarations -open Environ open Mod_subst open Modops open Nativecode @@ -32,7 +31,7 @@ and translate_field prefix mp env acc (l,x) = (if !Flags.debug then let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in Feedback.msg_debug (Pp.str msg)); - compile_constant_field (pre_env env) prefix con acc cb + compile_constant_field env prefix con acc cb | SFBmind mb -> (if !Flags.debug then let id = mb.mind_packets.(0).mind_typename in diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml deleted file mode 100644 index 8ebe48e20..000000000 --- a/kernel/pre_env.ml +++ /dev/null @@ -1,213 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <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 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(* Created by Benjamin Grégoire out of environ.ml for better - modularity in the design of the bytecode virtual evaluation - machine, Dec 2005 *) -(* Bug fix by Jean-Marc Notin *) - -(* This file defines the type of kernel environments *) - -open Util -open Names -open Declarations - -module NamedDecl = Context.Named.Declaration - -(* The type of environments. *) - -(* The key attached to each constant is used by the VM to retrieve previous *) -(* evaluations of the constant. It is essentially an index in the symbols table *) -(* used by the VM. *) -type key = int CEphemeron.key option ref - -(** Linking information for the native compiler. *) - -type link_info = - | Linked of string - | LinkedInteractive of string - | NotLinked - -type constant_key = constant_body * (link_info ref * key) - -type mind_key = mutual_inductive_body * link_info ref - -type globals = { - env_constants : constant_key Cmap_env.t; - env_inductives : mind_key Mindmap_env.t; - env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t} - -type stratification = { - env_universes : UGraph.t; - env_engagement : engagement -} - -type val_kind = - | VKvalue of (Vmvalues.values * Id.Set.t) CEphemeron.key - | VKnone - -type lazy_val = val_kind ref - -let force_lazy_val vk = match !vk with -| VKnone -> None -| VKvalue v -> try Some (CEphemeron.get v) with CEphemeron.InvalidKey -> None - -let dummy_lazy_val () = ref VKnone -let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key) - -type named_context_val = { - env_named_ctx : Context.Named.t; - env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; -} - -type rel_context_val = { - env_rel_ctx : Context.Rel.t; - env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t; -} - -type env = { - env_globals : globals; (* globals = constants + inductive types + modules + module-types *) - env_named_context : named_context_val; (* section variables *) - env_rel_context : rel_context_val; - env_nb_rel : int; - env_stratification : stratification; - env_typing_flags : typing_flags; - retroknowledge : Retroknowledge.retroknowledge; - indirect_pterms : Opaqueproof.opaquetab; -} - -let empty_named_context_val = { - env_named_ctx = []; - env_named_map = Id.Map.empty; -} - -let empty_rel_context_val = { - env_rel_ctx = []; - env_rel_map = Range.empty; -} - -let empty_env = { - env_globals = { - env_constants = Cmap_env.empty; - env_inductives = Mindmap_env.empty; - env_modules = MPmap.empty; - env_modtypes = MPmap.empty}; - env_named_context = empty_named_context_val; - env_rel_context = empty_rel_context_val; - env_nb_rel = 0; - env_stratification = { - env_universes = UGraph.initial_universes; - env_engagement = PredicativeSet }; - env_typing_flags = Declareops.safe_flags Conv_oracle.empty; - retroknowledge = Retroknowledge.initial_retroknowledge; - indirect_pterms = Opaqueproof.empty_opaquetab } - - -(* Rel context *) - -let nb_rel env = env.env_nb_rel - -let push_rel_context_val d ctx = { - env_rel_ctx = Context.Rel.add d ctx.env_rel_ctx; - env_rel_map = Range.cons (d, ref VKnone) ctx.env_rel_map; -} - -let match_rel_context_val ctx = match ctx.env_rel_ctx with -| [] -> None -| decl :: rem -> - let (_, lval) = Range.hd ctx.env_rel_map in - let ctx = { env_rel_ctx = rem; env_rel_map = Range.tl ctx.env_rel_map } in - Some (decl, lval, ctx) - -let push_rel d env = - { env with - env_rel_context = push_rel_context_val d env.env_rel_context; - env_nb_rel = env.env_nb_rel + 1 } - -let lookup_rel n env = - try fst (Range.get env.env_rel_context.env_rel_map (n - 1)) - with Invalid_argument _ -> raise Not_found - -let lookup_rel_val n env = - try snd (Range.get env.env_rel_context.env_rel_map (n - 1)) - with Invalid_argument _ -> raise Not_found - -let rel_skipn n ctx = { - env_rel_ctx = Util.List.skipn n ctx.env_rel_ctx; - env_rel_map = Range.skipn n ctx.env_rel_map; -} - -let env_of_rel n env = - { env with - env_rel_context = rel_skipn n env.env_rel_context; - env_nb_rel = env.env_nb_rel - n - } - -(* Named context *) - -let push_named_context_val_val d rval ctxt = -(* assert (not (Id.Map.mem (NamedDecl.get_id d) ctxt.env_named_map)); *) - { - env_named_ctx = Context.Named.add d ctxt.env_named_ctx; - env_named_map = Id.Map.add (NamedDecl.get_id d) (d, rval) ctxt.env_named_map; - } - -let push_named_context_val d ctxt = - push_named_context_val_val d (ref VKnone) ctxt - -let match_named_context_val c = match c.env_named_ctx with -| [] -> None -| decl :: ctx -> - let (_, v) = Id.Map.find (NamedDecl.get_id decl) c.env_named_map in - let map = Id.Map.remove (NamedDecl.get_id decl) c.env_named_map in - let cval = { env_named_ctx = ctx; env_named_map = map } in - Some (decl, v, cval) - -let map_named_val f ctxt = - let open Context.Named.Declaration in - let fold accu d = - let d' = map_constr f d in - let accu = - if d == d' then accu - else Id.Map.modify (get_id d) (fun _ (_, v) -> (d', v)) accu - in - (accu, d') - in - let map, ctx = List.fold_left_map fold ctxt.env_named_map ctxt.env_named_ctx in - if map == ctxt.env_named_map then ctxt - else { env_named_ctx = ctx; env_named_map = map } - -let push_named d env = - {env with env_named_context = push_named_context_val d env.env_named_context} - -let lookup_named id env = - fst (Id.Map.find id env.env_named_context.env_named_map) - -let lookup_named_val id env = - snd(Id.Map.find id env.env_named_context.env_named_map) - -(* Warning all the names should be different *) -let env_of_named id env = env - -(* Global constants *) - -let lookup_constant_key kn env = - Cmap_env.find kn env.env_globals.env_constants - -let lookup_constant kn env = - fst (Cmap_env.find kn env.env_globals.env_constants) - -(* Mutual Inductives *) -let lookup_mind kn env = - fst (Mindmap_env.find kn env.env_globals.env_inductives) - -let lookup_mind_key kn env = - Mindmap_env.find kn env.env_globals.env_inductives diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli deleted file mode 100644 index b05074814..000000000 --- a/kernel/pre_env.mli +++ /dev/null @@ -1,108 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <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 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names -open Constr -open Declarations - -(** The type of environments. *) - -type link_info = - | Linked of string - | LinkedInteractive of string - | NotLinked - -type key = int CEphemeron.key option ref - -type constant_key = constant_body * (link_info ref * key) - -type mind_key = mutual_inductive_body * link_info ref - -type globals = { - env_constants : constant_key Cmap_env.t; - env_inductives : mind_key Mindmap_env.t; - env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t} - -type stratification = { - env_universes : UGraph.t; - env_engagement : engagement -} - -type lazy_val - -val force_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) option -val dummy_lazy_val : unit -> lazy_val -val build_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) -> unit - -type named_context_val = private { - env_named_ctx : Context.Named.t; - env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; -} - -type rel_context_val = private { - env_rel_ctx : Context.Rel.t; - env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t; -} - -type env = { - env_globals : globals; - env_named_context : named_context_val; - env_rel_context : rel_context_val; - env_nb_rel : int; - env_stratification : stratification; - env_typing_flags : typing_flags; - retroknowledge : Retroknowledge.retroknowledge; - indirect_pterms : Opaqueproof.opaquetab; -} - -val empty_named_context_val : named_context_val - -val empty_env : env - -(** Rel context *) - -val empty_rel_context_val : rel_context_val -val push_rel_context_val : - Context.Rel.Declaration.t -> rel_context_val -> rel_context_val -val match_rel_context_val : - rel_context_val -> (Context.Rel.Declaration.t * lazy_val * rel_context_val) option - -val nb_rel : env -> int -val push_rel : Context.Rel.Declaration.t -> env -> env -val lookup_rel : int -> env -> Context.Rel.Declaration.t -val lookup_rel_val : int -> env -> lazy_val -val env_of_rel : int -> env -> env - -(** Named context *) - -val push_named_context_val : - Context.Named.Declaration.t -> named_context_val -> named_context_val -val push_named_context_val_val : - Context.Named.Declaration.t -> lazy_val -> named_context_val -> named_context_val -val match_named_context_val : - named_context_val -> (Context.Named.Declaration.t * lazy_val * named_context_val) option -val map_named_val : - (constr -> constr) -> named_context_val -> named_context_val - -val push_named : Context.Named.Declaration.t -> env -> env -val lookup_named : Id.t -> env -> Context.Named.Declaration.t -val lookup_named_val : Id.t -> env -> lazy_val -val env_of_named : Id.t -> env -> env - -(** Global constants *) - - -val lookup_constant_key : Constant.t -> env -> constant_key -val lookup_constant : Constant.t -> env -> constant_body - -(** Mutual Inductives *) -val lookup_mind_key : MutInd.t -> env -> mind_key -val lookup_mind : MutInd.t -> env -> mutual_inductive_body diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 38106fbf6..8ca596d48 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -789,24 +789,6 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta env univs t1 t2 = infer_conv_universes CUMUL l2r evars ts env univs t1 t2 -(* This reference avoids always having to link C code with the kernel *) -let vm_conv = ref (fun cv_pb env -> - gen_conv cv_pb env ~evars:((fun _->None), universes env)) - -let warn_bytecode_compiler_failed = - let open Pp in - CWarnings.create ~name:"bytecode-compiler-failed" ~category:"bytecode-compiler" - (fun () -> strbrk "Bytecode compiler failed, " ++ - strbrk "falling back to standard conversion") - -let set_vm_conv (f:conv_pb -> types kernel_conversion_function) = vm_conv := f -let vm_conv cv_pb env t1 t2 = - try - !vm_conv cv_pb env t1 t2 - with Not_found | Invalid_argument _ -> - warn_bytecode_compiler_failed (); - gen_conv cv_pb env t1 t2 - let default_conv cv_pb ?(l2r=false) env t1 t2 = gen_conv cv_pb env t1 t2 @@ -880,6 +862,17 @@ let dest_prod env = in decrec env Context.Rel.empty +let dest_lam env = + let rec decrec env m c = + let t = whd_all env c in + match kind t with + | Lambda (n,a,c0) -> + let d = LocalAssum (n,a) in + decrec (push_rel d env) (Context.Rel.add d m) c0 + | _ -> m,t + in + decrec env Context.Rel.empty + (* The same but preserving lets in the context, not internal ones. *) let dest_prod_assum env = let rec prodec_rec env l ty = @@ -925,3 +918,12 @@ let is_arity env c = let _ = dest_arity env c in true with NotArity -> false + +let eta_expand env t ty = + let ctxt, codom = dest_prod env ty in + let ctxt',t = dest_lam env t in + let d = Context.Rel.nhyps ctxt - Context.Rel.nhyps ctxt' in + let eta_args = List.rev_map mkRel (List.interval 1 d) in + let t = Term.applistc (Vars.lift d t) eta_args in + let t = Term.it_mkLambda_or_LetIn t (List.firstn d ctxt) in + Term.it_mkLambda_or_LetIn t ctxt' diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 14e4270b7..e53ab6aef 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -87,10 +87,6 @@ val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) -> Names.transparent_state -> (constr,'a) generic_conversion_function -(** option for conversion *) -val set_vm_conv : (conv_pb -> types kernel_conversion_function) -> unit -val vm_conv : conv_pb -> types kernel_conversion_function - val default_conv : conv_pb -> ?l2r:bool -> types kernel_conversion_function val default_conv_leq : ?l2r:bool -> types kernel_conversion_function @@ -122,6 +118,7 @@ val betazeta_appvect : int -> constr -> constr array -> constr val dest_prod : env -> types -> Context.Rel.t * types val dest_prod_assum : env -> types -> Context.Rel.t * types +val dest_lam : env -> types -> Context.Rel.t * constr val dest_lam_assum : env -> types -> Context.Rel.t * types exception NotArity @@ -129,4 +126,4 @@ exception NotArity val dest_arity : env -> types -> Term.arity (* raises NotArity if not an arity *) val is_arity : env -> types -> bool -val warn_bytecode_compiler_failed : ?loc:Loc.t -> unit -> unit +val eta_expand : env -> constr -> types -> constr diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 0334e7a9e..281c37b85 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -134,7 +134,7 @@ val get_native_before_match_info : retroknowledge -> entry -> Nativeinstr.lambda -> Nativeinstr.lambda -(** the following functions are solely used in Pre_env and Environ to implement +(** the following functions are solely used in Environ and Safe_typing to implement the functions register and unregister (and mem) of Environ *) val add_field : retroknowledge -> field -> entry -> retroknowledge val mem : retroknowledge -> field -> bool diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index de2a890fb..12c82e20d 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -59,6 +59,7 @@ etc. *) +open CErrors open Util open Names open Declarations @@ -914,16 +915,12 @@ let register field value by_clause senv = but it is meant to become a replacement for environ.register *) let register_inline kn senv = let open Environ in - let open Pre_env in if not (evaluable_constant kn senv.env) then CErrors.user_err Pp.(str "Register inline: an evaluable constant is expected"); - let env = pre_env senv.env in + let env = senv.env in let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in let cb = {cb with const_inline_code = true} in - let new_constants = Cmap_env.add kn (cb,r) env.env_globals.env_constants in - let new_globals = { env.env_globals with env_constants = new_constants } in - let env = { env with env_globals = new_globals } in - { senv with env = env_of_pre_env env } + let env = add_constant kn cb env in { senv with env} let add_constraints c = add_constraints @@ -953,3 +950,125 @@ Would this be correct with respect to undo's and stuff ? let set_strategy e k l = { e with env = (Environ.set_oracle e.env (Conv_oracle.set_strategy (Environ.oracle e.env) k l)) } + +(** Register retroknowledge hooks *) + +open Retroknowledge + +(* the Environ.register function synchronizes the proactive and reactive + retroknowledge. *) +let dispatch = + + (* subfunction used for static decompilation of int31 (after a vm_compute, + see pretyping/vnorm.ml for more information) *) + let constr_of_int31 = + let nth_digit_plus_one i n = (* calculates the nth (starting with 0) + digit of i and adds 1 to it + (nth_digit_plus_one 1 3 = 2) *) + if Int.equal (i land (1 lsl n)) 0 then + 1 + else + 2 + in + fun ind -> fun digit_ind -> fun tag -> + let array_of_int i = + Array.init 31 (fun n -> Constr.mkConstruct + (digit_ind, nth_digit_plus_one i (30-n))) + in + (* We check that no bit above 31 is set to one. This assertion used to + fail in the VM, and led to conversion tests failing at Qed. *) + assert (Int.equal (tag lsr 31) 0); + Constr.mkApp(Constr.mkConstruct(ind, 1), array_of_int tag) + in + + (* subfunction which dispatches the compiling information of an + int31 operation which has a specific vm instruction (associates + it to the name of the coq definition in the reactive retroknowledge) *) + let int31_op n op prim kn = + { empty_reactive_info with + vm_compiling = Some (Clambda.compile_prim n op kn); + native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn)); + } + in + +fun rk value field -> + (* subfunction which shortens the (very common) dispatch of operations *) + let int31_op_from_const n op prim = + match Constr.kind value with + | Constr.Const kn -> int31_op n op prim kn + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant.") + in + let int31_binop_from_const op prim = int31_op_from_const 2 op prim in + let int31_unop_from_const op prim = int31_op_from_const 1 op prim in + match field with + | KInt31 (grp, Int31Type) -> + let int31bit = + (* invariant : the type of bits is registered, otherwise the function + would raise Not_found. The invariant is enforced in safe_typing.ml *) + match field with + | KInt31 (grp, Int31Type) -> Retroknowledge.find rk (KInt31 (grp,Int31Bits)) + | _ -> anomaly ~label:"Environ.register" + (Pp.str "add_int31_decompilation_from_type called with an abnormal field.") + in + let i31bit_type = + match Constr.kind int31bit with + | Constr.Ind (i31bit_type,_) -> i31bit_type + | _ -> anomaly ~label:"Environ.register" + (Pp.str "Int31Bits should be an inductive type.") + in + let int31_decompilation = + match Constr.kind value with + | Constr.Ind (i31t,_) -> + constr_of_int31 i31t i31bit_type + | _ -> anomaly ~label:"Environ.register" + (Pp.str "should be an inductive type.") + in + { empty_reactive_info with + vm_decompile_const = Some int31_decompilation; + vm_before_match = Some Clambda.int31_escape_before_match; + native_before_match = Some (Nativelambda.before_match_int31 i31bit_type); + } + | KInt31 (_, Int31Constructor) -> + { empty_reactive_info with + vm_constant_static = Some Clambda.compile_structured_int31; + vm_constant_dynamic = Some Clambda.dynamic_int31_compilation; + native_constant_static = Some Nativelambda.compile_static_int31; + native_constant_dynamic = Some Nativelambda.compile_dynamic_int31; + } + | KInt31 (_, Int31Plus) -> int31_binop_from_const Cbytecodes.Kaddint31 + CPrimitives.Int31add + | KInt31 (_, Int31PlusC) -> int31_binop_from_const Cbytecodes.Kaddcint31 + CPrimitives.Int31addc + | KInt31 (_, Int31PlusCarryC) -> int31_binop_from_const Cbytecodes.Kaddcarrycint31 + CPrimitives.Int31addcarryc + | KInt31 (_, Int31Minus) -> int31_binop_from_const Cbytecodes.Ksubint31 + CPrimitives.Int31sub + | KInt31 (_, Int31MinusC) -> int31_binop_from_const Cbytecodes.Ksubcint31 + CPrimitives.Int31subc + | KInt31 (_, Int31MinusCarryC) -> int31_binop_from_const + Cbytecodes.Ksubcarrycint31 CPrimitives.Int31subcarryc + | KInt31 (_, Int31Times) -> int31_binop_from_const Cbytecodes.Kmulint31 + CPrimitives.Int31mul + | KInt31 (_, Int31TimesC) -> int31_binop_from_const Cbytecodes.Kmulcint31 + CPrimitives.Int31mulc + | KInt31 (_, Int31Div21) -> int31_op_from_const 3 Cbytecodes.Kdiv21int31 + CPrimitives.Int31div21 + | KInt31 (_, Int31Diveucl) -> int31_binop_from_const Cbytecodes.Kdivint31 + CPrimitives.Int31diveucl + | KInt31 (_, Int31AddMulDiv) -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31 + CPrimitives.Int31addmuldiv + | KInt31 (_, Int31Compare) -> int31_binop_from_const Cbytecodes.Kcompareint31 + CPrimitives.Int31compare + | KInt31 (_, Int31Head0) -> int31_unop_from_const Cbytecodes.Khead0int31 + CPrimitives.Int31head0 + | KInt31 (_, Int31Tail0) -> int31_unop_from_const Cbytecodes.Ktail0int31 + CPrimitives.Int31tail0 + | KInt31 (_, Int31Lor) -> int31_binop_from_const Cbytecodes.Klorint31 + CPrimitives.Int31lor + | KInt31 (_, Int31Land) -> int31_binop_from_const Cbytecodes.Klandint31 + CPrimitives.Int31land + | KInt31 (_, Int31Lxor) -> int31_binop_from_const Cbytecodes.Klxorint31 + CPrimitives.Int31lxor + | _ -> empty_reactive_info + +let _ = Hook.set Retroknowledge.dispatch_hook dispatch diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index e621a61c7..7352c1882 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -460,7 +460,7 @@ let build_constant_declaration kn env result = let tps = let res = match result.cook_proj with - | None -> compile_constant_body env univs def + | None -> Cbytegen.compile_constant_body ~fail_on_error:false env univs def | Some pb -> (* The compilation of primitive projections is a bit tricky, because they refer to themselves (the body of p looks like fun c => @@ -480,7 +480,7 @@ let build_constant_declaration kn env result = } in let env = add_constant kn cb env in - compile_constant_body env univs def + Cbytegen.compile_constant_body ~fail_on_error:false env univs def in Option.map Cemitcodes.from_val res in { const_hyps = hyps; diff --git a/kernel/typeops.ml b/kernel/typeops.ml index be4c0e1ec..fd9cefb2c 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -221,7 +221,7 @@ let check_cast env c ct k expected_type = try match k with | VMcast -> - vm_conv CUMUL env ct expected_type + Vconv.vm_conv CUMUL env ct expected_type | DEFAULTcast -> default_conv ~l2r:false CUMUL env ct expected_type | REVERTcast -> diff --git a/kernel/vconv.ml b/kernel/vconv.ml index f11803b67..4e4168922 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -6,9 +6,6 @@ open Vm open Vmvalues open Csymtable -let val_of_constr env c = - val_of_constr (pre_env env) c - (* Test la structure des piles *) let compare_zipper z1 z2 = @@ -185,8 +182,18 @@ and conv_arguments env ?from:(from=0) k args1 args2 cu = !rcu else raise NotConvertible +let warn_bytecode_compiler_failed = + let open Pp in + CWarnings.create ~name:"bytecode-compiler-failed" ~category:"bytecode-compiler" + (fun () -> strbrk "Bytecode compiler failed, " ++ + strbrk "falling back to standard conversion") + let vm_conv_gen cv_pb env univs t1 t2 = - try + if not Coq_config.bytecode_compiler then + Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None) + full_transparent_state env univs t1 t2 + else + try let v1 = val_of_constr env t1 in let v2 = val_of_constr env t2 in fst (conv_val env cv_pb (nb_rel env) v1 v2 univs) @@ -204,5 +211,3 @@ let vm_conv cv_pb env t1 t2 = if not b then let univs = (univs, checked_universes) in let _ = vm_conv_gen cv_pb env univs t1 t2 in () - -let _ = if Coq_config.bytecode_compiler then Reduction.set_vm_conv vm_conv diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 620f6b5e8..1a3184898 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -9,7 +9,6 @@ (************************************************************************) open Constr -open Environ open Reduction (********************************************************************** @@ -19,6 +18,3 @@ val vm_conv : conv_pb -> types kernel_conversion_function (** A conversion function parametrized by a universe comparator. Used outside of the kernel. *) val vm_conv_gen : conv_pb -> (types, 'a) generic_conversion_function - -(** Precompute a VM value from a constr *) -val val_of_constr : env -> constr -> Vmvalues.values diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index fb6be430f..5463893ad 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -52,7 +52,7 @@ let instantiate_tac n c ido = match ido with ConclLocation () -> evar_list sigma (pf_concl gl) | HypLocation (id,hloc) -> - let decl = Environ.lookup_named_val id (Goal.V82.hyps sigma (sig_it gl)) in + let decl = Environ.lookup_named id (pf_env gl) in match hloc with InHyp -> (match decl with diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 85911394f..978ceed1e 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -457,13 +457,12 @@ let native_norm env sigma c ty = if not Coq_config.native_compiler then user_err Pp.(str "Native_compute reduction has been disabled at configure time.") else - let penv = Environ.pre_env env in (* Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1); Format.eprintf "Numbers of free variables (rel): %i\n" (List.length vl2); *) let ml_filename, prefix = Nativelib.get_ml_filename () in - let code, upd = mk_norm_code penv (evars_of_evar_map sigma) prefix c in + let code, upd = mk_norm_code env (evars_of_evar_map sigma) prefix c in let profile = get_profiling_enabled () in match Nativelib.compile ml_filename code ~profile:profile with | true, fn -> diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 6bd75c93d..68f9610d1 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -215,10 +215,7 @@ let judge_of_cast env sigma cj k tj = uj_type = expected_type } let enrich_env env sigma = - let penv = Environ.pre_env env in - let penv' = Pre_env.({ penv with env_stratification = - { penv.env_stratification with env_universes = Evd.universes sigma } }) in - Environ.env_of_pre_env penv' + set_universes env @@ Evd.universes sigma let check_fix env sigma pfix = let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 049c3aff5..a1ba4a6a9 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -383,7 +383,7 @@ let cbv_vm env sigma c t = (** This evar-normalizes terms beforehand *) let c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in - let v = Vconv.val_of_constr env c in + let v = Csymtable.val_of_constr env c in EConstr.of_constr (nf_val env sigma v t) let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f347798c6..65490bbbc 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -266,7 +266,7 @@ let print_namespace ns = let matches mp = match match_modulepath ns mp with | Some [] -> true | _ -> false in - let constants = (Environ.pre_env (Global.env ())).Pre_env.env_globals.Pre_env.env_constants in + let constants = (Global.env ()).Environ.env_globals.Environ.env_constants in let constants_in_namespace = Cmap_env.fold (fun c (body,_) acc -> let kn = Constant.user c in |