# HG changeset patch # User haftmann # Date 1281509420 -7200 # Node ID ac3080d48b010e30cea875406a43a742a4ff002a # Parent cb8e2ac6397b1d7dd24686ffb9dfcc36b49419ea# Parent 1cfc2b128e333347ec71a1286905caf9efbfd4d8 merged diff -r cb8e2ac6397b -r ac3080d48b01 src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Wed Aug 11 13:30:24 2010 +0800 +++ b/src/Pure/Isar/theory_target.ML Wed Aug 11 08:50:20 2010 +0200 @@ -107,20 +107,54 @@ Local_Theory.target (Class_Target.refresh_syntax target); -(* mixfix notation *) +(* define *) + +fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c); + +fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = + let + val (const, lthy2) = lthy |> Local_Theory.theory_result + (Sign.declare_const ((b, U), mx)); + val lhs = list_comb (const, type_params @ term_params); + val ((_, def), lthy3) = lthy2 |> Local_Theory.theory_result + (Thm.add_def false false (b_def, Logic.mk_equals (lhs, rhs))); + in ((lhs, def), lthy3) end; + +fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) = + theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) + #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, mx), lhs) + #> pair (lhs, def)) + +fun class_foundation (ta as Target {target, ...}) + (((b, U), mx), (b_def, rhs)) (type_params, term_params) = + theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) + #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs) + #> class_target ta (Class_Target.declare target ((b, mx), (type_params, lhs))) + #> pair (lhs, def)) + +fun instantiation_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = + case Class_Target.instantiation_param lthy b + of SOME c => if mx <> NoSyn then syntax_error c + else lthy |> Local_Theory.theory_result (AxClass.declare_overloaded (c, U) + ##>> AxClass.define_overloaded b_def (c, rhs)) + ||> Class_Target.confirm_declaration b + | NONE => lthy |> + theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params); + +fun overloading_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = + case Overloading.operation lthy b + of SOME (c, checked) => if mx <> NoSyn then syntax_error c + else lthy |> Local_Theory.theory_result (Overloading.declare (c, U) + ##>> Overloading.define checked b_def (c, rhs)) + ||> Overloading.confirm b + | NONE => lthy |> + theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params); fun fork_mixfix (Target {is_locale, is_class, ...}) mx = if not is_locale then (NoSyn, NoSyn, mx) else if not is_class then (NoSyn, mx, NoSyn) else (mx, NoSyn, NoSyn); - -(* define *) - -local - -fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c); - fun foundation (ta as Target {target, is_locale, is_class, ...}) (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = let @@ -155,12 +189,6 @@ (Class_Target.declare target ((b, mx1), (type_params, lhs))) end; -in - -fun define ta = Generic_Target.define (foundation ta); - -end; - (* notes *) @@ -185,9 +213,9 @@ |> Local_Theory.target (Locale.add_thmss locale kind local_facts') end -fun notes (Target {target, is_locale, ...}) = - Generic_Target.notes (if is_locale then locale_notes target - else fn kind => fn global_facts => fn _ => theory_notes kind global_facts); +fun target_notes (ta as Target {target, is_locale, ...}) = + if is_locale then locale_notes target + else fn kind => fn global_facts => fn _ => theory_notes kind global_facts; (* abbrev *) @@ -203,17 +231,12 @@ fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) prmode (b, mx) (global_rhs, t') xs lthy = - let - val (mx1, mx2, mx3) = fork_mixfix ta mx; - in if is_locale + if is_locale then lthy - |> locale_abbrev ta prmode ((b, mx2), global_rhs) xs - |> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx1), t')) + |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs + |> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx), t')) else lthy - |> theory_abbrev prmode ((b, mx3), global_rhs) - end; - -fun abbrev ta = Generic_Target.abbrev (target_abbrev ta); + |> theory_abbrev prmode ((b, mx), global_rhs); (* pretty *) @@ -262,9 +285,9 @@ |> init_data ta |> Data.put ta |> Local_Theory.init NONE (Long_Name.base_name target) - {define = define ta, - notes = notes ta, - abbrev = abbrev ta, + {define = Generic_Target.define (foundation ta), + notes = Generic_Target.notes (target_notes ta), + abbrev = Generic_Target.abbrev (target_abbrev ta), declaration = fn pervasive => target_declaration ta { syntax = false, pervasive = pervasive }, syntax_declaration = fn pervasive => target_declaration ta @@ -287,7 +310,22 @@ val ctxt = ProofContext.init_global thy; val ops = raw_ops |> map (fn (name, const, checked) => (name, Term.dest_Const (prep_const ctxt const), checked)); - in thy |> init_target (make_target "" false false ([], [], []) ops) end; + in + thy + |> Overloading.init ops + |> Local_Theory.init NONE "" + {define = Generic_Target.define overloading_foundation, + notes = Generic_Target.notes + (fn kind => fn global_facts => fn _ => theory_notes kind global_facts), + abbrev = Generic_Target.abbrev + (fn prmode => fn (b, mx) => fn (t, _) => fn _ => + theory_abbrev prmode ((b, mx), t)), + declaration = fn pervasive => theory_declaration, + syntax_declaration = fn pervasive => theory_declaration, + pretty = single o Overloading.pretty, + reinit = gen_overloading prep_const raw_ops o ProofContext.theory_of, + exit = Local_Theory.target_of o Overloading.conclude} + end; in @@ -296,7 +334,21 @@ fun context_cmd "-" thy = init NONE thy | context_cmd target thy = init (SOME (Locale.intern thy target)) thy; -fun instantiation arities = init_target (make_target "" false false arities []); +fun instantiation arities thy = + thy + |> Class_Target.init_instantiation arities + |> Local_Theory.init NONE "" + {define = Generic_Target.define instantiation_foundation, + notes = Generic_Target.notes + (fn kind => fn global_facts => fn _ => theory_notes kind global_facts), + abbrev = Generic_Target.abbrev + (fn prmode => fn (b, mx) => fn (t, _) => fn _ => theory_abbrev prmode ((b, mx), t)), + declaration = fn pervasive => theory_declaration, + syntax_declaration = fn pervasive => theory_declaration, + pretty = single o Class_Target.pretty_instantiation, + reinit = instantiation arities o ProofContext.theory_of, + exit = Local_Theory.target_of o Class_Target.conclude_instantiation}; + fun instantiation_cmd arities thy = instantiation (Class_Target.read_multi_arity thy arities) thy;