tuned signature;
authorwenzelm
Fri May 17 13:46:18 2013 +0200 (2013-05-17)
changeset 52049156e12d5cb92
parent 52048 9003b293e775
child 52050 b40ed9dcf903
tuned signature;
src/HOL/Library/positivstellensatz.ML
src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML
src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
src/HOL/Tools/sat_funcs.ML
src/HOL/Tools/sat_solver.ML
src/Pure/General/table.ML
src/Pure/envir.ML
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Fri May 17 11:35:52 2013 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Fri May 17 13:46:18 2013 +0200
     1.3 @@ -44,9 +44,10 @@
     1.4          in if z w then Tab.delete k t else Tab.update (k,w) t end;
     1.5    in Tab.fold h a b end;
     1.6  
     1.7 -fun choose f = case Tab.min_key f of
     1.8 -    SOME k => (k, the (Tab.lookup f k))
     1.9 -  | NONE => error "FuncFun.choose : Completely empty function"
    1.10 +fun choose f =
    1.11 +  (case Tab.min f of
    1.12 +    SOME entry => entry
    1.13 +  | NONE => error "FuncFun.choose : Completely empty function")
    1.14  
    1.15  fun onefunc kv = update kv empty
    1.16  
     2.1 --- a/src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML	Fri May 17 11:35:52 2013 +0200
     2.2 +++ b/src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML	Fri May 17 13:46:18 2013 +0200
     2.3 @@ -263,11 +263,11 @@
     2.4  fun m_elem_at m i = Inttab.lookup m i
     2.5  
     2.6  fun v_only_elem v =
     2.7 -    case Inttab.min_key v of
     2.8 +    case Inttab.min v of
     2.9          NONE => NONE
    2.10 -      | SOME vmin => (case Inttab.max_key v of
    2.11 +      | SOME (vmin, _) => (case Inttab.max v of
    2.12                            NONE => SOME vmin
    2.13 -                        | SOME vmax => if vmin = vmax then SOME vmin else NONE)
    2.14 +                        | SOME (vmax, _) => if vmin = vmax then SOME vmin else NONE)
    2.15  
    2.16  fun v_fold f = Inttab.fold f;
    2.17  fun m_fold f = Inttab.fold f;
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Fri May 17 11:35:52 2013 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Fri May 17 13:46:18 2013 +0200
     3.3 @@ -42,7 +42,7 @@
     3.4    (let val v = hd (Inttab.lookup_list tab key) in
     3.5      (v, Inttab.remove_list (op =) (key, v) tab)
     3.6    end) handle List.Empty => raise Fail "sledgehammer_compress: pop"
     3.7 -fun pop_max tab = pop tab (the (Inttab.max_key tab))
     3.8 +fun pop_max tab = pop tab (fst (the (Inttab.max tab)))
     3.9    handle Option.Option => raise Fail "sledgehammer_compress: pop_max"
    3.10  fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab
    3.11  
     4.1 --- a/src/HOL/Tools/sat_funcs.ML	Fri May 17 11:35:52 2013 +0200
     4.2 +++ b/src/HOL/Tools/sat_funcs.ML	Fri May 17 13:46:18 2013 +0200
     4.3 @@ -365,7 +365,7 @@
     4.4              (* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *)
     4.5              val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm
     4.6              (* initialize the clause array with the given clauses *)
     4.7 -            val max_idx = the (Inttab.max_key clause_table)
     4.8 +            val max_idx = fst (the (Inttab.max clause_table))
     4.9              val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
    4.10              val _ =
    4.11                fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1))
     5.1 --- a/src/HOL/Tools/sat_solver.ML	Fri May 17 11:35:52 2013 +0200
     5.2 +++ b/src/HOL/Tools/sat_solver.ML	Fri May 17 13:46:18 2013 +0200
     5.3 @@ -856,8 +856,8 @@
     5.4                val _   = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".")
     5.5                (* set 'clause_offset' to the largest used clause ID *)
     5.6                val _   = if !clause_offset = ~1 then clause_offset :=
     5.7 -                (case Inttab.max_key (!clause_table) of
     5.8 -                  SOME id => id
     5.9 +                (case Inttab.max (!clause_table) of
    5.10 +                  SOME (id, _) => id
    5.11                  | NONE => cnf_number_of_clauses (Prop_Logic.defcnf fm) - 1  (* the first clause ID is 0, not 1 *))
    5.12                  else
    5.13                    ()
    5.14 @@ -899,7 +899,7 @@
    5.15                (* for its literals to obtain the empty clause                *)
    5.16                val vids         = map (fn l => l div 2) ls
    5.17                val rs           = cid :: map (fn v => !clause_offset + v) vids
    5.18 -              val new_empty_id = the_default (!clause_offset) (Inttab.max_key (!clause_table)) + 1
    5.19 +              val new_empty_id = the_default (!clause_offset) (Option.map fst (Inttab.max (!clause_table))) + 1
    5.20              in
    5.21                (* update clause table and conflict id *)
    5.22                clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table)
     6.1 --- a/src/Pure/General/table.ML	Fri May 17 11:35:52 2013 +0200
     6.2 +++ b/src/Pure/General/table.ML	Fri May 17 13:46:18 2013 +0200
     6.3 @@ -25,8 +25,8 @@
     6.4    val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
     6.5    val dest: 'a table -> (key * 'a) list
     6.6    val keys: 'a table -> key list
     6.7 -  val min_key: 'a table -> key option
     6.8 -  val max_key: 'a table -> key option
     6.9 +  val min: 'a table -> (key * 'a) option
    6.10 +  val max: 'a table -> (key * 'a) option
    6.11    val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
    6.12    val exists: (key * 'a -> bool) -> 'a table -> bool
    6.13    val forall: (key * 'a -> bool) -> 'a table -> bool
    6.14 @@ -116,19 +116,19 @@
    6.15  fun keys tab = fold_rev_table (cons o #1) tab [];
    6.16  
    6.17  
    6.18 -(* min/max keys *)
    6.19 +(* min/max entries *)
    6.20  
    6.21 -fun min_key Empty = NONE
    6.22 -  | min_key (Branch2 (Empty, (k, _), _)) = SOME k
    6.23 -  | min_key (Branch3 (Empty, (k, _), _, _, _)) = SOME k
    6.24 -  | min_key (Branch2 (left, _, _)) = min_key left
    6.25 -  | min_key (Branch3 (left, _, _, _, _)) = min_key left;
    6.26 +fun min Empty = NONE
    6.27 +  | min (Branch2 (Empty, p, _)) = SOME p
    6.28 +  | min (Branch3 (Empty, p, _, _, _)) = SOME p
    6.29 +  | min (Branch2 (left, _, _)) = min left
    6.30 +  | min (Branch3 (left, _, _, _, _)) = min left;
    6.31  
    6.32 -fun max_key Empty = NONE
    6.33 -  | max_key (Branch2 (_, (k, _), Empty)) = SOME k
    6.34 -  | max_key (Branch3 (_, _, _, (k, _), Empty)) = SOME k
    6.35 -  | max_key (Branch2 (_, _, right)) = max_key right
    6.36 -  | max_key (Branch3 (_, _, _, _, right)) = max_key right;
    6.37 +fun max Empty = NONE
    6.38 +  | max (Branch2 (_, p, Empty)) = SOME p
    6.39 +  | max (Branch3 (_, _, _, p, Empty)) = SOME p
    6.40 +  | max (Branch2 (_, _, right)) = max right
    6.41 +  | max (Branch3 (_, _, _, _, right)) = max right;
    6.42  
    6.43  
    6.44  (* get_first *)
     7.1 --- a/src/Pure/envir.ML	Fri May 17 11:35:52 2013 +0200
     7.2 +++ b/src/Pure/envir.ML	Fri May 17 13:46:18 2013 +0200
     7.3 @@ -128,8 +128,8 @@
     7.4  
     7.5  (*Determine if the least index updated exceeds lim*)
     7.6  fun above (Envir {tenv, tyenv, ...}) lim =
     7.7 -  (case Vartab.min_key tenv of SOME (_, i) => i > lim | NONE => true) andalso
     7.8 -  (case Vartab.min_key tyenv of SOME (_, i) => i > lim | NONE => true);
     7.9 +  (case Vartab.min tenv of SOME ((_, i), _) => i > lim | NONE => true) andalso
    7.10 +  (case Vartab.min tyenv of SOME ((_, i), _) => i > lim | NONE => true);
    7.11  
    7.12  (*Update, checking Var-Var assignments: try to suppress higher indexes*)
    7.13  fun vupdate (aU as (a, U), t) (env as Envir {tyenv, ...}) =