diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/prompt.lem | 84 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 310 | ||||
| -rw-r--r-- | src/gen_lib/vector.lem | 59 | ||||
| -rw-r--r-- | src/lem_interp/interp.lem | 1 | ||||
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 61 | ||||
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 6 | ||||
| -rw-r--r-- | src/lem_interp/sail_impl_base.lem | 307 | ||||
| -rw-r--r-- | src/pretty_print.ml | 571 | ||||
| -rw-r--r-- | src/process_file.ml | 4 |
9 files changed, 765 insertions, 638 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index 412bfbc1..6dea2e9b 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -1,35 +1,41 @@ open import Pervasives_extra open import Sail_impl_base -open import Vector open import Sail_values -val return : forall 's 'e 'a. 'a -> outcome 's 'e 'a + import Interp_interface +(* this needs to go away: it's only so we can make the ppcmem outcome types the +same *) + +val return : forall 's 'a. 'a -> outcome 's 'a let return a = Done a -val bind : forall 's 'e 'a 'b. outcome 's 'e 'a -> ('a -> outcome 's 'e 'b) -> outcome 's 'e 'b +val bind : forall 's 'a 'b. outcome 's 'a -> ('a -> outcome 's 'b) -> outcome 's 'b let rec bind m f = match m with - | Done a -> f a + | Done a -> f a | Read_mem descr k -> Read_mem descr (fun v -> let (o,opt) = k v in (bind o f,opt)) | Read_reg descr k -> Read_reg descr (fun v -> let (o,opt) = k v in (bind o f,opt)) | Write_memv descr k -> Write_memv descr (fun v -> let (o,opt) = k v in (bind o f,opt)) - | Write_ea descr o_s -> Write_ea descr (let (o,opt) = o_s in (bind o f,opt)) - | 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 o_s -> Escape o_s + | Write_ea descr o_s -> Write_ea descr (let (o,opt) = o_s in (bind o f,opt)) + | 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 + | Fail descr -> Fail descr + | Error descr -> Error descr + | Internal descr o_s -> Internal descr (let (o,opt) = o_s in (bind o f ,opt)) end -type M 'e 'a = Sail_impl_base.outcome unit 'e 'a +type M 'a = Sail_impl_base.outcome Interp_interface.instruction_state 'a -let (>>=) = bind -val (>>) : forall 'e 'b. M 'e unit -> M 'e 'b -> M 'e 'b -let (>>) m n = m >>= fun _ -> n +let inline (>>=) = bind +val (>>) : forall 'b. M unit -> M 'b -> M 'b +let inline (>>) m n = m >>= fun _ -> n -val exit : forall 'a 'e. 'e -> M 'e 'a -let exit e = Escape (Just (return e,Nothing)) +val exit : forall 'a. string -> M 'a +let exit s = Fail (Just s) -val read_memory : forall 'e. read_kind -> vector bitU -> integer -> M 'e (vector bitU) +val read_memory : read_kind -> vector bitU -> integer -> M (vector bitU) let read_memory rk addr sz = let addr = address_lifted_of_bitv addr in let sz = natFromInteger sz in @@ -38,20 +44,20 @@ let read_memory rk addr sz = (Done bitv,Nothing) in Read_mem (rk,addr,sz) k -val write_memory_ea : forall 'e. write_kind -> vector bitU -> integer -> M 'e unit +val write_memory_ea : write_kind -> vector bitU -> integer -> M unit let write_memory_ea wk addr sz = let addr = address_lifted_of_bitv addr in let sz = natFromInteger sz in Write_ea (wk,addr,sz) (Done (),Nothing) -val write_memory_val : forall 'e. vector bitU -> M 'e bool +val write_memory_val : vector bitU -> M bool let write_memory_val v = let v = byte_lifteds_of_bitv v in let k successful = (return successful,Nothing) in Write_memv v k -val read_reg_range : forall 'e. register -> integer -> integer -> M 'e (vector bitU) +val read_reg_range : register -> integer -> integer -> M (vector bitU) let read_reg_range reg i j = let (i,j) = (natFromInteger i,natFromInteger j) in let reg = Reg_slice (name_of_reg reg) (start_of_reg_nat reg) (dir_of_reg reg) @@ -61,11 +67,11 @@ let read_reg_range reg i j = (Done v,Nothing) in Read_reg reg k -val read_reg_bit : forall 'e. register -> integer -> M 'e bitU -let read_reg_bit reg i = +val read_reg_bit : register -> integer -> M bitU +let read_reg_bit reg i = read_reg_range reg i i >>= fun v -> return (access v i) -val read_reg : forall 'e. register -> M 'e (vector bitU) +val read_reg : register -> M (vector bitU) let read_reg reg = let reg = Reg (name_of_reg reg) (start_of_reg_nat reg) (size_of_reg_nat reg) (dir_of_reg reg) in @@ -75,8 +81,8 @@ let read_reg reg = Read_reg reg k -val read_reg_field : forall 'e. register -> register_field -> M 'e (vector bitU) -let read_reg_field reg regfield = +val read_reg_field : register -> register_field -> M (vector bitU) +let read_reg_field reg regfield = let (i,j) = register_field_indices_nat reg regfield in let reg = Reg_slice (name_of_reg reg) (start_of_reg_nat reg) (dir_of_reg reg) (if i<j then (i,j) else (j,i)) in @@ -85,48 +91,48 @@ let read_reg_field reg regfield = (Done v,Nothing) in Read_reg reg k -val read_reg_bitfield : forall 'e. register -> register_field -> M 'e bitU +val read_reg_bitfield : register -> register_field -> M bitU let read_reg_bitfield reg rbit = read_reg_bit reg (fst (register_field_indices reg rbit)) -val write_reg_range : forall 'e. register -> integer -> integer -> vector bitU -> M 'e unit +val write_reg_range : register -> integer -> integer -> vector bitU -> M unit let write_reg_range reg i j v = let rv = registerValueFromBitv v reg in let (i,j) = (natFromInteger i,natFromInteger j) in let reg = Reg_slice (name_of_reg reg) (start_of_reg_nat reg) (dir_of_reg reg) (i,j) in Write_reg (reg,rv) (Done (),Nothing) -val write_reg_bit : forall 'e. register -> integer -> bitU -> M 'e unit +val write_reg_bit : register -> integer -> bitU -> M unit let write_reg_bit reg i bit = write_reg_range reg i i (Vector [bit] 0 true) -val write_reg : forall 'e. register -> vector bitU -> M 'e unit +val write_reg : register -> vector bitU -> M unit let write_reg reg v = let rv = registerValueFromBitv v reg in let reg = Reg (name_of_reg reg) (start_of_reg_nat reg) (size_of_reg_nat reg) (dir_of_reg reg) in Write_reg (reg,rv) (Done (),Nothing) -val write_reg_field : forall 'e. register -> register_field -> vector bitU -> M 'e unit +val write_reg_field : register -> register_field -> vector bitU -> M unit let write_reg_field reg regfield = uncurry (write_reg_range reg) (register_field_indices reg regfield) -val write_reg_bitfield : forall 'e. register -> register_field -> bitU -> M 'e unit +val write_reg_bitfield : register -> register_field -> bitU -> M unit let write_reg_bitfield reg rbit = write_reg_bit reg (fst (register_field_indices reg rbit)) -val barrier : forall 'e. barrier_kind -> M 'e unit +val barrier : barrier_kind -> M unit let barrier bk = Barrier bk (Done (), Nothing) -val footprint : forall 'e. M 'e unit +val footprint : M unit let footprint = Footprint (Done (),Nothing) -val foreachM_inc : forall 'e 'vars. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> M 'e 'vars) -> M 'e 'vars -let rec foreachM_inc (i,stop,by) vars body = +val foreachM_inc : forall 'vars. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> M 'vars) -> M 'vars +let rec foreachM_inc (i,stop,by) vars body = if i <= stop then body i vars >>= fun vars -> @@ -134,9 +140,9 @@ let rec foreachM_inc (i,stop,by) vars body = else return vars -val foreachM_dec : forall 'e 'vars. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> M 'e 'vars) -> M 'e 'vars -let rec foreachM_dec (i,stop,by) vars body = +val foreachM_dec : forall 'vars. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> M 'vars) -> M 'vars +let rec foreachM_dec (i,stop,by) vars body = if i >= stop then body i vars >>= fun vars -> @@ -150,7 +156,7 @@ let write_two_regs r1 r2 vec = let () = ensure (is_inc_r1 = is_inc_r2) "write_two_regs called with vectors of different direction" in is_inc_r1 in - + let (size_r1 : integer) = size_of_reg r1 in let (start_vec : integer) = get_start vec in let size_vec = length vec in diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 3e4971df..d4b95ac8 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -1,15 +1,74 @@ open import Pervasives_extra open import Sail_impl_base -open import Vector open import Interp (* only for converting between shallow- and deep-embedding values *) open import Interp_ast (* only for converting between shallow- and deep-embedding values *) -type i = integer -type n = natural +type ii = integer +type nn = natural type bitU = O | I | Undef + +(* element list * start * has increasing direction *) +type vector 'a = Vector of list 'a * integer * bool + +let rec nth xs (n : integer) = + match xs with + | x :: xs -> if n = 0 then x else nth xs (n - 1) + | _ -> failwith "nth applied to empty list" + end + + +let get_dir (Vector _ _ ord) = ord +let get_start (Vector _ s _) = s +let length (Vector bs _ _) = integerFromNat (length bs) + +let rec replace bs ((n : integer),b') = match bs with + | [] -> [] + | b :: bs -> + if n = 0 then + b' :: bs + else + b :: replace bs (n - 1,b') + end + +let vector_concat (Vector bs start is_inc) (Vector bs' _ _) = + Vector (bs ++ bs') start is_inc + +let inline (^^) = vector_concat + +val slice : forall 'a. vector 'a -> integer -> integer -> vector 'a +let slice (Vector bs start is_inc) n m = + let n = natFromInteger n in + let m = natFromInteger m in + let start = natFromInteger start in + let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in + let (_,suffix) = List.splitAt offset bs in + let (subvector,_) = List.splitAt length suffix in + let n = integerFromNat n in + Vector subvector n is_inc + +val update : forall 'a. vector 'a -> integer -> integer -> vector 'a -> vector 'a +let update (Vector bs start is_inc) n m (Vector bs' _ _) = + let n = natFromInteger n in + let m = natFromInteger m in + let start = natFromInteger start in + let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in + let (prefix,_) = List.splitAt offset bs in + let (_,suffix) = List.splitAt (offset + length) bs in + let start = integerFromNat start in + Vector (prefix ++ (List.take length bs') ++ suffix) start is_inc + +val access : forall 'a. vector 'a -> integer -> 'a +let access (Vector bs start is_inc) n = + if is_inc then nth bs (n - start) else nth bs (start - n) + +val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a +let update_pos v n b = + update v n n (Vector [b] 0 true) + + type register_field = string type register_field_index = string * (integer * integer) (* name, start and end *) @@ -38,11 +97,21 @@ let size_of_reg_nat reg = natFromInteger (size_of_reg reg) let start_of_reg_nat reg = natFromInteger (start_of_reg reg) +val register_field_indices_aux : register -> register_field -> maybe (integer * integer) +let rec register_field_indices_aux register rfield = + match register with + | Register _ _ _ _ rfields -> List.lookup rfield rfields + | RegisterPair r1 r2 -> + let m_indices = register_field_indices_aux r1 rfield in + if isJust m_indices then m_indices else register_field_indices_aux r2 rfield + | UndefinedRegister -> Nothing + end + val register_field_indices : register -> register_field -> integer * integer -let register_field_indices (Register _ _ _ _ rfields) rfield = - match List.lookup rfield rfields with - | None -> failwith "Invalid register/register-field combination" +let register_field_indices register rfield = + match register_field_indices_aux register rfield with | Just indices -> indices + | Nothing -> failwith "Invalid register/register-field combination" end let register_field_indices_nat reg regfield= @@ -55,7 +124,6 @@ let to_bool = function | Undef -> failwith "to_bool applied to Undef" end - let bit_lifted_of_bitU = function | O -> Bitl_zero | I -> Bitl_one @@ -87,7 +155,7 @@ let bitwise_not_bit = function | _ -> Undef end -let (~) = bitwise_not_bit +let inline (~) = bitwise_not_bit val pow : integer -> integer -> integer let pow m n = m ** (natFromInteger n) @@ -118,13 +186,13 @@ val bitwise_xor_bit : bitU * bitU -> bitU let bitwise_xor_bit = bitwise_binop_bit xor val (&.) : bitU -> bitU -> bitU -let (&.) x y = bitwise_and_bit (x,y) +let inline (&.) x y = bitwise_and_bit (x,y) val (|.) : bitU -> bitU -> bitU -let (|.) x y = bitwise_or_bit (x,y) +let inline (|.) x y = bitwise_or_bit (x,y) val (+.) : bitU -> bitU -> bitU -let (+.) x y = bitwise_xor_bit (x,y) +let inline (+.) x y = bitwise_xor_bit (x,y) let bitwise_binop op (Vector bsl start is_inc, Vector bsr _ _) = let revbs = foldl (fun acc pair -> bitwise_binop_bit op pair :: acc) [] (zip bsl bsr) in @@ -140,7 +208,7 @@ let unsigned (Vector bs _ _ as v) : integer = (fun (acc,exp) b -> (acc + (if b = I then integerPow 2 exp else 0),exp +1)) (0,0) bs) let unsigned_big = unsigned - + let signed v : integer = match most_significant v with | I -> 0 - (1 + (unsigned (bitwise_not v))) @@ -151,7 +219,7 @@ let signed v : integer = let signed_big = signed let to_num sign = if sign then signed else unsigned - + let max_64u = (integerPow 2 64) - 1 let max_64 = (integerPow 2 63) - 1 let min_64 = 0 - (integerPow 2 63) @@ -163,7 +231,7 @@ let min_8 = (0 - 128 : integer) let max_5 = (31 : integer) let min_5 = (0 - 32 : integer) -let get_max_representable_in sign (n : integer) : integer = +let get_max_representable_in sign (n : integer) : integer = if (n = 64) then match sign with | true -> max_64 | false -> max_64u end else if (n=32) then match sign with | true -> max_32 | false -> max_32u end else if (n=8) then max_8 @@ -172,7 +240,7 @@ let get_max_representable_in sign (n : integer) : integer = | false -> integerPow 2 (natFromInteger n) end -let get_min_representable_in _ (n : integer) : integer = +let get_min_representable_in _ (n : integer) : integer = if n = 64 then min_64 else if n = 32 then min_32 else if n = 8 then min_8 @@ -196,7 +264,7 @@ let rec add_one_bit bs co (i : integer) = | (I,false) -> add_one_bit (replace bs (i,O)) true (i-1) | (I,true) -> add_one_bit bs true (i-1) | _ -> failwith "add_one_bit applied to list with undefined bit" - (* | Vundef,_ -> assert false*) + (* | Vundef,_ -> assert false*) end let to_vec is_inc ((len : integer),(n : integer)) = @@ -212,7 +280,7 @@ let to_vec is_inc ((len : integer),(n : integer)) = Vector (add_one_bit bs false (len-1)) start is_inc let to_vec_big = to_vec - + let to_vec_inc = to_vec true let to_vec_dec = to_vec false @@ -221,7 +289,7 @@ let to_vec_undef is_inc (len : integer) = let to_vec_inc_undef = to_vec_undef true let to_vec_dec_undef = to_vec_undef false - + let exts (len, vec) = to_vec (get_dir vec) (len,signed vec) let extz (len, vec) = to_vec (get_dir vec) (len,unsigned vec) @@ -244,8 +312,8 @@ let arith_op_vec op sign (size : integer) (Vector _ _ is_inc as l) r = (* add_vec * add_vec_signed - * minus_vec - * multiply_vec + * minus_vec + * multiply_vec * multiply_vec_signed *) let add_VVV = arith_op_vec integerAdd false 1 @@ -259,8 +327,8 @@ let arith_op_vec_range op sign size (Vector _ _ is_inc as l) r = (* add_vec_range * add_vec_range_signed - * minus_vec_range - * mult_vec_range + * minus_vec_range + * mult_vec_range * mult_vec_range_signed *) let add_VIV = arith_op_vec_range integerAdd false 1 @@ -274,7 +342,7 @@ let arith_op_range_vec op sign size l (Vector _ _ is_inc as r) = (* add_range_vec * add_range_vec_signed - * minus_range_vec + * minus_range_vec * mult_range_vec * mult_range_vec_signed *) @@ -288,7 +356,7 @@ let arith_op_range_vec_range op sign l r = op l (to_num sign r) (* add_range_vec_range * add_range_vec_range_signed - * minus_range_vec_range + * minus_range_vec_range *) let add_IVI = arith_op_range_vec_range integerAdd false let addS_IVI = arith_op_range_vec_range integerAdd true @@ -306,7 +374,7 @@ let minus_VII = arith_op_vec_range_range integerMinus false -let arith_op_vec_vec_range op sign l r = +let arith_op_vec_vec_range op sign l r = let (l',r') = (to_num sign l,to_num sign r) in op l' r' @@ -320,7 +388,7 @@ 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 to_vec is_inc (length l * size,n) - + (* add_vec_bit * add_vec_bit_signed * minus_vec_bit_signed @@ -373,21 +441,21 @@ let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (siz let correct_size_num = to_vec is_inc (act_size,n) in let one_larger = to_vec is_inc (act_size + 1,nu) in let overflow = - if changed + if changed then if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size - then O else I + then O else I else I in (correct_size_num,overflow,most_significant one_larger) (* add_overflow_vec_bit_signed * minus_overflow_vec_bit - * minus_overflow_vec_bit_signed + * minus_overflow_vec_bit_signed *) let addSO_VBV = arith_op_overflow_vec_bit integerAdd true 1 let minusO_VBV = arith_op_overflow_vec_bit integerMinus false 1 let minusSO_VBV = arith_op_overflow_vec_bit integerMinus true 1 - + type shift = LL_shift | RR_shift | LLL_shift let shift_op_vec op ((Vector bs start is_inc as l),(n : integer)) = @@ -400,7 +468,7 @@ let shift_op_vec op ((Vector bs start is_inc as l),(n : integer)) = | RR_shift (*">>"*) -> let right_vec = slice l start n in let left_vec = Vector (List.replicate (natFromInteger n) O) 0 true in - vector_concat left_vec right_vec + vector_concat left_vec right_vec | LLL_shift (*"<<<"*) -> let left_vec = slice l n (if is_inc then len + start else start - len) in let right_vec = slice l start n in @@ -411,7 +479,7 @@ let bitwise_leftshift = shift_op_vec LL_shift (*"<<"*) let bitwise_rightshift = shift_op_vec RR_shift (*">>"*) let bitwise_rotate = shift_op_vec LLL_shift (*"<<<"*) -let rec arith_op_no0 (op : integer -> integer -> integer) l r = +let rec arith_op_no0 (op : integer -> integer -> integer) l r = if r = 0 then Nothing else Just (op l r) @@ -420,14 +488,14 @@ let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Vector let act_size = length l * size in let (l',r') = (to_num sign l,to_num sign r) in let n = arith_op_no0 op l' r' in - let (representable,n') = - match n with - | Just n' -> + let (representable,n') = + match n with + | Just n' -> (n' <= get_max_representable_in sign act_size && n' >= get_min_representable_in sign act_size, n') | _ -> (false,0) end in - if representable + if representable then to_vec is_inc (act_size,n') else Vector (List.replicate (natFromInteger act_size) Undef) start is_inc @@ -442,14 +510,14 @@ let arith_op_overflow_no0_vec op sign size ((Vector _ start is_inc) as l) r = let (l_u,r_u) = (to_num false l,to_num false r) in let n = arith_op_no0 op l' r' in let n_u = arith_op_no0 op l_u r_u in - let (representable,n',n_u') = - match (n, n_u) with - | (Just n',Just n_u') -> + let (representable,n',n_u') = + match (n, n_u) with + | (Just n',Just n_u') -> ((n' <= get_max_representable_in sign rep_size && n' >= (get_min_representable_in sign rep_size)), n', n_u') | _ -> (true,0,0) end in - let (correct_size_num,one_more) = + let (correct_size_num,one_more) = if representable then (to_vec is_inc (act_size,n'),to_vec is_inc (act_size + 1,n_u')) else @@ -474,7 +542,7 @@ let rec repeat xs n = if n = 0 then [] else xs ++ repeat xs (n-1) -let duplicate_bits (Vector bits start direction,len) = +let duplicate_bits (Vector bits start direction,len) = let bits' = repeat bits len in Vector bits' start direction @@ -486,7 +554,7 @@ let lteq = compare_op (<=) let gteq = compare_op (>=) -let compare_op_vec op sign (l,r) = +let compare_op_vec op sign (l,r) = let (l',r') = (to_num sign l, to_num sign r) in compare_op op (l',r') @@ -504,7 +572,7 @@ let gt_vec_unsigned = compare_op_vec (>) false let lteq_vec_unsigned = compare_op_vec (<=) false let gteq_vec_unsigned = compare_op_vec (>=) false -let compare_op_vec_range op sign (l,r) = +let compare_op_vec_range op sign (l,r) = compare_op op ((to_num sign l),r) let lt_vec_range = compare_op_vec_range (<) true @@ -571,9 +639,13 @@ val bitv_of_byte_lifteds : list Sail_impl_base.byte_lifted -> vector bitU let bitv_of_byte_lifteds v = Vector (foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v) 0 true +val bitv_of_bytes : list Sail_impl_base.byte -> vector bitU +let bitv_of_bytes v = + Vector (foldl (fun x (Byte y) -> x ++ (List.map bitU_of_bit y)) [] v) 0 true + val byte_lifteds_of_bitv : vector bitU -> list byte_lifted -let byte_lifteds_of_bitv (Vector bits length is_inc) = +let byte_lifteds_of_bitv (Vector bits length is_inc) = let bits = List.map bit_lifted_of_bitU bits in byte_lifteds_of_bit_lifteds bits @@ -590,7 +662,7 @@ let bitvFromRegisterValue v = val registerValueFromBitv : vector bitU -> register -> register_value -let registerValueFromBitv (Vector bits start is_inc) reg = +let registerValueFromBitv (Vector bits start is_inc) reg = let start = natFromInteger start in let bit_lifteds = List.map bit_lifted_of_bitU bits in @@ -604,7 +676,6 @@ class (ToNatural 'a) val toNatural : 'a -> natural end - instance (ToNatural integer) let toNatural = naturalFromInteger end @@ -632,7 +703,7 @@ let toNaturalFiveTup (n1,n2,n3,n4,n5) = val foreach_inc : forall 'vars. (integer * integer * integer) -> 'vars -> (integer -> 'vars -> 'vars) -> 'vars -let rec foreach_inc (i,stop,by) vars body = +let rec foreach_inc (i,stop,by) vars body = if i <= stop then let vars = body i vars in foreach_inc (i + by,stop,by) vars body @@ -640,7 +711,7 @@ let rec foreach_inc (i,stop,by) vars body = val foreach_dec : forall 'vars. (integer * integer * integer) -> 'vars -> (integer -> 'vars -> 'vars) -> 'vars -let rec foreach_dec (i,stop,by) vars body = +let rec foreach_dec (i,stop,by) vars body = if i >= stop then let vars = body i vars in foreach_dec (i - by,stop,by) vars body @@ -654,11 +725,13 @@ let assert' b msg_opt = if to_bool b then failwith msg else () + class (ToFromInterpValue 'a) val toInterpValue : 'a -> Interp.value val fromInterpValue : Interp.value -> 'a end + instance (ToFromInterpValue bool) let toInterpValue = function | true -> Interp.V_lit (L_aux (L_one) Unknown) @@ -731,7 +804,7 @@ let tuple3FromInterpValue = function | _ -> failwith "fromInterpValue a*b: unexpected value" end -instance forall 'a 'b 'c. ToFromInterpValue 'a, ToFromInterpValue 'b, ToFromInterpValue 'c => +instance forall 'a 'b 'c. ToFromInterpValue 'a, ToFromInterpValue 'b, ToFromInterpValue 'c => (ToFromInterpValue ('a * 'b * 'c)) let toInterpValue = tuple3ToInterpValue let fromInterpValue = tuple3FromInterpValue @@ -745,8 +818,8 @@ let tuple4FromInterpValue = function | _ -> failwith "fromInterpValue a*b: unexpected value" end -instance forall 'a 'b 'c 'd. ToFromInterpValue 'a, ToFromInterpValue 'b, - ToFromInterpValue 'c, ToFromInterpValue 'd => +instance forall 'a 'b 'c 'd. ToFromInterpValue 'a, ToFromInterpValue 'b, + ToFromInterpValue 'c, ToFromInterpValue 'd => (ToFromInterpValue ('a * 'b * 'c * 'd)) let toInterpValue = tuple4ToInterpValue let fromInterpValue = tuple4FromInterpValue @@ -761,8 +834,8 @@ let tuple5FromInterpValue = function | _ -> failwith "fromInterpValue a*b: unexpected value" end -instance forall 'a 'b 'c 'd 'e. - ToFromInterpValue 'a, ToFromInterpValue 'b, +instance forall 'a 'b 'c 'd 'e. + ToFromInterpValue 'a, ToFromInterpValue 'b, ToFromInterpValue 'c, ToFromInterpValue 'd, ToFromInterpValue 'e => (ToFromInterpValue ('a * 'b * 'c * 'd * 'e)) @@ -782,7 +855,7 @@ let tuple6FromInterpValue = function end instance forall 'a 'b 'c 'd 'e 'f. - ToFromInterpValue 'a, ToFromInterpValue 'b, + ToFromInterpValue 'a, ToFromInterpValue 'b, ToFromInterpValue 'c, ToFromInterpValue 'd, ToFromInterpValue 'e, ToFromInterpValue 'f => (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f)) @@ -802,7 +875,7 @@ let tuple7FromInterpValue = function end instance forall 'a 'b 'c 'd 'e 'f 'g. - ToFromInterpValue 'a, ToFromInterpValue 'b, + ToFromInterpValue 'a, ToFromInterpValue 'b, ToFromInterpValue 'c, ToFromInterpValue 'd, ToFromInterpValue 'e, ToFromInterpValue 'f, ToFromInterpValue 'g => @@ -824,7 +897,7 @@ let tuple8FromInterpValue = function end instance forall 'a 'b 'c 'd 'e 'f 'g 'h. - ToFromInterpValue 'a, ToFromInterpValue 'b, + ToFromInterpValue 'a, ToFromInterpValue 'b, ToFromInterpValue 'c, ToFromInterpValue 'd, ToFromInterpValue 'e, ToFromInterpValue 'f, ToFromInterpValue 'g, ToFromInterpValue 'h => @@ -846,7 +919,7 @@ let tuple9FromInterpValue = function end instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i. - ToFromInterpValue 'a, ToFromInterpValue 'b, + ToFromInterpValue 'a, ToFromInterpValue 'b, ToFromInterpValue 'c, ToFromInterpValue 'd, ToFromInterpValue 'e, ToFromInterpValue 'f, ToFromInterpValue 'g, ToFromInterpValue 'h, @@ -870,7 +943,7 @@ let tuple10FromInterpValue = function end instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j. - ToFromInterpValue 'a, ToFromInterpValue 'b, + ToFromInterpValue 'a, ToFromInterpValue 'b, ToFromInterpValue 'c, ToFromInterpValue 'd, ToFromInterpValue 'e, ToFromInterpValue 'f, ToFromInterpValue 'g, ToFromInterpValue 'h, @@ -894,7 +967,7 @@ let tuple11FromInterpValue = function end instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k. - ToFromInterpValue 'a, ToFromInterpValue 'b, + ToFromInterpValue 'a, ToFromInterpValue 'b, ToFromInterpValue 'c, ToFromInterpValue 'd, ToFromInterpValue 'e, ToFromInterpValue 'f, ToFromInterpValue 'g, ToFromInterpValue 'h, @@ -920,7 +993,7 @@ let tuple12FromInterpValue = function end instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l. - ToFromInterpValue 'a, ToFromInterpValue 'b, + ToFromInterpValue 'a, ToFromInterpValue 'b, ToFromInterpValue 'c, ToFromInterpValue 'd, ToFromInterpValue 'e, ToFromInterpValue 'f, ToFromInterpValue 'g, ToFromInterpValue 'h, @@ -972,7 +1045,7 @@ instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (vector 'a)) end (* Here the type information is not accurate: instead of T_id "option" it should - be T_app (T_id "option) (...), but temporarily we'll do it like this. The + be T_app (T_id "option") (...), but temporarily we'll do it like this. The same thing has to be fixed in pretty_print.ml when we're generating the type-class instances. *) val maybeToInterpValue : forall 'a. ToFromInterpValue 'a => maybe 'a -> Interp.value @@ -993,3 +1066,118 @@ instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (maybe 'a)) let fromInterpValue = maybeFromInterpValue end + +module SI = Interp +module SIA = Interp_ast + +let read_kindFromInterpValue = function + | SI.V_ctor (SIA.Id_aux (SIA.Id "Read_plain") _) _ _ v -> Read_plain + | SI.V_ctor (SIA.Id_aux (SIA.Id "Read_tag") _) _ _ v -> Read_tag + | SI.V_ctor (SIA.Id_aux (SIA.Id "Read_tag_reserve") _) _ _ v -> Read_tag_reserve + | SI.V_ctor (SIA.Id_aux (SIA.Id "Read_reserve") _) _ _ v -> Read_reserve + | SI.V_ctor (SIA.Id_aux (SIA.Id "Read_acquire") _) _ _ v -> Read_acquire + | SI.V_ctor (SIA.Id_aux (SIA.Id "Read_exclusive") _) _ _ v -> Read_exclusive + | SI.V_ctor (SIA.Id_aux (SIA.Id "Read_exclusive_acquire") _) _ _ v -> Read_exclusive_acquire + | SI.V_ctor (SIA.Id_aux (SIA.Id "Read_stream") _) _ _ v -> Read_stream + | _ -> failwith "fromInterpValue read_kind: unexpected value" + end + +let read_kindToInterpValue = function + | Read_plain -> SI.V_ctor (SIA.Id_aux (SIA.Id "Read_plain") SIA.Unknown) (SIA.T_id "read_kind") (SI.C_Enum 0) (toInterpValue ()) + | Read_tag -> SI.V_ctor (SIA.Id_aux (SIA.Id "Read_tag") SIA.Unknown) (SIA.T_id "read_kind") (SI.C_Enum 1) (toInterpValue ()) + | Read_tag_reserve -> SI.V_ctor (SIA.Id_aux (SIA.Id "Read_tag_reserve") SIA.Unknown) (SIA.T_id "read_kind") (SI.C_Enum 1) (toInterpValue ()) + | Read_reserve -> SI.V_ctor (SIA.Id_aux (SIA.Id "Read_reserve") SIA.Unknown) (SIA.T_id "read_kind") (SI.C_Enum 2) (toInterpValue ()) + | Read_acquire -> SI.V_ctor (SIA.Id_aux (SIA.Id "Read_acquire") SIA.Unknown) (SIA.T_id "read_kind") (SI.C_Enum 3) (toInterpValue ()) + | Read_exclusive -> SI.V_ctor (SIA.Id_aux (SIA.Id "Read_exclusive") SIA.Unknown) (SIA.T_id "read_kind") (SI.C_Enum 4) (toInterpValue ()) + | Read_exclusive_acquire -> SI.V_ctor (SIA.Id_aux (SIA.Id "Read_exclusive_acquire") SIA.Unknown) (SIA.T_id "read_kind") (SI.C_Enum 5) (toInterpValue ()) + | Read_stream -> SI.V_ctor (SIA.Id_aux (SIA.Id "Read_stream") SIA.Unknown) (SIA.T_id "read_kind") (SI.C_Enum 6) (toInterpValue ()) + end + +instance (ToFromInterpValue read_kind) + let toInterpValue = read_kindToInterpValue + let fromInterpValue = read_kindFromInterpValue +end + + +let write_kindFromInterpValue = function + | SI.V_ctor (SIA.Id_aux (SIA.Id "Write_plain") _) _ _ v -> Write_plain + | SI.V_ctor (SIA.Id_aux (SIA.Id "Write_tag") _) _ _ v -> Write_tag + | SI.V_ctor (SIA.Id_aux (SIA.Id "Write_tag_conditional") _) _ _ v -> Write_tag_conditional + | SI.V_ctor (SIA.Id_aux (SIA.Id "Write_conditional") _) _ _ v -> Write_conditional + | SI.V_ctor (SIA.Id_aux (SIA.Id "Write_release") _) _ _ v -> Write_release + | SI.V_ctor (SIA.Id_aux (SIA.Id "Write_exclusive") _) _ _ v -> Write_exclusive + | SI.V_ctor (SIA.Id_aux (SIA.Id "Write_exclusive_release") _) _ _ v -> Write_exclusive_release + | _ -> failwith "fromInterpValue write_kind: unexpected value " + end + +let write_kindToInterpValue = function + | Write_plain -> SI.V_ctor (SIA.Id_aux (SIA.Id "Write_plain") SIA.Unknown) (SIA.T_id "write_kind") (SI.C_Enum 0) (toInterpValue ()) + | Write_tag -> SI.V_ctor (SIA.Id_aux (SIA.Id "Write_tag") SIA.Unknown) (SIA.T_id "write_kind") (SI.C_Enum 1) (toInterpValue ()) + | Write_tag_conditional -> SI.V_ctor (SIA.Id_aux (SIA.Id "Write_tag_conditional") SIA.Unknown) (SIA.T_id "write_kind") (SI.C_Enum 1) (toInterpValue ()) + | Write_conditional -> SI.V_ctor (SIA.Id_aux (SIA.Id "Write_conditional") SIA.Unknown) (SIA.T_id "write_kind") (SI.C_Enum 2) (toInterpValue ()) + | Write_release -> SI.V_ctor (SIA.Id_aux (SIA.Id "Write_release") SIA.Unknown) (SIA.T_id "write_kind") (SI.C_Enum 3) (toInterpValue ()) + | Write_exclusive -> SI.V_ctor (SIA.Id_aux (SIA.Id "Write_exclusive") SIA.Unknown) (SIA.T_id "write_kind") (SI.C_Enum 4) (toInterpValue ()) + | Write_exclusive_release -> SI.V_ctor (SIA.Id_aux (SIA.Id "Write_exclusive_release") SIA.Unknown) (SIA.T_id "write_kind") (SI.C_Enum 5) (toInterpValue ()) + end + +instance (ToFromInterpValue write_kind) + let toInterpValue = write_kindToInterpValue + let fromInterpValue = write_kindFromInterpValue +end + +let barrier_kindFromInterpValue = function + | SI.V_ctor (SIA.Id_aux (SIA.Id "Barrier_Sync") _) _ _ v -> Barrier_Sync + | SI.V_ctor (SIA.Id_aux (SIA.Id "Barrier_LwSync") _) _ _ v -> Barrier_LwSync + | SI.V_ctor (SIA.Id_aux (SIA.Id "Barrier_Eieio") _) _ _ v -> Barrier_Eieio + | SI.V_ctor (SIA.Id_aux (SIA.Id "Barrier_Isync") _) _ _ v -> Barrier_Isync + | SI.V_ctor (SIA.Id_aux (SIA.Id "Barrier_DMB") _) _ _ v -> Barrier_DMB + | SI.V_ctor (SIA.Id_aux (SIA.Id "Barrier_DMB_ST") _) _ _ v -> Barrier_DMB_ST + | SI.V_ctor (SIA.Id_aux (SIA.Id "Barrier_DMB_LD") _) _ _ v -> Barrier_DMB_LD + | SI.V_ctor (SIA.Id_aux (SIA.Id "Barrier_DSB") _) _ _ v -> Barrier_DSB + | SI.V_ctor (SIA.Id_aux (SIA.Id "Barrier_DSB_ST") _) _ _ v -> Barrier_DSB_ST + | SI.V_ctor (SIA.Id_aux (SIA.Id "Barrier_DSB_LD") _) _ _ v -> Barrier_DSB_LD + | SI.V_ctor (SIA.Id_aux (SIA.Id "Barrier_ISB") _) _ _ v -> Barrier_ISB + | _ -> failwith "fromInterpValue barrier_kind: unexpected value" + end + +let barrier_kindToInterpValue = function + | Barrier_Sync -> SI.V_ctor (SIA.Id_aux (SIA.Id "Barrier_Sync") SIA.Unknown) (SIA.T_id "barrier_kind") (SI.C_Enum 0) (toInterpValue ()) + | Barrier_LwSync -> SI.V_ctor (SIA.Id_aux (SIA.Id "Barrier_LwSync") SIA.Unknown) (SIA.T_id "barrier_kind") (SI.C_Enum 1) (toInterpValue ()) + | Barrier_Eieio -> SI.V_ctor (SIA.Id_aux (SIA.Id "Barrier_Eieio") SIA.Unknown) (SIA.T_id "barrier_kind") (SI.C_Enum 2) (toInterpValue ()) + | Barrier_Isync -> SI.V_ctor (SIA.Id_aux (SIA.Id "Barrier_Isync") SIA.Unknown) (SIA.T_id "barrier_kind") (SI.C_Enum 3) (toInterpValue ()) + | Barrier_DMB -> SI.V_ctor (SIA.Id_aux (SIA.Id "Barrier_DMB") SIA.Unknown) (SIA.T_id "barrier_kind") (SI.C_Enum 4) (toInterpValue ()) + | Barrier_DMB_ST -> SI.V_ctor (SIA.Id_aux (SIA.Id "Barrier_DMB_ST") SIA.Unknown) (SIA.T_id "barrier_kind") (SI.C_Enum 5) (toInterpValue ()) + | Barrier_DMB_LD -> SI.V_ctor (SIA.Id_aux (SIA.Id "Barrier_DMB_LD") SIA.Unknown) (SIA.T_id "barrier_kind") (SI.C_Enum 6) (toInterpValue ()) + | Barrier_DSB -> SI.V_ctor (SIA.Id_aux (SIA.Id "Barrier_DSB") SIA.Unknown) (SIA.T_id "barrier_kind") (SI.C_Enum 7) (toInterpValue ()) + | Barrier_DSB_ST -> SI.V_ctor (SIA.Id_aux (SIA.Id "Barrier_DSB_ST") SIA.Unknown) (SIA.T_id "barrier_kind") (SI.C_Enum 8) (toInterpValue ()) + | Barrier_DSB_LD -> SI.V_ctor (SIA.Id_aux (SIA.Id "Barrier_DSB_LD") SIA.Unknown) (SIA.T_id "barrier_kind") (SI.C_Enum 9) (toInterpValue ()) + | Barrier_ISB -> SI.V_ctor (SIA.Id_aux (SIA.Id "Barrier_ISB") SIA.Unknown) (SIA.T_id "barrier_kind") (SI.C_Enum 10) (toInterpValue ()) + end + +instance (ToFromInterpValue barrier_kind) + let toInterpValue = barrier_kindToInterpValue + let fromInterpValue = barrier_kindFromInterpValue +end + + +let instruction_kindFromInterpValue = function + | SI.V_ctor (SIA.Id_aux (SIA.Id "IK_barrier") _) _ _ v -> IK_barrier (fromInterpValue v) + | SI.V_ctor (SIA.Id_aux (SIA.Id "IK_mem_read") _) _ _ v -> IK_mem_read (fromInterpValue v) + | SI.V_ctor (SIA.Id_aux (SIA.Id "IK_mem_write") _) _ _ v -> IK_mem_write (fromInterpValue v) + | SI.V_ctor (SIA.Id_aux (SIA.Id "IK_cond_branch") _) _ _ v -> IK_cond_branch + | SI.V_ctor (SIA.Id_aux (SIA.Id "IK_simple") _) _ _ v -> IK_simple + | _ -> failwith "fromInterpValue instruction_kind: unexpected value" + end + +let instruction_kindToInterpValue = function + | IK_barrier v -> SI.V_ctor (SIA.Id_aux (SIA.Id "IK_barrier") SIA.Unknown) (SIA.T_id "instruction_kind") SI.C_Union (toInterpValue v) + | IK_mem_read v -> SI.V_ctor (SIA.Id_aux (SIA.Id "IK_mem_read") SIA.Unknown) (SIA.T_id "instruction_kind") SI.C_Union (toInterpValue v) + | IK_mem_write v -> SI.V_ctor (SIA.Id_aux (SIA.Id "IK_mem_write") SIA.Unknown) (SIA.T_id "instruction_kind") SI.C_Union (toInterpValue v) + | IK_cond_branch -> SI.V_ctor (SIA.Id_aux (SIA.Id "IK_cond_branch") SIA.Unknown) (SIA.T_id "instruction_kind") SI.C_Union (toInterpValue ()) + | IK_simple -> SI.V_ctor (SIA.Id_aux (SIA.Id "IK_simple") SIA.Unknown) (SIA.T_id "instruction_kind") SI.C_Union (toInterpValue ()) + end + +instance (ToFromInterpValue instruction_kind) + let toInterpValue = instruction_kindToInterpValue + let fromInterpValue = instruction_kindFromInterpValue +end diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem deleted file mode 100644 index 07238180..00000000 --- a/src/gen_lib/vector.lem +++ /dev/null @@ -1,59 +0,0 @@ -open import Pervasives_extra - -(* element list * start * has increasing direction *) -type vector 'a = Vector of list 'a * integer * bool - -let rec nth xs (n : integer) = - match xs with - | x :: xs -> if n = 0 then x else nth xs (n - 1) - | _ -> failwith "nth applied to empty list" - end - - -let get_dir (Vector _ _ ord) = ord -let get_start (Vector _ s _) = s -let length (Vector bs _ _) = integerFromNat (length bs) - -let rec replace bs ((n : integer),b') = match bs with - | [] -> [] - | b :: bs -> - if n = 0 then - b' :: bs - else - b :: replace bs (n - 1,b') - end - -let vector_concat (Vector bs start is_inc) (Vector bs' _ _) = - Vector (bs ++ bs') start is_inc - -let (^^) = vector_concat - -val slice : forall 'a. vector 'a -> integer -> integer -> vector 'a -let slice (Vector bs start is_inc) n m = - let n = natFromInteger n in - let m = natFromInteger m in - let start = natFromInteger start in - let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in - let (_,suffix) = List.splitAt offset bs in - let (subvector,_) = List.splitAt length suffix in - let n = integerFromNat n in - Vector subvector n is_inc - -val update : forall 'a. vector 'a -> integer -> integer -> vector 'a -> vector 'a -let update (Vector bs start is_inc) n m (Vector bs' _ _) = - let n = natFromInteger n in - let m = natFromInteger m in - let start = natFromInteger start in - let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in - let (prefix,_) = List.splitAt offset bs in - let (_,suffix) = List.splitAt (offset + length) bs in - let start = integerFromNat start in - Vector (prefix ++ (List.take length bs') ++ suffix) start is_inc - -val access : forall 'a. vector 'a -> integer -> 'a -let access (Vector bs start is_inc) n = - if is_inc then nth bs (n - start) else nth bs (start - n) - -val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a -let update_pos v n b = - update v n n (Vector [b] 0 true) diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index cbde6e8b..cdfde00b 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -14,6 +14,7 @@ open import Instruction_extractor type tannot = Interp_utilities.tannot + val debug_print : string -> unit declare ocaml target_rep function debug_print s = `Printf.eprintf` "%s" s diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 340904f2..dad84a5c 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -524,17 +524,17 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | Interp.V_ctor (Id_aux (Id "IK_barrier") _) _ _ (Interp.V_ctor (Id_aux (Id b) _) _ _ _) -> IK_barrier (match b with - | "Barrier_Sync" -> Sync - | "Barrier_LwSync" -> LwSync - | "Barrier_Eieio" -> Eieio - | "Barrier_Isync" -> Isync - | "Barrier_DMB" -> DMB - | "Barrier_DMB_ST" -> DMB_ST - | "Barrier_DMB_LD" -> DMB_LD - | "Barrier_DSB" -> DSB - | "Barrier_DSB_ST" -> DSB_ST - | "Barrier_DSB_LD" -> DSB_LD - | "Barrier_ISB" -> ISB + | "Barrier_Sync" -> Barrier_Sync + | "Barrier_LwSync" -> Barrier_LwSync + | "Barrier_Eieio" -> Barrier_Eieio + | "Barrier_Isync" -> Barrier_Isync + | "Barrier_DMB" -> Barrier_DMB + | "Barrier_DMB_ST" -> Barrier_DMB_ST + | "Barrier_DMB_LD" -> Barrier_DMB_LD + | "Barrier_DSB" -> Barrier_DSB + | "Barrier_DSB_ST" -> Barrier_DSB_ST + | "Barrier_DSB_LD" -> Barrier_DSB_LD + | "Barrier_ISB" -> Barrier_ISB end) | Interp.V_ctor (Id_aux (Id "IK_mem_read") _) _ _ (Interp.V_ctor (Id_aux (Id r) _) _ _ _) -> @@ -620,7 +620,7 @@ let interp_value_to_instr_external top_level instr = end -let decode_to_istate top_level registers value = +let decode_to_instruction top_level registers value : instruction_or_decode_error = let mode = make_interpreter_mode true false in let (Context ((Interp.Env _ instructions _ _ _ _ _ _) as top_env) direction _ _ _ _ _ _) = top_level in let intern_val = intern_opcode direction value in @@ -637,7 +637,6 @@ let decode_to_istate top_level registers value = match (instr_decoded_error) with | Ivh_value instr -> let instr_external = interp_value_to_instr_external top_level instr in - let (arg,_) = Interp.to_exp mode Interp.eenv instr in let (instr_decoded_error,events) = interp_to_value_helper (Just value) Ivh_unsupported val_str instr_external internal_direction registers [] false @@ -648,27 +647,29 @@ let decode_to_istate top_level registers value = (Interp_ast.Unknown, Nothing)) top_env Interp.eenv (Interp.emem "decode second top level") Interp.Top) Nothing) in match (instr_decoded_error) with - | Ivh_value instr -> - (*let (arg,_) = Interp.to_exp mode Interp.eenv instr in*) - Instr instr_external - (IState (Interp.Thunk_frame - (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown,Nothing)) - top_env Interp.eenv (Interp.emem "execute") Interp.Top) - top_level) + | Ivh_value instr -> IDE_instr instr_external instr | Ivh_value_after_exn v -> Assert_extra.failwith "supported_instructions called exit, so support will be needed for that now" - | Ivh_error err -> Decode_error err + | Ivh_error err -> IDE_decode_error err end | Ivh_value_after_exn _ -> - Assert_extra.failwith ("Decode of " ^ val_str ^ " called exit.") - | Ivh_error err -> Decode_error err + Assert_extra.failwith ("Decode of " ^ val_str ^ " called exit.") + | Ivh_error err -> IDE_decode_error err end -let decode_to_instruction (top_level:context) registers (value:opcode) : instruction_or_decode_error = - match decode_to_istate top_level registers value with - | Instr inst is -> IDE_instr inst - | Decode_error de -> IDE_decode_error de +let decode_to_istate (top_level:context) registers (value:opcode) : i_state_or_error = + let (Context top_env _ _ _ _ _ _ _) = top_level in + match decode_to_instruction top_level registers value with + | IDE_instr instr instrv -> + let mode = make_interpreter_mode true false in + let (arg,_) = Interp.to_exp mode Interp.eenv instrv in + Instr instr + (IState (Interp.Thunk_frame + (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown,Nothing)) + top_env Interp.eenv (Interp.emem "execute") Interp.Top) + top_level) + | IDE_decode_error de -> Decode_error de end @@ -840,8 +841,8 @@ let interp mode (IState interp_state context) = | (o,_) -> o end -val state_to_outcome_s : forall 'v. interp_mode -> instruction_state -> Sail_impl_base.outcome_s instruction_state unit unit -val outcome_to_outcome : interp_mode -> Interp_interface.outcome -> Sail_impl_base.outcome instruction_state unit unit +val state_to_outcome_s : forall 'v. interp_mode -> instruction_state -> Sail_impl_base.outcome_s instruction_state unit +val outcome_to_outcome : interp_mode -> Interp_interface.outcome -> Sail_impl_base.outcome instruction_state unit let rec outcome_to_outcome mode = function | Interp_interface.Read_mem rk addr size _ k -> Sail_impl_base.Read_mem (rk,addr,size) (fun v -> state_to_outcome_s mode (k v)) @@ -862,7 +863,7 @@ let rec outcome_to_outcome mode = function | Interp_interface.Nondet_choice _ _ -> failwith "Nondet_choice not supported yet" | Interp_interface.Escape maybestate _ -> - Sail_impl_base.Escape (Maybe.map (state_to_outcome_s mode) maybestate) + Sail_impl_base.Escape Nothing (Maybe.map (state_to_outcome_s mode) maybestate) | Interp_interface.Fail maybestring -> Sail_impl_base.Fail maybestring | Interp_interface.Internal maybestring maybeprint state -> diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index cf8c51a2..a648b437 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -156,6 +156,10 @@ val build_context : specification -> memory_reads -> memory_writes -> memory_wri val initial_instruction_state : context -> string -> list register_value -> instruction_state (* string is a function name, list of value are the parameters to that function *) +type instruction_or_decode_error = + | IDE_instr of instruction * Interp.value + | IDE_decode_error of decode_error + (** propose to remove the following type and use the above instead *) type i_state_or_error = | Instr of instruction * instruction_state @@ -198,4 +202,4 @@ val instruction_analysis : -> maybe (list (reg_name * register_value)) -> instruction -> (list reg_name * list reg_name * list reg_name * list nia * dia * instruction_kind) -val initial_outcome_s_of_instruction : context -> interp_mode -> instruction -> Sail_impl_base.outcome_s instruction_state string unit +val initial_outcome_s_of_instruction : context -> interp_mode -> instruction -> Sail_impl_base.outcome_s instruction_state unit diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 4587004f..81d84dec 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -398,9 +398,10 @@ type write_kind = type barrier_kind = (* Power barriers *) - Sync | LwSync | Eieio | Isync + Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync (* AArch64 barriers *) - | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB + | Barrier_DMB | Barrier_DMB_ST | Barrier_DMB_LD | Barrier_DSB + | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB type instruction_kind = | IK_barrier of barrier_kind @@ -414,30 +415,30 @@ they just have particular nias (and will be IK_simple *) | IK_simple (* the address_lifted types should go away here and be replaced by address *) -type outcome 's 'e 'a = +type outcome 's 'a = (* Request to read memory, value is location to read, integer is size to read, followed by registers that were used in computing that size *) - | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> outcome_s 's 'e 'a) + | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> outcome_s 's 'a) (* Tell the system a write is imminent, at address lifted, of size nat *) - | Write_ea of (write_kind * address_lifted * nat) * outcome_s 's 'e 'a + | Write_ea of (write_kind * address_lifted * nat) * outcome_s 's 'a (* Request to write memory at last signalled address. Memory value should be 8 times the size given in ea signal *) - | Write_memv of memory_value * (bool -> outcome_s 's 'e 'a) + | Write_memv of memory_value * (bool -> outcome_s 's 'a) (* Request a memory barrier *) - | Barrier of barrier_kind * outcome_s 's 'e 'a + | Barrier of barrier_kind * outcome_s 's 'a (* Tell the system to dynamically recalculate dependency footprint *) - | Footprint of outcome_s 's 'e 'a + | Footprint of outcome_s 's 'a (* Request to read register, will track dependency when mode.track_values *) - | Read_reg of reg_name * (register_value -> outcome_s 's 'e 'a) + | Read_reg of reg_name * (register_value -> outcome_s 's 'a) (* Request to write register *) - | Write_reg of (reg_name * register_value) * (outcome_s 's 'e 'a) - | Escape of maybe (outcome_s 's 'e 'e) + | Write_reg of (reg_name * register_value) * (outcome_s 's 'a) + | Escape of maybe string * maybe (outcome_s 's unit) (*Result of a failed assert with possible error message to report*) | Fail of maybe string - | Internal of (maybe string * maybe (unit -> string)) * outcome_s 's 'e 'a + | Internal of (maybe string * maybe (unit -> string)) * outcome_s 's 'a | Done of 'a | Error of string - and outcome_s 's 'e 'a = outcome 's 'e 'a * maybe 's + and outcome_s 's 'a = outcome 's 'a * maybe 's let ~{ocaml} read_kindCompare rk1 rk2 = match (rk1, rk2) with @@ -613,137 +614,137 @@ end let ~{ocaml} barrier_kindCompare bk1 bk2 = match (bk1, bk2) with - | (Sync, Sync) -> EQ - | (Sync, LwSync) -> LT - | (Sync, Eieio) -> LT - | (Sync, Isync) -> LT - | (Sync, DMB) -> LT - | (Sync, DMB_ST) -> LT - | (Sync, DMB_LD) -> LT - | (Sync, DSB) -> LT - | (Sync, DSB_ST) -> LT - | (Sync, DSB_LD) -> LT - | (Sync, ISB) -> LT - - | (LwSync, Sync) -> GT - | (LwSync, LwSync) -> EQ - | (LwSync, Eieio) -> LT - | (LwSync, Isync) -> LT - | (LwSync, DMB) -> LT - | (LwSync, DMB_ST) -> LT - | (LwSync, DMB_LD) -> LT - | (LwSync, DSB) -> LT - | (LwSync, DSB_ST) -> LT - | (LwSync, DSB_LD) -> LT - | (LwSync, ISB) -> LT - - | (Eieio, Sync) -> GT - | (Eieio, LwSync) -> GT - | (Eieio, Eieio) -> EQ - | (Eieio, Isync) -> LT - | (Eieio, DMB) -> LT - | (Eieio, DMB_ST) -> LT - | (Eieio, DMB_LD) -> LT - | (Eieio, DSB) -> LT - | (Eieio, DSB_ST) -> LT - | (Eieio, DSB_LD) -> LT - | (Eieio, ISB) -> LT - - | (Isync, Sync) -> GT - | (Isync, LwSync) -> GT - | (Isync, Eieio) -> GT - | (Isync, Isync) -> EQ - | (Isync, DMB) -> LT - | (Isync, DMB_ST) -> LT - | (Isync, DMB_LD) -> LT - | (Isync, DSB) -> LT - | (Isync, DSB_ST) -> LT - | (Isync, DSB_LD) -> LT - | (Isync, ISB) -> LT - - | (DMB, Sync) -> GT - | (DMB, LwSync) -> GT - | (DMB, Eieio) -> GT - | (DMB, Isync) -> GT - | (DMB, DMB) -> EQ - | (DMB, DMB_ST) -> LT - | (DMB, DMB_LD) -> LT - | (DMB, DSB) -> LT - | (DMB, DSB_ST) -> LT - | (DMB, DSB_LD) -> LT - | (DMB, ISB) -> LT - - | (DMB_ST, Sync) -> GT - | (DMB_ST, LwSync) -> GT - | (DMB_ST, Eieio) -> GT - | (DMB_ST, Isync) -> GT - | (DMB_ST, DMB) -> GT - | (DMB_ST, DMB_ST) -> EQ - | (DMB_ST, DMB_LD) -> LT - | (DMB_ST, DSB) -> LT - | (DMB_ST, DSB_ST) -> LT - | (DMB_ST, DSB_LD) -> LT - | (DMB_ST, ISB) -> LT - - | (DMB_LD, Sync) -> GT - | (DMB_LD, LwSync) -> GT - | (DMB_LD, Eieio) -> GT - | (DMB_LD, Isync) -> GT - | (DMB_LD, DMB) -> GT - | (DMB_LD, DMB_ST) -> GT - | (DMB_LD, DMB_LD) -> EQ - | (DMB_LD, DSB) -> LT - | (DMB_LD, DSB_ST) -> LT - | (DMB_LD, DSB_LD) -> LT - | (DMB_LD, ISB) -> LT - - | (DSB, Sync) -> GT - | (DSB, LwSync) -> GT - | (DSB, Eieio) -> GT - | (DSB, Isync) -> GT - | (DSB, DMB) -> GT - | (DSB, DMB_ST) -> GT - | (DSB, DMB_LD) -> GT - | (DSB, DSB) -> EQ - | (DSB, DSB_ST) -> LT - | (DSB, DSB_LD) -> LT - | (DSB, ISB) -> LT - - | (DSB_ST, Sync) -> GT - | (DSB_ST, LwSync) -> GT - | (DSB_ST, Eieio) -> GT - | (DSB_ST, Isync) -> GT - | (DSB_ST, DMB) -> GT - | (DSB_ST, DMB_ST) -> GT - | (DSB_ST, DMB_LD) -> GT - | (DSB_ST, DSB) -> GT - | (DSB_ST, DSB_ST) -> EQ - | (DSB_ST, DSB_LD) -> LT - | (DSB_ST, ISB) -> LT - - | (DSB_LD, Sync) -> GT - | (DSB_LD, LwSync) -> GT - | (DSB_LD, Eieio) -> GT - | (DSB_LD, Isync) -> GT - | (DSB_LD, DMB) -> GT - | (DSB_LD, DMB_ST) -> GT - | (DSB_LD, DMB_LD) -> GT - | (DSB_LD, DSB) -> GT - | (DSB_LD, DSB_ST) -> GT - | (DSB_LD, DSB_LD) -> EQ - | (DSB_LD, ISB) -> LT + | (Barrier_Sync, Barrier_Sync) -> EQ + | (Barrier_Sync, Barrier_LwSync) -> LT + | (Barrier_Sync, Barrier_Eieio) -> LT + | (Barrier_Sync, Barrier_Isync) -> LT + | (Barrier_Sync, Barrier_DMB) -> LT + | (Barrier_Sync, Barrier_DMB_ST) -> LT + | (Barrier_Sync, Barrier_DMB_LD) -> LT + | (Barrier_Sync, Barrier_DSB) -> LT + | (Barrier_Sync, Barrier_DSB_ST) -> LT + | (Barrier_Sync, Barrier_DSB_LD) -> LT + | (Barrier_Sync, Barrier_ISB) -> LT + + | (Barrier_LwSync, Barrier_Sync) -> GT + | (Barrier_LwSync, Barrier_LwSync) -> EQ + | (Barrier_LwSync, Barrier_Eieio) -> LT + | (Barrier_LwSync, Barrier_Isync) -> LT + | (Barrier_LwSync, Barrier_DMB) -> LT + | (Barrier_LwSync, Barrier_DMB_ST) -> LT + | (Barrier_LwSync, Barrier_DMB_LD) -> LT + | (Barrier_LwSync, Barrier_DSB) -> LT + | (Barrier_LwSync, Barrier_DSB_ST) -> LT + | (Barrier_LwSync, Barrier_DSB_LD) -> LT + | (Barrier_LwSync, Barrier_ISB) -> LT + + | (Barrier_Eieio, Barrier_Sync) -> GT + | (Barrier_Eieio, Barrier_LwSync) -> GT + | (Barrier_Eieio, Barrier_Eieio) -> EQ + | (Barrier_Eieio, Barrier_Isync) -> LT + | (Barrier_Eieio, Barrier_DMB) -> LT + | (Barrier_Eieio, Barrier_DMB_ST) -> LT + | (Barrier_Eieio, Barrier_DMB_LD) -> LT + | (Barrier_Eieio, Barrier_DSB) -> LT + | (Barrier_Eieio, Barrier_DSB_ST) -> LT + | (Barrier_Eieio, Barrier_DSB_LD) -> LT + | (Barrier_Eieio, Barrier_ISB) -> LT + + | (Barrier_Isync, Barrier_Sync) -> GT + | (Barrier_Isync, Barrier_LwSync) -> GT + | (Barrier_Isync, Barrier_Eieio) -> GT + | (Barrier_Isync, Barrier_Isync) -> EQ + | (Barrier_Isync, Barrier_DMB) -> LT + | (Barrier_Isync, Barrier_DMB_ST) -> LT + | (Barrier_Isync, Barrier_DMB_LD) -> LT + | (Barrier_Isync, Barrier_DSB) -> LT + | (Barrier_Isync, Barrier_DSB_ST) -> LT + | (Barrier_Isync, Barrier_DSB_LD) -> LT + | (Barrier_Isync, Barrier_ISB) -> LT + + | (Barrier_DMB, Barrier_Sync) -> GT + | (Barrier_DMB, Barrier_LwSync) -> GT + | (Barrier_DMB, Barrier_Eieio) -> GT + | (Barrier_DMB, Barrier_Isync) -> GT + | (Barrier_DMB, Barrier_DMB) -> EQ + | (Barrier_DMB, Barrier_DMB_ST) -> LT + | (Barrier_DMB, Barrier_DMB_LD) -> LT + | (Barrier_DMB, Barrier_DSB) -> LT + | (Barrier_DMB, Barrier_DSB_ST) -> LT + | (Barrier_DMB, Barrier_DSB_LD) -> LT + | (Barrier_DMB, Barrier_ISB) -> LT + + | (Barrier_DMB_ST, Barrier_Sync) -> GT + | (Barrier_DMB_ST, Barrier_LwSync) -> GT + | (Barrier_DMB_ST, Barrier_Eieio) -> GT + | (Barrier_DMB_ST, Barrier_Isync) -> GT + | (Barrier_DMB_ST, Barrier_DMB) -> GT + | (Barrier_DMB_ST, Barrier_DMB_ST) -> EQ + | (Barrier_DMB_ST, Barrier_DMB_LD) -> LT + | (Barrier_DMB_ST, Barrier_DSB) -> LT + | (Barrier_DMB_ST, Barrier_DSB_ST) -> LT + | (Barrier_DMB_ST, Barrier_DSB_LD) -> LT + | (Barrier_DMB_ST, Barrier_ISB) -> LT + + | (Barrier_DMB_LD, Barrier_Sync) -> GT + | (Barrier_DMB_LD, Barrier_LwSync) -> GT + | (Barrier_DMB_LD, Barrier_Eieio) -> GT + | (Barrier_DMB_LD, Barrier_Isync) -> GT + | (Barrier_DMB_LD, Barrier_DMB) -> GT + | (Barrier_DMB_LD, Barrier_DMB_ST) -> GT + | (Barrier_DMB_LD, Barrier_DMB_LD) -> EQ + | (Barrier_DMB_LD, Barrier_DSB) -> LT + | (Barrier_DMB_LD, Barrier_DSB_ST) -> LT + | (Barrier_DMB_LD, Barrier_DSB_LD) -> LT + | (Barrier_DMB_LD, Barrier_ISB) -> LT + + | (Barrier_DSB, Barrier_Sync) -> GT + | (Barrier_DSB, Barrier_LwSync) -> GT + | (Barrier_DSB, Barrier_Eieio) -> GT + | (Barrier_DSB, Barrier_Isync) -> GT + | (Barrier_DSB, Barrier_DMB) -> GT + | (Barrier_DSB, Barrier_DMB_ST) -> GT + | (Barrier_DSB, Barrier_DMB_LD) -> GT + | (Barrier_DSB, Barrier_DSB) -> EQ + | (Barrier_DSB, Barrier_DSB_ST) -> LT + | (Barrier_DSB, Barrier_DSB_LD) -> LT + | (Barrier_DSB, Barrier_ISB) -> LT + + | (Barrier_DSB_ST, Barrier_Sync) -> GT + | (Barrier_DSB_ST, Barrier_LwSync) -> GT + | (Barrier_DSB_ST, Barrier_Eieio) -> GT + | (Barrier_DSB_ST, Barrier_Isync) -> GT + | (Barrier_DSB_ST, Barrier_DMB) -> GT + | (Barrier_DSB_ST, Barrier_DMB_ST) -> GT + | (Barrier_DSB_ST, Barrier_DMB_LD) -> GT + | (Barrier_DSB_ST, Barrier_DSB) -> GT + | (Barrier_DSB_ST, Barrier_DSB_ST) -> EQ + | (Barrier_DSB_ST, Barrier_DSB_LD) -> LT + | (Barrier_DSB_ST, Barrier_ISB) -> LT + + | (Barrier_DSB_LD, Barrier_Sync) -> GT + | (Barrier_DSB_LD, Barrier_LwSync) -> GT + | (Barrier_DSB_LD, Barrier_Eieio) -> GT + | (Barrier_DSB_LD, Barrier_Isync) -> GT + | (Barrier_DSB_LD, Barrier_DMB) -> GT + | (Barrier_DSB_LD, Barrier_DMB_ST) -> GT + | (Barrier_DSB_LD, Barrier_DMB_LD) -> GT + | (Barrier_DSB_LD, Barrier_DSB) -> GT + | (Barrier_DSB_LD, Barrier_DSB_ST) -> GT + | (Barrier_DSB_LD, Barrier_DSB_LD) -> EQ + | (Barrier_DSB_LD, Barrier_ISB) -> LT - | (ISB, Sync) -> GT - | (ISB, LwSync) -> GT - | (ISB, Eieio) -> GT - | (ISB, Isync) -> GT - | (ISB, DMB) -> GT - | (ISB, DMB_ST) -> GT - | (ISB, DMB_LD) -> GT - | (ISB, DSB) -> GT - | (ISB, DSB_ST) -> GT - | (ISB, DSB_LD) -> GT - | (ISB, ISB) -> EQ + | (Barrier_ISB, Barrier_Sync) -> GT + | (Barrier_ISB, Barrier_LwSync) -> GT + | (Barrier_ISB, Barrier_Eieio) -> GT + | (Barrier_ISB, Barrier_Isync) -> GT + | (Barrier_ISB, Barrier_DMB) -> GT + | (Barrier_ISB, Barrier_DMB_ST) -> GT + | (Barrier_ISB, Barrier_DMB_LD) -> GT + | (Barrier_ISB, Barrier_DSB) -> GT + | (Barrier_ISB, Barrier_DSB_ST) -> GT + | (Barrier_ISB, Barrier_DSB_LD) -> GT + | (Barrier_ISB, Barrier_ISB) -> EQ end let inline {ocaml} barrier_kindCompare = defaultCompare @@ -820,16 +821,6 @@ let inline ~{coq} instructionEqual = unsafe_structural_equality let {coq} instructionInequal i1 i2 = not (instructionEqual i1 i2) let inline ~{coq} instructionInequal = unsafe_structural_inequality -type decode_error = - | Unsupported_instruction_error of instruction - | Not_an_instruction_error of opcode - | Internal_error of string - -type instruction_or_decode_error = - | IDE_instr of instruction - | IDE_decode_error of decode_error - - (** operations and coercions on basic values *) val word8_to_bitls : word8 -> list bit_lifted @@ -1364,3 +1355,13 @@ end type v_kind = Bitv | Bytev + + +type decode_error = + | Unsupported_instruction_error of instruction + | Not_an_instruction_error of opcode + | Internal_error of string + + + + diff --git a/src/pretty_print.ml b/src/pretty_print.ml index bc9791de..244a7263 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -32,7 +32,7 @@ let lemnum default n = match n with | 5 -> "five" | 6 -> "six" | 7 -> "seven" - | 8 -> "eight" + | 8 -> "eight" | 15 -> "fifteen" | 16 -> "sixteen" | 20 -> "twenty" @@ -69,7 +69,7 @@ let rec pp_format_l_lem = function (* | Parse_ast.Int(s,None) -> "(Int \"" ^ s ^ "\" Nothing)" | Parse_ast.Int(s,(Some l)) -> "(Int \"" ^ s ^ "\" (Just " ^ (pp_format_l_lem l) ^ "))" | Parse_ast.Range(p1,p2) -> "(Range \"" ^ p1.Lexing.pos_fname ^ "\" " ^ - (string_of_int p1.Lexing.pos_lnum) ^ " " ^ + (string_of_int p1.Lexing.pos_lnum) ^ " " ^ (string_of_int (p1.Lexing.pos_cnum - p1.Lexing.pos_bol)) ^ " " ^ (string_of_int p2.Lexing.pos_lnum) ^ " " ^ (string_of_int (p2.Lexing.pos_cnum - p2.Lexing.pos_bol)) ^ ")"*) @@ -100,7 +100,7 @@ let pp_format_bkind_lem (BK_aux(k,l)) = let pp_lem_bkind ppf bk = base ppf (pp_format_bkind_lem bk) -let pp_format_kind_lem (K_aux(K_kind(klst),l)) = +let pp_format_kind_lem (K_aux(K_kind(klst),l)) = "(K_aux (K_kind [" ^ list_format "; " pp_format_bkind_lem klst ^ "]) " ^ (pp_format_l_lem l) ^ ")" let pp_lem_kind ppf k = base ppf (pp_format_kind_lem k) @@ -110,14 +110,14 @@ let rec pp_format_typ_lem (Typ_aux(t,l)) = (match t with | Typ_id(id) -> "(Typ_id " ^ pp_format_id_lem id ^ ")" | Typ_var(var) -> "(Typ_var " ^ pp_format_var_lem var ^ ")" - | Typ_fn(arg,ret,efct) -> "(Typ_fn " ^ pp_format_typ_lem arg ^ " " ^ + | Typ_fn(arg,ret,efct) -> "(Typ_fn " ^ pp_format_typ_lem arg ^ " " ^ pp_format_typ_lem ret ^ " " ^ (pp_format_effects_lem efct) ^ ")" | Typ_tup(typs) -> "(Typ_tup [" ^ (list_format "; " pp_format_typ_lem typs) ^ "])" | Typ_app(id,args) -> "(Typ_app " ^ (pp_format_id_lem id) ^ " [" ^ (list_format "; " pp_format_typ_arg_lem args) ^ "])" | Typ_wild -> "Typ_wild") ^ " " ^ (pp_format_l_lem l) ^ ")" -and pp_format_nexp_lem (Nexp_aux(n,l)) = +and pp_format_nexp_lem (Nexp_aux(n,l)) = "(Nexp_aux " ^ (match n with | Nexp_id(i) -> "(Nexp_id " ^ pp_format_id_lem i ^ ")" @@ -129,8 +129,8 @@ and pp_format_nexp_lem (Nexp_aux(n,l)) = | Nexp_exp(n1) -> "(Nexp_exp " ^ (pp_format_nexp_lem n1) ^ ")" | Nexp_neg(n1) -> "(Nexp_neg " ^ (pp_format_nexp_lem n1) ^ ")") ^ " " ^ (pp_format_l_lem l) ^ ")" -and pp_format_ord_lem (Ord_aux(o,l)) = - "(Ord_aux " ^ +and pp_format_ord_lem (Ord_aux(o,l)) = + "(Ord_aux " ^ (match o with | Ord_var(v) -> "(Ord_var " ^ pp_format_var_lem v ^ ")" | Ord_inc -> "Ord_inc" @@ -162,7 +162,7 @@ and pp_format_effects_lem (Effect_aux(e,l)) = "(Effect_set [" ^ (list_format "; " pp_format_base_effect_lem efcts) ^ " ])") ^ " " ^ (pp_format_l_lem l) ^ ")" -and pp_format_typ_arg_lem (Typ_arg_aux(t,l)) = +and pp_format_typ_arg_lem (Typ_arg_aux(t,l)) = "(Typ_arg_aux " ^ (match t with | Typ_arg_typ(t) -> "(Typ_arg_typ " ^ pp_format_typ_lem t ^ ")" @@ -183,7 +183,7 @@ let pp_format_nexp_constraint_lem (NC_aux(nc,l)) = | NC_fixed(n1,n2) -> "(NC_fixed " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")" | NC_bounded_ge(n1,n2) -> "(NC_bounded_ge " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")" | NC_bounded_le(n1,n2) -> "(NC_bounded_le " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")" - | NC_nat_set_bounded(id,bounds) -> "(NC_nat_set_bounded " ^ + | NC_nat_set_bounded(id,bounds) -> "(NC_nat_set_bounded " ^ pp_format_var_lem id ^ " [" ^ list_format "; " string_of_int bounds ^ @@ -193,7 +193,7 @@ let pp_format_nexp_constraint_lem (NC_aux(nc,l)) = let pp_lem_nexp_constraint ppf nc = base ppf (pp_format_nexp_constraint_lem nc) let pp_format_qi_lem (QI_aux(qi,lq)) = - "(QI_aux " ^ + "(QI_aux " ^ (match qi with | QI_const(n_const) -> "(QI_const " ^ pp_format_nexp_constraint_lem n_const ^ ")" | QI_id(KOpt_aux(ki,lk)) -> @@ -201,19 +201,19 @@ let pp_format_qi_lem (QI_aux(qi,lq)) = (match ki with | KOpt_none(var) -> "(KOpt_none " ^ pp_format_var_lem var ^ ")" | KOpt_kind(k,var) -> "(KOpt_kind " ^ pp_format_kind_lem k ^ " " ^ pp_format_var_lem var ^ ")") ^ " " ^ - (pp_format_l_lem lk) ^ "))") ^ " " ^ + (pp_format_l_lem lk) ^ "))") ^ " " ^ (pp_format_l_lem lq) ^ ")" let pp_lem_qi ppf qi = base ppf (pp_format_qi_lem qi) let pp_format_typquant_lem (TypQ_aux(tq,l)) = - "(TypQ_aux " ^ + "(TypQ_aux " ^ (match tq with | TypQ_no_forall -> "TypQ_no_forall" | TypQ_tq(qlist) -> - "(TypQ_tq [" ^ + "(TypQ_tq [" ^ (list_format "; " pp_format_qi_lem qlist) ^ - "])") ^ " " ^ + "])") ^ " " ^ (pp_format_l_lem l) ^ ")" let pp_lem_typquant ppf tq = base ppf (pp_format_typquant_lem tq) @@ -221,7 +221,7 @@ let pp_lem_typquant ppf tq = base ppf (pp_format_typquant_lem tq) let pp_format_typscm_lem (TypSchm_aux(TypSchm_ts(tq,t),l)) = "(TypSchm_aux (TypSchm_ts " ^ (pp_format_typquant_lem tq) ^ " " ^ pp_format_typ_lem t ^ ") " ^ (pp_format_l_lem l) ^ ")" - + let pp_lem_typscm ppf ts = base ppf (pp_format_typscm_lem ts) let pp_format_lit_lem (L_aux(lit,l)) = @@ -259,7 +259,7 @@ and pp_format_targ = function | TA_ord o -> "(T_arg_order " ^ pp_format_o o ^ ")" and pp_format_n n = match n.nexp with - | Nid (i, n) -> "(Ne_id \"" ^ i ^ " " ^ "\")" + | Nid (i, n) -> "(Ne_id \"" ^ i ^ " " ^ "\")" | Nvar i -> "(Ne_var \"" ^ i ^ "\")" | Nconst i -> "(Ne_const " ^ (lemnum string_of_int (int_of_big_int i)) ^ ")" | Npos_inf -> "Ne_inf" @@ -273,7 +273,7 @@ and pp_format_n n = | Nneg_inf -> "(Ne_unary Ne_inf)" | Npow _ -> "power_not_implemented" | Ninexact -> "(Ne_add Ne_inf (Ne_unary Ne_inf)" -and pp_format_e e = +and pp_format_e e = "(Effect_aux " ^ (match e.effect with | Evar i -> "(Effect_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))" @@ -281,8 +281,8 @@ and pp_format_e e = (list_format "; " pp_format_base_effect_lem es) ^ " ])" | Euvar(_) -> "(Effect_var (Kid_aux (Var \"fresh_v\") Unknown))") ^ " Unknown)" -and pp_format_o o = - "(Ord_aux " ^ +and pp_format_o o = + "(Ord_aux " ^ (match o.order with | Ovar i -> "(Ord_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))" | Oinc -> "Ord_inc" @@ -293,7 +293,7 @@ and pp_format_o o = let rec pp_format_tag = function | Emp_local -> "Tag_empty" | Emp_intro -> "Tag_intro" - | Emp_set -> "Tag_set" + | Emp_set -> "Tag_set" | Emp_global -> "Tag_global" | Tuple_assign tags -> "(Tag_tuple_assign [" ^ list_format " ;" pp_format_tag tags ^ "])" | External (Some s) -> "(Tag_extern (Just \""^s^"\"))" @@ -304,18 +304,18 @@ let rec pp_format_tag = function | Alias alias_inf -> "Tag_alias" | Spec -> "Tag_spec" -let rec pp_format_nes nes = +let rec pp_format_nes nes = "[" ^ (* (list_format "; " (fun ne -> match ne with | LtEq(_,n1,n2) -> "(Nec_lteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")" | Eq(_,n1,n2) -> "(Nec_eq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")" | GtEq(_,n1,n2) -> "(Nec_gteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")" - | In(_,i,ns) | InS(_,{nexp=Nvar i},ns) -> + | In(_,i,ns) | InS(_,{nexp=Nvar i},ns) -> "(Nec_in \"" ^ i ^ "\" [" ^ (list_format "; " string_of_int ns)^ "])" - | InS(_,_,ns) -> + | InS(_,_,ns) -> "(Nec_in \"fresh\" [" ^ (list_format "; " string_of_int ns)^ "])" - | CondCons(_,nes_c,nes_t) -> + | CondCons(_,nes_c,nes_t) -> "(Nec_cond " ^ (pp_format_nes nes_c) ^ " " ^ (pp_format_nes nes_t) ^ ")" | BranchCons(_,nes_b) -> "(Nec_branch " ^ (pp_format_nes nes_b) ^ ")" @@ -324,7 +324,7 @@ let rec pp_format_nes nes = let pp_format_annot = function | NoTyp -> "Nothing" - | Base((_,t),tag,nes,efct,efctsum,_) -> + | Base((_,t),tag,nes,efct,efctsum,_) -> (*TODO print out bindings for use in pattern match in interpreter*) "(Just (" ^ pp_format_t t ^ ", " ^ pp_format_tag tag ^ ", " ^ pp_format_nes nes ^ ", " ^ pp_format_e efct ^ ", " ^ pp_format_e efctsum ^ "))" @@ -344,7 +344,7 @@ let rec pp_format_pat_lem (P_aux(p,(l,annot))) = | P_app(id,pats) -> "(P_app " ^ pp_format_id_lem id ^ " [" ^ list_format "; " pp_format_pat_lem pats ^ "])" | P_record(fpats,_) -> "(P_record [" ^ - list_format "; " (fun (FP_aux(FP_Fpat(id,fpat),_)) -> + list_format "; " (fun (FP_aux(FP_Fpat(id,fpat),_)) -> "(FP_Fpat " ^ pp_format_id_lem id ^ " " ^ pp_format_pat_lem fpat ^ ")") fpats ^ "])" | P_vector(pats) -> "(P_vector [" ^ list_format "; " pp_format_pat_lem pats ^ "])" @@ -352,29 +352,29 @@ let rec pp_format_pat_lem (P_aux(p,(l,annot))) = "(P_vector_indexed [" ^ list_format "; " (fun (i,p) -> Printf.sprintf "(%d, %s)" i (pp_format_pat_lem p)) ipats ^ "])" | P_vector_concat(pats) -> "(P_vector_concat [" ^ list_format "; " pp_format_pat_lem pats ^ "])" | P_tup(pats) -> "(P_tup [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])" - | P_list(pats) -> "(P_list [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])") ^ + | P_list(pats) -> "(P_list [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])") ^ " (" ^ pp_format_l_lem l ^ ", " ^ pp_format_annot annot ^ "))" let pp_lem_pat ppf p = base ppf (pp_format_pat_lem p) let rec pp_lem_let ppf (LB_aux(lb,(l,annot))) = - let print_lb ppf lb = + let print_lb ppf lb = match lb with - | LB_val_explicit(ts,pat,exp) -> + | LB_val_explicit(ts,pat,exp) -> fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "LB_val_explicit" pp_lem_typscm ts pp_lem_pat pat pp_lem_exp exp - | LB_val_implicit(pat,exp) -> + | LB_val_implicit(pat,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "LB_val_implicit" pp_lem_pat pat pp_lem_exp exp in fprintf ppf "@[<0>(LB_aux %a (%a, %a))@]" print_lb lb pp_lem_l l pp_annot annot -and pp_lem_exp ppf (E_aux(e,(l,annot))) = - let print_e ppf e = +and pp_lem_exp ppf (E_aux(e,(l,annot))) = + let print_e ppf e = match e with | E_block(exps) -> fprintf ppf "@[<0>(E_aux %a [%a] %a (%a, %a))@]" - kwd "(E_block" + kwd "(E_block" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")" pp_lem_l l pp_annot annot | E_nondet(exps) -> fprintf ppf "@[<0>(E_aux %a [%a] %a (%a, %a))@]" - kwd "(E_nondet" + kwd "(E_nondet" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")" pp_lem_l l pp_annot annot | E_id(id) -> fprintf ppf "(E_aux (%a %a) (%a, %a))" kwd "E_id" pp_lem_id id pp_lem_l l pp_annot annot @@ -391,30 +391,30 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) = | E_if(c,t,e) -> fprintf ppf "@[<0>(E_aux (E_if %a @[<1>%a@] @[<1> %a@]) (%a, %a))@]" pp_lem_exp c pp_lem_exp t pp_lem_exp e pp_lem_l l pp_annot annot | E_for(id,exp1,exp2,exp3,order,exp4) -> - fprintf ppf "@[<0>(E_aux (E_for %a %a %a %a %a @ @[<1> %a @]) (%a, %a))@]" + fprintf ppf "@[<0>(E_aux (E_for %a %a %a %a %a @ @[<1> %a @]) (%a, %a))@]" pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3 pp_lem_ord order pp_lem_exp exp4 pp_lem_l l pp_annot annot | E_vector(exps) -> fprintf ppf "@[<0>(E_aux (%a [%a]) (%a, %a))@]" kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps pp_lem_l l pp_annot annot - | E_vector_indexed(iexps,(Def_val_aux (default, (dl,dannot)))) -> + | E_vector_indexed(iexps,(Def_val_aux (default, (dl,dannot)))) -> let iformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) %a@]" i kwd ", " pp_lem_exp e kwd ";" in let lformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) @]" i kwd ", " pp_lem_exp e in let default_string ppf _ = (match default with - | Def_val_empty -> fprintf ppf "(Def_val_aux Def_val_empty (%a,%a))" pp_lem_l dl pp_annot dannot + | Def_val_empty -> fprintf ppf "(Def_val_aux Def_val_empty (%a,%a))" pp_lem_l dl pp_annot dannot | Def_val_dec e -> fprintf ppf "(Def_val_aux (Def_val_dec %a) (%a,%a))" - pp_lem_exp e pp_lem_l dl pp_annot dannot) in + pp_lem_exp e pp_lem_l dl pp_annot dannot) in fprintf ppf "@[<0>(E_aux (%a [%a] %a) (%a, %a))@]" kwd "E_vector_indexed" (list_pp iformat lformat) iexps default_string () pp_lem_l l pp_annot annot | E_vector_access(v,e) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_vector_access" pp_lem_exp v pp_lem_exp e pp_lem_l l pp_annot annot - | E_vector_subrange(v,e1,e2) -> + | E_vector_subrange(v,e1,e2) -> fprintf ppf "@[<0>(E_aux (E_vector_subrange %a %a %a) (%a, %a))@]" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_l l pp_annot annot - | E_vector_update(v,e1,e2) -> + | E_vector_update(v,e1,e2) -> fprintf ppf "@[<0>(E_aux (E_vector_update %a %a %a) (%a, %a))@]" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_l l pp_annot annot - | E_vector_update_subrange(v,e1,e2,e3) -> + | E_vector_update_subrange(v,e1,e2,e3) -> fprintf ppf "@[<0>(E_aux (E_vector_update_subrange %a %a %a %a) (%a, %a))@]" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_exp e3 pp_lem_l l pp_annot annot | E_vector_append(v1,v2) -> @@ -424,7 +424,7 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) = (list_pp pp_semi_lem_exp pp_lem_exp) exps pp_lem_l l pp_annot annot | E_cons(e1,e2) -> fprintf ppf "@[<0>(E_aux (E_cons %a %a) (%a, %a))@]" pp_lem_exp e1 pp_lem_exp e2 pp_lem_l l pp_annot annot - | E_record(FES_aux(FES_Fexps(fexps,_),(fl,fannot))) -> + | E_record(FES_aux(FES_Fexps(fexps,_),(fl,fannot))) -> fprintf ppf "@[<0>(E_aux (E_record (FES_aux (FES_Fexps [%a] false) (%a,%a))) (%a, %a))@]" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps pp_lem_l fl pp_annot fannot pp_lem_l l pp_annot annot | E_record_update(exp,(FES_aux(FES_Fexps(fexps,_),(fl,fannot)))) -> @@ -433,7 +433,7 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) = pp_lem_l fl pp_annot fannot pp_lem_l l pp_annot annot | E_field(fexp,id) -> fprintf ppf "@[<0>(E_aux (E_field %a %a) (%a, %a))@]" pp_lem_exp fexp pp_lem_id id pp_lem_l l pp_annot annot - | E_case(exp,pexps) -> + | E_case(exp,pexps) -> fprintf ppf "@[<0>(E_aux (E_case %a [%a]) (%a, %a))@]" pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps pp_lem_l l pp_annot annot | E_let(leb,exp) -> fprintf ppf "@[<0>(E_aux (E_let %a %a) (%a, %a))@]" @@ -454,14 +454,14 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) = | Tapp("register",[TA_typ {t=Tapp("vector",[TA_nexp _;TA_nexp r;_;_])}]) | Tapp("vector",[TA_nexp _;TA_nexp r;_;_]) -> (match r.nexp with - | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]" + | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]" kwd (lemnum string_of_int (int_of_big_int bi)) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob)) | Nvar v -> fprintf ppf "@[<0>(E_aux (E_id (Id_aux (Id \"%a\") %a)) (%a,%a))@]" kwd v pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob)) | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given vector without known length")) | Tapp("implicit",[TA_nexp r]) -> (match r.nexp with - | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]" + | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]" kwd (lemnum string_of_int (int_of_big_int bi)) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob)) | Nvar v -> fprintf ppf "@[<0>(E_aux (E_id (Id_aux (Id \"%a\") %a)) (%a,%a))@]" kwd v pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob)) @@ -481,16 +481,16 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) = and pp_semi_lem_exp ppf e = fprintf ppf "@[<1>%a%a@]" pp_lem_exp e kwd ";" -and pp_lem_fexp ppf (FE_aux(FE_Fexp(id,exp),(l,annot))) = +and pp_lem_fexp ppf (FE_aux(FE_Fexp(id,exp),(l,annot))) = fprintf ppf "@[<1>(FE_aux (FE_Fexp %a %a) (%a, %a))@]" pp_lem_id id pp_lem_exp exp pp_lem_l l pp_annot annot and pp_semi_lem_fexp ppf fexp = fprintf ppf "@[<1>%a %a@]" pp_lem_fexp fexp kwd ";" -and pp_lem_case ppf (Pat_aux(Pat_exp(pat,exp),(l,annot))) = +and pp_lem_case ppf (Pat_aux(Pat_exp(pat,exp),(l,annot))) = fprintf ppf "@[<1>(Pat_aux (Pat_exp %a@ %a) (%a, %a))@]" pp_lem_pat pat pp_lem_exp exp pp_lem_l l pp_annot annot and pp_semi_lem_case ppf case = fprintf ppf "@[<1>%a %a@]" pp_lem_case case kwd ";" and pp_lem_lexp ppf (LEXP_aux(lexp,(l,annot))) = - let print_le ppf lexp = + let print_le ppf lexp = match lexp with | LEXP_id(id) -> fprintf ppf "(%a %a)" kwd "LEXP_id" pp_lem_id id | LEXP_memory(id,args) -> @@ -498,7 +498,7 @@ and pp_lem_lexp ppf (LEXP_aux(lexp,(l,annot))) = | LEXP_cast(typ,id) -> fprintf ppf "(LEXP_cast %a %a)" pp_lem_typ typ pp_lem_id id | LEXP_tup tups -> fprintf ppf "(LEXP_tuple [%a])" (list_pp pp_semi_lem_lexp pp_lem_lexp) tups | LEXP_vector(v,exp) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_vector" pp_lem_lexp v pp_lem_exp exp - | LEXP_vector_range(v,e1,e2) -> + | LEXP_vector_range(v,e1,e2) -> fprintf ppf "@[(%a %a %a %a)@]" kwd "LEXP_vector_range" pp_lem_lexp v pp_lem_exp e1 pp_lem_exp e2 | LEXP_field(v,id) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_field" pp_lem_lexp v pp_lem_id id in @@ -533,35 +533,35 @@ let pp_lem_namescm ppf (Name_sect_aux(ns,l)) = | Name_sect_some(s) -> fprintf ppf "(Name_sect_aux (Name_sect_some \"%s\") %a)" s pp_lem_l l let rec pp_lem_range ppf (BF_aux(r,l)) = - match r with + match r with | BF_single(i) -> fprintf ppf "(BF_aux (BF_single %i) %a)" i pp_lem_l l | BF_range(i1,i2) -> fprintf ppf "(BF_aux (BF_range %i %i) %a)" i1 i2 pp_lem_l l | BF_concat(ir1,ir2) -> fprintf ppf "(BF_aux (BF_concat %a %a) %a)" pp_lem_range ir1 pp_lem_range ir2 pp_lem_l l let pp_lem_typdef ppf (TD_aux(td,(l,annot))) = - let print_td ppf td = + let print_td ppf td = match td with - | TD_abbrev(id,namescm,typschm) -> + | TD_abbrev(id,namescm,typschm) -> fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "TD_abbrev" pp_lem_id id pp_lem_namescm namescm pp_lem_typscm typschm - | TD_record(id,nm,typq,fs,_) -> + | TD_record(id,nm,typq,fs,_) -> let f_pp ppf (typ,id) = fprintf ppf "@[<1>(%a, %a)%a@]" pp_lem_typ typ pp_lem_id id kwd ";" in - fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" + fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" kwd "TD_record" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp f_pp f_pp) fs | TD_variant(id,nm,typq,ar,_) -> - let a_pp ppf (Tu_aux(typ_u,l)) = + let a_pp ppf (Tu_aux(typ_u,l)) = match typ_u with - | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_aux (Tu_ty_id %a %a) %a);@]" + | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_aux (Tu_ty_id %a %a) %a);@]" pp_lem_typ typ pp_lem_id id pp_lem_l l | Tu_id(id) -> fprintf ppf "@[<1>(Tu_aux (Tu_id %a) %a);@]" pp_lem_id id pp_lem_l l in - fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" - kwd "TD_variant" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar + fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" + kwd "TD_variant" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar | TD_enum(id,ns,enums,_) -> let pp_id_semi ppf id = fprintf ppf "%a%a " pp_lem_id id kwd ";" in fprintf ppf "@[<0>(%a %a %a [%a] false)@]" kwd "TD_enum" pp_lem_id id pp_lem_namescm ns (list_pp pp_id_semi pp_lem_id) enums - | TD_register(id,n1,n2,rs) -> + | TD_register(id,n1,n2,rs) -> let pp_rid ppf (r,id) = fprintf ppf "(%a, %a)%a " pp_lem_range r pp_lem_id id kwd ";" in let pp_rids = (list_pp pp_rid pp_rid) in fprintf ppf "@[<0>(%a %a %a %a [%a])@]" @@ -570,33 +570,33 @@ let pp_lem_typdef ppf (TD_aux(td,(l,annot))) = fprintf ppf "@[<0>(TD_aux %a (%a, %a))@]" print_td td pp_lem_l l pp_annot annot let pp_lem_kindef ppf (KD_aux(kd,(l,annot))) = - let print_kd ppf kd = + let print_kd ppf kd = match kd with - | KD_abbrev(kind,id,namescm,typschm) -> + | KD_abbrev(kind,id,namescm,typschm) -> fprintf ppf "@[<0>(KD_abbrev %a %a %a %a)@]" pp_lem_kind kind pp_lem_id id pp_lem_namescm namescm pp_lem_typscm typschm | KD_nabbrev(kind,id,namescm,n) -> fprintf ppf "@[<0>(KD_nabbrev %a %a %a %a)@]" pp_lem_kind kind pp_lem_id id pp_lem_namescm namescm pp_lem_nexp n - | KD_record(kind,id,nm,typq,fs,_) -> + | KD_record(kind,id,nm,typq,fs,_) -> let f_pp ppf (typ,id) = fprintf ppf "@[<1>(%a, %a)%a@]" pp_lem_typ typ pp_lem_id id kwd ";" in - fprintf ppf "@[<0>(%a %a %a %a %a [%a] false)@]" + fprintf ppf "@[<0>(%a %a %a %a %a [%a] false)@]" kwd "KD_record" pp_lem_kind kind pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp f_pp f_pp) fs | KD_variant(kind,id,nm,typq,ar,_) -> - let a_pp ppf (Tu_aux(typ_u,l)) = + let a_pp ppf (Tu_aux(typ_u,l)) = match typ_u with - | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_aux (Tu_ty_id %a %a) %a);@]" + | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_aux (Tu_ty_id %a %a) %a);@]" pp_lem_typ typ pp_lem_id id pp_lem_l l | Tu_id(id) -> fprintf ppf "@[<1>(Tu_aux (Tu_id %a) %a);@]" pp_lem_id id pp_lem_l l in - fprintf ppf "@[<0>(%a %a %a %a %a [%a] false)@]" - kwd "KD_variant" pp_lem_kind kind pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar + fprintf ppf "@[<0>(%a %a %a %a %a [%a] false)@]" + kwd "KD_variant" pp_lem_kind kind pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar | KD_enum(kind,id,ns,enums,_) -> let pp_id_semi ppf id = fprintf ppf "%a%a " pp_lem_id id kwd ";" in fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" kwd "KD_enum" pp_lem_kind kind pp_lem_id id pp_lem_namescm ns (list_pp pp_id_semi pp_lem_id) enums - | KD_register(kind,id,n1,n2,rs) -> + | KD_register(kind,id,n1,n2,rs) -> let pp_rid ppf (r,id) = fprintf ppf "(%a, %a)%a " pp_lem_range r pp_lem_id id kwd ";" in let pp_rids = (list_pp pp_rid pp_rid) in fprintf ppf "@[<0>(%a %a %a %a %a [%a])@]" @@ -608,10 +608,10 @@ let pp_lem_rec ppf (Rec_aux(r,l)) = match r with | Rec_nonrec -> fprintf ppf "(Rec_aux Rec_nonrec %a)" pp_lem_l l | Rec_rec -> fprintf ppf "(Rec_aux Rec_rec %a)" pp_lem_l l - + let pp_lem_tannot_opt ppf (Typ_annot_opt_aux(t,l)) = match t with - | Typ_annot_opt_some(tq,typ) -> + | Typ_annot_opt_some(tq,typ) -> fprintf ppf "(Typ_annot_opt_aux (Typ_annot_opt_some %a %a) %a)" pp_lem_typquant tq pp_lem_typ typ pp_lem_l l let pp_lem_effects_opt ppf (Effect_opt_aux(e,l)) = @@ -620,12 +620,12 @@ let pp_lem_effects_opt ppf (Effect_opt_aux(e,l)) = | Effect_opt_effect e -> fprintf ppf "(Effect_opt_aux (Effect_opt_effect %a) %a)" pp_lem_effects e pp_lem_l l let pp_lem_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),(l,annot))) = - fprintf ppf "@[<0>(FCL_aux (%a %a %a %a) (%a,%a))@]@\n" + fprintf ppf "@[<0>(FCL_aux (%a %a %a %a) (%a,%a))@]@\n" kwd "FCL_Funcl" pp_lem_id id pp_lem_pat pat pp_lem_exp exp pp_lem_l l pp_annot annot let pp_lem_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),(l,annot))) = let pp_funcls ppf funcl = fprintf ppf "%a %a" pp_lem_funcl funcl kwd ";" in - fprintf ppf "@[<0>(FD_aux (%a %a %a %a [%a]) (%a, %a))@]" + fprintf ppf "@[<0>(FD_aux (%a %a %a %a [%a]) (%a, %a))@]" kwd "FD_function" pp_lem_rec r pp_lem_tannot_opt typa pp_lem_effects_opt efa (list_pp pp_funcls pp_funcls) fcls pp_lem_l l pp_annot annot @@ -633,19 +633,19 @@ let pp_lem_aspec ppf (AL_aux(aspec,(l,annot))) = let pp_reg_id ppf (RI_aux((RI_id ri),(l,annot))) = fprintf ppf "@[<0>(RI_aux (RI_id %a) (%a,%a))@]" pp_lem_id ri pp_lem_l l pp_annot annot in match aspec with - | AL_subreg(reg,subreg) -> + | AL_subreg(reg,subreg) -> fprintf ppf "@[<0>(AL_aux (AL_subreg %a %a) (%a,%a))@]" pp_reg_id reg pp_lem_id subreg pp_lem_l l pp_annot annot | AL_bit(reg,ac) -> fprintf ppf "@[<0>(AL_aux (AL_bit %a %a) (%a,%a))@]" pp_reg_id reg pp_lem_exp ac pp_lem_l l pp_annot annot | AL_slice(reg,b,e) -> - fprintf ppf "@[<0>(AL_aux (AL_slice %a %a %a) (%a,%a))@]" + fprintf ppf "@[<0>(AL_aux (AL_slice %a %a %a) (%a,%a))@]" pp_reg_id reg pp_lem_exp b pp_lem_exp e pp_lem_l l pp_annot annot | AL_concat(f,s) -> fprintf ppf "@[<0>(AL_aux (AL_concat %a %a) (%a,%a))@]" pp_reg_id f pp_reg_id s pp_lem_l l pp_annot annot let pp_lem_dec ppf (DEC_aux(reg,(l,annot))) = - match reg with + match reg with | DEC_reg(typ,id) -> fprintf ppf "@[<0>(DEC_aux (DEC_reg %a %a) (%a,%a))@]" pp_lem_typ typ pp_lem_id id pp_lem_l l pp_annot annot | DEC_alias(id,alias_spec) -> @@ -664,7 +664,7 @@ let pp_lem_def ppf d = | DEF_fundef(f_def) -> fprintf ppf "(DEF_fundef %a);@\n" pp_lem_fundef f_def | DEF_val(lbind) -> fprintf ppf "(DEF_val %a);@\n" pp_lem_let lbind | DEF_reg_dec(dec) -> fprintf ppf "(DEF_reg_dec %a);@\n" pp_lem_dec dec - | DEF_comm d -> fprintf ppf "" + | DEF_comm d -> fprintf ppf "" | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "initial_check didn't remove all scattered Defs") let pp_lem_defs ppf (Defs(defs)) = @@ -1054,18 +1054,18 @@ let doc_exp, doc_let = (match e with | E_lit (L_aux(L_one, _)) | E_lit (L_aux(L_zero, _)) -> utf8string - ("0b" ^ + ("0b" ^ (List.fold_right (fun (E_aux( e,_)) rst -> - (match e with + (match e with | E_lit(L_aux(l, _)) -> ((match l with | L_one -> "1" | L_zero -> "0" | L_undef -> "u" | _ -> assert false) ^ rst) - | _ -> assert false)) exps "")) + | _ -> assert false)) exps "")) | _ -> default_print ())) | E_vector_indexed (iexps, (Def_val_aux (default,_))) -> - let default_string = + let default_string = (match default with - | Def_val_empty -> string "" - | Def_val_dec e -> concat [semi; space; string "default"; equals; (exp e)]) in + | Def_val_empty -> string "" + | Def_val_dec e -> concat [semi; space; string "default"; equals; (exp e)]) in let iexp (i,e) = doc_op equals (doc_int i) (exp e) in brackets (concat [(separate_map comma iexp iexps); default_string]) | E_vector_update(v,e1,e2) -> @@ -1123,7 +1123,7 @@ let doc_exp, doc_let = (match r.nexp with | Nvar v -> utf8string v | Nconst bi -> utf8string (Big_int.string_of_big_int bi) - | _ -> raise (Reporting_basic.err_unreachable l + | _ -> raise (Reporting_basic.err_unreachable l ("Internal exp given vector without known length, instead given " ^ n_to_string r))) | Tapp("implicit",[TA_nexp r]) -> (match r.nexp with @@ -1270,7 +1270,7 @@ let doc_kindef (KD_aux(kd,_)) = match kd with braces doc_rids; ]) - + let doc_rec (Rec_aux(r,_)) = match r with | Rec_nonrec -> empty (* include trailing space because caller doesn't know if we return @@ -1313,7 +1313,7 @@ let doc_dec (DEC_aux (reg,_)) = | DEC_reg(typ,id) -> separate space [string "register"; doc_typ typ; doc_id id] | DEC_alias(id,alspec) -> doc_op equals (string "register alias" ^^ space ^^ doc_id id) (doc_alias alspec) - | DEC_typ_alias(typ,id,alspec) -> + | DEC_typ_alias(typ,id,alspec) -> doc_op equals (string "register alias" ^^ space ^^ doc_typ typ) (doc_alias alspec) let doc_scattered (SD_aux (sdef, _)) = match sdef with @@ -1357,7 +1357,7 @@ let to_buf ?(len=100) buf doc = ToBuffer.pretty 1. len buf doc let pp_defs f d = print f (doc_defs d) let pp_exp b e = to_buf b (doc_exp e) -let pat_to_string p = +let pat_to_string p = let b = Buffer.create 20 in to_buf b (doc_pat p); Buffer.contents b @@ -1374,7 +1374,7 @@ let is_number char = let doc_id_ocaml (Id_aux(i,_)) = match i with - | Id("bit") -> string "vbit" + | Id("bit") -> string "vbit" | Id i -> string (if i.[0] = '\'' || is_number(i.[0]) then "_" ^ i else String.uncapitalize i) @@ -1385,7 +1385,7 @@ let doc_id_ocaml (Id_aux(i,_)) = let doc_id_ocaml_type (Id_aux(i,_)) = match i with - | Id("bit") -> string "vbit" + | Id("bit") -> string "vbit" | Id i -> string (String.uncapitalize i) | DeIid x -> (* add an extra space through empty to avoid a closing-comment @@ -1394,7 +1394,7 @@ let doc_id_ocaml_type (Id_aux(i,_)) = let doc_id_ocaml_ctor n (Id_aux(i,_)) = match i with - | Id("bit") -> string "vbit" + | Id("bit") -> string "vbit" | Id i -> string ((if n > 246 then "`" else "") ^ (String.capitalize i)) | DeIid x -> (* add an extra space through empty to avoid a closing-comment @@ -1426,7 +1426,7 @@ let doc_typ_ocaml, doc_atomic_typ_ocaml = (string "number") | Typ_app(id,args) -> (separate_map space doc_typ_arg_ocaml args) ^^ space ^^ (doc_id_ocaml_type id) - | _ -> atomic_typ ty + | _ -> atomic_typ ty and atomic_typ ((Typ_aux (t, _)) as ty) = match t with | Typ_id id -> doc_id_ocaml_type id | Typ_var v -> doc_var v @@ -1461,7 +1461,7 @@ let doc_typquant_ocaml (TypQ_aux(tq,_)) typ_doc = typ_doc let doc_typscm_ocaml (TypSchm_aux(TypSchm_ts(tq,t),_)) = (doc_typquant tq (doc_typ_ocaml t)) -(*Note: vector concatenation, literal vectors, indexed vectors, and record should +(*Note: vector concatenation, literal vectors, indexed vectors, and record should be removed prior to pp. The latter two have never yet been seen *) let doc_pat_ocaml = @@ -1476,7 +1476,7 @@ let doc_pat_ocaml = | P_wild -> underscore | P_id id -> doc_id_ocaml id | P_as(p,id) -> parens (separate space [pat p; string "as"; doc_id_ocaml id]) - | P_typ(typ,p) -> doc_op colon (pat p) (doc_typ_ocaml typ) + | P_typ(typ,p) -> doc_op colon (pat p) (doc_typ_ocaml typ) | P_app(id,[]) -> (match annot with | Base(_,Constructor n,_,_,_,_) -> @@ -1560,10 +1560,10 @@ let doc_exp_ocaml, doc_let_ocaml = (* this way requires the following OCaml declarations first - let rec foreach_inc i stop by body = + let rec foreach_inc i stop by body = if i <= stop then (body i; foreach_inc (i + by) stop by body) else () - let rec foreach_dec i stop by body = + let rec foreach_dec i stop by body = if i >= stop then (body i; foreach_dec (i - by) stop by body) else () *)*) @@ -1677,16 +1677,16 @@ let doc_exp_ocaml, doc_let_ocaml = | _ -> false, "false" in let start = match start.nexp with | Nconst i | N2n(_,Some i)-> string_of_big_int i - | N2n({nexp=Nconst i},_) -> string_of_int (Util.power 2 (int_of_big_int i)) + | N2n({nexp=Nconst i},_) -> string_of_int (Util.power 2 (int_of_big_int i)) | _ -> if dir then "0" else string_of_int (List.length iexps) in let size = match len.nexp with | Nconst i | N2n(_,Some i)-> string_of_big_int i | N2n({nexp=Nconst i},_) -> string_of_int (Util.power 2 (int_of_big_int i)) in - let default_string = + let default_string = (match default with - | Def_val_empty -> string "None" - | Def_val_dec e -> parens (string "Some " ^^ (exp e))) in + | Def_val_empty -> string "None" + | Def_val_dec e -> parens (string "Some " ^^ (exp e))) in let iexp (i,e) = parens (separate_map comma_sp (fun x -> x) [(doc_int i); (exp e)]) in parens (separate space [call; (brackets (separate_map semi iexp iexps)); @@ -1711,7 +1711,7 @@ let doc_exp_ocaml, doc_let_ocaml = | E_exit e -> separate space [string "exit"; exp e;] | E_app_infix (e1,id,e2) -> - let call = + let call = match annot with | Base((_,t),External(Some name),_,_,_,_) -> string name | _ -> doc_id_ocaml id in @@ -1728,7 +1728,7 @@ let doc_exp_ocaml, doc_let_ocaml = | E_internal_plet (pat,e1,e2) -> (separate space [(exp e1); string ">>= fun"; doc_pat_ocaml pat;arrow]) ^/^ exp e2 - + | E_internal_return (e1) -> separate space [string "return"; exp e1;] and let_exp (LB_aux(lb,_)) = match lb with @@ -1759,7 +1759,7 @@ let doc_exp_ocaml, doc_let_ocaml = | Base((_,{t=Tapp("reg",_)}),Emp_set,_,_,_,_),false | Base((_,{t=Tabbrev(_,{t=Tapp("reg",_)})}),Emp_set,_,_,_,_),false -> string "!" ^^ name | _ -> name - + and doc_lexp_array_ocaml ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with | LEXP_vector(v,e) -> (match annot with @@ -1813,11 +1813,11 @@ let doc_exp_ocaml, doc_let_ocaml = (group (parens ((string (if is_bit then "get_barray" else "get_varray")) ^^ space ^^ string reg)) ^^ dot ^^ parens (doc_int start)) (exp e_new_v) - else + else parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_vec")) ^^ space ^^ string reg ^^ space ^^ doc_int start ^^ space ^^ doc_int stop ^^ space ^^ exp e_new_v) | Alias_pair(reg1,reg2) -> - parens ((string "set_two_regs") ^^ space ^^ string reg1 ^^ space ^^ string reg2 ^^ space ^^ exp e_new_v)) + parens ((string "set_two_regs") ^^ space ^^ string reg1 ^^ space ^^ string reg2 ^^ space ^^ exp e_new_v)) | _ -> parens (separate space [string "set_register"; doc_id_ocaml id; exp e_new_v])) @@ -1864,7 +1864,7 @@ let doc_typdef_ocaml (TD_aux(td,_)) = match td with let doc_rids = group (separate_map (semi ^^ (break 1)) doc_rid rs) in match n1,n2 with | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) -> - let dir = i1 < i2 in + let dir = i1 < i2 in let size = if dir then i2-i1 +1 else i1-i2 in doc_op equals ((string "let") ^^ space ^^ doc_id_ocaml id ^^ space ^^ (string "init_val")) @@ -1914,7 +1914,7 @@ let doc_kdef_ocaml (KD_aux(kd,_)) = match kd with let doc_rids = group (separate_map (semi ^^ (break 1)) doc_rid rs) in match n1,n2 with | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) -> - let dir = i1 < i2 in + let dir = i1 < i2 in let size = if dir then i2-i1 +1 else i1-i2 in doc_op equals ((string "let") ^^ space ^^ doc_id_ocaml id ^^ space ^^ (string "init_val")) @@ -1988,7 +1988,7 @@ let doc_dec_ocaml (DEC_aux (reg,(l,annot))) = doc_int (int_of_big_int size); string "Vzero";])]; doc_int (int_of_big_int start); - o; + o; brackets empty])] | _ -> empty) | Tapp("register", [TA_typ {t=Tid idt}]) | @@ -2019,7 +2019,7 @@ let doc_defs_ocaml (Defs(defs)) = separate_map hardline doc_def_ocaml defs let pp_defs_ocaml f d top_line opens = print f (string "(*" ^^ (string top_line) ^^ string "*)" ^/^ - (separate_map hardline (fun lib -> (string "open") ^^ space ^^ (string lib)) opens) ^/^ + (separate_map hardline (fun lib -> (string "open") ^^ space ^^ (string lib)) opens) ^/^ (doc_defs_ocaml d)) @@ -2052,47 +2052,8 @@ let keywords = "LT"; "GT"; "EQ"; - -(* "nia"; - "NIA_successor"; - "NIA_concrete_address"; - "NIA_LR"; - "NIA_CTR"; - "NIA_register"; - "read_kind"; - "Read_plain"; - "Read_tag"; - "Read_reserve"; - "Read_acquire"; - "Read_exclusive"; - "Read_exclusive_acquire"; - "Read_stream"; - "write_kind"; - "Write_plain"; - "Write_tag"; - "Write_conditional"; - "Write_release"; - "Write_exclusive"; - "Write_exclusive_release"; - "barrier_kind"; - "Barrier_Sync"; - "Barrier_LwSync"; - "Barrier_Eieio"; - "Barrier_Isync"; - "Barrier_DMB"; - "Barrier_DMB_ST"; - "Barrier_DMB_LD"; - "Barrier_DSB"; - "Barrier_DSB_ST"; - "Barrier_DSB_LD"; - "Barrier_ISB"; - "instruction_kind"; - "IK_barrier"; - "IK_mem_read"; - "IK_mem_write"; - "IK_cond_branch"; - "IK_simple"; *) - ] + "integer"; + ] let fix_id i = if M.mem i keywords then M.find i keywords else i @@ -2111,8 +2072,8 @@ let doc_id_lem (Id_aux(i,_)) = let doc_id_lem_type (Id_aux(i,_)) = match i with - | Id("int") -> string "integer" - | Id("nat") -> string "integer" + | Id("int") -> string "SV.ii" + | Id("nat") -> string "SV.ii" | Id("option") -> string "maybe" | Id i -> string (fix_id i) | DeIid x -> @@ -2122,7 +2083,7 @@ let doc_id_lem_type (Id_aux(i,_)) = let doc_id_lem_ctor (Id_aux(i,_)) = match i with - | Id("bit") -> string "bitU" + | Id("bit") -> string "bitU" | Id("int") -> string "integer" | Id("nat") -> string "integer" | Id("Some") -> string "Just" @@ -2148,7 +2109,7 @@ let effectful (Effect_aux (eff,_)) = let rec is_number {t=t} = match t with | Tabbrev (t1,t2) -> is_number t1 || is_number t2 - | Tapp ("range",_) + | Tapp ("range",_) | Tapp ("implicit",_) | Tapp ("atom",_) -> true | _ -> false @@ -2159,10 +2120,10 @@ let doc_typ_lem, doc_atomic_typ_lem = and typ' regtypes ty = fn_typ regtypes false ty and fn_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with | Typ_fn(arg,ret,efct) -> - let exc_typ = string "string" in + (*let exc_typ = string "string" in*) let ret_typ = if effectful efct - then separate space [string "M";parens exc_typ;fn_typ regtypes true ret] + then separate space [string "M";(*parens exc_typ;*) fn_typ regtypes true ret] else separate space [fn_typ regtypes false ret] in let tpp = separate space [tup_typ regtypes true arg; arrow;ret_typ] in (* once we have proper excetions we need to know what the exceptions type is *) @@ -2186,7 +2147,7 @@ let doc_typ_lem, doc_atomic_typ_lem = | Typ_app(id,args) -> let tpp = (doc_id_lem_type id) ^^ space ^^ (separate_map space (doc_typ_arg_lem regtypes) args) in if atyp_needed then parens tpp else tpp - | _ -> atomic_typ regtypes atyp_needed ty + | _ -> atomic_typ regtypes atyp_needed ty and atomic_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with | Typ_id (Id_aux (Id "bool",_)) -> string "bitU" | Typ_id (Id_aux (Id "boolean",_)) -> string "bitU" @@ -2221,9 +2182,9 @@ let doc_lit_lem in_pat (L_aux(lit,l)) a = | L_true -> "I" | L_num i -> let ipp = string_of_int i in - if in_pat then "("^ipp^":n)" - else if i < 0 then "((0"^ipp^"):i)" - else "("^ipp^":i)" + if in_pat then "("^ipp^":nn)" + else if i < 0 then "((0"^ipp^"):ii)" + else "("^ipp^":ii)" | L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*) | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*) | L_undef -> @@ -2233,6 +2194,8 @@ let doc_lit_lem in_pat (L_aux(lit,l)) a = | Tabbrev ({t = Tid "bit"},_) -> "Undef" | Tapp ("register",_) | Tabbrev ({t = Tapp ("register",_)},_) -> "UndefinedRegister 0" + | Tid "string" + | Tabbrev ({t = Tapp ("string",_)},_) -> "\"\"" | _ -> "(failwith \"undefined value of unsupported type\")") | L_string s -> "\"" ^ s ^ "\"") @@ -2243,7 +2206,7 @@ let doc_typquant_lem (TypQ_aux(tq,_)) typ_doc = typ_doc let doc_typschm_lem regtypes (TypSchm_aux(TypSchm_ts(tq,t),_)) = (doc_typquant_lem tq (doc_typ_lem regtypes t)) -(*Note: vector concatenation, literal vectors, indexed vectors, and record should +(*Note: vector concatenation, literal vectors, indexed vectors, and record should be removed prior to pp. The latter two have never yet been seen *) let rec doc_pat_lem regtypes apat_needed (P_aux (p,(l,annot)) as pa) = match p with @@ -2261,11 +2224,11 @@ let rec doc_pat_lem regtypes apat_needed (P_aux (p,(l,annot)) as pa) = match p w | P_lit lit -> doc_lit_lem true lit annot | P_wild -> underscore | P_id id -> - begin match id with + begin match id with | Id_aux (Id "None",_) -> string "Nothing" (* workaround temporary issue *) | _ -> doc_id_lem id end | P_as(p,id) -> parens (separate space [doc_pat_lem regtypes true p; string "as"; doc_id_lem id]) - | P_typ(typ,p) -> doc_op colon (doc_pat_lem regtypes true p) (doc_typ_lem regtypes typ) + | P_typ(typ,p) -> doc_op colon (doc_pat_lem regtypes true p) (doc_typ_lem regtypes typ) | P_vector pats -> let ppp = (separate space) @@ -2354,9 +2317,9 @@ let doc_exp_lem, doc_let_lem = | E_cons(l,r) -> doc_op (group (colon^^colon)) (expY l) (expY r) | E_if(c,t,e) -> let (E_aux (_,(_,cannot))) = c in - let epp = + let epp = separate space [string "if";group (align (string "to_bool" ^//^ group (expY c)))] ^^ - break 1 ^^ + break 1 ^^ (prefix 2 1 (string "then") (expN t)) ^^ (break 1) ^^ (prefix 2 1 (string "else") (expN e)) in if aexp_needed then parens (align epp) else epp @@ -2400,14 +2363,14 @@ let doc_exp_lem, doc_let_lem = | [] -> doc_id_lem_ctor f | [arg] -> doc_id_lem_ctor f ^^ space ^^ expY arg | _ -> - doc_id_lem_ctor f ^^ space ^^ + doc_id_lem_ctor f ^^ space ^^ parens (separate_map comma expY args) in if aexp_needed then parens (align epp) else epp | Base (_,External (Some "bitwise_not_bit"),_,_,_,_) -> let [a] = args in let epp = align (string "~" ^^ expY a) in if aexp_needed then parens (align epp) else epp - | _ -> + | _ -> let call = match annot with | Base(_,External (Some n),_,_,_,_) -> (match n with @@ -2455,7 +2418,7 @@ let doc_exp_lem, doc_let_lem = then (string (recordtyp ^ "_")) ^^ doc_id_lem id else doc_id_lem id in expY fexp ^^ dot ^^ fname - | _ -> + | _ -> raise (report l "E_field expression with no register or record type")) | E_block [] -> string "()" | E_block exps -> raise (report l "Blocks should have been removed till now.") @@ -2473,22 +2436,22 @@ let doc_exp_lem, doc_let_lem = (match alias_info with | Alias_field(reg,field) -> let epp = match t.t with - | Tid "bit" | Tabbrev (_,{t=Tid "bit"}) -> + | Tid "bit" | Tabbrev (_,{t=Tid "bit"}) -> (separate space) [string "read_reg_bitfield"; string reg;string_lit(string field)] - | _ -> + | _ -> (separate space) [string "read_reg_field"; string reg; string_lit(string field)] in if aexp_needed then parens (align epp) else epp | Alias_pair(reg1,reg2) -> - let epp = + let epp = if has_rreg_effect eff then separate space [string "read_two_regs";string reg1;string reg2] else separate space [string "RegisterPair";string reg1;string reg2] in if aexp_needed then parens (align epp) else epp | Alias_extract(reg,start,stop) -> - let epp = + let epp = if start = stop then (separate space) [string "access";doc_int start; @@ -2514,7 +2477,7 @@ let doc_exp_lem, doc_let_lem = let recordtyp = match t with | Tid recordtyp | Tabbrev ({t = Tid recordtyp},_) -> recordtyp - | _ -> raise (report l "cannot get record type") in + | _ -> raise (report l "cannot get record type") in let epp = anglebars (space ^^ (align (separate_map (semi_sp ^^ break 1) (doc_fexp regtypes recordtyp) fexps)) ^^ space) in @@ -2524,7 +2487,7 @@ let doc_exp_lem, doc_let_lem = let recordtyp = match t with | Tid recordtyp | Tabbrev ({t = Tid recordtyp},_) -> recordtyp - | _ -> raise (report l "cannot get record type") in + | _ -> raise (report l "cannot get record type") in anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp regtypes recordtyp) fexps)) | E_vector exps -> (match annot with @@ -2568,12 +2531,12 @@ let doc_exp_lem, doc_let_lem = | _ -> false, "false" in let start = match start.nexp with | Nconst i | N2n(_,Some i)-> string_of_big_int i - | N2n({nexp=Nconst i},_) -> string_of_int (Util.power 2 (int_of_big_int i)) + | N2n({nexp=Nconst i},_) -> string_of_int (Util.power 2 (int_of_big_int i)) | _ -> if dir then "0" else string_of_int (List.length iexps) in let size = match len.nexp with | Nconst i | N2n(_,Some i)-> string_of_big_int i | N2n({nexp=Nconst i},_) -> string_of_int (Util.power 2 (int_of_big_int i)) in - let default_string = + let default_string = match default with | Def_val_empty -> if is_bit_vector t then string "Undef" @@ -2583,7 +2546,7 @@ let doc_exp_lem, doc_let_lem = match t with | Tapp ("register", [TA_typ ({t = rt})]) -> - + let n = match rt with | Tapp ("vector",TA_nexp {nexp = Nconst i} :: TA_nexp {nexp = Nconst j} ::_) -> abs_big_int (sub_big_int i j) @@ -2620,7 +2583,7 @@ let doc_exp_lem, doc_let_lem = | E_list exps -> brackets (separate_map semi (expN) exps) | E_case(e,pexps) -> - + let only_integers (E_aux(_,(_,annot)) as e) = match annot with | Base((_,t),_,_,_,_,_) -> @@ -2635,10 +2598,10 @@ let doc_exp_lem, doc_let_lem = | _ -> expY e) | _ -> expY e in - + (* This is a hack, incomplete. It's because lem does not allow pattern-matching on integers *) - let epp = + let epp = group ((separate space [string "match"; only_integers e; string "with"]) ^/^ (separate_map (break 1) (doc_case regtypes) pexps) ^/^ (string "end")) in @@ -2656,7 +2619,7 @@ let doc_exp_lem, doc_let_lem = align (match name with | "power" -> aux2 "pow" - + | "bitwise_and_bit" -> aux "&." | "bitwise_or_bit" -> aux "|." | "bitwise_xor_bit" -> aux "+." @@ -2716,7 +2679,7 @@ let doc_exp_lem, doc_let_lem = | _ -> string name ^//^ parens (expN e1 ^^ comma ^/^ expN e2)) in if aexp_needed then parens (align epp) else epp - | _ -> + | _ -> let epp = align (doc_id_lem id ^//^ parens (expN e1 ^^ comma ^/^ expN e2)) in if aexp_needed then parens (align epp) else epp) @@ -2768,7 +2731,7 @@ let doc_exp_lem, doc_let_lem = top_exp regtypes true e]) | LEXP_id id -> doc_id_lem id | LEXP_cast (typ,id) -> doc_id_lem id - | _ -> + | _ -> raise (Reporting_basic.err_unreachable l ("doc_lexp_deref_lem: Shouldn't happen")) (* expose doc_exp_lem and doc_let *) in top_exp, let_exp @@ -2798,122 +2761,144 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with doc_op equals (concat [string "type"; space; doc_id_lem_type id;]) (doc_typquant_lem typq (anglebars (space ^^ align fs_doc ^^ space))) - | TD_variant(id,nm,typq,ar,_) -> - let ar_doc = group (separate_map (break 1) (doc_type_union_lem regtypes) ar) in - let typ_pp = (doc_op equals) - (concat [string "type"; space; doc_id_lem_type id;]) - (doc_typquant_lem typq ar_doc) in - let make_id pat id = - separate space [string "SIA.Id_aux"; - parens (string "SIA.Id " ^^ string_lit (doc_id id)); - if pat then underscore else string "SIA.Unknown"] in - let fromInterpValueF = concat [doc_id_lem_type id;string "FromInterpValue"] in - let toInterpValueF = concat [doc_id_lem_type id;string "ToInterpValue"] in - let fromInterpValuePP = - (prefix 2 1) - (separate space [string "let";fromInterpValueF;equals;string "function"]) - ( - ((separate_map (break 1)) - (fun (Tu_aux (tu,_)) -> - match tu with - | Tu_ty_id (ty,cid) -> - (separate space) - [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v"; - arrow; - doc_id_lem_ctor cid; - parens (string "fromInterpValue v")] - | Tu_id cid -> + | TD_variant(id,nm,typq,ar,_) -> + (match id with + | Id_aux ((Id "read_kind"),_) -> empty + | Id_aux ((Id "write_kind"),_) -> empty + | Id_aux ((Id "barrier_kind"),_) -> empty + | Id_aux ((Id "instruction_kind"),_) -> empty + | _ -> + let ar_doc = group (separate_map (break 1) (doc_type_union_lem regtypes) ar) in + let typ_pp = + + (doc_op equals) + (concat [string "type"; space; doc_id_lem_type id;]) + (doc_typquant_lem typq ar_doc) in + let make_id pat id = + separate space [string "SIA.Id_aux"; + parens (string "SIA.Id " ^^ string_lit (doc_id id)); + if pat then underscore else string "SIA.Unknown"] in + let fromInterpValueF = concat [doc_id_lem_type id;string "FromInterpValue"] in + let toInterpValueF = concat [doc_id_lem_type id;string "ToInterpValue"] in + let fromInterpValuePP = + (prefix 2 1) + (separate space [string "let";fromInterpValueF;equals;string "function"]) + ( + ((separate_map (break 1)) + (fun (Tu_aux (tu,_)) -> + match tu with + | Tu_ty_id (ty,cid) -> + (separate space) + [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v"; + arrow; + doc_id_lem_ctor cid; + parens (string "fromInterpValue v")] + | Tu_id cid -> + (separate space) + [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v"; + arrow; + doc_id_lem_ctor cid]) + ar) ^/^ + ((separate space) + [pipe;underscore;arrow;string "failwith"; + string_lit (concat [string "fromInterpValue";space;doc_id_lem_type id;colon; + space;string "unexpected value"])]) ^/^ + string "end") in + let toInterpValuePP = + (prefix 2 1) + (separate space [string "let";toInterpValueF;equals;string "function"]) + ( + ((separate_map (break 1)) + (fun (Tu_aux (tu,_)) -> + match tu with + | Tu_ty_id (ty,cid) -> + (separate space) + [pipe;doc_id_lem_ctor cid;string "v";arrow; + string "SI.V_ctor"; + parens (make_id false cid); + parens (string "SIA.T_id " ^^ string_lit (doc_id id)); + string "SI.C_Union"; + parens (string "toInterpValue v")] + | Tu_id cid -> + (separate space) + [pipe;doc_id_lem_ctor cid;arrow; + string "SI.V_ctor"; + parens (make_id false cid); + parens (string "SIA.T_id " ^^ string_lit (doc_id id)); + string "SI.C_Union"; + parens (string "toInterpValue ()")]) + ar) ^/^ + string "end") in + let fromToInterpValuePP = + ((prefix 2 1) + (concat [string "instance ";parens (string "ToFromInterpValue " ^^ doc_id_lem_type id)]) + (concat [string "let toInterpValue = ";toInterpValueF;hardline; + string "let fromInterpValue = ";fromInterpValueF])) + ^/^ string "end" in + typ_pp ^^ hardline ^^ hardline ^^ + fromInterpValuePP ^^ hardline ^^ hardline ^^ + toInterpValuePP ^^ hardline ^^ hardline ^^ + fromToInterpValuePP ^^ hardline) + | TD_enum(id,nm,enums,_) -> + (match id with + | Id_aux ((Id "read_kind"),_) -> empty + | Id_aux ((Id "write_kind"),_) -> empty + | Id_aux ((Id "barrier_kind"),_) -> empty + | Id_aux ((Id "instruction_kind"),_) -> empty + | _ -> + let rec range i j = if i > j then [] else i :: (range (i+1) j) in + let nats = range 0 in + let enums_doc = group (separate_map (break 1 ^^ pipe ^^ space) doc_id_lem_ctor enums) in + let typ_pp = (doc_op equals) + (concat [string "type"; space; doc_id_lem_type id;]) + (enums_doc) in + let fromInterpValueF = concat [doc_id_lem_type id;string "FromInterpValue"] in + let toInterpValueF = concat [doc_id_lem_type id;string "ToInterpValue"] in + let make_id pat id = + separate space [string "SIA.Id_aux"; + parens (string "SIA.Id " ^^ string_lit (doc_id id)); + if pat then underscore else string "SIA.Unknown"] in + let fromInterpValuePP = + (prefix 2 1) + (separate space [string "let";fromInterpValueF;equals;string "function"]) + ( + ((separate_map (break 1)) + (fun cid -> (separate space) [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v"; arrow; doc_id_lem_ctor cid]) - ar) ^/^ - string "end") in - let toInterpValuePP = - (prefix 2 1) - (separate space [string "let";toInterpValueF;equals;string "function"]) - ( - ((separate_map (break 1)) - (fun (Tu_aux (tu,_)) -> - match tu with - | Tu_ty_id (ty,cid) -> - (separate space) - [pipe;doc_id_lem_ctor cid;string "v";arrow; - string "SI.V_ctor"; - parens (make_id false cid); - parens (string "SIA.T_id " ^^ string_lit (doc_id id)); - string "SI.C_Union"; - parens (string "toInterpValue v")] - | Tu_id cid -> + enums) ^/^ + ((separate space) + [pipe;underscore;arrow;string "failwith"; + string_lit (concat [string "fromInterpValue";space;doc_id_lem_type id;colon; + space;string "unexpected value"])]) ^/^ + string "end") in + let toInterpValuePP = + (prefix 2 1) + (separate space [string "let";toInterpValueF;equals;string "function"]) + ( + ((separate_map (break 1)) + (fun (cid,number) -> (separate space) [pipe;doc_id_lem_ctor cid;arrow; string "SI.V_ctor"; parens (make_id false cid); parens (string "SIA.T_id " ^^ string_lit (doc_id id)); - string "SI.C_Union"; + parens (string ("SI.C_Enum " ^ string_of_int number)); parens (string "toInterpValue ()")]) - ar) ^/^ - string "end") in - let fromToInterpValuePP = - ((prefix 2 1) - (concat [string "instance ";parens (string "ToFromInterpValue " ^^ doc_id_lem_type id)]) - (concat [string "let toInterpValue = ";toInterpValueF;hardline; - string "let fromInterpValue = ";fromInterpValueF])) - ^/^ string "end" in - typ_pp ^^ hardline ^^ hardline ^^ - fromInterpValuePP ^^ hardline ^^ hardline ^^ - toInterpValuePP ^^ hardline ^^ hardline ^^ - fromToInterpValuePP ^^ hardline - | TD_enum(id,nm,enums,_) -> - let rec range i j = if i > j then [] else i :: (range (i+1) j) in - let nats = range 0 in - let enums_doc = group (separate_map (break 1 ^^ pipe ^^ space) doc_id_lem_ctor enums) in - let typ_pp = (doc_op equals) - (concat [string "type"; space; doc_id_lem_type id;]) - (enums_doc) in - let fromInterpValueF = concat [doc_id_lem_type id;string "FromInterpValue"] in - let toInterpValueF = concat [doc_id_lem_type id;string "ToInterpValue"] in - let make_id pat id = - separate space [string "SIA.Id_aux"; - parens (string "SIA.Id " ^^ string_lit (doc_id id)); - if pat then underscore else string "SIA.Unknown"] in - let fromInterpValuePP = - (prefix 2 1) - (separate space [string "let";fromInterpValueF;equals;string "function"]) - ( - ((separate_map (break 1)) - (fun cid -> - (separate space) - [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v"; - arrow; - doc_id_lem_ctor cid]) - enums) ^/^ - string "end") in - let toInterpValuePP = - (prefix 2 1) - (separate space [string "let";toInterpValueF;equals;string "function"]) - ( - ((separate_map (break 1)) - (fun (cid,number) -> - (separate space) - [pipe;doc_id_lem_ctor cid;arrow; - string "SI.V_ctor"; - parens (make_id false cid); - parens (string "SIA.T_id " ^^ string_lit (doc_id id)); - parens (string ("SI.C_Enum " ^ string_of_int number)); - parens (string "toInterpValue ()")]) - (List.combine enums (nats ((List.length enums) - 1)))) ^/^ - string "end") in - let fromToInterpValuePP = - ((prefix 2 1) - (concat [string "instance ";parens (string "ToFromInterpValue " ^^ doc_id_lem_type id)]) - (concat [string "let toInterpValue = ";toInterpValueF;hardline; - string "let fromInterpValue = ";fromInterpValueF])) - ^/^ string "end" in - typ_pp ^^ hardline ^^ hardline ^^ - fromInterpValuePP ^^ hardline ^^ hardline ^^ - toInterpValuePP ^^ hardline ^^ hardline ^^ - fromToInterpValuePP ^^ hardline + (List.combine enums (nats ((List.length enums) - 1)))) ^/^ + string "end") in + let fromToInterpValuePP = + ((prefix 2 1) + (concat [string "instance ";parens (string "ToFromInterpValue " ^^ doc_id_lem_type id)]) + (concat [string "let toInterpValue = ";toInterpValueF;hardline; + string "let fromInterpValue = ";fromInterpValueF])) + ^/^ string "end" in + typ_pp ^^ hardline ^^ hardline ^^ + fromInterpValuePP ^^ hardline ^^ hardline ^^ + toInterpValuePP ^^ hardline ^^ hardline ^^ + fromToInterpValuePP ^^ hardline) | TD_register(id,n1,n2,rs) -> match n1,n2 with | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) -> @@ -2997,7 +2982,7 @@ let doc_dec_lem (DEC_aux (reg,(l,annot))) = |_-> empty) | _ -> empty) | DEC_alias(id,alspec) -> empty - | DEC_typ_alias(typ,id,alspec) -> empty + | DEC_typ_alias(typ,id,alspec) -> empty let doc_spec_lem regtypes (VS_aux (valspec,annot)) = match valspec with @@ -3005,8 +2990,8 @@ let doc_spec_lem regtypes (VS_aux (valspec,annot)) = | VS_extern_spec _ -> empty (* ignore these at the moment *) | VS_val_spec (typschm,id) -> separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem regtypes typschm] ^/^ hardline - - + + let doc_def_lem regtypes def = match def with | DEF_default df -> empty | DEF_spec v_spec -> doc_spec_lem regtypes v_spec @@ -3020,7 +3005,7 @@ let doc_def_lem regtypes def = match def with let doc_defs_lem regtypes (Defs defs) = separate_map empty (doc_def_lem regtypes) defs -let find_regtypes (Defs defs) = +let find_regtypes (Defs defs) = List.fold_left (fun acc def -> match def with @@ -3036,7 +3021,7 @@ let pp_defs_lem f d top_line opens = let regtypes = find_regtypes d in let defs = doc_defs_lem regtypes d in (print f) - (concat + (concat [string "(*" ^^ (string top_line) ^^ string "*)";hardline; (separate_map hardline) (fun lib -> separate space [string "open import";string lib]) opens;hardline; @@ -3045,6 +3030,6 @@ let pp_defs_lem f d top_line opens = hardline; string "module SI = Interp"; hardline; string "module SIA = Interp_ast"; hardline; + string "module SV = Sail_values"; hardline; hardline; defs]) - diff --git a/src/process_file.ml b/src/process_file.ml index 16feb92b..3012b288 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -177,13 +177,13 @@ let output1 libpath out_arg filename defs = let ((o,_, _) as ext_o) = open_output_with_check_unformatted (f' ^ "_embedded.lem") in (Pretty_print.pp_defs_lem o defs (generated_line filename)) - ["Pervasives_extra";"Sail_impl_base";"Vector";"Prompt";"Sail_values"]; + ["Pervasives_extra";"Sail_impl_base";"Prompt";"Sail_values"]; close_output_with_check ext_o | Lem_out (Some lib) -> let ((o,_, _) as ext_o) = open_output_with_check_unformatted (f' ^ "_embedded.lem") in (Pretty_print.pp_defs_lem o defs (generated_line filename)) - ["Pervasives_extra";"Sail_impl_base";"Vector";"Prompt";"Sail_values";lib]; + ["Pervasives_extra";"Sail_impl_base";"Prompt";"Sail_values";lib]; close_output_with_check ext_o; | Ocaml_out None -> let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in |