Cleanup, use Util list functions when possible

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

4 files changed, 31 insertions, 307 deletions

diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 1989e7dcf0..9b174967fb 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -13,46 +13,15 @@ open Pp
 open Util
 open Subtac_utils
 
-let reverse_array arr = 
-  Array.of_list (List.rev (Array.to_list arr))
-    
 let trace s = 
   if !Options.debug then (msgnl s; msgerr s)
   else ()
 
-(** Utilities to find indices in lists *)
-let list_index x l =
-  let rec aux i = function
-      k :: tl -> if k = x then i else aux (succ i) tl
-    | [] -> raise Not_found
-  in aux 0 l
-
-let list_assoc_index x l =
-  let rec aux i = function
-      (k, _, v) :: tl -> if k = x then i else aux (succ i) tl
-    | [] -> raise Not_found
-  in aux 0 l
-
-let rec list_split_at n l = 
-  match n with
-    | 0 -> ([], l)
-    | n' ->
-	match l with
-	  | [] -> assert(false)
-	  | hd :: tl -> let (l, r) = list_split_at (pred n') tl in
-	      (hd :: l, r)
-
 (** Substitute evar references in t using De Bruijn indices, 
   where n binders were passed through. *)
 let subst_evar_constr evs n t = 
   let seen = ref Intset.empty in
-  let evar_info id = 
-    let rec aux i = function
-	(k, x) :: tl -> 
-	  if k = id then x else aux (succ i) tl
-      | [] -> raise Not_found
-    in aux 0 evs
-  in
+  let evar_info id = List.assoc id evs in
   let rec substrec depth c = match kind_of_term c with
     | Evar (k, args) ->
 	let (id, idstr), hyps, chop, _, _ = 
@@ -66,7 +35,7 @@ let subst_evar_constr evs n t =
 	  *)
 	let args = 
 	  let n = match chop with None -> 0 | Some c -> c in 
-	  let (l, r) = list_split_at n (List.rev (Array.to_list args)) in
+	  let (l, r) = list_chop n (List.rev (Array.to_list args)) in
 	    List.rev r
 	in
 	let args =
@@ -94,10 +63,7 @@ let subst_evar_constr evs n t =
 (** Substitute variable references in t using De Bruijn indices, 
   where n binders were passed through. *)
 let subst_vars acc n t = 
-  let var_index id = 
-    let idx = list_index id acc in
-      idx + 1
-  in
+  let var_index id = Util.list_index id acc in
   let rec substrec depth c = match kind_of_term c with
     | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c)
     | _ -> map_constr_with_binders succ substrec depth c
@@ -131,12 +97,9 @@ let etype_of_evar evs hyps concl =
 
 open Tacticals
     
-let rec take n l = 
-  if n = 0 then [] else List.hd l :: take (pred n) (List.tl l)    
-
 let trunc_named_context n ctx = 
   let len = List.length ctx in
-    take (len - n) ctx
+    list_firstn (len - n) ctx
   
 let rec chop_product n t = 
   if n = 0 then Some t
@@ -200,11 +163,7 @@ let eterm_obligations name nclen isevars evm fs t tycon =
      with _ -> ());
     Array.of_list (List.rev evars), t'
 
-let mkMetas n = 
-  let rec aux i acc = 
-    if i > 0 then aux (pred i) (Evarutil.mk_new_meta () :: acc)
-    else acc
-  in aux n []
+let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n
 
 (* let eterm evm t (tycon : types option) =  *)
 (*   let t, tycon, evs = eterm_term evm t tycon in *)
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index f489325a11..b5deafc5f8 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1558,14 +1558,7 @@ let inh_conv_coerce_to_tycon loc env isevars j tycon =
     | None -> j
 
 let out_ind = function IsInd (_, IndType(x, y)) -> (x, y) | _ -> assert(false)
-  
-let list_mapi f l = 
-  let rec aux n = function
-      [] -> []
-    | hd :: tl -> f n hd :: aux (succ n) tl
-  in aux 0 l
 	       
-
 let string_of_name name = 
   match name with
     | Anonymous -> "anonymous"
@@ -1596,7 +1589,6 @@ let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |])
 let mk_JMeq typ x typ' y = mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
 let mk_JMeq_refl typ x = mkApp (Lazy.force Subtac_utils.jmeq_refl, [| typ; x |])
     
-
 let hole = RHole (dummy_loc, Evd.QuestionMark true)
 
 let context_of_arsign l =
@@ -1713,21 +1705,6 @@ let vars_of_ctx ctx =
 	      | Name n -> n, RVar (dummy_loc, n) :: vars)
       ctx (id_of_string "vars_of_ctx: error", [])
   in List.rev y
