-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathnormalization.ml
99 lines (75 loc) · 3.79 KB
/
normalization.ml
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
open Ast
let nameSupply = ref 1
let freshName _ = nameSupply := !nameSupply + 1;
String.concat "" ["temp" ; string_of_int (!nameSupply )]
let rec normalizeExp e = match e with
| And (e1, e2) -> let r1 = normalizeExp e1 in
let r2 = normalizeExp e2 in
(Seq (fst r1, fst r2),
And (snd r1, snd r2))
| Gt (e1, e2) -> let r1 = normalizeExp e1 in
let r2 = normalizeExp e2 in
(Seq (fst r1, fst r2),
Gt (snd r1, snd r2))
| Plus (e1, e2) -> let r1 = normalizeExp e1 in
let r2 = normalizeExp e2 in
(Seq (fst r1, fst r2),
Plus (snd r1, snd r2))
| Minus (e1, e2) -> let r1 = normalizeExp e1 in
let r2 = normalizeExp e2 in
(Seq (fst r1, fst r2),
Minus (snd r1, snd r2))
| Times (e1, e2) -> let r1 = normalizeExp e1 in
let r2 = normalizeExp e2 in
(Seq (fst r1, fst r2),
Times (snd r1, snd r2))
| Division (e1, e2) -> let r1 = normalizeExp e1 in
let r2 = normalizeExp e2 in
(Seq (fst r1, fst r2),
Division (snd r1, snd r2))
| Not e1 -> let r1 = normalizeExp e1 in
(fst r1,
Not (snd r1))
| RcvExp ch -> let x = freshName() in
(Decl (x, RcvExp ch),
Var x)
(* Introduce Skip for convenience, maybe should have
represented a sequence of commands as a list ... *)
| IConst i -> (Skip, IConst i)
| BConst b -> (Skip, BConst b)
| Var x -> (Skip, Var x)
(* Need to normalize function arguments and make sure that order remains right *)
| FuncExp (x,es) -> let rs = List.map normalizeExp es in
let c = List.fold_left (fun a -> fun b -> Seq (a,b)) Skip (List.map fst rs) in
let xs = List.map snd rs in
let y = freshName() in
(Seq (c, Decl (y, FuncExp (x,xs))),
Var y)
let rec normalizeStmt s = match s with
| Seq (s1,s2) -> Seq (normalizeStmt s1, normalizeStmt s2)
| Go s -> Go (normalizeStmt s)
| Transmit (x,e) -> let r = normalizeExp e in
Seq (fst r, Transmit (x, snd r))
| RcvStmt x -> RcvStmt x
| Decl (x,e) -> let r = normalizeExp e in
Seq (fst r, Decl (x, snd r))
| DeclChan x -> DeclChan x
| Assign (x,e) -> let r = normalizeExp e in
Seq (fst r, Assign (x, snd r))
| While (e,s) -> let r = normalizeExp e in
Seq (fst r, While (snd r, normalizeStmt s))
| ITE (e,s1,s2) -> let r = normalizeExp e in
Seq (fst r, ITE (snd r, normalizeStmt s1, normalizeStmt s2))
| Return e -> let r = normalizeExp e in
Seq (fst r, Return (snd r))
| FuncCall (x, es) -> let rs = List.map normalizeExp es in
let c = List.fold_left (fun a -> fun b -> Seq (a,b)) Skip (List.map fst rs) in
let xs = List.map snd rs in
Seq (c, FuncCall (x,xs))
| Print e -> let r = normalizeExp e in
Seq (fst r, Print (snd r))
| Skip -> Skip
let normalizeProc p = match p with
Proc (x, args, tys, s) -> Proc (x, args, tys, normalizeStmt s)
let normalizeProg p = match p with
Prog (ps, s) -> Prog (List.map normalizeProc ps, normalizeStmt s)