From 8d5463de72f7426a35192b8406a134a52053624c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 15 Sep 2024 23:03:38 -0700 Subject: [PATCH 1/2] Extraction: print mllb_attrs --- src/extraction/FStar.Extraction.ML.Syntax.fst | 1 + 1 file changed, 1 insertion(+) diff --git a/src/extraction/FStar.Extraction.ML.Syntax.fst b/src/extraction/FStar.Extraction.ML.Syntax.fst index 8c73452057e..6ee9223330e 100644 --- a/src/extraction/FStar.Extraction.ML.Syntax.fst +++ b/src/extraction/FStar.Extraction.ML.Syntax.fst @@ -202,6 +202,7 @@ and mlletbinding_to_doc (lbs) = and mllb_to_doc (lb) = record [ fld "mllb_name" (doc_of_string lb.mllb_name); + fld "mllb_attrs" (list_to_doc lb.mllb_attrs mlexpr_to_doc); fld "mllb_tysc" (option_to_doc lb.mllb_tysc (fun (_, t) -> mlty_to_doc t)); fld "mllb_add_unit" (doc_of_string (string_of_bool lb.mllb_add_unit)); fld "mllb_def" (mlexpr_to_doc lb.mllb_def); From 8a0432b0aebc9328b118b46d6a1f88732d8f5f10 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 15 Sep 2024 23:03:46 -0700 Subject: [PATCH 2/2] snap --- .../generated/FStar_Extraction_ML_Syntax.ml | 27 ++++++++++++------- 1 file changed, 17 insertions(+), 10 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml index dc63e156a6c..499e8ad75c4 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Syntax.ml @@ -1091,21 +1091,28 @@ and (mllb_to_doc : mllb -> FStar_Pprint.document) = fld "mllb_name" uu___2 in let uu___2 = let uu___3 = - let uu___4 = - option_to_doc lb.mllb_tysc - (fun uu___5 -> match uu___5 with | (uu___6, t) -> mlty_to_doc t) in - fld "mllb_tysc" uu___4 in + let uu___4 = list_to_doc lb.mllb_attrs mlexpr_to_doc in + fld "mllb_attrs" uu___4 in let uu___4 = let uu___5 = let uu___6 = - let uu___7 = - FStar_Compiler_Util.string_of_bool lb.mllb_add_unit in - FStar_Pprint.doc_of_string uu___7 in - fld "mllb_add_unit" uu___6 in + option_to_doc lb.mllb_tysc + (fun uu___7 -> + match uu___7 with | (uu___8, t) -> mlty_to_doc t) in + fld "mllb_tysc" uu___6 in let uu___6 = let uu___7 = - let uu___8 = mlexpr_to_doc lb.mllb_def in fld "mllb_def" uu___8 in - [uu___7] in + let uu___8 = + let uu___9 = + FStar_Compiler_Util.string_of_bool lb.mllb_add_unit in + FStar_Pprint.doc_of_string uu___9 in + fld "mllb_add_unit" uu___8 in + let uu___8 = + let uu___9 = + let uu___10 = mlexpr_to_doc lb.mllb_def in + fld "mllb_def" uu___10 in + [uu___9] in + uu___7 :: uu___8 in uu___5 :: uu___6 in uu___3 :: uu___4 in uu___1 :: uu___2 in