1 (* Title: Interpret/derive.sml
3 (c) due to copyright terms
5 Try to make (term * rule * result) steps (= derivation) by use of a Rule_Set.T.
7 (1) derive steps from a given term towards another give term
8 (2) term transformations, which cannot be done by rewriting, e.g cancellation of polynomials.
17 val do_one : Proof.context -> Rule_Set.T -> Rule.rule list -> Rewrite_Ord.function ->
18 term option -> term -> derivation
19 val steps_reverse : Proof.context -> Rule_Set.T -> Rule.rule list -> Rewrite_Ord.function ->
20 term option -> term -> rule_result list
21 val steps : Proof.context -> Rewrite_Ord.T -> Rule_Set.T -> Rule.rule list -> term -> term ->
23 val embed: State_Steps.T -> Calc.T -> Pos.pos' list * Calc.T
25 val trtas2str : Proof.context -> (term * Rule.rule * (term * term list)) list -> string
26 val deriv2str : Proof.context -> (term * Rule.rule * (term * term list)) list -> string
27 val rev_deriv' : Proof.context -> 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c)
32 structure Derive(**): DERIVE(**) =
36 (** the triple for a step **)
38 type rule_result = Rule.rule * Calc.result;
39 type step = term * Rule.rule * Calc.result;
40 type derivation = step list;
42 fun trta2str ctxt (t, r, (t', a)) =
43 "\n(" ^ UnparseC.term ctxt t ^ ", " ^ Rule.to_string_short r ^
44 ", (" ^ UnparseC.term ctxt t' ^ ", " ^ UnparseC.terms ctxt a ^ "))"
45 fun trtas2str ctxt trtas = (strs2str o (map (trta2str ctxt))) trtas
46 val deriv2str = trtas2str
49 (** make one triple towards the goal term **)
52 (tracing ("do_one exceeds " ^ int2str (Config.get ctxt rewrite_limit) ^ "with derivation =\n");
53 tracing (deriv2str ctxt rts));
54 fun msg_2 ctxt thmid =
55 if not (Config.get ctxt rewrite_trace) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");
57 if Config.get ctxt rewrite_trace then tracing ("=== rewrites to: " ^ UnparseC.term ctxt t') else ();
59 if not (Config.get ctxt rewrite_trace) then () else tracing ("### trying calc. \"" ^ op_^"\"");
61 if not (Config.get ctxt rewrite_trace) then () else tracing("=== calc. to: " ^ UnparseC.term ctxt t')
64 fun do_one ctxt asm_rls rs ro goal tt =
66 datatype switch = Appl | Noap (* TODO: unify with version in Rewrite *)
67 fun rew_once _ rts t Noap [] =
68 (case goal of NONE => rts | SOME _ =>
69 raise ERROR ("Derive.do_one: no derivation for " ^ UnparseC.term ctxt t))
70 | rew_once lim rts t Appl [] = rew_once lim rts t Noap rs
71 | rew_once lim rts t apno rs' =
73 NONE => rew_or_calc lim rts t apno rs'
74 | SOME g => if g = t then rts else rew_or_calc lim rts t apno rs')
75 and rew_or_calc lim rts t apno (rrs' as (r :: rs')) =
77 then (msg_1 ctxt rts; rts)
80 Rule.Thm (thmid, tm) =>
82 case Rewrite.rewrite_ ctxt ro asm_rls true tm t of
83 NONE => rew_once lim rts t apno rs'
85 (msg_3 ctxt t'; rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))
86 | Rule.Eval (c as (op_, _)) =>
88 case Eval.adhoc_thm ctxt c t of
89 NONE => rew_once lim rts t apno rs'
92 val (t', a') = case Rewrite.rewrite_ ctxt ro asm_rls true tm t of
94 | NONE => raise ERROR "adhoc_thm: NONE"
96 val r' = Rule.Thm (thmid, tm)
97 in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end)
98 handle Rewrite.NO_REWRITE => raise ERROR "derive_norm, Eval: no rewrite")
100 (case Rewrite.rewrite_set_ ctxt true rls t of
101 NONE => rew_once lim rts t apno rs'
102 | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')
103 | rule => raise ERROR ("rew_once: uncovered case " ^ Rule.to_string ctxt rule))
104 | rew_or_calc _ _ _ _ [] = raise ERROR "rew_or_calc: called with []"
105 in rew_once (Config.get ctxt rewrite_limit) [] tt Noap rs end
108 (** concatenate several steps in revers order **)
110 fun rev_deriv ctxt (t, r, (_, a)) = (ThmC.make_sym_rule ctxt r, (t, a));
111 fun steps_reverse ctxt asm_rls rs ro goal t =
112 (rev o (map (rev_deriv ctxt))) (do_one ctxt asm_rls rs ro goal t)
115 (** concatenate several steps **)
117 fun rev_deriv' ctxt (t, r, (t', a)) = (t', ThmC.make_sym_rule ctxt r, (t, a));
119 (* case fo = ifo excluded already in inform *)
120 fun steps ctxt rew_ord asm_rls rules fo ifo =
122 fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty
123 | derivat dt = (#1 o #3 o last_elem) dt
124 fun equal (_, _, (t1, _)) (_, _, (t2, _)) = t1 = t2
125 val fod = do_one ctxt asm_rls rules (snd rew_ord) NONE fo
126 val ifod = do_one ctxt asm_rls rules (snd rew_ord) NONE ifo
129 ([], []) => if fo = ifo then (true, []) else (false, [])
130 | (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, [])
131 | ([], ifod) => if fo = derivat ifod then (true, ((map (rev_deriv' ctxt)) o rev) ifod) else (false, [])
133 if derivat fod = derivat ifod (*common normal form found*) then
135 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)
136 in (true, fod' @ (map (rev_deriv' ctxt) rifod')) end
140 (** embed a derivation into the Ctree **)
142 fun embed tacis (pt, pos as (p, Pos.Frm)) =
143 (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj
144 and transfer the istate (from _after_ compare_deriv) from Frm to Res*)
146 val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of
147 (SOME (ist, ctxt), _) => (ist, ctxt)
148 | (NONE, _) => raise ERROR "Derive.embed Frm: uncovered case get_obj"
149 val (res, asm) = ((State_Steps.result ctxt) o last_elem) tacis
150 val form = Ctree.get_obj Ctree.g_form pt p
151 (*val p = lev_on p; ---------------only difference to (..,Res) below*)
152 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' form, (pos, (Istate_Def.Uistate, ctxt))) ::
153 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
154 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))]
155 val {rew_rls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
156 val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res))
157 val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id rew_rls))
158 val pt = Ctree.update_branch pt p Ctree.TransitiveB
159 in (c, (pt, pos)) end
160 | embed tacis (pt, (p, Pos.Res)) =
161 (*inform at Res: append a Transitive-PrfObj
162 and transfer the istate (from _after_ compare_deriv) from Res to new Res*)
164 val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of
165 (_, SOME (ist, ctxt)) => (ist, ctxt)
166 | (_, NONE) => raise ERROR "Derive.embed Frm: uncovered case get_obj"
167 val (res, asm) = ((State_Steps.result ctxt) o last_elem) tacis
168 val (f, _) = Ctree.get_obj Ctree.g_result pt p
169 val p = Pos.lev_on p(*---------------only difference to (..,Frm) above*);
170 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::
171 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
172 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];
173 val {rew_rls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
174 val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res))
175 val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id rew_rls))
176 val pt = Ctree.update_branch pt p Ctree.TransitiveB
177 in (c, (pt, pos)) end
178 | embed _ _ = raise ERROR "Derive.embed: uncovered definition"