diff options
| author | Aseem Rastogi <aseemr@microsoft.com> | 2020-01-22 05:50:12 (GMT) |
|---|---|---|
| committer | Aseem Rastogi <aseemr@microsoft.com> | 2020-01-22 05:50:12 (GMT) |
| commit | 2b19dfd4becac44fca7d10a8a024f16ab7847662 (patch) | |
| tree | c128838f018d73ed726d8ff15c65d2a962fd126a | |
| parent | 115db27aacf84ac59986ad8d345a527c55a643ef (diff) | |
| download | FStar-2b19dfd4becac44fca7d10a8a024f16ab7847662.zip FStar-2b19dfd4becac44fca7d10a8a024f16ab7847662.tar.gz FStar-2b19dfd4becac44fca7d10a8a024f16ab7847662.tar.bz2 | |
adding a testcase
| -rw-r--r-- | examples/layeredeffects/RST.fst | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/examples/layeredeffects/RST.fst b/examples/layeredeffects/RST.fst index ec7dc8a..9a98181 100644 --- a/examples/layeredeffects/RST.fst +++ b/examples/layeredeffects/RST.fst @@ -103,3 +103,24 @@ let test () : RSTATE array emp array_resource = let ptr = alloc () in return ptr + + +(* + * Following example showcases a bug in checking match terms for layered effects + * + * When typechecking the pattern `C a x`, we generate a term with projectors and discriminators + * for each of the pattern bvs, a and x in this case, and those terms are then lax checked + * Crucially when lax checking pat_bv_tm for `x`, `a` must be in the environement, + * earlier it wasn't + *) + +noeq +type m : Type -> Type = +| C : a:Type -> x:a -> m a + + +assume val rst_unit (_:unit) : RSTATE unit emp (fun _ -> emp) + +let test_match (a:Type) (f:m a) : RSTATE unit emp (fun _ -> emp) += match f with + | C a x -> rst_unit () |