
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: 




