TFL/thry.sml
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5193 5f6f7195dacf
child 6397 e70ae9b575cc
permissions -rw-r--r--
tidying
paulson@3302
     1
(*  Title:      TFL/thry
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
paulson@2112
     7
structure Thry : Thry_sig (* LThry_sig *) = 
paulson@2112
     8
struct
paulson@2112
     9
paulson@2112
    10
structure S = USyntax;
paulson@2112
    11
paulson@2112
    12
fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg};
paulson@2112
    13
paulson@2112
    14
(*---------------------------------------------------------------------------
paulson@2112
    15
 *    Matching 
paulson@2112
    16
 *---------------------------------------------------------------------------*)
paulson@2112
    17
paulson@3353
    18
local fun tybind (x,y) = (TVar (x,["term"]) , y)
paulson@3353
    19
      fun tmbind (x,y) = (Var  (x,type_of y), y)
paulson@2112
    20
in
paulson@2112
    21
 fun match_term thry pat ob = 
paulson@2112
    22
    let val tsig = #tsig(Sign.rep_sg(sign_of thry))
paulson@2112
    23
        val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob)
paulson@2112
    24
    in (map tmbind tm_theta, map tybind ty_theta)
paulson@2112
    25
    end
paulson@2112
    26
paulson@2112
    27
 fun match_type thry pat ob = 
paulson@2112
    28
    map tybind(Type.typ_match (#tsig(Sign.rep_sg(sign_of thry))) ([],(pat,ob)))
paulson@2112
    29
end;
paulson@2112
    30
paulson@2112
    31
paulson@2112
    32
(*---------------------------------------------------------------------------
paulson@2112
    33
 * Typing 
paulson@2112
    34
 *---------------------------------------------------------------------------*)
paulson@2112
    35
paulson@2112
    36
fun typecheck thry = cterm_of (sign_of thry);
paulson@2112
    37
paulson@2112
    38
paulson@2112
    39
(*---------------------------------------------------------------------------
berghofe@5193
    40
 * Get information about datatypes
paulson@2112
    41
 *---------------------------------------------------------------------------*)
wenzelm@4107
    42
berghofe@5193
    43
fun get_info thy ty = Symtab.lookup (DatatypePackage.get_datatypes thy, ty);
wenzelm@4107
    44
berghofe@5193
    45
fun match_info thy tname =
berghofe@5193
    46
  case (DatatypePackage.case_const_of thy tname, DatatypePackage.constrs_of thy tname) of
berghofe@5193
    47
      (Some case_const, Some constructors) =>
berghofe@5193
    48
        Some {case_const = case_const, constructors = constructors}
berghofe@5193
    49
    | _ => None;
paulson@2112
    50
berghofe@5193
    51
fun induct_info thy tname = case get_info thy tname of
berghofe@5193
    52
        None => None
berghofe@5193
    53
      | Some {nchotomy, ...} =>
berghofe@5193
    54
          Some {nchotomy = nchotomy,
berghofe@5193
    55
                constructors = the (DatatypePackage.constrs_of thy tname)};
paulson@2112
    56
berghofe@5193
    57
fun extract_info thy =
berghofe@5193
    58
 let val infos = map snd (Symtab.dest (DatatypePackage.get_datatypes thy))
berghofe@5193
    59
 in {case_congs = map (mk_meta_eq o #case_cong) infos,
berghofe@5193
    60
     case_rewrites = flat (map (map mk_meta_eq o #case_rewrites) infos)}
paulson@2112
    61
 end;
paulson@2112
    62
paulson@2112
    63
end; (* Thry *)