Fix bug that was throwing away the cast telling the interpreter to read a register

3 files changed, 43 insertions, 37 deletions

diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index d863c2b2..4ce89f71 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -638,56 +638,56 @@ let rec pp_lem_let ppf (LB_aux(lb,(l,annot))) =
   fprintf ppf "@[<0>(LB_aux %a (%a, %a))@]" print_lb lb pp_lem_l l pp_annot annot
 
 and pp_lem_exp ppf (E_aux(e,(l,annot))) = 
-  let rec print_e ppf e = 
+  let print_e ppf e = 
     match e with
-    | E_block(exps) -> fprintf ppf "@[<0>%a [%a] %a@]"
-        kwd "(E_block" 
-        (list_pp pp_semi_lem_exp pp_lem_exp) exps
-        kwd ")"
-    | E_id(id) -> fprintf ppf "(%a %a)" kwd "E_id" pp_lem_id id
-    | E_lit(lit) -> fprintf ppf "(%a %a)" kwd "E_lit" pp_lem_lit lit
-    | E_cast(typ,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cast" pp_lem_typ typ pp_lem_exp exp 
+    | E_block(exps) -> fprintf ppf "@[<0>(E_aux %a [%a] %a (%a, %a))@]"
+      kwd "(E_block" 
+      (list_pp pp_semi_lem_exp pp_lem_exp) exps
+      kwd ")" pp_lem_l l pp_annot annot
+    | E_id(id) -> fprintf ppf "(E_aux (%a %a) (%a, %a))" kwd "E_id" pp_lem_id id pp_lem_l l pp_annot annot
+    | E_lit(lit) -> fprintf ppf "(E_aux (%a %a) (%a, %a))" kwd "E_lit" pp_lem_lit lit pp_lem_l l pp_annot annot
+    | E_cast(typ,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_cast" pp_lem_typ typ pp_lem_exp exp pp_lem_l l pp_annot annot
     | E_internal_cast((_,None),e) -> pp_lem_exp ppf e
     | E_internal_cast((_,Some((_,t),_,_,_)), (E_aux(ec,(_,eannot)) as exp)) ->
       (match t.t,eannot with
-	| Tapp("vector",[TA_nexp n1;_;_;_]),Some((_,{t=Tapp("vector",[TA_nexp n2;_;_;_])}),_,_,_) ->
-	  if nexp_eq n1 n2 
-	  then print_e ppf ec
-	  else fprintf ppf "@[<0>(E_cast %a %a)@]" pp_lem_typ (t_to_typ t) pp_lem_exp exp
-	| _ -> fprintf ppf "@[<0>(E_cast %a %a)@]" pp_lem_typ (t_to_typ t) pp_lem_exp exp)
-    | E_app(f,args) -> fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_app" pp_lem_id f (list_pp pp_semi_lem_exp pp_lem_exp) args
-    | E_app_infix(l,op,r) -> fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_app_infix" pp_lem_exp l pp_lem_id op pp_lem_exp r
-    | E_tuple(exps) -> fprintf ppf "@[<0>%a [%a] %a@]" kwd "(E_tuple" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")"
-    | E_if(c,t,e) -> fprintf ppf "@[<0>(%a %a @[<1>%a@] @[<1> %a@])@]" kwd "E_if" pp_lem_exp c pp_lem_exp t pp_lem_exp e
+      | Tapp("vector",[TA_nexp n1;_;_;_]),Some((_,{t=Tapp("vector",[TA_nexp n2;_;_;_])}),_,_,_) ->
+	if nexp_eq n1 n2 
+	  then pp_lem_exp ppf exp
+	else fprintf ppf "@[<0>(E_aux (E_cast %a %a) (%a, %a))@]" pp_lem_typ (t_to_typ t) pp_lem_exp exp pp_lem_l l pp_annot annot
+      | _ -> fprintf ppf "@[<0>(E_aux (E_cast %a %a) (%a, %a))@]" pp_lem_typ (t_to_typ t) pp_lem_exp exp pp_lem_l l pp_annot annot)
+    | E_app(f,args) -> fprintf ppf "@[<0>(E_aux (%a %a [%a]) (%a, %a))@]" kwd "E_app" pp_lem_id f (list_pp pp_semi_lem_exp pp_lem_exp) args pp_lem_l l pp_annot annot
+    | E_app_infix(l',op,r) -> fprintf ppf "@[<0>(E_aux (%a %a %a %a) (%a, %a))@]" kwd "E_app_infix" pp_lem_exp l' pp_lem_id op pp_lem_exp r pp_lem_l l pp_annot annot
+    | E_tuple(exps) -> fprintf ppf "@[<0>(E_aux %a [%a] %a (%a, %a))@]" kwd "(E_tuple" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")" pp_lem_l l pp_annot annot
+    | E_if(c,t,e) -> fprintf ppf "@[<0>(E_aux (%a %a @[<1>%a@] @[<1> %a@]) (%a, %a))@]" kwd "E_if" pp_lem_exp c pp_lem_exp t pp_lem_exp e pp_lem_l l pp_annot annot
     | E_for(id,exp1,exp2,exp3,order,exp4) ->
-      fprintf ppf "@[<0>(%a %a %a %a %a %a @ @[<1> %a @])@]" 
-	kwd "E_for" pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3 pp_lem_ord order pp_lem_exp exp4
-    | E_vector(exps) -> fprintf ppf "@[<0>(%a [%a])@]" kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps
+      fprintf ppf "@[<0>(E_aux (%a %a %a %a %a %a @ @[<1> %a @]) (%a, %a))@]" 
+	kwd "E_for" pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3 pp_lem_ord order pp_lem_exp exp4 pp_lem_l l pp_annot annot
+    | E_vector(exps) -> fprintf ppf "@[<0>(E_aux (%a [%a]) (%a, %a))@]" kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps pp_lem_l l pp_annot annot
     | E_vector_indexed(iexps) -> 
       let iformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) %a@]" i kwd ", " pp_lem_exp e kwd ";" in
       let lformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) @]" i kwd ", " pp_lem_exp e in
