move list utilities from Util to Lists

+ fix a bug in "compare"

Makefile.in

@@ -108,7 +108,7 @@ LIBGENERATED = src/util/config.ml src/util/rc.ml src/parser/lexer.ml \
 	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
 	       src/driver/driver_lexer.ml src/session/xml.ml
 
-LIB_UTIL = config opt stdlib exn_printer pp debug loc print_tree \
+LIB_UTIL = config opt lists stdlib exn_printer pp debug loc print_tree \
 	   cmdline hashweak hashcons util warning sysutil rc plugin
 
 LIB_CORE = ident ty term pattern decl theory task pretty env trans printer

src/core/decl.ml

@@ -68,7 +68,7 @@ let open_ls_defn_cb ld =
   let ls,_,_ = ld in
   let vl,t = open_ls_defn ld in
   let close ls' vl' t' =
-    if t_equal t t' && list_all2 vs_equal vl vl' && ls_equal ls ls'
+    if t_equal t t' && Lists.equal vs_equal vl vl' && ls_equal ls ls'
     then ls,ld else make_ls_defn ls' vl' t'
   in
   vl,t,close
@@ -316,10 +316,10 @@ module Hsdecl = Hashcons.Make (struct
   type t = decl
 
   let cs_equal (cs1,pl1) (cs2,pl2) =
-    ls_equal cs1 cs2 && list_all2 (Opt.equal ls_equal) pl1 pl2
+    ls_equal cs1 cs2 && Lists.equal (Opt.equal ls_equal) pl1 pl2
 
   let eq_td (ts1,td1) (ts2,td2) =
-    ts_equal ts1 ts2 && list_all2 cs_equal td1 td2
+    ts_equal ts1 ts2 && Lists.equal cs_equal td1 td2
 
   let eq_ld (ls1,(_,f1,_)) (ls2,(_,f2,_)) =
     ls_equal ls1 ls2 && t_equal f1 f2
@@ -328,14 +328,14 @@ module Hsdecl = Hashcons.Make (struct
     pr_equal pr1 pr2 && t_equal fr1 fr2
 
   let eq_ind (ps1,al1) (ps2,al2) =
-    ls_equal ps1 ps2 && list_all2 eq_iax al1 al2
+    ls_equal ps1 ps2 && Lists.equal eq_iax al1 al2
 
   let equal d1 d2 = match d1.d_node, d2.d_node with
     | Dtype  s1, Dtype  s2 -> ts_equal s1 s2
-    | Ddata  l1, Ddata  l2 -> list_all2 eq_td l1 l2
+    | Ddata  l1, Ddata  l2 -> Lists.equal eq_td l1 l2
     | Dparam s1, Dparam s2 -> ls_equal s1 s2
-    | Dlogic l1, Dlogic l2 -> list_all2 eq_ld l1 l2
-    | Dind   (s1,l1), Dind (s2,l2) -> s1 = s2 && list_all2 eq_ind l1 l2
+    | Dlogic l1, Dlogic l2 -> Lists.equal eq_ld l1 l2
+    | Dind   (s1,l1), Dind (s2,l2) -> s1 = s2 && Lists.equal eq_ind l1 l2
     | Dprop (k1,pr1,f1), Dprop (k2,pr2,f2) ->
         k1 = k2 && pr_equal pr1 pr2 && t_equal f1 f2
     | _,_ -> false
@@ -577,7 +577,7 @@ let decl_fold fn acc d = match d.d_node with
 let list_rpair_map_fold fn =
   let fn acc (x1,x2) =
     let acc,x2 = fn acc x2 in acc,(x1,x2) in
-  Util.map_fold_left fn
+  Lists.map_fold_left fn
 
 let decl_map_fold fn acc d = match d.d_node with
   | Dtype _ | Ddata _ | Dparam _ -> acc, d
@@ -587,7 +587,7 @@ let decl_map_fold fn acc d = match d.d_node with
         let acc,e = fn acc e in
         acc, close ls vl e
       in
-      let acc,l = Util.map_fold_left fn acc l in
+      let acc,l = Lists.map_fold_left fn acc l in
       acc, create_logic_decl l
   | Dind (s, l) ->
       let acc, l = list_rpair_map_fold (list_rpair_map_fold fn) acc l in

src/core/term.ml

@@ -324,11 +324,11 @@ let vs_check v t = ty_equal_check v.vs_ty (t_type t)
 
 (* trigger equality and traversal *)
 
-let tr_equal = list_all2 (list_all2 t_equal)
+let tr_equal = Lists.equal (Lists.equal t_equal)
 
 let tr_map fn = List.map (List.map fn)
 let tr_fold fn = List.fold_left (List.fold_left fn)
-let tr_map_fold fn = Util.map_fold_left (Util.map_fold_left fn)
+let tr_map_fold fn = Lists.map_fold_left (Lists.map_fold_left fn)
 
 (* bind_info equality, hash, and traversal *)
 
@@ -365,7 +365,7 @@ module Hsterm = Hashcons.Make (struct
     pat_equal p1 p2 && bnd_equal b1 b2 && t_equal t1 t2
 
   let t_eq_quant (vl1,b1,tl1,f1) (vl2,b2,tl2,f2) =
-    t_equal f1 f2 && list_all2 vs_equal vl1 vl2 &&
+    t_equal f1 f2 && Lists.equal vs_equal vl1 vl2 &&
     bnd_equal b1 b2 && tr_equal tl1 tl2
 
   let t_equal_node t1 t2 = match t1,t2 with
@@ -378,7 +378,7 @@ module Hsterm = Hashcons.Make (struct
     | Tlet (t1,b1), Tlet (t2,b2) ->
         t_equal t1 t2 && t_eq_bound b1 b2
     | Tcase (t1,bl1), Tcase (t2,bl2) ->
-        t_equal t1 t2 && list_all2 t_eq_branch bl1 bl2
+        t_equal t1 t2 && Lists.equal t_eq_branch bl1 bl2
     | Teps f1, Teps f2 -> t_eq_bound f1 f2
     | Tquant (q1,b1), Tquant (q2,b2) ->
         q1 = q2 && t_eq_quant b1 b2
@@ -548,7 +548,7 @@ let t_map_fold_unsafe fn acc t = match t.t_node with
   | Tvar _ | Tconst _ ->
       acc, t
   | Tapp (f,tl) ->
-      let acc,sl = map_fold_left fn acc tl in
+      let acc,sl = Lists.map_fold_left fn acc tl in
       if List.for_all2 t_equal sl tl then acc,t else
       acc, t_label_copy t (t_app f sl t.t_ty)
   | Tif (f,t1,t2) ->
@@ -563,7 +563,7 @@ let t_map_fold_unsafe fn acc t = match t.t_node with
       acc, t_label_copy t (t_let e b t.t_ty)
   | Tcase (e,bl) ->
       let acc, e = fn acc e in
-      let acc, bl = map_fold_left (bound_map_fold fn) acc bl in
+      let acc, bl = Lists.map_fold_left (bound_map_fold fn) acc bl in
       acc, t_label_copy t (t_case e bl t.t_ty)
   | Teps b ->
       let acc, b = bound_map_fold fn acc b in
@@ -656,7 +656,7 @@ let vs_rename h v =
   Mvs.add v (t_var u) h, u
 
 let vl_rename h vl =
-  Util.map_fold_left vs_rename h vl
+  Lists.map_fold_left vs_rename h vl
 
 let pat_rename h p =
   let add_vs v () = fresh_vsymbol v in
@@ -696,7 +696,7 @@ let t_open_branch_cb tbr =
 let t_open_quant_cb fq =
   let vl, tl, f = t_open_quant fq in
   let close vl' tl' f' =
-    if t_equal f f' && tr_equal tl tl' && list_all2 vs_equal vl vl'
+    if t_equal f f' && tr_equal tl tl' && Lists.equal vs_equal vl vl'
     then fq else t_close_quant vl' tl' f'
   in
   vl, tl, f, close
@@ -853,7 +853,7 @@ let gen_vs_rename fnT h v =
   Mvs.add v u h, u
 
 let gen_vl_rename fnT h vl =
-  Util.map_fold_left (gen_vs_rename fnT) h vl
+  Lists.map_fold_left (gen_vs_rename fnT) h vl
 
 let gen_pat_rename fnT fnL h p =
   let add_vs v () = gen_fresh_vsymbol fnT v in
@@ -1035,7 +1035,7 @@ let t_map_fold fn acc t = match t.t_node with
       let brn acc b =
         let p,t,close = t_open_branch_cb b in
         let acc,t = fn acc t in acc, close p t in
-      let acc, bl = map_fold_left brn acc bl in
+      let acc, bl = Lists.map_fold_left brn acc bl in
       acc, t_label_copy t (t_case e bl)
   | Teps b ->
       let u,t1,close = t_open_bound_cb b in
@@ -1207,7 +1207,7 @@ let rec t_equal_alpha c1 c2 m1 m2 t1 t2 =
           let m2 = pat_rename_alpha c2 m2 p2 in
           t_equal_alpha c1 c2 m1 m2 e1 e2
         in
-        list_all2 br_eq bl1 bl2
+        Lists.equal br_eq bl1 bl2
     | Teps b1, Teps b2 ->
         let u1,e1 = t_open_bound b1 in
         let u2,e2 = t_open_bound b2 in
@@ -1216,7 +1216,7 @@ let rec t_equal_alpha c1 c2 m1 m2 t1 t2 =
         t_equal_alpha c1 c2 m1 m2 e1 e2
     | Tquant (q1,((vl1,_,_,_) as b1)), Tquant (q2,((vl2,_,_,_) as b2)) ->
         q1 = q2 &&
-        list_all2 (fun v1 v2 -> ty_equal v1.vs_ty v2.vs_ty) vl1 vl2 &&
+        Lists.equal (fun v1 v2 -> ty_equal v1.vs_ty v2.vs_ty) vl1 vl2 &&
         let vl1,_,e1 = t_open_quant b1 in
         let vl2,_,e2 = t_open_quant b2 in
         let m1 = vl_rename_alpha c1 m1 vl1 in

src/core/theory.ml

@@ -202,7 +202,7 @@ module Hstdecl = Hashcons.Make (struct
     | Clone (th1,sm1), Clone (th2,sm2) ->
         id_equal th1.th_name th2.th_name && eq_smap sm1 sm2
     | Meta (t1,al1), Meta (t2,al2) ->
-        t1 = t2 && list_all2 eq_marg al1 al2
+        t1 = t2 && Lists.equal eq_marg al1 al2
     | _,_ -> false
 
   let hs_cl_ts _ ts acc = Hashcons.combine acc (ts_hash ts)

src/core/trans.ml

@@ -38,11 +38,11 @@ let conv_res c f x = c (f x)
 
 let singleton f x = [f x]
 
-let compose   f g x =            g (f x)
-let compose_l f g x = list_apply g (f x)
+let compose   f g x =             g (f x)
+let compose_l f g x = Lists.apply g (f x)
 
 let seq l x = List.fold_left (|>) x l
-let seq_l l x = List.fold_left (fun x f -> list_apply f x) [x] l
+let seq_l l x = List.fold_left (fun x f -> Lists.apply f x) [x] l
 
 module Wtask = Hashweak.Make (struct
   type t = task_hd
@@ -78,7 +78,7 @@ let fold fn v =
   in
   accum []
 
-let fold_l fn v = fold (fun task -> list_apply (fn task)) [v]
+let fold_l fn v = fold (fun task -> Lists.apply (fn task)) [v]
 
 let fold_map   fn v t = conv_res snd            (fold   fn (v, t))
 let fold_map_l fn v t = conv_res (List.map snd) (fold_l fn (v, t))

src/driver/autodetection.ml

@@ -121,7 +121,7 @@ let load rc =
   let atps = get_family rc "ATP" in
   let atps = List.rev_map (load_prover ATP) atps in
   let itps = get_family rc "ITP" in
-  let tps = List.fold_left (cons (load_prover ITP)) atps itps in
+  let tps = List.fold_left (Lists.cons (load_prover ITP)) atps itps in
   tps
 
 let load_prover_shortcut acc (_, section) =

src/parser/denv.ml

@@ -260,7 +260,7 @@ and fmla env = function
         let v = create_user_vs id (ty_of_dty ty) in
         Mstr.add id.id v env, v
       in
-      let env, vl = map_fold_left uquant env uqu in
+      let env, vl = Lists.map_fold_left uquant env uqu in
       let trigger = function
         | TRterm t -> term env t
         | TRfmla f -> fmla env f

src/parser/typing.ml

@@ -528,7 +528,7 @@ and dterm_node ~localize loc uc env = function
         in
         add_var id.id ty env, (id,ty)
       in
-      let env, uqu = map_fold_left uquant env uqu in
+      let env, uqu = Lists.map_fold_left uquant env uqu in
       let trigger e =
         try
           TRterm (dterm ~localize uc env e)
@@ -647,7 +647,7 @@ and dfmla_node ~localize loc uc env = function
         in
         add_var id.id ty env, (id,ty)
       in
-      let env, uqu = map_fold_left uquant env uqu in
+      let env, uqu = Lists.map_fold_left uquant env uqu in
       let trigger e =
         try
           TRterm (dterm ~localize uc env e)

src/printer/pvs.ml

@@ -735,7 +735,7 @@ let print_ind_decl info fmt (ps,al) =
   let _, _, all_ty_params = ls_ty_vars ps in
   let vl = List.map (create_vsymbol (id_fresh "z")) ps.ls_args in
   let tl = List.map t_var vl in
-  let dj = Util.map_join_left (Eliminate_inductive.exi tl) t_or al in
+  let dj = Lists.map_join_left (Eliminate_inductive.exi tl) t_or al in
   print_name fmt ps.ls_name;
   fprintf fmt "@[<hov 2>%a%a%a: INDUCTIVE bool =@ @[<hov>%a@]@]@\n"
     print_ls ps print_params all_ty_params (print_arguments info) vl

src/programs/pgm_types.ml

@@ -428,7 +428,7 @@ end = struct
     | Tpure ty ->
         Tpure (ty_inst ts ty)
     | Tarrow (bl, c) ->
-        let s, bl = Util.map_fold_left (subst_binder ts) s bl in
+        let s, bl = Lists.map_fold_left (subst_binder ts) s bl in
         Tarrow (bl, subst_type_c ts s c)
 
   and subst_binder ts s pv =
@@ -458,7 +458,7 @@ end = struct
           let s' = Mvs.add v.pv_pure (t_var pure) s in
           s', v'
         in
-        let s, bl' = Util.map_fold_left rename Mvs.empty bl in
+        let s, bl' = Lists.map_fold_left rename Mvs.empty bl in
         Tarrow (bl', subst_type_c Mtv.empty s c)
 
   let v_result ty = create_vsymbol (id_fresh "result") ty

src/programs/pgm_typing.ml

@@ -326,7 +326,7 @@ let rec dutype_v env = function
   | Ptree.Tpure pt ->
       DUTpure (dtype ~user:true env pt)
   | Ptree.Tarrow (bl, c) ->
-      let env, bl = map_fold_left dubinder env bl in
+      let env, bl = Lists.map_fold_left dubinder env bl in
       let c = dutype_c env c in
       DUTarrow (bl, c)
 
@@ -513,7 +513,7 @@ and dexpr_desc ~ghost ~userloc env loc = function
       expected_type e2 ty2;
       DEapply (e1, e2), ty
   | Ptree.Efun (bl, t) ->
-      let env, bl = map_fold_left dubinder env bl in
+      let env, bl = Lists.map_fold_left dubinder env bl in
       let _, ((_,e,_) as t) = dtriple ~ghost ~userloc env t in
       let tyl = List.map (fun (_,ty) -> ty) bl in
       let ty = dcurrying tyl e.dexpr_type in
@@ -768,10 +768,10 @@ and dletrec ~ghost ~userloc env dl =
     let env = add_local_top env id.id ty in
     env, ((id, ty), bl, t)
   in
-  let env, dl = map_fold_left add_one env dl in
+  let env, dl = Lists.map_fold_left add_one env dl in
   (* then type-check all of them and unify *)
   let type_one ((id, tyres), bl, t) =
-    let env, bl = map_fold_left dubinder env bl in
+    let env, bl = Lists.map_fold_left dubinder env bl in
     let v, ((_,e,_) as t) = dtriple ~ghost ~userloc env t in
     let tyl = List.map (fun (_,ty) -> ty) bl in
     let ty = dcurrying tyl e.dexpr_type in
@@ -1062,7 +1062,7 @@ let rec iutype_v env = function
   | DUTpure ty ->
       ITpure (Denv.ty_of_dty ty)
   | DUTarrow (bl, c) ->
-      let env, bl = map_fold_left iubinder env bl in
+      let env, bl = Lists.map_fold_left iubinder env bl in
       ITarrow (bl, iutype_c env c)
 
 and iutype_c env c =
@@ -1169,7 +1169,7 @@ let ipattern env p =
     | Term.Pwild ->
         env, IPwild
     | Term.Papp (ls, pl) ->
-        let env, pl = map_fold_left ipattern env pl in
+        let env, pl = Lists.map_fold_left ipattern env pl in
         env, IPapp (ls, pl)
     | Term.Por (p1, p2) ->
         let env, p1 = ipattern env p1 in
@@ -1286,7 +1286,7 @@ and iexpr_desc env loc ty = function
             e.iexpr_desc
       end
   | DEfun (bl, e1) ->
-      let env, bl = map_fold_left iubinder env bl in
+      let env, bl = Lists.map_fold_left iubinder env bl in
       IEfun (bl, itriple env e1)
   | DElet (x, e1, e2) ->
       let e1 = iexpr env e1 in
@@ -1412,10 +1412,10 @@ and iletrec env dl =
     let env, v = iadd_local env (id_user x.id x.id_loc) ty in
     env, (v, bl, var, t)
   in
-  let env, dl = map_fold_left step1 env dl in
+  let env, dl = Lists.map_fold_left step1 env dl in
   (* then translate variants and bodies *)
   let step2 (v, bl, var, (_,_,_ as t)) =
-    let env, bl = map_fold_left iubinder env bl in
+    let env, bl = Lists.map_fold_left iubinder env bl in
     let var = Opt.map (ivariant env) var in
     let t = itriple env t in
     let var, t = match var with
@@ -1501,7 +1501,7 @@ let post_effect ef ((v, q), ql) =
     let ef, q = term_effect ef q in ef, (e, (x, q))
   in
   let ef, q = term_effect ef q in
-  let ef, ql = map_fold_left exn_effect ef ql in
+  let ef, ql = Lists.map_fold_left exn_effect ef ql in
   ef, ((v, q), ql)
 
 let effect e =
@@ -1548,7 +1548,7 @@ and type_c env c =
     c_post        = q; }
 
 and add_binders env bl =
-  map_fold_left add_binder env bl
+  Lists.map_fold_left add_binder env bl
 
 and add_binder env (i, ty) =
   let v = tpure ty in
@@ -1567,7 +1567,7 @@ and pattern_node env ty p =
       env, (pat_wild ty, Pwild)
   | IPapp (ls, pl) ->
       let ls = (get_psymbol ls).ps_pure in (* impure -> pure *)
-      let env, pl = map_fold_left pattern env pl in
+      let env, pl = Lists.map_fold_left pattern env pl in
       let lpl = List.map (fun p -> p.ppat_pat) pl in
       env, (pat_app ls lpl ty, Papp (ls, pl))
   | IPor (p1, p2) ->
@@ -1798,7 +1798,7 @@ and expr_desc gl env loc ty = function
         let ef = E.union ef e.expr_effect in
         ef, (p, e)
       in
-      let ef, bl = map_fold_left branch E.empty bl in
+      let ef, bl = Lists.map_fold_left branch E.empty bl in
       Ematch (v, bl), tpure ty, ef
   | IEabsurd ->
       Eabsurd, tpure ty, E.empty
@@ -1911,7 +1911,7 @@ and letrec gl env dl = (* : env * recfun list *)
       in
       Mvs.add i.i_impure c m, (v, bl, var, t)
     in
-    map_fold_left type1 Mvs.empty dl
+    Lists.map_fold_left type1 Mvs.empty dl
   in
   let rec fixpoint m =
     (* printf "fixpoint...@\n"; *)
@@ -2392,7 +2392,7 @@ let rec decl ~wp env ltm lmod uc (loc,dcl) = match dcl with
         in
         uc, (ps, d)
       in
-      let uc, dl = map_fold_left one uc dl in
+      let uc, dl = Lists.map_fold_left one uc dl in
       let d = Dletrec dl in
       let uc = add_decl d uc in
       if wp then Pgm_wp.decl uc d else uc

src/session/session.ml

@@ -56,11 +56,11 @@ let print_ident_path fmt ip =
     (Pp.print_list Pp.dot Pp.string) ip.ip_qualid
 
 let compare_ident_path x y =
-  let c = list_compare String.compare x.ip_library y.ip_library in
+  let c = Lists.compare String.compare x.ip_library y.ip_library in
   if c <> 0 then -c else (* in order to be bottom up *)
   let c = String.compare x.ip_theory y.ip_theory in
   if c <> 0 then c else
-  let c = list_compare String.compare x.ip_qualid y.ip_qualid in
+  let c = Lists.compare String.compare x.ip_qualid y.ip_qualid in
   c
 
 module Pos = struct
@@ -98,7 +98,7 @@ module Mmeta_args = Map.Make(struct
     | MAint x, MAint y -> compare x y
     | _ -> compare (meta_arg_id x) (meta_arg_id y)
 
-  let compare = list_compare compare_meta_arg
+  let compare = Lists.compare compare_meta_arg
 end)
 module Smeta_args = Mmeta_args.Set
 

src/transform/eliminate_algebraic.ml

@@ -170,7 +170,7 @@ and rewriteF kn state av sign f = match f.t_node with
         | _ -> Printer.unsupportedTerm f uncompiled
       in
       let op = if sign then t_and_simp else t_or_simp in
-      map_join_left find op (find_constructors kn ts)
+      Lists.map_join_left find op (find_constructors kn ts)
   | Tquant (q, bf) when (q = Tforall && sign) || (q = Texists && not sign) ->
       let vl, tr, f1, close = t_open_quant_cb bf in
       let tr = TermTF.tr_map (rewriteT kn state)
@@ -315,7 +315,7 @@ let add_inversion (state,task) ts ty csl =
     let pjl = Mls.find cs state.pj_map in
     let app pj = t_app_infer pj [ax_hd] in
     t_equ ax_hd (fs_app cs (List.map app pjl) ty) in
-  let ax_f = map_join_left mk_cs t_or csl in
+  let ax_f = Lists.map_join_left mk_cs t_or csl in
   let ax_f = t_forall_close [ax_vs] [] ax_f in
   state, add_prop_decl task Paxiom ax_pr ax_f
 

src/transform/eliminate_inductive.ml

@@ -35,7 +35,7 @@ let inv acc (ps,al) =
   let vl = List.map (create_vsymbol (id_fresh "z")) ps.ls_args in
   let tl = List.map t_var vl in
   let hd = ps_app ps tl in
-  let dj = Util.map_join_left (exi tl) t_or al in
+  let dj = Lists.map_join_left (exi tl) t_or al in
   let hsdj = Simplify_formula.fmla_remove_quant (t_implies hd dj) in
   let ax = t_forall_close vl [] hsdj in
   let nm = id_derive (ps.ls_name.id_string ^ "_inversion") ps.ls_name in

src/transform/encoding_instantiate.ml

@@ -306,7 +306,7 @@ and rewrite_fmla menv tvar vsvar f =
       ps_app p tl'
     | Tquant(q, b) ->
       let vl, tl, f1, cb = t_open_quant_cb b in
-      let vsvar,vl = map_fold_left (conv_vs menv tvar) vsvar vl in
+      let vsvar,vl = Lists.map_fold_left (conv_vs menv tvar) vsvar vl in
 
       let f1 = fnF vsvar f1 in
       (* Ici un trigger qui ne match pas assez de variables

src/transform/encoding_sort.ml

@@ -105,7 +105,7 @@ and rewrite_fmla tenv ud vm f =
   | Tquant (q,b) ->
       let vl, tl, f1, close = t_open_quant_cb b in
       let add m v = let v' = conv_vs tenv ud v in Mvs.add v (t_var v') m, v' in
-      let vm', vl' = Util.map_fold_left add vm vl in
+      let vm', vl' = Lists.map_fold_left add vm vl in
       let tl' = TermTF.tr_map (fnT vm') (fnF vm') tl in
       let f1' = fnF vm' f1 in
       t_quant q (close vl' tl' f1')

src/transform/induction.ml

@@ -75,7 +75,7 @@ module VsList =
 struct
   type t = vsymbol list
   let hash = Hashcons.combine_list vs_hash 3
-  let equal = Util.list_all2 vs_equal
+  let equal = Lists.equal vs_equal
   let cmp_vs vs1 vs2 = Pervasives.compare (vs_hash vs2) (vs_hash vs1)
   let compare t1 t2 =
     let rec aux t1 t2 = match t1,t2 with

src/transform/introduction.ml

@@ -38,7 +38,7 @@ let rec intros pr f = match f.t_node with
         Mvs.add vs (fs_app ls [] vs.vs_ty) subst,
         create_param_decl ls
       in
-      let subst, dl = Util.map_fold_left intro_var Mvs.empty vsl in
+      let subst, dl = Lists.map_fold_left intro_var Mvs.empty vsl in
       let f = t_subst subst f in
       dl @ intros pr f
   | Tlet (t,fb) ->

src/transform/split_goal.ml

@@ -17,7 +17,7 @@ let apply_append fn acc l =
   List.fold_left (fun l e -> fn e :: l) acc (List.rev l)
 
 let apply_append2 fn acc l1 l2 =
-  Util.list_fold_product (fun l e1 e2 -> fn e1 e2 :: l)
+  Lists.fold_product (fun l e1 e2 -> fn e1 e2 :: l)
     acc (List.rev l1) (List.rev l2)
 
 let split_case forig spl c acc tl bl =

src/util/lists.ml

+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2012   --   INRIA - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
+(* useful list combinators *)
+
+let rev_map_fold_left f acc l =
+  let acc, rev =
+    List.fold_left
+      (fun (acc, rev) e -> let acc, e = f acc e in acc, e :: rev)
+      (acc, []) l
+  in
+  acc, rev
+
+let map_fold_left f acc l =
+  let acc, rev = rev_map_fold_left f acc l in
+  acc, List.rev rev
+
+let equal pr l1 l2 =
+  try List.for_all2 pr l1 l2 with Invalid_argument _ -> false
+
+let rec compare cmp l1 l2 = match l1,l2 with
+  | [], [] ->  0
+  | [], _  -> -1
+  | _,  [] ->  1
+  | a1::l1, a2::l2 ->
+      let c = cmp a1 a2 in if c = 0 then compare cmp l1 l2 else c
+
+let map_join_left map join = function
+  | x :: xl -> List.fold_left (fun acc x -> join acc (map x)) (map x) xl
+  | _ -> invalid_arg "List.Lists.map_join_left"
+
+let apply f l =
+  List.rev (List.fold_left (fun acc x -> List.rev_append (f x) acc) [] l)
+
+let cons f acc x = (f x)::acc
+
+let fold_product f acc l1 l2 =
+  List.fold_left
+    (fun acc e1 ->
+       List.fold_left
+         (fun acc e2 -> f acc e1 e2)
+         acc l2)
+    acc l1
+
+let fold_product_l f acc ll =
+  let ll = List.rev ll in
+  let rec aux acc le = function
+    | [] -> f acc le
+    | l::ll -> List.fold_left (fun acc e -> aux acc (e::le) ll) acc l
+  in
+  aux acc [] ll
+
+let flatten_rev fl =
+  List.fold_left (fun acc l -> List.rev_append l acc) [] fl
+
+let part cmp l =
+  let l = List.stable_sort cmp l in
+  match l with
+    | [] -> []
+    | e::l ->
+      let rec aux acc curr last = function
+        | [] -> ((last::curr)::acc)
+        | a::l when cmp last a = 0 -> aux acc (last::curr) a l
+        | a::l -> aux ((last::curr)::acc) [] a l in
+      aux [] [] e l
+
+let rec first f = function
+  | [] -> raise Not_found
+  | a::l -> match f a with
+      | None -> first f l
+      | Some r -> r
+
+let find_nth p l =
+  let rec aux p n = function
+    | [] -> raise Not_found
+    | a::l -> if p a then n else aux p (n+1) l in
+  aux p 0 l
+
+
+let first_nth f l =
+  let rec aux f n = function
+    | [] -> raise Not_found
+    | a::l -> match f a with
+      | None -> aux f (n+1) l
+      | Some r -> n,r in
+  aux f 0 l
+
+let iteri f l =
+  let rec iter i = function
+    | [] -> ()
+    | x :: l -> f i x; iter (i + 1) l
+  in
+  iter 0 l
+
+let mapi f l =
+  let rec map i = function
+    | [] -> []
+    | x :: l -> let v = f i x in v :: map (i + 1) l
+  in
+  map 0 l
+
+let fold_lefti f acc l =
+  let rec fold_left acc i = function
+    | [] -> acc
+    | a :: l -> fold_left (f acc i a) (i + 1) l
+  in
+  fold_left acc 0 l
+
+let rec prefix n l =
+  if n = 0 then []
+  else if n < 0 || l = [] then invalid_arg "Util.chop"
+  else List.hd l :: prefix (n - 1) (List.tl l)
+
+let rec chop n l =
+  if n = 0 then l
+  else if n < 0 || l = [] then invalid_arg "Util.chop"
+  else chop (n - 1) (List.tl l)
+
+let rec chop_last = function
+  | [] -> invalid_arg "Util.chop_last"
+  | [r] -> [], r
+  | x :: s -> let s, r = chop_last s in x :: s, r
+

src/util/lists.mli

+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2012   --   INRIA - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
+(* useful list combinators *)
+
+val rev_map_fold_left :
+  ('acc -> 'a -> 'acc * 'b) -> 'acc -> 'a list -> 'acc * 'b list
+
+val map_fold_left :
+  ('acc -> 'a -> 'acc * 'b) -> 'acc -> 'a list -> 'acc * 'b list
+
+val equal : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
+
+val compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int
+
+val cons : ('a -> 'b) -> 'b list -> 'a -> 'b list
+
+val map_join_left : ('a -> 'b) -> ('b -> 'b -> 'b) -> 'a list -> 'b
+
+val apply : ('a -> 'b list) -> 'a list -> 'b list
+(** [apply f [a1;..;an]] returns (f a1)@...@(f an) *)
+
+val fold_product : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b list -> 'c list -> 'a
+(** [fold_product f acc l1 l2] apply the function [f] with the
+    accumulator [acc] on all the pair of elements of [l1] and [l2]
+    tail-recursive *)
+
+val fold_product_l : ('a -> 'b list -> 'a) -> 'a -> 'b list list -> 'a
+(** generalisation of {! Lists.fold_product} not tail-recursive *)
+
+val flatten_rev : 'a list list -> 'a list
+
+val part : ('a -> 'a -> int) -> 'a list -> 'a list list
+(** [part cmp l] returns the list of the congruence classes with
+    respect to [cmp]. They are returned in reverse order *)
+
+val first : ('a -> 'b option) -> 'a list -> 'b
+(** [first f l] returns the first result of the application of
+    [f] to an element of [l] which doesn't return [None]. [raise
+    Not_found] if all the element of [l] return [None] *)
+
+val find_nth : ('a -> bool) -> 'a list -> int
+(** [find_nth p l] returns the index of the first element that
+    satifies the predicate [p]. [raise Not_found] if no element of [l]
+    verify the predicate *)
+
+val first_nth : ('a -> 'b option) -> 'a list -> int * 'b
+(** The combinaison of {!list_first} and {!list_find_nth}. *)
+
+val mapi : (int -> 'a -> 'b) -> 'a list -> 'b list
+val iteri : (int -> 'a -> unit) -> 'a list -> unit
+val fold_lefti : ('a -> int -> 'b -> 'a) -> 'a -> 'b list -> 'a
+(** similar to List.map, List.iter and List.fold_left,