wneuper/isa: test/Tools/isac/Interpret/mathengine.sml@0af380e9bed0

     1 (* test for sml/ME/mathengine.sml

     2    authors: Walther Neuper 2000, 2006

     3    (c) due to copyright terms

     4 *)

     5 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

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

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

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

    10 "----------- change to parse ctxt -----------------------";

    11 "----------- debugging setContext..pbl_ -----------------";

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

    13 "----------- fun step -----------------------------------";

    14 "----------- fun autocalc -------------------------------";

    15 "----------- fun autoCalculate --------------------------";

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

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

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

    20 "----------- change to parse ctxt -----------------------";

    21 "----------- change to parse ctxt -----------------------";

    22 "----------- change to parse ctxt -----------------------";

    23 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)

    24 "===== start calculation: from problem description (fmz) to origin";

    25 val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];

    26 val (thyID, pblID, metID) =

    27   ("Test", ["calculate", "test"], ["Test", "test_calculate"]);

    28 val (p,_,_,nxt,_,pt) = CalcTreeTEST [(fmz, (thyID, pblID, metID))];

    29 "----- ";

    30 (* call sequence: CalcTreeTEST

    31                 > nxt_specify_init_calc

    32                 > prep_ori

    33 *)

    34 val (thy, pbt) = (Thy_Info.get_theory thyID, (#ppc o get_pbt) pblID);

    35 "----- in  prep_ori";

    36 val ctxt = ProofContext.init_global thy;

    38     val ctopts = map (parse thy) fmz;

    39     val dts = map ((split_dts thy) o term_of o the) ctopts;

    40 (*split_dts:

    41 (term * term list) list

    42         formulas: e.g. ((1+2)*4/3)^^^2

    43  description: e.g. realTestGiven

    44 *)

    45  prep_ori;

    46 (* FROM

    47 val it = fn:

    48    string list -> theory -> (string * (term * 'a)) list -> ori list

    49 TO

    50 val it = fn:

    51    string list -> theory -> (string * (term * 'a)) list -> (ori list * ctxt)

    52 AND

    53 FROM val oris = prep_ori...

    54 TO   val (oris, _) = prep_ori...

    55 *)

    56 "----- insert ctxt in ptree";

    57 (* datatype ppobj

    58 FROM loc   : istate option * istate option,

    59 TO   loc   : (istate * ctxt) option * (istate * ctxt) option,

    60 e.g.

    61 FROM val pt = Nd (PblObj

    62        {.., loc = (SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)),

    63           NONE),

    64 TO   val pt = Nd (PblObj

    65        {.., loc =

    66         ((SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)), ctxt),

    67           NONE),

    68 *)

    70 "===== interactive specification: from origin to specification (probl)";

    71 val (p,_,_,nxt,_,pt) = me nxt p [1] pt;

    72   (*nxt =("Add_Given", Model_Problem)*)

    73 val (p,_,_,nxt,_,pt) = me nxt p [1] pt;

    74   (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)

    75 "----- ";

    76 (* call sequence: me Model_Problem

    77                 > me ("Add_Given", Add_Given "realTestGiven (((1 + 2) * 4 / 3) ^^^ 2)")

    78                 > locatetac tac

    79                 > loc_specify_

    80                 > specify          GET ctxt (stored in ctree)

    81                 > specify_additem

    82                 > appl_add

    84 *)

    85 "----- in appl_add";

    86 (* FROM appl_add thy

    87    TO   appl_add ctxt

    88    FROM parse thy str

    89    TO   parseNEW ctxt str

    90 *)

    91 val (p,_,_,nxt,_,pt) = me nxt p [1] pt;

    92   (*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)

    93 val (p,_,_,nxt,_,pt) = me nxt p [1] pt;

    94   (*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)

    96 "===== end specify: from specification (probl) to guard (method)";

    97 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

    98   (*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*)

   100 "===== start interpretation: from guard to environment";

   101 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   102   (*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*)

   103 "----- ";

   104 (* call sequence: me ("Apply_Method",...

   105                 > locatetac

   106                 > loc_solve_

   107                 > solve ("Apply_Method",...

   108 *)

   109 val ((_,tac), ptp) = (nxt, (pt, p));

   110 locatetac tac (pt,p);

   111   val (mI, m) = mk_tac'_ tac;

   112   val Appl m = applicable_in p pt m;

   113   member op = specsteps mI;

   114   loc_solve_ (mI,m) ptp;

   115     val (m, (pt, pos)) = ((mI,m), ptp);

   116     solve m (pt, pos);

   117       val ((_, m as Apply_Method' (mI, _, _)), (pt, (pos as (p,_)))) =

   118         (m, (pt, pos));

   119       val {srls,...} = get_met mI;

   120       val PblObj{meth=itms,...} = get_obj I pt p;

   121       val thy' = get_obj g_domID pt p;

   122       val thy = assoc_thy thy';

   123       val (is as ScrState (env,_,_,_,_,_), sc) = init_scrstate thy itms mI;

   125 "----- go on in the calculation";

   126 val (p,_,f,nxt,_,pt) = me nxt pos [1] pt;

   127   (*nxt = ("Calculate",Calculate "PLUS")*)

   128 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   129   (*nxt = ("Calculate",Calculate "TIMES")*)

   131 "===== input a formula to be derived from previous istate";

   132 "----- appendFormula TODO: first repair error";

   133   val cs = ((pt,p),[]);

   134   val ("ok", cs' as (_,_,(pt,p))) = step p cs;

   135   val ifo = (* encode "4^^^2" \<longrightarrow>*) "4^2"; val encode = I;

   136 (*

   137   val ("no derivation found", (_,_,(pt, p))) = inform cs' (encode ifo);

   138   here ^^^^^^^^^^^^^^^^^^^^^ should be "ok"

   139 *)

   141 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   142 (*nxt = ("Calculate",Calculate "DIVIDE")*)

   143 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   144 (*nxt = ("Calculate",Calculate "POWER")*)

   145 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   146 (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)

   147 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   148 (*nxt = ("End_Proof'",End_Proof')*)

   149 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then ()

   150 else error "calculate.sml: script test_calculate changed behaviour";

   152 "===== tactic Subproblem: from environment to origin";

   153 "----- TODO";

   157 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

   159 (*=== inhibit exn ?=============================================================

   161 "----------- debugging setContext..pbl_ -----------------";

   162 "----------- debugging setContext..pbl_ -----------------";

   163 "----------- debugging setContext..pbl_ -----------------";

   164 states:=[];

   165 CalcTree

   166 [(["equality (x+1=2)", "solveFor x","solutions L"],

   167   ("Test",

   168    ["sqroot-test","univariate","equation","test"],

   169    ["Test","squ-equ-test-subpbl1"]))];

   170 Iterator 1;

   171 moveActiveRoot 1; modelProblem 1;

   173 val pos as (p,_) = ([],Pbl);

   174 val guh = "pbl_equ_univ";

   175 checkContext 1 pos guh;

   176 val ((pt,_),_) = get_calc 1;

   177 val pp = par_pblobj pt p;

   178 val keID = guh2kestoreID guh;

   179 case context_pbl keID pt pp of (true,["univariate", "equation"],_,_,_)=>()

   180 | _ => error "mathengine.sml: context_pbl .. pbl_equ_univ checked";

   182 case get_obj g_spec pt p of (_, ["e_pblID"], _) => ()

   183 | _ => error "mathengine.sml: context_pbl .. pbl still empty";

   184 setContext 1 pos guh;

   185 val ((pt,_),_) = get_calc 1;

   186 case get_obj g_spec pt p of (_, ["univariate", "equation"], _) => ()

   187 | _ => error "mathengine.sml: context_pbl .. pbl set";

   190 setContext 1 pos "met_eq_lin";

   191 val ((pt,_),_) = get_calc 1;

   192 case get_obj g_spec pt p of (_,  _, ["LinEq", "solve_lineq_equation"]) => ()

   193 | _ => error "mathengine.sml: context_pbl .. pbl set";

   196 "----------- tryrefine ----------------------------------";

   197 "----------- tryrefine ----------------------------------";

   198 "----------- tryrefine ----------------------------------";

   199 states:=[];

   200 CalcTree [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",

   201 	    "solveFor x", "solutions L"],

   202 	   ("RatEq",["univariate","equation"],["no_met"]))];

   203 Iterator 1;

   204 moveActiveRoot 1; autoCalculate 1 CompleteCalc;

   206 refineProblem 1 ([1],Res) "pbl_equ_univ"

   207 (*gives "pbl_equ_univ_rat" correct*);

   209 refineProblem 1 ([1],Res) (pblID2guh ["linear","univariate","equation"])

   210 (*gives "pbl_equ_univ_lin" incorrect*);

   212 ===== inhibit exn ?===========================================================*)

   215 "----------- fun step -----------------------------------";

   216 "----------- fun step -----------------------------------";

   217 "----------- fun step -----------------------------------";

   218 val p = e_pos'; val c = [];

   219 val (p,_,f,nxt,_,pt) =

   220     CalcTreeTEST

   221         [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],

   222           ("Integrate", ["integrate","function"], ["diff","integration"]))];

   223 "----- step 1: returns tac = Model_Problem ---";

   224 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);

   225 "----- step 2: returns tac =  ---";

   226 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);

   227 "----- step 3: returns tac =  ---";

   228 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);

   229 "----- step 4: returns tac =  ---";

   230 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);

   231 "----- step 5: returns tac =  ---";

   233 (*========== inhibit exn =======================================================

   234 2002 stops here as well: TODO review actual arguments:

   235 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);

   236 "----- step 6: returns tac =  ---";

   237 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);

   238 "----- step 7: returns tac =  ---";

   239 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);

   240 "----- step 8: returns tac =  ---";

   241 val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);

   242 ============ inhibit exn =====================================================*)

   245 "----------- fun autocalc -------------------------------";

   246 "----------- fun autocalc -------------------------------";

   247 "----------- fun autocalc -------------------------------";

   248 val p = e_pos'; val c = [];

   249 val (p,_,f,nxt,_,pt) =

   250     CalcTreeTEST

   251         [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],

   252           ("Integrate",["integrate","function"], ["diff","integration"]))];

   253 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*

   254 modeling is skipped FIXME

   255  *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)

   256 tracing "----- step 1 ---";

   257 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;

   258 tracing "----- step 2 ---";

   259 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;

   260 tracing "----- step 3 ---";

   261 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;

   262 tracing "----- step 4 ---";

   263 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;

   264 tracing "----- step 5 ---";

   265 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;

   266 tracing "----- step 6 ---";

   267 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;

   268 tracing "----- step 7 ---";

   269 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;

   270 tracing "----- step 8 ---";

   271 val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;

   272 (*========== inhibit exn 110310 ================================================

   273 if str = "end-of-calculation" andalso

   274    term2str (get_obj g_res pt (fst p)) = "c + x + 1 / 3 * x ^^^ 3" then ()

   275 else error "mathengine.sml -- fun autocalc -- end";

   276 ============ inhibit exn =====================================================*)

   279 "----------- fun autoCalculate -----------------------------------";

   280 "----------- fun autoCalculate -----------------------------------";

   281 "----------- fun autoCalculate -----------------------------------";

   282 states := [];

   283 CalcTree (*ATTENTION: encode_fmz ... unlike CalcTreeTEST*)

   284     [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],

   285       ("Integrate", ["integrate", "function"], ["diff", "integration"]))];

   286 Iterator 1;

   287 moveActiveRoot 1;

   288 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*

   289 modeling is skipped FIXME

   290 see test/../interface -- solve_linear as rootpbl FE -- for OTHER expl:

   291  setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");

   292  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);

   294  fetchProposedTactic 1;

   295  setNextTactic 1 (Add_Given "solveFor x");

   296  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

   298  fetchProposedTactic 1;

   299  setNextTactic 1 (Add_Find "solutions L");

   300  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

   302  fetchProposedTactic 1;

   303  setNextTactic 1 (Specify_Theory "Test");

   304  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);

   305 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)

   306 autoCalculate 1 (Step 1);

   307 "----- step 1 ---";

   308 autoCalculate 1 (Step 1);

   309 "----- step 2 ---";

   310 autoCalculate 1 (Step 1);

   311 "----- step 3 ---";

   312 autoCalculate 1 (Step 1);

   313 "----- step 4 ---";

   314 autoCalculate 1 (Step 1);

   315 "----- step 5 ---";

   316 autoCalculate 1 (Step 1);

   317 "----- step 6 ---";

   318 autoCalculate 1 (Step 1);

   319 "----- step 7 ---";

   320 autoCalculate 1 (Step 1);

   321 "----- step 8 ---";

   322 autoCalculate 1 (Step 1);

   323 val (ptp as (_, p), _) = get_calc 1;

   324 val (Form t,_,_) = pt_extract ptp;

   325 (*========== inhibit exn 110310 ================================================

   326 if term2str t = "c + x + 1 / 3 * x ^^^ 3" andalso p = ([], Res) then ()

   327 else error "mathengine.sml -- fun autoCalculate -- end";

   328 ============ inhibit exn =====================================================*)

   330 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)

author	Walther Neuper <neuper@ist.tugraz.at>
	Sat, 19 Mar 2011 15:03:36 +0100
branch	decompose-isar
changeset 41940	0af380e9bed0
parent 41929	e4b645e5f25b
child 41943	f33f6959948b
child 41949	c1859b72ae8d
permissions	-rw-r--r--