1.1 --- a/TODO.md Mon Jul 19 18:29:46 2021 +0200
1.2 +++ b/TODO.md Mon Jul 19 18:39:02 2021 +0200
1.3 @@ -67,7 +67,6 @@
1.4 + TOODOO are exclusive for this changeset; most follow from TOODOO.1
1.5 + TOODOO.1: exception TYPE raised by Skip_Proof.make_thm
1.6 + ? how to do algebraic operations on numerals ? Presburger ? simplifier ?
1.7 - + clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");
1.8
1.9 * WN: DONE cleanup remaining ^^^ in comments (but sometimes it is just ASCII art), partially;
1.10 Left ^^^ in doc-isac (old master-theses, etc: "x^^^#2 + #8" ... # are left, too)
2.1 --- a/src/Tools/isac/ProgLang/Calculate.thy Mon Jul 19 18:29:46 2021 +0200
2.2 +++ b/src/Tools/isac/ProgLang/Calculate.thy Mon Jul 19 18:39:02 2021 +0200
2.3 @@ -13,8 +13,7 @@
2.4 Since that time numeral calculations are done by ML functions, all named eval_
2.5 and integrated into rewriting. eval_binop below is not bound to a specific constant
2.6 (like in Prog_Expr.thy), rather calculates results of Isabelle's binary operations + - * / ^.
2.7 - Nowadays the code in Calculate.thy and evaluate.sml should be replaced by native Isabelle
2.8 - code.
2.9 +
2.10 A specialty are the ad-hoc theorems for numeral calculations created in order to provide
2.11 the rewrite engine with theorems as done in general.
2.12 \<close>
3.1 --- a/src/Tools/isac/ProgLang/evaluate.sml Mon Jul 19 18:29:46 2021 +0200
3.2 +++ b/src/Tools/isac/ProgLang/evaluate.sml Mon Jul 19 18:39:02 2021 +0200
3.3 @@ -7,7 +7,6 @@
3.4
3.5 signature EVALUATE =
3.6 sig
3.7 - type float
3.8 val calc_equ: string -> int * int -> bool
3.9 val power: int -> int -> int
3.10 val sign_mult: int -> int -> int
3.11 @@ -19,15 +18,7 @@
3.12 val adhoc_thm1_: theory -> Eval_Def.cal -> term -> (string * thm) option
3.13 val norm: term -> term
3.14 val popt2str: ('a * term) option -> string
3.15 -(** )
3.16 - val numeral: term -> ((int * int) * (int * int)) option
3.17 -( **)
3.18 val calcul: string -> term * term -> term
3.19 -(** )
3.20 - val term_of_float: typ -> float -> term
3.21 - val var_op_float: term -> string -> typ -> typ ->float -> term
3.22 - val float_op_var: term -> string -> typ -> typ -> float -> term
3.23 -( **)
3.24 val trace_on: bool Unsynchronized.ref
3.25 val int_of_numeral: term -> int
3.26 \<^isac_test>\<open>
3.27 @@ -43,10 +34,6 @@
3.28 struct
3.29 (**)
3.30
3.31 -type float =
3.32 - (int * int) (* value: significand * exponent *)
3.33 - * (int * int); (* precision: significand * exponent *)
3.34 -
3.35 (* trace internal steps of isac's numeral calculations *)
3.36 val trace_on = Unsynchronized.ref false;
3.37
3.38 @@ -208,22 +195,6 @@
3.39 else (*3*) mk_rule (prems, concl, @{term True})
3.40 end;
3.41
3.42 -(* convert int and float to internal floatingpoint prepresentation *)
3.43 -(** )
3.44 -fun numeral (Free (str, _)) =
3.45 - (case ThmC_Def.int_opt_of_string str of
3.46 - SOME i => SOME ((i, 0), (0, 0))
3.47 - | NONE => NONE)
3.48 - | numeral (Const ("Float.Float", _) $
3.49 - (Const ("Product_Type.Pair", _) $
3.50 - (Const ("Product_Type.Pair", _) $ Free (v1, _) $ Free (v2,_)) $
3.51 - (Const ("Product_Type.Pair", _) $ Free (p1, _) $ Free (p2,_)))) =
3.52 - (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
3.53 - (SOME v1', SOME v2', SOME p1', SOME p2') => SOME ((v1', v2'), (p1', p2'))
3.54 - | _ => NONE)
3.55 - | numeral _ = NONE;
3.56 -( **)
3.57 -
3.58 (*** handle numerals in eval_binop ***)
3.59
3.60 (* preliminary HACK *)
3.61 @@ -246,51 +217,6 @@
3.62 | str => raise ERROR ("calcul not impl.for op_ " ^ str)
3.63 in HOLogic.mk_number T result end;
3.64
3.65 -(*.convert internal floatingpoint prepresentation to int and float.*)
3.66 -(** )
3.67 -fun term_of_float T ((val1, 0), ( 0, 0)) =
3.68 - TermC.term_of_num T val1
3.69 - | term_of_float T ((val1, val2), (precision1, precision2)) =
3.70 - let val pT = TermC.pairT T T
3.71 - in Const ("Float.Float", (TermC.pairT pT pT) --> T)
3.72 - $ (TermC.pairt (TermC.pairt (Free (TermC.str_of_int val1, T))
3.73 - (Free (TermC.str_of_int val2, T)))
3.74 - (TermC.pairt (Free (TermC.str_of_int precision1, T))
3.75 - (Free (TermC.str_of_int precision2, T))))
3.76 - end;
3.77 -( **)
3.78 -(*> val t = str2term "Float ((1,2),(0,0))";
3.79 -> val Const ("Float.Float", fT) $ _ = t;
3.80 -> atomtyp fT;
3.81 -> val ffT = (pairT (pairT HOLogic.realT HOLogic.realT)
3.82 -> (pairT HOLogic.realT HOLogic.realT)) --> HOLogic.realT;
3.83 -> atomtyp ffT;
3.84 -> fT = ffT;
3.85 -val it = true : bool
3.86 -
3.87 -t = float_term_of_num HOLogic.realT ((1,2),(0,0));
3.88 -val it = true : bool*)
3.89 -
3.90 -(*.assoc. convert internal floatingpoint prepresentation to int and float.*)
3.91 -(** )
3.92 -fun var_op_float v op_ optype ntyp ((v1, 0), (0, 0)) =
3.93 - TermC.mk_var_op_num v op_ optype ntyp v1
3.94 - | var_op_float v op_ optype T ((v1, v2), (p1, p2)) =
3.95 - let val pT = TermC.pairT T T
3.96 - in Const (op_, optype) $ v $
3.97 - (Const ("Float.Float", (TermC.pairT pT pT) --> T)
3.98 - $ (TermC.pairt (TermC.pairt (Free (TermC.str_of_int v1, T))
3.99 - (Free (TermC.str_of_int v2, T)))
3.100 - (TermC.pairt (Free (TermC.str_of_int p1, T))
3.101 - (Free (TermC.str_of_int p2, T)))))
3.102 - end;
3.103 -( **)
3.104 -(*> val t = str2term "a + b";
3.105 -> val Const (\<^const_name>\<open>plus\<close>, optype) $ _ $ _ = t;
3.106 -> val t = str2term "v + Float ((11,-1),(0,0))";val v = str2term "v";
3.107 -> t = var_op_float v \<^const_name>\<open>plus\<close> optype HOLogic.realT ((11,~1),(0,0));
3.108 -val it = true : bool*)
3.109 -
3.110 end
3.111
3.112