author  krauss 
Mon, 23 Oct 2006 17:46:11 +0200  
changeset 21100  cda93bbf35db 
parent 19349  36e537f89585 
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 
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 

19349  62 
fun match_info thy dtco = 
63 
case (DatatypePackage.get_datatype thy dtco, 

64 
DatatypePackage.get_datatype_constrs thy dtco) of 

65 
(SOME { case_name, ... }, SOME constructors) => 

66 
SOME {case_const = Const (case_name, Sign.the_const_type thy case_name), constructors = map Const constructors} 

15531  67 
 _ => NONE; 
10769  68 

19349  69 
fun induct_info thy dtco = case DatatypePackage.get_datatype thy dtco of 
15531  70 
NONE => NONE 
71 
 SOME {nchotomy, ...} => 

72 
SOME {nchotomy = nchotomy, 

19349  73 
constructors = (map Const o the o DatatypePackage.get_datatype_constrs thy) dtco}; 
10769  74 

75 
fun extract_info thy = 

19349  76 
let val infos = (map snd o Symtab.dest o DatatypePackage.get_datatypes) thy 
10769  77 
in {case_congs = map (mk_meta_eq o #case_cong) infos, 
15570  78 
case_rewrites = List.concat (map (map mk_meta_eq o #case_rewrites) infos)} 
10769  79 
end; 
80 

81 

82 
end; 