TFL/thry.ML
author nipkow
Wed May 26 14:57:06 2004 +0200 (2004-05-26)
changeset 14804 8de39d3e8eb6
parent 12340 24d31d47af1a
child 15531 08c8dad8e399
permissions -rw-r--r--
Corrected printer bug for bounded quantifiers Q x<=y. P
     1 (*  Title:      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 fun tybind (x,y) = (TVar (x, HOLogic.typeS) , y)
    30       fun tmbind (x,y) = (Var  (x, Term.type_of y), y)
    31 in
    32  fun match_term thry pat ob =
    33     let val tsig = Sign.tsig_of (Theory.sign_of thry)
    34         val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob)
    35     in (map tmbind tm_theta, map tybind ty_theta)
    36     end
    37 
    38  fun match_type thry pat ob = map tybind (Vartab.dest
    39    (Type.typ_match (Sign.tsig_of (Theory.sign_of thry)) (Vartab.empty, (pat,ob))))
    40 end;
    41 
    42 
    43 (*---------------------------------------------------------------------------
    44  * Typing
    45  *---------------------------------------------------------------------------*)
    46 
    47 fun typecheck thry t =
    48   Thm.cterm_of (Theory.sign_of thry) t
    49     handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg
    50       | TERM (msg, _) => raise THRY_ERR "typecheck" msg;
    51 
    52 
    53 (*---------------------------------------------------------------------------
    54  * Get information about datatypes
    55  *---------------------------------------------------------------------------*)
    56 
    57 fun get_info thy ty = Symtab.lookup (DatatypePackage.get_datatypes thy, ty);
    58 
    59 fun match_info thy tname =
    60   case (DatatypePackage.case_const_of thy tname, DatatypePackage.constrs_of thy tname) of
    61       (Some case_const, Some constructors) =>
    62         Some {case_const = case_const, constructors = constructors}
    63     | _ => None;
    64 
    65 fun induct_info thy tname = case get_info thy tname of
    66         None => None
    67       | Some {nchotomy, ...} =>
    68           Some {nchotomy = nchotomy,
    69                 constructors = the (DatatypePackage.constrs_of thy tname)};
    70 
    71 fun extract_info thy =
    72  let val infos = map snd (Symtab.dest (DatatypePackage.get_datatypes thy))
    73  in {case_congs = map (mk_meta_eq o #case_cong) infos,
    74      case_rewrites = flat (map (map mk_meta_eq o #case_rewrites) infos)}
    75  end;
    76 
    77 
    78 end;