uniform use of Integer.add/mult/sum/prod;
authorwenzelm
Mon Oct 19 21:54:57 2009 +0200 (2009-10-19)
changeset 33002f3f02f36a3e2
parent 33001 82382652e5e7
child 33003 1c93cfa807bc
uniform use of Integer.add/mult/sum/prod;
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Tools/Datatype/datatype_codegen.ML
src/HOL/Tools/Function/fundef_datatype.ML
src/HOL/Tools/Function/scnp_solve.ML
src/HOL/Tools/Groebner_Basis/normalizer.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/refute.ML
src/Provers/Arith/fast_lin_arith.ML
src/Pure/General/integer.ML
src/Tools/atomize_elim.ML
src/Tools/nbe.ML
     1.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Mon Oct 19 16:47:21 2009 +0200
     1.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Mon Oct 19 21:54:57 2009 +0200
     1.3 @@ -223,7 +223,7 @@
     1.4  fun monomial_var x = FuncUtil.Ctermfunc.onefunc (x, 1);
     1.5  
     1.6  val monomial_mul =
     1.7 -  FuncUtil.Ctermfunc.combine (curry op +) (K false);
     1.8 +  FuncUtil.Ctermfunc.combine Integer.add (K false);
     1.9  
    1.10  fun monomial_pow m k =
    1.11    if k = 0 then monomial_1
    1.12 @@ -233,7 +233,7 @@
    1.13    FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => FuncUtil.Ctermfunc.tryapplyd m2 x 0 >= k andalso a) m1 true;;
    1.14  
    1.15  fun monomial_div m1 m2 =
    1.16 - let val m = FuncUtil.Ctermfunc.combine (curry op +)
    1.17 + let val m = FuncUtil.Ctermfunc.combine Integer.add
    1.18     (fn x => x = 0) m1 (FuncUtil.Ctermfunc.map (fn x => ~ x) m2)
    1.19   in if FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => k >= 0 andalso a) m true then m
    1.20    else error "monomial_div: non-divisible"
     2.1 --- a/src/HOL/Library/positivstellensatz.ML	Mon Oct 19 16:47:21 2009 +0200
     2.2 +++ b/src/HOL/Library/positivstellensatz.ML	Mon Oct 19 21:54:57 2009 +0200
     2.3 @@ -83,8 +83,8 @@
     2.4   else
     2.5    let val mon1 = dest_monomial m1 
     2.6        val mon2 = dest_monomial m2
     2.7 -      val deg1 = fold (curry op + o snd) mon1 0
     2.8 -      val deg2 = fold (curry op + o snd) mon2 0 
     2.9 +      val deg1 = fold (Integer.add o snd) mon1 0
    2.10 +      val deg2 = fold (Integer.add o snd) mon2 0 
    2.11    in if deg1 < deg2 then GREATER else if deg1 > deg2 then LESS
    2.12       else list_ord (prod_ord cterm_ord int_ord) (mon1,mon2)
    2.13    end;
     3.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Oct 19 16:47:21 2009 +0200
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Oct 19 21:54:57 2009 +0200
     3.3 @@ -22,7 +22,7 @@
     3.4      val (_, _, constrs) = the (AList.lookup (op =) descr i);
     3.5      fun arg_nonempty (_, DatatypeAux.DtRec i) = if member (op =) is i
     3.6            then NONE
     3.7 -          else Option.map (curry op + 1 o snd) (find_nonempty descr (i::is) i)
     3.8 +          else Option.map (Integer.add 1 o snd) (find_nonempty descr (i::is) i)
     3.9        | arg_nonempty _ = SOME 0;
    3.10      fun max xs = Library.foldl
    3.11        (fn (NONE, _) => NONE
     4.1 --- a/src/HOL/Tools/Function/fundef_datatype.ML	Mon Oct 19 16:47:21 2009 +0200
     4.2 +++ b/src/HOL/Tools/Function/fundef_datatype.ML	Mon Oct 19 21:54:57 2009 +0200
     4.3 @@ -54,7 +54,7 @@
     4.4        val _ = map check_constr_pattern args
     4.5                    
     4.6                    (* just count occurrences to check linearity *)
     4.7 -      val _ = if fold (fold_aterms (fn Bound _ => curry (op +) 1 | _ => I)) args 0 > length qs
     4.8 +      val _ = if fold (fold_aterms (fn Bound _ => Integer.add 1 | _ => I)) args 0 > length qs
     4.9                then err "Nonlinear patterns" else ()
    4.10      in
    4.11        ()
     5.1 --- a/src/HOL/Tools/Function/scnp_solve.ML	Mon Oct 19 16:47:21 2009 +0200
     5.2 +++ b/src/HOL/Tools/Function/scnp_solve.ML	Mon Oct 19 21:54:57 2009 +0200
     5.3 @@ -46,7 +46,7 @@
     5.4  fun num_prog_pts (GP (arities, _)) = length arities ;
     5.5  fun num_graphs (GP (_, gs)) = length gs ;
     5.6  fun arity (GP (arities, gl)) i = nth arities i ;
     5.7 -fun ndigits (GP (arities, _)) = IntInf.log2 (List.foldl (op +) 0 arities) + 1
     5.8 +fun ndigits (GP (arities, _)) = IntInf.log2 (Integer.sum arities) + 1
     5.9  
    5.10  
    5.11  (** Propositional formulas **)
     6.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Mon Oct 19 16:47:21 2009 +0200
     6.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Mon Oct 19 21:54:57 2009 +0200
     6.3 @@ -391,8 +391,8 @@
     6.4   in fn tm1 => fn tm2 =>
     6.5    let val vdegs1 = map dest_varpow (powervars tm1)
     6.6        val vdegs2 = map dest_varpow (powervars tm2)
     6.7 -      val deg1 = fold_rev ((curry (op +)) o snd) vdegs1 num_0
     6.8 -      val deg2 = fold_rev ((curry (op +)) o snd) vdegs2 num_0
     6.9 +      val deg1 = fold (Integer.add o snd) vdegs1 num_0
    6.10 +      val deg2 = fold (Integer.add o snd) vdegs2 num_0
    6.11    in if deg1 < deg2 then ~1 else if deg1 > deg2 then 1
    6.12                              else lexorder vdegs1 vdegs2
    6.13    end
     7.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Mon Oct 19 16:47:21 2009 +0200
     7.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Oct 19 21:54:57 2009 +0200
     7.3 @@ -188,7 +188,7 @@
     7.4      (Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c1 $ x1) $ r1,
     7.5      Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c2 $ x2) $ r2) =>
     7.6     if x1 = x2 then
     7.7 -     let val c = numeral2 (curry op +) c1 c2
     7.8 +     let val c = numeral2 Integer.add c1 c2
     7.9        in if c = zero then linear_add vars r1 r2
    7.10           else addC$(mulC$c$x1)$(linear_add vars r1 r2)
    7.11       end
    7.12 @@ -198,7 +198,7 @@
    7.13        addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
    7.14   | (_, Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c2 $ x2) $ r2) =>
    7.15        addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
    7.16 - | (_, _) => numeral2 (curry op +) tm1 tm2;
    7.17 + | (_, _) => numeral2 Integer.add tm1 tm2;
    7.18  
    7.19  fun linear_neg tm = linear_cmul ~1 tm;
    7.20  fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2);
     8.1 --- a/src/HOL/Tools/refute.ML	Mon Oct 19 16:47:21 2009 +0200
     8.2 +++ b/src/HOL/Tools/refute.ML	Mon Oct 19 21:54:57 2009 +0200
     8.3 @@ -1616,30 +1616,14 @@
     8.4    end;
     8.5  
     8.6  (* ------------------------------------------------------------------------- *)
     8.7 -(* sum: returns the sum of a list 'xs' of integers                           *)
     8.8 -(* ------------------------------------------------------------------------- *)
     8.9 -
    8.10 -  (* int list -> int *)
    8.11 -
    8.12 -  fun sum xs = List.foldl op+ 0 xs;
    8.13 -
    8.14 -(* ------------------------------------------------------------------------- *)
    8.15 -(* product: returns the product of a list 'xs' of integers                   *)
    8.16 -(* ------------------------------------------------------------------------- *)
    8.17 -
    8.18 -  (* int list -> int *)
    8.19 -
    8.20 -  fun product xs = List.foldl op* 1 xs;
    8.21 -
    8.22 -(* ------------------------------------------------------------------------- *)
    8.23  (* size_of_dtyp: the size of (an initial fragment of) an inductive data type *)
    8.24  (*               is the sum (over its constructors) of the product (over     *)
    8.25  (*               their arguments) of the size of the argument types          *)
    8.26  (* ------------------------------------------------------------------------- *)
    8.27  
    8.28    fun size_of_dtyp thy typ_sizes descr typ_assoc constructors =
    8.29 -    sum (map (fn (_, dtyps) =>
    8.30 -      product (map (size_of_type thy (typ_sizes, []) o
    8.31 +    Integer.sum (map (fn (_, dtyps) =>
    8.32 +      Integer.prod (map (size_of_type thy (typ_sizes, []) o
    8.33          (typ_of_dtyp descr typ_assoc)) dtyps))
    8.34            constructors);
    8.35  
    8.36 @@ -2326,8 +2310,8 @@
    8.37              let
    8.38                (* number of all constructors, including those of different  *)
    8.39                (* (mutually recursive) datatypes within the same descriptor *)
    8.40 -              val mconstrs_count = sum (map (fn (_, (_, _, cs)) => length cs)
    8.41 -                (#descr info))
    8.42 +              val mconstrs_count =
    8.43 +                Integer.sum (map (fn (_, (_, _, cs)) => length cs) (#descr info))
    8.44              in
    8.45                if mconstrs_count < length params then
    8.46                  (* too many actual parameters; for now we'll use the *)
     9.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Mon Oct 19 16:47:21 2009 +0200
     9.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Mon Oct 19 21:54:57 2009 +0200
     9.3 @@ -301,14 +301,14 @@
     9.4    if n = 1 then i
     9.5    else if n = 0 andalso ty = Lt then sys_error "multiply_ineq"
     9.6    else if n < 0 andalso (ty=Le orelse ty=Lt) then sys_error "multiply_ineq"
     9.7 -  else Lineq (n * k, ty, map (curry op* n) l, Multiplied (n, just));
     9.8 +  else Lineq (n * k, ty, map (Integer.mult n) l, Multiplied (n, just));
     9.9  
    9.10  (* ------------------------------------------------------------------------- *)
    9.11  (* Add together (in)equations.                                               *)
    9.12  (* ------------------------------------------------------------------------- *)
    9.13  
    9.14  fun add_ineq (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) =
    9.15 -  let val l = map2 (curry (op +)) l1 l2
    9.16 +  let val l = map2 Integer.add l1 l2
    9.17    in Lineq(k1+k2,find_add_type(ty1,ty2),l,Added(just1,just2)) end;
    9.18  
    9.19  (* ------------------------------------------------------------------------- *)
    10.1 --- a/src/Pure/General/integer.ML	Mon Oct 19 16:47:21 2009 +0200
    10.2 +++ b/src/Pure/General/integer.ML	Mon Oct 19 21:54:57 2009 +0200
    10.3 @@ -1,13 +1,16 @@
    10.4  (*  Title:      Pure/General/integer.ML
    10.5      Author:     Florian Haftmann, TU Muenchen
    10.6  
    10.7 -Unbounded integers.
    10.8 +Auxiliary operations on (unbounded) integers.
    10.9  *)
   10.10  
   10.11  signature INTEGER =
   10.12  sig
   10.13 +  val add: int -> int -> int
   10.14 +  val mult: int -> int -> int
   10.15 +  val sum: int list -> int
   10.16 +  val prod: int list -> int
   10.17    val sign: int -> order
   10.18 -  val sum: int list -> int
   10.19    val div_mod: int -> int -> int * int
   10.20    val square: int -> int
   10.21    val pow: int -> int -> int (* exponent -> base -> result *)
   10.22 @@ -20,9 +23,13 @@
   10.23  structure Integer : INTEGER =
   10.24  struct
   10.25  
   10.26 -fun sign x = int_ord (x, 0);
   10.27 +fun add x y = x + y;
   10.28 +fun mult x y = x * y;
   10.29  
   10.30 -fun sum xs = fold (curry op +) xs 0;
   10.31 +fun sum xs = fold add xs 0;
   10.32 +fun prod xs = fold mult xs 1;
   10.33 +
   10.34 +fun sign x = int_ord (x, 0);
   10.35  
   10.36  fun div_mod x y = IntInf.divMod (x, y);
   10.37  
    11.1 --- a/src/Tools/atomize_elim.ML	Mon Oct 19 16:47:21 2009 +0200
    11.2 +++ b/src/Tools/atomize_elim.ML	Mon Oct 19 21:54:57 2009 +0200
    11.3 @@ -42,7 +42,7 @@
    11.4  (* rearrange_prems as a conversion *)
    11.5  fun rearrange_prems_conv pi ct =
    11.6      let
    11.7 -      val pi' = 0 :: map (curry op + 1) pi
    11.8 +      val pi' = 0 :: map (Integer.add 1) pi
    11.9        val fwd  = Thm.trivial ct
   11.10                    |> Drule.rearrange_prems pi'
   11.11        val back = Thm.trivial (snd (Thm.dest_implies (cprop_of fwd)))
    12.1 --- a/src/Tools/nbe.ML	Mon Oct 19 16:47:21 2009 +0200
    12.2 +++ b/src/Tools/nbe.ML	Mon Oct 19 21:54:57 2009 +0200
    12.3 @@ -303,7 +303,7 @@
    12.4      fun subst_nonlin_vars args =
    12.5        let
    12.6          val vs = (fold o Code_Thingol.fold_varnames)
    12.7 -          (fn v => AList.map_default (op =) (v, 0) (curry (op +) 1)) args [];
    12.8 +          (fn v => AList.map_default (op =) (v, 0) (Integer.add 1)) args [];
    12.9          val names = Name.make_context (map fst vs);
   12.10          fun declare v k ctxt = let val vs = Name.invents ctxt v k
   12.11            in (vs, fold Name.declare vs ctxt) end;