1.1 --- a/src/Tools/isac/MathEngBasic/ctree-access.sml Tue Feb 11 11:58:45 2020 +0100
1.2 +++ b/src/Tools/isac/MathEngBasic/ctree-access.sml Tue Feb 11 17:25:45 2020 +0100
1.3 @@ -39,12 +39,12 @@
1.4 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.5 val cappend_parent : CTbasic.ctree -> int list -> Istate_Def.T * Proof.context -> term ->
1.6 Tactic.input -> CTbasic.branch -> CTbasic.ctree * CTbasic.pos' list
1.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
1.9 val update_loc' : CTbasic.ctree -> CTbasic.pos ->
1.10 (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option -> CTbasic.ctree
1.11 val append_problem : int list -> Istate_Def.T * Proof.context -> Selem.fmz ->
1.12 Model.ori list * Celem.spec * term -> CTbasic.ctree -> CTbasic.ctree
1.13 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.14 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.15 end
1.16 (**)
1.17 structure CTaccess(**): CALC_TREE_ACCESS(**) =
2.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Tue Feb 11 11:58:45 2020 +0100
2.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Tue Feb 11 17:25:45 2020 +0100
2.3 @@ -211,7 +211,7 @@
2.4 result: Selem.result, (* result and assumptions *)
2.5 ostate: ostate} (* Complete <=> result is OK *)
2.6 | PblObj of
2.7 - {cell : TermC.lrd option, (* unused: meaningful only for some _Prf_Obj *)
2.8 + {cell : TermC.lrd option, (* DELETE: meaningful only for some _Prf_Obj *)
2.9 fmz : Selem.fmz, (* from init:FIXME never use this spec;-drop *)
2.10 origin: (Model.ori list) *(* representation from fmz+pbt+met
2.11 for efficiently adding items in probl, meth *)
2.12 @@ -220,8 +220,9 @@
2.13 spec : Celem.spec, (* explicitly input *)
2.14 probl : Model.itm list, (* itms explicitly input *)
2.15 meth : Model.itm list, (* itms automatically added to copy of probl *)
2.16 - ctxt : Proof.context, (* WN110513 introduced to avoid [*] [**] *)
2.17 - env : (Istate_Def.T * Proof.context) option, (* istate only for initac in script
2.18 + ctxt : Proof.context, (* DELETE: WN110513 introduced to avoid [*] [**] *)
2.19 + env : (Istate_Def.T * Proof.context) option, (* DELETE:
2.20 + istate only for initac in script
2.21 context for specify phase on this node NO..
2.22 ..NO: this conflicts with init_form/initac: see Apply_Method without init_form *)
2.23 loc : (Istate_Def.T * Proof.context) option * (Istate_Def.T * (* like PrfObj *)
3.1 --- a/src/Tools/isac/MathEngine/step.sml Tue Feb 11 11:58:45 2020 +0100
3.2 +++ b/src/Tools/isac/MathEngine/step.sml Tue Feb 11 17:25:45 2020 +0100
3.3 @@ -4,7 +4,8 @@
3.4 *)
3.5
3.6 (* survey on results of by_tactic, find_next, by_term:
3.7 - * Step_Specify TODO
3.8 + * Step_Specify
3.9 + * by_tactic "ok", "ok",
3.10 * Step_Solve
3.11 * locate_input_tactic : "ok", "unsafe-ok", "not-applicable", "end-of-calculation"
3.12 * locate_input_term : "ok", "syntax error", "same-formula", "no derivation found",
3.13 @@ -86,6 +87,7 @@
3.14 | SOME _ => switch_specify_solve p_ (pt, ip)
3.15 end
3.16
3.17 +
3.18 (** locate an input tactic **)
3.19
3.20 datatype lOc_ = ERror of string | UNsafe of Chead.calcstate' | Updated of Chead.calcstate'
4.1 --- a/src/Tools/isac/Specify/Specify.thy Tue Feb 11 11:58:45 2020 +0100
4.2 +++ b/src/Tools/isac/Specify/Specify.thy Tue Feb 11 17:25:45 2020 +0100
4.3 @@ -16,6 +16,286 @@
4.4
4.5 ML \<open>
4.6 \<close> ML \<open>
4.7 +open Ctree
4.8 +open Pos
4.9 +open Chead
4.10 +\<close> ML \<open>
4.11 +\<close> ML \<open>
4.12 +\<close> ML \<open>
4.13 +\<close> ML \<open>
4.14 +fun header p_ pI mI =
4.15 + case p_ of Pbl => Generate.Problem (if pI = Celem.e_pblID then [] else pI)
4.16 + | Met => Generate.Method mI
4.17 + | pos => error ("header called with "^ pos_2str pos)
4.18 +\<close> ML \<open>
4.19 +fun overwrite_ppc thy itm ppc =
4.20 + let
4.21 + fun repl _ (_, _, _, _, itm_) [] =
4.22 + error ("overwrite_ppc: " ^ (Model.itm_2str_ (Rule.thy2ctxt thy) itm_) ^ " not found")
4.23 + | repl ppc' itm (p :: ppc) =
4.24 + if (#1 itm) = (#1 p)
4.25 + then ppc' @ [itm] @ ppc
4.26 + else repl (ppc' @ [p]) itm ppc
4.27 + in repl [] itm ppc end
4.28 +\<close> ML \<open>
4.29 +fun seek_ppc _ [] = NONE
4.30 + | seek_ppc id (p :: ppc) = if id = #1 (p: Model.itm) then SOME p else seek_ppc id ppc
4.31 +\<close> ML \<open>
4.32 +fun insert_ppc thy itm ppc =
4.33 + let
4.34 + fun eq_untouched d (0, _, _, _, itm_) = (d = Model.d_in itm_)
4.35 + | eq_untouched _ _ = false
4.36 + val ppc' = case seek_ppc (#1 itm) ppc of
4.37 + SOME _ => overwrite_ppc thy itm ppc (*itm updated in is_notyet_input WN.11.03*)
4.38 + | NONE => (ppc @ [itm])
4.39 + in filter_out (eq_untouched ((Model.d_in o #5) itm)) ppc' end
4.40 +\<close> ML \<open>
4.41 +fun specify_additem sel ct (pt, (p, Met)) =
4.42 + let
4.43 + val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of
4.44 + (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
4.45 + => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
4.46 + | _ => error "specify_additem: uncovered case of get_obj I pt p"
4.47 + val thy = if dI = Rule.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI
4.48 + val cpI = if pI = Celem.e_pblID then pI' else pI
4.49 + val cmI = if mI = Celem.e_metID then mI' else mI
4.50 + val {ppc, pre, prls, ...} = Specify.get_met cmI
4.51 + in
4.52 + case Chead.appl_add ctxt sel oris met ppc ct of
4.53 + Chead.Add itm => (*..union old input *)
4.54 + let
4.55 + val met' = insert_ppc thy itm met
4.56 + val arg = case sel of
4.57 + "#Given" => Tactic.Add_Given' (ct, met')
4.58 + | "#Find" => Tactic.Add_Find' (ct, met')
4.59 + | "#Relate"=> Tactic.Add_Relation'(ct, met')
4.60 + | str => error ("specify_additem: uncovered case with " ^ str)
4.61 + val (p, pt') = case Generate.generate1 thy arg (Istate_Def.Uistate, ctxt) (p, Met) pt of
4.62 + ((p, Met), _, _, pt') => (p, pt')
4.63 + | _ => error "specify_additem: uncovered case of generate1"
4.64 + val pre' = Stool.check_preconds thy prls pre met'
4.65 + val pb = foldl and_ (true, map fst pre')
4.66 + val (p_, nxt) =
4.67 + nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
4.68 + ((#ppc o Specify.get_pbt) cpI,ppc) (dI,pI,mI);
4.69 + in
4.70 + ("ok", ([], [], (pt', (p, p_))))
4.71 + end
4.72 + | Err msg =>
4.73 + let
4.74 + val pre' = Stool.check_preconds thy prls pre met
4.75 + val pb = foldl and_ (true, map fst pre')
4.76 + val (p_, nxt) =
4.77 + nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
4.78 + ((#ppc o Specify.get_pbt) cpI,(#ppc o Specify.get_met) cmI) (dI,pI,mI);
4.79 + in
4.80 + (msg, ([], [], (pt, (p, p_))))
4.81 + end
4.82 + end
4.83 + | specify_additem sel ct (pt, (p,_(*Frm, Pbl*))) =
4.84 + let
4.85 + val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of
4.86 + (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
4.87 + => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
4.88 + | _ => error "specify_additem Frm, Pbl: uncovered case of get_obj I pt p"
4.89 + val thy = if dI = Rule.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI
4.90 + val cpI = if pI = Celem.e_pblID then pI' else pI
4.91 + val cmI = if mI = Celem.e_metID then mI' else mI
4.92 + val {ppc, where_, prls, ...} = Specify.get_pbt cpI
4.93 + in
4.94 + case appl_add ctxt sel oris pbl ppc ct of
4.95 + Add itm => (*..union old input *)
4.96 + let
4.97 + val pbl' = insert_ppc thy itm pbl
4.98 + val arg = case sel of
4.99 + "#Given" => Tactic.Add_Given' (ct, pbl')
4.100 + | "#Find" => Tactic.Add_Find' (ct, pbl')
4.101 + | "#Relate"=> Tactic.Add_Relation'(ct, pbl')
4.102 + | str => error ("specify_additem Frm, Pbl: uncovered case with " ^ str)
4.103 + val (p, pt') = case Generate.generate1 thy arg (Istate_Def.Uistate, ctxt) (p,Pbl) pt of
4.104 + ((p, Pbl), _, _, pt') => (p, pt')
4.105 + | _ => error "specify_additem: uncovered case of Generate.generate1"
4.106 + val pre = Stool.check_preconds thy prls where_ pbl'
4.107 + val pb = foldl and_ (true, map fst pre)
4.108 + val (p_, nxt) =
4.109 + nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
4.110 + val ppc = if p_= Pbl then pbl' else met
4.111 + in
4.112 + ("ok", ([], [], (pt', (p, p_))))
4.113 + end
4.114 + | Err msg =>
4.115 + let
4.116 + val pre = Stool.check_preconds thy prls where_ pbl
4.117 + val pb = foldl and_ (true, map fst pre)
4.118 + val (p_, nxt) =
4.119 + nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
4.120 + (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
4.121 + in
4.122 + (msg, ([], [], (pt, (p, p_))))
4.123 + end
4.124 + end
4.125 +\<close> ML \<open>
4.126 +specify_additem: string -> Rule.cterm' -> Calc.T -> string * Chead.calcstate'
4.127 +\<close> ML \<open>
4.128 +\<close> ML \<open>
4.129 +\<close> ML \<open>
4.130 +fun by_tactic (Tactic.Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ =
4.131 + let (* either """"""""""""""" all empty or complete *)
4.132 + val thy = Celem.assoc_thy dI'
4.133 + val (oris, ctxt) =
4.134 + if dI' = Rule.e_domID orelse pI' = Celem.e_pblID (*andalso? WN110511*)
4.135 + then ([], ContextC.e_ctxt)
4.136 + else pI' |> #ppc o Specify.get_pbt |> Specify.prep_ori fmz thy
4.137 + (* these are deprecated vvvvvvvvvvvvvvvvvvvvvvvvvv*)
4.138 + val (pt, _) = cappend_problem e_ctree [] (Istate_Def.e_istate, ctxt) (fmz, spec')
4.139 + (oris, (dI',pI',mI'), Rule.e_term)
4.140 + val pt = update_loc' pt [] (SOME (Istate_Def.e_istate, ctxt), NONE)
4.141 + in
4.142 + case mI' of
4.143 + ["no_met"] => ("Refine_Tacitly", ([], [], (pt, ([], Pbl))))
4.144 + | _ => ("ok", ([], [], (pt, ([], Pbl))))
4.145 + end
4.146 + (* ONLY for STARTING modeling phase *)
4.147 + | by_tactic (Tactic.Model_Problem' (_, pbl, met)) (pt, pos as (p, _)) =
4.148 + let
4.149 + val (oris, dI',pI',mI', dI, ctxt) = case get_obj I pt p of
4.150 + PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, _), ctxt, ...} =>
4.151 + (oris, dI',pI',mI', dI, ctxt)
4.152 + | _ => error "Step_Solve.by_tactic (Model_Problem': uncovered case get_obj"
4.153 + val thy' = if dI = Rule.e_domID then dI' else dI
4.154 + val thy = Celem.assoc_thy thy'
4.155 + val {ppc, prls, where_, ...} = Specify.get_pbt pI'
4.156 + val pre = Stool.check_preconds thy prls where_ pbl
4.157 + val pb = foldl and_ (true, map fst pre)
4.158 + val ((p, _), _, _, pt) =
4.159 + Generate.generate1 thy (Tactic.Model_Problem'([],pbl,met)) (Istate_Def.Uistate, ctxt) pos pt
4.160 + val (_, _) = Chead.nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
4.161 + (ppc,(#ppc o Specify.get_met) mI') (dI',pI',mI');
4.162 + in
4.163 + ("ok", ([], [], (pt, (p, Pbl))))
4.164 + end
4.165 + (* called only if no_met is specified *)
4.166 + | by_tactic (Tactic.Refine_Tacitly' (pI, pIre, _, _, _)) (pt, pos) =
4.167 + let
4.168 +(* val (dI', ctxt) = case get_obj I pt p of
4.169 + PblObj {origin= (_, (dI', _, _), _), ctxt, ...} => (dI', ctxt)
4.170 + | _ => error "Step_Solve.by_tactic (Refine_Tacitly': uncovered case get_obj"*)
4.171 + val {met, thy,...} = Specify.get_pbt pIre
4.172 + val (domID, metID) = (Rule.string_of_thy thy, if length met = 0 then Celem.e_metID else hd met)
4.173 + val ((p,_), _, _, pt) =
4.174 + Generate.generate1 thy (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)]))
4.175 + (Istate_Def.Uistate, ContextC.e_ctxt) pos pt
4.176 +(* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
4.177 +(* val (pbl, pre, _) = ([], [], false)*)
4.178 + in
4.179 + ("ok", ([], [], (pt,(p, Pbl))))
4.180 + end
4.181 + | by_tactic (Tactic.Refine_Problem' rfd) (pt, pos) =
4.182 + let
4.183 + val ctxt = get_ctxt pt pos
4.184 + val (pos, _, _, pt) =
4.185 + Generate.generate1 (Celem.assoc_thy "Isac_Knowledge")
4.186 + (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) pos pt
4.187 + in
4.188 + ("ok", ([], [], (pt,pos)))
4.189 + end
4.190 + (*WN110515 initialise ctxt again from itms and add preconds*)
4.191 + | by_tactic (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (pt, pos as (p,_)) =
4.192 + let
4.193 + val (oris, dI', pI', mI', dI, mI, ctxt, met) = case get_obj I pt p of
4.194 + PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, mI), ctxt, meth = met, ...} =>
4.195 + (oris, dI', pI', mI', dI, mI, ctxt, met)
4.196 + | _ => error "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"
4.197 + val thy = Celem.assoc_thy dI
4.198 + val (p, pt) =
4.199 + case Generate.generate1 thy (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (Istate_Def.Uistate, ctxt) pos pt of
4.200 + ((p, Pbl), _, _, pt) => (p, pt)
4.201 + | _ => error "Step_Solve.by_tactic (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"
4.202 + val dI'' = Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)
4.203 + val mI'' = if mI = Celem.e_metID then mI' else mI
4.204 + val (_, nxt) = Chead.nxt_spec Pbl ok oris (dI', pI', mI') (itms, met) ((#ppc o Specify.get_pbt) pI,
4.205 + (#ppc o Specify.get_met) mI'') (dI, pI, mI);
4.206 + in
4.207 + ("ok", ([], [], (pt, (p, Pbl))))
4.208 + end
4.209 + (*WN110515 initialise ctxt again from itms and add preconds*)
4.210 + | by_tactic (Tactic.Specify_Method' (mID, _, _)) (pt,pos as (p, _)) =
4.211 + let
4.212 + val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of
4.213 + PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
4.214 + (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
4.215 + | _ => error "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"
4.216 + val {ppc, pre, prls,...} = Specify.get_met mID
4.217 + val thy = Celem.assoc_thy dI
4.218 + val dI'' = if dI = Rule.e_domID then dI' else dI
4.219 + val pI'' = if pI = Celem.e_pblID then pI' else pI
4.220 + val oris = Specify.add_field' thy ppc oris
4.221 + val met = if met = [] then pbl else met
4.222 + val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls) oris
4.223 + val itms = Specify.hack_until_review_Specify_1 mI' itms
4.224 + val (pos, _, _, pt) =
4.225 + Generate.generate1 thy (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) pos pt
4.226 + val (_, nxt) = Chead.nxt_spec Met true oris (dI', pI',mI') (pbl, itms)
4.227 + ((#ppc o Specify.get_pbt) pI'', ppc) (dI'', pI'', mID)
4.228 + in
4.229 + ("ok", ([], [], (pt, pos)))
4.230 + end
4.231 + | by_tactic (Tactic.Add_Given' (ct, _)) (pt, p) = specify_additem "#Given" ct (pt, p)
4.232 + | by_tactic (Tactic.Add_Find' (ct, _)) (pt, p) = specify_additem "#Find" ct (pt, p)
4.233 + | by_tactic (Tactic.Add_Relation' (ct, _)) (pt, p) = specify_additem"#Relate" ct (pt, p)
4.234 + | by_tactic (Tactic.Specify_Theory' domID) (pt, pos as (p,p_)) =
4.235 + let
4.236 + val p_ = case p_ of Met => Met | _ => Pbl
4.237 + val thy = Celem.assoc_thy domID
4.238 + val (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt) = case get_obj I pt p of
4.239 + PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, mI), probl = pbl, meth = met, ctxt, ...} =>
4.240 + (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt)
4.241 + | _ => error "Step_Solve.by_tactic (Specify_Theory': uncovered case get_obj"
4.242 + val mppc = case p_ of Met => met | _ => pbl
4.243 + val cpI = if pI = Celem.e_pblID then pI' else pI
4.244 + val {prls = per, ppc, where_ = pwh, ...} = Specify.get_pbt cpI
4.245 + val cmI = if mI = Celem.e_metID then mI' else mI
4.246 + val {prls = mer, ppc = mpc, pre= mwh, ...} = Specify.get_met cmI
4.247 + val pre = case p_ of
4.248 + Met => (Stool.check_preconds thy mer mwh met)
4.249 + | _ => (Stool.check_preconds thy per pwh pbl)
4.250 + val pb = foldl and_ (true, map fst pre)
4.251 + in
4.252 + if domID = dI
4.253 + then
4.254 + let val (p_, nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI)
4.255 + in
4.256 + ("ok", ([], [], (pt, (p, p_))))
4.257 + end
4.258 + else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
4.259 + let
4.260 + val ((p, p_), _, _, pt) = Generate.generate1 thy (Tactic.Specify_Theory' domID) (Istate_Def.Uistate, ctxt) (p,p_) pt
4.261 + val (p_,nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI)
4.262 + in
4.263 + ("ok", ([], [], (pt, (p, p_))))
4.264 + end
4.265 + end
4.266 + | by_tactic _ _ = raise ERROR "Step_Specify.by_tactic uncovered pattern in fun.def"
4.267 +\<close> ML \<open>
4.268 +\<close> ML \<open>
4.269 +\<close> ML \<open>
4.270 +by_tactic: Tactic.T -> Calc.T -> string * Chead.calcstate'
4.271 +\<close> ML \<open>
4.272 +\<close> ML \<open>
4.273 +\<close> ML \<open>
4.274 +(*-------------------------------------------------------------------------------------------* )
4.275 + | by_tactic m' _ _ _ = error ("specify: not impl. for " ^ Tactic.string_of m')
4.276 +( *-------------------------------------------------------------------------------------------*)
4.277 +\<close> ML \<open>
4.278 +\<close> ML \<open>
4.279 +specify : Tactic.T -> Ctree.pos' -> Ctree.cid -> Ctree.ctree ->
4.280 + Ctree.pos' * (Ctree.pos' * Istate_Def.T) * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
4.281 +\<close> ML \<open>
4.282 +\<close> ML \<open>
4.283 +\<close> ML \<open>
4.284 +\<close> ML \<open>
4.285 +\<close> ML \<open>
4.286 +\<close> ML \<open>
4.287 \<close> ML \<open>
4.288 \<close>
4.289 end
5.1 --- a/src/Tools/isac/Specify/calchead.sml Tue Feb 11 11:58:45 2020 +0100
5.2 +++ b/src/Tools/isac/Specify/calchead.sml Tue Feb 11 17:25:45 2020 +0100
5.3 @@ -111,9 +111,9 @@
5.4 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
5.5 val e_calcstate : Calc.T * Generate.taci list
5.6 val e_calcstate' : calcstate'
5.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.8 - val posterms2str : (pos' * term * 'a) list -> string
5.9 - val postermtacs2str : (pos' * term * Tactic.input option) list -> string
5.10 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
5.11 + val posterms2str : (Pos.pos' * term * 'a) list -> string
5.12 + val postermtacs2str : (Pos.pos' * term * Tactic.input option) list -> string
5.13 val is_copy_named_idstr : string -> bool
5.14 val is_copy_named_generating_idstr : string -> bool
5.15 val is_copy_named_generating : 'a * ('b * term) -> bool
5.16 @@ -126,7 +126,7 @@
5.17 val appl_add: Proof.context -> string -> Model.ori list ->
5.18 Model.itm list -> (string * (term * term)) list -> Rule.cterm' -> additm
5.19 val seek_oridts: Proof.context -> ''a -> term * term list -> (int * 'b list * ''a * term * term list) list -> string * (int * 'b list * ''a * term * term list) * term list
5.20 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.21 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.22
5.23 (*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*)
5.24 val variants_in : term list -> int
6.1 --- a/src/Tools/isac/Specify/generate.sml Tue Feb 11 11:58:45 2020 +0100
6.2 +++ b/src/Tools/isac/Specify/generate.sml Tue Feb 11 17:25:45 2020 +0100
6.3 @@ -5,8 +5,6 @@
6.4
6.5 signature GENERATE_CALC_TREE =
6.6 sig
6.7 - (* vvv request into signature is incremental with *.sml *)
6.8 - (* for calchead.sml --------------------------------------------------------------- vvv *)
6.9 type taci
6.10 val e_taci : taci
6.11 datatype pblmet = Method of Celem.metID | Problem of Celem.pblID | Upblmet
7.1 --- a/src/Tools/isac/TODO.thy Tue Feb 11 11:58:45 2020 +0100
7.2 +++ b/src/Tools/isac/TODO.thy Tue Feb 11 17:25:45 2020 +0100
7.3 @@ -29,9 +29,9 @@
7.4 -> Rule.rls(*..\<in> ist \<rightarrow> REMOVE*) * (Istate.T * Proof.context) * Program.T
7.5 \item init_istate ?-> Detail_Rls?
7.6 \item xxx
7.7 + \item rename Ctree.pos' --> Pos.pos', type decl duplicate? delete, separate!
7.8 \item xxx
7.9 - \item xxx
7.10 - \item xxx
7.11 + \item Istate_Def.e_istate -> Istate.empty
7.12 \item xxx
7.13 \item xxx
7.14 \item xxx