forked from HIPERFIT/contracts
-
Notifications
You must be signed in to change notification settings - Fork 1
/
TODO.txt
54 lines (30 loc) · 1.34 KB
/
TODO.txt
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
transfer(me,you) ; iter(10,transfer(you,me))
E ::= (oe,ve,te)
C[iter(n,c)] E =
if n = 0 then zero
else C[both(c,translate(1,iter(n-1,c)))] E
checkWithin(e,n,c1,c2) =
iter(n,if(acc(false,\x.x or e),c1),c2) -- WRONG!
seq(c1,c2) = both(checkWithin())
all[translate(0 ,transfer(me,you)),
translate(10,transfer(me,you)),
translate(20,transfer(me,you)),
translate(30,transfer(me,you)),
translate(40,transfer(me,you))]
waitUB(x,ub,c) = let timeFuture = now()+x
in checkWithin(timeFuture > now(),ub,c,zero)
iter(12,\x.translate(34,translate(x*30,transfer(me,you))))
iter(12,\x.translate(34,waitUB(x*30,1200,transfer(me,you))))
iter(12,\x.translate(34,let timeFuture = now()+x*30
in checkWithin(timeFuture > now(),
1200,
transfer(me,you),
zero)))
iter(12,\x.waitUB(x*30,1200,payoutInThreeDaysMF(me,you)))
payoutInThreeDaysMF(p1,p2) = if (obs("Month",0) <> obs("Month",3) checkWithin(obs("ForwardInfo7daysTodayWeekday", -7),100,transfer(me,you),zero)
-- iter with sequential composition
C[c1;c2] E := C[c1] E ++ C[c2] E
C[iter(n,c)] E :=
if n = 0 then zero
else C[c;iter(n-1,c)] E
monthly_year := iter(12, delay(30, transfer(you,me)))