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