Merge pull request #3161 from FStarLang/aseem_pulse_ht_extract

Add record name in the MLE_Record node

ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml

@@ -299,7 +299,7 @@ let rec build_expr (e: mlexpr): expression =
    | MLE_CTor args -> build_constructor_expr args
    | MLE_Seq args -> build_seq args
    | MLE_Tuple l -> Exp.tuple (map build_expr l)
-   | MLE_Record (path, l) ->
+   | MLE_Record (path, _, l) ->
       let fields = map (fun (x,y) -> (path_to_ident(path, x), build_expr y)) l in
       Exp.record fields None
    | MLE_Proj (e, path) ->

src/extraction/FStar.Extraction.Krml.fst

@@ -972,7 +972,7 @@ and translate_expr' env e: expr =
   | MLE_Coerce (e, t_from, t_to) ->
       ECast (translate_expr env e, translate_type env t_to)
 
-  | MLE_Record (_, fields) ->
+  | MLE_Record (_, _, fields) ->
       EFlat (assert_lid env e.mlty, List.map (fun (field, expr) ->
         field, translate_expr env expr) fields)
 

src/extraction/FStar.Extraction.ML.Code.fst

@@ -383,7 +383,7 @@ let rec doc_of_expr (currentModule : mlsymbol) (outer : level) (e : mlexpr) : do
     | MLE_Name path ->
         text (ptsym currentModule path)
 
-    | MLE_Record (path, fields) ->
+    | MLE_Record (path, _, fields) ->
         let for1 (name, e) =
             let doc = doc_of_expr currentModule (min_op_prec, NonAssoc) e in
             reduce1 [text (ptsym currentModule (path, name)); text "="; doc] in

src/extraction/FStar.Extraction.ML.RegEmb.fst

@@ -70,7 +70,7 @@ let ml_record : Ident.lid -> list (string & mlexpr) -> mlexpr =
   fun l args ->
     let s = Ident.path_of_lid l in
     // [] -> assuming same module
-    mk (MLE_Record ([], args))
+    mk (MLE_Record ([], l |> Ident.ident_of_lid |> Ident.string_of_id, args))
 
 let ml_lam nm e =
     mk <| MLE_Fun ([(nm, MLTY_Top)], e)

src/extraction/FStar.Extraction.ML.RemoveUnusedParameters.fst

@@ -142,7 +142,7 @@ let rec elim_mlexpr' (env:env_t) (e:mlexpr') =
   | MLE_CTor(l, es) -> MLE_CTor(l, List.map (elim_mlexpr env) es)
   | MLE_Seq es -> MLE_Seq (List.map (elim_mlexpr env) es)
   | MLE_Tuple es -> MLE_Tuple (List.map (elim_mlexpr env) es)
-  | MLE_Record(syms, fields) -> MLE_Record(syms, List.map (fun (s, e) -> s, elim_mlexpr env e) fields)
+  | MLE_Record(syms, nm, fields) -> MLE_Record(syms, nm, List.map (fun (s, e) -> s, elim_mlexpr env e) fields)
   | MLE_Proj (e, p) -> MLE_Proj(elim_mlexpr env e, p)
   | MLE_If(e, e1, e2_opt) -> MLE_If(elim_mlexpr env e, elim_mlexpr env e1, BU.map_opt e2_opt (elim_mlexpr env))
   | MLE_Raise(p, es) -> MLE_Raise (p, List.map (elim_mlexpr env) es)

src/extraction/FStar.Extraction.ML.Syntax.fst

@@ -166,7 +166,9 @@ type mlexpr' =
 | MLE_CTor   of mlpath * list mlexpr
 | MLE_Seq    of list mlexpr
 | MLE_Tuple  of list mlexpr
-| MLE_Record of list mlsymbol * list (mlsymbol * mlexpr) // path of record type, and fields with values
+| MLE_Record of list mlsymbol * mlsymbol * list (mlsymbol * mlexpr) // path of record type,
+                                                                    // name of record type,
+                                                                    // and fields with values
 | MLE_Proj   of mlexpr * mlpath
 | MLE_If     of mlexpr * mlexpr * option mlexpr
 | MLE_Raise  of mlpath * list mlexpr
@@ -314,8 +316,8 @@ let rec mlexpr_to_string (e:mlexpr) =
     BU.format1 "(MLE_Seq [%s])" (String.concat "; " (List.map mlexpr_to_string es))
   | MLE_Tuple es ->
     BU.format1 "(MLE_Tuple [%s])" (String.concat "; " (List.map mlexpr_to_string es))
-  | MLE_Record (p, es) ->
-    BU.format2 "(MLE_Record (%s, [%s]))" (String.concat "; " p) (String.concat "; " (List.map (fun (x, e) -> BU.format2 "(%s, %s)" x (mlexpr_to_string e)) es))
+  | MLE_Record (p, n, es) ->
+    BU.format2 "(MLE_Record (%s, [%s]))" (String.concat "; " (p@[n])) (String.concat "; " (List.map (fun (x, e) -> BU.format2 "(%s, %s)" x (mlexpr_to_string e)) es))
   | MLE_Proj (e, p) ->
     BU.format2 "(MLE_Proj (%s, %s))" (mlexpr_to_string e) (mlpath_to_string p)
   | MLE_If (e1, e2, None) ->

src/extraction/FStar.Extraction.ML.Term.fst

@@ -374,7 +374,7 @@ let rec is_ml_value e =
     | MLE_Fun   _ -> true
     | MLE_CTor (_, exps)
     | MLE_Tuple exps -> BU.for_all is_ml_value exps
-    | MLE_Record (_, fields) -> BU.for_all (fun (_, e) -> is_ml_value e) fields
+    | MLE_Record (_, _, fields) -> BU.for_all (fun (_, e) -> is_ml_value e) fields
     | MLE_TApp (h, _) -> is_ml_value h
     | _ -> false
 
@@ -1149,7 +1149,7 @@ let maybe_eta_data_and_project_record (g:uenv) (qual : option fv_qual) (residual
         let path = List.map string_of_id (ns_of_lid tyname) in
         let fields = record_fields g tyname fields args in
         let path = no_fstar_stubs_ns path in
-        with_ty e.mlty <| MLE_Record(path, fields)
+        with_ty e.mlty <| MLE_Record (path, tyname |> ident_of_lid |> string_of_id, fields)
       | _ -> e
      in
     let resugar_and_maybe_eta qual e =