diff --git a/lib/pulse/lib/Pulse.Lib.HashTable.fst b/lib/pulse/lib/Pulse.Lib.HashTable.fst index 6bcd0cddc..ac9b27946 100644 --- a/lib/pulse/lib/Pulse.Lib.HashTable.fst +++ b/lib/pulse/lib/Pulse.Lib.HashTable.fst @@ -45,10 +45,15 @@ let models_timeless #kt #vt (ht:ht_t kt vt) (pht:pht_t kt vt) : Lemma (timeless (models ht pht)) [SMTPat (timeless (models ht pht))] = () +(* NOTE: We do not add the Rust attributes in these definitions since + 1- They anyway be ignored by Pulse (currently, should fix) + 2- The ones that really matter are the ones in the declarations + in the fsti (which currently are, and must be, F* vals). +*) fn alloc - (#[@@@ Rust_generics_bounds ["Copy"; "PartialEq"; "Clone"]] k:eqtype) - (#[@@@ Rust_generics_bounds ["Clone"]] v:Type0) + (#k:eqtype) + (#v:Type0) (hashf:(k -> SZ.t)) (l:pos_us) requires pure (SZ.fits (2 `op_Multiply` SZ.v l)) returns ht:ht_t k v @@ -63,11 +68,9 @@ fn alloc ht } - - fn dealloc - (#[@@@ Rust_generics_bounds ["Copy"; "PartialEq"; "Clone"]] k:eqtype) - (#[@@@ Rust_generics_bounds ["Clone"]] v:Type0) + (#k:eqtype) + (#v:Type0) (ht:ht_t k v) requires exists* pht. models ht pht ensures emp @@ -85,8 +88,8 @@ let size_t_mod (x:SZ.t) (y : SZ.t { y =!= 0sz }) #push-options "--fuel 1 --ifuel 1" fn lookup - (#[@@@ Rust_generics_bounds ["Copy"; "PartialEq"; "Clone"]] kt:eqtype) - (#[@@@ Rust_generics_bounds ["Clone"]] vt:Type0) + (#kt:eqtype) + (#vt:Type0) (#pht:erased (pht_t kt vt)) (ht:ht_t kt vt) (k:kt) @@ -200,8 +203,8 @@ fn lookup fn replace - (#[@@@ Rust_generics_bounds ["Copy"; "PartialEq"; "Clone"]] kt:eqtype) - (#[@@@ Rust_generics_bounds ["Clone"]] vt:Type0) + (#kt:eqtype) + (#vt:Type0) (#pht:erased (pht_t kt vt)) (ht:ht_t kt vt) (idx:SZ.t) @@ -244,8 +247,8 @@ fn replace #push-options "--fuel 1 --ifuel 2 --z3rlimit_factor 4" fn insert - (#[@@@ Rust_generics_bounds ["Copy"; "PartialEq"; "Clone"]] kt:eqtype) - (#[@@@ Rust_generics_bounds ["Clone"]] vt:Type0) + (#kt:eqtype) + (#vt:Type0) (ht:ht_t kt vt) (k:kt) (v:vt) (#pht:(p:erased (pht_t kt vt){PHT.not_full p.repr})) requires models ht pht @@ -424,8 +427,8 @@ let is_used fn not_full - (#[@@@ Rust_generics_bounds ["Copy"; "PartialEq"; "Clone"]] kt:eqtype) - (#[@@@ Rust_generics_bounds ["Clone"]] vt:Type0) + (#kt:eqtype) + (#vt:Type0) (ht:ht_t kt vt) (#pht:erased (pht_t kt vt)) @@ -492,8 +495,8 @@ fn not_full fn insert_if_not_full - (#[@@@ Rust_generics_bounds ["Copy"; "PartialEq"; "Clone"]] kt:eqtype) - (#[@@@ Rust_generics_bounds ["Clone"]] vt:Type0) + (#kt:eqtype) + (#vt:Type0) (ht:ht_t kt vt) (k:kt) (v:vt) (#pht:erased (PHT.pht_t kt vt)) requires models ht pht @@ -522,8 +525,8 @@ fn insert_if_not_full #push-options "--z3rlimit_factor 4" fn delete - (#[@@@ Rust_generics_bounds ["Copy"; "PartialEq"; "Clone"]] kt:eqtype) - (#[@@@ Rust_generics_bounds ["Clone"]] vt:Type0) + (#kt:eqtype) + (#vt:Type0) (ht:ht_t kt vt) (k:kt) (#pht:erased (pht_t kt vt)) diff --git a/src/syntax_extension/PulseSyntaxExtension.Desugar.fst b/src/syntax_extension/PulseSyntaxExtension.Desugar.fst index ee1737b90..9eb4787fd 100644 --- a/src/syntax_extension/PulseSyntaxExtension.Desugar.fst +++ b/src/syntax_extension/PulseSyntaxExtension.Desugar.fst @@ -893,6 +893,16 @@ and desugar_binders (env:env_t) (bs:Sugar.binders) let rng = b.A.brange in let (aq, b, t, attrs) = destruct_binder b in let! t = desugar_term env t in + if Cons? attrs && not (Options.Ext.enabled "pulse:binder_attrs") then ( + let open FStarC.Errors.Msg in + (* Using "Unused01" error code is a huge hack, but we don't + have a way of extending error codes. *) + fail_doc [ + text "NOTE: Pulse does not properly support binder attributes. \ + They will be ignored by later stages."; + text "This error can be ignored (at your own risk) by passing --ext pulse:binder_attrs." + ] (List.hd attrs).range + ) else return ();! let! attrs = mapM (desugar_term env) attrs in let env, bv = push_bv env b in let! env, bs, bvs = aux env bs in diff --git a/src/syntax_extension/PulseSyntaxExtension.Err.fst b/src/syntax_extension/PulseSyntaxExtension.Err.fst index 3ba03516d..274d611eb 100644 --- a/src/syntax_extension/PulseSyntaxExtension.Err.fst +++ b/src/syntax_extension/PulseSyntaxExtension.Err.fst @@ -49,8 +49,11 @@ instance err_monad : monad err = { ( let! ) = bind_err } +let fail_doc #a (message:list Pprint.document) (range:R.range) : err a = + fun ctr -> Inr (Some (message, range)), ctr + let fail #a (message:string) (range:R.range) : err a = - fun ctr -> Inr (Some (FStarC.Errors.mkmsg message, range)), ctr + fail_doc (FStarC.Errors.mkmsg message) range let fail_if (b:bool) (message:string) (range:R.range) : err unit = if b then fail message range else return () diff --git a/test/BinderAttrs.fst b/test/BinderAttrs.fst index 374c31514..364ca30a1 100644 --- a/test/BinderAttrs.fst +++ b/test/BinderAttrs.fst @@ -8,6 +8,9 @@ assume val f1 ([@@@123] x:int) : stt int emp (fun _ -> emp) +(* Binder attrs currently rejected altogether. Ignore that. *) +#set-options "--ext pulse:binder_attrs" + fn f2 ([@@@123] x:int) requires emp returns int diff --git a/test/nolib/BinderAttrs.fst b/test/nolib/BinderAttrs.fst new file mode 100644 index 000000000..374c31514 --- /dev/null +++ b/test/nolib/BinderAttrs.fst @@ -0,0 +1,36 @@ +module BinderAttrs + +#lang-pulse +open Pulse.Nolib +open FStar.Tactics.V2 + +assume +val f1 ([@@@123] x:int) : + stt int emp (fun _ -> emp) + +fn f2 ([@@@123] x:int) + requires emp + returns int + ensures emp +{ 1 } + +(* f1 and f2 should both have the same binder attributes. *) + +let typ_of (nm : string) : Tac typ = + let tm = pack (Tv_FVar (pack_fv (explode_qn nm))) in + tc (cur_env ()) tm + +let check (t : typ) : Tac unit = + match t with + | Tv_Arrow b _c -> ( + match b.attrs with + | [] -> fail "no attrs" + | _ -> () + ) + | _ -> + fail "not an arrow" + +let _ = assert True by check (typ_of (`%f1)) + +[@@expect_failure] (* should work, Pulse currently dropping binder attrs *) +let _ = assert True by check (typ_of (`%f2))