Fix a small issue with SymbolicToPure.translate_loop

2 files changed, 43 insertions, 50 deletions

diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index b19e0be6..33082dc3 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -133,33 +133,39 @@ let type_id_to_string (fmt : type_formatter) (id : type_id) : string =
       | Option -> "Option"
       | Vec -> "Vec")
 
-let rec ty_to_string (fmt : type_formatter) (ty : ty) : string =
+let rec ty_to_string (fmt : type_formatter) (inside : bool) (ty : ty) : string =
   match ty with
   | Adt (id, tys) -> (
-      let tys = List.map (ty_to_string fmt) tys in
+      let tys = List.map (ty_to_string fmt false) tys in
       match id with
       | Tuple -> "(" ^ String.concat " * " tys ^ ")"
       | AdtId _ | Assumed _ ->
-          let tys = if tys = [] then "" else " " ^ String.concat " " tys in
-          type_id_to_string fmt id ^ tys)
+          let tys_s = if tys = [] then "" else " " ^ String.concat " " tys in
+          let ty_s = type_id_to_string fmt id ^ tys_s in
+          if tys <> [] && inside then "(" ^ ty_s ^ ")" else ty_s)
   | TypeVar tv -> fmt.type_var_id_to_string tv
   | Bool -> "bool"
   | Char -> "char"
   | Integer int_ty -> integer_type_to_string int_ty
   | Str -> "str"
-  | Array aty -> "[" ^ ty_to_string fmt aty ^ "; ?]"
-  | Slice sty -> "[" ^ ty_to_string fmt sty ^ "]"
+  | Array aty -> "[" ^ ty_to_string fmt false aty ^ "; ?]"
+  | Slice sty -> "[" ^ ty_to_string fmt false sty ^ "]"
   | Arrow (arg_ty, ret_ty) ->
-      ty_to_string fmt arg_ty ^ " -> " ^ ty_to_string fmt ret_ty
+      let ty =
+        ty_to_string fmt true arg_ty ^ " -> " ^ ty_to_string fmt false ret_ty
+      in
+      if inside then "(" ^ ty ^ ")" else ty
 
-let field_to_string fmt (f : field) : string =
+let field_to_string fmt inside (f : field) : string =
   match f.field_name with
-  | None -> ty_to_string fmt f.field_ty
-  | Some field_name -> field_name ^ " : " ^ ty_to_string fmt f.field_ty
+  | None -> ty_to_string fmt inside f.field_ty
+  | Some field_name ->
+      let s = field_name ^ " : " ^ ty_to_string fmt false f.field_ty in
+      if inside then "(" ^ s ^ ")" else s
 
 let variant_to_string fmt (v : variant) : string =
   v.variant_name ^ "("
-  ^ String.concat ", " (List.map (field_to_string fmt) v.fields)
+  ^ String.concat ", " (List.map (field_to_string fmt false) v.fields)
   ^ ")"
 
 let type_decl_to_string (fmt : type_formatter) (def : type_decl) : string =
@@ -174,7 +180,7 @@ let type_decl_to_string (fmt : type_formatter) (def : type_decl) : string =
       if List.length fields > 0 then
         let fields =
           String.concat ","
-            (List.map (fun f -> "\n  " ^ field_to_string fmt f) fields)
+            (List.map (fun f -> "\n  " ^ field_to_string fmt false f) fields)
         in
         "struct " ^ name ^ params ^ "{" ^ fields ^ "}"
       else "struct " ^ name ^ params ^ "{}"
@@ -193,7 +199,7 @@ let var_to_varname (v : var) : string =
 
 let var_to_string (fmt : type_formatter) (v : var) : string =
   let varname = var_to_varname v in
-  "(" ^ varname ^ " : " ^ ty_to_string fmt v.ty ^ ")"
+  "(" ^ varname ^ " : " ^ ty_to_string fmt false v.ty ^ ")"
 
 let rec mprojection_to_string (fmt : ast_formatter) (inside : string)
     (p : mprojection) : string =
@@ -380,7 +386,7 @@ let adt_g_value_to_string (fmt : value_formatter)
       raise
         (Failure
            ("Inconsistently typed value: expected ADT type but found:"
-          ^ "\n- ty: " ^ ty_to_string fmt ty ^ "\n- variant_id: "
+          ^ "\n- ty: " ^ ty_to_string fmt false ty ^ "\n- variant_id: "
            ^ Print.option_to_string VariantId.to_string variant_id))
 
 let rec typed_pattern_to_string (fmt : ast_formatter) (v : typed_pattern) :
