1structure basic :> basic = 2struct 3 4open HolKernel Parse boolSyntax boolLib bossLib pairSyntax wordsSyntax; 5 6(*---------------------------------------------------------------------------*) 7(* Common used data structures and functions *) 8(*---------------------------------------------------------------------------*) 9 10(*---------------------------------------------------------------------------*) 11(* (Atomic) Variables and Operators *) 12(*---------------------------------------------------------------------------*) 13 14(* Is the term a word? *) 15fun is_word_literal tm = 16 case total dest_n2w tm 17 of NONE => false 18 | SOME (ntm,wty) => numSyntax.is_numeral ntm; 19 20(* Is the term a word or num literal? *) 21fun is_literal tm = 22 is_word_literal tm orelse numSyntax.is_numeral tm 23 24fun is_8bit_literal tm = 25 is_word_literal tm andalso numSyntax.int_of_term (#2 (dest_comb tm)) < 256 26 27(* Is the term an atomic term? *) 28fun is_atomic t = 29 is_var t orelse is_word_literal t orelse 30 numSyntax.is_numeral t orelse is_const t orelse 31 is_neg t (* ~x is considered to be an atom *) 32 ; 33 34fun OR test [] = false 35 | OR test (h::t) = test h orelse OR test t; 36 37(*---------------------------------------------------------------------------*) 38(* Is the operator a binary arithmetic operator? *) 39(*---------------------------------------------------------------------------*) 40 41fun is_num_arithop op0 = 42 let open numSyntax 43 in 44 OR (same_const op0) [plus_tm,minus_tm,mult_tm,exp_tm] 45 end; 46 47(*---------------------------------------------------------------------------*) 48(* Is the operator an arithmetic comparison operator? *) 49(*---------------------------------------------------------------------------*) 50 51fun is_num_cmpop op0 = 52 let open numSyntax 53 val equality = inst [alpha |-> num] boolSyntax.equality 54 in 55 OR (same_const op0) [greater_tm, geq_tm,less_tm,equality,leq_tm] 56 end; 57 58(*---------------------------------------------------------------------------*) 59(* Is the operator an arithmetic word operator? *) 60(*---------------------------------------------------------------------------*) 61 62fun is_word_arithop op0 = 63 let open wordsSyntax 64 in 65 OR (same_const op0) [word_add_tm,word_sub_tm,word_mul_tm] 66 end; 67 68(*---------------------------------------------------------------------------*) 69(* Is the operator a multiplication operator? *) 70(*---------------------------------------------------------------------------*) 71 72fun is_mult_op op0 = 73 (op0 = numSyntax.mult_tm) orelse 74 (#1 (dest_const(wordsSyntax.word_mul_tm)) = #1 (dest_const op0) 75 handle _ => false); 76 77(*---------------------------------------------------------------------------*) 78(* Is the operator a word comparison operator? Includes equality *) 79(* comparisons. *) 80(*---------------------------------------------------------------------------*) 81 82val is_word_equality = 83 Lib.can (match_term (mk_const("=",``:'a word -> 'a word -> bool``))); 84 85fun is_word_cmpop op0 = 86 let open wordsSyntax 87 in 88 is_word_equality op0 orelse 89 OR (same_const op0) [word_lt_tm,word_le_tm,word_gt_tm,word_ge_tm, 90 word_hi_tm, word_hs_tm, word_lo_tm, word_ls_tm] 91 end; 92 93(*---------------------------------------------------------------------------*) 94(* Is the operator a bitwise word operator? *) 95(*---------------------------------------------------------------------------*) 96 97fun is_word_shiftop op0 = 98 let open wordsSyntax 99 in 100 OR (same_const op0) 101 [word_ror_tm,word_rol_tm,word_lsl_tm,word_lsr_tm,word_asr_tm] 102 end; 103 104(*---------------------------------------------------------------------------*) 105(* Is the operator a bitwise word operator? *) 106(*---------------------------------------------------------------------------*) 107 108fun is_word_bitwiseop op0 = 109 let open wordsSyntax 110 in 111 OR (same_const op0) [word_xor_tm,word_and_tm,word_or_tm] 112 end; 113 114 115(*---------------------------------------------------------------------------*) 116(* Is the operator a logical operator? *) 117(*---------------------------------------------------------------------------*) 118 119fun is_relop op0 = 120 let open boolSyntax 121 in 122 OR (same_const op0) [conjunction,disjunction] 123 end; 124 125fun is_binop opr = 126 is_relop opr orelse 127 is_word_bitwiseop opr orelse 128 is_num_arithop opr orelse 129 is_word_arithop opr orelse 130 is_num_cmpop opr orelse 131 is_word_cmpop opr orelse 132 is_word_shiftop opr; 133 134 135(*---------------------------------------------------------------------------*) 136(* Is the expression in a conditional test an (atomic) comparison? *) 137(*---------------------------------------------------------------------------*) 138 139fun is_atom_cond tm = 140 is_comb tm andalso 141 let val (op0,_) = strip_comb tm 142 in 143 is_num_cmpop op0 orelse is_word_cmpop op0 144 end; 145 146(*---------------------------------------------------------------------------*) 147(* Last Expression *) 148(*---------------------------------------------------------------------------*) 149 150fun last_exp exp = 151 if is_let exp then 152 last_exp (#3 (dest_plet exp)) 153 else exp; 154 155(*---------------------------------------------------------------------------*) 156(* Term manipulating functions *) 157(*---------------------------------------------------------------------------*) 158 159(* substitute variables in an expression *) 160fun subst_exp rule exp = 161 if is_plet exp then 162 let val (v, M, N) = dest_plet exp 163 in 164 mk_plet (v, subst_exp rule M, subst_exp rule N) 165 end 166 else if is_cond exp then 167 let val (c,t,f) = dest_cond exp 168 in 169 mk_cond (subst_exp rule c, subst_exp rule t, subst_exp rule f) 170 end 171 else if is_pair exp then 172 let val (t1,t2) = dest_pair exp 173 in mk_pair (subst_exp rule t1, subst_exp rule t2) 174 end 175 else subst rule exp 176 177(* Term t1 occurs in t2? *) 178fun occurs_in t1 t2 = can (find_term (aconv t1)) t2; 179 180(* Convert a function definition into a lamba format *) 181fun abs_fun def = 182 let 183 val t0 = concl (SPEC_ALL def) 184 val (fname, args) = dest_comb (lhs t0) 185 val body = rhs t0 186 val th1 = prove (mk_eq (fname, mk_pabs(args,body)), 187 SIMP_TAC std_ss [FUN_EQ_THM, pairTheory.FORALL_PROD, Once def]) 188 in 189 th1 190 end 191 handle HOL_ERR _ => def (* already an abstraction *) 192 193(*---------------------------------------------------------------------------*) 194(* Find the ouput of a term. *) 195(*---------------------------------------------------------------------------*) 196 197fun identify_output t = 198 let 199 fun trav t = 200 if is_let t then 201 let val (v,M,N) = dest_plet t 202 in trav N end 203 else if is_cond t then 204 let val (J, M1, M2) = dest_cond t 205 val t1 = trav M1 206 val t2 = trav M2 207 in if t1 = t2 then t1 208 else case t1 of 209 SOME x => (case t2 of 210 SOME y => raise Fail "the outputs of two branches are different!" 211 | NONE => SOME x 212 ) 213 | NONE => t1 214 end 215 else if is_pabs t then 216 let val (M,N) = dest_pabs t in trav N end 217 else if is_pair t orelse is_atomic t then 218 SOME t 219 else if is_comb t then 220 NONE 221 else NONE 222 in 223 valOf (trav t) 224 end 225 226(*---------------------------------------------------------------------------*) 227(* Sanity check of the source program. *) 228(*---------------------------------------------------------------------------*) 229 230fun pre_check (args,body) = 231 let 232 val fv = free_vars (mk_pair(args,body)) 233 val var_type = type_of (hd (fv)) 234 handle _ => (* no argument *) 235 let fun trav M = 236 if is_plet M then trav (#1 (dest_plet M)) 237 else if is_comb M then trav (#2 (dest_comb M)) 238 else if is_pair M then trav (#1 (dest_pair M)) 239 else type_of M 240 in trav body end 241 val sane = List.all (fn x => type_of x = var_type) fv 242 in 243 (sane, var_type) 244 end 245 246(*---------------------------------------------------------------------------*) 247 248 249end (* struct *) 250