1signature RW =
2sig
3  include Abbrev
4
5  (* Simplification sets *)
6  type simpls
7  val empty_simpls : simpls
8  val dest_simpls  : simpls -> {congs:thm list, rws:thm list}
9  val mk_simpls    : (thm -> thm) -> thm -> thm list
10  val MK_RULES     : thm -> thm list
11  val add_rws      : simpls -> thm list -> simpls
12  val add_congs    : simpls -> thm list -> simpls
13  val join_simpls  : simpls -> simpls -> simpls
14  val std_simpls   : simpls
15  val pp_simpls    : simpls PP.pprinter
16  val embedded_ref : (term -> term -> bool) ref
17
18  (* The implicit simplification set *)
19  val add_implicit_congs  : thm list -> unit
20  val add_implicit_rws    : thm list -> unit
21  val add_implicit_simpls : simpls -> unit
22  val implicit_simpls : unit -> simpls
23  val set_implicit_simpls : simpls -> unit
24
25  (* Solvers and monitoring *)
26  val solver_err : unit -> 'a
27  val rw_solver : simpls -> thm list -> term -> thm
28  val std_solver : 'a -> thm list -> term -> thm
29  val always_fails : 'a -> 'b -> 'c -> 'd
30
31  (* Tells whether to add context to the simpls as term is traversed *)
32  datatype context_policy = ADD | DONT_ADD
33
34  (* The atomic conditional term rewriter. *)
35  val RW_STEP:{context:'a * context_policy, simpls:simpls,
36               prover:simpls -> 'a -> term -> thm}
37               -> term -> thm
38
39  type cntxt_solver = {context:thm list * context_policy,
40                       simpls:simpls,
41                       prover:simpls -> thm list -> term -> thm};
42
43  type strategy = (cntxt_solver -> term -> thm)
44               -> (cntxt_solver -> term -> thm)
45
46  val DEPTH   : strategy
47  val REDEPTH : strategy
48  val TOP_DEPTH : strategy
49  val ONCE_DEPTH : strategy
50  val RATOR : strategy
51  val RAND  : strategy
52  val ABST  : strategy
53
54  datatype repetitions = Once | Fully | Special of strategy
55  datatype rules   = Default of thm list
56                   | Pure of thm list
57                   | Simpls of simpls * thm list
58  datatype context = Context of thm list * context_policy
59  datatype congs   = Congs of thm list
60  datatype solver  = Solver of simpls -> thm list -> term -> thm
61
62  (* Parameterized rewriters for terms, theorems, and goals *)
63  val Rewrite      :repetitions -> rules*context*congs*solver -> conv
64  val REWRITE_RULE :repetitions -> rules*context*congs*solver -> thm -> thm
65  val ASM_REWRITE_RULE:repetitions -> rules*context*congs*solver -> thm -> thm
66  val REWRITE_TAC     :repetitions -> rules*context*congs*solver -> tactic
67  val ASM_REWRITE_TAC :repetitions -> rules*context*congs*solver -> tactic
68
69
70  (* Specialized rewriters for different types *)
71  (* Terms *)
72
73  val CRW_CONV          : thm list -> term -> thm
74  val RW_CONV           : thm list -> term -> thm
75  val PURE_RW_CONV      : thm list -> term -> thm
76  val ONCE_RW_CONV      : thm list -> term -> thm
77  val PURE_ONCE_RW_CONV : thm list -> term -> thm
78
79
80  (* Theorems *)
81  val CRW_RULE          : thm list -> thm -> thm
82  val RW_RULE           : thm list -> thm -> thm
83  val PURE_RW_RULE      : thm list -> thm -> thm
84  val ONCE_RW_RULE      : thm list -> thm -> thm
85  val PURE_ONCE_RW_RULE : thm list -> thm -> thm
86
87  val ASM_CRW_RULE      : thm list -> thm -> thm
88  val ASM_RW_RULE       : thm list -> thm -> thm
89  val PURE_ASM_RW_RULE  : thm list -> thm -> thm
90  val ONCE_ASM_RW_RULE  : thm list -> thm -> thm
91  val PURE_ONCE_ASM_RW_RULE : thm list -> thm -> thm
92
93
94  (* Goals *)
95  val RW_TAC          : thm list -> tactic
96  val CRW_TAC         : thm list -> tactic
97  val PURE_RW_TAC     : thm list -> tactic
98  val ONCE_RW_TAC     : thm list -> tactic
99  val PURE_ONCE_RW_TAC: thm list -> tactic
100
101  val ASM_RW_TAC      : thm list -> tactic
102  val ASM_CRW_TAC     : thm list -> tactic
103  val PURE_ASM_RW_TAC : thm list -> tactic
104  val ONCE_ASM_RW_TAC : thm list -> tactic
105  val PURE_ONCE_ASM_RW_TAC : thm list -> tactic
106
107  (* Folding in beta-conversion and a user-given standard simpset *)
108  val Simpl : tactic -> thm list -> thm list -> tactic
109
110end
111