|
| 1 | +(** Unifiable references. |
| 2 | + * |
| 3 | + * Unifiable references provide a Union/Find data type with a ref-like |
| 4 | + * interface. A Union/Find structure consists of a type constructor |
| 5 | + * 'a uref with operations for creating an element of type 'a uref (uRef), |
| 6 | + * getting the contents of an element (!!), checking for equality of |
| 7 | + * two elements (equal), and for unifying two elements (unify). |
| 8 | + *) |
| 9 | + |
| 10 | +signature UREF = sig |
| 11 | + type 'a uref |
| 12 | + |
| 13 | + val uref : 'a -> 'a uref |
| 14 | + val !! : 'a uref -> 'a |
| 15 | + val ::= : 'a uref * 'a -> unit |
| 16 | + |
| 17 | + val unify : ('a * 'a -> 'a) -> 'a uref * 'a uref -> unit |
| 18 | + |
| 19 | + val eq : 'a uref * 'a uref -> bool |
| 20 | + val compare : ('a * 'a -> order) -> 'a uref * 'a uref -> order |
| 21 | +end |
| 22 | + |
| 23 | +(** |
| 24 | +
|
| 25 | +[type 'a uref] is the type of uref-elements with contents of type 'a. |
| 26 | +
|
| 27 | +[uref x] creates a new element with contents x. |
| 28 | +
|
| 29 | +[!!e] returns the contents of e. |
| 30 | +
|
| 31 | +[e ::= x] updates the contents of e to be x. |
| 32 | +
|
| 33 | +[unify f (e, e')] makes e and e' equal; if v and v' are the contents |
| 34 | +of e and e', respectively, before unioning them, then the contents of |
| 35 | +the unioned element is f(v,v'). |
| 36 | +
|
| 37 | +[eq (e, e')] returns true if and only if e and e' are either made by |
| 38 | +the same call to uref or if they have been unioned (see below). |
| 39 | +
|
| 40 | +[compare cmp (e, e')] returns EQUAL if eq (e, e') returns true; |
| 41 | +otherwise return cmp (!!e, !!e'). |
| 42 | +
|
| 43 | +Discussion: |
| 44 | +
|
| 45 | +The uref type constructor is analogous to the ref type constructor as |
| 46 | +expressed in the following table: |
| 47 | +
|
| 48 | + ------------------------------------------------------------------- |
| 49 | + type 'a ref 'a uref |
| 50 | + ------------------------------------------------------------------- |
| 51 | + introduction ref uref |
| 52 | + elimination ! !! |
| 53 | + equality = eq |
| 54 | + updating := ::= |
| 55 | + unioning unify |
| 56 | + ------------------------------------------------------------------- |
| 57 | +
|
| 58 | +The main difference between 'a ref and 'a uref is in the unify |
| 59 | +operation. Without unify, 'a ref and 'a uref can be used |
| 60 | +interchangebly. An assignment to a reference changes only the |
| 61 | +contents of the reference, but not the reference itself. In |
| 62 | +particular, any two pointers that were different (in the sense of the |
| 63 | +equality predicate = returning false) before an assignment will still |
| 64 | +be so. Their contents may or may not be equal after the assignment, |
| 65 | +though. In contrast, applying the unify operation to two uref |
| 66 | +elements makes the two elements themselves equal (in the sense of the |
| 67 | +predicate equal returning true). As a consequence their contents will |
| 68 | +also be identical; the actual content is determined by a binary |
| 69 | +function parameter to unify. |
| 70 | +
|
| 71 | +AUTHOR: |
| 72 | +
|
| 73 | +This software was originally authored by Fritz |
| 74 | +Henglein. Simplifications have been made by Henning Niss (eliminating |
| 75 | +redundant matches) and Martin Elsman (removed some exposed |
| 76 | +functionality such as link and union. |
| 77 | +
|
| 78 | +Copyright (c) 199x-2020 Fritz Henglein, Henning Niss, University of |
| 79 | +Copenhagen. |
| 80 | +
|
| 81 | +*) |
0 commit comments