From e4282ea99c664d8d58067bee199cbbcf881b60d5 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 4 Jul 2009 13:28:35 +0200 Subject: Imported Upstream version 8.2.pl1+dfsg --- kernel/environ.ml | 40 +++++++++++++++++++++++++++------------- kernel/environ.mli | 9 +++++---- kernel/mod_subst.ml | 20 ++++++++++---------- kernel/modops.ml | 8 ++++---- kernel/safe_typing.ml | 4 ++-- 5 files changed, 48 insertions(+), 33 deletions(-) (limited to 'kernel') diff --git a/kernel/environ.ml b/kernel/environ.ml index 86e02623..cd4efe27 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: environ.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: environ.ml 12187 2009-06-13 19:36:59Z msozeau $ *) open Util open Names @@ -554,7 +554,7 @@ fun env field value -> type context_object = | Variable of identifier (* A section variable or a Let definition *) | Axiom of constant (* An axiom or a constant. *) - + | Opaque of constant (* An opaque constant. *) (* Defines a set of [assumption] *) module OrderedContextObject = @@ -566,15 +566,19 @@ struct | Axiom k1 , Axiom k2 -> Pervasives.compare k1 k2 (* spiwack: it would probably be cleaner to provide a [kn_ord] function *) + | Opaque k1 , Opaque k2 -> Pervasives.compare k1 k2 | Variable _ , Axiom _ -> -1 | Axiom _ , Variable _ -> 1 + | Opaque _ , _ -> -1 + | _, Opaque _ -> 1 end module ContextObjectSet = Set.Make (OrderedContextObject) module ContextObjectMap = Map.Make (OrderedContextObject) -let assumptions (* t env *) = +let assumptions ?(add_opaque=false) st (* t env *) = + let (idts,knst) = st in (* Infix definition for chaining function that accumulate on a and a ContextObjectSet, ContextObjectMap. *) let ( ** ) f1 f2 s m = let (s',m') = f1 s m in f2 s' m' in @@ -650,16 +654,26 @@ let assumptions (* t env *) = and add_kn kn env s acc = let cb = lookup_constant kn env in - match cb.Declarations.const_body with - | None -> - let ctype = - match cb.Declarations.const_type with - | PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level) - | NonPolymorphicType t -> t - in - (s,ContextObjectMap.add (Axiom kn) ctype acc) - | Some body -> aux (Declarations.force body) env s acc - + let do_type cst = + let ctype = + match cb.Declarations.const_type with + | PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level) + | NonPolymorphicType t -> t + in + (s,ContextObjectMap.add cst ctype acc) + in + let (s,acc) = + if cb.Declarations.const_body <> None + && (cb.Declarations.const_opaque || not (Cpred.mem kn knst)) + && add_opaque + then + do_type (Opaque kn) + else (s,acc) + in + match cb.Declarations.const_body with + | None -> do_type (Axiom kn) + | Some body -> aux (Declarations.force body) env s acc + and aux_memoize_kn kn env = try_and_go (Axiom kn) (add_kn kn env) in diff --git a/kernel/environ.mli b/kernel/environ.mli index 97e19782..b68123f6 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: environ.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id: environ.mli 12187 2009-06-13 19:36:59Z msozeau $ i*) (*i*) open Names @@ -244,13 +244,14 @@ val register : env -> field -> Retroknowledge.entry -> env type context_object = | Variable of identifier (* A section variable or a Let definition *) | Axiom of constant (* An axiom or a constant. *) + | Opaque of constant (* An opaque constant. *) (* AssumptionSet.t is a set of [assumption] *) module OrderedContextObject : Set.OrderedType with type t = context_object module ContextObjectMap : Map.S with type key = context_object -(* collects all the assumptions on which a term relies (together with - their type *) -val assumptions : constr -> env -> Term.types ContextObjectMap.t +(* collects all the assumptions (optionally including opaque definitions) + on which a term relies (together with their type) *) +val assumptions : ?add_opaque:bool -> transparent_state -> constr -> env -> Term.types ContextObjectMap.t diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index ab4b8e47..9a76922b 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: mod_subst.ml 10849 2008-04-25 15:55:16Z soubiran $ *) +(* $Id: mod_subst.ml 11924 2009-02-13 13:51:54Z soubiran $ *) open Pp open Util @@ -250,11 +250,11 @@ let join (subst1 : substitution) (subst2 : substitution) = try let res = match resolve with - Some res -> res - | None -> + |None -> begin match resolve' with None -> raise BothSubstitutionsAreIdentitySubstitutions - | Some res -> raise (ChangeDomain res) + | Some res -> raise (ChangeDomain res) end + | Some res -> res in Some (List.map @@ -356,23 +356,23 @@ let update_subst subst1 subst2 = | MPI mp -> mp in match mp with - | MPbound mbid -> ((MBI mbid),newmp)::l - | MPself msid -> ((MSI msid),newmp)::l - | _ -> ((MPI mp),newmp)::l + | MPbound mbid -> ((MBI mbid),newmp,resolve)::l + | MPself msid -> ((MSI msid),newmp,resolve)::l + | _ -> ((MPI mp),newmp,resolve)::l in let subst_mbi = Umap.fold subst_inv subst2 [] in let alias_subst key (mp,resolve) sub= let newsetkey = match key with | MPI mp1 -> - let compute_set_newkey l (k,mp') = + let compute_set_newkey l (k,mp',resolve) = let mp_from_key = match k with | MBI msid -> MPbound msid | MSI msid -> MPself msid | MPI mp -> mp in let new_mp1 = replace_mp_in_mp mp_from_key mp' mp1 in - if new_mp1 == mp1 then l else (MPI new_mp1)::l + if new_mp1 == mp1 then l else (MPI new_mp1,resolve)::l in begin match List.fold_left compute_set_newkey [] subst_mbi with @@ -384,7 +384,7 @@ let update_subst subst1 subst2 = match newsetkey with | None -> sub | Some l -> - List.fold_left (fun s k -> Umap.add k (mp,resolve) s) + List.fold_left (fun s (k,r) -> Umap.add k (mp,r) s) sub l in Umap.fold alias_subst subst1 empty_subst diff --git a/kernel/modops.ml b/kernel/modops.ml index 25a11c69..949a7402 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modops.ml 11514 2008-10-28 13:39:02Z soubiran $ i*) +(*i $Id: modops.ml 11923 2009-02-13 12:20:27Z soubiran $ i*) (*i*) open Util @@ -272,9 +272,9 @@ let rec eval_struct env = function (subst_key (map_msid msid mp) sub_alias) (map_msid msid mp) | _ -> sub_alias in - let sub_alias1 = update_subst sub_alias - (map_mbid farg_id mp (None)) in - let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in + let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in + let sub_alias1 = update_subst sub_alias + (map_mbid farg_id mp (Some resolve)) in eval_struct env (subst_struct_expr (join sub_alias1 (map_mbid farg_id mp (Some resolve))) fbody_b) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index fbb05a2d..7a2db86b 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: safe_typing.ml 11453 2008-10-15 14:42:34Z soubiran $ *) +(* $Id: safe_typing.ml 12187 2009-06-13 19:36:59Z msozeau $ *) open Util open Names @@ -113,7 +113,7 @@ let add_constraints cst senv = (* 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 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 -- cgit v1.2.3