59 (* data for creating a new node in ctree; designed for use as: |
59 (* data for creating a new node in ctree; designed for use as: |
60 fun ass* scrstate steps = / ... case ass* scrstate steps of / |
60 fun ass* scrstate steps = / ... case ass* scrstate steps of / |
61 Assoc (scrstate, steps) => ... ass* scrstate steps *) |
61 Assoc (scrstate, steps) => ... ass* scrstate steps *) |
62 type step = |
62 type step = |
63 tac_ (*transformed from associated tac *) |
63 tac_ (*transformed from associated tac *) |
64 * mout (*result with indentation etc. *) |
64 * Ctree.mout (*result with indentation etc. *) |
65 * ptree (*containing node created by tac_ + resp. scrstate *) |
65 * ptree (*containing node created by tac_ + resp. scrstate *) |
66 * pos' (*position in ptree; ptree * pos' is the proofstate *) |
66 * pos' (*position in ptree; ptree * pos' is the proofstate *) |
67 * pos' list; (*of ptree-nodes probably cut (by fst tac_) *) |
67 * pos' list; (*of ptree-nodes probably cut (by fst tac_) *) |
68 |
68 |
69 fun rule2thm'' (Thm (id, thm)) = (id, thm) : thm'' |
69 fun rule2thm'' (Thm (id, thm)) = (id, thm) : thm'' |
78 val thy = assoc_thy thy' |
78 val thy = assoc_thy thy' |
79 val ctxt = get_ctxt pt p |> insert_assumptions am |
79 val ctxt = get_ctxt pt p |> insert_assumptions am |
80 val m = Rewrite' (thy', ro, er, pa, rule2thm'' r, f, (f', am)) |
80 val m = Rewrite' (thy', ro, er, pa, rule2thm'' r, f, (f', am)) |
81 val is = RrlsState (f', f'', rss, rts) |
81 val is = RrlsState (f', f'', rss, rts) |
82 val p = case p of (_, Frm) => p | (p', Res) => (lev_on p', Res) | _ => error "rts2steps: p1" |
82 val p = case p of (_, Frm) => p | (p', Res) => (lev_on p', Res) | _ => error "rts2steps: p1" |
83 val (p', cid, mout, pt') = generate1 thy m (is, ctxt) p pt |
83 val (p', cid, mout, pt') = Ctree.generate1 thy m (is, ctxt) p pt |
84 in (is, (m, mout, pt', p', cid) :: steps) end |
84 in (is, (m, mout, pt', p', cid) :: steps) end |
85 | rts2steps steps ((pt, p) ,(f, f'', rss, rts), (thy', ro, er, pa)) ((r, (f', am)) :: rts') = |
85 | rts2steps steps ((pt, p) ,(f, f'', rss, rts), (thy', ro, er, pa)) ((r, (f', am)) :: rts') = |
86 let |
86 let |
87 val thy = assoc_thy thy' |
87 val thy = assoc_thy thy' |
88 val ctxt = get_ctxt pt p |> insert_assumptions am |
88 val ctxt = get_ctxt pt p |> insert_assumptions am |
89 val m = Rewrite' (thy', ro, er, pa, rule2thm'' r, f, (f', am)) |
89 val m = Rewrite' (thy', ro, er, pa, rule2thm'' r, f, (f', am)) |
90 val is = RrlsState (f', f'', rss, rts) |
90 val is = RrlsState (f', f'', rss, rts) |
91 val p = case p of (_, Frm) => p | (p', Res) => (lev_on p', Res) | _ => error "rts2steps: p1" |
91 val p = case p of (_, Frm) => p | (p', Res) => (lev_on p', Res) | _ => error "rts2steps: p1" |
92 val (p', cid, mout, pt') = generate1 thy m (is, ctxt) p pt |
92 val (p', cid, mout, pt') = Ctree.generate1 thy m (is, ctxt) p pt |
93 in rts2steps ((m, mout, pt', p', cid)::steps) |
93 in rts2steps ((m, mout, pt', p', cid)::steps) |
94 ((pt', p'), (f', f'', rss, rts), (thy', ro, er, pa)) rts' |
94 ((pt', p'), (f', f'', rss, rts), (thy', ro, er, pa)) rts' |
95 end |
95 end |
96 | rts2steps _ _ _ = error "rts2steps: uncovered fun-def" |
96 | rts2steps _ _ _ = error "rts2steps: uncovered fun-def" |
97 |
97 |
663 | _ => error ("assy: call by " ^ pos'2str (p,p_)); |
663 | _ => error ("assy: call by " ^ pos'2str (p,p_)); |
664 in |
664 in |
665 case assod pt d m stac of |
665 case assod pt d m stac of |
666 Ass (m,v') => |
666 Ass (m,v') => |
667 let val (p'',c',f',pt') = |
667 let val (p'',c',f',pt') = |
668 generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt; |
668 Ctree.generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt; |
669 in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end |
669 in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end |
670 | AssWeak (m,v') => |
670 | AssWeak (m,v') => |
671 let val (p'',c',f',pt') = |
671 let val (p'',c',f',pt') = |
672 generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,false), ctxt) (p',p_) pt; |
672 Ctree.generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,false), ctxt) (p',p_) pt; |
673 in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end |
673 in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end |
674 | NotAss => |
674 | NotAss => |
675 (case ap of (*switch for Or: 1st AssOnly, 2nd AssGen*) |
675 (case ap of (*switch for Or: 1st AssOnly, 2nd AssGen*) |
676 AssOnly => (NasNap (v, E)) |
676 AssOnly => (NasNap (v, E)) |
677 | _ => |
677 | _ => |
678 (case applicable_in (p,p_) pt (stac2tac pt (assoc_thy thy') stac) of |
678 (case applicable_in (p,p_) pt (stac2tac pt (assoc_thy thy') stac) of |
679 Chead.Appl m' => |
679 Chead.Appl m' => |
680 let |
680 let |
681 val is = (E,l,a',tac_2res m',S,false(*FIXXXME.WN0?*)) |
681 val is = (E,l,a',tac_2res m',S,false(*FIXXXME.WN0?*)) |
682 val (p'',c',f',pt') = |
682 val (p'',c',f',pt') = |
683 generate1 (assoc_thy thy') m' (ScrState is, ctxt) (p',p_) pt; |
683 Ctree.generate1 (assoc_thy thy') m' (ScrState is, ctxt) (p', p_) pt; |
684 in NasApp (is,(m,f',pt',p'',c @ c')::ss) end |
684 in NasApp (is,(m,f',pt',p'',c @ c')::ss) end |
685 | Chead.Notappl _ => (NasNap (v, E)) |
685 | Chead.Notappl _ => (NasNap (v, E)) |
686 ) |
686 ) |
687 ) |
687 ) |
688 end) |
688 end) |
820 | locate_gen (thy',srls) (m:tac_) ((pt,p):ptree * pos') |
820 | locate_gen (thy',srls) (m:tac_) ((pt,p):ptree * pos') |
821 (scr as Prog (_ $ body),d) (ScrState (E,l,a,v,S,b), ctxt) = |
821 (scr as Prog (_ $ body),d) (ScrState (E,l,a,v,S,b), ctxt) = |
822 let val thy = assoc_thy thy'; |
822 let val thy = assoc_thy thy'; |
823 in case if l = [] orelse ( |
823 in case if l = [] orelse ( |
824 (*init.in solve..Apply_Method...*)(last_elem o fst) p = 0 andalso snd p = Res) |
824 (*init.in solve..Apply_Method...*)(last_elem o fst) p = 0 andalso snd p = Res) |
825 then (assy (thy',ctxt,srls,d,Aundef) ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]) body) |
825 then (assy (thy',ctxt,srls,d,Aundef) ((E,[R],a,v,S,b), [(m,Ctree.EmptyMout,pt,p,[])]) body) |
826 else (astep_up (thy',ctxt,srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) ) of |
826 else (astep_up (thy',ctxt,srls,scr,d) ((E,l,a,v,S,b), [(m,Ctree.EmptyMout,pt,p,[])]) ) of |
827 Assoc ((is as (_,_,_,_,_,strong_ass), ss as (_ :: _))) => |
827 Assoc ((is as (_,_,_,_,_,strong_ass), ss as (_ :: _))) => |
828 (if strong_ass |
828 (if strong_ass |
829 then (Steps (ScrState is, ss)) |
829 then (Steps (ScrState is, ss)) |
830 else |
830 else |
831 if rew_only ss (*andalso 'not strong_ass'= associated weakly*) |
831 if rew_only ss (*andalso 'not strong_ass'= associated weakly*) |
832 then |
832 then |
833 let |
833 let |
834 val (po,p_) = p |
834 val (po,p_) = p |
835 val po' = case p_ of Frm => po | Res => lev_on po | _ => error ("locate_gen " ^ pos_2str p_) |
835 val po' = case p_ of Frm => po | Res => lev_on po | _ => error ("locate_gen " ^ pos_2str p_) |
836 val (p'',c'',f'',pt'') = generate1 thy m (ScrState is, ctxt) (po',p_) pt |
836 val (p'',c'',f'',pt'') = Ctree.generate1 thy m (ScrState is, ctxt) (po',p_) pt |
837 in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end |
837 in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end |
838 else Steps (ScrState is, ss)) |
838 else Steps (ScrState is, ss)) |
839 |
839 |
840 | NasApp _ => NotLocatable |
840 | NasApp _ => NotLocatable |
841 | err => error ("not-found-in-script: NotLocatable from " ^ PolyML.makestring err) |
841 | err => error ("not-found-in-script: NotLocatable from " ^ PolyML.makestring err) |