(* Title: tests for Interpret/mstools.sml

   Author: Walther Neuper 100930, Mathias Lehnfeld

   (c) copyright due to lincense terms.

*)

"-----------------------------------------------------------------------------------------------";

"table of contents -----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"----------- go through Model_Problem until nxt_tac --------------------------------------------";

"----------- fun comp_dts -- fun split_dts -----------------------------------------------------";

"----------- type penv -------------------------------------------------------------------------";

"----------- fun untouched ---------------------------------------------------------------------";

"----------- fun pbl_ids -----------------------------------------------------------------------";

"----------- fun upd_penv ----------------------------------------------------------------------";

"----------- fun upd ---------------------------------------------------------------------------";

"----------- fun upds_envv ---------------------------------------------------------------------";

"----------- fun common_subthy -----------------------------------------------------------------";

"--------------------------------------------------------";

"--------------------------------------------------------";

"--------------------------------------------------------";

"--------------------------------------------------------";

"----------- go through Model_Problem until nxt_tac --------------------------------------------";

"----------- go through Model_Problem until nxt_tac --------------------------------------------";

"----------- go through Model_Problem until nxt_tac --------------------------------------------";

(*FIXME.WN110511 delete this test? (goes through "Model_Problem until nxt_tac)*)

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"]);

(*========== inhibit exn AK110725 ================================================

(* ERROR: same as above, see lines 120- 123 *)

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

========== inhibit exn AK110725 ================================================*)

(*========== inhibit exn AK110725 ================================================

(* ERROR: p, nxt, pt not declared due to above error *)

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; (*nxt = ("Subproblem",*)

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

"~~~~~ 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=oldNB*)

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); (*tac = Add_Given "equality (-1 + x = 0)"*)

"~~~~~ 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);

"~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) = (ctxt, sel, oris, pbl, ((#ppc o get_pbt) cpI), ct);

val SOME t = parseNEW ctxt str;

is_known ctxt sel oris t;

"~~~~~ fun is_known, args:"; val (ctxt, sel, ori, t) = (ctxt, sel, oris, t);

val _ = tracing ("RM is_known: t=" ^ term2str t);

val ots = (distinct o flat o (map #5)) (ori:ori list);

val oids = ((map (fst o dest_Free)) o distinct o flat o (map vars)) ots;

val (d, ts) = split_dts t;

"~~~~~ fun split_dts, args:"; val (t as d $ arg) = t;

(*if is_dsc d then () else error "TODO";*)

if is_dsc d then () else error "TODO";

"----- these were the errors (call hierarchy from bottom up)";

appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct;(*WAS

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

nxt_specif_additem "#Given" ct ptp;(*WAS

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

nxt_specif tac ptp;(*WAS

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

nxt_specify_ (pt,ip); (*WAS

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

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

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

========== inhibit exn AK110725 ================================================*)

"----------- fun comp_dts -- fun split_dts -----------------------------------------------------";

"----------- fun comp_dts -- fun split_dts -----------------------------------------------------";

"----------- fun comp_dts -- fun split_dts -----------------------------------------------------";

(*val t = str2term "maximum A"; 

> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);

val it = "maximum A" : cterm

> val t = str2term "fixedValues [r=Arbfix]"; 

> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);

"fixedValues [r = Arbfix]"

> val t = str2term "valuesFor [a]"; 

> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);

"valuesFor [a]"

> val t = str2term "valuesFor [a,b]"; 

> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);

"valuesFor [a, b]"

> val t = str2term "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"; 

> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);

relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"

> val t = str2term "boundVariable a";

> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);

"boundVariable a"

> val t = str2term "interval {x::real. 0 <= x & x <= 2*r}"; 

> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);

"interval {x. 0 <= x & x <= 2 * r}"

> val t = str2term "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))"; 

> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);

"equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"

> val t = str2term "solveFor x"; 

> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);

"solveFor x"

> val t = str2term "errorBound (eps=0)"; 

> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);

"errorBound (eps = 0)"

> val t = str2term "solutions L";

> val (d,ts) = split_dts thy t; comp_dts thy (d,ts);

"solutions L"

before 6.5.03:

> val t = (Thm.term_of o the o (parse thy)) "testdscforlist [#1]";

> val (d,ts) = split_dts t;

> comp_dts thy (d,ts);

