Reference cells in Shen.

ref-cells.shen

(package ref-cells [ref <-r r->]

 (datatype one-cell-vector
   X : A;
   ________________________________
   (@v X <>) : (one-cell-vector A);

   __________________________________________
   V : (one-cell-vector A) >> V : (vector A);)

 (datatype unit-type
   __________
   [] : unit;)

 (datatype ref-types
   V : (one-cell-vector A);
   _____________________________________________
   (@p (ref-reader V) (ref-writer V)) : (ref A);

   _____________________________________________
   R : (ref A) >> R : ((lazy A) * (A --> unit));)

 (define ref-reader
   { (one-cell-vector A) --> (lazy A) }
   R -> (freeze (<-vector R 1)))

 (define ref-writer
   { (one-cell-vector A) --> A --> unit }
   R X -> (do (vector-> R 1 X) []))

 (define ref
   { A --> (ref A) }
   X -> (let V (@v X <>)
	  (@p (ref-reader V) (ref-writer V))))

 (define <-r
   { (ref A) --> A }
   R -> (thaw (fst R)))

 (define r->
   { (ref A) --> A --> unit }
   R X -> ((snd R) X)))