diff -r 5100a9c3abf8 -r 875b6efa7ced src/Pure/isac/smltest/Scripts/calculate-float.sml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/isac/smltest/Scripts/calculate-float.sml	Wed Jul 21 13:53:39 2010 +0200
@@ -0,0 +1,147 @@
+(* (c) Stefan Rath 2005
+   tests for sml/Scripts/calculate.sml
+
+   use"~/proto2/isac/src/smltest/Scripts/calculate-float.sml";
+   use"calculate-float.sml";
+   *)
+
+
+(*WN.28.3.03 fuer Matthias*)
+(*Floatingpointnumbers, direkte Darstellung der abstrakten Syntax:*)
+ val thy = Float.thy;
+ val t = str2term "Float ((1,2),(0,0))";
+ atomt t;
+ val t = (term_of o the o (parse thy)) 
+	     "Float ((1,2),(0,0)) + Float ((3,4),(0,0)) * \
+	     \Float ((5,6),(0,0)) / Float ((7,8),(0,0))";
+ atomt t;
+(*die konkrete Syntax wird noch verschoenert*)
+
+ val thy = "Test.thy";
+ val op_ = "divide_";
+ val ct = "-6 / 3";
+ val Some (ct,_) = calculate thy (the (assoc (calclist, op_))) ct;
+
+(*-----WN050315------------------------------------------------------*)
+(*..*)
+val t = str2term "Float ((1,2),(0,0))";
+atomty t;
+val Const ("Float.Float",_) $
+	  (Const ("Pair",_) $ 
+		 (Const ("Pair",_) $ Free (i1,_) $ Free (i2,_)) $ _) = t;
+    
+val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0))";
+atomty t;
+(*-----WN050315------------------------------------------------------*)
+
+
+val thy = Float.thy;
+
+(*.calculate the value of a pair of floats.*)
+val ((a,b),(c,d)) = calc "op +" ((~1,0),(0,0)) ((2,0),(0,0));
+
+
+(*.build the term.*)
+term_of_float HOLogic.realT ((~1,0),(0,0));
+term_of_float HOLogic.realT ((~1,11),(0,0));
+
+(*--18.3.05-------------------------*)
+val t = Free ("sdfsdfsdf", HOLogic.realT);
+val t = Free ("-123,456", HOLogic.realT);
+val t = Free ("0,123456", HOLogic.realT);
+term2str t;
+(*----(1)------------------------------*)
+val t = str2term "IFloat (1, 2, 3)";
+val t = str2term "CFloat (1, 2)";
+atomt t;
+atomty t;
+val Some ct = parse Float.thy "IFloat (1, 2, 3)";
+val Some ct = parse Float.thy "CFloat (1, 2)";
+atomt (term_of ct);
+atomty (term_of ct);
+(*----(2)------------------------------*)
+val Some ct = parse Float.thy "IFloat (-1, 2, 3)";
+val t = (term_of ct);
+atomty t;
+(*#######################################################################3
+val Const
+         ("Float.IFloat", _) $
+	 (Const
+              ("Pair", _) $
+              Free (no, _) $
+              (Const
+                   ("Pair", _) $
+		   Free (commas, _) $ Free (exp, _))) = t;
+
+fun IFloat2CFloat 
+	(Const
+        ("Float.IFloat", _) $
+	(Const
+             ("Pair", _) $
+             Free (no, _) $
+             (Const
+                  ("Pair", _) $
+		  Free (commas, _) $ Free (exp, _)))) =
+	Const ("Float.CFloat", HOLogic.realT(*wrong type*)) $
+	      (Const
+		   ("Pair", HOLogic.realT(*wrong type*)) $
+		   Free (no^"."^commas, HOLogic.realT) 
+		   $ Free ("accuracy", HOLogic.realT))
+
+  | IFloat2CFloat t =
+    raise error ("IFloat2CFloat: invalid argument "^term2str t);
+
+val cf = IFloat2CFloat t;
+term2str cf;
+
+(*in IsacKnowledge/Float.ML: fun pairt -> Pair-term*)
+
+fun CFloat2Free (Const ("Float.CFloat", _) $
+		       (Const ("Pair", _) $ Free (no_commas, _) $ _)) =
+    Free (no_commas, HOLogic.realT);
+
+val t' = CFloat2Free cf;
+term2str t';
+
+fun CFloat2sml (Const ("Float.CFloat", _) $
+		      (Const ("Pair", _) $ Free (float, _) $ _(**))) =
+    float;
+CFloat2sml cf;
+
+(*--18.3.05-------------------------*)
+
+
+(*.the function evaluating a binary operator.*)
+val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0))";
+val Some (thmid, t) = eval_binop "#add_" "op +" t thy;
+term2str t;
+
+
+(*.scan a term for a pair of floats.*)
+ val Some (thmid,t') = get_pair thy op_ eval_fn t;
+
+
+(*.use 'calculate' explicitly.*)
+ val thy = Test.thy;
+ val op_ = "divide_";
+ val t = str2term "sqrt (x ^^^ 2 + -3 * x) =\
+		  \Float ((5,6),(0,0)) / Float ((7,8),(0,0))";
+ val Some (t',_) = calculate_ thy (the (assoc (calclist, op_))) t;
+ term2str t';
+
+
+(*.rewrite with ruleset TEST...simplify (calling calculate internally.*)
+val t = str2term "a + Float ((1,2),(0,0)) + a + Float ((3,4),(0,0)) * \
+		 \Float ((5,6),(0,0)) / Float ((7,8),(0,0))";
+val Some (t',_) = rewrite_set_ thy false norm_Rational(*///*) t; term2str t';
+(*Float ((...,...) + 2*a*)
+
+
+(*. parse a float as seen by the user  .*)
+val Some t = parse Float.thy "123.456"; 
+val Some t = parse Float.thy "-123.456"; 
+val Some t = parse Float.thy "123.456 E6789"; 
+val Some t = parse Float.thy "123.456 E-6789"; 
+val Some t = parse Float.thy "-123.456 E-6789"; 
+
+################################################################*)