1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/ME/ctreeNEWdel.sml Fri Mar 04 19:11:15 2005 +0100
1.3 @@ -0,0 +1,341 @@
1.4 +(* use"../ME/ctreeNEW.sml";
1.5 + use"ME/ctreeNEW.sml";
1.6 + use"ctreeNEW.sml";
1.7 + *)
1.8 +
1.9 +
1.10 +(*.get all positions in a ptree until ([],Res) or ostate=Incomplete
1.11 +val get_allp = fn :
1.12 + pos' list -> : accumulated, start with []
1.13 + pos -> : the offset for subtrees wrt the root
1.14 + ptree -> : (sub)tree
1.15 + pos' : initialization (the last pos' before ...)
1.16 + -> pos' list : of positions in this (sub) tree (relative to the root)
1.17 +.*)
1.18 +(*###################################################################*)
1.19 +(* val (cuts, P, pt, pos) = ([], [3], get_nd pt [3], ([], Frm):pos');
1.20 + val (cuts, P, pt, pos) = ([], [2], get_nd pt [2], ([], Frm):pos');
1.21 + length (children pt);
1.22 + *)
1.23 +fun get_allp (cuts:pos' list) (P:pos, pos:pos') pt =
1.24 + (let val nxt = move_dn [] pt pos (*exn if Incomplete reached*)
1.25 + in if nxt <> ([],Res)
1.26 + then get_allp (cuts @ [nxt]) (P, nxt) pt
1.27 + else (map (apfst (curry op@ P)) (cuts @ [nxt])): pos' list
1.28 + end) handle PTREE _ => (map (apfst (curry op@ P)) cuts);
1.29 +(*###################################################################*)
1.30 +
1.31 +
1.32 +
1.33 +(*----OLD-----*)
1.34 +fun get_allps (cuts: pos' list) (P:pos) [] = cuts
1.35 + | get_allps cuts P (pt::pts) =
1.36 + let val cuts' =
1.37 + get_allp [] (P, ([], Frm)) pt
1.38 + in get_allps (cuts @ cuts') (lev_on P) pts end;
1.39 +
1.40 +print_depth 11;
1.41 +(* val (cuts: pos' list, P, pt::pts) = ([], [1], children pt);
1.42 + val cuts' = get_allp [] P pt ([], Frm);
1.43 + val (cuts: pos' list, P, pt::pts) = (cuts @ cuts', lev_on P, pts);
1.44 + val cuts' = get_allp [] P pt ([], Frm);
1.45 + length (children pt);
1.46 + *)
1.47 +(*the pts are assumed to be on the same level*)
1.48 +fun get_allps (cuts: pos' list) (P:pos) [] = cuts
1.49 + | get_allps cuts P (pt::pts) =
1.50 + let val below = get_allp [] (P, ([], Frm)) pt
1.51 + val levfrm =
1.52 + if is_pblnd pt
1.53 + then (P, Pbl)::below
1.54 + else if last_elem P = 1
1.55 + then (P, Frm)::below
1.56 + else (*Trans*) below
1.57 + val levres = levfrm @ (if null below then [(P, Res)] else [])
1.58 + in get_allps (cuts @ levres) (lev_on P) pts end;
1.59 +
1.60 +
1.61 +
1.62 +print_depth 11; move_dn; print_depth 3;
1.63 +print_depth 11; get_allpos'; print_depth 3;
1.64 +
1.65 +
1.66 +(**.these 2 funs decide on how far cut_tree goes.**)
1.67 +(*.shall the nodes _after_ the pos to be inserted at be deleted?.*)
1.68 +fun test_trans (PrfObj{branch = Transitive,...}) = true
1.69 + | test_trans (PrfObj{branch = NoBranch,...}) = true
1.70 + | test_trans (PblObj{branch = Transitive,...}) = true
1.71 + | test_trans (PblObj{branch = NoBranch,...}) = true
1.72 + | test_trans _ = false;
1.73 +(*.shall cutting be continued on the higher level(s)?
1.74 + the Nd regarded will NOT be changed.*)
1.75 +fun cutlevup (PblObj _) = false (*for tests of LK0502*)
1.76 + | cutlevup _ = true;
1.77 +
1.78 +(*cut_bottom new S(603)..(608)
1.79 +cut the level at the bottom of the pos (used by cappend_...)
1.80 +and handle the parent in order to avoid extra case for root
1.81 +fn: ptree -> : the _whole_ ptree for cut_levup
1.82 + pos * posel -> : the pos after split_last
1.83 + ptree -> : the parent of the Nd to be cut
1.84 +return
1.85 + (ptree * : the updated ptree
1.86 + pos' list) * : the pos's cut
1.87 + bool : cutting shall be continued on the higher level(s)
1.88 +*)
1.89 +(**############# 2nd get_allp finished############################**)
1.90 +(* val (Nd (b, bs)) = get_nd pt P;
1.91 + *)
1.92 +print_depth 11;
1.93 +fun cut_bottom (P:pos, p:posel) (Nd (b, bs)) =
1.94 + if p > length bs
1.95 + then ((pt', []), cutlevup b)
1.96 + else
1.97 + let (*divide level into 3 parts...*)
1.98 + val keep = take (p - 1, bs)
1.99 + val pt' as Nd (_,bs') = nth p bs
1.100 + (*^^^^^_here_ will be 'insert'ed by 'append_..'*)
1.101 + val (tail, tp) = (takerest (p, bs),
1.102 + if null (takerest (p, bs)) then 0 else p + 1)
1.103 + val (children, cuts) =
1.104 + if test_trans b
1.105 + then (keep,
1.106 + (if is_pblnd pt' then [(P @ [p], Pbl)] else [])
1.107 + @ (get_allp [] (P @ [p], (P, Frm)) pt')
1.108 + @ (get_allps [] (P @ [p+1]) tail))
1.109 + else (keep @ [(*'insert'ed by 'append_..'*)] @ tail,
1.110 + get_allp [] (P @ [p], (P, Frm)) pt')
1.111 + val (pt'', cuts) =
1.112 + if cutlevup b
1.113 + then (Nd (del_res b, children),
1.114 + cuts @ (if g_ostate b = Incomplete then []
1.115 + else [(P,Res)]))
1.116 + else (Nd (b, children), cuts)
1.117 + (*val _= writeln("####cut_bottom (P, p)="^pos2str (P @ [p])^
1.118 + ", Nd=.............................................")
1.119 + val _= show_pt pt''
1.120 + val _= writeln("####cut_bottom form='"^
1.121 + term2str (get_obj g_form pt'' []))
1.122 + val _= writeln("####cut_bottom cuts#="^string_of_int (length cuts)^
1.123 + ", cuts="^pos's2str cuts)*)
1.124 + in ((pt'', cuts:pos' list), cutlevup b) end;
1.125 +print_depth 3;
1.126 +(**######################################################################**);
1.127 +(*.go all levels from the bottom of 'pos' up to the root,
1.128 + on each level compose the children of a node and accumulate the cut Nds
1.129 +args
1.130 + pos' list -> : for accumulation
1.131 + bool -> : cutting shall be continued on the higher level(s)
1.132 + ptree -> : the whole ptree for 'get_nd pt P' on each level
1.133 + ptree -> : the Nd from the lower level for insertion at path
1.134 + pos * posel -> : pos=path split for convenience
1.135 + ptree -> : Nd the children of are under consideration on this call
1.136 +returns :
1.137 + ptree * pos' list : the updated parent-Nd and the pos's of the Nds cut
1.138 +.*)
1.139 +print_depth 99;
1.140 +fun cut_levup cuts clevup pt pt' (P:pos, p:posel) (pt'' as Nd (b, []))=
1.141 + if null P then (pt'', cuts:pos' list)
1.142 + else let val (P, p) = split_last P
1.143 + val clevup' = if clevup then cutlevup b else false
1.144 + in cut_levup cuts clevup' pt pt'' (P, p) (get_nd pt P)
1.145 + end
1.146 +
1.147 + | cut_levup cuts clevup pt pt' (P, p) (Nd (b, bs)) =
1.148 + if p > length bs
1.149 + then
1.150 +
1.151 + else
1.152 + let (*divide level into 3 parts...*)
1.153 + val keep = take (p - 1, bs)
1.154 + (*val pt' comes as argument from below*)
1.155 + val (tail, tp) = (takerest (p, bs),
1.156 + if null (takerest (p, bs)) then 0 else p + 1)
1.157 + val (children, cuts') =
1.158 + if clevup
1.159 + then (keep @ [pt'], get_allps [] (P @ [p+1]) tail)
1.160 + else (keep @ [pt'] @ tail, [])
1.161 + val clevup' = if clevup then cutlevup b else false
1.162 + (*the first Nd with false stops cutting on all levels above*)
1.163 + val (pt'', cuts') =
1.164 + if clevup'
1.165 + then (Nd (del_res b, children),
1.166 + cuts' @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
1.167 + else (Nd (b, children), cuts')
1.168 + (*val _= writeln("#####cut_levup clevup= "^bool2str clevup)
1.169 + val _= writeln("#####cut_levup cutlevup b= "^bool2str (cutlevup b))
1.170 + val _= writeln("#####cut_levup (P, p)="^pos2str (P @ [p])^
1.171 + ", Nd=.............................................")
1.172 + val _= show_pt pt''
1.173 + val _= writeln("#####cut_levup form='"^
1.174 + term2str (get_obj g_form pt'' []))
1.175 + val _= writeln("#####cut_levup cuts#="^string_of_int (length cuts)^
1.176 + ", cuts="^pos's2str cuts)*)
1.177 + in if null P then (pt'', cuts @ cuts')
1.178 + else let val (P, p) = split_last P
1.179 + in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P)
1.180 + end
1.181 + end;
1.182 +print_depth 3;
1.183 +(**######################################################################**);
1.184 +(* use"ME/ctreeNEW.sml";
1.185 + use"ctreeNEW.sml";
1.186 + *)
1.187 +print_depth 99;
1.188 +(* val (pos,_) = ([2],1234);
1.189 + *)
1.190 +fun cut_tree pt (pos,_) =
1.191 + (let val (P, p) = split_last pos
1.192 + val ((pt', cuts), clevup) = cut_bottom (P, p) (get_nd pt P)
1.193 + (* pt' is the updated parent of the Nd to cappend_..*)
1.194 + in if null P then (pt', cuts)
1.195 + else let val (P, p) = split_last P
1.196 + in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P)
1.197 + end
1.198 + end) handle _ => raise error "error in cut_tree";
1.199 +print_depth 3;
1.200 +
1.201 +
1.202 +
1.203 +(*######## eval from here ##########################################**)
1.204 +(*######## eval from here ##########################################**)
1.205 +(*######## eval from here ##########################################**)
1.206 +
1.207 +fun append_atomic p l f r f' s pt =
1.208 + let (**)val _= writeln("##append_atomic: pos ="^pos2str p)(**)
1.209 + val (iss, f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
1.210 + then (*after Take*)
1.211 + ((fst (get_obj g_loc pt p), Some l),
1.212 + get_obj g_form pt p)
1.213 + (*040223 else ((Some l, None), f)*)
1.214 + else ((None, Some l), f)
1.215 + in insert (PrfObj {cell = [(*3.00. unused*)],
1.216 + form = f,
1.217 + tac = r,
1.218 + loc = iss,
1.219 + branch= NoBranch,
1.220 + result= f',
1.221 + ostate= s}) pt p end;
1.222 +
1.223 +(*20.8.02: cappend_* FIXXXXME cut branches below cannot be decided here:
1.224 + detail - generate - cappend: inserted, not appended !!!
1.225 +
1.226 + cut decided in applicable_in !?!
1.227 +*)
1.228 +fun cappend_atomic pt p loc f r f' s =
1.229 + let val _= writeln("#cappend_atomic: pos ="^pos2str p)
1.230 + val (pt',c) = cut_tree pt (p,Frm)
1.231 + val _= writeln("#cappend_atomic: after cut")
1.232 + val pt'' = append_atomic p loc f r f' s pt'
1.233 + in (pt'',c) end;
1.234 +fun cappend_atomic pt p loc f r f' s =
1.235 +(* val (pt, p, loc, f, r, f', s) =
1.236 + (pt,p,l,f,Rewrite_Set_Inst (subst2subs subs',id_rls rls'),
1.237 + (f',asm),Complete);
1.238 + *)
1.239 +((**)writeln("###cappend_atomic: pos ="^pos2str p);(**)
1.240 + apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm))
1.241 +);
1.242 +
1.243 +(* called by Take *)
1.244 +fun append_form p l f pt =
1.245 +(writeln("###append_form: pos ="^pos2str p);
1.246 + insert (PrfObj {cell = [(*3.00. unused*)],
1.247 + form = (*if existpt p pt
1.248 + andalso get_obj g_tac pt p = Empty_Tac
1.249 + (*distinction from 'old' (+complete!) pobjs*)
1.250 + then get_obj g_form pt p else*) f,
1.251 + tac = Empty_Tac,
1.252 + loc = (Some l, None),
1.253 + branch= NoBranch,
1.254 + result= (e_term,[]),
1.255 + ostate= Incomplete}) pt p
1.256 +);
1.257 +(* val (p,loc,f) = ([1], e_istate, str2term "x + 1 = 2");
1.258 + val (p,loc,f) = (fst p, e_istate, str2term "-1 + x = 0");
1.259 + *)
1.260 +fun cappend_form pt p loc f =
1.261 +(writeln("###cappend_f rm: pos ="^pos2str p);
1.262 + apfst (append_form p loc f) (cut_tree pt (p,Frm))
1.263 +);
1.264 +fun cappend_form pt p loc f =
1.265 + let val _= writeln("#capp nd_form: pos ="^pos2str p)
1.266 + val (pt',c) = cut_tree pt (p,Frm)
1.267 + val _= writeln("#cappend_form: after cut")
1.268 + val pt'' = append_form p loc f pt'
1.269 + val _= writeln("#cappend_form: after append_form")
1.270 + in (pt'',c) end;
1.271 +
1.272 +
1.273 +fun append_result pt p l f s =
1.274 +((*writeln("###append_result: pos ="^pos2str p);*)
1.275 + (appl_obj (repl_result (fst (get_obj g_loc pt p),
1.276 + Some l) f s) pt p, [])
1.277 +);
1.278 +
1.279 +
1.280 +(*WN041022 deprecated, still for kbtest/diffapp.sml, /systest/root-equ.sml*)
1.281 +fun append_parent p l f r b pt =
1.282 + let (*val _= writeln("###append_parent: pos ="^pos2str p);*)
1.283 + val (ll,f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
1.284 + then ((fst (get_obj g_loc pt p), Some l),
1.285 + get_obj g_form pt p)
1.286 + else ((Some l, None), f)
1.287 + in insert (PrfObj
1.288 + {cell = [(*unused*)],
1.289 + form = f,
1.290 + tac = r,
1.291 + loc = ll,
1.292 + branch= b,
1.293 + result= (e_term,[]),
1.294 + ostate= Incomplete}) pt p end;
1.295 +fun cappend_parent pt p loc f r b =
1.296 +((*writeln("###cappend_parent: pos ="^pos2str p);*)
1.297 + apfst (append_parent p loc f r b) (cut_tree pt (p,Und))
1.298 +);
1.299 +
1.300 +
1.301 +fun append_problem [] l fmz (strs,spec,hdf) _ =
1.302 +((*writeln("###append_problem: pos = []");*)
1.303 + (Nd (PblObj
1.304 + {cell = [(*3.00. unused*)],
1.305 + origin= (strs,spec,hdf),
1.306 + fmz = fmz,
1.307 + spec = empty_spec,
1.308 + probl = []:itm list,
1.309 + meth = []:itm list,
1.310 + env = None,
1.311 + loc = (Some l, None),
1.312 + branch= TransitiveB,(*FIXXXXXME.27.8.03: for equations only*)
1.313 + result= (e_term,[]),
1.314 + ostate= Incomplete},[]))
1.315 +)
1.316 + | append_problem p l fmz (strs,spec,hdf) pt =
1.317 +((*writeln("###append_problem: pos ="^pos2str p);*)
1.318 + insert (PblObj
1.319 + {cell = [(*3.00. unused*)],
1.320 + origin= (strs,spec,hdf),
1.321 + fmz = fmz,
1.322 + spec = empty_spec,
1.323 + probl = []:itm list,
1.324 + meth = []:itm list,
1.325 + env = None,
1.326 + loc = (Some l, None),
1.327 + branch= TransitiveB,
1.328 + result= (e_term,[]),
1.329 + ostate= Incomplete}) pt p
1.330 +);
1.331 +fun cappend_problem _ [] loc fmz ori =
1.332 +((*writeln("###cappend_problem: pos = []");*)
1.333 + (append_problem [] loc fmz ori EmptyPtree,[])
1.334 +)
1.335 + | cappend_problem pt p loc fmz ori =
1.336 +((*writeln("###cappend_problem: pos ="^pos2str p);*)
1.337 + apfst (append_problem p (loc:istate) fmz ori) (cut_tree pt (p,Frm))
1.338 +);
1.339 +
1.340 +
1.341 +(* use"ME/ctreeNEW.sml";
1.342 + use"ctreeNEW.sml";
1.343 + *)
1.344 +
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/sml/ME/ctreeOLD.sml Fri Mar 04 19:11:15 2005 +0100
2.3 @@ -0,0 +1,1984 @@
2.4 +(* use"ME/ctree.sml";
2.5 + use"ctree.sml";
2.6 + W.N.26.10.99
2.7 +
2.8 +writeln (pr_ptree pr_short pt);
2.9 +
2.10 +val Nd ( _, ns) = pt;
2.11 +
2.12 +*)
2.13 +
2.14 +
2.15 +signature PTREE =
2.16 +sig
2.17 + type ptree
2.18 + type envp
2.19 + val e_ptree : ptree
2.20 + exception PTREE of string
2.21 + type branch
2.22 + type ostate
2.23 + type cellID
2.24 + type cid
2.25 + type posel
2.26 + type pos
2.27 + type pos'
2.28 + type loc
2.29 + type domID
2.30 + type pblID
2.31 + type metID
2.32 + type spec
2.33 + type 'a ppc
2.34 + type con
2.35 + type subs
2.36 + type subst
2.37 + type env
2.38 + type ets
2.39 + val ets2str : ets -> string
2.40 + type item
2.41 + type tac
2.42 + type tac_
2.43 + val tac_2str : tac_ -> string
2.44 + type safe
2.45 + val safe2str : safe -> string
2.46 +
2.47 + type meth
2.48 + val cappend_atomic : ptree -> pos -> loc -> cterm' -> tac
2.49 + -> cterm' -> ostate -> cid -> ptree * posel list * cid
2.50 + val cappend_form : ptree
2.51 + -> pos -> loc -> cterm' -> cid -> ptree * pos * cid
2.52 + val cappend_parent : ptree -> pos -> loc -> cterm' -> tac
2.53 + -> branch -> cid -> ptree * int list * cid
2.54 + val cappend_problem : ptree -> posel list(*FIXME*) -> loc
2.55 + -> cterm' list * spec -> cid -> ptree * int list * cellID list
2.56 + val append_result : ptree -> pos -> cterm' -> ostate -> ptree * pos
2.57 +
2.58 + type ppobj
2.59 + val g_branch : ppobj -> branch
2.60 + val g_cell : ppobj -> cid
2.61 + val g_args : ppobj -> (int * (term list)) list (*args of scr*)
2.62 + val g_form : ppobj -> cterm'
2.63 + val g_loc : ppobj -> loc
2.64 + val g_met : ppobj -> meth
2.65 + val g_domID : ppobj -> domID
2.66 + val g_metID : ppobj -> metID
2.67 + val g_model : ppobj -> cterm' ppc
2.68 + val g_tac : ppobj -> tac
2.69 + val g_origin : ppobj -> cterm' list * spec
2.70 + val g_ostate : ppobj -> ostate
2.71 + val g_pbl : ppobj -> pblID * item ppc
2.72 + val g_result : ppobj -> cterm'
2.73 + val g_spec : ppobj -> spec
2.74 +(* val get_all : (ppobj -> 'a) -> ptree -> 'a list
2.75 + val get_alls : (ppobj -> 'a) -> ptree list -> 'a list *)
2.76 + val get_obj : (ppobj -> 'a) -> ptree -> pos -> 'a
2.77 + val gpt_cell : ptree -> cid
2.78 + val par_pblobj : ptree -> pos -> pos
2.79 + val pre_pos : pos -> pos
2.80 + val lev_dn : int list -> int list
2.81 + val lev_on : pos -> posel list
2.82 + val lev_pred : pos -> pos
2.83 + val lev_up : pos -> pos
2.84 +(* val pr_cell : pos -> ppobj -> string
2.85 + val pr_pos : int list -> string *)
2.86 + val pr_ptree : (pos -> ppobj -> string) -> ptree -> string
2.87 + val pr_short : pos -> ppobj -> string
2.88 +(* val repl : 'a list -> int -> 'a -> 'a list
2.89 + val repl_app : 'a list -> int -> 'a -> 'a list
2.90 + val repl_branch : branch -> ppobj -> ppobj
2.91 + val repl_domID : domID -> ppobj -> ppobj
2.92 + val repl_form : cterm' -> ppobj -> ppobj
2.93 + val repl_met : item ppc -> ppobj -> ppobj
2.94 + val repl_metID : metID -> ppobj -> ppobj
2.95 + val repl_model : cterm' list -> ppobj -> ppobj
2.96 + val repl_tac : tac -> ppobj -> ppobj
2.97 + val repl_pbl : item ppc -> ppobj -> ppobj
2.98 + val repl_pblID : pblID -> ppobj -> ppobj
2.99 + val repl_result : cterm' -> ostate -> ppobj -> ppobj
2.100 + val repl_spec : spec -> ppobj -> ppobj
2.101 + val repl_subs : (string * string) list -> ppobj -> ppobj
2.102 + val test_trans : ppobj -> bool
2.103 + val uni__asm : (string * pos) list -> ppobj -> ppobj
2.104 + val uni__cid : cellID list -> ppobj -> ppobj *)
2.105 + val union_asm : ptree -> pos -> (string * pos) list -> ptree
2.106 + val union_cid : ptree -> pos -> cellID list -> ptree
2.107 + val update_branch : ptree -> pos -> branch -> ptree
2.108 + val update_domID : ptree -> pos -> domID -> ptree
2.109 + val update_met : ptree -> pos -> meth -> ptree
2.110 + val update_metppc : ptree -> pos -> item ppc -> ptree
2.111 + val update_metID : ptree -> pos -> metID -> ptree
2.112 + val update_tac : ptree -> pos -> tac -> ptree
2.113 + val update_pbl : ptree -> pos -> pblID * item ppc -> ptree
2.114 + val update_pblppc : ptree -> pos -> item ppc -> ptree
2.115 + val update_pblID : ptree -> pos -> pblID -> ptree
2.116 + val update_spec : ptree -> pos -> spec -> ptree
2.117 + val update_subs : ptree -> pos -> (string * string) list -> ptree
2.118 +
2.119 + val rep_pblobj : ppobj
2.120 + -> {branch:branch, cell:cid, env:envp, loc:loc, meth:meth, model:cterm' ppc,
2.121 + origin:cterm' list * spec, ostate:ostate, probl:pblID * item ppc,
2.122 + result:cterm', spec:spec}
2.123 + val rep_prfobj : ppobj
2.124 + -> {branch:branch, cell:cid, form:cterm', loc:loc, tac:tac,
2.125 + ostate:ostate, result:cterm'}
2.126 +end
2.127 +
2.128 +(* --------------
2.129 +structure Ptree (**): PTREE (**) =
2.130 +struct
2.131 + -------------- *)
2.132 +
2.133 +type env = (term * term) list;
2.134 +
2.135 +
2.136 +datatype branch =
2.137 + NoBranch | AndB | OrB
2.138 + | TransitiveB (* FIXXXME.8.03: set branch from met in Apply_Method
2.139 + FIXXXME.0402: -"- in Begin_Trans'*)
2.140 + | SequenceB | IntersectB | CollectB | MapB;
2.141 +fun branch2str NoBranch = "NoBranch"
2.142 + | branch2str AndB = "AndB"
2.143 + | branch2str OrB = "OrB"
2.144 + | branch2str TransitiveB = "TransitiveB"
2.145 + | branch2str SequenceB = "SequenceB"
2.146 + | branch2str IntersectB = "IntersectB"
2.147 + | branch2str CollectB = "CollectB"
2.148 + | branch2str MapB = "MapB";
2.149 +
2.150 +datatype ostate =
2.151 + Incomplete | Complete | Inconsistent(*WN041020 latter unused*);
2.152 +
2.153 +type cellID = int;
2.154 +type cid = cellID list;
2.155 +
2.156 +type posel = int; (* roundabout for (some of) nice signatures *)
2.157 +type pos = posel list;
2.158 +val pos2str = ints2str';
2.159 +datatype pos_ =
2.160 + Pbl (*PblObj-position: problem-type*)
2.161 + | Met (*PblObj-position: method*)
2.162 + | Frm (*PblObj-position: -> Pbl in ME (not by moveDown !)
2.163 + | PrfObj-position: formula*)
2.164 + | Res (*PblObj | PrfObj-position: result*)
2.165 + | Und; (*undefined*)
2.166 +fun pos_2str Pbl = "Pbl"
2.167 + | pos_2str Met = "Met"
2.168 + | pos_2str Frm = "Frm"
2.169 + | pos_2str Res = "Res"
2.170 + | pos_2str Und = "Und";
2.171 +
2.172 +type pos' = pos * pos_;
2.173 +(*WN.12.03 remembering interator (pos * pos_) for ptree
2.174 + pos : lev_on, lev_dn, lev_up,
2.175 + lev_onFrm, lev_dnRes (..see solve Apply_Method !)
2.176 + pos_:
2.177 +# generate1 sets pos_ if possible ...?WN0502?NOT...
2.178 +# generate1 does NOT set pos, because certain nodes can be lev_on OR lev_dn
2.179 + exceptions: Begin/End_Trans
2.180 +# thus generate(1) called in
2.181 +.# assy, locate_gen
2.182 +.# nxt_solv (tac_ -cases); general case:
2.183 + val pos' = case pos' of (p,Res) => (lev_on p',Res) | _ => pos'
2.184 +# WN050220, S(604):
2.185 + generate1...(Rewrite(f,..,res))..(pos, pos_)
2.186 + cappend_atomic.................pos ////// gets f+res always!!!
2.187 + cut_tree....................pos, pos_
2.188 +*)
2.189 +fun pos'2str (p,p_) = pair2str (ints2str' p, pos_2str p_);
2.190 +fun pos's2str ps = (strs2str' o (map pos'2str)) ps;
2.191 +val e_pos' = ([],Und):pos';
2.192 +
2.193 +fun res2str (t, ts) = pair2str (term2str t, terms2str ts);
2.194 +fun asm2str (t, p:pos) = pair2str (term2str t, ints2str' p);
2.195 +fun asms2str asms = (strs2str' o (map asm2str)) asms;
2.196 +
2.197 +
2.198 +
2.199 +datatype lrd = (*elements of a path (=loc_) into an Isabelle term*)
2.200 + L (*go left at $*)
2.201 + | R (*go right at $*)
2.202 + | D; (*go down at Abs*)
2.203 +type loc_ = lrd list;
2.204 +fun ldr2str L = "L"
2.205 + | ldr2str R = "R"
2.206 + | ldr2str D = "D";
2.207 +fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k;
2.208 +
2.209 +(*26.4.02: never used after introduction of scripts !!!*)
2.210 +type loc = loc_ * (* + interpreter-state *)
2.211 + (loc_ * rls') (* -"- for script of the ruleset*)
2.212 + option;
2.213 +val e_loc = ([],None):loc;
2.214 +val ee_loc = (e_loc,e_loc);
2.215 +
2.216 +
2.217 +datatype safe = Sundef | Safe | Unsafe | Helpless;
2.218 +fun safe2str Sundef = "Sundef"
2.219 + | safe2str Safe = "Safe"
2.220 + | safe2str Unsafe = "Unsafe"
2.221 + | safe2str Helpless = "Helpless";
2.222 +
2.223 +type subs = cterm' list; (*16.11.00 for FE-KE*)
2.224 +fun subst2str' thy' (s:subst) =
2.225 + (strs2str o
2.226 + (map (pair2str o
2.227 + (apsnd (Sign.string_of_term (sign_of (assoc_thy thy')))) o
2.228 + (apfst (Sign.string_of_term (sign_of (assoc_thy thy'))))))) s;
2.229 +
2.230 +type scrstate = (*state for script interpreter*)
2.231 + env(*stack*) (*used to instantiate tac for checking assod
2.232 + 12.03.noticed: e_ not updated during execution ?!?*)
2.233 + * loc_ (*location of tac in script*)
2.234 + * term option(*argument of curried functions*)
2.235 + * term (*value obtained by tac executed
2.236 + updated also after a derivation by 'new_val'*)
2.237 + * safe (*estimation of how result will be obtained*)
2.238 + * bool; (*true = strongly .., false = weakly associated:
2.239 + only used during ass_dn/up*)
2.240 +val e_scrstate = ([],[],None,e_term,Sundef,false):scrstate;
2.241 +
2.242 +
2.243 +(*21.8.02 ---> definitions.sml for datatype scr
2.244 +type rrlsstate = (*state for reverse rewriting*)
2.245 + (term * (*the current formula*)
2.246 + rule list (*of reverse rewrite set (#1#)*)
2.247 + list * (*may be serveral, eg. in norm_rational*)
2.248 + (rule * (*Thm (+ Thm generated from Calc) resulting in ...*)
2.249 + (term * (*... rewrite with ...*)
2.250 + term list)) (*... assumptions*)
2.251 + list); (*derivation from given term to normalform
2.252 + in reverse order with sym_thm;
2.253 + (#1#) could be extracted from here #1*) --------*)
2.254 +
2.255 +datatype istate = (*interpreter state*)
2.256 + Uistate (*undefined in modspec, in '_deriv'ation*)
2.257 + | ScrState of scrstate (*for script interpreter*)
2.258 + | RrlsState of rrlsstate; (*for reverse rewriting*)
2.259 +type iist = istate option * istate option;
2.260 +val e_istate = (ScrState ([],[],None,e_term,Sundef,false)):istate;
2.261 +(*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*)
2.262 +fun rta2str (r,(t,a)) = "\n("^(rule2str r)^",("^(term2str t)^", "^
2.263 + (terms2str a)^"))";
2.264 +fun istate2str Uistate = "Uistate"
2.265 + | istate2str (ScrState (e,l,to,t,s,b):istate) =
2.266 + "ScrState ("^ subst2str e ^",\n "^
2.267 + loc_2str l ^", "^ termopt2str to ^",\n "^
2.268 + term2str t ^", "^ safe2str s ^", "^ bool2str b ^")"
2.269 + | istate2str (RrlsState (t,t1,rss,rtas)) =
2.270 + "RrlsState ("^(term2str t)^", "^(term2str t1)^", "^
2.271 + ((strs2str o (map (strs2str o (map rule2str)))) rss)^", "^
2.272 + ((strs2str o (map rta2str)) rtas)^")";
2.273 +fun istates2str (None, None) = "(#None, #None)"
2.274 + | istates2str (None, Some ist) = "(#None,\n#Some "^istate2str ist^")"
2.275 + | istates2str (Some ist, None) = "(#Some "^istate2str ist^",\n #None)"
2.276 + | istates2str (Some i1, Some i2) = "(#Some "^istate2str i1^",\n #Some "^
2.277 + istate2str i2^")";
2.278 +
2.279 +fun new_val v (ScrState (env, loc_, topt, _, safe, bool)) =
2.280 + (ScrState (env, loc_, topt, v, safe, bool))
2.281 + | new_val _ _ = raise error "new_val: only for ScrState";
2.282 +
2.283 +datatype con = land | lor;
2.284 +
2.285 +
2.286 +fun subst2subs s = map (pair2str o
2.287 + (apfst (Sign.string_of_term (sign_of thy))) o
2.288 + (apsnd (Sign.string_of_term (sign_of thy)))) s;
2.289 +fun subst2subs' s = map ((apfst (Sign.string_of_term (sign_of thy))) o
2.290 + (apsnd (Sign.string_of_term (sign_of thy)))) s;
2.291 +
2.292 +
2.293 +
2.294 +fun isapair2pair (Const ("Pair",_) $ a $ b) = (a,b);
2.295 +fun subs2subst thy s = map (isapair2pair o term_of o the o (parse thy)) s;
2.296 +(*> subs2subst thy ["(bdv,x)","(err,#0)"];
2.297 +val it =
2.298 + [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real")),
2.299 + (Free ("err","RealDef.real"),Free ("#0","RealDef.real"))]
2.300 + : (term * term) list*)
2.301 +
2.302 +
2.303 +
2.304 +
2.305 +
2.306 +
2.307 +(*FE <-> KE: strings*)
2.308 +datatype tac =
2.309 + Init_Proof of ((cterm' list) * spec)
2.310 +(*Init_Proo_Hid of (dgmode * (cterm' list) * spec)
2.311 +| Init_Proof 7.6.02java-sml*)
2.312 +| Model_Problem of pblID
2.313 +| Refine_Problem of pblID | Refine_Tacitly of pblID
2.314 +(*| Match_Problem of pblID*)
2.315 +| Add_Given of cterm' | Del_Given of cterm'
2.316 +| Add_Find of cterm' | Del_Find of cterm'
2.317 +| Add_Relation of cterm' | Del_Relation of cterm'
2.318 +
2.319 +| Specify_Theory of domID | Specify_Problem of pblID
2.320 +| Specify_Method of metID
2.321 +| Apply_Method of metID | Check_Postcond of pblID
2.322 +| Free_Solve
2.323 +
2.324 +| Rewrite_Inst of ( subs * thm') | Rewrite of thm'
2.325 + | Rewrite_Asm of thm'
2.326 +| Rewrite_Set_Inst of ( subs * rls') | Rewrite_Set of rls'
2.327 +| Detail_Set_Inst of ( subs * rls') | Detail_Set of rls'
2.328 +| End_Detail (*end of script from next_tac,
2.329 + in solve: switches back to parent script*)
2.330 +| Derive of rls' (*an input formula using rls*)
2.331 +| Calculate of string | End_Ruleset
2.332 + (* plus | minus | times | cancel | pow | sqrt *)
2.333 +| Substitute of subs | Apply_Assumption of cterm' list
2.334 +
2.335 +| Take of cterm' | Take_Inst of cterm'
2.336 +| Group of (con * int list )
2.337 +(*| Subproblem_Full of (spec * (cterm' list)) *)
2.338 +| Subproblem of (domID * pblID)
2.339 +| CAScmd of cterm' (*6.6.02 URD: Function formula *)
2.340 +| End_Subproblem
2.341 +
2.342 +| Split_And | Conclude_And
2.343 +| Split_Or | Conclude_Or
2.344 +| Begin_Trans | End_Trans
2.345 +| Begin_Sequ | End_Sequ(* substitute root.env *)
2.346 +| Split_Intersect | End_Intersect
2.347 +| Check_elementwise of cterm' | Collect_Trues
2.348 +| Or_to_List
2.349 +
2.350 +| Empty_Tac (*TODO.11.6.03 ... of string: could carry msg of (Notappl msg)
2.351 + in 'helpless'*)
2.352 +| Tac of string(* eg.'repeat'*)
2.353 +| User (*internal, for ets*) | End_Proof';(* inout*)
2.354 +
2.355 +
2.356 +(* tac2str /--> library.sml: needed in dialog.sml for 'separable *)
2.357 +fun tac2str (ma:tac) = case ma of
2.358 + Init_Proof (ppc, spec) =>
2.359 + "Init_Proof "^(pair2str (strs2str ppc, spec2str spec))
2.360 + | Model_Problem pblID => "Model_Problem "^(strs2str pblID)
2.361 + | Refine_Tacitly pblID => "Refine_Tacitly "^(strs2str pblID)
2.362 + | Refine_Problem pblID => "Refine_Problem "^(strs2str pblID)
2.363 +(*| Match_Problem pblID => "Match_Problem "^(strs2str pblID)*)
2.364 + | Add_Given cterm' => "Add_Given "^cterm'
2.365 + | Del_Given cterm' => "Del_Given "^cterm'
2.366 + | Add_Find cterm' => "Add_Find "^cterm'
2.367 + | Del_Find cterm' => "Del_Find "^cterm'
2.368 + | Add_Relation cterm' => "Add_Relation "^cterm'
2.369 + | Del_Relation cterm' => "Del_Relation "^cterm'
2.370 +
2.371 + | Specify_Theory domID => "Specify_Theory "^(quote domID )
2.372 + | Specify_Problem pblID => "Specify_Problem "^(strs2str pblID )
2.373 + | Specify_Method metID => "Specify_Method "^(strs2str metID)
2.374 + | Apply_Method metID => "Apply_Method "^(strs2str metID)
2.375 + | Check_Postcond pblID => "Check_Postcond "^(strs2str pblID)
2.376 + | Free_Solve => "Free_Solve"
2.377 +
2.378 + | Rewrite_Inst (subs,thm')=>
2.379 + "Rewrite_Inst "^(pair2str (subs2str subs, spair2str thm'))
2.380 + | Rewrite thm' => "Rewrite "^(spair2str thm')
2.381 + | Rewrite_Asm thm' => "Rewrite_Asm "^(spair2str thm')
2.382 + | Rewrite_Set_Inst (subs, rls) =>
2.383 + "Rewrite_Set_Inst "^(pair2str (subs2str subs, quote rls))
2.384 + | Rewrite_Set rls => "Rewrite_Set "^(quote rls )
2.385 + | Detail_Set rls => "Detail_Set "^(quote rls )
2.386 + | Detail_Set_Inst (subs, rls) =>
2.387 + "Detail_Set_Inst "^(pair2str (subs2str subs, quote rls))
2.388 + | End_Detail => "End_Detail"
2.389 + | Derive rls' => "Derive "^rls'
2.390 + | Calculate op_ => "Calculate "^op_
2.391 + | Substitute subs => "Substitute "^(subs2str subs)
2.392 + | Apply_Assumption ct's => "Apply_Assumption "^(strs2str ct's)
2.393 +
2.394 + | Take cterm' => "Take "^(quote cterm' )
2.395 + | Take_Inst cterm' => "Take_Inst "^(quote cterm' )
2.396 + | Group (con, ints) =>
2.397 + "Group "^(pair2str (con2str con, ints2str ints))
2.398 + | Subproblem (domID, pblID) =>
2.399 + "Subproblem "^(pair2str (domID, strs2str pblID))
2.400 +(*| Subproblem_Full (spec, cts') =>
2.401 + "Subproblem_Full "^(pair2str (spec2str spec, strs2str cts'))*)
2.402 + | End_Subproblem => "End_Subproblem"
2.403 + | CAScmd cterm' => "CAScmd "^(quote cterm')
2.404 +
2.405 + | Check_elementwise cterm'=> "Check_elementwise "^(quote cterm')
2.406 + | Or_to_List => "Or_to_List "
2.407 + | Collect_Trues => "Collect_Trues"
2.408 +
2.409 + | Empty_Tac => "Empty_Tac"
2.410 + | Tac string => "Tac "^string
2.411 + | User => "User"
2.412 + | End_Proof' => "tac End_Proof'"
2.413 + | _ => "tac2str not impl. for ?!";
2.414 +
2.415 +fun is_rewset (Rewrite_Set_Inst _) = true
2.416 + | is_rewset (Rewrite_Set _) = true
2.417 + | is_rewset _ = false;
2.418 +
2.419 +fun tac2IDstr (ma:tac) = case ma of
2.420 + Model_Problem _ => "Model_Problem"
2.421 + | Refine_Tacitly pblID => "Refine_Tacitly"
2.422 + | Refine_Problem pblID => "Refine_Problem"
2.423 + | Add_Given cterm' => "Add_Given"
2.424 + | Del_Given cterm' => "Del_Given"
2.425 + | Add_Find cterm' => "Add_Find"
2.426 + | Del_Find cterm' => "Del_Find"
2.427 + | Add_Relation cterm' => "Add_Relation"
2.428 + | Del_Relation cterm' => "Del_Relation"
2.429 +
2.430 + | Specify_Theory domID => "Specify_Theory"
2.431 + | Specify_Problem pblID => "Specify_Problem"
2.432 + | Specify_Method metID => "Specify_Method"
2.433 + | Apply_Method metID => "Apply_Method"
2.434 + | Check_Postcond pblID => "Check_Postcond"
2.435 + | Free_Solve => "Free_Solve"
2.436 +
2.437 + | Rewrite_Inst (subs,thm')=> "Rewrite_Inst"
2.438 + | Rewrite thm' => "Rewrite"
2.439 + | Rewrite_Asm thm' => "Rewrite_Asm"
2.440 + | Rewrite_Set_Inst (subs, rls) => "Rewrite_Set_Inst"
2.441 + | Rewrite_Set rls => "Rewrite_Set"
2.442 + | Detail_Set rls => "Detail_Set"
2.443 + | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst"
2.444 + | Derive rls' => "Derive "
2.445 + | Calculate op_ => "Calculate "
2.446 + | Substitute subs => "Substitute"
2.447 + | Apply_Assumption ct's => "Apply_Assumption"
2.448 +
2.449 + | Take cterm' => "Take"
2.450 + | Take_Inst cterm' => "Take_Inst"
2.451 + | Group (con, ints) => "Group"
2.452 + | Subproblem (domID, pblID) => "Subproblem"
2.453 + | End_Subproblem => "End_Subproblem"
2.454 + | CAScmd cterm' => "CAScmd"
2.455 +
2.456 + | Check_elementwise cterm'=> "Check_elementwise"
2.457 + | Or_to_List => "Or_to_List "
2.458 + | Collect_Trues => "Collect_Trues"
2.459 +
2.460 + | Empty_Tac => "Empty_Tac"
2.461 + | Tac string => "Tac "
2.462 + | User => "User"
2.463 + | End_Proof' => "End_Proof'"
2.464 + | _ => "tac2str not impl. for ?!";
2.465 +
2.466 +
2.467 +type fmz_ = cterm' list;
2.468 +type fmz = fmz_ * spec;
2.469 +val e_fmz = ([],e_spec);
2.470 +
2.471 +(*tac_ is made from tac in applicable_in,
2.472 + and carries all data necessary for generate;*)
2.473 +datatype tac_ =
2.474 +(* datatype tac = *)
2.475 + Init_Proof' of ((cterm' list) * spec)
2.476 + (* ori list !: code specify -> applicable*)
2.477 +| Model_Problem' of pblID *
2.478 + itm list (*the 'untouched' pbl*)
2.479 +| Refine_Tacitly' of pblID * (*input*)
2.480 + pblID * (*the refined from applicable_in*)
2.481 + domID * (*from new pbt?! filled in specify*)
2.482 + metID * (*from new pbt?! filled in specify*)
2.483 + itm list (*drop ! 9.03: remains [] for
2.484 + Model_Problem recognizing its activation*)
2.485 +| Refine_Problem' of (pblID * (itm list * (bool * Term.term) list))
2.486 + (*FIXME?040215 drop: done automatically in init_proof + Subproblem'*)
2.487 +| Add_Given' of cterm' *
2.488 + itm list (*updated with input in fun specify_additem*)
2.489 +| Add_Find' of cterm' *
2.490 + itm list (*updated with input in fun specify_additem*)
2.491 +| Add_Relation' of cterm' *
2.492 + itm list (*updated with input in fun specify_additem*)
2.493 +| Del_Given' of cterm' | Del_Find' of cterm' | Del_Relation' of cterm'
2.494 + (*4.00.: all.. term: in applicable_in ..? Syn ?only for FormFK?*)
2.495 +
2.496 +| Specify_Theory' of domID
2.497 +| Specify_Problem' of (pblID * (* *)
2.498 + (bool * (* matches *)
2.499 + (itm list * (* ppc *)
2.500 + (bool * term) list))) (* preconditions *)
2.501 +| Specify_Method' of metID *
2.502 + ori list * (*repl. "#undef"*)
2.503 + itm list (*... updated from pbl to met*)
2.504 +| Apply_Method' of metID *
2.505 + (term option) * (*init_form*)
2.506 + istate
2.507 +| Check_Postcond' of
2.508 + pblID *
2.509 + (term * (*returnvalue of script in solve*)
2.510 + cterm' list)(*collect by get_assumptions_ in applicable_in, except if
2.511 + butlast tac is Check_elementwise: take only these asms*)
2.512 +| Free_Solve'
2.513 +
2.514 +| Rewrite_Inst' of theory' * rew_ord' * rls
2.515 + * bool * subst * thm' * term * (term * term list)
2.516 + (*... form * (result* asumpts ), saves time*)
2.517 +| Rewrite' of theory' * rew_ord' * rls * bool * thm' *
2.518 + term * (term * term list)
2.519 +| Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm' *
2.520 + term * (term * term list)
2.521 +| Rewrite_Set_Inst' of theory' * bool * subst * rls *
2.522 + term * (term * term list)
2.523 +| Detail_Set_Inst' of theory' * bool * subst * rls *
2.524 + term * (term * term list)
2.525 +| Rewrite_Set' of theory' * bool * rls * term * (term * term list)
2.526 +| Detail_Set' of theory' * bool * rls * term * (term * term list)
2.527 +| End_Detail' of (term * (term list)) (*see End_Trans'*)
2.528 +| End_Ruleset' of term
2.529 +| Derive' of rls
2.530 +| Calculate' of theory' * string * term * (term * thm')
2.531 + (*WN.29.4.03 asm?: * term list??*)
2.532 +| Substitute' of subst * term (*10.8.00+..*)* term
2.533 +| Apply_Assumption' of term list * term
2.534 +
2.535 +| Take' of term | Take_Inst' of term
2.536 +| Group' of (con * int list * term)
2.537 +| Subproblem' of (spec *
2.538 + (ori list) * (*filled in assod Subproblem'*)
2.539 + term * (*-"-, headline of calc-head *)
2.540 + fmz_ *
2.541 + term) (*Subproblem(dom,pbl)*)
2.542 +| CAScmd' of term
2.543 +| End_Subproblem' of term (*???*)
2.544 +| Split_And' of term | Conclude_And' of term
2.545 +| Split_Or' of term | Conclude_Or' of term
2.546 +| Begin_Trans' of term | End_Trans' of (term * (term list))
2.547 +| Begin_Sequ' | End_Sequ'(* substitute root.env*)
2.548 +| Split_Intersect' of term | End_Intersect' of term
2.549 +| Check_elementwise' of (*special case:*)
2.550 + term * (*(1)the current formula: [x=1,x=...]*)
2.551 + string * (*(2)the pred from Check_elementwise *)
2.552 + (term * (*(3)composed from (1) and (2): {x. pred}*)
2.553 + term list) (*20.5.03 assumptions*)
2.554 +
2.555 +| Or_to_List' of term * term (* (a | b, [a,b]) *)
2.556 +| Collect_Trues' of term
2.557 +
2.558 +| Empty_Tac_ | Tac_ of (*for dummies*)
2.559 + theory *
2.560 + string * (*form*)
2.561 + string * (*in Tac*)
2.562 + string (*result of Tac".."*)
2.563 +| User' (*internal for ets*) | End_Proof'';(*End_Proof:inout*)
2.564 +(*TODO?: done partially for tests*)
2.565 +fun tac_2str ma = case ma of
2.566 + Init_Proof' (ppc, spec) =>
2.567 + "Init_Proof' "^(pair2str (strs2str ppc, spec2str spec))
2.568 + | Model_Problem' (pblID,_) => "Model_Problem' "^(strs2str pblID )
2.569 + | Refine_Tacitly'(p,prefin,domID,metID,itms)=>
2.570 + "Refine_Tacitly' ("
2.571 + ^(strs2str p)^", "^(strs2str prefin)^", "
2.572 + ^domID^", "^(strs2str metID)^", pbl-itms)"
2.573 + | Refine_Problem' ms => "Refine_Problem' ("^(*matchs2str ms*)"..."^")"
2.574 +(*| Match_Problem' (pI, (ok, (itms, pre))) =>
2.575 + "Match_Problem' "^(spair2str (strs2str pI,
2.576 + spair2str (bool2str ok,
2.577 + spair2str ("itms2str itms",
2.578 + "items2str pre"))))*)
2.579 + | Add_Given' cterm' => "Add_Given' "(*^cterm'*)
2.580 + | Del_Given' cterm' => "Del_Given' "(*^cterm'*)
2.581 + | Add_Find' cterm' => "Add_Find' "(*^cterm'*)
2.582 + | Del_Find' cterm' => "Del_Find' "(*^cterm'*)
2.583 + | Add_Relation' cterm' => "Add_Relation' "(*^cterm'*)
2.584 + | Del_Relation' cterm' => "Del_Relation' "(*^cterm'*)
2.585 +
2.586 + | Specify_Theory' domID => "Specify_Theory' "^(quote domID )
2.587 + | Specify_Problem' (pI, (ok, (itms, pre))) =>
2.588 + "Specify_Problem' "^(spair2str (strs2str pI,
2.589 + spair2str (bool2str ok,
2.590 + spair2str ("itms2str itms",
2.591 + "items2str pre"))))
2.592 + | Specify_Method' (pI,oris,itms) =>
2.593 + "Specify_Method' ("^metID2str pI^", "^oris2str oris^", )"
2.594 +
2.595 + | Apply_Method' (metID,_,_) => "Apply_Method' "^(strs2str metID)
2.596 + | Check_Postcond' (pblID,(scval,asm)) =>
2.597 + "Check_Postcond' "^(spair2str(strs2str pblID,
2.598 + spair2str (term2str scval, strs2str asm)))
2.599 +
2.600 + | Free_Solve' => "Free_Solve'"
2.601 +
2.602 + | Rewrite_Inst' (*subs,thm'*) _ =>
2.603 + "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
2.604 + | Rewrite' thm' => "Rewrite' "(*^(spair2str thm')*)
2.605 + | Rewrite_Asm' thm' => "Rewrite_Asm' "(*^(spair2str thm')*)
2.606 + | Rewrite_Set_Inst' (*subs,thm'*) _ =>
2.607 + "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
2.608 + | Rewrite_Set'(thy',pasm,rls',f,(f',asm))
2.609 + => "Rewrite_Set' ("^thy'^","^(bool2str pasm)^","^(id_rls rls')^","
2.610 + ^(Sign.string_of_term (sign_of thy) f)^",("^(Sign.string_of_term (sign_of thy) f')
2.611 + ^","^((strs2str o (map (Sign.string_of_term (sign_of thy)))) asm)^"))"
2.612 +
2.613 + | End_Detail' _ => "End_Detail' xxx"
2.614 + | Detail_Set' _ => "Detail_Set' xxx"
2.615 + | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
2.616 +
2.617 + | Derive' rls => "Derive' "^id_rls rls
2.618 + | Calculate' _ => "Calculate' "
2.619 + | Substitute' subs => "Substitute' "(*^(subs2str subs)*)
2.620 + | Apply_Assumption' ct's => "Apply_Assumption' "(*^(strs2str ct's)*)
2.621 +
2.622 + | Take' cterm' => "Take' "(*^(quote cterm' )*)
2.623 + | Take_Inst' cterm' => "Take_Inst' "(*^(quote cterm' )*)
2.624 + | Group' (con, ints, _) =>
2.625 + "Group' "^(pair2str (con2str con, ints2str ints))
2.626 + | Subproblem' (spec, oris, _,_,pbl_form) =>
2.627 + "Subproblem' "(*^(pair2str (domID, strs2str ,...))*)
2.628 + | End_Subproblem' _ => "End_Subproblem'"
2.629 + | CAScmd' cterm' => "CAScmd' "(*^(quote cterm')*)
2.630 +
2.631 + | Empty_Tac_ => "Empty_Tac_"
2.632 + | User' => "User'"
2.633 + | Tac_ (_,form,id,result) => "Tac_ (thy,"^form^","^id^","^result^")"
2.634 + | _ => "tac_2str not impl. for arg";
2.635 +
2.636 +(*'executed tactics' (tac_s) with local environment etc.;
2.637 + used for continuing eval script + for generate*)
2.638 +type ets =
2.639 + (loc_ * (* of tactic in scr, tactic (weakly) associated with tac_*)
2.640 + (tac_ * (* (for generate) *)
2.641 + env * (* with 'tactic=result' as a rule, tactic ev. _not_ ready:
2.642 + for handling 'parallel let'*)
2.643 + env * (* with results of (ready) tacs *)
2.644 + term * (* itr_arg of tactic, for upd. env at Repeat, Try*)
2.645 + term * (* result value of the tac *)
2.646 + safe))
2.647 + list;
2.648 +val Ets = []:ets;
2.649 +
2.650 +
2.651 +fun ets2s (l,(m,eno,env,iar,res,s)) =
2.652 + "\n("^(loc_2str l)^",("^(tac_2str m)^
2.653 + ",\n ens= "^(subst2str eno)^
2.654 + ",\n env= "^(subst2str env)^
2.655 + ",\n iar= "^(Sign.string_of_term (sign_of thy) iar)^
2.656 + ",\n res= "^(Sign.string_of_term (sign_of thy) res)^
2.657 + ",\n "^(safe2str s)^"))";
2.658 +fun ets2str (ets:ets) = (strs2str o (map ets2s)) ets;
2.659 +
2.660 +
2.661 +type envp =(*9.5.03: unused, delete with field in ptree.PblObj FIXXXME*)
2.662 + (int * term list) list * (*assoc-list: args of met*)
2.663 + (int * rls) list * (*assoc-list: tacs already done ///15.9.00*)
2.664 + (int * ets) list * (*assoc-list: tacs etc. already done*)
2.665 + (string * pos) list; (*asms * from where*)
2.666 +val empty_envp = ([],[],[],[]):envp;
2.667 +
2.668 +datatype ppobj =
2.669 + PrfObj of {cell : cid, (* 4.00 superfluous: use cid in DG only!!*)
2.670 + form : term,
2.671 + tac : tac, (* also in istate*)
2.672 + loc : istate option * istate option, (*for form, result
2.673 +13.8.02: (None,None) <==> e_istate ! see update_loc, get_loc*)
2.674 + branch: branch,
2.675 + result: term * term list,
2.676 + (*FIXX@ME result:term * term list
2.677 + => applicable_in =..rewrite_set_
2.678 + => rls = {erls: rls (NOT rls'),...}*)
2.679 + ostate: ostate} (*Complete <=> result is OK*)
2.680 + | PblObj of {cell : cid, (*unused*)
2.681 + fmz : fmz, (*from init:FIXME never use this spec;-drop*)
2.682 + origin: (ori list) * (*representation from fmz+pbt
2.683 + for efficiently adding items in probl, meth*)
2.684 + spec * (*updated by Refine_Tacitly*)
2.685 + term, (*headline of calc-head*)
2.686 + spec : spec, (*explicitly input*)
2.687 + probl : itm list, (*itms explicitly input*)
2.688 + meth : itm list, (*itms automatically added to copy of probl*)
2.689 + env : istate option,(*for _sub_problem, if no init_form*)
2.690 + loc : istate option * istate option, (*for pbl+met, result*)
2.691 + branch: branch,
2.692 + result: term * term list,
2.693 + ostate: ostate}; (*Complete <=> result is _proven_ OK*)
2.694 +datatype ptree =
2.695 + EmptyPtree
2.696 + | Nd of ppobj * (ptree list);
2.697 +val e_ptree = EmptyPtree;
2.698 +
2.699 +fun rep_prfobj (PrfObj {cell,form,tac,loc,branch,result,ostate}) =
2.700 + {cell=cell,form=form,tac=tac,loc=loc,branch=branch,result=result,ostate=ostate};
2.701 +fun rep_pblobj (PblObj {cell,origin,fmz,spec,probl,meth,env,
2.702 + loc,branch,result,ostate}) =
2.703 + {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,
2.704 + env=env,loc=loc,branch=branch,result=result,ostate=ostate};
2.705 +fun is_prfobj (PrfObj _) = true
2.706 + | is_prfobj _ =false;
2.707 +(*val is_prfobj' = get_obj is_prfobj; *)
2.708 +fun is_pblobj (PblObj _) = true
2.709 + | is_pblobj _ = false;
2.710 +(*val is_pblobj' = get_obj is_pblobj; 'Error: unbound constructor get_obj'*)
2.711 +
2.712 +
2.713 +exception PTREE of string;
2.714 +fun nth _ [] = raise PTREE "nth _ []"
2.715 + | nth 1 (x::xs) = x
2.716 + | nth n (x::xs) = nth (n-1) xs;
2.717 +(*> nth 2 [11,22,33]; -->> val it = 22 : int*)
2.718 +
2.719 +fun lev_up ([]:pos) = raise PTREE "lev_up []"
2.720 + | lev_up p = (drop_last p):pos;
2.721 +fun lev_on ([]:pos) = raise PTREE "lev_on []"
2.722 + | lev_on pos =
2.723 + let val len = length pos
2.724 + in (drop_last pos) @ [(nth len pos)+1] end;
2.725 +fun lev_onFrm ((p,_):pos') = (lev_on p,Frm):pos'
2.726 + | lev_onFrm p = raise PTREE ("*** lev_onFrm: pos'="^(pos'2str p));
2.727 +(*040216: for inform --> embed_deriv: remains on same level*)
2.728 +fun lev_back (([],_):pos') = raise PTREE "lev_on_back: called by ([],_)"
2.729 + | lev_back (p,_) =
2.730 + if last_elem p <= 1 then (p, Frm):pos'
2.731 + else ((drop_last p) @ [(nth (length p) p) - 1], Res);
2.732 +(*.increase pos by n within a level.*)
2.733 +fun pos_plus 0 pos = pos
2.734 + | pos_plus n ((p,Frm):pos') = pos_plus (n-1) (p, Res)
2.735 + | pos_plus n ((p, _):pos') = pos_plus (n-1) (lev_on p, Res);
2.736 +
2.737 +
2.738 +
2.739 +fun lev_pred ([]:pos) = raise PTREE "lev_pred []"
2.740 + | lev_pred (pos:pos) =
2.741 + let val len = length pos
2.742 + in ((drop_last pos) @ [(nth len pos)-1]):pos end;
2.743 +(*lev_pred [1,2,3];
2.744 +val it = [1,2,2] : pos
2.745 +> lev_pred [1];
2.746 +val it = [0] : pos *)
2.747 +
2.748 +fun lev_dn p = p @ [0];
2.749 +(*> (lev_dn o lev_on) [1,2,3];
2.750 +val it = [1,2,4,0] : pos *)
2.751 +(*fun lev_dn' ((p,p_):pos') = (lev_dn p, Frm):pos'; WN.3.12.03: never used*)
2.752 +fun lev_dnRes ((p,_):pos') = (lev_dn p, Res):pos';
2.753 +
2.754 +(*4.4.00*)
2.755 +fun lev_up_ ((p,Res):pos') = (lev_up p,Res):pos'
2.756 + | lev_up_ p' = raise error ("lev_up_: called for "^(pos'2str p'));
2.757 +fun lev_dn_ ((p,_):pos') = (lev_dn p,Res):pos'
2.758 +fun ind ((p,_):pos') = length p; (*WN050108 deprecated in favour of lev_of*)
2.759 +fun lev_of ((p,_):pos') = length p;
2.760 +
2.761 +
2.762 +(** convert ptree to a string **)
2.763 +
2.764 +(* convert a pos from list to string *)
2.765 +fun pr_pos ps = (space_implode "." (map string_of_int ps))^". ";
2.766 +(* show hd origin or form only *)
2.767 +fun pr_short (p:pos) (PblObj {origin = (ori,_,_),...}) =
2.768 + ((pr_pos p) ^ " ----- pblobj -----\n")
2.769 +(* ((((Sign.string_of_term (sign_of thy)) o #4 o hd) ori)^" "^
2.770 + (((Sign.string_of_term (sign_of thy)) o hd(*!?!*) o #5 o hd) ori))^
2.771 + "\n") *)
2.772 + | pr_short p (PrfObj {form = form,...}) =
2.773 + ((pr_pos p) ^ (term2str form) ^ "\n");
2.774 +fun pr_cell (p:pos) (PblObj {cell = c, origin = (ori,_,_),...}) =
2.775 + ((ints2str c) ^" "^
2.776 + ((((Sign.string_of_term (sign_of thy)) o #4 o hd) ori)^" "^
2.777 + (((Sign.string_of_term (sign_of thy)) o hd(*!?!*) o #5 o hd) ori))^
2.778 + "\n")
2.779 + | pr_cell p (PrfObj {cell = c, form = form,...}) =
2.780 + ((ints2str c) ^" "^ (term2str form) ^ "\n");
2.781 +
2.782 +
2.783 +(* convert ptree *)
2.784 +fun pr_ptree f pt =
2.785 + let
2.786 + fun pr_pt pfn _ EmptyPtree = ""
2.787 + | pr_pt pfn ps (Nd (b, [])) = pfn ps b
2.788 + | pr_pt pfn ps (Nd (b, ts)) = (pfn ps b)^
2.789 + (prts pfn (ps:pos) 1 ts)
2.790 + and prts pfn ps p [] = ""
2.791 + | prts pfn ps p (t::ts) = (pr_pt pfn (ps @ [p]) t)^
2.792 + (prts pfn ps (p+1) ts)
2.793 + in pr_pt f [] pt end;
2.794 +(*
2.795 +> fun prfn ps b = (pr_pos ps)^" "^b(*TODO*)^"\n";
2.796 +> val pt = ref EmptyPtree;
2.797 +> pt:=Nd("root",
2.798 + [Nd("xx1",[]),
2.799 + Nd("xx2",
2.800 + [Nd("xx2.1.",[]),
2.801 + Nd("xx2.2.",[])]),
2.802 + Nd("xx3",[])]);
2.803 +> writeln (pr_ptree prfn (!pt));
2.804 +*)
2.805 +
2.806 +
2.807 +(** access the branches of ptree **)
2.808 +
2.809 +fun ins_nth 1 e l = e::l
2.810 + | ins_nth n e [] = raise PTREE "ins_nth n e []"
2.811 + | ins_nth n e (l::ls) = l::(ins_nth (n-1) e ls);
2.812 +fun repl [] _ _ = raise PTREE "repl [] _ _"
2.813 + | repl (l::ls) 1 e = e::ls
2.814 + | repl (l::ls) n e = l::(repl ls (n-1) e);
2.815 +fun repl_app ls n e =
2.816 + let val lim = 1 + length ls
2.817 + in if n > lim then raise PTREE "repl_app: n > lim"
2.818 + else if n = lim then ls @ [e]
2.819 + else repl ls n e end;
2.820 +(*
2.821 +> repl [1,2,3] 2 22222;
2.822 +val it = [1,22222,3] : int list
2.823 +> repl_app [1,2,3,4] 5 5555;
2.824 +val it = [1,2,3,4,5555] : int list
2.825 +> repl_app [1,2,3] 2 22222;
2.826 +val it = [1,22222,3] : int list
2.827 +> repl_app [1] 2 22222 ;
2.828 +val it = [1,22222] : int list
2.829 +*)
2.830 +
2.831 +
2.832 +(*.get from obj at pos by f : ppobj -> 'a.*)
2.833 +fun get_obj f EmptyPtree _ = raise PTREE "get_obj f EmptyPtree"
2.834 + | get_obj f (Nd (b, _)) [] = f b
2.835 + | get_obj f (Nd (b, bs)) (p::ps) =
2.836 +(* val (f, Nd (b, bs), (p::ps)) = (I, pt, p);
2.837 + *)
2.838 + let val _ = (nth p bs) handle _ => raise PTREE ("get_obj: pos = "^
2.839 + (ints2str' (p::ps))^" does not exist");
2.840 + in (get_obj f (nth p bs) (ps:pos))
2.841 + (*before WN050419: 'wrong type..' raised also if pos doesn't exist*)
2.842 + handle _ => raise PTREE (*"get_obj: at pos = "^
2.843 + (ints2str' (p::ps))^" wrong type of ppobj"*)
2.844 + ("get_obj: pos = "^
2.845 + (ints2str' (p::ps))^" does not exist")
2.846 + end;
2.847 +fun get_nd EmptyPtree _ = raise PTREE "get_nd EmptyPtree"
2.848 + | get_nd n [] = n
2.849 + | get_nd (Nd (_,nds)) (pos as p::(ps:pos)) = (get_nd (nth p nds) ps)
2.850 + handle _ => raise PTREE ("get_nd: not existent pos = "^(ints2str' pos));
2.851 +
2.852 +
2.853 +(* for use by get_obj *)
2.854 +fun g_cell (PblObj {cell = c,...}) = c
2.855 + | g_cell (PrfObj {cell = c,...}) = c;
2.856 +fun g_form (PrfObj {form = f,...}) = f
2.857 + | g_form (PblObj {origin=(_,_,f),...}) = f;
2.858 +(* | g_form _ = raise PTREE "g_form not for PblObj";*)
2.859 +fun g_origin (PblObj {origin = ori,...}) = ori
2.860 + | g_origin _ = raise PTREE "g_origin not for PrfObj";
2.861 +fun g_fmz (PblObj {fmz = f,...}) = f
2.862 + | g_fmz _ = raise PTREE "g_fmz not for PrfObj";
2.863 +fun g_spec (PblObj {spec = s,...}) = s
2.864 + | g_spec _ = raise PTREE "g_spec not for PrfObj";
2.865 +fun g_pbl (PblObj {probl = p,...}) = p
2.866 + | g_pbl _ = raise PTREE "g_pbl not for PrfObj";
2.867 +fun g_met (PblObj {meth = p,...}) = p
2.868 + | g_met _ = raise PTREE "g_met not for PrfObj";
2.869 +fun g_domID (PblObj {spec = (d,_,_),...}) = d
2.870 + | g_domID _ = raise PTREE "g_metID not for PrfObj";
2.871 +fun g_metID (PblObj {spec = (_,_,m),...}) = m
2.872 + | g_metID _ = raise PTREE "g_metID not for PrfObj";
2.873 +fun g_env (PblObj {env,...}) = env
2.874 + | g_env _ = raise PTREE "g_env not for PrfObj";
2.875 +fun g_loc (PblObj {loc = l,...}) = l
2.876 + | g_loc (PrfObj {loc = l,...}) = l;
2.877 +fun g_branch (PblObj {branch = b,...}) = b
2.878 + | g_branch (PrfObj {branch = b,...}) = b;
2.879 +fun g_tac (PblObj {spec = (d,p,m),...}) = Apply_Method m
2.880 + | g_tac (PrfObj {tac = m,...}) = m;
2.881 +fun g_result (PblObj {result = r,...}) = r
2.882 + | g_result (PrfObj {result = r,...}) = r;
2.883 +fun g_ostate (PblObj {ostate = r,...}) = r
2.884 + | g_ostate (PrfObj {ostate = r,...}) = r;
2.885 +fun g_ostate' (Nd (PblObj {ostate = r,...}, _)) = r
2.886 + | g_ostate' (Nd (PrfObj {ostate = r,...}, _)) = r;
2.887 +
2.888 +fun gpt_cell (Nd (PblObj {cell = c,...},_)) = c
2.889 + | gpt_cell (Nd (PrfObj {cell = c,...},_)) = c;
2.890 +
2.891 +(*in CalcTree/Subproblem an 'just_created_' model is created;
2.892 + this is filled to 'untouched' by Model/Refine_Problem*)
2.893 +fun just_created_ (PblObj {meth, probl, spec, ...}) =
2.894 + null meth andalso null probl andalso spec = e_spec;
2.895 +val e_origin = ([],e_spec,e_term): (ori list) * spec * term;
2.896 +
2.897 +fun just_created (pt,(p,_):pos') =
2.898 + let val ppobj = get_obj I pt p
2.899 + in is_pblobj ppobj andalso just_created_ ppobj end;
2.900 +
2.901 +fun existpt pos pt = can (get_obj I pt) pos;
2.902 +fun existpt' ((p,p_):pos') pt =
2.903 + if can (get_obj I pt) p
2.904 + then case p_ of
2.905 + Res => get_obj g_ostate pt p = Complete
2.906 + | _ => true
2.907 + else false;
2.908 +
2.909 +fun fst_onlev (([], Frm):pos') = true
2.910 + | fst_onlev (([], Pbl):pos') = true
2.911 + | fst_onlev (([], Met):pos') = true
2.912 + | fst_onlev (pos, Frm) = last_elem pos = 1
2.913 + | fst_onlev _ = false;
2.914 +fun last_onlev pt pos = not (existpt (lev_on pos) pt);
2.915 +
2.916 +
2.917 +(*.find the position of the next parent which is a PblObj in ptree.*)
2.918 +fun par_pblobj pt ([]:pos) = ([]:pos)
2.919 + | par_pblobj pt p =
2.920 + let fun par pt [] = []
2.921 + | par pt p = if is_pblobj (get_obj I pt p) then p
2.922 + else par pt (lev_up p)
2.923 + in par pt (lev_up p) end;
2.924 +(* lev_up for hard_gen operating with pos = [...,0] *)
2.925 +
2.926 +(*.find the position and the children of the next parent which is a PblObj.*)
2.927 +fun par_children (Nd (PblObj _, children)) ([]:pos) = (children, []:pos)
2.928 + | par_children (pt as Nd (PblObj _, children)) p =
2.929 + let fun par [] = (children, [])
2.930 + | par p = let val Nd (obj, children) = get_nd pt p
2.931 + in if is_pblobj obj then (children, p) else par (lev_up p)
2.932 + end;
2.933 + in par (lev_up p) end;
2.934 +
2.935 +(*.get the children of a node in ptree.*)
2.936 +fun children (Nd (PblObj _, cn)) = cn
2.937 + | children (Nd (PrfObj _, cn)) = cn;
2.938 +
2.939 +
2.940 +(*.find the next parent, which is either a PblObj (return true)
2.941 + or a PrfObj with tac = Detail_Set (return false).*)
2.942 +(*FIXME.3.4.03:re-organize par_pbl_det after rls' --> rls*)
2.943 +fun par_pbl_det pt ([]:pos) = (true, []:pos, Erls)
2.944 + | par_pbl_det pt p =
2.945 + let fun par pt [] = (true, [], Erls)
2.946 + | par pt p = if is_pblobj (get_obj I pt p) then (true, p, Erls)
2.947 + else case get_obj g_tac pt p of
2.948 + (*Detail_Set rls' => (false, p, assoc_rls rls')
2.949 + (*^^^--- before 040206 after ---vvv*)
2.950 + |*)Rewrite_Set rls' => (false, p, assoc_rls rls')
2.951 + | Rewrite_Set_Inst (_, rls') =>
2.952 + (false, p, assoc_rls rls')
2.953 + | _ => par pt (lev_up p)
2.954 + in par pt (lev_up p) end;
2.955 +
2.956 +
2.957 +
2.958 +
2.959 +(*.get from the whole ptree by f : ppobj -> 'a.*)
2.960 +fun get_all f EmptyPtree = []
2.961 + | get_all f (Nd (b, [])) = [f b]
2.962 + | get_all f (Nd (b, bs)) = [f b] @ (get_alls f bs)
2.963 +and get_alls f [] = []
2.964 + | get_alls f pts = flat (map (get_all f) pts);
2.965 +
2.966 +
2.967 +(*.insert obj b into ptree at pos, ev.overwriting this pos.*)
2.968 +fun insert b EmptyPtree ([]:pos) = Nd (b, [])
2.969 + | insert b EmptyPtree _ = raise PTREE "insert b Empty _"
2.970 + | insert b (Nd ( _, _)) [] = raise PTREE "insert b _ []"
2.971 + | insert b (Nd (b', bs)) (p::[]) =
2.972 + Nd (b', repl_app bs p (Nd (b,[])))
2.973 + | insert b (Nd (b', bs)) (p::ps) =
2.974 + Nd (b', repl_app bs p (insert b (nth p bs) ps));
2.975 +(*
2.976 +> type ppobj = string;
2.977 +> writeln (pr_ptree prfn (!pt));
2.978 + val pt = ref Empty;
2.979 + pt:= insert ("root":ppobj) EmptyPtree [];
2.980 + pt:= insert ("xx1":ppobj) (!pt) [1];
2.981 + pt:= insert ("xx2":ppobj) (!pt) [2];
2.982 + pt:= insert ("xx3":ppobj) (!pt) [3];
2.983 + pt:= insert ("xx2.1":ppobj) (!pt) [2,1];
2.984 + pt:= insert ("xx2.2":ppobj) (!pt) [2,2];
2.985 + pt:= insert ("xx2.1.1":ppobj) (!pt) [2,1,1];
2.986 + pt:= insert ("xx2.1.2":ppobj) (!pt) [2,1,2];
2.987 + pt:= insert ("xx2.1.3":ppobj) (!pt) [2,1,3];
2.988 +*)
2.989 +
2.990 +(*.insert children to a node without children.*)
2.991 +(*compare: fun insert*)
2.992 +fun ins_chn _ EmptyPtree (_:pos) = raise PTREE "ins_chn: EmptyPtree"
2.993 + | ins_chn ns (Nd _) [] = raise PTREE "ins_chn: pos = []"
2.994 + | ins_chn ns (Nd (b, bs)) (p::[]) =
2.995 + if p > length bs then raise PTREE "ins_chn: pos not existent"
2.996 + else let val Nd (b', bs') = nth p bs
2.997 + in if null bs' then Nd (b, repl_app bs p (Nd (b', ns)))
2.998 + else raise PTREE "ins_chn: pos mustNOT be overwritten" end
2.999 + | ins_chn ns (Nd (b, bs)) (p::ps) =
2.1000 + Nd (b, repl_app bs p (ins_chn ns (nth p bs) ps));
2.1001 +
2.1002 +print_depth 11;ins_chn;print_depth 3 (*###insert#########################*);
2.1003 +
2.1004 +
2.1005 +(** apply f to obj at pos, f: ppobj -> ppobj **)
2.1006 +
2.1007 +fun appl_to_node f (Nd (b,bs)) = Nd (f b, bs);
2.1008 +fun appl_obj f EmptyPtree [] = EmptyPtree
2.1009 + | appl_obj f EmptyPtree _ = raise PTREE "appl_obj f Empty _"
2.1010 + | appl_obj f (Nd (b, bs)) [] = Nd (f b, bs)
2.1011 + | appl_obj f (Nd (b, bs)) (p::[]) =
2.1012 + Nd (b, repl_app bs p (((appl_to_node f) o (nth p)) bs))
2.1013 + | appl_obj f (Nd (b, bs)) (p::ps) =
2.1014 + Nd (b, repl_app bs p (appl_obj f (nth p bs) (ps:pos)));
2.1015 +
2.1016 +(* for use by appl_obj *)
2.1017 +fun repl_form f (PrfObj {cell=c,form= _,tac=tac,loc=loc,
2.1018 + branch=branch,result=result,ostate=ostate}) =
2.1019 + PrfObj {cell=c,form= f,tac=tac,loc=loc,
2.1020 + branch=branch,result=result,ostate=ostate}
2.1021 + | repl_form _ _ = raise PTREE "repl_form takes no PblObj";
2.1022 +fun repl_pbl x (PblObj {cell=cell,origin=origin,fmz=fmz,
2.1023 + spec=spec,probl=_,meth=meth,env=env,loc=loc,
2.1024 + branch=branch,result=result,ostate=ostate}) =
2.1025 + PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl= x,
2.1026 + meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
2.1027 + | repl_pbl _ _ = raise PTREE "repl_pbl takes no PrfObj";
2.1028 +fun repl_met x (PblObj {cell=cell,origin=origin,fmz=fmz,
2.1029 + spec=spec,probl=probl,meth=_,env=env,loc=loc,
2.1030 + branch=branch,result=result,ostate=ostate}) =
2.1031 + PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
2.1032 + meth= x,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
2.1033 + | repl_met _ _ = raise PTREE "repl_pbl takes no PrfObj";
2.1034 +
2.1035 +fun repl_spec x (PblObj {cell=cell,origin=origin,fmz=fmz,
2.1036 + spec= _,probl=probl,meth=meth,env=env,loc=loc,
2.1037 + branch=branch,result=result,ostate=ostate}) =
2.1038 + PblObj {cell=cell,origin=origin,fmz=fmz,spec= x,probl=probl,
2.1039 + meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
2.1040 + | repl_spec _ _ = raise PTREE "repl_domID takes no PrfObj";
2.1041 +fun repl_domID x (PblObj {cell=cell,origin=origin,fmz=fmz,
2.1042 + spec=(_,p,m),probl=probl,meth=meth,env=env,loc=loc,
2.1043 + branch=branch,result=result,ostate=ostate}) =
2.1044 + PblObj {cell=cell,origin=origin,fmz=fmz,spec=(x,p,m),probl=probl,
2.1045 + meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
2.1046 + | repl_domID _ _ = raise PTREE "repl_domID takes no PrfObj";
2.1047 +fun repl_pblID x (PblObj {cell=cell,origin=origin,fmz=fmz,
2.1048 + spec=(d,_,m),probl=probl,meth=meth,env=env,loc=loc,
2.1049 + branch=branch,result=result,ostate=ostate}) =
2.1050 + PblObj {cell=cell,origin=origin,fmz=fmz,spec=(d,x,m),probl=probl,
2.1051 + meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
2.1052 + | repl_pblID _ _ = raise PTREE "repl_pblID takes no PrfObj";
2.1053 +fun repl_metID x (PblObj {cell=cell,origin=origin,fmz=fmz,
2.1054 + spec=(d,p,_),probl=probl,meth=meth,env=env,loc=loc,
2.1055 + branch=branch,result=result,ostate=ostate}) =
2.1056 + PblObj {cell=cell,origin=origin,fmz=fmz,spec=(d,p,x),probl=probl,
2.1057 + meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
2.1058 + | repl_metID _ _ = raise PTREE "repl_metID takes no PrfObj";
2.1059 +
2.1060 +fun repl_result l f' s (PrfObj {cell=cell,form=form,tac=tac,loc=_,
2.1061 + branch=branch,result = _ ,ostate = _}) =
2.1062 + PrfObj {cell=cell,form=form,tac=tac,loc= l,
2.1063 + branch=branch,result = f',ostate = s}
2.1064 + | repl_result l f' s (PblObj {cell=cell,origin=origin,fmz=fmz,
2.1065 + spec=spec,probl=probl,meth=meth,env=env,loc=_,
2.1066 + branch=branch,result= _ ,ostate= _}) =
2.1067 + PblObj {cell=cell,origin=origin,fmz=fmz,
2.1068 + spec=spec,probl=probl,meth=meth,env=env,loc= l,
2.1069 + branch=branch,result= f',ostate= s};
2.1070 +
2.1071 +fun repl_tac x (PrfObj {cell=cell,form=form,tac= _,loc=loc,
2.1072 + branch=branch,result=result,ostate=ostate}) =
2.1073 + PrfObj {cell=cell,form=form,tac= x,loc=loc,
2.1074 + branch=branch,result=result,ostate=ostate}
2.1075 + | repl_tac _ _ = raise PTREE "repl_tac takes no PblObj";
2.1076 +
2.1077 +fun repl_branch b (PblObj {cell=cell,origin=origin,fmz=fmz,
2.1078 + spec=spec,probl=probl,meth=meth,env=env,loc=loc,
2.1079 + branch= _,result=result,ostate=ostate}) =
2.1080 + PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
2.1081 + meth=meth,env=env,loc=loc,branch= b,result=result,ostate=ostate}
2.1082 + | repl_branch b (PrfObj {cell=cell,form=form,tac=tac,loc=loc,
2.1083 + branch= _,result=result,ostate=ostate}) =
2.1084 + PrfObj {cell=cell,form=form,tac=tac,loc=loc,
2.1085 + branch= b,result=result,ostate=ostate};
2.1086 +
2.1087 +fun repl_env e
2.1088 + (PblObj {cell=cell,origin=origin,fmz=fmz,
2.1089 + spec=spec,probl=probl,meth=meth,env=_,loc=loc,
2.1090 + branch=branch,result=result,ostate=ostate}) =
2.1091 + PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
2.1092 + meth=meth,env=e,loc=loc,branch=branch,
2.1093 + result=result,ostate=ostate}
2.1094 + | repl_env _ _ = raise PTREE "repl_ets takes no PrfObj";
2.1095 +
2.1096 +fun repl_oris oris
2.1097 + (PblObj {cell=cell,origin=(_,spe,hdf),fmz=fmz,
2.1098 + spec=spec,probl=probl,meth=meth,env=env,loc=loc,
2.1099 + branch=branch,result=result,ostate=ostate}) =
2.1100 + PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl,
2.1101 + meth=meth,env=env,loc=loc,branch=branch,
2.1102 + result=result,ostate=ostate}
2.1103 + | repl_oris _ _ = raise PTREE "repl_oris takes no PrfObj";
2.1104 +fun repl_orispec spe
2.1105 + (PblObj {cell=cell,origin=(oris,_,hdf),fmz=fmz,
2.1106 + spec=spec,probl=probl,meth=meth,env=env,loc=loc,
2.1107 + branch=branch,result=result,ostate=ostate}) =
2.1108 + PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl,
2.1109 + meth=meth,env=env,loc=loc,branch=branch,
2.1110 + result=result,ostate=ostate}
2.1111 + | repl_orispec _ _ = raise PTREE "repl_orispec takes no PrfObj";
2.1112 +
2.1113 +fun repl_loc l (PblObj {cell=cell,origin=origin,fmz=fmz,
2.1114 + spec=spec,probl=probl,meth=meth,env=env,loc=_,
2.1115 + branch=branch,result=result,ostate=ostate}) =
2.1116 + PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
2.1117 + meth=meth,env=env,loc=l,branch=branch,result=result,ostate=ostate}
2.1118 + | repl_loc l (PrfObj {cell=cell,form=form,tac=tac,loc=_,
2.1119 + branch=branch,result=result,ostate=ostate}) =
2.1120 + PrfObj {cell=cell,form=form,tac=tac,loc= l,
2.1121 + branch=branch,result=result,ostate=ostate};
2.1122 +
2.1123 +fun uni__cid cell'
2.1124 + (PblObj {cell=cell,origin=origin,fmz=fmz,
2.1125 + spec=spec,probl=probl,meth=meth,env=env,loc=loc,
2.1126 + branch=branch,result=result,ostate=ostate}) =
2.1127 + PblObj {cell=cell union cell',origin=origin,fmz=fmz,spec=spec,probl=probl,
2.1128 + meth=meth,env=env,loc=loc,branch=branch,
2.1129 + result=result,ostate=ostate}
2.1130 + | uni__cid cell'
2.1131 + (PrfObj {cell=cell,form=form,tac=tac,loc=loc,
2.1132 + branch=branch,result=result,ostate=ostate}) =
2.1133 + PrfObj {cell=cell union cell',form=form,tac=tac,loc=loc,
2.1134 + branch=branch,result=result,ostate=ostate};
2.1135 +
2.1136 +(*WN050219 put here for interpreting code for cut_tree below...*)
2.1137 +type ocalhd =
2.1138 + bool * (*ALL itms+preconds true*)
2.1139 + pos_ * (*model belongs to Problem | Method*)
2.1140 + term * (*header: Problem... or Cas
2.1141 + FIXXXME.12.03: item! for marking syntaxerrors*)
2.1142 + itm list * (*model: given, find, relate*)
2.1143 + ((bool * term) list) *(*model: preconds*)
2.1144 + spec; (*specification*)
2.1145 +val e_ocalhd = (false, Und, e_term, [e_itm], [(false, e_term)], e_spec);
2.1146 +
2.1147 +datatype ptform =
2.1148 + Form of term
2.1149 + | ModSpec of ocalhd;
2.1150 +val e_ptform = Form e_term;
2.1151 +val e_ptform' = ModSpec e_ocalhd;
2.1152 +
2.1153 +
2.1154 +
2.1155 +(*.applies (snd f) to the branches at a pos if ((fst f) b),
2.1156 + f : (ppobj -> bool) * (int -> ptree list -> ptree list).*)
2.1157 +
2.1158 +fun appl_branch f EmptyPtree [] = (EmptyPtree, false)
2.1159 + | appl_branch f EmptyPtree _ = raise PTREE "appl_branch f Empty _"
2.1160 + | appl_branch f (Nd ( _, _)) [] = raise PTREE "appl_branch f _ []"
2.1161 + | appl_branch f (Nd (b, bs)) (p::[]) =
2.1162 + if (fst f) b then (Nd (b, (snd f) (p:posel) bs), true)
2.1163 + else (Nd (b, bs), false)
2.1164 + | appl_branch f (Nd (b, bs)) (p::ps) =
2.1165 + let val (b',bool) = appl_branch f (nth p bs) ps
2.1166 + in (Nd (b, repl_app bs p b'), bool) end;
2.1167 +
2.1168 +(* for cut_level; appl_branch(deprecated) *)
2.1169 +fun test_trans (PrfObj{branch = Transitive,...}) = true
2.1170 + | test_trans (PblObj{branch = Transitive,...}) = true
2.1171 + | test_trans _ = false;
2.1172 +
2.1173 +fun is_pblobj' pt (p:pos) =
2.1174 + let val ppobj = get_obj I pt p
2.1175 + in is_pblobj ppobj end;
2.1176 +
2.1177 +
2.1178 +fun delete_result pt (p:pos) =
2.1179 + (appl_obj (repl_result (fst (get_obj g_loc pt p), None)
2.1180 + (e_term,[]) Incomplete) pt p);
2.1181 +
2.1182 +fun del_res (PblObj {cell, fmz, origin, spec, probl, meth,
2.1183 + env, loc=(l1,_), branch, result, ostate}) =
2.1184 + PblObj {cell=cell,fmz=fmz,origin=origin,spec=spec,probl=probl,meth=meth,
2.1185 + env=env, loc=(l1,None), branch=branch, result=(e_term,[]),
2.1186 + ostate=Incomplete}
2.1187 +
2.1188 + | del_res (PrfObj {cell, form, tac, loc=(l1,_), branch, result, ostate}) =
2.1189 + PrfObj {cell=cell,form=form,tac=tac, loc=(l1,None), branch=branch,
2.1190 + result=(e_term,[]), ostate=Incomplete};
2.1191 +
2.1192 +
2.1193 +
2.1194 +
2.1195 +
2.1196 +
2.1197 +(*
2.1198 +fun update_fmz pt pos x = appl_obj (repl_fmz x) pt pos;
2.1199 + 1.00 not used anymore*)
2.1200 +
2.1201 +(*FIXME.WN.12.03: update_X X pos pt -> pt could be chained by o (efficiency?)*)
2.1202 +fun update_env pt pos x = appl_obj (repl_env x) pt pos;
2.1203 +fun update_domID pt pos x = appl_obj (repl_domID x) pt pos;
2.1204 +fun update_pblID pt pos x = appl_obj (repl_pblID x) pt pos;
2.1205 +fun update_metID pt pos x = appl_obj (repl_metID x) pt pos;
2.1206 +fun update_spec pt pos x = appl_obj (repl_spec x) pt pos;
2.1207 +
2.1208 +fun update_pbl pt pos x = appl_obj (repl_pbl x) pt pos;
2.1209 +fun update_pblppc pt pos x = appl_obj (repl_pbl x) pt pos;
2.1210 +
2.1211 +fun update_met pt pos x = appl_obj (repl_met x) pt pos;
2.1212 +(*1.09.01 ----
2.1213 +fun update_metppc pt pos x =
2.1214 + let val {rew_ord'=od,rls'=rs,asm_thm=at,asm_rls=ar,...} =
2.1215 + get_obj g_met pt pos
2.1216 + in appl_obj (repl_met
2.1217 + {rew_ord'=od,rls'=rs,asm_thm=at,asm_rls=ar,ppc=x})
2.1218 + pt pos end;*)
2.1219 +fun update_metppc pt pos x = appl_obj (repl_met x) pt pos;
2.1220 +
2.1221 +fun union_cid pt pos x = appl_obj (uni__cid x) pt pos;
2.1222 +
2.1223 +fun update_branch pt pos x = appl_obj (repl_branch x) pt pos;
2.1224 +fun update_tac pt pos x = appl_obj (repl_tac x) pt pos;
2.1225 +
2.1226 +fun update_oris pt pos x = appl_obj (repl_oris x) pt pos;
2.1227 +fun update_orispec pt pos x = appl_obj (repl_orispec x) pt pos;
2.1228 +
2.1229 + (*done by append_* !! 3.5.02*)
2.1230 +fun update_loc pt (p,_) (ScrState ([],[],None,
2.1231 + Const ("empty",_),Sundef,false)) =
2.1232 + appl_obj (repl_loc (None,None)) pt p
2.1233 + | update_loc pt (p,Res) x =
2.1234 + let val (lform,_) = get_obj g_loc pt p
2.1235 + in appl_obj (repl_loc (lform,Some x)) pt p end
2.1236 +
2.1237 + | update_loc pt (p,_) x =
2.1238 + let val (_,lres) = get_obj g_loc pt p
2.1239 + in appl_obj (repl_loc (Some x,lres)) pt p end;
2.1240 +
2.1241 +(*13.8.02---------------------------
2.1242 +fun get_loc EmptyPtree _ = None
2.1243 + | get_loc pt (p,Res) =
2.1244 + let val (lfrm,lres) = get_obj g_loc pt p
2.1245 + in if lres = e_istate then lfrm else lres end
2.1246 + | get_loc pt (p,_) =
2.1247 + let val (lfrm,lres) = get_obj g_loc pt p
2.1248 + in if lfrm = e_istate then lres else lfrm end; 5.10.00: too liberal ?*)
2.1249 +(*13.8.02: options, because istate is no equalitype any more*)
2.1250 +fun get_loc EmptyPtree _ = e_istate
2.1251 + | get_loc pt (p,Res) =
2.1252 + (case get_obj g_loc pt p of
2.1253 + (Some i, None) => i
2.1254 + | (None , None) => e_istate
2.1255 + | (_ , Some i) => i)
2.1256 + | get_loc pt (p,_) =
2.1257 + (case get_obj g_loc pt p of
2.1258 + (None , Some i) => i (*13.8.02 just copied from ^^^: too liberal ?*)
2.1259 + | (None , None) => e_istate
2.1260 + | (Some i, _) => i);
2.1261 +val get_istate = get_loc; (*3.5.02*)
2.1262 +
2.1263 +(*.collect the assumptions within a problem up to a certain position.*)
2.1264 +type asms = (term * pos) list;(*WN0502 should be (pos' * term) list
2.1265 + ...........===^===*)
2.1266 +
2.1267 +fun get_asm (b:pos, p:pos) (Nd (PblObj {result=(_,asm),...},_)) =
2.1268 + ((*writeln ("### get_asm PblObj:(b,p)= "^
2.1269 + (pair2str(ints2str b, ints2str p)));*)
2.1270 + (map (rpair b) asm):asms)
2.1271 + | get_asm (b, p) (Nd (PrfObj {result=(_,asm),...}, [])) =
2.1272 + ((*writeln ("### get_asm PrfObj []:(b,p)= "^
2.1273 + (pair2str(ints2str b, ints2str p)));*)
2.1274 + (map (rpair b) asm))
2.1275 + | get_asm (b, p:pos) (Nd (PrfObj _, nds)) =
2.1276 + let (*val _= writeln ("### get_asm PrfObj nds:(b,p)= "^
2.1277 + (pair2str(ints2str b, ints2str p)));*)
2.1278 + val levdn =
2.1279 + if p <> [] then (b @ [hd p]:pos, tl p:pos)
2.1280 + else (b @ [1], [99999]) (*_deeper_ nesting is always _before_ p*)
2.1281 + in gets_asm levdn 1 nds end
2.1282 +and gets_asm _ _ [] = []
2.1283 + | gets_asm (b, p' as p::ps) i (nd::nds) =
2.1284 + if p < i then []
2.1285 + else ((*writeln ("### gets_asm: (b,p')= "^(pair2str(ints2str b,
2.1286 + ints2str p')));*)
2.1287 + (get_asm (b @ [i], ps) nd) @ (gets_asm (b, p') (i + 1) nds));
2.1288 +
2.1289 +fun get_assumptions_ (Nd (PblObj {result=(r,asm),...}, cn)) (([], _):pos') =
2.1290 + if r = e_term then gets_asm ([], [99999]) 1 cn
2.1291 + else map (rpair []) asm
2.1292 + | get_assumptions_ pt (p,p_) =
2.1293 + let val (cn, base) = par_children pt p
2.1294 + val offset = drop (length base, p)
2.1295 + val base' = replicate (length base) 1
2.1296 + val offset' = case p_ of
2.1297 + Frm => let val (qs,q) = split_last offset
2.1298 + in qs @ [q - 1] end
2.1299 + | _ => offset
2.1300 + (*val _= writeln ("... get_assumptions: (b,o)= "^
2.1301 + (pair2str(ints2str base',ints2str offset)))*)
2.1302 + in gets_asm (base', offset) 1 cn end;
2.1303 +
2.1304 +
2.1305 +(*---------
2.1306 +end
2.1307 +
2.1308 +open Ptree;
2.1309 +----------*)
2.1310 +
2.1311 +(*pos of the formula on FE relative to the current pos,
2.1312 + which is the next writepos*)
2.1313 +fun pre_pos ([]:pos) = []:pos
2.1314 + | pre_pos pp =
2.1315 + let val (ps,p) = split_last pp
2.1316 + in case p of 1 => ps | n => ps @ [n-1] end;
2.1317 +
2.1318 +(*WN.20.5.03 ... but not used*)
2.1319 +fun posless [] (_::_) = true
2.1320 + | posless (_::_) [] = false
2.1321 + | posless (p::ps) (q::qs) = if p = q then posless ps qs else p < q;
2.1322 +(* posless [2,3,4] [3,4,5];
2.1323 +true
2.1324 +> posless [2,3,4] [1,2,3];
2.1325 +false
2.1326 +> posless [2,3] [2,3,4];
2.1327 +true
2.1328 +> posless [2,3,4] [2,3];
2.1329 +false
2.1330 +> posless [6] [6,5,2];
2.1331 +true
2.1332 ++++ see Isabelle/../library.ML*)
2.1333 +
2.1334 +
2.1335 +(**.development for extracting an 'interval' from ptree.**)
2.1336 +
2.1337 +(*version 1 stopped 8.03 in favour of get_interval with !!!move_dn
2.1338 + actually used (inefficient) version with move_dn: see modspec.sml*)
2.1339 +local
2.1340 +
2.1341 +fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*)
2.1342 +fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*)
2.1343 +fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x;
2.1344 +fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;
2.1345 +
2.1346 +fun getnd i (b,p) q (Nd (po, nds)) =
2.1347 + (if i <= 0 then [[b]] else []) @
2.1348 + (getnds (i-1) true (b@[hdp p], tlp p) (tlq q)
2.1349 + (take_fromto (hdp p) (hdq q) nds))
2.1350 +
2.1351 +and getnds _ _ _ _ [] = [] (*no children*)
2.1352 + | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*)
2.1353 +
2.1354 + | getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*)
2.1355 + (getnd i ( b, p ) [99999] n1) @
2.1356 + (getnd ~99999 (lev_on b,[0]) q n2)
2.1357 +
2.1358 + | getnds i _ (b,p) q [n1, n2] = (*intern, r-margin*)
2.1359 + (getnd i ( b,[0]) [99999] n1) @
2.1360 + (getnd ~99999 (lev_on b,[0]) q n2)
2.1361 +
2.1362 + | getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*)
2.1363 + (getnd i ( b, p ) [99999] nd) @
2.1364 + (getnds ~99999 false (lev_on b,[0]) q nds)
2.1365 +
2.1366 + | getnds i _ (b,p) q (nd::(nds as _::_)) = (*intern, ...*)
2.1367 + (getnd i ( b,[0]) [99999] nd) @
2.1368 + (getnds ~99999 false (lev_on b,[0]) q nds);
2.1369 +in
2.1370 +(*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes
2.1371 + where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
2.1372 +(1) the 'f' are given
2.1373 +(1a) by 'from' if 'f' = the respective element of 'from' (left margin)
2.1374 +(1b) -inifinity, if 'f' > the respective element of 'from' (internal node)
2.1375 +(2) the 't' ar given
2.1376 +(2a) by 'to' if 't' = the respective element of 'to' (right margin)
2.1377 +(2b) inifinity, if 't' < the respective element of 'to (internal node)'
2.1378 +the 'f' and 't' are set by hdp,... *)
2.1379 +fun get_trace pt p q =
2.1380 + (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q)))
2.1381 + (take_fromto (hdp p) (hdq q) (children pt));
2.1382 +end;
2.1383 +(*WN0510 stoppde this development;
2.1384 + actually used (inefficient) version with move_dn: getElementsFromTo*)
2.1385 +
2.1386 +
2.1387 +
2.1388 +
2.1389 +fun get_somespec ((dI,pI,mI):spec) ((dI',pI',mI'):spec) =
2.1390 + let val domID = if dI = e_domID
2.1391 + then if dI' = e_domID
2.1392 + then raise error"pt_extract: no domID in probl,origin"
2.1393 + else dI'
2.1394 + else dI
2.1395 + val pblID = if pI = e_pblID
2.1396 + then if pI' = e_pblID
2.1397 + then raise error"pt_extract: no pblID in probl,origin"
2.1398 + else pI'
2.1399 + else pI
2.1400 + val metID = if mI = e_metID
2.1401 + then if pI' = e_metID
2.1402 + then raise error"pt_extract: no metID in probl,origin"
2.1403 + else mI'
2.1404 + else mI
2.1405 + in (domID, pblID, metID):spec end;
2.1406 +fun get_somespec' ((dI,pI,mI):spec) ((dI',pI',mI'):spec) =
2.1407 + let val domID = if dI = e_domID then dI' else dI
2.1408 + val pblID = if pI = e_pblID then pI' else pI
2.1409 + val metID = if mI = e_metID then mI' else mI
2.1410 + in (domID, pblID, metID):spec end;
2.1411 +
2.1412 +(*extract a formula or model from ptree for itms2itemppc or model2xml*)
2.1413 +fun preconds2str bts =
2.1414 + (strs2str o (map (linefeed o pair2str o
2.1415 + (apsnd term2str) o
2.1416 + (apfst bool2str)))) bts;
2.1417 +fun ocalhd2str ((b, p, hdf, itms, prec, spec):ocalhd) =
2.1418 + "("^bool2str b^", "^pos_2str p^", "^term2str hdf^
2.1419 + ", "^itms2str (assoc_thy "Isac.thy") itms^
2.1420 + ", "^preconds2str prec^", \n"^spec2str spec^" )";
2.1421 +
2.1422 +
2.1423 +
2.1424 +fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj;
2.1425 +
2.1426 +
2.1427 +(**.functions for the 'ptree iterator' as seen from the FE-Kernel interface.**)
2.1428 +
2.1429 +(*.move one step down into existing nodes of ptree; regard TransitiveB.*)
2.1430 +fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*)
2.1431 +(* val (Nd (c, ns), ([],p_)) = (pt, get_pos cI uI);
2.1432 + *)
2.1433 + if is_pblobj c
2.1434 + then case p_ of (*Frm => ([], Pbl) 1.12.03
2.1435 + |*) Res => raise PTREE "move_dn: end of calculation"
2.1436 + | _ => if null ns (*go down from Pbl + Met*)
2.1437 + then raise PTREE "move_dn: solve problem not started"
2.1438 + else ([1], Frm)
2.1439 + else (case p_ of Res => raise PTREE "move_dn: end of (sub-)tree"
2.1440 + | _ => if null ns
2.1441 + then raise PTREE "move_dn: pos not existent 1"
2.1442 + else ([1], Frm))
2.1443 +
2.1444 + (*iterate towards end of pos*)
2.1445 +(* val (P,(Nd (_, ns)),(p::(ps as (_::_)),p_)) = ([]:pos, pt, get_pos cI uI);
2.1446 + val (P,(Nd (_, ns)),(p::(ps as (_::_)),p_)) = ((P@[p]),(nth p ns),(ps, p_));
2.1447 + *)
2.1448 + | move_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
2.1449 + if p > length ns then raise PTREE "move_dn: pos not existent 2"
2.1450 + else move_dn ((P@[p]): pos) (nth p ns) (ps, p_)
2.1451 +(* val (P, (Nd (c, ns)), ([p], p_)) = ((P@[p]), (nth p ns), (ps, p_));
2.1452 + val (P, (Nd (c, ns)), ([p], p_)) = ([],pt,get_pos cI uI);
2.1453 + *)
2.1454 + | move_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
2.1455 + if p > length ns then raise PTREE "move_dn: pos not existent 3"
2.1456 + else if is_pblnd (nth p ns) then
2.1457 + ((*writeln("### move_dn: is_pblnd (nth p ns), P= "^ints2str' P^", \n"^
2.1458 + "length ns= "^((string_of_int o length) ns)^
2.1459 + ", p= "^string_of_int p^", p_= "^pos_2str p_);*)
2.1460 + case p_ of Res => if p = length ns
2.1461 + then if g_ostate c = Complete then (P, Res)
2.1462 + else raise PTREE (ints2str' P^" not complete")
2.1463 + (*FIXME here handle not-sequent-branches*)
2.1464 + else if g_branch c = TransitiveB
2.1465 + andalso (not o is_pblnd o (nth (p+1))) ns
2.1466 + then (P@[p+1], Res)
2.1467 + else (P@[p+1], if is_pblnd (nth (p+1) ns)
2.1468 + then Pbl else Frm)
2.1469 + | _ => if (null o children o (nth p)) ns (*go down from Pbl*)
2.1470 + then raise PTREE "move_dn: solve subproblem not started"
2.1471 + else (P @ [p, 1],
2.1472 + if (is_pblnd o hd o children o (nth p)) ns
2.1473 + then Pbl else Frm)
2.1474 + )
2.1475 + (* val (P, Nd (c, ns), ([p], p_)) = ([], pt, ([1], Frm));
2.1476 + *)
2.1477 + else case p_ of Frm => if (null o children o (nth p)) ns
2.1478 + (*then if g_ostate c = Complete then (P@[p],Res)*)
2.1479 + then if g_ostate' (nth p ns) = Complete
2.1480 + then (P@[p],Res)
2.1481 + else raise PTREE "move_dn: pos not existent 4"
2.1482 + else (P @ [p, 1], (*go down*)
2.1483 + if (is_pblnd o hd o children o (nth p)) ns
2.1484 + then Pbl else Frm)
2.1485 + | Res => if p = length ns
2.1486 + then
2.1487 + if g_ostate c = Complete then (P, Res)
2.1488 + else raise PTREE (ints2str' P^" not complete")
2.1489 + else
2.1490 + if g_branch c = TransitiveB
2.1491 + andalso (not o is_pblnd o (nth (p+1))) ns
2.1492 + then if (null o children o (nth (p+1))) ns
2.1493 + then (P@[p+1], Res)
2.1494 + else (P@[p+1,1], Frm)(*040221*)
2.1495 + else (P@[p+1], if is_pblnd (nth (p+1) ns)
2.1496 + then Pbl else Frm);
2.1497 +
2.1498 +
2.1499 +
2.1500 +(*.go one level down into ptree.*)
2.1501 +fun movelevel_dn [] (Nd (c, ns)) ([],p_) = (*root problem*)
2.1502 + if is_pblobj c
2.1503 + then if null ns
2.1504 + then raise PTREE "solve problem not started"
2.1505 + else ([1], if (is_pblnd o hd) ns then Pbl else Frm)
2.1506 + else raise PTREE "pos not existent 1"
2.1507 +
2.1508 + (*iterate towards end of pos*)
2.1509 + | movelevel_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
2.1510 + if p > length ns then raise PTREE "pos not existent 2"
2.1511 + else movelevel_dn (P@[p]) (nth p ns) (ps, p_)
2.1512 +
2.1513 + | movelevel_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
2.1514 + if p > length ns then raise PTREE "pos not existent 3" else
2.1515 + case p_ of Res =>
2.1516 + if p = length ns
2.1517 + then raise PTREE "no children"
2.1518 + else
2.1519 + if g_branch c = TransitiveB
2.1520 + then if (null o children o (nth (p+1))) ns
2.1521 + then raise PTREE "no children"
2.1522 + else (P @ [p+1, 1],
2.1523 + if (is_pblnd o hd o children o (nth (p+1))) ns
2.1524 + then Pbl else Frm)
2.1525 + else if (null o children o (nth p)) ns
2.1526 + then raise PTREE "no children"
2.1527 + else (P @ [p, 1], if (is_pblnd o hd o children o (nth p)) ns
2.1528 + then Pbl else Frm)
2.1529 + | _ => if (null o children o (nth p)) ns
2.1530 + then raise PTREE "no children"
2.1531 + else (P @ [p, 1], (*go down*)
2.1532 + if (is_pblnd o hd o children o (nth p)) ns
2.1533 + then Pbl else Frm);
2.1534 +
2.1535 +
2.1536 +
2.1537 +(*.go to the previous position in ptree; regard TransitiveB.*)
2.1538 +fun move_up _ (Nd (c, ns)) (([],p_):pos') = (*root problem*)
2.1539 + if is_pblobj c
2.1540 + then case p_ of Res => if null ns then ([], Pbl) (*Res -> Pbl (not Met)!*)
2.1541 + else ([length ns], Res)
2.1542 + | _ => raise PTREE "begin of calculation"
2.1543 + else raise PTREE "pos not existent"
2.1544 +
2.1545 + | move_up P (Nd (_, ns)) (p::(ps as (_::_)),p_) = (*iterate to end of pos*)
2.1546 + if p > length ns then raise PTREE "pos not existent"
2.1547 + else move_up (P@[p]) (nth p ns) (ps,p_)
2.1548 +
2.1549 + | move_up P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
2.1550 + if p > length ns then raise PTREE "pos not existent"
2.1551 + else if is_pblnd (nth p ns) then
2.1552 + case p_ of Res =>
2.1553 + let val nc = (length o children o (nth p)) ns
2.1554 + in if nc = 0 then (P@[p], Pbl) (*Res -> Pbl (not Met)!*)
2.1555 + else (P @ [p, nc], Res) end (*go down*)
2.1556 + | _ => if p = 1 then (P, Pbl) else (P@[p-1], Res)
2.1557 + else case p_ of Frm => if p <> 1 then (P, Frm)
2.1558 + else if is_pblobj c then (P, Pbl) else (P, Frm)
2.1559 + | Res =>
2.1560 + let val nc = (length o children o (nth p)) ns
2.1561 + in if nc = 0 (*cannot go down*)
2.1562 + then if g_branch c = TransitiveB andalso p <> 1
2.1563 + then (P@[p-1], Res) else (P@[p], Frm)
2.1564 + else (P @ [p, nc], Res) end; (*go down*)
2.1565 +
2.1566 +
2.1567 +
2.1568 +(*.go one level up in ptree; sets the position on Frm.*)
2.1569 +fun movelevel_up _ (Nd (c, ns)) (([],p_):pos') = (*root problem*)
2.1570 + raise PTREE "pos not existent"
2.1571 +
2.1572 + (*iterate towards end of pos*)
2.1573 + | movelevel_up P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
2.1574 + if p > length ns then raise PTREE "pos not existent"
2.1575 + else movelevel_up (P@[p]) (nth p ns) (ps,p_)
2.1576 +
2.1577 + | movelevel_up P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
2.1578 + if p > length ns then raise PTREE "pos not existent"
2.1579 + else if is_pblobj c then (P, Pbl) else (P, Frm);
2.1580 +
2.1581 +
2.1582 +(*.go to the next calc-head up in the calc-tree.*)
2.1583 +fun movecalchd_up pt ((p, Res):pos') =
2.1584 + (par_pblobj pt p, Pbl):pos'
2.1585 + | movecalchd_up pt (p, _) =
2.1586 + if is_pblobj (get_obj I pt p)
2.1587 + then (p, Pbl) else (par_pblobj pt p, Pbl);
2.1588 +
2.1589 +(*WN0502 made for interSteps; _only_ works for branch TransitiveB*)
2.1590 +fun lev_pred' pt (pos:pos' as (p,Res)) =
2.1591 + if (is_pblobj o (get_obj I pt)) p then (p,Pbl):pos' else move_up [] pt pos
2.1592 + | lev_pred' pt p = move_up [] pt p;
2.1593 +
2.1594 +
2.1595 +(**.insert into ctree and cut branches accordingly.**)
2.1596 +
2.1597 +(*.get all positions of certain intervals on the ctree.*)
2.1598 +(*OLD VERSION without move_dn; kept for occasional redesign
2.1599 + get all pos's to be cut in a ptree
2.1600 + below a pos or from a ptree list after i-th element (NO level_up).*)
2.1601 +fun get_allpos' (_:pos, _:posel) EmptyPtree = ([]:pos' list)
2.1602 + | get_allpos' (p, 1) (Nd (b, bs)) = (*p is pos of Nd*)
2.1603 + if g_ostate b = Incomplete
2.1604 + then (writeln("get_allpos' (p, 1) Incomplete: p="^ints2str' p);
2.1605 + [(p,Frm)] @ (get_allpos's (p, 1) bs)
2.1606 + )
2.1607 + else (writeln("get_allpos' (p, 1) else: p="^ints2str' p);
2.1608 + [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p,Res)]
2.1609 + )
2.1610 + (*WN041020 here we assume what is presented on the worksheet ?!*)
2.1611 + | get_allpos' (p, i) (Nd (b, bs)) = (*p is pos of Nd*)
2.1612 + if length bs > 0 orelse is_pblobj b
2.1613 + then if g_ostate b = Incomplete
2.1614 + then [(p,Frm)] @ (get_allpos's (p, 1) bs)
2.1615 + else [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p,Res)]
2.1616 + else
2.1617 + if g_ostate b = Incomplete
2.1618 + then []
2.1619 + else [(p,Res)]
2.1620 +(*WN041020 here we assume what is presented on the worksheet ?!*)
2.1621 +and get_allpos's _ [] = []
2.1622 + | get_allpos's (p, i) (pt::pts) = (*p is pos of parent-Nd*)
2.1623 + (get_allpos' (p@[i], i) pt) @ (get_allpos's (p, i+1) pts);
2.1624 +
2.1625 +(*.get all positions of certain intervals on the ctree.*)
2.1626 +(*NEW version WN050225*)
2.1627 +
2.1628 +
2.1629 +(*.cut branches.*)
2.1630 +(*before WN041019......
2.1631 +val cut_branch = (test_trans, curry take):
2.1632 + (ppobj -> bool) * (int -> ptree list -> ptree list);
2.1633 +.. formlery used for ...
2.1634 +fun cut_tree''' _ [] = EmptyPtree
2.1635 + | cut_tree''' pt pos =
2.1636 + let val (pt',cut) = appl_branch cut_branch pt pos
2.1637 + in if cut andalso length pos > 1 then cut_tree''' pt' (lev_up pos)
2.1638 + else pt' end;
2.1639 +*)
2.1640 +(*OLD version before WN050225*)
2.1641 +(*WN050106 like cut_level, but deletes exactly 1 node --- for tests ONLY*)
2.1642 +fun cut_level_'_ (_:pos' list) (_:pos) EmptyPtree (_:pos') =
2.1643 + raise PTREE "cut_level_'_ Empty _"
2.1644 + | cut_level_'_ _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level_'_ _ []"
2.1645 + | cut_level_'_ cuts P (Nd (b, bs)) (p::[],p_) =
2.1646 + if test_trans b
2.1647 + then (Nd (b, drop_nth [] (p:posel, bs)),
2.1648 + (* ~~~~~~~~~~~*)
2.1649 + cuts @
2.1650 + (if p_ = Frm then [(P@[p],Res)] else ([]:pos' list)) @
2.1651 + (*WN041020 here we assume what is presented on the worksheet ?!*)
2.1652 + (get_allpos's (P, p+1) (drop_nth [] (p, bs))))
2.1653 + (* ~~~~~~~~~~~*)
2.1654 + else (Nd (b, bs), cuts)
2.1655 + | cut_level_'_ cuts P (Nd (b, bs)) ((p::ps),p_) =
2.1656 + let val (bs',cuts') = cut_level_'_ cuts P (nth p bs) (ps, p_)
2.1657 + in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
2.1658 +
2.1659 +(*before WN050219*)
2.1660 +fun cut_level (_:pos' list) (_:pos) EmptyPtree (_:pos') =
2.1661 + raise PTREE "cut_level EmptyPtree _"
2.1662 + | cut_level _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level _ []"
2.1663 +
2.1664 + | cut_level cuts P (Nd (b, bs)) (p::[],p_) =
2.1665 + if test_trans b
2.1666 + then (Nd (b, take (p:posel, bs)),
2.1667 + cuts @
2.1668 + (if p_ = Frm andalso (*#*) g_ostate b = Complete
2.1669 + then [(P@[p],Res)] else ([]:pos' list)) @
2.1670 + (*WN041020 here we assume what is presented on the worksheet ?!*)
2.1671 + (get_allpos's (P, p+1) (takerest (p, bs))))
2.1672 + else (Nd (b, bs), cuts)
2.1673 +
2.1674 + | cut_level cuts P (Nd (b, bs)) ((p::ps),p_) =
2.1675 + let val (bs',cuts') = cut_level cuts P (nth p bs) (ps, p_)
2.1676 + in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
2.1677 +
2.1678 +(*OLD version before WN050219, overwritten below*)
2.1679 +fun cut_tree _ (([],_):pos') = raise PTREE "cut_tree _ ([],_)"
2.1680 + | cut_tree pt (pos as ([p],_)) =
2.1681 + let val (pt', cuts) = cut_level ([]:pos' list) [] pt pos
2.1682 + in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
2.1683 + then [] else [([],Res)])) end
2.1684 + | cut_tree pt (p,p_) =
2.1685 + let
2.1686 + fun cutfn pt cuts (p,p_) =
2.1687 + let val (pt', cuts') = cut_level [] (lev_up p) pt (p,p_)
2.1688 + val cuts'' = if get_obj g_ostate pt (lev_up p) = Incomplete
2.1689 + then [] else [(lev_up p, Res)]
2.1690 + in if length cuts' > 0 andalso length p > 1
2.1691 + then cutfn pt' (cuts @ cuts') (lev_up p, Frm(*-->(p,Res)*))
2.1692 + else (pt',cuts @ cuts') end
2.1693 + val (pt', cuts) = cutfn pt [] (p,p_)
2.1694 + in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
2.1695 + then [] else [([], Res)])) end;
2.1696 +
2.1697 +
2.1698 +
2.1699 +(*.get all positions in a ptree until ([],Res) or ostate=Incomplete
2.1700 +val get_allp = fn :
2.1701 + pos' list -> : accumulated, start with []
2.1702 + pos -> : the offset for subtrees wrt the root
2.1703 + ptree -> : (sub)tree
2.1704 + pos' : initialization (the last pos' before ...)
2.1705 + -> pos' list : of positions in this (sub) tree (relative to the root)
2.1706 +.*)
2.1707 +(*###################################################################*)
2.1708 +(* val (cuts, P, pt, pos) = ([], [3], get_nd pt [3], ([], Frm):pos');
2.1709 + val (cuts, P, pt, pos) = ([], [2], get_nd pt [2], ([], Frm):pos');
2.1710 + length (children pt);
2.1711 + *)
2.1712 +fun get_allp (cuts:pos' list) (P:pos, pos:pos') pt =
2.1713 + (let val nxt = move_dn [] pt pos (*exn if Incomplete reached*)
2.1714 + in if nxt <> ([],Res)
2.1715 + then get_allp (cuts @ [nxt]) (P, nxt) pt
2.1716 + else (map (apfst (curry op@ P)) (cuts @ [nxt])): pos' list
2.1717 + end) handle PTREE _ => (map (apfst (curry op@ P)) cuts);
2.1718 +(*###################################################################*)
2.1719 +
2.1720 +
2.1721 +
2.1722 +(*the pts are assumed to be on the same level*)
2.1723 +fun get_allps (cuts: pos' list) (P:pos) [] = cuts
2.1724 + | get_allps cuts P (pt::pts) =
2.1725 + let val below = get_allp [] (P, ([], Frm)) pt
2.1726 + val levfrm =
2.1727 + if is_pblnd pt
2.1728 + then (P, Pbl)::below
2.1729 + else if last_elem P = 1
2.1730 + then (P, Frm)::below
2.1731 + else (*Trans*) below
2.1732 + val levres = levfrm @ (if null below then [(P, Res)] else [])
2.1733 + in get_allps (cuts @ levres) (lev_on P) pts end;
2.1734 +
2.1735 +
2.1736 +
2.1737 +
2.1738 +(**.these 2 funs decide on how far cut_tree goes.**)
2.1739 +(*.shall the nodes _after_ the pos to be inserted at be deleted?.*)
2.1740 +fun test_trans (PrfObj{branch = Transitive,...}) = true
2.1741 + | test_trans (PrfObj{branch = NoBranch,...}) = true
2.1742 + | test_trans (PblObj{branch = Transitive,...}) = true
2.1743 + | test_trans (PblObj{branch = NoBranch,...}) = true
2.1744 + | test_trans _ = false;
2.1745 +(*.shall cutting be continued on the higher level(s)?
2.1746 + the Nd regarded will NOT be changed.*)
2.1747 +fun cutlevup (PblObj _) = false (*for tests of LK0502*)
2.1748 + | cutlevup _ = true;
2.1749 +
2.1750 +(*cut_bottom new S(603)..(608)
2.1751 +cut the level at the bottom of the pos (used by cappend_...)
2.1752 +and handle the parent in order to avoid extra case for root
2.1753 +fn: ptree -> : the _whole_ ptree for cut_levup
2.1754 + pos * posel -> : the pos after split_last
2.1755 + ptree -> : the parent of the Nd to be cut
2.1756 +return
2.1757 + (ptree * : the updated ptree
2.1758 + pos' list) * : the pos's cut
2.1759 + bool : cutting shall be continued on the higher level(s)
2.1760 +*)
2.1761 +print_depth 99;
2.1762 +fun cut_bottom _ (pt' as Nd (b, [])) = ((pt', []), cutlevup b)
2.1763 + | cut_bottom (P:pos, p:posel) (Nd (b, bs)) =
2.1764 + let (*divide level into 3 parts...*)
2.1765 + val keep = take (p - 1, bs)
2.1766 + val pt' as Nd (_,bs') = nth p bs
2.1767 + (*^^^^^_here_ will be 'insert'ed by 'append_..'*)
2.1768 + val (tail, tp) = (takerest (p, bs),
2.1769 + if null (takerest (p, bs)) then 0 else p + 1)
2.1770 + val (children, cuts) =
2.1771 + if test_trans b
2.1772 + then (keep,
2.1773 + (if is_pblnd pt' then [(P @ [p], Pbl)] else [])
2.1774 + @ (get_allp [] (P @ [p], (P, Frm)) pt')
2.1775 + @ (get_allps [] (P @ [p+1]) tail))
2.1776 + else (keep @ [(*'insert'ed by 'append_..'*)] @ tail,
2.1777 + get_allp [] (P @ [p], (P, Frm)) pt')
2.1778 + val (pt'', cuts) =
2.1779 + if cutlevup b
2.1780 + then (Nd (del_res b, children),
2.1781 + cuts @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
2.1782 + else (Nd (b, children), cuts)
2.1783 + (*val _= writeln("####cut_bottom (P, p)="^pos2str (P @ [p])^
2.1784 + ", Nd=.............................................")
2.1785 + val _= show_pt pt''
2.1786 + val _= writeln("####cut_bottom form='"^
2.1787 + term2str (get_obj g_form pt'' []))
2.1788 + val _= writeln("####cut_bottom cuts#="^string_of_int (length cuts)^
2.1789 + ", cuts="^pos's2str cuts)*)
2.1790 + in ((pt'', cuts:pos' list), cutlevup b) end;
2.1791 +print_depth 3;
2.1792 +(**######################################################################**);
2.1793 +(*.go all levels from the bottom of 'pos' up to the root,
2.1794 + on each level compose the children of a node and accumulate the cut Nds
2.1795 +args
2.1796 + pos' list -> : for accumulation
2.1797 + bool -> : cutting shall be continued on the higher level(s)
2.1798 + ptree -> : the whole ptree for 'get_nd pt P' on each level
2.1799 + ptree -> : the Nd from the lower level for insertion at path
2.1800 + pos * posel -> : pos=path split for convenience
2.1801 + ptree -> : Nd the children of are under consideration on this call
2.1802 +returns :
2.1803 + ptree * pos' list : the updated parent-Nd and the pos's of the Nds cut
2.1804 +.*)
2.1805 +print_depth 99;
2.1806 +fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:posel) (Nd (b, bs)) =
2.1807 + let (*divide level into 3 parts...*)
2.1808 + val keep = take (p - 1, bs)
2.1809 + (*val pt' comes as argument from below*)
2.1810 + val (tail, tp) = (takerest (p, bs),
2.1811 + if null (takerest (p, bs)) then 0 else p + 1)
2.1812 + val (children, cuts') =
2.1813 + if clevup
2.1814 + then (keep @ [pt'], get_allps [] (P @ [p+1]) tail)
2.1815 + else (keep @ [pt'] @ tail, [])
2.1816 + val clevup' = if clevup then cutlevup b else false
2.1817 + (*the first Nd with false stops cutting on all levels above*)
2.1818 + val (pt'', cuts') =
2.1819 + if clevup'
2.1820 + then (Nd (del_res b, children),
2.1821 + cuts' @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
2.1822 + else (Nd (b, children), cuts')
2.1823 + (*val _= writeln("#####cut_levup clevup= "^bool2str clevup)
2.1824 + val _= writeln("#####cut_levup cutlevup b= "^bool2str (cutlevup b))
2.1825 + val _= writeln("#####cut_levup (P, p)="^pos2str (P @ [p])^
2.1826 + ", Nd=.............................................")
2.1827 + val _= show_pt pt''
2.1828 + val _= writeln("#####cut_levup form='"^
2.1829 + term2str (get_obj g_form pt'' []))
2.1830 + val _= writeln("#####cut_levup cuts#="^string_of_int (length cuts)^
2.1831 + ", cuts="^pos's2str cuts)*)
2.1832 + in if null P then (pt'', (cuts @ cuts'):pos' list)
2.1833 + else let val (P, p) = split_last P
2.1834 + in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P)
2.1835 + end
2.1836 + end;
2.1837 +print_depth 3;
2.1838 +(**######################################################################**);
2.1839 +print_depth 99;
2.1840 +fun cut_tree pt (pos,_) =
2.1841 + if not (existpt pos pt)
2.1842 + then (pt,[]) (*appending a formula never cuts anything*)
2.1843 + else let val (P, p) = split_last pos
2.1844 + val ((pt', cuts), clevup) = cut_bottom (P, p) (get_nd pt P)
2.1845 + (* pt' is the updated parent of the Nd to cappend_..*)
2.1846 + in if null P then (pt', cuts)
2.1847 + else let val (P, p) = split_last P
2.1848 + in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P)
2.1849 + end
2.1850 + end;
2.1851 +print_depth 3;
2.1852 +
2.1853 +
2.1854 +
2.1855 +(*######## eval from here ##########################################**)
2.1856 +(*######## eval from here ##########################################**)
2.1857 +(*######## eval from here ##########################################**)
2.1858 +
2.1859 +fun append_atomic p l f r f' s pt =
2.1860 + let (*val _= writeln("##append_atomic: pos ="^pos2str p^
2.1861 + ", Nd=.............................................")
2.1862 + val _= show_pt pt*)
2.1863 + val (iss, f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
2.1864 + then (*after Take*)
2.1865 + ((fst (get_obj g_loc pt p), Some l),
2.1866 + get_obj g_form pt p)
2.1867 + (*040223 else ((Some l, None), f)*)
2.1868 + else ((None, Some l), f)
2.1869 + in insert (PrfObj {cell = [(*3.00. unused*)],
2.1870 + form = f,
2.1871 + tac = r,
2.1872 + loc = iss,
2.1873 + branch= NoBranch,
2.1874 + result= f',
2.1875 + ostate= s}) pt p end;
2.1876 +
2.1877 +(*20.8.02: cappend_* FIXXXXME cut branches below cannot be decided here:
2.1878 + detail - generate - cappend: inserted, not appended !!!
2.1879 +
2.1880 + cut decided in applicable_in !?!
2.1881 +*)
2.1882 +fun cappend_atomic pt p loc f r f' s =
2.1883 + let val _= writeln("#cappend_atomic: pos ="^pos2str p)
2.1884 + val (pt',c) = cut_tree pt (p,Frm)
2.1885 + val _= writeln("#cappend_atomic: after cut")
2.1886 + val pt'' = append_atomic p loc f r f' s pt'
2.1887 + in (pt'',c) end;
2.1888 +fun cappend_atomic pt p loc f r f' s =
2.1889 +(* val (pt, p, loc, f, r, f', s) =
2.1890 + (pt,p,l,f,Rewrite_Set_Inst (subst2subs subs',id_rls rls'),
2.1891 + (f',asm),Complete);
2.1892 + *)
2.1893 +((*writeln("###cappend_atomic: pos ="^pos2str p);*)
2.1894 + apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm))
2.1895 +);
2.1896 +
2.1897 +(* called by Take *)
2.1898 +fun append_form p l f pt =
2.1899 +((*writeln("###append_form: pos ="^pos2str p);*)
2.1900 + insert (PrfObj {cell = [(*3.00. unused*)],
2.1901 + form = (*if existpt p pt
2.1902 + andalso get_obj g_tac pt p = Empty_Tac
2.1903 + (*distinction from 'old' (+complete!) pobjs*)
2.1904 + then get_obj g_form pt p else*) f,
2.1905 + tac = Empty_Tac,
2.1906 + loc = (Some l, None),
2.1907 + branch= NoBranch,
2.1908 + result= (e_term,[]),
2.1909 + ostate= Incomplete}) pt p
2.1910 +);
2.1911 +(* val (p,loc,f) = ([1], e_istate, str2term "x + 1 = 2");
2.1912 + val (p,loc,f) = (fst p, e_istate, str2term "-1 + x = 0");
2.1913 + *)
2.1914 +fun cappend_form pt p loc f =
2.1915 +((*writeln("###cappend_form: pos ="^pos2str p);*)
2.1916 + apfst (append_form p loc f) (cut_tree pt (p,Frm))
2.1917 +);
2.1918 +
2.1919 +
2.1920 +
2.1921 +fun append_result pt p l f s =
2.1922 +((*writeln("###append_result: pos ="^pos2str p);*)
2.1923 + (appl_obj (repl_result (fst (get_obj g_loc pt p),
2.1924 + Some l) f s) pt p, [])
2.1925 +);
2.1926 +
2.1927 +
2.1928 +(*WN041022 deprecated, still for kbtest/diffapp.sml, /systest/root-equ.sml*)
2.1929 +fun append_parent p l f r b pt =
2.1930 + let (*val _= writeln("###append_parent: pos ="^pos2str p);*)
2.1931 + val (ll,f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
2.1932 + then ((fst (get_obj g_loc pt p), Some l),
2.1933 + get_obj g_form pt p)
2.1934 + else ((Some l, None), f)
2.1935 + in insert (PrfObj
2.1936 + {cell = [(*unused*)],
2.1937 + form = f,
2.1938 + tac = r,
2.1939 + loc = ll,
2.1940 + branch= b,
2.1941 + result= (e_term,[]),
2.1942 + ostate= Incomplete}) pt p end;
2.1943 +fun cappend_parent pt p loc f r b =
2.1944 +((*writeln("###cappend_parent: pos ="^pos2str p);*)
2.1945 + apfst (append_parent p loc f r b) (cut_tree pt (p,Und))
2.1946 +);
2.1947 +
2.1948 +
2.1949 +fun append_problem [] l fmz (strs,spec,hdf) _ =
2.1950 +((*writeln("###append_problem: pos = []");*)
2.1951 + (Nd (PblObj
2.1952 + {cell = [(*3.00. unused*)],
2.1953 + origin= (strs,spec,hdf),
2.1954 + fmz = fmz,
2.1955 + spec = empty_spec,
2.1956 + probl = []:itm list,
2.1957 + meth = []:itm list,
2.1958 + env = None,
2.1959 + loc = (Some l, None),
2.1960 + branch= TransitiveB,(*FIXXXXXME.27.8.03: for equations only*)
2.1961 + result= (e_term,[]),
2.1962 + ostate= Incomplete},[]))
2.1963 +)
2.1964 + | append_problem p l fmz (strs,spec,hdf) pt =
2.1965 +((*writeln("###append_problem: pos ="^pos2str p);*)
2.1966 + insert (PblObj
2.1967 + {cell = [(*3.00. unused*)],
2.1968 + origin= (strs,spec,hdf),
2.1969 + fmz = fmz,
2.1970 + spec = empty_spec,
2.1971 + probl = []:itm list,
2.1972 + meth = []:itm list,
2.1973 + env = None,
2.1974 + loc = (Some l, None),
2.1975 + branch= TransitiveB,
2.1976 + result= (e_term,[]),
2.1977 + ostate= Incomplete}) pt p
2.1978 +);
2.1979 +fun cappend_problem _ [] loc fmz ori =
2.1980 +((*writeln("###cappend_problem: pos = []");*)
2.1981 + (append_problem [] loc fmz ori EmptyPtree,[])
2.1982 +)
2.1983 + | cappend_problem pt p loc fmz ori =
2.1984 +((*writeln("###cappend_problem: pos ="^pos2str p);*)
2.1985 + apfst (append_problem p (loc:istate) fmz ori) (cut_tree pt (p,Frm))
2.1986 +);
2.1987 +