[sledge] Fix type of Exp.rename

Reviewed By: ngorogiannis

Differential Revision: D16905897

fbshipit-source-id: 2f6740b52

sledge/src/llair/exp.ml

@@ -1326,13 +1326,13 @@ let map e ~f =
   in
   fix map_ (fun e -> e) e
 
-let rename e sub =
-  let rec rename_ e sub =
+let rename sub e =
+  let rec rename_ sub e =
     match e with
     | Var _ -> Var.Subst.apply sub e
-    | _ -> map ~f:(fun f -> rename_ f sub) e
+    | _ -> map ~f:(rename_ sub) e
   in
-  rename_ e sub |> check (invariant ~partial:true)
+  rename_ sub e |> check (invariant ~partial:true)
 
 (** Query *)
 

sledge/src/llair/exp.mli

@@ -208,7 +208,7 @@ val fold : t -> init:'a -> f:(t -> 'a -> 'a) -> 'a
 (** Transform *)
 
 val map : t -> f:(t -> t) -> t
-val rename : t -> Var.Subst.t -> t
+val rename : Var.Subst.t -> t -> t
 
 (** Query *)
 

sledge/src/symbheap/equality.ml

@@ -285,7 +285,7 @@ let map_exps ({sat= _; rep} as r) ~f =
     pf "%a" pp_diff (r, r') ;
     invariant r']
 
-let rename r sub = map_exps r ~f:(fun e -> Exp.rename e sub)
+let rename r sub = map_exps r ~f:(Exp.rename sub)
 
 let fold_exps r ~init ~f =
   Map.fold r.rep ~f:(fun ~key ~data z -> f (f z data) key) ~init

sledge/src/symbheap/sh.ml

@@ -186,11 +186,11 @@ let rec simplify {us; xs; cong; pure; heap; djns} =
 (** Quantification and Vocabulary *)
 
 let rename_seg sub ({loc; bas; len; siz; arr} as h) =
-  let loc = Exp.rename loc sub in
-  let bas = Exp.rename bas sub in
-  let len = Exp.rename len sub in
-  let siz = Exp.rename siz sub in
-  let arr = Exp.rename arr sub in
+  let loc = Exp.rename sub loc in
+  let bas = Exp.rename sub bas in
+  let len = Exp.rename sub len in
+  let siz = Exp.rename sub siz in
+  let arr = Exp.rename sub arr in
   ( if
     loc == h.loc && bas == h.bas && len == h.len && siz == h.siz
     && arr == h.arr
@@ -203,9 +203,7 @@ let rename_seg sub ({loc; bas; len; siz; arr} as h) =
     invariant *)
 let rec apply_subst sub ({us= _; xs= _; cong; pure; heap; djns} as q) =
   let cong = Equality.rename cong sub in
-  let pure =
-    List.map_preserving_phys_equal pure ~f:(fun b -> Exp.rename b sub)
-  in
+  let pure = List.map_preserving_phys_equal pure ~f:(Exp.rename sub) in
   let heap = List.map_preserving_phys_equal heap ~f:(rename_seg sub) in
   let djns =
     List.map_preserving_phys_equal djns ~f:(fun d ->

sledge/src/symbheap/state_domain.ml

@@ -82,7 +82,7 @@ let jump actuals formals ?temps q =
   ;
   let q', freshen_locals = Sh.freshen q ~wrt:(Var.Set.of_list formals) in
   let and_eq q formal actual =
-    let actual' = Exp.rename actual freshen_locals in
+    let actual' = Exp.rename freshen_locals actual in
     Sh.and_ (Exp.eq (Exp.var formal) actual') q
   in
   let and_eqs formals actuals q =
@@ -108,7 +108,7 @@ let call ~summaries actuals formals locals globals q =
   let wrt = Set.add_list formals locals in
   let q', freshen_locals = Sh.freshen q ~wrt in
   let and_eq q formal actual =
-    let actual' = Exp.rename actual freshen_locals in
+    let actual' = Exp.rename freshen_locals actual in
     Sh.and_ (Exp.eq (Exp.var formal) actual') q
   in
   let and_eqs formals actuals q =
@@ -190,7 +190,7 @@ let create_summary ~locals ~formals ~entry ~current =
   let restore_formals q =
     Set.fold formals ~init:q ~f:(fun q var ->
         let var = Exp.var var in
-        let renamed_var = Exp.rename var subst in
+        let renamed_var = Exp.rename subst var in
         Sh.and_ (Exp.eq renamed_var var) q )
   in
   (* Add back the original formals name *)