1signature armSyntax = 2sig 3 4 include Abbrev 5 6 val dest_strip : term -> string * term list 7 val dest_monad_type : hol_type -> hol_type 8 9 val valuestate_tm : term 10 val error_tm : term 11 val constT_tm : term 12 val seqT_tm : term 13 val parT_tm : term 14 val forT_tm : term 15 val readT_tm : term 16 val writeT_tm : term 17 val read__reg_tm : term 18 val write__reg_tm : term 19 val read__psr_tm : term 20 val write__psr_tm : term 21 val read_reg_mode_tm : term 22 val write_reg_mode_tm : term 23 val read_reg_tm : term 24 val write_reg_tm : term 25 val read_cpsr_tm : term 26 val write_cpsr_tm : term 27 val read_spsr_tm : term 28 val write_spsr_tm : term 29 val read_memA_tm : term 30 val write_memA_tm : term 31 val decode_psr_tm : term 32 val bytes_tm : term 33 val align_tm : term 34 val aligned_tm : term 35 val ITAdvance_tm : term 36 val NoInterrupt_tm : term 37 val HW_Reset_tm : term 38 val HW_Fiq_tm : term 39 val HW_Irq_tm : term 40 val Encoding_ARM_tm : term 41 val Encoding_Thumb_tm : term 42 val Encoding_Thumb2_tm : term 43 val Encoding_ThumbEE_tm : term 44 val clear_event_register_tm : term 45 val send_event_tm : term 46 val wait_for_interrupt_tm : term 47 val clear_wait_for_interrupt_tm : term 48 val arm_decode_tm : term 49 val thumb_decode_tm : term 50 val thumbee_decode_tm : term 51 val thumb2_decode_tm : term 52 53 val mk_valuestate : term * term -> term 54 val mk_error : term -> term 55 val mk_constT : term -> term 56 val mk_seqT : term * term -> term 57 val mk_parT : term * term -> term 58 val mk_forT : term * term * term -> term 59 val mk_readT : term -> term 60 val mk_writeT : term -> term 61 val mk_read__reg : term * term -> term 62 val mk_write__reg : term * term * term -> term 63 val mk_read__psr : term * term -> term 64 val mk_write__psr : term * term * term -> term 65 val mk_read_reg_mode : term * term * term -> term 66 val mk_write_reg_mode : term * term * term * term -> term 67 val mk_read_reg : term * term -> term 68 val mk_write_reg : term * term * term -> term 69 val mk_read_cpsr : term -> term 70 val mk_write_cpsr : term * term -> term 71 val mk_read_spsr : term -> term 72 val mk_write_spsr : term * term -> term 73 val mk_read_memA : term * term * term -> term 74 val mk_write_memA : term * term * term * term -> term 75 val mk_decode_psr : term -> term 76 val mk_bytes : term * term -> term 77 val mk_align : term * term -> term 78 val mk_aligned : term * term -> term 79 val mk_ITAdvance : term -> term 80 val mk_clear_event_register : term -> term 81 val mk_send_event : term -> term 82 val mk_wait_for_interrupt : term -> term 83 val mk_clear_wait_for_interrupt : term -> term 84 val mk_read_memA_1 : term * term -> term 85 val mk_write_memA_1 : term * term * term -> term 86 val mk_read_memA_2 : term * term -> term 87 val mk_write_memA_2 : term * term * term -> term 88 val mk_read_memA_4 : term * term -> term 89 val mk_write_memA_4 : term * term * term -> term 90 val mk_arm_decode : term * term -> term 91 val mk_thumb_decode : term * term * term -> term 92 val mk_thumbee_decode : term * term * term -> term 93 val mk_thumb2_decode : term * term * term * term -> term 94 95 val dest_valuestate : term -> term * term 96 val dest_error : term -> term 97 val dest_constT : term -> term 98 val dest_seqT : term -> term * term 99 val dest_parT : term -> term * term 100 val dest_forT : term -> term * term * term 101 val dest_readT : term -> term 102 val dest_writeT : term -> term 103 val dest_read__reg : term -> term * term 104 val dest_write__reg : term -> term * term * term 105 val dest_read__psr : term -> term * term 106 val dest_write__psr : term -> term * term * term 107 val dest_read_reg_mode : term -> term * term 108 val dest_write_reg_mode : term -> term * term * term 109 val dest_read_reg : term -> term * term 110 val dest_write_reg : term -> term * term * term 111 val dest_read_cpsr : term -> term 112 val dest_write_cpsr : term -> term * term 113 val dest_read_spsr : term -> term 114 val dest_write_spsr : term -> term * term 115 val dest_read_memA : term -> term * term 116 val dest_write_memA : term -> term * term * term 117 val dest_clear_event_register : term -> term 118 val dest_send_event : term -> term 119 val dest_wait_for_interrupt : term -> term 120 val dest_clear_wait_for_interrupt : term -> term 121 val dest_decode_psr : term -> term 122 val dest_bytes : term -> term 123 val dest_align : term -> term 124 val dest_aligned : term -> term 125 val dest_ITAdvance : term -> term 126 val dest_arm_decode : term -> term * term 127 val dest_thumb_decode : term -> term * term * term 128 val dest_thumbee_decode : term -> term * term * term 129 val dest_thumb2_decode : term -> term * term * term 130 131 val is_valuestate : term -> bool 132 val is_error : term -> bool 133 val is_constT : term -> bool 134 val is_seqT : term -> bool 135 val is_parT : term -> bool 136 val is_forT : term -> bool 137 val is_readT : term -> bool 138 val is_writeT : term -> bool 139 val is_read__reg : term -> bool 140 val is_write__reg : term -> bool 141 val is_read__psr : term -> bool 142 val is_write__psr : term -> bool 143 val is_read_reg_mode : term -> bool 144 val is_write_reg_mode : term -> bool 145 val is_read_reg : term -> bool 146 val is_write_reg : term -> bool 147 val is_read_cpsr : term -> bool 148 val is_write_cpsr : term -> bool 149 val is_read_spsr : term -> bool 150 val is_write_spsr : term -> bool 151 val is_read_memA : term -> bool 152 val is_write_memA : term -> bool 153 val is_clear_event_register : term -> bool 154 val is_send_event : term -> bool 155 val is_wait_for_interrupt : term -> bool 156 val is_clear_wait_for_interrupt : term -> bool 157 val is_decode_psr : term -> bool 158 val is_bytes : term -> bool 159 val is_align : term -> bool 160 val is_aligned : term -> bool 161 val is_ITAdvance : term -> bool 162 val is_arm_decode : term -> bool 163 val is_thumb_decode : term -> bool 164 val is_thumbee_decode : term -> bool 165 val is_thumb2_decode : term -> bool 166 167end 168