working dec vectors

7 files changed, 80 insertions, 32 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index e2d6b781..0a112962 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -263,8 +263,8 @@ let is_lit_vector (L_aux l _) =
 end
 
 (* XXX Both make an endian assumption, and should use a flag to switch*)
-val litV_to_vec : lit -> value
-let litV_to_vec (L_aux lit l) =
+val litV_to_vec : lit -> bool -> value
+let litV_to_vec (L_aux lit l) is_inc =
   match lit with
   | L_hex s ->
     let to_v b = V_lit (L_aux b l) in
@@ -295,10 +295,14 @@ let litV_to_vec (L_aux lit l) =
 			 | #'e' -> [L_one ;L_one ;L_one ;L_zero]
 			 | #'f' -> [L_one ;L_one ;L_one ;L_one ] end)
 		       (String.toCharList s))) in
-    V_vector 0 true hexes
+    if is_inc 
+    then V_vector 0 true hexes
+    else V_vector (integerFromNat ((List.length hexes) -1)) false hexes
   | L_bin s -> 
     let bits = List.map (fun s -> match s with | #'0' -> (V_lit (L_aux L_zero l)) | #'1' -> (V_lit (L_aux L_one l)) end) (String.toCharList s) in
-    V_vector 0 true bits
+    if is_inc
+    then V_vector 0 true bits
+    else V_vector (integerFromNat ((List.length bits) -1)) false bits
   end
 
 (* Like List_extra.nth with a integer instead of nat index -
@@ -660,11 +664,11 @@ let rec match_pattern (P_aux p _) value =
   match p with 
   | P_lit(lit) -> 
     if is_lit_vector lit then
-      let (V_vector n inc bits) = litV_to_vec lit in
+      let (V_vector n inc bits) = litV_to_vec lit true in (*TODO use type annotation to select between increasing and decreasing*)
       match value with
       | V_lit litv -> 
         if is_lit_vector litv then 
-          let (V_vector n' inc' bits') = litV_to_vec litv in
+          let (V_vector n' inc' bits') = litV_to_vec litv true in (*TODO find a way to determine increasing or decreasing *)
           if n=n' && inc = inc' then (foldr2 (fun l r rest -> (l = r) && rest) true bits bits',false, [])
           else (false,false,[])
         else (false,false,[])
@@ -918,7 +922,9 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
   match exp with
     | E_lit lit -> 
       if is_lit_vector lit 
-      then (Value (litV_to_vec lit) Tag_empty,l_mem,l_env) 
+      then 
+        let is_inc = (match typ with | T_app "vector" (T_args [_;_;T_arg_order (Ord_aux Ord_inc _);_]) -> true | _ -> false end) in
+        (Value (litV_to_vec lit is_inc) Tag_empty,l_mem,l_env) 
       else (Value (V_lit lit) Tag_empty, l_mem,l_env)
     | E_cast ((Typ_aux typ _) as ctyp) exp -> 
       resolve_outcome (interp_main mode t_level l_env l_mem exp)
@@ -1306,7 +1312,12 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
     | E_tuple(exps) -> 
       exp_list mode t_level (fun exps -> E_aux (E_tuple exps) (l,annot)) V_tuple l_env l_mem [] exps
     | E_vector(exps) ->
-      exp_list mode t_level (fun exps -> E_aux (E_vector exps) (l,annot)) (fun vals -> V_vector 0 true vals) l_env l_mem [] exps
+      let is_inc = (match typ with
+        | T_app "vector" (T_args [ _; _; T_arg_order (Ord_aux Ord_inc _); _]) -> true
+        | _ -> false end) in
+      let base = integerFromNat (if is_inc then 0 else (List.length exps) - 1) in
+      exp_list mode t_level 
+        (fun exps -> E_aux (E_vector exps) (l,annot)) (fun vals -> V_vector base is_inc vals) l_env l_mem [] exps
     | E_vector_indexed iexps (Def_val_aux default dannot) ->
       let (indexes,exps) = List.unzip iexps in
       let (is_inc,base,len) = (match typ with
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index a03fad5c..199d070a 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -78,17 +78,23 @@ let bitwise_binop op (V_tuple [V_vector idx inc v; V_vector idx' inc' v']) =
  * http://en.wikipedia.org/wiki/Bit_numbering *)
 let to_num signed (V_vector idx inc l) =
   (* Word library in Lem expects bitseq with LSB first *)
-  let l = if inc then reverse l else l in
+(*TODO: Kathy think more
+  We thought a reverse was needed due to above comments only in inc case.
+  However, we seem to be interpresting bit vectors such that reverse is always needed
+  and despite numbering MSB is on the left.
+*)
+  let l = (*if inc then reverse l else l*) reverse l in
   (* Make sure the last bit is a zero to force unsigned numbers *)
   let l = if signed then l else l ++ [V_lit (L_aux L_zero Unknown)] in
   V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool l))))) Unknown);;
 
+(*TODO As with above, consider the reverse here in both cases, where we're again always interpreting with the MSB on the left *)
 let to_vec_inc (V_tuple([V_lit(L_aux (L_num len) _); (V_lit(L_aux (L_num n) ln))])) =
   let l = boolListFrombitSeq (natFromInteger len) (bitSeqFromInteger Nothing n) in
   V_vector 0 true (map bool_to_bit (reverse l)) ;;
 let to_vec_dec (V_tuple([V_lit(L_aux (L_num len) _); (V_lit(L_aux (L_num n) ln))])) =
   let l = boolListFrombitSeq (natFromInteger len) (bitSeqFromInteger Nothing n) in
-  V_vector 0 false (map bool_to_bit l) ;;
+  V_vector (len - 1) false (map bool_to_bit (reverse l)) ;;
 let to_vec ord len n =
   if ord
   then to_vec_inc (V_tuple ([V_lit(L_aux (L_num (integerFromNat len)) Interp_ast.Unknown); n]))
@@ -131,12 +137,12 @@ let arith_op_vec_range op (V_tuple args) = match args with
 end ;;
 
 let arith_op_range_vec_range op (V_tuple args) = match args with
-  | [n;(V_vector _ _ _ as l2)] ->
-    arith_op op (V_tuple [n;(to_num true l2)])
+  | [n;(V_vector _ ord _ as l2)] ->
+    arith_op op (V_tuple [n;(to_num ord l2)])
 end ;;
 let arith_op_vec_range_range op (V_tuple args) = match args with
-  | [(V_vector _ _ _ as l1);n] ->
-    arith_op op (V_tuple [(to_num true l1);n])
+  | [(V_vector _ ord _ as l1);n] ->
+    arith_op op (V_tuple [(to_num ord l1);n])
 end ;;
 
 let compare_op op (V_tuple args) = match args with
@@ -155,8 +161,8 @@ let rec vec_concat (V_tuple args) = match args with
   | [V_vector n d l; V_vector n' d' l'] ->
       (* XXX d = d' ? droping n' ? *)
       V_vector n d (l ++ l')
-  | [V_lit l; x] -> vec_concat (V_tuple [litV_to_vec l; x])
-  | [x; V_lit l] -> vec_concat (V_tuple [x; litV_to_vec l])
+  | [V_lit l; x] -> vec_concat (V_tuple [litV_to_vec l true; x]) (*TODO, get the correct order*)
+  | [x; V_lit l] -> vec_concat (V_tuple [x; litV_to_vec l true]) (*TODO, get the correct order*)
   end ;;
 
 let function_map = [
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 91a81634..2f8c5e97 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -62,7 +62,7 @@ let rec val_to_string = function
  | V_vector (first_index, inc, l) ->
      let last_index = add_int_big_int (if inc then List.length l - 1 else 1 - List.length l) first_index  in
      let repr =
-       try bitvec_to_string (if inc then l else List.rev l)
+       try bitvec_to_string (* (if inc then l else List.rev l)*) l
        with Failure _ ->
          sprintf "[%s]" (String.concat "; " (List.map val_to_string l)) in
      sprintf "%s [%s..%s]" repr (string_of_big_int first_index) (string_of_big_int last_index)
@@ -148,9 +148,9 @@ module Reg = struct
   let to_string id v =
     sprintf "%s -> %s" (id_to_string id) (val_to_string v)
   let find id m =
-    eprintf "reg_find called with %s\n" (id_to_string id);
+(*    eprintf "reg_find called with %s\n" (id_to_string id);*)
     let v = find id m in
-    eprintf "%s -> %s\n" (id_to_string id) (val_to_string v);
+(*    eprintf "%s -> %s\n" (id_to_string id) (val_to_string v);*)
     v
 end ;;
 
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index f4729814..40b6d60f 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -416,6 +416,7 @@ let pp_lem_default ppf (DT_aux(df,l)) =
     match df with
       | DT_kind(bk,var) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_kind" pp_lem_bkind bk pp_lem_var var
       | DT_typ(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_typ" pp_lem_typscm ts pp_lem_id id
+      | DT_order(ord) -> fprintf ppf "@[<0>(DT_order %a)@]" pp_lem_ord ord
   in
   fprintf ppf "@[<0>(DT_aux %a %a)@]" print_de df pp_lem_l l
 
@@ -951,6 +952,7 @@ let doc_exp, doc_let =
 let doc_default (DT_aux(df,_)) = match df with
   | DT_kind(bk,v) -> separate space [string "default"; doc_bkind bk; doc_var v]
   | DT_typ(ts,id) -> separate space [string "default"; doc_typscm ts; doc_id id]
+  | DT_order(ord) -> separate space [string "default"; string "order"; doc_ord ord]
 
 let doc_spec (VS_aux(v,_)) = match v with
   | VS_val_spec(ts,id) ->
diff --git a/src/test/test1.sail b/src/test/test1.sail
index 1ca615c5..489206d3 100644
--- a/src/test/test1.sail
+++ b/src/test/test1.sail
@@ -1,3 +1,4 @@
+default Order inc
 default Nat 'i
 default Order 'o
 default bool b
@@ -7,7 +8,6 @@ val forall Type 'i, 'b. ('i, 'b) -> 'i effect pure fst
 typedef int_list [name = "il"] = list<nat>
 typedef reco = const struct forall 'i, 'a, 'b. { 'a['i] v; 'b w; }
 typedef maybe = const union forall 'a. { Nne; 'a Sme; }
-typedef colors = enumerate { red; green; blue }
 typedef creg = register bits [5:10] { 5 : h ; 6..7 : j}
 let bool e = true
 val forall Nat 'a, Nat 'b. bit['a:'b] sliced
@@ -41,6 +41,8 @@ function unit a (bit) b = if identity(b) then (identity()) else ()
 
 function bit sw s = switch s { case 0 -> bitzero }
 
+typedef colors = enumerate { red; green; blue }
+
 let colors rgb = red
 
 function bit enu (red) = 0
diff --git a/src/test/test2.sail b/src/test/test2.sail
index 57542d3f..ab0a72b7 100644
--- a/src/test/test2.sail
+++ b/src/test/test2.sail
@@ -1,3 +1,5 @@
+default Order dec
+
 function nat id ( n ) = n
 
 register (bit[5]) c
@@ -8,7 +10,10 @@ function unit f() = {
   else 
    a := 4
  );
- c := (bit[5]) (3 + 0b00001) mod 2;
+ a:= (nat) 0b010101;
+ a:= (nat) (0b0101010 + 0b0101000);
+ c := (bit[5]) (3 + 0b00101) mod 3;
+ if c[1] then c:= 31 else c:= 0;
  b := a;
 }
 
diff --git a/src/type_check.ml b/src/type_check.ml
index fde2df33..1171a48d 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -236,8 +236,22 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
 	  pats ([],[],[],[]) in
       let env = List.fold_right (fun e env -> Envmap.union e env) t_envs Envmap.empty in (*Need to check for non-duplication of variables*)
       let (u,cs) = List.fold_right (fun u (t,cs) -> let t',cs = type_consistent (Patt l) d_env u t in t',cs) ts (item_t,[]) in
-      let t = {t = Tapp("vector",[(TA_nexp {nexp= Nconst zero});(TA_nexp {nexp= Nconst (big_int_of_int (List.length ts))});(TA_ord{order=Oinc});(TA_typ u)])} in
-      (P_aux(P_vector(pats'),(l,Base(([],t),Emp_local,cs,pure_e))), env,cs@constraints,t)
+      let len = List.length ts in
+      let t = 
+        match (ord.order,d_env.default_o.order) with
+        | (Oinc,_) | (Ovar _, Oinc) | (Ouvar _,Oinc) -> 
+          {t = Tapp("vector",[TA_nexp {nexp= Nconst zero};
+                              TA_nexp {nexp= Nconst (big_int_of_int len)};
+                              TA_ord{order=Oinc};
+                              TA_typ u])}
+        | (Odec,_) | (Ovar _, Odec) | (Ouvar _,Odec) -> 
+          {t= Tapp("vector", [TA_nexp {nexp = Nconst (if len = 0 then zero else (big_int_of_int (len -1)))};
+                              TA_nexp {nexp = Nconst (big_int_of_int len)};
+                              TA_ord{order=Odec};
+                              TA_typ u;])}
+        | _ -> raise (Reporting_basic.err_unreachable l "Default order not set") in
+      (*TODO Should gather the constraints here, with regard to the expected base and rise, and potentially reset them above*)
+      (P_aux(P_vector(pats'),(l,Base(([],t),Emp_local,cs,pure_e))), env,cs@constraints,t) 
     | P_vector_indexed(ipats) -> 
       let item_t = match expect_actual.t with
 	| Tapp("vector",[b;r;o;TA_typ i]) -> i
@@ -265,7 +279,7 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
 	    (((i,pat')::pats),(t::ts),(env::t_envs),(cons@constraints)))
 	  ipats ([],[],[],[]) in
       let co = Patt l in
-      let env = List.fold_right (fun e env -> Envmap.union e env) t_envs Envmap.empty in (*Need to check for non-duplication of variables*)
+      let env = List.fold_right (fun e env -> Envmap.union e env) t_envs Envmap.empty in (*TODO Need to check for non-duplication of variables*)
       let (u,cs) = List.fold_right (fun u (t,cs) -> type_consistent co d_env u t) ts (item_t,[]) in
       let t = {t = Tapp("vector",[(TA_nexp base);(TA_nexp rise);
 				  (TA_ord{order=(if inc_or_dec then Oinc else Odec)});(TA_typ u)])} in
@@ -329,7 +343,7 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
 	    let (pat',env,cons,t) = check_pattern envs emp_tag item_t pat in 
 	    (pat'::pats,t::ts,env::t_envs,cons@constraints))
 	  pats ([],[],[],[]) in
-      let env = List.fold_right (fun e env -> Envmap.union e env) envs Envmap.empty in (*Need to check for non-duplication of variables*)
+      let env = List.fold_right (fun e env -> Envmap.union e env) envs Envmap.empty in (*TODO Need to check for non-duplication of variables*)
       let u,cs = List.fold_right (fun u (t,cs) -> let t',cs' = type_consistent (Patt l) d_env u t in t',cs@cs') ts (item_t,[]) in
       let t = {t = Tapp("list",[TA_typ u])} in
       (P_aux(P_list(pats'),(l,Base(([],t),Emp_local,cs,pure_e))), env,constraints@cs,t)
@@ -436,11 +450,11 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
 	| L_hex s -> simp_exp e l {t = Tapp("vector",
 			                    [TA_nexp{nexp = Nconst zero};
 				             TA_nexp{nexp = Nconst (big_int_of_int ((String.length s)*4))};
-				             TA_ord{order = Oinc};TA_typ{t = Tid "bit"}])},[],pure_e
+				             TA_ord d_env.default_o;TA_typ{t = Tid "bit"}])},[],pure_e
 	| L_bin s -> simp_exp e l {t = Tapp("vector",
 			                    [TA_nexp{nexp = Nconst zero};
 				             TA_nexp{nexp = Nconst (big_int_of_int (String.length s))};
-				             TA_ord{order = Oinc};TA_typ{t = Tid"bit"}])},[],pure_e
+				             TA_ord d_env.default_o ;TA_typ{t = Tid"bit"}])},[],pure_e
 	| L_string s -> simp_exp e l {t = Tid "string"},[],pure_e
 	| L_undef -> simp_exp e l (new_t ()),[],{effect=Eset[BE_aux(BE_undef,l)]}) in
       let t',cs',e' = type_coerce (Expr l) d_env false (get_e_typ e) e expect_t in
@@ -658,13 +672,21 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
       (E_aux(E_for(id,from',to_',step',order,block'),(l,Base(([],b_t),Emp_local,local_cs,pure_e))),expect_t,Envmap.empty,
        b_c@from_c@to_c@step_c@local_cs,(union_effects b_ef (union_effects step_ef (union_effects to_ef from_ef))))
     | E_vector(es) ->
-      let item_t = match expect_t.t with
-        | Tapp("vector",[base;rise;ord;TA_typ item_t]) -> item_t
-        | _ -> new_t () in
+      let item_t,ord = match expect_t.t with
+        | Tapp("vector",[base;rise;TA_ord ord;TA_typ item_t]) -> item_t,ord
+        | _ -> new_t (),d_env.default_o in
       let es,cs,effect = (List.fold_right 
 			    (fun (e,_,_,c,ef) (es,cs,effect) -> (e::es),(c@cs),union_effects ef effect)
 			    (List.map (check_exp envs item_t) es) ([],[],pure_e)) in
-      let t = {t = Tapp("vector",[TA_nexp({nexp=Nconst zero});TA_nexp({nexp=Nconst (big_int_of_int (List.length es))});TA_ord({order=Oinc});TA_typ item_t])} in
+      let len = List.length es in
+      let t = match ord.order,d_env.default_o.order with
+        | (Oinc,_) | (Ouvar _,Oinc) | (Ovar _,Oinc) -> 
+          {t = Tapp("vector", [TA_nexp {nexp=Nconst zero}; TA_nexp {nexp = Nconst (big_int_of_int len)};
+                               TA_ord {order = Oinc}; TA_typ item_t])}
+        | (Odec,_) | (Ouvar _,Odec) | (Ovar _,Odec) -> 
+          {t = Tapp("vector",[TA_nexp {nexp=Nconst (big_int_of_int (len-1))};
+                              TA_nexp {nexp=Nconst (big_int_of_int len)};
+                              TA_ord {order= Odec}; TA_typ item_t])} in
       let t',cs',e' = type_coerce (Expr l) d_env false t (E_aux(E_vector es,(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in
       (e',t',t_env,cs@cs',effect)
     | E_vector_indexed(eis,(Def_val_aux(default,(ld,annot)))) ->
@@ -1329,7 +1351,7 @@ let check_type_def envs (TD_aux(td,(l,annot))) =
                                                      TA_nexp {nexp=Nconst (big_int_of_int ((i2 - i1) +1))}; TA_ord({order=Oinc}); TA_typ {t=Tid "bit"}])}
 			      else typ_error l ("register type declaration " ^ id' ^ " contains a field specification outside of the declared register size")
 			    else typ_error l ("register type declaration " ^ id' ^ " is not consistently increasing")
-			  | BF_concat _ -> assert false (* What is this supposed to imply again?*)),Emp_global,[],pure_e)))
+			  | BF_concat _ -> assert false (* TODO: This implies that the variable refers to a concatenation of the different ranges specified; so now I need to implement it thusly*)),Emp_global,[],pure_e)))
 		ranges 
 	    in
 	    let tannot = into_register d_env (Base(([],ty),Emp_global,[],pure_e)) in