1.1 --- a/src/Tools/isac/Interpret/ctree.sml Tue Sep 17 11:22:53 2013 +0200
1.2 +++ b/src/Tools/isac/Interpret/ctree.sml Tue Sep 17 18:00:59 2013 +0200
1.3 @@ -1053,30 +1053,30 @@
1.4
1.5 (*.insert obj b into ptree at pos, ev.overwriting this pos.
1.6 covers library.ML TODO.WN110315 rename*)
1.7 -fun insert b EmptyPtree ([]:pos) = Nd (b, [])
1.8 - | insert b EmptyPtree _ = raise PTREE "insert b Empty _"
1.9 - | insert b (Nd ( _, _)) [] = raise PTREE "insert b _ []"
1.10 - | insert b (Nd (b', bs)) (p::[]) =
1.11 +fun insert_pt b EmptyPtree ([]:pos) = Nd (b, [])
1.12 + | insert_pt b EmptyPtree _ = raise PTREE "insert_pt b Empty _"
1.13 + | insert_pt b (Nd ( _, _)) [] = raise PTREE "insert_pt b _ []"
1.14 + | insert_pt b (Nd (b', bs)) (p::[]) =
1.15 Nd (b', repl_app bs p (Nd (b,[])))
1.16 - | insert b (Nd (b', bs)) (p::ps) =
1.17 - Nd (b', repl_app bs p (insert b (nth p bs) ps));
1.18 + | insert_pt b (Nd (b', bs)) (p::ps) =
1.19 + Nd (b', repl_app bs p (insert_pt b (nth p bs) ps));
1.20 (*
1.21 > type ppobj = string;
1.22 > tracing (pr_ptree prfn (!pt));
1.23 val pt = Unsynchronized.ref Empty;
1.24 - pt:= insert ("root'":ppobj) EmptyPtree [];
1.25 - pt:= insert ("xx1":ppobj) (!pt) [1];
1.26 - pt:= insert ("xx2":ppobj) (!pt) [2];
1.27 - pt:= insert ("xx3":ppobj) (!pt) [3];
1.28 - pt:= insert ("xx2.1":ppobj) (!pt) [2,1];
1.29 - pt:= insert ("xx2.2":ppobj) (!pt) [2,2];
1.30 - pt:= insert ("xx2.1.1":ppobj) (!pt) [2,1,1];
1.31 - pt:= insert ("xx2.1.2":ppobj) (!pt) [2,1,2];
1.32 - pt:= insert ("xx2.1.3":ppobj) (!pt) [2,1,3];
1.33 + pt:= insert_pt ("root'":ppobj) EmptyPtree [];
1.34 + pt:= insert_pt ("xx1":ppobj) (!pt) [1];
1.35 + pt:= insert_pt ("xx2":ppobj) (!pt) [2];
1.36 + pt:= insert_pt ("xx3":ppobj) (!pt) [3];
1.37 + pt:= insert_pt ("xx2.1":ppobj) (!pt) [2,1];
1.38 + pt:= insert_pt ("xx2.2":ppobj) (!pt) [2,2];
1.39 + pt:= insert_pt ("xx2.1.1":ppobj) (!pt) [2,1,1];
1.40 + pt:= insert_pt ("xx2.1.2":ppobj) (!pt) [2,1,2];
1.41 + pt:= insert_pt ("xx2.1.3":ppobj) (!pt) [2,1,3];
1.42 *)
1.43
1.44 (*.insert children to a node without children.*)
1.45 -(*compare: fun insert*)
1.46 +(*compare: fun insert_pt*)
1.47 fun ins_chn _ EmptyPtree (_:pos) = raise PTREE "ins_chn: EmptyPtree"
1.48 | ins_chn ns (Nd _) [] = raise PTREE "ins_chn: pos = []"
1.49 | ins_chn ns (Nd (b, bs)) (p::[]) =
1.50 @@ -1087,7 +1087,7 @@
1.51 | ins_chn ns (Nd (b, bs)) (p::ps) =
1.52 Nd (b, repl_app bs p (ins_chn ns (nth p bs) ps));
1.53
1.54 -(* print_depth 11;ins_chn;print_depth 3; ###insert#########################*);
1.55 +(* print_depth 11;ins_chn;print_depth 3; ###insert_pt#########################*);
1.56
1.57
1.58 (** apply f to obj at pos, f: ppobj -> ppobj **)
1.59 @@ -1835,7 +1835,7 @@
1.60 let (*divide level into 3 parts...*)
1.61 val keep = take (p - 1, bs)
1.62 val pt' as Nd (_,bs') = nth p bs
1.63 - (*^^^^^_here_ will be 'insert'ed by 'append_..'*)
1.64 + (*^^^^^_here_ will be 'insert_pt'ed by 'append_..'*)
1.65 val (tail, tp) = (takerest (p, bs),
1.66 if null (takerest (p, bs)) then 0 else p + 1)
1.67 val (children, cuts) =
1.68 @@ -1844,7 +1844,7 @@
1.69 (if is_pblnd pt' then [(P @ [p], Pbl)] else [])
1.70 @ (get_allp [] (P @ [p], (P, Frm)) pt')
1.71 @ (get_allps [] (P @ [p+1]) tail))
1.72 - else (keep @ [(*'insert'ed by 'append_..'*)] @ tail,
1.73 + else (keep @ [(*'insert_pt'ed by 'append_..'*)] @ tail,
1.74 get_allp [] (P @ [p], (P, Frm)) pt')
1.75 val (pt'', cuts) =
1.76 if cutlevup b
1.77 @@ -1926,7 +1926,7 @@
1.78 ((fst (get_obj g_loc pt p), SOME l),
1.79 get_obj g_form pt p)
1.80 else ((NONE, SOME l), f)
1.81 - in insert (PrfObj {cell = NONE,
1.82 + in insert_pt (PrfObj {cell = NONE,
1.83 form = f,
1.84 tac = r,
1.85 loc = iss,
1.86 @@ -1964,7 +1964,7 @@
1.87 (* called by Take *)
1.88 fun append_form p l f pt =
1.89 ((*tracing("##@append_form: pos ="^pos2str p);*)
1.90 - insert (PrfObj {cell = NONE,
1.91 + insert_pt (PrfObj {cell = NONE,
1.92 form = (*if existpt p pt
1.93 andalso get_obj g_tac pt p = Empty_Tac
1.94 (*distinction from 'old' (+complete!) pobjs*)
1.95 @@ -2007,7 +2007,7 @@
1.96 then ((fst (get_obj g_loc pt p), SOME l),
1.97 get_obj g_form pt p)
1.98 else ((SOME l, NONE), f)
1.99 - in insert (PrfObj
1.100 + in insert_pt (PrfObj
1.101 {cell = NONE,
1.102 form = f,
1.103 tac = r,
1.104 @@ -2039,7 +2039,7 @@
1.105 )
1.106 | append_problem p l fmz (strs,spec,hdf) pt =
1.107 ((*tracing("###append_problem: pos ="^pos2str p);*)
1.108 - insert (PblObj
1.109 + insert_pt (PblObj
1.110 {cell = NONE,
1.111 origin= (strs,spec,hdf),
1.112 fmz = fmz,