diff options
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/sail_values.lem | 38 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 6 | ||||
| -rw-r--r-- | src/gen_lib/vector.lem | 12 |
3 files changed, 30 insertions, 26 deletions
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index c47e763f..a51a0091 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -13,15 +13,7 @@ let get_elements (Vector elements _) = elements let get_start (Vector _ s) = s let length (Vector bs _) = length bs -let rec nth n xs = match (n,l) with - | (0,x :: xs) -> x - | (n + 1,x :: xs) -> nth n xs -end - -let vector_access (Vector bs start) n = - if is_inc then nth bs (n - start) else nth bs (start - n) - - +(* let write_two_registers r1 r2 vec = let size = length_register r1 in let start = get_start vec in @@ -32,7 +24,7 @@ let write_two_registers r1 r2 vec = vec (if is_inc then size - start else start - size) (if is_inc then vsize - start else start - vsize) in write_register r1 r1_v >> write_register r2 r2_v - + *) let rec replace bs ((n : nat),b') = match (n,bs) with | (_, []) -> [] @@ -141,7 +133,7 @@ let rec add_one_bit bs co i = (* | Vundef,_ -> assert false*) end -let to_vec len (n : integer) = +let to_vec (len,(n : integer)) = let bs = List.replicate len B0 in let start = if is_inc then 0 else len-1 in if n = 0 then Vector bs start @@ -152,6 +144,8 @@ let to_vec len (n : integer) = let (Vector bs start) = bitwise_not (Vector abs_bs start) in Vector (add_one_bit bs false (len-1)) start +let to_vec_inc = to_vec +let to_vec_dec = to_vec let to_vec_undef len = Vector (replicate len BU) (if is_inc then 0 else len-1) @@ -167,7 +161,7 @@ let power = uncurry integerPow let arith_op_vec op sign size (l,r) = let (l',r') = (to_num sign l, to_num sign r) in let n = op l' r' in - to_vec (size * (length l)) n + to_vec (size * (length l),n) let add_vec = arith_op_vec integerAdd false 1 let add_vec_signed = arith_op_vec integerAdd true 1 @@ -176,7 +170,7 @@ let multiply_vec = arith_op_vec integerMult false 2 let multiply_vec_signed = arith_op_vec integerMult true 2 let arith_op_vec_range op sign size (l,r) = - arith_op_vec op sign size (l, to_vec (length l) r) + arith_op_vec op sign size (l, to_vec (length l,r)) let add_vec_range = arith_op_vec_range integerAdd false 1 let add_vec_range_signed = arith_op_vec_range integerAdd true 1 @@ -185,7 +179,7 @@ let mult_vec_range = arith_op_vec_range integerMult false 2 let mult_vec_range_signed = arith_op_vec_range integerMult true 2 let arith_op_range_vec op sign size (l,r) = - arith_op_vec op sign size (to_vec (length r) l, r) + arith_op_vec op sign size (to_vec (length r, l), r) let add_range_vec = arith_op_range_vec integerAdd false 1 let add_range_vec_signed = arith_op_range_vec integerAdd true 1 @@ -215,7 +209,7 @@ let add_vec_vec_range_signed = arith_op_vec_vec_range integerAdd true let arith_op_vec_bit op sign (size : nat) (l,r) = let l' = to_num sign l in let n = op l' match r with | B1 -> (1 : integer) | _ -> 0 end in - to_vec (length l * size) n + to_vec (length l * size,n) let add_vec_bit = arith_op_vec_bit integerAdd false 1 let add_vec_bit_signed = arith_op_vec_bit integerAdd true 1 @@ -228,8 +222,8 @@ let rec arith_op_overflow_vec (op : integer -> integer -> integer) sign size (l, let (l_unsign,r_unsign) = (to_num false l,to_num false r) in let n = op l_sign r_sign in let n_unsign = op l_unsign r_unsign in - let correct_size_num = to_vec act_size n in - let one_more_size_u = to_vec (act_size + 1) n_unsign in + let correct_size_num = to_vec (act_size,n) in + let one_more_size_u = to_vec (act_size + 1,n_unsign) in let overflow = if n <= get_max_representable_in sign len && n >= get_min_representable_in sign len @@ -253,8 +247,8 @@ let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (siz | B0 -> (l',l_u,false) end in (* | _ -> assert false *) - let correct_size_num = to_vec act_size n in - let one_larger = to_vec (act_size + 1) nu in + let correct_size_num = to_vec (act_size,n) in + let one_larger = to_vec (act_size + 1,nu) in let overflow = if changed then @@ -308,7 +302,7 @@ let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size (((Vecto | _ -> (false,0) end in if representable - then to_vec act_size n' + then to_vec (act_size,n') else Vector (List.replicate act_size BU) start let mod_vec = arith_op_vec_no0 integerMod false 1 @@ -331,7 +325,7 @@ let arith_op_overflow_no0_vec op sign size (((Vector _ start) as l),r) = end in let (correct_size_num,one_more) = if representable then - (to_vec act_size n',to_vec (act_size + 1) n_u') + (to_vec (act_size,n'),to_vec (act_size + 1,n_u')) else (Vector (List.replicate act_size BU) start, Vector (List.replicate (act_size + 1) BU) start) in @@ -342,7 +336,7 @@ let quot_overflow_vec = arith_op_overflow_no0_vec integerDiv false 1 let quot_overflow_vec_signed = arith_op_overflow_no0_vec integerDiv true 1 let arith_op_vec_range_no0 op sign size (l,r) = - arith_op_vec_no0 op sign size (l,to_vec (length l) r) + arith_op_vec_no0 op sign size (l,to_vec (length l,r)) let mod_vec_range = arith_op_vec_range_no0 integerMod false 1 diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index ce3be419..f9404416 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -1,12 +1,12 @@ open import Pervasives -type M 's 'a = <| runState : 's -> ('a * 's) |> +type M 's 'a = 's -> ('a * 's) val return : forall 's 'a. 'a -> M 's 'a -let return a = <| runState = (fun s -> (a,s)) |> +let return a = fun s -> (a,s) val bind : forall 's 'a 'b. M 's 'a -> ('a -> M 's 'b) -> M 's 'b -let bind m f = <| runState = (fun s -> let (a,s) = m.runState s in (f a).runState s) |> +let bind m f s = let (a,s') = m s in f a s' let (>>=) = bind let (>>) m n = m >>= fun _ -> n diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem index 75628f45..d5f47492 100644 --- a/src/gen_lib/vector.lem +++ b/src/gen_lib/vector.lem @@ -1,8 +1,15 @@ open import Pervasives type bit = B0 | B1 | BU -type vector = Vector of list bit * nat +type vector 'a = Vector of list 'a * nat +let rec nth xs (n : nat) = match (n,xs) with + | (0,x :: xs) -> x + | (n + 1,x :: xs) -> nth xs n +end + +let vector_access is_inc (Vector bs start) n = + if is_inc then nth bs (n - start) else nth bs (start - n) let read_vector_subrange is_inc (Vector bs start) n m = let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in @@ -16,4 +23,7 @@ let write_vector_subrange is_inc (Vector bs start) n m (Vector bs' _) = let (_,suffix) = List.splitAt (offset + length) bs in Vector (prefix ++ (List.take length bs') ++ suffix) start +let write_vector_bit is_inc v n (Vector [b] 0) = + write_vector_subrange is_inc v n n b + let hd (x :: xs) = x |