TFL/thry.ML
author obua
Fri, 16 Sep 2005 21:02:15 +0200
changeset 17440 df77edc4f5d0
parent 17412 e26cb20ef0cc
child 18184 43c4589a9a78
permissions -rw-r--r--
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
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
15798
016f3be5a5ec Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents: 15570
diff changeset
    29
local
016f3be5a5ec Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents: 15570
diff changeset
    30
016f3be5a5ec Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents: 15570
diff changeset
    31
fun tybind (ixn, (S, T)) = (TVar (ixn, S), T);
016f3be5a5ec Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents: 15570
diff changeset
    32
10769
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    33
in
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    34
15798
016f3be5a5ec Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents: 15570
diff changeset
    35
fun match_term thry pat ob =
016f3be5a5ec Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents: 15570
diff changeset
    36
  let
17203
29b2563f5c11 refer to theory instead of low-level tsig;
wenzelm
parents: 16935
diff changeset
    37
    val (ty_theta, tm_theta) = Pattern.match thry (pat,ob)
15798
016f3be5a5ec Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents: 15570
diff changeset
    38
    fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t)
016f3be5a5ec Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents: 15570
diff changeset
    39
  in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
016f3be5a5ec Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents: 15570
diff changeset
    40
  end;
016f3be5a5ec Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents: 15570
diff changeset
    41
16935
4d7f19d340e8 Sign.typ_match;
wenzelm
parents: 15798
diff changeset
    42
fun match_type thry pat ob =
4d7f19d340e8 Sign.typ_match;
wenzelm
parents: 15798
diff changeset
    43
  map tybind (Vartab.dest (Sign.typ_match thry (pat, ob) Vartab.empty));
15798
016f3be5a5ec Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents: 15570
diff changeset
    44
10769
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    45
end;
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    46
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    47
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    48
(*---------------------------------------------------------------------------
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    49
 * Typing
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    50
 *---------------------------------------------------------------------------*)
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    51
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    52
fun typecheck thry t =
17203
29b2563f5c11 refer to theory instead of low-level tsig;
wenzelm
parents: 16935
diff changeset
    53
  Thm.cterm_of thry t
10769
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    54
    handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    55
      | TERM (msg, _) => raise THRY_ERR "typecheck" msg;
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    56
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    57
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    58
(*---------------------------------------------------------------------------
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    59
 * Get information about datatypes
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    60
 *---------------------------------------------------------------------------*)
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    61
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17227
diff changeset
    62
val get_info = Symtab.lookup o DatatypePackage.get_datatypes;
10769
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    63
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    64
fun match_info thy tname =
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    65
  case (DatatypePackage.case_const_of thy tname, DatatypePackage.constrs_of thy tname) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 12340
diff changeset
    66
      (SOME case_const, SOME constructors) =>
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 12340
diff changeset
    67
        SOME {case_const = case_const, constructors = constructors}
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 12340
diff changeset
    68
    | _ => NONE;
10769
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    69
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    70
fun induct_info thy tname = case get_info thy tname of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 12340
diff changeset
    71
        NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 12340
diff changeset
    72
      | SOME {nchotomy, ...} =>
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 12340
diff changeset
    73
          SOME {nchotomy = nchotomy,
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
    74
                constructors = valOf (DatatypePackage.constrs_of thy tname)};
10769
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    75
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    76
fun extract_info thy =
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    77
 let val infos = map snd (Symtab.dest (DatatypePackage.get_datatypes thy))
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    78
 in {case_congs = map (mk_meta_eq o #case_cong) infos,
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
    79
     case_rewrites = List.concat (map (map mk_meta_eq o #case_rewrites) infos)}
10769
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    80
 end;
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    81
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    82
70b9b0cfe05f renamed .sml files to .ML;
wenzelm
parents:
diff changeset
    83
end;