sail-to-lem progress

6 files changed, 147 insertions, 145 deletions

diff --git a/src/gen_lib/power_extras.lem b/src/gen_lib/power_extras.lem
index b43c6403..e08da230 100644
--- a/src/gen_lib/power_extras.lem
+++ b/src/gen_lib/power_extras.lem
@@ -27,10 +27,10 @@ let MEMr (addr,l) = read_memory (unsigned addr) l
 let MEMr_reserve (addr,l) = read_memory (unsigned addr) l
 
 let MEMw_EA (addr,l) = write_writeEA (unsigned addr) l
-let MEMw_EA_conditional (addr,l) = write_writeEA (unsigned addr) l
+let MEMw_EA_cond (addr,l) = write_writeEA (unsigned addr) l
                                         
 let MEMw (addr,l,value) = write_memory (unsigned addr) l value
-let MEMw_conditional (addr,l,value) = write_memory (unsigned addr) l value >> return true
+let MEMw_conditional (addr,l,value) = write_memory (unsigned addr) l value >> return I
 
 let I_Sync () = return ()
 let H_Sync () = return ()
@@ -39,7 +39,7 @@ let EIEIO_Sync () = return ()
 
 let recalculate_dependency () = return ()
 
-let trap () = exit ()
+let trap () = exit "error"
 (* this needs to change, but for that we'd have to make the type checker know about trap 
  * as an effect *)
 
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 738a0b20..4cd76156 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -1,4 +1,4 @@
-open import Pervasves_extra
+open import Pervasives_extra
 open import Vector
 open import Arch
 
@@ -83,47 +83,47 @@ type reg_name =
    * specifies a part of the field, indexed w.r.t. the register as a whole *)
   | Reg_f_slice of string * nat * direction * string * slice * slice 
 
