1.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Mon Dec 23 15:41:36 2019 +0100
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Mon Dec 23 16:38:09 2019 +0100
1.3 @@ -100,7 +100,7 @@
1.4 compare "fun CalcTreeTEST" which does NOT decode.*)
1.5 fun CalcTree [(fmz, sp)] (*for several variants lateron*) =
1.6 ((let
1.7 - val cs = Chead.nxt_specify_init_calc (encode_fmz (fmz, sp))
1.8 + val cs = SpecifyNEW.nxt_specify_init_calc (encode_fmz (fmz, sp))
1.9 val cI = add_calc cs (*FIXME.WN.8.03: error-handling missing*)
1.10 in calctreeOK2xml cI end)
1.11 handle _ => sysERROR2xml 0 "error in kernel 2")
1.12 @@ -309,7 +309,7 @@
1.13 fun modelProblem cI =
1.14 (let val (ptp, _) = get_calc cI
1.15 val ptp = Chead.reset_calchead ptp
1.16 - val (_, _, ptp) = Chead.nxt_specif Tactic.Model_Problem ptp
1.17 + val (_, _, ptp) = Step_Specify.by_tactic Tactic.Model_Problem ptp
1.18 in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (Chead.get_ocalhd ptp)) end)
1.19 handle _ => sysERROR2xml cI "error in kernel 11";
1.20
2.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Mon Dec 23 15:41:36 2019 +0100
2.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Mon Dec 23 16:38:09 2019 +0100
2.3 @@ -32,7 +32,6 @@
2.4 datatype lOc_ = ERror of string | UNsafe of Chead.calcstate' | Updated of Chead.calcstate'
2.5 val loc_solve_ : Tactic.T -> Ctree.ctree * Ctree.pos' -> lOc_
2.6 val loc_specify_ : Tactic.T -> Ctree.state -> lOc_
2.7 - val nxt_specify_: Ctree.ctree * Ctree.pos' -> string * Chead.calcstate'
2.8 val TESTg_form : Ctree.state -> Generate.mout
2.9 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.10
2.11 @@ -88,46 +87,11 @@
2.12 (*for SEVER.tacs user to ask ? *)
2.13 end
2.14
2.15 -(* iterated by nxt_me; there (the resulting) ptp dropped
2.16 - may call nxt_solve Apply_Method --- thus evaluated here after solve.sml *)
2.17 -fun nxt_specify_ (ptp as (pt, (p, p_))) =
2.18 - let
2.19 - val (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) =
2.20 - case Ctree.get_obj I pt p of
2.21 - pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
2.22 - probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)
2.23 - | Ctree.PrfObj _ => error "nxt_specify_: not on PrfObj"
2.24 - in
2.25 - if Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin
2.26 - then
2.27 - case mI' of
2.28 - ["no_met"] => ("dummy", Chead.nxt_specif (Tactic.Refine_Tacitly pI') (pt, (p, Pos.Pbl)))
2.29 - | _ => ("dummy", Chead.nxt_specif Tactic.Model_Problem (pt, (p, Pos.Pbl)))
2.30 - else
2.31 - let
2.32 - val cpI = if pI = Celem.e_pblID then pI' else pI;
2.33 - val cmI = if mI = Celem.e_metID then mI' else mI;
2.34 - val {ppc, prls, where_, ...} = Specify.get_pbt cpI;
2.35 - val pre = Stool.check_preconds "thy 100820" prls where_ probl;
2.36 - val pb = foldl and_ (true, map fst pre);
2.37 - (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
2.38 - val (_, tac) =
2.39 - Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
2.40 - val ist_ctxt = Ctree.get_loc pt (p, p_)
2.41 - in
2.42 - case tac of
2.43 - Tactic.Apply_Method mI =>
2.44 - LucinNEW.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt))
2.45 - ist_ctxt ptp
2.46 - | _ => ("dummy", Chead.nxt_specif tac ptp)
2.47 - end
2.48 - end
2.49 -
2.50 (* specify a new method; WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' *)
2.51 fun set_method mI ptp =
2.52 let
2.53 val (mits, pt, p) =
2.54 - case Chead.nxt_specif (Tactic.Specify_Method mI) ptp of
2.55 + case Step_Specify.by_tactic (Tactic.Specify_Method mI) ptp of
2.56 ([(_, Tactic.Specify_Method' (_, _, mits), _)], [], (pt, (p, _))) => (mits, pt, p)
2.57 | _ => error "set_method: case 1 uncovered"
2.58 val pre = [] (*...from Specify_Method'*)
2.59 @@ -145,7 +109,7 @@
2.60 fun set_problem pI ptp =
2.61 let
2.62 val (complete, pits, pre, pt, p) =
2.63 - case Chead.nxt_specif (Tactic.Specify_Problem pI) ptp of
2.64 + case Step_Specify.by_tactic (Tactic.Specify_Problem pI) ptp of
2.65 ([(_, Tactic.Specify_Problem' (_, (complete, (pits, pre))),_)], _, (pt, (p,_)))
2.66 => (complete, pits, pre, pt, p)
2.67 | _ => error "set_problem: case 1 uncovered"
2.68 @@ -161,7 +125,7 @@
2.69 fun set_theory tI ptp =
2.70 let
2.71 val (complete, pits, pre, pt, p) =
2.72 - case Chead.nxt_specif (Tactic.Specify_Theory tI) ptp of
2.73 + case Step_Specify.by_tactic (Tactic.Specify_Theory tI) ptp of
2.74 ([(_, Tactic.Specify_Problem' (_, (complete, (pits, pre))), _)], _, (pt, (p, _)))
2.75 => (complete, pits, pre, pt, p)
2.76 | _ => error "set_theory: case 1 uncovered"
2.77 @@ -368,7 +332,7 @@
2.78 compare "fun CalcTree" which DOES decode *)
2.79 fun CalcTreeTEST [(fmz, sp)] =
2.80 let
2.81 - val ((pt, p), tacis) = Chead.nxt_specify_init_calc (fmz, sp)
2.82 + val ((pt, p), tacis) = SpecifyNEW.nxt_specify_init_calc (fmz, sp)
2.83 val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
2.84 val f = TESTg_form (pt,p)
2.85 in (p, []:NEW, f, tac, Telem.Sundef, pt) end
3.1 --- a/src/Tools/isac/MathEngine/step.sml Mon Dec 23 15:41:36 2019 +0100
3.2 +++ b/src/Tools/isac/MathEngine/step.sml Mon Dec 23 16:38:09 2019 +0100
3.3 @@ -21,7 +21,6 @@
3.4 structure Step(**): STEP(**) =
3.5 struct
3.6
3.7 -(* was fun Math_Engine.nxt_specify_, should go to Step_specify.do_next *)
3.8 fun specify_do_next (ptp as (pt, (p, p_))) =
3.9 let
3.10 val (_, (p_', tac)) = SpecifyNEW.find_next_tactic ptp
4.1 --- a/src/Tools/isac/Specify/Specify.thy Mon Dec 23 15:41:36 2019 +0100
4.2 +++ b/src/Tools/isac/Specify/Specify.thy Mon Dec 23 16:38:09 2019 +0100
4.3 @@ -11,8 +11,8 @@
4.4 ML_file generate.sml
4.5 ML_file calchead.sml
4.6 ML_file appl.sml
4.7 + ML_file "step-specify.sml"
4.8 ML_file specify.sml
4.9 - ML_file "step-specify.sml"
4.10
4.11 ML \<open>
4.12 \<close> ML \<open>
5.1 --- a/src/Tools/isac/Specify/calchead.sml Mon Dec 23 15:41:36 2019 +0100
5.2 +++ b/src/Tools/isac/Specify/calchead.sml Mon Dec 23 16:38:09 2019 +0100
5.3 @@ -69,10 +69,8 @@
5.4 type calcstate
5.5 type calcstate'
5.6
5.7 - val nxt_specify_init_calc : Selem.fmz -> calcstate
5.8 val specify : Tactic.T -> Ctree.pos' -> Ctree.cid -> Ctree.ctree ->
5.9 Ctree.pos' * (Ctree.pos' * Istate_Def.T) * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
5.10 - val nxt_specif : Tactic.input -> Ctree.state -> calcstate'
5.11 val nxt_spec : Ctree.pos_ -> bool -> Model.ori list -> Celem.spec -> Model.itm list * Model.itm list ->
5.12 (string * (term * 'a)) list * (string * (term * 'b)) list -> Celem.spec -> Ctree.pos_ * Tactic.input
5.13
5.14 @@ -109,13 +107,13 @@
5.15 val is_error: Model.itm_ -> bool
5.16 val complete_mod_: (int * int list * string * term * term list) list * ('a * (term * term)) list * ('b * (term * term)) list * Model.itm list -> Model.itm list * Model.itm list
5.17 val nxt_specif_additem: string -> Rule.cterm' -> Ctree.state -> calcstate'
5.18 + val vals_of_oris : Model.ori list -> term list
5.19 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
5.20 val e_calcstate : Ctree.state * Generate.taci list
5.21 val e_calcstate' : calcstate'
5.22 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.23 val posterms2str : (pos' * term * 'a) list -> string
5.24 val postermtacs2str : (pos' * term * Tactic.input option) list -> string
5.25 - val vals_of_oris : Model.ori list -> term list
5.26 val is_copy_named_idstr : string -> bool
5.27 val is_copy_named_generating_idstr : string -> bool
5.28 val is_copy_named_generating : 'a * ('b * term) -> bool
5.29 @@ -139,7 +137,6 @@
5.30 val chktyps : theory -> term list * term list -> term list (* only in old tests*)
5.31 val chk_vars : term Model.ppc -> string * term list
5.32 val unbound_ppc : term Model.ppc -> term list
5.33 - val nxt_model_pbl : Tactic.T -> Ctree.state -> Tactic.T
5.34 val is_complete_modspec : Ctree.state -> bool
5.35 val get_formress : (string * Ctree.pos' * term) list list -> Ctree.pos -> Ctree.ctree list ->
5.36 (string * Ctree.pos' * term) list
5.37 @@ -1027,191 +1024,11 @@
5.38 if pI = Celem.e_pblID then opI else pI,
5.39 if mI = Celem.e_metID then omI else mI)
5.40
5.41 -(* find a next applicable tac (for calcstate) and update ctree
5.42 - (for ev. finding several more tacs due to hide) *)
5.43 -(* FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !! *)
5.44 -(* WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg *)
5.45 -(* WN.24.10.03 fun by_tactic = ...................................?? *)
5.46 -fun nxt_specif (tac as Tactic.Model_Problem) (pt, pos as (p, _)) =
5.47 - let
5.48 - val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of
5.49 - PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt)
5.50 - | _ => error "nxt_specif Model_Problem; uncovered case get_obj"
5.51 - val (dI, pI, mI) = some_spec ospec spec
5.52 - val thy = Celem.assoc_thy dI
5.53 - val mpc = (#ppc o Specify.get_met) mI (* just for reuse complete_mod_ *)
5.54 - val {cas, ppc, ...} = Specify.get_pbt pI
5.55 - val pbl = Generate.init_pbl ppc (* fill in descriptions *)
5.56 - (*----------------if you think, this should be done by the Dialog
5.57 - in the java front-end, search there for WN060225-modelProblem----*)
5.58 - val (pbl, met) = case cas of
5.59 - NONE => (pbl, [])
5.60 - | _ => complete_mod_ (oris, mpc, ppc, probl)
5.61 - (*----------------------------------------------------------------*)
5.62 - val tac_ = Tactic.Model_Problem' (pI, pbl, met)
5.63 - val (pos,c,_,pt) = Generate.generate1 thy tac_ (Istate_Def.Uistate, ctxt) pos pt
5.64 - in ([(tac, tac_, (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt,pos)) end
5.65 - | nxt_specif (Tactic.Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
5.66 - | nxt_specif (Tactic.Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
5.67 - | nxt_specif (Tactic.Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
5.68 - (*. called only if no_met is specified .*)
5.69 - | nxt_specif (Tactic.Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
5.70 - let
5.71 - val (oris, dI, ctxt) = case get_obj I pt p of
5.72 - (PblObj {origin = (oris, (dI, _, _), _), ctxt, ...}) => (oris, dI, ctxt)
5.73 - | _ => error "nxt_specif Refine_Tacitly: uncovered case get_obj"
5.74 - val opt = Specify.refine_ori oris pI
5.75 - in
5.76 - case opt of
5.77 - SOME pI' =>
5.78 - let
5.79 - val {met, ...} = Specify.get_pbt pI'
5.80 - (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
5.81 - val mI = if length met = 0 then Celem.e_metID else hd met
5.82 - val thy = Celem.assoc_thy dI
5.83 - val (pos, c, _, pt) =
5.84 - Generate.generate1 thy (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) pos pt
5.85 - in
5.86 - ([(Tactic.Refine_Tacitly pI, Tactic.Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
5.87 - (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt,pos))
5.88 - end
5.89 - | NONE => ([], [], ptp)
5.90 - end
5.91 - | nxt_specif (Tactic.Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
5.92 - let
5.93 - val (dI, dI', probl, ctxt) = case get_obj I pt p of
5.94 - PblObj {origin= (_, (dI, _, _), _), spec = (dI', _, _), probl, ctxt, ...} =>
5.95 - (dI, dI', probl, ctxt)
5.96 - | _ => error "nxt_specif Refine_Problem: uncovered case get_obj"
5.97 - val thy = if dI' = Rule.e_domID then dI else dI'
5.98 - in
5.99 - case Specify.refine_pbl (Celem.assoc_thy thy) pI probl of
5.100 - NONE => ([], [], ptp)
5.101 - | SOME rfd =>
5.102 - let
5.103 - val (pos,c,_,pt) = Generate.generate1 (Celem.assoc_thy thy) (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) pos pt
5.104 - in
5.105 - ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' rfd, (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt,pos))
5.106 - end
5.107 - end
5.108 - | nxt_specif (Tactic.Specify_Problem pI) (pt, pos as (p,_)) =
5.109 - let
5.110 - val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
5.111 - PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
5.112 - (oris, dI, dI', pI', probl, ctxt)
5.113 - | _ => error ""
5.114 - val thy = Celem.assoc_thy (if dI' = Rule.e_domID then dI else dI');
5.115 - val {ppc,where_,prls,...} = Specify.get_pbt pI
5.116 - val pbl =
5.117 - if pI' = Celem.e_pblID andalso pI = Celem.e_pblID
5.118 - then (false, (Generate.init_pbl ppc, []))
5.119 - else Specify.match_itms_oris thy probl (ppc,where_,prls) oris
5.120 - (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
5.121 - val (c, pt) = case Generate.generate1 thy (Tactic.Specify_Problem' (pI, pbl)) (Istate_Def.Uistate, ctxt) pos pt of
5.122 - ((_, Pbl), c, _, pt) => (c, pt)
5.123 - | _ => error ""
5.124 - in
5.125 - ([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, pbl), (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt,pos))
5.126 - end
5.127 - (* transfers oris (not required in pbl) to met-model for script-env
5.128 - FIXME.WN.8.03: application of several mIDs to SAME model? *)
5.129 - | nxt_specif (Tactic.Specify_Method mID) (pt, pos as (p,_)) =
5.130 - let
5.131 - val (oris, pbl, dI, met, ctxt) = case get_obj I pt p of
5.132 - PblObj {origin = (oris, _, _), probl = pbl, spec = (dI, _, _), meth=met, ctxt, ...}
5.133 - => (oris, pbl, dI, met, ctxt)
5.134 - | _ => error "nxt_specif Specify_Method: uncovered case get_obj"
5.135 - val {ppc,pre,prls,...} = Specify.get_met mID
5.136 - val thy = Celem.assoc_thy dI
5.137 - val oris = Specify.add_field' thy ppc oris
5.138 - val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
5.139 - val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc,pre,prls ) oris
5.140 - val itms = Specify.hack_until_review_Specify_2 mID itms
5.141 - val (pos, c, _, pt) =
5.142 - Generate.generate1 thy (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) pos pt
5.143 - in
5.144 - ([(Tactic.Specify_Method mID, Tactic.Specify_Method' (mID, oris, itms), (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt, pos))
5.145 - end
5.146 - | nxt_specif (Tactic.Specify_Theory dI) (pt, pos as (_, Pbl)) =
5.147 - let
5.148 - val ctxt = get_ctxt pt pos
5.149 - val (pos, c, _, pt) =
5.150 - Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") (Tactic.Specify_Theory' dI) (Istate_Def.Uistate, ctxt) pos pt
5.151 - in (*FIXXXME: check if pbl can still be parsed*)
5.152 - ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI, (pos, (Istate_Def.Uistate, ctxt)))], c,
5.153 - (pt, pos))
5.154 - end
5.155 - | nxt_specif (Tactic.Specify_Theory dI) (pt, pos as (_, Met)) =
5.156 - let
5.157 - val ctxt = get_ctxt pt pos
5.158 - val (pos, c, _, pt) = Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") (Tactic.Specify_Theory' dI) (Istate_Def.Uistate, ctxt) pos pt
5.159 - in (*FIXXXME: check if met can still be parsed*)
5.160 - ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI, (pos, (Istate_Def.Uistate, ctxt)))], c, (pt, pos))
5.161 - end
5.162 - | nxt_specif m' _ = error ("nxt_specif: not impl. for " ^ Tactic.tac2str m')
5.163 -
5.164 (* get the values from oris; handle the term list w.r.t. penv *)
5.165 -fun vals_of_oris oris =
5.166 +fun vals_of_oris (oris: Model.ori list) =
5.167 ((map (Model.mkval' o (#5))) o
5.168 (filter ((member_swap op= 1) o (#2)))) oris
5.169
5.170 -(* create a calc-tree with oris via an cas.refined pbl *)
5.171 -fun nxt_specify_init_calc ([], (dI, pI, mI)) =
5.172 - if pI <> []
5.173 - then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
5.174 - let
5.175 - val {cas, met, ppc, thy, ...} = Specify.get_pbt pI
5.176 - val dI = if dI = "" then Rule.theory2theory' thy else dI
5.177 - val mI = if mI = [] then hd met else mI
5.178 - val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t
5.179 - val (pt,_) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.e_ctxt) ([], (dI, pI, mI))
5.180 - ([], (dI,pI,mI), hdl)
5.181 - val pt = update_spec pt [] (dI, pI, mI)
5.182 - val pits = Generate.init_pbl' ppc
5.183 - val pt = update_pbl pt [] pits
5.184 - in ((pt, ([] , Pbl)), []) end
5.185 - else
5.186 - if mI <> []
5.187 - then (* from met-browser *)
5.188 - let
5.189 - val {ppc, ...} = Specify.get_met mI
5.190 - val dI = if dI = "" then "Isac_Knowledge" else dI
5.191 - val (pt, _) =
5.192 - cappend_problem e_ctree [] (Istate_Def.e_istate, ContextC.e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), Rule.e_term (*FIXME met*))
5.193 - val pt = update_spec pt [] (dI, pI, mI)
5.194 - val mits = Generate.init_pbl' ppc
5.195 - val pt = update_met pt [] mits
5.196 - in ((pt, ([], Met)), []) end
5.197 - else (* new example, pepare for interactive modeling *)
5.198 - let
5.199 - val (pt, _) =
5.200 - cappend_problem e_ctree [] (Istate_Def.e_istate, ContextC.e_ctxt) ([], Celem.e_spec) ([], Celem.e_spec, Rule.e_term)
5.201 - in ((pt, ([], Pbl)), []) end
5.202 - | nxt_specify_init_calc (fmz, (dI, pI, mI)) =
5.203 - let (* both """"""""""""""""""""""""" either empty or complete *)
5.204 - val thy = Celem.assoc_thy dI
5.205 - val (pI, (pors, pctxt), mI) =
5.206 - if mI = ["no_met"]
5.207 - then
5.208 - let
5.209 - val (pors, pctxt) = Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy;
5.210 - val pI' = Specify.refine_ori' pors pI;
5.211 - in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
5.212 - (hd o #met o Specify.get_pbt) pI')
5.213 - end
5.214 - else (pI, Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy, mI)
5.215 - val {cas, ppc, thy = thy', ...} = Specify.get_pbt pI (*take dI from _refined_ pbl*)
5.216 - val dI = Rule.theory2theory' (Stool.common_subthy (thy, thy'))
5.217 - val hdl = case cas of
5.218 - NONE => Auto_Prog.pblterm dI pI
5.219 - | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
5.220 - val (pt, _) =
5.221 - cappend_problem e_ctree [] (Istate_Def.e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl)
5.222 - val pt = update_ctxt pt [] pctxt
5.223 - in
5.224 - ((pt, ([], Pbl)), fst3 (nxt_specif Tactic.Model_Problem (pt, ([], Pbl))))
5.225 - end
5.226 -
5.227 (* fun tag_form thy (formal, given) = Thm.global_cterm_of thy
5.228 (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *)
5.229 fun tag_form thy (formal, given) =
5.230 @@ -1248,14 +1065,6 @@
5.231 distinct (subtract op = (union op = gi fi) re)
5.232 end
5.233
5.234 -(* called only once, if a Subproblem has been located in the script*)
5.235 -fun nxt_model_pbl (Tactic.Subproblem' ((_, pblID, metID), _, _, _, _, _)) ptp =
5.236 - (case metID of
5.237 - ["no_met"] => (snd3 o hd o fst3) (nxt_specif (Tactic.Refine_Tacitly pblID) ptp)
5.238 - | _ => (snd3 o hd o fst3) (nxt_specif Tactic.Model_Problem ptp))
5.239 - (*all stored in tac_ itms^^^^^^^^^^*)
5.240 - | nxt_model_pbl tac_ _ = error ("nxt_model_pbl: called by tac= " ^ Tactic.string_of tac_)
5.241 -
5.242 (* complete _NON_empty calc-head for autocalc (sub-)pbl from oris
5.243 + met from fmz; assumes pos on PblObj, meth = [] *)
5.244 fun complete_mod (pt, pos as (p, p_) : pos') =
6.1 --- a/src/Tools/isac/Specify/specify.sml Mon Dec 23 15:41:36 2019 +0100
6.2 +++ b/src/Tools/isac/Specify/specify.sml Mon Dec 23 16:38:09 2019 +0100
6.3 @@ -1,6 +1,8 @@
6.4 signature SPECIFY_NEW =
6.5 sig
6.6 val find_next_tactic: Ctree.state -> string * (Pos.pos_ * Tactic.input)
6.7 + val nxt_specify_init_calc : Selem.fmz -> Chead.calcstate
6.8 + val nxt_model_pbl : Tactic.T -> Ctree.state -> Tactic.T
6.9
6.10 end
6.11
6.12 @@ -9,6 +11,7 @@
6.13 struct
6.14 (**)
6.15 open Pos
6.16 +open Ctree
6.17 open Chead
6.18
6.19 (* was Chead.nxt_spec *)
6.20 @@ -73,4 +76,70 @@
6.21 end
6.22 end
6.23
6.24 +(* create a calc-tree with oris via an cas.refined pbl *)
6.25 +fun nxt_specify_init_calc ([], (dI, pI, mI)) =
6.26 + if pI <> []
6.27 + then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
6.28 + let
6.29 + val {cas, met, ppc, thy, ...} = Specify.get_pbt pI
6.30 + val dI = if dI = "" then Rule.theory2theory' thy else dI
6.31 + val mI = if mI = [] then hd met else mI
6.32 + val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t
6.33 + val (pt,_) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.e_ctxt) ([], (dI, pI, mI))
6.34 + ([], (dI,pI,mI), hdl)
6.35 + val pt = update_spec pt [] (dI, pI, mI)
6.36 + val pits = Generate.init_pbl' ppc
6.37 + val pt = update_pbl pt [] pits
6.38 + in ((pt, ([] , Pbl)), []) end
6.39 + else
6.40 + if mI <> []
6.41 + then (* from met-browser *)
6.42 + let
6.43 + val {ppc, ...} = Specify.get_met mI
6.44 + val dI = if dI = "" then "Isac_Knowledge" else dI
6.45 + val (pt, _) =
6.46 + cappend_problem e_ctree [] (Istate_Def.e_istate, ContextC.e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), Rule.e_term (*FIXME met*))
6.47 + val pt = update_spec pt [] (dI, pI, mI)
6.48 + val mits = Generate.init_pbl' ppc
6.49 + val pt = update_met pt [] mits
6.50 + in ((pt, ([], Met)), []) end
6.51 + else (* new example, pepare for interactive modeling *)
6.52 + let
6.53 + val (pt, _) =
6.54 + cappend_problem e_ctree [] (Istate_Def.e_istate, ContextC.e_ctxt) ([], Celem.e_spec) ([], Celem.e_spec, Rule.e_term)
6.55 + in ((pt, ([], Pbl)), []) end
6.56 + | nxt_specify_init_calc (fmz, (dI, pI, mI)) =
6.57 + let (* both """"""""""""""""""""""""" either empty or complete *)
6.58 + val thy = Celem.assoc_thy dI
6.59 + val (pI, (pors, pctxt), mI) =
6.60 + if mI = ["no_met"]
6.61 + then
6.62 + let
6.63 + val (pors, pctxt) = Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy;
6.64 + val pI' = Specify.refine_ori' pors pI;
6.65 + in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
6.66 + (hd o #met o Specify.get_pbt) pI')
6.67 + end
6.68 + else (pI, Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy, mI)
6.69 + val {cas, ppc, thy = thy', ...} = Specify.get_pbt pI (*take dI from _refined_ pbl*)
6.70 + val dI = Rule.theory2theory' (Stool.common_subthy (thy, thy'))
6.71 + val hdl = case cas of
6.72 + NONE => Auto_Prog.pblterm dI pI
6.73 + | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
6.74 + val (pt, _) =
6.75 + cappend_problem e_ctree [] (Istate_Def.e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl)
6.76 + val pt = update_ctxt pt [] pctxt
6.77 + in
6.78 + ((pt, ([], Pbl)), fst3 (Step_Specify.by_tactic Tactic.Model_Problem (pt, ([], Pbl))))
6.79 + end
6.80 +
6.81 +(* called only once, if a Subproblem has been located in the script*)
6.82 +fun nxt_model_pbl (Tactic.Subproblem' ((_, pblID, metID), _, _, _, _, _)) ptp =
6.83 + (case metID of
6.84 + ["no_met"] => (snd3 o hd o fst3) (Step_Specify.by_tactic (Tactic.Refine_Tacitly pblID) ptp)
6.85 + | _ => (snd3 o hd o fst3) (Step_Specify.by_tactic Tactic.Model_Problem ptp))
6.86 + (*all stored in tac_ itms^^^^^^^^^^*)
6.87 + | nxt_model_pbl tac_ _ = error ("nxt_model_pbl: called by tac= " ^ Tactic.string_of tac_)
6.88 +
6.89 +
6.90 end
7.1 --- a/src/Tools/isac/TODO.thy Mon Dec 23 15:41:36 2019 +0100
7.2 +++ b/src/Tools/isac/TODO.thy Mon Dec 23 16:38:09 2019 +0100
7.3 @@ -72,9 +72,7 @@
7.4 \begin{itemize}
7.5 \item Step_Specify.check <-- Applicable.applicable_in
7.6 \item Step_Specify.add <-- Generate.generate1
7.7 - \item Step_Specify.by_tactic : Tactic.input -> Ctree.state -> ...stay as is
7.8 \item Step_Specify.by_formula: ?term? -> Ctree.state -> ...stay as is
7.9 - \item Step_Specify.do_next : Ctree.state -> ...stay as is
7.10 \end{itemize}
7.11 \item Step_Solve in Interpret/step-solve.sml
7.12 \begin{itemize}
7.13 @@ -82,8 +80,6 @@
7.14 inserts all data into Tactic.T available -- not all are at time of call!
7.15 \item Step_Solve.add <-- Generate.generate1
7.16 \item Step_Solve.by_formula : term -> Ctree.state -> ...stay as is
7.17 - \item Step_Solve.do_next : Ctree.state -> ...stay as is
7.18 - ^^^^LucinNEW.do_next
7.19 \end{itemize}
7.20 \item Step in MathEngine/step.sml
7.21 \begin{itemize}
8.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Dec 23 15:41:36 2019 +0100
8.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Dec 23 16:38:09 2019 +0100
8.3 @@ -386,7 +386,7 @@
8.4 val (_, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
8.5
8.6 (*NEW*) val Next_Step (_, _, Rewrite_Set' (_, _, Rls {id = "Test_simplify", ...}, _, _)) = (*case*)
8.7 -(*NEW*) find_next_tactic sc (pt, pos) ist ctxt (*of*);
8.8 +(*NEW*) LucinNEW.find_next_tactic sc (pt, pos) ist ctxt (*of*);
8.9 "~~~~~ fun find_next_tactic , args:"; val (Rule.Prog prog, ptp as (pt, (p, _)), Istate.Pstate ist, ctxt)
8.10 = (sc, (pt, pos), ist, ctxt);
8.11 (*OLD* ) val Accept_Tac2 (m', ist as {act_arg, ...}, ctxt) =
8.12 @@ -405,7 +405,7 @@
8.13 (*NEW*)
8.14 "~~~~~ from fun find_next_tactic\<longrightarrow>and do_next , return:"; val (Next_Step (ist, ctxt, tac))
8.15 = (Next_Step (Istate.Pstate ist, Tactic.insert_assumptions tac ctxt, tac));
8.16 -(*NEW* ) case find_next_tactic sc (pt, pos) ist ctxt of
8.17 +(*NEW* ) case LucinNEW.find_next_tactic sc (pt, pos) ist ctxt of
8.18 (*NEW*) Next_Step (ist, ctxt, tac) =>
8.19 ( *NEW*)
8.20 LucinNEW.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
8.21 @@ -453,14 +453,14 @@
8.22 val (res, asm) = (get_obj g_result pt (fst p));
8.23
8.24 if term2str res = "[x = 1]" andalso terms2str asm = "[\"precond_rootmet 1\"]"
8.25 -then () else error "re-build: fun find_next_tactic CHANGED 1";
8.26 +then () else error "re-build: fu LucinNEW.find_next_tactic CHANGED 1";
8.27
8.28 if p = ([], Und) (*.. should be ([], Res) *)
8.29 then
8.30 case get_obj g_tac pt (fst p) of
8.31 Apply_Method ["Test", "squ-equ-test-subpbl1"] => ((*ok, further tactics are level down*))
8.32 - | _ => error "re-build: fun find_next_tactic CHANGED 3"
8.33 -else error "re-build: fun find_next_tactic CHANGED 2";
8.34 + | _ => error "re-build: fun LucinNEW.find_next_tactic CHANGED 3"
8.35 +else error "re-build: fun LucinNEW.find_next_tactic CHANGED 2";
8.36 \\--------- exception Size raised (line 171 of "./basis/LibrarySupport.sml") ---------------//*)
8.37
8.38
9.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Mon Dec 23 15:41:36 2019 +0100
9.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Mon Dec 23 16:38:09 2019 +0100
9.3 @@ -165,7 +165,7 @@
9.4 val ini = Lucin.init_form thy sc env;
9.5 val p = lev_dn p;
9.6 val NONE = (*case*) ini (*of*);
9.7 - val (m', (is', ctxt'), _) = find_next_tactic sc (pt, (p, Res)) is ctxt;
9.8 + val (m', (is', ctxt'), _) = LucinNEW.find_next_tactic sc (pt, (p, Res)) is ctxt;
9.9 val d = Rule.e_rls (*FIXME: get simplifier from domID*);
9.10 val Safe_Step ((pt', p'), _, _, _) = (*case*) locate_input_tactic sc (pt,(p, Res)) is' ctxt' m' (*of*);
9.11 Safe_Step : state * Istate.T * Proof.context * Tactic.T -> input_tactic_result;
10.1 --- a/test/Tools/isac/MathEngBasic/ctree-navi.sml Mon Dec 23 15:41:36 2019 +0100
10.2 +++ b/test/Tools/isac/MathEngBasic/ctree-navi.sml Mon Dec 23 16:38:09 2019 +0100
10.3 @@ -65,7 +65,7 @@
10.4 val pb = foldl and_ (true, map fst pre);
10.5 val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth)
10.6 (ppc, (#ppc o get_met) cmI) (dI, pI, mI); (*tac = Add_Given "equality (-1 + x = 0)"*)
10.7 -"~~~~~ fun nxt_specif, args:"; val (Add_Given ct, ptp) = (tac, ptp);
10.8 +"~~~~~ fun Step_Specify.by_tactic, args:"; val (Add_Given ct, ptp) = (tac, ptp);
10.9 "~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp);
10.10 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
10.11 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
10.12 @@ -88,7 +88,7 @@
10.13 Err "[error] appl_add: is_known: identifiers [equality] not in example"*)
10.14 nxt_specif_additem "#Given" ct ptp;(*WAS
10.15 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
10.16 -nxt_specif tac ptp;(*WAS
10.17 +Step_Specify.by_tactic tac ptp;(*WAS
10.18 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
10.19 nxt_specify_ (pt,ip); (*WAS
10.20 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
11.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml Mon Dec 23 15:41:36 2019 +0100
11.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml Mon Dec 23 16:38:09 2019 +0100
11.3 @@ -65,7 +65,7 @@
11.4 val pb = foldl and_ (true, map fst pre);
11.5 val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth)
11.6 (ppc, (#ppc o get_met) cmI) (dI, pI, mI); (*tac = Add_Given "equality (-1 + x = 0)"*)
11.7 -"~~~~~ fun nxt_specif, args:"; val (Add_Given ct, ptp) = (tac, ptp);
11.8 +"~~~~~ fun Step_Specify.by_tactic, args:"; val (Add_Given ct, ptp) = (tac, ptp);
11.9 "~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp);
11.10 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
11.11 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
11.12 @@ -88,7 +88,7 @@
11.13 Err "[error] appl_add: is_known: identifiers [equality] not in example"*)
11.14 nxt_specif_additem "#Given" ct ptp;(*WAS
11.15 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
11.16 -nxt_specif tac ptp;(*WAS
11.17 +Step_Specify.by_tactic tac ptp;(*WAS
11.18 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
11.19 nxt_specify_ (pt,ip); (*WAS
11.20 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
12.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Mon Dec 23 15:41:36 2019 +0100
12.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Mon Dec 23 16:38:09 2019 +0100
12.3 @@ -365,7 +365,7 @@
12.4 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
12.5 val thy' = get_obj g_domID pt (par_pblobj pt p);
12.6 val (srls, (ist, ctxt), sc) = from_pblobj_or_detail' thy' (p,p_) pt;
12.7 -val Next_Step (istate, ctxt, tac) = find_next_tactic sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*)
12.8 +val Next_Step (istate, ctxt, tac) = LucinNEW.find_next_tactic sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*)
12.9 case tac of Or_to_List' _ => ()
12.10 | _ => error "Or_to_List broken ?"
12.11
12.12 @@ -404,7 +404,7 @@
12.13 (pors, (dI, pI, mI), hdl)
12.14 val pt = update_ctxt pt [] pctxt;
12.15
12.16 -"~~~~~ fun nxt_specif, args:"; val ((tac as Model_Problem), (pt, pos as (p,p_))) = (Model_Problem, (pt, ([], Pbl)));
12.17 +"~~~~~ fun Step_Specify.by_tactic, args:"; val ((tac as Model_Problem), (pt, pos as (p,p_))) = (Model_Problem, (pt, ([], Pbl)));
12.18 val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p;
12.19 "tracing bottom up"; #1(ospec) = "Build_Inverse_Z_Transform"; (*WAS true*)
12.20
12.21 @@ -469,7 +469,7 @@
12.22 e_metID = get_obj g_metID pt (par_pblobj pt p) = false;
12.23 val thy' = get_obj g_domID pt (par_pblobj pt p);
12.24 val (srls, (ist, ctxt), sc) = from_pblobj_or_detail' thy' (p,p_) pt;
12.25 - val Next_Step (is, ctxt, tac_) = find_next_tactic sc (pt,pos) ist ctxt;
12.26 + val Next_Step (is, ctxt, tac_) = LucinNEW.find_next_tactic sc (pt,pos) ist ctxt;
12.27 (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)
12.28
12.29 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
13.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Mon Dec 23 15:41:36 2019 +0100
13.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Mon Dec 23 16:38:09 2019 +0100
13.3 @@ -23,13 +23,13 @@
13.4 val (pt, _) = cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
13.5 (pors, (dI, pI, mI), hdl)
13.6 val pt = update_ctxt pt [] pctxt
13.7 -;((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate;
13.8 +;((pt, ([], Pbl)), fst3 (Step_Specify.by_tactic Model_Problem (pt, ([], Pbl)))) : calcstate;
13.9
13.10 (* INVESTIGATE val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];*)
13.11 (*///----------------------------------------- save for final check ------------------------\\\*)
13.12 val [(fmz''''', spec''''')] = [(fmz, (dI',pI',mI'))];
13.13 "~~~~~ fun CalcTreeTEST, args:"; val ([(fmz, sp)]) = ([(fmz, (dI',pI',mI'))]);
13.14 - val ((pt, p), tacis) = Chead.nxt_specify_init_calc (fmz, sp)
13.15 + val ((pt, p), tacis) = SpecifyNEW.nxt_specify_init_calc (fmz, sp)
13.16 (*ADD check*)
13.17 val PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, _), ctxt, ...} = get_obj I pt (fst p);
13.18 (* ERROR nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt
14.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Mon Dec 23 15:41:36 2019 +0100
14.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Mon Dec 23 16:38:09 2019 +0100
14.3 @@ -104,7 +104,7 @@
14.4 val (_, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
14.5
14.6 val Next_Step (_, _, _) =
14.7 - (*case*) find_next_tactic sc (pt, pos) ist ctxt (*of*);
14.8 + (*case*) LucinNEW.find_next_tactic sc (pt, pos) ist ctxt (*of*);
14.9 "~~~~~ fun find_next_tactic , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
14.10 = (sc, (pt, pos), ist, ctxt);
14.11
14.12 @@ -158,7 +158,7 @@
14.13 val (srls, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
14.14
14.15 val Next_Step (_, _, _) =
14.16 - (*case*) find_next_tactic sc (pt, pos) ist ctxt (*of*);
14.17 + (*case*) LucinNEW.find_next_tactic sc (pt, pos) ist ctxt (*of*);
14.18 "~~~~~ fun find_next_tactic , args:"; val (Rule.Prog prog, (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
14.19 = (sc, (pt, pos), ist, ctxt);
14.20
15.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Mon Dec 23 15:41:36 2019 +0100
15.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Mon Dec 23 16:38:09 2019 +0100
15.3 @@ -27,7 +27,7 @@
15.4 andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) (*then*);
15.5
15.6 (*+*)val (_, ([_], _, (pt''''', p'''''))) =
15.7 - nxt_specify_ (pt, ip);
15.8 + Step.specify_do_next (pt, ip);
15.9 "~~~~~ fun nxt_specify_ , args:"; val ((ptp as (pt, (p, p_)))) = (pt, ip);
15.10 val (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) =
15.11 case Ctree.get_obj I pt p of
16.1 --- a/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Mon Dec 23 15:41:36 2019 +0100
16.2 +++ b/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Mon Dec 23 16:38:09 2019 +0100
16.3 @@ -56,7 +56,7 @@
16.4 val thy' = get_obj g_domID pt (par_pblobj pt p);
16.5 val (srls, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
16.6
16.7 - find_next_tactic sc (pt, pos) ist ctxt;
16.8 + LucinNEW.find_next_tactic sc (pt, pos) ist ctxt;
16.9 "~~~~~ fun find_next_tactic , args:"; val (Rule.Prog prog, (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
16.10 = (sc, (pt, pos), ist, ctxt);
16.11
17.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Mon Dec 23 15:41:36 2019 +0100
17.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Mon Dec 23 16:38:09 2019 +0100
17.3 @@ -47,7 +47,7 @@
17.4 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
17.5 val thy' = get_obj g_domID pt (par_pblobj pt p);
17.6 val (srls, (ist, ctxt), sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
17.7 -val End_Program (ist, tac) = find_next_tactic sc (pt,pos) ist ctxt;
17.8 +val End_Program (ist, tac) = LucinNEW.find_next_tactic sc (pt,pos) ist ctxt;
17.9
17.10 (*+*);tac; (* = Check_Postcond' *)
17.11
18.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Mon Dec 23 15:41:36 2019 +0100
18.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Mon Dec 23 16:38:09 2019 +0100
18.3 @@ -58,7 +58,7 @@
18.4 val (srls, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
18.5
18.6 val Next_Step (_, _, Check_elementwise' _) =
18.7 - (*case*) find_next_tactic sc (pt, pos) ist ctxt (*of*);
18.8 + (*case*) LucinNEW.find_next_tactic sc (pt, pos) ist ctxt (*of*);
18.9 "~~~~~ fun find_next_tactic , args:"; val ((Rule.Prog prog), (ptp as (pt, (p, _))), Istate.Pstate ist, ctxt)
18.10 = (sc, (pt, pos), ist, ctxt);
18.11
19.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Mon Dec 23 15:41:36 2019 +0100
19.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Mon Dec 23 16:38:09 2019 +0100
19.3 @@ -565,7 +565,7 @@
19.4 val Steps [(m',f',pt',p',c',s')] =
19.5 locate_input_tactic thy' m (pt,(p,p_)) (sc,d) is;
19.6 val is' = get_istate pt' p';
19.7 - find_next_tactic thy' sc (pt'(*'*),p') is' (*as (ist, ctxt) ---> ist ctxt*);
19.8 + LucinNEW.find_next_tactic thy' sc (pt'(*'*),p') is' (*as (ist, ctxt) ---> ist ctxt*);
19.9
19.10
19.11
20.1 --- a/test/Tools/isac/Specify/appl.sml Mon Dec 23 15:41:36 2019 +0100
20.2 +++ b/test/Tools/isac/Specify/appl.sml Mon Dec 23 16:38:09 2019 +0100
20.3 @@ -69,7 +69,7 @@
20.4
20.5 (*============ inhibit exn AK110726 ==============================================
20.6 (* ERROR: Exception Bind raised and subsequent errors (not declared...)*)
20.7 -"~~~~~ fun nxt_specif, args:"; val (Add_Given ct, ptp) = (tac, ptp);
20.8 +"~~~~~ fun Step_Specify.by_tactic, args:"; val (Add_Given ct, ptp) = (tac, ptp);
20.9 "~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp);
20.10 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
20.11 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
21.1 --- a/test/Tools/isac/Specify/calchead.sml Mon Dec 23 15:41:36 2019 +0100
21.2 +++ b/test/Tools/isac/Specify/calchead.sml Mon Dec 23 16:38:09 2019 +0100
21.3 @@ -195,7 +195,7 @@
21.4 (*Add_Relation "relations\n [((a::real) // (#2::real)) ..."*)
21.5
21.6 (*---------------------------- FIXXXXME.meNEW !!! partial Add-Relation !!!
21.7 - nxt_specif <> specify ?!
21.8 + Step_Specify.by_tactic <> specify ?!
21.9
21.10 if nxt<>(Add_Relation
21.11 "relations [(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]")
22.1 --- a/test/Tools/isac/Specify/step-specify.sml Mon Dec 23 15:41:36 2019 +0100
22.2 +++ b/test/Tools/isac/Specify/step-specify.sml Mon Dec 23 16:38:09 2019 +0100
22.3 @@ -49,7 +49,7 @@
22.4 andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) (*then*);
22.5
22.6 val ("dummy", ([(Specify_Theory "Integrate", _, _)], _, _)) =
22.7 - nxt_specify_ (pt, ip);
22.8 + Step.specify_do_next (pt, ip);
22.9 "~~~~~ fun nxt_specify_ , args:"; val ((ptp as (pt, (p, p_)))) = (pt, ip);
22.10 val (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) =
22.11 (*isa<>REP ^^*)
22.12 @@ -81,9 +81,9 @@
22.13 = (Pbl, Tactic.Specify_Theory dI');
22.14 val _ = (*case*) tac (*of*);
22.15
22.16 - ("dummy", Chead.nxt_specif tac ptp) (*return from nxt_specify_*);
22.17 + ("dummy", Step_Specify.by_tactic tac ptp) (*return from nxt_specify_*);
22.18 "~~~~~ from fun nxt_specify_\<longrightarrow>fun Math_Engine.do_next\<longrightarrow>fun autocalc, return:"; val (str, (_, c', ptp))
22.19 - = ("dummy", Chead.nxt_specif tac ptp);
22.20 + = ("dummy", Step_Specify.by_tactic tac ptp);
22.21
22.22 (str, c''''' @ c', ptp) (*return from autocalc*);
22.23