wneuper/isa: src/Tools/isac/Interpret/ctree.sml@255c853ea2f0 (annotated)

wneuper@59274	1	(* Title: the calctree, which holds a calculation
wneuper@59274	2	Author: Walther Neuper 1999
wneuper@59274	3	(c) due to copyright terms
neuper@37906	4	*)
neuper@37906	5
wneuper@59275	6	signature CALC_TREEE =
wneuper@59275	7	sig (* vvv--- .sml require these typs incrementally, with these exception -----------------vvv )
wneuper@59275	8	(* for ptyps.sml *)
wneuper@59275	9	type fmz_ = cterm' list
wneuper@59275	10	type fmz = fmz_ * spec;
wneuper@59275	11	val e_fmz : fmz_ * spec (* for datatypes.sml *)
wneuper@59275	12	type con
wneuper@59275	13	type scrstate
wneuper@59275	14	datatype istate = RrlsState of rrlsstate \| ScrState of scrstate \| Uistate
wneuper@59275	15	val istate2str : istate -> string
wneuper@59275	16	val e_istate : istate
wneuper@59275	17	type subs
wneuper@59275	18	type sube
wneuper@59275	19	val sube2str : cterm' list -> string
wneuper@59275	20	type subte
wneuper@59275	21	val sube2subst : theory -> cterm' list -> (term * term) list
wneuper@59275	22	val sube2subte : cterm' list -> term list
wneuper@59275	23	val subs2subst : theory -> cterm' list -> (term * term) list
wneuper@59275	24	val subst2sube : (term * term) list -> cterm' list (* for datatypes.sml *)
wneuper@59275	25	val subst2subs : (term * term) list -> cterm' list
wneuper@59275	26	val subst2subs' : (term * term) list -> (string * string) list
wneuper@59275	27	val subte2sube : term list -> cterm' list
wneuper@59275	28
wneuper@59275	29	type result
wneuper@59275	30	datatype tac_ = (* TODO.WN161219: replace every cterm' by term *)
wneuper@59275	31	Add_Find' of cterm' * itm list \| Add_Given' of cterm' * itm list \| Add_Relation' of cterm' * itm list
wneuper@59275	32	\| Apply_Assumption' of term list * term
wneuper@59275	33	\| Apply_Method' of metID * term option * istate * Proof.context
wneuper@59275	34	(/--- TODO: re-design ? -----------------------------------------------------------------\)
wneuper@59275	35	\| Begin_Sequ' \| Begin_Trans' of term
wneuper@59275	36	\| Split_And' of term \| Split_Or' of term \| Split_Intersect' of term
wneuper@59275	37	\| Conclude_And' of term \| Conclude_Or' of term \| Collect_Trues' of term
wneuper@59275	38	\| End_Sequ' \| End_Trans' of result
wneuper@59275	39	\| End_Ruleset' of term \| End_Subproblem' of term \| End_Intersect' of term \| End_Proof''
wneuper@59275	40	(\--- TODO: re-design ? -----------------------------------------------------------------/)
wneuper@59275	41	\| CAScmd' of term
wneuper@59275	42	\| Calculate' of theory' * string * term * (term * thm')
wneuper@59275	43	\| Check_Postcond' of pblID * result
wneuper@59275	44	\| Check_elementwise' of term * cterm' * result
wneuper@59275	45	\| Del_Find' of cterm' \| Del_Given' of cterm' \| Del_Relation' of cterm'
wneuper@59275	46
wneuper@59275	47	\| Derive' of rls
wneuper@59275	48	\| Detail_Set' of theory' * bool * rls * term * result
wneuper@59275	49	\| Detail_Set_Inst' of theory' * bool * subst * rls * term * result
wneuper@59275	50	\| End_Detail' of result
wneuper@59275	51
wneuper@59275	52	\| Empty_Tac_
wneuper@59275	53	\| Free_Solve'
wneuper@59275	54
wneuper@59275	55	\| Init_Proof' of cterm' list * spec
wneuper@59275	56	\| Model_Problem' of pblID * itm list * itm list
wneuper@59275	57	\| Or_to_List' of term * term
wneuper@59275	58	\| Refine_Problem' of pblID * (itm list * (bool * term) list)
wneuper@59275	59	\| Refine_Tacitly' of pblID * pblID * domID * metID * itm list
wneuper@59275	60
wneuper@59275	61	\| Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * result
wneuper@59275	62	\| Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * result
wneuper@59275	63	\| Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * result
wneuper@59275	64	\| Rewrite_Set' of theory' * bool * rls * term * result
wneuper@59275	65	\| Rewrite_Set_Inst' of theory' * bool * subst * rls * term * result
wneuper@59275	66
wneuper@59275	67	\| Specify_Method' of metID * ori list * itm list
wneuper@59275	68	\| Specify_Problem' of pblID * (bool * (itm list * (bool * term) list))
wneuper@59275	69	\| Specify_Theory' of domID
wneuper@59275	70	\| Subproblem' of spec * ori list * term * fmz_ * Proof.context * term
wneuper@59275	71	\| Substitute' of rew_ord_ * rls * subte * term * term
wneuper@59275	72	\| Tac_ of theory * string * string * string
wneuper@59275	73	\| Take' of term \| Take_Inst' of term
wneuper@59275	74	datatype tac =
wneuper@59275	75	Add_Find of cterm' \| Add_Given of cterm' \| Add_Relation of cterm'
wneuper@59275	76	\| Apply_Assumption of cterm' list
wneuper@59275	77	\| Apply_Method of metID
wneuper@59275	78
wneuper@59275	79	\| Begin_Sequ \| Begin_Trans
wneuper@59275	80	\| Split_And \| Split_Or \| Split_Intersect
wneuper@59275	81	\| Conclude_And \| Conclude_Or \| Collect_Trues
wneuper@59275	82	\| End_Sequ \| End_Trans
wneuper@59275	83	\| End_Ruleset \| End_Subproblem \| End_Intersect \| End_Proof'
wneuper@59275	84
wneuper@59275	85	\| CAScmd of cterm'
wneuper@59275	86	\| Calculate of string
wneuper@59275	87	\| Check_Postcond of pblID
wneuper@59275	88	\| Check_elementwise of cterm'
wneuper@59275	89	\| Del_Find of cterm' \| Del_Given of cterm' \| Del_Relation of cterm'
wneuper@59275	90
wneuper@59275	91	\| Derive of rls'
wneuper@59275	92	\| Detail_Set of rls'
wneuper@59275	93	\| Detail_Set_Inst of subs * rls'
wneuper@59275	94	\| End_Detail
wneuper@59275	95
wneuper@59275	96	\| Empty_Tac
wneuper@59275	97	\| Free_Solve
wneuper@59275	98	\| Group of con * int list
wneuper@59275	99
wneuper@59275	100	\| Init_Proof of cterm' list * spec
wneuper@59275	101	\| Model_Problem
wneuper@59275	102	\| Or_to_List
wneuper@59275	103	\| Refine_Problem of pblID
wneuper@59275	104	\| Refine_Tacitly of pblID
wneuper@59275	105
wneuper@59275	106	\| Rewrite of thm''
wneuper@59275	107	\| Rewrite_Asm of thm''
wneuper@59275	108	\| Rewrite_Inst of subs * thm''
wneuper@59275	109	\| Rewrite_Set of rls'
wneuper@59275	110	\| Rewrite_Set_Inst of subs * rls'
wneuper@59275	111
wneuper@59275	112	\| Specify_Method of metID
wneuper@59275	113	\| Specify_Problem of pblID
wneuper@59275	114	\| Specify_Theory of domID
wneuper@59275	115	\| Subproblem of domID * pblID
wneuper@59275	116
wneuper@59275	117	\| Substitute of sube
wneuper@59275	118	\| Tac of string
wneuper@59275	119	\| Take of cterm' \| Take_Inst of cterm'
wneuper@59275	120	val tac2str : tac -> string
wneuper@59275	121	val rls_of : tac -> rls' (* for solve.sml *)
wneuper@59275	122	val tac2IDstr : tac -> string
wneuper@59275	123	val is_rewset : tac -> bool (* for mathengine.sml *)
wneuper@59275	124	val is_rewtac : tac -> bool (* for interface.sml *)
wneuper@59275	125
wneuper@59275	126	eqtype posel
wneuper@59275	127	type pos = posel list
wneuper@59275	128	val pos2str : int list -> string (* for datatypes.sml *)
wneuper@59275	129	datatype pos_ = Frm \| Met \| Pbl \| Res \| Und
wneuper@59275	130	val pos_2str : pos_ -> string
wneuper@59275	131	type pos'
wneuper@59275	132	val pos'2str : pos' -> string
wneuper@59275	133	val str2pos_ : string -> pos_ (* for datatypes.sml *)
wneuper@59275	134	val e_pos' : pos'
wneuper@59275	135	type state
wneuper@59275	136	(* for generate.sml ?!? ca.*)
wneuper@59275	137	datatype safe = Helpless \| Safe \| Sundef \| Unsafe
wneuper@59275	138	val tac_2str : tac_ -> string
wneuper@59275	139	eqtype cellID
wneuper@59275	140
wneuper@59275	141	datatype branch = AndB \| CollectB \| IntersectB \| MapB \| NoBranch \| OrB \| SequenceB \| TransitiveB
wneuper@59275	142	datatype ostate = Complete \| Incomplete \| Inconsistent
wneuper@59275	143	datatype ppobj =
wneuper@59275	144	PblObj of
wneuper@59275	145	{branch: branch,
wneuper@59275	146	cell: lrd option,
wneuper@59275	147	loc: (istate * Proof.context) option * (istate * Proof.context) option,
wneuper@59275	148	ostate: ostate,
wneuper@59275	149	result: result,
wneuper@59275	150
wneuper@59275	151	fmz: fmz,
wneuper@59275	152	origin: ori list * spec * term,
wneuper@59275	153	probl: itm list,
wneuper@59275	154	meth: itm list,
wneuper@59275	155	spec: spec,
wneuper@59275	156	ctxt: Proof.context,
wneuper@59275	157	env: (istate * Proof.context) option}
wneuper@59275	158	\| PrfObj of
wneuper@59275	159	{branch: branch,
wneuper@59275	160	cell: lrd option,
wneuper@59275	161	loc: (istate * Proof.context) option * (istate * Proof.context) option,
wneuper@59275	162	ostate: ostate,
wneuper@59275	163	result: result,
wneuper@59275	164
wneuper@59275	165	form: term,
wneuper@59275	166	tac: tac}
wneuper@59275	167	val lev_on : pos -> pos
wneuper@59275	168	val lev_dn : pos -> pos
wneuper@59275	169	val lev_dn_ : pos' -> pos'
wneuper@59275	170	val lev_up : pos -> pos
wneuper@59275	171	val lev_of : pos' -> int
wneuper@59275	172	val pos_plus : int -> pos' -> pos'
wneuper@59275	173	val lev_back' : pos' -> pos' (* for inform.sml *)
wneuper@59275	174
wneuper@59279	175	datatype ctree = EmptyPtree \| Nd of ppobj * ctree list
wneuper@59279	176	val e_ctree : ctree (* TODO: replace by EmptyPtree*)
wneuper@59279	177	val existpt' : pos' -> ctree -> bool (* for interface.sml *)
wneuper@59279	178	val exist_lev_on' : ctree -> pos' -> bool (* for interface.sml *)
wneuper@59275	179	val is_interpos : pos' -> bool (* for interface.sml *)
wneuper@59279	180	val lev_on' : ctree -> pos' -> pos' (* for interface.sml *)
wneuper@59279	181	val lev_pred' : ctree -> pos' -> pos' (* for interface.sml *)
wneuper@59279	182	val move_up : pos -> ctree -> pos' -> pos' (* for interface.sml *)
wneuper@59279	183	val movelevel_dn : pos -> ctree -> pos' -> pos' (* for interface.sml *)
wneuper@59279	184	val movelevel_up : pos -> ctree -> pos' -> pos' (* for interface.sml *)
wneuper@59279	185	val movecalchd_up : ctree -> pos' -> pos' (* for interface.sml *)
wneuper@59279	186	val par_pblobj : ctree -> pos -> pos
wneuper@59279	187	val ins_chn : ctree list -> ctree -> pos -> ctree (* for solve.sml *)
wneuper@59279	188	val children : ctree -> ctree list (* for solve.sml *)
wneuper@59279	189	val get_nd : ctree -> pos -> ctree (* for solve.sml *)
wneuper@59275	190	val just_created_ : ppobj -> bool (* for mathengine.sml *)
wneuper@59279	191	val just_created : ctree * pos' -> bool (* for mathengine.sml *)
wneuper@59279	192	val is_curr_endof_calc : ctree -> pos' -> bool (* for interface.sml *)
wneuper@59275	193	val e_origin : ori list * spec * term (* for mathengine.sml *)
wneuper@59275	194
wneuper@59279	195	val move_dn : pos -> ctree -> pos' -> pos'
wneuper@59275	196	val is_pblobj : ppobj -> bool
wneuper@59279	197	val is_pblobj' : ctree -> pos -> bool
wneuper@59279	198	val is_pblnd : ctree -> bool
wneuper@59279	199	val last_onlev : ctree -> pos -> bool
wneuper@59275	200
wneuper@59275	201	val g_spec : ppobj -> spec
wneuper@59275	202	val g_loc : ppobj -> (istate * Proof.context) option * (istate * Proof.context) option
wneuper@59275	203	val g_form : ppobj -> term
wneuper@59275	204	val g_pbl : ppobj -> itm list
wneuper@59275	205	val g_met : ppobj -> itm list
wneuper@59275	206	val g_metID : ppobj -> metID
wneuper@59275	207	val g_result : ppobj -> result
wneuper@59275	208	val g_tac : ppobj -> tac
wneuper@59275	209	val g_domID : ppobj -> domID (* for appl.sml TODO: replace by thyID *)
wneuper@59275	210	val g_env : ppobj -> (istate * Proof.context) option (* for appl.sml *)
wneuper@59275	211
wneuper@59275	212	val g_origin : ppobj -> ori list * spec * term (* for script.sml *)
wneuper@59279	213	val get_loc : ctree -> pos' -> istate * Proof.context (* for script.sml *)
wneuper@59279	214	val get_istate : ctree -> pos' -> istate (* for script.sml *)
wneuper@59279	215	val get_ctxt : ctree -> pos' -> Proof.context
wneuper@59279	216	val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a
wneuper@59279	217	val get_curr_formula : ctree * pos' -> term
wneuper@59279	218	val get_assumptions_ : ctree -> pos' -> term list (* for appl.sml *)
wneuper@59275	219
wneuper@59279	220	val append_result : ctree -> pos -> istate * Proof.context -> result ->
wneuper@59279	221	ostate -> ctree * 'a list
wneuper@59275	222	val append_atomic : (* for solve.sml *)
wneuper@59279	223	pos -> istate * Proof.context -> term -> tac -> result -> ostate -> ctree -> ctree
wneuper@59279	224	val cappend_atomic : ctree -> pos -> istate * Proof.context -> term -> tac -> result ->
wneuper@59279	225	ostate -> ctree * pos' list
wneuper@59279	226	val cappend_form : ctree -> pos -> istate * Proof.context -> term -> ctree * pos' list
wneuper@59279	227	val cappend_problem : ctree -> pos -> istate * Proof.context -> fmz ->
wneuper@59279	228	ori list * spec * term -> ctree * pos' list
wneuper@59275	229
wneuper@59279	230	val update_branch : ctree -> pos -> branch -> ctree
wneuper@59279	231	val update_ctxt : ctree -> pos -> Proof.context -> ctree
wneuper@59279	232	val update_env : ctree -> pos -> (istate * Proof.context) option -> ctree
wneuper@59279	233	val update_oris : ctree -> pos -> ori list -> ctree
wneuper@59279	234	val update_orispec : ctree -> pos -> spec -> ctree
wneuper@59279	235	val update_pbl : ctree -> pos -> itm list -> ctree
wneuper@59279	236	val update_pblppc : ctree -> pos -> itm list -> ctree (* =vvv= ? *)
wneuper@59279	237	val update_pblID : ctree -> pos -> pblID -> ctree (* =^^^= ? *)
wneuper@59279	238	val update_met : ctree -> pos -> itm list -> ctree (* =vvv= ? *)
wneuper@59279	239	val update_metppc : ctree -> pos -> itm list -> ctree (* =^^^= ? *)
wneuper@59279	240	val update_metID : ctree -> pos -> metID -> ctree
wneuper@59279	241	val update_domID : ctree -> pos -> domID -> ctree
wneuper@59279	242	val update_spec : ctree -> pos -> spec -> ctree
wneuper@59279	243	val update_tac : ctree -> pos -> tac -> ctree
wneuper@59275	244
wneuper@59275	245	val e_ctxt : Proof.context
wneuper@59275	246	val is_e_ctxt : Proof.context -> bool (* for appl.sml *)
wneuper@59275	247	val new_val : term -> istate -> istate
wneuper@59275	248	(* for calchead.sml *)
wneuper@59275	249	type cid = cellID list
wneuper@59275	250	type ocalhd = bool * pos_ * term * itm list * (bool * term) list * spec
wneuper@59275	251	datatype ptform = Form of term \| ModSpec of ocalhd
wneuper@59275	252	val get_somespec' : spec -> spec -> spec
wneuper@59275	253	exception PTREE of string;
wneuper@59275	254	(* for appl.sml *)
wneuper@59279	255	val par_pbl_det : ctree -> pos -> bool * pos * rls
wneuper@59275	256	(* for rewtools.sml *)
wneuper@59275	257	val rule2tac : theory -> (term * term) list -> rule -> tac
wneuper@59275	258	val eq_tac : tac * tac -> bool
wneuper@59275	259	(* for script.sml *)
wneuper@59279	260	val rootthy : ctree -> theory
wneuper@59275	261	(/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\ )
wneuper@59279	262	val update_loc' : ctree -> pos -> (istate * Proof.context) option * (istate * Proof.context) option -> ctree
wneuper@59279	263	val append_problem : int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree -> ctree
wneuper@59275	264	val g_res : ppobj -> term
wneuper@59279	265	val pr_ctree : (pos -> ppobj -> string) -> ctree -> string
wneuper@59275	266	val pr_short : pos -> ppobj -> string
wneuper@59279	267	val existpt : pos -> ctree -> bool
wneuper@59275	268	val is_empty_tac : tac -> bool
wneuper@59275	269	val e_subs : string list
wneuper@59275	270	val e_sube : cterm' list
wneuper@59275	271	val g_branch : ppobj -> branch
wneuper@59275	272	val g_ctxt : ppobj -> Proof.context
wneuper@59275	273	val g_fmz : ppobj -> fmz
wneuper@59279	274	val get_allp : pos' list -> pos * (int list * pos_) -> ctree -> pos' list
wneuper@59279	275	val get_allps : (pos * pos_) list -> posel list -> ctree list -> pos' list
wneuper@59279	276	val get_allpos' : pos * posel -> ctree -> pos' list
wneuper@59279	277	val get_allpos's : pos * posel -> ctree list -> (pos * pos_) list
wneuper@59279	278	val cut_bottom : pos * posel -> ctree -> (ctree * pos' list) * bool
wneuper@59279	279	val cut_tree : ctree -> pos * 'a -> ctree * pos' list
wneuper@59279	280	val cut_level : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
wneuper@59279	281	val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
wneuper@59279	282	val get_trace : ctree -> int list -> int list -> int list list
wneuper@59275	283	val subte2subst : term list -> (term * term) list
wneuper@59275	284	val branch2str : branch -> string
wneuper@59275	285	( \--- ! aktivate for Test_Isac END ----------------------------------------------------------/)
wneuper@59275	286	end
wneuper@59275	287	(*
wneuper@59275	288	structure Ctree :
wneuper@59275	289	sig
wneuper@59275	290	val Ets : ets exception PTREE of string
wneuper@59275	291	val append_atomic :
wneuper@59279	292	pos -> istate * Proof.context -> term -> tac -> term * term list -> ostate -> ctree -> ctree
wneuper@59279	293	val append_form : int list -> istate * Proof.context -> term -> ctree -> ctree
wneuper@59279	294	val append_parent : pos -> istate * Proof.context -> term -> tac -> branch -> ctree -> ctree
wneuper@59279	295	val append_problem : int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree -> ctree
wneuper@59279	296	val append_result : ctree -> pos -> istate * Proof.context -> term * term list -> ostate -> ctree * 'a list
wneuper@59279	297	val appl_branch : (ppobj -> bool) * (posel -> ctree list -> ctree list) -> ctree -> int list -> ctree * bool
wneuper@59279	298	val appl_obj : (ppobj -> ppobj) -> ctree -> pos -> ctree
wneuper@59279	299	val appl_to_node : (ppobj -> ppobj) -> ctree -> ctree
wneuper@59275	300	datatype branch = AndB \| CollectB \| IntersectB \| MapB \| NoBranch \| OrB \| SequenceB \| TransitiveB
wneuper@59275	301	val branch2str : branch -> string
wneuper@59275	302	val cappend_atomic :
wneuper@59279	303	ctree -> pos -> istate * Proof.context -> term -> tac -> term * term list -> ostate -> ctree * pos' list
wneuper@59279	304	val cappend_form : ctree -> pos -> istate * Proof.context -> term -> ctree * pos' list
wneuper@59279	305	val cappend_parent : ctree -> pos -> istate * Proof.context -> term -> tac -> branch -> ctree * pos' list
wneuper@59275	306	val cappend_problem :
wneuper@59279	307	ctree -> int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree * pos' list
wneuper@59275	308	eqtype cellID
wneuper@59279	309	val children : ctree -> ctree list
wneuper@59275	310	type cid = cellID list
wneuper@59275	311	datatype con = land \| lor
wneuper@59279	312	val cut_bottom : pos * posel -> ctree -> (ctree * pos' list) * bool
wneuper@59279	313	val cut_level : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
wneuper@59279	314	val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
wneuper@59279	315	val cut_levup : pos' list -> bool -> ctree -> ctree -> posel list * posel -> ctree -> ctree * pos' list
wneuper@59279	316	val cut_tree : ctree -> pos * 'a -> ctree * pos' list
wneuper@59275	317	val cutlevup : ppobj -> bool
wneuper@59275	318	val del_res : ppobj -> ppobj
wneuper@59279	319	val delete_result : ctree -> pos -> ctree
wneuper@59275	320	val e_ctxt : Proof.context
wneuper@59275	321	val e_fmz : 'a list * spec
wneuper@59275	322	val e_ocalhd : bool * pos_ * term * itm list * (bool * term) list * spec
wneuper@59275	323	val e_origin : ori list * spec * term
wneuper@59275	324	val e_ptform : ptform
wneuper@59275	325	val e_ptform' : ptform
wneuper@59279	326	val e_ctree : ctree
wneuper@59275	327	val e_scrstate : scrstate
wneuper@59275	328	val e_sube : cterm' list
wneuper@59275	329	val e_subs : string list
wneuper@59275	330	val e_subte : term list
wneuper@59275	331	val empty_envp : envp type env = (term * term) list
wneuper@59275	332	type envp = (int * term list) list * (int * rls) list * (int * ets) list * (string * pos) list
wneuper@59275	333	val eq_tac : tac * tac -> bool type ets = (loc_ * (tac_ * env * env * term * term * safe)) list
wneuper@59275	334	val ets2s : loc_ * (tac_ * subst * subst * term * term * safe) -> string
wneuper@59275	335	val ets2str : ets -> string
wneuper@59279	336	val exist_lev_on' : ctree -> pos' -> bool
wneuper@59279	337	val existpt : pos -> ctree -> bool
wneuper@59279	338	val existpt' : pos' -> ctree -> bool
wneuper@59275	339	type fmz = fmz_ * spec
wneuper@59275	340	type fmz_ = cterm' list
wneuper@59275	341	val g_branch : ppobj -> branch
wneuper@59275	342	val g_cell : ppobj -> lrd option
wneuper@59275	343	val g_ctxt : ppobj -> Proof.context
wneuper@59275	344	val g_domID : ppobj -> domID
wneuper@59275	345	val g_env : ppobj -> (istate * Proof.context) option
wneuper@59275	346	val g_fmz : ppobj -> fmz
wneuper@59275	347	val g_form : ppobj -> term
wneuper@59279	348	val g_form' : ctree -> term
wneuper@59275	349	val g_loc : ppobj -> (istate * Proof.context) option * (istate * Proof.context) option
wneuper@59275	350	val g_met : ppobj -> itm list
wneuper@59275	351	val g_metID : ppobj -> metID
wneuper@59275	352	val g_origin : ppobj -> ori list * spec * term
wneuper@59275	353	val g_ostate : ppobj -> ostate
wneuper@59279	354	val g_ostate' : ctree -> ostate
wneuper@59275	355	val g_pbl : ppobj -> itm list
wneuper@59275	356	val g_res : ppobj -> term
wneuper@59279	357	val g_res' : ctree -> term
wneuper@59275	358	val g_result : ppobj -> term * term list
wneuper@59275	359	val g_spec : ppobj -> spec
wneuper@59275	360	val g_tac : ppobj -> tac
wneuper@59279	361	val get_all : (ppobj -> 'a) -> ctree -> 'a list
wneuper@59279	362	val get_allp : pos' list -> pos * (int list * pos_) -> ctree -> pos' list
wneuper@59279	363	val get_allpos' : pos * posel -> ctree -> pos' list
wneuper@59279	364	val get_allpos's : pos * posel -> ctree list -> (pos * pos_) list
wneuper@59279	365	val get_allps : (pos * pos_) list -> posel list -> ctree list -> pos' list
wneuper@59279	366	val get_alls : (ppobj -> 'a) -> ctree list -> 'a list
wneuper@59279	367	val get_assumptions_ : ctree -> pos * pos_ -> term list
wneuper@59279	368	val get_ctxt : ctree -> pos * pos_ -> Proof.context
wneuper@59279	369	val get_curr_formula : ctree * (pos * pos_) -> term
wneuper@59279	370	val get_istate : ctree -> pos * pos_ -> istate
wneuper@59279	371	val get_loc : ctree -> pos * pos_ -> istate * Proof.context
wneuper@59279	372	val get_nd : ctree -> pos -> ctree
wneuper@59279	373	val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a
wneuper@59275	374	val get_somespec : spec -> spec -> spec
wneuper@59275	375	val get_somespec' : spec -> spec -> spec
wneuper@59279	376	val get_trace : ctree -> int list -> int list -> int list list
wneuper@59279	377	val gpt_cell : ctree -> lrd option
wneuper@59275	378	type iist = istate option * istate option
wneuper@59275	379	val ind : pos' -> int
wneuper@59279	380	val ins_chn : ctree list -> ctree -> int list -> ctree
wneuper@59275	381	val ins_nth : int -> 'a -> 'a list -> 'a list
wneuper@59279	382	val insert_pt : ppobj -> ctree -> int list -> ctree
wneuper@59279	383	val is_curr_endof_calc : ctree -> pos' -> bool
wneuper@59275	384	val is_e_ctxt : Proof.context -> bool
wneuper@59275	385	val is_empty_tac : tac -> bool
wneuper@59275	386	val is_interpos : pos' -> bool
wneuper@59279	387	val is_pblnd : ctree -> bool
wneuper@59275	388	val is_pblobj : ppobj -> bool
wneuper@59279	389	val is_pblobj' : ctree -> pos -> bool
wneuper@59275	390	val is_prfobj : ppobj -> bool
wneuper@59275	391	val is_rewset : tac -> bool
wneuper@59275	392	val is_rewtac : tac -> bool
wneuper@59275	393	val isasub2subst : term -> (term * term) list
wneuper@59275	394	datatype istate = RrlsState of rrlsstate \| ScrState of scrstate \| Uistate
wneuper@59275	395	val istate2str : istate -> string
wneuper@59275	396	val istates2str : istate option * istate option -> string
wneuper@59279	397	val just_created : ctree * pos' -> bool
wneuper@59275	398	val just_created_ : ppobj -> bool
wneuper@59279	399	val last_onlev : ctree -> pos -> bool
wneuper@59275	400	val lev_back' : pos' -> pos'
wneuper@59275	401	val lev_dn : posel list -> posel list
wneuper@59275	402	val lev_dnRes : pos' -> pos'
wneuper@59275	403	val lev_dn_ : pos' -> pos'
wneuper@59275	404	val lev_of : pos' -> int
wneuper@59275	405	val lev_on : pos -> posel list
wneuper@59279	406	val lev_on' : ctree -> pos' -> pos'
wneuper@59275	407	val lev_onFrm : pos' -> pos'
wneuper@59275	408	val lev_pred : pos -> pos
wneuper@59279	409	val lev_pred' : ctree -> pos' -> pos'
wneuper@59275	410	val lev_up : pos -> pos
wneuper@59275	411	val lev_up_ : pos' -> pos'
wneuper@59279	412	val move_dn : pos -> ctree -> int list * pos_ -> int list * pos_
wneuper@59279	413	val move_up : int list -> ctree -> int list * pos_ -> int list * pos_
wneuper@59279	414	val movecalchd_up : ctree -> pos' -> pos'
wneuper@59279	415	val movelevel_dn : int list -> ctree -> int list * pos_ -> int list * pos_
wneuper@59279	416	val movelevel_up : int list -> ctree -> int list * pos_ -> int list * pos_
wneuper@59275	417	val new_val : term -> istate -> istate
wneuper@59275	418	val nth : int -> 'a list -> 'a
wneuper@59275	419	type ocalhd = bool * pos_ * term * itm list * (bool * term) list * spec
wneuper@59275	420	val ocalhd2str : ocalhd -> string
wneuper@59275	421	datatype ostate = Complete \| Incomplete \| Inconsistent
wneuper@59275	422	val ostate2str : ostate -> string
wneuper@59279	423	val par_children : ctree -> pos -> ctree list * pos
wneuper@59279	424	val par_pbl_det : ctree -> pos -> bool * pos * rls
wneuper@59279	425	val par_pblobj : ctree -> pos -> pos
wneuper@59275	426	type pos = posel list
wneuper@59275	427	type pos' = pos * pos_
wneuper@59275	428	val pos's2str : (int list * pos_) list -> string
wneuper@59275	429	val pos2str : int list -> string
wneuper@59275	430	datatype pos_ = Frm \| Met \| Pbl \| Res \| Und
wneuper@59275	431	val pos_2str : pos_ -> string
wneuper@59275	432	val pos_plus : int -> pos * pos_ -> pos'
wneuper@59275	433	eqtype posel
wneuper@59275	434	val posless : int list -> int list -> bool
wneuper@59275	435	datatype ppobj
wneuper@59275	436	= PblObj of
wneuper@59275	437	{branch: branch,
wneuper@59275	438	cell: lrd option,
wneuper@59275	439	ctxt: Proof.context,
wneuper@59275	440	env: (istate * Proof.context) option,
wneuper@59275	441	fmz: fmz,
wneuper@59275	442	loc: (istate * Proof.context) option * (istate * Proof.context) option,
wneuper@59275	443	meth: itm list,
wneuper@59275	444	origin: ori list * spec * term, ostate: ostate, probl: itm list, result: term * term list, spec: spec}
wneuper@59275	445	\| PrfObj of
wneuper@59275	446	{branch: branch,
wneuper@59275	447	cell: lrd option,
wneuper@59275	448	form: term,
wneuper@59275	449	loc: (istate * Proof.context) option * (istate * Proof.context) option,
wneuper@59275	450	ostate: ostate, result: term * term list, tac: tac}
wneuper@59275	451	val pr_pos : int list -> string
wneuper@59279	452	val pr_ctree : (pos -> ppobj -> string) -> ctree -> string
wneuper@59275	453	val pr_short : pos -> ppobj -> string
wneuper@59275	454	val pre_pos : pos -> pos
wneuper@59275	455	val preconds2str : (bool * term) list -> string
wneuper@59275	456	datatype ptform = Form of term \| ModSpec of ocalhd
wneuper@59279	457	datatype ctree = EmptyPtree \| Nd of ppobj * ctree list
wneuper@59275	458	val rep_pblobj :
wneuper@59275	459	ppobj ->
wneuper@59275	460	{branch: branch,
wneuper@59275	461	cell: lrd option,
wneuper@59275	462	ctxt: Proof.context,
wneuper@59275	463	env: (istate * Proof.context) option,
wneuper@59275	464	fmz: fmz,
wneuper@59275	465	loc: (istate * Proof.context) option * (istate * Proof.context) option,
wneuper@59275	466	meth: itm list,
wneuper@59275	467	origin: ori list * spec * term, ostate: ostate, probl: itm list, result: term * term list, spec: spec}
wneuper@59275	468	val rep_prfobj :
wneuper@59275	469	ppobj ->
wneuper@59275	470	{branch: branch,
wneuper@59275	471	cell: lrd option,
wneuper@59275	472	form: term,
wneuper@59275	473	loc: (istate * Proof.context) option * (istate * Proof.context) option,
wneuper@59275	474	ostate: ostate, result: term * term list, tac: tac}
wneuper@59275	475	val repl : 'a list -> int -> 'a -> 'a list
wneuper@59275	476	val repl_app : 'a list -> int -> 'a -> 'a list
wneuper@59275	477	val repl_branch : branch -> ppobj -> ppobj
wneuper@59275	478	val repl_ctxt : Proof.context -> ppobj -> ppobj
wneuper@59275	479	val repl_domID : domID -> ppobj -> ppobj
wneuper@59275	480	val repl_env : (istate * Proof.context) option -> ppobj -> ppobj
wneuper@59275	481	val repl_form : term -> ppobj -> ppobj
wneuper@59275	482	val repl_loc : (istate * Proof.context) option * (istate * Proof.context) option -> ppobj -> ppobj
wneuper@59275	483	val repl_met : itm list -> ppobj -> ppobj
wneuper@59275	484	val repl_metID : metID -> ppobj -> ppobj
wneuper@59275	485	val repl_oris : ori list -> ppobj -> ppobj
wneuper@59275	486	val repl_orispec : spec -> ppobj -> ppobj
wneuper@59275	487	val repl_pbl : itm list -> ppobj -> ppobj
wneuper@59275	488	val repl_pblID : pblID -> ppobj -> ppobj
wneuper@59275	489	val repl_result :
wneuper@59275	490	(istate * Proof.context) option * (istate * Proof.context) option ->
wneuper@59275	491	term * term list -> ostate -> ppobj -> ppobj
wneuper@59275	492	val repl_spec : spec -> ppobj -> ppobj
wneuper@59275	493	val repl_tac : tac -> ppobj -> ppobj
wneuper@59275	494	val res2str : term * term list -> string
wneuper@59275	495	val rls_of : tac -> rls'
wneuper@59275	496	val rls_of_rewset : tac -> rls' * subst option
wneuper@59279	497	val rootthy : ctree -> theory
wneuper@59275	498	val rta2str : rule * (term * term list) -> string
wneuper@59275	499	val rule2tac : theory -> (term * term) list -> rule -> tac
wneuper@59275	500	val safe2str : safe -> string
wneuper@59275	501	type scrstate = env * loc_ * term option * term * safe * bool
wneuper@59275	502	val scrstate2str : subst * loc_ * term option * term * safe * bool -> string
wneuper@59275	503	val str2pos_ : string -> pos_
wneuper@59275	504	type sube = cterm' list
wneuper@59275	505	val sube2str : string list -> string
wneuper@59275	506	val sube2subst : theory -> string list -> (term * term) list
wneuper@59275	507	val sube2subte : string list -> term list
wneuper@59275	508	type subs = cterm' list
wneuper@59275	509	val subs2subst : theory -> string list -> (term * term) list
wneuper@59275	510	val subst2sube : (term * term) list -> string list
wneuper@59275	511	val subst2subs : (term * term) list -> string list
wneuper@59275	512	val subst2subs' : (term * term) list -> (string * string) list
wneuper@59275	513	type subte = term list
wneuper@59275	514	val subte2str : term list -> string
wneuper@59275	515	val subte2sube : term list -> string list
wneuper@59275	516	val subte2subst : term list -> (term * term) list
wneuper@59275	517	datatype tac
wneuper@59275	518	= Add_Find of cterm' \| Add_Given of cterm' \| Add_Relation of cterm' \| Apply_Assumption of cterm' list
wneuper@59275	519	\| Apply_Method of metID \| Begin_Sequ \| Begin_Trans \| CAScmd of cterm' \| Calculate of string
wneuper@59275	520	\| Check_Postcond of pblID \| Check_elementwise of cterm' \| Collect_Trues \| Conclude_And \| Conclude_Or
wneuper@59275	521	\| Del_Find of cterm' \| Del_Given of cterm' \| Del_Relation of cterm' \| Derive of rls' \| Detail_Set of rls'
wneuper@59275	522	\| Detail_Set_Inst of subs * rls' \| Empty_Tac \| End_Detail \| End_Intersect \| End_Proof' \| End_Ruleset
wneuper@59275	523	\| End_Sequ \| End_Subproblem \| End_Trans \| Free_Solve \| Group of con * int list
wneuper@59275	524	\| Init_Proof of cterm' list * spec \| Model_Problem \| Or_to_List \| Refine_Problem of pblID
wneuper@59275	525	\| Refine_Tacitly of pblID \| Rewrite of thm'' \| Rewrite_Asm of thm'' \| Rewrite_Inst of subs * thm''
wneuper@59275	526	\| Rewrite_Set of rls' \| Rewrite_Set_Inst of subs * rls' \| Specify_Method of metID
wneuper@59275	527	\| Specify_Problem of pblID \| Specify_Theory of domID \| Split_And \| Split_Intersect \| Split_Or
wneuper@59275	528	\| Subproblem of domID * pblID \| Substitute of sube \| Tac of string \| Take of cterm' \| Take_Inst of cterm'
wneuper@59275	529	val tac2IDstr : tac -> string
wneuper@59275	530	datatype tac_
wneuper@59275	531	= Add_Find' of cterm' * itm list \| Add_Given' of cterm' * itm list \| Add_Relation' of cterm' * itm list
wneuper@59275	532	\| Apply_Assumption' of term list * term \| Apply_Method' of metID * term option * istate * Proof.context
wneuper@59275	533	\| Begin_Sequ' \| Begin_Trans' of term \| CAScmd' of term
wneuper@59275	534	\| Calculate' of theory' * string * term * (term * thm') \| Check_Postcond' of pblID * (term * term list)
wneuper@59275	535	\| Check_elementwise' of term * string * (term * term list) \| Collect_Trues' of term
wneuper@59275	536	\| Conclude_And' of term \| Conclude_Or' of term \| Del_Find' of cterm' \| Del_Given' of cterm'
wneuper@59275	537	\| Del_Relation' of cterm' \| Derive' of rls
wneuper@59275	538	\| Detail_Set' of theory' * bool * rls * term * (term * term list)
wneuper@59275	539	\| Detail_Set_Inst' of theory' * bool * subst * rls * term * (term * term list) \| Empty_Tac_
wneuper@59275	540	\| End_Detail' of term * term list \| End_Intersect' of term \| End_Proof'' \| End_Ruleset' of term
wneuper@59275	541	\| End_Sequ' \| End_Subproblem' of term \| End_Trans' of term * term list \| Free_Solve'
wneuper@59275	542	\| Group' of con * int list * term \| Init_Proof' of cterm' list * spec
wneuper@59275	543	\| Model_Problem' of pblID * itm list * itm list \| Or_to_List' of term * term
wneuper@59275	544	\| Refine_Problem' of pblID * (itm list * (bool * term) list)
wneuper@59275	545	\| Refine_Tacitly' of pblID * pblID * domID * metID * itm list
wneuper@59275	546	\| Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * (term * term list)
wneuper@59275	547	\| Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * (term * term list)
wneuper@59275	548	\| Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * (term * term list)
wneuper@59275	549	\| Rewrite_Set' of theory' * bool * rls * term * (term * term list)
wneuper@59275	550	\| Rewrite_Set_Inst' of theory' * bool * subst * rls * term * (term * term list)
wneuper@59275	551	\| Specify_Method' of metID * ori list * itm list
wneuper@59275	552	\| Specify_Problem' of pblID * (bool * (itm list * (bool * term) list)) \| Specify_Theory' of domID
wneuper@59275	553	\| Split_And' of term \| Split_Intersect' of term \| Split_Or' of term
wneuper@59275	554	\| Subproblem' of spec * ori list * term * fmz_ * Proof.context * term
wneuper@59275	555	\| Substitute' of rew_ord_ * rls * subte * term * term \| Tac_ of theory * string * string * string
wneuper@59275	556	\| Take' of term \| Take_Inst' of term
wneuper@59275	557	val tac_2str : tac_ -> string
wneuper@59275	558	val test_trans : ppobj -> bool
wneuper@59275	559	val thm_of_rew : tac -> thmID * subst option
wneuper@59275	560	val topt2str : term option -> string
wneuper@59279	561	val update_branch : ctree -> pos -> branch -> ctree
wneuper@59279	562	val update_ctxt : ctree -> pos -> Proof.context -> ctree
wneuper@59279	563	val update_domID : ctree -> pos -> domID -> ctree
wneuper@59279	564	val update_env : ctree -> pos -> (istate * Proof.context) option -> ctree
wneuper@59279	565	val update_loc' : ctree -> pos -> (istate * Proof.context) option * (istate * Proof.context) option -> ctree
wneuper@59279	566	val update_met : ctree -> pos -> itm list -> ctree
wneuper@59279	567	val update_metID : ctree -> pos -> metID -> ctree
wneuper@59279	568	val update_metppc : ctree -> pos -> itm list -> ctree
wneuper@59279	569	val update_oris : ctree -> pos -> ori list -> ctree
wneuper@59279	570	val update_orispec : ctree -> pos -> spec -> ctree
wneuper@59279	571	val update_pbl : ctree -> pos -> itm list -> ctree
wneuper@59279	572	val update_pblID : ctree -> pos -> pblID -> ctree
wneuper@59279	573	val update_pblppc : ctree -> pos -> itm list -> ctree
wneuper@59279	574	val update_spec : ctree -> pos -> spec -> ctree
wneuper@59279	575	val update_tac : ctree -> pos -> tac -> ctree end
wneuper@59275	576	*)
wneuper@59275	577
wneuper@59275	578	(**)
wneuper@59275	579	structure Ctree(): CALC_TREEE() =
wneuper@59275	580	struct
wneuper@59275	581	(**)
wneuper@59274	582	type result = term * term list
neuper@37906	583	type env = (term * term) list;
neuper@37906	584
neuper@37906	585	datatype branch =
wneuper@59274	586	NoBranch \| AndB \| OrB
wneuper@59274	587	\| TransitiveB (* FIXXXME.0308: set branch from met in Apply_Method
wneuper@59274	588	FIXXXME.0402: -"- in Begin_Trans'*)
wneuper@59274	589	\| SequenceB \| IntersectB \| CollectB \| MapB;
wneuper@59274	590
wneuper@59274	591	fun branch2str NoBranch = "NoBranch" (* for tests only *)
neuper@37906	592	\| branch2str AndB = "AndB"
neuper@37906	593	\| branch2str OrB = "OrB"
neuper@37906	594	\| branch2str TransitiveB = "TransitiveB"
neuper@37906	595	\| branch2str SequenceB = "SequenceB"
neuper@37906	596	\| branch2str IntersectB = "IntersectB"
neuper@37906	597	\| branch2str CollectB = "CollectB"
neuper@37906	598	\| branch2str MapB = "MapB";
neuper@37906	599
neuper@37906	600	datatype ostate =
wneuper@59274	601	Incomplete \| Complete \| Inconsistent (* WN041020 latter still unused *);
wneuper@59274	602	fun ostate2str Incomplete = "Incomplete" (* for tests only *)
neuper@37906	603	\| ostate2str Complete = "Complete"
neuper@37906	604	\| ostate2str Inconsistent = "Inconsistent";
neuper@37906	605
neuper@37906	606	type cellID = int;
neuper@37906	607	type cid = cellID list;
neuper@37906	608
wneuper@59274	609	type posel = int; (* for readability in funs accessing Ctree *)
wneuper@59274	610	type pos = int list;
neuper@37906	611	val pos2str = ints2str';
neuper@37906	612	datatype pos_ =
wneuper@59274	613	Pbl (* PblObj-position: problem-type *)
wneuper@59274	614	\| Met (* PblObj-position: method *)
wneuper@59274	615	\| Frm (* PblObj-position: -> Pbl in ME (not by moveDown !)
wneuper@59274	616	\| PrfObj-position: formula *)
wneuper@59274	617	\| Res (* PblObj \| PrfObj-position: result *)
wneuper@59274	618	\| Und; (* undefined*)
neuper@37906	619	fun pos_2str Pbl = "Pbl"
neuper@37906	620	\| pos_2str Met = "Met"
neuper@37906	621	\| pos_2str Frm = "Frm"
neuper@37906	622	\| pos_2str Res = "Res"
neuper@37906	623	\| pos_2str Und = "Und";
wneuper@59124	624	fun str2pos_ "Pbl" = Pbl
wneuper@59124	625	\| str2pos_ "Met" = Met
wneuper@59124	626	\| str2pos_ "Frm" = Frm
wneuper@59124	627	\| str2pos_ "Res" = Res
wneuper@59124	628	\| str2pos_ "Und" = Und
wneuper@59124	629	\| str2pos_ str = error ("str2pos_: wrong argument = " ^ str)
neuper@37906	630
neuper@37906	631	type pos' = pos * pos_;
wneuper@59279	632	(WN0312 remembering interator (pos pos_) for ctree
neuper@37906	633	pos : lev_on, lev_dn, lev_up,
neuper@42003	634	lev_onFrm, lev_dnRes (..see solve Apply_Method !)
neuper@42003	635	pos_:
neuper@37906	636	# generate1 sets pos_ if possible ...?WN0502?NOT...
neuper@37906	637	# generate1 does NOT set pos, because certain nodes can be lev_on OR lev_dn
neuper@37906	638	exceptions: Begin/End_Trans
neuper@37906	639	# thus generate(1) called in
neuper@37906	640	.# assy, locate_gen
neuper@37906	641	.# nxt_solv (tac_ -cases); general case:
neuper@37906	642	val pos' = case pos' of (p,Res) => (lev_on p',Res) \| _ => pos'
neuper@37906	643	# WN050220, S(604):
neuper@37906	644	generate1...(Rewrite(f,..,res))..(pos, pos_)
neuper@37906	645	cappend_atomic.................pos ////// gets f+res always!!!
neuper@37906	646	cut_tree....................pos, pos_
neuper@37906	647	*)
wneuper@59274	648	fun pos'2str (p, p_) = pair2str (ints2str' p, pos_2str p_);
wneuper@59274	649	fun pos's2str ps = (strs2str' o (map pos'2str)) ps; (* for tests only *)
wneuper@59274	650	val e_pos' = ([], Und);
neuper@37906	651
neuper@37906	652	fun res2str (t, ts) = pair2str (term2str t, terms2str ts);
neuper@37906	653
neuper@37906	654
neuper@37906	655
neuper@37906	656	(*26.4.02: never used after introduction of scripts !!!
neuper@37906	657	type loc = loc_ * (* + interpreter-state *)
neuper@37906	658	(loc_ * rls') (* -"- for script of the ruleset*)
neuper@37906	659	option;
neuper@37926	660	val e_loc = ([],NONE):loc;
neuper@37906	661	val ee_loc = (e_loc,e_loc);*)
neuper@37906	662
neuper@37906	663
neuper@37906	664	datatype safe = Sundef \| Safe \| Unsafe \| Helpless;
neuper@37906	665	fun safe2str Sundef = "Sundef"
neuper@37906	666	\| safe2str Safe = "Safe"
neuper@37906	667	\| safe2str Unsafe = "Unsafe"
neuper@37906	668	\| safe2str Helpless = "Helpless";
neuper@37906	669
neuper@37906	670	type subs = cterm' list; (16.11.00 for FE-KE)
neuper@37906	671	val e_subs = ["(bdv, x)"];
neuper@37906	672
neuper@42433	673	(* argument type of tac Rewrite_Inst *)
neuper@37906	674	type sube = cterm' list;
wneuper@59274	675	val e_sube = []: cterm' list;
neuper@37906	676	fun sube2str s = strs2str s;
neuper@37906	677
neuper@37906	678	(._sub_stitution as _t_erms of _e_qualities.)
neuper@37906	679	type subte = term list;
wneuper@59274	680	val e_subte = []: term list;
neuper@37906	681	fun subte2str ss = terms2str ss;
neuper@37906	682
neuper@42360	683	val subte2sube = map term2str;
neuper@42360	684	val subst2subs = map (pair2str o (apfst term2str) o (apsnd term2str));
wneuper@59159	685	fun subst2sube subst = map term2str (map HOLogic.mk_eq subst)
neuper@42360	686	val subst2subs' = map ((apfst term2str) o (apsnd term2str));
neuper@42385	687	fun subs2subst thy s = map (isapair2pair o (parse_patt thy)) s;
neuper@42385	688	fun sube2subst thy s = map (dest_equals' o (parse_patt thy)) s;
neuper@42360	689	val sube2subte = map str2term;
neuper@42360	690	val subte2subst = map HOLogic.dest_eq;
neuper@37906	691
neuper@37906	692	fun isasub2subst isasub = ((map isapair2pair) o isalist2list) isasub;
neuper@37906	693
neuper@37906	694	type scrstate = (state for script interpreter)
neuper@37906	695	env(stack) (*used to instantiate tac for checking assod
neuper@37906	696	12.03.noticed: e_ not updated during execution ?!?*)
neuper@37906	697	* loc_ (location of tac in script)
neuper@37906	698	* term option(argument of curried functions)
neuper@37906	699	* term (*value obtained by tac executed
neuper@37906	700	updated also after a derivation by 'new_val'*)
neuper@37906	701	* safe (estimation of how result will be obtained)
neuper@37906	702	* bool; (*true = strongly .., false = weakly associated:
neuper@37906	703	only used during ass_dn/up*)
wneuper@59274	704	val e_scrstate = ([],[],NONE,e_term,Sundef,false): scrstate;
neuper@42360	705	fun topt2str NONE = "NONE"
neuper@42360	706	\| topt2str (SOME t) = "SOME" ^ term2str t;
neuper@42360	707	fun scrstate2str (env, loc_, topt, t, safe, bool) =
neuper@42360	708	"(" ^ env2str env ^ ", " ^ loc_2str loc_ ^ ", " ^ topt2str topt ^ ", \n" ^
neuper@42360	709	term2str t ^ ", " ^ safe2str safe ^ ", " ^ bool2str bool ^ ")";
neuper@37906	710
neuper@41996	711	(* for handling type istate see fun from_pblobj_or_detail', +? *)
neuper@41996	712	datatype istate = (interpreter state)
neuper@41996	713	Uistate (undefined in modspec, in '_deriv'ation)
neuper@41996	714	\| ScrState of scrstate (for script interpreter)
neuper@41996	715	\| RrlsState of rrlsstate; (for reverse rewriting)
wneuper@59274	716	val e_istate = (ScrState ([],[],NONE,e_term,Sundef,false));
neuper@48761	717	val e_ctxt = Proof_Context.init_global @{theory "Pure"};
neuper@41992	718
neuper@41992	719	(* ATTENTION: does _not_ recognise Variable.declare_constraints, etc...*)
neuper@48761	720	fun is_e_ctxt ctxt = Theory.eq_thy (Proof_Context.theory_of ctxt, @{theory "Pure"});
neuper@37906	721
neuper@37906	722	type iist = istate option * istate option;
neuper@37906	723	(val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type)
neuper@37906	724
neuper@37906	725
neuper@37906	726	fun rta2str (r,(t,a)) = "\n("^(rule2str r)^",("^(term2str t)^", "^
neuper@37906	727	(terms2str a)^"))";
neuper@37906	728	fun istate2str Uistate = "Uistate"
wneuper@59274	729	\| istate2str (ScrState (e, l, to, t, s, b)) =
neuper@37906	730	"ScrState ("^ subst2str e ^",\n "^
neuper@37906	731	loc_2str l ^", "^ termopt2str to ^",\n "^
neuper@37906	732	term2str t ^", "^ safe2str s ^", "^ bool2str b ^")"
neuper@37906	733	\| istate2str (RrlsState (t,t1,rss,rtas)) =
neuper@37906	734	"RrlsState ("^(term2str t)^", "^(term2str t1)^", "^
neuper@37906	735	((strs2str o (map (strs2str o (map rule2str)))) rss)^", "^
neuper@37906	736	((strs2str o (map rta2str)) rtas)^")";
neuper@37925	737	fun istates2str (NONE, NONE) = "(#NONE, #NONE)"
neuper@37925	738	\| istates2str (NONE, SOME ist) = "(#NONE,\n#SOME "^istate2str ist^")"
neuper@37925	739	\| istates2str (SOME ist, NONE) = "(#SOME "^istate2str ist^",\n #NONE)"
neuper@37925	740	\| istates2str (SOME i1, SOME i2) = "(#SOME "^istate2str i1^",\n #SOME "^
wneuper@59274	741	istate2str i2 ^")";
neuper@37906	742
neuper@37906	743	fun new_val v (ScrState (env, loc_, topt, _, safe, bool)) =
neuper@37906	744	(ScrState (env, loc_, topt, v, safe, bool))
neuper@38031	745	\| new_val _ _ = error "new_val: only for ScrState";
neuper@37906	746
neuper@37906	747	datatype con = land \| lor;
neuper@37906	748
neuper@37906	749
neuper@37906	750
wneuper@59252	751	(*.tactics propagate the construction of the calc-tree;
neuper@37906	752	there are
neuper@37906	753	(a) 'specsteps' for the specify-phase, and others for the solve-phase
neuper@37906	754	(b) those of the solve-phase are 'initac's and others;
neuper@37906	755	initacs start with a formula different from the preceding formula.
neuper@37906	756	see 'type tac_' for the internal representation of tactics.*)
wneuper@59274	757	datatype tac = (* TODO: arrange according to signature *)
neuper@37906	758	Init_Proof of ((cterm' list) * spec)
neuper@37906	759	('specsteps'...)
neuper@37906	760	\| Model_Problem
neuper@37906	761	\| Refine_Problem of pblID \| Refine_Tacitly of pblID
neuper@37906	762
neuper@37906	763	\| Add_Given of cterm' \| Del_Given of cterm'
neuper@37906	764	\| Add_Find of cterm' \| Del_Find of cterm'
neuper@37906	765	\| Add_Relation of cterm' \| Del_Relation of cterm'
neuper@37906	766
neuper@37906	767	\| Specify_Theory of domID \| Specify_Problem of pblID
neuper@37906	768	\| Specify_Method of metID
neuper@37906	769	(...'specsteps')
neuper@37906	770	\| Apply_Method of metID
neuper@37906	771	(*.creates an 'istate' in PblObj.env; in case of 'init_form'
neuper@37906	772	creates a formula at ((lev_on o lev_dn) p, Frm) and in this ppobj.'loc'
neuper@37925	773	'SOME istate' (at fst of 'loc').
neuper@37906	774	As each step (in the solve-phase) has a resulting formula (at the front-end)
neuper@37906	775	Apply_Method also does the 1st step in the script (an 'initac') if there
neuper@37906	776	is no 'init_form' .*)
neuper@37906	777	\| Check_Postcond of pblID
neuper@37906	778	\| Free_Solve
neuper@37906	779
wneuper@59253	780	(* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
wneuper@59253	781	because there all the thms are present with both (thmID, thm)
wneuper@59253	782	(where user-views can show both or only one of (thmID, thm)),
wneuper@59253	783	and thm is created from ThmID by assoc_thm'' when entering isabisac *)
wneuper@59252	784	\| Rewrite_Inst of ( subs * thm'') \| Rewrite of thm'' \| Rewrite_Asm of thm''
neuper@37906	785	\| Rewrite_Set_Inst of ( subs * rls') \| Rewrite_Set of rls'
neuper@37906	786	\| Detail_Set_Inst of ( subs * rls') \| Detail_Set of rls'
neuper@37906	787	\| End_Detail (*end of script from next_tac,
neuper@37906	788	in solve: switches back to parent script WN0509 drop!*)
neuper@37906	789	\| Derive of rls' (an input formula using rls WN0509 drop!)
neuper@37906	790	\| Calculate of string (* plus \| minus \| times \| cancel \| pow \| sqrt *)
neuper@37906	791	\| End_Ruleset
neuper@37906	792	\| Substitute of sube \| Apply_Assumption of cterm' list
neuper@37906	793
neuper@37906	794	\| Take of cterm' (an 'initac')
neuper@37906	795	\| Take_Inst of cterm'
neuper@37906	796	\| Group of (con * int list )
neuper@37906	797	\| Subproblem of (domID * pblID) (an 'initac')
neuper@37906	798	\| CAScmd of cterm' (6.6.02 URD: Function formula; WN0509 drop!)
neuper@37906	799	\| End_Subproblem (WN0509 drop!)
neuper@37906	800
neuper@37906	801	\| Split_And \| Conclude_And
neuper@37906	802	\| Split_Or \| Conclude_Or
neuper@37906	803	\| Begin_Trans \| End_Trans
neuper@37906	804	\| Begin_Sequ \| End_Sequ(* substitute root.env *)
neuper@37906	805	\| Split_Intersect \| End_Intersect
neuper@37906	806	\| Check_elementwise of cterm' \| Collect_Trues
neuper@42394	807	\| Or_to_List (WN120315 ~ @{thm d2_prescind1},2,3,4 in PolyEq.thy )
neuper@37906	808
neuper@38051	809	\| Empty_Tac (* TODO.11.6.03 ... of string: could carry msg of (Notappl msg)
neuper@38051	810	in 'helpless'*)
neuper@38051	811	\| Tac of string (* eg.'repeat'WN0509 drop! (ab)used to report syntaxerror )
neuper@38051	812	\| End_Proof'; (* inout *)
neuper@37906	813
neuper@37906	814	(* tac2str /--> library.sml: needed in dialog.sml for 'separable *)
wneuper@59274	815	fun tac2str ma = case ma of
neuper@37906	816	Init_Proof (ppc, spec) =>
neuper@37906	817	"Init_Proof "^(pair2str (strs2str ppc, spec2str spec))
neuper@37906	818	\| Model_Problem => "Model_Problem "
neuper@37906	819	\| Refine_Tacitly pblID => "Refine_Tacitly "^(strs2str pblID)
neuper@37906	820	\| Refine_Problem pblID => "Refine_Problem "^(strs2str pblID)
neuper@37906	821	\| Add_Given cterm' => "Add_Given "^cterm'
neuper@37906	822	\| Del_Given cterm' => "Del_Given "^cterm'
neuper@37906	823	\| Add_Find cterm' => "Add_Find "^cterm'
neuper@37906	824	\| Del_Find cterm' => "Del_Find "^cterm'
neuper@37906	825	\| Add_Relation cterm' => "Add_Relation "^cterm'
neuper@37906	826	\| Del_Relation cterm' => "Del_Relation "^cterm'
neuper@37906	827
neuper@37906	828	\| Specify_Theory domID => "Specify_Theory "^(quote domID )
neuper@37906	829	\| Specify_Problem pblID => "Specify_Problem "^(strs2str pblID )
neuper@37906	830	\| Specify_Method metID => "Specify_Method "^(strs2str metID)
neuper@37906	831	\| Apply_Method metID => "Apply_Method "^(strs2str metID)
neuper@37906	832	\| Check_Postcond pblID => "Check_Postcond "^(strs2str pblID)
neuper@37906	833	\| Free_Solve => "Free_Solve"
neuper@37906	834
wneuper@59253	835	\| Rewrite_Inst (subs, (id, thm)) =>
wneuper@59253	836	"Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm \|> Thm.prop_of \|> term2str)))
wneuper@59253	837	\| Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm \|> Thm.prop_of \|> term2str)
wneuper@59253	838	\| Rewrite_Asm (id, thm) => "Rewrite_Asm " ^ spair2str (id, thm \|> Thm.prop_of \|> term2str)
neuper@37906	839	\| Rewrite_Set_Inst (subs, rls) =>
neuper@37906	840	"Rewrite_Set_Inst "^(pair2str (subs2str subs, quote rls))
neuper@37906	841	\| Rewrite_Set rls => "Rewrite_Set "^(quote rls )
neuper@37906	842	\| Detail_Set rls => "Detail_Set "^(quote rls )
neuper@37906	843	\| Detail_Set_Inst (subs, rls) =>
neuper@37906	844	"Detail_Set_Inst "^(pair2str (subs2str subs, quote rls))
neuper@37906	845	\| End_Detail => "End_Detail"
neuper@37906	846	\| Derive rls' => "Derive "^rls'
neuper@37906	847	\| Calculate op_ => "Calculate "^op_
neuper@37906	848	\| Substitute sube => "Substitute "^sube2str sube
neuper@37906	849	\| Apply_Assumption ct's => "Apply_Assumption "^(strs2str ct's)
neuper@37906	850
neuper@37906	851	\| Take cterm' => "Take "^(quote cterm' )
neuper@37906	852	\| Take_Inst cterm' => "Take_Inst "^(quote cterm' )
neuper@37906	853	\| Group (con, ints) =>
neuper@37906	854	"Group "^(pair2str (con2str con, ints2str ints))
neuper@37906	855	\| Subproblem (domID, pblID) =>
neuper@37906	856	"Subproblem "^(pair2str (domID, strs2str pblID))
neuper@37906	857	(*\| Subproblem_Full (spec, cts') =>
neuper@37906	858	"Subproblem_Full "^(pair2str (spec2str spec, strs2str cts'))*)
neuper@37906	859	\| End_Subproblem => "End_Subproblem"
neuper@37906	860	\| CAScmd cterm' => "CAScmd "^(quote cterm')
neuper@37906	861
neuper@37906	862	\| Check_elementwise cterm'=> "Check_elementwise "^(quote cterm')
neuper@37906	863	\| Or_to_List => "Or_to_List "
neuper@37906	864	\| Collect_Trues => "Collect_Trues"
neuper@37906	865
neuper@37906	866	\| Empty_Tac => "Empty_Tac"
neuper@37906	867	\| Tac string => "Tac "^string
neuper@37906	868	\| End_Proof' => "tac End_Proof'"
neuper@37906	869	\| _ => "tac2str not impl. for ?!";
neuper@37906	870
wneuper@59253	871	fun is_empty_tac tac = case tac of Empty_Tac => true \| _ => false
wneuper@59253	872
wneuper@59253	873	fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
wneuper@59253	874	\| eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
wneuper@59253	875	\| eq_tac (Rewrite_Set id1, Rewrite_Set id2) = id1 = id2
wneuper@59253	876	\| eq_tac (Rewrite_Set_Inst (_, id1), Rewrite_Set_Inst (_, id2)) = id1 = id2
wneuper@59253	877	\| eq_tac (Calculate id1, Calculate id2) = id1 = id2
wneuper@59253	878	\| eq_tac _ = false
wneuper@59253	879
neuper@37906	880	fun is_rewset (Rewrite_Set_Inst _) = true
neuper@37906	881	\| is_rewset (Rewrite_Set _) = true
neuper@37906	882	\| is_rewset _ = false;
neuper@37906	883	fun is_rewtac (Rewrite _) = true
neuper@37906	884	\| is_rewtac (Rewrite_Inst _) = true
neuper@37906	885	\| is_rewtac (Rewrite_Asm _) = true
neuper@37906	886	\| is_rewtac tac = is_rewset tac;
neuper@37906	887
wneuper@59274	888	fun tac2IDstr ma = case ma of
neuper@37906	889	Model_Problem => "Model_Problem"
neuper@37906	890	\| Refine_Tacitly pblID => "Refine_Tacitly"
neuper@37906	891	\| Refine_Problem pblID => "Refine_Problem"
neuper@37906	892	\| Add_Given cterm' => "Add_Given"
neuper@37906	893	\| Del_Given cterm' => "Del_Given"
neuper@37906	894	\| Add_Find cterm' => "Add_Find"
neuper@37906	895	\| Del_Find cterm' => "Del_Find"
neuper@37906	896	\| Add_Relation cterm' => "Add_Relation"
neuper@37906	897	\| Del_Relation cterm' => "Del_Relation"
neuper@37906	898
neuper@37906	899	\| Specify_Theory domID => "Specify_Theory"
neuper@37906	900	\| Specify_Problem pblID => "Specify_Problem"
neuper@37906	901	\| Specify_Method metID => "Specify_Method"
neuper@37906	902	\| Apply_Method metID => "Apply_Method"
neuper@37906	903	\| Check_Postcond pblID => "Check_Postcond"
neuper@37906	904	\| Free_Solve => "Free_Solve"
neuper@37906	905
neuper@37906	906	\| Rewrite_Inst (subs,thm')=> "Rewrite_Inst"
neuper@37906	907	\| Rewrite thm' => "Rewrite"
neuper@37906	908	\| Rewrite_Asm thm' => "Rewrite_Asm"
neuper@37906	909	\| Rewrite_Set_Inst (subs, rls) => "Rewrite_Set_Inst"
neuper@37906	910	\| Rewrite_Set rls => "Rewrite_Set"
neuper@37906	911	\| Detail_Set rls => "Detail_Set"
neuper@37906	912	\| Detail_Set_Inst (subs, rls) => "Detail_Set_Inst"
neuper@37906	913	\| Derive rls' => "Derive "
neuper@37906	914	\| Calculate op_ => "Calculate "
neuper@37906	915	\| Substitute subs => "Substitute"
neuper@37906	916	\| Apply_Assumption ct's => "Apply_Assumption"
neuper@37906	917
neuper@37906	918	\| Take cterm' => "Take"
neuper@37906	919	\| Take_Inst cterm' => "Take_Inst"
neuper@37906	920	\| Group (con, ints) => "Group"
neuper@37906	921	\| Subproblem (domID, pblID) => "Subproblem"
neuper@37906	922	\| End_Subproblem => "End_Subproblem"
neuper@37906	923	\| CAScmd cterm' => "CAScmd"
neuper@37906	924
neuper@37906	925	\| Check_elementwise cterm'=> "Check_elementwise"
neuper@37906	926	\| Or_to_List => "Or_to_List "
neuper@37906	927	\| Collect_Trues => "Collect_Trues"
neuper@37906	928
neuper@37906	929	\| Empty_Tac => "Empty_Tac"
neuper@37906	930	\| Tac string => "Tac "
neuper@37906	931	\| End_Proof' => "End_Proof'"
neuper@37906	932	\| _ => "tac2str not impl. for ?!";
neuper@37906	933
neuper@37906	934	fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
neuper@37906	935	\| rls_of (Rewrite_Set rls) = rls
neuper@38031	936	\| rls_of tac = error ("rls_of: called with tac '"^tac2IDstr tac^"'");
neuper@37906	937
neuper@37906	938	fun thm_of_rew (Rewrite_Inst (subs,(thmID,_))) =
wneuper@59274	939	(thmID, SOME ((subs2subst (assoc_thy "Isac") subs)))
neuper@37925	940	\| thm_of_rew (Rewrite (thmID,_)) = (thmID, NONE)
neuper@37925	941	\| thm_of_rew (Rewrite_Asm (thmID,_)) = (thmID, NONE);
neuper@37906	942
neuper@37906	943	fun rls_of_rewset (Rewrite_Set_Inst (subs,rls)) =
wneuper@59274	944	(rls, SOME ((subs2subst (assoc_thy "Isac") subs)))
neuper@37925	945	\| rls_of_rewset (Rewrite_Set rls) = (rls, NONE)
neuper@37925	946	\| rls_of_rewset (Detail_Set rls) = (rls, NONE)
neuper@37906	947	\| rls_of_rewset (Detail_Set_Inst (subs, rls)) =
wneuper@59274	948	(rls, SOME ((subs2subst (assoc_thy "Isac") subs)));
neuper@37906	949
s1210629013@52153	950	fun rule2tac thy _ (Calc (opID, thm)) = Calculate (assoc_calc thy opID)
wneuper@59253	951	\| rule2tac _ [] (Thm thm'') = Rewrite thm''
wneuper@59253	952	\| rule2tac _ subst (Thm thm'') =
wneuper@59253	953	Rewrite_Inst (subst2subs subst, thm'')
s1210629013@52153	954	\| rule2tac _ [] (Rls_ rls) = Rewrite_Set (id_rls rls)
s1210629013@52153	955	\| rule2tac _ subst (Rls_ rls) =
neuper@37906	956	Rewrite_Set_Inst (subst2subs subst, (id_rls rls))
s1210629013@52153	957	\| rule2tac _ _ rule =
neuper@38031	958	error ("rule2tac: called with '" ^ rule2str rule ^ "'");
neuper@37906	959
neuper@37906	960	type fmz_ = cterm' list;
neuper@37906	961
neuper@37906	962	(*.a formalization of an example containing data
neuper@37906	963	sufficient for mechanically finding the solution for the example.*)
neuper@37906	964	(*FIXME.WN051014: dont store fmz = (_,spec) in the PblObj,
neuper@37906	965	this is done in origin*)
neuper@37906	966	type fmz = fmz_ * spec;
neuper@37906	967	val e_fmz = ([],e_spec);
neuper@37906	968
neuper@42360	969	(* tac_ contains results from check in 'fun applicable_in'.
neuper@42360	970	This is useful for costly results, e.g. from rewriting;
neuper@42360	971	however, these results might be changed by Scripts like
neuper@42360	972	" eq = (Rewrite_Set ansatz_rls False) eql;" ^
neuper@42360	973	" eq = drop_questionmarks eq;" ^
neuper@42360	974	" eq = (Rewrite_Set equival_trans False) eq;" ^
neuper@42360	975	WN120106 TODO ANALOGOUSLY TO Substitute':
neuper@42360	976	So tac_ contains the term t the result was calculated from
neuper@42360	977	in order to compare t with t' possibly changed by "Expr "
neuper@42360	978	and re-calculate result if t<>t'*)
wneuper@59274	979	datatype tac_ = (* TODO: arrange according to signature *)
neuper@42023	980	Init_Proof' of ((cterm' list) * spec)
neuper@42023	981	\| Model_Problem' of
neuper@42023	982	pblID *
neuper@42023	983	itm list * (the 'untouched' pbl)
neuper@42023	984	itm list (the casually completed met)
neuper@42023	985	\| Refine_Tacitly' of
neuper@42023	986	pblID * (input)
neuper@42023	987	pblID * (the refined from applicable_in)
neuper@42023	988	domID * (from new pbt?! filled in specify)
neuper@42023	989	metID * (from new pbt?! filled in specify)
neuper@42023	990	itm list (*drop ! 9.03: remains [] for
neuper@37906	991	Model_Problem recognizing its activation*)
neuper@42023	992	\| Refine_Problem' of (pblID * (itm list * (bool * Term.term) list))
neuper@42023	993	(FIXME?040215 drop: done automatically in init_proof + Subproblem')
neuper@42023	994	\| Add_Given' of
neuper@42023	995	cterm' *
neuper@42023	996	itm list (updated with input in fun specify_additem)
neuper@42023	997	\| Add_Find' of cterm' * itm list (* see Add_Given' *)
neuper@42023	998	\| Add_Relation' of cterm' * itm list (* see Add_Given' *)
neuper@42023	999	\| Del_Given' of cterm' \| Del_Find' of cterm' \| Del_Relation' of cterm'
neuper@42023	1000	(4.00.: all.. term: in applicable_in ..? Syn ?only for FormFK?)
neuper@42023	1001	\| Specify_Theory' of domID
neuper@42023	1002	\| Specify_Problem' of
neuper@42023	1003	(pblID * (* *)
neuper@42023	1004	(bool * (* matches *)
neuper@42023	1005	(itm list * (* ppc *)
neuper@42023	1006	(bool * term) list))) (* preconditions *)
neuper@42023	1007	\| Specify_Method' of
neuper@42023	1008	metID *
neuper@42023	1009	ori list * (repl. "#undef")
neuper@42023	1010	itm list (... updated from pbl to met)
neuper@42023	1011	\| Apply_Method' of
neuper@42023	1012	metID *
neuper@42023	1013	(term option) * (init_form)
neuper@42023	1014	istate * Proof.context
neuper@42023	1015	\| Check_Postcond' of
neuper@42023	1016	pblID *
neuper@42023	1017	(term * (returnvalue of script in solve)
neuper@42023	1018	term list) (*collect by get_assumptions_ in applicable_in, except if
neuper@37906	1019	butlast tac is Check_elementwise: take only these asms*)
neuper@42023	1020	\| Free_Solve'
wneuper@55501	1021	(* context_thy would be simpler if instead thm' woudl be thm *)
wneuper@59253	1022	\| Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * (term * term list)
wneuper@59274	1023	\| Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * result
wneuper@59274	1024	\| Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * result
wneuper@59274	1025	\| Rewrite_Set_Inst' of theory' * bool * subst * rls * term * result
wneuper@59274	1026	\| Detail_Set_Inst' of theory' * bool * subst * rls * term * result
wneuper@59274	1027	\| Rewrite_Set' of theory' * bool * rls * term * result
wneuper@59274	1028	\| Detail_Set' of theory' * bool * rls * term * result
neuper@42023	1029	\| End_Detail' of (term * (term list)) (see End_Trans')
neuper@42023	1030	\| End_Ruleset' of term
neuper@42023	1031	\| Derive' of rls
neuper@42023	1032	\| Calculate' of theory' * string * term * (term * thm')
neuper@42023	1033	\| Substitute' of
neuper@42360	1034	rew_ord_ * (for re-calculation )
neuper@42360	1035	rls * (for re-calculation )
neuper@42360	1036	subte * (the 'substitution': terms of type bool)
neuper@42360	1037	term * (to be substituted in )
neuper@42360	1038	term (resulting from the substitution )
neuper@42023	1039	\| Apply_Assumption' of term list * term
neuper@42023	1040	\| Take' of term
neuper@42023	1041	\| Take_Inst' of term
neuper@42023	1042	\| Subproblem' of
neuper@42023	1043	(spec *
neuper@42023	1044	(ori list) * (* filled in assod Subproblem' *)
neuper@42023	1045	term * (-"-, headline of calc-head )
neuper@42023	1046	fmz_ *
neuper@42023	1047	Proof.context ( transported from assod to generate1 *)
neuper@42023	1048	term) (* Subproblem(dom,pbl) OR cascmd*)
neuper@42023	1049	\| CAScmd' of term
neuper@42023	1050	\| End_Subproblem' of term (???)
neuper@42023	1051	\| Split_And' of term \| Conclude_And' of term
neuper@42023	1052	\| Split_Or' of term \| Conclude_Or' of term
neuper@42023	1053	\| Begin_Trans' of term \| End_Trans' of (term * (term list))
neuper@42023	1054	\| Begin_Sequ' \| End_Sequ'(* substitute root.env*)
neuper@42023	1055	\| Split_Intersect' of term \| End_Intersect' of term
neuper@42023	1056	\| Check_elementwise' of (special case:)
neuper@42023	1057	term * ((1)the current formula: [x=1,x=...])
neuper@42023	1058	string * ((2)the pred from Check_elementwise )
neuper@42023	1059	(term * ((3)composed from (1) and (2): {x. pred})
neuper@42023	1060	term list) (20.5.03 assumptions)
neuper@42023	1061	\| Or_to_List' of term * term (* (a \| b, [a,b]) *)
neuper@42023	1062	\| Collect_Trues' of term
neuper@42023	1063	\| Empty_Tac_
neuper@42023	1064	\| Tac_ of (for dummies)
neuper@42023	1065	theory *
neuper@42023	1066	string * (form)
neuper@42023	1067	string * (in Tac)
neuper@42023	1068	string (result of Tac"..")
neuper@42023	1069	\| End_Proof'';(End_Proof:inout)
neuper@37906	1070
neuper@37906	1071	fun tac_2str ma = case ma of
neuper@37906	1072	Init_Proof' (ppc, spec) =>
neuper@37906	1073	"Init_Proof' "^(pair2str (strs2str ppc, spec2str spec))
neuper@37906	1074	\| Model_Problem' (pblID,_,_) => "Model_Problem' "^(strs2str pblID )
neuper@37906	1075	\| Refine_Tacitly'(p,prefin,domID,metID,itms)=>
neuper@37906	1076	"Refine_Tacitly' ("
neuper@37906	1077	^(strs2str p)^", "^(strs2str prefin)^", "
neuper@37906	1078	^domID^", "^(strs2str metID)^", pbl-itms)"
neuper@37906	1079	\| Refine_Problem' ms => "Refine_Problem' ("^(matchs2str ms)"..."^")"
neuper@37906	1080	(*\| Match_Problem' (pI, (ok, (itms, pre))) =>
neuper@37906	1081	"Match_Problem' "^(spair2str (strs2str pI,
neuper@37906	1082	spair2str (bool2str ok,
neuper@37924	1083	spair2str ("itms2str_ itms",
neuper@37906	1084	"items2str pre"))))*)
neuper@37906	1085	\| Add_Given' cterm' => "Add_Given' "(^cterm')
neuper@37906	1086	\| Del_Given' cterm' => "Del_Given' "(^cterm')
neuper@37906	1087	\| Add_Find' cterm' => "Add_Find' "(^cterm')
neuper@37906	1088	\| Del_Find' cterm' => "Del_Find' "(^cterm')
neuper@37906	1089	\| Add_Relation' cterm' => "Add_Relation' "(^cterm')
neuper@37906	1090	\| Del_Relation' cterm' => "Del_Relation' "(^cterm')
neuper@37906	1091
neuper@37906	1092	\| Specify_Theory' domID => "Specify_Theory' "^(quote domID )
neuper@37906	1093	\| Specify_Problem' (pI, (ok, (itms, pre))) =>
neuper@37906	1094	"Specify_Problem' "^(spair2str (strs2str pI,
neuper@37906	1095	spair2str (bool2str ok,
neuper@37924	1096	spair2str ("itms2str_ itms",
neuper@37906	1097	"items2str pre"))))
neuper@37906	1098	\| Specify_Method' (pI,oris,itms) =>
neuper@37906	1099	"Specify_Method' ("^metID2str pI^", "^oris2str oris^", )"
neuper@37906	1100
bonzai@41948	1101	\| Apply_Method' (metID,_,_,_) => "Apply_Method' "^(strs2str metID)
neuper@37906	1102	\| Check_Postcond' (pblID,(scval,asm)) =>
neuper@42018	1103	"Check_Postcond' " ^
neuper@42018	1104	(spair2str (strs2str pblID, spair2str (term2str scval, terms2str asm)))
neuper@37906	1105
neuper@37906	1106	\| Free_Solve' => "Free_Solve'"
neuper@37906	1107
neuper@37906	1108	\| Rewrite_Inst' (subs,thm') _ =>
neuper@37906	1109	"Rewrite_Inst' "(^(pair2str (subs2str subs, spair2str thm')))
neuper@37906	1110	\| Rewrite' thm' => "Rewrite' "(^(spair2str thm'))
neuper@37906	1111	\| Rewrite_Asm' thm' => "Rewrite_Asm' "(^(spair2str thm'))
neuper@37906	1112	\| Rewrite_Set_Inst' (subs,thm') _ =>
neuper@37906	1113	"Rewrite_Set_Inst' "(^(pair2str (subs2str subs, quote rls)))
neuper@38053	1114	\| Rewrite_Set' (thy', pasm, rls', f, (f', asm)) =>
neuper@38053	1115	"Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^ "," ^ id_rls rls' ^ "," ^
neuper@38053	1116	term2str f ^ ",(" ^ term2str f' ^ "," ^ terms2str asm ^ "))"
neuper@37906	1117	\| End_Detail' _ => "End_Detail' xxx"
neuper@37906	1118	\| Detail_Set' _ => "Detail_Set' xxx"
neuper@37906	1119	\| Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
neuper@37906	1120
neuper@37906	1121	\| Derive' rls => "Derive' "^id_rls rls
neuper@37906	1122	\| Calculate' _ => "Calculate' "
neuper@42360	1123	\| Substitute' _ => "Substitute' "(^(subs2str subs))
neuper@37906	1124	\| Apply_Assumption' ct's => "Apply_Assumption' "(^(strs2str ct's))
neuper@37906	1125
neuper@37906	1126	\| Take' cterm' => "Take' "(^(quote cterm' ))
neuper@37906	1127	\| Take_Inst' cterm' => "Take_Inst' "(^(quote cterm' ))
neuper@41983	1128	\| Subproblem' (spec, oris, _, _, _, pbl_form) =>
neuper@37906	1129	"Subproblem' "(^(pair2str (domID, strs2str ,...)))
neuper@37906	1130	\| End_Subproblem' _ => "End_Subproblem'"
neuper@37906	1131	\| CAScmd' cterm' => "CAScmd' "(^(quote cterm'))
neuper@37906	1132
neuper@37906	1133	\| Empty_Tac_ => "Empty_Tac_"
neuper@37906	1134	\| Tac_ (_,form,id,result) => "Tac_ (thy,"^form^","^id^","^result^")"
neuper@37906	1135	\| _ => "tac_2str not impl. for arg";
neuper@37906	1136
neuper@37906	1137	(*'executed tactics' (tac_s) with local environment etc.;
neuper@37906	1138	used for continuing eval script + for generate*)
neuper@37906	1139	type ets =
neuper@37906	1140	(loc_ * (* of tactic in scr, tactic (weakly) associated with tac_*)
neuper@37906	1141	(tac_ * (* (for generate) *)
neuper@37906	1142	env * (* with 'tactic=result' as a rule, tactic ev. _not_ ready:
neuper@37906	1143	for handling 'parallel let'*)
neuper@37906	1144	env * (* with results of (ready) tacs *)
neuper@37906	1145	term * (* itr_arg of tactic, for upd. env at Repeat, Try*)
neuper@37906	1146	term * (* result value of the tac *)
neuper@37906	1147	safe))
neuper@37906	1148	list;
wneuper@59274	1149	val Ets = []: ets;
neuper@37906	1150
neuper@37906	1151
neuper@37906	1152	fun ets2s (l,(m,eno,env,iar,res,s)) =
neuper@38053	1153	"\n(" ^ loc_2str l ^ ",(" ^ tac_2str m ^
neuper@38053	1154	",\n ens= " ^ subst2str eno ^
neuper@38053	1155	",\n env= " ^ subst2str env ^
neuper@38053	1156	",\n iar= " ^ term2str iar ^
neuper@38053	1157	",\n res= " ^ term2str res ^
neuper@38053	1158	",\n " ^ safe2str s ^ "))";
wneuper@59274	1159	fun ets2str (ets: ets) = (strs2str o (map ets2s)) ets;
neuper@37906	1160
neuper@37906	1161
wneuper@59279	1162	type envp =(9.5.03: unused, delete with field in ctree.PblObj FIXXXME)
neuper@37906	1163	(int * term list) list * (assoc-list: args of met)
neuper@37906	1164	(int * rls) list * (assoc-list: tacs already done ///15.9.00)
neuper@37906	1165	(int * ets) list * (assoc-list: tacs etc. already done)
neuper@37906	1166	(string * pos) list; (asms from where*)
wneuper@59274	1167	val empty_envp = ([], [], [], []): envp;
neuper@37906	1168
wneuper@59274	1169	datatype ppobj = (* TODO: arrange according to signature *)
neuper@41975	1170	PrfObj of
neuper@41975	1171	{cell : lrd option, (* where in form tac has been applied *)
neuper@41975	1172	(^^^FIXME.WN0607 rename this field)
neuper@41975	1173	form : term, (* where tac is applied to *)
neuper@41975	1174	tac : tac, (* also in istate *)
neuper@41977	1175	loc : (istate * (* script interpreter state *)
neuper@41977	1176	Proof.context) (* context for provers, type inference *)
neuper@41977	1177	option * (* both for interpreter location on Frm, Pbl, Met *)
neuper@41977	1178	(istate * (* script interpreter state *)
neuper@41977	1179	Proof.context) (* context for provers, type inference *)
neuper@41977	1180	option, (* both for interpreter location on Res *)
neuper@41977	1181	((NONE,NONE) <==> e_istate ! see update_loc, get_loc)
neuper@41975	1182	branch: branch, (* only rudimentary *)
wneuper@59274	1183	result: result, (* result and assumptions *)
neuper@41975	1184	ostate: ostate} (* Complete <=> result is OK *)
neuper@41975	1185	\| PblObj of
neuper@41975	1186	{cell : lrd option, (* unused: meaningful only for some _Prf_Obj *)
neuper@41975	1187	fmz : fmz, (* from init:FIXME never use this spec;-drop *)
neuper@41975	1188	origin: (ori list) * (* representation from fmz+pbt
neuper@41975	1189	for efficiently adding items in probl, meth *)
neuper@41977	1190	spec * (* updated by Refine_Tacitly *)
neuper@41977	1191	term, (* headline of calc-head, as calculated initially(!)*)
neuper@41975	1192	spec : spec, (* explicitly input *)
neuper@41975	1193	probl : itm list, (* itms explicitly input *)
neuper@41975	1194	meth : itm list, (* itms automatically added to copy of probl *)
neuper@41988	1195	ctxt : Proof.context, (* WN110513 introduced to avoid [] [])
neuper@41975	1196	env : (istate * Proof.context) option,
neuper@41977	1197	(* istate only for initac in script
neuper@41984	1198	context for specify phase on this node NO..
neuper@41990	1199	..NO: this conflicts with init_form/initac: see Apply_Method without init_form *)
neuper@41984	1200	loc : (istate * Proof.context) option * (istate * (* like PrfObj *)
neuper@41988	1201	Proof.context) option, (* for spec-phase [*], NO..
neuper@41988	1202	..NO: raises errors not tracable on WN110513 [*])
neuper@41977	1203	branch: branch, (* like PrfObj *)
wneuper@59274	1204	result: result, (* like PrfObj *)
neuper@41977	1205	ostate: ostate}; (* like PrfObj *)
neuper@37906	1206
neuper@37906	1207	(*.this tree contains isac's calculations; TODO.WN03 rename to ctree;
neuper@37906	1208	the structure has been copied from an early version of Theorema(c);
neuper@37906	1209	it has the disadvantage, that there is no space
neuper@37906	1210	for the first tactic in a script generating the first formula at (p,Frm);
neuper@37906	1211	this trouble has been covered by 'init_form' and 'Take' so far,
neuper@37906	1212	but it is crucial if the first tactic in a script is eg. 'Subproblem';
neuper@37906	1213	see 'type tac ', Apply_Method.
neuper@37906	1214	.*)
wneuper@59279	1215	datatype ctree =
neuper@37906	1216	EmptyPtree
wneuper@59279	1217	\| Nd of ppobj * (ctree list);
wneuper@59279	1218	val e_ctree = EmptyPtree;
wneuper@59279	1219	type state = ctree * pos
neuper@37906	1220
neuper@37906	1221	fun rep_prfobj (PrfObj {cell,form,tac,loc,branch,result,ostate}) =
neuper@37906	1222	{cell=cell,form=form,tac=tac,loc=loc,branch=branch,result=result,ostate=ostate};
neuper@41988	1223	fun rep_pblobj (PblObj {cell,origin,fmz,spec,probl,meth,ctxt,
neuper@41988	1224	env,loc,branch,result,ostate}) =
neuper@41988	1225	{cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,ctxt=ctxt,
neuper@41988	1226	env=env,loc=loc,branch=branch,result=result,ostate=ostate};
neuper@37906	1227	fun is_prfobj (PrfObj _) = true
neuper@37906	1228	\| is_prfobj _ =false;
neuper@37906	1229	(val is_prfobj' = get_obj is_prfobj; )
neuper@37906	1230	fun is_pblobj (PblObj _) = true
neuper@37906	1231	\| is_pblobj _ = false;
neuper@37906	1232	(val is_pblobj' = get_obj is_pblobj; 'Error: unbound constructor get_obj')
neuper@37906	1233
neuper@37906	1234
neuper@37906	1235	exception PTREE of string;
neuper@37906	1236	fun nth _ [] = raise PTREE "nth _ []"
neuper@37906	1237	\| nth 1 (x::xs) = x
neuper@37906	1238	\| nth n (x::xs) = nth (n-1) xs;
neuper@37906	1239	(> nth 2 [11,22,33]; -->> val it = 22 : int)
neuper@37906	1240
wneuper@59274	1241	fun lev_up [] = raise PTREE "lev_up []"
neuper@37906	1242	\| lev_up p = (drop_last p):pos;
wneuper@59274	1243	fun lev_on [] = raise PTREE "lev_on []"
neuper@37906	1244	\| lev_on pos =
neuper@37906	1245	let val len = length pos
neuper@37906	1246	in (drop_last pos) @ [(nth len pos)+1] end;
wneuper@59274	1247	fun lev_onFrm (p,_) = (lev_on p,Frm):pos'
neuper@37906	1248	\| lev_onFrm p = raise PTREE ("*** lev_onFrm: pos'="^(pos'2str p));
neuper@42427	1249	(040216: for inform --> embed_deriv: remains on same level TODO.WN120517 compare lev_pred)
wneuper@59274	1250	fun lev_back' ([],_) = raise PTREE "lev_back': called by ([],_)"
neuper@42427	1251	\| lev_back' (p,_) =
neuper@37906	1252	if last_elem p <= 1 then (p, Frm):pos'
neuper@37906	1253	else ((drop_last p) @ [(nth (length p) p) - 1], Res);
neuper@37906	1254	(.increase pos by n within a level.)
neuper@37906	1255	fun pos_plus 0 pos = pos
wneuper@59274	1256	\| pos_plus n (p,Frm) = pos_plus (n-1) (p, Res)
wneuper@59274	1257	\| pos_plus n (p, _) = pos_plus (n-1) (lev_on p, Res);
neuper@37906	1258
wneuper@59274	1259	fun lev_pred [] = raise PTREE "lev_pred []"
wneuper@59274	1260	\| lev_pred pos =
neuper@37906	1261	let val len = length pos
wneuper@59274	1262	in ((drop_last pos) @ [(nth len pos)-1]) end;
neuper@37906	1263	(*lev_pred [1,2,3];
neuper@37906	1264	val it = [1,2,2] : pos
neuper@37906	1265	> lev_pred [1];
neuper@37906	1266	val it = [0] : pos *)
neuper@37906	1267
neuper@37906	1268	fun lev_dn p = p @ [0];
neuper@37906	1269	(*> (lev_dn o lev_on) [1,2,3];
neuper@37906	1270	val it = [1,2,4,0] : pos *)
neuper@37906	1271	(fun lev_dn' ((p,p_):pos') = (lev_dn p, Frm):pos'; WN.3.12.03: never used)
wneuper@59274	1272	fun lev_dnRes (p,_) = (lev_dn p, Res);
neuper@37906	1273
neuper@37906	1274	(4.4.00)
wneuper@59274	1275	fun lev_up_ (p,Res) = (lev_up p,Res):pos'
neuper@38031	1276	\| lev_up_ p' = error ("lev_up_: called for "^(pos'2str p'));
wneuper@59274	1277	fun lev_dn_ (p, _) = (lev_dn p, Res)
wneuper@59274	1278	fun ind (p,_) = length p; (WN050108 deprecated in favour of lev_of)
wneuper@59274	1279	fun lev_of (p,_) = length p;
neuper@37906	1280
neuper@37906	1281
wneuper@59279	1282	( convert ctree to a string )
neuper@37906	1283
neuper@37906	1284	(* convert a pos from list to string *)
neuper@37906	1285	fun pr_pos ps = (space_implode "." (map string_of_int ps))^". ";
neuper@37906	1286	(* show hd origin or form only *)
wneuper@59274	1287	fun pr_short p (PblObj {origin = (ori,_,_),...}) =
neuper@37906	1288	((pr_pos p) ^ " ----- pblobj -----\n")
neuper@37929	1289	(* ((((Syntax.string_of_term (thy2ctxt' "Isac")) o #4 o hd) ori)^" "^
neuper@37929	1290	(((Syntax.string_of_term (thy2ctxt' "Isac")) o hd(!?!) o #5 o hd) ori))^
neuper@37906	1291	"\n") *)
neuper@37906	1292	\| pr_short p (PrfObj {form = form,...}) =
neuper@37906	1293	((pr_pos p) ^ (term2str form) ^ "\n");
neuper@37906	1294	(*
neuper@37906	1295	fun pr_cell (p:pos) (PblObj {cell = c, origin = (ori,_,_),...}) =
neuper@37906	1296	((ints2str c) ^" "^
neuper@37929	1297	((((Syntax.string_of_term (thy2ctxt' "Isac")) o #4 o hd) ori)^" "^
neuper@37929	1298	(((Syntax.string_of_term (thy2ctxt' "Isac")) o hd(!?!) o #5 o hd) ori))^
neuper@37906	1299	"\n")
neuper@37906	1300	\| pr_cell p (PrfObj {cell = c, form = form,...}) =
neuper@37906	1301	((ints2str c) ^" "^ (term2str form) ^ "\n");
neuper@37906	1302	*)
neuper@37906	1303
wneuper@59279	1304	(* convert ctree *)
wneuper@59279	1305	fun pr_ctree f pt =
neuper@37906	1306	let
neuper@37906	1307	fun pr_pt pfn _ EmptyPtree = ""
neuper@37906	1308	\| pr_pt pfn ps (Nd (b, [])) = pfn ps b
neuper@37906	1309	\| pr_pt pfn ps (Nd (b, ts)) = (pfn ps b)^
wneuper@59274	1310	(prts pfn ps 1 ts)
neuper@37906	1311	and prts pfn ps p [] = ""
neuper@37906	1312	\| prts pfn ps p (t::ts) = (pr_pt pfn (ps @ [p]) t)^
neuper@37906	1313	(prts pfn ps (p+1) ts)
neuper@37906	1314	in pr_pt f [] pt end;
neuper@37906	1315	(*
neuper@37906	1316	> fun prfn ps b = (pr_pos ps)^" "^b(TODO)^"\n";
neuper@55432	1317	(val pt = Unsynchronized.ref EmptyPtree;)
neuper@37986	1318	> pt:=Nd("root'",
neuper@37906	1319	[Nd("xx1",[]),
neuper@37906	1320	Nd("xx2",
neuper@37906	1321	[Nd("xx2.1.",[]),
neuper@37906	1322	Nd("xx2.2.",[])]),
neuper@37906	1323	Nd("xx3",[])]);
wneuper@59279	1324	> tracing (pr_ctree prfn (!pt));
neuper@37906	1325	*)
neuper@37906	1326
neuper@37906	1327
wneuper@59279	1328	( access the branches of ctree )
neuper@37906	1329
neuper@37906	1330	fun ins_nth 1 e l = e::l
neuper@37906	1331	\| ins_nth n e [] = raise PTREE "ins_nth n e []"
neuper@37906	1332	\| ins_nth n e (l::ls) = l::(ins_nth (n-1) e ls);
neuper@37906	1333	fun repl [] _ _ = raise PTREE "repl [] _ _"
neuper@37906	1334	\| repl (l::ls) 1 e = e::ls
neuper@37906	1335	\| repl (l::ls) n e = l::(repl ls (n-1) e);
neuper@37906	1336	fun repl_app ls n e =
neuper@37906	1337	let val lim = 1 + length ls
neuper@37906	1338	in if n > lim then raise PTREE "repl_app: n > lim"
neuper@37906	1339	else if n = lim then ls @ [e]
neuper@37906	1340	else repl ls n e end;
neuper@37906	1341	(*
neuper@37906	1342	> repl [1,2,3] 2 22222;
neuper@37906	1343	val it = [1,22222,3] : int list
neuper@37906	1344	> repl_app [1,2,3,4] 5 5555;
neuper@37906	1345	val it = [1,2,3,4,5555] : int list
neuper@37906	1346	> repl_app [1,2,3] 2 22222;
neuper@37906	1347	val it = [1,22222,3] : int list
neuper@37906	1348	> repl_app [1] 2 22222 ;
neuper@37906	1349	val it = [1,22222] : int list
neuper@37906	1350	*)
neuper@37906	1351
neuper@37906	1352
neuper@37906	1353	(.get from obj at pos by f : ppobj -> 'a.)
wneuper@59274	1354	fun get_obj f EmptyPtree _ = raise PTREE "get_obj f EmptyPtree"
neuper@37906	1355	\| get_obj f (Nd (b, _)) [] = f b
neuper@37906	1356	\| get_obj f (Nd (b, bs)) (p::ps) =
neuper@37906	1357	(* val (f, Nd (b, bs), (p::ps)) = (I, pt, p);
neuper@37906	1358	*)
neuper@37906	1359	let val _ = (nth p bs) handle _ => raise PTREE ("get_obj: pos = "^
neuper@37906	1360	(ints2str' (p::ps))^" does not exist");
wneuper@59274	1361	in (get_obj f (nth p bs) ps)
neuper@37906	1362	(before WN050419: 'wrong type..' raised also if pos doesn't exist)
neuper@37906	1363	handle _ => raise PTREE (*"get_obj: at pos = "^
neuper@37906	1364	(ints2str' (p::ps))^" wrong type of ppobj"*)
neuper@37906	1365	("get_obj: pos = "^
neuper@37906	1366	(ints2str' (p::ps))^" does not exist")
neuper@37906	1367	end;
neuper@37906	1368	fun get_nd EmptyPtree _ = raise PTREE "get_nd EmptyPtree"
neuper@37906	1369	\| get_nd n [] = n
wneuper@59274	1370	\| get_nd (Nd (_,nds)) (pos as p :: ps) = (get_nd (nth p nds) ps)
neuper@37906	1371	handle _ => raise PTREE ("get_nd: not existent pos = "^(ints2str' pos));
neuper@37906	1372
neuper@37906	1373	(* for use by get_obj *)
neuper@37925	1374	fun g_cell (PblObj {cell = c,...}) = NONE
neuper@37906	1375	\| g_cell (PrfObj {cell = c,...}) = c;(WN0607 hack for quick introduction of lrd + rewrite-at (thms, calcs))
neuper@37906	1376	fun g_form (PrfObj {form = f,...}) = f
neuper@37906	1377	\| g_form (PblObj {origin=(_,_,f),...}) = f;
neuper@37906	1378	fun g_form' (Nd (PrfObj {form = f,...}, _)) = f
neuper@37906	1379	\| g_form' (Nd (PblObj {origin=(_,_,f),...}, _)) = f;
neuper@37906	1380	(* \| g_form _ = raise PTREE "g_form not for PblObj";*)
neuper@37906	1381	fun g_origin (PblObj {origin = ori,...}) = ori
neuper@37906	1382	\| g_origin _ = raise PTREE "g_origin not for PrfObj";
neuper@37906	1383	fun g_fmz (PblObj {fmz = f,...}) = f
neuper@37906	1384	\| g_fmz _ = raise PTREE "g_fmz not for PrfObj";
neuper@37906	1385	fun g_spec (PblObj {spec = s,...}) = s
neuper@37906	1386	\| g_spec _ = raise PTREE "g_spec not for PrfObj";
neuper@37906	1387	fun g_pbl (PblObj {probl = p,...}) = p
neuper@37906	1388	\| g_pbl _ = raise PTREE "g_pbl not for PrfObj";
neuper@37906	1389	fun g_met (PblObj {meth = p,...}) = p
neuper@37906	1390	\| g_met _ = raise PTREE "g_met not for PrfObj";
neuper@37906	1391	fun g_domID (PblObj {spec = (d,_,_),...}) = d
neuper@37906	1392	\| g_domID _ = raise PTREE "g_metID not for PrfObj";
neuper@37906	1393	fun g_metID (PblObj {spec = (_,_,m),...}) = m
neuper@37906	1394	\| g_metID _ = raise PTREE "g_metID not for PrfObj";
neuper@41989	1395	fun g_ctxt (PblObj {ctxt, ...}) = ctxt
neuper@41989	1396	\| g_ctxt _ = raise PTREE "g_ctxt not for PrfObj";
neuper@37906	1397	fun g_env (PblObj {env,...}) = env
neuper@37906	1398	\| g_env _ = raise PTREE "g_env not for PrfObj";
neuper@37906	1399	fun g_loc (PblObj {loc = l,...}) = l
neuper@37906	1400	\| g_loc (PrfObj {loc = l,...}) = l;
neuper@37906	1401	fun g_branch (PblObj {branch = b,...}) = b
neuper@37906	1402	\| g_branch (PrfObj {branch = b,...}) = b;
neuper@37906	1403	fun g_tac (PblObj {spec = (d,p,m),...}) = Apply_Method m
neuper@37906	1404	\| g_tac (PrfObj {tac = m,...}) = m;
neuper@37906	1405	fun g_result (PblObj {result = r,...}) = r
neuper@37906	1406	\| g_result (PrfObj {result = r,...}) = r;
neuper@37906	1407	fun g_res (PblObj {result = (r,_),...}) = r
neuper@37906	1408	\| g_res (PrfObj {result = (r,_),...}) = r;
neuper@37906	1409	fun g_res' (Nd (PblObj {result = (r,_),...}, _)) = r
neuper@37906	1410	\| g_res' (Nd (PrfObj {result = (r,_),...}, _)) = r;
neuper@37906	1411	fun g_ostate (PblObj {ostate = r,...}) = r
neuper@37906	1412	\| g_ostate (PrfObj {ostate = r,...}) = r;
neuper@37906	1413	fun g_ostate' (Nd (PblObj {ostate = r,...}, _)) = r
neuper@37906	1414	\| g_ostate' (Nd (PrfObj {ostate = r,...}, _)) = r;
neuper@37906	1415
neuper@37925	1416	fun gpt_cell (Nd (PblObj {cell = c,...},_)) = NONE
neuper@37906	1417	\| gpt_cell (Nd (PrfObj {cell = c,...},_)) = c;
neuper@37906	1418
neuper@42428	1419	(* get the formula preceeding the current position in a calculation *)
neuper@42431	1420	fun get_curr_formula (pt, pos as (p, p_)) =
neuper@42428	1421	case p_ of
neuper@42428	1422	Frm => get_obj g_form pt p
neuper@42428	1423	\| Res => (fst o (get_obj g_result pt)) p
neuper@42428	1424	\| _ => #3 (get_obj g_origin pt p);
neuper@42428	1425
neuper@37906	1426	(*in CalcTree/Subproblem an 'just_created_' model is created;
neuper@37906	1427	this is filled to 'untouched' by Model/Refine_Problem*)
neuper@37906	1428	fun just_created_ (PblObj {meth, probl, spec, ...}) =
neuper@37906	1429	null meth andalso null probl andalso spec = e_spec;
wneuper@59274	1430	val e_origin = ([],e_spec,e_term);
neuper@37906	1431
wneuper@59274	1432	fun just_created (pt, (p, _)) =
neuper@37906	1433	let val ppobj = get_obj I pt p
neuper@37906	1434	in is_pblobj ppobj andalso just_created_ ppobj end;
neuper@37906	1435
neuper@37906	1436	(.does the pos in the ctree exist ?.)
neuper@37906	1437	fun existpt pos pt = can (get_obj I pt) pos;
neuper@37906	1438	(.does the pos' in the ctree exist, ie. extra check for result in the node.)
wneuper@59274	1439	fun existpt' (p,p_) pt =
neuper@37906	1440	if can (get_obj I pt) p
neuper@37906	1441	then case p_ of
neuper@37906	1442	Res => get_obj g_ostate pt p = Complete
neuper@37906	1443	\| _ => true
neuper@37906	1444	else false;
neuper@37906	1445
neuper@37906	1446	(.is this position appropriate for calculating intermediate steps?.)
wneuper@59274	1447	fun is_interpos (_, Res) = true
neuper@37906	1448	\| is_interpos _ = false;
neuper@37906	1449
neuper@37906	1450	fun last_onlev pt pos = not (existpt (lev_on pos) pt);
neuper@37906	1451
neuper@37906	1452
wneuper@59279	1453	(.find the position of the next parent which is a PblObj in ctree.)
wneuper@59274	1454	fun par_pblobj pt [] = []
neuper@37906	1455	\| par_pblobj pt p =
neuper@37906	1456	let fun par pt [] = []
neuper@37906	1457	\| par pt p = if is_pblobj (get_obj I pt p) then p
neuper@37906	1458	else par pt (lev_up p)
neuper@37906	1459	in par pt (lev_up p) end;
neuper@37906	1460	(* lev_up for hard_gen operating with pos = [...,0] *)
neuper@37906	1461
neuper@37906	1462	(.find the position and the children of the next parent which is a PblObj.)
wneuper@59274	1463	fun par_children (Nd (PblObj _, children)) [] = (children, [])
neuper@37906	1464	\| par_children (pt as Nd (PblObj _, children)) p =
neuper@37906	1465	let fun par [] = (children, [])
neuper@37906	1466	\| par p = let val Nd (obj, children) = get_nd pt p
neuper@37906	1467	in if is_pblobj obj then (children, p) else par (lev_up p)
neuper@37906	1468	end;
neuper@37906	1469	in par (lev_up p) end;
neuper@37906	1470
wneuper@59279	1471	(.get the children of a node in ctree.)
neuper@37906	1472	fun children (Nd (PblObj _, cn)) = cn
neuper@37906	1473	\| children (Nd (PrfObj _, cn)) = cn;
neuper@37906	1474
neuper@37906	1475
neuper@37906	1476	(*.find the next parent, which is either a PblObj (return true)
neuper@37906	1477	or a PrfObj with tac = Detail_Set (return false).*)
neuper@37906	1478	(FIXME.3.4.03:re-organize par_pbl_det after rls' --> rls)
wneuper@59274	1479	fun par_pbl_det pt [] = (true, [], Erls)
neuper@37906	1480	\| par_pbl_det pt p =
neuper@37906	1481	let fun par pt [] = (true, [], Erls)
neuper@37906	1482	\| par pt p = if is_pblobj (get_obj I pt p) then (true, p, Erls)
neuper@37906	1483	else case get_obj g_tac pt p of
neuper@37906	1484	(*Detail_Set rls' => (false, p, assoc_rls rls')
neuper@37906	1485	(^^^--- before 040206 after ---vvv)
neuper@37906	1486	\|*)Rewrite_Set rls' => (false, p, assoc_rls rls')
neuper@37906	1487	\| Rewrite_Set_Inst (_, rls') =>
neuper@37906	1488	(false, p, assoc_rls rls')
neuper@37906	1489	\| _ => par pt (lev_up p)
neuper@37906	1490	in par pt (lev_up p) end;
neuper@37906	1491
neuper@37906	1492
neuper@37906	1493
neuper@37906	1494
wneuper@59279	1495	(.get from the whole ctree by f : ppobj -> 'a.)
neuper@37906	1496	fun get_all f EmptyPtree = []
neuper@37906	1497	\| get_all f (Nd (b, [])) = [f b]
neuper@37906	1498	\| get_all f (Nd (b, bs)) = [f b] @ (get_alls f bs)
neuper@37906	1499	and get_alls f [] = []
neuper@37906	1500	\| get_alls f pts = flat (map (get_all f) pts);
neuper@37906	1501
neuper@37906	1502
wneuper@59279	1503	(*.insert obj b into ctree at pos, ev.overwriting this pos.
neuper@41931	1504	covers library.ML TODO.WN110315 rename*)
wneuper@59274	1505	fun insert_pt b EmptyPtree [] = Nd (b, [])
neuper@52111	1506	\| insert_pt b EmptyPtree _ = raise PTREE "insert_pt b Empty _"
neuper@52111	1507	\| insert_pt b (Nd ( _, _)) [] = raise PTREE "insert_pt b _ []"
neuper@52111	1508	\| insert_pt b (Nd (b', bs)) (p::[]) =
neuper@37906	1509	Nd (b', repl_app bs p (Nd (b,[])))
neuper@52111	1510	\| insert_pt b (Nd (b', bs)) (p::ps) =
neuper@52111	1511	Nd (b', repl_app bs p (insert_pt b (nth p bs) ps));
neuper@37906	1512	(*
neuper@37906	1513	> type ppobj = string;
wneuper@59279	1514	> tracing (pr_ctree prfn (!pt));
neuper@55432	1515	(val pt = Unsynchronized.ref Empty;)
neuper@52111	1516	pt:= insert_pt ("root'":ppobj) EmptyPtree [];
neuper@52111	1517	pt:= insert_pt ("xx1":ppobj) (!pt) [1];
neuper@52111	1518	pt:= insert_pt ("xx2":ppobj) (!pt) [2];
neuper@52111	1519	pt:= insert_pt ("xx3":ppobj) (!pt) [3];
neuper@52111	1520	pt:= insert_pt ("xx2.1":ppobj) (!pt) [2,1];
neuper@52111	1521	pt:= insert_pt ("xx2.2":ppobj) (!pt) [2,2];
neuper@52111	1522	pt:= insert_pt ("xx2.1.1":ppobj) (!pt) [2,1,1];
neuper@52111	1523	pt:= insert_pt ("xx2.1.2":ppobj) (!pt) [2,1,2];
neuper@52111	1524	pt:= insert_pt ("xx2.1.3":ppobj) (!pt) [2,1,3];
neuper@37906	1525	*)
neuper@37906	1526
neuper@37906	1527	(.insert children to a node without children.)
neuper@52111	1528	(compare: fun insert_pt)
wneuper@59274	1529	fun ins_chn _ EmptyPtree _ = raise PTREE "ins_chn: EmptyPtree"
neuper@37906	1530	\| ins_chn ns (Nd _) [] = raise PTREE "ins_chn: pos = []"
neuper@37906	1531	\| ins_chn ns (Nd (b, bs)) (p::[]) =
neuper@37906	1532	if p > length bs then raise PTREE "ins_chn: pos not existent"
neuper@37906	1533	else let val Nd (b', bs') = nth p bs
neuper@37906	1534	in if null bs' then Nd (b, repl_app bs p (Nd (b', ns)))
neuper@37906	1535	else raise PTREE "ins_chn: pos mustNOT be overwritten" end
neuper@37906	1536	\| ins_chn ns (Nd (b, bs)) (p::ps) =
neuper@37906	1537	Nd (b, repl_app bs p (ins_chn ns (nth p bs) ps));
neuper@37906	1538
neuper@52111	1539	(* print_depth 11;ins_chn;print_depth 3; ###insert_pt#########################*);
neuper@37906	1540
neuper@37906	1541
neuper@37906	1542	( apply f to obj at pos, f: ppobj -> ppobj )
neuper@37906	1543
neuper@37906	1544	fun appl_to_node f (Nd (b,bs)) = Nd (f b, bs);
neuper@37906	1545	fun appl_obj f EmptyPtree [] = EmptyPtree
neuper@37906	1546	\| appl_obj f EmptyPtree _ = raise PTREE "appl_obj f Empty _"
neuper@37906	1547	\| appl_obj f (Nd (b, bs)) [] = Nd (f b, bs)
neuper@37906	1548	\| appl_obj f (Nd (b, bs)) (p::[]) =
neuper@37906	1549	Nd (b, repl_app bs p (((appl_to_node f) o (nth p)) bs))
neuper@37906	1550	\| appl_obj f (Nd (b, bs)) (p::ps) =
neuper@37906	1551	Nd (b, repl_app bs p (appl_obj f (nth p bs) (ps:pos)));
neuper@37906	1552
neuper@37906	1553	(* for use by appl_obj *)
neuper@37906	1554	fun repl_form f (PrfObj {cell=c,form= _,tac=tac,loc=loc,
neuper@37906	1555	branch=branch,result=result,ostate=ostate}) =
neuper@37906	1556	PrfObj {cell=c,form= f,tac=tac,loc=loc,
neuper@37906	1557	branch=branch,result=result,ostate=ostate}
neuper@37906	1558	\| repl_form _ _ = raise PTREE "repl_form takes no PblObj";
neuper@37906	1559	fun repl_pbl x (PblObj {cell=cell,origin=origin,fmz=fmz,
neuper@41988	1560	spec=spec,probl=_,meth=meth,ctxt=ctxt,env=env,loc=loc,
neuper@37906	1561	branch=branch,result=result,ostate=ostate}) =
neuper@37906	1562	PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl= x,
neuper@41988	1563	meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
neuper@37906	1564	\| repl_pbl _ _ = raise PTREE "repl_pbl takes no PrfObj";
neuper@37906	1565	fun repl_met x (PblObj {cell=cell,origin=origin,fmz=fmz,
neuper@41988	1566	spec=spec,probl=probl,meth=_,ctxt=ctxt,env=env,loc=loc,
neuper@37906	1567	branch=branch,result=result,ostate=ostate}) =
neuper@37906	1568	PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
neuper@41988	1569	meth= x,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
neuper@37906	1570	\| repl_met _ _ = raise PTREE "repl_pbl takes no PrfObj";
neuper@37906	1571
neuper@37906	1572	fun repl_spec x (PblObj {cell=cell,origin=origin,fmz=fmz,
neuper@41988	1573	spec= _,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
neuper@37906	1574	branch=branch,result=result,ostate=ostate}) =
neuper@37906	1575	PblObj {cell=cell,origin=origin,fmz=fmz,spec= x,probl=probl,
neuper@41988	1576	meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
neuper@37906	1577	\| repl_spec _ _ = raise PTREE "repl_domID takes no PrfObj";
neuper@37906	1578	fun repl_domID x (PblObj {cell=cell,origin=origin,fmz=fmz,
neuper@41988	1579	spec=(_,p,m),probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
neuper@37906	1580	branch=branch,result=result,ostate=ostate}) =
neuper@37906	1581	PblObj {cell=cell,origin=origin,fmz=fmz,spec=(x,p,m),probl=probl,
neuper@41988	1582	meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
neuper@37906	1583	\| repl_domID _ _ = raise PTREE "repl_domID takes no PrfObj";
neuper@37906	1584	fun repl_pblID x (PblObj {cell=cell,origin=origin,fmz=fmz,
neuper@41988	1585	spec=(d,_,m),probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
neuper@37906	1586	branch=branch,result=result,ostate=ostate}) =
neuper@37906	1587	PblObj {cell=cell,origin=origin,fmz=fmz,spec=(d,x,m),probl=probl,
neuper@41988	1588	meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
neuper@37906	1589	\| repl_pblID _ _ = raise PTREE "repl_pblID takes no PrfObj";
neuper@37906	1590	fun repl_metID x (PblObj {cell=cell,origin=origin,fmz=fmz,
neuper@41988	1591	spec=(d,p,_),probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
neuper@37906	1592	branch=branch,result=result,ostate=ostate}) =
neuper@37906	1593	PblObj {cell=cell,origin=origin,fmz=fmz,spec=(d,p,x),probl=probl,
neuper@41988	1594	meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate}
neuper@37906	1595	\| repl_metID _ _ = raise PTREE "repl_metID takes no PrfObj";
neuper@37906	1596
neuper@37906	1597	fun repl_result l f' s (PrfObj {cell=cell,form=form,tac=tac,loc=_,
neuper@37906	1598	branch=branch,result = _ ,ostate = _}) =
neuper@37906	1599	PrfObj {cell=cell,form=form,tac=tac,loc= l,
neuper@37906	1600	branch=branch,result = f',ostate = s}
neuper@37906	1601	\| repl_result l f' s (PblObj {cell=cell,origin=origin,fmz=fmz,
neuper@41988	1602	spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=_,
neuper@37906	1603	branch=branch,result= _ ,ostate= _}) =
neuper@37906	1604	PblObj {cell=cell,origin=origin,fmz=fmz,
neuper@41988	1605	spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc= l,
neuper@37906	1606	branch=branch,result= f',ostate= s};
neuper@37906	1607
neuper@37906	1608	fun repl_tac x (PrfObj {cell=cell,form=form,tac= _,loc=loc,
neuper@37906	1609	branch=branch,result=result,ostate=ostate}) =
neuper@37906	1610	PrfObj {cell=cell,form=form,tac= x,loc=loc,
neuper@37906	1611	branch=branch,result=result,ostate=ostate}
neuper@37906	1612	\| repl_tac _ _ = raise PTREE "repl_tac takes no PblObj";
neuper@37906	1613
neuper@37906	1614	fun repl_branch b (PblObj {cell=cell,origin=origin,fmz=fmz,
neuper@41988	1615	spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
neuper@37906	1616	branch= _,result=result,ostate=ostate}) =
neuper@37906	1617	PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
neuper@41988	1618	meth=meth,ctxt=ctxt,env=env,loc=loc,branch= b,result=result,ostate=ostate}
neuper@37906	1619	\| repl_branch b (PrfObj {cell=cell,form=form,tac=tac,loc=loc,
neuper@37906	1620	branch= _,result=result,ostate=ostate}) =
neuper@37906	1621	PrfObj {cell=cell,form=form,tac=tac,loc=loc,
neuper@37906	1622	branch= b,result=result,ostate=ostate};
neuper@37906	1623
neuper@41989	1624	fun repl_ctxt x
neuper@41989	1625	(PblObj {cell, origin, fmz, spec, probl, meth,
neuper@41989	1626	ctxt=_, env, loc, branch, result, ostate}) =
neuper@41989	1627	PblObj {cell=cell, origin=origin, fmz=fmz, spec=spec, probl=probl, meth=meth,
neuper@41989	1628	ctxt=x, env=env, loc=loc, branch=branch, result=result, ostate=ostate}
neuper@41989	1629	\| repl_ctxt _ _ = raise PTREE "repl_env takes no PrfObj";
neuper@41989	1630
neuper@37906	1631	fun repl_env e
neuper@41989	1632	(PblObj {cell=cell, origin=origin, fmz=fmz, spec=spec, probl=probl, meth=meth,
neuper@41989	1633	ctxt=ctxt, env=_, loc=loc, branch=branch, result=result, ostate=ostate}) =
neuper@41989	1634	PblObj {cell=cell, origin=origin, fmz=fmz, spec=spec, probl=probl, meth=meth,
neuper@41989	1635	ctxt=ctxt, env=e, loc=loc, branch=branch, result=result, ostate=ostate}
neuper@41989	1636	\| repl_env _ _ = raise PTREE "repl_env takes no PrfObj";
neuper@37906	1637
neuper@37906	1638	fun repl_oris oris
neuper@37906	1639	(PblObj {cell=cell,origin=(_,spe,hdf),fmz=fmz,
neuper@41988	1640	spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
neuper@37906	1641	branch=branch,result=result,ostate=ostate}) =
neuper@37906	1642	PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl,
neuper@41988	1643	meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,
neuper@37906	1644	result=result,ostate=ostate}
neuper@37906	1645	\| repl_oris _ _ = raise PTREE "repl_oris takes no PrfObj";
neuper@37906	1646	fun repl_orispec spe
neuper@37906	1647	(PblObj {cell=cell,origin=(oris,_,hdf),fmz=fmz,
neuper@41988	1648	spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc,
neuper@37906	1649	branch=branch,result=result,ostate=ostate}) =
neuper@37906	1650	PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl,
neuper@41988	1651	meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,
neuper@37906	1652	result=result,ostate=ostate}
neuper@37906	1653	\| repl_orispec _ _ = raise PTREE "repl_orispec takes no PrfObj";
neuper@37906	1654
neuper@41988	1655	fun repl_loc l (PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,
neuper@41988	1656	ctxt=ctxt,env=env,loc=_,branch=branch,result=result,ostate=ostate}) =
neuper@41988	1657	PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,
neuper@41988	1658	ctxt=ctxt,env=env,loc=l,branch=branch,result=result,ostate=ostate}
neuper@41983	1659	\| repl_loc l (PrfObj {cell=cell,form=form,tac=tac,
neuper@41983	1660	loc=_,branch=branch,result=result,ostate=ostate}) =
neuper@41983	1661	PrfObj {cell=cell,form=form,tac=tac,
neuper@41983	1662	loc= l,branch=branch,result=result,ostate=ostate};
neuper@37906	1663
neuper@37906	1664	(WN050219 put here for interpreting code for cut_tree below...)
neuper@37906	1665	type ocalhd =
neuper@37906	1666	bool * (ALL itms+preconds true)
neuper@37906	1667	pos_ * (model belongs to Problem \| Method)
neuper@37906	1668	term * (*header: Problem... or Cas
neuper@37906	1669	FIXXXME.12.03: item! for marking syntaxerrors*)
neuper@37906	1670	itm list * (model: given, find, relate)
neuper@37906	1671	((bool * term) list) (model: preconds*)
neuper@37906	1672	spec; (specification)
neuper@37906	1673	val e_ocalhd = (false, Und, e_term, [e_itm], [(false, e_term)], e_spec);
neuper@37906	1674
wneuper@59152	1675	datatype ptform = Form of term \| ModSpec of ocalhd;
neuper@37906	1676	val e_ptform = Form e_term;
neuper@37906	1677	val e_ptform' = ModSpec e_ocalhd;
neuper@37906	1678
neuper@37906	1679	(*.applies (snd f) to the branches at a pos if ((fst f) b),
wneuper@59279	1680	f : (ppobj -> bool) * (int -> ctree list -> ctree list).*)
neuper@37906	1681
neuper@37906	1682	fun appl_branch f EmptyPtree [] = (EmptyPtree, false)
neuper@37906	1683	\| appl_branch f EmptyPtree _ = raise PTREE "appl_branch f Empty _"
neuper@37906	1684	\| appl_branch f (Nd ( _, _)) [] = raise PTREE "appl_branch f _ []"
neuper@37906	1685	\| appl_branch f (Nd (b, bs)) (p::[]) =
wneuper@59274	1686	if (fst f) b then (Nd (b, (snd f) p bs), true)
neuper@37906	1687	else (Nd (b, bs), false)
neuper@37906	1688	\| appl_branch f (Nd (b, bs)) (p::ps) =
neuper@37906	1689	let val (b',bool) = appl_branch f (nth p bs) ps
neuper@37906	1690	in (Nd (b, repl_app bs p b'), bool) end;
neuper@37906	1691
neuper@37906	1692	(* for cut_level; appl_branch(deprecated) *)
neuper@37906	1693	fun test_trans (PrfObj{branch = Transitive,...}) = true
neuper@37906	1694	\| test_trans (PblObj{branch = Transitive,...}) = true
neuper@37906	1695	\| test_trans _ = false;
neuper@37906	1696
wneuper@59274	1697	fun is_pblobj' pt p =
neuper@37906	1698	let val ppobj = get_obj I pt p
neuper@37906	1699	in is_pblobj ppobj end;
neuper@37906	1700
wneuper@59274	1701	fun delete_result pt p =
neuper@37925	1702	(appl_obj (repl_result (fst (get_obj g_loc pt p), NONE)
neuper@37906	1703	(e_term,[]) Incomplete) pt p);
neuper@37906	1704
neuper@37906	1705	fun del_res (PblObj {cell, fmz, origin, spec, probl, meth,
neuper@41988	1706	ctxt, env, loc=(l1,_), branch, result, ostate}) =
neuper@37906	1707	PblObj {cell=cell,fmz=fmz,origin=origin,spec=spec,probl=probl,meth=meth,
neuper@41988	1708	ctxt=ctxt,env=env, loc=(l1,NONE), branch=branch, result=(e_term,[]),
neuper@37906	1709	ostate=Incomplete}
neuper@37906	1710
neuper@37906	1711	\| del_res (PrfObj {cell, form, tac, loc=(l1,_), branch, result, ostate}) =
neuper@37925	1712	PrfObj {cell=cell,form=form,tac=tac, loc=(l1,NONE), branch=branch,
neuper@37906	1713	result=(e_term,[]), ostate=Incomplete};
neuper@37906	1714
neuper@42009	1715	(FIXME.WN0312 update_X X pos pt -> pt could be chained by o (efficiency?))
neuper@42009	1716	(fun update_fmz pt pos x = appl_obj (repl_fmz x) pt pos; WN01xx )
neuper@41996	1717	fun update_ctxt pt pos x = appl_obj (repl_ctxt x) pt pos; (*for use on PblObj,
neuper@42394	1718	otherwise use fun generate1; compare fun get_ctxt*)
neuper@37906	1719	fun update_env pt pos x = appl_obj (repl_env x) pt pos;
neuper@37906	1720	fun update_domID pt pos x = appl_obj (repl_domID x) pt pos;
neuper@37906	1721	fun update_pblID pt pos x = appl_obj (repl_pblID x) pt pos;
neuper@37906	1722	fun update_metID pt pos x = appl_obj (repl_metID x) pt pos;
neuper@37906	1723	fun update_spec pt pos x = appl_obj (repl_spec x) pt pos;
neuper@37906	1724	fun update_pbl pt pos x = appl_obj (repl_pbl x) pt pos;
neuper@37906	1725	fun update_pblppc pt pos x = appl_obj (repl_pbl x) pt pos;
neuper@37906	1726	fun update_met pt pos x = appl_obj (repl_met x) pt pos;
neuper@41990	1727	fun update_metppc pt pos x = appl_obj (repl_met x) pt pos;
neuper@37906	1728	fun update_branch pt pos x = appl_obj (repl_branch x) pt pos;
neuper@41990	1729	fun update_tac pt pos x = appl_obj (repl_tac x) pt pos;
neuper@37906	1730	fun update_oris pt pos x = appl_obj (repl_oris x) pt pos;
neuper@42009	1731	fun update_orispec pt pos x = appl_obj (repl_orispec x) pt pos;
neuper@37906	1732
neuper@42009	1733	(WN050305 for handling cut_tree in cappend_atomic + for testing)
neuper@42009	1734	fun update_loc' pt pos x = appl_obj (repl_loc x) pt pos;
neuper@37906	1735
neuper@37906	1736	(13.8.02: options, because istate is no equalitype any more)
bonzai@41948	1737	fun get_loc EmptyPtree _ = (e_istate, e_ctxt)
neuper@37906	1738	\| get_loc pt (p,Res) =
neuper@37906	1739	(case get_obj g_loc pt p of
neuper@37925	1740	(SOME i, NONE) => i
bonzai@41948	1741	\| (NONE , NONE) => (e_istate, e_ctxt)
neuper@37925	1742	\| (_ , SOME i) => i)
neuper@37906	1743	\| get_loc pt (p,_) =
neuper@37906	1744	(case get_obj g_loc pt p of
neuper@37925	1745	(NONE , SOME i) => i (13.8.02 just copied from ^^^: too liberal ?)
bonzai@41948	1746	\| (NONE , NONE) => (e_istate, e_ctxt)
neuper@37925	1747	\| (SOME i, _) => i);
bonzai@41953	1748	fun get_istate pt p = get_loc pt p \|> #1;
neuper@41990	1749	fun get_ctxt pt (pos as (p, p_)) =
neuper@41990	1750	if member op = [Frm, Res] p_
neuper@41990	1751	then get_loc pt pos \|> #2 (for script interpretation rely on fun get_loc)
neuper@41990	1752	else get_obj g_ctxt pt p (for specify phase take ctx from PblObj)
neuper@37906	1753
e0726734@41957	1754	fun get_assumptions_ pt p = get_ctxt pt p \|> get_assumptions;
neuper@37906	1755
neuper@37906	1756	(*pos of the formula on FE relative to the current pos,
neuper@37906	1757	which is the next writepos*)
wneuper@59274	1758	fun pre_pos [] = []
neuper@37906	1759	\| pre_pos pp =
neuper@37906	1760	let val (ps,p) = split_last pp
neuper@37906	1761	in case p of 1 => ps \| n => ps @ [n-1] end;
neuper@37906	1762
neuper@37906	1763	(WN.20.5.03 ... but not used)
neuper@37906	1764	fun posless [] (_::_) = true
neuper@37906	1765	\| posless (_::_) [] = false
neuper@37906	1766	\| posless (p::ps) (q::qs) = if p = q then posless ps qs else p < q;
neuper@37906	1767	(* posless [2,3,4] [3,4,5];
neuper@37906	1768	true
neuper@37906	1769	> posless [2,3,4] [1,2,3];
neuper@37906	1770	false
neuper@37906	1771	> posless [2,3] [2,3,4];
neuper@37906	1772	true
neuper@37906	1773	> posless [2,3,4] [2,3];
neuper@37906	1774	false
neuper@37906	1775	> posless [6] [6,5,2];
neuper@37906	1776	true
neuper@37906	1777	+++ see Isabelle/../library.ML*)
neuper@37906	1778
neuper@37906	1779
wneuper@59279	1780	(.development for extracting an 'interval' from ctree.)
neuper@37906	1781
neuper@41990	1782	(*WN0510 version stopped in favour of get_interval with !!!move_dn, getFormulaeFromTo
neuper@37906	1783	actually used (inefficient) version with move_dn: see modspec.sml*)
neuper@37906	1784	local
neuper@37906	1785
neuper@37906	1786	fun hdp [] = 1 \| hdp [0] = 1 \| hdp x = hd x;(start with first)
neuper@37906	1787	fun hdq [] = 99999 \| hdq [0] = 99999 \| hdq x = hd x;(take until last)
neuper@37906	1788	fun tlp [] = [0] \| tlp [_] = [0] \| tlp x = tl x;
neuper@37906	1789	fun tlq [] = [99999] \| tlq [_] = [99999] \| tlq x = tl x;
neuper@37906	1790
neuper@37906	1791	fun getnd i (b,p) q (Nd (po, nds)) =
neuper@37906	1792	(if i <= 0 then [[b]] else []) @
neuper@37906	1793	(getnds (i-1) true (b@[hdp p], tlp p) (tlq q)
neuper@37906	1794	(take_fromto (hdp p) (hdq q) nds))
neuper@37906	1795
neuper@37906	1796	and getnds _ _ _ _ [] = [] (no children)
neuper@37906	1797	\| getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (l+r-margin)
neuper@37906	1798
neuper@37906	1799	\| getnds i true (b,p) q [n1, n2] = (l-margin, r-margin)
neuper@37906	1800	(getnd i ( b, p ) [99999] n1) @
neuper@37906	1801	(getnd ~99999 (lev_on b,[0]) q n2)
neuper@37906	1802
neuper@37906	1803	\| getnds i _ (b,p) q [n1, n2] = (intern, r-margin)
neuper@37906	1804	(getnd i ( b,[0]) [99999] n1) @
neuper@37906	1805	(getnd ~99999 (lev_on b,[0]) q n2)
neuper@37906	1806
neuper@37906	1807	\| getnds i true (b,p) q (nd::(nds as _::_)) = (l-margin, intern)
neuper@37906	1808	(getnd i ( b, p ) [99999] nd) @
neuper@37906	1809	(getnds ~99999 false (lev_on b,[0]) q nds)
neuper@37906	1810
neuper@37906	1811	\| getnds i _ (b,p) q (nd::(nds as _::_)) = (intern, ...)
neuper@37906	1812	(getnd i ( b,[0]) [99999] nd) @
neuper@37906	1813	(getnds ~99999 false (lev_on b,[0]) q nds);
neuper@37906	1814	in
wneuper@59279	1815	(*get an 'interval from to' from a ctree as 'intervals f t' of respective nodes
neuper@37906	1816	where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
neuper@37906	1817	(1) the 'f' are given
neuper@37906	1818	(1a) by 'from' if 'f' = the respective element of 'from' (left margin)
neuper@37906	1819	(1b) -inifinity, if 'f' > the respective element of 'from' (internal node)
neuper@37906	1820	(2) the 't' ar given
neuper@37906	1821	(2a) by 'to' if 't' = the respective element of 'to' (right margin)
neuper@37906	1822	(2b) inifinity, if 't' < the respective element of 'to (internal node)'
neuper@37906	1823	the 'f' and 't' are set by hdp,... *)
neuper@37906	1824	fun get_trace pt p q =
neuper@37906	1825	(flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q)))
neuper@37906	1826	(take_fromto (hdp p) (hdq q) (children pt));
neuper@37906	1827	end;
neuper@37906	1828
wneuper@59274	1829	fun get_somespec (dI,pI,mI) (dI',pI',mI') =
neuper@37906	1830	let val domID = if dI = e_domID
neuper@37906	1831	then if dI' = e_domID
neuper@38031	1832	then error"pt_extract: no domID in probl,origin"
neuper@37906	1833	else dI'
neuper@37906	1834	else dI
neuper@37906	1835	val pblID = if pI = e_pblID
neuper@37906	1836	then if pI' = e_pblID
neuper@38031	1837	then error"pt_extract: no pblID in probl,origin"
neuper@37906	1838	else pI'
neuper@37906	1839	else pI
neuper@37906	1840	val metID = if mI = e_metID
neuper@37906	1841	then if pI' = e_metID
neuper@38031	1842	then error"pt_extract: no metID in probl,origin"
neuper@37906	1843	else mI'
neuper@37906	1844	else mI
wneuper@59274	1845	in (domID, pblID, metID) end;
wneuper@59274	1846	fun get_somespec' (dI,pI,mI) (dI',pI',mI') =
neuper@37906	1847	let val domID = if dI = e_domID then dI' else dI
neuper@37906	1848	val pblID = if pI = e_pblID then pI' else pI
neuper@37906	1849	val metID = if mI = e_metID then mI' else mI
wneuper@59274	1850	in (domID, pblID, metID) end;
neuper@37906	1851
wneuper@59279	1852	(extract a formula or model from ctree for itms2itemppc or model2xml)
neuper@37906	1853	fun preconds2str bts =
neuper@37906	1854	(strs2str o (map (linefeed o pair2str o
neuper@37906	1855	(apsnd term2str) o
neuper@37906	1856	(apfst bool2str)))) bts;
wneuper@59274	1857	fun ocalhd2str (b, p, hdf, itms, prec, spec) =
neuper@37906	1858	"("^bool2str b^", "^pos_2str p^", "^term2str hdf^
neuper@37928	1859	", "^itms2str_ (thy2ctxt' "Isac") itms^
neuper@37906	1860	", "^preconds2str prec^", \n"^spec2str spec^" )";
neuper@37906	1861
neuper@37906	1862
neuper@37906	1863
neuper@37906	1864	fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj;
neuper@37906	1865
neuper@37906	1866
wneuper@59279	1867	(.functions for the 'ctree iterator' as seen from the FE-Kernel interface.)
neuper@37906	1868
wneuper@59279	1869	(*move one step down into existing nodes of ctree; regard TransitiveB
neuper@37906	1870	~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~##################
neuper@37906	1871	fun move_dn _ (Nd (c, ns)) ([],p_) = (root problem)
neuper@37906	1872	(* val (Nd (c, ns), ([],p_)) = (pt, get_pos cI uI);
neuper@37906	1873	*)
neuper@37906	1874	if is_pblobj c
neuper@37906	1875	then case p_ of (*Frm => ([], Pbl) 1.12.03
neuper@37906	1876	\|*) Res => raise PTREE "move_dn: end of calculation"
neuper@37906	1877	\| _ => if null ns (go down from Pbl + Met)
neuper@37906	1878	then raise PTREE "move_dn: solve problem not started"
neuper@37906	1879	else ([1], Frm)
neuper@37906	1880	else (case p_ of Res => raise PTREE "move_dn: end of (sub-)tree"
neuper@37906	1881	\| _ => if null ns
neuper@37906	1882	then raise PTREE "move_dn: pos not existent 1"
neuper@37906	1883	else ([1], Frm))
neuper@37906	1884
neuper@37906	1885	(iterate towards end of pos)
neuper@37906	1886	(* val (P,(Nd (_, ns)),(p::(ps as (_::_)),p_)) = ([]:pos, pt, get_pos cI uI);
neuper@37906	1887	val (P,(Nd (_, ns)),(p::(ps as (_::_)),p_)) = ((P@[p]),(nth p ns),(ps, p_));
neuper@37906	1888	*)
neuper@37906	1889	\| move_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
neuper@37906	1890	if p > length ns then raise PTREE "move_dn: pos not existent 2"
neuper@37906	1891	else move_dn ((P@[p]): pos) (nth p ns) (ps, p_)
neuper@37906	1892	(* val (P, (Nd (c, ns)), ([p], p_)) = ((P@[p]), (nth p ns), (ps, p_));
neuper@37906	1893	val (P, (Nd (c, ns)), ([p], p_)) = ([],pt,get_pos cI uI);
neuper@37906	1894	*)
neuper@37906	1895	\| move_dn P (Nd (c, ns)) ([p], p_) = (act on last element of pos)
neuper@37906	1896	if p > length ns then raise PTREE "move_dn: pos not existent 3"
neuper@37906	1897	else if is_pblnd (nth p ns) then
neuper@38015	1898	((*tracing("### move_dn: is_pblnd (nth p ns), P= "^ints2str' P^", \n"^
neuper@37906	1899	"length ns= "^((string_of_int o length) ns)^
neuper@37906	1900	", p= "^string_of_int p^", p_= "^pos_2str p_);*)
neuper@37906	1901	case p_ of Res => if p = length ns
neuper@37906	1902	then if g_ostate c = Complete then (P, Res)
neuper@37906	1903	else raise PTREE (ints2str' P^" not complete")
neuper@37906	1904	(FIXME here handle not-sequent-branches)
neuper@37906	1905	else if g_branch c = TransitiveB
neuper@37906	1906	andalso (not o is_pblnd o (nth (p+1))) ns
neuper@37906	1907	then (P@[p+1], Res)
neuper@37906	1908	else (P@[p+1], if is_pblnd (nth (p+1) ns)
neuper@37906	1909	then Pbl else Frm)
neuper@37906	1910	\| _ => if (null o children o (nth p)) ns (go down from Pbl)
neuper@37906	1911	then raise PTREE "move_dn: solve subproblem not started"
neuper@37906	1912	else (P @ [p, 1],
neuper@37906	1913	if (is_pblnd o hd o children o (nth p)) ns
neuper@37906	1914	then Pbl else Frm)
neuper@37906	1915	)
neuper@37906	1916	(* val (P, Nd (c, ns), ([p], p_)) = ([], pt, ([1], Frm));
neuper@37906	1917	*)
neuper@37906	1918	else case p_ of Frm => if (null o children o (nth p)) ns
neuper@37906	1919	(then if g_ostate c = Complete then (P@[p],Res))
neuper@37906	1920	then if g_ostate' (nth p ns) = Complete
neuper@37906	1921	then (P@[p],Res)
neuper@37906	1922	else raise PTREE "move_dn: pos not existent 4"
neuper@37906	1923	else (P @ [p, 1], (go down)
neuper@37906	1924	if (is_pblnd o hd o children o (nth p)) ns
neuper@37906	1925	then Pbl else Frm)
neuper@37906	1926	\| Res => if p = length ns
neuper@37906	1927	then
neuper@37906	1928	if g_ostate c = Complete then (P, Res)
neuper@37906	1929	else raise PTREE (ints2str' P^" not complete")
neuper@37906	1930	else
neuper@37906	1931	if g_branch c = TransitiveB
neuper@37906	1932	andalso (not o is_pblnd o (nth (p+1))) ns
neuper@37906	1933	then if (null o children o (nth (p+1))) ns
neuper@37906	1934	then (P@[p+1], Res)
neuper@37906	1935	else (P@[p+1,1], Frm)(040221)
neuper@37906	1936	else (P@[p+1], if is_pblnd (nth (p+1) ns)
neuper@37906	1937	then Pbl else Frm);
neuper@37906	1938	*)
wneuper@59279	1939	(*.move one step down into existing nodes of ctree; skip Res = Frm.nxt;
neuper@37906	1940	move_dn at the end of the calc-tree raises PTREE.*)
neuper@37906	1941	fun move_dn _ (Nd (c, ns)) ([],p_) = (root problem)
neuper@37906	1942	(case p_ of
neuper@37906	1943	Res => raise PTREE "move_dn: end of calculation"
neuper@37906	1944	\| _ => if null ns (go down from Pbl + Met)
neuper@37906	1945	then raise PTREE "move_dn: solve problem not started"
neuper@37906	1946	else ([1], Frm))
neuper@37906	1947	\| move_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =(iterate to end of pos)
neuper@37906	1948	if p > length ns then raise PTREE "move_dn: pos not existent 2"
wneuper@59274	1949	else move_dn (P@[p]) (nth p ns) (ps, p_)
neuper@37906	1950
neuper@37906	1951	\| move_dn P (Nd (c, ns)) ([p], p_) = (act on last element of pos)
neuper@37906	1952	if p > length ns then raise PTREE "move_dn: pos not existent 3"
neuper@37906	1953	else case p_ of
neuper@37906	1954	Res =>
neuper@37906	1955	if p = length ns (last Res on this level: go a level up)
neuper@37906	1956	then if g_ostate c = Complete then (P, Res)
neuper@37906	1957	else raise PTREE (ints2str' P^" not complete 1")
neuper@37906	1958	else (go to the next Nd on this level, or down into the next Nd)
neuper@37906	1959	if is_pblnd (nth (p+1) ns) then (P@[p+1], Pbl)
neuper@37906	1960	else
neuper@37906	1961	if g_res' (nth p ns) = g_form' (nth (p+1) ns)
neuper@37906	1962	then if (null o children o (nth (p+1))) ns
neuper@37906	1963	then (take the Res if Complete)
neuper@37906	1964	if g_ostate' (nth (p+1) ns) = Complete
neuper@37906	1965	then (P@[p+1], Res)
neuper@37906	1966	else raise PTREE (ints2str' (P@[p+1])^
neuper@37906	1967	" not complete 2")
neuper@37906	1968	else (P@[p+1,1], Frm)(go down into the next PrfObj)
neuper@37906	1969	else (P@[p+1], Frm)(take Frm: exists if the Nd exists)
neuper@37906	1970	\| Frm => (go down or to the Res of this Nd)
neuper@37906	1971	if (null o children o (nth p)) ns
neuper@37906	1972	then if g_ostate' (nth p ns) = Complete then (P @ [p], Res)
neuper@37906	1973	else raise PTREE (ints2str' (P @ [p])^" not complete 3")
neuper@37906	1974	else (P @ [p, 1], Frm)
neuper@37906	1975	\| _ => (is Pbl or Met)
neuper@37906	1976	if (null o children o (nth p)) ns
neuper@37906	1977	then raise PTREE "move_dn:solve subproblem not startd"
neuper@37906	1978	else (P @ [p, 1],
neuper@37906	1979	if (is_pblnd o hd o children o (nth p)) ns
neuper@37906	1980	then Pbl else Frm);
neuper@37906	1981
neuper@37906	1982
wneuper@59279	1983	(.go one level down into ctree.)
neuper@37906	1984	fun movelevel_dn [] (Nd (c, ns)) ([],p_) = (root problem)
neuper@37906	1985	if is_pblobj c
neuper@37906	1986	then if null ns
neuper@37906	1987	then raise PTREE "solve problem not started"
neuper@37906	1988	else ([1], if (is_pblnd o hd) ns then Pbl else Frm)
neuper@37906	1989	else raise PTREE "pos not existent 1"
neuper@37906	1990
neuper@37906	1991	(iterate towards end of pos)
neuper@37906	1992	\| movelevel_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
neuper@37906	1993	if p > length ns then raise PTREE "pos not existent 2"
neuper@37906	1994	else movelevel_dn (P@[p]) (nth p ns) (ps, p_)
neuper@37906	1995
neuper@37906	1996	\| movelevel_dn P (Nd (c, ns)) ([p], p_) = (act on last element of pos)
neuper@37906	1997	if p > length ns then raise PTREE "pos not existent 3" else
neuper@37906	1998	case p_ of Res =>
neuper@37906	1999	if p = length ns
neuper@37906	2000	then raise PTREE "no children"
neuper@37906	2001	else
neuper@37906	2002	if g_branch c = TransitiveB
neuper@37906	2003	then if (null o children o (nth (p+1))) ns
neuper@37906	2004	then raise PTREE "no children"
neuper@37906	2005	else (P @ [p+1, 1],
neuper@37906	2006	if (is_pblnd o hd o children o (nth (p+1))) ns
neuper@37906	2007	then Pbl else Frm)
neuper@37906	2008	else if (null o children o (nth p)) ns
neuper@37906	2009	then raise PTREE "no children"
neuper@37906	2010	else (P @ [p, 1], if (is_pblnd o hd o children o (nth p)) ns
neuper@37906	2011	then Pbl else Frm)
neuper@37906	2012	\| _ => if (null o children o (nth p)) ns
neuper@37906	2013	then raise PTREE "no children"
neuper@37906	2014	else (P @ [p, 1], (go down)
neuper@37906	2015	if (is_pblnd o hd o children o (nth p)) ns
neuper@37906	2016	then Pbl else Frm);
neuper@37906	2017
neuper@37906	2018
neuper@37906	2019
wneuper@59279	2020	(.go to the previous position in ctree; regard TransitiveB.)
wneuper@59274	2021	fun move_up _ (Nd (c, ns)) ([],p_) = (root problem)
neuper@37906	2022	if is_pblobj c
neuper@37906	2023	then case p_ of Res => if null ns then ([], Pbl) (Res -> Pbl (not Met)!)
neuper@37906	2024	else ([length ns], Res)
neuper@37906	2025	\| _ => raise PTREE "begin of calculation"
neuper@37906	2026	else raise PTREE "pos not existent"
neuper@37906	2027
neuper@37906	2028	\| move_up P (Nd (_, ns)) (p::(ps as (_::_)),p_) = (iterate to end of pos)
neuper@37906	2029	if p > length ns then raise PTREE "pos not existent"
neuper@37906	2030	else move_up (P@[p]) (nth p ns) (ps,p_)
neuper@37906	2031
neuper@37906	2032	\| move_up P (Nd (c, ns)) ([p], p_) = (act on last element of pos)
neuper@37906	2033	if p > length ns then raise PTREE "pos not existent"
neuper@37906	2034	else if is_pblnd (nth p ns) then
neuper@37906	2035	case p_ of Res =>
neuper@37906	2036	let val nc = (length o children o (nth p)) ns
neuper@37906	2037	in if nc = 0 then (P@[p], Pbl) (Res -> Pbl (not Met)!)
neuper@37906	2038	else (P @ [p, nc], Res) end (go down)
neuper@37906	2039	\| _ => if p = 1 then (P, Pbl) else (P@[p-1], Res)
neuper@37906	2040	else case p_ of Frm => if p <> 1 then (P, Frm)
neuper@37906	2041	else if is_pblobj c then (P, Pbl) else (P, Frm)
neuper@37906	2042	\| Res =>
neuper@37906	2043	let val nc = (length o children o (nth p)) ns
neuper@37906	2044	in if nc = 0 (cannot go down)
neuper@37906	2045	then if g_branch c = TransitiveB andalso p <> 1
neuper@37906	2046	then (P@[p-1], Res) else (P@[p], Frm)
neuper@37906	2047	else (P @ [p, nc], Res) end; (go down)
neuper@37906	2048
neuper@37906	2049
neuper@37906	2050
wneuper@59279	2051	(.go one level up in ctree; sets the position on Frm.)
neuper@37906	2052	fun movelevel_up _ (Nd (c, ns)) (([],p_):pos') = (root problem)
neuper@37906	2053	raise PTREE "pos not existent"
neuper@37906	2054
neuper@37906	2055	(iterate towards end of pos)
neuper@37906	2056	\| movelevel_up P (Nd (_, ns)) (p::(ps as (_::_)),p_) =
neuper@37906	2057	if p > length ns then raise PTREE "pos not existent"
neuper@37906	2058	else movelevel_up (P@[p]) (nth p ns) (ps,p_)
neuper@37906	2059
neuper@37906	2060	\| movelevel_up P (Nd (c, ns)) ([p], p_) = (act on last element of pos)
neuper@37906	2061	if p > length ns then raise PTREE "pos not existent"
neuper@37906	2062	else if is_pblobj c then (P, Pbl) else (P, Frm);
neuper@37906	2063
neuper@37906	2064
neuper@37906	2065	(.go to the next calc-head up in the calc-tree.)
neuper@37906	2066	fun movecalchd_up pt ((p, Res):pos') =
neuper@37906	2067	(par_pblobj pt p, Pbl):pos'
neuper@37906	2068	\| movecalchd_up pt (p, _) =
neuper@37906	2069	if is_pblobj (get_obj I pt p)
neuper@37906	2070	then (p, Pbl) else (par_pblobj pt p, Pbl);
neuper@37906	2071
neuper@37906	2072	(.determine the previous pos' on the same level.)
neuper@42427	2073	(WN0502 made for interSteps; _only_ works for branch TransitiveB WN120517 compare lev_back)
neuper@37906	2074	fun lev_pred' pt (pos:pos' as ([],Res)) = ([],Pbl):pos'
neuper@37906	2075	\| lev_pred' pt (pos:pos' as (p, Res)) =
neuper@37906	2076	let val (p', last) = split_last p
neuper@37906	2077	in if last = 1
neuper@37906	2078	then if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm)
neuper@37906	2079	else if get_obj g_res pt (p' @ [last - 1]) = get_obj g_form pt p
neuper@37906	2080	then (p' @ [last - 1], Res) (TransitiveB)
neuper@37906	2081	else if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm)
neuper@37906	2082	end;
neuper@37906	2083
neuper@42427	2084
neuper@37906	2085	(.determine the next pos' on the same level.)
neuper@37906	2086	fun lev_on' pt (([],Pbl):pos') = ([],Res):pos'
neuper@37906	2087	\| lev_on' pt (p, Res) =
neuper@37906	2088	if get_obj g_res pt p = get_obj g_form pt (lev_on p)(TransitiveB)
neuper@37906	2089	then if existpt' (lev_on p, Res) pt then (lev_on p, Res)
neuper@38031	2090	else error ("lev_on': (p, Res) -> (p, Res) not existent, \
neuper@37906	2091	\p = "^ints2str' (lev_on p))
neuper@37906	2092	else (lev_on p, Frm)
neuper@37906	2093	\| lev_on' pt (p, _) =
neuper@37906	2094	if existpt' (p, Res) pt then (p, Res)
neuper@38031	2095	else error ("lev_on': (p, Frm) -> (p, Res) not existent, \
neuper@37906	2096	\p = "^ints2str' p);
neuper@37906	2097
neuper@37906	2098	fun exist_lev_on' pt p = (lev_on' pt p; true) handle _ => false;
neuper@37906	2099
neuper@37906	2100	(.is the pos' at the last element of a calulation _AND_ can be continued.)
neuper@37906	2101	(* val (pt, pos as (p,p_)) = (pt, ([1],Frm));
neuper@37906	2102	*)
neuper@37906	2103	fun is_curr_endof_calc pt (([],Res) : pos') = false
neuper@37906	2104	\| is_curr_endof_calc pt (pos as (p,_)) =
neuper@37906	2105	not (exist_lev_on' pt pos)
neuper@37906	2106	andalso get_obj g_ostate pt (lev_up p) = Incomplete;
neuper@37906	2107
neuper@37906	2108
neuper@37906	2109	(.insert into ctree and cut branches accordingly.)
neuper@37906	2110
neuper@37906	2111	(.get all positions of certain intervals on the ctree.)
neuper@37906	2112	(*OLD VERSION without move_dn; kept for occasional redesign
wneuper@59279	2113	get all pos's to be cut in a ctree
wneuper@59279	2114	below a pos or from a ctree list after i-th element (NO level_up).*)
neuper@37906	2115	fun get_allpos' (_:pos, _:posel) EmptyPtree = ([]:pos' list)
neuper@37906	2116	\| get_allpos' (p, 1) (Nd (b, bs)) = (p is pos of Nd)
neuper@37906	2117	if g_ostate b = Incomplete
neuper@38015	2118	then ((tracing("get_allpos' (p, 1) Incomplete: p="^ints2str' p);)
neuper@37906	2119	[(p,Frm)] @ (get_allpos's (p, 1) bs)
neuper@37906	2120	)
neuper@38015	2121	else ((tracing("get_allpos' (p, 1) else: p="^ints2str' p);)
neuper@37906	2122	[(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p,Res)]
neuper@37906	2123	)
neuper@37906	2124	(WN041020 here we assume what is presented on the worksheet ?!)
neuper@37906	2125	\| get_allpos' (p, i) (Nd (b, bs)) = (p is pos of Nd)
neuper@37906	2126	if length bs > 0 orelse is_pblobj b
neuper@37906	2127	then if g_ostate b = Incomplete
neuper@37906	2128	then [(p,Frm)] @ (get_allpos's (p, 1) bs)
neuper@37906	2129	else [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p,Res)]
neuper@37906	2130	else
neuper@37906	2131	if g_ostate b = Incomplete
neuper@37906	2132	then []
neuper@37906	2133	else [(p,Res)]
neuper@37906	2134	(WN041020 here we assume what is presented on the worksheet ?!)
neuper@37906	2135	and get_allpos's _ [] = []
neuper@37906	2136	\| get_allpos's (p, i) (pt::pts) = (p is pos of parent-Nd)
neuper@37906	2137	(get_allpos' (p@[i], i) pt) @ (get_allpos's (p, i+1) pts);
neuper@37906	2138
neuper@37906	2139	(.get all positions of certain intervals on the ctree.)
neuper@37906	2140	(NEW version WN050225)
neuper@37906	2141
neuper@37906	2142
neuper@37906	2143	(.cut branches.)
neuper@37906	2144	(*before WN041019......
neuper@37906	2145	val cut_branch = (test_trans, curry take):
wneuper@59279	2146	(ppobj -> bool) * (int -> ctree list -> ctree list);
neuper@37906	2147	.. formlery used for ...
neuper@37906	2148	fun cut_tree''' _ [] = EmptyPtree
neuper@37906	2149	\| cut_tree''' pt pos =
neuper@37906	2150	let val (pt',cut) = appl_branch cut_branch pt pos
neuper@37906	2151	in if cut andalso length pos > 1 then cut_tree''' pt' (lev_up pos)
neuper@37906	2152	else pt' end;
neuper@37906	2153	*)
neuper@37906	2154	(OLD version before WN050225)
neuper@37906	2155	(WN050106 like cut_level, but deletes exactly 1 node --- for tests ONLY)
neuper@37906	2156	fun cut_level_'_ (_:pos' list) (_:pos) EmptyPtree (_:pos') =
neuper@37906	2157	raise PTREE "cut_level_'_ Empty _"
neuper@37906	2158	\| cut_level_'_ _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level_'_ _ []"
neuper@37906	2159	\| cut_level_'_ cuts P (Nd (b, bs)) (p::[],p_) =
neuper@37906	2160	if test_trans b
neuper@37906	2161	then (Nd (b, drop_nth [] (p:posel, bs)),
neuper@37906	2162	(* ~~~~~~~~~~~*)
neuper@37906	2163	cuts @
neuper@37906	2164	(if p_ = Frm then [(P@[p],Res)] else ([]:pos' list)) @
neuper@37906	2165	(WN041020 here we assume what is presented on the worksheet ?!)
neuper@37906	2166	(get_allpos's (P, p+1) (drop_nth [] (p, bs))))
neuper@37906	2167	(* ~~~~~~~~~~~*)
neuper@37906	2168	else (Nd (b, bs), cuts)
neuper@37906	2169	\| cut_level_'_ cuts P (Nd (b, bs)) ((p::ps),p_) =
neuper@37906	2170	let val (bs',cuts') = cut_level_'_ cuts P (nth p bs) (ps, p_)
neuper@37906	2171	in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
neuper@37906	2172
neuper@37906	2173	(before WN050219)
neuper@37906	2174	fun cut_level (_:pos' list) (_:pos) EmptyPtree (_:pos') =
neuper@37906	2175	raise PTREE "cut_level EmptyPtree _"
neuper@37906	2176	\| cut_level _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level _ []"
neuper@37906	2177
neuper@37906	2178	\| cut_level cuts P (Nd (b, bs)) (p::[],p_) =
neuper@37906	2179	if test_trans b
neuper@37906	2180	then (Nd (b, take (p:posel, bs)),
neuper@37906	2181	cuts @
neuper@37906	2182	(if p_ = Frm andalso (#) g_ostate b = Complete
neuper@37906	2183	then [(P@[p],Res)] else ([]:pos' list)) @
neuper@37906	2184	(WN041020 here we assume what is presented on the worksheet ?!)
neuper@37906	2185	(get_allpos's (P, p+1) (takerest (p, bs))))
neuper@37906	2186	else (Nd (b, bs), cuts)
neuper@37906	2187
neuper@37906	2188	\| cut_level cuts P (Nd (b, bs)) ((p::ps),p_) =
neuper@37906	2189	let val (bs',cuts') = cut_level cuts P (nth p bs) (ps, p_)
neuper@37906	2190	in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
neuper@37906	2191
neuper@37906	2192	(OLD version before WN050219, overwritten below)
neuper@37906	2193	fun cut_tree _ (([],_):pos') = raise PTREE "cut_tree _ ([],_)"
neuper@37906	2194	\| cut_tree pt (pos as ([p],_)) =
neuper@37906	2195	let val (pt', cuts) = cut_level ([]:pos' list) [] pt pos
neuper@37906	2196	in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
neuper@37906	2197	then [] else [([],Res)])) end
neuper@37906	2198	\| cut_tree pt (p,p_) =
neuper@37906	2199	let
neuper@37906	2200	fun cutfn pt cuts (p,p_) =
neuper@37906	2201	let val (pt', cuts') = cut_level [] (lev_up p) pt (p,p_)
neuper@37906	2202	val cuts'' = if get_obj g_ostate pt (lev_up p) = Incomplete
neuper@37906	2203	then [] else [(lev_up p, Res)]
neuper@37906	2204	in if length cuts' > 0 andalso length p > 1
neuper@37906	2205	then cutfn pt' (cuts @ cuts') (lev_up p, Frm(-->(p,Res)))
neuper@37906	2206	else (pt',cuts @ cuts') end
neuper@37906	2207	val (pt', cuts) = cutfn pt [] (p,p_)
neuper@37906	2208	in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
neuper@37906	2209	then [] else [([], Res)])) end;
neuper@37906	2210
neuper@37906	2211
neuper@37906	2212	(########/ inserted from ctreeNEW.sml \#################################*)
neuper@37906	2213
wneuper@59279	2214	(*.get all positions in a ctree until ([],Res) or ostate=Incomplete
neuper@37906	2215	val get_allp = fn :
neuper@37906	2216	pos' list -> : accumulated, start with []
neuper@37906	2217	pos -> : the offset for subtrees wrt the root
wneuper@59279	2218	ctree -> : (sub)tree
neuper@37906	2219	pos' : initialization (the last pos' before ...)
neuper@37906	2220	-> pos' list : of positions in this (sub) tree (relative to the root)
neuper@37906	2221	.*)
neuper@37906	2222	(* val (cuts, P, pt, pos) = ([], [3], get_nd pt [3], ([], Frm):pos');
neuper@37906	2223	val (cuts, P, pt, pos) = ([], [2], get_nd pt [2], ([], Frm):pos');
neuper@37906	2224	length (children pt);
neuper@37906	2225	*)
neuper@37906	2226	fun get_allp (cuts:pos' list) (P:pos, pos:pos') pt =
neuper@37906	2227	(let val nxt = move_dn [] pt pos (exn if Incomplete reached)
neuper@37906	2228	in if nxt <> ([],Res)
neuper@37906	2229	then get_allp (cuts @ [nxt]) (P, nxt) pt
neuper@37906	2230	else (map (apfst (curry op@ P)) (cuts @ [nxt])): pos' list
neuper@37906	2231	end) handle PTREE _ => (map (apfst (curry op@ P)) cuts);
neuper@37906	2232
neuper@37906	2233
neuper@37906	2234	(the pts are assumed to be on the same level)
neuper@37906	2235	fun get_allps (cuts: pos' list) (P:pos) [] = cuts
neuper@37906	2236	\| get_allps cuts P (pt::pts) =
neuper@37906	2237	let val below = get_allp [] (P, ([], Frm)) pt
neuper@37906	2238	val levfrm =
neuper@37906	2239	if is_pblnd pt
neuper@37906	2240	then (P, Pbl)::below
neuper@37906	2241	else if last_elem P = 1
neuper@37906	2242	then (P, Frm)::below
neuper@37906	2243	else (Trans) below
neuper@37906	2244	val levres = levfrm @ (if null below then [(P, Res)] else [])
neuper@37906	2245	in get_allps (cuts @ levres) (lev_on P) pts end;
neuper@37906	2246
neuper@37906	2247
neuper@37906	2248	(.these 2 funs decide on how far cut_tree goes.)
neuper@37906	2249	(.shall the nodes _after_ the pos to be inserted at be deleted?.)
neuper@37906	2250	fun test_trans (PrfObj{branch = Transitive,...}) = true
neuper@37906	2251	\| test_trans (PrfObj{branch = NoBranch,...}) = true
neuper@37906	2252	\| test_trans (PblObj{branch = Transitive,...}) = true
neuper@37906	2253	\| test_trans (PblObj{branch = NoBranch,...}) = true
neuper@37906	2254	\| test_trans _ = false;
neuper@37906	2255	(*.shall cutting be continued on the higher level(s)?
neuper@37906	2256	the Nd regarded will NOT be changed.*)
neuper@37906	2257	fun cutlevup (PblObj _) = false (for tests of LK0502)
neuper@37906	2258	\| cutlevup _ = true;
neuper@37906	2259	val cutlevup = test_trans;(WN060727 after summerterm tests.LK0502 withdrawn)
neuper@37906	2260
neuper@37906	2261	(*cut_bottom new sml603..608
neuper@37906	2262	cut the level at the bottom of the pos (used by cappend_...)
neuper@37906	2263	and handle the parent in order to avoid extra case for root
wneuper@59279	2264	fn: ctree -> : the _whole_ ctree for cut_levup
neuper@37906	2265	pos * posel -> : the pos after split_last
wneuper@59279	2266	ctree -> : the parent of the Nd to be cut
neuper@37906	2267	return
wneuper@59279	2268	(ctree * : the updated ctree
neuper@37906	2269	pos' list) * : the pos's cut
neuper@37906	2270	bool : cutting shall be continued on the higher level(s)
neuper@37906	2271	*)
neuper@37906	2272	fun cut_bottom _ (pt' as Nd (b, [])) = ((pt', []), cutlevup b)
neuper@37906	2273	\| cut_bottom (P:pos, p:posel) (Nd (b, bs)) =
neuper@37906	2274	let (divide level into 3 parts...)
neuper@37906	2275	val keep = take (p - 1, bs)
neuper@37906	2276	val pt' as Nd (_,bs') = nth p bs
neuper@52111	2277	(^^^^^_here_ will be 'insert_pt'ed by 'append_..')
neuper@37906	2278	val (tail, tp) = (takerest (p, bs),
neuper@37906	2279	if null (takerest (p, bs)) then 0 else p + 1)
neuper@37906	2280	val (children, cuts) =
neuper@37906	2281	if test_trans b
neuper@37906	2282	then (keep,
neuper@37906	2283	(if is_pblnd pt' then [(P @ [p], Pbl)] else [])
neuper@37906	2284	@ (get_allp [] (P @ [p], (P, Frm)) pt')
neuper@37906	2285	@ (get_allps [] (P @ [p+1]) tail))
neuper@52111	2286	else (keep @ [('insert_pt'ed by 'append_..')] @ tail,
neuper@37906	2287	get_allp [] (P @ [p], (P, Frm)) pt')
neuper@37906	2288	val (pt'', cuts) =
neuper@37906	2289	if cutlevup b
neuper@37906	2290	then (Nd (del_res b, children),
neuper@37906	2291	cuts @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
neuper@37906	2292	else (Nd (b, children), cuts)
neuper@38015	2293	(*val _= tracing("####cut_bottom (P, p)="^pos2str (P @ [p])^
neuper@37906	2294	", Nd=.............................................")
neuper@37906	2295	val _= show_pt pt''
neuper@38015	2296	val _= tracing("####cut_bottom form='"^
neuper@37906	2297	term2str (get_obj g_form pt'' []))
neuper@38015	2298	val _= tracing("####cut_bottom cuts#="^string_of_int (length cuts)^
neuper@37906	2299	", cuts="^pos's2str cuts)*)
neuper@37906	2300	in ((pt'', cuts:pos' list), cutlevup b) end;
neuper@37906	2301
neuper@37906	2302
neuper@37906	2303	(*.go all levels from the bottom of 'pos' up to the root,
neuper@37906	2304	on each level compose the children of a node and accumulate the cut Nds
neuper@37906	2305	args
neuper@37906	2306	pos' list -> : for accumulation
neuper@37906	2307	bool -> : cutting shall be continued on the higher level(s)
wneuper@59279	2308	ctree -> : the whole ctree for 'get_nd pt P' on each level
wneuper@59279	2309	ctree -> : the Nd from the lower level for insertion at path
neuper@37906	2310	pos * posel -> : pos=path split for convenience
wneuper@59279	2311	ctree -> : Nd the children of are under consideration on this call
neuper@37906	2312	returns :
wneuper@59279	2313	ctree * pos' list : the updated parent-Nd and the pos's of the Nds cut
neuper@37906	2314	.*)
neuper@37906	2315	fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:posel) (Nd (b, bs)) =
neuper@37906	2316	let (divide level into 3 parts...)
neuper@37906	2317	val keep = take (p - 1, bs)
neuper@37906	2318	(val pt' comes as argument from below)
neuper@37906	2319	val (tail, tp) = (takerest (p, bs),
neuper@37906	2320	if null (takerest (p, bs)) then 0 else p + 1)
neuper@37906	2321	val (children, cuts') =
neuper@37906	2322	if clevup
neuper@37906	2323	then (keep @ [pt'], get_allps [] (P @ [p+1]) tail)
neuper@37906	2324	else (keep @ [pt'] @ tail, [])
neuper@37906	2325	val clevup' = if clevup then cutlevup b else false
neuper@37906	2326	(the first Nd with false stops cutting on all levels above)
neuper@37906	2327	val (pt'', cuts') =
neuper@37906	2328	if clevup'
neuper@37906	2329	then (Nd (del_res b, children),
neuper@37906	2330	cuts' @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
neuper@37906	2331	else (Nd (b, children), cuts')
neuper@38015	2332	(*val _= tracing("#####cut_levup clevup= "^bool2str clevup)
neuper@38015	2333	val _= tracing("#####cut_levup cutlevup b= "^bool2str (cutlevup b))
neuper@38015	2334	val _= tracing("#####cut_levup (P, p)="^pos2str (P @ [p])^
neuper@37906	2335	", Nd=.............................................")
neuper@37906	2336	val _= show_pt pt''
neuper@38015	2337	val _= tracing("#####cut_levup form='"^
neuper@37906	2338	term2str (get_obj g_form pt'' []))
neuper@38015	2339	val _= tracing("#####cut_levup cuts#="^string_of_int (length cuts)^
neuper@37906	2340	", cuts="^pos's2str cuts)*)
neuper@37906	2341	in if null P then (pt'', (cuts @ cuts'):pos' list)
neuper@37906	2342	else let val (P, p) = split_last P
neuper@37906	2343	in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P)
neuper@37906	2344	end
neuper@37906	2345	end;
neuper@37906	2346
neuper@37906	2347	(*.cut nodes after and below an inserted node in the ctree;
neuper@37906	2348	the cuts range is limited by the predicate 'fun cutlevup'.*)
neuper@37906	2349	fun cut_tree pt (pos,_) =
neuper@37906	2350	if not (existpt pos pt)
neuper@37906	2351	then (pt,[]) (appending a formula never cuts anything)
neuper@37906	2352	else let val (P, p) = split_last pos
neuper@37906	2353	val ((pt', cuts), clevup) = cut_bottom (P, p) (get_nd pt P)
neuper@37906	2354	(* pt' is the updated parent of the Nd to cappend_..*)
neuper@37906	2355	in if null P then (pt', cuts)
neuper@37906	2356	else let val (P, p) = split_last P
neuper@37906	2357	in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P)
neuper@37906	2358	end
neuper@37906	2359	end;
neuper@37906	2360
neuper@37906	2361	fun append_atomic p l f r f' s pt =
neuper@38015	2362	let (val _= tracing("#@append_atomic: pos ="^pos2str p))
wneuper@59253	2363	val (iss, f) = if existpt p pt andalso is_empty_tac (get_obj g_tac pt p)
neuper@37906	2364	then (after Take)
neuper@37925	2365	((fst (get_obj g_loc pt p), SOME l),
neuper@37906	2366	get_obj g_form pt p)
neuper@37925	2367	else ((NONE, SOME l), f)
neuper@52111	2368	in insert_pt (PrfObj {cell = NONE,
neuper@37906	2369	form = f,
neuper@37906	2370	tac = r,
neuper@37906	2371	loc = iss,
neuper@37906	2372	branch= NoBranch,
neuper@37906	2373	result= f',
neuper@37906	2374	ostate= s}) pt p end;
neuper@37906	2375
neuper@37906	2376
neuper@37906	2377	(20.8.02: cappend_ FIXXXXME cut branches below cannot be decided here:
neuper@37906	2378	detail - generate - cappend: inserted, not appended !!!
neuper@37906	2379
neuper@37906	2380	cut decided in applicable_in !?!
neuper@37906	2381	*)
neuper@37906	2382	fun cappend_atomic pt p loc f r f' s =
neuper@37906	2383	(* val (pt, p, loc, f, r, f', s) =
neuper@37906	2384	(pt,p,l,f,Rewrite_Set_Inst (subst2subs subs',id_rls rls'),
neuper@37906	2385	(f',asm),Complete);
neuper@37906	2386	*)
neuper@38015	2387	((tracing("##@cappend_atomic: pos ="^pos2str p);)
neuper@37906	2388	apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm))
neuper@37906	2389	);
neuper@37906	2390	(TODO.WN050305 redesign the handling of istates)
neuper@37906	2391	fun cappend_atomic pt p ist_res f r f' s =
wneuper@59253	2392	if existpt p pt andalso is_empty_tac (get_obj g_tac pt p)
neuper@41994	2393	then (after Take: transfer Frm and respective istate)
neuper@41994	2394	let
neuper@41994	2395	val (ist_form, f) =
neuper@41994	2396	(get_loc pt (p,Frm), get_obj g_form pt p)
neuper@41994	2397	val (pt, cs) = cut_tree pt (p,Frm)
neuper@41994	2398	val pt = append_atomic p (e_istate, e_ctxt) f r f' s pt
neuper@41994	2399	val pt = update_loc' pt p (SOME ist_form, SOME ist_res)
neuper@41994	2400	in (pt, cs) end
neuper@41994	2401	else apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
neuper@37906	2402
neuper@37906	2403	(* called by Take *)
neuper@37906	2404	fun append_form p l f pt =
neuper@38015	2405	((tracing("##@append_form: pos ="^pos2str p);)
neuper@52111	2406	insert_pt (PrfObj {cell = NONE,
neuper@37906	2407	form = (*if existpt p pt
neuper@37906	2408	andalso get_obj g_tac pt p = Empty_Tac
neuper@37906	2409	(distinction from 'old' (+complete!) pobjs)
neuper@37906	2410	then get_obj g_form pt p else*) f,
neuper@37906	2411	tac = Empty_Tac,
neuper@37925	2412	loc = (SOME l, NONE),
neuper@37906	2413	branch= NoBranch,
neuper@37906	2414	result= (e_term,[]),
neuper@37906	2415	ostate= Incomplete}) pt p
neuper@37906	2416	);
neuper@37906	2417	(* val (p,loc,f) = ([1], e_istate, str2term "x + 1 = 2");
neuper@37906	2418	val (p,loc,f) = (fst p, e_istate, str2term "-1 + x = 0");
neuper@37906	2419	*)
neuper@37906	2420	fun cappend_form pt p loc f =
neuper@38015	2421	((tracing("##@cappend_form: pos ="^pos2str p);)
neuper@37906	2422	apfst (append_form p loc f) (cut_tree pt (p,Frm))
neuper@37906	2423	);
neuper@37906	2424	fun cappend_form pt p loc f =
neuper@38015	2425	let (*val _= tracing("##@cappend_form: pos ="^pos2str p)
neuper@38015	2426	val _= tracing("##@cappend_form before cut_tree: loc ="^istate2str loc)*)
neuper@37906	2427	val (pt', cs) = cut_tree pt (p,Frm)
neuper@37906	2428	val pt'' = append_form p loc f pt'
neuper@38015	2429	(*val _= tracing("##@cappend_form after append: loc ="^
neuper@37906	2430	istates2str (get_obj g_loc pt'' p))*)
neuper@37906	2431	in (pt'', cs) end;
neuper@37906	2432
neuper@37906	2433
neuper@37906	2434
neuper@37906	2435	fun append_result pt p l f s =
wneuper@59274	2436	(appl_obj (repl_result (fst (get_obj g_loc pt p), SOME l) f s) pt p, []);
neuper@37906	2437
neuper@37906	2438
neuper@37906	2439	(WN041022 deprecated, still for kbtest/diffapp.sml, /systest/root-equ.sml)
neuper@37906	2440	fun append_parent p l f r b pt =
neuper@38015	2441	let (val _= tracing("###append_parent: pos ="^pos2str p);)
wneuper@59253	2442	val (ll,f) = if existpt p pt andalso is_empty_tac (get_obj g_tac pt p)
neuper@37925	2443	then ((fst (get_obj g_loc pt p), SOME l),
neuper@37906	2444	get_obj g_form pt p)
neuper@37925	2445	else ((SOME l, NONE), f)
neuper@52111	2446	in insert_pt (PrfObj
neuper@37925	2447	{cell = NONE,
neuper@37906	2448	form = f,
neuper@37906	2449	tac = r,
neuper@37906	2450	loc = ll,
neuper@37906	2451	branch= b,
neuper@37906	2452	result= (e_term,[]),
neuper@37906	2453	ostate= Incomplete}) pt p end;
neuper@37906	2454	fun cappend_parent pt p loc f r b =
neuper@38015	2455	((tracing("###cappend_parent: pos ="^pos2str p);)
neuper@37906	2456	apfst (append_parent p loc f r b) (cut_tree pt (p,Und))
neuper@37906	2457	);
neuper@37906	2458
neuper@37906	2459
neuper@37906	2460	fun append_problem [] l fmz (strs,spec,hdf) _ =
neuper@38015	2461	((tracing("###append_problem: pos = []");)
neuper@37906	2462	(Nd (PblObj
neuper@37925	2463	{cell = NONE,
neuper@37906	2464	origin= (strs,spec,hdf),
neuper@37906	2465	fmz = fmz,
neuper@37906	2466	spec = empty_spec,
neuper@37906	2467	probl = []:itm list,
neuper@37906	2468	meth = []:itm list,
neuper@41988	2469	ctxt = e_ctxt,
neuper@37925	2470	env = NONE,
neuper@37925	2471	loc = (SOME l, NONE),
neuper@37906	2472	branch= TransitiveB,(FIXXXXXME.27.8.03: for equations only)
neuper@37906	2473	result= (e_term,[]),
neuper@37906	2474	ostate= Incomplete},[]))
neuper@37906	2475	)
neuper@37906	2476	\| append_problem p l fmz (strs,spec,hdf) pt =
neuper@38015	2477	((tracing("###append_problem: pos ="^pos2str p);)
neuper@52111	2478	insert_pt (PblObj
neuper@37925	2479	{cell = NONE,
neuper@37906	2480	origin= (strs,spec,hdf),
neuper@37906	2481	fmz = fmz,
neuper@37906	2482	spec = empty_spec,
neuper@37906	2483	probl = []:itm list,
neuper@37906	2484	meth = []:itm list,
neuper@41988	2485	ctxt = e_ctxt,
neuper@37925	2486	env = NONE,
neuper@37925	2487	loc = (SOME l, NONE),
neuper@37906	2488	branch= TransitiveB,
neuper@37906	2489	result= (e_term,[]),
neuper@37906	2490	ostate= Incomplete}) pt p
neuper@37906	2491	);
neuper@37906	2492	fun cappend_problem _ [] loc fmz ori =
neuper@38015	2493	((tracing("###cappend_problem: pos = []");)
neuper@37906	2494	(append_problem [] loc fmz ori EmptyPtree,[])
neuper@37906	2495	)
neuper@37906	2496	\| cappend_problem pt p loc fmz ori =
neuper@38015	2497	((tracing("###cappend_problem: pos ="^pos2str p);)
bonzai@41948	2498	apfst (append_problem p (loc:(istate * Proof.context)) fmz ori) (cut_tree pt (p,Frm))
neuper@37906	2499	);
neuper@37906	2500
neuper@37906	2501	(*.get the theory explicitly specified for the rootpbl;
neuper@37906	2502	thus use this function _after_ finishing specification.*)
neuper@41988	2503	fun rootthy (Nd (PblObj {spec=(thyID, _, _), ...}, _)) = assoc_thy thyID
neuper@38031	2504	\| rootthy _ = error "rootthy";
neuper@37906	2505
wneuper@59275	2506	(**)
wneuper@59275	2507	end
wneuper@59275	2508	(**)
wneuper@59277	2509	(/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\ )
wneuper@59275	2510	open Ctree
wneuper@59277	2511	( \--- ! aktivate for Test_Isac END ----------------------------------------------------------/)
wneuper@59278	2512
wneuper@59278	2513	(* policy for "open" structures:
wneuper@59278	2514	--------------------------------
wneuper@59278	2515	The above "open Ctree" creates an unclear situation with structures, in particular in test/.
wneuper@59278	2516	This is work in progress, but urges to make policy explicit:
wneuper@59278	2517
wneuper@59278	2518	(1) All structures are closed with a signature; this for prepares re-arrangement of structures.
wneuper@59278	2519	(2) Some structures are pervasive (e.g. Ctree) such, that an "open" ensures readability locally.
wneuper@59278	2520	(3) test/ is preceeded by "open" for all structures, in order to ease copy&paste from scr/ to test/
wneuper@59278	2521
wneuper@59278	2522	ad (1) Presently this point is under construction.
wneuper@59278	2523	ad (2) Such local "open" are kept to a minimum (with the goal to reach Isabelle's state).
wneuper@59278	2524	ad (3) See https://intra.ist.tugraz.at/hg/isa/file/2ba35efb07b7/test/Tools/isac/Test_Isac.thy#l70
wneuper@59278	2525	*)

author	Walther Neuper <wneuper@ist.tugraz.at>
	Thu, 22 Dec 2016 11:36:20 +0100
changeset 59279	255c853ea2f0
parent 59278	a474900d5bd2
child 59280	ee5efb0697f6
permissions	-rw-r--r--