wneuper/isa: test/Tools/isac/Test

     2 theory Test_Some imports Isac begin

     4 use"../../../test/Tools/isac/Interpret/inform.sml"

     6 ML {*

     7 val thy = @{theory "Isac"};

     8 val ctxt = ProofContext.init_global thy;

     9 print_depth 5;

    10 *}

    11 ML {*

    12 *}

    13 ML {* (*================== --> test/../inform.sml*)

    14 "--------- UC errpat, fillpat ---------------------------"; (*--> test/../interface.sml*)

    15 "--------- embed fun get_fillform --------------------------------"; (*--> test/../inform.sml*)

    16 states := [];

    17 CalcTree

    18 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],

    19   ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];

    20 Iterator 1;

    21 moveActiveRoot 1;

    22 autoCalculate 1 CompleteCalcHead;

    23 autoCalculate 1 (Step 1);

    24 autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)

    25 appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)";

    26 (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),

    27   would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.

    28   results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>

    29   instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)

    30 FindFillpatterns 1 "chain-rule-diff-both";

    31 (*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =

    32   d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)

    33 *}

    34 ML {*

    35 requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");

    36 *}

    37 ML {*

    38 *}

    39 ML {*

    40 *}

    41 ML {*

    42 *}

    43 ML {* (*==================*)

    44 *}

    45 ML {*

    46 *}

    47 ML {* (*==================*)

    48 "~~~~~ fun , args:"; val () = ();

    49 "~~~~~ to  return val:"; val () = ();

    51 *}

    52 text {**}

    53 ML {*

    55 *}

    56 end

    58 (*============ inhibit exn WN120406 ==============================================

    59 ============ inhibit exn WN120406 ==============================================*)

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

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

    64 (*=========================^^^ correct until here ^^^===========================*)

author	Walther Neuper <neuper@ist.tugraz.at>
	Tue, 22 May 2012 13:40:06 +0200
changeset 42432	7dc25d1526a5
parent 42430	5b629bb1c073
child 42433	ed0ff27b6165
permissions	-rw-r--r--