author  wenzelm 
Sat, 21 Jan 2006 23:02:14 +0100  
changeset 18728  6790126ab5f6 
parent 18163  9b729737bf14 
child 18935  f22be3d61ed5 
permissions  rwrr 
18060  1 
(* Title: Pure/consts.ML 
2 
ID: $Id$ 

3 
Author: Makarius 

4 

5 
Polymorphic constants. 

6 
*) 

7 

8 
signature CONSTS = 

9 
sig 

10 
type T 

11 
val dest: T > {declarations: typ NameSpace.table, constraints: typ NameSpace.table} 

12 
val space: T > NameSpace.T 

13 
val declaration: T > string > typ (*exception TYPE*) 

14 
val constraint: T > string > typ (*exception TYPE*) 

15 
val monomorphic: T > string > bool 

18146  16 
val typargs: T > string * typ > typ list 
18163  17 
val instance: T > string * typ list > typ 
18060  18 
val declare: NameSpace.naming > bstring * typ > T > T 
19 
val constrain: string * typ > T > T 

20 
val hide: bool > string > T > T 

21 
val empty: T 

22 
val merge: T * T > T 

23 
end 

24 

25 
structure Consts: CONSTS = 

26 
struct 

27 

28 

29 
(** datatype T **) 

30 

31 
datatype T = Consts of 

18117
61a430a67d7c
const args: do not store variable names (unused);
wenzelm
parents:
18065
diff
changeset

32 
{declarations: ((typ * int list list) * serial) NameSpace.table, 
18060  33 
constraints: typ Symtab.table}; 
34 

35 
fun make_consts (declarations, constraints) = 

36 
Consts {declarations = declarations, constraints = constraints}; 

37 

38 
fun map_consts f (Consts {declarations, constraints}) = 

39 
make_consts (f (declarations, constraints)); 

40 

41 
fun dest (Consts {declarations = (space, decls), constraints}) = 

42 
{declarations = (space, Symtab.map (#1 o #1) decls), 

43 
constraints = (space, constraints)}; 

44 

45 
fun space (Consts {declarations = (space, _), ...}) = space; 

46 

47 

48 
(* lookup consts *) 

49 

50 
fun the_const (Consts {declarations = (_, decls), ...}) c = 

51 
(case Symtab.lookup decls c of SOME (decl, _) => decl 

52 
 NONE => raise TYPE ("Undeclared constant " ^ quote c, [], [])); 

53 

54 
fun declaration consts c = #1 (the_const consts c); 

55 

56 
fun constraint (consts as Consts {constraints, ...}) c = 

57 
(case Symtab.lookup constraints c of 

58 
SOME T => T 

59 
 NONE => declaration consts c); 

60 

61 
fun monomorphic consts c = null (#2 (the_const consts c)); 

62 

63 

64 
(* typargs  view actual const type as instance of declaration *) 

65 

66 
fun sub (Type (_, Ts)) (i :: is) = sub (nth Ts i) is 

67 
 sub T [] = T 

68 
 sub T _ = raise Subscript; 

69 

18146  70 
fun typargs consts (c, T) = map (sub T) (#2 (the_const consts c)); 
18060  71 

18163  72 
fun instance consts (c, Ts) = 
73 
let 

74 
val declT = declaration consts c; 

75 
val vars = map Term.dest_TVar (typargs consts (c, declT)); 

76 
in declT > Term.instantiateT (vars ~~ Ts) end; 

77 

18060  78 

79 

80 
(** build consts **) 

81 

82 
fun err_dup_consts cs = 

83 
error ("Duplicate declaration of constant(s) " ^ commas_quote cs); 

84 

85 
fun err_inconsistent_constraints cs = 

86 
error ("Inconsistent type constraints for constant(s) " ^ commas_quote cs); 

87 

88 

89 
(* declarations etc. *) 

90 

91 
fun args_of declT = 

92 
let 

93 
fun args (Type (_, Ts)) pos = args_list Ts 0 pos 

94 
 args (TVar v) pos = insert (eq_fst op =) (v, rev pos) 

95 
 args (TFree _) _ = I 

96 
and args_list (T :: Ts) i is = args T (i :: is) #> args_list Ts (i + 1) is 

97 
 args_list [] _ _ = I; 

18117
61a430a67d7c
const args: do not store variable names (unused);
wenzelm
parents:
18065
diff
changeset

98 
in map #2 (rev (args declT [] [])) end; 
18060  99 

100 
fun declare naming (c, T) = map_consts (apfst (fn declarations => 

101 
let 

102 
val decl = (c, ((T, args_of T), serial ())); 

103 
val declarations' = NameSpace.extend_table naming (declarations, [decl]) 

104 
handle Symtab.DUPS cs => err_dup_consts cs; 

105 
in declarations' end)); 

106 

107 
val constrain = map_consts o apsnd o Symtab.update; 

108 

109 
fun hide fully c = map_consts (apfst (apfst (NameSpace.hide fully c))); 

110 

111 

112 
(* empty and merge *) 

113 

114 
val empty = make_consts (NameSpace.empty_table, Symtab.empty); 

115 

116 
fun merge 

117 
(Consts {declarations = declarations1, constraints = constraints1}, 

118 
Consts {declarations = declarations2, constraints = constraints2}) = 

119 
let 

120 
val declarations = NameSpace.merge_tables (eq_snd (op =)) (declarations1, declarations2) 

121 
handle Symtab.DUPS cs => err_dup_consts cs; 

122 
val constraints = Symtab.merge (op =) (constraints1, constraints2) 

123 
handle Symtab.DUPS cs => err_inconsistent_constraints cs; 

124 
in make_consts (declarations, constraints) end; 

125 

126 
end; 