(* (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 "Groups.plus_class.plus" ((~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_" "Groups.plus_class.plus" 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"; 

################################################################*)