Mercurial Mercurial > wneuper > isac / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/smltest/ME/script.sml
author wneuper
Fri, 04 Jan 2008 11:16:28 +0100
branchstart-work-070517
changeset 274 365f988a7516
parent 273 7cb662bd345d
permissions -rw-r--r--
for PolyMinus at Sch"arding, make p.33 confluent 
     1 (* tests for ME/script.sml

     2    TODO.WN0509 collect typical tests from systest here !!!!!

     3    author: Walther Neuper 050908

     4    (c) copyright due to lincense terms.

     5 

     6 use"../smltest/ME/script.sml";

     7 use"script.sml";

     8 *)

     9 "-----------------------------------------------------------------";

    10 "table of contents -----------------------------------------------";

    11 "-----------------------------------------------------------------";

    12 "----------- WN0509 why does next_tac doesnt find Substitute -----";

    13 "----------- WN0509 Substitute 2nd part --------------------------";

    14 "----------- fun sel_appl_atomic_tacs ----------------------------";

    15 "-----------------------------------------------------------------";

    16 "-----------------------------------------------------------------";

    17 "-----------------------------------------------------------------";

    18 

    19 

    20 "----------- WN0509 why does next_tac doesnt find Substitute -----";

    21 "----------- WN0509 why does next_tac doesnt find Substitute -----";

    22 "----------- WN0509 why does next_tac doesnt find Substitute -----";

    23 

    24 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)

    25 val str = (*#1#*)

    26 "Script BiegelinieScript                                             \

    27 \(l_::real) (q__::real) (v_::real) (b_::real=>real)                    \

    28 \(rb_::bool list) (rm_::bool list) =                                  \

    29 \  (let q___ = Take (M_b v_ = q__);                                          \

    30 \       (M1__::bool) = ((Substitute [v_ = 0])) q___           \

    31 \ in True)";

    32 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;

    33 

    34 val str = (*#2#*)

    35 "Script BiegelinieScript                                             \

    36 \(l_::real) (q__::real) (v_::real) (b_::real=>real)                    \

    37 \(rb_::bool list) (rm_::bool list) =                                  \

    38 \  (let q___ = Take (q_ v_ = q__);                                          \

    39 \       (M1__::bool) = ((Substitute [v_ = 0]) @@ \

    40 \                       (Substitute [M_b 0 = 0]))  q___          \

    41 \ in True)";(*..doesnt find Substitute with ..@@ !!!!!!!!!!!!!!!!!!!!!*)

    42 

    43 val str = (*#3#*)

    44 "Script BiegelinieScript                                             \

    45 \(l_::real) (q__::real) (v_::real) (b_::real=>real)                    \

    46 \(rb_::bool list) (rm_::bool list) =                                  \

    47 \  (let q___ = Take (q_ v_ = q__);                                          \

    48 \      (M1__::bool) = Substitute [v_ = 0]      q___ ;        \

    49 \       M1__ =        Substitute [M_b 0 = 0]  M1__           \

    50 \ in True)"

    51 ;

    52 val str = (*#4#*)

    53 "Script BiegelinieScript                                             \

    54 \(l_::real) (q__::real) (v_::real) (b_::real=>real)                    \

    55 \(rb_::bool list) (rm_::bool list) =                                  \

    56 \  (let q___ = Take (q_ v_ = q__);                                          \

    57 \      (M1__::bool) = Substitute [v_ = 0]      q___ ;        \

    58 \       M1__ =        Substitute [v_ = 1]      q___ ;        \

    59 \       M1__ =        Substitute [v_ = 2]      q___ ;        \

    60 \       M1__ =        Substitute [v_ = 3]      q___ ;        \

    61 \       M1__ =        Substitute [M_b 0 = 0]  M1__           \

    62 \ in True)"

    63 ;

    64 val str = (*#5#*)

    65 "Script BiegelinieScript                                             \

    66 \(l_::real) (q__::real) (v_::real) (b_::real=>real)                    \

    67 \(rb_::bool list) (rm_::bool list) =                                  \

    68 \  (let q___ = Take (M_b v_ = q__);                                          \

    69 \      (M1__::bool) = Substitute [v_ = 0]      q___ ;        \

    70 \       M2__ = Take q___ ;                                     \

    71 \       M2__ =        Substitute [v_ = 2]      q___           \

    72 \ in True)"

    73 ;

    74 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;

    75 atomty sc';

    76 val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];

    77 (*---------------------------------------------------------------------

    78 if sc = sc' then () else raise error"script.sml, doesnt find Substitute #1";

    79 ---------------------------------------------------------------------*)

    80 

    81 val fmz = ["Traegerlaenge L",

    82 	   "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",

    83 	   "Biegelinie y",

    84 	   "RandbedingungenBiegung [y 0 = 0, y L = 0]",

    85 	   "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",

    86 	   "FunktionsVariable x"];

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

    88   ("Biegelinie.thy",["MomentBestimmte","Biegelinien"],

    89    ["IntegrierenUndKonstanteBestimmen"]);

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

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

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

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

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

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

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

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

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

    99 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()

   100 	  | _ => raise error "script.sml, doesnt find Substitute #2";

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

   102 (* *** generate1: not impl.for Substitute' !!!!!!!!!!(*#1#*)!!!!!!!!!!!*)

   103 (* val nxt = ("Check_Postcond",.. !!!!!!!!!!!!!!!!!!!(*#2#*)!!!!!!!!!!!*)

   104 

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

   106 (* *** generate1: not impl.for Empty_Tac_  !!!!!!!!!!(*#3#*)!!!!!!!!!!!*)

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

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

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

   110 (*---------------------------------------------------------------------*)

   111 case nxt of (_, End_Proof') => () 

   112 	  | _ => raise error "script.sml, doesnt find Substitute #3";

   113 (*---------------------------------------------------------------------*)

   114 (*the reason, that next_tac didnt find the 2nd Substitute, was that

   115   the Take inbetween was missing, and thus the 2nd Substitute was applied

   116   the last formula in ctree, and not to argument from script*)

   117 

   118 

   119 "----------- WN0509 Substitute 2nd part --------------------------";

   120 "----------- WN0509 Substitute 2nd part --------------------------";

   121 "----------- WN0509 Substitute 2nd part --------------------------";

   122 (*replace met 'IntegrierenUndKonstanteBestimmen' with this script...*)

   123 val str = (*Substitute ; Substitute works*)

   124 "Script BiegelinieScript                                             \

   125 \(l_::real) (q__::real) (v_::real) (b_::real=>real)                    \

   126 \(rb_::bool list) (rm_::bool list) =                                  "^

   127 (*begin after the 2nd integrate*)

   128 "  (let M__ = Take (M_b v_ = q__);                                     \

   129 \       e1__ = nth_ 1 rm_ ;                                         \

   130 \       (x1__::real) = argument_in (lhs e1__);                       \

   131 \       (M1__::bool) = Substitute [v_ = x1__] M__;                   \

   132 \        M1__        = Substitute [e1__] M1__                    \

   133 \ in True)"

   134 ;

   135 (*---^^^-OK-----------------------------------------------------------------*)

   136 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;

   137 atomty sc';

   138 (*---vvv-NOT ok-------------------------------------------------------------*)

   139 val str = (*Substitute @@ Substitute does NOT work???*)

   140 "Script BiegelinieScript                                             \

   141 \(l_::real) (q__::real) (v_::real) (b_::real=>real)                    \

   142 \(rb_::bool list) (rm_::bool list) =                                  "^

   143 (*begin after the 2nd integrate*)

   144 "  (let M__ = Take (M_b v_ = q__);                                     \

   145 \       e1__ = nth_ 1 rm_ ;                                         \

   146 \       (x1__::real) = argument_in (lhs e1__);                       \

   147 \       (M1__::bool) = ((Substitute [v_ = x1__]) @@ \

   148 \                       (Substitute [e1__]))        M__           \

   149 \ in True)"

   150 ;

   151 

   152 val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];

   153 (*---------------------------------------------------------------------

   154 if sc = sc' then () else raise error"script.sml, doesnt find Substitute #1";

   155 ---------------------------------------------------------------------*)

   156 val fmz = ["Traegerlaenge L",

   157 	   "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)",

   158 	   "Biegelinie y",

   159 	   "RandbedingungenBiegung [y 0 = 0, y L = 0]",

   160 	   "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",

   161 	   "FunktionsVariable x"];

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

   163   ("Biegelinie.thy",["MomentBestimmte","Biegelinien"],

   164    ["IntegrierenUndKonstanteBestimmen"]);

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

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

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

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

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

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

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

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

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

   174 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()

   175 	  | _ => raise error "script.sml, doesnt find Substitute #2";

   176 trace_rewrite:=true;

   177 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);

   178 trace_rewrite:=false;

   179 (*Exception TYPE raised:

   180 Illegal type for constant "op =" :: "[real, bool] => bool"

   181 Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) =

   182 ListG.nth_ (1 + -1 + -1) []

   183 Exception-

   184    TYPE

   185       ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",

   186          [],

   187          [Const ("Trueprop", "bool => prop") $

   188                (Const ("op =", "[RealDef.real, bool] => bool") $ ... $ ...)])

   189    raised

   190 ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"

   191 ie. the argument had not been simplified before          ^^^^^^^^^^^^^^^

   192 thus corrected eval_argument_in OK*)

   193 

   194 val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];

   195 val e1__ = str2term"nth_ 1 [M_b 0 = 0, M_b L = 0]";

   196 val e1__ = eval_listexpr_ Biegelinie.thy srls e1__; term2str e1__;

   197 if term2str e1__ = "M_b 0 = 0" then () else 

   198 raise error"script.sml diff.beh. eval_listexpr_ nth_ 1 [...";

   199 

   200 (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...

   201 val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";

   202 val x1__ = eval_listexpr_ Biegelinie.thy srls x1__; term2str x1__;

   203 (*no rewrite*)

   204 calculate_ Biegelinie.thy ("Tools.lhs", eval_rhs"eval_lhs_") x1__;

   205 val Some (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)

   206 

   207 val l__ = str2term"lhs (M_b 0 = 0)";

   208 val l__ = eval_listexpr_ Biegelinie.thy srls l__; term2str l__;

   209 val Some (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;

   210 

   211 

   212 trace_rewrite:=true;

   213 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);

   214 trace_rewrite:=false;

   215 

   216 show_mets();

   217 

   218 "----------- fun sel_appl_atomic_tacs ----------------------------";

   219 "----------- fun sel_appl_atomic_tacs ----------------------------";

   220 "----------- fun sel_appl_atomic_tacs ----------------------------";

   221 states:=[];

   222 CalcTree

   223 [(["equality (x+1=2)", "solveFor x","solutions L"], 

   224   ("Test.thy", 

   225    ["sqroot-test","univariate","equation","test"],

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

   227 Iterator 1;

   228 moveActiveRoot 1;

   229 autoCalculate 1 CompleteCalcHead;

   230 autoCalculate 1 (Step 1);

   231 autoCalculate 1 (Step 1);

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

   233 val appltacs = sel_appl_atomic_tacs pt p;

   234 if appltacs = 

   235    [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),

   236     Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),

   237     Calculate "times"] then ()

   238 else raise error "script.sml fun sel_appl_atomic_tacs diff.behav.";

   239 

   240 trace_script := true;

   241 trace_script := false;

   242 applyTactic 1 p (hd appltacs);

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

   244 val appltacs = sel_appl_atomic_tacs pt p;

   245 

   246 "----- WN080102 these vvv do not work, because locatetac starts the search\

   247  \1 stac too low";

   248 applyTactic 1 p (hd appltacs);

   249 autoCalculate 1 CompleteCalc;

   250
wneuper/isac