@@ -391,7 +397,7 @@ let rec typed_pattern_to_string (fmt : ast_formatter) (v : typed_pattern) :
   | PatVar (v, Some mp) ->
       let mp = "[@mplace=" ^ mplace_to_string fmt mp ^ "]" in
       "(" ^ var_to_varname v ^ " " ^ mp ^ " : "
-      ^ ty_to_string (ast_to_type_formatter fmt) v.ty
+      ^ ty_to_string (ast_to_type_formatter fmt) false v.ty
       ^ ")"
   | PatDummy -> "_"
   | PatAdt av ->
@@ -403,15 +409,15 @@ let rec typed_pattern_to_string (fmt : ast_formatter) (v : typed_pattern) :
 let fun_sig_to_string (fmt : ast_formatter) (sg : fun_sig) : string =
   let ty_fmt = ast_to_type_formatter fmt in
   let type_params = List.map type_var_to_string sg.type_params in
-  let inputs = List.map (ty_to_string ty_fmt) sg.inputs in
-  let output = ty_to_string ty_fmt sg.output in
+  let inputs = List.map (ty_to_string ty_fmt false) sg.inputs in
+  let output = ty_to_string ty_fmt false sg.output in
   let all_types = List.concat [ type_params; inputs; [ output ] ] in
   String.concat " -> " all_types
 
 let inst_fun_sig_to_string (fmt : ast_formatter) (sg : inst_fun_sig) : string =
   let ty_fmt = ast_to_type_formatter fmt in
-  let inputs = List.map (ty_to_string ty_fmt) sg.inputs in
-  let output = ty_to_string ty_fmt sg.output in
+  let inputs = List.map (ty_to_string ty_fmt false) sg.inputs in
+  let output = ty_to_string ty_fmt false sg.output in
   let all_types = List.append inputs [ output ] in
   String.concat " -> " all_types
 
@@ -551,7 +557,7 @@ and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string)
         in
         (* Convert the type instantiation *)
         let ty_fmt = ast_to_type_formatter fmt in
-        let tys = List.map (ty_to_string ty_fmt) qualif.type_args in
+        let tys = List.map (ty_to_string ty_fmt true) qualif.type_args in
         (* *)
         (qualif_s, tys)
     | _ ->
@@ -620,15 +626,21 @@ and loop_to_string (fmt : ast_formatter) (indent : string)
     (indent_incr : string) (loop : loop) : string =
   let indent1 = indent ^ indent_incr in
   let indent2 = indent1 ^ indent_incr in
+  let type_fmt = ast_to_type_formatter fmt in
+  let loop_inputs =
+    "fresh_vars: ["
+    ^ String.concat "; " (List.map (var_to_string type_fmt) loop.inputs)
+    ^ "]"
+  in
   let fun_end =
     texpression_to_string fmt false indent2 indent_incr loop.fun_end
   in
   let loop_body =
     texpression_to_string fmt false indent2 indent_incr loop.loop_body
   in
-  "loop {\n" ^ indent1 ^ "fun_end: {\n" ^ indent2 ^ fun_end ^ "\n" ^ indent1
-  ^ "}\n" ^ indent1 ^ "loop_body: {\n" ^ indent2 ^ loop_body ^ "\n" ^ indent1
-  ^ "}\n" ^ indent ^ "}"
+  "loop {\n" ^ indent1 ^ loop_inputs ^ "\n" ^ indent1 ^ "fun_end: {\n" ^ indent2
+  ^ fun_end ^ "\n" ^ indent1 ^ "}\n" ^ indent1 ^ "loop_body: {\n" ^ indent2
+  ^ loop_body ^ "\n" ^ indent1 ^ "}\n" ^ indent ^ "}"
 
 and meta_to_string (fmt : ast_formatter) (meta : meta) : string =
   let meta =
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index b5cb3a4d..a2b41165 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -248,7 +248,7 @@ let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string =
 let ty_to_string (ctx : bs_ctx) (ty : ty) : string =
   let fmt = bs_ctx_to_pp_ast_formatter ctx in
   let fmt = PrintPure.ast_to_type_formatter fmt in
-  PrintPure.ty_to_string fmt ty
+  PrintPure.ty_to_string fmt false ty
 
 let type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string =
   let type_params = def.type_params in
