src/HOL/Tools/TFL/thry.ML
author wenzelm
Fri Jul 17 23:11:40 2009 +0200 (2009-07-17)
changeset 32035 8e77b6a250d5
parent 31784 bd3486c57ba3
child 32952 aeb1e44fbc19
permissions -rw-r--r--
tuned/modernized Envir.subst_XXX;
wenzelm@23150
     1
(*  Title:      HOL/Tools/TFL/thry.ML
wenzelm@23150
     2
    ID:         $Id$
wenzelm@23150
     3
    Author:     Konrad Slind, Cambridge University Computer Laboratory
wenzelm@23150
     4
    Copyright   1997  University of Cambridge
wenzelm@23150
     5
*)
wenzelm@23150
     6
wenzelm@23150
     7
signature THRY =
wenzelm@23150
     8
sig
wenzelm@23150
     9
  val match_term: theory -> term -> term -> (term * term) list * (typ * typ) list
wenzelm@23150
    10
  val match_type: theory -> typ -> typ -> (typ * typ) list
wenzelm@23150
    11
  val typecheck: theory -> term -> cterm
wenzelm@23150
    12
  (*datatype facts of various flavours*)
wenzelm@23150
    13
  val match_info: theory -> string -> {constructors: term list, case_const: term} option
wenzelm@23150
    14
  val induct_info: theory -> string -> {constructors: term list, nchotomy: thm} option
wenzelm@23150
    15
  val extract_info: theory -> {case_congs: thm list, case_rewrites: thm list}
wenzelm@23150
    16
end;
wenzelm@23150
    17
wenzelm@23150
    18
structure Thry: THRY =
wenzelm@23150
    19
struct
wenzelm@23150
    20
wenzelm@23150
    21
wenzelm@23150
    22
fun THRY_ERR func mesg = Utils.ERR {module = "Thry", func = func, mesg = mesg};
wenzelm@23150
    23
wenzelm@23150
    24
wenzelm@23150
    25
(*---------------------------------------------------------------------------
wenzelm@23150
    26
 *    Matching
wenzelm@23150
    27
 *---------------------------------------------------------------------------*)
wenzelm@23150
    28
wenzelm@23150
    29
local
wenzelm@23150
    30
wenzelm@23150
    31
fun tybind (ixn, (S, T)) = (TVar (ixn, S), T);
wenzelm@23150
    32
wenzelm@23150
    33
in
wenzelm@23150
    34
wenzelm@23150
    35
fun match_term thry pat ob =
wenzelm@23150
    36
  let
wenzelm@23150
    37
    val (ty_theta, tm_theta) = Pattern.match thry (pat,ob) (Vartab.empty, Vartab.empty);
wenzelm@32035
    38
    fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.subst_type ty_theta T), t)
wenzelm@23150
    39
  in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
wenzelm@23150
    40
  end;
wenzelm@23150
    41
wenzelm@23150
    42
fun match_type thry pat ob =
wenzelm@23150
    43
  map tybind (Vartab.dest (Sign.typ_match thry (pat, ob) Vartab.empty));
wenzelm@23150
    44
wenzelm@23150
    45
end;
wenzelm@23150
    46
wenzelm@23150
    47
wenzelm@23150
    48
(*---------------------------------------------------------------------------
wenzelm@23150
    49
 * Typing
wenzelm@23150
    50
 *---------------------------------------------------------------------------*)
wenzelm@23150
    51
wenzelm@23150
    52
fun typecheck thry t =
wenzelm@23150
    53
  Thm.cterm_of thry t
wenzelm@23150
    54
    handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg
wenzelm@23150
    55
      | TERM (msg, _) => raise THRY_ERR "typecheck" msg;
wenzelm@23150
    56
wenzelm@23150
    57
wenzelm@23150
    58
(*---------------------------------------------------------------------------
wenzelm@23150
    59
 * Get information about datatypes
wenzelm@23150
    60
 *---------------------------------------------------------------------------*)
wenzelm@23150
    61
wenzelm@23150
    62
fun match_info thy dtco =
haftmann@31784
    63
  case (Datatype.get_info thy dtco,
haftmann@31784
    64
         Datatype.get_constrs thy dtco) of
wenzelm@23150
    65
      (SOME { case_name, ... }, SOME constructors) =>
wenzelm@23150
    66
        SOME {case_const = Const (case_name, Sign.the_const_type thy case_name), constructors = map Const constructors}
wenzelm@23150
    67
    | _ => NONE;
wenzelm@23150
    68
haftmann@31784
    69
fun induct_info thy dtco = case Datatype.get_info thy dtco of
wenzelm@23150
    70
        NONE => NONE
wenzelm@23150
    71
      | SOME {nchotomy, ...} =>
wenzelm@23150
    72
          SOME {nchotomy = nchotomy,
haftmann@31784
    73
                constructors = (map Const o the o Datatype.get_constrs thy) dtco};
wenzelm@23150
    74
wenzelm@23150
    75
fun extract_info thy =
haftmann@31784
    76
 let val infos = (map snd o Symtab.dest o Datatype.get_all) thy
wenzelm@23150
    77
 in {case_congs = map (mk_meta_eq o #case_cong) infos,
wenzelm@23150
    78
     case_rewrites = List.concat (map (map mk_meta_eq o #case_rewrites) infos)}
wenzelm@23150
    79
 end;
wenzelm@23150
    80
wenzelm@23150
    81
wenzelm@23150
    82
end;