File ‹Transform_Const.ML›
signature TRANSFORM_CONST =
sig
type MONAD_CONSTS = {
monad_name: string,
mk_stateT: typ -> typ,
return: term -> term,
app: (term * term) -> term,
if_termN: string,
checkmemVN: string,
rewrite_app_beta_conv: conv
}
val get_monad_const: string -> MONAD_CONSTS
end
structure Transform_Const : TRANSFORM_CONST =
struct
val pureappN = @{const_name Pure_Monad.App}
fun pureapp tm = Const (pureappN, dummyT) $ tm
type MONAD_CONSTS = {
monad_name: string,
mk_stateT: typ -> typ,
return: term -> term,
app: (term * term) -> term,
if_termN: string,
checkmemVN: string,
rewrite_app_beta_conv: conv
}
val state_monad: MONAD_CONSTS =
let
val memT = TFree ("MemoryType", @{sort type})
val memT = dummyT
fun mk_stateT tp =
Type (@{type_name State_Monad.state}, [memT, tp])
val returnN = @{const_name State_Monad.return}
fun return tm = Const (returnN, dummyT --> mk_stateT dummyT) $ tm
val appN = @{const_name State_Monad_Ext.fun_app_lifted}
fun app (tm0, tm1) = Const (appN, dummyT) $ tm0 $ tm1
fun checkmem'C ctxt = Transform_Misc.get_const_pat ctxt "checkmem'"
fun checkmem' ctxt param body = checkmem'C ctxt $ param $ body
val checkmemVN = "checkmem"
val checkmemC = @{const_name "state_mem_defs.checkmem"}
fun rewrite_app_beta_conv ctm =
case Thm.term_of ctm of
Const (@{const_name State_Monad_Ext.fun_app_lifted}, _)
$ (Const (@{const_name State_Monad.return}, _) $ Abs _)
$ (Const (@{const_name State_Monad.return}, _) $ _)
=> Conv.rewr_conv @{thm State_Monad_Ext.return_app_return_meta} ctm
| _ => Conv.no_conv ctm
in {
monad_name = "state",
mk_stateT = mk_stateT,
return = return,
app = app,
if_termN = @{const_name State_Monad_Ext.if⇩T},
checkmemVN = checkmemVN,
rewrite_app_beta_conv = rewrite_app_beta_conv
} end
val heap_monad: MONAD_CONSTS =
let
fun mk_stateT tp =
Type (@{type_name Heap_Monad.Heap}, [tp])
val returnN = @{const_name Heap_Monad.return}
fun return tm = Const (returnN, dummyT --> mk_stateT dummyT) $ tm
val appN = @{const_name Heap_Monad_Ext.fun_app_lifted}
fun app (tm0, tm1) = Const (appN, dummyT) $ tm0 $ tm1
fun checkmem'C ctxt = Transform_Misc.get_const_pat ctxt "checkmem'"
fun checkmem' ctxt param body = checkmem'C ctxt $ param $ body
val checkmemVN = "checkmem"
val checkmemC = @{const_name "heap_mem_defs.checkmem"}
fun rewrite_app_beta_conv ctm =
case Thm.term_of ctm of
Const (@{const_name Heap_Monad_Ext.fun_app_lifted}, _)
$ (Const (@{const_name Heap_Monad.return}, _) $ Abs _)
$ (Const (@{const_name Heap_Monad.return}, _) $ _)
=> Conv.rewr_conv @{thm Heap_Monad_Ext.return_app_return_meta} ctm
| _ => Conv.no_conv ctm
in {
monad_name = "heap",
mk_stateT = mk_stateT,
return = return,
app = app,
if_termN = @{const_name Heap_Monad_Ext.if⇩T},
checkmemVN = checkmemVN,
rewrite_app_beta_conv = rewrite_app_beta_conv
} end
val monad_consts_dict = [
("state", state_monad),
("heap", heap_monad)
]
fun get_monad_const name =
case AList.lookup op= monad_consts_dict name of
SOME consts => consts
| NONE => error("unrecognized monad: " ^ name ^ " , choices: " ^ commas (map fst monad_consts_dict));
end