summaryrefslogtreecommitdiff
path: root/src/gen_lib/state_monad.lem
diff options
context:
space:
mode:
authorBrian Campbell2018-05-17 16:39:30 +0100
committerBrian Campbell2018-05-17 16:39:30 +0100
commit1867ec89a4493ca6ce92c8926885c4090b6d3d5d (patch)
tree8f6b4a527d80180341c8b19efd21c869a5e30065 /src/gen_lib/state_monad.lem
parent333bbb7cbfda60eda1bfe6642e068f2795056c1d (diff)
parentf5672ea6a1e04ad1f2bee91ad86584b183d323b4 (diff)
Merge branch 'cheri-mono' into sail2
Diffstat (limited to 'src/gen_lib/state_monad.lem')
-rw-r--r--src/gen_lib/state_monad.lem14
1 files changed, 7 insertions, 7 deletions
diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem
index a2919762..89021890 100644
--- a/src/gen_lib/state_monad.lem
+++ b/src/gen_lib/state_monad.lem
@@ -94,12 +94,12 @@ let assert_expS exp msg = if exp then returnS () else failS msg
(* For early return, we abuse exceptions by throwing and catching
the return value. The exception type is "either 'r 'e", where "Right e"
represents a proper exception and "Left r" an early return of value "r". *)
-type monadSR 'regs 'a 'r 'e = monadS 'regs 'a (either 'r 'e)
+type monadRS 'regs 'a 'r 'e = monadS 'regs 'a (either 'r 'e)
-val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadSR 'regs 'a 'r 'e
+val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadRS 'regs 'a 'r 'e
let early_returnS r = throwS (Left r)
-val catch_early_returnS : forall 'regs 'a 'e. monadSR 'regs 'a 'a 'e -> monadS 'regs 'a 'e
+val catch_early_returnS : forall 'regs 'a 'e. monadRS 'regs 'a 'a 'e -> monadS 'regs 'a 'e
let catch_early_returnS m =
try_catchS m
(function
@@ -108,12 +108,12 @@ let catch_early_returnS m =
end)
(* Lift to monad with early return by wrapping exceptions *)
-val liftSR : forall 'a 'r 'regs 'e. monadS 'regs 'a 'e -> monadSR 'regs 'a 'r 'e
-let liftSR m = try_catchS m (fun e -> throwS (Right e))
+val liftRS : forall 'a 'r 'regs 'e. monadS 'regs 'a 'e -> monadRS 'regs 'a 'r 'e
+let liftRS m = try_catchS m (fun e -> throwS (Right e))
(* Catch exceptions in the presence of early returns *)
-val try_catchSR : forall 'regs 'a 'r 'e1 'e2. monadSR 'regs 'a 'r 'e1 -> ('e1 -> monadSR 'regs 'a 'r 'e2) -> monadSR 'regs 'a 'r 'e2
-let try_catchSR m h =
+val try_catchRS : forall 'regs 'a 'r 'e1 'e2. monadRS 'regs 'a 'r 'e1 -> ('e1 -> monadRS 'regs 'a 'r 'e2) -> monadRS 'regs 'a 'r 'e2
+let try_catchRS m h =
try_catchS m
(function
| Left r -> throwS (Left r)