diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-07 17:59:15 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-07 18:20:56 +0100 |
commit | 2ee61d5995ef572f0124691f10630305a59b4f73 (patch) | |
tree | eaeffb7be70ce770a822108f8a527312f67fd8b2 /kernel/safe_typing.ml | |
parent | ba021624830c7ad5df0688d144e4305551ae1a5f (diff) | |
parent | de109d8c0c68f569b907e6e24271f259ba28888e (diff) |
Prepare upload to squeeze-backportsdebian/8.3.pl3+dfsg-1_bpo60+1
Diffstat (limited to 'kernel/safe_typing.ml')
-rw-r--r-- | kernel/safe_typing.ml | 49 |
1 files changed, 25 insertions, 24 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index dee2f5e8..4575d5bc 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: safe_typing.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: safe_typing.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Names @@ -40,10 +40,26 @@ type module_info = variant : modvariant; resolver : delta_resolver; resolver_of_param : delta_resolver;} - + let check_label l labset = if Labset.mem l labset then error_existing_label l +let check_labels ls senv = + Labset.iter (fun l -> check_label l senv) ls + +let labels_of_mib mib = + let add,get = + let labels = ref Labset.empty in + (fun id -> labels := Labset.add (label_of_id id) !labels), + (fun () -> !labels) + in + let visit_mip mip = + add mip.mind_typename; + Array.iter add mip.mind_consnames + in + Array.iter visit_mip mib.mind_packets; + get () + let set_engagement_opt oeng env = match oeng with Some eng -> set_engagement eng env @@ -107,22 +123,6 @@ let add_constraints cst senv = univ = Univ.Constraint.union cst senv.univ } -(*spiwack: functions for safe retroknowledge *) - -(* terms which are closed under the environnement env, i.e - terms which only depends on constant who are themselves closed *) -let closed env term = - ContextObjectMap.is_empty (assumptions full_transparent_state env term) - -(* the set of safe terms in an environement any recursive set of - terms who are known not to prove inconsistent statement. It should - include at least all the closed terms. But it could contain other ones - like the axiom of excluded middle for instance *) -let safe = - closed - - - (* universal lifting, used for the "get" operations mostly *) let retroknowledge f senv = Environ.retroknowledge f (env_of_senv senv) @@ -242,17 +242,16 @@ let add_mind dir l mie senv = if l <> label_of_id id then anomaly ("the label of inductive packet and its first inductive"^ " type do not match"); - check_label l senv.labset; - (* TODO: when we will allow reorderings we will have to verify - all labels *) let mib = translate_mind senv.env mie in + let labels = labels_of_mib mib in + check_labels labels senv.labset; let senv' = add_constraints mib.mind_constraints senv in let kn = make_mind senv.modinfo.modpath dir l in let env'' = Environ.add_mind kn mib senv'.env in kn, { old = senv'.old; env = env''; modinfo = senv'.modinfo; - labset = Labset.add l senv'.labset; (* TODO: the same as above *) + labset = Labset.union labels senv'.labset; revstruct = (l,SFBmind mib)::senv'.revstruct; univ = senv'.univ; engagement = senv'.engagement; @@ -495,12 +494,14 @@ let end_module l restype senv = (canonical_mind (mind_of_delta resolver (mind_of_kn kn))) in + let labels = labels_of_mib mib in + check_labels labels senv.labset; let senv' = add_constraints mib.mind_constraints senv in let env'' = Environ.add_mind mind mib senv'.env in { old = senv'.old; env = env''; modinfo = senv'.modinfo; - labset = Labset.add l senv'.labset; + labset = Labset.union labels senv'.labset; revstruct = (l,SFBmind mib)::senv'.revstruct; univ = senv'.univ; engagement = senv'.engagement; |