wneuper/isa: test/Tools/isac/Test

     1 theory Test_Some

     2   imports "Isac.Build_Isac" "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"

     3 begin

     5 ML \<open>open ML_System\<close>

     6 ML \<open>

     7   open Kernel;

     8   open Math_Engine;

     9   open Test_Code;              CalcTreeTEST;

    10   open LItool;                 arguments_from_model;

    11   open Sub_Problem;

    12   open Fetch_Tacs;

    13   open Step

    14   open Env;

    15   open LI;                     scan_dn;

    16   open Istate;

    17   open Error_Pattern;

    18   open Error_Pattern_Def;

    19   open Specification;

    20   open Ctree;                  append_problem;

    21   open Pos;

    22   open Program;

    23   open Prog_Tac;

    24   open Tactical;

    25   open Prog_Expr;

    26   open Auto_Prog;              rule2stac;

    27   open Input_Descript;

    28   open Specify;

    29   open Specify;

    30   open Step_Specify;

    31   open Step_Solve;

    32   open Step;

    33   open Solve;                  (* NONE *)

    34   open ContextC;               transfer_asms_from_to;

    35   open Tactic;                 (* NONE *)

    36   open I_Model;

    37   open O_Model;

    38   open P_Model;                (* NONE *)

    39   open Rewrite;

    40   open Eval;                   get_pair;

    41   open TermC;                  atomt;

    42   open Rule;

    43   open Rule_Set;               Sequence;

    44   open Eval_Def

    45   open ThyC

    46   open ThmC_Def

    47   open ThmC

    48   open Rewrite_Ord

    49   open UnparseC

    50 \<close>

    51 (**)ML_file "BridgeJEdit/vscode-example.sml"(**)

    53 section \<open>code for copy & paste ===============================================================\<close>

    54 ML \<open>

    55 "~~~~~ fun xxx , args:"; val () = ();

    56 "~~~~~ and xxx , args:"; val () = ();

    57 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();

    58 (*if*) (*then*); (*else*);   (*case*) (*of*);  (*return value*); (*in*) (*end*);

    59 "xx"

    60 ^ "xxx"   (*+*) (*+++*) (* keep for continuation*) (*isa*) (*isa2*) (**)

    61 \<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)

    62  (*//----------------- adhoc inserted n ----------------------------------------------------\\*)

    63 (*\\------------------ adhoc inserted n ----------------------------------------------------//*)

    64 \<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)

    66 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)

    67 (*//------------------ step into XXXXX -----------------------------------------------------\\*)

    68 (*-------------------- stop step into XXXXX --------------------------------------------------*)

    69 \<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*)

    70 (*\\------------------ step into XXXXX -----------------------------------------------------//*)

    71 \<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)

    73 (*/------------------- check entry to XXXXX -------------------------------------------------\*)

    74 (*\------------------- check entry to XXXXX -------------------------------------------------/*)

    75 (*/------------------- check within XXXXX ---------------------------------------------------\*)

    76 (*\------------------- check within XXXXX ---------------------------------------------------/*)

    77 (*/------------------- check result of XXXXX ------------------------------------------------\*)

    78 (*\------------------- check result of XXXXX ------------------------------------------------/*)

    79 (* final test ... ----------------------------------------------------------------------------*)

    81 \<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*)

    82 (*//------------------ build new fun XXXXX -------------------------------------------------\\*)

    83 (*\\------------------ build new fun XXXXX -------------------------------------------------//*)

    84 \<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*)

    85 \<close> ML \<open>

    86 \<close>

    87 ML \<open>

    88 \<close> ML \<open>

    89 \<close> ML \<open>

    90 \<close>

    91 text \<open>

    92   declare [[show_types]]

    93   declare [[show_sorts]]

    94   find_theorems "?a <= ?a"

    96   print_theorems

    97   print_facts

    98   print_statement ""

    99   print_theory

   100   ML_command \<open>Pretty.writeln prt\<close>

   101   declare [[ML_print_depth = 999]]

   102   declare [[ML_exception_trace]]

   103 \<close>

   105 section \<open>===================================================================================\<close>

   106 ML \<open>

   107 \<close> ML \<open>

   108 \<close> ML \<open>

   109 \<close> ML \<open>

   110 \<close>

   112 section \<open>========= test/../Knowlegde/equsystem-1a.sml ======================================\<close>

   113 ML \<open>

   114 \<close> ML \<open>

   115 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";

   116 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";

   117 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";

   118 val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\

   119 	               \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",

   120 	   "solveForVars [c, c_2]", "solution LL"];

   121 val (dI',pI',mI') =

   122   ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],

   123    ["EqSystem", "normalise", "2x2"]);

   124 val p = e_pos'; val c = [];

   125 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   126 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   127 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   128 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   129 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   130 case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => ()

   131 	  | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify";

   133 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   134 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

   136 (*+*)if f2str f =

   137   "[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n" ^

   138   " 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]" then () else error "";

   139 (*+*)(Ctree.get_istate_LI pt p |> Istate.string_of) =

   140    "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\"], [], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, true)";

   142 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

   143 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

   144 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

   145 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

   147 (*+isa==isa2*)val "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]" = f2str f;

   148   val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\"], [R, L, R, L, R, R, R, L, R, R], srls_normalise_2x2, SOME e_s, \n[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2], ORundef, true, false)" =

   149 (*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of);

   151 case nxt of

   152     (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()

   153   | _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem";

   155 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   156 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   157 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   158 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

   159 case nxt of

   160     (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()

   161   | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";

   163 val (p,_,f,nxt,_,pt) = me nxt p c pt;

   165   val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n  ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =

   166 (*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of);

   168 val (p''',_,f,nxt''',_,pt''') = me nxt p c pt;f2str f;

   169 (*/------------------- step into me Apply_Method -------------------------------------------\*)

   170 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);

   171 \<close> ML \<open>

   172       val (pt'''', p'''') = (* keep for continuation*)

   173   	    (*Step.by_tactic is here for testing by me; do_next would suffice in me*)

   175  case Step.by_tactic tac (pt, p) of

   176   		    ("ok", (_, _, ptp)) => ptp;

   177 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));

   179 (*+isa==isa2*)val ([5], Met) = p;

   180 (*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt (fst p);

   181   val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n  ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =

   182 (*+isa==isa2*)is1 |> Istate.string_of;

   183   val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n  ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =

   184 (*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of);

   186   (*case*)

   187       Step.check tac (pt, p) (*of*);

   188 "~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p) );

   190 (*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n  ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =

   191 (*+isa==isa2*)(Ctree.get_istate_LI ctree pos |> Istate.string_of);

   193   (*if*) Tactic.for_specify tac (*else*);

   194 val Applicable.Yes xxx =

   196 Solve_Step.check tac (ctree, pos);

   198 (*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n  ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =

   199 (*+isa==isa2*)(Ctree.get_istate_LI ctree pos |> Istate.string_of);

   201 "~~~~~ from Step.check to Step.by_tactic return val:"; val (Applicable.Yes tac') = (Applicable.Yes xxx);

   202 	    (*if*)  Tactic.for_specify' tac' (*else*);

   204 Step_Solve.by_tactic tac' ptp;;

   205 "~~~~~ fun by_tactic , args:"; val ((tac as Tactic.Apply_Method' _), (ptp as (pt, p)))

   206   = (tac', ptp);

   208 (*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n  ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =

   209 (*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of);

   211         LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp;

   212 "~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _)))

   213   = (tac, (get_istate_LI pt p, get_ctxt_LI pt p), ptp);

   214          val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)

   215            PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)

   216          val {ppc, ...} = MethodC.from_store ctxt mI;

   217          val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc

   218          val srls = LItool.get_simplifier (pt, pos)

   219          val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of

   220            (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)

   222 (*+*)val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, true)" =

   223 (*+isa==isa2*)is |> Istate.string_of

   225         val ini = LItool.implicit_take prog env;

   226         val pos = start_new_level pos

   227 val NONE =

   228         (*case*) ini (*of*);

   229             val (tac''', ist''', ctxt''') =

   230    case LI.find_next_step prog (pt, (lev_dn p, Res)) is ctxt of

   231                 Next_Step (ist, ctxt, tac) => (tac, ist, ctxt)

   233   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =

   234 (*+isa==isa2*)ist''' |> Istate.string_of;

   236 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)

   237   = (prog ,(pt, (lev_dn p, Res)), is, ctxt);

   238 val Accept_Tac

   239     (Take' ttt, iii, _) =

   240   (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);

   242 (*+isa==isa2*)val "c_2 = 0" = (ttt |> UnparseC.term);

   243   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =

   244 (*+isa==isa2*)(Pstate iii |> Istate.string_of);

   246 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))

   247   = ((prog, (ptp, ctxt)), (Pstate ist));

   248   (*if*) path = [] (*then*);

   250            scan_dn cc (trans_scan_dn ist) (Program.body_of prog);

   251 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))))

   252   = (cc, (trans_scan_dn ist), (Program.body_of prog));

   254   (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*);

   255 "~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)

   256   = (cc ,(ist |> path_down [L, R]), e);

   258   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, false)" =

   259 (*+isa==isa2*)(Pstate ist |> Istate.string_of);

   261     (*if*) Tactical.contained_in t (*else*);

   263       (*case*)

   264     LItool.check_leaf "next  " ctxt eval (get_subst ist) t (*of*);

   265 "~~~~~ fun check_leaf , args:"; val (call, ctxt, srls, (E, (a, v)), t)

   266   = ("next  ", ctxt, eval, (get_subst ist), t);

   268     (*case*)

   269   Prog_Tac.eval_leaf E a v t (*of*);

   270 "~~~~~ fun eval_leaf , args:"; val (E, _, _, (t as (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ _)))

   271   = (E, a, v, t);

   273 val return =

   274      (Program.Tac (subst_atomic E t), NONE:term option);

   275 "~~~~~ from fun eval_leaf \<longrightarrow>fun check_leaf , return:"; val (Program.Tac stac, a') = return;

   276 	        val stac' = Rewrite.eval_prog_expr ctxt srls

   277               (subst_atomic (Env.update_opt E (a, v)) stac)

   279 val return =

   280       (Program.Tac stac', a');

   281 "~~~~~ from fun check_leaf \<longrightarrow>fun scan_dn , return:"; val (Program.Tac prog_tac, form_arg) = return;

   283            check_tac cc ist (prog_tac, form_arg);

   284 "~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))

   285   = (cc, ist, (prog_tac, form_arg));

   286     val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac

   287 val _ =

   288     (*case*) m (*of*); (*tac as string/input*)

   290       (*case*)

   291 Solve_Step.check m (pt, p) (*of*);

   292 "~~~~~ fun check , args:"; val ((Tactic.Take str), (pt, pos)) = (m, (pt, p));

   294 val return =

   295     check_tac cc ist (prog_tac, form_arg)

   297   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, false)" =

   298 (*+isa==isa2*)(Pstate ist |> Istate.string_of);

   300 "~~~~~ from fun scan_dn \<longrightarrow>fun scan_to_tactic \<longrightarrow>fun find_next_step , return:";

   301        val (Accept_Tac (tac, ist, ctxt)) = return;

   303   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =

   304 (*+isa==isa2*)(Pstate ist |> Istate.string_of)

   306 val return =

   307       Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac);

   308 "~~~~~ from fun find_next_step \<longrightarrow>fun by_tactic , return:"; val Next_Step (ist, ctxt, tac) = return;

   309             val (tac', ist', ctxt') = (tac, ist, ctxt)

   310 val Tactic.Take' t =

   311             (*case*) tac' (*of*);

   312                   val show_add = Tactic.Apply_Method' (mI, SOME t, ist', ctxt');

   314 (*+isa==isa2*)pos; (*from check_tac*)

   315 (*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt [5];

   316   val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n  ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" =

   317 (*+isa==isa2*)is1 |> Istate.string_of;

   318   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =

   319 (*+isa==isa2*)(ist' |> Istate.string_of)

   320 (*-------------------- stop step into me Apply_Method ----------------------------------------*)

   321 (*+isa==isa2*)val "c_2 = 0" = f2str f;

   322   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" =

   323 (*+isa==isa2*)(Ctree.get_istate_LI pt''' p''' |> Istate.string_of)

   324 (*\\------------------- step into me Apply_Method ------------------------------------------//*)

   326 \<close> ML \<open>

   327 val (p'''',_,f,nxt'''',_,pt'''') = me nxt''' p''' c pt''';f2str f;

   328 \<close> ML \<open>

   329 (*+isa==isa2*)val ([5, 1], Frm) = p'''';

   330 (*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = f2str f;

   331 (*+isa<>isa2*)val (**)Check_Postcond ["triangular", "2x2", "LINEAR", "system"](** )

   332                        Substitute ["c_2 = 0"]( **) = nxt'''';

   333 (*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt'''' (fst p'''');

   334   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =

   335 (*+isa==isa2*)is1 |> Istate.string_of;

   336   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =

   337 (*+isa==isa2*)Ctree.get_istate_LI pt'''' p'''' |> Istate.string_of;

   338 \<close> ML \<open> (*//----------- step into me Take ---------------------------------------------------\\*)

   339 (*//------------------ step into me Take ---------------------------------------------------\\*)

   340 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt''', p''', c, pt''');

   341 \<close> ML \<open>

   342       val (pt, p) = (* keep for continuation*)

   343   	    (*Step.by_tactic is here for testing by me; do_next would suffice in me*)

   345  case Step.by_tactic tac (pt, p) of

   346   		    ("ok", (_, _, ptp)) => ptp;

   347 \<close> ML \<open>

   348   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =

   349 (*isa==isa2*)Ctree.get_istate_LI pt p |> Istate.string_of;

   350 \<close> ML \<open>

   351     (*case*)

   352       Step.do_next p ((pt, Pos.e_pos'), []) (*of*);

   353 \<close> ML \<open>

   354 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));

   355 \<close> ML \<open>

   356   (*if*) Pos.on_calc_end ip (*else*);

   357 \<close> ML \<open>

   358       val (_, probl_id, _) = Calc.references (pt, p);

   359 \<close> ML \<open>

   360 val _ =

   361       (*case*) tacis (*of*);

   362 \<close> ML \<open>

   363         (*if*) probl_id = Problem.id_empty (*else*);

   364 \<close> ML \<open>

   365            switch_specify_solve p_ (pt, ip);

   366 \<close> ML \<open>

   367 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));

   368 \<close> ML \<open>

   369       (*if*) Pos.on_specification ([], state_pos) (*else*);

   370 \<close> ML \<open>

   371         LI.do_next (pt, input_pos);

   372 \<close> ML \<open>

   373 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);

   374 \<close> ML \<open>

   375     (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);

   376 \<close> ML \<open>

   377         val thy' = get_obj g_domID pt (par_pblobj pt p);

   378 	      val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;

   379 \<close> ML \<open>

   380   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =

   381 (*+isa==isa2*)ist |> Istate.string_of;

   382 \<close> ML \<open>

   383         (*case*)

   384         LI.find_next_step sc (pt, pos) ist ctxt (*of*);

   385 \<close> ML \<open>

   386 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)

   387   = (sc, (pt, pos), ist, ctxt);

   388 \<close> ML \<open>

   389   (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);

   390 \<close> ML \<open>

   391 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))

   392   = ((prog, (ptp, ctxt)), (Pstate ist));

   393 \<close> ML \<open>

   394   (*if*) path = [] (*else*);

   395 \<close> ML \<open>

   396            go_scan_up (prog, cc) (trans_scan_up ist);

   397 \<close> ML \<open>

   398 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))

   399   = ((prog, cc), (trans_scan_up ist));

   400 \<close> ML \<open>

   401   val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, false)" =

   402 (*+isa==isa2*)Pstate ist |> Istate.string_of;

   403 (*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = act_arg |> UnparseC.term;

   404 \<close> ML \<open>

   405     (*if*) path = [R] (*root of the program body*) (*else*);

   406 \<close> ML \<open>

   407            scan_up pcc (ist |> path_up) (go_up path sc);

   408 \<close> ML \<open>

   409 "~~~~~ and scan_up , args:"; val ((pcc as (sc, cc)), ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ _))

   410   = (pcc, (ist |> path_up), (go_up path sc));

   411 \<close> ML \<open>

   412         val (i, body) = check_Let_up ist sc

   413 \<close> ML \<open>

   414   (*case*) scan_dn cc (ist |> path_up_down [R, D] |> upd_env i) body (*of*);

   415 \<close> ML \<open>

   416 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))))

   417   = (cc, (ist |> path_up_down [R, D] |> upd_env i), body);

   418 \<close> ML \<open>

   419 val goback =

   420   (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*);

   421 \<close> ML \<open>

   422 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*1*), _) $ e1 $ e2 $ a))

   423   = (cc, (ist |> path_down [L, R]), e);

   424 \<close> ML \<open>

   425   (*case*) scan_dn cc (ist |> path_down_form ([L, L, R], a)) e1 (*of*);

   426 \<close> ML \<open>

   427 "~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)

   428   = (cc, (ist |> path_down_form ([L, L, R], a)), e1);

   429 \<close> ML \<open>

   430         (*if*) Tactical.contained_in t (*else*);

   431 \<close> ML \<open>

   432       (*case*)

   433     LItool.check_leaf "next  " ctxt eval (get_subst ist) t (*of*);

   434 \<close> ML \<open>

   435 "~~~~~ fun check_leaf , args:"; val (call, ctxt, srls, (E, (a, v)), t)

   436   = ("next  ", ctxt, eval, (get_subst ist), t);

   437 \<close> ML \<open>

   438 val (Program.Tac stac, a') =

   439     (*case*) Prog_Tac.eval_leaf E a v t (*of*);

   440 \<close> ML \<open>

   441 	        val stac' = Rewrite.eval_prog_expr ctxt srls

   442               (subst_atomic (Env.update_opt E (a, v)) stac)

   443 \<close> ML \<open>

   444 (*+*)val "Substitute [c_2 = 0] (L * c + c_2 = q_0 * L \<up> 2 / 2)" = stac' |> UnparseC.term;

   445 \<close> ML \<open>

   446 val return =

   447         (Program.Tac stac', a')

   448 \<close> ML \<open>

   449 "~~~~~ from fun check_leaf \<longrightarrow>fun scan_dn , return:"; val ((Program.Tac prog_tac, form_arg))

   450    = (return);

   451 \<close> ML \<open>

   452            check_tac cc ist (prog_tac, form_arg);

   453 \<close> ML \<open>

   454 "~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))

   455   = (cc, ist, (prog_tac, form_arg));

   456 \<close> ML \<open>

   457     val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac

   458 \<close> ML \<open>

   459 val _ =

   460     (*case*) m (*of*);

   461 \<close> ML \<open>

   462       (*case*)

   463 Solve_Step.check m (pt, p) (*of*);

   464 \<close> ML \<open>

   465 "~~~~~ fun check , args:"; val ((Tactic.Substitute sube), (cs as (pt, pos as (p, _))))

   466   = (m, (pt, p));

   467 \<close> ML \<open>

   468         val pp = Ctree.par_pblobj pt p

   469         val ctxt = Ctree.get_loc pt pos |> snd

   470         val thy = Proof_Context.theory_of ctxt

   471         val f = Calc.current_formula cs;

   472 		    val {rew_ord', erls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp)

   473 		    val subte = Subst.input_to_terms ctxt sube (*?TODO: input requires parse _: _ -> _ option?*)

   474 		    val ro = get_rew_ord ctxt rew_ord'

   475 \<close> ML \<open>

   476 		    (*if*) foldl and_ (true, map TermC.contains_Var subte) (*else*);

   477 \<close> ML \<open>

   478 (*+isa==isa2*)sube : TermC.as_string list

   479 \<close> ML \<open>

   480 (*+isa==isa2*)val "L * c + c_2 = q_0 * L \<up> 2 / 2" = f |> UnparseC.term

   481 \<close> ML \<open>

   482 (*+isa<>isa2*)val (** )["c_2 = (0::'a)"]( **)["c_2 = 0"](**) = subte |> map UnparseC.term

   483 \<close> ML \<open>

   484 val SOME ttt =

   485 		      (*case*) Rewrite.rewrite_terms_ ctxt ro erls subte f (*of*);

   486 \<close> ML \<open>

   487 \<close> ML \<open> (*//----------- build new fun Subst.input_to_terms ----------------------------------\\*)

   488 (*//------------------ build new fun XXXXX -------------------------------------------------\\*)

   489 \<close> ML \<open>

   490 fun input_to_terms ctxt strs = map (TermC.parse ctxt) strs;

   491 \<close> ML \<open>

   492 input_to_terms: Proof.context -> Subst.input -> Subst.as_eqs

   493 \<close> ML \<open>

   494 (* TermC.parse ctxt fails with "c_2 = 0" \<longrightarrow> \<open>c_2 = (0 :: 'a)\<close> and thus requires adapt_to_type*)

   495 fun input_to_terms ctxt strs = strs

   496   |> map (TermC.parse ctxt)

   497   |> map (Model_Pattern.adapt_term_to_type ctxt)

   498 \<close> ML \<open>

   499 \<close> ML \<open>

   500 \<close> ML \<open>

   501 \<close> ML \<open>

   502 (*\\------------------ build new fun XXXXX -------------------------------------------------//*)

   503 \<close> ML \<open> (*\\----------- build new fun Subst.input_to_terms ----------------------------------//*)

   504 \<close> ML \<open>

   505 \<close> ML \<open>

   506 \<close> ML \<open>

   507 \<close> ML \<open>

   508 \<close> ML \<open>

   509 \<close> ML \<open>

   510 \<close> ML \<open>

   511 \<close> ML \<open>

   512 \<close> text \<open>

   513 "~~~~~ from fun scan_dn \<longrightarrow>fun scan_up , return:"; val (Accept_Tac ict) = (goback);

   514 \<close> text \<open>

   515 "~~~~~ from fun scan_up \<longrightarrow>fun go_scan_up" ^

   516        " \<longrightarrow>fun scan_to_tactic \<longrightarrow>fun find_next_step , return:"; val (Accept_Tac (tac, ist, ctxt))

   517   =  (Accept_Tac ict);

   518 \<close> ML \<open>

   519 \<close> ML \<open>

   520 \<close> ML \<open>

   521 \<close> ML \<open>

   522 \<close> ML \<open>

   523 \<close> ML \<open>

   524 \<close> ML \<open>

   525 \<close> ML \<open>

   526 (*-------------------- stop step into me Take ------------------------------------------------*)

   527 \<close> ML \<open> (*------------- stop step into me Take ------------------------------------------------*)

   528 (*\\------------------ step into me Take ---------------------------------------------------//*)

   529 \<close> ML \<open> (*\\----------- step into me Take ---------------------------------------------------//*)

   530 \<close> ML \<open>

   531 val (p,_,f,nxt,_,pt) = me nxt'''' p'''' c pt'''';f2str f;

   532 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

   533 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

   534 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

   535 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

   536 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

   537 \<close> ML \<open>

   538 (*+*)val (**)"L * c + c_2 = q_0 * L \<up> 2 / 2"(** )

   539              "[c = L * q_0 / 2, c_2 = 0]"( **) = f2str f;

   540 \<close> ML \<open>

   541   val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nL * c + c_2 = q_0 * L \<up> 2 / 2, ORundef, true, true)" =

   542 (*val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\", \"\n(e_2, c = L * q_0 / 2)\", \"\n(e__s, [c_2 = 0, c = L * q_0 / 2])\"], [R, R, D, R, D, R, D, R, D, R, D, L, R], srls_top_down_2x2, SOME e__s, \n[c = L * q_0 / 2, c_2 = 0], ORundef, true, true)" =*)

   543 (*+*)(Ctree.get_istate_LI pt p |> Istate.string_of)

   544 \<close> text \<open>

   545 case nxt of

   546     (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()

   547   | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";

   548 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

   549 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;

   551 (* final test ... ----------------------------------------------------------------------------*)

   552 if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()

   553 else error "eqsystem.sml me [EqSys...2x2] finished f2str f";

   555 case nxt of

   556     (End_Proof') => ()

   557   | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";

   558 \<close> ML \<open>

   559 Test_Tool.show_pt pt (*[

   560 (([], Frm), solveSystem

   561  [[0 = - 1 * q_0 * 0 \<up> 2 div 2 + 0 * c + c_2],

   562   [0 = - 1 * q_0 * L \<up> 2 div 2 + L * c + c_2]]

   563  [[c], [c_2]]),

   564 (([1], Frm), [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,

   565  0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]),

   566 (([1], Res), [0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]),

   567 (([2], Res), [0 = c_2, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]),

   568 (([3], Res), [c_2 = 0, L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2)]),

   569 (([4], Res), [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]),

   570 (([5], Pbl), solveSystem [L * c + c_2 = q_0 * L \<up> 2 / 2] [c_2]),

   571 (([5, 1], Frm), L * c + c_2 = q_0 * L \<up> 2 / 2),

   573 (([5, 1], Res), L * c + 0 = q_0 * L \<up> 2 / 2),

   574 (([5, 2], Res), L * c = q_0 * L \<up> 2 / 2),

   575 (([5, 3], Res), c = q_0 * L \<up> 2 / 2 / L),

   576 (([5, 4], Res), c = L * q_0 / 2),

   577 (([5, 5], Frm), [c_2 = 0, c = L * q_0 / 2]),

   578 (([5, 5], Res), [c = L * q_0 / 2, c_2 = 0]),

   579 (([5], Res), [c = L * q_0 / 2, c_2 = 0]),

   580 (([], Res), [c = L * q_0 / 2, c_2 = 0])]

   581 *)

   582 \<close> ML \<open>

   583 \<close>

   585 section \<open>===================================================================================\<close>

   586 ML \<open>

   587 \<close> ML \<open>

   588 \<close> ML \<open>

   589 \<close> ML \<open>

   590 \<close>

   592 section \<open>code for copy & paste ===============================================================\<close>

   593 ML \<open>

   594 "~~~~~ fun xxx , args:"; val () = ();

   595 "~~~~~ and xxx , args:"; val () = ();

   596 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();

   597 (*if*) (*then*); (*else*);   (*case*) (*of*);  (*return value*); (*in*) (*end*);

   598 "xx"

   599 ^ "xxx"   (*+*) (*+++*) (* keep for continuation*) (*+isa<>isa2*) (**)

   600 \<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)

   601  (*//----------------- adhoc inserted n ----------------------------------------------------\\*)

   602 (*\\------------------ adhoc inserted n ----------------------------------------------------//*)

   603 \<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)

   605 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)

   606 (*//------------------ step into XXXXX -----------------------------------------------------\\*)

   607 (*-------------------- stop step into XXXXX --------------------------------------------------*)

   608 \<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*)

   609 (*\\------------------ step into XXXXX -----------------------------------------------------//*)

   610 \<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)

   612 \<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*)

   613 (*//------------------ build new fun XXXXX -------------------------------------------------\\*)

   614 (*\\------------------ build new fun XXXXX -------------------------------------------------//*)

   615 \<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*)

   616 \<close>

   617 end

author	wneuper <Walther.Neuper@jku.at>
	Wed, 19 Oct 2022 10:43:04 +0200
changeset 60567	bb3140a02f3d
parent 60558	2350ba2640fd
child 60569	f5454fd2e013
permissions	-rw-r--r--