Fixes for power compilation reworking

3 files changed, 31 insertions, 25 deletions

diff --git a/src/parser.mly b/src/parser.mly
index 2ae64887..3f8b6db5 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -404,6 +404,8 @@ exp_typ:
      { $1 }
    | TwoStarStar atomic_typ
      { tloc (ATyp_exp($2)) }
+   | TwoStarStar Num
+     { tloc (ATyp_exp (tloc (ATyp_constant $2))) }
 
 nexp_typ:
    | exp_typ
diff --git a/src/type_check.ml b/src/type_check.ml
index ea95a0bd..e20851de 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -800,7 +800,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
         let else',else_t,else_env,else_c,else_bs,else_ef = check_exp envs imp_param (new_t ()) else_ in
 	(*TOTHINK Possibly I should first consistency check else and then, with Guarantee, then check against expect_t with Require*)
         let then_t',then_c' = type_consistent (Expr l) d_env Require true then_t expect_t in
-        let else_t',else_c' = type_consistent (Expr l) d_env Require true else_t then_t'  in
+        let else_t',else_c' = type_consistent (Expr l) d_env Require true else_t expect_t  in
         let t_cs = CondCons((Expr l),c1,then_c@then_c') in
         let e_cs = CondCons((Expr l),[],else_c@else_c') in
         (E_aux(E_if(cond',then',else'),(l,simple_annot expect_t)),
@@ -900,26 +900,30 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	                          (E_aux (E_vector_indexed(es,default'),(l,simple_annot t))) expect_t in
       (e',t',t_env,cs@cs_d@cs_bounds@cs',nob,union_effects ef_d (union_effects ef' effect))
     | E_vector_access(vec,i) ->
-      let base,rise,ord = new_n(),new_n(),new_o() in
+      let base,len,ord = new_n(),new_n(),new_o() 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 min,max = new_n(),new_n() in
+      let vt = {t= Tapp("vector",[TA_nexp base;TA_nexp len;TA_ord ord; TA_typ item_t])} in
       let (vec',t',_,cs,_,ef) = check_exp envs imp_param vt vec in
-      let it = {t= Tapp("range",[TA_nexp min;TA_nexp m_rise])} in
+      let it = {t= Tapp("range",[TA_nexp min;TA_nexp max])} in
       let (i',ti',_,cs_i,_,ef_i) = check_exp envs imp_param 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 oinc_max_access = mk_sub (mk_add base len) n_one in
+      let odec_min_access = mk_sub base len in
       let cs_loc = 
 	match (ord.order,d_env.default_o.order) with
 	  | (Oinc,_) ->
-	    [LtEq((Expr l),Require,base,min); LtEq((Expr l),Require, mk_add min m_rise,mk_add base rise)] 
+	    [LtEq((Expr l),Require,base,min); 
+	     LtEq((Expr l),Require, max,oinc_max_access); LtEq((Expr l),Require, min,oinc_max_access)] 
 	  | (Odec,_) -> 
-	    [GtEq((Expr l),Require,base,min); LtEq((Expr l),Require,mk_add min m_rise,mk_sub base rise)]
+	    [GtEq((Expr l),Require,base,min); LtEq((Expr l),Require,min,odec_min_access); LtEq((Expr l),Require,max,odec_min_access)]
 	  | (_,Oinc) -> 
-	    [LtEq((Expr l),Require,base,min); LtEq((Expr l),Require,mk_add min m_rise, mk_add base rise)] 
+	    [LtEq((Expr l),Require,base,min); 
+	     LtEq((Expr l),Require, max,oinc_max_access); LtEq((Expr l),Require, min,oinc_max_access)] 
 	  | (_,Odec) ->
-	    [GtEq((Expr l),Require,base,min); LtEq((Expr l),Require, mk_add min m_rise, mk_sub base rise)]
+	    [GtEq((Expr l),Require,base,min); LtEq((Expr l),Require,min,odec_min_access); LtEq((Expr l),Require,max,odec_min_access)]
 	  | _ -> typ_error l "A vector must be either increasing or decreasing to access a single element"
       in 
       (*let _ = Printf.eprintf "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*)
@@ -1467,8 +1471,8 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp *
       (match item_actual.t with
 	| Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ t]) ->
 	  let acc_t = match ord.order with
-	    | Oinc -> {t = Tapp("range",[TA_nexp base;TA_nexp rise])} 
-	    | Odec -> {t = Tapp("range",[TA_nexp (mk_sub base rise);TA_nexp rise])} 
+	    | Oinc -> {t = Tapp("range",[TA_nexp base;TA_nexp (mk_sub (mk_add base rise) n_one)])} 
+	    | Odec -> {t = Tapp("range",[TA_nexp (mk_sub (mk_sub base rise) n_one);TA_nexp (mk_sub base n_one)])} 
 	    | _ -> typ_error l ("Assignment to one vector element requires either inc or dec order")
 	  in
 	  let (e,t',_,cs',_,ef_e) = check_exp envs imp_param acc_t acc in
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 06372e15..09775475 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1305,8 +1305,8 @@ let initial_typ_env =
        Base(((mk_typ_params ["a";"b";"c"]),
              (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})), External (Some "mod"),[],pure_e,nob),
        true,
-       [Base(((mk_nat_params["n";"m";"o"]),
-              (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m"); mk_range n_one (mk_nv "o")])
+       [Base(((mk_nat_params["n";"m";"o";"p"]),
+              (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m"); mk_range (mk_nv "p") (mk_nv "o")])
                            (mk_range n_zero (mk_sub (mk_nv "o") n_one)))),
              External (Some "mod"),[GtEq(Specc(Parse_ast.Int("mod",None)),Require,(mk_nv "o"),n_one)],pure_e,nob);
         Base(((mk_nat_params["n";"m";"o"])@(mk_ord_params["ord"]),
@@ -1962,13 +1962,13 @@ let rec conforms_to_t d_env loosely within_coercion spec actual =
       conforms_to_t d_env loosely within_coercion ts ta
       && conforms_to_o loosely os oa
       && conforms_to_n false within_coercion eq_big_int rs ra
-    | (Tapp("range",[TA_nexp bs;TA_nexp rs]),Tapp("range",[TA_nexp ba;TA_nexp ra]),_) ->
-      conforms_to_n true within_coercion le_big_int bs ba && conforms_to_n true within_coercion ge_big_int rs ra 
-    | (Tapp("atom",[TA_nexp n]),Tapp("range",[TA_nexp ba;TA_nexp ra]),_) ->
-      conforms_to_n true within_coercion le_big_int ba n && conforms_to_n true within_coercion ge_big_int n ra
-    | (Tapp("range",[TA_nexp bs;TA_nexp rs]),Tapp("atom",[TA_nexp n]),_) ->
+    | (Tapp("range",[TA_nexp bs;TA_nexp rs]),Tapp("range",[TA_nexp ba;TA_nexp ra]),_) -> true (*
+      conforms_to_n true within_coercion le_big_int bs ba && conforms_to_n true within_coercion ge_big_int rs ra *)
+    | (Tapp("atom",[TA_nexp n]),Tapp("range",[TA_nexp ba;TA_nexp ra]),_) -> true (*
+      conforms_to_n true within_coercion le_big_int ba n && conforms_to_n true within_coercion ge_big_int n ra *)
+    | (Tapp("range",[TA_nexp bs;TA_nexp rs]),Tapp("atom",[TA_nexp n]),_) -> true (*
       conforms_to_n true within_coercion le_big_int bs n && conforms_to_n true within_coercion ge_big_int rs n &&
-	conforms_to_n true within_coercion ge_big_int bs n
+	conforms_to_n true within_coercion ge_big_int bs n *)
     | (Tapp(is,tas), Tapp(ia, taa),_) -> 
 (*      let _ = Printf.printf "conforms to given two apps: %b, %b\n" (is = ia) (List.length tas = List.length taa) in*)
       (is = ia) && (List.length tas = List.length taa) && (List.for_all2 (conforms_to_ta d_env loosely within_coercion) tas taa)
@@ -2023,11 +2023,11 @@ let rec type_consistent_internal co d_env enforce widen t1 cs1 t2 cs2 =
   | Tapp("range",[TA_nexp b1;TA_nexp r1;]),Tapp("range",[TA_nexp b2;TA_nexp r2;]) -> 
     if (nexp_eq b1 b2)&&(nexp_eq r1 r2) 
     then (t2,csp)
-    else (t1, csp@[GtEq(co,enforce,b1,b2);LtEq(co,enforce,r1,r2)])
+    else (t1, csp@[LtEq(co,enforce,b1,b2);LtEq(co,enforce,r1,r2)])
   | Tapp("atom",[TA_nexp a]),Tapp("range",[TA_nexp b1; TA_nexp r1]) ->
     (t1, csp@[GtEq(co,enforce,a,b1);LtEq(co,enforce,a,r1)])
   | Tapp("range",[TA_nexp b1; TA_nexp r1]),Tapp("atom",[TA_nexp a]) ->
-    (t2, csp@[GtEq(co,enforce,b1,a);LtEq(co,enforce,r1,a)])
+    (t2, csp@[LtEq(co,enforce,b1,a);LtEq(co,enforce,r1,a)])
   | Tapp("atom",[TA_nexp a1]),Tapp("atom",[TA_nexp a2]) ->
     if nexp_eq a1 a2
     then (t2,csp)
@@ -2160,11 +2160,11 @@ let rec type_coerce_internal co d_env enforce is_explicit widen t1 cs1 e t2 cs2
       (match args1,args2 with
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
         [TA_nexp b2;TA_nexp r2;] -> 
-	let cs = [Eq(co,b2,n_zero);GtEq(co,Guarantee,r2,mk_sub {nexp=N2n(r1,None)} n_one)] in
+	let cs = [Eq(co,b2,n_zero);LtEq(co,Guarantee,mk_sub {nexp=N2n(r1,None)} n_one,r2)] in
 	(t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num_inc",l)),[e]),(l,Base(([],t2),External None,cs,pure_e,nob))))
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}],
         [TA_nexp b2;TA_nexp r2;] -> 
-	let cs = [Eq(co,b2,n_zero);GtEq(co,Guarantee,r2,mk_sub {nexp=N2n(r1,None)} n_one)] in
+	let cs = [Eq(co,b2,n_zero);LtEq(co,Guarantee,mk_sub {nexp=N2n(r1,None)} n_one,r2)] in
 	(t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num_dec",l)),[e]),(l,Base(([],t2),External None,cs,pure_e,nob))))
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> 
 	eq_error l "Cannot convert a vector to an range without an order"
@@ -2175,11 +2175,11 @@ let rec type_coerce_internal co d_env enforce is_explicit widen t1 cs1 e t2 cs2
       (match args1,args2 with
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
         [TA_nexp b2] -> 
-	let cs = [GtEq(co,Guarantee,b2,mk_sub {nexp=N2n(r1,None)} n_one)] in
+	let cs = [GtEq(co,Guarantee,b2,n_zero);LtEq(co,Guarantee,b2,mk_sub {nexp=N2n(r1,None)} n_one)] in
 	(t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num_inc",l)),[e]),(l,Base(([],t2),External None,cs,pure_e,nob))))
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}],
         [TA_nexp b2] -> 
-	let cs = [GtEq(co,Guarantee,b2,mk_sub {nexp=N2n(r1,None)} n_one)] in
+	let cs = [Eq(co,b2,mk_sub {nexp=N2n(r1,None)} n_one)] in
 	(t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num_dec",l)),[e]),(l,Base(([],t2),External None,cs,pure_e,nob))))
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> 
 	eq_error l "Cannot convert a vector to an range without an order"