diff options
Diffstat (limited to 'src/rewriter.ml')
| -rw-r--r-- | src/rewriter.ml | 260 |
1 files changed, 131 insertions, 129 deletions
diff --git a/src/rewriter.ml b/src/rewriter.ml index d957ee6c..d9e3925b 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -90,6 +90,7 @@ let fix_effsum_exp (E_aux (e,(l,annot))) = | 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_comment _ | E_comment_struc _ -> pure_e | E_internal_cast (_,e) -> get_effsum_exp e | E_internal_exp _ -> pure_e | E_internal_exp_user _ -> pure_e @@ -278,139 +279,140 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) = let rewrap e = E_aux (e,(l,annot)) in let rewrite = rewriters.rewrite_exp rewriters nmap in match exp with - | E_block exps -> rewrap (E_block (List.map rewrite exps)) - | E_nondet exps -> rewrap (E_nondet (List.map rewrite exps)) - | E_lit (L_aux ((L_hex _ | L_bin _) as lit,_)) -> - let es = List.map (fun p -> E_aux (E_lit p ,(Parse_ast.Generated l,simple_annot {t = Tid "bit"}))) - (vector_string_to_bit_list l lit) in - rewrap (E_vector es) - | E_id _ | E_lit _ -> rewrap exp - | E_cast (typ, exp) -> rewrap (E_cast (typ, rewrite exp)) - | E_app (id,exps) -> rewrap (E_app (id,List.map rewrite exps)) - | E_app_infix(el,id,er) -> rewrap (E_app_infix(rewrite el,id,rewrite er)) - | E_tuple exps -> rewrap (E_tuple (List.map rewrite exps)) - | E_if (c,t,e) -> rewrap (E_if (rewrite c,rewrite t, rewrite e)) - | E_for (id, e1, e2, e3, o, body) -> - rewrap (E_for (id, rewrite e1, rewrite e2, rewrite e3, o, rewrite body)) - | E_vector exps -> rewrap (E_vector (List.map rewrite exps)) - | E_vector_indexed (exps,(Def_val_aux(default,dannot))) -> - let def = match default with - | Def_val_empty -> default - | Def_val_dec e -> Def_val_dec (rewrite e) in - rewrap (E_vector_indexed (List.map (fun (i,e) -> (i, rewrite e)) exps, Def_val_aux(def,dannot))) - | E_vector_access (vec,index) -> rewrap (E_vector_access (rewrite vec,rewrite index)) - | E_vector_subrange (vec,i1,i2) -> - rewrap (E_vector_subrange (rewrite vec,rewrite i1,rewrite i2)) - | E_vector_update (vec,index,new_v) -> - rewrap (E_vector_update (rewrite vec,rewrite index,rewrite new_v)) - | E_vector_update_subrange (vec,i1,i2,new_v) -> - rewrap (E_vector_update_subrange (rewrite vec,rewrite i1,rewrite i2,rewrite new_v)) - | E_vector_append (v1,v2) -> rewrap (E_vector_append (rewrite v1,rewrite v2)) - | E_list exps -> rewrap (E_list (List.map rewrite exps)) - | E_cons(h,t) -> rewrap (E_cons (rewrite h,rewrite t)) - | E_record (FES_aux (FES_Fexps(fexps, bool),fannot)) -> - rewrap (E_record - (FES_aux (FES_Fexps - (List.map (fun (FE_aux(FE_Fexp(id,e),fannot)) -> - FE_aux(FE_Fexp(id,rewrite e),fannot)) fexps, bool), fannot))) - | E_record_update (re,(FES_aux (FES_Fexps(fexps, bool),fannot))) -> - rewrap (E_record_update ((rewrite re), - (FES_aux (FES_Fexps - (List.map (fun (FE_aux(FE_Fexp(id,e),fannot)) -> - FE_aux(FE_Fexp(id,rewrite e),fannot)) fexps, bool), fannot)))) - | E_field(exp,id) -> rewrap (E_field(rewrite exp,id)) - | E_case (exp ,pexps) -> - rewrap (E_case (rewrite exp, - (List.map - (fun (Pat_aux (Pat_exp(p,e),pannot)) -> - Pat_aux (Pat_exp(rewriters.rewrite_pat rewriters nmap p,rewrite e),pannot)) pexps))) - | E_let (letbind,body) -> rewrap (E_let(rewriters.rewrite_let rewriters nmap letbind,rewrite body)) - | E_assign (lexp,exp) -> rewrap (E_assign(rewriters.rewrite_lexp rewriters nmap lexp,rewrite exp)) - | E_exit e -> rewrap (E_exit (rewrite e)) - | E_assert(e1,e2) -> rewrap (E_assert(rewrite e1,rewrite e2)) - | E_internal_cast ((l,casted_annot),exp) -> - let new_exp = rewrite 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 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" + | E_comment _ | E_comment_struc _ -> rewrap exp + | E_block exps -> rewrap (E_block (List.map rewrite exps)) + | E_nondet exps -> rewrap (E_nondet (List.map rewrite exps)) + | E_lit (L_aux ((L_hex _ | L_bin _) as lit,_)) -> + let es = List.map (fun p -> E_aux (E_lit p ,(Parse_ast.Generated l,simple_annot {t = Tid "bit"}))) + (vector_string_to_bit_list l lit) in + rewrap (E_vector es) + | E_id _ | E_lit _ -> rewrap exp + | E_cast (typ, exp) -> rewrap (E_cast (typ, rewrite exp)) + | E_app (id,exps) -> rewrap (E_app (id,List.map rewrite exps)) + | E_app_infix(el,id,er) -> rewrap (E_app_infix(rewrite el,id,rewrite er)) + | E_tuple exps -> rewrap (E_tuple (List.map rewrite exps)) + | E_if (c,t,e) -> rewrap (E_if (rewrite c,rewrite t, rewrite e)) + | E_for (id, e1, e2, e3, o, body) -> + rewrap (E_for (id, rewrite e1, rewrite e2, rewrite e3, o, rewrite body)) + | E_vector exps -> rewrap (E_vector (List.map rewrite exps)) + | E_vector_indexed (exps,(Def_val_aux(default,dannot))) -> + let def = match default with + | Def_val_empty -> default + | Def_val_dec e -> Def_val_dec (rewrite e) in + rewrap (E_vector_indexed (List.map (fun (i,e) -> (i, rewrite e)) exps, Def_val_aux(def,dannot))) + | E_vector_access (vec,index) -> rewrap (E_vector_access (rewrite vec,rewrite index)) + | E_vector_subrange (vec,i1,i2) -> + rewrap (E_vector_subrange (rewrite vec,rewrite i1,rewrite i2)) + | E_vector_update (vec,index,new_v) -> + rewrap (E_vector_update (rewrite vec,rewrite index,rewrite new_v)) + | E_vector_update_subrange (vec,i1,i2,new_v) -> + rewrap (E_vector_update_subrange (rewrite vec,rewrite i1,rewrite i2,rewrite new_v)) + | E_vector_append (v1,v2) -> rewrap (E_vector_append (rewrite v1,rewrite v2)) + | E_list exps -> rewrap (E_list (List.map rewrite exps)) + | E_cons(h,t) -> rewrap (E_cons (rewrite h,rewrite t)) + | E_record (FES_aux (FES_Fexps(fexps, bool),fannot)) -> + rewrap (E_record + (FES_aux (FES_Fexps + (List.map (fun (FE_aux(FE_Fexp(id,e),fannot)) -> + FE_aux(FE_Fexp(id,rewrite e),fannot)) fexps, bool), fannot))) + | E_record_update (re,(FES_aux (FES_Fexps(fexps, bool),fannot))) -> + rewrap (E_record_update ((rewrite re), + (FES_aux (FES_Fexps + (List.map (fun (FE_aux(FE_Fexp(id,e),fannot)) -> + FE_aux(FE_Fexp(id,rewrite e),fannot)) fexps, bool), fannot)))) + | E_field(exp,id) -> rewrap (E_field(rewrite exp,id)) + | E_case (exp ,pexps) -> + rewrap (E_case (rewrite exp, + (List.map + (fun (Pat_aux (Pat_exp(p,e),pannot)) -> + Pat_aux (Pat_exp(rewriters.rewrite_pat rewriters nmap p,rewrite e),pannot)) pexps))) + | E_let (letbind,body) -> rewrap (E_let(rewriters.rewrite_let rewriters nmap letbind,rewrite body)) + | E_assign (lexp,exp) -> rewrap (E_assign(rewriters.rewrite_lexp rewriters nmap lexp,rewrite exp)) + | E_exit e -> rewrap (E_exit (rewrite e)) + | E_assert(e1,e2) -> rewrap (E_assert(rewrite e1,rewrite e2)) + | E_internal_cast ((l,casted_annot),exp) -> + let new_exp = rewrite 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 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*) - rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"),Parse_ast.Generated l)), - Parse_ast.Generated l),new_exp)) - | _ -> new_exp)) - | _ -> new_exp) - | Base((_,t),_,_,_,_,_),_ -> - (*let _ = Printf.eprintf "Considering removing an internal cast where the remaining type is %s\n%!" + rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"),Parse_ast.Generated l)), + Parse_ast.Generated l),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" + (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 - rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"), Parse_ast.Generated l)), - Parse_ast.Generated l), 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) -> - 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, 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;_;_])}]) - | Tapp("vector", [_;TA_nexp r;_;_]) -> - (*let _ = Printf.eprintf "vector case with %s, bounds are %s\n" + rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"), Parse_ast.Generated l)), + Parse_ast.Generated l), 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) -> + 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, 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;_;_])}]) + | Tapp("vector", [_;TA_nexp r;_;_]) -> + (*let _ = Printf.eprintf "vector case with %s, bounds are %s\n" (n_to_string r) (bounds_to_string bounds) in*) - let nexps = expand_nexp r in - (match (match_to_program_vars nexps bounds) with - | [] -> rewrite_nexp_to_exp None l r - | map -> rewrite_nexp_to_exp (Some map) l r) - | Tapp("implicit", [TA_nexp i]) -> - (*let _ = Printf.eprintf "Implicit case with %s\n" (n_to_string i) in*) - let nexps = expand_nexp i in - (match (match_to_program_vars nexps bounds) with - | [] -> rewrite_nexp_to_exp None l i - | map -> rewrite_nexp_to_exp (Some map) l i) - | _ -> - raise (Reporting_basic.err_unreachable l - ("Internal_exp given unexpected types " ^ (t_to_string t)))) - | _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp given none Base annot"))) - | E_internal_exp_user ((l,user_spec),(_,impl)) -> - (match (user_spec,impl) with - | (Base((_,tu),_,_,_,_,_), Base((_,ti),_,_,_,_,bounds)) -> - (*let _ = Printf.eprintf "E_interal_user getting rewritten two types are %s and %s\n" + let nexps = expand_nexp r in + (match (match_to_program_vars nexps bounds) with + | [] -> rewrite_nexp_to_exp None l r + | map -> rewrite_nexp_to_exp (Some map) l r) + | Tapp("implicit", [TA_nexp i]) -> + (*let _ = Printf.eprintf "Implicit case with %s\n" (n_to_string i) in*) + let nexps = expand_nexp i in + (match (match_to_program_vars nexps bounds) with + | [] -> rewrite_nexp_to_exp None l i + | map -> rewrite_nexp_to_exp (Some map) l i) + | _ -> + raise (Reporting_basic.err_unreachable l + ("Internal_exp given unexpected types " ^ (t_to_string t)))) + | _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp given none Base annot"))) + | E_internal_exp_user ((l,user_spec),(_,impl)) -> + (match (user_spec,impl) with + | (Base((_,tu),_,_,_,_,_), Base((_,ti),_,_,_,_,bounds)) -> + (*let _ = Printf.eprintf "E_interal_user getting rewritten two types are %s and %s\n" (t_to_string tu) (t_to_string ti) in*) - let bounds = match nmap with | None -> bounds | Some (nm,_) -> add_map_to_bounds nm bounds in - (match (tu.t,ti.t) with - | (Tapp("implicit", [TA_nexp u]),Tapp("implicit",[TA_nexp i])) -> - (*let _ = Printf.eprintf "Implicit case with %s\n" (n_to_string i) in*) - let nexps = expand_nexp i in - (match (match_to_program_vars nexps bounds) with - | [] -> rewrite_nexp_to_exp None l i - (*add u to program_vars env; for now it will work out properly by accident*) - | map -> rewrite_nexp_to_exp (Some map) l i) - | _ -> - raise (Reporting_basic.err_unreachable l - ("Internal_exp_user given unexpected types " ^ (t_to_string tu) ^ ", " ^ (t_to_string ti)))) - | _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp_user given none Base annot"))) - | E_internal_let _ -> raise (Reporting_basic.err_unreachable l "Internal let found before it should have been introduced") - | E_internal_return _ -> raise (Reporting_basic.err_unreachable l "Internal return found before it should have been introduced") - | E_internal_plet _ -> raise (Reporting_basic.err_unreachable l " Internal plet found before it should have been introduced") - + let bounds = match nmap with | None -> bounds | Some (nm,_) -> add_map_to_bounds nm bounds in + (match (tu.t,ti.t) with + | (Tapp("implicit", [TA_nexp u]),Tapp("implicit",[TA_nexp i])) -> + (*let _ = Printf.eprintf "Implicit case with %s\n" (n_to_string i) in*) + let nexps = expand_nexp i in + (match (match_to_program_vars nexps bounds) with + | [] -> rewrite_nexp_to_exp None l i + (*add u to program_vars env; for now it will work out properly by accident*) + | map -> rewrite_nexp_to_exp (Some map) l i) + | _ -> + raise (Reporting_basic.err_unreachable l + ("Internal_exp_user given unexpected types " ^ (t_to_string tu) ^ ", " ^ (t_to_string ti)))) + | _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp_user given none Base annot"))) + | E_internal_let _ -> raise (Reporting_basic.err_unreachable l "Internal let found before it should have been introduced") + | E_internal_return _ -> raise (Reporting_basic.err_unreachable l "Internal return found before it should have been introduced") + | E_internal_plet _ -> raise (Reporting_basic.err_unreachable l " Internal plet found before it should have been introduced") + let rewrite_let rewriters map (LB_aux(letbind,(l,annot))) = let local_map = get_map_tannot annot in let map = @@ -457,7 +459,7 @@ let rewrite_fun rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,fdannot)) let rewrite_def rewriters d = match d with - | DEF_type _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ -> d + | DEF_type _ | DEF_kind _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ | DEF_comm _ -> d | DEF_fundef fdef -> DEF_fundef (rewriters.rewrite_fun rewriters fdef) | DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters None letbind) | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "DEF_scattered survived to rewritter") |