From 22927698146e4a8efc78dc56a818630192f24c9f Mon Sep 17 00:00:00 2001 From: Aseem Rastogi Date: Tue, 12 Dec 2023 17:08:59 +0000 Subject: [PATCH 1/2] keep record name in MLE_Record --- src/extraction/FStar.Extraction.Krml.fst | 2 +- src/extraction/FStar.Extraction.ML.Code.fst | 2 +- src/extraction/FStar.Extraction.ML.RegEmb.fst | 2 +- .../FStar.Extraction.ML.RemoveUnusedParameters.fst | 2 +- src/extraction/FStar.Extraction.ML.Syntax.fst | 8 +++++--- src/extraction/FStar.Extraction.ML.Term.fst | 4 ++-- 6 files changed, 11 insertions(+), 9 deletions(-) diff --git a/src/extraction/FStar.Extraction.Krml.fst b/src/extraction/FStar.Extraction.Krml.fst index 03055995837..6d7156ac9cf 100644 --- a/src/extraction/FStar.Extraction.Krml.fst +++ b/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) diff --git a/src/extraction/FStar.Extraction.ML.Code.fst b/src/extraction/FStar.Extraction.ML.Code.fst index eda2caa7692..9651e6b4992 100644 --- a/src/extraction/FStar.Extraction.ML.Code.fst +++ b/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 diff --git a/src/extraction/FStar.Extraction.ML.RegEmb.fst b/src/extraction/FStar.Extraction.ML.RegEmb.fst index bb447c9ef6d..30a4e23ca0f 100644 --- a/src/extraction/FStar.Extraction.ML.RegEmb.fst +++ b/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) diff --git a/src/extraction/FStar.Extraction.ML.RemoveUnusedParameters.fst b/src/extraction/FStar.Extraction.ML.RemoveUnusedParameters.fst index 11b1f9dd49c..eb7a8080d60 100644 --- a/src/extraction/FStar.Extraction.ML.RemoveUnusedParameters.fst +++ b/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) diff --git a/src/extraction/FStar.Extraction.ML.Syntax.fst b/src/extraction/FStar.Extraction.ML.Syntax.fst index 29bbe08ba41..070b0fc2143 100644 --- a/src/extraction/FStar.Extraction.ML.Syntax.fst +++ b/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) -> diff --git a/src/extraction/FStar.Extraction.ML.Term.fst b/src/extraction/FStar.Extraction.ML.Term.fst index d18de01b796..72df6af7cd0 100644 --- a/src/extraction/FStar.Extraction.ML.Term.fst +++ b/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 = From 283a023a624eb85f633f47137bda5ac09df079bf Mon Sep 17 00:00:00 2001 From: Aseem Rastogi Date: Tue, 12 Dec 2023 17:09:04 +0000 Subject: [PATCH 2/2] snap --- .../fstar-lib/FStar_Extraction_ML_PrintML.ml | 2 +- .../generated/FStar_Extraction_Krml.ml | 22 ++++++++-------- .../generated/FStar_Extraction_ML_Code.ml | 26 +++++++++---------- .../generated/FStar_Extraction_ML_RegEmb.ml | 9 ++++++- ...ar_Extraction_ML_RemoveUnusedParameters.ml | 4 +-- .../generated/FStar_Extraction_ML_Syntax.ml | 13 ++++++---- .../generated/FStar_Extraction_ML_Term.ml | 14 +++++++--- 7 files changed, 53 insertions(+), 37 deletions(-) diff --git a/ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml b/ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml index 906d0899dc8..a912bf87e70 100644 --- a/ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml +++ b/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) -> diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml b/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml index a06c7da9f07..9617bbe9608 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml @@ -2462,18 +2462,18 @@ and (translate_expr' : env -> FStar_Extraction_ML_Syntax.mlexpr -> expr) = let uu___1 = translate_expr env1 e1 in let uu___2 = translate_type env1 t_to in (uu___1, uu___2) in ECast uu___ - | FStar_Extraction_ML_Syntax.MLE_Record (uu___, fields) -> - let uu___1 = - let uu___2 = assert_lid env1 e.FStar_Extraction_ML_Syntax.mlty in - let uu___3 = + | FStar_Extraction_ML_Syntax.MLE_Record (uu___, uu___1, fields) -> + let uu___2 = + let uu___3 = assert_lid env1 e.FStar_Extraction_ML_Syntax.mlty in + let uu___4 = FStar_Compiler_List.map - (fun uu___4 -> - match uu___4 with + (fun uu___5 -> + match uu___5 with | (field, expr1) -> - let uu___5 = translate_expr env1 expr1 in - (field, uu___5)) fields in - (uu___2, uu___3) in - EFlat uu___1 + let uu___6 = translate_expr env1 expr1 in + (field, uu___6)) fields in + (uu___3, uu___4) in + EFlat uu___2 | FStar_Extraction_ML_Syntax.MLE_Proj (e1, path) -> let uu___ = let uu___1 = assert_lid env1 e1.FStar_Extraction_ML_Syntax.mlty in @@ -3125,7 +3125,7 @@ let (translate : FStar_Extraction_ML_Syntax.mllib -> file Prims.list) = "Unable to translate module: %s because:\n %s\n" m_name uu___3); FStar_Pervasives_Native.None)) modules -let (uu___1714 : unit) = +let (uu___1715 : unit) = register_post_translate_type_without_decay translate_type_without_decay'; register_post_translate_type translate_type'; register_post_translate_type_decl translate_type_decl'; diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Code.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Code.ml index adf8345d757..aa235a87342 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Code.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Code.ml @@ -535,22 +535,22 @@ let rec (doc_of_expr : | FStar_Extraction_ML_Syntax.MLE_Var x -> text x | FStar_Extraction_ML_Syntax.MLE_Name path -> let uu___ = ptsym currentModule path in text uu___ - | FStar_Extraction_ML_Syntax.MLE_Record (path, fields) -> - let for1 uu___ = - match uu___ with + | FStar_Extraction_ML_Syntax.MLE_Record (path, uu___, fields) -> + let for1 uu___1 = + match uu___1 with | (name, e1) -> let doc1 = doc_of_expr currentModule (min_op_prec, NonAssoc) e1 in - let uu___1 = - let uu___2 = - let uu___3 = ptsym currentModule (path, name) in - text uu___3 in - [uu___2; text "="; doc1] in - reduce1 uu___1 in - let uu___ = - let uu___1 = FStar_Compiler_List.map for1 fields in - combine (text "; ") uu___1 in - cbrackets uu___ + let uu___2 = + let uu___3 = + let uu___4 = ptsym currentModule (path, name) in + text uu___4 in + [uu___3; text "="; doc1] in + reduce1 uu___2 in + let uu___1 = + let uu___2 = FStar_Compiler_List.map for1 fields in + combine (text "; ") uu___2 in + cbrackets uu___1 | FStar_Extraction_ML_Syntax.MLE_CTor (ctor, []) -> let name = let uu___ = is_standard_constructor ctor in diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_RegEmb.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_RegEmb.ml index c6cf09eff2f..8b2cbdecff6 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_RegEmb.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_RegEmb.ml @@ -46,7 +46,14 @@ let (ml_record : fun l -> fun args -> let s = FStar_Ident.path_of_lid l in - mk (FStar_Extraction_ML_Syntax.MLE_Record ([], args)) + let uu___ = + let uu___1 = + let uu___2 = + let uu___3 = FStar_Ident.ident_of_lid l in + FStar_Ident.string_of_id uu___3 in + ([], uu___2, args) in + FStar_Extraction_ML_Syntax.MLE_Record uu___1 in + mk uu___ let (ml_lam : FStar_Extraction_ML_Syntax.mlident -> FStar_Extraction_ML_Syntax.mlexpr -> FStar_Extraction_ML_Syntax.mlexpr) diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_RemoveUnusedParameters.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_RemoveUnusedParameters.ml index a03e118fa06..d176a94d1c3 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_RemoveUnusedParameters.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_RemoveUnusedParameters.ml @@ -164,7 +164,7 @@ let rec (elim_mlexpr' : | FStar_Extraction_ML_Syntax.MLE_Tuple es -> let uu___ = FStar_Compiler_List.map (elim_mlexpr env) es in FStar_Extraction_ML_Syntax.MLE_Tuple uu___ - | FStar_Extraction_ML_Syntax.MLE_Record (syms, fields) -> + | FStar_Extraction_ML_Syntax.MLE_Record (syms, nm, fields) -> let uu___ = let uu___1 = FStar_Compiler_List.map @@ -172,7 +172,7 @@ let rec (elim_mlexpr' : match uu___2 with | (s, e1) -> let uu___3 = elim_mlexpr env e1 in (s, uu___3)) fields in - (syms, uu___1) in + (syms, nm, uu___1) in FStar_Extraction_ML_Syntax.MLE_Record uu___ | FStar_Extraction_ML_Syntax.MLE_Proj (e1, p) -> let uu___ = let uu___1 = elim_mlexpr env e1 in (uu___1, p) in diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml index 56c4d743824..359062050a0 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml @@ -429,7 +429,8 @@ type mlexpr' = | MLE_CTor of (mlpath * mlexpr Prims.list) | MLE_Seq of mlexpr Prims.list | MLE_Tuple of mlexpr Prims.list - | MLE_Record of (mlsymbol Prims.list * (mlsymbol * mlexpr) Prims.list) + | MLE_Record of (mlsymbol Prims.list * mlsymbol * (mlsymbol * mlexpr) + Prims.list) | MLE_Proj of (mlexpr * mlpath) | MLE_If of (mlexpr * mlexpr * mlexpr FStar_Pervasives_Native.option) | MLE_Raise of (mlpath * mlexpr Prims.list) @@ -511,8 +512,9 @@ let (uu___is_MLE_Record : mlexpr' -> Prims.bool) = fun projectee -> match projectee with | MLE_Record _0 -> true | uu___ -> false let (__proj__MLE_Record__item___0 : - mlexpr' -> (mlsymbol Prims.list * (mlsymbol * mlexpr) Prims.list)) = - fun projectee -> match projectee with | MLE_Record _0 -> _0 + mlexpr' -> + (mlsymbol Prims.list * mlsymbol * (mlsymbol * mlexpr) Prims.list)) + = fun projectee -> match projectee with | MLE_Record _0 -> _0 let (uu___is_MLE_Proj : mlexpr' -> Prims.bool) = fun projectee -> match projectee with | MLE_Proj _0 -> true | uu___ -> false @@ -838,7 +840,7 @@ let rec (mlexpr_to_string : mlexpr -> Prims.string) = let uu___1 = FStar_Compiler_List.map mlexpr_to_string es in FStar_Compiler_String.concat "; " uu___1 in FStar_Compiler_Util.format1 "(MLE_Tuple [%s])" uu___ - | MLE_Record (p, es) -> + | MLE_Record (p, n, es) -> let uu___ = let uu___1 = FStar_Compiler_List.map @@ -849,7 +851,8 @@ let rec (mlexpr_to_string : mlexpr -> Prims.string) = FStar_Compiler_Util.format2 "(%s, %s)" x uu___3) es in FStar_Compiler_String.concat "; " uu___1 in FStar_Compiler_Util.format2 "(MLE_Record (%s, [%s]))" - (FStar_Compiler_String.concat "; " p) uu___ + (FStar_Compiler_String.concat "; " + (FStar_Compiler_List.op_At p [n])) uu___ | MLE_Proj (e1, p) -> let uu___ = mlexpr_to_string e1 in FStar_Compiler_Util.format2 "(MLE_Proj (%s, %s))" uu___ diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml index 3b0c04a06f6..7fcfd765d0f 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml @@ -599,9 +599,9 @@ let rec (is_ml_value : FStar_Extraction_ML_Syntax.mlexpr -> Prims.bool) = FStar_Compiler_Util.for_all is_ml_value exps | FStar_Extraction_ML_Syntax.MLE_Tuple exps -> FStar_Compiler_Util.for_all is_ml_value exps - | FStar_Extraction_ML_Syntax.MLE_Record (uu___, fields) -> + | FStar_Extraction_ML_Syntax.MLE_Record (uu___, uu___1, fields) -> FStar_Compiler_Util.for_all - (fun uu___1 -> match uu___1 with | (uu___2, e1) -> is_ml_value e1) + (fun uu___2 -> match uu___2 with | (uu___3, e1) -> is_ml_value e1) fields | FStar_Extraction_ML_Syntax.MLE_TApp (h, uu___) -> is_ml_value h | uu___ -> false @@ -1901,9 +1901,15 @@ let (maybe_eta_data_and_project_record : FStar_Compiler_List.map FStar_Ident.string_of_id uu___1 in let fields1 = record_fields g tyname fields args in let path1 = FStar_Extraction_ML_UEnv.no_fstar_stubs_ns path in + let uu___1 = + let uu___2 = + let uu___3 = + let uu___4 = FStar_Ident.ident_of_lid tyname in + FStar_Ident.string_of_id uu___4 in + (path1, uu___3, fields1) in + FStar_Extraction_ML_Syntax.MLE_Record uu___2 in FStar_Extraction_ML_Syntax.with_ty - e.FStar_Extraction_ML_Syntax.mlty - (FStar_Extraction_ML_Syntax.MLE_Record (path1, fields1)) + e.FStar_Extraction_ML_Syntax.mlty uu___1 | uu___ -> e in let resugar_and_maybe_eta qual1 e = let uu___ = eta_args g [] residualType in