closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)

 For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a

4 files changed, 32 insertions, 33 deletions

diff --git a/kernel/closure.ml b/kernel/cClosure.ml
index 04c1bb657..d475f097c 100644
--- a/kernel/closure.ml
+++ b/kernel/cClosure.ml
@@ -154,7 +154,7 @@ module RedFlags = (struct
     | ETA -> { red with r_eta = false }
     | DELTA -> { red with r_delta = false }
     | CONST kn ->
- 	let (l1,l2) = red.r_const in
+	let (l1,l2) = red.r_const in
 	{ red with r_const = l1, Cpred.remove kn l2 }
     | MATCH -> { red with r_match = false }
     | FIX -> { red with r_fix = false }
@@ -187,7 +187,7 @@ module RedFlags = (struct
     | DELTA -> (* Used for Rel/Var defined in context *)
 	incr_cnt red.r_delta delta
 
-  let red_projection red p = 
+  let red_projection red p =
     if Projection.unfolded p then true
     else red_set red (fCONST (Projection.constant p))
 
@@ -238,7 +238,7 @@ type table_key = constant puniverses tableKey
 
 let eq_pconstant_key (c,u) (c',u') =
   eq_constant_key c c' && Univ.Instance.equal u u'
-  
+
 module IdKeyHash =
 struct
   open Hashset.Combine
@@ -261,7 +261,7 @@ type 'a infos_cache = {
   i_rels : constr option array;
   i_tab : 'a KeyTable.t }
 
-and 'a infos = { 
+and 'a infos = {
   i_flags : reds;
   i_cache : 'a infos_cache }
 
@@ -320,7 +320,7 @@ let defined_rels flags env =
 (*  else (0,[])*)
 
 let create mk_cl flgs env evars =
-  let cache = 
+  let cache =
     { i_repr = mk_cl;
       i_env = env;
       i_sigma = evars;
@@ -670,7 +670,7 @@ let rec zip m stk =
     | ZcaseT(ci,p,br,e)::s ->
         let t = FCaseT(ci, p, m, br, e) in
         zip {norm=neutr m.norm; term=t} s
-    | Zproj (i,j,cst) :: s -> 
+    | Zproj (i,j,cst) :: s ->
         zip {norm=neutr m.norm; term=FProj(Projection.make cst true,m)} s
     | Zfix(fx,par)::s ->
         zip fx (par @ append_stack [|m|] s)
@@ -777,7 +777,7 @@ let rec try_drop_parameters depth n argstk =
           let aft = Array.sub args n (q-n) in
           reloc_rargs depth (append_stack aft s)
     | Zshift(k)::s -> try_drop_parameters (depth-k) n s
-    | [] -> 
+    | [] ->
 	if Int.equal n 0 then []
 	else raise Not_found
     | _ -> assert false
@@ -786,23 +786,23 @@ let rec try_drop_parameters depth n argstk =
 let drop_parameters depth n argstk =
   try try_drop_parameters depth n argstk
   with Not_found ->
-  (* we know that n < stack_args_size(argstk) (if well-typed term) *) 
+  (* we know that n < stack_args_size(argstk) (if well-typed term) *)
   anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor")
 
 (** [eta_expand_ind_stack env ind c s t] computes stacks corresponding
-    to the conversion of the eta expansion of t, considered as an inhabitant 
+    to the conversion of the eta expansion of t, considered as an inhabitant
     of ind, and the Constructor c of this inductive type applied to arguments
     s.
     @assumes [t] is an irreducible term, and not a constructor. [ind] is the inductive
-    of the constructor term [c] 
-    @raises Not_found if the inductive is not a primitive record, or if the 
+    of the constructor term [c]
+    @raises Not_found if the inductive is not a primitive record, or if the
     constructor is partially applied.
  *)
 let eta_expand_ind_stack env ind m s (f, s') =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
     | Some (Some (_,projs,pbs)) when
-	mib.Declarations.mind_finite == Decl_kinds.BiFinite -> 
+	mib.Declarations.mind_finite == Decl_kinds.BiFinite ->
 	(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
 	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
       let pars = mib.Declarations.mind_nparams in
@@ -812,12 +812,12 @@ let eta_expand_ind_stack env ind m s (f, s') =
       let argss = try_drop_parameters depth pars args in
       let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
 					 term = FProj (Projection.make p true, right) }) projs in
-	argss, [Zapp hstack]	
+	argss, [Zapp hstack]
     | _ -> raise Not_found (* disallow eta-exp for non-primitive records *)
 
 let rec project_nth_arg n argstk =
   match argstk with
-  | Zapp args :: s -> 
+  | Zapp args :: s ->
       let q = Array.length args in
 	if n >= q then project_nth_arg (n - q) s
 	else (* n < q *) args.(n)
@@ -872,7 +872,7 @@ let rec knh info m stk =
           (match try Some (lookup_projection p (info_env info)) with Not_found -> None with
 	  | None -> (m, stk)
 	  | Some pb ->
-	     knh info c (Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, 
+	     knh info c (Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg,
 				Projection.constant p)
 			 :: zupdate m stk))
 	else (m,stk)
@@ -974,8 +974,8 @@ let rec zip_term zfun m stk =
         let t = mkCase(ci, zfun (mk_clos e p), m,
 		       Array.map (fun b -> zfun (mk_clos e b)) br) in
         zip_term zfun t s
-    | Zproj(_,_,p)::s -> 
-        let t = mkProj (Projection.make p true, m) in 
+    | Zproj(_,_,p)::s ->
+        let t = mkProj (Projection.make p true, m) in
 	zip_term zfun t s
     | Zfix(fx,par)::s ->
         let h = mkApp(zip_term zfun (zfun fx) par,[|m|]) in
@@ -1055,18 +1055,17 @@ let oracle_of_infos infos = Environ.oracle infos.i_cache.i_env
 
 let env_of_infos infos = infos.i_cache.i_env
 
-let infos_with_reds infos reds = 
+let infos_with_reds infos reds =
   { infos with i_flags = reds }
 
-let unfold_reference info key = 
+let unfold_reference info key =
   match key with
   | ConstKey (kn,_) ->
     if red_set info.i_flags (fCONST kn) then
-      ref_value_cache info key  
+      ref_value_cache info key
     else None
-  | VarKey i -> 
+  | VarKey i ->
     if red_set info.i_flags (fVAR i) then
       ref_value_cache info key
     else None
   | _ -> ref_value_cache info key
-  
diff --git a/kernel/closure.mli b/kernel/cClosure.mli
index 76145e3f8..077756ac7 100644
--- a/kernel/closure.mli
+++ b/kernel/cClosure.mli
@@ -66,7 +66,7 @@ module type RedFlagsSig = sig
 
   (** Tests if a reduction kind is set *)
   val red_set : reds -> red_kind -> bool
-    
+
   (** This tests if the projection is in unfolded state already or
       is unfodable due to delta. *)
   val red_projection : reds -> projection -> bool
@@ -95,7 +95,7 @@ val unfold_red : evaluable_global_reference -> reds
 type table_key = constant puniverses tableKey
 
 type 'a infos_cache
-type 'a infos = { 
+type 'a infos = {
   i_flags : reds;
   i_cache : 'a infos_cache }
 
@@ -204,16 +204,16 @@ val whd_val : clos_infos -> fconstr -> constr
 val whd_stack :
   clos_infos -> fconstr -> stack -> fconstr * stack
 
-(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding 
-    to the conversion of the eta expansion of t, considered as an inhabitant 
+(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding
+    to the conversion of the eta expansion of t, considered as an inhabitant
     of ind, and the Constructor c of this inductive type applied to arguments
     s.
     @assumes [t] is a rigid term, and not a constructor. [ind] is the inductive
-    of the constructor term [c] 
-    @raises Not_found if the inductive is not a primitive record, or if the 
+    of the constructor term [c]
+    @raises Not_found if the inductive is not a primitive record, or if the
     constructor is partially applied.
  *)
-val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> 
+val eta_expand_ind_stack : env -> inductive -> fconstr -> stack ->
    (fconstr * stack) -> stack * stack
 
 (** Conversion auxiliary functions to do step by step normalisation *)
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 1e132e3ab..15f213ce9 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -25,7 +25,7 @@ Nativelambda
 Nativecode
 Nativelib
 Environ
-Closure
+CClosure
 Reduction
 Nativeconv
 Type_errors
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 67b05e526..6c664f791 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -21,7 +21,7 @@ open Names
 open Term
 open Vars
 open Environ
-open Closure
+open CClosure
 open Esubst
 open Context.Rel.Declaration
 
@@ -318,7 +318,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	   convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
        with NotConvertible ->
            (* else the oracle tells which constant is to be expanded *)
-	 let oracle = Closure.oracle_of_infos infos in
+	 let oracle = CClosure.oracle_of_infos infos in
          let (app1,app2) =
            if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then
 	     match unfold_reference infos fl1 with
@@ -537,7 +537,7 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
   else raise NotConvertible
 
 let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
-  let reds = Closure.RedFlags.red_add_transparent betaiotazeta trans in
+  let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
   let infos = create_clos_infos ~evars reds env in
   ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs