1.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Thu May 07 11:42:19 2020 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Thu May 07 12:15:37 2020 +0200
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 = SpecifyNEW.nxt_specify_init_calc (encode_fmz (fmz, sp))
1.8 + val cs = Step_Specify.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")
2.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Thu May 07 11:42:19 2020 +0200
2.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Thu May 07 12:15:37 2020 +0200
2.3 @@ -35,7 +35,7 @@
2.4
2.5 datatype nxt_ =
2.6 HElpless (**)
2.7 -| Nexts of Chead.calcstate (**)
2.8 +| Nexts of Calc.T * State_Steps.T (**)
2.9
2.10 (* specify a new method; WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' *)
2.11 fun set_method mI ptp =
3.1 --- a/src/Tools/isac/Specify/calchead.sml Thu May 07 11:42:19 2020 +0200
3.2 +++ b/src/Tools/isac/Specify/calchead.sml Thu May 07 12:15:37 2020 +0200
3.3 @@ -160,9 +160,9 @@
3.4 this state just by "fun generate "
3.5 *)
3.6 type calcstate =
3.7 - (ctree * pos') * (* the calc-state to which the tacis could be applied *)
3.8 - State_Steps.T (* ev. several (hidden) steps;
3.9 - in REVERSE order: first tac_ to apply is last_elem *)
3.10 + Calc.T * (* the calc-state to which the tacis could be applied *)
3.11 + State_Steps.T (* ev. several (hidden) steps;
3.12 + in REVERSE order: first tac_ to apply is last_elem *)
3.13 val e_calcstate = ((EmptyPtree, e_pos'), [State_Steps.single_empty]);
3.14
3.15 (*the state used during one calculation within the mathengine; it contains
3.16 @@ -176,9 +176,9 @@
3.17 this state just by "fun generate ".*)
3.18 type calcstate' =
3.19 State_Steps.T * (* cas. several (hidden) steps;
3.20 - in REVERSE order: first tac_ to apply is last_elem *)
3.21 - pos' list * (* a "continuous" sequence of pos', deleted by application of taci list *)
3.22 - (ctree * pos') (* the calc-state resulting from the application of tacis *)
3.23 + in REVERSE order: first tac_ to apply is last_elem *)
3.24 + pos' list * (* a "continuous" sequence of pos', deleted by application of taci list *)
3.25 + Calc.T (* the calc-state resulting from the application of tacis *)
3.26 val e_calcstate' = ([State_Steps.single_empty], [e_pos'], (EmptyPtree, e_pos')) : calcstate';
3.27
3.28 (* is the calchead complete ? *)
3.29 @@ -268,7 +268,7 @@
3.30 | d_in (I_Model.Inc ((d,_),_)) = [d]
3.31 | d_in (I_Model.Sup (d,_)) = [d]
3.32 | d_in (I_Model.Mis (d,_)) = [d]
3.33 - | d_in i = error ("all_dsc_in: uncovered case with " ^ I_Model.feedback_to_string' i)
3.34 + | d_in i = raise ERROR ("all_dsc_in: uncovered case with " ^ I_Model.feedback_to_string' i)
3.35 in (flat o (map d_in)) itm_s end;
3.36
3.37 fun is_error (I_Model.Cor _) = false
4.1 --- a/src/Tools/isac/Specify/specify.sml Thu May 07 11:42:19 2020 +0200
4.2 +++ b/src/Tools/isac/Specify/specify.sml Thu May 07 12:15:37 2020 +0200
4.3 @@ -1,7 +1,6 @@
4.4 signature SPECIFY_NEW =
4.5 sig
4.6 val find_next_step: Calc.T -> string * (Pos.pos_ * Tactic.input)
4.7 - val nxt_specify_init_calc : Formalise.T -> Chead.calcstate
4.8 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.9 (*NONE*)
4.10 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.11 @@ -79,60 +78,4 @@
4.12 end
4.13 end
4.14
4.15 -(* create a calc-tree with oris via an cas.refined pbl *)
4.16 -fun nxt_specify_init_calc ([], (dI, pI, mI)) =
4.17 - if pI <> []
4.18 - then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
4.19 - let
4.20 - val {cas, met, ppc, thy, ...} = Specify.get_pbt pI
4.21 - val dI = if dI = "" then Context.theory_name thy else dI
4.22 - val mI = if mI = [] then hd met else mI
4.23 - val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t
4.24 - val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))
4.25 - ([], (dI,pI,mI), hdl, ContextC.empty)
4.26 - val pt = update_spec pt [] (dI, pI, mI)
4.27 - val pits = Generate.init_pbl' ppc
4.28 - val pt = update_pbl pt [] pits
4.29 - in ((pt, ([] , Pbl)), []) end
4.30 - else
4.31 - if mI <> []
4.32 - then (* from met-browser *)
4.33 - let
4.34 - val {ppc, ...} = Specify.get_met mI
4.35 - val dI = if dI = "" then "Isac_Knowledge" else dI
4.36 - val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty) ([], (dI, pI, mI))
4.37 - ([], (dI, pI, mI), TermC.empty, ContextC.empty)
4.38 - val pt = update_spec pt [] (dI, pI, mI)
4.39 - val mits = Generate.init_pbl' ppc
4.40 - val pt = update_met pt [] mits
4.41 - in ((pt, ([], Met)), []) end
4.42 - else (* new example, pepare for interactive modeling *)
4.43 - let
4.44 - val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
4.45 - ([], Spec.empty) ([], Spec.empty, TermC.empty, ContextC.empty)
4.46 - in ((pt, ([], Pbl)), []) end
4.47 - | nxt_specify_init_calc (fmz, (dI, pI, mI)) =
4.48 - let (* both """"""""""""""""""""""""" either empty or complete *)
4.49 - val thy = ThyC.get_theory dI
4.50 - val (pI, (pors, pctxt), mI) =
4.51 - if mI = ["no_met"]
4.52 - then
4.53 - let
4.54 - val (pors, pctxt) = Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy;
4.55 - val pI' = Specify.refine_ori' pors pI;
4.56 - in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
4.57 - (hd o #met o Specify.get_pbt) pI')
4.58 - end
4.59 - else (pI, Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy, mI)
4.60 - val {cas, ppc, thy = thy', ...} = Specify.get_pbt pI (*take dI from _refined_ pbl*)
4.61 - val dI = Context.theory_name (Stool.common_subthy (thy, thy'))
4.62 - val hdl = case cas of
4.63 - NONE => Auto_Prog.pblterm dI pI
4.64 - | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
4.65 - val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt) (fmz, (dI, pI, mI))
4.66 - (pors, (dI, pI, mI), hdl, pctxt)
4.67 - in
4.68 - ((pt, ([], Pbl)), fst3 (Step_Specify.by_tactic_input Tactic.Model_Problem (pt, ([], Pbl))))
4.69 - end
4.70 -
4.71 -end
4.72 +(**)end(**)
5.1 --- a/src/Tools/isac/Specify/step-specify.sml Thu May 07 11:42:19 2020 +0200
5.2 +++ b/src/Tools/isac/Specify/step-specify.sml Thu May 07 12:15:37 2020 +0200
5.3 @@ -9,8 +9,7 @@
5.4 val by_tactic_input: Tactic.input -> Calc.T -> Chead.calcstate'
5.5 val by_tactic: Tactic.T -> Calc.T -> string * Chead.calcstate'
5.6 (* ---- keep, probably required later in devel. ----------------------------------------------- *)
5.7 - val nxt_specify_init_calc: Formalise.T
5.8 - -> Calc.T * State_Steps.T
5.9 + val nxt_specify_init_calc: Formalise.T -> Calc.T * State_Steps.T
5.10 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.11 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.12
6.1 --- a/src/Tools/isac/TODO.thy Thu May 07 11:42:19 2020 +0200
6.2 +++ b/src/Tools/isac/TODO.thy Thu May 07 12:15:37 2020 +0200
6.3 @@ -27,13 +27,8 @@
6.4 (*\------- to from -------/*)
6.5 \begin{itemize}
6.6 \item xxx
6.7 - \item fun specify_init_calc defined twice
6.8 - \item xxx
6.9 - \item push nes identifiers back from O/I_Model to Model_Def
6.10 - \item xxx
6.11 \item rename Tactic.Calculate -> Tactic.Evaluate
6.12 \item xxx
6.13 - \item xxx
6.14 \item replace src/ Erls by Rule_Set.Empty
6.15 \item xxx
6.16 \item rename ptyps.sml -> specify-etc.sml
7.1 --- a/src/Tools/isac/Test_Code/test-code.sml Thu May 07 11:42:19 2020 +0200
7.2 +++ b/src/Tools/isac/Test_Code/test-code.sml Thu May 07 12:15:37 2020 +0200
7.3 @@ -55,7 +55,7 @@
7.4 compare "fun CalcTree" which DOES decode *)
7.5 fun CalcTreeTEST [(fmz, sp)] =
7.6 let
7.7 - val ((pt, p), tacis) = SpecifyNEW.nxt_specify_init_calc (fmz, sp)
7.8 + val ((pt, p), tacis) = Step_Specify.nxt_specify_init_calc (fmz, sp)
7.9 val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
7.10 val f = TESTg_form (pt,p)
7.11 in (p, []:NEW, f, tac, Celem.Sundef, pt) end
8.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Thu May 07 11:42:19 2020 +0200
8.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Thu May 07 12:15:37 2020 +0200
8.3 @@ -28,7 +28,7 @@
8.4 (*///----------------------------------------- save for final check ------------------------\\\*)
8.5 val [(fmz''''', spec''''')] = [(fmz, (dI',pI',mI'))];
8.6 "~~~~~ fun CalcTreeTEST, args:"; val ([(fmz, sp)]) = ([(fmz, (dI',pI',mI'))]);
8.7 - val ((pt, p), tacis) = SpecifyNEW.nxt_specify_init_calc (fmz, sp)
8.8 + val ((pt, p), tacis) = Step_Specify.nxt_specify_init_calc (fmz, sp)
8.9 (*ADD check*)
8.10 val PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, _), ctxt, ...} = get_obj I pt (fst p);
8.11 (* ERROR nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt