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