Update printing for testing, fix some bugs found along the way

6 files changed, 274 insertions, 59 deletions

diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 9f807ee4..804a50bd 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -282,6 +282,9 @@ let function_map = [
   ("minus", arith_op (-));
   ("minus_vec", arith_op_vec (-) 1);
   ("minus_vec_range", arith_op_vec_range (-) 1);
+  ("minus_range_vec", arith_op_range_vec (-) 1);
+  ("minus_vec_range_range", arith_op_vec_range_range (-));
+  ("minus_range_vec_range", arith_op_range_vec_range (-));
   ("multiply", arith_op ( * ));
   ("multiply_vec", arith_op_vec ( * ) 2);
   ("mult_range_vec", arith_op_range_vec ( * ) 2);
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 80089f85..1e3ed6da 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -51,11 +51,42 @@ let val_to_string v = match v with
     (string_of_int l) ^ " bits -- 0b" ^ collapse_leading (String.concat "" (List.map (function | true -> "1" | _ -> "0") bools))
   | Bytevector words ->
     let l = List.length words in
-    (string_of_int l) ^ " bytes --" ^
+    (string_of_int l) ^ " bytes -- 0x" ^
       (String.concat ""
-	 (List.map (fun i -> (Printf.sprintf "0x%x " i)) words))
+	 (List.map (fun i -> let s = (Printf.sprintf "%x" i) in if (String.length s = 1) then "0"^s else s) words))
   | Unknown0 -> "Unknown"
 
+let half_byte_to_hex v = 
+  match v with
+    | [false;false;false;false] -> "0"
+    | [false;false;false;true ] -> "1"
+    | [false;false;true ;false] -> "2"
+    | [false;false;true ;true ] -> "3"
+    | [false;true ;false;false] -> "4"
+    | [false;true ;false;true ] -> "5"
+    | [false;true ;true ;false] -> "6"
+    | [false;true ;true ;true ] -> "7"
+    | [true ;false;false;false] -> "8"
+    | [true ;false;false;true ] -> "9"
+    | [true ;false;true ;false] -> "a"
+    | [true ;false;true ;true ] -> "b"
+    | [true ;true ;false;false] -> "c"
+    | [true ;true ;false;true ] -> "d"
+    | [true ;true ;true ;false] -> "e"
+    | [true ;true ;true ;true ] -> "f"
+
+let rec bit_to_hex v = 
+  match v with
+    | [] -> ""
+    | a::b::c::d::vs -> half_byte_to_hex [a;b;c;d] ^ bit_to_hex vs
+    | _ -> "bitstring given not divisible by 4"
+
+let val_to_hex_string v = match v with
+  | Bitvector(bools, _, _) -> "0x" ^ bit_to_hex bools
+  | Bytevector words -> val_to_string v
+  | Unknown0 -> "Error: cannot turn Unknown into hex"
+;;
+
 let reg_name_to_string = function
   | Reg0 s -> s
   | Reg_slice(s,(first,second)) -> 
diff --git a/src/lem_interp/printing_functions.mli b/src/lem_interp/printing_functions.mli
index da9347ef..fab5f8ce 100644
--- a/src/lem_interp/printing_functions.mli
+++ b/src/lem_interp/printing_functions.mli
@@ -9,6 +9,8 @@ val loc_to_string : l -> string
 val get_loc : tannot exp -> string
 (*interp_interface.value to string*)
 val val_to_string : value0 -> string
+(*Force all representations to hex strings instead of a mixture of hex and binary strings*)
+val val_to_hex_string : value0 -> string
 (* format one register *)
 val reg_name_to_string : reg_name -> string
 (* format the register dependencies *)
diff --git a/src/test/power.sail b/src/test/power.sail
index ff0fe384..a57193fd 100644
--- a/src/test/power.sail
+++ b/src/test/power.sail
@@ -524,6 +524,42 @@ function clause execute (Stdu (RS, RA, DS)) =
     GPR[RA] := EA
   }
 
