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