
  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 |    >*T1.do
 30 |      r1 <- ^*1
 31 |      r2 <- ^*1
 32 |      n `times` T1.do
 33 |        f1 <- &*r1
 34 |        f2 <- &*r2
 35 |        r2 =* (f1 + f2)
 36 |        r1 =* f2
 37 |      &*r1
 38 |