Extset, Extmap: add left versions for some binary operations

[add_left] and [remove_left] are useful in left folds,
[contains] allows to use partial application in maps.

src/core/decl.ml

@@ -455,8 +455,8 @@ let create_data_decl tdl =
     if cl = [] then raise (EmptyAlgDecl ts);
     if ts.ts_def <> None then raise (IllegalTypeAlias ts);
     let news = news_id news ts.ts_name in
-    let pjs = List.fold_left (fun s (_,pl) -> List.fold_left
-      (Opt.fold (fun s ls -> Sls.add ls s)) s pl) Sls.empty cl in
+    let pjs = List.fold_left (fun s (_,pl) ->
+      List.fold_left (Opt.fold Sls.add_left) s pl) Sls.empty cl in
     let news = Sls.fold (fun pj s -> news_id s pj.ls_name) pjs news in
     let ty = ty_app ts (List.map ty_var ts.ts_args) in
     List.fold_left (check_constr ts ty cll pjs) (syms,news) cl
@@ -744,9 +744,8 @@ let check_positivity kn d = match d.d_node with
           | Tyapp (ts,tl) ->
               let check pos ty =
                 if pos then check_ty ty else
-                if ty_s_any (fun ts -> Sts.mem ts tss) ty
-                then raise (NonPositiveTypeDecl (tys,cs,ty))
-              in
+                if ty_s_any (Sts.contains tss) ty then
+                  raise (NonPositiveTypeDecl (tys,cs,ty)) in
               List.iter2 check (ts_extract_pos kn Sts.empty ts) tl
         in
         List.iter check_ty cs.ls_args
@@ -776,7 +775,7 @@ let parse_record kn fll =
   let cs, pjl = match find_constructors kn ts with
     | [cs,pjl] -> cs, List.map (Opt.get_exn (BadRecordField fs)) pjl
     | _ -> raise (BadRecordField fs) in
-  let pjs = List.fold_left (fun s pj -> Sls.add pj s) Sls.empty pjl in
+  let pjs = Sls.of_list pjl in
   let flm = List.fold_left (fun m (pj,v) ->
     if not (Sls.mem pj pjs) then raise (BadRecordField pj) else
     Mls.add_new (DuplicateRecordField pj) pj v m) Mls.empty fll in

src/core/theory.ml

@@ -538,7 +538,7 @@ exception BadInstance of ident
 let cl_init_ty cl ({ts_name = id} as ts) ty =
   if not (Sid.mem id cl.cl_local) then raise (NonLocal id);
   let stv = Stv.of_list ts.ts_args in
-  if not (ty_v_all (fun v -> Stv.mem v stv) ty) then raise (BadInstance id);
+  if not (ty_v_all (Stv.contains stv) ty) then raise (BadInstance id);
   cl.ty_table <- Mts.add ts ty cl.ty_table
 
 let cl_init_ts cl ({ts_name = id} as ts) ts' =

src/core/ty.ml

@@ -143,7 +143,7 @@ let ty_v_all pr ty = Util.all ty_v_fold pr ty
 let ty_v_any pr ty = Util.any ty_v_fold pr ty
 
 let ty_full_inst m ty = ty_v_map (fun v -> Mtv.find v m) ty
-let ty_freevars s ty = ty_v_fold (fun s v -> Stv.add v s) s ty
+let ty_freevars s ty = ty_v_fold Stv.add_left s ty
 let ty_closed ty = ty_v_all Util.ffalse ty
 
 (* smart constructors *)

src/transform/discriminate.ml

@@ -235,7 +235,7 @@ let ft_select_lsinst =
   ((Hstr.create 17) : (Env.env,Lsmap.t) Trans.flag_trans)
 
 let metas_from_env env =
-  let fold_inst tyl _ s = List.fold_left (fun s ty -> Sty.add ty s) s tyl in
+  let fold_inst tyl _ s = List.fold_right Sty.add tyl s in
   let fold_ls _ insts s = Mtyl.fold fold_inst insts s in
   let sty = Mls.fold fold_ls env Sty.empty in
   let add ty decls = create_meta Libencoding.meta_kept [MAty ty] :: decls in

src/transform/eliminate_algebraic.ml

