From 300293c119981054c95182a90c829058530a6b6f Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 25 Dec 2011 13:19:42 +0100 Subject: Imported Upstream version 8.3.pl3 --- kernel/environ.ml | 145 +----------------------------------------------------- 1 file changed, 2 insertions(+), 143 deletions(-) (limited to 'kernel/environ.ml') diff --git a/kernel/environ.ml b/kernel/environ.ml index 935faae6..e6fafce9 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* in Retroknowledge.add_field retroknowledge_with_reactive_info field value } - - -(**************************************************************) -(* spiwack: the following definitions are used by the function - [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 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 = -struct - type t = context_object - let compare x y = - match x , y with - | Variable i1 , Variable i2 -> id_ord i1 i2 - | 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 ?(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 - (* This function eases memoization, by checking if an object is already - stored before trying and applying a function. - If the object is there, the function is not fired (we are in a - particular case where memoized object don't need a treatment at all). - If the object isn't there, it is stored and the function is fired*) - let try_and_go o f s m = - if ContextObjectSet.mem o s then - (s,m) - else - f (ContextObjectSet.add o s) m - in - let identity2 s m = (s,m) in - (* Goes recursively into the term 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 - 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. - Calls to the environment are memoized, thus avoiding to explore - the DAG of the environment as if it was a tree (can cause - exponential behavior and prevent the algorithm from terminating - in reasonable time). [s] is a set of [context_object], representing - the object already visited.*) - let rec aux t env s acc = - match kind_of_term t with - | Var id -> aux_memoize_id id env s acc - | Meta _ | Evar _ -> - Util.anomaly "Environ.assumption: does not expect a meta or an evar" - | Cast (e1,_,e2) | Prod (_,e1,e2) | Lambda (_,e1,e2) -> - ((aux e1 env)**(aux e2 env)) s acc - | LetIn (_,e1,e2,e3) -> ((aux e1 env)** - (aux e2 env)** - (aux e3 env)) - s acc - | App (e1, e_array) -> ((aux e1 env)** - (Array.fold_right - (fun e f -> (aux e env)**f) - e_array identity2)) - s acc - | Case (_,e1,e2,e_array) -> ((aux e1 env)** - (aux e2 env)** - (Array.fold_right - (fun e f -> (aux e env)**f) - e_array identity2)) - s acc - | Fix (_,(_, e1_array, e2_array)) | CoFix (_,(_,e1_array, e2_array)) -> - ((Array.fold_right - (fun e f -> (aux e env)**f) - e1_array identity2) ** - (Array.fold_right - (fun e f -> (aux e env)**f) - e2_array identity2)) - s acc - | Const kn -> aux_memoize_kn kn env s acc - | _ -> (s,acc) (* closed atomic types + rel *) - - and add_id id env s acc = - (* a Var can be either a variable, or a "Let" definition.*) - match lookup_named id env with - | (_,None,t) -> - (s,ContextObjectMap.add (Variable id) t acc) - | (_,Some bdy,_) -> aux bdy env s acc - - and aux_memoize_id id env = - try_and_go (Variable id) (add_id id env) - - and add_kn kn env s acc = - let cb = lookup_constant kn env in - 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 - fun t env -> - snd (aux t env (ContextObjectSet.empty) (ContextObjectMap.empty)) - -(* /spiwack *) - - - -- cgit v1.2.3