1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/systest/script_if.sml Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,169 @@
1.4 +(* 1.if-te-else- 8.02 f"ur Richard
1.5 +
1.6 + use"ifthenelse.sml";
1.7 + use"tests/rationals2.sml";
1.8 + *)
1.9 +
1.10 +
1.11 +
1.12 +(*---------------- 25.7.02 ---------------------*)
1.13 +
1.14 +val thy = Isac.thy;
1.15 +val t = (term_of o the o (parse thy)) "contains_root (sqrt(x)=1)";
1.16 +val Some(ss,tt) = eval_contains_root "xxx" 1 t thy;
1.17 +
1.18 +val t = (term_of o the o (parse thy)) "is_rootequation_in (sqrt(x)=1) x";
1.19 +val Some(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy;
1.20 +
1.21 +(*---
1.22 +val v = (term_of o the o (parse thy)) "x";
1.23 +val t = (term_of o the o (parse thy)) "sqrt(#3+#4*x)";
1.24 +scan t v;
1.25 +val t = (term_of o the o (parse thy)) "sqrt(#3+#4*a)";
1.26 +scan t v;
1.27 +val t = (term_of o the o (parse thy)) "#1 + #2*sqrt(#3+#4*x)";
1.28 +scan t v;
1.29 +val t = (term_of o the o (parse thy)) "x + #2*sqrt(#3+#4*a)";
1.30 +scan t v;
1.31 +---*)
1.32 +val t = (term_of o the o (parse thy))
1.33 + "is_rootequation_in (1 + 2*sqrt(3+4*x)=0) x";
1.34 +val Some(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy;
1.35 +
1.36 +val t = (term_of o the o (parse thy))
1.37 + "is_rootequation_in (x + 2*sqrt(3+4*a)=0) x";
1.38 +val Some(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy;
1.39 +
1.40 +val t = (term_of o the o (parse Test.thy))
1.41 + "is_rootequation_in (sqrt(x)=1) x";
1.42 +atomty Test.thy t;
1.43 +val t = (term_of o the o (parse Isac.thy))
1.44 + "is_rootequation_in (sqrt(x)=1) x";
1.45 +atomty Isac.thy t;
1.46 +
1.47 +(*
1.48 +val Some(tt,_) = rewrite_set_ Test.thytrue tval_rls t;
1.49 +*)
1.50 +val Some(tt,_) = rewrite_set_ Isac.thy true tval_rls t;
1.51 +
1.52 +rewrite_set "Isac.thy" true
1.53 + "tval_rls" "is_rootequation_in (sqrt(x)=1) x";
1.54 +rewrite_set "Test.thy" true
1.55 + "tval_rls" "is_rootequation_in (sqrt(x)=1) x";
1.56 +
1.57 +
1.58 +(*WN: ^^^--- bitte nimm vorerst immer Isac.thy, damit wird richtig gematcht,
1.59 + siehe unten. Wir werden w"ahrend der Arbeit auf diesen Fehler drauskommen*)
1.60 +store_pbt
1.61 + (prep_pbt (*Test.thy*) Isac.thy
1.62 + (["root","univariate","equation","test"],
1.63 + [("#Given" ,["equality e_","solveFor v_"]),
1.64 + ("#Where" ,["is_rootequation_in (e_::bool) (v_::real)"]),
1.65 + ("#Find" ,["solutions v_i_"])
1.66 + ],
1.67 + append_rls e_rls [Calc ("Test.is'_rootequation'_in",
1.68 + eval_is_rootequation_in "")],
1.69 + [("Test.thy","methode")]));
1.70 +
1.71 +match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] (get_pbt ["root","univariate","equation","test"]);
1.72 +
1.73 +
1.74 +(*---------------- 29.7.02 ---------------------*)
1.75 +
1.76 +store_pbt
1.77 + (prep_pbt Isac.thy
1.78 + (["approximate","univariate","equation","test"],
1.79 + [("#Given" ,["equality e_","solveFor v_","errorBound err_"]),
1.80 + ("#Where" ,["matches (?a = ?b) e_"]),
1.81 + ("#Find" ,["solutions v_i_"])
1.82 + ],
1.83 + append_rls e_rls [Calc ("Tools.matches",eval_matches "#matches_")],
1.84 + []));
1.85 +
1.86 +methods:= overwritel (!methods,
1.87 +[
1.88 + prep_met
1.89 + (("Isac.thy","solve_univar_err"):metID,
1.90 + [("#Given" ,["equality e_","solveFor v_","errorBound err_"]),
1.91 + ("#Find" ,["solutions v_i_"])
1.92 + ],
1.93 + {rew_ord'="tless_true",rls'="tval_rls",erls=e_rls,prls=e_rls,calc=[],
1.94 + asm_rls=[],asm_thm=[]},
1.95 + "Script Solve_univar_err (e_::bool) (v_::real) (err_::bool) = \
1.96 + \ (if (is_rootequation_in e_ v_)\
1.97 + \ then ((SubProblem (Isac_,[squareroot,univariate,equation],\
1.98 + \ (SqRoot_,square_equation)) [bool_ e_, real_ v_, bool_ err_]))\
1.99 + \ else ((SubProblem (Isac_,[linear,univariate,equation],\
1.100 + \ (RatArith_,solve_linear)) [bool_ e_, real_ v_])))"
1.101 + )]);
1.102 +
1.103 +val fmz = ["equality (1+2*x=0)","solveFor x","errorBound (eps=0)",
1.104 + "solutions L"];
1.105 +val (dI',pI',mI') =
1.106 + ("Isac.thy",["approximate","univariate","equation","test"],
1.107 + ("Isac.thy","solve_univar_err"));
1.108 +val p = e_pos'; val c = [];
1.109 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.110 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
1.111 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.112 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.113 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.114 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.115 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.116 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.117 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.118 +(*val nxt = ("Apply_Method",Apply_Method ("Isac.thy","solve_univar_err"))*)
1.119 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.120 +val (p,_,f,nxt,_,pt) = (me nxt p [1] pt) handle e => print_exn_G e;
1.121 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.122 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.123 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.124 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.125 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.126 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.127 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.128 +(*val nxt = ("Apply_Method",Apply_Method ("RatArith.thy","solve_linear"))*)
1.129 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.130 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.131 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.132 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.133 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.134 +if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -1 / 2]"))
1.135 + andalso nxt = ("End_Proof'",End_Proof') then ()
1.136 +else raise error "new behaviour in testexample rationals2.sml 1+2*x=0";
1.137 +
1.138 +(*---------------------------------*)
1.139 +"-------------- is_rootequ_in - SubProblem -------------------------";
1.140 +"-------------- is_rootequ_in - SubProblem -------------------------";
1.141 +"-------------- is_rootequ_in - SubProblem -------------------------";
1.142 +val fmz = ["equality (sqrt(x) - 1 = 0)","solveFor x","errorBound (eps=0)",
1.143 + "solutions L"];
1.144 +val (dI',pI',mI') =
1.145 + ("Isac.thy",["approximate","univariate","equation","test"],
1.146 + ("Isac.thy","solve_univar_err"));
1.147 +val p = e_pos'; val c = [];
1.148 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.149 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
1.150 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.151 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.152 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.153 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.154 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.155 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.156 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.157 +(*val nxt = ("Apply_Method",Apply_Method ("Isac.thy","solve_univar_err"))*)
1.158 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.159 +val (p,_,f,nxt,_,pt) = (me nxt p [1] pt) handle e => print_exn_G e;
1.160 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.161 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.162 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.163 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.164 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.165 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.166 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.167 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.168 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.169 +if p = ([1,1],Frm) andalso
1.170 + f = Form' (FormKF (~1,EdUndef,2,Nundef,"sqrt x - 1 = 0")) andalso
1.171 + nxt = ("Empty_Mstep",Empty_Mstep) (*script ist noch 'helpless'*) then ()
1.172 +else raise error "new behaviour in testexample rationals2.sml sqrt(x) - 1 = 0";