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 61 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 emacs/actorscript-mode.el
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,14 @@
"Bool"
"Nat"
"Int"
"Int8"
"Int16"
"Int32"
"Int64"
"Nat8"
"Nat16"
"Nat32"
"Nat64"
"Word8"
"Word16"
"Word32"
Expand Down
8 changes: 8 additions & 0 deletions src/as_frontend/arrange.ml
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,15 @@ and lit (l:lit) = match l with
| BoolLit true -> "BoolLit" $$ [ Atom "true" ]
| BoolLit false -> "BoolLit" $$ [ Atom "false" ]
| NatLit n -> "NatLit" $$ [ Atom (Value.Nat.to_pretty_string n) ]
| Nat8Lit n -> "Nat8Lit" $$ [ Atom (Value.Nat8.to_pretty_string n) ]
| Nat16Lit n -> "Nat16Lit" $$ [ Atom (Value.Nat16.to_pretty_string n) ]
| Nat32Lit n -> "Nat32Lit" $$ [ Atom (Value.Nat32.to_pretty_string n) ]
| Nat64Lit n -> "Nat64Lit" $$ [ Atom (Value.Nat64.to_pretty_string n) ]
| IntLit i -> "IntLit" $$ [ Atom (Value.Int.to_pretty_string i) ]
| Int8Lit i -> "Int8Lit" $$ [ Atom (Value.Int_8.to_pretty_string i) ]
| Int16Lit i -> "Int16Lit" $$ [ Atom (Value.Int_16.to_pretty_string i) ]
| Int32Lit i -> "Int32Lit" $$ [ Atom (Value.Int_32.to_pretty_string i) ]
| Int64Lit i -> "Int64Lit" $$ [ Atom (Value.Int_64.to_pretty_string i) ]
| Word8Lit w -> "Word8Lit" $$ [ Atom (Value.Word8.to_pretty_string w) ]
| Word16Lit w -> "Word16Lit" $$ [ Atom (Value.Word16.to_pretty_string w) ]
| Word32Lit w -> "Word32Lit" $$ [ Atom (Value.Word32.to_pretty_string w) ]
Expand Down
8 changes: 8 additions & 0 deletions src/as_frontend/coverage.ml
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,15 @@ let value_of_lit = function
| NullLit -> V.Null
| BoolLit b -> V.Bool b
| NatLit n -> V.Int n
| Nat8Lit w -> V.Nat8 w
| Nat16Lit w -> V.Nat16 w
| Nat32Lit w -> V.Nat32 w
| Nat64Lit w -> V.Nat64 w
| IntLit i -> V.Int i
| Int8Lit w -> V.Int8 w
| Int16Lit w -> V.Int16 w
| Int32Lit w -> V.Int32 w
| Int64Lit w -> V.Int64 w
| Word8Lit w -> V.Word8 w
| Word16Lit w -> V.Word16 w
| Word32Lit w -> V.Word32 w
Expand Down
16 changes: 16 additions & 0 deletions src/as_frontend/syntax.ml
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,15 @@ type lit =
| NullLit
| BoolLit of bool
| NatLit of Value.Nat.t
| Nat8Lit of Value.Nat8.t
| Nat16Lit of Value.Nat16.t
| Nat32Lit of Value.Nat32.t
| Nat64Lit of Value.Nat64.t
| IntLit of Value.Int.t
| Int8Lit of Value.Int_8.t
| Int16Lit of Value.Int_16.t
| Int32Lit of Value.Int_32.t
| Int64Lit of Value.Int_64.t
| Word8Lit of Value.Word8.t
| Word16Lit of Value.Word16.t
| Word32Lit of Value.Word32.t
Expand Down Expand Up @@ -196,6 +204,14 @@ let string_of_lit = function
| BoolLit true -> "true"
| IntLit n
| NatLit n -> Value.Int.to_pretty_string n
| Int8Lit n -> Value.Int_8.to_pretty_string n
| Int16Lit n -> Value.Int_16.to_pretty_string n
| Int32Lit n -> Value.Int_32.to_pretty_string n
| Int64Lit n -> Value.Int_64.to_pretty_string n
| Nat8Lit n -> Value.Nat8.to_pretty_string n
| Nat16Lit n -> Value.Nat16.to_pretty_string n
| Nat32Lit n -> Value.Nat32.to_pretty_string n
| Nat64Lit n -> Value.Nat64.to_pretty_string n
| Word8Lit n -> Value.Word8.to_pretty_string n
| Word16Lit n -> Value.Word16.to_pretty_string n
| Word32Lit n -> Value.Word32.to_pretty_string n
Expand Down
41 changes: 39 additions & 2 deletions src/as_frontend/typing.ml
Original file line number Diff line number Diff line change
Expand Up @@ -302,7 +302,15 @@ let check_lit_val env t of_string at s =
(T.string_of_typ (T.Prim t))

