# HG changeset patch # User wenzelm # Date 1268508794 -3600 # Node ID 09e238561460a88c6cbf0200380ee0436574feae # Parent f7f88f2e004fe1d325ff7d149ad92825f660ce7c local theory specifications handle hidden polymorphism implicitly; diff -r f7f88f2e004f -r 09e238561460 NEWS --- a/NEWS Sat Mar 13 19:35:53 2010 +0100 +++ b/NEWS Sat Mar 13 20:33:14 2010 +0100 @@ -64,6 +64,12 @@ *** Pure *** +* Local theory specifications may depend on extra type variables that +are not present in the result type -- arguments TYPE('a) :: 'a itself +are added internally. For example: + + definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)" + * Code generator: details of internal data cache have no impact on the user space functionality any longer. diff -r f7f88f2e004f -r 09e238561460 src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Sat Mar 13 19:35:53 2010 +0100 +++ b/src/Pure/Isar/theory_target.ML Sat Mar 13 20:33:14 2010 +0100 @@ -247,15 +247,19 @@ fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c); -fun declare_const (ta as Target {target, is_locale, is_class, ...}) xs ((b, T), mx) lthy = +fun declare_const (ta as Target {target, is_locale, is_class, ...}) + extra_tfrees xs ((b, T), mx) lthy = let - val params = + val type_params = map (Logic.mk_type o TFree) extra_tfrees; + val term_params = rev (Variable.fixes_of (Local_Theory.target_of lthy)) |> map_filter (fn (_, x) => (case AList.lookup (op =) xs x of - SOME T => SOME (x, T) + SOME T => SOME (Free (x, T)) | NONE => NONE)); - val U = map #2 params ---> T; + val params = type_params @ term_params; + + val U = map Term.fastype_of params ---> T; val (mx1, mx2, mx3) = fork_mixfix ta mx; val (const, lthy') = lthy |> (case Class_Target.instantiation_param lthy b of @@ -270,7 +274,7 @@ else Local_Theory.theory_result (Overloading.declare (c', U)) ##> Overloading.confirm b | NONE => Local_Theory.theory_result (Sign.declare_const ((b, U), mx3)))); - val t = Term.list_comb (const, map Free params); + val t = Term.list_comb (const, params); in lthy' |> is_locale ? term_syntax ta false (locale_const ta Syntax.mode_default ((b, mx2), t)) @@ -293,19 +297,25 @@ val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' []; val T = Term.fastype_of rhs; + val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []); + val extra_tfrees = + fold_types (fold_atyps + (fn TFree v => if member (op =) tfreesT v then I else insert (op =) v | _ => I)) rhs [] + |> sort_wrt #1; (*const*) - val ((lhs, local_def), lthy2) = lthy |> declare_const ta xs ((b, T), mx); + val ((lhs, local_def), lthy2) = lthy |> declare_const ta extra_tfrees xs ((b, T), mx); val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def); + val Const (head, _) = Term.head_of lhs'; (*def*) val (global_def, lthy3) = lthy2 |> Local_Theory.theory_result (case Overloading.operation lthy b of - SOME (_, checked) => Overloading.define checked name' (fst (dest_Const lhs'), rhs') + SOME (_, checked) => Overloading.define checked name' (head, rhs') | NONE => if is_some (Class_Target.instantiation_param lthy b) - then AxClass.define_overloaded name' (fst (dest_Const lhs'), rhs') + then AxClass.define_overloaded name' (head, rhs') else Thm.add_def false false (name', Logic.mk_equals (lhs', rhs'))); val def = Local_Defs.trans_terms lthy3 [(*c == global.c xs*) local_def,