uniform use of Integer.min/max;
authorwenzelm
Tue Oct 20 20:54:31 2009 +0200 (2009-10-20)
changeset 330292fefe039edf1
parent 33028 9aa8bfb1649d
child 33030 2f4b36efa95e
uniform use of Integer.min/max;
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
src/HOL/SMT/Tools/z3_proof_terms.ML
src/HOL/Tools/Function/scnp_solve.ML
src/HOL/Tools/Groebner_Basis/groebner.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/prop_logic.ML
src/HOL/Tools/quickcheck_generators.ML
src/HOL/Tools/record.ML
src/HOL/Tools/res_hol_clause.ML
src/HOL/ex/predicate_compile.ML
src/Provers/splitter.ML
src/Pure/General/integer.ML
src/Pure/Tools/find_theorems.ML
src/Pure/meta_simplifier.ML
src/Tools/Code/code_thingol.ML
src/Tools/atomize_elim.ML
     1.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Tue Oct 20 20:03:23 2009 +0200
     1.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Tue Oct 20 20:54:31 2009 +0200
     1.3 @@ -21,8 +21,8 @@
     1.4  val rat_2 = Rat.two;
     1.5  val rat_10 = Rat.rat_of_int 10;
     1.6  val rat_1_2 = rat_1 // rat_2;
     1.7 -val max = curry Int.max;
     1.8 -val min = curry Int.min;
     1.9 +val max = Integer.max;
    1.10 +val min = Integer.min;
    1.11  
    1.12  val denominator_rat = Rat.quotient_of_rat #> snd #> Rat.rat_of_int;
    1.13  val numerator_rat = Rat.quotient_of_rat #> fst #> Rat.rat_of_int;
     2.1 --- a/src/HOL/SMT/Tools/z3_proof_terms.ML	Tue Oct 20 20:03:23 2009 +0200
     2.2 +++ b/src/HOL/SMT/Tools/z3_proof_terms.ML	Tue Oct 20 20:54:31 2009 +0200
     2.3 @@ -89,7 +89,7 @@
     2.4  local
     2.5  fun mk_inst nctxt cert vs =
     2.6    let
     2.7 -    val max = fold (curry Int.max o fst) vs 0
     2.8 +    val max = fold (Integer.max o fst) vs 0
     2.9      val names = fst (Name.variants (replicate (max + 1) var_prefix) nctxt)
    2.10      fun mk (i, v) = (v, cert (Free (nth names i, #T (Thm.rep_cterm v))))
    2.11    in map mk vs end
     3.1 --- a/src/HOL/Tools/Function/scnp_solve.ML	Tue Oct 20 20:03:23 2009 +0200
     3.2 +++ b/src/HOL/Tools/Function/scnp_solve.ML	Tue Oct 20 20:54:31 2009 +0200
     3.3 @@ -79,7 +79,7 @@
     3.4  fun var_constrs (gp as GP (arities, gl)) =
     3.5    let
     3.6      val n = Int.max (num_graphs gp, num_prog_pts gp)
     3.7 -    val k = List.foldl Int.max 1 arities
     3.8 +    val k = fold Integer.max arities 1
     3.9  
    3.10      (* Injective, provided  a < 8, x < n, and i < k. *)
    3.11      fun prod a x i j = ((j * k + i) * n + x) * 8 + a + 1
     4.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Tue Oct 20 20:03:23 2009 +0200
     4.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Tue Oct 20 20:54:31 2009 +0200
     4.3 @@ -380,7 +380,7 @@
     4.4          val pol' = augment pol
     4.5          val allpols = (grob_sub (grob_mul grob_z pol') grob_1)::pols'
     4.6          val (l,cert) = grobner_weak vars' allpols
     4.7 -        val d = fold_rev (fold_rev (curry Int.max o hd o snd) o snd) cert 0
     4.8 +        val d = fold (fold (Integer.max o hd o snd) o snd) cert 0
     4.9          fun transform_monomial (c,m) =
    4.10              grob_cmul (c,tl m) (grob_pow vars pol (d - hd m))
    4.11          fun transform_polynomial q = fold_rev (grob_add o transform_monomial) q []
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 20 20:03:23 2009 +0200
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 20 20:54:31 2009 +0200
     5.3 @@ -615,7 +615,7 @@
     5.4  fun guess_nparams T =
     5.5    let
     5.6      val argTs = binder_types T
     5.7 -    val nparams = fold (curry Int.max)
     5.8 +    val nparams = fold Integer.max
     5.9        (map (fn x => x + 1) (find_indexes is_predT argTs)) 0
    5.10    in nparams end;
    5.11  
     6.1 --- a/src/HOL/Tools/prop_logic.ML	Tue Oct 20 20:03:23 2009 +0200
     6.2 +++ b/src/HOL/Tools/prop_logic.ML	Tue Oct 20 20:54:31 2009 +0200
     6.3 @@ -387,7 +387,7 @@
     6.4  			if !next_idx_is_valid then
     6.5  				Unsynchronized.inc next_idx
     6.6  			else (
     6.7 -				next_idx          := Termtab.fold (curry Int.max o snd) table 0;
     6.8 +				next_idx := Termtab.fold (Integer.max o snd) table 0;
     6.9  				next_idx_is_valid := true;
    6.10  				Unsynchronized.inc next_idx
    6.11  			)
     7.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Tue Oct 20 20:03:23 2009 +0200
     7.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Tue Oct 20 20:54:31 2009 +0200
     7.3 @@ -256,7 +256,7 @@
     7.4          val T = termifyT simpleT;
     7.5          val tTs = (map o apsnd) termifyT simple_tTs;
     7.6          val is_rec = exists is_some ks;
     7.7 -        val k = fold (fn NONE => I | SOME k => curry Int.max k) ks 0;
     7.8 +        val k = fold (fn NONE => I | SOME k => Integer.max k) ks 0;
     7.9          val vs = Name.names Name.context "x" (map snd simple_tTs);
    7.10          val vs' = (map o apsnd) termifyT vs;
    7.11          val tc = HOLogic.mk_return T @{typ Random.seed}
     8.1 --- a/src/HOL/Tools/record.ML	Tue Oct 20 20:03:23 2009 +0200
     8.2 +++ b/src/HOL/Tools/record.ML	Tue Oct 20 20:54:31 2009 +0200
     8.3 @@ -750,7 +750,7 @@
     8.4                      val types = map snd flds';
     8.5                      val (args, rest) = splitargs (map fst flds') fargs;
     8.6                      val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
     8.7 -                    val midx = fold (fn T => fn i => Int.max (maxidx_of_typ T, i)) argtypes 0;
     8.8 +                    val midx = fold Term.maxidx_typ argtypes 0;
     8.9                      val varifyT = varifyT midx;
    8.10                      val vartypes = map varifyT types;
    8.11  
     9.1 --- a/src/HOL/Tools/res_hol_clause.ML	Tue Oct 20 20:03:23 2009 +0200
     9.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Tue Oct 20 20:54:31 2009 +0200
     9.3 @@ -437,7 +437,7 @@
     9.4        case head of
     9.5            CombConst (a,_,_) => (*predicate or function version of "equal"?*)
     9.6              let val a = if a="equal" andalso not toplev then "c_fequal" else a
     9.7 -            val const_min_arity = Symtab.map_default (a,n) (curry Int.min n) const_min_arity
     9.8 +            val const_min_arity = Symtab.map_default (a, n) (Integer.min n) const_min_arity
     9.9              in
    9.10                if toplev then (const_min_arity, const_needs_hBOOL)
    9.11                else (const_min_arity, Symtab.update (a,true) (const_needs_hBOOL))
    10.1 --- a/src/HOL/ex/predicate_compile.ML	Tue Oct 20 20:03:23 2009 +0200
    10.2 +++ b/src/HOL/ex/predicate_compile.ML	Tue Oct 20 20:54:31 2009 +0200
    10.3 @@ -542,7 +542,7 @@
    10.4  fun guess_nparams T =
    10.5    let
    10.6      val argTs = binder_types T
    10.7 -    val nparams = fold (curry Int.max)
    10.8 +    val nparams = fold Integer.max
    10.9        (map (fn x => x + 1) (find_indexes is_predT argTs)) 0
   10.10    in nparams end;
   10.11  
    11.1 --- a/src/Provers/splitter.ML	Tue Oct 20 20:03:23 2009 +0200
    11.2 +++ b/src/Provers/splitter.ML	Tue Oct 20 20:54:31 2009 +0200
    11.3 @@ -159,9 +159,9 @@
    11.4  (* check if the innermost abstraction that needs to be removed
    11.5     has a body of type T; otherwise the expansion thm will fail later on
    11.6  *)
    11.7 -fun type_test (T,lbnos,apsns) =
    11.8 -  let val (_,U: typ,_) = List.nth(apsns, Library.foldl Int.min (hd lbnos, tl lbnos))
    11.9 -  in T=U end;
   11.10 +fun type_test (T, lbnos, apsns) =
   11.11 +  let val (_, U: typ, _) = List.nth (apsns, foldl1 Int.min lbnos)
   11.12 +  in T = U end;
   11.13  
   11.14  (*************************************************************************
   11.15     Create a "split_pack".
    12.1 --- a/src/Pure/General/integer.ML	Tue Oct 20 20:03:23 2009 +0200
    12.2 +++ b/src/Pure/General/integer.ML	Tue Oct 20 20:54:31 2009 +0200
    12.3 @@ -6,6 +6,8 @@
    12.4  
    12.5  signature INTEGER =
    12.6  sig
    12.7 +  val min: int -> int -> int
    12.8 +  val max: int -> int -> int
    12.9    val add: int -> int -> int
   12.10    val mult: int -> int -> int
   12.11    val sum: int list -> int
   12.12 @@ -23,6 +25,9 @@
   12.13  structure Integer : INTEGER =
   12.14  struct
   12.15  
   12.16 +fun min x y = Int.min (x, y);
   12.17 +fun max x y = Int.max (x, y);
   12.18 +
   12.19  fun add x y = x + y;
   12.20  fun mult x y = x * y;
   12.21  
    13.1 --- a/src/Pure/Tools/find_theorems.ML	Tue Oct 20 20:03:23 2009 +0200
    13.2 +++ b/src/Pure/Tools/find_theorems.ML	Tue Oct 20 20:54:31 2009 +0200
    13.3 @@ -109,7 +109,7 @@
    13.4        in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end;
    13.5  
    13.6      fun bestmatch [] = NONE
    13.7 -      | bestmatch xs = SOME (foldr1 Int.min xs);
    13.8 +      | bestmatch xs = SOME (foldl1 Int.min xs);
    13.9  
   13.10      val match_thm = matches o refine_term;
   13.11    in
   13.12 @@ -142,7 +142,7 @@
   13.13      (*dest rules always have assumptions, so a dest with one
   13.14        assumption is as good as an intro rule with none*)
   13.15      if not (null successful)
   13.16 -    then SOME (Thm.nprems_of thm - 1, foldr1 Int.min successful) else NONE
   13.17 +    then SOME (Thm.nprems_of thm - 1, foldl1 Int.min successful) else NONE
   13.18    end;
   13.19  
   13.20  fun filter_intro doiff ctxt goal (_, thm) =
   13.21 @@ -173,7 +173,7 @@
   13.22          assumption is as good as an intro rule with none*)
   13.23        if is_nontrivial (ProofContext.theory_of ctxt) (Thm.major_prem_of thm)
   13.24          andalso not (null successful)
   13.25 -      then SOME (Thm.nprems_of thm - 1, foldr1 Int.min successful) else NONE
   13.26 +      then SOME (Thm.nprems_of thm - 1, foldl1 Int.min successful) else NONE
   13.27      end
   13.28    else NONE
   13.29  
    14.1 --- a/src/Pure/meta_simplifier.ML	Tue Oct 20 20:03:23 2009 +0200
    14.2 +++ b/src/Pure/meta_simplifier.ML	Tue Oct 20 20:54:31 2009 +0200
    14.3 @@ -1158,8 +1158,8 @@
    14.4              let
    14.5                val prem' = Thm.rhs_of eqn;
    14.6                val tprems = map term_of prems;
    14.7 -              val i = 1 + Library.foldl Int.max (~1, map (fn p =>
    14.8 -                find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn)));
    14.9 +              val i = 1 + fold Integer.max (map (fn p =>
   14.10 +                find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn))) ~1;
   14.11                val (rrs', asm') = rules_of_prem ss prem'
   14.12              in mut_impc prems concl rrss asms (prem' :: prems')
   14.13                (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
    15.1 --- a/src/Tools/Code/code_thingol.ML	Tue Oct 20 20:03:23 2009 +0200
    15.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Oct 20 20:54:31 2009 +0200
    15.3 @@ -420,7 +420,7 @@
    15.4  fun same_arity thy thms =
    15.5    let
    15.6      val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
    15.7 -    val k = fold (curry Int.max o num_args_of o Thm.prop_of) thms 0;
    15.8 +    val k = fold (Integer.max o num_args_of o Thm.prop_of) thms 0;
    15.9    in map (expand_eta thy k) thms end;
   15.10  
   15.11  fun mk_desymbolization pre post mk vs =
    16.1 --- a/src/Tools/atomize_elim.ML	Tue Oct 20 20:03:23 2009 +0200
    16.2 +++ b/src/Tools/atomize_elim.ML	Tue Oct 20 20:54:31 2009 +0200
    16.3 @@ -34,7 +34,7 @@
    16.4  
    16.5  (* Compute inverse permutation *)
    16.6  fun invert_perm pi =
    16.7 -      (pi @ ((0 upto (fold (curry Int.max) pi 0)) \\ pi))
    16.8 +      (pi @ ((0 upto (fold Integer.max pi 0)) \\ pi))
    16.9             |> map_index I
   16.10             |> sort (int_ord o pairself snd)
   16.11             |> map fst