1.1 --- a/src/Tools/isac/Interpret/ctree.sml Thu Dec 22 11:36:20 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/ctree.sml Thu Dec 22 11:55:16 2016 +0100
1.3 @@ -284,296 +284,6 @@
1.4 val branch2str : branch -> string
1.5 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.6 end
1.7 -(*
1.8 -structure Ctree :
1.9 -sig
1.10 - val Ets : ets exception PTREE of string
1.11 - val append_atomic :
1.12 - pos -> istate * Proof.context -> term -> tac -> term * term list -> ostate -> ctree -> ctree
1.13 - val append_form : int list -> istate * Proof.context -> term -> ctree -> ctree
1.14 - val append_parent : pos -> istate * Proof.context -> term -> tac -> branch -> ctree -> ctree
1.15 - val append_problem : int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree -> ctree
1.16 - val append_result : ctree -> pos -> istate * Proof.context -> term * term list -> ostate -> ctree * 'a list
1.17 - val appl_branch : (ppobj -> bool) * (posel -> ctree list -> ctree list) -> ctree -> int list -> ctree * bool
1.18 - val appl_obj : (ppobj -> ppobj) -> ctree -> pos -> ctree
1.19 - val appl_to_node : (ppobj -> ppobj) -> ctree -> ctree
1.20 - datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB
1.21 - val branch2str : branch -> string
1.22 - val cappend_atomic :
1.23 - ctree -> pos -> istate * Proof.context -> term -> tac -> term * term list -> ostate -> ctree * pos' list
1.24 - val cappend_form : ctree -> pos -> istate * Proof.context -> term -> ctree * pos' list
1.25 - val cappend_parent : ctree -> pos -> istate * Proof.context -> term -> tac -> branch -> ctree * pos' list
1.26 - val cappend_problem :
1.27 - ctree -> int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree * pos' list
1.28 - eqtype cellID
1.29 - val children : ctree -> ctree list
1.30 - type cid = cellID list
1.31 - datatype con = land | lor
1.32 - val cut_bottom : pos * posel -> ctree -> (ctree * pos' list) * bool
1.33 - val cut_level : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
1.34 - val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
1.35 - val cut_levup : pos' list -> bool -> ctree -> ctree -> posel list * posel -> ctree -> ctree * pos' list
1.36 - val cut_tree : ctree -> pos * 'a -> ctree * pos' list
1.37 - val cutlevup : ppobj -> bool
1.38 - val del_res : ppobj -> ppobj
1.39 - val delete_result : ctree -> pos -> ctree
1.40 - val e_ctxt : Proof.context
1.41 - val e_fmz : 'a list * spec
1.42 - val e_ocalhd : bool * pos_ * term * itm list * (bool * term) list * spec
1.43 - val e_origin : ori list * spec * term
1.44 - val e_ptform : ptform
1.45 - val e_ptform' : ptform
1.46 - val e_ctree : ctree
1.47 - val e_scrstate : scrstate
1.48 - val e_sube : cterm' list
1.49 - val e_subs : string list
1.50 - val e_subte : term list
1.51 - val empty_envp : envp type env = (term * term) list
1.52 - type envp = (int * term list) list * (int * rls) list * (int * ets) list * (string * pos) list
1.53 - val eq_tac : tac * tac -> bool type ets = (loc_ * (tac_ * env * env * term * term * safe)) list
1.54 - val ets2s : loc_ * (tac_ * subst * subst * term * term * safe) -> string
1.55 - val ets2str : ets -> string
1.56 - val exist_lev_on' : ctree -> pos' -> bool
1.57 - val existpt : pos -> ctree -> bool
1.58 - val existpt' : pos' -> ctree -> bool
1.59 - type fmz = fmz_ * spec
1.60 - type fmz_ = cterm' list
1.61 - val g_branch : ppobj -> branch
1.62 - val g_cell : ppobj -> lrd option
1.63 - val g_ctxt : ppobj -> Proof.context
1.64 - val g_domID : ppobj -> domID
1.65 - val g_env : ppobj -> (istate * Proof.context) option
1.66 - val g_fmz : ppobj -> fmz
1.67 - val g_form : ppobj -> term
1.68 - val g_form' : ctree -> term
1.69 - val g_loc : ppobj -> (istate * Proof.context) option * (istate * Proof.context) option
1.70 - val g_met : ppobj -> itm list
1.71 - val g_metID : ppobj -> metID
1.72 - val g_origin : ppobj -> ori list * spec * term
1.73 - val g_ostate : ppobj -> ostate
1.74 - val g_ostate' : ctree -> ostate
1.75 - val g_pbl : ppobj -> itm list
1.76 - val g_res : ppobj -> term
1.77 - val g_res' : ctree -> term
1.78 - val g_result : ppobj -> term * term list
1.79 - val g_spec : ppobj -> spec
1.80 - val g_tac : ppobj -> tac
1.81 - val get_all : (ppobj -> 'a) -> ctree -> 'a list
1.82 - val get_allp : pos' list -> pos * (int list * pos_) -> ctree -> pos' list
1.83 - val get_allpos' : pos * posel -> ctree -> pos' list
1.84 - val get_allpos's : pos * posel -> ctree list -> (pos * pos_) list
1.85 - val get_allps : (pos * pos_) list -> posel list -> ctree list -> pos' list
1.86 - val get_alls : (ppobj -> 'a) -> ctree list -> 'a list
1.87 - val get_assumptions_ : ctree -> pos * pos_ -> term list
1.88 - val get_ctxt : ctree -> pos * pos_ -> Proof.context
1.89 - val get_curr_formula : ctree * (pos * pos_) -> term
1.90 - val get_istate : ctree -> pos * pos_ -> istate
1.91 - val get_loc : ctree -> pos * pos_ -> istate * Proof.context
1.92 - val get_nd : ctree -> pos -> ctree
1.93 - val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a
1.94 - val get_somespec : spec -> spec -> spec
1.95 - val get_somespec' : spec -> spec -> spec
1.96 - val get_trace : ctree -> int list -> int list -> int list list
1.97 - val gpt_cell : ctree -> lrd option
1.98 - type iist = istate option * istate option
1.99 - val ind : pos' -> int
1.100 - val ins_chn : ctree list -> ctree -> int list -> ctree
1.101 - val ins_nth : int -> 'a -> 'a list -> 'a list
1.102 - val insert_pt : ppobj -> ctree -> int list -> ctree
1.103 - val is_curr_endof_calc : ctree -> pos' -> bool
1.104 - val is_e_ctxt : Proof.context -> bool
1.105 - val is_empty_tac : tac -> bool
1.106 - val is_interpos : pos' -> bool
1.107 - val is_pblnd : ctree -> bool
1.108 - val is_pblobj : ppobj -> bool
1.109 - val is_pblobj' : ctree -> pos -> bool
1.110 - val is_prfobj : ppobj -> bool
1.111 - val is_rewset : tac -> bool
1.112 - val is_rewtac : tac -> bool
1.113 - val isasub2subst : term -> (term * term) list
1.114 - datatype istate = RrlsState of rrlsstate | ScrState of scrstate | Uistate
1.115 - val istate2str : istate -> string
1.116 - val istates2str : istate option * istate option -> string
1.117 - val just_created : ctree * pos' -> bool
1.118 - val just_created_ : ppobj -> bool
1.119 - val last_onlev : ctree -> pos -> bool
1.120 - val lev_back' : pos' -> pos'
1.121 - val lev_dn : posel list -> posel list
1.122 - val lev_dnRes : pos' -> pos'
1.123 - val lev_dn_ : pos' -> pos'
1.124 - val lev_of : pos' -> int
1.125 - val lev_on : pos -> posel list
1.126 - val lev_on' : ctree -> pos' -> pos'
1.127 - val lev_onFrm : pos' -> pos'
1.128 - val lev_pred : pos -> pos
1.129 - val lev_pred' : ctree -> pos' -> pos'
1.130 - val lev_up : pos -> pos
1.131 - val lev_up_ : pos' -> pos'
1.132 - val move_dn : pos -> ctree -> int list * pos_ -> int list * pos_
1.133 - val move_up : int list -> ctree -> int list * pos_ -> int list * pos_
1.134 - val movecalchd_up : ctree -> pos' -> pos'
1.135 - val movelevel_dn : int list -> ctree -> int list * pos_ -> int list * pos_
1.136 - val movelevel_up : int list -> ctree -> int list * pos_ -> int list * pos_
1.137 - val new_val : term -> istate -> istate
1.138 - val nth : int -> 'a list -> 'a
1.139 - type ocalhd = bool * pos_ * term * itm list * (bool * term) list * spec
1.140 - val ocalhd2str : ocalhd -> string
1.141 - datatype ostate = Complete | Incomplete | Inconsistent
1.142 - val ostate2str : ostate -> string
1.143 - val par_children : ctree -> pos -> ctree list * pos
1.144 - val par_pbl_det : ctree -> pos -> bool * pos * rls
1.145 - val par_pblobj : ctree -> pos -> pos
1.146 - type pos = posel list
1.147 - type pos' = pos * pos_
1.148 - val pos's2str : (int list * pos_) list -> string
1.149 - val pos2str : int list -> string
1.150 - datatype pos_ = Frm | Met | Pbl | Res | Und
1.151 - val pos_2str : pos_ -> string
1.152 - val pos_plus : int -> pos * pos_ -> pos'
1.153 - eqtype posel
1.154 - val posless : int list -> int list -> bool
1.155 - datatype ppobj
1.156 - = PblObj of
1.157 - {branch: branch,
1.158 - cell: lrd option,
1.159 - ctxt: Proof.context,
1.160 - env: (istate * Proof.context) option,
1.161 - fmz: fmz,
1.162 - loc: (istate * Proof.context) option * (istate * Proof.context) option,
1.163 - meth: itm list,
1.164 - origin: ori list * spec * term, ostate: ostate, probl: itm list, result: term * term list, spec: spec}
1.165 - | PrfObj of
1.166 - {branch: branch,
1.167 - cell: lrd option,
1.168 - form: term,
1.169 - loc: (istate * Proof.context) option * (istate * Proof.context) option,
1.170 - ostate: ostate, result: term * term list, tac: tac}
1.171 - val pr_pos : int list -> string
1.172 - val pr_ctree : (pos -> ppobj -> string) -> ctree -> string
1.173 - val pr_short : pos -> ppobj -> string
1.174 - val pre_pos : pos -> pos
1.175 - val preconds2str : (bool * term) list -> string
1.176 - datatype ptform = Form of term | ModSpec of ocalhd
1.177 - datatype ctree = EmptyPtree | Nd of ppobj * ctree list
1.178 - val rep_pblobj :
1.179 - ppobj ->
1.180 - {branch: branch,
1.181 - cell: lrd option,
1.182 - ctxt: Proof.context,
1.183 - env: (istate * Proof.context) option,
1.184 - fmz: fmz,
1.185 - loc: (istate * Proof.context) option * (istate * Proof.context) option,
1.186 - meth: itm list,
1.187 - origin: ori list * spec * term, ostate: ostate, probl: itm list, result: term * term list, spec: spec}
1.188 - val rep_prfobj :
1.189 - ppobj ->
1.190 - {branch: branch,
1.191 - cell: lrd option,
1.192 - form: term,
1.193 - loc: (istate * Proof.context) option * (istate * Proof.context) option,
1.194 - ostate: ostate, result: term * term list, tac: tac}
1.195 - val repl : 'a list -> int -> 'a -> 'a list
1.196 - val repl_app : 'a list -> int -> 'a -> 'a list
1.197 - val repl_branch : branch -> ppobj -> ppobj
1.198 - val repl_ctxt : Proof.context -> ppobj -> ppobj
1.199 - val repl_domID : domID -> ppobj -> ppobj
1.200 - val repl_env : (istate * Proof.context) option -> ppobj -> ppobj
1.201 - val repl_form : term -> ppobj -> ppobj
1.202 - val repl_loc : (istate * Proof.context) option * (istate * Proof.context) option -> ppobj -> ppobj
1.203 - val repl_met : itm list -> ppobj -> ppobj
1.204 - val repl_metID : metID -> ppobj -> ppobj
1.205 - val repl_oris : ori list -> ppobj -> ppobj
1.206 - val repl_orispec : spec -> ppobj -> ppobj
1.207 - val repl_pbl : itm list -> ppobj -> ppobj
1.208 - val repl_pblID : pblID -> ppobj -> ppobj
1.209 - val repl_result :
1.210 - (istate * Proof.context) option * (istate * Proof.context) option ->
1.211 - term * term list -> ostate -> ppobj -> ppobj
1.212 - val repl_spec : spec -> ppobj -> ppobj
1.213 - val repl_tac : tac -> ppobj -> ppobj
1.214 - val res2str : term * term list -> string
1.215 - val rls_of : tac -> rls'
1.216 - val rls_of_rewset : tac -> rls' * subst option
1.217 - val rootthy : ctree -> theory
1.218 - val rta2str : rule * (term * term list) -> string
1.219 - val rule2tac : theory -> (term * term) list -> rule -> tac
1.220 - val safe2str : safe -> string
1.221 - type scrstate = env * loc_ * term option * term * safe * bool
1.222 - val scrstate2str : subst * loc_ * term option * term * safe * bool -> string
1.223 - val str2pos_ : string -> pos_
1.224 - type sube = cterm' list
1.225 - val sube2str : string list -> string
1.226 - val sube2subst : theory -> string list -> (term * term) list
1.227 - val sube2subte : string list -> term list
1.228 - type subs = cterm' list
1.229 - val subs2subst : theory -> string list -> (term * term) list
1.230 - val subst2sube : (term * term) list -> string list
1.231 - val subst2subs : (term * term) list -> string list
1.232 - val subst2subs' : (term * term) list -> (string * string) list
1.233 - type subte = term list
1.234 - val subte2str : term list -> string
1.235 - val subte2sube : term list -> string list
1.236 - val subte2subst : term list -> (term * term) list
1.237 - datatype tac
1.238 - = Add_Find of cterm' | Add_Given of cterm' | Add_Relation of cterm' | Apply_Assumption of cterm' list
1.239 - | Apply_Method of metID | Begin_Sequ | Begin_Trans | CAScmd of cterm' | Calculate of string
1.240 - | Check_Postcond of pblID | Check_elementwise of cterm' | Collect_Trues | Conclude_And | Conclude_Or
1.241 - | Del_Find of cterm' | Del_Given of cterm' | Del_Relation of cterm' | Derive of rls' | Detail_Set of rls'
1.242 - | Detail_Set_Inst of subs * rls' | Empty_Tac | End_Detail | End_Intersect | End_Proof' | End_Ruleset
1.243 - | End_Sequ | End_Subproblem | End_Trans | Free_Solve | Group of con * int list
1.244 - | Init_Proof of cterm' list * spec | Model_Problem | Or_to_List | Refine_Problem of pblID
1.245 - | Refine_Tacitly of pblID | Rewrite of thm'' | Rewrite_Asm of thm'' | Rewrite_Inst of subs * thm''
1.246 - | Rewrite_Set of rls' | Rewrite_Set_Inst of subs * rls' | Specify_Method of metID
1.247 - | Specify_Problem of pblID | Specify_Theory of domID | Split_And | Split_Intersect | Split_Or
1.248 - | Subproblem of domID * pblID | Substitute of sube | Tac of string | Take of cterm' | Take_Inst of cterm'
1.249 - val tac2IDstr : tac -> string
1.250 - datatype tac_
1.251 - = Add_Find' of cterm' * itm list | Add_Given' of cterm' * itm list | Add_Relation' of cterm' * itm list
1.252 - | Apply_Assumption' of term list * term | Apply_Method' of metID * term option * istate * Proof.context
1.253 - | Begin_Sequ' | Begin_Trans' of term | CAScmd' of term
1.254 - | Calculate' of theory' * string * term * (term * thm') | Check_Postcond' of pblID * (term * term list)
1.255 - | Check_elementwise' of term * string * (term * term list) | Collect_Trues' of term
1.256 - | Conclude_And' of term | Conclude_Or' of term | Del_Find' of cterm' | Del_Given' of cterm'
1.257 - | Del_Relation' of cterm' | Derive' of rls
1.258 - | Detail_Set' of theory' * bool * rls * term * (term * term list)
1.259 - | Detail_Set_Inst' of theory' * bool * subst * rls * term * (term * term list) | Empty_Tac_
1.260 - | End_Detail' of term * term list | End_Intersect' of term | End_Proof'' | End_Ruleset' of term
1.261 - | End_Sequ' | End_Subproblem' of term | End_Trans' of term * term list | Free_Solve'
1.262 - | Group' of con * int list * term | Init_Proof' of cterm' list * spec
1.263 - | Model_Problem' of pblID * itm list * itm list | Or_to_List' of term * term
1.264 - | Refine_Problem' of pblID * (itm list * (bool * term) list)
1.265 - | Refine_Tacitly' of pblID * pblID * domID * metID * itm list
1.266 - | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * (term * term list)
1.267 - | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * (term * term list)
1.268 - | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * (term * term list)
1.269 - | Rewrite_Set' of theory' * bool * rls * term * (term * term list)
1.270 - | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * (term * term list)
1.271 - | Specify_Method' of metID * ori list * itm list
1.272 - | Specify_Problem' of pblID * (bool * (itm list * (bool * term) list)) | Specify_Theory' of domID
1.273 - | Split_And' of term | Split_Intersect' of term | Split_Or' of term
1.274 - | Subproblem' of spec * ori list * term * fmz_ * Proof.context * term
1.275 - | Substitute' of rew_ord_ * rls * subte * term * term | Tac_ of theory * string * string * string
1.276 - | Take' of term | Take_Inst' of term
1.277 - val tac_2str : tac_ -> string
1.278 - val test_trans : ppobj -> bool
1.279 - val thm_of_rew : tac -> thmID * subst option
1.280 - val topt2str : term option -> string
1.281 - val update_branch : ctree -> pos -> branch -> ctree
1.282 - val update_ctxt : ctree -> pos -> Proof.context -> ctree
1.283 - val update_domID : ctree -> pos -> domID -> ctree
1.284 - val update_env : ctree -> pos -> (istate * Proof.context) option -> ctree
1.285 - val update_loc' : ctree -> pos -> (istate * Proof.context) option * (istate * Proof.context) option -> ctree
1.286 - val update_met : ctree -> pos -> itm list -> ctree
1.287 - val update_metID : ctree -> pos -> metID -> ctree
1.288 - val update_metppc : ctree -> pos -> itm list -> ctree
1.289 - val update_oris : ctree -> pos -> ori list -> ctree
1.290 - val update_orispec : ctree -> pos -> spec -> ctree
1.291 - val update_pbl : ctree -> pos -> itm list -> ctree
1.292 - val update_pblID : ctree -> pos -> pblID -> ctree
1.293 - val update_pblppc : ctree -> pos -> itm list -> ctree
1.294 - val update_spec : ctree -> pos -> spec -> ctree
1.295 - val update_tac : ctree -> pos -> tac -> ctree end
1.296 -*)
1.297
1.298 (**)
1.299 structure Ctree(**): CALC_TREEE(**) =
1.300 @@ -1205,7 +915,7 @@
1.301 ostate: ostate}; (* like PrfObj *)
1.302
1.303 (*.this tree contains isac's calculations; TODO.WN03 rename to ctree;
1.304 - the structure has been copied from an early version of Theorema(c);
1.305 + the tree's structure has been copied from an early version of Theorema(c);
1.306 it has the disadvantage, that there is no space
1.307 for the first tactic in a script generating the first formula at (p,Frm);
1.308 this trouble has been covered by 'init_form' and 'Take' so far,
2.1 --- a/src/Tools/isac/Interpret/inform.sml Thu Dec 22 11:36:20 2016 +0100
2.2 +++ b/src/Tools/isac/Interpret/inform.sml Thu Dec 22 11:55:16 2016 +0100
2.3 @@ -371,7 +371,7 @@
2.4 (* compare inform with ctree.form at current pos by nrls;
2.5 if found, embed the derivation generated during comparison
2.6 if not, let the mat-engine compute the next ctree.form *)
2.7 -(* structure copied from complete_solve
2.8 +(* code's structure is copied from complete_solve
2.9 CAUTION: tacis in returned calcstate' do NOT construct resulting ptp --
2.10 all_modspec etc. has to be inserted at Subproblem'*)
2.11 fun compare_step ((tacis, c, ptp as (pt, pos as (p,p_))): Chead.calcstate') ifo =