-
Notifications
You must be signed in to change notification settings - Fork 3
/
krivine.ml
175 lines (133 loc) · 7.67 KB
/
krivine.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
162
163
164
165
166
167
168
169
170
171
172
173
(* expressions for the language *)
type exp = Nil | Int of int | Bool of bool | Var of string | Abs of string * exp | App of exp * exp | Absolute of exp| Not of exp
| Add of exp*exp| Sub of exp*exp| Div of exp*exp| Mul of exp*exp| Mod of exp*exp| Exp of exp*exp
| And of exp*exp| Or of exp*exp| Imp of exp*exp
| Equ of exp*exp| GTEqu of exp*exp| LTEqu of exp*exp| Grt of exp*exp| Lst of exp*exp
| Ifthenelse of (exp*exp*exp);;
(* opcode list generated by compiler, if used *)
type opcode = NIL | INT of int | BOOL of bool | LOOKUP of string | CLOS of string*(opcode list) | CALL | RET | ADD;;
(* inter-dependent types *)
type table = (string * answer) list
and answer = I of int | B of bool | Vclos of table*string*control
and stack = answer list
and environment = table
and control = opcode list
and dump = stack*environment*control
and program = exp list
and stackCLOS = closure list
and closure = CLtype of exp*environmentCLOS
and environmentCLOS = (exp*closure) list;;
(* Exceptions *)
exception Variable_not_intialized;;
exception InvalidOperation;;
exception OperationNotSupported;;
exception InvalidBigStepAnswerClosure;;
exception ReturnEmpty;;
(* functions used in inter-computation *)
let rec lookup (e, env) = match (e, env) with
| (e, (e1,cl)::c') -> if e1<>e then lookup (e, c') else
(match cl with
| CLtype (Abs (x,x1), env) -> CLtype (Abs (x, x1), (e1,cl)::env)
| _ -> cl)
| (e, []) -> raise Variable_not_intialized;;
let rec power a b = match (a,b) with
(a,0) -> 1 |
(a,b) -> a*(power a (b-1));;
let imp a b = match(a,b) with (true,false) -> false | _-> true;;
(* val absApplied : closure * closure list -> closure * closure list = <fun> *)
let absApplied (cl, s) = match (cl, s) with
| (CLtype(Abs(x ,e), env), c::c') -> (CLtype(e, (Var x, c)::env), c')
| (_,[]) -> raise InvalidOperation
| _ -> raise InvalidOperation;;
(* functions defined as : closure * closure -> closure = <fun> *)
let add (a1, a2) = match (a1,a2) with
(CLtype(Int i1, env1), CLtype(Int i2, env2)) -> CLtype(Int (i1+i2), [])
| _-> raise InvalidOperation;;
let mul (a1, a2) = match (a1,a2) with
(CLtype(Int i1, env1), CLtype(Int i2, env2)) -> CLtype(Int (i1*i2), [])
| _-> raise InvalidOperation;;
let sub (a1, a2) = match (a1,a2) with
(CLtype(Int i1, env1), CLtype(Int i2, env2)) -> CLtype(Int (i1-i2), [])
| _-> raise InvalidOperation;;
let div (a1, a2) = match (a1,a2) with
(CLtype(Int i1, env1), CLtype(Int i2, env2)) -> CLtype(Int (i1/i2), [])
| _-> raise InvalidOperation;;
let exponential (a1, a2) = match (a1,a2) with
(CLtype(Int i1, env1), CLtype(Int i2, env2)) -> CLtype(Int (power i1 i2), [])
| _-> raise InvalidOperation;;
let modulus (a1, a2) = match (a1,a2) with
(CLtype(Int i1, env1), CLtype(Int i2, env2)) -> CLtype(Int (i1 mod i2), [])
| _-> raise InvalidOperation;;
let absolute (a1) = match (a1) with
(CLtype(Int i1, env1)) -> CLtype(Int (if i1>0 then i1 else ((-1)*i1)), [])
| _-> raise InvalidOperation;;
let andop (a1, a2) = match (a1,a2) with
(CLtype(Bool i1, env1), CLtype(Bool i2, env2)) -> CLtype(Bool (i1 && i2), [])
| _-> raise InvalidOperation;;
let orop (a1, a2) = match (a1,a2) with
(CLtype(Bool i1, env1), CLtype(Bool i2, env2)) -> CLtype(Bool (i1 || i2), [])
| _-> raise InvalidOperation;;
let imp (a1, a2) = match (a1,a2) with
(CLtype(Bool i1, env1), CLtype(Bool i2, env2)) -> CLtype(Bool (imp i1 i2), [])
| _-> raise InvalidOperation;;
let notop (a1) = match (a1) with
(CLtype(Bool i1, env1)) -> CLtype(Bool (not i1), [])
| _-> raise InvalidOperation;;
let equal (a1, a2) = match (a1,a2) with
(CLtype(Int i1, env1), CLtype(Int i2, env2)) -> CLtype(Bool (if i1==i2 then true else false), [])
| _-> raise InvalidOperation;;
let greaterthanorequal (a1, a2) = match (a1,a2) with
(CLtype(Int i1, env1), CLtype(Int i2, env2)) -> CLtype(Bool (if i1>=i2 then true else false), [])
| _-> raise InvalidOperation;;
let lessthanorequal (a1, a2) = match (a1,a2) with
(CLtype(Int i1, env1), CLtype(Int i2, env2)) -> CLtype(Bool (if i1<=i2 then true else false), [])
| _-> raise InvalidOperation;;
let greaterthan (a1, a2) = match (a1,a2) with
(CLtype(Int i1, env1), CLtype(Int i2, env2)) -> CLtype(Bool (if i1>i2 then true else false), [])
| _-> raise InvalidOperation;;
let lessthan (a1, a2) = match (a1,a2) with
(CLtype(Int i1, env1), CLtype(Int i2, env2)) -> CLtype(Bool (if i1<i2 then true else false), [])
| _-> raise InvalidOperation;;
(* Krivine machine evaluation with expression *)
let rec krivinemachine cl (s:stackCLOS) = match cl with
| CLtype (Nil, env) -> CLtype (Nil, env)
| CLtype (Int i, env) -> CLtype (Int i, env)
| CLtype (Bool b, env) -> CLtype (Bool b, env)
| CLtype (Var v, env) -> krivinemachine (lookup (Var(v), env)) s
| CLtype (Abs(x, e), env) ->
let (cl', s') = absApplied (cl, s) in
krivinemachine cl' s'
| CLtype (App(e1, e2), env) -> krivinemachine (CLtype(e1, env)) (CLtype(e2, env)::s)
| CLtype (Add(e1, e2), env) -> (krivinemachine (add ((krivinemachine (CLtype(e1, env)) []), (krivinemachine (CLtype(e2, env)) []))) s)
| CLtype (Sub(e1, e2), env) -> (krivinemachine (sub ((krivinemachine (CLtype(e1, env)) []), (krivinemachine (CLtype(e2, env)) []))) s)
| CLtype (Mul(e1, e2), env) -> (krivinemachine (mul ((krivinemachine (CLtype(e1, env)) []), (krivinemachine (CLtype(e2, env)) []))) s)
| CLtype (Div(e1, e2), env) -> (krivinemachine (div ((krivinemachine (CLtype(e1, env)) []), (krivinemachine (CLtype(e2, env)) []))) s)
| CLtype (Exp(e1, e2), env) -> (krivinemachine (exponential ((krivinemachine (CLtype(e1, env)) []), (krivinemachine (CLtype(e2, env)) []))) s)
| CLtype (Mod(e1, e2), env) -> (krivinemachine (modulus ((krivinemachine (CLtype(e1, env)) []), (krivinemachine (CLtype(e2, env)) []))) s)
| CLtype (Absolute(e1), env) -> (krivinemachine (absolute ((krivinemachine (CLtype(e1, env)) []))) s)
| CLtype (And(e1, e2), env) -> (krivinemachine (andop ((krivinemachine (CLtype(e1, env)) []), (krivinemachine (CLtype(e2, env)) []))) s)
| CLtype (Or(e1, e2), env) -> (krivinemachine (orop ((krivinemachine (CLtype(e1, env)) []), (krivinemachine (CLtype(e2, env)) []))) s)
| CLtype (Imp(e1, e2), env) -> (krivinemachine (imp ((krivinemachine (CLtype(e1, env)) []), (krivinemachine (CLtype(e2, env)) []))) s)
| CLtype (Not(e1), env) -> (krivinemachine (notop ( (krivinemachine (CLtype(e1, env)) []))) s)
| CLtype (Equ(e1, e2), env) -> (krivinemachine (equal ((krivinemachine (CLtype(e1, env)) []), (krivinemachine (CLtype(e2, env)) []))) s)
| CLtype (GTEqu(e1, e2), env) -> (krivinemachine (greaterthanorequal ((krivinemachine (CLtype(e1, env)) []), (krivinemachine (CLtype(e2, env)) []))) s)
| CLtype (LTEqu(e1, e2), env) -> (krivinemachine (lessthanorequal ((krivinemachine (CLtype(e1, env)) []), (krivinemachine (CLtype(e2, env)) []))) s)
| CLtype (Grt(e1, e2), env) -> (krivinemachine (greaterthan ((krivinemachine (CLtype(e1, env)) []), (krivinemachine (CLtype(e2, env)) []))) s)
| CLtype (Lst(e1, e2), env) -> (krivinemachine (lessthan ((krivinemachine (CLtype(e1, env)) []), (krivinemachine (CLtype(e2, env)) []))) s)
| CLtype (Ifthenelse(e0, e1, e2), env) ->
let a0 = (krivinemachine (CLtype(e0, env)) []) in
(match a0 with
| CLtype(Bool b, env) -> (if b then (krivinemachine (CLtype(e1, env)) s) else (krivinemachine (CLtype(e1, env)) s))
| _ -> raise InvalidOperation)
;;
(* Execution of krivine function *)
let rec executekrivine (prog: program) (env: environmentCLOS): answer = match prog with
| p::prog' ->
let cl = krivinemachine (CLtype(p, env)) [] in
(match cl with
| CLtype (Nil, env') -> executekrivine prog' env'
| CLtype (Int i, _) -> I i
| CLtype (Bool b, _) -> B b
| _-> raise InvalidBigStepAnswerClosure
)
| _-> raise ReturnEmpty;;