Prettier top-level lets in ML.

src/ml/FStarC_Extraction_ML_PrintML.ml

@@ -6,6 +6,7 @@ open Location
 open Pprintast
 open Ast_helper
 open Ast
+open Ppxlib.Ast_builder.Default
 open Longident
 
 open FStarC_Extraction_ML_Syntax
@@ -291,7 +292,7 @@ let rec build_expr (e: mlexpr): expression =
      let recf = match flavour with
        | Rec -> Recursive
        | NonRec -> Nonrecursive in
-     let val_bindings = map (build_binding false) lbs in
+     let val_bindings = map (build_binding false recf) lbs in
      Exp.let_ recf val_bindings (build_expr expr)
    | MLE_App (e, es) ->
       let args = map (fun x -> (Nolabel, build_expr x)) es in
@@ -383,33 +384,46 @@ and build_constructor_expr ((path, sym), exp): expression =
       Exp.construct (path_to_ident(path', name)) (Some inner)
 
 and build_fun l e =
-   match l with
-   | ({mlbinder_name=id; mlbinder_ty=ty}::tl) ->
-      let p = build_binding_pattern id in
-      Exp.fun_ Nolabel None p (build_fun tl e)
-   | [] -> build_expr e
+  let mk_binder {mlbinder_name=id; mlbinder_ty=ty} =
+    pparam_val ?loc:Location.none Nolabel None (build_binding_pattern id) in
+  pexp_function ?loc:Location.none (List.map mk_binder l) None (Pfunction_body (build_expr e))
 
 and build_case ((lhs, guard, rhs): mlbranch): case =
   {pc_lhs = (build_pattern lhs);
    pc_guard = BatOption.map build_expr guard;
    pc_rhs = (build_expr rhs)}
 
-and build_binding (toplevel: bool) (lb: mllb): value_binding =
-  (* Add a constraint on the binding (ie. an annotation) for top-level lets *)
-  let mk1 s = mkloc (String.sub s 1 (String.length s - 1)) none in
-  let ty =
-      match lb.mllb_tysc with
-      | None -> None
-      | Some ts ->
-           if lb.print_typ && toplevel
-           then let vars = List.map mk1 (ty_param_names (fst ts)) in
-                let ty = snd ts in
-                Some (build_core_type ~annots:vars ty)
-           else None
-  in
-  let e = build_expr lb.mllb_def in
-  let p = build_binding_pattern ?ty:ty lb.mllb_name in
-  (Vb.mk p e)
+(* Takes an expression [fun x y -> t] and a type [a -> b -> c] and pushes the
+type annotation into the function as far as possible:
+  [fun (x: a) (y: b) : c -> t] *)
+and build_expr_with_type (e: mlexpr) (t: mlty) : expression =
+  match e.expr, t with
+  | MLE_Fun ([], e), _ -> build_expr_with_type e t
+  | MLE_Fun ({mlbinder_name; mlbinder_ty}::ls, body), MLTY_Fun (ty1, _tag, ty2) ->
+    (* this breaks the typing information, but build_expr only looks at e.expr *)
+    let e = { e with expr = MLE_Fun (ls, body) } in
+    let argpat = build_binding_pattern ?ty:(Some (build_core_type mlbinder_ty)) mlbinder_name in
+    pexp_fun ?loc:Location.none Nolabel None argpat (build_expr_with_type e ty2)
+  | _ ->
+    let e = build_expr e in
+    let ty = build_core_type t in
+    (* Functions with no arguments are still printed as type ascriptions. *)
+    pexp_function ?loc:Location.none [] (Some (Pconstraint ty)) (Pfunction_body e)
+
+and build_binding (toplevel: bool) is_rec (lb: mllb): value_binding =
+  let e, ty =
+    match lb.mllb_tysc with
+    | Some ((_::_) as vars, ty) when toplevel && is_rec = Recursive ->
+      (* add type annotation for recursive binds to enable support for polymorphic recursion *)
+      let mk1 s = mkloc (String.sub s 1 (String.length s - 1)) none in
+      let vars = List.map mk1 (ty_param_names vars) in
+      build_expr lb.mllb_def, Some (build_core_type ~annots:vars ty)
+   | Some (_vars, ty) when toplevel ->
+      (* add type annotation to parameters and return type for top-level bindings *)
+      build_expr_with_type lb.mllb_def ty, None
+    | _ ->
+      build_expr lb.mllb_def, None in
+  Vb.mk (build_binding_pattern ?ty:ty lb.mllb_name) e
 
 let build_label_decl (sym, ty): label_declaration =
   Type.field (mk_sym sym) (build_core_type ty)
@@ -498,12 +512,12 @@ let build_module1 (m1: mlmodule1): structure_item option =
       | None   -> None)
   | MLM_Let (flav, mllbs) ->
      let recf = match flav with | Rec -> Recursive | NonRec -> Nonrecursive in
-     let bindings = map (build_binding true) mllbs in
+     let bindings = map (build_binding true recf) mllbs in
      Some (Str.value recf bindings)
   | MLM_Exn exn -> Some (Str.exception_ (build_exn exn))
   | MLM_Top expr ->
       let lb = mk_top_mllb expr in
-      let binding = build_binding true lb in
+      let binding = build_binding true Nonrecursive lb in
       Some (Str.value Nonrecursive [binding])
   | MLM_Loc (p, f) -> None
 

tests/bug-reports/closed/Bug2058.ml.expected

@@ -1,13 +1,14 @@
 open Prims
 type record1 = {
   field: Prims.string }
-let (__proj__Mkrecord1__item__field : record1 -> Prims.string) =
-  fun projectee -> match projectee with | { field;_} -> field
-let (r0 : record1) = { field = "aaa" }
+let __proj__Mkrecord1__item__field (projectee : record1) : Prims.string=
+  match projectee with | { field;_} -> field
+let r0 : record1= { field = "aaa" }
 type record2 = {
   field1: Prims.string Prims.list }
-let (__proj__Mkrecord2__item__field : record2 -> Prims.string Prims.list) =
-  fun projectee -> match projectee with | { field1 = field;_} -> field
-let (r1 : record2) = { field1 = ["aaa"] }
-let (r2 : record1) = { field = "aaa" }
-let (r3 : record2) = { field1 = ["aaa"; "bbb"] }
+let __proj__Mkrecord2__item__field (projectee : record2) :
+  Prims.string Prims.list=
+  match projectee with | { field1 = field;_} -> field
+let r1 : record2= { field1 = ["aaa"] }
+let r2 : record1= { field = "aaa" }
+let r3 : record2= { field1 = ["aaa"; "bbb"] }

tests/bug-reports/closed/Bug2595.ml.expected

@@ -2,84 +2,74 @@ open Prims
 type sum_type =
   | SumType1 of Prims.string 
   | SumType2 of Prims.nat 
-let (uu___is_SumType1 : sum_type -> Prims.bool) =
-  fun projectee ->
-    match projectee with | SumType1 _0 -> true | uu___ -> false
-let (__proj__SumType1__item___0 : sum_type -> Prims.string) =
-  fun projectee -> match projectee with | SumType1 _0 -> _0
-let (uu___is_SumType2 : sum_type -> Prims.bool) =
-  fun projectee ->
-    match projectee with | SumType2 _0 -> true | uu___ -> false
-let (__proj__SumType2__item___0 : sum_type -> Prims.nat) =
-  fun projectee -> match projectee with | SumType2 _0 -> _0
-let (test_buggy : (Prims.bool, Obj.t) Prims.dtuple2 -> sum_type) =
-  fun x ->
-    match x with
-    | Prims.Mkdtuple2 (false, x2) -> SumType1 (Obj.magic x2)
-    | Prims.Mkdtuple2 (true, x4) -> SumType2 (Obj.magic x4)
+let uu___is_SumType1 (projectee : sum_type) : Prims.bool=
+  match projectee with | SumType1 _0 -> true | uu___ -> false
+let __proj__SumType1__item___0 (projectee : sum_type) : Prims.string=
+  match projectee with | SumType1 _0 -> _0
+let uu___is_SumType2 (projectee : sum_type) : Prims.bool=
+  match projectee with | SumType2 _0 -> true | uu___ -> false
+let __proj__SumType2__item___0 (projectee : sum_type) : Prims.nat=
+  match projectee with | SumType2 _0 -> _0
+let test_buggy (x : (Prims.bool, Obj.t) Prims.dtuple2) : sum_type=
+  match x with
+  | Prims.Mkdtuple2 (false, x2) -> SumType1 (Obj.magic x2)
+  | Prims.Mkdtuple2 (true, x4) -> SumType2 (Obj.magic x4)
 type sum_type2 =
   | SumType2_1 of Prims.string * Prims.string 
   | SumType2_2 of Prims.nat * Prims.nat 
-let (uu___is_SumType2_1 : sum_type2 -> Prims.bool) =
-  fun projectee ->
-    match projectee with | SumType2_1 (_0, _1) -> true | uu___ -> false
-let (__proj__SumType2_1__item___0 : sum_type2 -> Prims.string) =
-  fun projectee -> match projectee with | SumType2_1 (_0, _1) -> _0
-let (__proj__SumType2_1__item___1 : sum_type2 -> Prims.string) =
-  fun projectee -> match projectee with | SumType2_1 (_0, _1) -> _1
-let (uu___is_SumType2_2 : sum_type2 -> Prims.bool) =
-  fun projectee ->
-    match projectee with | SumType2_2 (_0, _1) -> true | uu___ -> false
-let (__proj__SumType2_2__item___0 : sum_type2 -> Prims.nat) =
-  fun projectee -> match projectee with | SumType2_2 (_0, _1) -> _0
-let (__proj__SumType2_2__item___1 : sum_type2 -> Prims.nat) =
-  fun projectee -> match projectee with | SumType2_2 (_0, _1) -> _1
-let (test_buggy2 : (Prims.bool, Obj.t) Prims.dtuple2 -> sum_type2) =
-  fun x ->
-    match Obj.magic x with
-    | Prims.Mkdtuple2 (false, (y, z)) ->
-        SumType2_1 ((Obj.magic y), (Obj.magic z))
-    | Prims.Mkdtuple2 (true, (y, z)) ->
-        SumType2_2 ((Obj.magic y), (Obj.magic z))
-let (test_ok2 :
-  (Prims.bool, (Prims.nat * Prims.int)) Prims.dtuple2 -> sum_type2) =
-  fun x ->
-    match x with
-    | Prims.Mkdtuple2 (true, (z, y)) -> SumType2_2 (z, y)
-    | Prims.Mkdtuple2 (false, (z, y)) -> SumType2_2 (z, z)
+let uu___is_SumType2_1 (projectee : sum_type2) : Prims.bool=
+  match projectee with | SumType2_1 (_0, _1) -> true | uu___ -> false
+let __proj__SumType2_1__item___0 (projectee : sum_type2) : Prims.string=
+  match projectee with | SumType2_1 (_0, _1) -> _0
+let __proj__SumType2_1__item___1 (projectee : sum_type2) : Prims.string=
+  match projectee with | SumType2_1 (_0, _1) -> _1
+let uu___is_SumType2_2 (projectee : sum_type2) : Prims.bool=
+  match projectee with | SumType2_2 (_0, _1) -> true | uu___ -> false
+let __proj__SumType2_2__item___0 (projectee : sum_type2) : Prims.nat=
+  match projectee with | SumType2_2 (_0, _1) -> _0
+let __proj__SumType2_2__item___1 (projectee : sum_type2) : Prims.nat=
+  match projectee with | SumType2_2 (_0, _1) -> _1
+let test_buggy2 (x : (Prims.bool, Obj.t) Prims.dtuple2) : sum_type2=
+  match Obj.magic x with
+  | Prims.Mkdtuple2 (false, (y, z)) ->
+      SumType2_1 ((Obj.magic y), (Obj.magic z))
+  | Prims.Mkdtuple2 (true, (y, z)) ->
+      SumType2_2 ((Obj.magic y), (Obj.magic z))
+let test_ok2 (x : (Prims.bool, (Prims.nat * Prims.int)) Prims.dtuple2) :
+  sum_type2=
+  match x with
+  | Prims.Mkdtuple2 (true, (z, y)) -> SumType2_2 (z, y)
+  | Prims.Mkdtuple2 (false, (z, y)) -> SumType2_2 (z, z)
 type 'a mixed =
   | Mixed of 'a * Prims.int 
-let uu___is_Mixed : 'a . 'a mixed -> Prims.bool = fun projectee -> true
-let __proj__Mixed__item___0 : 'a . 'a mixed -> 'a =
-  fun projectee -> match projectee with | Mixed (_0, _1) -> _0
-let __proj__Mixed__item___1 : 'a . 'a mixed -> Prims.int =
-  fun projectee -> match projectee with | Mixed (_0, _1) -> _1
+let uu___is_Mixed (projectee : 'a mixed) : Prims.bool= true
+let __proj__Mixed__item___0 (projectee : 'a mixed) : 'a=
+  match projectee with | Mixed (_0, _1) -> _0
+let __proj__Mixed__item___1 (projectee : 'a mixed) : Prims.int=
+  match projectee with | Mixed (_0, _1) -> _1
 type t3 =
   | T3_1 of Prims.string * Prims.int 
   | T3_2 of Prims.nat * Prims.int 
-let (uu___is_T3_1 : t3 -> Prims.bool) =
-  fun projectee ->
-    match projectee with | T3_1 (_0, _1) -> true | uu___ -> false
-let (__proj__T3_1__item___0 : t3 -> Prims.string) =
-  fun projectee -> match projectee with | T3_1 (_0, _1) -> _0
-let (__proj__T3_1__item___1 : t3 -> Prims.int) =
-  fun projectee -> match projectee with | T3_1 (_0, _1) -> _1
-let (uu___is_T3_2 : t3 -> Prims.bool) =
-  fun projectee ->
-    match projectee with | T3_2 (_0, _1) -> true | uu___ -> false
-let (__proj__T3_2__item___0 : t3 -> Prims.nat) =
-  fun projectee -> match projectee with | T3_2 (_0, _1) -> _0
-let (__proj__T3_2__item___1 : t3 -> Prims.int) =
-  fun projectee -> match projectee with | T3_2 (_0, _1) -> _1
-let (test_mixed : (Prims.bool, Obj.t) Prims.dtuple2 -> t3) =
-  fun x ->
-    match Obj.magic x with
-    | Prims.Mkdtuple2 (true, Mixed (s, z)) -> T3_1 ((Obj.magic s), z)
-    | Prims.Mkdtuple2 (false, Mixed (n, z)) -> T3_2 ((Obj.magic n), z)
+let uu___is_T3_1 (projectee : t3) : Prims.bool=
+  match projectee with | T3_1 (_0, _1) -> true | uu___ -> false
+let __proj__T3_1__item___0 (projectee : t3) : Prims.string=
+  match projectee with | T3_1 (_0, _1) -> _0
+let __proj__T3_1__item___1 (projectee : t3) : Prims.int=
+  match projectee with | T3_1 (_0, _1) -> _1
+let uu___is_T3_2 (projectee : t3) : Prims.bool=
+  match projectee with | T3_2 (_0, _1) -> true | uu___ -> false
+let __proj__T3_2__item___0 (projectee : t3) : Prims.nat=
+  match projectee with | T3_2 (_0, _1) -> _0
+let __proj__T3_2__item___1 (projectee : t3) : Prims.int=
+  match projectee with | T3_2 (_0, _1) -> _1
+let test_mixed (x : (Prims.bool, Obj.t) Prims.dtuple2) : t3=
+  match Obj.magic x with
+  | Prims.Mkdtuple2 (true, Mixed (s, z)) -> T3_1 ((Obj.magic s), z)
+  | Prims.Mkdtuple2 (false, Mixed (n, z)) -> T3_2 ((Obj.magic n), z)
 type flen = Prims.pos
 type ('a, 'len) ntuple_ = Obj.t
 type ('a, 'len) ntuple = Obj.t
-let rest_ : 'a . flen -> Obj.t -> Obj.t =
-  fun len -> fun s -> FStar_Pervasives_Native.snd (Obj.magic s)
-let rest : 'a . flen -> Obj.t -> Obj.t =
-  fun len -> fun s -> match Obj.magic s with | (_1, _2) -> _2
+let rest_ (len : flen) (s : Obj.t) : Obj.t=
+  FStar_Pervasives_Native.snd (Obj.magic s)
+let rest (len : flen) (s : Obj.t) : Obj.t=
+  match Obj.magic s with | (_1, _2) -> _2

tests/bug-reports/closed/Bug2699.ml.expected

@@ -1,7 +1,7 @@
 open Prims
-let (broken_length_f32 : (FStar_UInt32.t * FStar_UInt32.t)) =
+let broken_length_f32 : (FStar_UInt32.t * FStar_UInt32.t)=
   ((FStar_UInt32.uint_to_t (Prims.of_int (24))),
     (FStar_UInt32.uint_to_t (Prims.of_int (28))))
-let (works_length_f32 : (FStar_UInt32.t * FStar_UInt32.t)) =
+let works_length_f32 : (FStar_UInt32.t * FStar_UInt32.t)=
   ((FStar_UInt32.uint_to_t (Prims.of_int (24))),
     (FStar_UInt32.uint_to_t (Prims.of_int (28))))

tests/bug-reports/closed/Bug2895.ml.expected

@@ -1,28 +1,27 @@
 open Prims
 type 't foo = 't -> Prims.bool
-let rec (f : Prims.string foo) = fun u -> false
-let (test : Prims.bool) = f "123"
+let rec f : Prims.string foo= fun u -> false
+let test : Prims.bool= f "123"
 type 't comparator_for = 't -> 't -> Prims.bool
-let rec (univ_eq : Prims.int comparator_for) = fun u1 -> fun u2 -> false
+let rec univ_eq : Prims.int comparator_for= fun u1 u2 -> false
 type ('t, 'x, 'y) cmpres = Prims.bool
 type 't comparator_for' = 't -> 't -> ('t, Obj.t, Obj.t) cmpres
-let (string_eq : Prims.string comparator_for') = fun x -> fun y -> x = y
-let (bool_eq : Prims.bool comparator_for') = fun x -> fun y -> x = y
+let string_eq : Prims.string comparator_for'= fun x y -> x = y
+let bool_eq : Prims.bool comparator_for'= fun x y -> x = y
 type sb =
   | S of Prims.string 
   | B of Prims.bool 
-let (uu___is_S : sb -> Prims.bool) =
-  fun projectee -> match projectee with | S _0 -> true | uu___ -> false
-let (__proj__S__item___0 : sb -> Prims.string) =
-  fun projectee -> match projectee with | S _0 -> _0
-let (uu___is_B : sb -> Prims.bool) =
-  fun projectee -> match projectee with | B _0 -> true | uu___ -> false
-let (__proj__B__item___0 : sb -> Prims.bool) =
-  fun projectee -> match projectee with | B _0 -> _0
-let rec (sb_eq : sb comparator_for') =
-  fun sb1 ->
-    fun sb2 ->
-      match (sb1, sb2) with
-      | (S s1, S s2) -> Obj.magic (Obj.repr (string_eq s1 s2))
-      | (B b1, B b2) -> Obj.magic (Obj.repr (bool_eq b1 b2))
-      | uu___ -> Obj.magic (Obj.repr false)
+let uu___is_S (projectee : sb) : Prims.bool=
+  match projectee with | S _0 -> true | uu___ -> false
+let __proj__S__item___0 (projectee : sb) : Prims.string=
+  match projectee with | S _0 -> _0
+let uu___is_B (projectee : sb) : Prims.bool=
+  match projectee with | B _0 -> true | uu___ -> false
+let __proj__B__item___0 (projectee : sb) : Prims.bool=
+  match projectee with | B _0 -> _0
+let rec sb_eq : sb comparator_for'=
+  fun sb1 sb2 ->
+    match (sb1, sb2) with
+    | (S s1, S s2) -> Obj.magic (Obj.repr (string_eq s1 s2))
+    | (B b1, B b2) -> Obj.magic (Obj.repr (bool_eq b1 b2))
+    | uu___ -> Obj.magic (Obj.repr false)

tests/bug-reports/closed/Bug2912.ml.expected

@@ -1,3 +1,3 @@
 open Prims
-let id : 'uuuuu . 'uuuuu -> 'uuuuu = fun x -> x
+let id (x : 'uuuuu) : 'uuuuu= x
 type pack = (unit, Obj.t) Prims.dtuple2

tests/bug-reports/closed/Bug310.ml.expected

@@ -1,21 +1,18 @@
 open Prims
 type ('a, 'a1) capture = ('a1 * 'a)
-let (struct1 : Prims.int) = Prims.int_one
-let (struct11 : Prims.int) = (Prims.of_int (2))
-let (test : (Prims.int * Prims.int)) =
+let struct1 : Prims.int= Prims.int_one
+let struct11 : Prims.int= (Prims.of_int (2))
+let test : (Prims.int * Prims.int)=
   let x = Prims.int_zero in let x1 = (Prims.of_int (2)) in (x, x1)
-let (r : unit -> unit -> (Obj.t -> Obj.t) -> Prims.int) =
-  fun uu___ -> fun uu___1 -> fun uu___2 -> Prims.int_zero
-let (g : Prims.int -> Prims.int -> Prims.int) =
-  fun uu___ -> fun uu___1 -> Prims.int_zero
-let (ko : Prims.int -> Prims.int) =
-  fun a -> let a1 = a in r () () (fun uu___ -> (Obj.magic (g a1)) uu___)
+let r (uu___ : unit) (uu___1 : unit) (uu___2 : Obj.t -> Obj.t) : Prims.int=
+  Prims.int_zero
+let g (uu___ : Prims.int) (uu___1 : Prims.int) : Prims.int= Prims.int_zero
+let ko (a : Prims.int) : Prims.int=
+  let a1 = a in r () () (fun uu___ -> (Obj.magic (g a1)) uu___)
 type record_t = {
   struct1: Prims.int ;
   constraint1: Prims.bool }
-let (__proj__Mkrecord_t__item__struct : record_t -> Prims.int) =
-  fun projectee ->
-    match projectee with | { struct1 = struct2; constraint1;_} -> struct2
-let (__proj__Mkrecord_t__item__constraint : record_t -> Prims.bool) =
-  fun projectee ->
-    match projectee with | { struct1 = struct2; constraint1;_} -> constraint1
+let __proj__Mkrecord_t__item__struct (projectee : record_t) : Prims.int=
+  match projectee with | { struct1 = struct2; constraint1;_} -> struct2
+let __proj__Mkrecord_t__item__constraint (projectee : record_t) : Prims.bool=
+  match projectee with | { struct1 = struct2; constraint1;_} -> constraint1

tests/bug-reports/closed/Bug3473.ml.expected

@@ -1,4 +1,4 @@
 open Prims
 let rec uhoh : 't . unit -> 't = fun uu___ -> uhoh ()
-let (foo : Prims.nat FStar_Pervasives_Native.option -> Prims.string) =
-  fun x -> uhoh (); "foo"
+let foo (x : Prims.nat FStar_Pervasives_Native.option) : Prims.string=
+  uhoh (); "foo"

tests/bug-reports/closed/Bug3865.ml.expected

@@ -3,14 +3,14 @@ type 't myty = 't -> 't
 type pak = {
   t: unit ;
   f: Obj.t myty }
-let (__proj__Mkpak__item__f : pak -> Obj.t myty) =
-  fun projectee -> match projectee with | { t; f;_} -> f
-let (intpak : pak) =
+let __proj__Mkpak__item__f (projectee : pak) : Obj.t myty=
+  match projectee with | { t; f;_} -> f
+let intpak : pak=
   {
     t = ();
     f = (fun x -> let x = Obj.magic x in Obj.magic (x + Prims.int_one))
   }
-let (use : unit) =
+let use : unit=
   let x = intpak.f (Obj.magic (Prims.of_int (123))) in
   FStar_IO.print_string
     (Prims.strcat (Prims.string_of_int (Obj.magic x)) "\n")

tests/bug-reports/closed/Bug3865b.ml.expected

@@ -1,5 +1,5 @@
 open Prims
 type 'dummyV0 ast0_wf_typ =
   | WfTRewrite of Prims.int * Prims.int * Obj.t ast0_wf_typ [@@deriving show]
-let uu___is_WfTRewrite uu___ =
-  fun uu___1 -> match uu___1 with | WfTRewrite _ -> true | _ -> false
+let uu___is_WfTRewrite uu___ uu___1 =
+  match uu___1 with | WfTRewrite _ -> true | _ -> false