-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathREADME.txt
201 lines (156 loc) · 6.43 KB
/
README.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
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
# MINI-ML #
university project which goal is to encode by ourself a Caml-like langage called 'Mini-ML' .
Link to Thibault Balabonski's enunciate for this project :
https://www.lri.fr/~blsk/CompilationLDD3/dm-mml.html
##### Description of MiniML #####
A mini-ml program is composed of type definitions serie followed by a single expression to interpret .
example (test/syracuse.mml) :
```
type intref = { mutable value: int; }
type sequence = { start: int; next: int -> int; stop: int -> bool; }
(* maximal value of a numeric sequence *)
let max_value (s:sequence) =
let max = { value = s.start; } in
let rec iter (n:int): unit =
if max.value < n then max.value <- n;
if not (s.stop n) then iter (s.next n)
in
iter s.start;
max.value
in
(* collatz conjecture: for any n, this sequence eventually reaches 1 *)
let syracuse n = {
start = n;
next = (fun (k:int) -> if k mod 2 == 0 then k/2 else 3*k+1);
stop = (fun (k:int) -> k <= 1);
}
in
max_value (syracuse 27)
```
##### MiniML Syntax #####
prog := [ type_def ]* expr eof
type_def := type ident = { [[mutable]? ident : type ;]+ }
type := int
| bool
| unit
| ident
| type -> type
| ( type )
expr := s_expr
| uop s_expr
| expr bop expr
| expr s_expr
| if expr then expr
| if expr then expr else expr
| fun ident -> expr
| let ident [( ident : type )]* = expr in expr
| let rec ident [( ident : type )]* : type = expr in expr
| s_expr . ident <- expr
| expr ; expr
s_expr := n
| true
| false
| ()
| ident
| s_expr . ident
| { [ident = expr ;]+ }
| ( expr )
uop := -
| not
bop := +
| -
| *
| /
| mod
| ==
| !=
| <
| <=
| &&
| ||
*
##### Type Checking rules #####
Constants typing rules :
___________ _______________ _________________
E |- n: int E |- true: bool E |- false: bool
Unary Operand :
E |- e: int E |- e: bool
----------- ------------
E |- e: int E|- not e: bool
Binary Operand :
E |- e1: int E |- e2: int E |- e1: int E |- e2: int
(1) --------------------------- (2) ---------------------------
E |- e1 op1 e2 : int E |- e1 op2 e2 : bool
E |- e1: t E |- e2: t
(3) -------------------------
E |- e1 op3 e2 : bool
with op1 := + | - | * | / | mod
op2 := < | <= | && | ||
op3 := == | !=
Variables :
E(x) = t E |- e1 : t1 E, x:t1 |- e2 : t2
---------- -----------------------------------
E |- x : t E |- let x = e1 in e2 : t2
Conditionnal expression :
E |- e0 : bool E |- e1 : t E |- e2 : t
----------------------------------------------
E |- if e0 then e1 else e2 : t
Functions and all fun-like stuff :
E, x:t1 |- e : t2 E |- e1 : t2 -> t1 E |- e2 : t2
------------------------------- -----------------------------------
E |- fun (x:t1) -> e : t1 -> t2 E |- e1 e2 : t1
E, x:t1 |- e : t2
-----------------------
E |- Fix(x, t1, e) : t2
Sequencies Operand :
E |- e1 : t1 E |- e2 : t2
-----------------------------
E |- e1 ; e2 : t2
Structures :
E |- e : s s.x : t E |- e1 : s s.x : t mutable E |- e2 : t
---------------------- -----------------------------------------------
E |- e.x : t E |- e1.x <- e2 : unit
s.x1 : t1 E |- e1 : t1 ... s.xN : tN E |- eN : tN
-----------------------------------------------------------------
E |- { x1 = e1; ...; xN = eN; } : s
##### Progression #####
I consider going through this project with the 2nd working-method given by T.Balabonski :
Implementing + Testing each line before going to the next one.
X : Done (quite sure)
~ : Not completed
* : Done but not sure / build error
| Lexer | Parser | TypeChecker | Interpreter |
Arithmetic | X | X | X | X |
Variables | X | X | X | X |
Functions | X | X | X | X |
Structures | X | X | X | X |
Fix Point | X | X | X | X |
Extensions I added :
Matching Pattern
Correct Errors
Uniform Arrays (only declaration...) with Len, Eq & Concat Operand
##### in-sighted Extensions #####
Int Arrays : (first overall idea)
as an expr ? ==> mml.ml - ArrayInt of string * (int/expr) list
recognized as ? ==> mmlparser.mly - let array l = [int,int,int, ... ,];
LET ARRAY id=IDENT ASS LBRACKET elems=list_elm RBRACKET SEMI { ArrayInt(id,elems) }
list_elm: | n=CST COMMA { Int(n) } (*how to make the last elem without comma ?*)
typechecked as ? ==> typechecker.ml - must check for each element in 'elems' if it's well typed TInt
then return the type TArrayInt (without any arhument !)
interpreted as ? ==> interpreter.ml - return a list of VInt ? (might use (VInt) list)
a VArrayInt could be nice...
printed as ? ==> rly don't wanna do this...
ANOTHER COMPLETION :: maybe could add something to get a special element ? like GetI, how to do ???
Matching pattern :(not any idea of how to do)
as an expr for sure ==> mml.ml - MatchPattern of expr * (expr) list * (expr) list * expr ???
recognized as ? ==> mmlparser.mly - match 'expr' with
| 'expr_bis' -> 'expr_bis_consequence'
...
| 'expr_n-1' -> 'expr_n-1_consequence'
| '_' -> 'expr_n_consequence'
typechecked as ? ==> typechecker.ml - must check if 'expr' is of same type as all 'expr_bis' -> 'expr_n' ?
'_' expr is needed to be associated to 'expr_n' !
then must check if all 'expr_i_consequence' is well typed ...
intepreted as ? ==> intepreter.ml - if 'expr' == 'expr_i" then 'expr_i_consequence' else 'expr_n_consequence' ?
Correct Errors implementation (shall not be very hard but seems important to do...) -> Tried to do it properly in the TypeChecker
Uniform Arrays ???