-      
-let unsafe_fold_right f = function
-    hd :: tl -> List.fold_right f tl hd
-  | [] -> raise (Invalid_argument "unsafe_fold_right")
-
-let mk_conj l =
-  let conj_typ = Lazy.force Subtac_utils.and_typ in
-    unsafe_fold_right
-      (fun c conj ->
-	 mkApp (conj_typ, [| c ; conj |]))
-      l
-
-let mk_not c =
-  let notc = Lazy.force Subtac_utils.not_ref in
-    mkApp (notc, [| c |])
 
 let rec is_included x y = 
   match x, y with
@@ -1763,7 +1740,6 @@ let build_ineqs prevpatterns pats liftsign =
 			  succ n, (* nth pattern *)
 			  mkApp (Lazy.force eq_ind,
 				[| lift (lens + liftsign) ppat_ty ;
-(* 				   ppat_c ;  *)
 				   liftn liftsign (succ lens) ppat_c ;
 				   lift len' curpat_c |]) :: 
 			    List.map 
@@ -1801,11 +1777,6 @@ let lift_rel_contextn n k sign =
   in
   liftrec (rel_context_length sign + k) sign
 
-let lift_arsign n (x, y) =
-  match lift_rel_context n (x :: y) with
-    | x :: y -> x, y
-    | [] -> assert(false)
-
 let constrs_of_pats typing_fun tycon env isevars eqns tomatchs sign neqs eqs arity =
   let i = ref 0 in
   let (x, y, z) = 
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 9a11f60b3e..b557b40569 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -264,11 +264,30 @@ let mk_ex_pi1 a b c =
 let mk_ex_pi2 a b c =
   mkApp (Lazy.force ex_pi2, [| a; b; c |])
     
-
 let mkSubset name typ prop = 
   mkApp ((Lazy.force sig_).typ,
 	 [| typ; mkLambda (name, typ, prop) |])
 
+let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |])
+let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |])
+let mk_JMeq typ x typ' y = mkApp (Lazy.force jmeq_ind, [| typ; x ; typ'; y |])
+let mk_JMeq_refl typ x = mkApp (Lazy.force jmeq_refl, [| typ; x |])
+
+let unsafe_fold_right f = function
+    hd :: tl -> List.fold_right f tl hd
+  | [] -> raise (Invalid_argument "unsafe_fold_right")
+
+let mk_conj l =
+  let conj_typ = Lazy.force and_typ in
+    unsafe_fold_right
+      (fun c conj ->
+	 mkApp (conj_typ, [| c ; conj |]))
+      l
+
+let mk_not c =
+  let notc = Lazy.force not_ref in
+    mkApp (notc, [| c |])
+
 let and_tac l hook =
   let andc = Coqlib.build_coq_and () in      
   let rec aux ((accid, goal, tac, extract) as acc) = function
@@ -318,221 +337,7 @@ let destruct_ex ext ex =
   in aux ex ext
 
 open Rawterm
-
-let rec concatMap f l = 
-  match l with
-      hd :: tl -> f hd @ concatMap f tl      
-    | [] -> []
 	
