wneuper/isac: src/sml/systest/refine.sml@90390fecbe74

     1 (* intermediately stores !ptyps

     2    WN.16.9.01

     3    use"tests/refine.sml";

     4    *)

     7 "----------------------- store test-pbtyps ----------------------------";

     8 "----------------------- refin test-pbtyps ----------------------------";

     9 "----------------------- refine_ori test-pbtyps ----------------------------";

    10 "----------------------- refine test-pbtyps ----------------------------";

    11 "----------------------- Refine_Problem (aus subp-rooteq.sml) ---------";

    16 "----------------------- store test-pbtyps ----------------------------";

    17 val intermediate_ptyps = !ptyps;

    18 ptyps:= ([]:ptyps);

    20 store_pbt

    21  (prep_pbt DiffApp.thy

    22  (["pbla"],

    23   [("#Given", ["fixedValues a_"])], e_rls, None, []));

    24 store_pbt

    25  (prep_pbt DiffApp.thy

    26  (["pbla1","pbla"],

    27   [("#Given", ["fixedValues a_","maximum a1_"])], e_rls, None, []));

    28 store_pbt

    29  (prep_pbt DiffApp.thy

    30  (["pbla2","pbla"],

    31   [("#Given", ["fixedValues a_","valuesFor a2_"])], e_rls, None, []));

    32 store_pbt

    33  (prep_pbt DiffApp.thy

    34  (["pbla2x","pbla2","pbla"],

    35   [("#Given", ["fixedValues a_","valuesFor a2_","functionOf a2x_"])],

    36   e_rls, None, []));

    37 store_pbt

    38  (prep_pbt DiffApp.thy

    39  (["pbla2y","pbla2","pbla"],

    40   [("#Given" ,["fixedValues a_","valuesFor a2_","boundVariable a2y_"])],

    41   e_rls, None, []));

    42 store_pbt

    43  (prep_pbt DiffApp.thy

    44  (["pbla2z","pbla2","pbla"],

    45   [("#Given" ,["fixedValues a_","valuesFor a2_","interval a2z_"])],

    46   e_rls, None, []));

    47 store_pbt

    48  (prep_pbt DiffApp.thy

    49  (["pbla3","pbla"],

    50   [("#Given" ,["fixedValues a_","relations a3_"])],

    51   e_rls, None, []));

    53 show_ptyps();

    55 (*case 1: no refinement *)

    56 val thy = Isac.thy;

    57 val (d1,ts1,vs1) = split_dts thy ((term_of o the o (parse thy))

    58 				"fixedValues [aaa=0]");

    59 val (d2,ts2,vs2) = split_dts thy ((term_of o the o (parse thy))

    60 				"errorBound (ddd=0)");

    61 val ori1 = [(1,[1],"#Given",d1,ts1),

    62 	    (2,[1],"#Given",d2,ts2)]:ori list;

    65 (*case 2: refined to pbt without children *)

    66 val (d2,ts2,vs2) = split_dts thy ((term_of o the o (parse thy))

    67 				"relations aaa333");

    68 val ori2 = [(1,[1],"#Given",d1,ts1),

    69 	    (2,[1],"#Given",d2,ts2)]:ori list;

    72 (*case 3: refined to pbt with children *)

    73 val (d2,ts2,vs2) = split_dts thy ((term_of o the o (parse thy))

    74 				"valuesFor aaa222");

    75 val ori3 = [(1,[1],"#Given",d1,ts1),

    76 	    (2,[1],"#Given",d2,ts2)]:ori list;

    79 (*case 4: refined to children (without child)*)

    80 val (d3,ts3,vs3) = split_dts thy ((term_of o the o (parse thy))

    81 				"boundVariable aaa222yyy");

    82 val ori4 = [(1,[1],"#Given",d1,ts1),

    83 	    (2,[1],"#Given",d2,ts2),

    84 	    (3,[1],"#Given",d3,ts3)]:ori list;

    86 "----------------------- refin test-pbtyps ----------------------------";

    88 (*case 1: no refinement *)

    89 refin [] ori1 (hd (!ptyps));

    90 (*val it = Some ["pbla"] : pblID option*)

    92 (*case 2: refined to pbt without children *)

    93 refin [] ori2 (hd (!ptyps));

    94 (*val it = Some ["pbla","pbla3"] : pblID option*)

    96 (*case 3: refined to pbt with children *)

    97 refin [] ori3 (hd (!ptyps));

    98 (*val it = Some ["pbla","pbla2"] : pblID option*)

   100 (*case 4: refined to children (without child)*)

   101 refin [] ori4 (hd (!ptyps));

   102 (*val it = Some ["pbla","pbla2","pbla2y"] : pblID option*)

   104 (*case 5: start refinement somewhere in ptyps*)

   105 val [Ptyp ("pbla",_,[_, ppp as Ptyp ("pbla2",_,_), _])] = !ptyps;

   106 refin ["pbla"] ori4 ppp;

   107 (*val it = Some ["pbla2","pbla2y"] : pblRD option*)

   110 "----------------------- refine_ori test-pbtyps ----------------------------";

   112 (*case 1: no refinement *)

   113 refine_ori ori1 ["pbla"];

   114 (*val it = None : pblID option !!!!*)

   116 (*case 2: refined to pbt without children *)

   117 refine_ori ori2 ["pbla"];

   118 (*val it = Some ["pbla3","pbla"] : pblID option*)

   120 (*case 3: refined to pbt with children *)

   121 refine_ori ori3 ["pbla"];

   122 (*val it = Some ["pbla2","pbla"] : pblID option*)

   124 (*case 4: refined to children (without child)*)

   125 val opt = refine_ori ori4 ["pbla"];

   126 if opt = Some ["pbla2y","pbla2","pbla"] then ()

   127 else raise error "new behaviour in refine.sml case 4";

   129 (*case 5: start refinement somewhere in ptyps*)

   130 refine_ori ori4 ["pbla2","pbla"];

   131 (*val it = Some ["pbla2y","pbla2","pbla"] : pblID option*)

   134 "----------------------- refine test-pbtyps ----------------------------";

   136 val fmz1 = ["fixedValues [aaa=0]","errorBound (ddd=0)"];

   137 val fmz2 = ["fixedValues [aaa=0]","relations aaa333"];

   138 val fmz3 = ["fixedValues [aaa=0]","valuesFor aaa222"];

   139 val fmz4 = ["fixedValues [aaa=0]","valuesFor aaa222",

   140 	    "boundVariable aaa222yyy"];

   142 (*case 1: no refinement *)

   143 refine fmz1 ["pbla"];

   144 (*

   145 *** pass ["pbla"]

   146 *** pass ["pbla","pbla1"]

   147 *** pass ["pbla","pbla2"]

   148 *** pass ["pbla","pbla3"]

   149 val it =

   150   [Matches

   151      (["pbla"],

   152       {Find=[],

   153        Given=[Correct "fixedValues [aaa = #0]",

   154               Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),

   155    NoMatch

   156      (["pbla1","pbla"],

   157       {Find=[],

   158        Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",

   159               Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),

   160    NoMatch

   161      (["pbla2","pbla"],

   162       {Find=[],

   163        Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_",

   164               Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),

   165    NoMatch

   166      (["pbla3","pbla"],

   167       {Find=[],

   168        Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_",

   169               Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]})]

   170   : match list*)

   172 (*case 2: refined to pbt without children *)

   173 refine fmz2 ["pbla"];

   174 (*

   175 *** pass ["pbla"]

   176 *** pass ["pbla","pbla1"]

   177 *** pass ["pbla","pbla2"]

   178 *** pass ["pbla","pbla3"]

   179 val it =

   180   [Matches

   181      (["pbla"],

   182       {Find=[],

   183        Given=[Correct "fixedValues [aaa = #0]",Superfl "relations aaa333"],

   184        Relate=[],Where=[],With=[]}),

   185    NoMatch

   186      (["pbla1","pbla"],

   187       {Find=[],

   188        Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",

   189               Superfl "relations aaa333"],Relate=[],Where=[],With=[]}),

   190    NoMatch

   191      (["pbla2","pbla"],

   192       {Find=[],

   193        Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_",

   194               Superfl "relations aaa333"],Relate=[],Where=[],With=[]}),

   195    Matches

   196      (["pbla3","pbla"],

   197       {Find=[],

   198        Given=[Correct "fixedValues [aaa = #0]",Correct "relations aaa333"],

   199        Relate=[],Where=[],With=[]})] : match list*)

   201 (*case 3: refined to pbt with children *)

   202 refine fmz3 ["pbla"];

   203 (*

   204 *** pass ["pbla"]

   205 *** pass ["pbla","pbla1"]

   206 *** pass ["pbla","pbla2"]

   207 *** pass ["pbla","pbla2","pbla2x"]

   208 *** pass ["pbla","pbla2","pbla2y"]

   209 *** pass ["pbla","pbla2","pbla2z"]

   210 *** pass ["pbla","pbla3"]

   211 val it =

   212   [Matches

   213      (["pbla"],

   214       {Find=[],

   215        Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222"],

   216        Relate=[],Where=[],With=[]}),

   217    NoMatch

   218      (["pbla1","pbla"],

   219       {Find=[],

   220        Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",

   221               Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]}),

   222    Matches

   223      (["pbla2","pbla"],

   224       {Find=[],

   225        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222"],

   226        Relate=[],Where=[],With=[]}),

   227    NoMatch

   228      (["pbla2x","pbla2","pbla"],

   229       {Find=[],

   230        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

   231               Missing "functionOf a2x_"],Relate=[],Where=[],With=[]}),

   232    NoMatch

   233      (["pbla2y","pbla2","pbla"],

   234       {Find=[],

   235        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

   236               Missing "boundVariable a2y_"],Relate=[],Where=[],With=[]}),

   237    NoMatch

   238      (["pbla2z","pbla2","pbla"],

   239       {Find=[],

   240        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

   241               Missing "interval a2z_"],Relate=[],Where=[],With=[]}),

   242    NoMatch

   243      (["pbla3","pbla"],

   244       {Find=[],

   245        Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_",

   246               Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]})]

   247   : match list*)

   249 (*case 4: refined to children (without child)*)

   250 refine fmz4 ["pbla"];

   251 (*

   252 *** pass ["pbla"]

   253 *** pass ["pbla","pbla1"]

   254 *** pass ["pbla","pbla2"]

   255 *** pass ["pbla","pbla2","pbla2x"]

   256 *** pass ["pbla","pbla2","pbla2y"]

   257 val it =

   258   [Matches

   259      (["pbla"],

   260       {Find=[],

   261        Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222",

   262               Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),

   263    NoMatch

   264      (["pbla1","pbla"],

   265       {Find=[],

   266        Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",

   267               Superfl "valuesFor aaa222",Superfl "boundVariable aaa222yyy"],

   268        Relate=[],Where=[],With=[]}),

   269    Matches

   270      (["pbla2","pbla"],

   271       {Find=[],

   272        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

   273               Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),

   274    NoMatch

   275      (["pbla2x","pbla2","pbla"],

   276       {Find=[],

   277        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

   278               Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"],

   279        Relate=[],Where=[],With=[]}),

   280    Matches

   281      (["pbla2y","pbla2","pbla"],

   282       {Find=[],

   283        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

   284               Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]

   285   : match list*)

   287 (*case 5: start refinement somewhere in ptyps*)

   288 refine fmz4 ["pbla2","pbla"];

   289 (*

   290 *** pass ["pbla","pbla2"]

   291 *** pass ["pbla","pbla2","pbla2x"]

   292 *** pass ["pbla","pbla2","pbla2y"]

   293 val it =

   294   [Matches

   295      (["pbla2","pbla"],

   296       {Find=[],

   297        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

   298               Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),

   299    NoMatch

   300      (["pbla2x","pbla2","pbla"],

   301       {Find=[],

   302        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

   303               Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"],

   304        Relate=[],Where=[],With=[]}),

   305    Matches

   306      (["pbla2y","pbla2","pbla"],

   307       {Find=[],

   308        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

   309               Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]

   310   : match list*)

   313 ptyps:= intermediate_ptyps;

   314 show_ptyps();

   318 "----------------------- Refine_Problem (aus subp-rooteq.sml) ---------";

   319 "----------------refine.sml: miniscript with mini-subpbl -------------";

   320 val fmz = ["equality ((x+1)*(x+2)=x^^^2+8)","solveFor x",

   321 	   "errorBound (eps=0)","solutions L"];

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

   323 		     ("Test.thy","squ-equ-test-subpbl1"));

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

   325 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

   326 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;

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

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

   330 val nxt = ("Specify_Problem",

   331 	   Specify_Problem ["linear","univariate","equation","test"]);

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

   333 (*ML> f;

   334 val it = Form' (PpcKF (0,EdUndef,0,Nundef,

   335         (Problem ["linear","univariate","equation","test"],

   336          {Find=[Incompl "solutions []"],

   337           Given=[Incompl "errorBound",

   338                  Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",

   339                  Correct "solveFor x"],Relate=[],

   340           Where=[False "matches (x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)

   341                 |\nmatches (?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)

   342                 |\nmatches (?a + x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)

   343         |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],

   344           With=[]}))) : mout

   346 val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)")*)

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

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

   349 (*val nxt = ("Refine_Problem",Refine_Problem ["linear","univariate","equation","test"]

   350              kann nicht gut gehen            --------- *)

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

   352 (*val nxt = ("Specify_Problem",Specify_Problem []) FIXXXME*)

   354 val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation","test"]);

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

   356 (*("Specify_Problem",Specify_Problem ["normalize","univariate","equation","test"])*)

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

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

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

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

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

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

   363 (*val nxt = ("Subproblem",Subproblem ("Test.thy",[#,#,#])) : string * mstep

   364   in Script "uberdefiniert                         -^-*)

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

   366 (*val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation","test"]*)

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

   368 (*val nxt = ("Add_Given",Add_Given "equality (x + #1 + #-1 * #2 = #0)") *)

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

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

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

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

   373 (*("Specify_Problem",Specify_Problem ["linear","univariate","equation","test"])*)

   375 val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation","test"]);

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

   377 (*val nxt = ("Specify_Method",Specify_Method ("RatArith.thy","solve_linear"))*)

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

   379 (*val nxt = ("Apply_Method",Apply_Method ("RatArith.thy","solve_linear"))*)

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

   381 (*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)

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

   383 (*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*)

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

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

   386 (*val nxt = ("Check_Postcond",Check_Postcond ["linear","univariate","eq*)

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

   388 (*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)

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

   390 (*("Check_Postcond",Check_Postcond ["normalize","univariate","equation","test"])*)

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

   392 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;

   393 if (snd nxt)=End_Proof' andalso res="[x = 2]" then ()

   394 else raise error "new behaviour in test:refine.sml: miniscript with mini-subpbl";

author	agriesma
	Thu, 17 Apr 2003 18:01:03 +0200
branch	griesmayer
changeset 338	90390fecbe74
child 708	7d3338563b8c
permissions	-rw-r--r--