diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cooking.ml | 2 | ||||
| -rw-r--r-- | kernel/cooking.mli | 3 | ||||
| -rw-r--r-- | kernel/declarations.ml | 6 | ||||
| -rw-r--r-- | kernel/declarations.mli | 3 | ||||
| -rw-r--r-- | kernel/entries.ml | 2 | ||||
| -rw-r--r-- | kernel/entries.mli | 2 | ||||
| -rw-r--r-- | kernel/modops.ml | 26 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 11 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 4 |
9 files changed, 40 insertions, 19 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 7751e5bf6..e9200cd75 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -131,4 +131,4 @@ let cook_constant env r = let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in Typeops.make_polymorphic_if_arity env typ in let boxed = Cemitcodes.is_boxed cb.const_body_code in - (body, typ, cb.const_constraints, cb.const_opaque, boxed) + (body, typ, cb.const_constraints, cb.const_opaque, boxed,false) diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 0646b1c22..4afdaa55e 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -25,7 +25,8 @@ type recipe = { val cook_constant : env -> recipe -> - constr_substituted option * constant_type * constraints * bool * bool + constr_substituted option * constant_type * constraints * bool * bool + * bool (*s Utility functions used in module [Discharge]. *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index d0f2289dc..1be251a50 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -49,7 +49,8 @@ type constant_body = { const_body_code : Cemitcodes.to_patch_substituted; (* const_type_code : Cemitcodes.to_patch; *) const_constraints : constraints; - const_opaque : bool } + const_opaque : bool; + const_inline : bool} (*s Inductive types (internal representation with redundant information). *) @@ -202,7 +203,8 @@ let subst_const_body sub cb = { const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code; (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*) const_constraints = cb.const_constraints; - const_opaque = cb.const_opaque } + const_opaque = cb.const_opaque; + const_inline = cb.const_inline} let subst_arity sub = function | Monomorphic s -> diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 22cfd62a0..7f7f7dcc3 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -47,7 +47,8 @@ type constant_body = { const_body_code : to_patch_substituted; (*i const_type_code : to_patch;i*) const_constraints : constraints; - const_opaque : bool } + const_opaque : bool; + const_inline : bool} val subst_const_body : substitution -> constant_body -> constant_body diff --git a/kernel/entries.ml b/kernel/entries.ml index fb134b1c7..17da967c2 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -62,7 +62,7 @@ type definition_entry = { const_entry_opaque : bool; const_entry_boxed : bool} -type parameter_entry = types +type parameter_entry = types*bool type constant_entry = | DefinitionEntry of definition_entry diff --git a/kernel/entries.mli b/kernel/entries.mli index 61c0b8c3b..56ea852da 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -61,7 +61,7 @@ type definition_entry = { const_entry_opaque : bool; const_entry_boxed : bool } -type parameter_entry = types +type parameter_entry = types*bool (*inline flag*) type constant_entry = | DefinitionEntry of definition_entry diff --git a/kernel/modops.ml b/kernel/modops.ml index e9e1d67eb..96d19552a 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -235,13 +235,29 @@ and constants_of_modtype env mp modtype = | MTBfunsig _ -> [] (* returns a resolver for kn that maps mbid to mp *) -(* Nota: Some delta-expansions used to happen here. - Browse SVN if you want to know more. *) let resolver_of_environment mbid modtype mp env = let constants = constants_of_modtype env (MPbound mbid) modtype in - let resolve = List.map (fun (con,_) -> con,None) constants in - Mod_subst.make_resolver resolve - + let resolve = + List.map + (fun (con,expecteddef) -> + let con' = replace_mp_in_con (MPbound mbid) mp con in + let constr = + try + if expecteddef.Declarations.const_inline then + let constant = lookup_constant con' env in + if constant.Declarations.const_opaque then + None + else + option_map Declarations.force + constant.Declarations.const_body + else + None + with Not_found -> error_no_such_label (con_label con') + in + con,constr + ) constants + in + Mod_subst.make_resolver resolve let strengthen_const env mp l cb = match cb.const_opaque, cb.const_body with diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 8b0f45ac9..aedc44ac8 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -93,11 +93,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 - | ParameterEntry t -> + c.const_entry_opaque, c.const_entry_boxed, false + | ParameterEntry (t,nl) -> let (j,cst) = infer env t in None, NonPolymorphicType (Typeops.assumption_of_judgment env j), cst, - false, false + false, false, nl let global_vars_set_constant_type env = function | NonPolymorphicType t -> global_vars_set env t @@ -107,7 +107,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) = +let build_constant_declaration env kn (body,typ,cst,op,boxed,inline) = let ids = match body with | None -> global_vars_set_constant_type env typ @@ -124,7 +124,8 @@ let build_constant_declaration env kn (body,typ,cst,op,boxed) = const_body_code = tps; (* const_type_code = to_patch env typ;*) const_constraints = cst; - const_opaque = op } + const_opaque = op; + const_inline = inline} (*s Global and local constant declaration. *) diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 83434e2ec..abff3e8b7 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -26,10 +26,10 @@ val translate_local_assum : env -> types -> types * Univ.constraints val infer_declaration : env -> constant_entry -> - constr_substituted option * constant_type * constraints * bool * bool + constr_substituted option * constant_type * constraints * bool * bool * bool val build_constant_declaration : env -> 'a -> - constr_substituted option * constant_type * constraints * bool * bool -> + constr_substituted option * constant_type * constraints * bool * bool * bool -> constant_body val translate_constant : env -> constant -> constant_entry -> constant_body |