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/OLDTESTS/script_if.sml
author Walther Neuper <neuper@ist.tugraz.at>
Tue, 28 Sep 2010 09:06:56 +0200
branchisac-update-Isa09-2
changeset 38031 460c24a6a6ba
parent 37986 7b1d2366c191
child 38050 4c52ad406c20
permissions -rw-r--r--
tuned error and writeln

# raise error --> error
# writeln in atomtyp, atomty, atomt and xmlsrc 
     1 (* 1.if-te-else- 8.02 f"ur Richard

     2 

     3    use"ifthenelse.sml";

     4    use"tests/rationals2.sml";

     5    *)

     6 

     7 

     8 

     9 (*---------------- 25.7.02 ---------------------*)

    10 

    11 val thy = Isac.thy;

    12 val t = (term_of o the o (parse thy)) "contains_root (sqrt(x)=1)";

    13 val SOME(ss,tt) = eval_contains_root "xxx" 1 t thy;

    14 

    15 val t = (term_of o the o (parse thy)) "is_rootequation_in (sqrt(x)=1) x";

    16 val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy; 

    17 

    18 (*---

    19 val v = (term_of o the o (parse thy)) "x";

    20 val t = (term_of o the o (parse thy)) "sqrt(#3+#4*x)";

    21 scan t v;

    22 val t = (term_of o the o (parse thy)) "sqrt(#3+#4*a)";

    23 scan t v;

    24 val t = (term_of o the o (parse thy)) "#1 + #2*sqrt(#3+#4*x)";

    25 scan t v;

    26 val t = (term_of o the o (parse thy)) "x + #2*sqrt(#3+#4*a)";

    27 scan t v;

    28 ---*)

    29 val t = (term_of o the o (parse thy)) 

    30 	    "is_rootequation_in (1 + 2*sqrt(3+4*x)=0) x";

    31 val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy; 

    32 

    33 val t = (term_of o the o (parse thy)) 

    34 	    "is_rootequation_in (x + 2*sqrt(3+4*a)=0) x";

    35 val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy; 

    36 

    37 val t = (term_of o the o (parse Test.thy)) 

    38 	    "is_rootequation_in (sqrt(x)=1) x";

    39 atomty t;

    40 val t = (term_of o the o (parse Isac.thy)) 

    41 	    "is_rootequation_in (sqrt(x)=1) x";

    42 atomty t;

    43 

    44 (*

    45 val SOME(tt,_) = rewrite_set_ Test.thytrue tval_rls t;

    46 *)

    47 val SOME(tt,_) = rewrite_set_ Isac.thy true tval_rls t;

    48 

    49 rewrite_set "Isac.thy" true 

    50 	    "tval_rls" "is_rootequation_in (sqrt(x)=1) x";

    51 rewrite_set "Test.thy" true 

    52 	    "tval_rls" "is_rootequation_in (sqrt(x)=1) x";

    53 

    54 

    55 (*WN: ^^^--- bitte nimm vorerst immer Isac.thy, damit wird richtig gematcht, 

    56   siehe unten. Wir werden w"ahrend der Arbeit auf diesen Fehler drauskommen*)

    57 store_pbt

    58  (prep_pbt (*Test.thy*) Isac.thy

    59  (["root'","univariate","equation","test"],

    60   [("#Given" ,["equality e_e","solveFor v_v"]),

    61    ("#Where" ,["is_rootequation_in (e_e::bool) (v_::real)"]),

    62    ("#Find"  ,["solutions v_i_"]) 

    63   ],

    64   append_rls e_rls [Calc ("Test.is'_rootequation'_in",

    65 			  eval_is_rootequation_in "")],

    66   [("Test.thy","methode")]));

    67 

    68 match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] (get_pbt ["root'","univariate","equation","test"]); 

    69 

    70 

    71 (*---------------- 29.7.02 ---------------------*)

    72 

    73 store_pbt

    74  (prep_pbt Isac.thy

    75  (["approximate","univariate","equation","test"],

    76   [("#Given" ,["equality e_e","solveFor v_v","errorBound err_"]),

    77    ("#Where" ,["matches (?a = ?b) e_e"]),

    78    ("#Find"  ,["solutions v_i_"])

    79   ],

    80   append_rls e_rls [Calc ("Tools.matches",eval_matches "#matches_")],

    81   []));

    82 

    83 methods:= overwritel (!methods,

    84 [

    85  prep_met

    86  (("Isac.thy","solve_univar_err"):metID,

    87    [("#Given" ,["equality e_e","solveFor v_v","errorBound err_"]),

    88     ("#Find"  ,["solutions v_i_"])

    89     ],

    90    {rew_ord'="tless_true",rls'="tval_rls",erls=e_rls,prls=e_rls,calc=[],

    91     asm_rls=[],asm_thm=[]},

    92  "Script Solve_univar_err (e_e::bool) (v_::real) (err_::bool) =  \

    93  \ (if (is_rootequation_in e_e v_v)\

    94  \  then ((SubProblem (Isac_,[squareroot,univariate,equation],\

    95  \         (SqRoot_,square_equation)) [BOOL e_e, REAL v_v, BOOL err_]))\

    96  \  else ((SubProblem (Isac_,[linear,univariate,equation],\

    97  \         (RatArith_,solve_linear)) [BOOL e_e, REAL v_])))"

    98  )]);

    99 

   100 val fmz = ["equality (1+2*x=0)","solveFor x","errorBound (eps=0)",

   101 	   "solutions L"];

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

   103   ("Isac.thy",["approximate","univariate","equation","test"],

   104    ("Isac.thy","solve_univar_err"));

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

   106 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

   107 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;

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

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

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

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

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

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

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

   115 (*val nxt = ("Apply_Method",Apply_Method ("Isac.thy","solve_univar_err"))*)

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

   117 val (p,_,f,nxt,_,pt) = (me nxt p [1] pt) handle e => print_exn_G e;

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

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

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

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

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

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

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

   125 (*val nxt = ("Apply_Method",Apply_Method ("RatArith.thy","solve_linear"))*)

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

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

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

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

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

   131 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -1 / 2]"))

   132    andalso nxt = ("End_Proof'",End_Proof') then ()

   133 else error "new behaviour in testexample rationals2.sml 1+2*x=0";

   134 

   135 (*---------------------------------*)

   136 "-------------- is_rootequ_in - SubProblem -------------------------";

   137 "-------------- is_rootequ_in - SubProblem -------------------------";

   138 "-------------- is_rootequ_in - SubProblem -------------------------";

   139 val fmz = ["equality (sqrt(x) - 1 = 0)","solveFor x","errorBound (eps=0)",

   140 	   "solutions L"];

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

   142   ("Isac.thy",["approximate","univariate","equation","test"],

   143    ("Isac.thy","solve_univar_err"));

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

   145 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

   146 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;

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

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

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

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

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

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

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

   154 (*val nxt = ("Apply_Method",Apply_Method ("Isac.thy","solve_univar_err"))*)

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

   156 val (p,_,f,nxt,_,pt) = (me nxt p [1] pt) handle e => print_exn_G e;

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

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

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

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

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

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

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

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

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

   166 if p = ([1,1],Frm) andalso 

   167    f = Form' (FormKF (~1,EdUndef,2,Nundef,"sqrt x - 1 = 0")) andalso

   168    nxt = ("Empty_Tac",Empty_Tac) (*script ist noch 'helpless'*) then ()

   169 else error "new behaviour in testexample rationals2.sml sqrt(x) - 1 = 0";
wneuper/isa