diff options
| author | Brian Campbell | 2017-12-07 13:31:46 +0000 |
|---|---|---|
| committer | Brian Campbell | 2017-12-07 13:31:46 +0000 |
| commit | 19386b2b3e595e4b5bc95dfd06fb9d32d786143e (patch) | |
| tree | 2c8ce6c528c705479ea2cbeffa297db3689a07c7 /lib | |
| parent | 691efa994a72d0e9cdbcdfcc4d6a9b1976d91e2b (diff) | |
Support monomorphisation with set constrained integers
Also, to support this,
constant propagation for integer multiply,
fix substitution of concrete values for nvars,
size parameters in single argument functions,
fix kind for itself,
add eq_atom to prelude
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/prelude.sail | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/lib/prelude.sail b/lib/prelude.sail index 92bfb180..a7f6fb2f 100644 --- a/lib/prelude.sail +++ b/lib/prelude.sail @@ -266,6 +266,8 @@ overload (deinfix |) [or_bool; bitwise_or] val extern forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure eq_vec +val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure eq_atom = "eq" + val extern forall Type 'a. ('a, 'a) -> bool effect pure eq val extern forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure neq_vec @@ -274,7 +276,7 @@ val extern forall Type 'a. ('a, 'a) -> bool effect pure neq (*function forall Num 'n, Num 'm, Order 'ord. bool neq_vec (v1, v2) = bool_not(eq_vec(v1, v2))*) -overload (deinfix ==) [eq_vec; eq] +overload (deinfix ==) [eq_vec; eq_atom; eq] overload (deinfix !=) [neq_vec; neq] val extern forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure gteq_vec |