1signature match_goal =
2sig
3
4include Abbrev
5
6datatype name =
7    Assumption of string option
8  | Conclusion
9  | Anything
10
11type pattern = term quotation
12type matcher = name * pattern * bool (* whole term? *)
13
14(*
15semantics of names:
16Assumption (SOME s)
17  - must be an assumption
18  - must be the same as any other assumptions called s
19  - must be different from any other assumptions not called s
20Assumption NONE
21  - must be an assumption
22Conclusion
23  - must be the conclusion
24Anything
25  (no constraints)
26*)
27
28(*
29semantics of whole term boolean:
30  - if true then the match must be of the whole assumption/conclusion
31  - otherwise, match any subterm (i.e., like Coq's context patterns)
32*)
33
34(*
35semantics of pattern variables:
36  2 kinds of variable:
37  - free variable in goal
38  - unification variable
39      - by convention, must end, and not start, with an underscore
40  assume all free variables cannot be mistaken for unification variables
41    (if attempting to bind a non-unification variable, the match will fail)
42*)
43
44(*
45semantics of matcher list with a tactic (match_case):
46Iterate over matchers, all must match:
471. Parse quotation in context of goal (and check no free vars ending with _)
482. Attempt to match the appropriate part of the goal with the pattern (keep track which match)
49   - if failed, backtrack within current matcher;
50   - if no assumptions match, backtrack to previous matcher
513. Go to the next matcher
524. When all matchers are done:
53   - Introduce abbreviations for all unification variables
54   - Try running the tactic
55     - if it fails: undo abbreviations, backtrack
56     - if it succeeds: undo abbreviations, done
57
58semantics of (matcher list * thms_tactic) list:
59Iterate over list, taking first thing that works.
60*)
61
62type mg_tactic = (string -> thm) * (string -> term) -> tactic
63
64val match1_tac : matcher * mg_tactic -> tactic
65
66val match_tac : matcher list * mg_tactic -> tactic
67
68val first_match_tac : (matcher list * mg_tactic) list -> tactic
69
70(* TODO: maybe these should be elsewhere *)
71val kill_asm : thm -> tactic
72val drule_thm : thm -> thm -> tactic
73(* -- *)
74
75structure mg : sig
76  (* name and match whole assumption *)
77  val a     : string -> pattern -> matcher
78
79  (* match whole assumption *)
80  val ua    : pattern -> matcher
81  val au    : pattern -> matcher
82
83  (* name and match assumption subterm *)
84  val ab    : string -> pattern -> matcher
85  val ba    : string -> pattern -> matcher
86
87  (* match assumption subterm *)
88  val uab   : pattern -> matcher
89  val uba   : pattern -> matcher
90  val aub   : pattern -> matcher
91  val abu   : pattern -> matcher
92  val bau   : pattern -> matcher
93  val bua   : pattern -> matcher
94
95  (* match whole conclusion *)
96  val c     : pattern -> matcher
97
98  (* match conclusion subterm *)
99  val cb    : pattern -> matcher
100  val bc    : pattern -> matcher
101
102  (* match whole assumption or conclusion *)
103  val ac    : pattern -> matcher
104  val ca    : pattern -> matcher
105
106  (* match assumption or conclusion subterm *)
107  val acb   : pattern -> matcher
108  val abc   : pattern -> matcher
109  val bca   : pattern -> matcher
110  val cba   : pattern -> matcher
111  val cab   : pattern -> matcher
112  val bac   : pattern -> matcher
113end
114
115end
116