(* Title:  All tests on isac; observe outcommented

   Author: Walther Neuper 101001

   (c) copyright due to lincense terms.

$ cd /usr/local/isabisac/test/Tools/isac

$ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy &

1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890

        10        20        30        40        50        60        70        80         90      100

*)

theory Test_Isac imports Isac

uses 

  (         "library.sml")

  (         "calcelems.sml")

  ("ProgLang/termC.sml") 

  ("ProgLang/calculate.sml")

  ("ProgLang/rewrite.sml")

(*("ProgLang/listg.sml") ("ProgLang/scrtools.sml") ("ProgLang/tools.sml") *)

  ("Interpret/mstools.sml") 

  ("Interpret/ctree.sml")

  ("Interpret/ptyps.sml") 

(*("Interpret/generate.sml")*)

  ("Interpret/calchead.sml") 

(*("Interpret/appl.sml")*)

  ("Interpret/rewtools.sml") 

(*("Interpret/script.sml")

  ("Interpret/solve.sml") 

  ("Interpret/inform.sml")*)

  ("Interpret/mathengine.sml")

(*("xmlsrc/mathml.sml")

  ("xmlsrc/datatypes.sml")

  ("xmlsrc/pbl-met-hierarchy.sml")

  ("xmlsrc/thy-hierarchy.sml")*)

  ("xmlsrc/interface-xml.sml")

  ("Frontend/messages.sml")

  ("Frontend/states.sml")

  ("Frontend/interface.sml")

  ("print_exn_G.sml")

  ("Knowledge/delete.sml")

  ("Knowledge/descript.sml")

  ("Knowledge/atools.sml")

  ("Knowledge/simplify.sml")

  ("Knowledge/poly.sml")

  ("Knowledge/rational.sml")

  ("Knowledge/equation.sml")

  ("Knowledge/root.sml")

  ("Knowledge/lineq.sml")

  ("Knowledge/rooteq.sml")

  ("Knowledge/rateq.sml")

  ("Knowledge/rootrateq.sml")

(*("Knowledge/polyeq.sml")*)

  ("Knowledge/calculus.sml")

  ("Knowledge/trig.sml")

  ("Knowledge/logexp.sml")

  ("Knowledge/diff.sml")

  ("Knowledge/integrate.sml")

  ("Knowledge/eqsystem.sml")

  ("Knowledge/test.sml")

  ("Knowledge/polyminus.sml")

  ("Knowledge/vect.sml")

  ("Knowledge/diffapp.sml")

  ("Knowledge/biegelinie.sml")

  ("Knowledge/algein.sml")

  ("Knowledge/diophanteq.sml")

  ("Knowledge/isac.sml")

begin

  ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}

  use          "library.sml"        (*new 2011*)

  use          "calcelems.sml"      (*complete*)

  use "ProgLang/termC.sml"          (*part.*)

  use "ProgLang/calculate.sml"      (*part.*)

  use "ProgLang/rewrite.sml"        (*part.*)

(*use "ProgLang/listg.sml"            2002*)

(*use "ProgLang/scrtools.sml"         2002*)

(*use "ProgLang/tools.sml"            2002*)

  ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}

  ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}

ML {*

val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];

val (dI',pI',mI') =

  ("Test", ["sqroot-test","univariate","equation","test"],

   ["Test","squ-equ-test-subpbl1"]);

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: 

       Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)

(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: applicable_in (p,Pbl) pt (Tac id): not at Pbl*)

show_pt pt; (*WAS ...(([3], Pbl), solve (-1 + x = 0, x))] OK*)

"~~~~~ fun me, args:"; val (_,tac) = nxt;

val (pt, p) = case locatetac tac (pt,p) of

	("ok", (_, _, ptp))  => ptp | _ => error "script.sml locatetac";

"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))

val pIopt = get_pblID (pt,ip);

tacis; (*= []*)

pIopt; (*= SOME ["sqroot-test", "univariate", ...]*)

member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= true*)

"~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);

val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),

			  probl,spec=(dI,pI,mI),...}) = get_obj I pt p;

just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (*false*)

val cpI = if pI = e_pblID then pI' else pI;

		val cmI = if mI = e_metID then mI' else mI;

		val {ppc, prls, where_, ...} = get_pbt cpI;

		val pre = check_preconds "thy 100820" prls where_ probl;

		val pb = foldl and_ (true, map fst pre);

