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