wneuper/isa: src/Tools/isac/ProgLang/evaluate.sml@3a7fb975af9d

     1 (* calculate values for function constants

     2    (c) Walther Neuper 000106

     4 Some formula transformations cannot be done by rewriting;

     5 these are done by structure Eval, which works tightly intertwined with structure Rewrite.

     6 *)

     8 signature EVALUATE =

     9 sig

    10   type float

    11   val calc_equ: string -> int * int -> bool

    12   val power: int -> int -> int

    13   val sign_mult: int -> int -> int

    14   val squfact: int -> int

    15   val gcd: int -> int -> int

    16   val sqrt: int -> int

    17   val adhoc_thm: theory -> string * Eval_Def.eval_fn -> term -> (string * thm) option

    18   val adhoc_thm1_: theory -> Eval_Def.cal -> term -> (string * thm) option

    19   val norm: term -> term

    20   val popt2str: ('a * term) option -> string

    21   val numeral: term -> ((int * int) * (int * int)) option

    22   val calcul: string -> float -> float -> float

    23   val term_of_float: typ -> float -> term

    24   val var_op_float: term -> string -> typ -> typ ->float -> term

    25   val float_op_var: term -> string -> typ -> typ -> float -> term

    26   val trace_on: bool Unsynchronized.ref

    28 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

    29   (* NONE *)

    30 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

    31   val get_pair: theory -> string -> Eval_Def.eval_fn -> term -> (string * term) option

    32   val mk_rule: term list * term * term -> term

    33   val divisors: int -> int list

    34   val doubles: int list -> int list

    35 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

    36 end

    38 (**)

    39 structure Eval(**): EVALUATE(**) =

    40 struct

    41 (**)

    43 type float =

    44   (int * int)   (* value:     significand * exponent *)

    45   * (int * int); (* precision: significand * exponent *)

    47 (* trace internal steps of isac's numeral calculations *)

    48 val trace_on = Unsynchronized.ref false;

    50 (** calculate integers **)

    52 fun calc_equ "less"  (n1, n2) = n1 < n2

    53   | calc_equ "less_eq" (n1, n2) = n1 <= n2

    54   | calc_equ op_ _ = error ("calc_equ: operator = " ^ op_ ^ " not defined");

    55 fun sqrt (n:int) = if n < 0 then 0 else (trunc o Math.sqrt o Real.fromInt (*FIXME*)) n;

    56 fun power _ 0 = 1

    57   | power b n =

    58     if n > 0 then b* (power b (n - 1))

    59     else error ("power " ^ TermC.str_of_int b ^ " " ^ TermC.str_of_int n);

    60 fun gcd 0 b = b

    61   | gcd a b = if a < b then gcd (b mod a) a else gcd (a mod b) b;

    62 fun sign n =

    63   if n < 0 then ~1

    64 	else if n = 0 then 0 else 1;

    65 fun sign_mult n1 n2 = (sign n1) * (sign n2);

    67 infix dvd;

    68 fun d dvd n = n mod d = 0;

    69 fun divisors n =

    70   let fun pdiv ds d n =

    71     if d = n then d :: ds

    72     else if d dvd n then pdiv (d :: ds) d (n div d)

    73 	 else pdiv ds (d + 1) n

    74   in pdiv [] 2 n end;

    76 fun doubles ds = (* ds is ordered *)

    77   let fun dbls ds [] = ds

    78 	| dbls ds [ _ ] = ds

    79 	| dbls ds (i :: i' :: is) = if i = i' then dbls (i :: ds) is

    80 				else dbls ds (i'::is)

    81   in dbls [] ds end;

    82 fun squfact 0 = 0

    83   | squfact 1 = 1

    84   | squfact n = foldl op* (1, (doubles o divisors) n);

    87 (** calculate numerals **)

    89 fun popt2str (SOME (_, term)) = "SOME " ^ UnparseC.term term (*TODO \<longrightarrow> str_of_termopt*)

    90   | popt2str NONE = "NONE";

    92 (* scan a term for applying eval_fn ef

    93 args

    94   thy:

    95   op_: operator (as string) selecting the root of the pair

    96   ef : fn : (string -> term -> theory -> (string * term) option)

    97              ^^^^^^... for creating the string for the resulting theorem

    98   t  : term to be scanned

    99 result:

   100   (string * term) option: found by the eval_* -function of type

   101        fn : string -> string -> term -> theory -> (string * term) option

   102             ^^^^^^... the selecting operator op_ (variable for eval_binop)

   103 *)

   104 fun trace_calc0 str =

   105   if ! trace_on then writeln ("### " ^ str) else ()

   106 fun trace_calc1 str1 str2 =

   107   if ! trace_on then writeln (str1 ^ str2) else ()

   108 fun trace_calc2 str term popt =

   109   if ! trace_on then writeln (str ^ UnparseC.term term ^ " , " ^ popt2str popt) else ()

   110 fun trace_calc3 str term =

   111   if ! trace_on then writeln ("### " ^ str ^ UnparseC.term term) else ()

   112 fun trace_calc4 str t1 t2 =

   113   if ! trace_on then writeln ("### " ^ str ^ UnparseC.term t1 ^ " $ " ^ UnparseC.term t2) else ()

   115 fun get_pair thy op_ (ef: Eval_Def.eval_fn) (t as (Const (op0, _) $ arg)) =                (* unary fns *)

   116     if op_ = op0 then

   117       let val popt = ef op_ t thy

   118       in case popt of SOME _ => popt | NONE => get_pair thy op_ ef arg end

   119     else get_pair thy op_ ef arg

   120   | get_pair thy "Prog_Expr.ident" ef (t as (Const ("Prog_Expr.ident", _) $ _ $ _ )) =

   121     ef "Prog_Expr.ident" t thy                                                      (* not nested *)

   122   | get_pair thy op_ ef (t as (Const (op0,_) $ t1 $ t2)) =                      (* binary funs *)

   123     (trace_calc1 "1.. get_pair: binop = " op_;

   124     if op_ = op0 then

   125       let

   126         val popt = ef op_ t thy

   127         val _ = trace_calc2 "2.. get_pair: " t popt

   128       in case popt of SOME _ => popt | NONE =>

   129         let

   130           val popt = get_pair thy op_ ef t1

   131           val _ = trace_calc2 "3.. get_pair: " t1  popt

   132         in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end

   133       end

   134     else                                                                    (* search subterms *)

   135       let

   136         val popt = get_pair thy op_ ef t1

   137         val _ = trace_calc2 "4.. get_pair: " t popt

   138       in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end)

   139   | get_pair thy op_ ef (t as (Const (op0, _) $ t1 $ t2 $ t3)) =               (* ternary funs *)

   140     (trace_calc3 "get_pair 4a: t= "t;

   141     trace_calc1 "get_pair 4a: op_= " op_;

   142     trace_calc1 "get_pair 4a: op0= " op0;

   143     if op_ = op0 then

   144       case ef op_ t thy of st as SOME _ => st | NONE =>

   145         (case get_pair thy op_ ef t2 of st as SOME _ => st | NONE => get_pair thy op_ ef t3)

   146     else

   147       (case get_pair thy op_ ef t1 of st as SOME _ => st | NONE =>

   148         (case get_pair thy op_ ef t2 of st as SOME _ => st | NONE => get_pair thy op_ ef t3)))

   149   | get_pair thy op_ ef (Abs (_, _, body)) = get_pair thy op_ ef body

   150   | get_pair thy op_ ef (t1 $ t2) =

   151     let

   152       val _ = trace_calc4 "5.. get_pair t1 $ t2: " t1 t2;

   153       val popt = get_pair thy op_ ef t1

   154     in case popt of SOME _ => popt

   155       | NONE => (trace_calc0 "### get_pair: t1 $ t2 -> NONE"; get_pair thy op_ ef t2)

   156     end

   157   | get_pair _ _ _ _ = NONE

   159 (* get a thm from an op_ somewhere in the term;

   160    apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711) *)

   161 fun adhoc_thm thy (op_, eval_fn) ct =

   162   case get_pair thy op_ eval_fn ct of

   163     NONE => NONE

   164   | SOME (thmid, t) => SOME (thmid, ThmC_Def.make_thm thy t);

   166 (* get a thm applying an op_ to a term;

   167    apply ONLY to (numbers_to_string term), numbers_to_string (- 4711) --> (-4711) *)

   168 fun adhoc_thm1_ thy (op_, eval_fn) ct =

   169   case eval_fn op_ ct thy of

   170 	  NONE => NONE

   171   | SOME (thmid,t) => SOME (thmid, ThmC_Def.make_thm thy t);

   173 (** for ordered and conditional rewriting **)

   175 fun mk_rule (prems, l, r) =

   176     HOLogic.Trueprop $ (Logic.list_implies (prems, TermC.mk_equality (l, r)));

   178 (* 'norms' a rule, e.g.

   179 (*1*) from a = 1 ==> a*(b+c) = b+c

   180       to   a = 1 ==> a*(b+c) = b+c                     no change

   181 (*2*) from t = t

   182       to  (t = t) = True                               !!

   183 (*3*) from [| k < l; m + l = k + n |] ==> m < n

   184       to   [| k < l; m + l = k + n |] ==> m < n = True !! *)

   185 fun norm rule =

   186   let

   187     val (prems, concl) =

   188       (map TermC.strip_trueprop (Logic.strip_imp_prems rule),

   189         (TermC.strip_trueprop o  Logic.strip_imp_concl) rule)

   190   in

   191     if TermC.is_equality concl

   192     then

   193       let val (l, r) = TermC.dest_equals concl

   194       in

   195         if l = r then (*2*) mk_rule (prems, concl, @{term True}) else (*1*) rule

   196       end

   197     else (*3*) mk_rule (prems, concl, @{term True})

   198   end;

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

   201 fun numeral (Free (str, _)) =

   202     (case ThmC_Def.int_opt_of_string str of

   203 	 SOME i => SOME ((i, 0), (0, 0))

   204        | NONE => NONE)

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

   206 		   (Const ("Product_Type.Pair", _) $

   207 			  (Const ("Product_Type.Pair", _) $ Free (v1, _) $ Free (v2,_)) $

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

   209     (case (ThmC_Def.int_opt_of_string v1, ThmC_Def.int_opt_of_string v2, ThmC_Def.int_opt_of_string p1, ThmC_Def.int_opt_of_string p2) of

   210 	(SOME v1', SOME v2', SOME p1', SOME p2') =>

   211 	SOME ((v1', v2'), (p1', p2'))

   212       | _ => NONE)

   213   | numeral _ = NONE;

   215 (*** handle numerals in eval_binop ***)

   216 (* TODO rebuild fun calcul, fun term_of_float,fun var_op_float, fun float_op_var:

   217    Float ((a, b), _:int * int, (c, d), _:int * int) has been deleted already *)

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

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

   221 fun calcul "Groups.plus_class.plus" ((a, b), _:int * int) ((c, d), _:int * int)  = (*FIXME.WN1008 drop Float.calc, var_op_float, float_op_var, term_of_float*)

   222     if b < d

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

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

   225   | calcul "Groups.minus_class.minus" ((a, 0), _) ((c, 0), _) =       (*FIXXXME float + prec.*)

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

   227   | calcul "Groups.times_class.times" ((a, b), _) ((c, d), _) =       (*FIXXXME precision*)

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

   229   | calcul "Rings.divide_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)

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

   231   | calcul "Prog_Expr.pow" ((a, _), _) ((c, _), _) = (*FIXXXME Float + prec.*)

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

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

   234     error ("calcul: not impl. for Float (("^

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

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

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

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

   239 (*> calcul "Groups.plus_class.plus" ((~1,0),(0,0)) ((2,0),(0,0));

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

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

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

   244     TermC.term_of_num T val1

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

   246     let val pT = TermC.pairT T T

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

   248 	     $ (TermC.pairt (TermC.pairt (Free (TermC.str_of_int val1, T))

   249 			     (Free (TermC.str_of_int val2, T)))

   250 		      (TermC.pairt (Free (TermC.str_of_int precision1, T))

   251 			     (Free (TermC.str_of_int precision2, T))))

   252     end;

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

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

   255 > atomtyp fT;

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

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

   258 > atomtyp ffT;

   259 > fT = ffT;

   260 val it = true : bool

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

   263 val it = true : bool*)

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

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

   267     TermC.mk_var_op_num v op_ optype ntyp v1

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

   269     let val pT = TermC.pairT T T

   270     in Const (op_, optype) $ v $

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

   272 		    $ (TermC.pairt (TermC.pairt (Free (TermC.str_of_int v1, T))

   273 				    (Free (TermC.str_of_int v2, T)))

   274 			     (TermC.pairt (Free (TermC.str_of_int p1, T))

   275 				    (Free (TermC.str_of_int p2, T)))))

   276     end;

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

   278 > val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;

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

   280 > t = var_op_float v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));

   281 val it = true : bool*)

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

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

   285     TermC.mk_num_op_var v op_ optype ntyp v1

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

   287     let val pT = TermC.pairT T T

   288     in Const (op_, optype) $

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

   290 		    $ (TermC.pairt (TermC.pairt (Free (TermC.str_of_int v1, T))

   291 				    (Free (TermC.str_of_int v2, T)))

   292 			     (TermC.pairt (Free (TermC.str_of_int p1, T))

   293 				    (Free (TermC.str_of_int p2, T))))) $ v

   294     end;

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

   296 > val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;

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

   298 > t = float_op_var v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));

   299 val it = true : bool*)

   301 end

author	Walther Neuper <walther.neuper@jku.at>
	Wed, 29 Apr 2020 09:03:01 +0200
changeset 59919	3a7fb975af9d
parent 59902	e7910a62eaf2
child 59962	6a59d252345d
permissions	-rw-r--r--