src/HOL/Tools/TFL/thry.ML
author wenzelm
Thu, 31 May 2007 13:18:52 +0200
changeset 23150 073a65f0bc40
child 31723 f5cafe803b55
permissions -rw-r--r--
moved TFL files to canonical place;
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);
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    38
    fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t)
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 =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    63
  case (DatatypePackage.get_datatype thy dtco,
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    64
         DatatypePackage.get_datatype_constrs thy dtco) of
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
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    69
fun induct_info thy dtco = case DatatypePackage.get_datatype thy dtco of
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,
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    73
                constructors = (map Const o the o DatatypePackage.get_datatype_constrs thy) dtco};
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 =
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    76
 let val infos = (map snd o Symtab.dest o DatatypePackage.get_datatypes) thy
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    77
 in {case_congs = map (mk_meta_eq o #case_cong) infos,
073a65f0bc40 moved TFL files to canonical place;
wenzelm
parents:
diff changeset
    78
     case_rewrites = List.concat (map (map mk_meta_eq o #case_rewrites) infos)}
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;