Code extraction

Optimization of proxy variables.

drivers/ocaml64.drv

@@ -72,11 +72,11 @@ module ref.Ref
 end
 
 module ref.Refint
-  syntax val incr "%1 := Z.succ (Pervasives.(!) %1)"
-  syntax val decr "%1 := Z.pred (Pervasives.(!) %1)"
-  syntax val (+=) "%1 := Z.add (Pervasives.(!) %1) %2"
-  syntax val (-=) "%1 := Z.sub (Pervasives.(!) %1) %2"
-  syntax val ( *= ) "%1 := Z.mul (Pervasives.(!) %1) %2"
+  syntax val incr "%1 := Z.succ (!%1)"
+  syntax val decr "%1 := Z.pred (!%1)"
+  syntax val (+=) "%1 := Z.add (!%1) %2"
+  syntax val (-=) "%1 := Z.sub (!%1) %2"
+  syntax val ( *= ) "%1 := Z.mul (!%1) %2"
 end
 
 module null.Null

src/mlw/compile.ml

@@ -791,7 +791,8 @@ module Transform = struct
     (*   (\* because of Lvar we know the constructor is completely applied *\) *)
     (*   add_subst pv e1 e2 *)
     | Elet (Lvar (pv, e1), e2)
-      when Slab.mem Expr.proxy_label pv.pv_vs.vs_name.id_label ->
+      when Slab.mem Expr.proxy_label pv.pv_vs.vs_name.id_label &&
+           eff_pure e1.e_effect ->
       let e1 = expr info subst e1 in
       add_subst pv e1 e2
     | Elet (ld, e) ->

src/mlw/ocaml_printer.ml

@@ -333,6 +333,7 @@ module Print = struct
       (* avoids parenthesis around values *)
       fprintf fmt "%a" (print_apply info (Hrs.find_def ht_rs rs rs)) []
     | Eapp (rs, pvl) ->
+      eprintf "rs->%s@." rs.rs_name.id_string;
       fprintf fmt (protect_on paren "%a")
         (print_apply info (Hrs.find_def ht_rs rs rs)) pvl
     | Ematch (e, pl) ->