diff options
Diffstat (limited to 'kernel')
44 files changed, 566 insertions, 1659 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 8ac1ecc79e..a944dbb06c 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 435cf0a792..1d8861cbc0 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 } @@ -1052,7 +1051,12 @@ let norm_val info tab v = let inject c = mk_clos (subs_id 0) c -let whd_stack infos tab m stk = +let whd_stack infos tab m stk = match m.norm with +| Whnf | Norm -> + (** No need to perform [kni] nor to unlock updates because + every head subterm of [m] is [Whnf] or [Norm] *) + knh infos m stk +| Red | Cstr -> let k = kni infos tab m stk in let () = if !share then ignore (fapp_stack k) in (* to unlock Zupdates! *) k diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index e2f5a3b827..63daa4a7c3 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -239,9 +239,6 @@ val lift_fconstr_vect : int -> fconstr array -> fconstr array val mk_clos : fconstr subs -> constr -> fconstr val mk_clos_vect : fconstr subs -> constr array -> fconstr array -val mk_clos_deep : - (fconstr subs -> constr -> fconstr) -> - fconstr subs -> constr -> fconstr val kni: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack val knr: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 5ed9b6c675..599856b647 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 a771945dd2..df5b17da31 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 1c4cdcbeb4..57d3e6fc27 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/cemitcodes.ml b/kernel/cemitcodes.ml index cea09c5104..f4e6d45c23 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -13,7 +13,7 @@ (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *) open Names -open Term +open Constr open Cbytecodes open Copcodes open Mod_subst diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli index 4a3c03d85e..f42c46175c 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 0727eaeac8..b722e42008 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 @@ -707,12 +708,10 @@ let rec lambda_of_constr env c = Lcofix(init, (names, ltypes, lbodies)) | Proj (p,c) -> - let kn = Projection.constant p in - let cb = lookup_constant kn env.global_env in - let pb = Option.get cb.const_proj in + let pb = lookup_projection p env.global_env in let n = pb.proj_arg in let lc = lambda_of_constr env c in - Lproj (n,kn,lc) + Lproj (n,Projection.constant p,lc) and lambda_of_app env f args = match Constr.kind f with diff --git a/kernel/clambda.mli b/kernel/clambda.mli index 6cf46163e3..8ff10b4549 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/cooking.ml b/kernel/cooking.ml index 6f4541e956..5783453e66 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -156,7 +156,7 @@ type inline = bool type result = { cook_body : constant_def; cook_type : types; - cook_proj : projection_body option; + cook_proj : bool; cook_universes : constant_universes; cook_inline : inline; cook_context : Context.Named.t option; @@ -227,28 +227,10 @@ let cook_constant ~hcons env { from = cb; info } = hyps) hyps ~init:cb.const_hyps in let typ = abstract_constant_type (expmod cb.const_type) hyps in - let projection pb = - let c' = abstract_constant_body (expmod pb.proj_body) hyps in - let etab = abstract_constant_body (expmod (fst pb.proj_eta)) hyps in - let etat = abstract_constant_body (expmod (snd pb.proj_eta)) hyps in - let ((mind, _), _), n' = - try - let c' = share_univs cache (IndRef (pb.proj_ind,0)) Univ.Instance.empty modlist in - match kind c' with - | App (f,l) -> (destInd f, Array.length l) - | Ind ind -> ind, 0 - | _ -> assert false - with Not_found -> (((pb.proj_ind,0),Univ.Instance.empty), 0) - in - let ctx, ty' = decompose_prod_n (n' + pb.proj_npars + 1) typ in - { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg; - proj_eta = etab, etat; - proj_type = ty'; proj_body = c' } - in { cook_body = body; cook_type = typ; - cook_proj = Option.map projection cb.const_proj; + cook_proj = cb.const_proj; cook_universes = univs; cook_inline = cb.const_inline_code; cook_context = Some const_hyps; diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 7bd0ae5663..0d907f3dea 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -21,7 +21,7 @@ type inline = bool type result = { cook_body : constant_def; cook_type : types; - cook_proj : projection_body option; + cook_proj : bool; cook_universes : constant_universes; cook_inline : inline; cook_context : Context.Named.t option; diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 4f3cbf289d..9bacdb65f4 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 d32cfba36d..72c96b0b9f 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/declarations.ml b/kernel/declarations.ml index b7427d20a7..913c13173d 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -87,7 +87,7 @@ type constant_body = { const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : constant_universes; - const_proj : projection_body option; + const_proj : bool; const_inline_code : bool; const_typing_flags : typing_flags; (** The typing options which were used for diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 832d478b3e..75c0e5b4cc 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -94,14 +94,13 @@ let subst_const_body sub cb = else let body' = subst_const_def sub cb.const_body in let type' = subst_const_type sub cb.const_type in - let proj' = Option.Smart.map (subst_const_proj sub) cb.const_proj in if body' == cb.const_body && type' == cb.const_type - && proj' == cb.const_proj then cb + then cb else { const_hyps = []; const_body = body'; const_type = type'; - const_proj = proj'; + const_proj = cb.const_proj; const_body_code = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_universes = cb.const_universes; diff --git a/kernel/environ.ml b/kernel/environ.ml index 9d4063e433..fb89576dd0 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -28,26 +28,206 @@ 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_projections : projection_body 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_projections = 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 +252,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 +281,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 +347,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 +390,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 = @@ -320,18 +487,12 @@ let type_in_type_constant cst env = not (lookup_constant cst env).const_typing_flags.check_universes let lookup_projection cst env = - match (lookup_constant (Projection.constant cst) env).const_proj with - | Some pb -> pb - | None -> anomaly (Pp.str "lookup_projection: constant is not a projection.") + Cmap_env.find (Projection.constant cst) env.env_globals.env_projections let is_projection cst env = - match (lookup_constant cst env).const_proj with - | Some _ -> true - | None -> false + (lookup_constant cst env).const_proj (* Mutual Inductives *) -let lookup_mind = lookup_mind - let polymorphic_ind (mind,i) env = Declareops.inductive_is_polymorphic (lookup_mind mind env) @@ -351,11 +512,18 @@ let template_polymorphic_pind (ind,u) env = if not (Univ.Instance.is_empty u) then false else template_polymorphic_ind ind env -let add_mind_key kn mind_key env = +let add_mind_key kn (mind, _ as mind_key) env = let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in + let new_projections = match mind.mind_record with + | None | Some None -> env.env_globals.env_projections + | Some (Some (id, kns, pbs)) -> + Array.fold_left2 (fun projs kn pb -> + Cmap_env.add kn pb projs) + env.env_globals.env_projections kns pbs + in let new_globals = { env.env_globals with - env_inductives = new_inds } in + env_inductives = new_inds; env_projections = new_projections; } in { env with env_globals = new_globals } let add_mind kn mib env = @@ -468,10 +636,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 +694,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 fdd84b25b1..8928b32f1b 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -28,16 +28,61 @@ 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_projections : projection_body 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 +115,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 +149,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 +160,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 +179,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 +223,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 +303,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 +312,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 +326,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/inductive.ml b/kernel/inductive.ml index 9bed598bb7..090acdf16e 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -803,9 +803,7 @@ let rec subterm_specif renv stack t = (* We take the subterm specs of the constructor of the record *) let wf_args = (dest_subterms wf).(0) in (* We extract the tree of the projected argument *) - let kn = Projection.constant p in - let cb = lookup_constant kn renv.env in - let pb = Option.get cb.const_proj in + let pb = lookup_projection p renv.env in let n = pb.proj_arg in spec_of_tree (List.nth wf_args n) | Dead_code -> Dead_code diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 5d270125a4..50713b9579 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 1baab7c98c..d63dc057b4 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 cb41a5123a..ac76d28cf3 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/names.ml b/kernel/names.ml index 58d311dd58..54f089e607 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -760,55 +760,8 @@ let eq_ind_chk (kn1,i1) (kn2,i2) = Int.equal i1 i2 && eq_mind_chk kn1 kn2 (*******************************************************************) (** Compatibility layers *) -(** Backward compatibility for [Id] *) - -type identifier = Id.t - -let id_eq = Id.equal -let id_ord = Id.compare -let string_of_id = Id.to_string -let id_of_string = Id.of_string - -module Idset = Id.Set -module Idmap = Id.Map -module Idpred = Id.Pred - -(** Compatibility layer for [Name] *) - -let name_eq = Name.equal - -(** Compatibility layer for [DirPath] *) - -type dir_path = DirPath.t -let dir_path_ord = DirPath.compare -let dir_path_eq = DirPath.equal -let make_dirpath = DirPath.make -let repr_dirpath = DirPath.repr -let empty_dirpath = DirPath.empty -let is_empty_dirpath = DirPath.is_empty -let string_of_dirpath = DirPath.to_string -let initial_dir = DirPath.initial - -(** Compatibility layer for [MBId] *) - type mod_bound_id = MBId.t -let mod_bound_id_ord = MBId.compare -let mod_bound_id_eq = MBId.equal -let make_mbid = MBId.make -let repr_mbid = MBId.repr -let debug_string_of_mbid = MBId.debug_to_string -let string_of_mbid = MBId.to_string -let id_of_mbid = MBId.to_id - -(** Compatibility layer for [Label] *) - -type label = Id.t -let mk_label = Label.make -let string_of_label = Label.to_string -let pr_label = Label.print -let id_of_label = Label.to_id -let label_of_id = Label.of_id -let eq_label = Label.equal +let eq_constant_key = Constant.UserOrd.equal (** Compatibility layer for [ModPath] *) @@ -816,32 +769,13 @@ type module_path = ModPath.t = | MPfile of DirPath.t | MPbound of MBId.t | MPdot of module_path * Label.t -let check_bound_mp = ModPath.is_bound -let string_of_mp = ModPath.to_string -let mp_ord = ModPath.compare -let mp_eq = ModPath.equal -let initial_path = ModPath.initial - -(** Compatibility layer for [KerName] *) - -type kernel_name = KerName.t -let make_kn = KerName.make -let repr_kn = KerName.repr -let modpath = KerName.modpath -let label = KerName.label -let string_of_kn = KerName.to_string -let pr_kn = KerName.print -let kn_ord = KerName.compare (** Compatibility layer for [Constant] *) -type constant = Constant.t - +module Projection = +struct + type t = Constant.t * bool -module Projection = -struct - type t = constant * bool - let make c b = (c, b) let constant = fst @@ -906,6 +840,9 @@ module GlobRef = struct end +type global_reference = GlobRef.t +[@@ocaml.deprecated "Alias for [GlobRef.t]"] + type evaluable_global_reference = | EvalVarRef of Id.t | EvalConstRef of Constant.t @@ -915,40 +852,3 @@ let eq_egr e1 e2 = match e1, e2 with EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2 | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2 | _, _ -> false - -let constant_of_kn = Constant.make1 -let constant_of_kn_equiv = Constant.make -let make_con = Constant.make3 -let repr_con = Constant.repr3 -let canonical_con = Constant.canonical -let user_con = Constant.user -let con_label = Constant.label -let con_modpath = Constant.modpath -let eq_constant = Constant.equal -let eq_constant_key = Constant.UserOrd.equal -let con_ord = Constant.CanOrd.compare -let con_user_ord = Constant.UserOrd.compare -let string_of_con = Constant.to_string -let pr_con = Constant.print -let debug_string_of_con = Constant.debug_to_string -let debug_pr_con = Constant.debug_print -let con_with_label = Constant.change_label - -(** Compatibility layer for [MutInd] *) - -type mutual_inductive = MutInd.t -let mind_of_kn = MutInd.make1 -let mind_of_kn_equiv = MutInd.make -let make_mind = MutInd.make3 -let canonical_mind = MutInd.canonical -let user_mind = MutInd.user -let repr_mind = MutInd.repr3 -let mind_label = MutInd.label -let mind_modpath = MutInd.modpath -let eq_mind = MutInd.equal -let mind_ord = MutInd.CanOrd.compare -let mind_user_ord = MutInd.UserOrd.compare -let string_of_mind = MutInd.to_string -let pr_mind = MutInd.print -let debug_string_of_mind = MutInd.debug_to_string -let debug_pr_mind = MutInd.debug_print diff --git a/kernel/names.mli b/kernel/names.mli index 566fcd0f91..f988b559a8 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -538,116 +538,8 @@ val eq_ind_chk : inductive -> inductive -> bool (** {6 Deprecated functions. For backward compatibility.} *) -(** {5 Identifiers} *) - -type identifier = Id.t -[@@ocaml.deprecated "Alias for [Id.t]"] - -val string_of_id : Id.t -> string -[@@ocaml.deprecated "Same as [Id.to_string]."] - -val id_of_string : string -> Id.t -[@@ocaml.deprecated "Same as [Id.of_string]."] - -val id_ord : Id.t -> Id.t -> int -[@@ocaml.deprecated "Same as [Id.compare]."] - -val id_eq : Id.t -> Id.t -> bool -[@@ocaml.deprecated "Same as [Id.equal]."] - -module Idset : Set.S with type elt = Id.t and type t = Id.Set.t -[@@ocaml.deprecated "Same as [Id.Set]."] - -module Idpred : Predicate.S with type elt = Id.t and type t = Id.Pred.t -[@@ocaml.deprecated "Same as [Id.Pred]."] - -module Idmap : module type of Id.Map -[@@ocaml.deprecated "Same as [Id.Map]."] - -(** {5 Directory paths} *) - -type dir_path = DirPath.t -[@@ocaml.deprecated "Alias for [DirPath.t]."] - -val dir_path_ord : DirPath.t -> DirPath.t -> int -[@@ocaml.deprecated "Same as [DirPath.compare]."] - -val dir_path_eq : DirPath.t -> DirPath.t -> bool -[@@ocaml.deprecated "Same as [DirPath.equal]."] - -val make_dirpath : module_ident list -> DirPath.t -[@@ocaml.deprecated "Same as [DirPath.make]."] - -val repr_dirpath : DirPath.t -> module_ident list -[@@ocaml.deprecated "Same as [DirPath.repr]."] - -val empty_dirpath : DirPath.t -[@@ocaml.deprecated "Same as [DirPath.empty]."] - -val is_empty_dirpath : DirPath.t -> bool -[@@ocaml.deprecated "Same as [DirPath.is_empty]."] - -val string_of_dirpath : DirPath.t -> string -[@@ocaml.deprecated "Same as [DirPath.to_string]."] - -val initial_dir : DirPath.t -[@@ocaml.deprecated "Same as [DirPath.initial]."] - -(** {5 Labels} *) - -type label = Label.t -[@@ocaml.deprecated "Same as [Label.t]."] -(** Alias type *) - -val mk_label : string -> Label.t -[@@ocaml.deprecated "Same as [Label.make]."] - -val string_of_label : Label.t -> string -[@@ocaml.deprecated "Same as [Label.to_string]."] - -val pr_label : Label.t -> Pp.t -[@@ocaml.deprecated "Same as [Label.print]."] - -val label_of_id : Id.t -> Label.t -[@@ocaml.deprecated "Same as [Label.of_id]."] - -val id_of_label : Label.t -> Id.t -[@@ocaml.deprecated "Same as [Label.to_id]."] - -val eq_label : Label.t -> Label.t -> bool -[@@ocaml.deprecated "Same as [Label.equal]."] - -(** {5 Unique bound module names} *) - type mod_bound_id = MBId.t [@@ocaml.deprecated "Same as [MBId.t]."] - -val mod_bound_id_ord : MBId.t -> MBId.t -> int -[@@ocaml.deprecated "Same as [MBId.compare]."] - -val mod_bound_id_eq : MBId.t -> MBId.t -> bool -[@@ocaml.deprecated "Same as [MBId.equal]."] - -val make_mbid : DirPath.t -> Id.t -> MBId.t -[@@ocaml.deprecated "Same as [MBId.make]."] - -val repr_mbid : MBId.t -> int * Id.t * DirPath.t -[@@ocaml.deprecated "Same as [MBId.repr]."] - -val id_of_mbid : MBId.t -> Id.t -[@@ocaml.deprecated "Same as [MBId.to_id]."] - -val string_of_mbid : MBId.t -> string -[@@ocaml.deprecated "Same as [MBId.to_string]."] - -val debug_string_of_mbid : MBId.t -> string -[@@ocaml.deprecated "Same as [MBId.debug_to_string]."] - -(** {5 Names} *) - -val name_eq : Name.t -> Name.t -> bool -[@@ocaml.deprecated "Same as [Name.equal]."] - (** {5 Module paths} *) type module_path = ModPath.t = @@ -656,52 +548,6 @@ type module_path = ModPath.t = | MPdot of ModPath.t * Label.t [@@ocaml.deprecated "Alias type"] -val mp_ord : ModPath.t -> ModPath.t -> int -[@@ocaml.deprecated "Same as [ModPath.compare]."] - -val mp_eq : ModPath.t -> ModPath.t -> bool -[@@ocaml.deprecated "Same as [ModPath.equal]."] - -val check_bound_mp : ModPath.t -> bool -[@@ocaml.deprecated "Same as [ModPath.is_bound]."] - -val string_of_mp : ModPath.t -> string -[@@ocaml.deprecated "Same as [ModPath.to_string]."] - -val initial_path : ModPath.t -[@@ocaml.deprecated "Same as [ModPath.initial]."] - -(** {5 Kernel names} *) - -type kernel_name = KerName.t -[@@ocaml.deprecated "Alias type"] - -val make_kn : ModPath.t -> DirPath.t -> Label.t -> KerName.t -[@@ocaml.deprecated "Same as [KerName.make]."] - -val repr_kn : KerName.t -> ModPath.t * DirPath.t * Label.t -[@@ocaml.deprecated "Same as [KerName.repr]."] - -val modpath : KerName.t -> ModPath.t -[@@ocaml.deprecated "Same as [KerName.modpath]."] - -val label : KerName.t -> Label.t -[@@ocaml.deprecated "Same as [KerName.label]."] - -val string_of_kn : KerName.t -> string -[@@ocaml.deprecated "Same as [KerName.to_string]."] - -val pr_kn : KerName.t -> Pp.t -[@@ocaml.deprecated "Same as [KerName.print]."] - -val kn_ord : KerName.t -> KerName.t -> int -[@@ocaml.deprecated "Same as [KerName.compare]."] - -(** {5 Constant names} *) - -type constant = Constant.t -[@@ocaml.deprecated "Alias type"] - module Projection : sig type t @@ -749,6 +595,9 @@ module GlobRef : sig end +type global_reference = GlobRef.t +[@@ocaml.deprecated "Alias for [GlobRef.t]"] + (** Better to have it here that in Closure, since required in grammar.cma *) (* XXX: Move to a module *) type evaluable_global_reference = @@ -756,101 +605,3 @@ type evaluable_global_reference = | EvalConstRef of Constant.t val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool - -val constant_of_kn_equiv : KerName.t -> KerName.t -> Constant.t -[@@ocaml.deprecated "Same as [Constant.make]"] - -val constant_of_kn : KerName.t -> Constant.t -[@@ocaml.deprecated "Same as [Constant.make1]"] - -val make_con : ModPath.t -> DirPath.t -> Label.t -> Constant.t -[@@ocaml.deprecated "Same as [Constant.make3]"] - -val repr_con : Constant.t -> ModPath.t * DirPath.t * Label.t -[@@ocaml.deprecated "Same as [Constant.repr3]"] - -val user_con : Constant.t -> KerName.t -[@@ocaml.deprecated "Same as [Constant.user]"] - -val canonical_con : Constant.t -> KerName.t -[@@ocaml.deprecated "Same as [Constant.canonical]"] - -val con_modpath : Constant.t -> ModPath.t -[@@ocaml.deprecated "Same as [Constant.modpath]"] - -val con_label : Constant.t -> Label.t -[@@ocaml.deprecated "Same as [Constant.label]"] - -val eq_constant : Constant.t -> Constant.t -> bool -[@@ocaml.deprecated "Same as [Constant.equal]"] - -val con_ord : Constant.t -> Constant.t -> int -[@@ocaml.deprecated "Same as [Constant.CanOrd.compare]"] - -val con_user_ord : Constant.t -> Constant.t -> int -[@@ocaml.deprecated "Same as [Constant.UserOrd.compare]"] - -val con_with_label : Constant.t -> Label.t -> Constant.t -[@@ocaml.deprecated "Same as [Constant.change_label]"] - -val string_of_con : Constant.t -> string -[@@ocaml.deprecated "Same as [Constant.to_string]"] - -val pr_con : Constant.t -> Pp.t -[@@ocaml.deprecated "Same as [Constant.print]"] - -val debug_pr_con : Constant.t -> Pp.t -[@@ocaml.deprecated "Same as [Constant.debug_print]"] - -val debug_string_of_con : Constant.t -> string -[@@ocaml.deprecated "Same as [Constant.debug_to_string]"] - -(** {5 Mutual Inductive names} *) - -type mutual_inductive = MutInd.t -[@@ocaml.deprecated "Alias type"] - -val mind_of_kn : KerName.t -> MutInd.t -[@@ocaml.deprecated "Same as [MutInd.make1]"] - -val mind_of_kn_equiv : KerName.t -> KerName.t -> MutInd.t -[@@ocaml.deprecated "Same as [MutInd.make]"] - -val make_mind : ModPath.t -> DirPath.t -> Label.t -> MutInd.t -[@@ocaml.deprecated "Same as [MutInd.make3]"] - -val user_mind : MutInd.t -> KerName.t -[@@ocaml.deprecated "Same as [MutInd.user]"] - -val canonical_mind : MutInd.t -> KerName.t -[@@ocaml.deprecated "Same as [MutInd.canonical]"] - -val repr_mind : MutInd.t -> ModPath.t * DirPath.t * Label.t -[@@ocaml.deprecated "Same as [MutInd.repr3]"] - -val eq_mind : MutInd.t -> MutInd.t -> bool -[@@ocaml.deprecated "Same as [MutInd.equal]"] - -val mind_ord : MutInd.t -> MutInd.t -> int -[@@ocaml.deprecated "Same as [MutInd.CanOrd.compare]"] - -val mind_user_ord : MutInd.t -> MutInd.t -> int -[@@ocaml.deprecated "Same as [MutInd.UserOrd.compare]"] - -val mind_label : MutInd.t -> Label.t -[@@ocaml.deprecated "Same as [MutInd.label]"] - -val mind_modpath : MutInd.t -> ModPath.t -[@@ocaml.deprecated "Same as [MutInd.modpath]"] - -val string_of_mind : MutInd.t -> string -[@@ocaml.deprecated "Same as [MutInd.to_string]"] - -val pr_mind : MutInd.t -> Pp.t -[@@ocaml.deprecated "Same as [MutInd.print]"] - -val debug_pr_mind : MutInd.t -> Pp.t -[@@ocaml.deprecated "Same as [MutInd.debug_print]"] - -val debug_string_of_mind : MutInd.t -> string -[@@ocaml.deprecated "Same as [MutInd.debug_to_string]"] diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index c82d982b4b..036cd4847e 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,_) -> @@ -1859,7 +1859,7 @@ and compile_named env sigma univ auxdefs id = let compile_constant env sigma prefix ~interactive con cb = match cb.const_proj with - | None -> + | false -> let no_univs = match cb.const_universes with | Monomorphic_const _ -> true @@ -1903,7 +1903,8 @@ let compile_constant env sigma prefix ~interactive con cb = if interactive then LinkedInteractive prefix else Linked prefix end - | Some pb -> + | true -> + let pb = lookup_projection (Projection.make con false) env in let mind = pb.proj_ind in let ind = (mind,0) in let mib = lookup_mind mind env in @@ -2029,11 +2030,12 @@ let rec compile_deps env sigma prefix ~interactive init t = else let comp_stack, (mind_updates, const_updates) = match cb.const_proj, cb.const_body with - | None, Def t -> + | false, Def t -> compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t) - | Some pb, _ -> - let mind = pb.proj_ind in - compile_mind_deps env prefix ~interactive init mind + | true, _ -> + let pb = lookup_projection (Projection.make c false) env in + let mind = pb.proj_ind in + compile_mind_deps env prefix ~interactive init mind | _ -> init in let code, name = diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 4b23cc5f8b..42f2cbc2e4 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 c71f746bec..c07025660e 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 9c17cc2b5f..c319be32d7 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 12cd5fe83a..8b61ed0c5a 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 9a1e19b3cb..26bfeb7e0e 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 c69cf722bc..8bff436322 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 8ebe48e202..0000000000 --- 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 b05074814b..0000000000 --- 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 38106fbf67..f4af313867 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -648,25 +648,24 @@ let check_leq univs u u' = let check_sort_cmp_universes env pb s0 s1 univs = let open Sorts in - match (s0,s1) with + if not (type_in_type env) then + match (s0,s1) with | (Prop c1, Prop c2) when is_cumul pb -> begin match c1, c2 with - | Null, _ | _, Pos -> () (* Prop <= Set *) - | _ -> raise NotConvertible + | Null, _ | _, Pos -> () (* Prop <= Set *) + | _ -> raise NotConvertible end | (Prop c1, Prop c2) -> if c1 != c2 then raise NotConvertible | (Prop c1, Type u) -> - if not (type_in_type env) then - let u0 = univ_of_sort s0 in - (match pb with - | CUMUL -> check_leq univs u0 u - | CONV -> check_eq univs u0 u) + let u0 = univ_of_sort s0 in + (match pb with + | CUMUL -> check_leq univs u0 u + | CONV -> check_eq univs u0 u) | (Type u, Prop c) -> raise NotConvertible | (Type u1, Type u2) -> - if not (type_in_type env) then - (match pb with - | CUMUL -> check_leq univs u1 u2 - | CONV -> check_eq univs u1 u2) + (match pb with + | CUMUL -> check_leq univs u1 u2 + | CONV -> check_eq univs u1 u2) let checked_sort_cmp_universes env pb s0 s1 univs = check_sort_cmp_universes env pb s0 s1 univs; univs @@ -699,25 +698,25 @@ let infer_leq (univs, cstrs as cuniv) u u' = let infer_cmp_universes env pb s0 s1 univs = let open Sorts in - match (s0,s1) with + if type_in_type env then univs + else + match (s0,s1) with | (Prop c1, Prop c2) when is_cumul pb -> begin match c1, c2 with - | Null, _ | _, Pos -> univs (* Prop <= Set *) - | _ -> raise NotConvertible + | Null, _ | _, Pos -> univs (* Prop <= Set *) + | _ -> raise NotConvertible end | (Prop c1, Prop c2) -> if c1 == c2 then univs else raise NotConvertible | (Prop c1, Type u) -> let u0 = univ_of_sort s0 in - (match pb with - | CUMUL -> infer_leq univs u0 u - | CONV -> infer_eq univs u0 u) + (match pb with + | CUMUL -> infer_leq univs u0 u + | CONV -> infer_eq univs u0 u) | (Type u, Prop c) -> raise NotConvertible | (Type u1, Type u2) -> - if not (type_in_type env) then - (match pb with - | CUMUL -> infer_leq univs u1 u2 - | CONV -> infer_eq univs u1 u2) - else univs + (match pb with + | CUMUL -> infer_leq univs u1 u2 + | CONV -> infer_eq univs u1 u2) let infer_convert_instances ~flex u u' (univs,cstrs) = let cstrs' = @@ -789,24 +788,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 +861,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 +917,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 14e4270b7c..e53ab6aefb 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 0334e7a9e9..281c37b851 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 de2a890fb5..12c82e20de 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.ml b/kernel/term.ml index e1affb1c07..b44e038e9f 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -15,219 +15,17 @@ open Names open Vars open Constr -(**********************************************************************) -(** Redeclaration of types from module Constr *) -(**********************************************************************) - +(* Deprecated *) type contents = Sorts.contents = Pos | Null - -type sorts = Sorts.t = - | Prop of contents (** Prop and Set *) - | Type of Univ.Universe.t (** Type *) +[@@ocaml.deprecated "Alias for Sorts.contents"] type sorts_family = Sorts.family = InProp | InSet | InType +[@@ocaml.deprecated "Alias for Sorts.family"] -type constr = Constr.t -(** Alias types, for compatibility. *) - -type types = Constr.t -(** Same as [constr], for documentation purposes. *) - -type existential_key = Evar.t -type existential = Constr.existential - -type metavariable = Constr.metavariable - -type case_style = Constr.case_style = - LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle - -type case_printing = Constr.case_printing = - { ind_tags : bool list; cstr_tags : bool list array; style : case_style } - -type case_info = Constr.case_info = - { ci_ind : inductive; - ci_npar : int; - ci_cstr_ndecls : int array; - ci_cstr_nargs : int array; - ci_pp_info : case_printing - } - -type cast_kind = Constr.cast_kind = - VMcast | NATIVEcast | DEFAULTcast | REVERTcast - -(********************************************************************) -(* Constructions as implemented *) -(********************************************************************) - -type rec_declaration = Constr.rec_declaration -type fixpoint = Constr.fixpoint -type cofixpoint = Constr.cofixpoint -type 'constr pexistential = 'constr Constr.pexistential -type ('constr, 'types) prec_declaration = - ('constr, 'types) Constr.prec_declaration -type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint -type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint -type 'a puniverses = 'a Univ.puniverses - -(** Simply type aliases *) -type pconstant = Constant.t puniverses -type pinductive = inductive puniverses -type pconstructor = constructor puniverses - -type ('constr, 'types, 'sort, 'univs) kind_of_term = - ('constr, 'types, 'sort, 'univs) Constr.kind_of_term = - | Rel of int - | Var of Id.t - | Meta of metavariable - | Evar of 'constr pexistential - | Sort of 'sort - | Cast of 'constr * cast_kind * 'types - | Prod of Name.t * 'types * 'types - | Lambda of Name.t * 'types * 'constr - | LetIn of Name.t * 'constr * 'types * 'constr - | App of 'constr * 'constr array - | Const of (Constant.t * 'univs) - | Ind of (inductive * 'univs) - | Construct of (constructor * 'univs) - | Case of case_info * 'constr * 'constr * 'constr array - | Fix of ('constr, 'types) pfixpoint - | CoFix of ('constr, 'types) pcofixpoint - | Proj of Projection.t * 'constr - -type values = Vmvalues.values - -(**********************************************************************) -(** Redeclaration of functions from module Constr *) -(**********************************************************************) - -let set_sort = Sorts.set -let prop_sort = Sorts.prop -let type1_sort = Sorts.type1 -let sorts_ord = Sorts.compare -let is_prop_sort = Sorts.is_prop -let family_of_sort = Sorts.family -let univ_of_sort = Sorts.univ_of_sort -let sort_of_univ = Sorts.sort_of_univ - -(** {6 Term constructors. } *) - -let mkRel = Constr.mkRel -let mkVar = Constr.mkVar -let mkMeta = Constr.mkMeta -let mkEvar = Constr.mkEvar -let mkSort = Constr.mkSort -let mkProp = Constr.mkProp -let mkSet = Constr.mkSet -let mkType = Constr.mkType -let mkCast = Constr.mkCast -let mkProd = Constr.mkProd -let mkLambda = Constr.mkLambda -let mkLetIn = Constr.mkLetIn -let mkApp = Constr.mkApp -let mkConst = Constr.mkConst -let mkProj = Constr.mkProj -let mkInd = Constr.mkInd -let mkConstruct = Constr.mkConstruct -let mkConstU = Constr.mkConstU -let mkIndU = Constr.mkIndU -let mkConstructU = Constr.mkConstructU -let mkConstructUi = Constr.mkConstructUi -let mkCase = Constr.mkCase -let mkFix = Constr.mkFix -let mkCoFix = Constr.mkCoFix - -(**********************************************************************) -(** Aliases of functions from module Constr *) -(**********************************************************************) - -let eq_constr = Constr.equal -let eq_constr_univs = Constr.eq_constr_univs -let leq_constr_univs = Constr.leq_constr_univs -let eq_constr_nounivs = Constr.eq_constr_nounivs - -let kind_of_term = Constr.kind -let compare = Constr.compare -let constr_ord = compare -let fold_constr = Constr.fold -let map_puniverses = Constr.map_puniverses -let map_constr = Constr.map -let map_constr_with_binders = Constr.map_with_binders -let iter_constr = Constr.iter -let iter_constr_with_binders = Constr.iter_with_binders -let compare_constr = Constr.compare_head -let hash_constr = Constr.hash -let hcons_sorts = Sorts.hcons -let hcons_constr = Constr.hcons -let hcons_types = Constr.hcons - -(**********************************************************************) -(** HERE BEGINS THE INTERESTING STUFF *) -(**********************************************************************) - -(**********************************************************************) -(* Non primitive term destructors *) -(**********************************************************************) - -exception DestKO = DestKO -(* Destructs a de Bruijn index *) -let destRel = destRel -let destMeta = destRel -let isMeta = isMeta -let destVar = destVar -let isSort = isSort -let destSort = destSort -let isprop = isprop -let is_Prop = is_Prop -let is_Set = is_Set -let is_Type = is_Type -let is_small = is_small -let iskind = iskind -let isEvar = isEvar -let isEvar_or_Meta = isEvar_or_Meta -let destCast = destCast -let isCast = isCast -let isRel = isRel -let isRelN = isRelN -let isVar = isVar -let isVarId = isVarId -let isInd = isInd -let destProd = destProd -let isProd = isProd -let destLambda = destLambda -let isLambda = isLambda -let destLetIn = destLetIn -let isLetIn = isLetIn -let destApp = destApp -let destApplication = destApp -let isApp = isApp -let destConst = destConst -let isConst = isConst -let destEvar = destEvar -let destInd = destInd -let destConstruct = destConstruct -let isConstruct = isConstruct -let destCase = destCase -let isCase = isCase -let isProj = isProj -let destProj = destProj -let destFix = destFix -let isFix = isFix -let destCoFix = destCoFix -let isCoFix = isCoFix - -(******************************************************************) -(* Flattening and unflattening of embedded applications and casts *) -(******************************************************************) - -let decompose_app c = - match kind_of_term c with - | App (f,cl) -> (f, Array.to_list cl) - | _ -> (c,[]) - -let decompose_appvect c = - match kind_of_term c with - | App (f,cl) -> (f, cl) - | _ -> (c,[||]) +type sorts = Sorts.t = + | Prop of Sorts.contents (** Prop and Set *) + | Type of Univ.Universe.t (** Type *) +[@@ocaml.deprecated "Alias for Sorts.t"] (****************************************************************************) (* Functions for dealing with constr terms *) @@ -321,7 +119,7 @@ let rec to_lambda n prod = if Int.equal n 0 then prod else - match kind_of_term prod with + match kind prod with | Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda (n-1) bd) | Cast (c,_,_) -> to_lambda n c | _ -> user_err ~hdr:"to_lambda" (mt ()) @@ -330,7 +128,7 @@ let rec to_prod n lam = if Int.equal n 0 then lam else - match kind_of_term lam with + match kind lam with | Lambda (na,ty,bd) -> mkProd (na,ty,to_prod (n-1) bd) | Cast (c,_,_) -> to_prod n c | _ -> user_err ~hdr:"to_prod" (mt ()) @@ -342,7 +140,7 @@ let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c) let lambda_applist c l = let rec app subst c l = - match kind_of_term c, l with + match kind c, l with | Lambda(_,_,c), arg::l -> app (arg::subst) c l | _, [] -> substl subst c | _ -> anomaly (Pp.str "Not enough lambda's.") in @@ -355,7 +153,7 @@ let lambda_applist_assum n c l = if Int.equal n 0 then if l == [] then substl subst t else anomaly (Pp.str "Too many arguments.") - else match kind_of_term t, l with + else match kind t, l with | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l | _, [] -> anomaly (Pp.str "Not enough arguments.") @@ -367,7 +165,7 @@ let lambda_appvect_assum n c v = lambda_applist_assum n c (Array.to_list v) (* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *) let prod_applist c l = let rec app subst c l = - match kind_of_term c, l with + match kind c, l with | Prod(_,_,c), arg::l -> app (arg::subst) c l | _, [] -> substl subst c | _ -> anomaly (Pp.str "Not enough prod's.") in @@ -381,7 +179,7 @@ let prod_applist_assum n c l = if Int.equal n 0 then if l == [] then substl subst t else anomaly (Pp.str "Too many arguments.") - else match kind_of_term t, l with + else match kind t, l with | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l | _, [] -> anomaly (Pp.str "Not enough arguments.") @@ -397,7 +195,7 @@ let prod_appvect_assum n c v = prod_applist_assum n c (Array.to_list v) (* Transforms a product term (x1:T1)..(xn:Tn)T into the pair ([(xn,Tn);...;(x1,T1)],T), where T is not a product *) let decompose_prod = - let rec prodec_rec l c = match kind_of_term c with + let rec prodec_rec l c = match kind c with | Prod (x,t,c) -> prodec_rec ((x,t)::l) c | Cast (c,_,_) -> prodec_rec l c | _ -> l,c @@ -407,7 +205,7 @@ let decompose_prod = (* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *) let decompose_lam = - let rec lamdec_rec l c = match kind_of_term c with + let rec lamdec_rec l c = match kind c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c | Cast (c,_,_) -> lamdec_rec l c | _ -> l,c @@ -420,7 +218,7 @@ let decompose_prod_n n = if n < 0 then user_err (str "decompose_prod_n: integer parameter must be positive"); let rec prodec_rec l n c = if Int.equal n 0 then l,c - else match kind_of_term c with + else match kind c with | Prod (x,t,c) -> prodec_rec ((x,t)::l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c | _ -> user_err (str "decompose_prod_n: not enough products") @@ -433,7 +231,7 @@ let decompose_lam_n n = if n < 0 then user_err (str "decompose_lam_n: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c - else match kind_of_term c with + else match kind c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c | _ -> user_err (str "decompose_lam_n: not enough abstractions") @@ -445,7 +243,7 @@ let decompose_lam_n n = let decompose_prod_assum = let open Context.Rel.Declaration in let rec prodec_rec l c = - match kind_of_term c with + match kind c with | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) c | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c | Cast (c,_,_) -> prodec_rec l c @@ -458,7 +256,7 @@ let decompose_prod_assum = let decompose_lam_assum = let rec lamdec_rec l c = let open Context.Rel.Declaration in - match kind_of_term c with + match kind c with | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c | Cast (c,_,_) -> lamdec_rec l c @@ -477,7 +275,7 @@ let decompose_prod_n_assum n = if Int.equal n 0 then l,c else let open Context.Rel.Declaration in - match kind_of_term c with + match kind c with | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c @@ -498,7 +296,7 @@ let decompose_lam_n_assum n = if Int.equal n 0 then l,c else let open Context.Rel.Declaration in - match kind_of_term c with + match kind c with | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c | Cast (c,_,_) -> lamdec_rec l n c @@ -514,7 +312,7 @@ let decompose_lam_n_decls n = if Int.equal n 0 then l,c else let open Context.Rel.Declaration in - match kind_of_term c with + match kind c with | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c @@ -541,12 +339,12 @@ let strip_lam_n n t = snd (decompose_lam_n n t) Such a term can canonically be seen as the pair of a context of types and of a sort *) -type arity = Context.Rel.t * sorts +type arity = Context.Rel.t * Sorts.t let destArity = let open Context.Rel.Declaration in let rec prodec_rec l c = - match kind_of_term c with + match kind c with | Prod (x,t,c) -> prodec_rec (LocalAssum (x,t) :: l) c | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c | Cast (c,_,_) -> prodec_rec l c @@ -558,7 +356,7 @@ let destArity = let mkArity (sign,s) = it_mkProd_or_LetIn (mkSort s) sign let rec isArity c = - match kind_of_term c with + match kind c with | Prod (_,_,c) -> isArity c | LetIn (_,b,_,c) -> isArity (subst1 b c) | Cast (c,_,_) -> isArity c @@ -569,13 +367,13 @@ let rec isArity c = (* Experimental, used in Presburger contrib *) type ('constr, 'types) kind_of_type = - | SortType of sorts + | SortType of Sorts.t | CastType of 'types * 'types | ProdType of Name.t * 'types * 'types | LetInType of Name.t * 'constr * 'types * 'types | AtomicType of 'constr * 'constr array -let kind_of_type t = match kind_of_term t with +let kind_of_type t = match kind t with | Sort s -> SortType s | Cast (c,_,t) -> CastType (c, t) | Prod (na,t,c) -> ProdType (na, t, c) diff --git a/kernel/term.mli b/kernel/term.mli index ee84dcb2b0..f651d1a580 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -11,166 +11,6 @@ open Names open Constr -(** {5 Redeclaration of types from module Constr and Sorts} - - This reexports constructors of inductive types defined in module [Constr], - for compatibility purposes. Refer to this module for further info. - -*) - -exception DestKO -[@@ocaml.deprecated "Alias for [Constr.DestKO]"] - -(** {5 Simple term case analysis. } *) -val isRel : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isRel]"] -val isRelN : int -> constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isRelN]"] -val isVar : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isVar]"] -val isVarId : Id.t -> constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isVarId]"] -val isInd : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isInd]"] -val isEvar : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isEvar]"] -val isMeta : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isMeta]"] -val isEvar_or_Meta : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isEvar_or_Meta]"] -val isSort : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isSort]"] -val isCast : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isCast]"] -val isApp : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isApp]"] -val isLambda : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isLambda]"] -val isLetIn : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isletIn]"] -val isProd : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isProp]"] -val isConst : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isConst]"] -val isConstruct : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isConstruct]"] -val isFix : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isFix]"] -val isCoFix : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isCoFix]"] -val isCase : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isCase]"] -val isProj : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isProj]"] - -val is_Prop : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.is_Prop]"] -val is_Set : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.is_Set]"] -val isprop : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isprop]"] -val is_Type : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.is_Type]"] -val iskind : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.is_kind]"] -val is_small : Sorts.t -> bool -[@@ocaml.deprecated "Alias for [Constr.is_small]"] - - -(** {5 Term destructors } *) -(** Destructor operations are partial functions and - @raise DestKO if the term has not the expected form. *) - -(** Destructs a de Bruijn index *) -val destRel : constr -> int -[@@ocaml.deprecated "Alias for [Constr.destRel]"] - -(** Destructs an existential variable *) -val destMeta : constr -> metavariable -[@@ocaml.deprecated "Alias for [Constr.destMeta]"] - -(** Destructs a variable *) -val destVar : constr -> Id.t -[@@ocaml.deprecated "Alias for [Constr.destVar]"] - -(** Destructs a sort. [is_Prop] recognizes the sort {% \textsf{%}Prop{% }%}, whether - [isprop] recognizes both {% \textsf{%}Prop{% }%} and {% \textsf{%}Set{% }%}. *) -val destSort : constr -> Sorts.t -[@@ocaml.deprecated "Alias for [Constr.destSort]"] - -(** Destructs a casted term *) -val destCast : constr -> constr * cast_kind * constr -[@@ocaml.deprecated "Alias for [Constr.destCast]"] - -(** Destructs the product {% $ %}(x:t_1)t_2{% $ %} *) -val destProd : types -> Name.t * types * types -[@@ocaml.deprecated "Alias for [Constr.destProd]"] - -(** Destructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *) -val destLambda : constr -> Name.t * types * constr -[@@ocaml.deprecated "Alias for [Constr.destLambda]"] - -(** Destructs the let {% $ %}[x:=b:t_1]t_2{% $ %} *) -val destLetIn : constr -> Name.t * constr * types * constr -[@@ocaml.deprecated "Alias for [Constr.destLetIn]"] - -(** Destructs an application *) -val destApp : constr -> constr * constr array -[@@ocaml.deprecated "Alias for [Constr.destApp]"] - -(** Obsolete synonym of destApp *) -val destApplication : constr -> constr * constr array -[@@ocaml.deprecated "Alias for [Constr.destApplication]"] - -(** Decompose any term as an applicative term; the list of args can be empty *) -val decompose_app : constr -> constr * constr list -[@@ocaml.deprecated "Alias for [Constr.decompose_app]"] - -(** Same as [decompose_app], but returns an array. *) -val decompose_appvect : constr -> constr * constr array -[@@ocaml.deprecated "Alias for [Constr.decompose_appvect]"] - -(** Destructs a constant *) -val destConst : constr -> Constant.t Univ.puniverses -[@@ocaml.deprecated "Alias for [Constr.destConst]"] - -(** Destructs an existential variable *) -val destEvar : constr -> existential -[@@ocaml.deprecated "Alias for [Constr.destEvar]"] - -(** Destructs a (co)inductive type *) -val destInd : constr -> inductive Univ.puniverses -[@@ocaml.deprecated "Alias for [Constr.destInd]"] - -(** Destructs a constructor *) -val destConstruct : constr -> constructor Univ.puniverses -[@@ocaml.deprecated "Alias for [Constr.destConstruct]"] - -(** Destructs a [match c as x in I args return P with ... | -Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args -return P in t1], or [if c then t1 else t2]) -@return [(info,c,fun args x => P,[|...|fun yij => ti| ...|])] -where [info] is pretty-printing information *) -val destCase : constr -> case_info * constr * constr * constr array -[@@ocaml.deprecated "Alias for [Constr.destCase]"] - -(** Destructs a projection *) -val destProj : constr -> Projection.t * constr -[@@ocaml.deprecated "Alias for [Constr.destProj]"] - -(** Destructs the {% $ %}i{% $ %}th function of the block - [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1} - with f{_ 2} ctx{_ 2} = b{_ 2} - ... - with f{_ n} ctx{_ n} = b{_ n}], - where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. -*) -val destFix : constr -> fixpoint -[@@ocaml.deprecated "Alias for [Constr.destFix]"] - -val destCoFix : constr -> cofixpoint -[@@ocaml.deprecated "Alias for [Constr.destCoFix]"] - (** {5 Derived constructors} *) (** non-dependent product [t1 -> t2], an alias for @@ -349,242 +189,14 @@ type ('constr, 'types) kind_of_type = val kind_of_type : types -> (constr, types) kind_of_type -(** {5 Redeclaration of stuff from module [Sorts]} *) - -val set_sort : Sorts.t -[@@ocaml.deprecated "Alias for Sorts.set"] - -val prop_sort : Sorts.t -[@@ocaml.deprecated "Alias for Sorts.prop"] - -val type1_sort : Sorts.t -[@@ocaml.deprecated "Alias for Sorts.type1"] - -val sorts_ord : Sorts.t -> Sorts.t -> int -[@@ocaml.deprecated "Alias for Sorts.compare"] - -val is_prop_sort : Sorts.t -> bool -[@@ocaml.deprecated "Alias for Sorts.is_prop"] - -val family_of_sort : Sorts.t -> Sorts.family -[@@ocaml.deprecated "Alias for Sorts.family"] - -(** {5 Redeclaration of stuff from module [Constr]} - - See module [Constr] for further info. *) - -(** {6 Term constructors. } *) - -val mkRel : int -> constr -[@@ocaml.deprecated "Alias for Constr.mkRel"] -val mkVar : Id.t -> constr -[@@ocaml.deprecated "Alias for Constr.mkVar"] -val mkMeta : metavariable -> constr -[@@ocaml.deprecated "Alias for Constr.mkMeta"] -val mkEvar : existential -> constr -[@@ocaml.deprecated "Alias for Constr.mkEvar"] -val mkSort : Sorts.t -> types -[@@ocaml.deprecated "Alias for Constr.mkSort"] -val mkProp : types -[@@ocaml.deprecated "Alias for Constr.mkProp"] -val mkSet : types -[@@ocaml.deprecated "Alias for Constr.mkSet"] -val mkType : Univ.Universe.t -> types -[@@ocaml.deprecated "Alias for Constr.mkType"] -val mkCast : constr * cast_kind * constr -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkProd : Name.t * types * types -> types -[@@ocaml.deprecated "Alias for Constr"] -val mkLambda : Name.t * types * constr -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkLetIn : Name.t * constr * types * constr -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkApp : constr * constr array -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkConst : Constant.t -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkProj : Projection.t * constr -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkInd : inductive -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkConstruct : constructor -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkConstU : Constant.t Univ.puniverses -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkIndU : inductive Univ.puniverses -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkConstructU : constructor Univ.puniverses -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkConstructUi : (pinductive * int) -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkCase : case_info * constr * constr * constr array -> constr -[@@ocaml.deprecated "Alias for Constr.mkCase"] -val mkFix : fixpoint -> constr -[@@ocaml.deprecated "Alias for Constr.mkFix"] -val mkCoFix : cofixpoint -> constr -[@@ocaml.deprecated "Alias for Constr.mkCoFix"] - -(** {6 Aliases} *) - -val eq_constr : constr -> constr -> bool -[@@ocaml.deprecated "Alias for Constr.equal"] - -(** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts, - application grouping and the universe constraints in [u]. *) -val eq_constr_univs : constr UGraph.check_function -[@@ocaml.deprecated "Alias for Constr.eq_constr_univs"] - -(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo - alpha, casts, application grouping and the universe constraints in [u]. *) -val leq_constr_univs : constr UGraph.check_function -[@@ocaml.deprecated "Alias for Constr.leq_constr_univs"] - -(** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts, - application grouping and ignoring universe instances. *) -val eq_constr_nounivs : constr -> constr -> bool -[@@ocaml.deprecated "Alias for Constr.qe_constr_nounivs"] - -val kind_of_term : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term -[@@ocaml.deprecated "Alias for Constr.kind"] - -val compare : constr -> constr -> int -[@@ocaml.deprecated "Alias for [Constr.compare]"] - -val constr_ord : constr -> constr -> int -[@@ocaml.deprecated "Alias for [Term.compare]"] - -val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a -[@@ocaml.deprecated "Alias for [Constr.fold]"] - -val map_constr : (constr -> constr) -> constr -> constr -[@@ocaml.deprecated "Alias for [Constr.map]"] - -val map_constr_with_binders : - ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr -[@@ocaml.deprecated "Alias for [Constr.map_with_binders]"] - -val map_puniverses : ('a -> 'b) -> 'a Univ.puniverses -> 'b Univ.puniverses -[@@ocaml.deprecated "Alias for [Constr.map_puniverses]"] -val univ_of_sort : Sorts.t -> Univ.Universe.t -[@@ocaml.deprecated "Alias for [Sorts.univ_of_sort]"] -val sort_of_univ : Univ.Universe.t -> Sorts.t -[@@ocaml.deprecated "Alias for [Sorts.sort_of_univ]"] - -val iter_constr : (constr -> unit) -> constr -> unit -[@@ocaml.deprecated "Alias for [Constr.iter]"] - -val iter_constr_with_binders : - ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit -[@@ocaml.deprecated "Alias for [Constr.iter_with_binders]"] - -val compare_constr : (int -> constr -> constr -> bool) -> int -> constr -> constr -> bool -[@@ocaml.deprecated "Alias for [Constr.compare_head]"] - -type constr = Constr.constr -[@@ocaml.deprecated "Alias for Constr.t"] - -(** Alias types, for compatibility. *) - -type types = Constr.types -[@@ocaml.deprecated "Alias for Constr.types"] - +(* Deprecated *) type contents = Sorts.contents = Pos | Null [@@ocaml.deprecated "Alias for Sorts.contents"] +type sorts_family = Sorts.family = InProp | InSet | InType +[@@ocaml.deprecated "Alias for Sorts.family"] + type sorts = Sorts.t = | Prop of Sorts.contents (** Prop and Set *) | Type of Univ.Universe.t (** Type *) [@@ocaml.deprecated "Alias for Sorts.t"] - -type sorts_family = Sorts.family = InProp | InSet | InType -[@@ocaml.deprecated "Alias for Sorts.family"] - -type 'a puniverses = 'a Univ.puniverses -[@@ocaml.deprecated "Alias for Constr.puniverses"] - -(** Simply type aliases *) -type pconstant = Constr.pconstant -[@@ocaml.deprecated "Alias for Constr.pconstant"] -type pinductive = Constr.pinductive -[@@ocaml.deprecated "Alias for Constr.pinductive"] -type pconstructor = Constr.pconstructor -[@@ocaml.deprecated "Alias for Constr.pconstructor"] -type existential_key = Evar.t -[@@ocaml.deprecated "Alias for Evar.t"] -type existential = Constr.existential -[@@ocaml.deprecated "Alias for Constr.existential"] -type metavariable = Constr.metavariable -[@@ocaml.deprecated "Alias for Constr.metavariable"] - -type case_style = Constr.case_style = - LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle -[@@ocaml.deprecated "Alias for Constr.case_style"] - -type case_printing = Constr.case_printing = - { ind_tags : bool list; cstr_tags : bool list array; style : Constr.case_style } -[@@ocaml.deprecated "Alias for Constr.case_printing"] - -type case_info = Constr.case_info = - { ci_ind : inductive; - ci_npar : int; - ci_cstr_ndecls : int array; - ci_cstr_nargs : int array; - ci_pp_info : Constr.case_printing - } -[@@ocaml.deprecated "Alias for Constr.case_info"] - -type cast_kind = Constr.cast_kind = - VMcast | NATIVEcast | DEFAULTcast | REVERTcast -[@@ocaml.deprecated "Alias for Constr.cast_kind"] - -type rec_declaration = Constr.rec_declaration -[@@ocaml.deprecated "Alias for Constr.rec_declaration"] -type fixpoint = Constr.fixpoint -[@@ocaml.deprecated "Alias for Constr.fixpoint"] -type cofixpoint = Constr.cofixpoint -[@@ocaml.deprecated "Alias for Constr.cofixpoint"] -type 'constr pexistential = 'constr Constr.pexistential -[@@ocaml.deprecated "Alias for Constr.pexistential"] -type ('constr, 'types) prec_declaration = - ('constr, 'types) Constr.prec_declaration -[@@ocaml.deprecated "Alias for Constr.prec_declaration"] -type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint -[@@ocaml.deprecated "Alias for Constr.pfixpoint"] -type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint -[@@ocaml.deprecated "Alias for Constr.pcofixpoint"] - -type ('constr, 'types, 'sort, 'univs) kind_of_term = - ('constr, 'types, 'sort, 'univs) Constr.kind_of_term = - | Rel of int - | Var of Id.t - | Meta of Constr.metavariable - | Evar of 'constr Constr.pexistential - | Sort of 'sort - | Cast of 'constr * Constr.cast_kind * 'types - | Prod of Name.t * 'types * 'types - | Lambda of Name.t * 'types * 'constr - | LetIn of Name.t * 'constr * 'types * 'constr - | App of 'constr * 'constr array - | Const of (Constant.t * 'univs) - | Ind of (inductive * 'univs) - | Construct of (constructor * 'univs) - | Case of Constr.case_info * 'constr * 'constr * 'constr array - | Fix of ('constr, 'types) Constr.pfixpoint - | CoFix of ('constr, 'types) Constr.pcofixpoint - | Proj of Projection.t * 'constr -[@@ocaml.deprecated "Alias for Constr.kind_of_term"] - -type values = Vmvalues.values -[@@ocaml.deprecated "Alias for Vmvalues.values"] - -val hash_constr : Constr.constr -> int -[@@ocaml.deprecated "Alias for Constr.hash"] - -val hcons_sorts : Sorts.t -> Sorts.t -[@@ocaml.deprecated "Alias for [Sorts.hcons]"] - -val hcons_constr : Constr.constr -> Constr.constr -[@@ocaml.deprecated "Alias for [Constr.hcons]"] - -val hcons_types : Constr.types -> Constr.types -[@@ocaml.deprecated "Alias for [Constr.hcons]"] diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index e621a61c76..db1109e75e 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -250,7 +250,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = Undef nl; cook_type = t; - cook_proj = None; + cook_proj = false; cook_universes = univs; cook_inline = false; cook_context = ctx; @@ -291,7 +291,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = def; cook_type = typ; - cook_proj = None; + cook_proj = false; cook_universes = Monomorphic_const univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; @@ -343,7 +343,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = def; cook_type = typ; - cook_proj = None; + cook_proj = false; cook_universes = univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; @@ -370,7 +370,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = Def (Mod_subst.from_val (Constr.hcons term)); cook_type = typ; - cook_proj = Some pb; + cook_proj = true; cook_universes = univs; cook_inline = false; cook_context = None; @@ -458,30 +458,8 @@ let build_constant_declaration kn env result = check declared inferred) lc) in let univs = result.cook_universes in let tps = - let res = - match result.cook_proj with - | None -> compile_constant_body 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 => - Proj(p,c)). We break the cycle by building an ad-hoc compilation - environment. A cleaner solution would be that kernel projections are - simply Proj(i,c) with i an int and c a constr, but we would have to - get rid of the compatibility layer. *) - let cb = - { const_hyps = hyps; - const_body = def; - const_type = typ; - const_proj = result.cook_proj; - const_body_code = None; - const_universes = univs; - const_inline_code = result.cook_inline; - const_typing_flags = Environ.typing_flags env; - } - in - let env = add_constant kn cb env in - compile_constant_body env univs def - in Option.map Cemitcodes.from_val res + let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in + Option.map Cemitcodes.from_val res in { const_hyps = hyps; const_body = def; diff --git a/kernel/typeops.ml b/kernel/typeops.ml index be4c0e1ecc..325d5cecd7 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 -> @@ -528,13 +528,3 @@ let judge_of_case env ci pj cj lfj = let lf, lft = dest_judgev lfj in make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) (type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft) - -let type_of_projection_constant env (p,u) = - let cst = Projection.constant p in - let cb = lookup_constant cst env in - match cb.const_proj with - | Some pb -> - if Declareops.constant_is_polymorphic cb then - Vars.subst_instance_constr u pb.proj_type - else pb.proj_type - | None -> raise (Invalid_argument "type_of_projection: not a projection") diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 85b2cfffde..546f2d2b4d 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -100,8 +100,6 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -val type_of_projection_constant : env -> Projection.t puniverses -> types - val type_of_constant_in : env -> pconstant -> types (** Check that hyps are included in env and fails with error otherwise *) diff --git a/kernel/vconv.ml b/kernel/vconv.ml index f11803b67c..4e4168922d 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 620f6b5e8a..1a31848989 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 |