-      fprintf ppf "@[<0>(%a [%a]) @]" kwd "E_vector_indexed" (list_pp iformat lformat) iexps
-    | E_vector_access(v,e) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_vector_access" pp_lem_exp v pp_lem_exp e
+      fprintf ppf "@[<0>(E_aux (%a [%a]) (%a, %a))@]" kwd "E_vector_indexed" (list_pp iformat lformat) iexps pp_lem_l l pp_annot annot
+    | E_vector_access(v,e) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_vector_access" pp_lem_exp v pp_lem_exp e pp_lem_l l pp_annot annot
     | E_vector_subrange(v,e1,e2) -> 
-      fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_vector_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 
+      fprintf ppf "@[<0>(E_aux (%a %a %a %a) (%a, %a))@]" kwd "E_vector_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_l l pp_annot annot
     | E_vector_update(v,e1,e2) -> 
-      fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_vector_update" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2
+      fprintf ppf "@[<0>(E_aux (%a %a %a %a) (%a, %a))@]" kwd "E_vector_update" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_l l pp_annot annot
     | E_vector_update_subrange(v,e1,e2,e3) -> 
-      fprintf ppf "@[<0>(%a %a %a %a %a)@]" kwd "E_vector_update_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_exp e3 
-    | E_list(exps) -> fprintf ppf "@[<0>(%a [%a])@]" kwd "E_list" (list_pp pp_semi_lem_exp pp_lem_exp) exps
-    | E_cons(e1,e2) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cons" pp_lem_exp e1 pp_lem_exp e2
+      fprintf ppf "@[<0>(E_aux (%a %a %a %a %a) (%a, %a))@]" kwd "E_vector_update_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_exp e3 pp_lem_l l pp_annot annot
+    | E_list(exps) -> fprintf ppf "@[<0>(E_aux (%a [%a]) (%a, %a))@]" kwd "E_list" (list_pp pp_semi_lem_exp pp_lem_exp) exps pp_lem_l l pp_annot annot
+    | E_cons(e1,e2) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_cons" pp_lem_exp e1 pp_lem_exp e2 pp_lem_l l pp_annot annot
     | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> 
-      fprintf ppf "@[<0>(%a [%a]))@]" kwd "E_record(FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps
+      fprintf ppf "@[<0>(E_aux (%a [%a])) (%a, %a))@]" kwd "E_record(FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps pp_lem_l l pp_annot annot
     | E_record_update(exp,(FES_aux(FES_Fexps(fexps,_),_))) ->
