Skip to content

Commit a209c42

Browse files
Aplace0927Aplace0927
committed
feat(hw6): debug step2
1 parent f3eff89 commit a209c42

File tree

5 files changed

+1996
-74
lines changed

5 files changed

+1996
-74
lines changed

‎HW/HW6/eval.ml

+98-74
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ let value2exp (v: value): exp =
4747
| VTrue -> True
4848
| VFalse -> False
4949
| VEunit -> Eunit
50-
| VNum (i) -> Num (i)
50+
| VNum(i) -> Num(i)
5151
| _ -> raise NotConvertible
5252

5353
(* Problem 1.
@@ -65,24 +65,26 @@ module ControlFlow =
6565
struct
6666
let return (st: state) (vl: value): state =
6767
match st with
68-
| Return_ST(_, _, _) -> raise Stuck
6968
| Anal_ST(heap, stck, expr, envr) -> Return_ST(heap, stck, vl)
70-
let call (st: state) (fr: frame) (ex: exp): state =
69+
| Return_ST(heap, Frame_SK(oldstck, newfrm), valu) -> Return_ST(heap, oldstck, vl)
70+
| _ -> raise Stuck
71+
let call (st: state) (fr: frame) (ex: exp) (nv: env): state =
7172
match st with
72-
| Return_ST(_, _, _) -> raise Stuck
7373
| Anal_ST(heap, stck, expr, envr) -> Anal_ST(heap, Frame_SK(stck, fr), ex, envr)
74-
let jump (st: state) (fr: frame) (ex: exp) (nv: env): state =
75-
match st with
76-
| Return_ST(_, _, _) -> raise Stuck
77-
| Anal_ST(heap, stck, expr, envr) -> Anal_ST(heap, Frame_SK(stck, fr), ex, nv)
74+
| Return_ST(heap, Frame_SK(oldstck, newfrm), valu) -> Anal_ST(heap, Frame_SK(oldstck, fr), ex, nv)
75+
| _ -> raise Stuck
7876
let branch (st: state) (ex: exp) (nv: env): state =
7977
match st with
80-
| Return_ST(_, _, _) -> raise Stuck
81-
| Anal_ST(heap, stck, expr, envr) -> Anal_ST(heap, stck, ex, nv)
78+
| Return_ST(heap, Frame_SK(oldstck, newfrm), valu) -> Anal_ST(heap, oldstck, ex, nv)
79+
| _ -> raise Stuck
8280
let allocate (st: state) (ex: exp) (nv: env) (he, loc: (int * stoval) list * index): state =
8381
match st with
84-
| Return_ST(_, _, _) -> raise Stuck
85-
| Anal_ST(heap, stck, expr, envr) -> Anal_ST(he, stck, ex, [loc] @ nv)
82+
| Return_ST(heap, Frame_SK(oldstck, newfrm), valu) -> Anal_ST(he, oldstck, ex, [loc] @ nv)
83+
| _ -> raise Stuck
84+
let recurse (st: state) (ex: exp) (nv: env) (he, loc: (int * stoval) list * index): state =
85+
match st with
86+
| Return_ST(heap, stck, valu) -> Anal_ST(he, stck, ex, [loc] @ nv)
87+
| _ -> raise Stuck
8688
end
8789

8890
let context (txp: texp): int Gamma.t =
@@ -239,68 +241,67 @@ let rec step1 (e: exp): exp =
239241

240242
(* Problem 3.
241243
* step2 : state -> state *)
242-
let step2 (st: state): state =
243-
match st with
244-
| Anal_ST (heap, stck, expr, envr: stoval Heap.heap * stack * exp * env) -> (
245-
match expr with
246-
| Eunit -> ControlFlow.return (st) (VEunit)
247-
| Ind(x) -> (
248-
if ((List.length (envr)) <= x) then raise Stuck
249-
else (
250-
let fram = Heap.deref (heap) (List.nth (envr) (x)) in
251-
match fram with
252-
| Computed(valu) -> ControlFlow.return (st) (valu)
253-
| Delayed(expr, envr) -> ControlFlow.call (st) (FLoc(List.nth (envr) (x))) (expr)
244+
let step2 (st: state): state =
245+
match st with
246+
| Anal_ST (heap, stck, expr, envr: stoval Heap.heap * stack * exp * env) -> (
247+
match expr with
248+
| Eunit -> ControlFlow.return (st) (VEunit)
249+
| Ind(x) -> (
250+
if ((List.length (envr)) <= x) then raise Stuck
251+
else (
252+
let fram = Heap.deref (heap) (List.nth (envr) (x)) in
253+
match fram with
254+
| Computed(valu) -> ControlFlow.return (st) (valu)
255+
| Delayed(expr, envr_d) -> Anal_ST (heap, Frame_SK(stck, FLoc(List.nth (envr) (x))), expr, envr_d)
256+
)
254257
)
258+
| Lam(elam) -> ControlFlow.return (st) (VClosure(envr, Lam(elam)))
259+
| App(efun, earg) -> ControlFlow.call (st) (FApp(envr, earg)) (efun) (envr)
260+
| Pair(efst, esnd) -> ControlFlow.return (st) (VClosure(envr, Pair(efst, esnd)))
261+
| Fst(epair) -> ControlFlow.call (st) (FFst) (epair) (envr)
262+
| Snd(epair) -> ControlFlow.call (st) (FSnd) (epair) (envr)
263+
| Case(ecase, el, er) -> ControlFlow.call (st) (FCase(envr, el, er)) (ecase) (envr)
264+
| Inl(ecase) -> ControlFlow.return (st) (VInl(envr, ecase))
265+
| Inr(ecase) -> ControlFlow.return (st) (VInr(envr, ecase))
266+
| Fix(expr) -> ControlFlow.return (st) (VClosure(envr, Fix(expr)))
267+
| True -> ControlFlow.return (st) (VTrue)
268+
| False -> ControlFlow.return (st) (VFalse)
269+
| Ifthenelse(eif, etrue, efalse) -> ControlFlow.call (st) (FIfthenelse(envr, etrue, efalse)) (eif) (envr)
270+
| Num(n) -> ControlFlow.return (st) (VNum(n))
271+
| Plus -> ControlFlow.return (st) (VPlus)
272+
| Minus -> ControlFlow.return (st) (VMinus)
273+
| Eq -> ControlFlow.return (st) (VEq)
255274
)
256-
| Lam(elam) -> ControlFlow.return (st) (VClosure(envr, Lam(elam)))
257-
| App(efun, earg) -> ControlFlow.call (st) (FApp(envr, earg)) (efun)
258-
| Pair(efst, esnd) -> ControlFlow.return (st) (VClosure(envr, Pair(efst, esnd)))
259-
| Fst(epair) -> ControlFlow.call (st) (FFst) (epair)
260-
| Snd(epair) -> ControlFlow.call (st) (FSnd) (epair)
261-
| Case(ecase, el, er) -> ControlFlow.call (st) (FCase(envr, el, er)) (ecase)
262-
| Inl(ecase) -> ControlFlow.return (st) (VInl(envr, ecase))
263-
| Inr(ecase) -> ControlFlow.return (st) (VInr(envr, ecase))
264-
| Fix(expr) -> ControlFlow.return (st) (VClosure(envr, Fix(expr)))
265-
| True -> ControlFlow.return (st) (VTrue)
266-
| False -> ControlFlow.return (st) (VFalse)
267-
| Ifthenelse(eif, etrue, efalse) -> ControlFlow.call (st) (FIfthenelse(envr, etrue, efalse)) (eif)
268-
| Num(n) -> ControlFlow.return (st) (VNum(n))
269-
| Plus -> ControlFlow.return (st) (VPlus)
270-
| Minus -> ControlFlow.return (st) (VMinus)
271-
| Eq -> ControlFlow.return (st) (VEq)
275+
| Return_ST (heap, stck, envr: stoval Heap.heap * stack * value) -> (
276+
match stck with
277+
| Hole_SK -> raise Stuck
278+
| Frame_SK (stck, fr) ->
279+
(match fr, envr with
280+
| _, VEunit -> raise Stuck
281+
| _, VClosure(nlam, Fix(exp)) -> ControlFlow.recurse (st) (exp) (nlam) (Heap.allocate (heap) (Delayed(Fix(exp), nlam)))
282+
| (FLoc (idx), env) -> Return_ST(Heap.update (heap) (idx) (Computed env), stck, env)
283+
| (FApp (napp, eapp), VClosure (nfun, Lam (efun))) -> ControlFlow.allocate (st) (efun) (nfun) (Heap.allocate (heap) (Delayed(eapp, napp)))
284+
| (FFst, VClosure(npair, Pair(efst, esnd))) -> ControlFlow.branch (st) (efst) (npair)
285+
| (FSnd, VClosure(npair, Pair(efst, esnd))) -> ControlFlow.branch (st) (esnd) (npair)
286+
| (FCase(ncase, el, er), VInl(ninl, ecase)) -> ControlFlow.allocate (st) (el) (ncase) (Heap.allocate (heap) (Delayed(ecase, ninl)))
287+
| (FCase(ncase, el, er), VInr(ninr, ecase)) -> ControlFlow.allocate (st) (er) (ncase) (Heap.allocate (heap) (Delayed(ecase, ninr)))
288+
| (FIfthenelse(nif, etrue, efalse), VTrue) -> ControlFlow.branch (st) (etrue) (nif)
289+
| (FIfthenelse(nif, etrue, efalse), VFalse) -> ControlFlow.branch (st) (efalse) (nif)
290+
| (FApp(napp, eapp), VPlus) -> ControlFlow.call (st) (FPlus) (eapp) (napp)
291+
| (FApp(napp, eapp), VMinus) -> ControlFlow.call (st) (FMinus) (eapp) (napp)
292+
| (FApp(napp, eapp), VEq) -> ControlFlow.call (st) (FEq) (eapp) (napp)
293+
| (FPlus, VClosure(nfun, Pair(efst, esnd))) -> ControlFlow.call (st) (FPlus_Env_Exp(nfun, esnd)) (efst) (nfun)
294+
| (FMinus, VClosure(nfun, Pair(efst, esnd))) -> ControlFlow.call (st) (FMinus_Env_Exp(nfun, esnd)) (efst) (nfun)
295+
| (FEq, VClosure(nfun, Pair(efst, esnd))) -> ControlFlow.call (st) (FEq_Env_Exp(nfun, esnd)) (efst) (nfun)
296+
| (FPlus_Env_Exp(nplus, eplus), VNum(i)) -> ControlFlow.call (st) (FPlus_Num(i)) (eplus) (nplus)
297+
| (FMinus_Env_Exp(nminus, eminus), VNum(i)) -> ControlFlow.call (st) (FMinus_Num(i)) (eminus) (nminus)
298+
| (FEq_Env_Exp(neq, eeq), VNum(i)) -> ControlFlow.call (st) (FEq_Num(i)) (eeq) (neq)
299+
| (FPlus_Num(i), VNum(j)) -> ControlFlow.return (st) (VNum(i + j))
300+
| (FMinus_Num(i), VNum(j)) -> ControlFlow.return (st) (VNum(i - j))
301+
| (FEq_Num(i), VNum(j)) -> ControlFlow.return (st) (if i = j then VTrue else VFalse)
302+
| _ -> raise Stuck
303+
)
272304
)
273-
| Return_ST (heap, stck, envr: stoval Heap.heap * stack * value) -> (
274-
match stck with
275-
| Hole_SK -> raise Stuck
276-
| Frame_SK (stck, fr) ->
277-
(match fr, envr with
278-
| _, VEunit -> raise Stuck
279-
| _, VClosure(nlam, Fix(exp)) -> ControlFlow.allocate (st) (exp) (nlam) (Heap.allocate (heap) (Delayed(Fix(exp), nlam)))
280-
| (FLoc (idx), env) -> Return_ST(Heap.update (heap) (idx) (Computed env), stck, env)
281-
| (FApp (napp, eapp), VClosure (nfun, Lam (efun))) -> ControlFlow.allocate (st) (efun) (nfun) (Heap.allocate (heap) (Delayed(eapp, napp)))
282-
| (FFst, VClosure(npair, Pair(efst, esnd))) -> ControlFlow.branch (st) (efst) (npair)
283-
| (FSnd, VClosure(npair, Pair(efst, esnd))) -> ControlFlow.branch (st) (esnd) (npair)
284-
| (FCase(ncase, el, er), VInl(ninl, ecase)) -> ControlFlow.allocate (st) (el) (ncase) (Heap.allocate (heap) (Delayed(ecase, ninl)))
285-
| (FCase(ncase, el, er), VInr(ninr, ecase)) -> ControlFlow.allocate (st) (er) (ncase) (Heap.allocate (heap) (Delayed(ecase, ninr)))
286-
| (FIfthenelse(nif, etrue, efalse), VTrue) -> ControlFlow.branch (st) (etrue) (nif)
287-
| (FIfthenelse(nif, etrue, efalse), VFalse) -> ControlFlow.branch (st) (efalse) (nif)
288-
| (FApp(napp, eapp), VPlus) -> ControlFlow.jump (st) (FPlus) (eapp) (napp)
289-
| (FApp(napp, eapp), VMinus) -> ControlFlow.jump (st) (FMinus) (eapp) (napp)
290-
| (FApp(napp, eapp), VEq) -> ControlFlow.jump (st) (FEq) (eapp) (napp)
291-
| (FPlus, VClosure(nfun, Pair(efst, esnd))) -> ControlFlow.jump (st) (FPlus_Env_Exp(nfun, esnd)) (efst) (nfun)
292-
| (FMinus, VClosure(nfun, Pair(efst, esnd))) -> ControlFlow.jump (st) (FMinus_Env_Exp(nfun, esnd)) (efst) (nfun)
293-
| (FEq, VClosure(nfun, Pair(efst, esnd))) -> ControlFlow.jump (st) (FEq_Env_Exp(nfun, esnd)) (efst) (nfun)
294-
| (FPlus_Env_Exp(nplus, eplus), VNum(i)) -> ControlFlow.jump (st) (FPlus_Num(i)) (eplus) (nplus)
295-
| (FMinus_Env_Exp(nminus, eminus), VNum(i)) -> ControlFlow.jump (st) (FMinus_Num(i)) (eminus) (nminus)
296-
| (FEq_Env_Exp(neq, eeq), VNum(i)) -> ControlFlow.jump (st) (FEq_Num(i)) (eeq) (neq)
297-
| (FPlus_Num(i), VNum(j)) -> ControlFlow.return (st) (VNum(i + j))
298-
| (FMinus_Num(i), VNum(j)) -> ControlFlow.return (st) (VNum(i - j))
299-
| (FEq_Num(i), VNum(j)) -> ControlFlow.return (st) (if i = j then VTrue else VFalse)
300-
| _ -> raise Stuck
301-
)
302-
)
303-
304305
(* exp2string : Tml.exp -> string *)
305306
let rec exp2string exp =
306307
match exp with
@@ -323,12 +324,35 @@ let rec exp2string exp =
323324
| Num n -> "<" ^ (string_of_int n) ^ ">"
324325
| Plus -> "+" | Minus -> "-" | Eq -> "="
325326

327+
let rec val2string (vlu: value): string =
328+
match vlu with
329+
| VClosure (_, func) -> (
330+
match func with
331+
| Lam(elam) -> "[env, lam. (" ^ (exp2string elam) ^ ")]"
332+
| Fix(efix) -> "[env, fix. (" ^ (exp2string efix) ^ ")]"
333+
| Pair(efst, esnd) -> "[env, (" ^ (exp2string efst) ^ "), (" ^ (exp2string esnd) ^ ")]"
334+
| _ -> "[env, (?)]"
335+
)
336+
| VInl(_, e) -> "inl. " ^ (exp2string e) ^ ""
337+
| VInr(_, e) -> "inr. " ^ (exp2string e) ^ ""
338+
| VPlus -> exp2string (Plus)
339+
| VMinus -> exp2string (Minus)
340+
| VEq -> exp2string (Eq)
341+
| VNum _ | VTrue | VFalse | VEunit -> exp2string (value2exp (vlu))
342+
326343
(* state2string : state -> string
327344
* you may modify this function for debugging your code *)
328-
let state2string st =
345+
let state2string (st: state): string =
346+
let stackdepth (stc: stack) =
347+
let rec stackdepth_tail (stc: stack) (dep: int) =
348+
match stc with
349+
| Hole_SK -> dep
350+
| Frame_SK(oldstck, newfrm) -> stackdepth_tail (oldstck) (dep + 1)
351+
in string_of_int (stackdepth_tail (stc) (0))
352+
in
329353
match st with
330-
| Anal_ST(_,_,exp,_) -> "Analysis : " ^ exp2string (exp)
331-
| Return_ST(_,_,valu) -> "Return : " ^ exp2string (value2exp (valu))
354+
| Anal_ST(_, stck, expr, _) -> "{{"^ stackdepth (stck) ^ "}} -> (" ^ (exp2string (expr)) ^ ")"
355+
| Return_ST(_, stck, valu) -> "{{"^ stackdepth (stck) ^ "}} <- (" ^ (val2string (valu)) ^ ")"
332356

333357
(* ------------------------------------------------------------- *)
334358
let stepOpt1 e = try Some (step1 e) with Stuck -> None

‎HW/HW6/hw6

164 KB
Binary file not shown.

0 commit comments

Comments
 (0)