forked from B-Lang-org/bsc
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge remote-tracking branch 'upstream/main' into genwrap
- Loading branch information
Showing
12 changed files
with
245 additions
and
11 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,25 @@ | ||
| package BuildList where | ||
|
|
||
| import List | ||
|
|
||
| -- A typeclass used to implement a vector construction function which can take | ||
| -- any number of arguments (>0). | ||
| -- The type parameter `a` is the type of the elements in the list. | ||
| -- The type parameter `r` is the return type of the function, which can be a | ||
| -- list (base case) or a function (recursive case) that takes another element | ||
| -- and returns a new function. | ||
| -- The list here is built in reverse for efficiency, and then reversed. | ||
| class BuildList a r | r -> a where | ||
| lst' :: List a -> a -> r | ||
|
|
||
| instance BuildList a (List a) where | ||
| lst' l x = reverse $ x :> l | ||
|
|
||
| instance (BuildList a r) => BuildList a (a -> r) where | ||
| lst' l x y = lst' (x :> l) y | ||
|
|
||
| -- Example usage: | ||
| -- lst 1 2 3 4 5 => 1 :> 2 :> 3 :> 4 :> 5 :> nil | ||
| -- lst False => False :> nil | ||
| lst :: (BuildList a r) => a -> r | ||
| lst x = lst' nil x |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
|
|
||
| # Test functionality | ||
| test_veri_only TestBuildList | ||
|
|
||
| # Test type check error messages | ||
| compile_fail TestBuildListFail.bs | ||
| compare_file TestBuildListFail.bs.bsc-out | ||
|
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,5 @@ | ||
| # for "make clean" to work everywhere | ||
|
|
||
| CONFDIR = $(realpath ../..) | ||
|
|
||
| include $(CONFDIR)/clean.mk |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,42 @@ | ||
| package TestBuildList where | ||
|
|
||
| import List | ||
| import BuildList | ||
|
|
||
| {-# properties sysTestBuildList = { synthesize } #-} | ||
|
|
||
| sysTestBuildList :: Module Empty | ||
| sysTestBuildList = | ||
| module | ||
| let | ||
| v1 :: List Bool | ||
| v1 = lst True False True True | ||
|
|
||
| v2 :: List (UInt 8); | ||
| v2 = lst 7 32 | ||
|
|
||
| v3 :: List Bool | ||
| v3 = lst False True True | ||
|
|
||
| v4 :: List (UInt 4) | ||
| v4 = lst 3 | ||
|
|
||
| done :: Reg Bool <- mkReg False | ||
|
|
||
| rules | ||
| "r": when not done | ||
| ==> action | ||
| $display "v1[0] -> %b" (v1!!0) | ||
| $display "v1[1] -> %b" (v1!!1) | ||
| $display "v1[2] -> %b" (v1!!2) | ||
| $display "v1[3] -> %b" (v1!!3) | ||
| $display "v2[0] -> %d" (v2!!0) | ||
| $display "v2[1] -> %d" (v2!!1) | ||
| $display "v3[0] -> %b" (v3!!0) | ||
| $display "v3[1] -> %b" (v3!!1) | ||
| $display "v3[2] -> %b" (v3!!2) | ||
| $display "v4[0] -> %d" (v4!!0) | ||
| done := True | ||
|
|
||
| "r2": when done | ||
| ==> $finish 0 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,27 @@ | ||
| package TestBuildListFail where | ||
|
|
||
| import List | ||
| import BuildList | ||
|
|
||
| -- Test error messages | ||
|
|
||
| -- Wrong element type, Literal | ||
| fn1 :: Bool | ||
| fn1 = | ||
| let v :: List Bool | ||
| v = lst 0 1 2 | ||
| in v == v | ||
|
|
||
| -- Wrong element type, concrete | ||
| fn2 :: Bool | ||
| fn2 = | ||
| let v :: List Integer | ||
| v = lst True False True | ||
| in v == v | ||
|
|
||
| -- Wrong return type | ||
| fn3 :: Bool | ||
| fn3 = | ||
| let v :: Bit 3 | ||
| v = lst True False True | ||
| in v == v |
24 changes: 24 additions & 0 deletions
24
testsuite/bsc.lib/BuildList/TestBuildListFail.bs.bsc-out.expected
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,24 @@ | ||
| checking package dependencies | ||
| compiling TestBuildListFail.bs | ||
| Error: "TestBuildListFail.bs", line 12, column 13: (T0031) | ||
| The contexts for this expression could not be resolved because there are no | ||
| instances of the form: | ||
| Prelude.Literal Prelude.Bool | ||
| The context was implied by expressions at the following positions: | ||
| "TestBuildListFail.bs", line 12, column 17 | ||
| Error: "TestBuildListFail.bs", line 18, column 8: (T0032) | ||
| This expression requires the following context which could not be resolved: | ||
| BuildList.BuildList Prelude.Bool (Prelude.Bool -> Prelude.Bool -> Prelude.List Prelude.Integer) | ||
| The context was implied by expressions at the following positions: | ||
| "TestBuildListFail.bs", line 19, column 13 | ||
| An instance for this context exists, but it depends on the following context | ||
| for which there is no instance: | ||
| BuildList.BuildList Prelude.Bool (Prelude.List Prelude.Integer) | ||
| Error: "TestBuildListFail.bs", line 25, column 8: (T0032) | ||
| This expression requires the following context which could not be resolved: | ||
| BuildList.BuildList Prelude.Bool (Prelude.Bool -> Prelude.Bool -> Prelude.Bit 3) | ||
| The context was implied by expressions at the following positions: | ||
| "TestBuildListFail.bs", line 26, column 13 | ||
| An instance for this context exists, but it depends on the following context | ||
| for which there is no instance: | ||
| BuildList.BuildList Prelude.Bool (Prelude.Bit 3) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,10 @@ | ||
| v1[0] -> 1 | ||
| v1[1] -> 0 | ||
| v1[2] -> 1 | ||
| v1[3] -> 1 | ||
| v2[0] -> 7 | ||
| v2[1] -> 32 | ||
| v3[0] -> 0 | ||
| v3[1] -> 1 | ||
| v3[2] -> 1 | ||
| v4[0] -> 3 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters