src/Pure/isac/smltest/OLDTESTS/modspec.sml
author Walther Neuper <neuper@ist.tugraz.at>
Wed, 21 Jul 2010 13:53:39 +0200
branchisac-from-Isabelle2009-2
changeset 37871 875b6efa7ced
permissions -rw-r--r--
added isac-hook in Pure/thm and isac-code
     1 (* WN040107
     2    use"../systest/modspec.sml";
     3    use"systest/modspec.sml";
     4    use"modspec.sml";
     5  *)
     6 
     7 "--------- get_interval after replace} other 2 -------------------";
     8 "-----------------------------------------------------------------";
     9 
    10 
    11 "--------- get_interval after replace} other 2 -------------------";
    12 "--------- get_interval after replace} other 2 -------------------";
    13 "--------- get_interval after replace} other 2 -------------------";
    14  states:=[];
    15  CalcTree
    16  [(["equality (x+1=2)", "solveFor x","solutions L"], 
    17    ("Test.thy", 
    18     ["sqroot-test","univariate","equation","test"],
    19     ["Test","squ-equ-test-subpbl1"]))];
    20  Iterator 1;
    21  moveActiveRoot 1;
    22  autoCalculate 1 CompleteCalc;
    23  moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
    24  replaceFormula 1 "x = 1"; 
    25  (*... returns calcChangedEvent with ...*)
    26  val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
    27  val ((pt,_),_) = get_calc 1;
    28 
    29 print_depth 99;map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3;
    30 if map fst (get_interval ([],Pbl) ([],Res) 9999 pt) = 
    31     [([], Pbl), ([1], Frm),([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), 
    32      ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
    33       ([3, 2], Res)] then () else
    34 raise error "modspec.sml: diff.behav. get_interval after replace} other 2 a";
    35 
    36 print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt);
    37 print_depth 3;
    38 if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) = 
    39     [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else
    40 raise error "modspec.sml: diff.behav. get_interval after replace} other 2 b";