1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/ME/ctreeNEW.sml Mon Feb 21 19:02:39 2005 +0100
1.3 @@ -0,0 +1,146 @@
1.4 +(* use"ME/ctreeNEW.sml";
1.5 + use"ctreeNEW.sml";
1.6 + *)
1.7 +
1.8 +
1.9 +
1.10 +(*drop first element and make run on []*)
1.11 +fun get_tlpos' p pt =
1.12 + let val ps = get_allpos' p pt
1.13 + in if null ps then ps else tl ps end;
1.14 +fun get_tlpos's p pts =
1.15 + let val ps = get_allpos's p pts
1.16 + in if null ps then ps else tl ps end;
1.17 +
1.18 +(*---OLD---*)
1.19 +fun get_allp (cuts: pos' list) (P:pos) pt ((p, p_): pos') =
1.20 + (let val nxt = move_dn P pt (drop (length P, p), p_)
1.21 + (*exn if Incomplete reached*)
1.22 + in if nxt <> ([],Res)
1.23 + then get_allp (cuts @ [nxt]) P pt nxt
1.24 + else (cuts @ [nxt]): pos' list
1.25 + end) handle PTREE _ => cuts;
1.26 +(*.get all positions in a ptree until ([],Res) or ostate=Incomplete
1.27 +val get_allp = fn :
1.28 + pos' list -> : accumulated, start with []
1.29 + pos -> : the offset for subtrees wrt the root
1.30 + ptree -> : (sub)tree
1.31 + pos' : before the positions in ...
1.32 + -> pos' list : of positions in this (sub) tree (relative to the root)
1.33 +.*)
1.34 +print_depth 11;
1.35 +(* val (cuts, P, pt, pos) = ([], [3], get_nd pt [3], ([]:int list,Frm));
1.36 + *)
1.37 +(*----OLD-----*)
1.38 +fun get_allp (cuts: pos' list) (P:pos) pt (pos:pos') =
1.39 + (let val nxt = move_dn P pt pos
1.40 + (*exn if Incomplete reached*)
1.41 + in if nxt <> ([],Res)
1.42 + then get_allp (cuts @ [nxt]) P pt nxt
1.43 + else (cuts @ [nxt]): pos' list
1.44 + end) handle PTREE _ => cuts;
1.45 +print_depth 3;
1.46 +print_depth 11;
1.47 +(* val (cuts, P, pt, pos) = ([], [3], get_nd pt [3], ([], Frm):pos');
1.48 + val (cuts, P, pt, pos) = ([], [2], get_nd pt [2], ([], Frm):pos');
1.49 + length (children pt);
1.50 + *)
1.51 +fun get_allp (cuts:pos' list) (P:pos) pt (pos:pos') =
1.52 + (let val nxt = move_dn [] pt pos (*exn if Incomplete reached*)
1.53 + in if nxt <> ([],Res)
1.54 + then get_allp (cuts @ [nxt]) P pt nxt
1.55 + else (map (apfst (curry op@ P)) (cuts @ [nxt])): pos' list
1.56 + end) handle PTREE _ => (map (apfst (curry op@ P)) cuts);
1.57 +print_depth 3;
1.58 +
1.59 +
1.60 +
1.61 +(*----OLD-----*)
1.62 +print_depth 11;
1.63 +(*the pts are assumed to be on the same level*)
1.64 +fun get_allps (cuts: pos' list) (P:pos) (pt::pts) =
1.65 + let val cuts' = get_allp [] P pt ([], Frm)
1.66 + val nxt = last_elem cuts'
1.67 + in if nxt <> ([],Res)
1.68 + then get_allps (cuts @ cuts') P pts
1.69 + else cuts @ cuts'
1.70 + end;
1.71 +print_depth 3;
1.72 +(* use"ME/ctreeNEW.sml";
1.73 + use"ctreeNEW.sml";
1.74 + *)
1.75 +print_depth 11;
1.76 +(* val (cuts: pos' list, P, pt::pts) = ([], [1], children pt);
1.77 + val cuts' = get_allp [] P pt ([], Frm);
1.78 + val (cuts: pos' list, P, pt::pts) = (cuts @ cuts', lev_on P, pts);
1.79 + val cuts' = get_allp [] P pt ([], Frm);
1.80 + length (children pt);
1.81 + *)
1.82 +(*the pts are assumed to be on the same level*)
1.83 +fun get_allps (cuts: pos' list) (P:pos) (pt::pts) =
1.84 + let val cuts' = get_allp [] P pt ([], Frm)
1.85 + in get_allps (cuts @ cuts') (lev_on P) pts end;
1.86 +print_depth 3;
1.87 +
1.88 +
1.89 +fun del_res (PblObj {cell, fmz, origin, spec, probl, meth,
1.90 + env, loc=(l1,_), branch, result, ostate}) =
1.91 + PblObj {cell=cell,fmz=fmz,origin=origin,spec=spec,probl=probl,meth=meth,
1.92 + env=env, loc=(l1,None), branch=branch, result=(e_term,[]),
1.93 + ostate=Incomplete}
1.94 +
1.95 + | del_res (PrfObj {cell, form, tac, loc=(l1,_), branch, result, ostate}) =
1.96 + PrfObj {cell=cell,form=form,tac=tac, loc=(l1,None), branch=branch,
1.97 + result=(e_term,[]), ostate=Incomplete};
1.98 +
1.99 +
1.100 +print_depth 11; move_dn; print_depth 3;
1.101 +print_depth 11; get_allpos'; print_depth 3;
1.102 +
1.103 +
1.104 +(* for cut_level; appl_branch(deprecated) *)
1.105 +(*WN050221: applied wrt a single Nd, _not_ for a level of children*)
1.106 +fun test_trans (PrfObj{branch = Transitive,...}) = true
1.107 + | test_trans (PrfObj{branch = NoBranch,...}) = true
1.108 + (*| test_trans (PblObj{branch = NoBranch,...}) = true
1.109 + WN050221 for test on worksheet*)
1.110 + | test_trans _ = false;
1.111 +
1.112 +(*WN050220: new design S(603)..(608)
1.113 +p_ is not required !!!*)
1.114 +
1.115 +(* val (cuts, P, pt as Nd (b,bs), (p::[])) = ([], [], pt, pos);
1.116 + val (cuts, P, pt as Nd (b,bs), (p::[])) = ([], [], pt, [2]);
1.117 + *)
1.118 +fun cut_tre cuts P (Nd (b, bs)) (p::[]) =
1.119 + let (*top down divide each level into 3 parts...*)
1.120 + val keep = take (p - 1, bs)
1.121 + val Nd (b',bs') = nth p bs(*here* will be 'insert'ed by 'append_..'*)
1.122 + val tail = takerest (p, bs)
1.123 + in if test_trans b'
1.124 + then (Nd (del_res b(*...and handle parent*), keep(*here at end*)),
1.125 + cuts
1.126 + @ (get_allpos's (P @ [p], 1) bs')
1.127 + @ (get_allpos's (P, p + 1) tail)
1.128 + @ (if g_ostate b = Incomplete then [(P,Res)] else []))
1.129 +
1.130 + else (Nd (b, keep @ [(*Nd (b',bs') 'insert'ed*)] @ tail),
1.131 + cuts
1.132 + @ (get_allpos's (P @ [p], 1) bs'))
1.133 + end
1.134 + | cut_tre cuts P (pt as Nd (b,bs)) (p::ps) = (pt,[])
1.135 +;
1.136 +(*
1.137 + let (*top down divide each level into 3 parts...*)
1.138 + val keep = take (p - 1, bs)
1.139 + val (pt' as (Nd (b',_)), cuts') = cut_tre cuts (P@[p]) (nth p bs) ps
1.140 + val tail = takerest (p, bs)
1.141 + in if test_trans b'
1.142 + then (Nd ((*if P=[]...del_res*)b,
1.143 + keep @ [delete_result pt' []]),
1.144 + cuts @ cuts' @ ([(*Res pt'?*)]) @ (get_allpos's tail))
1.145 + else (Nd (b, keep @ [pt'] @ tail),
1.146 + cuts @ cuts' @ ([(*Res pt'*)]))
1.147 + end
1.148 +*)
1.149 +fun cut_tree pt (p,_) = cut_tre [] [] pt pos;