-type outcome 'a =
+type outcome 'e 'a =
   (* Request to read memory, value is location to read followed by registers that location depended 
    * on when mode.track_values, integer is size to read, followed by registers that were used in 
    * computing that size *)
   (* address_lifted should go away: doesn't make sense to allow for undefined bits in addresses *)
   | Read_mem of read_kind * address_lifted * nat * maybe (list reg_name) *
-                  (memory_value -> outcome 'a)
+                  (memory_value -> outcome 'e 'a)
                     
   (* Request to write memory, first value and dependent registers is location, second is the value 
    * to write *)
   | Write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value *
-                   maybe (list reg_name) * (bool -> outcome 'a)
+                   maybe (list reg_name) * (bool -> outcome 'e 'a)
                                              
   (* Tell the system a write is imminent, at address lifted tanted by register list, of size nat *)
-  | Write_ea of write_kind * address_lifted * nat * maybe (list reg_name) * outcome 'a
+  | Write_ea of write_kind * address_lifted * nat * maybe (list reg_name) * outcome 'e 'a
                                                                               
   (* Request to write memory at last signaled address. Memory value should be 8* the size given in 
    * ea signal *)
-  | Write_memv of memory_value * maybe (list reg_name) * (bool -> outcome 'a)
+  | Write_memv of memory_value * maybe (list reg_name) * (bool -> outcome 'e 'a)
                                                            
   (* Request a memory barrier *)
   (* outcome 'a used to be (unit -> outcome 'a), but since the code is purely functional we don't 
    * need that *)
-  | Barrier of barrier_kind * outcome 'a
+  | Barrier of barrier_kind * outcome 'e 'a
                                 
   (* Tell the system to dynamically recalculate dependency footprint *)
-  | Footprint of outcome 'a
+  | Footprint of outcome 'e 'a
                    
   (* Request to read register *)
-  | Read_reg of reg_name * (register_value -> outcome 'a)
+  | Read_reg of reg_name * (register_value -> outcome 'e 'a)
                              
   (* Request to write register *)
-  | Write_reg of reg_name * register_value * outcome 'a
+  | Write_reg of reg_name * register_value * outcome 'e 'a
                                                
   (* List of instruction states to be run in parrallel, any order permitted.
      Expects concurrency model to choose an order: a permutation of the original list *)
-  | Nondet_choice of list (outcome unit) * (list (outcome unit) -> outcome 'a)
+  | Nondet_choice of unit
                                                 
   (* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally 
    * provide a handler. *)
-  | Escape of (outcome unit) (* currently without handlers *) (* of maybe (unit -> outcome 'a) *)
+  | Escape of 'e (* currently without handlers *) (* of maybe (unit -> outcome 'a) *)
 
   (* Stop for incremental stepping, function can be used to display function call data *)
   | Done of 'a
@@ -133,12 +133,7 @@ type M 'e 'a = outcome 'e 'a
 val return : forall 'e 'a. 'a -> M 'e 'a
 let return a = Done a
 
-val (>>=) : forall 'a 'b. M 'a -> ('a -> M 'b) -> M 'b
-val (>>>) : forall 'a 'b 'c. ('a -> M 'b) -> ('b -> M 'c) -> ('a -> M 'c)
-
-val (>>) : forall 'b. M unit -> (unit -> M 'b) -> M 'b
-let (>>) m n = m >>= fun _ -> n
-
+val (>>=) : forall 'e 'a 'b. M 'e 'a -> ('a -> M 'e 'b) -> M 'e 'b
 let rec (>>=) m f = match m with
   | Done a -> f a
   | Read_mem rk addr sz rs k ->        Read_mem rk addr sz rs        (fun v -> (k v) >>= f)
@@ -149,12 +144,15 @@ let rec (>>=) m f = match m with
   | Footprint k ->                     Footprint                     (k >>= f)
   | Read_reg reg k ->                  Read_reg reg                  (fun v -> (k v) >>= f)
   | Write_reg reg v k ->               Write_reg reg v               (k >>= f)
-  | Nondet_choice actions k ->         Nondet_choice actions         (fun c -> (k c) >>= f)
-  | Escape -> Escape
+  | Nondet_choice () -> Nondet_choice ()
+  | Escape e -> Escape e
   end
 
-val exit : forall 'a 'e. 'e -> M 'a
-let exit _ = Escape
+val (>>) : forall 'e 'b. M 'e unit -> M 'e 'b -> M 'e 'b
+let (>>) m n = m >>= fun _ -> n
+
+val exit : forall 'a 'e. 'e -> M 'e 'a
+let exit = Escape
 
 val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
 let rec byte_chunks n list = match (n,list) with
@@ -164,40 +162,40 @@ let rec byte_chunks n list = match (n,list) with
 end
 
 val bitvFromBytes : list byte -> vector bit
-let bitvFromBytes v = V (foldl (++) [] v) 0 defaultDir
+let bitvFromBytes v = Vector (foldl (++) [] v) 0 defaultDir
 
 let dir is_inc = if is_inc then D_increasing else D_decreasing
 
 val bitvFromRegisterValue : register_value -> vector bit
 let bitvFromRegisterValue v =
-  V (v.rv_bits) (integerFromNat (v.rv_start)) (v.rv_dir = D_increasing)
+  Vector (v.rv_bits) (integerFromNat (v.rv_start)) (v.rv_dir = D_increasing)
 
 val registerValueFromBitv : vector bit -> register -> register_value
-let registerValueFromBitv (V bits start is_inc) reg = 
+let registerValueFromBitv (Vector bits start is_inc) reg = 
   let start = natFromInteger start in
   <| rv_bits = bits;
      rv_dir = dir is_inc;
      rv_start_internal = start;
      rv_start = start+1 - (natFromInteger (length_reg reg)) |>
 
-val read_memory : read_kind -> integer -> integer -> M (vector bit)
+val read_memory : forall 'e. read_kind -> integer -> integer -> M 'e (vector bit)
 let read_memory rk addr sz =
   let sz = natFromInteger sz in
   Read_mem rk addr sz Nothing (compose Done bitvFromBytes)
 
-val write_memory : write_kind -> integer -> integer -> vector bit -> M bool
-let write_memory wk addr sz (V v _ _) =
+val write_memory : forall 'e. write_kind -> integer -> integer -> vector bit -> M 'e bool
+let write_memory wk addr sz (Vector v _ _) =
   let sz = natFromInteger sz in
   Write_mem wk addr sz Nothing (byte_chunks sz v) Nothing Done
 
-val read_reg_range : register -> (integer * integer) -> M (vector bit)
+val read_reg_range : forall 'e. register -> (integer * integer) -> M 'e (vector bit)
 let read_reg_range reg (i,j) =
   let (i,j) = (natFromInteger i,natFromInteger j) in
   let start = natFromInteger (start_index_reg reg) in
   let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
   Read_reg reg (compose Done bitvFromRegisterValue)
 
-val write_reg_range : register -> (integer * integer) -> vector bit -> M unit
+val write_reg_range : forall 'e. register -> (integer * integer) -> vector bit -> M 'e unit
 let write_reg_range reg (i,j) v =
   let rv = registerValueFromBitv v reg in
   let start = natFromInteger (start_index_reg reg) in
@@ -205,24 +203,24 @@ let write_reg_range reg (i,j) v =
   let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
   Write_reg reg rv (Done ())
 
-val read_reg_bit : register -> integer -> M bit
+val read_reg_bit : forall 'e. register -> integer -> M 'e bit
 let read_reg_bit reg i = 
   let i = natFromInteger i in
   let start = natFromInteger (start_index_reg reg) in
   let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,i) in
   Read_reg reg (fun v -> Done (access (bitvFromRegisterValue v) 1))
 
-val write_reg_bit : register -> integer -> bit -> M unit
-let write_reg_bit reg i bit = write_reg_range reg (i,i) (V [bit] 0 true)
+val write_reg_bit : forall 'e. register -> integer -> bit -> M 'e unit
+let write_reg_bit reg i bit = write_reg_range reg (i,i) (Vector [bit] 0 true)
 
-val read_reg : register -> M (vector bit)
+val read_reg : forall 'e. register -> M 'e (vector bit)
 let read_reg reg =
   let start = natFromInteger (start_index_reg reg) in
   let sz = natFromInteger (length_reg reg) in
   let reg = Reg (register_to_string reg) start sz (dir defaultDir) in
   Read_reg reg (compose Done bitvFromRegisterValue)
 
-val write_reg : register -> vector bit -> M unit
+val write_reg : forall 'e. register -> vector bit -> M 'e unit
 let write_reg reg v =
   let rv = registerValueFromBitv v reg in
   let start = natFromInteger (start_index_reg reg) in
@@ -230,7 +228,7 @@ let write_reg reg v =
   let reg = Reg (register_to_string reg) start sz (dir defaultDir) in
   Write_reg reg rv (Done ())
 
-val read_reg_field : register -> register_field -> M (vector bit)
+val read_reg_field : forall 'e. register -> register_field -> M 'e (vector bit)
 let read_reg_field reg rfield = 
   let (i,j) =
     let (i,j) = field_indices rfield in
@@ -239,36 +237,17 @@ let read_reg_field reg rfield =
   let reg = Reg_slice (register_to_string reg) start (dir defaultDir) (i,j) in
   Read_reg reg (compose Done bitvFromRegisterValue)
 
-val write_reg_field : register -> register_field -> vector bit -> M unit
+val write_reg_field : forall 'e. register -> register_field -> vector bit -> M 'e unit
 let write_reg_field reg rfield = write_reg_range reg (field_indices rfield)
 
-val read_reg_bitfield : register -> register_bitfield -> M bit
+val read_reg_bitfield : forall 'e. register -> register_bitfield -> M 'e bit
 let read_reg_bitfield reg rbit = read_reg_bit reg (field_index_bit rbit)
 
-val write_reg_bitfield : register -> register_bitfield -> bit -> M unit
+val write_reg_bitfield : forall 'e. register -> register_bitfield -> bit -> M 'e unit
 let write_reg_bitfield reg rbit = write_reg_bit reg (field_index_bit rbit)
 
-val foreach_inc :  forall 'vars. (integer * integer * integer) (*(nat * nat * nat)*) -> 'vars ->
-                  (integer (*nat*) -> 'vars -> (unit * 'vars)) -> (unit * 'vars)
-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
-  else ((),vars)
-
-val foreach_dec : forall 'vars. (integer * integer * integer) (*(nat * nat * nat)*) -> 'vars ->
-                  (integer (*nat*) -> 'vars -> (unit * 'vars)) -> (unit * 'vars)
-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
-  else ((),vars)
-
-
-val foreachM_inc : forall 'vars. (nat * nat * nat) -> 'vars ->
-                  (nat -> 'vars -> M (unit * 'vars)) -> M (unit * 'vars)
+val foreachM_inc : forall 'e 'vars. (nat * nat * nat) -> 'vars ->
+                  (nat -> 'vars -> M 'e (unit * 'vars)) -> M 'e (unit * 'vars)
 let rec foreachM_inc (i,stop,by) vars body = 
   if i <= stop
   then
@@ -277,8 +256,8 @@ let rec foreachM_inc (i,stop,by) vars body =
   else return ((),vars)
 
 
-val foreachM_dec : forall 'vars. (nat * nat * nat) -> 'vars ->
-                  (nat -> 'vars -> M (unit * 'vars)) -> M (unit * 'vars)
+val foreachM_dec : forall 'e 'vars. (nat * nat * nat) -> 'vars ->
+                  (nat -> 'vars -> M 'e (unit * 'vars)) -> M 'e (unit * 'vars)
 let rec foreachM_dec (i,stop,by) vars body = 
   if i >= stop
   then
@@ -287,8 +266,6 @@ let rec foreachM_dec (i,stop,by) vars body =
   else return ((),vars)
 
 
-let length l = integerFromNat (length l)
-
 let write_two_regs r1 r2 vec =
   let size = length_reg r1 in
   let start = get_start vec in
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 3914bdef..b9a4fbd1 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -3,12 +3,8 @@ open import Vector
 open import Arch
 
 type i = integer
-type number = integer
-
 type n = natural
 
-let length l = integerFromNat (length l)
-
 let has_undef (Vector bs _ _) = List.any (function Undef -> true | _ -> false end) bs
 
 let most_significant = function
@@ -407,10 +403,9 @@ let duplicate (bit,length) =
   Vector (List.replicate (natFromInteger length) bit) 0 true
 
 val repeat : forall 'a. list 'a -> integer -> list 'a
-let rec repeat xs = function
-  | 0 -> []
-  | n -> xs ++ repeat xs (n-1)
-  end
+let rec repeat xs n =
+  if n = 0 then []
+  else xs ++ repeat xs (n-1)
 
 let duplicate_bits (Vector bits start direction,len) = 
   let bits' = repeat bits len in
@@ -502,25 +497,52 @@ let mask (n,Vector bits start dir) =
 
 
 
-(* this is for a temporary workaround int/nat/integer/natural issues*)
-
-class (subInteger 'a)
-  val toInteger : 'a -> integer
+class (ToNatural 'a)
+  val toNatural : 'a -> natural
 end
 
 
-instance (subInteger integer)
-  let toInteger = id
+instance (ToNatural integer)
+  let toNatural = naturalFromInteger
 end
 
-instance (subInteger int)
-  let toInteger = integerFromInt
+instance (ToNatural int)
+  let toNatural = naturalFromInt
 end
 
-instance (subInteger nat)
-  let toInteger = integerFromNat
+instance (ToNatural nat)
+  let toNatural = naturalFromNat
 end
 
-instance (subInteger natural)
-  let toInteger = integerFromNatural
+instance (ToNatural natural)
+  let toNatural = id
 end
+
+
+let toNaturalFiveTup (n1,n2,n3,n4,n5) =
+  (toNatural n1,
+   toNatural n2,
+   toNatural n3,
+   toNatural n4,
+   toNatural n5)
+
+
+
+
+val foreach_inc :  forall 'vars. (integer * integer * integer) (*(nat * nat * nat)*) -> 'vars ->
+                  (integer (*nat*) -> 'vars -> (unit * 'vars)) -> (unit * 'vars)
+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
+  else ((),vars)
+
+val foreach_dec : forall 'vars. (integer * integer * integer) (*(nat * nat * nat)*) -> 'vars ->
+                  (integer (*nat*) -> 'vars -> (unit * 'vars)) -> (unit * 'vars)
+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
+  else ((),vars)
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 6db45002..51658d6e 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -1,6 +1,7 @@
 open import Pervasives_extra
 open import Vector
 open import Arch
+open import Sail_values
 
 (* 'a is result type, 'e is error type *)
 type State 's 'e 'a = 's -> (either 'a 'e * 's)
@@ -21,23 +22,23 @@ let rec ints_aux acc x =
 
 let ints = ints_aux []
 
+type M 'e 'a = State state 'e 'a
+                     
 val return : forall 's 'e 'a. 'a -> State 's 'e 'a
 let return a s = (Left a,s)
 
-val bind : forall 's 'e 'a 'b. State 's 'e 'a -> ('a -> State 's 'e 'b) -> State 's 'e 'b
-let bind m f s = match m s with
+val (>>=) : forall 's 'e 'a 'b. State 's 'e 'a -> ('a -> State 's 'e 'b) -> State 's 'e 'b
+let (>>=) m f s = match m s with
   | (Left a,s') -> f a s'
   | (Right error,s') -> (Right error,s')
   end
 
-val exit : forall 's 'e 'a. 'e -> State 's 'e 'a
-let exit e s = (Right e,s)
-
-let (>>=) = bind
-
 val (>>): forall 's 'e 'b. State 's 'e unit -> State 's 'e 'b -> State 's 'e 'b
 let (>>) m n = m >>= fun _ -> n
 
+val exit : forall 's 'e 'a. 'e -> State 's 'e 'a
+let exit e s = (Right e,s)
+
 let assert' b msg_opt =
   let msg = match msg_opt with
   | Just msg -> msg
@@ -115,46 +116,6 @@ val write_reg : forall 'e. register -> vector bit -> State state 'e unit
 let write_reg reg v s =
   let s' = write_regstate s reg v in
   (Left (),s')
-    
-
-val foreach_inc :  forall 's 'e 'vars. (integer * integer * integer) (*(nat * nat * nat)*) -> 'vars ->
-                  (integer (*nat*) -> 'vars -> (unit * 'vars)) -> (unit * 'vars)
-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
-  else ((),vars)
-
-
-val foreach_dec : forall 's 'e 'vars. (integer * integer * integer) (*(nat * nat * nat)*) -> 'vars ->
-                  (integer (*nat*) -> 'vars -> (unit * 'vars)) -> (unit * 'vars)
-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
-  else ((),vars)
-
-
-val foreachM_inc : forall 's 'e 'vars. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> State 's 'e (unit * 'vars)) -> State 's 'e (unit * 'vars)
-let rec foreachM_inc (i,stop,by) vars body = 
-  if i <= stop
-  then
-    body i vars >>= fun (_,vars) ->
-    foreachM_inc (i + by,stop,by) vars body
-  else return ((),vars)
-
-
-val foreachM_dec : forall 's 'e 'vars. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> State 's 'e (unit * 'vars)) -> State 's 'e (unit * 'vars)
-let rec foreachM_dec (i,stop,by) vars body = 
-  if i >= stop
-  then
-    body i vars >>= fun (_,vars) ->
-    foreachM_dec (i - by,stop,by) vars body
-  else return ((),vars)
 
 val read_reg_field : forall 'e. register -> register_field -> State state 'e (vector bit)
 let read_reg_field reg rfield = uncurry (read_reg_range reg) (field_indices rfield)
@@ -180,10 +141,6 @@ let write_reg_field_bit reg rfield i v =
   let (i',_) = field_indices rfield in
   write_reg_bit reg (i + i') v
 
-
-
-let length l = integerFromNat (length l)
-
 let write_two_regs r1 r2 vec =
   let size = length_reg r1 in
   let start = get_start vec in
@@ -200,4 +157,21 @@ let read_two_regs r1 r2 =
   read_reg r2 >>= fun v2 ->
   return (v1 ^^ v2)
 
-type M 'e 'a = State state 'e 'a
+val foreachM_inc : forall 'e 'vars. (i * i * i) -> 'vars ->
+                  (i -> 'vars -> M 'e (unit * 'vars)) -> M 'e (unit * 'vars)
+let rec foreachM_inc (i,stop,by) vars body = 
+  if i <= stop
+  then
+    body i vars >>= fun (_,vars) ->
+    foreachM_inc (i + by,stop,by) vars body
+  else return ((),vars)
+
+
+val foreachM_dec : forall 'e 'vars. (i * i * i) -> 'vars ->
+                  (i -> 'vars -> M 'e (unit * 'vars)) -> M 'e (unit * 'vars)
+let rec foreachM_dec (i,stop,by) vars body = 
+  if i >= stop
+  then
+    body i vars >>= fun (_,vars) ->
+    foreachM_dec (i - by,stop,by) vars body
+  else return ((),vars)
diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem
index 72c8b584..7c22e3ba 100644
--- a/src/gen_lib/vector.lem
+++ b/src/gen_lib/vector.lem
@@ -1,6 +1,8 @@
 open import Pervasives_extra
 
 type bit = O | I | Undef
+
+(* element list * start * has increasing direction *)
 type vector 'a = Vector of list 'a * integer * bool
 
 let rec nth xs (n : integer) =
@@ -16,7 +18,7 @@ let to_bool = function
   end
 
 let get_start (Vector _ s _) = s
-let length (Vector bs _ _) = length bs
+let length (Vector bs _ _) = integerFromNat (length bs)
 
 let rec replace bs ((n : integer),b') = match bs with
   | [] -> []
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index cd0392b0..3b8b657c 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -2068,7 +2068,6 @@ let doc_id_lem (Id_aux(i,_)) =
 
 let doc_id_lem_type (Id_aux(i,_)) =
   match i with
-  | Id("bit") -> string "bit"
   | Id("int") -> string "integer"
   | Id("nat") -> string "integer"
   | Id("option") -> string "maybe"
@@ -2103,6 +2102,14 @@ let effectful (Effect_aux (eff,_)) =
          | _ -> false)
        effs
 
+let rec is_number {t=t} =
+  match t with
+  | Tabbrev (t1,t2) -> is_number t1 || is_number t2
+  | Tapp ("range",_) 
+  | Tapp ("implicit",_)
+  | Tapp ("atom",_) -> true
+  | _ -> false
+
 let doc_typ_lem, doc_atomic_typ_lem =
   (* following the structure of parser for precedence *)
   let rec typ regtypes ty = fn_typ true regtypes ty
@@ -2128,11 +2135,11 @@ let doc_typ_lem, doc_atomic_typ_lem =
          let tpp = string "vector" ^^ space ^^ typ regtypes typa in
          if atyp_needed then parens tpp else tpp
       | Typ_app(Id_aux (Id "range", _),_) ->
-         (string "number")
+         (string "integer")
       | Typ_app(Id_aux (Id "implicit", _),_) ->
          (string "integer")
       | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) ->
-         (string "number")
+         (string "integer")
       | 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
@@ -2169,7 +2176,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 i < 0 then "((0"^ipp^") : i)" else "("^ipp^" : i)"
+     if in_pat then  "("^ipp^" : n)" 
+     else if i < 0 then "((0"^ipp^") : i)"
+     else "("^ipp^" : i)"
   | 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 ->
@@ -2608,9 +2617,27 @@ let doc_exp_lem, doc_let_lem =
   | E_list exps ->
       brackets (separate_map semi (top_exp (regs,regtypes) false) exps)
   | E_case(e,pexps) ->
+
+     let only_integers (E_aux(_,(_,annot)) as e) =
+       match annot with
+       | Base((_,t),_,_,_,_,_) ->
+          if is_number t then
+            let e_pp = top_exp (regs,regtypes) true e in
+            align (string "toNatural" ^//^ e_pp)
+          else
+            (match t with
+             | {t = Ttup ([t1;t2;t3;t4;t5] as ts)} when List.for_all is_number ts ->
+                let e_pp = top_exp (regs,regtypes) true e in
+                align (string "toNaturalFiveTup" ^//^ e_pp)
+             | _ -> exp e)
+       | _ -> exp e
+      in
+
+     (* This is a hack, incomplete. It's because lem does not allow
+        pattern-matching on integers *)
      let epp = 
        (prefix 0 1)
-         (separate space [string "match"; exp e; string "with"])
+         (separate space [string "match"; only_integers e; string "with"])
          (separate_map (break 1) (doc_case (regs,regtypes)) pexps) ^^ (break 1) ^^
          (string "end" ^^ (break 1)) in
      if aexp_needed then parens (align epp) else epp