1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/ME/ctree.sml Mon Dec 31 14:18:53 2007 +0100
1.3 @@ -0,0 +1,2162 @@
1.4 +(* use"../ME/ctree.sml";
1.5 + use"ME/ctree.sml";
1.6 + use"ctree.sml";
1.7 + W.N.26.10.99
1.8 +
1.9 +writeln (pr_ptree pr_short pt);
1.10 +
1.11 +val Nd ( _, ns) = pt;
1.12 +
1.13 +*)
1.14 +
1.15 +(*structure Ptree (**): PTREE (**) = ###### outcommented ######*)
1.16 +signature PTREE =
1.17 +sig
1.18 + type ptree
1.19 + type envp
1.20 + val e_ptree : ptree
1.21 + exception PTREE of string
1.22 + type branch
1.23 + type ostate
1.24 + type cellID
1.25 + type cid
1.26 + type posel
1.27 + type pos
1.28 + type pos'
1.29 + type loc
1.30 + type domID
1.31 + type pblID
1.32 + type metID
1.33 + type spec
1.34 + type 'a ppc
1.35 + type con
1.36 + type subs
1.37 + type subst
1.38 + type env
1.39 + type ets
1.40 + val ets2str : ets -> string
1.41 + type item
1.42 + type tac
1.43 + type tac_
1.44 + val tac_2str : tac_ -> string
1.45 + type safe
1.46 + val safe2str : safe -> string
1.47 +
1.48 + type meth
1.49 + val cappend_atomic : ptree -> pos -> loc -> cterm' -> tac
1.50 + -> cterm' -> ostate -> cid -> ptree * posel list * cid
1.51 + val cappend_form : ptree
1.52 + -> pos -> loc -> cterm' -> cid -> ptree * pos * cid
1.53 + val cappend_parent : ptree -> pos -> loc -> cterm' -> tac
1.54 + -> branch -> cid -> ptree * int list * cid
1.55 + val cappend_problem : ptree -> posel list(*FIXME*) -> loc
1.56 + -> cterm' list * spec -> cid -> ptree * int list * cellID list
1.57 + val append_result : ptree -> pos -> cterm' -> ostate -> ptree * pos
1.58 +
1.59 + type ppobj
1.60 + val g_branch : ppobj -> branch
1.61 + val g_cell : ppobj -> cid
1.62 + val g_args : ppobj -> (int * (term list)) list (*args of scr*)
1.63 + val g_form : ppobj -> cterm'
1.64 + val g_loc : ppobj -> loc
1.65 + val g_met : ppobj -> meth
1.66 + val g_domID : ppobj -> domID
1.67 + val g_metID : ppobj -> metID
1.68 + val g_model : ppobj -> cterm' ppc
1.69 + val g_tac : ppobj -> tac
1.70 + val g_origin : ppobj -> cterm' list * spec
1.71 + val g_ostate : ppobj -> ostate
1.72 + val g_pbl : ppobj -> pblID * item ppc
1.73 + val g_result : ppobj -> cterm'
1.74 + val g_spec : ppobj -> spec
1.75 +(* val get_all : (ppobj -> 'a) -> ptree -> 'a list
1.76 + val get_alls : (ppobj -> 'a) -> ptree list -> 'a list *)
1.77 + val get_obj : (ppobj -> 'a) -> ptree -> pos -> 'a
1.78 + val gpt_cell : ptree -> cid
1.79 + val par_pblobj : ptree -> pos -> pos
1.80 + val pre_pos : pos -> pos
1.81 + val lev_dn : int list -> int list
1.82 + val lev_on : pos -> posel list
1.83 + val lev_pred : pos -> pos
1.84 + val lev_up : pos -> pos
1.85 +(* val pr_cell : pos -> ppobj -> string
1.86 + val pr_pos : int list -> string *)
1.87 + val pr_ptree : (pos -> ppobj -> string) -> ptree -> string
1.88 + val pr_short : pos -> ppobj -> string
1.89 +(* val repl : 'a list -> int -> 'a -> 'a list
1.90 + val repl_app : 'a list -> int -> 'a -> 'a list
1.91 + val repl_branch : branch -> ppobj -> ppobj
1.92 + val repl_domID : domID -> ppobj -> ppobj
1.93 + val repl_form : cterm' -> ppobj -> ppobj
1.94 + val repl_met : item ppc -> ppobj -> ppobj
1.95 + val repl_metID : metID -> ppobj -> ppobj
1.96 + val repl_model : cterm' list -> ppobj -> ppobj
1.97 + val repl_tac : tac -> ppobj -> ppobj
1.98 + val repl_pbl : item ppc -> ppobj -> ppobj
1.99 + val repl_pblID : pblID -> ppobj -> ppobj
1.100 + val repl_result : cterm' -> ostate -> ppobj -> ppobj
1.101 + val repl_spec : spec -> ppobj -> ppobj
1.102 + val repl_subs : (string * string) list -> ppobj -> ppobj *)
1.103 + val rootthy : ptree -> domID
1.104 +(* val test_trans : ppobj -> bool
1.105 + val uni__asm : (string * pos) list -> ppobj -> ppobj
1.106 + val uni__cid : cellID list -> ppobj -> ppobj *)
1.107 + val union_asm : ptree -> pos -> (string * pos) list -> ptree
1.108 + val union_cid : ptree -> pos -> cellID list -> ptree
1.109 + val update_branch : ptree -> pos -> branch -> ptree
1.110 + val update_domID : ptree -> pos -> domID -> ptree
1.111 + val update_met : ptree -> pos -> meth -> ptree
1.112 + val update_metppc : ptree -> pos -> item ppc -> ptree
1.113 + val update_metID : ptree -> pos -> metID -> ptree
1.114 + val update_tac : ptree -> pos -> tac -> ptree
1.115 + val update_pbl : ptree -> pos -> pblID * item ppc -> ptree
1.116 + val update_pblppc : ptree -> pos -> item ppc -> ptree
1.117 + val update_pblID : ptree -> pos -> pblID -> ptree
1.118 + val update_spec : ptree -> pos -> spec -> ptree
1.119 + val update_subs : ptree -> pos -> (string * string) list -> ptree
1.120 +
1.121 + val rep_pblobj : ppobj
1.122 + -> {branch:branch, cell:cid, env:envp, loc:loc, meth:meth, model:cterm' ppc,
1.123 + origin:cterm' list * spec, ostate:ostate, probl:pblID * item ppc,
1.124 + result:cterm', spec:spec}
1.125 + val rep_prfobj : ppobj
1.126 + -> {branch:branch, cell:cid, form:cterm', loc:loc, tac:tac,
1.127 + ostate:ostate, result:cterm'}
1.128 +end
1.129 +
1.130 +(* --------------
1.131 +structure Ptree (**): PTREE (**) =
1.132 +struct
1.133 + -------------- *)
1.134 +
1.135 +type env = (term * term) list;
1.136 +
1.137 +
1.138 +datatype branch =
1.139 + NoBranch | AndB | OrB
1.140 + | TransitiveB (* FIXXXME.8.03: set branch from met in Apply_Method
1.141 + FIXXXME.0402: -"- in Begin_Trans'*)
1.142 + | SequenceB | IntersectB | CollectB | MapB;
1.143 +fun branch2str NoBranch = "NoBranch"
1.144 + | branch2str AndB = "AndB"
1.145 + | branch2str OrB = "OrB"
1.146 + | branch2str TransitiveB = "TransitiveB"
1.147 + | branch2str SequenceB = "SequenceB"
1.148 + | branch2str IntersectB = "IntersectB"
1.149 + | branch2str CollectB = "CollectB"
1.150 + | branch2str MapB = "MapB";
1.151 +
1.152 +datatype ostate =
1.153 + Incomplete | Complete | Inconsistent(*WN041020 latter unused*);
1.154 +fun ostate2str Incomplete = "Incomplete"
1.155 + | ostate2str Complete = "Complete"
1.156 + | ostate2str Inconsistent = "Inconsistent";
1.157 +
1.158 +type cellID = int;
1.159 +type cid = cellID list;
1.160 +
1.161 +type posel = int; (* roundabout for (some of) nice signatures *)
1.162 +type pos = posel list;
1.163 +val pos2str = ints2str';
1.164 +datatype pos_ =
1.165 + Pbl (*PblObj-position: problem-type*)
1.166 + | Met (*PblObj-position: method*)
1.167 + | Frm (*PblObj-position: -> Pbl in ME (not by moveDown !)
1.168 + | PrfObj-position: formula*)
1.169 + | Res (*PblObj | PrfObj-position: result*)
1.170 + | Und; (*undefined*)
1.171 +fun pos_2str Pbl = "Pbl"
1.172 + | pos_2str Met = "Met"
1.173 + | pos_2str Frm = "Frm"
1.174 + | pos_2str Res = "Res"
1.175 + | pos_2str Und = "Und";
1.176 +
1.177 +type pos' = pos * pos_;
1.178 +(*WN.12.03 remembering interator (pos * pos_) for ptree
1.179 + pos : lev_on, lev_dn, lev_up,
1.180 + lev_onFrm, lev_dnRes (..see solve Apply_Method !)
1.181 + pos_:
1.182 +# generate1 sets pos_ if possible ...?WN0502?NOT...
1.183 +# generate1 does NOT set pos, because certain nodes can be lev_on OR lev_dn
1.184 + exceptions: Begin/End_Trans
1.185 +# thus generate(1) called in
1.186 +.# assy, locate_gen
1.187 +.# nxt_solv (tac_ -cases); general case:
1.188 + val pos' = case pos' of (p,Res) => (lev_on p',Res) | _ => pos'
1.189 +# WN050220, S(604):
1.190 + generate1...(Rewrite(f,..,res))..(pos, pos_)
1.191 + cappend_atomic.................pos ////// gets f+res always!!!
1.192 + cut_tree....................pos, pos_
1.193 +*)
1.194 +fun pos'2str (p,p_) = pair2str (ints2str' p, pos_2str p_);
1.195 +fun pos's2str ps = (strs2str' o (map pos'2str)) ps;
1.196 +val e_pos' = ([],Und):pos';
1.197 +
1.198 +fun res2str (t, ts) = pair2str (term2str t, terms2str ts);
1.199 +fun asm2str (t, p:pos) = pair2str (term2str t, ints2str' p);
1.200 +fun asms2str asms = (strs2str' o (map asm2str)) asms;
1.201 +
1.202 +
1.203 +
1.204 +(*26.4.02: never used after introduction of scripts !!!
1.205 +type loc = loc_ * (* + interpreter-state *)
1.206 + (loc_ * rls') (* -"- for script of the ruleset*)
1.207 + option;
1.208 +val e_loc = ([],None):loc;
1.209 +val ee_loc = (e_loc,e_loc);*)
1.210 +
1.211 +
1.212 +datatype safe = Sundef | Safe | Unsafe | Helpless;
1.213 +fun safe2str Sundef = "Sundef"
1.214 + | safe2str Safe = "Safe"
1.215 + | safe2str Unsafe = "Unsafe"
1.216 + | safe2str Helpless = "Helpless";
1.217 +
1.218 +type subs = cterm' list; (*16.11.00 for FE-KE*)
1.219 +val e_subs = ["(bdv, x)"];
1.220 +
1.221 +(*._sub_stitution as strings of _e_qualities.*)
1.222 +type sube = cterm' list;
1.223 +val e_sube = []:cterm' list;
1.224 +fun sube2str s = strs2str s;
1.225 +
1.226 +(*._sub_stitution as _t_erms of _e_qualities.*)
1.227 +type subte = term list;
1.228 +val e_subte = []:term list;
1.229 +fun subte2str ss = terms2str ss;
1.230 +
1.231 +fun subte2sube ss = map term2str ss;
1.232 +
1.233 +(*fun subst2str' thy' (s:subst) =
1.234 + (strs2str o
1.235 + (map (pair2str o
1.236 + (apsnd (Sign.string_of_term (sign_of (assoc_thy thy')))) o
1.237 + (apfst (Sign.string_of_term (sign_of (assoc_thy thy'))))))) s;*)
1.238 +fun subst2subs s = map (pair2str o
1.239 + (apfst (Sign.string_of_term (sign_of thy))) o
1.240 + (apsnd (Sign.string_of_term (sign_of thy)))) s;
1.241 +fun subst2subs' s = map ((apfst (Sign.string_of_term (sign_of thy))) o
1.242 + (apsnd (Sign.string_of_term (sign_of thy)))) s;
1.243 +fun subs2subst thy s = map (isapair2pair o term_of o the o (parse thy)) s;
1.244 +(*> subs2subst thy ["(bdv,x)","(err,#0)"];
1.245 +val it =
1.246 + [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real")),
1.247 + (Free ("err","RealDef.real"),Free ("#0","RealDef.real"))]
1.248 + : (term * term) list*)
1.249 +fun sube2subte ss = map str2term ss;
1.250 +
1.251 +
1.252 +fun isasub2subst isasub = ((map isapair2pair) o isalist2list) isasub;
1.253 +
1.254 +
1.255 +type scrstate = (*state for script interpreter*)
1.256 + env(*stack*) (*used to instantiate tac for checking assod
1.257 + 12.03.noticed: e_ not updated during execution ?!?*)
1.258 + * loc_ (*location of tac in script*)
1.259 + * term option(*argument of curried functions*)
1.260 + * term (*value obtained by tac executed
1.261 + updated also after a derivation by 'new_val'*)
1.262 + * safe (*estimation of how result will be obtained*)
1.263 + * bool; (*true = strongly .., false = weakly associated:
1.264 + only used during ass_dn/up*)
1.265 +val e_scrstate = ([],[],None,e_term,Sundef,false):scrstate;
1.266 +
1.267 +
1.268 +(*21.8.02 ---> definitions.sml for datatype scr
1.269 +type rrlsstate = (*state for reverse rewriting*)
1.270 + (term * (*the current formula*)
1.271 + rule list (*of reverse rewrite set (#1#)*)
1.272 + list * (*may be serveral, eg. in norm_rational*)
1.273 + (rule * (*Thm (+ Thm generated from Calc) resulting in ...*)
1.274 + (term * (*... rewrite with ...*)
1.275 + term list)) (*... assumptions*)
1.276 + list); (*derivation from given term to normalform
1.277 + in reverse order with sym_thm;
1.278 + (#1#) could be extracted from here #1*) --------*)
1.279 +
1.280 +datatype istate = (*interpreter state*)
1.281 + Uistate (*undefined in modspec, in '_deriv'ation*)
1.282 + | ScrState of scrstate (*for script interpreter*)
1.283 + | RrlsState of rrlsstate; (*for reverse rewriting*)
1.284 +val e_istate = (ScrState ([],[],None,e_term,Sundef,false)):istate;
1.285 +
1.286 +type iist = istate option * istate option;
1.287 +(*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*)
1.288 +
1.289 +
1.290 +fun rta2str (r,(t,a)) = "\n("^(rule2str r)^",("^(term2str t)^", "^
1.291 + (terms2str a)^"))";
1.292 +fun istate2str Uistate = "Uistate"
1.293 + | istate2str (ScrState (e,l,to,t,s,b):istate) =
1.294 + "ScrState ("^ subst2str e ^",\n "^
1.295 + loc_2str l ^", "^ termopt2str to ^",\n "^
1.296 + term2str t ^", "^ safe2str s ^", "^ bool2str b ^")"
1.297 + | istate2str (RrlsState (t,t1,rss,rtas)) =
1.298 + "RrlsState ("^(term2str t)^", "^(term2str t1)^", "^
1.299 + ((strs2str o (map (strs2str o (map rule2str)))) rss)^", "^
1.300 + ((strs2str o (map rta2str)) rtas)^")";
1.301 +fun istates2str (None, None) = "(#None, #None)"
1.302 + | istates2str (None, Some ist) = "(#None,\n#Some "^istate2str ist^")"
1.303 + | istates2str (Some ist, None) = "(#Some "^istate2str ist^",\n #None)"
1.304 + | istates2str (Some i1, Some i2) = "(#Some "^istate2str i1^",\n #Some "^
1.305 + istate2str i2^")";
1.306 +
1.307 +fun new_val v (ScrState (env, loc_, topt, _, safe, bool)) =
1.308 + (ScrState (env, loc_, topt, v, safe, bool))
1.309 + | new_val _ _ = raise error "new_val: only for ScrState";
1.310 +
1.311 +datatype con = land | lor;
1.312 +
1.313 +
1.314 +type spec =
1.315 + domID * (*WN.12.03: is replaced by thy from get_met ?FIXME? in:
1.316 + specify (Init_Proof..), nxt_specify_init_calc,
1.317 + assod (.SubProblem...), stac2tac (.SubProblem...)*)
1.318 + pblID *
1.319 + metID;
1.320 +fun spec2str ((dom,pbl,met)(*:spec*)) =
1.321 + "(" ^ (quote dom) ^ ", " ^ (strs2str pbl) ^
1.322 + ", " ^ (strs2str met) ^ ")";
1.323 +(*> spec2str empty_spec;
1.324 +val it = "(\"\", [], (\"\", \"\"))" : string *)
1.325 +val empty_spec = (e_domID,e_pblID,e_metID):spec;
1.326 +val e_spec = empty_spec;
1.327 +
1.328 +
1.329 +
1.330 +(*.tactics propagate the construction of the calc-tree;
1.331 + there are
1.332 + (a) 'specsteps' for the specify-phase, and others for the solve-phase
1.333 + (b) those of the solve-phase are 'initac's and others;
1.334 + initacs start with a formula different from the preceding formula.
1.335 + see 'type tac_' for the internal representation of tactics.*)
1.336 +datatype tac =
1.337 + Init_Proof of ((cterm' list) * spec)
1.338 +(*'specsteps'...*)
1.339 +| Model_Problem
1.340 +| Refine_Problem of pblID | Refine_Tacitly of pblID
1.341 +
1.342 +| Add_Given of cterm' | Del_Given of cterm'
1.343 +| Add_Find of cterm' | Del_Find of cterm'
1.344 +| Add_Relation of cterm' | Del_Relation of cterm'
1.345 +
1.346 +| Specify_Theory of domID | Specify_Problem of pblID
1.347 +| Specify_Method of metID
1.348 +(*...'specsteps'*)
1.349 +| Apply_Method of metID
1.350 +(*.creates an 'istate' in PblObj.env; in case of 'init_form'
1.351 + creates a formula at ((lev_on o lev_dn) p, Frm) and in this ppobj.'loc'
1.352 + 'Some istate' (at fst of 'loc').
1.353 + As each step (in the solve-phase) has a resulting formula (at the front-end)
1.354 + Apply_Method also does the 1st step in the script (an 'initac') if there
1.355 + is no 'init_form' .*)
1.356 +| Check_Postcond of pblID
1.357 +| Free_Solve
1.358 +
1.359 +| Rewrite_Inst of ( subs * thm') | Rewrite of thm'
1.360 + | Rewrite_Asm of thm'
1.361 +| Rewrite_Set_Inst of ( subs * rls') | Rewrite_Set of rls'
1.362 +| Detail_Set_Inst of ( subs * rls') | Detail_Set of rls'
1.363 +| End_Detail (*end of script from next_tac,
1.364 + in solve: switches back to parent script WN0509 drop!*)
1.365 +| Derive of rls' (*an input formula using rls WN0509 drop!*)
1.366 +| Calculate of string (* plus | minus | times | cancel | pow | sqrt *)
1.367 +| End_Ruleset
1.368 +| Substitute of sube | Apply_Assumption of cterm' list
1.369 +
1.370 +| Take of cterm' (*an 'initac'*)
1.371 +| Take_Inst of cterm'
1.372 +| Group of (con * int list )
1.373 +| Subproblem of (domID * pblID) (*an 'initac'*)
1.374 +| CAScmd of cterm' (*6.6.02 URD: Function formula; WN0509 drop!*)
1.375 +| End_Subproblem (*WN0509 drop!*)
1.376 +
1.377 +| Split_And | Conclude_And
1.378 +| Split_Or | Conclude_Or
1.379 +| Begin_Trans | End_Trans
1.380 +| Begin_Sequ | End_Sequ(* substitute root.env *)
1.381 +| Split_Intersect | End_Intersect
1.382 +| Check_elementwise of cterm' | Collect_Trues
1.383 +| Or_to_List
1.384 +
1.385 +| Empty_Tac (*TODO.11.6.03 ... of string: could carry msg of (Notappl msg)
1.386 + in 'helpless'*)
1.387 +| Tac of string(* eg.'repeat'*WN0509 drop!*)
1.388 +| User (*internal, for ets*WN0509 drop!*)
1.389 +| End_Proof';(* inout*)
1.390 +
1.391 +(* tac2str /--> library.sml: needed in dialog.sml for 'separable *)
1.392 +fun tac2str (ma:tac) = case ma of
1.393 + Init_Proof (ppc, spec) =>
1.394 + "Init_Proof "^(pair2str (strs2str ppc, spec2str spec))
1.395 + | Model_Problem => "Model_Problem "
1.396 + | Refine_Tacitly pblID => "Refine_Tacitly "^(strs2str pblID)
1.397 + | Refine_Problem pblID => "Refine_Problem "^(strs2str pblID)
1.398 + | Add_Given cterm' => "Add_Given "^cterm'
1.399 + | Del_Given cterm' => "Del_Given "^cterm'
1.400 + | Add_Find cterm' => "Add_Find "^cterm'
1.401 + | Del_Find cterm' => "Del_Find "^cterm'
1.402 + | Add_Relation cterm' => "Add_Relation "^cterm'
1.403 + | Del_Relation cterm' => "Del_Relation "^cterm'
1.404 +
1.405 + | Specify_Theory domID => "Specify_Theory "^(quote domID )
1.406 + | Specify_Problem pblID => "Specify_Problem "^(strs2str pblID )
1.407 + | Specify_Method metID => "Specify_Method "^(strs2str metID)
1.408 + | Apply_Method metID => "Apply_Method "^(strs2str metID)
1.409 + | Check_Postcond pblID => "Check_Postcond "^(strs2str pblID)
1.410 + | Free_Solve => "Free_Solve"
1.411 +
1.412 + | Rewrite_Inst (subs,thm')=>
1.413 + "Rewrite_Inst "^(pair2str (subs2str subs, spair2str thm'))
1.414 + | Rewrite thm' => "Rewrite "^(spair2str thm')
1.415 + | Rewrite_Asm thm' => "Rewrite_Asm "^(spair2str thm')
1.416 + | Rewrite_Set_Inst (subs, rls) =>
1.417 + "Rewrite_Set_Inst "^(pair2str (subs2str subs, quote rls))
1.418 + | Rewrite_Set rls => "Rewrite_Set "^(quote rls )
1.419 + | Detail_Set rls => "Detail_Set "^(quote rls )
1.420 + | Detail_Set_Inst (subs, rls) =>
1.421 + "Detail_Set_Inst "^(pair2str (subs2str subs, quote rls))
1.422 + | End_Detail => "End_Detail"
1.423 + | Derive rls' => "Derive "^rls'
1.424 + | Calculate op_ => "Calculate "^op_
1.425 + | Substitute sube => "Substitute "^sube2str sube
1.426 + | Apply_Assumption ct's => "Apply_Assumption "^(strs2str ct's)
1.427 +
1.428 + | Take cterm' => "Take "^(quote cterm' )
1.429 + | Take_Inst cterm' => "Take_Inst "^(quote cterm' )
1.430 + | Group (con, ints) =>
1.431 + "Group "^(pair2str (con2str con, ints2str ints))
1.432 + | Subproblem (domID, pblID) =>
1.433 + "Subproblem "^(pair2str (domID, strs2str pblID))
1.434 +(*| Subproblem_Full (spec, cts') =>
1.435 + "Subproblem_Full "^(pair2str (spec2str spec, strs2str cts'))*)
1.436 + | End_Subproblem => "End_Subproblem"
1.437 + | CAScmd cterm' => "CAScmd "^(quote cterm')
1.438 +
1.439 + | Check_elementwise cterm'=> "Check_elementwise "^(quote cterm')
1.440 + | Or_to_List => "Or_to_List "
1.441 + | Collect_Trues => "Collect_Trues"
1.442 +
1.443 + | Empty_Tac => "Empty_Tac"
1.444 + | Tac string => "Tac "^string
1.445 + | User => "User"
1.446 + | End_Proof' => "tac End_Proof'"
1.447 + | _ => "tac2str not impl. for ?!";
1.448 +
1.449 +fun is_rewset (Rewrite_Set_Inst _) = true
1.450 + | is_rewset (Rewrite_Set _) = true
1.451 + | is_rewset _ = false;
1.452 +fun is_rewtac (Rewrite _) = true
1.453 + | is_rewtac (Rewrite_Inst _) = true
1.454 + | is_rewtac (Rewrite_Asm _) = true
1.455 + | is_rewtac tac = is_rewset tac;
1.456 +
1.457 +fun tac2IDstr (ma:tac) = case ma of
1.458 + Model_Problem => "Model_Problem"
1.459 + | Refine_Tacitly pblID => "Refine_Tacitly"
1.460 + | Refine_Problem pblID => "Refine_Problem"
1.461 + | Add_Given cterm' => "Add_Given"
1.462 + | Del_Given cterm' => "Del_Given"
1.463 + | Add_Find cterm' => "Add_Find"
1.464 + | Del_Find cterm' => "Del_Find"
1.465 + | Add_Relation cterm' => "Add_Relation"
1.466 + | Del_Relation cterm' => "Del_Relation"
1.467 +
1.468 + | Specify_Theory domID => "Specify_Theory"
1.469 + | Specify_Problem pblID => "Specify_Problem"
1.470 + | Specify_Method metID => "Specify_Method"
1.471 + | Apply_Method metID => "Apply_Method"
1.472 + | Check_Postcond pblID => "Check_Postcond"
1.473 + | Free_Solve => "Free_Solve"
1.474 +
1.475 + | Rewrite_Inst (subs,thm')=> "Rewrite_Inst"
1.476 + | Rewrite thm' => "Rewrite"
1.477 + | Rewrite_Asm thm' => "Rewrite_Asm"
1.478 + | Rewrite_Set_Inst (subs, rls) => "Rewrite_Set_Inst"
1.479 + | Rewrite_Set rls => "Rewrite_Set"
1.480 + | Detail_Set rls => "Detail_Set"
1.481 + | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst"
1.482 + | Derive rls' => "Derive "
1.483 + | Calculate op_ => "Calculate "
1.484 + | Substitute subs => "Substitute"
1.485 + | Apply_Assumption ct's => "Apply_Assumption"
1.486 +
1.487 + | Take cterm' => "Take"
1.488 + | Take_Inst cterm' => "Take_Inst"
1.489 + | Group (con, ints) => "Group"
1.490 + | Subproblem (domID, pblID) => "Subproblem"
1.491 + | End_Subproblem => "End_Subproblem"
1.492 + | CAScmd cterm' => "CAScmd"
1.493 +
1.494 + | Check_elementwise cterm'=> "Check_elementwise"
1.495 + | Or_to_List => "Or_to_List "
1.496 + | Collect_Trues => "Collect_Trues"
1.497 +
1.498 + | Empty_Tac => "Empty_Tac"
1.499 + | Tac string => "Tac "
1.500 + | User => "User"
1.501 + | End_Proof' => "End_Proof'"
1.502 + | _ => "tac2str not impl. for ?!";
1.503 +
1.504 +fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
1.505 + | rls_of (Rewrite_Set rls) = rls
1.506 + | rls_of tac = raise error ("rls_of: called with tac '"^tac2IDstr tac^"'");
1.507 +
1.508 +fun thm_of_rew (Rewrite_Inst (subs,(thmID,_))) =
1.509 + (thmID, Some ((subs2subst (assoc_thy "Isac.thy") subs):subst))
1.510 + | thm_of_rew (Rewrite (thmID,_)) = (thmID, None)
1.511 + | thm_of_rew (Rewrite_Asm (thmID,_)) = (thmID, None);
1.512 +
1.513 +fun rls_of_rewset (Rewrite_Set_Inst (subs,rls)) =
1.514 + (rls, Some ((subs2subst (assoc_thy "Isac.thy") subs):subst))
1.515 + | rls_of_rewset (Rewrite_Set rls) = (rls, None)
1.516 + | rls_of_rewset (Detail_Set rls) = (rls, None)
1.517 + | rls_of_rewset (Detail_Set_Inst (subs, rls)) =
1.518 + (rls, Some ((subs2subst (assoc_thy "Isac.thy") subs):subst));
1.519 +
1.520 +(*fun rule2tac (Thm (thmID, thm)) =
1.521 + Rewrite (thmID, string_of_thmI thm)
1.522 + | rule2tac (Rls_ rls) = Rewrite_Set (id_rls rls)
1.523 + | rule2tac (Rls_ rls) = Rewrite_Set (id_rls rls)
1.524 + | rule2tac rule =
1.525 + raise error ("rule2tac: called with '" ^ rule2str rule ^ "'");
1.526 +WN071231*)
1.527 +fun rule2tac _ (Calc (opID, thm)) = Calculate opID
1.528 + | rule2tac [] (Thm (thmID, thm)) = Rewrite (thmID, string_of_thmI thm)
1.529 + | rule2tac subst (Thm (thmID, thm)) =
1.530 + Rewrite_Inst (subst2subs subst, (thmID, string_of_thmI thm))
1.531 + | rule2tac [] (Rls_ rls) = Rewrite_Set (id_rls rls)
1.532 + | rule2tac subst (Rls_ rls) =
1.533 + Rewrite_Set_Inst (subst2subs subst, (id_rls rls))
1.534 + | rule2tac _ rule =
1.535 + raise error ("rule2tac: called with '" ^ rule2str rule ^ "'");
1.536 +
1.537 +
1.538 +type fmz_ = cterm' list;
1.539 +
1.540 +(*.a formalization of an example containing data
1.541 + sufficient for mechanically finding the solution for the example.*)
1.542 +(*FIXME.WN051014: dont store fmz = (_,spec) in the PblObj,
1.543 + this is done in origin*)
1.544 +type fmz = fmz_ * spec;
1.545 +val e_fmz = ([],e_spec);
1.546 +
1.547 +(*tac_ is made from tac in applicable_in,
1.548 + and carries all data necessary for generate;*)
1.549 +datatype tac_ =
1.550 +(* datatype tac = *)
1.551 + Init_Proof' of ((cterm' list) * spec)
1.552 + (* ori list !: code specify -> applicable*)
1.553 +| Model_Problem' of pblID *
1.554 + itm list * (*the 'untouched' pbl*)
1.555 + itm list (*the casually completed met*)
1.556 +| Refine_Tacitly' of pblID * (*input*)
1.557 + pblID * (*the refined from applicable_in*)
1.558 + domID * (*from new pbt?! filled in specify*)
1.559 + metID * (*from new pbt?! filled in specify*)
1.560 + itm list (*drop ! 9.03: remains [] for
1.561 + Model_Problem recognizing its activation*)
1.562 +| Refine_Problem' of (pblID * (itm list * (bool * Term.term) list))
1.563 + (*FIXME?040215 drop: done automatically in init_proof + Subproblem'*)
1.564 +| Add_Given' of cterm' *
1.565 + itm list (*updated with input in fun specify_additem*)
1.566 +| Add_Find' of cterm' *
1.567 + itm list (*updated with input in fun specify_additem*)
1.568 +| Add_Relation' of cterm' *
1.569 + itm list (*updated with input in fun specify_additem*)
1.570 +| Del_Given' of cterm' | Del_Find' of cterm' | Del_Relation' of cterm'
1.571 + (*4.00.: all.. term: in applicable_in ..? Syn ?only for FormFK?*)
1.572 +
1.573 +| Specify_Theory' of domID
1.574 +| Specify_Problem' of (pblID * (* *)
1.575 + (bool * (* matches *)
1.576 + (itm list * (* ppc *)
1.577 + (bool * term) list))) (* preconditions *)
1.578 +| Specify_Method' of metID *
1.579 + ori list * (*repl. "#undef"*)
1.580 + itm list (*... updated from pbl to met*)
1.581 +| Apply_Method' of metID *
1.582 + (term option) * (*init_form*)
1.583 + istate
1.584 +| Check_Postcond' of
1.585 + pblID *
1.586 + (term * (*returnvalue of script in solve*)
1.587 + cterm' list)(*collect by get_assumptions_ in applicable_in, except if
1.588 + butlast tac is Check_elementwise: take only these asms*)
1.589 +| Free_Solve'
1.590 +
1.591 +| Rewrite_Inst' of theory' * rew_ord' * rls
1.592 + * bool * subst * thm' * term * (term * term list)
1.593 +| Rewrite' of theory' * rew_ord' * rls * bool * thm' *
1.594 + term * (term * term list)
1.595 +| Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm' *
1.596 + term * (term * term list)
1.597 +| Rewrite_Set_Inst' of theory' * bool * subst * rls *
1.598 + term * (term * term list)
1.599 +| Detail_Set_Inst' of theory' * bool * subst * rls *
1.600 + term * (term * term list)
1.601 +| Rewrite_Set' of theory' * bool * rls * term * (term * term list)
1.602 +| Detail_Set' of theory' * bool * rls * term * (term * term list)
1.603 +| End_Detail' of (term * (term list)) (*see End_Trans'*)
1.604 +| End_Ruleset' of term
1.605 +| Derive' of rls
1.606 +| Calculate' of theory' * string * term * (term * thm')
1.607 + (*WN.29.4.03 asm?: * term list??*)
1.608 +| Substitute' of subte (*the 'substitution': terms of type bool*)
1.609 + * term (*to be substituted in*)
1.610 + * term (*resulting from the substitution*)
1.611 +| Apply_Assumption' of term list * term
1.612 +
1.613 +| Take' of term | Take_Inst' of term
1.614 +| Group' of (con * int list * term)
1.615 +| Subproblem' of (spec *
1.616 + (ori list) * (*filled in assod Subproblem'*)
1.617 + term * (*-"-, headline of calc-head *)
1.618 + fmz_ *
1.619 + term) (*Subproblem(dom,pbl)*)
1.620 +| CAScmd' of term
1.621 +| End_Subproblem' of term (*???*)
1.622 +| Split_And' of term | Conclude_And' of term
1.623 +| Split_Or' of term | Conclude_Or' of term
1.624 +| Begin_Trans' of term | End_Trans' of (term * (term list))
1.625 +| Begin_Sequ' | End_Sequ'(* substitute root.env*)
1.626 +| Split_Intersect' of term | End_Intersect' of term
1.627 +| Check_elementwise' of (*special case:*)
1.628 + term * (*(1)the current formula: [x=1,x=...]*)
1.629 + string * (*(2)the pred from Check_elementwise *)
1.630 + (term * (*(3)composed from (1) and (2): {x. pred}*)
1.631 + term list) (*20.5.03 assumptions*)
1.632 +
1.633 +| Or_to_List' of term * term (* (a | b, [a,b]) *)
1.634 +| Collect_Trues' of term
1.635 +
1.636 +| Empty_Tac_ | Tac_ of (*for dummies*)
1.637 + theory *
1.638 + string * (*form*)
1.639 + string * (*in Tac*)
1.640 + string (*result of Tac".."*)
1.641 +| User' (*internal for ets*) | End_Proof'';(*End_Proof:inout*)
1.642 +
1.643 +fun tac_2str ma = case ma of
1.644 + Init_Proof' (ppc, spec) =>
1.645 + "Init_Proof' "^(pair2str (strs2str ppc, spec2str spec))
1.646 + | Model_Problem' (pblID,_,_) => "Model_Problem' "^(strs2str pblID )
1.647 + | Refine_Tacitly'(p,prefin,domID,metID,itms)=>
1.648 + "Refine_Tacitly' ("
1.649 + ^(strs2str p)^", "^(strs2str prefin)^", "
1.650 + ^domID^", "^(strs2str metID)^", pbl-itms)"
1.651 + | Refine_Problem' ms => "Refine_Problem' ("^(*matchs2str ms*)"..."^")"
1.652 +(*| Match_Problem' (pI, (ok, (itms, pre))) =>
1.653 + "Match_Problem' "^(spair2str (strs2str pI,
1.654 + spair2str (bool2str ok,
1.655 + spair2str ("itms2str itms",
1.656 + "items2str pre"))))*)
1.657 + | Add_Given' cterm' => "Add_Given' "(*^cterm'*)
1.658 + | Del_Given' cterm' => "Del_Given' "(*^cterm'*)
1.659 + | Add_Find' cterm' => "Add_Find' "(*^cterm'*)
1.660 + | Del_Find' cterm' => "Del_Find' "(*^cterm'*)
1.661 + | Add_Relation' cterm' => "Add_Relation' "(*^cterm'*)
1.662 + | Del_Relation' cterm' => "Del_Relation' "(*^cterm'*)
1.663 +
1.664 + | Specify_Theory' domID => "Specify_Theory' "^(quote domID )
1.665 + | Specify_Problem' (pI, (ok, (itms, pre))) =>
1.666 + "Specify_Problem' "^(spair2str (strs2str pI,
1.667 + spair2str (bool2str ok,
1.668 + spair2str ("itms2str itms",
1.669 + "items2str pre"))))
1.670 + | Specify_Method' (pI,oris,itms) =>
1.671 + "Specify_Method' ("^metID2str pI^", "^oris2str oris^", )"
1.672 +
1.673 + | Apply_Method' (metID,_,_) => "Apply_Method' "^(strs2str metID)
1.674 + | Check_Postcond' (pblID,(scval,asm)) =>
1.675 + "Check_Postcond' "^(spair2str(strs2str pblID,
1.676 + spair2str (term2str scval, strs2str asm)))
1.677 +
1.678 + | Free_Solve' => "Free_Solve'"
1.679 +
1.680 + | Rewrite_Inst' (*subs,thm'*) _ =>
1.681 + "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
1.682 + | Rewrite' thm' => "Rewrite' "(*^(spair2str thm')*)
1.683 + | Rewrite_Asm' thm' => "Rewrite_Asm' "(*^(spair2str thm')*)
1.684 + | Rewrite_Set_Inst' (*subs,thm'*) _ =>
1.685 + "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
1.686 + | Rewrite_Set'(thy',pasm,rls',f,(f',asm))
1.687 + => "Rewrite_Set' ("^thy'^","^(bool2str pasm)^","^(id_rls rls')^","
1.688 + ^(Sign.string_of_term (sign_of thy) f)^",("^(Sign.string_of_term (sign_of thy) f')
1.689 + ^","^((strs2str o (map (Sign.string_of_term (sign_of thy)))) asm)^"))"
1.690 +
1.691 + | End_Detail' _ => "End_Detail' xxx"
1.692 + | Detail_Set' _ => "Detail_Set' xxx"
1.693 + | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
1.694 +
1.695 + | Derive' rls => "Derive' "^id_rls rls
1.696 + | Calculate' _ => "Calculate' "
1.697 + | Substitute' subs => "Substitute' "(*^(subs2str subs)*)
1.698 + | Apply_Assumption' ct's => "Apply_Assumption' "(*^(strs2str ct's)*)
1.699 +
1.700 + | Take' cterm' => "Take' "(*^(quote cterm' )*)
1.701 + | Take_Inst' cterm' => "Take_Inst' "(*^(quote cterm' )*)
1.702 + | Group' (con, ints, _) =>
1.703 + "Group' "^(pair2str (con2str con, ints2str ints))
1.704 + | Subproblem' (spec, oris, _,_,pbl_form) =>
1.705 + "Subproblem' "(*^(pair2str (domID, strs2str ,...))*)
1.706 + | End_Subproblem' _ => "End_Subproblem'"
1.707 + | CAScmd' cterm' => "CAScmd' "(*^(quote cterm')*)
1.708 +
1.709 + | Empty_Tac_ => "Empty_Tac_"
1.710 + | User' => "User'"
1.711 + | Tac_ (_,form,id,result) => "Tac_ (thy,"^form^","^id^","^result^")"
1.712 + | _ => "tac_2str not impl. for arg";
1.713 +
1.714 +(*'executed tactics' (tac_s) with local environment etc.;
1.715 + used for continuing eval script + for generate*)
1.716 +type ets =
1.717 + (loc_ * (* of tactic in scr, tactic (weakly) associated with tac_*)
1.718 + (tac_ * (* (for generate) *)
1.719 + env * (* with 'tactic=result' as a rule, tactic ev. _not_ ready:
1.720 + for handling 'parallel let'*)
1.721 + env * (* with results of (ready) tacs *)
1.722 + term * (* itr_arg of tactic, for upd. env at Repeat, Try*)
1.723 + term * (* result value of the tac *)
1.724 + safe))
1.725 + list;
1.726 +val Ets = []:ets;
1.727 +
1.728 +
1.729 +fun ets2s (l,(m,eno,env,iar,res,s)) =
1.730 + "\n("^(loc_2str l)^",("^(tac_2str m)^
1.731 + ",\n ens= "^(subst2str eno)^
1.732 + ",\n env= "^(subst2str env)^
1.733 + ",\n iar= "^(Sign.string_of_term (sign_of thy) iar)^
1.734 + ",\n res= "^(Sign.string_of_term (sign_of thy) res)^
1.735 + ",\n "^(safe2str s)^"))";
1.736 +fun ets2str (ets:ets) = (strs2str o (map ets2s)) ets;
1.737 +
1.738 +
1.739 +type envp =(*9.5.03: unused, delete with field in ptree.PblObj FIXXXME*)
1.740 + (int * term list) list * (*assoc-list: args of met*)
1.741 + (int * rls) list * (*assoc-list: tacs already done ///15.9.00*)
1.742 + (int * ets) list * (*assoc-list: tacs etc. already done*)
1.743 + (string * pos) list; (*asms * from where*)
1.744 +val empty_envp = ([],[],[],[]):envp;
1.745 +
1.746 +datatype ppobj =
1.747 + PrfObj of {cell : lrd option, (*where in form tac has been applied*)
1.748 + (*^^^FIXME.WN0607 rename this field*)
1.749 + form : term,
1.750 + tac : tac, (* also in istate*)
1.751 + loc : istate option * istate option, (*for form, result
1.752 +13.8.02: (None,None) <==> e_istate ! see update_loc, get_loc*)
1.753 + branch: branch,
1.754 + result: term * term list,
1.755 + ostate: ostate} (*Complete <=> result is OK*)
1.756 + | PblObj of {cell : lrd option,(*unused: meaningful only for some _Prf_Obj*)
1.757 + fmz : fmz, (*from init:FIXME never use this spec;-drop*)
1.758 + origin: (ori list) * (*representation from fmz+pbt
1.759 + for efficiently adding items in probl, meth*)
1.760 + spec * (*updated by Refine_Tacitly*)
1.761 + term, (*headline of calc-head, as calculated
1.762 + initially(!)*)
1.763 + (*# the origin of a root-pbl is created from fmz
1.764 + (thus providing help for input to the user),
1.765 + # the origin of a sub-pbl is created from the argument
1.766 + -list of a script-tac 'SubProblem (spec) [arg-list]'
1.767 + by 'match_ags'*)
1.768 + spec : spec, (*explicitly input*)
1.769 + probl : itm list, (*itms explicitly input*)
1.770 + meth : itm list, (*itms automatically added to copy of probl
1.771 + TODO: input like to 'probl'*)
1.772 + env : istate option,(*for problem with initac in script*)
1.773 + loc : istate option * istate option, (*for pbl+met * result*)
1.774 + branch: branch,
1.775 + result: term * term list,
1.776 + ostate: ostate}; (*Complete <=> result is _proven_ OK*)
1.777 +
1.778 +(*.this tree contains isac's calculations; TODO.WN03 rename to ctree;
1.779 + the structure has been copied from an early version of Theorema(c);
1.780 + it has the disadvantage, that there is no space
1.781 + for the first tactic in a script generating the first formula at (p,Frm);
1.782 + this trouble has been covered by 'init_form' and 'Take' so far,
1.783 + but it is crucial if the first tactic in a script is eg. 'Subproblem';
1.784 + see 'type tac ', Apply_Method.
1.785 +.*)
1.786 +datatype ptree =
1.787 + EmptyPtree
1.788 + | Nd of ppobj * (ptree list);
1.789 +val e_ptree = EmptyPtree;
1.790 +
1.791 +fun rep_prfobj (PrfObj {cell,form,tac,loc,branch,result,ostate}) =
1.792 + {cell=cell,form=form,tac=tac,loc=loc,branch=branch,result=result,ostate=ostate};
1.793 +fun rep_pblobj (PblObj {cell,origin,fmz,spec,probl,meth,env,
1.794 + loc,branch,result,ostate}) =
1.795 + {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,
1.796 + env=env,loc=loc,branch=branch,result=result,ostate=ostate};
1.797 +fun is_prfobj (PrfObj _) = true
1.798 + | is_prfobj _ =false;
1.799 +(*val is_prfobj' = get_obj is_prfobj; *)
1.800 +fun is_pblobj (PblObj _) = true
1.801 + | is_pblobj _ = false;
1.802 +(*val is_pblobj' = get_obj is_pblobj; 'Error: unbound constructor get_obj'*)
1.803 +
1.804 +
1.805 +exception PTREE of string;
1.806 +fun nth _ [] = raise PTREE "nth _ []"
1.807 + | nth 1 (x::xs) = x
1.808 + | nth n (x::xs) = nth (n-1) xs;
1.809 +(*> nth 2 [11,22,33]; -->> val it = 22 : int*)
1.810 +
1.811 +fun lev_up ([]:pos) = raise PTREE "lev_up []"
1.812 + | lev_up p = (drop_last p):pos;
1.813 +fun lev_on ([]:pos) = raise PTREE "lev_on []"
1.814 + | lev_on pos =
1.815 + let val len = length pos
1.816 + in (drop_last pos) @ [(nth len pos)+1] end;
1.817 +fun lev_onFrm ((p,_):pos') = (lev_on p,Frm):pos'
1.818 + | lev_onFrm p = raise PTREE ("*** lev_onFrm: pos'="^(pos'2str p));
1.819 +(*040216: for inform --> embed_deriv: remains on same level*)
1.820 +fun lev_back (([],_):pos') = raise PTREE "lev_on_back: called by ([],_)"
1.821 + | lev_back (p,_) =
1.822 + if last_elem p <= 1 then (p, Frm):pos'
1.823 + else ((drop_last p) @ [(nth (length p) p) - 1], Res);
1.824 +(*.increase pos by n within a level.*)
1.825 +fun pos_plus 0 pos = pos
1.826 + | pos_plus n ((p,Frm):pos') = pos_plus (n-1) (p, Res)
1.827 + | pos_plus n ((p, _):pos') = pos_plus (n-1) (lev_on p, Res);
1.828 +
1.829 +
1.830 +
1.831 +fun lev_pred ([]:pos) = raise PTREE "lev_pred []"
1.832 + | lev_pred (pos:pos) =
1.833 + let val len = length pos
1.834 + in ((drop_last pos) @ [(nth len pos)-1]):pos end;
1.835 +(*lev_pred [1,2,3];
1.836 +val it = [1,2,2] : pos
1.837 +> lev_pred [1];
1.838 +val it = [0] : pos *)
1.839 +
1.840 +fun lev_dn p = p @ [0];
1.841 +(*> (lev_dn o lev_on) [1,2,3];
1.842 +val it = [1,2,4,0] : pos *)
1.843 +(*fun lev_dn' ((p,p_):pos') = (lev_dn p, Frm):pos'; WN.3.12.03: never used*)
1.844 +fun lev_dnRes ((p,_):pos') = (lev_dn p, Res):pos';
1.845 +
1.846 +(*4.4.00*)
1.847 +fun lev_up_ ((p,Res):pos') = (lev_up p,Res):pos'
1.848 + | lev_up_ p' = raise error ("lev_up_: called for "^(pos'2str p'));
1.849 +fun lev_dn_ ((p,_):pos') = (lev_dn p,Res):pos'
1.850 +fun ind ((p,_):pos') = length p; (*WN050108 deprecated in favour of lev_of*)
1.851 +fun lev_of ((p,_):pos') = length p;
1.852 +
1.853 +
1.854 +(** convert ptree to a string **)
1.855 +
1.856 +(* convert a pos from list to string *)
1.857 +fun pr_pos ps = (space_implode "." (map string_of_int ps))^". ";
1.858 +(* show hd origin or form only *)
1.859 +fun pr_short (p:pos) (PblObj {origin = (ori,_,_),...}) =
1.860 + ((pr_pos p) ^ " ----- pblobj -----\n")
1.861 +(* ((((Sign.string_of_term (sign_of thy)) o #4 o hd) ori)^" "^
1.862 + (((Sign.string_of_term (sign_of thy)) o hd(*!?!*) o #5 o hd) ori))^
1.863 + "\n") *)
1.864 + | pr_short p (PrfObj {form = form,...}) =
1.865 + ((pr_pos p) ^ (term2str form) ^ "\n");
1.866 +(*
1.867 +fun pr_cell (p:pos) (PblObj {cell = c, origin = (ori,_,_),...}) =
1.868 + ((ints2str c) ^" "^
1.869 + ((((Sign.string_of_term (sign_of thy)) o #4 o hd) ori)^" "^
1.870 + (((Sign.string_of_term (sign_of thy)) o hd(*!?!*) o #5 o hd) ori))^
1.871 + "\n")
1.872 + | pr_cell p (PrfObj {cell = c, form = form,...}) =
1.873 + ((ints2str c) ^" "^ (term2str form) ^ "\n");
1.874 +*)
1.875 +
1.876 +(* convert ptree *)
1.877 +fun pr_ptree f pt =
1.878 + let
1.879 + fun pr_pt pfn _ EmptyPtree = ""
1.880 + | pr_pt pfn ps (Nd (b, [])) = pfn ps b
1.881 + | pr_pt pfn ps (Nd (b, ts)) = (pfn ps b)^
1.882 + (prts pfn (ps:pos) 1 ts)
1.883 + and prts pfn ps p [] = ""
1.884 + | prts pfn ps p (t::ts) = (pr_pt pfn (ps @ [p]) t)^
1.885 + (prts pfn ps (p+1) ts)
1.886 + in pr_pt f [] pt end;
1.887 +(*
1.888 +> fun prfn ps b = (pr_pos ps)^" "^b(*TODO*)^"\n";
1.889 +> val pt = ref EmptyPtree;
1.890 +> pt:=Nd("root",
1.891 + [Nd("xx1",[]),
1.892 + Nd("xx2",
1.893 + [Nd("xx2.1.",[]),
1.894 + Nd("xx2.2.",[])]),
1.895 + Nd("xx3",[])]);
1.896 +> writeln (pr_ptree prfn (!pt));
1.897 +*)
1.898 +
1.899 +
1.900 +(** access the branches of ptree **)
1.901 +
1.902 +fun ins_nth 1 e l = e::l
1.903 + | ins_nth n e [] = raise PTREE "ins_nth n e []"
1.904 + | ins_nth n e (l::ls) = l::(ins_nth (n-1) e ls);
1.905 +fun repl [] _ _ = raise PTREE "repl [] _ _"
1.906 + | repl (l::ls) 1 e = e::ls
1.907 + | repl (l::ls) n e = l::(repl ls (n-1) e);
1.908 +fun repl_app ls n e =
1.909 + let val lim = 1 + length ls
1.910 + in if n > lim then raise PTREE "repl_app: n > lim"
1.911 + else if n = lim then ls @ [e]
1.912 + else repl ls n e end;
1.913 +(*
1.914 +> repl [1,2,3] 2 22222;
1.915 +val it = [1,22222,3] : int list
1.916 +> repl_app [1,2,3,4] 5 5555;
1.917 +val it = [1,2,3,4,5555] : int list
1.918 +> repl_app [1,2,3] 2 22222;
1.919 +val it = [1,22222,3] : int list
1.920 +> repl_app [1] 2 22222 ;
1.921 +val it = [1,22222] : int list
1.922 +*)
1.923 +
1.924 +
1.925 +(*.get from obj at pos by f : ppobj -> 'a.*)
1.926 +fun get_obj f EmptyPtree (_:pos) = raise PTREE "get_obj f EmptyPtree"
1.927 + | get_obj f (Nd (b, _)) [] = f b
1.928 + | get_obj f (Nd (b, bs)) (p::ps) =
1.929 +(* val (f, Nd (b, bs), (p::ps)) = (I, pt, p);
1.930 + *)
1.931 + let val _ = (nth p bs) handle _ => raise PTREE ("get_obj: pos = "^
1.932 + (ints2str' (p::ps))^" does not exist");
1.933 + in (get_obj f (nth p bs) (ps:pos))
1.934 + (*before WN050419: 'wrong type..' raised also if pos doesn't exist*)
1.935 + handle _ => raise PTREE (*"get_obj: at pos = "^
1.936 + (ints2str' (p::ps))^" wrong type of ppobj"*)
1.937 + ("get_obj: pos = "^
1.938 + (ints2str' (p::ps))^" does not exist")
1.939 + end;
1.940 +fun get_nd EmptyPtree _ = raise PTREE "get_nd EmptyPtree"
1.941 + | get_nd n [] = n
1.942 + | get_nd (Nd (_,nds)) (pos as p::(ps:pos)) = (get_nd (nth p nds) ps)
1.943 + handle _ => raise PTREE ("get_nd: not existent pos = "^(ints2str' pos));
1.944 +
1.945 +
1.946 +(* for use by get_obj *)
1.947 +fun g_cell (PblObj {cell = c,...}) = None
1.948 + | g_cell (PrfObj {cell = c,...}) = c;(*WN0607 hack for quick introduction of lrd + rewrite-at (thms, calcs)*)
1.949 +fun g_form (PrfObj {form = f,...}) = f
1.950 + | g_form (PblObj {origin=(_,_,f),...}) = f;
1.951 +fun g_form' (Nd (PrfObj {form = f,...}, _)) = f
1.952 + | g_form' (Nd (PblObj {origin=(_,_,f),...}, _)) = f;
1.953 +(* | g_form _ = raise PTREE "g_form not for PblObj";*)
1.954 +fun g_origin (PblObj {origin = ori,...}) = ori
1.955 + | g_origin _ = raise PTREE "g_origin not for PrfObj";
1.956 +fun g_fmz (PblObj {fmz = f,...}) = f
1.957 + | g_fmz _ = raise PTREE "g_fmz not for PrfObj";
1.958 +fun g_spec (PblObj {spec = s,...}) = s
1.959 + | g_spec _ = raise PTREE "g_spec not for PrfObj";
1.960 +fun g_pbl (PblObj {probl = p,...}) = p
1.961 + | g_pbl _ = raise PTREE "g_pbl not for PrfObj";
1.962 +fun g_met (PblObj {meth = p,...}) = p
1.963 + | g_met _ = raise PTREE "g_met not for PrfObj";
1.964 +fun g_domID (PblObj {spec = (d,_,_),...}) = d
1.965 + | g_domID _ = raise PTREE "g_metID not for PrfObj";
1.966 +fun g_metID (PblObj {spec = (_,_,m),...}) = m
1.967 + | g_metID _ = raise PTREE "g_metID not for PrfObj";
1.968 +fun g_env (PblObj {env,...}) = env
1.969 + | g_env _ = raise PTREE "g_env not for PrfObj";
1.970 +fun g_loc (PblObj {loc = l,...}) = l
1.971 + | g_loc (PrfObj {loc = l,...}) = l;
1.972 +fun g_branch (PblObj {branch = b,...}) = b
1.973 + | g_branch (PrfObj {branch = b,...}) = b;
1.974 +fun g_tac (PblObj {spec = (d,p,m),...}) = Apply_Method m
1.975 + | g_tac (PrfObj {tac = m,...}) = m;
1.976 +fun g_result (PblObj {result = r,...}) = r
1.977 + | g_result (PrfObj {result = r,...}) = r;
1.978 +fun g_res (PblObj {result = (r,_),...}) = r
1.979 + | g_res (PrfObj {result = (r,_),...}) = r;
1.980 +fun g_res' (Nd (PblObj {result = (r,_),...}, _)) = r
1.981 + | g_res' (Nd (PrfObj {result = (r,_),...}, _)) = r;
1.982 +fun g_ostate (PblObj {ostate = r,...}) = r
1.983 + | g_ostate (PrfObj {ostate = r,...}) = r;
1.984 +fun g_ostate' (Nd (PblObj {ostate = r,...}, _)) = r
1.985 + | g_ostate' (Nd (PrfObj {ostate = r,...}, _)) = r;
1.986 +
1.987 +fun gpt_cell (Nd (PblObj {cell = c,...},_)) = None
1.988 + | gpt_cell (Nd (PrfObj {cell = c,...},_)) = c;
1.989 +
1.990 +(*in CalcTree/Subproblem an 'just_created_' model is created;
1.991 + this is filled to 'untouched' by Model/Refine_Problem*)
1.992 +fun just_created_ (PblObj {meth, probl, spec, ...}) =
1.993 + null meth andalso null probl andalso spec = e_spec;
1.994 +val e_origin = ([],e_spec,e_term): (ori list) * spec * term;
1.995 +
1.996 +fun just_created (pt,(p,_):pos') =
1.997 + let val ppobj = get_obj I pt p
1.998 + in is_pblobj ppobj andalso just_created_ ppobj end;
1.999 +
1.1000 +(*.does the pos in the ctree exist ?.*)
1.1001 +fun existpt pos pt = can (get_obj I pt) pos;
1.1002 +(*.does the pos' in the ctree exist, ie. extra check for result in the node.*)
1.1003 +fun existpt' ((p,p_):pos') pt =
1.1004 + if can (get_obj I pt) p
1.1005 + then case p_ of
1.1006 + Res => get_obj g_ostate pt p = Complete
1.1007 + | _ => true
1.1008 + else false;
1.1009 +
1.1010 +(*.is this position appropriate for calculating intermediate steps?.*)
1.1011 +fun is_interpos ((_, Res):pos') = true
1.1012 + | is_interpos _ = false;
1.1013 +
1.1014 +fun last_onlev pt pos = not (existpt (lev_on pos) pt);
1.1015 +
1.1016 +
1.1017 +(*.find the position of the next parent which is a PblObj in ptree.*)
1.1018 +fun par_pblobj pt ([]:pos) = ([]:pos)
1.1019 + | par_pblobj pt p =
1.1020 + let fun par pt [] = []
1.1021 + | par pt p = if is_pblobj (get_obj I pt p) then p
1.1022 + else par pt (lev_up p)
1.1023 + in par pt (lev_up p) end;
1.1024 +(* lev_up for hard_gen operating with pos = [...,0] *)
1.1025 +
1.1026 +(*.find the position and the children of the next parent which is a PblObj.*)
1.1027 +fun par_children (Nd (PblObj _, children)) ([]:pos) = (children, []:pos)
1.1028 + | par_children (pt as Nd (PblObj _, children)) p =
1.1029 + let fun par [] = (children, [])
1.1030 + | par p = let val Nd (obj, children) = get_nd pt p
1.1031 + in if is_pblobj obj then (children, p) else par (lev_up p)
1.1032 + end;
1.1033 + in par (lev_up p) end;
1.1034 +
1.1035 +(*.get the children of a node in ptree.*)
1.1036 +fun children (Nd (PblObj _, cn)) = cn
1.1037 + | children (Nd (PrfObj _, cn)) = cn;
1.1038 +
1.1039 +
1.1040 +(*.find the next parent, which is either a PblObj (return true)
1.1041 + or a PrfObj with tac = Detail_Set (return false).*)
1.1042 +(*FIXME.3.4.03:re-organize par_pbl_det after rls' --> rls*)
1.1043 +fun par_pbl_det pt ([]:pos) = (true, []:pos, Erls)
1.1044 + | par_pbl_det pt p =
1.1045 + let fun par pt [] = (true, [], Erls)
1.1046 + | par pt p = if is_pblobj (get_obj I pt p) then (true, p, Erls)
1.1047 + else case get_obj g_tac pt p of
1.1048 + (*Detail_Set rls' => (false, p, assoc_rls rls')
1.1049 + (*^^^--- before 040206 after ---vvv*)
1.1050 + |*)Rewrite_Set rls' => (false, p, assoc_rls rls')
1.1051 + | Rewrite_Set_Inst (_, rls') =>
1.1052 + (false, p, assoc_rls rls')
1.1053 + | _ => par pt (lev_up p)
1.1054 + in par pt (lev_up p) end;
1.1055 +
1.1056 +
1.1057 +
1.1058 +
1.1059 +(*.get from the whole ptree by f : ppobj -> 'a.*)
1.1060 +fun get_all f EmptyPtree = []
1.1061 + | get_all f (Nd (b, [])) = [f b]
1.1062 + | get_all f (Nd (b, bs)) = [f b] @ (get_alls f bs)
1.1063 +and get_alls f [] = []
1.1064 + | get_alls f pts = flat (map (get_all f) pts);
1.1065 +
1.1066 +
1.1067 +(*.insert obj b into ptree at pos, ev.overwriting this pos.*)
1.1068 +fun insert b EmptyPtree ([]:pos) = Nd (b, [])
1.1069 + | insert b EmptyPtree _ = raise PTREE "insert b Empty _"
1.1070 + | insert b (Nd ( _, _)) [] = raise PTREE "insert b _ []"
1.1071 + | insert b (Nd (b', bs)) (p::[]) =
1.1072 + Nd (b', repl_app bs p (Nd (b,[])))
1.1073 + | insert b (Nd (b', bs)) (p::ps) =
1.1074 + Nd (b', repl_app bs p (insert b (nth p bs) ps));
1.1075 +(*
1.1076 +> type ppobj = string;
1.1077 +> writeln (pr_ptree prfn (!pt));
1.1078 + val pt = ref Empty;
1.1079 + pt:= insert ("root":ppobj) EmptyPtree [];
1.1080 + pt:= insert ("xx1":ppobj) (!pt) [1];
1.1081 + pt:= insert ("xx2":ppobj) (!pt) [2];
1.1082 + pt:= insert ("xx3":ppobj) (!pt) [3];
1.1083 + pt:= insert ("xx2.1":ppobj) (!pt) [2,1];
1.1084 + pt:= insert ("xx2.2":ppobj) (!pt) [2,2];
1.1085 + pt:= insert ("xx2.1.1":ppobj) (!pt) [2,1,1];
1.1086 + pt:= insert ("xx2.1.2":ppobj) (!pt) [2,1,2];
1.1087 + pt:= insert ("xx2.1.3":ppobj) (!pt) [2,1,3];
1.1088 +*)
1.1089 +
1.1090 +(*.insert children to a node without children.*)
1.1091 +(*compare: fun insert*)
1.1092 +fun ins_chn _ EmptyPtree (_:pos) = raise PTREE "ins_chn: EmptyPtree"
1.1093 + | ins_chn ns (Nd _) [] = raise PTREE "ins_chn: pos = []"
1.1094 + | ins_chn ns (Nd (b, bs)) (p::[]) =
1.1095 + if p > length bs then raise PTREE "ins_chn: pos not existent"
1.1096 + else let val Nd (b', bs') = nth p bs
1.1097 + in if null bs' then Nd (b, repl_app bs p (Nd (b', ns)))
1.1098 + else raise PTREE "ins_chn: pos mustNOT be overwritten" end
1.1099 + | ins_chn ns (Nd (b, bs)) (p::ps) =
1.1100 + Nd (b, repl_app bs p (ins_chn ns (nth p bs) ps));
1.1101 +
1.1102 +(* print_depth 11;ins_chn;print_depth 3; ###insert#########################*);
1.1103 +
1.1104 +
1.1105 +(** apply f to obj at pos, f: ppobj -> ppobj **)
1.1106 +
1.1107 +fun appl_to_node f (Nd (b,bs)) = Nd (f b, bs);
1.1108 +fun appl_obj f EmptyPtree [] = EmptyPtree
1.1109 + | appl_obj f EmptyPtree _ = raise PTREE "appl_obj f Empty _"
1.1110 + | appl_obj f (Nd (b, bs)) [] = Nd (f b, bs)
1.1111 + | appl_obj f (Nd (b, bs)) (p::[]) =
1.1112 + Nd (b, repl_app bs p (((appl_to_node f) o (nth p)) bs))
1.1113 + | appl_obj f (Nd (b, bs)) (p::ps) =
1.1114 + Nd (b, repl_app bs p (appl_obj f (nth p bs) (ps:pos)));
1.1115 +
1.1116 +(* for use by appl_obj *)
1.1117 +fun repl_form f (PrfObj {cell=c,form= _,tac=tac,loc=loc,
1.1118 + branch=branch,result=result,ostate=ostate}) =
1.1119 + PrfObj {cell=c,form= f,tac=tac,loc=loc,
1.1120 + branch=branch,result=result,ostate=ostate}
1.1121 + | repl_form _ _ = raise PTREE "repl_form takes no PblObj";
1.1122 +fun repl_pbl x (PblObj {cell=cell,origin=origin,fmz=fmz,
1.1123 + spec=spec,probl=_,meth=meth,env=env,loc=loc,
1.1124 + branch=branch,result=result,ostate=ostate}) =
1.1125 + PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl= x,
1.1126 + meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1.1127 + | repl_pbl _ _ = raise PTREE "repl_pbl takes no PrfObj";
1.1128 +fun repl_met x (PblObj {cell=cell,origin=origin,fmz=fmz,
1.1129 + spec=spec,probl=probl,meth=_,env=env,loc=loc,
1.1130 + branch=branch,result=result,ostate=ostate}) =
1.1131 + PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
1.1132 + meth= x,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1.1133 + | repl_met _ _ = raise PTREE "repl_pbl takes no PrfObj";
1.1134 +
1.1135 +fun repl_spec x (PblObj {cell=cell,origin=origin,fmz=fmz,
1.1136 + spec= _,probl=probl,meth=meth,env=env,loc=loc,
1.1137 + branch=branch,result=result,ostate=ostate}) =
1.1138 + PblObj {cell=cell,origin=origin,fmz=fmz,spec= x,probl=probl,
1.1139 + meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1.1140 + | repl_spec _ _ = raise PTREE "repl_domID takes no PrfObj";
1.1141 +fun repl_domID x (PblObj {cell=cell,origin=origin,fmz=fmz,
1.1142 + spec=(_,p,m),probl=probl,meth=meth,env=env,loc=loc,
1.1143 + branch=branch,result=result,ostate=ostate}) =
1.1144 + PblObj {cell=cell,origin=origin,fmz=fmz,spec=(x,p,m),probl=probl,
1.1145 + meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1.1146 + | repl_domID _ _ = raise PTREE "repl_domID takes no PrfObj";
1.1147 +fun repl_pblID x (PblObj {cell=cell,origin=origin,fmz=fmz,
1.1148 + spec=(d,_,m),probl=probl,meth=meth,env=env,loc=loc,
1.1149 + branch=branch,result=result,ostate=ostate}) =
1.1150 + PblObj {cell=cell,origin=origin,fmz=fmz,spec=(d,x,m),probl=probl,
1.1151 + meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1.1152 + | repl_pblID _ _ = raise PTREE "repl_pblID takes no PrfObj";
1.1153 +fun repl_metID x (PblObj {cell=cell,origin=origin,fmz=fmz,
1.1154 + spec=(d,p,_),probl=probl,meth=meth,env=env,loc=loc,
1.1155 + branch=branch,result=result,ostate=ostate}) =
1.1156 + PblObj {cell=cell,origin=origin,fmz=fmz,spec=(d,p,x),probl=probl,
1.1157 + meth=meth,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
1.1158 + | repl_metID _ _ = raise PTREE "repl_metID takes no PrfObj";
1.1159 +
1.1160 +fun repl_result l f' s (PrfObj {cell=cell,form=form,tac=tac,loc=_,
1.1161 + branch=branch,result = _ ,ostate = _}) =
1.1162 + PrfObj {cell=cell,form=form,tac=tac,loc= l,
1.1163 + branch=branch,result = f',ostate = s}
1.1164 + | repl_result l f' s (PblObj {cell=cell,origin=origin,fmz=fmz,
1.1165 + spec=spec,probl=probl,meth=meth,env=env,loc=_,
1.1166 + branch=branch,result= _ ,ostate= _}) =
1.1167 + PblObj {cell=cell,origin=origin,fmz=fmz,
1.1168 + spec=spec,probl=probl,meth=meth,env=env,loc= l,
1.1169 + branch=branch,result= f',ostate= s};
1.1170 +
1.1171 +fun repl_tac x (PrfObj {cell=cell,form=form,tac= _,loc=loc,
1.1172 + branch=branch,result=result,ostate=ostate}) =
1.1173 + PrfObj {cell=cell,form=form,tac= x,loc=loc,
1.1174 + branch=branch,result=result,ostate=ostate}
1.1175 + | repl_tac _ _ = raise PTREE "repl_tac takes no PblObj";
1.1176 +
1.1177 +fun repl_branch b (PblObj {cell=cell,origin=origin,fmz=fmz,
1.1178 + spec=spec,probl=probl,meth=meth,env=env,loc=loc,
1.1179 + branch= _,result=result,ostate=ostate}) =
1.1180 + PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
1.1181 + meth=meth,env=env,loc=loc,branch= b,result=result,ostate=ostate}
1.1182 + | repl_branch b (PrfObj {cell=cell,form=form,tac=tac,loc=loc,
1.1183 + branch= _,result=result,ostate=ostate}) =
1.1184 + PrfObj {cell=cell,form=form,tac=tac,loc=loc,
1.1185 + branch= b,result=result,ostate=ostate};
1.1186 +
1.1187 +fun repl_env e
1.1188 + (PblObj {cell=cell,origin=origin,fmz=fmz,
1.1189 + spec=spec,probl=probl,meth=meth,env=_,loc=loc,
1.1190 + branch=branch,result=result,ostate=ostate}) =
1.1191 + PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
1.1192 + meth=meth,env=e,loc=loc,branch=branch,
1.1193 + result=result,ostate=ostate}
1.1194 + | repl_env _ _ = raise PTREE "repl_ets takes no PrfObj";
1.1195 +
1.1196 +fun repl_oris oris
1.1197 + (PblObj {cell=cell,origin=(_,spe,hdf),fmz=fmz,
1.1198 + spec=spec,probl=probl,meth=meth,env=env,loc=loc,
1.1199 + branch=branch,result=result,ostate=ostate}) =
1.1200 + PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl,
1.1201 + meth=meth,env=env,loc=loc,branch=branch,
1.1202 + result=result,ostate=ostate}
1.1203 + | repl_oris _ _ = raise PTREE "repl_oris takes no PrfObj";
1.1204 +fun repl_orispec spe
1.1205 + (PblObj {cell=cell,origin=(oris,_,hdf),fmz=fmz,
1.1206 + spec=spec,probl=probl,meth=meth,env=env,loc=loc,
1.1207 + branch=branch,result=result,ostate=ostate}) =
1.1208 + PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl,
1.1209 + meth=meth,env=env,loc=loc,branch=branch,
1.1210 + result=result,ostate=ostate}
1.1211 + | repl_orispec _ _ = raise PTREE "repl_orispec takes no PrfObj";
1.1212 +
1.1213 +fun repl_loc l (PblObj {cell=cell,origin=origin,fmz=fmz,
1.1214 + spec=spec,probl=probl,meth=meth,env=env,loc=_,
1.1215 + branch=branch,result=result,ostate=ostate}) =
1.1216 + PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
1.1217 + meth=meth,env=env,loc=l,branch=branch,result=result,ostate=ostate}
1.1218 + | repl_loc l (PrfObj {cell=cell,form=form,tac=tac,loc=_,
1.1219 + branch=branch,result=result,ostate=ostate}) =
1.1220 + PrfObj {cell=cell,form=form,tac=tac,loc= l,
1.1221 + branch=branch,result=result,ostate=ostate};
1.1222 +(*
1.1223 +fun uni__cid cell'
1.1224 + (PblObj {cell=cell,origin=origin,fmz=fmz,
1.1225 + spec=spec,probl=probl,meth=meth,env=env,loc=loc,
1.1226 + branch=branch,result=result,ostate=ostate}) =
1.1227 + PblObj {cell=cell union cell',origin=origin,fmz=fmz,spec=spec,probl=probl,
1.1228 + meth=meth,env=env,loc=loc,branch=branch,
1.1229 + result=result,ostate=ostate}
1.1230 + | uni__cid cell'
1.1231 + (PrfObj {cell=cell,form=form,tac=tac,loc=loc,
1.1232 + branch=branch,result=result,ostate=ostate}) =
1.1233 + PrfObj {cell=cell union cell',form=form,tac=tac,loc=loc,
1.1234 + branch=branch,result=result,ostate=ostate};
1.1235 +*)
1.1236 +
1.1237 +(*WN050219 put here for interpreting code for cut_tree below...*)
1.1238 +type ocalhd =
1.1239 + bool * (*ALL itms+preconds true*)
1.1240 + pos_ * (*model belongs to Problem | Method*)
1.1241 + term * (*header: Problem... or Cas
1.1242 + FIXXXME.12.03: item! for marking syntaxerrors*)
1.1243 + itm list * (*model: given, find, relate*)
1.1244 + ((bool * term) list) *(*model: preconds*)
1.1245 + spec; (*specification*)
1.1246 +val e_ocalhd = (false, Und, e_term, [e_itm], [(false, e_term)], e_spec);
1.1247 +
1.1248 +datatype ptform =
1.1249 + Form of term
1.1250 + | ModSpec of ocalhd;
1.1251 +val e_ptform = Form e_term;
1.1252 +val e_ptform' = ModSpec e_ocalhd;
1.1253 +
1.1254 +
1.1255 +
1.1256 +(*.applies (snd f) to the branches at a pos if ((fst f) b),
1.1257 + f : (ppobj -> bool) * (int -> ptree list -> ptree list).*)
1.1258 +
1.1259 +fun appl_branch f EmptyPtree [] = (EmptyPtree, false)
1.1260 + | appl_branch f EmptyPtree _ = raise PTREE "appl_branch f Empty _"
1.1261 + | appl_branch f (Nd ( _, _)) [] = raise PTREE "appl_branch f _ []"
1.1262 + | appl_branch f (Nd (b, bs)) (p::[]) =
1.1263 + if (fst f) b then (Nd (b, (snd f) (p:posel) bs), true)
1.1264 + else (Nd (b, bs), false)
1.1265 + | appl_branch f (Nd (b, bs)) (p::ps) =
1.1266 + let val (b',bool) = appl_branch f (nth p bs) ps
1.1267 + in (Nd (b, repl_app bs p b'), bool) end;
1.1268 +
1.1269 +(* for cut_level; appl_branch(deprecated) *)
1.1270 +fun test_trans (PrfObj{branch = Transitive,...}) = true
1.1271 + | test_trans (PblObj{branch = Transitive,...}) = true
1.1272 + | test_trans _ = false;
1.1273 +
1.1274 +fun is_pblobj' pt (p:pos) =
1.1275 + let val ppobj = get_obj I pt p
1.1276 + in is_pblobj ppobj end;
1.1277 +
1.1278 +
1.1279 +fun delete_result pt (p:pos) =
1.1280 + (appl_obj (repl_result (fst (get_obj g_loc pt p), None)
1.1281 + (e_term,[]) Incomplete) pt p);
1.1282 +
1.1283 +fun del_res (PblObj {cell, fmz, origin, spec, probl, meth,
1.1284 + env, loc=(l1,_), branch, result, ostate}) =
1.1285 + PblObj {cell=cell,fmz=fmz,origin=origin,spec=spec,probl=probl,meth=meth,
1.1286 + env=env, loc=(l1,None), branch=branch, result=(e_term,[]),
1.1287 + ostate=Incomplete}
1.1288 +
1.1289 + | del_res (PrfObj {cell, form, tac, loc=(l1,_), branch, result, ostate}) =
1.1290 + PrfObj {cell=cell,form=form,tac=tac, loc=(l1,None), branch=branch,
1.1291 + result=(e_term,[]), ostate=Incomplete};
1.1292 +
1.1293 +
1.1294 +(*
1.1295 +fun update_fmz pt pos x = appl_obj (repl_fmz x) pt pos;
1.1296 + 1.00 not used anymore*)
1.1297 +
1.1298 +(*FIXME.WN.12.03: update_X X pos pt -> pt could be chained by o (efficiency?)*)
1.1299 +fun update_env pt pos x = appl_obj (repl_env x) pt pos;
1.1300 +fun update_domID pt pos x = appl_obj (repl_domID x) pt pos;
1.1301 +fun update_pblID pt pos x = appl_obj (repl_pblID x) pt pos;
1.1302 +fun update_metID pt pos x = appl_obj (repl_metID x) pt pos;
1.1303 +fun update_spec pt pos x = appl_obj (repl_spec x) pt pos;
1.1304 +
1.1305 +fun update_pbl pt pos x = appl_obj (repl_pbl x) pt pos;
1.1306 +fun update_pblppc pt pos x = appl_obj (repl_pbl x) pt pos;
1.1307 +
1.1308 +fun update_met pt pos x = appl_obj (repl_met x) pt pos;
1.1309 +(*1.09.01 ----
1.1310 +fun update_metppc pt pos x =
1.1311 + let val {rew_ord'=od,rls'=rs,asm_thm=at,asm_rls=ar,...} =
1.1312 + get_obj g_met pt pos
1.1313 + in appl_obj (repl_met
1.1314 + {rew_ord'=od,rls'=rs,asm_thm=at,asm_rls=ar,ppc=x})
1.1315 + pt pos end;*)
1.1316 +fun update_metppc pt pos x = appl_obj (repl_met x) pt pos;
1.1317 +
1.1318 +(*fun union_cid pt pos x = appl_obj (uni__cid x) pt pos;*)
1.1319 +
1.1320 +fun update_branch pt pos x = appl_obj (repl_branch x) pt pos;
1.1321 +fun update_tac pt pos x = appl_obj (repl_tac x) pt pos;
1.1322 +
1.1323 +fun update_oris pt pos x = appl_obj (repl_oris x) pt pos;
1.1324 +fun update_orispec pt pos x = appl_obj (repl_orispec x) pt pos;
1.1325 +
1.1326 + (*done by append_* !! 3.5.02; ununsed WN050305 thus outcommented
1.1327 +fun update_loc pt (p,_) (ScrState ([],[],None,
1.1328 + Const ("empty",_),Sundef,false)) =
1.1329 + appl_obj (repl_loc (None,None)) pt p
1.1330 + | update_loc pt (p,Res) x =
1.1331 + let val (lform,_) = get_obj g_loc pt p
1.1332 + in appl_obj (repl_loc (lform,Some x)) pt p end
1.1333 +
1.1334 + | update_loc pt (p,_) x =
1.1335 + let val (_,lres) = get_obj g_loc pt p
1.1336 + in appl_obj (repl_loc (Some x,lres)) pt p end;-------------*)
1.1337 +
1.1338 +(*WN050305 for handling cut_tree in cappend_atomic -- TODO redesign !*)
1.1339 +fun update_loc' pt p iss = appl_obj (repl_loc iss) pt p;
1.1340 +
1.1341 +(*13.8.02---------------------------
1.1342 +fun get_loc EmptyPtree _ = None
1.1343 + | get_loc pt (p,Res) =
1.1344 + let val (lfrm,lres) = get_obj g_loc pt p
1.1345 + in if lres = e_istate then lfrm else lres end
1.1346 + | get_loc pt (p,_) =
1.1347 + let val (lfrm,lres) = get_obj g_loc pt p
1.1348 + in if lfrm = e_istate then lres else lfrm end; 5.10.00: too liberal ?*)
1.1349 +(*13.8.02: options, because istate is no equalitype any more*)
1.1350 +fun get_loc EmptyPtree _ = e_istate
1.1351 + | get_loc pt (p,Res) =
1.1352 + (case get_obj g_loc pt p of
1.1353 + (Some i, None) => i
1.1354 + | (None , None) => e_istate
1.1355 + | (_ , Some i) => i)
1.1356 + | get_loc pt (p,_) =
1.1357 + (case get_obj g_loc pt p of
1.1358 + (None , Some i) => i (*13.8.02 just copied from ^^^: too liberal ?*)
1.1359 + | (None , None) => e_istate
1.1360 + | (Some i, _) => i);
1.1361 +val get_istate = get_loc; (*3.5.02*)
1.1362 +
1.1363 +(*.collect the assumptions within a problem up to a certain position.*)
1.1364 +type asms = (term * pos) list;(*WN0502 should be (pos' * term) list
1.1365 + ...........===^===*)
1.1366 +
1.1367 +fun get_asm (b:pos, p:pos) (Nd (PblObj {result=(_,asm),...},_)) =
1.1368 + ((*writeln ("### get_asm PblObj:(b,p)= "^
1.1369 + (pair2str(ints2str b, ints2str p)));*)
1.1370 + (map (rpair b) asm):asms)
1.1371 + | get_asm (b, p) (Nd (PrfObj {result=(_,asm),...}, [])) =
1.1372 + ((*writeln ("### get_asm PrfObj []:(b,p)= "^
1.1373 + (pair2str(ints2str b, ints2str p)));*)
1.1374 + (map (rpair b) asm))
1.1375 + | get_asm (b, p:pos) (Nd (PrfObj _, nds)) =
1.1376 + let (*val _= writeln ("### get_asm PrfObj nds:(b,p)= "^
1.1377 + (pair2str(ints2str b, ints2str p)));*)
1.1378 + val levdn =
1.1379 + if p <> [] then (b @ [hd p]:pos, tl p:pos)
1.1380 + else (b @ [1], [99999]) (*_deeper_ nesting is always _before_ p*)
1.1381 + in gets_asm levdn 1 nds end
1.1382 +and gets_asm _ _ [] = []
1.1383 + | gets_asm (b, p' as p::ps) i (nd::nds) =
1.1384 + if p < i then []
1.1385 + else ((*writeln ("### gets_asm: (b,p')= "^(pair2str(ints2str b,
1.1386 + ints2str p')));*)
1.1387 + (get_asm (b @ [i], ps) nd) @ (gets_asm (b, p') (i + 1) nds));
1.1388 +
1.1389 +fun get_assumptions_ (Nd (PblObj {result=(r,asm),...}, cn)) (([], _):pos') =
1.1390 + if r = e_term then gets_asm ([], [99999]) 1 cn
1.1391 + else map (rpair []) asm
1.1392 + | get_assumptions_ pt (p,p_) =
1.1393 + let val (cn, base) = par_children pt p
1.1394 + val offset = drop (length base, p)
1.1395 + val base' = replicate (length base) 1
1.1396 + val offset' = case p_ of
1.1397 + Frm => let val (qs,q) = split_last offset
1.1398 + in qs @ [q - 1] end
1.1399 + | _ => offset
1.1400 + (*val _= writeln ("... get_assumptions: (b,o)= "^
1.1401 + (pair2str(ints2str base',ints2str offset)))*)
1.1402 + in gets_asm (base', offset) 1 cn end;
1.1403 +
1.1404 +
1.1405 +(*---------
1.1406 +end
1.1407 +
1.1408 +open Ptree;
1.1409 +----------*)
1.1410 +
1.1411 +(*pos of the formula on FE relative to the current pos,
1.1412 + which is the next writepos*)
1.1413 +fun pre_pos ([]:pos) = []:pos
1.1414 + | pre_pos pp =
1.1415 + let val (ps,p) = split_last pp
1.1416 + in case p of 1 => ps | n => ps @ [n-1] end;
1.1417 +
1.1418 +(*WN.20.5.03 ... but not used*)
1.1419 +fun posless [] (_::_) = true
1.1420 + | posless (_::_) [] = false
1.1421 + | posless (p::ps) (q::qs) = if p = q then posless ps qs else p < q;
1.1422 +(* posless [2,3,4] [3,4,5];
1.1423 +true
1.1424 +> posless [2,3,4] [1,2,3];
1.1425 +false
1.1426 +> posless [2,3] [2,3,4];
1.1427 +true
1.1428 +> posless [2,3,4] [2,3];
1.1429 +false
1.1430 +> posless [6] [6,5,2];
1.1431 +true
1.1432 ++++ see Isabelle/../library.ML*)
1.1433 +
1.1434 +
1.1435 +(**.development for extracting an 'interval' from ptree.**)
1.1436 +
1.1437 +(*version 1 stopped 8.03 in favour of get_interval with !!!move_dn
1.1438 + actually used (inefficient) version with move_dn: see modspec.sml*)
1.1439 +local
1.1440 +
1.1441 +fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*)
1.1442 +fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*)
1.1443 +fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x;
1.1444 +fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;
1.1445 +
1.1446 +fun getnd i (b,p) q (Nd (po, nds)) =
1.1447 + (if i <= 0 then [[b]] else []) @
1.1448 + (getnds (i-1) true (b@[hdp p], tlp p) (tlq q)
1.1449 + (take_fromto (hdp p) (hdq q) nds))
1.1450 +
1.1451 +and getnds _ _ _ _ [] = [] (*no children*)
1.1452 + | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*)
1.1453 +
1.1454 + | getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*)
1.1455 + (getnd i ( b, p ) [99999] n1) @
1.1456 + (getnd ~99999 (lev_on b,[0]) q n2)
1.1457 +
1.1458 + | getnds i _ (b,p) q [n1, n2] = (*intern, r-margin*)
1.1459 + (getnd i ( b,[0]) [99999] n1) @
1.1460 + (getnd ~99999 (lev_on b,[0]) q n2)
1.1461 +
1.1462 + | getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*)
1.1463 + (getnd i ( b, p ) [99999] nd) @
1.1464 + (getnds ~99999 false (lev_on b,[0]) q nds)
1.1465 +
1.1466 + | getnds i _ (b,p) q (nd::(nds as _::_)) = (*intern, ...*)
1.1467 + (getnd i ( b,[0]) [99999] nd) @
1.1468 + (getnds ~99999 false (lev_on b,[0]) q nds);
1.1469 +in
1.1470 +(*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes
1.1471 + where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
1.1472 +(1) the 'f' are given
1.1473 +(1a) by 'from' if 'f' = the respective element of 'from' (left margin)
1.1474 +(1b) -inifinity, if 'f' > the respective element of 'from' (internal node)
1.1475 +(2) the 't' ar given
1.1476 +(2a) by 'to' if 't' = the respective element of 'to' (right margin)
1.1477 +(2b) inifinity, if 't' < the respective element of 'to (internal node)'
1.1478 +the 'f' and 't' are set by hdp,... *)
1.1479 +fun get_trace pt p q =
1.1480 + (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q)))
1.1481 + (take_fromto (hdp p) (hdq q) (children pt));
1.1482 +end;
1.1483 +(*WN0510 stoppde this development;
1.1484 + actually used (inefficient) version with move_dn: getFormulaeFromTo*)
1.1485 +
1.1486 +
1.1487 +
1.1488 +
1.1489 +fun get_somespec ((dI,pI,mI):spec) ((dI',pI',mI'):spec) =
1.1490 + let val domID = if dI = e_domID
1.1491 + then if dI' = e_domID
1.1492 + then raise error"pt_extract: no domID in probl,origin"
1.1493 + else dI'
1.1494 + else dI
1.1495 + val pblID = if pI = e_pblID
1.1496 + then if pI' = e_pblID
1.1497 + then raise error"pt_extract: no pblID in probl,origin"
1.1498 + else pI'
1.1499 + else pI
1.1500 + val metID = if mI = e_metID
1.1501 + then if pI' = e_metID
1.1502 + then raise error"pt_extract: no metID in probl,origin"
1.1503 + else mI'
1.1504 + else mI
1.1505 + in (domID, pblID, metID):spec end;
1.1506 +fun get_somespec' ((dI,pI,mI):spec) ((dI',pI',mI'):spec) =
1.1507 + let val domID = if dI = e_domID then dI' else dI
1.1508 + val pblID = if pI = e_pblID then pI' else pI
1.1509 + val metID = if mI = e_metID then mI' else mI
1.1510 + in (domID, pblID, metID):spec end;
1.1511 +
1.1512 +(*extract a formula or model from ptree for itms2itemppc or model2xml*)
1.1513 +fun preconds2str bts =
1.1514 + (strs2str o (map (linefeed o pair2str o
1.1515 + (apsnd term2str) o
1.1516 + (apfst bool2str)))) bts;
1.1517 +fun ocalhd2str ((b, p, hdf, itms, prec, spec):ocalhd) =
1.1518 + "("^bool2str b^", "^pos_2str p^", "^term2str hdf^
1.1519 + ", "^itms2str (assoc_thy "Isac.thy") itms^
1.1520 + ", "^preconds2str prec^", \n"^spec2str spec^" )";
1.1521 +
1.1522 +
1.1523 +
1.1524 +fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj;
1.1525 +
1.1526 +
1.1527 +(**.functions for the 'ptree iterator' as seen from the FE-Kernel interface.**)
1.1528 +
1.1529 +(*move one step down into existing nodes of ptree; regard TransitiveB
1.1530 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~##################
1.1531 +fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*)
1.1532 +(* val (Nd (c, ns), ([],p_)) = (pt, get_pos cI uI);
1.1533 + *)
1.1534 + if is_pblobj c
1.1535 + then case p_ of (*Frm => ([], Pbl) 1.12.03
1.1536 + |*) Res => raise PTREE "move_dn: end of calculation"
1.1537 + | _ => if null ns (*go down from Pbl + Met*)
1.1538 + then raise PTREE "move_dn: solve problem not started"
1.1539 + else ([1], Frm)
1.1540 + else (case p_ of Res => raise PTREE "move_dn: end of (sub-)tree"
1.1541 + | _ => if null ns
1.1542 + then raise PTREE "move_dn: pos not existent 1"
1.1543 + else ([1], Frm))
1.1544 +
1.1545 + (*iterate towards end of pos*)
1.1546 +(* val (P,(Nd (_, ns)),(p::(ps as (_::_)),p_)) = ([]:pos, pt, get_pos cI uI);
1.1547 + val (P,(Nd (_, ns)),(p::(ps as (_::_)),p_)) = ((P@[p]),(nth p ns),(ps, p_));
1.1548 + *)
1.1549 + | move_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
1.1550 + if p > length ns then raise PTREE "move_dn: pos not existent 2"
1.1551 + else move_dn ((P@[p]): pos) (nth p ns) (ps, p_)
1.1552 +(* val (P, (Nd (c, ns)), ([p], p_)) = ((P@[p]), (nth p ns), (ps, p_));
1.1553 + val (P, (Nd (c, ns)), ([p], p_)) = ([],pt,get_pos cI uI);
1.1554 + *)
1.1555 + | move_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1.1556 + if p > length ns then raise PTREE "move_dn: pos not existent 3"
1.1557 + else if is_pblnd (nth p ns) then
1.1558 + ((*writeln("### move_dn: is_pblnd (nth p ns), P= "^ints2str' P^", \n"^
1.1559 + "length ns= "^((string_of_int o length) ns)^
1.1560 + ", p= "^string_of_int p^", p_= "^pos_2str p_);*)
1.1561 + case p_ of Res => if p = length ns
1.1562 + then if g_ostate c = Complete then (P, Res)
1.1563 + else raise PTREE (ints2str' P^" not complete")
1.1564 + (*FIXME here handle not-sequent-branches*)
1.1565 + else if g_branch c = TransitiveB
1.1566 + andalso (not o is_pblnd o (nth (p+1))) ns
1.1567 + then (P@[p+1], Res)
1.1568 + else (P@[p+1], if is_pblnd (nth (p+1) ns)
1.1569 + then Pbl else Frm)
1.1570 + | _ => if (null o children o (nth p)) ns (*go down from Pbl*)
1.1571 + then raise PTREE "move_dn: solve subproblem not started"
1.1572 + else (P @ [p, 1],
1.1573 + if (is_pblnd o hd o children o (nth p)) ns
1.1574 + then Pbl else Frm)
1.1575 + )
1.1576 + (* val (P, Nd (c, ns), ([p], p_)) = ([], pt, ([1], Frm));
1.1577 + *)
1.1578 + else case p_ of Frm => if (null o children o (nth p)) ns
1.1579 + (*then if g_ostate c = Complete then (P@[p],Res)*)
1.1580 + then if g_ostate' (nth p ns) = Complete
1.1581 + then (P@[p],Res)
1.1582 + else raise PTREE "move_dn: pos not existent 4"
1.1583 + else (P @ [p, 1], (*go down*)
1.1584 + if (is_pblnd o hd o children o (nth p)) ns
1.1585 + then Pbl else Frm)
1.1586 + | Res => if p = length ns
1.1587 + then
1.1588 + if g_ostate c = Complete then (P, Res)
1.1589 + else raise PTREE (ints2str' P^" not complete")
1.1590 + else
1.1591 + if g_branch c = TransitiveB
1.1592 + andalso (not o is_pblnd o (nth (p+1))) ns
1.1593 + then if (null o children o (nth (p+1))) ns
1.1594 + then (P@[p+1], Res)
1.1595 + else (P@[p+1,1], Frm)(*040221*)
1.1596 + else (P@[p+1], if is_pblnd (nth (p+1) ns)
1.1597 + then Pbl else Frm);
1.1598 +*)
1.1599 +(*.move one step down into existing nodes of ptree; skip Res = Frm.nxt;
1.1600 + move_dn at the end of the calc-tree raises PTREE.*)
1.1601 +fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*)
1.1602 + (case p_ of
1.1603 + Res => raise PTREE "move_dn: end of calculation"
1.1604 + | _ => if null ns (*go down from Pbl + Met*)
1.1605 + then raise PTREE "move_dn: solve problem not started"
1.1606 + else ([1], Frm))
1.1607 + | move_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =(*iterate to end of pos*)
1.1608 + if p > length ns then raise PTREE "move_dn: pos not existent 2"
1.1609 + else move_dn ((P@[p]): pos) (nth p ns) (ps, p_)
1.1610 +
1.1611 + | move_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1.1612 + if p > length ns then raise PTREE "move_dn: pos not existent 3"
1.1613 + else case p_ of
1.1614 + Res =>
1.1615 + if p = length ns (*last Res on this level: go a level up*)
1.1616 + then if g_ostate c = Complete then (P, Res)
1.1617 + else raise PTREE (ints2str' P^" not complete 1")
1.1618 + else (*go to the next Nd on this level, or down into the next Nd*)
1.1619 + if is_pblnd (nth (p+1) ns) then (P@[p+1], Pbl)
1.1620 + else
1.1621 + if g_res' (nth p ns) = g_form' (nth (p+1) ns)
1.1622 + then if (null o children o (nth (p+1))) ns
1.1623 + then (*take the Res if Complete*)
1.1624 + if g_ostate' (nth (p+1) ns) = Complete
1.1625 + then (P@[p+1], Res)
1.1626 + else raise PTREE (ints2str' (P@[p+1])^
1.1627 + " not complete 2")
1.1628 + else (P@[p+1,1], Frm)(*go down into the next PrfObj*)
1.1629 + else (P@[p+1], Frm)(*take Frm: exists if the Nd exists*)
1.1630 + | Frm => (*go down or to the Res of this Nd*)
1.1631 + if (null o children o (nth p)) ns
1.1632 + then if g_ostate' (nth p ns) = Complete then (P @ [p], Res)
1.1633 + else raise PTREE (ints2str' (P @ [p])^" not complete 3")
1.1634 + else (P @ [p, 1], Frm)
1.1635 + | _ => (*is Pbl or Met*)
1.1636 + if (null o children o (nth p)) ns
1.1637 + then raise PTREE "move_dn:solve subproblem not startd"
1.1638 + else (P @ [p, 1],
1.1639 + if (is_pblnd o hd o children o (nth p)) ns
1.1640 + then Pbl else Frm);
1.1641 +
1.1642 +
1.1643 +(*.go one level down into ptree.*)
1.1644 +fun movelevel_dn [] (Nd (c, ns)) ([],p_) = (*root problem*)
1.1645 + if is_pblobj c
1.1646 + then if null ns
1.1647 + then raise PTREE "solve problem not started"
1.1648 + else ([1], if (is_pblnd o hd) ns then Pbl else Frm)
1.1649 + else raise PTREE "pos not existent 1"
1.1650 +
1.1651 + (*iterate towards end of pos*)
1.1652 + | movelevel_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
1.1653 + if p > length ns then raise PTREE "pos not existent 2"
1.1654 + else movelevel_dn (P@[p]) (nth p ns) (ps, p_)
1.1655 +
1.1656 + | movelevel_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1.1657 + if p > length ns then raise PTREE "pos not existent 3" else
1.1658 + case p_ of Res =>
1.1659 + if p = length ns
1.1660 + then raise PTREE "no children"
1.1661 + else
1.1662 + if g_branch c = TransitiveB
1.1663 + then if (null o children o (nth (p+1))) ns
1.1664 + then raise PTREE "no children"
1.1665 + else (P @ [p+1, 1],
1.1666 + if (is_pblnd o hd o children o (nth (p+1))) ns
1.1667 + then Pbl else Frm)
1.1668 + else if (null o children o (nth p)) ns
1.1669 + then raise PTREE "no children"
1.1670 + else (P @ [p, 1], if (is_pblnd o hd o children o (nth p)) ns
1.1671 + then Pbl else Frm)
1.1672 + | _ => if (null o children o (nth p)) ns
1.1673 + then raise PTREE "no children"
1.1674 + else (P @ [p, 1], (*go down*)
1.1675 + if (is_pblnd o hd o children o (nth p)) ns
1.1676 + then Pbl else Frm);
1.1677 +
1.1678 +
1.1679 +
1.1680 +(*.go to the previous position in ptree; regard TransitiveB.*)
1.1681 +fun move_up _ (Nd (c, ns)) (([],p_):pos') = (*root problem*)
1.1682 + if is_pblobj c
1.1683 + then case p_ of Res => if null ns then ([], Pbl) (*Res -> Pbl (not Met)!*)
1.1684 + else ([length ns], Res)
1.1685 + | _ => raise PTREE "begin of calculation"
1.1686 + else raise PTREE "pos not existent"
1.1687 +
1.1688 + | move_up P (Nd (_, ns)) (p::(ps as (_::_)),p_) = (*iterate to end of pos*)
1.1689 + if p > length ns then raise PTREE "pos not existent"
1.1690 + else move_up (P@[p]) (nth p ns) (ps,p_)
1.1691 +
1.1692 + | move_up P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1.1693 + if p > length ns then raise PTREE "pos not existent"
1.1694 + else if is_pblnd (nth p ns) then
1.1695 + case p_ of Res =>
1.1696 + let val nc = (length o children o (nth p)) ns
1.1697 + in if nc = 0 then (P@[p], Pbl) (*Res -> Pbl (not Met)!*)
1.1698 + else (P @ [p, nc], Res) end (*go down*)
1.1699 + | _ => if p = 1 then (P, Pbl) else (P@[p-1], Res)
1.1700 + else case p_ of Frm => if p <> 1 then (P, Frm)
1.1701 + else if is_pblobj c then (P, Pbl) else (P, Frm)
1.1702 + | Res =>
1.1703 + let val nc = (length o children o (nth p)) ns
1.1704 + in if nc = 0 (*cannot go down*)
1.1705 + then if g_branch c = TransitiveB andalso p <> 1
1.1706 + then (P@[p-1], Res) else (P@[p], Frm)
1.1707 + else (P @ [p, nc], Res) end; (*go down*)
1.1708 +
1.1709 +
1.1710 +
1.1711 +(*.go one level up in ptree; sets the position on Frm.*)
1.1712 +fun movelevel_up _ (Nd (c, ns)) (([],p_):pos') = (*root problem*)
1.1713 + raise PTREE "pos not existent"
1.1714 +
1.1715 + (*iterate towards end of pos*)
1.1716 + | movelevel_up P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
1.1717 + if p > length ns then raise PTREE "pos not existent"
1.1718 + else movelevel_up (P@[p]) (nth p ns) (ps,p_)
1.1719 +
1.1720 + | movelevel_up P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*)
1.1721 + if p > length ns then raise PTREE "pos not existent"
1.1722 + else if is_pblobj c then (P, Pbl) else (P, Frm);
1.1723 +
1.1724 +
1.1725 +(*.go to the next calc-head up in the calc-tree.*)
1.1726 +fun movecalchd_up pt ((p, Res):pos') =
1.1727 + (par_pblobj pt p, Pbl):pos'
1.1728 + | movecalchd_up pt (p, _) =
1.1729 + if is_pblobj (get_obj I pt p)
1.1730 + then (p, Pbl) else (par_pblobj pt p, Pbl);
1.1731 +
1.1732 +(*.determine the previous pos' on the same level.*)
1.1733 +(*WN0502 made for interSteps; _only_ works for branch TransitiveB*)
1.1734 +fun lev_pred' pt (pos:pos' as ([],Res)) = ([],Pbl):pos'
1.1735 + | lev_pred' pt (pos:pos' as (p, Res)) =
1.1736 + let val (p', last) = split_last p
1.1737 + in if last = 1
1.1738 + then if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm)
1.1739 + else if get_obj g_res pt (p' @ [last - 1]) = get_obj g_form pt p
1.1740 + then (p' @ [last - 1], Res) (*TransitiveB*)
1.1741 + else if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm)
1.1742 + end;
1.1743 +
1.1744 +(*.determine the next pos' on the same level.*)
1.1745 +fun lev_on' pt (([],Pbl):pos') = ([],Res):pos'
1.1746 + | lev_on' pt (p, Res) =
1.1747 + if get_obj g_res pt p = get_obj g_form pt (lev_on p)(*TransitiveB*)
1.1748 + then if existpt' (lev_on p, Res) pt then (lev_on p, Res)
1.1749 + else raise error ("lev_on': (p, Res) -> (p, Res) not existent, \
1.1750 + \p = "^ints2str' (lev_on p))
1.1751 + else (lev_on p, Frm)
1.1752 + | lev_on' pt (p, _) =
1.1753 + if existpt' (p, Res) pt then (p, Res)
1.1754 + else raise error ("lev_on': (p, Frm) -> (p, Res) not existent, \
1.1755 + \p = "^ints2str' p);
1.1756 +
1.1757 +fun exist_lev_on' pt p = (lev_on' pt p; true) handle _ => false;
1.1758 +
1.1759 +(*.is the pos' at the last element of a calulation _AND_ can be continued.*)
1.1760 +(* val (pt, pos as (p,p_)) = (pt, ([1],Frm));
1.1761 + *)
1.1762 +fun is_curr_endof_calc pt (([],Res) : pos') = false
1.1763 + | is_curr_endof_calc pt (pos as (p,_)) =
1.1764 + not (exist_lev_on' pt pos)
1.1765 + andalso get_obj g_ostate pt (lev_up p) = Incomplete;
1.1766 +
1.1767 +
1.1768 +(**.insert into ctree and cut branches accordingly.**)
1.1769 +
1.1770 +(*.get all positions of certain intervals on the ctree.*)
1.1771 +(*OLD VERSION without move_dn; kept for occasional redesign
1.1772 + get all pos's to be cut in a ptree
1.1773 + below a pos or from a ptree list after i-th element (NO level_up).*)
1.1774 +fun get_allpos' (_:pos, _:posel) EmptyPtree = ([]:pos' list)
1.1775 + | get_allpos' (p, 1) (Nd (b, bs)) = (*p is pos of Nd*)
1.1776 + if g_ostate b = Incomplete
1.1777 + then ((*writeln("get_allpos' (p, 1) Incomplete: p="^ints2str' p);*)
1.1778 + [(p,Frm)] @ (get_allpos's (p, 1) bs)
1.1779 + )
1.1780 + else ((*writeln("get_allpos' (p, 1) else: p="^ints2str' p);*)
1.1781 + [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p,Res)]
1.1782 + )
1.1783 + (*WN041020 here we assume what is presented on the worksheet ?!*)
1.1784 + | get_allpos' (p, i) (Nd (b, bs)) = (*p is pos of Nd*)
1.1785 + if length bs > 0 orelse is_pblobj b
1.1786 + then if g_ostate b = Incomplete
1.1787 + then [(p,Frm)] @ (get_allpos's (p, 1) bs)
1.1788 + else [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p,Res)]
1.1789 + else
1.1790 + if g_ostate b = Incomplete
1.1791 + then []
1.1792 + else [(p,Res)]
1.1793 +(*WN041020 here we assume what is presented on the worksheet ?!*)
1.1794 +and get_allpos's _ [] = []
1.1795 + | get_allpos's (p, i) (pt::pts) = (*p is pos of parent-Nd*)
1.1796 + (get_allpos' (p@[i], i) pt) @ (get_allpos's (p, i+1) pts);
1.1797 +
1.1798 +(*.get all positions of certain intervals on the ctree.*)
1.1799 +(*NEW version WN050225*)
1.1800 +
1.1801 +
1.1802 +(*.cut branches.*)
1.1803 +(*before WN041019......
1.1804 +val cut_branch = (test_trans, curry take):
1.1805 + (ppobj -> bool) * (int -> ptree list -> ptree list);
1.1806 +.. formlery used for ...
1.1807 +fun cut_tree''' _ [] = EmptyPtree
1.1808 + | cut_tree''' pt pos =
1.1809 + let val (pt',cut) = appl_branch cut_branch pt pos
1.1810 + in if cut andalso length pos > 1 then cut_tree''' pt' (lev_up pos)
1.1811 + else pt' end;
1.1812 +*)
1.1813 +(*OLD version before WN050225*)
1.1814 +(*WN050106 like cut_level, but deletes exactly 1 node --- for tests ONLY*)
1.1815 +fun cut_level_'_ (_:pos' list) (_:pos) EmptyPtree (_:pos') =
1.1816 + raise PTREE "cut_level_'_ Empty _"
1.1817 + | cut_level_'_ _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level_'_ _ []"
1.1818 + | cut_level_'_ cuts P (Nd (b, bs)) (p::[],p_) =
1.1819 + if test_trans b
1.1820 + then (Nd (b, drop_nth [] (p:posel, bs)),
1.1821 + (* ~~~~~~~~~~~*)
1.1822 + cuts @
1.1823 + (if p_ = Frm then [(P@[p],Res)] else ([]:pos' list)) @
1.1824 + (*WN041020 here we assume what is presented on the worksheet ?!*)
1.1825 + (get_allpos's (P, p+1) (drop_nth [] (p, bs))))
1.1826 + (* ~~~~~~~~~~~*)
1.1827 + else (Nd (b, bs), cuts)
1.1828 + | cut_level_'_ cuts P (Nd (b, bs)) ((p::ps),p_) =
1.1829 + let val (bs',cuts') = cut_level_'_ cuts P (nth p bs) (ps, p_)
1.1830 + in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
1.1831 +
1.1832 +(*before WN050219*)
1.1833 +fun cut_level (_:pos' list) (_:pos) EmptyPtree (_:pos') =
1.1834 + raise PTREE "cut_level EmptyPtree _"
1.1835 + | cut_level _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level _ []"
1.1836 +
1.1837 + | cut_level cuts P (Nd (b, bs)) (p::[],p_) =
1.1838 + if test_trans b
1.1839 + then (Nd (b, take (p:posel, bs)),
1.1840 + cuts @
1.1841 + (if p_ = Frm andalso (*#*) g_ostate b = Complete
1.1842 + then [(P@[p],Res)] else ([]:pos' list)) @
1.1843 + (*WN041020 here we assume what is presented on the worksheet ?!*)
1.1844 + (get_allpos's (P, p+1) (takerest (p, bs))))
1.1845 + else (Nd (b, bs), cuts)
1.1846 +
1.1847 + | cut_level cuts P (Nd (b, bs)) ((p::ps),p_) =
1.1848 + let val (bs',cuts') = cut_level cuts P (nth p bs) (ps, p_)
1.1849 + in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
1.1850 +
1.1851 +(*OLD version before WN050219, overwritten below*)
1.1852 +fun cut_tree _ (([],_):pos') = raise PTREE "cut_tree _ ([],_)"
1.1853 + | cut_tree pt (pos as ([p],_)) =
1.1854 + let val (pt', cuts) = cut_level ([]:pos' list) [] pt pos
1.1855 + in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
1.1856 + then [] else [([],Res)])) end
1.1857 + | cut_tree pt (p,p_) =
1.1858 + let
1.1859 + fun cutfn pt cuts (p,p_) =
1.1860 + let val (pt', cuts') = cut_level [] (lev_up p) pt (p,p_)
1.1861 + val cuts'' = if get_obj g_ostate pt (lev_up p) = Incomplete
1.1862 + then [] else [(lev_up p, Res)]
1.1863 + in if length cuts' > 0 andalso length p > 1
1.1864 + then cutfn pt' (cuts @ cuts') (lev_up p, Frm(*-->(p,Res)*))
1.1865 + else (pt',cuts @ cuts') end
1.1866 + val (pt', cuts) = cutfn pt [] (p,p_)
1.1867 + in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
1.1868 + then [] else [([], Res)])) end;
1.1869 +
1.1870 +
1.1871 +(*########/ inserted from ctreeNEW.sml \#################################**)
1.1872 +
1.1873 +(*.get all positions in a ptree until ([],Res) or ostate=Incomplete
1.1874 +val get_allp = fn :
1.1875 + pos' list -> : accumulated, start with []
1.1876 + pos -> : the offset for subtrees wrt the root
1.1877 + ptree -> : (sub)tree
1.1878 + pos' : initialization (the last pos' before ...)
1.1879 + -> pos' list : of positions in this (sub) tree (relative to the root)
1.1880 +.*)
1.1881 +(* val (cuts, P, pt, pos) = ([], [3], get_nd pt [3], ([], Frm):pos');
1.1882 + val (cuts, P, pt, pos) = ([], [2], get_nd pt [2], ([], Frm):pos');
1.1883 + length (children pt);
1.1884 + *)
1.1885 +fun get_allp (cuts:pos' list) (P:pos, pos:pos') pt =
1.1886 + (let val nxt = move_dn [] pt pos (*exn if Incomplete reached*)
1.1887 + in if nxt <> ([],Res)
1.1888 + then get_allp (cuts @ [nxt]) (P, nxt) pt
1.1889 + else (map (apfst (curry op@ P)) (cuts @ [nxt])): pos' list
1.1890 + end) handle PTREE _ => (map (apfst (curry op@ P)) cuts);
1.1891 +
1.1892 +
1.1893 +(*the pts are assumed to be on the same level*)
1.1894 +fun get_allps (cuts: pos' list) (P:pos) [] = cuts
1.1895 + | get_allps cuts P (pt::pts) =
1.1896 + let val below = get_allp [] (P, ([], Frm)) pt
1.1897 + val levfrm =
1.1898 + if is_pblnd pt
1.1899 + then (P, Pbl)::below
1.1900 + else if last_elem P = 1
1.1901 + then (P, Frm)::below
1.1902 + else (*Trans*) below
1.1903 + val levres = levfrm @ (if null below then [(P, Res)] else [])
1.1904 + in get_allps (cuts @ levres) (lev_on P) pts end;
1.1905 +
1.1906 +
1.1907 +(**.these 2 funs decide on how far cut_tree goes.**)
1.1908 +(*.shall the nodes _after_ the pos to be inserted at be deleted?.*)
1.1909 +fun test_trans (PrfObj{branch = Transitive,...}) = true
1.1910 + | test_trans (PrfObj{branch = NoBranch,...}) = true
1.1911 + | test_trans (PblObj{branch = Transitive,...}) = true
1.1912 + | test_trans (PblObj{branch = NoBranch,...}) = true
1.1913 + | test_trans _ = false;
1.1914 +(*.shall cutting be continued on the higher level(s)?
1.1915 + the Nd regarded will NOT be changed.*)
1.1916 +fun cutlevup (PblObj _) = false (*for tests of LK0502*)
1.1917 + | cutlevup _ = true;
1.1918 +val cutlevup = test_trans;(*WN060727 after summerterm tests.LK0502 withdrawn*)
1.1919 +
1.1920 +(*cut_bottom new sml603..608
1.1921 +cut the level at the bottom of the pos (used by cappend_...)
1.1922 +and handle the parent in order to avoid extra case for root
1.1923 +fn: ptree -> : the _whole_ ptree for cut_levup
1.1924 + pos * posel -> : the pos after split_last
1.1925 + ptree -> : the parent of the Nd to be cut
1.1926 +return
1.1927 + (ptree * : the updated ptree
1.1928 + pos' list) * : the pos's cut
1.1929 + bool : cutting shall be continued on the higher level(s)
1.1930 +*)
1.1931 +fun cut_bottom _ (pt' as Nd (b, [])) = ((pt', []), cutlevup b)
1.1932 + | cut_bottom (P:pos, p:posel) (Nd (b, bs)) =
1.1933 + let (*divide level into 3 parts...*)
1.1934 + val keep = take (p - 1, bs)
1.1935 + val pt' as Nd (_,bs') = nth p bs
1.1936 + (*^^^^^_here_ will be 'insert'ed by 'append_..'*)
1.1937 + val (tail, tp) = (takerest (p, bs),
1.1938 + if null (takerest (p, bs)) then 0 else p + 1)
1.1939 + val (children, cuts) =
1.1940 + if test_trans b
1.1941 + then (keep,
1.1942 + (if is_pblnd pt' then [(P @ [p], Pbl)] else [])
1.1943 + @ (get_allp [] (P @ [p], (P, Frm)) pt')
1.1944 + @ (get_allps [] (P @ [p+1]) tail))
1.1945 + else (keep @ [(*'insert'ed by 'append_..'*)] @ tail,
1.1946 + get_allp [] (P @ [p], (P, Frm)) pt')
1.1947 + val (pt'', cuts) =
1.1948 + if cutlevup b
1.1949 + then (Nd (del_res b, children),
1.1950 + cuts @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
1.1951 + else (Nd (b, children), cuts)
1.1952 + (*val _= writeln("####cut_bottom (P, p)="^pos2str (P @ [p])^
1.1953 + ", Nd=.............................................")
1.1954 + val _= show_pt pt''
1.1955 + val _= writeln("####cut_bottom form='"^
1.1956 + term2str (get_obj g_form pt'' []))
1.1957 + val _= writeln("####cut_bottom cuts#="^string_of_int (length cuts)^
1.1958 + ", cuts="^pos's2str cuts)*)
1.1959 + in ((pt'', cuts:pos' list), cutlevup b) end;
1.1960 +
1.1961 +
1.1962 +(*.go all levels from the bottom of 'pos' up to the root,
1.1963 + on each level compose the children of a node and accumulate the cut Nds
1.1964 +args
1.1965 + pos' list -> : for accumulation
1.1966 + bool -> : cutting shall be continued on the higher level(s)
1.1967 + ptree -> : the whole ptree for 'get_nd pt P' on each level
1.1968 + ptree -> : the Nd from the lower level for insertion at path
1.1969 + pos * posel -> : pos=path split for convenience
1.1970 + ptree -> : Nd the children of are under consideration on this call
1.1971 +returns :
1.1972 + ptree * pos' list : the updated parent-Nd and the pos's of the Nds cut
1.1973 +.*)
1.1974 +fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:posel) (Nd (b, bs)) =
1.1975 + let (*divide level into 3 parts...*)
1.1976 + val keep = take (p - 1, bs)
1.1977 + (*val pt' comes as argument from below*)
1.1978 + val (tail, tp) = (takerest (p, bs),
1.1979 + if null (takerest (p, bs)) then 0 else p + 1)
1.1980 + val (children, cuts') =
1.1981 + if clevup
1.1982 + then (keep @ [pt'], get_allps [] (P @ [p+1]) tail)
1.1983 + else (keep @ [pt'] @ tail, [])
1.1984 + val clevup' = if clevup then cutlevup b else false
1.1985 + (*the first Nd with false stops cutting on all levels above*)
1.1986 + val (pt'', cuts') =
1.1987 + if clevup'
1.1988 + then (Nd (del_res b, children),
1.1989 + cuts' @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
1.1990 + else (Nd (b, children), cuts')
1.1991 + (*val _= writeln("#####cut_levup clevup= "^bool2str clevup)
1.1992 + val _= writeln("#####cut_levup cutlevup b= "^bool2str (cutlevup b))
1.1993 + val _= writeln("#####cut_levup (P, p)="^pos2str (P @ [p])^
1.1994 + ", Nd=.............................................")
1.1995 + val _= show_pt pt''
1.1996 + val _= writeln("#####cut_levup form='"^
1.1997 + term2str (get_obj g_form pt'' []))
1.1998 + val _= writeln("#####cut_levup cuts#="^string_of_int (length cuts)^
1.1999 + ", cuts="^pos's2str cuts)*)
1.2000 + in if null P then (pt'', (cuts @ cuts'):pos' list)
1.2001 + else let val (P, p) = split_last P
1.2002 + in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P)
1.2003 + end
1.2004 + end;
1.2005 +
1.2006 +(*.cut nodes after and below an inserted node in the ctree;
1.2007 + the cuts range is limited by the predicate 'fun cutlevup'.*)
1.2008 +fun cut_tree pt (pos,_) =
1.2009 + if not (existpt pos pt)
1.2010 + then (pt,[]) (*appending a formula never cuts anything*)
1.2011 + else let val (P, p) = split_last pos
1.2012 + val ((pt', cuts), clevup) = cut_bottom (P, p) (get_nd pt P)
1.2013 + (* pt' is the updated parent of the Nd to cappend_..*)
1.2014 + in if null P then (pt', cuts)
1.2015 + else let val (P, p) = split_last P
1.2016 + in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P)
1.2017 + end
1.2018 + end;
1.2019 +
1.2020 +fun append_atomic p l f r f' s pt =
1.2021 + let (**val _= writeln("#@append_atomic: pos ="^pos2str p)**)
1.2022 + val (iss, f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
1.2023 + then (*after Take*)
1.2024 + ((fst (get_obj g_loc pt p), Some l),
1.2025 + get_obj g_form pt p)
1.2026 + else ((None, Some l), f)
1.2027 + in insert (PrfObj {cell = None,
1.2028 + form = f,
1.2029 + tac = r,
1.2030 + loc = iss,
1.2031 + branch= NoBranch,
1.2032 + result= f',
1.2033 + ostate= s}) pt p end;
1.2034 +
1.2035 +
1.2036 +(*20.8.02: cappend_* FIXXXXME cut branches below cannot be decided here:
1.2037 + detail - generate - cappend: inserted, not appended !!!
1.2038 +
1.2039 + cut decided in applicable_in !?!
1.2040 +*)
1.2041 +fun cappend_atomic pt p loc f r f' s =
1.2042 +(* val (pt, p, loc, f, r, f', s) =
1.2043 + (pt,p,l,f,Rewrite_Set_Inst (subst2subs subs',id_rls rls'),
1.2044 + (f',asm),Complete);
1.2045 + *)
1.2046 +((*writeln("##@cappend_atomic: pos ="^pos2str p);*)
1.2047 + apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm))
1.2048 +);
1.2049 +(*TODO.WN050305 redesign the handling of istates*)
1.2050 +fun cappend_atomic pt p ist_res f r f' s =
1.2051 + if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
1.2052 + then (*after Take: transfer Frm and respective istate*)
1.2053 + let val (ist_form, f) = (get_loc pt (p,Frm),
1.2054 + get_obj g_form pt p)
1.2055 + val (pt, cs) = cut_tree pt (p,Frm)
1.2056 + val pt = append_atomic p e_istate f r f' s pt
1.2057 + val pt = update_loc' pt p (Some ist_form, Some ist_res)
1.2058 + in (pt, cs) end
1.2059 + else apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
1.2060 +
1.2061 +
1.2062 +(* called by Take *)
1.2063 +fun append_form p l f pt =
1.2064 +((*writeln("##@append_form: pos ="^pos2str p);*)
1.2065 + insert (PrfObj {cell = None,
1.2066 + form = (*if existpt p pt
1.2067 + andalso get_obj g_tac pt p = Empty_Tac
1.2068 + (*distinction from 'old' (+complete!) pobjs*)
1.2069 + then get_obj g_form pt p else*) f,
1.2070 + tac = Empty_Tac,
1.2071 + loc = (Some l, None),
1.2072 + branch= NoBranch,
1.2073 + result= (e_term,[]),
1.2074 + ostate= Incomplete}) pt p
1.2075 +);
1.2076 +(* val (p,loc,f) = ([1], e_istate, str2term "x + 1 = 2");
1.2077 + val (p,loc,f) = (fst p, e_istate, str2term "-1 + x = 0");
1.2078 + *)
1.2079 +fun cappend_form pt p loc f =
1.2080 +((*writeln("##@cappend_form: pos ="^pos2str p);*)
1.2081 + apfst (append_form p loc f) (cut_tree pt (p,Frm))
1.2082 +);
1.2083 +fun cappend_form pt p loc f =
1.2084 +let (*val _= writeln("##@cappend_form: pos ="^pos2str p)
1.2085 + val _= writeln("##@cappend_form before cut_tree: loc ="^istate2str loc)*)
1.2086 + val (pt', cs) = cut_tree pt (p,Frm)
1.2087 + val pt'' = append_form p loc f pt'
1.2088 + (*val _= writeln("##@cappend_form after append: loc ="^
1.2089 + istates2str (get_obj g_loc pt'' p))*)
1.2090 +in (pt'', cs) end;
1.2091 +
1.2092 +
1.2093 +
1.2094 +fun append_result pt p l f s =
1.2095 +((*writeln("##@append_result: pos ="^pos2str p);*)
1.2096 + (appl_obj (repl_result (fst (get_obj g_loc pt p),
1.2097 + Some l) f s) pt p, [])
1.2098 +);
1.2099 +
1.2100 +
1.2101 +(*WN041022 deprecated, still for kbtest/diffapp.sml, /systest/root-equ.sml*)
1.2102 +fun append_parent p l f r b pt =
1.2103 + let (*val _= writeln("###append_parent: pos ="^pos2str p);*)
1.2104 + val (ll,f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
1.2105 + then ((fst (get_obj g_loc pt p), Some l),
1.2106 + get_obj g_form pt p)
1.2107 + else ((Some l, None), f)
1.2108 + in insert (PrfObj
1.2109 + {cell = None,
1.2110 + form = f,
1.2111 + tac = r,
1.2112 + loc = ll,
1.2113 + branch= b,
1.2114 + result= (e_term,[]),
1.2115 + ostate= Incomplete}) pt p end;
1.2116 +fun cappend_parent pt p loc f r b =
1.2117 +((*writeln("###cappend_parent: pos ="^pos2str p);*)
1.2118 + apfst (append_parent p loc f r b) (cut_tree pt (p,Und))
1.2119 +);
1.2120 +
1.2121 +
1.2122 +fun append_problem [] l fmz (strs,spec,hdf) _ =
1.2123 +((*writeln("###append_problem: pos = []");*)
1.2124 + (Nd (PblObj
1.2125 + {cell = None,
1.2126 + origin= (strs,spec,hdf),
1.2127 + fmz = fmz,
1.2128 + spec = empty_spec,
1.2129 + probl = []:itm list,
1.2130 + meth = []:itm list,
1.2131 + env = None,
1.2132 + loc = (Some l, None),
1.2133 + branch= TransitiveB,(*FIXXXXXME.27.8.03: for equations only*)
1.2134 + result= (e_term,[]),
1.2135 + ostate= Incomplete},[]))
1.2136 +)
1.2137 + | append_problem p l fmz (strs,spec,hdf) pt =
1.2138 +((*writeln("###append_problem: pos ="^pos2str p);*)
1.2139 + insert (PblObj
1.2140 + {cell = None,
1.2141 + origin= (strs,spec,hdf),
1.2142 + fmz = fmz,
1.2143 + spec = empty_spec,
1.2144 + probl = []:itm list,
1.2145 + meth = []:itm list,
1.2146 + env = None,
1.2147 + loc = (Some l, None),
1.2148 + branch= TransitiveB,
1.2149 + result= (e_term,[]),
1.2150 + ostate= Incomplete}) pt p
1.2151 +);
1.2152 +fun cappend_problem _ [] loc fmz ori =
1.2153 +((*writeln("###cappend_problem: pos = []");*)
1.2154 + (append_problem [] loc fmz ori EmptyPtree,[])
1.2155 +)
1.2156 + | cappend_problem pt p loc fmz ori =
1.2157 +((*writeln("###cappend_problem: pos ="^pos2str p);*)
1.2158 + apfst (append_problem p (loc:istate) fmz ori) (cut_tree pt (p,Frm))
1.2159 +);
1.2160 +
1.2161 +(*.get the theory explicitly specified for the rootpbl;
1.2162 + thus use this function _after_ finishing specification.*)
1.2163 +fun rootthy (Nd (PblObj {spec=(thyID, _, _),...}, _)) = assoc_thy thyID
1.2164 + | rootthy _ = raise error "rootthy";
1.2165 +