diff options
| author | Thomas Bauereiss <tb592@cl.cam.ac.uk> | 2020-02-28 12:37:51 +0000 |
|---|---|---|
| committer | Thomas Bauereiss <tb592@cl.cam.ac.uk> | 2020-02-28 12:37:51 +0000 |
| commit | f08b8a860143353848d4e1b2cb754f43434cd02d (patch) | |
| tree | 5c368ce609e45de740bbde2c1f7ac036057b741b | |
| parent | c71ed5b110b13be9e656feeda2ac82d452b4fee9 (diff) | |
| download | sail-riscv-f08b8a860143353848d4e1b2cb754f43434cd02d.zip sail-riscv-f08b8a860143353848d4e1b2cb754f43434cd02d.tar.gz sail-riscv-f08b8a860143353848d4e1b2cb754f43434cd02d.tar.bz2 | |
Make types of min/max more precise
Might help typechecking sail-cheri-riscv code.
| -rw-r--r-- | model/prelude.sail | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/model/prelude.sail b/model/prelude.sail index a8faf3d..29e7c4f 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -80,17 +80,15 @@ val rem_round_zero = {ocaml: "rem_round_zero", interpreter: "rem_round_zero", le /* The following should get us euclidean modulus, and is compatible with pre and post 0.9 versions of sail */ overload operator % = {emod_int, mod} -val min_nat = {ocaml: "min_int", interpreter: "min_int", lem: "min", coq: "min_nat", c: "min_int"} : (nat, nat) -> nat +val min_int = {ocaml: "min_int", interpreter: "min_int", lem: "min", coq: "min_atom", c: "min_int"} : forall 'x 'y. + (int('x), int('y)) -> {'z, ('x <= 'y & 'z == 'x) | ('x > 'y & 'z == 'y). int('z)} -val min_int = {ocaml: "min_int", interpreter: "min_int", lem: "min", coq: "Z.min", c: "min_int"} : (int, int) -> int +val max_int = {ocaml: "max_int", interpreter: "max_int", lem: "max", coq: "max_atom", c: "max_int"} : forall 'x 'y. + (int('x), int('y)) -> {'z, ('x >= 'y & 'z == 'x) | ('x < 'y & 'z == 'y). int('z)} -val max_nat = {ocaml: "max_int", interpreter: "max_int", lem: "max", coq: "max_nat", c: "max_int"} : (nat, nat) -> nat +overload min = {min_int} -val max_int = {ocaml: "max_int", interpreter: "max_int", lem: "max", coq: "Z.max", c: "max_int"} : (int, int) -> int - -overload min = {min_nat, min_int} - -overload max = {max_nat, max_int} +overload max = {max_int} val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n) |