Replace nat by natural in interpreter

2 files changed, 29 insertions, 20 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index bc9d33b2..a9e87056 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -20,7 +20,7 @@ type value =
  | V_lit of lit
  | V_tuple of list value
  | V_list of list value
- | V_vector of nat * bool * list value (* The nat stores the first index, the bool whether that's most or least significant *)
+ | V_vector of natural * bool * list value (* The nat stores the first index, the bool whether that's most or least significant *)
  | V_record of list (id * value)
  | V_ctor of id * value
 
@@ -35,10 +35,10 @@ type reg_form =
 
 (* These may need to be refined or expanded based on memory requirement *)
 type action = 
- | Read_reg of reg_form * maybe (nat * nat)
- | Write_reg of reg_form * maybe (nat* nat) * value
- | Read_mem of id * value * maybe (nat * nat)
- | Write_mem of id * value * maybe (nat * nat) * value
+ | Read_reg of reg_form * maybe (natural * natural)
+ | Write_reg of reg_form * maybe (natural* natural) * value
+ | Read_mem of id * value * maybe (natural * natural)
+ | Write_mem of id * value * maybe (natural * natural) * value
  | Call_extern of string * value
 
 (* Inverted call stack, where top item on the stack is waiting for an action and all other frames for the right stack *)
@@ -181,16 +181,24 @@ let litV_to_vec l =
     V_vector 0 true bits
   end
 
-val access_vector : value -> nat -> value
+(* Like List_extra.nth with a natural instead of nat index -
+ * using an unsafe coercion. *)
+val list_nth : forall 'a . list 'a -> natural -> 'a
+let list_nth l n = List_extra.nth l (natFromNatural n)
+
+val list_length : forall 'a . list 'a -> natural
+let list_length l = naturalFromNat (List.length l)
+
+val access_vector : value -> natural -> value
 let access_vector v n =
   match v with
   | V_vector m inc vs -> 
     if inc then
-    List_extra.nth vs (n - m)
-    else List_extra.nth vs (m - n)
+    list_nth vs (n - m)
+    else list_nth vs (m - n)
   end
 
-val from_n_to_n :forall 'a. nat -> nat -> nat -> list 'a -> list 'a
+val from_n_to_n :forall 'a. natural -> natural -> natural -> list 'a -> list 'a
 let rec from_n_to_n from to_ acc ls =
   match ls with
   | [] -> []
@@ -202,7 +210,7 @@ let rec from_n_to_n from to_ acc ls =
     else from_n_to_n from to_ (acc + 1) ls
   end
 
-val slice_vector : value -> nat -> nat -> value
+val slice_vector : value -> natural -> natural -> value
 let slice_vector v n1 n2 =
   match v with
   | V_vector m inc vs ->
@@ -238,14 +246,14 @@ let rec update_vector_slice vector value mem =
       mem vs
 end
 
-val fupdate_vec : value -> nat -> value -> value
+val fupdate_vec : value -> natural -> value -> value
 let fupdate_vec v n vexp =
   match v with
   | V_vector m inc vals -> 
-    V_vector m inc (List.update vals (if inc then (n-m) else (m-n)) vexp)
+    V_vector m inc (List.update vals (natFromNatural (if inc then (n-m) else (m-n))) vexp)
   end
 
-val replace_is : forall 'a. list 'a -> list 'a -> nat -> nat -> nat -> list 'a
+val replace_is : forall 'a. list 'a -> list 'a -> natural -> natural -> natural -> list 'a
 let rec replace_is ls vs base start stop =
   match (ls,vs) with
   | ([],_) -> []
@@ -257,7 +265,7 @@ let rec replace_is ls vs base start stop =
     else l::(replace_is ls (v::vs) (base+1) start stop)
   end
 
-val fupdate_vector_slice : value -> value -> nat -> nat -> value
+val fupdate_vector_slice : value -> value -> natural -> natural -> value
 let fupdate_vector_slice vec replace start stop =
   match (vec,replace) with
   | (V_vector m inc vals,V_vector _ inc' reps) ->
@@ -293,7 +301,7 @@ let rec to_exp v =
       else if inc then
         E_vector_indexed (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,(n, to_exp e)::acc)) (n,[]) vals)))
       else 
-        E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n, to_exp e)::acc)) (n-(List.length vals),[]) vals))
+        E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n, to_exp e)::acc)) (n-(list_length vals),[]) vals))
     | V_record(ivals) -> E_record(FES_Fexps (List.map (fun (id,value) -> (FE_Fexp id (to_exp value))) ivals) false)
     | V_list(vals) -> E_list (List.map to_exp vals)
     | V_ctor id vals -> E_app id [to_exp vals]
@@ -393,10 +401,10 @@ let rec match_pattern p value =
  | P_vector_indexed ipats ->
    match value with
    | V_vector n inc vals ->
-     let v_len = if inc then List.length vals + n else n - List.length vals in
+     let v_len = if inc then list_length vals + n else n - list_length vals in
      List.foldr
        (fun (i,pat) (matched_p,bounds) -> if matched_p && i < v_len then
-	   let (matched_p,new_bounds) = match_pattern pat (List_extra.nth vals (if inc then i+n else i-n)) in
+	   let (matched_p,new_bounds) = match_pattern pat (list_nth vals (if inc then i+n else i-n)) in
 	   (matched_p,new_bounds++bounds)
          else (false,[]))
        (true,[]) ipats
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index e3f51480..beeefc7a 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -9,7 +9,7 @@ let lit_to_string = function
  | L_one -> "bitone"
  | L_true -> "true"
  | L_false -> "false"
- | L_num n -> string_of_int n
+ | L_num n -> Big_int.string_of_big_int n
  | L_hex s -> s
  | L_bin s -> s
  | L_undef -> "undefined"
@@ -32,7 +32,7 @@ let rec val_to_string = function
  | V_vector (first_index, msb, l) ->
      let order = if msb then "big-endian" else "little-endian" in
      let repr = String.concat "; " (List.map val_to_string l) in
-     sprintf "vector [%s] (%s, from %d)" repr order first_index
+     sprintf "vector [%s] (%s, from %s)" repr order (Big_int.string_of_big_int first_index)
  | V_record l ->
      let pp (id, value) = sprintf "%s = %s" (id_to_string id) (val_to_string value) in
      let repr = String.concat "; " (List.map  pp l) in
@@ -54,7 +54,8 @@ let rec stack_to_string = function
 
 
 let reg_to_string = function Reg (id,_) | SubReg (id,_,_) -> id_to_string id ;;
-let sub_to_string = function None -> "" | Some (x, y) -> sprintf " (%d, %d)" x y
+let sub_to_string = function None -> "" | Some (x, y) -> sprintf " (%s, %s)"
+  (Big_int.string_of_big_int x) (Big_int.string_of_big_int y)
 let act_to_string = function
  | Read_reg (reg, sub) ->
      sprintf "read_reg %s%s" (reg_to_string reg) (sub_to_string sub)