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