(* Title: tests for Interpret/mstools.sml

   Author: Walther Neuper 100930, Mathias Lehnfeld

   (c) copyright due to lincense terms.

*)

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

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

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

"----------- fun Input_Descript.join -- fun Input_Descript.split -------------------------------";

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

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

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

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

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

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

"----------- fun sub_common for ThyC -----------------------------------------------------------";

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

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

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

"----------- fun Input_Descript.join -- fun Input_Descript.split -------------------------------";

"----------- fun Input_Descript.join -- fun Input_Descript.split -------------------------------";

"----------- fun Input_Descript.join -- fun Input_Descript.split -------------------------------";

(*val t = TermC.parse_test @{context} "maximum A"; 

> val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);

val it = "maximum A" : cterm

> val t = TermC.parse_test @{context} "fixedValues [r=Arbfix]"; 

> val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);

"fixedValues [r = Arbfix]"

> val t = TermC.parse_test @{context} "valuesFor [a]"; 

> val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);

"valuesFor [a]"

> val t = TermC.parse_test @{context} "valuesFor [a,b]"; 

> val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);

"valuesFor [a, b]"

> val t = TermC.parse_test @{context} "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"; 

> val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);

relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]"

> val t = TermC.parse_test @{context} "boundVariable a";

> val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);

"boundVariable a"

> val t = TermC.parse_test @{context} "interval {x::real. 0 <= x & x <= 2*r}"; 

> val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);

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

> val t = TermC.parse_test @{context} "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))"; 

> val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);

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

> val t = TermC.parse_test @{context} "solveFor x"; 

> val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);

"solveFor x"

> val t = TermC.parse_test @{context} "errorBound (eps=0)"; 

> val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);

"errorBound (eps = 0)"

> val t = TermC.parse_test @{context} "solutions L";

> val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);

"solutions L"

before 6.5.03:

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

> val (d,ts) = Input_Descript.split t;

> Input_Descript.join thy (d,ts);

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

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

> val (d,ts) = Input_Descript.split t;

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

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

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

> val (d,ts) = Input_Descript.split t;

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

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

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

> val (d,ts) = Input_Descript.split 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 (TermC.parse thy)) "e_::bool";

  val ev = (Thm.term_of o the o (TermC.parse thy)) "#4 + #3 * x \<up> #2 = #0";

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

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

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

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

  val rv2 = (Thm.term_of o the o (TermC.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 [I_Model.single_empty];

val it = true : bool

> untouched [I_Model.single_empty, (1,[],false,"I_Model.single_empty",Syn "I_Model.single_empty")];

val it = false : bool*)

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

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

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

(*

val t as t1 $ t2 = TermC.parse_test @{context} "antiDerivativeName M_b";

pbl_ids ctxt t1 t2;

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

  val (d,argl) = strip_comb t;

  Input_Descript.is_a d;                      (*see Input_Descript.split*)

  dest_list (d,argl);

  val (_ $ v) = t;

  TermC.is_list v;

  pbl_ids ctxt d v;

[Const (\<^const_name>\<open>Cons\<close>, "[bool, bool List.list] => bool List.list") $

       (Const # $ Free # $ Const (#,#)) $ Const (\<^const_name>\<open>Nil\<close>, "bool List..

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

val dsc = Const (\<^const_name>\<open>Input_Descript.solveFor\<close>, "RealDef.real => Tools.una") : term

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

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

  pbl_ids ctxt dsc vl;

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

  val (dsc,vl) = (Input_Descript.split o Thm.term_of o the o(TermC.parse thy))

		       "errorBound (eps=#0)";

  val (dsc,id) = (split_did o Thm.term_of o the o(TermC.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 (TermC.parse thy)) "solveFor x";

  val (dsc,id) = (split_did o Thm.term_of o the o (TermC.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(TermC.parse thy))"errorBound (eps=#0)";

  val (dsc,id) = (split_did o Thm.term_of o the o(TermC.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(TermC.parse thy))"boundVariable b";

  val (dsc,id) = (split_did o Thm.term_of o the o(TermC.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 MethodC.from_store ctxt) 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 sub_common for ThyC -----------------------------------------------------------";

"----------- fun sub_common for ThyC -----------------------------------------------------------";

"----------- fun sub_common for ThyC -----------------------------------------------------------";

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

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

then () else error "ThyC.sub_common 1";

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

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

then () else error "ThyC.sub_common 2";

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

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

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

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

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

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

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

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