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