author  paulson 
Fri, 29 Apr 2005 18:13:28 +0200  
changeset 15890  ff6787d730d5 
parent 15798  016f3be5a5ec 
child 16935  4d7f19d340e8 
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 
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset

37 
val tsig = Sign.tsig_of (Theory.sign_of thry) 
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset

38 
val (ty_theta, tm_theta) = Pattern.match tsig (pat,ob) 
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset

39 
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

40 
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

41 
end; 
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset

42 

016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset

43 
fun match_type thry pat ob = map tybind (Vartab.dest 
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset

44 
(Type.typ_match (Sign.tsig_of (Theory.sign_of thry)) (Vartab.empty, (pat, ob)))); 
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15570
diff
changeset

45 

10769  46 
end; 
47 

48 

49 
(* 

50 
* Typing 

51 
**) 

52 

53 
fun typecheck thry t = 

54 
Thm.cterm_of (Theory.sign_of thry) t 

55 
handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg 

56 
 TERM (msg, _) => raise THRY_ERR "typecheck" msg; 

57 

58 

59 
(* 

60 
* Get information about datatypes 

61 
**) 

62 

63 
fun get_info thy ty = Symtab.lookup (DatatypePackage.get_datatypes thy, ty); 

64 

65 
fun match_info thy tname = 

66 
case (DatatypePackage.case_const_of thy tname, DatatypePackage.constrs_of thy tname) of 

15531  67 
(SOME case_const, SOME constructors) => 
68 
SOME {case_const = case_const, constructors = constructors} 

69 
 _ => NONE; 

10769  70 

71 
fun induct_info thy tname = case get_info thy tname of 

15531  72 
NONE => NONE 
73 
 SOME {nchotomy, ...} => 

74 
SOME {nchotomy = nchotomy, 

15570  75 
constructors = valOf (DatatypePackage.constrs_of thy tname)}; 
10769  76 

77 
fun extract_info thy = 

78 
let val infos = map snd (Symtab.dest (DatatypePackage.get_datatypes thy)) 

79 
in {case_congs = map (mk_meta_eq o #case_cong) infos, 

15570  80 
case_rewrites = List.concat (map (map mk_meta_eq o #case_rewrites) infos)} 
10769  81 
end; 
82 

83 

84 
end; 