akargl@42108: (* 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@42279: "--------- check: fmz matches pbt -----------------------"; wneuper@59265: "--------- fun typeless ---------------------------------"; wneuper@59265: "--------- fun variants_in ------------------------------"; wneuper@59265: "--------- fun is_list_type -----------------------------"; wneuper@59265: "--------- fun has_list_type ----------------------------"; wneuper@59265: "--------- fun tag_form ---------------------------------"; wneuper@59265: "--------- fun foldr1, foldl1 ---------------------------"; neuper@38010: "--------------------------------------------------------"; neuper@38010: "--------------------------------------------------------"; neuper@38010: "--------------------------------------------------------"; neuper@38009: akargl@42108: neuper@38011: "--------- get_interval after replace} other 2 ----------"; neuper@38011: "--------- get_interval after replace} other 2 ----------"; neuper@38011: "--------- get_interval after replace} other 2 ----------"; s1210629013@55445: reset_states (); neuper@41970: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@41970: ("Test", ["sqroot-test","univariate","equation","test"], neuper@37906: ["Test","squ-equ-test-subpbl1"]))]; neuper@37906: Iterator 1; neuper@37906: moveActiveRoot 1; wneuper@59248: 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: wneuper@59111: default_print_depth 99;map fst (get_interval ([],Pbl) ([],Res) 9999 pt);default_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: wneuper@59111: default_print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); default_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: "--------- 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@48894: "valuesFor [a,b::real]", neuper@48894: "relations [A=a*(b::real), (a/2)^^^2 + (b/2)^^^2 = (r::real)^^^2]", neuper@48894: "relations [A=a*(b::real), (a/2)^^^2 + (b/2)^^^2 = (r::real)^^^2]", neuper@48894: "relations [A=a*(b::real), a/2=r*sin alpha, b/2 = (r::real)*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@38058: ("DiffApp",["maximum_of","function"], neuper@37906: ["DiffApp","max_by_calculus"]); neuper@37906: val c = []:cid; neuper@37906: neuper@37906: val (p,_,f,(_,nxt),_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; neuper@37906: val nxt = tac2tac_ pt p nxt; wneuper@59267: val(p,_, 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; wneuper@59267: val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; neuper@37906: (**) neuper@37906: neuper@37906: val nxt = tac2tac_ pt p (Add_Find "valuesFor [(a::real)]"); wneuper@59267: val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; neuper@37906: if ppc<>(Problem [], neuper@37906: {Find=[Incompl "maximum",Incompl "valuesFor [a]"], neuper@37906: Given=[Correct "fixedValues [r = Arbfix]"], neuper@48894: Relate=[Incompl "relations"], Where=[],With=[]}) neuper@38031: then error "test-maximum.sml: model stepwise - different behaviour" neuper@48894: else (); neuper@37906: neuper@48894: val nxt = tac2tac_ pt p (Add_Given "boundVariable (a::real)"); neuper@48894: (* WN1130630 THE maximum example WORKS IN isabisac09-2; neuper@48894: MOST LIKELY IT IS BROKEN BY INTRODUCING ctxt. neuper@48894: Some tests have been broken much earlier, neuper@48894: see test/../calchead.sml "inhibit exn 010830". *) neuper@48894: (*========== inhibit exn WN1130630 maximum example broken ========================= wneuper@59267: val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; neuper@48894: ============ inhibit exn WN1130630 maximum example broken =======================*) neuper@48894: neuper@48894: val nxt = tac2tac_ pt p (Add_Given "boundVariable a+"); neuper@48894: (*========== inhibit exn WN1130630 maximum example broken ========================= akargl@42181: (* ERROR: Exception Bind raised *) wneuper@59267: val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; neuper@48894: ============ inhibit exn WN1130630 maximum example broken =======================*) neuper@37906: neuper@37906: val m = Specify_Problem ["maximum_of","function"]; neuper@37906: val nxt = tac2tac_ pt p m; wneuper@59267: val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; neuper@48894: (*========== inhibit exn WN1130630 maximum example broken ========================= 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@48894: ============ inhibit exn WN1130630 maximum example broken =======================*) neuper@37906: neuper@37906: val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]); wneuper@59267: val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; neuper@48894: (*========== inhibit exn WN1130630 maximum example broken ========================= 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@48894: ============ inhibit exn WN1130630 maximum example broken =======================*) 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@38058: ("DiffApp",["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; wneuper@59267: val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt e_pos' [] pt; neuper@37906: val nxt = tac2tac_ pt p nxt; wneuper@59267: val(p,_, 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; wneuper@59267: val(p,_, 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; wneuper@59267: val(p,_, 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; wneuper@59267: val(p,_, 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; wneuper@59267: val(p,_, 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; wneuper@59267: val(p,_, 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; wneuper@59267: val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; neuper@37906: ------------------------------ FIXXXXME.meNEW !!! ---*) neuper@37906: neuper@38058: (*val nxt = Specify_Theory "DiffApp" : 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; wneuper@59267: val(p,_, 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; wneuper@59267: val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; neuper@38058: (*val nxt = Specify_Method ("DiffApp","max_by_calculus")*) neuper@37906: neuper@37906: val nxt = tac2tac_ pt p nxt; wneuper@59267: val(p,_, 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; wneuper@59267: val(p,_, 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; wneuper@59267: val(p,_, 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; wneuper@59267: val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; neuper@38058: (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *) wneuper@59253: case nxt of (Apply_Method ["DiffApp","max_by_calculus"]) => () wneuper@59253: | _ => error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus"; 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'))]; !!!*) wneuper@59267: val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt e_pos' [] neuper@37906: EmptyPtree; neuper@37906: val nxt = tac2tac_ pt p nxt; wneuper@59267: val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Specify_Theory "e_domID" : tac*) neuper@37906: neuper@38058: val nxt = Specify_Theory "DiffApp"; neuper@37906: val nxt = tac2tac_ pt p nxt; wneuper@59267: val(p,_, 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; wneuper@59267: val(p,_, 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; wneuper@59267: val(p,_, 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: wneuper@59267: val(p,_, 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; wneuper@59267: val(p,_, 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: akargl@42181: (*========== inhibit exn 010830 =======================================================*) 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: *) akargl@42181: (*========== inhibit exn 010830 =======================================================*) neuper@37906: neuper@37906: val nxt = Add_Relation "relations [(A=a+b)]"; neuper@37906: val nxt = tac2tac_ pt p nxt; wneuper@59267: val(p,_, 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; wneuper@59267: val(p,_, 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; wneuper@59267: val(p,_, 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; wneuper@59267: val(p,_, 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; wneuper@59267: val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; neuper@37906: (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *) akargl@42108: neuper@37906: (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env .... neuper@38058: if nxt<>(Apply_Method ("DiffApp","max_by_calculus")) neuper@38031: then error "test specify, fmz <> []: nxt <> Add_Relation.." neuper@37906: else (); neuper@37906: *) neuper@37906: (* 2.4.00 nach Transfer specify -> hard_gen neuper@38058: val nxt = Apply_Method ("DiffApp","max_by_calculus"); wneuper@59267: val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; *) neuper@37906: (*val nxt = Empty_Tac : tac*) 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@41972: (Const ("Product_Type.Pair",_) $ neuper@37906: Free (dI',_) $ neuper@41972: (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = neuper@37906: (*...copied from stac2tac_*) neuper@38011: str2term ( neuper@55279: "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@55279: 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@48894: val xxx = match_ags @{theory "EqSystem"} pats ags; neuper@38011: "-a2-----------------------------------------------------"; neuper@48894: 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@38011: "-b------------------------------------------------------"; neuper@37906: val Const ("Script.SubProblem",_) $ neuper@41972: (Const ("Product_Type.Pair",_) $ neuper@37906: Free (dI',_) $ neuper@41972: (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = neuper@37906: (*...copied from stac2tac_*) neuper@38011: str2term ( neuper@55279: "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@55279: val pI = ["LINEAR","system"]; neuper@37906: val pats = (#ppc o get_pbt) pI; neuper@38011: "-b1-----------------------------------------------------"; neuper@48894: val xxx = match_ags @{theory "Isac"} pats ags; neuper@38011: "-b2-----------------------------------------------------"; neuper@48894: 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@38011: "-c---ERROR case: stac is missing #Given equalities e_s--"; neuper@37906: val stac as Const ("Script.SubProblem",_) $ neuper@41972: (Const ("Product_Type.Pair",_) $ neuper@37906: Free (dI',_) $ neuper@41972: (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = neuper@37906: (*...copied from stac2tac_*) neuper@38011: str2term ( neuper@55279: "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^ neuper@38011: " [REAL_LIST [c, c_2]]"); neuper@38011: val ags = isalist2list ags'; neuper@55279: val pI = ["LINEAR","system"]; neuper@37906: val pats = (#ppc o get_pbt) pI; neuper@48895: (*============ inhibit exn AK110726 ============================================== neuper@38051: val xxx - match_ags (theory "EqSystem") pats ags; neuper@48895: ============ inhibit exn AK110726 ==============================================*) neuper@38011: "-c1-----------------------------------------------------"; neuper@38011: "--------------------------step through code match_ags---"; neuper@48894: 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@48895: (*============ inhibit exn AK110726 ============================================== neuper@38051: val oris' - matc thy pbt' ags []; neuper@48895: ============ inhibit exn AK110726 ==============================================*) 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@48895: (*============ inhibit exn AK110726 ============================================== neuper@38051: val opt - mtc thy p a; neuper@48895: ============ inhibit exn AK110726 ==============================================*) neuper@38011: "--------------------------------step through code mtc---"; neuper@48894: val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a); wneuper@59188: Thm.global_cterm_of; neuper@48894: val ttt = (dsc $ var); neuper@48895: (*============ inhibit exn AK110726 ============================================== wneuper@59188: Thm.global_cterm_of thy (dsc $ var); neuper@48895: ============ inhibit exn AK110726 ==============================================*) neuper@48894: neuper@48894: "-------------------------------------step through end---"; neuper@48894: "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--"; neuper@48894: val Const ("Script.SubProblem",_) $ neuper@48894: (Const ("Product_Type.Pair",_) $ neuper@48894: Free (dI',_) $ neuper@48894: (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = neuper@48894: (*...copied from stac2tac_*) neuper@48894: str2term ( neuper@55279: "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^ neuper@48894: " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^ neuper@48894: " REAL_LIST [c, c_2]]"); neuper@48894: val ags = isalist2list ags'; neuper@55279: val pI = ["LINEAR","system"]; neuper@48894: val pats = (#ppc o get_pbt) pI; neuper@48894: "-a1-----------------------------------------------------"; neuper@48894: (*match_ags = fn : theory -> pat list -> term list -> ori list*) neuper@48894: val xxx = match_ags @{theory "EqSystem"} pats ags; neuper@48894: "-a2-----------------------------------------------------"; neuper@48894: case match_ags @{theory "Isac"} pats ags of neuper@48894: [(1, [1], "#Given", Const ("Descript.equalities", _), _), neuper@48894: (2, [1], "#Given", Const ("EqSystem.solveForVars", _), neuper@48894: [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]), neuper@48894: (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])] neuper@48894: =>() neuper@48894: | _ => error "calchead.sml match_ags 2 args Nok ----------------"; neuper@48894: neuper@48894: "-b------------------------------------------------------"; neuper@48894: val Const ("Script.SubProblem",_) $ neuper@48894: (Const ("Product_Type.Pair",_) $ neuper@48894: Free (dI',_) $ neuper@48894: (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = neuper@48894: (*...copied from stac2tac_*) neuper@48894: str2term ( neuper@55279: "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^ neuper@48894: " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^ neuper@48894: " REAL_LIST [c, c_2], BOOL_LIST ss''']"); neuper@48894: val ags = isalist2list ags'; neuper@55279: val pI = ["LINEAR","system"]; neuper@48894: val pats = (#ppc o get_pbt) pI; neuper@48894: "-b1-----------------------------------------------------"; neuper@48894: val xxx = match_ags @{theory "Isac"} pats ags; neuper@48894: "-b2-----------------------------------------------------"; neuper@48894: case match_ags @{theory "EqSystem"} pats ags of neuper@48894: [(1, [1], "#Given", Const ("Descript.equalities", _), _), neuper@48894: (2, [1], "#Given", Const ("EqSystem.solveForVars", _), neuper@48894: [_ $ Free ("c", _) $ _, neuper@48894: _ $ Free ("c_2", _) $ _]), neuper@48894: (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])] neuper@48894: (* type of Find: [Free ("ss'''", "bool List.list")]*) neuper@48894: =>() neuper@48894: | _ => error "calchead.sml match_ags copy-named dropped --------"; neuper@48894: neuper@48894: "-c---ERROR case: stac is missing #Given equalities e_s--"; neuper@48894: val stac as Const ("Script.SubProblem",_) $ neuper@48894: (Const ("Product_Type.Pair",_) $ neuper@48894: Free (dI',_) $ neuper@48894: (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = neuper@48894: (*...copied from stac2tac_*) neuper@48894: str2term ( neuper@55279: "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^ neuper@48894: " [REAL_LIST [c, c_2]]"); neuper@48894: val ags = isalist2list ags'; neuper@55279: val pI = ["LINEAR","system"]; neuper@48894: val pats = (#ppc o get_pbt) pI; neuper@48895: (*============ inhibit exn AK110726 ============================================== neuper@48894: val xxx - match_ags (theory "EqSystem") pats ags; neuper@48894: -------------------------------------------------------------------*) neuper@48894: "-c1-----------------------------------------------------"; neuper@48894: "--------------------------step through code match_ags---"; neuper@48894: val (thy, pbt:pat list, ags) = (@{theory "EqSystem"}, pats, ags); neuper@48894: fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_); neuper@48894: val pbt' = filter_out is_copy_named pbt; (*=equalities, solveForVars*) neuper@48894: val cy = filter is_copy_named pbt; (*=solution*) neuper@48895: (*============ inhibit exn AK110726 ============================================== neuper@48894: val oris' - matc thy pbt' ags []; neuper@48894: -------------------------------------------------------------------*) neuper@48894: "-------------------------------step through code matc---"; neuper@48894: val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []); neuper@48894: (is_copy_named_idstr o free2str) t; neuper@48894: "---if False:..."; neuper@48895: (*============ inhibit exn AK110726 ============================================== neuper@48894: val opt - mtc thy p a; neuper@48894: -------------------------------------------------------------------*) neuper@48894: "--------------------------------step through code mtc---"; neuper@48894: val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a); wneuper@59188: Thm.global_cterm_of; neuper@48894: val ttt = (dsc $ var); neuper@48895: (*============ inhibit exn AK110726 ============================================== wneuper@59188: Thm.global_cterm_of thy (dsc $ var); neuper@38051: -------------------------------------------------------------------*) neuper@38011: "-------------------------------------step through end---"; neuper@38011: neuper@48894: 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@48894: "-d------------------------------------------------------"; neuper@48894: val stac as Const ("Script.SubProblem",_) $ neuper@48894: (Const ("Product_Type.Pair",_) $ neuper@48894: Free (dI',_) $ neuper@48894: (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = neuper@48894: (*...copied from stac2tac_*) neuper@48894: str2term ( neuper@48894: "SubProblem (Test',[univariate,equation,test]," ^ neuper@48894: " [no_met]) [BOOL (x+1=2), REAL x]"); neuper@48894: val AGS = isalist2list ags'; neuper@48894: val pI = ["univariate","equation","test"]; neuper@48894: neuper@48894: neuper@48894: case ((match_ags @{theory "EqSystem"} pats ags) neuper@48894: handle ERROR _ => []) of (*why not TYPE ?WN100920*) neuper@48894: [] => match_ags_msg pI stac ags neuper@48894: | _ => error "calchead.sml match_ags 1st arg missing --------"; neuper@37906: neuper@38011: "-d------------------------------------------------------"; neuper@37906: val stac as Const ("Script.SubProblem",_) $ neuper@41972: (Const ("Product_Type.Pair",_) $ neuper@37906: Free (dI',_) $ neuper@41972: (Const ("Product_Type.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@48894: 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); wneuper@59188: Thm.global_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); wneuper@59188: Thm.global_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@48894: then case (rev o Symbol.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@48894: val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t; neuper@38011: (*"v_v" OLD: "v_"*) neuper@48894: val ext = (last_elem o drop_last o Symbol.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@55279: (*SOME (Free ("x", "Real.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@41922: [Const ("HOL.eq", _) $ (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: "--------- 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@55279: (*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: "--------- 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@38058: ("Integrate", ["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@55279: Const ("Descript.functionTerm", "Real.real => Tools.una"), neuper@38051: [Const ("op +", neuper@55279: "["Real.real, "Real.real] => "Real.real") $ neuper@38051: (Const ("Atools.pow", neuper@55279: "["Real.real, "Real.real] => "Real.real") $ neuper@55279: Free ("x", "Real.real") $ Free ("2", "Real.real")) $ neuper@55279: Free ("1", "Real.real")]), neuper@38051: (2, [1], "#Given", neuper@55279: Const ("Integrate.integrateBy", "Real.real => Tools.una"), neuper@55279: [Free ("x", "Real.real")]), neuper@38051: (3, [1], "#Find", neuper@55279: Const ("Integrate.antiDerivative", "Real.real => Tools.una"), neuper@55279: [Free ("FF", "Real.real")])], neuper@38058: ("Integrate", ["integrate", "function"], ["diff", "integration"]), neuper@38051: Const ("Integrate.Integrate", neuper@55279: "("Real.real, "Real.real) * => "Real.real") $ neuper@41972: (Const ("Product_Type.Pair", neuper@55279: "["Real.real, "Real.real] neuper@55279: => ("Real.real, "Real.real) *") $ neuper@38051: (Const ("op +", neuper@55279: "["Real.real, "Real.real] => "Real.real") $ neuper@38051: (Const ("Atools.pow", neuper@55279: "["Real.real, "Real.real] => "Real.real") $ neuper@55279: Free ("x", "Real.real") $ Free ("2", "Real.real")) $ neuper@55279: Free ("1", "Real.real")) $ neuper@55279: Free ("x", "Real.real"))), neuper@38051: ostate = Incomplete, result = (Const ("empty", "'a"), [])}, wneuper@59279: []) : ctree*) neuper@38051: "----- WN101007 worked until here (checked same as isac2002) ---"; wneuper@59253: case nxt of ("Model_Problem", Model_Problem) => () wneuper@59253: | _ => 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@38058: ("Integrate", ["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@55279: "Real.real => Tools.una"),[]), neuper@38051: (Const ("empty", "'a"), []))), neuper@38051: (0, [], false, "#Given", neuper@38051: Inc ((Const ("Integrate.integrateBy", neuper@55279: "Real.real => Tools.una"),[]), neuper@38051: (Const ("empty", "'a"), []))), neuper@38051: (0, [], false, "#Find", neuper@38051: Inc ((Const ("Integrate.antiDerivative", neuper@55279: "Real.real => Tools.una"),[]), neuper@38051: (Const ("empty", "'a"), [])))], neuper@38051: branch = TransitiveB, origin = neuper@38051: ([(1, [1], "#Given", neuper@55279: Const ("Descript.functionTerm", "Real.real => Tools.una"), neuper@38051: [Const ("op +", neuper@55279: "["Real.real, "Real.real] => "Real.real") $ neuper@38051: (Const ("Atools.pow", neuper@55279: "["Real.real, "Real.real] => "Real.real") $ neuper@55279: Free ("x", "Real.real") $ Free ("2", "Real.real")) $ neuper@55279: Free ("1", "Real.real")]), neuper@38051: (2, [1], "#Given", neuper@55279: Const ("Integrate.integrateBy", "Real.real => Tools.una"), neuper@55279: [Free ("x", "Real.real")]), neuper@38051: (3, [1], "#Find", neuper@55279: Const ("Integrate.antiDerivative", "Real.real => Tools.una"), neuper@55279: [Free ("FF", "Real.real")])], neuper@38058: ("Integrate", ["integrate", "function"], ["diff", "integration"]), neuper@38051: Const ("Integrate.Integrate", neuper@55279: "("Real.real, "Real.real) * => "Real.real") $ neuper@41972: (Const ("Product_Type.Pair", neuper@55279: "["Real.real, "Real.real] neuper@55279: => ("Real.real, "Real.real) *") $ neuper@38051: (Const ("op +", neuper@55279: "["Real.real, "Real.real] => "Real.real") $ neuper@38051: (Const ("Atools.pow", neuper@55279: "["Real.real, "Real.real] => "Real.real") $ neuper@55279: Free ("x", "Real.real") $ Free ("2", "Real.real")) $ neuper@55279: Free ("1", "Real.real")) $ neuper@55279: Free ("x", "Real.real"))), neuper@38051: ostate = Incomplete, result = (Const ("empty", "'a"), [])}, wneuper@59279: []) : ctree*) wneuper@59279: "----- WN101007 ctree checked same as isac2002, diff. in nxt --- REPAIRED"; wneuper@59253: case nxt of ("Add_Given", Add_Given "functionTerm (x + 1)") => () wneuper@59253: | _ => error "clchead.sml: check specify phase step 2"; neuper@38051: "--- step 3 --"; neuper@38051: val (p,_,f,nxt,_,pt) = me nxt p c pt; wneuper@59279: "----- WN101008 ctree checked same as isac2002, diff. in nxt --- REPAIRED"; wneuper@59253: case nxt of ("Add_Given", Add_Given "integrateBy x") => () wneuper@59253: | _ => error "clchead.sml: check specify phase step 2"; neuper@42279: neuper@42279: "--------- check: fmz matches pbt -----------------------"; neuper@42279: "--------- check: fmz matches pbt -----------------------"; neuper@42279: "--------- check: fmz matches pbt -----------------------"; neuper@42279: "101230 error *** nxt_add: EX itm. not(dat(itm)<=dat(ori))"; neuper@42279: "the following fmz caused the above error"; neuper@42279: val fmz = ["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"]; neuper@42279: val pI = ["plus_minus","polynom","vereinfachen"]; neuper@42279: neuper@42279: "----- this fmz is transformed to this internal format (TERM --> Pure.term):"; neuper@42279: val ([(1, [1], "#undef", _, [Const ("Pure.term", _ (*"'a \ prop"*)) $ _]), neuper@42279: (*#############################^^^^^^^^^ defined by Isabelle*) neuper@55279: (2, [1], "#Find", Const ("Simplify.normalform", _ (*"Real.real \ Tools.una"*)), neuper@55279: [Free ("N", _ (*"Real.real"*))])], neuper@42279: _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI); neuper@42279: "#undef means: the element with description TERM in fmz did not match "; neuper@42279: "with any element of pbl (fetched by pI), because there we have Simplify.Term"; neuper@42279: "defined in Simplify.thy"; neuper@42279: neuper@42279: "So we try out how to create Simplify.Term:"; neuper@42279: "----- trial 1"; neuper@42279: val Const ("Pure.term", _) $ Free ("ttt", _) = str2term "TERM ttt"; neuper@42279: " ^^^^^^^^^ see above"; neuper@42279: atomwy t; neuper@42279: neuper@42279: "----- trial 2"; neuper@42279: val Free ("term", _) $ Free ("ttt", _) = str2term "term ttt"; neuper@42279: " ^^^^^^^^^^^ means, that no appropriate Const has be found (descriptions are all Const !)"; neuper@42279: atomwy t; neuper@42279: neuper@42279: "----- trial 3"; neuper@42279: val Const ("Simplify.Term", _) $ Free ("ttt", _) = str2term "Term ttt"; neuper@42279: " ^^^^^^^^^^^^^^ this is what in Simplify.thy has been defined "; neuper@42279: " and unsed in pbl [plus_minus,polynom,vereinfachen]"; neuper@42279: atomwy t; neuper@42279: neuper@42279: "----- so this is the correct fmz:"; neuper@42279: val fmz = ["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"]; neuper@42279: val ([(1, [1], "#Given", Const ("Simplify.Term", _), [Const ("Groups.plus_class.plus", _) $ _ $ _]), neuper@42279: (*########################^^^^^^^^^ defined in Simplify.thy*) neuper@42279: (2, [1], "#Find", Const ("Simplify.normalform", _ ), neuper@42279: [Free ("N", _ )])], neuper@42279: _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI); neuper@42279: neuper@42279: "----- we could have checked the pbl at the very beginning and compare with (internal) fmz:"; neuper@42279: val [("#Given", (Const ("Simplify.Term", _), Free ("t_t", _))), neuper@42279: ("#Find", (Const ("Simplify.normalform", _), Free ("n_n", _)))] = (#ppc o get_pbt) pI; neuper@42279: wneuper@59265: "--------- fun typeless ---------------------------------"; wneuper@59265: "--------- fun typeless ---------------------------------"; wneuper@59265: "--------- fun typeless ---------------------------------"; wneuper@59265: (* wneuper@59265: > val (SOME ct) = parse thy "max_relation (A=#2*a*b - a^^^#2)"; wneuper@59265: > val (_,t1) = split_dsc_t hs (Thm.term_of ct); wneuper@59265: > val (SOME ct) = parse thy "A=#2*a*b - a^^^#2"; wneuper@59265: > val (_,t2) = split_dsc_t hs (Thm.term_of ct); wneuper@59265: > typeless t1 = typeless t2; wneuper@59265: val it = true : bool wneuper@59265: *) wneuper@59265: "--------- fun variants_in ------------------------------"; wneuper@59265: "--------- fun variants_in ------------------------------"; wneuper@59265: "--------- fun variants_in ------------------------------"; wneuper@59265: (* wneuper@59265: > cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0; wneuper@59265: val it = ([3],[4,5,5,5,5,5]) : int list * int list wneuper@59265: > coll (op=) [] [1,2,2,2,4,5,5,5,5,5]; wneuper@59265: val it = [1,3,1,5] : int list wneuper@59265: *) wneuper@59265: "--------- fun is_list_type -----------------------------"; wneuper@59265: "--------- fun is_list_type -----------------------------"; wneuper@59265: "--------- fun is_list_type -----------------------------"; wneuper@59265: (* fun destr (Type(str,sort)) = (str,sort); wneuper@59265: > val (SOME ct) = parse thy "lll::real list"; wneuper@59265: > val ty = (#T o rep_cterm) ct; wneuper@59265: > is_list_type ty; wneuper@59265: val it = true : bool wneuper@59265: > destr ty; wneuper@59265: val it = ("List.list",["RealDef.real"]) : string * typ list wneuper@59265: > atomty ((#t o rep_cterm) ct); wneuper@59265: *** ------------- wneuper@59265: *** Free ( lll, real list) wneuper@59265: val it = () : unit wneuper@59265: wneuper@59265: > val (SOME ct) = parse thy "[lll::real]"; wneuper@59265: > val ty = (#T o rep_cterm) ct; wneuper@59265: > is_list_type ty; wneuper@59265: val it = true : bool wneuper@59265: > destr ty; wneuper@59265: val it = ("List.list",["'a"]) : string * typ list wneuper@59265: > atomty ((#t o rep_cterm) ct); wneuper@59265: *** ------------- wneuper@59265: *** Const ( List.list.Cons, [real, real list] => real list) wneuper@59265: *** Free ( lll, real) wneuper@59265: *** Const ( List.list.Nil, real list) wneuper@59265: wneuper@59265: > val (SOME ct) = parse thy "lll"; wneuper@59265: > val ty = (#T o rep_cterm) ct; wneuper@59265: > is_list_type ty; wneuper@59265: val it = false : bool *) wneuper@59265: "--------- fun has_list_type ----------------------------"; wneuper@59265: "--------- fun has_list_type ----------------------------"; wneuper@59265: "--------- fun has_list_type ----------------------------"; wneuper@59265: (* wneuper@59265: > val (SOME ct) = parse thy "lll::real list"; wneuper@59265: > has_list_type (Thm.term_of ct); wneuper@59265: val it = true : bool wneuper@59265: > val (SOME ct) = parse thy "[lll::real]"; wneuper@59265: > has_list_type (Thm.term_of ct); wneuper@59265: val it = false : bool *) wneuper@59265: "--------- fun tag_form ---------------------------------"; wneuper@59265: "--------- fun tag_form ---------------------------------"; wneuper@59265: "--------- fun tag_form ---------------------------------"; wneuper@59265: (* val formal = (the o (parse thy)) "[R::real]"; wneuper@59265: > val given = (the o (parse thy)) "fixed_values (cs::real list)"; wneuper@59265: > tag_form thy (formal, given); wneuper@59265: val it = "fixed_values [R]" : cterm wneuper@59265: *) wneuper@59265: "--------- fun foldr1, foldl1 ---------------------------"; wneuper@59265: "--------- fun foldr1, foldl1 ---------------------------"; wneuper@59265: "--------- fun foldr1, foldl1 ---------------------------"; wneuper@59265: (* wneuper@59265: > val (SOME ct) = parse thy "[a=b,c=d,e=f]"; wneuper@59265: > val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct)); wneuper@59265: > val conj = foldr1 HOLogic.mk_conj (isalist2list (Thm.term_of ct)); wneuper@59265: > Thm.global_cterm_of thy conj; wneuper@59265: val it = "(a = b & c = d) & e = f" : cterm wneuper@59265: *) wneuper@59265: (* wneuper@59265: > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]"; wneuper@59265: > val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct)); wneuper@59265: > val conj = foldl1 HOLogic.mk_conj (isalist2list (Thm.term_of ct)); wneuper@59265: > Thm.global_cterm_of thy conj; wneuper@59265: val it = "a = b & c = d & e = f & g = h" : cterm wneuper@59265: *)