val it = "testdscforlist [#1]" : cterm

> val t = (Thm.term_of o the o (parse thy)) "(A::real)";

> val (d,ts) = split_dts t;

val d = Const ("empty","empty") : term

val ts = [Free ("A","RealDef.real")] : term list

> val t = (Thm.term_of o the o (parse thy)) "[R=(R::real)]";

> val (d,ts) = split_dts t;

val d = Const ("empty","empty") : term

val ts = [Const # $ Free # $ Free (#,#)] : term list

> val t = (Thm.term_of o the o (parse thy)) "[#1,#2]";

> val (d,ts) = split_dts t;

val ts = [Free ("#1","'a"),Free ("#2","'a")] : NOT WANTED

*)

"----------- type penv -------------------------------------------------------------------------";

"----------- type penv -------------------------------------------------------------------------";

"----------- type penv -------------------------------------------------------------------------";

(*

  val e_ = (Thm.term_of o the o (parse thy)) "e_::bool";

  val ev = (Thm.term_of o the o (parse thy)) "#4 + #3 * x^^^#2 = #0";

  val v_ = (Thm.term_of o the o (parse thy)) "v_";

  val vv = (Thm.term_of o the o (parse thy)) "x";

  val r_ = (Thm.term_of o the o (parse thy)) "err_::bool";

  val rv1 = (Thm.term_of o the o (parse thy)) "#0";

  val rv2 = (Thm.term_of o the o (parse thy)) "eps";

  val penv = [(e_,[ev]),(v_,[vv]),(r_,[rv2,rv2])]:penv;

  map getval penv;

[(Free ("e_","bool"),

  Const (#,#) $ (# $ # $ (# $ #)) $ Free ("#0","RealDef.real")),

 (Free ("v_","RealDef.real"),Free ("x","RealDef.real")),

 (Free ("err_","bool"),Free ("#0","RealDef.real"))] : (term * term) list      

*)

"----------- fun untouched ---------------------------------------------------------------------";

"----------- fun untouched ---------------------------------------------------------------------";

"----------- fun untouched ---------------------------------------------------------------------";

(*> untouched [];

val it = true : bool

> untouched [e_itm];

val it = true : bool

> untouched [e_itm, (1,[],false,"e_itm",Syn "e_itm")];

val it = false : bool*)

"----------- fun pbl_ids -----------------------------------------------------------------------";

"----------- fun pbl_ids -----------------------------------------------------------------------";

"----------- fun pbl_ids -----------------------------------------------------------------------";

(*

val t as t1 $ t2 = str2term "antiDerivativeName M_b";

pbl_ids ctxt t1 t2;

  val t = (Thm.term_of o the o (parse thy)) "fixedValues [r=Arbfix]";

  val (d,argl) = strip_comb t;

  is_dsc d;                      (*see split_dts*)

  dest_list (d,argl);

  val (_ $ v) = t;

  is_list v;

  pbl_ids ctxt d v;

[Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $

       (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List..

  val (dsc,vl) = (split_dts o Thm.term_of o the o (parse thy)) "solveFor x";

val dsc = Const ("Input_Descript.solveFor","RealDef.real => Tools.una") : term

val vl = Free ("x","RealDef.real") : term 

  val (dsc,id) = (split_did o Thm.term_of o the o (parse thy)) "solveFor v_";

  pbl_ids ctxt dsc vl;

val it = [Free ("x","RealDef.real")] : term list

  val (dsc,vl) = (split_dts o Thm.term_of o the o(parse thy))

		       "errorBound (eps=#0)";

  val (dsc,id) = (split_did o Thm.term_of o the o(parse thy)) "errorBound err_";

  pbl_ids ctxt dsc vl;

val it = [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")] : term list     *)

"----------- fun upd_penv ----------------------------------------------------------------------";

"----------- fun upd_penv ----------------------------------------------------------------------";

"----------- fun upd_penv ----------------------------------------------------------------------";

(* 

  val penv = [];

  val (dsc,vl) = (split_did o Thm.term_of o the o (parse thy)) "solveFor x";

  val (dsc,id) = (split_did o Thm.term_of o the o (parse thy)) "solveFor v_";

  val penv = upd_penv thy penv dsc (id, vl);

[(Free ("v_","RealDef.real"),

  [Const (#,#) $ Free (#,#) $ Free ("#0","RealDef.real")])]

: (term * term list) list                                                     

  val (dsc,vl) = (split_did o Thm.term_of o the o(parse thy))"errorBound (eps=#0)";

  val (dsc,id) = (split_did o Thm.term_of o the o(parse thy))"errorBound err_";

  upd_penv thy penv dsc (id, vl);

[(Free ("v_","RealDef.real"),

  [Const (#,#) $ Free (#,#) $ Free ("#0","RealDef.real")]),

 (Free ("err_","bool"),

  [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")])]

: (term * term list) list    ^.........!!!!

*)

"----------- fun upd ---------------------------------------------------------------------------";

"----------- fun upd ---------------------------------------------------------------------------";

"----------- fun upd ---------------------------------------------------------------------------";

(*

  val i = 2;

  val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv;

  val (dsc,vl) = (split_did o Thm.term_of o the o(parse thy))"boundVariable b";

  val (dsc,id) = (split_did o Thm.term_of o the o(parse thy))"boundVariable v_";

  upd thy envv dsc (id, vl) i;

val it = (2,[(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")])])

  : int * (term * term list) list*)

"----------- fun upds_envv ---------------------------------------------------------------------";

"----------- fun upds_envv ---------------------------------------------------------------------";

"----------- fun upds_envv ---------------------------------------------------------------------";

(* eval test-maximum.sml until Specify_Method ...

  val PblObj{probl=(_,pbl),origin=(_,(_,_,mI),_),...} = get_obj I pt [];

  val met = (#ppc o get_met) mI;

  val envv = [];

  val eargs = flat eargs;

  val (vs, dsc, id, vl) = hd eargs;

  val envv = upds_envv thy envv [(vs, dsc, id, vl)];

  val (vs, dsc, id, vl) = hd (tl eargs);

  val envv = upds_envv thy envv [(vs, dsc, id, vl)];

  val (vs, dsc, id, vl) = hd (tl (tl eargs));

  val envv = upds_envv thy envv [(vs, dsc, id, vl)];

  val (vs, dsc, id, vl) = hd (tl (tl (tl eargs)));

  val envv = upds_envv thy envv [(vs, dsc, id, vl)];

[(1,

  [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),

   (Free ("m_","bool"),[Free (#,#)]),

   (Free ("vs_","bool List.list"),[# $ # $ Const #]),

   (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]),

 (2,

  [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),

   (Free ("m_","bool"),[Free (#,#)]),

   (Free ("vs_","bool List.list"),[# $ # $ Const #]),

   (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]),

 (3,

  [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),

   (Free ("m_","bool"),[Free (#,#)]),

   (Free ("vs_","bool List.list"),[# $ # $ Const #])])] : envv *)

"----------- fun common_subthy -----------------------------------------------------------------";

"----------- fun common_subthy -----------------------------------------------------------------";

"----------- fun common_subthy -----------------------------------------------------------------";

val (thy1, thy2) = (@{theory Partial_Fractions}, @{theory Inverse_Z_Transform});

if Context.theory_name (common_subthy (thy1, thy2)) = "Inverse_Z_Transform"

then () else error "common_subthy 1";

val (thy1, thy2) = (@{theory Inverse_Z_Transform}, @{theory Partial_Fractions});(* Isac.Inverse_Z_Transform *)

if Context.theory_name (common_subthy (thy1, thy2)) = "Inverse_Z_Transform"

then () else error "common_subthy 2";

val (thy1, thy2) = (@{theory Partial_Fractions}, @{theory PolyEq});

if Context.theory_name (common_subthy (thy1, thy2)) = "Isac_Knowledge" then () else error "common_subthy 3";

val (thy1, thy2) = (@{theory Partial_Fractions}, @{theory Isac_Knowledge});

if Context.theory_name (common_subthy (thy1, thy2)) = "Isac_Knowledge" then () else error "common_subthy 4";

val (thy1, thy2) = (@{theory PolyEq}, @{theory Partial_Fractions});

if Context.theory_name (common_subthy (thy1, thy2)) = "Isac_Knowledge" then () else error "common_subthy 5";

val (thy1, thy2) = (@{theory Isac_Knowledge}, @{theory Partial_Fractions});

if Context.theory_name (common_subthy (thy1, thy2)) = "Isac_Knowledge" then () else error "common_subthy 6";