(* Title: tests for Interpret/ptyps.sml

    Author: Walther Neuper 010916

    (c) due to copyright terms

 *)

 "-----------------------------------------------------------------";

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

 "-----------------------------------------------------------------";

 "-ptyps.thy: store test-pbtyps by 'setup' ------------------------";

 "----------- testdata for refin, refine_ori ----------------------";

 (*"----------- refin test-pbtyps -------requires 'setup'------------";*)

 "----------- refine_ori test-pbtyps --requires 'setup'------------";

 "----------- refine test-pbtyps ------requires 'setup'------------";

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

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

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

 "----------- fun mark --------------------------------------------";

 "----------- fun coll --------------------------------------------";

 "----------- fun coll_variants -----------------------------------";

 "----------- fun add_id ------------------------------------------";

 "----------- fun filter_vat --------------------------------------";

 "----------- fun match_pbl ---------------------------------------";

 "----------- fun match_oris --------------------------------------";

 "-------- fun get_fun_ids ----------------------------------------------------";

 "-----------------------------------------------------------------";

 "-----------------------------------------------------------------";

 "-----------------------------------------------------------------";

 "----------- testdata for refin, refine_ori ----------------------";

 "----------- testdata for refin, refine_ori ----------------------";

 "----------- testdata for refin, refine_ori ----------------------";

 show_ptyps();

 val thy = @{theory "Isac_Knowledge"};

 val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"};

 (*case 1: no refinement *)

 val (d1,ts1) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "fixedValues [aaa = 0]");

 val (d2,ts2) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "errorBound (ddd = 0)");

 val ori1 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]: ori list;

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

 val (d2,ts2) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "relations [aaa333]");

 val ori2 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:ori list;

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

 val (d2,ts2) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "valuesFor [aaa222]");

 val ori3 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:ori list;

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

 val (d3,ts3) = I_Model.split_dts ((Thm.term_of o the o (parse thy)) "boundVariable aaa222yyy");

 val ori4 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2), (3,[1],"#Given",d3,ts3)]:ori list;

 (*=================================================================

 This test expects pbls at a certain position in the tree.

 Since parallel evaluation (i.e. Theory_Data) this cannot be expected.

 Solutions would be

 * provide an access function for a branch (not only leaves)

 * sort the tree of pbls.

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

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

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

 (* fragile test setup: expects ptyps as fixed *)

 val level_1 = case nth 9 (get_ptyps ()) of

 Store.Node ("test", _, level_1) => level_1 | _ => error "refin broken: root-branch in ptyps changed?"

 val level_2 = case nth 4 level_1 of

 Store.Node ("refine", _, level_2) => level_2 | _ => error "refin broken: lev1-branch in ptyps changed?"

 val pbla_branch = case level_2 of 

 [Store.Node ("pbla", _, _)] => level_2 | _ => error "refin broken: lev2-branch in ptyps changed?";

 (*case 1: no refinement *)

 case refin [] ori1 (hd pbla_branch) of 

   SOME ["pbla"] => () | _ => error "refin case 1 broken";

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

 case refin [] ori2 (hd pbla_branch) of 

   SOME ["pbla", "pbla3"] => () | _ => error "refin case 2 broken";

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

 case refin [] ori3 (hd pbla_branch) of 

   SOME ["pbla", "pbla2"] => () | _ => error "refin case 3 broken";

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

 case refin [] ori4 (hd pbla_branch) of 

   SOME ["pbla", "pbla2", "pbla2y"] => () | _ => error "refin case 4 broken";

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

 val [Store.Node ("pbla",_,[_, ppp as Store.Node ("pbla2",_,_), _])] = pbla_branch;

 case refin ["pbla"] ori4 ppp of 

   SOME ["pbla", "pbla2", "pbla2y"] => () | _ => error "refin case 5 broken";

 ==================================================================*)

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

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

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

 (*case 1: no refinement *)

 case refine_ori ori1 ["pbla", "refine", "test"] of 

   NONE => () | _ => error "refine_ori case 1 broken";

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

 case refine_ori ori2 ["pbla", "refine", "test"] of 

   SOME ["pbla3", "pbla", "refine", "test"] => () | _ => error "refine_ori case 2 broken";

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

 case refine_ori ori3 ["pbla", "refine", "test"] of 

   SOME ["pbla2", "pbla", "refine", "test"] => () | _ => error "refine_ori case 3 broken";

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

 case refine_ori ori4 ["pbla", "refine", "test"] of 

   SOME ["pbla2y","pbla2","pbla", "refine", "test"] => () | _ => error "refine_ori case 4 broken";

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

 case refine_ori ori4 ["pbla2","pbla", "refine", "test"] of 

   SOME ["pbla2y", "pbla2", "pbla", "refine", "test"] => () | _ => error "refine_ori case 5 broken";

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

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

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

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

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

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

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

 	    "boundVariable aaa222yyy"];

 (*case 1: no refinement *)

 case refine fmz1 ["pbla", "refine", "test"] of

   [Matches (["pbla", "refine", "test"], _), 

    NoMatch (["pbla1", "pbla", "refine", "test"], _), 

    NoMatch (["pbla2", "pbla", "refine", "test"], _), 

    NoMatch (["pbla3", "pbla", "refine", "test"], _)] => ()

  | _ => error "--- refine test-pbtyps --- broken with case 1";

 (* 

 *** pass ["pbla"]

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

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

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

 val it =

   [Matches

      (["pbla"],

       {Find=[],

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

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

    NoMatch

      (["pbla1","pbla"],

       {Find=[],

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

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

    NoMatch

      (["pbla2","pbla"],

       {Find=[],

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

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

    NoMatch

      (["pbla3","pbla"],

       {Find=[],

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

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

   : match list*)

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

 case refine fmz2 ["pbla", "refine", "test"] of

   [Matches (["pbla", "refine", "test"], _),

    NoMatch (["pbla1", "pbla", "refine", "test"], _),

    NoMatch (["pbla2", "pbla", "refine", "test"], _),

    Matches (["pbla3", "pbla", "refine", "test"], _)] => ()

  | _ => error "--- refine test-pbtyps --- broken with case 2";

 (* 

 *** pass ["pbla"]

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

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

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

 val it =

   [Matches

      (["pbla"],

       {Find=[],

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

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

    NoMatch

      (["pbla1","pbla"],

       {Find=[],

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

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

    NoMatch

      (["pbla2","pbla"],

       {Find=[],

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

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

    Matches

      (["pbla3","pbla"],

       {Find=[],

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

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

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

 case refine fmz3 ["pbla", "refine", "test"] of

   [Matches (["pbla", "refine", "test"], _),

    NoMatch (["pbla1", "pbla", "refine", "test"], _),

    Matches (["pbla2", "pbla", "refine", "test"], _),

    NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),

    NoMatch (["pbla2y", "pbla2", "pbla", "refine", "test"], _),

    NoMatch (["pbla2z", "pbla2", "pbla", "refine", "test"], _),

    NoMatch (["pbla3", "pbla", "refine", "test"], _)] => ()

  | _ => error "--- refine test-pbtyps --- broken with case 3";

 (* 

 *** pass ["pbla"]

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

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

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

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

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

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

 val it =

   [Matches

      (["pbla"],

       {Find=[],

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

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

    NoMatch

      (["pbla1","pbla"],

       {Find=[],

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

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

    Matches

      (["pbla2","pbla"],

       {Find=[],

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

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

    NoMatch

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

       {Find=[],

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

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

    NoMatch

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

       {Find=[],

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

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

    NoMatch

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

       {Find=[],

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

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

    NoMatch

      (["pbla3","pbla"],

       {Find=[],

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

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

   : match list*)

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

 case refine fmz4 ["pbla", "refine", "test"] of

     [Matches (["pbla", "refine", "test"], _), 

      NoMatch (["pbla1", "pbla", "refine", "test"], _), 

      Matches (["pbla2", "pbla", "refine", "test"], _), 

      NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _), 

      Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => ()

   | _ => error "--- refine test-pbtyps --- broken with case 4";

 (* 

 *** pass ["pbla"]

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

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

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

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

 val it =

   [Matches

      (["pbla"],

       {Find=[],

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

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

    NoMatch

      (["pbla1","pbla"],

       {Find=[],

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

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

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

    Matches

      (["pbla2","pbla"],

       {Find=[],

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

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

    NoMatch

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

       {Find=[],

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

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

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

    Matches

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

       {Find=[],

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

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

   : match list*)

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

 case refine fmz4 ["pbla2","pbla", "refine", "test"] of

     [Matches (["pbla2", "pbla", "refine", "test"], _), 

      NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _), 

      Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => ()

   | _ => error "--- refine test-pbtyps --- broken with case 5";

 (* 

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

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

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

 val it =

   [Matches

      (["pbla2","pbla"],

       {Find=[],

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

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

    NoMatch

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

       {Find=[],

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

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

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

    Matches

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

       {Find=[],

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

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

   : match list*)

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

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

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

 val c = [];

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

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

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

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

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

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

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

 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "solutions L"*)

 (*=== specify a not-matching problem ---vvvvvvvvvvvvvvvvvvvvvvvvvvvv*)

 val nxt = (Specify_Problem ["LINEAR","univariate","equation","test"]);

 (*=== specify a not-matching problem ---^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)

 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "solutions L"*)

 val www =

 case f of PpcKF (Problem [],

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

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

    Where = [False www(*! ! ! ! ! !*)],

    Relate = [],...}) => www(*! ! !*)

 | _ => error "--- Refine_Problem broken 1";

 if www = "matches (x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\nmatches (?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\nmatches (?a + x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8) \<or>\nmatches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x ^^^ 2 + 8)"

 then () else error "--- Refine_Problem broken 2";

 (*ML> f; 

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

         (Problem ["LINEAR","univariate","equation","test"],   <<<<<===== diff.to above WN120313

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

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

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

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

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

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

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

           With=[]}))) : mout

 *)

 (*[], Pbl*)val (p,_,f,nxt,_,pt) = (me nxt p c pt) (*Empty_Tac ?!?*);

 (*=== refine problem -----vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)

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

 (*=== refine problem -----^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)

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

 (*("Specify_Problem", Specify_Problem ["normalise", "univariate", ...])*)

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

 (*nxt = ("Specify_Theory", Specify_Theory "Test")*)

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

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

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

 (*nxt = ("Apply_Method", *)

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

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

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

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

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

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

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

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

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

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

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

 (**)

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

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

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

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

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

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

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

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

 (*("Specify_Problem", Specify_Problem ["LINEAR", "univariate", ...])*)

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

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

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

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

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

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

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

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

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

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

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

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

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

 (*Check_Postcond ["normalise","univariate","equation","test"])*)

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

 val FormKF res = f;

 if res = "[x = 2]"

 then case nxt of End_Proof' => ()

   | _ => error "new behaviour in test:refine.sml:miniscript with mini-subpb 1"

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

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

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

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

 val n = Probl_Def.empty;

 (#guh : Problem.T -> Check_Unique.id) Probl_Def.empty;

 fun XXXnode coll (Store.Node (_,[n],ns)) =

     [(#guh : Problem.T -> Check_Unique.id) n]

 and XXXnodes coll [] = coll

   | XXXnodes coll (n::ns : Problem.T Store.T) = (XXXnode coll n) @ 

 					    (XXXnodes coll ns);

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

 fun node coll (Store.Node (_,[n],ns)) =

     [(#guh : 'a -> Check_Unique.id) n]

 and nodes coll [] = coll

   | nodes coll (n::ns : 'a Store.T) = (node coll n) @ (nodes coll ns);

 Error:

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

    Found near #guh : 'a -> Check_Unique.id

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

 ((Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.id))) (get_ptyps ());

 sort string_ord (((Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.id))) (get_ptyps ()));

 show_pblguhs ();

 sort_pblguhs ();

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

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

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

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

 (* ERROR: Exception Bind raised *)

 val (Store.Node (id1,[n1 as {guh=guh1,...} : Problem.T], ns1)::

      Store.Node (id2,[n2 as {guh=guh2,...} : Problem.T], ns2):: _) = (get_ptyps ());

 (*

 nodes [] guh1 (get_ptyps ());

 nodes [] guh2 (get_ptyps ());

 *)

 val (Store.Node (id1,[n1 as {guh=guh1,...} : Problem.T], ns1)

      ::

      Store.Node (id2,[n2 as {guh=guh2,...} : Problem.T], 

 	   (Store.Node (id21,[n21 as {guh=guh21,...} : Problem.T], ns21)) :: _ )

      ::

      Store.Node (id3,[n3 as {guh=guh3,...} : Problem.T], ns3)

      ::

      _ ) = (get_ptyps ());

 (*

 nodes [] guh3 (get_ptyps ());

 nodes [] guh21 (get_ptyps ());

 *)

 "----------- fun mark --------------------------------------------";

 "----------- fun mark --------------------------------------------";

 "----------- fun mark --------------------------------------------";

 (*

 > val xs = [1,1,1,2,4,4,5];

 > mark (op=) xs;

 val it = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)]

 *)

 "----------- fun coll --------------------------------------------";

 "----------- fun coll --------------------------------------------";

 "----------- fun coll --------------------------------------------";

 (* 

 > val xs = [1,1,1,2,4,4,4];

 > coll (op=) xs;

 val it = [1,2,4] : int list

 *)

 "----------- fun coll_variants -----------------------------------";

 "----------- fun coll_variants -----------------------------------";

 "----------- fun coll_variants -----------------------------------";

 (* val xs = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)];

 > col [] ([(fst o hd) xs],(snd o hd) xs) (tl xs);

 val it = [([1,2,3],1),([0],2),([1,2],4),([0],5)]  *)

 "----------- fun add_id ------------------------------------------";

 "----------- fun add_id ------------------------------------------";

 "----------- fun add_id ------------------------------------------";

 (*

 > val xs = [([1,2,3],1),([0],2),([1,2],4),([0],5)];

 > add_id xs;

 val it = [(1,([#,#,#],1)),(2,([#],2)),(3,([#,#],4)),(4,([#],5))]

  *)

 "----------- fun filter_vat --------------------------------------";

 "----------- fun filter_vat --------------------------------------";

 "----------- fun filter_vat --------------------------------------";

 (*> map (filter_vat oris) [1,2,3];

 val it =

   [[(1,[1,2,3],"#Given",Const (#,#),[# $ #]),

     (2,[1,2,3],"#Find",Const (#,#),[Free #]),

     (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),

     (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]),

     (6,[1],"#undef",Const (#,#),[Free #]),

     (9,[1,2],"#undef",Const (#,#),[# $ #]),

     (11,[1,2,3],"#undef",Const (#,#),[# $ #])],

    [(1,[1,2,3],"#Given",Const (#,#),[# $ #]),

     (2,[1,2,3],"#Find",Const (#,#),[Free #]),

     (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),

     (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]),

     (7,[2],"#undef",Const (#,#),[Free #]),

     (9,[1,2],"#undef",Const (#,#),[# $ #]),

     (11,[1,2,3],"#undef",Const (#,#),[# $ #])],

    [(1,[1,2,3],"#Given",Const (#,#),[# $ #]),

     (2,[1,2,3],"#Find",Const (#,#),[Free #]),

     (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),

     (5,[3],"#Relate",Const (#,#),[# $ #,# $ #,# $ #]),

     (8,[3],"#undef",Const (#,#),[Free #]),

     (10,[3],"#undef",Const (#,#),[# $ #]),

     (11,[1,2,3],"#undef",Const (#,#),[# $ #])]] : ori list list*)

 "----------- fun match_pbl ---------------------------------------";

 "----------- fun match_pbl ---------------------------------------";

 "----------- fun match_pbl ---------------------------------------";

 (* 

 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",

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

 val pbt as {thy = thy, where_ = pre, ppc = ppc,...} =

     get_pbt ["univariate","equation"];

 match_pbl fmz pbt;

 *)

 "----------- fun match_oris --------------------------------------";

 "----------- fun match_oris --------------------------------------";

 "----------- fun match_oris --------------------------------------";

 (* val (pblRD,ori)=("xxx",oris);

  val py = get_pbt ["equation"];

  val py = get_pbt ["univariate","equation"];

  val py = get_pbt ["linear","univariate","equation"];

  val py = get_pbt ["root\"","univariate","equation"];

  match_oris (#prls py) ori (#ppc py, #where_ py);

   *)

 "-------- fun get_fun_ids ----------------------------------------------------";

 "-------- fun get_fun_ids ----------------------------------------------------";

 "-------- fun get_fun_ids ----------------------------------------------------";

 val met_fun_ids = get_fun_ids @{theory Biegelinie};

 if map fst (get_fun_ids @{theory Biegelinie}) = 

   ["Biegelinie.function_to_equality", "Biegelinie.biegelinie", "Biegelinie.belastung_zu_biegelinie",

     "Biegelinie.setzte_randbedingungen"] then () else error "get_fun_ids changed"