
  0 | module Scratchpad
  1 | 
  2 | import Data.Linear.Ref1
  3 | import Syntax.T1
  4 | 
  5 | %default total
  6 | 
  7 | export prefix 9 ^*
  8 | (^*) : a -> F1 s (Ref s a)
  9 | (^*) = ref1
 10 | 
 11 | export prefix 9 &*
 12 | (&*) : Ref s a -> F1 s a
 13 | (&*) = read1
 14 | 
 15 | export infix 9 =*
 16 | (=*) : Ref s a -> a -> F1' s
 17 | (=*) = write1
 18 | 
 19 | export prefix 0 >*
 20 | (>*) : ({0 s : Type} -> F1 s a) -> a
 21 | (>*) f = run1 f
 22 | 
 23 | export infix 0 `times`
 24 | times : Nat -> F1' s -> F1' s
 25 | times = forN
 26 | 
 27 | fibo : Nat -> Nat
 28 | fibo n =
 29 |    -- `>*` runs a linear computation to completion and returns the result, T1.do
 30 |    -- activates the syntax sugar for making the token passing implicit
 31 |    >*T1.do
 32 |      -- `^*` creates a new mutable reference from a value
 33 |      r1 <- ^*1
 34 |      r2 <- ^*1
 35 |      -- `n `times` x` runs the linear computation `x` n times, like a for loop
 36 |      n `times` T1.do
 37 |        -- `&*` reads a mutable reference to get its current value
 38 |        f1 <- &*r1
 39 |        f2 <- &*r2
 40 |        -- `=*` sets the value of a mutable reference
 41 |        r2 =* (f1 + f2)
 42 |        r1 =* f2
 43 |      &*r1
 44 |