From f19a9d9d3a410fda982b2cf9154da5774f9ec84f Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 28 Jan 2011 13:20:41 +0000 Subject: Remove the "Boxed" syntaxes and the const_entry_boxed field According to B. Gregoire, this stuff is obsolete. Fine control on when to launch the VM in conversion problems is now provided by VMcast. We were already almost never boxing definitions anymore in stdlib files. "(Un)Boxed Definition foo" will now trigger a parsing error, same with Fixpoint. The option "(Un)Set Boxed Definitions" aren't there anymore, but tolerated (as no-ops), since unknown options raise a warning instead of an error by default. Some more cleaning could be done in the vm. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13806 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/cbytegen.ml | 11 +++-------- kernel/cbytegen.mli | 4 ++-- kernel/cemitcodes.ml | 9 ++------- kernel/cemitcodes.mli | 4 +--- kernel/cooking.ml | 3 +-- kernel/cooking.mli | 2 +- kernel/csymtable.ml | 5 ++--- kernel/entries.ml | 3 +-- kernel/entries.mli | 3 +-- kernel/environ.mli | 4 ++-- kernel/mod_typing.ml | 4 ++-- kernel/modops.ml | 2 +- kernel/term_typing.ml | 8 ++++---- kernel/term_typing.mli | 4 ++-- 14 files changed, 25 insertions(+), 41 deletions(-) (limited to 'kernel') diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 9c00af5dff..337b907512 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -714,18 +714,13 @@ let compile env c = Format.print_flush(); *) init_code,!fun_code, Array.of_list fv -let compile_constant_body env body opaque boxed = +let compile_constant_body env body opaque = if opaque then BCconstant else match body with | None -> BCconstant | Some sb -> let body = Declarations.force sb in - if boxed then - let res = compile env body in - let to_patch = to_memory res in - BCdefined(true, to_patch) - else - match kind_of_term body with + match kind_of_term body with | Const kn' -> (* we use the canonical name of the constant*) let con= constant_of_kn (canonical_con kn') in @@ -733,7 +728,7 @@ let compile_constant_body env body opaque boxed = | _ -> let res = compile env body in let to_patch = to_memory res in - BCdefined (false, to_patch) + BCdefined to_patch (* spiwack: additional function which allow different part of compilation of the diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index bf9c0be263..403c1c7b5b 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -10,8 +10,8 @@ val compile : env -> constr -> bytecodes * bytecodes * fv (** init, fun, fv *) val compile_constant_body : - env -> constr_substituted option -> bool -> bool -> body_code - (** opaque *) (* boxed *) + env -> constr_substituted option -> bool -> body_code + (** opaque *) (** spiwack: this function contains the information needed to perform diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 1138031c7a..277b343b24 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -331,12 +331,12 @@ let subst_to_patch s (code,pl,fv) = code,List.rev_map (subst_patch s) pl,fv type body_code = - | BCdefined of bool * to_patch + | BCdefined of to_patch | BCallias of constant | BCconstant let subst_body_code s = function - | BCdefined (b,tp) -> BCdefined (b,subst_to_patch s tp) + | BCdefined tp -> BCdefined (subst_to_patch s tp) | BCallias kn -> BCallias (fst (subst_con s kn)) | BCconstant -> BCconstant @@ -348,11 +348,6 @@ let force = force subst_body_code let subst_to_patch_subst = subst_substituted -let is_boxed tps = - match force tps with - | BCdefined(b,_) -> b - | _ -> false - let to_memory (init_code, fun_code, fv) = init(); emit init_code; diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index a8ecc82b41..43cebb4748 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -22,7 +22,7 @@ type to_patch = emitcodes * (patch list) * fv val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch type body_code = - | BCdefined of bool*to_patch + | BCdefined of to_patch | BCallias of constant | BCconstant @@ -33,8 +33,6 @@ val from_val : body_code -> to_patch_substituted val force : to_patch_substituted -> body_code -val is_boxed : to_patch_substituted -> bool - val subst_to_patch_subst : Mod_subst.substitution -> to_patch_substituted -> to_patch_substituted val to_memory : bytecodes * bytecodes * fv -> to_patch diff --git a/kernel/cooking.ml b/kernel/cooking.ml index e4336683d1..d01398841c 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -137,5 +137,4 @@ let cook_constant env r = let j = make_judge (force (Option.get body)) typ in Typeops.make_polymorphic_if_constant_for_ind env j in - let boxed = Cemitcodes.is_boxed cb.const_body_code in - (body, typ, cb.const_constraints, cb.const_opaque, boxed,false) + (body, typ, cb.const_constraints, cb.const_opaque, false) diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 0f604a4bee..09b42d0b12 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -24,7 +24,7 @@ type recipe = { val cook_constant : env -> recipe -> constr_substituted option * constant_type * constraints * bool * bool - * bool + (** {6 Utility functions used in module [Discharge]. } *) diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 983c1f26df..897cbf13a8 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -125,10 +125,9 @@ let rec slot_for_getglobal env kn = with NotEvaluated -> let pos = match Cemitcodes.force cb.const_body_code with - | BCdefined(boxed,(code,pl,fv)) -> + | BCdefined(code,pl,fv) -> let v = eval_to_patch env (code,pl,fv) in - if boxed then set_global_boxed kn v - else set_global v + set_global v | BCallias kn' -> slot_for_getglobal env kn' | BCconstant -> set_global (val_of_constant kn) in rk := Some pos; diff --git a/kernel/entries.ml b/kernel/entries.ml index 714da03196..dbf802bb12 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -57,8 +57,7 @@ type mutual_inductive_entry = { type definition_entry = { const_entry_body : constr; const_entry_type : types option; - const_entry_opaque : bool; - const_entry_boxed : bool} + const_entry_opaque : bool } (* type and the inlining flag *) type parameter_entry = types * bool diff --git a/kernel/entries.mli b/kernel/entries.mli index 2ba3064550..d45e2bbdb8 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -53,8 +53,7 @@ type mutual_inductive_entry = { type definition_entry = { const_entry_body : constr; const_entry_type : types option; - const_entry_opaque : bool; - const_entry_boxed : bool } + const_entry_opaque : bool } type parameter_entry = types * bool (*inline flag*) diff --git a/kernel/environ.mli b/kernel/environ.mli index 078d70965d..f26d49dde4 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -190,8 +190,8 @@ type unsafe_type_judgment = { (** {6 Compilation of global declaration } *) val compile_constant_body : - env -> constr_substituted option -> bool -> bool -> Cemitcodes.body_code - (** opaque *) (* boxed *) + env -> constr_substituted option -> bool -> Cemitcodes.body_code + (** opaque *) exception Hyp_not_found diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 5a3dade530..407ae73ca7 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -95,7 +95,7 @@ and check_with_aux_def env sign with_decl mp equiv = let cb' = {cb with const_body = body; const_body_code = Cemitcodes.from_val - (compile_constant_body env' body false false); + (compile_constant_body env' body false); const_constraints = cst} in SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst | Some b -> @@ -105,7 +105,7 @@ and check_with_aux_def env sign with_decl mp equiv = let cb' = {cb with const_body = body; const_body_code = Cemitcodes.from_val - (compile_constant_body env' body false false); + (compile_constant_body env' body false); const_constraints = cst} in SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst end diff --git a/kernel/modops.ml b/kernel/modops.ml index 9da2f49622..ce968b40ef 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -276,7 +276,7 @@ let strengthen_const env mp_from l cb resolver = const_body = const_subs; const_opaque = false; const_body_code = Cemitcodes.from_val - (compile_constant_body env const_subs false false) + (compile_constant_body env const_subs false) } diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index f765dd77e9..432460d7d5 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -94,11 +94,11 @@ let infer_declaration env dcl = let (j,cst) = infer env c.const_entry_body in let (typ,cst) = constrain_type env j cst c.const_entry_type in Some (Declarations.from_val j.uj_val), typ, cst, - c.const_entry_opaque, c.const_entry_boxed, false + c.const_entry_opaque, false | ParameterEntry (t,nl) -> let (j,cst) = infer env t in None, NonPolymorphicType (Typeops.assumption_of_judgment env j), cst, - false, false, nl + false, nl let global_vars_set_constant_type env = function | NonPolymorphicType t -> global_vars_set env t @@ -108,7 +108,7 @@ let global_vars_set_constant_type env = function (fun t c -> Idset.union (global_vars_set env t) c)) ctx ~init:Idset.empty -let build_constant_declaration env kn (body,typ,cst,op,boxed,inline) = +let build_constant_declaration env kn (body,typ,cst,op,inline) = let ids = match body with | None -> global_vars_set_constant_type env typ @@ -117,7 +117,7 @@ let build_constant_declaration env kn (body,typ,cst,op,boxed,inline) = (global_vars_set env (Declarations.force b)) (global_vars_set_constant_type env typ) in - let tps = Cemitcodes.from_val (compile_constant_body env body op boxed) in + let tps = Cemitcodes.from_val (compile_constant_body env body op) in let hyps = keep_hyps env ids in { const_hyps = hyps; const_body = body; diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 628aa93756..500858a59c 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -22,10 +22,10 @@ val translate_local_assum : env -> types -> types * Univ.constraints val infer_declaration : env -> constant_entry -> - constr_substituted option * constant_type * constraints * bool * bool * bool + constr_substituted option * constant_type * constraints * bool * bool val build_constant_declaration : env -> 'a -> - constr_substituted option * constant_type * constraints * bool * bool * bool -> + constr_substituted option * constant_type * constraints * bool * bool -> constant_body val translate_constant : env -> constant -> constant_entry -> constant_body -- cgit v1.2.3