Change rewriter to better reset dec vectors to count from (length - 1) instead of whatever random spot they might be in, where functions expect length-n to 0

3 files changed, 46 insertions, 28 deletions

diff --git a/src/rewriter.ml b/src/rewriter.ml
index eccdcc28..acba482e 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -113,24 +113,40 @@ let rec rewrite_exp (E_aux (exp,(l,annot))) =
     | E_exit e -> rewrap (E_exit (rewrite_exp e))
     | E_internal_cast ((_,casted_annot),exp) -> 
       let new_exp = rewrite_exp exp in
+      (*let _ = Printf.eprintf "Removing an internal_cast with %s\n" (tannot_to_string casted_annot) in*)
       (match casted_annot,exp with
 	| Base((_,t),_,_,_,_),E_aux(ec,(ecl,Base((_,exp_t),_,_,_,_))) ->
+	  (*let _ = Printf.eprintf "Considering removing an internal cast where the two types are %s and %s\n" (t_to_string t) (t_to_string exp_t) in*)
 	  (match t.t,exp_t.t with
 	    (*TODO should pass d_env into here so that I can look at the abbreviations if there are any here*)
 	    | Tapp("vector",[TA_nexp n1;TA_nexp nw1;TA_ord o1;_]),
-	      Tapp("vector",[TA_nexp n2;TA_nexp nw2;TA_ord o2;_]) ->
+	      Tapp("vector",[TA_nexp n2;TA_nexp nw2;TA_ord o2;_]) 
+	    | Tapp("vector",[TA_nexp n1;TA_nexp nw1;TA_ord o1;_]),
+	      Tapp("reg",[TA_typ {t=(Tapp("vector",[TA_nexp n2; TA_nexp nw2; TA_ord o2;_]))}]) ->
 	      (match n1.nexp with
 		| Nconst i1 -> if nexp_eq n1 n2 then new_exp else rewrap (E_cast (t_to_typ t,new_exp))
 		| _ -> (match o1.order with
 		    | Odec -> 
 		      (*let _ = Printf.eprintf "Considering removing a cast or not: %s %s, %b\n" (n_to_string nw1) (n_to_string n1) (nexp_one_more_than nw1 n1) in*)
-		      if nexp_one_more_than nw1 n1 
-		      then rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"), Unknown)), Unknown), new_exp))
-		      else new_exp
+		      (*if nexp_one_more_than nw1 n1 
+		      then *) rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"), Unknown)), Unknown), new_exp))
+		      (*else new_exp*)
 		    | _ -> new_exp)
 		| _ ->  new_exp)
 	    | _ -> new_exp)
-	| _ -> new_exp)
+	| Base((_,t),_,_,_,_),_ ->
+	  (*let _ = Printf.eprintf "Considering removing an internal cast where the remaining type is %s\n%!" (t_to_string t) in*)
+	  (match t.t with
+	    | Tapp("vector",[TA_nexp n1;TA_nexp nw1;TA_ord o1;_]) ->
+	      (match o1.order with
+		| Odec -> 
+		  (*let _ = Printf.eprintf "Considering removing a cast or not: %s %s, %b\n" (n_to_string nw1) (n_to_string n1) (nexp_one_more_than nw1 n1) in
+		  if nexp_one_more_than nw1 n1 
+		  then*) rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"), Unknown)), Unknown), new_exp))
+		  (*else new_exp*)
+		| _ -> new_exp)
+	    | _ -> new_exp)
+	| _ -> (*let _ = Printf.eprintf "Not a base match?\n" in*) new_exp)
     | E_internal_exp (l,impl) ->
       (match impl with
 	| Base((_,t),_,_,_,bounds) ->
diff --git a/src/type_check.ml b/src/type_check.ml
index 0c6cbf46..8ee47e10 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -952,41 +952,41 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       (*let _ = Printf.eprintf "checking e_vector_subrange: expect_t is %s\n" (t_to_string expect_t) in*)
       let base,length,ord = new_n(),new_n(),new_o() in
       let new_length = new_n() in
-      let n1_size = new_n() in
-      let n2_size = new_n() in
+      let n1_start = new_n() in
+      let n2_end = new_n() in
       let item_t = match expect_t.t with
 	| Tapp("vector",[TA_nexp base_n;TA_nexp rise_n; TA_ord ord_n; TA_typ item_t]) -> item_t
 	| _ -> new_t() in
       let vt = {t=Tapp("vector",[TA_nexp base;TA_nexp length;TA_ord ord;TA_typ item_t])} in
       let (vec',vt',_,cs,_,ef) = check_exp envs imp_param vt vec in      
-      let i1t = {t=Tapp("atom",[TA_nexp n1_size])} in
+      let i1t = {t=Tapp("atom",[TA_nexp n1_start])} in
       let (i1', ti1, _,cs_i1,_,ef_i1) = check_exp envs imp_param i1t i1 in
-      let i2t = {t=Tapp("atom",[TA_nexp n2_size])} in
+      let i2t = {t=Tapp("atom",[TA_nexp n2_end])} in
       let (i2', ti2, _,cs_i2,_,ef_i2) = check_exp envs imp_param i2t i2 in
       let cs_loc =
 	match (ord.order,d_env.default_o.order) with
 	  | (Oinc,_) -> 
-	    [LtEq((Expr l), Require, base, n1_size);
-	     LtEq((Expr l), Require, n1_size, n2_size);
-	     LtEq((Expr l), Require, n2_size, mk_sub (mk_add base length) n_one);
-	     Eq((Expr l), new_length, mk_add (mk_sub n2_size n1_size) n_one)]
+	    [LtEq((Expr l), Require, base, n1_start);
+	     LtEq((Expr l), Require, n1_start, n2_end);
+	     LtEq((Expr l), Require, n2_end, mk_sub (mk_add base length) n_one);
+	     Eq((Expr l), new_length, mk_add (mk_sub n2_end n1_start) n_one)]
 	  | (Odec,_) ->
-	    [GtEq((Expr l), Require, base, n1_size);
-	     GtEq((Expr l), Require, n1_size, n2_size);
-	     GtEq((Expr l), Require, n2_size, mk_add (mk_sub base length) n_one);
-	     Eq((Expr l), new_length, mk_add (mk_sub n1_size n2_size) n_one)]	    
+	    [GtEq((Expr l), Require, base, n1_start);
+	     GtEq((Expr l), Require, n1_start, n2_end);
+	     GtEq((Expr l), Require, n2_end, mk_add (mk_sub base length) n_one);
+	     Eq((Expr l), new_length, mk_add (mk_sub n1_start n2_end) n_one)]	    
 	  | (_,Oinc) ->
-	    [LtEq((Expr l), Require, base, n1_size);
-	     LtEq((Expr l), Require, n1_size, n2_size);
-	     LtEq((Expr l), Require, n2_size, mk_sub (mk_add base length) n_one);
-	     Eq((Expr l), new_length, mk_add (mk_sub n2_size n1_size) n_one)]
+	    [LtEq((Expr l), Require, base, n1_start);
+	     LtEq((Expr l), Require, n1_start, n2_end);
+	     LtEq((Expr l), Require, n2_end, mk_sub (mk_add base length) n_one);
+	     Eq((Expr l), new_length, mk_add (mk_sub n2_end n1_start) n_one)]
 	  | (_,Odec) -> 
-	    [GtEq((Expr l), Require, base, n1_size);
-	     GtEq((Expr l), Require, n1_size, n2_size);
-	     GtEq((Expr l), Require, n2_size, mk_add (mk_sub base length) n_one);
-	     Eq((Expr l), new_length, mk_add (mk_sub n1_size n2_size) n_one)]
+	    [GtEq((Expr l), Require, base, n1_start);
+	     GtEq((Expr l), Require, n1_start, n2_end);
+	     GtEq((Expr l), Require, n2_end, mk_add (mk_sub base length) n_one);
+	     Eq((Expr l), new_length, mk_add (mk_sub n1_start n2_end) n_one)]
 	  | _ -> typ_error l "A vector must be either increasing or decreasing to access a slice" in
-      let nt = {t = Tapp("vector", [TA_nexp n1_size; TA_nexp new_length; TA_ord ord; TA_typ item_t]) } in
+      let nt = {t = Tapp("vector", [TA_nexp n1_start; TA_nexp new_length; TA_ord ord; TA_typ item_t]) } in
       let (t,cs3,ef3,e') = 
 	type_coerce (Expr l) d_env Require false false b_env nt 
 	  (E_aux(E_vector_subrange(vec',i1',i2'),(l,constrained_annot nt cs_loc))) expect_t in
@@ -1066,6 +1066,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       let item_t,ord = match expect_t.t with
         | Tapp("vector",[_;_;TA_ord o;TA_typ i]) -> i,o
         | Tapp("range",_) -> bit_t,new_o ()
+	| Tapp("atom",_) -> bit_t, new_o ()
         | _ -> new_t (),new_o () in
       let base1,rise1 = new_n(), new_n() in
       let base2,rise2 = new_n(),new_n() in
diff --git a/src/type_internal.ml b/src/type_internal.ml
index e29aa64c..debd676e 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -2274,9 +2274,10 @@ let rec type_consistent_internal co d_env enforce widen t1 cs1 t2 cs2 =
 	else ({t=Tapp ("range",[TA_nexp a2;TA_nexp a1])},csp)
       (*| Nconst _, Nuvar _ | Nuvar _, Nconst _->
 	(t1, csp@[Eq(co,a1,a2)])*) (*TODO This is the correct constraint. However, without the proper support for In checks actually working, this will cause specs to not build*)	
-      | _ -> let nu1,nu2 = new_n (),new_n () in 
+      | _ -> (*let nu1,nu2 = new_n (),new_n () in 
 	     ({t=Tapp("range",[TA_nexp nu1;TA_nexp nu2])},
-	      csp@[LtEq(co,enforce,nu1,a1);LtEq(co,enforce,nu1,a2);LtEq(co,enforce,a1,nu2);LtEq(co,enforce,a2,nu2)]))
+	      csp@[LtEq(co,enforce,nu1,a1);LtEq(co,enforce,nu1,a2);LtEq(co,enforce,a1,nu2);LtEq(co,enforce,a2,nu2)])*)
+	(t1, csp@[LtEq(co,enforce,a1,a2);(GtEq(co,enforce,a1,a2))])) (*EQ is the right thing to do, but see above. Introducing new free vars here is bad*)
   | Tapp("vector",[TA_nexp _; TA_nexp l1; ord; ty1]),Tapp("vector",[TA_nexp _; TA_nexp l2; ord2; ty2]) ->
     (t2, Eq(co,l1,l2)::((type_arg_eq co d_env enforce widen ord ord2)@(type_arg_eq co d_env enforce widen ty1 ty2)))
   | Tapp(id1,args1), Tapp(id2,args2) ->