diff options
Diffstat (limited to 'src/gen_lib/state.lem')
| -rw-r--r-- | src/gen_lib/state.lem | 61 |
1 files changed, 41 insertions, 20 deletions
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index cbec7204..69b9e301 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -238,35 +238,56 @@ let rec foreachM_dec (stop,i,by) vars body = foreachM_dec (stop,i - by,by) vars body else return vars -val while_PP : forall 'vars. bool -> 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars -let rec while_PP is_while vars cond body = - if (cond vars = is_while) - then while_PP is_while (body vars) cond body - else vars +val while_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars +let rec while_PP vars cond body = + if cond vars then while_PP (body vars) cond body else vars -val while_PM : forall 'regs 'vars 'e. bool -> 'vars -> ('vars -> bool) -> +val while_PM : forall 'regs 'vars 'e. 'vars -> ('vars -> bool) -> ('vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e -let rec while_PM is_while vars cond body = - if (cond vars = is_while) - then body vars >>= fun vars -> while_PM is_while vars cond body +let rec while_PM vars cond body = + if cond vars then + body vars >>= fun vars -> while_PM vars cond body else return vars -val while_MP : forall 'regs 'vars 'e. bool -> 'vars -> ('vars -> ME 'regs bool 'e) -> +val while_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> ME 'regs bool 'e) -> ('vars -> 'vars) -> ME 'regs 'vars 'e -let rec while_MP is_while vars cond body = - cond vars >>= fun continue -> - if (continue = is_while) - then while_MP is_while (body vars) cond body - else return vars +let rec while_MP vars cond body = + cond vars >>= fun cond_val -> + if cond_val then while_MP (body vars) cond body else return vars -val while_MM : forall 'regs 'vars 'e. bool -> 'vars -> ('vars -> ME 'regs bool 'e) -> +val while_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> ME 'regs bool 'e) -> ('vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e -let rec while_MM is_while vars cond body = - cond vars >>= fun continue -> - if (continue = is_while) - then body vars >>= fun vars -> while_MM is_while vars cond body +let rec while_MM vars cond body = + cond vars >>= fun cond_val -> + if cond_val then + body vars >>= fun vars -> while_MM vars cond body else return vars +val until_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars +let rec until_PP vars cond body = + let vars = body vars in + if (cond vars) then vars else until_PP (body vars) cond body + +val until_PM : forall 'regs 'vars 'e. 'vars -> ('vars -> bool) -> + ('vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e +let rec until_PM vars cond body = + body vars >>= fun vars -> + if (cond vars) then return vars else until_PM vars cond body + +val until_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> ME 'regs bool 'e) -> + ('vars -> 'vars) -> ME 'regs 'vars 'e +let rec until_MP vars cond body = + let vars = body vars in + cond vars >>= fun cond_val -> + if cond_val then return vars else until_MP vars cond body + +val until_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> ME 'regs bool 'e) -> + ('vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e +let rec until_MM vars cond body = + body vars >>= fun vars -> + cond vars >>= fun cond_val -> + if cond_val then return vars else until_MM vars cond body + (*let write_two_regs r1 r2 bvec state = let vec = bvec_to_vec bvec in let is_inc = |