149 scheme is called the \emph{more part}. Logically it is just a free |
149 scheme is called the \emph{more part}. Logically it is just a free |
150 variable, which is occasionally referred to as ``row variable'' in |
150 variable, which is occasionally referred to as ``row variable'' in |
151 the literature. The more part of a record scheme may be |
151 the literature. The more part of a record scheme may be |
152 instantiated by zero or more further components. For example, the |
152 instantiated by zero or more further components. For example, the |
153 previous scheme may get instantiated to @{text "\<lparr>x = a, y = b, z = |
153 previous scheme may get instantiated to @{text "\<lparr>x = a, y = b, z = |
154 c, \<dots> = m'"}, where @{text m'} refers to a different more part. |
154 c, \<dots> = m'\<rparr>"}, where @{text m'} refers to a different more part. |
155 Fixed records are special instances of record schemes, where |
155 Fixed records are special instances of record schemes, where |
156 ``@{text "\<dots>"}'' is properly terminated by the @{text "() :: unit"} |
156 ``@{text "\<dots>"}'' is properly terminated by the @{text "() :: unit"} |
157 element. In fact, @{text "\<lparr>x = a, y = b\<rparr>"} is just an abbreviation |
157 element. In fact, @{text "\<lparr>x = a, y = b\<rparr>"} is just an abbreviation |
158 for @{text "\<lparr>x = a, y = b, \<dots> = ()\<rparr>"}. |
158 for @{text "\<lparr>x = a, y = b, \<dots> = ()\<rparr>"}. |
159 |
159 |
241 |
241 |
242 \medskip \textbf{Selectors} and \textbf{updates} are available for |
242 \medskip \textbf{Selectors} and \textbf{updates} are available for |
243 any field (including ``@{text more}''): |
243 any field (including ``@{text more}''): |
244 |
244 |
245 \begin{matharray}{lll} |
245 \begin{matharray}{lll} |
246 @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\ |
246 @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\ |
247 @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow> \<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr>"} \\ |
247 @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\ |
248 \end{matharray} |
248 \end{matharray} |
249 |
249 |
250 There is special syntax for application of updates: @{text "r\<lparr>x := |
250 There is special syntax for application of updates: @{text "r\<lparr>x := |
251 a\<rparr>"} abbreviates term @{text "x_update a r"}. Further notation for |
251 a\<rparr>"} abbreviates term @{text "x_update a r"}. Further notation for |
252 repeated updates is also available: @{text "r\<lparr>x := a\<rparr>\<lparr>y := b\<rparr>\<lparr>z := |
252 repeated updates is also available: @{text "r\<lparr>x := a\<rparr>\<lparr>y := b\<rparr>\<lparr>z := |
260 |
260 |
261 \medskip The \textbf{make} operation provides a cumulative record |
261 \medskip The \textbf{make} operation provides a cumulative record |
262 constructor function: |
262 constructor function: |
263 |
263 |
264 \begin{matharray}{lll} |
264 \begin{matharray}{lll} |
265 @{text "t.make"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr>"} \\ |
265 @{text "t.make"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\ |
266 \end{matharray} |
266 \end{matharray} |
267 |
267 |
268 \medskip We now reconsider the case of non-root records, which are |
268 \medskip We now reconsider the case of non-root records, which are |
269 derived of some parent. In general, the latter may depend on |
269 derived of some parent. In general, the latter may depend on |
270 another parent as well, resulting in a list of \emph{ancestor |
270 another parent as well, resulting in a list of \emph{ancestor |
273 of this by lifting operations over this context of ancestor fields. |
273 of this by lifting operations over this context of ancestor fields. |
274 Assuming that @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"} has ancestor |
274 Assuming that @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"} has ancestor |
275 fields @{text "b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k"}, |
275 fields @{text "b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k"}, |
276 the above record operations will get the following types: |
276 the above record operations will get the following types: |
277 |
277 |
278 \begin{matharray}{lll} |
278 \medskip |
279 @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\ |
279 \begin{tabular}{lll} |
|
280 @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\ |
280 @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow> |
281 @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow> |
281 \<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr> \<Rightarrow> |
282 \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> |
282 \<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr>"} \\ |
283 \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\ |
283 @{text "t.make"} & @{text "::"} & @{text "\<rho>\<^sub>1 \<Rightarrow> \<dots> \<rho>\<^sub>k \<Rightarrow> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> |
284 @{text "t.make"} & @{text "::"} & @{text "\<rho>\<^sub>1 \<Rightarrow> \<dots> \<rho>\<^sub>k \<Rightarrow> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> |
284 \<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n"} \\ |
285 \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\ |
285 \end{matharray} |
286 \end{tabular} |
286 \noindent |
287 \medskip |
287 |
288 |
288 \medskip Some further operations address the extension aspect of a |
289 \noindent Some further operations address the extension aspect of a |
289 derived record scheme specifically: @{text "t.fields"} produces a |
290 derived record scheme specifically: @{text "t.fields"} produces a |
290 record fragment consisting of exactly the new fields introduced here |
291 record fragment consisting of exactly the new fields introduced here |
291 (the result may serve as a more part elsewhere); @{text "t.extend"} |
292 (the result may serve as a more part elsewhere); @{text "t.extend"} |
292 takes a fixed record and adds a given more part; @{text |
293 takes a fixed record and adds a given more part; @{text |
293 "t.truncate"} restricts a record scheme to a fixed record. |
294 "t.truncate"} restricts a record scheme to a fixed record. |
294 |
295 |
295 \begin{matharray}{lll} |
296 \medskip |
296 @{text "t.fields"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n"} \\ |
297 \begin{tabular}{lll} |
297 @{text "t.extend"} & @{text "::"} & @{text "\<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr> \<Rightarrow> |
298 @{text "t.fields"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\ |
298 \<zeta> \<Rightarrow> \<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr>"} \\ |
299 @{text "t.extend"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr> \<Rightarrow> |
299 @{text "t.truncate"} & @{text "::"} & @{text "\<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k, c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr>"} \\ |
300 \<zeta> \<Rightarrow> \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\ |
300 \end{matharray} |
301 @{text "t.truncate"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\ |
|
302 \end{tabular} |
|
303 \medskip |
301 |
304 |
302 \noindent Note that @{text "t.make"} and @{text "t.fields"} coincide |
305 \noindent Note that @{text "t.make"} and @{text "t.fields"} coincide |
303 for root records. |
306 for root records. |
304 *} |
307 *} |
305 |
308 |