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.

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

AST-89 Range restricted Nat* and Int* #487

Merged
merged 70 commits into from
Jun 18, 2019
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
70 commits
Select commit Hold shift + click to select a range
9609c1e
add finite-bitwidth integral primitive types
ggreif Jun 4, 2019
ad41b0b
WIP: compiles
ggreif Jun 5, 2019
4637882
WIP: more progress
ggreif Jun 5, 2019
a9fb7a3
WIP: first round of backed changes
ggreif Jun 6, 2019
1a42bce
More conversions
ggreif Jun 6, 2019
b710aa4
WIP: added WordN->NatN/IntN
ggreif Jun 6, 2019
e0e3dcf
refactor tests
ggreif Jun 6, 2019
1e59f40
implement and test Nat->Nat32 and Int->Int32
ggreif Jun 6, 2019
324e416
implement Nat->Nat* and Int->Int*
ggreif Jun 7, 2019
8c0fec8
fix Word32->Nat32
ggreif Jun 7, 2019
4ba1823
soup up roundtrip tests
ggreif Jun 7, 2019
77c4693
fix roundtrip bug
ggreif Jun 7, 2019
6dbc868
serialisation support
ggreif Jun 8, 2019
bdc2d91
compile literals
ggreif Jun 9, 2019
34f8a8e
New primitive types for emacs mode (AST-89)
ggreif Jun 9, 2019
656e268
fix conversions (i.e. boxing)
ggreif Jun 9, 2019
e83eca6
test Int/Nat16/32 serialisation
ggreif Jun 9, 2019
e8a5240
trap for outrange Nat->Nat8/16/32
ggreif Jun 10, 2019
664c798
range check for Int->Int8/16/32
ggreif Jun 10, 2019
18dd7a9
cope with libTomMath flaw for now
ggreif Jun 10, 2019
e8ebf62
range check for ->Nat64
ggreif Jun 11, 2019
76dc485
resolved
ggreif Jun 11, 2019
15f798b
range check for ->Int64
ggreif Jun 11, 2019
53652f2
factor out special_unop_typing
ggreif Jun 11, 2019
921a8ac
extend special_unop_typing to other Nat* types too
ggreif Jun 11, 2019
93c4f20
Merge remote-tracking branch 'origin/master' into gabor/ranged-int-nat
ggreif Jun 12, 2019
e324f85
fix func import oversight
ggreif Jun 12, 2019
74be50d
update ok files
ggreif Jun 12, 2019
2b53e98
intro of/to_big_int method for NumType
ggreif Jun 12, 2019
b662da3
WIP: more intermediate string elimination
ggreif Jun 12, 2019
84b63c4
fix Nat64->Word64
ggreif Jun 12, 2019
250c033
test literal max Nat64
ggreif Jun 12, 2019
34d731f
fix max Nat64Lit in backend
ggreif Jun 12, 2019
4245894
add @tex_of functions for ranged numeric types
ggreif Jun 13, 2019
7ab1dd3
fix data-params.as
ggreif Jun 13, 2019
e46e42c
implement debug show for range-limited numeric types
ggreif Jun 13, 2019
8fdd687
update output
ggreif Jun 13, 2019
bb2c388
remove-duplicate
ggreif Jun 13, 2019
ad78ca5
convert exceptions to traps
ggreif Jun 13, 2019
5a8de71
obsolete test
ggreif Jun 13, 2019
1d19805
Merge remote-tracking branch 'origin/master' into gabor/ranged-int-nat
ggreif Jun 13, 2019
a55e103
port portions of e46e42c4f from src/ir_passes/show.ml
ggreif Jun 13, 2019
9ba1105
simplify
ggreif Jun 13, 2019
bafbef2
Merge remote-tracking branch 'origin/master' into gabor/ranged-int-nat
ggreif Jun 13, 2019
b37c85a
bad merge
ggreif Jun 13, 2019
fd4a921
negation for Int*/Nat*
ggreif Jun 13, 2019
5ba6157
refactor relops a bit
ggreif Jun 13, 2019
f57de0f
relops for Int* in interpreter
ggreif Jun 13, 2019
3222223
codegen comparisons
ggreif Jun 14, 2019
1bcf9e3
trapping negation for Int* and comparisons for Nat*/Int*
ggreif Jun 14, 2019
449e99b
resolve TODO
ggreif Jun 14, 2019
704e0c2
test negation corner case
ggreif Jun 14, 2019
6c5ee4a
fix compile warnings
ggreif Jun 14, 2019
2db2fc7
Merge branch 'master' into gabor/ranged-int-nat
ggreif Jun 15, 2019
48e11ee
lower-case
ggreif Jun 16, 2019
bc0ed24
add Nat8 negation test
ggreif Jun 16, 2019
5963583
refactor to share code
ggreif Jun 16, 2019
b4caf31
commit @nomeata's fix for fits_signed_bits
ggreif Jun 17, 2019
a5afc38
revert the ability to negate Nat{8,16,32,64} and get an Int{8,16,32,64}
ggreif Jun 17, 2019
ce7b7a7
tweaks
ggreif Jun 17, 2019
032a91e
handle a few review comments
ggreif Jun 17, 2019
129ca99
more review feedback
ggreif Jun 17, 2019
bbbda66
more review feedback
ggreif Jun 17, 2019
f5d8987
implement ordering relation(s)
ggreif Jun 18, 2019
1ded795
minor tweaks, doc fixes and codegen optimisations
ggreif Jun 18, 2019
de4e053
fix build
ggreif Jun 18, 2019
eafa524
pattern matching {Word,Int,Nat}x{8,16,32,64}
ggreif Jun 18, 2019
789f1f9
rename BoxedWord64
ggreif Jun 18, 2019
2fe00c8
remove FIXMEs
ggreif Jun 18, 2019
8f45485
factor out the type-dependent creation of UnboxedSmallWord literals
ggreif Jun 18, 2019
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
42 changes: 42 additions & 0 deletions src/codegen/compile.ml
Original file line number Diff line number Diff line change
Expand Up @@ -5132,6 +5132,48 @@ and compile_lit_pat env l =
| (NatLit _ | IntLit _) ->
compile_lit_as env SR.Vanilla l ^^
BigNum.compile_eq env
| Nat8Lit _ ->
snd (compile_lit env l) ^^
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I see no point spelling out the SR for compile_lit_as all the time, instead I rely on what is done by both lines below implicitly. Also there is no guarantee that the latter operates on Vanilla (other than inspecting the implementation).

