summaryrefslogtreecommitdiff
path: root/src/gen_lib
diff options
context:
space:
mode:
Diffstat (limited to 'src/gen_lib')
-rw-r--r--src/gen_lib/prompt.lem2
-rw-r--r--src/gen_lib/sail_values.lem111
2 files changed, 57 insertions, 56 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index f770042c..72effa2f 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -15,7 +15,7 @@ let rec bind m f = match m with
| Barrier descr o_s -> Barrier descr (let (o,opt) = o_s in (bind o f,opt))
| Footprint o_s -> Footprint (let (o,opt) = o_s in (bind o f,opt))
| Write_reg descr o_s -> Write_reg descr (let (o,opt) = o_s in (bind o f,opt))
- | Escape descr mo -> Escape descr mo
+ | Escape descr -> Escape descr
| Fail descr -> Fail descr
| Error descr -> Error descr
| Internal descr o_s -> Internal descr (let (o,opt) = o_s in (bind o f ,opt))
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 0d47a5e8..4771bcd7 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -17,12 +17,12 @@ let rec replace bs ((n : integer),b') = match bs with
(*** Bits *)
-type bitU = O | I | Undef
+type bitU = B0 | B1 | BU
let showBitU = function
- | O -> "O"
- | I -> "I"
- | Undef -> "Undef"
+ | B0 -> "O"
+ | B1 -> "I"
+ | BU -> "U"
end
instance (Show bitU)
@@ -31,52 +31,52 @@ end
let bitU_to_bool = function
- | O -> false
- | I -> true
- | Undef -> failwith "to_bool applied to Undef"
+ | B0 -> false
+ | B1 -> true
+ | BU -> failwith "to_bool applied to BU"
end
let bit_lifted_of_bitU = function
- | O -> Bitl_zero
- | I -> Bitl_one
- | Undef -> Bitl_undef
+ | B0 -> Bitl_zero
+ | B1 -> Bitl_one
+ | BU -> Bitl_undef
end
let bitU_of_bit = function
- | Bitc_zero -> O
- | Bitc_one -> I
+ | Bitc_zero -> B0
+ | Bitc_one -> B1
end
let bit_of_bitU = function
- | O -> Bitc_zero
- | I -> Bitc_one
- | Undef -> failwith "bit_of_bitU: Undef"
+ | B0 -> Bitc_zero
+ | B1 -> Bitc_one
+ | BU -> failwith "bit_of_bitU: BU"
end
let bitU_of_bit_lifted = function
- | Bitl_zero -> O
- | Bitl_one -> I
- | Bitl_undef -> Undef
+ | Bitl_zero -> B0
+ | Bitl_one -> B1
+ | Bitl_undef -> BU
| Bitl_unknown -> failwith "bitU_of_bit_lifted Bitl_unknown"
end
let bitwise_not_bit = function
- | I -> O
- | O -> I
- | Undef -> Undef
+ | B1 -> B0
+ | B0 -> B1
+ | BU -> BU
end
let inline (~) = bitwise_not_bit
val is_one : integer -> bitU
let is_one i =
- if i = 1 then I else O
+ if i = 1 then B1 else B0
-let bool_to_bitU b = if b then I else O
+let bool_to_bitU b = if b then B1 else B0
let bitwise_binop_bit op = function
- | (Undef,_) -> Undef (*Do we want to do this or to respect | of I and & of B0 rules?*)
- | (_,Undef) -> Undef (*Do we want to do this or to respect | of I and & of B0 rules?*)
+ | (BU,_) -> BU (*Do we want to do this or to respect | of I and & of B0 rules?*)
+ | (_,BU) -> BU (*Do we want to do this or to respect | of I and & of B0 rules?*)
| (x,y) -> bool_to_bitU (op (bitU_to_bool x) (bitU_to_bool y))
end
@@ -234,9 +234,9 @@ let unsigned (Vector bs _ _) : integer =
List.foldr
(fun b (acc,exp) ->
match b with
- | I -> (acc + integerPow 2 exp,exp + 1)
- | O -> (acc, exp + 1)
- | Undef -> failwith "unsigned: vector has undefined bits"
+ | B1 -> (acc + integerPow 2 exp,exp + 1)
+ | B0 -> (acc, exp + 1)
+ | BU -> failwith "unsigned: vector has undefined bits"
end)
(0,0) bs in
sum
@@ -245,9 +245,9 @@ let unsigned_big = unsigned
let signed v : integer =
match most_significant v with
- | I -> 0 - (1 + (unsigned (bitwise_not v)))
- | O -> unsigned v
- | Undef -> failwith "signed applied to vector with undefined bits"
+ | B1 -> 0 - (1 + (unsigned (bitwise_not v)))
+ | B0 -> unsigned v
+ | BU -> failwith "signed applied to vector with undefined bits"
end
let hardware_mod (a: integer) (b:integer) : integer =
@@ -301,19 +301,19 @@ let get_min_representable_in _ (n : integer) : integer =
val to_bin_aux : natural -> list bitU
let rec to_bin_aux x =
if x = 0 then []
- else (if x mod 2 = 1 then I else O) :: to_bin_aux (x / 2)
+ else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2)
let to_bin n = List.reverse (to_bin_aux n)
val pad_zero : list bitU -> integer -> list bitU
let rec pad_zero bits n =
- if n = 0 then bits else pad_zero (O :: bits) (n -1)
+ if n = 0 then bits else pad_zero (B0 :: bits) (n -1)
let rec add_one_bit_ignore_overflow_aux bits = match bits with
| [] -> []
- | O :: bits -> I :: bits
- | I :: bits -> O :: add_one_bit_ignore_overflow_aux bits
- | Undef :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit"
+ | B0 :: bits -> B1 :: bits
+ | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits
+ | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit"
end
let add_one_bit_ignore_overflow bits =
@@ -339,7 +339,7 @@ let to_vec_inc = to_vec true
let to_vec_dec = to_vec false
let to_vec_undef is_inc (len : integer) =
- Vector (replicate (natFromInteger len) Undef) (if is_inc then 0 else len-1) is_inc
+ Vector (replicate (natFromInteger len) BU) (if is_inc then 0 else len-1) is_inc
let to_vec_inc_undef = to_vec_undef true
let to_vec_dec_undef = to_vec_undef false
@@ -440,7 +440,7 @@ let addS_VVI = arith_op_vec_vec_range integerAdd true
let arith_op_vec_bit op sign (size : integer) (Vector _ _ is_inc as l)r =
let l' = to_num sign l in
- let n = op l' (match r with | I -> (1 : integer) | _ -> 0 end) in
+ let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in
to_vec is_inc (length l * size,n)
(* add_vec_bit
@@ -463,7 +463,7 @@ let rec arith_op_overflow_vec (op : integer -> integer -> integer) sign size (Ve
let overflow =
if n <= get_max_representable_in sign len &&
n >= get_min_representable_in sign len
- then O else I in
+ then B0 else B1 in
let c_out = most_significant one_more_size_u in
(correct_size_num,overflow,c_out)
@@ -487,9 +487,9 @@ let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (siz
let l' = to_num sign l in
let l_u = to_num false l in
let (n,nu,changed) = match r_bit with
- | I -> (op l' 1, op l_u 1, true)
- | O -> (l',l_u,false)
- | _ -> failwith "arith_op_overflow_vec_bit applied to undefined bit"
+ | B1 -> (op l' 1, op l_u 1, true)
+ | B0 -> (l',l_u,false)
+ | BU -> failwith "arith_op_overflow_vec_bit applied to undefined bit"
end in
(* | _ -> assert false *)
let correct_size_num = to_vec is_inc (act_size,n) in
@@ -498,8 +498,8 @@ let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (siz
if changed
then
if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size
- then O else I
- else O in
+ then B0 else B1
+ else B0 in
(correct_size_num,overflow,most_significant one_larger)
(* add_overflow_vec_bit_signed
@@ -516,9 +516,9 @@ let shift_op_vec op (Vector bs start is_inc,(n : integer)) =
let n = natFromInteger n in
match op with
| LL_shift (*"<<"*) ->
- Vector (sublist bs (n,List.length bs -1) ++ List.replicate n O) start is_inc
+ Vector (sublist bs (n,List.length bs -1) ++ List.replicate n B0) start is_inc
| RR_shift (*">>"*) ->
- Vector (List.replicate n O ++ sublist bs (0,n-1)) start is_inc
+ Vector (List.replicate n B0 ++ sublist bs (0,n-1)) start is_inc
| LLL_shift (*"<<<"*) ->
Vector (sublist bs (n,List.length bs - 1) ++ sublist bs (0,n-1)) start is_inc
end
@@ -545,7 +545,7 @@ let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Vector
end in
if representable
then to_vec is_inc (act_size,n')
- else Vector (List.replicate (natFromInteger act_size) Undef) start is_inc
+ else Vector (List.replicate (natFromInteger act_size) BU) start is_inc
let mod_VVV = arith_op_vec_no0 hardware_mod false 1
let quot_VVV = arith_op_vec_no0 hardware_quot false 1
@@ -569,9 +569,9 @@ let arith_op_overflow_no0_vec op sign size ((Vector _ start is_inc) as l) r =
if representable then
(to_vec is_inc (act_size,n'),to_vec is_inc (act_size + 1,n_u'))
else
- (Vector (List.replicate (natFromInteger act_size) Undef) start is_inc,
- Vector (List.replicate (natFromInteger (act_size + 1)) Undef) start is_inc) in
- let overflow = if representable then O else I in
+ (Vector (List.replicate (natFromInteger act_size) BU) start is_inc,
+ Vector (List.replicate (natFromInteger (act_size + 1)) BU) start is_inc) in
+ let overflow = if representable then B0 else B1 in
(correct_size_num,overflow,most_significant one_more)
let quotO_VVV = arith_op_overflow_no0_vec hardware_quot false 1
@@ -658,7 +658,7 @@ let make_indexed_vector entries default start length dir =
(*
val make_bit_vector_undef : integer -> vector bitU
let make_bitvector_undef length =
- Vector (replicate (natFromInteger length) Undef) 0 true
+ Vector (replicate (natFromInteger length) BU) 0 true
*)
(* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *)
@@ -887,10 +887,11 @@ let assert' b msg_opt =
(* convert numbers unsafely to naturals *)
class (ToNatural 'a) val toNatural : 'a -> natural end
-instance (ToNatural integer) let toNatural = naturalFromInteger end
-instance (ToNatural int) let toNatural = naturalFromInt end
-instance (ToNatural nat) let toNatural = naturalFromNat end
-instance (ToNatural natural) let toNatural = id end
+(* eta-expanded for Isabelle output, otherwise it breaks *)
+instance (ToNatural integer) let toNatural = (fun n -> naturalFromInteger n) end
+instance (ToNatural int) let toNatural = (fun n -> naturalFromInt n) end
+instance (ToNatural nat) let toNatural = (fun n -> naturalFromNat n) end
+instance (ToNatural natural) let toNatural = (fun n -> n) end
let toNaturalFiveTup (n1,n2,n3,n4,n5) =
(toNatural n1,
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 09:53:48 +0000