wenzelm@10769: (*  Title:      TFL/thry.ML
wenzelm@10769:     ID:         $Id$
wenzelm@10769:     Author:     Konrad Slind, Cambridge University Computer Laboratory
wenzelm@10769:     Copyright   1997  University of Cambridge
wenzelm@10769: *)
wenzelm@10769: 
wenzelm@10769: signature THRY =
wenzelm@10769: sig
wenzelm@10769:   val match_term: theory -> term -> term -> (term * term) list * (typ * typ) list
wenzelm@10769:   val match_type: theory -> typ -> typ -> (typ * typ) list
wenzelm@10769:   val typecheck: theory -> term -> cterm
wenzelm@10769:   (*datatype facts of various flavours*)
wenzelm@10769:   val match_info: theory -> string -> {constructors: term list, case_const: term} option
wenzelm@10769:   val induct_info: theory -> string -> {constructors: term list, nchotomy: thm} option
wenzelm@10769:   val extract_info: theory -> {case_congs: thm list, case_rewrites: thm list}
wenzelm@10769: end;
wenzelm@10769: 
wenzelm@10769: structure Thry: THRY =
wenzelm@10769: struct
wenzelm@10769: 
wenzelm@10769: 
wenzelm@10769: fun THRY_ERR func mesg = Utils.ERR {module = "Thry", func = func, mesg = mesg};
wenzelm@10769: 
wenzelm@10769: 
wenzelm@10769: (*---------------------------------------------------------------------------
wenzelm@10769:  *    Matching
wenzelm@10769:  *---------------------------------------------------------------------------*)
wenzelm@10769: 
wenzelm@12340: local fun tybind (x,y) = (TVar (x, HOLogic.typeS) , y)
wenzelm@10769:       fun tmbind (x,y) = (Var  (x, Term.type_of y), y)
wenzelm@10769: in
wenzelm@10769:  fun match_term thry pat ob =
wenzelm@10769:     let val tsig = Sign.tsig_of (Theory.sign_of thry)
wenzelm@10769:         val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob)
wenzelm@10769:     in (map tmbind tm_theta, map tybind ty_theta)
wenzelm@10769:     end
wenzelm@10769: 
wenzelm@10769:  fun match_type thry pat ob = map tybind (Vartab.dest
wenzelm@10769:    (Type.typ_match (Sign.tsig_of (Theory.sign_of thry)) (Vartab.empty, (pat,ob))))
wenzelm@10769: end;
wenzelm@10769: 
wenzelm@10769: 
wenzelm@10769: (*---------------------------------------------------------------------------
wenzelm@10769:  * Typing
wenzelm@10769:  *---------------------------------------------------------------------------*)
wenzelm@10769: 
wenzelm@10769: fun typecheck thry t =
wenzelm@10769:   Thm.cterm_of (Theory.sign_of thry) t
wenzelm@10769:     handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg
wenzelm@10769:       | TERM (msg, _) => raise THRY_ERR "typecheck" msg;
wenzelm@10769: 
wenzelm@10769: 
wenzelm@10769: (*---------------------------------------------------------------------------
wenzelm@10769:  * Get information about datatypes
wenzelm@10769:  *---------------------------------------------------------------------------*)
wenzelm@10769: 
wenzelm@10769: fun get_info thy ty = Symtab.lookup (DatatypePackage.get_datatypes thy, ty);
wenzelm@10769: 
wenzelm@10769: fun match_info thy tname =
wenzelm@10769:   case (DatatypePackage.case_const_of thy tname, DatatypePackage.constrs_of thy tname) of
skalberg@15531:       (SOME case_const, SOME constructors) =>
skalberg@15531:         SOME {case_const = case_const, constructors = constructors}
skalberg@15531:     | _ => NONE;
wenzelm@10769: 
wenzelm@10769: fun induct_info thy tname = case get_info thy tname of
skalberg@15531:         NONE => NONE
skalberg@15531:       | SOME {nchotomy, ...} =>
skalberg@15531:           SOME {nchotomy = nchotomy,
wenzelm@10769:                 constructors = the (DatatypePackage.constrs_of thy tname)};
wenzelm@10769: 
wenzelm@10769: fun extract_info thy =
wenzelm@10769:  let val infos = map snd (Symtab.dest (DatatypePackage.get_datatypes thy))
wenzelm@10769:  in {case_congs = map (mk_meta_eq o #case_cong) infos,
wenzelm@10769:      case_rewrites = flat (map (map mk_meta_eq o #case_rewrites) infos)}
wenzelm@10769:  end;
wenzelm@10769: 
wenzelm@10769: 
wenzelm@10769: end;