# HG changeset patch # User haftmann # Date 1197364993 -3600 # Node ID 23d34f86b88fe3513ce1a2d70fc44b08765541a4 # Parent 35a5f7f4b97b9e15a8ed87c0c9a5b15e44afa63e continued diff -r 35a5f7f4b97b -r 23d34f86b88f src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML Tue Dec 11 10:23:12 2007 +0100 +++ b/src/Pure/Isar/overloading.ML Tue Dec 11 10:23:13 2007 +0100 @@ -8,12 +8,12 @@ signature OVERLOADING = sig val init: ((string * typ) * (string * bool)) list -> theory -> local_theory - val prep_spec: local_theory -> term -> term val conclude: local_theory -> local_theory val declare: string * typ -> theory -> term * theory val confirm: string -> local_theory -> local_theory val define: bool -> string -> string * term -> theory -> thm * theory val operation: Proof.context -> string -> (string * bool) option + val pretty: Proof.context -> Pretty.T end; structure Overloading: OVERLOADING = @@ -52,11 +52,6 @@ | NONE => t) | t => t); -fun prep_spec lthy = - let - val overloading = get_overloading lthy; - in subst_operation overloading end; - fun term_check ts lthy = let val overloading = get_overloading lthy; @@ -66,7 +61,8 @@ fun term_uncheck ts lthy = let val overloading = get_overloading lthy; - fun subst (t as Free (v, ty)) = (case get_first (fn ((c, _), (v', _)) => if v = v' then SOME c else NONE) overloading + fun subst (t as Free (v, ty)) = (case get_first (fn ((c, _), (v', _)) => + if v = v' then SOME c else NONE) overloading of SOME c => Const (c, ty) | NONE => t) | subst t = t; @@ -79,11 +75,12 @@ fun init overloading thy = let val _ = if null overloading then error "At least one parameter must be given" else (); + fun declare ((_, ty), (v, _ )) = Variable.declare_term (Free (v, ty)); in thy |> ProofContext.init |> OverloadingData.put overloading - |> fold (Variable.declare_term o Logic.mk_type o snd o fst) overloading + |> fold declare overloading |> Context.proof_map ( Syntax.add_term_check 0 "overloading" term_check #> Syntax.add_term_uncheck 0 "overloading" term_uncheck) @@ -99,4 +96,16 @@ lthy end; +fun pretty lthy = + let + val thy = ProofContext.theory_of lthy; + val overloading = get_overloading lthy; + fun pr_operation ((c, ty), (v, _)) = + (Pretty.block o Pretty.breaks) [Pretty.str (Sign.extern_const thy c), Pretty.str "::", + Sign.pretty_typ thy ty, Pretty.str "as", Pretty.str v]; + in + (Pretty.block o Pretty.fbreaks) + (Pretty.str "overloading" :: map pr_operation overloading) + end; + end;