TFL/thry.sml
author wenzelm
Mon Sep 11 18:00:47 2000 +0200 (2000-09-11)
changeset 9924 3370f6aa3200
parent 9867 bf8300fa4238
permissions -rw-r--r--
updated;
wenzelm@9867
     1
(*  Title:      TFL/thry.sml
paulson@3302
     2
    ID:         $Id$
paulson@3302
     3
    Author:     Konrad Slind, Cambridge University Computer Laboratory
paulson@3302
     4
    Copyright   1997  University of Cambridge
paulson@3302
     5
*)
paulson@3302
     6
wenzelm@9867
     7
signature Thry_sig =
wenzelm@9867
     8
sig
wenzelm@9867
     9
  val match_term : theory -> term -> term 
wenzelm@9867
    10
                    -> (term*term)list * (typ*typ)list
wenzelm@9867
    11
wenzelm@9867
    12
  val match_type : theory -> typ -> typ -> (typ*typ)list
wenzelm@9867
    13
wenzelm@9867
    14
  val typecheck : theory -> term -> cterm
wenzelm@9867
    15
wenzelm@9867
    16
  (* Datatype facts of various flavours *)
wenzelm@9867
    17
  val match_info: theory -> string -> {constructors:term list,
wenzelm@9867
    18
                                     case_const:term} option
wenzelm@9867
    19
wenzelm@9867
    20
  val induct_info: theory -> string -> {constructors:term list,
wenzelm@9867
    21
                                      nchotomy:thm} option
wenzelm@9867
    22
wenzelm@9867
    23
  val extract_info: theory -> {case_congs:thm list, case_rewrites:thm list}
wenzelm@9867
    24
wenzelm@9867
    25
end;
wenzelm@9867
    26
wenzelm@9867
    27
paulson@2112
    28
structure Thry : Thry_sig (* LThry_sig *) = 
paulson@2112
    29
struct
paulson@2112
    30
paulson@2112
    31
structure S = USyntax;
paulson@2112
    32
paulson@2112
    33
fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg};
paulson@2112
    34
paulson@2112
    35
(*---------------------------------------------------------------------------
paulson@2112
    36
 *    Matching 
paulson@2112
    37
 *---------------------------------------------------------------------------*)
paulson@2112
    38
paulson@3353
    39
local fun tybind (x,y) = (TVar (x,["term"]) , y)
paulson@3353
    40
      fun tmbind (x,y) = (Var  (x,type_of y), y)
paulson@2112
    41
in
paulson@2112
    42
 fun match_term thry pat ob = 
wenzelm@6397
    43
    let val tsig = #tsig(Sign.rep_sg(Theory.sign_of thry))
paulson@2112
    44
        val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob)
paulson@2112
    45
    in (map tmbind tm_theta, map tybind ty_theta)
paulson@2112
    46
    end
paulson@2112
    47
berghofe@8416
    48
 fun match_type thry pat ob = map tybind (Vartab.dest
berghofe@8416
    49
   (Type.typ_match (#tsig(Sign.rep_sg(Theory.sign_of thry))) (Vartab.empty, (pat,ob))))
paulson@2112
    50
end;
paulson@2112
    51
paulson@2112
    52
paulson@2112
    53
(*---------------------------------------------------------------------------
paulson@2112
    54
 * Typing 
paulson@2112
    55
 *---------------------------------------------------------------------------*)
paulson@2112
    56
wenzelm@6397
    57
fun typecheck thry = Thm.cterm_of (Theory.sign_of thry);
paulson@2112
    58
paulson@2112
    59
paulson@2112
    60
(*---------------------------------------------------------------------------
berghofe@5193
    61
 * Get information about datatypes
paulson@2112
    62
 *---------------------------------------------------------------------------*)
wenzelm@4107
    63
berghofe@5193
    64
fun get_info thy ty = Symtab.lookup (DatatypePackage.get_datatypes thy, ty);
wenzelm@4107
    65
berghofe@5193
    66
fun match_info thy tname =
berghofe@5193
    67
  case (DatatypePackage.case_const_of thy tname, DatatypePackage.constrs_of thy tname) of
berghofe@5193
    68
      (Some case_const, Some constructors) =>
berghofe@5193
    69
        Some {case_const = case_const, constructors = constructors}
berghofe@5193
    70
    | _ => None;
paulson@2112
    71
berghofe@5193
    72
fun induct_info thy tname = case get_info thy tname of
berghofe@5193
    73
        None => None
berghofe@5193
    74
      | Some {nchotomy, ...} =>
berghofe@5193
    75
          Some {nchotomy = nchotomy,
berghofe@5193
    76
                constructors = the (DatatypePackage.constrs_of thy tname)};
paulson@2112
    77
berghofe@5193
    78
fun extract_info thy =
berghofe@5193
    79
 let val infos = map snd (Symtab.dest (DatatypePackage.get_datatypes thy))
berghofe@5193
    80
 in {case_congs = map (mk_meta_eq o #case_cong) infos,
berghofe@5193
    81
     case_rewrites = flat (map (map mk_meta_eq o #case_rewrites) infos)}
paulson@2112
    82
 end;
paulson@2112
    83
paulson@2112
    84
end; (* Thry *)