-let list_mapi f = 
-  let rec aux i = function 
-      hd :: tl -> f i hd :: aux (succ i) tl 
-    | [] -> []
-  in aux 0
-
-(*
-let make_discr (loc, po, tml, eqns) =
-  let mkHole = RHole (dummy_loc, InternalHole) in
-  
-  let rec vars_of_pat = function
-      RPatVar (loc, n) -> (match n with Anonymous -> [] | Name n -> [n])
-    | RPatCstr (loc, csrt, pats, _) -> 
-	concatMap vars_of_pat pats
-  in
-  let rec constr_of_pat l = function 
-      RPatVar (loc, n) -> 
-	(match n with 
-	     Anonymous -> 
-	       let n = next_name_away_from "x" l in
-		 RVar n, (n :: l)
-	   | Name n -> RVar n, l)
-    | RPatCstr (loc, csrt, pats, _) -> 
-	let (args, vars) =
-	  List.fold_left
-	    (fun (args, vars) x ->
-	       let c, vars = constr_of_pat vars x in
-		 c :: args, vars)
-	    ([], l) pats
-	in		 
-	  RApp ((RRef (dummy_loc, ConstructRef cstr)), args), vars
-  in
-  let rec constr_of_pat l = function 
-      RPatVar (loc, n) -> 
-	(match n with 
-	     Anonymous -> 
-	       let n = next_name_away_from "x" l in
-		 RVar n, (n :: l)
-	   | Name n -> RVar n, l)
-    | RPatCstr (loc, csrt, pats, _) -> 
-	let (args, vars) =
-	  List.fold_left
-	    (fun (args, vars) x ->
-	       let c, vars = constr_of_pat vars x in
-		 c :: args, vars)
-	    ([], l) pats
-	in		 
-	  RApp ((RRef (dummy_loc, ConstructRef cstr)), args), vars
-  in
-  let constrs_of_pats v l =
-    List.fold_left 
-      (fun (v, acc) x -> 
-	 let x', v' = constr_of_pat v x in
-	   (l', v' :: acc))
-      (v, []) l
-  in
-  let rec pat_of_pat l = function
-      RPatVar (loc, n) -> 
-	let n', l = match n with
-	    Anonymous -> 
-	      let n = next_name_away_from "x" l in
-		n, n :: l
-	  | Name n -> n, n :: l 
-	in
-	  RPatVar (loc, Name n'), l
-    | RPatCstr (loc, cstr, pats, (loc, alias)) ->
-	let args, vars, s = 
-	  List.fold_left (fun (args, vars) x -> 
-			    let pat', vars = pat_of_pat vars pat in
-			      pat' :: args, vars)
-	    ([], alias :: l) pats
-	in RPatCstr (loc, cstr, args, (loc, alias)), vars
-  in
-  let pats_of_pats l =
-    List.fold_left 
-      (fun (v, acc) x -> 
-	 let x', v' = pat_of_pat v x in
-	   (v', x' :: acc))
-      ([], []) l
-  in
-  let eq_of_pat p used c = 
-    let constr, vars' = constr_of_pat used p in
-    let eq = RApp (dummy_loc, RRef (dummy_loc, Lazy.force eqind_ref), [mkHole; constr; c]) in
-      vars', eq
-  in
-  let eqs_of_pats ps used cstrs =
-    List.fold_left2 
-      (fun (vars, eqs) pat c ->
-	 let (vars', eq) = eq_of_pat pat c in
-	   match eqs with 
-	       None -> Some eq 
-	     | Some eqs ->
-		 Some (RApp (dummy_loc, RRef (dummy_loc, Lazy.force and_ref), [eq, eqs])))
-      (used, None) ps cstrs
-  in
-  let quantify c l =
-    List.fold_left
-      (fun acc name -> RProd (dummy_loc, name, mkHole, acc))
-      c l
-  in
-  let quantpats = 
-    List.fold_left
-      (fun (acc, pats) ((loc, idl, cpl, c) as x) ->
-	 let vars, cpl = pats_of_pats cpl in
-	 let l', constrs = constrs_of_pats vars cpl in	   
-	 let discrs = 
-	   List.map (fun (_, _, cpl', _) -> 
-		       let qvars, eqs = eqs_of_pats cpl' l' constrs in
-		       let neg = RApp (dummy_loc, RRef (dummy_loc, Lazy.force not_ref), [out_some eqs]) in
-		       let pat_ineq = quantify qvars neg in
-			 
-		    )
-	     pats in
-	   
-			 
-
-
-	   
-	   
-
-	   (x, pat_ineq))
-  in
-    List.fold_left 
-      (fun acc ((loc, idl, cpl, c0) pat) -> 
-    
-		
-		let c' = 
-		  List.fold_left 
-		    (fun acc (n, t) ->
-		       RLambda (dummy_loc, n, mkHole, acc))
-		    c eqs_types
-		in (loc, idl, cpl, c'))
-      eqns
-  i
-*)
-(* let rewrite_cases_aux (loc, po, tml, eqns) = *)
-(*   let tml = list_mapi (fun i (c, (n, opt)) -> c,  *)
-(* 		       ((match n with *)
-(* 			    Name id -> (match c with *)
-(* 					  | RVar (_, id') when id = id' -> *)
-(* 					      Name (id_of_string (string_of_id id ^ "'")) *)
-(* 					  | _ -> n) *)
-(* 			  | Anonymous -> Name (id_of_string ("x" ^ string_of_int i))), *)
-(* 			opt)) tml  *)
-(*   in *)
-(*   let mkHole = RHole (dummy_loc, InternalHole) in *)
-(*   (\* let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqind_ref)), *\) *)
-(* (\* 		       [mkHole; c; n]) *\) *)
-(* (\*   in *\) *)
-(*   let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqdep_ind_ref)), *)
-(* 		       [mkHole; c; mkHole; n]) *)
-(*   in *)
-(*   let eqs_types =  *)
-(*     List.map *)
-(*       (fun (c, (n, _)) -> *)
-(* 	 let id = match n with Name id -> id | _ -> assert false in *)
-(* 	 let heqid = id_of_string ("Heq" ^ string_of_id id) in *)
-(* 	   Name heqid, mkeq c (RVar (dummy_loc, id))) *)
-(*       tml *)
-(*   in *)
-(*   let po =  *)
-(*     List.fold_right *)
-(*       (fun (n,t) acc -> *)
-(* 	 RProd (dummy_loc, Anonymous, t, acc)) *)
-(*       eqs_types (match po with  *)
-(* 		     Some e -> e *)
-(* 		   | None -> mkHole) *)
-(*   in *)
-(*   let eqns =    *)
-(*     List.map (fun (loc, idl, cpl, c) -> *)
-(* 		let c' =  *)
-(* 		  List.fold_left  *)
-(* 		    (fun acc (n, t) -> *)
-(* 		       RLambda (dummy_loc, n, mkHole, acc)) *)
-(* 		    c eqs_types *)
-(* 		in (loc, idl, cpl, c')) *)
-(*       eqns *)
-(*   in *)
-(*   let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref), *)
-(* 			      [mkHole; c]) *)
-(*   in *)
-(*   (\*let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref), *)
-(* 			      [mkHole; c]) *)
-(*   in*\) *)
-(*   let refls = List.map (fun (c, _) -> mk_refl_equal c) tml in *)
-(*   let case = RCases (loc,Some po,tml,eqns) in *)
-(*   let app = RApp (dummy_loc, case, refls) in *)
-(*     app *)
-
-(* let rec rewrite_cases c =  *)
-(*   match c with  *)
-(*       RCases _ -> let c' = map_rawconstr rewrite_cases c in *)
-(* 	(match c' with  *)
-(* 	   | RCases (x, y, z, w) -> rewrite_cases_aux (x,y,z,w) *)
-(* 	   | _ -> assert(false)) *)
-(*     | _ -> map_rawconstr rewrite_cases c *)
-	  
-(* let rewrite_cases env c = *)
-(*   let c' = rewrite_cases c in *)
-(*   let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in *)
-(*     c' *)
-
-let list_mapi f = 
-  let rec aux i = function 
-      hd :: tl -> f i hd :: aux (succ i) tl 
-    | [] -> []
-  in aux 0
-
-
 let id_of_name = function
     Name n -> n
   | Anonymous -> raise (Invalid_argument "id_of_name")
@@ -548,23 +353,6 @@ let recursive_message v =
 		    spc () ++ str "are recursively defined")
 
 (* Solve an obligation using tactics, return the corresponding proof term *)
-(*
-let solve_by_tac ev t =
-  debug 1 (str "Solving goal using tactics: " ++ Evd.pr_evar_info ev);
-  let goal = Proof_trees.mk_goal ev.evar_hyps ev.evar_concl None in
-  debug 1 (str "Goal created");
-  let ts = Tacmach.mk_pftreestate goal in
-  debug 1 (str "Got pftreestate");
-  let solved_state = Tacmach.solve_pftreestate t ts in
-  debug 1 (str "Solved goal");
-    let _, l = Tacmach.extract_open_pftreestate solved_state in
-      List.iter (fun (_, x) -> debug 1 (str "left hole of type " ++ my_print_constr (Global.env()) x)) l;
-    let c = Tacmach.extract_pftreestate solved_state in
-    debug 1 (str "Extracted term");
-    debug 1 (str "Term constructed in solve by tac: " ++ my_print_constr (Global.env ()) c);
-    c
-    *)
-
 let solve_by_tac evi t =
   debug 2 (str "Solving goal using tactics: " ++ Evd.pr_evar_info evi);
   let id = id_of_string "H" in
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index a87bbfbeda..5a5dd4274b 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -100,6 +100,12 @@ val mkProj1 : constr -> constr -> constr -> constr
 val mkProj1 : constr -> constr -> constr -> constr
 val mk_ex_pi1 : constr -> constr -> constr -> constr
 val mk_ex_pi1 : constr -> constr -> constr -> constr
+val mk_eq : types -> constr -> constr -> types
+val mk_eq_refl : types -> constr -> constr
+val mk_JMeq : types -> constr-> types -> constr -> types
+val mk_JMeq_refl : types -> constr -> constr
+val mk_conj : types list -> types
+val mk_not : types -> types
 
 val build_dependent_sum : (identifier * types) list -> Proof_type.tactic * types
 val and_tac : (identifier * 'a * constr * Proof_type.tactic) list ->