1signature compilerLib =
2sig
3
4  include Abbrev
5
6  (* supported targets are "arm", "ppc" and "x86" *)
7
8  (* mc_define defines a function and puts the definition on a queue
9     waiting to be compiled, returns function definition and pre *)
10  val mc_define        : term quotation -> thm * thm
11
12  (* mc_compile fname target: compiles function fname to target code,
13     returns a Hoare triple containing the generated code *)
14  val mc_compile       : string -> string -> thm
15
16  (* mc_compile_all fname: compiles function fname to all targets *)
17  val mc_compile_all   : string -> (string * thm) list
18
19  (* these functions expose the back-end functions *)
20  val compile      : string -> term -> thm * thm * thm
21  val compile_all  : term -> (string * thm) list * thm * thm
22
23  (* the tactic used for proving function equivalence *)
24  val COMPILER_TAC : tactic
25
26end
27