1.1 --- a/TODO.md Fri Aug 04 23:07:04 2023 +0200
1.2 +++ b/TODO.md Tue Aug 15 12:22:49 2023 +0200
1.3 @@ -52,6 +52,8 @@
1.4
1.5 ***** priority of WN items is top down, most urgent/simple on top
1.6
1.7 +* WN: ---broken elementwise input to lists---
1.8 +* WN: undetected ERROR in autoCalculate --- due to Post_Conds.check? (_OLD .. dispels ?)
1.9 * WN: "review (descriptor, ts)"; ts : term list, because this supports element-wise input of lists.
1.10 ts = [_] is determined by <Model_Pattern.is_list_descr descriptor>.
1.11 Thus, as long (descriptor, ts) is together, ts never contains <Const ("List.list.Cons", _)> --
2.1 --- a/src/Tools/isac/BaseDefinitions/store.sml Fri Aug 04 23:07:04 2023 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/store.sml Tue Aug 15 12:22:49 2023 +0200
2.3 @@ -19,6 +19,10 @@
2.4
2.5 val update: key -> string list -> 'a -> 'a T -> 'a T
2.6 val apply: 'a T -> ('a node -> 'b) -> key -> (*rev*)key -> 'b
2.7 +
2.8 +(*from isac_test for Minisubpbl*)
2.9 + val get_node: string list -> string list -> 'a T -> 'a node
2.10 +
2.11 end
2.12
2.13 (**)
2.14 @@ -113,4 +117,37 @@
2.15 else (py :: (update ID (i :: is) data pyss))
2.16 | update _ _ _ _ = raise ERROR "update called with undef pattern.";
2.17
2.18 +fun get_node(*1*) _ revkey [] = raise ERROR ("Store.get_node []: not found: " ^ strs2str revkey)
2.19 + | get_node(*2*) (key as (k1 :: _)) revkey ((node as Node (key', _, [])) :: ns) = (*spec.case same l.*)
2.20 +(writeln ("get_node 2 " ^ key');
2.21 + if k1 = key' then node
2.22 + else get_node key revkey ns (*continue on same level*)
2.23 +)
2.24 + | get_node(*3*) [k1] revkey ((node as Node (key', _, bs)) :: ns) =
2.25 +(writeln ("get_node 3 " ^ key');
2.26 + if k1 = key' then node
2.27 + else get_node [k1] revkey ns
2.28 +)
2.29 + | get_node(*4*) (key as (k1 :: ks)) revkey (Node (key', _, bs) :: ns) =
2.30 +(writeln ("get_node 4 " ^ key');
2.31 + if k1 = key'
2.32 + then get_node_down ks revkey bs
2.33 + else get_node key revkey ns
2.34 +)
2.35 + | get_node(*5*) _ revkey _ =
2.36 + raise ERROR ("Store.get_node: probably more than one node element for " ^ strs2str revkey)
2.37 +and get_node_down(*6*) [k1] revkey ((node as Node (key', _, _)) :: ns) = (*base case go down*)
2.38 +(writeln ("get_node_down 6 " ^ key');
2.39 + if k1 = key' then node
2.40 + else get_node [k1] revkey ns
2.41 +)
2.42 + | get_node_down(*7*) (key as (k1 :: ks)) revkey (Node (key', _, bs) :: ns) =
2.43 +(writeln ("get_node_down 7 " ^ key');
2.44 + if k1 = key'
2.45 + then get_node_down ks revkey bs
2.46 + else get_node key revkey ns
2.47 +)
2.48 + | get_node_down(*8*) _ revkey _ =
2.49 + raise ERROR ("Store.get_node: probably more than one node element for " ^ strs2str revkey)
2.50 +
2.51 (**)end(**)
3.1 --- a/src/Tools/isac/Build_Isac.thy Fri Aug 04 23:07:04 2023 +0200
3.2 +++ b/src/Tools/isac/Build_Isac.thy Tue Aug 15 12:22:49 2023 +0200
3.3 @@ -188,9 +188,7 @@
3.4 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/100-init-rootpbl.sml"
3.5 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml"
3.6 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150-add-given-Equation.sml"
3.7 -(**)
3.8 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml"
3.9 -(**)
3.10 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/200-start-method.sml"
3.11 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method-NEXT_STEP.sml"
3.12 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml"
4.1 --- a/src/Tools/isac/MathEngine/me-misc.sml Fri Aug 04 23:07:04 2023 +0200
4.2 +++ b/src/Tools/isac/MathEngine/me-misc.sml Tue Aug 15 12:22:49 2023 +0200
4.3 @@ -21,6 +21,7 @@
4.4 struct
4.5 (**)
4.6
4.7 +(*T_TESTold* )
4.8 fun pt_model (Ctree.PblObj {meth, spec, origin = (_, spec', hdl), ctxt, ...}) Pos.Met =
4.9 let
4.10 val (_, _, metID) = Ctree.get_somespec' spec spec'
4.11 @@ -34,6 +35,22 @@
4.12 in
4.13 Ctree.ModSpec (allcorrect, Pos.Met, hdl, meth, where_, spec)
4.14 end
4.15 +( *T_TEST**)
4.16 +fun pt_model (Ctree.PblObj {meth, spec, origin = (_, spec', hdl), ctxt, ...}) Pos.Met =
4.17 + let
4.18 + val (_, _, metID) = Ctree.get_somespec' spec spec'
4.19 + val where_ = if metID = MethodC.id_empty then []
4.20 + else
4.21 + let
4.22 + val {where_rls, where_, model, ...} = MethodC.from_store ctxt metID
4.23 + val (_, where_) = Pre_Conds.check_OLD ctxt where_rls where_
4.24 + (model, I_Model.OLD_to_TEST meth)
4.25 + in where_ end
4.26 + val allcorrect = I_Model.is_complete meth andalso foldl and_ (true, (map #1 where_))
4.27 + in
4.28 + Ctree.ModSpec (allcorrect, Pos.Met, hdl, meth, where_, spec)
4.29 + end
4.30 +(*T_TESTnew*)
4.31 (*T_TESTold* )
4.32 | pt_model (Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}) _(*Frm,Pbl*) =
4.33 let
5.1 --- a/src/Tools/isac/Specify/cas-command.sml Fri Aug 04 23:07:04 2023 +0200
5.2 +++ b/src/Tools/isac/Specify/cas-command.sml Tue Aug 15 12:22:49 2023 +0200
5.3 @@ -41,6 +41,7 @@
5.4 fun is_from (hdf : TermC.as_string) ((fmz_, spec) : Formalise.T) =
5.5 hdf <> "" andalso fmz_ = [] andalso spec = References.empty
5.6
5.7 +(*T_TESTold* )
5.8 fun input_ ((dI, pI, mI): References.T) dtss = (*WN110515 reconsider thy..ctxt*)
5.9 let
5.10 val thy = Know_Store.get_via_last_thy dI
5.11 @@ -63,6 +64,30 @@
5.12 val (_, where_) = Pre_Conds.check ctxt where_rls where_ mits 0
5.13 val ctxt = Proof_Context.init_global thy
5.14 in (pI, pits, mI, mits, where_, ctxt) end;
5.15 +( *T_TEST**)
5.16 +fun input_ ((dI, pI, mI): References.T) dtss = (*WN110515 reconsider thy..ctxt*)
5.17 + let
5.18 + val thy = Know_Store.get_via_last_thy dI
5.19 + val ctxt = Proof_Context.init_global thy
5.20 + val {model, ...} = Problem.from_store ctxt pI
5.21 + val its_ = map (dtss2itm_ model) dtss (*([1],true,"#Given",Cor (...))*)
5.22 + val its = O_Model.add_enumerate its_
5.23 + val pits = map flattup2 its
5.24 + val (pI, mI) =
5.25 + if mI <> ["no_met"]
5.26 + then (pI, mI)
5.27 + else
5.28 + case Refine.problem thy pI pits of
5.29 + SOME (pI, _) => (pI, (hd o #solve_mets o Problem.from_store ctxt) pI)
5.30 + | NONE => (pI, (hd o #solve_mets o Problem.from_store ctxt) pI)
5.31 + val {model, where_, where_rls, ...} = MethodC.from_store ctxt mI
5.32 + val its_ = map (dtss2itm_ model) dtss (*([1],true,"#Given",Cor (...))*)
5.33 + val its = O_Model.add_enumerate its_
5.34 + val mits = map flattup2 its
5.35 + val (_, where_) = Pre_Conds.check_OLD ctxt where_rls where_ (model, I_Model.OLD_to_TEST mits)
5.36 + val ctxt = Proof_Context.init_global thy
5.37 + in (pI, pits, mI, mits, where_, ctxt) end;
5.38 +(*T_TESTnew*)
5.39
5.40 (* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *)
5.41 fun input hdt =
6.1 --- a/src/Tools/isac/Specify/i-model.sml Fri Aug 04 23:07:04 2023 +0200
6.2 +++ b/src/Tools/isac/Specify/i-model.sml Tue Aug 15 12:22:49 2023 +0200
6.3 @@ -73,7 +73,7 @@
6.4 (*T_TESTold* )
6.5 val of_max_variant: Model_Pattern.T -> T_TEST -> T_TEST * Pre_Conds.env_subst * Pre_Conds.env_eval
6.6 ( *T_TEST*)
6.7 - val of_max_variant:Model_Pattern.T -> Model_Def.i_model_TEST ->
6.8 + val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->
6.9 Model_Def.i_model_TEST * Env.T * (Pre_Conds.env_subst * Pre_Conds.env_eval)
6.10 (*T_TESTnew*)
6.11
7.1 --- a/src/Tools/isac/Specify/m-match.sml Fri Aug 04 23:07:04 2023 +0200
7.2 +++ b/src/Tools/isac/Specify/m-match.sml Tue Aug 15 12:22:49 2023 +0200
7.3 @@ -33,6 +33,10 @@
7.4 datatype match' = (* constructors for tests only *)
7.5 Matches' of P_Model.T | NoMatch' of P_Model.T
7.6 val match_pbl : Formalise.model -> Problem.T -> match'
7.7 +
7.8 +(*from isac_test for Minisubpbl*)
7.9 + val chk1_: Model_Pattern.T -> O_Model.single -> I_Model.T
7.10 +
7.11 \<^isac_test>\<open>
7.12 (*val matc: theory -> Model_Pattern.T -> term list -> O_Model.T -> O_Model.T*)
7.13 val matc: theory -> Model_Pattern.T -> term list -> O_Model.T -> O_Model.T
7.14 @@ -81,6 +85,7 @@
7.15
7.16 (* check a problem (ie. ori list) for matching a problemtype,
7.17 takes the I_Model.variables for concluding completeness (FIXME could be another!) *)
7.18 +(*T_TESTold* )
7.19 fun match_oris ctxt where_rls oris (pbt, where_) =
7.20 let
7.21 val itms = (flat o (map (chk1_ pbt))) oris;
7.22 @@ -88,9 +93,20 @@
7.23 val complete = chk1_mis mvat itms pbt;
7.24 val (pb, _(*where_'*)) = Pre_Conds.check ctxt where_rls where_ itms mvat;
7.25 in if complete andalso pb then true else false end;
7.26 +( *T_TEST**)
7.27 +fun match_oris ctxt where_rls o_model (model_pattern, where_) =
7.28 + let
7.29 + val i_model = (flat o (map (chk1_ model_pattern))) o_model;
7.30 + val mvat = I_Model.variables i_model;
7.31 + val complete = chk1_mis mvat i_model model_pattern;
7.32 + val (pb, _(*where_'*)) = Pre_Conds.check_OLD ctxt where_rls where_
7.33 + (model_pattern, I_Model.OLD_to_TEST i_model);
7.34 + in if complete andalso pb then true else false end;
7.35 +(*T_TESTnew*)
7.36
7.37 (* check a problem (ie. ori list) for matching a problemtype,
7.38 returns items for output to math-experts *)
7.39 +(*T_TESTold* )
7.40 fun match_oris' thy oris (model, where_, where_rls) =
7.41 let
7.42 val itms = (flat o (map (chk1_ model))) oris;
7.43 @@ -99,6 +115,16 @@
7.44 val miss = chk1_mis' oris model;
7.45 val (pb, where_') = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_ itms mvat;
7.46 in (miss = [] andalso pb, (itms @ miss @ sups, where_')) end;
7.47 +( *T_TEST**)
7.48 +fun match_oris' thy o_model (model, where_, where_rls) =
7.49 + let
7.50 + val i_model = (flat o (map (chk1_ model))) o_model;
7.51 + val sups = ((map ori2itmSup) o (filter (field_eq "#undef"))) o_model;
7.52 + val miss = chk1_mis' o_model model;
7.53 + val (pb, where_') = Pre_Conds.check_OLD (Proof_Context.init_global thy) where_rls where_
7.54 + (model, I_Model.OLD_to_TEST i_model);
7.55 + in (miss = [] andalso pb, (i_model @ miss @ sups, where_')) end;
7.56 +(*T_TESTnew*)
7.57
7.58
7.59 (** check a problem (ie. itm list) for matching a problemtype **)
7.60 @@ -112,6 +138,7 @@
7.61 (2) filter (dsc(pbt) = dsc(oris)) oris; -> news;
7.62 (3) newitms = filter (mv mem vat(news)) news
7.63 (4) pbt @ newitms *)
7.64 +(*T_TESTold* )
7.65 fun match_itms_oris ctxt pbl (pbt, where_, where_rls) oris =
7.66 let
7.67 (*0*)val mv = Pre_Conds.max_variant pbl;
7.68 @@ -130,6 +157,27 @@
7.69 (*4*)val itms' = pbl @ newitms;
7.70 val (pb, where_') = Pre_Conds.check ctxt where_rls where_ itms' mv;
7.71 in (length mis = 0 andalso pb, (itms', where_')) end;
7.72 +( *T_TEST**)
7.73 +fun match_itms_oris ctxt pbl (pbt, where_, where_rls) oris =
7.74 + let
7.75 + (*0*)val mv = Pre_Conds.max_variant pbl;
7.76 +
7.77 + fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.descriptor itm_;
7.78 + fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
7.79 + SOME _ => false | NONE => true;
7.80 + (*1*)val mis = (filter (notmem pbl)) pbt;
7.81 +
7.82 + fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';
7.83 + fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));
7.84 + (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
7.85 + val news = (flat o (map (oris2itms oris))) mis;
7.86 + (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
7.87 + val newitms = filter mem_vat news;
7.88 + (*4*)val itms' = pbl @ newitms;
7.89 + val (pb, where_') = Pre_Conds.check_OLD ctxt where_rls where_
7.90 + (pbt, I_Model.OLD_to_TEST itms');
7.91 + in (length mis = 0 andalso pb, (itms', where_')) end;
7.92 +(*T_TESTnew*)
7.93
7.94
7.95 (** for use by math-authors **)
8.1 --- a/src/Tools/isac/Specify/p-spec.sml Fri Aug 04 23:07:04 2023 +0200
8.2 +++ b/src/Tools/isac/Specify/p-spec.sml Tue Aug 15 12:22:49 2023 +0200
8.3 @@ -198,17 +198,31 @@
8.4 in if pos_ = Pos.Pbl
8.5 then
8.6 let
8.7 +(*T_TESTold* )
8.8 val {where_rls, where_,...} = Problem.from_store ctxt
8.9 (#2 (References.select_input ospec spec))
8.10 val (_, where_) = Pre_Conds.check ctxt where_rls where_ pits 0
8.11 +( *T_TEST**)
8.12 + val {where_rls, where_, model, ...} = Problem.from_store ctxt
8.13 + (#2 (References.select_input ospec spec))
8.14 + val (_, where_) = Pre_Conds.check_OLD ctxt where_rls where_
8.15 + (model, I_Model.OLD_to_TEST pits)
8.16 +(*T_TESTnew*)
8.17 in (Ctree.update_pbl pt p pits,
8.18 (SpecificationC.is_complete' pits where_ spec, Pos.Pbl, hdf', pits, where_, spec))
8.19 end
8.20 else
8.21 let
8.22 +(*T_TESTold* )
8.23 val {where_rls,where_,...} = MethodC.from_store ctxt
8.24 (#3 (References.select_input ospec spec))
8.25 val (_, where_) = Pre_Conds.check ctxt where_rls where_ mits 0
8.26 +( *T_TEST**)
8.27 + val {where_rls,where_, model, ...} = MethodC.from_store ctxt
8.28 + (#3 (References.select_input ospec spec))
8.29 + val (_, where_) = Pre_Conds.check_OLD ctxt where_rls where_
8.30 + (model, I_Model.OLD_to_TEST mits)
8.31 +(*T_TESTnew*)
8.32 in (Ctree.update_met pt p mits,
8.33 (SpecificationC.is_complete' mits where_ spec, Pos.Met, hdf', mits, where_, spec))
8.34 end
9.1 --- a/src/Tools/isac/Specify/pre-conditions.sml Fri Aug 04 23:07:04 2023 +0200
9.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml Tue Aug 15 12:22:49 2023 +0200
9.3 @@ -53,11 +53,12 @@
9.4 val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->
9.5 Model_Def.i_model_TEST * env_subst * env_eval
9.6 ( *T_TEST*)
9.7 - val of_max_variant:Model_Pattern.T -> Model_Def.i_model_TEST ->
9.8 + val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->
9.9 Model_Def.i_model_TEST * Env.T * (env_subst * env_eval)
9.10 (*T_TESTnew*)
9.11
9.12 (*from isac_test for Minisubpbl*)
9.13 + val handle_lists: term -> Model_Def.descriptor * term list -> Env.T;
9.14 val discern_feedback_subst: Model_Def.descriptor -> Model_Def.i_model_feedback_TEST -> Env.T;
9.15 val discern_type_subst: term * term -> term list -> Env.T;
9.16 val discern_type_eval: Model_Def.descriptor -> term list -> env_eval
9.17 @@ -319,8 +320,15 @@
9.18 fold (curry and_) (map (fn t => TermC.is_atom t) ts) true
9.19 (* all_lhs_atoms: term list -> bool*)
9.20 fun all_lhs_atoms ts = fold (curry and_) (map (fn t =>
9.21 + if can TermC.lhs t andalso not (TermC.is_num (TermC.lhs t))
9.22 + then TermC.is_atom (TermC.lhs t)
9.23 + else false) ts) true
9.24 +(*T_TESTold* )
9.25 +fun all_lhs_atoms ts = fold (curry and_) (map (fn t =>
9.26 if can TermC.lhs t then TermC.is_atom (TermC.lhs t) else false) ts) true
9.27 +( *T_TEST*)
9.28 (* distinguish_atoms: term list -> Env.T*)
9.29 +(*T_TESTnew*)
9.30 fun distinguish_atoms (*[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2], \<epsilon> = 0.01, [L]*) ts =
9.31 if all_atoms ts
9.32 then map (rpair TermC.empty (*dummy rhs*)) ts
9.33 @@ -392,9 +400,6 @@
9.34 (* all_atoms: term list -> bool*)
9.35 fun all_atoms ts =
9.36 fold (curry and_) (map (fn t => TermC.is_atom t) ts) true
9.37 -(* all_lhs_atoms: term list -> bool*)
9.38 -fun all_lhs_atoms ts = fold (curry and_) (map (fn t =>
9.39 - if can TermC.lhs t then TermC.is_atom (TermC.lhs t) else false) ts) true
9.40 (* discern_atoms: term list -> (term * term) list*)
9.41 fun discern_atoms (*[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2], \<epsilon> = 0.01, [L]*) ts =
9.42 if all_atoms ts
9.43 @@ -507,14 +512,27 @@
9.44
9.45 (** of_max_variant **)
9.46
9.47 +(*T_TESTold* )
9.48 fun handle_lists id (descr, ts) =
9.49 - if Model_Pattern.is_list_descr descr
9.50 - then if length ts > 1 (*list with more than 1 element needs to collect by [.., .., ..]*)
9.51 - then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)] (*AdditValues [u, v]*)
9.52 - else if TermC.is_atom (Library.the_single ts)
9.53 - then [(id, Library.the_single ts)] (* solutions L, ...*)
9.54 - else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)](*Constants [r = 7]*)
9.55 - else [(id, Library.the_single ts)] (* solveFor x, Extremum (A = ...)*)
9.56 + if Model_Pattern.is_list_descr descr
9.57 + then if length ts > 1 (*list with more than 1 element needs to collect by [.., .., ..]*)
9.58 + then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)] (*AdditValues [u, v]*)
9.59 + else if TermC.is_atom (Library.the_single ts)
9.60 + then [(id, Library.the_single ts)] (* solutions L, ...*)
9.61 + else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)](*Constants [r = 7]*)
9.62 + else [(id, Library.the_single ts)] (* solveFor x, Extremum (A = ...)*)
9.63 +( *T_TEST***)
9.64 +fun handle_lists id (descr, ts) =
9.65 + if Model_Pattern.is_list_descr descr
9.66 + then if length ts > 1 (*list with more than 1 element needs to collect by [.., .., ..]*)
9.67 + then if TermC.is_list (hd ts) (*---broken elementwise input to lists---*)
9.68 + then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) (map TermC.the_single ts))]
9.69 + else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)] (*AdditValues [u, v]*)
9.70 + else if TermC.is_atom (Library.the_single ts)
9.71 + then [(id, Library.the_single ts)] (* solutions L, ...*)
9.72 + else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)](*Constants [r = 7]*)
9.73 + else [(id, Library.the_single ts)] (* solveFor x, Extremum (A = ...)*)
9.74 +(*T_TESTnew*)
9.75
9.76 fun mk_env_model _ (Model_Def.Cor_TEST ((_, []), _)) = []
9.77 | mk_env_model id (Model_Def.Cor_TEST ((descr, ts), _)) =
9.78 @@ -546,6 +564,7 @@
9.79 Free (id_string, ts |> hd |> TermC.lhs |> type_of)
9.80 | switch_type_TEST descr _ = raise ERROR ("switch_type_TEST undefined argument " ^
9.81 quote (UnparseC.term (ContextC.for_ERROR ()) descr))
9.82 +(*T_TESTold* )
9.83 fun discern_typ _ (_, []) = []
9.84 | discern_typ id (descr, ts) =
9.85 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
9.86 @@ -566,6 +585,31 @@
9.87 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
9.88 end
9.89 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)
9.90 +( *T_TEST*)
9.91 +fun discern_typ _ (_, []) = []
9.92 + | discern_typ id (descr, ts) =
9.93 +(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
9.94 + let
9.95 + val ts = if Model_Pattern.is_list_descr descr
9.96 + then if TermC.is_list (hd ts)
9.97 + then ts |> map TermC.isalist2list |> flat
9.98 + else ts
9.99 + else ts
9.100 + in
9.101 +(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)
9.102 + if Model_Pattern.typ_of_element descr = HOLogic.boolT andalso all_lhs_atoms ts
9.103 + then
9.104 + if length ts > 1
9.105 + then (writeln "model items of type 'bool' in lists with 'lengt ts > 1' NOT YET IMPLEMENTED";
9.106 + [])
9.107 + else [((switch_type_TEST id ts, TermC.lhs (hd ts)),
9.108 + (TermC.lhs (hd ts), TermC.rhs (hd ts)))]
9.109 + else []
9.110 +(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
9.111 + end
9.112 +(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)
9.113 +(*T_TESTnew*)
9.114 +
9.115 fun discern_feedback id (Model_Def.Cor_TEST ((descr, ts), _)) = discern_typ id (descr, ts)
9.116 | discern_feedback _ (Model_Def.Syn_TEST _) = [] (*TODO: handle correct elements*)
9.117 | discern_feedback id (Model_Def.Inc_TEST ((descr, ts), _)) = discern_typ id (descr, ts)
9.118 @@ -664,7 +708,7 @@
9.119
9.120 (* expects the precondition from Problem, ie. needs substitution by env_model*)
9.121 fun check_OLD _ _ [] _ = (true, [])
9.122 - | check_OLD ctxt where_rls pres (model_patt, i_model) =
9.123 + | check_OLD ctxt where_rls where_ (model_patt, i_model) =
9.124 let
9.125 (*T_TESTold* )
9.126 val (env_subst, env_eval) = sep_variants_envs_OLD model_patt i_model
9.127 @@ -676,7 +720,7 @@
9.128 end;
9.129 ( *T_TEST*)
9.130 val (_, env_model, (env_subst, env_eval)) = of_max_variant model_patt i_model
9.131 - val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
9.132 + val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
9.133 val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
9.134 val full_subst = if env_eval = [] then pres_subst_other
9.135 else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
10.1 --- a/src/Tools/isac/Specify/refine.sml Fri Aug 04 23:07:04 2023 +0200
10.2 +++ b/src/Tools/isac/Specify/refine.sml Tue Aug 15 12:22:49 2023 +0200
10.3 @@ -41,6 +41,11 @@
10.4 (**)
10.5 val refin'': theory -> Problem.id -> I_Model.T -> match_ list -> Problem.T Store.node -> match_ list
10.6
10.7 +(*from isac_test for Minisubpbl*)
10.8 + val app_ptyp: (Probl_Def.T Store.node -> 'a) -> Store.key -> Store.key -> 'a
10.9 +(*val refin: Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option*)
10.10 + val refin: Proof.context -> Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option
10.11 +
10.12 \<^isac_test>\<open>
10.13 (*val test : Formalise.model -> Problem.id -> M_Match.T list*)
10.14 (*val refine : Formalise.model -> Problem.id -> M_Match.T list*)
10.15 @@ -50,8 +55,6 @@
10.16 (**)
10.17 val refins'': theory -> Problem.id -> I_Model.T -> match_ list -> Problem.T Store.node list -> match_ list
10.18 (**)
10.19 -(*val refin: Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option*)
10.20 - val refin: Proof.context -> Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option
10.21 \<close>
10.22 end
10.23
10.24 @@ -121,6 +124,7 @@
10.25
10.26 (* check a problem (ie. itm list) for matching a problemtype,
10.27 takes the Pre_Conds.max_variant for concluding completeness (could be another!) *)
10.28 +(*T_TESTold* )
10.29 fun match_itms thy itms (pbt, where_, where_rls) =
10.30 let
10.31 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b;
10.32 @@ -131,6 +135,19 @@
10.33 val mis = chk_mis mvat itms'' untouched pbt;
10.34 val (pb, where_') = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_ itms'' mvat
10.35 in (length mis = 0 andalso pb, (itms'@ mis, where_')) end;
10.36 +( *T_TEST**)
10.37 +fun match_itms thy itms (pbt, where_, where_rls) =
10.38 + let
10.39 + fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b;
10.40 + val itms' = map (chk_ thy pbt) itms; (* all found are #3 true *)
10.41 + val mvat = Pre_Conds.max_variant itms';
10.42 + val itms'' = filter (okv mvat) itms';
10.43 + val untouched = filter eq0 itms; (* i.e. dsc only (from init)*)
10.44 + val mis = chk_mis mvat itms'' untouched pbt;
10.45 + val (pb, where_') = Pre_Conds.check_OLD (Proof_Context.init_global thy) where_rls where_
10.46 + (pbt, I_Model.OLD_to_TEST itms'')
10.47 + in (length mis = 0 andalso pb, (itms'@ mis, where_')) end;
10.48 +(*T_TESTnew*)
10.49
10.50 (* refine a problem; version for tactic Refine_Problem *)
10.51 fun refin'' _ (pblRD: Problem.id) itms pbls (Store.Node (pI, [py], [])) =
10.52 @@ -169,22 +186,23 @@
10.53 | SOME (Match_ (rfd as (pI', _))) => if pblID = pI' then NONE else SOME rfd;
10.54
10.55 (*
10.56 - refine a problem; construct pblRD while scanning
10.57 - val refin: Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option
10.58 + refine a problem; construct pblRD while scanning Problem.T Store.T
10.59 +TODO: as \<open>refin: 'a -> .. -> 'b option\<close> could be ignorant of Store.T structure.
10.60 *)
10.61 -(*val refin: Proof.context -> Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option*)
10.62 fun refin ctxt pblRD ori (Store.Node (pI, [py], [])) =
10.63 let
10.64 +val _ = writeln ("refin 1: " ^ strs2str pblRD)
10.65 val {where_rls, model, where_, ...} = py: Problem.T
10.66 val model = map (Model_Pattern.adapt_to_type ctxt) model
10.67 val where_ = map (ParseC.adapt_term_to_type ctxt) where_
10.68 in
10.69 if M_Match.match_oris ctxt where_rls ori (model, where_)
10.70 - then SOME (pblRD @ [pI])
10.71 + then SOME (pblRD(**) @ [pI](**))
10.72 else NONE
10.73 end
10.74 | refin ctxt pblRD ori (Store.Node (pI, [py], pys)) =
10.75 let
10.76 +val _ = writeln ("refin 2: " ^ strs2str pblRD)
10.77 val {where_rls, model, where_, ...} = py: Problem.T
10.78 val model = map (Model_Pattern.adapt_to_type ctxt) model
10.79 val where_ = map (ParseC.adapt_term_to_type ctxt) where_
10.80 @@ -192,18 +210,20 @@
10.81 if M_Match.match_oris ctxt where_rls ori (model, where_)
10.82 then (case refins ctxt (pblRD @ [pI]) ori pys of
10.83 SOME pblRD' => SOME pblRD'
10.84 - | NONE => SOME (pblRD @ [pI]))
10.85 + | NONE => SOME (pblRD (**)@ [pI](**)))
10.86 else NONE
10.87 end
10.88 | refin _ _ _ _ = raise ERROR "refin: uncovered fun def."
10.89 and refins _ _ _ [] = NONE
10.90 | refins ctxt pblRD ori ((p as Store.Node _) :: pts) =
10.91 +(writeln ("refins: " ^ strs2str pblRD);
10.92 (case refin ctxt pblRD ori p of
10.93 - SOME pblRD' => SOME pblRD'
10.94 - | NONE => refins ctxt pblRD ori pts);
10.95 + SOME pblRD' => SOME (pblRD')
10.96 + | NONE => refins ctxt pblRD ori pts)
10.97 +);
10.98
10.99 \<^isac_test>\<open>
10.100 -(* refine a problem; version providing output for math-experts *)
10.101 +(* refine a problem; version providing output for math authors *)
10.102 (*val refin': Proof.context -> Problem.id -> Formalise.model -> M_Match.T list ->
10.103 Probl_Def.T Store.node -> M_Match.T list*)
10.104 fun refin' ctxt pblRD fmz pbls (Store.Node (pI, [py: Probl_Def.T], [])) =
10.105 @@ -252,6 +272,7 @@
10.106 TODO: rename \<rightarrow> apply_to_node
10.107 apply a fun to a ptyps node.
10.108 val app_ptyp: (Probl_Def.T Store.node -> 'a) -> Store.key -> Store.key -> 'a
10.109 +TODO: Store.apply scans Store.T only to the first hit; see Store.apply.
10.110 *)
10.111 fun app_ptyp x = Store.apply (get_pbls ()) x;
10.112
11.1 --- a/src/Tools/isac/Specify/specification.sml Fri Aug 04 23:07:04 2023 +0200
11.2 +++ b/src/Tools/isac/Specify/specification.sml Tue Aug 15 12:22:49 2023 +0200
11.3 @@ -117,9 +117,16 @@
11.4 val (ospec, hdf', spec, probl, ctxt) = case Ctree.get_obj I pt p of
11.5 Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl, ctxt, ...} => (ospec, hdf', spec, probl, ctxt)
11.6 | _ => raise ERROR "get Pbl: uncovered case get_obj"
11.7 +(*T_TESTold* )
11.8 val {where_rls, where_, ...} =
11.9 Problem.from_store ctxt (#2 (References.select_input ospec spec))
11.10 val (_, where_) = Pre_Conds.check ctxt where_rls where_ probl 0
11.11 +( *T_TEST**)
11.12 + val {where_rls, where_, model, ...} =
11.13 + Problem.from_store ctxt (#2 (References.select_input ospec spec))
11.14 + val (_, where_) = Pre_Conds.check_OLD ctxt where_rls where_
11.15 + (model, I_Model.OLD_to_TEST probl)
11.16 +(*T_TESTnew*)
11.17 in
11.18 (is_complete' probl where_ spec, Pos.Pbl, hdf', probl, where_, spec)
11.19 end
11.20 @@ -128,8 +135,13 @@
11.21 val (ospec, hdf', spec, meth, ctxt) = case Ctree.get_obj I pt p of
11.22 Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ctxt, ...} => (ospec, hdf', spec, meth, ctxt)
11.23 | _ => raise ERROR "get Met: uncovered case get_obj"
11.24 - val {where_rls, where_, ...} = MethodC.from_store ctxt (#3 (References.select_input ospec spec))
11.25 - val (_, where_) = Pre_Conds.check ctxt where_rls where_ meth 0
11.26 +(*T_TESTold* )
11.27 +( *T_TEST**)
11.28 + val {where_rls, where_, model, ...} =
11.29 + MethodC.from_store ctxt (#3 (References.select_input ospec spec))
11.30 + val (_, where_) = Pre_Conds.check_OLD ctxt where_rls where_
11.31 + (model, I_Model.OLD_to_TEST meth)
11.32 +(*T_TESTnew*)
11.33 in
11.34 (is_complete' meth where_ spec, Pos.Met, hdf', meth, where_, spec)
11.35 end
12.1 --- a/test/Tools/isac/Interpret/li-tool.sml Fri Aug 04 23:07:04 2023 +0200
12.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Tue Aug 15 12:22:49 2023 +0200
12.3 @@ -1,4 +1,4 @@
12.4 -(* Title: test/../script.sml
12.5 +(* Title: Interpret/li-tool.sml
12.6 Author: Walther Neuper 050908
12.7 (c) copyright due to lincense terms.
12.8 *)
12.9 @@ -224,8 +224,8 @@
12.10 This test is deeply nested (down into details of creating environments).
12.11 In order to make Sidekick show the structure add to each
12.12 * (*/...\*) and (*\.../*)
12.13 - * a companion > ML < (*/...\*) and > ML < (*\.../*)
12.14 - Note the wrong^ ^delimiters.
12.15 + * a companion > ML < (*/...\*) and > ML < (*\.../*)
12.16 + Note the wrong ^----^ delimiters.
12.17 *)
12.18 val fmz = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
12.19 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
12.20 @@ -234,22 +234,29 @@
12.21 val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
12.22 ["IntegrierenUndKonstanteBestimmen2"]);
12.23 val p = e_pos'; val c = [];
12.24 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*)
12.25 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "Traegerlaenge L"*)
12.26 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "Streckenlast q_0"*)
12.27 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "Biegelinie y"*)
12.28 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))]; val Model_Problem = nxt
12.29 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Traegerlaenge L" = nxt
12.30 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Streckenlast q_0" = nxt
12.31 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Biegelinie y" = nxt
12.32 +(*/---broken elementwise input to lists---\* )
12.33 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)
12.34 + (*isa* ) val Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" = nxt
12.35 + ( *isa2*) val Add_Relation "Randbedingungen [y 0 = 0]" = nxt
12.36 (*[], 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]"*)
12.37 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Theory "Biegelinie"*)
12.38 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Problem ["Biegelinien"]*)
12.39 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*)
12.40 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)
12.41 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)
12.42 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "AbleitungBiegelinie dy"*)
12.43 + (*isa*) val Specify_Theory "Biegelinie" = nxt
12.44 + (*isa2* ) val Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]" = nxt( **)
12.45 +( *\---broken elementwise input to lists---/*)
12.46 +(*[], 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
12.47 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
12.48 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["Biegelinien"] = nxt
12.49 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
12.50 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "FunktionsVariable x" = nxt
12.51 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]" = nxt
12.52 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy" = nxt
12.53
12.54 (*[], Met*)val return_Add_Given_AbleitungBieg
12.55 - = me nxt p c pt; (*\<rightarrow>Apply_Method ["IntegrierenUndKonstanteBestimmen2"]*)
12.56 -(*+*)val Add_Given "AbleitungBiegelinie dy" = nxt; (*specify SUBproblem auf ([1], Pbl)*)
12.57 + = me nxt p c pt;
12.58 +(*/------------------- step into me_Add_Given_AbleitungBieg --------------------------------\\*)
12.59
12.60 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
12.61 val ctxt = Ctree.get_ctxt pt p
12.62 @@ -308,34 +315,34 @@
12.63
12.64 (*case*)
12.65 LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI (*of*);
12.66 -(*/------------------- step into init_pstate -----------------------------------------------\\*)
12.67 +(*//------------------ step into init_pstate -----------------------------------------------\\*)
12.68 "~~~~~ fun init_pstate , args:"; val (ctxt, i_model, met_id) = (ctxt, (I_Model.OLD_to_TEST itms), mI);
12.69 val (model_patt, program, prog, prog_rls, where_, where_rls) =
12.70 case MethodC.from_store ctxt met_id of
12.71 - {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...} =>
12.72 + {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...}=>
12.73 (model_patt, program, prog, prog_rls, where_, where_rls)
12.74
12.75 - val (_, env_subst, env_eval) =
12.76 - I_Model.of_max_variant model_patt i_model;
12.77 -(*//------------------ step into of_max_variant --------------------------------------------\\*)
12.78 + val return_of_max_variant =
12.79 + of_max_variant model_patt i_model;
12.80 +(*///----------------- step into of_max_variant --------------------------------------------\\*)
12.81 "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
12.82 val all_variants =
12.83 map (fn (_, variants, _, _, _) => variants) i_model
12.84 |> flat
12.85 |> distinct op =
12.86 - val variants_separated = map (Pre_Conds.filter_variants' i_model) all_variants
12.87 - val sums_corr = map (Pre_Conds.cnt_corrects) variants_separated
12.88 - val sum_variant_s = Pre_Conds.arrange_args1 sums_corr (1, all_variants)
12.89 + val variants_separated = map (filter_variants' i_model) all_variants
12.90 + val sums_corr = map (cnt_corrects) variants_separated
12.91 + val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
12.92 val (_, max_variant) = hd (*..crude decision, up to improvement *)
12.93 (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
12.94 val i_model_max =
12.95 filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
12.96 - val equal_descr_pairs =
12.97 - map (Pre_Conds.get_equal_descr i_model) model_patt
12.98 - |> flat;
12.99 + val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
12.100 +;
12.101 (*+*)if (equal_descr_pairs |> descr_pairs_to_string @{context}) = "[" ^
12.102 (*defined: in program+model--vvvv--,----------------------------------------- in problem ---vvv*)
12.103 "((#Given, (Traegerlaenge, l_l)), (1, [1], true ,#Given, " ^ "(Cor_TEST Traegerlaenge L ,(l_l, [L]), Position.T))), " ^
12.104 +(*-------------------------------------------------------------------------------------penv-^^^^^^^^^ DROP!*)
12.105 "((#Given, (Streckenlast, q_q)), (2, [1], true ,#Given, " ^
12.106 "(Cor_TEST Streckenlast q_0 ,(q_q, [q_0]), Position.T))), " ^
12.107 "((#Given, (FunktionsVariable, fun_var)), (5, [1], true ,#Given, " ^
12.108 @@ -345,197 +352,47 @@
12.109 "((#Given, (AbleitungBiegelinie, id_der)), (7, [1], true ,#Given, " ^
12.110 "(Cor_TEST AbleitungBiegelinie dy ,(id_der, [dy]), Position.T))), " ^
12.111 "((#Find, (Biegelinie, b_b)), (3, [1], true ,#Find, (Cor_TEST Biegelinie y ,(b_b, [y]), Position.T))), " ^
12.112 +(*-----------------------------------------------------------------------penv-^^^^^^^^^ DROP!*)
12.113 "((#Relate, (Randbedingungen, r_b)), (4, [1], true ,#Relate, " ^
12.114 "(Cor_TEST Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]), Position.T)))]"
12.115 +(*-----------------------------------------------------------------penv-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ DROP!*)
12.116 then () else error "of_max_variant: equal_descr_pairs CHANGED";
12.117
12.118 - val env_subst =
12.119 - mk_env_subst_DEL equal_descr_pairs;
12.120 -(*/------------------- ERRORs to remove in CS subsequent to "prepare 1 PIDE turn 11"-000----\* )
12.121 -(*+*)if ( env_subst |> Subst.to_string @{context}) = "[\"\n" ^
12.122 -(*ERRORs------^^^^^^^^^----------isa2: penv ---vvv----------------------..isa2, thus "correct"*)
12.123 -(*1*)"(l_l, L)\", \"\n" ^ (* (l_l, [L]) *)
12.124 -(*2*)"(q_q, q_0)\", \"\n" ^ (* (q_q, [q_0]) *)
12.125 -(*3*)"(fun_var, x)\", \"\n" ^ (* (fun_var, [x]) *)
12.126 -(*4*)"(vs, GleichungsVariablen)\", \"\n" ^ (* (vs, [[c, c_2, c_3, c_4]]) *)
12.127 -(*5*)"(id_der, dy)\", \"\n" ^ (* (id_der, [dy]) *)
12.128 -(*6*)"(b_b, y)\"]" (* (b_b, [y]) *)
12.129 -(*7 missing*) (* (r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]) *)
12.130 -(*+*)then () else error "of_max_variant: env_subst BETTER ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? "
12.131 -( *\------------------- ERRORs to remove ..--------------------------------------------------/*)
12.132 + val return_make_env_model = make_env_model equal_descr_pairs;
12.133 +(*////---------------- step into make_env_model --------------------------------------------\\*)
12.134 +"~~~~~ fun make_env_model , args:"; val (equal_descr_pairs) = (equal_descr_pairs);
12.135 +"~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 4 equal_descr_pairs;
12.136 +"~~~~~ fun mk_env_model , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) = (id, feedb);
12.137
12.138 -(*///----------------- step into mk_env_subst_DEL ------------------------------------------\\*)
12.139 -"~~~~~ fun mk_env_subst_DEL , args:"; val (equal_descr_pairs) = (equal_descr_pairs);
12.140 + handle_lists id (descr, ts);
12.141 +"~~~~~ fun handle_lists , args:"; val (id, (descr, ts)) = (id, (descr, ts));
12.142 +(*+*)val xxx = ts |> UnparseC.terms @{context};
12.143 + (*if*) Model_Pattern.is_list_descr descr (*then*);
12.144 + (*if*) length ts > 1 (*then*);
12.145 + (*if*) TermC.is_list (hd ts) (*then*);
12.146 +val return_handle_lists_step =
12.147 + [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) (map TermC.the_single ts))]
12.148 +(*+*)val "[\"\n(vs, [c, c_2, c_3, c_4])\"]"
12.149 + = return_handle_lists_step |> Subst.to_string @{context}
12.150 +(*\\\\---------------- step into make_env_model --------------------------------------------//*)
12.151 + val env_model = return_make_env_model
12.152 +(*+*)val "[\"\n(l_l, L)\", \"\n(q_q, q_0)\", \"\n(fun_var, x)\", \"\n(vs, [c, c_2, c_3, c_4])\", \"\n(id_der, dy)\", \"\n(b_b, y)\", \"\n(r_b, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\"]"
12.153 + = env_model |> Subst.to_string @{context}
12.154
12.155 -(*///################# nth 1 equal_descr_pairs ############################################=\\*)
12.156 - val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
12.157 - => (Pre_Conds.discern_feedback_subst id feedb) (*|> map fst (*rhs dropped*)|> map (pair id)*) ) (nth 1 equal_descr_pairs);
12.158 -"~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 1 equal_descr_pairs);
12.159 -(*--------------------------------------------------------------------------^^^----------------*)
12.160 +(*|||----------------- contine of_max_variant ------------------------------------------------*)
12.161 + val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
12.162 + val subst_eval_list = make_envs_preconds equal_givens
12.163 + val (env_subst, env_eval) = split_list subst_eval_list
12.164 +val return_of_max_variant_step = (i_model_max, env_model, (env_subst, env_eval));
12.165
12.166 - Pre_Conds.discern_feedback_subst id feedb;
12.167 -"~~~~~ fun discern_feedback_subst , args:"; val (id, Cor_TEST ((descr, [ts]), _)) = (id, feedb);
12.168 - (*if*) TermC.is_list ts (*else*);
12.169 - val ts = [ts]
12.170 -;
12.171 - Pre_Conds.discern_type_subst (descr, id) ts;
12.172 -"~~~~~ fun discern_type_subst , args:"; val ((descr, id), ts) = ((descr, id), ts);
12.173 -val _(*"real \<Rightarrow> una"*) =
12.174 - (*case*) type_of descr (*of*);
12.175 -val return_discern_type_subst_1 = [(id, Library.the_single ts)]
12.176 -(*\\\################# nth 1 equal_descr_pairs ############################################=//*)
12.177 -
12.178 -(*///################# nth 4 equal_descr_pairs ############################################=\\*)
12.179 - val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
12.180 - => (discern_feedback_subst id feedb) (*|> map fst (*rhs dropped*)|> map (pair id)*) ) (nth 1 equal_descr_pairs);
12.181 -"~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 4 equal_descr_pairs);
12.182 -(*--------------------------------------------------------------------------^^^----------------*)
12.183 -
12.184 - Pre_Conds.discern_feedback_subst id feedb;
12.185 -"~~~~~ fun discern_feedback_subst , args:"; val (id, Cor_TEST ((descr, (*[*)ts(*]*)), _)) = (id, feedb);
12.186 -(*+*)val (Free ("vs", _), "[[c], [c_2], [c_3], [c_4]]")
12.187 - = (id, ts |> UnparseC.terms @{context});
12.188 -
12.189 - (*if*) fold (curry and_) (map TermC.is_list ts) true (*then*);
12.190 - val ts = ts;
12.191 -
12.192 - discern_type_subst (descr, id) ts;
12.193 -"~~~~~ fun discern_type_subst , args:"; val ((descr, id), ts) = ((descr, id), ts);
12.194 -val (Type ("fun", [Type ("List.list", [Type ("Real.real", [])]), _])) =
12.195 - (*case*) type_of descr (*of*);
12.196 - (*if*) TermC.is_list (hd ts) (*then*);
12.197 -
12.198 -val return_discern_type_subst_4 =
12.199 -(* if TermC.is_list (hd ts)
12.200 - then*) [(id, ts |> map TermC.the_single |> TermC.list2isalist HOLogic.realT)]
12.201 -(* else []*)
12.202 -(*+*)val "[\"\n(vs, [c, c_2, c_3, c_4])\"]"
12.203 - = return_discern_type_subst_4 |> Subst.to_string @{context}
12.204 -
12.205 -(*-------------------- contine discern_feedback_subst ----------------------------------------*)
12.206 -val return_discern_feedback_subst_4 = return_discern_type_subst_4
12.207 -(*-------------------- contine mk_env_subst_DEL ----------------------------------------------*)
12.208 -val return_mk_env_subst_DEL_4 = return_discern_feedback_subst_4
12.209 -(*+*)val "[\"\n(vs, [c, c_2, c_3, c_4])\"]"
12.210 - = return_mk_env_subst_DEL_4 |> Subst.to_string @{context}
12.211 -(*\\\################# nth 4 equal_descr_pairs ############################################=//*)
12.212 -
12.213 -(*///################# nth 7 equal_descr_pairs ############################################=\\*)
12.214 - val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
12.215 - => (discern_feedback_subst id feedb) (*|> map fst (*rhs dropped*)|> map (pair id)*) ) (nth 7 equal_descr_pairs);
12.216 -"~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 7 equal_descr_pairs);
12.217 -(*--------------------------------------------------------------------------^^^----------------*)
12.218 -
12.219 - Pre_Conds.discern_feedback_subst id feedb;
12.220 -"~~~~~ fun discern_feedback_subst , args:"; val (id, Cor_TEST ((descr, (*[*)ts(*]*)), _)) = (id, feedb);
12.221 -(*+*)val (Free ("r_b", _), "[[y 0 = 0], [y L = 0], [M_b 0 = 0], [M_b L = 0]]")
12.222 - = (id, ts |> UnparseC.terms @{context});
12.223 -
12.224 - (*if*) fold (curry and_) (map TermC.is_list ts) true (*then*);
12.225 - val ts = ts;
12.226 -
12.227 - discern_type_subst (descr, id) ts;
12.228 -"~~~~~ fun discern_type_subst , args:"; val ((descr, id), ts) = ((descr, id), ts);
12.229 -val (Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) =
12.230 - (*case*) type_of descr (*of*);
12.231 - (*if*) TermC.is_list (hd ts) (*then*);
12.232 -
12.233 -val return_discern_type_subst_7 =
12.234 -(* if TermC.is_list (hd ts)
12.235 - then*) [(id, ts |> map TermC.the_single |> TermC.list2isalist HOLogic.boolT)]
12.236 -(* else []*)
12.237 -(*+*)val "[\"\n(r_b, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\"]"
12.238 - = return_discern_type_subst_7 |> Subst.to_string @{context}
12.239 -
12.240 -(*-------------------- contine discern_feedback_subst ----------------------------------------*)
12.241 -val return_discern_feedback_subst_7 = return_discern_type_subst_7
12.242 -(*-------------------- contine mk_env_subst_DEL ----------------------------------------------*)
12.243 -val return_mk_env_subst_DEL_7 = return_discern_type_subst_7
12.244 -(*+*)val "[\"\n(r_b, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\"]"
12.245 - = return_mk_env_subst_DEL_7 |> Subst.to_string @{context};
12.246 -(*\\\################# nth 7 equal_descr_pairs ############################################=//*)
12.247 -
12.248 -(*BEFORE correct (vs, [c, c_2, c_3, c_4])* )
12.249 -(*+*)val "[\"\n(l_l, L)\", \"\n(q_q, q_0)\", \"\n(fun_var, x)\", \"\n(vs, vs)\", \"\n(id_der, dy)\", \"\n(b_b, y)\"]"
12.250 -(*ERRORs still -----------------------------------------------------------^^^-------------------------------------, r_b*)
12.251 - = (env_subst |> Subst.to_string @{context})
12.252 -*)
12.253 -(*NOW only nth 7 is missing.. (but mk_env_eval_DEL completely broken)* )
12.254 -(*+*)val "[\"\n(l_l, L)\", \"\n(q_q, q_0)\", \"\n(fun_var, x)\", \"\n(vs, [c, c_2, c_3, c_4])\", \"\n(id_der, dy)\", \"\n(b_b, y)\"]"
12.255 -(*ERRORs still ---------------------------------------------------------------------------------------------------------------------, r_b*)
12.256 - = (env_subst |> Subst.to_string @ {context})
12.257 -*)
12.258 -(*+*)if (env_subst |> Subst.to_string @{context}) = "[\"\n" ^
12.259 -(*1*)"(l_l, L)\", \"\n" ^
12.260 -(*2*)"(q_q, q_0)\", \"\n" ^
12.261 -(*3*)"(fun_var, x)\", \"\n" ^
12.262 -(*4*)"(vs, [c, c_2, c_3, c_4])\", \"\n" ^
12.263 -(*5*)"(id_der, dy)\", \"\n" ^
12.264 -(*6*)"(b_b, y)\", \"\n" ^
12.265 -(*7*)"(r_b, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\"]"
12.266 -(*+*)then () else error "env_subst CHANGED";
12.267 -
12.268 -
12.269 -(*+*)if (i_model_max |> I_Model.to_string_TEST @{context}) = "[\n" ^
12.270 - "(1, [1], true ,#Given, (Cor_TEST Traegerlaenge L ,(l_l, [L]), Position.T)), \n" ^
12.271 - "(2, [1], true ,#Given, (Cor_TEST Streckenlast q_0 ,(q_q, [q_0]), Position.T)), \n" ^
12.272 - "(3, [1], true ,#Find, (Cor_TEST Biegelinie y ,(b_b, [y]), Position.T)), \n" ^
12.273 - "(4, [1], true ,#Relate, (Cor_TEST Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]), Position.T)), \n" ^
12.274 - "(5, [1], true ,#Given, (Cor_TEST FunktionsVariable x ,(fun_var, [x]), Position.T)), \n" ^
12.275 - "(6, [1], true ,#Given, (Cor_TEST GleichungsVariablen [c, c_2, c_3, c_4] ,(vs, [[c, c_2, c_3, c_4]]), Position.T)), \n" ^
12.276 - "(7, [1], true ,#Given, (Cor_TEST AbleitungBiegelinie dy ,(id_der, [dy]), Position.T))]"
12.277 -(*+*)then () else error "i_model_max CHANGED";
12.278 -
12.279 -(*||------------------ continue of_max_variant ---------------------------------------------\\*)
12.280 -
12.281 - mk_env_eval_DEL i_model_max;
12.282 -(*///----------------- step into mk_env_eval_DEL -------------------------------------------\\*)
12.283 -"~~~~~ fun mk_env_eval_DEL , args:"; val (i_singles) = (i_model_max);
12.284 - val xxx = (fn (_, _, _, _, (feedb, _)) => discern_feedback_subst id feedb);
12.285 -
12.286 -(*///################# nth 1 i_model_max \<longrightarrow>[], <>[] only in maximum-example ##############=\\*)
12.287 -"~~~~~ fun xxx , args:"; val (_, _, _, _, (feedb, _)) = nth 1 i_model_max;
12.288 -(*---------------------------------------------------------^^^------------*)
12.289 -(*+*)val "Cor_TEST Traegerlaenge L ,(l_l, [L])"
12.290 - = feedb |> I_Model.feedback_to_string'_TEST @{context};
12.291 -
12.292 - discern_feedback_subst id feedb;
12.293 -"~~~~~ fun discern_feedback_subst , args:"; val (Model_Def.Cor_TEST ((descr, [ts]), _)) = (feedb);
12.294 - (*if*) TermC.is_list ts (*else*);
12.295 - val ts = (*if TermC.is_list ts then TermC.isalist2list ts else*) [ts];
12.296 -
12.297 - Pre_Conds.discern_type_eval descr ts;
12.298 -"~~~~~ fun discern_type_eval , args:"; val (descr, ts) = (descr, ts);
12.299 -val _(*"real \<Rightarrow> una"*) =
12.300 - (*case*) type_of descr (*of*)
12.301 -;
12.302 - Pre_Conds.discern_atoms ts;
12.303 -"~~~~~ fun discern_atoms , args:"; val (ts) = (ts);
12.304 - (*if*) all_atoms ts (*then*);
12.305 -
12.306 -val return_distinguish_ts_eval_1 =
12.307 - map (rpair TermC.empty (*dummy rhs*)) ts
12.308 -(*-------------------- contine discern_type_subst --------------------------------------------*)
12.309 -(*-------------------- contine discern_feedback_subst ----------------------------------------*)
12.310 -(*-------------------- contine mk_env_eval_DEL -----------------------------------------------*)
12.311 -val return_mk_env_subst_DEL_1
12.312 - = filter_out (fn (_, b) => b = TermC.empty) return_distinguish_ts_eval_1
12.313 -(*+*)val [] = return_mk_env_subst_DEL_1
12.314 -(*\\\################# nth 1 i_model_max \<longrightarrow>[], <>[] only in maximum-example ##############=//*)
12.315 -(*\\\----------------- step into mk_env_eval_DEL -------------------------------------------//*)
12.316 -
12.317 -(*||------------------ contine of_max_variant ------------------------------------------------*)
12.318 -(* val env_eval = mk_env_eval_DEL i_model_max*)
12.319 - val env_eval = mk_env_eval_DEL i_model_max
12.320 -(*+*)val [] = env_eval
12.321 -val return_of_max_variant = (i_model_max, env_subst, env_eval)
12.322 -(*\\------------------ step into of_max_variant --------------------------------------------//*)
12.323 +(*+*)if return_of_max_variant_step = return_of_max_variant then () else error "<>";
12.324 +(*\\\----------------- step into of_max_variant --------------------------------------------//*)
12.325 + val (_, env_model, (env_subst, env_eval)) = return_of_max_variant
12.326
12.327 (*|------------------- contine init_pstate ---------------------------------------------------*)
12.328 - val actuals = map snd env_subst
12.329 -(*+*)val "[L, q_0, x, [c, c_2, c_3, c_4], dy, y, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]"
12.330 + val actuals = map snd env_model
12.331 +(*+*) val "[L, q_0, x, [c, c_2, c_3, c_4], dy, y, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]"
12.332 = actuals |> UnparseC.terms @{context}
12.333 -(*+*)val 7 = length actuals
12.334
12.335 val formals = Program.formal_args prog
12.336 (*+*)val "[l_l, q_q, fun_var, b_b, r_b, vs, id_der]"
12.337 @@ -547,12 +404,14 @@
12.338 val ist = Istate.e_pstate
12.339 |> Istate.set_eval prog_rls
12.340 |> Istate.set_env_true (relate_args [] formals actuals ctxt prog met_id formals actuals)
12.341 +;
12.342 +(*+*)(relate_args [] formals actuals ctxt prog met_id formals actuals)
12.343 +;
12.344 val return_init_pstate = (Istate.Pstate ist, ctxt, program)
12.345 -(*\------------------- step into init_pstate -----------------------------------------------//*)
12.346 -(*\------------------- step into me Add_Given_AbleitungBieg --------------------------------//*)
12.347 -
12.348 -val (p,_,f,nxt,_,pt) = return_Add_Given_AbleitungBieg
12.349 +(*\\------------------ step into init_pstate -----------------------------------------------//*)
12.350 +(*\------------------- step into me_Add_Given_AbleitungBieg --------------------------------//*)
12.351 +val (p,_,f,nxt,_,pt) = return_Add_Given_AbleitungBieg;
12.352 + val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
12.353 (* final test ... ----------------------------------------------------------------------------*)
12.354 (*+*)val ([], Met) = p
12.355 (*+*)val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
12.356 -
13.1 --- a/test/Tools/isac/Knowledge/algein.sml Fri Aug 04 23:07:04 2023 +0200
13.2 +++ b/test/Tools/isac/Knowledge/algein.sml Tue Aug 15 12:22:49 2023 +0200
13.3 @@ -43,26 +43,38 @@
13.4 ("Isac_Knowledge",["numerischSymbolische", "Berechnung"],
13.5 ["Berechnung", "erstNumerisch"]);
13.6 val p = e_pos'; val c = [];
13.7 -val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))](*nxt = ("Model_Pr*);
13.8 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenLaenge (k = 10)"*);
13.9 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "Querschnitt (q = 1)"*);
13.10 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenUnten [b1 = k - 2*q]"*);
13.11 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenUnten [b2 = k - 2 * q, b3=..b4*);
13.12 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenSenkrecht [v1 = k]"*);
13.13 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenSenkrecht [v2 = k, v3 = k, v4]*);
13.14 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenOben [b1 = k - 2 *q])*);
13.15 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenOben [b2 = k - 2 * q, b3 =, b4*);
13.16 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Find "GesamtLaenge L"*);
13.17 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Theory "AlgEin"*);
13.18 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Problem ["numerischSymbolis,Be*);
13.19 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Method ["Berechnung", "erstSym*);
13.20 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*Apply_Method*);
13.21 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute["Oben = boollist2sum [b1 =*);
13.22 +val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))]; val Model_Probelm = nxt
13.23 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenLaenge (k = 10)" = nxt
13.24 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Querschnitt (q = 1)" = nxt
13.25 +(*/---broken elementwise input to lists---\* )
13.26 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenUnten [b1 = k - 2 * q]" = nxt
13.27 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenUnten [b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q]" = nxt
13.28 +( *\---broken elementwise input to lists---/*)
13.29 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenUnten [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q]" = nxt
13.30 +
13.31 +(*/---broken elementwise input to lists---\* )
13.32 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenSenkrecht [v1 = k]" = nxt
13.33 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenSenkrecht [v2 = k, v3 = k, v4 = k]" = nxt
13.34 +( *\---broken elementwise input to lists---/*)
13.35 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenSenkrecht [v1 = k, v2 = k, v3 = k, v4 = k]" = nxt
13.36 +
13.37 +(*/---broken elementwise input to lists---\* )
13.38 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenOben [t1 = k - 2 * q]" = nxt
13.39 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenOben [t2 = k - 2 * q, t3 = k - 2 * q, t4 = k - 2 * q]" = nxt
13.40 +( *\---broken elementwise input to lists---/*)
13.41 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "KantenOben [t1 = k - 2 * q, t2 = k - 2 * q, t3 = k - 2 * q, t4 = k - 2 * q]" = nxt
13.42 +
13.43 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "GesamtLaenge L" = nxt
13.44 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Isac_Knowledge" = nxt
13.45 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["numerischSymbolische", "Berechnung"] = nxt
13.46 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["Berechnung", "erstNumerisch"] = nxt
13.47 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["Berechnung", "erstNumerisch"] = nxt
13.48 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["oben = t1 + t2 + t3 + t4"] = nxt;
13.49 f2str f;
13.50 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute ["t1 = k - 2 * q", *);f2str f;
13.51 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute ["k = 10", "q = 1"]*);f2str f;
13.52 -val (p,_,f,nxt,_,pt) = me nxt p c pt(*Rewrite_Set "norm_Rational"*);f2str f;
13.53 -val (p,_,f,nxt,_,pt) = me nxt p c pt(**);
13.54 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["t1 = k - 2 * q", "t2 = k - 2 * q", "t3 = k - 2 * q", "t4 = k - 2 * q"] = nxt
13.55 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["k = 10", "q = 1"] = nxt
13.56 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set "norm_Poly" = nxt
13.57 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["senkrecht = v1 + v2 + v3 + v4"] = nxt;
13.58 if f2str f = "L = 32 + senkrecht + unten" then ()
13.59 else error "algein.sml diff.behav. in erstNumerisch 1";
13.60 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
13.61 @@ -74,11 +86,12 @@
13.62 then case nxt of End_Proof' => ()
13.63 | _ => error "algein.sml diff.behav. in erstNumerisch 99 1"
13.64 else error "algein.sml diff.behav. in erstNumerisch 99 2";
13.65 -DEconstrCalcTree 1;
13.66 +
13.67
13.68 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
13.69 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
13.70 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
13.71 +(*/------------------- WN230815 test broke since ???, undetected ERROR in autoCalculate ----\\* )
13.72 CalcTree @{context}
13.73 [(["KantenLaenge (k=(10::real))", "Querschnitt (q=(1::real))",
13.74 "KantenUnten [b1 = k - 2*(q::real), b2 = k - 2*(q::real), b3 = k - 2*(q::real), b4 = k - 2*(q::real) ]",
13.75 @@ -93,6 +106,7 @@
13.76 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
13.77 if p = ([], Res) andalso UnparseC.term @{context} (get_obj g_res pt (fst p)) = "L = 104" then()
13.78 else error "algein.sml: 'Berechnung' 'erstSymbolisch' changed";
13.79 +( *\------------------- WN230815 test broke since ???, undetected ERROR in autoCalculate ----//*)
13.80
13.81 "----------- Widerspruch 3 = 777 ---------------------------------";
13.82 "----------- Widerspruch 3 = 777 ---------------------------------";
14.1 --- a/test/Tools/isac/Knowledge/biegelinie-1.sml Fri Aug 04 23:07:04 2023 +0200
14.2 +++ b/test/Tools/isac/Knowledge/biegelinie-1.sml Tue Aug 15 12:22:49 2023 +0200
14.3 @@ -21,7 +21,7 @@
14.4 "-----------------------------------------------------------------";
14.5 "------ biegelinie-4.sml -----------------------------------------";
14.6 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto TODO investigate failure ------";
14.7 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
14.8 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' --------------------------------";
14.9 "----------- biegel Bsp.7.70. check Problem + MethodC model ----------------------------------";
14.10 "-----------------------------------------------------------------";
14.11 "-----------------------------------------------------------------";
15.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Fri Aug 04 23:07:04 2023 +0200
15.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Tue Aug 15 12:22:49 2023 +0200
15.3 @@ -34,7 +34,7 @@
15.4 if p = ([], Pbl) then () else error ""
15.5 get_obj I pt (fst p); (*TODO investigate failure*)
15.6
15.7 -(* NOTE: \<up> \<up> \<up> \<up> \<up> ^^ no progress already in isabisac15, but not noticed \<up> \<up> \<up> \<up> \<up> ^^ * )
15.8 +(* NOTE: \<up> \<up> \<up> \<up> \<up> ^^ no progress already in isabisac15, but not noticed \<up> \<up> \<up> \<up> \<up> ^^ * )
15.9 (*[], Met*)autoCalculate 1 CompleteCalcHead;
15.10 (*[1], Pbl*)autoCalculate 1 (Steps 1); (* into SubProblem *)
15.11 (*[1], Res*)autoCalculate 1 CompleteSubpbl; (**)
15.12 @@ -70,7 +70,7 @@
15.13 SOME (Check_Postcond ["normalise", "4x4", "LINEAR", "system"]) => ()
15.14 | _ => error "ERROR biegel.7.70 changed 1"
15.15 else error "ERROR biegel.7.70 changed 2";
15.16 -( * NOTE: \<up> \<up> \<up> \<up> \<up> ^^ no progress already in isabisac15, but not noticed \<up> \<up> \<up> \<up> \<up> ^^ *)
15.17 +( * NOTE: \<up> \<up> \<up> \<up> \<up> ^^ no progress already in isabisac15, but not noticed \<up> \<up> \<up> \<up> \<up> ^^ *)
15.18
15.19
15.20 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' --------------------------------";
15.21 @@ -84,7 +84,8 @@
15.22 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))]
15.23
15.24 val (tac as Model_Problem (*["vonBelastungZu", "Biegelinien"]*), (pt, p as ([1], Pbl))) =
15.25 - (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
15.26 + (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'|> me'
15.27 + (*---broken elementwise input to lists---* ) |> me' ( *---broken elementwise input to lists---*)
15.28 (*INVISIBLE: SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''])*)
15.29 |> me';
15.30 val (tac as Subproblem ("Biegelinie", ["named", "integrate", "function"]), (pt, p as ([1, 2], Res))) =
15.31 @@ -119,14 +120,15 @@
15.32
15.33 (*INVISIBLE: SubProblem (''Biegelinie'', [''makeFunctionTo'', ''"equation''])*)
15.34 val (tac as Model_Problem (*[''makeFunctionTo'', ''"equation'']*), (pt, p as ([2, 1], Pbl))) =
15.35 - (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
15.36 + (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
15.37 + (*---broken elementwise input to lists---* ) |> me' ( *---broken elementwise input to lists---*)
15.38 (* ERROR for a long time -----vvvvvvvvvvvvvvvvvvvvvvvv.. (should be evaluated!) *)
15.39 val (tac as Substitute ["x = 0"], (pt, p as ([2, 1, 1], Frm))) =
15.40 (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me';
15.41
15.42 if p = ([2, 1, 1], Frm) andalso (Calc.current_formula (pt, p) |> UnparseC.term @{context}) =
15.43 "y x =\nc_4 + c_3 * x +\n1 / (- 1 * EI) *\n(c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)"
15.44 -then () else error "";
15.45 +then () else error "IntegrierenUndKonstanteBestimmen2 FAILED";
15.46
15.47
15.48 (**** biegel Bsp.7.70. check Problem + MethodC model ##################################### ****)
16.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml Fri Aug 04 23:07:04 2023 +0200
16.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml Tue Aug 15 12:22:49 2023 +0200
16.3 @@ -1,8 +1,6 @@
16.4 (* Title: tests on DiophantEq.thy
16.5 Author: Mathias Lehnfeld 2011
16.6 (c) due to copyright terms
16.7 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
16.8 - 10 20 30 40 50 60 70 80
16.9 *)
16.10 "--------------------------------------------------------";
16.11 "table of contents --------------------------------------";
16.12 @@ -45,6 +43,8 @@
16.13 "----------- mathengine with usecase1 -------------------";
16.14 "----------- mathengine with usecase1 -------------------";
16.15 "----------- mathengine with usecase1 -------------------";
16.16 +"----------- Take as 1st stac in program -------------------------------------------------------";
16.17 +(*/--------- valueless test with experimental Problem and MethodC -----------------------------\* )
16.18 val p = e_pos'; val c = [];
16.19 val (fmz, (thy, pbl, met)) =
16.20 (["boolTestGiven (xxx + 111 = abc + (123::int))", "intTestGiven xxx",
16.21 @@ -61,6 +61,7 @@
16.22 val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.23 val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.24 *)
16.25 +( *\--------- valueless test with experimental Problem and MethodC -----------------------------/*)
16.26
16.27 "----------- rewriting for usecase2 ---------------------";
16.28 "----------- rewriting for usecase2 ---------------------";
16.29 @@ -81,6 +82,7 @@
16.30 "----------- mathengine with usecase2 -------------------";
16.31 "----------- mathengine with usecase2 -------------------";
16.32 "----------- mathengine with usecase2 -------------------";
16.33 +(*/--------- valueless test with experimenta Problem and MethodC ------------------------------\* )
16.34 val p = e_pos'; val c = [];
16.35 val (fmz, (thy, pbl, met)) =
16.36 (["intTestGiven (xxx + abc + - 1 * 111 + (123::int))", "intTestFind sss"],
16.37 @@ -102,4 +104,6 @@
16.38 (*nxt = ("Empty_Tac", ...) #############################*)
16.39 val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.40 *)
16.41 +( *\--------- valueless test with experimental Problem and MethodC -----------------------------/*)
16.42
16.43 +
17.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Fri Aug 04 23:07:04 2023 +0200
17.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Tue Aug 15 12:22:49 2023 +0200
17.3 @@ -475,6 +475,7 @@
17.4 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
17.5 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
17.6 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
17.7 +(*/------------------- WN230815 test broke since ???, undetected ERROR in autoCalculate ----\\* )
17.8 States.reset ();
17.9 CalcTree @{context} [(["Term (2*u - 5 - (3 - 4*u) + (8*u + 9))",
17.10 "normalform N"],
17.11 @@ -501,6 +502,7 @@
17.12 if p = ([], Res) andalso UnparseC.term @{context} (get_obj g_res pt (fst p)) = "29 = 29"
17.13 then () else error "polyminus.sml: Probe 29 = 29";
17.14 Test_Tool.show_pt pt;
17.15 +( *\------------------- WN230815 test broke since ???, undetected ERROR in autoCalculate ----//*)
17.16
17.17
17.18 "----------- try fun applyTactics --------------------------------";
18.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Fri Aug 04 23:07:04 2023 +0200
18.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Tue Aug 15 12:22:49 2023 +0200
18.3 @@ -2,6 +2,8 @@
18.4 Author: Walther Neuper 1105
18.5 (c) copyright due to lincense terms.
18.6
18.7 +COMPARE Specify/specify.sml --- specify-phase: low level functions ---
18.8 +
18.9 ATTENTION: the file creates buffer overflow if copied in one piece !
18.10
18.11 Note: This test --- steps into me --- more than once, to a somewhat extreme extent;
19.1 --- a/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Fri Aug 04 23:07:04 2023 +0200
19.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Tue Aug 15 12:22:49 2023 +0200
19.3 @@ -225,123 +225,17 @@
19.4 (model_patt, program, prog, prog_rls, where_, where_rls)
19.5 | _ => raise ERROR ("init_pstate with " ^ MethodC.id_to_string met_id)
19.6
19.7 - val (i_model_max, env_subst, env_eval) =
19.8 - of_max_variant model_patt i_model;
19.9 -val return_of_max_variant = (i_model_max, env_subst, env_eval);
19.10 -(*///----------------- step into of_max_variant NEW ----------------------------------------\\*)
19.11 -"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
19.12 -
19.13 -(*+*)i_model: I_Model.T_TEST;
19.14 -
19.15 - val all_variants =
19.16 - map (fn (_, variants, _, _, _) => variants) i_model
19.17 - |> flat
19.18 - |> distinct op =
19.19 - val variants_separated = map (filter_variants' i_model) all_variants
19.20 - val sums_corr = map (cnt_corrects) variants_separated
19.21 -(*+*)val [3] = sums_corr;
19.22 -
19.23 - val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
19.24 -(*+*)val [(3, 1)] = sum_variant_s;
19.25 -
19.26 - val (_, max_variant) = hd (*..crude decision, up to improvement *)
19.27 - (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
19.28 -(*+*)val 1 = max_variant;
19.29 -
19.30 - val i_model_max =
19.31 - filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
19.32 -(*+*)val 3 = length i_model_max;
19.33 -
19.34 - val equal_descr_pairs =
19.35 - map (get_equal_descr i_model) model_patt
19.36 - |> flat
19.37 -(*+*)val 3 = length equal_descr_pairs; (*only 1 variant in this test*)
19.38 -
19.39 - val env_subst =
19.40 - Pre_Conds.mk_env_subst_DEL equal_descr_pairs;
19.41 -(*+*)(equal_descr_pairs |> descr_pairs_to_string @{context}) = "[" ^
19.42 - "((#Given, (equality, e_e)), " ^
19.43 - "(1, [1], true ,#Given, (Cor_TEST equality (x + 1 = 2) ,(e_e, [x + 1 = 2]), Position.T))), " ^
19.44 - "((#Given, (solveFor, v_v)), " ^
19.45 - "(2, [1], true ,#Given, (Cor_TEST solveFor x ,(v_v, [x]), Position.T))), " ^
19.46 - "((#Find, (solutions, v_v'i')), " ^
19.47 - "(3, [1], true ,#Find, (Cor_TEST solutions L ,(v_v'i', [L]), Position.T)))]";
19.48 -(*------------------------------------------------^^^^^^^^^^^^^--- NOT FOUND*)
19.49 -
19.50 -(*////--------- ------ step into mk_env_subst_DEL ------------------------------------------\\*)
19.51 -"~~~~~ fun mk_env_subst_DEL , args:"; val (equal_descr_pairs) = (equal_descr_pairs);
19.52 -
19.53 -val xxx =
19.54 - (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
19.55 - => (discern_feedback_subst id feedb));
19.56 -"~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 3 equal_descr_pairs);
19.57 -val [(Free ("v_v'i'", _), Free ("L", _))] =
19.58 - (discern_feedback_subst id feedb);
19.59 -"~~~~~ fun discern_feedback_subst , args:"; val (id, (Model_Def.Cor_TEST ((descr, [ts]), _)))
19.60 - = (id, feedb);
19.61 - discern_type_subst (descr, id) [ts];
19.62 -"~~~~~ fun discern_type_subst , args:"; val ((descr, id), ts) = ((descr, id), [ts]);
19.63 -val (Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) =
19.64 - (*case*) type_of descr (*of*);
19.65 - (*if*) TermC.is_list (hd ts) (*else*);
19.66 -
19.67 -val return_discern_type_subst_3 =
19.68 -(* if TermC.is_list (hd ts)
19.69 - then [(id, ts |> map TermC.the_single |> TermC.list2isalist HOLogic.boolT)]
19.70 - else*) [(id, Library.the_single ts)]
19.71 -
19.72 -(*\\\\---------------- step into mk_env_subst_DEL ------------------------------------------//*)
19.73 -(*+*)val "[\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\", \"\n(v_v'i', L)\"]" =
19.74 - env_subst |> Subst.to_string @{context}
19.75 -
19.76 -(*|||----------------- contine of_max_variant ------------------------------------------------*)
19.77 - val env_eval = Pre_Conds.mk_env_eval_DEL i_model_max
19.78 -(*+*)val [] =
19.79 - map (fn (t1, t2) => "(" ^ UnparseC.term @{context} t1 ^ ", " ^ UnparseC.term @{context} t2 ^ ")")
19.80 - env_eval
19.81 -
19.82 -val return_of_max_variant_step = (i_model_max, env_subst, env_eval);
19.83 -(*+*)if return_of_max_variant_step = return_of_max_variant then () else error "<>";
19.84 -(*\\\----------------- step into of_max_variant NEW ----------------------------------------\\*)
19.85 -val (i_model_max, env_subst, _) = return_of_max_variant
19.86 -
19.87 -(*||------------------ continue init_pstate NEW --------------------------------------------\\*)
19.88 - val actuals = map snd env_subst
19.89 + val (_, env_model, (env_subst, env_eval)) = I_Model.of_max_variant model_patt i_model;
19.90 + val actuals = map snd env_model
19.91 (*+*)val "[x + 1 = 2, x, L]" = actuals |> UnparseC.terms @{context}
19.92
19.93 - val formals = Program.formal_args prog
19.94 + val formals = Program.formal_args prog
19.95 (*+*)val "[e_e, v_v]" = (formals |> UnparseC.terms @{context})
19.96
19.97 (*+*)val "minisubpbl e_e v_v =\n(let e_ea =\n (Try (Rewrite_Set ''norm_equation'') #>\n Try (Rewrite_Set ''Test_simplify''))\n e_e;\n L_La =\n SubProblem\n (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],\n [''Test'', ''solve_linear''])\n [BOOL e_e, REAL v_v]\n in Check_elementwise L_L {v_v. Assumptions})" =
19.98 (prog |> UnparseC.term @{context})
19.99
19.100 - val preconds =
19.101 - Pre_Conds.check_from_store ctxt where_rls where_ env_subst env_eval
19.102 -val return_check_from_store = preconds
19.103 -(*+*)val (true, [(true, Const ("Test.precond_rootmet", _) $ Free ("x", _))]) = return_check_from_store;
19.104 -(*///----------------- step into check_from_store ------------------------------------------//*)
19.105 -"~~~~~ fun check_from_store , args:"; val (ctxt, where_rls, preconds, env_subst, env_eval) =
19.106 - (ctxt, where_rls, where_, env_subst, env_eval);
19.107 -
19.108 -(*+*)val "[precond_rootmet v_v]" = (where_ |> UnparseC.terms @{context})
19.109 -(*+*)val "[\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\", \"\n(v_v'i', L)\"]" = env_subst |> Subst.to_string @{context}
19.110 -(*+*)val [] = env_eval (*special case, Maximum-expl more general*)
19.111 -
19.112 - val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
19.113 -(*+*)val [(true, Const ("Test.precond_rootmet", _) $ Free ("x", _))] = pres_subst
19.114 -
19.115 - val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
19.116 -(*+*)val [(true, Const ("Test.precond_rootmet", _) $ Free ("x", _))] = full_subst
19.117 -
19.118 - val evals = map (eval ctxt where_rls) full_subst
19.119 -(*+*)val [(true, Const ("Test.precond_rootmet", _) $ Free ("x", _))] = evals
19.120 -
19.121 -val return_check_from_store_step = (foldl and_ (true, map fst evals), pres_subst)
19.122 -(*+*)val (true, [(true, Const ("Test.precond_rootmet", _) $ Free ("x", _))]) =
19.123 - return_check_from_store_step;
19.124 -(*+*)if return_check_from_store_step = return_check_from_store then () else error "<>";
19.125 -(*\\\----------------- step into check_from_store ------------------------------------------//*)
19.126 - val preconds = return_check_from_store
19.127 + val preconds = Pre_Conds.check_envs_TEST ctxt where_rls where_ (env_model, (env_subst, env_eval))
19.128
19.129 (*||------------------ continue init_pstate NEW --------------------------------------------\\*)
19.130 val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));
19.131 @@ -427,4 +321,4 @@
19.132 . . . . . . . . . . Rewrite_Set "Test_simplify",
19.133 ([2], Res), - 1 + x = 0
19.134 . . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"]] ..INCORRECT
19.135 -*)
19.136 +*)
19.137 \ No newline at end of file
20.1 --- a/test/Tools/isac/Specify/i-model.sml Fri Aug 04 23:07:04 2023 +0200
20.2 +++ b/test/Tools/isac/Specify/i-model.sml Tue Aug 15 12:22:49 2023 +0200
20.3 @@ -18,6 +18,7 @@
20.4 open Test_Code;
20.5 open Tactic;
20.6 open Pos;
20.7 +
20.8 "----------- investigate fun add_single in I_Model -------------------------------------------";
20.9 "----------- investigate fun add_single in I_Model -------------------------------------------";
20.10 "----------- investigate fun add_single in I_Model -------------------------------------------";
20.11 @@ -69,10 +70,10 @@
20.12 "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"
20.13 (*+*)then () else error "INITIAL O_Model CHANGED";
20.14 (*+*)if I_Model.to_string ctxt pbl = "[\n" ^
20.15 - "(0 ,[] ,false ,#Given ,Inc Streckenlast ,(??.empty, [])), \n" ^
20.16 - "(0 ,[] ,false ,#Find ,Inc Biegelinie ,(??.empty, [])), \n" ^
20.17 - "(0 ,[] ,false ,#Relate ,Inc Randbedingungen [] ,(??.empty, [])), \n" ^
20.18 - "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L]))]"
20.19 + "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^
20.20 + "(2 ,[1] ,false ,#Given ,Inc Streckenlast ,(Streckenlast, [])), \n" ^
20.21 + "(3 ,[1] ,false ,#Find ,Inc Biegelinie ,(Biegelinie, [])), \n" ^
20.22 + "(4 ,[1] ,false ,#Relate ,Inc Randbedingungen [] ,(Randbedingungen, []))]"
20.23 (*+*)then () else error "INITIAL I_Model CHANGED";
20.24
20.25 val return_check_single = (*case*)
20.26 @@ -104,10 +105,10 @@
20.27 val tac' = I_Model.make_tactic m_field (ct, i_model')
20.28 ;
20.29 (*+*)if I_Model.to_string ctxt i_model' = "[\n" ^
20.30 - "(0 ,[] ,false ,#Find ,Inc Biegelinie ,(??.empty, [])), \n" ^
20.31 - "(0 ,[] ,false ,#Relate ,Inc Randbedingungen [] ,(??.empty, [])), \n" ^
20.32 "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^
20.33 - "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0]))]"
20.34 + "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
20.35 + "(3 ,[1] ,false ,#Find ,Inc Biegelinie ,(Biegelinie, [])), \n" ^
20.36 + "(4 ,[1] ,false ,#Relate ,Inc Randbedingungen [] ,(Randbedingungen, []))]"
20.37 (*+*)then () else error "FINAL I_Model CHANGED";
20.38
20.39 val (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)
20.40 @@ -120,9 +121,15 @@
20.41
20.42 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]"*)
20.43
20.44 -(* final test ...*)
20.45 +(* final test ... BEFORE BREAKING ELEMENTWISE INPUT TO LISTS* )
20.46 if p = ([], Pbl) then
20.47 - case nxt of Add_Relation "Randbedingungen [y 0 = 0]" => () | _ => error "investigate fun add_single CHANGED 1"
20.48 + case nxt of Add_Relation "Randbedingungen [y 0 = 0]" => () | _
20.49 + => error "investigate fun add_single CHANGED 1"
20.50 +else error "investigate fun add_single CHANGED 2"
20.51 +( * final test ... AFTER BREAKING ELEMENTWISE INPUT TO LISTS*)
20.52 +if p = ([], Pbl) then
20.53 + case nxt of Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" => () | _
20.54 + => error "investigate fun add_single CHANGED 1"
20.55 else error "investigate fun add_single CHANGED 2"
20.56
20.57 "----------- build I_Model.init_TEST -----------------------------------------------------------";
21.1 --- a/test/Tools/isac/Specify/refine.sml Fri Aug 04 23:07:04 2023 +0200
21.2 +++ b/test/Tools/isac/Specify/refine.sml Tue Aug 15 12:22:49 2023 +0200
21.3 @@ -9,8 +9,9 @@
21.4 "refine.thy: store test-pbtyps by 'setup' ------------------------------------------------------";
21.5 "----------- testdata for refin, Refine.refine_ori --------------------------------------------";
21.6 (*"----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";*)
21.7 -"----------- Refine.refine_ori test-pbtyps --requires 'setup'----------------------------------";
21.8 +"----------- Refine.refine_ori test-pbtyps --requires 'setup'-----------------------------------";
21.9 "----------- refine test-pbtyps ------requires 'setup'------------------------------------------";
21.10 +"----------- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";
21.11 "----------- Refine_Problem (from subp-rooteq.sml) ---------------------------------------------";
21.12 "----------- equation with CalcTree [ = 6 / 5] for timing: with/out adapt_to_type --------------";
21.13 "----------- refine ad-hoc equation for timing: with/out adapt_to_type -------------------------";
21.14 @@ -315,6 +316,164 @@
21.15 : match list*)
21.16
21.17
21.18 +"----------- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";
21.19 +"----------- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";
21.20 +"----------- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";
21.21 +(*overwrites NEW funs in Test_Theory ABOVE* )
21.22 +open Refine
21.23 +open M_Match
21.24 +open Pre_Conds
21.25 +( *overwrites NEW funs in Test_Theory ABOVE*)
21.26 +(*
21.27 + refinement of the first eqsystem in Biegelinie, IntegrierenUndKonstanteBestimmen2;
21.28 + this example was the demonstrator;
21.29 + respective data are in ~/proto4/../exp_Statics_Biegel_Timischl_7-70.xml.
21.30 + Data for this test are from biegelinie-5.sml, --- me IntegrierenUndKonstanteBestimmen2 ALL ---
21.31 +*)
21.32 +(*+*)val o_model = [
21.33 +(1, [1], "#Given", @{term "equalities"},
21.34 + [@{term "[(0::real) = - 1 * c_4 / - 1]"},
21.35 + @{term "[(0::real) = (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / - 24]"},
21.36 + @{term "[(0::real) = c_2]"},
21.37 + @{term "[(0::real) = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"}] ),
21.38 +(*Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c", "real") $ Const ("List.list.Nil", "real list"),*)
21.39 +(2, [1], "#Given", @{term "solveForVars"},
21.40 + [@{term "[c] ::real list"},
21.41 + @{term "[c_2]::real list"},
21.42 + @{term "[c_3]::real list"},
21.43 + @{term "[c_4]::real list"}] ),
21.44 +(3, [1], "#Find", @{term "solution"}, [@{term "ss'''::bool list"}] )]
21.45 +;
21.46 +val SOME ["normalise", "4x4", "LINEAR", "system"] =
21.47 + refine_ori @{context} o_model ["LINEAR", "system"];
21.48 +"~~~~~ fun refine_ori , args:"; val (ctxt, oris, pblID) =
21.49 + (@{context}, o_model, ["LINEAR", "system"]);
21.50 +
21.51 + val opt as SOME ["system", "LINEAR", "4x4", "normalise"]
21.52 + = app_ptyp (refin ctxt ((rev o tl) pblID) oris) pblID (rev pblID);
21.53 +(*
21.54 + app_ptyp works strangely, parameter passing is awkward.
21.55 + Present refin knows structure of Store.T, thus we bypass app_ptyp
21.56 +*)
21.57 +(*!*)val pblID = ["LINEAR", "system"];(**)
21.58 +val return_refin as SOME ["system", "LINEAR", "LINEAR", "4x4", "normalise"] = (**)
21.59 + refin ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));
21.60 +"~~~~~ fun refin , args:"; val (ctxt, pblRD, ori, (Store.Node (pI, [py], pys)))
21.61 + = (ctxt, (rev pblID), oris, Store.get_node (rev pblID) pblID (get_pbls ()));
21.62 + val {where_rls, model, where_, ...} = py: Problem.T
21.63 + val model = map (Model_Pattern.adapt_to_type ctxt) model
21.64 + val where_ = map (ParseC.adapt_term_to_type ctxt) where_;
21.65 + (*if*) M_Match.match_oris ctxt where_rls ori (model, where_) (*then*);
21.66 +val return_refin as SOME ["system", "LINEAR"] = SOME (pblRD (** )@ [pI]( **))
21.67 +
21.68 +(*follow the trace created in parallel by writeln in Store.get_node and Refine.refin*)
21.69 +(*!*)val pblID = ["4x4", "LINEAR", "system"];(**)
21.70 +val return_refin as SOME ["system", "LINEAR", "4x4", "4x4", "normalise"] = (**)
21.71 + refin ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));
21.72 +"~~~~~ fun refin , args:"; val (ctxt, pblRD, ori, (Store.Node (pI, [py], pys)))
21.73 + = (ctxt, (rev pblID), oris, Store.get_node (rev pblID) pblID (get_pbls ()));
21.74 + val {where_rls, model, where_, ...} = py: Problem.T
21.75 + val model = map (Model_Pattern.adapt_to_type ctxt) model
21.76 + val where_ = map (ParseC.adapt_term_to_type ctxt) where_
21.77 +
21.78 +(*+*)val (**)true(** )false( **) = (*if*)
21.79 + M_Match.match_oris ctxt where_rls o_model (model, where_);
21.80 +"~~~~~ fun match_oris , args:"; val (ctxt, where_rls, o_model, (model_pattern, where_)) =
21.81 + (ctxt, where_rls, o_model, (model, where_));
21.82 + val i_model = (flat o (map (chk1_ model_pattern))) o_model;
21.83 +
21.84 +(*+*)val "[\n(1, [\"1\"], #Given, equalities, [\"[0 = - 1 * c_4 / - 1]\", \"[0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24]\", \"[0 = c_2]\", \"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]\"]), \n(2, [\"1\"], #Given, solveForVars, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n(3, [\"1\"], #Find, solution, [\"ss'''\"])]"
21.85 + = o_model |> O_Model.to_string @{context};
21.86 +(*+*)if "[\n" ^
21.87 + "(1 ,[1] ,true ,#Given ,Cor equalities\n [0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2] ,(e_s, [[0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]])), \n" ^
21.88 + "(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2, c_3, c_4] ,(v_s, [[c, c_2, c_3, c_4]])), \n" ^
21.89 + "(3 ,[1] ,true ,#Find ,Cor solution ss''' ,(ss''', [ss''']))]"
21.90 + = (i_model |> I_Model.to_string @{context}) then () else raise error "i_model CAHNGED";
21.91 +(*+*)val "[\"(#Given, (equalities, e_s))\", \"(#Given, (solveForVars, v_s))\", \"(#Find, (solution, ss'''))\"]"
21.92 + = model_pattern |> Model_Pattern.to_string @{context}
21.93 +(*+*)val "[Length e_s = 4, Length v_s = 4]" = where_ |> UnparseC.terms @{context}
21.94 +
21.95 + val mvat = I_Model.variables i_model;
21.96 + val complete = chk1_mis mvat i_model model_pattern;
21.97 +
21.98 + val (pb as true, (** )_( **)where_'(**)) =
21.99 + Pre_Conds.check_OLD ctxt where_rls where_ (model_pattern, I_Model.OLD_to_TEST i_model);
21.100 +"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
21.101 + (ctxt, where_rls, where_, (model_pattern, I_Model.OLD_to_TEST i_model));
21.102 +
21.103 +(*+*)val [(true, xxx), (true, yyy)] = where_'
21.104 +(*+*)val "[Length\n [0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2] =\n4, Length [c, c_2, c_3, c_4] = 4]"
21.105 + = where_' |> map #2 |> UnparseC.terms @{context}
21.106 +
21.107 + val (_, env_model, (env_subst, env_eval)) =
21.108 + of_max_variant model_patt i_model;
21.109 +"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
21.110 + val all_variants =
21.111 + map (fn (_, variants, _, _, _) => variants) i_model
21.112 + |> flat
21.113 + |> distinct op =
21.114 + val variants_separated = map (filter_variants' i_model) all_variants
21.115 + val sums_corr = map (cnt_corrects) variants_separated
21.116 + val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
21.117 + val (_, max_variant) = hd (*..crude decision, up to improvement *)
21.118 + (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
21.119 + val i_model_max =
21.120 + filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
21.121 + val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
21.122 +
21.123 + val env_model = make_env_model equal_descr_pairs
21.124 + val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
21.125 +
21.126 + val subst_eval_list =
21.127 + make_envs_preconds equal_givens;
21.128 +"~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
21.129 +"~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 1 equal_givens);
21.130 +"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) =
21.131 + (id, feedb);
21.132 +
21.133 +val return_discern_typ as [] =
21.134 + discern_typ id (descr, ts);
21.135 +"~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts));
21.136 +
21.137 +(*+*)val "[[0 = - 1 * c_4 / - 1], [0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24], [0 = c_2], [0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]]"
21.138 + = ts |> UnparseC.terms @{context}
21.139 +
21.140 + val ts = if Model_Pattern.is_list_descr descr
21.141 + then if TermC.is_list (hd ts)
21.142 + then ts |> map TermC.isalist2list |> flat
21.143 + else ts
21.144 + else ts
21.145 +
21.146 +(*+*)val "[0 = - 1 * c_4 / - 1, 0 =\n(- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n- 24, 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"
21.147 + = ts |> UnparseC.terms @{context};
21.148 +
21.149 + (*if*) Model_Pattern.typ_of_element descr = HOLogic.boolT (*then*);
21.150 +
21.151 +(*+*)val false = all_lhs_atoms ts
21.152 +(*-------------------- contine check_OLD -----------------------------------------------------*)
21.153 +
21.154 + val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
21.155 +
21.156 +(*+*)if "[\"\n" ^
21.157 + "(e_s, [0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2])\", \"\n" ^
21.158 + "(v_s, [c, c_2, c_3, c_4])\", \"\n(ss''', ss''')\"]"
21.159 + = (env_model |> Subst.to_string @{context}) then () else error "env_model CAHNGED";
21.160 +(*+*)val "[]" = env_eval |> Subst.to_string @{context} (*GOON \<rightarrow> []*)
21.161 +
21.162 + val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
21.163 + val full_subst = if env_eval = [] then pres_subst_other
21.164 + else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
21.165 + val evals = map (eval ctxt where_rls) full_subst
21.166 +val return_check_OLD = (foldl and_ (true, map fst evals), pres_subst_other)
21.167 +
21.168 +val return_refin as SOME ["system", "LINEAR", "4x4"] = SOME (pblRD(** ) @ [pI]( **))
21.169 +
21.170 +(*follow the trace created in parallel by writeln in Store.get_node and Refine.refin*)
21.171 +(*!*)val pblID = ["normalise", "4x4", "LINEAR", "system"];(**)
21.172 +val return_refin as SOME ["system", "LINEAR", "4x4", "normalise", "normalise"] =
21.173 + refin ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));
21.174 +
21.175 +
21.176 "----------- Refine_Problem (from subp-rooteq.sml) ---------------------------------------------";
21.177 "----------- Refine_Problem (from subp-rooteq.sml) ---------------------------------------------";
21.178 "----------- Refine_Problem (from subp-rooteq.sml) ---------------------------------------------";
21.179 @@ -345,7 +504,7 @@
21.180 case f of Test_Out.PpcKF (Test_Out.Problem [],
21.181 {Find = [Incompl "solutions []"], With = [],
21.182 Given = [Correct "equality ((x + 1) * (x + 2) = x \<up> 2 + 8)", Correct "solveFor x"],
21.183 - Where = [False www(*! ! ! ! ! !*)],
21.184 + Where = [Correct(*WAS False*) www(*! ! ! ! ! !*)],
21.185 Relate = [],...}) => www(*! ! !*)
21.186 | _ => error "--- Refine_Problem broken 1";
21.187 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)"
21.188 @@ -379,7 +538,7 @@
21.189 | ("failure", _) => raise ERROR "sys-raise ERROR"
21.190 | _ => raise ERROR "me: uncovered case Step.by_tactic"
21.191
21.192 - val ("helpless", ([(*\<Or> should contain tac \<Or>*)], [], _)) = (*case*)
21.193 + val ("ok", ([(Add_Find "solutions L", _, _)], [], _)) = (*case*)
21.194 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
21.195 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
21.196 (*if*) Pos.on_calc_end ip (*else*);
21.197 @@ -391,7 +550,7 @@
21.198 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
21.199 (*if*) Pos.on_specification ([], state_pos) (*then*);
21.200
21.201 - val ("failure", ([], [], _)) =
21.202 + val ("ok", ([(Add_Find "solutions L", _, _)], [], _)) =
21.203 specify_do_next (pt, input_pos);
21.204 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
21.205 val (_, (p_', tac)) =
21.206 @@ -405,21 +564,19 @@
21.207 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
21.208 (*if*) p_ = Pos.Pbl (*then*);
21.209
21.210 - val ("dummy", (Pbl, Refine_Problem ["sqroot-test", "univariate", "equation", "test"])) =
21.211 + val ("dummy", (Pbl, Add_Find "solutions L")) =
21.212 for_problem ctxt oris (o_refs, refs) (pbl, met);
21.213 "~~~~~ fun for_problem , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
21.214 (oris, (o_refs, refs), (pbl, met));
21.215 - val cdI = if dI = ThyC.id_empty then dI' else dI;
21.216 - val ctxt = Proof_Context.init_global (ThyC.get_theory @{context} cdI)
21.217 val cpI = if pI = Problem.id_empty then pI' else pI;
21.218 val cmI = if mI = MethodC.id_empty then mI' else mI;
21.219 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
21.220 val {model = mpc, ...} = MethodC.from_store ctxt cmI
21.221 - val (preok, (*+*)xxxxx(*+*) ) = Pre_Conds.check ctxt where_rls where_ pbl 0;
21.222 + val (preok, _) = Pre_Conds.check_OLD ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
21.223 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
21.224 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
21.225 val NONE = (*case*) find_first (I_Model.is_error o #5) pbl (*of*);
21.226 - val NONE = (*case*)
21.227 + val SOME ("#Find", "solutions L") = (*case*)
21.228 item_to_add (ThyC.get_theory @{context} (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);
21.229 (*if*) not preok (*then*);
21.230
21.231 @@ -435,27 +592,28 @@
21.232
21.233 (*-------------------- contiue step into specify_do_next ------------------------------------*)
21.234 val ist_ctxt = Ctree.get_loc pt (p, p_)
21.235 - val Refine_Problem ["sqroot-test", "univariate", "equation", "test"] =
21.236 +val Add_Find "solutions L" =
21.237 (*case*) tac (*of*);
21.238 - val ("failure", ([(*\<Or> should contain tac \<Or>*)], [], _)) =
21.239 +
21.240 + val ("ok", ([(Add_Find "solutions L", _, _)], [], _)) =
21.241 Step_Specify.by_tactic_input tac (pt, (p, p_'));
21.242 -"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Refine_Problem pI), (ptp as (pt, pos as (p,_)))) =
21.243 +"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Find ct), (ptp as (pt, pos as (p,_)))) =
21.244 (tac, (pt, (p, p_')));
21.245 - val (dI, dI', probl, ctxt) = case get_obj I pt p of
21.246 - PblObj {origin= (_, (dI, _, _), _), spec = (dI', _, _), probl, ctxt, ...} =>
21.247 - (dI, dI', probl, ctxt)
21.248 - val thy = if dI' = ThyC.id_empty then dI else dI'
21.249
21.250 - val NONE = (*case*) (*------------------------------- vvv*)
21.251 - Refine.problem (ThyC.get_theory @{context} thy) pI probl (*of*);
21.252 -"~~~~~ fun problem , args:"; val (thy, pblID, itms) = ((ThyC.get_theory @{context} thy), pI, probl);
21.253 -(* val SOME (Refine.Match_ (["sqroot-test", "univariate", "equation", "test"], _)) =*)
21.254 - val NONE = (*case*)
21.255 - Refine.refined_ ((Store.apply (get_pbls ())) (Refine.refin'' thy ((rev o tl) pblID) itms []) pblID (rev pblID)) (*of*);
21.256 -(*return from problem*);
21.257 + Specify.by_Add_ "#Find" ct ptp;
21.258 +"~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) =
21.259 + ("#Find", ct, ptp);
21.260 (*-------------------- stop step into -------------------------------------------------------*)
21.261 -val (p,f,nxt,pt) = (p''''',f''''',nxt''''',pt''''');
21.262 +val (p,f,nxt,pt) = (p''''',f''''',nxt''''',pt'''''); val Add_Find "solutions L" = nxt;
21.263 (*\------------------- step into me Add_Find "solutions L" ---------------------------------/*)
21.264 +(*
21.265 + WN230814
21.266 + repaired 'step into me Add_Find "solutions L"' above (ERROR was Tactic.Refine);
21.267 + But with the repair the subsequent steps repeatedly led to Add_Find "solutions L" --
21.268 + -- which was NOT repaird, too.
21.269 + So we kept the old test code below, because it leads to the correct result "[x = 2]".
21.270 +
21.271 +---------------------- old test code from before above repair -------------------------------
21.272
21.273 (*=== refine problem -----vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
21.274 val nxt = (Refine_Problem ["univariate", "equation", "test"]);
21.275 @@ -511,6 +669,7 @@
21.276 then case nxt of End_Proof' => ()
21.277 | _ => error "new behaviour in test:refine.sml:miniscript with mini-subpb 1"
21.278 else error "new behaviour in test:refine.sml:miniscript with mini-subpb 2"
21.279 +*)
21.280
21.281 "----------- equation with CalcTree [ = 6 / 5] for timing: with/out adapt_to_type --------------";
21.282 "----------- equation with CalcTree [ = 6 / 5] for timing: with/out adapt_to_type --------------";
21.283 @@ -551,4 +710,4 @@
21.284 *** pass ["equation", "univariate", "polynomial", "degree_3"]
21.285 *** pass ["equation", "univariate", "polynomial", "degree_4"]
21.286 *** pass ["equation", "univariate", "polynomial", "normalise"]
21.287 -*)
21.288 \ No newline at end of file
21.289 +*)
22.1 --- a/test/Tools/isac/Specify/specify.sml Fri Aug 04 23:07:04 2023 +0200
22.2 +++ b/test/Tools/isac/Specify/specify.sml Tue Aug 15 12:22:49 2023 +0200
22.3 @@ -89,15 +89,21 @@
22.4 "errorBound (eps=(0::real))"],
22.5 ("Diff_App", ["maximum_of", "function"], ["Diff_App", "max_by_calculus"]))];
22.6 (*** stepwise Specification: Problem model================================================= ***)
22.7 - val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "fixedValues [r = Arbfix]"*)
22.8 - val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "maximum A"*)
22.9 - val (p,_,f,nxt,_,pt) = me nxt p c pt; (*Add_Find "valuesFor [a]"*)
22.10 - val (p,_,f,nxt,_,pt) = me nxt p c pt; (*Add_Find "valuesFor [b]"*)
22.11 - val (p,_,f,nxt,_,pt) = me nxt p c pt; (*Add_Relation "relations [A = a * b]"*)
22.12 - val (p,_,f,nxt,_,pt) = me nxt p c pt; (*Add_Relation "relations [(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]"*)
22.13 - val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Diff_App"*)
22.14 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "fixedValues [r = Arbfix]" = nxt
22.15 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "maximum A" = nxt
22.16 +(*/---broken elementwise input to lists---\* )
22.17 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "valuesFor [a]" = nxt
22.18 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "valuesFor [b]" = nxt
22.19 +( *\---broken elementwise input to lists---/*)
22.20 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "valuesFor [a, b]" = nxt
22.21 +(*/---broken elementwise input to lists---\* )
22.22 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "relations [A = a * b]" = nxt
22.23 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "relations [(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]" = nxt
22.24 +( *\---broken elementwise input to lists---/*)
22.25 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]" = nxt
22.26 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Diff_App" = nxt
22.27
22.28 -(*** Problem model is complete ============================================================ ***)
22.29 +(*/------------------- directly to Problem model is complete --------------------------------\*)
22.30 val thy = @{theory "Diff_App"};
22.31 val ctxt = Proof_Context.init_global thy;
22.32 val (o_model, _, _) = get_obj g_origin pt (fst p);
22.33 @@ -135,20 +141,22 @@
22.34 "(3 ,[1, 2, 3] ,true ,#Find ,Cor valuesFor [a, b] ,(v_s, [[a, b]])), \n" ^
22.35 "(4 ,[1, 2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] ,(r_s, [[A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])), \n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_v, [a])), \n(9 ,[1, 2] ,true ,#undef ,Cor interval {x. 0 \<le> x \<and> x \<le> 2 * r} ,(i_tv, [{x. 0 \<le> x \<and> x \<le> 2 * r}])), \n(11 ,[1, 2, 3] ,true ,#undef ,Cor errorBound (eps = 0) ,(e_rr, [eps = 0]))]"
22.36 then () else error "completetest.sml: new behav. in I_Model.complete 1";
22.37 -(*** MethodC model has a copy of Problem ================================================== ***)
22.38 +(*\------------------- directly to Problem model is complete --------------------------------/*)
22.39
22.40 - val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["maximum_of", "function"]*)
22.41 - val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Method ["Diff_App", "max_by_calculus"]*)
22.42 +(*/------------------- MethodC model has a copy of Problem ----------------------------------\*)
22.43 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["maximum_of", "function"] = nxt
22.44 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["Diff_App", "max_by_calculus"] = nxt
22.45 +(*\------------------- MethodC model has a copy of Problem ----------------------------------/*)
22.46
22.47 -(*** stepwise Specification: MethodC model ================================================ ***)
22.48 - val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "boundVariable a"*)
22.49 - val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "interval {x. 0 \<le> x \<and> x \<le> 2 * r}"*)
22.50 - val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "errorBound (eps = 0)"*)
22.51 +(*/------------------- stepwise Specification: MethodC model --------------------------------\*)
22.52 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "boundVariable a" = nxt
22.53 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "interval {x. 0 \<le> x \<and> x \<le> 2 * r}" = nxt
22.54 + val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "errorBound (eps = 0)" = nxt;
22.55 (*** MethodC model is complete ============================================================ ***)
22.56 -(*val (p,_,f,nxt,_,pt) = me nxt p c pt; ( *exception TERM raised (line 359 of "term.ML"):
22.57 +(** )val (p,_,f,nxt,_,pt) = me nxt p c pt; (*exception TERM raised (line 359 of "term.ML"):
22.58 fastype_of: Bound
22.59 - B.0*)
22.60 -(*** Specification of Problem and MethodC model is complete, Solution starts ============== ***)
22.61 + B.0 *)( **)
22.62 +(*\------------------ Specification of Problem and MethodC model is complete, Solution starts/*)
22.63
22.64
22.65 "----------- revise Specify.do_all -------------------------------------------------------------";
22.66 @@ -291,7 +299,9 @@
22.67 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "Streckenlast q_0"*)
22.68 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "Biegelinie y"*)
22.69 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)
22.70 +(*/---broken elementwise input to lists---\* )
22.71 (*[], 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]"*)
22.72 +( *\---broken elementwise input to lists---/*)
22.73 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Theory "Biegelinie"*)
22.74 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Problem ["Biegelinien"]*)
22.75 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*)
22.76 @@ -979,19 +989,19 @@
22.77 (*-------------------- stop step into me\<rightarrow>Add_Given "Biegelinie y" --------------------------*)
22.78 (*\------------------- step into me\<rightarrow>Add_Given "Biegelinie y" ||||||||||||||||||||||||||||||/*)
22.79
22.80 -(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*\<rightarrow>Add_Given "AbleitungBiegelinie dy"*)
22.81 -(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Apply_Method ["Biegelinien", "ausBelastung"]*)
22.82 -(*[1, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Rewrite ("sym_neg_equal_iff_equal", "(?a1 = ?b1) = (- ?a1 = - ?b1)")*)
22.83 -(*[1, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Rewrite ("Belastung_Querkraft", "- qq ?x = Q' ?x")*)
22.84 -(*[1, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Subproblem ("Biegelinie", ["named", "integrate", "function"])*)
22.85 -(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Model_Problem*)
22.86 -(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "functionTerm (- q_0)"*)
22.87 -(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "integrateBy x"*)
22.88 -
22.89 +(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; val Add_Given "AbleitungBiegelinie dy"= nxt
22.90 +(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["Biegelinien", "ausBelastung"]= nxt
22.91 +(*[1, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("sym_neg_equal_iff_equal", _)= nxt
22.92 +(*[1, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("Belastung_Querkraft", _)= nxt
22.93 +(*[1, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["named", "integrate", "function"])= nxt
22.94 +(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Model_Problem= nxt
22.95 +(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Given "functionTerm (- q_0)"= nxt
22.96 +(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Given "integrateBy x"= nxt
22.97 +;
22.98 (*/------------------- check result of Add_Given "functionTerm (- q_0)" --------------------\*)
22.99 if p = ([1, 3], Pbl) andalso
22.100 f = Test_Out.PpcKF (Test_Out.Problem [], {Find = [Incompl "antiDerivativeName"],
22.101 - Given = [Incompl "integrateBy", Correct "functionTerm (- q_0)"],
22.102 + Given = [Correct "functionTerm (- q_0)", Incompl "integrateBy"],
22.103 Relate = [], Where = [], With = []})
22.104 then
22.105 (case nxt of Add_Given "integrateBy x" => () | _ => error "specify-phase: low level CHANGED 1")
23.1 --- a/test/Tools/isac/Specify/sub-problem.sml Fri Aug 04 23:07:04 2023 +0200
23.2 +++ b/test/Tools/isac/Specify/sub-problem.sml Tue Aug 15 12:22:49 2023 +0200
23.3 @@ -25,7 +25,8 @@
23.4 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))]
23.5
23.6 val (tac as Model_Problem (*["vonBelastungZu", "Biegelinien"]*), (pt, p as ([1], Pbl))) =
23.7 - (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
23.8 + (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
23.9 + (*---broken elementwise input to lists---* ) |> me'( *---broken elementwise input to lists---*)
23.10 (*INVISIBLE: SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''])*)
23.11 |> me';
23.12
24.1 --- a/test/Tools/isac/Test_Isac_Short.thy Fri Aug 04 23:07:04 2023 +0200
24.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Tue Aug 15 12:22:49 2023 +0200
24.3 @@ -142,31 +142,22 @@
24.4 "~~~~~ and xxx , args:"; val () = ();
24.5 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
24.6 "~~~~~ continue fun xxx"; val () = ();
24.7 -(*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
24.8 +(*if*) (*then*); (*else*); (*andalso*) (*case*) (*of*); (*return value*); (*in*) (*end*);
24.9 "xx"
24.10 ^ "xxx" (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)
24.11 -\<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)
24.12 - (*//----------------- adhoc inserted n ----------------------------------------------------\\*)
24.13 -(*\\------------------ adhoc inserted n ----------------------------------------------------//*)
24.14 -\<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)
24.15 -
24.16 +\<close> ML \<open> (*//----------- build fun XXXXX -----------------------------------------------------\\*)
24.17 +(*//------------------ build fun XXXXX -----------------------------------------------------\\*)
24.18 +(*\\------------------ build fun XXXXX -----------------------------------------------------//*)
24.19 +\<close> ML \<open> (*\\----------- build fun XXXXX -----------------------------------------------------//*)
24.20 +val return_XXXXX = "XXXXX"
24.21 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
24.22 (*//------------------ step into XXXXX -----------------------------------------------------\\*)
24.23 -(*keep for continuing YYYYY*)
24.24 -\<close> ML \<open> (*------------- continuing XXXXX ------------------------------------------------------*)
24.25 -(*-------------------- continuing XXXXX ------------------------------------------------------*)
24.26 -(*kept for continuing XXXXX*)
24.27 -(*-------------------- stop step into XXXXX --------------------------------------------------*)
24.28 -\<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*)
24.29 +\<close> ML \<open> (*||----------- contine XXXXX ---------------------------------------------------------*)
24.30 +(*||------------------ contine XXXXX ---------------------------------------------------------*)
24.31 (*\\------------------ step into XXXXX -----------------------------------------------------//*)
24.32 \<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)
24.33 +val "XXXXX" = return_XXXXX;
24.34
24.35 -(*/------------------- check entry to XXXXX -------------------------------------------------\*)
24.36 -(*\------------------- check entry to XXXXX -------------------------------------------------/*)
24.37 -(*/------------------- check within XXXXX ---------------------------------------------------\*)
24.38 -(*\------------------- check within XXXXX ---------------------------------------------------/*)
24.39 -(*/------------------- check result of XXXXX ------------------------------------------------\*)
24.40 -(*\------------------- check result of XXXXX ------------------------------------------------/*)
24.41 (* final test ... ----------------------------------------------------------------------------*)
24.42
24.43 \<close> ML \<open> (*//----------- inserted hidden code ------------------------------------------------\\*)
24.44 @@ -174,10 +165,6 @@
24.45 (*\\------------------ inserted hidden code ------------------------------------------------//*)
24.46 \<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)
24.47
24.48 -\<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*)
24.49 -(*//------------------ build new fun XXXXX -------------------------------------------------\\*)
24.50 -(*\\------------------ build new fun XXXXX -------------------------------------------------//*)
24.51 -\<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*)
24.52 \<close>
24.53 ML \<open>
24.54 \<close> ML \<open>
24.55 @@ -269,7 +256,7 @@
24.56
24.57 ML_file "Specify/formalise.sml"
24.58 ML_file "Specify/o-model.sml"
24.59 - ML_file "Specify/i-model.sml"
24.60 + ML_file "Specify/i-model.sml" (* (BROKEN!) test on elementwise input to lists*)
24.61 ML_file "Specify/pre-conditions.sml"
24.62 ML_file "Specify/p-model.sml"
24.63 ML_file "Specify/m-match.sml"
24.64 @@ -325,7 +312,7 @@
24.65 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
24.66 (*ML_file "Knowledge/rateq.sml" some complicated equations not recovered----Test_Isac_Short*)
24.67 ML_file "Knowledge/rootrat.sml"
24.68 - ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
24.69 + ML_file "Knowledge/rootrateq.sml"(*one complicated equations not recovered from 2002 *)
24.70 (*ML_file "Knowledge/partial_fractions.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*)
24.71 ML_file "Knowledge/polyeq-1.sml"
24.72 (*ML_file "Knowledge/polyeq-2.sml" Test_Isac_Short*)
24.73 @@ -790,7 +777,11 @@
24.74 Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS;
24.75 see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial.
24.76 \<close>
24.77 -
24.78 +ML \<open>
24.79 +\<close> ML \<open>
24.80 +\<close> ML \<open>
24.81 +\<close> ML \<open>
24.82 +\<close>
24.83 end
24.84 (*========== inhibit exn 130719 Isabelle2013 ===================================
24.85 ============ inhibit exn 130719 Isabelle2013 =================================*)
25.1 --- a/test/Tools/isac/Test_Some.thy Fri Aug 04 23:07:04 2023 +0200
25.2 +++ b/test/Tools/isac/Test_Some.thy Tue Aug 15 12:22:49 2023 +0200
25.3 @@ -121,10 +121,413 @@
25.4 \<close>
25.5
25.6 section \<open>===================================================================================\<close>
25.7 -section \<open>===== ============================================================================\<close>
25.8 +section \<open>===== Interpret/li-tool.sml =======================================================\<close>
25.9 ML \<open>
25.10 \<close> ML \<open>
25.11 +(* Title: Interpret/li-tool.sml
25.12 + Author: Walther Neuper 050908
25.13 + (c) copyright due to lincense terms.
25.14 +*)
25.15 +"-----------------------------------------------------------------";
25.16 +"table of contents -----------------------------------------------";
25.17 +"-----------------------------------------------------------------";
25.18 +"----------- fun implicit_take, fun get_first_argument -------------------------";
25.19 +"----------- fun from_prog ---------------------------------------";
25.20 +"----------- fun specific_from_prog ----------------------------";
25.21 +"----------- fun de_esc_underscore -------------------------------";
25.22 +"----------- fun go ----------------------------------------------";
25.23 +"----------- fun formal_args -------------------------------------";
25.24 +"----------- fun dsc_valT ----------------------------------------";
25.25 +"----------- fun arguments_from_model ---------------------------------------";
25.26 +"----------- fun init_pstate -----------------------------------------------------------------";
25.27 +"-----------------------------------------------------------------";
25.28 +"-----------------------------------------------------------------";
25.29 +"-----------------------------------------------------------------";
25.30 +
25.31 +val thy = @{theory Isac_Knowledge};
25.32 +
25.33 \<close> ML \<open>
25.34 +"----------- fun init_pstate -----------------------------------------------------------------";
25.35 +"----------- fun init_pstate -----------------------------------------------------------------";
25.36 +"----------- fun init_pstate -----------------------------------------------------------------";
25.37 +(*
25.38 + This test is deeply nested (down into details of creating environments).
25.39 + In order to make Sidekick show the structure add to each
25.40 + * (*/...\*) and (*\.../*)
25.41 + * a companion > ML < (*/...\*) and > ML < (*\.../*)
25.42 + Note the wrong ^----^ delimiters.
25.43 +*)
25.44 +val fmz = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
25.45 + "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
25.46 + "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
25.47 + "AbleitungBiegelinie dy"];
25.48 +val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
25.49 + ["IntegrierenUndKonstanteBestimmen2"]);
25.50 +val p = e_pos'; val c = [];
25.51 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))]; val Model_Problem = nxt
25.52 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Traegerlaenge L" = nxt
25.53 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Streckenlast q_0" = nxt
25.54 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Biegelinie y" = nxt
25.55 +\<close> ML \<open>
25.56 +(*/---broken elementwise input to lists---\* )
25.57 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)
25.58 + (*isa* ) val Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" = nxt
25.59 + ( *isa2*) val Add_Relation "Randbedingungen [y 0 = 0]" = nxt
25.60 +(*[], 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]"*)
25.61 + (*isa*) val Specify_Theory "Biegelinie" = nxt
25.62 + (*isa2* ) val Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]" = nxt( **)
25.63 +( *\---broken elementwise input to lists---/*)
25.64 +\<close> ML \<open>
25.65 +(*[], 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
25.66 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
25.67 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["Biegelinien"] = nxt
25.68 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
25.69 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "FunktionsVariable x" = nxt
25.70 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]" = nxt
25.71 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy" = nxt
25.72 +
25.73 +\<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)
25.74 +(*[], Met*)val return_Add_Given_AbleitungBieg
25.75 + = me nxt p c pt;
25.76 +\<close> ML \<open> (*/------------ step into me_Add_Given_AbleitungBieg --------------------------------\\*)
25.77 +(*/------------------- step into me_Add_Given_AbleitungBieg --------------------------------\\*)
25.78 +
25.79 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
25.80 + val ctxt = Ctree.get_ctxt pt p
25.81 +val ("ok", (_, _, ptp as (pt, p))) =
25.82 + (*case*) Step.by_tactic tac (pt, p) (*of*);
25.83 +
25.84 +\<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)
25.85 + (*case*)
25.86 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
25.87 +\<close> ML \<open>
25.88 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
25.89 + (p, ((pt, Pos.e_pos'), []) );
25.90 + (*if*) Pos.on_calc_end ip (*else*);
25.91 + val (_, probl_id, _) = Calc.references (pt, p);
25.92 +val _ =
25.93 + (*case*) tacis (*of*);
25.94 + (*if*) probl_id = Problem.id_empty (*else*);
25.95 +
25.96 +\<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)
25.97 + switch_specify_solve p_ (pt, ip);
25.98 +\<close> ML \<open>
25.99 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
25.100 + (*if*) Pos.on_specification ([], state_pos) (*then*);
25.101 +
25.102 +\<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)
25.103 + specify_do_next (pt, input_pos);
25.104 +\<close> ML \<open>
25.105 +"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
25.106 + val (_, (p_', tac)) = Specify.find_next_step ptp
25.107 + val ist_ctxt = Ctree.get_loc pt (p, p_)
25.108 +val Tactic.Apply_Method mI =
25.109 + (*case*) tac (*of*);
25.110 +
25.111 +\<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)
25.112 + LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
25.113 + ist_ctxt (pt, (p, p_'));
25.114 +\<close> ML \<open>
25.115 +"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
25.116 + ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));
25.117 + val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)
25.118 + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
25.119 + | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
25.120 + val {model, ...} = MethodC.from_store ctxt mI;
25.121 + val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
25.122 +;
25.123 +(*+*)if (itms |> I_Model.to_string @{context}) = "[\n" ^
25.124 + "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^
25.125 + "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
25.126 + "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^
25.127 + "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]])), \n" ^
25.128 + "(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(fun_var, [x])), \n" ^
25.129 + "(6 ,[1] ,true ,#Given ,Cor GleichungsVariablen [c, c_2, c_3, c_4] ,(vs, [[c, c_2, c_3, c_4]])), \n" ^
25.130 + "(7 ,[1] ,true ,#Given ,Cor AbleitungBiegelinie dy ,(id_der, [dy]))]"
25.131 +(*+*)then () else error "init_pstate: initial i_model changed";
25.132 +(*+*)if (itms |> I_Model.penv_to_string @{context}) = "[" ^ (*to be eliminated*)
25.133 +(*1*)"(l_l, [L]), " ^
25.134 +(*2*)"(q_q, [q_0]), " ^
25.135 +(*3*)"(b_b, [y]), " ^
25.136 +(*4*)"(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]), " ^
25.137 +(*5*)"(fun_var, [x]), " ^
25.138 +(*6*)"(vs, [[c, c_2, c_3, c_4]]), " ^
25.139 +(*7*)"(id_der, [dy])]"
25.140 +(*+*)then () else error "init_pstate: initial penv changed";
25.141 +
25.142 +\<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)
25.143 + (*case*)
25.144 + LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI (*of*);
25.145 +\<close> ML \<open>(*//------------ step into init_pstate -----------------------------------------------\\*)
25.146 +(*//------------------ step into init_pstate -----------------------------------------------\\*)
25.147 +"~~~~~ fun init_pstate , args:"; val (ctxt, i_model, met_id) = (ctxt, (I_Model.OLD_to_TEST itms), mI);
25.148 + val (model_patt, program, prog, prog_rls, where_, where_rls) =
25.149 + case MethodC.from_store ctxt met_id of
25.150 + {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...}=>
25.151 + (model_patt, program, prog, prog_rls, where_, where_rls)
25.152 +
25.153 +\<close> ML \<open>
25.154 + val return_of_max_variant =
25.155 + I_Model.of_max_variant model_patt i_model;
25.156 +\<close> ML \<open>(*///----------- step into of_max_variant --------------------------------------------\\*)
25.157 +(*///----------------- step into of_max_variant --------------------------------------------\\*)
25.158 +"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
25.159 + val all_variants =
25.160 + map (fn (_, variants, _, _, _) => variants) i_model
25.161 + |> flat
25.162 + |> distinct op =
25.163 + val variants_separated = map (filter_variants' i_model) all_variants
25.164 + val sums_corr = map (cnt_corrects) variants_separated
25.165 + val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
25.166 + val (_, max_variant) = hd (*..crude decision, up to improvement *)
25.167 + (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
25.168 + val i_model_max =
25.169 + filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
25.170 + val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
25.171 +;
25.172 +(*+*)if (equal_descr_pairs |> descr_pairs_to_string @{context}) = "[" ^
25.173 +(*defined: in program+model--vvvv--,----------------------------------------- in problem ---vvv*)
25.174 + "((#Given, (Traegerlaenge, l_l)), (1, [1], true ,#Given, " ^ "(Cor_TEST Traegerlaenge L ,(l_l, [L]), Position.T))), " ^
25.175 + "((#Given, (Streckenlast, q_q)), (2, [1], true ,#Given, " ^
25.176 + "(Cor_TEST Streckenlast q_0 ,(q_q, [q_0]), Position.T))), " ^
25.177 + "((#Given, (FunktionsVariable, fun_var)), (5, [1], true ,#Given, " ^
25.178 + "(Cor_TEST FunktionsVariable x ,(fun_var, [x]), Position.T))), " ^
25.179 + "((#Given, (GleichungsVariablen, vs)), (6, [1], true ,#Given, " ^
25.180 + "(Cor_TEST GleichungsVariablen [c, c_2, c_3, c_4] ,(vs, [[c, c_2, c_3, c_4]]), Position.T))), " ^
25.181 + "((#Given, (AbleitungBiegelinie, id_der)), (7, [1], true ,#Given, " ^
25.182 + "(Cor_TEST AbleitungBiegelinie dy ,(id_der, [dy]), Position.T))), " ^
25.183 + "((#Find, (Biegelinie, b_b)), (3, [1], true ,#Find, (Cor_TEST Biegelinie y ,(b_b, [y]), Position.T))), " ^
25.184 + "((#Relate, (Randbedingungen, r_b)), (4, [1], true ,#Relate, " ^
25.185 + "(Cor_TEST Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]), Position.T)))]"
25.186 +then () else error "of_max_variant: equal_descr_pairs CHANGED";
25.187 +(*/////############### old test code ##################################################\\\\\\* )
25.188 +
25.189 + val env_subst =
25.190 + mk_env_subst_DEL equal_descr_pairs;
25.191 +(*/------------------- ERRORs to remove in CS subsequent to "prepare 1 PIDE turn 11"-000----\* )
25.192 +(*+*)if ( env_subst |> Subst.to_string @{context}) = "[\"\n" ^
25.193 +(*ERRORs------^^^^^^^^^----------isa2: penv ---vvv----------------------..isa2, thus "correct"*)
25.194 +(*1*)"(l_l, L)\", \"\n" ^ (* (l_l, [L]) *)
25.195 +(*2*)"(q_q, q_0)\", \"\n" ^ (* (q_q, [q_0]) *)
25.196 +(*3*)"(fun_var, x)\", \"\n" ^ (* (fun_var, [x]) *)
25.197 +(*4*)"(vs, GleichungsVariablen)\", \"\n" ^ (* (vs, [[c, c_2, c_3, c_4]]) *)
25.198 +(*5*)"(id_der, dy)\", \"\n" ^ (* (id_der, [dy]) *)
25.199 +(*6*)"(b_b, y)\"]" (* (b_b, [y]) *)
25.200 +(*7 missing*) (* (r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]) *)
25.201 +(*+*)then () else error "of_max_variant: env_subst BETTER ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? "
25.202 +( *\------------------- ERRORs to remove ..--------------------------------------------------/*)
25.203 +
25.204 +(*///----------------- step into mk_env_subst_DEL ------------------------------------------\\*)
25.205 +"~~~~~ fun mk_env_subst_DEL , args:"; val (equal_descr_pairs) = (equal_descr_pairs);
25.206 +
25.207 +(*///################# nth 1 equal_descr_pairs ############################################=\\*)
25.208 + val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
25.209 + => (Pre_Conds.discern_feedback_subst id feedb) (*|> map fst (*rhs dropped*)|> map (pair id)*) ) (nth 1 equal_descr_pairs);
25.210 +"~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 1 equal_descr_pairs);
25.211 +(*--------------------------------------------------------------------------^^^----------------*)
25.212 +
25.213 + Pre_Conds.discern_feedback_subst id feedb;
25.214 +"~~~~~ fun discern_feedback_subst , args:"; val (id, Cor_TEST ((descr, [ts]), _)) = (id, feedb);
25.215 + (*if*) TermC.is_list ts (*else*);
25.216 + val ts = [ts]
25.217 +;
25.218 + Pre_Conds.discern_type_subst (descr, id) ts;
25.219 +"~~~~~ fun discern_type_subst , args:"; val ((descr, id), ts) = ((descr, id), ts);
25.220 +val _(*"real \<Rightarrow> una"*) =
25.221 + (*case*) type_of descr (*of*);
25.222 +val return_discern_type_subst_1 = [(id, Library.the_single ts)]
25.223 +(*\\\################# nth 1 equal_descr_pairs ############################################=//*)
25.224 +
25.225 +(*///################# nth 4 equal_descr_pairs ############################################=\\*)
25.226 + val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
25.227 + => (discern_feedback_subst id feedb) (*|> map fst (*rhs dropped*)|> map (pair id)*) ) (nth 1 equal_descr_pairs);
25.228 +"~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 4 equal_descr_pairs);
25.229 +(*--------------------------------------------------------------------------^^^----------------*)
25.230 +
25.231 + Pre_Conds.discern_feedback_subst id feedb;
25.232 +"~~~~~ fun discern_feedback_subst , args:"; val (id, Cor_TEST ((descr, (*[*)ts(*]*)), _)) = (id, feedb);
25.233 +(*+*)val (Free ("vs", _), "[[c], [c_2], [c_3], [c_4]]")
25.234 + = (id, ts |> UnparseC.terms @{context});
25.235 +
25.236 + (*if*) fold (curry and_) (map TermC.is_list ts) true (*then*);
25.237 + val ts = ts;
25.238 +
25.239 + discern_type_subst (descr, id) ts;
25.240 +"~~~~~ fun discern_type_subst , args:"; val ((descr, id), ts) = ((descr, id), ts);
25.241 +val (Type ("fun", [Type ("List.list", [Type ("Real.real", [])]), _])) =
25.242 + (*case*) type_of descr (*of*);
25.243 + (*if*) TermC.is_list (hd ts) (*then*);
25.244 +
25.245 +val return_discern_type_subst_4 =
25.246 +(* if TermC.is_list (hd ts)
25.247 + then*) [(id, ts |> map TermC.the_single |> TermC.list2isalist HOLogic.realT)]
25.248 +(* else []*)
25.249 +(*+*)val "[\"\n(vs, [c, c_2, c_3, c_4])\"]"
25.250 + = return_discern_type_subst_4 |> Subst.to_string @{context}
25.251 +
25.252 +(*-------------------- contine discern_feedback_subst ----------------------------------------*)
25.253 +val return_discern_feedback_subst_4 = return_discern_type_subst_4
25.254 +(*-------------------- contine mk_env_subst_DEL ----------------------------------------------*)
25.255 +val return_mk_env_subst_DEL_4 = return_discern_feedback_subst_4
25.256 +(*+*)val "[\"\n(vs, [c, c_2, c_3, c_4])\"]"
25.257 + = return_mk_env_subst_DEL_4 |> Subst.to_string @{context}
25.258 +(*\\\################# nth 4 equal_descr_pairs ############################################=//*)
25.259 +
25.260 +(*///################# nth 7 equal_descr_pairs ############################################=\\*)
25.261 + val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
25.262 + => (discern_feedback_subst id feedb) (*|> map fst (*rhs dropped*)|> map (pair id)*) ) (nth 7 equal_descr_pairs);
25.263 +"~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 7 equal_descr_pairs);
25.264 +(*--------------------------------------------------------------------------^^^----------------*)
25.265 +
25.266 + Pre_Conds.discern_feedback_subst id feedb;
25.267 +"~~~~~ fun discern_feedback_subst , args:"; val (id, Cor_TEST ((descr, (*[*)ts(*]*)), _)) = (id, feedb);
25.268 +(*+*)val (Free ("r_b", _), "[[y 0 = 0], [y L = 0], [M_b 0 = 0], [M_b L = 0]]")
25.269 + = (id, ts |> UnparseC.terms @{context});
25.270 +
25.271 + (*if*) fold (curry and_) (map TermC.is_list ts) true (*then*);
25.272 + val ts = ts;
25.273 +
25.274 + discern_type_subst (descr, id) ts;
25.275 +"~~~~~ fun discern_type_subst , args:"; val ((descr, id), ts) = ((descr, id), ts);
25.276 +val (Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) =
25.277 + (*case*) type_of descr (*of*);
25.278 + (*if*) TermC.is_list (hd ts) (*then*);
25.279 +
25.280 +val return_discern_type_subst_7 =
25.281 +(* if TermC.is_list (hd ts)
25.282 + then*) [(id, ts |> map TermC.the_single |> TermC.list2isalist HOLogic.boolT)]
25.283 +(* else []*)
25.284 +(*+*)val "[\"\n(r_b, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\"]"
25.285 + = return_discern_type_subst_7 |> Subst.to_string @{context}
25.286 +
25.287 +(*-------------------- contine discern_feedback_subst ----------------------------------------*)
25.288 +val return_discern_feedback_subst_7 = return_discern_type_subst_7
25.289 +(*-------------------- contine mk_env_subst_DEL ----------------------------------------------*)
25.290 +val return_mk_env_subst_DEL_7 = return_discern_type_subst_7
25.291 +(*+*)val "[\"\n(r_b, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\"]"
25.292 + = return_mk_env_subst_DEL_7 |> Subst.to_string @{context};
25.293 +(*\\\################# nth 7 equal_descr_pairs ############################################=//*)
25.294 +
25.295 +(*BEFORE correct (vs, [c, c_2, c_3, c_4])* )
25.296 +(*+*)val "[\"\n(l_l, L)\", \"\n(q_q, q_0)\", \"\n(fun_var, x)\", \"\n(vs, vs)\", \"\n(id_der, dy)\", \"\n(b_b, y)\"]"
25.297 +(*ERRORs still -----------------------------------------------------------^^^-------------------------------------, r_b*)
25.298 + = (env_subst |> Subst.to_string @{context})
25.299 +*)
25.300 +(*NOW only nth 7 is missing.. (but mk_env_eval_DEL completely broken)* )
25.301 +(*+*)val "[\"\n(l_l, L)\", \"\n(q_q, q_0)\", \"\n(fun_var, x)\", \"\n(vs, [c, c_2, c_3, c_4])\", \"\n(id_der, dy)\", \"\n(b_b, y)\"]"
25.302 +(*ERRORs still ---------------------------------------------------------------------------------------------------------------------, r_b*)
25.303 + = (env_subst |> Subst.to_string @ {context})
25.304 +*)
25.305 +(*+*)if (env_subst |> Subst.to_string @{context}) = "[\"\n" ^
25.306 +(*1*)"(l_l, L)\", \"\n" ^
25.307 +(*2*)"(q_q, q_0)\", \"\n" ^
25.308 +(*3*)"(fun_var, x)\", \"\n" ^
25.309 +(*4*)"(vs, [c, c_2, c_3, c_4])\", \"\n" ^
25.310 +(*5*)"(id_der, dy)\", \"\n" ^
25.311 +(*6*)"(b_b, y)\", \"\n" ^
25.312 +(*7*)"(r_b, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\"]"
25.313 +(*+*)then () else error "env_subst CHANGED";
25.314 +
25.315 +
25.316 +(*+*)if (i_model_max |> I_Model.to_string_TEST @{context}) = "[\n" ^
25.317 + "(1, [1], true ,#Given, (Cor_TEST Traegerlaenge L ,(l_l, [L]), Position.T)), \n" ^
25.318 + "(2, [1], true ,#Given, (Cor_TEST Streckenlast q_0 ,(q_q, [q_0]), Position.T)), \n" ^
25.319 + "(3, [1], true ,#Find, (Cor_TEST Biegelinie y ,(b_b, [y]), Position.T)), \n" ^
25.320 + "(4, [1], true ,#Relate, (Cor_TEST Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]), Position.T)), \n" ^
25.321 + "(5, [1], true ,#Given, (Cor_TEST FunktionsVariable x ,(fun_var, [x]), Position.T)), \n" ^
25.322 + "(6, [1], true ,#Given, (Cor_TEST GleichungsVariablen [c, c_2, c_3, c_4] ,(vs, [[c, c_2, c_3, c_4]]), Position.T)), \n" ^
25.323 + "(7, [1], true ,#Given, (Cor_TEST AbleitungBiegelinie dy ,(id_der, [dy]), Position.T))]"
25.324 +(*+*)then () else error "i_model_max CHANGED";
25.325 +
25.326 +(*||------------------ continue of_max_variant ---------------------------------------------\\*)
25.327 +
25.328 + mk_env_eval_DEL i_model_max;
25.329 +(*///----------------- step into mk_env_eval_DEL -------------------------------------------\\*)
25.330 +"~~~~~ fun mk_env_eval_DEL , args:"; val (i_singles) = (i_model_max);
25.331 + val xxx = (fn (_, _, _, _, (feedb, _)) => discern_feedback_subst id feedb);
25.332 +
25.333 +(*///################# nth 1 i_model_max \<longrightarrow>[], <>[] only in maximum-example ##############=\\*)
25.334 +"~~~~~ fun xxx , args:"; val (_, _, _, _, (feedb, _)) = nth 1 i_model_max;
25.335 +(*---------------------------------------------------------^^^------------*)
25.336 +(*+*)val "Cor_TEST Traegerlaenge L ,(l_l, [L])"
25.337 + = feedb |> I_Model.feedback_to_string'_TEST @{context};
25.338 +
25.339 + discern_feedback_subst id feedb;
25.340 +"~~~~~ fun discern_feedback_subst , args:"; val (Model_Def.Cor_TEST ((descr, [ts]), _)) = (feedb);
25.341 + (*if*) TermC.is_list ts (*else*);
25.342 + val ts = (*if TermC.is_list ts then TermC.isalist2list ts else*) [ts];
25.343 +
25.344 + Pre_Conds.discern_type_eval descr ts;
25.345 +"~~~~~ fun discern_type_eval , args:"; val (descr, ts) = (descr, ts);
25.346 +val _(*"real \<Rightarrow> una"*) =
25.347 + (*case*) type_of descr (*of*)
25.348 +;
25.349 + Pre_Conds.discern_atoms ts;
25.350 +"~~~~~ fun discern_atoms , args:"; val (ts) = (ts);
25.351 + (*if*) all_atoms ts (*then*);
25.352 +
25.353 +val return_distinguish_ts_eval_1 =
25.354 + map (rpair TermC.empty (*dummy rhs*)) ts
25.355 +(*-------------------- contine discern_type_subst --------------------------------------------*)
25.356 +(*-------------------- contine discern_feedback_subst ----------------------------------------*)
25.357 +(*-------------------- contine mk_env_eval_DEL -----------------------------------------------*)
25.358 +val return_mk_env_subst_DEL_1
25.359 + = filter_out (fn (_, b) => b = TermC.empty) return_distinguish_ts_eval_1
25.360 +(*+*)val [] = return_mk_env_subst_DEL_1
25.361 +(*\\\################# nth 1 i_model_max \<longrightarrow>[], <>[] only in maximum-example ##############=//*)
25.362 +(*\\\----------------- step into mk_env_eval_DEL -------------------------------------------//*)
25.363 +
25.364 +(*|||----------------- contine of_max_variant ------------------------------------------------*)
25.365 +
25.366 +(* val env_eval = mk_env_eval_DEL i_model_max*)
25.367 + val env_eval = mk_env_eval_DEL i_model_max
25.368 +(*+*)val [] = env_eval
25.369 +val return_of_max_variant_step = (i_model_max, env_model, (env_subst, env_eval))
25.370 +;
25.371 +return_of_max_variant_step = return_of_max_variant
25.372 +( *\\\\\############### old test code ##################################################//////*)
25.373 +\<close> ML \<open>
25.374 +(*\\\----------------- step into of_max_variant --------------------------------------------//*)
25.375 + val (_, env_model, (env_subst, env_eval)) = return_of_max_variant
25.376 +
25.377 +(*|------------------- contine init_pstate ---------------------------------------------------*)
25.378 + val actuals = map snd env_model
25.379 +(*+* )val "[L, q_0, x, [c, c_2, c_3, c_4], dy, y, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]"
25.380 + = actuals |> UnparseC.terms @{context}(**)
25.381 +(*+*)val 7 = length actuals( **)
25.382 +(*WRONG ----------------v-v--v---v--v---v--v---v-----------v-------v--v-------v--v---------v--v---------v*)
25.383 +(*+*) val "[L, q_0, x, [[c], [c_2], [c_3], [c_4]], dy, y, [[y 0 = 0], [y L = 0], [M_b 0 = 0], [M_b L = 0]]]"
25.384 + = actuals |> UnparseC.terms @{context}
25.385 +\<close> ML \<open>
25.386 + val formals = Program.formal_args prog
25.387 +(*+*)val "[l_l, q_q, fun_var, b_b, r_b, vs, id_der]"
25.388 + = formals |> UnparseC.terms @{context}
25.389 +(*+*)val 7 = length formals
25.390 +
25.391 +\<close> ML \<open>
25.392 + val preconds = Pre_Conds.check_from_store ctxt where_rls where_ env_subst env_eval
25.393 +\<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)
25.394 + val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));
25.395 + val ist = Istate.e_pstate
25.396 + |> Istate.set_eval prog_rls
25.397 + |> Istate.set_env_true (relate_args [] formals actuals ctxt prog met_id formals actuals)
25.398 +\<close> text \<open> (*ERROR type_of: real/real list/(#) [c_4]*)
25.399 +(*+*)(relate_args [] formals actuals ctxt prog met_id formals actuals)
25.400 +\<close> text \<open>
25.401 +val return_init_pstate = (Istate.Pstate ist, ctxt, program)
25.402 +\<close> ML \<open>(*\\------------ step into init_pstate -----------------------------------------------//*)
25.403 +(*\\------------------ step into init_pstate -----------------------------------------------//*)
25.404 +\<close> ML \<open>(*\------------- step into me_Add_Given_AbleitungBieg --------------------------------//*)
25.405 +(*\------------------- step into me_Add_Given_AbleitungBieg --------------------------------//*)
25.406 +\<close> text \<open> (*\------------ step into me_Add_Given_AbleitungBieg --------------------------------//*)
25.407 +val (p,_,f,nxt,_,pt) = return_Add_Given_AbleitungBieg;
25.408 + val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
25.409 +
25.410 +\<close> text \<open>
25.411 +(* final test ... ----------------------------------------------------------------------------*)
25.412 +(*+*)val ([], Met) = p
25.413 +(*+*)val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
25.414 +
25.415 \<close> ML \<open>
25.416 \<close>
25.417
26.1 --- a/test/Tools/isac/Test_Theory.thy Fri Aug 04 23:07:04 2023 +0200
26.2 +++ b/test/Tools/isac/Test_Theory.thy Tue Aug 15 12:22:49 2023 +0200
26.3 @@ -11,13 +11,13 @@
26.4 "~~~~~ and xxx , args:"; val () = ();
26.5 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
26.6 "~~~~~ continue fun xxx"; val () = ();
26.7 -(*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
26.8 +(*if*) (*then*); (*else*); (*andalso*) (*case*) (*of*); (*return value*); (*in*) (*end*);
26.9 "xx"
26.10 ^ "xxx" (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)
26.11 -\<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)
26.12 -(*//------------------ adhoc inserted n ----------------------------------------------------\\*)
26.13 -(*\\------------------ adhoc inserted n ----------------------------------------------------//*)
26.14 -\<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)
26.15 +\<close> ML \<open> (*//----------- build fun XXXXX -----------------------------------------------------\\*)
26.16 +(*//------------------ build fun XXXXX -----------------------------------------------------\\*)
26.17 +(*\\------------------ build fun XXXXX -----------------------------------------------------//*)
26.18 +\<close> ML \<open> (*\\----------- build fun XXXXX -----------------------------------------------------//*)
26.19 val return_XXXXX = "XXXXX"
26.20 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
26.21 (*//------------------ step into XXXXX -----------------------------------------------------\\*)
26.22 @@ -27,13 +27,6 @@
26.23 \<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)
26.24 val "XXXXX" = return_XXXXX;
26.25
26.26 -
26.27 -(*/------------------- check entry to XXXXX -------------------------------------------------\*)
26.28 -(*\------------------- check entry to XXXXX -------------------------------------------------/*)
26.29 -(*/------------------- check within XXXXX ---------------------------------------------------\*)
26.30 -(*\------------------- check within XXXXX ---------------------------------------------------/*)
26.31 -(*/------------------- check result of XXXXX ------------------------------------------------\*)
26.32 -(*\------------------- check result of XXXXX ------------------------------------------------/*)
26.33 (* final test ... ----------------------------------------------------------------------------*)
26.34
26.35 \<close> ML \<open> (*//----------- inserted hidden code ------------------------------------------------\\*)
26.36 @@ -41,10 +34,6 @@
26.37 (*\\------------------ inserted hidden code ------------------------------------------------//*)
26.38 \<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)
26.39
26.40 -\<close> ML \<open> (*//----------- build fun XXXXX -----------------------------------------------------\\*)
26.41 -(*//------------------ build fun XXXXX -----------------------------------------------------\\*)
26.42 -(*\\------------------ build fun XXXXX -----------------------------------------------------//*)
26.43 -\<close> ML \<open> (*\\----------- build fun XXXXX -----------------------------------------------------//*)
26.44 \<close>
26.45 ML \<open>
26.46 \<close> ML \<open>
26.47 @@ -170,8 +159,12 @@
26.48 "~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
26.49 (ctxt, where_rls, where_, (model, I_Model.OLD_to_TEST probl));
26.50 \<close> ML \<open>
26.51 - val (_, _, (env_subst, env_eval)) =
26.52 + val (_, (** )_( **)env_model(**), (env_subst, env_eval)) =
26.53 of_max_variant model_patt i_model;
26.54 +\<close> ML \<open>
26.55 +(*maxi*)val "[]" = env_model |> Subst.to_string @{context}
26.56 +(*maxi*)val "[]" = env_subst |> Subst.to_string @{context}
26.57 +\<close> ML \<open>
26.58 "~~~~~ fun of_max_variant , args:"; val (_, []) = (model_patt, i_model);
26.59 (*\------------------- step into init_calc -------------------------------------------------//*)
26.60 \<close> ML \<open> (*\------------ step into init_calc -------------------------------------------------//*)
26.61 @@ -224,6 +217,9 @@
26.62 (*//------------------ step into do_next ---------------------------------------------------\\*)
26.63 "~~~~~ fun do_next , args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) =
26.64 (p, ((pt, e_pos'),[]));
26.65 +\<close> ML \<open>
26.66 +(*+*)val Pbl = p_
26.67 +\<close> ML \<open>
26.68 val pIopt = get_pblID (pt,ip);
26.69 (*if*) ip = ([],Res); (* = false*)
26.70 val _ = (*case*) tacis (*of*);
26.71 @@ -234,6 +230,7 @@
26.72 Step.switch_specify_solve p_ (pt, ip);
26.73 \<close> ML \<open>
26.74 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
26.75 +\<close> ML \<open>
26.76 (*if*) Pos.on_specification ([], state_pos) (*then*);
26.77
26.78 \<close> ML \<open>
26.79 @@ -266,16 +263,41 @@
26.80 val cmI = if mI = MethodC.id_empty then mI' else mI;
26.81 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
26.82 val {model = mpc, ...} = MethodC.from_store ctxt cmI;
26.83 -\<close> ML \<open> (*//----------- adhoc inserted fun of_max_variant -----------------------------------\\*)
26.84 -(*//------------------ adhoc inserted fun of_max_variant -----------------------------------\\* )
26.85 +
26.86 +\<close> ML \<open> (*//----------- adhoc inserted fun check_OLD ----------------------------------------\\*)
26.87 +(*//------------------ adhoc inserted fun check_OLD ----------------------------------------\\* )
26.88 +
26.89 +(*T_TESTold* )
26.90 +fun all_lhs_atoms ts = fold (curry and_) (map (fn t =>
26.91 + if can TermC.lhs t then TermC.is_atom (TermC.lhs t) else false) ts) true
26.92 +( *T_TEST*)
26.93 +fun all_lhs_atoms ts = fold (curry and_) (map (fn t =>
26.94 + if can TermC.lhs t andalso not (TermC.is_num (TermC.lhs t))
26.95 + then TermC.is_atom (TermC.lhs t)
26.96 + else false) ts) true
26.97 +(*T_TESTnew*)
26.98 +
26.99 +(*T_TESTold* )
26.100 fun handle_lists id (descr, ts) =
26.101 - if Model_Pattern.is_list_descr descr
26.102 - then if length ts > 1 (*list with more than 1 element needs to collect by [.., .., ..]*)
26.103 - then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)] (*AdditValues [u, v]*)
26.104 - else if TermC.is_atom (Library.the_single ts)
26.105 - then [(id, Library.the_single ts)] (* solutions L, ...*)
26.106 - else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)](*Constants [r = 7]*)
26.107 - else [(id, Library.the_single ts)] (* solveFor x, Extremum (A = ...)*)
26.108 + if Model_Pattern.is_list_descr descr
26.109 + then if length ts > 1 (*list with more than 1 element needs to collect by [.., .., ..]*)
26.110 + then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)] (*AdditValues [u, v]*)
26.111 + else if TermC.is_atom (Library.the_single ts)
26.112 + then [(id, Library.the_single ts)] (* solutions L, ...*)
26.113 + else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)](*Constants [r = 7]*)
26.114 + else [(id, Library.the_single ts)] (* solveFor x, Extremum (A = ...)*)
26.115 +( *T_TEST***)
26.116 +fun handle_lists id (descr, ts) =
26.117 + if Model_Pattern.is_list_descr descr
26.118 + then if length ts > 1 (*list with more than 1 element needs to collect by [.., .., ..]*)
26.119 + then if TermC.is_list (hd ts) (*---broken elementwise input to lists---*)
26.120 + then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) (map TermC.the_single ts))]
26.121 + else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)] (*AdditValues [u, v]*)
26.122 + else if TermC.is_atom (Library.the_single ts)
26.123 + then [(id, Library.the_single ts)] (* solutions L, ...*)
26.124 + else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)](*Constants [r = 7]*)
26.125 + else [(id, Library.the_single ts)] (* solveFor x, Extremum (A = ...)*)
26.126 +(*T_TESTnew*)
26.127 ;
26.128 handle_lists: term -> descriptor * term list -> (term * term) list;
26.129
26.130 @@ -321,6 +343,7 @@
26.131 ;
26.132 switch_type_TEST: descriptor -> term list -> descriptor;
26.133
26.134 +(*T_TESTold* )
26.135 fun discern_typ _ (_, []) = []
26.136 | discern_typ id (descr, ts) =
26.137 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
26.138 @@ -341,8 +364,32 @@
26.139 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
26.140 end
26.141 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)
26.142 +( *T_TEST*)
26.143 +fun discern_typ _ (_, []) = []
26.144 + | discern_typ id (descr, ts) =
26.145 +(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
26.146 + let
26.147 + val ts = if Model_Pattern.is_list_descr descr
26.148 + then if TermC.is_list (hd ts)
26.149 + then ts |> map TermC.isalist2list |> flat
26.150 + else ts
26.151 + else ts
26.152 + in
26.153 +(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)
26.154 + if Model_Pattern.typ_of_element descr = HOLogic.boolT andalso all_lhs_atoms ts
26.155 + then
26.156 + if length ts > 1
26.157 + then (writeln "model items of type 'bool' in lists with 'lengt ts > 1' NOT YET IMPLEMENTED";
26.158 + [])
26.159 + else [((switch_type_TEST id ts, TermC.lhs (hd ts)),
26.160 + (TermC.lhs (hd ts), TermC.rhs (hd ts)))]
26.161 + else []
26.162 +(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
26.163 + end
26.164 +(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)
26.165 ;
26.166 discern_typ: term -> descriptor * term list -> ((term * term) * (term * term)) list;
26.167 +(*T_TESTnew*)
26.168
26.169 fun discern_feedback id (Model_Def.Cor_TEST ((descr, ts), _)) = discern_typ id (descr, ts)
26.170 | discern_feedback _ (Model_Def.Syn_TEST _) = [] (*TODO: handle correct elements*)
26.171 @@ -393,7 +440,7 @@
26.172 end
26.173 (*T_TESTnew*)
26.174 ;
26.175 -of_max_variant:Model_Pattern.T -> Model_Def.i_model_TEST ->
26.176 +of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->
26.177 Model_Def.i_model_TEST * Env.T * (env_subst * env_eval);
26.178
26.179 fun check_OLD _ _ [] _ = (true, [])
26.180 @@ -570,10 +617,14 @@
26.181 \<close> ML \<open>
26.182 val (env_subst, env_eval) = split_list subst_eval_list
26.183 \<close> ML \<open>
26.184 +(*maxi*)val "[\"\n(fixes, [r = 7])\"]" = env_model |> Subst.to_string @{context}
26.185 +(*maxi*)val "[\"\n(fixes, r)\"]" = env_subst |> Subst.to_string @{context}
26.186 +\<close> ML \<open>
26.187 val return_of_max_variant = (i_model_max, env_model, (env_subst, env_eval)); (*GOON*)
26.188 (*\\\\\ \\------------ step into of_max_variant --------------------------------------------//*)
26.189 \<close> ML \<open> (*\\\\\ \\----- step into of_max_variant --------------------------------------------//*)
26.190 val (i_model_max, env_model, (env_subst, env_eval)) = return_of_max_variant
26.191 +\<close> ML \<open>
26.192 (*!!!/----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---\*)
26.193 val (i_max_variant, env_model, (env_subst, env_eval)) = (i_model_max, [], ([], []))
26.194 (*!!!\----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---/*)
26.195 @@ -955,7 +1006,10 @@
26.196 "~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
26.197 (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
26.198 \<close> ML \<open> (*ERROR lhs called with [r = 7]*)
26.199 - val (_, _, (env_subst, env_eval)) = of_max_variant model_patt i_model;
26.200 + val (_, (** )_( **)env_model(**), (env_subst, env_eval)) = of_max_variant model_patt i_model;
26.201 +\<close> ML \<open>
26.202 +(*maxi*)val "[\"\n(fixes, [[r = 7]])\"]" = env_model |> Subst.to_string @{context}
26.203 +(*maxi*)val "[\"\n(fixes, r)\"]" = env_subst |> Subst.to_string @{context}
26.204 \<close> ML \<open>
26.205 "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
26.206 \<close> ML \<open>
26.207 @@ -1084,6 +1138,8 @@
26.208 val return_of_max_variant as (_, _, (env_subst, env_eval)) =
26.209 of_max_variant model_patt i_model
26.210 \<close> ML \<open>
26.211 +(*maxi*)val "[\"\n(fixes, [[r = 7]])\"]" = env_model |> Subst.to_string @{context}
26.212 +(*maxi*)val "[\"\n(fixes, r)\"]" = env_subst |> Subst.to_string @{context}
26.213 (*+*)val [(Free ("fixes", T1), Free ("r", T2))] = env_subst (*?!? Const*)
26.214 (*+*)val Type ("Real.real", []) = T1
26.215 (*+*)val Type ("Real.real", []) = T2
26.216 @@ -1392,7 +1448,7 @@
26.217 (* Title: "Minisubpbl/100-init-rootpbl-NEXT_STEP.sml"
26.218 Author: Walther Neuper 2307
26.219 *)
26.220 -
26.221 +(*overwrites NEW funs in Test_Theory ABOVE* )
26.222 open Ctree;
26.223 open Pos;
26.224 open TermC;
26.225 @@ -1405,6 +1461,7 @@
26.226 open Specify;
26.227 open LItool;
26.228 open LI;
26.229 +( *overwrites NEW funs in Test_Theory ABOVE*)
26.230
26.231 "----------- Minisubpbl/100-init-rootpbl-NEXT_STEP.sml ---------------------------------------";
26.232 "----------- Minisubpbl/100-init-rootpbl-NEXT_STEP.sml ---------------------------------------";
26.233 @@ -1480,9 +1537,11 @@
26.234 \<close> ML \<open>
26.235 val (_, env_model, (env_subst, env_eval)) = of_max_variant model_patt i_model
26.236 \<close> ML \<open>
26.237 +(*equa*)val "[\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\", \"\n(v_v'i', L)\"]" = env_model |> Subst.to_string @{context}
26.238 +(*equa*)val "[]" = env_subst |> Subst.to_string @{context}
26.239 +\<close> ML \<open>
26.240 val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
26.241 \<close> ML \<open>
26.242 -(*+*)val [] = env_subst
26.243 (*+*)val [(false, Const ("Test.precond_rootpbl", _) $ Free ("v_v", _))] = pres_subst
26.244 \<close> ML \<open>
26.245 val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
26.246 @@ -1575,6 +1634,10 @@
26.247 "~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
26.248 (ctxt, where_rls, where_, (m_patt, I_Model.OLD_to_TEST itms'));
26.249 val (_, env_model, (env_subst, env_eval)) = of_max_variant model_patt i_model
26.250 +\<close> ML \<open>
26.251 +(*equa*)val "[\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\", \"\n(v_v'i', L)\"]" = env_model |> Subst.to_string @{context}
26.252 +(*equa*)val "[]" = env_subst |> Subst.to_string @{context}
26.253 +\<close> ML \<open>
26.254 val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
26.255 val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
26.256 val full_subst = if env_eval = [] then pres_subst_other
26.257 @@ -1629,13 +1692,13 @@
26.258 (*case*) tacis (*of*);
26.259 (*if*) probl_id = Problem.id_empty (*else*);
26.260
26.261 -\<close> text \<open> (*ERROR 2 formal args: [e_e, v_v], 0 actual args: []*)
26.262 +\<close> ML \<open> (*ERROR 2 formal args: [e_e, v_v], 0 actual args: []*)
26.263 switch_specify_solve p_ (pt, ip);
26.264 \<close> ML \<open>
26.265 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
26.266 (*if*) Pos.on_specification ([], state_pos) (*then*);
26.267
26.268 -\<close> text \<open> (*ERROR 2 formal args: [e_e, v_v], 0 actual args: []*)
26.269 +\<close> ML \<open> (*ERROR 2 formal args: [e_e, v_v], 0 actual args: []*)
26.270 specify_do_next (pt, input_pos);
26.271 \<close> ML \<open>
26.272 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
26.273 @@ -1644,7 +1707,7 @@
26.274 (*+*)val Tactic.Apply_Method mI =
26.275 (*case*) tac (*of*);
26.276
26.277 -\<close> text \<open> (*ERROR 2 formal args: [e_e, v_v], 0 actual args: []*)
26.278 +\<close> ML \<open> (*ERROR 2 formal args: [e_e, v_v], 0 actual args: []*)
26.279 LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
26.280 ist_ctxt (pt, (p, p_'));
26.281 \<close> ML \<open>
26.282 @@ -1738,7 +1801,7 @@
26.283
26.284 \<close> ML \<open>
26.285 val return_of_max_variant =
26.286 - I_Model.of_max_variant model_patt i_model;
26.287 + of_max_variant model_patt i_model;
26.288 \<close> ML \<open>(*///----------- step into of_max_variant --------------------------------------------\\*)
26.289 (*///----------------- step into of_max_variant --------------------------------------------\\*)
26.290 "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
26.291 @@ -1914,6 +1977,832 @@
26.292 \<close>
26.293
26.294
26.295 +section \<open>===== Interpret/li-tool.sml =======================================================\<close>
26.296 +ML \<open>
26.297 +\<close> ML \<open>
26.298 +(* Title: Interpret/li-tool.sml
26.299 + Author: Walther Neuper 050908
26.300 + (c) copyright due to lincense terms.
26.301 +*)
26.302 +"-----------------------------------------------------------------";
26.303 +"table of contents -----------------------------------------------";
26.304 +"-----------------------------------------------------------------";
26.305 +"----------- fun implicit_take, fun get_first_argument -------------------------";
26.306 +"----------- fun from_prog ---------------------------------------";
26.307 +"----------- fun specific_from_prog ----------------------------";
26.308 +"----------- fun de_esc_underscore -------------------------------";
26.309 +"----------- fun go ----------------------------------------------";
26.310 +"----------- fun formal_args -------------------------------------";
26.311 +"----------- fun dsc_valT ----------------------------------------";
26.312 +"----------- fun arguments_from_model ---------------------------------------";
26.313 +"----------- fun init_pstate -----------------------------------------------------------------";
26.314 +"-----------------------------------------------------------------";
26.315 +"-----------------------------------------------------------------";
26.316 +"-----------------------------------------------------------------";
26.317 +
26.318 +val thy = @{theory Isac_Knowledge};
26.319 +
26.320 +\<close> ML \<open>
26.321 +"----------- fun init_pstate -----------------------------------------------------------------";
26.322 +"----------- fun init_pstate -----------------------------------------------------------------";
26.323 +"----------- fun init_pstate -----------------------------------------------------------------";
26.324 +(*
26.325 + This test is deeply nested (down into details of creating environments).
26.326 + In order to make Sidekick show the structure add to each
26.327 + * (*/...\*) and (*\.../*)
26.328 + * a companion > ML < (*/...\*) and > ML < (*\.../*)
26.329 + Note the wrong ^----^ delimiters.
26.330 +*)
26.331 +val fmz = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
26.332 + "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
26.333 + "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
26.334 + "AbleitungBiegelinie dy"];
26.335 +val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
26.336 + ["IntegrierenUndKonstanteBestimmen2"]);
26.337 +val p = e_pos'; val c = [];
26.338 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))]; val Model_Problem = nxt
26.339 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Traegerlaenge L" = nxt
26.340 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Streckenlast q_0" = nxt
26.341 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Biegelinie y" = nxt
26.342 +\<close> ML \<open>
26.343 +(*/---broken elementwise input to lists---\* )
26.344 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)
26.345 + (*isa* ) val Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" = nxt
26.346 + ( *isa2*) val Add_Relation "Randbedingungen [y 0 = 0]" = nxt
26.347 +(*[], 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]"*)
26.348 + (*isa*) val Specify_Theory "Biegelinie" = nxt
26.349 + (*isa2* ) val Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]" = nxt( **)
26.350 +( *\---broken elementwise input to lists---/*)
26.351 +\<close> ML \<open>
26.352 +(*[], 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
26.353 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
26.354 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["Biegelinien"] = nxt
26.355 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
26.356 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "FunktionsVariable x" = nxt
26.357 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]" = nxt
26.358 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy" = nxt
26.359 +
26.360 +\<close> ML \<open>
26.361 +(*[], Met*)val return_Add_Given_AbleitungBieg
26.362 + = me nxt p c pt;
26.363 +\<close> ML \<open> (*/------------ step into me_Add_Given_AbleitungBieg --------------------------------\\*)
26.364 +(*/------------------- step into me_Add_Given_AbleitungBieg --------------------------------\\*)
26.365 +
26.366 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
26.367 + val ctxt = Ctree.get_ctxt pt p
26.368 +val ("ok", (_, _, ptp as (pt, p))) =
26.369 + (*case*) Step.by_tactic tac (pt, p) (*of*);
26.370 +
26.371 +\<close> ML \<open>
26.372 + (*case*)
26.373 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
26.374 +\<close> ML \<open>
26.375 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
26.376 + (p, ((pt, Pos.e_pos'), []) );
26.377 + (*if*) Pos.on_calc_end ip (*else*);
26.378 + val (_, probl_id, _) = Calc.references (pt, p);
26.379 +val _ =
26.380 + (*case*) tacis (*of*);
26.381 + (*if*) probl_id = Problem.id_empty (*else*);
26.382 +
26.383 +\<close> ML \<open>
26.384 + switch_specify_solve p_ (pt, ip);
26.385 +\<close> ML \<open>
26.386 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
26.387 + (*if*) Pos.on_specification ([], state_pos) (*then*);
26.388 +
26.389 +\<close> ML \<open>
26.390 + specify_do_next (pt, input_pos);
26.391 +\<close> ML \<open>
26.392 +"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
26.393 + val (_, (p_', tac)) = Specify.find_next_step ptp
26.394 + val ist_ctxt = Ctree.get_loc pt (p, p_)
26.395 +val Tactic.Apply_Method mI =
26.396 + (*case*) tac (*of*);
26.397 +
26.398 +\<close> ML \<open>
26.399 + LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
26.400 + ist_ctxt (pt, (p, p_'));
26.401 +\<close> ML \<open>
26.402 +"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
26.403 + ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));
26.404 + val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)
26.405 + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
26.406 + | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
26.407 + val {model, ...} = MethodC.from_store ctxt mI;
26.408 + val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
26.409 +;
26.410 +(*+*)if (itms |> I_Model.to_string @{context}) = "[\n" ^
26.411 + "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^
26.412 + "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
26.413 + "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^
26.414 + "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]])), \n" ^
26.415 + "(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(fun_var, [x])), \n" ^
26.416 + "(6 ,[1] ,true ,#Given ,Cor GleichungsVariablen [c, c_2, c_3, c_4] ,(vs, [[c, c_2, c_3, c_4]])), \n" ^
26.417 + "(7 ,[1] ,true ,#Given ,Cor AbleitungBiegelinie dy ,(id_der, [dy]))]"
26.418 +(*+*)then () else error "init_pstate: initial i_model changed";
26.419 +(*+*)if (itms |> I_Model.penv_to_string @{context}) = "[" ^ (*to be eliminated*)
26.420 +(*1*)"(l_l, [L]), " ^
26.421 +(*2*)"(q_q, [q_0]), " ^
26.422 +(*3*)"(b_b, [y]), " ^
26.423 +(*4*)"(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]), " ^
26.424 +(*5*)"(fun_var, [x]), " ^
26.425 +(*6*)"(vs, [[c, c_2, c_3, c_4]]), " ^
26.426 +(*7*)"(id_der, [dy])]"
26.427 +(*+*)then () else error "init_pstate: initial penv changed";
26.428 +
26.429 +\<close> ML \<open>
26.430 + (*case*)
26.431 + LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI (*of*);
26.432 +\<close> ML \<open>(*//------------ step into init_pstate -----------------------------------------------\\*)
26.433 +(*//------------------ step into init_pstate -----------------------------------------------\\*)
26.434 +"~~~~~ fun init_pstate , args:"; val (ctxt, i_model, met_id) = (ctxt, (I_Model.OLD_to_TEST itms), mI);
26.435 + val (model_patt, program, prog, prog_rls, where_, where_rls) =
26.436 + case MethodC.from_store ctxt met_id of
26.437 + {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...}=>
26.438 + (model_patt, program, prog, prog_rls, where_, where_rls)
26.439 +
26.440 +\<close> ML \<open>
26.441 + val return_of_max_variant =
26.442 + of_max_variant model_patt i_model;
26.443 +\<close> ML \<open>(*///----------- step into of_max_variant --------------------------------------------\\*)
26.444 +(*///----------------- step into of_max_variant --------------------------------------------\\*)
26.445 +"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
26.446 + val all_variants =
26.447 + map (fn (_, variants, _, _, _) => variants) i_model
26.448 + |> flat
26.449 + |> distinct op =
26.450 + val variants_separated = map (filter_variants' i_model) all_variants
26.451 + val sums_corr = map (cnt_corrects) variants_separated
26.452 + val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
26.453 + val (_, max_variant) = hd (*..crude decision, up to improvement *)
26.454 + (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
26.455 + val i_model_max =
26.456 + filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
26.457 + val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
26.458 +;
26.459 +(*+*)if (equal_descr_pairs |> descr_pairs_to_string @{context}) = "[" ^
26.460 +(*defined: in program+model--vvvv--,----------------------------------------- in problem ---vvv*)
26.461 + "((#Given, (Traegerlaenge, l_l)), (1, [1], true ,#Given, " ^ "(Cor_TEST Traegerlaenge L ,(l_l, [L]), Position.T))), " ^
26.462 +(*-------------------------------------------------------------------------------------penv-^^^^^^^^^ DROP!*)
26.463 + "((#Given, (Streckenlast, q_q)), (2, [1], true ,#Given, " ^
26.464 + "(Cor_TEST Streckenlast q_0 ,(q_q, [q_0]), Position.T))), " ^
26.465 + "((#Given, (FunktionsVariable, fun_var)), (5, [1], true ,#Given, " ^
26.466 + "(Cor_TEST FunktionsVariable x ,(fun_var, [x]), Position.T))), " ^
26.467 + "((#Given, (GleichungsVariablen, vs)), (6, [1], true ,#Given, " ^
26.468 + "(Cor_TEST GleichungsVariablen [c, c_2, c_3, c_4] ,(vs, [[c, c_2, c_3, c_4]]), Position.T))), " ^
26.469 + "((#Given, (AbleitungBiegelinie, id_der)), (7, [1], true ,#Given, " ^
26.470 + "(Cor_TEST AbleitungBiegelinie dy ,(id_der, [dy]), Position.T))), " ^
26.471 + "((#Find, (Biegelinie, b_b)), (3, [1], true ,#Find, (Cor_TEST Biegelinie y ,(b_b, [y]), Position.T))), " ^
26.472 +(*-----------------------------------------------------------------------penv-^^^^^^^^^ DROP!*)
26.473 + "((#Relate, (Randbedingungen, r_b)), (4, [1], true ,#Relate, " ^
26.474 + "(Cor_TEST Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]), Position.T)))]"
26.475 +(*-----------------------------------------------------------------penv-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ DROP!*)
26.476 +then () else error "of_max_variant: equal_descr_pairs CHANGED";
26.477 +
26.478 + val return_make_env_model = make_env_model equal_descr_pairs;
26.479 +\<close> ML \<open> (*////--------- step into make_env_model --------------------------------------------\\*)
26.480 +(*////---------------- step into make_env_model --------------------------------------------\\*)
26.481 +\<close> ML \<open>
26.482 +"~~~~~ fun make_env_model , args:"; val (equal_descr_pairs) = (equal_descr_pairs);
26.483 +\<close> ML \<open>
26.484 +"~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 4 equal_descr_pairs;
26.485 +\<close> ML \<open>
26.486 +"~~~~~ fun mk_env_model , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) = (id, feedb);
26.487 +\<close> ML \<open>
26.488 + handle_lists id (descr, ts);
26.489 +"~~~~~ fun handle_lists , args:"; val (id, (descr, ts)) = (id, (descr, ts));
26.490 +\<close> ML \<open>
26.491 +(*+*)val xxx = ts |> UnparseC.terms @{context}
26.492 +\<close> ML \<open>
26.493 + (*if*) Model_Pattern.is_list_descr descr (*then*);
26.494 +\<close> ML \<open>
26.495 + (*if*) length ts > 1 (*then*);
26.496 +\<close> ML \<open>
26.497 + (*if*) TermC.is_list (hd ts) (*then*);
26.498 +\<close> ML \<open>
26.499 +val return_handle_lists_step =
26.500 + [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) (map TermC.the_single ts))]
26.501 +\<close> ML \<open>
26.502 +(*+*)val "[\"\n(vs, [c, c_2, c_3, c_4])\"]"
26.503 + = return_handle_lists_step |> Subst.to_string @{context}
26.504 +(*\\\\---------------- step into make_env_model --------------------------------------------//*)
26.505 +\<close> ML \<open> (*\\\\--------- step into make_env_model --------------------------------------------//*)
26.506 + val env_model = return_make_env_model
26.507 +(*+*)val "[\"\n(l_l, L)\", \"\n(q_q, q_0)\", \"\n(fun_var, x)\", \"\n(vs, [c, c_2, c_3, c_4])\", \"\n(id_der, dy)\", \"\n(b_b, y)\", \"\n(r_b, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\"]"
26.508 + = env_model |> Subst.to_string @{context}
26.509 +\<close> ML \<open> (*|||---------- contine of_max_variant ------------------------------------------------*)
26.510 +(*|||----------------- contine of_max_variant ------------------------------------------------*)
26.511 + val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
26.512 + val subst_eval_list = make_envs_preconds equal_givens
26.513 + val (env_subst, env_eval) = split_list subst_eval_list
26.514 +\<close> ML \<open>
26.515 +(*bieg*)val "[\"\n(l_l, L)\", \"\n(q_q, q_0)\", \"\n(fun_var, x)\", \"\n(vs, [c, c_2, c_3, c_4])\", \"\n(id_der, dy)\", \"\n(b_b, y)\", \"\n(r_b, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\"]" = env_model |> Subst.to_string @{context}
26.516 +(*bieg*)val "[]" = env_subst |> Subst.to_string @{context}
26.517 +\<close> ML \<open>
26.518 +val return_of_max_variant_step = (i_model_max, env_model, (env_subst, env_eval))
26.519 +\<close> ML \<open>
26.520 +(*+*)if return_of_max_variant_step = return_of_max_variant then () else error "<>"
26.521 +\<close> ML \<open>(*\\\----------- step into of_max_variant --------------------------------------------//*)
26.522 +(*\\\----------------- step into of_max_variant --------------------------------------------//*)
26.523 + val (_, env_model, (env_subst, env_eval)) = return_of_max_variant
26.524 +\<close> ML \<open>
26.525 +(*|------------------- contine init_pstate ---------------------------------------------------*)
26.526 + val actuals = map snd env_model
26.527 +(*+*) val "[L, q_0, x, [c, c_2, c_3, c_4], dy, y, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]"
26.528 + = actuals |> UnparseC.terms @{context}
26.529 +\<close> ML \<open>
26.530 + val formals = Program.formal_args prog
26.531 +(*+*)val "[l_l, q_q, fun_var, b_b, r_b, vs, id_der]"
26.532 + = formals |> UnparseC.terms @{context}
26.533 +(*+*)val 7 = length formals
26.534 +
26.535 +\<close> ML \<open>
26.536 + val preconds = Pre_Conds.check_from_store ctxt where_rls where_ env_subst env_eval
26.537 +\<close> ML \<open>
26.538 + val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));
26.539 + val ist = Istate.e_pstate
26.540 + |> Istate.set_eval prog_rls
26.541 + |> Istate.set_env_true (relate_args [] formals actuals ctxt prog met_id formals actuals)
26.542 +\<close> ML \<open>
26.543 +(*+*)(relate_args [] formals actuals ctxt prog met_id formals actuals)
26.544 +\<close> ML \<open>
26.545 +val return_init_pstate = (Istate.Pstate ist, ctxt, program)
26.546 +\<close> ML \<open>(*\\------------ step into init_pstate -----------------------------------------------//*)
26.547 +(*\\------------------ step into init_pstate -----------------------------------------------//*)
26.548 +\<close> ML \<open>(*\------------- step into me_Add_Given_AbleitungBieg --------------------------------//*)
26.549 +(*\------------------- step into me_Add_Given_AbleitungBieg --------------------------------//*)
26.550 +\<close> ML \<open> (*\------------ step into me_Add_Given_AbleitungBieg --------------------------------//*)
26.551 +val (p,_,f,nxt,_,pt) = return_Add_Given_AbleitungBieg;
26.552 + val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
26.553 +
26.554 +\<close> ML \<open>
26.555 +(* final test ... ----------------------------------------------------------------------------*)
26.556 +(*+*)val ([], Met) = p
26.557 +(*+*)val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
26.558 +
26.559 +\<close> ML \<open>
26.560 +\<close>
26.561 +
26.562 +section \<open>===================================================================================\<close>
26.563 +section \<open>===== refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ==================\<close>
26.564 +ML \<open> (*\<longrightarrow> refine.sml*)
26.565 +"----------- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";
26.566 +"----------- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";
26.567 +"----------- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";
26.568 +(*overwrites NEW funs in Test_Theory ABOVE* )
26.569 +open Refine
26.570 +open M_Match
26.571 +open Pre_Conds
26.572 +( *overwrites NEW funs in Test_Theory ABOVE*)
26.573 +(*
26.574 + refinement of the first eqsystem in Biegelinie, IntegrierenUndKonstanteBestimmen2;
26.575 + this example was the demonstrator;
26.576 + respective data are in ~/proto4/../exp_Statics_Biegel_Timischl_7-70.xml.
26.577 + Data for this test are from biegelinie-5.sml, --- me IntegrierenUndKonstanteBestimmen2 ALL ---
26.578 +*)
26.579 +\<close> ML \<open>
26.580 +(*+*)val o_model = [
26.581 +(1, [1], "#Given", @{term "equalities"},
26.582 + [@{term "[(0::real) = - 1 * c_4 / - 1]"},
26.583 + @{term "[(0::real) = (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / - 24]"},
26.584 + @{term "[(0::real) = c_2]"},
26.585 + @{term "[(0::real) = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"}] ),
26.586 +(*Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c", "real") $ Const ("List.list.Nil", "real list"),*)
26.587 +(2, [1], "#Given", @{term "solveForVars"},
26.588 + [@{term "[c] ::real list"},
26.589 + @{term "[c_2]::real list"},
26.590 + @{term "[c_3]::real list"},
26.591 + @{term "[c_4]::real list"}] ),
26.592 +(3, [1], "#Find", @{term "solution"}, [@{term "ss'''::bool list"}] )]
26.593 +\<close> ML \<open>
26.594 +(*ERROR exception Bind* )
26.595 +val ["normalise", "4x4", "LINEAR", "system"] =
26.596 + refine_ori' @{context} o_model ["LINEAR", "system"];
26.597 +val SOME ["normalise", "4x4", "LINEAR", "system"] =
26.598 +( *ERROR exception Bind*)
26.599 + refine_ori @{context} o_model ["LINEAR", "system"];
26.600 +\<close> ML \<open>
26.601 +"~~~~~ fun refine_ori , args:"; val (ctxt, oris, pblID) =
26.602 + (@{context}, o_model, ["LINEAR", "system"]);
26.603 +\<close> ML \<open>
26.604 +(*ERROR exception Bind* )
26.605 + val opt as SOME ["system", "LINEAR", "4x4", "normalise"]
26.606 + =( *ERROR exception Bind*)
26.607 + app_ptyp (refin ctxt ((rev o tl) pblID) oris) pblID (rev pblID);
26.608 +\<close> ML \<open>
26.609 +(*
26.610 + app_ptyp works strangely, parameter passing is awkward.
26.611 + Present refin knows structure of Store.T, thus we bypass app_ptyp
26.612 +( **)
26.613 +\<close> ML \<open>
26.614 +
26.615 +(*!*)val pblID = ["LINEAR", "system"];(**)
26.616 +(*isa* )val return_refin as SOME ["system", "LINEAR", "LINEAR"] = ( **)
26.617 +(*isa2*)val return_refin as SOME ["system", "LINEAR", "LINEAR", "4x4", "normalise"] = (**)
26.618 + refin ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));
26.619 +\<close> ML \<open>
26.620 +"~~~~~ fun refin , args:"; val (ctxt, pblRD, ori, (Store.Node (pI, [py], pys)))
26.621 + = (ctxt, (rev pblID), oris, Store.get_node (rev pblID) pblID (get_pbls ()));
26.622 +\<close> ML \<open>
26.623 + val {where_rls, model, where_, ...} = py: Problem.T
26.624 + val model = map (Model_Pattern.adapt_to_type ctxt) model
26.625 + val where_ = map (ParseC.adapt_term_to_type ctxt) where_
26.626 +\<close> ML \<open>
26.627 + (*if*) M_Match.match_oris ctxt where_rls ori (model, where_) (*then*);
26.628 +\<close> ML \<open>
26.629 +val return_refin as SOME ["system", "LINEAR"] = SOME (pblRD (** )@ [pI]( **))
26.630 +\<close> ML \<open>
26.631 +(*follow the trace created in parallel by writeln in Store.get_node and Refine.refin*)
26.632 +(*!*)val pblID = ["4x4", "LINEAR", "system"];(**)
26.633 +(*isa* )val return_refin as NONE = ( **)
26.634 +(*isa2*)val return_refin as SOME ["system", "LINEAR", "4x4", "4x4", "normalise"] = (**)
26.635 + refin ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));
26.636 +\<close> ML \<open>
26.637 +"~~~~~ fun refin , args:"; val (ctxt, pblRD, ori, (Store.Node (pI, [py], pys)))
26.638 + = (ctxt, (rev pblID), oris, Store.get_node (rev pblID) pblID (get_pbls ()));
26.639 +\<close> ML \<open>
26.640 + val {where_rls, model, where_, ...} = py: Problem.T
26.641 + val model = map (Model_Pattern.adapt_to_type ctxt) model
26.642 + val where_ = map (ParseC.adapt_term_to_type ctxt) where_
26.643 +\<close> ML \<open>
26.644 +(*isa*) (*if*) M_Match.match_oris ctxt where_rls ori (model, where_) (*else*);
26.645 +(*isa2*)(*if*) M_Match.match_oris ctxt where_rls ori (model, where_) (*then*);
26.646 +\<close> ML \<open>
26.647 +"~~~~~ fun match_oris , args:"; val (ctxt, where_rls, oris, (pbt, where_)) =
26.648 + (ctxt, where_rls, ori, (model, where_));
26.649 +\<close> ML \<open>
26.650 +(*+*)val Rule_Def.Repeat
26.651 + {asm_rls = Rule_Set.Empty, calc = [], errpatts = [], id = "prls_4x4_linear_system", preconds = [], prog_rls = Rule_Set.Empty, program = Empty_Prog, rew_ord = ("dummy_ord", _), rules =
26.652 + [Thm ("LENGTH_CONS", _), Thm ("LENGTH_NIL", _), Eval ("Groups.plus_class.plus", _), Eval ("HOL.eq", _)]}
26.653 + = where_rls
26.654 +(*+*)val "[\n(1, [\"1\"], #Given, equalities, [\"[0 = - 1 * c_4 / - 1]\", \"[0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24]\", \"[0 = c_2]\", \"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]\"]), \n(2, [\"1\"], #Given, solveForVars, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n(3, [\"1\"], #Find, solution, [\"ss'''\"])]"
26.655 + = oris |> O_Model.to_string @{context}
26.656 +(*+*)val "[\"(#Given, (equalities, e_s))\", \"(#Given, (solveForVars, v_s))\", \"(#Find, (solution, ss'''))\"]"
26.657 + = pbt |> Model_Pattern.to_string @{context}
26.658 +(*+*)val "[Length e_s = 4, Length v_s = 4]" = where_ |> UnparseC.terms @{context}
26.659 +\<close> ML \<open>
26.660 +\<close> ML \<open>
26.661 +(*old*)val itms = (flat o (map (M_Match.chk1_ pbt))) oris;
26.662 +(*+isa2*)val 3 = length itms
26.663 +\<close> ML \<open>
26.664 +(*old*)val mvat = I_Model.variables itms;
26.665 +(*+isa2*)val "[[0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2], [c, c_2, c_3, c_4], ss''']"
26.666 + = mvat |> UnparseC.terms @{context}
26.667 +\<close> ML \<open>
26.668 +(*old*)val complete = M_Match.chk1_mis mvat itms pbt;
26.669 +(*+isa2*)val true = complete
26.670 +\<close> ML \<open>
26.671 +(*old*)val (pb as true, _(*where_'*)) = Pre_Conds.check ctxt where_rls where_ itms mvat;
26.672 +\<close> ML \<open>
26.673 +\<close> ML \<open>
26.674 +(*----------------------vvvvvvvvv---------------------------------------------------------------*)
26.675 +"~~~~~ fun match_oris , NEWNEWNEW args:"; val (ctxt, where_rls, o_model, (model_pattern, where_)) =
26.676 + (ctxt, where_rls, ori, (model, where_));
26.677 +\<close> ML \<open>
26.678 +(*new*)val i_model = (flat o (map (M_Match.chk1_ pbt))) o_model;
26.679 +\<close> ML \<open>
26.680 +(*+*)if "[\n" ^
26.681 + "(1 ,[1] ,true ,#Given ,Cor equalities\n [0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2] ,(e_s, [[0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]])), \n" ^
26.682 + "(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2, c_3, c_4] ,(v_s, [[c, c_2, c_3, c_4]])), \n" ^
26.683 + "(3 ,[1] ,true ,#Find ,Cor solution ss''' ,(ss''', [ss''']))]"
26.684 + = (i_model |> I_Model.to_string @{context}) then () else raise error "i_model CAHNGED";
26.685 +\<close> ML \<open>
26.686 +(*new*)val (pb as true, (** )_( **)where_'(**)) = Pre_Conds.check_OLD ctxt where_rls where_
26.687 + (model_pattern, I_Model.OLD_to_TEST i_model);
26.688 +\<close> ML \<open>
26.689 +(*+*)val [(true, xxx), (true, yyy)] = where_'
26.690 +\<close> ML \<open>
26.691 +(*+*)val "[Length\n [0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2] =\n4, Length [c, c_2, c_3, c_4] = 4]"
26.692 + = where_' |> map #2 |> UnparseC.terms @{context}
26.693 +\<close> ML \<open>
26.694 +"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
26.695 + (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST itms));
26.696 +\<close> ML \<open>
26.697 + val (_, env_model, (env_subst, env_eval)) =
26.698 + of_max_variant model_patt i_model
26.699 +\<close> ML \<open>
26.700 +(*eqsy*)val "[\"\n(e_s, [0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2])\", \"\n(v_s, [c, c_2, c_3, c_4])\", \"\n(ss''', ss''')\"]" = env_model |> Subst.to_string @{context} (*should \<rightarrow> []*)
26.701 +(*eqsy*)val "[]" = env_subst |> Subst.to_string @{context} (* \<rightarrow> []*)
26.702 +\<close> ML \<open>
26.703 +"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
26.704 +\<close> ML \<open>
26.705 + val all_variants =
26.706 + map (fn (_, variants, _, _, _) => variants) i_model
26.707 + |> flat
26.708 + |> distinct op =
26.709 + val variants_separated = map (filter_variants' i_model) all_variants
26.710 + val sums_corr = map (cnt_corrects) variants_separated
26.711 + val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
26.712 + val (_, max_variant) = hd (*..crude decision, up to improvement *)
26.713 + (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
26.714 + val i_model_max =
26.715 + filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
26.716 + val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
26.717 +
26.718 + val env_model = make_env_model equal_descr_pairs
26.719 + val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
26.720 +\<close> ML \<open>
26.721 + val subst_eval_list =
26.722 + make_envs_preconds equal_givens
26.723 +\<close> ML \<open>
26.724 +"~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
26.725 +\<close> ML \<open>
26.726 +"~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 1 equal_givens);
26.727 +\<close> ML \<open>
26.728 +"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) =
26.729 + (id, feedb);
26.730 +\<close> ML \<open>
26.731 +val return_discern_typ as [] =
26.732 + discern_typ id (descr, ts);
26.733 +\<close> ML \<open>
26.734 +"~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts));
26.735 +\<close> ML \<open>
26.736 +(*+*)val "[[0 = - 1 * c_4 / - 1], [0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24], [0 = c_2], [0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]]"
26.737 + = ts |> UnparseC.terms @{context}
26.738 +\<close> ML \<open>
26.739 + (*if*) Model_Pattern.typ_of_element descr = HOLogic.boolT (*then*);
26.740 +\<close> ML \<open>
26.741 +(*+*)val false = all_lhs_atoms ts
26.742 +(*-------------------- contine check_OLD -----------------------------------------------------*)
26.743 +
26.744 + val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
26.745 +\<close> ML \<open>
26.746 +(*+*)if "[\"\n" ^
26.747 + "(e_s, [0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2])\", \"\n" ^
26.748 + "(v_s, [c, c_2, c_3, c_4])\", \"\n(ss''', ss''')\"]"
26.749 + = (env_model |> Subst.to_string @{context}) then () else error "env_model CAHNGED";
26.750 +\<close> ML \<open>
26.751 +(*+*)val "[]" = env_eval |> Subst.to_string @{context} (*GOON \<rightarrow> []*)
26.752 +\<close> ML \<open>
26.753 + val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
26.754 +\<close> ML \<open>
26.755 + val full_subst = if env_eval = [] then pres_subst_other
26.756 + else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
26.757 +\<close> ML \<open>
26.758 + val evals = map (eval ctxt where_rls) full_subst
26.759 +\<close> ML \<open>
26.760 +val return_check_OLD = (foldl and_ (true, map fst evals), pres_subst_other)
26.761 +\<close> ML \<open>
26.762 +\<close> ML \<open>
26.763 +\<close> ML \<open>
26.764 +\<close> ML \<open>
26.765 +val return_refin as SOME ["system", "LINEAR", "4x4"] = SOME (pblRD(** ) @ [pI]( **))
26.766 +\<close> ML \<open>
26.767 +(*follow the trace created in parallel by writeln in Store.get_node and Refine.refin*)
26.768 +(*!*)val pblID = ["normalise", "4x4", "LINEAR", "system"];(**)
26.769 +(*isa*)val return_refin as SOME ["system", "LINEAR", "4x4", "normalise", "normalise"] = (**)
26.770 +(*isa2* )val return_refin as SOME ["system", "LINEAR", "4x4", "normalise", "normalise"] = ( **)
26.771 + refin ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));
26.772 +\<close> ML \<open>
26.773 +"~~~~~ fun refin , args:"; val (ctxt, pblRD, ori, (Store.Node (pI, [py], pys)))
26.774 + = (ctxt, (rev pblID), oris, Store.get_node (rev pblID) pblID (get_pbls ()));
26.775 +\<close> ML \<open>
26.776 +\<close> ML \<open>
26.777 +\<close> ML \<open>
26.778 +\<close>
26.779 +
26.780 +section \<open>===================================================================================\<close>
26.781 +section \<open>===== me IntegrierenUndKonstanteBestimmen2 ALL ====================================\<close>
26.782 +ML \<open>
26.783 +open Sub_Problem
26.784 +\<close> ML \<open> (*\<rightarrow> biegelinie-4.sml OR NEW biegelinie-5.sml *)
26.785 +"----------- me IntegrierenUndKonstanteBestimmen2 ALL ----------------------------------------";
26.786 +"----------- me IntegrierenUndKonstanteBestimmen2 ALL ----------------------------------------";
26.787 +"----------- me IntegrierenUndKonstanteBestimmen2 ALL ----------------------------------------";
26.788 +(*
26.789 + This test is deeply nested (down into details of creating environments).
26.790 + In order to make Sidekick show the structure add to each
26.791 + * (*/...\*) and (*\.../*)
26.792 + * a companion > ML < (*/...\*) and > ML < (*\.../*)
26.793 + Note the wrong ^----^ delimiters.
26.794 +*)
26.795 +val fmz = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
26.796 + "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
26.797 + "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
26.798 + "AbleitungBiegelinie dy"];
26.799 +val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
26.800 + ["IntegrierenUndKonstanteBestimmen2"]);
26.801 +val p = e_pos'; val c = [];
26.802 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))]; val Model_Problem = nxt
26.803 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Traegerlaenge L" = nxt
26.804 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Streckenlast q_0" = nxt
26.805 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Biegelinie y" = nxt
26.806 +(*/---broken elementwise input to lists---\* )
26.807 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)
26.808 +(*[], 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]"*)
26.809 +( *\---broken elementwise input to lists---/*)
26.810 +(*[], 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
26.811 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
26.812 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["Biegelinien"] = nxt
26.813 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
26.814 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "FunktionsVariable x" = nxt
26.815 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]" = nxt
26.816 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy" = nxt
26.817 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
26.818 +\<close> ML \<open>
26.819 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
26.820 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Streckenlast q_0" = nxt
26.821 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "FunktionsVariable x" = nxt
26.822 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Funktionen funs'''" = nxt
26.823 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
26.824 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["vonBelastungZu", "Biegelinien"] = nxt
26.825 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["Biegelinien", "ausBelastung"] = nxt
26.826 +(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Biegelinie y" = nxt
26.827 +(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy" = nxt
26.828 +(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["Biegelinien", "ausBelastung"] = nxt
26.829 +\<close> ML \<open>
26.830 +(*[1, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("sym_neg_equal_iff_equal", _) = nxt
26.831 +(*[1, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("Belastung_Querkraft", _) = nxt
26.832 +(*[1, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["named", "integrate", "function"]) = nxt
26.833 +(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
26.834 +(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "functionTerm (- q_0)" = nxt
26.835 +(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "integrateBy x" = nxt
26.836 +(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "antiDerivativeName Q" = nxt
26.837 +(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
26.838 +(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["named", "integrate", "function"] = nxt
26.839 +(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["diff", "integration", "named"] = nxt
26.840 +(*[1, 3], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["diff", "integration", "named"] = nxt
26.841 +\<close> ML \<open>
26.842 +(*[1, 3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set_Inst (["(''bdv'', x)"], "simplify_Integral") = nxt
26.843 +(*[1, 3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set_Inst (["(''bdv'', x)"], "integration") = nxt
26.844 +(*[1, 3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Check_Postcond ["named", "integrate", "function"] = nxt
26.845 +\<close> ML \<open>
26.846 +(*[1, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("Querkraft_Moment", _) = nxt
26.847 +(*[1, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["named", "integrate", "function"]) = nxt
26.848 +(*[1, 5], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
26.849 +(*[1, 5], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "functionTerm (c + - 1 * q_0 * x)" = nxt
26.850 +(*[1, 5], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "integrateBy x" = nxt
26.851 +(*[1, 5], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "antiDerivativeName M_b" = nxt
26.852 +(*[1, 5], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
26.853 +(*[1, 5], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["named", "integrate", "function"] = nxt
26.854 +(*[1, 5], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["diff", "integration", "named"] = nxt
26.855 +(*[1, 5], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["diff", "integration", "named"] = nxt
26.856 +\<close> ML \<open>
26.857 +(*[1, 5, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set_Inst (["(''bdv'', x)"], "integration") = nxt
26.858 +(*[1, 5, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Check_Postcond ["named", "integrate", "function"] = nxt
26.859 +\<close> ML \<open>
26.860 +(*[1, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("Moment_Neigung", _) = nxt
26.861 +(*[1, 6], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("make_fun_explicit", _) = nxt
26.862 +(*[1, 7], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["named", "integrate", "function"]) = nxt
26.863 +(*[1, 8], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
26.864 +(*[1, 8], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "functionTerm (1 / - EI * (c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2))" = nxt
26.865 +(*[1, 8], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "integrateBy x" = nxt
26.866 +(*[1, 8], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "antiDerivativeName dy" = nxt
26.867 +(*[1, 8], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
26.868 +(*[1, 8], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["named", "integrate", "function"] = nxt
26.869 +(*[1, 8], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["diff", "integration", "named"] = nxt
26.870 +(*[1, 8], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["diff", "integration", "named"] = nxt
26.871 +\<close> ML \<open>
26.872 +(*[1, 8, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set_Inst (["(''bdv'', x)"], "simplify_Integral") = nxt
26.873 +(*[1, 8, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set_Inst (["(''bdv'', x)"], "integration") = nxt
26.874 +(*[1, 8, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Check_Postcond ["named", "integrate", "function"] = nxt
26.875 +\<close> ML \<open>
26.876 +(*[1, 8], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["named", "integrate", "function"]) = nxt
26.877 +(*[1, 9], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
26.878 +(*[1, 9], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "functionTerm\n (c_3 +\n 1 / (- 1 * EI) *\n (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3))" = nxt
26.879 +(*[1, 9], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "integrateBy x" = nxt
26.880 +(*[1, 9], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "antiDerivativeName y" = nxt
26.881 +(*[1, 9], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
26.882 +(*[1, 9], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["named", "integrate", "function"] = nxt
26.883 +(*[1, 9], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["diff", "integration", "named"] = nxt
26.884 +(*[1, 9], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["diff", "integration", "named"] = nxt
26.885 +\<close> ML \<open>
26.886 +(*[1, 9, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set_Inst (["(''bdv'', x)"], "integration") = nxt
26.887 +(*[1, 9, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Check_Postcond ["named", "integrate", "function"] = nxt
26.888 +(*[1, 9], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Check_Postcond ["vonBelastungZu", "Biegelinien"] = nxt
26.889 +(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["setzeRandbedingungen", "Biegelinien"]) = nxt
26.890 +\<close> ML \<open>
26.891 +(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
26.892 +(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Funktionen\n [Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n dy x =\n c_3 +\n 1 / (- 1 * EI) *\n (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]" = nxt
26.893 +(*/---broken elementwise input to lists---\* )
26.894 +(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)
26.895 +(*[2], 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]"*)
26.896 +( *\---broken elementwise input to lists---/*)
26.897 +(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" = nxt
26.898 +(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Gleichungen equs'''" = nxt
26.899 +(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
26.900 +(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["setzeRandbedingungen", "Biegelinien"] = nxt
26.901 +(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["Biegelinien", "setzeRandbedingungenEin"] = nxt
26.902 +(*[2], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["Biegelinien", "setzeRandbedingungenEin"] = nxt
26.903 +\<close> ML \<open>
26.904 +(*[2, 1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
26.905 +(*[2, 1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "functionEq\n (y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4))" = nxt
26.906 +(*[2, 1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "substitution (y 0 = 0)" = nxt
26.907 +(*[2, 1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "equality equ'''" = nxt
26.908 +(*[2, 1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
26.909 +(*[2, 1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["makeFunctionTo", "equation"] = nxt
26.910 +(*[2, 1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["Equation", "fromFunction"] = nxt
26.911 +(*[2, 1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["Equation", "fromFunction"] = nxt
26.912 +\<close> ML \<open>
26.913 +(*[2, 1, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["x = 0"] = nxt
26.914 +(*[2, 1, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["y 0 = 0"] = nxt
26.915 +(*[2, 1, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set "norm_Rational" = nxt
26.916 +(*[2, 1, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Check_Postcond ["makeFunctionTo", "equation"] = nxt
26.917 +\<close> ML \<open>
26.918 +(*[2, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["makeFunctionTo", "equation"]) = nxt
26.919 +(*[2, 2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
26.920 +(*[2, 2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "functionEq\n (y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4))" = nxt
26.921 +(*[2, 2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "substitution (y L = 0)" = nxt
26.922 +(*[2, 2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "equality equ'''" = nxt
26.923 +(*[2, 2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
26.924 +(*[2, 2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["makeFunctionTo", "equation"] = nxt
26.925 +(*[2, 2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["Equation", "fromFunction"] = nxt
26.926 +(*[2, 2], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["Equation", "fromFunction"] = nxt
26.927 +\<close> ML \<open>
26.928 +(*[2, 2, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["x = L"] = nxt
26.929 +(*[2, 2, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["y L = 0"] = nxt
26.930 +(*[2, 2, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set "norm_Rational" = nxt
26.931 +(*[2, 2, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Check_Postcond ["makeFunctionTo", "equation"] = nxt
26.932 +\<close> ML \<open>
26.933 +(*[2, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["makeFunctionTo", "equation"]) = nxt
26.934 +(*[2, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
26.935 +(*[2, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "functionEq (M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2)" = nxt
26.936 +(*[2, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "substitution (M_b 0 = 0)" = nxt
26.937 +(*[2, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "equality equ'''" = nxt
26.938 +(*[2, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
26.939 +(*[2, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["makeFunctionTo", "equation"] = nxt
26.940 +(*[2, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["Equation", "fromFunction"] = nxt
26.941 +(*[2, 3], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["Equation", "fromFunction"] = nxt
26.942 +\<close> ML \<open>
26.943 +(*[2, 3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["x = 0"] = nxt
26.944 +(*[2, 3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["M_b 0 = 0"] = nxt
26.945 +(*[2, 3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set "norm_Rational" = nxt
26.946 +(*[2, 3, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Check_Postcond ["makeFunctionTo", "equation"] = nxt
26.947 +\<close> ML \<open>
26.948 +(*[2, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["makeFunctionTo", "equation"]) = nxt
26.949 +(*[2, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
26.950 +(*[2, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "functionEq (M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2)" = nxt
26.951 +(*[2, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "substitution (M_b L = 0)" = nxt
26.952 +(*[2, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "equality equ'''" = nxt
26.953 +(*[2, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
26.954 +(*[2, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["makeFunctionTo", "equation"] = nxt
26.955 +(*[2, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["Equation", "fromFunction"] = nxt
26.956 +(*[2, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["Equation", "fromFunction"] = nxt
26.957 +\<close> ML \<open>
26.958 +(*[2, 4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["x = L"] = nxt
26.959 +(*[2, 4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["M_b L = 0"] = nxt
26.960 +(*[2, 4, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set "norm_Rational" = nxt
26.961 +(*[2, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Check_Postcond ["makeFunctionTo", "equation"] = nxt
26.962 +(*[2, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Check_Postcond ["setzeRandbedingungen", "Biegelinien"] = nxt
26.963 +
26.964 +\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
26.965 +(*[2], Res*)val return_Check_Postcond_setzeRandbedingungen = me nxt p c pt;
26.966 +\<close> ML \<open> (*/------------ step into me_Check_Postcond_setzeRandbedingungen --------------------\\*)
26.967 +(*/------------------- step into me_Check_Postcond_setzeRandbedingungen --------------------\\*)
26.968 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
26.969 +\<close> ML \<open>
26.970 + val ctxt = Ctree.get_ctxt pt p
26.971 +\<close> ML \<open>
26.972 + val (pt, p) =
26.973 + case Step.by_tactic tac (pt, p) of
26.974 + ("ok", (_, _, ptp)) => ptp
26.975 +\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
26.976 + (*case*)
26.977 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
26.978 +\<close> ML \<open>
26.979 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
26.980 +\<close> ML \<open>
26.981 + (*if*) Pos.on_calc_end ip (*else*);
26.982 + val (_, probl_id, _) = Calc.references (pt, p);
26.983 +\<close> ML \<open>
26.984 +val _ =
26.985 + (*case*) tacis (*of*);
26.986 +\<close> ML \<open>
26.987 + (*if*) probl_id = Problem.id_empty (*else*);
26.988 +\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
26.989 + switch_specify_solve p_ (pt, ip);
26.990 +\<close> ML \<open>
26.991 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
26.992 +\<close> ML \<open>
26.993 + (*if*) Pos.on_specification ([], state_pos) (*else*);
26.994 +\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
26.995 + LI.do_next (pt, input_pos)
26.996 +\<close> ML \<open>
26.997 +"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
26.998 +\<close> ML \<open>
26.999 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
26.1000 +\<close> ML \<open>
26.1001 + val ((ist, ctxt), sc) = LItool.resume_prog pos pt;
26.1002 +\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
26.1003 +val Next_Step (Pstate _, _, Subproblem' _) =
26.1004 + (*case*) find_next_step sc ptp ist ctxt (*of*);
26.1005 +\<close> ML \<open>
26.1006 +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)
26.1007 + = (sc, ptp, ist, ctxt);
26.1008 +\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
26.1009 +val Accept_Tac (Subproblem' _, _, _) =
26.1010 + (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
26.1011 +\<close> ML \<open>
26.1012 +"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
26.1013 + = ((prog, (ptp, ctxt)), (Pstate ist));
26.1014 +\<close> ML \<open>
26.1015 + (*if*) path = [] (*else*);
26.1016 +\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
26.1017 +val Accept_Tac (Subproblem' _, _, _) =
26.1018 + go_scan_up (prog, cc) (trans_scan_up ist);
26.1019 +\<close> ML \<open>
26.1020 +"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, (_, ctxt))), (ist as {path, act_arg, found_accept, ...}))
26.1021 + = ((prog, cc), (trans_scan_up ist));
26.1022 +\<close> ML \<open>
26.1023 + (*if*) path = [R] (*root of the program body*) (*else*);
26.1024 +\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
26.1025 + scan_up pcc (ist |> path_up) (go_up ctxt path sc)
26.1026 +\<close> ML \<open>
26.1027 +"~~~~~ and scan_up , args:"; val ((pcc as (sc, cc as (_, ctxt))), ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ _))
26.1028 + = (pcc, (ist |> path_up), (go_up ctxt path sc));
26.1029 +\<close> ML \<open>
26.1030 + val (i, body) = check_Let_up ctxt ist sc
26.1031 +\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
26.1032 +val Accept_Tac (Subproblem' _, _, _) =
26.1033 + (*case*) scan_dn cc (ist |> path_up_down [R, D] |> upd_env i) body (*of*);
26.1034 +\<close> ML \<open>
26.1035 +"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))))
26.1036 + = (cc, (ist |> path_up_down [R, D] |> upd_env i), body);
26.1037 +\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
26.1038 +val Accept_Tac (Subproblem' _, _, _) =
26.1039 + (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*);
26.1040 +\<close> ML \<open>
26.1041 +"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t (*fall-through*))
26.1042 + = (cc, (ist |> path_down [L, R]), e);
26.1043 +\<close> ML \<open>
26.1044 + (*if*) Tactical.contained_in t (*else*);
26.1045 +\<close> ML \<open>
26.1046 +val (Program.Tac prog_tac, form_arg) =
26.1047 + (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
26.1048 +\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
26.1049 + check_tac cc ist (prog_tac, form_arg);
26.1050 +\<close> ML \<open>
26.1051 +"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))
26.1052 + = (cc, ist, (prog_tac, form_arg));
26.1053 +\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
26.1054 + val Subproblem ("Biegelinie", ["normalise", "4x4", "LINEAR", "system"]) =
26.1055 + LItool.tac_from_prog (pt, p) prog_tac;
26.1056 +\<close> ML \<open>
26.1057 +"~~~~~ fun tac_from_prog , args:"; val ((pt, pos), intac)
26.1058 + = ((pt, p), prog_tac);
26.1059 +\<close> ML \<open>
26.1060 + val pos = Pos.back_from_new pos
26.1061 + val ctxt = Ctree.get_ctxt pt pos
26.1062 + val thy = Proof_Context.theory_of ctxt
26.1063 +\<close> ML \<open>
26.1064 +val (ptac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ _ $ _) =
26.1065 + (*case*) intac (*of*)
26.1066 +\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
26.1067 +val Subproblem ("Biegelinie", ["normalise", "4x4", "LINEAR", "system"]) =
26.1068 + fst (Sub_Problem.tac_from_prog (pt, pos) ptac) (*might involve problem refinement etc*)
26.1069 +\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
26.1070 +val (Subproblem _, Subproblem' _) =
26.1071 +Sub_Problem.tac_from_prog (pt, pos) ptac;
26.1072 +\<close> ML \<open>
26.1073 +"~~~~~ fun tac_from_prog , args:"; val ((pt, p), (stac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ spec' $ ags'))
26.1074 + = ((pt, pos), ptac);
26.1075 +\<close> ML \<open>
26.1076 + val (dI, pI, mI) = Prog_Tac.dest_spec spec'
26.1077 +(*+*)val ("Biegelinie", ["LINEAR", "system"], ["no_met"]) = Prog_Tac.dest_spec spec'
26.1078 +
26.1079 + val thy = common_sub_thy (Know_Store.get_via_last_thy dI, Ctree.root_thy pt);
26.1080 + val init_ctxt = Proof_Context.init_global thy
26.1081 + val ags = TermC.isalist2list ags';
26.1082 +\<close> ML \<open>
26.1083 + (*if*) mI = ["no_met"] (*then*);
26.1084 + val pors = (M_Match.arguments thy ((#model o (Problem.from_store init_ctxt)) pI) ags): O_Model.T
26.1085 +\<close> ML \<open>
26.1086 +(*+*)if (pors |> O_Model.to_string @{context}) = "[\n" ^
26.1087 + "(1, [\"1\"], #Given, equalities, [\"[0 = - 1 * c_4 / - 1]\", " ^
26.1088 + "\"[0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24]\", " ^
26.1089 + "\"[0 = c_2]\", " ^
26.1090 + "\"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]" ^
26.1091 + "\"]), \n" ^
26.1092 + "(2, [\"1\"], #Given, solveForVars, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
26.1093 + "(3, [\"1\"], #Find, solution, [\"ss'''\"])]" then () else error "pors CHANGED";
26.1094 +\<close> ML \<open>
26.1095 + val pI' = Refine.refine_ori' init_ctxt pors pI;
26.1096 +\<close> ML \<open>
26.1097 +(*+*)val ["normalise", "4x4", "LINEAR", "system"] = pI';
26.1098 +\<close> ML \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
26.1099 +val return_tac_from_prog_step = (pI', pors (* refinement over models with diff.precond only *),
26.1100 + (hd o #solve_mets o Problem.from_store init_ctxt) pI');
26.1101 +\<close> ML \<open>
26.1102 + (Problem.from_store init_ctxt) pI'; (*.., solve_mets = [], ...*)
26.1103 +\<close> ML \<open>
26.1104 +val [["EqSystem", "normalise", "4x4"]] =
26.1105 + (#solve_mets o Problem.from_store init_ctxt) pI';
26.1106 +\<close> ML \<open>
26.1107 +\<close> ML \<open>
26.1108 +\<close> ML \<open>
26.1109 +\<close> ML \<open> (*|------------ contine me_Check_Postcond_setzeRandbedingungen ------------------------*)
26.1110 +(*|------------------- contine me_Check_Postcond_setzeRandbedingungen ------------------------*)
26.1111 +(*\------------------- step into me_Check_Postcond_setzeRandbedingungen --------------------//*)
26.1112 +\<close> ML \<open> (*\------------ step into me_Check_Postcond_setzeRandbedingungen --------------------//*)
26.1113 +\<close> text \<open>
26.1114 +val (p,_,f,nxt,_,pt) = return_Check_Postcond_setzeRandbedingungen;
26.1115 +\<close> ML \<open>
26.1116 +\<close> ML \<open>
26.1117 +\<close> ML \<open>
26.1118 +\<close> ML \<open>
26.1119 +\<close>
26.1120 +
26.1121 section \<open>===================================================================================\<close>
26.1122 section \<open>===== ============================================================================\<close>
26.1123 ML \<open>