diff options
| -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 | ||||
| -rw-r--r-- | parsing/printer.ml | 67 | ||||
| -rw-r--r-- | parsing/printer.mli | 2 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Int31.v | 2 |
7 files changed, 140 insertions, 96 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index a2ece57c4c..880e978afb 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 13ef7386f0..30cec7ed94 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 c5b4800d56..ca41c2d7d9 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 35bb1267ab..a3df35ad5a 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 diff --git a/parsing/printer.ml b/parsing/printer.ml index 521dad6a0d..8ef206649e 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -491,44 +491,39 @@ let prterm = pr_lconstr (* spiwack: printer function for sets of Environ.assumption. It is used primarily by the Print Assumption command. *) -exception EmptyAssumptionSet - let pr_assumptionset env s = - if (Environ.AssumptionSet.is_empty s) then + if (Environ.ContextObjectMap.is_empty s) then str "Closed under the global context" else - let (vars, axioms) = Environ.AssumptionSet.partition - (function |Variable _ -> true | _ -> false) - s + let (vars,axioms) = + Environ.ContextObjectMap.fold (fun o typ r -> + let (v,a) = r in + match o with + | Variable id -> ( Some ( + Option.default (fnl ()) v + ++ str (string_of_id id) + ++ str " : " + ++ pr_ltype typ + ++ fnl () + ) + , + a ) + | Axiom kn -> ( v , + Some ( + Option.default (fnl ()) a + ++ (pr_constant env kn) + ++ str " : " + ++ pr_ltype typ + ++ fnl () + ) + ) + ) + s (None,None) in - (if Environ.AssumptionSet.is_empty vars then - mt () - else - str "Section Variables:" ++ - (Environ.AssumptionSet.fold - (function Variable (id,typ ) -> - (fun b -> b++str (string_of_id id) - ++str " : " - ++pr_ltype typ - ++fnl ()) - | _ -> anomaly - "Printer.pr_assumptionset: failure of partition (Variable)") - vars (fnl ())) - ) - ++ fnl () - ++ - if Environ.AssumptionSet.is_empty axioms then - mt () - else - str "Axioms:" ++ - (Environ.AssumptionSet.fold - (function Axiom (cst, typ) -> - (fun b -> b++(pr_constant env cst) - ++str " : " - ++pr_ltype typ - ++fnl ()) - | _ -> anomaly - "Printer.pr_assumptionset: failure of partition (Axiom)") - axioms - (fnl ())) + let (vars,axioms) = + ( Option.map (fun p -> str "Section Variables:" ++ p) vars , + Option.map (fun p -> str "Axioms:" ++ p) axioms + ) + in + (Option.default (mt ()) vars) ++ (Option.default (mt ()) axioms) diff --git a/parsing/printer.mli b/parsing/printer.mli index 338bff3b3a..262826ac8c 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -124,7 +124,7 @@ val prterm : constr -> std_ppcmds (* = pr_lconstr *) (* spiwack: printer function for sets of Environ.assumption. It is used primarily by the Print Assumption command. *) -val pr_assumptionset : env -> Environ.AssumptionSet.t -> std_ppcmds +val pr_assumptionset : env -> Term.types Environ.ContextObjectMap.t ->std_ppcmds type printer_pr = { diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index ba40ffd87c..b3a985b63b 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -43,7 +43,7 @@ Inductive int31 : Type := I31 : nfun digits size int31. (* spiwack: Registration of the type of integers, so that the matchs in the functions below perform dynamic decompilation (otherwise some segfault - occur when they are applied to one non-closed term and one closed term *) + occur when they are applied to one non-closed term and one closed term). *) Register digits as int31 bits in "coq_int31" by True. Register int31 as int31 type in "coq_int31" by True. |