diff options
Diffstat (limited to 'src/rewriter.ml')
| -rw-r--r-- | src/rewriter.ml | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/src/rewriter.ml b/src/rewriter.ml index 6d7b29c7..c2b8e618 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -130,6 +130,7 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with union_effects (fun_app_effects f env) (union_eff_exps [e1;e2]) | E_if (e1,e2,e3) -> union_eff_exps [e1;e2;e3] | E_for (_,e1,e2,e3,_,e4) -> union_eff_exps [e1;e2;e3;e4] + | E_loop (_,e1,e2) -> union_eff_exps [e1;e2] | E_vector es -> union_eff_exps es | E_vector_indexed (ies,opt_default) -> let (_,es) = List.split ies in @@ -388,6 +389,8 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot))) = | 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_loop (loop, e1, e2) -> + rewrap (E_loop (loop, rewrite e1, rewrite e2)) | E_vector exps -> rewrap (E_vector (List.map rewrite exps)) | E_vector_indexed (exps,(Def_val_aux(default,dannot))) -> let def = match default with @@ -698,6 +701,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; e_tuple : 'exp list -> 'exp_aux ; e_if : 'exp * 'exp * 'exp -> 'exp_aux ; e_for : id * 'exp * 'exp * 'exp * Ast.order * 'exp -> 'exp_aux + ; e_loop : loop * 'exp * 'exp -> 'exp_aux ; e_vector : 'exp list -> 'exp_aux ; e_vector_indexed : (int * 'exp) list * 'opt_default -> 'exp_aux ; e_vector_access : 'exp * 'exp -> 'exp_aux @@ -763,6 +767,8 @@ let rec fold_exp_aux alg = function | E_if (e1,e2,e3) -> alg.e_if (fold_exp alg e1, fold_exp alg e2, fold_exp alg e3) | E_for (id,e1,e2,e3,order,e4) -> alg.e_for (id,fold_exp alg e1, fold_exp alg e2, fold_exp alg e3, order, fold_exp alg e4) + | E_loop (loop_type, e1, e2) -> + alg.e_loop (loop_type, fold_exp alg e1, fold_exp alg e2) | E_vector es -> alg.e_vector (List.map (fold_exp alg) es) | E_vector_indexed (es,opt) -> alg.e_vector_indexed (List.map (fun (id,e) -> (id,fold_exp alg e)) es, fold_opt_default alg opt) @@ -840,6 +846,7 @@ let id_exp_alg = ; e_tuple = (fun es -> E_tuple es) ; e_if = (fun (e1,e2,e3) -> E_if (e1,e2,e3)) ; e_for = (fun (id,e1,e2,e3,order,e4) -> E_for (id,e1,e2,e3,order,e4)) + ; e_loop = (fun (lt, e1, e2) -> E_loop (lt, e1, e2)) ; e_vector = (fun es -> E_vector es) ; e_vector_indexed = (fun (es,opt2) -> E_vector_indexed (es,opt2)) ; e_vector_access = (fun (e1,e2) -> E_vector_access (e1,e2)) @@ -937,6 +944,8 @@ let compute_exp_alg bot join = ; e_if = (fun ((v1,e1),(v2,e2),(v3,e3)) -> (join_list [v1;v2;v3], E_if (e1,e2,e3))) ; e_for = (fun (id,(v1,e1),(v2,e2),(v3,e3),order,(v4,e4)) -> (join_list [v1;v2;v3;v4], E_for (id,e1,e2,e3,order,e4))) + ; e_loop = (fun (lt, (v1, e1), (v2, e2)) -> + (join_list [v1;v2], E_loop (lt, e1, e2))) ; e_vector = split_join (fun es -> E_vector es) ; e_vector_indexed = (fun (es,(v2,opt2)) -> let (is,es) = List.split es in @@ -1177,6 +1186,7 @@ let rewrite_sizeof (Defs defs) = ; e_tuple = (fun es -> let (es, es') = List.split es in (E_tuple es, E_tuple es')) ; e_if = (fun ((e1,e1'),(e2,e2'),(e3,e3')) -> (E_if (e1,e2,e3), E_if (e1',e2',e3'))) ; e_for = (fun (id,(e1,e1'),(e2,e2'),(e3,e3'),order,(e4,e4')) -> (E_for (id,e1,e2,e3,order,e4), E_for (id,e1',e2',e3',order,e4'))) + ; e_loop = (fun (lt, (e1, e1'), (e2, e2')) -> (E_loop (lt, e1, e2), E_loop (lt, e1', e2'))) ; e_vector = (fun es -> let (es, es') = List.split es in (E_vector es, E_vector es')) ; e_vector_indexed = (fun (es,(opt2,opt2')) -> let (is, es) = List.split es in let (es, es') = List.split es in let (es, es') = (List.combine is es, List.combine is es') in (E_vector_indexed (es,opt2), E_vector_indexed (es',opt2'))) ; e_vector_access = (fun ((e1,e1'),(e2,e2')) -> (E_vector_access (e1,e2), E_vector_access (e1',e2'))) @@ -2840,6 +2850,10 @@ let rewrite_defs_letbind_effects = n_exp_name by (fun by -> let body = n_exp_term (effectful body) body in k (rewrap (E_for (id,start,stop,by,dir,body)))))) + | E_loop (loop, cond, body) -> + let cond = n_exp_term (effectful cond) cond in + let body = n_exp_term (effectful body) body in + k (rewrap (E_loop (loop,cond,body))) | E_vector exps -> n_exp_nameL exps (fun exps -> k (rewrap (E_vector exps))) @@ -3164,6 +3178,29 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = else P_aux (P_tup [pat; mktup_pat pl vars], simple_annot pl (typ_of v)) in Added_vars (v,pat) + | E_loop(loop,cond,body) -> + let vars = List.map (fun (var,(l,t)) -> E_aux (E_id var,(l,t))) (find_updated_vars body) in + let vartuple = mktup el vars in + (* let cond = rewrite_var_updates (add_vars false cond vartuple) in *) + let body = rewrite_var_updates (add_vars overwrite body vartuple) in + let (E_aux (_,(_,bannot))) = body in + let fname = match effectful cond, effectful body with + | false, false -> "while_PP" + | false, true -> "while_PM" + | true, false -> "while_MP" + | true, true -> "while_MM" in + let funcl = Id_aux (Id fname,Parse_ast.Generated el) in + let is_while = + match loop with + | While -> E_aux (E_lit (mk_lit L_true), simple_annot el bool_typ) + | Until -> E_aux (E_lit (mk_lit L_false), simple_annot el bool_typ) in + let v = E_aux (E_app (funcl,[is_while;cond;body;vartuple]), + (Parse_ast.Generated el, bannot)) in + let pat = + if overwrite then mktup_pat el vars + else P_aux (P_tup [pat; mktup_pat pl vars], + simple_annot pl (typ_of v)) in + Added_vars (v,pat) | E_if (c,e1,e2) -> let vars = List.map (fun (var,(l,t)) -> E_aux (E_id var,(l,t))) (dedup eqidtyp (find_updated_vars e1 @ find_updated_vars e2)) in |