Skip to content
Permalink
Browse files

Add an initial implementation of match_goal

This is a tactic builder that does automatic logic-programming-style
search over (sub)terms in the assumptions and conclusion of a goal
ensuring certain patterns match and that a given tactic (which can refer
to the terms and assumptions named by the pattern) succeeds.

Work with Jack Gallagher, and inspired by a similar facility in Coq.
  • Loading branch information
xrchz committed Apr 10, 2016
1 parent e648a40 commit 3d4f44c9c46ed67a003c69a7957bf570b24d3a07
Showing with 395 additions and 0 deletions.
  1. +113 −0 src/1/match_goal.sig
  2. +207 −0 src/1/match_goal.sml
  3. +75 −0 src/1/selftest.sml
@@ -0,0 +1,113 @@
signature mg = sig
type pat = Abbrev.term Abbrev.quotation
type matcher = string * pat * bool

(* name and match whole assumption *)
val a : string -> pat -> matcher

(* match whole assumption *)
val ua : pat -> matcher
val au : pat -> matcher

(* name and match assumption subterm *)
val ab : string -> pat -> matcher
val ba : string -> pat -> matcher

(* match assumption subterm *)
val uab : pat -> matcher
val uba : pat -> matcher
val aub : pat -> matcher
val abu : pat -> matcher
val bau : pat -> matcher
val bua : pat -> matcher

(* match whole conclusion *)
val c : pat -> matcher

(* match conclusion subterm *)
val cb : pat -> matcher
val bc : pat -> matcher

(* match whole assumption or conclusion *)
val ac : pat -> matcher
val ca : pat -> matcher

(* match assumption or conclusion subterm *)
val acb : pat -> matcher
val abc : pat -> matcher
val bca : pat -> matcher
val cba : pat -> matcher
val cab : pat -> matcher
val bac : pat -> matcher
end

signature match_goal =
sig

include Abbrev

type matcher = string * term quotation * bool

(*
name of assumption pattern whole term?
string * term quotation * bool
semantics of names:
(any normal string, e.g., "H") - must be an assumption
"_" -> must be assumption, but don't care about its name - can match other different or same
"H2" -> must be an assumption, must be different from "H"
"H" -> must be an assumption, and the same one as "H"
"?" -> must be the conclusion
"" -> match anything, don't care about name or previous matches
*)

