sail changes for making lem embedding Isabelle-friendlier

1 files changed, 56 insertions, 55 deletions

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