1.1 --- a/src/Tools/isac/Interpret/ctree-basic.sml Fri Jan 06 15:02:46 2017 +0100
1.2 +++ b/src/Tools/isac/Interpret/ctree-basic.sml Fri Jan 06 15:52:58 2017 +0100
1.3 @@ -17,10 +17,6 @@
1.4
1.5 (*===\<Longrightarrow> KEEP IN ctree-basic.sml =============================================================*)
1.6
1.7 -(* ---- made visible ONLY for structure CTaccess : CALC_TREE_ACCESS --------------------------- *)
1.8 -
1.9 -(* ---- made visible ONLY for structure CTnavi : CALC_TREE_NAVIGATION ------------------------- *)
1.10 -
1.11 (* ---- for tests only: made visible in order to remove the warning --------------------------- *)
1.12 type state
1.13 type result
1.14 @@ -230,31 +226,6 @@
1.15 val get_curr_formula : state -> term
1.16 val get_assumptions_ : ctree -> pos' -> term list (* for appl.sml *)
1.17
1.18 - val append_result : ctree -> pos -> istate * Proof.context -> result ->
1.19 - ostate -> ctree * 'a list
1.20 - val append_atomic : (* for solve.sml *)
1.21 - pos -> istate * Proof.context -> term -> tac -> result -> ostate -> ctree -> ctree
1.22 - val cappend_atomic : ctree -> pos -> istate * Proof.context -> term -> tac -> result ->
1.23 - ostate -> ctree * pos' list
1.24 - val cappend_form : ctree -> pos -> istate * Proof.context -> term -> ctree * pos' list
1.25 - val cappend_problem : ctree -> pos -> istate * Proof.context -> fmz ->
1.26 - ori list * spec * term -> ctree * pos' list
1.27 -
1.28 - val update_branch : ctree -> pos -> branch -> ctree
1.29 - val update_ctxt : ctree -> pos -> Proof.context -> ctree
1.30 - val update_env : ctree -> pos -> (istate * Proof.context) option -> ctree
1.31 - val update_oris : ctree -> pos -> ori list -> ctree
1.32 - val update_orispec : ctree -> pos -> spec -> ctree
1.33 - val update_pbl : ctree -> pos -> itm list -> ctree
1.34 - val update_pblppc : ctree -> pos -> itm list -> ctree (* =vvv= ? *)
1.35 - val update_pblID : ctree -> pos -> pblID -> ctree (* =^^^= ? *)
1.36 - val update_met : ctree -> pos -> itm list -> ctree (* =vvv= ? *)
1.37 - val update_metppc : ctree -> pos -> itm list -> ctree (* =^^^= ? *)
1.38 - val update_metID : ctree -> pos -> metID -> ctree
1.39 - val update_domID : ctree -> pos -> domID -> ctree
1.40 - val update_spec : ctree -> pos -> spec -> ctree
1.41 - val update_tac : ctree -> pos -> tac -> ctree
1.42 -
1.43 val e_ctxt : Proof.context
1.44 val is_e_ctxt : Proof.context -> bool (* for appl.sml *)
1.45 val new_val : term -> istate -> istate
1.46 @@ -271,14 +242,20 @@
1.47 val eq_tac : tac * tac -> bool
1.48 (* for script.sml *)
1.49 val rootthy : ctree -> theory
1.50 +(* ---- made visible ONLY for structure CTaccess : CALC_TREE_ACCESS --------------------------- *)
1.51 + val appl_obj : (ppobj -> ppobj) -> ctree -> pos -> ctree
1.52 + val existpt : pos -> ctree -> bool (* also for tests *)
1.53 + val is_empty_tac : tac -> bool (* also for tests *)
1.54 + val cut_tree : ctree -> pos * 'a -> ctree * pos' list (* also for tests *)
1.55 + val insert_pt : ppobj -> ctree -> int list -> ctree
1.56 +(* ---- made visible ONLY for structure CTnavi : CALC_TREE_NAVIGATION ------------------------- *)
1.57 +
1.58 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.59 val update_loc' : ctree -> pos -> (istate * Proof.context) option * (istate * Proof.context) option -> ctree
1.60 val append_problem : int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree -> ctree
1.61 val g_res : ppobj -> term
1.62 val pr_ctree : (pos -> ppobj -> string) -> ctree -> string
1.63 val pr_short : pos -> ppobj -> string
1.64 - val existpt : pos -> ctree -> bool
1.65 - val is_empty_tac : tac -> bool
1.66 val e_subs : string list
1.67 val e_sube : cterm' list
1.68 val g_branch : ppobj -> branch
1.69 @@ -289,7 +266,6 @@
1.70 val get_allpos' : pos * posel -> ctree -> pos' list
1.71 val get_allpos's : pos * posel -> ctree list -> (pos * pos_) list
1.72 val cut_bottom : pos * posel -> ctree -> (ctree * pos' list) * bool
1.73 - val cut_tree : ctree -> pos * 'a -> ctree * pos' list
1.74 val cut_level : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
1.75 val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
1.76 val get_trace : ctree -> int list -> int list -> int list list
1.77 @@ -318,9 +294,6 @@
1.78 istate * Proof.context -> term -> tac -> result -> ostate -> ctree * (int list * pos_) list
1.79 val cappend_form :
1.80 ctree -> int list -> istate * Proof.context -> term -> ctree * (int list * pos_) list
1.81 - val cappend_parent :
1.82 - ctree ->
1.83 - int list -> istate * Proof.context -> term -> tac -> branch -> ctree * (int list * pos_) list
1.84 val cappend_problem :
1.85 ctree ->
1.86 int list ->
1.87 @@ -370,7 +343,6 @@
1.88 val get_somespec' : domID * pblID * metID -> domID * pblID * metID -> domID * pblID * metID
1.89 val get_trace : ctree -> int list -> int list -> int list list
1.90 type iist = istate option * istate option val ins_chn : ctree list -> ctree -> int list -> ctree
1.91 - val insert_pt : ppobj -> ctree -> int list -> ctree
1.92 val is_curr_endof_calc : ctree -> int list * pos_ -> bool val is_e_ctxt : Proof.context -> bool
1.93 val is_empty_tac : tac -> bool val is_interpos : 'a * pos_ -> bool val is_pblnd : ctree -> bool
1.94 val is_pblobj : ppobj -> bool val is_pblobj' : ctree -> int list -> bool
1.95 @@ -418,7 +390,7 @@
1.96 val pr_ctree : (int list -> ppobj -> string) -> ctree -> string val pr_pos : int list -> string
1.97 val pr_short : int list -> ppobj -> string val preconds2str : (bool * term) list -> string
1.98 datatype ptform = Form of term | ModSpec of ocalhd val repl : 'a list -> int -> 'a -> 'a list
1.99 - val repl_app : 'a list -> int -> 'a -> 'a list val repl_branch : branch -> ppobj -> ppobj
1.100 + val repl_app : 'a list -> int -> 'a -> 'a list
1.101 val repl_ctxt : Proof.context -> ppobj -> ppobj val repl_domID : domID -> ppobj -> ppobj
1.102 val repl_env : (istate * Proof.context) option -> ppobj -> ppobj
1.103 val repl_loc : (istate * Proof.context) option * (istate * Proof.context) option -> ppobj -> ppobj
1.104 @@ -1280,92 +1252,6 @@
1.105 | appl_obj f (Nd (b, bs)) (p :: []) = Nd (b, repl_app bs p (((appl_to_node f) o (nth p)) bs))
1.106 | appl_obj f (Nd (b, bs)) (p :: ps) = Nd (b, repl_app bs p (appl_obj f (nth p bs) (ps:pos)));
1.107
1.108 -(* for use by appl_obj *)
1.109 -fun repl_pbl x (PblObj {cell, origin, fmz, spec, probl = _, meth, ctxt, env, loc,
1.110 - branch, result, ostate}) =
1.111 - PblObj {cell = cell, origin = origin, fmz = fmz, spec = spec, probl= x, meth = meth,
1.112 - ctxt = ctxt, env = env, loc = loc, branch = branch, result = result, ostate = ostate}
1.113 - | repl_pbl _ _ = raise PTREE "repl_pbl takes no PrfObj";
1.114 -fun repl_met x (PblObj {cell, origin, fmz, spec, probl, meth = _, ctxt, env, loc,
1.115 - branch, result, ostate}) =
1.116 - PblObj {cell = cell, origin = origin, fmz= fmz, spec = spec, probl = probl,
1.117 - meth = x, ctxt = ctxt, env = env, loc = loc, branch = branch, result = result,
1.118 - ostate = ostate}
1.119 - | repl_met _ _ = raise PTREE "repl_pbl takes no PrfObj";
1.120 -fun repl_spec x (PblObj {cell, origin, fmz, spec = _, probl, meth, ctxt, env, loc,
1.121 - branch, result, ostate}) =
1.122 - PblObj {cell = cell, origin = origin, fmz = fmz, spec = x, probl = probl,
1.123 - meth = meth, ctxt = ctxt, env = env, loc = loc, branch = branch, result = result,
1.124 - ostate = ostate}
1.125 - | repl_spec _ _ = raise PTREE "repl_domID takes no PrfObj";
1.126 -fun repl_domID x (PblObj {cell, origin, fmz, spec = (_, p, m), probl, meth, ctxt, env, loc,
1.127 - branch, result, ostate}) =
1.128 - PblObj {cell = cell, origin = origin, fmz = fmz, spec= (x, p, m), probl = probl,
1.129 - meth = meth, ctxt = ctxt, env = env, loc = loc, branch = branch, result = result,
1.130 - ostate = ostate}
1.131 - | repl_domID _ _ = raise PTREE "repl_domID takes no PrfObj";
1.132 -fun repl_pblID x (PblObj {cell, origin, fmz, spec= (d, _, m), probl, meth, ctxt, env, loc,
1.133 - branch, result, ostate}) =
1.134 - PblObj {cell = cell, origin = origin, fmz = fmz, spec= (d, x, m), probl = probl,
1.135 - meth = meth, ctxt = ctxt, env = env, loc = loc, branch = branch, result = result,
1.136 - ostate = ostate}
1.137 - | repl_pblID _ _ = raise PTREE "repl_pblID takes no PrfObj";
1.138 -fun repl_metID x (PblObj {cell, origin, fmz, spec = (d, p,_), probl, meth, ctxt, env, loc,
1.139 - branch, result, ostate}) =
1.140 - PblObj {cell = cell, origin = origin, fmz = fmz, spec = (d, p, x), probl = probl,
1.141 - meth = meth, ctxt = ctxt, env = env, loc = loc, branch = branch, result = result,
1.142 - ostate = ostate}
1.143 - | repl_metID _ _ = raise PTREE "repl_metID takes no PrfObj";
1.144 -fun repl_result l f' s (PrfObj {cell, form, tac, loc = _, branch, result = _ , ostate = _}) =
1.145 - PrfObj {cell = cell, form = form, tac = tac, loc = l, branch = branch, result = f', ostate = s}
1.146 - | repl_result l f' s (PblObj {cell, origin, fmz, spec, probl, meth, ctxt, env, loc = _,
1.147 - branch, result = _ , ostate= _}) =
1.148 - PblObj {cell = cell, origin = origin, fmz= fmz, spec = spec, probl = probl,
1.149 - meth = meth, ctxt = ctxt, env = env, loc = l, branch = branch, result = f', ostate = s};
1.150 -fun repl_tac x (PrfObj {cell, form, tac = _, loc, branch, result, ostate}) =
1.151 - PrfObj {cell = cell, form = form, tac = x, loc = loc, branch = branch,
1.152 - result = result, ostate = ostate}
1.153 - | repl_tac _ _ = raise PTREE "repl_tac takes no PblObj";
1.154 -fun repl_branch b (PblObj {cell, origin, fmz, spec, probl, meth, ctxt, env, loc, branch = _,
1.155 - result, ostate}) =
1.156 - PblObj {cell = cell, origin = origin, fmz = fmz, spec = spec, probl = probl,
1.157 - meth = meth, ctxt = ctxt, env = env, loc = loc, branch = b, result = result,
1.158 - ostate = ostate}
1.159 - | repl_branch b (PrfObj {cell, form, tac, loc, branch = _, result, ostate}) =
1.160 - PrfObj {cell = cell, form = form, tac = tac, loc = loc, branch = b,
1.161 - result = result, ostate = ostate};
1.162 -fun repl_ctxt x (PblObj {cell, origin, fmz, spec, probl, meth,
1.163 - ctxt = _, env, loc, branch, result, ostate}) =
1.164 - PblObj {cell = cell, origin = origin, fmz = fmz, spec = spec, probl = probl,
1.165 - meth = meth, ctxt = x, env = env, loc = loc, branch = branch, result = result,
1.166 - ostate = ostate}
1.167 - | repl_ctxt _ _ = raise PTREE "repl_env takes no PrfObj";
1.168 -fun repl_env e (PblObj {cell, origin, fmz, spec, probl, meth,
1.169 - ctxt, env = _, loc, branch, result, ostate}) =
1.170 - PblObj {cell = cell, origin = origin, fmz = fmz, spec = spec, probl = probl,
1.171 - meth = meth, ctxt = ctxt, env = e, loc = loc, branch = branch, result = result,
1.172 - ostate = ostate}
1.173 - | repl_env _ _ = raise PTREE "repl_env takes no PrfObj";
1.174 -fun repl_oris oris (PblObj { cell, origin = (_, spe, hdf),fmz, spec, probl, meth,
1.175 - ctxt, env, loc, branch, result, ostate}) =
1.176 - PblObj{cell = cell, origin = (oris, spe, hdf), fmz = fmz, spec = spec, probl = probl,
1.177 - meth = meth, ctxt = ctxt, env = env, loc = loc, branch = branch, result = result,
1.178 - ostate = ostate}
1.179 - | repl_oris _ _ = raise PTREE "repl_oris takes no PrfObj";
1.180 -fun repl_orispec spe (PblObj {cell, origin = (oris, _, hdf), fmz, spec, probl, meth,
1.181 - ctxt, env, loc, branch, result, ostate}) =
1.182 - PblObj{cell = cell, origin = (oris, spe, hdf), fmz = fmz, spec = spec, probl = probl,
1.183 - meth = meth, ctxt = ctxt, env = env, loc = loc, branch = branch, result = result,
1.184 - ostate = ostate}
1.185 - | repl_orispec _ _ = raise PTREE "repl_orispec takes no PrfObj";
1.186 -fun repl_loc l (PblObj {cell, origin, fmz, spec, probl, meth,
1.187 - ctxt, env, loc = _ , branch, result, ostate}) =
1.188 - PblObj {cell = cell, origin = origin, fmz = fmz, spec = spec, probl = probl,
1.189 - meth = meth, ctxt = ctxt, env = env, loc = l, branch = branch, result = result,
1.190 - ostate = ostate}
1.191 - | repl_loc l (PrfObj {cell, form, tac, loc = _, branch, result, ostate}) =
1.192 - PrfObj {cell = cell, form = form, tac = tac, loc= l, branch = branch, result = result,
1.193 - ostate = ostate}
1.194
1.195 type ocalhd =
1.196 bool * (* ALL itms+preconds true *)
1.197 @@ -1394,22 +1280,6 @@
1.198 PrfObj {cell = cell, form = form, tac = tac, loc = (l1, NONE), branch = branch,
1.199 result = (e_term, []), ostate = Incomplete};
1.200
1.201 -fun update_ctxt pt pos x = appl_obj (repl_ctxt x) pt pos; (* for use on PblObj,
1.202 - otherwise use fun generate1; compare fun get_ctxt*)
1.203 -fun update_env pt pos x = appl_obj (repl_env x) pt pos;
1.204 -fun update_domID pt pos x = appl_obj (repl_domID x) pt pos;
1.205 -fun update_pblID pt pos x = appl_obj (repl_pblID x) pt pos;
1.206 -fun update_metID pt pos x = appl_obj (repl_metID x) pt pos;
1.207 -fun update_spec pt pos x = appl_obj (repl_spec x) pt pos;
1.208 -fun update_pbl pt pos x = appl_obj (repl_pbl x) pt pos;
1.209 -fun update_pblppc pt pos x = appl_obj (repl_pbl x) pt pos;
1.210 -fun update_met pt pos x = appl_obj (repl_met x) pt pos;
1.211 -fun update_metppc pt pos x = appl_obj (repl_met x) pt pos;
1.212 -fun update_branch pt pos x = appl_obj (repl_branch x) pt pos;
1.213 -fun update_tac pt pos x = appl_obj (repl_tac x) pt pos;
1.214 -fun update_oris pt pos x = appl_obj (repl_oris x) pt pos;
1.215 -fun update_orispec pt pos x = appl_obj (repl_orispec x) pt pos;
1.216 -fun update_loc' pt pos x = appl_obj (repl_loc x) pt pos;
1.217
1.218 fun get_loc EmptyPtree _ = (e_istate, e_ctxt)
1.219 | get_loc pt (p, Res) =
1.220 @@ -1874,73 +1744,8 @@
1.221 in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P) end
1.222 end;
1.223
1.224 -fun append_atomic p l f r f' s pt =
1.225 - let
1.226 - val (iss, f) =
1.227 - if existpt p pt andalso is_empty_tac (get_obj g_tac pt p)
1.228 - then (*after Take*) ((fst (get_obj g_loc pt p), SOME l), get_obj g_form pt p)
1.229 - else ((NONE, SOME l), f)
1.230 - in
1.231 - insert_pt (PrfObj {cell = NONE, form = f, tac = r, loc = iss, branch = NoBranch,
1.232 - result = f', ostate = s}) pt p
1.233 - end;
1.234
1.235
1.236 -(* 20.8.02: cappend_* FIXXXXME cut branches below cannot be decided here:
1.237 - detail - generate - cappend: inserted, not appended !!!
1.238 - cut decided in applicable_in !?!
1.239 -*)
1.240 -fun cappend_atomic pt p ist_res f r f' s =
1.241 - if existpt p pt andalso is_empty_tac (get_obj g_tac pt p)
1.242 - then (*after Take: transfer Frm and respective istate*)
1.243 - let
1.244 - val (ist_form, f) =
1.245 - (get_loc pt (p,Frm), get_obj g_form pt p)
1.246 - val (pt, cs) = cut_tree pt (p,Frm)
1.247 - val pt = append_atomic p (e_istate, e_ctxt) f r f' s pt
1.248 - val pt = update_loc' pt p (SOME ist_form, SOME ist_res)
1.249 - in (pt, cs) end
1.250 - else apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
1.251 -
1.252 -(* called by Take *)
1.253 -fun append_form p l f pt =
1.254 - insert_pt (PrfObj {cell = NONE, form = f, tac = Empty_Tac, loc = (SOME l, NONE),
1.255 - branch = NoBranch, result = (e_term, []), ostate = Incomplete}) pt p;
1.256 -
1.257 -fun cappend_form pt p loc f =
1.258 - let
1.259 - val (pt', cs) = cut_tree pt (p, Frm)
1.260 - val pt'' = append_form p loc f pt'
1.261 - in (pt'', cs) end;
1.262 -
1.263 -fun append_result pt p l f s =
1.264 - (appl_obj (repl_result (fst (get_obj g_loc pt p), SOME l) f s) pt p, []);
1.265 -
1.266 -(*WN041022 deprecated, still for kbtest/diffapp.sml, /systest/root-equ.sml*)
1.267 -fun append_parent p l f r b pt =
1.268 - let
1.269 - val (ll, f) =
1.270 - if existpt p pt andalso is_empty_tac (get_obj g_tac pt p)
1.271 - then ((fst (get_obj g_loc pt p), SOME l), get_obj g_form pt p)
1.272 - else ((SOME l, NONE), f)
1.273 - in insert_pt (PrfObj {cell = NONE, form = f, tac = r, loc = ll,
1.274 - branch = b, result = (e_term, []), ostate= Incomplete}) pt p
1.275 - end;
1.276 -fun cappend_parent pt p loc f r b = (* for tests only *)
1.277 - apfst (append_parent p loc f r b) (cut_tree pt (p, Und));
1.278 -
1.279 -fun append_problem [] l fmz (strs, spec, hdf) _ =
1.280 - (Nd (PblObj {cell = NONE, origin = (strs, spec, hdf), fmz = fmz, spec = empty_spec,
1.281 - probl = [], meth = [], ctxt = e_ctxt, env = NONE, loc = (SOME l, NONE),
1.282 - branch = TransitiveB, result = (e_term, []), ostate = Incomplete}, []))
1.283 - | append_problem p l fmz (strs, spec, hdf) pt =
1.284 - insert_pt (PblObj {cell = NONE, origin = (strs, spec, hdf), fmz = fmz, spec = empty_spec,
1.285 - probl = [], meth = [], ctxt = e_ctxt, env = NONE, loc = (SOME l, NONE),
1.286 - branch = TransitiveB, result = (e_term, []), ostate= Incomplete}) pt p;
1.287 -fun cappend_problem _ [] loc fmz ori = (append_problem [] loc fmz ori EmptyPtree, [])
1.288 - | cappend_problem pt p loc fmz ori =
1.289 - apfst (append_problem p loc fmz ori) (cut_tree pt (p, Frm));
1.290 -
1.291 (* get the theory explicitly specified for the rootpbl;
1.292 thus use this function _after_ finishing specification *)
1.293 fun rootthy (Nd (PblObj {spec = (thyID, _, _), ...}, _)) = assoc_thy thyID