1 (* Title: read and write access to the calctree
2 Author: Walther Neuper 2017
3 (c) due to copyright terms
5 signature CALC_TREE_ACCESS =
8 val update_branch : CTbasic.ctree -> CTbasic.pos -> CTbasic.branch -> CTbasic.ctree
9 val update_ctxt : CTbasic.ctree -> CTbasic.pos -> Proof.context -> CTbasic.ctree
10 val update_env : CTbasic.ctree -> CTbasic.pos -> (Selem.istate * Proof.context) option -> CTbasic.ctree
11 val update_domID : CTbasic.ctree -> CTbasic.pos -> domID -> CTbasic.ctree
12 val update_met : CTbasic.ctree -> CTbasic.pos -> itm list -> CTbasic.ctree (* =vvv= ? *)
13 val update_metppc : CTbasic.ctree -> CTbasic.pos -> itm list -> CTbasic.ctree (* =^^^= ? *)
14 val update_metID : CTbasic.ctree -> CTbasic.pos -> metID -> CTbasic.ctree
15 val update_pbl : CTbasic.ctree -> CTbasic.pos -> itm list -> CTbasic.ctree (* =vvv= ? *)
16 val update_pblppc : CTbasic.ctree -> CTbasic.pos -> itm list -> CTbasic.ctree (* =^^^= ? *)
17 val update_pblID : CTbasic.ctree -> CTbasic.pos -> pblID -> CTbasic.ctree
18 val update_oris : CTbasic.ctree -> CTbasic.pos -> ori list -> CTbasic.ctree
19 val update_orispec : CTbasic.ctree -> CTbasic.pos -> spec -> CTbasic.ctree
20 val update_spec : CTbasic.ctree -> CTbasic.pos -> spec -> CTbasic.ctree
21 val update_tac : CTbasic.ctree -> CTbasic.pos -> CTbasic.tac -> CTbasic.ctree
23 val cappend_form : CTbasic.ctree -> CTbasic.pos -> Selem.istate * Proof.context -> term ->
24 CTbasic.ctree * CTbasic.pos' list
25 val cappend_problem : CTbasic.ctree -> CTbasic.pos -> Selem.istate * Proof.context ->
26 Selem.fmz -> ori list * spec * term -> CTbasic.ctree * CTbasic.pos' list
27 val append_result : CTbasic.ctree -> CTbasic.pos -> Selem.istate * Proof.context ->
28 Selem.result -> CTbasic.ostate -> CTbasic.ctree * 'a list
29 val append_atomic : (* for solve.sml *)
30 CTbasic.pos -> Selem.istate * Proof.context -> term -> CTbasic.tac -> Selem.result ->
31 CTbasic.ostate -> CTbasic.ctree -> CTbasic.ctree
32 val cappend_atomic : CTbasic.ctree -> CTbasic.pos -> Selem.istate * Proof.context -> term ->
33 CTbasic.tac -> Selem.result -> CTbasic.ostate -> CTbasic.ctree * CTbasic.pos' list
34 (* ---- for tests only: made visible in order to remove the warning --------------------------- *)
35 val cappend_parent : CTbasic.ctree -> int list -> Selem.istate * Proof.context -> term ->
36 CTbasic.tac -> CTbasic.branch -> CTbasic.ctree * CTbasic.pos' list
37 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
38 val update_loc' : CTbasic.ctree -> CTbasic.pos ->
39 (Selem.istate * Proof.context) option * (Selem.istate * Proof.context) option -> CTbasic.ctree
40 val append_problem : int list -> Selem.istate * Proof.context -> Selem.fmz ->
41 ori list * spec * term -> CTbasic.ctree -> CTbasic.ctree
42 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
45 structure CTaccess(**): CALC_TREE_ACCESS(**) =
50 (* for use by appl_obj *)
51 fun repl_pbl x (PblObj {cell, origin, fmz, spec, probl = _, meth, ctxt, env, loc,
52 branch, result, ostate}) =
53 PblObj {cell = cell, origin = origin, fmz = fmz, spec = spec, probl= x, meth = meth,
54 ctxt = ctxt, env = env, loc = loc, branch = branch, result = result, ostate = ostate}
55 | repl_pbl _ _ = raise PTREE "repl_pbl takes no PrfObj";
56 fun repl_met x (PblObj {cell, origin, fmz, spec, probl, meth = _, ctxt, env, loc,
57 branch, result, ostate}) =
58 PblObj {cell = cell, origin = origin, fmz= fmz, spec = spec, probl = probl,
59 meth = x, ctxt = ctxt, env = env, loc = loc, branch = branch, result = result,
61 | repl_met _ _ = raise PTREE "repl_pbl takes no PrfObj";
62 fun repl_spec x (PblObj {cell, origin, fmz, spec = _, probl, meth, ctxt, env, loc,
63 branch, result, ostate}) =
64 PblObj {cell = cell, origin = origin, fmz = fmz, spec = x, probl = probl,
65 meth = meth, ctxt = ctxt, env = env, loc = loc, branch = branch, result = result,
67 | repl_spec _ _ = raise PTREE "repl_domID takes no PrfObj";
68 fun repl_domID x (PblObj {cell, origin, fmz, spec = (_, p, m), probl, meth, ctxt, env, loc,
69 branch, result, ostate}) =
70 PblObj {cell = cell, origin = origin, fmz = fmz, spec= (x, p, m), probl = probl,
71 meth = meth, ctxt = ctxt, env = env, loc = loc, branch = branch, result = result,
73 | repl_domID _ _ = raise PTREE "repl_domID takes no PrfObj";
74 fun repl_pblID x (PblObj {cell, origin, fmz, spec= (d, _, m), probl, meth, ctxt, env, loc,
75 branch, result, ostate}) =
76 PblObj {cell = cell, origin = origin, fmz = fmz, spec= (d, x, m), probl = probl,
77 meth = meth, ctxt = ctxt, env = env, loc = loc, branch = branch, result = result,
79 | repl_pblID _ _ = raise PTREE "repl_pblID takes no PrfObj";
80 fun repl_metID x (PblObj {cell, origin, fmz, spec = (d, p,_), probl, meth, ctxt, env, loc,
81 branch, result, ostate}) =
82 PblObj {cell = cell, origin = origin, fmz = fmz, spec = (d, p, x), probl = probl,
83 meth = meth, ctxt = ctxt, env = env, loc = loc, branch = branch, result = result,
85 | repl_metID _ _ = raise PTREE "repl_metID takes no PrfObj";
86 fun repl_result l f' s (PrfObj {cell, form, tac, loc = _, branch, result = _ , ostate = _}) =
87 PrfObj {cell = cell, form = form, tac = tac, loc = l, branch = branch, result = f', ostate = s}
88 | repl_result l f' s (PblObj {cell, origin, fmz, spec, probl, meth, ctxt, env, loc = _,
89 branch, result = _ , ostate= _}) =
90 PblObj {cell = cell, origin = origin, fmz= fmz, spec = spec, probl = probl,
91 meth = meth, ctxt = ctxt, env = env, loc = l, branch = branch, result = f', ostate = s};
92 fun repl_tac x (PrfObj {cell, form, tac = _, loc, branch, result, ostate}) =
93 PrfObj {cell = cell, form = form, tac = x, loc = loc, branch = branch,
94 result = result, ostate = ostate}
95 | repl_tac _ _ = raise PTREE "repl_tac takes no PblObj";
96 fun repl_ctxt x (PblObj {cell, origin, fmz, spec, probl, meth,
97 ctxt = _, env, loc, branch, result, ostate}) =
98 PblObj {cell = cell, origin = origin, fmz = fmz, spec = spec, probl = probl,
99 meth = meth, ctxt = x, env = env, loc = loc, branch = branch, result = result,
101 | repl_ctxt _ _ = raise PTREE "repl_env takes no PrfObj";
102 fun repl_env e (PblObj {cell, origin, fmz, spec, probl, meth,
103 ctxt, env = _, loc, branch, result, ostate}) =
104 PblObj {cell = cell, origin = origin, fmz = fmz, spec = spec, probl = probl,
105 meth = meth, ctxt = ctxt, env = e, loc = loc, branch = branch, result = result,
107 | repl_env _ _ = raise PTREE "repl_env takes no PrfObj";
108 fun repl_oris oris (PblObj { cell, origin = (_, spe, hdf),fmz, spec, probl, meth,
109 ctxt, env, loc, branch, result, ostate}) =
110 PblObj{cell = cell, origin = (oris, spe, hdf), fmz = fmz, spec = spec, probl = probl,
111 meth = meth, ctxt = ctxt, env = env, loc = loc, branch = branch, result = result,
113 | repl_oris _ _ = raise PTREE "repl_oris takes no PrfObj";
114 fun repl_orispec spe (PblObj {cell, origin = (oris, _, hdf), fmz, spec, probl, meth,
115 ctxt, env, loc, branch, result, ostate}) =
116 PblObj{cell = cell, origin = (oris, spe, hdf), fmz = fmz, spec = spec, probl = probl,
117 meth = meth, ctxt = ctxt, env = env, loc = loc, branch = branch, result = result,
119 | repl_orispec _ _ = raise PTREE "repl_orispec takes no PrfObj";
120 fun repl_loc l (PblObj {cell, origin, fmz, spec, probl, meth,
121 ctxt, env, loc = _ , branch, result, ostate}) =
122 PblObj {cell = cell, origin = origin, fmz = fmz, spec = spec, probl = probl,
123 meth = meth, ctxt = ctxt, env = env, loc = l, branch = branch, result = result,
125 | repl_loc l (PrfObj {cell, form, tac, loc = _, branch, result, ostate}) =
126 PrfObj {cell = cell, form = form, tac = tac, loc= l, branch = branch, result = result,
130 fun repl_branch b (PblObj {cell, origin, fmz, spec, probl, meth, ctxt, env, loc, branch = _,
132 PblObj {cell = cell, origin = origin, fmz = fmz, spec = spec, probl = probl,
133 meth = meth, ctxt = ctxt, env = env, loc = loc, branch = b, result = result,
135 | repl_branch b (PrfObj {cell, form, tac, loc, branch = _, result, ostate}) =
136 PrfObj {cell = cell, form = form, tac = tac, loc = loc, branch = b,
137 result = result, ostate = ostate};
139 fun update_branch pt pos x = appl_obj (repl_branch x) pt pos;
140 fun update_ctxt pt pos x = appl_obj (repl_ctxt x) pt pos; (* for use on PblObj,
141 otherwise use fun generate1; compare fun get_ctxt*)
142 fun update_env pt pos x = appl_obj (repl_env x) pt pos;
143 fun update_domID pt pos x = appl_obj (repl_domID x) pt pos;
144 fun update_met pt pos x = appl_obj (repl_met x) pt pos;
145 fun update_metppc pt pos x = appl_obj (repl_met x) pt pos;
146 fun update_metID pt pos x = appl_obj (repl_metID x) pt pos;
147 fun update_pbl pt pos x = appl_obj (repl_pbl x) pt pos;
148 fun update_pblppc pt pos x = appl_obj (repl_pbl x) pt pos;
149 fun update_pblID pt pos x = appl_obj (repl_pblID x) pt pos;
150 fun update_oris pt pos x = appl_obj (repl_oris x) pt pos;
151 fun update_orispec pt pos x = appl_obj (repl_orispec x) pt pos;
152 fun update_spec pt pos x = appl_obj (repl_spec x) pt pos;
153 fun update_tac pt pos x = appl_obj (repl_tac x) pt pos;
155 fun update_loc' pt pos x = appl_obj (repl_loc x) pt pos;
158 fun append_form p l f pt =
159 insert_pt (PrfObj {cell = NONE, form = f, tac = Empty_Tac, loc = (SOME l, NONE),
160 branch = NoBranch, result = (e_term, []), ostate = Incomplete}) pt p;
161 fun cappend_form pt p loc f =
163 val (pt', cs) = cut_tree pt (p, Frm)
164 val pt'' = append_form p loc f pt'
167 fun append_problem [] l fmz (strs, spec, hdf) _ =
168 (Nd (PblObj {cell = NONE, origin = (strs, spec, hdf), fmz = fmz, spec = empty_spec,
169 probl = [], meth = [], ctxt = Selem.e_ctxt, env = NONE, loc = (SOME l, NONE),
170 branch = TransitiveB, result = (e_term, []), ostate = Incomplete}, []))
171 | append_problem p l fmz (strs, spec, hdf) pt =
172 insert_pt (PblObj {cell = NONE, origin = (strs, spec, hdf), fmz = fmz, spec = empty_spec,
173 probl = [], meth = [], ctxt = Selem.e_ctxt, env = NONE, loc = (SOME l, NONE),
174 branch = TransitiveB, result = (e_term, []), ostate= Incomplete}) pt p;
175 fun cappend_problem _ [] loc fmz ori = (append_problem [] loc fmz ori EmptyPtree, [])
176 | cappend_problem pt p loc fmz ori =
177 apfst (append_problem p loc fmz ori) (cut_tree pt (p, Frm));
179 (*WN041022 deprecated, still for kbtest/diffapp.sml, /systest/root-equ.sml*)
180 fun append_parent p l f r b pt =
183 if existpt p pt andalso is_empty_tac (get_obj g_tac pt p)
184 then ((fst (get_obj g_loc pt p), SOME l), get_obj g_form pt p)
185 else ((SOME l, NONE), f)
186 in insert_pt (PrfObj {cell = NONE, form = f, tac = r, loc = ll,
187 branch = b, result = (e_term, []), ostate= Incomplete}) pt p
189 fun cappend_parent pt p loc f r b = (* for tests only *)
190 apfst (append_parent p loc f r b) (cut_tree pt (p, Und));
192 fun append_atomic p l f r f' s pt =
195 if existpt p pt andalso is_empty_tac (get_obj g_tac pt p)
196 then (*after Take*) ((fst (get_obj g_loc pt p), SOME l), get_obj g_form pt p)
197 else ((NONE, SOME l), f)
199 insert_pt (PrfObj {cell = NONE, form = f, tac = r, loc = iss, branch = NoBranch,
200 result = f', ostate = s}) pt p
203 (* 20.8.02: cappend_* FIXXXXME cut branches below cannot be decided here:
204 detail - generate - cappend: inserted, not appended !!!
205 cut decided in applicable_in !?!
207 fun cappend_atomic pt p ist_res f r f' s =
208 if existpt p pt andalso is_empty_tac (get_obj g_tac pt p)
209 then (*after Take: transfer Frm and respective istate*)
212 (get_loc pt (p,Frm), get_obj g_form pt p)
213 val (pt, cs) = cut_tree pt (p,Frm)
214 val pt = append_atomic p (Selem.e_istate, Selem.e_ctxt) f r f' s pt
215 val pt = update_loc' pt p (SOME ist_form, SOME ist_res)
217 else apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
219 fun append_result pt p l f s =
220 (appl_obj (repl_result (fst (get_obj g_loc pt p), SOME l) f s) pt p, []);