(* use"Float.ML";

    *)

 (*WN.28.3.03 fuer Matthias*)

 (*Floatingpointnumbers, direkte Darstellung der abstrakten Syntax:*)

  val t = (term_of o the o (parse thy)) "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*)

 (*--- 15.4.03

 fun calc "op +"  (n1, n2) = n1+n2

   | calc "op -"  (n1, n2) = n1-n2

   | calc "op *"  (n1, n2) = n1*n2

   | calc "HOL.divide"(n1, n2) = n1 div n2

   | calc "Atools.pow"(n1, n2) = power n1 n2

   | calc op_ _ = raise error ("calc: operator = "^op_^" not defined");

 ---*)

 (*.used for calculating built in binary operations in Isabelle2002.

    integer numerals n are ((n,0),(0,0)) i.e. precision is (0,0)*)

 fun calc "op +" ((a, b), _:int * int) ((c, d), _:int * int)  = 

     if b < d 

     then ((a + c * power 10 (d - b), b), (0, 0))(*FIXXXME precision*)

     else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*)

   | calc "op -" ((a, 0), _) ((c, 0), _) =       (*FIXXXME float + prec.*)

     ((a - c,0),(0,0))

   | calc "op *" ((a, b), _) ((c, d), _) =       (*FIXXXME precision*)

     ((a * c, b + d), (0, 0))

   | calc "HOL.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)

     ((a div c, 0), (0, 0))

   | calc "Atools.pow" ((a, b), _) ((c, d), _) = (*FIXXXME float + prec.*)

     ((power a c, 0), (0, 0))

   | calc op_ ((a, b), (p11, p12)) ((c, d), (p21, p22)) = 

     raise error ("calc: not impl. for Float (("^

 		 (string_of_int a  )^","^(string_of_int b  )^"), ("^

 		 (string_of_int p11)^","^(string_of_int p12)^")) "^op_^" (("^

 		 (string_of_int c  )^","^(string_of_int d  )^"), ("^

 		 (string_of_int p21)^","^(string_of_int p22)^"))");

 (*> calc "op +" ((~1,0),(0,0)) ((2,0),(0,0)); 

 val it = ((1,0),(0,0))*)

 (*.convert int and float to internal floatingpoint prepresentation.*)

 fun numeral (Free (str, T)) = 

     (case int_of_str str of

 	 Some i => Some ((i, 0), (0, 0))

        | None => None)

   | numeral (Const ("Float.Float", _) $

 		   (Const ("Pair", _) $

 			  (Const ("Pair", T) $ Free (v1, _) $ Free (v2,_)) $

 			  (Const ("Pair", _) $ Free (p1, _) $ Free (p2,_))))=

     (case (int_of_str v1, int_of_str v2, int_of_str p1, int_of_str p2) of

 	(Some v1', Some v2', Some p1', Some p2') =>

 	Some ((v1', v2'), (p1', p2'))

       | _ => None)

   | numeral _ = None;

 (*.convert internal floatingpoint prepresentation to int and float.*)

 fun term_of_float T ((val1,    0), (         0,          0)) =

     term_of_num T val1

   | term_of_float T ((val1, val2), (precision1, precision2)) =

     let val pT = pairT T T

     in Const ("Float.Float", (pairT pT pT) --> T)

 	     $ (pairt (pairt (Free (str_of_int val1, T))

 			     (Free (str_of_int val2, T)))

 		      (pairt (Free (str_of_int precision1, T))

 			     (Free (str_of_int precision2, T))))

     end;

 (*> val t = str2term "Float ((1,2),(0,0))";

 > val Const ("Float.Float", fT) $ _ = t;

 > atomtyp fT;

 > val ffT = (pairT (pairT HOLogic.realT HOLogic.realT) 

 > 	     (pairT HOLogic.realT HOLogic.realT)) --> HOLogic.realT;

 > atomtyp ffT;

 > fT = ffT;

 val it = true : bool

 t = float_term_of_num HOLogic.realT ((1,2),(0,0));

 val it = true : bool*)

 (*.assoc. convert internal floatingpoint prepresentation to int and float.*)

 fun var_op_float v op_ optype ntyp ((v1, 0), (0, 0)) =

     var_op_num v op_ optype ntyp v1

   | var_op_float v op_ optype T ((v1, v2), (p1, p2)) =

     let val pT = pairT T T

     in Const (op_, optype) $ v $ 

 	     (Const ("Float.Float", (pairT pT pT) --> T)

 		    $ (pairt (pairt (Free (str_of_int v1, T))

 				    (Free (str_of_int v2, T)))

 			     (pairt (Free (str_of_int p1, T))

 				    (Free (str_of_int p2, T)))))

     end;

 (*> val t = str2term "a + b";

 > val Const ("op +", optype) $ _ $ _ = t;

 > val t = str2term "v + Float ((11,-1),(0,0))";val v = str2term "v";

 > t = var_op_float v "op +" optype HOLogic.realT ((11,~1),(0,0));

 val it = true : bool*)

 (*.assoc. convert internal floatingpoint prepresentation to int and float.*)

 fun float_op_var v op_ optype ntyp ((v1, 0), (0, 0)) =

     num_op_var v op_ optype ntyp v1

   | float_op_var v op_ optype T ((v1, v2), (p1, p2)) =

     let val pT = pairT T T

     in Const (op_,optype) $ 

 	     (Const ("Float.Float", (pairT pT pT) --> T)

 		    $ (pairt (pairt (Free (str_of_int v1, T))

 				    (Free (str_of_int v2, T)))

 			     (pairt (Free (str_of_int p1, T))

 				    (Free (str_of_int p2, T))))) $ v

     end;

 (*> val t = str2term "a + b";

 > val Const ("op +", optype) $ _ $ _ = t;

 > val t = str2term "Float ((11,-1),(0,0)) + v";val v = str2term "v";

 > t = float_op_var v "op +" optype HOLogic.realT ((11,~1),(0,0));

 val it = true : bool*)