Mercurial > urweb

comparison src/core_util.sig @ 626:230654093b51

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
demo/hello compiles with kind polymorphism
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Feb 2009 17:17:01 -0500
parents 3162bbf8e30f
children 54ec237a3028
comparison
equal deleted inserted replaced
625:47947d6e9750 626:230654093b51
28 signature CORE_UTIL = sig 28 signature CORE_UTIL = sig
29 29
30 structure Kind : sig 30 structure Kind : sig
31 val compare : Core.kind * Core.kind -> order 31 val compare : Core.kind * Core.kind -> order
32 32
33 val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB,
34 bind : 'context * string -> 'context}
35 -> ('context, Core.kind, 'state, 'abort) Search.mapfolderB
33 val mapfold : (Core.kind', 'state, 'abort) Search.mapfolder 36 val mapfold : (Core.kind', 'state, 'abort) Search.mapfolder
34 -> (Core.kind, 'state, 'abort) Search.mapfolder 37 -> (Core.kind, 'state, 'abort) Search.mapfolder
35 val map : (Core.kind' -> Core.kind') -> Core.kind -> Core.kind 38 val map : (Core.kind' -> Core.kind') -> Core.kind -> Core.kind
36 val exists : (Core.kind' -> bool) -> Core.kind -> bool 39 val exists : (Core.kind' -> bool) -> Core.kind -> bool
40 val mapB : {kind : 'context -> Core.kind' -> Core.kind',
41 bind : 'context * string -> 'context}
42 -> 'context -> (Core.kind -> Core.kind)
37 end 43 end
38 44
39 structure Con : sig 45 structure Con : sig
40 val compare : Core.con * Core.con -> order 46 val compare : Core.con * Core.con -> order
41 47
42 datatype binder = 48 datatype binder =
43 Rel of string * Core.kind 49 RelK of string
44 | Named of string * int * Core.kind * Core.con option 50 | RelC of string * Core.kind
45 51 | NamedC of string * int * Core.kind * Core.con option
46 val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder, 52
53 val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB,
47 con : ('context, Core.con', 'state, 'abort) Search.mapfolderB, 54 con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
48 bind : 'context * binder -> 'context} 55 bind : 'context * binder -> 'context}
49 -> ('context, Core.con, 'state, 'abort) Search.mapfolderB 56 -> ('context, Core.con, 'state, 'abort) Search.mapfolderB
50 val mapfold : {kind : (Core.kind', 'state, 'abort) Search.mapfolder, 57 val mapfold : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
51 con : (Core.con', 'state, 'abort) Search.mapfolder} 58 con : (Core.con', 'state, 'abort) Search.mapfolder}
53 60
54 val map : {kind : Core.kind' -> Core.kind', 61 val map : {kind : Core.kind' -> Core.kind',
55 con : Core.con' -> Core.con'} 62 con : Core.con' -> Core.con'}
56 -> Core.con -> Core.con 63 -> Core.con -> Core.con
57 64
58 val mapB : {kind : Core.kind' -> Core.kind', 65 val mapB : {kind : 'context -> Core.kind' -> Core.kind',
59 con : 'context -> Core.con' -> Core.con', 66 con : 'context -> Core.con' -> Core.con',
60 bind : 'context * binder -> 'context} 67 bind : 'context * binder -> 'context}
61 -> 'context -> (Core.con -> Core.con) 68 -> 'context -> (Core.con -> Core.con)
62 69
63 val fold : {kind : Core.kind' * 'state -> 'state, 70 val fold : {kind : Core.kind' * 'state -> 'state,
74 81
75 structure Exp : sig 82 structure Exp : sig
76 val compare : Core.exp * Core.exp -> order 83 val compare : Core.exp * Core.exp -> order
77 84
78 datatype binder = 85 datatype binder =
79 RelC of string * Core.kind 86 RelK of string
87 | RelC of string * Core.kind
80 | NamedC of string * int * Core.kind * Core.con option 88 | NamedC of string * int * Core.kind * Core.con option
81 | RelE of string * Core.con 89 | RelE of string * Core.con
82 | NamedE of string * int * Core.con * Core.exp option * string 90 | NamedE of string * int * Core.con * Core.exp option * string
83 91
84 val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder, 92 val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB,
85 con : ('context, Core.con', 'state, 'abort) Search.mapfolderB, 93 con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
86 exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB, 94 exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB,
87 bind : 'context * binder -> 'context} 95 bind : 'context * binder -> 'context}
88 -> ('context, Core.exp, 'state, 'abort) Search.mapfolderB 96 -> ('context, Core.exp, 'state, 'abort) Search.mapfolderB
89 val mapfold : {kind : (Core.kind', 'state, 'abort) Search.mapfolder, 97 val mapfold : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
93 101
94 val map : {kind : Core.kind' -> Core.kind', 102 val map : {kind : Core.kind' -> Core.kind',
95 con : Core.con' -> Core.con', 103 con : Core.con' -> Core.con',
96 exp : Core.exp' -> Core.exp'} 104 exp : Core.exp' -> Core.exp'}
97 -> Core.exp -> Core.exp 105 -> Core.exp -> Core.exp
98 val mapB : {kind : Core.kind' -> Core.kind', 106 val mapB : {kind : 'context -> Core.kind' -> Core.kind',
99 con : 'context -> Core.con' -> Core.con', 107 con : 'context -> Core.con' -> Core.con',
100 exp : 'context -> Core.exp' -> Core.exp', 108 exp : 'context -> Core.exp' -> Core.exp',
101 bind : 'context * binder -> 'context} 109 bind : 'context * binder -> 'context}
102 -> 'context -> (Core.exp -> Core.exp) 110 -> 'context -> (Core.exp -> Core.exp)
103 111
104 val fold : {kind : Core.kind' * 'state -> 'state, 112 val fold : {kind : Core.kind' * 'state -> 'state,
105 con : Core.con' * 'state -> 'state, 113 con : Core.con' * 'state -> 'state,
106 exp : Core.exp' * 'state -> 'state} 114 exp : Core.exp' * 'state -> 'state}
107 -> 'state -> Core.exp -> 'state 115 -> 'state -> Core.exp -> 'state
108 116
109 val foldB : {kind : Core.kind' * 'state -> 'state, 117 val foldB : {kind : 'context * Core.kind' * 'state -> 'state,
110 con : 'context * Core.con' * 'state -> 'state, 118 con : 'context * Core.con' * 'state -> 'state,
111 exp : 'context * Core.exp' * 'state -> 'state, 119 exp : 'context * Core.exp' * 'state -> 'state,
112 bind : 'context * binder -> 'context} 120 bind : 'context * binder -> 'context}
113 -> 'context -> 'state -> Core.exp -> 'state 121 -> 'context -> 'state -> Core.exp -> 'state
114 122
115 val exists : {kind : Core.kind' -> bool, 123 val exists : {kind : Core.kind' -> bool,
116 con : Core.con' -> bool, 124 con : Core.con' -> bool,
117 exp : Core.exp' -> bool} -> Core.exp -> bool 125 exp : Core.exp' -> bool} -> Core.exp -> bool
118 126
119 val existsB : {kind : Core.kind' -> bool, 127 val existsB : {kind : 'context * Core.kind' -> bool,
120 con : 'context * Core.con' -> bool, 128 con : 'context * Core.con' -> bool,
121 exp : 'context * Core.exp' -> bool, 129 exp : 'context * Core.exp' -> bool,
122 bind : 'context * binder -> 'context} 130 bind : 'context * binder -> 'context}
123 -> 'context -> Core.exp -> bool 131 -> 'context -> Core.exp -> bool
124 132
125 val foldMap : {kind : Core.kind' * 'state -> Core.kind' * 'state, 133 val foldMap : {kind : Core.kind' * 'state -> Core.kind' * 'state,
126 con : Core.con' * 'state -> Core.con' * 'state, 134 con : Core.con' * 'state -> Core.con' * 'state,
127 exp : Core.exp' * 'state -> Core.exp' * 'state} 135 exp : Core.exp' * 'state -> Core.exp' * 'state}
128 -> 'state -> Core.exp -> Core.exp * 'state 136 -> 'state -> Core.exp -> Core.exp * 'state
129 val foldMapB : {kind : Core.kind' * 'state -> Core.kind' * 'state, 137 val foldMapB : {kind : 'context * Core.kind' * 'state -> Core.kind' * 'state,
130 con : 'context * Core.con' * 'state -> Core.con' * 'state, 138 con : 'context * Core.con' * 'state -> Core.con' * 'state,
131 exp : 'context * Core.exp' * 'state -> Core.exp' * 'state, 139 exp : 'context * Core.exp' * 'state -> Core.exp' * 'state,
132 bind : 'context * binder -> 'context} 140 bind : 'context * binder -> 'context}
133 -> 'context -> 'state -> Core.exp -> Core.exp * 'state 141 -> 'context -> 'state -> Core.exp -> Core.exp * 'state
134 end 142 end
135 143
136 structure Decl : sig 144 structure Decl : sig
137 datatype binder = datatype Exp.binder 145 datatype binder = datatype Exp.binder
138 146
139 val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder, 147 val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB,
140 con : ('context, Core.con', 'state, 'abort) Search.mapfolderB, 148 con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
141 exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB, 149 exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB,
142 decl : ('context, Core.decl', 'state, 'abort) Search.mapfolderB, 150 decl : ('context, Core.decl', 'state, 'abort) Search.mapfolderB,
143 bind : 'context * binder -> 'context} 151 bind : 'context * binder -> 'context}
144 -> ('context, Core.decl, 'state, 'abort) Search.mapfolderB 152 -> ('context, Core.decl, 'state, 'abort) Search.mapfolderB
157 val foldMap : {kind : Core.kind' * 'state -> Core.kind' * 'state, 165 val foldMap : {kind : Core.kind' * 'state -> Core.kind' * 'state,
158 con : Core.con' * 'state -> Core.con' * 'state, 166 con : Core.con' * 'state -> Core.con' * 'state,
159 exp : Core.exp' * 'state -> Core.exp' * 'state, 167 exp : Core.exp' * 'state -> Core.exp' * 'state,
160 decl : Core.decl' * 'state -> Core.decl' * 'state} 168 decl : Core.decl' * 'state -> Core.decl' * 'state}
161 -> 'state -> Core.decl -> Core.decl * 'state 169 -> 'state -> Core.decl -> Core.decl * 'state
162 val foldMapB : {kind : Core.kind' * 'state -> Core.kind' * 'state, 170 val foldMapB : {kind : 'context * Core.kind' * 'state -> Core.kind' * 'state,
163 con : 'context * Core.con' * 'state -> Core.con' * 'state, 171 con : 'context * Core.con' * 'state -> Core.con' * 'state,
164 exp : 'context * Core.exp' * 'state -> Core.exp' * 'state, 172 exp : 'context * Core.exp' * 'state -> Core.exp' * 'state,
165 decl : 'context * Core.decl' * 'state -> Core.decl' * 'state, 173 decl : 'context * Core.decl' * 'state -> Core.decl' * 'state,
166 bind : 'context * binder -> 'context} 174 bind : 'context * binder -> 'context}
167 -> 'context -> 'state -> Core.decl -> Core.decl * 'state 175 -> 'context -> 'state -> Core.decl -> Core.decl * 'state
175 structure File : sig 183 structure File : sig
176 val maxName : Core.file -> int 184 val maxName : Core.file -> int
177 185
178 datatype binder = datatype Exp.binder 186 datatype binder = datatype Exp.binder
179 187
180 val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder, 188 val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB,
181 con : ('context, Core.con', 'state, 'abort) Search.mapfolderB, 189 con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
182 exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB, 190 exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB,
183 decl : ('context, Core.decl', 'state, 'abort) Search.mapfolderB, 191 decl : ('context, Core.decl', 'state, 'abort) Search.mapfolderB,
184 bind : 'context * binder -> 'context} 192 bind : 'context * binder -> 'context}
185 -> ('context, Core.file, 'state, 'abort) Search.mapfolderB 193 -> ('context, Core.file, 'state, 'abort) Search.mapfolderB
188 con : (Core.con', 'state, 'abort) Search.mapfolder, 196 con : (Core.con', 'state, 'abort) Search.mapfolder,
189 exp : (Core.exp', 'state, 'abort) Search.mapfolder, 197 exp : (Core.exp', 'state, 'abort) Search.mapfolder,
190 decl : (Core.decl', 'state, 'abort) Search.mapfolder} 198 decl : (Core.decl', 'state, 'abort) Search.mapfolder}
191 -> (Core.file, 'state, 'abort) Search.mapfolder 199 -> (Core.file, 'state, 'abort) Search.mapfolder
192 200
193 val mapB : {kind : Core.kind' -> Core.kind', 201 val mapB : {kind : 'context -> Core.kind' -> Core.kind',
194 con : 'context -> Core.con' -> Core.con', 202 con : 'context -> Core.con' -> Core.con',
195 exp : 'context -> Core.exp' -> Core.exp', 203 exp : 'context -> Core.exp' -> Core.exp',
196 decl : 'context -> Core.decl' -> Core.decl', 204 decl : 'context -> Core.decl' -> Core.decl',
197 bind : 'context * binder -> 'context} 205 bind : 'context * binder -> 'context}
198 -> 'context -> Core.file -> Core.file 206 -> 'context -> Core.file -> Core.file