diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 64 | ||||
| -rw-r--r-- | kernel/environ.mli | 15 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 2 |
3 files changed, 45 insertions, 36 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 4266602983..faf0757127 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -528,14 +528,18 @@ fun env field value -> } +(**************************************************************) (* spiwack: the following definitions are used by the function - needed_assumption which gives as an output the set of all + [assumptions] which gives as an output the set of all axioms and sections variables on which a given term depends in a context (expectingly the Global context) *) + type assumption = - | Variable of identifier*constr - | Axiom of constant*constr + | Variable of identifier*constr (* A section variable and its type *) + | Axiom of constant*constr (* An axiom and its type*) + +(* Defines a set of [assumption] *) module OrderedAssumption = struct type t = assumption @@ -544,45 +548,43 @@ end module AssumptionSet = Set.Make (OrderedAssumption) -(* definition for redability purposes *) +(* infix definition of set-union for redability purposes *) let ( ** ) s1 s2 = AssumptionSet.union s1 s2 -let rec needed_assumptions t env = - (* goes recursively into the terms to see if it depends on assumptions - the 3 important cases are : Var _ which means that the term refers - to a section variable or a "Let" definition, - Rel _ which means the term is a variable - which has been bound earlier by a Lambda or a Prod (returns [] ) - Const _ where we need to first unfold +let rec assumptions t env = + (* Goes recursively into the terms to see if it depends on assumptions + the 3 important cases are : - Const _ where we need to first unfold the constant and return the needed assumptions of its body in the - environnement *) + environment, + - Rel _ which means the term is a variable + which has been bound earlier by a Lambda or a Prod (returns [] ), + - Var _ which means that the term refers + to a section variable or a "Let" definition, in the former it is + an assumption of [t], in the latter is must be unfolded like a Const. + The other cases are straightforward recursion.*) match kind_of_term t with - | Var id -> (* a var can be either a variable, or a "Let" definition.*) + | Var id -> (* a Var can be either a variable, or a "Let" definition.*) (match named_body id env with | None -> AssumptionSet.singleton (Variable (id,named_type id env)) - | Some bdy -> needed_assumptions bdy env) - | Meta _ | Evar _ -> assert false + | Some bdy -> assumptions bdy env) + | Meta _ | Evar _ -> Util.anomaly "Environ.assumption: does not expect a meta or an evar" | Cast (e1,_,e2) | Prod (_,e1,e2) | Lambda (_,e1,e2) -> - (needed_assumptions e1 env)**(needed_assumptions e2 env) - | LetIn (_,e1,e2,e3) ->(needed_assumptions e1 env)** - (needed_assumptions e2 env)** - (needed_assumptions e3 env) - | App (e1, e_array) -> (needed_assumptions e1 env)** - (Array.fold_right (fun e -> fun s -> - (needed_assumptions e env)**s) + (assumptions e1 env)**(assumptions e2 env) + | LetIn (_,e1,e2,e3) ->(assumptions e1 env)** + (assumptions e2 env)** + (assumptions e3 env) + | App (e1, e_array) -> (assumptions e1 env)** + (Array.fold_right (fun e s -> (assumptions e env)**s) e_array AssumptionSet.empty) - | Case (_,e1,e2,e_array) -> (needed_assumptions e1 env)** - (needed_assumptions e2 env)** - (Array.fold_right (fun e -> fun s -> - (needed_assumptions e env)**s) + | Case (_,e1,e2,e_array) -> (assumptions e1 env)** + (assumptions e2 env)** + (Array.fold_right (fun e s -> (assumptions e env)**s) e_array AssumptionSet.empty) | Fix (_,(_, e1_array, e2_array)) | CoFix (_,(_,e1_array, e2_array)) -> - Array.fold_right (fun e -> fun s -> - (needed_assumptions e env)**s) + Array.fold_right (fun e s -> (assumptions e env)**s) e1_array - (Array.fold_right (fun e -> fun s -> - (needed_assumptions e env)**s) + (Array.fold_right (fun e s -> (assumptions e env)**s) e2_array AssumptionSet.empty) | Const kn -> let cb = lookup_constant kn env in @@ -594,7 +596,7 @@ let rec needed_assumptions t env = | NonPolymorphicType t -> t in AssumptionSet.singleton (Axiom (kn,ctype)) - | Some body -> needed_assumptions (Declarations.force body) env) + | Some body -> assumptions (Declarations.force body) env) | _ -> AssumptionSet.empty (* closed atomic types + rel *) (* /spiwack *) diff --git a/kernel/environ.mli b/kernel/environ.mli index 293c55a691..bfbb5dd3c2 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -231,15 +231,22 @@ val unregister : env -> field -> env val register : env -> field -> Retroknowledge.entry -> env + + +(******************************************************************) (* spiwack: a few declarations for the "Print Assumption" command *) + type assumption = - | Variable of identifier*Term.constr - | Axiom of constant*Term.constr + | Variable of identifier*Term.constr (* A section variable and its type *) + | Axiom of constant*Term.constr (* An axiom and its type*) -module OrderedAssumption : Set.OrderedType with type t = assumption +(* AssumptionSet.t is a set of [assumption] *) +module OrderedAssumption : Set.OrderedType with type t = assumption module AssumptionSet : Set.S with type elt = assumption -val needed_assumptions : constr -> env -> AssumptionSet.t +(* collects all the assumptions on which a term relies (together with + their type *) +val assumptions : constr -> env -> AssumptionSet.t diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d65caf7cab..91e4c73fc9 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -109,7 +109,7 @@ let env_of_senv = env_of_safe_env (* terms which are closed under the environnement env, i.e terms which only depends on constant who are themselves closed *) let closed env term = - AssumptionSet.is_empty (needed_assumptions env term) + AssumptionSet.is_empty (assumptions 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 |