compile_eq env Type.(Prim Nat8)
| Nat16Lit _ ->
snd (compile_lit env l) ^^
compile_eq env Type.(Prim Nat16)
| Nat32Lit _ ->
BoxedSmallWord.unbox env ^^
snd (compile_lit env l) ^^
compile_eq env Type.(Prim Nat32)
| Nat64Lit _ ->
BoxedWord.unbox env ^^
snd (compile_lit env l) ^^
compile_eq env Type.(Prim Nat64)
| Int8Lit _ ->
snd (compile_lit env l) ^^
compile_eq env Type.(Prim Int8)
| Int16Lit _ ->
snd (compile_lit env l) ^^
compile_eq env Type.(Prim Int16)
| Int32Lit _ ->
BoxedSmallWord.unbox env ^^
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since the scrutinee is captured as SR.Vanilla we need to unbox it for *32 and *64 prim types.

snd (compile_lit env l) ^^
compile_eq env Type.(Prim Int32)
| Int64Lit _ ->
BoxedWord.unbox env ^^
snd (compile_lit env l) ^^
compile_eq env Type.(Prim Int64)
| Word8Lit _ ->
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Words were an earlier omission, filled in now.

snd (compile_lit env l) ^^
compile_eq env Type.(Prim Word8)
| Word16Lit _ ->
snd (compile_lit env l) ^^
compile_eq env Type.(Prim Word16)
| Word32Lit _ ->
BoxedSmallWord.unbox env ^^
snd (compile_lit env l) ^^
compile_eq env Type.(Prim Word32)
| Word64Lit _ ->
BoxedWord.unbox env ^^
snd (compile_lit env l) ^^
compile_eq env Type.(Prim Word64)
| (TextLit t) ->
Text.lit env t ^^
Text.compare env
Expand Down
4 changes: 4 additions & 0 deletions src/lowering/desugar.ml
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,10 @@ let apply_sign op l = Syntax.(match op, l with
| PosOp, l -> l
| NegOp, NatLit n -> NatLit (Value.Nat.sub Value.Nat.zero n)
| NegOp, IntLit n -> IntLit (Value.Int.sub Value.Int.zero n)
| NegOp, Int8Lit n -> Int8Lit (Value.Int_8.sub Value.Int_8.zero n)
| NegOp, Int16Lit n -> Int16Lit (Value.Int_16.sub Value.Int_16.zero n)
| NegOp, Int32Lit n -> Int32Lit (Value.Int_32.sub Value.Int_32.zero n)
| NegOp, Int64Lit n -> Int64Lit (Value.Int_64.sub Value.Int_64.zero n)
| _, _ -> raise (Invalid_argument "Invalid signed pattern")
)

