src/HOL/Types_To_Sets/unoverload_type.ML
author immler
Tue Jun 12 19:32:42 2018 +0200 (17 months ago)
changeset 68430 b0eb6a91924d
parent 68429 38961724a017
child 68433 f396f5490a8c
permissions -rw-r--r--
tuned
immler@68428
     1
(*  Title:      HOL/Types_To_Sets/unoverload_type.ML
immler@68428
     2
    Author:     Fabian Immler, TU M√ľnchen
immler@68428
     3
immler@68428
     4
Internalize sorts and unoverload parameters of a type variable.
immler@68428
     5
*)
immler@68428
     6
immler@68428
     7
signature UNOVERLOAD_TYPE =
immler@68428
     8
sig
immler@68428
     9
  val unoverload_type: Context.generic -> string -> thm -> thm
immler@68428
    10
  val unoverload_type_attr: string -> attribute
immler@68428
    11
end;
immler@68428
    12
immler@68428
    13
structure Unoverload_Type : UNOVERLOAD_TYPE =
immler@68428
    14
struct
immler@68428
    15
immler@68428
    16
fun those [] = []
immler@68428
    17
  | those (NONE::xs) = those xs
immler@68428
    18
  | those (SOME x::xs) = x::those xs
immler@68428
    19
immler@68428
    20
fun params_of_sort context sort =
immler@68428
    21
  let
immler@68428
    22
    val algebra = Sign.classes_of (Context.theory_of context)
immler@68428
    23
    val params = List.concat (map (Sorts.super_classes algebra) sort) |>
immler@68428
    24
      map (try (Axclass.get_info (Context.theory_of context))) |>
immler@68428
    25
      those |>
immler@68428
    26
      map #params |>
immler@68428
    27
      List.concat
immler@68428
    28
  in params end
immler@68428
    29
immler@68429
    30
fun internalize_sort' ctvar thm =
immler@68429
    31
  let
immler@68429
    32
    val (_, thm') = Internalize_Sort.internalize_sort ctvar thm
immler@68429
    33
    val class_premise = case Thm.prems_of thm' of t::_=> t | [] =>
immler@68430
    34
      raise THM ("internalize_sort': no premise?", 0, [thm'])
immler@68429
    35
    val class_vars = Term.add_tvars class_premise []
immler@68429
    36
    val tvar = case class_vars of [x] => TVar x | _ =>
immler@68430
    37
      raise TERM ("internalize_sort': not one type class variable.", [class_premise])
immler@68429
    38
  in
immler@68429
    39
    (tvar, thm')
immler@68429
    40
  end
immler@68429
    41
immler@68428
    42
fun unoverload_type context s thm =
immler@68428
    43
  let
immler@68428
    44
    val tvars = Term.add_tvars (Thm.prop_of thm) []
immler@68428
    45
    val thy = Context.theory_of context
immler@68428
    46
  in
immler@68428
    47
  case find_first (fn ((n,_), _) => n = s) tvars of NONE =>
immler@68430
    48
    raise THM ("unoverload_type: type variable ("^s^") not in theorem", 0, [thm])
immler@68428
    49
  | SOME (x as (_, sort)) =>
immler@68428
    50
    let
immler@68429
    51
      val (tvar, thm') = internalize_sort' (Thm.global_ctyp_of thy (TVar x)) thm
immler@68428
    52
      val consts = params_of_sort context sort |>
immler@68428
    53
        map (apsnd (map_type_tfree (fn ("'a", _) =>  tvar | x => TFree x)))
immler@68428
    54
    in
immler@68428
    55
      fold (fn c => Unoverloading.unoverload (Thm.global_cterm_of thy (Const c))) consts thm'
immler@68428
    56
    end
immler@68428
    57
  end
immler@68428
    58
immler@68428
    59
val tyN = (Args.context -- Args.typ) >>
immler@68428
    60
  (fn (_, TFree (n, _)) => n
immler@68428
    61
  | (ctxt, t) => error ("Not a type variable: " ^ Syntax.string_of_typ ctxt t))
immler@68428
    62
immler@68428
    63
fun unoverload_type_attr n = Thm.rule_attribute [] (fn context => unoverload_type context n)
immler@68428
    64
immler@68428
    65
val _ = Context.>> (Context.map_theory (Attrib.setup @{binding unoverload_type}
immler@68428
    66
  (tyN >> unoverload_type_attr) "internalize a sort"))
immler@68428
    67
immler@68428
    68
end