1.1 --- a/test/Tools/isac/Minisubpbl/000-comments.sml	Wed Oct 25 12:34:12 2023 +0200
     1.2 +++ b/test/Tools/isac/Minisubpbl/000-comments.sml	Thu Oct 26 10:29:17 2023 +0200
     1.3 @@ -3,7 +3,11 @@
     1.4     (c) copyright due to lincense terms.
     1.5  *)
     1.6  
     1.7 -(* The tests in this directory use one specific example exclusively.
     1.8 +(* The tests in this directory use specific example exclusively
     1.9 +  * nnn-   Minisubpbl      me + Step.do_next
    1.10 +  * nnna-  Maximum-example me + Step.do_next
    1.11 +  * nnnb-  biegel          me + Step.do_next
    1.12 +  nnn- are specific:
    1.13    The example uses data specifically defined in Test.thy exclusively.
    1.14    The example covers the essential features of isac's mathengine.
    1.15    Each test is kept in a separate file.
    1.16 @@ -19,4 +23,10 @@
    1.17    500  shift interpretation from sub-method to root-method
    1.18    550  found error in Check_Elementwise Assumptions
    1.19    600  check postconditions of subproblem and rootproblem
    1.20 +
    1.21 +  These examples step into relevant low level functions and help to develop respective new code.
    1.22 +  Goal:
    1.23 +  Outside this directory tests cover high level functions in order to support surveys.
    1.24 +  Currently many of tests outside address repair of errors with specific examples;
    1.25 +    these shall be removed and respective details be covered by "Minisubpbl" -?-> "Step_Tests"
    1.26  *)

     2.1 --- a/test/Tools/isac/Test_Theory.thy	Wed Oct 25 12:34:12 2023 +0200
     2.2 +++ b/test/Tools/isac/Test_Theory.thy	Thu Oct 26 10:29:17 2023 +0200
     2.3 @@ -30,6 +30,7 @@
     2.4  (*if*) (*then*); (*else*); (*andalso*)  (*case*) (*of*);  (*return value*); (*in*) (*end*);
     2.5  "xx"
     2.6  ^ "xxx"   (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)
     2.7 +
     2.8  \<close> ML \<open> (*//----------- build fun XXXXX -----------------------------------------------------\\*)
     2.9  (*//------------------ build fun XXXXX -----------------------------------------------------\\*)
    2.10  (*\\------------------ build fun XXXXX -----------------------------------------------------//*)
    2.11 @@ -68,110 +69,12 @@
    2.12  \<close>
    2.13  
    2.14  section \<open>===================================================================================\<close>
    2.15 -section \<open>===== new code match_itms_oris ====================================================\<close>
    2.16 +section \<open>=====  ============================================================================\<close>
    2.17  ML \<open>
    2.18  \<close> ML \<open>
    2.19 -open Ctree;
    2.20 -open Pos;
    2.21 -open TermC;
    2.22 -open Istate;
    2.23 -open Tactic;
    2.24 -open I_Model;
    2.25 -open P_Model
    2.26 -open Rewrite;
    2.27 -open Step;
    2.28 -open LItool;
    2.29 -open LI;
    2.30 -open Test_Code
    2.31 -open Specify
    2.32 -open ME_Misc
    2.33 -open Pre_Conds;
    2.34 -\<close> ML \<open> (*//----------- build fun match_itms_oris -------------------------------------------\\*)
    2.35 -(*//------------------ build fun match_itms_oris -------------------------------------------\\*)
    2.36 -\<close> ML \<open>
    2.37 -\<close> text \<open> (*\<longrightarrow> model-def.sml*)
    2.38 -fun member_vnt [] _ = true
    2.39 -  | member_vnt vnts vnt = member op= vnts vnt
    2.40 -;
    2.41 -member_vnt: variants -> variant -> bool
    2.42 -\<close> ML \<open>
    2.43 -\<close> text \<open> (*\<longrightarrow> i-model.sml   <> Pre_Conds.get_descr_vnt*)
    2.44 -(*
    2.45 -  in case there is an item in i2_model = met with Sup_TEST, 
    2.46 -  find_first an appropriate (variant, descriptor) item in i1_model = pbl and add it instead Sup_TEST,
    2.47 -  otherwise keep the items of i2_model.
    2.48 -*)
    2.49 -fun add_other max_vnt i1_model (i2, _, bool2, m_field2, (Sup_TEST (descr2, ts2), pos2)) =
    2.50 -    (case find_first (fn (_, vnts1, _, _, (feedb1, _)) => case Pre_Conds.get_dscr' feedb1 of
    2.51 -          NONE => false
    2.52 -        | SOME descr1 => descr1 = descr2 andalso Model_Def.member_vnt vnts1 max_vnt) i1_model of
    2.53 -      NONE =>
    2.54 -        (i2, [max_vnt], bool2, m_field2, (Sup_TEST (descr2, ts2), pos2)) (*the present in i2_model*)
    2.55 -    | SOME i1_single => i1_single)                      (*shift the item from i1_model to i2_model*)
    2.56 -  | add_other _ _ i2_single = i2_single                     (*keep all the other items in i2_model*)
    2.57 -;
    2.58 -add_other: variant -> I_Model.T_TEST -> I_Model.single_TEST -> I_Model.single_TEST
    2.59 -\<close> ML \<open>
    2.60 -\<close> text \<open> (*\<longrightarrow> i-model.sml*)
    2.61 -(*
    2.62 -  Establish the order of items (wrt. descriptor) in the method's i_model as given by meth_patt,
    2.63 -  i.e as required by the formal arguments of the program.
    2.64 -  Missing items are inserted as Sup(erfluous).
    2.65 -/-TODO-----------------------^^-Inc [] ------- output with input-template automatically------\
    2.66 -\-TODO---------------------------------------------------------------------------------------/
    2.67 -  In order to maintain what the user sees as Model, copy the items from the problem's i_model
    2.68 -  to the method's i_model.
    2.69 -*)
    2.70 -(*compare fun s_make_complete*)
    2.71 -fun fill_method o_model (pbl_imod, met_imod) met_patt =
    2.72 -  let
    2.73 -    val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod
    2.74 -    (*probably pbl/met_imod = [], so take met_patt; if empty return Sup*)
    2.75 -    val i_from_met = map (fn (_, (descr, _)) => (*order from met_patt*)
    2.76 -      Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt (*\<longrightarrow> right order for args*)
    2.77 -
    2.78 -    val met_max_vnts = Model_Def.max_variants o_model i_from_met;
    2.79 -    val max_vnt = hd (inter op= pbl_max_vnts met_max_vnts);
    2.80 -    (*add items from pbl_imod (without overwriting existing items in met_imod)*)
    2.81 -  in
    2.82 -    map (add_other max_vnt pbl_imod) i_from_met
    2.83 -  end 
    2.84 -;
    2.85 -fill_method: O_Model.T -> I_Model.T_TEST * I_Model.T_TEST-> Model_Pattern.T ->
    2.86 -    I_Model.T_TEST
    2.87 -\<close> ML \<open>
    2.88 -\<close> ML \<open> (*\<longrightarrow> m-match.sml*)
    2.89 -(*the OLD version built upon a wrong idea with find missing items from o_model*)
    2.90 -\<close> ML \<open>
    2.91 -(*OLD*)
    2.92 -(*---*)
    2.93 -fun match_itms_oris ctxt o_model (pbl_imod, met_imod) (met_patt, where_, where_rls) =
    2.94 -  let
    2.95 -    val met_imod = I_Model.fill_method o_model (pbl_imod, met_imod) met_patt
    2.96 -    val (check, preconds) = Pre_Conds.check ctxt where_rls where_ (met_patt, met_imod)
    2.97 -  in    
    2.98 -   (check, (met_imod, preconds))
    2.99 -  end
   2.100 -(*NEW*)
   2.101 -;
   2.102 -match_itms_oris: Proof.context -> O_Model.T -> I_Model.T_TEST * I_Model.T_TEST ->
   2.103 -    Model_Pattern.T * Pre_Conds.unchecked * Rule_Def.rule_set ->
   2.104 -      bool * (I_Model.T_TEST * Pre_Conds.T)
   2.105 -\<close> ML \<open>
   2.106 -(*\\------------------ build fun match_itms_oris -------------------------------------------//*)
   2.107 -\<close> ML \<open> (*\\----------- build fun match_itms_oris -------------------------------------------//*)
   2.108 -\<close> ML \<open>
   2.109 -\<close>
   2.110 -
   2.111 -(*ML_file "Minisubpbl/100-init-rootpbl-NEXT_STEP.sml" (*get from isa-a-.. -----------------*)
   2.112 -section \<open>===================================================================================\<close>
   2.113 -section \<open>=====  ============================================================================\<close>
   2.114 -ML \<open> 
   2.115 -\<close> ML \<open>
   2.116  
   2.117  \<close> ML \<open>
   2.118  \<close>
   2.119 ----------------------------------------------------------------------- testing unnecessary *)
   2.120  
   2.121  (*ML_file "Minisubpbl/150a-add-given-Maximum.sml"*)
   2.122  section \<open>===================================================================================\<close>
   2.123 @@ -461,6 +364,21 @@
   2.124              (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);
   2.125  "~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
   2.126    = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, pbt, pbl);
   2.127 +\<close> ML \<open> (*//----------- build fun item_to_add -----------------------------------------------\\*)
   2.128 +(*//------------------ build fun item_to_add -----------------------------------------------\\*)
   2.129 +\<close> ML \<open> (*shift this block up in separate section a.s.a.p*)
   2.130 +\<close> ML \<open>
   2.131 +\<close> ML \<open>
   2.132 +\<close> ML \<open>
   2.133 +\<close> ML \<open>
   2.134 +\<close> ML \<open>
   2.135 +\<close> ML \<open>
   2.136 +\<close> ML \<open>
   2.137 +\<close> ML \<open>
   2.138 +\<close> ML \<open>
   2.139 +\<close> ML \<open>
   2.140 +(*\\------------------ build fun item_to_add -----------------------------------------------//*)
   2.141 +\<close> ML \<open> (*\\----------- build fun item_to_add -----------------------------------------------//*)
   2.142        fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
   2.143          | false_and_not_Sup (_, _, false, _, _) = true
   2.144          | false_and_not_Sup _ = false
   2.145 @@ -1000,7 +918,7 @@
   2.146  (*OLD* )
   2.147     M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
   2.148  ( *---*)
   2.149 -           match_itms_oris ctxt o_model' (I_Model.OLD_to_TEST i_prob, I_Model.OLD_to_TEST i_prob)
   2.150 +     M_Match.match_itms_oris ctxt o_model' (I_Model.OLD_to_TEST i_prob, I_Model.OLD_to_TEST i_prob)
   2.151                (m_patt, where_, where_rls);
   2.152  (*NEW*)
   2.153  \<close> ML \<open> (*///---------- step into match_itms_oris -------------------------------------------\\*)