Remove duplicated function

compiler/dcalc/ast.ml

@@ -280,40 +280,40 @@ end
 
 let map_expr
     (ctx : 'a)
-    (t : 'a -> expr Pos.marked -> expr Pos.marked Bindlib.box)
+    ~(f : 'a -> expr Pos.marked -> expr Pos.marked Bindlib.box)
     (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
   match Pos.unmark e with
   | EVar (v, _pos) -> evar v (Pos.get_position e)
-  | EApp (f, args) ->
-      eapp (t ctx f) (List.map (t ctx) args) (Pos.get_position e)
+  | EApp (e1, args) ->
+      eapp (f ctx e1) (List.map (f ctx) args) (Pos.get_position e)
   | EAbs ((binder, binder_pos), typs) ->
       eabs
-        (Bindlib.box_mbinder (t ctx) binder)
+        (Bindlib.box_mbinder (f ctx) binder)
         binder_pos typs (Pos.get_position e)
-  | ETuple (args, s) -> etuple (List.map (t ctx) args) s (Pos.get_position e)
+  | ETuple (args, s) -> etuple (List.map (f ctx) args) s (Pos.get_position e)
   | ETupleAccess (e1, n, s_name, typs) ->
-      etupleaccess ((t ctx) e1) n s_name typs (Pos.get_position e)
+      etupleaccess ((f ctx) e1) n s_name typs (Pos.get_position e)
   | EInj (e1, i, e_name, typs) ->
-      einj ((t ctx) e1) i e_name typs (Pos.get_position e)
+      einj ((f ctx) e1) i e_name typs (Pos.get_position e)
   | EMatch (arg, arms, e_name) ->
-      ematch ((t ctx) arg) (List.map (t ctx) arms) e_name (Pos.get_position e)
-  | EArray args -> earray (List.map (t ctx) args) (Pos.get_position e)
+      ematch ((f ctx) arg) (List.map (f ctx) arms) e_name (Pos.get_position e)
+  | EArray args -> earray (List.map (f ctx) args) (Pos.get_position e)
   | ELit l -> elit l (Pos.get_position e)
-  | EAssert e1 -> eassert ((t ctx) e1) (Pos.get_position e)
+  | EAssert e1 -> eassert ((f ctx) e1) (Pos.get_position e)
   | EOp op -> Bindlib.box (EOp op, Pos.get_position e)
   | EDefault (excepts, just, cons) ->
       edefault
-        (List.map (t ctx) excepts)
-        ((t ctx) just)
-        ((t ctx) cons)
+        (List.map (f ctx) excepts)
+        ((f ctx) just)
+        ((f ctx) cons)
         (Pos.get_position e)
   | EIfThenElse (e1, e2, e3) ->
-      eifthenelse ((t ctx) e1) ((t ctx) e2) ((t ctx) e3) (Pos.get_position e)
-  | ErrorOnEmpty e1 -> eerroronempty ((t ctx) e1) (Pos.get_position e)
+      eifthenelse ((f ctx) e1) ((f ctx) e2) ((f ctx) e3) (Pos.get_position e)
+  | ErrorOnEmpty e1 -> eerroronempty ((f ctx) e1) (Pos.get_position e)
 
 (** See [Bindlib.box_term] documentation for why we are doing that. *)
 let box_expr (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
-  let rec id_t () e = map_expr () id_t e in
+  let rec id_t () e = map_expr () ~f:id_t e in
   id_t () e
 
 module VarMap = Map.Make (Var)
@@ -593,7 +593,7 @@ let rec expr_size (e : expr Pos.marked) : int =
 let remove_logging_calls (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
   let rec f () e =
     match Pos.unmark e with
-    | EApp ((EOp (Unop (Log _)), _), [ arg ]) -> map_expr () f arg
-    | _ -> map_expr () f e
+    | EApp ((EOp (Unop (Log _)), _), [ arg ]) -> map_expr () ~f arg
+    | _ -> map_expr () ~f e
   in
   f () e

compiler/dcalc/optimizations.ml

@@ -256,32 +256,3 @@ let optimize_program (p : program) : program =
     (program_map partial_evaluation
        { var_values = VarMap.empty; decl_ctx = p.decl_ctx }
        p)
-
-let rec remove_all_logs (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
-  let pos = Pos.get_position e in
-  let rec_helper = remove_all_logs in
-  match Pos.unmark e with
-  | EVar (x, _) -> evar x pos
-  | ETuple (args, s_name) -> etuple (List.map rec_helper args) s_name pos
-  | ETupleAccess (arg, i, s_name, typs) ->
-      etupleaccess (rec_helper arg) i s_name typs pos
-  | EInj (arg, i, e_name, typs) -> einj (rec_helper arg) i e_name typs pos
-  | EMatch (arg, arms, e_name) ->
-      ematch (rec_helper arg) (List.map rec_helper arms) e_name pos
-  | EArray args -> earray (List.map rec_helper args) pos
-  | ELit l -> elit l pos
-  | EAbs ((binder, binder_pos), typs) ->
-      let vars, body = Bindlib.unmbind binder in
-      let new_body = rec_helper body in
-      let new_binder = Bindlib.bind_mvar vars new_body in
-      eabs new_binder binder_pos typs pos
-  | EApp (f, args) -> eapp (rec_helper f) (List.map rec_helper args) pos
-  | EAssert e1 -> eassert (rec_helper e1) pos
-  | EOp op -> eop op pos
-  | EDefault (exceptions, just, cons) ->
-      edefault
-        (List.map rec_helper exceptions)
-        (rec_helper just) (rec_helper cons) pos
-  | EIfThenElse (e1, e2, e3) ->
-      eifthenelse (rec_helper e1) (rec_helper e2) (rec_helper e3) pos
-  | ErrorOnEmpty e1 -> eerroronempty (rec_helper e1) pos

compiler/dcalc/optimizations.mli

@@ -22,4 +22,3 @@ open Ast
 
 val optimize_expr : decl_ctx -> expr Pos.marked -> expr Pos.marked Bindlib.box
 val optimize_program : program -> program
-val remove_all_logs : expr Pos.marked -> expr Pos.marked Bindlib.box

compiler/verification/solver.ml

@@ -34,8 +34,7 @@ let solve_vc
               Z3backend.Io.translate_expr
                 (Z3backend.Io.make_context decl_ctx
                    vc.Conditions.vc_free_vars_typ)
-                (Bindlib.unbox
-                   (Dcalc.Optimizations.remove_all_logs vc.Conditions.vc_guard))
+                vc.Conditions.vc_guard
             in
             Z3backend.Io.Success (z3_vc, ctx)
           with Failure msg -> Fail msg ))