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