1.1 --- a/src/Pure/Isar/theory_target.ML Wed Aug 11 13:30:24 2010 +0800
1.2 +++ b/src/Pure/Isar/theory_target.ML Wed Aug 11 08:50:20 2010 +0200
1.3 @@ -107,20 +107,54 @@
1.4 Local_Theory.target (Class_Target.refresh_syntax target);
1.5
1.6
1.7 -(* mixfix notation *)
1.8 +(* define *)
1.9 +
1.10 +fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
1.11 +
1.12 +fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
1.13 + let
1.14 + val (const, lthy2) = lthy |> Local_Theory.theory_result
1.15 + (Sign.declare_const ((b, U), mx));
1.16 + val lhs = list_comb (const, type_params @ term_params);
1.17 + val ((_, def), lthy3) = lthy2 |> Local_Theory.theory_result
1.18 + (Thm.add_def false false (b_def, Logic.mk_equals (lhs, rhs)));
1.19 + in ((lhs, def), lthy3) end;
1.20 +
1.21 +fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
1.22 + theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
1.23 + #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, mx), lhs)
1.24 + #> pair (lhs, def))
1.25 +
1.26 +fun class_foundation (ta as Target {target, ...})
1.27 + (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
1.28 + theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
1.29 + #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs)
1.30 + #> class_target ta (Class_Target.declare target ((b, mx), (type_params, lhs)))
1.31 + #> pair (lhs, def))
1.32 +
1.33 +fun instantiation_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
1.34 + case Class_Target.instantiation_param lthy b
1.35 + of SOME c => if mx <> NoSyn then syntax_error c
1.36 + else lthy |> Local_Theory.theory_result (AxClass.declare_overloaded (c, U)
1.37 + ##>> AxClass.define_overloaded b_def (c, rhs))
1.38 + ||> Class_Target.confirm_declaration b
1.39 + | NONE => lthy |>
1.40 + theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
1.41 +
1.42 +fun overloading_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
1.43 + case Overloading.operation lthy b
1.44 + of SOME (c, checked) => if mx <> NoSyn then syntax_error c
1.45 + else lthy |> Local_Theory.theory_result (Overloading.declare (c, U)
1.46 + ##>> Overloading.define checked b_def (c, rhs))
1.47 + ||> Overloading.confirm b
1.48 + | NONE => lthy |>
1.49 + theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
1.50
1.51 fun fork_mixfix (Target {is_locale, is_class, ...}) mx =
1.52 if not is_locale then (NoSyn, NoSyn, mx)
1.53 else if not is_class then (NoSyn, mx, NoSyn)
1.54 else (mx, NoSyn, NoSyn);
1.55
1.56 -
1.57 -(* define *)
1.58 -
1.59 -local
1.60 -
1.61 -fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
1.62 -
1.63 fun foundation (ta as Target {target, is_locale, is_class, ...})
1.64 (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
1.65 let
1.66 @@ -155,12 +189,6 @@
1.67 (Class_Target.declare target ((b, mx1), (type_params, lhs)))
1.68 end;
1.69
1.70 -in
1.71 -
1.72 -fun define ta = Generic_Target.define (foundation ta);
1.73 -
1.74 -end;
1.75 -
1.76
1.77 (* notes *)
1.78
1.79 @@ -185,9 +213,9 @@
1.80 |> Local_Theory.target (Locale.add_thmss locale kind local_facts')
1.81 end
1.82
1.83 -fun notes (Target {target, is_locale, ...}) =
1.84 - Generic_Target.notes (if is_locale then locale_notes target
1.85 - else fn kind => fn global_facts => fn _ => theory_notes kind global_facts);
1.86 +fun target_notes (ta as Target {target, is_locale, ...}) =
1.87 + if is_locale then locale_notes target
1.88 + else fn kind => fn global_facts => fn _ => theory_notes kind global_facts;
1.89
1.90
1.91 (* abbrev *)
1.92 @@ -203,17 +231,12 @@
1.93
1.94 fun target_abbrev (ta as Target {target, is_locale, is_class, ...})
1.95 prmode (b, mx) (global_rhs, t') xs lthy =
1.96 - let
1.97 - val (mx1, mx2, mx3) = fork_mixfix ta mx;
1.98 - in if is_locale
1.99 + if is_locale
1.100 then lthy
1.101 - |> locale_abbrev ta prmode ((b, mx2), global_rhs) xs
1.102 - |> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx1), t'))
1.103 + |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
1.104 + |> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx), t'))
1.105 else lthy
1.106 - |> theory_abbrev prmode ((b, mx3), global_rhs)
1.107 - end;
1.108 -
1.109 -fun abbrev ta = Generic_Target.abbrev (target_abbrev ta);
1.110 + |> theory_abbrev prmode ((b, mx), global_rhs);
1.111
1.112
1.113 (* pretty *)
1.114 @@ -262,9 +285,9 @@
1.115 |> init_data ta
1.116 |> Data.put ta
1.117 |> Local_Theory.init NONE (Long_Name.base_name target)
1.118 - {define = define ta,
1.119 - notes = notes ta,
1.120 - abbrev = abbrev ta,
1.121 + {define = Generic_Target.define (foundation ta),
1.122 + notes = Generic_Target.notes (target_notes ta),
1.123 + abbrev = Generic_Target.abbrev (target_abbrev ta),
1.124 declaration = fn pervasive => target_declaration ta
1.125 { syntax = false, pervasive = pervasive },
1.126 syntax_declaration = fn pervasive => target_declaration ta
1.127 @@ -287,7 +310,22 @@
1.128 val ctxt = ProofContext.init_global thy;
1.129 val ops = raw_ops |> map (fn (name, const, checked) =>
1.130 (name, Term.dest_Const (prep_const ctxt const), checked));
1.131 - in thy |> init_target (make_target "" false false ([], [], []) ops) end;
1.132 + in
1.133 + thy
1.134 + |> Overloading.init ops
1.135 + |> Local_Theory.init NONE ""
1.136 + {define = Generic_Target.define overloading_foundation,
1.137 + notes = Generic_Target.notes
1.138 + (fn kind => fn global_facts => fn _ => theory_notes kind global_facts),
1.139 + abbrev = Generic_Target.abbrev
1.140 + (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
1.141 + theory_abbrev prmode ((b, mx), t)),
1.142 + declaration = fn pervasive => theory_declaration,
1.143 + syntax_declaration = fn pervasive => theory_declaration,
1.144 + pretty = single o Overloading.pretty,
1.145 + reinit = gen_overloading prep_const raw_ops o ProofContext.theory_of,
1.146 + exit = Local_Theory.target_of o Overloading.conclude}
1.147 + end;
1.148
1.149 in
1.150
1.151 @@ -296,7 +334,21 @@
1.152 fun context_cmd "-" thy = init NONE thy
1.153 | context_cmd target thy = init (SOME (Locale.intern thy target)) thy;
1.154
1.155 -fun instantiation arities = init_target (make_target "" false false arities []);
1.156 +fun instantiation arities thy =
1.157 + thy
1.158 + |> Class_Target.init_instantiation arities
1.159 + |> Local_Theory.init NONE ""
1.160 + {define = Generic_Target.define instantiation_foundation,
1.161 + notes = Generic_Target.notes
1.162 + (fn kind => fn global_facts => fn _ => theory_notes kind global_facts),
1.163 + abbrev = Generic_Target.abbrev
1.164 + (fn prmode => fn (b, mx) => fn (t, _) => fn _ => theory_abbrev prmode ((b, mx), t)),
1.165 + declaration = fn pervasive => theory_declaration,
1.166 + syntax_declaration = fn pervasive => theory_declaration,
1.167 + pretty = single o Class_Target.pretty_instantiation,
1.168 + reinit = instantiation arities o ProofContext.theory_of,
1.169 + exit = Local_Theory.target_of o Class_Target.conclude_instantiation};
1.170 +
1.171 fun instantiation_cmd arities thy =
1.172 instantiation (Class_Target.read_multi_arity thy arities) thy;
1.173