1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
{-# OPTIONS --guardedness --rewriting #-}
module Main where
open import Data.Bool.Base using (Bool; true; false)
open import Data.Nat.Base using (ℕ; zero; suc; _+_)
open import Data.Nat.Show using (show)
open import Data.Product.Base using (_,_)
open import Data.String.Base using (String; _++_)
open import Data.Default
open import Debug.Trace using (trace)
open import IO.Base using (Main; run)
open import IO.Finite using (putStrLn)
open import Function.Base using (_$_)
open import Effect.Monad
open import Effect.Monad.State
open import Effect.Monad.State.Instances
open import Effect.Monad.Identity.Instances
open import IO.Instances
open RawMonad {{...}}
open RawMonadState {{...}}
record Fib : Set where
field tracing : Bool
index : ℕ
current : ℕ
next : ℕ
open Fib
initFib : Bool → Fib
initFib b = record
{ tracing = b
; index = 0
; current = 0
; next = 1
}
displayFib : ℕ → ℕ → String
displayFib idx fibn = "fib " ++ show idx ++ " = " ++ show fibn
fibM : ℕ → State Fib ℕ
fibM 0 = gets current
fibM (suc n) = do
b ← gets tracing
when b $ do
idx ← gets index
fibn ← gets current
trace (displayFib idx fibn) (pure _)
modify (λ r → record r { index = suc (index r) ; current = next r ; next = next r + current r })
fibM n
fib : ℕ → Bool → ℕ
fib n b = evalState (fibM n) (initFib b)
fibStr : ℕ → {{WithDefault false}} → String
fibStr n {{b}} = displayFib n (fib n (value b))
main : Main
main = run $ do
putStrLn $ fibStr 0
putStrLn $ fibStr 1
putStrLn $ fibStr 2
putStrLn $ fibStr 3
putStrLn $ fibStr 5
putStrLn $ fibStr 6
putStrLn $ fibStr 7
putStrLn $ fibStr 8
putStrLn $ fibStr 9
putStrLn $ fibStr 10
|
