diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/entries.ml | 3 | ||||
| -rw-r--r-- | kernel/entries.mli | 3 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 37 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 5 |
4 files changed, 32 insertions, 16 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index 28f11c9af4..a4485fac7f 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -56,12 +56,13 @@ type mutual_inductive_entry = { type definition_entry = { const_entry_body : constr; + const_entry_secctx : section_context option; const_entry_type : types option; const_entry_opaque : bool } type inline = int option (* inlining level, None for no inlining *) -type parameter_entry = types * inline +type parameter_entry = section_context option * types * inline type constant_entry = | DefinitionEntry of definition_entry diff --git a/kernel/entries.mli b/kernel/entries.mli index 08740afae7..b726d0ec0d 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -52,12 +52,13 @@ type mutual_inductive_entry = { type definition_entry = { const_entry_body : constr; + const_entry_secctx : section_context option; const_entry_type : types option; const_entry_opaque : bool } type inline = int option (* inlining level, None for no inlining *) -type parameter_entry = types * inline +type parameter_entry = section_context option * types * inline type constant_entry = | DefinitionEntry of definition_entry diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index cc9366c116..478b9c6fc6 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -102,11 +102,11 @@ let infer_declaration env dcl = then OpaqueDef (Declarations.opaque_from_val j.uj_val) else Def (Declarations.from_val j.uj_val) in - def, typ, cst - | ParameterEntry (t,nl) -> + def, typ, cst, c.const_entry_secctx + | ParameterEntry (ctx,t,nl) -> let (j,cst) = infer env t in let t = hcons_constr (Typeops.assumption_of_judgment env j) in - Undef nl, NonPolymorphicType t, cst + Undef nl, NonPolymorphicType t, cst, ctx let global_vars_set_constant_type env = function | NonPolymorphicType t -> global_vars_set env t @@ -116,14 +116,26 @@ 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 (def,typ,cst) = - let ids_typ = global_vars_set_constant_type env typ in - let ids_def = match def with - | Undef _ -> Idset.empty - | Def cs -> global_vars_set env (Declarations.force cs) - | OpaqueDef lc -> global_vars_set env (Declarations.force_opaque lc) - in - let hyps = keep_hyps env (Idset.union ids_typ ids_def) in +let build_constant_declaration env kn (def,typ,cst,ctx) = + let hyps = + let inferred = + let ids_typ = global_vars_set_constant_type env typ in + let ids_def = match def with + | Undef _ -> Idset.empty + | Def cs -> global_vars_set env (Declarations.force cs) + | OpaqueDef lc -> + global_vars_set env (Declarations.force_opaque lc) in + keep_hyps env (Idset.union ids_typ ids_def) in + let declared = match ctx with + | None -> inferred + | Some declared -> declared in + let mk_set l = List.fold_right Idset.add (List.map pi1 l) Idset.empty in + let inferred_set, declared_set = mk_set inferred, mk_set declared in + if not (Idset.subset inferred_set declared_set) then + error ("The following section variable are used but not declared:\n"^ + (String.concat ", " (List.map string_of_id + (Idset.elements (Idset.diff inferred_set declared_set))))); + declared in let tps = Cemitcodes.from_val (compile_constant_body env def) in { const_hyps = hyps; const_body = def; @@ -137,7 +149,8 @@ let translate_constant env kn ce = build_constant_declaration env kn (infer_declaration env ce) let translate_recipe env kn r = - build_constant_declaration env kn (Cooking.cook_constant env r) + build_constant_declaration env kn + (let def,typ,cst = Cooking.cook_constant env r in def,typ,cst,None) (* Insertion of inductive types. *) diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 158f2c7877..3bbf566774 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -22,10 +22,11 @@ val translate_local_assum : env -> types -> types * Univ.constraints val infer_declaration : env -> constant_entry -> - constant_def * constant_type * constraints + constant_def * constant_type * constraints * Sign.section_context option val build_constant_declaration : env -> 'a -> - constant_def * constant_type * constraints -> constant_body + constant_def * constant_type * constraints * Sign.section_context option -> + constant_body val translate_constant : env -> constant -> constant_entry -> constant_body |