author  obua 
Tue, 13 Sep 2005 17:05:59 +0200  
changeset 17335  7cff05c90a0e 
parent 17227  398a7353ca69 
child 17412  e26cb20ef0cc 
permissions  rwrr 
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 
17203  37 
val (ty_theta, tm_theta) = Pattern.match thry (pat,ob) 
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 

17227  62 
val get_info = Symtab.curried_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; 