1229 in appl_obj (repl_loc (lform,Some x)) pt p end |
1229 in appl_obj (repl_loc (lform,Some x)) pt p end |
1230 |
1230 |
1231 | update_loc pt (p,_) x = |
1231 | update_loc pt (p,_) x = |
1232 let val (_,lres) = get_obj g_loc pt p |
1232 let val (_,lres) = get_obj g_loc pt p |
1233 in appl_obj (repl_loc (Some x,lres)) pt p end; |
1233 in appl_obj (repl_loc (Some x,lres)) pt p end; |
|
1234 (*WN050305 for handling cut_tree in cappend_atomic -- TODO redesign !*) |
|
1235 fun update_loc' pt p iss = appl_obj (repl_loc iss) pt p; |
1234 |
1236 |
1235 (*13.8.02--------------------------- |
1237 (*13.8.02--------------------------- |
1236 fun get_loc EmptyPtree _ = None |
1238 fun get_loc EmptyPtree _ = None |
1237 | get_loc pt (p,Res) = |
1239 | get_loc pt (p,Res) = |
1238 let val (lfrm,lres) = get_obj g_loc pt p |
1240 let val (lfrm,lres) = get_obj g_loc pt p |
1822 in if null P then (pt'', (cuts @ cuts'):pos' list) |
1824 in if null P then (pt'', (cuts @ cuts'):pos' list) |
1823 else let val (P, p) = split_last P |
1825 else let val (P, p) = split_last P |
1824 in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P) |
1826 in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P) |
1825 end |
1827 end |
1826 end; |
1828 end; |
1827 |
1829 |
1828 |
1830 |
1829 fun cut_tree pt (pos,_) = |
1831 fun cut_tree pt (pos,_) = |
1830 if not (existpt pos pt) |
1832 if not (existpt pos pt) |
1831 then (pt,[]) (*appending a formula never cuts anything*) |
1833 then (pt,[]) (*appending a formula never cuts anything*) |
1832 else let val (P, p) = split_last pos |
1834 else let val (P, p) = split_last pos |
1868 *) |
1870 *) |
1869 (writeln("##@cappend_atomic: pos ="^pos2str p); |
1871 (writeln("##@cappend_atomic: pos ="^pos2str p); |
1870 apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm)) |
1872 apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm)) |
1871 ); |
1873 ); |
1872 fun cappend_atomic pt p loc f r f' s = |
1874 fun cappend_atomic pt p loc f r f' s = |
1873 let val _= writeln("##@cappend_atomic: pos ="^pos2str p) |
1875 let val _= writeln("##@cappend_atomic: pos ="^pos2str p); |
1874 val _= writeln("##@cappend_atomic before cut_tree: loc ="^istate2str loc) |
1876 val _= writeln("##@cappend_atomic arg loc ="^istate2str loc); |
1875 val (pt', cs) = cut_tree pt (p,Frm) |
1877 val _= if existpt p pt |
|
1878 then writeln("##@cappend_atomic before cut_ loc ="^ |
|
1879 istates2str (get_obj g_loc pt p)) |
|
1880 else writeln("##@cappend_atomic pos not existent before cut_"); |
|
1881 val (pt', cs) = cut_tree pt (p,Frm); |
|
1882 val _= if existpt p pt' |
|
1883 then writeln("##@cappend_atomic after cut_ loc ="^ |
|
1884 istates2str (get_obj g_loc pt' p)) |
|
1885 else writeln("##@cappend_atomic pos not existent after cut_"); |
|
1886 val pt'' = append_atomic p loc f r f' s pt'; |
|
1887 val _= writeln("##@cappend_atomic after append: loc ="^ |
|
1888 istates2str (get_obj g_loc pt'' p)); |
|
1889 in (pt'', cs) end; |
|
1890 |
|
1891 fun cappend_atomic pt p loc f r f' s = |
|
1892 let val (pt', cs) = cut_tree pt (p,Frm) |
1876 val pt'' = append_atomic p loc f r f' s pt' |
1893 val pt'' = append_atomic p loc f r f' s pt' |
1877 val _= writeln("##@cappend_atomic after append: loc ="^ |
|
1878 istates2str (get_obj g_loc pt'' p)) |
|
1879 in (pt'', cs) end; |
1894 in (pt'', cs) end; |
|
1895 |
|
1896 fun cappend_atomic pt p ist_res f r f' s = |
|
1897 if existpt p pt andalso get_obj g_tac pt p=Empty_Tac |
|
1898 then (*after Take: transfer Frm and respective istate*) |
|
1899 let val (ist_form, f) = (get_loc pt (p,Frm), |
|
1900 get_obj g_form pt p) |
|
1901 val (pt, cs) = cut_tree pt (p,Frm) |
|
1902 val pt = append_atomic p e_istate f r f' s pt |
|
1903 val pt = update_loc' pt p (Some ist_form, Some ist_res) |
|
1904 in (pt, cs) end |
|
1905 else apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm)); |
|
1906 |
1880 |
1907 |
1881 (* called by Take *) |
1908 (* called by Take *) |
1882 fun append_form p l f pt = |
1909 fun append_form p l f pt = |
1883 (writeln("##@append_form: pos ="^pos2str p); |
1910 (writeln("##@append_form: pos ="^pos2str p); |
1884 insert (PrfObj {cell = [(*3.00. unused*)], |
1911 insert (PrfObj {cell = [(*3.00. unused*)], |