summaryrefslogtreecommitdiff
path: root/src/rewriter.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/rewriter.ml')
-rw-r--r--src/rewriter.ml275
1 files changed, 227 insertions, 48 deletions
diff --git a/src/rewriter.ml b/src/rewriter.ml
index edf0d4a5..62870083 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -63,7 +63,6 @@ type 'a rewriters = {
rewrite_defs : 'a rewriters -> 'a defs -> 'a defs;
}
-let effect_of_fpat (FP_aux (_,(_,a))) = effect_of_annot a
let effect_of_lexp (LEXP_aux (_,(_,a))) = effect_of_annot a
let effect_of_fexp (FE_aux (_,(_,a))) = effect_of_annot a
let effect_of_fexps fexps =
@@ -140,7 +139,6 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match destruct_tannot (snd annot)
| Some (env, typ, eff) ->
let effsum = match e with
| E_block es -> union_eff_exps es
- | E_nondet es -> union_eff_exps es
| E_id _ | E_ref _
| E_lit _ -> eff
| E_cast (_,e) -> effect_of e
@@ -151,7 +149,7 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match destruct_tannot (snd annot)
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_loop (_,_,e1,e2) -> union_eff_exps [e1;e2]
| E_vector es -> union_eff_exps es
| E_vector_access (e1,e2) -> union_eff_exps [e1;e2]
| E_vector_subrange (e1,e2,e3) -> union_eff_exps [e1;e2;e3]
@@ -256,9 +254,6 @@ let rewrite_pat rewriters (P_aux (pat,(l,annot)) as orig_pat) =
| P_as(pat,id) -> rewrap (P_as(rewrite pat, id))
| P_typ(typ,pat) -> rewrap (P_typ(typ, rewrite pat))
| P_app(id ,pats) -> rewrap (P_app(id, List.map rewrite pats))
- | P_record(fpats,_) ->
- rewrap (P_record(List.map (fun (FP_aux(FP_Fpat(id,pat),pannot)) -> FP_aux(FP_Fpat(id, rewrite pat), pannot)) fpats,
- false))
| P_vector pats -> rewrap (P_vector(List.map rewrite pats))
| P_vector_concat pats -> rewrap (P_vector_concat (List.map rewrite pats))
| P_tup pats -> rewrap (P_tup (List.map rewrite pats))
@@ -271,7 +266,6 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) =
let rewrite = rewriters.rewrite_exp rewriters 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_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))
@@ -280,8 +274,12 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) =
| 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_loop (loop, m, e1, e2) ->
+ let m = match m with
+ | Measure_aux (Measure_none,_) -> m
+ | Measure_aux (Measure_some exp,l) -> Measure_aux (Measure_some (rewrite exp),l)
+ in
+ rewrap (E_loop (loop, m, rewrite e1, rewrite e2))
| E_vector exps -> rewrap (E_vector (List.map rewrite exps))
| E_vector_access (vec,index) -> rewrap (E_vector_access (rewrite vec,rewrite index))
| E_vector_subrange (vec,i1,i2) ->
@@ -362,8 +360,9 @@ let rewrite_def rewriters d = match d with
| DEF_internal_mutrec fdefs -> DEF_internal_mutrec (List.map (rewriters.rewrite_fun rewriters) fdefs)
| DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters letbind)
| DEF_pragma (pragma, arg, l) -> DEF_pragma (pragma, arg, l)
- | DEF_scattered _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "DEF_scattered survived to rewritter")
+ | DEF_scattered _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "DEF_scattered survived to rewriter")
| DEF_measure (id,pat,exp) -> DEF_measure (id,rewriters.rewrite_pat rewriters pat, rewriters.rewrite_exp rewriters exp)
+ | DEF_loop_measures (id,_) -> raise (Reporting.err_unreachable (id_loc id) __POS__ "DEF_loop_measures survived to rewriter")
let rewrite_defs_base rewriters (Defs defs) =
let rec rewrite ds = match ds with
@@ -439,7 +438,7 @@ let rewrite_defs_base_parallel j rewriters (Defs defs) =
exit 1
done;
Defs (List.concat !rewritten)
-
+
let rewriters_base =
{rewrite_exp = rewrite_exp;
rewrite_pat = rewrite_pat;
@@ -451,7 +450,7 @@ let rewriters_base =
let rewrite_defs (Defs defs) = rewrite_defs_base rewriters_base (Defs defs)
-type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
+type ('a,'pat,'pat_aux) pat_alg =
{ p_lit : lit -> 'pat_aux
; p_wild : 'pat_aux
; p_or : 'pat * 'pat -> 'pat_aux
@@ -461,7 +460,6 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
; p_id : id -> 'pat_aux
; p_var : 'pat * typ_pat -> 'pat_aux
; p_app : id * 'pat list -> 'pat_aux
- ; p_record : 'fpat list * bool -> 'pat_aux
; p_vector : 'pat list -> 'pat_aux
; p_vector_concat : 'pat list -> 'pat_aux
; p_tup : 'pat list -> 'pat_aux
@@ -469,11 +467,9 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
; p_cons : 'pat * 'pat -> 'pat_aux
; p_string_append : 'pat list -> 'pat_aux
; p_aux : 'pat_aux * 'a annot -> 'pat
- ; fP_aux : 'fpat_aux * 'a annot -> 'fpat
- ; fP_Fpat : id * 'pat -> 'fpat_aux
}
-let rec fold_pat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat_aux -> 'pat_aux =
+let rec fold_pat_aux (alg : ('a,'pat,'pat_aux) pat_alg) : 'a pat_aux -> 'pat_aux =
function
| P_lit lit -> alg.p_lit lit
| P_wild -> alg.p_wild
@@ -484,7 +480,6 @@ let rec fold_pat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat
| P_as (p,id) -> alg.p_as (fold_pat alg p, id)
| P_typ (typ,p) -> alg.p_typ (typ,fold_pat alg p)
| P_app (id,ps) -> alg.p_app (id,List.map (fold_pat alg) ps)
- | P_record (ps,b) -> alg.p_record (List.map (fold_fpat alg) ps, b)
| P_vector ps -> alg.p_vector (List.map (fold_pat alg) ps)
| P_vector_concat ps -> alg.p_vector_concat (List.map (fold_pat alg) ps)
| P_tup ps -> alg.p_tup (List.map (fold_pat alg) ps)
@@ -492,18 +487,12 @@ let rec fold_pat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat
| P_cons (ph,pt) -> alg.p_cons (fold_pat alg ph, fold_pat alg pt)
| P_string_append ps -> alg.p_string_append (List.map (fold_pat alg) ps)
-and fold_pat (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat -> 'pat =
+and fold_pat (alg : ('a,'pat,'pat_aux) pat_alg) : 'a pat -> 'pat =
function
| P_aux (pat,annot) -> alg.p_aux (fold_pat_aux alg pat,annot)
-and fold_fpat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a fpat_aux -> 'fpat_aux =
- function
- | FP_Fpat (id,pat) -> alg.fP_Fpat (id,fold_pat alg pat)
-and fold_fpat (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a fpat -> 'fpat =
- function
- | FP_aux (fpat,annot) -> alg.fP_aux (fold_fpat_aux alg fpat,annot)
(* identity fold from term alg to term alg *)
-let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg =
+let id_pat_alg : ('a,'a pat, 'a pat_aux) pat_alg =
{ p_lit = (fun lit -> P_lit lit)
; p_wild = P_wild
; p_or = (fun (pat1, pat2) -> P_or(pat1, pat2))
@@ -513,7 +502,6 @@ let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg =
; p_id = (fun id -> P_id id)
; p_var = (fun (pat,tpat) -> P_var (pat,tpat))
; p_app = (fun (id,ps) -> P_app (id,ps))
- ; p_record = (fun (ps,b) -> P_record (ps,b))
; p_vector = (fun ps -> P_vector ps)
; p_vector_concat = (fun ps -> P_vector_concat ps)
; p_tup = (fun ps -> P_tup ps)
@@ -521,15 +509,12 @@ let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg =
; p_cons = (fun (ph,pt) -> P_cons (ph,pt))
; p_string_append = (fun (ps) -> P_string_append (ps))
; p_aux = (fun (pat,annot) -> P_aux (pat,annot))
- ; fP_aux = (fun (fpat,annot) -> FP_aux (fpat,annot))
- ; fP_Fpat = (fun (id,pat) -> FP_Fpat (id,pat))
}
type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
- 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg =
+ 'pat,'pat_aux) exp_alg =
{ e_block : 'exp list -> 'exp_aux
- ; e_nondet : 'exp list -> 'exp_aux
; e_id : id -> 'exp_aux
; e_ref : id -> 'exp_aux
; e_lit : lit -> 'exp_aux
@@ -539,7 +524,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_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_loop : loop * ('exp option * Parse_ast.l) * 'exp * 'exp -> 'exp_aux
; e_vector : 'exp list -> 'exp_aux
; e_vector_access : 'exp * 'exp -> 'exp_aux
; e_vector_subrange : 'exp * 'exp * 'exp -> 'exp_aux
@@ -586,12 +571,11 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
; pat_aux : 'pexp_aux * 'a annot -> 'pexp
; lB_val : 'pat * 'exp -> 'letbind_aux
; lB_aux : 'letbind_aux * 'a annot -> 'letbind
- ; pat_alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg
+ ; pat_alg : ('a,'pat,'pat_aux) pat_alg
}
let rec fold_exp_aux alg = function
| E_block es -> alg.e_block (List.map (fold_exp alg) es)
- | E_nondet es -> alg.e_nondet (List.map (fold_exp alg) es)
| E_id id -> alg.e_id id
| E_ref id -> alg.e_ref id
| E_lit lit -> alg.e_lit lit
@@ -602,8 +586,12 @@ 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_loop (loop_type, m, e1, e2) ->
+ let m = match m with
+ | Measure_aux (Measure_none,l) -> None,l
+ | Measure_aux (Measure_some exp,l) -> Some (fold_exp alg exp),l
+ in
+ alg.e_loop (loop_type, m, fold_exp alg e1, fold_exp alg e2)
| E_vector es -> alg.e_vector (List.map (fold_exp alg) es)
| E_vector_access (e1,e2) -> alg.e_vector_access (fold_exp alg e1, fold_exp alg e2)
| E_vector_subrange (e1,e2,e3) ->
@@ -671,7 +659,6 @@ let fold_function alg (FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, fun
let id_exp_alg =
{ e_block = (fun es -> E_block es)
- ; e_nondet = (fun es -> E_nondet es)
; e_id = (fun id -> E_id id)
; e_ref = (fun id -> E_ref id)
; e_lit = (fun lit -> (E_lit lit))
@@ -681,7 +668,9 @@ 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_loop = (fun (lt, (m,l), e1, e2) ->
+ let m = match m with None -> Measure_none | Some e -> Measure_some e in
+ E_loop (lt, Measure_aux (m,l), e1, e2))
; e_vector = (fun es -> E_vector es)
; e_vector_access = (fun (e1,e2) -> E_vector_access (e1,e2))
; e_vector_subrange = (fun (e1,e2,e3) -> E_vector_subrange (e1,e2,e3))
@@ -749,7 +738,6 @@ let compute_pat_alg bot join =
; p_id = (fun id -> (bot, P_id id))
; p_var = (fun ((v,pat),kid) -> (v, P_var (pat,kid)))
; p_app = (fun (id,ps) -> split_join (fun ps -> P_app (id,ps)) ps)
- ; p_record = (fun (ps,b) -> split_join (fun ps -> P_record (ps,b)) ps)
; p_vector = split_join (fun ps -> P_vector ps)
; p_vector_concat = split_join (fun ps -> P_vector_concat ps)
; p_tup = split_join (fun ps -> P_tup ps)
@@ -757,15 +745,12 @@ let compute_pat_alg bot join =
; p_cons = (fun ((vh,ph),(vt,pt)) -> (join vh vt, P_cons (ph,pt)))
; p_string_append = split_join (fun ps -> P_string_append ps)
; p_aux = (fun ((v,pat),annot) -> (v, P_aux (pat,annot)))
- ; fP_aux = (fun ((v,fpat),annot) -> (v, FP_aux (fpat,annot)))
- ; fP_Fpat = (fun (id,(v,pat)) -> (v, FP_Fpat (id,pat)))
}
let compute_exp_alg bot join =
let join_list vs = List.fold_left join bot vs in
let split_join f es = let (vs,es) = List.split es in (join_list vs, f es) in
{ e_block = split_join (fun es -> E_block es)
- ; e_nondet = split_join (fun es -> E_nondet es)
; e_id = (fun id -> (bot, E_id id))
; e_ref = (fun id -> (bot, E_ref id))
; e_lit = (fun lit -> (bot, E_lit lit))
@@ -776,8 +761,12 @@ 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_loop = (fun (lt, (m,l), (v1, e1), (v2, e2)) ->
+ let vs,m = match m with
+ | None -> [], Measure_none
+ | Some (v,e) -> [v], Measure_some e
+ in
+ (join_list (vs@[v1;v2]), E_loop (lt, Measure_aux (m,l), e1, e2)))
; e_vector = split_join (fun es -> E_vector es)
; e_vector_access = (fun ((v1,e1),(v2,e2)) -> (join v1 v2, E_vector_access (e1,e2)))
; e_vector_subrange = (fun ((v1,e1),(v2,e2),(v3,e3)) -> (join_list [v1;v2;v3], E_vector_subrange (e1,e2,e3)))
@@ -853,7 +842,6 @@ let pure_pat_alg bot join =
; p_id = (fun id -> bot)
; p_var = (fun (v,kid) -> v)
; p_app = (fun (id,ps) -> join_list ps)
- ; p_record = (fun (ps,b) -> join_list ps)
; p_vector = join_list
; p_vector_concat = join_list
; p_tup = join_list
@@ -861,14 +849,11 @@ let pure_pat_alg bot join =
; p_string_append = join_list
; p_cons = (fun (vh,vt) -> join vh vt)
; p_aux = (fun (v,annot) -> v)
- ; fP_aux = (fun (v,annot) -> v)
- ; fP_Fpat = (fun (id,v) -> v)
}
let pure_exp_alg bot join =
let join_list vs = List.fold_left join bot vs in
{ e_block = join_list
- ; e_nondet = join_list
; e_id = (fun id -> bot)
; e_ref = (fun id -> bot)
; e_lit = (fun lit -> bot)
@@ -878,7 +863,8 @@ let pure_exp_alg bot join =
; e_tuple = join_list
; e_if = (fun (v1,v2,v3) -> join_list [v1;v2;v3])
; e_for = (fun (id,v1,v2,v3,order,v4) -> join_list [v1;v2;v3;v4])
- ; e_loop = (fun (lt, v1, v2) -> join v1 v2)
+ ; e_loop = (fun (lt, (m,_), v1, v2) ->
+ let v = join v1 v2 in match m with None -> v | Some v' -> join v v')
; e_vector = join_list
; e_vector_access = (fun (v1,v2) -> join v1 v2)
; e_vector_subrange = (fun (v1,v2,v3) -> join_list [v1;v2;v3])
@@ -927,3 +913,196 @@ let pure_exp_alg bot join =
; lB_aux = (fun (vl,annot) -> vl)
; pat_alg = pure_pat_alg bot join
}
+
+let default_fold_fexp f x (FE_aux (FE_Fexp (id,e),annot)) =
+ let x,e = f x e in
+ x, FE_aux (FE_Fexp (id,e),annot)
+
+let default_fold_pexp f x (Pat_aux (pe,ann)) =
+ let x,pe = match pe with
+ | Pat_exp (p,e) ->
+ let x,e = f x e in
+ x,Pat_exp (p,e)
+ | Pat_when (p,e1,e2) ->
+ let x,e1 = f x e1 in
+ let x,e2 = f x e2 in
+ x,Pat_when (p,e1,e2)
+ in x, Pat_aux (pe,ann)
+
+let default_fold_letbind f x (LB_aux (LB_val (p,e),ann)) =
+ let x,e = f x e in
+ x, LB_aux (LB_val (p,e),ann)
+
+let rec default_fold_lexp f x (LEXP_aux (le,ann) as lexp) =
+ let re le = LEXP_aux (le,ann) in
+ match le with
+ | LEXP_id _
+ | LEXP_cast _
+ -> x, lexp
+ | LEXP_deref e ->
+ let x, e = f x e in
+ x, re (LEXP_deref e)
+ | LEXP_memory (id,es) ->
+ let x,es = List.fold_left (fun (x,es) e ->
+ let x,e' = f x e in x,e'::es) (x,[]) es in
+ x, re (LEXP_memory (id, List.rev es))
+ | LEXP_tup les ->
+ let x,les = List.fold_left (fun (x,les) le ->
+ let x,le' = default_fold_lexp f x le in x,le'::les) (x,[]) les in
+ x, re (LEXP_tup (List.rev les))
+ | LEXP_vector_concat les ->
+ let x,les = List.fold_left (fun (x,les) le ->
+ let x,le' = default_fold_lexp f x le in x,le'::les) (x,[]) les in
+ x, re (LEXP_vector_concat (List.rev les))
+ | LEXP_vector (le,e) ->
+ let x, le = default_fold_lexp f x le in
+ let x, e = f x e in
+ x, re (LEXP_vector (le,e))
+ | LEXP_vector_range (le,e1,e2) ->
+ let x, le = default_fold_lexp f x le in
+ let x, e1 = f x e1 in
+ let x, e2 = f x e2 in
+ x, re (LEXP_vector_range (le,e1,e2))
+ | LEXP_field (le,id) ->
+ let x, le = default_fold_lexp f x le in
+ x, re (LEXP_field (le,id))
+
+let default_fold_exp f x (E_aux (e,ann) as exp) =
+ let re e = E_aux (e,ann) in
+ match e with
+ | E_block es ->
+ let x,es = List.fold_left (fun (x,es) e ->
+ let x,e' = f x e in x,e'::es) (x,[]) es in
+ x, re (E_block (List.rev es))
+ | E_id _
+ | E_ref _
+ | E_lit _ -> x, exp
+ | E_cast (typ,e) ->
+ let x,e = f x e in
+ x, re (E_cast (typ,e))
+ | E_app (id,es) ->
+ let x,es = List.fold_left (fun (x,es) e ->
+ let x,e' = f x e in x,e'::es) (x,[]) es in
+ x, re (E_app (id, List.rev es))
+ | E_app_infix (e1,id,e2) ->
+ let x,e1 = f x e1 in
+ let x,e2 = f x e2 in
+ x, re (E_app_infix (e1,id,e2))
+ | E_tuple es ->
+ let x,es = List.fold_left (fun (x,es) e ->
+ let x,e' = f x e in x,e'::es) (x,[]) es in
+ x, re (E_tuple (List.rev es))
+ | E_if (e1,e2,e3) ->
+ let x,e1 = f x e1 in
+ let x,e2 = f x e2 in
+ let x,e3 = f x e3 in
+ x, re (E_if (e1,e2,e3))
+ | E_for (id,e1,e2,e3,order,e4) ->
+ let x,e1 = f x e1 in
+ let x,e2 = f x e2 in
+ let x,e3 = f x e3 in
+ let x,e4 = f x e4 in
+ x, re (E_for (id,e1,e2,e3,order,e4))
+ | E_loop (loop_type, m, e1, e2) ->
+ let x,m = match m with
+ | Measure_aux (Measure_none,_) -> x,m
+ | Measure_aux (Measure_some exp,l) ->
+ let x, exp = f x exp in
+ x, Measure_aux (Measure_some exp,l)
+ in
+ let x,e1 = f x e1 in
+ let x,e2 = f x e2 in
+ x, re (E_loop (loop_type, m, e1, e2))
+ | E_vector es ->
+ let x,es = List.fold_left (fun (x,es) e ->
+ let x,e' = f x e in x,e'::es) (x,[]) es in
+ x, re (E_vector (List.rev es))
+ | E_vector_access (e1,e2) ->
+ let x,e1 = f x e1 in
+ let x,e2 = f x e2 in
+ x, re (E_vector_access (e1,e2))
+ | E_vector_subrange (e1,e2,e3) ->
+ let x,e1 = f x e1 in
+ let x,e2 = f x e2 in
+ let x,e3 = f x e3 in
+ x, re (E_vector_subrange (e1,e2,e3))
+ | E_vector_update (e1,e2,e3) ->
+ let x,e1 = f x e1 in
+ let x,e2 = f x e2 in
+ let x,e3 = f x e3 in
+ x, re (E_vector_update (e1,e2,e3))
+ | E_vector_update_subrange (e1,e2,e3,e4) ->
+ let x,e1 = f x e1 in
+ let x,e2 = f x e2 in
+ let x,e3 = f x e3 in
+ let x,e4 = f x e4 in
+ x, re (E_vector_update_subrange (e1,e2,e3,e4))
+ | E_vector_append (e1,e2) ->
+ let x,e1 = f x e1 in
+ let x,e2 = f x e2 in
+ x, re (E_vector_append (e1,e2))
+ | E_list es ->
+ let x,es = List.fold_left (fun (x,es) e ->
+ let x,e' = f x e in x,e'::es) (x,[]) es in
+ x, re (E_list (List.rev es))
+ | E_cons (e1,e2) ->
+ let x,e1 = f x e1 in
+ let x,e2 = f x e2 in
+ x, re (E_cons (e1,e2))
+ | E_record fexps ->
+ let x,fexps = List.fold_left (fun (x,fes) fe ->
+ let x,fe' = default_fold_fexp f x fe in x,fe'::fes) (x,[]) fexps in
+ x, re (E_record (List.rev fexps))
+ | E_record_update (e,fexps) ->
+ let x,e = f x e in
+ let x,fexps = List.fold_left (fun (x,fes) fe ->
+ let x,fe' = default_fold_fexp f x fe in x,fe'::fes) (x,[]) fexps in
+ x, re (E_record_update (e, List.rev fexps))
+ | E_field (e,id) ->
+ let x,e = f x e in x, re (E_field (e,id))
+ | E_case (e,pexps) ->
+ let x,e = f x e in
+ let x,pexps = List.fold_left (fun (x,pes) pe ->
+ let x,pe' = default_fold_pexp f x pe in x,pe'::pes) (x,[]) pexps in
+ x, re (E_case (e, List.rev pexps))
+ | E_try (e,pexps) ->
+ let x,e = f x e in
+ let x,pexps = List.fold_left (fun (x,pes) pe ->
+ let x,pe' = default_fold_pexp f x pe in x,pe'::pes) (x,[]) pexps in
+ x, re (E_try (e, List.rev pexps))
+ | E_let (letbind,e) ->
+ let x,letbind = default_fold_letbind f x letbind in
+ let x,e = f x e in
+ x, re (E_let (letbind,e))
+ | E_assign (lexp,e) ->
+ let x,lexp = default_fold_lexp f x lexp in
+ let x,e = f x e in
+ x, re (E_assign (lexp,e))
+ | E_sizeof _
+ | E_constraint _
+ -> x,exp
+ | E_exit e ->
+ let x,e = f x e in x, re (E_exit e)
+ | E_throw e ->
+ let x,e = f x e in x, re (E_throw e)
+ | E_return e ->
+ let x,e = f x e in x, re (E_return e)
+ | E_assert(e1,e2) ->
+ let x,e1 = f x e1 in
+ let x,e2 = f x e2 in
+ x, re (E_assert (e1,e2))
+ | E_var (lexp,e1,e2) ->
+ let x,lexp = default_fold_lexp f x lexp in
+ let x,e1 = f x e1 in
+ let x,e2 = f x e2 in
+ x, re (E_var (lexp,e1,e2))
+ | E_internal_plet (pat,e1,e2) ->
+ let x,e1 = f x e1 in
+ let x,e2 = f x e2 in
+ x, re (E_internal_plet (pat,e1,e2))
+ | E_internal_return e ->
+ let x,e = f x e in x, re (E_internal_return e)
+ | E_internal_value _ -> x,exp
+
+let rec foldin_exp f x e = f (default_fold_exp (foldin_exp f)) x e
+let rec foldin_pexp f x e = default_fold_pexp (foldin_exp f) x e
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 12:21:43 +0000