forked from melsman/contracts
-
Notifications
You must be signed in to change notification settings - Fork 1
/
ContractTransform.sml
203 lines (193 loc) · 9.57 KB
/
ContractTransform.sml
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
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
structure ContractTransform = struct
local open Currency Contract ContractBase in
infix !+! !*! !-!
(* Contract normalisation:
o gather Transl outside of If, CheckWithin. Both and Scale inside
o multiply Scale, add Transl, cutting them when empty below
TODO: use (temporary) tag to avoid repeated traversals!!!
*)
fun normalise (Transl (i,c)) = (case normalise c of
(* aggregate several Transl *) Transl (i',c') => transl (i + i', c')
| Zero => Zero
| other => transl (i,other))
| normalise (If (b,c1,c2)) =
(case (normalise c1,normalise c2) of
(Zero,Zero) => Zero
(* lift Transl constr.s to top *)
| (Transl (i1,c1'),Transl (i2,c2'))
=> if i1 =i2 then transl(i1, normalise (iff (b, c1', c2')))
else let val iMin = Int.min (i1, i2)
val i1' = i1 - iMin
val i2' = i2 - iMin
in transl(iMin, iff (translExp (b, ~iMin),
transl(i1', c1'),
transl(i2', c2')))
end
| (Transl (i1,c1'),Zero) => transl (i1, normalise (iff (b, c1', zero)))
| (Zero,Transl (i2,c2')) => transl (i2, normalise (iff (b, zero, c2')))
| (c1' as If(b',c11,_),c2') =>
if eqExp (b, b') then normalise (iff (b, c11, c2'))
else iff (b, c1', c2')
| (c1',c2' as If(b',_,c22)) =>
if eqExp (b, b') then normalise (iff (b, c1', c22))
else iff (b, c1', c2')
| (c1' as CheckWithin(b',_,c11,_),c2') =>
if eqExp (b, b') then normalise (iff (b, c11, c2'))
else iff (b, c1', c2')
| (c1',c2') => iff (b, c1', c2'))
| normalise (CheckWithin (b, i, c1, c2)) =
(case (normalise c1, normalise c2) of
(Zero,Zero) => Zero
(* lift Transl constr.s to top *)
| (Transl (i1,c1'),Transl (i2,c2'))
=> if i1 = i2 then transl(i1, checkWithin (translExp (b, ~i1), i, c1', c2'))
else let val iMin = Int.min (i1, i2)
val i1' = i1 - iMin
val i2' = i2 - iMin
val b' = translExp (b, ~iMin)
in transl(iMin, checkWithin (b', i, transl(i1',c1'),
transl(i2', c2')))
end
| (Transl (i1,c1'),Zero) => transl (i1, checkWithin (translExp (b, ~i1), i, c1', zero))
| (Zero,Transl (i2,c2')) => transl (i2, checkWithin (translExp (b, ~i2), i, zero, c2'))
| (c1' as If(b',c11,_),c2') =>
if eqExp (b, b') then normalise (checkWithin (b, i, c11, c2'))
else checkWithin (b, i, c1', c2')
| (c1',c2' as If(b',_,c22)) =>
if eqExp (b, b') then normalise (checkWithin (b, i, c1', c22))
else checkWithin (b, i, c1', c2')
| (c1' as CheckWithin(b',_,c11,_),c2') =>
if eqExp (b, b') then normalise (checkWithin (b, i, c11, c2'))
else checkWithin (b, i, c1', c2')
| (c1', c2') => checkWithin (b, i, c1', c2'))
| normalise (Both (c1,c2)) =
(case (normalise c1, normalise c2) of
(Zero,Zero) => Zero
| (Zero,c) => c
| (c,Zero) => c
(* lift Transl constr.s to top *)
| (Transl (i1,c1'),Transl (i2,c2'))
=> if i1 = i2 then transl(i1, both (c1', c2'))
else let val iMin = Int.min (i1, i2)
val i1' = i1 - iMin
val i2' = i2 - iMin
in transl(iMin, both (transl(i1',c1'), transl(i2', c2')))
end
| (If(b1,c11,c12),If(b2,c21,c22))
(* memo: maybe better to lift "Both" up, right below "Transl"?*)
=> if eqExp (b1,b2) then iff (b1, both (c11,c21), both (c12,c22))
else both ( iff (b1,c11,c12), iff (b2, c21, c22))
(* create right-bias (as constructor does) *)
| (Both(c11,c12),c2) => normalise (both (c11,both (c12,c2)))
| (c1', c2') => if eqContr (c1', c2')
then normalise (scale (R 2.0,c1'))
else both (c1', c2'))
| normalise (Scale (e, c)) =
(case normalise c of
Zero => Zero
| Scale (e',c') => scale (e !*! e', c') (* aggregate scales *)
| Transl (i,c') =>
transl (i, normalise (scale (e,c'))) (* transl to top *)
| If (e,c1,c2) => (* iff outside scale *)
iff (e, normalise (scale (e,c1)), normalise (scale (e,c2)))
| CheckWithin (e,i,c1,c2) =>
checkWithin (e, i,
normalise (scale (e,c1)), normalise (scale (e,c2)))
| Both (c1,c2) =>
(* repeated normalisation to merge chains of "scale" *)
both (normalise (scale (e,c1)), normalise (scale (e,c2)))
| other => scale (e, other))
(* leave let where they are (for now, could float them out) *)
| normalise (Let (v,e,c1)) = (case normalise c1 of
Zero => Zero
| c1' => Let (v,e, normalise c1'))
(* zero and flows stay *)
| normalise a = a
(* unrolling all CheckWithin constructors into a corresponding iff chain *)
fun unrollCWs (If(e,c1,c2)) = iff (e, unrollCWs c1, unrollCWs c2)
| unrollCWs (Both (c1,c2)) = both (unrollCWs c1, unrollCWs c2)
| unrollCWs Zero = zero
| unrollCWs (Transl (i,c)) = transl (i, unrollCWs c)
| unrollCWs (Scale (e,c)) = scale (e,unrollCWs c)
| unrollCWs (TransfOne (c,p1,p2)) = TransfOne (c,p1,p2)
| unrollCWs (CheckWithin (e,t,c1,c2)) =
let fun check i = iff (translExp (e,i), transl (i,c1),
if i = t then transl (t,c2) else check (i+1))
in check 0
end
| unrollCWs (Let (v,e,c1)) = Let (v,e,unrollCWs c1)
(* routine assumes a is normalised contract and applies no own
optimisations except removing empty branches *)
fun removeParty_ (p : string) ( a : contr) =
let fun remv c =
case c of
TransfOne (_,p1,p2) => if p = p1 orelse p = p2
then zero else c
| Scale (s,c') => (case remv c' of
Zero => zero
| other => Scale (s,other))
| Transl (d,c') => (case remv c' of
Zero => zero
| other => Transl (d, other))
| Both(c1,c2) => Both (remv c1, remv c2)
| Zero => Zero
| If (b,c1,c2) => (case (remv c1, remv c2) of
(Zero,Zero) => zero
| (c1', c2') => If (b,c1',c2'))
| CheckWithin (b,i,c1,c2) =>
(case (remv c1, remv c2) of
(Zero,Zero) => zero
| (c1', c2') => CheckWithin (b,i,c1',c2'))
| Let (v,e,c1) => case remv c1 of
Zero => Zero
| c1' => Let (v,e,c1')
in normalise (remv a)
end
(* this routine should work with any contract *)
fun removeParty p a = removeParty_ p (normalise a)
(* replaces p1 by p2 in all contracts inside a. Assumes normalised a.
Could try to aggregate flows between same parties afterwards *)
fun mergeParties_ (p1 : party) (p2 : party) (a : contr) =
let fun merge c =
case c of
Zero => zero
| TransfOne (cur,pA,pB) =>
if pA = p1 then
if pB = p1 orelse pB = p2 then zero
else TransfOne (cur,p2,pB)
else
if pB = p1 then
if pA = p2 then zero
else TransfOne (cur,p2,pB)
else c
| Scale (s,c') => (case merge c' of
Zero => zero
| other => Scale (s,other))
| Transl (i,c') => (case merge c' of
Zero => zero
| other => Transl (i,other))
| Both(c1,c2) => Both (merge c1,merge c2)
(* merging parties can render conditional branches
equivalent (i.e. same normalised contract) *)
| If (b,c1,c2) => (case (normalise (merge c1),
normalise (merge c2)) of
(Zero, Zero) => zero
| (c1', c2') =>
if eqContr (c1',c2') then c1'
else If (b,c1',c2'))
| CheckWithin (b,i,c1,c2) =>
(case (normalise (merge c1),
normalise (merge c2)) of
(Zero, Zero) => zero
| (c1', c2') =>
if eqContr (c1',c2') then c1'
else CheckWithin (b,i,c1',c2'))
| Let (v,e,c1) => case merge c1 of
Zero => Zero
| c1' => Let (v,e,c1')
in normalise (merge a)
end
(* replaces p1 by p2 in all contracts inside a*)
fun mergeParties p1 p2 a = mergeParties p1 p2 (normalise a)
end
end