From 5bc5f5dee8921f8d24260dae54177e00c291fcb1 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 10 Dec 2018 20:39:16 +0000
Subject: Various changes:

* Improve type inference for numeric if statements (if_infer test)

* Correctly handle constraints for existentially quantified constructors (constraint_ctor test)

* Canonicalise all numeric types in function arguments, which
  triggers some weird edge cases between parametric polymorphism and
  subtyping of numeric arguments

* Because of this eq_int, eq_range, and eq_atom etc become identical

* Avoid duplicating destruct_exist in Env

* Handle some odd subtyping cases better
---
 aarch64/prelude.sail | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'aarch64')

diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index 8cd18fac..505ca7b6 100755
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -143,12 +143,12 @@ val UInt = {
   interpreter: "uint",
   c: "sail_unsigned",
   coq: "uint"
-} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
+} : forall 'n. bits('n) -> {'m, 0 <= 'm <= 2 ^ 'n - 1. int('m)}
 
 val SInt = {
   c: "sail_signed",
   _: "sint"
-} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
+} : forall 'n. bits('n) -> {'m, (- (2 ^ ('n - 1))) <= 'm <= 2 ^ ('n - 1) - 1. int('m)}
 
 val hex_slice = "hex_slice" : forall 'n 'm. (string, atom('n), atom('m)) -> bits('n - 'm) effect {escape}
 
-- 
cgit v1.2.3