diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 141 | ||||
| -rw-r--r-- | kernel/environ.mli | 17 | ||||
| -rw-r--r-- | kernel/kernel.mllib | 2 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 16 |
4 files changed, 1 insertions, 175 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index a0b7d2cbc..59336a762 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -528,144 +528,3 @@ fun env field value -> 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 Declarations.constant_has_body cb - && (Declarations.is_opaque cb || not (Cpred.mem kn knst)) - && add_opaque - then - do_type (Opaque kn) - else (s,acc) - in - match Declarations.body_of_constant cb 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 *) - - - diff --git a/kernel/environ.mli b/kernel/environ.mli index af1e17591..aa6f52128 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -228,20 +228,3 @@ val unregister : env -> field -> env val register : env -> field -> Retroknowledge.entry -> env - -(** a few declarations for the "Print Assumption" command - @author spiwack *) -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 (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/kernel.mllib b/kernel/kernel.mllib index a628e5cfe..8c1dd53ad 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -29,4 +29,4 @@ Safe_typing Vm Csymtable -Vconv
\ No newline at end of file +Vconv diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index e4cb78bde..c620d8dd2 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -197,22 +197,6 @@ let update_resolver f senv = { senv with modinfo = { mi with resolver = f mi.resolver }} -(*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) |