Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support for negative literals in patterns #2976

Merged
merged 1 commit into from
Jun 26, 2023
Merged

Support for negative literals in patterns #2976

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions ocaml/fstar-lib/FStar_Parser_Parse.mly
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -621,6 +621,18 @@ atomicPattern:
{ mk_pattern (PatWild (Some Implicit, [])) (rr $loc) }
| c=constant
{ mk_pattern (PatConst c) (rr $loc(c)) }
| tok=MINUS c=constant
{ let r = rr2 $loc(tok) $loc(c) in
let c =
match c with
| Const_int (s, swopt) ->
(match swopt with
| None
| Some (Signed, _) -> Const_int ("-" ^ s, swopt)
| _ -> raise_error (Fatal_SyntaxError, "Syntax_error: negative integer constant with unsigned width") r)
| _ -> raise_error (Fatal_SyntaxError, "Syntax_error: negative constant that is not an integer") r
in
mk_pattern (PatConst c) r }
| BACKTICK_PERC q=atomicTerm
{ mk_pattern (PatVQuote q) (rr $loc) }
| qual_id=aqualifiedWithAttrs(lident)
Expand Down
32 changes: 32 additions & 0 deletions tests/bug-reports/Bug2415.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
module Bug2415

let sign = (z:int{z = 0 \/ z = (-1) \/ z = 1})

let example_1 (s:sign) : string =
match s with
| -1 -> "negative"
| 1 -> "positive"
| 0 -> "zero"
| -2 -> assert False; ""

open FStar.Int32
open FStar.Int8
open FStar.UInt32
open FStar.UInt8

type i8 = FStar.Int8.t
type i32 = FStar.Int32.t
type u8 = FStar.UInt8.t
type u32 = FStar.UInt32.t

let test1 (n:i32) =
match n with
| -1l -> assert (Int32.v n == -1)
| 1l -> assert (Int32.v n == 1)
| _ -> ()

[@@ expect_failure [114]] // type of pattern (Int32.t) does not match the type of scrutinee (Int8.t)
let test2 (n:i8) =
match n with
| -0l -> ()
| _ -> ()
3 changes: 2 additions & 1 deletion tests/bug-reports/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,8 @@ SHOULD_VERIFY_CLOSED=Bug022.fst Bug024.fst Bug025.fst Bug026.fst Bug026b.fst Bug
Bug2635.fst Bug2637.fst Bug2641.fst Bug1486.fst PropProofs.fst \
Bug2684a.fst Bug2684b.fst Bug2684c.fst Bug2684d.fst Bug2659b.fst\
Bug2756.fst MutualRecPositivity.fst Bug2806a.fst Bug2806b.fst Bug2806c.fst Bug2806d.fst Bug2809.fst\
Bug2849a.fst Bug2849b.fst Bug2045.fst Bug2876.fst Bug2882.fst Bug2895.fst Bug2894.fst
Bug2849a.fst Bug2849b.fst Bug2045.fst Bug2876.fst Bug2882.fst Bug2895.fst Bug2894.fst \
Bug2415.fst

SHOULD_VERIFY_INTERFACE_CLOSED=Bug771.fsti Bug771b.fsti
SHOULD_VERIFY_AND_WARN_CLOSED=Bug016.fst
Expand Down