Expand Down
29 changes: 29 additions & 0 deletions test/run/ranged-nums.as
Original file line number Diff line number Diff line change
Expand Up @@ -16,3 +16,32 @@ let _ = -127 : Int8;
let _ = -32767 : Int16;
let _ = -2_147_483_647 : Int32;
let _ = -9_223_372_036_854_775_807 : Int64;

// test patterns

func n8 (n : Nat8) = assert (switch n { case 0 false; case 1 false; case 42 true; case _ false });
func n16 (n : Nat16) = assert (switch n { case 0 false; case 1 false; case 65000 true; case _ false });
func n32 (n : Nat32) = assert (switch n { case 0 false; case 1 false; case 4_294_967_295 true; case _ false });
func n64 (n : Nat64) = assert (switch n { case 0 false; case 1 false; case 42 true; case _ false });


n8 42;
n16 65000;
n32 4_294_967_295;
n64 42;


func i8 (n : Int8) = assert (switch n { case 0 false; case (-42) true; case 1 false; case 42 true; case _ false });
func i16 (n : Int16) = assert (switch n { case 0 false; case (-32000) true; case 1 false; case 32000 true; case _ false });
func i32 (n : Int32) = assert (switch n { case 0 false; case (-20000000) true; case 1 false; case 1_294_967_295 true; case _ false });
func i64 (n : Int64) = assert (switch n { case 0 false; case (-420000000000) true; case 1 false; case 42 true; case _ false });


i8 42;
i8 (-42);
i16 32000;
i16 (-32000);
i32 1_294_967_295;
i32 (-20000000);
i64 (-420000000000);
i64 42;
14 changes: 14 additions & 0 deletions test/run/words.as
Original file line number Diff line number Diff line change
Expand Up @@ -276,3 +276,17 @@ func checkpointJuliett() {};
assert (3 : Word8 ** (4 : Word8) == (81 : Word8));
assert (3 : Word8 ** (5 : Word8) == (243 : Word8));
};


// check whether patterns work

func w8 (n : Word8) = assert (switch n { case 0 false; case 1 false; case 42 true; case _ false });
func w16 (n : Word16) = assert (switch n { case 0 false; case 1 false; case 65000 true; case _ false });
func w32 (n : Word32) = assert (switch n { case 0 false; case 1 false; case 4_294_967_295 true; case _ false });
func w64 (n : Word64) = assert (switch n { case 0 false; case 1 false; case 42 true; case _ false });


w8 42;
w16 65000;
w32 4_294_967_295;
w64 42;