-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathmain.ml
161 lines (135 loc) · 3.95 KB
/
main.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
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
open Bigstep;;
let run stmt state ins =
let stmt_desugared = desugar stmt in
let initial_cfg = StmtCfg (stmt_desugared, state, ins) in
let final_cfg = eval initial_cfg in
print_string "original program:\n";
print_stmt stmt;
print_string "desugared program:\n";
print_stmt stmt_desugared;
print_cfg initial_cfg;
print_string "\n ---evals to--->\n";
print_cfg final_cfg;
print_string "\n\n"
;;
(* Some shortcut functions for ASTs *)
let aexp_plus e1 e2 = PlusAExp (e1, e2);;
let bexp_not e = NotBExp (e);;
let bexp_lessthan e1 e2 = LessThanBExp (e1, e2);;
let stmt_assign x e = AssignStmt (x, e);;
let stmt_while cond block = WhileStmt (cond, block);;
let stmt_block block = BlockStmt (block);;
let block_stmt stmt = StmtBlock (stmt);;
let stmt_assign_n n = AssignStmt ("n", IntAExp (n));;
let stmt_assign_x n = AssignStmt ("x", IntAExp (n));;
let stmt_assign_y n = AssignStmt ("y", IntAExp (n));;
let stmt_assign_s n = AssignStmt ("s", IntAExp (n));;
let aexp_plus_s_n = PlusAExp (IdAExp ("s"), IdAExp ("n"));;
let aexp_minus_n_1 = PlusAExp (IdAExp ("n"), IntAExp (-1));;
let bexp_lessthan_n n = LessThanBExp (IdAExp ("n"), IntAExp (n));;
let bexp_lessthan_x n = LessThanBExp (IdAExp ("x"), IntAExp (n));;
let bexp_lessthan_y n = LessThanBExp (IdAExp ("y"), IntAExp (n));;
let bexp_lessthan_s n = LessThanBExp (IdAExp ("s"), IntAExp (n));;
let rec make_seqstmt stmts = match stmts with
| [] -> BlockStmt (EmptyBlock)
| stmt::rest_stmts -> SeqStmt (stmt, make_seqstmt rest_stmts)
;;
(* Tests programs *)
(* let_read_print *)
(* int i;
* i = read();
* print(i);
*)
let pgm_let_read_print =
make_seqstmt [
(DeclarationStmt (["i"]));
(stmt_assign "i" ReadAExp);
(PrintStmt (IdAExp ("i")))]
;;
let test_let_read_print () =
let initial_state = [] in
let stmt = pgm_let_read_print in
let ins = [42] in
print_string "test_let_read_print:\n";
run stmt initial_state ins
;;
(* sum_io *)
(* int i, s, n;
* n = read();
* while (i <= n) {
* s = s + ++i;
* }
* print(s);
*)
let pgm_sum_io =
make_seqstmt [
(DeclarationStmt (["i"; "n"; "s"]));
(stmt_assign "n" ReadAExp);
(stmt_while
(bexp_lessthan (IdAExp ("i")) (IdAExp ("n")))
(block_stmt (stmt_assign "s" (aexp_plus (IdAExp ("s")) (IncAExp ("i"))))));
(PrintStmt (IdAExp ("s")))]
;;
let test_sum_io () =
let initial_state = [] in
let stmt = pgm_sum_io in
let ins = [100] in
print_string "test_sum_io:\n";
run stmt initial_state ins
;;
(*
let test_sum_10 () =
let initial_state = [("n",0);("s",0)] in
let stmt =
make_seqstmt [
(stmt_assign_n 10);
(stmt_assign_s 0);
(stmt_while (bexp_not (bexp_lessthan_n 1))
(block_stmt
(make_seqstmt [
(stmt_assign "s" aexp_plus_s_n);
(stmt_assign "n" aexp_minus_n_1)])))] in
let ins = [] in
print_string "test_sum_10:\n";
run stmt initial_state ins
;;
let test_sum_100 () =
let initial_state = [("n",0);("s",0)] in
let stmt =
make_seqstmt [
(stmt_assign_n 100);
(stmt_assign_s 0);
(stmt_while (bexp_not (bexp_lessthan_n 1))
(block_stmt
(make_seqstmt [
(stmt_assign "s" aexp_plus_s_n);
(stmt_assign "n" aexp_minus_n_1)])))] in
let ins = [] in
print_string "test_sum_100:\n";
run stmt initial_state ins
;;
let test_sum_1000 () =
let initial_state = [("n",0);("s",0)] in
let stmt =
make_seqstmt [
(stmt_assign_n 1000);
(stmt_assign_s 0);
(stmt_while (bexp_not (bexp_lessthan_n 1))
(block_stmt
(make_seqstmt [
(stmt_assign "s" aexp_plus_s_n);
(stmt_assign "n" aexp_minus_n_1)])))] in
let ins = [] in
print_string "test_sum_1000:\n";
run stmt initial_state ins
;;
*)
let main () =
print_string "--- Welcome to Big-Step Semantics ---\n";
print_string "--- Xiaohong Chen ---\n\n";
test_sum_io ();
test_let_read_print ();
print_string "\n--- Bye bye ---\n";
;;
let () = main ()
;;