walther@59906: (* Title: Interpret/derive.sml walther@59934: Author: Walther Neuper walther@59906: (c) due to copyright terms walther@59906: walther@59934: Try to make (term * rule * result) steps (= derivation) by use of a Rule_Set.T. walther@59934: Two purposes: walther@59934: (1) derive steps from a given term towards another give term walther@59934: (2) term transformations, which cannot be done by rewriting, e.g cancellation of polynomials. walther@59906: *) walther@59906: walther@59907: signature DERIVE = walther@59906: sig walther@59934: type rule_result walther@59934: type step walther@59907: type derivation walther@59934: Walther@60509: val do_one : Proof.context -> Rule_Set.T -> Rule.rule list -> Rewrite_Ord.function -> walther@59907: term option -> term -> derivation Walther@60509: val steps_reverse : Proof.context -> Rule_Set.T -> Rule.rule list -> Rewrite_Ord.function -> walther@59934: term option -> term -> rule_result list Walther@60509: val steps : Rewrite_Ord.T -> Rule_Set.T -> Rule.rule list -> term -> term -> walther@59934: bool * derivation walther@59932: val embed: State_Steps.T -> Calc.T -> Pos.pos' list * Calc.T wenzelm@60223: \<^isac_test>\ walther@59906: val trtas2str : (term * Rule.rule * (term * term list)) list -> string walther@59906: val deriv2str : (term * Rule.rule * (term * term list)) list -> string walther@59906: val rev_deriv' : 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c) wenzelm@60223: \ walther@59906: end walther@59906: walther@59906: (**) walther@59907: structure Derive(**): DERIVE(**) = walther@59906: struct walther@59906: (**) walther@59907: walther@59907: (** the triple for a step **) walther@59907: walther@59934: type rule_result = Rule.rule * Calc.result; walther@59934: type step = term * Rule.rule * Calc.result; walther@59934: type derivation = step list; walther@59906: walther@59906: fun trta2str (t, r, (t', a)) = walther@59906: "\n(" ^ UnparseC.term t ^ ", " ^ Rule.to_string_short r ^ ", (" ^ UnparseC.term t' ^ ", " ^ UnparseC.terms a ^ "))" walther@59906: fun trtas2str trtas = (strs2str o (map trta2str)) trtas walther@59906: val deriv2str = trtas2str walther@59906: walther@59934: walther@59907: (** make one triple towards the goal term **) walther@59906: Walther@60501: fun msg_1 ctxt rts = Walther@60501: (tracing ("do_one exceeds " ^ int2str (Config.get ctxt rewrite_limit) ^ "with derivation =\n"); walther@59907: tracing (deriv2str rts)); Walther@60500: fun msg_2 ctxt thmid = Walther@60500: if not (Config.get ctxt rewrite_trace) then () else tracing ("### trying thm \"" ^ thmid ^ "\""); Walther@60500: fun msg_3 ctxt t' = Walther@60500: if Config.get ctxt rewrite_trace then tracing ("=== rewrites to: " ^ UnparseC.term t') else (); Walther@60500: fun msg_4 ctxt op_ = Walther@60500: if not (Config.get ctxt rewrite_trace) then () else tracing ("### trying calc. \"" ^ op_^"\""); Walther@60500: fun msg_5 ctxt t' = Walther@60500: if not (Config.get ctxt rewrite_trace) then () else tracing("=== calc. to: " ^ UnparseC.term t') walther@59906: walther@59934: Walther@60500: fun do_one ctxt erls rs ro goal tt = walther@59906: let walther@59907: datatype switch = Appl | Noap (* TODO: unify with version in Rewrite *) walther@59906: fun rew_once _ rts t Noap [] = walther@59907: (case goal of NONE => rts | SOME _ => walther@59934: raise ERROR ("Derive.do_one: no derivation for " ^ UnparseC.term t)) walther@59906: | rew_once lim rts t Appl [] = rew_once lim rts t Noap rs walther@59906: | rew_once lim rts t apno rs' = walther@59906: (case goal of walther@59906: NONE => rew_or_calc lim rts t apno rs' walther@59906: | SOME g => if g = t then rts else rew_or_calc lim rts t apno rs') walther@59906: and rew_or_calc lim rts t apno (rrs' as (r :: rs')) = walther@59906: if lim < 0 Walther@60501: then (msg_1 ctxt rts; rts) walther@59906: else walther@59906: (case r of walther@59906: Rule.Thm (thmid, tm) => Walther@60500: (msg_2 ctxt thmid; Walther@60500: case Rewrite.rewrite_ ctxt ro erls true tm t of walther@59906: NONE => rew_once lim rts t apno rs' walther@59906: | SOME (t', a') => Walther@60500: (msg_3 ctxt t'; rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')) walther@59906: | Rule.Eval (c as (op_, _)) => Walther@60500: (msg_4 ctxt op_; Walther@60500: case Eval.adhoc_thm (Proof_Context.theory_of ctxt) c t of walther@59906: NONE => rew_once lim rts t apno rs' walther@59906: | SOME (thmid, tm) => walther@59906: (let Walther@60500: val (t', a') = case Rewrite.rewrite_ ctxt ro erls true tm t of walther@59906: SOME ta => ta walther@59907: | NONE => raise ERROR "adhoc_thm: NONE" Walther@60500: val _ = msg_5 ctxt t' walther@59906: val r' = Rule.Thm (thmid, tm) walther@59906: in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end) walther@60269: handle Rewrite.NO_REWRITE => raise ERROR "derive_norm, Eval: no rewrite") walther@59907: | Rule.Rls_ rls => Walther@60500: (case Rewrite.rewrite_set_ ctxt true rls t of walther@59906: NONE => rew_once lim rts t apno rs' walther@59906: | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs') walther@59907: | rule => raise ERROR ("rew_once: uncovered case " ^ Rule.to_string rule)) walther@59907: | rew_or_calc _ _ _ _ [] = raise ERROR "rew_or_calc: called with []" Walther@60501: in rew_once (Config.get ctxt rewrite_limit) [] tt Noap rs end walther@59906: walther@59907: walther@59907: (** concatenate several steps in revers order **) walther@59907: walther@59906: fun rev_deriv (t, r, (_, a)) = (ThmC.make_sym_rule r, (t, a)); walther@59907: fun steps_reverse thy erls rs ro goal t = walther@59907: (rev o (map rev_deriv)) (do_one thy erls rs ro goal t) walther@59906: walther@59907: walther@59907: (** concatenate several steps **) walther@59907: walther@59906: fun rev_deriv' (t, r, (t', a)) = (t', ThmC.make_sym_rule r, (t, a)); walther@59906: walther@59906: (* fo = ifo excluded already in inform *) walther@59907: fun steps rew_ord erls rules fo ifo = walther@59906: let walther@59906: fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty walther@59906: | derivat dt = (#1 o #3 o last_elem) dt walther@59907: fun equal (_, _, (t1, _)) (_, _, (t2, _)) = t1 = t2 Walther@60500: val fod = do_one (Proof_Context.init_global (ThyC.Isac())) erls rules (snd rew_ord) NONE fo Walther@60500: val ifod = do_one (Proof_Context.init_global (ThyC.Isac())) erls rules (snd rew_ord) NONE ifo walther@59906: in walther@59906: case (fod, ifod) of walther@59906: ([], []) => if fo = ifo then (true, []) else (false, []) walther@59906: | (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, []) walther@59906: | ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, []) walther@59906: | (fod, ifod) => walther@59906: if derivat fod = derivat ifod (*common normal form found*) then walther@59906: let walther@59906: val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod) walther@59906: in (true, fod' @ (map rev_deriv' rifod')) end walther@59906: else (false, []) walther@59906: end walther@59906: walther@59934: (** embed a derivation into the Ctree **) walther@59934: walther@59932: fun embed tacis (pt, pos as (p, Pos.Frm)) = walther@59932: (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402 walther@59932: and transfer the istate (from _after_ compare_deriv) from Frm to Res*) walther@59932: let walther@59932: val (res, asm) = (State_Steps.result o last_elem) tacis walther@59932: val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of walther@59932: (SOME (ist, ctxt), _) => (ist, ctxt) walther@59934: | (NONE, _) => raise ERROR "Derive.embed Frm: uncovered case get_obj" walther@59932: val form = Ctree.get_obj Ctree.g_form pt p walther@59932: (*val p = lev_on p; ---------------only difference to (..,Res) below*) walther@59932: val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' form, (pos, (Istate_Def.Uistate, ctxt))) :: walther@59932: (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm), walther@59932: (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))] walther@60154: val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)) walther@59932: val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res)) walther@59932: val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls)) walther@59932: val pt = Ctree.update_branch pt p Ctree.TransitiveB walther@59932: in (c, (pt, pos)) end walther@59932: | embed tacis (pt, (p, Pos.Res)) = walther@59932: (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ? walther@59932: and transfer the istate (from _after_ compare_deriv) from Res to new Res*) walther@59932: let walther@59932: val (res, asm) = (State_Steps.result o last_elem) tacis walther@59932: val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of walther@59932: (_, SOME (ist, ctxt)) => (ist, ctxt) walther@59934: | (_, NONE) => raise ERROR "Derive.embed Frm: uncovered case get_obj" walther@59932: val (f, _) = Ctree.get_obj Ctree.g_result pt p walther@59932: val p = Pos.lev_on p(*---------------only difference to (..,Frm) above*); walther@59932: val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) :: walther@59932: (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm), walther@59932: (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))]; walther@60154: val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)) walther@59932: val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res)) walther@59932: val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls)) walther@59932: val pt = Ctree.update_branch pt p Ctree.TransitiveB walther@59932: in (c, (pt, pos)) end walther@59934: | embed _ _ = raise ERROR "Derive.embed: uncovered definition" walther@59932: walther@59906: (**)end(**)