File ‹items.ML›
val TY_NULL = "NULL"
val TY_EQ = "EQ"
val TY_VAR = "VAR"
val TY_PROP = "PROP"
val TY_TERM = "TERM"
val TY_PROPERTY = "PROPERTY"
datatype raw_item = Handler of term list * term * thm
| Fact of string * term list * thm
type box_item = {uid: int, id: box_id, sc: int, ty_str: string,
tname: cterm list, prop: thm}
signature BOXITEM =
sig
val var_to_fact: term -> raw_item
val term_to_fact: term -> raw_item
val is_fact_raw: raw_item -> bool
val match_ty_str_raw: string -> raw_item -> bool
val match_ty_strs_raw: string list -> raw_item -> bool
val get_tname_raw: raw_item -> term list
val get_thm_raw: raw_item -> thm
val is_handler_raw: raw_item -> bool
val dest_handler_raw: raw_item -> term list * term * thm
val eq_ritem: raw_item * raw_item -> bool
val instantiate: (cterm * cterm) list -> raw_item -> raw_item
val obtain_variant_frees:
Proof.context * raw_item list -> Proof.context * (cterm * cterm) list
val null_item: box_item
val item_with_id: box_id -> box_item -> box_item
val item_with_incr: box_item -> box_item
val item_replace_incr: box_item -> box_item
val eq_item: box_item * box_item -> bool
val match_ty_str: string -> box_item -> bool
val match_ty_strs: string list -> box_item -> bool
val merged_id: Proof.context -> box_item list -> box_id
val mk_box_item: Proof.context -> int * box_id * int * raw_item -> box_item
end;
functor BoxItem(UtilBase: BASIC_UTIL_BASE) : BOXITEM =
struct
fun var_to_fact t = Fact (TY_VAR, [t], UtilBase.true_th)
fun term_to_fact t = Fact (TY_TERM, [t], UtilBase.true_th)
fun is_fact_raw ritem =
case ritem of Fact _ => true | _ => false
fun match_ty_str_raw s ritem =
case ritem of Fact (ty_str, _, _) => s = "" orelse ty_str = s | _ => false
fun match_ty_strs_raw slist ritem =
case ritem of Fact (ty_str, _, _) => member (op =) slist ty_str | _ => false
fun get_tname_raw ritem =
case ritem of Fact (_, ts, _) => ts | _ => raise Fail "get_tname_raw"
fun get_thm_raw ritem =
case ritem of Fact (_, _, th) => th | _ => raise Fail "get_thm_raw"
fun is_handler_raw ritem =
case ritem of Handler _ => true | _ => false
fun dest_handler_raw ritem =
case ritem of Handler (vars, t, ex_th) => (vars, t, ex_th)
| _ => raise Fail "dest_handler_raw: wrong type"
fun eq_ritem (ritem1, ritem2) =
case ritem1 of
Fact (ty1, ts1, th1) =>
(case ritem2 of
Fact (ty2, ts2, th2) =>
ty1 = ty2 andalso eq_list (op aconv) (ts1, ts2) andalso
Thm.eq_thm_prop (th1, th2)
| _ => false)
| Handler (vars1, t1, ex_th1) =>
(case ritem2 of
Fact _ => false
| Handler (vars2, t2, ex_th2) =>
eq_list (op aconv) (vars1, vars2) andalso t1 aconv t2 andalso
Thm.eq_thm_prop (ex_th1, ex_th2))
fun obtain_variant_frees (ctxt, ritems) =
let
val all_vars =
ritems |> filter (match_ty_str_raw TY_VAR) |> maps get_tname_raw
|> filter is_Free |> map dest_Free
|> filter (Util.is_just_internal o fst)
val all_vars' =
all_vars |> map (fn (x, T) => (Name.dest_internal x, T))
|> Variable.variant_frees ctxt []
val subst = map (apply2 (Thm.cterm_of ctxt o Free)) (all_vars ~~ all_vars')
in
(fold Util.declare_free_term (map Free all_vars') ctxt, subst)
end
fun instantiate subst ritem =
let
val subst_fun = Term.subst_atomic (map (apply2 Thm.term_of) subst)
in
case ritem of
Handler (vars, t, ex_th) =>
Handler (map subst_fun vars, subst_fun t,
Util.subst_thm_atomic subst ex_th)
| Fact (ty_str, tname, th) =>
Fact (ty_str, map subst_fun tname, Util.subst_thm_atomic subst th)
end
val null_item = {uid = 0, id = [], sc = 0, ty_str = TY_NULL,
tname = [], prop = UtilBase.true_th}
fun item_with_id id {uid, sc, ty_str, tname, prop, ...} =
{uid = uid, id = id, sc = sc, ty_str = ty_str, tname = tname, prop = prop}
fun item_with_incr item =
item_with_id (BoxID.add_incr_id (#id item)) item
fun item_replace_incr item =
item_with_id (BoxID.replace_incr_id (#id item)) item
fun eq_item (item1, item2) = (#uid item1 = #uid item2)
fun match_ty_str s {ty_str, ...} = (s = "" orelse s = ty_str)
fun match_ty_strs slist {ty_str, ...} = member (op =) slist ty_str
fun merged_id ctxt items =
case items of
[] => []
| {id, ...} :: items' => BoxID.merge_boxes ctxt (id, merged_id ctxt items')
fun mk_box_item ctxt (uid, id, sc, ritem) =
case ritem of
Handler _ => raise Fail "mk_box_item: ritem must be Fact"
| Fact (ty_str, ts, prop) =>
{uid = uid, id = id, sc = sc, ty_str = ty_str,
tname = map (Thm.cterm_of ctxt) ts, prop = prop}
end
type item_matcher = {
pre_match: term -> box_item -> Proof.context -> bool,
match: term -> box_item -> Proof.context -> id_inst -> id_inst_th list
}
type item_output = Proof.context -> term list * thm -> string
type item_io_info = {
prop_matchers: (item_matcher * serial) list,
typed_matchers: (item_matcher * serial) list,
term_fn: ((term list -> term list) * serial) option,
output_fn: (item_output * serial) option,
shadow_fn: ((Proof.context -> box_id -> term list * cterm list -> bool) * serial) option
}
datatype match_arg = PropMatch of term
| TypedMatch of string * term
| TypedUniv of string
| PropertyMatch of term
| WellFormMatch of term * term
type prfstep_filter = Proof.context -> id_inst -> bool
signature ITEM_IO =
sig
val pat_of_match_arg: match_arg -> term
val subst_arg: Type.tyenv * Envir.tenv -> match_arg -> match_arg
val assert_valid_arg: match_arg -> unit
val check_ty_str: string -> match_arg -> bool
val is_ordinary_match: match_arg -> bool
val is_side_match: match_arg -> bool
val add_item_type:
string * (term list -> term list) option *
item_output option *
(Proof.context -> box_id -> term list * cterm list -> bool) option ->
theory -> theory
val add_prop_matcher: string * item_matcher -> theory -> theory
val add_typed_matcher: string * item_matcher -> theory -> theory
val get_io_info: theory -> string -> item_io_info
val get_prop_matchers: theory -> string -> item_matcher list
val get_typed_matchers: theory -> string -> item_matcher list
val prop_matcher: item_matcher
val term_prop_matcher: item_matcher
val null_eq_matcher: item_matcher
val term_typed_matcher: item_matcher
val eq_tname_typed_matcher: item_matcher
val null_property_matcher: item_matcher
val term_property_matcher: item_matcher
val pre_match_arg: Proof.context -> match_arg -> box_item -> bool
val match_arg: Proof.context -> match_arg -> box_item -> id_inst ->
id_inst_th list
val no_rewr_terms: term list -> term list
val rewr_terms_of_item: Proof.context -> string * term list -> term list
val output_prop_fn: item_output
val string_of_item_info: Proof.context -> string * term list * thm -> string
val add_basic_item_io: theory -> theory
val string_of_raw_item: Proof.context -> raw_item -> string
val string_of_item: Proof.context -> box_item -> string
val trace_ritem: Proof.context -> string -> raw_item -> unit
val trace_item: Proof.context -> string -> box_item -> unit
val trace_ritems: Proof.context -> string -> raw_item list -> unit
val trace_items: Proof.context -> string -> box_item list -> unit
end;
functor ItemIO(
structure Matcher: MATCHER;
structure Property: PROPERTY;
structure PropertyData: PROPERTY_DATA
structure RewriteTable: REWRITE_TABLE;
structure UtilBase: UTIL_BASE;
structure UtilLogic: UTIL_LOGIC
) : ITEM_IO =
struct
fun add_prop_matcher_to_info
mtch {prop_matchers, typed_matchers, term_fn, output_fn, shadow_fn} : item_io_info =
{prop_matchers = (mtch, serial ()) :: prop_matchers, typed_matchers = typed_matchers,
term_fn = term_fn, output_fn = output_fn, shadow_fn = shadow_fn}
fun add_typed_matcher_to_info
mtch {prop_matchers, typed_matchers, term_fn, output_fn, shadow_fn} : item_io_info =
{prop_matchers = prop_matchers, typed_matchers = (mtch, serial ()) :: typed_matchers,
term_fn = term_fn, output_fn = output_fn, shadow_fn = shadow_fn}
structure Data = Theory_Data
(
type T = item_io_info Symtab.table
val empty = Symtab.empty
val merge = Symtab.join (fn _ =>
fn ({prop_matchers = pm1, typed_matchers = tm1, term_fn = tf1, output_fn = of1,
shadow_fn = sf1},
{prop_matchers = pm2, typed_matchers = tm2, term_fn = tf2, output_fn = of2,
shadow_fn = sf2}) =>
{prop_matchers = Library.merge (eq_snd op =) (pm1, pm2),
typed_matchers = Library.merge (eq_snd op =) (tm1, tm2),
term_fn = (if eq_option (eq_snd op =) (tf1, tf2) then tf1
else raise Fail "join_infos: term_fn non-equal"),
output_fn = (if eq_option (eq_snd op =) (of1, of2) then of1
else raise Fail "join_infos: output_fn non-equal"),
shadow_fn = (if eq_option (eq_snd op =) (sf1, sf2) then sf1
else raise Fail "join_infos: shadow_fn non-equal")})
)
fun pat_of_match_arg arg =
case arg of
PropMatch pat => pat
| TypedMatch (_, pat) => pat
| TypedUniv _ => Term.dummy
| PropertyMatch pat => pat
| WellFormMatch (_, req) => req
fun subst_arg inst arg =
case arg of
PropMatch pat => PropMatch (Util.subst_term_norm inst pat)
| TypedMatch (ty_str, pat) =>
TypedMatch (ty_str, Util.subst_term_norm inst pat)
| TypedUniv ty_str => TypedUniv ty_str
| PropertyMatch pat =>
PropertyMatch (Util.subst_term_norm inst pat)
| WellFormMatch (t, req) =>
WellFormMatch (Util.subst_term_norm inst t, Util.subst_term_norm inst req)
fun assert_valid_arg arg =
case arg of
PropMatch pat =>
assert (fastype_of pat = UtilBase.boolT)
"assert_valid_arg: arg for PropMatch should be bool."
| TypedMatch _ => ()
| TypedUniv _ => ()
| PropertyMatch pat =>
assert (fastype_of pat = UtilBase.boolT)
"assert_valid_arg: arg for PropertyMatch should be bool."
| WellFormMatch (_, req) =>
assert (fastype_of req = UtilBase.boolT)
"assert_valid_arg: arg for WellFormMatch should be bool."
fun check_ty_str ty_str arg =
case arg of
TypedMatch (ty_str', _) => ty_str = ty_str'
| TypedUniv ty_str' => ty_str = ty_str'
| _ => true
fun is_ordinary_match arg =
case arg of PropMatch _ => true
| TypedMatch _ => true
| _ => false
fun is_side_match arg =
case arg of PropertyMatch _ => true
| WellFormMatch _ => true
| _ => false
fun identify NONE = NONE
| identify (SOME x) = (SOME (x, serial ()))
fun add_item_type (ty_str, term_fn, output_fn, shadow_fn) =
let
val item_info : item_io_info =
{prop_matchers = [], typed_matchers = [],
term_fn = identify term_fn,
output_fn = identify output_fn,
shadow_fn = identify shadow_fn}
in
Data.map (Symtab.update_new (ty_str, item_info))
end
fun add_prop_matcher (ty_str, it_match) = Data.map (
Symtab.map_entry ty_str (add_prop_matcher_to_info it_match))
fun add_typed_matcher (ty_str, it_match) = Data.map (
Symtab.map_entry ty_str (add_typed_matcher_to_info it_match))
fun get_io_info thy ty_str =
the (Symtab.lookup (Data.get thy) ty_str)
handle Option.Option => raise Fail ("get_io_info: not found " ^ ty_str)
fun get_prop_matchers thy ty_str = #prop_matchers (get_io_info thy ty_str) |> map fst
fun get_typed_matchers thy ty_str = #typed_matchers (get_io_info thy ty_str) |> map fst
val prop_matcher =
let
fun pre_match pat {tname, ...} ctxt =
let
val ct = the_single tname
val t = Thm.term_of ct
in
if UtilLogic.is_neg pat then
UtilLogic.is_neg t andalso
Matcher.pre_match_head ctxt (UtilLogic.get_neg pat, UtilLogic.get_cneg ct)
else
Term.is_Var pat orelse
(not (UtilLogic.is_neg t) andalso Matcher.pre_match_head ctxt (pat, ct))
end
fun match pat {tname, prop, ...} ctxt (id, inst) =
let
val ct = the_single tname
val t = Thm.term_of ct
in
if UtilLogic.is_neg pat andalso UtilLogic.is_neg t then
let
val insts' = Matcher.rewrite_match_head
ctxt (UtilLogic.get_neg pat, UtilLogic.get_cneg ct) (id, inst)
fun process_inst (inst, eq_th) =
let
val make_neg_eq' = Thm.combination (Thm.reflexive UtilBase.cNot)
in
(inst, Thm.equal_elim (
UtilLogic.make_trueprop_eq (make_neg_eq' (meta_sym eq_th))) prop)
end
in
map process_inst insts'
end
else if not (UtilLogic.is_neg pat) andalso
(Term.is_Var pat orelse not (UtilLogic.is_neg t)) then
let
val insts' = Matcher.rewrite_match_head ctxt (pat, ct) (id, inst)
fun process_inst (inst, eq_th) =
(inst, Thm.equal_elim (
UtilLogic.make_trueprop_eq (meta_sym eq_th)) prop)
in
map process_inst insts'
end
else []
end
in
{pre_match = pre_match, match = match}
end
val term_prop_matcher =
let
fun pre_match pat {tname, ...} ctxt =
if not (Util.has_vars pat) then false
else if UtilBase.is_eq_term pat then
Matcher.pre_match ctxt (fst (UtilBase.dest_eq pat), the_single tname)
else false
fun match pat {tname, ...} ctxt (id, inst) =
if not (UtilBase.is_eq_term pat) then [] else
if not (Util.has_vars pat) then [] else
let
val (lhs, rhs) = UtilBase.dest_eq pat
val cu = the_single tname
val pairs = if Term.is_Var lhs then
[(false, (lhs, cu)), (true, (rhs, cu))]
else [(true, (lhs, cu)), (false, (rhs, cu))]
val insts' = Matcher.rewrite_match_list ctxt pairs (id, inst)
fun process_inst (inst, ths) =
let
val (th1, th2) = the_pair ths
in
(inst, UtilLogic.to_obj_eq (Util.transitive_list [th1, meta_sym th2]))
end
in
map process_inst insts'
end
in
{pre_match = pre_match, match = match}
end
val null_eq_matcher =
let
fun pre_match pat _ _ = UtilBase.is_eq_term pat
fun match pat _ ctxt (id, inst) =
if not (UtilBase.is_eq_term pat) then [] else
if Util.has_vars pat then [] else
let
val (lhs, rhs) = UtilBase.dest_eq pat
val infos = RewriteTable.equiv_info_t ctxt id (lhs, rhs)
fun process_info (id', th) =
((id', inst), UtilLogic.to_obj_eq th)
in
map process_info infos
end
in
{pre_match = pre_match, match = match}
end
val term_typed_matcher =
let
fun pre_match pat {tname, ...} ctxt =
Matcher.pre_match_head ctxt (pat, the_single tname)
fun match pat {tname, ...} ctxt (id, inst) =
Matcher.rewrite_match_head ctxt (pat, the_single tname) (id, inst)
in
{pre_match = pre_match, match = match}
end
val eq_tname_typed_matcher =
let
fun pre_match pat {tname, ...} ctxt =
let
val thy = Proof_Context.theory_of ctxt
val (lhs, rhs) = the_pair (map Thm.term_of tname)
val _ = Pattern.first_order_match thy (pat, UtilBase.mk_eq (lhs, rhs)) fo_init
in
true
end
handle Pattern.MATCH => false
fun match pat {tname, ...} ctxt (id, inst) =
let
val thy = Proof_Context.theory_of ctxt
val (lhs, rhs) = the_pair (map Thm.term_of tname)
val inst' =
Pattern.first_order_match thy (pat, UtilBase.mk_eq (lhs, rhs)) inst
in
[((id, inst'), UtilBase.true_th)]
end
handle Pattern.MATCH => []
in
{pre_match = pre_match, match = match}
end
val null_property_matcher =
let
fun pre_match pat _ _ =
Property.is_property pat
fun match pat _ ctxt (id, inst) =
if Util.has_vars pat then []
else if not (Property.is_property pat) then []
else map (fn (id', th) => ((id', inst), th))
(PropertyData.get_property_t ctxt (id, pat))
in
{pre_match = pre_match, match = match}
end
val term_property_matcher =
let
fun pre_match pat {tname, ...} ctxt =
Property.is_property pat andalso
Matcher.pre_match_head ctxt (
Property.get_property_arg pat, the_single tname)
fun match pat {tname, ...} ctxt (id, inst) =
if not (Util.has_vars pat) then [] else
if not (Property.is_property pat) then
[]
else let
val arg = Property.get_property_arg pat
in
let
val insts' = Matcher.rewrite_match_head
ctxt (arg, the_single tname) (id, inst)
fun process_inst ((id', inst'), _) =
let
val t = Util.subst_term_norm inst' pat
in
map (fn (id'', th) => ((id'', inst'), th))
(PropertyData.get_property_t ctxt (id', t))
end
in
maps process_inst insts'
end
end
in
{pre_match = pre_match, match = match}
end
fun pre_match_arg ctxt arg (item as {ty_str, ...}) =
if not (check_ty_str ty_str arg) then false else
let
val _ = assert_valid_arg arg
val thy = Proof_Context.theory_of ctxt
val {prop_matchers, typed_matchers, ...} = get_io_info thy ty_str
in
case arg of
PropMatch pat =>
Term.is_Var pat orelse
(UtilLogic.is_neg pat andalso Term.is_Var (UtilLogic.get_neg pat)) orelse
not (Util.is_pattern pat) orelse
exists (fn f => f pat item ctxt) (map (#pre_match o fst) prop_matchers)
| TypedMatch (_, pat) =>
not (Util.is_pattern pat) orelse
exists (fn f => f pat item ctxt) (map (#pre_match o fst) typed_matchers)
| TypedUniv _ => true
| PropertyMatch _ =>
raise Fail "pre_match_arg: should not be called on PropertyMatch."
| WellFormMatch _ =>
raise Fail "pre_match_arg: should not be called on WellFormMatch."
end
fun match_arg ctxt arg (item as {id, ty_str, ...}) (id', inst) =
if not (check_ty_str ty_str arg) then [] else
let
val _ = assert_valid_arg arg
val thy = Proof_Context.theory_of ctxt
val {prop_matchers, typed_matchers, ...} = get_io_info thy ty_str
val pat = pat_of_match_arg arg
val id'' = BoxID.merge_boxes ctxt (id, id')
in
case arg of
PropMatch _ => maps (fn f => f pat item ctxt (id'', inst))
(map (#match o fst) prop_matchers)
| TypedUniv _ => [((id'', inst), UtilBase.true_th)]
| TypedMatch _ => maps (fn f => f pat item ctxt (id'', inst))
(map (#match o fst) typed_matchers)
| PropertyMatch _ =>
raise Fail "match_arg: should not be called on PropertyMatch."
| WellFormMatch _ =>
raise Fail "match_arg: should not be called on WellFormMatch."
end
val no_rewr_terms = K []
fun arg_rewr_terms ts = maps Util.dest_args ts
fun prop_rewr_terms ts =
let
val t = the_single ts
in
if UtilLogic.is_neg t then t |> dest_arg |> Util.dest_args
else t |> Util.dest_args
end
fun rewr_terms_of_item ctxt (ty_str, tname) =
let
val thy = Proof_Context.theory_of ctxt
val {term_fn, ...} = get_io_info thy ty_str
in
case term_fn of
NONE => tname
| SOME (f, _) => f tname
end
fun output_prop_fn ctxt (_, th) = Thm.prop_of th |> Syntax.string_of_term ctxt
fun string_of_item_info ctxt (ty_str, ts, th) =
let
val thy = Proof_Context.theory_of ctxt
val {output_fn, ...} = get_io_info thy ty_str
in
case output_fn of
NONE => ty_str ^ " " ^ (Util.string_of_terms ctxt ts)
| SOME (f, _) => f ctxt (ts, th)
end
fun string_of_raw_item ctxt ritem =
case ritem of
Handler (_, t, _) => "Handler " ^ (Syntax.string_of_term ctxt t)
| Fact info => string_of_item_info ctxt info
fun string_of_item ctxt {ty_str, tname, prop, ...} =
string_of_item_info ctxt (ty_str, map Thm.term_of tname, prop)
fun trace_ritem ctxt s ritem =
tracing (s ^ " " ^ (string_of_raw_item ctxt ritem))
fun trace_ritems ctxt s ritems =
tracing (s ^ "\n" ^ (cat_lines (map (string_of_raw_item ctxt) ritems)))
fun trace_item ctxt s item =
tracing (s ^ " " ^ (string_of_item ctxt item))
fun trace_items ctxt s items =
tracing (s ^ "\n" ^ (cat_lines (map (string_of_item ctxt) items)))
fun shadow_prop_fn ctxt id (ts1, cts2) =
let
val (t1, ct2) = (the_single ts1, the_single cts2)
val (lhs, crhs) = if UtilLogic.is_neg t1 andalso UtilLogic.is_neg (Thm.term_of ct2) then
(UtilLogic.get_neg t1, UtilLogic.get_cneg ct2)
else
(t1, ct2)
in
(Matcher.rewrite_match_head ctxt (lhs, crhs) (id, fo_init))
|> filter (fn ((id', _), _) => id' = id)
|> not o null
end
fun shadow_term_fn ctxt id (ts1, cts2) =
let
val (lhs, crhs) = (the_single ts1, the_single cts2)
in
(Matcher.rewrite_match_head ctxt (lhs, crhs) (id, fo_init))
|> filter (fn ((id', _), _) => id' = id)
|> not o null
end
val add_basic_item_io =
fold add_item_type [
(TY_NULL, NONE, NONE, NONE),
(TY_PROP, SOME prop_rewr_terms, SOME output_prop_fn, SOME shadow_prop_fn),
(TY_TERM, SOME no_rewr_terms, NONE, SOME shadow_term_fn),
(TY_EQ, NONE, SOME output_prop_fn, NONE),
(TY_VAR, NONE, NONE, NONE),
(TY_PROPERTY, SOME arg_rewr_terms, NONE, NONE)
] #> fold add_prop_matcher [
(TY_PROP, prop_matcher), (TY_TERM, term_prop_matcher),
(TY_NULL, null_eq_matcher), (TY_NULL, null_property_matcher),
(TY_TERM, term_property_matcher)
] #> fold add_typed_matcher [
(TY_PROP, prop_matcher), (TY_TERM, term_typed_matcher),
(TY_VAR, term_typed_matcher), (TY_EQ, eq_tname_typed_matcher)
]
end