299 | is_calc _ = false; |
299 | is_calc _ = false; |
300 fun op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_)) = op_ |
300 fun op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_)) = op_ |
301 | op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_) $ _) = op_ |
301 | op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_) $ _) = op_ |
302 | op_of_calc t = error ("op_of_calc called with" ^ term2str t); |
302 | op_of_calc t = error ("op_of_calc called with" ^ term2str t); |
303 (* |
303 (* |
304 val Script sc = (#scr o rep_rls) Test_simplify; |
304 val Prog sc = (#scr o rep_rls) Test_simplify; |
305 val stacs = stacpbls sc; |
305 val stacs = stacpbls sc; |
306 |
306 |
307 val calcs = filter is_calc stacs; |
307 val calcs = filter is_calc stacs; |
308 val ids = map op_of_calc calcs; |
308 val ids = map op_of_calc calcs; |
309 map (curry assoc1 (!calclist')) ids; |
309 map (curry assoc1 (!calclist')) ids; |
330 ((inst_abs @{theory}) o term_of o the o (parse @{theory})) |
330 ((inst_abs @{theory}) o term_of o the o (parse @{theory})) |
331 "Script Stepwise (t_t::'z) =\ |
331 "Script Stepwise (t_t::'z) =\ |
332 \(Repeat\ |
332 \(Repeat\ |
333 \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \ |
333 \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \ |
334 \ (Try (Repeat (Rewrite add_commute False))) @@ \ |
334 \ (Try (Repeat (Rewrite add_commute False))) @@ \ |
335 \ (Try (Repeat (Rewrite real_mult_commute False)))) \ |
335 \ (Try (Repeat (Rewrite mult_commute False)))) \ |
336 \ t_t)"; |
336 \ t_t)"; |
337 val ScrStep $ _ $ _ = (*'z not affected by parse: 'a --> real*) |
337 val ScrStep $ _ $ _ = (*'z not affected by parse: 'a --> real*) |
338 ((inst_abs @{theory}) o term_of o the o (parse @{theory})) |
338 ((inst_abs @{theory}) o term_of o the o (parse @{theory})) |
339 "Script Stepwise (t_t::'z) =\ |
339 "Script Stepwise (t_t::'z) =\ |
340 \(Repeat\ |
340 \(Repeat\ |
341 \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \ |
341 \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \ |
342 \ (Try (Repeat (Rewrite add_commute False))) @@ \ |
342 \ (Try (Repeat (Rewrite add_commute False))) @@ \ |
343 \ (Try (Repeat (Rewrite real_mult_commute False)))) \ |
343 \ (Try (Repeat (Rewrite mult_commute False)))) \ |
344 \ t_t)"; |
344 \ t_t)"; |
345 (*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body |
345 (*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body |
346 are inconsistent !!!*) |
346 are inconsistent !!!*) |
347 val ScrStep_inst $ Term $ Bdv $ _=(*'z not affected by parse: 'a --> real*) |
347 val ScrStep_inst $ Term $ Bdv $ _=(*'z not affected by parse: 'a --> real*) |
348 ((inst_abs @{theory}) o term_of o the o (parse @{theory})) |
348 ((inst_abs @{theory}) o term_of o the o (parse @{theory})) |
349 "Script Stepwise_inst (t_t::'z) (v::real) =\ |
349 "Script Stepwise_inst (t_t::'z) (v::real) =\ |
350 \(Repeat\ |
350 \(Repeat\ |
351 \ ((Try (Repeat (Rewrite_Inst [(bdv,v)] real_diff_minus False))) @@ \ |
351 \ ((Try (Repeat (Rewrite_Inst [(bdv,v)] real_diff_minus False))) @@ \ |
352 \ (Try (Repeat (Rewrite_Inst [(bdv,v)] add_commute False))) @@\ |
352 \ (Try (Repeat (Rewrite_Inst [(bdv,v)] add_commute False))) @@\ |
353 \ (Try (Repeat (Rewrite_Inst [(bdv,v)] real_mult_commute False)))) \ |
353 \ (Try (Repeat (Rewrite_Inst [(bdv,v)] mult_commute False)))) \ |
354 \ t_t)"; |
354 \ t_t)"; |
355 val Repeat $ _ = |
355 val Repeat $ _ = |
356 ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) |
356 ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) |
357 "Repeat (Rewrite real_diff_minus False t)"; |
357 "Repeat (Rewrite real_diff_minus False t)"; |
358 val Try $ _ = |
358 val Try $ _ = |
378 "Rewrite_Set_Inst [(bdv,v)] real_diff_minus False"; |
378 "Rewrite_Set_Inst [(bdv,v)] real_diff_minus False"; |
379 val SEq $ _ $ _ $ _ = |
379 val SEq $ _ $ _ $ _ = |
380 ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) |
380 ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) |
381 " ((Try (Repeat (Rewrite real_diff_minus False))) @@ \ |
381 " ((Try (Repeat (Rewrite real_diff_minus False))) @@ \ |
382 \ (Try (Repeat (Rewrite add_commute False))) @@ \ |
382 \ (Try (Repeat (Rewrite add_commute False))) @@ \ |
383 \ (Try (Repeat (Rewrite real_mult_commute False)))) t"; |
383 \ (Try (Repeat (Rewrite mult_commute False)))) t"; |
384 |
384 |
385 fun rule2stac _ (Thm (thmID, _)) = |
385 fun rule2stac _ (Thm (thmID, _)) = |
386 Try $ (Repeat $ (Rew $ Free (thmID, IDtype) $ @{term False})) |
386 Try $ (Repeat $ (Rew $ Free (thmID, IDtype) $ @{term False})) |
387 | rule2stac calc (Calc (c, _)) = |
387 | rule2stac calc (Calc (c, _)) = |
388 Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype))) |
388 Try $ (Repeat $ (Cal $ Free (assoc_calc (calc ,c), IDtype))) |
472 calc = (*FIXXXME.040207 use also for met*) |
472 calc = (*FIXXXME.040207 use also for met*) |
473 ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o |
473 ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o |
474 (filter is_calc) o stacpbls) sc, |
474 (filter is_calc) o stacpbls) sc, |
475 rules = rules, |
475 rules = rules, |
476 errpatts=errpatts, |
476 errpatts=errpatts, |
477 scr = Script sc} end |
477 scr = Prog sc} end |
478 | prep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,rules,errpatts,...}) = |
478 | prep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,rules,errpatts,...}) = |
479 let val sc = (rules2scr_Seq (!calclist') rules) |
479 let val sc = (rules2scr_Seq (!calclist') rules) |
480 in Seq {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls, |
480 in Seq {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls, |
481 srls=srls, |
481 srls=srls, |
482 calc = ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o |
482 calc = ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o |
483 (filter is_calc) o stacpbls) sc, |
483 (filter is_calc) o stacpbls) sc, |
484 rules=rules, |
484 rules=rules, |
485 errpatts=errpatts, |
485 errpatts=errpatts, |
486 scr = Script sc} end |
486 scr = Prog sc} end |
487 | prep_rls (Rrls {id,...}) = |
487 | prep_rls (Rrls {id,...}) = |
488 error ("prep_rls not required for Rrls \"" ^ id ^ "\""); |
488 error ("prep_rls not required for Rrls \"" ^ id ^ "\""); |
489 (* |
489 |
490 val Script sc = (#scr o rep_rls o prep_rls) isolate_root; |
|
491 (tracing o term2str) sc; |
|
492 val Script sc = (#scr o rep_rls o prep_rls) isolate_bdv; |
|
493 (tracing o term2str) sc; |
|
494 *) |
|