prepare 10: check completeness of Specification regards variants and Position.T
1.1 --- a/README.md Wed Sep 27 12:17:44 2023 +0200
1.2 +++ b/README.md Mon Oct 02 12:02:59 2023 +0200
1.3 @@ -64,6 +64,7 @@
1.4
1.5 isabisac/bin/isabelle jedit -l Isac_Test_Base isa/test/Tools/isac/Test_Isac_Short.thy &
1.6 ====isabisac$ ./bin/isabelle jedit -l Isac_Test_Base ../isa/test/Tools/isac/Test_Isac_Short.thy &
1.7 +====isabisac$ ./bin/isabelle jedit -l Isac_Test_Base ../isa/test/Tools/isac/Test_Isac.thy &
1.8 ====isabisac$ ./bin/isabelle jedit -l Isac_Test_Base ../isa/test/Tools/isac/Test_Some.thy &
1.9
1.10 * Parallel Build
2.1 --- a/TODO.md Wed Sep 27 12:17:44 2023 +0200
2.2 +++ b/TODO.md Mon Oct 02 12:02:59 2023 +0200
2.3 @@ -52,6 +52,11 @@
2.4
2.5 ***** priority of WN items is top down, most urgent/simple on top
2.6
2.7 +* WN: make signature of I_Model.s_make_complete equal to I_Model.s_are_complete (pbl_id!)
2.8 +* WN: uncomment: I_Model.check_internal (*filter (fn (_, _, _, m_field ,_) ..*)
2.9 + after I_Model.s_make_complete does NOT create m_field #undef, "i_model_empty";
2.10 + see test/../i-model.sml --- setup test data for I_Model.s_make_complete ---
2.11 +* WN: replace of_max_variant by max_variants + make_environments
2.12 * WN: ---broken elementwise input to lists---
2.13 * WN: undetected ERROR in autoCalculate --- due to Post_Conds.check? (_OLD .. dispels ?)
2.14 * WN: "review (descriptor, ts)"; ts : term list, because this supports element-wise input of lists.
3.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Wed Sep 27 12:17:44 2023 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Mon Oct 02 12:02:59 2023 +0200
3.3 @@ -50,6 +50,10 @@
3.4 val setNextTactic : States.calcID -> Tactic.input -> XML.tree
3.5 val setProblem : States.calcID -> Problem.id -> XML.tree
3.6 val setTheory : States.calcID -> ThyC.id -> XML.tree
3.7 +
3.8 +(*from isac_test for Minisubpbl*)
3.9 + val appendFormula' : States.calcID -> TermC.as_string -> XML.tree (*unit future*)
3.10 +
3.11 end
3.12
3.13 (**)
3.14 @@ -167,8 +171,9 @@
3.15 fun autoCalculate cI auto = (*Future.fork
3.16 (fn () => (( *)let
3.17 val pold = States.get_pos cI 1
3.18 + val calc = States.get_calc cI
3.19 in
3.20 - case Math_Engine.autocalc [] pold (States.get_calc cI) auto of
3.21 + case Math_Engine.autocalc [] pold calc auto of
3.22 ("ok", c, ptp as (_,p)) =>
3.23 (States.upd_calc cI (ptp, []); States.upd_ipos cI 1 p;
3.24 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
4.1 --- a/src/Tools/isac/Build_Isac.thy Wed Sep 27 12:17:44 2023 +0200
4.2 +++ b/src/Tools/isac/Build_Isac.thy Mon Oct 02 12:02:59 2023 +0200
4.3 @@ -272,6 +272,7 @@
4.4
4.5 ML \<open>
4.6 \<close> ML \<open>
4.7 +
4.8 \<close> ML \<open>
4.9 \<close>
4.10 end
5.1 --- a/src/Tools/isac/Interpret/step-solve.sml Wed Sep 27 12:17:44 2023 +0200
5.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Mon Oct 02 12:02:59 2023 +0200
5.3 @@ -88,7 +88,7 @@
5.4 *)
5.5 (*fun by_term (next_cs as (_, _, (pt, pos as (p, _))): Calc.state_post) istr =*)
5.6 (*will come directly from PIDE--vvvvvvvvvvv*)
5.7 -fun by_term (pt, pos as (p, _)) (istr(*, pp*)) =
5.8 +fun by_term (pt, pos as (p, _)) istr =
5.9 let
5.10 val f_in = Syntax.read_term (Ctree.get_ctxt pt pos) istr
5.11 handle ERROR msg => error (msg (*^ Position.here pp*))
6.1 --- a/src/Tools/isac/MathEngine/MathEngine.thy Wed Sep 27 12:17:44 2023 +0200
6.2 +++ b/src/Tools/isac/MathEngine/MathEngine.thy Mon Oct 02 12:02:59 2023 +0200
6.3 @@ -17,6 +17,7 @@
6.4
6.5 ML \<open>
6.6 \<close> ML \<open>
6.7 +
6.8 \<close> ML \<open>
6.9 \<close>
6.10 end
7.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Wed Sep 27 12:17:44 2023 +0200
7.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Mon Oct 02 12:02:59 2023 +0200
7.3 @@ -115,7 +115,7 @@
7.4 else if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp
7.5 end
7.6 else
7.7 - if not (References.are_complete (pt,pos))
7.8 + if not (References.are_complete (pt, pos))
7.9 then
7.10 let val ptp = References.complete (pt, pos)
7.11 in
8.1 --- a/src/Tools/isac/MathEngine/me-misc.sml Wed Sep 27 12:17:44 2023 +0200
8.2 +++ b/src/Tools/isac/MathEngine/me-misc.sml Mon Oct 02 12:02:59 2023 +0200
8.3 @@ -21,33 +21,19 @@
8.4 struct
8.5 (**)
8.6
8.7 -fun pt_model (Ctree.PblObj {meth, spec, origin = (_, spec', hdl), ctxt, ...}) Pos.Met =
8.8 +fun pt_model (Ctree.PblObj {meth, spec, origin = (_, o_spec, hdl), ctxt, ...}) Pos.Met =
8.9 let
8.10 - val (_, _, metID) = Ctree.get_somespec' spec spec'
8.11 - val where_ = if metID = MethodC.id_empty then []
8.12 - else
8.13 - let
8.14 - val {where_rls, where_, model, ...} = MethodC.from_store ctxt metID
8.15 - val (_, where_) = Pre_Conds.check ctxt where_rls where_
8.16 - (model, I_Model.OLD_to_TEST meth)
8.17 - in where_ end
8.18 - val allcorrect = I_Model.is_complete meth andalso foldl and_ (true, (map #1 where_))
8.19 + val (_, _, met_id) = References.select_input o_spec spec
8.20 + val (allcorr, _) = Pre_Conds.check_internal ctxt (I_Model.OLD_to_TEST meth) (Pos.Met, met_id)
8.21 in
8.22 - Ctree.ModSpec (allcorrect, Pos.Met, hdl, meth, where_, spec)
8.23 + Ctree.ModSpec (allcorr, Pos.Met, hdl, meth, (*where_*)[(*MethodC.from_store in check*)], spec)
8.24 end
8.25 - | pt_model (Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}) _(*Frm,Pbl*) =
8.26 + | pt_model (Ctree.PblObj {probl, spec, origin = (_, o_spec, hdl), ctxt, ...}) _(*Frm,Pbl*) =
8.27 let
8.28 - val (_, pI, _) = Ctree.get_somespec' spec spec'
8.29 - val where_ = if pI = Problem.id_empty then []
8.30 - else
8.31 - let
8.32 - val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
8.33 - val (_, where_) = Pre_Conds.check ctxt where_rls where_
8.34 - (model, I_Model.OLD_to_TEST probl)
8.35 - in where_ end
8.36 - val allcorrect = I_Model.is_complete probl andalso foldl and_ (true, (map #1 where_))
8.37 + val (_, _, met_id) = References.select_input o_spec spec
8.38 + val (allcorr, _) = Pre_Conds.check_internal ctxt (I_Model.OLD_to_TEST probl) (Pos.Met, met_id)
8.39 in
8.40 - Ctree.ModSpec (allcorrect, Pos.Pbl, hdl, probl, where_, spec)
8.41 + Ctree.ModSpec (allcorr, Pos.Pbl, hdl, probl, (*where_*)[(*Problem.from_store in check*)], spec)
8.42 end
8.43 | pt_model _ _ = raise ERROR "pt_model: uncovered definition"
8.44
9.1 --- a/src/Tools/isac/MathEngine/step.sml Wed Sep 27 12:17:44 2023 +0200
9.2 +++ b/src/Tools/isac/MathEngine/step.sml Mon Oct 02 12:02:59 2023 +0200
9.3 @@ -71,7 +71,7 @@
9.4 fun switch_specify_solve state_pos (pt, input_pos) =
9.5 let
9.6 val result =
9.7 - if Pos.on_specification ([], state_pos)
9.8 + if Pos.on_specification ([(*or some other int list, relevant is ..*)], state_pos)
9.9 then specify_do_next (pt, input_pos)
9.10 else LI.do_next (pt, input_pos)
9.11 in
10.1 --- a/src/Tools/isac/Specify/i-model.sml Wed Sep 27 12:17:44 2023 +0200
10.2 +++ b/src/Tools/isac/Specify/i-model.sml Mon Oct 02 12:02:59 2023 +0200
10.3 @@ -64,19 +64,17 @@
10.4 val add: single -> T -> T
10.5 val s_make_complete: O_Model.T -> T_TEST * T_TEST -> Model_Pattern.T * Model_Pattern.T ->
10.6 T_TEST * T_TEST
10.7 + val s_are_complete: Proof.context -> O_Model.T -> T_TEST * T_TEST -> Problem.id * MethodC.id
10.8 + -> bool
10.9
10.10 val is_error: feedback -> bool
10.11 - val is_complete: T -> bool
10.12 - val is_complete_variant: Model_Def.variant -> T_TEST-> bool
10.13 val to_p_model: theory -> feedback -> string
10.14
10.15 -(*from isac_test for Minisubpbl*)
10.16 +(*/----- from isac_test for Minisubpbl*)
10.17 val msg: variants -> feedback_TEST -> string
10.18 val transfer_terms: O_Model.single -> single_TEST
10.19
10.20 val eq1: ''a -> 'b * (''a * 'c) -> bool
10.21 - val filter_outs: O_Model.T -> T -> O_Model.T
10.22 - val filter_outs_TEST: O_Model.T -> T_TEST -> O_Model.T
10.23 val feedback_to_string: Proof.context -> feedback -> string
10.24 val feedback_TEST_to_string: Proof.context -> feedback_TEST -> string
10.25
10.26 @@ -84,6 +82,7 @@
10.27 'a * 'b * bool * string * feedback
10.28 val seek_ppc: int -> T -> single option
10.29 val overwrite_ppc: theory -> single -> T -> T
10.30 +(*\----- from isac_test for Minisubpbl*)
10.31
10.32 \<^isac_test>\<open>
10.33 (**)
10.34 @@ -128,10 +127,10 @@
10.35 type env = Env.T
10.36
10.37
10.38 -fun feedback_OLD_to_TEST (Cor ((d, ts), penv)) = (Model_Def.Cor_TEST (d, ts))
10.39 +fun feedback_OLD_to_TEST (Cor ((d, ts), _)) = (Model_Def.Cor_TEST (d, ts))
10.40 | feedback_OLD_to_TEST (Syn c) = (Model_Def.Syn_TEST c)
10.41 | feedback_OLD_to_TEST (Typ c) = (Model_Def.Syn_TEST c)
10.42 - | feedback_OLD_to_TEST (Inc ((d, ts), penv)) = (Model_Def.Inc_TEST (d, ts))
10.43 + | feedback_OLD_to_TEST (Inc ((d, ts), _)) = (Model_Def.Inc_TEST (d, ts))
10.44 | feedback_OLD_to_TEST (Sup (d, ts)) = (Model_Def.Sup_TEST (d, ts))
10.45 | feedback_OLD_to_TEST (Mis (d, pid)) = Model_Def.Syn_TEST ((UnparseC.term (ContextC.for_ERROR ()) d) ^ " " ^
10.46 (UnparseC.term (ContextC.for_ERROR ()) pid))
10.47 @@ -222,7 +221,6 @@
10.48 O_Model.add_enumerate pre_items |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e))
10.49 end
10.50
10.51 -(*/---------------- old code -----------------------------------------------------------------\*)
10.52 fun o_model_values (Cor ((_, ts), _)) = ts
10.53 | o_model_values (Syn _) = []
10.54 | o_model_values (Typ _) = []
10.55 @@ -353,7 +351,6 @@
10.56 else Add (i', [], true, f, Cor ((d, ts), (id, [Input_Descript.join'''' (d, ts)])))
10.57 end)
10.58 end
10.59 - (*for MethodC: #undef completed vvvvv vvvvvv term_as_string*)
10.60 (*will come directly from PIDE ----------------------vvvvvvvvvvv*)
10.61 | check_single ctxt m_field o_model i_model m_patt (str(*, pos*)) =
10.62 let
10.63 @@ -409,63 +406,27 @@
10.64
10.65 (** complete I_Model.T **)
10.66
10.67 -(*
10.68 - Survey on completion of i-models.
10.69 - one most general version, I_Model.s_make_complete, shall replace all old versions
10.70 +(* assumes pbl_imod is complete_TEST, met_imod is complete_TEST*)
10.71 +fun s_are_complete _ _ ([], _) _ = false
10.72 + | s_are_complete _ _ (_, []) _ = false
10.73 + | s_are_complete ctxt o_model (pbl_imod, met_imod) (pbl_id, met_id) =
10.74 + let
10.75 + val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod
10.76 + val met_max_vnts = Model_Def.max_variants o_model met_imod
10.77 + val max_vnts = inter op= pbl_max_vnts met_max_vnts
10.78 + val max_vnt = if max_vnts = []
10.79 + then raise ERROR "I_Model.s_are_complete: request user to review met_imod"
10.80 + else hd max_vnts
10.81
10.82 - Divide functionality of I_Model.of_max_variant into parts in order for re-use in is_complete
10.83 - I_Model.max_variants
10.84 - return variant list, because Problem#model might be insufficient to determine
10.85 - variant of MethodC.#model (FunctionVariable a ! b)
10.86 - + (Model_Pattern.single * I_Model.single) list for make_environments
10.87 - ^^NO: need ONLY max_variants
10.88 - Pre_Conds.make_environments
10.89 - takes above list
10.90 + val (pbl_imod', met_imod') = (
10.91 + filter (fn (_, vnts, _, _, _) => member_swap op = max_vnt vnts) pbl_imod,
10.92 + filter (fn (_, vnts, _, _, _) => member_swap op = max_vnt vnts) met_imod)
10.93
10.94 - Coordination with I_Model.is_complete:
10.95 - uses I_Model.max_variants, Pre_Conds.make_environments for Pre_Conds.check
10.96 - determines by use of both models independently (?)
10.97 -*)
10.98 -
10.99 -fun complete' pbt (i, v, f, d, ts) =
10.100 - case \<^try>\<open> (i, v, true, f, Cor ((d, ts),
10.101 - ((find_first ((fn descriptor => (fn (_, (d, _)) => descriptor = d)) d)) pbt |> the |> snd |> snd, ts)
10.102 - ))\<close> of
10.103 - SOME x => x
10.104 - | NONE => (i, v, true, f, Cor ((d, ts), (d, ts)))
10.105 -
10.106 -(*filter out oris which have same description in itms*)
10.107 -(* ---------------------------------- type problems ---vv---------vv
10.108 -fun filter_outs oris [] = oris
10.109 - | filter_outs oris (i::itms) =
10.110 - let
10.111 - val ors = filter_out ((curry op = ((descriptor o #5) i)) o (#4)) oris
10.112 - in
10.113 - filter_outs ors itms
10.114 - end
10.115 -*)
10.116 -(*with types..*)
10.117 -(*T_TESTold*)
10.118 -fun filter_outs oris [] = oris
10.119 - | filter_outs oris (i::itms) =
10.120 - let
10.121 - val ors = filter_out ((curry op = ((descriptor o
10.122 - (#5: single -> feedback)) i)) o
10.123 - (#4: O_Model.single -> O_Model.descriptor)) oris
10.124 - in
10.125 - filter_outs ors itms
10.126 - end
10.127 -(*T_TEST*)
10.128 -fun filter_outs_TEST oris [] = oris
10.129 - | filter_outs_TEST oris (i::itms) =
10.130 - let
10.131 - val ors = filter_out ((curry op = ((descriptor_TEST o
10.132 - ((#1 o #5): single_TEST -> feedback_TEST) ) i) ) o
10.133 - (#4: O_Model.single -> O_Model.descriptor) ) oris
10.134 - in
10.135 - filter_outs_TEST ors itms
10.136 - end
10.137 -(*T_TESTnew*)
10.138 + val (pbl_check, _) = Pre_Conds.check_internal ctxt pbl_imod' (Pos.Pbl, pbl_id)
10.139 + val (met_check, _) = Pre_Conds.check_internal ctxt met_imod' (Pos.Met, met_id)
10.140 + in
10.141 + pbl_check andalso met_check
10.142 + end
10.143
10.144 fun is_error (Cor _) = false
10.145 | is_error (Sup _) = false
10.146 @@ -488,14 +449,6 @@
10.147 handles superfluous items carelessly *)
10.148 fun add itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
10.149
10.150 -(*TODO: also check if all elements are I_Model.Cor*)
10.151 -fun is_complete ([]: T) = false
10.152 - | is_complete itms = foldl and_ (true, (map #3 itms))
10.153 -
10.154 -(*for PIDE: are all feedback Cor ? MISSING: Pre_Conds.check *)
10.155 -fun is_complete_variant no_model_items i_model =
10.156 - no_model_items = length (filter (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false) i_model)
10.157 -
10.158 val of_max_variant = Pre_Conds.of_max_variant
10.159
10.160 fun msg vnts feedb = "get_descr_vnt' returns NONE: i.e. it does not find an item of o_model with\n" ^
11.1 --- a/src/Tools/isac/Specify/pre-conditions.sml Wed Sep 27 12:17:44 2023 +0200
11.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml Mon Oct 02 12:02:59 2023 +0200
11.3 @@ -21,8 +21,8 @@
11.4 val max_variant: Model_Def.i_model -> Model_Def.variant
11.5 val environment_TEST: Model_Pattern.T -> Model_Def.i_model_TEST -> Env.T
11.6
11.7 -(*TODO: replace in pre-conditions.m, see fun max_variants + make_envs_preconds,
11.8 - see i-model.sml (** complete I_Model.T **) *)
11.9 + val make_environments: Model_Pattern.T -> Model_Def.i_model_TEST -> Env.T * (env_subst * env_eval)
11.10 +(*TODO: replace vvv with ^^^*)
11.11 val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->
11.12 (bool * Model_Def.variant * Model_Def.i_model_TEST) * Env.T * (env_subst * env_eval)
11.13 val make_envs_preconds: (Model_Pattern.single * Model_Def.i_model_single_TEST) list ->
11.14 @@ -30,12 +30,14 @@
11.15
11.16 val check_pos: Proof.context -> Rule_Set.T -> unchecked_pos ->
11.17 Model_Pattern.T * Model_Def.i_model_TEST -> checked_pos
11.18 + val check_internal: Proof.context -> Model_Def.i_model_TEST -> (Pos.pos_ * References_Def.id)
11.19 + -> checked
11.20 val check_envs: Proof.context -> Rule_Set.T -> unchecked -> Env.T * (env_subst * env_eval)
11.21 -> checked
11.22 val check: Proof.context -> Rule_Set.T -> unchecked ->
11.23 Model_Pattern.T * Model_Def.i_model_TEST -> checked
11.24
11.25 -(*from isac_test for Minisubpbl*)
11.26 +(*/----- from isac_test for Minisubpbl*)
11.27 val get_equal_descr: Model_Def.i_model_TEST -> Model_Pattern.single ->
11.28 (Model_Pattern.single * Model_Def.i_model_single_TEST) list
11.29 val unchecked_OLD_to_TEST: term list -> (term * Position.T) list
11.30 @@ -58,6 +60,7 @@
11.31 Model_Def.i_model_single_TEST
11.32 val get_descr_vnt': Model_Def.i_model_feedback_TEST -> Model_Def.variants -> O_Model.T ->
11.33 O_Model.T
11.34 +(*\----- from isac_test for Minisubpbl*)
11.35
11.36 \<^isac_test>\<open>
11.37 (**)
11.38 @@ -103,6 +106,7 @@
11.39
11.40 type input = TermC.as_string list;
11.41
11.42 +
11.43 (** tools **)
11.44
11.45 fun to_str ctxt (b, t) = pair2str (bool2str b, UnparseC.term ctxt t);
11.46 @@ -141,7 +145,7 @@
11.47 (* new code with I_Model.T_TEST proper handling variants *)
11.48
11.49 (*get descriptor of those items which can contribute to Subst.T and Env.T*)
11.50 -(* get_dscr: feedback_TEST -> descriptor option*)
11.51 +(* get_dscr': feedback_TEST -> descriptor option*)
11.52 fun get_dscr' (Cor_TEST (descr, _)) = SOME descr
11.53 | get_dscr' (Inc_TEST (descr, _)) = SOME descr
11.54 | get_dscr' (Sup_TEST (descr, _)) = SOME descr
11.55 @@ -250,6 +254,38 @@
11.56 map (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb) equal_givens
11.57 |> flat
11.58
11.59 +fun make_environments model_patt i_model =
11.60 + let
11.61 + val equal_descr_pairs = map (get_equal_descr i_model) model_patt
11.62 + |> flat
11.63 + val env_model = make_env_model equal_descr_pairs
11.64 + val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
11.65 + val subst_eval_list = make_envs_preconds equal_givens
11.66 + val (env_subst, env_eval) = split_list subst_eval_list
11.67 + in
11.68 + (env_model, (env_subst, env_eval))
11.69 + end
11.70 +
11.71 +fun check_internal ctxt i_model (pbl_met, id) =
11.72 + let
11.73 + val (model, where_rls, where_) = case pbl_met of
11.74 + Pos.Pbl => let val {model, where_rls, where_, ...} = Problem.from_store ctxt id
11.75 + in (model, where_rls, where_) end
11.76 + | Pos.Met => let val {model, where_rls, where_, ...} = MethodC.from_store ctxt id
11.77 + in (model, where_rls, where_) end
11.78 + | _ => raise ERROR ("Pre_Conds.check_internal calles with " ^ Pos.pos_2str pbl_met)
11.79 + val (env_model, (env_subst, env_eval)) = (*Pre_Conds.*)make_environments model
11.80 + ((*filter (fn (_, _, _, m_field ,_) => m_field = "#Given")*) i_model)
11.81 +
11.82 + val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
11.83 + val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
11.84 + val full_subst = if env_eval = [] then pres_subst_other
11.85 + else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
11.86 + val evals = map (eval ctxt where_rls) full_subst
11.87 + in
11.88 + (foldl and_ (true, map fst evals), pres_subst_other)
11.89 + end;
11.90 +
11.91 (*T_TESTold*)
11.92 fun of_max_variant _ [] = ((false, 0, []), [], ([], []))
11.93 | of_max_variant model_patt i_model =
11.94 @@ -275,55 +311,6 @@
11.95 = length model_patt, max_variant, i_model_max),
11.96 env_model, (env_subst, env_eval))
11.97 end
11.98 -(*T_TEST* \<longrightarrow> Model_Def)
11.99 -fun max_variants model_patt i_model =
11.100 - let
11.101 - val all_variants =
11.102 - map (fn (_, variants, _, _, _) => variants) i_model
11.103 - |> flat
11.104 - |> distinct op =
11.105 - val variants_separated = map (filter_variants' i_model) all_variants
11.106 - val sums_corr = map (cnt_corrects) variants_separated
11.107 - val sum_variant_s = arrange_args sums_corr (1, all_variants)
11.108 -
11.109 - val max_first = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
11.110 - val maxes = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first
11.111 - |> map snd
11.112 - val option_sequence = map
11.113 - (fn (_, vnt) => if (member (op =) maxes vnt) then SOME vnt else NONE) sum_variant_s
11.114 -(*THAT IS NONSENSE, SEE Test_Theory (*+*)if (pbl_max_imos*)
11.115 - val max_i_models = map (fn (pos_in_sum_variant_s, i_model) =>
11.116 - if is_some pos_in_sum_variant_s then i_model else [])
11.117 - (option_sequence ~~ variants_separated)
11.118 - |> filter_out (fn place_holder => place_holder = []);
11.119 -(*/-- fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------\ * )
11.120 - PROBALBY FOR RE-USE:
11.121 - val option_sequence = map
11.122 - (fn (_, vnt) => if (member (op =) maxes vnt) then SOME vnt else NONE) sum_variant_s
11.123 - val max_i_models = map (fn (pos_in_sum_variant_s, i_model) =>
11.124 - if is_some pos_in_sum_variant_s then i_model else [])
11.125 - (option_sequence ~~ variants_separated)
11.126 - |> filter_out (fn place_holder => place_holder = []);
11.127 - \<longrightarrow> [
11.128 - [(1, [1, 2, 3]), (2, [1, 2, 3]), (3, [1, 2, 3]), (4, [1, 2, 3]), (5, [1, 2])],
11.129 - [(1, [1, 2, 3]), (2, [1, 2, 3]), (3, [1, 2, 3]), (4, [1, 2, 3]), (5, [1, 2])]]
11.130 ------- ----------------------------------------------------------------------------------------
11.131 - val equal_descr_pairs = map (get_equal_descr (hd max_i_models)) model_patt
11.132 - |> flat (*a hack for continuing ------------^^-- "turn to PIDE", works for test example*)
11.133 - val env_model = make_env_model equal_descr_pairs
11.134 - val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
11.135 - val subst_eval_list = make_envs_preconds equal_givens
11.136 - val (env_subst, env_eval) = split_list subst_eval_list
11.137 -( *\-- fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------/ *)
11.138 - in
11.139 - ((maxes, max_i_models)(*, env_model, (env_subst, env_eval)*))
11.140 -(* (maxes, max_i_models)*)
11.141 -(*/-- fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------\ * )
11.142 - (env_model, (env_subst, env_eval)
11.143 -( *\--fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------/ *)
11.144 - end
11.145 -( *T_TESTnew*)
11.146 -
11.147
11.148 (*extract the environment from an I_Model.of_max_variant*)
11.149 fun environment_TEST model_patt i_model = of_max_variant model_patt i_model |> #2
12.1 --- a/src/Tools/isac/Specify/specification.sml Wed Sep 27 12:17:44 2023 +0200
12.2 +++ b/src/Tools/isac/Specify/specification.sml Mon Oct 02 12:02:59 2023 +0200
12.3 @@ -91,17 +91,17 @@
12.4 foldl and_ (true, map #1 (where_: Pre_Conds.T)) andalso
12.5 dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> MethodC.id_empty
12.6
12.7 -(* check I_Model.is_complete either for Problem or MethodC *)
12.8 -fun is_complete (pt, pos as (p, Pos.Pbl)) =
12.9 - if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
12.10 - then (I_Model.is_complete o (Ctree.get_obj Ctree.g_pbl pt)) p
12.11 - else raise ERROR ("is_complete: called by PrfObj at " ^ Pos.pos'2str pos)
12.12 - | is_complete (pt, pos as (p, Pos.Met)) =
12.13 - if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
12.14 - then (I_Model.is_complete o (Ctree.get_obj Ctree.g_met pt)) p
12.15 - else raise ERROR ("is_complete: called by PrfObj at " ^ Pos.pos'2str pos)
12.16 - | is_complete (_, pos) =
12.17 - raise ERROR ("is_complete called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)")
12.18 +fun is_complete (pt, (p, _)) =
12.19 + let
12.20 + val (itms, oris, probl, o_spec, spec, ctxt) = case Ctree.get_obj I pt p of
12.21 + Ctree.PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ctxt, ...}
12.22 + => (itms, oris, probl, o_spec, spec, ctxt)
12.23 + | _ => raise ERROR "SpecificationC.is_complete only with PblObj"
12.24 + val (_, pbl_id, met_id) = References.select_input o_spec spec
12.25 + in
12.26 + I_Model.s_are_complete ctxt oris
12.27 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_id, met_id)
12.28 + end
12.29
12.30 (** handle acces to Ctree **)
12.31
13.1 --- a/src/Tools/isac/Test_Code/test-code.sml Wed Sep 27 12:17:44 2023 +0200
13.2 +++ b/src/Tools/isac/Test_Code/test-code.sml Mon Oct 02 12:02:59 2023 +0200
13.3 @@ -45,10 +45,11 @@
13.4 Ctree.Form t => Test_Out.FormKF (UnparseC.term ctxt t)
13.5 | Ctree.ModSpec (_, p_, _, gfr, where_, _) =>
13.6 Test_Out.PpcKF (
13.7 - (case p_ of Pos.Pbl => Test_Out.Problem []
13.8 + (case p_ of
13.9 + Pos.Pbl => Test_Out.Problem []
13.10 | Pos.Met => Test_Out.MethodC []
13.11 - | _ => raise ERROR "TESTg_form: uncovered case",
13.12 - P_Model.from (Proof_Context.theory_of ctxt) gfr where_))
13.13 + | _ => raise ERROR "TESTg_form: uncovered case"),
13.14 + P_Model.from (Proof_Context.theory_of ctxt) gfr where_)
13.15 end
13.16 (* for quick test-print-out, until 'type inout' is removed *)
13.17 fun f2str (Test_Out.FormKF cterm') = cterm'
14.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Wed Sep 27 12:17:44 2023 +0200
14.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Mon Oct 02 12:02:59 2023 +0200
14.3 @@ -420,18 +420,11 @@
14.4 (*if*) Ctree.is_pblobj ppobj (*then*);
14.5
14.6 pt_model ppobj p_;
14.7 -"~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}),
14.8 +"~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, o_spec, hdl), ctxt, ...}),
14.9 Pbl(*Frm,Pbl*)) = (ppobj, p_);
14.10 - val (_, pI, _) = Ctree.get_somespec' spec spec';
14.11 - (*if*) pI = Problem.id_empty (*else*);
14.12 -(* val where_ = if pI = Problem.id_empty then []*)
14.13 -(* else *)
14.14 -(* let *)
14.15 - val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
14.16 - val (_, where_) = (*Pre_Conds.*)check ctxt where_rls where_ (model, I_Model.OLD_to_TEST probl)
14.17 -(* in where_ end *)
14.18 - val allcorrect = I_Model.is_complete probl andalso foldl and_ (true, (map #1 where_))
14.19 -val return_pt_model = Ctree.ModSpec (allcorrect, Pos.Pbl, hdl, probl, where_, spec)
14.20 + val (_, _, met_id) = References.select_input o_spec spec
14.21 + val (allcorr, _) = Pre_Conds.check_internal ctxt (I_Model.OLD_to_TEST probl) (Pos.Met, met_id)
14.22 +val return_pt_model = Ctree.ModSpec (allcorr, Pos.Pbl, hdl, probl, (*where_*)[(*Problem.from_store in check*)], spec)
14.23
14.24 (*|------------------- continue with TESTg_form ----------------------------------------------*)
14.25 val Ctree.ModSpec (spec as (_, p_, _, gfr, where_, _)) =
15.1 --- a/test/Tools/isac/Specify/refine.sml Wed Sep 27 12:17:44 2023 +0200
15.2 +++ b/test/Tools/isac/Specify/refine.sml Mon Oct 02 12:02:59 2023 +0200
15.3 @@ -501,6 +501,7 @@
15.4
15.5 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "solutions L"*)
15.6
15.7 +(*WAS at change set b817019bfda7 and before (while Test_Isac.thy was without other errors):
15.8 val www =
15.9 case f of Test_Out.PpcKF (Test_Out.Problem [],
15.10 {Find = [Incompl "solutions []"], With = [],
15.11 @@ -510,6 +511,7 @@
15.12 | _ => error "--- Refine_Problem broken 1";
15.13 if www = "matches (x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\nmatches (?b * x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\nmatches (?a + x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\nmatches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8)"
15.14 then () else error "--- Refine_Problem broken 2";
15.15 +*)
15.16 (*ML> f;
15.17 val it = Form' (Test_Out.PpcKF (0,EdUndef,0,Nundef,
15.18 (Problem ["LINEAR", "univariate", "equation", "test"], <<<<<===== diff.to above WN120313
16.1 --- a/test/Tools/isac/Specify/specify.sml Wed Sep 27 12:17:44 2023 +0200
16.2 +++ b/test/Tools/isac/Specify/specify.sml Mon Oct 02 12:02:59 2023 +0200
16.3 @@ -777,7 +777,7 @@
16.4 "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
16.5 "(4, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
16.6 "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]";
16.7 -(*+*)I_Model.is_complete pbl = true;
16.8 +(*+*)val (true, []) = Pre_Conds.check_internal ctxt (I_Model.OLD_to_TEST pbl) (Pos.Met, mI');
16.9 (*+*)I_Model.to_string @{context} met = "[\n" ^
16.10 "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
16.11 "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
17.1 --- a/test/Tools/isac/Test_Isac.thy Wed Sep 27 12:17:44 2023 +0200
17.2 +++ b/test/Tools/isac/Test_Isac.thy Mon Oct 02 12:02:59 2023 +0200
17.3 @@ -277,939 +277,6 @@
17.4 ML_file "Specify/cas-command.sml"
17.5 ML_file "Specify/p-spec.sml"
17.6 ML_file "Specify/specify.sml"
17.7 -ML \<open>
17.8 -\<close> ML \<open>
17.9 -(* Title: "Specify/specify.sml"
17.10 - Author: Walther Neuper
17.11 - (c) due to copyright terms
17.12 -*)
17.13 -
17.14 -"-----------------------------------------------------------------------------------------------";
17.15 -"table of contents -----------------------------------------------------------------------------";
17.16 -"-----------------------------------------------------------------------------------------------";
17.17 -"-----------------------------------------------------------------------------------------------";
17.18 -"----------- maximum-example: Specify.finish_phase ---------------------------------------------";
17.19 -"----------- revise Specify.do_all -------------------------------------------------------------";
17.20 -"----------- specify-phase: low level functions ------------------------------------------------";
17.21 -"-----------------------------------------------------------------------------------------------";
17.22 -"-----------------------------------------------------------------------------------------------";
17.23 -"-----------------------------------------------------------------------------------------------";
17.24 -open Pos;
17.25 -open Ctree;
17.26 -open Test_Code;
17.27 -open Tactic;
17.28 -open Specify;
17.29 -open Step;
17.30 -
17.31 -open O_Model;
17.32 -open I_Model;
17.33 -open P_Model;
17.34 -open Specify_Step;
17.35 -open Test_Code;
17.36 -
17.37 -(**** maximum-example: Specify.finish_phase ############################################# ****)
17.38 -"----------- maximum-example: Specify.finish_phase ---------------------------------------------";
17.39 -"----------- maximum-example: Specify.finish_phase ---------------------------------------------";
17.40 -(*//-------- WAS OUT OF Test UNTIL 200209, ERROR PROBABLY FROM INTRO. OF Isabelle's funpack --\\* )
17.41 - val (p,_,f,nxt,_,pt) =
17.42 - Test_Code.init_calc @{context}
17.43 - [(["fixedValues [r=Arbfix]", "maximum A",
17.44 - "valuesFor [a,b]",
17.45 - "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
17.46 - "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
17.47 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
17.48 -
17.49 - "boundVariable a", "boundVariable b", "boundVariable alpha",
17.50 - "interval {x::real. 0 <= x & x <= 2*r}",
17.51 - "interval {x::real. 0 <= x & x <= 2*r}",
17.52 - "interval {x::real. 0 <= x & x <= pi}",
17.53 - "errorBound (eps=(0::real))"],
17.54 - ("Diff_App",["maximum_of", "function"],["Diff_App", "max_by_calculus"])
17.55 - )];
17.56 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
17.57 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
17.58 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
17.59 - (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*)
17.60 - val pits = get_obj g_pbl pt (fst p);
17.61 - writeln (I_Model.to_string ctxt pits);
17.62 -(*[
17.63 -(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
17.64 -(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])),
17.65 -(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
17.66 -(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*)
17.67 - val (pt,p) = Specify.finish_phase (pt,p);
17.68 - val pits = get_obj g_pbl pt (fst p);
17.69 - if I_Model.to_string ctxt pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] ,(rs_, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]))]"
17.70 - then () else error "completetest.sml: new behav. in Specify.finish_phase 3";
17.71 - writeln (I_Model.to_string ctxt pits);
17.72 -(*[
17.73 -(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
17.74 -(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
17.75 -(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
17.76 -(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up>
17.77 -2 = r \<up> 2] ,(relations, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]))]*)
17.78 - val mits = get_obj g_met pt (fst p);
17.79 - if I_Model.to_string ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] ,(rs_, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]"
17.80 - then () else error "completetest.sml: new behav. in Specify.finish_phase 3";
17.81 - writeln (I_Model.to_string ctxt mits);
17.82 -(*[
17.83 -(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
17.84 -(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
17.85 -(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
17.86 -(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up>
17.87 -2 = r \<up> 2] ,(relations, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])),
17.88 -(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
17.89 -(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
17.90 -0 <= x & x <= 2 * r}])),
17.91 -(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
17.92 -( *\\-------- WAS OUT OF Test UNTIL 200209, ERROR PROBABLY FROM INTRO. OF Isabelle's funpack --//*)
17.93 -
17.94 -
17.95 -(**** revise Specify.do_all ############################################################## ****);
17.96 -"----------- revise Specify.do_all -------------------------------------------------------------";
17.97 -"----------- revise Specify.do_all -------------------------------------------------------------";
17.98 -(* from Minisubplb/100-init-rootpbl.sml:
17.99 -val (_(*example text*),
17.100 - (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
17.101 - "Extremum (A = 2 * u * v - u \<up> 2)" ::
17.102 - "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
17.103 - "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
17.104 - "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
17.105 - "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
17.106 - "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
17.107 - "ErrorBound (\<epsilon> = (0::real))" :: []),
17.108 - refs as ("Diff_App",
17.109 - ["univariate_calculus", "Optimisation"],
17.110 - ["Optimisation", "by_univariate_calculus"])))
17.111 - = Store.get (Know_Store.get_expls @ {theory Know_Store}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
17.112 -*)
17.113 -val model = ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
17.114 - "Extremum (A = 2 * u * v - u \<up> 2)" ::
17.115 - "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
17.116 - "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
17.117 - "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
17.118 - "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
17.119 - "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
17.120 - "ErrorBound (\<epsilon> = (0::real))" :: [])
17.121 -val refs = ("Diff_App",
17.122 - ["univariate_calculus", "Optimisation"],
17.123 - ["Optimisation", "by_univariate_calculus"])
17.124 -
17.125 -val (p,_,f,nxt,_,pt) =
17.126 - Test_Code.init_calc @{context} [(model, refs)];
17.127 -"~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))])
17.128 - = (@{context}, [(model, refs)]);
17.129 -
17.130 - Specify.do_all (pt, p);
17.131 -(*//------------------ step into do_all ----------------------------------------------------\\*)
17.132 -"~~~~~ fun do_all , args:"; val (pt, (*old* )pos as( *old*) (p, _)) = (pt, p);
17.133 - val (itms, oris, probl, o_refs, spec, ctxt) = case Ctree.get_obj I pt p of
17.134 - Ctree.PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ctxt, ...}
17.135 - => (itms, oris, probl, o_spec, spec, ctxt)
17.136 - | _ => raise ERROR "LI.by_tactic: no PblObj"
17.137 - val (_, pbl_id', met_id') = References.select_input o_refs spec
17.138 - val {model = pbl_patt, ...} = Problem.from_store ctxt pbl_id';
17.139 - val {model = met_patt, ...} = MethodC.from_store ctxt met_id';
17.140 - val (pbl_imod, met_imod) = I_Model.s_make_complete oris
17.141 - (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
17.142 -;
17.143 -(*-------------------- stop step into do_all -------------------------------------------------*)
17.144 -(*/------------------- check result of I_Model.complete' ------------------------------------\*)
17.145 -\<close> ML \<open>
17.146 -(*+*)if Model_Pattern.to_string @{context} met_patt = "[\"" ^
17.147 - "(#Given, (Constants, fixes))\", \"" ^
17.148 - "(#Given, (Maximum, maxx))\", \"" ^
17.149 - "(#Given, (Extremum, extr))\", \"" ^
17.150 - "(#Given, (SideConditions, sideconds))\", \"" ^
17.151 - "(#Given, (FunctionVariable, funvar))\", \"" ^
17.152 - "(#Given, (Input_Descript.Domain, doma))\", \"" ^
17.153 - "(#Given, (ErrorBound, err))\", \"" ^
17.154 - "(#Find, (AdditionalValues, vals))\"]"
17.155 -(*+*)then () else error "mod_pat CHANGED";
17.156 -\<close> ML \<open>
17.157 -(*+*)if I_Model.to_string_TEST @{context} met_imod = "[\n" ^
17.158 - "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
17.159 - "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
17.160 - "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
17.161 - "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
17.162 - "(7, [1], true ,#undef, (Cor_TEST FunctionVariable a , pen2str, Position.T)), \n" ^
17.163 - "(10, [1, 2], true ,#undef, (Cor_TEST Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^
17.164 - "(12, [1, 2, 3], true ,#undef, (Cor_TEST ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^
17.165 - "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
17.166 -(*+*)then () else error "met_imod CHANGED";
17.167 -(*\------------------- check result of I_Model.complete' ------------------------------------/*)
17.168 -(*\\------------------ step into do_all ----------------------------------------------------//*)
17.169 -
17.170 -\<close> ML \<open>
17.171 -(*-------------------- continuing do_all -----------------------------------------------------*)
17.172 - val (pt, _) = Ctree.cupdate_problem pt p
17.173 - (o_refs, I_Model.TEST_to_OLD pbl_imod, I_Model.TEST_to_OLD met_imod, ctxt)
17.174 -;
17.175 -
17.176 -
17.177 -
17.178 -\<close> ML \<open>
17.179 -(**** specify-phase: low level functions ################################################# ****)
17.180 -"----------- specify-phase: low level functions -----------------------------------------";
17.181 -"----------- specify-phase: low level functions -----------------------------------------";
17.182 -open Pos;
17.183 -open Ctree;
17.184 -open Test_Code;
17.185 -open Tactic;
17.186 -open Specify;
17.187 -open Step;
17.188 -
17.189 -open O_Model;
17.190 -open I_Model;
17.191 -open P_Model;
17.192 -open Specify_Step;
17.193 -
17.194 -val formalise = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
17.195 - "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
17.196 -(*
17.197 - Now follow items for ALL SubProblems,
17.198 - since ROOT MethodC must provide values for "actuals" of ALL SubProblems.
17.199 - See Biegelinie.thy subsection \<open>Survey on Methods\<close>.
17.200 -*)
17.201 -(*
17.202 - Items for MethodC "IntegrierenUndKonstanteBestimmen2"
17.203 -*)
17.204 - "FunktionsVariable x",
17.205 - (*"Biegelinie y", ..already input for Problem above*)
17.206 - "AbleitungBiegelinie dy",
17.207 - "Biegemoment M_b",
17.208 - "Querkraft Q",
17.209 -(*
17.210 - Item for Problem "LINEAR/system", which by [''no_met''] involves refinement
17.211 -*)
17.212 - "GleichungsVariablen [c, c_2, c_3, c_4]"
17.213 -];
17.214 -(*
17.215 - Note: the above sequence of items follows the sequence of formal arguments (and of model items)
17.216 - of MethodC "IntegrierenUndKonstanteBestimmen2"
17.217 -*)
17.218 -val references = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
17.219 -val p = e_pos'; val c = [];
17.220 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(formalise, references)]; (*nxt = Model_Problem*)
17.221 -
17.222 -(*/------------------- check result of Test_Code.init_calc @{context} ----------------------------------------\*)
17.223 -(*+*)val (o_model, ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]), _) =
17.224 - get_obj g_origin pt (fst p);
17.225 -(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
17.226 - "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
17.227 - "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
17.228 - "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
17.229 - "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
17.230 - "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
17.231 - "(6, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"]), \n" ^
17.232 - "(7, [\"1\"], #undef, Biegemoment, [\"M_b\"]), \n" ^
17.233 - "(8, [\"1\"], #undef, Querkraft, [\"Q\"]), \n" ^
17.234 - "(9, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"])]"
17.235 -then () else error "[IntegrierenUndKonstanteBestimmen2] O_Model CHANGED";
17.236 -(*\------------------- check result of Test_Code.init_calc @{context} ----------------------------------------/*)
17.237 -
17.238 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Traegerlaenge L" = nxt
17.239 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Streckenlast q_0" = nxt
17.240 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Biegelinie y" = nxt
17.241 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" = nxt
17.242 -(*/---broken elementwise input to lists---\* )
17.243 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)
17.244 -( *\---broken elementwise input to lists---/*)
17.245 -
17.246 -val return_me_Add_Relation_Randbedingungen = me nxt p c pt; (*\<rightarrow>Specify_Problem ["Biegelinien"]*)
17.247 -(*/------------------- step into me_Add_Relation_Randbedingungen ---------------------------\\*)
17.248 -"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
17.249 - val ctxt = Ctree.get_ctxt pt p
17.250 - val (pt, p) =
17.251 - (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
17.252 - case Step.by_tactic tac (pt, p) of
17.253 - ("ok", (_, _, ptp)) => ptp
17.254 -
17.255 -val ("ok", ([(Specify_Theory "Biegelinie", _, _)], _, _)) =
17.256 - (*case*)
17.257 - Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
17.258 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
17.259 - (p, ((pt, Pos.e_pos'), []));
17.260 - (*if*) Pos.on_calc_end ip (*else*);
17.261 - val (_, probl_id, _) = Calc.references (pt, p);
17.262 -val _ =
17.263 - (*case*) tacis (*of*);
17.264 - (*if*) probl_id = Problem.id_empty (*else*);
17.265 -
17.266 -\<close> ML \<open>
17.267 - switch_specify_solve p_ (pt, ip);
17.268 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
17.269 - (*if*) Pos.on_specification ([], state_pos) (*then*);
17.270 -
17.271 - specify_do_next (pt, input_pos);
17.272 -"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
17.273 - val (_, (p_', tac)) = Specify.find_next_step ptp
17.274 - val ist_ctxt = Ctree.get_loc pt (p, p_)
17.275 -val Specify_Theory "Biegelinie" =
17.276 - (*case*) tac (*of*);
17.277 -
17.278 -Step_Specify.by_tactic_input tac (pt, (p, p_'));
17.279 -
17.280 -(*|------------------- contine me_Add_Relation_Randbedingungen -------------------------------*)
17.281 -(*\------------------- step into me_Add_Relation_Randbedingungen ---------------------------//*)
17.282 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = return_me_Add_Relation_Randbedingungen;
17.283 - val Specify_Theory "Biegelinie" = nxt
17.284 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["Biegelinien"] = nxt
17.285 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
17.286 -
17.287 -(*[], Met*)val return_me_Specify_Method_IntegrierenUndKonstanteBestimmen2
17.288 - = me nxt p c pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)
17.289 -(*/------------------- step into me_Specify_Method_IntegrierenUndKonstanteBestimmen2--------\*)
17.290 -
17.291 -(*/------------------- initial check for whole me ------------------------------------------\*)
17.292 -(*+*)val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt;
17.293 -
17.294 -(*+*)val {origin = (o_model, o_refs, _), probl = i_pbl, meth = i_met, spec, ...} =
17.295 - Calc.specify_data (pt, p);
17.296 -(*+*)if o_refs = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"])
17.297 -(*+*)then () else error "initial o_refs CHANGED";
17.298 -(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
17.299 - "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
17.300 - "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
17.301 - "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
17.302 - "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
17.303 - "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
17.304 - "(6, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"]), \n" ^
17.305 - "(7, [\"1\"], #undef, Biegemoment, [\"M_b\"]), \n" ^
17.306 - "(8, [\"1\"], #undef, Querkraft, [\"Q\"]), \n" ^
17.307 - "(9, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"])]"
17.308 -(*+*)then () else error "initial o_model CHANGED";
17.309 -(*+*)if I_Model.to_string @{context} i_pbl = "[\n" ^
17.310 - "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
17.311 - "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n" ^
17.312 - "(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str), \n" ^
17.313 - "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] , pen2str)]"
17.314 -(*+*)then () else error "initial i_pbl CHANGED";
17.315 -(*+*)if I_Model.to_string @{context} i_met = "[]"
17.316 -(*+*)then () else error "initial i_met CHANGED";
17.317 -(*+*)val (_, ["Biegelinien"], _) = spec;
17.318 -(*\------------------- initial check for whole me ------------------------------------------/*)
17.319 -
17.320 -"~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
17.321 -(*/------------------- step into Step.by_tactic \\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\*)
17.322 - val (pt'''''_', p'''''_') = case
17.323 -
17.324 - Step.by_tactic tac (pt, p) of ("ok", (_, _, ptp)) => ptp;
17.325 -(*/------------------- check for entry to Step.by_tactic -----------------------------------\*)
17.326 -(*+*)val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = tac;
17.327 -(*+*)val {origin = (o_model, _, _), ...} = Calc.specify_data (pt, p);
17.328 -(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
17.329 - "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
17.330 - "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
17.331 - "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
17.332 - "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
17.333 - "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
17.334 - "(6, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"]), \n" ^
17.335 - "(7, [\"1\"], #undef, Biegemoment, [\"M_b\"]), \n" ^
17.336 - "(8, [\"1\"], #undef, Querkraft, [\"Q\"]), \n" ^
17.337 - "(9, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"])]"
17.338 -(*+*)then () else error "o_model AFTER Specify_Method NOTok CHANGED";
17.339 -(*\------------------- check for Step.by_tactic --------------------------------------------/*)
17.340 -"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
17.341 - val Applicable.Yes tac' = (*case*)
17.342 -
17.343 - Step.check tac (pt, p) (*of*);
17.344 -"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
17.345 - (*if*) Tactic.for_specify tac (*then*);
17.346 -
17.347 -Specify_Step.check tac (ctree, pos);
17.348 -"~~~~~ fun check , args:"; val ((Tactic.Specify_Method mID), (ctree, pos)) = (tac, (ctree, pos));
17.349 -
17.350 - val (o_model''''', _, i_model''''') =
17.351 - Specify_Step.complete_for mID (ctree, pos);
17.352 -"~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (mID, (ctree, pos));
17.353 - val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
17.354 - ...} = Calc.specify_data (ctree, pos);
17.355 - val (dI, _, _) = References.select_input o_refs refs;
17.356 - val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
17.357 - val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
17.358 - val (o_model', ctxt') =
17.359 -
17.360 - O_Model.complete_for m_patt root_model (o_model, ctxt);
17.361 -(*/------------------- check entry to O_Model.complete_for -----------------------------------------\*)
17.362 -(*+*)Model_Pattern.to_string @{context} m_patt = "[\"" ^
17.363 - "(#Given, (Traegerlaenge, l))\", \"" ^
17.364 - "(#Given, (Streckenlast, q))\", \"" ^
17.365 - "(#Given, (FunktionsVariable, v))\", \"" ^
17.366 - "(#Given, (GleichungsVariablen, vs))\", \"" ^
17.367 - "(#Given, (AbleitungBiegelinie, id_abl))\", \"" ^
17.368 - "(#Find, (Biegelinie, b))\", \"" ^
17.369 - "(#Relate, (Randbedingungen, s))\"]";
17.370 -(*+*) O_Model.to_string @{context} root_model;
17.371 -(*\------------------- check entry to O_Model.complete_for -----------------------------------------/*)
17.372 -"~~~~~ fun complete_for , args:"; val (m_patt, root_model, (o_model, ctxt)) = (m_patt, root_model, (o_model, ctxt));
17.373 - val missing = m_patt |> filter_out
17.374 - (fn (_, (descriptor, _)) => (member op = (map #4 o_model) descriptor));
17.375 - val add = (root_model
17.376 - |> filter
17.377 - (fn (_, _, _, descriptor, _) => (member op = (map (fst o snd) missing)) descriptor))
17.378 -;
17.379 - ((o_model @ add)
17.380 - |> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
17.381 - |> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
17.382 - |> add_enumerate (* for correct enumeration *)
17.383 - |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
17.384 - ctxt |> ContextC.add_constraints (add |> values |> TermC.vars')) (*return from O_Model.complete_for*);
17.385 -"~~~~~ fun complete_for \<longrightarrow>fun Specify_Step.complete_for , return:"; val (o_model', ctxt') =
17.386 - ((o_model @ add)
17.387 - |> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
17.388 - |> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
17.389 - |> add_enumerate (* for correct enumeration *)
17.390 - |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
17.391 - ctxt |> ContextC.add_constraints (add |> values |> TermC.vars'));
17.392 -
17.393 -(*/------------------- check of result from O_Model.complete_for -----------------------------------\*)
17.394 -(*+*) O_Model.to_string @{context} o_model'; "O_Model.complete_for: result o_model CHANGED";
17.395 -(*\------------------- check of result from O_Model.complete_for -----------------------------------/*)
17.396 -
17.397 - val thy = ThyC.get_theory @{context} dI
17.398 - val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
17.399 -
17.400 - (o_model', ctxt', i_model) (*return from Specify_Step.complete_for*);
17.401 -
17.402 -"~~~~~ fun complete_for \<longrightarrow>fun Specify_Step.check , return:"; val (o_model, _, i_model) =
17.403 - (o_model', ctxt', i_model);
17.404 -
17.405 - Applicable.Yes (Tactic.Specify_Method' (mID, o_model, i_model)) (*return from Specify_Step.check*);
17.406 -"~~~~~ fun Specify_Step.check \<longrightarrow>fun Step.check \<longrightarrow>fun Step.by_tactic , return:"; val (Applicable.Yes tac') =
17.407 - (Applicable.Yes (Tactic.Specify_Method' (mID, o_model, i_model)));
17.408 - (*if*) Tactic.for_specify' tac' (*then*);
17.409 - val ("ok", ([], [], (_, _))) =
17.410 -
17.411 -Step_Specify.by_tactic tac' ptp;
17.412 -"~~~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt,pos as (p, _))) =
17.413 - (tac', ptp);
17.414 -(*NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
17.415 -(*NEW*) ...} = Calc.specify_data (pt, pos);
17.416 -(*NEW*) val (dI, _, mID) = References.select_input o_refs refs;
17.417 -(*NEW*) val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
17.418 -(*NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
17.419 -(*NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
17.420 -(*NEW*) val thy = ThyC.get_theory @{context} dI
17.421 -(*NEW*) val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
17.422 -(*NEW*) val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, o_model', i_model))
17.423 -(*NEW*) (Istate_Def.Uistate, ctxt') (pt, pos)
17.424 -
17.425 -(*/------------------- check result of Step_Specify.by_tactic ------------------------------\*)
17.426 -(*+*)val {origin = (o_model, _, _), meth, ...} = Calc.specify_data (pt, pos);
17.427 -(*+*)O_Model.to_string @{context} o_model;
17.428 -(*+*)if I_Model.to_string @{context} meth = "[\n" ^
17.429 - "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
17.430 - "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n" ^
17.431 - "(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str), \n" ^
17.432 - "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] , pen2str), \n" ^
17.433 - "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^
17.434 - "(6 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der), \n" ^
17.435 - "(7 ,[1] ,false ,#Given ,Mis Biegemoment id_momentum), \n" ^
17.436 - "(8 ,[1] ,false ,#Given ,Mis Querkraft id_lat_force), \n" ^
17.437 - "(9 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs)]"
17.438 -(*+*)then () else error "result of Step_Specify.by_tactic o_model CHANGED";
17.439 -(*\------------------- check result of Step_Specify.by_tactic ------------------------------/*)
17.440 -(*\------------------- step into Step.by_tactic /////////////////////////////////////////////*)
17.441 -
17.442 -
17.443 -\<close> ML \<open>
17.444 -val (_, ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =
17.445 - Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []) (*of*);
17.446 -(*/------------------- step into Step.do_next \\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\*)
17.447 -"~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
17.448 - (p'''''_', ((pt'''''_', Pos.e_pos'), []));
17.449 - (*if*) Pos.on_calc_end ip (*else*);
17.450 - val (_, probl_id, _) = Calc.references (pt, p);
17.451 - val _ = (*case*) tacis (*of*);
17.452 - (*if*) probl_id = Problem.id_empty (*else*);
17.453 -
17.454 -val (_, ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =
17.455 - switch_specify_solve p_ (pt, ip);
17.456 -"~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
17.457 - (*if*) Pos.on_specification ([], state_pos) (*then*);
17.458 -
17.459 -val ("ok", ([(Add_Given "FunktionsVariable x", _, _)], [], (pt'''''_'', p'''''_''))) =
17.460 - Step.specify_do_next (pt, input_pos);
17.461 -(*/------------------- check result of specify_do_next -------------------------------------\*)
17.462 -(*+*)val {origin = (ooo_mod, _, _), meth, ...} = Calc.specify_data (pt'''''_'', p'''''_'');
17.463 -(*+*) O_Model.to_string @{context} ooo_mod; "result of Step_Specify.by_tactic o_model CHANGED";
17.464 -(*+*)if I_Model.to_string @{context} meth = "[\n" ^
17.465 - "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
17.466 - "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n" ^
17.467 - "(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str), \n" ^
17.468 - "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] , pen2str), \n" ^
17.469 - "(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x , pen2str), \n" ^
17.470 - "(6 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der), \n" ^
17.471 - "(7 ,[1] ,false ,#Given ,Mis Biegemoment id_momentum), \n" ^
17.472 - "(8 ,[1] ,false ,#Given ,Mis Querkraft id_lat_force), \n" ^
17.473 - "(9 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs)]"
17.474 -(*+*)then () else error "result of Step_Specify.by_tactic i_model CHANGED";
17.475 -(*\------------------- check result of specify_do_next -------------------------------------/*)
17.476 -"~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
17.477 -
17.478 -(**)val (_, (p_', Add_Given "FunktionsVariable x")) =(**)
17.479 - Specify.find_next_step ptp;
17.480 -"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
17.481 - val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
17.482 - spec = refs, ...} = Calc.specify_data (pt, pos);
17.483 - val ctxt = Ctree.get_ctxt pt pos;
17.484 - (*if*) Ctree.just_created (pt, (p, p_)) andalso origin <> Ctree.e_origin (*else*);
17.485 - (*if*) p_ = Pos.Pbl (*else*);
17.486 -
17.487 -val return = for_problem ctxt oris (o_refs, refs) (pbl, met);
17.488 -"~~~~~ fun for_method , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
17.489 - (oris, (o_refs, refs), (pbl, met));
17.490 - val cmI = if mI = MethodC.id_empty then mI' else mI;
17.491 - val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI;
17.492 - val (preok, _) = Pre_Conds.check ctxt where_rls where_ (mpc, I_Model.OLD_to_TEST met);
17.493 -"~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) = (return);
17.494 -(*/------------------- check within find_next_step -----------------------------------------\*)
17.495 -(*+*)Model_Pattern.to_string @{context} (MethodC.from_store ctxt mI' |> #model) = "[\"" ^
17.496 - "(#Given, (Traegerlaenge, l))\", \"" ^
17.497 - "(#Given, (Streckenlast, q))\", \"" ^
17.498 - "(#Given, (FunktionsVariable, v))\", \"" ^ (* <---------- take m_field from here !!!*)
17.499 - "(#Given, (GleichungsVariablen, vs))\", \"" ^
17.500 - "(#Given, (AbleitungBiegelinie, id_abl))\", \"" ^
17.501 - "(#Find, (Biegelinie, b))\", \"" ^
17.502 - "(#Relate, (Randbedingungen, s))\"]";
17.503 -(*\------------------- check within find_next_step -----------------------------------------/*)
17.504 -
17.505 - (*case*) item_to_add (ThyC.get_theory @{context} (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
17.506 -"~~~~~ ~ fun item_to_add , args:"; val (thy, oris, _, itms) =
17.507 - ((ThyC.get_theory @{context} (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
17.508 -(*OLD*)fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v (**)andalso (#3 ori) <> "#undef"(**)
17.509 - fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
17.510 - fun test_id ids r = member op= ids (#1 (r : O_Model.single))
17.511 - fun test_subset itm (_, _, _, d, ts) =
17.512 - (I_Model.descriptor (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.o_model_values (#5 itm), ts)
17.513 - fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
17.514 - | false_and_not_Sup (_, _, false, _, _) = true
17.515 - | false_and_not_Sup _ = false
17.516 - val v = if itms = [] then 1 else Pre_Conds.max_variant itms
17.517 - val vors = if v = 0 then oris else filter (testr_vt v) oris (* oris..vat *)
17.518 - val vits =
17.519 - if v = 0
17.520 - then itms (* because of dsc without dat *)
17.521 - else filter (testi_vt v) itms; (* itms..vat *)
17.522 - val icl = filter false_and_not_Sup vits; (* incomplete *)
17.523 -
17.524 -(*/------------------- check within item_to_add --------------------------------------------\*)
17.525 -(*+*)if I_Model.to_string @{context} icl = "[\n" ^ (*.. values, not formals*)
17.526 - "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^ (*.. values, not formals*)
17.527 - "(6 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der), \n" ^ (*.. values, not formals*)
17.528 - "(7 ,[1] ,false ,#Given ,Mis Biegemoment id_momentum), \n" ^ (*.. values, not formals*)
17.529 - "(8 ,[1] ,false ,#Given ,Mis Querkraft id_lat_force), \n" ^ (*.. values, not formals*)
17.530 - "(9 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs)]"
17.531 -(*+*)then () else error "icl within item_to_add CHANGED";
17.532 -(*+*) O_Model.to_string @{context} vors; "vors within item_to_add CHANGED";
17.533 -(*+*)if I_Model.to_string @{context} itms = "[\n" ^
17.534 - "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
17.535 - "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n" ^
17.536 - "(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str), \n" ^
17.537 - "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] , pen2str), \n" ^
17.538 - "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^
17.539 - "(6 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der), \n" ^
17.540 - "(7 ,[1] ,false ,#Given ,Mis Biegemoment id_momentum), \n" ^
17.541 - "(8 ,[1] ,false ,#Given ,Mis Querkraft id_lat_force), \n" ^
17.542 - "(9 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs)]"
17.543 -(*+*)then () else error "i_model within item_to_add CHANGED";
17.544 -(*\------------------- check within item_to_add --------------------------------------------/*)
17.545 -
17.546 - (*if*) icl = [] (*else*);
17.547 - val SOME ori =(*case*) find_first (test_subset (hd icl)) vors (*of*);
17.548 -
17.549 -(*+*)val (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]) = ori
17.550 -(*+*)val SOME ("#Given", "FunktionsVariable x") =
17.551 -
17.552 - SOME
17.553 - (I_Model.get_field_term thy ori (hd icl)) (*return from item_to_add*);
17.554 -"~~~~~ ~~ fun get_field_term , args:"; val (thy, (_, _, _, d, ts), (_, _, _, fd, itm_)) = (thy, ori, (hd icl));
17.555 -
17.556 -val rrrrr =
17.557 - (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join)
17.558 - (d, subtract op = (o_model_values itm_) ts)) (*return from get_field_term*);
17.559 -"~~~~~ ~~ from fun get_field_term \<longrightarrow>fun item_to_add \<longrightarrow>fun find_next_step , return:"; val (SOME (fd, ct')) =
17.560 - (SOME rrrrr);
17.561 - ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*return from find_next_step*);
17.562 -
17.563 -(*+*)val Add_Given "FunktionsVariable x" = P_Model.mk_additem fd ct';
17.564 -
17.565 -"~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) =
17.566 - ("dummy", (Pos.Met, P_Model.mk_additem fd ct'));
17.567 - val ist_ctxt = Ctree.get_loc pt (p, p_)
17.568 - val _ = (*case*) tac (*of*);
17.569 -
17.570 - ("dummy",
17.571 -Step_Specify.by_tactic_input tac (pt, (p, p_'))) (*return from specify_do_next*);
17.572 -"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =
17.573 - (tac, (pt, (p, p_')));
17.574 -
17.575 - val ("ok", ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =
17.576 - Specify.by_Add_ "#Given" ct ptp (*return from by_tactic_input*);
17.577 -"~~~~~ ~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, ptp);
17.578 - val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
17.579 - (*if*) p_ = Pos.Met (*then*);
17.580 - val (i_model, m_patt) = (met,
17.581 - (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
17.582 -
17.583 -val Add (5, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), (Free ("fun_var", _), [Free ("x", _)]))) =
17.584 - (*case*)
17.585 - I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
17.586 -"~~~~~ ~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
17.587 - (ctxt, m_field, oris, i_model, m_patt, ct);
17.588 -(*.NEW*) val SOME (t as (descriptor $ _)) = (*case*) ParseC.term_opt ctxt str (*of*);
17.589 -(*.NEW*) val SOME m_field = (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
17.590 -
17.591 -val ("", (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), [Free ("x", _)]) =
17.592 - (*case*)
17.593 - O_Model.contains ctxt m_field o_model t (*of*);
17.594 -"~~~~~ ~~~ fun contains , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
17.595 - val ots = ((distinct op =) o flat o (map #5)) ori
17.596 - val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots
17.597 - val (d, ts) = Input_Descript.split t
17.598 - val ids = map (fst o dest_Free) (((distinct op =) o (flat o (map TermC.vars))) ts);
17.599 - (*if*) (subtract op = oids ids) <> [] (*else*);
17.600 - (*if*) d = TermC.empty (*else*);
17.601 - (*if*) member op = (map #4 ori) d (*then*);
17.602 -
17.603 - associate_input ctxt sel (d, ts) ori;
17.604 -"~~~~~ ~~~~ fun associate_input , args:"; val (ctxt, m_field, (descript, vals), ((id, vat, m_field', descript', vals') :: oris)) =
17.605 - (ctxt, sel, (d, ts), ori);
17.606 -
17.607 -(*/------------------- check within associate_input ------------------------------------------\*)
17.608 -(*+*)val Add_Given "FunktionsVariable x" = tac;
17.609 -(*+*)m_field = "#Given";
17.610 -(*+*)val Const (\<^const_name>\<open>FunktionsVariable\<close>, _) = descript;
17.611 -(*+*)val [Free ("x", _)] = vals;
17.612 -(*+*)O_Model.to_string @{context} ori = "[\n" ^
17.613 - "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
17.614 - "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
17.615 - "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
17.616 - "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
17.617 - "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
17.618 - "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
17.619 - "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]";
17.620 -(*+*)val (id, vat, m_field', descript', vals') = nth 5 ori
17.621 -(*+*)val (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]) =
17.622 - (id, vat, m_field', descript', vals')
17.623 -(*\------------------- check within associate_input ----------------------------------------/*)
17.624 -(*\------------------- step into me_Specify_Method_IntegrierenUndKonstanteBestimmen2--------*)
17.625 -(*[], Met*)val (p,_,f,nxt,_,pt) = return_me_Specify_Method_IntegrierenUndKonstanteBestimmen2
17.626 - val Add_Given "FunktionsVariable x" = nxt;
17.627 -
17.628 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy" = nxt
17.629 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Biegemoment M_b" = nxt
17.630 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Querkraft Q" = nxt
17.631 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]" = nxt
17.632 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
17.633 -
17.634 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
17.635 -(*/------------------- check entry to me Model_Problem -------------------------------------\*)
17.636 -(*+*)val ([1], Pbl) = p;
17.637 -(*+*)val (o_model, ("Biegelinie", ["vonBelastungZu", "Biegelinien"], ["Biegelinien", "ausBelastung"]), _) =
17.638 - get_obj g_origin pt (fst p);
17.639 -(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
17.640 - "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
17.641 - "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
17.642 - "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
17.643 -(*
17.644 -.. here the O_Model does NOT know, which MethodC will be chosen,
17.645 -so "belastung_zu_biegelinie q__q v_v b_b id_abl" is NOT known,
17.646 -"b_b" and "id_abl" are NOT missing.
17.647 -*)
17.648 -then () else error "[Biegelinien, ausBelastung] initial O_Model CHANGED";
17.649 -(*\------------------- check entry to me Model_Problem -------------------------------------/*)
17.650 -
17.651 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "Streckenlast q_0"*)
17.652 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)
17.653 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "Funktionen funs'''":*)
17.654 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Theory "Biegelinie"*)
17.655 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Problem ["vonBelastungZu", "Biegelinien"]*)
17.656 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Method ["Biegelinien", "ausBelastung"]*)
17.657 -
17.658 -(*[1], Met*)val return_me_Specify_Method_ausBelastung = me nxt p c pt; (*\<rightarrow>Add_Given "Biegelinie y"*)
17.659 -(*//------------------ step into me_Specify_Method_ausBelastung ----------------------------\\*)
17.660 -(*+*)val Specify_Method ["Biegelinien", "ausBelastung"] = nxt;
17.661 -(*+*)(* by \<up> \<up> \<up> \<up> "b_b" and "id_abl" must be requested: PUT THEM INTO O_Model*)
17.662 -
17.663 -"~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
17.664 -
17.665 - val ("ok", ([], [], (_, _))) = (*case*)
17.666 - Step.by_tactic tac (pt, p) (*of*);
17.667 -"~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
17.668 - val Applicable.Yes tac' = (*case*) check tac (pt, p) (*of*);
17.669 - (*if*) Tactic.for_specify' tac' (*then*);
17.670 -
17.671 - val ("ok", ([], [], (_, _))) =
17.672 -Step_Specify.by_tactic tac' ptp;
17.673 -(*/------------------- initial check for Step_Specify.by_tactic ----------------------------\*)
17.674 -(*+*)val (o_model, ("Biegelinie", ["vonBelastungZu", "Biegelinien"], ["Biegelinien", "ausBelastung"]), _) =
17.675 - get_obj g_origin pt (fst p);
17.676 -(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
17.677 - "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
17.678 - "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
17.679 - "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
17.680 -(*
17.681 -.. here the MethodC has been determined by the user,
17.682 -so "belastung_zu_biegelinie q__q v_v b_b id_abl" IS KNOWN and,
17.683 -"b_b" and "id_abl" WOULD BE missing (added by O_Model.).
17.684 -*)
17.685 -then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY MethodC";
17.686 -(*\------------------- initial check for Step_Specify.by_tactic ----------------------------/*)
17.687 -"~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt, pos as (p, _))) =
17.688 - (tac', ptp);
17.689 -(*.NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt,
17.690 -(*.NEW*) ...} =Calc.specify_data (pt, pos);
17.691 -(*.NEW*) val (dI, _, mID) = References.select_input o_refs refs;
17.692 -(*.NEW*) val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
17.693 -(*.NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
17.694 -(*.NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt);
17.695 -
17.696 -(*/------------------- check for entry to O_Model.complete_for -----------------------------\*)
17.697 -(*+*)if mID = ["Biegelinien", "ausBelastung"]
17.698 -(*+*)then () else error "MethodC [Biegelinien, ausBelastung] CHANGED";
17.699 -(*+*)if Model_Pattern.to_string @{context} m_patt = "[\"" ^
17.700 - "(#Given, (Streckenlast, q__q))\", \"" ^
17.701 - "(#Given, (FunktionsVariable, v_v))\", \"" ^
17.702 - "(#Given, (Biegelinie, b_b))\", \"" ^
17.703 - "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^
17.704 - "(#Given, (Biegemoment, id_momentum))\", \"" ^
17.705 - "(#Given, (Querkraft, id_lat_force))\", \"" ^
17.706 - "(#Find, (Funktionen, fun_s))\"]"
17.707 -(*+*)then () else error "[Biegelinien, ausBelastung] Model_Pattern CHANGED";
17.708 -(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
17.709 - "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
17.710 - "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
17.711 - "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
17.712 -(*+*)then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY MethodC CHANGED";
17.713 -(*+*) O_Model.to_string @{context} root_model;
17.714 -(*+*) O_Model.to_string @{context} o_model';
17.715 - "[Biegelinien, ausBelastung] O_Model EXTENDED BY MethodC CHANGED";
17.716 -(*\------------------- check for entry to O_Model.complete_for -----------------------------/*)
17.717 -
17.718 - O_Model.complete_for m_patt root_model (o_model, ctxt);
17.719 -"~~~~ fun complete_for , args:"; val (m_patt, root_model, (o_model, ctxt)) =
17.720 - (m_patt, root_model, (o_model, ctxt));
17.721 - val missing = m_patt |> filter_out
17.722 - (fn (_, (descriptor, _)) => (member op = (map #4 o_model) descriptor))
17.723 -;
17.724 - val add = root_model
17.725 - |> filter
17.726 - (fn (_, _, _, descriptor, _) => (member op = (map (fst o snd) missing)) descriptor)
17.727 -;
17.728 - (o_model @ add
17.729 -(*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
17.730 -(*NEW*)
17.731 - |> map (fn (_, b, c, d, e) => (b, c, d, e))
17.732 - |> add_enumerate
17.733 - |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),
17.734 - ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars')) (*return from O_Model.complete_for*);
17.735 -"~~~~ from fun O_Model.complete_for \<longrightarrow>Step_Specify.by_tactic , return:"; val (o_model', ctxt') =
17.736 - ((o_model @ add)
17.737 -(*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
17.738 -(*NEW*)
17.739 - |> map (fn (_, b, c, d, e) => (b, c, d, e))
17.740 - |> add_enumerate
17.741 - |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),
17.742 - ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars'));
17.743 -
17.744 -(*/------------------- check within O_Model.complete_for -------------------------------------------\*)
17.745 -(*+*) O_Model.to_string @{context} o_model';
17.746 - "[Biegelinien, ausBelastung] O_Model EXTENDED BY MethodC CHANGED";
17.747 -(*\------------------- check within O_Model.complete_for -------------------------------------------/*)
17.748 -
17.749 -(*.NEW*) val thy = ThyC.get_theory @{context} dI
17.750 -(*.NEW*) val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
17.751 -(*.NEW*) val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, o_model', i_model))
17.752 -(*.NEW*) (Istate_Def.Uistate, ctxt') (pt, pos)
17.753 -;
17.754 -(*+*) I_Model.to_string @{context} i_model; "[Biegelinien, ausBelastung] I_Model CHANGED 1";
17.755 -(*+*)val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt, ...} =
17.756 -(*+*) Calc.specify_data (pt, pos);
17.757 -(*+*)pos = ([1], Met);
17.758 -
17.759 - ("ok", ([], [], (pt, pos))) (*return from Step_Specify.by_tactic*);
17.760 -"~~~ from Step_Specify.by_tactic \<longrightarrow>Step.by_tactic \<longrightarrow>fun me , return:"; val ("ok", (_, _, (pt, p))) =
17.761 - ("ok", ([], [], (pt, pos)));
17.762 -(* val ("helpless", ([(xxxxx, _, _)], _, _)) = (*case*)*)
17.763 - (* SHOULD BE \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> Add_Given "Biegelinie y" | Add_Given "AbleitungBiegelinie dy"*)
17.764 -
17.765 -val ("ok", ([( Add_Given "Biegelinie y", _, _)], [], _)) =
17.766 - Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
17.767 -"~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
17.768 -(*.NEW*)(*if*) on_calc_end ip (*else*);
17.769 -(*.NEW*) val (_, probl_id, _) = Calc.references (pt, p);
17.770 -(*-"-*) val _ = (*case*) tacis (*of*);
17.771 -(*.NEW*) (*if*) probl_id = Problem.id_empty (*else*);
17.772 -
17.773 -(*.NEW*)val ("ok", ([(Add_Given "Biegelinie y", _, _)], _, _)) =
17.774 - switch_specify_solve p_ (pt, ip);
17.775 -"~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
17.776 - (*if*) Pos.on_specification ([], state_pos) (*then*);
17.777 -
17.778 - val ("ok", ([(Add_Given "Biegelinie y", _, _)], _, _)) =
17.779 - specify_do_next (pt, input_pos);
17.780 -"~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
17.781 -
17.782 - val (_, (p_', tac)) =
17.783 - Specify.find_next_step ptp;
17.784 -"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
17.785 - val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
17.786 - spec = refs, ...} = Calc.specify_data (pt, pos);
17.787 - val ctxt = Ctree.get_ctxt pt pos
17.788 -;
17.789 -(*+*)O_Model.to_string @{context} oris = "[\n" ^
17.790 - "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
17.791 - "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
17.792 - "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
17.793 - "(4, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
17.794 - "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]";
17.795 -(*+*)I_Model.is_complete pbl = true;
17.796 -(*+*)I_Model.to_string @{context} met = "[\n" ^
17.797 - "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
17.798 - "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
17.799 - "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^
17.800 - "(4 ,[1] ,false ,#Given ,Mis Biegelinie b_b), \n" ^
17.801 - "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]";
17.802 -
17.803 - (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
17.804 - (*if*) p_ = Pos.Pbl (*else*);
17.805 -val return = for_method ctxt oris (o_refs, refs) (pbl, met);
17.806 -"~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) = (return);
17.807 -
17.808 - val ist_ctxt = Ctree.get_loc pt (p, p_)
17.809 - val Add_Given "Biegelinie y" = (*case*) tac (*of*);
17.810 -val return = Step_Specify.by_tactic_input tac (pt, (p, p_'));
17.811 -(*+*)val Add_Given "Biegelinie y" = tac;
17.812 - val ist_ctxt = Ctree.get_loc pt (p, p_)
17.813 - val _ = (*case*) tac (*of*);
17.814 -
17.815 - val (_, ([(Add_Given "Biegelinie y", _, _)], _, (p'''''_'', ([1], Met)))) =
17.816 -Step_Specify.by_tactic_input tac (pt, (p, p_'))
17.817 -(*/------------------- check result of Step_Specify.by_tactic_input ------------------------\*)
17.818 -(*+*)val {meth, ...} = Calc.specify_data (p'''''_'', ([1], Met));
17.819 -(*+*)I_Model.to_string @{context} meth = "[\n" ^ (* result does NOT show Add_Given "Biegelinie y" *)
17.820 - "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
17.821 - "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
17.822 - "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^
17.823 - "(4 ,[1] ,false ,#Given ,Mis Biegelinie b_b), \n" ^
17.824 - "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]";
17.825 -(*\------------------- check result of Step_Specify.by_tactic_input ------------------------/*)
17.826 -"~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) = (tac, (pt, (p, p_')));
17.827 -
17.828 - Specify.by_Add_ "#Given" ct ptp;
17.829 -"~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, ptp);
17.830 - val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
17.831 - (*if*) p_ = Pos.Met (*then*);
17.832 - val (i_model, m_patt) = (met,
17.833 - (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
17.834 -
17.835 -val Add (4, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Biegelinie\<close>, _), [Free ("y", _)]), (Free ("b_b", _), [Free ("y", _)]))) =
17.836 - (*case*)
17.837 - check_single ctxt m_field oris i_model m_patt ct (*of*);
17.838 -
17.839 -(*/------------------- check for entry to check_single -------------------------------------\*)
17.840 -(*+*) O_Model.to_string @{context} oris; "[Biegelinien, ausBelastung] O_Model CHANGED for entry";
17.841 -(*+*) I_Model.to_string ctxt met; "[Biegelinien, ausBelastung] I_Model CHANGED for entry";
17.842 -(*\------------------- check for entry to check_single -------------------------------------/*)
17.843 -
17.844 -"~~~~~ ~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
17.845 - (ctxt, sel, oris, met, ((#model o MethodC.from_store ctxt) cmI), ct);
17.846 - val SOME t = (*case*) ParseC.term_opt ctxt str (*of*);
17.847 -
17.848 -(*+*)val Const (\<^const_name>\<open>Biegelinie\<close>, _) $ Free ("y", _) = t;
17.849 -
17.850 -(*("associate_input: input ('Biegelinie y') not found in oris (typed)", (0, [], "#Given", Const (\<^const_name>\<open>Biegelinie\<close>, "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("y", "real \<Rightarrow> real")]), [])*)
17.851 - (*case*)
17.852 - contains ctxt m_field o_model t (*of*);
17.853 -"~~~~~ ~~ fun contains , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
17.854 - val ots = ((distinct op =) o flat o (map #5)) ori
17.855 - val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots
17.856 - val (d, ts) = Input_Descript.split t
17.857 - val ids = map (fst o dest_Free) (((distinct op =) o (flat o (map TermC.vars))) ts);
17.858 - (*if*) (subtract op = oids ids) <> [] (*else*);
17.859 - (*if*) d = TermC.empty (*else*);
17.860 - (*if*) not (subset op = (map make_typeless ts, map make_typeless ots)) (*else*);
17.861 -
17.862 - (*case*) O_Model.associate_input' ctxt sel ts ori (*of*);
17.863 -"~~~~~ ~~~ fun associate_input' , args:"; val (ctxt, sel, ts, ((id, vat, sel', d, ts') :: oris)) = (ctxt, sel, ts, ori);
17.864 -
17.865 -(*+/---------------- bypass recursion of associate_input' ----------------\*)
17.866 -(*+*)O_Model.to_string @{context} oris = "[\n" ^
17.867 - "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
17.868 - "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
17.869 - "(4, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
17.870 - "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]";
17.871 -(*+*)val (id, vat, sel', d, ts') = nth 3 oris; (* 3rd iteration *)
17.872 -(*+\---------------- bypass recursion of associate_input' ----------------/*)
17.873 -
17.874 - (*if*) sel = sel' andalso (inter op = ts ts') <> [] (*else*);
17.875 -
17.876 -(*/------------------- check within associate_input' -------------------------------\*)
17.877 -(*+*)if sel = "#Given" andalso sel' = "#Given"
17.878 -(*+*)then () else error "associate_input' Model_Pattern CHANGED";
17.879 -(*BUT: m_field can change from root-Problem to sub-MethodC --------------------vvv*)
17.880 -(* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
17.881 -(*+*)if (Problem.from_store ctxt ["vonBelastungZu", "Biegelinien"] |> #model |> Model_Pattern.to_string @{context}) = "[\"" ^
17.882 - "(#Given, (Streckenlast, q_q))\", \"" ^
17.883 - "(#Given, (FunktionsVariable, v_v))\", \"" ^
17.884 - "(#Find, (Funktionen, funs'''))\"]"
17.885 -(*+*)then () else error "associate_input' Model_Pattern of Subproblem CHANGED";
17.886 -(* root-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv ------------------------------------- \<up>*)
17.887 -(*+*)if (Problem.from_store ctxt ["Biegelinien"] |> #model |> Model_Pattern.to_string @{context}) = "[\"" ^
17.888 - "(#Given, (Traegerlaenge, l_l))\", \"" ^
17.889 - "(#Given, (Streckenlast, q_q))\", \"" ^
17.890 - "(#Find, (Biegelinie, b_b))\", \"" ^ (*------------------------------------- \<up> *)
17.891 - "(#Relate, (Randbedingungen, r_b))\"]"
17.892 -(*+*)then () else error "associate_input' Model_Pattern root-problem CHANGED";
17.893 -(* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
17.894 -(*+*)if (MethodC.from_store ctxt ["Biegelinien", "ausBelastung"] |> #model |> Model_Pattern.to_string @{context}) = "[\"" ^
17.895 - "(#Given, (Streckenlast, q__q))\", \"" ^
17.896 - "(#Given, (FunktionsVariable, v_v))\", \"" ^
17.897 - "(#Given, (Biegelinie, b_b))\", \"" ^
17.898 - "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^
17.899 - "(#Given, (Biegemoment, id_momentum))\", \"" ^
17.900 - "(#Given, (Querkraft, id_lat_force))\", \"" ^
17.901 - "(#Find, (Funktionen, fun_s))\"]"
17.902 -(*+*)then () else error "associate_input' Model_Pattern CHANGED";
17.903 -(*+*)if UnparseC.term @{context} d = "Biegelinie" andalso UnparseC.terms @{context} ts = "[y]"
17.904 -(*+*) andalso UnparseC.terms @{context} ts' = "[y]"
17.905 -(*+*)then
17.906 -(*+*) (case (inter op = ts ts') of [Free ("y", _(*"real \<Rightarrow> real"*))] => ()
17.907 -(*+*) | _ => error "check within associate_input' CHANGED 1")
17.908 -(*+*)else error "check within associate_input' CHANGED 2";
17.909 -(*\------------------- check within associate_input' -------------------------------/*)
17.910 -
17.911 -(*|------------------- contine me_Specify_Method_ausBelastung --------------------------------*)
17.912 -(*\------------------- step into me_Specify_Method_ausBelastung ----------------------------//*)
17.913 -(*[1], Met*)val (p,_,f,nxt,_,pt) = return_me_Specify_Method_ausBelastung;
17.914 - val Add_Given "Biegelinie y" = nxt
17.915 -
17.916 -(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy"= nxt
17.917 -(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Biegemoment M_b" = nxt
17.918 -(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Querkraft Q" = nxt
17.919 -(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["Biegelinien", "ausBelastung"] = nxt
17.920 -
17.921 -(*[1, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("sym_neg_equal_iff_equal", _)= nxt
17.922 -(*[1, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("Belastung_Querkraft", _)= nxt
17.923 -(*[1, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["named", "integrate", "function"])= nxt
17.924 -(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Model_Problem= nxt
17.925 -(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Given "functionTerm (- q_0)"= nxt
17.926 -(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Given "integrateBy x"= nxt
17.927 -;
17.928 -(*/------------------- check result of Add_Given "functionTerm (- q_0)" --------------------\*)
17.929 -if p = ([1, 3], Pbl) andalso
17.930 - f = Test_Out.PpcKF (Test_Out.Problem [], {Find = [Incompl "antiDerivativeName"],
17.931 - Given = [Correct "functionTerm (- q_0)", Incompl "integrateBy"],
17.932 - Relate = [], Where = [], With = []})
17.933 -then
17.934 - (case nxt of Add_Given "integrateBy x" => () | _ => error "specify-phase: low level CHANGED 1")
17.935 -else error "specify-phase: low level CHANGED 2";
17.936 -(*\------------------- check result of Add_Given "functionTerm (- q_0)" --------------------/*)
17.937 -
17.938 -
17.939 -\<close>
17.940 ML_file "Specify/sub-problem.sml"
17.941 ML_file "Specify/step-specify.sml"
17.942
18.1 --- a/test/Tools/isac/Test_Isac_Short.thy Wed Sep 27 12:17:44 2023 +0200
18.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Oct 02 12:02:59 2023 +0200
18.3 @@ -167,8 +167,8 @@
18.4 val return_XXXXX = "XXXXX"
18.5 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
18.6 (*//------------------ step into XXXXX -----------------------------------------------------\\*)
18.7 -\<close> ML \<open> (*||----------- contine XXXXX ---------------------------------------------------------*)
18.8 -(*||------------------ contine XXXXX ---------------------------------------------------------*)
18.9 +\<close> ML \<open> (*||----------- contine-- XXXXX -------------------------------------------------------*)
18.10 +(*||------------------ contine-- XXXXX -------------------------------------------------------*)
18.11 (*\\------------------ step into XXXXX -----------------------------------------------------//*)
18.12 \<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)
18.13 val "XXXXX" = return_XXXXX;
19.1 --- a/test/Tools/isac/Test_Some.thy Wed Sep 27 12:17:44 2023 +0200
19.2 +++ b/test/Tools/isac/Test_Some.thy Mon Oct 02 12:02:59 2023 +0200
19.3 @@ -85,8 +85,8 @@
19.4 val return_XXXXX = "XXXXX"
19.5 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
19.6 (*//------------------ step into XXXXX -----------------------------------------------------\\*)
19.7 -\<close> ML \<open> (*||----------- contine XXXXX ---------------------------------------------------------*)
19.8 -(*||------------------ contine XXXXX ---------------------------------------------------------*)
19.9 +\<close> ML \<open> (*||----------- contine-- XXXXX -------------------------------------------------------*)
19.10 +(*||------------------ contine-- XXXXX -------------------------------------------------------*)
19.11 (*\\------------------ step into XXXXX -----------------------------------------------------//*)
19.12 \<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)
19.13 val "XXXXX" = return_XXXXX;
19.14 @@ -109,11 +109,277 @@
19.15 \<close> ML \<open>
19.16 \<close>
19.17
19.18 -(** )ML_file "Knowledge/biegelinie-4.sml" ( ** )check file with test under repair below( **)
19.19 +(**)ML_file "MathEngine/step.sml" (** )check file with test under repair below( **)
19.20 section \<open>===================================================================================\<close>
19.21 section \<open>===== ============================================================================\<close>
19.22 ML \<open>
19.23 \<close> ML \<open>
19.24 +\<close> ML \<open>
19.25 +\<close> ML \<open>
19.26 +"--------- embed fun Step.inconsistent -------------------";
19.27 +"--------- embed fun Step.inconsistent -------------------";
19.28 +"--------- embed fun Step.inconsistent -------------------";
19.29 +States.reset ();
19.30 +CalcTree @{context}
19.31 +[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
19.32 + ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
19.33 +Iterator 1;
19.34 +moveActiveRoot 1;
19.35 +\<close> ML \<open>
19.36 + val ppp = States.get_pos 1 1
19.37 +\<close> ML \<open>
19.38 + val previous_pos as ([], Pbl) = ppp(*+*)
19.39 + val previous_calc = States.get_calc 1(*+*)
19.40 +\<close> ML \<open>
19.41 +
19.42 + autoCalculate 1 CompleteCalcHead;
19.43 +\<close> ML \<open> (*/------------ step into autoCalculate \<longrightarrow> ([], Met) -------------------------------\\*)
19.44 +(*/------------------- step into autoCalculate \<longrightarrow> ([], Met) -------------------------------\\*)
19.45 +"~~~~~ fun autoCalculate , args:"; val (cI, auto) = (1, CompleteCalcHead);
19.46 +\<close> ML \<open>
19.47 + val pold as ([], Pbl) = previous_pos (*..States.get_pos cI 1 ..AFTER RUNNING autoCalculate !!!*)
19.48 + val calc = previous_calc (*..States.get_pos cI 1 ..AFTER RUNNING autoCalculate !!!*)
19.49 +\<close> ML \<open>
19.50 + (*case*)
19.51 +Math_Engine.autocalc [] pold calc auto (*of*);
19.52 +"~~~~~~ fun autocalc , args:"; val (c, (pos as (_, p_)), ((pt, _), _(*tacis could help 1x in solve*)), auto) =
19.53 + ([], pold, calc, auto);
19.54 +\<close> ML \<open>
19.55 +(*+*)val false = Solve.autoord auto > 3
19.56 +(*+*)val true = Ctree.just_created (pt, pos)
19.57 +val false =
19.58 + (*if*) Solve.autoord auto > 3 andalso Ctree.just_created (pt, pos) (*else*);
19.59 +\<close> ML \<open>
19.60 +
19.61 +val true =
19.62 + (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*then*);
19.63 +\<close> ML \<open>
19.64 +(*isa*) val false =(**)
19.65 +(*isa2* )val true =( **)
19.66 + (*if*) not (
19.67 +SpecificationC.is_complete (pt, pos)) (*else*);
19.68 +\<close> ML \<open>
19.69 +(*isa*)
19.70 +"~~~~~~~~~ fun is_complete , args:"; val (pt, pos as (p, p_)) = (pt, pos);
19.71 + val (itms, oris, probl, o_spec, spec, ctxt) = case get_obj I pt p of
19.72 + PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ctxt, ...}
19.73 + => (itms, oris, probl, o_spec, spec, ctxt)
19.74 + | _ => raise ERROR "SpecificationC.is_complete only with PblObj"
19.75 + val (_, pbl_id, met_id) = References.select_input o_spec spec
19.76 +\<close> ML \<open>
19.77 +val return_is_complete = I_Model.s_are_complete ctxt oris
19.78 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_id, met_id)
19.79 +\<close> ML \<open>(*GOON*)
19.80 +(*+*)val [] = probl
19.81 +(*+*)val [] = itms
19.82 +\<close> ML \<open>
19.83 +\<close> ML \<open>
19.84 +\<close> ML \<open>
19.85 +\<close> ML \<open>
19.86 +\<close> ML \<open>
19.87 +\<close> ML \<open>
19.88 +\<close> ML \<open>
19.89 +val true =
19.90 + (*if*) not (References.are_complete (pt, pos)) (*then*);
19.91 +\<close> ML \<open>
19.92 + val ptp = References.complete (pt, pos)
19.93 +\<close> ML \<open>
19.94 +val true =
19.95 + (*if*) Solve.autoord auto = 3 (*then*);
19.96 +\<close> ML \<open>
19.97 +val return_autocalc = ("ok", c, ptp)
19.98 +\<close> ML \<open>
19.99 +(*+isa*)val (_, ([], Pbl)) = ptp(*+*)
19.100 +\<close> ML \<open>
19.101 +\<close> ML \<open>
19.102 +\<close> ML \<open>
19.103 +\<close> ML \<open>
19.104 +\<close> ML \<open>
19.105 +\<close> ML \<open>
19.106 +\<close> ML \<open>
19.107 +(*+isa*)val ([], Pbl) = pold(*+*)
19.108 +(*+isa2* )val ([], Pbl) = pold( *+*)
19.109 +\<close> ML \<open>
19.110 +(*\------------------- step into autoCalculate \<longrightarrow> ([], Met) -------------------------------//*)
19.111 +\<close> ML \<open> (*\------------ step into autoCalculate \<longrightarrow> ([], Met) -------------------------------//*)
19.112 +
19.113 +autoCalculate 1 (Steps 1);
19.114 +autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))*)
19.115 +;
19.116 + @{term "d_d x (x \<up> 2) + cos (4 * x \<up> 3)" }
19.117 +;
19.118 +\<close> ML \<open>
19.119 + appendFormula 1 "d_d x (x \<up> 2) + cos (4 * x \<up> 3)"; (*ERROR with chain rule*)
19.120 +(*ERROR
19.121 +CAS_Cmd "(+)" missing in theory "Test_Isac_Short" (and ancestors).
19.122 +val it = <SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 17: lev_back': called by ([],_)</ERROR></SYSERROR>: XML.tree*)
19.123 +(*/------------------- step into appendFormula ---------------------------------------------\\*)
19.124 +"~~~~~ fun appendFormula , args:"; val (cI, ifo) = (1, "d_d x (x \<up> 2) + cos (4 * x \<up> 3)");
19.125 +\<close> ML \<open>
19.126 + appendFormula' cI ifo;
19.127 +(*ERROR
19.128 +CAS_Cmd "(+)" missing in theory "Test_Isac_Short" (and ancestors).
19.129 +val it = <SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 17: lev_back': called by ([],_)</ERROR></SYSERROR>: XML.tree*)
19.130 +"~~~~~ fun appendFormula' , args:"; val (cI, ifo) = (cI, ifo);
19.131 +\<close> ML \<open>
19.132 + val cs = States.get_calc cI
19.133 + val pos = States.get_pos cI 1
19.134 +\<close> ML \<open>
19.135 +(*val ("ok", (_, _, ptp)) = (*case*)*)
19.136 +val return_do_next =
19.137 + Step.do_next pos cs (*of*);
19.138 +(*+isa*)val ([], Pbl) = pos(*+*)
19.139 +(*+isa2* )val ([1], Res) = pos( *+*)
19.140 +\<close> ML \<open>
19.141 +\<close> ML \<open> (*//----------- step into do_next ---------------------------------------------------\\*)
19.142 +(*//------------------ step into do_next ---------------------------------------------------\\*)
19.143 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (pos, cs);
19.144 +\<close> ML \<open>
19.145 + (*if*) Pos.on_calc_end ip (*else*);
19.146 + val (_, probl_id, _) = Calc.references (pt, p);
19.147 +\<close> ML \<open>
19.148 +val _ =
19.149 + (*case*) tacis (*of*);
19.150 + (*if*) probl_id = Problem.id_empty (*else*);
19.151 +\<close> ML \<open>
19.152 + switch_specify_solve p_ (pt, ip);
19.153 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
19.154 +\<close> ML \<open>
19.155 +(*+isa*)val true =(*+*)
19.156 +(*+isa2* )val false =( *+*)
19.157 + (*if*) Pos.on_specification ([(*or some other int list*)], state_pos) (*then*);
19.158 +\<close> ML \<open>
19.159 +\<close> ML \<open>
19.160 +\<close> ML \<open>
19.161 +\<close> ML \<open>
19.162 +\<close> ML \<open>
19.163 +\<close> ML \<open> (*||----------- contine-- do_next -----------------------------------------------------*)
19.164 +(*||------------------ contine-- do_next -----------------------------------------------------*)
19.165 +(*\\------------------ step into do_next ---------------------------------------------------//*)
19.166 +\<close> ML \<open> (*\\----------- step into do_next ---------------------------------------------------//*)
19.167 +val ("ok", (_, _, ptp)) = return_do_next;
19.168 +"~~~~~ fun do_next , args:"; val () = ();
19.169 +\<close> text \<open>
19.170 + (*case*)
19.171 +Step_Solve.by_term ptp (encode ifo) (*of*);
19.172 +(*ERROR
19.173 +CAS_Cmd "(+)" missing in theory "Test_Isac_Short" (and ancestors).
19.174 +lev_back': called by ([],_)*)
19.175 +\<close> ML \<open>
19.176 +"~~~~~ fun by_term , args:"; val ((pt, pos as (p, _)), istr) = (ptp, (encode ifo));
19.177 +\<close> ML \<open>
19.178 + val f_in = Syntax.read_term (Ctree.get_ctxt pt pos) istr
19.179 + handle ERROR msg => error (msg (*^ Position.here pp*))
19.180 + val pos_pred = lev_back(*'*) pos
19.181 + val f_pred = Ctree.get_curr_formula (pt, pos_pred);
19.182 + val f_succ = Ctree.get_curr_formula (pt, pos);
19.183 +\<close> ML \<open>
19.184 + (*if*) f_succ = f_in (*else*);
19.185 +\<close> ML \<open>
19.186 +val NONE =
19.187 + (*case*) CAS_Cmd.input f_in (*of*);
19.188 +(*ERROR CAS_Cmd "(+)" missing in theory "Test_Isac_Short" (and ancestors). *)
19.189 +\<close> text \<open>
19.190 + (*case*)
19.191 + LI.locate_input_term (pt, pos) f_in (*of*);
19.192 +(*ERROR lev_back': called by ([],_)*)
19.193 +\<close> ML \<open>
19.194 +"~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
19.195 +\<close> text \<open>
19.196 + val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
19.197 +(*ERROR lev_back': called by ([],_)*)
19.198 +\<close> ML \<open>
19.199 +(*+isa*)val ([], Pbl) = pos(*+*)
19.200 +(*+isa2* )val ([2], Res) = pos( *+*)
19.201 +\<close> ML \<open>
19.202 +\<close> ML \<open>
19.203 +\<close> ML \<open>
19.204 +\<close> ML \<open>
19.205 +\<close> ML \<open>
19.206 +\<close> ML \<open>
19.207 +\<close> ML \<open>
19.208 +\<close> ML \<open>
19.209 +\<close> ML \<open>
19.210 +\<close> ML \<open>
19.211 +\<close> ML \<open>
19.212 +
19.213 +\<close> text \<open> (*ERROR lev_back': called by ([],_)*)
19.214 + (*case*)
19.215 +Step_Solve.by_term ptp (encode ifo) (*of*); (*WAS ERROR: Inner syntax error \n Failed to parse term*)
19.216 +(*\------------------- step into appendFormula ---------------------------------------------//*)
19.217 +
19.218 +(* the check for errpat is maximally liberal (whole term modulo "rew_rls" from "type met"),
19.219 + would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
19.220 + results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
19.221 + instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
19.222 +(*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
19.223 +*)
19.224 +\<close> ML \<open>
19.225 +findFillpatterns 1 "chain-rule-diff-both";
19.226 +(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =
19.227 + d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
19.228 +\<close> ML \<open>
19.229 +"~~~~~ fun requestFillformula, args:"; val (cI, (errpatID, fillpatID)) =
19.230 + (1, ("chain-rule-diff-both", "fill-both-args"));
19.231 + val ((pt, _), _) = States.get_calc cI
19.232 + val pos as (p, _) = States.get_pos cI 1;
19.233 +\<close> text \<open> (*ERROR Step.inconsistent changed 1*)
19.234 + val fillforms = Error_Pattern.find_fill_patterns (pt, pos) errpatID;
19.235 +
19.236 +if pos = ([1], Res) then () else error "Step.inconsistent changed 1";
19.237 +
19.238 + val (_, fillform, thm, sube_opt) :: _ = filter ((curry op = fillpatID) o
19.239 + (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms;
19.240 +
19.241 +"~~~~~ fun Step.inconsistent, args:";
19.242 + val ((subs_opt, thm'), f', (is, ctxt), pos, pt) =
19.243 + ((sube_opt, thm'_of_thm thm), fillform, (get_loc pt pos), pos, pt);
19.244 +
19.245 + val f = get_curr_formula (pt, pos);
19.246 + val pos' as (p', _) = (lev_on p, Res);
19.247 +
19.248 +if pos = ([1], Res) then () else error "Step.inconsistent changed 2a";
19.249 +if UnparseC.term @ {context} f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))"
19.250 + then () else error "Step.inconsistent changed 2b";
19.251 +
19.252 + val (pt,c) =
19.253 + case subs_opt of
19.254 + NONE => cappend_atomic pt p' (is, ContextC.insert_assumptions [] ctxt) f
19.255 + (Rewrite thm') (f', []) Inconsistent
19.256 + | SOME subs => cappend_atomic pt p' (is, ContextC.insert_assumptions [] ctxt) f
19.257 + (Rewrite_Inst (subs, thm')) (f', []) Inconsistent
19.258 + val pt = update_branch pt p' TransitiveB;
19.259 +
19.260 +if get_obj g_tac pt p' = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", ""))
19.261 + andalso pos = ([1], Res) andalso pos' = ([2], Res) andalso p' = [2]
19.262 +then () else error "Step.inconsistent changed 3";
19.263 +
19.264 +"~~~~~ to requestFillformula return val:"; val (pt, pos') = (pt, pos');
19.265 +(*val (pt, pos') = Step.inconsistent (sube_opt, thm'_of_thm thm)
19.266 + (fillform, []) (get_loc pt pos) pos' pt*)
19.267 +States.upd_calc cI ((pt, pos'), []); States.upd_ipos cI 1 pos';
19.268 +
19.269 +"~~~~~ final check:";
19.270 +val ((pt, _),_) = States.get_calc 1;
19.271 +val p = States.get_pos 1 1;
19.272 +val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
19.273 +if p = ([2], Res) andalso
19.274 + get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", "")) andalso
19.275 + UnparseC.term @ {context} f =
19.276 + "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos ?u * d_d x ?_dummy_2"
19.277 + (*WAS with old findFillpatterns:
19.278 + "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos ?_dummy_2 * d_d x ?_dummy_3"
19.279 + WN120731 replaced
19.280 + "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos ?u * d_d x ?_dummy_2"
19.281 + WN120804 replaced
19.282 + "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos ?_dummy_1 * d_d x ?_dummy_2"*)
19.283 +then () else error "Step.inconsistent changed: fill-formula?";
19.284 +
19.285 +Test_Tool.show_pt pt; (*ATTENTION: omits the last step, if pt is incomplete, ([2], Res) EXISTS !*)
19.286 +============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
19.287 +
19.288 +
19.289 +\<close> ML \<open>
19.290
19.291 \<close> ML \<open>
19.292 \<close>