diff options
| author | Thomas Bauereiss | 2017-11-07 15:34:35 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-11-07 15:34:35 +0000 |
| commit | 1dbf01cafae9aba80582754f17d831c8bc11cdba (patch) | |
| tree | 8c69c4f27f97e9bc696e6706d9ba66ef4f5fdded /cheri | |
| parent | ff9610e460b60fc35a529dfbc1d6b8d9c0072104 (diff) | |
Declare prelude functions as extern
Also, rename a few functions for uniformity, e.g. bool_and -> and_bool
Diffstat (limited to 'cheri')
| -rw-r--r-- | cheri/cheri_prelude_128.sail | 4 | ||||
| -rw-r--r-- | cheri/cheri_prelude_256.sail | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail index f1f33a56..5e63221e 100644 --- a/cheri/cheri_prelude_128.sail +++ b/cheri/cheri_prelude_128.sail @@ -35,8 +35,8 @@ (* 128 bit cap + tag *) typedef CapReg = bit[129] -val cast bool -> bit effect pure cast_bool_bit -val cast forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_boolvec_bitvec +val cast extern bool -> bit effect pure cast_bool_bit +val cast extern forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_boolvec_bitvec val cast forall 'm. [|0:2**'m - 1|] -> vector<'m - 1,'m,dec,bit> effect pure cast_range_bitvec function vector<'m - 1,'m,dec,bit> cast_range_bitvec (v) = to_vec (v) val extern bool -> bool effect pure not diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail index 7cf3d69c..7b42020d 100644 --- a/cheri/cheri_prelude_256.sail +++ b/cheri/cheri_prelude_256.sail @@ -35,8 +35,8 @@ (* 256 bit cap + tag *) typedef CapReg = bit[257] -val cast bool -> bit effect pure cast_bool_bit -val cast forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_boolvec_bitvec +val cast extern bool -> bit effect pure cast_bool_bit +val cast extern forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_boolvec_bitvec val cast forall 'm. [|0:2**'m - 1|] -> vector<'m - 1,'m,dec,bit> effect pure cast_range_bitvec function vector<'m - 1,'m,dec,bit> cast_range_bitvec (v) = to_vec (v) val extern bool -> bool effect pure not |