Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/ProgLang/calculate-float.sml
author Walther Neuper <neuper@ist.tugraz.at>
Thu, 23 Sep 2010 14:49:23 +0200
branchisac-update-Isa09-2
changeset 38014 3e11e3c2dc42
parent 37960 ec20007095f2
permissions -rw-r--r--
updated "op +", "op -", "op *". "HOL.divide" in src & test

find . -type f -exec sed -i s/"\"op +\""/"\"Groups.plus_class.plus\""/g {} \;
find . -type f -exec sed -i s/"\"op -\""/"\"Groups.minus_class.minus\""/g {} \;
find . -type f -exec sed -i s/"\"op *\""/"\"Groups.times_class.times\""/g {} \;
find . -type f -exec sed -i s/"\"HOL.divide\""/"\"Rings.inverse_class.divide\""/g {} \; 
     1 (* (c) Stefan Rath 2005

     2    tests for sml/Scripts/calculate.sml

     3 

     4    use"~/proto2/isac/src/smltest/Scripts/calculate-float.sml";

     5    use"calculate-float.sml";

     6    *)

     7 

     8 

     9 (*WN.28.3.03 fuer Matthias*)

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

    11  val thy = Float.thy;

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

    13  atomt t;

    14  val t = (term_of o the o (parse thy)) 

    15 	     "Float ((1,2),(0,0)) + Float ((3,4),(0,0)) * \

    16 	     \Float ((5,6),(0,0)) / Float ((7,8),(0,0))";

    17  atomt t;

    18 (*die konkrete Syntax wird noch verschoenert*)

    19 

    20  val thy = "Test.thy";

    21  val op_ = "divide_";

    22  val ct = "-6 / 3";

    23  val SOME (ct,_) = calculate thy (the (assoc (calclist, op_))) ct;

    24 

    25 (*-----WN050315------------------------------------------------------*)

    26 (*..*)

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

    28 atomty t;

    29 val Const ("Float.Float",_) $

    30 	  (Const ("Pair",_) $ 

    31 		 (Const ("Pair",_) $ Free (i1,_) $ Free (i2,_)) $ _) = t;

    32     

    33 val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0))";

    34 atomty t;

    35 (*-----WN050315------------------------------------------------------*)

    36 

    37 

    38 val thy = Float.thy;

    39 

    40 (*.calculate the value of a pair of floats.*)

    41 val ((a,b),(c,d)) = calc "Groups.plus_class.plus" ((~1,0),(0,0)) ((2,0),(0,0));

    42 

    43 

    44 (*.build the term.*)

    45 term_of_float HOLogic.realT ((~1,0),(0,0));

    46 term_of_float HOLogic.realT ((~1,11),(0,0));

    47 

    48 (*--18.3.05-------------------------*)

    49 val t = Free ("sdfsdfsdf", HOLogic.realT);

    50 val t = Free ("-123,456", HOLogic.realT);

    51 val t = Free ("0,123456", HOLogic.realT);

    52 term2str t;

    53 (*----(1)------------------------------*)

    54 val t = str2term "IFloat (1, 2, 3)";

    55 val t = str2term "CFloat (1, 2)";

    56 atomt t;

    57 atomty t;

    58 val SOME ct = parse Float.thy "IFloat (1, 2, 3)";

    59 val SOME ct = parse Float.thy "CFloat (1, 2)";

    60 atomt (term_of ct);

    61 atomty (term_of ct);

    62 (*----(2)------------------------------*)

    63 val SOME ct = parse Float.thy "IFloat (-1, 2, 3)";

    64 val t = (term_of ct);

    65 atomty t;

    66 (*#######################################################################3

    67 val Const

    68          ("Float.IFloat", _) $

    69 	 (Const

    70               ("Pair", _) $

    71               Free (no, _) $

    72               (Const

    73                    ("Pair", _) $

    74 		   Free (commas, _) $ Free (exp, _))) = t;

    75 

    76 fun IFloat2CFloat 

    77 	(Const

    78         ("Float.IFloat", _) $

    79 	(Const

    80              ("Pair", _) $

    81              Free (no, _) $

    82              (Const

    83                   ("Pair", _) $

    84 		  Free (commas, _) $ Free (exp, _)))) =

    85 	Const ("Float.CFloat", HOLogic.realT(*wrong type*)) $

    86 	      (Const

    87 		   ("Pair", HOLogic.realT(*wrong type*)) $

    88 		   Free (no^"."^commas, HOLogic.realT) 

    89 		   $ Free ("accuracy", HOLogic.realT))

    90 

    91   | IFloat2CFloat t =

    92     raise error ("IFloat2CFloat: invalid argument "^term2str t);

    93 

    94 val cf = IFloat2CFloat t;

    95 term2str cf;

    96 

    97 (*in IsacKnowledge/Float.ML: fun pairt -> Pair-term*)

    98 

    99 fun CFloat2Free (Const ("Float.CFloat", _) $

   100 		       (Const ("Pair", _) $ Free (no_commas, _) $ _)) =

   101     Free (no_commas, HOLogic.realT);

   102 

   103 val t' = CFloat2Free cf;

   104 term2str t';

   105 

   106 fun CFloat2sml (Const ("Float.CFloat", _) $

   107 		      (Const ("Pair", _) $ Free (float, _) $ _(**))) =

   108     float;

   109 CFloat2sml cf;

   110 

   111 (*--18.3.05-------------------------*)

   112 

   113 

   114 (*.the function evaluating a binary operator.*)

   115 val t = str2term "Float ((1,2),(0,0)) + Float ((3,4),(0,0))";

   116 val SOME (thmid, t) = eval_binop "#add_" "Groups.plus_class.plus" t thy;

   117 term2str t;

   118 

   119 

   120 (*.scan a term for a pair of floats.*)

   121  val SOME (thmid,t') = get_pair thy op_ eval_fn t;

   122 

   123 

   124 (*.use 'calculate' explicitly.*)

   125  val thy = Test.thy;

   126  val op_ = "divide_";

   127  val t = str2term "sqrt (x ^^^ 2 + -3 * x) =\

   128 		  \Float ((5,6),(0,0)) / Float ((7,8),(0,0))";

   129  val SOME (t',_) = calculate_ thy (the (assoc (calclist, op_))) t;

   130  term2str t';

   131 

   132 

   133 (*.rewrite with ruleset TEST...simplify (calling calculate internally.*)

   134 val t = str2term "a + Float ((1,2),(0,0)) + a + Float ((3,4),(0,0)) * \

   135 		 \Float ((5,6),(0,0)) / Float ((7,8),(0,0))";

   136 val SOME (t',_) = rewrite_set_ thy false norm_Rational(*///*) t; term2str t';

   137 (*Float ((...,...) + 2*a*)

   138 

   139 

   140 (*. parse a float as seen by the user  .*)

   141 val SOME t = parse Float.thy "123.456"; 

   142 val SOME t = parse Float.thy "-123.456"; 

   143 val SOME t = parse Float.thy "123.456 E6789"; 

   144 val SOME t = parse Float.thy "123.456 E-6789"; 

   145 val SOME t = parse Float.thy "-123.456 E-6789"; 

   146 

   147 ################################################################*)
wneuper/isa