1 (* Title: HOL/Tools/TFL/thry.ML |
|
2 Author: Konrad Slind, Cambridge University Computer Laboratory |
|
3 *) |
|
4 |
|
5 signature THRY = |
|
6 sig |
|
7 val match_term: theory -> term -> term -> (term * term) list * (typ * typ) list |
|
8 val match_type: theory -> typ -> typ -> (typ * typ) list |
|
9 val typecheck: theory -> term -> cterm |
|
10 (*datatype facts of various flavours*) |
|
11 val match_info: theory -> string -> {constructors: term list, case_const: term} option |
|
12 val induct_info: theory -> string -> {constructors: term list, nchotomy: thm} option |
|
13 val extract_info: theory -> {case_congs: thm list, case_rewrites: thm list} |
|
14 end; |
|
15 |
|
16 structure Thry: THRY = |
|
17 struct |
|
18 |
|
19 |
|
20 fun THRY_ERR func mesg = Utils.ERR {module = "Thry", func = func, mesg = mesg}; |
|
21 |
|
22 |
|
23 (*--------------------------------------------------------------------------- |
|
24 * Matching |
|
25 *---------------------------------------------------------------------------*) |
|
26 |
|
27 local |
|
28 |
|
29 fun tybind (ixn, (S, T)) = (TVar (ixn, S), T); |
|
30 |
|
31 in |
|
32 |
|
33 fun match_term thry pat ob = |
|
34 let |
|
35 val (ty_theta, tm_theta) = Pattern.match thry (pat,ob) (Vartab.empty, Vartab.empty); |
|
36 fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.subst_type ty_theta T), t) |
|
37 in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta)) |
|
38 end; |
|
39 |
|
40 fun match_type thry pat ob = |
|
41 map tybind (Vartab.dest (Sign.typ_match thry (pat, ob) Vartab.empty)); |
|
42 |
|
43 end; |
|
44 |
|
45 |
|
46 (*--------------------------------------------------------------------------- |
|
47 * Typing |
|
48 *---------------------------------------------------------------------------*) |
|
49 |
|
50 fun typecheck thy t = |
|
51 Thm.global_cterm_of thy t |
|
52 handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg |
|
53 | TERM (msg, _) => raise THRY_ERR "typecheck" msg; |
|
54 |
|
55 |
|
56 (*--------------------------------------------------------------------------- |
|
57 * Get information about datatypes |
|
58 *---------------------------------------------------------------------------*) |
|
59 |
|
60 fun match_info thy dtco = |
|
61 case (BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] dtco, |
|
62 BNF_LFP_Compat.get_constrs thy dtco) of |
|
63 (SOME {case_name, ... }, SOME constructors) => |
|
64 SOME {case_const = Const (case_name, Sign.the_const_type thy case_name), constructors = map Const constructors} |
|
65 | _ => NONE; |
|
66 |
|
67 fun induct_info thy dtco = case BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] dtco of |
|
68 NONE => NONE |
|
69 | SOME {nchotomy, ...} => |
|
70 SOME {nchotomy = nchotomy, |
|
71 constructors = (map Const o the o BNF_LFP_Compat.get_constrs thy) dtco}; |
|
72 |
|
73 fun extract_info thy = |
|
74 let val infos = map snd (Symtab.dest (BNF_LFP_Compat.get_all thy [BNF_LFP_Compat.Keep_Nesting])) |
|
75 in {case_congs = map (mk_meta_eq o #case_cong) infos, |
|
76 case_rewrites = maps (map mk_meta_eq o #case_rewrites) infos} |
|
77 end; |
|
78 |
|
79 |
|
80 end; |
|