1 (* Title: Interpret/derive.sml
2 Author: Walther Neuper 2019
3 (c) due to copyright terms
5 Derive makes (term * rule * result) steps (= derivation) for term transformations,
6 which cannot be done by rewriting, e.g cancellation of polynomials.
11 (*TODO cleanup signature*)
16 val do_one : theory -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ ->
17 term option -> term -> derivation
18 (*val reverse_deriv *)
19 val steps_reverse : theory -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ ->
20 term option -> term -> deri list
22 val steps : Rule_Def.rew_ord -> Rule_Set.T -> Rule.rule list -> term -> term ->
24 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
26 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
27 val trtas2str : (term * Rule.rule * (term * term list)) list -> string
28 val deriv2str : (term * Rule.rule * (term * term list)) list -> string
29 val rev_deriv' : 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c)
30 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
34 structure Derive(**): DERIVE(**) =
38 (** the triple for a step **)
40 type der = (* derivation for inserting one level of nodes into the Ctree *)
41 ( term * (* where the rule is applied to *)
42 Rule.rule * (* rule to be applied *)
43 ( term * (* resulting from rule application *)
44 term list));(* assumptions resulting from rule application *)
45 type deri = Rule.rule * (term * term list)
46 type derivation = der list
48 fun trta2str (t, r, (t', a)) =
49 "\n(" ^ UnparseC.term t ^ ", " ^ Rule.to_string_short r ^ ", (" ^ UnparseC.term t' ^ ", " ^ UnparseC.terms a ^ "))"
50 fun trtas2str trtas = (strs2str o (map trta2str)) trtas
51 val deriv2str = trtas2str
53 (** make one triple towards the goal term **)
56 (tracing ("do_one exceeds " ^ int2str (! Rewrite.lim_deriv) ^ "with derivation =\n");
57 tracing (deriv2str rts));
59 if not (! Rewrite.trace_on) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");
61 if ! Rewrite.trace_on then tracing ("=== rewrites to: " ^ UnparseC.term t') else ();
63 if not (! Rewrite.trace_on) then () else tracing ("### trying calc. \"" ^ op_^"\"");
65 if not (! Rewrite.trace_on) then () else tracing("=== calc. to: " ^ UnparseC.term t')
67 fun do_one thy erls rs ro goal tt =
69 datatype switch = Appl | Noap (* TODO: unify with version in Rewrite *)
70 fun rew_once _ rts t Noap [] =
71 (case goal of NONE => rts | SOME _ =>
72 raise ERROR ("do_one: no derivation for " ^ UnparseC.term t))
73 | rew_once lim rts t Appl [] = rew_once lim rts t Noap rs
74 (*| Seq _ => rts) FIXXXXXME 14.3.03*)
75 | rew_once lim rts t apno rs' =
77 NONE => rew_or_calc lim rts t apno rs'
78 | SOME g => if g = t then rts else rew_or_calc lim rts t apno rs')
79 and rew_or_calc lim rts t apno (rrs' as (r :: rs')) =
84 Rule.Thm (thmid, tm) =>
86 case Rewrite.rewrite_ thy ro erls true tm t of
87 NONE => rew_once lim rts t apno rs'
89 (msg_3 t'; rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))
90 | Rule.Eval (c as (op_, _)) =>
92 case Eval.adhoc_thm thy c (TermC.uminus_to_string t) of
93 NONE => rew_once lim rts t apno rs'
96 val (t', a') = case Rewrite.rewrite_ thy ro erls true tm t of
98 | NONE => raise ERROR "adhoc_thm: NONE"
100 val r' = Rule.Thm (thmid, tm)
101 in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end)
102 handle _ => raise ERROR "derive_norm, Eval: no rewrite")
104 (case Rewrite.rewrite_set_ thy true rls t of
105 NONE => rew_once lim rts t apno rs'
106 | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')
107 | rule => raise ERROR ("rew_once: uncovered case " ^ Rule.to_string rule))
108 | rew_or_calc _ _ _ _ [] = raise ERROR "rew_or_calc: called with []"
109 in rew_once (! Rewrite.lim_deriv) [] tt Noap rs end
112 (** concatenate several steps in revers order **)
114 fun rev_deriv (t, r, (_, a)) = (ThmC.make_sym_rule r, (t, a));
115 fun steps_reverse thy erls rs ro goal t =
116 (rev o (map rev_deriv)) (do_one thy erls rs ro goal t)
119 (** concatenate several steps **)
121 fun rev_deriv' (t, r, (t', a)) = (t', ThmC.make_sym_rule r, (t, a));
123 (* fo = ifo excluded already in inform *)
124 fun steps rew_ord erls rules fo ifo =
126 fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty
127 | derivat dt = (#1 o #3 o last_elem) dt
128 fun equal (_, _, (t1, _)) (_, _, (t2, _)) = t1 = t2
129 val fod = do_one (ThyC.Isac()) erls rules (snd rew_ord) NONE fo
130 val ifod = do_one (ThyC.Isac()) erls rules (snd rew_ord) NONE ifo
133 ([], []) => if fo = ifo then (true, []) else (false, [])
134 | (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, [])
135 | ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, [])
137 if derivat fod = derivat ifod (*common normal form found*) then
139 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)
140 in (true, fod' @ (map rev_deriv' rifod')) end