# HG changeset patch # User haftmann # Date 1247205584 -7200 # Node ID a290c36e94d638a524f8b5b6194797723200a9dc # Parent 7b7dfbf38034105ad7cfe7dbde6af3aa9fae1ca4# Parent 801aabf9f376710511051d36217ce7cde7c20af0 merged diff -r 7b7dfbf38034 -r a290c36e94d6 src/HOL/Library/comm_ring.ML --- 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) diff -r 7b7dfbf38034 -r a290c36e94d6 src/HOL/Library/reflection.ML --- 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, diff -r 7b7dfbf38034 -r a290c36e94d6 src/HOL/Quickcheck.thy --- 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\ - (\k. Pair (if (k div 2 = 0) then Code_Eval.valtermify True else Code_Eval.valtermify False))" + "random i = Random.range 2 o\ + (\k. Pair (if k = 0 then Code_Eval.valtermify False else Code_Eval.valtermify True))" instance .. @@ -97,7 +97,7 @@ \ Random.seed \ (('a\term_of \ 'b\typerep) \ (unit \ term)) \ 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 \ Random.seed \ (('a \ 'b) \ (unit \ term)) \ Random.seed" where diff -r 7b7dfbf38034 -r a290c36e94d6 src/HOL/Tools/Datatype/datatype_rep_proofs.ML --- 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))); diff -r 7b7dfbf38034 -r a290c36e94d6 src/HOL/Tools/inductive.ML --- 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) diff -r 7b7dfbf38034 -r a290c36e94d6 src/HOL/Tools/inductive_realizer.ML --- 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)) => diff -r 7b7dfbf38034 -r a290c36e94d6 src/HOL/Tools/quickcheck_generators.ML --- 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; diff -r 7b7dfbf38034 -r a290c36e94d6 src/HOL/Tools/refute.ML --- 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 diff -r 7b7dfbf38034 -r a290c36e94d6 src/HOL/ex/predicate_compile.ML --- 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')) diff -r 7b7dfbf38034 -r a290c36e94d6 src/HOLCF/Tools/domain/domain_extender.ML --- 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 diff -r 7b7dfbf38034 -r a290c36e94d6 src/HOLCF/Tools/domain/domain_library.ML --- 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 diff -r 7b7dfbf38034 -r a290c36e94d6 src/Provers/Arith/fast_lin_arith.ML --- 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 diff -r 7b7dfbf38034 -r a290c36e94d6 src/Pure/Isar/class.ML --- 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) = diff -r 7b7dfbf38034 -r a290c36e94d6 src/Pure/Isar/class_target.ML --- 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; diff -r 7b7dfbf38034 -r a290c36e94d6 src/Pure/Isar/expression.ML --- 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; diff -r 7b7dfbf38034 -r a290c36e94d6 src/Pure/Isar/locale.ML --- 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 *) diff -r 7b7dfbf38034 -r a290c36e94d6 src/Pure/library.ML --- 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;