From fdd822e278f495fc346b7a360147a1a7436042fe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 9 Feb 2025 18:49:21 -0800 Subject: [PATCH 01/14] Remove Prims.array --- src/basic/FStarC.Array.fsti | 4 ++++ src/basic/FStarC.Bytes.fsti | 2 +- src/basic/FStarC.Util.fsti | 1 + src/extraction/FStarC.Extraction.ML.Syntax.fsti | 2 +- src/ml/FStarC_Array.ml | 2 ++ ulib/Prims.fst | 6 ------ 6 files changed, 9 insertions(+), 8 deletions(-) create mode 100644 src/basic/FStarC.Array.fsti create mode 100644 src/ml/FStarC_Array.ml diff --git a/src/basic/FStarC.Array.fsti b/src/basic/FStarC.Array.fsti new file mode 100644 index 00000000000..3128de72e3f --- /dev/null +++ b/src/basic/FStarC.Array.fsti @@ -0,0 +1,4 @@ +module FStarC.Array + +assume new +type array : Type -> Type0 diff --git a/src/basic/FStarC.Bytes.fsti b/src/basic/FStarC.Bytes.fsti index a7407511dbd..9e1636d8a8b 100644 --- a/src/basic/FStarC.Bytes.fsti +++ b/src/basic/FStarC.Bytes.fsti @@ -17,7 +17,7 @@ module FStarC.Bytes open FStarC.Effect open FStarC.BaseTypes -type bytes = array byte +type bytes = FStarC.Array.array byte val length : bytes -> int val get: bytes -> int -> int val zero_create : int -> bytes diff --git a/src/basic/FStarC.Util.fsti b/src/basic/FStarC.Util.fsti index 1a1fa94ff63..5eec11db522 100644 --- a/src/basic/FStarC.Util.fsti +++ b/src/basic/FStarC.Util.fsti @@ -18,6 +18,7 @@ module FStarC.Util open FStarC.Effect open FStarC.Json open FStarC.BaseTypes +open FStarC.Array exception Impos diff --git a/src/extraction/FStarC.Extraction.ML.Syntax.fsti b/src/extraction/FStarC.Extraction.ML.Syntax.fsti index fcc954257e5..7e9d927ba0f 100644 --- a/src/extraction/FStarC.Extraction.ML.Syntax.fsti +++ b/src/extraction/FStarC.Extraction.ML.Syntax.fsti @@ -69,7 +69,7 @@ type mlconstant = | MLC_Float of float | MLC_Char of char | MLC_String of string -| MLC_Bytes of array byte +| MLC_Bytes of FStarC.Array.array byte type mlpattern = | MLP_Wild diff --git a/src/ml/FStarC_Array.ml b/src/ml/FStarC_Array.ml new file mode 100644 index 00000000000..df06b582563 --- /dev/null +++ b/src/ml/FStarC_Array.ml @@ -0,0 +1,2 @@ +type 't array' = 't array +type 't array = 't array' diff --git a/ulib/Prims.fst b/ulib/Prims.fst index 11fb8c45079..0435286a350 100644 --- a/ulib/Prims.fst +++ b/ulib/Prims.fst @@ -597,12 +597,6 @@ val op_disEquality: #[@@@unrefine]a: eqtype -> a -> a -> Tot bool assume new type exn : Type0 -(** [array]: TODO: should be removed. - See FStar.Seq, LowStar.Buffer, etc. *) -assume new -type array : Type -> Type0 - - (** String concatenation and its abbreviation as [^]. TODO, both should be removed in favor of what is present in FStar.String *) assume From ddf66361d82fc4c50b3750b4d12c7ee0d20fde8b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 10 Feb 2025 10:03:31 -0800 Subject: [PATCH 02/14] Update expected output (linu numbers changed) --- .../error-messages/Coercions.fst.json_output.expected | 10 +++++----- tests/error-messages/Coercions.fst.output.expected | 10 +++++----- .../NegativeTests.Neg.fst.json_output.expected | 6 +++--- .../NegativeTests.Neg.fst.output.expected | 6 +++--- tests/error-messages/PatAnnot.fst.json_output.expected | 4 ++-- tests/error-messages/PatAnnot.fst.output.expected | 4 ++-- ...t.FunctionalExtensionality.fst.json_output.expected | 2 +- .../Test.FunctionalExtensionality.fst.output.expected | 2 +- .../TestErrorLocations.fst.json_output.expected | 4 ++-- .../TestErrorLocations.fst.output.expected | 4 ++-- tests/ide/emacs/Integration.push-pop.ideout.expected | 8 ++++---- 11 files changed, 30 insertions(+), 30 deletions(-) diff --git a/tests/error-messages/Coercions.fst.json_output.expected b/tests/error-messages/Coercions.fst.json_output.expected index 59a402e094b..f39970aa947 100644 --- a/tests/error-messages/Coercions.fst.json_output.expected +++ b/tests/error-messages/Coercions.fst.json_output.expected @@ -5,17 +5,17 @@ {"msg":["Computed type 'a\nand effect GTot\nis not compatible with the annotated type 'a\nand effect Tot"],"level":"Error","range":{"def":{"file_name":"Coercions.fst","start_pos":{"line":19,"col":37},"end_pos":{"line":19,"col":38}},"use":{"file_name":"Coercions.fst","start_pos":{"line":19,"col":37},"end_pos":{"line":19,"col":38}}},"number":34,"ctx":["While typechecking the top-level declaration `let test0'`","While typechecking the top-level declaration `[@@expect_failure] let test0'`"]} >>] >> Got issues: [ -{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"Coercions.fst","start_pos":{"line":71,"col":4},"end_pos":{"line":71,"col":8}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_literal_bad`","While typechecking the top-level declaration `[@@expect_failure] let test_literal_bad`"]} +{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":674,"col":18},"end_pos":{"line":674,"col":24}},"use":{"file_name":"Coercions.fst","start_pos":{"line":71,"col":4},"end_pos":{"line":71,"col":8}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_literal_bad`","While typechecking the top-level declaration `[@@expect_failure] let test_literal_bad`"]} >>] >> Got issues: [ -{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"Coercions.fst","start_pos":{"line":74,"col":49},"end_pos":{"line":74,"col":57}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_int_nat_1`","While typechecking the top-level declaration `[@@expect_failure] let test_int_nat_1`"]} +{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":674,"col":18},"end_pos":{"line":674,"col":24}},"use":{"file_name":"Coercions.fst","start_pos":{"line":74,"col":49},"end_pos":{"line":74,"col":57}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_int_nat_1`","While typechecking the top-level declaration `[@@expect_failure] let test_int_nat_1`"]} >>] >> Got issues: [ -{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"Coercions.fst","start_pos":{"line":76,"col":55},"end_pos":{"line":76,"col":56}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_int_nat_2`","While typechecking the top-level declaration `[@@expect_failure] let test_int_nat_2`"]} +{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":674,"col":18},"end_pos":{"line":674,"col":24}},"use":{"file_name":"Coercions.fst","start_pos":{"line":76,"col":55},"end_pos":{"line":76,"col":56}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_int_nat_2`","While typechecking the top-level declaration `[@@expect_failure] let test_int_nat_2`"]} >>] >> Got issues: [ -{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"Coercions.fst","start_pos":{"line":78,"col":50},"end_pos":{"line":78,"col":51}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_int_nat_1'`","While typechecking the top-level declaration `[@@expect_failure] let test_int_nat_1'`"]} +{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":674,"col":18},"end_pos":{"line":674,"col":24}},"use":{"file_name":"Coercions.fst","start_pos":{"line":78,"col":50},"end_pos":{"line":78,"col":51}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_int_nat_1'`","While typechecking the top-level declaration `[@@expect_failure] let test_int_nat_1'`"]} >>] >> Got issues: [ -{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"Coercions.fst","start_pos":{"line":80,"col":51},"end_pos":{"line":80,"col":52}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_int_nat_2'`","While typechecking the top-level declaration `[@@expect_failure] let test_int_nat_2'`"]} +{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":674,"col":18},"end_pos":{"line":674,"col":24}},"use":{"file_name":"Coercions.fst","start_pos":{"line":80,"col":51},"end_pos":{"line":80,"col":52}}},"number":19,"ctx":["While typechecking the top-level declaration `let test_int_nat_2'`","While typechecking the top-level declaration `[@@expect_failure] let test_int_nat_2'`"]} >>] diff --git a/tests/error-messages/Coercions.fst.output.expected b/tests/error-messages/Coercions.fst.output.expected index d1c31fa4d09..721a91448f4 100644 --- a/tests/error-messages/Coercions.fst.output.expected +++ b/tests/error-messages/Coercions.fst.output.expected @@ -20,7 +20,7 @@ - Expected type Prims.nat got type Prims.int - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Prims.fst(680,18-680,24) + - See also Prims.fst(674,18-674,24) >>] >> Got issues: [ @@ -29,7 +29,7 @@ - Expected type Prims.nat got type Prims.int - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Prims.fst(680,18-680,24) + - See also Prims.fst(674,18-674,24) >>] >> Got issues: [ @@ -38,7 +38,7 @@ - Expected type Prims.nat got type Prims.int - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Prims.fst(680,18-680,24) + - See also Prims.fst(674,18-674,24) >>] >> Got issues: [ @@ -47,7 +47,7 @@ - Expected type Prims.nat got type Prims.int - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Prims.fst(680,18-680,24) + - See also Prims.fst(674,18-674,24) >>] >> Got issues: [ @@ -56,6 +56,6 @@ - Expected type Prims.nat got type Prims.int - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Prims.fst(680,18-680,24) + - See also Prims.fst(674,18-674,24) >>] diff --git a/tests/error-messages/NegativeTests.Neg.fst.json_output.expected b/tests/error-messages/NegativeTests.Neg.fst.json_output.expected index cee9400b4f5..c6bd81f6e43 100644 --- a/tests/error-messages/NegativeTests.Neg.fst.json_output.expected +++ b/tests/error-messages/NegativeTests.Neg.fst.json_output.expected @@ -1,8 +1,8 @@ >> Got issues: [ -{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":20,"col":8},"end_pos":{"line":20,"col":10}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let x`","While typechecking the top-level declaration `[@@expect_failure] let x`"]} +{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":674,"col":18},"end_pos":{"line":674,"col":24}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":20,"col":8},"end_pos":{"line":20,"col":10}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let x`","While typechecking the top-level declaration `[@@expect_failure] let x`"]} >>] >> Got issues: [ -{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":24,"col":8},"end_pos":{"line":24,"col":10}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let y`","While typechecking the top-level declaration `[@@expect_failure] let y`"]} +{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":674,"col":18},"end_pos":{"line":674,"col":24}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":24,"col":8},"end_pos":{"line":24,"col":10}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let y`","While typechecking the top-level declaration `[@@expect_failure] let y`"]} >>] >> Got issues: [ {"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":27,"col":30},"end_pos":{"line":27,"col":35}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":27,"col":30},"end_pos":{"line":27,"col":35}}},"number":19,"ctx":["While typechecking the top-level declaration `let assert_0_eq_1`","While typechecking the top-level declaration `[@@expect_failure] let assert_0_eq_1`"]} @@ -23,7 +23,7 @@ {"msg":["Subtyping check failed","Expected type _: FStar.Pervasives.result Prims.int {V? _}\ngot type FStar.Pervasives.result Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.Pervasives.fsti","start_pos":{"line":526,"col":4},"end_pos":{"line":526,"col":5}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":50,"col":45},"end_pos":{"line":50,"col":47}}},"number":19,"ctx":["While typechecking the top-level declaration `val NegativeTests.Neg.test`","While typechecking the top-level declaration `[@@expect_failure] val NegativeTests.Neg.test`"]} >>] >> Got issues: [ -{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":55,"col":25},"end_pos":{"line":55,"col":26}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let h1`","While typechecking the top-level declaration `[@@expect_failure] let h1`"]} +{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":674,"col":18},"end_pos":{"line":674,"col":24}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":55,"col":25},"end_pos":{"line":55,"col":26}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let h1`","While typechecking the top-level declaration `[@@expect_failure] let h1`"]} >>] >> Got issues: [ {"msg":["Type annotation _: Type0{NegativeTests.Neg.phi_1510} for inductive\nNegativeTests.Neg.t is not Type or eqtype, or it is eqtype but contains\nnoeq/unopteq qualifiers"],"level":"Error","range":{"def":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":59,"col":5},"end_pos":{"line":59,"col":6}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":59,"col":5},"end_pos":{"line":59,"col":6}}},"number":309,"ctx":["While typechecking the top-level declaration `type NegativeTests.Neg.t`","While typechecking the top-level declaration `[@@expect_failure] type NegativeTests.Neg.t`"]} diff --git a/tests/error-messages/NegativeTests.Neg.fst.output.expected b/tests/error-messages/NegativeTests.Neg.fst.output.expected index 498f2dbc414..6d8b1194a04 100644 --- a/tests/error-messages/NegativeTests.Neg.fst.output.expected +++ b/tests/error-messages/NegativeTests.Neg.fst.output.expected @@ -4,7 +4,7 @@ - Expected type Prims.nat got type Prims.int - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Prims.fst(680,18-680,24) + - See also Prims.fst(674,18-674,24) >>] >> Got issues: [ @@ -13,7 +13,7 @@ - Expected type Prims.nat got type Prims.int - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Prims.fst(680,18-680,24) + - See also Prims.fst(674,18-674,24) >>] >> Got issues: [ @@ -72,7 +72,7 @@ - Expected type Prims.nat got type Prims.int - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Prims.fst(680,18-680,24) + - See also Prims.fst(674,18-674,24) >>] >> Got issues: [ diff --git a/tests/error-messages/PatAnnot.fst.json_output.expected b/tests/error-messages/PatAnnot.fst.json_output.expected index 435057e1d85..e3a2a64e2d7 100644 --- a/tests/error-messages/PatAnnot.fst.json_output.expected +++ b/tests/error-messages/PatAnnot.fst.json_output.expected @@ -11,8 +11,8 @@ {"msg":["Subtyping check failed","Expected type Prims.squash Prims.l_False\ngot type Prims.unit","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"PatAnnot.fst","start_pos":{"line":40,"col":26},"end_pos":{"line":40,"col":31}},"use":{"file_name":"PatAnnot.fst","start_pos":{"line":39,"col":10},"end_pos":{"line":39,"col":12}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let s`","While typechecking the top-level declaration `[@@expect_failure] let s`"]} >>] >> Got issues: [ -{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"PatAnnot.fst","start_pos":{"line":46,"col":10},"end_pos":{"line":46,"col":11}}},"number":19,"ctx":["While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]} +{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":674,"col":18},"end_pos":{"line":674,"col":24}},"use":{"file_name":"PatAnnot.fst","start_pos":{"line":46,"col":10},"end_pos":{"line":46,"col":11}}},"number":19,"ctx":["While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]} >>] >> Got issues: [ -{"msg":["Type annotation on parameter incompatible with the expected type","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"PatAnnot.fst","start_pos":{"line":55,"col":36},"end_pos":{"line":55,"col":39}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let test3`","While typechecking the top-level declaration `[@@expect_failure] let test3`"]} +{"msg":["Type annotation on parameter incompatible with the expected type","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":674,"col":18},"end_pos":{"line":674,"col":24}},"use":{"file_name":"PatAnnot.fst","start_pos":{"line":55,"col":36},"end_pos":{"line":55,"col":39}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let test3`","While typechecking the top-level declaration `[@@expect_failure] let test3`"]} >>] diff --git a/tests/error-messages/PatAnnot.fst.output.expected b/tests/error-messages/PatAnnot.fst.output.expected index b67efbcdcae..ece939fd7fa 100644 --- a/tests/error-messages/PatAnnot.fst.output.expected +++ b/tests/error-messages/PatAnnot.fst.output.expected @@ -38,7 +38,7 @@ - Expected type Prims.nat got type Prims.int - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Prims.fst(680,18-680,24) + - See also Prims.fst(674,18-674,24) >>] >> Got issues: [ @@ -46,6 +46,6 @@ - Type annotation on parameter incompatible with the expected type - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Prims.fst(680,18-680,24) + - See also Prims.fst(674,18-674,24) >>] diff --git a/tests/error-messages/Test.FunctionalExtensionality.fst.json_output.expected b/tests/error-messages/Test.FunctionalExtensionality.fst.json_output.expected index 448ade477c8..90816250603 100644 --- a/tests/error-messages/Test.FunctionalExtensionality.fst.json_output.expected +++ b/tests/error-messages/Test.FunctionalExtensionality.fst.json_output.expected @@ -5,7 +5,7 @@ {"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Test.FunctionalExtensionality.fst","start_pos":{"line":80,"col":9},"end_pos":{"line":80,"col":43}},"use":{"file_name":"Test.FunctionalExtensionality.fst","start_pos":{"line":80,"col":2},"end_pos":{"line":80,"col":8}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let unable_to_extend_equality_to_larger_domains_1`","While typechecking the top-level declaration `[@@expect_failure] let unable_to_extend_equality_to_larger_domains_1`"]} >>] >> Got issues: [ -{"msg":["Subtyping check failed","Expected type _: Prims.int -> Prims.int\ngot type Prims.nat ^-> Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"Test.FunctionalExtensionality.fst","start_pos":{"line":92,"col":36},"end_pos":{"line":92,"col":47}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let unable_to_extend_equality_to_larger_domains_2`","While typechecking the top-level declaration `[@@expect_failure] let unable_to_extend_equality_to_larger_domains_2`"]} +{"msg":["Subtyping check failed","Expected type _: Prims.int -> Prims.int\ngot type Prims.nat ^-> Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":674,"col":18},"end_pos":{"line":674,"col":24}},"use":{"file_name":"Test.FunctionalExtensionality.fst","start_pos":{"line":92,"col":36},"end_pos":{"line":92,"col":47}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let unable_to_extend_equality_to_larger_domains_2`","While typechecking the top-level declaration `[@@expect_failure] let unable_to_extend_equality_to_larger_domains_2`"]} >>] >> Got issues: [ {"msg":["Subtyping check failed","Expected type Prims.int ^-> Prims.int\ngot type Prims.int ^-> Prims.nat","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.FunctionalExtensionality.fsti","start_pos":{"line":102,"col":60},"end_pos":{"line":102,"col":77}},"use":{"file_name":"Test.FunctionalExtensionality.fst","start_pos":{"line":142,"col":57},"end_pos":{"line":142,"col":58}}},"number":19,"ctx":["While typechecking the top-level declaration `let sub_currently_not`","While typechecking the top-level declaration `[@@expect_failure] let sub_currently_not`"]} diff --git a/tests/error-messages/Test.FunctionalExtensionality.fst.output.expected b/tests/error-messages/Test.FunctionalExtensionality.fst.output.expected index e62722efcb2..3d4feda16e4 100644 --- a/tests/error-messages/Test.FunctionalExtensionality.fst.output.expected +++ b/tests/error-messages/Test.FunctionalExtensionality.fst.output.expected @@ -21,7 +21,7 @@ - Expected type _: Prims.int -> Prims.int got type Prims.nat ^-> Prims.int - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Prims.fst(680,18-680,24) + - See also Prims.fst(674,18-674,24) >>] >> Got issues: [ diff --git a/tests/error-messages/TestErrorLocations.fst.json_output.expected b/tests/error-messages/TestErrorLocations.fst.json_output.expected index a59c4c4e37f..663e6df8e2b 100644 --- a/tests/error-messages/TestErrorLocations.fst.json_output.expected +++ b/tests/error-messages/TestErrorLocations.fst.json_output.expected @@ -11,7 +11,7 @@ {"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"TestErrorLocations.fst","start_pos":{"line":27,"col":50},"end_pos":{"line":27,"col":58}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":37,"col":10},"end_pos":{"line":37,"col":11}}},"number":19,"ctx":["While typechecking the top-level declaration `let test3`","While typechecking the top-level declaration `[@@expect_failure] let test3`"]} >>] >> Got issues: [ -{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":43,"col":20},"end_pos":{"line":43,"col":21}}},"number":19,"ctx":["While typechecking the top-level declaration `let test4`","While typechecking the top-level declaration `[@@expect_failure] let test4`"]} +{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":674,"col":18},"end_pos":{"line":674,"col":24}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":43,"col":20},"end_pos":{"line":43,"col":21}}},"number":19,"ctx":["While typechecking the top-level declaration `let test4`","While typechecking the top-level declaration `[@@expect_failure] let test4`"]} >>] >> Got issues: [ {"msg":["Could not prove post-condition","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"TestErrorLocations.fst","start_pos":{"line":46,"col":84},"end_pos":{"line":46,"col":90}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":48,"col":14},"end_pos":{"line":48,"col":19}}},"number":19,"ctx":["While typechecking the top-level declaration `let test5`","While typechecking the top-level declaration `[@@expect_failure] let test5`"]} @@ -23,7 +23,7 @@ {"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":451,"col":90},"end_pos":{"line":451,"col":102}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":62,"col":15},"end_pos":{"line":62,"col":17}}},"number":19,"ctx":["While typechecking the top-level declaration `let test7`","While typechecking the top-level declaration `[@@expect_failure] let test7`"]} >>] >> Got issues: [ -{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":66,"col":27},"end_pos":{"line":66,"col":28}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let test8`","While typechecking the top-level declaration `[@@expect_failure] let test8`"]} +{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":674,"col":18},"end_pos":{"line":674,"col":24}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":66,"col":27},"end_pos":{"line":66,"col":28}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let test8`","While typechecking the top-level declaration `[@@expect_failure] let test8`"]} >>] >> Got issues: [ {"msg":["Subtyping check failed","Expected type Type0\ngot type Type0","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"TestErrorLocations.fst","start_pos":{"line":68,"col":52},"end_pos":{"line":68,"col":66}},"use":{"file_name":"TestErrorLocations.fst","start_pos":{"line":70,"col":25},"end_pos":{"line":70,"col":34}}},"number":19,"ctx":["While typechecking the top-level declaration `val TestErrorLocations.test9`","While typechecking the top-level declaration `[@@expect_failure] val TestErrorLocations.test9`"]} diff --git a/tests/error-messages/TestErrorLocations.fst.output.expected b/tests/error-messages/TestErrorLocations.fst.output.expected index 6cd9b1b93dd..145709bf076 100644 --- a/tests/error-messages/TestErrorLocations.fst.output.expected +++ b/tests/error-messages/TestErrorLocations.fst.output.expected @@ -34,7 +34,7 @@ - Expected type Prims.nat got type Prims.int - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Prims.fst(680,18-680,24) + - See also Prims.fst(674,18-674,24) >>] >> Got issues: [ @@ -67,7 +67,7 @@ - Expected type Prims.nat got type Prims.int - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Prims.fst(680,18-680,24) + - See also Prims.fst(674,18-674,24) >>] >> Got issues: [ diff --git a/tests/ide/emacs/Integration.push-pop.ideout.expected b/tests/ide/emacs/Integration.push-pop.ideout.expected index a537345f0a0..adcf1b784ea 100644 --- a/tests/ide/emacs/Integration.push-pop.ideout.expected +++ b/tests/ide/emacs/Integration.push-pop.ideout.expected @@ -78,17 +78,17 @@ {"kind": "response", "query-id": "80", "response": [], "status": "success"} {"kind": "response", "query-id": "91", "response": [{"level": "error", "message": "- Syntax error\n", "number": 168, "ranges": [{"beg": [12, 0], "end": [12, 0], "fname": ""}]}], "status": "success"} {"kind": "response", "query-id": "98", "response": [], "status": "success"} -{"kind": "response", "query-id": "101", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type nat got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also Prims.fst(680,18-680,24)\n", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [680, 18], "end": [680, 24], "fname": "Prims.fst"}]}], "status": "failure"} +{"kind": "response", "query-id": "101", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type nat got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also Prims.fst(674,18-674,24)\n", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [674, 18], "end": [674, 24], "fname": "Prims.fst"}]}], "status": "failure"} {"kind": "response", "query-id": "107", "response": [], "status": "success"} {"kind": "response", "query-id": "108", "response": [], "status": "success"} {"kind": "response", "query-id": "112", "response": null, "status": "success"} {"kind": "response", "query-id": "114", "response": [], "status": "success"} -{"kind": "response", "query-id": "116", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type nat got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also Prims.fst(680,18-680,24)\n", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [680, 18], "end": [680, 24], "fname": "Prims.fst"}]}], "status": "failure"} +{"kind": "response", "query-id": "116", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type nat got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also Prims.fst(674,18-674,24)\n", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [674, 18], "end": [674, 24], "fname": "Prims.fst"}]}], "status": "failure"} {"kind": "response", "query-id": "118", "response": [], "status": "success"} {"kind": "response", "query-id": "119", "response": [], "status": "success"} {"kind": "response", "query-id": "122", "response": null, "status": "success"} {"kind": "response", "query-id": "124", "response": [], "status": "success"} -{"kind": "response", "query-id": "126", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type nat got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also Prims.fst(680,18-680,24)\n", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [680, 18], "end": [680, 24], "fname": "Prims.fst"}]}], "status": "failure"} +{"kind": "response", "query-id": "126", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type nat got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also Prims.fst(674,18-674,24)\n", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [674, 18], "end": [674, 24], "fname": "Prims.fst"}]}], "status": "failure"} {"kind": "response", "query-id": "128", "response": [], "status": "success"} {"kind": "response", "query-id": "130", "response": [], "status": "success"} {"kind": "response", "query-id": "133", "response": [], "status": "success"} @@ -106,7 +106,7 @@ {"kind": "response", "query-id": "191", "response": null, "status": "success"} {"kind": "response", "query-id": "192", "response": null, "status": "success"} {"kind": "response", "query-id": "194", "response": [], "status": "success"} -{"kind": "response", "query-id": "198", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type nat got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also Prims.fst(680,18-680,24)\n", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [680, 18], "end": [680, 24], "fname": "Prims.fst"}]}], "status": "failure"} +{"kind": "response", "query-id": "198", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type nat got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also Prims.fst(674,18-674,24)\n", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [674, 18], "end": [674, 24], "fname": "Prims.fst"}]}], "status": "failure"} {"kind": "response", "query-id": "200", "response": [], "status": "success"} {"kind": "response", "query-id": "204", "response": [], "status": "success"} {"kind": "response", "query-id": "205", "response": [{"level": "error", "message": "- Assertion failed\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also (13,15-13,23)\n", "number": 19, "ranges": [{"beg": [13, 8], "end": [13, 14], "fname": ""}, {"beg": [13, 15], "end": [13, 23], "fname": ""}]}], "status": "failure"} From ae2a1662ca2112f1a394e7a95c74f0d658f25948 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sat, 8 Feb 2025 18:13:55 -0800 Subject: [PATCH 03/14] lib: Use no_prelude markers --- ulib/FStar.Pervasives.Native.fst | 2 +- ulib/FStar.Pervasives.fst | 2 +- ulib/FStar.Pervasives.fsti | 4 ++-- ulib/Prims.fst | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/ulib/FStar.Pervasives.Native.fst b/ulib/FStar.Pervasives.Native.fst index f6db654977b..092aafcd999 100644 --- a/ulib/FStar.Pervasives.Native.fst +++ b/ulib/FStar.Pervasives.Native.fst @@ -13,7 +13,7 @@ See the License for the specific language governing permissions and limitations under the License. *) - +[@@"no_prelude"] module FStar.Pervasives.Native (* This is a file from the core library, dependencies must be explicit *) diff --git a/ulib/FStar.Pervasives.fst b/ulib/FStar.Pervasives.fst index dcda2f11043..bd27ca162ce 100644 --- a/ulib/FStar.Pervasives.fst +++ b/ulib/FStar.Pervasives.fst @@ -13,7 +13,7 @@ See the License for the specific language governing permissions and limitations under the License. *) - +[@@"no_prelude"] module FStar.Pervasives (* This is a file from the core library, dependencies must be explicit *) diff --git a/ulib/FStar.Pervasives.fsti b/ulib/FStar.Pervasives.fsti index a17946aa581..b1466ebd1c6 100644 --- a/ulib/FStar.Pervasives.fsti +++ b/ulib/FStar.Pervasives.fsti @@ -13,12 +13,12 @@ See the License for the specific language governing permissions and limitations under the License. *) - +[@@"no_prelude"] module FStar.Pervasives (* This is a file from the core library, dependencies must be explicit *) open Prims -include FStar.Pervasives.Native +open FStar.Pervasives.Native /// This module is implicitly opened in the scope of all other /// modules. diff --git a/ulib/Prims.fst b/ulib/Prims.fst index 11fb8c45079..08b19572be4 100644 --- a/ulib/Prims.fst +++ b/ulib/Prims.fst @@ -13,7 +13,7 @@ See the License for the specific language governing permissions and limitations under the License. *) - +[@@"no_prelude"] module Prims /// This module is implicitly opened in the scope of all other modules. From 00196e2f13bd4ce087b0cd8874e35f0fbad3ef46 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sat, 8 Feb 2025 18:14:09 -0800 Subject: [PATCH 04/14] Introduce FStar.Prelude.fsti --- ulib/FStar.Prelude.fsti | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 ulib/FStar.Prelude.fsti diff --git a/ulib/FStar.Prelude.fsti b/ulib/FStar.Prelude.fsti new file mode 100644 index 00000000000..541429d4a30 --- /dev/null +++ b/ulib/FStar.Prelude.fsti @@ -0,0 +1,6 @@ +[@@"no_prelude"] +module FStar.Prelude + +include Prims +include FStar.Pervasives.Native +include FStar.Pervasives From f22816cf78a00771a4979d56698ce23b5af49061 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sat, 8 Feb 2025 16:19:17 -0800 Subject: [PATCH 05/14] Open FStar.Prelude by default, respect [@@"no_prelude"], remove any other special handling --- src/basic/FStarC.Basefiles.fst | 26 ---- src/basic/FStarC.Basefiles.fsti | 9 -- src/fstar/FStarC.Universal.fst | 23 ++-- src/interactive/FStarC.Interactive.Ide.fst | 4 +- .../FStarC.Interactive.PushHelper.fst | 3 +- src/ml/FStarC_Parser_ParseIt.ml | 5 +- src/parser/FStarC.Parser.AST.fst | 33 +++-- src/parser/FStarC.Parser.AST.fsti | 15 ++- src/parser/FStarC.Parser.Dep.fst | 117 +++++++++--------- src/parser/FStarC.Parser.Dep.fsti | 5 +- src/parser/FStarC.Parser.Driver.fst | 10 +- src/parser/FStarC.Parser.ToDocument.fst | 10 +- src/syntax/FStarC.Syntax.DsEnv.fst | 29 +++-- src/syntax/FStarC.Syntax.DsEnv.fsti | 2 + src/tests/FStarC.Tests.Pars.fst | 2 +- src/tosyntax/FStarC.ToSyntax.Interleave.fst | 47 +------ src/tosyntax/FStarC.ToSyntax.ToSyntax.fst | 19 ++- src/tosyntax/FStarC.ToSyntax.ToSyntax.fsti | 1 - 18 files changed, 159 insertions(+), 201 deletions(-) delete mode 100644 src/basic/FStarC.Basefiles.fst delete mode 100644 src/basic/FStarC.Basefiles.fsti diff --git a/src/basic/FStarC.Basefiles.fst b/src/basic/FStarC.Basefiles.fst deleted file mode 100644 index a521ff9be45..00000000000 --- a/src/basic/FStarC.Basefiles.fst +++ /dev/null @@ -1,26 +0,0 @@ -module FStarC.Basefiles - -open FStarC -open FStarC.Effect - -module O = FStarC.Options -module BU = FStarC.Util -module E = FStarC.Errors - -let must_find (fn:string) : string = - match Find.find_file fn with - | Some f -> f - | None -> - E.raise_error0 E.Fatal_ModuleNotFound [ - E.text (BU.format1 "Unable to find required file \"%s\" in the module search path." fn); - ] - -let prims () = - match O.custom_prims() with - | Some fn -> fn (* user-specified prims *) - | None -> must_find "Prims.fst" - -let prims_basename () = BU.basename (prims ()) -let pervasives () = must_find "FStar.Pervasives.fsti" -let pervasives_basename () = BU.basename (pervasives ()) -let pervasives_native_basename () = must_find "FStar.Pervasives.Native.fst" |> BU.basename diff --git a/src/basic/FStarC.Basefiles.fsti b/src/basic/FStarC.Basefiles.fsti deleted file mode 100644 index 76410a129c7..00000000000 --- a/src/basic/FStarC.Basefiles.fsti +++ /dev/null @@ -1,9 +0,0 @@ -module FStarC.Basefiles - -open FStarC.Effect - -val prims : unit -> string -val prims_basename : unit -> string -val pervasives : unit -> string -val pervasives_basename : unit -> string -val pervasives_native_basename : unit -> string diff --git a/src/fstar/FStarC.Universal.fst b/src/fstar/FStarC.Universal.fst index 521ccd36c7c..199d86ce8e8 100644 --- a/src/fstar/FStarC.Universal.fst +++ b/src/fstar/FStarC.Universal.fst @@ -95,14 +95,14 @@ let parse (env:uenv) (pre_fn: option string) (fn:string) | Some pre_fn -> let pre_ast, _ = Parser.Driver.parse_file pre_fn in match pre_ast, ast with - | Parser.AST.Interface (lid1, decls1, _), Parser.AST.Module (lid2, decls2) + | Parser.AST.Interface {mname=lid1; decls=decls1}, Parser.AST.Module {mname=lid2; decls=decls2} when Ident.lid_equals lid1 lid2 -> let _, env = with_dsenv_of_env env (FStarC.ToSyntax.Interleave.initialize_interface lid1 decls1) in with_dsenv_of_env env (FStarC.ToSyntax.Interleave.interleave_module ast true) - | Parser.AST.Interface (lid1, _, _), Parser.AST.Module (lid2, _) -> + | Parser.AST.Interface {mname=lid1}, Parser.AST.Interface {mname=lid2} -> (* Names do not match *) Errors.raise_error lid1 Errors.Fatal_PreModuleMismatch @@ -181,8 +181,8 @@ let tc_one_fragment curmod (env:TcEnv.env_t) frag = let range_of_first_mod_decl modul = match modul with - | Parser.AST.Module (_, { Parser.AST.drange = d } :: _) - | Parser.AST.Interface (_, { Parser.AST.drange = d } :: _, _) -> d + | Parser.AST.Module {decls = d :: _} -> d.drange + | Parser.AST.Interface {decls = d :: _} -> d.drange | _ -> Range.dummyRange in let filter_lang_decls (d:FStarC.Parser.AST.decl) = @@ -218,8 +218,8 @@ let tc_one_fragment curmod (env:TcEnv.env_t) frag = let open FStarC.Parser.AST in let decls = match ast_modul with - | Module (_, decls) - | Interface (_, decls, _) -> decls + | Module {decls} + | Interface {decls} -> decls in List.filter filter_lang_decls decls in @@ -252,7 +252,14 @@ let tc_one_fragment curmod (env:TcEnv.env_t) frag = //We already have a parsed decl, usually from FStarC.Interactive.Incremental match d.d with | FStarC.Parser.AST.TopLevelModule lid -> - check_module_name_declaration (FStarC.Parser.AST.Module(lid, [d])) + let no_prelude = + d.attrs |> List.existsb (function t -> + match t.tm with + | Const (FStarC.Const.Const_string ("no_prelude", _)) -> true + | _ -> false) + in + let modul = Parser.AST.Module { mname = lid; decls = [d]; no_prelude } in + check_module_name_declaration modul | _ -> check_decls [d] ) @@ -279,7 +286,7 @@ let tc_one_fragment curmod (env:TcEnv.env_t) frag = let load_interface_decls env interface_file_name : TcEnv.env_t = let r = Pars.parse None (Pars.Filename interface_file_name) in match r with - | Pars.ASTFragment (Inl (FStarC.Parser.AST.Interface(l, decls, _)), _) -> + | Pars.ASTFragment (Inl (FStarC.Parser.AST.Interface {mname=l; decls}), _) -> snd (with_dsenv_of_tcenv env <| FStarC.ToSyntax.Interleave.initialize_interface l decls) | Pars.ASTFragment _ -> Errors.raise_error0 FStarC.Errors.Fatal_ParseErrors diff --git a/src/interactive/FStarC.Interactive.Ide.fst b/src/interactive/FStarC.Interactive.Ide.fst index 3593ea83539..3d4ad6bf2ca 100644 --- a/src/interactive/FStarC.Interactive.Ide.fst +++ b/src/interactive/FStarC.Interactive.Ide.fst @@ -537,8 +537,8 @@ let run_segment (st: repl_state) (code: string) = match Parser.Driver.parse_fragment None frag with | Parser.Driver.Empty -> [] | Parser.Driver.Decls decls - | Parser.Driver.Modul (Parser.AST.Module (_, decls)) - | Parser.Driver.Modul (Parser.AST.Interface (_, decls, _)) -> decls in + | Parser.Driver.Modul (Parser.AST.Module {decls}) + | Parser.Driver.Modul (Parser.AST.Interface {decls}) -> decls in match with_captured_errors st.repl_env Util.sigint_ignore (fun _ -> Some <| collect_decls ()) with diff --git a/src/interactive/FStarC.Interactive.PushHelper.fst b/src/interactive/FStarC.Interactive.PushHelper.fst index 0ae6fae5d77..922999449c4 100644 --- a/src/interactive/FStarC.Interactive.PushHelper.fst +++ b/src/interactive/FStarC.Interactive.PushHelper.fst @@ -364,7 +364,8 @@ let add_module_completions this_fname deps table = let loaded_mods_set = List.fold_left (fun acc dep -> psmap_add acc (Parser.Dep.lowercase_module_name dep) true) - (psmap_empty ()) (Basefiles.prims () :: deps) in // Prims is an implicit dependency + (psmap_empty ()) deps + in let loaded modname = psmap_find_default loaded_mods_set modname false in let this_mod_key = diff --git a/src/ml/FStarC_Parser_ParseIt.ml b/src/ml/FStarC_Parser_ParseIt.ml index 95239de317d..b061801088e 100644 --- a/src/ml/FStarC_Parser_ParseIt.ml +++ b/src/ml/FStarC_Parser_ParseIt.ml @@ -393,10 +393,7 @@ let parse (lang_opt:lang_opts) fn = let frags = match fileOrFragment with | FStar_Pervasives.Inl modul -> if has_extension filename interface_extensions - then match modul with - | FStarC_Parser_AST.Module(l,d) -> - FStar_Pervasives.Inl (FStarC_Parser_AST.Interface(l, d, true)) - | _ -> failwith "Impossible" + then FStar_Pervasives.Inl (FStarC_Parser_AST.as_interface modul) else FStar_Pervasives.Inl modul | _ -> fileOrFragment in ASTFragment (frags, FStarC_Parser_Util.flush_comments ()) diff --git a/src/parser/FStarC.Parser.AST.fst b/src/parser/FStarC.Parser.AST.fst index 2e7d6cbdb7a..9200bb24c4c 100644 --- a/src/parser/FStarC.Parser.AST.fst +++ b/src/parser/FStarC.Parser.AST.fst @@ -48,8 +48,8 @@ instance hasRange_decl : hasRange decl = { let lid_of_modul (m:modul) : lid = match m with - | Module(lid, _) -> lid - | Interface (lid, _, _) -> lid + | Module {mname} + | Interface {mname} -> mname let check_id id = let first_char = String.substring (string_of_id id) 0 1 in @@ -251,16 +251,16 @@ let rec extract_named_refinement (remove_parens:bool) (t1:term) : option (ident //NS: needed to hoist this to workaround a bootstrapping bug // leaving it within as_frag causes the type-checker to take a very long time, perhaps looping -let rec as_mlist (cur: (lid & decl) & list decl) (ds:list decl) : modul = - let ((m_name, m_decl), cur) = cur in +let rec as_mlist (cur: (lid & decl & bool) & list decl) (ds:list decl) : modul = + let ((m_name, m_decl, no_prelude), cur) = cur in match ds with - | [] -> Module(m_name, m_decl :: List.rev cur) + | [] -> Module { no_prelude; mname = m_name; decls = m_decl :: List.rev cur } | d :: ds -> begin match d.d with | TopLevelModule m' -> raise_error d Fatal_UnexpectedModuleDeclaration "Unexpected module declaration" | _ -> - as_mlist ((m_name, m_decl), d::cur) ds + as_mlist ((m_name, m_decl, no_prelude), d::cur) ds end let as_frag (ds:list decl) : inputFragment = @@ -270,7 +270,13 @@ let as_frag (ds:list decl) : inputFragment = in match d.d with | TopLevelModule m -> - let m = as_mlist ((m,d), []) ds in + let no_prelude = + d.attrs |> List.existsb (function t -> + match t.tm with + | Const (FStarC.Const.Const_string ("no_prelude", _)) -> true + | _ -> false) + in + let m = as_mlist ((m,d, no_prelude), []) ds in Inl m | _ -> let ds = d::ds in @@ -799,10 +805,11 @@ let rec decl_to_string (d:decl) = match d.d with | Unparseable -> "unparseable" -let modul_to_string (m:modul) = match m with - | Module (_, decls) - | Interface (_, decls, _) -> - decls |> List.map decl_to_string |> String.concat "\n" +let modul_to_string (m:modul) = + match m with + | Module {decls} + | Interface {decls} -> + decls |> List.map decl_to_string |> String.concat "\n" let decl_is_val id decl = match decl.d with @@ -863,3 +870,7 @@ let mk_decl d r decorations = let d = { d=d; drange=r; quals=[]; attrs=[]; interleaved=false } in add_decorations d decorations +let as_interface (m:modul) : modul = + match m with + | Module {no_prelude; mname; decls} -> Interface { no_prelude; mname; decls; admitted = true } + | i -> i diff --git a/src/parser/FStarC.Parser.AST.fsti b/src/parser/FStarC.Parser.AST.fsti index 778b8d3f61f..d8434d214e0 100644 --- a/src/parser/FStarC.Parser.AST.fsti +++ b/src/parser/FStarC.Parser.AST.fsti @@ -288,8 +288,17 @@ and effect_decl = instance val hasRange_decl : hasRange decl type modul = - | Module of lid & list decl - | Interface of lid & list decl & bool (* flag to mark admitted interfaces *) + | Module { + no_prelude : bool; + mname : lid; + decls : list decl; + } + | Interface { + no_prelude : bool; + mname : lid; + decls : list decl; + admitted : bool; (* flag to mark admitted interfaces *) + } type file = modul type inputFragment = either file (list decl) @@ -365,3 +374,5 @@ val idents_of_binders : list binder -> range -> list ident instance val showable_decl : showable decl instance val showable_term : showable term + +val as_interface (m:modul) : modul diff --git a/src/parser/FStarC.Parser.Dep.fst b/src/parser/FStarC.Parser.Dep.fst index 979a94c2cc4..99878ec7c59 100644 --- a/src/parser/FStarC.Parser.Dep.fst +++ b/src/parser/FStarC.Parser.Dep.fst @@ -190,8 +190,10 @@ type parsing_data_elt = | P_lid of lident //record_lid | P_inline_for_extraction -type parsing_data = - | Mk_pd of list parsing_data_elt +type parsing_data = { + elts : list parsing_data_elt; + no_prelude : bool; +} let str_of_parsing_data_elt elt = let str_of_open_kind = function @@ -207,18 +209,25 @@ let str_of_parsing_data_elt elt = | P_lid lid -> "P_lid (" ^ (string_of_lid lid) ^ ")" | P_inline_for_extraction -> "P_inline_for_extraction" -let str_of_parsing_data = function - | Mk_pd l -> - l |> List.fold_left (fun s elt -> s ^ "; " ^ (elt |> str_of_parsing_data_elt)) "" +instance showable_parsing_data_elt : showable parsing_data_elt = { + show = str_of_parsing_data_elt; +} + +let str_of_parsing_data pd = + "{ elts = " ^ show pd.elts ^ + "; no_prelude = " ^ show pd.no_prelude ^ + "}" + +instance showable_parsing_data : showable parsing_data = { + show = str_of_parsing_data; +} let friends (p:parsing_data) : list lident = - let Mk_pd p = p in List.collect (function | P_dep (true, l) -> [l] | _ -> []) - p - + p.elts let parsing_data_elt_eq (e1:parsing_data_elt) (e2:parsing_data_elt) = match e1, e2 with @@ -232,7 +241,7 @@ let parsing_data_elt_eq (e1:parsing_data_elt) (e2:parsing_data_elt) = | P_inline_for_extraction, P_inline_for_extraction -> true | _, _ -> false -let empty_parsing_data = Mk_pd [] +let empty_parsing_data = { elts = []; no_prelude = false } type deps = { dep_graph:dependence_graph; //dependences of the entire project, not just those reachable from the command line @@ -538,33 +547,6 @@ let check_module_declaration_against_filename (lid: lident) (filename: string): exception Exit -(* In public interface *) - -let core_modules () = [ "Prims"; "FStar.Pervasives"; "FStar.Pervasives.Native" ] - -let implicit_ns_deps = - [ Const.fstar_ns_lid ] - -let implicit_module_deps = - [ Const.prims_lid; Const.pervasives_lid ] - -let hard_coded_dependencies full_filename = - let filename : string = basename full_filename in - - let implicit_module_deps = List.map (fun l -> l, Open_module) implicit_module_deps in - let implicit_ns_deps = List.map (fun l -> l, Open_namespace) implicit_ns_deps in - - (* The core libraries do not have any implicit dependencies *) - if List.mem (module_name_of_file filename) (core_modules ()) then [] - else match namespace_of_module (module_name_of_file full_filename) with - | None -> implicit_ns_deps @ implicit_module_deps - (* - * AR: we open FStar, and then ns - * which means that enter_namespace will be called first for F*, and then for ns - * giving precedence to My.M over FStar.M - *) - | Some ns -> implicit_ns_deps @ implicit_module_deps @ [(ns, Open_namespace)] - let dep_subsumed_by d d' = match d, d' with | PreferInterface l', FriendImplementation l -> l=l' @@ -618,6 +600,11 @@ let enter_namespace ); !found +let prelude : list (open_kind & lid) = [ + (Open_namespace, Const.fstar_ns_lid); + (Open_module, Ident.lid_of_str "FStar.Prelude"); +] + (* * Get parsing data for a file * First see if the data in the checked file is good (using the provided callback) @@ -651,17 +638,23 @@ let collect_one = let deps : ref (list dependence) = mk_ref [] in let has_inline_for_extraction = mk_ref false in - + let mname = lowercase_module_name filename in let mo_roots = - let mname = lowercase_module_name filename in if is_interface filename && has_implementation original_map mname then [ UseImplementation mname ] else [] in - let auto_open = hard_coded_dependencies filename |> List.map (fun (lid, k) -> - P_implicit_open_module_or_namespace (k, lid)) + let auto_open = + if pd.no_prelude + then [] + else + (prelude |> List.map (fun (k, l) -> P_open (false, l))) + @ + (match namespace_of_module mname with + | None -> [] + | Some ns -> [ P_implicit_open_module_or_namespace (Open_namespace, ns) ]) in let working_map = SMap.copy original_map in @@ -777,17 +770,15 @@ let collect_one * Iterate over the parsing data elements *) begin - match pd with - | Mk_pd l -> - (auto_open @ l) |> List.iter (fun elt -> - match elt with - | P_begin_module lid -> begin_module lid - | P_open (b, lid) -> record_open b lid - | P_implicit_open_module_or_namespace (k, lid) -> record_implicit_open_module_or_namespace (lid, k) - | P_dep (b, lid) -> add_dep_on_module lid b - | P_alias (id, lid) -> ignore (record_module_alias id lid) - | P_lid lid -> record_lid lid - | P_inline_for_extraction -> set_interface_inlining ()) + (auto_open @ pd.elts) |> List.iter (fun elt -> + match elt with + | P_begin_module lid -> begin_module lid + | P_open (b, lid) -> record_open b lid + | P_implicit_open_module_or_namespace (k, lid) -> record_implicit_open_module_or_namespace (lid, k) + | P_dep (b, lid) -> add_dep_on_module lid b + | P_alias (id, lid) -> ignore (record_module_alias id lid) + | P_lid lid -> record_lid lid + | P_inline_for_extraction -> set_interface_inlining ()) end; (* * And then return the dependences @@ -809,18 +800,23 @@ let collect_one else //parse the file and traverse the AST to collect parsing data let num_of_toplevelmods = mk_ref 0 in - let pd : ref (list parsing_data_elt) = mk_ref [] in + let pd : ref parsing_data = mk_ref empty_parsing_data in let add_to_parsing_data elt = - if not (List.existsML (fun e -> parsing_data_elt_eq e elt) !pd) - then pd := elt::!pd + if not (List.existsML (fun e -> parsing_data_elt_eq e elt) (!pd).elts) + then pd := { !pd with elts = elt::(!pd).elts } + in + + let set_no_prelude b = + pd := { !pd with no_prelude = b } in let rec collect_module = function - | Module (lid, decls) - | Interface (lid, decls, _) -> - check_module_declaration_against_filename lid filename; - add_to_parsing_data (P_begin_module lid); + | Module {no_prelude; mname; decls} + | Interface {no_prelude; mname; decls} -> + set_no_prelude no_prelude; + check_module_declaration_against_filename mname filename; + add_to_parsing_data (P_begin_module mname); collect_decls decls and collect_decls decls = @@ -1230,7 +1226,8 @@ let collect_one in let ast, _ = Driver.parse_file filename in collect_module ast; - let pd = Mk_pd (List.rev !pd) in + let pd = !pd in + let pd = { pd with elts = List.rev pd.elts } in let deps, has_inline_for_extraction, mo_roots = from_parsing_data pd original_map filename in (* Util.print2 "Deps for %s: %s\n" filename (String.concat " " (!deps)); *) pd, deps, has_inline_for_extraction, mo_roots @@ -1498,7 +1495,7 @@ let collect (all_cmd_line_files: list file_name) begin let parsing_data, (deps, mo_roots, needs_interface_inlining) = match SMap.try_find !collect_one_cache file_name with - | Some cached -> Mk_pd [], cached + | Some cached -> empty_parsing_data, cached | None -> let parsing_data, deps, needs_interface_inlining, additional_roots = collect_one file_system_map file_name get_parsing_data_from_cache in parsing_data, (deps, additional_roots, needs_interface_inlining) in diff --git a/src/parser/FStarC.Parser.Dep.fsti b/src/parser/FStarC.Parser.Dep.fsti index f8945c46cb1..dd9749ef59b 100644 --- a/src/parser/FStarC.Parser.Dep.fsti +++ b/src/parser/FStarC.Parser.Dep.fsti @@ -30,10 +30,7 @@ val lowercase_module_name : string -> string val build_inclusion_candidates_list : unit -> list (string & string) -val core_modules (_: unit) : list string -(* Given a filename, returns the list of automatically opened modules -and namespaces *) -val hard_coded_dependencies : string -> list (lident & open_kind) +val prelude : list (open_kind & lid) val is_interface: string -> bool val is_implementation: string -> bool diff --git a/src/parser/FStarC.Parser.Driver.fst b/src/parser/FStarC.Parser.Driver.fst index deef1b1833a..297b19bcab5 100644 --- a/src/parser/FStarC.Parser.Driver.fst +++ b/src/parser/FStarC.Parser.Driver.fst @@ -43,13 +43,13 @@ let parse_fragment lang_opt (frag: ParseIt.input_frag) : fragment = let maybe_dump_module (m:modul) = match m with - | Module (l, ds) - | Interface (l, ds, _) -> - if FStarC.Options.dump_module (Ident.string_of_lid l) + | Module {mname; decls} + | Interface {mname; decls} -> + if FStarC.Options.dump_module (Ident.string_of_lid mname) then ( print2 "Parsed module %s\n%s\n" - (Ident.string_of_lid l) - (List.map show ds |> String.concat "\n") + (show mname) + (List.map show decls |> String.concat "\n") ) (* Returns a non-desugared AST (as in [parser/ast.fs]) or aborts. *) let parse_file fn = diff --git a/src/parser/FStarC.Parser.ToDocument.fst b/src/parser/FStarC.Parser.ToDocument.fst index a8a4c35f0d1..d4c80fcb65a 100644 --- a/src/parser/FStarC.Parser.ToDocument.fst +++ b/src/parser/FStarC.Parser.ToDocument.fst @@ -2285,9 +2285,9 @@ let binder_to_document b = p_binder true b let modul_to_document (m:modul) = match m with - | Module (_, decls) - | Interface (_, decls, _) -> - decls |> List.map decl_to_document |> separate hardline + | Module {decls} + | Interface {decls} -> + separate_map hardline p_decl decls let comments_to_document (comments : list (string & FStarC.Range.range)) = separate_map hardline (fun (comment, range) -> str comment) comments @@ -2323,8 +2323,8 @@ let decls_with_comments_to_document (decls:list decl) comments = (* are described in the ``Taking care of comments`` section *) let modul_with_comments_to_document (m:modul) comments = let decls = match m with - | Module (_, decls) - | Interface (_, decls, _) -> decls + | Module {decls} + | Interface {decls} -> decls in decls_with_comments_to_document decls comments diff --git a/src/syntax/FStarC.Syntax.DsEnv.fst b/src/syntax/FStarC.Syntax.DsEnv.fst index baa3fc7d831..f0b9ea76180 100644 --- a/src/syntax/FStarC.Syntax.DsEnv.fst +++ b/src/syntax/FStarC.Syntax.DsEnv.fst @@ -101,7 +101,8 @@ type env = { remaining_iface_decls:list (lident&list Parser.AST.decl); (* A map from interface names to their stil-to-be-processed top-level decls *) syntax_only: bool; (* Whether next push should skip type-checking *) ds_hooks: dsenv_hooks; (* hooks that the interactive more relies onto for symbol tracking *) - dep_graph: FStarC.Parser.Dep.deps + dep_graph: FStarC.Parser.Dep.deps; + no_prelude: bool; (* whether the module was marked no_prelude *) } and dsenv_hooks = { ds_push_open_hook : env -> open_module_or_namespace -> unit; @@ -189,7 +190,9 @@ let empty_env deps = {curmodule=None; remaining_iface_decls=[]; syntax_only=false; ds_hooks=default_ds_hooks; - dep_graph=deps} + dep_graph=deps; + no_prelude=false; + } let dep_graph env = env.dep_graph let set_dep_graph env ds = {env with dep_graph=ds} let sigmap env = env.sigmap @@ -1435,13 +1438,15 @@ let as_exported_id_set (e:option exported_ids) = type module_inclusion_info = { mii_exported_ids:option exported_ids; mii_trans_exported_ids:option exported_ids; - mii_includes:option (list (lident & restriction)) + mii_includes:option (list (lident & restriction)); + mii_no_prelude:bool; } let default_mii = { mii_exported_ids=None; mii_trans_exported_ids=None; - mii_includes=None + mii_includes=None; + mii_no_prelude=false; } let as_includes = function @@ -1456,21 +1461,26 @@ let inclusion_info env (l:lident) = { mii_exported_ids = as_ids_opt env.exported_ids; mii_trans_exported_ids = as_ids_opt env.trans_exported_ids; - mii_includes = BU.map_opt (SMap.try_find env.includes mname) (fun r -> !r) + mii_includes = BU.map_opt (SMap.try_find env.includes mname) (fun r -> !r); + mii_no_prelude = env.no_prelude; } let prepare_module_or_interface intf admitted env mname (mii:module_inclusion_info) = (* AR: open the pervasives namespace *) let prep env = let filename = BU.strcat (string_of_lid mname) ".fst" in - let auto_open = FStarC.Parser.Dep.hard_coded_dependencies filename in + let auto_open = if mii.mii_no_prelude then [] else FStarC.Parser.Dep.prelude in let auto_open = let convert_kind = function | FStarC.Parser.Dep.Open_namespace -> Open_namespace | FStarC.Parser.Dep.Open_module -> Open_module in - List.map (fun (lid, kind) -> (lid, convert_kind kind, Unrestricted)) auto_open + auto_open |> List.map (fun (kind, lid) -> (lid, convert_kind kind, Unrestricted)) + in + let namespace_of_module = + if List.length (ns_of_lid mname) > 0 + then [ (lid_of_ids (ns_of_lid mname), Open_namespace, Unrestricted) ] + else [] in - let namespace_of_module = if List.length (ns_of_lid mname) > 0 then [ (lid_of_ids (ns_of_lid mname), Open_namespace, Unrestricted) ] else [] in (* [scope_mods] is a stack, so reverse the order *) let auto_open = namespace_of_module @ List.rev auto_open in @@ -1586,3 +1596,6 @@ let resolve_name (e:env) (name:lident) ) | Some (Eff_name(se, l)) -> Some (Inr (S.lid_and_dd_as_fv l None)) + +let set_no_prelude (e:env) (b:bool) = + { e with no_prelude = b } diff --git a/src/syntax/FStarC.Syntax.DsEnv.fsti b/src/syntax/FStarC.Syntax.DsEnv.fsti index 357c122bfd3..71ed10ec6d2 100644 --- a/src/syntax/FStarC.Syntax.DsEnv.fsti +++ b/src/syntax/FStarC.Syntax.DsEnv.fsti @@ -137,3 +137,5 @@ val prepare_module_or_interface: bool -> bool -> env -> lident -> module_inclusi (* private *) val unique: bool -> bool -> env -> lident -> bool (* private *) val check_admits: env -> modul -> modul (* private *) val finish: env -> modul -> env + +val set_no_prelude : env -> bool -> env diff --git a/src/tests/FStarC.Tests.Pars.fst b/src/tests/FStarC.Tests.Pars.fst index 9f87202b852..9c27e9c24c2 100644 --- a/src/tests/FStarC.Tests.Pars.fst +++ b/src/tests/FStarC.Tests.Pars.fst @@ -77,7 +77,7 @@ let init_once () : unit = FStarC.Universal.core_check in env.solver.init env; - let dsenv, prims_mod = parse_mod (Basefiles.prims()) (DsEnv.empty_env Parser.Dep.empty_deps) in + let dsenv, prims_mod = parse_mod (Find.find_file "FStar.Prelude.fsti" |> BU.must) (DsEnv.empty_env Parser.Dep.empty_deps) in let env = {env with dsenv=dsenv} in let _prims_mod, env = Tc.check_module env prims_mod false in // needed to run tests with chars diff --git a/src/tosyntax/FStarC.ToSyntax.Interleave.fst b/src/tosyntax/FStarC.ToSyntax.Interleave.fst index 7d142cd6887..909db1d48bb 100644 --- a/src/tosyntax/FStarC.ToSyntax.Interleave.fst +++ b/src/tosyntax/FStarC.ToSyntax.Interleave.fst @@ -314,50 +314,11 @@ let ml_mode_check_initial_interface mname (iface:list decl) = | ModuleAbbrev _ -> true | _ -> false) -let ulib_modules = [ - "FStar.Calc"; - "FStar.TSet"; - "FStar.Seq.Base"; - "FStar.Seq.Properties"; - "FStar.UInt"; - "FStar.UInt8"; - "FStar.UInt16"; - "FStar.UInt32"; - "FStar.UInt64"; - "FStar.Int"; - "FStar.Int8"; - "FStar.Int16"; - "FStar.Int32"; - "FStar.Int64"; -] - -(* - * AR: ml mode optimizations are only applied in ml mode and only to non-core files - * - * otherwise we skip effect declarations like Lemma from Pervasives.fsti, - * resulting in desugaring failures when typechecking Pervasives.fst - *) -let apply_ml_mode_optimizations (mname:lident) : bool = - (* - * AR: 03/29: - * As we introduce interfaces for modules in ulib/, the interleaving code - * doesn't interact with it too well when bootstrapping - * Essentially we do optimizations here (e.g. not taking any interface decls but vals) - * when bootstrapping - * This doesn't work well for ulib files (but is ok for compiler files) - * A better way to fix this problem would be to make compiler files in a separate namespace - * and then do these optimizations (as well as --MLish etc.) only for them - * But until then ... (sigh) - *) - Options.ml_ish () && - (not (List.contains (Ident.string_of_lid mname) (Parser.Dep.core_modules ()))) && - (not (List.contains (Ident.string_of_lid mname) ulib_modules)) - let prefix_one_decl mname iface impl = match impl.d with | TopLevelModule _ -> iface, [impl] | _ -> - if apply_ml_mode_optimizations mname + if Options.ml_ish () then ml_mode_prefix_with_iface_decls iface impl else prefix_with_iface_decls iface impl @@ -368,7 +329,7 @@ module E = FStarC.Syntax.DsEnv let initialize_interface (mname:Ident.lid) (l:list decl) : E.withenv unit = fun (env:E.env) -> let decls = - if apply_ml_mode_optimizations mname + if Options.ml_ish () then ml_mode_check_initial_interface mname l else check_initial_interface l in match E.iface_decls env mname with @@ -406,7 +367,7 @@ let interleave_module (a:modul) (expect_complete_modul:bool) : E.withenv modul = fun (env:E.env) -> match a with | Interface _ -> a, env - | Module(l, impls) -> begin + | Module {no_prelude; mname=l; decls=impls} -> begin match E.iface_decls env l with | None -> a, env | Some iface -> @@ -434,7 +395,7 @@ let interleave_module (a:modul) (expect_complete_modul:bool) : E.withenv modul = //since some batch-mode checks, e.g., must_erase_for_extraction //depend on having all the iface decls around in - let a = Module(l, impls) in + let a = Module { no_prelude; mname=l; decls=impls } in match remaining_iface_vals with | _::_ when expect_complete_modul -> let open FStarC.Pprint in diff --git a/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst b/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst index 7ace0b67a82..65148720460 100644 --- a/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst +++ b/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst @@ -3580,8 +3580,8 @@ and desugar_redefine_effect env d d_attrs trans_qual quals eff_name eff_binders let sub = sub' 0 in let mname=qualify env0 eff_name in let ed = { - mname = mname; cattributes = cattributes; + mname = mname; univs = ed.univs; binders = binders; signature = U.apply_eff_sig sub ed.signature; @@ -4308,18 +4308,20 @@ let desugar_modul_common (curmod: option S.modul) env (m:AST.modul) : env_t & Sy let env = match curmod, m with | None, _ -> env - | Some ({ name = prev_lid }), Module (current_lid, _) + | Some ({ name = prev_lid }), Module {mname = current_lid } when lid_equals prev_lid current_lid && Options.interactive () -> // If we're in the interactive mode reading the contents of an fst after // desugaring the corresponding fsti, don't finish the fsti env | Some prev_mod, _ -> fst (Env.finish_module_or_interface env prev_mod) in - let (env, pop_when_done), mname, decls, intf = match m with - | Interface(mname, decls, admitted) -> + let (env, pop_when_done), mname, decls, intf = + match m with + | Interface {no_prelude; mname; decls; admitted} -> Env.prepare_module_or_interface true admitted env mname Env.default_mii, mname, decls, true - | Module(mname, decls) -> - Env.prepare_module_or_interface false false env mname Env.default_mii, mname, decls, false in + | Module {no_prelude; mname; decls} -> + Env.prepare_module_or_interface false false env mname Env.default_mii, mname, decls, false + in let env, sigelts = desugar_decls env decls in let modul = { name = mname; @@ -4328,11 +4330,6 @@ let desugar_modul_common (curmod: option S.modul) env (m:AST.modul) : env_t & Sy } in env, modul, pop_when_done -let as_interface (m:AST.modul) : AST.modul = - match m with - | AST.Module(mname, decls) -> AST.Interface(mname, decls, true) - | i -> i - let desugar_partial_modul curmod (env:env_t) (m:AST.modul) : env_t & Syntax.modul = let m = if Options.interactive () && diff --git a/src/tosyntax/FStarC.ToSyntax.ToSyntax.fsti b/src/tosyntax/FStarC.ToSyntax.ToSyntax.fsti index d17130526d9..6690c02a4f9 100644 --- a/src/tosyntax/FStarC.ToSyntax.ToSyntax.fsti +++ b/src/tosyntax/FStarC.ToSyntax.ToSyntax.fsti @@ -31,7 +31,6 @@ module S = FStarC.Syntax.Syntax type extension_tosyntax_decl_t = env -> FStarC.Dyn.dyn -> lids:list lident -> Range.range -> list sigelt' val register_extension_tosyntax (lang_name:string) (cb:extension_tosyntax_decl_t) : unit -val as_interface: AST.modul -> AST.modul val desugar_term: env -> term -> S.term val desugar_machine_integer: env -> repr:string -> (FStarC.Const.signedness & FStarC.Const.width) From 9e83ca25a787c9d36e103528cf84eefca70ce2b7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sat, 8 Feb 2025 22:39:05 -0800 Subject: [PATCH 06/14] Update expected output: revealing IDE bug, modules transitively included are not considered for autocomplete --- tests/ide/emacs/Backtracking.refinements.ideout.expected | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/ide/emacs/Backtracking.refinements.ideout.expected b/tests/ide/emacs/Backtracking.refinements.ideout.expected index 19222334d94..7cde8be0629 100644 --- a/tests/ide/emacs/Backtracking.refinements.ideout.expected +++ b/tests/ide/emacs/Backtracking.refinements.ideout.expected @@ -6,7 +6,7 @@ {"kind": "response", "query-id": "5", "response": [], "status": "success"} {"kind": "response", "query-id": "6", "response": [], "status": "success"} {"kind": "response", "query-id": "7", "response": null, "status": "success"} -{"kind": "response", "query-id": "8", "response": [[3, "Prims", "nat"], [0, "", "nat"]], "status": "success"} +{"kind": "response", "query-id": "8", "response": [], "status": "success"} {"kind": "response", "query-id": "9", "response": [], "status": "success"} {"kind": "response", "query-id": "10", "response": [], "status": "success"} {"kind": "response", "query-id": "11", "response": null, "status": "success"} @@ -35,7 +35,7 @@ {"kind": "response", "query-id": "34", "response": [], "status": "success"} {"kind": "response", "query-id": "35", "response": [{"level": "error", "message": "- Identifier not found: b\n", "number": 72, "ranges": [{"beg": [5, 7], "end": [5, 8], "fname": ""}]}], "status": "success"} {"kind": "response", "query-id": "36", "response": [{"level": "error", "message": "- Identifier not found: b\n", "number": 72, "ranges": [{"beg": [5, 7], "end": [5, 8], "fname": ""}]}], "status": "success"} -{"kind": "response", "query-id": "37", "response": [[3, "Prims", "nat"], [0, "", "nat"]], "status": "success"} +{"kind": "response", "query-id": "37", "response": [], "status": "success"} {"kind": "response", "query-id": "38", "response": [], "status": "success"} {"kind": "response", "query-id": "39", "response": [{"level": "error", "message": "- Syntax error\n", "number": 168, "ranges": [{"beg": [5, 15], "end": [5, 15], "fname": ""}]}], "status": "success"} {"kind": "response", "query-id": "40", "response": [{"level": "error", "message": "- Syntax error\n", "number": 168, "ranges": [{"beg": [5, 19], "end": [5, 19], "fname": ""}]}], "status": "success"} From a0dcfb59a44726d934dc050328489be13906f670 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 9 Feb 2025 19:00:20 -0800 Subject: [PATCH 07/14] Pervasives: move custom attributes into FStar.Attributes, add to Prelude --- src/extraction/FStarC.Extraction.ML.Modul.fst | 30 +- src/parser/FStarC.Parser.Const.fst | 79 ++-- src/tactics/FStarC.Tactics.Hooks.fst | 2 +- .../FStarC.TypeChecker.DeferredImplicits.fst | 2 +- src/typechecker/FStarC.TypeChecker.Util.fst | 5 +- ulib/FStar.Attributes.fsti | 419 +++++++++++++++++ ulib/FStar.Pervasives.fst | 64 +-- ulib/FStar.Pervasives.fsti | 443 +----------------- ulib/FStar.Prelude.fsti | 1 + ulib/FStar.Tactics.MkProjectors.fst | 2 +- 10 files changed, 500 insertions(+), 547 deletions(-) create mode 100644 ulib/FStar.Attributes.fsti diff --git a/src/extraction/FStarC.Extraction.ML.Modul.fst b/src/extraction/FStarC.Extraction.ML.Modul.fst index ed334f703a6..821b2ce0056 100644 --- a/src/extraction/FStarC.Extraction.ML.Modul.fst +++ b/src/extraction/FStarC.Extraction.ML.Modul.fst @@ -129,26 +129,26 @@ let rec extract_meta x : option meta = match SS.compress x with | { n = Tm_fvar fv } -> begin match string_of_lid (lid_of_fv fv) with - | "FStar.Pervasives.PpxDerivingShow" -> Some PpxDerivingShow - | "FStar.Pervasives.PpxDerivingYoJson" -> Some PpxDerivingYoJson - | "FStar.Pervasives.CInline" -> Some CInline - | "FStar.Pervasives.CNoInline" -> Some CNoInline - | "FStar.Pervasives.Substitute" -> Some Substitute - | "FStar.Pervasives.Gc" -> Some GCType - | "FStar.Pervasives.CAbstractStruct" -> Some CAbstract - | "FStar.Pervasives.CIfDef" -> Some CIfDef - | "FStar.Pervasives.CMacro" -> Some CMacro + | "FStar.Attributes.PpxDerivingShow" -> Some PpxDerivingShow + | "FStar.Attributes.PpxDerivingYoJson" -> Some PpxDerivingYoJson + | "FStar.Attributes.CInline" -> Some CInline + | "FStar.Attributes.CNoInline" -> Some CNoInline + | "FStar.Attributes.Substitute" -> Some Substitute + | "FStar.Attributes.Gc" -> Some GCType + | "FStar.Attributes.CAbstractStruct" -> Some CAbstract + | "FStar.Attributes.CIfDef" -> Some CIfDef + | "FStar.Attributes.CMacro" -> Some CMacro | "Prims.deprecated" -> Some (Deprecated "") | _ -> None end | { n = Tm_app {hd={ n = Tm_fvar fv }; args=[{ n = Tm_constant (Const_string (s, _)) }, _]} } -> begin match string_of_lid (lid_of_fv fv) with - | "FStar.Pervasives.PpxDerivingShowConstant" -> Some (PpxDerivingShowConstant s) - | "FStar.Pervasives.Comment" -> Some (Comment s) - | "FStar.Pervasives.CPrologue" -> Some (CPrologue s) - | "FStar.Pervasives.CEpilogue" -> Some (CEpilogue s) - | "FStar.Pervasives.CConst" -> Some (CConst s) - | "FStar.Pervasives.CCConv" -> Some (CCConv s) + | "FStar.Attributes.PpxDerivingShowConstant" -> Some (PpxDerivingShowConstant s) + | "FStar.Attributes.Comment" -> Some (Comment s) + | "FStar.Attributes.CPrologue" -> Some (CPrologue s) + | "FStar.Attributes.CEpilogue" -> Some (CEpilogue s) + | "FStar.Attributes.CConst" -> Some (CConst s) + | "FStar.Attributes.CCConv" -> Some (CCConv s) | "Prims.deprecated" -> Some (Deprecated s) | _ -> None end diff --git a/src/parser/FStarC.Parser.Const.fst b/src/parser/FStarC.Parser.Const.fst index e7dc2e89b9b..85a0931b155 100644 --- a/src/parser/FStarC.Parser.Const.fst +++ b/src/parser/FStarC.Parser.Const.fst @@ -29,6 +29,7 @@ let p2l l = lid_of_path l dummyRange let pconst s = p2l ["Prims";s] let psconst s = p2l ["FStar"; "Pervasives"; s] +let attr s = p2l ["FStar"; "Attributes"; s] let psnconst s = p2l ["FStar"; "Pervasives" ; "Native" ; s] let prims_lid = p2l ["Prims"] let pervasives_native_lid = p2l ["FStar"; "Pervasives"; "Native"] @@ -332,46 +333,50 @@ let steps_unmeta = psconst "unmeta" (* attributes *) let deprecated_attr = pconst "deprecated" let warn_on_use_attr = pconst "warn_on_use" -let inline_let_attr = p2l ["FStar"; "Pervasives"; "inline_let"] -let rename_let_attr = p2l ["FStar"; "Pervasives"; "rename_let"] -let plugin_attr = p2l ["FStar"; "Pervasives"; "plugin"] -let tcnorm_attr = p2l ["FStar"; "Pervasives"; "tcnorm"] -let dm4f_bind_range_attr = p2l ["FStar"; "Pervasives"; "dm4f_bind_range"] -let must_erase_for_extraction_attr = psconst "must_erase_for_extraction" -let strict_on_arguments_attr = p2l ["FStar"; "Pervasives"; "strict_on_arguments"] -let resolve_implicits_attr_string = "FStar.Pervasives.resolve_implicits" -let unification_tag_lid = psconst "defer_to" -let override_resolve_implicits_handler_lid = p2l ["FStar"; "Pervasives"; "override_resolve_implicits_handler"] -let handle_smt_goals_attr = psconst "handle_smt_goals" -let handle_smt_goals_attr_string = "FStar.Pervasives.handle_smt_goals" -let erasable_attr = p2l ["FStar"; "Pervasives"; "erasable"] -let comment_attr = p2l ["FStar"; "Pervasives"; "Comment"] -let c_inline_attr = p2l ["FStar"; "Pervasives"; "CInline"] -let fail_attr = psconst "expect_failure" -let fail_lax_attr = psconst "expect_lax_failure" -let tcdecltime_attr = psconst "tcdecltime" -let noextract_to_attr = psconst "noextract_to" -let unifier_hint_injective_lid = psconst "unifier_hint_injective" +let inline_let_attr = attr "inline_let" +let rename_let_attr = attr "rename_let" +let plugin_attr = attr "plugin" +let tcnorm_attr = attr "tcnorm" +let dm4f_bind_range_attr = attr "dm4f_bind_range" +let must_erase_for_extraction_attr = attr "must_erase_for_extraction" +let strict_on_arguments_attr = attr "strict_on_arguments" +let resolve_implicits_attr_string = attr "resolve_implicits" +let override_resolve_implicits_handler_lid = attr "override_resolve_implicits_handler" +let handle_smt_goals_attr = attr "handle_smt_goals" +let erasable_attr = attr "erasable" +let fail_attr = attr "expect_failure" +let fail_lax_attr = attr "expect_lax_failure" +let unification_tag_lid = attr "defer_to" + +let comment_attr = attr "Comment" +let c_inline_attr = attr "CInline" +let attr_substitute_lid = attr "Substitute" + let normalize_for_extraction_lid = psconst "normalize_for_extraction" let normalize_for_extraction_type_lid = psconst "normalize_for_extraction_type" -let commute_nested_matches_lid = psconst "commute_nested_matches" -let remove_unused_type_parameters_lid = psconst "remove_unused_type_parameters" -let ite_soundness_by_attr = psconst "ite_soundness_by" -let default_effect_attr = psconst "default_effect" -let top_level_effect_attr = psconst "top_level_effect" -let effect_parameter_attr = psconst "effect_param" -let bind_has_range_args_attr = psconst "bind_has_range_args" -let primitive_extraction_attr = psconst "primitive_extraction" -let binder_strictly_positive_attr = psconst "strictly_positive" -let binder_unused_attr = psconst "unused" -let no_auto_projectors_decls_attr = psconst "no_auto_projectors_decls" -let no_auto_projectors_attr = psconst "no_auto_projectors" -let no_subtping_attr_lid = psconst "no_subtyping" -let admit_termination_lid = psconst "admit_termination" + +let tcdecltime_attr = attr "tcdecltime" +let noextract_to_attr = attr "noextract_to" +let unifier_hint_injective_lid = attr "unifier_hint_injective" +let commute_nested_matches_lid = attr "commute_nested_matches" +let ite_soundness_by_attr = attr "ite_soundness_by" +let default_effect_attr = attr "default_effect" +let top_level_effect_attr = attr "top_level_effect" +let effect_parameter_attr = attr "effect_param" +let bind_has_range_args_attr = attr "bind_has_range_args" +let primitive_extraction_attr = attr "primitive_extraction" +let binder_strictly_positive_attr = attr "strictly_positive" +let binder_unused_attr = attr "unused" +let no_auto_projectors_decls_attr = attr "no_auto_projectors_decls" +let no_auto_projectors_attr = attr "no_auto_projectors" +let no_subtping_attr_lid = attr "no_subtyping" +let admit_termination_lid = attr "admit_termination" let unrefine_binder_attr = pconst "unrefine" let do_not_unrefine_attr = pconst "do_not_unrefine" -let attr_substitute_lid = p2l ["FStar"; "Pervasives"; "Substitute"] -let desugar_of_variant_record_lid = psconst "desugar_of_variant_record" +let desugar_of_variant_record_lid = attr "desugar_of_variant_record" +let coercion_lid = attr "coercion" + +let remove_unused_type_parameters_lid = psconst "remove_unused_type_parameters" //the type of well-founded relations, used for decreases clauses with relations @@ -516,4 +521,4 @@ let document_lid = p2l ["FStar"; "Pprint"; "document"] let issue_lid = p2l ["FStar"; "Issue"; "issue"] let extract_as_lid = p2l ["FStar"; "ExtractAs"; "extract_as"] -let extract_as_impure_effect_lid = p2l ["FStar"; "Pervasives"; "extract_as_impure_effect"] +let extract_as_impure_effect_lid = attr "extract_as_impure_effect" diff --git a/src/tactics/FStarC.Tactics.Hooks.fst b/src/tactics/FStarC.Tactics.Hooks.fst index c5cd6b18946..435e5fbe19e 100644 --- a/src/tactics/FStarC.Tactics.Hooks.fst +++ b/src/tactics/FStarC.Tactics.Hooks.fst @@ -762,7 +762,7 @@ let solve_implicits (env:Env.env) (tau:term) (imps:Env.implicits) : unit = (* Retrieves a tactic associated to a given attribute, if any *) let find_user_tac_for_attr env (a:term) : option sigelt = - let hooks = Env.lookup_attr env PC.handle_smt_goals_attr_string in + let hooks = Env.lookup_attr env (Ident.string_of_lid PC.handle_smt_goals_attr) in hooks |> BU.try_find (fun _ -> true) (* This function takes an environment [env] and a goal [goal], and tries to run diff --git a/src/typechecker/FStarC.TypeChecker.DeferredImplicits.fst b/src/typechecker/FStarC.TypeChecker.DeferredImplicits.fst index 68619b00e6e..42bdaa6488e 100644 --- a/src/typechecker/FStarC.TypeChecker.DeferredImplicits.fst +++ b/src/typechecker/FStarC.TypeChecker.DeferredImplicits.fst @@ -116,7 +116,7 @@ let find_user_tac_for_uvar env (u:ctx_uvar) : option sigelt = match u.ctx_uvar_meta with | Some (Ctx_uvar_meta_attr a) -> (* hooks: all definitions with the resolve_implicits attr *) - let hooks = Env.lookup_attr env FStarC.Parser.Const.resolve_implicits_attr_string in + let hooks = Env.lookup_attr env (string_of_lid Parser.Const.resolve_implicits_attr_string) in (* candidates: hooks that also have the attribute [a] *) let candidates = hooks |> List.filter diff --git a/src/typechecker/FStarC.TypeChecker.Util.fst b/src/typechecker/FStarC.TypeChecker.Util.fst index 2f5393f5a78..566371ae9b7 100644 --- a/src/typechecker/FStarC.TypeChecker.Util.fst +++ b/src/typechecker/FStarC.TypeChecker.Util.fst @@ -15,9 +15,10 @@ *) module FStarC.TypeChecker.Util + +open FStarC open FStarC.Effect open FStarC.List -open FStarC open FStarC.Util open FStarC.Errors open FStarC.Errors.Msg @@ -2486,7 +2487,7 @@ let find_coercion (env:Env.env) (checked: lcomp) (exp_t: typ) (e:term) let? exp_head_lid = head_lid_of exp_t in let? computed_head_lid = head_lid_of computed_t in - let candidates = Env.lookup_attr env "FStar.Pervasives.coercion" in + let candidates = Env.lookup_attr env (string_of_lid C.coercion_lid) in candidates |> first_opt (fun se -> (* `f` is the candidate coercion, `e` the term to coerce *) let? f_name, f_us, f_typ = diff --git a/ulib/FStar.Attributes.fsti b/ulib/FStar.Attributes.fsti new file mode 100644 index 00000000000..2feb664ea68 --- /dev/null +++ b/ulib/FStar.Attributes.fsti @@ -0,0 +1,419 @@ +[@@"no_prelude"] +module FStar.Attributes + +open Prims + +/// Attributes: +/// +/// An attribute is any F* term. +/// +/// Attributes are desugared and checked for being well-scoped. But, +/// they are not type-checked. +/// +/// It is associated with a definition using the [[@@attribute]] +/// notation, just preceding the definition. + +(** We collect several internal ocaml attributes into a single + inductive type. + + This may be unnecessary. In the future, we are likely to flatten + this definition into several definitions of abstract top-level + names. + + An example: + + {[ + [@@ CInline ] let f x = UInt32.(x +%^ 1) + ]} + + is extracted to C by KaRaMeL to a C definition tagged with the + [inline] qualifier. *) +type __internal_ocaml_attributes = + | PpxDerivingShow (* Generate [@@@ deriving show ] on the resulting OCaml type *) + | PpxDerivingShowConstant of string (* Similar, but for constant printers. *) + | PpxDerivingYoJson (* Generate [@@@ deriving yojson ] on the resulting OCaml type *) + | CInline + (* KaRaMeL-only: generates a C "inline" attribute on the resulting + * function declaration. When used on a local definition (i.e. a letbinding) + KaRaMeL will try to inline this binding in the extracted C code. *) + | Substitute + (* KaRaMeL-only: forces KaRaMeL to inline the function at call-site; this is + * deprecated and the recommended way is now to use F*'s + * [inline_for_extraction], which now also works for stateful functions. *) + | Gc + (* KaRaMeL-only: instructs KaRaMeL to heap-allocate any value of this + * data-type; this requires running with a conservative GC as the + * allocations are not freed. *) + | Comment of string + (* KaRaMeL-only: attach a comment to the declaration. Note that using F*-doc + * syntax automatically fills in this attribute. *) + | CPrologue of string + (* KaRaMeL-only: verbatim C code to be prepended to the declaration. + * Multiple attributes are valid and accumulate, separated by newlines. *) + | CEpilogue of string (* Ibid. *) + | CConst of string + (* KaRaMeL-only: indicates that the parameter with that name is to be marked + * as C const. This will be checked by the C compiler, not by KaRaMeL or F*. + * + * This is deprecated and doesn't work as intended. Use + * LowStar.ConstBuffer.fst instead! *) + | CCConv of string (* A calling convention for C, one of stdcall, cdecl, fastcall *) + | CAbstractStruct + (* KaRaMeL-only: for types that compile to struct types (records and + * inductives), indicate that the header file should only contain a forward + * declaration, which in turn forces the client to only ever use this type + * through a pointer. *) + | CIfDef (* KaRaMeL-only: on a given `val foo`, compile if foo with #ifdef. *) + | CMacro +(* KaRaMeL-only: for a top-level `let v = e`, compile as a macro *) + | CNoInline + (* For security-sensitive functions only: generate special attributes in C + to prevent inlining; if the function is subjected to a -static-header + option, the `inline` attribute will be removed, but the static will + remain. *) + +(** The [inline_let] attribute on a local let-binding, instructs the + extraction pipeline to inline the definition. This may be both to + avoid generating unnecessary intermediate variables, and also to + enable further partial evaluation. Note, use this with care, since + inlining all lets can lead to an exponential blowup in code + size. *) +val inline_let : unit + +(** The [rename_let] attribute support a form of metaprogramming for + the names of let-bound variables used in extracted code. + + This is useful, particularly in conjunction with partial + evaluation, to ensure that names reflect their usage context. + + See tests/micro-benchmarks/Renaming*.fst *) +val rename_let (new_name: string) : Tot unit + +(** The [plugin] attribute is used in conjunction with native + compilation of F* components, accelerating their reduction + relative to the default strategy of just interpreting them. + + See examples/native_tactics for several examples. *) +val plugin (x: int) : Tot unit + +(** An attribute to mark things that the typechecker should *first* + elaborate and typecheck, but unfold before verification. *) +val tcnorm : unit + +(** This attribute is used with the Dijkstra Monads for Free + construction to track position information in generated VCs *) +val dm4f_bind_range : unit + +(** We erase all ghost functions and unit-returning pure functions to + [()] at extraction. This creates a small issue with abstract + types. Consider a module that defines an abstract type [t] whose + (internal) definition is [unit] and also defines [f: int -> t]. [f] + would be erased to be just [()] inside the module, while the + client calls to [f] would not, since [t] is abstract. To get + around this, when extracting interfaces, if we encounter an + abstract type, we tag it with this attribute, so that + extraction can treat it specially. + + Note, since the use of cross-module inlining (the [--cmi] option), + this attribute is no longer necessary. We retain it for legacy, + but will remove it in the future. *) +val must_erase_for_extraction : unit + +(** When attached a top-level definition, the typechecker will succeed + if and only if checking the definition results in an error. The + error number list is actually OPTIONAL. If present, it will be + checked that the definition raises exactly those errors in the + specified multiplicity, but order does not matter. *) +val expect_failure (errs: list int) : Tot unit + +(** When --admit_smt_queries true is present, with the previous attribute since some + definitions only fail when verification is turned on. With this + attribute, one can ensure that a definition fails while lax-checking + too. Same semantics as above, but lax mode will be turned on for the + definition. *) +val expect_lax_failure (errs: list int) : Tot unit + +(** Print the time it took to typecheck a top-level definition *) +val tcdecltime : unit + +(** This attribute is to be used as a hint for the unifier. A + function-typed symbol `t` marked with this attribute will be treated + as being injective in all its arguments by the unifier. That is, + given a problem `t a1..an =?= t b1..bn` the unifier will solve it by + proving `ai =?= bi` for all `i`, without trying to unfold the + definition of `t`. *) +val unifier_hint_injective : unit + +(** + This attribute is used to control the evaluation order + and unfolding strategy for certain definitions. + + In particular, given + {[ + [@@(strict_on_arguments [1;2])] + let f x0 (x1:list x0) (x1:option x0) = e + ]} + + An application [f e0 e1 e2] is reduced by the normalizer by: + + 1. evaluating [e0 ~>* v0, e1 ~>* v1, e2 ~>* v2] + + 2 a. + If, according to the positional arguments [1;2], + if v1 and v2 have constant head symbols + (e.g., v1 = Cons _ _ _, and v2 = None _) + then [f] is unfolded to [e] and reduced as + {[e[v0/x0][v1/x1][v2/x2]]} + + 2 b. + + Otherwise, [f] is not unfolded and the term is [f e0 e1 e2] + reduces to [f v0 v1 v2]. *) +val strict_on_arguments (x: list int) : Tot unit + +(** + * An attribute to tag a tactic designated to solve any + * unsolved implicit arguments remaining at the end of type inference. + **) +val resolve_implicits : unit + +(** + * Implicit arguments can be tagged with an attribute [abc] to dispatch + * their solving to a user-defined tactic also tagged with the same + * attribute and resolve_implicits [@@abc; resolve_implicits]. + + * However, sometimes it is useful to have multiple such + * [abc]-tagged tactics in scope. In such a scenario, to choose among them, + * one can use the attribute as shown below to declare that [t] overrides + * all the tactics [t1...tn] and should be used to solve [abc]-tagged + * implicits, so long as [t] is not iself overridden by some other tactic. + + [@@resolve_implicits; abc; override_resolve_implicits_handler abc [`%t1; ... `%tn]] + let t = e + + **) +val override_resolve_implicits_handler : #a:Type -> a -> list string -> Tot unit + +(** A tactic registered to solve implicits with the (handle_smt_goals) + attribute will receive the SMT goal generated during typechecking + just before it is passed to the SMT solver. + *) +val handle_smt_goals : unit + +(** This attribute can be added to an inductive type definition, + indicating that it should be erased on extraction to `unit`. + + However, any pattern matching on the inductive type results + in a `Ghost` effect, ensuring that computationally relevant + code cannot rely on the values of the erasable type. + + See tests/micro-benchmarks/Erasable.fst, for examples. Also + see https://github.com/FStarLang/FStar/issues/1844 *) +val erasable : unit + +(** [commute_nested_matches] + This attribute can be used to decorate an inductive type [t] + + During normalization, if reduction is blocked on matching the + constructors of [t] in the following sense: + + [ + match (match e0 with | P1 -> e1 | ... | Pn -> en) with + | Q1 -> f1 ... | Qm -> fm + ] + + i.e., the outer match is stuck due to the inner match on [e0] + being stuck, and if the head constructor the outer [Qi] patterns + are the constructors of the decorated inductive type [t], then, + this is reduced to + + [ + match e0 with + | P1 -> (match e1 with | Q1 -> f1 ... | Qm -> fm) + | ... + | Pn -> (match en with | Q1 -> f1 ... | Qm -> fm) + ] + + This is sometimes useful when partially evaluating code before + extraction, particularly when aiming to obtain first-order code + for KaRaMeL. However, this attribute should be used with care, + since if after the rewriting the inner matches do not reduce, then + this can cause an explosion in code size. + + See tests/micro-benchmarks/CommuteNestedMatches.fst + and examples/layeredeffects/LowParseWriters.fsti + *) +val commute_nested_matches : unit + +(** This attribute controls extraction: it can be used to disable + extraction of a given top-level definition into a specific backend, + such as "OCaml". If any extracted code must call into an erased + function, an error will be raised (code 340). + *) +val noextract_to (backend:string) : Tot unit + + +(** A layered effect definition may optionally be annotated with + (ite_soundness_by t) attribute, where t is another attribute + When so, the implicits and the smt guard generated when + checking the soundness of the if-then-else combinator, are + dispatched to the tactic in scope that has the t attribute (in addition + to the resolve_implicits attribute as usual) + + See examples/layeredeffects/IteSoundess.fst for a few examples + *) +val ite_soundness_by (attribute: unit): Tot unit + +(** By-default functions that have a layered effect, need to have a type + annotation for their bodies + However, a layered effect definition may contain the default_effect + attribute to indicate to the typechecker that for missing annotations, + use the default effect. + The default effect attribute takes as argument a string, that is the name + of the default effect, two caveats: + - The argument must be a string constant (not a name, for example) + - The argument should be the fully qualified name + For example, the TAC effect in FStar.Tactics.Effect.fsti specifies + its default effect as FStar.Tactics.Tac + F* will typecheck that the default effect only takes one argument, + the result type of the computation + *) +val default_effect (s:string) : Tot unit + +(** A layered effect may optionally be annotated with the + top_level_effect attribute so indicate that this effect may + appear at the top-level + (e.g., a top-level let x = e, where e has a layered effect type) + + The top_level_effect attribute takes (optional) string argument, that is the + name of the effect abbreviation that may constrain effect arguments + for the top-level effect + + As with default effect, the string argument must be a string constant, + and fully qualified + + E.g. a Hoare-style effect `M a pre post`, may have the attribute + `@@ top_level_effect "N"`, where the effect abbreviation `N` may be: + + effect N a post = M a True post + + i.e., enforcing a trivial precondition if `M` appears at the top-level + + If the argument to `top_level_effect` is absent, then the effect itself + is allowed at the top-level with any effect arguments + + See tests/micro-benchmarks/TopLevelIndexedEffects.fst for examples + + *) +val top_level_effect (s:string) : Tot unit + +(** This attribute can be annotated on the binders in an effect signature + to indicate that they are effect parameters. For example, for a + state effect that is parametric in the type of the state, the state + index may be marked as an effect parameter. + + Also see https://github.com/FStarLang/FStar/wiki/Indexed-effects + + *) +val effect_param : unit + +(** Bind definition for a layered effect may optionally contain range + arguments, that are provided by the typechecker during reification + This attribute on the effect definition indicates that the bind + has range arguments. + See for example the TAC effect in FStar.Tactics.Effect.fsti + *) +val bind_has_range_args : unit + + +(** An indexed effect definition may be annotated with + this attribute to indicate that the effect should be + extracted "natively". E.g., the `bind` of the effect is + extracted to primitive `let` bindings + + As an example, `Steel` effects (the effect for concurrent + separation logic) are marked as such + + *) +val primitive_extraction : unit + +(** A qualifier on a type definition which when used in co-domain position + on an arrow type will be extracted as if it were an impure effect type. + + e.g., if you have + + [@@extract_as_impure_effect] + val stt (a:Type) (pre:_) (post:_) : Type + + then arrows of the form `a -> stt b p q` will be extracted + similarly to `a -> Dv b`. + *) +val extract_as_impure_effect : unit + + +(** A binder in a definition/declaration may optionally be annotated as strictly_positive + When the let definition is used in a data constructor type in an inductive + definition, this annotation is used to check the positivity of the inductive + + Further F* checks that the binder is actually positive in the let definition + + See tests/micro-benchmarks/Positivity.fst and NegativeTests.Positivity.fst for a few examples + *) +val strictly_positive : unit + +(** A binder in a definition/declaration may optionally be annotated as unused. + This is used in the strict positivity checker. E.g., a type such as the one + below is accepted + + let f ([@@@unused] a:Type) = unit + type t = | MkT: f t -> t + + F* checks that the binder is actually unused in the definition + + See tests/micro-benchmarks/Positivity.fst for a few examples + *) +val unused : unit + +(** This attribute may be added to an inductive type + to disable auto generated projectors + + Normally there should not be any need to use this unless: + for some reason F* cannot typecheck the auto-generated projectors. + + Another reason to use this attribute may be to avoid generating and + typechecking lot of projectors, most of which are not going to be used + in the rest of the program + *) +val no_auto_projectors : unit + +(** As [no_auto_projectors] but also do not even generate declarations + for them. *) +val no_auto_projectors_decls : unit + +(** This attribute can be added to a let definition + and indicates to the typechecker to typecheck the signature of the definition + without using subtyping. This is sometimes useful for indicating that a lemma + can be applied by the tactic engine without requiring to check additional + subtyping obligations +*) +val no_subtyping : unit + +(* This can be attached to a recursive definition to admit its proof + of termination (but nothing else). *) +val admit_termination : unit + +(* This marks a given definition as a coercion to be automatically + applied by the typechecker. See doc/rec/coercions.txt for more + information. *) +val coercion : unit + +(** Marks a record type as being the result of an automatic desugar of + a constructor with a record payload. + For example, in a module `M`, `type foo = | A {x: int}` desugars + to the type `M.foo` and a type `M.foo__A__payload`. That latter + type `foo__A__payload` is decorated with an attribute + `desugar_of_variant_record ["M.A"]`. *) +val desugar_of_variant_record (type_name: string): unit + +(** Tag for implicits that are to be solved by a tactic. *) +val defer_to (#a:Type) (tag : a) : unit diff --git a/ulib/FStar.Pervasives.fst b/ulib/FStar.Pervasives.fst index bd27ca162ce..8a6da305eab 100644 --- a/ulib/FStar.Pervasives.fst +++ b/ulib/FStar.Pervasives.fst @@ -143,69 +143,7 @@ let invertOption _ = () let rec false_elim #_ _ = false_elim () -let inline_let = () - -let rename_let _ = () - -let plugin _ = () - -let tcnorm = () - -let must_erase_for_extraction = () - -let dm4f_bind_range = () - -let expect_failure _ = () - -let expect_lax_failure _ = () - -let tcdecltime = () - -let unifier_hint_injective = () - -let strict_on_arguments _ = () - -let resolve_implicits = () - -let override_resolve_implicits_handler #a x l = () - -let handle_smt_goals = () - -let erasable = () - -let commute_nested_matches = () - -let noextract_to _ = () +let singleton #_ x = x let normalize_for_extraction _ = () let normalize_for_extraction_type = () - -let ite_soundness_by _ = () - -let default_effect _ = () -let top_level_effect _ = () -let effect_param = () -let bind_has_range_args = () -let primitive_extraction = () - -let extract_as_impure_effect = () - -let strictly_positive = () - -let unused = () - -let no_auto_projectors = () - -let no_auto_projectors_decls = () - -let no_subtyping = () - -let admit_termination = () - -let singleton #_ x = x - -let coercion = () - -let desugar_of_variant_record _ = () - -let defer_to #a (_:a) = () diff --git a/ulib/FStar.Pervasives.fsti b/ulib/FStar.Pervasives.fsti index b1466ebd1c6..a5d7eb5ab00 100644 --- a/ulib/FStar.Pervasives.fsti +++ b/ulib/FStar.Pervasives.fsti @@ -76,7 +76,7 @@ val smt_pat_or (x: list (list pattern)) : Tot pattern (** eqtype is defined in prims at universe 0 Although, usually, only universe 0 types have decidable equality, - sometimes it is possible to define a type in a higher univese also + sometimes it is possible to define a type in a higher universe also with decidable equality (e.g., type t : Type u#1 = | Unit) Further, sometimes, as in Lemma below, we need to use a @@ -776,256 +776,25 @@ let ignore (#a: Type) (x: a) : Tot unit = () infinitely looping function, since the termination check succeeds in a [False] context. *) val false_elim (#a: Type) (u: unit{False}) : Tot a +(** Pure and ghost inner let bindings are now always inlined during + the wp computation, if: the return type is not unit and the head + symbol is not marked irreducible. -/// Attributes: -/// -/// An attribute is any F* term. -/// -/// Attributes are desugared and checked for being well-scoped. But, -/// they are not type-checked. -/// -/// It is associated with a definition using the [[@@attribute]] -/// notation, just preceding the definition. - -(** We collect several internal ocaml attributes into a single - inductive type. - - This may be unnecessary. In the future, we are likely to flatten - this definition into several definitions of abstract top-level - names. - - An example: - - {[ - [@@ CInline ] let f x = UInt32.(x +%^ 1) - ]} - - is extracted to C by KaRaMeL to a C definition tagged with the - [inline] qualifier. *) -type __internal_ocaml_attributes = - | PpxDerivingShow (* Generate [@@@ deriving show ] on the resulting OCaml type *) - | PpxDerivingShowConstant of string (* Similar, but for constant printers. *) - | PpxDerivingYoJson (* Generate [@@@ deriving yojson ] on the resulting OCaml type *) - | CInline - (* KaRaMeL-only: generates a C "inline" attribute on the resulting - * function declaration. When used on a local definition (i.e. a letbinding) - KaRaMeL will try to inline this binding in the extracted C code. *) - | Substitute - (* KaRaMeL-only: forces KaRaMeL to inline the function at call-site; this is - * deprecated and the recommended way is now to use F*'s - * [inline_for_extraction], which now also works for stateful functions. *) - | Gc - (* KaRaMeL-only: instructs KaRaMeL to heap-allocate any value of this - * data-type; this requires running with a conservative GC as the - * allocations are not freed. *) - | Comment of string - (* KaRaMeL-only: attach a comment to the declaration. Note that using F*-doc - * syntax automatically fills in this attribute. *) - | CPrologue of string - (* KaRaMeL-only: verbatim C code to be prepended to the declaration. - * Multiple attributes are valid and accumulate, separated by newlines. *) - | CEpilogue of string (* Ibid. *) - | CConst of string - (* KaRaMeL-only: indicates that the parameter with that name is to be marked - * as C const. This will be checked by the C compiler, not by KaRaMeL or F*. - * - * This is deprecated and doesn't work as intended. Use - * LowStar.ConstBuffer.fst instead! *) - | CCConv of string (* A calling convention for C, one of stdcall, cdecl, fastcall *) - | CAbstractStruct - (* KaRaMeL-only: for types that compile to struct types (records and - * inductives), indicate that the header file should only contain a forward - * declaration, which in turn forces the client to only ever use this type - * through a pointer. *) - | CIfDef (* KaRaMeL-only: on a given `val foo`, compile if foo with #ifdef. *) - | CMacro -(* KaRaMeL-only: for a top-level `let v = e`, compile as a macro *) - | CNoInline - (* For security-sensitive functions only: generate special attributes in C - to prevent inlining; if the function is subjected to a -static-header - option, the `inline` attribute will be removed, but the static will - remain. *) - -(** The [inline_let] attribute on a local let-binding, instructs the - extraction pipeline to inline the definition. This may be both to - avoid generating unnecessary intermediate variables, and also to - enable further partial evaluation. Note, use this with care, since - inlining all lets can lead to an exponential blowup in code - size. *) -val inline_let : unit - -(** The [rename_let] attribute support a form of metaprogramming for - the names of let-bound variables used in extracted code. - - This is useful, particularly in conjunction with partial - evaluation, to ensure that names reflect their usage context. - - See tests/micro-benchmarks/Renaming*.fst *) -val rename_let (new_name: string) : Tot unit - -(** The [plugin] attribute is used in conjunction with native - compilation of F* components, accelerating their reduction - relative to the default strategy of just interpreting them. - - See examples/native_tactics for several examples. *) -val plugin (x: int) : Tot unit - -(** An attribute to mark things that the typechecker should *first* - elaborate and typecheck, but unfold before verification. *) -val tcnorm : unit - -(** We erase all ghost functions and unit-returning pure functions to - [()] at extraction. This creates a small issue with abstract - types. Consider a module that defines an abstract type [t] whose - (internal) definition is [unit] and also defines [f: int -> t]. [f] - would be erased to be just [()] inside the module, while the - client calls to [f] would not, since [t] is abstract. To get - around this, when extracting interfaces, if we encounter an - abstract type, we tag it with this attribute, so that - extraction can treat it specially. - - Note, since the use of cross-module inlining (the [--cmi] option), - this attribute is no longer necessary. We retain it for legacy, - but will remove it in the future. *) -val must_erase_for_extraction : unit - -(** This attribute is used with the Dijkstra Monads for Free - construction to track position information in generated VCs *) -val dm4f_bind_range : unit - -(** When attached a top-level definition, the typechecker will succeed - if and only if checking the definition results in an error. The - error number list is actually OPTIONAL. If present, it will be - checked that the definition raises exactly those errors in the - specified multiplicity, but order does not matter. *) -val expect_failure (errs: list int) : Tot unit - -(** When --admit_smt_queries true is present, with the previous attribute since some - definitions only fail when verification is turned on. With this - attribute, one can ensure that a definition fails while lax-checking - too. Same semantics as above, but lax mode will be turned on for the - definition. *) -val expect_lax_failure (errs: list int) : Tot unit - -(** Print the time it took to typecheck a top-level definition *) -val tcdecltime : unit - -(** This attribute is to be used as a hint for the unifier. A - function-typed symbol `t` marked with this attribute will be treated - as being injective in all its arguments by the unifier. That is, - given a problem `t a1..an =?= t b1..bn` the unifier will solve it by - proving `ai =?= bi` for all `i`, without trying to unfold the - definition of `t`. *) -val unifier_hint_injective : unit - -(** - This attribute is used to control the evaluation order - and unfolding strategy for certain definitions. - - In particular, given - {[ - [@@(strict_on_arguments [1;2])] - let f x0 (x1:list x0) (x1:option x0) = e - ]} - - An application [f e0 e1 e2] is reduced by the normalizer by: - - 1. evaluating [e0 ~>* v0, e1 ~>* v1, e2 ~>* v2] - - 2 a. - If, according to the positional arguments [1;2], - if v1 and v2 have constant head symbols - (e.g., v1 = Cons _ _ _, and v2 = None _) - then [f] is unfolded to [e] and reduced as - {[e[v0/x0][v1/x1][v2/x2]]} - - 2 b. - - Otherwise, [f] is not unfolded and the term is [f e0 e1 e2] - reduces to [f v0 v1 v2]. *) -val strict_on_arguments (x: list int) : Tot unit - -(** - * An attribute to tag a tactic designated to solve any - * unsolved implicit arguments remaining at the end of type inference. - **) -val resolve_implicits : unit + To circumvent this behavior, singleton can be used. + See the example usage in ulib/FStar.Algebra.Monoid.fst. *) +val singleton (#a: Type) (x: a) : Tot (y: a{y == x}) -(** - * Implicit arguments can be tagged with an attribute [abc] to dispatch - * their solving to a user-defined tactic also tagged with the same - * attribute and resolve_implicits [@@abc; resolve_implicits]. - - * However, sometimes it is useful to have multiple such - * [abc]-tagged tactics in scope. In such a scenario, to choose among them, - * one can use the attribute as shown below to declare that [t] overrides - * all the tactics [t1...tn] and should be used to solve [abc]-tagged - * implicits, so long as [t] is not iself overridden by some other tactic. - - [@@resolve_implicits; abc; override_resolve_implicits_handler abc [`%t1; ... `%tn]] - let t = e - - **) -val override_resolve_implicits_handler : #a:Type -> a -> list string -> Tot unit - -(** A tactic registered to solve implicits with the (handle_smt_goals) - attribute will receive the SMT goal generated during typechecking - just before it is passed to the SMT solver. - *) -val handle_smt_goals : unit - -(** This attribute can be added to an inductive type definition, - indicating that it should be erased on extraction to `unit`. - - However, any pattern matching on the inductive type results - in a `Ghost` effect, ensuring that computationally relevant - code cannot rely on the values of the erasable type. - - See tests/micro-benchmarks/Erasable.fst, for examples. Also - see https://github.com/FStarLang/FStar/issues/1844 *) -val erasable : unit - -(** [commute_nested_matches] - This attribute can be used to decorate an inductive type [t] - - During normalization, if reduction is blocked on matching the - constructors of [t] in the following sense: - - [ - match (match e0 with | P1 -> e1 | ... | Pn -> en) with - | Q1 -> f1 ... | Qm -> fm - ] - - i.e., the outer match is stuck due to the inner match on [e0] - being stuck, and if the head constructor the outer [Qi] patterns - are the constructors of the decorated inductive type [t], then, - this is reduced to - - [ - match e0 with - | P1 -> (match e1 with | Q1 -> f1 ... | Qm -> fm) - | ... - | Pn -> (match en with | Q1 -> f1 ... | Qm -> fm) - ] - - This is sometimes useful when partially evaluating code before - extraction, particularly when aiming to obtain first-order code - for KaRaMeL. However, this attribute should be used with care, - since if after the rewriting the inner matches do not reduce, then - this can cause an explosion in code size. - - See tests/micro-benchmarks/CommuteNestedMatches.fst - and examples/layeredeffects/LowParseWriters.fsti - *) -val commute_nested_matches : unit +(** A weakening coercion from eqtype to Type. -(** This attribute controls extraction: it can be used to disable - extraction of a given top-level definition into a specific backend, - such as "OCaml". If any extracted code must call into an erased - function, an error will be raised (code 340). - *) -val noextract_to (backend:string) : Tot unit + One of its uses is in types of layered effect combinators that + are subjected to stricter typing discipline (no subtyping) *) +unfold let eqtype_as_type (a:eqtype) : Type = a +(** A coercion of the [x] from [a] to [b], when [a] is provably equal + to [b]. In most cases, F* will silently coerce from [a] to [b] + along a provable equality (as in the body of this + function). Occasionally, you may need to apply this explicitly *) +let coerce_eq (#a:Type) (#b:Type) (_:squash (a == b)) (x:a) : b = x (** This attribute decorates a let binding, e.g., @@ -1058,183 +827,3 @@ val normalize_for_extraction (steps:list norm_step) : Tot unit (* When using [normalize_for_extraction] this flag indicates that the type * of the definition should also be normalized. *) val normalize_for_extraction_type : unit - -(** A layered effect definition may optionally be annotated with - (ite_soundness_by t) attribute, where t is another attribute - When so, the implicits and the smt guard generated when - checking the soundness of the if-then-else combinator, are - dispatched to the tactic in scope that has the t attribute (in addition - to the resolve_implicits attribute as usual) - - See examples/layeredeffects/IteSoundess.fst for a few examples - *) -val ite_soundness_by (attribute: unit): Tot unit - -(** By-default functions that have a layered effect, need to have a type - annotation for their bodies - However, a layered effect definition may contain the default_effect - attribute to indicate to the typechecker that for missing annotations, - use the default effect. - The default effect attribute takes as argument a string, that is the name - of the default effect, two caveats: - - The argument must be a string constant (not a name, for example) - - The argument should be the fully qualified name - For example, the TAC effect in FStar.Tactics.Effect.fsti specifies - its default effect as FStar.Tactics.Tac - F* will typecheck that the default effect only takes one argument, - the result type of the computation - *) -val default_effect (s:string) : Tot unit - -(** A layered effect may optionally be annotated with the - top_level_effect attribute so indicate that this effect may - appear at the top-level - (e.g., a top-level let x = e, where e has a layered effect type) - - The top_level_effect attribute takes (optional) string argument, that is the - name of the effect abbreviation that may constrain effect arguments - for the top-level effect - - As with default effect, the string argument must be a string constant, - and fully qualified - - E.g. a Hoare-style effect `M a pre post`, may have the attribute - `@@ top_level_effect "N"`, where the effect abbreviation `N` may be: - - effect N a post = M a True post - - i.e., enforcing a trivial precondition if `M` appears at the top-level - - If the argument to `top_level_effect` is absent, then the effect itself - is allowed at the top-level with any effect arguments - - See tests/micro-benchmarks/TopLevelIndexedEffects.fst for examples - - *) -val top_level_effect (s:string) : Tot unit - -(** This attribute can be annotated on the binders in an effect signature - to indicate that they are effect parameters. For example, for a - state effect that is parametric in the type of the state, the state - index may be marked as an effect parameter. - - Also see https://github.com/FStarLang/FStar/wiki/Indexed-effects - - *) -val effect_param : unit - -(** Bind definition for a layered effect may optionally contain range - arguments, that are provided by the typechecker during reification - This attribute on the effect definition indicates that the bind - has range arguments. - See for example the TAC effect in FStar.Tactics.Effect.fsti - *) -val bind_has_range_args : unit - - -(** An indexed effect definition may be annotated with - this attribute to indicate that the effect should be - extracted "natively". E.g., the `bind` of the effect is - extracted to primitive `let` bindings - - As an example, `Steel` effects (the effect for concurrent - separation logic) are marked as such - - *) -val primitive_extraction : unit - -(** A qualifier on a type definition which when used in co-domain position - on an arrow type will be extracted as if it were an impure effect type. - - e.g., if you have - - [@@extract_as_impure_effect] - val stt (a:Type) (pre:_) (post:_) : Type - - then arrows of the form `a -> stt b p q` will be extracted - similarly to `a -> Dv b`. - *) -val extract_as_impure_effect : unit - - -(** A binder in a definition/declaration may optionally be annotated as strictly_positive - When the let definition is used in a data constructor type in an inductive - definition, this annotation is used to check the positivity of the inductive - - Further F* checks that the binder is actually positive in the let definition - - See tests/micro-benchmarks/Positivity.fst and NegativeTests.Positivity.fst for a few examples - *) -val strictly_positive : unit - -(** A binder in a definition/declaration may optionally be annotated as unused. - This is used in the strict positivity checker. E.g., a type such as the one - below is accepted - - let f ([@@@unused] a:Type) = unit - type t = | MkT: f t -> t - - F* checks that the binder is actually unused in the definition - - See tests/micro-benchmarks/Positivity.fst for a few examples - *) -val unused : unit - -(** This attribute may be added to an inductive type - to disable auto generated projectors - - Normally there should not be any need to use this unless: - for some reason F* cannot typecheck the auto-generated projectors. - - Another reason to use this attribute may be to avoid generating and - typechecking lot of projectors, most of which are not going to be used - in the rest of the program - *) -val no_auto_projectors : unit - -(** As [no_auto_projectors] but also do not even generate declarations - for them. *) -val no_auto_projectors_decls : unit - -(** This attribute can be added to a let definition - and indicates to the typechecker to typecheck the signature of the definition - without using subtyping. This is sometimes useful for indicating that a lemma - can be applied by the tactic engine without requiring to check additional - subtyping obligations -*) -val no_subtyping : unit - -val admit_termination : unit - -(** Pure and ghost inner let bindings are now always inlined during - the wp computation, if: the return type is not unit and the head - symbol is not marked irreducible. - - To circumvent this behavior, singleton can be used. - See the example usage in ulib/FStar.Algebra.Monoid.fst. *) -val singleton (#a: Type) (x: a) : Tot (y: a{y == x}) - -(** A weakening coercion from eqtype to Type. - - One of its uses is in types of layered effect combinators that - are subjected to stricter typing discipline (no subtyping) *) -unfold let eqtype_as_type (a:eqtype) : Type = a - -(** A coercion of the [x] from [a] to [b], when [a] is provably equal - to [b]. In most cases, F* will silently coerce from [a] to [b] - along a provable equality (as in the body of this - function). Occasionally, you may need to apply this explicitly *) -let coerce_eq (#a:Type) (#b:Type) (_:squash (a == b)) (x:a) : b = x - -val coercion : unit - -(** Marks a record type as being the result of an automatic desugar of - a constructor with a record payload. - For example, in a module `M`, `type foo = | A {x: int}` desugars - to the type `M.foo` and a type `M.foo__A__payload`. That latter - type `foo__A__payload` is decorated with an attribute - `desugar_of_variant_record ["M.A"]`. *) -val desugar_of_variant_record (type_name: string): unit - -(** Tag for implicits that are to be solved by a tactic. *) -val defer_to (#a:Type) (tag : a) : unit diff --git a/ulib/FStar.Prelude.fsti b/ulib/FStar.Prelude.fsti index 541429d4a30..90bdb996c4a 100644 --- a/ulib/FStar.Prelude.fsti +++ b/ulib/FStar.Prelude.fsti @@ -4,3 +4,4 @@ module FStar.Prelude include Prims include FStar.Pervasives.Native include FStar.Pervasives +include FStar.Attributes diff --git a/ulib/FStar.Tactics.MkProjectors.fst b/ulib/FStar.Tactics.MkProjectors.fst index e512e890ad1..7340ade90f0 100644 --- a/ulib/FStar.Tactics.MkProjectors.fst +++ b/ulib/FStar.Tactics.MkProjectors.fst @@ -97,7 +97,7 @@ let embed_string (s:string) : term = (* For compatibility: the typechecker sets this attribute for all projectors. Karamel relies on it to do inlining. *) let substitute_attr : term = - `Pervasives.Substitute + `Attributes.Substitute let mk_proj_decl (is_method:bool) (tyqn:name) ctorname From 87b5c35460ce1aa3bc5c05817057bd6792fabbd3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 9 Feb 2025 20:01:42 -0800 Subject: [PATCH 08/14] Move norm_steps away from pervasives, fix the cross-stage dependency for this type Needed to mark norm as noextract, which makes sense! --- src/basic/FStarC.NormSteps.fst | 86 +++++++++ src/extraction/FStarC.Extraction.ML.UEnv.fst | 26 +-- src/fstar/FStarC.Main.fst | 1 + src/parser/FStarC.Parser.Const.fst | 41 ++--- src/syntax/FStarC.Syntax.Embeddings.fst | 7 +- src/syntax/FStarC.Syntax.Embeddings.fsti | 2 +- src/tactics/FStarC.Tactics.V1.Basic.fst | 8 +- src/tactics/FStarC.Tactics.V1.Basic.fsti | 7 +- src/tactics/FStarC.Tactics.V2.Basic.fst | 8 +- src/tactics/FStarC.Tactics.V2.Basic.fsti | 8 +- src/typechecker/FStarC.TypeChecker.Cfg.fst | 38 ++-- src/typechecker/FStarC.TypeChecker.Cfg.fsti | 5 +- .../FStarC.TypeChecker.NBETerm.fst | 70 ++++---- .../FStarC.TypeChecker.NBETerm.fsti | 2 +- ulib/FStar.NormSteps.fst | 85 +++++++++ ulib/FStar.NormSteps.fsti | 163 ++++++++++++++++++ ulib/FStar.Pervasives.fst | 82 --------- ulib/FStar.Pervasives.fsti | 163 +----------------- ulib/FStar.Prelude.fsti | 1 + 19 files changed, 443 insertions(+), 360 deletions(-) create mode 100644 src/basic/FStarC.NormSteps.fst create mode 100644 ulib/FStar.NormSteps.fst create mode 100644 ulib/FStar.NormSteps.fsti diff --git a/src/basic/FStarC.NormSteps.fst b/src/basic/FStarC.NormSteps.fst new file mode 100644 index 00000000000..20fdbe691b4 --- /dev/null +++ b/src/basic/FStarC.NormSteps.fst @@ -0,0 +1,86 @@ +module FStarC.NormSteps + +(* A mirror of FStar.NormSteps in ulib *) + +open Prims +noeq +type norm_step = + | Simpl // Logical simplification, e.g., [P /\ True ~> P] + | Weak // Weak reduction: Do not reduce under binders + | HNF // Head normal form + | Primops // Reduce primitive operators, e.g., [1 + 1 ~> 2] + | Delta // Unfold all non-recursive definitions + | Zeta // Unroll recursive calls + | ZetaFull // Unroll recursive calls fully + | Iota // Reduce case analysis (i.e., match) + | NBE // Use normalization-by-evaluation, instead of interpretation (experimental) + | Reify // Reify effectful definitions into their representations + | NormDebug // Turn on debugging for this call + | UnfoldOnly : list string -> norm_step // Unlike Delta, unfold definitions for only the given + | UnfoldOnce : list string -> norm_step + // names, each string is a fully qualified name + // like `A.M.f` + // idem + | UnfoldFully : list string -> norm_step + | UnfoldAttr : list string -> norm_step // Unfold definitions marked with the given attributes + | UnfoldQual : list string -> norm_step + | UnfoldNamespace : list string -> norm_step + | Unmeta : norm_step + | Unascribe // Remove type ascriptions [t <: ty ~> t] + +irreducible +let simplify = Simpl + +irreducible +let weak = Weak + +irreducible +let hnf = HNF + +irreducible +let primops = Primops + +irreducible +let delta = Delta + +irreducible +let norm_debug = NormDebug + +irreducible +let zeta = Zeta + +irreducible +let zeta_full = ZetaFull + +irreducible +let iota = Iota + +irreducible +let nbe = NBE + +irreducible +let reify_ = Reify + +irreducible +let delta_only s = UnfoldOnly s + +irreducible +let delta_once s = UnfoldOnce s + +irreducible +let delta_fully s = UnfoldFully s + +irreducible +let delta_attr s = UnfoldAttr s + +irreducible +let delta_qualifier s = UnfoldAttr s + +irreducible +let delta_namespace s = UnfoldNamespace s + +irreducible +let unmeta = Unmeta + +irreducible +let unascribe = Unascribe diff --git a/src/extraction/FStarC.Extraction.ML.UEnv.fst b/src/extraction/FStarC.Extraction.ML.UEnv.fst index 5696abe2ecb..9fcdab9d918 100644 --- a/src/extraction/FStarC.Extraction.ML.UEnv.fst +++ b/src/extraction/FStarC.Extraction.ML.UEnv.fst @@ -254,6 +254,9 @@ let is_fv_type g fv = let no_fstar_stubs_ns (ns : list mlsymbol) : list mlsymbol = match ns with + | "FStar"::"NormSteps"::rest when plug () -> + "Fstarcompiler.FStarC"::"NormSteps"::rest + | "FStar"::"Stubs"::rest when plug_no_lib () && Options.Ext.enabled "__guts" -> "FStarC"::rest (* These 3 modules are special, and are not in the guts. They live in src/ml/full and @@ -439,29 +442,8 @@ let new_mlpath_of_lident (g:uenv) (x : lident) : mlpath & uenv = | "FStar.Pervasives.either" | "FStar.Pervasives.Inl" | "FStar.Pervasives.Inr" + when plug () -> guts mlp - | "FStar.Pervasives.norm_step" - | "FStar.Pervasives.norm_debug" - | "FStar.Pervasives.simplify" - | "FStar.Pervasives.weak" - | "FStar.Pervasives.hnf" - | "FStar.Pervasives.primops" - | "FStar.Pervasives.delta" - | "FStar.Pervasives.norm_debug" - | "FStar.Pervasives.zeta" - | "FStar.Pervasives.zeta_full" - | "FStar.Pervasives.iota" - | "FStar.Pervasives.nbe" - | "FStar.Pervasives.reify_" - | "FStar.Pervasives.delta_only" - | "FStar.Pervasives.delta_fully" - | "FStar.Pervasives.delta_attr" - | "FStar.Pervasives.delta_qualifier" - | "FStar.Pervasives.delta_namespace" - | "FStar.Pervasives.unmeta" - | "FStar.Pervasives.unascribe" - when plug () - -> guts mlp (* special case to not expose FStarC.Errors *) | "FStar.Stubs.Tactics.Common.Stop" -> "Fstarcompiler.FStarC"::"Errors"::[], "Stop" diff --git a/src/fstar/FStarC.Main.fst b/src/fstar/FStarC.Main.fst index 48218ff5faa..d4d97f522d4 100644 --- a/src/fstar/FStarC.Main.fst +++ b/src/fstar/FStarC.Main.fst @@ -37,6 +37,7 @@ open FStarC.Reflection.V1.Interpreter {} open FStarC.Reflection.V2.Interpreter {} (* Same, except that it only defines some types for userspace to refer to. *) open FStarC.Tactics.Types.Reflection {} +open FStarC.NormSteps {} (* process_args: parses command line arguments, setting FStarC.Options *) (* returns an error status and list of filenames *) diff --git a/src/parser/FStarC.Parser.Const.fst b/src/parser/FStarC.Parser.Const.fst index 85a0931b155..28463c33646 100644 --- a/src/parser/FStarC.Parser.Const.fst +++ b/src/parser/FStarC.Parser.Const.fst @@ -310,25 +310,27 @@ let normalize_term = psconst "normalize_term" let norm = psconst "norm" (* lids for normalizer steps *) -let steps_simpl = psconst "simplify" -let steps_weak = psconst "weak" -let steps_hnf = psconst "hnf" -let steps_primops = psconst "primops" -let steps_zeta = psconst "zeta" -let steps_zeta_full = psconst "zeta_full" -let steps_iota = psconst "iota" -let steps_delta = psconst "delta" -let steps_reify = psconst "reify_" -let steps_norm_debug = psconst "norm_debug" -let steps_unfoldonly = psconst "delta_only" -let steps_unfoldonce = psconst "delta_once" -let steps_unfoldfully = psconst "delta_fully" -let steps_unfoldattr = psconst "delta_attr" -let steps_unfoldqual = psconst "delta_qualifier" -let steps_unfoldnamespace = psconst "delta_namespace" -let steps_unascribe = psconst "unascribe" -let steps_nbe = psconst "nbe" -let steps_unmeta = psconst "unmeta" +let mk_norm_step_lid l = p2l ["FStar"; "NormSteps"; l] +let norm_step_lid = mk_norm_step_lid "norm_step" +let steps_simpl = mk_norm_step_lid "simplify" +let steps_weak = mk_norm_step_lid "weak" +let steps_hnf = mk_norm_step_lid "hnf" +let steps_primops = mk_norm_step_lid "primops" +let steps_zeta = mk_norm_step_lid "zeta" +let steps_zeta_full = mk_norm_step_lid "zeta_full" +let steps_iota = mk_norm_step_lid "iota" +let steps_delta = mk_norm_step_lid "delta" +let steps_reify = mk_norm_step_lid "reify_" +let steps_norm_debug = mk_norm_step_lid "norm_debug" +let steps_unfoldonly = mk_norm_step_lid "delta_only" +let steps_unfoldonce = mk_norm_step_lid "delta_once" +let steps_unfoldfully = mk_norm_step_lid "delta_fully" +let steps_unfoldattr = mk_norm_step_lid "delta_attr" +let steps_unfoldqual = mk_norm_step_lid "delta_qualifier" +let steps_unfoldnamespace = mk_norm_step_lid "delta_namespace" +let steps_unascribe = mk_norm_step_lid "unascribe" +let steps_nbe = mk_norm_step_lid "nbe" +let steps_unmeta = mk_norm_step_lid "unmeta" (* attributes *) let deprecated_attr = pconst "deprecated" @@ -448,7 +450,6 @@ let binder_lid = lid_of_path (["FStar"; "Stubs"; "Reflection"; "Types"; "binder" let binders_lid = lid_of_path (["FStar"; "Stubs"; "Reflection"; "Types"; "binders"]) FStarC.Range.dummyRange let bv_lid = lid_of_path (["FStar"; "Stubs"; "Reflection"; "Types"; "bv"]) FStarC.Range.dummyRange let fv_lid = lid_of_path (["FStar"; "Stubs"; "Reflection"; "Types"; "fv"]) FStarC.Range.dummyRange -let norm_step_lid = psconst "norm_step" let postprocess_with = p2l ["FStar"; "Tactics"; "Effect"; "postprocess_with"] let postprocess_type = p2l ["FStar"; "Tactics"; "Effect"; "postprocess_type"] let preprocess_with = p2l ["FStar"; "Tactics"; "Effect"; "preprocess_with"] diff --git a/src/syntax/FStarC.Syntax.Embeddings.fst b/src/syntax/FStarC.Syntax.Embeddings.fst index ace7668d992..7539d88d8a1 100644 --- a/src/syntax/FStarC.Syntax.Embeddings.fst +++ b/src/syntax/FStarC.Syntax.Embeddings.fst @@ -803,11 +803,12 @@ let steps_Unascribe = tconst PC.steps_unascribe let steps_NBE = tconst PC.steps_nbe let steps_Unmeta = tconst PC.steps_unmeta -let e_norm_step : embedding Pervasives.norm_step = +let e_norm_step : embedding NormSteps.norm_step = + let open FStarC.NormSteps in let typ () = S.t_norm_step in let emb_t_norm_step () = ET_app (PC.norm_step_lid |> Ident.string_of_lid, []) in let printer _ = "norm_step" in - let em (n:Pervasives.norm_step) (rng:range) _shadow norm : term = + let em (n:NormSteps.norm_step) (rng:range) _shadow norm : term = lazy_embed printer emb_t_norm_step @@ -864,7 +865,7 @@ let e_norm_step : embedding Pervasives.norm_step = ) in - let un (t:term) norm : option Pervasives.norm_step = + let un (t:term) norm : option NormSteps.norm_step = lazy_unembed printer emb_t_norm_step diff --git a/src/syntax/FStarC.Syntax.Embeddings.fsti b/src/syntax/FStarC.Syntax.Embeddings.fsti index f81d114ffee..7628e9c04fc 100644 --- a/src/syntax/FStarC.Syntax.Embeddings.fsti +++ b/src/syntax/FStarC.Syntax.Embeddings.fsti @@ -38,7 +38,7 @@ instance val e_int : embedding Z.t instance val e_fsint : embedding int instance val e_string : embedding string instance val e_real : embedding Real.real -instance val e_norm_step : embedding Pervasives.norm_step +instance val e_norm_step : embedding NormSteps.norm_step instance val e_vconfig : embedding FStarC.VConfig.vconfig instance val e_order : embedding FStarC.Order.order diff --git a/src/tactics/FStarC.Tactics.V1.Basic.fst b/src/tactics/FStarC.Tactics.V1.Basic.fst index ddba7d9f60a..f868a2c4193 100644 --- a/src/tactics/FStarC.Tactics.V1.Basic.fst +++ b/src/tactics/FStarC.Tactics.V1.Basic.fst @@ -788,7 +788,7 @@ let intro_rec () : tac (binder & binder) = | None -> fail1 "intro_rec: goal is not an arrow (%s)" (tts (goal_env goal) (goal_type goal)) -let norm (s : list Pervasives.norm_step) : tac unit = +let norm (s : list NormSteps.norm_step) : tac unit = let! goal = cur_goal in if_verbose (fun () -> BU.print1 "norm: witness = %s\n" (show (goal_witness goal))) ;! // Translate to actual normalizer steps @@ -798,7 +798,7 @@ let norm (s : list Pervasives.norm_step) : tac unit = replace_cur (goal_with_type goal t) -let norm_term_env (e : env) (s : list Pervasives.norm_step) (t : term) : tac term = wrap_err "norm_term" <| ( +let norm_term_env (e : env) (s : list NormSteps.norm_step) (t : term) : tac term = wrap_err "norm_term" <| ( let! ps = get in if_verbose (fun () -> BU.print1 "norm_term_env: t = %s\n" (show t)) ;! // only for elaborating lifts and all that, we don't care if it's actually well-typed @@ -866,7 +866,7 @@ let t_exact try_refine set_expected_typ tm : tac unit = wrap_err "exact" <| ( | Inl e when not (try_refine) -> traise e | Inl e -> if_verbose (fun () -> BU.print_string "__exact_now failed, trying refine...\n") ;! - match! catch (norm [Pervasives.Delta] ;! refine_intro () ;! __exact_now set_expected_typ tm) with + match! catch (norm [NormSteps.Delta] ;! refine_intro () ;! __exact_now set_expected_typ tm) with | Inr r -> if_verbose (fun () -> BU.print_string "__exact_now: failed after refining too\n") ;! ret r @@ -1265,7 +1265,7 @@ let binder_retype (b : binder) : tac unit = wrap_err "binder_retype" <| ( ) (* TODO: move to bv *) -let norm_binder_type (s : list Pervasives.norm_step) (b : binder) : tac unit = wrap_err "norm_binder_type" <| ( +let norm_binder_type (s : list NormSteps.norm_step) (b : binder) : tac unit = wrap_err "norm_binder_type" <| ( let! goal = cur_goal in let bv = b.binder_bv in match split_env bv (goal_env goal) with diff --git a/src/tactics/FStarC.Tactics.V1.Basic.fsti b/src/tactics/FStarC.Tactics.V1.Basic.fsti index 7d1dd7919ca..6449a1d7b86 100644 --- a/src/tactics/FStarC.Tactics.V1.Basic.fsti +++ b/src/tactics/FStarC.Tactics.V1.Basic.fsti @@ -23,6 +23,7 @@ module FStarC.Tactics.V1.Basic * between compiler and userspace (and a few other * annoyances too). *) +open FStarC open FStarC.Syntax.Syntax open FStarC.TypeChecker.Env open FStarC.Reflection.V1.Data @@ -48,9 +49,9 @@ val tc : env -> term -> tac typ val tcc : env -> term -> tac comp val unshelve : term -> tac unit val unquote : typ -> term -> tac term -val norm : list Pervasives.norm_step -> tac unit -val norm_term_env : env -> list Pervasives.norm_step -> term -> tac term -val norm_binder_type : list Pervasives.norm_step -> binder -> tac unit +val norm : list NormSteps.norm_step -> tac unit +val norm_term_env : env -> list NormSteps.norm_step -> term -> tac term +val norm_binder_type : list NormSteps.norm_step -> binder -> tac unit val intro : unit -> tac binder val intro_rec : unit -> tac (binder & binder) val rename_to : binder -> string -> tac binder diff --git a/src/tactics/FStarC.Tactics.V2.Basic.fst b/src/tactics/FStarC.Tactics.V2.Basic.fst index e3dd1ebf388..64d00d853b8 100644 --- a/src/tactics/FStarC.Tactics.V2.Basic.fst +++ b/src/tactics/FStarC.Tactics.V2.Basic.fst @@ -839,7 +839,7 @@ let intro_rec () : tac (RD.binding & RD.binding) = | None -> fail1 "intro_rec: goal is not an arrow (%s)" (tts (goal_env goal) (goal_type goal)) -let norm (s : list Pervasives.norm_step) : tac unit = +let norm (s : list NormSteps.norm_step) : tac unit = let! goal = cur_goal in if_verbose (fun () -> BU.print1 "norm: witness = %s\n" (show (goal_witness goal))) ;! // Translate to actual normalizer steps @@ -849,7 +849,7 @@ let norm (s : list Pervasives.norm_step) : tac unit = replace_cur (goal_with_type goal t) let __norm_term_env - (well_typed:bool) (e : env) (s : list Pervasives.norm_step) (t : term) + (well_typed:bool) (e : env) (s : list NormSteps.norm_step) (t : term) : tac term = wrap_err "norm_term" <| ( let! ps = get in @@ -926,7 +926,7 @@ let t_exact try_refine set_expected_typ tm : tac unit = wrap_err "exact" <| ( | Inl e when not (try_refine) -> traise e | Inl e -> if_verbose (fun () -> BU.print_string "__exact_now failed, trying refine...\n") ;! - match! catch (norm [Pervasives.Delta] ;! refine_intro () ;! __exact_now set_expected_typ tm) with + match! catch (norm [NormSteps.Delta] ;! refine_intro () ;! __exact_now set_expected_typ tm) with | Inr r -> if_verbose (fun () -> BU.print_string "__exact_now: failed after refining too\n") ;! return r @@ -1378,7 +1378,7 @@ let var_retype (b : RD.binding) : tac unit = wrap_err "binder_retype" <| ( (Some goal_sc) ) -let norm_binding_type (s : list Pervasives.norm_step) (b : RD.binding) : tac unit = wrap_err "norm_binding_type" <| ( +let norm_binding_type (s : list NormSteps.norm_step) (b : RD.binding) : tac unit = wrap_err "norm_binding_type" <| ( let! goal = cur_goal in let bv = binding_to_bv b in match split_env bv (goal_env goal) with diff --git a/src/tactics/FStarC.Tactics.V2.Basic.fsti b/src/tactics/FStarC.Tactics.V2.Basic.fsti index 8989e6930f3..14eb8724c00 100644 --- a/src/tactics/FStarC.Tactics.V2.Basic.fsti +++ b/src/tactics/FStarC.Tactics.V2.Basic.fsti @@ -53,9 +53,9 @@ val tc : env -> term -> tac typ val tcc : env -> term -> tac comp val unshelve : term -> tac unit val unquote : typ -> term -> tac term -val norm : list Pervasives.norm_step -> tac unit -val norm_term_env : env -> list Pervasives.norm_step -> term -> tac term -val norm_binding_type : list Pervasives.norm_step -> RD.binding -> tac unit +val norm : list NormSteps.norm_step -> tac unit +val norm_term_env : env -> list NormSteps.norm_step -> term -> tac term +val norm_binding_type : list NormSteps.norm_step -> RD.binding -> tac unit val intro : unit -> tac RD.binding val intros : (max:Z.t) -> tac (list RD.binding) val intro_rec : unit -> tac (RD.binding & RD.binding) @@ -142,7 +142,7 @@ val refl_instantiate_implicits : env -> term -> expected_typ:option term val refl_try_unify : env -> list (bv & typ) -> term -> term -> tac (option (list (bv & term)) & issues) val refl_maybe_relate_after_unfolding : env -> term -> term -> tac (option Core.side & issues) val refl_maybe_unfold_head : env -> term -> tac (option term & issues) -val refl_norm_well_typed_term : env -> list norm_step -> term -> tac term +val refl_norm_well_typed_term : env -> list NormSteps.norm_step -> term -> tac term val push_open_namespace : env -> list string -> tac env val push_module_abbrev : env -> string -> list string -> tac env diff --git a/src/typechecker/FStarC.TypeChecker.Cfg.fst b/src/typechecker/FStarC.TypeChecker.Cfg.fst index 794aa9a89f4..d574f942bcd 100644 --- a/src/typechecker/FStarC.TypeChecker.Cfg.fst +++ b/src/typechecker/FStarC.TypeChecker.Cfg.fst @@ -445,31 +445,31 @@ let should_reduce_local_let cfg lb = not (cfg.steps.pure_subterms_within_computations) let translate_norm_step = function - | Pervasives.Zeta -> [Zeta] - | Pervasives.ZetaFull -> [ZetaFull] - | Pervasives.Iota -> [Iota] - | Pervasives.Delta -> [UnfoldUntil delta_constant] - | Pervasives.Simpl -> [Simplify] - | Pervasives.Weak -> [Weak] - | Pervasives.HNF -> [HNF] - | Pervasives.Primops -> [Primops] - | Pervasives.Reify -> [Reify] - | Pervasives.NormDebug -> [NormDebug] - | Pervasives.UnfoldOnly names -> + | NormSteps.Zeta -> [Zeta] + | NormSteps.ZetaFull -> [ZetaFull] + | NormSteps.Iota -> [Iota] + | NormSteps.Delta -> [UnfoldUntil delta_constant] + | NormSteps.Simpl -> [Simplify] + | NormSteps.Weak -> [Weak] + | NormSteps.HNF -> [HNF] + | NormSteps.Primops -> [Primops] + | NormSteps.Reify -> [Reify] + | NormSteps.NormDebug -> [NormDebug] + | NormSteps.UnfoldOnly names -> [UnfoldUntil delta_constant; UnfoldOnly (List.map I.lid_of_str names)] - | Pervasives.UnfoldOnce names -> + | NormSteps.UnfoldOnce names -> [UnfoldUntil delta_constant; UnfoldOnce (List.map I.lid_of_str names)] - | Pervasives.UnfoldFully names -> + | NormSteps.UnfoldFully names -> [UnfoldUntil delta_constant; UnfoldFully (List.map I.lid_of_str names)] - | Pervasives.UnfoldAttr names -> + | NormSteps.UnfoldAttr names -> [UnfoldUntil delta_constant; UnfoldAttr (List.map I.lid_of_str names)] - | Pervasives.UnfoldQual names -> + | NormSteps.UnfoldQual names -> [UnfoldUntil delta_constant; UnfoldQual names] - | Pervasives.UnfoldNamespace names -> + | NormSteps.UnfoldNamespace names -> [UnfoldUntil delta_constant; UnfoldNamespace names] - | Pervasives.Unascribe -> [Unascribe] - | Pervasives.NBE -> [NBE] - | Pervasives.Unmeta -> [Unmeta] + | NormSteps.Unascribe -> [Unascribe] + | NormSteps.NBE -> [NBE] + | NormSteps.Unmeta -> [Unmeta] let translate_norm_steps s = let s = List.concatMap translate_norm_step s in diff --git a/src/typechecker/FStarC.TypeChecker.Cfg.fsti b/src/typechecker/FStarC.TypeChecker.Cfg.fsti index b59b03eb136..bfb20dee345 100644 --- a/src/typechecker/FStarC.TypeChecker.Cfg.fsti +++ b/src/typechecker/FStarC.TypeChecker.Cfg.fsti @@ -15,9 +15,8 @@ *) module FStarC.TypeChecker.Cfg -open FStarC.Effect + open FStarC -open FStarC.Util open FStar.String open FStarC.Const open FStar.Char @@ -145,4 +144,4 @@ val config: list step -> Env.env -> cfg val should_reduce_local_let : cfg -> letbinding -> bool -val translate_norm_steps: list Pervasives.norm_step -> list Env.step +val translate_norm_steps: list NormSteps.norm_step -> list Env.step diff --git a/src/typechecker/FStarC.TypeChecker.NBETerm.fst b/src/typechecker/FStarC.TypeChecker.NBETerm.fst index 1e241105dc3..6c218e81b41 100644 --- a/src/typechecker/FStarC.TypeChecker.NBETerm.fst +++ b/src/typechecker/FStarC.TypeChecker.NBETerm.fst @@ -689,81 +689,81 @@ let e_unsupported #a : embedding a = mk_emb em un (fun () -> lid_as_typ PC.term_lid [] []) (fun () -> ET_abstract) let e_norm_step = - let em cb (n:Pervasives.norm_step) : t = + let em cb (n:NormSteps.norm_step) : t = match n with - | Pervasives.Simpl -> mkFV (lid_as_fv PC.steps_simpl None) [] [] - | Pervasives.Weak -> mkFV (lid_as_fv PC.steps_weak None) [] [] - | Pervasives.HNF -> mkFV (lid_as_fv PC.steps_hnf None) [] [] - | Pervasives.Primops -> mkFV (lid_as_fv PC.steps_primops None) [] [] - | Pervasives.Delta -> mkFV (lid_as_fv PC.steps_delta None) [] [] - | Pervasives.Zeta -> mkFV (lid_as_fv PC.steps_zeta None) [] [] - | Pervasives.Iota -> mkFV (lid_as_fv PC.steps_iota None) [] [] - | Pervasives.Reify -> mkFV (lid_as_fv PC.steps_reify None) [] [] - | Pervasives.NBE -> mkFV (lid_as_fv PC.steps_nbe None) [] [] - | Pervasives.UnfoldOnly l -> + | NormSteps.Simpl -> mkFV (lid_as_fv PC.steps_simpl None) [] [] + | NormSteps.Weak -> mkFV (lid_as_fv PC.steps_weak None) [] [] + | NormSteps.HNF -> mkFV (lid_as_fv PC.steps_hnf None) [] [] + | NormSteps.Primops -> mkFV (lid_as_fv PC.steps_primops None) [] [] + | NormSteps.Delta -> mkFV (lid_as_fv PC.steps_delta None) [] [] + | NormSteps.Zeta -> mkFV (lid_as_fv PC.steps_zeta None) [] [] + | NormSteps.Iota -> mkFV (lid_as_fv PC.steps_iota None) [] [] + | NormSteps.Reify -> mkFV (lid_as_fv PC.steps_reify None) [] [] + | NormSteps.NBE -> mkFV (lid_as_fv PC.steps_nbe None) [] [] + | NormSteps.UnfoldOnly l -> mkFV (lid_as_fv PC.steps_unfoldonly None) [] [as_arg (embed (e_list e_string) cb l)] - | Pervasives.UnfoldFully l -> + | NormSteps.UnfoldFully l -> mkFV (lid_as_fv PC.steps_unfoldfully None) [] [as_arg (embed (e_list e_string) cb l)] - | Pervasives.UnfoldAttr l -> + | NormSteps.UnfoldAttr l -> mkFV (lid_as_fv PC.steps_unfoldattr None) [] [as_arg (embed (e_list e_string) cb l)] - | Pervasives.UnfoldQual l -> + | NormSteps.UnfoldQual l -> mkFV (lid_as_fv PC.steps_unfoldqual None) [] [as_arg (embed (e_list e_string) cb l)] - | Pervasives.UnfoldNamespace l -> + | NormSteps.UnfoldNamespace l -> mkFV (lid_as_fv PC.steps_unfoldnamespace None) [] [as_arg (embed (e_list e_string) cb l)] - | Pervasives.ZetaFull -> mkFV (lid_as_fv PC.steps_zeta_full None) [] [] - | Pervasives.Unascribe -> mkFV (lid_as_fv PC.steps_unascribe None) [] [] + | NormSteps.ZetaFull -> mkFV (lid_as_fv PC.steps_zeta_full None) [] [] + | NormSteps.Unascribe -> mkFV (lid_as_fv PC.steps_unascribe None) [] [] in - let un cb (t0:t) : option Pervasives.norm_step = + let un cb (t0:t) : option NormSteps.norm_step = match t0.nbe_t with | FV (fv, _, []) when S.fv_eq_lid fv PC.steps_simpl -> - Some Pervasives.Simpl + Some NormSteps.Simpl | FV (fv, _, []) when S.fv_eq_lid fv PC.steps_weak -> - Some Pervasives.Weak + Some NormSteps.Weak | FV (fv, _, []) when S.fv_eq_lid fv PC.steps_hnf -> - Some Pervasives.HNF + Some NormSteps.HNF | FV (fv, _, []) when S.fv_eq_lid fv PC.steps_primops -> - Some Pervasives.Primops + Some NormSteps.Primops | FV (fv, _, []) when S.fv_eq_lid fv PC.steps_delta -> - Some Pervasives.Delta + Some NormSteps.Delta | FV (fv, _, []) when S.fv_eq_lid fv PC.steps_zeta -> - Some Pervasives.Zeta + Some NormSteps.Zeta | FV (fv, _, []) when S.fv_eq_lid fv PC.steps_iota -> - Some Pervasives.Iota + Some NormSteps.Iota | FV (fv, _, []) when S.fv_eq_lid fv PC.steps_nbe -> - Some Pervasives.NBE + Some NormSteps.NBE | FV (fv, _, []) when S.fv_eq_lid fv PC.steps_reify -> - Some Pervasives.Reify + Some NormSteps.Reify | FV (fv, _, []) when S.fv_eq_lid fv PC.steps_zeta_full -> - Some Pervasives.ZetaFull + Some NormSteps.ZetaFull | FV (fv, _, []) when S.fv_eq_lid fv PC.steps_unascribe -> - Some Pervasives.Unascribe + Some NormSteps.Unascribe | FV (fv, _, [(l, _)]) when S.fv_eq_lid fv PC.steps_unfoldonly -> BU.bind_opt (unembed (e_list e_string) cb l) (fun ss -> - Some <| Pervasives.UnfoldOnly ss) + Some <| NormSteps.UnfoldOnly ss) | FV (fv, _, [(l, _)]) when S.fv_eq_lid fv PC.steps_unfoldfully -> BU.bind_opt (unembed (e_list e_string) cb l) (fun ss -> - Some <| Pervasives.UnfoldFully ss) + Some <| NormSteps.UnfoldFully ss) | FV (fv, _, [(l, _)]) when S.fv_eq_lid fv PC.steps_unfoldattr -> BU.bind_opt (unembed (e_list e_string) cb l) (fun ss -> - Some <| Pervasives.UnfoldAttr ss) + Some <| NormSteps.UnfoldAttr ss) | FV (fv, _, [(l, _)]) when S.fv_eq_lid fv PC.steps_unfoldqual -> BU.bind_opt (unembed (e_list e_string) cb l) (fun ss -> - Some <| Pervasives.UnfoldQual ss) + Some <| NormSteps.UnfoldQual ss) | FV (fv, _, [(l, _)]) when S.fv_eq_lid fv PC.steps_unfoldnamespace -> BU.bind_opt (unembed (e_list e_string) cb l) (fun ss -> - Some <| Pervasives.UnfoldNamespace ss) + Some <| NormSteps.UnfoldNamespace ss) | _ -> Errors.log_issue0 Errors.Warning_NotEmbedded (BU.format1 "Not an embedded norm_step: %s" (t_to_string t0)); None in mk_emb em un (fun () -> mkFV (lid_as_fv PC.norm_step_lid None) [] []) - (SE.emb_typ_of norm_step) + (SE.emb_typ_of NormSteps.norm_step) (* Interface for building primitive steps *) diff --git a/src/typechecker/FStarC.TypeChecker.NBETerm.fsti b/src/typechecker/FStarC.TypeChecker.NBETerm.fsti index a18edd1f0c7..f0ab8cc7161 100644 --- a/src/typechecker/FStarC.TypeChecker.NBETerm.fsti +++ b/src/typechecker/FStarC.TypeChecker.NBETerm.fsti @@ -286,7 +286,7 @@ instance val e_range : embedding Range.range (* sealed *) instance val e_issue : embedding FStarC.Errors.issue instance val e_document : embedding FStarC.Pprint.document instance val e_vconfig : embedding vconfig -instance val e_norm_step : embedding Pervasives.norm_step +instance val e_norm_step : embedding NormSteps.norm_step instance val e_list : #a:Type -> embedding a -> Prims.Tot (embedding (list a)) instance val e_option : embedding 'a -> Prims.Tot (embedding (option 'a)) instance val e_tuple2 : embedding 'a -> embedding 'b -> Prims.Tot (embedding ('a & 'b)) diff --git a/ulib/FStar.NormSteps.fst b/ulib/FStar.NormSteps.fst new file mode 100644 index 00000000000..10a830cf2d3 --- /dev/null +++ b/ulib/FStar.NormSteps.fst @@ -0,0 +1,85 @@ +[@@"no_prelude"] +module FStar.NormSteps + +open Prims +noeq +type norm_step = + | Simpl // Logical simplification, e.g., [P /\ True ~> P] + | Weak // Weak reduction: Do not reduce under binders + | HNF // Head normal form + | Primops // Reduce primitive operators, e.g., [1 + 1 ~> 2] + | Delta // Unfold all non-recursive definitions + | Zeta // Unroll recursive calls + | ZetaFull // Unroll recursive calls fully + | Iota // Reduce case analysis (i.e., match) + | NBE // Use normalization-by-evaluation, instead of interpretation (experimental) + | Reify // Reify effectful definitions into their representations + | NormDebug // Turn on debugging for this call + | UnfoldOnly : list string -> norm_step // Unlike Delta, unfold definitions for only the given + | UnfoldOnce : list string -> norm_step + // names, each string is a fully qualified name + // like `A.M.f` + // idem + | UnfoldFully : list string -> norm_step + | UnfoldAttr : list string -> norm_step // Unfold definitions marked with the given attributes + | UnfoldQual : list string -> norm_step + | UnfoldNamespace : list string -> norm_step + | Unmeta : norm_step + | Unascribe // Remove type ascriptions [t <: ty ~> t] + +irreducible +let simplify = Simpl + +irreducible +let weak = Weak + +irreducible +let hnf = HNF + +irreducible +let primops = Primops + +irreducible +let delta = Delta + +irreducible +let norm_debug = NormDebug + +irreducible +let zeta = Zeta + +irreducible +let zeta_full = ZetaFull + +irreducible +let iota = Iota + +irreducible +let nbe = NBE + +irreducible +let reify_ = Reify + +irreducible +let delta_only s = UnfoldOnly s + +irreducible +let delta_once s = UnfoldOnce s + +irreducible +let delta_fully s = UnfoldFully s + +irreducible +let delta_attr s = UnfoldAttr s + +irreducible +let delta_qualifier s = UnfoldAttr s + +irreducible +let delta_namespace s = UnfoldNamespace s + +irreducible +let unmeta = Unmeta + +irreducible +let unascribe = Unascribe diff --git a/ulib/FStar.NormSteps.fsti b/ulib/FStar.NormSteps.fsti new file mode 100644 index 00000000000..6841a6a83c5 --- /dev/null +++ b/ulib/FStar.NormSteps.fsti @@ -0,0 +1,163 @@ +[@@"no_prelude"] +module FStar.NormSteps + +open Prims + +(** Value of [norm_step] are used to enable specific normalization + steps, controlling how the normalizer reduces terms. *) +val norm_step : Type0 + +(** Logical simplification, e.g., [P /\ True ~> P] *) +val simplify : norm_step + +(** Weak reduction: Do not reduce under binders *) +val weak : norm_step + +(** Head normal form: Do not reduce in function arguments or in binder types *) +val hnf : norm_step + +(** Reduce primitive operators, e.g., [1 + 1 ~> 2] *) +val primops : norm_step + +(** Unfold all non-recursive definitions *) +val delta : norm_step + +(** Turn on debugging for this specific call. *) +val norm_debug : norm_step + +(** Unroll recursive calls + + Note: Since F*'s termination check is semantic rather than + syntactically structural, recursive calls in inconsistent contexts, + or recursive evaluation of open terms can diverge. + + When asking for the [zeta] step, F* implements a heuristic to + disable [zeta] when reducing terms beneath a blocked match. This + helps prevent some trivial looping behavior. However, it also + means that with [zeta] alone, your term may not reduce as much as + you might want. See [zeta_full] for that. + *) +val zeta : norm_step + +(** Unroll recursive calls + + Unlike [zeta], [zeta_full] has no looping prevention + heuristics. F* will try to unroll recursive functions as much as + it can, potentially looping. Use with care. + + Note, [zeta_full] implies [zeta]. + See [tests/micro-benchmarks/ReduceRecUnderMatch.fst] for an example. + *) +val zeta_full : norm_step + +(** Reduce case analysis (i.e., match) *) +val iota : norm_step + +(** Use normalization-by-evaluation, instead of interpretation (experimental) *) +val nbe : norm_step + +(** Reify effectful definitions into their representations *) +val reify_ : norm_step + +(** Unlike [delta], unfold definitions for only the names in the given + list. Each string is a fully qualified name like [A.M.f] *) +val delta_only (s: list string) : Tot norm_step + +(** Like [delta_only], unfold only the definitions in this list, +but do so only once. This is useful for a controlled unfolding +of recursive definitions. NOTE: if there are many occurrences +of a variable in this list, it is unspecified which one will +be unfolded (currently it depends on normalization order). *) +val delta_once (s: list string) : Tot norm_step + +(** Unfold definitions for only the names in the given list, but + unfold each definition encountered after unfolding as well. + + For example, given + + {[ + let f0 = 0 + let f1 = f0 + 1 + ]} + + [norm [delta_only [`%f1]] f1] will reduce to [f0 + 1]. + [norm [delta_fully [`%f1]] f1] will reduce to [0 + 1]. + + Each string is a fully qualified name like [A.M.f], typically + constructed using a quotation, as in the example above. *) +val delta_fully (s: list string) : Tot norm_step + +(** Rather than mention a symbol to unfold by name, it can be + convenient to tag a collection of related symbols with a common + attribute and then to ask the normalizer to reduce them all. + + For example, given: + + {[ + irreducible let my_attr = () + + [@@my_attr] + let f0 = 0 + + [@@my_attr] + let f1 = f0 + 1 + ]} + + {[norm [delta_attr [`%my_attr]] f1]} + + will reduce to [0 + 1]. + + *) +val delta_attr (s: list string) : Tot norm_step + +(** + For example, given: + + {[ + unfold + let f0 = 0 + + inline_for_extraction + let f1 = f0 + 1 + + ]} + + {[norm [delta_qualifier ["unfold"; "inline_for_extraction"]] f1]} + + will reduce to [0 + 1]. + + *) +val delta_qualifier (s: list string) : Tot norm_step + +val delta_namespace (s: list string) : Tot norm_step + +(** + This step removes the some internal meta nodes during normalization + + In most cases you shouldn't need to use this step explicitly + + *) +val unmeta : norm_step + +(** + This step removes ascriptions during normalization + + An ascription is a type or computation type annotation on + an expression, written as (e <: t) or (e <: C) + + normalize (e <: (t|C)) usually would normalize both the expression e + and the ascription + + However, with unascribe step on, it will drop the ascription + and return the result of (normalize e), + + Removing ascriptions may improve the performance, + as the normalization has less work to do + + However, ascriptions help in re-typechecking of the terms, + and in some cases, are necessary for doing so + + Use it with care + + *) +val unascribe : norm_step diff --git a/ulib/FStar.Pervasives.fst b/ulib/FStar.Pervasives.fst index 8a6da305eab..c81d953dd13 100644 --- a/ulib/FStar.Pervasives.fst +++ b/ulib/FStar.Pervasives.fst @@ -43,88 +43,6 @@ let normalize_term #_ x = x let normalize a = a -noeq -type norm_step = - | Simpl // Logical simplification, e.g., [P /\ True ~> P] - | Weak // Weak reduction: Do not reduce under binders - | HNF // Head normal form - | Primops // Reduce primitive operators, e.g., [1 + 1 ~> 2] - | Delta // Unfold all non-recursive definitions - | Zeta // Unroll recursive calls - | ZetaFull // Unroll recursive calls fully - | Iota // Reduce case analysis (i.e., match) - | NBE // Use normalization-by-evaluation, instead of interpretation (experimental) - | Reify // Reify effectful definitions into their representations - | NormDebug // Turn on debugging for this call - | UnfoldOnly : list string -> norm_step // Unlike Delta, unfold definitions for only the given - | UnfoldOnce : list string -> norm_step - // names, each string is a fully qualified name - // like `A.M.f` - // idem - | UnfoldFully : list string -> norm_step - | UnfoldAttr : list string -> norm_step // Unfold definitions marked with the given attributes - | UnfoldQual : list string -> norm_step - | UnfoldNamespace : list string -> norm_step - | Unmeta : norm_step - | Unascribe // Remove type ascriptions [t <: ty ~> t] - -irreducible -let simplify = Simpl - -irreducible -let weak = Weak - -irreducible -let hnf = HNF - -irreducible -let primops = Primops - -irreducible -let delta = Delta - -irreducible -let norm_debug = NormDebug - -irreducible -let zeta = Zeta - -irreducible -let zeta_full = ZetaFull - -irreducible -let iota = Iota - -irreducible -let nbe = NBE - -irreducible -let reify_ = Reify - -irreducible -let delta_only s = UnfoldOnly s - -irreducible -let delta_once s = UnfoldOnce s - -irreducible -let delta_fully s = UnfoldFully s - -irreducible -let delta_attr s = UnfoldAttr s - -irreducible -let delta_qualifier s = UnfoldAttr s - -irreducible -let delta_namespace s = UnfoldNamespace s - -irreducible -let unmeta = Unmeta - -irreducible -let unascribe = Unascribe - let norm _ #_ x = x let assert_norm _ = () diff --git a/ulib/FStar.Pervasives.fsti b/ulib/FStar.Pervasives.fsti index a5d7eb5ab00..b940c7d0079 100644 --- a/ulib/FStar.Pervasives.fsti +++ b/ulib/FStar.Pervasives.fsti @@ -146,178 +146,23 @@ val ambient (#a: Type) (x: a) : Type0 (** cf. [ambient], above *) val intro_ambient (#a: Type) (x: a) : Tot (squash (ambient x)) +open FStar.NormSteps /// Controlling normalization (** In any invocation of the F* normalizer, every occurrence of [normalize_term e] is reduced to the full normal for of [e]. *) +noextract val normalize_term (#a: Type) (x: a) : Tot a (** In any invocation of the F* normalizer, every occurrence of [normalize e] is reduced to the full normal for of [e]. *) +noextract val normalize (a: Type0) : Type0 -(** Value of [norm_step] are used to enable specific normalization - steps, controlling how the normalizer reduces terms. *) -val norm_step : Type0 - -(** Logical simplification, e.g., [P /\ True ~> P] *) -val simplify : norm_step - -(** Weak reduction: Do not reduce under binders *) -val weak : norm_step - -(** Head normal form: Do not reduce in function arguments or in binder types *) -val hnf : norm_step - -(** Reduce primitive operators, e.g., [1 + 1 ~> 2] *) -val primops : norm_step - -(** Unfold all non-recursive definitions *) -val delta : norm_step - -(** Turn on debugging for this specific call. *) -val norm_debug : norm_step - -(** Unroll recursive calls - - Note: Since F*'s termination check is semantic rather than - syntactically structural, recursive calls in inconsistent contexts, - or recursive evaluation of open terms can diverge. - - When asking for the [zeta] step, F* implements a heuristic to - disable [zeta] when reducing terms beneath a blocked match. This - helps prevent some trivial looping behavior. However, it also - means that with [zeta] alone, your term may not reduce as much as - you might want. See [zeta_full] for that. - *) -val zeta : norm_step - -(** Unroll recursive calls - - Unlike [zeta], [zeta_full] has no looping prevention - heuristics. F* will try to unroll recursive functions as much as - it can, potentially looping. Use with care. - - Note, [zeta_full] implies [zeta]. - See [tests/micro-benchmarks/ReduceRecUnderMatch.fst] for an example. - *) -val zeta_full : norm_step - -(** Reduce case analysis (i.e., match) *) -val iota : norm_step - -(** Use normalization-by-evaluation, instead of interpretation (experimental) *) -val nbe : norm_step - -(** Reify effectful definitions into their representations *) -val reify_ : norm_step - -(** Unlike [delta], unfold definitions for only the names in the given - list. Each string is a fully qualified name like [A.M.f] *) -val delta_only (s: list string) : Tot norm_step - -(** Like [delta_only], unfold only the definitions in this list, -but do so only once. This is useful for a controlled unfolding -of recursive definitions. NOTE: if there are many occurrences -of a variable in this list, it is unspecified which one will -be unfolded (currently it depends on normalization order). *) -val delta_once (s: list string) : Tot norm_step - -(** Unfold definitions for only the names in the given list, but - unfold each definition encountered after unfolding as well. - - For example, given - - {[ - let f0 = 0 - let f1 = f0 + 1 - ]} - - [norm [delta_only [`%f1]] f1] will reduce to [f0 + 1]. - [norm [delta_fully [`%f1]] f1] will reduce to [0 + 1]. - - Each string is a fully qualified name like [A.M.f], typically - constructed using a quotation, as in the example above. *) -val delta_fully (s: list string) : Tot norm_step - -(** Rather than mention a symbol to unfold by name, it can be - convenient to tag a collection of related symbols with a common - attribute and then to ask the normalizer to reduce them all. - - For example, given: - - {[ - irreducible let my_attr = () - - [@@my_attr] - let f0 = 0 - - [@@my_attr] - let f1 = f0 + 1 - ]} - - {[norm [delta_attr [`%my_attr]] f1]} - - will reduce to [0 + 1]. - - *) -val delta_attr (s: list string) : Tot norm_step - -(** - For example, given: - - {[ - unfold - let f0 = 0 - - inline_for_extraction - let f1 = f0 + 1 - - ]} - - {[norm [delta_qualifier ["unfold"; "inline_for_extraction"]] f1]} - - will reduce to [0 + 1]. - - *) -val delta_qualifier (s: list string) : Tot norm_step - -val delta_namespace (s: list string) : Tot norm_step - -(** - This step removes the some internal meta nodes during normalization - - In most cases you shouldn't need to use this step explicitly - - *) -val unmeta : norm_step - -(** - This step removes ascriptions during normalization - - An ascription is a type or computation type annotation on - an expression, written as (e <: t) or (e <: C) - - normalize (e <: (t|C)) usually would normalize both the expression e - and the ascription - - However, with unascribe step on, it will drop the ascription - and return the result of (normalize e), - - Removing ascriptions may improve the performance, - as the normalization has less work to do - - However, ascriptions help in re-typechecking of the terms, - and in some cases, are necessary for doing so - - Use it with care - - *) -val unascribe : norm_step - (** [norm s e] requests normalization of [e] with the reduction steps [s]. *) +noextract val norm (s: list norm_step) (#a: Type) (x: a) : Tot a (** [assert_norm p] reduces [p] as much as possible and then asks the diff --git a/ulib/FStar.Prelude.fsti b/ulib/FStar.Prelude.fsti index 90bdb996c4a..be5faa2b37d 100644 --- a/ulib/FStar.Prelude.fsti +++ b/ulib/FStar.Prelude.fsti @@ -4,4 +4,5 @@ module FStar.Prelude include Prims include FStar.Pervasives.Native include FStar.Pervasives +include FStar.NormSteps include FStar.Attributes From 5040bcd43011c023145ec9922009713c3e440900 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 9 Feb 2025 20:37:47 -0800 Subject: [PATCH 09/14] X64.Vale.Decls: bump rlimit --- tests/vale/X64.Vale.Decls.fst | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/tests/vale/X64.Vale.Decls.fst b/tests/vale/X64.Vale.Decls.fst index e790f3d271b..b081ee3f4f6 100644 --- a/tests/vale/X64.Vale.Decls.fst +++ b/tests/vale/X64.Vale.Decls.fst @@ -213,12 +213,14 @@ irreducible val va_irreducible_lemma_Add64 : va_b0:va_codes -> va_s0:va_state -> ((va_eval_dst_operand_uint64 va_s0 dst) + (va_eval_operand_uint64 va_s0 src))) /\ (va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_dst_operand dst va_sM va_s0))))))) +#push-options "--z3rlimit_factor 20" irreducible let va_irreducible_lemma_Add64 va_b0 va_s0 va_sN dst src = (va_reveal_opaque (va_transparent_code_Add64 dst src)); let (va_old_s:va_state) = va_s0 in let (va_sM, (va_cM:va_code), va_bM) = (va_lemma_block va_b0 va_s0 va_sN) in regs_eval_code_one(va_transparent_code_Add64 dst src) dst va_s0 va_sM; (va_bM, va_sM) +#pop-options let va_lemma_Add64 = va_irreducible_lemma_Add64 val va_transparent_code_Add64Wrap : dst:va_dst_operand -> src:va_operand -> Tot va_code @@ -309,6 +311,7 @@ irreducible val va_irreducible_lemma_Adc64Wrap : va_b0:va_codes -> va_s0:va_stat (va_get_flags va_s0)) then 1 else 0) >= nat64_max) /\ (va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_dst_operand dst va_sM va_s0))))))) +#push-options "--z3rlimit_factor 20" irreducible let va_irreducible_lemma_Adc64Wrap va_b0 va_s0 va_sN dst src = (va_reveal_opaque (va_transparent_code_Adc64Wrap dst src)); let (va_old_s:va_state) = va_s0 in @@ -326,6 +329,7 @@ irreducible let va_irreducible_lemma_Adc64Wrap va_b0 va_s0 va_sN dst src = (va_update_ok va_sM (va_update_dst_operand dst va_sM va_s0)))) ); (va_bM, va_sM) +#pop-options let va_lemma_Adc64Wrap = va_irreducible_lemma_Adc64Wrap val va_transparent_code_Sub64 : dst:va_dst_operand -> src:va_operand -> Tot va_code @@ -444,6 +448,7 @@ irreducible val va_irreducible_lemma_IMul64 : va_b0:va_codes -> va_s0:va_state - (va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_dst_operand dst va_sM va_s0))))))) #restart-solver +#push-options "--z3rlimit_factor 20" irreducible let va_irreducible_lemma_IMul64 va_b0 va_s0 va_sN dst src = (va_reveal_opaque (va_transparent_code_IMul64 dst src)); let (va_old_s:va_state) = va_s0 in @@ -451,6 +456,7 @@ irreducible let va_irreducible_lemma_IMul64 va_b0 va_s0 va_sN dst src = regs_eval_code_one (va_transparent_code_IMul64 dst src) dst va_s0 va_sM; (lemma_mul_nat (va_eval_dst_operand_uint64 va_old_s dst) (va_eval_operand_uint64 va_old_s src)); (va_bM, va_sM) +#pop-options let va_lemma_IMul64 = va_irreducible_lemma_IMul64 val va_transparent_code_Xor64 : dst:va_dst_operand -> src:va_operand -> Tot va_code From c9d740bb3d9fea3d164d22ba92bb73db125a00d7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 9 Feb 2025 20:38:42 -0800 Subject: [PATCH 10/14] Update expected output (line numbers, module names) --- ...NegativeTests.Neg.fst.json_output.expected | 2 +- .../NegativeTests.Neg.fst.output.expected | 2 +- tests/vale/DeltaAttr.fst.output.expected | 44 +++++++++---------- 3 files changed, 22 insertions(+), 26 deletions(-) diff --git a/tests/error-messages/NegativeTests.Neg.fst.json_output.expected b/tests/error-messages/NegativeTests.Neg.fst.json_output.expected index cee9400b4f5..0f9042de2ee 100644 --- a/tests/error-messages/NegativeTests.Neg.fst.json_output.expected +++ b/tests/error-messages/NegativeTests.Neg.fst.json_output.expected @@ -20,7 +20,7 @@ {"msg":["Subtyping check failed","Expected type _: FStar.Pervasives.Native.option 'a {Some? _}\ngot type FStar.Pervasives.Native.option 'a","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.Pervasives.Native.fst","start_pos":{"line":33,"col":4},"end_pos":{"line":33,"col":8}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":46,"col":30},"end_pos":{"line":46,"col":31}}},"number":19,"ctx":["While typechecking the top-level declaration `let bad_projector`","While typechecking the top-level declaration `[@@expect_failure] let bad_projector`"]} >>] >> Got issues: [ -{"msg":["Subtyping check failed","Expected type _: FStar.Pervasives.result Prims.int {V? _}\ngot type FStar.Pervasives.result Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.Pervasives.fsti","start_pos":{"line":526,"col":4},"end_pos":{"line":526,"col":5}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":50,"col":45},"end_pos":{"line":50,"col":47}}},"number":19,"ctx":["While typechecking the top-level declaration `val NegativeTests.Neg.test`","While typechecking the top-level declaration `[@@expect_failure] val NegativeTests.Neg.test`"]} +{"msg":["Subtyping check failed","Expected type _: FStar.Pervasives.result Prims.int {V? _}\ngot type FStar.Pervasives.result Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.Pervasives.fsti","start_pos":{"line":371,"col":4},"end_pos":{"line":371,"col":5}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":50,"col":45},"end_pos":{"line":50,"col":47}}},"number":19,"ctx":["While typechecking the top-level declaration `val NegativeTests.Neg.test`","While typechecking the top-level declaration `[@@expect_failure] val NegativeTests.Neg.test`"]} >>] >> Got issues: [ {"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":55,"col":25},"end_pos":{"line":55,"col":26}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let h1`","While typechecking the top-level declaration `[@@expect_failure] let h1`"]} diff --git a/tests/error-messages/NegativeTests.Neg.fst.output.expected b/tests/error-messages/NegativeTests.Neg.fst.output.expected index 498f2dbc414..1294cb7b019 100644 --- a/tests/error-messages/NegativeTests.Neg.fst.output.expected +++ b/tests/error-messages/NegativeTests.Neg.fst.output.expected @@ -63,7 +63,7 @@ got type FStar.Pervasives.result Prims.int - The SMT solver could not prove the query. Use --query_stats for more details. - - See also FStar.Pervasives.fsti(526,4-526,5) + - See also FStar.Pervasives.fsti(371,4-371,5) >>] >> Got issues: [ diff --git a/tests/vale/DeltaAttr.fst.output.expected b/tests/vale/DeltaAttr.fst.output.expected index af16be38e6b..49816b4d3de 100644 --- a/tests/vale/DeltaAttr.fst.output.expected +++ b/tests/vale/DeltaAttr.fst.output.expected @@ -20,29 +20,27 @@ let sub_1 x = x - 1 <: Prims.int let add x = x + x <: Prims.int let test_1 x = FStar.Tactics.Effect.synth_by_tactic (fun _ -> - DeltaAttr.normalize [FStar.Pervasives.delta_attr ["DeltaAttr.myattr"]] + DeltaAttr.normalize [FStar.NormSteps.delta_attr ["DeltaAttr.myattr"]] (DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x)))) <: Prims.int let test_2 x = FStar.Tactics.Effect.synth_by_tactic (fun _ -> - DeltaAttr.normalize [FStar.Pervasives.delta_attr ["DeltaAttr.otherattr"]] + DeltaAttr.normalize [FStar.NormSteps.delta_attr ["DeltaAttr.otherattr"]] (DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x)))) <: Prims.int let test_3 x = FStar.Tactics.Effect.synth_by_tactic (fun _ -> - DeltaAttr.normalize [ - FStar.Pervasives.delta_attr ["DeltaAttr.myattr"; "DeltaAttr.otherattr"] - ] + DeltaAttr.normalize [FStar.NormSteps.delta_attr ["DeltaAttr.myattr"; "DeltaAttr.otherattr"]] (DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x)))) <: Prims.int let test_3' x = FStar.Tactics.Effect.synth_by_tactic (fun _ -> DeltaAttr.normalize [ - FStar.Pervasives.delta_attr ["DeltaAttr.myattr"]; - FStar.Pervasives.delta_attr ["DeltaAttr.otherattr"] + FStar.NormSteps.delta_attr ["DeltaAttr.myattr"]; + FStar.NormSteps.delta_attr ["DeltaAttr.otherattr"] ] (DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x)))) <: @@ -50,8 +48,8 @@ let test_3' x = let test_4 x = FStar.Tactics.Effect.synth_by_tactic (fun _ -> DeltaAttr.normalize [ - FStar.Pervasives.delta_attr ["DeltaAttr.myattr"]; - FStar.Pervasives.delta_only ["DeltaAttr.add"] + FStar.NormSteps.delta_attr ["DeltaAttr.myattr"]; + FStar.NormSteps.delta_only ["DeltaAttr.add"] ] (DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x)))) <: @@ -59,9 +57,9 @@ let test_4 x = let test_5 x = FStar.Tactics.Effect.synth_by_tactic (fun _ -> DeltaAttr.normalize [ - FStar.Pervasives.delta_only ["DeltaAttr.add"]; - FStar.Pervasives.delta_only ["DeltaAttr.add_1"]; - FStar.Pervasives.delta_only ["DeltaAttr.sub_1"] + FStar.NormSteps.delta_only ["DeltaAttr.add"]; + FStar.NormSteps.delta_only ["DeltaAttr.add_1"]; + FStar.NormSteps.delta_only ["DeltaAttr.sub_1"] ] (DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x)))) <: @@ -90,29 +88,27 @@ let sub_1 x = x - 1 <: Prims.int let add x = x + x <: Prims.int let test_1 x = FStar.Tactics.Effect.synth_by_tactic (fun _ -> - DeltaAttr.normalize [FStar.Pervasives.delta_attr ["DeltaAttr.myattr"]] + DeltaAttr.normalize [FStar.NormSteps.delta_attr ["DeltaAttr.myattr"]] (DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x)))) <: Prims.int let test_2 x = FStar.Tactics.Effect.synth_by_tactic (fun _ -> - DeltaAttr.normalize [FStar.Pervasives.delta_attr ["DeltaAttr.otherattr"]] + DeltaAttr.normalize [FStar.NormSteps.delta_attr ["DeltaAttr.otherattr"]] (DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x)))) <: Prims.int let test_3 x = FStar.Tactics.Effect.synth_by_tactic (fun _ -> - DeltaAttr.normalize [ - FStar.Pervasives.delta_attr ["DeltaAttr.myattr"; "DeltaAttr.otherattr"] - ] + DeltaAttr.normalize [FStar.NormSteps.delta_attr ["DeltaAttr.myattr"; "DeltaAttr.otherattr"]] (DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x)))) <: Prims.int let test_3' x = FStar.Tactics.Effect.synth_by_tactic (fun _ -> DeltaAttr.normalize [ - FStar.Pervasives.delta_attr ["DeltaAttr.myattr"]; - FStar.Pervasives.delta_attr ["DeltaAttr.otherattr"] + FStar.NormSteps.delta_attr ["DeltaAttr.myattr"]; + FStar.NormSteps.delta_attr ["DeltaAttr.otherattr"] ] (DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x)))) <: @@ -120,8 +116,8 @@ let test_3' x = let test_4 x = FStar.Tactics.Effect.synth_by_tactic (fun _ -> DeltaAttr.normalize [ - FStar.Pervasives.delta_attr ["DeltaAttr.myattr"]; - FStar.Pervasives.delta_only ["DeltaAttr.add"] + FStar.NormSteps.delta_attr ["DeltaAttr.myattr"]; + FStar.NormSteps.delta_only ["DeltaAttr.add"] ] (DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x)))) <: @@ -129,9 +125,9 @@ let test_4 x = let test_5 x = FStar.Tactics.Effect.synth_by_tactic (fun _ -> DeltaAttr.normalize [ - FStar.Pervasives.delta_only ["DeltaAttr.add"]; - FStar.Pervasives.delta_only ["DeltaAttr.add_1"]; - FStar.Pervasives.delta_only ["DeltaAttr.sub_1"] + FStar.NormSteps.delta_only ["DeltaAttr.add"]; + FStar.NormSteps.delta_only ["DeltaAttr.add_1"]; + FStar.NormSteps.delta_only ["DeltaAttr.sub_1"] ] (DeltaAttr.add (DeltaAttr.sub_1 (DeltaAttr.add_1 x)))) <: From 2a8b41d536f9212d42c64d92325f15a05e554e51 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 9 Feb 2025 22:22:51 -0800 Subject: [PATCH 11/14] F#: rename prims.fs -> Prims.fs --- fsharp/base/{prims.fs => Prims.fs} | 0 fsharp/ulibfs.fsproj | 2 +- 2 files changed, 1 insertion(+), 1 deletion(-) rename fsharp/base/{prims.fs => Prims.fs} (100%) diff --git a/fsharp/base/prims.fs b/fsharp/base/Prims.fs similarity index 100% rename from fsharp/base/prims.fs rename to fsharp/base/Prims.fs diff --git a/fsharp/ulibfs.fsproj b/fsharp/ulibfs.fsproj index 61d0616506b..d9bdc12f15d 100644 --- a/fsharp/ulibfs.fsproj +++ b/fsharp/ulibfs.fsproj @@ -15,7 +15,7 @@ - + From 2c7e0b7288779c7f6c2920887109de97af05e2b5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 9 Feb 2025 22:01:53 -0800 Subject: [PATCH 12/14] Fix F# extraction, no need to open Prims --- fsharp/base/Prims.fs | 1 + fsharp/ulibfs.fsproj | 1 + src/extraction/FStarC.Extraction.ML.Code.fst | 2 +- 3 files changed, 3 insertions(+), 1 deletion(-) diff --git a/fsharp/base/Prims.fs b/fsharp/base/Prims.fs index 41e833d385a..9a5ccdb82fd 100644 --- a/fsharp/base/Prims.fs +++ b/fsharp/base/Prims.fs @@ -32,6 +32,7 @@ let ( >= ) (x:int) (y:int) = x >= y let ( < ) (x:int) (y:int) = x < y let ( > ) (x:int) (y:int) = x > y let (mod) (x:int) (y:int) = snd (ediv_rem x y) +let mod_f x y = x mod y let ( ~- ) (x:int) = -x let abs (x:int) = BigInteger.Abs x let of_int (x:FSharp.Core.int) = BigInteger x diff --git a/fsharp/ulibfs.fsproj b/fsharp/ulibfs.fsproj index d9bdc12f15d..07ec6913806 100644 --- a/fsharp/ulibfs.fsproj +++ b/fsharp/ulibfs.fsproj @@ -51,6 +51,7 @@ + diff --git a/src/extraction/FStarC.Extraction.ML.Code.fst b/src/extraction/FStarC.Extraction.ML.Code.fst index 92b9a1d2771..e0089c64954 100644 --- a/src/extraction/FStarC.Extraction.ML.Code.fst +++ b/src/extraction/FStarC.Extraction.ML.Code.fst @@ -121,6 +121,7 @@ let mlpath_of_mlpath (currentModule : mlsymbol) (x : mlpath) : mlpath = match string_of_mlpath x with | "Prims.Some" -> ([], "Some") | "Prims.None" -> ([], "None") + | "Prims.op_Modulus" -> (["Prims"], "mod_f") | _ -> let ns, x = x in (path_of_ns currentModule ns, x) @@ -158,7 +159,6 @@ let infix_prim_ops = [ ("op_GreaterThanOrEqual", e_bin_prio_order , ">="); ("op_LessThan" , e_bin_prio_order , "<" ); ("op_GreaterThan" , e_bin_prio_order , ">" ); - ("op_Modulus" , e_bin_prio_order , "mod" ); ] (* -------------------------------------------------------------------- *) From 73e7ec0b66d1c6e5779e580812ef2dbbb47ef420 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 9 Feb 2025 22:07:44 -0800 Subject: [PATCH 13/14] extraction: remove unneeded opens --- src/extraction/FStarC.Extraction.ML.Code.fst | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/src/extraction/FStarC.Extraction.ML.Code.fst b/src/extraction/FStarC.Extraction.ML.Code.fst index e0089c64954..dfceca27e7f 100644 --- a/src/extraction/FStarC.Extraction.ML.Code.fst +++ b/src/extraction/FStarC.Extraction.ML.Code.fst @@ -804,14 +804,6 @@ let doc_of_mllib_r (MLLib mllib) = ] and for1_mod istop (mod_name, sigmod, MLLib sub) = let target_mod_name = Util.flatten_mlpath mod_name in - let maybe_open_pervasives = - match mod_name with - | ["FStar"], "Pervasives" -> [] - | _ -> - let pervasives = Util.flatten_mlpath (["FStar"], "Pervasives") in - [hardline; - text ("open " ^ pervasives)] - in let head = reduce1 (if Util.codegen_fsharp() then [text "module"; text target_mod_name] else if not istop @@ -827,9 +819,6 @@ let doc_of_mllib_r (MLLib mllib) = reduce <| (prefix @ [ head; hardline; - text "open Prims"] @ - maybe_open_pervasives @ - [hardline; (match doc with | None -> empty | Some s -> cat s hardline); From 056738fb386f2d7027da14cb70dfcf60e0c97fb8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 9 Feb 2025 22:47:38 -0800 Subject: [PATCH 14/14] Update expected F# output, less opens --- tests/bug-reports/closed/RemoveUnusedTyparsIFace_A.fs.expected | 2 -- tests/bug-reports/closed/RemoveUnusedTyparsIFace_B.fs.expected | 2 -- tests/bug-reports/closed/RemoveUnusedTypars_A.fs.expected | 2 -- tests/bug-reports/closed/RemoveUnusedTypars_B.fs.expected | 2 -- 4 files changed, 8 deletions(-) diff --git a/tests/bug-reports/closed/RemoveUnusedTyparsIFace_A.fs.expected b/tests/bug-reports/closed/RemoveUnusedTyparsIFace_A.fs.expected index 8543bcf999a..6b75718cd26 100644 --- a/tests/bug-reports/closed/RemoveUnusedTyparsIFace_A.fs.expected +++ b/tests/bug-reports/closed/RemoveUnusedTyparsIFace_A.fs.expected @@ -1,7 +1,5 @@ #light "off" module RemoveUnusedTyparsIFace_A -open Prims -open FStar_Pervasives type 'a t = 'a Prims.list diff --git a/tests/bug-reports/closed/RemoveUnusedTyparsIFace_B.fs.expected b/tests/bug-reports/closed/RemoveUnusedTyparsIFace_B.fs.expected index fd9348d6372..2ade2e28c92 100644 --- a/tests/bug-reports/closed/RemoveUnusedTyparsIFace_B.fs.expected +++ b/tests/bug-reports/closed/RemoveUnusedTyparsIFace_B.fs.expected @@ -1,7 +1,5 @@ #light "off" module RemoveUnusedTyparsIFace_B -open Prims -open FStar_Pervasives let f = (fun ( x : 'a RemoveUnusedTyparsIFace_A.t ) -> x) diff --git a/tests/bug-reports/closed/RemoveUnusedTypars_A.fs.expected b/tests/bug-reports/closed/RemoveUnusedTypars_A.fs.expected index 6c8b1818332..f62f837cd29 100644 --- a/tests/bug-reports/closed/RemoveUnusedTypars_A.fs.expected +++ b/tests/bug-reports/closed/RemoveUnusedTypars_A.fs.expected @@ -1,7 +1,5 @@ #light "off" module RemoveUnusedTypars_A -open Prims -open FStar_Pervasives type 'a t = 'a Prims.list diff --git a/tests/bug-reports/closed/RemoveUnusedTypars_B.fs.expected b/tests/bug-reports/closed/RemoveUnusedTypars_B.fs.expected index 44a98c72875..f7b5938f282 100644 --- a/tests/bug-reports/closed/RemoveUnusedTypars_B.fs.expected +++ b/tests/bug-reports/closed/RemoveUnusedTypars_B.fs.expected @@ -1,7 +1,5 @@ #light "off" module RemoveUnusedTypars_B -open Prims -open FStar_Pervasives let f = (fun ( x : 'a RemoveUnusedTypars_A.t ) -> x)