let check_nat env = check_lit_val env T.Nat Value.Nat.of_string
let check_nat8 env = check_lit_val env T.Nat8 Value.Nat8.of_string
let check_nat16 env = check_lit_val env T.Nat16 Value.Nat16.of_string
let check_nat32 env = check_lit_val env T.Nat32 Value.Nat32.of_string
let check_nat64 env = check_lit_val env T.Nat64 Value.Nat64.of_string
let check_int env = check_lit_val env T.Int Value.Int.of_string
let check_int8 env = check_lit_val env T.Int8 Value.Int_8.of_string
let check_int16 env = check_lit_val env T.Int16 Value.Int_16.of_string
let check_int32 env = check_lit_val env T.Int32 Value.Int_32.of_string
let check_int64 env = check_lit_val env T.Int64 Value.Int_64.of_string
let check_word8 env = check_lit_val env T.Word8 Value.Word8.of_string_u
let check_word16 env = check_lit_val env T.Word16 Value.Word16.of_string_u
let check_word32 env = check_lit_val env T.Word32 Value.Word32.of_string_u
Expand All @@ -315,7 +323,15 @@ let infer_lit env lit at : T.prim =
| NullLit -> T.Null
| BoolLit _ -> T.Bool
| NatLit _ -> T.Nat
| Nat8Lit _ -> T.Nat8
| Nat16Lit _ -> T.Nat16
| Nat32Lit _ -> T.Nat32
| Nat64Lit _ -> T.Nat64
| IntLit _ -> T.Int
| Int8Lit _ -> T.Int8
| Int16Lit _ -> T.Int16
| Int32Lit _ -> T.Int32
| Int64Lit _ -> T.Int64
| Word8Lit _ -> T.Word8
| Word16Lit _ -> T.Word16
| Word32Lit _ -> T.Word32
Expand All @@ -340,8 +356,24 @@ let check_lit env t lit at =
| T.Opt _, NullLit -> ()
| T.Prim T.Nat, PreLit (s, T.Nat) ->
lit := NatLit (check_nat env at s)
| T.Prim T.Nat8, PreLit (s, T.Nat) ->
lit := Nat8Lit (check_nat8 env at s)
| T.Prim T.Nat16, PreLit (s, T.Nat) ->
lit := Nat16Lit (check_nat16 env at s)
| T.Prim T.Nat32, PreLit (s, T.Nat) ->
lit := Nat32Lit (check_nat32 env at s)
| T.Prim T.Nat64, PreLit (s, T.Nat) ->
lit := Nat64Lit (check_nat64 env at s)
| T.Prim T.Int, PreLit (s, (T.Nat | T.Int)) ->
lit := IntLit (check_int env at s)
| T.Prim T.Int8, PreLit (s, (T.Nat | T.Int)) ->
lit := Int8Lit (check_int8 env at s)
| T.Prim T.Int16, PreLit (s, (T.Nat | T.Int)) ->
lit := Int16Lit (check_int16 env at s)
| T.Prim T.Int32, PreLit (s, (T.Nat | T.Int)) ->
lit := Int32Lit (check_int32 env at s)
| T.Prim T.Int64, PreLit (s, (T.Nat | T.Int)) ->
lit := Int64Lit (check_int64 env at s)
| T.Prim T.Word8, PreLit (s, (T.Nat | T.Int)) ->
lit := Word8Lit (check_word8 env at s)
| T.Prim T.Word16, PreLit (s, (T.Nat | T.Int)) ->
Expand Down Expand Up @@ -394,6 +426,11 @@ and infer_exp' f env exp : T.typ =
end;
t'

and special_unop_typing = let open T in
function
| Prim Nat -> Prim Int
| t -> t

and infer_exp'' env exp : T.typ =
match exp.it with
| PrimE _ ->
Expand All @@ -411,7 +448,7 @@ and infer_exp'' env exp : T.typ =
| UnE (ot, op, exp1) ->
let t1 = infer_exp_promote env exp1 in
(* Special case for subtyping *)
let t = if t1 = T.Prim T.Nat then T.Prim T.Int else t1 in
let t = special_unop_typing t1 in
if not env.pre then begin
assert (!ot = Type.Pre);
Copy link
Contributor

Choose a reason for hiding this comment

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

