1.1 --- a/src/Tools/isac/Specify/specify.sml Fri Jun 12 11:41:57 2020 +0200
1.2 +++ b/src/Tools/isac/Specify/specify.sml Sun Jun 14 15:39:55 2020 +0200
1.3 @@ -6,10 +6,7 @@
1.4
1.5 val item_to_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T ->
1.6 (Model_Def.m_field * TermC.as_string) option
1.7 -(*TODO: vvvvvvvvvvvvvv unify code*)
1.8 - val by_tactic_input': string -> TermC.as_string -> Calc.T -> Calc.state_post
1.9 val by_Add_: string -> TermC.as_string -> Calc.T -> string * Calc.state_post
1.10 -(*TODO: ^^^^^^^^^^^^^^ unify code*)
1.11 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.12 (*NONE*)
1.13 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.14 @@ -76,7 +73,9 @@
1.15
1.16
1.17 (** find a next step in the specify-phase **)
1.18 -
1.19 +(*
1.20 + there should be mutual recursion between for_problem and for_method
1.21 +*)
1.22 fun for_problem oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) =
1.23 let
1.24 val cpI = if pI = Problem.id_empty then pI' else pI;
1.25 @@ -85,7 +84,7 @@
1.26 val {ppc = mpc, ...} = Method.from_store cmI
1.27 val (preok, _) = Pre_Conds.check prls where_ pbl 0;
1.28 in
1.29 - (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then
1.30 + if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then
1.31 ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))
1.32 else if pI' = Problem.id_empty andalso pI = Problem.id_empty then
1.33 ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))
1.34 @@ -110,7 +109,7 @@
1.35 (case item_to_add (ThyC.get_theory dI) oris mpc met of
1.36 SOME (fd, ct') =>
1.37 ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*30.8.01: pre?!?*)
1.38 - | NONE => ("dummy", (Pos.Met, Tactic.Apply_Method mI)))))
1.39 + | NONE => ("dummy", (Pos.Met, Tactic.Apply_Method mI))))
1.40 end
1.41
1.42 fun for_method oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) =
1.43 @@ -156,7 +155,7 @@
1.44 end
1.45
1.46
1.47 -(** tools for ... **)
1.48 +(** tools **)
1.49
1.50 fun by_Add_ m_field ct (pt, pos as (_, p_)) =
1.51 let
1.52 @@ -176,74 +175,12 @@
1.53 val tac' = I_Model.get_tac m_field (ct, i_model')
1.54 val (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)
1.55 in
1.56 - ("ok", ([], [], (pt', pos)))
1.57 + ("ok", ([(Tactic.input_from_T tac', tac', (pos, (Istate_Def.Uistate, ctxt)))],
1.58 + [], (pt', pos)))
1.59 end
1.60 | I_Model.Err msg => (msg, ([], [], (pt, pos)))
1.61 end
1.62
1.63 -(*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
1.64 - -- for input from scratch*)
1.65 -fun by_tactic_input' sel ct (ptp as (pt, (p, Pos.Pbl))) =
1.66 - let
1.67 - val (oris, dI', pI', dI, pI, pbl, ctxt) = case Ctree.get_obj I pt p of
1.68 - Ctree.PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>
1.69 - (oris, dI', pI', dI, pI, pbl, ctxt)
1.70 - | _ => raise ERROR "specify (Specify_Theory': uncovered case get_obj"
1.71 - val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
1.72 - val cpI = if pI = Problem.id_empty then pI' else pI;
1.73 - in
1.74 - case I_Model.check_single ctxt sel oris pbl ((#ppc o Problem.from_store) cpI) ct of
1.75 - I_Model.Add itm (*..union old input *) =>
1.76 - let
1.77 - val pbl' = I_Model.add_single thy itm pbl
1.78 - val (tac, tac_) = case sel of
1.79 - "#Given" => (Tactic.Add_Given ct, Tactic.Add_Given' (ct, pbl'))
1.80 - | "#Find" => (Tactic.Add_Find ct, Tactic.Add_Find' (ct, pbl'))
1.81 - | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, pbl'))
1.82 - | sel => raise ERROR ("by_tactic_input': uncovered case of " ^ sel)
1.83 - val (p, c, pt') =
1.84 - case Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of
1.85 - ((p, Pos.Pbl), c, _, pt') => (p, c, pt')
1.86 - | _ => raise ERROR "by_tactic_input': uncovered case generate1"
1.87 - in
1.88 - ([(tac, tac_, ((p, Pos.Pbl), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Pos.Pbl)))
1.89 - end
1.90 - | I_Model.Err msg => (*TODO.WN03 pass error-msgs to the frontend..
1.91 - FIXME ..and dont abuse a tactic for that purpose*)
1.92 - ([(Tactic.Tac msg, Tactic.Tac_ (ThyC.get_theory "Isac_Knowledge", msg,msg,msg),
1.93 - (Pos.e_pos', (Istate_Def.empty, ContextC.empty)))], [], ptp)
1.94 - end
1.95 - | by_tactic_input' sel ct (ptp as (pt, (p, Pos.Met))) =
1.96 - let
1.97 -(*NEW* ) *.specify_data ( *NEW*)
1.98 - val (oris, dI', mI', dI, mI, met, ctxt) = case Ctree.get_obj I pt p of
1.99 - Ctree.PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>
1.100 - (oris, dI', mI', dI, mI, met, ctxt)
1.101 - | _ => raise ERROR "by_tactic_input' Met: uncovered case get_obj"
1.102 -(*NEW* ) References.select ( *NEW*)
1.103 - val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
1.104 - val cmI = if mI = Method.id_empty then mI' else mI;
1.105 - in
1.106 - case I_Model.check_single ctxt sel oris met ((#ppc o Method.from_store) cmI) ct of
1.107 - I_Model.Add itm (*..union old input *) =>
1.108 - let
1.109 - val met' = I_Model.add_single thy itm met;
1.110 - val (tac, tac_) = case sel of
1.111 - "#Given" => (Tactic.Add_Given ct, Tactic.Add_Given' (ct, met'))
1.112 - | "#Find" => (Tactic.Add_Find ct, Tactic.Add_Find' (ct, met'))
1.113 - | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, met'))
1.114 - | sel => raise ERROR ("by_tactic_input' Met: uncovered case of" ^ sel)
1.115 - val (p, c, pt') =
1.116 - case Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of
1.117 - ((p, Pos.Met), c, _, pt') => (p, c, pt')
1.118 - | _ => raise ERROR "by_tactic_input': uncovered case generate1 (WARNING WHY ?)"
1.119 - in
1.120 - ([(tac, tac_, ((p, Pos.Met), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Pos.Met)))
1.121 - end
1.122 - | I_Model.Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)
1.123 - end
1.124 - | by_tactic_input' _ _ (_, p) = raise ERROR ("by_tactic_input' not impl. for" ^ Pos.pos'2str p)
1.125 -
1.126 (* complete _NON_empty calc-head for autocalc (sub-)pbl from oris
1.127 + met from fmz; assumes pos on PblObj, meth = [] *)
1.128 fun finish_phase (pt, pos as (p, p_)) =