1 (* For the moment, we hold the lock while the client function [f] is busy. In 2 a concurrent implementation, we might wish to hold the lock only during a 3 short period. We could release the lock before invoking [f], and acquire it 4 again when [f] is done (suggestion by Guillaume Melquiond). Some thought 5 would be required if we wish to guarantee that [f] is invoked at most once 6 for every input. TEMPORARY *) 7 8 open lock (* new, acquire, release *) 9 open hashtable (* table, create, find, add *) 10 11 (* The simple memoizing combinator. *) 12 13 (* A lock is used to protect the hash table and to allow its use in a 14 duplicable object (the memoized function). *) 15 16 val memoize 17 [a, b, s : perm] 18 duplicable a => duplicable b => 19 (hash: a -> int, eq: (a, a) -> bool, f: (a | s) -> b) 20 : (a | s) -> b = 21 22 (* Create the internal hash table. *) 23 let t = create (11, hash, eq) in 24 (* Create a lock which (at runtime) prevents re-entrant calls 25 into the memoized function and (at type-checking time) allows 26 us to hide the existence of the hash table. *) 27 let l : lock (t @ table a b) = new () in 28 29 (* Now, construct the memoized function. *) 30 fun (x: a | s) : b = 31 (* Acquire the lock. This yields the permission [t @ table a b]. *) 32 acquire l; 33 (* Find [y] in the table, if it is there already, or compute [y] 34 and store it in the table for potential later re-use. *) 35 let y = 36 match find (x, t) with 37 | Some { contents = y } -> 38 y 39 | None -> 40 let y = f x in 41 assert held l; 42 add (x, y, t); 43 y 44 end 45 in 46 (* Release the lock. This consumes [t @ table a b]. *) 47 release l; 48 (* Return [y]. *) 49 y 50 51 (* The recursive memoizing combinator. *) 52 53 (* A technician would say that, by requiring [f] to be polymorphic in [p], we 54 are manually building in an application of the second-order frame rule. 55 This allows us to pass the permission [t @ table a b], disguised as an 56 abstract permission [p], to the function [f], which itself passes it on to 57 [self]. This allows us not to release and re-acquire the lock at every 58 recursive invocation. Incidentally, it guarantees that [f] cannot store 59 [self] and invoke it at a later time. *) 60 61 val fix 62 [a, b] 63 duplicable a => duplicable b => 64 ( 65 hash: a -> int, 66 eq: (a, a) -> bool, 67 f: [p : perm] ((a | p) -> b, a | p) -> b 68 ) 69 : a -> b = 70 71 (* Create the internal hash table and lock. *) 72 let t = create [a, b] (11, hash, eq) in 73 let l : lock (t @ table a b) = new () in 74 75 (* For the sake of efficiency, we prefer not to release and re-acquire 76 the lock at every recursive invocation. Thus, the recursive function 77 that we define below assumes that the lock is held -- hence, the 78 table is available. *) 79 80 (* Construct the recursive function. *) 81 let rec memoized (x: a | t @ table a b) : b = 82 match find (x, t) with 83 | Some { contents = y } -> 84 y 85 | None -> 86 let y = f (memoized, x) in 87 add (x, y, t); 88 y 89 end 90 in 91 92 (* Now, construct the final memoized function. *) 93 fun (x: a) : b = 94 (* Acquire the lock. This yields the permission [t @ table a b]. *) 95 acquire l; 96 (* Invoke the recursive computation. *) 97 let y = memoized x in 98 (* Release the lock. This consumes [t @ table a b]. *) 99 release l; 100 (* Return [y]. *) 101 y 102 103 (* TEMPORARY once the bug is fixed, we might wish [fix] to have type 104 105 val fix 106 [a, b, s : perm] 107 duplicable a => duplicable b => 108 ( 109 hash: a -> int, 110 eq: (a, a) -> bool, 111 f: [p : perm] ((a | p * s) -> b, a | p * s) -> b 112 ) 113 : (a | s) -> b = 114 115 This requires adding *s to memoized, 116 adding |s to the final anonymous function. *) 117 118 (* 119 Local Variables: 120 compile-command: "../mezzo memoize.mz" 121 End: 122 *)