walther@59906
|
1 |
(* Title: Interpret/derive.sml
|
walther@59934
|
2 |
Author: Walther Neuper
|
walther@59906
|
3 |
(c) due to copyright terms
|
walther@59906
|
4 |
|
walther@59934
|
5 |
Try to make (term * rule * result) steps (= derivation) by use of a Rule_Set.T.
|
walther@59934
|
6 |
Two purposes:
|
walther@59934
|
7 |
(1) derive steps from a given term towards another give term
|
walther@59934
|
8 |
(2) term transformations, which cannot be done by rewriting, e.g cancellation of polynomials.
|
walther@59906
|
9 |
*)
|
walther@59906
|
10 |
|
walther@59907
|
11 |
signature DERIVE =
|
walther@59906
|
12 |
sig
|
walther@59934
|
13 |
type rule_result
|
walther@59934
|
14 |
type step
|
walther@59907
|
15 |
type derivation
|
walther@59934
|
16 |
|
walther@59907
|
17 |
val do_one : theory -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ ->
|
walther@59907
|
18 |
term option -> term -> derivation
|
walther@59907
|
19 |
val steps_reverse : theory -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ ->
|
walther@59934
|
20 |
term option -> term -> rule_result list
|
walther@59907
|
21 |
val steps : Rule_Def.rew_ord -> Rule_Set.T -> Rule.rule list -> term -> term ->
|
walther@59934
|
22 |
bool * derivation
|
walther@59932
|
23 |
val embed: State_Steps.T -> Calc.T -> Pos.pos' list * Calc.T
|
wenzelm@60223
|
24 |
\<^isac_test>\<open>
|
walther@59906
|
25 |
val trtas2str : (term * Rule.rule * (term * term list)) list -> string
|
walther@59906
|
26 |
val deriv2str : (term * Rule.rule * (term * term list)) list -> string
|
walther@59906
|
27 |
val rev_deriv' : 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c)
|
wenzelm@60223
|
28 |
\<close>
|
walther@59906
|
29 |
end
|
walther@59906
|
30 |
|
walther@59906
|
31 |
(**)
|
walther@59907
|
32 |
structure Derive(**): DERIVE(**) =
|
walther@59906
|
33 |
struct
|
walther@59906
|
34 |
(**)
|
walther@59907
|
35 |
|
walther@59907
|
36 |
(** the triple for a step **)
|
walther@59907
|
37 |
|
walther@59934
|
38 |
type rule_result = Rule.rule * Calc.result;
|
walther@59934
|
39 |
type step = term * Rule.rule * Calc.result;
|
walther@59934
|
40 |
type derivation = step list;
|
walther@59906
|
41 |
|
walther@59906
|
42 |
fun trta2str (t, r, (t', a)) =
|
walther@59906
|
43 |
"\n(" ^ UnparseC.term t ^ ", " ^ Rule.to_string_short r ^ ", (" ^ UnparseC.term t' ^ ", " ^ UnparseC.terms a ^ "))"
|
walther@59906
|
44 |
fun trtas2str trtas = (strs2str o (map trta2str)) trtas
|
walther@59906
|
45 |
val deriv2str = trtas2str
|
walther@59906
|
46 |
|
walther@59934
|
47 |
|
walther@59907
|
48 |
(** make one triple towards the goal term **)
|
walther@59906
|
49 |
|
walther@59907
|
50 |
fun msg_1 rts =
|
walther@59907
|
51 |
(tracing ("do_one exceeds " ^ int2str (! Rewrite.lim_deriv) ^ "with derivation =\n");
|
walther@59907
|
52 |
tracing (deriv2str rts));
|
walther@59907
|
53 |
fun msg_2 thmid =
|
walther@59907
|
54 |
if not (! Rewrite.trace_on) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");
|
walther@59907
|
55 |
fun msg_3 t' =
|
walther@59907
|
56 |
if ! Rewrite.trace_on then tracing ("=== rewrites to: " ^ UnparseC.term t') else ();
|
walther@59907
|
57 |
fun msg_4 op_ =
|
walther@59907
|
58 |
if not (! Rewrite.trace_on) then () else tracing ("### trying calc. \"" ^ op_^"\"");
|
walther@59907
|
59 |
fun msg_5 t' =
|
walther@59907
|
60 |
if not (! Rewrite.trace_on) then () else tracing("=== calc. to: " ^ UnparseC.term t')
|
walther@59906
|
61 |
|
walther@59934
|
62 |
|
walther@59907
|
63 |
fun do_one thy erls rs ro goal tt =
|
walther@59906
|
64 |
let
|
walther@59907
|
65 |
datatype switch = Appl | Noap (* TODO: unify with version in Rewrite *)
|
walther@59906
|
66 |
fun rew_once _ rts t Noap [] =
|
walther@59907
|
67 |
(case goal of NONE => rts | SOME _ =>
|
walther@59934
|
68 |
raise ERROR ("Derive.do_one: no derivation for " ^ UnparseC.term t))
|
walther@59906
|
69 |
| rew_once lim rts t Appl [] = rew_once lim rts t Noap rs
|
walther@59906
|
70 |
| rew_once lim rts t apno rs' =
|
walther@59906
|
71 |
(case goal of
|
walther@59906
|
72 |
NONE => rew_or_calc lim rts t apno rs'
|
walther@59906
|
73 |
| SOME g => if g = t then rts else rew_or_calc lim rts t apno rs')
|
walther@59906
|
74 |
and rew_or_calc lim rts t apno (rrs' as (r :: rs')) =
|
walther@59906
|
75 |
if lim < 0
|
walther@59907
|
76 |
then (msg_1 rts; rts)
|
walther@59906
|
77 |
else
|
walther@59906
|
78 |
(case r of
|
walther@59906
|
79 |
Rule.Thm (thmid, tm) =>
|
walther@59907
|
80 |
(msg_2 thmid;
|
walther@59906
|
81 |
case Rewrite.rewrite_ thy ro erls true tm t of
|
walther@59906
|
82 |
NONE => rew_once lim rts t apno rs'
|
walther@59906
|
83 |
| SOME (t', a') =>
|
walther@59907
|
84 |
(msg_3 t'; rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))
|
walther@59906
|
85 |
| Rule.Eval (c as (op_, _)) =>
|
walther@59907
|
86 |
(msg_4 op_;
|
walther@59907
|
87 |
case Eval.adhoc_thm thy c (TermC.uminus_to_string t) of
|
walther@59906
|
88 |
NONE => rew_once lim rts t apno rs'
|
walther@59906
|
89 |
| SOME (thmid, tm) =>
|
walther@59906
|
90 |
(let
|
walther@59906
|
91 |
val (t', a') = case Rewrite.rewrite_ thy ro erls true tm t of
|
walther@59906
|
92 |
SOME ta => ta
|
walther@59907
|
93 |
| NONE => raise ERROR "adhoc_thm: NONE"
|
walther@59907
|
94 |
val _ = msg_5 t'
|
walther@59906
|
95 |
val r' = Rule.Thm (thmid, tm)
|
walther@59906
|
96 |
in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end)
|
walther@59907
|
97 |
handle _ => raise ERROR "derive_norm, Eval: no rewrite")
|
walther@59907
|
98 |
| Rule.Rls_ rls =>
|
walther@59906
|
99 |
(case Rewrite.rewrite_set_ thy true rls t of
|
walther@59906
|
100 |
NONE => rew_once lim rts t apno rs'
|
walther@59906
|
101 |
| SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')
|
walther@59907
|
102 |
| rule => raise ERROR ("rew_once: uncovered case " ^ Rule.to_string rule))
|
walther@59907
|
103 |
| rew_or_calc _ _ _ _ [] = raise ERROR "rew_or_calc: called with []"
|
walther@59906
|
104 |
in rew_once (! Rewrite.lim_deriv) [] tt Noap rs end
|
walther@59906
|
105 |
|
walther@59907
|
106 |
|
walther@59907
|
107 |
(** concatenate several steps in revers order **)
|
walther@59907
|
108 |
|
walther@59906
|
109 |
fun rev_deriv (t, r, (_, a)) = (ThmC.make_sym_rule r, (t, a));
|
walther@59907
|
110 |
fun steps_reverse thy erls rs ro goal t =
|
walther@59907
|
111 |
(rev o (map rev_deriv)) (do_one thy erls rs ro goal t)
|
walther@59906
|
112 |
|
walther@59907
|
113 |
|
walther@59907
|
114 |
(** concatenate several steps **)
|
walther@59907
|
115 |
|
walther@59906
|
116 |
fun rev_deriv' (t, r, (t', a)) = (t', ThmC.make_sym_rule r, (t, a));
|
walther@59906
|
117 |
|
walther@59906
|
118 |
(* fo = ifo excluded already in inform *)
|
walther@59907
|
119 |
fun steps rew_ord erls rules fo ifo =
|
walther@59906
|
120 |
let
|
walther@59906
|
121 |
fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty
|
walther@59906
|
122 |
| derivat dt = (#1 o #3 o last_elem) dt
|
walther@59907
|
123 |
fun equal (_, _, (t1, _)) (_, _, (t2, _)) = t1 = t2
|
walther@59907
|
124 |
val fod = do_one (ThyC.Isac()) erls rules (snd rew_ord) NONE fo
|
walther@59907
|
125 |
val ifod = do_one (ThyC.Isac()) erls rules (snd rew_ord) NONE ifo
|
walther@59906
|
126 |
in
|
walther@59906
|
127 |
case (fod, ifod) of
|
walther@59906
|
128 |
([], []) => if fo = ifo then (true, []) else (false, [])
|
walther@59906
|
129 |
| (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, [])
|
walther@59906
|
130 |
| ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, [])
|
walther@59906
|
131 |
| (fod, ifod) =>
|
walther@59906
|
132 |
if derivat fod = derivat ifod (*common normal form found*) then
|
walther@59906
|
133 |
let
|
walther@59906
|
134 |
val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)
|
walther@59906
|
135 |
in (true, fod' @ (map rev_deriv' rifod')) end
|
walther@59906
|
136 |
else (false, [])
|
walther@59906
|
137 |
end
|
walther@59906
|
138 |
|
walther@59934
|
139 |
(** embed a derivation into the Ctree **)
|
walther@59934
|
140 |
|
walther@59932
|
141 |
fun embed tacis (pt, pos as (p, Pos.Frm)) =
|
walther@59932
|
142 |
(*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402
|
walther@59932
|
143 |
and transfer the istate (from _after_ compare_deriv) from Frm to Res*)
|
walther@59932
|
144 |
let
|
walther@59932
|
145 |
val (res, asm) = (State_Steps.result o last_elem) tacis
|
walther@59932
|
146 |
val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of
|
walther@59932
|
147 |
(SOME (ist, ctxt), _) => (ist, ctxt)
|
walther@59934
|
148 |
| (NONE, _) => raise ERROR "Derive.embed Frm: uncovered case get_obj"
|
walther@59932
|
149 |
val form = Ctree.get_obj Ctree.g_form pt p
|
walther@59932
|
150 |
(*val p = lev_on p; ---------------only difference to (..,Res) below*)
|
walther@59932
|
151 |
val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' form, (pos, (Istate_Def.Uistate, ctxt))) ::
|
walther@59932
|
152 |
(State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
|
walther@59932
|
153 |
(Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))]
|
walther@60154
|
154 |
val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
|
walther@59932
|
155 |
val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res))
|
walther@59932
|
156 |
val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls))
|
walther@59932
|
157 |
val pt = Ctree.update_branch pt p Ctree.TransitiveB
|
walther@59932
|
158 |
in (c, (pt, pos)) end
|
walther@59932
|
159 |
| embed tacis (pt, (p, Pos.Res)) =
|
walther@59932
|
160 |
(*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ?
|
walther@59932
|
161 |
and transfer the istate (from _after_ compare_deriv) from Res to new Res*)
|
walther@59932
|
162 |
let
|
walther@59932
|
163 |
val (res, asm) = (State_Steps.result o last_elem) tacis
|
walther@59932
|
164 |
val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of
|
walther@59932
|
165 |
(_, SOME (ist, ctxt)) => (ist, ctxt)
|
walther@59934
|
166 |
| (_, NONE) => raise ERROR "Derive.embed Frm: uncovered case get_obj"
|
walther@59932
|
167 |
val (f, _) = Ctree.get_obj Ctree.g_result pt p
|
walther@59932
|
168 |
val p = Pos.lev_on p(*---------------only difference to (..,Frm) above*);
|
walther@59932
|
169 |
val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::
|
walther@59932
|
170 |
(State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
|
walther@59932
|
171 |
(Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];
|
walther@60154
|
172 |
val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
|
walther@59932
|
173 |
val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res))
|
walther@59932
|
174 |
val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls))
|
walther@59932
|
175 |
val pt = Ctree.update_branch pt p Ctree.TransitiveB
|
walther@59932
|
176 |
in (c, (pt, pos)) end
|
walther@59934
|
177 |
| embed _ _ = raise ERROR "Derive.embed: uncovered definition"
|
walther@59932
|
178 |
|
walther@59906
|
179 |
(**)end(**)
|