diff -r 2290cc06049b -r 81d6dc597559 src/Provers/eqsubst.ML --- a/src/Provers/eqsubst.ML Fri Jun 09 17:32:38 2006 +0200 +++ b/src/Provers/eqsubst.ML Sun Jun 11 00:28:18 2006 +0200 @@ -10,9 +10,13 @@ val setup : theory -> theory end; -structure EqSubst: EQSUBST = -struct +structure EqSubst +(* : EQSUBST *) += struct +structure Z = Zipper; + +(* changes object "=" to meta "==" which prepares a given rewrite rule *) fun prep_meta_eq ctxt = let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt) in mk #> map Drule.zero_var_indexes end; @@ -29,7 +33,129 @@ type searchinfo = theory * int (* maxidx *) - * BasicIsaFTerm.FcTerm (* focusterm to search under *) + * Zipper.T (* focusterm to search under *) + + +(* skipping non-empty sub-sequences but when we reach the end + of the seq, remembering how much we have left to skip. *) +datatype 'a skipseq = SkipMore of int + | SkipSeq of 'a Seq.seq Seq.seq; +(* given a seqseq, skip the first m non-empty seq's, note deficit *) +fun skipto_skipseq m s = + let + fun skip_occs n sq = + case Seq.pull sq of + NONE => SkipMore n + | SOME (h,t) => + (case Seq.pull h of NONE => skip_occs n t + | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t) + else skip_occs (n - 1) t) + in (skip_occs m s) end; + +(* note: outerterm is the taget with the match replaced by a bound + variable : ie: "P lhs" beocmes "%x. P x" + insts is the types of instantiations of vars in lhs + and typinsts is the type instantiations of types in the lhs + Note: Final rule is the rule lifted into the ontext of the + taget thm. *) +fun mk_foo_match mkuptermfunc Ts t = + let + val ty = Term.type_of t + val bigtype = (rev (map snd Ts)) ---> ty + fun mk_foo 0 t = t + | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1))) + val num_of_bnds = (length Ts) + (* foo_term = "fooabs y0 ... yn" where y's are local bounds *) + val foo_term = mk_foo num_of_bnds (Bound num_of_bnds) + in Abs("fooabs", bigtype, mkuptermfunc foo_term) end; + +(* T is outer bound vars, n is number of locally bound vars *) +(* THINK: is order of Ts correct...? or reversed? *) +fun fakefree_badbounds Ts t = + let val (FakeTs,Ts,newnames) = + List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => + let val newname = Term.variant usednames n + in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs, + (newname,ty)::Ts, + newname::usednames) end) + ([],[],[]) + Ts + in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end; + +(* before matching we need to fake the bound vars that are missing an +abstraction. In this function we additionally construct the +abstraction environment, and an outer context term (with the focus +abstracted out) for use in rewriting with RWInst.rw *) +fun prep_zipper_match z = + let + val t = Z.trm z + val c = Z.ctxt z + val Ts = Z.C.nty_ctxt c + val (FakeTs', Ts', t') = fakefree_badbounds Ts t + val absterm = mk_foo_match (Z.C.apply c) Ts' t' + in + (t', (FakeTs', Ts', absterm)) + end; + +(* Matching and Unification with exception handled *) +fun clean_match thy (a as (pat, t)) = + let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty) + in SOME (Vartab.dest tyenv, Vartab.dest tenv) + end handle Pattern.MATCH => NONE; +(* given theory, max var index, pat, tgt; returns Seq of instantiations *) +fun clean_unify sgn ix (a as (pat, tgt)) = + let + (* type info will be re-derived, maybe this can be cached + for efficiency? *) + val pat_ty = Term.type_of pat; + val tgt_ty = Term.type_of tgt; + (* is it OK to ignore the type instantiation info? + or should I be using it? *) + val typs_unify = + SOME (Sign.typ_unify sgn (pat_ty, tgt_ty) (Term.Vartab.empty, ix)) + handle Type.TUNIFY => NONE; + in + case typs_unify of + SOME (typinsttab, ix2) => + let + (* is it right to throw away the flexes? + or should I be using them somehow? *) + fun mk_insts env = + (Vartab.dest (Envir.type_env env), + Envir.alist_of env); + val initenv = Envir.Envir {asol = Vartab.empty, + iTs = typinsttab, maxidx = ix2}; + val useq = (Unify.smash_unifiers (sgn,initenv,[a])) + handle UnequalLengths => Seq.empty + | Term.TERM _ => Seq.empty; + fun clean_unify' useq () = + (case (Seq.pull useq) of + NONE => NONE + | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t))) + handle UnequalLengths => NONE + | Term.TERM _ => NONE; + in + (Seq.make (clean_unify' useq)) + end + | NONE => Seq.empty + end; + +(* Matching and Unification for zippers *) +(* Note: Ts is a modified version of the original names of the outer +bound variables. New names have been introduced to make sure they are +unique w.r.t all names in the term and each other. usednames' is +oldnames + new names. *) +fun clean_match_z thy pat z = + let val (t, (FakeTs,Ts,absterm)) = prep_zipper_match z in + case clean_match thy (pat, t) of + NONE => NONE + | SOME insts => SOME (insts, FakeTs, Ts, absterm) end; +(* ix = max var index *) +fun clean_unify_z sgn ix pat z = + let val (t, (FakeTs, Ts,absterm)) = prep_zipper_match z in + Seq.map (fn insts => (insts, FakeTs, Ts, absterm)) + (clean_unify sgn ix (t, pat)) end; + (* FOR DEBUGGING... type trace_subst_errT = int (* subgoal *) @@ -46,54 +172,45 @@ val trace_subst_err = (ref NONE : trace_subst_errT option ref); val trace_subst_search = ref false; exception trace_subst_exp of trace_subst_errT; - *) +*) + + +fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l + | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t + | bot_left_leaf_of x = x; +fun valid_match_start z = + (case bot_left_leaf_of (Z.trm z) of + Const _ => true + | Free _ => true + | Abs _ => true (* allowed to look inside abs... search decides if we actually consider the abstraction itself *) + | _ => false); (* avoid vars - always suceeds uninterestingly. *) + (* search from top, left to right, then down *) -fun search_tlr_all_f f ft = - let - fun maux ft = - let val t' = (IsaFTerm.focus_of_fcterm ft) - (* val _ = - if !trace_subst_search then - (writeln ("Examining: " ^ (TermLib.string_of_term t')); - TermLib.writeterm t'; ()) - else (); *) - in - (case t' of - (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft), - Seq.cons (f ft) (maux (IsaFTerm.focus_right ft))) - | (Abs _) => Seq.cons (f ft) (maux (IsaFTerm.focus_abs ft)) - | leaf => Seq.single (f ft)) end - in maux ft end; +val search_tlr_all = ZipperSearch.all_td_lr; (* search from top, left to right, then down *) -fun search_tlr_valid_f f ft = - let - fun maux ft = - let - val hereseq = if IsaFTerm.valid_match_start ft then f ft else Seq.empty - in - (case (IsaFTerm.focus_of_fcterm ft) of - (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft), - Seq.cons hereseq (maux (IsaFTerm.focus_right ft))) - | (Abs _) => Seq.cons hereseq (maux (IsaFTerm.focus_abs ft)) - | leaf => Seq.single hereseq) - end - in maux ft end; +fun search_tlr_valid validf = + let + fun sf_valid_td_lr z = + let val here = if validf z then [Z.Here z] else [] in + case Z.trm z + of _ $ _ => here @ [Z.LookIn (Z.move_down_left z), + Z.LookIn (Z.move_down_right z)] + | Abs _ => here @ [Z.LookIn (Z.move_down_abs z)] + | _ => here + end; + in Z.lzy_search sf_valid_td_lr end; (* search all unifications *) -fun searchf_tlr_unify_all (sgn, maxidx, ft) lhs = - IsaFTerm.find_fcterm_matches - search_tlr_all_f - (IsaFTerm.clean_unify_ft sgn maxidx lhs) - ft; +fun searchf_tlr_unify_all (sgn, maxidx, z) lhs = + Seq.map (clean_unify_z sgn maxidx lhs) + (Z.limit_apply search_tlr_all z); (* search only for 'valid' unifiers (non abs subterms and non vars) *) -fun searchf_tlr_unify_valid (sgn, maxidx, ft) lhs = - IsaFTerm.find_fcterm_matches - search_tlr_valid_f - (IsaFTerm.clean_unify_ft sgn maxidx lhs) - ft; +fun searchf_tlr_unify_valid (sgn, maxidx, z) lhs = + Seq.map (clean_unify_z sgn maxidx lhs) + (Z.limit_apply (search_tlr_valid valid_match_start) z); (* apply a substitution in the conclusion of the theorem th *) @@ -124,9 +241,9 @@ val conclterm = Logic.strip_imp_concl fixedbody; val conclthm = trivify conclterm; val maxidx = Term.maxidx_of_term conclterm; - val ft = ((IsaFTerm.focus_right - o IsaFTerm.focus_left - o IsaFTerm.fcterm_of_term + val ft = ((Z.move_down_right (* ==> *) + o Z.move_down_left (* Trueprop *) + o Z.mktop o Thm.prop_of) conclthm) in ((cfvs, conclthm), (sgn, maxidx, ft)) @@ -150,12 +267,14 @@ (* General substitution of multiple occurances using one of the given theorems*) + + exception eqsubst_occL_exp of string * (int list) * (thm list) * int * thm; fun skip_first_occs_search occ srchf sinfo lhs = - case (IsaPLib.skipto_seqseq occ (srchf sinfo lhs)) of - IsaPLib.skipmore _ => Seq.empty - | IsaPLib.skipseq ss => Seq.flat ss; + case (skipto_skipseq occ (srchf sinfo lhs)) of + SkipMore _ => Seq.empty + | SkipSeq ss => Seq.flat ss; fun eqsubst_tac ctxt occL thms i th = let val nprems = Thm.nprems_of th in @@ -163,8 +282,10 @@ let val thmseq = (Seq.of_list thms) fun apply_occ occ th = thmseq |> Seq.maps - (fn r => eqsubst_tac' ctxt (skip_first_occs_search - occ searchf_tlr_unify_valid) r + (fn r => eqsubst_tac' + ctxt + (skip_first_occs_search + occ searchf_tlr_unify_valid) r (i + ((Thm.nprems_of th) - nprems)) th); val sortedoccL = @@ -235,15 +356,15 @@ val pth = trivify asmt; val maxidx = Term.maxidx_of_term asmt; - val ft = ((IsaFTerm.focus_right - o IsaFTerm.fcterm_of_term + val ft = ((Z.move_down_right (* trueprop *) + o Z.mktop o Thm.prop_of) pth) in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end; (* prepare subst in every possible assumption *) fun prep_subst_in_asms i gth = map (prep_subst_in_asm i gth) - ((rev o IsaPLib.mk_num_list o length) + ((fn l => Library.upto (1, length l)) (Logic.prems_of_goal (Thm.prop_of gth) i)); @@ -257,8 +378,8 @@ fun occ_search occ [] = Seq.empty | occ_search occ ((asminfo, searchinfo)::moreasms) = (case searchf searchinfo occ lhs of - IsaPLib.skipmore i => occ_search i moreasms - | IsaPLib.skipseq ss => + SkipMore i => occ_search i moreasms + | SkipSeq ss => Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss), occ_search 1 moreasms)) @@ -270,7 +391,7 @@ fun skip_first_asm_occs_search searchf sinfo occ lhs = - IsaPLib.skipto_seqseq occ (searchf sinfo lhs); + skipto_skipseq occ (searchf sinfo lhs); fun eqsubst_asm_tac ctxt occL thms i th = let val nprems = Thm.nprems_of th