1signature m0_stepLib =
2sig
3   val thumb_instruction: Term.term -> string
4   val thumb_step: bool * bool -> string -> Thm.thm list
5   val thumb_step_code: bool * bool -> string quotation -> Thm.thm list list
6   val thumb_step_hex: bool * bool -> string -> Thm.thm list
7   val thumb_decode: bool -> Term.term -> Thm.thm list
8   val thumb_decode_hex: bool -> string -> Thm.thm list
9   val hex_to_bits: string -> Term.term
10   val list_instructions: unit -> (string * Term.term) list
11   val print_instructions: unit -> unit
12
13   (*
14
15     open m0_stepLib
16     val () = print_instructions ()
17     val ev = thumb_step (true, true)
18     fun pev s = (print (s ^ "\n"); Count.apply ev s);
19     val _ = Count.apply (List.map ev) (list_instructions ())
20     val _ = Count.apply (List.map (Lib.total pev)) (list_instructions ())
21     ev "POP; 2"
22     ev "ADD (pc)"
23
24   *)
25end
26