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 2 commits
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
8 changes: 8 additions & 0 deletions src/as_values/value.ml
Original file line number Diff line number Diff line change
Expand Up @@ -384,6 +384,14 @@ let rec compare x1 x2 =
if x1 == x2 then 0 else
match x1, x2 with
| Int n1, Int n2 -> Int.compare n1 n2
| Int8 n1, Int8 n2 -> Int_8.compare n1 n2
| Int16 n1, Int16 n2 -> Int_16.compare n1 n2
| Int32 n1, Int32 n2 -> Int_32.compare n1 n2
| Int64 n1, Int64 n2 -> Int_64.compare n1 n2
| Nat8 n1, Nat8 n2 -> Nat8.compare n1 n2
| Nat16 n1, Nat16 n2 -> Nat16.compare n1 n2
| Nat32 n1, Nat32 n2 -> Nat32.compare n1 n2
| Nat64 n1, Nat64 n2 -> Nat64.compare n1 n2
| Opt v1, Opt v2 -> compare v1 v2
| Tup vs1, Tup vs2 -> Lib.List.compare compare vs1 vs2
| Array a1, Array a2 -> Lib.Array.compare compare a1 a2
Expand Down
16 changes: 5 additions & 11 deletions src/codegen/compile.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1149,7 +1149,7 @@ end (* Closure *)


module BoxedWord = struct
(* We store large nats and ints in immutable boxed 64bit heap objects.
(* We store large word64s, nat64s and int64s in immutable boxed 64bit heap objects.
ggreif marked this conversation as resolved.
Show resolved Hide resolved

Small values (just <2^5 for now, so that both code paths are well-tested)
are stored unboxed, tagged, see BitTagged.
Expand All @@ -1160,11 +1160,6 @@ module BoxedWord = struct
│ tag │ i64 │
└─────┴─────┴─────┘

Note, that due to the equivalence of in-memory and on-stack
representations, the 64-bit word type is also represented in this
way. As we get proper bigints, the memory representations should
be disambiguated and stack representations adapted. (Renaming
those will point out where the backend needs adjustments.)
*)

let payload_field = Tagged.header_size
Expand Down Expand Up @@ -1289,7 +1284,7 @@ module UnboxedSmallWord = struct
| Type.(Int16|Nat16|Word16) -> 16
| _ -> 32

let shift_of_type ty = Int32.of_int (32 - (bits_of_type ty))
let shift_of_type ty = Int32.of_int (32 - bits_of_type ty)

let bitwidth_mask_of_type = function
| Type.Word8 -> 0b111l
Expand Down Expand Up @@ -4377,7 +4372,7 @@ let compile_lit env lit =
(* Booleans are directly in Vanilla representation *)
| BoolLit false -> SR.bool, Bool.lit false
| BoolLit true -> SR.bool, Bool.lit true
(* This maps int to int32, instead of a proper arbitrary precision library *)
(* This maps int to a proper arbitrary precision library *)
ggreif marked this conversation as resolved.
Show resolved Hide resolved
| IntLit n
| NatLit n -> SR.Vanilla, BigNum.compile_lit env n
| Word8Lit n -> SR.Vanilla, compile_unboxed_const (Value.Word8.to_bits n)
Expand Down Expand Up @@ -4561,7 +4556,7 @@ let rec compile_binop env t op =
| _ -> todo_trap env "compile_binop" (Arrange_ops.binop op)
)

let compile_eq env t = match t with
let compile_eq env = function
| Type.(Prim Text) -> Text.compare env
| Type.(Prim Bool) -> G.i (Compare (Wasm.Values.I32 I32Op.Eq))
| Type.(Prim (Nat | Int)) -> BigNum.compile_eq env
Expand Down Expand Up @@ -5133,8 +5128,7 @@ and compile_lit_pat env l =
| BoolLit true ->
G.nop
| BoolLit false ->
Bool.lit false ^^
G.i (Compare (Wasm.Values.I32 I32Op.Eq))
G.i (Test (Wasm.Values.I32 I32Op.Eqz))
nomeata marked this conversation as resolved.
Show resolved Hide resolved
| (NatLit _ | IntLit _) ->
compile_lit_as env SR.Vanilla l ^^
BigNum.compile_eq env
Expand Down