wneuper/isa: test/Tools/isac/MathEngBasic/mstools.sml@78a78f428ef8

     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 "----------- fun untouched ---------------------------------------------------------------------";

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

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

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

    13 "-----------------------------------------------------------------------------------------------";

    14 "-----------------------------------------------------------------------------------------------";

    15 "-----------------------------------------------------------------------------------------------";

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

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

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

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

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

    22 val it = "maximum A" : cterm

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

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

    25 "fixedValues [r = Arbfix]"

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

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

    28 "valuesFor [a]"

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

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

    31 "valuesFor [a, b]"

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

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

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

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

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

    37 "boundVariable a"

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

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

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

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

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

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

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

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

    47 "solveFor x"

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

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

    50 "errorBound (eps = 0)"

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

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

    53 "solutions L"

    55 before 6.5.03:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    72 *)

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

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

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

    77 (*> untouched [];

    78 val it = true : bool

    79 > untouched [I_Model.single_empty];

    80 val it = true : bool

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

    82 val it = false : bool*)

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

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

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

    86 (*

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

    88 pbl_ids ctxt t1 t2;

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

    91   val (d,argl) = strip_comb t;

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

    93   dest_list (d,argl);

    94   val (_ $ v) = t;

    95   TermC.is_list v;

    96   pbl_ids ctxt d v;

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

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

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

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

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

   104   val (dsc,id) = ((Model_Pattern.split_descriptor ctxt)  o Thm.term_of o the o (TermC.parse thy)) "solveFor v_";

   105   pbl_ids ctxt dsc vl;

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

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

   109 		       "errorBound (eps=#0)";

   110   val (dsc,id) = ((Model_Pattern.split_descriptor ctxt)  o Thm.term_of o the o(TermC.parse thy)) "errorBound err_";

   111   pbl_ids ctxt dsc vl;

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

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

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

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

   117 (*

   118   val i = 2;

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

   120   val (dsc,vl) = ((Model_Pattern.split_descriptor ctxt)  o Thm.term_of o the o(TermC.parse thy))"boundVariable b";

   121   val (dsc,id) = ((Model_Pattern.split_descriptor ctxt)  o Thm.term_of o the o(TermC.parse thy))"boundVariable v_";

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

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

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

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

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

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

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

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

   131   val met = (#model o MethodC.from_store ctxt) mI;

   133   val envv = [];

   134   val eargs = flat eargs;

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

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

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

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

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

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

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

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

   146 [(1,

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

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

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

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

   151  (2,

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

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

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

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

   156  (3,

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

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

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

author	wneuper <Walther.Neuper@jku.at>
	Sun, 27 Aug 2023 11:19:14 +0200
changeset 60739	78a78f428ef8
parent 60660	c4b24621077e
permissions	-rw-r--r--