diff -r a37a3ab989f4 -r 3147f2c1525c test/Tools/isac/Interpret/calchead.sml --- a/test/Tools/isac/Interpret/calchead.sml Tue Sep 14 15:46:56 2010 +0200 +++ b/test/Tools/isac/Interpret/calchead.sml Thu Sep 23 08:43:36 2010 +0200 @@ -3,8 +3,8 @@ 051013, (c) due to copyright terms -use"../smltest/ME/calchead.sml"; -use"calchead.sml"; +12345678901234567890123456789012345678901234567890123456789012345678901234567890 + 10 20 30 40 50 60 70 80 *) "--------------------------------------------------------"; @@ -16,15 +16,16 @@ "--------- maximum example with 'specify', fmz = [] -----"; "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--"; "--------- regression test fun is_copy_named ------------"; +"--------- regr.test fun cpy_nam ------------------------"; "--------------------------------------------------------"; "--------------------------------------------------------"; "--------------------------------------------------------"; -(*========================================================================== -"--------- get_interval after replace} other 2 -------------------"; -"--------- get_interval after replace} other 2 -------------------"; -"--------- get_interval after replace} other 2 -------------------"; - states:=[]; +(*WN100914====================================================================== +"--------- get_interval after replace} other 2 ----------"; +"--------- get_interval after replace} other 2 ----------"; +"--------- get_interval after replace} other 2 ----------"; +states := []; CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], ("Test.thy", @@ -324,96 +325,199 @@ val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *) (*val nxt = Empty_Tac : tac*) +====================================================================WN100914*) -"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------"; -"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------"; -"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)-----------"; +"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--"; +"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--"; +"--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--"; val Const ("Script.SubProblem",_) $ (Const ("Pair",_) $ Free (dI',_) $ (Const ("Pair",_) $ pI' $ mI')) $ ags' = (*...copied from stac2tac_*) - str2term - "SubProblem (EqSystem_, [linear, system], [no_met])\ - \ [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2],\ - \ REAL_LIST [c, c_2]]"; + str2term ( + "SubProblem (EqSystem', [linear, system], [no_met]) " ^ + " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^ + " REAL_LIST [c, c_2]]"); val ags = isalist2list ags'; val pI = ["linear","system"]; val pats = (#ppc o get_pbt) pI; -case match_ags Isac.thy pats ags of +"-a1-----------------------------------------------------"; +(*match_ags = fn : theory -> pat list -> term list -> ori list*) +val xxx = match_ags (theory "EqSystem") pats ags; +"-a2-----------------------------------------------------"; +case match_ags (theory "Isac") pats ags of [(1, [1], "#Given", Const ("Descript.equalities", _), _), (2, [1], "#Given", Const ("EqSystem.solveForVars", _), [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]), - (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss___", _)])] + (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])] =>() - | _ => raise error "calchead.sml match_ags 2 args OK -----------------"; + | _ => raise error "calchead.sml match_ags 2 args Nok ----------------"; +"-b------------------------------------------------------"; val Const ("Script.SubProblem",_) $ (Const ("Pair",_) $ Free (dI',_) $ (Const ("Pair",_) $ pI' $ mI')) $ ags' = (*...copied from stac2tac_*) - str2term - "SubProblem (EqSystem_, [linear, system], [no_met])\ - \ [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2],\ - \ REAL_LIST [c, c_2], BOOL_LIST ss___]"; + str2term ( + "SubProblem (EqSystem', [linear, system], [no_met]) " ^ + " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^ + " REAL_LIST [c, c_2], BOOL_LIST ss''']"); val ags = isalist2list ags'; val pI = ["linear","system"]; val pats = (#ppc o get_pbt) pI; -case match_ags Isac.thy pats ags of +"-b1-----------------------------------------------------"; +val xxx = match_ags (theory "Isac") pats ags; +"-b2-----------------------------------------------------"; +case match_ags (theory "EqSystem") pats ags of [(1, [1], "#Given", Const ("Descript.equalities", _), _), (2, [1], "#Given", Const ("EqSystem.solveForVars", _), [_ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]), - (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss___", _)])] - (* type of Find: [Free ("ss___", "bool List.list")]*) + (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])] + (* type of Find: [Free ("ss'''", "bool List.list")]*) =>() | _ => raise error "calchead.sml match_ags copy-named dropped --------"; +"-c---ERROR case: stac is missing #Given equalities e_s--"; val stac as Const ("Script.SubProblem",_) $ (Const ("Pair",_) $ Free (dI',_) $ (Const ("Pair",_) $ pI' $ mI')) $ ags' = (*...copied from stac2tac_*) - str2term - "SubProblem (EqSystem_, [linear, system], [no_met])\ - \ [REAL_LIST [c, c_2]]"; -val ags = isalist2list ags'; + str2term ( + "SubProblem (EqSystem', [linear, system], [no_met]) " ^ + " [REAL_LIST [c, c_2]]"); +val ags = isalist2list ags'; val pI = ["linear","system"]; val pats = (#ppc o get_pbt) pI; -case ((match_ags Isac.thy pats ags) - handle TYPE _ => []) of +(*===inhibit exn provided by this testcase========================== +val xxx = match_ags (theory "EqSystem") pats ags; +===================================================================*) +"-c1-----------------------------------------------------"; +"--------------------------step through code match_ags---"; +val (thy, pbt:pat list, ags) = (theory "EqSystem", pats, ags); +fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_); + val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*) + val cy = filter is_copy_named pbt; (*=solution*) +(*===inhibit exn provided by this testcase========================== + val oris' = matc thy pbt' ags []; +===================================================================*) +"-------------------------------step through code matc---"; +val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []); +(is_copy_named_idstr o free2str) t; +"---if False:..."; +(*===inhibit exn provided by this testcase========================== +val opt = mtc thy p a; +===================================================================*) +"--------------------------------step through code mtc---"; +val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a); +cterm_of; +val ttt = (dsc $ var); +(*===inhibit exn provided by this testcase========================== +cterm_of thy (dsc $ var); +===================================================================*) +"-------------------------------------step through end---"; + +case ((match_ags (theory "EqSystem") pats ags) + handle ERROR _ => []) of (*why not TYPE ?WN100920*) [] => match_ags_msg pI stac ags | _ => raise error "calchead.sml match_ags 1st arg missing --------"; -(* -use"../smltest/ME/calchead.sml"; -*) +"-d------------------------------------------------------"; val stac as Const ("Script.SubProblem",_) $ (Const ("Pair",_) $ Free (dI',_) $ (Const ("Pair",_) $ pI' $ mI')) $ ags' = (*...copied from stac2tac_*) - str2term - "SubProblem (Test_,[univariate,equation,test],\ - \ [no_met]) [BOOL (x+1=2), REAL x]"; -val ags = isalist2list ags'; + str2term ( + "SubProblem (Test',[univariate,equation,test]," ^ + " [no_met]) [BOOL (x+1=2), REAL x]"); +val AGS = isalist2list ags'; val pI = ["univariate","equation","test"]; -val pats = (#ppc o get_pbt) pI; -case match_ags Isac.thy pats ags of - [(1, [1], "#Given", - Const ("Descript.equality", _), - [Const ("op =", _) $ (Const ("op +", _) $ Free ("x", _) $ _) $ _]), - (2, [1], "#Given", Const ("Descript.solveFor", _), [Free ("x", _)]), - (3, [1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)])] - (* type of Find: [Free ("x_i", "bool List.list")]*) +val PATS = (#ppc o get_pbt) pI; +"-d1-----------------------------------------------------"; +"--------------------------step through code match_ags---"; +val (thy, pbt:pat list, ags) = (theory "Test", PATS, AGS); +fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_); + val pbt' = filter_out is_copy_named pbt; + val cy = filter is_copy_named pbt; + val oris' = matc thy pbt' ags []; +"-------------------------------step through code matc---"; +val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []); +(is_copy_named_idstr o free2str) t; +"---if False:..."; +val opt = mtc thy p a; +"--------------------------------step through code mtc---"; +val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a); +val ttt = (dsc $ var); +cterm_of thy (dsc $ var); +val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori); + +"-d2-----------------------------------------------------"; +pbt = []; (*false*) +"-------------------------------step through code matc---"; +val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt, ags, oris @ [ori]); +(is_copy_named_idstr o free2str) t; +"---if False:..."; +val opt = mtc thy p a; +"--------------------------------step through code mtc---"; +val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a); +val ttt = (dsc $ var); +cterm_of thy (dsc $ var); +val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori); +"-d3-----------------------------------------------------"; +pbt = []; (*true, base case*) +"-----------------continue step through code match_ags---"; + val oris' = oris @ [ori]; (*result 2 oris, cpy_nam added later*) +"--------------------------------step through cpy_nam----"; +val (pbt, oris, p as (field, (dsc, t)):pat) = (pbt', oris', hd cy); +(*t = "v_v'i'" : term OLD: t = "v_i_"*) +"--------------------------------------------------------"; +fun is_copy_named_generating_idstr str = + if is_copy_named_idstr str + then case (rev o explode) str of + (*"_"::"_"::"_"::_ => false*) + "'"::"'"::"'"::_ => false + | _ => true + else false; +fun is_copy_named_generating (_, (_, t)) = + (is_copy_named_generating_idstr o free2str) t; +"--------------------------------------------------------"; +is_copy_named_generating p (*true*); + fun sel (_,_,d,ts) = comp_ts (d, ts); + val cy' = (implode o (drop_last_n 3) o explode o free2str) t; + (*"v_v" OLD: "v_"*) + val ext = (last_elem o drop_last o explode o free2str) t; + (*"i" OLD: "i"*) + val vars' = map (free2str o snd o snd) pbt(*cpy-nam filtered_out*); + (*["e_e", "v_v"] OLD: ["e_", "v_"]*) + val vals = map sel oris; + (*[x+1=2, x] OLD: [x+1=2, x] : term list*) +vars' ~~ vals; +(*[("e_e", [x+1=2), ("v_v", x)] OLD: [("e_", [x+1=2), ("v_", x)]*) +(assoc (vars'~~vals, cy')); +(*Some (Free ("x", "RealDef.real")) : term option*) + val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext; + (*x_i*) +"-----------------continue step through code match_ags---"; + val cy' = map (cpy_nam pbt' oris') cy; + (*[([1], "#Find", "solutions, [x_i"] (*as terms*) )]*) +"-------------------------------------step through end---"; + +case match_ags thy PATS AGS of +[(1, [1], "#Given", Const ("Descript.equality", _), + [Const ("op =", _) $ (Const ("Groups.plus_class.plus", _) $ + Free ("x", _) $ Free ("1", _)) $ Free ("2", _)]), + (2, [1], "#Given", Const ("Descript.solveFor", _), [Free ("x", _)]), + (3, [1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)])] => () | _ => raise error "calchead.sml match_ags [univariate,equation,test]--"; -==========================================================================*) "--------- regression test fun is_copy_named ------------"; "--------- regression test fun is_copy_named ------------"; @@ -431,3 +535,37 @@ val trm = (1, (2, @{term "L'''"})); if is_copy_named_generating trm then raise error "regr. is_copy_named" else (); *) + +"--------- regr.test fun cpy_nam ------------------------"; +"--------- regr.test fun cpy_nam ------------------------"; +"--------- regr.test fun cpy_nam ------------------------"; +(*data from above - match_ags, is_cp, cpy_nam +with EqSystem (!)-:*) +(*the model-pattern, is_copy_named are filter_out*) +pbt = [("#Given", (@{term "equality"}, @{term "e_e :: bool"})), + ("#Given", (@{term "solveFor"}, @{term "v_v :: real"} ))]; +(*the model specific for an example*) +oris = [([1], "#Given", @{term "equality"} , [str2term "x+1= 2"]), + ([1], "#Given", @{term "solveFor"} , [@{term "x :: real"} ])]; +cy = [("#Find", (@{term "solutions"}, @{term "v_v'i' :: bool list"}))]; +(*...all must be true*) + +case cpy_nam pbt oris (hd cy) of + ([1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)]) => () + | _ => raise error "calchead.sml regr.test cpy_nam-1-"; + +(*new data: cpy_nam without changing the name*) +@{term "equalities"}; type_of @{term "[x_1+1=2,x_2=0]"}; +@{term "solveForVars"}; type_of @{term "[x_1,x_2]::real list"}; +@{term "solution"}; type_of @{term "ss''' :: bool list"}; +(*the model-pattern for ["linear", "system"], is_copy_named are filter_out*) +val pbt = [("#Given", (@{term "equalities"}, @{term "e_s :: bool list"})), + ("#Given", (@{term "solveForVars v_s"}, @{term "v_s :: bool list"} ))]; +(*the model specific for an example*) +val oris = [([1], "#Given", @{term "equalities"} ,[str2term "[x_1+1=2,x_2=0]"]), + ([1], "#Given", @{term "solveForVars"} , [@{term "[x_1,x_2]::real list"}])]; +val cy = [("#Find", (@{term "solution"}, @{term "ss''' :: bool list"})) + (*could be more than 1*)]; + +case cpy_nam pbt oris (hd cy) of + ([1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)]) => () + | _ => raise error "calchead.sml regr.test cpy_nam-2-";