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

     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 rep_tac_ ----------------------------------------";

    18 "----------- fun init_pstate -----------------------------------------------------------------";

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

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

    21 "-----------------------------------------------------------------";

    23 val thy =  @{theory Isac_Knowledge};

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

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

    27 "----------- fun sel_appl_atomic_tacs ----------------------------";

    29 reset_states ();

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

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

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

    33 Iterator 1;

    34 moveActiveRoot 1;

    35 autoCalculate 1 CompleteCalcHead;

    36 autoCalculate 1 (Step 1);

    37 autoCalculate 1 (Step 1);

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

    39 val appltacs = sel_appl_atomic_tacs pt p;

    40 case appltacs of

    41   [Rewrite ("radd_commute", radd_commute),

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

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

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

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

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

    48 trace_script := true;

    49 trace_script := false;

    50 applyTactic 1 p (hd appltacs);

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

    52 val appltacs = sel_appl_atomic_tacs pt p;

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

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

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

    57 val p = get_pos cI 1;

    58 locatetac;

    59 locatetac tac;

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

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

    63 val (mI,m) = mk_tac'_ tac;

    64 applicable_in p pt m ; (*Appl*)

    65 member op = specsteps mI; (*false*)

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

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

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

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

    70 ptp (*ctree * pos'*);

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

    72 (*val (msg, cs') = solve m (pt, pos);

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

    74 m;

    75 (pt, pos);

    76 "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));

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

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

    80 val ctxt = get_ctxt pt po;

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

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

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

    85 assoc_thy;

    87 autoCalculate 1 CompleteCalc;

    89 "----------- fun init_form, fun get_stac -------------------------";

    90 "----------- fun init_form, fun get_stac -------------------------";

    91 "----------- fun init_form, fun get_stac -------------------------";

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

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

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

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

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

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

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

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

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

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

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

   103 "~~~~~ fun me, args:"; val (_,tac) = nxt;

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

   105 val (mI,m) = mk_tac'_ tac;

   106 val Appl m = applicable_in p pt m;

   107 member op = specsteps mI; (*false*)

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

   109 "~~~~~ fun solve , args:"; val (("Apply_Method", Apply_Method' (mI,_,_,ctxt)), pos as (p,_)) = (m, pos);

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

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

   112 val thy' = get_obj g_domID pt p;

   113 val thy = assoc_thy thy';

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

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

   116 val ini = init_form thy sc env;

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

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

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

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

   122 "----------- fun sel_rules ---------------------------------------";

   123 "----------- fun sel_rules ---------------------------------------";

   124 "----------- fun sel_rules ---------------------------------------";

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

   126 "--------- getTactic, fetchApplicableTactics ------------";

   127 *)

   128  reset_states ();

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

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

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

   132  Iterator 1;

   133  moveActiveRoot 1;

   134  autoCalculate 1 CompleteCalc;

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

   136  show_pt pt;

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

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

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

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

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

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

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

   146       Check_elementwise "Assumptions"] => ()

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

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

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

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

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

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

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

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

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

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

   160       Check_elementwise "Assumptions"] => ()

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

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

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

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

   167 "----------- fun sel_appl_atomic_tacs ----------------------------";

   168 "----------- fun sel_appl_atomic_tacs ----------------------------";

   169 "----------- fun sel_appl_atomic_tacs ----------------------------";

   170  reset_states ();

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

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

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

   174  Iterator 1;

   175  moveActiveRoot 1;

   176  autoCalculate 1 CompleteCalc;

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

   179  fetchApplicableTactics 1 99999 ([],Pbl);

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

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

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

   184 (*version 1:*)

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

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

   187   Check_elementwise "Assumptions"] => ()

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

   189 (*version 2:*)

   190 (*WAS:

   191 sel_appl_atomic_tacs pt p;

   192 ...

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

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

   195 *)

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

   198 is_spec_pos p_ = false;

   199         val pp = par_pblobj pt p

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

   201         val thy = assoc_thy thy'

   202         val metID = get_obj g_metID pt pp

   203         val metID' =

   204           if metID = e_metID

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

   206           else metID

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

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

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

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

   211            (interpret_leaf "selrul" thy' srls (get_subst ist) )) (stacpbls sc)

   212         val f =

   213           case p_ of

   214               Frm => get_obj g_form pt p

   215             | Res => (fst o (get_obj g_result pt)) p;

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

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

   218 ...

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

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

   221 *)

   223 "----------- fun de_esc_underscore -------------------------------";

   224 "----------- fun de_esc_underscore -------------------------------";

   225 "----------- fun de_esc_underscore -------------------------------";

   226 (*

   227 > val str = "Rewrite_Set_Inst";

   228 > val esc = esc_underscore str;

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

   230 > val des = de_esc_underscore esc;

   231  val des = de_esc_underscore esc;*)

   233 "----------- fun go ----------------------------------------------";

   234 "----------- fun go ----------------------------------------------";

   235 "----------- fun go ----------------------------------------------";

   236 (*

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

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

   239 > val plus_a = go [L] t;

   240 > val b = go [R] t;

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

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

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

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

   246 > val pl_pl_a_b = go [L] t;

   247 > val c = go [R] t;

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

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

   250 *)

   252 "----------- fun formal_args -------------------------------------";

   253 "----------- fun formal_args -------------------------------------";

   254 "----------- fun formal_args -------------------------------------";

   255 (*

   256 > formal_args scr;

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

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

   259 *)

   260 "----------- fun dsc_valT ----------------------------------------";

   261 "----------- fun dsc_valT ----------------------------------------";

   262 "----------- fun dsc_valT ----------------------------------------";

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

   264 > val T = type_of t;

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

   266 > val dsc = dsc_valT t;

   267 val dsc = "una" : string

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

   270 > val T = type_of t;

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

   272 > val dsc = dsc_valT t;

   273 val dsc = "nam" : string*)

   274 "----------- fun itms2args ---------------------------------------";

   275 "----------- fun itms2args ---------------------------------------";

   276 "----------- fun itms2args ---------------------------------------";

   277 (*

   278 > val sc = ... Solve_root_equation ...

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

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

   281 > val ts = itms2args thy mI itms;

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

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

   284 *)

   285 "----------- fun rep_tac_ ----------------------------------------";

   286 "----------- fun rep_tac_ ----------------------------------------";

   287 "----------- fun rep_tac_ ----------------------------------------";

   288 (***************fun rep_tac_ (Rewrite_Inst' (thy', rod, rls, put, subs, (thmID, _), f, (f', _))) =

   289 Fehlersuche 25.4.01

   290 (a)----- als String zusammensetzen:

   291 ML> term2str f;

   292 val it = "d_d x #4 + d_d x (x ^^^ #2 + #3 * x)" : string

   293 ML> term2str f';

   294 val it = "#0 + d_d x (x ^^^ #2 + #3 * x)" : string

   295 ML> subs;

   296 val it = [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real"))] : subst

   297 > val tt = (Thm.term_of o the o (parse thy))

   298   "(Rewrite_Inst[(''bdv'',x)]diff_const (d_d x #4 + d_d x (x ^^^ #2 + #3 * x)))=(#0 + d_d x (x ^^^ #2 + #3 * x))";

   299 > atomty tt;

   300 ML> tracing (term2str tt);

   301 (Rewrite_Inst [(''bdv'',x)] diff_const  d_d x #4 + d_d x (x ^^^ #2 + #3 * x)) =

   302  #0 + d_d x (x ^^^ #2 + #3 * x)

   304 (b)----- laut rep_tac_:

   305 > val ttt=HOLogic.mk_eq (lhs,f');

   306 > atomty ttt;

   309 (*Fehlersuche 1-2Monate vor 4.01:*)

   310 > val tt = (Thm.term_of o the o (parse thy))

   311   "Rewrite_Inst[(''bdv'',x)]square_equation_left True(x=#1+#2)";

   312 > atomty tt;

   314 > val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";

   315 > val f' = (Thm.term_of o the o (parse thy)) "x=#3";

   316 > val subs = [((Thm.term_of o the o (parse thy)) "bdv",

   317 	       (Thm.term_of o the o (parse thy)) "x")];

   318 > val sT = (type_of o fst o hd) subs;

   319 > val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))

   320 			      (map HOLogic.mk_prod subs);

   321 > val sT' = type_of subs';

   322 > val lhs = Const ("Prog_Tac.Rewrite'_Inst",[sT',idT,fT,fT] ---> fT)

   323   $ subs' $ Free (thmID,idT) $ @{term True} $ f;

   324 > lhs = tt;

   325 val it = true : bool

   326 > rep_tac_ (Rewrite_Inst'

   327 	       ("Program","tless_true","eval_rls",false,subs,

   328 		("square_equation_left",""),f,(f',[])));

   329 *)

   330 (****************************| rep_tac_ (Rewrite' (thy', _, _, put, (thmID, _), f, (f', _)))=

   331 > val tt = (Thm.term_of o the o (parse thy)) (*____   ____..test*)

   332   "Rewrite square_equation_left True (x=#1+#2) = (x=#3)";

   334 > val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";

   335 > val f' = (Thm.term_of o the o (parse thy)) "x=#3";

   336 > val Thm (id,thm) =

   337   rep_tac_ (Rewrite'

   338    ("Program","tless_true","eval_rls",false,

   339     ("square_equation_left",""),f,(f',[])));

   340 > val SOME ct = parse thy

   341   "Rewrite square_equation_left True (x=#1+#2)";

   342 > rewrite_ Program.thy tless_true eval_rls true thm ct;

   343 val it = SOME ("x = #3",[]) : (cterm * cterm list) option

   344 *)

   345 (****************************************  | rep_tac_ (Rewrite_Set_Inst'

   346 WN050824: type error ...

   347   let val fT = type_of f;

   348     val sT = (type_of o fst o hd) subs;

   349     val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))

   350       (map HOLogic.mk_prod subs);

   351     val sT' = type_of subs';

   352     val lhs = Const ("Prog_Tac.Rewrite'_Set'_Inst",

   353 		     [sT',idT,fT,fT] ---> fT)

   354       $ subs' $ Free (id_rls rls,idT) $ b $ f;

   355   in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end*)

   356 (* ... vals from Rewrite_Inst' ...

   357 > rep_tac_ (Rewrite_Set_Inst'

   358 	       ("Program",false,subs,

   359 		"isolate_bdv",f,(f',[])));

   360 *)

   361 (* val (Rewrite_Set' (thy',put,rls,f,(f',asm)))=m;

   362 *)

   363 (**************************************   | rep_tac_ (Rewrite_Set' (thy',put,rls,f,(f',asm)))=

   364 13.3.01:

   365 val thy = assoc_thy thy';

   366 val t = HOLogic.mk_eq (lhs,f');

   367 make_rule thy t;

   368 --------------------------------------------------

   369 val lll = (Thm.term_of o the o (parse thy))

   370   "Rewrite_Set SqRoot_simplify (d_d x (x ^^^ #2 + #3 * x) + d_d x #4)";

   372 --------------------------------------------------

   373 > val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";

   374 > val f' = (Thm.term_of o the o (parse thy)) "x=#3";

   375 > val Thm (id,thm) =

   376   rep_tac_ (Rewrite_Set'

   377    ("Program",false,"SqRoot_simplify",f,(f',[])));

   378 val id = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : string

   379 val thm = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : thm

   380 *)

   381 (*****************************************   | rep_tac_ (Calculate' (thy',op_,f,(f',thm')))=

   382 > val lhs'=(Thm.term_of o the o (parse thy))"Calculate plus (#1+#2)";

   383   ... test-root-equ.sml: calculate ...

   384 > val Appl m'=applicable_in p pt (Calculate "PLUS");

   385 > val (lhs,_)=tac_2etac m';

   386 > lhs'=lhs;

   387 val it = true : bool*)

   389 "----------- fun init_pstate -----------------------------------------------------------------";

   390 "----------- fun init_pstate -----------------------------------------------------------------";

   391 "----------- fun init_pstate -----------------------------------------------------------------";

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

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

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

   395 	     "AbleitungBiegelinie dy"];

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

   397 		     ["IntegrierenUndKonstanteBestimmen2"]);

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

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

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

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

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

   403 (*[], 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*)

   404 (*[], 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]"*)

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

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

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

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

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

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

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

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

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

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

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

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

   418 if scrstate2str st =

   419    "([\"\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)"

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

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

   423 if p = ([1], Pbl) andalso (fst nxt) = "Model_Problem" then ()

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

author	Walther Neuper <walther.neuper@jku.at>
	Tue, 26 Nov 2019 17:37:17 +0100
changeset 59721	755a780805f1
parent 59718	bc4b000caa39
child 59722	b73e64a8a329
permissions	-rw-r--r--