1 files changed, 54 insertions, 30 deletions

diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 1ca25b74..69b9e301 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -19,18 +19,18 @@ type sequential_state 'regs =
    and exception type 'e. *)
 type ME 'regs 'a 'e = sequential_state 'regs -> list ((either 'a 'e) * sequential_state 'regs)
 
-(* Most of the time, we don't distinguish between different types of exceptions *)
-type M 'regs 'a = ME 'regs 'a unit
+(* By default, we use strings to distinguish between different types of exceptions *)
+type M 'regs 'a = ME 'regs 'a string
 
 (* For early return, we abuse exceptions by throwing and catching
-   the return value. The exception type is "maybe 'r", where "Nothing"
-   represents a proper exception and "Just r" an early return of value "r". *)
-type MR 'regs 'a 'r = ME 'regs 'a (maybe 'r)
+   the return value. The exception type is "either 'r string", where "Right e"
+   represents a proper exception and "Left r" an early return of value "r". *)
+type MR 'regs 'a 'r = ME 'regs 'a (either 'r string)
 
 val liftR : forall 'a 'r 'regs. M 'regs 'a -> MR 'regs 'a 'r
 let liftR m s = List.map (function
   | (Left a, s') -> (Left a, s')
-  | (Right (), s') -> (Right Nothing, s')
+  | (Right e, s') -> (Right (Right e), s')
   end) (m s)
 
 val return : forall 'regs 'a 'e. 'a -> ME 'regs 'a 'e
@@ -48,17 +48,20 @@ val (>>): forall 'regs 'b 'e. ME 'regs unit 'e -> ME 'regs 'b 'e -> ME 'regs 'b
 let inline (>>) m n = m >>= fun _ -> n
 
 val exit : forall 'regs 'e 'a. 'e -> M 'regs 'a
-let exit _ s = [(Right (), s)]
+let exit _ s = [(Right "exit", s)]
+
+val assert_exp : forall 'regs. bool -> string -> M 'regs unit
+let assert_exp exp msg s = if exp then [(Left (), s)] else [(Right msg, s)]
 
 val early_return : forall 'regs 'a 'r. 'r -> MR 'regs 'a 'r
-let early_return r s = [(Right (Just r), s)]
+let early_return r s = [(Right (Left r), s)]
 
 val catch_early_return : forall 'regs 'a. MR 'regs 'a 'a -> M 'regs 'a
 let catch_early_return m s =
   List.map
     (function
-     | (Right (Just a), s') -> (Left a, s')
-     | (Right Nothing, s') -> (Right (), s')
+     | (Right (Left a), s') -> (Left a, s')
+     | (Right (Right e), s') -> (Right e, s')
      | (Left a, s') -> (Left a, s')
     end) (m s)
 
@@ -235,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 =