1(* =====================================================================
2 * FILE          : $Id$
3 * DESCRIPTION   : A programmable term traversal engine for hol90
4 *
5 * AUTHOR        : Donald Syme
6 *                 Based loosely on original HOL rewriting by
7 *                 Larry Paulson et al.
8 * ===================================================================== *)
9
10
11(* =====================================================================
12 * Traversal (opening) Rules
13 * =====================================================================*)
14
15structure Travrules :> Travrules =
16struct
17
18open HolKernel Drule Psyntax liteLib Trace Opening;
19
20fun WRAP x = STRUCT_WRAP "Travrules" x;
21fun ERR x = STRUCT_ERR "Travrules" x;
22
23
24   (* ---------------------------------------------------------------------
25    * preorders
26    * ---------------------------------------------------------------------*)
27
28  val equality = boolSyntax.equality;
29
30  datatype preorder = PREORDER of term
31                                  * (thm -> thm -> thm)
32                                  * ({Rinst:term,arg:term} -> thm);
33
34   fun find_relation rel  = let
35     fun f ((h as PREORDER (cid,_,_))::t) = if Opening.samerel cid rel then h
36                                            else f t
37       | f [] = ERR("find_relation","relation not found")
38   in
39     f
40   end;
41
42   fun ARB_TRANS thm c1 c2 = MATCH_MP thm (CONJ c1 c2);
43
44   fun mk_preorder (TRANS_THM,REFL_THM) = let
45     fun refl {Rinst,arg} = PART_MATCH rator REFL_THM (mk_comb(Rinst,arg))
46   in
47     PREORDER (rator(rator(snd(boolSyntax.strip_forall(concl REFL_THM)))),
48               ARB_TRANS TRANS_THM,
49               refl)
50   end
51
52   (* ---------------------------------------------------------------------
53    * travrules objects and basic operations on them
54    * merge_travrules:
55    * The order of congprocs is v. significant - the list in the object
56    * gets applied left to right.  Congprocs from
57    * the second of two travsets have
58    * priority - hence the "foldl" below.
59    * ---------------------------------------------------------------------*)
60
61   datatype travrules = TRAVRULES of {
62       relations : preorder list,
63       congprocs : congproc list,
64       weakenprocs : congproc list
65    };
66
67   fun dest(TRAVRULES x)  = x;
68   val gen_mk_travrules = TRAVRULES
69
70   fun rel_of_preorder (PREORDER(r,_,_)) = r
71
72   fun merge_travrules tl = let
73     val ts = map dest tl
74     fun uniquify l = let
75       val sorted = Listsort.sort (inv_img_cmp rel_of_preorder Term.compare) l
76       fun recurse acc [] = acc
77         | recurse acc [h] = h::acc
78         | recurse acc (h1::(rest as h2::t)) =
79           if samerel (rel_of_preorder h1) (rel_of_preorder h2) then
80             recurse acc rest
81           else
82             recurse (h1::acc) rest
83     in
84       recurse [] sorted
85     end
86   in
87     TRAVRULES {relations=uniquify (flatten (map #relations ts)),
88                congprocs=foldl (op @) [] (map #congprocs ts),
89                weakenprocs=flatten (map #weakenprocs ts)}
90     end;
91
92
93(* ---------------------------------------------------------------------
94 * equality_travrules
95 * ---------------------------------------------------------------------*)
96
97val EQ_preorder = let
98  fun eqrefl {Rinst,arg} = REFL arg
99in
100  PREORDER(boolSyntax.equality,TRANS,eqrefl)
101end
102val EQ_tr = gen_mk_travrules
103  {relations=[EQ_preorder],
104   congprocs=[Opening.EQ_CONGPROC],
105   weakenprocs=[]}
106
107fun cong2proc rels th = let
108  open Opening
109  val r = rel_of_congrule th
110  val PREORDER(_,_,refl) = find_relation r rels
111in
112  CONGPROC refl th
113end
114
115fun mk_travrules relns congs =
116    TRAVRULES {relations=relns,
117               congprocs=map (cong2proc relns) congs,
118               weakenprocs=[]}
119
120
121end (* struct *)
122