Skip to content

Commit

Permalink
Add tests for modules and scattered functions/unions
Browse files Browse the repository at this point in the history
  • Loading branch information
Alasdair committed Dec 19, 2023
1 parent b853a09 commit c8412b1
Show file tree
Hide file tree
Showing 14 changed files with 220 additions and 0 deletions.
9 changes: 9 additions & 0 deletions test/typecheck/fail/private_scattered_enum.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
Type error:
fail/private_scattered_enum.sail:15.12-13:
15 |enum clause E = B
 | ^
 | Enumeration E is not in scope
 |
 | fail/private_scattered_enum.sail:7.23-24:
 | 7 |private scattered enum E
 |  | ^ private definition here in A
17 changes: 17 additions & 0 deletions test/typecheck/fail/private_scattered_enum.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
$option -dmagic_hash

$project# A {} B { requires A }

$start_module# A

private scattered enum E

enum clause E = A

$end_module#

$start_module# B

enum clause E = B

$end_module#
9 changes: 9 additions & 0 deletions test/typecheck/fail/private_scattered_fn.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
Type error:
fail/private_scattered_fn.sail:17.16-17:
17 |function clause f _ = 0
 | ^
 | Cannot use private definition
 |
 | fail/private_scattered_fn.sail:7.12-13:
 | 7 |private val f : int -> int
 |  | ^ private definition here in A
19 changes: 19 additions & 0 deletions test/typecheck/fail/private_scattered_fn.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
$option -dmagic_hash

$project# A {} B { requires A }

$start_module# A

private val f : int -> int

scattered function f

function clause f 2 = 3

$end_module#

$start_module# B

function clause f _ = 0

$end_module#
9 changes: 9 additions & 0 deletions test/typecheck/fail/private_scattered_map.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
Type error:
fail/private_scattered_map.sail:17.15-16:
17 |mapping clause m = 1 <-> "1"
 | ^
 | Cannot use private definition
 |
 | fail/private_scattered_map.sail:7.12-13:
 | 7 |private val m : int <-> string
 |  | ^ private definition here in A
19 changes: 19 additions & 0 deletions test/typecheck/fail/private_scattered_map.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
$option -dmagic_hash

$project# A {} B { requires A }

$start_module# A

private val m : int <-> string

scattered mapping m

mapping clause m = 0 <-> "0"

$end_module#

$start_module# B

mapping clause m = 1 <-> "1"

$end_module#
9 changes: 9 additions & 0 deletions test/typecheck/fail/private_scattered_union.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
Type error:
fail/private_scattered_union.sail:15.13-14:
15 |union clause U = B : unit
 | ^
 | Cannot use private definition
 |
 | fail/private_scattered_union.sail:7.24-25:
 | 7 |private scattered union U
 |  | ^ private definition here in A
17 changes: 17 additions & 0 deletions test/typecheck/fail/private_scattered_union.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
$option -dmagic_hash

$project# A {} B { requires A }

$start_module# A

private scattered union U

union clause U = A : unit

$end_module#

$start_module# B

union clause U = B : unit

$end_module#
13 changes: 13 additions & 0 deletions test/typecheck/fail/scattered_function_mod.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
Type error:
fail/scattered_function_mod.sail:23.16-17:
23 |function clause f _ = 0
 | ^
 | Not in scope
 |
 | Try requiring module A to bring the following into scope for module C:
 | fail/scattered_function_mod.sail:7.4-5:
 | 7 |val f : int -> int
 |  | ^ definition here in A
 | fail/scattered_function_mod.sail:3.32-33:
 | 3 |$project# A {} B { requires A } C { requires B }
 |  | ^ add 'requires A' within C here
25 changes: 25 additions & 0 deletions test/typecheck/fail/scattered_function_mod.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
$option -dmagic_hash

$project# A {} B { requires A } C { requires B }

$start_module# A

val f : int -> int

scattered function f

function clause f 1 = 2

$end_module#

$start_module# B

function clause f 2 = 3

$end_module#

$start_module# C

function clause f _ = 0

$end_module#
13 changes: 13 additions & 0 deletions test/typecheck/fail/scattered_map_mod.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
Type error:
fail/scattered_map_mod.sail:23.15-16:
23 |mapping clause m = 2 <-> "2"
 | ^
 | Not in scope
 |
 | Try requiring module A to bring the following into scope for module C:
 | fail/scattered_map_mod.sail:7.4-5:
 | 7 |val m : int <-> string
 |  | ^ definition here in A
 | fail/scattered_map_mod.sail:3.32-33:
 | 3 |$project# A {} B { requires A } C { requires B }
 |  | ^ add 'requires A' within C here
25 changes: 25 additions & 0 deletions test/typecheck/fail/scattered_map_mod.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
$option -dmagic_hash

$project# A {} B { requires A } C { requires B }

$start_module# A

val m : int <-> string

scattered mapping m

mapping clause m = 0 <-> "0"

$end_module#

$start_module# B

mapping clause m = 1 <-> "1"

$end_module#

$start_module# C

mapping clause m = 2 <-> "2"

$end_module#
13 changes: 13 additions & 0 deletions test/typecheck/fail/scattered_union_mod.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
Type error:
fail/scattered_union_mod.sail:21.13-14:
21 |union clause U = U3 : string
 | ^
 | Not in scope
 |
 | Try requiring module A to bring the following into scope for module C:
 | fail/scattered_union_mod.sail:7.16-17:
 | 7 |scattered union U
 |  | ^ definition here in A
 | fail/scattered_union_mod.sail:3.32-33:
 | 3 |$project# A {} B { requires A } C { requires B }
 |  | ^ add 'requires A' within C here
23 changes: 23 additions & 0 deletions test/typecheck/fail/scattered_union_mod.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
$option -dmagic_hash

$project# A {} B { requires A } C { requires B }

$start_module# A

scattered union U

union clause U = U1 : unit

$end_module#

$start_module# B

union clause U = U2 : int

$end_module#

$start_module# C

union clause U = U3 : string

$end_module#

0 comments on commit c8412b1

Please sign in to comment.