File ‹matcher.ML›
signature MATCHER =
sig
val check_type_term: theory -> term * term -> id_inst -> (id_inst * term) option
val check_type: theory -> typ * typ -> id_inst -> id_inst option
val update_inst: term list -> indexname -> cterm -> id_inst -> id_inst_th list
val match_list: Proof.context -> term list -> term list * cterm list ->
id_inst -> id_inst_ths list
val match_comb: Proof.context -> term list -> term * cterm -> id_inst ->
id_inst_th list
val match_head: Proof.context -> term list -> term * cterm -> id_inst ->
id_inst_th list
val match_all_head: Proof.context -> term list -> term * cterm -> id_inst ->
id_inst_th list
val match: Proof.context -> term list -> term * cterm -> id_inst ->
id_inst_th list
val rewrite_match: Proof.context -> term * cterm -> id_inst -> id_inst_th list
val rewrite_match_head:
Proof.context -> term * cterm -> id_inst -> id_inst_th list
val rewrite_match_list: Proof.context -> (bool * (term * cterm)) list ->
id_inst -> id_inst_ths list
val rewrite_match_subset:
Proof.context -> term list -> term list * cterm list -> id_inst ->
id_inst_ths list
val pre_match_type: Proof.context -> typ * typ -> bool
val pre_match_comb: Proof.context -> term * cterm -> bool
val pre_match_head': Proof.context -> term * cterm -> bool
val pre_match_all_head: Proof.context -> term * cterm -> bool
val pre_match: Proof.context -> term * cterm -> bool
val pre_match_head: Proof.context -> term * cterm -> bool
end;
functor Matcher(RewriteTable: REWRITE_TABLE) : MATCHER =
struct
fun compare_inst (((id1, inst1), _), ((id2, inst2), _)) =
eq_list (op =) (id1, id2) andalso Util.eq_env (inst1, inst2)
fun check_type_term thy (t, u) (id, (tyinst, inst)) =
let
val (T, U) = (fastype_of t, fastype_of u)
in
if T = U then SOME ((id, (tyinst, inst)), t) else
let
val tyinst' = Sign.typ_match thy (T, U) tyinst
val t' = Envir.subst_term_types tyinst' t
in
SOME ((id, (tyinst', inst)), t')
end
end
handle Type.TYPE_MATCH => NONE
fun check_type thy (T, U) (id, (tyinst, inst)) =
let
val tyinst' = if T = U then tyinst
else Sign.typ_match thy (T, U) tyinst
in
SOME (id, (tyinst', inst))
end
handle Type.TYPE_MATCH => NONE
fun is_open bd_vars u =
case bd_vars of
[] => false
| _ =>
length (inter (op aconv) bd_vars (map Free (Term.add_frees u []))) > 0
fun update_inst bd_vars ixn cu (id, inst) =
let
val u = Thm.term_of cu
in
if is_open bd_vars u then []
else [((id, Util.update_env (ixn, u) inst), Thm.reflexive cu)]
end
fun match_list ctxt bd_vars (ts, cus) instsp =
if null ts andalso null cus then [(instsp, [])]
else if null ts orelse null cus then []
else let
fun hd_first () =
let
val insts_t = match ctxt bd_vars (hd ts, hd cus) instsp
fun process_inst_t (instsp', th) =
let
val insts_ts' = match_list ctxt bd_vars (tl ts, tl cus) instsp'
in
map (apsnd (cons th)) insts_ts'
end
in
maps process_inst_t insts_t
end
fun tl_first () =
let
val insts_ts' = match_list ctxt bd_vars (tl ts, tl cus) instsp
fun process_inst_ts' (instsp', ths) =
let
val insts_t = match ctxt bd_vars (hd ts, hd cus) instsp'
in
map (apsnd (fn th => th :: ths)) insts_t
end
in
maps process_inst_ts' insts_ts'
end
in
hd_first () handle Fail "invalid pattern" => tl_first ()
end
and match_comb ctxt bd_vars (t, cu) (instsp as (_, (_, inst))) =
let
val (tf, targs) = Term.strip_comb t
val (cuf, cuargs) = Drule.strip_comb cu
val uf = Thm.term_of cuf
in
if Term.aconv_untyped (tf, uf) then
let
val instsps' = match_list ctxt bd_vars (targs, cuargs) instsp
fun process_inst (instsp', ths) =
(instsp', Util.comb_equiv (cuf, ths))
in
map process_inst instsps'
end
else if is_Var tf then
let
val (ixn, _) = Term.dest_Var tf
in
case Vartab.lookup inst ixn of
NONE =>
if subset (op aconv) (targs, bd_vars) andalso
not (has_duplicates (op aconv) targs) then
let
val cu' = cu |> Thm.term_of
|> fold Util.lambda_abstract (rev targs)
|> Thm.cterm_of ctxt
in
map (fn (instsp', _) => (instsp', Thm.reflexive cu))
(update_inst bd_vars ixn cu' instsp)
end
else
raise Fail "invalid pattern"
| SOME (_, tf') =>
let
val t' = Term.list_comb (tf', targs) |> Envir.beta_norm
in
match ctxt bd_vars (t', cu) instsp
end
end
else []
end
and match_head ctxt bd_vars (t, cu) (instsp as (_, (_, inst))) =
let
val u = Thm.term_of cu
in
if fastype_of t <> fastype_of u then [] else
case (t, u) of
(Var ((x, i), _), _) =>
(case Vartab.lookup inst (x, i) of
NONE => if x = "NUMC" andalso
not (Consts.is_const_ctxt ctxt u) then []
else if x = "FREE" andalso not (Term.is_Free u) then []
else update_inst bd_vars (x, i) cu instsp
| SOME (_, u') => match_head ctxt bd_vars (u', cu) instsp)
| (Free (a, _), Free (b, _)) =>
if a = b then [(instsp, Thm.reflexive cu)] else []
| (Const (a, _), Const (b, _)) =>
if a = b then [(instsp, Thm.reflexive cu)] else []
| (_ $ _, _) => match_comb ctxt bd_vars (t, cu) instsp
| _ => []
end
and match_all_head ctxt bd_vars (t, cu) (id, env) =
let
val u = Thm.term_of cu
val u_equivs =
if is_open bd_vars u then [(id, Thm.reflexive cu)]
else RewriteTable.get_head_equiv_with_t ctxt (id, cu) t
fun process_equiv (id', eq_u) =
let
val cu' = Thm.rhs_of eq_u
val insts_u' = match_head ctxt bd_vars (t, cu') (id', env)
fun process_inst ((id', env'), eq_th) =
((id', env'), Util.transitive_list [eq_th, meta_sym eq_u])
in
map process_inst insts_u'
end
in
maps process_equiv u_equivs
end
and match ctxt bd_vars (t, cu) (instsp as (_, (_, inst))) =
case check_type_term (Proof_Context.theory_of ctxt) (t, Thm.term_of cu) instsp of
NONE => []
| SOME (instsp', t') =>
case (t', Thm.term_of cu) of
(Var ((x, i), _), _) =>
(case Vartab.lookup inst (x, i) of
NONE => if member (op =) ["NUMC", "FREE"] x then
match_all_head ctxt bd_vars (t', cu) instsp'
else
update_inst bd_vars (x, i) cu instsp'
| SOME (_, u') => match ctxt bd_vars (u', cu) instsp')
| (Abs (_, T, t'), Abs (x, U, _)) => (
case check_type (Proof_Context.theory_of ctxt) (T, U) instsp' of
NONE => []
| SOME (instsp'' as (_, (tyinst', _))) =>
let
val (cv, cu') = Thm.dest_abs_global cu
val v = Thm.term_of cv
val t'' = Envir.subst_term_types tyinst' t'
val t_free = Term.subst_bound (v, t'')
val insts' = match ctxt (v :: bd_vars) (t_free, cu') instsp''
fun process_inst (inst', th') =
(inst', Thm.abstract_rule x cv th')
in
map process_inst insts'
end)
| _ =>
(match_all_head ctxt bd_vars (t', cu) instsp')
|> distinct compare_inst
fun rewrite_match_gen at_head ctxt (t, cu) (id, env) =
if at_head then
case check_type_term (Proof_Context.theory_of ctxt) (t, Thm.term_of cu) (id, env) of
NONE => []
| SOME ((id, env), t) => match_head ctxt [] (t, cu) (id, env)
else
match ctxt [] (t, cu) (id, env)
val rewrite_match = rewrite_match_gen false
val rewrite_match_head = rewrite_match_gen true
fun rewrite_match_list ctxt pairs instsp =
case pairs of
[] => [(instsp, [])]
| (at_head, (t, cu)) :: pairs' =>
let
val insts_t = rewrite_match_gen at_head ctxt (t, cu) instsp
fun process_inst_t (instsp', th) =
let
val insts_ts' = rewrite_match_list ctxt pairs' instsp'
in
map (apsnd (cons th)) insts_ts'
end
in
maps process_inst_t insts_t
end
fun rewrite_match_subset ctxt bd_vars (ts, cus) instsp =
case ts of
[] => [(instsp, [])]
| t :: ts' =>
let
fun match_i i =
map (pair i) (match ctxt bd_vars (t, nth cus i) instsp)
fun process_match_i (i, (instsp', th)) =
let
val insts_ts' = rewrite_match_subset
ctxt bd_vars (ts', nth_drop i cus) instsp'
in
map (apsnd (cons th)) insts_ts'
end
in
(0 upto (length cus - 1))
|> maps match_i |> maps process_match_i
end
handle Fail "invalid pattern" =>
if length ts' > 0 andalso Term_Ord.term_ord (t, hd ts') = LESS then
rewrite_match_subset ctxt bd_vars (ts' @ [t], cus) instsp
else raise Fail "rewrite_match_subset: invalid pattern"
fun pre_match_type ctxt (T, U) =
let
val thy = Proof_Context.theory_of ctxt
val _ = Sign.typ_match thy (T, U) Vartab.empty
in
true
end
handle Type.TYPE_MATCH => false
fun pre_match_comb ctxt (t, cu) =
let
val (tf, targs) = Term.strip_comb t
val (cuf, cuargs) = Drule.strip_comb cu
val uf = Thm.term_of cuf
in
is_Var tf orelse (Term.aconv_untyped (tf, uf) andalso
length targs = length cuargs andalso
forall (pre_match ctxt) (targs ~~ cuargs))
end
and pre_match_head' ctxt (t, cu) =
let
val u = Thm.term_of cu
in
case (t, u) of
(Var ((x, _), T), _) =>
if Term.is_open u then false
else if not (pre_match_type ctxt (T, fastype_of u)) then false
else if x = "NUMC" then Consts.is_const_ctxt ctxt u
else if x = "FREE" then Term.is_Free u
else true
| (Free (a, T), Free (b, U)) =>
(a = b andalso pre_match_type ctxt (T, U))
| (Const (a, T), Const (b, U)) =>
(a = b andalso pre_match_type ctxt (T, U))
| (_ $ _, _) => pre_match_comb ctxt (t, cu)
| _ => false
end
and pre_match_all_head ctxt (t, cu) =
let
val thy = Proof_Context.theory_of ctxt
val u = Thm.term_of cu
val tyinst = Sign.typ_match thy (fastype_of t, fastype_of u) Vartab.empty
val t' = Envir.subst_term_types tyinst t
in
if Term.is_open u then pre_match_head' ctxt (t', cu)
else let
val u_equivs =
(RewriteTable.get_head_equiv_with_t ctxt ([], cu) t')
|> map snd |> map Thm.rhs_of
in
exists (fn cu' => pre_match_head' ctxt (t', cu')) u_equivs
end
end
handle Type.TYPE_MATCH => false
and pre_match ctxt (t, cu) =
let
val u = Thm.term_of cu
in
case (t, u) of
(Var ((x, _), T), _) =>
if Term.is_open u then false
else if not (pre_match_type ctxt (T, fastype_of u)) then false
else if member (op =) ["NUMC", "FREE"] x then
pre_match_all_head ctxt (t, cu)
else true
| (Abs (_, T, t'), Abs (_, U, _)) =>
if not (pre_match_type ctxt (T, U)) then false
else let
val (cv, cu') = Thm.dest_abs_global cu
val t'' = subst_bound (Thm.term_of cv, t')
in
pre_match ctxt (t'', cu')
end
| (Bound i, Bound j) => (i = j)
| (_, _) => pre_match_all_head ctxt (t, cu)
end
fun pre_match_head ctxt (t, cu) =
let
val thy = Proof_Context.theory_of ctxt
val u = Thm.term_of cu
val tyinst = Sign.typ_match thy (fastype_of t, fastype_of u) Vartab.empty
val t' = Envir.subst_term_types tyinst t
in
pre_match_head' ctxt (t', cu)
end
handle Type.TYPE_MATCH => false
end