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