@@ -808,7 +808,7 @@ let translate_fun_sig (fun_infos : FA.fun_info A.FunDeclId.Map.t)
   let sg = { type_params; inputs; output; doutputs; info } in
   { sg; output_names }
 
-let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * var * typed_pattern =
+let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * typed_pattern =
   (* Generate the fresh variable *)
   let id, var_counter = VarId.fresh ctx.var_counter in
   let state_var =
@@ -818,7 +818,7 @@ let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * var * typed_pattern =
   (* Update the context *)
   let ctx = { ctx with var_counter; state_var = id } in
   (* Return *)
-  (ctx, state_var, state_pat)
+  (ctx, state_pat)
 
 let fresh_var (basename : string option) (ty : 'r T.ty) (ctx : bs_ctx) :
     bs_ctx * var =
@@ -836,7 +836,7 @@ let fresh_named_var_for_symbolic_value (basename : string option)
   (* Generate the fresh variable *)
   let ctx, var = fresh_var basename sv.sv_ty ctx in
   (* Insert in the map *)
-  let sv_to_var = V.SymbolicValueId.Map.add sv.sv_id var ctx.sv_to_var in
+  let sv_to_var = V.SymbolicValueId.Map.add_strict sv.sv_id var ctx.sv_to_var in
   (* Update the context *)
   let ctx = { ctx with sv_to_var } in
   (* Return *)
@@ -1419,7 +1419,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
           let fuel = mk_fuel_input_as_list ctx effect_info in
           if effect_info.stateful then
             let state_var = mk_state_texpression ctx.state_var in
-            let ctx, _, nstate_var = bs_ctx_fresh_state_var ctx in
+            let ctx, nstate_var = bs_ctx_fresh_state_var ctx in
             (List.concat [ fuel; args; [ state_var ] ], ctx, Some nstate_var)
           else (List.concat [ fuel; args ], ctx, None)
         in
@@ -1611,7 +1611,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
   let back_state, ctx, nstate =
     if effect_info.stateful then
       let back_state = mk_state_texpression ctx.state_var in
-      let ctx, _, nstate = bs_ctx_fresh_state_var ctx in
+      let ctx, nstate = bs_ctx_fresh_state_var ctx in
       ([ back_state ], ctx, Some nstate)
     else ([], ctx, None)
   in
@@ -1805,7 +1805,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
       let back_state, ctx, nstate =
         if effect_info.stateful then
           let back_state = mk_state_texpression ctx.state_var in
-          let ctx, _, nstate = bs_ctx_fresh_state_var ctx in
+          let ctx, nstate = bs_ctx_fresh_state_var ctx in
           ([ back_state ], ctx, Some nstate)
         else ([], ctx, None)
       in
@@ -2144,12 +2144,11 @@ and translate_forward_end (ectx : C.eval_ctx)
          * - add the fuel
          * - add the state input argument
          * - generate a fresh state variable for the returned state
-         * TODO: we do exactly the same thing in {!translate_function_call}
          *)
         let fuel = mk_fuel_input_as_list ctx effect_info in
         if effect_info.stateful then
           let state_var = mk_state_texpression ctx.state_var in
-          let ctx, _nstate_var, nstate_pat = bs_ctx_fresh_state_var ctx in
+          let ctx, nstate_pat = bs_ctx_fresh_state_var ctx in
           ( List.concat [ fuel; args; [ state_var ] ],
             ctx,
             [ nstate_pat; output_pat ] )
@@ -2257,24 +2256,6 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
 
   (* Update the context for the loop body *)
   let ctx_loop = { ctx_end with inside_loop = true } in
-  (* We also need to introduce variables for the symbolic values which are
-     introduced in the fixed point (we have to filter the list of symbolic
-     values, to remove the not fresh ones - the fixed point introduces some
-     symbolic values and keeps some others)... *)
-  let ctx_loop =
-    let svl =
-      List.filter
-        (fun (sv : V.symbolic_value) ->
-          V.SymbolicValueId.Set.mem sv.sv_id loop.fresh_svalues)
-        loop.input_svalues
-    in
-    log#ldebug
-      (lazy
-        ("translate_loop:" ^ "\n- filtered svl: "
-        ^ (Print.list_to_string (symbolic_value_to_string ctx)) svl));
-    let ctx_loop, _ = fresh_vars_for_symbolic_values svl ctx_loop in
-    ctx_loop
-  in
 
   (* Translate the loop body *)
   let loop_body = translate_expression loop.loop_expr ctx_loop in