wneuper@59274: (* Title: the calctree, which holds a calculation wneuper@59274: Author: Walther Neuper 1999 wneuper@59274: (c) due to copyright terms neuper@37906: *) neuper@37906: wneuper@59275: signature CALC_TREEE = wneuper@59275: sig (* vvv--- *.sml require these typs incrementally, with these exception -----------------vvv *) wneuper@59275: (* for ptyps.sml *) wneuper@59275: type fmz_ = cterm' list wneuper@59275: type fmz = fmz_ * spec; wneuper@59275: val e_fmz : fmz_ * spec (* for datatypes.sml *) wneuper@59275: type con wneuper@59275: type scrstate wneuper@59275: datatype istate = RrlsState of rrlsstate | ScrState of scrstate | Uistate wneuper@59275: val istate2str : istate -> string wneuper@59275: val e_istate : istate wneuper@59275: type subs wneuper@59275: type sube wneuper@59275: val sube2str : cterm' list -> string wneuper@59275: type subte wneuper@59275: val sube2subst : theory -> cterm' list -> (term * term) list wneuper@59275: val sube2subte : cterm' list -> term list wneuper@59275: val subs2subst : theory -> cterm' list -> (term * term) list wneuper@59275: val subst2sube : (term * term) list -> cterm' list (* for datatypes.sml *) wneuper@59275: val subst2subs : (term * term) list -> cterm' list wneuper@59275: val subst2subs' : (term * term) list -> (string * string) list wneuper@59275: val subte2sube : term list -> cterm' list wneuper@59275: wneuper@59275: type result wneuper@59275: datatype tac_ = (* TODO.WN161219: replace *every* cterm' by term *) wneuper@59275: Add_Find' of cterm' * itm list | Add_Given' of cterm' * itm list | Add_Relation' of cterm' * itm list wneuper@59275: | Apply_Assumption' of term list * term wneuper@59275: | Apply_Method' of metID * term option * istate * Proof.context wneuper@59275: (*/--- TODO: re-design ? -----------------------------------------------------------------\*) wneuper@59275: | Begin_Sequ' | Begin_Trans' of term wneuper@59275: | Split_And' of term | Split_Or' of term | Split_Intersect' of term wneuper@59275: | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term wneuper@59275: | End_Sequ' | End_Trans' of result wneuper@59275: | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof'' wneuper@59275: (*\--- TODO: re-design ? -----------------------------------------------------------------/*) wneuper@59275: | CAScmd' of term wneuper@59275: | Calculate' of theory' * string * term * (term * thm') wneuper@59275: | Check_Postcond' of pblID * result wneuper@59275: | Check_elementwise' of term * cterm' * result wneuper@59275: | Del_Find' of cterm' | Del_Given' of cterm' | Del_Relation' of cterm' wneuper@59275: wneuper@59275: | Derive' of rls wneuper@59275: | Detail_Set' of theory' * bool * rls * term * result wneuper@59275: | Detail_Set_Inst' of theory' * bool * subst * rls * term * result wneuper@59275: | End_Detail' of result wneuper@59275: wneuper@59275: | Empty_Tac_ wneuper@59275: | Free_Solve' wneuper@59275: wneuper@59275: | Init_Proof' of cterm' list * spec wneuper@59275: | Model_Problem' of pblID * itm list * itm list wneuper@59275: | Or_to_List' of term * term wneuper@59275: | Refine_Problem' of pblID * (itm list * (bool * term) list) wneuper@59275: | Refine_Tacitly' of pblID * pblID * domID * metID * itm list wneuper@59275: wneuper@59275: | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * result wneuper@59275: | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * result wneuper@59275: | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * result wneuper@59275: | Rewrite_Set' of theory' * bool * rls * term * result wneuper@59275: | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * result wneuper@59275: wneuper@59275: | Specify_Method' of metID * ori list * itm list wneuper@59275: | Specify_Problem' of pblID * (bool * (itm list * (bool * term) list)) wneuper@59275: | Specify_Theory' of domID wneuper@59275: | Subproblem' of spec * ori list * term * fmz_ * Proof.context * term wneuper@59275: | Substitute' of rew_ord_ * rls * subte * term * term wneuper@59275: | Tac_ of theory * string * string * string wneuper@59275: | Take' of term | Take_Inst' of term wneuper@59275: datatype tac = wneuper@59275: Add_Find of cterm' | Add_Given of cterm' | Add_Relation of cterm' wneuper@59275: | Apply_Assumption of cterm' list wneuper@59275: | Apply_Method of metID wneuper@59275: wneuper@59275: | Begin_Sequ | Begin_Trans wneuper@59275: | Split_And | Split_Or | Split_Intersect wneuper@59275: | Conclude_And | Conclude_Or | Collect_Trues wneuper@59275: | End_Sequ | End_Trans wneuper@59275: | End_Ruleset | End_Subproblem | End_Intersect | End_Proof' wneuper@59275: wneuper@59275: | CAScmd of cterm' wneuper@59275: | Calculate of string wneuper@59275: | Check_Postcond of pblID wneuper@59275: | Check_elementwise of cterm' wneuper@59275: | Del_Find of cterm' | Del_Given of cterm' | Del_Relation of cterm' wneuper@59275: wneuper@59275: | Derive of rls' wneuper@59275: | Detail_Set of rls' wneuper@59275: | Detail_Set_Inst of subs * rls' wneuper@59275: | End_Detail wneuper@59275: wneuper@59275: | Empty_Tac wneuper@59275: | Free_Solve wneuper@59275: | Group of con * int list wneuper@59275: wneuper@59275: | Init_Proof of cterm' list * spec wneuper@59275: | Model_Problem wneuper@59275: | Or_to_List wneuper@59275: | Refine_Problem of pblID wneuper@59275: | Refine_Tacitly of pblID wneuper@59275: wneuper@59275: | Rewrite of thm'' wneuper@59275: | Rewrite_Asm of thm'' wneuper@59275: | Rewrite_Inst of subs * thm'' wneuper@59275: | Rewrite_Set of rls' wneuper@59275: | Rewrite_Set_Inst of subs * rls' wneuper@59275: wneuper@59275: | Specify_Method of metID wneuper@59275: | Specify_Problem of pblID wneuper@59275: | Specify_Theory of domID wneuper@59275: | Subproblem of domID * pblID wneuper@59275: wneuper@59275: | Substitute of sube wneuper@59275: | Tac of string wneuper@59275: | Take of cterm' | Take_Inst of cterm' wneuper@59275: val tac2str : tac -> string wneuper@59275: val rls_of : tac -> rls' (* for solve.sml *) wneuper@59275: val tac2IDstr : tac -> string wneuper@59275: val is_rewset : tac -> bool (* for mathengine.sml *) wneuper@59275: val is_rewtac : tac -> bool (* for interface.sml *) wneuper@59275: wneuper@59275: eqtype posel wneuper@59275: type pos = posel list wneuper@59275: val pos2str : int list -> string (* for datatypes.sml *) wneuper@59275: datatype pos_ = Frm | Met | Pbl | Res | Und wneuper@59275: val pos_2str : pos_ -> string wneuper@59275: type pos' wneuper@59275: val pos'2str : pos' -> string wneuper@59275: val str2pos_ : string -> pos_ (* for datatypes.sml *) wneuper@59275: val e_pos' : pos' wneuper@59275: type state wneuper@59275: (* for generate.sml ?!? ca.*) wneuper@59275: datatype safe = Helpless | Safe | Sundef | Unsafe wneuper@59275: val tac_2str : tac_ -> string wneuper@59275: eqtype cellID wneuper@59275: wneuper@59275: datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB wneuper@59275: datatype ostate = Complete | Incomplete | Inconsistent wneuper@59275: datatype ppobj = wneuper@59275: PblObj of wneuper@59275: {branch: branch, wneuper@59275: cell: lrd option, wneuper@59275: loc: (istate * Proof.context) option * (istate * Proof.context) option, wneuper@59275: ostate: ostate, wneuper@59275: result: result, wneuper@59275: wneuper@59275: fmz: fmz, wneuper@59275: origin: ori list * spec * term, wneuper@59275: probl: itm list, wneuper@59275: meth: itm list, wneuper@59275: spec: spec, wneuper@59275: ctxt: Proof.context, wneuper@59275: env: (istate * Proof.context) option} wneuper@59275: | PrfObj of wneuper@59275: {branch: branch, wneuper@59275: cell: lrd option, wneuper@59275: loc: (istate * Proof.context) option * (istate * Proof.context) option, wneuper@59275: ostate: ostate, wneuper@59275: result: result, wneuper@59275: wneuper@59275: form: term, wneuper@59275: tac: tac} wneuper@59275: val lev_on : pos -> pos wneuper@59275: val lev_dn : pos -> pos wneuper@59275: val lev_dn_ : pos' -> pos' wneuper@59275: val lev_up : pos -> pos wneuper@59275: val lev_of : pos' -> int wneuper@59275: val pos_plus : int -> pos' -> pos' wneuper@59275: val lev_back' : pos' -> pos' (* for inform.sml *) wneuper@59275: wneuper@59279: datatype ctree = EmptyPtree | Nd of ppobj * ctree list wneuper@59279: val e_ctree : ctree (* TODO: replace by EmptyPtree*) wneuper@59279: val existpt' : pos' -> ctree -> bool (* for interface.sml *) wneuper@59279: val exist_lev_on' : ctree -> pos' -> bool (* for interface.sml *) wneuper@59275: val is_interpos : pos' -> bool (* for interface.sml *) wneuper@59279: val lev_on' : ctree -> pos' -> pos' (* for interface.sml *) wneuper@59279: val lev_pred' : ctree -> pos' -> pos' (* for interface.sml *) wneuper@59279: val move_up : pos -> ctree -> pos' -> pos' (* for interface.sml *) wneuper@59279: val movelevel_dn : pos -> ctree -> pos' -> pos' (* for interface.sml *) wneuper@59279: val movelevel_up : pos -> ctree -> pos' -> pos' (* for interface.sml *) wneuper@59279: val movecalchd_up : ctree -> pos' -> pos' (* for interface.sml *) wneuper@59279: val par_pblobj : ctree -> pos -> pos wneuper@59279: val ins_chn : ctree list -> ctree -> pos -> ctree (* for solve.sml *) wneuper@59279: val children : ctree -> ctree list (* for solve.sml *) wneuper@59279: val get_nd : ctree -> pos -> ctree (* for solve.sml *) wneuper@59275: val just_created_ : ppobj -> bool (* for mathengine.sml *) wneuper@59279: val just_created : ctree * pos' -> bool (* for mathengine.sml *) wneuper@59279: val is_curr_endof_calc : ctree -> pos' -> bool (* for interface.sml *) wneuper@59275: val e_origin : ori list * spec * term (* for mathengine.sml *) wneuper@59275: wneuper@59279: val move_dn : pos -> ctree -> pos' -> pos' wneuper@59275: val is_pblobj : ppobj -> bool wneuper@59279: val is_pblobj' : ctree -> pos -> bool wneuper@59279: val is_pblnd : ctree -> bool wneuper@59279: val last_onlev : ctree -> pos -> bool wneuper@59275: wneuper@59275: val g_spec : ppobj -> spec wneuper@59275: val g_loc : ppobj -> (istate * Proof.context) option * (istate * Proof.context) option wneuper@59275: val g_form : ppobj -> term wneuper@59275: val g_pbl : ppobj -> itm list wneuper@59275: val g_met : ppobj -> itm list wneuper@59275: val g_metID : ppobj -> metID wneuper@59275: val g_result : ppobj -> result wneuper@59275: val g_tac : ppobj -> tac wneuper@59275: val g_domID : ppobj -> domID (* for appl.sml TODO: replace by thyID *) wneuper@59275: val g_env : ppobj -> (istate * Proof.context) option (* for appl.sml *) wneuper@59275: wneuper@59275: val g_origin : ppobj -> ori list * spec * term (* for script.sml *) wneuper@59279: val get_loc : ctree -> pos' -> istate * Proof.context (* for script.sml *) wneuper@59279: val get_istate : ctree -> pos' -> istate (* for script.sml *) wneuper@59279: val get_ctxt : ctree -> pos' -> Proof.context wneuper@59279: val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a wneuper@59279: val get_curr_formula : ctree * pos' -> term wneuper@59279: val get_assumptions_ : ctree -> pos' -> term list (* for appl.sml *) wneuper@59275: wneuper@59279: val append_result : ctree -> pos -> istate * Proof.context -> result -> wneuper@59279: ostate -> ctree * 'a list wneuper@59275: val append_atomic : (* for solve.sml *) wneuper@59279: pos -> istate * Proof.context -> term -> tac -> result -> ostate -> ctree -> ctree wneuper@59279: val cappend_atomic : ctree -> pos -> istate * Proof.context -> term -> tac -> result -> wneuper@59279: ostate -> ctree * pos' list wneuper@59279: val cappend_form : ctree -> pos -> istate * Proof.context -> term -> ctree * pos' list wneuper@59279: val cappend_problem : ctree -> pos -> istate * Proof.context -> fmz -> wneuper@59279: ori list * spec * term -> ctree * pos' list wneuper@59275: wneuper@59279: val update_branch : ctree -> pos -> branch -> ctree wneuper@59279: val update_ctxt : ctree -> pos -> Proof.context -> ctree wneuper@59279: val update_env : ctree -> pos -> (istate * Proof.context) option -> ctree wneuper@59279: val update_oris : ctree -> pos -> ori list -> ctree wneuper@59279: val update_orispec : ctree -> pos -> spec -> ctree wneuper@59279: val update_pbl : ctree -> pos -> itm list -> ctree wneuper@59279: val update_pblppc : ctree -> pos -> itm list -> ctree (* =vvv= ? *) wneuper@59279: val update_pblID : ctree -> pos -> pblID -> ctree (* =^^^= ? *) wneuper@59279: val update_met : ctree -> pos -> itm list -> ctree (* =vvv= ? *) wneuper@59279: val update_metppc : ctree -> pos -> itm list -> ctree (* =^^^= ? *) wneuper@59279: val update_metID : ctree -> pos -> metID -> ctree wneuper@59279: val update_domID : ctree -> pos -> domID -> ctree wneuper@59279: val update_spec : ctree -> pos -> spec -> ctree wneuper@59279: val update_tac : ctree -> pos -> tac -> ctree wneuper@59275: wneuper@59275: val e_ctxt : Proof.context wneuper@59275: val is_e_ctxt : Proof.context -> bool (* for appl.sml *) wneuper@59275: val new_val : term -> istate -> istate wneuper@59275: (* for calchead.sml *) wneuper@59275: type cid = cellID list wneuper@59275: type ocalhd = bool * pos_ * term * itm list * (bool * term) list * spec wneuper@59275: datatype ptform = Form of term | ModSpec of ocalhd wneuper@59275: val get_somespec' : spec -> spec -> spec wneuper@59275: exception PTREE of string; wneuper@59275: (* for appl.sml *) wneuper@59279: val par_pbl_det : ctree -> pos -> bool * pos * rls wneuper@59275: (* for rewtools.sml *) wneuper@59275: val rule2tac : theory -> (term * term) list -> rule -> tac wneuper@59275: val eq_tac : tac * tac -> bool wneuper@59275: (* for script.sml *) wneuper@59279: val rootthy : ctree -> theory wneuper@59275: (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) wneuper@59279: val update_loc' : ctree -> pos -> (istate * Proof.context) option * (istate * Proof.context) option -> ctree wneuper@59279: val append_problem : int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree -> ctree wneuper@59275: val g_res : ppobj -> term wneuper@59279: val pr_ctree : (pos -> ppobj -> string) -> ctree -> string wneuper@59275: val pr_short : pos -> ppobj -> string wneuper@59279: val existpt : pos -> ctree -> bool wneuper@59275: val is_empty_tac : tac -> bool wneuper@59275: val e_subs : string list wneuper@59275: val e_sube : cterm' list wneuper@59275: val g_branch : ppobj -> branch wneuper@59275: val g_ctxt : ppobj -> Proof.context wneuper@59275: val g_fmz : ppobj -> fmz wneuper@59279: val get_allp : pos' list -> pos * (int list * pos_) -> ctree -> pos' list wneuper@59279: val get_allps : (pos * pos_) list -> posel list -> ctree list -> pos' list wneuper@59279: val get_allpos' : pos * posel -> ctree -> pos' list wneuper@59279: val get_allpos's : pos * posel -> ctree list -> (pos * pos_) list wneuper@59279: val cut_bottom : pos * posel -> ctree -> (ctree * pos' list) * bool wneuper@59279: val cut_tree : ctree -> pos * 'a -> ctree * pos' list wneuper@59279: val cut_level : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list wneuper@59279: val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list wneuper@59279: val get_trace : ctree -> int list -> int list -> int list list wneuper@59275: val subte2subst : term list -> (term * term) list wneuper@59275: val branch2str : branch -> string wneuper@59275: ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) wneuper@59275: end wneuper@59275: (* wneuper@59275: structure Ctree : wneuper@59275: sig wneuper@59275: val Ets : ets exception PTREE of string wneuper@59275: val append_atomic : wneuper@59279: pos -> istate * Proof.context -> term -> tac -> term * term list -> ostate -> ctree -> ctree wneuper@59279: val append_form : int list -> istate * Proof.context -> term -> ctree -> ctree wneuper@59279: val append_parent : pos -> istate * Proof.context -> term -> tac -> branch -> ctree -> ctree wneuper@59279: val append_problem : int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree -> ctree wneuper@59279: val append_result : ctree -> pos -> istate * Proof.context -> term * term list -> ostate -> ctree * 'a list wneuper@59279: val appl_branch : (ppobj -> bool) * (posel -> ctree list -> ctree list) -> ctree -> int list -> ctree * bool wneuper@59279: val appl_obj : (ppobj -> ppobj) -> ctree -> pos -> ctree wneuper@59279: val appl_to_node : (ppobj -> ppobj) -> ctree -> ctree wneuper@59275: datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB wneuper@59275: val branch2str : branch -> string wneuper@59275: val cappend_atomic : wneuper@59279: ctree -> pos -> istate * Proof.context -> term -> tac -> term * term list -> ostate -> ctree * pos' list wneuper@59279: val cappend_form : ctree -> pos -> istate * Proof.context -> term -> ctree * pos' list wneuper@59279: val cappend_parent : ctree -> pos -> istate * Proof.context -> term -> tac -> branch -> ctree * pos' list wneuper@59275: val cappend_problem : wneuper@59279: ctree -> int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree * pos' list wneuper@59275: eqtype cellID wneuper@59279: val children : ctree -> ctree list wneuper@59275: type cid = cellID list wneuper@59275: datatype con = land | lor wneuper@59279: val cut_bottom : pos * posel -> ctree -> (ctree * pos' list) * bool wneuper@59279: val cut_level : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list wneuper@59279: val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list wneuper@59279: val cut_levup : pos' list -> bool -> ctree -> ctree -> posel list * posel -> ctree -> ctree * pos' list wneuper@59279: val cut_tree : ctree -> pos * 'a -> ctree * pos' list wneuper@59275: val cutlevup : ppobj -> bool wneuper@59275: val del_res : ppobj -> ppobj wneuper@59279: val delete_result : ctree -> pos -> ctree wneuper@59275: val e_ctxt : Proof.context wneuper@59275: val e_fmz : 'a list * spec wneuper@59275: val e_ocalhd : bool * pos_ * term * itm list * (bool * term) list * spec wneuper@59275: val e_origin : ori list * spec * term wneuper@59275: val e_ptform : ptform wneuper@59275: val e_ptform' : ptform wneuper@59279: val e_ctree : ctree wneuper@59275: val e_scrstate : scrstate wneuper@59275: val e_sube : cterm' list wneuper@59275: val e_subs : string list wneuper@59275: val e_subte : term list wneuper@59275: val empty_envp : envp type env = (term * term) list wneuper@59275: type envp = (int * term list) list * (int * rls) list * (int * ets) list * (string * pos) list wneuper@59275: val eq_tac : tac * tac -> bool type ets = (loc_ * (tac_ * env * env * term * term * safe)) list wneuper@59275: val ets2s : loc_ * (tac_ * subst * subst * term * term * safe) -> string wneuper@59275: val ets2str : ets -> string wneuper@59279: val exist_lev_on' : ctree -> pos' -> bool wneuper@59279: val existpt : pos -> ctree -> bool wneuper@59279: val existpt' : pos' -> ctree -> bool wneuper@59275: type fmz = fmz_ * spec wneuper@59275: type fmz_ = cterm' list wneuper@59275: val g_branch : ppobj -> branch wneuper@59275: val g_cell : ppobj -> lrd option wneuper@59275: val g_ctxt : ppobj -> Proof.context wneuper@59275: val g_domID : ppobj -> domID wneuper@59275: val g_env : ppobj -> (istate * Proof.context) option wneuper@59275: val g_fmz : ppobj -> fmz wneuper@59275: val g_form : ppobj -> term wneuper@59279: val g_form' : ctree -> term wneuper@59275: val g_loc : ppobj -> (istate * Proof.context) option * (istate * Proof.context) option wneuper@59275: val g_met : ppobj -> itm list wneuper@59275: val g_metID : ppobj -> metID wneuper@59275: val g_origin : ppobj -> ori list * spec * term wneuper@59275: val g_ostate : ppobj -> ostate wneuper@59279: val g_ostate' : ctree -> ostate wneuper@59275: val g_pbl : ppobj -> itm list wneuper@59275: val g_res : ppobj -> term wneuper@59279: val g_res' : ctree -> term wneuper@59275: val g_result : ppobj -> term * term list wneuper@59275: val g_spec : ppobj -> spec wneuper@59275: val g_tac : ppobj -> tac wneuper@59279: val get_all : (ppobj -> 'a) -> ctree -> 'a list wneuper@59279: val get_allp : pos' list -> pos * (int list * pos_) -> ctree -> pos' list wneuper@59279: val get_allpos' : pos * posel -> ctree -> pos' list wneuper@59279: val get_allpos's : pos * posel -> ctree list -> (pos * pos_) list wneuper@59279: val get_allps : (pos * pos_) list -> posel list -> ctree list -> pos' list wneuper@59279: val get_alls : (ppobj -> 'a) -> ctree list -> 'a list wneuper@59279: val get_assumptions_ : ctree -> pos * pos_ -> term list wneuper@59279: val get_ctxt : ctree -> pos * pos_ -> Proof.context wneuper@59279: val get_curr_formula : ctree * (pos * pos_) -> term wneuper@59279: val get_istate : ctree -> pos * pos_ -> istate wneuper@59279: val get_loc : ctree -> pos * pos_ -> istate * Proof.context wneuper@59279: val get_nd : ctree -> pos -> ctree wneuper@59279: val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a wneuper@59275: val get_somespec : spec -> spec -> spec wneuper@59275: val get_somespec' : spec -> spec -> spec wneuper@59279: val get_trace : ctree -> int list -> int list -> int list list wneuper@59279: val gpt_cell : ctree -> lrd option wneuper@59275: type iist = istate option * istate option wneuper@59275: val ind : pos' -> int wneuper@59279: val ins_chn : ctree list -> ctree -> int list -> ctree wneuper@59275: val ins_nth : int -> 'a -> 'a list -> 'a list wneuper@59279: val insert_pt : ppobj -> ctree -> int list -> ctree wneuper@59279: val is_curr_endof_calc : ctree -> pos' -> bool wneuper@59275: val is_e_ctxt : Proof.context -> bool wneuper@59275: val is_empty_tac : tac -> bool wneuper@59275: val is_interpos : pos' -> bool wneuper@59279: val is_pblnd : ctree -> bool wneuper@59275: val is_pblobj : ppobj -> bool wneuper@59279: val is_pblobj' : ctree -> pos -> bool wneuper@59275: val is_prfobj : ppobj -> bool wneuper@59275: val is_rewset : tac -> bool wneuper@59275: val is_rewtac : tac -> bool wneuper@59275: val isasub2subst : term -> (term * term) list wneuper@59275: datatype istate = RrlsState of rrlsstate | ScrState of scrstate | Uistate wneuper@59275: val istate2str : istate -> string wneuper@59275: val istates2str : istate option * istate option -> string wneuper@59279: val just_created : ctree * pos' -> bool wneuper@59275: val just_created_ : ppobj -> bool wneuper@59279: val last_onlev : ctree -> pos -> bool wneuper@59275: val lev_back' : pos' -> pos' wneuper@59275: val lev_dn : posel list -> posel list wneuper@59275: val lev_dnRes : pos' -> pos' wneuper@59275: val lev_dn_ : pos' -> pos' wneuper@59275: val lev_of : pos' -> int wneuper@59275: val lev_on : pos -> posel list wneuper@59279: val lev_on' : ctree -> pos' -> pos' wneuper@59275: val lev_onFrm : pos' -> pos' wneuper@59275: val lev_pred : pos -> pos wneuper@59279: val lev_pred' : ctree -> pos' -> pos' wneuper@59275: val lev_up : pos -> pos wneuper@59275: val lev_up_ : pos' -> pos' wneuper@59279: val move_dn : pos -> ctree -> int list * pos_ -> int list * pos_ wneuper@59279: val move_up : int list -> ctree -> int list * pos_ -> int list * pos_ wneuper@59279: val movecalchd_up : ctree -> pos' -> pos' wneuper@59279: val movelevel_dn : int list -> ctree -> int list * pos_ -> int list * pos_ wneuper@59279: val movelevel_up : int list -> ctree -> int list * pos_ -> int list * pos_ wneuper@59275: val new_val : term -> istate -> istate wneuper@59275: val nth : int -> 'a list -> 'a wneuper@59275: type ocalhd = bool * pos_ * term * itm list * (bool * term) list * spec wneuper@59275: val ocalhd2str : ocalhd -> string wneuper@59275: datatype ostate = Complete | Incomplete | Inconsistent wneuper@59275: val ostate2str : ostate -> string wneuper@59279: val par_children : ctree -> pos -> ctree list * pos wneuper@59279: val par_pbl_det : ctree -> pos -> bool * pos * rls wneuper@59279: val par_pblobj : ctree -> pos -> pos wneuper@59275: type pos = posel list wneuper@59275: type pos' = pos * pos_ wneuper@59275: val pos's2str : (int list * pos_) list -> string wneuper@59275: val pos2str : int list -> string wneuper@59275: datatype pos_ = Frm | Met | Pbl | Res | Und wneuper@59275: val pos_2str : pos_ -> string wneuper@59275: val pos_plus : int -> pos * pos_ -> pos' wneuper@59275: eqtype posel wneuper@59275: val posless : int list -> int list -> bool wneuper@59275: datatype ppobj wneuper@59275: = PblObj of wneuper@59275: {branch: branch, wneuper@59275: cell: lrd option, wneuper@59275: ctxt: Proof.context, wneuper@59275: env: (istate * Proof.context) option, wneuper@59275: fmz: fmz, wneuper@59275: loc: (istate * Proof.context) option * (istate * Proof.context) option, wneuper@59275: meth: itm list, wneuper@59275: origin: ori list * spec * term, ostate: ostate, probl: itm list, result: term * term list, spec: spec} wneuper@59275: | PrfObj of wneuper@59275: {branch: branch, wneuper@59275: cell: lrd option, wneuper@59275: form: term, wneuper@59275: loc: (istate * Proof.context) option * (istate * Proof.context) option, wneuper@59275: ostate: ostate, result: term * term list, tac: tac} wneuper@59275: val pr_pos : int list -> string wneuper@59279: val pr_ctree : (pos -> ppobj -> string) -> ctree -> string wneuper@59275: val pr_short : pos -> ppobj -> string wneuper@59275: val pre_pos : pos -> pos wneuper@59275: val preconds2str : (bool * term) list -> string wneuper@59275: datatype ptform = Form of term | ModSpec of ocalhd wneuper@59279: datatype ctree = EmptyPtree | Nd of ppobj * ctree list wneuper@59275: val rep_pblobj : wneuper@59275: ppobj -> wneuper@59275: {branch: branch, wneuper@59275: cell: lrd option, wneuper@59275: ctxt: Proof.context, wneuper@59275: env: (istate * Proof.context) option, wneuper@59275: fmz: fmz, wneuper@59275: loc: (istate * Proof.context) option * (istate * Proof.context) option, wneuper@59275: meth: itm list, wneuper@59275: origin: ori list * spec * term, ostate: ostate, probl: itm list, result: term * term list, spec: spec} wneuper@59275: val rep_prfobj : wneuper@59275: ppobj -> wneuper@59275: {branch: branch, wneuper@59275: cell: lrd option, wneuper@59275: form: term, wneuper@59275: loc: (istate * Proof.context) option * (istate * Proof.context) option, wneuper@59275: ostate: ostate, result: term * term list, tac: tac} wneuper@59275: val repl : 'a list -> int -> 'a -> 'a list wneuper@59275: val repl_app : 'a list -> int -> 'a -> 'a list wneuper@59275: val repl_branch : branch -> ppobj -> ppobj wneuper@59275: val repl_ctxt : Proof.context -> ppobj -> ppobj wneuper@59275: val repl_domID : domID -> ppobj -> ppobj wneuper@59275: val repl_env : (istate * Proof.context) option -> ppobj -> ppobj wneuper@59275: val repl_form : term -> ppobj -> ppobj wneuper@59275: val repl_loc : (istate * Proof.context) option * (istate * Proof.context) option -> ppobj -> ppobj wneuper@59275: val repl_met : itm list -> ppobj -> ppobj wneuper@59275: val repl_metID : metID -> ppobj -> ppobj wneuper@59275: val repl_oris : ori list -> ppobj -> ppobj wneuper@59275: val repl_orispec : spec -> ppobj -> ppobj wneuper@59275: val repl_pbl : itm list -> ppobj -> ppobj wneuper@59275: val repl_pblID : pblID -> ppobj -> ppobj wneuper@59275: val repl_result : wneuper@59275: (istate * Proof.context) option * (istate * Proof.context) option -> wneuper@59275: term * term list -> ostate -> ppobj -> ppobj wneuper@59275: val repl_spec : spec -> ppobj -> ppobj wneuper@59275: val repl_tac : tac -> ppobj -> ppobj wneuper@59275: val res2str : term * term list -> string wneuper@59275: val rls_of : tac -> rls' wneuper@59275: val rls_of_rewset : tac -> rls' * subst option wneuper@59279: val rootthy : ctree -> theory wneuper@59275: val rta2str : rule * (term * term list) -> string wneuper@59275: val rule2tac : theory -> (term * term) list -> rule -> tac wneuper@59275: val safe2str : safe -> string wneuper@59275: type scrstate = env * loc_ * term option * term * safe * bool wneuper@59275: val scrstate2str : subst * loc_ * term option * term * safe * bool -> string wneuper@59275: val str2pos_ : string -> pos_ wneuper@59275: type sube = cterm' list wneuper@59275: val sube2str : string list -> string wneuper@59275: val sube2subst : theory -> string list -> (term * term) list wneuper@59275: val sube2subte : string list -> term list wneuper@59275: type subs = cterm' list wneuper@59275: val subs2subst : theory -> string list -> (term * term) list wneuper@59275: val subst2sube : (term * term) list -> string list wneuper@59275: val subst2subs : (term * term) list -> string list wneuper@59275: val subst2subs' : (term * term) list -> (string * string) list wneuper@59275: type subte = term list wneuper@59275: val subte2str : term list -> string wneuper@59275: val subte2sube : term list -> string list wneuper@59275: val subte2subst : term list -> (term * term) list wneuper@59275: datatype tac wneuper@59275: = Add_Find of cterm' | Add_Given of cterm' | Add_Relation of cterm' | Apply_Assumption of cterm' list wneuper@59275: | Apply_Method of metID | Begin_Sequ | Begin_Trans | CAScmd of cterm' | Calculate of string wneuper@59275: | Check_Postcond of pblID | Check_elementwise of cterm' | Collect_Trues | Conclude_And | Conclude_Or wneuper@59275: | Del_Find of cterm' | Del_Given of cterm' | Del_Relation of cterm' | Derive of rls' | Detail_Set of rls' wneuper@59275: | Detail_Set_Inst of subs * rls' | Empty_Tac | End_Detail | End_Intersect | End_Proof' | End_Ruleset wneuper@59275: | End_Sequ | End_Subproblem | End_Trans | Free_Solve | Group of con * int list wneuper@59275: | Init_Proof of cterm' list * spec | Model_Problem | Or_to_List | Refine_Problem of pblID wneuper@59275: | Refine_Tacitly of pblID | Rewrite of thm'' | Rewrite_Asm of thm'' | Rewrite_Inst of subs * thm'' wneuper@59275: | Rewrite_Set of rls' | Rewrite_Set_Inst of subs * rls' | Specify_Method of metID wneuper@59275: | Specify_Problem of pblID | Specify_Theory of domID | Split_And | Split_Intersect | Split_Or wneuper@59275: | Subproblem of domID * pblID | Substitute of sube | Tac of string | Take of cterm' | Take_Inst of cterm' wneuper@59275: val tac2IDstr : tac -> string wneuper@59275: datatype tac_ wneuper@59275: = Add_Find' of cterm' * itm list | Add_Given' of cterm' * itm list | Add_Relation' of cterm' * itm list wneuper@59275: | Apply_Assumption' of term list * term | Apply_Method' of metID * term option * istate * Proof.context wneuper@59275: | Begin_Sequ' | Begin_Trans' of term | CAScmd' of term wneuper@59275: | Calculate' of theory' * string * term * (term * thm') | Check_Postcond' of pblID * (term * term list) wneuper@59275: | Check_elementwise' of term * string * (term * term list) | Collect_Trues' of term wneuper@59275: | Conclude_And' of term | Conclude_Or' of term | Del_Find' of cterm' | Del_Given' of cterm' wneuper@59275: | Del_Relation' of cterm' | Derive' of rls wneuper@59275: | Detail_Set' of theory' * bool * rls * term * (term * term list) wneuper@59275: | Detail_Set_Inst' of theory' * bool * subst * rls * term * (term * term list) | Empty_Tac_ wneuper@59275: | End_Detail' of term * term list | End_Intersect' of term | End_Proof'' | End_Ruleset' of term wneuper@59275: | End_Sequ' | End_Subproblem' of term | End_Trans' of term * term list | Free_Solve' wneuper@59275: | Group' of con * int list * term | Init_Proof' of cterm' list * spec wneuper@59275: | Model_Problem' of pblID * itm list * itm list | Or_to_List' of term * term wneuper@59275: | Refine_Problem' of pblID * (itm list * (bool * term) list) wneuper@59275: | Refine_Tacitly' of pblID * pblID * domID * metID * itm list wneuper@59275: | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * (term * term list) wneuper@59275: | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * (term * term list) wneuper@59275: | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * (term * term list) wneuper@59275: | Rewrite_Set' of theory' * bool * rls * term * (term * term list) wneuper@59275: | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * (term * term list) wneuper@59275: | Specify_Method' of metID * ori list * itm list wneuper@59275: | Specify_Problem' of pblID * (bool * (itm list * (bool * term) list)) | Specify_Theory' of domID wneuper@59275: | Split_And' of term | Split_Intersect' of term | Split_Or' of term wneuper@59275: | Subproblem' of spec * ori list * term * fmz_ * Proof.context * term wneuper@59275: | Substitute' of rew_ord_ * rls * subte * term * term | Tac_ of theory * string * string * string wneuper@59275: | Take' of term | Take_Inst' of term wneuper@59275: val tac_2str : tac_ -> string wneuper@59275: val test_trans : ppobj -> bool wneuper@59275: val thm_of_rew : tac -> thmID * subst option wneuper@59275: val topt2str : term option -> string wneuper@59279: val update_branch : ctree -> pos -> branch -> ctree wneuper@59279: val update_ctxt : ctree -> pos -> Proof.context -> ctree wneuper@59279: val update_domID : ctree -> pos -> domID -> ctree wneuper@59279: val update_env : ctree -> pos -> (istate * Proof.context) option -> ctree wneuper@59279: val update_loc' : ctree -> pos -> (istate * Proof.context) option * (istate * Proof.context) option -> ctree wneuper@59279: val update_met : ctree -> pos -> itm list -> ctree wneuper@59279: val update_metID : ctree -> pos -> metID -> ctree wneuper@59279: val update_metppc : ctree -> pos -> itm list -> ctree wneuper@59279: val update_oris : ctree -> pos -> ori list -> ctree wneuper@59279: val update_orispec : ctree -> pos -> spec -> ctree wneuper@59279: val update_pbl : ctree -> pos -> itm list -> ctree wneuper@59279: val update_pblID : ctree -> pos -> pblID -> ctree wneuper@59279: val update_pblppc : ctree -> pos -> itm list -> ctree wneuper@59279: val update_spec : ctree -> pos -> spec -> ctree wneuper@59279: val update_tac : ctree -> pos -> tac -> ctree end wneuper@59275: *) wneuper@59275: wneuper@59275: (**) wneuper@59275: structure Ctree(**): CALC_TREEE(**) = wneuper@59275: struct wneuper@59275: (**) wneuper@59274: type result = term * term list neuper@37906: type env = (term * term) list; neuper@37906: neuper@37906: datatype branch = wneuper@59274: NoBranch | AndB | OrB wneuper@59274: | TransitiveB (* FIXXXME.0308: set branch from met in Apply_Method wneuper@59274: FIXXXME.0402: -"- in Begin_Trans'*) wneuper@59274: | SequenceB | IntersectB | CollectB | MapB; wneuper@59274: wneuper@59274: fun branch2str NoBranch = "NoBranch" (* for tests only *) neuper@37906: | branch2str AndB = "AndB" neuper@37906: | branch2str OrB = "OrB" neuper@37906: | branch2str TransitiveB = "TransitiveB" neuper@37906: | branch2str SequenceB = "SequenceB" neuper@37906: | branch2str IntersectB = "IntersectB" neuper@37906: | branch2str CollectB = "CollectB" neuper@37906: | branch2str MapB = "MapB"; neuper@37906: neuper@37906: datatype ostate = wneuper@59274: Incomplete | Complete | Inconsistent (* WN041020 latter still unused *); wneuper@59274: fun ostate2str Incomplete = "Incomplete" (* for tests only *) neuper@37906: | ostate2str Complete = "Complete" neuper@37906: | ostate2str Inconsistent = "Inconsistent"; neuper@37906: neuper@37906: type cellID = int; neuper@37906: type cid = cellID list; neuper@37906: wneuper@59274: type posel = int; (* for readability in funs accessing Ctree *) wneuper@59274: type pos = int list; neuper@37906: val pos2str = ints2str'; neuper@37906: datatype pos_ = wneuper@59274: Pbl (* PblObj-position: problem-type *) wneuper@59274: | Met (* PblObj-position: method *) wneuper@59274: | Frm (* PblObj-position: -> Pbl in ME (not by moveDown !) wneuper@59274: | PrfObj-position: formula *) wneuper@59274: | Res (* PblObj | PrfObj-position: result *) wneuper@59274: | Und; (* undefined*) neuper@37906: fun pos_2str Pbl = "Pbl" neuper@37906: | pos_2str Met = "Met" neuper@37906: | pos_2str Frm = "Frm" neuper@37906: | pos_2str Res = "Res" neuper@37906: | pos_2str Und = "Und"; wneuper@59124: fun str2pos_ "Pbl" = Pbl wneuper@59124: | str2pos_ "Met" = Met wneuper@59124: | str2pos_ "Frm" = Frm wneuper@59124: | str2pos_ "Res" = Res wneuper@59124: | str2pos_ "Und" = Und wneuper@59124: | str2pos_ str = error ("str2pos_: wrong argument = " ^ str) neuper@37906: neuper@37906: type pos' = pos * pos_; wneuper@59279: (*WN0312 remembering interator (pos * pos_) for ctree neuper@37906: pos : lev_on, lev_dn, lev_up, neuper@42003: lev_onFrm, lev_dnRes (..see solve Apply_Method !) neuper@42003: pos_: neuper@37906: # generate1 sets pos_ if possible ...?WN0502?NOT... neuper@37906: # generate1 does NOT set pos, because certain nodes can be lev_on OR lev_dn neuper@37906: exceptions: Begin/End_Trans neuper@37906: # thus generate(1) called in neuper@37906: .# assy, locate_gen neuper@37906: .# nxt_solv (tac_ -cases); general case: neuper@37906: val pos' = case pos' of (p,Res) => (lev_on p',Res) | _ => pos' neuper@37906: # WN050220, S(604): neuper@37906: generate1...(Rewrite(f,..,res))..(pos, pos_) neuper@37906: cappend_atomic.................pos ////// gets f+res always!!! neuper@37906: cut_tree....................pos, pos_ neuper@37906: *) wneuper@59274: fun pos'2str (p, p_) = pair2str (ints2str' p, pos_2str p_); wneuper@59274: fun pos's2str ps = (strs2str' o (map pos'2str)) ps; (* for tests only *) wneuper@59274: val e_pos' = ([], Und); neuper@37906: neuper@37906: fun res2str (t, ts) = pair2str (term2str t, terms2str ts); neuper@37906: neuper@37906: neuper@37906: neuper@37906: (*26.4.02: never used after introduction of scripts !!! neuper@37906: type loc = loc_ * (* + interpreter-state *) neuper@37906: (loc_ * rls') (* -"- for script of the ruleset*) neuper@37906: option; neuper@37926: val e_loc = ([],NONE):loc; neuper@37906: val ee_loc = (e_loc,e_loc);*) neuper@37906: neuper@37906: neuper@37906: datatype safe = Sundef | Safe | Unsafe | Helpless; neuper@37906: fun safe2str Sundef = "Sundef" neuper@37906: | safe2str Safe = "Safe" neuper@37906: | safe2str Unsafe = "Unsafe" neuper@37906: | safe2str Helpless = "Helpless"; neuper@37906: neuper@37906: type subs = cterm' list; (*16.11.00 for FE-KE*) neuper@37906: val e_subs = ["(bdv, x)"]; neuper@37906: neuper@42433: (* argument type of tac Rewrite_Inst *) neuper@37906: type sube = cterm' list; wneuper@59274: val e_sube = []: cterm' list; neuper@37906: fun sube2str s = strs2str s; neuper@37906: neuper@37906: (*._sub_stitution as _t_erms of _e_qualities.*) neuper@37906: type subte = term list; wneuper@59274: val e_subte = []: term list; neuper@37906: fun subte2str ss = terms2str ss; neuper@37906: neuper@42360: val subte2sube = map term2str; neuper@42360: val subst2subs = map (pair2str o (apfst term2str) o (apsnd term2str)); wneuper@59159: fun subst2sube subst = map term2str (map HOLogic.mk_eq subst) neuper@42360: val subst2subs' = map ((apfst term2str) o (apsnd term2str)); neuper@42385: fun subs2subst thy s = map (isapair2pair o (parse_patt thy)) s; neuper@42385: fun sube2subst thy s = map (dest_equals' o (parse_patt thy)) s; neuper@42360: val sube2subte = map str2term; neuper@42360: val subte2subst = map HOLogic.dest_eq; neuper@37906: neuper@37906: fun isasub2subst isasub = ((map isapair2pair) o isalist2list) isasub; neuper@37906: neuper@37906: type scrstate = (*state for script interpreter*) neuper@37906: env(*stack*) (*used to instantiate tac for checking assod neuper@37906: 12.03.noticed: e_ not updated during execution ?!?*) neuper@37906: * loc_ (*location of tac in script*) neuper@37906: * term option(*argument of curried functions*) neuper@37906: * term (*value obtained by tac executed neuper@37906: updated also after a derivation by 'new_val'*) neuper@37906: * safe (*estimation of how result will be obtained*) neuper@37906: * bool; (*true = strongly .., false = weakly associated: neuper@37906: only used during ass_dn/up*) wneuper@59274: val e_scrstate = ([],[],NONE,e_term,Sundef,false): scrstate; neuper@42360: fun topt2str NONE = "NONE" neuper@42360: | topt2str (SOME t) = "SOME" ^ term2str t; neuper@42360: fun scrstate2str (env, loc_, topt, t, safe, bool) = neuper@42360: "(" ^ env2str env ^ ", " ^ loc_2str loc_ ^ ", " ^ topt2str topt ^ ", \n" ^ neuper@42360: term2str t ^ ", " ^ safe2str safe ^ ", " ^ bool2str bool ^ ")"; neuper@37906: neuper@41996: (* for handling type istate see fun from_pblobj_or_detail', +? *) neuper@41996: datatype istate = (*interpreter state*) neuper@41996: Uistate (*undefined in modspec, in '_deriv'ation*) neuper@41996: | ScrState of scrstate (*for script interpreter*) neuper@41996: | RrlsState of rrlsstate; (*for reverse rewriting*) wneuper@59274: val e_istate = (ScrState ([],[],NONE,e_term,Sundef,false)); neuper@48761: val e_ctxt = Proof_Context.init_global @{theory "Pure"}; neuper@41992: neuper@41992: (* ATTENTION: does _not_ recognise Variable.declare_constraints, etc...*) neuper@48761: fun is_e_ctxt ctxt = Theory.eq_thy (Proof_Context.theory_of ctxt, @{theory "Pure"}); neuper@37906: neuper@37906: type iist = istate option * istate option; neuper@37906: (*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*) neuper@37906: neuper@37906: neuper@37906: fun rta2str (r,(t,a)) = "\n("^(rule2str r)^",("^(term2str t)^", "^ neuper@37906: (terms2str a)^"))"; neuper@37906: fun istate2str Uistate = "Uistate" wneuper@59274: | istate2str (ScrState (e, l, to, t, s, b)) = neuper@37906: "ScrState ("^ subst2str e ^",\n "^ neuper@37906: loc_2str l ^", "^ termopt2str to ^",\n "^ neuper@37906: term2str t ^", "^ safe2str s ^", "^ bool2str b ^")" neuper@37906: | istate2str (RrlsState (t,t1,rss,rtas)) = neuper@37906: "RrlsState ("^(term2str t)^", "^(term2str t1)^", "^ neuper@37906: ((strs2str o (map (strs2str o (map rule2str)))) rss)^", "^ neuper@37906: ((strs2str o (map rta2str)) rtas)^")"; neuper@37925: fun istates2str (NONE, NONE) = "(#NONE, #NONE)" neuper@37925: | istates2str (NONE, SOME ist) = "(#NONE,\n#SOME "^istate2str ist^")" neuper@37925: | istates2str (SOME ist, NONE) = "(#SOME "^istate2str ist^",\n #NONE)" neuper@37925: | istates2str (SOME i1, SOME i2) = "(#SOME "^istate2str i1^",\n #SOME "^ wneuper@59274: istate2str i2 ^")"; neuper@37906: neuper@37906: fun new_val v (ScrState (env, loc_, topt, _, safe, bool)) = neuper@37906: (ScrState (env, loc_, topt, v, safe, bool)) neuper@38031: | new_val _ _ = error "new_val: only for ScrState"; neuper@37906: neuper@37906: datatype con = land | lor; neuper@37906: neuper@37906: neuper@37906: wneuper@59252: (*.tactics propagate the construction of the calc-tree; neuper@37906: there are neuper@37906: (a) 'specsteps' for the specify-phase, and others for the solve-phase neuper@37906: (b) those of the solve-phase are 'initac's and others; neuper@37906: initacs start with a formula different from the preceding formula. neuper@37906: see 'type tac_' for the internal representation of tactics.*) wneuper@59274: datatype tac = (* TODO: arrange according to signature *) neuper@37906: Init_Proof of ((cterm' list) * spec) neuper@37906: (*'specsteps'...*) neuper@37906: | Model_Problem neuper@37906: | Refine_Problem of pblID | Refine_Tacitly of pblID neuper@37906: neuper@37906: | Add_Given of cterm' | Del_Given of cterm' neuper@37906: | Add_Find of cterm' | Del_Find of cterm' neuper@37906: | Add_Relation of cterm' | Del_Relation of cterm' neuper@37906: neuper@37906: | Specify_Theory of domID | Specify_Problem of pblID neuper@37906: | Specify_Method of metID neuper@37906: (*...'specsteps'*) neuper@37906: | Apply_Method of metID neuper@37906: (*.creates an 'istate' in PblObj.env; in case of 'init_form' neuper@37906: creates a formula at ((lev_on o lev_dn) p, Frm) and in this ppobj.'loc' neuper@37925: 'SOME istate' (at fst of 'loc'). neuper@37906: As each step (in the solve-phase) has a resulting formula (at the front-end) neuper@37906: Apply_Method also does the 1st step in the script (an 'initac') if there neuper@37906: is no 'init_form' .*) neuper@37906: | Check_Postcond of pblID neuper@37906: | Free_Solve neuper@37906: wneuper@59253: (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end wneuper@59253: because there all the thms are present with both (thmID, thm) wneuper@59253: (where user-views can show both or only one of (thmID, thm)), wneuper@59253: and thm is created from ThmID by assoc_thm'' when entering isabisac *) wneuper@59252: | Rewrite_Inst of ( subs * thm'') | Rewrite of thm'' | Rewrite_Asm of thm'' neuper@37906: | Rewrite_Set_Inst of ( subs * rls') | Rewrite_Set of rls' neuper@37906: | Detail_Set_Inst of ( subs * rls') | Detail_Set of rls' neuper@37906: | End_Detail (*end of script from next_tac, neuper@37906: in solve: switches back to parent script WN0509 drop!*) neuper@37906: | Derive of rls' (*an input formula using rls WN0509 drop!*) neuper@37906: | Calculate of string (* plus | minus | times | cancel | pow | sqrt *) neuper@37906: | End_Ruleset neuper@37906: | Substitute of sube | Apply_Assumption of cterm' list neuper@37906: neuper@37906: | Take of cterm' (*an 'initac'*) neuper@37906: | Take_Inst of cterm' neuper@37906: | Group of (con * int list ) neuper@37906: | Subproblem of (domID * pblID) (*an 'initac'*) neuper@37906: | CAScmd of cterm' (*6.6.02 URD: Function formula; WN0509 drop!*) neuper@37906: | End_Subproblem (*WN0509 drop!*) neuper@37906: neuper@37906: | Split_And | Conclude_And neuper@37906: | Split_Or | Conclude_Or neuper@37906: | Begin_Trans | End_Trans neuper@37906: | Begin_Sequ | End_Sequ(* substitute root.env *) neuper@37906: | Split_Intersect | End_Intersect neuper@37906: | Check_elementwise of cterm' | Collect_Trues neuper@42394: | Or_to_List (*WN120315 ~ @{thm d2_prescind1},2,3,4 in PolyEq.thy *) neuper@37906: neuper@38051: | Empty_Tac (* TODO.11.6.03 ... of string: could carry msg of (Notappl msg) neuper@38051: in 'helpless'*) neuper@38051: | Tac of string (* eg.'repeat'*WN0509 drop! (ab)used to report syntaxerror *) neuper@38051: | End_Proof'; (* inout *) neuper@37906: neuper@37906: (* tac2str /--> library.sml: needed in dialog.sml for 'separable *) wneuper@59274: fun tac2str ma = case ma of neuper@37906: Init_Proof (ppc, spec) => neuper@37906: "Init_Proof "^(pair2str (strs2str ppc, spec2str spec)) neuper@37906: | Model_Problem => "Model_Problem " neuper@37906: | Refine_Tacitly pblID => "Refine_Tacitly "^(strs2str pblID) neuper@37906: | Refine_Problem pblID => "Refine_Problem "^(strs2str pblID) neuper@37906: | Add_Given cterm' => "Add_Given "^cterm' neuper@37906: | Del_Given cterm' => "Del_Given "^cterm' neuper@37906: | Add_Find cterm' => "Add_Find "^cterm' neuper@37906: | Del_Find cterm' => "Del_Find "^cterm' neuper@37906: | Add_Relation cterm' => "Add_Relation "^cterm' neuper@37906: | Del_Relation cterm' => "Del_Relation "^cterm' neuper@37906: neuper@37906: | Specify_Theory domID => "Specify_Theory "^(quote domID ) neuper@37906: | Specify_Problem pblID => "Specify_Problem "^(strs2str pblID ) neuper@37906: | Specify_Method metID => "Specify_Method "^(strs2str metID) neuper@37906: | Apply_Method metID => "Apply_Method "^(strs2str metID) neuper@37906: | Check_Postcond pblID => "Check_Postcond "^(strs2str pblID) neuper@37906: | Free_Solve => "Free_Solve" neuper@37906: wneuper@59253: | Rewrite_Inst (subs, (id, thm)) => wneuper@59253: "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> term2str))) wneuper@59253: | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> term2str) wneuper@59253: | Rewrite_Asm (id, thm) => "Rewrite_Asm " ^ spair2str (id, thm |> Thm.prop_of |> term2str) neuper@37906: | Rewrite_Set_Inst (subs, rls) => neuper@37906: "Rewrite_Set_Inst "^(pair2str (subs2str subs, quote rls)) neuper@37906: | Rewrite_Set rls => "Rewrite_Set "^(quote rls ) neuper@37906: | Detail_Set rls => "Detail_Set "^(quote rls ) neuper@37906: | Detail_Set_Inst (subs, rls) => neuper@37906: "Detail_Set_Inst "^(pair2str (subs2str subs, quote rls)) neuper@37906: | End_Detail => "End_Detail" neuper@37906: | Derive rls' => "Derive "^rls' neuper@37906: | Calculate op_ => "Calculate "^op_ neuper@37906: | Substitute sube => "Substitute "^sube2str sube neuper@37906: | Apply_Assumption ct's => "Apply_Assumption "^(strs2str ct's) neuper@37906: neuper@37906: | Take cterm' => "Take "^(quote cterm' ) neuper@37906: | Take_Inst cterm' => "Take_Inst "^(quote cterm' ) neuper@37906: | Group (con, ints) => neuper@37906: "Group "^(pair2str (con2str con, ints2str ints)) neuper@37906: | Subproblem (domID, pblID) => neuper@37906: "Subproblem "^(pair2str (domID, strs2str pblID)) neuper@37906: (*| Subproblem_Full (spec, cts') => neuper@37906: "Subproblem_Full "^(pair2str (spec2str spec, strs2str cts'))*) neuper@37906: | End_Subproblem => "End_Subproblem" neuper@37906: | CAScmd cterm' => "CAScmd "^(quote cterm') neuper@37906: neuper@37906: | Check_elementwise cterm'=> "Check_elementwise "^(quote cterm') neuper@37906: | Or_to_List => "Or_to_List " neuper@37906: | Collect_Trues => "Collect_Trues" neuper@37906: neuper@37906: | Empty_Tac => "Empty_Tac" neuper@37906: | Tac string => "Tac "^string neuper@37906: | End_Proof' => "tac End_Proof'" neuper@37906: | _ => "tac2str not impl. for ?!"; neuper@37906: wneuper@59253: fun is_empty_tac tac = case tac of Empty_Tac => true | _ => false wneuper@59253: wneuper@59253: fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2 wneuper@59253: | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2 wneuper@59253: | eq_tac (Rewrite_Set id1, Rewrite_Set id2) = id1 = id2 wneuper@59253: | eq_tac (Rewrite_Set_Inst (_, id1), Rewrite_Set_Inst (_, id2)) = id1 = id2 wneuper@59253: | eq_tac (Calculate id1, Calculate id2) = id1 = id2 wneuper@59253: | eq_tac _ = false wneuper@59253: neuper@37906: fun is_rewset (Rewrite_Set_Inst _) = true neuper@37906: | is_rewset (Rewrite_Set _) = true neuper@37906: | is_rewset _ = false; neuper@37906: fun is_rewtac (Rewrite _) = true neuper@37906: | is_rewtac (Rewrite_Inst _) = true neuper@37906: | is_rewtac (Rewrite_Asm _) = true neuper@37906: | is_rewtac tac = is_rewset tac; neuper@37906: wneuper@59274: fun tac2IDstr ma = case ma of neuper@37906: Model_Problem => "Model_Problem" neuper@37906: | Refine_Tacitly pblID => "Refine_Tacitly" neuper@37906: | Refine_Problem pblID => "Refine_Problem" neuper@37906: | Add_Given cterm' => "Add_Given" neuper@37906: | Del_Given cterm' => "Del_Given" neuper@37906: | Add_Find cterm' => "Add_Find" neuper@37906: | Del_Find cterm' => "Del_Find" neuper@37906: | Add_Relation cterm' => "Add_Relation" neuper@37906: | Del_Relation cterm' => "Del_Relation" neuper@37906: neuper@37906: | Specify_Theory domID => "Specify_Theory" neuper@37906: | Specify_Problem pblID => "Specify_Problem" neuper@37906: | Specify_Method metID => "Specify_Method" neuper@37906: | Apply_Method metID => "Apply_Method" neuper@37906: | Check_Postcond pblID => "Check_Postcond" neuper@37906: | Free_Solve => "Free_Solve" neuper@37906: neuper@37906: | Rewrite_Inst (subs,thm')=> "Rewrite_Inst" neuper@37906: | Rewrite thm' => "Rewrite" neuper@37906: | Rewrite_Asm thm' => "Rewrite_Asm" neuper@37906: | Rewrite_Set_Inst (subs, rls) => "Rewrite_Set_Inst" neuper@37906: | Rewrite_Set rls => "Rewrite_Set" neuper@37906: | Detail_Set rls => "Detail_Set" neuper@37906: | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst" neuper@37906: | Derive rls' => "Derive " neuper@37906: | Calculate op_ => "Calculate " neuper@37906: | Substitute subs => "Substitute" neuper@37906: | Apply_Assumption ct's => "Apply_Assumption" neuper@37906: neuper@37906: | Take cterm' => "Take" neuper@37906: | Take_Inst cterm' => "Take_Inst" neuper@37906: | Group (con, ints) => "Group" neuper@37906: | Subproblem (domID, pblID) => "Subproblem" neuper@37906: | End_Subproblem => "End_Subproblem" neuper@37906: | CAScmd cterm' => "CAScmd" neuper@37906: neuper@37906: | Check_elementwise cterm'=> "Check_elementwise" neuper@37906: | Or_to_List => "Or_to_List " neuper@37906: | Collect_Trues => "Collect_Trues" neuper@37906: neuper@37906: | Empty_Tac => "Empty_Tac" neuper@37906: | Tac string => "Tac " neuper@37906: | End_Proof' => "End_Proof'" neuper@37906: | _ => "tac2str not impl. for ?!"; neuper@37906: neuper@37906: fun rls_of (Rewrite_Set_Inst (_, rls)) = rls neuper@37906: | rls_of (Rewrite_Set rls) = rls neuper@38031: | rls_of tac = error ("rls_of: called with tac '"^tac2IDstr tac^"'"); neuper@37906: neuper@37906: fun thm_of_rew (Rewrite_Inst (subs,(thmID,_))) = wneuper@59274: (thmID, SOME ((subs2subst (assoc_thy "Isac") subs))) neuper@37925: | thm_of_rew (Rewrite (thmID,_)) = (thmID, NONE) neuper@37925: | thm_of_rew (Rewrite_Asm (thmID,_)) = (thmID, NONE); neuper@37906: neuper@37906: fun rls_of_rewset (Rewrite_Set_Inst (subs,rls)) = wneuper@59274: (rls, SOME ((subs2subst (assoc_thy "Isac") subs))) neuper@37925: | rls_of_rewset (Rewrite_Set rls) = (rls, NONE) neuper@37925: | rls_of_rewset (Detail_Set rls) = (rls, NONE) neuper@37906: | rls_of_rewset (Detail_Set_Inst (subs, rls)) = wneuper@59274: (rls, SOME ((subs2subst (assoc_thy "Isac") subs))); neuper@37906: s1210629013@52153: fun rule2tac thy _ (Calc (opID, thm)) = Calculate (assoc_calc thy opID) wneuper@59253: | rule2tac _ [] (Thm thm'') = Rewrite thm'' wneuper@59253: | rule2tac _ subst (Thm thm'') = wneuper@59253: Rewrite_Inst (subst2subs subst, thm'') s1210629013@52153: | rule2tac _ [] (Rls_ rls) = Rewrite_Set (id_rls rls) s1210629013@52153: | rule2tac _ subst (Rls_ rls) = neuper@37906: Rewrite_Set_Inst (subst2subs subst, (id_rls rls)) s1210629013@52153: | rule2tac _ _ rule = neuper@38031: error ("rule2tac: called with '" ^ rule2str rule ^ "'"); neuper@37906: neuper@37906: type fmz_ = cterm' list; neuper@37906: neuper@37906: (*.a formalization of an example containing data neuper@37906: sufficient for mechanically finding the solution for the example.*) neuper@37906: (*FIXME.WN051014: dont store fmz = (_,spec) in the PblObj, neuper@37906: this is done in origin*) neuper@37906: type fmz = fmz_ * spec; neuper@37906: val e_fmz = ([],e_spec); neuper@37906: neuper@42360: (* tac_ contains results from check in 'fun applicable_in'. neuper@42360: This is useful for costly results, e.g. from rewriting; neuper@42360: however, these results might be changed by Scripts like neuper@42360: " eq = (Rewrite_Set ansatz_rls False) eql;" ^ neuper@42360: " eq = drop_questionmarks eq;" ^ neuper@42360: " eq = (Rewrite_Set equival_trans False) eq;" ^ neuper@42360: WN120106 TODO ANALOGOUSLY TO Substitute': neuper@42360: So tac_ contains the term t the result was calculated from neuper@42360: in order to compare t with t' possibly changed by "Expr " neuper@42360: and re-calculate result if t<>t'*) wneuper@59274: datatype tac_ = (* TODO: arrange according to signature *) neuper@42023: Init_Proof' of ((cterm' list) * spec) neuper@42023: | Model_Problem' of neuper@42023: pblID * neuper@42023: itm list * (*the 'untouched' pbl*) neuper@42023: itm list (*the casually completed met*) neuper@42023: | Refine_Tacitly' of neuper@42023: pblID * (*input*) neuper@42023: pblID * (*the refined from applicable_in*) neuper@42023: domID * (*from new pbt?! filled in specify*) neuper@42023: metID * (*from new pbt?! filled in specify*) neuper@42023: itm list (*drop ! 9.03: remains [] for neuper@37906: Model_Problem recognizing its activation*) neuper@42023: | Refine_Problem' of (pblID * (itm list * (bool * Term.term) list)) neuper@42023: (*FIXME?040215 drop: done automatically in init_proof + Subproblem'*) neuper@42023: | Add_Given' of neuper@42023: cterm' * neuper@42023: itm list (*updated with input in fun specify_additem*) neuper@42023: | Add_Find' of cterm' * itm list (* see Add_Given' *) neuper@42023: | Add_Relation' of cterm' * itm list (* see Add_Given' *) neuper@42023: | Del_Given' of cterm' | Del_Find' of cterm' | Del_Relation' of cterm' neuper@42023: (*4.00.: all.. term: in applicable_in ..? Syn ?only for FormFK?*) neuper@42023: | Specify_Theory' of domID neuper@42023: | Specify_Problem' of neuper@42023: (pblID * (* *) neuper@42023: (bool * (* matches *) neuper@42023: (itm list * (* ppc *) neuper@42023: (bool * term) list))) (* preconditions *) neuper@42023: | Specify_Method' of neuper@42023: metID * neuper@42023: ori list * (*repl. "#undef"*) neuper@42023: itm list (*... updated from pbl to met*) neuper@42023: | Apply_Method' of neuper@42023: metID * neuper@42023: (term option) * (*init_form*) neuper@42023: istate * Proof.context neuper@42023: | Check_Postcond' of neuper@42023: pblID * neuper@42023: (term * (*returnvalue of script in solve*) neuper@42023: term list) (*collect by get_assumptions_ in applicable_in, except if neuper@37906: butlast tac is Check_elementwise: take only these asms*) neuper@42023: | Free_Solve' wneuper@55501: (* context_thy would be simpler if instead thm' woudl be thm *) wneuper@59253: | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * (term * term list) wneuper@59274: | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * result wneuper@59274: | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * result wneuper@59274: | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * result wneuper@59274: | Detail_Set_Inst' of theory' * bool * subst * rls * term * result wneuper@59274: | Rewrite_Set' of theory' * bool * rls * term * result wneuper@59274: | Detail_Set' of theory' * bool * rls * term * result neuper@42023: | End_Detail' of (term * (term list)) (*see End_Trans'*) neuper@42023: | End_Ruleset' of term neuper@42023: | Derive' of rls neuper@42023: | Calculate' of theory' * string * term * (term * thm') neuper@42023: | Substitute' of neuper@42360: rew_ord_ * (*for re-calculation *) neuper@42360: rls * (*for re-calculation *) neuper@42360: subte * (*the 'substitution': terms of type bool*) neuper@42360: term * (*to be substituted in *) neuper@42360: term (*resulting from the substitution *) neuper@42023: | Apply_Assumption' of term list * term neuper@42023: | Take' of term neuper@42023: | Take_Inst' of term neuper@42023: | Subproblem' of neuper@42023: (spec * neuper@42023: (ori list) * (* filled in assod Subproblem' *) neuper@42023: term * (*-"-, headline of calc-head *) neuper@42023: fmz_ * neuper@42023: Proof.context *(* transported from assod to generate1 *) neuper@42023: term) (* Subproblem(dom,pbl) OR cascmd*) neuper@42023: | CAScmd' of term neuper@42023: | End_Subproblem' of term (*???*) neuper@42023: | Split_And' of term | Conclude_And' of term neuper@42023: | Split_Or' of term | Conclude_Or' of term neuper@42023: | Begin_Trans' of term | End_Trans' of (term * (term list)) neuper@42023: | Begin_Sequ' | End_Sequ'(* substitute root.env*) neuper@42023: | Split_Intersect' of term | End_Intersect' of term neuper@42023: | Check_elementwise' of (*special case:*) neuper@42023: term * (*(1)the current formula: [x=1,x=...]*) neuper@42023: string * (*(2)the pred from Check_elementwise *) neuper@42023: (term * (*(3)composed from (1) and (2): {x. pred}*) neuper@42023: term list) (*20.5.03 assumptions*) neuper@42023: | Or_to_List' of term * term (* (a | b, [a,b]) *) neuper@42023: | Collect_Trues' of term neuper@42023: | Empty_Tac_ neuper@42023: | Tac_ of (*for dummies*) neuper@42023: theory * neuper@42023: string * (*form*) neuper@42023: string * (*in Tac*) neuper@42023: string (*result of Tac".."*) neuper@42023: | End_Proof'';(*End_Proof:inout*) neuper@37906: neuper@37906: fun tac_2str ma = case ma of neuper@37906: Init_Proof' (ppc, spec) => neuper@37906: "Init_Proof' "^(pair2str (strs2str ppc, spec2str spec)) neuper@37906: | Model_Problem' (pblID,_,_) => "Model_Problem' "^(strs2str pblID ) neuper@37906: | Refine_Tacitly'(p,prefin,domID,metID,itms)=> neuper@37906: "Refine_Tacitly' (" neuper@37906: ^(strs2str p)^", "^(strs2str prefin)^", " neuper@37906: ^domID^", "^(strs2str metID)^", pbl-itms)" neuper@37906: | Refine_Problem' ms => "Refine_Problem' ("^(*matchs2str ms*)"..."^")" neuper@37906: (*| Match_Problem' (pI, (ok, (itms, pre))) => neuper@37906: "Match_Problem' "^(spair2str (strs2str pI, neuper@37906: spair2str (bool2str ok, neuper@37924: spair2str ("itms2str_ itms", neuper@37906: "items2str pre"))))*) neuper@37906: | Add_Given' cterm' => "Add_Given' "(*^cterm'*) neuper@37906: | Del_Given' cterm' => "Del_Given' "(*^cterm'*) neuper@37906: | Add_Find' cterm' => "Add_Find' "(*^cterm'*) neuper@37906: | Del_Find' cterm' => "Del_Find' "(*^cterm'*) neuper@37906: | Add_Relation' cterm' => "Add_Relation' "(*^cterm'*) neuper@37906: | Del_Relation' cterm' => "Del_Relation' "(*^cterm'*) neuper@37906: neuper@37906: | Specify_Theory' domID => "Specify_Theory' "^(quote domID ) neuper@37906: | Specify_Problem' (pI, (ok, (itms, pre))) => neuper@37906: "Specify_Problem' "^(spair2str (strs2str pI, neuper@37906: spair2str (bool2str ok, neuper@37924: spair2str ("itms2str_ itms", neuper@37906: "items2str pre")))) neuper@37906: | Specify_Method' (pI,oris,itms) => neuper@37906: "Specify_Method' ("^metID2str pI^", "^oris2str oris^", )" neuper@37906: bonzai@41948: | Apply_Method' (metID,_,_,_) => "Apply_Method' "^(strs2str metID) neuper@37906: | Check_Postcond' (pblID,(scval,asm)) => neuper@42018: "Check_Postcond' " ^ neuper@42018: (spair2str (strs2str pblID, spair2str (term2str scval, terms2str asm))) neuper@37906: neuper@37906: | Free_Solve' => "Free_Solve'" neuper@37906: neuper@37906: | Rewrite_Inst' (*subs,thm'*) _ => neuper@37906: "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*) neuper@37906: | Rewrite' thm' => "Rewrite' "(*^(spair2str thm')*) neuper@37906: | Rewrite_Asm' thm' => "Rewrite_Asm' "(*^(spair2str thm')*) neuper@37906: | Rewrite_Set_Inst' (*subs,thm'*) _ => neuper@37906: "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*) neuper@38053: | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => neuper@38053: "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^ "," ^ id_rls rls' ^ "," ^ neuper@38053: term2str f ^ ",(" ^ term2str f' ^ "," ^ terms2str asm ^ "))" neuper@37906: | End_Detail' _ => "End_Detail' xxx" neuper@37906: | Detail_Set' _ => "Detail_Set' xxx" neuper@37906: | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx" neuper@37906: neuper@37906: | Derive' rls => "Derive' "^id_rls rls neuper@37906: | Calculate' _ => "Calculate' " neuper@42360: | Substitute' _ => "Substitute' "(*^(subs2str subs)*) neuper@37906: | Apply_Assumption' ct's => "Apply_Assumption' "(*^(strs2str ct's)*) neuper@37906: neuper@37906: | Take' cterm' => "Take' "(*^(quote cterm' )*) neuper@37906: | Take_Inst' cterm' => "Take_Inst' "(*^(quote cterm' )*) neuper@41983: | Subproblem' (spec, oris, _, _, _, pbl_form) => neuper@37906: "Subproblem' "(*^(pair2str (domID, strs2str ,...))*) neuper@37906: | End_Subproblem' _ => "End_Subproblem'" neuper@37906: | CAScmd' cterm' => "CAScmd' "(*^(quote cterm')*) neuper@37906: neuper@37906: | Empty_Tac_ => "Empty_Tac_" neuper@37906: | Tac_ (_,form,id,result) => "Tac_ (thy,"^form^","^id^","^result^")" neuper@37906: | _ => "tac_2str not impl. for arg"; neuper@37906: neuper@37906: (*'executed tactics' (tac_s) with local environment etc.; neuper@37906: used for continuing eval script + for generate*) neuper@37906: type ets = neuper@37906: (loc_ * (* of tactic in scr, tactic (weakly) associated with tac_*) neuper@37906: (tac_ * (* (for generate) *) neuper@37906: env * (* with 'tactic=result' as a rule, tactic ev. _not_ ready: neuper@37906: for handling 'parallel let'*) neuper@37906: env * (* with results of (ready) tacs *) neuper@37906: term * (* itr_arg of tactic, for upd. env at Repeat, Try*) neuper@37906: term * (* result value of the tac *) neuper@37906: safe)) neuper@37906: list; wneuper@59274: val Ets = []: ets; neuper@37906: neuper@37906: neuper@37906: fun ets2s (l,(m,eno,env,iar,res,s)) = neuper@38053: "\n(" ^ loc_2str l ^ ",(" ^ tac_2str m ^ neuper@38053: ",\n ens= " ^ subst2str eno ^ neuper@38053: ",\n env= " ^ subst2str env ^ neuper@38053: ",\n iar= " ^ term2str iar ^ neuper@38053: ",\n res= " ^ term2str res ^ neuper@38053: ",\n " ^ safe2str s ^ "))"; wneuper@59274: fun ets2str (ets: ets) = (strs2str o (map ets2s)) ets; neuper@37906: neuper@37906: wneuper@59279: type envp =(*9.5.03: unused, delete with field in ctree.PblObj FIXXXME*) neuper@37906: (int * term list) list * (*assoc-list: args of met*) neuper@37906: (int * rls) list * (*assoc-list: tacs already done ///15.9.00*) neuper@37906: (int * ets) list * (*assoc-list: tacs etc. already done*) neuper@37906: (string * pos) list; (*asms * from where*) wneuper@59274: val empty_envp = ([], [], [], []): envp; neuper@37906: wneuper@59274: datatype ppobj = (* TODO: arrange according to signature *) neuper@41975: PrfObj of neuper@41975: {cell : lrd option, (* where in form tac has been applied *) neuper@41975: (*^^^FIXME.WN0607 rename this field*) neuper@41975: form : term, (* where tac is applied to *) neuper@41975: tac : tac, (* also in istate *) neuper@41977: loc : (istate * (* script interpreter state *) neuper@41977: Proof.context) (* context for provers, type inference *) neuper@41977: option * (* both for interpreter location on Frm, Pbl, Met *) neuper@41977: (istate * (* script interpreter state *) neuper@41977: Proof.context) (* context for provers, type inference *) neuper@41977: option, (* both for interpreter location on Res *) neuper@41977: (*(NONE,NONE) <==> e_istate ! see update_loc, get_loc*) neuper@41975: branch: branch, (* only rudimentary *) wneuper@59274: result: result, (* result and assumptions *) neuper@41975: ostate: ostate} (* Complete <=> result is OK *) neuper@41975: | PblObj of neuper@41975: {cell : lrd option, (* unused: meaningful only for some _Prf_Obj *) neuper@41975: fmz : fmz, (* from init:FIXME never use this spec;-drop *) neuper@41975: origin: (ori list) * (* representation from fmz+pbt neuper@41975: for efficiently adding items in probl, meth *) neuper@41977: spec * (* updated by Refine_Tacitly *) neuper@41977: term, (* headline of calc-head, as calculated initially(!)*) neuper@41975: spec : spec, (* explicitly input *) neuper@41975: probl : itm list, (* itms explicitly input *) neuper@41975: meth : itm list, (* itms automatically added to copy of probl *) neuper@41988: ctxt : Proof.context, (* WN110513 introduced to avoid [*] [**]*) neuper@41975: env : (istate * Proof.context) option, neuper@41977: (* istate only for initac in script neuper@41984: context for specify phase on this node NO.. neuper@41990: ..NO: this conflicts with init_form/initac: see Apply_Method without init_form *) neuper@41984: loc : (istate * Proof.context) option * (istate * (* like PrfObj *) neuper@41988: Proof.context) option, (* for spec-phase [*], NO.. neuper@41988: ..NO: raises errors not tracable on WN110513 [**]*) neuper@41977: branch: branch, (* like PrfObj *) wneuper@59274: result: result, (* like PrfObj *) neuper@41977: ostate: ostate}; (* like PrfObj *) neuper@37906: neuper@37906: (*.this tree contains isac's calculations; TODO.WN03 rename to ctree; neuper@37906: the structure has been copied from an early version of Theorema(c); neuper@37906: it has the disadvantage, that there is no space neuper@37906: for the first tactic in a script generating the first formula at (p,Frm); neuper@37906: this trouble has been covered by 'init_form' and 'Take' so far, neuper@37906: but it is crucial if the first tactic in a script is eg. 'Subproblem'; neuper@37906: see 'type tac ', Apply_Method. neuper@37906: .*) wneuper@59279: datatype ctree = neuper@37906: EmptyPtree wneuper@59279: | Nd of ppobj * (ctree list); wneuper@59279: val e_ctree = EmptyPtree; wneuper@59279: type state = ctree * pos neuper@37906: neuper@37906: fun rep_prfobj (PrfObj {cell,form,tac,loc,branch,result,ostate}) = neuper@37906: {cell=cell,form=form,tac=tac,loc=loc,branch=branch,result=result,ostate=ostate}; neuper@41988: fun rep_pblobj (PblObj {cell,origin,fmz,spec,probl,meth,ctxt, neuper@41988: env,loc,branch,result,ostate}) = neuper@41988: {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,ctxt=ctxt, neuper@41988: env=env,loc=loc,branch=branch,result=result,ostate=ostate}; neuper@37906: fun is_prfobj (PrfObj _) = true neuper@37906: | is_prfobj _ =false; neuper@37906: (*val is_prfobj' = get_obj is_prfobj; *) neuper@37906: fun is_pblobj (PblObj _) = true neuper@37906: | is_pblobj _ = false; neuper@37906: (*val is_pblobj' = get_obj is_pblobj; 'Error: unbound constructor get_obj'*) neuper@37906: neuper@37906: neuper@37906: exception PTREE of string; neuper@37906: fun nth _ [] = raise PTREE "nth _ []" neuper@37906: | nth 1 (x::xs) = x neuper@37906: | nth n (x::xs) = nth (n-1) xs; neuper@37906: (*> nth 2 [11,22,33]; -->> val it = 22 : int*) neuper@37906: wneuper@59274: fun lev_up [] = raise PTREE "lev_up []" neuper@37906: | lev_up p = (drop_last p):pos; wneuper@59274: fun lev_on [] = raise PTREE "lev_on []" neuper@37906: | lev_on pos = neuper@37906: let val len = length pos neuper@37906: in (drop_last pos) @ [(nth len pos)+1] end; wneuper@59274: fun lev_onFrm (p,_) = (lev_on p,Frm):pos' neuper@37906: | lev_onFrm p = raise PTREE ("*** lev_onFrm: pos'="^(pos'2str p)); neuper@42427: (*040216: for inform --> embed_deriv: remains on same level TODO.WN120517 compare lev_pred*) wneuper@59274: fun lev_back' ([],_) = raise PTREE "lev_back': called by ([],_)" neuper@42427: | lev_back' (p,_) = neuper@37906: if last_elem p <= 1 then (p, Frm):pos' neuper@37906: else ((drop_last p) @ [(nth (length p) p) - 1], Res); neuper@37906: (*.increase pos by n within a level.*) neuper@37906: fun pos_plus 0 pos = pos wneuper@59274: | pos_plus n (p,Frm) = pos_plus (n-1) (p, Res) wneuper@59274: | pos_plus n (p, _) = pos_plus (n-1) (lev_on p, Res); neuper@37906: wneuper@59274: fun lev_pred [] = raise PTREE "lev_pred []" wneuper@59274: | lev_pred pos = neuper@37906: let val len = length pos wneuper@59274: in ((drop_last pos) @ [(nth len pos)-1]) end; neuper@37906: (*lev_pred [1,2,3]; neuper@37906: val it = [1,2,2] : pos neuper@37906: > lev_pred [1]; neuper@37906: val it = [0] : pos *) neuper@37906: neuper@37906: fun lev_dn p = p @ [0]; neuper@37906: (*> (lev_dn o lev_on) [1,2,3]; neuper@37906: val it = [1,2,4,0] : pos *) neuper@37906: (*fun lev_dn' ((p,p_):pos') = (lev_dn p, Frm):pos'; WN.3.12.03: never used*) wneuper@59274: fun lev_dnRes (p,_) = (lev_dn p, Res); neuper@37906: neuper@37906: (*4.4.00*) wneuper@59274: fun lev_up_ (p,Res) = (lev_up p,Res):pos' neuper@38031: | lev_up_ p' = error ("lev_up_: called for "^(pos'2str p')); wneuper@59274: fun lev_dn_ (p, _) = (lev_dn p, Res) wneuper@59274: fun ind (p,_) = length p; (*WN050108 deprecated in favour of lev_of*) wneuper@59274: fun lev_of (p,_) = length p; neuper@37906: neuper@37906: wneuper@59279: (** convert ctree to a string **) neuper@37906: neuper@37906: (* convert a pos from list to string *) neuper@37906: fun pr_pos ps = (space_implode "." (map string_of_int ps))^". "; neuper@37906: (* show hd origin or form only *) wneuper@59274: fun pr_short p (PblObj {origin = (ori,_,_),...}) = neuper@37906: ((pr_pos p) ^ " ----- pblobj -----\n") neuper@37929: (* ((((Syntax.string_of_term (thy2ctxt' "Isac")) o #4 o hd) ori)^" "^ neuper@37929: (((Syntax.string_of_term (thy2ctxt' "Isac")) o hd(*!?!*) o #5 o hd) ori))^ neuper@37906: "\n") *) neuper@37906: | pr_short p (PrfObj {form = form,...}) = neuper@37906: ((pr_pos p) ^ (term2str form) ^ "\n"); neuper@37906: (* neuper@37906: fun pr_cell (p:pos) (PblObj {cell = c, origin = (ori,_,_),...}) = neuper@37906: ((ints2str c) ^" "^ neuper@37929: ((((Syntax.string_of_term (thy2ctxt' "Isac")) o #4 o hd) ori)^" "^ neuper@37929: (((Syntax.string_of_term (thy2ctxt' "Isac")) o hd(*!?!*) o #5 o hd) ori))^ neuper@37906: "\n") neuper@37906: | pr_cell p (PrfObj {cell = c, form = form,...}) = neuper@37906: ((ints2str c) ^" "^ (term2str form) ^ "\n"); neuper@37906: *) neuper@37906: wneuper@59279: (* convert ctree *) wneuper@59279: fun pr_ctree f pt = neuper@37906: let neuper@37906: fun pr_pt pfn _ EmptyPtree = "" neuper@37906: | pr_pt pfn ps (Nd (b, [])) = pfn ps b neuper@37906: | pr_pt pfn ps (Nd (b, ts)) = (pfn ps b)^ wneuper@59274: (prts pfn ps 1 ts) neuper@37906: and prts pfn ps p [] = "" neuper@37906: | prts pfn ps p (t::ts) = (pr_pt pfn (ps @ [p]) t)^ neuper@37906: (prts pfn ps (p+1) ts) neuper@37906: in pr_pt f [] pt end; neuper@37906: (* neuper@37906: > fun prfn ps b = (pr_pos ps)^" "^b(*TODO*)^"\n"; neuper@55432: (*val pt = Unsynchronized.ref EmptyPtree;*) neuper@37986: > pt:=Nd("root'", neuper@37906: [Nd("xx1",[]), neuper@37906: Nd("xx2", neuper@37906: [Nd("xx2.1.",[]), neuper@37906: Nd("xx2.2.",[])]), neuper@37906: Nd("xx3",[])]); wneuper@59279: > tracing (pr_ctree prfn (!pt)); neuper@37906: *) neuper@37906: neuper@37906: wneuper@59279: (** access the branches of ctree **) neuper@37906: neuper@37906: fun ins_nth 1 e l = e::l neuper@37906: | ins_nth n e [] = raise PTREE "ins_nth n e []" neuper@37906: | ins_nth n e (l::ls) = l::(ins_nth (n-1) e ls); neuper@37906: fun repl [] _ _ = raise PTREE "repl [] _ _" neuper@37906: | repl (l::ls) 1 e = e::ls neuper@37906: | repl (l::ls) n e = l::(repl ls (n-1) e); neuper@37906: fun repl_app ls n e = neuper@37906: let val lim = 1 + length ls neuper@37906: in if n > lim then raise PTREE "repl_app: n > lim" neuper@37906: else if n = lim then ls @ [e] neuper@37906: else repl ls n e end; neuper@37906: (* neuper@37906: > repl [1,2,3] 2 22222; neuper@37906: val it = [1,22222,3] : int list neuper@37906: > repl_app [1,2,3,4] 5 5555; neuper@37906: val it = [1,2,3,4,5555] : int list neuper@37906: > repl_app [1,2,3] 2 22222; neuper@37906: val it = [1,22222,3] : int list neuper@37906: > repl_app [1] 2 22222 ; neuper@37906: val it = [1,22222] : int list neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: (*.get from obj at pos by f : ppobj -> 'a.*) wneuper@59274: fun get_obj f EmptyPtree _ = raise PTREE "get_obj f EmptyPtree" neuper@37906: | get_obj f (Nd (b, _)) [] = f b neuper@37906: | get_obj f (Nd (b, bs)) (p::ps) = neuper@37906: (* val (f, Nd (b, bs), (p::ps)) = (I, pt, p); neuper@37906: *) neuper@37906: let val _ = (nth p bs) handle _ => raise PTREE ("get_obj: pos = "^ neuper@37906: (ints2str' (p::ps))^" does not exist"); wneuper@59274: in (get_obj f (nth p bs) ps) neuper@37906: (*before WN050419: 'wrong type..' raised also if pos doesn't exist*) neuper@37906: handle _ => raise PTREE (*"get_obj: at pos = "^ neuper@37906: (ints2str' (p::ps))^" wrong type of ppobj"*) neuper@37906: ("get_obj: pos = "^ neuper@37906: (ints2str' (p::ps))^" does not exist") neuper@37906: end; neuper@37906: fun get_nd EmptyPtree _ = raise PTREE "get_nd EmptyPtree" neuper@37906: | get_nd n [] = n wneuper@59274: | get_nd (Nd (_,nds)) (pos as p :: ps) = (get_nd (nth p nds) ps) neuper@37906: handle _ => raise PTREE ("get_nd: not existent pos = "^(ints2str' pos)); neuper@37906: neuper@37906: (* for use by get_obj *) neuper@37925: fun g_cell (PblObj {cell = c,...}) = NONE neuper@37906: | g_cell (PrfObj {cell = c,...}) = c;(*WN0607 hack for quick introduction of lrd + rewrite-at (thms, calcs)*) neuper@37906: fun g_form (PrfObj {form = f,...}) = f neuper@37906: | g_form (PblObj {origin=(_,_,f),...}) = f; neuper@37906: fun g_form' (Nd (PrfObj {form = f,...}, _)) = f neuper@37906: | g_form' (Nd (PblObj {origin=(_,_,f),...}, _)) = f; neuper@37906: (* | g_form _ = raise PTREE "g_form not for PblObj";*) neuper@37906: fun g_origin (PblObj {origin = ori,...}) = ori neuper@37906: | g_origin _ = raise PTREE "g_origin not for PrfObj"; neuper@37906: fun g_fmz (PblObj {fmz = f,...}) = f neuper@37906: | g_fmz _ = raise PTREE "g_fmz not for PrfObj"; neuper@37906: fun g_spec (PblObj {spec = s,...}) = s neuper@37906: | g_spec _ = raise PTREE "g_spec not for PrfObj"; neuper@37906: fun g_pbl (PblObj {probl = p,...}) = p neuper@37906: | g_pbl _ = raise PTREE "g_pbl not for PrfObj"; neuper@37906: fun g_met (PblObj {meth = p,...}) = p neuper@37906: | g_met _ = raise PTREE "g_met not for PrfObj"; neuper@37906: fun g_domID (PblObj {spec = (d,_,_),...}) = d neuper@37906: | g_domID _ = raise PTREE "g_metID not for PrfObj"; neuper@37906: fun g_metID (PblObj {spec = (_,_,m),...}) = m neuper@37906: | g_metID _ = raise PTREE "g_metID not for PrfObj"; neuper@41989: fun g_ctxt (PblObj {ctxt, ...}) = ctxt neuper@41989: | g_ctxt _ = raise PTREE "g_ctxt not for PrfObj"; neuper@37906: fun g_env (PblObj {env,...}) = env neuper@37906: | g_env _ = raise PTREE "g_env not for PrfObj"; neuper@37906: fun g_loc (PblObj {loc = l,...}) = l neuper@37906: | g_loc (PrfObj {loc = l,...}) = l; neuper@37906: fun g_branch (PblObj {branch = b,...}) = b neuper@37906: | g_branch (PrfObj {branch = b,...}) = b; neuper@37906: fun g_tac (PblObj {spec = (d,p,m),...}) = Apply_Method m neuper@37906: | g_tac (PrfObj {tac = m,...}) = m; neuper@37906: fun g_result (PblObj {result = r,...}) = r neuper@37906: | g_result (PrfObj {result = r,...}) = r; neuper@37906: fun g_res (PblObj {result = (r,_),...}) = r neuper@37906: | g_res (PrfObj {result = (r,_),...}) = r; neuper@37906: fun g_res' (Nd (PblObj {result = (r,_),...}, _)) = r neuper@37906: | g_res' (Nd (PrfObj {result = (r,_),...}, _)) = r; neuper@37906: fun g_ostate (PblObj {ostate = r,...}) = r neuper@37906: | g_ostate (PrfObj {ostate = r,...}) = r; neuper@37906: fun g_ostate' (Nd (PblObj {ostate = r,...}, _)) = r neuper@37906: | g_ostate' (Nd (PrfObj {ostate = r,...}, _)) = r; neuper@37906: neuper@37925: fun gpt_cell (Nd (PblObj {cell = c,...},_)) = NONE neuper@37906: | gpt_cell (Nd (PrfObj {cell = c,...},_)) = c; neuper@37906: neuper@42428: (* get the formula preceeding the current position in a calculation *) neuper@42431: fun get_curr_formula (pt, pos as (p, p_)) = neuper@42428: case p_ of neuper@42428: Frm => get_obj g_form pt p neuper@42428: | Res => (fst o (get_obj g_result pt)) p neuper@42428: | _ => #3 (get_obj g_origin pt p); neuper@42428: neuper@37906: (*in CalcTree/Subproblem an 'just_created_' model is created; neuper@37906: this is filled to 'untouched' by Model/Refine_Problem*) neuper@37906: fun just_created_ (PblObj {meth, probl, spec, ...}) = neuper@37906: null meth andalso null probl andalso spec = e_spec; wneuper@59274: val e_origin = ([],e_spec,e_term); neuper@37906: wneuper@59274: fun just_created (pt, (p, _)) = neuper@37906: let val ppobj = get_obj I pt p neuper@37906: in is_pblobj ppobj andalso just_created_ ppobj end; neuper@37906: neuper@37906: (*.does the pos in the ctree exist ?.*) neuper@37906: fun existpt pos pt = can (get_obj I pt) pos; neuper@37906: (*.does the pos' in the ctree exist, ie. extra check for result in the node.*) wneuper@59274: fun existpt' (p,p_) pt = neuper@37906: if can (get_obj I pt) p neuper@37906: then case p_ of neuper@37906: Res => get_obj g_ostate pt p = Complete neuper@37906: | _ => true neuper@37906: else false; neuper@37906: neuper@37906: (*.is this position appropriate for calculating intermediate steps?.*) wneuper@59274: fun is_interpos (_, Res) = true neuper@37906: | is_interpos _ = false; neuper@37906: neuper@37906: fun last_onlev pt pos = not (existpt (lev_on pos) pt); neuper@37906: neuper@37906: wneuper@59279: (*.find the position of the next parent which is a PblObj in ctree.*) wneuper@59274: fun par_pblobj pt [] = [] neuper@37906: | par_pblobj pt p = neuper@37906: let fun par pt [] = [] neuper@37906: | par pt p = if is_pblobj (get_obj I pt p) then p neuper@37906: else par pt (lev_up p) neuper@37906: in par pt (lev_up p) end; neuper@37906: (* lev_up for hard_gen operating with pos = [...,0] *) neuper@37906: neuper@37906: (*.find the position and the children of the next parent which is a PblObj.*) wneuper@59274: fun par_children (Nd (PblObj _, children)) [] = (children, []) neuper@37906: | par_children (pt as Nd (PblObj _, children)) p = neuper@37906: let fun par [] = (children, []) neuper@37906: | par p = let val Nd (obj, children) = get_nd pt p neuper@37906: in if is_pblobj obj then (children, p) else par (lev_up p) neuper@37906: end; neuper@37906: in par (lev_up p) end; neuper@37906: wneuper@59279: (*.get the children of a node in ctree.*) neuper@37906: fun children (Nd (PblObj _, cn)) = cn neuper@37906: | children (Nd (PrfObj _, cn)) = cn; neuper@37906: neuper@37906: neuper@37906: (*.find the next parent, which is either a PblObj (return true) neuper@37906: or a PrfObj with tac = Detail_Set (return false).*) neuper@37906: (*FIXME.3.4.03:re-organize par_pbl_det after rls' --> rls*) wneuper@59274: fun par_pbl_det pt [] = (true, [], Erls) neuper@37906: | par_pbl_det pt p = neuper@37906: let fun par pt [] = (true, [], Erls) neuper@37906: | par pt p = if is_pblobj (get_obj I pt p) then (true, p, Erls) neuper@37906: else case get_obj g_tac pt p of neuper@37906: (*Detail_Set rls' => (false, p, assoc_rls rls') neuper@37906: (*^^^--- before 040206 after ---vvv*) neuper@37906: |*)Rewrite_Set rls' => (false, p, assoc_rls rls') neuper@37906: | Rewrite_Set_Inst (_, rls') => neuper@37906: (false, p, assoc_rls rls') neuper@37906: | _ => par pt (lev_up p) neuper@37906: in par pt (lev_up p) end; neuper@37906: neuper@37906: neuper@37906: neuper@37906: wneuper@59279: (*.get from the whole ctree by f : ppobj -> 'a.*) neuper@37906: fun get_all f EmptyPtree = [] neuper@37906: | get_all f (Nd (b, [])) = [f b] neuper@37906: | get_all f (Nd (b, bs)) = [f b] @ (get_alls f bs) neuper@37906: and get_alls f [] = [] neuper@37906: | get_alls f pts = flat (map (get_all f) pts); neuper@37906: neuper@37906: wneuper@59279: (*.insert obj b into ctree at pos, ev.overwriting this pos. neuper@41931: covers library.ML TODO.WN110315 rename*) wneuper@59274: fun insert_pt b EmptyPtree [] = Nd (b, []) neuper@52111: | insert_pt b EmptyPtree _ = raise PTREE "insert_pt b Empty _" neuper@52111: | insert_pt b (Nd ( _, _)) [] = raise PTREE "insert_pt b _ []" neuper@52111: | insert_pt b (Nd (b', bs)) (p::[]) = neuper@37906: Nd (b', repl_app bs p (Nd (b,[]))) neuper@52111: | insert_pt b (Nd (b', bs)) (p::ps) = neuper@52111: Nd (b', repl_app bs p (insert_pt b (nth p bs) ps)); neuper@37906: (* neuper@37906: > type ppobj = string; wneuper@59279: > tracing (pr_ctree prfn (!pt)); neuper@55432: (*val pt = Unsynchronized.ref Empty;*) neuper@52111: pt:= insert_pt ("root'":ppobj) EmptyPtree []; neuper@52111: pt:= insert_pt ("xx1":ppobj) (!pt) [1]; neuper@52111: pt:= insert_pt ("xx2":ppobj) (!pt) [2]; neuper@52111: pt:= insert_pt ("xx3":ppobj) (!pt) [3]; neuper@52111: pt:= insert_pt ("xx2.1":ppobj) (!pt) [2,1]; neuper@52111: pt:= insert_pt ("xx2.2":ppobj) (!pt) [2,2]; neuper@52111: pt:= insert_pt ("xx2.1.1":ppobj) (!pt) [2,1,1]; neuper@52111: pt:= insert_pt ("xx2.1.2":ppobj) (!pt) [2,1,2]; neuper@52111: pt:= insert_pt ("xx2.1.3":ppobj) (!pt) [2,1,3]; neuper@37906: *) neuper@37906: neuper@37906: (*.insert children to a node without children.*) neuper@52111: (*compare: fun insert_pt*) wneuper@59274: fun ins_chn _ EmptyPtree _ = raise PTREE "ins_chn: EmptyPtree" neuper@37906: | ins_chn ns (Nd _) [] = raise PTREE "ins_chn: pos = []" neuper@37906: | ins_chn ns (Nd (b, bs)) (p::[]) = neuper@37906: if p > length bs then raise PTREE "ins_chn: pos not existent" neuper@37906: else let val Nd (b', bs') = nth p bs neuper@37906: in if null bs' then Nd (b, repl_app bs p (Nd (b', ns))) neuper@37906: else raise PTREE "ins_chn: pos mustNOT be overwritten" end neuper@37906: | ins_chn ns (Nd (b, bs)) (p::ps) = neuper@37906: Nd (b, repl_app bs p (ins_chn ns (nth p bs) ps)); neuper@37906: neuper@52111: (* print_depth 11;ins_chn;print_depth 3; ###insert_pt#########################*); neuper@37906: neuper@37906: neuper@37906: (** apply f to obj at pos, f: ppobj -> ppobj **) neuper@37906: neuper@37906: fun appl_to_node f (Nd (b,bs)) = Nd (f b, bs); neuper@37906: fun appl_obj f EmptyPtree [] = EmptyPtree neuper@37906: | appl_obj f EmptyPtree _ = raise PTREE "appl_obj f Empty _" neuper@37906: | appl_obj f (Nd (b, bs)) [] = Nd (f b, bs) neuper@37906: | appl_obj f (Nd (b, bs)) (p::[]) = neuper@37906: Nd (b, repl_app bs p (((appl_to_node f) o (nth p)) bs)) neuper@37906: | appl_obj f (Nd (b, bs)) (p::ps) = neuper@37906: Nd (b, repl_app bs p (appl_obj f (nth p bs) (ps:pos))); neuper@37906: neuper@37906: (* for use by appl_obj *) neuper@37906: fun repl_form f (PrfObj {cell=c,form= _,tac=tac,loc=loc, neuper@37906: branch=branch,result=result,ostate=ostate}) = neuper@37906: PrfObj {cell=c,form= f,tac=tac,loc=loc, neuper@37906: branch=branch,result=result,ostate=ostate} neuper@37906: | repl_form _ _ = raise PTREE "repl_form takes no PblObj"; neuper@37906: fun repl_pbl x (PblObj {cell=cell,origin=origin,fmz=fmz, neuper@41988: spec=spec,probl=_,meth=meth,ctxt=ctxt,env=env,loc=loc, neuper@37906: branch=branch,result=result,ostate=ostate}) = neuper@37906: PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl= x, neuper@41988: meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate} neuper@37906: | repl_pbl _ _ = raise PTREE "repl_pbl takes no PrfObj"; neuper@37906: fun repl_met x (PblObj {cell=cell,origin=origin,fmz=fmz, neuper@41988: spec=spec,probl=probl,meth=_,ctxt=ctxt,env=env,loc=loc, neuper@37906: branch=branch,result=result,ostate=ostate}) = neuper@37906: PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl, neuper@41988: meth= x,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate} neuper@37906: | repl_met _ _ = raise PTREE "repl_pbl takes no PrfObj"; neuper@37906: neuper@37906: fun repl_spec x (PblObj {cell=cell,origin=origin,fmz=fmz, neuper@41988: spec= _,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc, neuper@37906: branch=branch,result=result,ostate=ostate}) = neuper@37906: PblObj {cell=cell,origin=origin,fmz=fmz,spec= x,probl=probl, neuper@41988: meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate} neuper@37906: | repl_spec _ _ = raise PTREE "repl_domID takes no PrfObj"; neuper@37906: fun repl_domID x (PblObj {cell=cell,origin=origin,fmz=fmz, neuper@41988: spec=(_,p,m),probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc, neuper@37906: branch=branch,result=result,ostate=ostate}) = neuper@37906: PblObj {cell=cell,origin=origin,fmz=fmz,spec=(x,p,m),probl=probl, neuper@41988: meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate} neuper@37906: | repl_domID _ _ = raise PTREE "repl_domID takes no PrfObj"; neuper@37906: fun repl_pblID x (PblObj {cell=cell,origin=origin,fmz=fmz, neuper@41988: spec=(d,_,m),probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc, neuper@37906: branch=branch,result=result,ostate=ostate}) = neuper@37906: PblObj {cell=cell,origin=origin,fmz=fmz,spec=(d,x,m),probl=probl, neuper@41988: meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate} neuper@37906: | repl_pblID _ _ = raise PTREE "repl_pblID takes no PrfObj"; neuper@37906: fun repl_metID x (PblObj {cell=cell,origin=origin,fmz=fmz, neuper@41988: spec=(d,p,_),probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc, neuper@37906: branch=branch,result=result,ostate=ostate}) = neuper@37906: PblObj {cell=cell,origin=origin,fmz=fmz,spec=(d,p,x),probl=probl, neuper@41988: meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch,result=result,ostate=ostate} neuper@37906: | repl_metID _ _ = raise PTREE "repl_metID takes no PrfObj"; neuper@37906: neuper@37906: fun repl_result l f' s (PrfObj {cell=cell,form=form,tac=tac,loc=_, neuper@37906: branch=branch,result = _ ,ostate = _}) = neuper@37906: PrfObj {cell=cell,form=form,tac=tac,loc= l, neuper@37906: branch=branch,result = f',ostate = s} neuper@37906: | repl_result l f' s (PblObj {cell=cell,origin=origin,fmz=fmz, neuper@41988: spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=_, neuper@37906: branch=branch,result= _ ,ostate= _}) = neuper@37906: PblObj {cell=cell,origin=origin,fmz=fmz, neuper@41988: spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc= l, neuper@37906: branch=branch,result= f',ostate= s}; neuper@37906: neuper@37906: fun repl_tac x (PrfObj {cell=cell,form=form,tac= _,loc=loc, neuper@37906: branch=branch,result=result,ostate=ostate}) = neuper@37906: PrfObj {cell=cell,form=form,tac= x,loc=loc, neuper@37906: branch=branch,result=result,ostate=ostate} neuper@37906: | repl_tac _ _ = raise PTREE "repl_tac takes no PblObj"; neuper@37906: neuper@37906: fun repl_branch b (PblObj {cell=cell,origin=origin,fmz=fmz, neuper@41988: spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc, neuper@37906: branch= _,result=result,ostate=ostate}) = neuper@37906: PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl, neuper@41988: meth=meth,ctxt=ctxt,env=env,loc=loc,branch= b,result=result,ostate=ostate} neuper@37906: | repl_branch b (PrfObj {cell=cell,form=form,tac=tac,loc=loc, neuper@37906: branch= _,result=result,ostate=ostate}) = neuper@37906: PrfObj {cell=cell,form=form,tac=tac,loc=loc, neuper@37906: branch= b,result=result,ostate=ostate}; neuper@37906: neuper@41989: fun repl_ctxt x neuper@41989: (PblObj {cell, origin, fmz, spec, probl, meth, neuper@41989: ctxt=_, env, loc, branch, result, ostate}) = neuper@41989: PblObj {cell=cell, origin=origin, fmz=fmz, spec=spec, probl=probl, meth=meth, neuper@41989: ctxt=x, env=env, loc=loc, branch=branch, result=result, ostate=ostate} neuper@41989: | repl_ctxt _ _ = raise PTREE "repl_env takes no PrfObj"; neuper@41989: neuper@37906: fun repl_env e neuper@41989: (PblObj {cell=cell, origin=origin, fmz=fmz, spec=spec, probl=probl, meth=meth, neuper@41989: ctxt=ctxt, env=_, loc=loc, branch=branch, result=result, ostate=ostate}) = neuper@41989: PblObj {cell=cell, origin=origin, fmz=fmz, spec=spec, probl=probl, meth=meth, neuper@41989: ctxt=ctxt, env=e, loc=loc, branch=branch, result=result, ostate=ostate} neuper@41989: | repl_env _ _ = raise PTREE "repl_env takes no PrfObj"; neuper@37906: neuper@37906: fun repl_oris oris neuper@37906: (PblObj {cell=cell,origin=(_,spe,hdf),fmz=fmz, neuper@41988: spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc, neuper@37906: branch=branch,result=result,ostate=ostate}) = neuper@37906: PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl, neuper@41988: meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch, neuper@37906: result=result,ostate=ostate} neuper@37906: | repl_oris _ _ = raise PTREE "repl_oris takes no PrfObj"; neuper@37906: fun repl_orispec spe neuper@37906: (PblObj {cell=cell,origin=(oris,_,hdf),fmz=fmz, neuper@41988: spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=env,loc=loc, neuper@37906: branch=branch,result=result,ostate=ostate}) = neuper@37906: PblObj{cell=cell,origin=(oris,spe,hdf),fmz=fmz,spec=spec,probl=probl, neuper@41988: meth=meth,ctxt=ctxt,env=env,loc=loc,branch=branch, neuper@37906: result=result,ostate=ostate} neuper@37906: | repl_orispec _ _ = raise PTREE "repl_orispec takes no PrfObj"; neuper@37906: neuper@41988: fun repl_loc l (PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth, neuper@41988: ctxt=ctxt,env=env,loc=_,branch=branch,result=result,ostate=ostate}) = neuper@41988: PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth, neuper@41988: ctxt=ctxt,env=env,loc=l,branch=branch,result=result,ostate=ostate} neuper@41983: | repl_loc l (PrfObj {cell=cell,form=form,tac=tac, neuper@41983: loc=_,branch=branch,result=result,ostate=ostate}) = neuper@41983: PrfObj {cell=cell,form=form,tac=tac, neuper@41983: loc= l,branch=branch,result=result,ostate=ostate}; neuper@37906: neuper@37906: (*WN050219 put here for interpreting code for cut_tree below...*) neuper@37906: type ocalhd = neuper@37906: bool * (*ALL itms+preconds true*) neuper@37906: pos_ * (*model belongs to Problem | Method*) neuper@37906: term * (*header: Problem... or Cas neuper@37906: FIXXXME.12.03: item! for marking syntaxerrors*) neuper@37906: itm list * (*model: given, find, relate*) neuper@37906: ((bool * term) list) *(*model: preconds*) neuper@37906: spec; (*specification*) neuper@37906: val e_ocalhd = (false, Und, e_term, [e_itm], [(false, e_term)], e_spec); neuper@37906: wneuper@59152: datatype ptform = Form of term | ModSpec of ocalhd; neuper@37906: val e_ptform = Form e_term; neuper@37906: val e_ptform' = ModSpec e_ocalhd; neuper@37906: neuper@37906: (*.applies (snd f) to the branches at a pos if ((fst f) b), wneuper@59279: f : (ppobj -> bool) * (int -> ctree list -> ctree list).*) neuper@37906: neuper@37906: fun appl_branch f EmptyPtree [] = (EmptyPtree, false) neuper@37906: | appl_branch f EmptyPtree _ = raise PTREE "appl_branch f Empty _" neuper@37906: | appl_branch f (Nd ( _, _)) [] = raise PTREE "appl_branch f _ []" neuper@37906: | appl_branch f (Nd (b, bs)) (p::[]) = wneuper@59274: if (fst f) b then (Nd (b, (snd f) p bs), true) neuper@37906: else (Nd (b, bs), false) neuper@37906: | appl_branch f (Nd (b, bs)) (p::ps) = neuper@37906: let val (b',bool) = appl_branch f (nth p bs) ps neuper@37906: in (Nd (b, repl_app bs p b'), bool) end; neuper@37906: neuper@37906: (* for cut_level; appl_branch(deprecated) *) neuper@37906: fun test_trans (PrfObj{branch = Transitive,...}) = true neuper@37906: | test_trans (PblObj{branch = Transitive,...}) = true neuper@37906: | test_trans _ = false; neuper@37906: wneuper@59274: fun is_pblobj' pt p = neuper@37906: let val ppobj = get_obj I pt p neuper@37906: in is_pblobj ppobj end; neuper@37906: wneuper@59274: fun delete_result pt p = neuper@37925: (appl_obj (repl_result (fst (get_obj g_loc pt p), NONE) neuper@37906: (e_term,[]) Incomplete) pt p); neuper@37906: neuper@37906: fun del_res (PblObj {cell, fmz, origin, spec, probl, meth, neuper@41988: ctxt, env, loc=(l1,_), branch, result, ostate}) = neuper@37906: PblObj {cell=cell,fmz=fmz,origin=origin,spec=spec,probl=probl,meth=meth, neuper@41988: ctxt=ctxt,env=env, loc=(l1,NONE), branch=branch, result=(e_term,[]), neuper@37906: ostate=Incomplete} neuper@37906: neuper@37906: | del_res (PrfObj {cell, form, tac, loc=(l1,_), branch, result, ostate}) = neuper@37925: PrfObj {cell=cell,form=form,tac=tac, loc=(l1,NONE), branch=branch, neuper@37906: result=(e_term,[]), ostate=Incomplete}; neuper@37906: neuper@42009: (*FIXME.WN0312 update_X X pos pt -> pt could be chained by o (efficiency?)*) neuper@42009: (*fun update_fmz pt pos x = appl_obj (repl_fmz x) pt pos; WN01xx *) neuper@41996: fun update_ctxt pt pos x = appl_obj (repl_ctxt x) pt pos; (*for use on PblObj, neuper@42394: otherwise use fun generate1; compare fun get_ctxt*) neuper@37906: fun update_env pt pos x = appl_obj (repl_env x) pt pos; neuper@37906: fun update_domID pt pos x = appl_obj (repl_domID x) pt pos; neuper@37906: fun update_pblID pt pos x = appl_obj (repl_pblID x) pt pos; neuper@37906: fun update_metID pt pos x = appl_obj (repl_metID x) pt pos; neuper@37906: fun update_spec pt pos x = appl_obj (repl_spec x) pt pos; neuper@37906: fun update_pbl pt pos x = appl_obj (repl_pbl x) pt pos; neuper@37906: fun update_pblppc pt pos x = appl_obj (repl_pbl x) pt pos; neuper@37906: fun update_met pt pos x = appl_obj (repl_met x) pt pos; neuper@41990: fun update_metppc pt pos x = appl_obj (repl_met x) pt pos; neuper@37906: fun update_branch pt pos x = appl_obj (repl_branch x) pt pos; neuper@41990: fun update_tac pt pos x = appl_obj (repl_tac x) pt pos; neuper@37906: fun update_oris pt pos x = appl_obj (repl_oris x) pt pos; neuper@42009: fun update_orispec pt pos x = appl_obj (repl_orispec x) pt pos; neuper@37906: neuper@42009: (*WN050305 for handling cut_tree in cappend_atomic + for testing*) neuper@42009: fun update_loc' pt pos x = appl_obj (repl_loc x) pt pos; neuper@37906: neuper@37906: (*13.8.02: options, because istate is no equalitype any more*) bonzai@41948: fun get_loc EmptyPtree _ = (e_istate, e_ctxt) neuper@37906: | get_loc pt (p,Res) = neuper@37906: (case get_obj g_loc pt p of neuper@37925: (SOME i, NONE) => i bonzai@41948: | (NONE , NONE) => (e_istate, e_ctxt) neuper@37925: | (_ , SOME i) => i) neuper@37906: | get_loc pt (p,_) = neuper@37906: (case get_obj g_loc pt p of neuper@37925: (NONE , SOME i) => i (*13.8.02 just copied from ^^^: too liberal ?*) bonzai@41948: | (NONE , NONE) => (e_istate, e_ctxt) neuper@37925: | (SOME i, _) => i); bonzai@41953: fun get_istate pt p = get_loc pt p |> #1; neuper@41990: fun get_ctxt pt (pos as (p, p_)) = neuper@41990: if member op = [Frm, Res] p_ neuper@41990: then get_loc pt pos |> #2 (*for script interpretation rely on fun get_loc*) neuper@41990: else get_obj g_ctxt pt p (*for specify phase take ctx from PblObj*) neuper@37906: e0726734@41957: fun get_assumptions_ pt p = get_ctxt pt p |> get_assumptions; neuper@37906: neuper@37906: (*pos of the formula on FE relative to the current pos, neuper@37906: which is the next writepos*) wneuper@59274: fun pre_pos [] = [] neuper@37906: | pre_pos pp = neuper@37906: let val (ps,p) = split_last pp neuper@37906: in case p of 1 => ps | n => ps @ [n-1] end; neuper@37906: neuper@37906: (*WN.20.5.03 ... but not used*) neuper@37906: fun posless [] (_::_) = true neuper@37906: | posless (_::_) [] = false neuper@37906: | posless (p::ps) (q::qs) = if p = q then posless ps qs else p < q; neuper@37906: (* posless [2,3,4] [3,4,5]; neuper@37906: true neuper@37906: > posless [2,3,4] [1,2,3]; neuper@37906: false neuper@37906: > posless [2,3] [2,3,4]; neuper@37906: true neuper@37906: > posless [2,3,4] [2,3]; neuper@37906: false neuper@37906: > posless [6] [6,5,2]; neuper@37906: true neuper@37906: +++ see Isabelle/../library.ML*) neuper@37906: neuper@37906: wneuper@59279: (**.development for extracting an 'interval' from ctree.**) neuper@37906: neuper@41990: (*WN0510 version stopped in favour of get_interval with !!!move_dn, getFormulaeFromTo neuper@37906: actually used (inefficient) version with move_dn: see modspec.sml*) neuper@37906: local neuper@37906: neuper@37906: fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*) neuper@37906: fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*) neuper@37906: fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x; neuper@37906: fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x; neuper@37906: neuper@37906: fun getnd i (b,p) q (Nd (po, nds)) = neuper@37906: (if i <= 0 then [[b]] else []) @ neuper@37906: (getnds (i-1) true (b@[hdp p], tlp p) (tlq q) neuper@37906: (take_fromto (hdp p) (hdq q) nds)) neuper@37906: neuper@37906: and getnds _ _ _ _ [] = [] (*no children*) neuper@37906: | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*) neuper@37906: neuper@37906: | getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*) neuper@37906: (getnd i ( b, p ) [99999] n1) @ neuper@37906: (getnd ~99999 (lev_on b,[0]) q n2) neuper@37906: neuper@37906: | getnds i _ (b,p) q [n1, n2] = (*intern, r-margin*) neuper@37906: (getnd i ( b,[0]) [99999] n1) @ neuper@37906: (getnd ~99999 (lev_on b,[0]) q n2) neuper@37906: neuper@37906: | getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*) neuper@37906: (getnd i ( b, p ) [99999] nd) @ neuper@37906: (getnds ~99999 false (lev_on b,[0]) q nds) neuper@37906: neuper@37906: | getnds i _ (b,p) q (nd::(nds as _::_)) = (*intern, ...*) neuper@37906: (getnd i ( b,[0]) [99999] nd) @ neuper@37906: (getnds ~99999 false (lev_on b,[0]) q nds); neuper@37906: in wneuper@59279: (*get an 'interval from to' from a ctree as 'intervals f t' of respective nodes neuper@37906: where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous) neuper@37906: (1) the 'f' are given neuper@37906: (1a) by 'from' if 'f' = the respective element of 'from' (left margin) neuper@37906: (1b) -inifinity, if 'f' > the respective element of 'from' (internal node) neuper@37906: (2) the 't' ar given neuper@37906: (2a) by 'to' if 't' = the respective element of 'to' (right margin) neuper@37906: (2b) inifinity, if 't' < the respective element of 'to (internal node)' neuper@37906: the 'f' and 't' are set by hdp,... *) neuper@37906: fun get_trace pt p q = neuper@37906: (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q))) neuper@37906: (take_fromto (hdp p) (hdq q) (children pt)); neuper@37906: end; neuper@37906: wneuper@59274: fun get_somespec (dI,pI,mI) (dI',pI',mI') = neuper@37906: let val domID = if dI = e_domID neuper@37906: then if dI' = e_domID neuper@38031: then error"pt_extract: no domID in probl,origin" neuper@37906: else dI' neuper@37906: else dI neuper@37906: val pblID = if pI = e_pblID neuper@37906: then if pI' = e_pblID neuper@38031: then error"pt_extract: no pblID in probl,origin" neuper@37906: else pI' neuper@37906: else pI neuper@37906: val metID = if mI = e_metID neuper@37906: then if pI' = e_metID neuper@38031: then error"pt_extract: no metID in probl,origin" neuper@37906: else mI' neuper@37906: else mI wneuper@59274: in (domID, pblID, metID) end; wneuper@59274: fun get_somespec' (dI,pI,mI) (dI',pI',mI') = neuper@37906: let val domID = if dI = e_domID then dI' else dI neuper@37906: val pblID = if pI = e_pblID then pI' else pI neuper@37906: val metID = if mI = e_metID then mI' else mI wneuper@59274: in (domID, pblID, metID) end; neuper@37906: wneuper@59279: (*extract a formula or model from ctree for itms2itemppc or model2xml*) neuper@37906: fun preconds2str bts = neuper@37906: (strs2str o (map (linefeed o pair2str o neuper@37906: (apsnd term2str) o neuper@37906: (apfst bool2str)))) bts; wneuper@59274: fun ocalhd2str (b, p, hdf, itms, prec, spec) = neuper@37906: "("^bool2str b^", "^pos_2str p^", "^term2str hdf^ neuper@37928: ", "^itms2str_ (thy2ctxt' "Isac") itms^ neuper@37906: ", "^preconds2str prec^", \n"^spec2str spec^" )"; neuper@37906: neuper@37906: neuper@37906: neuper@37906: fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj; neuper@37906: neuper@37906: wneuper@59279: (**.functions for the 'ctree iterator' as seen from the FE-Kernel interface.**) neuper@37906: wneuper@59279: (*move one step down into existing nodes of ctree; regard TransitiveB neuper@37906: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~################## neuper@37906: fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*) neuper@37906: (* val (Nd (c, ns), ([],p_)) = (pt, get_pos cI uI); neuper@37906: *) neuper@37906: if is_pblobj c neuper@37906: then case p_ of (*Frm => ([], Pbl) 1.12.03 neuper@37906: |*) Res => raise PTREE "move_dn: end of calculation" neuper@37906: | _ => if null ns (*go down from Pbl + Met*) neuper@37906: then raise PTREE "move_dn: solve problem not started" neuper@37906: else ([1], Frm) neuper@37906: else (case p_ of Res => raise PTREE "move_dn: end of (sub-)tree" neuper@37906: | _ => if null ns neuper@37906: then raise PTREE "move_dn: pos not existent 1" neuper@37906: else ([1], Frm)) neuper@37906: neuper@37906: (*iterate towards end of pos*) neuper@37906: (* val (P,(Nd (_, ns)),(p::(ps as (_::_)),p_)) = ([]:pos, pt, get_pos cI uI); neuper@37906: val (P,(Nd (_, ns)),(p::(ps as (_::_)),p_)) = ((P@[p]),(nth p ns),(ps, p_)); neuper@37906: *) neuper@37906: | move_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) = neuper@37906: if p > length ns then raise PTREE "move_dn: pos not existent 2" neuper@37906: else move_dn ((P@[p]): pos) (nth p ns) (ps, p_) neuper@37906: (* val (P, (Nd (c, ns)), ([p], p_)) = ((P@[p]), (nth p ns), (ps, p_)); neuper@37906: val (P, (Nd (c, ns)), ([p], p_)) = ([],pt,get_pos cI uI); neuper@37906: *) neuper@37906: | move_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*) neuper@37906: if p > length ns then raise PTREE "move_dn: pos not existent 3" neuper@37906: else if is_pblnd (nth p ns) then neuper@38015: ((*tracing("### move_dn: is_pblnd (nth p ns), P= "^ints2str' P^", \n"^ neuper@37906: "length ns= "^((string_of_int o length) ns)^ neuper@37906: ", p= "^string_of_int p^", p_= "^pos_2str p_);*) neuper@37906: case p_ of Res => if p = length ns neuper@37906: then if g_ostate c = Complete then (P, Res) neuper@37906: else raise PTREE (ints2str' P^" not complete") neuper@37906: (*FIXME here handle not-sequent-branches*) neuper@37906: else if g_branch c = TransitiveB neuper@37906: andalso (not o is_pblnd o (nth (p+1))) ns neuper@37906: then (P@[p+1], Res) neuper@37906: else (P@[p+1], if is_pblnd (nth (p+1) ns) neuper@37906: then Pbl else Frm) neuper@37906: | _ => if (null o children o (nth p)) ns (*go down from Pbl*) neuper@37906: then raise PTREE "move_dn: solve subproblem not started" neuper@37906: else (P @ [p, 1], neuper@37906: if (is_pblnd o hd o children o (nth p)) ns neuper@37906: then Pbl else Frm) neuper@37906: ) neuper@37906: (* val (P, Nd (c, ns), ([p], p_)) = ([], pt, ([1], Frm)); neuper@37906: *) neuper@37906: else case p_ of Frm => if (null o children o (nth p)) ns neuper@37906: (*then if g_ostate c = Complete then (P@[p],Res)*) neuper@37906: then if g_ostate' (nth p ns) = Complete neuper@37906: then (P@[p],Res) neuper@37906: else raise PTREE "move_dn: pos not existent 4" neuper@37906: else (P @ [p, 1], (*go down*) neuper@37906: if (is_pblnd o hd o children o (nth p)) ns neuper@37906: then Pbl else Frm) neuper@37906: | Res => if p = length ns neuper@37906: then neuper@37906: if g_ostate c = Complete then (P, Res) neuper@37906: else raise PTREE (ints2str' P^" not complete") neuper@37906: else neuper@37906: if g_branch c = TransitiveB neuper@37906: andalso (not o is_pblnd o (nth (p+1))) ns neuper@37906: then if (null o children o (nth (p+1))) ns neuper@37906: then (P@[p+1], Res) neuper@37906: else (P@[p+1,1], Frm)(*040221*) neuper@37906: else (P@[p+1], if is_pblnd (nth (p+1) ns) neuper@37906: then Pbl else Frm); neuper@37906: *) wneuper@59279: (*.move one step down into existing nodes of ctree; skip Res = Frm.nxt; neuper@37906: move_dn at the end of the calc-tree raises PTREE.*) neuper@37906: fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*) neuper@37906: (case p_ of neuper@37906: Res => raise PTREE "move_dn: end of calculation" neuper@37906: | _ => if null ns (*go down from Pbl + Met*) neuper@37906: then raise PTREE "move_dn: solve problem not started" neuper@37906: else ([1], Frm)) neuper@37906: | move_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) =(*iterate to end of pos*) neuper@37906: if p > length ns then raise PTREE "move_dn: pos not existent 2" wneuper@59274: else move_dn (P@[p]) (nth p ns) (ps, p_) neuper@37906: neuper@37906: | move_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*) neuper@37906: if p > length ns then raise PTREE "move_dn: pos not existent 3" neuper@37906: else case p_ of neuper@37906: Res => neuper@37906: if p = length ns (*last Res on this level: go a level up*) neuper@37906: then if g_ostate c = Complete then (P, Res) neuper@37906: else raise PTREE (ints2str' P^" not complete 1") neuper@37906: else (*go to the next Nd on this level, or down into the next Nd*) neuper@37906: if is_pblnd (nth (p+1) ns) then (P@[p+1], Pbl) neuper@37906: else neuper@37906: if g_res' (nth p ns) = g_form' (nth (p+1) ns) neuper@37906: then if (null o children o (nth (p+1))) ns neuper@37906: then (*take the Res if Complete*) neuper@37906: if g_ostate' (nth (p+1) ns) = Complete neuper@37906: then (P@[p+1], Res) neuper@37906: else raise PTREE (ints2str' (P@[p+1])^ neuper@37906: " not complete 2") neuper@37906: else (P@[p+1,1], Frm)(*go down into the next PrfObj*) neuper@37906: else (P@[p+1], Frm)(*take Frm: exists if the Nd exists*) neuper@37906: | Frm => (*go down or to the Res of this Nd*) neuper@37906: if (null o children o (nth p)) ns neuper@37906: then if g_ostate' (nth p ns) = Complete then (P @ [p], Res) neuper@37906: else raise PTREE (ints2str' (P @ [p])^" not complete 3") neuper@37906: else (P @ [p, 1], Frm) neuper@37906: | _ => (*is Pbl or Met*) neuper@37906: if (null o children o (nth p)) ns neuper@37906: then raise PTREE "move_dn:solve subproblem not startd" neuper@37906: else (P @ [p, 1], neuper@37906: if (is_pblnd o hd o children o (nth p)) ns neuper@37906: then Pbl else Frm); neuper@37906: neuper@37906: wneuper@59279: (*.go one level down into ctree.*) neuper@37906: fun movelevel_dn [] (Nd (c, ns)) ([],p_) = (*root problem*) neuper@37906: if is_pblobj c neuper@37906: then if null ns neuper@37906: then raise PTREE "solve problem not started" neuper@37906: else ([1], if (is_pblnd o hd) ns then Pbl else Frm) neuper@37906: else raise PTREE "pos not existent 1" neuper@37906: neuper@37906: (*iterate towards end of pos*) neuper@37906: | movelevel_dn P (Nd (_, ns)) (p::(ps as (_::_)),p_) = neuper@37906: if p > length ns then raise PTREE "pos not existent 2" neuper@37906: else movelevel_dn (P@[p]) (nth p ns) (ps, p_) neuper@37906: neuper@37906: | movelevel_dn P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*) neuper@37906: if p > length ns then raise PTREE "pos not existent 3" else neuper@37906: case p_ of Res => neuper@37906: if p = length ns neuper@37906: then raise PTREE "no children" neuper@37906: else neuper@37906: if g_branch c = TransitiveB neuper@37906: then if (null o children o (nth (p+1))) ns neuper@37906: then raise PTREE "no children" neuper@37906: else (P @ [p+1, 1], neuper@37906: if (is_pblnd o hd o children o (nth (p+1))) ns neuper@37906: then Pbl else Frm) neuper@37906: else if (null o children o (nth p)) ns neuper@37906: then raise PTREE "no children" neuper@37906: else (P @ [p, 1], if (is_pblnd o hd o children o (nth p)) ns neuper@37906: then Pbl else Frm) neuper@37906: | _ => if (null o children o (nth p)) ns neuper@37906: then raise PTREE "no children" neuper@37906: else (P @ [p, 1], (*go down*) neuper@37906: if (is_pblnd o hd o children o (nth p)) ns neuper@37906: then Pbl else Frm); neuper@37906: neuper@37906: neuper@37906: wneuper@59279: (*.go to the previous position in ctree; regard TransitiveB.*) wneuper@59274: fun move_up _ (Nd (c, ns)) ([],p_) = (*root problem*) neuper@37906: if is_pblobj c neuper@37906: then case p_ of Res => if null ns then ([], Pbl) (*Res -> Pbl (not Met)!*) neuper@37906: else ([length ns], Res) neuper@37906: | _ => raise PTREE "begin of calculation" neuper@37906: else raise PTREE "pos not existent" neuper@37906: neuper@37906: | move_up P (Nd (_, ns)) (p::(ps as (_::_)),p_) = (*iterate to end of pos*) neuper@37906: if p > length ns then raise PTREE "pos not existent" neuper@37906: else move_up (P@[p]) (nth p ns) (ps,p_) neuper@37906: neuper@37906: | move_up P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*) neuper@37906: if p > length ns then raise PTREE "pos not existent" neuper@37906: else if is_pblnd (nth p ns) then neuper@37906: case p_ of Res => neuper@37906: let val nc = (length o children o (nth p)) ns neuper@37906: in if nc = 0 then (P@[p], Pbl) (*Res -> Pbl (not Met)!*) neuper@37906: else (P @ [p, nc], Res) end (*go down*) neuper@37906: | _ => if p = 1 then (P, Pbl) else (P@[p-1], Res) neuper@37906: else case p_ of Frm => if p <> 1 then (P, Frm) neuper@37906: else if is_pblobj c then (P, Pbl) else (P, Frm) neuper@37906: | Res => neuper@37906: let val nc = (length o children o (nth p)) ns neuper@37906: in if nc = 0 (*cannot go down*) neuper@37906: then if g_branch c = TransitiveB andalso p <> 1 neuper@37906: then (P@[p-1], Res) else (P@[p], Frm) neuper@37906: else (P @ [p, nc], Res) end; (*go down*) neuper@37906: neuper@37906: neuper@37906: wneuper@59279: (*.go one level up in ctree; sets the position on Frm.*) neuper@37906: fun movelevel_up _ (Nd (c, ns)) (([],p_):pos') = (*root problem*) neuper@37906: raise PTREE "pos not existent" neuper@37906: neuper@37906: (*iterate towards end of pos*) neuper@37906: | movelevel_up P (Nd (_, ns)) (p::(ps as (_::_)),p_) = neuper@37906: if p > length ns then raise PTREE "pos not existent" neuper@37906: else movelevel_up (P@[p]) (nth p ns) (ps,p_) neuper@37906: neuper@37906: | movelevel_up P (Nd (c, ns)) ([p], p_) = (*act on last element of pos*) neuper@37906: if p > length ns then raise PTREE "pos not existent" neuper@37906: else if is_pblobj c then (P, Pbl) else (P, Frm); neuper@37906: neuper@37906: neuper@37906: (*.go to the next calc-head up in the calc-tree.*) neuper@37906: fun movecalchd_up pt ((p, Res):pos') = neuper@37906: (par_pblobj pt p, Pbl):pos' neuper@37906: | movecalchd_up pt (p, _) = neuper@37906: if is_pblobj (get_obj I pt p) neuper@37906: then (p, Pbl) else (par_pblobj pt p, Pbl); neuper@37906: neuper@37906: (*.determine the previous pos' on the same level.*) neuper@42427: (*WN0502 made for interSteps; _only_ works for branch TransitiveB WN120517 compare lev_back*) neuper@37906: fun lev_pred' pt (pos:pos' as ([],Res)) = ([],Pbl):pos' neuper@37906: | lev_pred' pt (pos:pos' as (p, Res)) = neuper@37906: let val (p', last) = split_last p neuper@37906: in if last = 1 neuper@37906: then if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm) neuper@37906: else if get_obj g_res pt (p' @ [last - 1]) = get_obj g_form pt p neuper@37906: then (p' @ [last - 1], Res) (*TransitiveB*) neuper@37906: else if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm) neuper@37906: end; neuper@37906: neuper@42427: neuper@37906: (*.determine the next pos' on the same level.*) neuper@37906: fun lev_on' pt (([],Pbl):pos') = ([],Res):pos' neuper@37906: | lev_on' pt (p, Res) = neuper@37906: if get_obj g_res pt p = get_obj g_form pt (lev_on p)(*TransitiveB*) neuper@37906: then if existpt' (lev_on p, Res) pt then (lev_on p, Res) neuper@38031: else error ("lev_on': (p, Res) -> (p, Res) not existent, \ neuper@37906: \p = "^ints2str' (lev_on p)) neuper@37906: else (lev_on p, Frm) neuper@37906: | lev_on' pt (p, _) = neuper@37906: if existpt' (p, Res) pt then (p, Res) neuper@38031: else error ("lev_on': (p, Frm) -> (p, Res) not existent, \ neuper@37906: \p = "^ints2str' p); neuper@37906: neuper@37906: fun exist_lev_on' pt p = (lev_on' pt p; true) handle _ => false; neuper@37906: neuper@37906: (*.is the pos' at the last element of a calulation _AND_ can be continued.*) neuper@37906: (* val (pt, pos as (p,p_)) = (pt, ([1],Frm)); neuper@37906: *) neuper@37906: fun is_curr_endof_calc pt (([],Res) : pos') = false neuper@37906: | is_curr_endof_calc pt (pos as (p,_)) = neuper@37906: not (exist_lev_on' pt pos) neuper@37906: andalso get_obj g_ostate pt (lev_up p) = Incomplete; neuper@37906: neuper@37906: neuper@37906: (**.insert into ctree and cut branches accordingly.**) neuper@37906: neuper@37906: (*.get all positions of certain intervals on the ctree.*) neuper@37906: (*OLD VERSION without move_dn; kept for occasional redesign wneuper@59279: get all pos's to be cut in a ctree wneuper@59279: below a pos or from a ctree list after i-th element (NO level_up).*) neuper@37906: fun get_allpos' (_:pos, _:posel) EmptyPtree = ([]:pos' list) neuper@37906: | get_allpos' (p, 1) (Nd (b, bs)) = (*p is pos of Nd*) neuper@37906: if g_ostate b = Incomplete neuper@38015: then ((*tracing("get_allpos' (p, 1) Incomplete: p="^ints2str' p);*) neuper@37906: [(p,Frm)] @ (get_allpos's (p, 1) bs) neuper@37906: ) neuper@38015: else ((*tracing("get_allpos' (p, 1) else: p="^ints2str' p);*) neuper@37906: [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p,Res)] neuper@37906: ) neuper@37906: (*WN041020 here we assume what is presented on the worksheet ?!*) neuper@37906: | get_allpos' (p, i) (Nd (b, bs)) = (*p is pos of Nd*) neuper@37906: if length bs > 0 orelse is_pblobj b neuper@37906: then if g_ostate b = Incomplete neuper@37906: then [(p,Frm)] @ (get_allpos's (p, 1) bs) neuper@37906: else [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p,Res)] neuper@37906: else neuper@37906: if g_ostate b = Incomplete neuper@37906: then [] neuper@37906: else [(p,Res)] neuper@37906: (*WN041020 here we assume what is presented on the worksheet ?!*) neuper@37906: and get_allpos's _ [] = [] neuper@37906: | get_allpos's (p, i) (pt::pts) = (*p is pos of parent-Nd*) neuper@37906: (get_allpos' (p@[i], i) pt) @ (get_allpos's (p, i+1) pts); neuper@37906: neuper@37906: (*.get all positions of certain intervals on the ctree.*) neuper@37906: (*NEW version WN050225*) neuper@37906: neuper@37906: neuper@37906: (*.cut branches.*) neuper@37906: (*before WN041019...... neuper@37906: val cut_branch = (test_trans, curry take): wneuper@59279: (ppobj -> bool) * (int -> ctree list -> ctree list); neuper@37906: .. formlery used for ... neuper@37906: fun cut_tree''' _ [] = EmptyPtree neuper@37906: | cut_tree''' pt pos = neuper@37906: let val (pt',cut) = appl_branch cut_branch pt pos neuper@37906: in if cut andalso length pos > 1 then cut_tree''' pt' (lev_up pos) neuper@37906: else pt' end; neuper@37906: *) neuper@37906: (*OLD version before WN050225*) neuper@37906: (*WN050106 like cut_level, but deletes exactly 1 node --- for tests ONLY*) neuper@37906: fun cut_level_'_ (_:pos' list) (_:pos) EmptyPtree (_:pos') = neuper@37906: raise PTREE "cut_level_'_ Empty _" neuper@37906: | cut_level_'_ _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level_'_ _ []" neuper@37906: | cut_level_'_ cuts P (Nd (b, bs)) (p::[],p_) = neuper@37906: if test_trans b neuper@37906: then (Nd (b, drop_nth [] (p:posel, bs)), neuper@37906: (* ~~~~~~~~~~~*) neuper@37906: cuts @ neuper@37906: (if p_ = Frm then [(P@[p],Res)] else ([]:pos' list)) @ neuper@37906: (*WN041020 here we assume what is presented on the worksheet ?!*) neuper@37906: (get_allpos's (P, p+1) (drop_nth [] (p, bs)))) neuper@37906: (* ~~~~~~~~~~~*) neuper@37906: else (Nd (b, bs), cuts) neuper@37906: | cut_level_'_ cuts P (Nd (b, bs)) ((p::ps),p_) = neuper@37906: let val (bs',cuts') = cut_level_'_ cuts P (nth p bs) (ps, p_) neuper@37906: in (Nd (b, repl_app bs p bs'), cuts @ cuts') end; neuper@37906: neuper@37906: (*before WN050219*) neuper@37906: fun cut_level (_:pos' list) (_:pos) EmptyPtree (_:pos') = neuper@37906: raise PTREE "cut_level EmptyPtree _" neuper@37906: | cut_level _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level _ []" neuper@37906: neuper@37906: | cut_level cuts P (Nd (b, bs)) (p::[],p_) = neuper@37906: if test_trans b neuper@37906: then (Nd (b, take (p:posel, bs)), neuper@37906: cuts @ neuper@37906: (if p_ = Frm andalso (*#*) g_ostate b = Complete neuper@37906: then [(P@[p],Res)] else ([]:pos' list)) @ neuper@37906: (*WN041020 here we assume what is presented on the worksheet ?!*) neuper@37906: (get_allpos's (P, p+1) (takerest (p, bs)))) neuper@37906: else (Nd (b, bs), cuts) neuper@37906: neuper@37906: | cut_level cuts P (Nd (b, bs)) ((p::ps),p_) = neuper@37906: let val (bs',cuts') = cut_level cuts P (nth p bs) (ps, p_) neuper@37906: in (Nd (b, repl_app bs p bs'), cuts @ cuts') end; neuper@37906: neuper@37906: (*OLD version before WN050219, overwritten below*) neuper@37906: fun cut_tree _ (([],_):pos') = raise PTREE "cut_tree _ ([],_)" neuper@37906: | cut_tree pt (pos as ([p],_)) = neuper@37906: let val (pt', cuts) = cut_level ([]:pos' list) [] pt pos neuper@37906: in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete neuper@37906: then [] else [([],Res)])) end neuper@37906: | cut_tree pt (p,p_) = neuper@37906: let neuper@37906: fun cutfn pt cuts (p,p_) = neuper@37906: let val (pt', cuts') = cut_level [] (lev_up p) pt (p,p_) neuper@37906: val cuts'' = if get_obj g_ostate pt (lev_up p) = Incomplete neuper@37906: then [] else [(lev_up p, Res)] neuper@37906: in if length cuts' > 0 andalso length p > 1 neuper@37906: then cutfn pt' (cuts @ cuts') (lev_up p, Frm(*-->(p,Res)*)) neuper@37906: else (pt',cuts @ cuts') end neuper@37906: val (pt', cuts) = cutfn pt [] (p,p_) neuper@37906: in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete neuper@37906: then [] else [([], Res)])) end; neuper@37906: neuper@37906: neuper@37906: (*########/ inserted from ctreeNEW.sml \#################################**) neuper@37906: wneuper@59279: (*.get all positions in a ctree until ([],Res) or ostate=Incomplete neuper@37906: val get_allp = fn : neuper@37906: pos' list -> : accumulated, start with [] neuper@37906: pos -> : the offset for subtrees wrt the root wneuper@59279: ctree -> : (sub)tree neuper@37906: pos' : initialization (the last pos' before ...) neuper@37906: -> pos' list : of positions in this (sub) tree (relative to the root) neuper@37906: .*) neuper@37906: (* val (cuts, P, pt, pos) = ([], [3], get_nd pt [3], ([], Frm):pos'); neuper@37906: val (cuts, P, pt, pos) = ([], [2], get_nd pt [2], ([], Frm):pos'); neuper@37906: length (children pt); neuper@37906: *) neuper@37906: fun get_allp (cuts:pos' list) (P:pos, pos:pos') pt = neuper@37906: (let val nxt = move_dn [] pt pos (*exn if Incomplete reached*) neuper@37906: in if nxt <> ([],Res) neuper@37906: then get_allp (cuts @ [nxt]) (P, nxt) pt neuper@37906: else (map (apfst (curry op@ P)) (cuts @ [nxt])): pos' list neuper@37906: end) handle PTREE _ => (map (apfst (curry op@ P)) cuts); neuper@37906: neuper@37906: neuper@37906: (*the pts are assumed to be on the same level*) neuper@37906: fun get_allps (cuts: pos' list) (P:pos) [] = cuts neuper@37906: | get_allps cuts P (pt::pts) = neuper@37906: let val below = get_allp [] (P, ([], Frm)) pt neuper@37906: val levfrm = neuper@37906: if is_pblnd pt neuper@37906: then (P, Pbl)::below neuper@37906: else if last_elem P = 1 neuper@37906: then (P, Frm)::below neuper@37906: else (*Trans*) below neuper@37906: val levres = levfrm @ (if null below then [(P, Res)] else []) neuper@37906: in get_allps (cuts @ levres) (lev_on P) pts end; neuper@37906: neuper@37906: neuper@37906: (**.these 2 funs decide on how far cut_tree goes.**) neuper@37906: (*.shall the nodes _after_ the pos to be inserted at be deleted?.*) neuper@37906: fun test_trans (PrfObj{branch = Transitive,...}) = true neuper@37906: | test_trans (PrfObj{branch = NoBranch,...}) = true neuper@37906: | test_trans (PblObj{branch = Transitive,...}) = true neuper@37906: | test_trans (PblObj{branch = NoBranch,...}) = true neuper@37906: | test_trans _ = false; neuper@37906: (*.shall cutting be continued on the higher level(s)? neuper@37906: the Nd regarded will NOT be changed.*) neuper@37906: fun cutlevup (PblObj _) = false (*for tests of LK0502*) neuper@37906: | cutlevup _ = true; neuper@37906: val cutlevup = test_trans;(*WN060727 after summerterm tests.LK0502 withdrawn*) neuper@37906: neuper@37906: (*cut_bottom new sml603..608 neuper@37906: cut the level at the bottom of the pos (used by cappend_...) neuper@37906: and handle the parent in order to avoid extra case for root wneuper@59279: fn: ctree -> : the _whole_ ctree for cut_levup neuper@37906: pos * posel -> : the pos after split_last wneuper@59279: ctree -> : the parent of the Nd to be cut neuper@37906: return wneuper@59279: (ctree * : the updated ctree neuper@37906: pos' list) * : the pos's cut neuper@37906: bool : cutting shall be continued on the higher level(s) neuper@37906: *) neuper@37906: fun cut_bottom _ (pt' as Nd (b, [])) = ((pt', []), cutlevup b) neuper@37906: | cut_bottom (P:pos, p:posel) (Nd (b, bs)) = neuper@37906: let (*divide level into 3 parts...*) neuper@37906: val keep = take (p - 1, bs) neuper@37906: val pt' as Nd (_,bs') = nth p bs neuper@52111: (*^^^^^_here_ will be 'insert_pt'ed by 'append_..'*) neuper@37906: val (tail, tp) = (takerest (p, bs), neuper@37906: if null (takerest (p, bs)) then 0 else p + 1) neuper@37906: val (children, cuts) = neuper@37906: if test_trans b neuper@37906: then (keep, neuper@37906: (if is_pblnd pt' then [(P @ [p], Pbl)] else []) neuper@37906: @ (get_allp [] (P @ [p], (P, Frm)) pt') neuper@37906: @ (get_allps [] (P @ [p+1]) tail)) neuper@52111: else (keep @ [(*'insert_pt'ed by 'append_..'*)] @ tail, neuper@37906: get_allp [] (P @ [p], (P, Frm)) pt') neuper@37906: val (pt'', cuts) = neuper@37906: if cutlevup b neuper@37906: then (Nd (del_res b, children), neuper@37906: cuts @ (if g_ostate b = Incomplete then [] else [(P,Res)])) neuper@37906: else (Nd (b, children), cuts) neuper@38015: (*val _= tracing("####cut_bottom (P, p)="^pos2str (P @ [p])^ neuper@37906: ", Nd=.............................................") neuper@37906: val _= show_pt pt'' neuper@38015: val _= tracing("####cut_bottom form='"^ neuper@37906: term2str (get_obj g_form pt'' [])) neuper@38015: val _= tracing("####cut_bottom cuts#="^string_of_int (length cuts)^ neuper@37906: ", cuts="^pos's2str cuts)*) neuper@37906: in ((pt'', cuts:pos' list), cutlevup b) end; neuper@37906: neuper@37906: neuper@37906: (*.go all levels from the bottom of 'pos' up to the root, neuper@37906: on each level compose the children of a node and accumulate the cut Nds neuper@37906: args neuper@37906: pos' list -> : for accumulation neuper@37906: bool -> : cutting shall be continued on the higher level(s) wneuper@59279: ctree -> : the whole ctree for 'get_nd pt P' on each level wneuper@59279: ctree -> : the Nd from the lower level for insertion at path neuper@37906: pos * posel -> : pos=path split for convenience wneuper@59279: ctree -> : Nd the children of are under consideration on this call neuper@37906: returns : wneuper@59279: ctree * pos' list : the updated parent-Nd and the pos's of the Nds cut neuper@37906: .*) neuper@37906: fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:posel) (Nd (b, bs)) = neuper@37906: let (*divide level into 3 parts...*) neuper@37906: val keep = take (p - 1, bs) neuper@37906: (*val pt' comes as argument from below*) neuper@37906: val (tail, tp) = (takerest (p, bs), neuper@37906: if null (takerest (p, bs)) then 0 else p + 1) neuper@37906: val (children, cuts') = neuper@37906: if clevup neuper@37906: then (keep @ [pt'], get_allps [] (P @ [p+1]) tail) neuper@37906: else (keep @ [pt'] @ tail, []) neuper@37906: val clevup' = if clevup then cutlevup b else false neuper@37906: (*the first Nd with false stops cutting on all levels above*) neuper@37906: val (pt'', cuts') = neuper@37906: if clevup' neuper@37906: then (Nd (del_res b, children), neuper@37906: cuts' @ (if g_ostate b = Incomplete then [] else [(P,Res)])) neuper@37906: else (Nd (b, children), cuts') neuper@38015: (*val _= tracing("#####cut_levup clevup= "^bool2str clevup) neuper@38015: val _= tracing("#####cut_levup cutlevup b= "^bool2str (cutlevup b)) neuper@38015: val _= tracing("#####cut_levup (P, p)="^pos2str (P @ [p])^ neuper@37906: ", Nd=.............................................") neuper@37906: val _= show_pt pt'' neuper@38015: val _= tracing("#####cut_levup form='"^ neuper@37906: term2str (get_obj g_form pt'' [])) neuper@38015: val _= tracing("#####cut_levup cuts#="^string_of_int (length cuts)^ neuper@37906: ", cuts="^pos's2str cuts)*) neuper@37906: in if null P then (pt'', (cuts @ cuts'):pos' list) neuper@37906: else let val (P, p) = split_last P neuper@37906: in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P) neuper@37906: end neuper@37906: end; neuper@37906: neuper@37906: (*.cut nodes after and below an inserted node in the ctree; neuper@37906: the cuts range is limited by the predicate 'fun cutlevup'.*) neuper@37906: fun cut_tree pt (pos,_) = neuper@37906: if not (existpt pos pt) neuper@37906: then (pt,[]) (*appending a formula never cuts anything*) neuper@37906: else let val (P, p) = split_last pos neuper@37906: val ((pt', cuts), clevup) = cut_bottom (P, p) (get_nd pt P) neuper@37906: (* pt' is the updated parent of the Nd to cappend_..*) neuper@37906: in if null P then (pt', cuts) neuper@37906: else let val (P, p) = split_last P neuper@37906: in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P) neuper@37906: end neuper@37906: end; neuper@37906: neuper@37906: fun append_atomic p l f r f' s pt = neuper@38015: let (**val _= tracing("#@append_atomic: pos ="^pos2str p)**) wneuper@59253: val (iss, f) = if existpt p pt andalso is_empty_tac (get_obj g_tac pt p) neuper@37906: then (*after Take*) neuper@37925: ((fst (get_obj g_loc pt p), SOME l), neuper@37906: get_obj g_form pt p) neuper@37925: else ((NONE, SOME l), f) neuper@52111: in insert_pt (PrfObj {cell = NONE, neuper@37906: form = f, neuper@37906: tac = r, neuper@37906: loc = iss, neuper@37906: branch= NoBranch, neuper@37906: result= f', neuper@37906: ostate= s}) pt p end; neuper@37906: neuper@37906: neuper@37906: (*20.8.02: cappend_* FIXXXXME cut branches below cannot be decided here: neuper@37906: detail - generate - cappend: inserted, not appended !!! neuper@37906: neuper@37906: cut decided in applicable_in !?! neuper@37906: *) neuper@37906: fun cappend_atomic pt p loc f r f' s = neuper@37906: (* val (pt, p, loc, f, r, f', s) = neuper@37906: (pt,p,l,f,Rewrite_Set_Inst (subst2subs subs',id_rls rls'), neuper@37906: (f',asm),Complete); neuper@37906: *) neuper@38015: ((*tracing("##@cappend_atomic: pos ="^pos2str p);*) neuper@37906: apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm)) neuper@37906: ); neuper@37906: (*TODO.WN050305 redesign the handling of istates*) neuper@37906: fun cappend_atomic pt p ist_res f r f' s = wneuper@59253: if existpt p pt andalso is_empty_tac (get_obj g_tac pt p) neuper@41994: then (*after Take: transfer Frm and respective istate*) neuper@41994: let neuper@41994: val (ist_form, f) = neuper@41994: (get_loc pt (p,Frm), get_obj g_form pt p) neuper@41994: val (pt, cs) = cut_tree pt (p,Frm) neuper@41994: val pt = append_atomic p (e_istate, e_ctxt) f r f' s pt neuper@41994: val pt = update_loc' pt p (SOME ist_form, SOME ist_res) neuper@41994: in (pt, cs) end neuper@41994: else apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm)); neuper@37906: neuper@37906: (* called by Take *) neuper@37906: fun append_form p l f pt = neuper@38015: ((*tracing("##@append_form: pos ="^pos2str p);*) neuper@52111: insert_pt (PrfObj {cell = NONE, neuper@37906: form = (*if existpt p pt neuper@37906: andalso get_obj g_tac pt p = Empty_Tac neuper@37906: (*distinction from 'old' (+complete!) pobjs*) neuper@37906: then get_obj g_form pt p else*) f, neuper@37906: tac = Empty_Tac, neuper@37925: loc = (SOME l, NONE), neuper@37906: branch= NoBranch, neuper@37906: result= (e_term,[]), neuper@37906: ostate= Incomplete}) pt p neuper@37906: ); neuper@37906: (* val (p,loc,f) = ([1], e_istate, str2term "x + 1 = 2"); neuper@37906: val (p,loc,f) = (fst p, e_istate, str2term "-1 + x = 0"); neuper@37906: *) neuper@37906: fun cappend_form pt p loc f = neuper@38015: ((*tracing("##@cappend_form: pos ="^pos2str p);*) neuper@37906: apfst (append_form p loc f) (cut_tree pt (p,Frm)) neuper@37906: ); neuper@37906: fun cappend_form pt p loc f = neuper@38015: let (*val _= tracing("##@cappend_form: pos ="^pos2str p) neuper@38015: val _= tracing("##@cappend_form before cut_tree: loc ="^istate2str loc)*) neuper@37906: val (pt', cs) = cut_tree pt (p,Frm) neuper@37906: val pt'' = append_form p loc f pt' neuper@38015: (*val _= tracing("##@cappend_form after append: loc ="^ neuper@37906: istates2str (get_obj g_loc pt'' p))*) neuper@37906: in (pt'', cs) end; neuper@37906: neuper@37906: neuper@37906: neuper@37906: fun append_result pt p l f s = wneuper@59274: (appl_obj (repl_result (fst (get_obj g_loc pt p), SOME l) f s) pt p, []); neuper@37906: neuper@37906: neuper@37906: (*WN041022 deprecated, still for kbtest/diffapp.sml, /systest/root-equ.sml*) neuper@37906: fun append_parent p l f r b pt = neuper@38015: let (*val _= tracing("###append_parent: pos ="^pos2str p);*) wneuper@59253: val (ll,f) = if existpt p pt andalso is_empty_tac (get_obj g_tac pt p) neuper@37925: then ((fst (get_obj g_loc pt p), SOME l), neuper@37906: get_obj g_form pt p) neuper@37925: else ((SOME l, NONE), f) neuper@52111: in insert_pt (PrfObj neuper@37925: {cell = NONE, neuper@37906: form = f, neuper@37906: tac = r, neuper@37906: loc = ll, neuper@37906: branch= b, neuper@37906: result= (e_term,[]), neuper@37906: ostate= Incomplete}) pt p end; neuper@37906: fun cappend_parent pt p loc f r b = neuper@38015: ((*tracing("###cappend_parent: pos ="^pos2str p);*) neuper@37906: apfst (append_parent p loc f r b) (cut_tree pt (p,Und)) neuper@37906: ); neuper@37906: neuper@37906: neuper@37906: fun append_problem [] l fmz (strs,spec,hdf) _ = neuper@38015: ((*tracing("###append_problem: pos = []");*) neuper@37906: (Nd (PblObj neuper@37925: {cell = NONE, neuper@37906: origin= (strs,spec,hdf), neuper@37906: fmz = fmz, neuper@37906: spec = empty_spec, neuper@37906: probl = []:itm list, neuper@37906: meth = []:itm list, neuper@41988: ctxt = e_ctxt, neuper@37925: env = NONE, neuper@37925: loc = (SOME l, NONE), neuper@37906: branch= TransitiveB,(*FIXXXXXME.27.8.03: for equations only*) neuper@37906: result= (e_term,[]), neuper@37906: ostate= Incomplete},[])) neuper@37906: ) neuper@37906: | append_problem p l fmz (strs,spec,hdf) pt = neuper@38015: ((*tracing("###append_problem: pos ="^pos2str p);*) neuper@52111: insert_pt (PblObj neuper@37925: {cell = NONE, neuper@37906: origin= (strs,spec,hdf), neuper@37906: fmz = fmz, neuper@37906: spec = empty_spec, neuper@37906: probl = []:itm list, neuper@37906: meth = []:itm list, neuper@41988: ctxt = e_ctxt, neuper@37925: env = NONE, neuper@37925: loc = (SOME l, NONE), neuper@37906: branch= TransitiveB, neuper@37906: result= (e_term,[]), neuper@37906: ostate= Incomplete}) pt p neuper@37906: ); neuper@37906: fun cappend_problem _ [] loc fmz ori = neuper@38015: ((*tracing("###cappend_problem: pos = []");*) neuper@37906: (append_problem [] loc fmz ori EmptyPtree,[]) neuper@37906: ) neuper@37906: | cappend_problem pt p loc fmz ori = neuper@38015: ((*tracing("###cappend_problem: pos ="^pos2str p);*) bonzai@41948: apfst (append_problem p (loc:(istate * Proof.context)) fmz ori) (cut_tree pt (p,Frm)) neuper@37906: ); neuper@37906: neuper@37906: (*.get the theory explicitly specified for the rootpbl; neuper@37906: thus use this function _after_ finishing specification.*) neuper@41988: fun rootthy (Nd (PblObj {spec=(thyID, _, _), ...}, _)) = assoc_thy thyID neuper@38031: | rootthy _ = error "rootthy"; neuper@37906: wneuper@59275: (**) wneuper@59275: end wneuper@59275: (**) wneuper@59277: (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) wneuper@59275: open Ctree wneuper@59277: ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) wneuper@59278: wneuper@59278: (* policy for "open" structures: wneuper@59278: -------------------------------- wneuper@59278: The above "open Ctree" creates an unclear situation with structures, in particular in test/. wneuper@59278: This is work in progress, but urges to make policy explicit: wneuper@59278: wneuper@59278: (1) All structures are closed with a signature; this for prepares re-arrangement of structures. wneuper@59278: (2) Some structures are pervasive (e.g. Ctree) such, that an "open" ensures readability locally. wneuper@59278: (3) test/ is preceeded by "open" for all structures, in order to ease copy&paste from scr/ to test/ wneuper@59278: wneuper@59278: ad (1) Presently this point is under construction. wneuper@59278: ad (2) Such local "open" are kept to a minimum (with the goal to reach Isabelle's state). wneuper@59278: ad (3) See https://intra.ist.tugraz.at/hg/isa/file/2ba35efb07b7/test/Tools/isac/Test_Isac.thy#l70 wneuper@59278: *)