diff options
| author | Alasdair | 2018-12-13 01:30:41 +0000 |
|---|---|---|
| committer | Alasdair | 2018-12-13 01:30:41 +0000 |
| commit | 49f6fbde33a76424388c28543b3dc1d49867a525 (patch) | |
| tree | e678ead62197e64399471197552e1022769b8de2 /src/rewriter.ml | |
| parent | b9a051d186593fdd3bbf295e20f7ace78e668580 (diff) | |
| parent | f8d88d4cf2439f4920fa948b054c4f0b2899e368 (diff) | |
Merge remote-tracking branch 'origin/sail2' into asl_flow
Diffstat (limited to 'src/rewriter.ml')
| -rw-r--r-- | src/rewriter.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/rewriter.ml b/src/rewriter.ml index 200121c0..a70f6fab 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -346,7 +346,14 @@ let rewrite_lexp rewriters (LEXP_aux(lexp,(l,annot))) = let rewrite_fun rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot))) = let rewrite_funcl (FCL_aux (FCL_Funcl(id,pexp),(l,annot))) = (FCL_aux (FCL_Funcl (id, rewrite_pexp rewriters pexp),(l,annot))) - in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,fdannot)) + in + let recopt = match recopt with + | Rec_aux (Rec_nonrec, l) -> Rec_aux (Rec_nonrec, l) + | Rec_aux (Rec_rec, l) -> Rec_aux (Rec_rec, l) + | Rec_aux (Rec_measure (pat,exp),l) -> + Rec_aux (Rec_measure (rewrite_pat rewriters pat, rewrite_exp rewriters exp),l) + in + FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,fdannot)) let rewrite_def rewriters d = match d with | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), annot)) -> |