First attempt at making Print Assumption compatible with opaque modules (fix #2168)

 We replace Global.lookup_constant by our own code that looks for a module
 and enters its implementation. This is still preliminary work, I would prefer
 to understand more completely the part about module substitutions when
 entering an applied functor. But this code already appears to work quite well.
 Anyway, since we only search for constants, we don't need to reconstitute a
 100% accurate environment, as long as the same objects are in it.

 Note:

  - Digging inside module structures is slower than just using
    Global.lookup_constant. Hence we try to avoid it as long as we could.
    Only in front of axioms (or in front of constant unknown to Global)
    do we check whether we have an inner-module implementation for this
    constant. There is some memoization of the search for internal
    structure_body out of a module_path.

  - In case of inner-module axioms, we might not be able to print
    its type, but only its long name.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14600 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 141 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index a0b7d2cbce..59336a7624 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 *)
-
-
-