val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth) 

			  (ppc, (#ppc o get_met) cmI) (dI, pI, mI);

"~~~~~ fun nxt_specif, args:"; val (Add_Given ct, ptp) = (tac, ptp);

"~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp);

val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),

		  probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;

val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;

val cpI = if pI = e_pblID then pI' else pI;

val ctxt = get_ctxt pt (p, Pbl);

oris; (*= [(1, [1], "#Given", Const ("Descript.equality", "HOL.bool...*)

"~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) = 

                               (ctxt, sel, oris, pbl, (#ppc o get_pbt) cpI, ct);

*}

ML {*

val t = parseNEW ctxt str;

str;

t;

(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

if t = parseNEW ctxt "-1 + x = (0::real)" then ()

else error "TODO"

-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)

*}

ML {*

(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

print_depth 999; applicable_in p pt m;

Model_Problem';

-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)

*}

  use "Interpret/mstools.sml"       (*new 2010*)

  use "Interpret/ctree.sml"         (*!...see(25)*)

  use "Interpret/ptyps.sml"         (*    *)

(*use "Interpret/generate.sml"        new 2011*)

  use "Interpret/calchead.sml"      (*!    *)

  use "Interpret/appl.sml"          (*!complete WEGEN INTERMED TESTCODE*)

  use "Interpret/rewtools.sml"      (*!    *)

  use "Interpret/script.sml"        (*!TODO*)

(*use "Interpret/solve.sml"           !TODO*)

(*use "Interpret/inform.sml"          !TODO*)

  use "Interpret/mathengine.sml"    (*!part.*)

  ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}

  ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}

(*use "xmlsrc/mathml.sml"             TODO*)

(*use "xmlsrc/datatypes.sml"          TODO*)

(*use "xmlsrc/pbl-met-hierarchy.sml"  TODO*)

(*use "xmlsrc/thy-hierarchy.sml"      TODO after 2009-2*) 

  use "xmlsrc/interface-xml.sml"    (*TODO after 2009-2*)

  ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}

  ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}

  use "Frontend/messages.sml"        (*new 2011*)

  use "Frontend/states.sml"          (*new 2011*)

  use "Frontend/interface.sml"       (*part.*)                            

  use         "print_exn_G.sml"      (*new 2011*)

  ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}

  ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}

  use "Knowledge/delete.sml"         (*new 2011*)

  use "Knowledge/descript.sml"       (*new 2011*)

(*use "Knowledge/atools.sml"           2002, added termorder.sml 2011*)

  use "Knowledge/simplify.sml"       (*part.*)

(*use "Knowledge/poly.sml"             2002*)

(*use "Knowledge/rational.sml"         part.; diff.emacs--jedit*)

(*use "Knowledge/equation.sml"         2002*)

(*use "Knowledge/root.sml"             2002*)

  use "Knowledge/lineq.sml"          (*new 2011*)

(*use "Knowledge/rooteq.sml"           2002*)

(*use "Knowledge/rateq.sml"            2002*)

(*use "Knowledge/rootrat.sml"          2002*)

(*use "Knowledge/rootrateq.sml"        2002*)

(*use "Knowledge/polyeq.sml"           2002*)

(*use "Knowledge/rlang.sml"            2002???*)

  use "Knowledge/calculus.sml"       (*new 2011*)

(*use "Knowledge/trig.sml"             2002*)

(*use "Knowledge/logexp.sml"           2002*)

  use "Knowledge/diff.sml"           (*part.*)

(*use "Knowledge/integrate.sml"        part. was complete 2009-2

                                              diff.emacs--jedit*)

(*use "Knowledge/eqsystem.sml"         2002*)

  use "Knowledge/test.sml"           (*new 2011*)

  use "Knowledge/polyminus.sml"      (*part.*)

(*use "Knowledge/vect.sml"             2002*)

(*use "Knowledge/diffapp.sml"          2002*)

(*use "Knowledge/biegelinie.sml"       2002*)

(*use "Knowledge/algein.sml"           2002*)

  use "Knowledge/diophanteq.sml"     (*complete*)

  use "Knowledge/isac.sml"           (*part.*)

  ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*}

  ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}

  ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*}

  ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}

end

(*=== inhibit exn ?=============================================================

===== inhibit exn ?===========================================================*)

(*========== inhibit exn 110503 ================================================

"########### testcode inserted vvv ###########################################";

"########### testcode inserted ^^^ ###########################################";

============ inhibit exn 110503 ==============================================*)

(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)