+union ast member (bit[5], bit[5], bit[5]) Lswi
+
+function clause decode (0b011111 :
+(bit[5]) RT :
+(bit[5]) RA :
+(bit[5]) NB :
+0b1001010101 :
+(bit[1]) _ as instr) =
+  Lswi (RT,RA,NB)
+
+function clause execute (Lswi (RT, RA, NB)) =
+  {
+    (bit[64]) EA := 0;
+    if RA == 0 then EA := 0 else EA := GPR[RA];
+    (range<0, 32> ) r := 0;
+    r := RT - 1;
+    (range<0, 32> ) size := if NB == 0 then 32 else NB;
+    (bit[256]) membuffer := MEMr (EA,size);
+    j := 0;
+    i := 32;
+    foreach (n from (if NB == 0 then 32 else NB) to 1 by 1 in dec)
+    {
+      if i == 32
+      then {
+        r := (range<0, 32> ) (r + 1) mod 32;
+        GPR[r] := 0
+      }
+      else ();
+      (GPR[r])[i..i + 7] := membuffer[j .. j + 7];
+      j := j + 8;
+      i := i + 8;
+      if i == 64 then i := 32 else ();
+      EA := EA + 1
+    }
+  }
+
 union ast member (bit[5], bit[5], bit[16]) Addi
 
 function clause decode (0b001110 :
@@ -566,6 +602,24 @@ function clause execute (Subf (RT, RA, RB, OE, Rc)) =
     if Rc then set_overflow_cr0 (temp) else ()
   }
 
