diff options
author | Arnaud Spiwack <arnaud@spiwack.net> | 2015-09-25 15:09:15 +0200 |
---|---|---|
committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-09-25 15:09:15 +0200 |
commit | caf8402e4af75d85223e10cba68a6a145e050dab (patch) | |
tree | e8c3af2139d78b7e0117fd4987b7eb3732381577 /kernel | |
parent | 0b20282c49253aea4429384467b75a5bdb1f8ba4 (diff) |
Add a field in `constant_body` to track constant whose well-foundedness is assumed.
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/declarations.mli | 4 | ||||
-rw-r--r-- | kernel/declareops.ml | 3 | ||||
-rw-r--r-- | kernel/term_typing.ml | 9 | ||||
-rw-r--r-- | kernel/term_typing.mli | 2 |
4 files changed, 11 insertions, 7 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index ef3e1bb6a..591a7d404 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -74,7 +74,9 @@ type constant_body = { const_polymorphic : bool; (** Is it polymorphic or not *) const_universes : constant_universes; const_proj : projection_body option; - const_inline_code : bool } + const_inline_code : bool; + const_checked_guarded : bool; (** [false] is the (co)fixpoint in the constant were assumed to be well-founded. *) +} type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ] diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 870aef1d2..068bc498a 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -132,7 +132,8 @@ let subst_const_body sub cb = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_polymorphic = cb.const_polymorphic; const_universes = cb.const_universes; - const_inline_code = cb.const_inline_code } + const_inline_code = cb.const_inline_code; + const_checked_guarded = cb.const_checked_guarded } (** {7 Hash-consing of constants } *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 539305ed1..8a105ac97 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -186,7 +186,7 @@ let record_aux env s1 s2 = let suggest_proof_using = ref (fun _ _ _ _ _ -> ()) let set_suggest_proof_using f = suggest_proof_using := f -let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) = +let build_constant_declaration ~chkguard kn env (def,typ,proj,poly,univs,inline_code,ctx) = let check declared inferred = let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in let inferred_set, declared_set = mk_set inferred, mk_set declared in @@ -261,13 +261,14 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) const_body_code = tps; const_polymorphic = poly; const_universes = univs; - const_inline_code = inline_code } + const_inline_code = inline_code; + const_checked_guarded = chkguard } (*s Global and local constant declaration. *) let translate_constant ~chkguard env kn ce = - build_constant_declaration kn env (infer_declaration ~chkguard env (Some kn) ce) + build_constant_declaration ~chkguard kn env (infer_declaration ~chkguard env (Some kn) ce) let translate_local_assum ~chkguard env t = let j = infer ~chkguard env t in @@ -275,7 +276,7 @@ let translate_local_assum ~chkguard env t = t let translate_recipe env kn r = - build_constant_declaration kn env (Cooking.cook_constant env r) + build_constant_declaration ~chkguard:true kn env (Cooking.cook_constant env r) let translate_local_def ~chkguard env id centry = let def,typ,proj,poly,univs,inline_code,ctx = diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index a71587f0f..ba4d96a5f 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -41,7 +41,7 @@ val infer_declaration : chkguard:bool -> env -> constant option -> constant_entry -> Cooking.result val build_constant_declaration : - constant -> env -> Cooking.result -> constant_body + chkguard:bool -> constant -> env -> Cooking.result -> constant_body val set_suggest_proof_using : (constant -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> unit) -> unit |