summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/gen_lib/prompt.lem61
-rw-r--r--src/gen_lib/state.lem61
-rw-r--r--src/pretty_print_lem.ml8
-rw-r--r--src/rewriter.ml20
4 files changed, 97 insertions, 53 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index cdff2972..8ef9dd9b 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -177,35 +177,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 'vars 'r. bool -> 'vars -> ('vars -> bool) ->
+val while_PM : forall 'vars 'r. 'vars -> ('vars -> bool) ->
('vars -> MR 'vars 'r) -> MR 'vars 'r
-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 'vars 'r. bool -> 'vars -> ('vars -> MR bool 'r) ->
+val while_MP : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) ->
('vars -> 'vars) -> MR 'vars 'r
-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 'vars 'r. bool -> 'vars -> ('vars -> MR bool 'r) ->
+val while_MM : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) ->
('vars -> MR 'vars 'r) -> MR 'vars 'r
-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 'vars 'r. 'vars -> ('vars -> bool) ->
+ ('vars -> MR 'vars 'r) -> MR 'vars 'r
+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 'vars 'r. 'vars -> ('vars -> MR bool 'r) ->
+ ('vars -> 'vars) -> MR 'vars 'r
+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 'vars 'r. 'vars -> ('vars -> MR bool 'r) ->
+ ('vars -> MR 'vars 'r) -> MR 'vars 'r
+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 vec =
let is_inc =
let is_inc_r1 = is_inc_of_reg r1 in
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 =
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 67febd0a..3832c187 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -662,8 +662,10 @@ let doc_exp_lem, doc_let_lem =
)
)
| Id_aux ((Id (("while_PP" | "while_PM" |
- "while_MP" | "while_MM" ) as loopf),_)) ->
- let [is_while;cond;body;e5] = args in
+ "while_MP" | "while_MM" |
+ "until_PP" | "until_PM" |
+ "until_MP" | "until_MM") as loopf),_)) ->
+ let [cond;body;e5] = args in
let varspp = match e5 with
| E_aux (E_tuple vars,_) ->
let vars = List.map (fun (E_aux (E_id id,_)) -> doc_id_lem id) vars in
@@ -676,7 +678,7 @@ let doc_exp_lem, doc_let_lem =
string "_" in
parens (
(prefix 2 1)
- ((separate space) [string loopf;expY is_while;expY e5])
+ ((separate space) [string loopf; expY e5])
((prefix 0 1)
(parens (prefix 1 1 (separate space [string "fun";varspp;arrow]) (expN cond)))
(parens (prefix 1 1 (separate space [string "fun";varspp;arrow]) (expN body))))
diff --git a/src/rewriter.ml b/src/rewriter.ml
index c537e196..ba767081 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -3339,17 +3339,17 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
(* 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 fname = match loop, effectful cond, effectful body with
+ | While, false, false -> "while_PP"
+ | While, false, true -> "while_PM"
+ | While, true, false -> "while_MP"
+ | While, true, true -> "while_MM"
+ | Until, false, false -> "until_PP"
+ | Until, false, true -> "until_PM"
+ | Until, true, false -> "until_MP"
+ | Until, true, true -> "until_MM" in
let funcl = Id_aux (Id fname,gen_loc el) in
- let is_while =
- match loop with
- | While -> annot_exp (E_lit (mk_lit L_true)) (gen_loc el) env bool_typ
- | Until -> annot_exp (E_lit (mk_lit L_false)) (gen_loc el) env bool_typ in
- let v = E_aux (E_app (funcl,[is_while;cond;body;vartuple]), (gen_loc el, bannot)) in
+ let v = E_aux (E_app (funcl,[cond;body;vartuple]), (gen_loc el, bannot)) in
let pat =
if overwrite then mktup_pat el vars
else annot_pat (P_tup [pat; mktup_pat pl vars]) pl env (typ_of v) in
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 18:41:07 +0000