+union ast member (bit[5], bit[5], bit, bit) Neg
+
+function clause decode (0b011111 :
+(bit[5]) RT :
+(bit[5]) RA :
+(bit[5]) _ :
+[OE] :
+0b001101000 :
+[Rc] as instr) =
+  Neg (RT,RA,OE,Rc)
+
+function clause execute (Neg (RT, RA, OE, Rc)) =
+  {
+    (bit[64]) temp := ~ (GPR[RA]) + 1;
+    GPR[RT] := temp;
+    if Rc then set_overflow_cr0 (temp) else ()
+  }
+
 union ast member (bit[5], bit[5], bit[5], bit, bit) Mullw
 
 function clause decode (0b011111 :
diff --git a/src/test/run_power.ml b/src/test/run_power.ml
index 76a8292d..66d05e00 100644
--- a/src/test/run_power.ml
+++ b/src/test/run_power.ml
@@ -1,7 +1,6 @@
 open Printf ;;
-(*open Interp ;;*)
+open Big_int ;;
 open Interp_ast ;;
-(*open Interp_lib ;;*)
 open Interp_interface ;;
 open Interp_inter_imp ;;
 open Run_interp_model ;;
@@ -14,6 +13,8 @@ let sections = ref [] ;;
 let file = ref "" ;;
 let print_bytes = ref false ;;
 let bytes_file = ref "bytes_out.lem";;
+let test_format = ref false ;;
+let test_file = ref "test.txt";;
 
 let rec foldli f acc ?(i=0) = function
   | [] -> acc
@@ -22,7 +23,7 @@ let rec foldli f acc ?(i=0) = function
 
 let big_endian = true ;;
 
-let hex_to_big_int s = Big_int.big_int_of_int64 (Int64.of_string s) ;;
+let hex_to_big_int s = big_int_of_int64 (Int64.of_string s) ;;
 
 let big_int_to_vec for_mem b size =
   fst (extern_value
@@ -34,11 +35,12 @@ let big_int_to_vec for_mem b size =
 ;;
 
 let mem = ref Mem.empty ;;
+let reg = ref (Reg.add "dummy" Unknown0 Reg.empty) ;;
 
 let add_mem byte addr =
   assert(byte >= 0 && byte < 256);
-  (*Printf.printf "adder is %s, byte is %s\n" (Big_int.string_of_big_int addr) (string_of_int byte);*)
-  let addr = big_int_to_vec true addr (Big_int.big_int_of_int 64) in
+  (*Printf.printf "adder is %s, byte is %s\n" (string_of_big_int addr) (string_of_int byte);*)
+  let addr = big_int_to_vec true addr (big_int_of_int 64) in
   (*Printf.printf "adder is %s byte is %s\n" (val_to_string addr) (string_of_int byte);*)
   match addr with
     | Bytevector addr -> mem := Mem.add addr byte !mem
@@ -61,7 +63,7 @@ let add_section s =
 let load_section ic (offset,size,addr) =
   seek_in ic offset;
   for i = 0 to size - 1 do
-    add_mem (input_byte ic) (Big_int.add_int_big_int i addr);
+    add_mem (input_byte ic) (add_int_big_int i addr);
   done
 ;;
 
@@ -70,10 +72,118 @@ let load_memory (bits,addr) =
     if (Bitstring.bitstring_length bits = 0)
     then ()
     else let (Error.Success(bitsnum,rest)) = Ml_bindings.read_unsigned_char Endianness.default_endianness bits in
-	 add_mem (Uint32.to_int bitsnum) (Big_int.big_int_of_int addr);
+	 add_mem (Uint32.to_int bitsnum) (big_int_of_int addr);
 	 loop rest (1 + addr)
   in loop bits addr
 
+let get_reg reg name =
+  let reg_content = Reg.find name reg in reg_content
+
+(* use zero as a sentinel --- it might prevent a minimal loop from
+ * working in principle, but won't happen in practice *)
+let lr_init_value = zero_big_int
+
+let init_reg () =
+  let init name value size =
+    (* fix index - this is necessary for CR, indexed from 32 *)
+    let offset = function
+      | Bitvector(bits,inc,fst) ->
+        Bitvector(bits,inc,big_int_of_int (64 - size))
+     | _ -> assert false in
+    name, offset (big_int_to_vec false value (big_int_of_int size)) in
+  List.fold_left (fun r (k,v) -> Reg.add k v r) Reg.empty (
+    (* Special registers *)
+    [
+      init "CR" zero_big_int 32;
+      init "CTR" zero_big_int 64;
+      init "LR" lr_init_value 64;
+      init "XER" zero_big_int 64;
+      init "VRSAVE" zero_big_int 32;
+      init "FPSCR" zero_big_int 64;
+      init "VSCR" zero_big_int 32;
+    ] @
+    (* Commonly read before written general purpose register *)
+      [init "GPR0" zero_big_int 64;
+       init "GPR1" zero_big_int 64;
+       init "GPR2" zero_big_int 64;
+       init "GPR3" zero_big_int 64;
+       init "GPR31" zero_big_int 64;]
+      (*Conditionally include all general purpose registers *)
+    @ (if !test_format
+      then [ 
+	init "GPR4" zero_big_int 64;
+	init "GPR5" zero_big_int 64;
+	init "GPR6" zero_big_int 64;
+	init "GPR7" zero_big_int 64;
+	init "GPR8" zero_big_int 64;
+	init "GPR9" zero_big_int 64;
+	init "GPR10" zero_big_int 64;
+	init "GPR11" zero_big_int 64;
+	init "GPR12" zero_big_int 64;
+	init "GPR13" zero_big_int 64;
+	init "GPR14" zero_big_int 64;
+	init "GPR15" zero_big_int 64;
+	init "GPR16" zero_big_int 64;
+	init "GPR17" zero_big_int 64;
+	init "GPR18" zero_big_int 64;
+	init "GPR19" zero_big_int 64;
+	init "GPR20" zero_big_int 64;
+	init "GPR21" zero_big_int 64;
+	init "GPR22" zero_big_int 64;
+	init "GPR23" zero_big_int 64;
+	init "GPR24" zero_big_int 64;
+	init "GPR25" zero_big_int 64;
+	init "GPR26" zero_big_int 64;
+	init "GPR27" zero_big_int 64;
+	init "GPR28" zero_big_int 64;
+	init "GPR29" zero_big_int 64;
+	init "GPR30" zero_big_int 64;]
+      else [])
+      @
+      (if !test_format
+       then [
+	 init "VR0" zero_big_int 128;
+	 init "VR1" zero_big_int 128;
+	 init "VR2" zero_big_int 128;
+	 init "VR3" zero_big_int 128;
+	 init "VR4" zero_big_int 128;
+	 init "VR5" zero_big_int 128;
+	 init "VR6" zero_big_int 128;
+	 init "VR7" zero_big_int 128;
+	 init "VR8" zero_big_int 128;
+	 init "VR9" zero_big_int 128;
+	 init "VR10" zero_big_int 128;
+	 init "VR11" zero_big_int 128;
+	 init "VR12" zero_big_int 128;
+	 init "VR13" zero_big_int 128;
+	 init "VR14" zero_big_int 128;
+	 init "VR15" zero_big_int 128;
+	 init "VR16" zero_big_int 128;
+	 init "VR17" zero_big_int 128;
+	 init "VR18" zero_big_int 128;
+	 init "VR19" zero_big_int 128;
+	 init "VR20" zero_big_int 128;
+	 init "VR21" zero_big_int 128;
+	 init "VR22" zero_big_int 128;
+	 init "VR23" zero_big_int 128;
+	 init "VR24" zero_big_int 128;
+	 init "VR25" zero_big_int 128;
+	 init "VR26" zero_big_int 128;
+	 init "VR27" zero_big_int 128;
+	 init "VR28" zero_big_int 128;
+	 init "VR29" zero_big_int 128;
+	 init "VR30" zero_big_int 128;
+    	 init "VR31" zero_big_int 128;]
+       else [])
+      @
+      (*Not really registers*)
+     [(* Currint Instruciton Address, manually set *)
+       init "CIA" (hex_to_big_int !mainaddr) 64;
+       init "NIA" zero_big_int 64;
+       "mode64bit", Bitvector([true],true,zero_big_int);
+     ])
+;;
+
 let lem_print_memory m =
   let format_addr a = "[" ^ (List.fold_right (fun i r -> "(" ^ (string_of_int i) ^ ": word8);" ^ r) a "") ^ "]" in
   let preamble = "open import Pervasives\ntype word8 = nat\n" in
@@ -89,32 +199,30 @@ let lem_print_memory m =
   let _ = close_out o in
   Sys.rename temp_file_name !bytes_file 
 
-(* use zero as a sentinel --- it might prevent a minimal loop from
- * working in principle, but won't happen in practice *)
-let lr_init_value = Big_int.zero_big_int
-
-let init_reg () =
-  let init name value size =
-    (* fix index - this is necessary for CR, indexed from 32 *)
-    let offset = function
-      | Bitvector(bits,inc,fst) ->
-        Bitvector(bits,inc,Big_int.big_int_of_int (64 - size))
-     | _ -> assert false in
-    name, offset (big_int_to_vec false value (Big_int.big_int_of_int size)) in
-  List.fold_left (fun r (k,v) -> Reg.add k v r) Reg.empty [
-    (* XXX execute main() directly until we can handle the init phase *)
-    init "CIA" (hex_to_big_int !mainaddr) 64;
-    init "GPR0" Big_int.zero_big_int 64;
-    init "GPR1" Big_int.zero_big_int 64;
-    init "GPR2" Big_int.zero_big_int 64;
-    init "GPR31" Big_int.zero_big_int 64;
-    init "CTR" Big_int.zero_big_int 64;
-    init "CR" Big_int.zero_big_int 32;
-    init "LR" lr_init_value 64;
-    init "XER" Big_int.zero_big_int 64;
-    "mode64bit", Bitvector([true],true,Big_int.zero_big_int);
-  ]
-;;
+let print_test_results final_reg final_mem = 
+  let tilde = String.make 90 '~' in
+  let preamble = "\t\t"^"Value before test" ^ "\t\t\t" ^ "Value after test\n" ^ tilde ^ "\n" in
+  let format_register reg_name = 
+    let original_reg = get_reg !reg reg_name in
+    let final_reg = get_reg final_reg reg_name in
+    reg_name ^ ";\t\t" ^ Printing_functions.val_to_hex_string original_reg ^ ";\t\t\t" ^ Printing_functions.val_to_hex_string final_reg ^ "\n"
+  in
+  let rec numbered_reg base_name curr_index stop_index =
+    if curr_index > stop_index
+    then ""
+    else (format_register (base_name ^ (string_of_int curr_index))) ^ (numbered_reg base_name (curr_index +1) stop_index)
+  in
+  let special_reg = List.fold_right (fun r rs -> (format_register r) ^ rs) ["CR";"CTR";"LR";"XER"] "" in
+  let gpr_reg = numbered_reg "GPR" 0 31 in
+  let vr_reg = numbered_reg "VR" 0 31 in
+  let reg_contents = special_reg ^ gpr_reg ^ (format_register "VRSAVE") ^ vr_reg ^ (format_register "VSCR") in
+  let mem_contents = "Memory will go here\n" in
+  let footer = tilde ^ "\n" in
+  let (temp_file_name, o) = Filename.open_temp_file "tt_temp" "" in
+  let o' = Format.formatter_of_out_channel o in
+  Format.fprintf o' "%s" (preamble ^ reg_contents ^footer ^ mem_contents);
+  let _ = close_out o in
+  Sys.rename temp_file_name !test_file
 
 let eager_eval = ref true
 
@@ -122,12 +230,13 @@ let args = [
   ("--file", Arg.Set_string file, "filename binary code to load in memory");
   ("--data", Arg.String add_section, "name,offset,size,addr add a data section");
   ("--code", Arg.String add_section, "name,offset,size,addr add a code section");
-  (*("--startaddr", Arg.Set_string startaddr, "addr initial address (UNUSED)");*)
   ("--mainaddr", Arg.Set_string mainaddr, "addr address of the main section (entry point; default: 0)");
-  ("--quiet", Arg.Clear Run_interp_model.debug, " do not display interpreter actions");
-  ("--interactive", Arg.Clear eager_eval , " interactive execution");
-  ("--dump", Arg.Set print_bytes , " do not run, just generate a lem file of a list of bytes");
-  ("--out", Arg.Set_string bytes_file, " specify the name for a file generated by --dump");
+  ("--quiet", Arg.Clear Run_interp_model.debug, "do not display interpreter actions");
+  ("--interactive", Arg.Clear eager_eval , "interactive execution");
+  ("--test", Arg.Set test_format , "format output for single instruction tests, save in file");
+  ("--test_file", Arg.Set_string test_file , "specify the name for a file generated by --test");
+  ("--dump", Arg.Set print_bytes , "do not run, just generate a lem file of a list of bytes");
+  ("--dump_file", Arg.Set_string bytes_file, "specify the name for a file generated by --dump");
 ] ;;
 
 let time_it action arg =
@@ -137,10 +246,6 @@ let time_it action arg =
   finish_time -. start_time
 ;;
 
-let get_reg reg name =
-  let reg_content = Reg.find name reg in reg_content
-;;
-
 let eq_zero = function
   | Bitvector(bools,_,_) -> List.for_all (not) bools
 ;;
@@ -149,12 +254,14 @@ let rec fde_loop count main_func parameters mem reg ?mode track_dependencies pro
   debugf "\n**** instruction %d  ****\n" count;
   match Run_interp_model.run ~main_func ~parameters ~mem ~reg ~eager_eval:!eager_eval ~track_dependencies:(ref track_dependencies) ?mode prog with
   | false, _,_, _ -> eprintf "FAILURE\n"; exit 1
-  | true, mode, track_dependencies, (reg, mem) ->
-      if eq_zero (get_reg reg "CIA") then
-        eprintf "\nSUCCESS: returned with value %s\n"
-          (Printing_functions.val_to_string (get_reg reg "GPR3"))
+  | true, mode, track_dependencies, (my_reg, my_mem) ->
+      if eq_zero (get_reg my_reg "CIA") then
+        (if not(!test_format) 
+	 then eprintf "\nSUCCESS: returned with value %s\n"
+          (Printing_functions.val_to_string (get_reg my_reg "GPR3"))
+	 else print_test_results my_reg my_mem)	    
       else
-        fde_loop (count+1) main_func parameters mem reg ~mode:mode track_dependencies prog
+        fde_loop (count+1) main_func parameters my_mem my_reg ~mode:mode track_dependencies prog
 ;;
 
 let run () =
@@ -164,33 +271,37 @@ let run () =
     exit 1;
   end;
   if !eager_eval then Run_interp_model.debug := true;
+  if !test_format then Run_interp_model.debug := false;
   let (locations,start_address) = populate !file in
   let total_size = (List.length locations) in
-  eprintf "Loading binary into memory (%d sections)... %!" total_size;
+  if not(!test_format)
+  then eprintf "Loading binary into memory (%d sections)... %!" total_size;
   let t = time_it (List.iter load_memory) locations in
-  eprintf "done. (%f seconds)\n%!" t;
+  if not(!test_format)
+  then eprintf "done. (%f seconds)\n%!" t;
   let rec reading loc length = 
     if length = 0  
     then []
     else 
-      let location = big_int_to_vec true loc (Big_int.big_int_of_int 64) in
+      let location = big_int_to_vec true loc (big_int_of_int 64) in
       match location with
 	| Bytevector location ->
-	  (Mem.find location !mem)::(reading (Big_int.add_big_int loc Big_int.unit_big_int) (length - 1)) in
-  let addr = reading (Big_int.big_int_of_int start_address) 8 in
+	  (Mem.find location !mem)::(reading (add_big_int loc unit_big_int) (length - 1)) in
+  let addr = reading (big_int_of_int start_address) 8 in
   let _ = begin
     startaddr := addr;
     mainaddr := "0x" ^ (List.fold_left (^) "" (List.map (Printf.sprintf "%02x") addr));
   end in
-  let reg = init_reg () in
+  let my_reg = init_reg () in
+  reg := my_reg;
   (* entry point: unit -> unit fde *)
   let funk_name = "fde" in
   let parms = [] in
   let name = Filename.basename !file in
   if !print_bytes 
   then lem_print_memory !mem
-  else let t =time_it (fun () -> fde_loop 0 funk_name parms !mem reg false (name, Power.defs)) () in
-       eprintf "Execution time: %f seconds\n" t
+  else let t =time_it (fun () -> fde_loop 0 funk_name parms !mem !reg false (name, Power.defs)) () in
+       if not(!test_format) then eprintf "Execution time: %f seconds\n" t
 ;;
 
 run () ;;
diff --git a/src/type_internal.ml b/src/type_internal.ml
index e41a60d6..ba1dd4e2 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -920,12 +920,26 @@ let initial_typ_env =
                                      (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))),
                        External (Some "minus_vec_range"),
                         [LtEq(Specc(Parse_ast.Int("-",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})],pure_e);
-                   Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]),
+		  Base(((mk_nat_params ["n";"m";"o";"p";])@(mk_ord_params ["ord"]),
+			 (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");
+					       mk_range (mk_nv "o") (mk_nv "p")])
+			    (mk_range (mk_nv "o") (mk_add (mk_nv "p") {nexp = N2n (mk_nv "m",None)})))),
+		       External (Some "minus_vec_range_range"),
+		       [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})],pure_e);
+                  Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]),
                          (mk_pure_fun (mk_tup [mk_range (mk_nv "o") (mk_nv "p");
                                                mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");])
                                       (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))),
                         External (Some "minus_range_vec"),
-                       [LtEq(Specc(Parse_ast.Int("-",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})],pure_e); ]));
+			[LtEq(Specc(Parse_ast.Int("-",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})],pure_e); 
+		   Base(((mk_nat_params ["n";"m";"o";"p";])@(mk_ord_params ["ord"]),
+			 (mk_pure_fun (mk_tup [mk_range (mk_nv "o") (mk_nv "p");
+					       mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");])
+			    (mk_range (mk_nv "o") (mk_add (mk_nv "p") {nexp = N2n (mk_nv "m",None)})))),
+			External (Some "minus_range_vec_range"),
+			[LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})],pure_e);
+
+		  ]));
     ("*",Overload(Base(((mk_typ_params ["a";"b";"c"]),
                         (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})), External (Some "multiply"),[],pure_e),
 		  true,