neuper@41945: (* Title: All tests on isac; observe outcommented neuper@41943: Author: Walther Neuper 101001 neuper@41943: (c) copyright due to lincense terms. neuper@41943: neuper@41943: $ cd /usr/local/isabisac/test/Tools/isac neuper@41945: $ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy & neuper@41968: 1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890 neuper@41968: 10 20 30 40 50 60 70 80 90 100 neuper@41943: *) neuper@41943: neuper@41954: theory Test_Isac imports Isac neuper@41945: uses neuper@41945: ( "library.sml") neuper@41945: ( "calcelems.sml") neuper@41945: ("ProgLang/termC.sml") neuper@41945: ("ProgLang/calculate.sml") neuper@41945: ("ProgLang/rewrite.sml") neuper@41945: (*("ProgLang/listg.sml") ("ProgLang/scrtools.sml") ("ProgLang/tools.sml") *) neuper@41945: neuper@41945: ("Interpret/mstools.sml") bonzai@41951: ("Interpret/ctree.sml") neuper@41945: ("Interpret/ptyps.sml") neuper@41945: (*("Interpret/generate.sml")*) neuper@41945: ("Interpret/calchead.sml") neuper@41945: (*("Interpret/appl.sml")*) neuper@41945: ("Interpret/rewtools.sml") neuper@41945: (*("Interpret/script.sml") neuper@41945: ("Interpret/solve.sml") neuper@41945: ("Interpret/inform.sml")*) neuper@41945: ("Interpret/mathengine.sml") neuper@41945: neuper@41945: (*("xmlsrc/mathml.sml") neuper@41945: ("xmlsrc/datatypes.sml") neuper@41945: ("xmlsrc/pbl-met-hierarchy.sml") neuper@41945: ("xmlsrc/thy-hierarchy.sml")*) neuper@41945: ("xmlsrc/interface-xml.sml") neuper@41945: neuper@41945: ("Frontend/messages.sml") neuper@41945: ("Frontend/states.sml") neuper@41945: ("Frontend/interface.sml") neuper@41945: ("print_exn_G.sml") neuper@41945: neuper@41945: ("Knowledge/delete.sml") neuper@41945: ("Knowledge/descript.sml") neuper@41945: ("Knowledge/atools.sml") neuper@41945: ("Knowledge/simplify.sml") neuper@41945: ("Knowledge/poly.sml") neuper@41945: ("Knowledge/rational.sml") neuper@41945: ("Knowledge/equation.sml") neuper@41945: ("Knowledge/root.sml") neuper@41945: ("Knowledge/lineq.sml") neuper@41945: ("Knowledge/rooteq.sml") neuper@41945: ("Knowledge/rateq.sml") neuper@41945: ("Knowledge/rootrateq.sml") neuper@41945: (*("Knowledge/polyeq.sml")*) neuper@41945: ("Knowledge/calculus.sml") neuper@41945: ("Knowledge/trig.sml") neuper@41945: ("Knowledge/logexp.sml") neuper@41945: ("Knowledge/diff.sml") neuper@41945: ("Knowledge/integrate.sml") neuper@41945: ("Knowledge/eqsystem.sml") neuper@41945: ("Knowledge/test.sml") neuper@41945: ("Knowledge/polyminus.sml") neuper@41945: ("Knowledge/vect.sml") neuper@41945: ("Knowledge/diffapp.sml") neuper@41945: ("Knowledge/biegelinie.sml") neuper@41945: ("Knowledge/algein.sml") neuper@41945: ("Knowledge/diophanteq.sml") neuper@41945: ("Knowledge/isac.sml") neuper@41945: neuper@41943: begin neuper@41947: neuper@41943: ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*} neuper@41945: use "library.sml" (*new 2011*) neuper@41945: use "calcelems.sml" (*complete*) neuper@41943: use "ProgLang/termC.sml" (*part.*) neuper@41943: use "ProgLang/calculate.sml" (*part.*) neuper@41943: use "ProgLang/rewrite.sml" (*part.*) neuper@41943: (*use "ProgLang/listg.sml" 2002*) neuper@41943: (*use "ProgLang/scrtools.sml" 2002*) neuper@41943: (*use "ProgLang/tools.sml" 2002*) neuper@41943: ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*} neuper@41943: ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*} neuper@41973: ML {* neuper@41973: val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"]; neuper@41973: val (dI',pI',mI') = neuper@41973: ("Test", ["sqroot-test","univariate","equation","test"], neuper@41973: ["Test","squ-equ-test-subpbl1"]); neuper@41973: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; neuper@41973: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41973: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41973: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41973: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41973: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41973: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41973: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41973: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41973: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41973: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41973: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41973: (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: neuper@41973: Tac "[error] appl_add: is_known: identifiers [equality] not in example"*) neuper@41973: (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: applicable_in (p,Pbl) pt (Tac id): not at Pbl*) neuper@41973: show_pt pt; (*WAS ...(([3], Pbl), solve (-1 + x = 0, x))] OK*) neuper@41973: "~~~~~ fun me, args:"; val (_,tac) = nxt; neuper@41973: val (pt, p) = case locatetac tac (pt,p) of neuper@41973: ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac"; neuper@41973: "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), [])) neuper@41973: val pIopt = get_pblID (pt,ip); neuper@41973: tacis; (*= []*) neuper@41973: pIopt; (*= SOME ["sqroot-test", "univariate", ...]*) neuper@41973: member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= true*) neuper@41973: "~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip); neuper@41973: val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_), neuper@41973: probl,spec=(dI,pI,mI),...}) = get_obj I pt p; neuper@41973: just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (*false*) neuper@41973: val cpI = if pI = e_pblID then pI' else pI; neuper@41973: val cmI = if mI = e_metID then mI' else mI; neuper@41973: val {ppc, prls, where_, ...} = get_pbt cpI; neuper@41973: val pre = check_preconds "thy 100820" prls where_ probl; neuper@41973: val pb = foldl and_ (true, map fst pre); neuper@41973: val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth) neuper@41973: (ppc, (#ppc o get_met) cmI) (dI, pI, mI); neuper@41973: "~~~~~ fun nxt_specif, args:"; val (Add_Given ct, ptp) = (tac, ptp); neuper@41973: "~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp); neuper@41973: val (PblObj{meth=met,origin=(oris,(dI',pI',_),_), neuper@41973: probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p; neuper@41973: val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI; neuper@41973: val cpI = if pI = e_pblID then pI' else pI; neuper@41973: val ctxt = get_ctxt pt (p, Pbl); neuper@41973: oris; (*= [(1, [1], "#Given", Const ("Descript.equality", "HOL.bool...*) neuper@41973: "~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) = neuper@41973: (ctxt, sel, oris, pbl, (#ppc o get_pbt) cpI, ct); neuper@41975: *} neuper@41975: ML {* neuper@41975: val t = parseNEW ctxt str; neuper@41975: str; neuper@41975: t; neuper@41975: (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. neuper@41975: if t = parseNEW ctxt "-1 + x = (0::real)" then () neuper@41973: else error "TODO" neuper@41975: -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) neuper@41975: neuper@41973: *} neuper@41975: ML {* neuper@41975: (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. neuper@41975: print_depth 999; applicable_in p pt m; neuper@41975: Model_Problem'; neuper@41975: -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) neuper@41975: *} neuper@41975: use "Interpret/mstools.sml" (*new 2010*) neuper@41975: use "Interpret/ctree.sml" (*!...see(25)*) neuper@41943: use "Interpret/ptyps.sml" (* *) neuper@41943: (*use "Interpret/generate.sml" new 2011*) neuper@41972: use "Interpret/calchead.sml" (*! *) neuper@41975: use "Interpret/appl.sml" (*!complete WEGEN INTERMED TESTCODE*) neuper@41972: use "Interpret/rewtools.sml" (*! *) neuper@41972: use "Interpret/script.sml" (*!TODO*) neuper@41972: (*use "Interpret/solve.sml" !TODO*) neuper@41972: (*use "Interpret/inform.sml" !TODO*) neuper@41972: use "Interpret/mathengine.sml" (*!part.*) neuper@41943: ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*} neuper@41943: ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*} neuper@41943: (*use "xmlsrc/mathml.sml" TODO*) neuper@41943: (*use "xmlsrc/datatypes.sml" TODO*) neuper@41943: (*use "xmlsrc/pbl-met-hierarchy.sml" TODO*) neuper@41943: (*use "xmlsrc/thy-hierarchy.sml" TODO after 2009-2*) neuper@41943: use "xmlsrc/interface-xml.sml" (*TODO after 2009-2*) neuper@41943: ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*} neuper@41943: ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*} neuper@41943: use "Frontend/messages.sml" (*new 2011*) neuper@41943: use "Frontend/states.sml" (*new 2011*) neuper@41945: use "Frontend/interface.sml" (*part.*) neuper@41945: use "print_exn_G.sml" (*new 2011*) neuper@41943: ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*} neuper@41943: ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*} neuper@41943: use "Knowledge/delete.sml" (*new 2011*) neuper@41943: use "Knowledge/descript.sml" (*new 2011*) neuper@41943: (*use "Knowledge/atools.sml" 2002, added termorder.sml 2011*) neuper@41943: use "Knowledge/simplify.sml" (*part.*) neuper@41943: (*use "Knowledge/poly.sml" 2002*) neuper@41947: (*use "Knowledge/rational.sml" part.; diff.emacs--jedit*) neuper@41943: (*use "Knowledge/equation.sml" 2002*) neuper@41943: (*use "Knowledge/root.sml" 2002*) neuper@41943: use "Knowledge/lineq.sml" (*new 2011*) neuper@41943: (*use "Knowledge/rooteq.sml" 2002*) neuper@41943: (*use "Knowledge/rateq.sml" 2002*) neuper@41943: (*use "Knowledge/rootrat.sml" 2002*) neuper@41943: (*use "Knowledge/rootrateq.sml" 2002*) neuper@41943: (*use "Knowledge/polyeq.sml" 2002*) neuper@41956: (*use "Knowledge/rlang.sml" 2002???*) neuper@41943: use "Knowledge/calculus.sml" (*new 2011*) neuper@41943: (*use "Knowledge/trig.sml" 2002*) neuper@41943: (*use "Knowledge/logexp.sml" 2002*) neuper@41943: use "Knowledge/diff.sml" (*part.*) neuper@41947: (*use "Knowledge/integrate.sml" part. was complete 2009-2 neuper@41947: diff.emacs--jedit*) neuper@41943: (*use "Knowledge/eqsystem.sml" 2002*) neuper@41943: use "Knowledge/test.sml" (*new 2011*) neuper@41943: use "Knowledge/polyminus.sml" (*part.*) neuper@41943: (*use "Knowledge/vect.sml" 2002*) neuper@41943: (*use "Knowledge/diffapp.sml" 2002*) neuper@41943: (*use "Knowledge/biegelinie.sml" 2002*) neuper@41943: (*use "Knowledge/algein.sml" 2002*) neuper@41943: use "Knowledge/diophanteq.sml" (*complete*) neuper@41943: use "Knowledge/isac.sml" (*part.*) neuper@41943: ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*} neuper@41945: ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} neuper@41945: ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*} neuper@41945: ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} neuper@41943: neuper@41943: end neuper@41943: neuper@41943: (*=== inhibit exn ?============================================================= neuper@41943: ===== inhibit exn ?===========================================================*) neuper@41943: neuper@41969: (*========== inhibit exn 110503 ================================================ neuper@41943: neuper@41943: "########### testcode inserted vvv ###########################################"; neuper@41943: "########### testcode inserted ^^^ ###########################################"; neuper@41943: neuper@41969: ============ inhibit exn 110503 ==============================================*) neuper@41943: neuper@41943: (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. neuper@41943: -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) neuper@41975: