wneuper/isa: test/Tools/isac/Interpret/script.sml@fbaff8cf0179

     1 (* Title:  test/../script.sml

     2    Author: Walther Neuper 050908

     3    (c) copyright due to lincense terms.

     4 *)

     5 "-----------------------------------------------------------------";

     6 "table of contents -----------------------------------------------";

     7 "-----------------------------------------------------------------";

     8 "----------- fun sel_appl_atomic_tacs ----------------------------";

     9 "----------- fun init_form, fun get_stac -------------------------";

    10 "----------- fun sel_rules ---------------------------------------";

    11 "----------- fun sel_appl_atomic_tacs ----------------------------";

    12 "----------- fun de_esc_underscore -------------------------------";

    13 "----------- fun go ----------------------------------------------";

    14 "----------- fun formal_args -------------------------------------";

    15 "----------- fun dsc_valT ----------------------------------------";

    16 "----------- fun itms2args ---------------------------------------";

    17 "----------- fun init_pstate -----------------------------------------------------------------";

    18 "-----------------------------------------------------------------";

    19 "-----------------------------------------------------------------";

    20 "-----------------------------------------------------------------";

    22 val thy =  @{theory Isac_Knowledge};

    24 "----------- fun sel_appl_atomic_tacs ----------------------------";

    25 "----------- fun sel_appl_atomic_tacs ----------------------------";

    26 "----------- fun sel_appl_atomic_tacs ----------------------------";

    28 reset_states ();

    29 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],

    30   ("Test", ["sqroot-test","univariate","equation","test"],

    31    ["Test","squ-equ-test-subpbl1"]))];

    32 Iterator 1;

    33 moveActiveRoot 1;

    34 autoCalculate 1 CompleteCalcHead;

    35 autoCalculate 1 (Steps 1);

    36 autoCalculate 1 (Steps 1);

    37 val ((pt, p), _) = get_calc 1; show_pt pt;

    38 val appltacs = sel_appl_atomic_tacs pt p;

    39 case appltacs of

    40   [Rewrite ("radd_commute", radd_commute),

    41   Rewrite ("add_assoc", add_assoc), Calculate "TIMES"]

    42   => if (term2str o Thm.prop_of) radd_commute = "?m + ?n = ?n + ?m" andalso

    43         (term2str o Thm.prop_of) add_assoc = "?a + ?b + ?c = ?a + (?b + ?c)" then ()

    44         else error "script.sml fun sel_appl_atomic_tacs diff.behav. 2"

    45 | _ => error "script.sml fun sel_appl_atomic_tacs diff.behav. 1";

    47 trace_script := true;

    48 trace_script := false;

    49 applyTactic 1 p (hd appltacs);

    50 val ((pt, p), _) = get_calc 1; show_pt pt;

    51 val appltacs = sel_appl_atomic_tacs pt p;

    52 (*applyTactic 1 p (hd appltacs); WAS scan_dn1: call by ([3], Pbl)*)

    54 "~~~~~ fun applyTactic, args:"; val ((cI:calcID), ip, tac) = (1, p, (hd appltacs));

    55 val ((pt, _), _) = get_calc cI;

    56 val p = get_pos cI 1;

    57 locatetac;

    58 locatetac tac;

    60 (*locatetac tac (pt, ip); (*WAS scan_dn1: call by ([3], Pbl)*)*)

    61 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));

    62   val Appl m = applicable_in p pt tac ; (*Appl*)

    63   (*if*) Tactic.for_specify' m; (*false*)

    64 (*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)

    65 loc_solve_; (*without _ ??? result is -> lOc writing error ???*)

    66 (*val it = fn: string * tac_ -> ctree * (pos * pos_) -> lOc_*)

    67 (mI,m); (*string * tac*)

    68 ptp (*ctree * pos'*);

    69 "~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = (m, ptp);

    70 (*val (msg, cs') = Step_Solve.by_tactic m (pt, pos);

    71 (*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)

    72 m;

    73 (pt, pos);

    74 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));

    75 (*solve has still p_!!!!!!!!!!!!!!!!!!!!!!!!!*)

    77 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)

    78 val ctxt = get_ctxt pt po;

    80 (*generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) m (e_istate, ctxt) (p,p_) pt;

    81 (*Argument: m : tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)

    82 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)));

    83 assoc_thy;

    85 (* ERROR  which has NOT be created by this change set

    86 (1) actual         : ERROR exception PTREE "get_obj f EmptyPtree" raised (line 289 of "~~/src/Tools/isac/MathEngBasic/ctree-basic.sml")

    87 (2) in 927379190abd: generate1: not impl.for Empty_Tac

    89 in case (2) exn.ERROR _ was caught, while in case (1) exn.Ptree is not caught before toplevel

    91 autoCalculate 1 CompleteCalc; (* ONE ERROR *)

    92 ==============================^^^^^^^^^^^^^*)

    94 "----------- fun init_form, fun get_stac -------------------------";

    95 "----------- fun init_form, fun get_stac -------------------------";

    96 "----------- fun init_form, fun get_stac -------------------------";

    97 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];

    98 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],

    99   ["Test","squ-equ-test-subpbl1"]);

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

   101 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   102 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   103 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   104 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   105 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   106 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   107 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   108 "~~~~~ fun me, args:"; val tac = nxt;

   109 "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);

   110 val Appl m = applicable_in p pt tac;

   111  (*if*) Tactic.for_specify' m; (*false*)

   112 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = (m, ptp);

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

   114   = (m, pos);

   115 val {srls, ...} = get_met mI;

   116 val PblObj {meth=itms, ...} = get_obj I pt p;

   117 val thy' = get_obj g_domID pt p;

   118 val thy = assoc_thy thy';

   119 val srls = Lucin.get_simplifier (pt, pos)

   120 val (is as Pstate {env, ...}, ctxt, sc) = init_pstate srls ctxt itms mI;

   121 val ini = init_form thy sc env;

   122 "----- fun init_form, args:"; val (Prog sc) = sc;

   123 "----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);

   124 case get_stac thy sc of SOME (Free ("e_e", _)) => ()

   125 | _ => error "script: Const (?, ?) in script (as term) changed";;

   127 "----------- fun sel_rules ---------------------------------------";

   128 "----------- fun sel_rules ---------------------------------------";

   129 "----------- fun sel_rules ---------------------------------------";

   130 (* compare test/../interface.sml

   131 "--------- getTactic, fetchApplicableTactics ------------";

   132 *)

   133  reset_states ();

   134  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],

   135    ("Test", ["sqroot-test","univariate","equation","test"],

   136     ["Test","squ-equ-test-subpbl1"]))];

   137  Iterator 1;

   138  moveActiveRoot 1;

   139  autoCalculate 1 CompleteCalc;

   140  val ((pt,_),_) = get_calc 1;

   141  show_pt pt;

   143 (*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)

   144  val tacs = sel_rules pt ([],Pbl);

   145  case tacs of [Apply_Method ["Test", "squ-equ-test-subpbl1"]] => ()

   146  | _ => error "script.sml: diff.behav. in sel_rules ([],Pbl)";

   148  val tacs = sel_rules pt ([1],Res);

   149  case tacs of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",

   150       Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),

   151       Check_elementwise "Assumptions"] => ()

   152  | _ => error "script.sml: diff.behav. in sel_rules ([1],Res)";

   154  val tacs = sel_rules pt ([3],Pbl);

   155  case tacs of [Apply_Method ["Test", "solve_linear"]] => ()

   156  | _ => error "script.sml: diff.behav. in sel_rules ([3],Pbl)";

   158  val tacs = sel_rules pt ([3,1],Res);

   159  case tacs of [Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"), Rewrite_Set "Test_simplify"] => ()

   160  | _ => error "script.sml: diff.behav. in sel_rules ([3,1],Res)";

   162  val tacs = sel_rules pt ([3],Res);

   163  case tacs of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",

   164       Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),

   165       Check_elementwise "Assumptions"] => ()

   166  | _ => error "script.sml: diff.behav. in sel_rules ([3],Res)";

   168  val tacs = (sel_rules pt ([],Res)) handle PTREE str => [Tac str];

   169  case tacs of [Tac "no tactics applicable at the end of a calculation"] => ()

   170  | _ => error "script.sml: diff.behav. in sel_rules ([],Res)";

   172 "----------- fun sel_appl_atomic_tacs ----------------------------";

   173 "----------- fun sel_appl_atomic_tacs ----------------------------";

   174 "----------- fun sel_appl_atomic_tacs ----------------------------";

   175  reset_states ();

   176  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],

   177    ("Test", ["sqroot-test","univariate","equation","test"],

   178     ["Test","squ-equ-test-subpbl1"]))];

   179  Iterator 1;

   180  moveActiveRoot 1;

   181  autoCalculate 1 CompleteCalc;

   183 (*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)

   184  fetchApplicableTactics 1 99999 ([],Pbl);

   186  fetchApplicableTactics 1 99999 ([1],Res);

   187 "~~~~~ fun fetchApplicableTactics, args:"; val (cI, (scope:int), (p:pos')) = (1, 99999, ([1],Res));

   188 val ((pt, _), _) = get_calc cI;

   189 (*version 1:*)

   190 case sel_rules pt p of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",

   191   Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),

   192   Check_elementwise "Assumptions"] => ()

   193 | _ => error "fetchApplicableTactics ([1],Res) changed";

   194 (*version 2:*)

   195 (*WAS:

   196 sel_appl_atomic_tacs pt p;

   197 ...

   198 ### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])'

   199 ### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"'

   200 *)

   202 "~~~~~ fun sel_appl_atomic_tacs , args:"; val (pt, (p, p_)) = (pt, p);

   203 is_spec_pos p_ = false;

   204         val pp = par_pblobj pt p

   205         val thy' = (get_obj g_domID pt pp):theory'

   206         val thy = assoc_thy thy'

   207         val metID = get_obj g_metID pt pp

   208         val metID' =

   209           if metID = e_metID

   210           then (thd3 o snd3) (get_obj g_origin pt pp)

   211           else metID

   212         val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = get_met metID'

   213         val Pstate ist = get_istate pt (p,p_)

   214         val ctxt = get_ctxt pt (p, p_)

   215         val alltacs = (*we expect at least 1 stac in a script*)

   216           map ((stac2tac pt thy) o rep_stacexpr o #1 o

   217            (interpret_leaf "selrul" ctxt srls (get_subst ist) )) (stacpbls sc)

   218         val f =

   219           (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p

   220           | _ => error "");

   221 (*WN120611 stopped and took version 1 again for fetchApplicableTactics !

   222 (distinct o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs

   223 ...

   224 ### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])'

   225 ### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"'

   226 *)

   228 "----------- fun de_esc_underscore -------------------------------";

   229 "----------- fun de_esc_underscore -------------------------------";

   230 "----------- fun de_esc_underscore -------------------------------";

   231 (*

   232 > val str = "Rewrite_Set_Inst";

   233 > val esc = esc_underscore str;

   234 val it = "Rewrite'_Set'_Inst" : string

   235 > val des = de_esc_underscore esc;

   236  val des = de_esc_underscore esc;*)

   238 "----------- fun go ----------------------------------------------";

   239 "----------- fun go ----------------------------------------------";

   240 "----------- fun go ----------------------------------------------";

   241 (*

   242 > val t = (Thm.term_of o the o (parse thy)) "a+b";

   243 val it = Const (#,#) $ Free (#,#) $ Free ("b","RealDef.real") : term

   244 > val plus_a = go [L] t;

   245 > val b = go [R] t;

   246 > val plus = go [L,L] t;

   247 > val a = go [L,R] t;

   249 > val t = (Thm.term_of o the o (parse thy)) "a+b+c";

   250 val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c","RealDef.real") : term

   251 > val pl_pl_a_b = go [L] t;

   252 > val c = go [R] t;

   253 > val a = go [L,R,L,R] t;

   254 > val b = go [L,R,R] t;

   255 *)

   257 "----------- fun formal_args -------------------------------------";

   258 "----------- fun formal_args -------------------------------------";

   259 "----------- fun formal_args -------------------------------------";

   260 (*

   261 > formal_args scr;

   262   [Free ("f_","RealDef.real"),Free ("v_","RealDef.real"),

   263    Free ("eqs_","bool List.list")] : term list

   264 *)

   265 "----------- fun dsc_valT ----------------------------------------";

   266 "----------- fun dsc_valT ----------------------------------------";

   267 "----------- fun dsc_valT ----------------------------------------";

   268 (*> val t = (Thm.term_of o the o (parse thy)) "equality";

   269 > val T = type_of t;

   270 val T = "bool => Tools.una" : typ

   271 > val dsc = dsc_valT t;

   272 val dsc = "una" : string

   274 > val t = (Thm.term_of o the o (parse thy)) "fixedValues";

   275 > val T = type_of t;

   276 val T = "bool List.list => Tools.nam" : typ

   277 > val dsc = dsc_valT t;

   278 val dsc = "nam" : string*)

   279 "----------- fun itms2args ---------------------------------------";

   280 "----------- fun itms2args ---------------------------------------";

   281 "----------- fun itms2args ---------------------------------------";

   282 (*

   283 > val sc = ... Solve_root_equation ...

   284 > val mI = ("Program","sqrt-equ-test");

   285 > val PblObj{meth={ppc=itms,...},...} = get_obj I pt [];

   286 > val ts = itms2args thy mI itms;

   287 > map (term_to_string''' thy) ts;

   288 ["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list

   289 *)

   291 "----------- fun init_pstate -----------------------------------------------------------------";

   292 "----------- fun init_pstate -----------------------------------------------------------------";

   293 "----------- fun init_pstate -----------------------------------------------------------------";

   294 val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",

   295 	     "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",

   296 	     "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",

   297 	     "AbleitungBiegelinie dy"];

   298 val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],

   299 		     ["IntegrierenUndKonstanteBestimmen2"]);

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

   301 (*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*)

   302 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Traegerlaenge L"*)

   303 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Streckenlast q_0"*)

   304 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Biegelinie y"*)

   305 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)

   306 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)

   307 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*)

   308 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["Biegelinien"]*)

   309 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*)

   310 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)

   311 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)

   312 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "AbleitungBiegelinie dy"*)

   313 (*[], Met*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt''''' = Apply_Method ["IntegrierenUndKonstanteBestimmen2"*)

   315 (*+*)val PblObj {meth, spec = (thy, _ , metID), ...} = get_obj I pt''''' (fst p''''');

   316 (*+*)val ctxt = get_ctxt pt''''' p''''';

   317 (*+*)val srls = get_simplifier (pt''''', p''''');

   318 "~~~~~ fun init_pstate , args:"; val (srls, thy, itms, metID) = (srls, assoc_thy thy, meth, metID);

   319 val (Pstate st, ctxt, Prog _) = init_pstate srls ctxt itms metID;

   320 if scrstate2str st =

   321    "([\"\n(l, L)\",\"\n(q, q_0)\",\"\n(v, x)\",\"\n(b, dy)\",\"\n(s, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\",\"\n(vs, [c, c_2, c_3, c_4])\",\"\n(id_abl, y)\"], [], erls_IntegrierenUndK.., NONE, \n??.empty, ORundef, AppUndef_, true)"

   322 then () else error "init_pstate changed for Biegelinie";

   324 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Model_Problem*)

   325 if p = ([1], Pbl)

   326 then case nxt of Model_Problem => () | _ => error "Biegelinie 7.70 changed 1"

   327 else error "modeling root-problem of Biegelinie 7.70 changed";

author	Walther Neuper <walther.neuper@jku.at>
	Fri, 20 Dec 2019 10:24:52 +0100
changeset 59755	fbaff8cf0179
parent 59753	7ad0b6cfd408
child 59767	c4acd312bd53
permissions	-rw-r--r--