1.1 --- a/test/Tools/isac/Scripts/calculate-float.sml Mon Aug 30 14:29:49 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,147 +0,0 @@
1.4 -(* (c) Stefan Rath 2005
1.5 - tests for sml/Scripts/calculate.sml
1.6 -
1.7 - use"~/proto2/isac/src/smltest/Scripts/calculate-float.sml";
1.8 - use"calculate-float.sml";
1.9 - *)
1.10 -
1.11 -
1.12 -(*WN.28.3.03 fuer Matthias*)
1.13 -(*Floatingpointnumbers, direkte Darstellung der abstrakten Syntax:*)
1.14 - val thy = Float.thy;
1.15 - val t = str2term "Float ((1,2),(0,0))";
1.16 - atomt t;
1.17 - val t = (term_of o the o (parse thy))
1.18 - "Float ((1,2),(0,0)) + Float ((3,4),(0,0)) * \
1.19 - \Float ((5,6),(0,0)) / Float ((7,8),(0,0))";
1.20 - atomt t;
1.21 -(*die konkrete Syntax wird noch verschoenert*)
1.22 -
1.23 - val thy = "Test.thy";
1.24 - val op_ = "divide_";
1.25 - val ct = "-6 / 3";
1.26 - val SOME (ct,_) = calculate thy (the (assoc (calclist, op_))) ct;
1.27 -
1.28 -(*-----WN050315------------------------------------------------------*)
1.29 -(*..*)
1.30 -val t = str2term "Float ((1,2),(0,0))";
1.31 -atomty t;
1.32 -val Const ("Float.Float",_) $
1.33 - (Const ("Pair",_) $
1.34 - (Const ("Pair",_) $ Free (i1,_) $ Free (i2,_)) $ _) = t;
1.35 -
1.36 -val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0))";
1.37 -atomty t;
1.38 -(*-----WN050315------------------------------------------------------*)
1.39 -
1.40 -
1.41 -val thy = Float.thy;
1.42 -
1.43 -(*.calculate the value of a pair of floats.*)
1.44 -val ((a,b),(c,d)) = calc "op +" ((~1,0),(0,0)) ((2,0),(0,0));
1.45 -
1.46 -
1.47 -(*.build the term.*)
1.48 -term_of_float HOLogic.realT ((~1,0),(0,0));
1.49 -term_of_float HOLogic.realT ((~1,11),(0,0));
1.50 -
1.51 -(*--18.3.05-------------------------*)
1.52 -val t = Free ("sdfsdfsdf", HOLogic.realT);
1.53 -val t = Free ("-123,456", HOLogic.realT);
1.54 -val t = Free ("0,123456", HOLogic.realT);
1.55 -term2str t;
1.56 -(*----(1)------------------------------*)
1.57 -val t = str2term "IFloat (1, 2, 3)";
1.58 -val t = str2term "CFloat (1, 2)";
1.59 -atomt t;
1.60 -atomty t;
1.61 -val SOME ct = parse Float.thy "IFloat (1, 2, 3)";
1.62 -val SOME ct = parse Float.thy "CFloat (1, 2)";
1.63 -atomt (term_of ct);
1.64 -atomty (term_of ct);
1.65 -(*----(2)------------------------------*)
1.66 -val SOME ct = parse Float.thy "IFloat (-1, 2, 3)";
1.67 -val t = (term_of ct);
1.68 -atomty t;
1.69 -(*#######################################################################3
1.70 -val Const
1.71 - ("Float.IFloat", _) $
1.72 - (Const
1.73 - ("Pair", _) $
1.74 - Free (no, _) $
1.75 - (Const
1.76 - ("Pair", _) $
1.77 - Free (commas, _) $ Free (exp, _))) = t;
1.78 -
1.79 -fun IFloat2CFloat
1.80 - (Const
1.81 - ("Float.IFloat", _) $
1.82 - (Const
1.83 - ("Pair", _) $
1.84 - Free (no, _) $
1.85 - (Const
1.86 - ("Pair", _) $
1.87 - Free (commas, _) $ Free (exp, _)))) =
1.88 - Const ("Float.CFloat", HOLogic.realT(*wrong type*)) $
1.89 - (Const
1.90 - ("Pair", HOLogic.realT(*wrong type*)) $
1.91 - Free (no^"."^commas, HOLogic.realT)
1.92 - $ Free ("accuracy", HOLogic.realT))
1.93 -
1.94 - | IFloat2CFloat t =
1.95 - raise error ("IFloat2CFloat: invalid argument "^term2str t);
1.96 -
1.97 -val cf = IFloat2CFloat t;
1.98 -term2str cf;
1.99 -
1.100 -(*in IsacKnowledge/Float.ML: fun pairt -> Pair-term*)
1.101 -
1.102 -fun CFloat2Free (Const ("Float.CFloat", _) $
1.103 - (Const ("Pair", _) $ Free (no_commas, _) $ _)) =
1.104 - Free (no_commas, HOLogic.realT);
1.105 -
1.106 -val t' = CFloat2Free cf;
1.107 -term2str t';
1.108 -
1.109 -fun CFloat2sml (Const ("Float.CFloat", _) $
1.110 - (Const ("Pair", _) $ Free (float, _) $ _(**))) =
1.111 - float;
1.112 -CFloat2sml cf;
1.113 -
1.114 -(*--18.3.05-------------------------*)
1.115 -
1.116 -
1.117 -(*.the function evaluating a binary operator.*)
1.118 -val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0))";
1.119 -val SOME (thmid, t) = eval_binop "#add_" "op +" t thy;
1.120 -term2str t;
1.121 -
1.122 -
1.123 -(*.scan a term for a pair of floats.*)
1.124 - val SOME (thmid,t') = get_pair thy op_ eval_fn t;
1.125 -
1.126 -
1.127 -(*.use 'calculate' explicitly.*)
1.128 - val thy = Test.thy;
1.129 - val op_ = "divide_";
1.130 - val t = str2term "sqrt (x ^^^ 2 + -3 * x) =\
1.131 - \Float ((5,6),(0,0)) / Float ((7,8),(0,0))";
1.132 - val SOME (t',_) = calculate_ thy (the (assoc (calclist, op_))) t;
1.133 - term2str t';
1.134 -
1.135 -
1.136 -(*.rewrite with ruleset TEST...simplify (calling calculate internally.*)
1.137 -val t = str2term "a + Float ((1,2),(0,0)) + a + Float ((3,4),(0,0)) * \
1.138 - \Float ((5,6),(0,0)) / Float ((7,8),(0,0))";
1.139 -val SOME (t',_) = rewrite_set_ thy false norm_Rational(*///*) t; term2str t';
1.140 -(*Float ((...,...) + 2*a*)
1.141 -
1.142 -
1.143 -(*. parse a float as seen by the user .*)
1.144 -val SOME t = parse Float.thy "123.456";
1.145 -val SOME t = parse Float.thy "-123.456";
1.146 -val SOME t = parse Float.thy "123.456 E6789";
1.147 -val SOME t = parse Float.thy "123.456 E-6789";
1.148 -val SOME t = parse Float.thy "-123.456 E-6789";
1.149 -
1.150 -################################################################*)