-
Notifications
You must be signed in to change notification settings - Fork 5
/
Deliverable.hs
79 lines (63 loc) · 2.05 KB
/
Deliverable.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
module Deliverable where
import Compile(runCompare)
import GCM (GCM, output, component, Port, createPort, link, value, set)
import CP (createLVar, assert, lit, (.>=), (.>), (===), (==>), inRange)
import Library (Library(Library), item, (#), TypedValue((:::)), tFloat,
tPair, tTuple3, tPort, tGCM, (.->))
library :: Library
library = Library "crud"
[ item "rain" $
rain ::: "amount" #
tFloat .-> tGCM (tPort $ "rainfall" # tFloat)
, item "pump" $
pump ::: "capacity" #
tFloat .-> tGCM (tPair (tPort $ "inflow" # tFloat)
(tPort $ "outflow" # tFloat))
, item "runoff area" $
runoffArea ::: "storage capacity" #
tFloat .-> tGCM (tTuple3 (tPort $ "inflow" # tFloat)
(tPort $ "outlet" # tFloat)
(tPort $ "overflow" # tFloat))
]
rain :: Float -> GCM (Port Float)
rain amount = do
port <- createPort
set port amount
return port
pump :: Float -> GCM (Port Float, Port Float)
pump maxCap = do
inPort <- createPort
outPort <- createPort
component $ do
inflow <- value inPort
outflow <- value outPort
assert $ inflow === outflow
assert $ inflow `inRange` (0, lit maxCap)
return (inPort, outPort)
runoffArea :: Float -> GCM (Port Float, Port Float, Port Float)
runoffArea cap = do
inflow <- createPort
outlet <- createPort
overflow <- createPort
component $ do
currentStored <- createLVar
inf <- value inflow
out <- value outlet
ovf <- value overflow
sto <- value currentStored
assert $ sto === inf - out - ovf
assert $ sto `inRange` (0, lit cap)
assert $ (ovf .> 0) ==> (sto === lit cap)
assert $ ovf .>= 0
return (inflow, outlet, overflow)
example :: GCM ()
example = do
(inflowP, outflowP) <- pump 5
(inflowS, outletS, overflowS) <- runoffArea 5
rainflow <- rain 10
link inflowP outletS
link inflowS rainflow
output overflowS "Overflow"
main :: IO ()
main = do
runCompare example