diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 2 | ||||
| -rw-r--r-- | kernel/environ.ml | 148 | ||||
| -rw-r--r-- | kernel/environ.mli | 13 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 2 |
4 files changed, 107 insertions, 58 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index a2ece57c4..880e978af 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1190,7 +1190,7 @@ value coq_interprete Instruct (DIV21INT31) { print_instr("DIV21INT31"); /* spiwack: takes three int31 (the two first ones represent an - int62) and perfoms the euclidian division of the + int62) and performs the euclidian division of the int62 by the int31 */ uint64 bigint; bigint = UI64_of_value(accu); diff --git a/kernel/environ.ml b/kernel/environ.ml index 13ef7386f..30cec7ed9 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -554,25 +554,46 @@ fun env field value -> axioms and sections variables on which a given term depends in a context (expectingly the Global context) *) -type assumption = - | Variable of identifier*constr (* A section variable and its type *) - | Axiom of constant*constr (* An axiom and its type*) +type context_object = + | Variable of identifier (* A section variable or a Let definition *) + | Axiom of constant (* An axiom or a constant. *) (* Defines a set of [assumption] *) -module OrderedAssumption = +module OrderedContextObject = struct - type t = assumption - let compare = compare + 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 *) + | Variable _ , Axiom _ -> -1 + | Axiom _ , Variable _ -> 1 end -module AssumptionSet = Set.Make (OrderedAssumption) - -(* infix definition of set-union for redability purposes *) -let ( ** ) s1 s2 = AssumptionSet.union s1 s2 - -let rec assumptions t env = - (* Goes recursively into the terms to see if it depends on assumptions +module ContextObjectSet = Set.Make (OrderedContextObject) +module ContextObjectMap = Map.Make (OrderedContextObject) + + +let assumptions (* t env *) = + (* 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, @@ -581,44 +602,73 @@ let rec assumptions t env = - 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.*) - (match named_body id env with - | None -> - AssumptionSet.singleton (Variable (id,named_type id env)) - | Some bdy -> assumptions bdy env) - | Meta _ | Evar _ -> Util.anomaly "Environ.assumption: does not expect a meta or an evar" + 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) -> - (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) -> (assumptions e1 env)** - (assumptions e2 env)** - (Array.fold_right (fun e s -> (assumptions e env)**s) - e_array AssumptionSet.empty) + ((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 s -> (assumptions e env)**s) - e1_array - (Array.fold_right (fun e s -> (assumptions e env)**s) - e2_array AssumptionSet.empty) - | Const kn -> - 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 - AssumptionSet.singleton (Axiom (kn,ctype)) - | Some body -> assumptions (Declarations.force body) env) - | _ -> AssumptionSet.empty (* closed atomic types + rel *) - + ((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 + 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 + + 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 c5b4800d5..ca41c2d7d 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -241,17 +241,16 @@ val register : env -> field -> Retroknowledge.entry -> env (******************************************************************) (* spiwack: a few declarations for the "Print Assumption" command *) -type assumption = - | Variable of identifier*Term.constr (* A section variable and its type *) - | Axiom of constant*Term.constr (* An axiom and its type*) - +type context_object = + | Variable of identifier (* A section variable or a Let definition *) + | Axiom of constant (* An axiom or a constant. *) (* AssumptionSet.t is a set of [assumption] *) -module OrderedAssumption : Set.OrderedType with type t = assumption -module AssumptionSet : Set.S with type elt = 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 -> AssumptionSet.t +val assumptions : constr -> env -> Term.types ContextObjectMap.t diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 35bb1267a..a3df35ad5 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -110,7 +110,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 (assumptions env term) + ContextObjectMap.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 |