author | wenzelm |
Wed, 16 Nov 2005 17:45:30 +0100 | |
changeset 18184 | 43c4589a9a78 |
parent 17412 | e26cb20ef0cc |
child 19349 | 36e537f89585 |
permissions | -rw-r--r-- |
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 |
||
15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset
|
29 |
local |
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset
|
30 |
|
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset
|
31 |
fun tybind (ixn, (S, T)) = (TVar (ixn, S), T); |
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset
|
32 |
|
10769 | 33 |
in |
34 |
||
15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset
|
35 |
fun match_term thry pat ob = |
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset
|
36 |
let |
18184 | 37 |
val (ty_theta, tm_theta) = Pattern.match thry (pat,ob) (Vartab.empty, Vartab.empty); |
15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset
|
38 |
fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t) |
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset
|
39 |
in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta)) |
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset
|
40 |
end; |
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset
|
41 |
|
16935 | 42 |
fun match_type thry pat ob = |
43 |
map tybind (Vartab.dest (Sign.typ_match thry (pat, ob) Vartab.empty)); |
|
15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset
|
44 |
|
10769 | 45 |
end; |
46 |
||
47 |
||
48 |
(*--------------------------------------------------------------------------- |
|
49 |
* Typing |
|
50 |
*---------------------------------------------------------------------------*) |
|
51 |
||
52 |
fun typecheck thry t = |
|
17203 | 53 |
Thm.cterm_of thry t |
10769 | 54 |
handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg |
55 |
| TERM (msg, _) => raise THRY_ERR "typecheck" msg; |
|
56 |
||
57 |
||
58 |
(*--------------------------------------------------------------------------- |
|
59 |
* Get information about datatypes |
|
60 |
*---------------------------------------------------------------------------*) |
|
61 |
||
17412 | 62 |
val get_info = Symtab.lookup o DatatypePackage.get_datatypes; |
10769 | 63 |
|
64 |
fun match_info thy tname = |
|
65 |
case (DatatypePackage.case_const_of thy tname, DatatypePackage.constrs_of thy tname) of |
|
15531 | 66 |
(SOME case_const, SOME constructors) => |
67 |
SOME {case_const = case_const, constructors = constructors} |
|
68 |
| _ => NONE; |
|
10769 | 69 |
|
70 |
fun induct_info thy tname = case get_info thy tname of |
|
15531 | 71 |
NONE => NONE |
72 |
| SOME {nchotomy, ...} => |
|
73 |
SOME {nchotomy = nchotomy, |
|
15570 | 74 |
constructors = valOf (DatatypePackage.constrs_of thy tname)}; |
10769 | 75 |
|
76 |
fun extract_info thy = |
|
77 |
let val infos = map snd (Symtab.dest (DatatypePackage.get_datatypes thy)) |
|
78 |
in {case_congs = map (mk_meta_eq o #case_cong) infos, |
|
15570 | 79 |
case_rewrites = List.concat (map (map mk_meta_eq o #case_rewrites) infos)} |
10769 | 80 |
end; |
81 |
||
82 |
||
83 |
end; |