TFL/thry.ML
author kleing
Sat, 17 Apr 2004 00:46:22 +0200
changeset 14610 9c2e31e483b2
parent 12340 24d31d47af1a
child 15531 08c8dad8e399
permissions -rw-r--r--
added HOL-Matrix, added HOL/Matrix/ROOT.ML
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10769
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      TFL/thry.ML
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     3
    Author:     Konrad Slind, Cambridge University Computer Laboratory
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     4
    Copyright   1997  University of Cambridge
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     5
*)
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     6
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     7
signature THRY =
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     8
sig
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
     9
  val match_term: theory -> term -> term -> (term * term) list * (typ * typ) list
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    10
  val match_type: theory -> typ -> typ -> (typ * typ) list
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    11
  val typecheck: theory -> term -> cterm
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    12
  (*datatype facts of various flavours*)
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    13
  val match_info: theory -> string -> {constructors: term list, case_const: term} option
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    14
  val induct_info: theory -> string -> {constructors: term list, nchotomy: thm} option
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    15
  val extract_info: theory -> {case_congs: thm list, case_rewrites: thm list}
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    16
end;
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    17
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    18
structure Thry: THRY =
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    19
struct
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    20
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    21
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    22
fun THRY_ERR func mesg = Utils.ERR {module = "Thry", func = func, mesg = mesg};
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    23
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    24
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    25
(*---------------------------------------------------------------------------
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    26
 *    Matching
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    27
 *---------------------------------------------------------------------------*)
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    28
12340
24d31d47af1a HOLogic.typeS;
wenzelm
parents: 10769
diff changeset
    29
local fun tybind (x,y) = (TVar (x, HOLogic.typeS) , y)
10769
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    30
      fun tmbind (x,y) = (Var  (x, Term.type_of y), y)
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    31
in
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    32
 fun match_term thry pat ob =
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    33
    let val tsig = Sign.tsig_of (Theory.sign_of thry)
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    34
        val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob)
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    35
    in (map tmbind tm_theta, map tybind ty_theta)
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    36
    end
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    37
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    38
 fun match_type thry pat ob = map tybind (Vartab.dest
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    39
   (Type.typ_match (Sign.tsig_of (Theory.sign_of thry)) (Vartab.empty, (pat,ob))))
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    40
end;
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    41
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    42
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    43
(*---------------------------------------------------------------------------
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    44
 * Typing
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    45
 *---------------------------------------------------------------------------*)
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    46
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    47
fun typecheck thry t =
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    48
  Thm.cterm_of (Theory.sign_of thry) t
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    49
    handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    50
      | TERM (msg, _) => raise THRY_ERR "typecheck" msg;
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    51
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    52
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    53
(*---------------------------------------------------------------------------
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    54
 * Get information about datatypes
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    55
 *---------------------------------------------------------------------------*)
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    56
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    57
fun get_info thy ty = Symtab.lookup (DatatypePackage.get_datatypes thy, ty);
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    58
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    59
fun match_info thy tname =
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    60
  case (DatatypePackage.case_const_of thy tname, DatatypePackage.constrs_of thy tname) of
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    61
      (Some case_const, Some constructors) =>
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    62
        Some {case_const = case_const, constructors = constructors}
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    63
    | _ => None;
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    64
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    65
fun induct_info thy tname = case get_info thy tname of
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    66
        None => None
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    67
      | Some {nchotomy, ...} =>
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    68
          Some {nchotomy = nchotomy,
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    69
                constructors = the (DatatypePackage.constrs_of thy tname)};
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    70
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    71
fun extract_info thy =
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    72
 let val infos = map snd (Symtab.dest (DatatypePackage.get_datatypes thy))
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    73
 in {case_congs = map (mk_meta_eq o #case_cong) infos,
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    74
     case_rewrites = flat (map (map mk_meta_eq o #case_rewrites) infos)}
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    75
 end;
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    76
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    77
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    78
end;