neuper@38036: (* Title: tests on calchead.sml neuper@38036: Author: Walther Neuper 051013, neuper@37906: (c) due to copyright terms neuper@37906: neuper@38011: 12345678901234567890123456789012345678901234567890123456789012345678901234567890 neuper@38011: 10 20 30 40 50 60 70 80 neuper@37906: *) neuper@37906: neuper@38010: "--------------------------------------------------------"; neuper@38010: "table of contents --------------------------------------"; neuper@38010: "--------------------------------------------------------"; neuper@38010: "--------- get_interval after replace} other 2 ----------"; neuper@38010: "--------- maximum example with 'specify' ---------------"; neuper@38010: "--------- maximum example with 'specify', fmz <> [] ----"; neuper@38010: "--------- maximum example with 'specify', fmz = [] -----"; neuper@38010: "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--"; neuper@38010: "--------- regression test fun is_copy_named ------------"; neuper@38011: "--------- regr.test fun cpy_nam ------------------------"; neuper@38051: "--------- check specify phase --------------------------"; neuper@38010: "--------------------------------------------------------"; neuper@38010: "--------------------------------------------------------"; neuper@38010: "--------------------------------------------------------"; neuper@38009: neuper@38036: (*========== inhibit exn ======================================================= neuper@38011: "--------- get_interval after replace} other 2 ----------"; neuper@38011: "--------- get_interval after replace} other 2 ----------"; neuper@38011: "--------- get_interval after replace} other 2 ----------"; neuper@38011: states := []; neuper@37906: CalcTree neuper@37906: [(["equality (x+1=2)", "solveFor x","solutions L"], neuper@37906: ("Test.thy", neuper@37906: ["sqroot-test","univariate","equation","test"], neuper@37906: ["Test","squ-equ-test-subpbl1"]))]; neuper@37906: Iterator 1; neuper@37906: moveActiveRoot 1; neuper@37906: autoCalculate 1 CompleteCalc; neuper@37906: moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*) neuper@37906: replaceFormula 1 "x = 1"; neuper@37906: (*... returns calcChangedEvent with ...*) neuper@37906: val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res)); neuper@37906: val ((pt,_),_) = get_calc 1; neuper@37906: neuper@37906: print_depth 99;map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3; neuper@37906: if map fst (get_interval ([],Pbl) ([],Res) 9999 pt) = neuper@37906: [([], Pbl), ([1], Frm),([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), neuper@37906: ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), neuper@37906: ([3, 2], Res)] then () else neuper@38031: error "calchead.sml: diff.behav. get_interval after replace} other 2 a"; neuper@37906: neuper@37906: print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); neuper@37906: print_depth 3; neuper@37906: if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) = neuper@37906: [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else neuper@38031: error "modspec.sml: diff.behav. get_interval after replace} other 2 b"; neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: "--------- maximum example with 'specify' ------------------------"; neuper@37906: "--------- maximum example with 'specify' ------------------------"; neuper@37906: "--------- maximum example with 'specify' ------------------------"; neuper@37906: (*" Specify_Problem (match_itms_oris) ";*) neuper@37906: val fmz = neuper@37906: ["fixedValues [r=Arbfix]","maximum A", neuper@37906: "valuesFor [a,b]", neuper@37906: "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]", neuper@37906: "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]", neuper@37906: "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]", neuper@37906: neuper@37906: "boundVariable a","boundVariable b","boundVariable alpha", neuper@37906: "interval {x::real. 0 <= x & x <= 2*r}", neuper@37906: "interval {x::real. 0 <= x & x <= 2*r}", neuper@37906: "interval {x::real. 0 <= x & x <= pi}", neuper@37906: "errorBound (eps=(0::real))"]; neuper@37906: val (dI',pI',mI') = neuper@37906: ("DiffApp.thy",["maximum_of","function"], neuper@37906: ["DiffApp","max_by_calculus"]); neuper@37906: val c = []:cid; neuper@37906: neuper@37906: (*val nxt = Init_Proof' (fmz,(dI',pI',mI')); neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] EmptyPtree; neuper@37906: *) neuper@37906: val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*) neuper@37906: neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (**) neuper@37906: neuper@37906: (*---6.5.03 neuper@37906: val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]"); neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*uncaught exception TYPE 6.5.03*) neuper@37906: neuper@37906: if ppc<>(Problem [], neuper@37906: {Find=[Incompl "maximum",Incompl "valuesFor [a]"], neuper@37906: Given=[Correct "fixedValues [r = Arbfix]"], neuper@37906: Relate=[Incompl "relations []"], Where=[],With=[]}) neuper@38031: then error "test-maximum.sml: model stepwise - different behaviour" neuper@37906: else (); (*different with show_types !!!*) neuper@37906: 6.5.03---*) neuper@37906: neuper@37906: (*-----appl_add should not create Error', but accept as Sup,Syn neuper@37906: val nxt = tac2tac_ pt p (Add_Given "boundVariable a"); neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (**) neuper@37906: val nxt = tac2tac_ pt p (Add_Given "boundVariable a+"); neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (**)---*) neuper@37906: neuper@37906: val m = Specify_Problem ["maximum_of","function"]; neuper@37906: val nxt = tac2tac_ pt p m; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (**) neuper@37906: neuper@37906: if ppc<>(Problem ["maximum_of","function"], neuper@37906: {Find=[Incompl "maximum",Incompl "valuesFor"], neuper@37906: Given=[Correct "fixedValues [r = Arbfix]"], neuper@37906: Relate=[Incompl "relations []"], Where=[],With=[]}) neuper@38031: then error "diffappl.sml: Specify_Problem different behaviour" neuper@37906: else (); neuper@37906: (* WN.3.9.03 (#391) Model_Specify did init_pbl newly neuper@37906: if ppc<>(Problem ["maximum_of","function"], neuper@37906: {Find=[Missing "maximum m_",Missing "valuesFor vs_"], neuper@37906: Given=[Correct "fixedValues [r = Arbfix]"], neuper@37906: Relate=[Missing "relations rs_"],Where=[],With=[]}) neuper@38031: then error "diffappl.sml: Specify_Problem different behaviour" neuper@37906: else ();*) neuper@37906: neuper@37906: val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]); neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (**) neuper@37906: neuper@37906: if ppc<>(Method ["DiffApp","max_by_calculus"], neuper@37906: {Find=[Incompl "maximum",Incompl "valuesFor"], neuper@37981: Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v", neuper@37906: Missing "interval itv_",Missing "errorBound err_"], neuper@37906: Relate=[Incompl "relations []"],Where=[],With=[]}) neuper@38031: then error "diffappl.sml: Specify_Method different behaviour" neuper@37906: else (); neuper@37906: (* WN.3.9.03 (#391) Model_Specify did init_pbl newly neuper@37906: if ppc<>(Method ["DiffApp","max_by_calculus"], neuper@37906: {Find=[Missing "maximum m_",Missing "valuesFor vs_"], neuper@37981: Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v", neuper@37906: Missing "interval itv_",Missing "errorBound err_"], neuper@37906: Relate=[Missing "relations rs_"],Where=[],With=[]}) neuper@38031: then error "diffappl.sml: Specify_Method different behaviour" neuper@37906: else ();*) neuper@37906: neuper@37906: neuper@37906: neuper@37906: "--------- maximum example with 'specify', fmz <> [] -------------"; neuper@37906: "--------- maximum example with 'specify', fmz <> [] -------------"; neuper@37906: "--------- maximum example with 'specify', fmz <> [] -------------"; neuper@37906: val fmz = neuper@37906: ["fixedValues [r=Arbfix]","maximum A", neuper@37906: "valuesFor [a,b]", neuper@37906: "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]", neuper@37906: "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]", neuper@37906: "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]", neuper@37906: neuper@37906: "boundVariable a","boundVariable b","boundVariable alpha", neuper@37906: "interval {x::real. 0 <= x & x <= 2*r}", neuper@37906: "interval {x::real. 0 <= x & x <= 2*r}", neuper@37906: "interval {x::real. 0 <= x & x <= pi}", neuper@37906: "errorBound (eps=(0::real))"]; neuper@37906: val (dI',pI',mI') = neuper@37906: ("DiffApp.thy",["maximum_of","function"], neuper@37906: ["DiffApp","max_by_calculus"]); neuper@37906: val c = []:cid; neuper@37906: (*val nxt = Init_Proof' (fmz,(dI',pI',mI'));*) neuper@37906: val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; neuper@37906: neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] pt; neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Add_Given "fixedValues [(r::real) = Arbfix]" : tac*) neuper@37906: neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Add_Find "maximum (A::bool)" : tac*) neuper@37906: neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Add_Find "valuesFor [(a::real)]" : tac*) neuper@37906: neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Add_Find "valuesFor [(b::real)]" : tac*) neuper@37906: neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Add_Relation "relations [A = a * b]" *) neuper@37906: neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*Add_Relation "relations\n [((a::real) // (#2::real)) ..."*) neuper@37906: neuper@37906: (*---------------------------- FIXXXXME.meNEW !!! partial Add-Relation !!! neuper@37906: nxt_specif <> specify ?! neuper@37906: neuper@37906: if nxt<>(Add_Relation neuper@37906: "relations [(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]") neuper@38031: then error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*) neuper@37906: neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: ------------------------------ FIXXXXME.meNEW !!! ---*) neuper@37906: neuper@37906: (*val nxt = Specify_Theory "DiffApp.thy" : tac*) neuper@37906: neuper@37924: val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms); neuper@37906: neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Specify_Problem ["maximum_of","function"]*) neuper@37906: neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Specify_Method ("DiffApp.thy","max_by_calculus")*) neuper@37906: neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Add_Given "boundVariable a" : tac*) neuper@37906: neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Add_Given "interval {x. #0 <= x & x <= #2 * r}" : *) neuper@37906: neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Add_Given "errorBound (eps = #0)" : tac*) neuper@37906: neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Apply_Method ("DiffApp.thy","max_by_calculus") *) neuper@37906: if nxt<>(Apply_Method ["DiffApp","max_by_calculus"]) neuper@38031: then error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus" else (); neuper@37906: neuper@37906: neuper@37906: "--------- maximum example with 'specify', fmz = [] --------------"; neuper@37906: "--------- maximum example with 'specify', fmz = [] --------------"; neuper@37906: "--------- maximum example with 'specify', fmz = [] --------------"; neuper@37906: val fmz = []; neuper@37906: val (dI',pI',mI') = empty_spec; neuper@37906: val c = []:cid; neuper@37906: neuper@37906: val nxt = Init_Proof' (fmz,(dI',pI',mI'));(*!!!!!!!!*) neuper@37906: (*val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; !!!*) neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt e_pos' [] neuper@37906: EmptyPtree; neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Specify_Theory "e_domID" : tac*) neuper@37906: neuper@37906: val nxt = Specify_Theory "DiffApp.thy"; neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Specify_Problem ["e_pblID"] : tac*) neuper@37906: neuper@37906: val nxt = Specify_Problem ["maximum_of","function"]; neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Add_Given "fixedValues" : tac*) neuper@37906: neuper@37906: val nxt = Add_Given "fixedValues [r=Arbfix]"; neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Add_Find "maximum" : tac*) neuper@37906: neuper@37906: val nxt = Add_Find "maximum A"; neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: neuper@37906: neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Add_Find "valuesFor" : tac*) neuper@37906: neuper@37906: val nxt = Add_Find "valuesFor [a]"; neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Add_Relation "relations" --- neuper@37906: --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*) neuper@37906: neuper@37906: (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env .... neuper@37906: if nxt<>(Add_Relation "relations []") neuper@38031: then error "test specify, fmz <> []: nxt <> Add_Relation.." neuper@37906: else (); (*different with show_types !!!*) neuper@37906: *) neuper@37906: neuper@37906: val nxt = Add_Relation "relations [(A=a+b)]"; neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Specify_Method ("e_domID","e_metID") : tac*) neuper@37906: neuper@37906: val nxt = Specify_Method ["DiffApp","max_by_calculus"]; neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Add_Given "boundVariable" : tac*) neuper@37906: neuper@37906: val nxt = Add_Given "boundVariable alpha"; neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Add_Given "interval" : tac*) neuper@37906: neuper@37906: val nxt = Add_Given "interval {x. 2 <= x & x <= 3}"; neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Add_Given "errorBound" : tac*) neuper@37906: neuper@37906: val nxt = Add_Given "errorBound (eps=999)"; neuper@37906: val nxt = tac2tac_ pt p nxt; neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *) neuper@37906: (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env .... neuper@37906: if nxt<>(Apply_Method ("DiffApp.thy","max_by_calculus")) neuper@38031: then error "test specify, fmz <> []: nxt <> Add_Relation.." neuper@37906: else (); neuper@37906: *) neuper@37906: neuper@37906: (* 2.4.00 nach Transfer specify -> hard_gen neuper@37906: val nxt = Apply_Method ("DiffApp.thy","max_by_calculus"); neuper@37906: val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *) neuper@37906: (*val nxt = Empty_Tac : tac*) neuper@37906: neuper@38036: ============ inhibit exn =====================================================*) neuper@37906: neuper@38051: (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. neuper@38051: neuper@38011: "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--"; neuper@38011: "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--"; neuper@38011: "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--"; neuper@37906: val Const ("Script.SubProblem",_) $ neuper@37906: (Const ("Pair",_) $ neuper@37906: Free (dI',_) $ neuper@37906: (Const ("Pair",_) $ pI' $ mI')) $ ags' = neuper@37906: (*...copied from stac2tac_*) neuper@38011: str2term ( neuper@38011: "SubProblem (EqSystem', [linear, system], [no_met]) " ^ neuper@38011: " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^ neuper@38011: " REAL_LIST [c, c_2]]"); neuper@37906: val ags = isalist2list ags'; neuper@37906: val pI = ["linear","system"]; neuper@37906: val pats = (#ppc o get_pbt) pI; neuper@38011: "-a1-----------------------------------------------------"; neuper@38011: (*match_ags = fn : theory -> pat list -> term list -> ori list*) neuper@38011: val xxx = match_ags (theory "EqSystem") pats ags; neuper@38011: "-a2-----------------------------------------------------"; neuper@38011: case match_ags (theory "Isac") pats ags of neuper@37906: [(1, [1], "#Given", Const ("Descript.equalities", _), _), neuper@37906: (2, [1], "#Given", Const ("EqSystem.solveForVars", _), neuper@37906: [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]), neuper@38011: (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])] neuper@37906: =>() neuper@38031: | _ => error "calchead.sml match_ags 2 args Nok ----------------"; neuper@37906: neuper@37906: neuper@38011: "-b------------------------------------------------------"; neuper@37906: val Const ("Script.SubProblem",_) $ neuper@37906: (Const ("Pair",_) $ neuper@37906: Free (dI',_) $ neuper@37906: (Const ("Pair",_) $ pI' $ mI')) $ ags' = neuper@37906: (*...copied from stac2tac_*) neuper@38011: str2term ( neuper@38011: "SubProblem (EqSystem', [linear, system], [no_met]) " ^ neuper@38011: " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^ neuper@38011: " REAL_LIST [c, c_2], BOOL_LIST ss''']"); neuper@37906: val ags = isalist2list ags'; neuper@37906: val pI = ["linear","system"]; neuper@37906: val pats = (#ppc o get_pbt) pI; neuper@38011: "-b1-----------------------------------------------------"; neuper@38011: val xxx = match_ags (theory "Isac") pats ags; neuper@38011: "-b2-----------------------------------------------------"; neuper@38011: case match_ags (theory "EqSystem") pats ags of neuper@37906: [(1, [1], "#Given", Const ("Descript.equalities", _), _), neuper@37906: (2, [1], "#Given", Const ("EqSystem.solveForVars", _), neuper@37906: [_ $ Free ("c", _) $ _, neuper@37906: _ $ Free ("c_2", _) $ _]), neuper@38011: (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])] neuper@38011: (* type of Find: [Free ("ss'''", "bool List.list")]*) neuper@37906: =>() neuper@38031: | _ => error "calchead.sml match_ags copy-named dropped --------"; neuper@37906: neuper@37906: neuper@38011: "-c---ERROR case: stac is missing #Given equalities e_s--"; neuper@37906: val stac as Const ("Script.SubProblem",_) $ neuper@37906: (Const ("Pair",_) $ neuper@37906: Free (dI',_) $ neuper@37906: (Const ("Pair",_) $ pI' $ mI')) $ ags' = neuper@37906: (*...copied from stac2tac_*) neuper@38011: str2term ( neuper@38011: "SubProblem (EqSystem', [linear, system], [no_met]) " ^ neuper@38011: " [REAL_LIST [c, c_2]]"); neuper@38011: val ags = isalist2list ags'; neuper@37906: val pI = ["linear","system"]; neuper@37906: val pats = (#ppc o get_pbt) pI; neuper@38051: (*---inhibit exn provided by this testcase-------------------------- neuper@38051: val xxx - match_ags (theory "EqSystem") pats ags; neuper@38051: -------------------------------------------------------------------*) neuper@38011: "-c1-----------------------------------------------------"; neuper@38011: "--------------------------step through code match_ags---"; neuper@38011: val (thy, pbt:pat list, ags) = (theory "EqSystem", pats, ags); neuper@38011: fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_); neuper@38011: val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*) neuper@38011: val cy = filter is_copy_named pbt; (*=solution*) neuper@38051: (*---inhibit exn provided by this testcase-------------------------- neuper@38051: val oris' - matc thy pbt' ags []; neuper@38051: -------------------------------------------------------------------*) neuper@38011: "-------------------------------step through code matc---"; neuper@38011: val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []); neuper@38011: (is_copy_named_idstr o free2str) t; neuper@38011: "---if False:..."; neuper@38051: (*---inhibit exn provided by this testcase-------------------------- neuper@38051: val opt - mtc thy p a; neuper@38051: -------------------------------------------------------------------*) neuper@38011: "--------------------------------step through code mtc---"; neuper@38051: val (thy, (str, (dsc, _)):pat, ty $ var) - (thy, p, a); neuper@38011: cterm_of; neuper@38051: val ttt - (dsc $ var); neuper@38051: (*---inhibit exn provided by this testcase-------------------------- neuper@38011: cterm_of thy (dsc $ var); neuper@38051: -------------------------------------------------------------------*) neuper@38011: "-------------------------------------step through end---"; neuper@38011: neuper@38011: case ((match_ags (theory "EqSystem") pats ags) neuper@38011: handle ERROR _ => []) of (*why not TYPE ?WN100920*) neuper@37906: [] => match_ags_msg pI stac ags neuper@38031: | _ => error "calchead.sml match_ags 1st arg missing --------"; neuper@37906: neuper@37906: neuper@38011: "-d------------------------------------------------------"; neuper@37906: val stac as Const ("Script.SubProblem",_) $ neuper@37906: (Const ("Pair",_) $ neuper@37906: Free (dI',_) $ neuper@37906: (Const ("Pair",_) $ pI' $ mI')) $ ags' = neuper@37906: (*...copied from stac2tac_*) neuper@38011: str2term ( neuper@38011: "SubProblem (Test',[univariate,equation,test]," ^ neuper@38011: " [no_met]) [BOOL (x+1=2), REAL x]"); neuper@38011: val AGS = isalist2list ags'; neuper@37906: val pI = ["univariate","equation","test"]; neuper@38011: val PATS = (#ppc o get_pbt) pI; neuper@38011: "-d1-----------------------------------------------------"; neuper@38011: "--------------------------step through code match_ags---"; neuper@38011: val (thy, pbt:pat list, ags) = (theory "Test", PATS, AGS); neuper@38011: fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_); neuper@38011: val pbt' = filter_out is_copy_named pbt; neuper@38011: val cy = filter is_copy_named pbt; neuper@38011: val oris' = matc thy pbt' ags []; neuper@38011: "-------------------------------step through code matc---"; neuper@38011: val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []); neuper@38011: (is_copy_named_idstr o free2str) t; neuper@38011: "---if False:..."; neuper@38011: val opt = mtc thy p a; neuper@38011: "--------------------------------step through code mtc---"; neuper@38011: val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a); neuper@38011: val ttt = (dsc $ var); neuper@38011: cterm_of thy (dsc $ var); neuper@38011: val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori); neuper@38011: neuper@38011: "-d2-----------------------------------------------------"; neuper@38011: pbt = []; (*false*) neuper@38011: "-------------------------------step through code matc---"; neuper@38011: val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt, ags, oris @ [ori]); neuper@38011: (is_copy_named_idstr o free2str) t; neuper@38011: "---if False:..."; neuper@38011: val opt = mtc thy p a; neuper@38011: "--------------------------------step through code mtc---"; neuper@38011: val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a); neuper@38011: val ttt = (dsc $ var); neuper@38011: cterm_of thy (dsc $ var); neuper@38011: val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori); neuper@38011: "-d3-----------------------------------------------------"; neuper@38011: pbt = []; (*true, base case*) neuper@38011: "-----------------continue step through code match_ags---"; neuper@38011: val oris' = oris @ [ori]; (*result 2 oris, cpy_nam added later*) neuper@38011: "--------------------------------step through cpy_nam----"; neuper@38011: val (pbt, oris, p as (field, (dsc, t)):pat) = (pbt', oris', hd cy); neuper@38011: (*t = "v_v'i'" : term OLD: t = "v_i_"*) neuper@38011: "--------------------------------------------------------"; neuper@38011: fun is_copy_named_generating_idstr str = neuper@38011: if is_copy_named_idstr str neuper@38011: then case (rev o explode) str of neuper@38011: (*"_"::"_"::"_"::_ => false*) neuper@38011: "'"::"'"::"'"::_ => false neuper@38011: | _ => true neuper@38011: else false; neuper@38011: fun is_copy_named_generating (_, (_, t)) = neuper@38011: (is_copy_named_generating_idstr o free2str) t; neuper@38011: "--------------------------------------------------------"; neuper@38011: is_copy_named_generating p (*true*); neuper@38011: fun sel (_,_,d,ts) = comp_ts (d, ts); neuper@38011: val cy' = (implode o (drop_last_n 3) o explode o free2str) t; neuper@38011: (*"v_v" OLD: "v_"*) neuper@38011: val ext = (last_elem o drop_last o explode o free2str) t; neuper@38011: (*"i" OLD: "i"*) neuper@38011: val vars' = map (free2str o snd o snd) pbt(*cpy-nam filtered_out*); neuper@38011: (*["e_e", "v_v"] OLD: ["e_", "v_"]*) neuper@38011: val vals = map sel oris; neuper@38011: (*[x+1=2, x] OLD: [x+1=2, x] : term list*) neuper@38011: vars' ~~ vals; neuper@38011: (*[("e_e", [x+1=2), ("v_v", x)] OLD: [("e_", [x+1=2), ("v_", x)]*) neuper@38011: (assoc (vars'~~vals, cy')); neuper@38032: (*SOME (Free ("x", "RealDef.real")) : term option*) neuper@38011: val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext; neuper@38011: (*x_i*) neuper@38011: "-----------------continue step through code match_ags---"; neuper@38011: val cy' = map (cpy_nam pbt' oris') cy; neuper@38011: (*[([1], "#Find", "solutions, [x_i"] (*as terms*) )]*) neuper@38011: "-------------------------------------step through end---"; neuper@38011: neuper@38011: case match_ags thy PATS AGS of neuper@38011: [(1, [1], "#Given", Const ("Descript.equality", _), neuper@38011: [Const ("op =", _) $ (Const ("Groups.plus_class.plus", _) $ neuper@38011: Free ("x", _) $ Free ("1", _)) $ Free ("2", _)]), neuper@38011: (2, [1], "#Given", Const ("Descript.solveFor", _), [Free ("x", _)]), neuper@38011: (3, [1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)])] neuper@37906: => () neuper@38031: | _ => error "calchead.sml match_ags [univariate,equation,test]--"; neuper@38009: neuper@38010: neuper@38010: "--------- regression test fun is_copy_named ------------"; neuper@38010: "--------- regression test fun is_copy_named ------------"; neuper@38010: "--------- regression test fun is_copy_named ------------"; neuper@38010: val trm = (1, (2, @{term "v'i'"})); neuper@38031: if is_copy_named trm then () else error "regr. is_copy_named 1"; neuper@38010: val trm = (1, (2, @{term "e_e"})); neuper@38031: if is_copy_named trm then error "regr. is_copy_named 2" else (); neuper@38010: val trm = (1, (2, @{term "L'''"})); neuper@38031: if is_copy_named trm then () else error "regr. is_copy_named 3"; neuper@38010: neuper@38010: (* out-comment 'structure CalcHead'... neuper@38010: val trm = (1, (2, @{term "v'i'"})); neuper@38031: if is_copy_named_generating trm then () else error "regr. is_copy_named"; neuper@38010: val trm = (1, (2, @{term "L'''"})); neuper@38031: if is_copy_named_generating trm then error "regr. is_copy_named" else (); neuper@38010: *) neuper@38011: neuper@38011: "--------- regr.test fun cpy_nam ------------------------"; neuper@38011: "--------- regr.test fun cpy_nam ------------------------"; neuper@38011: "--------- regr.test fun cpy_nam ------------------------"; neuper@38011: (*data from above - match_ags, is_cp, cpy_nam +with EqSystem (!)-:*) neuper@38011: (*the model-pattern, is_copy_named are filter_out*) neuper@38011: pbt = [("#Given", (@{term "equality"}, @{term "e_e :: bool"})), neuper@38011: ("#Given", (@{term "solveFor"}, @{term "v_v :: real"} ))]; neuper@38011: (*the model specific for an example*) neuper@38011: oris = [([1], "#Given", @{term "equality"} , [str2term "x+1= 2"]), neuper@38011: ([1], "#Given", @{term "solveFor"} , [@{term "x :: real"} ])]; neuper@38011: cy = [("#Find", (@{term "solutions"}, @{term "v_v'i' :: bool list"}))]; neuper@38011: (*...all must be true*) neuper@38011: neuper@38011: case cpy_nam pbt oris (hd cy) of neuper@38011: ([1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)]) => () neuper@38031: | _ => error "calchead.sml regr.test cpy_nam-1-"; neuper@38011: neuper@38011: (*new data: cpy_nam without changing the name*) neuper@38011: @{term "equalities"}; type_of @{term "[x_1+1=2,x_2=0]"}; neuper@38011: @{term "solveForVars"}; type_of @{term "[x_1,x_2]::real list"}; neuper@38011: @{term "solution"}; type_of @{term "ss''' :: bool list"}; neuper@38011: (*the model-pattern for ["linear", "system"], is_copy_named are filter_out*) neuper@38011: val pbt = [("#Given", (@{term "equalities"}, @{term "e_s :: bool list"})), neuper@38011: ("#Given", (@{term "solveForVars v_s"}, @{term "v_s :: bool list"} ))]; neuper@38011: (*the model specific for an example*) neuper@38011: val oris = [([1], "#Given", @{term "equalities"} ,[str2term "[x_1+1=2,x_2=0]"]), neuper@38011: ([1], "#Given", @{term "solveForVars"} , [@{term "[x_1,x_2]::real list"}])]; neuper@38011: val cy = [("#Find", (@{term "solution"}, @{term "ss''' :: bool list"})) neuper@38011: (*could be more than 1*)]; neuper@38011: neuper@38011: case cpy_nam pbt oris (hd cy) of neuper@38011: ([1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)]) => () neuper@38031: | _ => error "calchead.sml regr.test cpy_nam-2-"; neuper@38051: neuper@38051: -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) neuper@38051: neuper@38051: neuper@38051: "--------- check specify phase --------------------------"; neuper@38051: "--------- check specify phase --------------------------"; neuper@38051: "--------- check specify phase --------------------------"; neuper@38051: (*val fmz = ["functionTerm (x^^^2 + 1)",*) neuper@38051: val fmz = ["functionTerm (x + 1)", neuper@38051: "integrateBy x","antiDerivative FF"]; neuper@38051: val (dI',pI',mI') = neuper@38051: ("Integrate",["integrate","function"], neuper@38051: ["diff","integration"]); neuper@38051: val p = e_pos'; val c = []; neuper@38051: "--- step 1 --"; neuper@38051: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; neuper@38051: (*> val it = "--- step 1 --" : string neuper@38051: val f = neuper@38051: Form' neuper@38051: (PpcKF neuper@38051: (0, EdUndef, 0, Nundef, neuper@38051: (Problem [], neuper@38051: {Find = [], With = [], Given = [], Where = [], Relate = []}))) neuper@38051: : mout neuper@38051: val nxt = ("Model_Problem", Model_Problem) : string * tac neuper@38051: val p = ([], Pbl) : pos' neuper@38051: val pt = neuper@38051: Nd (PblObj neuper@38051: {env = None, fmz = neuper@38051: (["functionTerm (x^^^2 + 1)", "integrateBy x", neuper@38051: "antiDerivative FF"], neuper@38051: ("Integrate.thy", ["integrate", "function"], neuper@38051: ["diff", "integration"])), neuper@38051: loc = neuper@38051: (Some (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)), neuper@38051: None), neuper@38051: cell = None, meth = [], spec = ("e_domID", ["e_pblID"], ["e_metID"]), neuper@38051: probl = [], branch = TransitiveB, neuper@38051: origin = neuper@38051: ([(1, [1], "#Given", neuper@38051: Const ("Descript.functionTerm", "RealDef.real => Tools.una"), neuper@38051: [Const ("op +", neuper@38051: "[RealDef.real, RealDef.real] => RealDef.real") $ neuper@38051: (Const ("Atools.pow", neuper@38051: "[RealDef.real, RealDef.real] => RealDef.real") $ neuper@38051: Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $ neuper@38051: Free ("1", "RealDef.real")]), neuper@38051: (2, [1], "#Given", neuper@38051: Const ("Integrate.integrateBy", "RealDef.real => Tools.una"), neuper@38051: [Free ("x", "RealDef.real")]), neuper@38051: (3, [1], "#Find", neuper@38051: Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"), neuper@38051: [Free ("FF", "RealDef.real")])], neuper@38051: ("Integrate.thy", ["integrate", "function"], ["diff", "integration"]), neuper@38051: Const ("Integrate.Integrate", neuper@38051: "(RealDef.real, RealDef.real) * => RealDef.real") $ neuper@38051: (Const ("Pair", neuper@38051: "[RealDef.real, RealDef.real] neuper@38051: => (RealDef.real, RealDef.real) *") $ neuper@38051: (Const ("op +", neuper@38051: "[RealDef.real, RealDef.real] => RealDef.real") $ neuper@38051: (Const ("Atools.pow", neuper@38051: "[RealDef.real, RealDef.real] => RealDef.real") $ neuper@38051: Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $ neuper@38051: Free ("1", "RealDef.real")) $ neuper@38051: Free ("x", "RealDef.real"))), neuper@38051: ostate = Incomplete, result = (Const ("empty", "'a"), [])}, neuper@38051: []) : ptree*) neuper@38051: "----- WN101007 worked until here (checked same as isac2002) ---"; neuper@38055: if nxt = ("Model_Problem", Model_Problem) then () neuper@38055: else error "clchead.sml: check specify phase step 1"; neuper@38051: "--- step 2 --"; neuper@38051: val (p,_,f,nxt,_,pt) = me nxt p c pt; (*Florian: see response buffer, top*) neuper@38051: (*val it = "--- step 2 --" : string neuper@38051: val p = ([], Pbl) : pos' neuper@38051: val f = neuper@38051: Form' neuper@38051: (PpcKF neuper@38051: (0, EdUndef, 0, Nundef, neuper@38051: (Problem [], neuper@38051: {Find = [Incompl "Integrate.antiDerivative"], neuper@38051: With = [], neuper@38051: Given = [Incompl "functionTerm", Incompl "integrateBy"], neuper@38051: Where = [], neuper@38051: Relate = []}))) : mout neuper@38051: val nxt = ("Add_Given", Add_Given "functionTerm (x ^^^ 2 + 1)") : tac'_ neuper@38051: val pt = neuper@38051: Nd (PblObj neuper@38051: {env = None, fmz = neuper@38051: (["functionTerm (x^^^2 + 1)", "integrateBy x", neuper@38051: "antiDerivative FF"], neuper@38051: ("Integrate.thy", ["integrate", "function"], neuper@38051: ["diff", "integration"])), neuper@38051: loc = neuper@38051: (Some neuper@38051: (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)), neuper@38051: None), neuper@38051: cell = None, meth = [], spec = neuper@38051: ("e_domID", ["e_pblID"], ["e_metID"]), probl = neuper@38051: [(0, [], false, "#Given", neuper@38051: Inc ((Const ("Descript.functionTerm", neuper@38051: "RealDef.real => Tools.una"),[]), neuper@38051: (Const ("empty", "'a"), []))), neuper@38051: (0, [], false, "#Given", neuper@38051: Inc ((Const ("Integrate.integrateBy", neuper@38051: "RealDef.real => Tools.una"),[]), neuper@38051: (Const ("empty", "'a"), []))), neuper@38051: (0, [], false, "#Find", neuper@38051: Inc ((Const ("Integrate.antiDerivative", neuper@38051: "RealDef.real => Tools.una"),[]), neuper@38051: (Const ("empty", "'a"), [])))], neuper@38051: branch = TransitiveB, origin = neuper@38051: ([(1, [1], "#Given", neuper@38051: Const ("Descript.functionTerm", "RealDef.real => Tools.una"), neuper@38051: [Const ("op +", neuper@38051: "[RealDef.real, RealDef.real] => RealDef.real") $ neuper@38051: (Const ("Atools.pow", neuper@38051: "[RealDef.real, RealDef.real] => RealDef.real") $ neuper@38051: Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $ neuper@38051: Free ("1", "RealDef.real")]), neuper@38051: (2, [1], "#Given", neuper@38051: Const ("Integrate.integrateBy", "RealDef.real => Tools.una"), neuper@38051: [Free ("x", "RealDef.real")]), neuper@38051: (3, [1], "#Find", neuper@38051: Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"), neuper@38051: [Free ("FF", "RealDef.real")])], neuper@38051: ("Integrate.thy", ["integrate", "function"], ["diff", "integration"]), neuper@38051: Const ("Integrate.Integrate", neuper@38051: "(RealDef.real, RealDef.real) * => RealDef.real") $ neuper@38051: (Const ("Pair", neuper@38051: "[RealDef.real, RealDef.real] neuper@38051: => (RealDef.real, RealDef.real) *") $ neuper@38051: (Const ("op +", neuper@38051: "[RealDef.real, RealDef.real] => RealDef.real") $ neuper@38051: (Const ("Atools.pow", neuper@38051: "[RealDef.real, RealDef.real] => RealDef.real") $ neuper@38051: Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $ neuper@38051: Free ("1", "RealDef.real")) $ neuper@38051: Free ("x", "RealDef.real"))), neuper@38051: ostate = Incomplete, result = (Const ("empty", "'a"), [])}, neuper@38051: []) : ptree*) neuper@38052: "----- WN101007 ptree checked same as isac2002, diff. in nxt --- REPAIRED"; neuper@38055: if nxt = ("Add_Given", Add_Given "functionTerm (x + 1)") then () neuper@38055: else error "clchead.sml: check specify phase step 2"; neuper@38051: "--- step 3 --"; neuper@38051: val (p,_,f,nxt,_,pt) = me nxt p c pt; neuper@38055: "----- WN101008 ptree checked same as isac2002, diff. in nxt --- REPAIRED"; neuper@38055: if nxt = ("Add_Given", Add_Given "integrateBy x") then () neuper@38055: else error "clchead.sml: check specify phase step 2"; neuper@38055: neuper@38052: (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. neuper@38051: -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)