I'd be very tempted to changed the syntax type checker to annotate BinE and UnE with the partially evaluated interpretations of the operators, so we don't have to repeat dispatch every time we call an operator... Whadday think? Again, this would be as a separate PR...

Copy link
Collaborator

Choose a reason for hiding this comment

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

Not sure if I like code-in-the-data here. Would cause problems for pretty-printing, or serialization/deserialization. Also, smells a bit of premature optimization. Show me profiling data before you argue about performance :-)

Copy link
Contributor

@crusso crusso Jun 17, 2019

Choose a reason for hiding this comment

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

@nomeata Not sure I buy that. The pretty printer can ignore it, serializer and deserialized drop and recompute from the type stored in ot. And I really don't think I need a profiler to tell me that doing redundant work (think of interpreted arithmetic in a loop) is a bad idea.

Plus, it would be more true to the intention that operators are resolved statically, not at runtime. Indeed, weren't you arguing for this in the past? But true, none of that should be part of this PR....

if not (Operator.has_unop t op) then
Expand Down Expand Up @@ -858,7 +895,7 @@ and infer_pat' env pat : T.typ * Scope.val_env =
| SignP (op, lit) ->
let t1 = T.Prim (infer_lit env lit pat.at) in
(* Special case for subtyping *)
let t = if t1 = T.Prim T.Nat then T.Prim T.Int else t1 in
let t = special_unop_typing t1 in
if not (Operator.has_unop t op) then
local_error env pat.at "operator is not defined for operand type\n %s"
(T.string_of_typ_expand t);
Expand Down
8 changes: 8 additions & 0 deletions src/as_ir/arrange_ir.ml
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,15 @@ and lit (l:lit) = match l with
| BoolLit true -> "BoolLit" $$ [ Atom "true" ]
| BoolLit false -> "BoolLit" $$ [ Atom "false" ]
| NatLit n -> "NatLit" $$ [ Atom (Value.Nat.to_pretty_string n) ]
| Nat8Lit w -> "Nat8Lit" $$ [ Atom (Value.Nat8.to_pretty_string w) ]
| Nat16Lit w -> "Nat16Lit" $$ [ Atom (Value.Nat16.to_pretty_string w) ]
| Nat32Lit w -> "Nat32Lit" $$ [ Atom (Value.Nat32.to_pretty_string w) ]
| Nat64Lit w -> "Nat64Lit" $$ [ Atom (Value.Nat64.to_pretty_string w) ]
| IntLit i -> "IntLit" $$ [ Atom (Value.Int.to_pretty_string i) ]
| Int8Lit w -> "Int8Lit" $$ [ Atom (Value.Int_8.to_pretty_string w) ]
| Int16Lit w -> "Int16Lit" $$ [ Atom (Value.Int_16.to_pretty_string w) ]
| Int32Lit w -> "Int32Lit" $$ [ Atom (Value.Int_32.to_pretty_string w) ]
| Int64Lit w -> "Int64Lit" $$ [ Atom (Value.Int_64.to_pretty_string w) ]
| Word8Lit w -> "Word8Lit" $$ [ Atom (Value.Word8.to_pretty_string w) ]
| Word16Lit w -> "Word16Lit" $$ [ Atom (Value.Word16.to_pretty_string w) ]
| Word32Lit w -> "Word32Lit" $$ [ Atom (Value.Word32.to_pretty_string w) ]
Expand Down
8 changes: 8 additions & 0 deletions src/as_ir/check_ir.ml
Original file line number Diff line number Diff line change
Expand Up @@ -250,7 +250,15 @@ let type_lit env lit at : T.prim =
| NullLit -> T.Null
| BoolLit _ -> T.Bool
| NatLit _ -> T.Nat
| Nat8Lit _ -> T.Nat8
| Nat16Lit _ -> T.Nat16
| Nat32Lit _ -> T.Nat32
| Nat64Lit _ -> T.Nat64
| IntLit _ -> T.Int
| Int8Lit _ -> T.Int8
| Int16Lit _ -> T.Int16
| Int32Lit _ -> T.Int32
| Int64Lit _ -> T.Int64
| Word8Lit _ -> T.Word8
| Word16Lit _ -> T.Word16
| Word32Lit _ -> T.Word32
Expand Down
16 changes: 16 additions & 0 deletions src/as_ir/ir.ml
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,15 @@ type lit =
| NullLit
| BoolLit of bool
| NatLit of Value.Nat.t
| Nat8Lit of Value.Nat8.t
| Nat16Lit of Value.Nat16.t
| Nat32Lit of Value.Nat32.t
| Nat64Lit of Value.Nat64.t
| IntLit of Value.Int.t
| Int8Lit of Value.Int_8.t
| Int16Lit of Value.Int_16.t
| Int32Lit of Value.Int_32.t
| Int64Lit of Value.Int_64.t
| Word8Lit of Value.Word8.t
| Word16Lit of Value.Word16.t
| Word32Lit of Value.Word32.t
Expand Down Expand Up @@ -110,6 +118,14 @@ let string_of_lit = function
| BoolLit true -> "true"
| IntLit n
| NatLit n -> Value.Int.to_pretty_string n
| Int8Lit n -> Value.Int_8.to_pretty_string n
| Int16Lit n -> Value.Int_16.to_pretty_string n
| Int32Lit n -> Value.Int_32.to_pretty_string n
| Int64Lit n -> Value.Int_64.to_pretty_string n
| Nat8Lit n -> Value.Nat8.to_pretty_string n
| Nat16Lit n -> Value.Nat16.to_pretty_string n
| Nat32Lit n -> Value.Nat32.to_pretty_string n
| Nat64Lit n -> Value.Nat64.to_pretty_string n
| Word8Lit n -> Value.Word8.to_pretty_string n
| Word16Lit n -> Value.Word16.to_pretty_string n
| Word32Lit n -> Value.Word32.to_pretty_string n
Expand Down
8 changes: 8 additions & 0 deletions src/as_types/arrange_type.ml
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,15 @@ let prim p = match p with
| Null -> Atom "Null"
| Bool -> Atom "Bool"
| Nat -> Atom "Nat"
| Nat8 -> Atom "Nat8"
| Nat16 -> Atom "Nat16"
| Nat32 -> Atom "Nat32"
| Nat64 -> Atom "Nat64"
| Int -> Atom "Int"
| Int8 -> Atom "Int8"
| Int16 -> Atom "Int16"
| Int32 -> Atom "Int32"
| Int64 -> Atom "Int64"
| Word8 -> Atom "Word8"
| Word16 -> Atom "Word16"
| Word32 -> Atom "Word32"
Expand Down
30 changes: 27 additions & 3 deletions src/as_types/type.ml
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,15 @@ type prim =
| Null
| Bool
| Nat
| Nat8
| Nat16
| Nat32
| Nat64
| Int
| Int8
| Int16
| Int32
| Int64
| Word8
| Word16
| Word32
Expand Down Expand Up @@ -72,7 +80,15 @@ let prim = function
| "Null" -> Null
| "Bool" -> Bool
| "Nat" -> Nat
| "Nat8" -> Nat8
| "Nat16" -> Nat16
| "Nat32" -> Nat32
| "Nat64" -> Nat64
| "Int" -> Int
| "Int8" -> Int8
| "Int16" -> Int16
| "Int32" -> Int32
| "Int64" -> Int64
| "Word8" -> Word8
| "Word16" -> Word16
| "Word32" -> Word32
Expand Down Expand Up @@ -399,9 +415,9 @@ let rec span = function
| Prim Null -> Some 1
| Prim Bool -> Some 2
| Prim (Nat | Int | Float | Text) -> None
| Prim Word8 -> Some 0x100
| Prim Word16 -> Some 0x10000
| Prim (Word32 | Word64 | Char) -> None (* for all practical purpuses *)
| Prim (Nat8 | Int8 | Word8) -> Some 0x100
| Prim (Nat16 | Int16 | Word16) -> Some 0x10000
| Prim (Nat32 | Int32 | Word32 | Nat64 | Int64 | Word64 | Char) -> None (* for all practical purposes *)
| Obj _ | Tup _ | Async _ -> Some 1
| Variant fs -> Some (List.length fs)
| Array _ | Func _ | Shared | Any -> None
Expand Down Expand Up @@ -785,7 +801,15 @@ let string_of_prim = function
| Null -> "Null"
| Bool -> "Bool"
| Nat -> "Nat"
| Nat8 -> "Nat8"
| Nat16 -> "Nat16"
| Nat32 -> "Nat32"
| Nat64 -> "Nat64"
| Int -> "Int"
| Int8 -> "Int8"
| Int16 -> "Int16"
| Int32 -> "Int32"
| Int64 -> "Int64"
| Float -> "Float"
| Word8 -> "Word8"
| Word16 -> "Word16"
Expand Down
8 changes: 8 additions & 0 deletions src/as_types/type.mli
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,15 @@ type prim =
| Null
| Bool
| Nat
| Nat8
| Nat16
| Nat32
| Nat64
| Int
| Int8
| Int16
| Int32
| Int64
| Word8
| Word16
| Word32
Expand Down
Loading