continued
authorhaftmann
Tue Dec 11 10:23:13 2007 +0100 (2007-12-11 ago)
changeset 2560623d34f86b88f
parent 25605 35a5f7f4b97b
child 25607 779c79c36c5e
continued
src/Pure/Isar/overloading.ML
     1.1 --- a/src/Pure/Isar/overloading.ML	Tue Dec 11 10:23:12 2007 +0100
     1.2 +++ b/src/Pure/Isar/overloading.ML	Tue Dec 11 10:23:13 2007 +0100
     1.3 @@ -8,12 +8,12 @@
     1.4  signature OVERLOADING =
     1.5  sig
     1.6    val init: ((string * typ) * (string * bool)) list -> theory -> local_theory
     1.7 -  val prep_spec: local_theory -> term -> term
     1.8    val conclude: local_theory -> local_theory
     1.9    val declare: string * typ -> theory -> term * theory
    1.10    val confirm: string -> local_theory -> local_theory
    1.11    val define: bool -> string -> string * term -> theory -> thm * theory
    1.12    val operation: Proof.context -> string -> (string * bool) option
    1.13 +  val pretty: Proof.context -> Pretty.T
    1.14  end;
    1.15  
    1.16  structure Overloading: OVERLOADING =
    1.17 @@ -52,11 +52,6 @@
    1.18        | NONE => t)
    1.19    | t => t);
    1.20  
    1.21 -fun prep_spec lthy =
    1.22 -  let
    1.23 -    val overloading = get_overloading lthy;
    1.24 -  in subst_operation overloading end;
    1.25 -
    1.26  fun term_check ts lthy =
    1.27    let
    1.28      val overloading = get_overloading lthy;
    1.29 @@ -66,7 +61,8 @@
    1.30  fun term_uncheck ts lthy =
    1.31    let
    1.32      val overloading = get_overloading lthy;
    1.33 -    fun subst (t as Free (v, ty)) = (case get_first (fn ((c, _), (v', _)) => if v = v' then SOME c else NONE) overloading
    1.34 +    fun subst (t as Free (v, ty)) = (case get_first (fn ((c, _), (v', _)) =>
    1.35 +        if v = v' then SOME c else NONE) overloading
    1.36           of SOME c => Const (c, ty)
    1.37            | NONE => t)
    1.38        | subst t = t;
    1.39 @@ -79,11 +75,12 @@
    1.40  fun init overloading thy =
    1.41    let
    1.42      val _ = if null overloading then error "At least one parameter must be given" else ();
    1.43 +    fun declare ((_, ty), (v, _ )) = Variable.declare_term (Free (v, ty));
    1.44    in
    1.45      thy
    1.46      |> ProofContext.init
    1.47      |> OverloadingData.put overloading
    1.48 -    |> fold (Variable.declare_term o Logic.mk_type o snd o fst) overloading
    1.49 +    |> fold declare overloading
    1.50      |> Context.proof_map (
    1.51          Syntax.add_term_check 0 "overloading" term_check
    1.52          #> Syntax.add_term_uncheck 0 "overloading" term_uncheck)
    1.53 @@ -99,4 +96,16 @@
    1.54      lthy
    1.55    end;
    1.56  
    1.57 +fun pretty lthy =
    1.58 +  let
    1.59 +    val thy = ProofContext.theory_of lthy;
    1.60 +    val overloading = get_overloading lthy;
    1.61 +    fun pr_operation ((c, ty), (v, _)) =
    1.62 +      (Pretty.block o Pretty.breaks) [Pretty.str (Sign.extern_const thy c), Pretty.str "::",
    1.63 +        Sign.pretty_typ thy ty, Pretty.str "as", Pretty.str v];
    1.64 +  in
    1.65 +    (Pretty.block o Pretty.fbreaks)
    1.66 +      (Pretty.str "overloading" :: map pr_operation overloading)
    1.67 +  end;
    1.68 +
    1.69  end;