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/Interpret/step-solve.sml
author wneuper <Walther.Neuper@jku.at>
Sat, 04 Feb 2023 17:00:25 +0100
changeset 60675 d841c720d288
parent 60665 fad0cbfb586d
permissions -rw-r--r--
eliminate use of Thy_Info 22: eliminate UnparseC.term, rename "_in_ctxt" -> "" 
     1 (* Title:  "Interpret/step-solve.sml"

     2    Author: Walther Neuper

     3    (c) due to copyright terms

     4 *)

     5 

     6 "-----------------------------------------------------------------------------------------------";

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

     8 "-----------------------------------------------------------------------------------------------";

     9 "-----------------------------------------------------------------------------------------------";

    10 "----------- Apply_Method with explicit Take by fun me (from integrate) ------------------------";

    11 "-----------------------------------------------------------------------------------------------";

    12 "-----------------------------------------------------------------------------------------------";

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

    14 

    15 "----------- Apply_Method with explicit Take by fun me (from integrate) ------------------------";

    16 "----------- Apply_Method with explicit Take by fun me (from integrate) ------------------------";

    17 "----------- Apply_Method with explicit Take by fun me (from integrate) ------------------------";

    18 (*cp fom..*)

    19 "----------- me method [diff,integration] ---------------";

    20 val fmz = ["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"];

    21 val spec = ("Integrate", ["integrate", "function"], ["diff", "integration"]);

    22 (*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, spec)];(*\<rightarrow>Model_Problem*)

    23 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Add_Given "functionTerm (x \<up> 2 + 1)"*)

    24 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Add_Given "integrateBy x"*)

    25 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Add_Find "Integrate.antiDerivative FF"*)

    26 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Specify_Theory "Integrate"*)

    27 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Specify_Problem ["integrate", "function"]*)

    28 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Specify_Method ["diff", "integration"]*)

    29 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Apply_Method ["diff", "integration"]*)

    30 

    31 (*+*)case nxt of (Apply_Method ["diff", "integration"]) => ()

    32 (*+*)          | _ => error "integrate.sml -- me method [diff,integration] -- spec";

    33 

    34 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Rewrite_Set_Inst (["(''bdv'', x)"], "integration")*)

    35 (*/--------- step into Apply_Method ----------------------------------------------------------\*)

    36 (*\--------- step into Apply_Method ----------------------------------------------------------/*)

    37 

    38 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Check_Postcond ["integrate", "function"]*)

    39 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>End_Proof'*)

    40 

    41 (*/--------- final test ----------------------------------------------------------------------\*)

    42 val (res, asm) = (get_obj g_result pt (fst p));

    43 if UnparseC.term @{context} res = "c + x + 1 / 3 * x \<up> 3" then ()

    44 else error "Apply_Method with explicit Take CHANGED";
wneuper/isa