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/Minisubpbl/790-complete-NEXT_STEP.sml
author wneuper <Walther.Neuper@jku.at>
Tue, 16 Aug 2022 15:53:20 +0200
changeset 60529 a823f87dd5aa
parent 60242 73ee61385493
child 60533 b840894bd75a
permissions -rw-r--r--
prepare test 2 for: push ctxt through LI 
     1 (* Title:  "Minisubpbl/790-complete-NEXT_STEP.sml"

     2    Author: Walther Neuper 1105

     3    (c) copyright due to lincense terms.

     4 *)

     5 

     6 "----------- Minisubpbl/790-complete-NEXT_STEP.sml --------------------------------------------";

     7 "----------- Minisubpbl/790-complete-NEXT_STEP.sml --------------------------------------------";

     8 "----------- Minisubpbl/790-complete-NEXT_STEP.sml --------------------------------------------";

     9 

    10 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];

    11 val (dI',pI',mI') =

    12   ("Test", ["sqroot-test", "univariate", "equation", "test"],

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

    14 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

    15 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Model_Problem*)

    16 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Specify_Theory*)

    17 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Specify_Problem ["sqroot-test", "univariate", "equation", "test"*)

    18 (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Specify_Method ["Test", "squ-equ-test-subpbl1"]*)

    19 (*1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Apply_Method ["Test", "squ-equ-test-subpbl1"]*)

    20 (*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Rewrite_Set "norm_equation"*)

    21 (*[2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Rewrite_Set "Test_simplify"*)

    22 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)

    23 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Model_Problem*)

    24 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Specify_Theory "Test"*)

    25 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)

    26 (*[3], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Specify_Method ["Test", "solve_linear"]*)

    27 (*[3, 1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Apply_Method ["Test", "solve_linear"]*)

    28 (*[3, 1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)

    29 (*[3, 2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Rewrite_Set "Test_simplify"*)

    30 (*[3], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)

    31 

    32 ((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms) = "[]";(*isa*)

    33 ((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms) = "[\"matches (?a = ?b) (-1 + x = 0)\"]";(*REP*)

    34 (* there are questionable assumptions either --------- \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up>  \<up> ^^*)

    35 

    36 (*[4], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Check_elementwise "Assumptions"*)

    37 

    38 ((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms) = "[]";(*isa*)

    39 ((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms) = "[\"precond_rootmet 1\"]";(*REP*)

    40 

    41 (*[], Res*)val ("ok", ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)

    42 

    43 ((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms) = "[]";(*isa*)

    44 ((get_obj g_result pt (fst p)) |> snd |> UnparseC.terms) = "[\"precond_rootmet 1\"]";(*REP*)

    45 

    46 (*[], Res*)val ("end-of-calculation", ([], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(**)

    47 

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

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

    50 

    51 if UnparseC.term res = "[x = 1]" andalso

    52   map UnparseC.term asm = []    (* assumptions have gone to the ctxt *)

    53 then () else error "Minisubpbl/790-complete-NEXT_STEP.sml, find_next_step CHANGED";

    54 

    55 if p = ([], Und)

    56 then

    57   case get_obj g_tac pt (fst p) of

    58     Apply_Method ["Test", "squ-equ-test-subpbl1"] => ()

    59   | _ => error "Minisubpbl/790-complete-NEXT_STEP.sml, WRONG RESULT CHANGED 2"

    60 else error "Minisubpbl/790-complete-NEXT_STEP.sml, WRONG RESULT CHANGED 1";

    61 

    62 (*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)

    63
wneuper/isa