TFL/thry.sml
author nipkow
Fri Oct 09 14:19:13 1998 +0200 (1998-10-09)
changeset 5633 fb7fa1b154c4
parent 5193 5f6f7195dacf
child 6397 e70ae9b575cc
permissions -rw-r--r--
Added a few breaks in error text.
     1 (*  Title:      TFL/thry
     2     ID:         $Id$
     3     Author:     Konrad Slind, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 *)
     6 
     7 structure Thry : Thry_sig (* LThry_sig *) = 
     8 struct
     9 
    10 structure S = USyntax;
    11 
    12 fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg};
    13 
    14 (*---------------------------------------------------------------------------
    15  *    Matching 
    16  *---------------------------------------------------------------------------*)
    17 
    18 local fun tybind (x,y) = (TVar (x,["term"]) , y)
    19       fun tmbind (x,y) = (Var  (x,type_of y), y)
    20 in
    21  fun match_term thry pat ob = 
    22     let val tsig = #tsig(Sign.rep_sg(sign_of thry))
    23         val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob)
    24     in (map tmbind tm_theta, map tybind ty_theta)
    25     end
    26 
    27  fun match_type thry pat ob = 
    28     map tybind(Type.typ_match (#tsig(Sign.rep_sg(sign_of thry))) ([],(pat,ob)))
    29 end;
    30 
    31 
    32 (*---------------------------------------------------------------------------
    33  * Typing 
    34  *---------------------------------------------------------------------------*)
    35 
    36 fun typecheck thry = cterm_of (sign_of thry);
    37 
    38 
    39 (*---------------------------------------------------------------------------
    40  * Get information about datatypes
    41  *---------------------------------------------------------------------------*)
    42 
    43 fun get_info thy ty = Symtab.lookup (DatatypePackage.get_datatypes thy, ty);
    44 
    45 fun match_info thy tname =
    46   case (DatatypePackage.case_const_of thy tname, DatatypePackage.constrs_of thy tname) of
    47       (Some case_const, Some constructors) =>
    48         Some {case_const = case_const, constructors = constructors}
    49     | _ => None;
    50 
    51 fun induct_info thy tname = case get_info thy tname of
    52         None => None
    53       | Some {nchotomy, ...} =>
    54           Some {nchotomy = nchotomy,
    55                 constructors = the (DatatypePackage.constrs_of thy tname)};
    56 
    57 fun extract_info thy =
    58  let val infos = map snd (Symtab.dest (DatatypePackage.get_datatypes thy))
    59  in {case_congs = map (mk_meta_eq o #case_cong) infos,
    60      case_rewrites = flat (map (map mk_meta_eq o #case_rewrites) infos)}
    61  end;
    62 
    63 end; (* Thry *)