Adding attributes to projectors, discriminators, and methods

Makefile

@@ -311,10 +311,12 @@ setlink-%:
 	ln -sf $(CURDIR)/.scripts/get_fstar_z3.sh bin/get_fstar_z3.sh
 
 stage1: .install-stage1.touch
+.PHONY: 1
 1: stage1
 	$(MAKE) setlink-1
 
 stage2: .install-stage2.touch
+.PHONY: 2
 2: stage2
 	$(MAKE) setlink-2
 

examples/data_structures/BinomialQueue.fst

@@ -506,6 +506,7 @@ let rec keys_append (l1 l2:forest) (ms1 ms2:ms)
   | [] -> ()
   | _::tl -> keys_append tl l2 (keys tl) ms2
 
+#push-options "--z3rlimit_factor 10"
 let rec unzip_repr (d:nat) (upper_bound:key_t) (t:tree) (lt:ms)
   : Lemma
       (requires
@@ -522,6 +523,7 @@ let rec unzip_repr (d:nat) (upper_bound:key_t) (t:tree) (lt:ms)
       (keys_of_tree right) (ms_append (keys_of_tree left)
                                       (ms_append (ms_singleton k)
                                                  ms_empty))
+#pop-options
 
 let heap_delete_max_repr (d:pos) (t:tree) (lt:ms)
   : Lemma

src/parser/FStarC.Parser.Const.fst

@@ -378,6 +378,9 @@ let do_not_unrefine_attr = pconst "do_not_unrefine"
 let desugar_of_variant_record_lid = attr "desugar_of_variant_record"
 let coercion_lid = attr "coercion"
 
+let projector_attr     = pconst "projector"
+let discriminator_attr = pconst "discriminator"
+
 let remove_unused_type_parameters_lid = psconst "remove_unused_type_parameters"
 
 

src/tosyntax/FStarC.ToSyntax.ToSyntax.fst

@@ -2792,6 +2792,7 @@ let mk_data_discriminators quals env datas attrs =
                   then S.Assumption::q@quals
                   else q@quals
     in
+    let attrs = S.fvar C.discriminator_attr None :: attrs in
     datas |> List.map (fun d ->
         let disc_name = U.mk_discriminator d in
         { sigel = Sig_declare_typ {lid=disc_name; us=[]; t=Syntax.tun};
@@ -2828,6 +2829,7 @@ let mk_indexed_projector_names iquals fvq attrs env lid (fields:list S.binder) =
             in
             quals (OnlyName :: S.Projector(lid, x.ppname) :: iquals)
         in
+        let attrs = S.fvar C.projector_attr None :: attrs in
         let decl = { sigel = Sig_declare_typ {lid=field_name; us=[]; t=Syntax.tun};
                      sigquals = quals;
                      sigrng = range_of_lid field_name;

src/typechecker/FStarC.TypeChecker.TcInductive.fst

@@ -1064,6 +1064,7 @@ let mk_discriminator_and_indexed_projectors iquals                   (* Qualifie
                 //(if only_decl && (not <| env.is_iface || env.admit) then [S.Assumption] else []) @
                 List.filter (function S.Inline_for_extraction | S.NoExtract | S.Private -> true | _ -> false ) iquals
             in
+            let attrs = S.fvar C.discriminator_attr None :: attrs in
 
             (* Type of the discriminator *)
             let binders = imp_binders@[unrefined_arg_binder] in
@@ -1170,6 +1171,7 @@ let mk_discriminator_and_indexed_projectors iquals                   (* Qualifie
               then S.Assumption::q
               else q
           in
+          let attrs = S.fvar C.projector_attr None :: attrs in
           let quals =
               let iquals = iquals |> List.filter (function
                   | S.Inline_for_extraction

tests/error-messages/ArrowRanges.fst.json_output.expected

@@ -1,5 +1,5 @@
 >> Got issues: [
-{"msg":["Subtyping check failed","Expected type Prims.eqtype\ngot type Type0","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":73,"col":23},"end_pos":{"line":73,"col":30}},"use":{"file_name":"ArrowRanges.fst","start_pos":{"line":4,"col":30},"end_pos":{"line":4,"col":39}}},"number":19,"ctx":["While typechecking the top-level declaration `let ppof`","While typechecking the top-level declaration `[@@expect_failure] let ppof`"]}
+{"msg":["Subtyping check failed","Expected type Prims.eqtype\ngot type Type0","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":81,"col":23},"end_pos":{"line":81,"col":30}},"use":{"file_name":"ArrowRanges.fst","start_pos":{"line":4,"col":30},"end_pos":{"line":4,"col":39}}},"number":19,"ctx":["While typechecking the top-level declaration `let ppof`","While typechecking the top-level declaration `[@@expect_failure] let ppof`"]}
 >>]
 >> Got issues: [
 {"msg":["Failed to prove that the type\n'ArrowRanges.ppof'\nsupports decidable equality because of this argument.","Add either the 'noeq' or 'unopteq' qualifier","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"ArrowRanges.fst","start_pos":{"line":7,"col":0},"end_pos":{"line":11,"col":1}},"use":{"file_name":"ArrowRanges.fst","start_pos":{"line":8,"col":10},"end_pos":{"line":8,"col":28}}},"number":19,"ctx":["While typechecking the top-level declaration `type ArrowRanges.ppof`","While typechecking the top-level declaration `[@@expect_failure] type ArrowRanges.ppof`"]}

tests/error-messages/ArrowRanges.fst.output.expected

@@ -4,7 +4,7 @@
   - Expected type Prims.eqtype got type Type0
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
-  - See also Prims.fst(73,23-73,30)
+  - See also Prims.fst(81,23-81,30)
 
 >>]
 >> Got issues: [

tests/error-messages/Basic.fst.json_output.expected

@@ -26,11 +26,11 @@
 {"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Basic.fst","start_pos":{"line":14,"col":50},"end_pos":{"line":14,"col":55}},"use":{"file_name":"Basic.fst","start_pos":{"line":14,"col":38},"end_pos":{"line":14,"col":49}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
 >>]
 >> 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":"Prims.fst","start_pos":{"line":451,"col":90},"end_pos":{"line":451,"col":102}},"use":{"file_name":"Basic.fst","start_pos":{"line":17,"col":29},"end_pos":{"line":17,"col":31}}},"number":19,"ctx":["While typechecking the top-level declaration `let test2`","While typechecking the top-level declaration `[@@expect_failure] let test2`"]}
+{"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":459,"col":90},"end_pos":{"line":459,"col":102}},"use":{"file_name":"Basic.fst","start_pos":{"line":17,"col":29},"end_pos":{"line":17,"col":31}}},"number":19,"ctx":["While typechecking the top-level declaration `let test2`","While typechecking the top-level declaration `[@@expect_failure] let test2`"]}
 >>]
 >> 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":"Prims.fst","start_pos":{"line":451,"col":90},"end_pos":{"line":451,"col":102}},"use":{"file_name":"Basic.fst","start_pos":{"line":20,"col":29},"end_pos":{"line":20,"col":31}}},"number":19,"ctx":["While typechecking the top-level declaration `let test3`","While typechecking the top-level declaration `[@@expect_failure] let test3`"]}
+{"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":459,"col":90},"end_pos":{"line":459,"col":102}},"use":{"file_name":"Basic.fst","start_pos":{"line":20,"col":29},"end_pos":{"line":20,"col":31}}},"number":19,"ctx":["While typechecking the top-level declaration `let test3`","While typechecking the top-level declaration `[@@expect_failure] let test3`"]}
 >>]
 >> 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":"Prims.fst","start_pos":{"line":451,"col":90},"end_pos":{"line":451,"col":102}},"use":{"file_name":"Basic.fst","start_pos":{"line":23,"col":46},"end_pos":{"line":23,"col":48}}},"number":19,"ctx":["While typechecking the top-level declaration `let test6`","While typechecking the top-level declaration `[@@expect_failure] let test6`"]}
