1signature arm_evalLib =
2sig
3   include Abbrev
4
5   type mode
6   type arm_state
7
8   val arm_compset          : computeLib.compset
9   val ARM_CONV             : conv
10   val ARM_RULE             : rule
11   val ARM_ASSEMBLE_CONV    : conv
12   val SORT_UPDATE_CONV     : conv
13
14   val hol_assemble1        : term -> Arbnum.num -> term frag list -> term
15   val hol_assemble         : term -> Arbnum.num -> term frag list list -> term
16   val list_assemble        : term -> string list -> term
17   val assemble1            : term -> string -> term
18   val assemble             : term -> string -> term
19
20   val empty_memory         : term
21   val empty_registers      : term
22   val empty_psrs           : term
23
24   val set_registers        : term -> term frag list -> term
25   val set_status_registers : term -> term frag list -> term
26
27   val dest_arm_eval    : term -> arm_state
28
29   val print_all_regs   : term -> unit
30   val print_usr_regs   : term -> unit
31   val print_std_regs   : term -> unit
32   val print_regs       : (int * mode) list -> term -> unit
33   val print_mem_range  : term -> Arbnum.num * int -> unit
34   val print_mem_block  : term -> int -> unit
35
36   val load_mem  : string -> int -> Arbnum.num -> term -> term
37   val save_mem  : string -> Arbnum.num -> Arbnum.num -> bool -> term -> unit
38
39   val init        : term -> term -> term -> term -> term -> thm
40   val next        : term * thm -> thm
41
42   val eval_cp     : int * term * term * term * term * term -> thm list
43   val evaluate_cp : int * term * term * term * term * term -> thm
44
45   val eval        : int * term * term * term -> thm list
46   val evaluate    : int * term * term * term -> thm
47end
48