10769

1 
(* Title: TFL/thry.ML


2 
ID: $Id$


3 
Author: Konrad Slind, Cambridge University Computer Laboratory


4 
Copyright 1997 University of Cambridge


5 
*)


6 


7 
signature THRY =


8 
sig


9 
val match_term: theory > term > term > (term * term) list * (typ * typ) list


10 
val match_type: theory > typ > typ > (typ * typ) list


11 
val typecheck: theory > term > cterm


12 
(*datatype facts of various flavours*)


13 
val match_info: theory > string > {constructors: term list, case_const: term} option


14 
val induct_info: theory > string > {constructors: term list, nchotomy: thm} option


15 
val extract_info: theory > {case_congs: thm list, case_rewrites: thm list}


16 
end;


17 


18 
structure Thry: THRY =


19 
struct


20 


21 


22 
fun THRY_ERR func mesg = Utils.ERR {module = "Thry", func = func, mesg = mesg};


23 


24 


25 
(*


26 
* Matching


27 
**)


28 


29 
local fun tybind (x,y) = (TVar (x, HOLogic.termS) , y)


30 
fun tmbind (x,y) = (Var (x, Term.type_of y), y)


31 
in


32 
fun match_term thry pat ob =


33 
let val tsig = Sign.tsig_of (Theory.sign_of thry)


34 
val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob)


35 
in (map tmbind tm_theta, map tybind ty_theta)


36 
end


37 


38 
fun match_type thry pat ob = map tybind (Vartab.dest


39 
(Type.typ_match (Sign.tsig_of (Theory.sign_of thry)) (Vartab.empty, (pat,ob))))


40 
end;


41 


42 


43 
(*


44 
* Typing


45 
**)


46 


47 
fun typecheck thry t =


48 
Thm.cterm_of (Theory.sign_of thry) t


49 
handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg


50 
 TERM (msg, _) => raise THRY_ERR "typecheck" msg;


51 


52 


53 
(*


54 
* Get information about datatypes


55 
**)


56 


57 
fun get_info thy ty = Symtab.lookup (DatatypePackage.get_datatypes thy, ty);


58 


59 
fun match_info thy tname =


60 
case (DatatypePackage.case_const_of thy tname, DatatypePackage.constrs_of thy tname) of


61 
(Some case_const, Some constructors) =>


62 
Some {case_const = case_const, constructors = constructors}


63 
 _ => None;


64 


65 
fun induct_info thy tname = case get_info thy tname of


66 
None => None


67 
 Some {nchotomy, ...} =>


68 
Some {nchotomy = nchotomy,


69 
constructors = the (DatatypePackage.constrs_of thy tname)};


70 


71 
fun extract_info thy =


72 
let val infos = map snd (Symtab.dest (DatatypePackage.get_datatypes thy))


73 
in {case_congs = map (mk_meta_eq o #case_cong) infos,


74 
case_rewrites = flat (map (map mk_meta_eq o #case_rewrites) infos)}


75 
end;


76 


77 


78 
end;