+{"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":459,"col":90},"end_pos":{"line":459,"col":102}},"use":{"file_name":"Basic.fst","start_pos":{"line":23,"col":46},"end_pos":{"line":23,"col":48}}},"number":19,"ctx":["While typechecking the top-level declaration `let test6`","While typechecking the top-level declaration `[@@expect_failure] let test6`"]}
 >>]

tests/error-messages/Basic.fst.output.expected

@@ -72,22 +72,22 @@
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
-  - See also Prims.fst(451,90-451,102)
+  - See also Prims.fst(459,90-459,102)
 
 >>]
 >> Got issues: [
 * Error 19 at Basic.fst(20,29-20,31):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
-  - See also Prims.fst(451,90-451,102)
+  - See also Prims.fst(459,90-459,102)
 
 >>]
 >> Got issues: [
 * Error 19 at Basic.fst(23,46-23,48):
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
-  - See also Prims.fst(451,90-451,102)
+  - See also Prims.fst(459,90-459,102)
 
 >>]

tests/error-messages/Bug1918.fst.json_output.expected

@@ -1,3 +1,3 @@
 >> Got issues: [
-{"msg":["Could not solve typeclass constraint `Bug1918.mon`"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Typeclasses.fst","start_pos":{"line":297,"col":6},"end_pos":{"line":300,"col":7}},"use":{"file_name":"Bug1918.fst","start_pos":{"line":11,"col":13},"end_pos":{"line":11,"col":14}}},"number":228,"ctx":["While synthesizing term with a tactic","Running tactic for meta-arg","While typechecking the top-level declaration `let comp2`","While typechecking the top-level declaration `[@@expect_failure] let comp2`"]}
+{"msg":["Could not solve typeclass constraint `Bug1918.mon`"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Typeclasses.fst","start_pos":{"line":293,"col":6},"end_pos":{"line":296,"col":7}},"use":{"file_name":"Bug1918.fst","start_pos":{"line":11,"col":13},"end_pos":{"line":11,"col":14}}},"number":228,"ctx":["While synthesizing term with a tactic","Running tactic for meta-arg","While typechecking the top-level declaration `let comp2`","While typechecking the top-level declaration `[@@expect_failure] let comp2`"]}
 >>]

tests/error-messages/Bug1918.fst.output.expected

@@ -1,6 +1,6 @@
 >> Got issues: [
 * Error 228 at Bug1918.fst(11,13-11,14):
   - Could not solve typeclass constraint `Bug1918.mon`
-  - See also FStar.Tactics.Typeclasses.fst(297,6-300,7)
+  - See also FStar.Tactics.Typeclasses.fst(293,6-296,7)
 
 >>]

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":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`"]}
+{"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":682,"col":18},"end_pos":{"line":682,"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":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`"]}
+{"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":682,"col":18},"end_pos":{"line":682,"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":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`"]}
+{"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":682,"col":18},"end_pos":{"line":682,"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":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'`"]}
+{"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":682,"col":18},"end_pos":{"line":682,"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":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'`"]}
+{"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":682,"col":18},"end_pos":{"line":682,"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'`"]}
 >>]

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(674,18-674,24)
+  - See also Prims.fst(682,18-682,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(674,18-674,24)
+  - See also Prims.fst(682,18-682,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(674,18-674,24)
+  - See also Prims.fst(682,18-682,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(674,18-674,24)
+  - See also Prims.fst(682,18-682,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(674,18-674,24)
+  - See also Prims.fst(682,18-682,24)
 
 >>]

tests/error-messages/Inference.fst.json_output.expected

@@ -1,4 +1,4 @@
 >> Got issues: [
-{"msg":["Subtyping check failed","Expected type Prims.eqtype\ngot type Type0","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":73,"col":23},"end_pos":{"line":73,"col":30}},"use":{"file_name":"Inference.fst","start_pos":{"line":20,"col":14},"end_pos":{"line":20,"col":15}}},"number":19,"ctx":["While typechecking the top-level declaration `let alloc_fails`","While typechecking the top-level declaration `[@@expect_failure] let alloc_fails`"]}
-{"msg":["Subtyping check failed","Expected type Prims.eqtype\ngot type Type0","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":73,"col":23},"end_pos":{"line":73,"col":30}},"use":{"file_name":"Inference.fst","start_pos":{"line":20,"col":14},"end_pos":{"line":20,"col":15}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let alloc_fails`","While typechecking the top-level declaration `[@@expect_failure] let alloc_fails`"]}
+{"msg":["Subtyping check failed","Expected type Prims.eqtype\ngot type Type0","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":81,"col":23},"end_pos":{"line":81,"col":30}},"use":{"file_name":"Inference.fst","start_pos":{"line":20,"col":14},"end_pos":{"line":20,"col":15}}},"number":19,"ctx":["While typechecking the top-level declaration `let alloc_fails`","While typechecking the top-level declaration `[@@expect_failure] let alloc_fails`"]}
+{"msg":["Subtyping check failed","Expected type Prims.eqtype\ngot type Type0","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":81,"col":23},"end_pos":{"line":81,"col":30}},"use":{"file_name":"Inference.fst","start_pos":{"line":20,"col":14},"end_pos":{"line":20,"col":15}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let alloc_fails`","While typechecking the top-level declaration `[@@expect_failure] let alloc_fails`"]}
 >>]