Permalink
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
50 lines (40 sloc) 1.8 KB
(*
The signature of the monadic translator.
*)
signature ml_monad_translatorLib =
sig
include ml_monadStoreLib
(* Functions to initialize the translation *)
val start_static_init_fixed_store_translation :
(string * thm * thm * thm) list ->
(string * thm * thm * thm * thm * thm * thm * thm) list ->
(string * (int * thm) * thm * thm * thm * thm * thm) list ->
string -> hol_type -> thm -> (thm * thm) list -> string list ->
(thm * thm) option -> term option ->
monadic_translation_parameters *
store_translation_result * (thm * thm) list
val start_dynamic_init_fixed_store_translation :
(string * thm * thm) list ->
(string * thm * thm * thm * thm * thm * thm) list ->
(string * thm * thm * thm * thm * thm) list ->
string -> hol_type -> thm -> (thm * thm) list -> string list ->
thm option -> monadic_translation_parameters * (thm * thm) list
(* Other functions to initialize the translation - the above ones should be preferred *)
val init_translation :
monadic_translation_parameters -> (thm * thm) list ->
(thm * thm * thm * thm * thm * thm) list ->
(thm * thm * thm * thm * thm) list ->
(thm * thm) list ->
thm option -> thm -> string list -> thm option -> unit
val add_raise_handle_functions : (thm * thm) list -> thm -> (thm * thm) list
val add_access_pattern : thm -> thm
(* Translation functions *)
val m_translate : thm -> thm
val m_translate_run : thm -> thm
val m2deep : term -> thm
(* Resume prior monadic translation.
Loads the state specific to the monadic translation from the specified
theory, followed by a call to translation_extends from the 'standard'
translator (i.e. fetching the rest of the translator state). *)
val m_translation_extends : string -> unit
end