1.1 --- a/src/Pure/Isar/overloading.ML Wed Aug 11 17:19:27 2010 +0200
1.2 +++ b/src/Pure/Isar/overloading.ML Wed Aug 11 17:59:32 2010 +0200
1.3 @@ -113,27 +113,22 @@
1.4
1.5 (** overloading target **)
1.6
1.7 -(* bookkeeping *)
1.8 -
1.9 -structure OverloadingData = Proof_Data
1.10 +structure Data = Proof_Data
1.11 (
1.12 type T = ((string * typ) * (string * bool)) list;
1.13 fun init _ = [];
1.14 );
1.15
1.16 -val get_overloading = OverloadingData.get o Local_Theory.target_of;
1.17 -val map_overloading = Local_Theory.target o OverloadingData.map;
1.18 +val get_overloading = Data.get o Local_Theory.target_of;
1.19 +val map_overloading = Local_Theory.target o Data.map;
1.20
1.21 fun operation lthy b = get_overloading lthy
1.22 |> get_first (fn ((c, _), (v, checked)) =>
1.23 - if Binding.name_of b = v then SOME (c, checked) else NONE);
1.24 -
1.25 -
1.26 -(* target *)
1.27 + if Binding.name_of b = v then SOME (c, (v, checked)) else NONE);
1.28
1.29 fun synchronize_syntax ctxt =
1.30 let
1.31 - val overloading = OverloadingData.get ctxt;
1.32 + val overloading = Data.get ctxt;
1.33 fun subst (c, ty) = case AList.lookup (op =) overloading (c, ty)
1.34 of SOME (v, _) => SOME (ty, Free (v, ty))
1.35 | NONE => NONE;
1.36 @@ -144,38 +139,20 @@
1.37 |> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false))
1.38 end
1.39
1.40 -fun init raw_overloading thy =
1.41 - let
1.42 - val _ = if null raw_overloading then error "At least one parameter must be given" else ();
1.43 - val overloading = map (fn (v, c_ty, checked) => (c_ty, (v, checked))) raw_overloading;
1.44 - in
1.45 - thy
1.46 - |> Theory.checkpoint
1.47 - |> ProofContext.init_global
1.48 - |> OverloadingData.put overloading
1.49 - |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
1.50 - |> add_improvable_syntax
1.51 - |> synchronize_syntax
1.52 - end;
1.53 +fun define_overloaded (c, U) (v, checked) (b_def, rhs) =
1.54 + Local_Theory.theory_result
1.55 + (Thm.add_def (not checked) true (b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
1.56 + ##> map_overloading (filter_out (fn (_, (v', _)) => v' = v))
1.57 + ##> Local_Theory.target synchronize_syntax
1.58 + #-> (fn (_, def) => pair (Const (c, U), def))
1.59
1.60 -fun declare c_ty = pair (Const c_ty);
1.61 -
1.62 -fun define checked b (c, t) =
1.63 - Thm.add_def (not checked) true (b, Logic.mk_equals (Const (c, Term.fastype_of t), t))
1.64 - #>> snd;
1.65 -
1.66 -fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
1.67 - #> Local_Theory.target synchronize_syntax
1.68 -
1.69 -fun conclude lthy =
1.70 - let
1.71 - val overloading = get_overloading lthy;
1.72 - val _ = if null overloading then () else
1.73 - error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
1.74 - o Syntax.string_of_term lthy o Const o fst) overloading));
1.75 - in
1.76 - lthy
1.77 - end;
1.78 +fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
1.79 + case operation lthy b
1.80 + of SOME (c, (v, checked)) => if mx <> NoSyn
1.81 + then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
1.82 + else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs)
1.83 + | NONE => lthy |>
1.84 + Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
1.85
1.86 fun pretty lthy =
1.87 let
1.88 @@ -184,32 +161,32 @@
1.89 fun pr_operation ((c, ty), (v, _)) =
1.90 (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
1.91 Pretty.str (Sign.extern_const thy c), Pretty.str "::", Syntax.pretty_typ lthy ty];
1.92 - in
1.93 - (Pretty.block o Pretty.fbreaks)
1.94 - (Pretty.str "overloading" :: map pr_operation overloading)
1.95 - end;
1.96 + in Pretty.str "overloading" :: map pr_operation overloading end;
1.97
1.98 -fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
1.99 +fun conclude lthy =
1.100 + let
1.101 + val overloading = get_overloading lthy;
1.102 + val _ = if null overloading then () else
1.103 + error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
1.104 + o Syntax.string_of_term lthy o Const o fst) overloading));
1.105 + in lthy end;
1.106
1.107 -fun overloading_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
1.108 - case operation lthy b
1.109 - of SOME (c, checked) => if mx <> NoSyn then syntax_error c
1.110 - else lthy |> Local_Theory.theory_result (declare (c, U)
1.111 - ##>> define checked b_def (c, rhs))
1.112 - ||> confirm b
1.113 - | NONE => lthy |>
1.114 - Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
1.115 -
1.116 -fun gen_overloading prep_const raw_ops thy =
1.117 +fun gen_overloading prep_const raw_overloading thy =
1.118 let
1.119 val ctxt = ProofContext.init_global thy;
1.120 - val ops = raw_ops |> map (fn (name, const, checked) =>
1.121 - (name, Term.dest_Const (prep_const ctxt const), checked));
1.122 + val _ = if null raw_overloading then error "At least one parameter must be given" else ();
1.123 + val overloading = raw_overloading |> map (fn (v, const, checked) =>
1.124 + (Term.dest_Const (prep_const ctxt const), (v, checked)));
1.125 in
1.126 thy
1.127 - |> init ops
1.128 + |> Theory.checkpoint
1.129 + |> ProofContext.init_global
1.130 + |> Data.put overloading
1.131 + |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
1.132 + |> add_improvable_syntax
1.133 + |> synchronize_syntax
1.134 |> Local_Theory.init NONE ""
1.135 - {define = Generic_Target.define overloading_foundation,
1.136 + {define = Generic_Target.define foundation,
1.137 notes = Generic_Target.notes
1.138 (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
1.139 abbrev = Generic_Target.abbrev
1.140 @@ -217,7 +194,7 @@
1.141 Generic_Target.theory_abbrev prmode ((b, mx), t)),
1.142 declaration = K Generic_Target.theory_declaration,
1.143 syntax_declaration = K Generic_Target.theory_declaration,
1.144 - pretty = single o pretty,
1.145 + pretty = pretty,
1.146 exit = Local_Theory.target_of o conclude}
1.147 end;
1.148