Merge pull request #368 from AeneasVerif/son/adt

Add some tests for structures with borrows and improve the code generation

src/Config.ml

@@ -278,6 +278,22 @@ let decompose_nested_let_patterns = ref false
  *)
 let unfold_monadic_let_bindings = ref false
 
+(** Introduce calls to [massert] (monadic assertion).
+
+    The pattern below is very frequent especially as it is introduced by
+    the [assert!] macro. If the option is [true], we perform the following
+    simplification:
+    {[
+      if b then e
+      else fail
+
+         ~~>
+      massert b;
+      e
+    ]}
+ *)
+let intro_massert = ref true
+
 (** Simplify the forward/backward functions, in case we merge them
     (i.e., the forward functions return the backward functions).
 

src/Main.ml

@@ -239,7 +239,9 @@ let () =
         match backend with
         | FStar ->
             (* F* can disambiguate the field names *)
-            record_fields_short_names := true
+            record_fields_short_names := true;
+            (* Introducing [massert] leads to type inferencing issues *)
+            intro_massert := false
         | Coq ->
             (* Some patterns are not supported *)
             decompose_monadic_let_bindings := true;

src/extract/Extract.ml

@@ -851,31 +851,43 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
         extract_texpression span ctx fmt false re;
         F.pp_print_string fmt ";";
         ctx)
-      else (
-        (* Print the "let" *)
-        if monadic then
-          match backend () with
-          | FStar ->
-              F.pp_print_string fmt "let*";
-              F.pp_print_space fmt ()
-          | Coq | Lean ->
+      else
+        (* Check if we can ignore the [let] - it is possible for some backends,
+           if the monadic expression evaluates to [()] *)
+        let ignore_let =
+          monadic && is_dummy_pattern lv && ty_is_unit lv.ty
+          && backend () = Lean
+        in
+        (* Print the [let] *)
+        let ctx =
+          if not ignore_let then (
+            if monadic then
+              match backend () with
+              | FStar ->
+                  F.pp_print_string fmt "let*";
+                  F.pp_print_space fmt ()
+              | Coq | Lean ->
+                  F.pp_print_string fmt "let";
+                  F.pp_print_space fmt ()
+              | HOL4 -> ()
+            else (
               F.pp_print_string fmt "let";
-              F.pp_print_space fmt ()
-          | HOL4 -> ()
-        else (
-          F.pp_print_string fmt "let";
-          F.pp_print_space fmt ());
-        let ctx = extract_typed_pattern span ctx fmt true true lv in
-        F.pp_print_space fmt ();
-        let eq =
-          match backend () with
-          | FStar -> "="
-          | Coq -> ":="
-          | Lean -> if monadic then "←" else ":="
-          | HOL4 -> if monadic then "<-" else "="
+              F.pp_print_space fmt ());
+            let ctx = extract_typed_pattern span ctx fmt true true lv in
+            F.pp_print_space fmt ();
+            let eq =
+              match backend () with
+              | FStar -> "="
+              | Coq -> ":="
+              | Lean -> if monadic then "←" else ":="
+              | HOL4 -> if monadic then "<-" else "="
+            in
+            F.pp_print_string fmt eq;
+            F.pp_print_space fmt ();
+            ctx)
+          else ctx
         in
-        F.pp_print_string fmt eq;
-        F.pp_print_space fmt ();
+        (* Print the bound expression *)
         extract_texpression span ctx fmt false re;
         (* End the let-binding *)
         (match backend () with
@@ -885,7 +897,7 @@ and extract_lets (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
         | Coq | FStar | HOL4 ->
             F.pp_print_space fmt ();
             F.pp_print_string fmt "in");
-        ctx)
+        ctx
     in
     (* Close the box for the let-binding *)
     F.pp_close_box fmt ();
@@ -1146,8 +1158,8 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx)
         if need_paren then F.pp_print_string fmt "(";
         F.pp_open_hvbox fmt ctx.indent_incr;
         if supd.init <> None then (
-          let var_name = ctx_get_var span (Option.get supd.init) ctx in
-          F.pp_print_string fmt var_name;
+          let init = Option.get supd.init in
+          extract_texpression span ctx fmt false init;
           F.pp_print_space fmt ();
           F.pp_print_string fmt "with";
           F.pp_print_space fmt ());
@@ -1171,11 +1183,24 @@ and extract_StructUpdate (span : Meta.span) (ctx : extraction_ctx)
             F.pp_open_hvbox fmt ctx.indent_incr;
             let f = ctx_get_field span supd.struct_id fid ctx in
             F.pp_print_string fmt f;
-            F.pp_print_string fmt (" " ^ assign);
-            F.pp_print_space fmt ();
-            F.pp_open_hvbox fmt ctx.indent_incr;
-            extract_texpression span ctx fmt true fe;
-            F.pp_close_box fmt ();
+            (* Simplification: if the field value is a variable the same
+               name as the field, we do not print it.
+
+               Example: we generate [{ x }] instead of [{ x := x }].
+            *)
+            let has_same_name =
+              match fe.e with
+              | Var vid ->
+                  let var_name = ctx_get_var span vid ctx in
+                  f = var_name
+              | _ -> false
+            in
+            if not has_same_name then (
+              F.pp_print_string fmt (" " ^ assign);
+              F.pp_print_space fmt ();
+              F.pp_open_hvbox fmt ctx.indent_incr;
+              extract_texpression span ctx fmt true fe;
+              F.pp_close_box fmt ());
             F.pp_close_box fmt ())
           supd.updates;
         F.pp_close_box fmt ();

src/interp/InterpreterStatements.ml

@@ -1372,12 +1372,6 @@ and eval_transparent_function_call_symbolic (config : config) (span : Meta.span)
          not (ty_has_nested_borrows (Some span) ctx.type_ctx.type_infos ty))
        (inst_sg.output :: inst_sg.inputs))
     span "Nested borrows are not supported yet";
-  cassert __FILE__ __LINE__
-    (List.for_all
-       (fun ty ->
-         not (ty_has_adt_with_borrows (Some span) ctx.type_ctx.type_infos ty))
-       (inst_sg.output :: inst_sg.inputs))
-    span "ADTs containing borrows are not supported yet";
   (* Evaluate the function call *)
   eval_function_call_symbolic_from_inst_sig config def.item_meta.span func
     def.signature regions_hierarchy inst_sg generics trait_method_generics

src/pure/PrintPure.ml

@@ -698,13 +698,16 @@ and switch_to_string ?(span : Meta.span option = None) (env : fmt_env)
 
 and struct_update_to_string ?(span : Meta.span option = None) (env : fmt_env)
     (indent : string) (indent_incr : string) (supd : struct_update) : string =
+  let indent1 = indent ^ indent_incr in
+  let indent2 = indent1 ^ indent_incr in
   let s =
     match supd.init with
     | None -> ""
-    | Some vid -> " " ^ var_id_to_string env vid ^ " with"
+    | Some init ->
+        " "
+        ^ texpression_to_string ~span env false indent1 indent_incr init
+        ^ " with"
   in
-  let indent1 = indent ^ indent_incr in
-  let indent2 = indent1 ^ indent_incr in
   (* The id should be a custom type decl id or an array *)
   match supd.struct_id with
   | TAdtId aid ->

src/pure/Pure.ml

@@ -963,7 +963,7 @@ and loop = {
  *)
 and struct_update = {
   struct_id : type_id;
-  init : var_id option;
+  init : texpression option;
   updates : (field_id * texpression) list;
 }