# File thry.ML

    (*  Title:      TFL/thry.ML
        ID:         $Id: thry.ML,v 1.9 2005/09/15 15:17:00 wenzelm Exp $
        Author:     Konrad Slind, Cambridge University Computer Laboratory
        Copyright   1997  University of Cambridge
    *)

    signature THRY =
    sig
      val match_term: theory -> term -> term -> (term * term) list * (typ * typ) list
      val match_type: theory -> typ -> typ -> (typ * typ) list
      val typecheck: theory -> term -> cterm
      (*datatype facts of various flavours*)
      val match_info: theory -> string -> {constructors: term list, case_const: term} option
      val induct_info: theory -> string -> {constructors: term list, nchotomy: thm} option
      val extract_info: theory -> {case_congs: thm list, case_rewrites: thm list}
    end;

    structure Thry: THRY =
    struct

    fun THRY_ERR func mesg = Utils.ERR {module = "Thry", func = func, mesg = mesg};

    (*---------------------------------------------------------------------------
     *    Matching
     *---------------------------------------------------------------------------*)

    local

    fun tybind (ixn, (S, T)) = (TVar (ixn, S), T);

    in

    fun match_term thry pat ob =
      let
        val (ty_theta, tm_theta) = Pattern.match thry (pat,ob)
        fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t)
      in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
      end;

    fun match_type thry pat ob =
      map tybind (Vartab.dest (Sign.typ_match thry (pat, ob) Vartab.empty));

    end;

    (*---------------------------------------------------------------------------
     * Typing
     *---------------------------------------------------------------------------*)

    fun typecheck thry t =
      Thm.cterm_of thry t
        handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg
          | TERM (msg, _) => raise THRY_ERR "typecheck" msg;

    (*---------------------------------------------------------------------------
     * Get information about datatypes
     *---------------------------------------------------------------------------*)

    val get_info = Symtab.lookup o DatatypePackage.get_datatypes;

    fun match_info thy tname =
      case (DatatypePackage.case_const_of thy tname, DatatypePackage.constrs_of thy tname) of
          (SOME case_const, SOME constructors) =>
            SOME {case_const = case_const, constructors = constructors}
        | _ => NONE;

    fun induct_info thy tname = case get_info thy tname of
            NONE => NONE
          | SOME {nchotomy, ...} =>
              SOME {nchotomy = nchotomy,
                    constructors = valOf (DatatypePackage.constrs_of thy tname)};

    fun extract_info thy =
     let val infos = map snd (Symtab.dest (DatatypePackage.get_datatypes thy))
     in {case_congs = map (mk_meta_eq o #case_cong) infos,
         case_rewrites = List.concat (map (map mk_meta_eq o #case_rewrites) infos)}
     end;

    end;