1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic-TEST.sml Wed Mar 08 17:47:07 2023 +0100
1.3 @@ -0,0 +1,816 @@
1.4 +(* Title: the calctree, which holds a calculation
1.5 + Author: Walther Neuper 1999
1.6 + (c) due to copyright terms
1.7 +
1.8 +Definitions required for Ctree, renamed later appropriately
1.9 +-------------------------vvvvv + I_Model.T-TEST are the only difference to
1.10 + BASIC_CALC_TREE
1.11 +*)
1.12 +
1.13 +signature BASIC_CALC_TREE_TEST =
1.14 +sig
1.15 +(**** signature ****)
1.16 +(** the basic datatype **)
1.17 + type state
1.18 + val e_state: state
1.19 +
1.20 + type con
1.21 + eqtype cellID
1.22 +
1.23 + datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB
1.24 + datatype ostate = Complete | Incomplete | Inconsistent
1.25 + type specify_data
1.26 + type solve_data
1.27 + datatype ppobj = PblObj of specify_data | PrfObj of solve_data
1.28 + datatype ctree = EmptyPtree | Nd of ppobj * ctree list
1.29 +
1.30 + val rep_solve_data: ppobj -> solve_data
1.31 + val rep_specify_data: ppobj -> specify_data
1.32 +
1.33 +(** basic functions **)
1.34 + val e_ctree : ctree (* TODO: replace by EmptyPtree*)
1.35 + val existpt' : Pos.pos' -> ctree -> bool
1.36 + val is_interpos : Pos.pos' -> bool
1.37 + val lev_pred' : ctree -> Pos.pos' -> Pos.pos'
1.38 + val ins_chn : ctree list -> ctree -> Pos.pos -> ctree
1.39 + val children : ctree -> ctree list
1.40 + val get_nd : ctree -> Pos.pos -> ctree
1.41 + val just_created_ : ppobj -> bool
1.42 + val just_created : state -> bool
1.43 + val e_origin : Model_Def.o_model * References_Def.T * term
1.44 +
1.45 + val is_pblobj : ppobj -> bool
1.46 + val is_pblobj' : ctree -> Pos.pos -> bool
1.47 + val is_pblnd : ctree -> bool
1.48 +
1.49 + val g_spec : ppobj -> References_Def.T
1.50 + val g_loc : ppobj -> (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option
1.51 + val g_form : ppobj -> term
1.52 + val g_pbl : ppobj -> Model_Def.i_model_TEST
1.53 + val g_met : ppobj -> Model_Def.i_model_TEST
1.54 + val g_metID : ppobj -> MethodC.id
1.55 + val g_result : ppobj -> Celem.result
1.56 + val g_tac : ppobj -> Tactic.input
1.57 + val g_domID : ppobj -> ThyC.id
1.58 +
1.59 + val g_origin : ppobj -> Model_Def.o_model * References_Def.T * term
1.60 + val get_loc : ctree -> Pos.pos' -> Istate_Def.T * Proof.context
1.61 + val get_istate_LI : ctree -> Pos.pos' -> Istate_Def.T
1.62 + val get_ctxt_LI: ctree -> Pos.pos' -> Proof.context
1.63 + val get_ctxt : ctree -> Pos.pos' -> Proof.context (*DEPRECATED*)
1.64 + val get_obj : (ppobj -> 'a) -> ctree -> Pos.pos -> 'a
1.65 + val get_curr_formula : state -> term
1.66 + val get_assumptions : ctree -> Pos.pos' -> term list
1.67 +
1.68 + val new_val : term -> Istate_Def.T -> Istate_Def.T
1.69 +
1.70 + type cid = cellID list
1.71 + datatype ptform = Form of term | ModSpec of Specification_Def.T
1.72 + val get_somespec' : References_Def.T -> References_Def.T -> References_Def.T
1.73 + exception PTREE of string;
1.74 +
1.75 + val root_thy : ctree -> theory
1.76 +(* ---- made visible ONLY for structure CTaccess : CALC_TREE_ACCESS --------------------------- *)
1.77 + val appl_obj : (ppobj -> ppobj) -> ctree -> Pos.pos -> ctree
1.78 + val existpt : Pos.pos -> ctree -> bool
1.79 + val cut_tree : ctree -> Pos.pos * 'a -> ctree * Pos.pos' list
1.80 + val insert_pt : ppobj -> ctree -> int list -> ctree
1.81 +(* ---- made visible ONLY for structure CTnavi : CALC_TREE_NAVIGATION ------------------------- *)
1.82 + val g_branch : ppobj -> branch
1.83 + val g_form' : ctree -> term
1.84 + val g_ostate : ppobj -> ostate
1.85 + val g_ostate' : ctree -> ostate
1.86 + val g_res : ppobj -> term
1.87 + val g_res' : ctree -> term
1.88 +(*/---- duplicates in CTnavi, reconsider structs -----------------------------------------------
1.89 + val lev_dn : CTbasic.Pos.pos -> Pos.pos (* duplicate in ctree-navi.sml *)
1.90 + val par_pblobj : CTbasic.ctree -> Pos.pos -> Pos.pos (* duplicate in ctree-navi.sml *)
1.91 + ---- duplicates in CTnavi, reconsider structs ----------------------------------------------/*)
1.92 +(*from isac_test for Minisubpbl*)
1.93 + val pr_ctree: Proof.context -> (Proof.context -> int list -> ppobj -> string) -> ctree -> string
1.94 + val pr_short: Proof.context -> Pos.pos -> ppobj -> string
1.95 +
1.96 +\<^isac_test>\<open>
1.97 + val g_ctxt : ppobj -> Proof.context
1.98 + val g_fmz : ppobj -> Model_Def.form_T
1.99 + val get_allp : Pos.pos' list -> Pos.pos * (int list * Pos.pos_) -> ctree -> Pos.pos' list
1.100 + val get_allps : (Pos.pos * Pos.pos_) list -> Pos.posel list -> ctree list -> Pos.pos' list
1.101 + val get_allpos' : Pos.pos * Pos.posel -> ctree -> Pos.pos' list
1.102 + val get_allpos's : Pos.pos * Pos.posel -> ctree list -> (Pos.pos * Pos.pos_) list
1.103 + val cut_bottom : Pos.pos * Pos.posel -> ctree -> (ctree * Pos.pos' list) * bool
1.104 + val cut_level : Pos.pos' list -> Pos.pos -> ctree -> int list * Pos.pos_ -> ctree * Pos.pos' list
1.105 + val cut_level__ : Pos.pos' list -> Pos.pos -> ctree -> int list * Pos.pos_ -> ctree * Pos.pos' list
1.106 + val get_trace : ctree -> int list -> int list -> int list list
1.107 + val branch2str : branch -> string
1.108 +\<close>
1.109 +end
1.110 +
1.111 +(**)
1.112 +structure CTbasic_TEST(**): BASIC_CALC_TREE_TEST(**) =
1.113 +struct
1.114 +(**)
1.115 +open Pos
1.116 +
1.117 +(**** Ctree ****)
1.118 +
1.119 +(*** general types* **)
1.120 +
1.121 +datatype branch =
1.122 + NoBranch | AndB | OrB
1.123 +| TransitiveB (* FIXXXME.0308: set branch from met in Apply_Method
1.124 + FIXXXME.0402: -"- in Begin_Trans'*)
1.125 +| SequenceB | IntersectB | CollectB | MapB;
1.126 +
1.127 +\<^isac_test>\<open>
1.128 +fun branch2str NoBranch = "NoBranch"
1.129 + | branch2str AndB = "AndB"
1.130 + | branch2str OrB = "OrB"
1.131 + | branch2str TransitiveB = "TransitiveB"
1.132 + | branch2str SequenceB = "SequenceB"
1.133 + | branch2str IntersectB = "IntersectB"
1.134 + | branch2str CollectB = "CollectB"
1.135 + | branch2str MapB = "MapB";
1.136 +\<close>
1.137 +
1.138 +datatype ostate =
1.139 + Incomplete | Complete | Inconsistent (* WN041020 latter still unused *);
1.140 +\<^isac_test>\<open>
1.141 +fun ostate2str Incomplete = "Incomplete"
1.142 + | ostate2str Complete = "Complete"
1.143 + | ostate2str Inconsistent = "Inconsistent";
1.144 +\<close>
1.145 +
1.146 +type cellID = int;
1.147 +type cid = cellID list;
1.148 +
1.149 +
1.150 +type iist = Istate_Def.T option * Istate_Def.T option;
1.151 +(*val e_iist = (empty, empty); --- sinnlos f"ur NICHT-equality-type*)
1.152 +
1.153 +
1.154 +fun new_val v (Istate_Def.Pstate pst) =
1.155 + (Istate_Def.Pstate (Istate_Def.set_act v pst))
1.156 + | new_val _ _ = raise ERROR "new_val: only for Pstate";
1.157 +
1.158 +datatype con = land | lor;
1.159 +
1.160 +(* executed tactics (tac_s) with local environment etc.;
1.161 + used for continuing eval script + for generate *)
1.162 +type ets =
1.163 + (TermC.path *(* of tactic in program, tactic (weakly) associated with tac_ *)
1.164 + (Tactic.T * (* (for generate) *)
1.165 + Env.T * (* with 'tactic=result' as rule, tactic ev. _not_ ready for 'parallel let' *)
1.166 + Env.T * (* with results of (ready) tacs *)
1.167 + term * (* itr_arg of tactic, for upd. env at Repeat, Try *)
1.168 + term * (* result value of the tac *)
1.169 + Celem.safe))
1.170 + list;
1.171 +
1.172 +type envp =(*9.5.03: unused, delete with field in ctree.PblObj FIXXXME*)
1.173 + (int * term list) list * (* assoc-list: args of met*)
1.174 + (int * Rule_Set.T) list * (* assoc-list: tacs already done ///15.9.00*)
1.175 + (int * ets) list * (* assoc-list: tacs etc. already done*)
1.176 + (string * pos) list; (* asms * from where*)
1.177 +
1.178 +
1.179 +(*** type Ctree ***)
1.180 +
1.181 +type specify_data =
1.182 + {fmz : Model_Def.form_T, (* for uniformity also created/used for/by Subproblem *)
1.183 + origin: (Model_Def.o_model) *(* = O_Model.T for efficiently checking input to I_Model *)
1.184 + References_Def.T * (* updated by Refine_Tacitly *)
1.185 + term, (* headline of calc-head, as calculated initially(!) *)
1.186 + spec : References_Def.T, (* explicitly input *)
1.187 + probl : Model_Def.i_model_TEST,(* = I_Model.T for interactive input to a Problem *)
1.188 + meth : Model_Def.i_model_TEST,(* = I_Model.T for interactive input to a MethodC *)
1.189 + ctxt : Proof.context, (* used while specifying this (Sub-)Problem and MethodC *)
1.190 + loc : (Istate_Def.T * Proof.context) option (* like in PrfObj, calling this SubProblem *)
1.191 + * (Istate_Def.T * Proof.context) option, (* like in PrfObj, finishing the SubProblem *)
1.192 + branch: branch, (* like PrfObj *)
1.193 + result: Celem.result, (* like PrfObj *)
1.194 + ostate: ostate}; (* like PrfObj *)
1.195 +type solve_data = (* TODO: arrange according to signature *)
1.196 + {form : term, (* where tactic is applied to *)
1.197 + tac : Tactic.input, (* tactic as presented to users *)
1.198 + loc : (Istate_Def.T * (* program interpreter state *)
1.199 + Proof.context) (* context for provers, type inference *)
1.200 + option * (* both for interpreter location on Frm, Pbl, Met *)
1.201 + (Istate_Def.T * (* script interpreter state *)
1.202 + Proof.context) (* context for provers, type inference *)
1.203 + option, (* both for interpreter location on Res, (NONE,NONE) == empty *)
1.204 + branch: branch, (* only rudimentary *)
1.205 + result: Celem.result, (* result and assumptions *)
1.206 + ostate: ostate} (* Complete <=> result is OK *)
1.207 +
1.208 +datatype ppobj =
1.209 + PblObj of specify_data (* data serving a whole specification-phase *)
1.210 +| PrfObj of solve_data; (* data for a proof step triggered by a tactic *)
1.211 +
1.212 +(* this tree contains isac's calculations;
1.213 + the tree's structure has been copied from an early version of Theorema(c);
1.214 + it has the disadvantage, that there is no space
1.215 + for the first tactic in a script generating the first formula at (p,Frm);
1.216 + this trouble has been covered by 'implicit_take' and 'Take' so far,
1.217 + but it is crucial if the first tactic in a script is eg. 'Subproblem';
1.218 + see 'type tac', Apply_Method.
1.219 +*)
1.220 +datatype ctree =
1.221 + EmptyPtree
1.222 +| Nd of ppobj * (ctree list);
1.223 +val e_ctree = EmptyPtree;
1.224 +type state = ctree * pos'
1.225 +val e_state = (EmptyPtree , e_pos')
1.226 +
1.227 +fun rep_solve_data (PrfObj solve_data) = solve_data
1.228 + | rep_solve_data _ = raise ERROR "rep_solve_data ONLY for solve_data"
1.229 +fun rep_specify_data (PblObj specify_data) = specify_data
1.230 + | rep_specify_data _ = raise ERROR "rep_solve_data ONLY for solve_data"
1.231 +
1.232 +
1.233 +(*** minimal set of functions on Ctree* **)
1.234 +
1.235 +fun is_pblobj (PblObj _) = true
1.236 + | is_pblobj _ = false;
1.237 +
1.238 +exception PTREE of string;
1.239 +fun nth _ [] = raise PTREE "nth _ []"
1.240 + | nth 1 (x :: _) = x
1.241 + | nth n (_ :: xs) = nth (n - 1) xs;
1.242 +(*> nth 2 [11,22,33]; -->> val it = 22 : int*)
1.243 +
1.244 +
1.245 +(** convert ctree to a string **)
1.246 +
1.247 +(* convert a pos from list to string *)
1.248 +fun pr_pos ps = (space_implode "." (map string_of_int ps)) ^ ". ";
1.249 +(* show hd origin or form only *)
1.250 +(**)
1.251 +fun pr_short _ p (PblObj _) = pr_pos p ^ " ----- pblobj -----\n"
1.252 + | pr_short ctxt p (PrfObj {form = form, ...}) = pr_pos p ^ UnparseC.term ctxt form ^ "\n";
1.253 +fun pr_ctree ctxt f pt =
1.254 + let
1.255 + fun pr_pt _ _ EmptyPtree = ""
1.256 + | pr_pt pfn ps (Nd (b, [])) = pfn ps b
1.257 + | pr_pt pfn ps (Nd (b, ts)) = pfn ps b ^ prts pfn ps 1 ts
1.258 + and prts _ _ _ [] = ""
1.259 + | prts pfn ps p (t :: ts) = (pr_pt pfn (ps @ [p]) t)^
1.260 + (prts pfn ps (p + 1) ts)
1.261 + in pr_pt (f ctxt) [] pt end;
1.262 +
1.263 +
1.264 +
1.265 +(** access the branches of ctree **)
1.266 +
1.267 +fun repl [] _ _ = raise PTREE "repl [] _ _"
1.268 + | repl (_ :: ls) 1 e = e :: ls
1.269 + | repl (l :: ls) n e = l :: (repl ls (n-1) e);
1.270 +fun repl_app ls n e =
1.271 + let
1.272 + val lim = 1 + length ls
1.273 + in
1.274 + if n > lim
1.275 + then raise PTREE "repl_app: n > lim"
1.276 + else if n = lim
1.277 + then ls @ [e]
1.278 + else repl ls n e end;
1.279 +
1.280 +(* get from obj at pos by f : ppobj -> 'a *)
1.281 +fun get_obj _ EmptyPtree _ = raise PTREE "get_obj f EmptyPtree"
1.282 + | get_obj f (Nd (b, _)) [] = f b
1.283 + | get_obj f (Nd (_, bs)) (p :: ps) =
1.284 + case \<^try>\<open> get_obj f (nth p bs) ps \<close> of
1.285 + SOME obj => obj
1.286 + | NONE => raise PTREE ("get_obj: pos = " ^ ints2str' (p :: ps) ^ " does not exist");
1.287 +fun get_nd EmptyPtree _ = raise PTREE "get_nd EmptyPtree"
1.288 + | get_nd n [] = n
1.289 + | get_nd (Nd (_, nds)) (pos as p :: ps) =
1.290 + case \<^try>\<open> get_nd (nth p nds) ps \<close> of
1.291 + SOME nd => nd
1.292 + | NONE => raise PTREE ("get_nd: not existent pos = " ^ ints2str' pos);
1.293 +
1.294 +(* for use by get_obj *)
1.295 +fun g_form (PrfObj {form = f,...}) = f
1.296 + | g_form (PblObj {origin= (_,_,f),...}) = f;
1.297 +fun g_form' (Nd (PrfObj {form = f, ...}, _)) = f
1.298 + | g_form' (Nd (PblObj {origin= (_, _, f),...}, _)) = f
1.299 + | g_form' _ = raise ERROR "g_form': uncovered fun def.";
1.300 +(* | g_form _ = raise PTREE "g_form not for PblObj";*)
1.301 +fun g_origin (PblObj {origin = ori, ...}) = ori
1.302 + | g_origin _ = raise PTREE "g_origin not for PrfObj";
1.303 +\<^isac_test>\<open>
1.304 +fun g_fmz (PblObj {fmz = f, ...}) = f
1.305 + | g_fmz _ = raise PTREE "g_fmz not for PrfObj";
1.306 +\<close>
1.307 +fun g_spec (PblObj {spec = s, ...}) = s
1.308 + | g_spec _ = raise PTREE "g_spec not for PrfObj";
1.309 +fun g_pbl (PblObj {probl = p, ...}) = p
1.310 + | g_pbl _ = raise PTREE "g_pbl not for PrfObj";
1.311 +fun g_met (PblObj {meth = p, ...}) = p
1.312 + | g_met _ = raise PTREE "g_met not for PrfObj";
1.313 +fun g_domID (PblObj {spec = (d, _, _), ...}) = d
1.314 + | g_domID _ = raise PTREE "g_metID not for PrfObj";
1.315 +fun g_metID (PblObj {spec = (_, _, m), ...}) = m
1.316 + | g_metID _ = raise PTREE "g_metID not for PrfObj";
1.317 +fun g_ctxt (PblObj {ctxt, ...}) = ctxt
1.318 + | g_ctxt _ = raise PTREE "g_ctxt not for PrfObj";
1.319 +fun g_loc (PblObj {loc = l, ...}) = l
1.320 + | g_loc (PrfObj {loc = l, ...}) = l;
1.321 +fun g_branch (PblObj {branch = b, ...}) = b
1.322 + | g_branch (PrfObj {branch = b, ...}) = b;
1.323 +fun g_tac (PblObj {spec = (_, _, m),...}) = Tactic.Apply_Method m
1.324 + | g_tac (PrfObj {tac = m, ...}) = m;
1.325 +fun g_result (PblObj {result = r, ...}) = r
1.326 + | g_result (PrfObj {result = r, ...}) = r;
1.327 +fun g_res (PblObj {result = (r, _) ,...}) = r
1.328 + | g_res (PrfObj {result = (r, _),...}) = r;
1.329 +fun g_res' (Nd (PblObj {result = (r, _), ...}, _)) = r
1.330 + | g_res' (Nd (PrfObj {result = (r, _),...}, _)) = r
1.331 + | g_res' _ = raise PTREE "g_res': uncovered fun def.";
1.332 +fun g_ostate (PblObj {ostate = r, ...}) = r
1.333 + | g_ostate (PrfObj {ostate = r, ...}) = r;
1.334 +fun g_ostate' (Nd (PblObj {ostate = r, ...}, _)) = r
1.335 + | g_ostate' (Nd (PrfObj {ostate = r, ...}, _)) = r
1.336 + | g_ostate' _ = raise PTREE "g_ostate': uncovered fun def.";
1.337 +
1.338 +(* get the formula preceeding the current position in a calculation *)
1.339 +fun get_curr_formula (pt, (p, p_)) =
1.340 + case p_ of
1.341 + Frm => get_obj g_form pt p
1.342 + | Res => (fst o (get_obj g_result pt)) p
1.343 + | _ => #3 (get_obj g_origin pt p); (* the headline*)
1.344 +
1.345 +(* in CalcTree/Subproblem an 'just_created_' model is created;
1.346 + this is filled to 'untouched' by Model/Refine_Problem *)
1.347 +fun just_created_ (PblObj {meth, probl, spec, ...}) =
1.348 + null meth andalso null probl andalso spec = References_Def.empty
1.349 + | just_created_ _ = raise PTREE "g_ostate': uncovered fun def.";
1.350 +val e_origin = ([], References_Def.empty, TermC.empty);
1.351 +
1.352 +fun just_created (pt, (p, _)) =
1.353 + let val ppobj = get_obj I pt p
1.354 + in is_pblobj ppobj andalso just_created_ ppobj end;
1.355 +
1.356 +(* does the pos in the ctree exist ? *)
1.357 +fun existpt pos pt = can (get_obj I pt) pos;
1.358 +(* does the pos' in the ctree exist, ie. extra check for result in the node *)
1.359 +fun existpt' (p, p_) pt =
1.360 + if can (get_obj I pt) p
1.361 + then case p_ of
1.362 + Res => get_obj g_ostate pt p = Complete
1.363 + | _ => true
1.364 + else false;
1.365 +
1.366 +(* is this position appropriate for calculating intermediate steps? *)
1.367 +fun is_interpos (_, Res) = true
1.368 + | is_interpos _ = false;
1.369 +
1.370 +(* get the children of a node in ctree *)
1.371 +fun children (Nd (PblObj _, cn)) = cn
1.372 + | children (Nd (PrfObj _, cn)) = cn
1.373 + | children _ = raise ERROR "children: uncovered fun def.";
1.374 +
1.375 +(*/--------------- duplicates in ctree-navi.sml: required also here below ---------------\*)
1.376 +\<^isac_test>\<open>
1.377 +fun lev_up [] = raise PTREE "lev_up []"
1.378 + | lev_up p = (drop_last p):pos;
1.379 +(* find the position of the next parent which is a PblObj in ctree *)
1.380 +fun par_pblobj _ [] = []
1.381 + | par_pblobj pt p =
1.382 + let
1.383 + fun par _ [] = []
1.384 + | par pt p =
1.385 + if is_pblobj (get_obj I pt p)
1.386 + then p
1.387 + else par pt (lev_up p)
1.388 + in par pt (lev_up p) end;
1.389 +\<close>
1.390 +(*\--------------- duplicates in ctree-navi.sml: required also here below ---------------/*)
1.391 +
1.392 +(* insert obj b into ctree at pos, ev.overwriting this pos *)
1.393 +fun insert_pt b EmptyPtree [] = Nd (b, [])
1.394 + | insert_pt _ EmptyPtree _ = raise PTREE "insert_pt b Empty _"
1.395 + | insert_pt b _ [] = Nd (b, [])
1.396 + | insert_pt b (Nd (b', bs)) (p :: []) = Nd (b', repl_app bs p (Nd (b, [])))
1.397 + | insert_pt b (Nd (b', bs)) (p :: ps) = Nd (b', repl_app bs p (insert_pt b (nth p bs) ps));
1.398 +
1.399 +(* insert children to a node without children. compare: fun insert_pt *)
1.400 +fun ins_chn _ EmptyPtree _ = raise PTREE "ins_chn: EmptyPtree"
1.401 + | ins_chn _ (Nd _) [] = raise PTREE "ins_chn: pos = []"
1.402 + | ins_chn ns (Nd (b, bs)) (p :: []) =
1.403 + if p > length bs
1.404 + then raise PTREE "ins_chn: pos not existent"
1.405 + else
1.406 + let
1.407 + val (b', bs') = case nth p bs of
1.408 + Nd (b', bs') => (b', bs')
1.409 + | _ => raise ERROR "ins_chn: uncovered case nth"
1.410 + in
1.411 + if null bs'
1.412 + then Nd (b, repl_app bs p (Nd (b', ns)))
1.413 + else raise PTREE "ins_chn: pos mustNOT be overwritten"
1.414 + end
1.415 + | ins_chn ns (Nd (b, bs)) (p::ps) = Nd (b, repl_app bs p (ins_chn ns (nth p bs) ps));
1.416 +
1.417 +(* apply f to obj at pos, f: ppobj -> ppobj *)
1.418 +fun appl_to_node f (Nd (b, bs)) = Nd (f b, bs)
1.419 + | appl_to_node _ _ = raise ERROR "appl_to_node: uncovered fun def.";
1.420 +fun appl_obj _ EmptyPtree [] = EmptyPtree
1.421 + | appl_obj _ EmptyPtree _ = raise PTREE "appl_obj f Empty _"
1.422 + | appl_obj f (Nd (b, bs)) [] = Nd (f b, bs)
1.423 + | appl_obj f (Nd (b, bs)) (p :: []) = Nd (b, repl_app bs p (((appl_to_node f) o (nth p)) bs))
1.424 + | appl_obj f (Nd (b, bs)) (p :: ps) = Nd (b, repl_app bs p (appl_obj f (nth p bs) (ps:pos)));
1.425 +
1.426 +datatype ptform = Form of term | ModSpec of Specification_Def.T;
1.427 +
1.428 +\<^isac_test>\<open>
1.429 +fun test_trans (PrfObj {branch, ...}) = true andalso branch = TransitiveB
1.430 + | test_trans (PblObj {branch, ...}) = true andalso branch = TransitiveB;
1.431 +\<close>
1.432 +
1.433 +fun is_pblobj' pt p =
1.434 + let val ppobj = get_obj I pt p
1.435 + in is_pblobj ppobj end;
1.436 +
1.437 +fun del_res (PblObj {fmz, origin, spec, probl, meth, ctxt, loc = (l1, _), branch, ...}) =
1.438 + PblObj {fmz = fmz, origin = origin, spec = spec, probl = probl, meth = meth,
1.439 + ctxt = ctxt, loc= (l1, NONE), branch = branch,
1.440 + result = (TermC.empty, []), ostate = Incomplete}
1.441 + | del_res (PrfObj {form, tac, loc= (l1, _), branch, ...}) =
1.442 + PrfObj {form = form, tac = tac, loc = (l1, NONE), branch = branch,
1.443 + result = (TermC.empty, []), ostate = Incomplete};
1.444 +
1.445 +
1.446 +fun get_loc EmptyPtree _ = (Istate_Def.empty, ContextC.empty)
1.447 + | get_loc pt (p, Res) =
1.448 + (case get_obj g_loc pt p of
1.449 + (SOME ist_ctxt, NONE) => ist_ctxt
1.450 + | (NONE , NONE) => (Istate_Def.empty, ContextC.empty)
1.451 + | (_ , SOME ist_ctxt) => ist_ctxt)
1.452 + | get_loc pt (p, _) =
1.453 + (case get_obj g_loc pt p of
1.454 + (NONE , SOME ist_ctxt) => ist_ctxt (* 020813 too liberal? *)
1.455 + | (NONE , NONE) => (Istate_Def.empty, ContextC.empty)
1.456 + | (SOME ist_ctxt, _) => ist_ctxt);
1.457 +fun get_istate_LI pt p = get_loc pt p |> #1;
1.458 +fun get_ctxt_LI pt p = get_loc pt p |> #2;
1.459 +fun get_ctxt pt (pos as (p, p_)) =
1.460 + if member op = [Frm, Res] p_
1.461 + then get_loc pt pos |> #2 (*for program interpretation rely on fun get_loc*)
1.462 + else (*p = Pbl: for specify phase take ctxt from PblObj *)
1.463 + if (p |> get_obj g_origin pt |> LibraryC.fst3) = [] (*CAS-command ? *)
1.464 + then (Know_Store.get_via_last_thy "Isac_Knowledge"(*CAS-command unknown*)) |> Defs.global_context |> fst
1.465 + else get_obj g_ctxt pt p
1.466 +
1.467 +fun get_assumptions pt p = get_ctxt pt p |> ContextC.get_assumptions;
1.468 +
1.469 +fun get_somespec' (dI, pI, mI) (dI', pI', mI') =
1.470 + let
1.471 + val domID = if dI = ThyC.id_empty then dI' else dI
1.472 + val pblID = if pI = Problem.id_empty then pI' else pI
1.473 + val metID = if mI = MethodC.id_empty then mI' else mI
1.474 + in (domID, pblID, metID) end;
1.475 +
1.476 +(**.development for extracting an 'interval' from ptree.**)
1.477 +
1.478 +\<^isac_test>\<open>
1.479 +(*WN0510 version stopped in favour of get_interval with !!!move_dn, getFormulaeFromTo
1.480 + actually used (inefficient) version with move_dn: see modspec.sml*)
1.481 +local
1.482 +
1.483 +fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*)
1.484 +fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*)
1.485 +fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x;
1.486 +fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;
1.487 +
1.488 +fun getnd i (b,p) q (Nd (_, nds)) =
1.489 + (if i <= 0 then [[b]] else []) @
1.490 + (getnds (i-1) true (b@[hdp p], tlp p) (tlq q)
1.491 + (take_fromto (hdp p) (hdq q) nds))
1.492 + | getnd _ _ _ _ = raise ERROR "getnd: uncovered case in fun.def."
1.493 +and getnds _ _ _ _ [] = [] (*no children*)
1.494 + | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*)
1.495 +
1.496 + | getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*)
1.497 + (getnd i ( b, p ) [99999] n1) @
1.498 + (getnd ~99999 (lev_on b,[0]) q n2)
1.499 +
1.500 + | getnds i _ (b, _) q [n1, n2] = (*intern, r-margin*)
1.501 + (getnd i ( b,[0]) [99999] n1) @
1.502 + (getnd ~99999 (lev_on b,[0]) q n2)
1.503 +
1.504 + | getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*)
1.505 + (getnd i ( b, p ) [99999] nd) @
1.506 + (getnds ~99999 false (lev_on b,[0]) q nds)
1.507 +
1.508 + | getnds i _ (b, _) q (nd::(nds as _::_)) = (*intern, ...*)
1.509 + (getnd i ( b,[0]) [99999] nd) @
1.510 + (getnds ~99999 false (lev_on b,[0]) q nds);
1.511 +in
1.512 +(*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes
1.513 + where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
1.514 +(1) the 'f' are given
1.515 +(1a) by 'from' if 'f' = the respective element of 'from' (left margin)
1.516 +(1b) -inifinity, if 'f' > the respective element of 'from' (internal node)
1.517 +(2) the 't' ar given
1.518 +(2a) by 'to' if 't' = the respective element of 'to' (right margin)
1.519 +(2b) inifinity, if 't' < the respective element of 'to (internal node)'
1.520 +the 'f' and 't' are set by hdp,... *)
1.521 +fun get_trace pt p q =
1.522 + (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q)))
1.523 + (take_fromto (hdp p) (hdq q) (children pt));
1.524 +end;
1.525 +
1.526 +(*extract a formula or model from ctree for itms2itemppc or model2xml*)
1.527 +fun preconds2str bts =
1.528 + (strs2str o (map (linefeed o pair2str o
1.529 + (apsnd (UnparseC.term @{context})) o
1.530 + (apfst bool2str)))) bts;
1.531 +
1.532 +fun ocalhd2str (b, p, hdf, itms, prec, spec) =
1.533 + "(" ^ bool2str b ^ ", " ^ pos_2str p ^ ", " ^ UnparseC.term @{context} hdf ^
1.534 + ", " ^ "\<forall>itms2str itms\<forall>" (*Model_Def.itms2str_ (ThyC.id_to_ctxt "Isac_Knowledge") itms*) ^
1.535 + ", " ^ preconds2str prec ^ ", \n" ^ References_Def.to_string spec ^ " )";
1.536 +\<close>
1.537 +
1.538 +
1.539 +fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj
1.540 + | is_pblnd _ = raise ERROR "is_pblnd: uncovered fun def.";
1.541 +
1.542 +
1.543 +(* determine the previous pos' on the same level
1.544 + WN0502 made for interSteps; _only_ works for branch TransitiveB WN120517 compare lev_back *)
1.545 +fun lev_pred' _ ([], Res) = ([], Pbl)
1.546 + | lev_pred' pt (p, Res) =
1.547 + let val (p', last) = split_last p
1.548 + in
1.549 + if last = 1
1.550 + then if (is_pblobj o (get_obj I pt)) p then (p, Pbl) else (p, Frm)
1.551 + else if get_obj g_res pt (p' @ [last - 1]) = get_obj g_form pt p
1.552 + then (p' @ [last - 1], Res) (* TransitiveB *)
1.553 + else if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm)
1.554 + end
1.555 + | lev_pred' _ _ = raise ERROR "";
1.556 +
1.557 +
1.558 +(**.insert into ctree and cut branches accordingly.**)
1.559 +
1.560 +\<^isac_test>\<open>
1.561 +(* get all positions of certain intervals on the ctree.
1.562 + old VERSION without move_dn; kept for occasional redesign
1.563 + get all pos's to be cut in a ctree
1.564 + below a pos or from a ctree list after i-th element (NO level_up) *)
1.565 +fun get_allpos' (_, _) EmptyPtree = []
1.566 + | get_allpos' (p, 1) (Nd (b, bs)) = (* p is pos of Nd *)
1.567 + if g_ostate b = Incomplete
1.568 + then (p, Frm) :: (get_allpos's (p, 1) bs)
1.569 + else (p, Frm) :: (get_allpos's (p, 1) bs) @ [(p, Res)]
1.570 + | get_allpos' (p, _) (Nd (b, bs)) = (* p is pos of Nd *)
1.571 + if length bs > 0 orelse is_pblobj b
1.572 + then if g_ostate b = Incomplete
1.573 + then [(p,Frm)] @ (get_allpos's (p, 1) bs)
1.574 + else [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p, Res)]
1.575 + else if g_ostate b = Incomplete then [] else [(p, Res)]
1.576 +and get_allpos's _ [] = []
1.577 + | get_allpos's (p, i) (pt :: pts) = (* p is pos of parent-Nd *)
1.578 + (get_allpos' (p @ [i], i) pt) @ (get_allpos's (p, i + 1) pts);
1.579 +
1.580 +(*WN050106 like cut_level, but deletes exactly 1 node *)
1.581 +fun cut_level__ _ _ EmptyPtree _ =raise PTREE "cut_level__ Empty _" (* for tests ONLY *)
1.582 + | cut_level__ _ _ (Nd ( _, _)) ([], _) = raise PTREE "cut_level__ _ []"
1.583 + | cut_level__ cuts P (Nd (b, bs)) (p :: [], p_) =
1.584 + if test_trans b
1.585 + then
1.586 + (Nd (b, drop_nth [] (p:Pos.posel, bs)),
1.587 + cuts @ (if p_ = Frm then [(P @ [p], Res)] else []) @
1.588 + (get_allpos's (P, p + 1) (drop_nth [] (p, bs))))
1.589 + else (Nd (b, bs), cuts)
1.590 + | cut_level__ cuts P (Nd (b, bs)) ((p :: ps), p_) =
1.591 + let
1.592 + val (bs', cuts') = cut_level__ cuts P (nth p bs) (ps, p_)
1.593 + in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
1.594 +
1.595 +fun cut_level _ _ EmptyPtree _ = raise PTREE "cut_level EmptyPtree _"
1.596 + | cut_level _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level _ []"
1.597 + | cut_level cuts P (Nd (b, bs)) (p :: [], p_) =
1.598 + if test_trans b
1.599 + then
1.600 + (Nd (b, take (p:Pos.posel, bs)),
1.601 + cuts @
1.602 + (if p_ = Frm andalso (*#*) g_ostate b = Complete then [(P@[p],Res)] else ([]:pos' list)) @
1.603 + (get_allpos's (P, p+1) (takerest (p, bs))))
1.604 + else (Nd (b, bs), cuts)
1.605 + | cut_level cuts P (Nd (b, bs)) ((p :: ps), p_) =
1.606 + let
1.607 + val (bs', cuts') = cut_level cuts P (nth p bs) (ps, p_)
1.608 + in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
1.609 +
1.610 +
1.611 +(*old version before WN050219, overwritten below*)
1.612 +fun cut_tree _ ([], _) = raise PTREE "cut_tree _ ([],_)"
1.613 + | cut_tree pt (pos as ([_], _)) =
1.614 + let
1.615 + val (pt', cuts) = cut_level [] [] pt pos
1.616 + in
1.617 + (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete then [] else [([], Res)]))
1.618 + end
1.619 + | cut_tree pt (p,p_) =
1.620 + let
1.621 + fun cutfn pt cuts (p, p_) =
1.622 + let
1.623 + val (pt', cuts') = cut_level [] (lev_up p) pt (p,p_)
1.624 + in
1.625 + if length cuts' > 0 andalso length p > 1
1.626 + then cutfn pt' (cuts @ cuts') (lev_up p, Frm(*-->(p,Res)*))
1.627 + else (pt', cuts @ cuts')
1.628 + end
1.629 + val (pt', cuts) = cutfn pt [] (p, p_)
1.630 + in
1.631 + (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete then [] else [([], Res)]))
1.632 + end;
1.633 +\<close>
1.634 +
1.635 +local
1.636 +fun move_dn _ (Nd (_, ns)) ([],p_) = (* root problem *)
1.637 + (case p_ of
1.638 + Res => raise PTREE "move_dn: end of calculation"
1.639 + | _ =>
1.640 + if null ns (* go down from Pbl + Met *)
1.641 + then raise PTREE "move_dn: solve problem not started"
1.642 + else ([1], Frm))
1.643 + | move_dn P (Nd (_, ns)) (p :: (ps as (_ :: _)), p_) = (* iterate to end of pos *)
1.644 + if p > length ns
1.645 + then raise PTREE "move_dn: pos not existent 2"
1.646 + else move_dn (P @ [p]) (nth p ns) (ps, p_)
1.647 + | move_dn P (Nd (c, ns)) ([p], p_) = (* act on last element of pos *)
1.648 + if p > length ns
1.649 + then raise PTREE "move_dn: pos not existent 3"
1.650 + else
1.651 + (case p_ of
1.652 + Res =>
1.653 + if p = length ns (* last Res on this level: go a level up *)
1.654 + then if g_ostate c = Complete
1.655 + then (P, Res)
1.656 + else raise PTREE (ints2str' P ^ " not complete 1")
1.657 + else (* go to the next Nd on this level, or down into the next Nd *)
1.658 + if is_pblnd (nth (p + 1) ns) then (P@[p + 1], Pbl)
1.659 + else if g_res' (nth p ns) = g_form' (nth (p + 1) ns)
1.660 + then if (null o children o (nth (p + 1))) ns
1.661 + then (* take the Res if Complete *)
1.662 + if g_ostate' (nth (p + 1) ns) = Complete
1.663 + then (P@[p + 1], Res)
1.664 + else raise PTREE (ints2str' (P@[p + 1]) ^ " not complete 2")
1.665 + else (P@[p + 1, 1], Frm) (* go down into the next PrfObj *)
1.666 + else (P@[p + 1], Frm) (* take Frm: exists if the Nd exists *)
1.667 + | Frm => (*go down or to the Res of this Nd*)
1.668 + if (null o children o (nth p)) ns
1.669 + then if g_ostate' (nth p ns) = Complete then (P @ [p], Res)
1.670 + else raise PTREE (ints2str' (P @ [p])^" not complete 3")
1.671 + else (P @ [p, 1], Frm)
1.672 + | _ => (* is Pbl or Met *)
1.673 + if (null o children o (nth p)) ns
1.674 + then raise PTREE "move_dn:solve subproblem not startd"
1.675 + else (P @ [p, 1],
1.676 + if (is_pblnd o hd o children o (nth p)) ns
1.677 + then Pbl else Frm))
1.678 + | move_dn _ _ _ = raise ERROR "";
1.679 +in
1.680 +(* get all positions in a ctree until ([],Res) or ostate=Incomplete
1.681 +val get_allp = fn :
1.682 + pos' list -> : accumulated, start with []
1.683 + pos -> : the offset for subtrees wrt the root
1.684 + ctree -> : (sub)tree
1.685 + pos' : initialization (the last pos' before ...)
1.686 + -> pos' list : of positions in this (sub) tree (relative to the root)
1.687 +*)
1.688 +fun get_allp cuts (P, pos) pt =
1.689 + (let
1.690 + val nxt = move_dn [] pt pos (*exn if Incomplete reached*)
1.691 + in
1.692 + if nxt <> ([], Res)
1.693 + then get_allp (cuts @ [nxt]) (P, nxt) pt
1.694 + else map (apfst (curry op @ P)) (cuts @ [nxt])
1.695 + end)
1.696 + handle PTREE _ => (map (apfst (curry op@ P)) cuts);
1.697 +end
1.698 +
1.699 +(* the pts are assumed to be on the same level *)
1.700 +fun get_allps cuts _ [] = cuts
1.701 + | get_allps cuts P (pt :: pts) =
1.702 + let
1.703 + val below = get_allp [] (P, ([], Frm)) pt
1.704 + val levfrm =
1.705 + if is_pblnd pt
1.706 + then (P, Pbl) :: below
1.707 + else if last_elem P = 1
1.708 + then (P, Frm) :: below
1.709 + else (*Trans*) below
1.710 + val levres = levfrm @ (if null below then [(P, Res)] else [])
1.711 + in
1.712 + get_allps (cuts @ levres) (lev_on P) pts
1.713 + end;
1.714 +
1.715 +(** these 2 funs decide on how far cut_tree goes **)
1.716 +(* shall the nodes _after_ the pos to be inserted at be deleted?
1.717 + shall cutting be continued on the higher level(s)? the Nd regarded will NOT be changed *)
1.718 +fun test_trans (PrfObj {branch, ...}) = (branch = TransitiveB orelse branch = NoBranch)
1.719 + | test_trans (PblObj {branch, ...}) = (branch = TransitiveB orelse branch = NoBranch);
1.720 +
1.721 +(* cut_bottom new sml603..608
1.722 +cut the level at the bottom of the pos (used by cappend_...)
1.723 +and handle the parent in order to avoid extra case for root
1.724 +fn: ctree -> : the _whole_ ctree for cut_levup
1.725 + pos * Pos.posel -> : the pos after split_last
1.726 + ctree -> : the parent of the Nd to be cut
1.727 +return
1.728 + (ctree * : the updated ctree
1.729 + pos' list) * : the pos's cut
1.730 + bool : cutting shall be continued on the higher level(s)
1.731 +*)
1.732 +fun cut_bottom _ (pt' as Nd (b, [])) = ((pt', []), test_trans b)
1.733 + | cut_bottom (P, p) (Nd (b, bs)) =
1.734 + let (*divide level into 3 parts...*)
1.735 + val keep = take (p - 1, bs)
1.736 + val pt' = case nth p bs of
1.737 + pt' as Nd _ => pt'
1.738 + | _ => raise ERROR "cut_bottom: uncovered case nth p bs"
1.739 + (*^^^^^_here_ will be 'insert_pt'ed by 'append_..'*)
1.740 + val (tail, _) = (takerest (p, bs), if null (takerest (p, bs)) then 0 else p + 1)
1.741 + val (children, cuts) =
1.742 + if test_trans b
1.743 + then
1.744 + (keep, (if is_pblnd pt' then [(P @ [p], Pbl)] else [])
1.745 + @ (get_allp [] (P @ [p], (P, Frm)) pt')
1.746 + @ (get_allps [] (P @ [p + 1]) tail))
1.747 + else (keep @ [(*'insert_pt'ed by 'append_..'*)] @ tail,
1.748 + get_allp [] (P @ [p], (P, Frm)) pt')
1.749 + val (pt'', cuts) =
1.750 + if test_trans b
1.751 + then (Nd (del_res b, children), cuts @ (if g_ostate b = Incomplete then [] else [(P, Res)]))
1.752 + else (Nd (b, children), cuts)
1.753 + in ((pt'', cuts), test_trans b) end
1.754 + | cut_bottom _ _ = raise ERROR "cut_bottom: uncovered fun def.";
1.755 +
1.756 +
1.757 +(* go all levels from the bottom of 'pos' up to the root,
1.758 + on each level compose the children of a node and accumulate the cut Nds
1.759 +args
1.760 + pos' list -> : for accumulation
1.761 + bool -> : cutting shall be continued on the higher level(s)
1.762 + ctree -> : the whole ctree for 'get_nd pt P' on each level
1.763 + ctree -> : the Nd from the lower level for insertion at path
1.764 + pos * Pos.posel -> : pos=path split for convenience
1.765 + ctree -> : Nd the children of are under consideration on this call
1.766 +returns :
1.767 + ctree * pos' list : the updated parent-Nd and the pos's of the Nds cut
1.768 +*)
1.769 +fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:Pos.posel) (Nd (b, bs)) =
1.770 + let (*divide level into 3 parts...*)
1.771 + val keep = take (p - 1, bs)
1.772 + (*val pt' comes as argument from below*)
1.773 + val (tail, _) =
1.774 + (takerest (p, bs), if null (takerest (p, bs)) then 0 else p + 1)
1.775 + val (children, cuts') =
1.776 + if clevup
1.777 + then (keep @ [pt'], get_allps [] (P @ [p+1]) tail)
1.778 + else (keep @ [pt'] @ tail, [])
1.779 + val clevup' = if clevup then test_trans b else false
1.780 + (*the first Nd with false stops cutting on all levels above*)
1.781 + val (pt'', cuts') =
1.782 + if clevup'
1.783 + then (Nd (del_res b, children), cuts' @ (if g_ostate b = Incomplete then [] else [(P, Res)]))
1.784 + else (Nd (b, children), cuts')
1.785 + in
1.786 + if null P
1.787 + then (pt'', cuts @ cuts')
1.788 + else
1.789 + let val (P, p) = split_last P
1.790 + in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P) end
1.791 + end
1.792 + | cut_levup _ _ _ _ _ _ = raise ERROR "cut_levup: uncovered fun def.";
1.793 +
1.794 +(* cut nodes after and below an inserted node in the ctree;
1.795 + the cuts range is limited by the predicate 'fun cutlevup' *)
1.796 +fun cut_tree pt (pos, _) =
1.797 + if not (existpt pos pt)
1.798 + then (pt, []) (*appending a formula never cuts anything*)
1.799 + else
1.800 + let
1.801 + val (P, p) = split_last pos
1.802 + val ((pt', cuts), clevup) = cut_bottom (P, p) (get_nd pt P)
1.803 + (* pt' is the updated parent of the Nd to cappend_..*)
1.804 + in
1.805 + if null P
1.806 + then (pt', cuts)
1.807 + else
1.808 + let val (P, p) = split_last P
1.809 + in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P) end
1.810 + end;
1.811 +
1.812 +(* get the theory explicitly just for the rootpbl;
1.813 + thus use this function _after_ finishing specification *)
1.814 +fun root_thy (Nd (PblObj {spec = (thyID, _, _), ctxt, ...}, _)) = ThyC.get_theory ctxt thyID
1.815 + | root_thy _ = raise ERROR "root_thy: uncovered fun def.";
1.816 +
1.817 +(**)
1.818 +end;
1.819 +(**)