
1 (* Title: Pure/sorts.ML 

2 ID: $Id$ 

3 Author: Markus Wenzel and Stefan Berghofer, TU Muenchen 

4 

5 Type classes and sorts. 

6 *) 

7 

8 signature SORTS = 

9 sig 

10 type classrel 

11 type arities 

12 val str_of_sort: sort > string 

13 val str_of_arity: string * sort list * sort > string 

14 val class_eq: classrel > class * class > bool 

15 val class_less: classrel > class * class > bool 

16 val class_le: classrel > class * class > bool 

17 val sort_eq: classrel > sort * sort > bool 

18 val sort_less: classrel > sort * sort > bool 

19 val sort_le: classrel > sort * sort > bool 

20 val sorts_le: classrel > sort list * sort list > bool 

21 val inter_class: classrel > class * sort > sort 

22 val inter_sort: classrel > sort * sort > sort 

23 val norm_sort: classrel > sort > sort 

24 val least_sort: classrel > arities > typ > sort 

25 val mg_domain: classrel > arities > string > sort > sort list 

26 val nonempty_sort: classrel > arities > sort list > sort > bool 

27 end; 

28 

29 structure Sorts: SORTS = 

30 struct 

31 

32 

33 (** type classes and sorts **) 

34 

35 (* 

36 Classes denote (possibly empty) collections of types that are 

37 partially ordered by class inclusion. They are represented 

38 symbolically by strings. 

39 

40 Sorts are intersections of finitely many classes. They are 

41 represented by lists of classes. Normal forms of sorts are sorted 

42 lists of minimal classes (wrt. current class inclusion). 

43 

44 (already defined in Pure/term.ML) 

45 *) 

46 

47 

48 (* sort signature information *) 

49 

50 (* 

51 classrel: 

52 association list representing the proper subclass relation; 

53 pairs (c, cs) represent the superclasses cs of c; 

54 

55 arities: 

56 twofold association list of all type arities; (t, ars) means 

57 that type constructor t has the arities ars; an element (c, Ss) of 

58 ars represents the arity t::(Ss)c. 

59 *) 

60 

61 type classrel = (class * class list) list; 

62 type arities = (string * (class * sort list) list) list; 

63 

64 

65 (* print sorts and arities *) 

66 

67 fun str_of_sort [c] = c 

68  str_of_sort cs = enclose "{" "}" (commas cs); 

69 

70 fun str_of_dom Ss = enclose "(" ")" (commas (map str_of_sort Ss)); 

71 

72 fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S 

73  str_of_arity (t, Ss, S) = 

74 t ^ " :: " ^ str_of_dom Ss ^ " " ^ str_of_sort S; 

75 

76 

77 

78 (** equality and inclusion **) 

79 

80 (* classes *) 

81 

82 fun class_eq _ (c1, c2:class) = c1 = c2; 

83 

84 fun class_less classrel (c1, c2) = 

85 (case assoc (classrel, c1) of 

86 Some cs => c2 mem_string cs 

87  None => false); 

88 

89 fun class_le classrel (c1, c2) = 

90 c1 = c2 orelse class_less classrel (c1, c2); 

91 

92 

93 (* sorts *) 

94 

95 fun sort_le classrel (S1, S2) = 

96 forall (fn c2 => exists (fn c1 => class_le classrel (c1, c2)) S1) S2; 

97 

98 fun sorts_le classrel (Ss1, Ss2) = 

99 ListPair.all (sort_le classrel) (Ss1, Ss2); 

100 

101 fun sort_eq classrel (S1, S2) = 

102 sort_le classrel (S1, S2) andalso sort_le classrel (S2, S1); 

103 

104 fun sort_less classrel (S1, S2) = 

105 sort_le classrel (S1, S2) andalso not (sort_le classrel (S2, S1)); 

106 

107 

108 (* normal forms of sorts *) 

109 

110 fun minimal_class classrel S c = 

111 not (exists (fn c' => class_less classrel (c', c)) S); 

112 

113 fun norm_sort classrel S = 

114 sort_strings (distinct (filter (minimal_class classrel S) S)); 

115 

116 

117 

118 (** intersection **) 

119 

120 (*intersect class with sort (preserves minimality)*) (* FIXME tune? *) 

121 fun inter_class classrel (c, S) = 

122 let 

123 fun intr [] = [c] 

124  intr (S' as c' :: c's) = 

125 if class_le classrel (c', c) then S' 

126 else if class_le classrel (c, c') then intr c's 

127 else c' :: intr c's 

128 in intr S end; 

129 

130 (*instersect sorts (preserves minimality)*) 

131 fun inter_sort classrel = foldr (inter_class classrel); 

132 

133 

134 

135 (** sorts of types **) 

136 

137 (* least_sort *) 

138 

139 fun least_sort classrel arities T = 

140 let 

141 fun match_dom Ss (c, Ss') = 

142 if sorts_le classrel (Ss, Ss') then Some c 

143 else None; 

144 

145 fun leastS (Type (a, Ts)) = 

146 norm_sort classrel 

147 (mapfilter (match_dom (map leastS Ts)) (assocs arities a)) 

148  leastS (TFree (_, S)) = S 

149  leastS (TVar (_, S)) = S 

150 in leastS T end; 

151 

152 

153 (* mg_domain *) (*exception TYPE*) 

154 

155 fun mg_dom arities a c = 

156 (case assoc2 (arities, (a, c)) of 

157 None => raise_type ("No way to get " ^ a ^ "::" ^ c ^ ".") [] [] 

158  Some Ss => Ss); 

159 

160 fun mg_domain _ _ _ [] = sys_error "mg_domain" (*don't know number of args!*) 

161  mg_domain classrel arities a S = 

162 let val doms = map (mg_dom arities a) S in 

163 foldl (ListPair.map (inter_sort classrel)) (hd doms, tl doms) 

164 end; 

165 

166 

167 

168 (** nonempty_sort **) 

169 

170 (* FIXME improve: proper sorts; nonbase, nonground types (vars from hyps) *) 

171 fun nonempty_sort classrel _ _ [] = true 

172  nonempty_sort classrel arities hyps S = 

173 exists (exists (fn (c, Ss) => [c] = S andalso null Ss) o snd) arities 

174 orelse exists (fn S' => sort_le classrel (S', S)) hyps; 

175 

176 end; 