diff options
| -rw-r--r-- | src/rewriter.ml | 9 | ||||
| -rw-r--r-- | src/type_internal.ml | 10 | ||||
| -rw-r--r-- | src/type_internal.mli | 1 |
3 files changed, 12 insertions, 8 deletions
diff --git a/src/rewriter.ml b/src/rewriter.ml index 496132b8..235b4f5f 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -89,6 +89,7 @@ let fix_effsum_exp (E_aux (e,(l,annot))) = | E_let (lb,e) -> union_effs [get_effsum_lb lb;get_effsum_exp e] | E_assign (lexp,e) -> union_effs [get_effsum_lexp lexp;get_effsum_exp e] | E_exit e -> get_effsum_exp e + | E_assert (c,m) -> pure_e | E_internal_cast (_,e) -> get_effsum_exp e | E_internal_exp _ -> pure_e | E_internal_exp_user _ -> pure_e @@ -343,7 +344,7 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) = | 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" + (*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*) rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"),Parse_ast.Generated l)), Parse_ast.Generated l),new_exp)) @@ -356,8 +357,8 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) = | 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*) + 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 rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"), Parse_ast.Generated l)), Parse_ast.Generated l), new_exp)) | _ -> new_exp) @@ -367,7 +368,7 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) = (match impl with | Base((_,t),_,_,_,_,bounds) -> let bounds = match nmap with | None -> bounds | Some (nm,_) -> add_map_to_bounds nm bounds in - (*let _ = Printf.eprintf "Rewriting internal expression, with type %s\n" (t_to_string t) in*) + (*let _ = Printf.eprintf "Rewriting internal expression, with type %s, and bounds %s\n" (t_to_string t) (bounds_to_string bounds) in*) (match t.t with (*Old case; should possibly be removed*) | Tapp("register",[TA_typ {t= Tapp("vector",[ _; TA_nexp r;_;_])}]) diff --git a/src/type_internal.ml b/src/type_internal.ml index d4eeefdf..22e79de8 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -1442,6 +1442,7 @@ let cons_efs_annot t cs efl efr = Base(([],t),Emp_local,cs,efl,efr,nob) let efs_annot t efl efr = Base(([],t),Emp_local,[],efl,efr,nob) let tag_efs_annot t tag efl efr = Base(([],t),tag,[],efl,efr,nob) let cons_bs_annot t cs bs = Base(([],t),Emp_local,cs,pure_e,pure_e,bs) +let cons_bs_annot_efr t cs bs efr = Base(([],t), Emp_local, cs, pure_e, efr, bs) let initial_abbrev_env = Envmap.from_list [ @@ -2839,13 +2840,13 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}], [TA_nexp b2;TA_nexp r2;] -> let cs = [] (*[LtEq(co,Guarantee,r2,mk_sub {nexp=N2n(r1,None)} n_one)] (*This constraint failing should be a warning, but truncation is ok*)*) in - let tannot = (l, constrained_annot_efr t2 cs (get_cummulative_effects (get_eannot e))) in + let tannot = (l, cons_bs_annot_efr t2 cs bounds (get_cummulative_effects (get_eannot e))) in (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_inc",l)), [(E_aux(E_internal_exp(tannot), tannot));e]),tannot)) | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}], [TA_nexp b2;TA_nexp r2;] -> let cs = [] (* See above [LtEq(co,Guarantee,r2,mk_sub {nexp=N2n(r1,None)} n_one)]*) in - let tannot = (l, constrained_annot_efr t2 cs (get_cummulative_effects (get_eannot e))) in + let tannot = (l, cons_bs_annot_efr t2 cs bounds (get_cummulative_effects (get_eannot e))) in (*let _ = Printf.eprintf "Generating to_vec_dec call: bounds are %s\n" (bounds_to_string bounds) in*) (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_dec",l)), [(E_aux(E_internal_exp(tannot), tannot)); e]),tannot)) @@ -2859,13 +2860,14 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}], [TA_nexp b2] -> let cs = [](*[LtEq(co,Guarantee,b2,mk_sub {nexp=N2n(r1,None)} n_one)]*) in - let tannot = (l, constrained_annot_efr t2 cs (get_cummulative_effects (get_eannot e))) in + let tannot = (l, cons_bs_annot_efr t2 cs bounds (get_cummulative_effects (get_eannot e))) in (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_inc",l)), [(E_aux(E_internal_exp(tannot), tannot));e]),tannot)) | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}], [TA_nexp b2] -> let cs = [](*[LtEq(co,Guarantee,b2,mk_sub {nexp=N2n(r1,None)} n_one)]*) in - let tannot = (l, constrained_annot_efr t2 cs (get_cummulative_effects (get_eannot e))) in + let tannot = (l, cons_bs_annot_efr t2 cs bounds (get_cummulative_effects (get_eannot e))) in + (*let _ = Printf.eprintf "Generating to_vec_dec call: bounds are %s\n" (bounds_to_string bounds) in*) (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_dec",l)), [(E_aux(E_internal_exp(tannot), tannot)); e]),tannot)) | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> diff --git a/src/type_internal.mli b/src/type_internal.mli index 3ce965c1..1748f0a7 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -224,6 +224,7 @@ val cons_efs_annot : t -> nexp_range list -> effect -> effect -> tannot val efs_annot : t -> effect -> effect -> tannot val tag_efs_annot: t -> tag -> effect -> effect -> tannot val cons_bs_annot : t -> nexp_range list -> bounds_env -> tannot +val cons_bs_annot_efr : t -> nexp_range list -> bounds_env -> effect -> tannot val t_to_string : t -> string |