summaryrefslogtreecommitdiff
path: root/src/gen_lib/state_monad.lem
diff options
context:
space:
mode:
authorJon French2018-06-11 15:25:02 +0100
committerJon French2018-06-11 15:25:02 +0100
commit826e94548a86a88d8fefeb1edef177c02bf5d68d (patch)
treefc9a5484440e030cc479101c5cab345c1c77468e /src/gen_lib/state_monad.lem
parent5717bb3d0cef5932cb2b33bc66b3b2f0c0552164 (diff)
parent4336409f923c10a8c5e4acc91fa7e6ef5551a88f (diff)
Merge branch 'sail2' into mappings
(involved some manual tinkering with gitignore, type_check, riscv)
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)