1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Mon Dec 11 12:14:28 2023 +0100
1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Mon Dec 11 16:12:53 2023 +0100
1.3 @@ -4,7 +4,7 @@
1.4 Outer syntax for Isabelle/Isac's Calculation interactive via Isabelle/PIDE.
1.5 Second trial following Makarius' definition of "problem" already existing in this repository.
1.6 *)
1.7 -
1.8 +
1.9 theory Calculation
1.10 imports E_Collect "$ISABELLE_ISAC/Knowledge/Build_Thydata"
1.11 keywords "Example" :: thy_decl
2.1 --- a/src/Tools/isac/Build_Isac.thy Mon Dec 11 12:14:28 2023 +0100
2.2 +++ b/src/Tools/isac/Build_Isac.thy Mon Dec 11 16:12:53 2023 +0100
2.3 @@ -269,19 +269,7 @@
2.4 subsection \<open>(5) Adopt Isabelle/jEdit for Isac\<close>
2.5
2.6 ML \<open>
2.7 -\<close> text \<open>
2.8 -I_Model.T_POS
2.9 \<close> ML \<open>
2.10 -I_Model.TEST_to_OLD ;
2.11 -I_Model.TEST_to_OLD_single ;
2.12 -I_Model.feedback_POS_to_OLD ;
2.13 -
2.14 -I_Model.OLD_to_POS ;
2.15 -I_Model.OLD_to_POS_single ;
2.16 -I_Model.feedback_OLD_to_POS ;
2.17 -(*OLD*)
2.18 -(*---*)
2.19 -(*NEW*)
2.20 \<close> ML \<open>
2.21 \<close>
2.22 end
3.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic-TEST.sml Mon Dec 11 12:14:28 2023 +0100
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,816 +0,0 @@
3.4 -(* Title: the calctree, which holds a calculation
3.5 - Author: Walther Neuper 1999
3.6 - (c) due to copyright terms
3.7 -
3.8 -Definitions required for Ctree, renamed later appropriately
3.9 --------------------------vvvvv + I_Model.T-TEST are the only difference to
3.10 - BASIC_CALC_TREE
3.11 -*)
3.12 -
3.13 -signature BASIC_CALC_TREE_POS =
3.14 -sig
3.15 -(**** signature ****)
3.16 -(** the basic datatype **)
3.17 - type state
3.18 - val e_state: state
3.19 -
3.20 - type con
3.21 - eqtype cellID
3.22 -
3.23 - datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB
3.24 - datatype ostate = Complete | Incomplete | Inconsistent
3.25 - type specify_data
3.26 - type solve_data
3.27 - datatype ppobj = PblObj of specify_data | PrfObj of solve_data
3.28 - datatype ctree = EmptyPtree | Nd of ppobj * ctree list
3.29 -
3.30 - val rep_solve_data: ppobj -> solve_data
3.31 - val rep_specify_data: ppobj -> specify_data
3.32 -
3.33 -(** basic functions **)
3.34 - val e_ctree : ctree (* TODO: replace by EmptyPtree*)
3.35 - val existpt' : Pos.pos' -> ctree -> bool
3.36 - val is_interpos : Pos.pos' -> bool
3.37 - val lev_pred' : ctree -> Pos.pos' -> Pos.pos'
3.38 - val ins_chn : ctree list -> ctree -> Pos.pos -> ctree
3.39 - val children : ctree -> ctree list
3.40 - val get_nd : ctree -> Pos.pos -> ctree
3.41 - val just_created_ : ppobj -> bool
3.42 - val just_created : state -> bool
3.43 - val e_origin : Model_Def.o_model * References_Def.T * term
3.44 -
3.45 - val is_pblobj : ppobj -> bool
3.46 - val is_pblobj' : ctree -> Pos.pos -> bool
3.47 - val is_pblnd : ctree -> bool
3.48 -
3.49 - val g_spec : ppobj -> References_Def.T
3.50 - val g_loc : ppobj -> (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option
3.51 - val g_form : ppobj -> term
3.52 - val g_pbl : ppobj -> Model_Def.i_model_POS
3.53 - val g_met : ppobj -> Model_Def.i_model_POS
3.54 - val g_metID : ppobj -> MethodC.id
3.55 - val g_result : ppobj -> Celem.result
3.56 - val g_tac : ppobj -> Tactic.input
3.57 - val g_domID : ppobj -> ThyC.id
3.58 -
3.59 - val g_origin : ppobj -> Model_Def.o_model * References_Def.T * term
3.60 - val get_loc : ctree -> Pos.pos' -> Istate_Def.T * Proof.context
3.61 - val get_istate_LI : ctree -> Pos.pos' -> Istate_Def.T
3.62 - val get_ctxt_LI: ctree -> Pos.pos' -> Proof.context
3.63 - val get_ctxt : ctree -> Pos.pos' -> Proof.context (*DEPRECATED*)
3.64 - val get_obj : (ppobj -> 'a) -> ctree -> Pos.pos -> 'a
3.65 - val get_curr_formula : state -> term
3.66 - val get_assumptions : ctree -> Pos.pos' -> term list
3.67 -
3.68 - val new_val : term -> Istate_Def.T -> Istate_Def.T
3.69 -
3.70 - type cid = cellID list
3.71 - datatype ptform = Form of term | ModSpec of Specification_Def.T
3.72 - val get_somespec' : References_Def.T -> References_Def.T -> References_Def.T
3.73 - exception PTREE of string;
3.74 -
3.75 - val root_thy : ctree -> theory
3.76 -(* ---- made visible ONLY for structure CTaccess : CALC_TREE_ACCESS --------------------------- *)
3.77 - val appl_obj : (ppobj -> ppobj) -> ctree -> Pos.pos -> ctree
3.78 - val existpt : Pos.pos -> ctree -> bool
3.79 - val cut_tree : ctree -> Pos.pos * 'a -> ctree * Pos.pos' list
3.80 - val insert_pt : ppobj -> ctree -> int list -> ctree
3.81 -(* ---- made visible ONLY for structure CTnavi : CALC_TREE_NAVIGATION ------------------------- *)
3.82 - val g_branch : ppobj -> branch
3.83 - val g_form' : ctree -> term
3.84 - val g_ostate : ppobj -> ostate
3.85 - val g_ostate' : ctree -> ostate
3.86 - val g_res : ppobj -> term
3.87 - val g_res' : ctree -> term
3.88 -(*/---- duplicates in CTnavi, reconsider structs -----------------------------------------------
3.89 - val lev_dn : CTbasic.Pos.pos -> Pos.pos (* duplicate in ctree-navi.sml *)
3.90 - val par_pblobj : CTbasic.ctree -> Pos.pos -> Pos.pos (* duplicate in ctree-navi.sml *)
3.91 - ---- duplicates in CTnavi, reconsider structs ----------------------------------------------/*)
3.92 -(*from isac_test for Minisubpbl*)
3.93 - val pr_ctree: Proof.context -> (Proof.context -> int list -> ppobj -> string) -> ctree -> string
3.94 - val pr_short: Proof.context -> Pos.pos -> ppobj -> string
3.95 -
3.96 -\<^isac_test>\<open>
3.97 - val g_ctxt : ppobj -> Proof.context
3.98 - val g_fmz : ppobj -> Model_Def.form_T
3.99 - val get_allp : Pos.pos' list -> Pos.pos * (int list * Pos.pos_) -> ctree -> Pos.pos' list
3.100 - val get_allps : (Pos.pos * Pos.pos_) list -> Pos.posel list -> ctree list -> Pos.pos' list
3.101 - val get_allpos' : Pos.pos * Pos.posel -> ctree -> Pos.pos' list
3.102 - val get_allpos's : Pos.pos * Pos.posel -> ctree list -> (Pos.pos * Pos.pos_) list
3.103 - val cut_bottom : Pos.pos * Pos.posel -> ctree -> (ctree * Pos.pos' list) * bool
3.104 - val cut_level : Pos.pos' list -> Pos.pos -> ctree -> int list * Pos.pos_ -> ctree * Pos.pos' list
3.105 - val cut_level__ : Pos.pos' list -> Pos.pos -> ctree -> int list * Pos.pos_ -> ctree * Pos.pos' list
3.106 - val get_trace : ctree -> int list -> int list -> int list list
3.107 - val branch2str : branch -> string
3.108 -\<close>
3.109 -end
3.110 -
3.111 -(**)
3.112 -structure CTbasic_POS(**): BASIC_CALC_TREE_POS(**) =
3.113 -struct
3.114 -(**)
3.115 -open Pos
3.116 -
3.117 -(**** Ctree ****)
3.118 -
3.119 -(*** general types* **)
3.120 -
3.121 -datatype branch =
3.122 - NoBranch | AndB | OrB
3.123 -| TransitiveB (* FIXXXME.0308: set branch from met in Apply_Method
3.124 - FIXXXME.0402: -"- in Begin_Trans'*)
3.125 -| SequenceB | IntersectB | CollectB | MapB;
3.126 -
3.127 -\<^isac_test>\<open>
3.128 -fun branch2str NoBranch = "NoBranch"
3.129 - | branch2str AndB = "AndB"
3.130 - | branch2str OrB = "OrB"
3.131 - | branch2str TransitiveB = "TransitiveB"
3.132 - | branch2str SequenceB = "SequenceB"
3.133 - | branch2str IntersectB = "IntersectB"
3.134 - | branch2str CollectB = "CollectB"
3.135 - | branch2str MapB = "MapB";
3.136 -\<close>
3.137 -
3.138 -datatype ostate =
3.139 - Incomplete | Complete | Inconsistent (* WN041020 latter still unused *);
3.140 -\<^isac_test>\<open>
3.141 -fun ostate2str Incomplete = "Incomplete"
3.142 - | ostate2str Complete = "Complete"
3.143 - | ostate2str Inconsistent = "Inconsistent";
3.144 -\<close>
3.145 -
3.146 -type cellID = int;
3.147 -type cid = cellID list;
3.148 -
3.149 -
3.150 -type iist = Istate_Def.T option * Istate_Def.T option;
3.151 -(*val e_iist = (empty, empty); --- sinnlos f"ur NICHT-equality-type*)
3.152 -
3.153 -
3.154 -fun new_val v (Istate_Def.Pstate pst) =
3.155 - (Istate_Def.Pstate (Istate_Def.set_act v pst))
3.156 - | new_val _ _ = raise ERROR "new_val: only for Pstate";
3.157 -
3.158 -datatype con = land | lor;
3.159 -
3.160 -(* executed tactics (tac_s) with local environment etc.;
3.161 - used for continuing eval script + for generate *)
3.162 -type ets =
3.163 - (TermC.path *(* of tactic in program, tactic (weakly) associated with tac_ *)
3.164 - (Tactic.T * (* (for generate) *)
3.165 - Env.T * (* with 'tactic=result' as rule, tactic ev. _not_ ready for 'parallel let' *)
3.166 - Env.T * (* with results of (ready) tacs *)
3.167 - term * (* itr_arg of tactic, for upd. env at Repeat, Try *)
3.168 - term * (* result value of the tac *)
3.169 - Celem.safe))
3.170 - list;
3.171 -
3.172 -type envp =(*9.5.03: unused, delete with field in ctree.PblObj FIXXXME*)
3.173 - (int * term list) list * (* assoc-list: args of met*)
3.174 - (int * Rule_Set.T) list * (* assoc-list: tacs already done ///15.9.00*)
3.175 - (int * ets) list * (* assoc-list: tacs etc. already done*)
3.176 - (string * pos) list; (* asms * from where*)
3.177 -
3.178 -
3.179 -(*** type Ctree ***)
3.180 -
3.181 -type specify_data =
3.182 - {fmz : Model_Def.form_T, (* for uniformity also created/used for/by Subproblem *)
3.183 - origin: (Model_Def.o_model) *(* = O_Model.T for efficiently checking input to I_Model *)
3.184 - References_Def.T * (* updated by Refine_Tacitly *)
3.185 - term, (* headline of calc-head, as calculated initially(!) *)
3.186 - spec : References_Def.T, (* explicitly input *)
3.187 - probl : Model_Def.i_model_POS,(* = I_Model.T for interactive input to a Problem *)
3.188 - meth : Model_Def.i_model_POS,(* = I_Model.T for interactive input to a MethodC *)
3.189 - ctxt : Proof.context, (* used while specifying this (Sub-)Problem and MethodC *)
3.190 - loc : (Istate_Def.T * Proof.context) option (* like in PrfObj, calling this SubProblem *)
3.191 - * (Istate_Def.T * Proof.context) option, (* like in PrfObj, finishing the SubProblem *)
3.192 - branch: branch, (* like PrfObj *)
3.193 - result: Celem.result, (* like PrfObj *)
3.194 - ostate: ostate}; (* like PrfObj *)
3.195 -type solve_data = (* TODO: arrange according to signature *)
3.196 - {form : term, (* where tactic is applied to *)
3.197 - tac : Tactic.input, (* tactic as presented to users *)
3.198 - loc : (Istate_Def.T * (* program interpreter state *)
3.199 - Proof.context) (* context for provers, type inference *)
3.200 - option * (* both for interpreter location on Frm, Pbl, Met *)
3.201 - (Istate_Def.T * (* script interpreter state *)
3.202 - Proof.context) (* context for provers, type inference *)
3.203 - option, (* both for interpreter location on Res, (NONE,NONE) == empty *)
3.204 - branch: branch, (* only rudimentary *)
3.205 - result: Celem.result, (* result and assumptions *)
3.206 - ostate: ostate} (* Complete <=> result is OK *)
3.207 -
3.208 -datatype ppobj =
3.209 - PblObj of specify_data (* data serving a whole specification-phase *)
3.210 -| PrfObj of solve_data; (* data for a proof step triggered by a tactic *)
3.211 -
3.212 -(* this tree contains isac's calculations;
3.213 - the tree's structure has been copied from an early version of Theorema(c);
3.214 - it has the disadvantage, that there is no space
3.215 - for the first tactic in a script generating the first formula at (p,Frm);
3.216 - this trouble has been covered by 'implicit_take' and 'Take' so far,
3.217 - but it is crucial if the first tactic in a script is eg. 'Subproblem';
3.218 - see 'type tac', Apply_Method.
3.219 -*)
3.220 -datatype ctree =
3.221 - EmptyPtree
3.222 -| Nd of ppobj * (ctree list);
3.223 -val e_ctree = EmptyPtree;
3.224 -type state = ctree * pos'
3.225 -val e_state = (EmptyPtree , e_pos')
3.226 -
3.227 -fun rep_solve_data (PrfObj solve_data) = solve_data
3.228 - | rep_solve_data _ = raise ERROR "rep_solve_data ONLY for solve_data"
3.229 -fun rep_specify_data (PblObj specify_data) = specify_data
3.230 - | rep_specify_data _ = raise ERROR "rep_solve_data ONLY for solve_data"
3.231 -
3.232 -
3.233 -(*** minimal set of functions on Ctree* **)
3.234 -
3.235 -fun is_pblobj (PblObj _) = true
3.236 - | is_pblobj _ = false;
3.237 -
3.238 -exception PTREE of string;
3.239 -fun nth _ [] = raise PTREE "nth _ []"
3.240 - | nth 1 (x :: _) = x
3.241 - | nth n (_ :: xs) = nth (n - 1) xs;
3.242 -(*> nth 2 [11,22,33]; -->> val it = 22 : int*)
3.243 -
3.244 -
3.245 -(** convert ctree to a string **)
3.246 -
3.247 -(* convert a pos from list to string *)
3.248 -fun pr_pos ps = (space_implode "." (map string_of_int ps)) ^ ". ";
3.249 -(* show hd origin or form only *)
3.250 -(**)
3.251 -fun pr_short _ p (PblObj _) = pr_pos p ^ " ----- pblobj -----\n"
3.252 - | pr_short ctxt p (PrfObj {form = form, ...}) = pr_pos p ^ UnparseC.term ctxt form ^ "\n";
3.253 -fun pr_ctree ctxt f pt =
3.254 - let
3.255 - fun pr_pt _ _ EmptyPtree = ""
3.256 - | pr_pt pfn ps (Nd (b, [])) = pfn ps b
3.257 - | pr_pt pfn ps (Nd (b, ts)) = pfn ps b ^ prts pfn ps 1 ts
3.258 - and prts _ _ _ [] = ""
3.259 - | prts pfn ps p (t :: ts) = (pr_pt pfn (ps @ [p]) t)^
3.260 - (prts pfn ps (p + 1) ts)
3.261 - in pr_pt (f ctxt) [] pt end;
3.262 -
3.263 -
3.264 -
3.265 -(** access the branches of ctree **)
3.266 -
3.267 -fun repl [] _ _ = raise PTREE "repl [] _ _"
3.268 - | repl (_ :: ls) 1 e = e :: ls
3.269 - | repl (l :: ls) n e = l :: (repl ls (n-1) e);
3.270 -fun repl_app ls n e =
3.271 - let
3.272 - val lim = 1 + length ls
3.273 - in
3.274 - if n > lim
3.275 - then raise PTREE "repl_app: n > lim"
3.276 - else if n = lim
3.277 - then ls @ [e]
3.278 - else repl ls n e end;
3.279 -
3.280 -(* get from obj at pos by f : ppobj -> 'a *)
3.281 -fun get_obj _ EmptyPtree _ = raise PTREE "get_obj f EmptyPtree"
3.282 - | get_obj f (Nd (b, _)) [] = f b
3.283 - | get_obj f (Nd (_, bs)) (p :: ps) =
3.284 - case \<^try>\<open> get_obj f (nth p bs) ps \<close> of
3.285 - SOME obj => obj
3.286 - | NONE => raise PTREE ("get_obj: pos = " ^ ints2str' (p :: ps) ^ " does not exist");
3.287 -fun get_nd EmptyPtree _ = raise PTREE "get_nd EmptyPtree"
3.288 - | get_nd n [] = n
3.289 - | get_nd (Nd (_, nds)) (pos as p :: ps) =
3.290 - case \<^try>\<open> get_nd (nth p nds) ps \<close> of
3.291 - SOME nd => nd
3.292 - | NONE => raise PTREE ("get_nd: not existent pos = " ^ ints2str' pos);
3.293 -
3.294 -(* for use by get_obj *)
3.295 -fun g_form (PrfObj {form = f,...}) = f
3.296 - | g_form (PblObj {origin= (_,_,f),...}) = f;
3.297 -fun g_form' (Nd (PrfObj {form = f, ...}, _)) = f
3.298 - | g_form' (Nd (PblObj {origin= (_, _, f),...}, _)) = f
3.299 - | g_form' _ = raise ERROR "g_form': uncovered fun def.";
3.300 -(* | g_form _ = raise PTREE "g_form not for PblObj";*)
3.301 -fun g_origin (PblObj {origin = ori, ...}) = ori
3.302 - | g_origin _ = raise PTREE "g_origin not for PrfObj";
3.303 -\<^isac_test>\<open>
3.304 -fun g_fmz (PblObj {fmz = f, ...}) = f
3.305 - | g_fmz _ = raise PTREE "g_fmz not for PrfObj";
3.306 -\<close>
3.307 -fun g_spec (PblObj {spec = s, ...}) = s
3.308 - | g_spec _ = raise PTREE "g_spec not for PrfObj";
3.309 -fun g_pbl (PblObj {probl = p, ...}) = p
3.310 - | g_pbl _ = raise PTREE "g_pbl not for PrfObj";
3.311 -fun g_met (PblObj {meth = p, ...}) = p
3.312 - | g_met _ = raise PTREE "g_met not for PrfObj";
3.313 -fun g_domID (PblObj {spec = (d, _, _), ...}) = d
3.314 - | g_domID _ = raise PTREE "g_metID not for PrfObj";
3.315 -fun g_metID (PblObj {spec = (_, _, m), ...}) = m
3.316 - | g_metID _ = raise PTREE "g_metID not for PrfObj";
3.317 -fun g_ctxt (PblObj {ctxt, ...}) = ctxt
3.318 - | g_ctxt _ = raise PTREE "g_ctxt not for PrfObj";
3.319 -fun g_loc (PblObj {loc = l, ...}) = l
3.320 - | g_loc (PrfObj {loc = l, ...}) = l;
3.321 -fun g_branch (PblObj {branch = b, ...}) = b
3.322 - | g_branch (PrfObj {branch = b, ...}) = b;
3.323 -fun g_tac (PblObj {spec = (_, _, m),...}) = Tactic.Apply_Method m
3.324 - | g_tac (PrfObj {tac = m, ...}) = m;
3.325 -fun g_result (PblObj {result = r, ...}) = r
3.326 - | g_result (PrfObj {result = r, ...}) = r;
3.327 -fun g_res (PblObj {result = (r, _) ,...}) = r
3.328 - | g_res (PrfObj {result = (r, _),...}) = r;
3.329 -fun g_res' (Nd (PblObj {result = (r, _), ...}, _)) = r
3.330 - | g_res' (Nd (PrfObj {result = (r, _),...}, _)) = r
3.331 - | g_res' _ = raise PTREE "g_res': uncovered fun def.";
3.332 -fun g_ostate (PblObj {ostate = r, ...}) = r
3.333 - | g_ostate (PrfObj {ostate = r, ...}) = r;
3.334 -fun g_ostate' (Nd (PblObj {ostate = r, ...}, _)) = r
3.335 - | g_ostate' (Nd (PrfObj {ostate = r, ...}, _)) = r
3.336 - | g_ostate' _ = raise PTREE "g_ostate': uncovered fun def.";
3.337 -
3.338 -(* get the formula preceeding the current position in a calculation *)
3.339 -fun get_curr_formula (pt, (p, p_)) =
3.340 - case p_ of
3.341 - Frm => get_obj g_form pt p
3.342 - | Res => (fst o (get_obj g_result pt)) p
3.343 - | _ => #3 (get_obj g_origin pt p); (* the headline*)
3.344 -
3.345 -(* in CalcTree/Subproblem an 'just_created_' model is created;
3.346 - this is filled to 'untouched' by Model/Refine_Problem *)
3.347 -fun just_created_ (PblObj {meth, probl, spec, ...}) =
3.348 - null meth andalso null probl andalso spec = References_Def.empty
3.349 - | just_created_ _ = raise PTREE "g_ostate': uncovered fun def.";
3.350 -val e_origin = ([], References_Def.empty, TermC.empty);
3.351 -
3.352 -fun just_created (pt, (p, _)) =
3.353 - let val ppobj = get_obj I pt p
3.354 - in is_pblobj ppobj andalso just_created_ ppobj end;
3.355 -
3.356 -(* does the pos in the ctree exist ? *)
3.357 -fun existpt pos pt = can (get_obj I pt) pos;
3.358 -(* does the pos' in the ctree exist, ie. extra check for result in the node *)
3.359 -fun existpt' (p, p_) pt =
3.360 - if can (get_obj I pt) p
3.361 - then case p_ of
3.362 - Res => get_obj g_ostate pt p = Complete
3.363 - | _ => true
3.364 - else false;
3.365 -
3.366 -(* is this position appropriate for calculating intermediate steps? *)
3.367 -fun is_interpos (_, Res) = true
3.368 - | is_interpos _ = false;
3.369 -
3.370 -(* get the children of a node in ctree *)
3.371 -fun children (Nd (PblObj _, cn)) = cn
3.372 - | children (Nd (PrfObj _, cn)) = cn
3.373 - | children _ = raise ERROR "children: uncovered fun def.";
3.374 -
3.375 -(*/--------------- duplicates in ctree-navi.sml: required also here below ---------------\*)
3.376 -\<^isac_test>\<open>
3.377 -fun lev_up [] = raise PTREE "lev_up []"
3.378 - | lev_up p = (drop_last p):pos;
3.379 -(* find the position of the next parent which is a PblObj in ctree *)
3.380 -fun par_pblobj _ [] = []
3.381 - | par_pblobj pt p =
3.382 - let
3.383 - fun par _ [] = []
3.384 - | par pt p =
3.385 - if is_pblobj (get_obj I pt p)
3.386 - then p
3.387 - else par pt (lev_up p)
3.388 - in par pt (lev_up p) end;
3.389 -\<close>
3.390 -(*\--------------- duplicates in ctree-navi.sml: required also here below ---------------/*)
3.391 -
3.392 -(* insert obj b into ctree at pos, ev.overwriting this pos *)
3.393 -fun insert_pt b EmptyPtree [] = Nd (b, [])
3.394 - | insert_pt _ EmptyPtree _ = raise PTREE "insert_pt b Empty _"
3.395 - | insert_pt b _ [] = Nd (b, [])
3.396 - | insert_pt b (Nd (b', bs)) (p :: []) = Nd (b', repl_app bs p (Nd (b, [])))
3.397 - | insert_pt b (Nd (b', bs)) (p :: ps) = Nd (b', repl_app bs p (insert_pt b (nth p bs) ps));
3.398 -
3.399 -(* insert children to a node without children. compare: fun insert_pt *)
3.400 -fun ins_chn _ EmptyPtree _ = raise PTREE "ins_chn: EmptyPtree"
3.401 - | ins_chn _ (Nd _) [] = raise PTREE "ins_chn: pos = []"
3.402 - | ins_chn ns (Nd (b, bs)) (p :: []) =
3.403 - if p > length bs
3.404 - then raise PTREE "ins_chn: pos not existent"
3.405 - else
3.406 - let
3.407 - val (b', bs') = case nth p bs of
3.408 - Nd (b', bs') => (b', bs')
3.409 - | _ => raise ERROR "ins_chn: uncovered case nth"
3.410 - in
3.411 - if null bs'
3.412 - then Nd (b, repl_app bs p (Nd (b', ns)))
3.413 - else raise PTREE "ins_chn: pos mustNOT be overwritten"
3.414 - end
3.415 - | ins_chn ns (Nd (b, bs)) (p::ps) = Nd (b, repl_app bs p (ins_chn ns (nth p bs) ps));
3.416 -
3.417 -(* apply f to obj at pos, f: ppobj -> ppobj *)
3.418 -fun appl_to_node f (Nd (b, bs)) = Nd (f b, bs)
3.419 - | appl_to_node _ _ = raise ERROR "appl_to_node: uncovered fun def.";
3.420 -fun appl_obj _ EmptyPtree [] = EmptyPtree
3.421 - | appl_obj _ EmptyPtree _ = raise PTREE "appl_obj f Empty _"
3.422 - | appl_obj f (Nd (b, bs)) [] = Nd (f b, bs)
3.423 - | appl_obj f (Nd (b, bs)) (p :: []) = Nd (b, repl_app bs p (((appl_to_node f) o (nth p)) bs))
3.424 - | appl_obj f (Nd (b, bs)) (p :: ps) = Nd (b, repl_app bs p (appl_obj f (nth p bs) (ps:pos)));
3.425 -
3.426 -datatype ptform = Form of term | ModSpec of Specification_Def.T;
3.427 -
3.428 -\<^isac_test>\<open>
3.429 -fun test_trans (PrfObj {branch, ...}) = true andalso branch = TransitiveB
3.430 - | test_trans (PblObj {branch, ...}) = true andalso branch = TransitiveB;
3.431 -\<close>
3.432 -
3.433 -fun is_pblobj' pt p =
3.434 - let val ppobj = get_obj I pt p
3.435 - in is_pblobj ppobj end;
3.436 -
3.437 -fun del_res (PblObj {fmz, origin, spec, probl, meth, ctxt, loc = (l1, _), branch, ...}) =
3.438 - PblObj {fmz = fmz, origin = origin, spec = spec, probl = probl, meth = meth,
3.439 - ctxt = ctxt, loc= (l1, NONE), branch = branch,
3.440 - result = (TermC.empty, []), ostate = Incomplete}
3.441 - | del_res (PrfObj {form, tac, loc= (l1, _), branch, ...}) =
3.442 - PrfObj {form = form, tac = tac, loc = (l1, NONE), branch = branch,
3.443 - result = (TermC.empty, []), ostate = Incomplete};
3.444 -
3.445 -
3.446 -fun get_loc EmptyPtree _ = (Istate_Def.empty, ContextC.empty)
3.447 - | get_loc pt (p, Res) =
3.448 - (case get_obj g_loc pt p of
3.449 - (SOME ist_ctxt, NONE) => ist_ctxt
3.450 - | (NONE , NONE) => (Istate_Def.empty, ContextC.empty)
3.451 - | (_ , SOME ist_ctxt) => ist_ctxt)
3.452 - | get_loc pt (p, _) =
3.453 - (case get_obj g_loc pt p of
3.454 - (NONE , SOME ist_ctxt) => ist_ctxt (* 020813 too liberal? *)
3.455 - | (NONE , NONE) => (Istate_Def.empty, ContextC.empty)
3.456 - | (SOME ist_ctxt, _) => ist_ctxt);
3.457 -fun get_istate_LI pt p = get_loc pt p |> #1;
3.458 -fun get_ctxt_LI pt p = get_loc pt p |> #2;
3.459 -fun get_ctxt pt (pos as (p, p_)) =
3.460 - if member op = [Frm, Res] p_
3.461 - then get_loc pt pos |> #2 (*for program interpretation rely on fun get_loc*)
3.462 - else (*p = Pbl: for specify phase take ctxt from PblObj *)
3.463 - if (p |> get_obj g_origin pt |> LibraryC.fst3) = [] (*CAS-command ? *)
3.464 - then (Know_Store.get_via_last_thy "Isac_Knowledge"(*CAS-command unknown*)) |> Defs.global_context |> fst
3.465 - else get_obj g_ctxt pt p
3.466 -
3.467 -fun get_assumptions pt p = get_ctxt pt p |> ContextC.get_assumptions;
3.468 -
3.469 -fun get_somespec' (dI, pI, mI) (dI', pI', mI') =
3.470 - let
3.471 - val domID = if dI = ThyC.id_empty then dI' else dI
3.472 - val pblID = if pI = Problem.id_empty then pI' else pI
3.473 - val metID = if mI = MethodC.id_empty then mI' else mI
3.474 - in (domID, pblID, metID) end;
3.475 -
3.476 -(**.development for extracting an 'interval' from ptree.**)
3.477 -
3.478 -\<^isac_test>\<open>
3.479 -(*WN0510 version stopped in favour of get_interval with !!!move_dn, getFormulaeFromTo
3.480 - actually used (inefficient) version with move_dn: see modspec.sml*)
3.481 -local
3.482 -
3.483 -fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*)
3.484 -fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*)
3.485 -fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x;
3.486 -fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;
3.487 -
3.488 -fun getnd i (b,p) q (Nd (_, nds)) =
3.489 - (if i <= 0 then [[b]] else []) @
3.490 - (getnds (i-1) true (b@[hdp p], tlp p) (tlq q)
3.491 - (take_fromto (hdp p) (hdq q) nds))
3.492 - | getnd _ _ _ _ = raise ERROR "getnd: uncovered case in fun.def."
3.493 -and getnds _ _ _ _ [] = [] (*no children*)
3.494 - | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*)
3.495 -
3.496 - | getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*)
3.497 - (getnd i ( b, p ) [99999] n1) @
3.498 - (getnd ~99999 (lev_on b,[0]) q n2)
3.499 -
3.500 - | getnds i _ (b, _) q [n1, n2] = (*intern, r-margin*)
3.501 - (getnd i ( b,[0]) [99999] n1) @
3.502 - (getnd ~99999 (lev_on b,[0]) q n2)
3.503 -
3.504 - | getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*)
3.505 - (getnd i ( b, p ) [99999] nd) @
3.506 - (getnds ~99999 false (lev_on b,[0]) q nds)
3.507 -
3.508 - | getnds i _ (b, _) q (nd::(nds as _::_)) = (*intern, ...*)
3.509 - (getnd i ( b,[0]) [99999] nd) @
3.510 - (getnds ~99999 false (lev_on b,[0]) q nds);
3.511 -in
3.512 -(*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes
3.513 - where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
3.514 -(1) the 'f' are given
3.515 -(1a) by 'from' if 'f' = the respective element of 'from' (left margin)
3.516 -(1b) -inifinity, if 'f' > the respective element of 'from' (internal node)
3.517 -(2) the 't' ar given
3.518 -(2a) by 'to' if 't' = the respective element of 'to' (right margin)
3.519 -(2b) inifinity, if 't' < the respective element of 'to (internal node)'
3.520 -the 'f' and 't' are set by hdp,... *)
3.521 -fun get_trace pt p q =
3.522 - (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q)))
3.523 - (take_fromto (hdp p) (hdq q) (children pt));
3.524 -end;
3.525 -
3.526 -(*extract a formula or model from ctree for itms2itemppc or model2xml*)
3.527 -fun preconds2str bts =
3.528 - (strs2str o (map (linefeed o pair2str o
3.529 - (apsnd (UnparseC.term @{context})) o
3.530 - (apfst bool2str)))) bts;
3.531 -
3.532 -fun ocalhd2str (b, p, hdf, itms, prec, spec) =
3.533 - "(" ^ bool2str b ^ ", " ^ pos_2str p ^ ", " ^ UnparseC.term @{context} hdf ^
3.534 - ", " ^ "\<forall>itms2str itms\<forall>" (*Model_Def.itms2str_ (ThyC.id_to_ctxt "Isac_Knowledge") itms*) ^
3.535 - ", " ^ preconds2str prec ^ ", \n" ^ References_Def.to_string spec ^ " )";
3.536 -\<close>
3.537 -
3.538 -
3.539 -fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj
3.540 - | is_pblnd _ = raise ERROR "is_pblnd: uncovered fun def.";
3.541 -
3.542 -
3.543 -(* determine the previous pos' on the same level
3.544 - WN0502 made for interSteps; _only_ works for branch TransitiveB WN120517 compare lev_back *)
3.545 -fun lev_pred' _ ([], Res) = ([], Pbl)
3.546 - | lev_pred' pt (p, Res) =
3.547 - let val (p', last) = split_last p
3.548 - in
3.549 - if last = 1
3.550 - then if (is_pblobj o (get_obj I pt)) p then (p, Pbl) else (p, Frm)
3.551 - else if get_obj g_res pt (p' @ [last - 1]) = get_obj g_form pt p
3.552 - then (p' @ [last - 1], Res) (* TransitiveB *)
3.553 - else if (is_pblobj o (get_obj I pt)) p then (p,Pbl) else (p, Frm)
3.554 - end
3.555 - | lev_pred' _ _ = raise ERROR "";
3.556 -
3.557 -
3.558 -(**.insert into ctree and cut branches accordingly.**)
3.559 -
3.560 -\<^isac_test>\<open>
3.561 -(* get all positions of certain intervals on the ctree.
3.562 - old VERSION without move_dn; kept for occasional redesign
3.563 - get all pos's to be cut in a ctree
3.564 - below a pos or from a ctree list after i-th element (NO level_up) *)
3.565 -fun get_allpos' (_, _) EmptyPtree = []
3.566 - | get_allpos' (p, 1) (Nd (b, bs)) = (* p is pos of Nd *)
3.567 - if g_ostate b = Incomplete
3.568 - then (p, Frm) :: (get_allpos's (p, 1) bs)
3.569 - else (p, Frm) :: (get_allpos's (p, 1) bs) @ [(p, Res)]
3.570 - | get_allpos' (p, _) (Nd (b, bs)) = (* p is pos of Nd *)
3.571 - if length bs > 0 orelse is_pblobj b
3.572 - then if g_ostate b = Incomplete
3.573 - then [(p,Frm)] @ (get_allpos's (p, 1) bs)
3.574 - else [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p, Res)]
3.575 - else if g_ostate b = Incomplete then [] else [(p, Res)]
3.576 -and get_allpos's _ [] = []
3.577 - | get_allpos's (p, i) (pt :: pts) = (* p is pos of parent-Nd *)
3.578 - (get_allpos' (p @ [i], i) pt) @ (get_allpos's (p, i + 1) pts);
3.579 -
3.580 -(*WN050106 like cut_level, but deletes exactly 1 node *)
3.581 -fun cut_level__ _ _ EmptyPtree _ =raise PTREE "cut_level__ Empty _" (* for tests ONLY *)
3.582 - | cut_level__ _ _ (Nd ( _, _)) ([], _) = raise PTREE "cut_level__ _ []"
3.583 - | cut_level__ cuts P (Nd (b, bs)) (p :: [], p_) =
3.584 - if test_trans b
3.585 - then
3.586 - (Nd (b, drop_nth [] (p:Pos.posel, bs)),
3.587 - cuts @ (if p_ = Frm then [(P @ [p], Res)] else []) @
3.588 - (get_allpos's (P, p + 1) (drop_nth [] (p, bs))))
3.589 - else (Nd (b, bs), cuts)
3.590 - | cut_level__ cuts P (Nd (b, bs)) ((p :: ps), p_) =
3.591 - let
3.592 - val (bs', cuts') = cut_level__ cuts P (nth p bs) (ps, p_)
3.593 - in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
3.594 -
3.595 -fun cut_level _ _ EmptyPtree _ = raise PTREE "cut_level EmptyPtree _"
3.596 - | cut_level _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level _ []"
3.597 - | cut_level cuts P (Nd (b, bs)) (p :: [], p_) =
3.598 - if test_trans b
3.599 - then
3.600 - (Nd (b, take (p:Pos.posel, bs)),
3.601 - cuts @
3.602 - (if p_ = Frm andalso (*#*) g_ostate b = Complete then [(P@[p],Res)] else ([]:pos' list)) @
3.603 - (get_allpos's (P, p+1) (takerest (p, bs))))
3.604 - else (Nd (b, bs), cuts)
3.605 - | cut_level cuts P (Nd (b, bs)) ((p :: ps), p_) =
3.606 - let
3.607 - val (bs', cuts') = cut_level cuts P (nth p bs) (ps, p_)
3.608 - in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
3.609 -
3.610 -
3.611 -(*old version before WN050219, overwritten below*)
3.612 -fun cut_tree _ ([], _) = raise PTREE "cut_tree _ ([],_)"
3.613 - | cut_tree pt (pos as ([_], _)) =
3.614 - let
3.615 - val (pt', cuts) = cut_level [] [] pt pos
3.616 - in
3.617 - (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete then [] else [([], Res)]))
3.618 - end
3.619 - | cut_tree pt (p,p_) =
3.620 - let
3.621 - fun cutfn pt cuts (p, p_) =
3.622 - let
3.623 - val (pt', cuts') = cut_level [] (lev_up p) pt (p,p_)
3.624 - in
3.625 - if length cuts' > 0 andalso length p > 1
3.626 - then cutfn pt' (cuts @ cuts') (lev_up p, Frm(*-->(p,Res)*))
3.627 - else (pt', cuts @ cuts')
3.628 - end
3.629 - val (pt', cuts) = cutfn pt [] (p, p_)
3.630 - in
3.631 - (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete then [] else [([], Res)]))
3.632 - end;
3.633 -\<close>
3.634 -
3.635 -local
3.636 -fun move_dn _ (Nd (_, ns)) ([],p_) = (* root problem *)
3.637 - (case p_ of
3.638 - Res => raise PTREE "move_dn: end of calculation"
3.639 - | _ =>
3.640 - if null ns (* go down from Pbl + Met *)
3.641 - then raise PTREE "move_dn: solve problem not started"
3.642 - else ([1], Frm))
3.643 - | move_dn P (Nd (_, ns)) (p :: (ps as (_ :: _)), p_) = (* iterate to end of pos *)
3.644 - if p > length ns
3.645 - then raise PTREE "move_dn: pos not existent 2"
3.646 - else move_dn (P @ [p]) (nth p ns) (ps, p_)
3.647 - | move_dn P (Nd (c, ns)) ([p], p_) = (* act on last element of pos *)
3.648 - if p > length ns
3.649 - then raise PTREE "move_dn: pos not existent 3"
3.650 - else
3.651 - (case p_ of
3.652 - Res =>
3.653 - if p = length ns (* last Res on this level: go a level up *)
3.654 - then if g_ostate c = Complete
3.655 - then (P, Res)
3.656 - else raise PTREE (ints2str' P ^ " not complete 1")
3.657 - else (* go to the next Nd on this level, or down into the next Nd *)
3.658 - if is_pblnd (nth (p + 1) ns) then (P@[p + 1], Pbl)
3.659 - else if g_res' (nth p ns) = g_form' (nth (p + 1) ns)
3.660 - then if (null o children o (nth (p + 1))) ns
3.661 - then (* take the Res if Complete *)
3.662 - if g_ostate' (nth (p + 1) ns) = Complete
3.663 - then (P@[p + 1], Res)
3.664 - else raise PTREE (ints2str' (P@[p + 1]) ^ " not complete 2")
3.665 - else (P@[p + 1, 1], Frm) (* go down into the next PrfObj *)
3.666 - else (P@[p + 1], Frm) (* take Frm: exists if the Nd exists *)
3.667 - | Frm => (*go down or to the Res of this Nd*)
3.668 - if (null o children o (nth p)) ns
3.669 - then if g_ostate' (nth p ns) = Complete then (P @ [p], Res)
3.670 - else raise PTREE (ints2str' (P @ [p])^" not complete 3")
3.671 - else (P @ [p, 1], Frm)
3.672 - | _ => (* is Pbl or Met *)
3.673 - if (null o children o (nth p)) ns
3.674 - then raise PTREE "move_dn:solve subproblem not startd"
3.675 - else (P @ [p, 1],
3.676 - if (is_pblnd o hd o children o (nth p)) ns
3.677 - then Pbl else Frm))
3.678 - | move_dn _ _ _ = raise ERROR "";
3.679 -in
3.680 -(* get all positions in a ctree until ([],Res) or ostate=Incomplete
3.681 -val get_allp = fn :
3.682 - pos' list -> : accumulated, start with []
3.683 - pos -> : the offset for subtrees wrt the root
3.684 - ctree -> : (sub)tree
3.685 - pos' : initialization (the last pos' before ...)
3.686 - -> pos' list : of positions in this (sub) tree (relative to the root)
3.687 -*)
3.688 -fun get_allp cuts (P, pos) pt =
3.689 - (let
3.690 - val nxt = move_dn [] pt pos (*exn if Incomplete reached*)
3.691 - in
3.692 - if nxt <> ([], Res)
3.693 - then get_allp (cuts @ [nxt]) (P, nxt) pt
3.694 - else map (apfst (curry op @ P)) (cuts @ [nxt])
3.695 - end)
3.696 - handle PTREE _ => (map (apfst (curry op@ P)) cuts);
3.697 -end
3.698 -
3.699 -(* the pts are assumed to be on the same level *)
3.700 -fun get_allps cuts _ [] = cuts
3.701 - | get_allps cuts P (pt :: pts) =
3.702 - let
3.703 - val below = get_allp [] (P, ([], Frm)) pt
3.704 - val levfrm =
3.705 - if is_pblnd pt
3.706 - then (P, Pbl) :: below
3.707 - else if last_elem P = 1
3.708 - then (P, Frm) :: below
3.709 - else (*Trans*) below
3.710 - val levres = levfrm @ (if null below then [(P, Res)] else [])
3.711 - in
3.712 - get_allps (cuts @ levres) (lev_on P) pts
3.713 - end;
3.714 -
3.715 -(** these 2 funs decide on how far cut_tree goes **)
3.716 -(* shall the nodes _after_ the pos to be inserted at be deleted?
3.717 - shall cutting be continued on the higher level(s)? the Nd regarded will NOT be changed *)
3.718 -fun test_trans (PrfObj {branch, ...}) = (branch = TransitiveB orelse branch = NoBranch)
3.719 - | test_trans (PblObj {branch, ...}) = (branch = TransitiveB orelse branch = NoBranch);
3.720 -
3.721 -(* cut_bottom new sml603..608
3.722 -cut the level at the bottom of the pos (used by cappend_...)
3.723 -and handle the parent in order to avoid extra case for root
3.724 -fn: ctree -> : the _whole_ ctree for cut_levup
3.725 - pos * Pos.posel -> : the pos after split_last
3.726 - ctree -> : the parent of the Nd to be cut
3.727 -return
3.728 - (ctree * : the updated ctree
3.729 - pos' list) * : the pos's cut
3.730 - bool : cutting shall be continued on the higher level(s)
3.731 -*)
3.732 -fun cut_bottom _ (pt' as Nd (b, [])) = ((pt', []), test_trans b)
3.733 - | cut_bottom (P, p) (Nd (b, bs)) =
3.734 - let (*divide level into 3 parts...*)
3.735 - val keep = take (p - 1, bs)
3.736 - val pt' = case nth p bs of
3.737 - pt' as Nd _ => pt'
3.738 - | _ => raise ERROR "cut_bottom: uncovered case nth p bs"
3.739 - (*^^^^^_here_ will be 'insert_pt'ed by 'append_..'*)
3.740 - val (tail, _) = (takerest (p, bs), if null (takerest (p, bs)) then 0 else p + 1)
3.741 - val (children, cuts) =
3.742 - if test_trans b
3.743 - then
3.744 - (keep, (if is_pblnd pt' then [(P @ [p], Pbl)] else [])
3.745 - @ (get_allp [] (P @ [p], (P, Frm)) pt')
3.746 - @ (get_allps [] (P @ [p + 1]) tail))
3.747 - else (keep @ [(*'insert_pt'ed by 'append_..'*)] @ tail,
3.748 - get_allp [] (P @ [p], (P, Frm)) pt')
3.749 - val (pt'', cuts) =
3.750 - if test_trans b
3.751 - then (Nd (del_res b, children), cuts @ (if g_ostate b = Incomplete then [] else [(P, Res)]))
3.752 - else (Nd (b, children), cuts)
3.753 - in ((pt'', cuts), test_trans b) end
3.754 - | cut_bottom _ _ = raise ERROR "cut_bottom: uncovered fun def.";
3.755 -
3.756 -
3.757 -(* go all levels from the bottom of 'pos' up to the root,
3.758 - on each level compose the children of a node and accumulate the cut Nds
3.759 -args
3.760 - pos' list -> : for accumulation
3.761 - bool -> : cutting shall be continued on the higher level(s)
3.762 - ctree -> : the whole ctree for 'get_nd pt P' on each level
3.763 - ctree -> : the Nd from the lower level for insertion at path
3.764 - pos * Pos.posel -> : pos=path split for convenience
3.765 - ctree -> : Nd the children of are under consideration on this call
3.766 -returns :
3.767 - ctree * pos' list : the updated parent-Nd and the pos's of the Nds cut
3.768 -*)
3.769 -fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:Pos.posel) (Nd (b, bs)) =
3.770 - let (*divide level into 3 parts...*)
3.771 - val keep = take (p - 1, bs)
3.772 - (*val pt' comes as argument from below*)
3.773 - val (tail, _) =
3.774 - (takerest (p, bs), if null (takerest (p, bs)) then 0 else p + 1)
3.775 - val (children, cuts') =
3.776 - if clevup
3.777 - then (keep @ [pt'], get_allps [] (P @ [p+1]) tail)
3.778 - else (keep @ [pt'] @ tail, [])
3.779 - val clevup' = if clevup then test_trans b else false
3.780 - (*the first Nd with false stops cutting on all levels above*)
3.781 - val (pt'', cuts') =
3.782 - if clevup'
3.783 - then (Nd (del_res b, children), cuts' @ (if g_ostate b = Incomplete then [] else [(P, Res)]))
3.784 - else (Nd (b, children), cuts')
3.785 - in
3.786 - if null P
3.787 - then (pt'', cuts @ cuts')
3.788 - else
3.789 - let val (P, p) = split_last P
3.790 - in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P) end
3.791 - end
3.792 - | cut_levup _ _ _ _ _ _ = raise ERROR "cut_levup: uncovered fun def.";
3.793 -
3.794 -(* cut nodes after and below an inserted node in the ctree;
3.795 - the cuts range is limited by the predicate 'fun cutlevup' *)
3.796 -fun cut_tree pt (pos, _) =
3.797 - if not (existpt pos pt)
3.798 - then (pt, []) (*appending a formula never cuts anything*)
3.799 - else
3.800 - let
3.801 - val (P, p) = split_last pos
3.802 - val ((pt', cuts), clevup) = cut_bottom (P, p) (get_nd pt P)
3.803 - (* pt' is the updated parent of the Nd to cappend_..*)
3.804 - in
3.805 - if null P
3.806 - then (pt', cuts)
3.807 - else
3.808 - let val (P, p) = split_last P
3.809 - in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P) end
3.810 - end;
3.811 -
3.812 -(* get the theory explicitly just for the rootpbl;
3.813 - thus use this function _after_ finishing specification *)
3.814 -fun root_thy (Nd (PblObj {spec = (thyID, _, _), ctxt, ...}, _)) = ThyC.get_theory ctxt thyID
3.815 - | root_thy _ = raise ERROR "root_thy: uncovered fun def.";
3.816 -
3.817 -(**)
3.818 -end;
3.819 -(**)
4.1 --- a/src/Tools/isac/Specify/i-model.sml Mon Dec 11 12:14:28 2023 +0100
4.2 +++ b/src/Tools/isac/Specify/i-model.sml Mon Dec 11 16:12:53 2023 +0100
4.3 @@ -10,12 +10,6 @@
4.4
4.5 type T
4.6 type T_POS
4.7 -(*OLD* )
4.8 - val OLD_to_POS: T -> T_POS .. already Test_Isac ok
4.9 - val OLD_to_POS: T_POS -> T_POS
4.10 - val TEST_to_OLD: T_POS -> T
4.11 -( *---*)
4.12 -(*NEW*)
4.13 val empty: T
4.14 val empty_POS: T_POS
4.15
4.16 @@ -41,17 +35,8 @@
4.17 val single_to_string_POS: Proof.context -> single_POS -> string
4.18 val to_string_POS: Proof.context -> T_POS -> string
4.19
4.20 - val feedback_OLD_to_POS: feedback -> feedback_POS
4.21 - val feedback_POS_to_OLD: feedback_POS -> feedback
4.22 - val OLD_to_POS_single: single -> single_POS
4.23 - val TEST_to_OLD_single: single_POS -> single
4.24 -
4.25 datatype add_single = Add of single_POS | Err of string
4.26 -(*OLD* )
4.27 - val init: Model_Pattern.T -> T
4.28 -( *---*)
4.29 val init_POS: Proof.context -> O_Model.T -> Model_Pattern.T -> T_POS
4.30 -(*NEW*)
4.31 val check_single: Proof.context -> m_field -> O_Model.T -> T_POS -> Model_Pattern.T ->
4.32 TermC.as_string -> add_single
4.33 val add_single: theory -> single_POS -> T_POS -> T_POS
4.34 @@ -134,29 +119,6 @@
4.35
4.36 type env = Env.T
4.37
4.38 -
4.39 -fun feedback_OLD_to_POS (Cor ((d, ts), _)) = (Model_Def.Cor_POS (d, ts))
4.40 - | feedback_OLD_to_POS (Syn c) = (Model_Def.Syn_POS c)
4.41 - | feedback_OLD_to_POS (Typ c) = (Model_Def.Syn_POS c)
4.42 - | feedback_OLD_to_POS (Inc ((d, ts), _)) = (Model_Def.Inc_POS (d, ts))
4.43 - | feedback_OLD_to_POS (Sup (d, ts)) = (Model_Def.Sup_POS (d, ts))
4.44 - | feedback_OLD_to_POS (Mis (d, pid)) = Model_Def.Syn_POS ((UnparseC.term (ContextC.for_ERROR ()) d) ^ " " ^
4.45 - (UnparseC.term (ContextC.for_ERROR ()) pid))
4.46 - | feedback_OLD_to_POS (Par s) = (Model_Def.Syn_POS s)
4.47 -fun OLD_to_POS_single (a, b, c, d, e) = (a, b, c, d, (feedback_OLD_to_POS e, Position.none))
4.48 -(*OLD* )
4.49 -fun OLD_to_POS i_old = map OLD_to_POS_single i_old
4.50 -fun OLD_to_POS i_old = I i_old
4.51 -( *---*)
4.52 -(*NEW*)
4.53 -
4.54 -fun feedback_POS_to_OLD (Model_Def.Cor_POS (d, ts)) = (Cor ((d, ts), (TermC.empty, [])))
4.55 - | feedback_POS_to_OLD (Model_Def.Syn_POS c) = (Syn c)
4.56 - | feedback_POS_to_OLD (Model_Def.Inc_POS (d, ts)) = (Inc ((d, ts), (TermC.empty, [])))
4.57 - | feedback_POS_to_OLD (Model_Def.Sup_POS (d, ts)) = (Sup (d, ts))
4.58 -fun TEST_to_OLD_single (a, b, c, d, (e, _)) = (a, b, c, d, feedback_POS_to_OLD e)
4.59 -fun TEST_to_OLD i_model = map TEST_to_OLD_single i_model
4.60 -
4.61 type message = string;
4.62 fun feedback_POS_to_string ctxt (Cor_POS (d, ts)) =
4.63 "Cor_POS " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
5.1 --- a/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy Mon Dec 11 12:14:28 2023 +0100
5.2 +++ b/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy Mon Dec 11 16:12:53 2023 +0100
5.3 @@ -1,6 +1,6 @@
5.4 theory Test_VSCode_Example
5.5 imports "Isac.Build_Isac" (*"Isac.Calculation"*)
5.6 - keywords "Example" :: thy_decl
5.7 +(*keywords "Example" :: thy_decl -- the active definition is in Calculation.thy*)
5.8 begin
5.9
5.10 text \<open>
5.11 @@ -54,8 +54,9 @@
5.12 calculation.sml --- build Outer_Syntax Example 3 ff*)
5.13 \<close> ML \<open>
5.14 \<close> ML \<open>
5.15 +(*/--------------------- the active definition is in Calculation.thy -------------------------\* )
5.16 val _ =
5.17 - Outer_Syntax.command \<^command_keyword>\<open>Example\<close>
5.18 + Outer_Syntax.command \<^command_keyword>\<open>Example_test\<close>
5.19 "prepare ISAC problem type and register it to Knowledge Store"
5.20 (Parse.name -- Parse.!!! ( \<^keyword>\<open>Specification\<close> -- \<^keyword>\<open>:\<close> --
5.21 \<^keyword>\<open>Model\<close> -- \<^keyword>\<open>:\<close> |-- Problem.parse_pos_model_input --
5.22 @@ -107,6 +108,7 @@
5.23 (example_id, (model_input, (thy_id, probl_id, meth_id))) (the_data thy)
5.24 end
5.25 in set_data state thy end)));
5.26 +( *\--------------------- the active definition is in Calculation.thy -------------------------/*)
5.27 \<close> ML \<open>
5.28 \<close> ML \<open> (*Example below*)
5.29 \<close>
6.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Mon Dec 11 12:14:28 2023 +0100
6.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Mon Dec 11 16:12:53 2023 +0100
6.3 @@ -725,9 +725,9 @@
6.4 = fst istate |> Istate.string_of ctxt
6.5 val ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]) = spec;
6.6 val "[\n(1, [1], true ,#Given, (Cor_POS functionTerm (x \<up> 2 + x + 1) , pen2str, Position.T)), \n(2, [1], true ,#Given, (Cor_POS differentiateFor x , pen2str, Position.T)), \n(3, [1], true ,#Find, (Cor_POS derivative f_'_f , pen2str, Position.T))]"
6.7 - = probl |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt
6.8 + = probl |> I_Model.to_string_POS ctxt
6.9 val "[\n(1, [1], true ,#Given, (Cor_POS functionTerm (x \<up> 2 + x + 1) , pen2str, Position.T)), \n(2, [1], true ,#Given, (Cor_POS differentiateFor x , pen2str, Position.T)), \n(3, [1], true ,#Find, (Cor_POS derivative f_'_f , pen2str, Position.T))]"
6.10 - = meth |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt;
6.11 + = meth |> I_Model.to_string_POS ctxt;
6.12
6.13 (*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
6.14 autoCalculate 1 (Steps 1);
7.1 --- a/test/Tools/isac/Interpret/li-tool.sml Mon Dec 11 12:14:28 2023 +0100
7.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Mon Dec 11 16:12:53 2023 +0100
7.3 @@ -68,7 +68,7 @@
7.4 val thy' = get_obj g_domID pt p;
7.5 val thy = ThyC.get_theory @{context} thy';
7.6 val prog_rls = LItool.get_simplifier (pt, pos)
7.7 -val (is as Pstate {env, ...}, ctxt, sc) = init_pstate ctxt (I_Model.OLD_to_POS itms) mI;
7.8 +val (is as Pstate {env, ...}, ctxt, sc) = init_pstate ctxt itms mI;
7.9 val ini = implicit_take @{context} sc env;
7.10 "----- fun implicit_take, args:"; val (Prog sc) = sc;
7.11 "----- fun get_first_argument, args:"; val (y, h $ body) = (thy, sc);
7.12 @@ -355,8 +355,7 @@
7.13 => (itms, oris, probl, o_spec, spec)
7.14 | _ => raise ERROR ""
7.15 val (_, pI', _) = References.select_input o_spec spec
7.16 - val (_, itms) = I_Model.s_make_complete ctxt oris
7.17 - (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS itms) (pI', mI)
7.18 + val (_, itms) = I_Model.s_make_complete ctxt oris (probl, itms) (pI', mI)
7.19 ;
7.20 (*+*)val "[\n(1, [1], true ,#Given, (Cor_POS Traegerlaenge L , pen2str, Position.T)), \n(2, [1], true ,#Given, (Cor_POS Streckenlast q_0 , pen2str, Position.T)), \n(4, [1], true ,#Relate, (Cor_POS Randbedingungen [M_b 0 = 0, y 0 = 0, y L = 0, M_b L = 0] , pen2str, Position.T)), \n(5, [1], true ,#Given, (Cor_POS FunktionsVariable x , pen2str, Position.T)), \n(6, [1], true ,#Given, (Cor_POS AbleitungBiegelinie y' , pen2str, Position.T)), \n(7, [1], true ,#Given, (Cor_POS Biegemoment M_b , pen2str, Position.T)), \n(8, [1], true ,#Given, (Cor_POS Querkraft Q , pen2str, Position.T)), \n(9, [1], true ,#Given, (Cor_POS GleichungsVariablen [c_3, c, c_2, c_4] , pen2str, Position.T)), \n(3, [1], true ,#Find, (Cor_POS Biegelinie y , pen2str, Position.T))]"
7.21 = itms |> I_Model.to_string_POS @{context};
8.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Dec 11 12:14:28 2023 +0100
8.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Dec 11 16:12:53 2023 +0100
8.3 @@ -71,8 +71,7 @@
8.4 => (itms, oris, probl, o_spec, spec)
8.5 | _ => raise ERROR ""
8.6 val (_, pI', _) = References.select_input o_spec spec
8.7 - val (_, itms) = I_Model.s_make_complete ctxt oris
8.8 - (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS itms) (pI', mI)
8.9 + val (_, itms) = I_Model.s_make_complete ctxt oris (probl, itms) (pI', mI)
8.10
8.11 val (is, env, ctxt, prog) = case
8.12 LItool.init_pstate ctxt itms mI of
8.13 @@ -169,8 +168,7 @@
8.14 => (itms, oris, probl, o_spec, spec)
8.15 | _ => raise ERROR ""
8.16 val (_, pI', _) = References.select_input o_spec spec
8.17 - val (_, itms) = I_Model.s_make_complete ctxt oris
8.18 - (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS itms) (pI', mI)
8.19 + val (_, itms) = I_Model.s_make_complete ctxt oris (probl, itms) (pI', mI)
8.20
8.21 val (is, env, ctxt, sc) = case
8.22 LItool.init_pstate ctxt itms mI of
9.1 --- a/test/Tools/isac/Knowledge/diff-app.sml Mon Dec 11 12:14:28 2023 +0100
9.2 +++ b/test/Tools/isac/Knowledge/diff-app.sml Mon Dec 11 16:12:53 2023 +0100
9.3 @@ -312,7 +312,7 @@
9.4 === inhibit exn 110722=============================================================*)
9.5
9.6 val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string @{context} oris);
9.7 -val pits = get_obj g_pbl pt (fst p);writeln(I_Model.to_string_POS ctxt (I_Model.OLD_to_POS pits));
9.8 +val pits = get_obj g_pbl pt (fst p);writeln (I_Model.to_string_POS ctxt pits);
9.9
9.10 (*=== inhibit exn 110722=============================================================
9.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.12 @@ -382,11 +382,11 @@
9.13
9.14 val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string @{context} oris);
9.15
9.16 -val pits = get_obj g_pbl pt (fst p);writeln(I_Model.to_string_POS ctxt (I_Model.OLD_to_POS pits));
9.17 -val pits = get_obj g_pbl pt [];writeln(I_Model.to_string_POS ctxt (I_Model.OLD_to_POS pits));
9.18 +val pits = get_obj g_pbl pt (fst p); writeln (I_Model.to_string_POS ctxt pits);
9.19 +val pits = get_obj g_pbl pt []; writeln (I_Model.to_string_POS ctxt pits);
9.20
9.21 -val mits = get_obj g_met pt (fst p);writeln(I_Model.to_string_POS ctxt (I_Model.OLD_to_POS mits));
9.22 -val mits = get_obj g_met pt [];writeln(I_Model.to_string_POS ctxt (I_Model.OLD_to_POS mits));
9.23 +val mits = get_obj g_met pt (fst p);writeln(I_Model.to_string_POS ctxt mits);
9.24 +val mits = get_obj g_met pt [];writeln(I_Model.to_string_POS ctxt mits);
9.25
9.26 (*=== inhibit exn 110722=============================================================
9.27 arguments_from_model ["Diff_App", "max_by_calculus"] mits;
9.28 @@ -438,7 +438,7 @@
9.29 fetchProposedTactic 1;
9.30 val ((pt,p),_) = States.get_calc 1;
9.31 val mits = get_obj g_met pt (fst p);
9.32 - writeln (I_Model.to_string_POS ctxt (I_Model.OLD_to_POS mits));
9.33 + writeln (I_Model.to_string_POS ctxt mits);
9.34 (*
9.35 if I_Model.to_string ctxt mits = "[\n(1 ,[1] ,true ,#Given ,Cor functionEq (hd r_s) ,(t_, [hd r_s])),\n(2 ,[1] ,true ,#Given ,Cor boundVariable v_v ,(v_, [v_])),\n(3 ,[1] ,true ,#Given ,Cor interval itv_ ,(itv_, [itv_])),\n(4 ,[1] ,true ,#Find ,Cor maxArgument v__0 ,(v_0, [v__0]))]" then ()
9.36 else error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1";
10.1 --- a/test/Tools/isac/Knowledge/eqsystem-1a.sml Mon Dec 11 12:14:28 2023 +0100
10.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1a.sml Mon Dec 11 16:12:53 2023 +0100
10.3 @@ -125,8 +125,7 @@
10.4 => (itms, oris, probl, o_spec, spec)
10.5 | _ => raise ERROR "LI.by_tactic: no PblObj"
10.6 val (_, pI', _) = References.select_input o_spec spec
10.7 - val (_, itms) = I_Model.s_make_complete ctxt oris
10.8 - (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS itms) (pI', mI)
10.9 + val (_, itms) = I_Model.s_make_complete ctxt oris (probl, itms) (pI', mI)
10.10 val (is, env, ctxt, prog) = case LItool.init_pstate ctxt itms mI of
10.11 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
10.12 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate"
11.1 --- a/test/Tools/isac/Knowledge/simplify.sml Mon Dec 11 12:14:28 2023 +0100
11.2 +++ b/test/Tools/isac/Knowledge/simplify.sml Mon Dec 11 16:12:53 2023 +0100
11.3 @@ -106,9 +106,9 @@
11.4
11.5 (** ) val (_, (Met, Specify_Method ["simplification", "of_rationals"])) = ( *isa*)
11.6 (**) val (_, (Met, Apply_Method ["simplification", "of_rationals"])) = (*isa2*)
11.7 - for_method ctxt oris (o_refs, refs) (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met);
11.8 + for_method ctxt oris (o_refs, refs) (pbl, met);
11.9 "~~~~~ fun for_method , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (_, met)) =
11.10 - (oris, (o_refs, refs), (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met));
11.11 + (oris, (o_refs, refs), (pbl, met));
11.12 val cmI = if mI = MethodC.id_empty then mI' else mI;
11.13 val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI;
11.14
12.1 --- a/test/Tools/isac/MathEngine/step.sml Mon Dec 11 12:14:28 2023 +0100
12.2 +++ b/test/Tools/isac/MathEngine/step.sml Mon Dec 11 16:12:53 2023 +0100
12.3 @@ -304,7 +304,7 @@
12.4 val PblObj {probl, ...} = get_obj I (fst ptp) [];
12.5
12.6 val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS fixedValues [r = Arbfix] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS valuesFor [a, b] , pen2str, Position.T)), \n(4, [1, 2], true ,#Relate, (Cor_POS relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
12.7 - = probl |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt
12.8 + = probl |> I_Model.to_string_POS ctxt
12.9
12.10 (*** Specification of References ========================================================== ***)
12.11 val ("ok", ([(Specify_Theory "Diff_App", _, _)], _, ptp))
12.12 @@ -326,7 +326,7 @@
12.13 val PblObj {meth, ...} = get_obj I (fst ptp) [];
12.14
12.15 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS fixedValues [r = Arbfix] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS maximum A , pen2str, Position.T)), \n(4, [1, 2], true ,#Relate, (Cor_POS relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS valuesFor [a, b] , pen2str, Position.T)), \n(6, [1], true ,#Given, (Cor_POS boundVariable a , pen2str, Position.T)), \n(9, [1, 2], true ,#Given, (Cor_POS interval {x. 0 \<le> x \<and> x \<le> 2 * r} , pen2str, Position.T)), \n(11, [1, 2, 3], true ,#Given, (Cor_POS errorBound (eps = 0) , pen2str, Position.T))]"
12.16 - = meth |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt
12.17 + = meth |> I_Model.to_string_POS ctxt
12.18
12.19 (*** Specification of Problem and MethodC model is complete, Solution starts ============== ***)
12.20
13.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Mon Dec 11 12:14:28 2023 +0100
13.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Mon Dec 11 16:12:53 2023 +0100
13.3 @@ -89,12 +89,12 @@
13.4 {Given = gi, Where = wh, Find= fi ,With = wi, Relate = re}
13.5 fun boolterm2item ctxt (true, term) = P_Model.Correct (UnparseC.term ctxt term)
13.6 | boolterm2item ctxt(false, term) = P_Model.False (UnparseC.term ctxt term);
13.7 + fun coll model [] = model
13.8 + | coll model ((_, _, _, field, (feedb, _)) :: itms) =
13.9 + coll (add_sel_ppc thy field model (item_from_feedback_POS thy feedb)) itms;
13.10 (*\\------------------ inserted hidden code ------------------------------------------------//*)
13.11
13.12 - fun coll model [] = model
13.13 - | coll model ((_, _, _, field, itm_)::itms) =
13.14 - coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
13.15 - val gfr = coll P_Model.empty (I_Model.TEST_to_OLD itms);
13.16 + val gfr = coll P_Model.empty itms;
13.17
13.18 (*val return =*)
13.19 add_where gfr (map (boolterm2item (Proof_Context.init_global thy)) where_);
14.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Mon Dec 11 12:14:28 2023 +0100
14.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Mon Dec 11 16:12:53 2023 +0100
14.3 @@ -58,10 +58,9 @@
14.4 (*if*) pI = Problem.id_empty (*else*);
14.5 val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
14.6 val (_, where_) =
14.7 - Pre_Conds.check ctxt where_rls where_
14.8 - (model, I_Model.OLD_to_POS probl);
14.9 + Pre_Conds.check ctxt where_rls where_ (model, probl);
14.10 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
14.11 - (ctxt, where_rls, where_, (model, I_Model.OLD_to_POS probl));
14.12 + (ctxt, where_rls, where_, (model, probl));
14.13 val (env_model, (env_subst, env_eval)) =
14.14 make_environments model_patt i_model;
14.15 "~~~~~ fun make_environments , args:"; val (_, []) = (model_patt, i_model);
14.16 @@ -130,7 +129,7 @@
14.17 [], (pt', pos)))
14.18 (*+++*)val {probl, ...} = Calc.specify_data (pt', pos);
14.19 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_POS Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_POS AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_POS Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_POS SideConditions [] [__=__, __=__], Position.T))]"
14.20 - = probl |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt
14.21 + = probl |> I_Model.to_string_POS ctxt
14.22 (*\\\\---------------- step into by_Add_ ---------------------------------------------------//*)
14.23 val return_by_tactic_step = return_by_Add_
14.24 (*\\\----------------- step into Step_Specify.by_tactic ------------------------------------//*)
14.25 @@ -142,7 +141,7 @@
14.26 (*+++*)val (pt, p) = ptp
14.27 (*+++*)val {probl, ...} = Calc.specify_data (pt, p);
14.28 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_POS Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_POS AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_POS Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_POS SideConditions [] [__=__, __=__], Position.T))]"
14.29 - = probl |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt;
14.30 + = probl |> I_Model.to_string_POS ctxt;
14.31
14.32 val (pt, p) = ptp; (*case*)
14.33 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
14.34 @@ -172,7 +171,7 @@
14.35 spec = refs, ...} = Calc.specify_data (pt, pos);
14.36 val ctxt = Ctree.get_ctxt pt pos;
14.37 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_POS Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_POS AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_POS Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_POS SideConditions [] [__=__, __=__], Position.T))]"
14.38 - = pbl |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt(*+*)
14.39 + = pbl |> I_Model.to_string_POS ctxt(*+*)
14.40
14.41 val false =
14.42 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
14.43 @@ -181,10 +180,10 @@
14.44
14.45 (** )val ("dummy", (Pbl, Add_Find "Maximum A")) =( **)
14.46 (**)val return_for_problem as ("dummy", (Pbl, Add_Find "Maximum A"))=(**)
14.47 - for_problem ctxt oris (o_refs, refs) (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met);
14.48 + for_problem ctxt oris (o_refs, refs) (pbl, met);
14.49 (*//------------------ step into for_problem -----------------------------------------------\\*)
14.50 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
14.51 - (ctxt, oris, (o_refs, refs), (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met));
14.52 + (ctxt, oris, (o_refs, refs), (pbl, met));
14.53 val cpI = if pI = Problem.id_empty then pI' else pI;
14.54 val cmI = if mI = MethodC.id_empty then mI' else mI;
14.55 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
14.56 @@ -344,9 +343,9 @@
14.57 (*if*) p_ = Pos.Pbl (*then*);
14.58
14.59 (**)val return_find_next_step_STEP as ("dummy", (Pbl, Add_Find "AdditionalValues [u]")) =(**)
14.60 - for_problem ctxt oris (o_refs, refs) (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met);
14.61 + for_problem ctxt oris (o_refs, refs) (pbl, met);
14.62 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
14.63 - (ctxt, oris, (o_refs, refs), ( I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met));
14.64 + (ctxt, oris, (o_refs, refs), (pbl, met));
14.65 val cpI = if pI = Problem.id_empty then pI' else pI;
14.66 val cmI = if mI = MethodC.id_empty then mI' else mI;
14.67 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
14.68 @@ -423,10 +422,10 @@
14.69
14.70 (** )val ("dummy", (Pbl, tac as Specify_Theory "Diff_App")) =( **)
14.71 (**)val return_for_problem =(**)
14.72 - for_problem ctxt oris (o_refs, refs) (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met);
14.73 + for_problem ctxt oris (o_refs, refs) (pbl, met);
14.74 (*///// /------------- step into for_problem -----------------------------------------------\\*)
14.75 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
14.76 - (ctxt, oris, (o_refs, refs), (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met));
14.77 + (ctxt, oris, (o_refs, refs), (pbl, met));
14.78 val cpI = if pI = Problem.id_empty then pI' else pI;
14.79 val cmI = if mI = MethodC.id_empty then mI' else mI;
14.80 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
14.81 @@ -634,11 +633,11 @@
14.82
14.83 (**)val return_match_itms_oris = (**)
14.84 (** )val (_, (i_model, _)) = ( **)
14.85 - M_Match.by_i_models ctxt o_model' (I_Model.OLD_to_POS i_prob, I_Model.OLD_to_POS i_prob)
14.86 + M_Match.by_i_models ctxt o_model' (i_prob, i_prob)
14.87 (m_patt, where_, where_rls);
14.88 (*///----------------- step into by_i_models -------------------------------------------\\*)
14.89 "~~~~~ fun by_i_models, args:"; val (ctxt, o_model, (pbl_imod, met_imod), (m_patt, where_, where_rls)) =
14.90 - (ctxt, o_model', (I_Model.OLD_to_POS i_prob, I_Model.OLD_to_POS i_prob), (m_patt, where_, where_rls));
14.91 + (ctxt, o_model', (i_prob, i_prob), (m_patt, where_, where_rls));
14.92
14.93 (**)val return_fill_method =(**)
14.94 (** )val met_imod =( **)
14.95 @@ -752,7 +751,7 @@
14.96 (*/------------------- step into me_Specify_Method -----------------------------------------\\*)
14.97 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
14.98
14.99 -(*+*)val "[]" =(*+*) get_obj g_met pt (fst p) |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt
14.100 +(*+*)val "[]" =(*+*) get_obj g_met pt (fst p) |> I_Model.to_string_POS ctxt
14.101
14.102 val ctxt = Ctree.get_ctxt pt p
14.103 val (pt, p) =
14.104 @@ -773,7 +772,7 @@
14.105 "~~~~~ fun by_i_models , args:"; val () = ();
14.106
14.107 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"
14.108 - = get_obj g_met pt (fst p) |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt;
14.109 + = get_obj g_met pt (fst p) |> I_Model.to_string_POS ctxt;
14.110
14.111 (*case*)
14.112 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
14.113 @@ -805,13 +804,13 @@
14.114 (*if*) p_ = Pos.Pbl (*else*);
14.115
14.116 (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"
14.117 - = met |> I_Model.OLD_to_POS |> I_Model.to_string_POS ctxt
14.118 + = met |> I_Model.to_string_POS ctxt
14.119
14.120 (**)val ("dummy", (Met, Add_Given "FunctionVariable a")) =(**)
14.121 - Specify.for_method ctxt oris (o_refs, refs) (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met);
14.122 + Specify.for_method ctxt oris (o_refs, refs) (pbl, met);
14.123 (*///// /------------- step into Step.for_method -------------------------------------------\\*)
14.124 "~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (_, met))
14.125 - = (ctxt, oris, (o_refs, refs), (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met));
14.126 + = (ctxt, oris, (o_refs, refs), (pbl, met));
14.127 val cmI = if mI = MethodC.id_empty then mI' else mI;
14.128 val {model, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
14.129 val (preok, _) = Pre_Conds.check ctxt where_rls where_ (model, met);
15.1 --- a/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Mon Dec 11 12:14:28 2023 +0100
15.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Mon Dec 11 16:12:53 2023 +0100
15.3 @@ -65,11 +65,9 @@
15.4 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
15.5
15.6 val (_, (i_model, _)) =
15.7 - M_Match.by_i_models ctxt o_model' (I_Model.OLD_to_POS i_prob,
15.8 - I_Model.OLD_to_POS i_prob) (m_patt, where_, where_rls);
15.9 + M_Match.by_i_models ctxt o_model' (i_prob, i_prob) (m_patt, where_, where_rls);
15.10 "~~~~~ fun by_i_models , args:"; val (ctxt, o_model, (pbl_imod, met_imod), (met_patt, where_, where_rls)) =
15.11 - (ctxt, o_model, (I_Model.OLD_to_POS i_prob,(*<--? --v?*)
15.12 - I_Model.OLD_to_POS i_prob), (m_patt, where_, where_rls));
15.13 + (ctxt, o_model, (i_prob, i_prob), (m_patt, where_, where_rls));
15.14 val met_imod = I_Model.fill_method o_model (pbl_imod, met_imod) met_patt
15.15
15.16 val (check, preconds) =
15.17 @@ -150,8 +148,7 @@
15.18 => (itms, oris, probl, o_spec, spec)
15.19 | _ => raise ERROR ""
15.20 val (_, pI', _) = References.select_input o_spec spec
15.21 - val (_, itms) = I_Model.s_make_complete ctxt oris
15.22 - (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS itms) (pI', mI)
15.23 + val (_, itms) = I_Model.s_make_complete ctxt oris (probl, itms) (pI', mI)
15.24
15.25 val (is, env, ctxt, prog) = case
15.26 LItool.init_pstate ctxt itms mI of
16.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Mon Dec 11 12:14:28 2023 +0100
16.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Mon Dec 11 16:12:53 2023 +0100
16.3 @@ -68,8 +68,7 @@
16.4 => (itms, oris, probl, o_spec, spec)
16.5 | _ => raise ERROR ""
16.6 val (_, pI', _) = References.select_input o_spec spec
16.7 - val (_, itms) = I_Model.s_make_complete ctxt oris
16.8 - (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS itms) (pI', mI)
16.9 + val (_, itms) = I_Model.s_make_complete ctxt oris (probl, itms) (pI', mI)
16.10
16.11 val (is, env, ctxt, prog) = case
16.12 LItool.init_pstate ctxt itms mI of
17.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Mon Dec 11 12:14:28 2023 +0100
17.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Mon Dec 11 16:12:53 2023 +0100
17.3 @@ -45,8 +45,7 @@
17.4 => (itms, oris, probl, o_spec, spec)
17.5 | _ => raise ERROR ""
17.6 val (_, pI', _) = References.select_input o_spec spec
17.7 - val (_, itms) = I_Model.s_make_complete ctxt oris
17.8 - (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS itms) (pI', mI)
17.9 + val (_, itms) = I_Model.s_make_complete ctxt oris (probl, itms) (pI', mI)
17.10
17.11 val thy' = get_obj g_domID pt p;
17.12 val thy = Know_Store.get_via_last_thy thy';
18.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Mon Dec 11 12:14:28 2023 +0100
18.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Mon Dec 11 16:12:53 2023 +0100
18.3 @@ -76,9 +76,9 @@
18.4 (*if*) p_ = Pos.Pbl (*then*);
18.5
18.6 val return_for_problem as (_, (_, xxx)) =
18.7 - Specify.for_problem ctxt oris (o_refs, refs) (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met);
18.8 + Specify.for_problem ctxt oris (o_refs, refs) (pbl, met);
18.9 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
18.10 - (ctxt, oris, (o_refs, refs), (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met));
18.11 + (ctxt, oris, (o_refs, refs), (pbl, met));
18.12 val cpI = if pI = Problem.id_empty then pI' else pI;
18.13 val cmI = if mI = MethodC.id_empty then mI' else mI;
18.14 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
18.15 @@ -199,8 +199,7 @@
18.16 (*+*)then () else error "assumptions 8";
18.17
18.18 val (_, pI', _) = References.select_input o_spec spec
18.19 - val (_, itms) = I_Model.s_make_complete ctxt oris
18.20 - (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS itms) (pI', mI)
18.21 + val (_, itms) = I_Model.s_make_complete ctxt oris (probl, itms) (pI', mI)
18.22 val prog_rls = LItool.get_simplifier (pt, pos)
18.23
18.24 val (is, env, ctxt, prog) = case
19.1 --- a/test/Tools/isac/Specify/i-model.sml Mon Dec 11 12:14:28 2023 +0100
19.2 +++ b/test/Tools/isac/Specify/i-model.sml Mon Dec 11 16:12:53 2023 +0100
19.3 @@ -167,7 +167,7 @@
19.4 (*+*)val [Free ("q_0", _)] = all;
19.5
19.6 (**)val ("", itm) =(**)
19.7 - (*case*) is_notyet_input ctxt (OLD_to_POS i_model) all ori' m_patt (*of*);
19.8 + (*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*);
19.9
19.10 (*+*)val (2, [1], true, "#Given", (Cor_POS (Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]), _)) = itm
19.11 (*\\------------------ step into check_single ----------------------------------------------//*)
20.1 --- a/test/Tools/isac/Specify/refine.sml Mon Dec 11 12:14:28 2023 +0100
20.2 +++ b/test/Tools/isac/Specify/refine.sml Mon Dec 11 16:12:53 2023 +0100
20.3 @@ -551,9 +551,9 @@
20.4 (*if*) p_ = Pos.Pbl (*then*);
20.5
20.6 val ("dummy", (Pbl, Add_Find "solutions L")) =
20.7 - for_problem ctxt oris (o_refs, refs) (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met);
20.8 + for_problem ctxt oris (o_refs, refs) (pbl, met);
20.9 "~~~~~ fun for_problem , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
20.10 - (oris, (o_refs, refs), (I_Model.OLD_to_POS pbl, I_Model.OLD_to_POS met));
20.11 + (oris, (o_refs, refs), (pbl, met));
20.12 val cpI = if pI = Problem.id_empty then pI' else pI;
20.13 val cmI = if mI = MethodC.id_empty then mI' else mI;
20.14 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
21.1 --- a/test/Tools/isac/Test_Isac.thy Mon Dec 11 12:14:28 2023 +0100
21.2 +++ b/test/Tools/isac/Test_Isac.thy Mon Dec 11 16:12:53 2023 +0100
21.3 @@ -245,21 +245,11 @@
21.4 ML_file "Minisubpbl/150a-add-given-Maximum.sml"
21.5 ML_file "Minisubpbl/150-add-given-Equation.sml"
21.6 ML_file "Minisubpbl/200-start-method-NEXT_STEP.sml"
21.7 -ML \<open>
21.8 -\<close> ML \<open>
21.9 -
21.10 -\<close> ML \<open>
21.11 -\<close>
21.12 ML_file "Minisubpbl/200-start-method.sml"
21.13 ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml"
21.14 ML_file "Minisubpbl/300-init-subpbl-NEXT_STEP.sml"
21.15 ML_file "Minisubpbl/300-init-subpbl.sml"
21.16 ML_file "Minisubpbl/400-start-meth-subpbl.sml"
21.17 -ML \<open>
21.18 -\<close> ML \<open>
21.19 -
21.20 -\<close> ML \<open>
21.21 -\<close>
21.22 ML_file "Minisubpbl/450-Rewrite_Set_Inst.sml"
21.23 ML_file "Minisubpbl/470-Check_elementwise-NEXT_STEP.sml"
21.24 ML_file "Minisubpbl/490-nxt-Check_Postcond.sml"