Use an intermediate base_monad type alias in Lem,

resolving the difference in type parameters between the prompt and state
monads, and allowing a single output file to be used with either.
Normally, the type alias is to the prompt monad, but for HOL4 we use the
state monad.

2 files changed, 22 insertions, 2 deletions

diff --git a/lib/hol/prompt.lem b/lib/hol/prompt.lem
index a04e0a0a..edbd3752 100644
--- a/lib/hol/prompt.lem
+++ b/lib/hol/prompt.lem
@@ -10,3 +10,9 @@ let inline of_bits_oracle = of_bits_oracleS
 let inline of_bits_fail = of_bits_failS
 let inline mword_oracle = mword_oracleS
 let inline reg_deref = read_regS
+
+let inline foreachM = foreachS
+let inline whileM = whileS
+let inline untilM = untilS
+let inline and_boolM = and_boolS
+let inline or_boolM = or_boolS
diff --git a/lib/hol/prompt_monad.lem b/lib/hol/prompt_monad.lem
index 4481f623..8fcd645a 100644
--- a/lib/hol/prompt_monad.lem
+++ b/lib/hol/prompt_monad.lem
@@ -9,27 +9,41 @@ open import State_monad
 type monad 'rv 'a 'e = monadS 'rv 'a 'e
 type monadR 'rv 'a 'e 'r = monadRS 'rv 'a 'e 'r
 
+(* We need to use a target_rep for these because HOL doesn't handle unused
+   type parameters well. *)
+
+type base_monad 'regval 'regstate 'a 'e = monad 'regstate 'a 'e
+declare hol target_rep type base_monad 'regval 'regstate 'a 'e = `monad` 'regstate 'a 'e
+type base_monadR 'regval 'regstate 'a 'r 'e = monadR 'regstate 'a 'r 'e
+declare hol target_rep type base_monadR 'regval 'regstate 'a 'r 'e = `monadR` 'regstate 'a 'r 'e
+
 let inline return = returnS
 let inline bind = bindS
 let inline (>>=) = (>>$=)
 let inline (>>) = (>>$)
 
+let inline exit = exitS
+
 let inline throw = throwS
 let inline try_catch = try_catchS
 
 let inline catch_early_return = catch_early_returnS
 let inline early_return = early_returnS
+let inline liftR = liftRS
+let inline try_catchR = try_catchRS
 
 let inline maybe_fail = maybe_failS
 
+let inline read_mem_bytes = read_mem_bytesS
 let inline read_reg = read_regS
 let inline reg_deref = read_regS
 let inline read_mem = read_memS
 let inline read_tag = read_tagS
+let inline excl_result = excl_resultS
+let inline write_reg = write_regS
 let inline write_tag = write_tagS
 let inline write_mem_ea wk addr sz = write_mem_eaS wk addr (nat_of_int sz)
 let inline write_mem_val = write_mem_valS
 let barrier _ = return ()
 
-let inline excl_result = excl_resultS
-let inline assert_exp = assert_expS
\ No newline at end of file
+let inline assert_exp = assert_expS