-
Notifications
You must be signed in to change notification settings - Fork 0
/
Test.hs
117 lines (97 loc) · 2.47 KB
/
Test.hs
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
{-# OPTIONS_GHC -fplugin BinderAnn.Pure #-}
module Main (main) where
import GCM
import CP
import Compile
import BinderAnn.Pure
main :: IO ()
main = do
res <- run True True simpleExample
putStr res
-- A source of flow a
source :: (CPType a) => a -> GCM (Port a)
source a = do
p <- createPort
set p a
return p
-- A sink of capacity a
sink :: (CPType a, Ord a, Num a) => a -> GCM (Port a)
sink a = do
p <- createPort
component $ do
inflow <- value p
assert $ inflow `inRange` (0, lit a)
return p
rain :: (Num a, CPType a) => a -> GCM (Port a)
-- Rain is a source of Floats
rain = source
-- A pipe with a fixed capacity
pipe :: (Num a, Ord a, CPType a) => a -> GCM (Port a)
pipe k = do
flow <- createPort
component $ do
f <- value flow
assert $ f `inRange` (0, lit k)
return flow
-- Storage as a GCM component
storage :: (Num a, Ord a, CPType a) => a -> GCM (Port a, Port a)
storage k = do
ip <- createPort
op <- createPort
linkBy (fun (\inflow -> max' 0 (inflow - lit k))) ip op
return (ip, op)
-- Fill inputs in order
fill :: (Num a, Ord a, CPType a) => Port a -> [(Maybe (Port a), Port a)] -> GCM ()
fill p [] = return ()
fill p ((Just cap, x):xs) = do
residual <- createPort
component $ do
res <- value residual
pv <- value p
xv <- value x
c <- value cap
assert $ xv === max' 0 (min' c pv)
assert $ res === pv - xv
fill residual xs
fill p ((Nothing, x):xs) = do
link p x
mapM_ (\p -> set (snd p) 0) xs
-- A pump has a maximum capacity and a flow
pump :: (Num a, Ord a, CPType a) => a -> GCM (Port a, Port a)
pump cmax = do
fp <- createPort
cp <- createPort
component $ do
f <- value fp
c <- value cp
assert $ c `inRange` (0, lit cmax)
assert $ f `inRange` (0, c)
return (fp, cp)
minimize gp op = component $ do
v <- value op
g <- value gp
assert (g === 0 - v)
-- Simple example with outputs and everything
simpleExample :: GCM ()
simpleExample = do
-- The rain
rain <- source 10
-- Storage
(inflow, overflow) <- storage 3
-- The pump
(flow, capacity) <- pump 6
-- Rain first goes in to the pump, and then the store
fill rain [(Just capacity, flow), (Nothing, inflow)]
-- Minimise overflow goal
goal <- createIntGoal
goal `minimize` overflow
-- Outputs
output' capacity
output' flow
output' overflow
output' inflow
-- with redundant strings
-- output capacity "capacity"
-- output flow "flow"
-- output overflow "overflow"
-- output inflow "inflow"