Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/ME/calchead.sml
author Walther Neuper <neuper@ist.tugraz.at>
Wed, 18 Aug 2010 13:40:09 +0200
branchisac-update-Isa09-2
changeset 37924 6c53fe2519e5
parent 37906 e2b23ba9df13
permissions -rw-r--r--
established thy-ctxt strategy (1..2) for ME/mstools.sml

strategy in 2 steps:
(1) update isac to Isabelle2009-2 with minimal changes
(a) 'parse thy' left as is
'str2t' --> 'str2term_' according to (b)
'comp_dts thy' left as is, but returns term NOT cterm
(b) pretty printing '*2str' always without thy | ctxt
pretty printing '*2str_' always with ctxt
(2) make parsing dependent on context of calculation
(a) 'parse thy' --> 'parse ctxt' simplified by searchin 'thy'
(b) nothin to do 
     1 (* tests on calchead.sml

     2    author: Walther Neuper

     3    051013,

     4    (c) due to copyright terms

     5 

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

     7 use"calchead.sml";

     8 *)

     9 

    10 "-----------------------------------------------------------------";

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

    12 "-----------------------------------------------------------------";

    13 "--------- get_interval after replace} other 2 -------------------";

    14 "--------- maximum example with 'specify' ------------------------";

    15 "--------- maximum example with 'specify', fmz <> [] -------------";

    16 "--------- maximum example with 'specify', fmz = [] --------------";

    17 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------";

    18 "-----------------------------------------------------------------";

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

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

    21 

    22 

    23 "--------- get_interval after replace} other 2 -------------------";

    24 "--------- get_interval after replace} other 2 -------------------";

    25 "--------- get_interval after replace} other 2 -------------------";

    26  states:=[];

    27  CalcTree

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

    29    ("Test.thy", 

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

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

    32  Iterator 1;

    33  moveActiveRoot 1;

    34  autoCalculate 1 CompleteCalc;

    35  moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)

    36  replaceFormula 1 "x = 1"; 

    37  (*... returns calcChangedEvent with ...*)

    38  val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));

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

    40 

    41 print_depth 99;map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3;

    42 if map fst (get_interval ([],Pbl) ([],Res) 9999 pt) = 

    43     [([], Pbl), ([1], Frm),([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), 

    44      ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),

    45       ([3, 2], Res)] then () else

    46 raise error "calchead.sml: diff.behav. get_interval after replace} other 2 a";

    47 

    48 print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt);

    49 print_depth 3;

    50 if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) = 

    51     [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else

    52 raise error "modspec.sml: diff.behav. get_interval after replace} other 2 b";

    53 

    54 

    55 

    56 

    57 "--------- maximum example with 'specify' ------------------------";

    58 "--------- maximum example with 'specify' ------------------------";

    59 "--------- maximum example with 'specify' ------------------------";

    60 (*"              Specify_Problem (match_itms_oris)       ";*)

    61 val fmz =

    62     ["fixedValues [r=Arbfix]","maximum A",

    63      "valuesFor [a,b]",

    64      "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",

    65      "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",

    66      "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",

    67 

    68      "boundVariable a","boundVariable b","boundVariable alpha",

    69      "interval {x::real. 0 <= x & x <= 2*r}",

    70      "interval {x::real. 0 <= x & x <= 2*r}",

    71      "interval {x::real. 0 <= x & x <= pi}",

    72      "errorBound (eps=(0::real))"];

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

    74   ("DiffApp.thy",["maximum_of","function"],

    75    ["DiffApp","max_by_calculus"]);

    76 val c = []:cid;

    77 

    78 (*val nxt = Init_Proof' (fmz,(dI',pI',mI'));

    79 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] EmptyPtree;

    80 *)

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

    82 val nxt = tac2tac_ pt p nxt; 

    83 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

    84 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)

    85 

    86 val nxt = tac2tac_ pt p nxt; 

    87 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

    88 (**)

    89 

    90 (*---6.5.03

    91 val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]"); 

    92 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

    93 (*uncaught exception TYPE 6.5.03*)

    94 

    95 if ppc<>(Problem [],  

    96          {Find=[Incompl "maximum",Incompl "valuesFor [a]"],

    97 	  Given=[Correct "fixedValues [r = Arbfix]"],

    98 	  Relate=[Incompl "relations []"], Where=[],With=[]})

    99 then raise error "test-maximum.sml: model stepwise - different behaviour" 

   100 else (); (*different with show_types !!!*)

   101 6.5.03---*)

   102 

   103 (*-----appl_add should not create Error', but accept as Sup,Syn

   104 val nxt = tac2tac_ pt p (Add_Given "boundVariable a"); 

   105 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   106 (**)

   107 val nxt = tac2tac_ pt p (Add_Given "boundVariable a+"); 

   108 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   109 (**)---*)

   110 

   111 val m = Specify_Problem ["maximum_of","function"];

   112 val nxt = tac2tac_ pt p m; 

   113 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   114 (**)

   115 

   116 if ppc<>(Problem ["maximum_of","function"],  

   117          {Find=[Incompl "maximum",Incompl "valuesFor"],

   118 	  Given=[Correct "fixedValues [r = Arbfix]"],

   119 	  Relate=[Incompl "relations []"], Where=[],With=[]})

   120 then raise error "diffappl.sml: Specify_Problem different behaviour" 

   121 else ();

   122 (* WN.3.9.03 (#391) Model_Specify did init_pbl newly 

   123 if ppc<>(Problem ["maximum_of","function"],

   124    {Find=[Missing "maximum m_",Missing "valuesFor vs_"],

   125     Given=[Correct "fixedValues [r = Arbfix]"],

   126     Relate=[Missing "relations rs_"],Where=[],With=[]})

   127 then raise error "diffappl.sml: Specify_Problem different behaviour" 

   128 else ();*)

   129 

   130 val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]);

   131 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   132 (**)

   133 

   134 if ppc<>(Method ["DiffApp","max_by_calculus"],

   135 	 {Find=[Incompl "maximum",Incompl "valuesFor"],

   136 	  Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_",

   137 		 Missing "interval itv_",Missing "errorBound err_"],

   138 	  Relate=[Incompl "relations []"],Where=[],With=[]})

   139 then raise error "diffappl.sml: Specify_Method different behaviour" 

   140 else ();

   141 (* WN.3.9.03 (#391) Model_Specify did init_pbl newly 

   142 if ppc<>(Method ["DiffApp","max_by_calculus"],

   143    {Find=[Missing "maximum m_",Missing "valuesFor vs_"],

   144     Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_",

   145            Missing "interval itv_",Missing "errorBound err_"],

   146     Relate=[Missing "relations rs_"],Where=[],With=[]})

   147 then raise error "diffappl.sml: Specify_Method different behaviour" 

   148 else ();*)

   149 

   150 

   151 

   152 "--------- maximum example with 'specify', fmz <> [] -------------";

   153 "--------- maximum example with 'specify', fmz <> [] -------------";

   154 "--------- maximum example with 'specify', fmz <> [] -------------";

   155 val fmz =

   156     ["fixedValues [r=Arbfix]","maximum A",

   157      "valuesFor [a,b]",

   158      "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",

   159      "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",

   160      "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",

   161 

   162      "boundVariable a","boundVariable b","boundVariable alpha",

   163      "interval {x::real. 0 <= x & x <= 2*r}",

   164      "interval {x::real. 0 <= x & x <= 2*r}",

   165      "interval {x::real. 0 <= x & x <= pi}",

   166      "errorBound (eps=(0::real))"];

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

   168   ("DiffApp.thy",["maximum_of","function"],

   169    ["DiffApp","max_by_calculus"]);

   170 val c = []:cid;

   171 (*val nxt = Init_Proof' (fmz,(dI',pI',mI'));*)

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

   173 

   174 val nxt = tac2tac_ pt p nxt; 

   175 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] pt;

   176 val nxt = tac2tac_ pt p nxt; 

   177 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   178 (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*)

   179 

   180 val nxt = tac2tac_ pt p nxt; 

   181 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   182 (*val nxt = Add_Find "maximum (A::bool)" : tac*)

   183 

   184 val nxt = tac2tac_ pt p nxt; 

   185 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   186 (*val nxt = Add_Find "valuesFor [(a::real)]" : tac*)

   187 

   188 val nxt = tac2tac_ pt p nxt; 

   189 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   190 (*val nxt = Add_Find "valuesFor [(b::real)]" : tac*)

   191 

   192 val nxt = tac2tac_ pt p nxt; 

   193 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   194 (*val nxt = Add_Relation "relations [A = a * b]" *)

   195 

   196 val nxt = tac2tac_ pt p nxt; 

   197 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   198 (*Add_Relation "relations\n [((a::real) // (#2::real)) ..."*)

   199 

   200 (*---------------------------- FIXXXXME.meNEW !!! partial Add-Relation !!!

   201   nxt_specif <> specify ?!

   202 

   203 if nxt<>(Add_Relation 

   204  "relations [(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]")

   205 then raise error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*)

   206 

   207 val nxt = tac2tac_ pt p nxt; 

   208 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   209 ------------------------------ FIXXXXME.meNEW !!! ---*)

   210 

   211 (*val nxt = Specify_Theory "DiffApp.thy" : tac*)

   212 

   213 val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms);

   214 

   215 val nxt = tac2tac_ pt p nxt; 

   216 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   217 (*val nxt = Specify_Problem ["maximum_of","function"]*)

   218 

   219 val nxt = tac2tac_ pt p nxt; 

   220 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   221 (*val nxt = Specify_Method ("DiffApp.thy","max_by_calculus")*)

   222 

   223 val nxt = tac2tac_ pt p nxt; 

   224 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   225 (*val nxt = Add_Given "boundVariable a" : tac*)

   226 

   227 val nxt = tac2tac_ pt p nxt; 

   228 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   229 (*val nxt = Add_Given "interval {x. #0 <= x & x <= #2 * r}" : *)

   230 

   231 val nxt = tac2tac_ pt p nxt; 

   232 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   233 (*val nxt = Add_Given "errorBound (eps = #0)" : tac*)

   234 

   235 val nxt = tac2tac_ pt p nxt; 

   236 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   237 (*val nxt = Apply_Method ("DiffApp.thy","max_by_calculus") *)

   238 if nxt<>(Apply_Method ["DiffApp","max_by_calculus"])

   239 then raise error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus" else ();

   240 

   241 

   242 "--------- maximum example with 'specify', fmz = [] --------------";

   243 "--------- maximum example with 'specify', fmz = [] --------------";

   244 "--------- maximum example with 'specify', fmz = [] --------------";

   245 val fmz = [];

   246 val (dI',pI',mI') = empty_spec;

   247 val c = []:cid;

   248 

   249 val nxt = Init_Proof' (fmz,(dI',pI',mI'));(*!!!!!!!!*)

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

   251 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] 

   252   EmptyPtree;

   253 val nxt = tac2tac_ pt p nxt; 

   254 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   255 (*val nxt = Specify_Theory "e_domID" : tac*)

   256 

   257 val nxt = Specify_Theory "DiffApp.thy";

   258 val nxt = tac2tac_ pt p nxt; 

   259 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   260 (*val nxt = Specify_Problem ["e_pblID"] : tac*)

   261 

   262 val nxt = Specify_Problem ["maximum_of","function"];

   263 val nxt = tac2tac_ pt p nxt; 

   264 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   265 (*val nxt = Add_Given "fixedValues" : tac*)

   266 

   267 val nxt = Add_Given "fixedValues [r=Arbfix]";

   268 val nxt = tac2tac_ pt p nxt; 

   269 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   270 (*val nxt = Add_Find "maximum" : tac*)

   271 

   272 val nxt = Add_Find "maximum A";

   273 val nxt = tac2tac_ pt p nxt; 

   274 

   275 

   276 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   277 (*val nxt = Add_Find "valuesFor" : tac*)

   278 

   279 val nxt = Add_Find "valuesFor [a]";

   280 val nxt = tac2tac_ pt p nxt; 

   281 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   282 (*val nxt = Add_Relation "relations" --- 

   283   --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*)

   284 

   285 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....

   286 if nxt<>(Add_Relation "relations []")

   287 then raise error "test specify, fmz <> []: nxt <> Add_Relation.." 

   288 else (); (*different with show_types !!!*)

   289 *)

   290 

   291 val nxt = Add_Relation "relations [(A=a+b)]";

   292 val nxt = tac2tac_ pt p nxt; 

   293 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   294 (*val nxt = Specify_Method ("e_domID","e_metID") : tac*)

   295 

   296 val nxt = Specify_Method ["DiffApp","max_by_calculus"];

   297 val nxt = tac2tac_ pt p nxt; 

   298 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   299 (*val nxt = Add_Given "boundVariable" : tac*)

   300 

   301 val nxt = Add_Given "boundVariable alpha";

   302 val nxt = tac2tac_ pt p nxt; 

   303 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   304 (*val nxt = Add_Given "interval" : tac*)

   305 

   306 val nxt = Add_Given "interval {x. 2 <= x & x <= 3}";

   307 val nxt = tac2tac_ pt p nxt; 

   308 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   309 (*val nxt = Add_Given "errorBound" : tac*)

   310 

   311 val nxt = Add_Given "errorBound (eps=999)";

   312 val nxt = tac2tac_ pt p nxt; 

   313 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;

   314 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)

   315 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....

   316 if nxt<>(Apply_Method ("DiffApp.thy","max_by_calculus"))

   317 then raise error "test specify, fmz <> []: nxt <> Add_Relation.." 

   318 else ();

   319 *)

   320 

   321 (* 2.4.00 nach Transfer specify -> hard_gen

   322 val nxt = Apply_Method ("DiffApp.thy","max_by_calculus");

   323 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *)

   324 (*val nxt = Empty_Tac : tac*)

   325 

   326 

   327 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------";

   328 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------";

   329 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------";

   330 val Const ("Script.SubProblem",_) $

   331 	  (Const ("Pair",_) $

   332 		 Free (dI',_) $ 

   333 		 (Const ("Pair",_) $ pI' $ mI')) $ ags' =

   334     (*...copied from stac2tac_*)

   335     str2term 

   336 	"SubProblem (EqSystem_, [linear, system], [no_met])\

   337  \            [bool_list_ [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2],\

   338  \             real_list_ [c, c_2]]";

   339 val ags = isalist2list ags';

   340 val pI = ["linear","system"];

   341 val pats = (#ppc o get_pbt) pI;

   342 case match_ags Isac.thy pats ags of 

   343     [(1, [1], "#Given", Const ("Descript.equalities", _), _),

   344      (2, [1], "#Given", Const ("EqSystem.solveForVars", _),

   345       [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),

   346      (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss___", _)])] 

   347     =>()

   348   | _ => raise error "calchead.sml match_ags 2 args OK -----------------";

   349 

   350 

   351 val Const ("Script.SubProblem",_) $

   352 	  (Const ("Pair",_) $

   353 		 Free (dI',_) $ 

   354 		 (Const ("Pair",_) $ pI' $ mI')) $ ags' =

   355     (*...copied from stac2tac_*)

   356     str2term 

   357 	"SubProblem (EqSystem_, [linear, system], [no_met])\

   358  \            [bool_list_ [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2],\

   359  \             real_list_ [c, c_2], bool_list_ ss___]";

   360 val ags = isalist2list ags';

   361 val pI = ["linear","system"];

   362 val pats = (#ppc o get_pbt) pI;

   363 case match_ags Isac.thy pats ags of 

   364     [(1, [1], "#Given", Const ("Descript.equalities", _), _),

   365      (2, [1], "#Given", Const ("EqSystem.solveForVars", _),

   366          [_ $ Free ("c", _) $ _,

   367           _ $ Free ("c_2", _) $ _]),

   368      (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss___", _)])]

   369     (*         type of Find:            [Free ("ss___", "bool List.list")]*)

   370     =>()

   371   | _ => raise error "calchead.sml match_ags copy-named dropped --------";

   372 

   373 

   374 val stac as Const ("Script.SubProblem",_) $

   375 	 (Const ("Pair",_) $

   376 		Free (dI',_) $ 

   377 		(Const ("Pair",_) $ pI' $ mI')) $ ags' =

   378     (*...copied from stac2tac_*)

   379     str2term 

   380 	"SubProblem (EqSystem_, [linear, system], [no_met])\

   381  \            [real_list_ [c, c_2]]";

   382 val ags = isalist2list ags';

   383 val pI = ["linear","system"];

   384 val pats = (#ppc o get_pbt) pI;

   385 case ((match_ags Isac.thy pats ags)

   386       handle TYPE _ => []) of 

   387     [] => match_ags_msg pI stac ags

   388   | _ => raise error "calchead.sml match_ags 1st arg missing --------";

   389 

   390 (*

   391 use"../smltest/ME/calchead.sml";

   392 *)

   393 

   394 val stac as Const ("Script.SubProblem",_) $

   395 	 (Const ("Pair",_) $

   396 		Free (dI',_) $ 

   397 		(Const ("Pair",_) $ pI' $ mI')) $ ags' =

   398     (*...copied from stac2tac_*)

   399     str2term 

   400 	"SubProblem (Test_,[univariate,equation,test],\

   401  \                    [no_met]) [bool_ (x+1=2), real_ x]";

   402 val ags = isalist2list ags';

   403 val pI = ["univariate","equation","test"];

   404 val pats = (#ppc o get_pbt) pI;

   405 case match_ags Isac.thy pats ags of

   406     [(1, [1], "#Given",

   407       Const ("Descript.equality", _),

   408       [Const ("op =", _) $ (Const ("op +", _) $ Free ("x", _) $ _) $ _]),

   409      (2, [1], "#Given", Const ("Descript.solveFor", _), [Free ("x", _)]),

   410      (3, [1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)])]

   411     (*         type of Find:             [Free ("x_i", "bool List.list")]*)

   412     => ()

   413   | _ => raise error "calchead.sml match_ags [univariate,equation,test]--";
wneuper/isa