Skip to content

Commit b4acdbb

Browse files
melsmanmelsman
committed
cleanup
1 parent 655674b commit b4acdbb

9 files changed

+449
-14
lines changed

‎CONTRACT.sig

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
signature CONTRACT = sig
2+
type var
3+
4+
(* Expressions *)
5+
type 'a num
6+
type 'a exp
7+
type boolE = bool exp
8+
type intE = int num exp
9+
type realE = real num exp
10+
11+
val Var : var -> 'a exp
12+
val I : int -> intE
13+
val R : real -> realE
14+
val B : bool -> boolE
15+
val !+! : 'a num exp * 'a num exp -> 'a num exp
16+
val !-! : 'a num exp * 'a num exp -> 'a num exp
17+
val !*! : 'a num exp * 'a num exp -> 'a num exp
18+
val max : 'a num exp * 'a num exp -> 'a num exp
19+
val min : 'a num exp * 'a num exp -> 'a num exp
20+
val !<! : 'a num exp * 'a num exp -> boolE
21+
val !=! : 'a exp * 'a exp -> boolE
22+
val !|! : boolE * boolE -> boolE
23+
val not : boolE -> boolE
24+
val obs : string*int -> 'a exp
25+
26+
(* Environments *)
27+
type date = Date.date
28+
type env
29+
val emptyEnv : env
30+
val addFixing : (string * date * real) * env -> env
31+
32+
(* Evaluation *)
33+
exception Eval of string
34+
val evalR : env * date -> realE -> real
35+
val evalI : env * date -> intE -> int
36+
val evalB : env * date -> boolE -> bool
37+
38+
(* Expression utilities *)
39+
val certainExp : 'a exp -> bool
40+
val simplifyExp : env * date -> 'a exp -> 'a exp
41+
val ppExp : 'a exp -> string
42+
43+
(* Contracts *)
44+
type party = string
45+
type cur = Currency.cur
46+
type contr
47+
val transfOne : cur * party * party -> contr
48+
val scale : realE * contr -> contr
49+
val transl : intE * contr -> contr
50+
val all : contr list -> contr
51+
val iff : boolE * contr * contr -> contr
52+
val checkWithin : boolE * intE * contr * contr -> contr
53+
54+
(* Some derived forms *)
55+
val emp : contr
56+
val flow : intE * realE * cur * party * party -> contr
57+
58+
(* Contract utilities *)
59+
val ppContr : contr -> string
60+
end

‎CURRENCY.sig

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
signature CURRENCY = sig
2+
eqtype cur
3+
val EUR : cur
4+
val DKK : cur
5+
val SEK : cur
6+
val USD : cur
7+
val GBP : cur
8+
val JPY : cur
9+
val ppCur : cur -> string
10+
end

‎Contract.sml

