111 (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*); |
111 (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*); |
112 "~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p, _))), ifo) = (([], [], (pt, pos_pred)), tm); |
112 "~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p, _))), ifo) = (([], [], (pt, pos_pred)), tm); |
113 val fo = Calc.current_formula ptp |
113 val fo = Calc.current_formula ptp |
114 val {rew_rls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)) |
114 val {rew_rls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)) |
115 val {rew_ord, asm_rls, rules, ...} = Rule_Set.rep rew_rls |
115 val {rew_ord, asm_rls, rules, ...} = Rule_Set.rep rew_rls |
116 val (found, der) = Derive.steps ctxt rew_ord asm_rls rules fo ifo; (*<---------------*) |
116 |
|
117 val (found, der) = |
|
118 Derive.steps ctxt rew_ord asm_rls rules fo ifo; (*<---------------*) |
|
119 (*//------------------ step into Derive.steps ----------------------------------------------\\*) |
|
120 "~~~~~ fun steps , args:"; val (ctxt, rew_ord, asm_rls, rules, fo, ifo) = |
|
121 (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 = Derive.do_one ctxt asm_rls rules (snd rew_ord) NONE fo |
|
126 val ifod = Derive.do_one ctxt asm_rls rules (snd rew_ord) NONE ifo |
|
127 val (fod, ifod) = |
|
128 (*case*) (fod, ifod) (*of*); |
|
129 (*if*) derivat fod = derivat ifod (*common normal form found*) (*then*); |
|
130 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod) |
|
131 |
|
132 (*/--- local to steps ---\*) |
|
133 fun rev_deriv' ctxt (t, r, (t', a)) = (t', ThmC.make_sym_rule_PIDE ctxt r, (t, a)); |
|
134 (*\--- local to steps ---/*) |
|
135 val return = (true, fod' @ (map |
|
136 (rev_deriv' ctxt) rifod')); |
|
137 "~~~~~ fun rev_deriv' , args:"; val (ctxt, (t, r, (t', a))) = (ctxt, nth 1 rifod'); |
|
138 |
|
139 val return = (t', |
|
140 ThmC.make_sym_rule_PIDE ctxt r, (t, a)); |
|
141 "~~~~~ fun make_sym_rule_PIDE , args:"; val (ctxt ,(Rule.Thm (thmID, thm))) = (ctxt, r); |
|
142 open ThmC |
|
143 val thm' = sym_thm thm |
|
144 val thmID' = case Symbol.explode thmID of |
|
145 "s" :: "y" :: "m" :: "_" :: id => implode id |
|
146 | "#" :: ":" :: _ => "#: " ^ string_of_thm_PIDE ctxt thm' |
|
147 | _ => "sym_" ^ thmID; |
|
148 (*-------------------- stop step into Derive.steps -------------------------------------------*) |
|
149 (*\\------------------ step into Derive.steps ----------------------------------------------//*) |
|
150 |
117 (*if*) found (*then*); |
151 (*if*) found (*then*); |
118 val tacis' = map (State_Steps.make_single rew_ord asm_rls) der; |
152 val tacis' = map (State_Steps.make_single rew_ord asm_rls) der; |
119 |
153 |
120 val (c', ptp) = |
154 val (c', ptp) = |
121 Derive.embed tacis' ptp; |
155 Derive.embed tacis' ptp; |
128 val p = Pos.lev_on p(*---------------only difference to (..,Frm) above*); |
162 val p = Pos.lev_on p(*---------------only difference to (..,Frm) above*); |
129 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) :: |
163 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) :: |
130 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm), |
164 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm), |
131 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))]; |
165 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))]; |
132 val {rew_rls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)) |
166 val {rew_rls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)) |
|
167 |
133 val (pt, c, pos as (p, _)) = |
168 val (pt, c, pos as (p, _)) = |
134 |
|
135 Solve_Step.s_add_general (rev tacis) (pt, [], (p, Res)); |
169 Solve_Step.s_add_general (rev tacis) (pt, [], (p, Res)); |
136 "~~~~~ fun s_add_general , args:"; val (tacis, (pt, c, _)) = ((rev tacis), (pt, [], (p, Res))); |
170 "~~~~~ fun s_add_general , args:"; val (tacis, (pt, c, _)) = ((rev tacis), (pt, [], (p, Res))); |
137 (*+*)length tacis = 8; |
171 (*+*)length tacis = 8; |
138 (*+*)if State_Steps.to_string ctxt tacis = "[\"\n" ^ |
172 (*+*)if State_Steps.to_string ctxt tacis = "[\"\n" ^ |
139 "( End_Trans, End_Trans' xxx, ( ([2, 6], Res), Pstate ([\"\n(e_e, x + 1 = 2)\", \"\n" ^ |
173 "( End_Trans, End_Trans' xxx, ( ([2, 6], Res), Pstate ([\"\n(e_e, x + 1 = 2)\", \"\n" ^ |
148 (*+*)then () else error "Derive.embed CHANGED"; |
182 (*+*)then () else error "Derive.embed CHANGED"; |
149 |
183 |
150 val (tacis', (_, tac_, (p, is))) = split_last tacis |
184 val (tacis', (_, tac_, (p, is))) = split_last tacis |
151 |
185 |
152 (*+*)val Begin_Trans' _ = tac_; |
186 (*+*)val Begin_Trans' _ = tac_; |
153 |
|
154 val (p',c',_,pt') = Specify_Step.add tac_ is (pt, p) |
|
155 (*-------------------- stop step into -------------------------------------------------------*) |
187 (*-------------------- stop step into -------------------------------------------------------*) |
156 (*\------------------- end step into -------------------------------------------------------/*) |
188 (*\------------------- end step into -------------------------------------------------------/*) |
|
189 |
|
190 val (p',c',_,pt') = |
|
191 Specify_Step.add tac_ is (pt, p); |
|
192 "~~~~~ fun add , args:"; val ((Tactic.Begin_Trans' t), l, (pt, (p, Frm))) = |
|
193 (tac_, is, (pt, p)); |
|
194 val (pt, c) = Ctree.cappend_form pt p l t |
|
195 val pt = Ctree.update_branch pt p Ctree.TransitiveB |
|
196 val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p |
|
197 val (pt, c') = Ctree.cappend_form pt p l t |
|
198 val return = ((p, Frm), c @ c', Test_Out.FormKF (UnparseC.term_in_ctxt ctxt t), pt) |
157 |
199 |
158 (*/--------------------- final test ----------------------------------------------------------\*) |
200 (*/--------------------- final test ----------------------------------------------------------\*) |
159 val (SOME (Uistate, ctxt_frm), SOME (ist_res, ctxt_res)) = get_obj g_loc (fst ptp''''') (fst (snd ptp''''')) |
201 val (SOME (Uistate, ctxt_frm), SOME (ist_res, ctxt_res)) = get_obj g_loc (fst ptp''''') (fst (snd ptp''''')) |
160 ; |
202 ; |
161 if |
203 if |
162 (ctxt_frm |> ContextC.get_assumptions |> UnparseC.terms) = "[\"precond_rootmet x\"]" |
204 (ctxt_frm |> ContextC.get_assumptions |> UnparseC.terms_in_ctxt ctxt) = "[precond_rootmet x]" |
163 andalso |
205 andalso |
164 (ctxt_res |> ContextC.get_assumptions |> UnparseC.terms) = "[\"precond_rootmet x\"]" |
206 (ctxt_res |> ContextC.get_assumptions |> UnparseC.terms_in_ctxt ctxt) = "[precond_rootmet x]" |
165 andalso |
207 andalso |
166 Istate.string_of ist_res = |
208 Istate.string_of ist_res = |
167 "Pstate ([\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\"], [], empty, NONE, \n2 + - 1 + x = 2, ORundef, false, true)" |
209 "Pstate ([\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\"], [], empty, NONE, \n2 + - 1 + x = 2, ORundef, false, true)" |
168 then () else error "/800-append-on-Frm.sml CHANGED"; |
210 then () else error "/800-append-on-Frm.sml CHANGED"; |
169 |
211 |