-      fprintf ppf "@[<0>(%a %a (%a [%a]))@]" 
-	kwd "E_record_update" pp_lem_exp exp kwd "FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps 
-    | E_field(fexp,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_field" pp_lem_exp fexp pp_lem_id id
+      fprintf ppf "@[<0>(E_aux (%a %a (%a [%a])) (%a, %a))@]" 
+	kwd "E_record_update" pp_lem_exp exp kwd "FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps pp_lem_l l pp_annot annot
+    | E_field(fexp,id) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_field" pp_lem_exp fexp pp_lem_id id pp_lem_l l pp_annot annot
     | E_case(exp,pexps) -> 
-      fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_case" pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps
-    | E_let(leb,exp) -> fprintf ppf "@[<0>(%a %a %a) @]" kwd "E_let" pp_lem_let leb pp_lem_exp exp
-    | E_assign(lexp,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp
+      fprintf ppf "@[<0>(E_aux (%a %a [%a]) (%a, %a))@]" kwd "E_case" pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps pp_lem_l l pp_annot annot
+    | E_let(leb,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_let" pp_lem_let leb pp_lem_exp exp pp_lem_l l pp_annot annot
+    | E_assign(lexp,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp pp_lem_l l pp_annot annot
   in
-  fprintf ppf "@[<0>(E_aux %a (%a, %a))@]" print_e e pp_lem_l l pp_annot annot
+  print_e ppf e
 
 and pp_semi_lem_exp ppf e = fprintf ppf "@[<1>%a%a@]" pp_lem_exp e kwd ";"
 
diff --git a/src/type_check.ml b/src/type_check.ml
index aa13639a..9d9b64fd 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -583,12 +583,15 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
       (e',t',t_env,cs@cs',effect)
     | E_vector_access(vec,i) ->
       let base,rise,ord = new_n(),new_n(),new_o() in
-      let min,m_rise = new_n(),new_n() in
       let item_t = new_t () in
+      let min,m_rise = new_n(),new_n() in
       let vt = {t= Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord; TA_typ item_t])} in
       let (vec',t',_,cs,ef) = check_exp envs vt vec in
       let it = {t= Tapp("range",[TA_nexp min;TA_nexp m_rise])} in
       let (i',ti',_,cs_i,ef_i) = check_exp envs it i in
+      let ord,item_t = match t'.t with
+        | Tabbrev(_,{t=Tapp("vector",[_;_;TA_ord ord;TA_typ t])}) | Tapp("vector",[_;_;TA_ord ord;TA_typ t]) -> ord,t
+        | _ -> ord,item_t in
       let cs_loc = 
 	match ord.order with
 	  | Oinc ->
@@ -597,6 +600,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
 	    [GtEq((Expr l),base,min); LtEq((Expr l),{nexp=Nadd(min,m_rise)},{nexp=Nadd(base,{nexp=Nneg rise})})]
 	  | _ -> typ_error l "A vector must be either increasing or decreasing to access a single element"
       in 
+      (*let _ = Printf.printf "Type checking vector access. item_t is %s and expect_t is %s\n" (t_to_string item_t) (t_to_string expect_t) in*)
       let t',cs',e'=type_coerce (Expr l) d_env item_t (E_aux(E_vector_access(vec',i'),(l,Some(([],item_t),Emp_local,[],pure_e)))) expect_t in
       (e',t',t_env,cs_loc@cs_i@cs@cs',union_effects ef ef_i)
     | E_vector_subrange(vec,i1,i2) ->
@@ -902,6 +906,7 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan
           let t_actual = match t.t with 
             | Tabbrev(i,t) -> t
             | _ -> t in
+          (*let _ = Printf.printf "Assigning to %s, t is %s\n" i (t_to_string t_actual) in*)
 	  (match t_actual.t,is_top with
 	    | Tapp("register",[TA_typ u]),_ ->
 	      let ef = {effect=Eset[BE_aux(BE_wreg,l)]} in
diff --git a/src/type_internal.ml b/src/type_internal.ml
index e406e976..04bec4e4 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -940,7 +940,8 @@ let rec type_coerce_internal co d_env t1 cs1 e t2 cs2 =
     | "register",_ ->
       (match args1 with
 	| [TA_typ t] ->
-          let new_e = E_aux(E_cast(t_to_typ t,e),(l,Some(([],t),External None,[],pure_e))) in (*Wrong effect, should be reading a register*)
+          (*let _ = Printf.printf "Adding cast to remove register read\n" in*)
+          let new_e = E_aux(E_cast(t_to_typ t,e),(l,Some(([],t),External None,[],(add_effect (BE_aux(BE_rreg, l)) pure_e)))) in
 	  type_coerce co d_env t new_e t2
 	| _ -> raise (Reporting_basic.err_unreachable l "register is not properly kinded"))
     | _,_ ->