@@ -169,7 +169,7 @@ and rewriteF kn state av sign f = match f.t_node with
       let vl, tr, f1, close = t_open_quant_cb bf in
       let tr = TermTF.tr_map (rewriteT kn state)
                       (rewriteF kn state Svs.empty sign) tr in
-      let av = List.fold_left (fun s v -> Svs.add v s) av vl in
+      let av = List.fold_right Svs.add vl av in
       let f1 = rewriteF kn state av sign f1 in
       t_quant_simp q (close vl tr f1)
   | Tbinop (o, _, _) when (o = Tand && sign) || (o = Tor && not sign) ->
@@ -330,7 +330,7 @@ let add_tags mts (state,task) (ts,csl) =
     let sts = Sts.add ts sts in
     let add s (ls,_) = List.fold_left (mat_ty sts) s ls.ls_args in
     let stv = List.fold_left add Stv.empty csl in
-    List.map (fun v -> Stv.mem v stv) ts.ts_args
+    List.map (Stv.contains stv) ts.ts_args
   and mat_ty sts stv ty = match ty.ty_node with
     | Tyvar tv -> Stv.add tv stv
     | Tyapp (ts,tl) ->

src/util/extmap.ml

@@ -78,6 +78,7 @@ module type S =
     val keys: 'a t -> key list
     val values: 'a t -> 'a list
     val of_list : (key * 'a) list -> 'a t
+    val contains: 'a t -> key -> bool
     val domain : 'a t -> unit t
     val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
     val is_num_elt : int -> 'a t -> bool
@@ -625,6 +626,8 @@ module type S =
     let of_list l =
       List.fold_left (fun acc (k,d) -> add k d acc) empty l
 
+    let contains m x = mem x m
+
     let domain m = map ignore m
 
     let subdomain pr m = mapi_filter (fun k v ->

src/util/extmap.mli

@@ -269,10 +269,13 @@ module type S =
         given to {!Extmap.Make}. *)
 
     val of_list: (key * 'a) list -> 'a t
-    (** construct a map from a pair of bindings *)
+    (** construct a map from a list of bindings. *)
+
+    val contains: 'a t -> key -> bool
+    (** [contains m x] is the same as [mem x m]. *)
 
     val domain : 'a t -> unit t
-    (** [domain m] returns the set of keys of binding [m] *)
+    (** [domain m] returns the set of keys of bindings in [m] *)
 
     val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
     (** [subdomain pr m] returns the set of keys of bindings in [m]

src/util/extset.ml

@@ -47,6 +47,9 @@ module type S = sig
   val add_new : exn -> elt -> t -> t
   val is_num_elt : int -> t -> bool
   val of_list : elt list -> t
+  val contains: t -> elt -> bool
+  val add_left: t -> elt -> t
+  val remove_left: t -> elt -> t
 end
 
 module MakeOfMap (M: Extmap.S) = struct
@@ -91,6 +94,9 @@ module MakeOfMap (M: Extmap.S) = struct
   let add_new e x s = M.add_new e x () s
   let is_num_elt n m = M.is_num_elt n m
   let of_list l = List.fold_left (fun acc a -> add a acc) empty l
+  let contains = M.contains
+  let add_left s e = M.add e () s
+  let remove_left s e = M.remove e s
 end
 
 module type OrderedType = Set.OrderedType

src/util/extset.mli

@@ -150,7 +150,7 @@ module type S =
     val translate : (elt -> elt) -> t -> t
     (** [translate f s] translates the elements in the set [s] by the
         function [f]. [f] must be strictly monotone on the elements of [s].
-        Otherwise it raises invalid_arg *)
+        Otherwise it raises [Invalid_arg]. *)
 
     val add_new : exn -> elt -> t -> t
     (** [add_new e x s] adds [x] to [s] if [s] does not contain [x],
@@ -161,6 +161,15 @@ module type S =
 
     val of_list: elt list -> t
     (** construct a set from a list of elements *)
+
+    val contains: t -> elt -> bool
+    (** [contains s x] is the same as [mem x s]. *)
+
+    val add_left: t -> elt -> t
+    (** [add_left s x] is the same as [add x s]. *)
+
+    val remove_left: t -> elt -> t
+    (** [remove_left s x] is the same as [remove x s]. *)
   end
 
 module MakeOfMap (M : Extmap.S) : S with module M = M