Make more progress propagating the changes

5 files changed, 151 insertions, 112 deletions

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index e9b91c6e..8134144a 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -760,6 +760,8 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool)
 
     Note that lvalues can introduce new variables: we thus return an extraction
     context updated with new bindings.
+    
+    TODO: we don't need something very generic anymore
  *)
 let extract_adt_g_value
     (extract_value : extraction_ctx -> bool -> 'v -> extraction_ctx)
@@ -830,57 +832,6 @@ let rec extract_typed_lvalue (ctx : extraction_ctx) (fmt : F.formatter)
       extract_adt_g_value extract_value fmt ctx inside av.variant_id
         av.field_values v.ty
 
-let extract_place (ctx : extraction_ctx) (fmt : F.formatter) (p : place) : unit
-    =
-  let rec extract_projection (pl : projection) : unit =
-    match pl with
-    | [] ->
-        (* No projection element left: print the variable *)
-        let var_name = ctx_get_var p.var ctx in
-        F.pp_print_string fmt var_name
-    | pe :: pl ->
-        (* Extract the interior of the projection *)
-        extract_projection pl;
-        (* Match on the projection element *)
-        let def_id =
-          match pe.pkind with
-          | E.ProjAdt (def_id, None) -> def_id
-          | E.ProjAdt (_, Some _) | E.ProjOption _ | E.ProjTuple _ ->
-              (* We can't have field accesses on enumerations (variables for
-               * the fields are introduced upon the moment we match over the
-               * enumeration). We also forbid field access on tuples, because
-               * we don't have the syntax to translate that... We thus
-               * deconstruct the tuples whenever we need to have access:
-               * `let (x, y) = p in ...` *)
-              raise (Failure "Unreachable")
-        in
-        let field_name = ctx_get_field (AdtId def_id) pe.field_id ctx in
-        (* We allow to break where the "." appears *)
-        F.pp_print_break fmt 0 0;
-        F.pp_print_string fmt ".";
-        F.pp_print_string fmt field_name
-  in
-  (* We allow to break where "." appears, but we try to prevent that by
-   * wrapping in a box *)
-  F.pp_open_hovbox fmt ctx.indent_incr;
-  extract_projection p.projection;
-  F.pp_close_box fmt ()
-
-(** [inside]: see [extract_ty] *)
-let rec extract_typed_rvalue (ctx : extraction_ctx) (fmt : F.formatter)
-    (inside : bool) (v : typed_rvalue) : extraction_ctx =
-  match v.value with
-  | RvConcrete cv ->
-      ctx.fmt.extract_constant_value fmt inside cv;
-      ctx
-  | RvPlace p ->
-      extract_place ctx fmt p;
-      ctx
-  | RvAdt av ->
-      let extract_value ctx inside v = extract_typed_rvalue ctx fmt inside v in
-      extract_adt_g_value extract_value fmt ctx inside av.variant_id
-        av.field_values v.ty
-
 (** [inside]: controls the introduction of parentheses. See [extract_ty]
     
     TODO: replace the formatting boolean [inside] with something more general?
@@ -889,16 +840,17 @@ let rec extract_typed_rvalue (ctx : extraction_ctx) (fmt : F.formatter)
 let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
     (inside : bool) (e : texpression) : unit =
   match e.e with
-  | Value (rv, _) ->
-      let _ = extract_typed_rvalue ctx fmt inside rv in
-      ()
+  | Local var_id ->
+      let var_name = ctx_get_var var_id ctx in
+      F.pp_print_string fmt var_name
+  | Const cv -> ctx.fmt.extract_constant_value fmt inside cv
   | App _ ->
       let app, args = destruct_apps e in
       extract_App ctx fmt inside app args
   | Abs _ ->
       let xl, e = destruct_abs_list e in
       extract_Abs ctx fmt inside xl e
-  | Func _ ->
+  | Qualif _ ->
       (* We use the app case *)
       extract_App ctx fmt inside e []
   | Let (monadic, lv, re, next_e) ->
@@ -908,48 +860,19 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
 
 and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
     (app : texpression) (args : texpression list) : unit =
-  (* We don't do the same thing if the app is a function identifier or a "regular" expression *)
+  (* We don't do the same thing if the app is a top-level identifier (function,
+   * ADT constructor...) or a "regular" expression *)
   match app.e with
-  | Func func -> (
-      (* Function identifier *)
-      match (func.func, args) with
-      | Unop unop, [ arg ] ->
-          ctx.fmt.extract_unop (extract_texpression ctx fmt) fmt inside unop arg
-      | Binop (binop, int_ty), [ arg0; arg1 ] ->
-          ctx.fmt.extract_binop
-            (extract_texpression ctx fmt)
-            fmt inside binop int_ty arg0 arg1
-      | Regular (fun_id, rg_id), _ ->
-          if inside then F.pp_print_string fmt "(";
-          (* Open a box for the function call *)
-          F.pp_open_hovbox fmt ctx.indent_incr;
-          (* Print the function name *)
-          let fun_name = ctx_get_function fun_id rg_id ctx in
-          F.pp_print_string fmt fun_name;
-          (* Print the type parameters *)
-          List.iter
-            (fun ty ->
-              F.pp_print_space fmt ();
-              extract_ty ctx fmt true ty)
-            func.type_params;
-          (* Print the arguments *)
-          List.iter
-            (fun ve ->
-              F.pp_print_space fmt ();
-              extract_texpression ctx fmt true ve)
-            args;
-          (* Close the box for the function call *)
-          F.pp_close_box fmt ();
-          (* Return *)
-          if inside then F.pp_print_string fmt ")"
-      | _ ->
-          raise
-            (Failure
-               ("Unreachable:\n" ^ "Function: " ^ show_fun_id func.func
-              ^ ",\nNumber of arguments: "
-               ^ string_of_int (List.length args)
-               ^ ",\nArguments: "
-               ^ String.concat " " (List.map show_texpression args))))
+  | Qualif qualif -> (
+      (* Top-level qualifier *)
+      match qualif.id with
+      | Func fun_id ->
+          extract_function_call ctx fmt inside fun_id qualif.type_params args
+      | AdtCons adt_cons_id ->
+          extract_adt_cons ctx fmt inside adt_cons_id qualif.type_params args
+      | Proj proj ->
+          extract_field_projector ctx fmt inside app proj qualif.type_params
+            args)
   | _ ->
       (* "Regular" expression *)
       (* Open parentheses *)
@@ -970,6 +893,126 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       (* Close parentheses *)
       if inside then F.pp_print_string fmt ")"
 
+(** Subcase of the app case: function call *)
+and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
+    (inside : bool) (fid : fun_id) (type_args : ty list)
+    (args : texpression list) : unit =
+  match (fid, args) with
+  | Unop unop, [ arg ] ->
+      (* A unop can have *at most* one argument (the result can't be a function!).
+       * Note that the way we generate the translation, we shouldn't get the
+       * case where we have no argument (all functions are fully instantiated,
+       * and no AST transformation introduces partial calls). *)
+      ctx.fmt.extract_unop (extract_texpression ctx fmt) fmt inside unop arg
+  | Binop (binop, int_ty), [ arg0; arg1 ] ->
+      (* Number of arguments: similar to unop *)
+      ctx.fmt.extract_binop
+        (extract_texpression ctx fmt)
+        fmt inside binop int_ty arg0 arg1
+  | Regular (fun_id, rg_id), _ ->
+      if inside then F.pp_print_string fmt "(";
+      (* Open a box for the function call *)
+      F.pp_open_hovbox fmt ctx.indent_incr;
+      (* Print the function name *)
+      let fun_name = ctx_get_function fun_id rg_id ctx in
+      F.pp_print_string fmt fun_name;
+      (* Print the type parameters *)
+      List.iter
+        (fun ty ->
+          F.pp_print_space fmt ();
+          extract_ty ctx fmt true ty)
+        type_args;
+      (* Print the arguments *)
+      List.iter
+        (fun ve ->
+          F.pp_print_space fmt ();
+          extract_texpression ctx fmt true ve)
+        args;
+      (* Close the box for the function call *)
+      F.pp_close_box fmt ();
+      (* Return *)
+      if inside then F.pp_print_string fmt ")"
+  | _ ->
+      raise
+        (Failure
+           ("Unreachable:\n" ^ "Function: " ^ show_fun_id fid
+          ^ ",\nNumber of arguments: "
+           ^ string_of_int (List.length args)
+           ^ ",\nArguments: "
+           ^ String.concat " " (List.map show_texpression args)))
+
+(** Subcase of the app case: ADT constructor *)
+and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
+    (adt_cons : adt_cons_id) (type_args : ty list) (args : texpression list) :
+    unit =
+  match adt_cons.adt_id with
+  | Tuple ->
+      (* Tuple *)
+      (* For now, we only support fully applied tuple constructors *)
+      assert (List.length type_args = List.length args);
+      F.pp_print_string fmt "(";
+      Collections.List.iter_link
+        (fun () ->
+          F.pp_print_string fmt ",";
+          F.pp_print_space fmt ())
+        (fun v -> extract_texpression ctx fmt false v)
+        args;
+      F.pp_print_string fmt ")"
+  | _ ->
+      (* "Regular" ADT *)
+      (* We print something of the form: `Cons field0 ... fieldn`.
+       * We could update the code to print something of the form:
+       * `{ field0=...; ...; fieldn=...; }` in case of fully
+       * applied structure constructors.
+       *)
+      let cons =
+        match adt_cons.variant_id with
+        | Some vid -> ctx_get_variant adt_cons.adt_id vid ctx
+        | None -> ctx_get_struct adt_cons.adt_id ctx
+      in
+      let use_parentheses = inside && args <> [] in
+      if use_parentheses then F.pp_print_string fmt "(";
+      F.pp_print_string fmt cons;
+      Collections.List.iter
+        (fun v ->
+          F.pp_print_space fmt ();
+          extract_texpression ctx fmt false v)
+        args;
+      if use_parentheses then F.pp_print_string fmt ")"
+
+(** Subcase of the app case: ADT field projector.  *)
+and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter)
+    (inside : bool) (original_app : texpression) (proj : proj_kind)
+    (_proj_type_params : ty list) (args : texpression list) : unit =
+  (* We isolate the first argument (if there is), in order to pretty print the
+   * projection (`x.field` instead of `MkAdt?.field x` *)
+  match args with
+  | [ arg ] ->
+      (* Exactly one argument: pretty-print *)
+      let field_name = ctx_get_field proj.adt_id proj.field_id ctx in
+      (* Open a box *)
+      F.pp_open_hovbox fmt ctx.indent_incr;
+      (* TODO: parentheses: we do something very crude *)
+      let use_parentheses = not (is_var arg) in
+      if use_parentheses then F.pp_print_string fmt "(";
+      (* Extract the expression *)
+      extract_texpression ctx fmt false arg;
+      (* We allow to break where the "." appears *)
+      F.pp_print_break fmt 0 0;
+      F.pp_print_string fmt ".";
+      F.pp_print_string fmt field_name;
+      (* Close the parentheses *)
+      if use_parentheses then F.pp_print_string fmt ")";
+      (* Close the box *)
+      F.pp_close_box fmt ()
+  | arg :: args ->
+      (* Call extract_App again, but in such a way that the first argument is
+       * isolated *)
+      extract_App ctx fmt inside (mk_app original_app arg) args
+  | [] ->
+      (* No argument: shouldn't happen *)
+      raise (Failure "Unreachable")
+
 and extract_Abs (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
     (xl : typed_lvalue list) (e : texpression) : unit =
   (* Open a box for the abs expression *)
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 9ba1bba7..3adf4eee 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -507,13 +507,12 @@ and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string)
                   adt_cons_id.adt_id adt_cons_id.variant_id
               in
               ConstStrings.constructor_prefix ^ variant_s
-          | Proj (ProjField (adt_id, field_id)) ->
+          | Proj { adt_id; field_id } ->
               let value_fmt = ast_to_value_formatter fmt in
               let adt_s = adt_variant_to_string value_fmt adt_id None in
               let field_s = adt_field_to_string value_fmt adt_id field_id in
               (* Adopting an F*-like syntax *)
               ConstStrings.constructor_prefix ^ adt_s ^ "?." ^ field_s
-          | Proj (ProjTuple field_id) -> "MkTuple?." ^ string_of_int field_id
         in
         (* Convert the type instantiation *)
         let ty_fmt = ast_to_type_formatter fmt in
diff --git a/src/Pure.ml b/src/Pure.ml
index 2f6ddf0a..243b493e 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -363,8 +363,12 @@ type adt_cons_id = { adt_id : type_id; variant_id : variant_id option }
 [@@deriving show]
 (** An identifier for an ADT constructor *)
 
-type proj_kind = ProjField of type_id * FieldId.id | ProjTuple of int
-[@@deriving show]
+type proj_kind = { adt_id : type_id; field_id : FieldId.id } [@@deriving show]
+(** Projection kind - For now we don't support projection of tuple fields 
+    (because not all the backends have syntax for this).
+    
+    TODO: rename
+ *)
 
 type qualif_id =
   | Func of fun_id
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index b6676db4..aaae94ca 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -341,7 +341,7 @@ let mk_simpl_tuple_ty (tys : ty list) : ty =
 (** TODO: rename to "mk_..." *)
 let unit_ty : ty = Adt (Tuple, [])
 
-(** TODO: rename to "mk_..." *)
+(** TODO: rename to "mk_unit_texpression" *)
 let unit_rvalue : texpression =
   let id = AdtCons { adt_id = Tuple; variant_id = None } in
   let qualif = { id; type_params = [] } in
@@ -592,24 +592,17 @@ module TypeCheck = struct
     | Qualif qualif -> (
         match qualif.id with
         | Func _ -> () (* TODO *)
-        | Proj (ProjField (type_id, field_id)) ->
-            (* Note we can only project fields of structurs (not enumerations) *)
+        | Proj { adt_id; field_id } ->
+            (* Note we can only project fields of structures (not enumerations) *)
             let variant_id = None in
             let expected_field_tys =
-              get_adt_field_types ctx.type_decls type_id variant_id
+              get_adt_field_types ctx.type_decls adt_id variant_id
                 qualif.type_params
             in
             let expected_field_ty = FieldId.nth expected_field_tys field_id in
             let _adt_ty, field_ty = destruct_arrow e.ty in
             (* TODO: check the adt_ty *)
             assert (expected_field_ty = field_ty)
-        | Proj (ProjTuple field_id) -> (
-            let tuple_ty, field_ty = destruct_arrow e.ty in
-            match tuple_ty with
-            | Adt (Tuple, tys) ->
-                let expected_field_ty = List.nth tys field_id in
-                assert (field_ty = expected_field_ty)
-            | _ -> raise (Failure "Inconsistently typed projector"))
         | AdtCons id ->
             (* TODO: we might also want to check the out type *)
             let expected_field_tys =
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 1150f80c..3a61784c 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -1408,7 +1408,7 @@ and translate_expansion (config : config) (p : S.mplace option)
                 in
                 let gen_field_proj (field_id : FieldId.id) (dest : var) :
                     texpression =
-                  let proj_kind = ProjField (adt_id, field_id) in
+                  let proj_kind = { adt_id; field_id } in
                   let qualif = { id = Proj proj_kind; type_params } in
                   let proj_e = Qualif qualif in
                   let proj_ty = mk_arrow scrutinee.ty dest.ty in