Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/MathEngBasic/mstools.sml
author wneuper <Walther.Neuper@jku.at>
Sun, 09 Oct 2022 07:44:22 +0200
changeset 60565 f92963a33fe3
parent 60559 aba19e46dd84
child 60583 da7dd260f66e
permissions -rw-r--r--
eliminate term2str in test/* 
     1 (* Title: tests for Interpret/mstools.sml

     2    Author: Walther Neuper 100930, Mathias Lehnfeld

     3    (c) copyright due to lincense terms.

     4 *)

     5 "-----------------------------------------------------------------------------------------------";

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

     7 "-----------------------------------------------------------------------------------------------";

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

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

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

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

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

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

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

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

    16 "-----------------------------------------------------------------------------------------------";

    17 "-----------------------------------------------------------------------------------------------";

    18 "-----------------------------------------------------------------------------------------------";

    19 

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

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

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

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

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

    25 val it = "maximum A" : cterm

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

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

    28 "fixedValues [r = Arbfix]"

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

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

    31 "valuesFor [a]"

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

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

    34 "valuesFor [a, b]"

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

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

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

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

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

    40 "boundVariable a"

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

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

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

    44 

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

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

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

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

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

    50 "solveFor x"

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

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

    53 "errorBound (eps = 0)"

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

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

    56 "solutions L"

    57 

    58 before 6.5.03:

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

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

    61 > Input_Descript.join thy (d,ts);

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

    63 

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

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

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

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

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

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

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

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

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

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

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

    75 *)

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

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

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

    79 (*

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

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

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

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

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

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

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

    87 

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

    89   map getval penv;

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

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

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

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

    94 *)

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

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

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

    98 (*> untouched [];

    99 val it = true : bool

   100 > untouched [I_Model.single_empty];

   101 val it = true : bool

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

   103 val it = false : bool*)

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

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

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

   107 (*

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

   109 pbl_ids ctxt t1 t2;

   110 

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

   112   val (d,argl) = strip_comb t;

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

   114   dest_list (d,argl);

   115   val (_ $ v) = t;

   116   TermC.is_list v;

   117   pbl_ids ctxt d v;

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

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

   120 

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

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

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

   124 

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

   126   pbl_ids ctxt dsc vl;

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

   128    

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

   130 		       "errorBound (eps=#0)";

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

   132   pbl_ids ctxt dsc vl;

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

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

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

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

   137 (* 

   138   val penv = [];

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

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

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

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

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

   144 : (term * term list) list                                                     

   145 

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

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

   148   upd_penv thy penv dsc (id, vl);

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

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

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

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

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

   154 *)

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

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

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

   158 (*

   159   val i = 2;

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

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

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

   163   upd thy envv dsc (id, vl) i;

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

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

   166 

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

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

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

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

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

   172   val met = (#ppc o MethodC.from_store ctxt) mI;

   173 

   174   val envv = [];

   175   val eargs = flat eargs;

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

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

   178 

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

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

   181 

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

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

   184 

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

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

   187 [(1,

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

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

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

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

   192  (2,

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

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

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

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

   197  (3,

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

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

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

   201 

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

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

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

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

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

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

   208 

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

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

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

   212 

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

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

   215 

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

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

   218 

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

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

   221 

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

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