# HG changeset patch # User huffman # Date 1268530613 28800 # Node ID 8b3327bcbf7d807d1d3e10bb7131e3fbacdf1647 # Parent bcc77916b7b964c0183ecebb1cf2f7d78e02e555# Parent 086504a943afeba89af2ca4aa9411da36986233f merged diff -r bcc77916b7b9 -r 8b3327bcbf7d NEWS --- a/NEWS Sat Mar 13 17:05:34 2010 -0800 +++ b/NEWS Sat Mar 13 17:36:53 2010 -0800 @@ -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 bcc77916b7b9 -r 8b3327bcbf7d src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Sat Mar 13 17:05:34 2010 -0800 +++ b/src/HOL/Tools/typedef.ML Sat Mar 13 17:36:53 2010 -0800 @@ -158,22 +158,11 @@ (* set definition *) - (* FIXME let Local_Theory.define handle hidden polymorphism (!??!) *) - - val rhs_tfrees = Term.add_tfrees set []; - val rhs_tfreesT = Term.add_tfreesT setT []; - - val set_argsT = lhs_tfrees - |> filter (member (op =) rhs_tfrees andf (not o member (op =) rhs_tfreesT)) - |> map TFree; - val set_args = map Logic.mk_type set_argsT; - val ((set', set_def), set_lthy) = if def_set then typedecl_lthy - |> Local_Theory.define - ((name, NoSyn), ((Thm.def_binding name, []), fold_rev lambda set_args set)) - |>> (fn (s, (_, set_def)) => (Term.list_comb (s, set_args), SOME set_def)) + |> Local_Theory.define ((name, NoSyn), ((Thm.def_binding name, []), set)) + |>> (fn (set', (_, set_def)) => (set', SOME set_def)) else ((set, NONE), typedecl_lthy); diff -r bcc77916b7b9 -r 8b3327bcbf7d src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Sat Mar 13 17:05:34 2010 -0800 +++ b/src/Pure/Isar/args.ML Sat Mar 13 17:36:53 2010 -0800 @@ -14,7 +14,6 @@ val pretty_src: Proof.context -> src -> Pretty.T val map_name: (string -> string) -> src -> src val morph_values: morphism -> src -> src - val maxidx_values: src -> int -> int val assignable: src -> src val closure: src -> src val context: Proof.context context_parser @@ -111,13 +110,6 @@ | T.Fact ths => T.Fact (Morphism.fact phi ths) | T.Attribute att => T.Attribute (Morphism.transform phi att))); -fun maxidx_values (Src ((_, args), _)) = args |> fold (fn arg => - (case T.get_value arg of - SOME (T.Typ T) => Term.maxidx_typ T - | SOME (T.Term t) => Term.maxidx_term t - | SOME (T.Fact ths) => fold Thm.maxidx_thm ths - | _ => I)); - val assignable = map_args T.assignable; val closure = map_args T.closure; diff -r bcc77916b7b9 -r 8b3327bcbf7d src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Sat Mar 13 17:05:34 2010 -0800 +++ b/src/Pure/Isar/element.ML Sat Mar 13 17:36:53 2010 -0800 @@ -55,9 +55,6 @@ val satisfy_facts: witness list -> (Attrib.binding * (thm list * Attrib.src list) list) list -> (Attrib.binding * (thm list * Attrib.src list) list) list - val generalize_facts: Proof.context -> Proof.context -> - (Attrib.binding * (thm list * Attrib.src list) list) list -> - (Attrib.binding * (thm list * Attrib.src list) list) list val eq_morphism: theory -> thm list -> morphism val transfer_morphism: theory -> morphism val init: context_i -> Context.generic -> Context.generic @@ -458,22 +455,6 @@ fact = map (MetaSimplifier.rewrite_rule thms)}; -(* generalize type/term parameters *) - -val maxidx_atts = fold Args.maxidx_values; - -fun generalize_facts inner outer facts = - let - val thy = ProofContext.theory_of inner; - val maxidx = - fold (fn ((_, atts), bs) => maxidx_atts atts #> fold (maxidx_atts o #2) bs) facts ~1; - val exp_fact = map (Thm.adjust_maxidx_thm maxidx) #> Variable.export inner outer; - val exp_term = Drule.term_rule thy (singleton exp_fact); - val exp_typ = Logic.type_map exp_term; - val morphism = Morphism.morphism {binding = I, typ = exp_typ, term = exp_term, fact = exp_fact}; - in facts_map (morph_ctxt morphism) facts end; - - (* transfer to theory using closure *) fun transfer_morphism thy = diff -r bcc77916b7b9 -r 8b3327bcbf7d src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Sat Mar 13 17:05:34 2010 -0800 +++ b/src/Pure/Isar/theory_target.ML Sat Mar 13 17:36:53 2010 -0800 @@ -179,7 +179,7 @@ end; -(* declare_const *) +(* consts *) fun fork_mixfix (Target {is_locale, is_class, ...}) mx = if not is_locale then (NoSyn, NoSyn, mx) @@ -209,34 +209,6 @@ Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)])))) end; -fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c); - -fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy = - let - val xs = filter depends (#1 (ProofContext.inferred_fixes (Local_Theory.target_of lthy))); - val U = map #2 xs ---> T; - val (mx1, mx2, mx3) = fork_mixfix ta mx; - val (const, lthy') = lthy |> - (case Class_Target.instantiation_param lthy b of - SOME c' => - if mx3 <> NoSyn then syntax_error c' - else Local_Theory.theory_result (AxClass.declare_overloaded (c', U)) - ##> Class_Target.confirm_declaration b - | NONE => - (case Overloading.operation lthy b of - SOME (c', _) => - if mx3 <> NoSyn then syntax_error c' - 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 xs); - in - lthy' - |> is_locale ? term_syntax ta false (locale_const ta Syntax.mode_default ((b, mx2), t)) - |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), t)) - |> Local_Defs.add_def ((b, NoSyn), t) - end; - (* abbrev *) @@ -271,6 +243,47 @@ (* define *) +local + +fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c); + +fun declare_const (ta as Target {target, is_locale, is_class, ...}) + extra_tfrees xs ((b, T), mx) lthy = + let + 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 (Free (x, T)) + | NONE => NONE)); + 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 + SOME c' => + if mx3 <> NoSyn then syntax_error c' + else Local_Theory.theory_result (AxClass.declare_overloaded (c', U)) + ##> Class_Target.confirm_declaration b + | NONE => + (case Overloading.operation lthy b of + SOME (c', _) => + if mx3 <> NoSyn then syntax_error c' + 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, params); + in + lthy' + |> is_locale ? term_syntax ta false (locale_const ta Syntax.mode_default ((b, mx2), t)) + |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), t)) + |> Local_Defs.add_def ((b, NoSyn), t) + end; + +in + fun define ta ((b, mx), ((name, atts), rhs)) lthy = let val thy = ProofContext.theory_of lthy; @@ -284,20 +297,26 @@ 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 (member (op =) 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_none (Class_Target.instantiation_param lthy b) - then Thm.add_def false false (name', Logic.mk_equals (lhs', rhs')) - else AxClass.define_overloaded name' (fst (dest_Const lhs'), rhs')); + if is_some (Class_Target.instantiation_param lthy b) + 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, (*global.c xs == rhs'*) global_def, @@ -308,6 +327,8 @@ |> notes ta "" [((name', atts), [([def], [])])]; in ((lhs, (res_name, res)), lthy4) end; +end; + (* init various targets *)