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 |
|
12340
|
29 |
local fun tybind (x,y) = (TVar (x, HOLogic.typeS) , y)
|
10769
|
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;
|