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