src/Pure/Isar/overloading.ML
author haftmann
Tue Jan 08 11:37:27 2008 +0100 (2008-01-08)
changeset 25861 494d9301cc75
parent 25606 23d34f86b88f
child 26238 c30bb8182da2
permissions -rw-r--r--
refined overloading target
haftmann@25519
     1
(*  Title:      Pure/Isar/overloading.ML
haftmann@25519
     2
    ID:         $Id$
haftmann@25519
     3
    Author:     Florian Haftmann, TU Muenchen
haftmann@25519
     4
haftmann@25519
     5
Overloaded definitions without any discipline.
haftmann@25519
     6
*)
haftmann@25519
     7
haftmann@25519
     8
signature OVERLOADING =
haftmann@25519
     9
sig
haftmann@25861
    10
  val init: (string * (string * typ) * bool) list -> theory -> local_theory
haftmann@25519
    11
  val conclude: local_theory -> local_theory
haftmann@25519
    12
  val declare: string * typ -> theory -> term * theory
haftmann@25519
    13
  val confirm: string -> local_theory -> local_theory
haftmann@25519
    14
  val define: bool -> string -> string * term -> theory -> thm * theory
haftmann@25519
    15
  val operation: Proof.context -> string -> (string * bool) option
haftmann@25606
    16
  val pretty: Proof.context -> Pretty.T
haftmann@25519
    17
end;
haftmann@25519
    18
haftmann@25519
    19
structure Overloading: OVERLOADING =
haftmann@25519
    20
struct
haftmann@25519
    21
haftmann@25519
    22
(* bookkeeping *)
haftmann@25519
    23
haftmann@25519
    24
structure OverloadingData = ProofDataFun
haftmann@25519
    25
(
haftmann@25519
    26
  type T = ((string * typ) * (string * bool)) list;
haftmann@25519
    27
  fun init _ = [];
haftmann@25519
    28
);
haftmann@25519
    29
haftmann@25519
    30
val get_overloading = OverloadingData.get o LocalTheory.target_of;
haftmann@25519
    31
val map_overloading = LocalTheory.target o OverloadingData.map;
haftmann@25519
    32
haftmann@25519
    33
fun operation lthy v = get_overloading lthy
haftmann@25519
    34
  |> get_first (fn ((c, _), (v', checked)) => if v = v' then SOME (c, checked) else NONE);
haftmann@25519
    35
haftmann@25519
    36
fun confirm c = map_overloading (filter_out (fn (_, (c', _)) => c' = c));
haftmann@25519
    37
haftmann@25519
    38
haftmann@25519
    39
(* overloaded declarations and definitions *)
haftmann@25519
    40
haftmann@25519
    41
fun declare c_ty = pair (Const c_ty);
haftmann@25519
    42
haftmann@25519
    43
fun define checked name (c, t) =
haftmann@25519
    44
  Thm.add_def (not checked) true (name, Logic.mk_equals (Const (c, Term.fastype_of t), t));
haftmann@25519
    45
haftmann@25519
    46
haftmann@25519
    47
(* syntax *)
haftmann@25519
    48
haftmann@25536
    49
fun subst_operation overloading = map_aterms (fn t as Const (c, ty) =>
haftmann@25536
    50
    (case AList.lookup (op =) overloading (c, ty)
haftmann@25536
    51
     of SOME (v, _) => Free (v, ty)
haftmann@25536
    52
      | NONE => t)
haftmann@25536
    53
  | t => t);
haftmann@25536
    54
haftmann@25519
    55
fun term_check ts lthy =
haftmann@25519
    56
  let
haftmann@25519
    57
    val overloading = get_overloading lthy;
haftmann@25536
    58
    val ts' = map (subst_operation overloading) ts;
haftmann@25519
    59
  in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', lthy) end;
haftmann@25519
    60
haftmann@25519
    61
fun term_uncheck ts lthy =
haftmann@25519
    62
  let
haftmann@25519
    63
    val overloading = get_overloading lthy;
haftmann@25606
    64
    fun subst (t as Free (v, ty)) = (case get_first (fn ((c, _), (v', _)) =>
haftmann@25606
    65
        if v = v' then SOME c else NONE) overloading
haftmann@25519
    66
         of SOME c => Const (c, ty)
haftmann@25519
    67
          | NONE => t)
haftmann@25519
    68
      | subst t = t;
haftmann@25519
    69
    val ts' = (map o map_aterms) subst ts;
haftmann@25519
    70
  in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', lthy) end;
haftmann@25519
    71
haftmann@25519
    72
haftmann@25519
    73
(* target *)
haftmann@25519
    74
haftmann@25519
    75
fun init overloading thy =
haftmann@25519
    76
  let
haftmann@25519
    77
    val _ = if null overloading then error "At least one parameter must be given" else ();
haftmann@25519
    78
  in
haftmann@25519
    79
    thy
haftmann@25519
    80
    |> ProofContext.init
haftmann@25861
    81
    |> OverloadingData.put (map (fn (v, c_ty, checked) => (c_ty, (v, checked))) overloading)
haftmann@25861
    82
    |> fold (fn (v, (_, ty), _) => Variable.declare_term (Free (v, ty))) overloading
haftmann@25519
    83
    |> Context.proof_map (
haftmann@25519
    84
        Syntax.add_term_check 0 "overloading" term_check
haftmann@25519
    85
        #> Syntax.add_term_uncheck 0 "overloading" term_uncheck)
haftmann@25519
    86
  end;
haftmann@25519
    87
haftmann@25519
    88
fun conclude lthy =
haftmann@25519
    89
  let
haftmann@25519
    90
    val overloading = get_overloading lthy;
haftmann@25519
    91
    val _ = if null overloading then () else
haftmann@25519
    92
      error ("Missing definition(s) for parameters " ^ commas (map (quote
haftmann@25519
    93
        o Syntax.string_of_term lthy o Const o fst) overloading));
haftmann@25519
    94
  in
haftmann@25519
    95
    lthy
haftmann@25519
    96
  end;
haftmann@25519
    97
haftmann@25606
    98
fun pretty lthy =
haftmann@25606
    99
  let
haftmann@25606
   100
    val thy = ProofContext.theory_of lthy;
haftmann@25606
   101
    val overloading = get_overloading lthy;
haftmann@25606
   102
    fun pr_operation ((c, ty), (v, _)) =
haftmann@25861
   103
      (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
haftmann@25861
   104
        Pretty.str (Sign.extern_const thy c), Pretty.str "::", Sign.pretty_typ thy ty];
haftmann@25606
   105
  in
haftmann@25606
   106
    (Pretty.block o Pretty.fbreaks)
haftmann@25606
   107
      (Pretty.str "overloading" :: map pr_operation overloading)
haftmann@25606
   108
  end;
haftmann@25606
   109
haftmann@25519
   110
end;