summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/rewriter.ml26
-rw-r--r--src/type_check.ml43
-rw-r--r--src/type_internal.ml5
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) ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 15:14:11 +0000