Allow negative "nat" internally

to_num and to_vec probably still need to be fixed

5 files changed, 35 insertions, 34 deletions

diff --git a/language/l2.lem b/language/l2.lem
index 0c94e399..82e2450f 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -51,7 +51,7 @@ type kind =
 
 type nexp_aux =  (* expression of kind Nat, for vector sizes and origins *)
  | Nexp_var of kid (* variable *)
- | Nexp_constant of natural (* constant *)
+ | Nexp_constant of integer (* constant *)
  | Nexp_times of nexp * nexp (* product *)
  | Nexp_sum of nexp * nexp (* sum *)
  | Nexp_exp of nexp (* exponential *)
@@ -117,7 +117,7 @@ type n_constraint_aux =  (* constraint over kind $Nat$ *)
  | NC_fixed of nexp * nexp
  | NC_bounded_ge of nexp * nexp
  | NC_bounded_le of nexp * nexp
- | NC_nat_set_bounded of kid * list natural
+ | NC_nat_set_bounded of kid * list integer
 
 
 type kinded_id = 
@@ -148,7 +148,7 @@ type lit_aux =  (* Literal constant *)
  | L_one (* $bitone : bit$ *)
  | L_true (* $true : bool$ *)
  | L_false (* $false : bool$ *)
- | L_num of natural (* natural number constant *)
+ | L_num of integer (* natural number constant *)
  | L_hex of string (* bit vector constant, C-style *)
  | L_bin of string (* bit vector constant, C-style *)
  | L_undef (* constant representing undefined values *)
