496 | Tac string => "Tac " |
496 | Tac string => "Tac " |
497 | User => "User" |
497 | User => "User" |
498 | End_Proof' => "End_Proof'" |
498 | End_Proof' => "End_Proof'" |
499 | _ => "tac2str not impl. for ?!"; |
499 | _ => "tac2str not impl. for ?!"; |
500 |
500 |
|
501 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls |
|
502 | rls_of (Rewrite_Set rls) = rls |
|
503 | rls_of tac = raise error ("rls_of: called with tac '"^tac2IDstr tac^"'"); |
|
504 |
501 fun thm_of_rew (Rewrite_Inst (subs,(thmID,_))) = |
505 fun thm_of_rew (Rewrite_Inst (subs,(thmID,_))) = |
502 (thmID, Some ((subs2subst (assoc_thy "Isac.thy") subs):subst)) |
506 (thmID, Some ((subs2subst (assoc_thy "Isac.thy") subs):subst)) |
503 | thm_of_rew (Rewrite (thmID,_)) = (thmID, None) |
507 | thm_of_rew (Rewrite (thmID,_)) = (thmID, None) |
504 | thm_of_rew (Rewrite_Asm (thmID,_)) = (thmID, None); |
508 | thm_of_rew (Rewrite_Asm (thmID,_)) = (thmID, None); |
505 |
509 |
507 (rls, Some ((subs2subst (assoc_thy "Isac.thy") subs):subst)) |
511 (rls, Some ((subs2subst (assoc_thy "Isac.thy") subs):subst)) |
508 | rls_of_rewset (Rewrite_Set rls) = (rls, None) |
512 | rls_of_rewset (Rewrite_Set rls) = (rls, None) |
509 | rls_of_rewset (Detail_Set rls) = (rls, None) |
513 | rls_of_rewset (Detail_Set rls) = (rls, None) |
510 | rls_of_rewset (Detail_Set_Inst (subs, rls)) = |
514 | rls_of_rewset (Detail_Set_Inst (subs, rls)) = |
511 (rls, Some ((subs2subst (assoc_thy "Isac.thy") subs):subst)); |
515 (rls, Some ((subs2subst (assoc_thy "Isac.thy") subs):subst)); |
|
516 |
|
517 fun Thm2Rewrite (Thm (thmID,_)) = Rewrite_Set thmID |
|
518 | Thm2Rewrite rule = |
|
519 raise error ("Thm2Rewrite: called with '" ^ rule2str rule ^ "'"); |
512 |
520 |
513 |
521 |
514 |
522 |
515 type fmz_ = cterm' list; |
523 type fmz_ = cterm' list; |
516 |
524 |
1074 in if null bs' then Nd (b, repl_app bs p (Nd (b', ns))) |
1082 in if null bs' then Nd (b, repl_app bs p (Nd (b', ns))) |
1075 else raise PTREE "ins_chn: pos mustNOT be overwritten" end |
1083 else raise PTREE "ins_chn: pos mustNOT be overwritten" end |
1076 | ins_chn ns (Nd (b, bs)) (p::ps) = |
1084 | ins_chn ns (Nd (b, bs)) (p::ps) = |
1077 Nd (b, repl_app bs p (ins_chn ns (nth p bs) ps)); |
1085 Nd (b, repl_app bs p (ins_chn ns (nth p bs) ps)); |
1078 |
1086 |
1079 print_depth 11;ins_chn;print_depth 3 (*###insert#########################*); |
1087 (* print_depth 11;ins_chn;print_depth 3; ###insert#########################*); |
1080 |
1088 |
1081 |
1089 |
1082 (** apply f to obj at pos, f: ppobj -> ppobj **) |
1090 (** apply f to obj at pos, f: ppobj -> ppobj **) |
1083 |
1091 |
1084 fun appl_to_node f (Nd (b,bs)) = Nd (f b, bs); |
1092 fun appl_to_node f (Nd (b,bs)) = Nd (f b, bs); |
1932 val _= writeln("####cut_bottom form='"^ |
1940 val _= writeln("####cut_bottom form='"^ |
1933 term2str (get_obj g_form pt'' [])) |
1941 term2str (get_obj g_form pt'' [])) |
1934 val _= writeln("####cut_bottom cuts#="^string_of_int (length cuts)^ |
1942 val _= writeln("####cut_bottom cuts#="^string_of_int (length cuts)^ |
1935 ", cuts="^pos's2str cuts)*) |
1943 ", cuts="^pos's2str cuts)*) |
1936 in ((pt'', cuts:pos' list), cutlevup b) end; |
1944 in ((pt'', cuts:pos' list), cutlevup b) end; |
1937 print_depth 3; |
|
1938 |
1945 |
1939 |
1946 |
1940 (*.go all levels from the bottom of 'pos' up to the root, |
1947 (*.go all levels from the bottom of 'pos' up to the root, |
1941 on each level compose the children of a node and accumulate the cut Nds |
1948 on each level compose the children of a node and accumulate the cut Nds |
1942 args |
1949 args |
1947 pos * posel -> : pos=path split for convenience |
1954 pos * posel -> : pos=path split for convenience |
1948 ptree -> : Nd the children of are under consideration on this call |
1955 ptree -> : Nd the children of are under consideration on this call |
1949 returns : |
1956 returns : |
1950 ptree * pos' list : the updated parent-Nd and the pos's of the Nds cut |
1957 ptree * pos' list : the updated parent-Nd and the pos's of the Nds cut |
1951 .*) |
1958 .*) |
1952 print_depth 99; |
|
1953 fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:posel) (Nd (b, bs)) = |
1959 fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:posel) (Nd (b, bs)) = |
1954 let (*divide level into 3 parts...*) |
1960 let (*divide level into 3 parts...*) |
1955 val keep = take (p - 1, bs) |
1961 val keep = take (p - 1, bs) |
1956 (*val pt' comes as argument from below*) |
1962 (*val pt' comes as argument from below*) |
1957 val (tail, tp) = (takerest (p, bs), |
1963 val (tail, tp) = (takerest (p, bs), |
1993 in if null P then (pt', cuts) |
1999 in if null P then (pt', cuts) |
1994 else let val (P, p) = split_last P |
2000 else let val (P, p) = split_last P |
1995 in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P) |
2001 in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P) |
1996 end |
2002 end |
1997 end; |
2003 end; |
1998 print_depth 3; |
|
1999 (*########\ inserted from ctreeNEW.sml /#################################**) |
|
2000 |
2004 |
2001 fun append_atomic p l f r f' s pt = |
2005 fun append_atomic p l f r f' s pt = |
2002 let (**val _= writeln("#@append_atomic: pos ="^pos2str p)**) |
2006 let (**val _= writeln("#@append_atomic: pos ="^pos2str p)**) |
2003 val (iss, f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac |
2007 val (iss, f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac |
2004 then (*after Take*) |
2008 then (*after Take*) |
2005 ((fst (get_obj g_loc pt p), Some l), |
2009 ((fst (get_obj g_loc pt p), Some l), |
2006 get_obj g_form pt p) |
2010 get_obj g_form pt p) |
2007 (*040223 else ((Some l, None), f)*) |
|
2008 else ((None, Some l), f) |
2011 else ((None, Some l), f) |
2009 in insert (PrfObj {cell = None, |
2012 in insert (PrfObj {cell = None, |
2010 form = f, |
2013 form = f, |
2011 tac = r, |
2014 tac = r, |
2012 loc = iss, |
2015 loc = iss, |
2013 branch= NoBranch, |
2016 branch= NoBranch, |
2014 result= f', |
2017 result= f', |
2015 ostate= s}) pt p end; |
2018 ostate= s}) pt p end; |
|
2019 |
2016 |
2020 |
2017 (*20.8.02: cappend_* FIXXXXME cut branches below cannot be decided here: |
2021 (*20.8.02: cappend_* FIXXXXME cut branches below cannot be decided here: |
2018 detail - generate - cappend: inserted, not appended !!! |
2022 detail - generate - cappend: inserted, not appended !!! |
2019 |
2023 |
2020 cut decided in applicable_in !?! |
2024 cut decided in applicable_in !?! |