wneuper/isa: test/Tools/isac/Interpret/ptyps.sml@460c24a6a6ba

     1 (* tests for ME/ptyps.sml

     2    CAUTION: intermediately stores !ptyps THUS EVALUATE IN 1 GO

     3    author: Walther Neuper

     4    010916,

     5    (c) due to copyright terms

     7 use"../smltest/ME/ptyps.sml";

     8 use"ptyps.sml";

     9 *)

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

    12 "table of contents -----------------------------------------------";

    13 "-----------------------------------------------------------------";

    14 "###### val intermediate_ptyps = !ptyps; #########################";

    15 "----------- store test-pbtyps -----------------------------------";

    16 "----------- refin test-pbtyps -----------------------------------";

    17 "----------- refine_ori test-pbtyps ------------------------------";

    18 "----------- refine test-pbtyps ----------------------------------";

    19 "###### ptyps:= intermediate_ptyps;###############################";

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

    21 "----------- fun coll_guhs ---------------------------------------";

    22 "----------- fun guh2kestoreID -----------------------------------";

    23 "-----------------------------------------------------------------";

    24 "-----------------------------------------------------------------";

    25 "-----------------------------------------------------------------";

    29 "###### val intermediate_ptyps = !ptyps; #########################";

    30 "###### val intermediate_ptyps = !ptyps; #########################";

    31 "###### val intermediate_ptyps = !ptyps; #########################";

    32 val intermediate_ptyps = !ptyps;

    34 "----------- store test-pbtyps -----------------------------------";

    35 "----------- store test-pbtyps -----------------------------------";

    36 "----------- store test-pbtyps -----------------------------------";

    37 ptyps:= ([]:ptyps);

    39 store_pbt

    40  (prep_pbt DiffApp.thy "pbl_pbla" [] e_pblID

    41  (["pbla"],

    42   [("#Given", ["fixedValues a_"])], e_rls, NONE, []));

    43 store_pbt

    44  (prep_pbt DiffApp.thy "pbl_pbla1" [] e_pblID

    45  (["pbla1","pbla"],

    46   [("#Given", ["fixedValues a_","maximum a1_"])], e_rls, NONE, []));

    47 store_pbt

    48  (prep_pbt DiffApp.thy "pbl_pbla2" [] e_pblID

    49  (["pbla2","pbla"],

    50   [("#Given", ["fixedValues a_","valuesFor a2_"])], e_rls, NONE, []));

    51 store_pbt

    52  (prep_pbt DiffApp.thy "pbl_pbla2x" [] e_pblID

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

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

    55   e_rls, NONE, []));

    56 store_pbt

    57  (prep_pbt DiffApp.thy "pbl_pbla2y" [] e_pblID

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

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

    60   e_rls, NONE, []));

    61 store_pbt

    62  (prep_pbt DiffApp.thy "pbl_pbla2z" [] e_pblID

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

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

    65   e_rls, NONE, []));

    66 store_pbt

    67  (prep_pbt DiffApp.thy "pbl_pbla3" [] e_pblID

    68  (["pbla3","pbla"],

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

    70   e_rls, NONE, []));

    72 show_ptyps();

    74 (*case 1: no refinement *)

    75 val thy = Isac.thy;

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

    77 				"fixedValues [aaa=0]");

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

    79 				"errorBound (ddd=0)");

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

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

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

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

    86 				"relations [aaa333]");

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

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

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

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

    93 				"valuesFor [aaa222]");

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

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

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

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

   100 				"boundVariable aaa222yyy");

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

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

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

   105 "----------- refin test-pbtyps -----------------------------------";

   106 "----------- refin test-pbtyps -----------------------------------";

   107 "----------- refin test-pbtyps -----------------------------------";

   108 (*case 1: no refinement *)

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

   110 (*val it = SOME ["pbla"] : pblID option*)

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

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

   114 (*val it = SOME ["pbla","pbla3"] : pblID option*)

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

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

   118 (*val it = SOME ["pbla","pbla2"] : pblID option*)

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

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

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

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

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

   126 refin ["pbla"] ori4 ppp;

   127 (*val it = SOME ["pbla2","pbla2y"] : pblRD option*)

   130 "----------- refine_ori test-pbtyps ------------------------------";

   131 "----------- refine_ori test-pbtyps ------------------------------";

   132 "----------- refine_ori test-pbtyps ------------------------------";

   133 (*case 1: no refinement *)

   134 refine_ori ori1 ["pbla"];

   135 (*val it = NONE : pblID option !!!!*)

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

   138 refine_ori ori2 ["pbla"];

   139 (*val it = SOME ["pbla3","pbla"] : pblID option*)

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

   142 refine_ori ori3 ["pbla"];

   143 (*val it = SOME ["pbla2","pbla"] : pblID option*)

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

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

   147 if opt = SOME ["pbla2y","pbla2","pbla"] then ()

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

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

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

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

   155 "----------- refine test-pbtyps ----------------------------------";

   156 "----------- refine test-pbtyps ----------------------------------";

   157 "----------- refine test-pbtyps ----------------------------------";

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

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

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

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

   162 	    "boundVariable aaa222yyy"];

   164 (*case 1: no refinement *)

   165 refine fmz1 ["pbla"];

   166 (*

   167 *** pass ["pbla"]

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

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

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

   171 val it =

   172   [Matches

   173      (["pbla"],

   174       {Find=[],

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

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

   177    NoMatch

   178      (["pbla1","pbla"],

   179       {Find=[],

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

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

   182    NoMatch

   183      (["pbla2","pbla"],

   184       {Find=[],

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

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

   187    NoMatch

   188      (["pbla3","pbla"],

   189       {Find=[],

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

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

   192   : match list*)

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

   195 refine fmz2 ["pbla"];

   196 (*

   197 *** pass ["pbla"]

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

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

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

   201 val it =

   202   [Matches

   203      (["pbla"],

   204       {Find=[],

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

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

   207    NoMatch

   208      (["pbla1","pbla"],

   209       {Find=[],

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

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

   212    NoMatch

   213      (["pbla2","pbla"],

   214       {Find=[],

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

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

   217    Matches

   218      (["pbla3","pbla"],

   219       {Find=[],

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

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

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

   224 refine fmz3 ["pbla"];

   225 (*

   226 *** pass ["pbla"]

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

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

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

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

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

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

   233 val it =

   234   [Matches

   235      (["pbla"],

   236       {Find=[],

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

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

   239    NoMatch

   240      (["pbla1","pbla"],

   241       {Find=[],

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

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

   244    Matches

   245      (["pbla2","pbla"],

   246       {Find=[],

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

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

   249    NoMatch

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

   251       {Find=[],

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

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

   254    NoMatch

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

   256       {Find=[],

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

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

   259    NoMatch

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

   261       {Find=[],

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

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

   264    NoMatch

   265      (["pbla3","pbla"],

   266       {Find=[],

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

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

   269   : match list*)

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

   272 refine fmz4 ["pbla"];

   273 (*

   274 *** pass ["pbla"]

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

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

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

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

   279 val it =

   280   [Matches

   281      (["pbla"],

   282       {Find=[],

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

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

   285    NoMatch

   286      (["pbla1","pbla"],

   287       {Find=[],

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

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

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

   291    Matches

   292      (["pbla2","pbla"],

   293       {Find=[],

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

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

   296    NoMatch

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

   298       {Find=[],

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

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

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

   302    Matches

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

   304       {Find=[],

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

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

   307   : match list*)

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

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

   311 (*

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

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

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

   315 val it =

   316   [Matches

   317      (["pbla2","pbla"],

   318       {Find=[],

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

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

   321    NoMatch

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

   323       {Find=[],

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

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

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

   327    Matches

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

   329       {Find=[],

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

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

   332   : match list*)

   334 "###### ptyps:= intermediate_ptyps;###############################";

   335 "###### ptyps:= intermediate_ptyps;###############################";

   336 "###### ptyps:= intermediate_ptyps;###############################";

   337 ptyps:= intermediate_ptyps;

   338 show_ptyps();

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

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

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

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

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

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

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

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

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

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

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

   351 (*nxt = ("Add_Find", Add_Find "solutions L")*)

   353 val nxt = ("Specify_Problem",(*vvvv---specify a not-matching problem*)

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

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

   356 (*ML> f;

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

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

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

   360           Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",

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

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

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

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

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

   366           With=[]}))) : mout

   367 val nxt = ("Add_Find",Add_Find "solutions L") ????!!!!????*)

   369 val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn e;

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

   371 (*val nxt = ("Empty_Tac",Empty_Tac)

   372 ... Refine_Problem ["linear"..] fails internally 040312: works!?!*)

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

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

   376 (*("Specify_Problem", Specify_Problem ["normalize", "univariate", ...])*)

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

   378 (*nxt = ("Specify_Theory", Specify_Theory "Test.thy")*)

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

   380 (*nxt = ("Specify_Method", Specify_Method ["Test", "squ-equ-test-subpbl1"]*)

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

   382 (*nxt = ("Apply_Method", *)

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

   384 (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)

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

   386 (*nxt = ("Rewrite_Set", Rewrite_Set "Test_simplify")*)

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

   388 (*Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]*)

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

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

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

   393 (*nxt = ("Add_Given", Add_Given "equality (-6 + 3 * x = 0)"*)

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

   395 (**)

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

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

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

   399 (*nxt = Specify_Problem ["linear","univariate","equation","test"])*)

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

   401 (*xt = ("Specify_Method", Specify_Method ["Test", "solve_linear"])*)

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

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

   404 (*("Specify_Problem", Specify_Problem ["linear", "univariate", ...])*)

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

   406 (*val nxt = ("Specify_Method",Specify_Method ("Test","solve_linear"))*)

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

   408 (*val nxt = ("Apply_Method",Apply_Method ("Test","solve_linear"))*)

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

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

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

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

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

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

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

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

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

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

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

   420 val Form' (FormKF (~1,EdUndef,_,Nundef,res)) = f;

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

   422 else error "new behaviour in test:refine.sml:miniscript with mini-subpb";

   425 "----------- fun coll_guhs ---------------------------------------";

   426 "----------- fun coll_guhs ---------------------------------------";

   427 "----------- fun coll_guhs ---------------------------------------";

   428 val n = e_pbt;

   429 (#guh : pbt -> guh) e_pbt;

   431 fun XXXnode coll (Ptyp (_,[n],ns)) =

   432     [(#guh : pbt -> guh) n]

   433 and XXXnodes coll [] = coll

   434   | XXXnodes coll (n::ns : pbt ptyp list) = (XXXnode coll n) @

   435 					    (XXXnodes coll ns);

   436 (*^^^ this works, but not this ...

   437 fun node coll (Ptyp (_,[n],ns)) =

   438     [(#guh : 'a -> guh) n]

   439 and nodes coll [] = coll

   440   | nodes coll (n::ns : 'a ptyp list) = (node coll n) @ (nodes coll ns);

   442 Error:

   443 Can't unify {guh: 'a, ...} with 'b (Cannot unify with explicit type variable)

   444    Found near #guh : 'a -> guh

   446 i.e. there is no common fun for pbls and mets ?!?*)

   448 coll_pblguhs (!ptyps);

   449 sort string_ord (coll_pblguhs (!ptyps));

   450 show_pblguhs ();

   451 sort_pblguhs ();

   453 "----------- fun guh2kestoreID -----------------------------------";

   454 "----------- fun guh2kestoreID -----------------------------------";

   455 "----------- fun guh2kestoreID -----------------------------------";

   456 "----- we assumed the problem-hierarchy containing 3 elements on toplevel";

   457 val (Ptyp (id1,[n1 as {guh=guh1,...} : pbt], ns1)::

   458      Ptyp (id2,[n2 as {guh=guh2,...} : pbt], ns2):: _) = (!ptyps);

   459 (*

   460 nodes [] guh1 (!ptyps);

   461 nodes [] guh2 (!ptyps);

   462 *)

   463 val (Ptyp (id1,[n1 as {guh=guh1,...} : pbt], ns1)

   464      ::

   465      Ptyp (id2,[n2 as {guh=guh2,...} : pbt],

   466 	   (Ptyp (id21,[n21 as {guh=guh21,...} : pbt], ns21)) :: _ )

   467      ::

   468      Ptyp (id3,[n3 as {guh=guh3,...} : pbt], ns3)

   469      ::

   470      _ ) = (!ptyps);

   471 (*

   472 nodes [] guh3 (!ptyps);

   473 nodes [] guh21 (!ptyps);

   474 *)

author	Walther Neuper <neuper@ist.tugraz.at>
	Tue, 28 Sep 2010 09:06:56 +0200
branch	isac-update-Isa09-2
changeset 38031	460c24a6a6ba
parent 37960	ec20007095f2
child 38036	02a9b2540eb7
permissions	-rw-r--r--