--- a/src/HOL/Library/comm_ring.ML Fri Jul 10 00:49:32 2009 +0200
+++ b/src/HOL/Library/comm_ring.ML Fri Jul 10 07:59:44 2009 +0200
@@ -41,7 +41,7 @@
fun reif_pol T vs (t as Free _) =
let
val one = @{term "1::nat"};
- val i = find_index_eq t vs
+ val i = find_index (fn t' => t' = t) vs
in if i = 0
then pol_PX T $ (pol_Pc T $ cring_one T)
$ one $ (pol_Pc T $ cring_zero T)
--- a/src/HOL/Library/reflection.ML Fri Jul 10 00:49:32 2009 +0200
+++ b/src/HOL/Library/reflection.ML Fri Jul 10 07:59:44 2009 +0200
@@ -103,8 +103,8 @@
NONE => error "index_of : type not found in environements!"
| SOME (tbs,tats) =>
let
- val i = find_index_eq t tats
- val j = find_index_eq t tbs
+ val i = find_index (fn t' => t' = t) tats
+ val j = find_index (fn t' => t' = t) tbs
in (if j = ~1 then
if i = ~1
then (length tbs + length tats,
--- a/src/HOL/Quickcheck.thy Fri Jul 10 00:49:32 2009 +0200
+++ b/src/HOL/Quickcheck.thy Fri Jul 10 07:59:44 2009 +0200
@@ -23,8 +23,8 @@
begin
definition
- "random i = Random.range i o\<rightarrow>
- (\<lambda>k. Pair (if (k div 2 = 0) then Code_Eval.valtermify True else Code_Eval.valtermify False))"
+ "random i = Random.range 2 o\<rightarrow>
+ (\<lambda>k. Pair (if k = 0 then Code_Eval.valtermify False else Code_Eval.valtermify True))"
instance ..
@@ -97,7 +97,7 @@
\<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
"random_fun_lift f = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of f Random.split_seed"
-instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
+instantiation "fun" :: ("{eq, term_of}", random) random
begin
definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Fri Jul 10 00:49:32 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Fri Jul 10 07:59:44 2009 +0200
@@ -111,7 +111,7 @@
else
Const ("Sum_Type.Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
end
- in mk_inj' sumT (length leafTs) (1 + find_index_eq T' leafTs)
+ in mk_inj' sumT (length leafTs) (1 + find_index (fn T'' => T'' = T') leafTs)
end;
(* make injections for constructors *)
@@ -137,7 +137,7 @@
if i <= n2 then Const (Suml_name, mkT T1) $ mk_inj T1 n2 i
else Const (Sumr_name, mkT T2) $ mk_inj T2 (n - n2) (i - n2)
end
- in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs)
+ in mk_inj branchT (length branchTs) (1 + find_index (fn T'' => T'' = T') branchTs)
end;
val mk_lim = List.foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
--- a/src/HOL/Tools/inductive.ML Fri Jul 10 00:49:32 2009 +0200
+++ b/src/HOL/Tools/inductive.ML Fri Jul 10 07:59:44 2009 +0200
@@ -222,7 +222,7 @@
val k = length params;
val (c, ts) = strip_comb t;
val (xs, ys) = chop k ts;
- val i = find_index_eq c cs;
+ val i = find_index (fn c' => c' = c) cs;
in
if xs = params andalso i >= 0 then
SOME (c, i, ys, chop (length ys)
--- a/src/HOL/Tools/inductive_realizer.ML Fri Jul 10 00:49:32 2009 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Fri Jul 10 07:59:44 2009 +0200
@@ -204,9 +204,9 @@
fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies =
let
val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct));
- val premss = List.mapPartial (fn (s, rs) => if s mem rsets then
- SOME (rs, map (fn (_, r) => List.nth (prems_of raw_induct,
- find_index_eq (prop_of r) (map prop_of intrs))) rs) else NONE) rss;
+ val premss = map_filter (fn (s, rs) => if member (op =) rsets s then
+ SOME (rs, map (fn (_, r) => nth (prems_of raw_induct)
+ (find_index (fn prp => prp = prop_of r) (map prop_of intrs))) rs) else NONE) rss;
val fs = maps (fn ((intrs, prems), dummy) =>
let
val fs = map (fn (rule, (ivs, intr)) =>
--- a/src/HOL/Tools/quickcheck_generators.ML Fri Jul 10 00:49:32 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Fri Jul 10 07:59:44 2009 +0200
@@ -27,7 +27,7 @@
fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"})
val size = @{term "i::code_numeral"};
-val size1 = @{term "(i::code_numeral) - 1"};
+val size_pred = @{term "(i::code_numeral) - 1"};
val size' = @{term "j::code_numeral"};
val seed = @{term "s::Random.seed"};
@@ -243,7 +243,7 @@
| mk_random_fun_lift (fT :: fTs) t =
mk_const @{const_name random_fun_lift} [fTs ---> T, fT] $
mk_random_fun_lift fTs t;
- val t = mk_random_fun_lift fTs (nth random_auxs k $ size1 $ size');
+ val t = mk_random_fun_lift fTs (nth random_auxs k $ size_pred $ size');
val size = Option.map snd (DatatypeCodegen.find_shortest_path descr k)
|> the_default 0;
in (SOME size, (t, fTs ---> T)) end;
--- a/src/HOL/Tools/refute.ML Fri Jul 10 00:49:32 2009 +0200
+++ b/src/HOL/Tools/refute.ML Fri Jul 10 07:59:44 2009 +0200
@@ -2401,7 +2401,7 @@
(* by our assumption on the order of recursion operators *)
(* and datatypes, this is the index of the datatype *)
(* corresponding to the given recursion operator *)
- val idt_index = find_index_eq s (#rec_names info)
+ val idt_index = find_index (fn s' => s' = s) (#rec_names info)
(* mutually recursive types must have the same type *)
(* parameters, unless the mutual recursion comes from *)
(* indirect recursion *)
@@ -2535,7 +2535,7 @@
(* returned *)
(* interpretation -> int -> int list option *)
fun get_args (Leaf xs) elem =
- if find_index_eq True xs = elem then
+ if find_index (fn x => x = True) xs = elem then
SOME []
else
NONE
@@ -2606,7 +2606,7 @@
(* corresponding recursive argument *)
fun rec_intr (DatatypeAux.DtRec i) (Leaf xs) =
(* recursive argument is "rec_i params elem" *)
- compute_array_entry i (find_index_eq True xs)
+ compute_array_entry i (find_index (fn x => x = True) xs)
| rec_intr (DatatypeAux.DtRec _) (Node _) =
raise REFUTE ("IDT_recursion_interpreter",
"interpretation for IDT is a node")
@@ -3237,7 +3237,7 @@
def_eq=false, next_idx=1, bounds=[], wellformed=True} cTerm
(* interpretation -> int list option *)
fun get_args (Leaf xs) =
- if find_index_eq True xs = element then
+ if find_index (fn x => x = True) xs = element then
SOME []
else
NONE
--- a/src/HOL/ex/predicate_compile.ML Fri Jul 10 00:49:32 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Fri Jul 10 07:59:44 2009 +0200
@@ -419,8 +419,8 @@
error ("Too few arguments for inductive predicate " ^ name)
else chop (length iss) args;
val k = length args2;
- val perm = map (fn i => (find_index_eq (Bound (b - i)) args2) + 1)
- (1 upto b)
+ val perm = map (fn i => (find_index (fn t => t = Bound (b - i)) args2) + 1)
+ (1 upto b)
val partial_mode = (1 upto k) \\ perm
in
if not (partial_mode subset is) then [] else
@@ -627,7 +627,7 @@
val (params, args') = chop (length ms) args
val (inargs, outargs) = get_args is' args'
val b = length vs
- val perm = map (fn i => (find_index_eq (Bound (b - i)) args') + 1) (1 upto b)
+ val perm = map (fn i => find_index (fn t => t = Bound (b - i)) args' + 1) (1 upto b)
val outp_perm =
snd (get_args is perm)
|> map (fn i => i - length (filter (fn x => x < i) is'))
--- a/src/HOLCF/Tools/domain/domain_extender.ML Fri Jul 10 00:49:32 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_extender.ML Fri Jul 10 07:59:44 2009 +0200
@@ -121,7 +121,7 @@
val thy' = thy'' |> Domain_Syntax.add_syntax comp_dnam eqs';
val dts = map (Type o fst) eqs';
val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
- fun strip ss = Library.drop (find_index_eq "'" ss +1, ss);
+ fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
fun typid (Type (id,_)) =
let val c = hd (Symbol.explode (Long_Name.base_name id))
in if Symbol.is_letter c then c else "t" end
--- a/src/HOLCF/Tools/domain/domain_library.ML Fri Jul 10 00:49:32 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_library.ML Fri Jul 10 07:59:44 2009 +0200
@@ -365,7 +365,7 @@
fun cpair_pat (p1,p2) = %%: @{const_name cpair_pat} $ p1 $ p2;
val mk_ctuple_pat = foldr1 cpair_pat;
fun lift_defined f = lift (fn x => defined (f x));
-fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
+fun bound_arg vns v = Bound (length vns - find_index (fn v' => v' = v) vns - 1);
fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) =
(case cont_eta_contract body of
--- a/src/Provers/Arith/fast_lin_arith.ML Fri Jul 10 00:49:32 2009 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Fri Jul 10 07:59:44 2009 +0200
@@ -391,7 +391,7 @@
|> hd
val (eq as Lineq(_,_,ceq,_),othereqs) =
extract_first (fn Lineq(_,_,l,_) => c mem l) eqs
- val v = find_index_eq c ceq
+ val v = find_index (fn v => v = c) ceq
val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0)
(othereqs @ noneqs)
val others = map (elim_var v eq) roth @ ioth
--- a/src/Pure/Isar/class.ML Fri Jul 10 00:49:32 2009 +0200
+++ b/src/Pure/Isar/class.ML Fri Jul 10 07:59:44 2009 +0200
@@ -311,7 +311,7 @@
val proto_sub = case TheoryTarget.peek lthy
of {is_class = false, ...} => error "Not in a class context"
| {target, ...} => target;
- val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup)
+ val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
val expr = ([(sup, (("", false), Expression.Positional []))], []);
val (([props], deps, export), goal_ctxt) =
--- a/src/Pure/Isar/class_target.ML Fri Jul 10 00:49:32 2009 +0200
+++ b/src/Pure/Isar/class_target.ML Fri Jul 10 07:59:44 2009 +0200
@@ -242,16 +242,15 @@
val diff_sort = Sign.complete_sort thy [sup]
|> subtract (op =) (Sign.complete_sort thy [sub])
|> filter (is_class thy);
+ val deps_witss = case some_dep_morph
+ of SOME dep_morph => [((sup, dep_morph), the_list some_wit)]
+ | NONE => []
in
thy
|> AxClass.add_classrel classrel
|> ClassData.map (Graph.add_edge (sub, sup))
|> activate_defs sub (these_defs thy diff_sort)
- |> fold (fn dep_morph => Locale.add_dependency sub (sup,
- dep_morph $> Element.satisfy_morphism (the_list some_wit) $> export))
- (the_list some_dep_morph)
- |> (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
- (Locale.get_registrations thy) thy)
+ |> Locale.add_dependencies sub deps_witss export
end;
--- a/src/Pure/Isar/expression.ML Fri Jul 10 00:49:32 2009 +0200
+++ b/src/Pure/Isar/expression.ML Fri Jul 10 07:59:44 2009 +0200
@@ -796,14 +796,9 @@
let
val target = intern thy raw_target;
val target_ctxt = Locale.init target thy;
-
val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
-
fun after_qed witss = ProofContext.theory
- (fold2 (fn (name, morph) => fn wits => Locale.add_dependency target
- (name, morph $> Element.satisfy_morphism wits $> export)) deps witss #>
- (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
- (Locale.get_registrations thy) thy));
+ (Locale.add_dependencies target (deps ~~ witss) export);
in Element.witness_proof after_qed propss goal_ctxt end;
in
@@ -860,7 +855,7 @@
end;
fun after_qed wits eqs = ProofContext.theory (fold_map store_reg (regs ~~ wits)
- #-> (fn regs => store_eqns_activate regs eqs));
+ #-> (fn regs => store_eqns_activate regs eqs));
in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
--- a/src/Pure/Isar/locale.ML Fri Jul 10 00:49:32 2009 +0200
+++ b/src/Pure/Isar/locale.ML Fri Jul 10 07:59:44 2009 +0200
@@ -45,7 +45,6 @@
val instance_of: theory -> string -> morphism -> term list
val specification_of: theory -> string -> term option * term list
val declarations_of: theory -> string -> declaration list * declaration list
- val dependencies_of: theory -> string -> (string * morphism) list
(* Storing results *)
val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
@@ -53,7 +52,6 @@
val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
val add_declaration: string -> declaration -> Proof.context -> Proof.context
- val add_dependency: string -> string * morphism -> theory -> theory
(* Activation *)
val activate_declarations: string * morphism -> Proof.context -> Proof.context
@@ -69,10 +67,11 @@
val unfold_add: attribute
val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
- (* Registrations *)
+ (* Registrations and dependencies *)
val add_registration: string * (morphism * morphism) -> theory -> theory
val amend_registration: morphism -> string * morphism -> theory -> theory
- val get_registrations: theory -> (string * morphism) list
+ val add_dependencies: string -> ((string * morphism) * Element.witness list) list ->
+ morphism -> theory -> theory
(* Diagnostic *)
val print_locales: theory -> unit
@@ -338,13 +337,19 @@
(* FIXME consolidate with dependencies, consider one data slot only *)
);
-val get_registrations =
- Registrations.get #> map (#1 #> apsnd op $>);
+fun reg_morph ((name, (base, export)), _) = (name, base $> export);
+
+fun these_registrations thy name = Registrations.get thy
+ |> filter (curry (op =) name o fst o fst)
+ |> map reg_morph;
+
+fun all_registrations thy = Registrations.get thy
+ |> map reg_morph;
fun add_registration (name, (base_morph, export)) thy =
roundup thy (fn (name', morph') => Registrations.map (cons ((name', (morph', export)), stamp ())))
- (name, base_morph) (get_idents (Context.Theory thy), thy) |> snd;
- (* FIXME |-> put_global_idents ?*)
+ (name, base_morph) (get_idents (Context.Theory thy), thy)
+ (* FIXME |-> (Context.theory_map o put_idents_diag)*) |> snd;
fun amend_registration morph (name, base_morph) thy =
let
@@ -364,6 +369,17 @@
end;
+(*** Dependencies ***)
+
+fun add_dependencies loc deps_witss export thy =
+ thy
+ |> fold (fn ((dep, morph), wits) => (change_locale loc o apsnd)
+ (cons ((dep, morph $> Element.satisfy_morphism wits $> export), stamp ())))
+ deps_witss
+ |> (fn thy => fold_rev (Context.theory_map o activate_facts)
+ (all_registrations thy) thy);
+
+
(*** Storing results ***)
(* Theorems *)
@@ -375,12 +391,12 @@
(change_locale loc o apfst o apsnd) (cons (args', stamp ()))
#>
(* Registrations *)
- (fn thy => fold_rev (fn (name, morph) =>
+ (fn thy => fold_rev (fn (_, morph) =>
let
val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
Attrib.map_facts (Attrib.attribute_i thy)
in PureThy.note_thmss kind args'' #> snd end)
- (get_registrations thy |> filter (fn (name, _) => name = loc)) thy))
+ (these_registrations thy loc) thy))
in ctxt'' end;
@@ -404,11 +420,6 @@
end;
-(* Dependencies *)
-
-fun add_dependency loc dep = (change_locale loc o apsnd) (cons (dep, stamp ()));
-
-
(*** Reasoning about locales ***)
(* Storage for witnesses, intro and unfold rules *)
--- a/src/Pure/library.ML Fri Jul 10 00:49:32 2009 +0200
+++ b/src/Pure/library.ML Fri Jul 10 07:59:44 2009 +0200
@@ -97,7 +97,6 @@
val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
val split_last: 'a list -> 'a list * 'a
val find_index: ('a -> bool) -> 'a list -> int
- val find_index_eq: ''a -> ''a list -> int
val find_first: ('a -> bool) -> 'a list -> 'a option
val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
val get_first: ('a -> 'b option) -> 'a list -> 'b option
@@ -503,8 +502,6 @@
| find n (x :: xs) = if pred x then n else find (n + 1) xs;
in find 0 end;
-fun find_index_eq x = find_index (equal x);
-
(*find first element satisfying predicate*)
val find_first = List.find;