(*
semantics of whole term boolean:
- if true then the match must be of the whole assumption/conclusion
- otherwise, match any subterm (i.e., like Coq's context patterns)
*)

(*
semantics of pattern variables:
2 kinds of variable:
- free variable in goal
- unification variable
- by convention, must end, and not start, with an underscore
assume all free variables cannot be mistaken for unification variables
(if attempting to bind a non-unification variable, the match will fail)
*)

(*
semantics of matcher list with a tactic (match_case):
Iterate over matchers, all must match:
1. Parse quotation in context of goal (and check no free vars ending with _)
2. Attempt to match the appropriate part of the goal with the pattern (keep track which match)
- if failed, backtrack within current matcher;
- if no assumptions match, backtrack to previous matcher
3. Go to the next matcher
4. When all matchers are done:
- Introduce abbreviations for all unification variables
- Try running the tactic
- if it fails: undo abbreviations, backtrack
- if it succeeds: undo abbreviations, done
semantics of (matcher list * thms_tactic) list:
Iterate over list, taking first thing that works.
*)

type mg_tactic = (string -> thm) * (string -> term) -> tactic

val match1_tac : matcher * mg_tactic -> tactic

val match_tac : matcher list * mg_tactic -> tactic

val match_all_tac : (matcher list * mg_tactic) list -> tactic

(* TODO: maybe these should be elsewhere *)
val kill_asm : thm -> tactic
val drule_thm : thm -> thm -> tactic
(* -- *)

structure mg : mg

end
@@ -0,0 +1,207 @@
structure match_goal :> match_goal =
struct

open HolKernel boolLib Streams

fun Redblackmap_contains (m,v) =
let
exception found
val _ = Redblackmap.app (fn (_,v') => if v = v' then raise found else ()) m
in false end
handle found => true

fun empty_stream() = raise end_of_stream

fun stream_append_list x = List.foldr (uncurry stream_append) empty_stream x

val ERR = Feedback.mk_HOL_ERR"match_goal";

type matcher = string * term quotation * bool

(* (name, assumption number) *)
type named_thms = (string, int) Redblackmap.dict
val (empty_named_thms:named_thms) = Redblackmap.mkDict String.compare;

(* If you want to be able to treat certain type variables as constants (e.g.,
if they are in the goal) then you need to keep track of the avoid_tys/tyIds
thing that raw_match uses. But we are not doing that. *)
type named_tms =
((term,term) subst) * ((hol_type,hol_type) subst)

val empty_named_tms : named_tms = ([],[])

type data = named_thms * named_tms

datatype name =
Assumption of string option
| Conclusion
| Anything

fun parse_name "" = Anything
| parse_name "?" = Conclusion
| parse_name "_" = Assumption NONE
| parse_name s = Assumption (SOME s)

fun is_underscore v =
case total dest_var v of NONE
=> raise(ERR"umatch""unexpected non-variable binding") (* should not happen *)
| SOME (s,_) => String.isPrefix "_" s

val is_uvar = String.isSuffix "_" o #1 o dest_var

fun umatch avoid_tms ((tmS,tyS):named_tms) pat ob : named_tms =
let
val ((tmS',tmIds'),(tyS',_)) = raw_match [] avoid_tms pat ob (tmS,tyS)
handle HOL_ERR _ => raise end_of_stream
val tmS'' = List.filter (not o is_underscore o #redex) tmS'
val _ = assert_exn (List.all (is_uvar o #redex)) tmS'' end_of_stream
val _ = assert_exn (curry HOLset.isSubset tmIds') avoid_tms end_of_stream
in
(tmS'', tyS')
end

fun umatch_subterms avoid_tms (ntms:named_tms) pat ob : unit -> named_tms stream =
stream_append
(fn () => Stream(umatch avoid_tms ntms pat ob,empty_stream))
(fn () =>
(case dest_term ob of
COMB(t1,t2) =>
stream_append
(umatch_subterms avoid_tms ntms pat t1)
(umatch_subterms avoid_tms ntms pat t2)
| LAMB(v,b) =>
umatch_subterms (HOLset.add(avoid_tms,v)) ntms pat b
| _ => empty_stream)
())

fun preprocess_matcher fvs =
fn (nm,q,b):matcher => (parse_name nm, Parse.parse_in_context fvs q, b)

type mg_tactic = (string -> thm) * (string -> term) -> tactic

fun match_single fvs ((asl,w):goal)
((nm,pat,whole):name * term * bool) ((nths,ntms):data) : unit -> data stream =
let
fun add_nth NONE _ = SOME nths
| add_nth (SOME l) i =
(case Redblackmap.peek(nths,l) of
NONE =>
if Redblackmap_contains(nths,i)
then NONE
else SOME (Redblackmap.insert(nths,l,i))
| SOME j => if i = j then SOME nths else NONE)

fun protect f NONE = K empty_stream
| protect f (SOME x) = f x

fun umatch_sing nths w =
(fn() => Stream ((nths, umatch fvs ntms pat w),empty_stream))
fun umatch_many nths w =
stream_map (fn ntms => (nths,ntms)) (umatch_subterms fvs ntms pat w)
in
case nm of
Conclusion =>
if whole then
umatch_sing nths w
else
umatch_many nths w
| Assumption l =>
if whole then
stream_append_list (Lib.mapi (protect umatch_sing o add_nth l) asl)
else
stream_append_list (Lib.mapi (protect umatch_many o add_nth l) asl)
| Anything =>
if whole then
stream_append_list (List.map (umatch_sing nths) (w::asl))
else
stream_append_list (List.map (umatch_many nths) (w::asl))
(*
(el 2 (List.map (umatch_many nths) (w::asl))) ()
val avoid_tms = fvs
val ob = el 2 (w::asl)
umatch_subterms fvs ntms pat (el 2 (w::asl))
val
el 2 (w::asl)
pat
*)
end

val tr1 = Substring.string o Substring.trimr 1 o Substring.full

fun match_tac (ms:matcher list,mtac:mg_tactic) (g as (asl,w):goal) : goal list * validation =
let
fun try_tactic ((thms,tms):data) : (unit -> (goal list * validation) stream) =
let
fun lookup_assum s =
let
val i = Redblackmap.find(thms,s)
val tm = List.nth(#1 g,i)
in ASSUME tm end
val s =
case tms of (tmS,tyS) =>
#1 (norm_subst ((tmS,empty_tmset),(tyS,[])))
|> List.map (fn {redex,residue} => (tr1(#1(dest_var redex)),residue))
val tac = mtac (lookup_assum,Lib.C assoc s)
val r = tac g
in
(fn()=>Stream (r,empty_stream))
end
handle HOL_ERR _ => empty_stream

fun search [] d = try_tactic d
| search (m::ms) d = stream_flat (stream_map (search ms) (m d))

val fvs = FVL (w::asl) empty_tmset

val matches = map (match_single fvs g o preprocess_matcher (HOLset.listItems fvs)) ms
in
(case search matches (empty_named_thms,empty_named_tms) () of
Stream (x,_) => x)
handle end_of_stream => raise ERR "match_tac" "no match"
end

val match_all_tac = FIRST o List.map match_tac

fun match1_tac (x,t) = match_tac ([x],t)

fun kill_asm th = first_x_assum((K ALL_TAC) o assert (equal (concl th) o concl))

fun drule_thm th = mp_tac o Lib.C MATCH_MP th

structure mg :> mg = struct
type matcher = matcher
type pat = term quotation

fun a nm p = (nm,p,true)

fun ua p = ("_",p,true)
val au = ua

fun ab nm p = (nm,p,false)
val ba = ab

fun uab p = ("_",p,false)
val uba = uab
val aub = uab
val abu = uab
val bau = uab
val bua = uab

fun c p = ("?",p,true)

fun cb p = ("?",p,false)
val bc = cb

fun ac p = ("",p,true)
val ca = ac

fun acb p = ("",p,false)
val abc = acb
val bca = acb
val cba = acb
val cab = acb
val bac = acb
end

end

0 comments on commit 3d4f44c

Please sign in to comment.
You can’t perform that action at this time.