Lines changed: 182 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,182 @@
1+
structure Contract :> CONTRACT = struct
2+
3+
type var = string
4+
datatype exp0 = I of int
5+
| R of real
6+
| B of bool
7+
| Var of var
8+
| BinOp of string * exp0 * exp0
9+
| UnOp of string * exp0
10+
| Obs of string * int
11+
12+
type 'a exp = exp0
13+
type boolE = bool exp
14+
type 'a num = unit
15+
type intE = int num exp
16+
type realE = real num exp
17+
18+
infix !+! !-! !*! !<! !=! !|!
19+
fun x !+! y = BinOp("+",x,y)
20+
fun x !-! y = BinOp("-",x,y)
21+
fun x !*! y = BinOp("*",x,y)
22+
fun x !<! y = BinOp("<",x,y)
23+
fun x !=! y = BinOp("=",x,y)
24+
fun x !|! y = BinOp("|",x,y)
25+
fun not x = UnOp("not",x)
26+
fun max (x,y) = BinOp("max",x,y)
27+
fun min (x,y) = BinOp("min",x,y)
28+
29+
val obs : (string*int) -> 'a exp = Obs
30+
31+
exception Eval of string
32+
33+
fun binopII opr i1 i2 =
34+
case opr of
35+
"+" => I (i1+i2)
36+
| "-" => I (i1-i2)
37+
| "*" => I (i1*i2)
38+
| "<" => B (i1<i2)
39+
| "=" => B (i1=i2)
40+
| "max" => I(if i1 >= i2 then i1 else i2)
41+
| "min" => I(if i1 <= i2 then i1 else i2)
42+
| _ => raise Fail ("binopII: operator not supported: " ^ opr)
43+
44+
fun binopRR opr r1 r2 =
45+
case opr of
46+
"+" => R (r1+r2)
47+
| "-" => R (r1-r2)
48+
| "*" => R (r1*r2)
49+
| "<" => B (r1<r2)
50+
| "=" => B (Real.compare(r1,r2) = EQUAL)
51+
| "max" => R(if r1 >= r2 then r1 else r2)
52+
| "min" => R(if r1 <= r2 then r1 else r2)
53+
| _ => raise Fail ("binopRR: operator not supported: " ^ opr)
54+
55+
fun binopBB opr b1 b2 =
56+
case opr of
57+
"=" => B (b1=b2)
58+
| _ => raise Fail ("binopBB: operator not supported: " ^ opr)
59+
60+
type date = Date.date
61+
62+
type env = string*date*int -> real option (* int is a date offset *)
63+
64+
val emptyEnv : env = fn _ => NONE
65+
66+
fun date_eq d1 d2 = Date.compare (d1,d2) = EQUAL
67+
68+
fun addFixing ((s,d,r),e:env) : env =
69+
fn k =>
70+
let val off = #3 k
71+
in if s = #1 k andalso off >= 0 andalso date_eq d (DateUtil.addDays off (#2 k)) then SOME r
72+
else if s = #1 k andalso off < 0 andalso date_eq (DateUtil.addDays (~off) d) (#2 k) then SOME r
73+
else e k
74+
end
75+
76+
fun eval (E:env,d:date) e =
77+
case e of
78+
Var s => raise Eval ("variable " ^ s)
79+
| I _ => e
80+
| R _ => e
81+
| B _ => e
82+
| Obs (s,off) =>
83+
(case E (s,d,off) of
84+
SOME r => R r
85+
| NONE => raise Eval "unresolved observable")
86+
| BinOp(opr,e1,e2) =>
87+
(case (eval (E,d) e1, eval (E,d) e2) of
88+
(I i1, I i2) => binopII opr i1 i2
89+
| (R r1, R r2) => binopRR opr r1 r2
90+
| (B b1, B b2) => binopBB opr b1 b2
91+
| _ => raise Fail "eval.BinOp: difference in argument types")
92+
| UnOp("not", e1) =>
93+
(case eval (E,d) e1 of
94+
B b => B(Bool.not b)
95+
| _ => raise Fail "eval.UnOp.not - wrong argument type")
96+
| UnOp(opr,_) => raise Fail ("eval.UnOp: unsupported operator: " ^ opr)
97+
98+
fun evalR E e =
99+
case eval E e of R r => r
100+
| _ => raise Fail "evalR: expecting real"
101+
fun evalI E e =
102+
case eval E e of I i => i
103+
| _ => raise Fail "evalI: expecting real"
104+
105+
fun evalB E e =
106+
case eval E e of B b => b
107+
| _ => raise Fail "evalB: expecting real"
108+
109+
fun ppExp e =
110+
let fun par s = "(" ^ s ^ ")"
111+
fun notfixed opr = opr = "max" orelse opr = "min"
112+
in case e of
113+
Var s => "Var" ^ par s
114+
| I i => Int.toString i
115+
| R r => Real.toString r
116+
| B b => Bool.toString b
117+
| Obs (s,off) => "Obs" ^ par (s ^ "@" ^ Int.toString off)
118+
| BinOp(opr,e1,e2) =>
119+
if notfixed opr then opr ^ par (ppExp e1 ^ "," ^ ppExp e2)
120+
else par(ppExp e1 ^ opr ^ ppExp e2)
121+
| UnOp(opr, e1) => opr ^ par (ppExp e1)
122+
end
123+
124+
fun certainExp e =
125+
case e of
126+
Var _ => false
127+
| I _ => true
128+
| R _ => true
129+
| B _ => true
130+
| Obs _ => false
131+
| BinOp(_,e1,e2) => certainExp e1 andalso certainExp e2
132+
| UnOp(_,e1) => certainExp e1
133+
134+
fun simplifyExp P e = (* memo: rewrite to bottom-up strategy to avoid the quadratic behavior *)
135+
eval P e
136+
handle Eval _ =>
137+
case e of
138+
UnOp(f,e1) => UnOp(f,simplifyExp P e1)
139+
| BinOp(f,e1,e2) => BinOp(f,simplifyExp P e1,simplifyExp P e2)
140+
| _ => e
141+
142+
open Currency
143+
type party = string
144+
datatype contr =
145+
TransfOne of cur * party * party
146+
| Scale of realE * contr
147+
| Transl of intE * contr
148+
| All of contr list
149+
| If of boolE * contr * contr
150+
| CheckWithin of boolE * intE * contr * contr
151+
(* if cond : boolE becomes true within time: intE then contract 1 in effect.
152+
otherwise (time expired, always false) contract 2 in effect
153+
*)
154+
155+
fun ppContr c =
156+
let fun par s = "(" ^ s ^ ")"
157+
in case c of
158+
TransfOne(c,p1,p2) => "TransfOne" ^ par (ppCur c ^ "," ^ p1 ^ "," ^ p2)
159+
| Scale (e,c) => "Scale" ^ par (ppExp e ^ "," ^ ppContr c)
160+
| Transl(e,c) => "Transl" ^ par (ppExp e ^ "," ^ ppContr c)
161+
| All[] => "emp"
162+
| All cs => "All" ^ par (ppContrs cs)
163+
| If(e,c1,c2) => "If" ^ par (ppExp e ^ ", " ^ ppContr c1 ^ ", " ^ ppContr c2)
164+
| CheckWithin (e1, e2, c1, c2) =>
165+
"CheckWithin" ^ par (ppExp e1 ^ ", " ^ ppExp e2 ^ ", " ^ ppContr c1 ^ ", " ^ ppContr c2)
166+
end
167+
and ppContrs [] = ""
168+
| ppContrs [c] = ppContr c
169+
| ppContrs (c::cs) = ppContr c ^ ", " ^ ppContrs cs
170+
171+
val transfOne = TransfOne
172+
val transl = Transl
173+
val checkWithin = CheckWithin
174+
val iff = If
175+
val all = All
176+
val scale = Scale
177+
178+
(* Shorthand notation *)
179+
fun flow(d,v,c,from,to) = scale(v,transl(d,transfOne(c,from,to)))
180+
val emp = All []
181+
182+
end

‎Currency.sml

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
structure Currency = struct
2+
datatype cur = EUR | DKK | SEK | USD | GBP | JPY
3+
fun ppCur EUR = "EUR"
4+
| ppCur DKK = "DKK"
5+
| ppCur SEK = "SEK"
6+
| ppCur USD = "USD"
7+
| ppCur GBP = "GBP"
8+
| ppCur JPY = "JPY"
9+
end

0 commit comments

Comments
 (0)