1.1 --- a/src/Tools/isac/Specify/specify.sml Sun Oct 29 07:14:14 2023 +0100
1.2 +++ b/src/Tools/isac/Specify/specify.sml Thu Nov 16 08:15:46 2023 +0100
1.3 @@ -7,14 +7,25 @@
1.4 val do_all: Calc.T -> Calc.T
1.5 val finish_phase: Calc.T -> Calc.T
1.6
1.7 +(*OLD* )
1.8 val item_to_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T ->
1.9 (Model_Def.m_field * TermC.as_string) option
1.10 +( *---*)
1.11 + val item_to_add: Proof.context -> O_Model.T -> I_Model.T_TEST ->
1.12 + (Model_Def.m_field * TermC.as_string) option
1.13 +(*NEW*)
1.14 val by_Add_: string -> TermC.as_string -> Calc.T -> string * Calc.state_post
1.15 (*from isac_test for Minisubpbl*)
1.16 +(*OLD* )
1.17 val for_problem: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T * I_Model.T ->
1.18 string * (Pos.pos_ * Tactic.input)
1.19 +( *---*)
1.20 + val for_problem: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T * I_Model.T_TEST ->
1.21 + string * (Pos.pos_ * Tactic.input)
1.22 +(*NEW*)
1.23 val for_method: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T * I_Model.T ->
1.24 string * (Pos.pos_ * Tactic.input)
1.25 + val select_inc_lists: I_Model.T_TEST -> I_Model.T_TEST
1.26
1.27 \<^isac_test>\<open>
1.28 (**)
1.29 @@ -26,6 +37,15 @@
1.30 struct
1.31 (**)
1.32
1.33 +fun select_inc_lists i_model =
1.34 + let
1.35 + (* filter problem with Const ("Input_Descript.solutions", _) *)
1.36 + val filt = (fn (_, _, _, _, (I_Model.Inc_TEST (descr, _::_) , _)) => Pre_Conds.is_list_descr descr
1.37 + | _ => false)
1.38 + in
1.39 + (filter filt i_model) @ (filter_out filt i_model)
1.40 + end
1.41 +(*OLD* )
1.42 (*
1.43 select an item in oris, notyet input in itms
1.44 (precondition: in itms are only I_Model.Cor, I_Model.Sup, I_Model.Inc)
1.45 @@ -73,6 +93,35 @@
1.46 NONE => raise ERROR "item_to_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
1.47 | SOME ori => SOME (I_Model.get_field_term thy ori (hd icl))
1.48 end
1.49 +( *---*)
1.50 +fun item_to_add ctxt o_model i_model =
1.51 + let
1.52 + val max_vnt = last_elem (*this decides, for which variant initially help is given*)
1.53 + (Model_Def.max_variants o_model i_model)
1.54 + val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model
1.55 + val i_to_select = i_model
1.56 + |> filter_out (fn (_, vnts, _, _, (I_Model.Cor_TEST _, _)) => member op= vnts max_vnt | _ => false)
1.57 + |> select_inc_lists
1.58 +(*OLD* )
1.59 + |> hd
1.60 + in
1.61 + case I_Model.fill_from_o o_vnts i_to_select of
1.62 + SOME (_, _, _, m_field, (feedb, _)) =>
1.63 + SOME (m_field, feedb |> I_Model.feedb_args_to_string ctxt)
1.64 + | NONE => raise ERROR "item_to_add: NONE not.impl."
1.65 + end
1.66 +( *---*)
1.67 +(** ) |> hd( **)
1.68 + in
1.69 + if i_to_select = [] then NONE
1.70 + else
1.71 + case I_Model.fill_from_o o_vnts (hd i_to_select) of
1.72 + SOME (_, _, _, m_field, (feedb, _)) =>
1.73 + SOME (m_field, feedb |> I_Model.feedb_args_to_string ctxt)
1.74 + | NONE => raise ERROR "item_to_add: NONE not.impl."
1.75 + end
1.76 +(*NEW*)
1.77 +(*NEW*)
1.78
1.79
1.80 (** find a next step in the specify-phase **)
1.81 @@ -92,13 +141,17 @@
1.82 else if pI' = Problem.id_empty andalso pI = Problem.id_empty then
1.83 ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))
1.84 else
1.85 - case find_first (I_Model.is_error o #5) pbl of
1.86 + case find_first (fn (_, _, _, _, feedb) => I_Model.is_error feedb) pbl of
1.87 SOME (_, _, _, fd, itm_) =>
1.88 ("dummy", (Pos.Pbl, P_Model.mk_delete (ThyC.get_theory ctxt
1.89 (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
1.90 | NONE =>
1.91 +(*OLD* )
1.92 (case item_to_add (ThyC.get_theory ctxt
1.93 (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
1.94 +( *---*)
1.95 + (case item_to_add ctxt oris (I_Model.OLD_to_TEST pbl) of
1.96 +(*NEW*)
1.97 SOME (fd, ct') => ("dummy", (Pos.Pbl, P_Model.mk_additem fd ct'))
1.98 | NONE => (*pbl-items complete*)
1.99 if not preok then ("dummy", (Pos.Pbl, Tactic.Refine_Problem pI'))
1.100 @@ -107,11 +160,15 @@
1.101 else if pI = Problem.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))
1.102 else if mI = MethodC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Method mI'))
1.103 else
1.104 - case find_first (I_Model.is_error o #5) met of
1.105 + case find_first (fn (_, _, _, _, feedb) => I_Model.is_error feedb) (I_Model.TEST_to_OLD met) of
1.106 SOME (_, _, _, fd, itm_) =>
1.107 ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory ctxt dI) fd itm_))
1.108 | NONE =>
1.109 +(*OLD* )
1.110 (case item_to_add (ThyC.get_theory ctxt dI) oris mpc met of
1.111 +( *---*)
1.112 + (case item_to_add ctxt oris met of
1.113 +(*NEW*)
1.114 SOME (fd, ct') =>
1.115 ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*30.8.01: where_?!?*)
1.116 | NONE => ("dummy", (Pos.Met, Tactic.Apply_Method mI))))
1.117 @@ -123,15 +180,19 @@
1.118 val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI;
1.119 val (preok, _) = Pre_Conds.check ctxt where_rls where_ (mpc, I_Model.OLD_to_TEST met);
1.120 in
1.121 - (case find_first (I_Model.is_error o #5) met of
1.122 + (case find_first (fn (_, _, _, _, feedb) => I_Model.is_error feedb) met of
1.123 SOME (_,_,_, fd, itm_) =>
1.124 ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory ctxt
1.125 (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
1.126 | NONE =>
1.127 +(*OLD* )
1.128 case item_to_add (ThyC.get_theory ctxt
1.129 - (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
1.130 + (if dI = ThyC.id_empty then dI' else dI)) oris mpc (met) of
1.131 +( *---*)
1.132 + case item_to_add ctxt oris (I_Model.OLD_to_TEST met) of
1.133 +(*NEW*)
1.134 SOME (fd, ct') =>
1.135 - ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*->->*)
1.136 + ("dummy", (Pos.Met, P_Model.mk_additem fd ct'))
1.137 | NONE =>
1.138 (if dI = ThyC.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Theory dI'))
1.139 else if pI = Problem.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Problem pI'))
1.140 @@ -156,7 +217,7 @@
1.141 ["no_met"] => ("ok", (Pos.Pbl, Tactic.Refine_Tacitly pI'))
1.142 | _ => ("ok", (Pos.Pbl, Tactic.Model_Problem))
1.143 else if p_ = Pos.Pbl then
1.144 - for_problem ctxt oris (o_refs, refs) (pbl, met)
1.145 + for_problem ctxt oris (o_refs, refs) (pbl, I_Model.OLD_to_TEST met)
1.146 else
1.147 for_method ctxt oris (o_refs, refs) (pbl, met)
1.148 end