-
Notifications
You must be signed in to change notification settings - Fork 1
/
scratch.idr
129 lines (85 loc) · 2.89 KB
/
scratch.idr
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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
module Main
import Control.Monad.Identity
import Data.Vect
import lens
import system
-- Example 1:
data State1 = Work Int Int | Ready
data O1 = Input | Busy | Output Int
Interface1 : Interface
Interface1 = MkInterface O1 I
where
I : O1 -> Type
I Input = (Int, Int)
I Busy = ()
I (Output _) = ()
implementation Show O1 where
show Input = "Input"
show Busy = "Busy"
show (Output n)= "Output: " ++ show n
BusyBeaver : PureSystem State1 Interface1
BusyBeaver = MkSystem readout update
where
readout : State1 -> output Interface1
update : (s : State1) -> (input Interface1 (readout s)) -> Identity State1
readout (Work 0 n) = Output n
readout (Work m n) = Busy
readout Ready = Input
update (Work 0 n) _ = pure Ready
update (Work m n) _ = pure $ Work (m - 1) (n + 1)
update Ready (m , n) = pure $ Work m n
Add : PureSystem Int (SimpleInterface Int (Int, Int))
Add = boxUp (pure . uncurry (+))
<<<<<<< HEAD
{-
=======
{-
>>>>>>> 1d23e3b576cc2fa4ed8a28084c2914af2c9f2e15
wiring1 : Lens Identity (interfaceOf (Add <+> (OneStepDelay Int))) (ForwardInterface Int)
wiring1 = MkLens fst b
where
f : output (interfaceOf (Add <+> (OneStepDelay Int))) -> output (ForwardInterface Int)
f = fst
b : (x : output (interfaceOf (Add <+> (OneStepDelay Int))))
-> input (ForwardInterface $ output Interface1) (f x)
-> Identity $ input (interfaceOf (Add <+> (OneStepDelay Int))) x
-}
nextTest : Selection Interface1
nextTest Input = (10, 13)
nextTest Busy = ()
nextTest (Output _) = ()
testTraj : Trajectory Interface1
testTraj = runPureSystem BusyBeaver Ready
testStream : Stream (output Interface1)
testStream = toStreamTrajectory testTraj nextTest
testList : List (output Interface1)
testList = take 30 testStream
-- Lotka Voltera Predator Prey Model
record LKState where
constructor MkLK
rabbits : Int
foxes : Int
record LKParams where
constructor MkParams
rabbitBirth : Int
interaction : Int
foxDeath : Int
LKInterface : Interface
LKInterface = MkInterface LKState (const LKParams)
LK : PureSystem LKState LKInterface
LK = MkSystem id update
where
update : (s : LKState) -> input LKInterface $ s -> Identity LKState
update s p = pure $ MkLK newrabbits newfoxes
where
newrabbits = (rabbits s) + (rabbitBirth p)*(rabbits s) - (interaction p) * (rabbits s) * (foxes s)
newfoxes = (foxes s) + (interaction p) * (rabbits s) * (foxes s) - (foxDeath p) * (foxes s)
data TicTacToeSquare = TTTEmpty | TTTX | TTTO
TicTacToeBoard : Type
TicTacToeBoard = Vect 3 (Vect 3 TicTacToeSquare)
TicTacToeMoves : TicTacToeBoard -> Type
TicTacToeMoves _ = TicTacToeBoard
TicTacToeInterface : Interface
TicTacToeInterface = MkInterface TicTacToeBoard TicTacToeMoves
main : IO ()
main = printLn $ show testList