@@ -197,7 +197,7 @@ type pat_aux 'a =  (* Pattern *)
  | P_app of id * list (pat 'a) (* union constructor pattern *)
  | P_record of list (fpat 'a) * bool (* struct pattern *)
  | P_vector of list (pat 'a) (* vector pattern *)
- | P_vector_indexed of list (natural * (pat 'a)) (* vector pattern (with explicit indices) *)
+ | P_vector_indexed of list (integer * (pat 'a)) (* vector pattern (with explicit indices) *)
  | P_vector_concat of list (pat 'a) (* concatenated vector pattern *)
  | P_tup of list (pat 'a) (* tuple pattern *)
  | P_list of list (pat 'a) (* list pattern *)
@@ -227,7 +227,7 @@ type exp_aux 'a =  (* Expression *)
  | E_if of (exp 'a) * (exp 'a) * (exp 'a) (* conditional *)
  | E_for of id * (exp 'a) * (exp 'a) * (exp 'a) * order * (exp 'a) (* loop *)
  | E_vector of list (exp 'a) (* vector (indexed from 0) *)
- | E_vector_indexed of list (natural * (exp 'a)) (* vector (indexed consecutively) *)
+ | E_vector_indexed of list (integer * (exp 'a)) (* vector (indexed consecutively) *)
  | E_vector_access of (exp 'a) * (exp 'a) (* vector access *)
  | E_vector_subrange of (exp 'a) * (exp 'a) * (exp 'a) (* subvector extraction *)
  | E_vector_update of (exp 'a) * (exp 'a) * (exp 'a) (* vector functional update *)
@@ -336,8 +336,8 @@ type tannot_opt =
 
 
 type index_range_aux =  (* index specification, for bitfields in register types *)
- | BF_single of natural (* single index *)
- | BF_range of natural * natural (* index range *)
+ | BF_single of integer (* single index *)
+ | BF_range of integer * integer (* index range *)
  | BF_concat of index_range * index_range (* concatenation of index ranges *)
 
 and index_range = 
@@ -447,7 +447,7 @@ type k =  (* Internal kinds *)
 
 type ne =  (* internal numeric expressions *)
  | Ne_var of kid
- | Ne_const of natural
+ | Ne_const of integer
  | Ne_mult of ne * ne
  | Ne_add of list ne
  | Ne_exp of ne
@@ -468,7 +468,7 @@ type nec =  (* Numeric expression constraints *)
  | Nec_lteq of ne * ne
  | Nec_eq of ne * ne
  | Nec_gteq of ne * ne
- | Nec_in of kid * list natural
+ | Nec_in of kid * list integer
 
 
 type tag =  (* Data indicating where the identifier arises and thus information necessary in compilation *)
diff --git a/language/l2.ott b/language/l2.ott
index 6faeb724..3abad576 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -7,7 +7,7 @@ metavar num ::=
   {{ lex numeric }}
   {{ ocaml int }}
   {{ hol num }}
-  {{ lem natural }}
+  {{ lem integer }}
   {{ com Numeric literals }}
 
 metavar hex ::=
diff --git a/language/l2_parse.ott b/language/l2_parse.ott
index b2e9cfdf..eb238b65 100644
--- a/language/l2_parse.ott
+++ b/language/l2_parse.ott
@@ -7,7 +7,7 @@ metavar num ::=
   {{ lex numeric }}
   {{ ocaml int }}
   {{ hol num }}
-  {{ lem natural }}
+  {{ lem integer }}
   {{ com Numeric literals }}
 
 metavar hex ::=
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 50d84556..a033285e 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -64,7 +64,7 @@ type value =
  | V_lit of lit
  | V_tuple of list value
  | V_list of list value
- | V_vector of natural * bool * list value (* The nat stores the first index, the bool whether that's most or least significant *)
+ | V_vector of integer * bool * list value (* The nat stores the first index, the bool whether that's most or least significant *)
  | V_record of t * list (id * value)
  | V_ctor of id * t * value
  | V_register of reg_form (* Value to store register access, when not actively reading or writing *)
@@ -98,10 +98,10 @@ let emem = Mem 1 Map.empty
 
 (* These may need to be refined or expanded based on memory requirement *)
 type action = 
- | 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
+ | Read_reg of reg_form * maybe (integer * integer)
+ | Write_reg of reg_form * maybe (integer* integer) * value
+ | Read_mem of id * value * maybe (integer * integer)
+ | Write_mem of id * value * maybe (integer * integer) * 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 *)
@@ -220,15 +220,15 @@ let litV_to_vec (L_aux lit l) =
     V_vector 0 true bits
   end
 
-(* Like List_extra.nth with a natural instead of nat index -
+(* Like List_extra.nth with a integer 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_nth : forall 'a . list 'a -> integer -> 'a
+let list_nth l n = List_extra.nth l (natFromInteger n)
 
-val list_length : forall 'a . list 'a -> natural
-let list_length l = naturalFromNat (List.length l)
+val list_length : forall 'a . list 'a -> integer
+let list_length l = integerFromNat (List.length l)
 
-val access_vector : value -> natural -> value
+val access_vector : value -> integer -> value
 let access_vector v n =
   match v with
   | V_vector m inc vs -> 
@@ -237,13 +237,13 @@ let access_vector v n =
     else list_nth vs (m - n)
   end
 
-val from_n_to_n :forall 'a. natural -> natural  -> list 'a -> list 'a
+val from_n_to_n :forall 'a. integer -> integer  -> list 'a -> list 'a
 let from_n_to_n from to_ ls =
-  let from = natFromNatural from in
-  let to_ = natFromNatural to_ in
+  let from = natFromInteger from in
+  let to_ = natFromInteger to_ in
   take (to_ - from + 1) (drop from ls)
 
-val slice_vector : value -> natural -> natural -> value
+val slice_vector : value -> integer -> integer -> value
 let slice_vector v n1 n2 =
   match v with
   | V_vector m inc vs ->
@@ -279,14 +279,14 @@ let rec update_vector_slice vector value mem =
       mem vs
 end
 
-val fupdate_vec : value -> natural -> value -> value
+val fupdate_vec : value -> integer -> value -> value
 let fupdate_vec v n vexp =
   match v with
   | V_vector m inc vals -> 
-    V_vector m inc (List.update vals (natFromNatural (if inc then (n-m) else (m-n))) vexp)
+    V_vector m inc (List.update vals (natFromInteger (if inc then (n-m) else (m-n))) vexp)
   end
 
-val replace_is : forall 'a. list 'a -> list 'a -> natural -> natural -> natural -> list 'a
+val replace_is : forall 'a. list 'a -> list 'a -> integer -> integer -> integer -> list 'a
 let rec replace_is ls vs base start stop =
   match (ls,vs) with
   | ([],_) -> []
@@ -298,7 +298,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 -> natural -> natural -> value
+val fupdate_vector_slice : value -> value -> integer -> integer -> value
 let fupdate_vector_slice vec replace start stop =
   match (vec,replace) with
   | (V_vector m inc vals,V_vector _ inc' reps) ->
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 9b3ba3b0..9a183f7f 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -31,16 +31,17 @@ let bool_to_bit b = match b with
  * By convention, MSB is on the left, so increasing = Big-Endian (MSB0),
  * hence MSB first.
  * http://en.wikipedia.org/wiki/Bit_numbering *)
+(* XXX signedness probably broken here *)
 let to_num_inc (V_vector idx true l) =
-  V_lit(L_aux (L_num(naturalFromBitSeq (BitSeq Nothing false (map bit_to_bool (reverse l))))) Unknown);;
+  V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool (reverse l)))))) Unknown);;
 let to_num_dec (V_vector idx false l) =
-  V_lit(L_aux (L_num(naturalFromBitSeq (BitSeq Nothing false (map bit_to_bool l)))) Unknown);;
+  V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool l))))) Unknown);;
 
 let to_vec_inc len (V_lit(L_aux (L_num n) ln)) =
-  let l = boolListFrombitSeq len (bitSeqFromNatural Nothing n) in
+  let l = boolListFrombitSeq len (bitSeqFromInteger Nothing n) in
   V_vector 0 true (map bool_to_bit (reverse l)) ;;
 let to_vec_dec len (V_lit(L_aux (L_num n) ln)) =
-  let l = boolListFrombitSeq len (bitSeqFromNatural Nothing n) in
+  let l = boolListFrombitSeq len (bitSeqFromInteger Nothing n) in
   V_vector 0 false (map bool_to_bit l) ;;
 
 let rec add (V_tuple args) = match args with