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