1.1 --- a/src/Tools/isac/BaseDefinitions/theoryC.sml Mon Jun 01 16:11:05 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/theoryC.sml Wed Jun 03 09:56:24 2020 +0200
1.3 @@ -11,7 +11,7 @@
1.4
1.5 val get_theory: id -> theory
1.6 val id_to_ctxt: id -> Proof.context
1.7 - val to_ctxt: theory -> Proof.context
1.8 + val to_ctxt: theory -> Proof.context (* inverse of Proof_Context.theory_of *)
1.9
1.10 val id_empty: id
1.11 val Isac: 'a -> theory
2.1 --- a/src/Tools/isac/Specify/specify.sml Mon Jun 01 16:11:05 2020 +0200
2.2 +++ b/src/Tools/isac/Specify/specify.sml Wed Jun 03 09:56:24 2020 +0200
2.3 @@ -8,7 +8,7 @@
2.4 (Model_Def.m_field * TermC.as_string) option
2.5 (*TODO: vvvvvvvvvvvvvv unify code*)
2.6 val by_tactic_input': string -> TermC.as_string -> Calc.T -> Calc.state_post
2.7 - val by_tactic': string -> TermC.as_string -> Calc.T -> string * Calc.state_post
2.8 + val by_Add_: string -> TermC.as_string -> Calc.T -> string * Calc.state_post
2.9 (*TODO: ^^^^^^^^^^^^^^ unify code*)
2.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.11 (*NONE*)
2.12 @@ -132,48 +132,28 @@
2.13 end
2.14 end
2.15
2.16 -fun by_tactic' sel ct (pt, pos as (p, Pos.Met)) =
2.17 - let
2.18 - val (met, oris, (dI', _, mI'), _, (dI, _, mI), ctxt) = Specification.get_data (pt, pos)
2.19 - val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
2.20 - val cmI = if mI = Method.id_empty then mI' else mI
2.21 - val {ppc, ...} = Method.from_store cmI
2.22 - in
2.23 - case I_Model.check_single ctxt sel oris met ppc ct of
2.24 - I_Model.Add itm => (*..union old input *)
2.25 - let
2.26 - val met' = I_Model.add_single thy itm met
2.27 - val tac' = I_Model.get_tac sel (ct, met')
2.28 - val (p, pt') =
2.29 - case Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of
2.30 - ((p, Pos.Met), _, _, pt') => (p, pt')
2.31 - | _ => raise ERROR "by_tactic': uncovered case of generate1"
2.32 - in
2.33 - ("ok", ([], [], (pt', (p, Pos.Met))))
2.34 - end
2.35 - | I_Model.Err msg => (msg, ([], [], (pt, (p, Pos.Met))))
2.36 - end
2.37 - | by_tactic' sel ct (pt, pos as (p, p_(*Frm, Pbl*))) =
2.38 - let
2.39 - val (_, oris, (dI', pI', _), pbl, (dI, pI, _), ctxt) = Specification.get_data (pt, pos)
2.40 - val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
2.41 - val cpI = if pI = Problem.id_empty then pI' else pI
2.42 - val {ppc, ...} = Problem.from_store cpI
2.43 - in
2.44 - case I_Model.check_single ctxt sel oris pbl ppc ct of
2.45 - I_Model.Add itm => (*..union old input *)
2.46 - let
2.47 - val pbl' = I_Model.add_single thy itm pbl
2.48 - val tac' = I_Model.get_tac sel (ct, pbl')
2.49 - val (p, pt') =
2.50 - case Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of
2.51 - ((p, Pos.Pbl), _, _, pt') => (p, pt')
2.52 - | _ => raise ERROR "by_tactic': uncovered case of Specify_Step.add"
2.53 - in
2.54 - ("ok", ([], [], (pt', (p, p_))))
2.55 - end
2.56 - | I_Model.Err msg => (msg, ([], [], (pt, (p, p_))))
2.57 - end
2.58 +fun by_Add_ m_field ct (pt, pos as (_, p_)) =
2.59 + let
2.60 + val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = Specification.get_data (pt, pos)
2.61 + val (i_model, m_patt) =
2.62 + if p_ = Pos.Met then
2.63 + (met,
2.64 + (if mI = Method.id_empty then mI' else mI) |> Method.from_store |> #ppc)
2.65 + else
2.66 + (pbl,
2.67 + (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store |> #ppc)
2.68 + in
2.69 + case I_Model.check_single ctxt m_field oris i_model m_patt ct of
2.70 + I_Model.Add i_single => (*..union old input *)
2.71 + let
2.72 + val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model
2.73 + val tac' = I_Model.get_tac m_field (ct, i_model')
2.74 + val (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)
2.75 + in
2.76 + ("ok", ([], [], (pt', pos)))
2.77 + end
2.78 + | I_Model.Err msg => (msg, ([], [], (pt, pos)))
2.79 + end
2.80
2.81 (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
2.82 -- for input from scratch*)
3.1 --- a/src/Tools/isac/Specify/step-specify.sml Mon Jun 01 16:11:05 2020 +0200
3.2 +++ b/src/Tools/isac/Specify/step-specify.sml Wed Jun 03 09:56:24 2020 +0200
3.3 @@ -182,9 +182,9 @@
3.4 in
3.5 ("ok", ([], [], (pt, pos)))
3.6 end
3.7 - | by_tactic (Tactic.Add_Given' (ct, _)) (pt, p) = Specify.by_tactic' "#Given" ct (pt, p)
3.8 - | by_tactic (Tactic.Add_Find' (ct, _)) (pt, p) = Specify.by_tactic' "#Find" ct (pt, p)
3.9 - | by_tactic (Tactic.Add_Relation' (ct, _)) (pt, p) = Specify.by_tactic'"#Relate" ct (pt, p)
3.10 + | by_tactic (Tactic.Add_Given' (ct, _)) (pt, p) = Specify.by_Add_ "#Given" ct (pt, p)
3.11 + | by_tactic (Tactic.Add_Find' (ct, _)) (pt, p) = Specify.by_Add_ "#Find" ct (pt, p)
3.12 + | by_tactic (Tactic.Add_Relation' (ct, _)) (pt, p) = Specify.by_Add_"#Relate" ct (pt, p)
3.13 (*strange old code, redes*)
3.14 | by_tactic (Tactic.Specify_Theory' domID) (pt, (p, p_)) =
3.15 let
4.1 --- a/src/Tools/isac/TODO.thy Mon Jun 01 16:11:05 2020 +0200
4.2 +++ b/src/Tools/isac/TODO.thy Wed Jun 03 09:56:24 2020 +0200
4.3 @@ -67,6 +67,8 @@
4.4 text \<open>
4.5 \begin{itemize}
4.6 \item xxx
4.7 + \item Specify_Step.add has dummy argument Istate_Def.Uistate -- remove down to Ctree
4.8 + \item xxx
4.9 \item Step_Specify.by_tactic (Tactic.Model_Problem' (id, _, met))
4.10 by_tactic (Tactic.Specify_Theory' domID)
4.11 had very old, strange code at 11b5b8b81876
5.1 --- a/test/Tools/isac/Specify/i-model.sml Mon Jun 01 16:11:05 2020 +0200
5.2 +++ b/test/Tools/isac/Specify/i-model.sml Wed Jun 03 09:56:24 2020 +0200
5.3 @@ -42,8 +42,8 @@
5.4 "~~~~~ fun by_tactic , args:"; val ((Tactic.Add_Given' (ct, _)), (pt, p)) = (tac', ptp);
5.5
5.6 val ("ok", ([], [], _)) =
5.7 - Specify.by_tactic' "#Given" ct (pt, p);
5.8 -"~~~~~ fun by_tactic' , args:"; val (sel, ct, (pt, pos as (p,_(*Frm, Pbl*)))) =
5.9 + Specify.by_Add_ "#Given" ct (pt, p);
5.10 +"~~~~~ fun by_Add_ , args:"; val (sel, ct, (pt, pos as (p,_(*Frm, Pbl*)))) =
5.11 ("#Given", ct, (pt, p));
5.12 val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = Specification.get_data (pt, pos)
5.13 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
5.14 @@ -90,7 +90,7 @@
5.15 (*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*);
5.16
5.17 Add itm (*return from add_single*);
5.18 -"~~~~~ from fun check_single \<longrightarrow>fun by_tactic' , return:"; val (I_Model.Add itm) = (Add itm);
5.19 +"~~~~~ from fun check_single \<longrightarrow>fun by_Add_ , return:"; val (I_Model.Add itm) = (Add itm);
5.20 val pbl' = I_Model.add_single thy itm pbl;
5.21
5.22 (*+*)if I_Model.to_string ctxt pbl' = "[\n" ^
5.23 @@ -105,7 +105,7 @@
5.24 val (p, pt') =
5.25 case Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of
5.26 ((p, Pos.Pbl), _, _, pt') => (p, pt')
5.27 - | _ => raise ERROR "by_tactic': uncovered case of Specify_Step.add"
5.28 + | _ => raise ERROR "by_Add_: uncovered case of Specify_Step.add"
5.29 (* only for getting final p_ ..*)
5.30 val pre = Pre_Conds.check' thy prls where_ pbl';
5.31 val pb = foldl and_ (true, map fst pre);