1(* =====================================================================
2 * FILE          : traverse.sig
3 * DESCRIPTION   : A programmable term traversal engine for hol90
4 *
5 * AUTHOR        : Donald Syme
6 * ===================================================================== *)
7
8signature Traverse =
9sig
10  include Abbrev
11
12   (* ---------------------------------------------------------------------
13    * type context
14    *
15    * Each reducer collects the working context on its own.
16    * A context object is the current state of a single reducer.
17    * ---------------------------------------------------------------------*)
18
19  type context = exn (* well known SML hack to allow any kind of data *)
20
21   (* ---------------------------------------------------------------------
22    * Reducers
23    *   These are the things that get applied to terms during
24    * traversal.  They prove theorems which state that the
25    * current term reduces to a related
26    *
27    * Each reducer manages its own storage of the working context (of one
28    * of the forms above - Nb. in SML exceptions are able to contain
29    * any kind of data, so contexts can be any appropriate format.  This
30    * is a hack, but it is the best way to get good data hiding in SML
31    * without resorting to functors)
32    *
33    * The fields of a reducer are:
34    *
35    * apply:  This is the reducer itself.  The arguments passed by
36    *   the traversal engine to the reduce routine are:
37    *    solver:
38    *      A continuation function, to be used if the reducer needs to
39    *      solve some side conditions and want to continue traversing
40    *      in order to do so.  The continuation invokes traversal
41    *      under equality, then calls EQT_ELIM.
42    *
43    *      At the moment the continuation is primarily designed to
44    *      be used to solve side conditions in context.
45    *
46    *      Note that this function is *not* the same as
47    *      the congruence side condition solver.
48    *
49    *    context:
50    *      The reducer's current view of the context, as
51    *      collected by its "addcontext" function.
52    *    term list:
53    *      The current side condition stack, which grows as nested calls
54    *      to the solver are made.
55    *
56    * conv:
57    *   A continuation function, to be used if the reducer
58    *   wants to continue traversing. The continuation invokes traversal
59    *   under equality. Similar to solver, but does not call EQT_ELIM.
60    *
61    * addcontext: routine is invoked every time more context is added
62    *   to the current environment by virtue of congruence routines.
63    *
64    * initial:  The inital context.
65    * ---------------------------------------------------------------------*)
66
67  datatype reducer = REDUCER of {
68         name : string option,
69         initial: context,
70         addcontext : context * thm list -> context,
71         apply: {solver:term list -> term -> thm,
72                 conv: term list -> term -> thm,
73                 context: context,
74                 stack:term list,
75                 relation : (term * (term -> thm))} -> conv
76       }
77
78  val dest_reducer : reducer ->
79        {name : string option,
80         initial: context,
81         addcontext : context * thm list -> context,
82         apply: {solver:term list -> term -> thm,
83                 conv: term list -> term -> thm,
84                 context: context,
85                 stack:term list,
86                 relation : (term * (term -> thm))} -> conv}
87
88  val addctxt : thm list -> reducer -> reducer
89
90 (* ----------------------------------------------------------------------
91     TRAVERSE : {rewriters: reducer list,
92                 dprocs: reducer list,
93                 travrules: travrules,
94                 relation: term,
95                 limit : int option}
96                -> thm list -> conv
97
98     Implements a procedure which tries to prove a term is related
99     to a (simpler) term by the relation given in the travrules.
100     This is done by traversing the term, applying the
101     procedures specified in the travrules at certain subterms.
102     The traversal strategy is similar to TOP_DEPTH_CONV.
103
104     The traversal has to be justified by congruence rules.
105     These are also in the travrules.  See "Congprocs" for a more
106     detailed description of congruence rules.
107
108     In the case of rewriting and simplification, the relation used is
109     equality (--`$=`--).  However traversal can also be used with
110     other congruences and preorders.
111
112     The behaviour of TRAVERSE depends almost totally on what
113     is contained in the input travrules.
114
115     The theorem list is a set of theorems to add initially as context
116     to the traversal.
117
118     FAILURE CONDITIONS
119
120     TRAVERSE never fails, though it may diverge or raise an exception
121     indicating that a term is unchanged by the traversal.
122
123     Bad congruence rules may cause very strange behaviour.
124    ---------------------------------------------------------------------- *)
125
126   type traverse_data = {rewriters: reducer list,
127                         limit : int option,
128                         dprocs: reducer list,
129                         travrules: Travrules.travrules,
130                         relation: term};
131
132   val TRAVERSE : traverse_data -> thm list -> conv
133
134end (* sig *)
135