Remove Expr.mk_binders (#1101)

The smart constructor `mk_binders` is useless because we can build
directly the set of binders in `D_cnf` and we avoid to embed variables
in symbols then extract it in `mk_binders`.

src/lib/frontend/cnf.ml

@@ -35,7 +35,13 @@ module SE = E.Set
 let varset_of_list =
   List.fold_left
     (fun acc (s,ty) ->
-       SE.add (E.mk_term s [] (Ty.shorten ty)) acc) SE.empty
+       let v =
+         match s with
+         | Sy.Var v -> v
+         | _ -> assert false
+       in
+       Var.Map.add v (Ty.shorten ty) acc
+    ) Var.Map.empty
 
 module ME =
   Map.Make
@@ -263,8 +269,7 @@ and make_form name_base ~toplevel f loc ~decl_kind : E.t =
         else Format.sprintf "#%s#sub-%d" name_base !name_tag
       in
       incr name_tag;
-      let qvars = varset_of_list qf.qf_bvars in
-      let binders = E.mk_binders qvars in
+      let binders = varset_of_list qf.qf_bvars in
       let ff = mk_form ~toplevel:false qf.qf_form.c in
 
       (* S : Formulas are purified afterwards.

src/lib/frontend/d_cnf.ml

@@ -1492,16 +1492,14 @@ let rec mk_expr
             ) tvl
           in
           (* Set of binders *)
-          let qvs =
+          let binders =
             List.fold_left (
               fun vl (ty, v, tv) ->
                 let sy = Sy.var v in
                 Cache.store_sy tv sy;
-                let e = E.mk_term sy [] ty in
-                SE.add e vl
-            ) SE.empty ntvl
+                Var.Map.add v ty vl
+            ) Var.Map.empty ntvl
           in
-          let binders = E.mk_binders qvs in
 
           (* filters *)
           let hyp =
@@ -1966,21 +1964,22 @@ let make dloc_file acc stmt =
             let st_loc = dl_to_ael dloc_file loc in
             let name_base = get_basename path in
 
-            let binders_set, defn =
+            let binders, defn =
               let rty = dty_to_ty body.term_ty in
-              let binders_set, rev_args =
+              let binders, rev_args =
                 List.fold_left (
-                  fun (binders_set, acc) (DE.{ path; id_ty; _ } as tv) ->
+                  fun (binders, acc) (DE.{ path; id_ty; _ } as tv) ->
                     let ty = dty_to_ty id_ty in
-                    let sy = Sy.var (Var.of_string (get_basename path)) in
+                    let v = Var.of_string (get_basename path) in
+                    let sy = Sy.var v in
                     Cache.store_sy tv sy;
                     let e = E.mk_term sy [] ty in
-                    SE.add e binders_set, e :: acc
-                ) (SE.empty, []) terml
+                    Var.Map.add v ty binders, e :: acc
+                ) (Var.Map.empty, []) terml
               in
               let sy = Cache.find_sy tcst in
               let e = E.mk_term sy (List.rev rev_args) rty in
-              binders_set, e
+              binders, e
             in
 
             let loc = st_loc in
@@ -1993,7 +1992,6 @@ let make dloc_file acc stmt =
                     ~toplevel:false ~decl_kind body
                 in
                 let qb = E.mk_eq ~iff:true defn ff in
-                let binders = E.mk_binders binders_set in
                 let ff =
                   E.mk_forall name_base Loc.dummy binders [] qb ~toplevel:true
                     ~decl_kind
@@ -2015,7 +2013,6 @@ let make dloc_file acc stmt =
                 in
                 let iff = Ty.equal (Expr.type_info defn) (Ty.Tbool) in
                 let qb = E.mk_eq ~iff defn ff in
-                let binders = E.mk_binders binders_set in
                 let ff =
                   E.mk_forall name_base Loc.dummy binders [] qb ~toplevel:true
                     ~decl_kind

src/lib/structures/expr.ml

@@ -746,12 +746,6 @@ let [@inline always] symbol_info t = t.f
    | _ -> true (* bool vars are terms *)
 *)
 
-let mk_binders st = TSet.fold (fun t sym ->
-    match t with
-    | { f = Sy.Var v; ty; _ } -> Var.Map.add v ty sym
-    | _ -> assert false
-  ) st Var.Map.empty
-
 let merge_vars acc b =
   Var.Map.merge (fun v a b ->
       match a, b with

src/lib/structures/expr.mli

@@ -167,8 +167,6 @@ val compare_quant : quantified -> quantified -> int
 val compare_let : letin -> letin -> int
 
 (** Some auxiliary functions *)
-
-val mk_binders : Set.t -> binders
 val free_vars : t -> (Ty.t * int) Var.Map.t -> (Ty.t * int) Var.Map.t
 val free_type_vars : t -> Ty.Svty.t
 val is_ground : t -> bool