diff options
Diffstat (limited to 'code')
| -rw-r--r-- | code/krivine.ml | 250 | ||||
| -rw-r--r-- | code/zam.ml | 546 |
2 files changed, 796 insertions, 0 deletions
diff --git a/code/krivine.ml b/code/krivine.ml new file mode 100644 index 0000000..dfbdd4a --- /dev/null +++ b/code/krivine.ml @@ -0,0 +1,250 @@ +(*********************************************) +(* (Extended) Krivine Machine implementation *) +(* *) +(* Guillermo Ramos Gutiérrez (2015) *) +(*********************************************) + + +(*********) +(* Utils *) +(*********) +let print_with f x = print_endline (f x) +let concat_with sep f xs = String.concat sep (List.map f xs) + +let rec find_idx_exn x = function + | [] -> raise Not_found + | (y::ys) -> if x = y then 0 else 1 + find_idx_exn x ys + +let rec map_rev f xs = + let rec iter acc = function + | [] -> acc + | (x::xs) -> iter (f x :: acc) xs in + iter [] xs + +type symbol = string * int +let show_symbol (s, _) = s +let symbol : string -> symbol = + let id = ref 0 in + let gensym c : symbol = + let newid = !id in + id := !id + 1; + (c, newid) + in + gensym + + +(**************************************) +(* (Extended) Untyped Lambda Calculus *) +(**************************************) +module Lambda = struct + type t = Var of symbol | App of t * t | Abs of symbol * t + | If of t * t * t | True | False + | Constr of t constr | Case of t * (symbol constr * t) list + | Fix of symbol * t + and 'a constr = symbol * 'a list + + let rec show m = + let show_branch ((x, args), m) = + "(" ^ show_symbol x ^ "(" ^ concat_with "," show_symbol args ^ ") → " + ^ show m ^ ")" in + match m with + | Var x -> show_symbol x + | App (m1, m2) -> "(" ^ show m1 ^ " " ^ show m2 ^ ")" + | Abs (x, m) -> "(λ" ^ show_symbol x ^ "." ^ show m ^ ")" + | If (m1, m2, m3) -> "if " ^ show m1 + ^ " then " ^ show m2 + ^ " else " ^ show m3 + | True -> "True" | False -> "False" + | Constr (x, ms) -> show_symbol x ^ "(" ^ concat_with ", " show ms ^ ")" + | Case (m, bs) -> "(case " ^ show m ^ " of " + ^ concat_with " " show_branch bs ^ ")" + | Fix (x, m) -> "fix(λ" ^ show_symbol x ^ "." ^ show m ^ ")" + let print = print_with show + + (* Constants *) + let none = symbol "None" + let some = symbol "Some" + + (* Peano arithmetic *) + let z = symbol "z" + let s = symbol "s" + + let rec peano_add n x = + if n == 0 then x else peano_add (n-1) (Constr (s, [x])) + + let peano_of_int ?(base=Constr (z, [])) n = peano_add n base + + (* Examples *) + let m1 = + let x = symbol "x" in + let y = symbol "y" in + let z = symbol "z" in + App (Abs (x, Var x), App (Abs (y, Var y), Abs (z, Var z))) + + let plus = + let m = symbol "m" in + let n = symbol "n" in + let f = symbol "f" in + let x = symbol "x" in + Abs (m, Abs (n, Abs (f, Abs (x, App (App (Var m, Var f), + App (App (Var n, Var f), Var x)))))) + + let nested_if = + If (True, If (False, False, True), False) + + (* s((λx.x) z) *) + let constr_test = + let x = symbol "x" in + peano_of_int ~base:(App (Abs (x, Var x), Constr (z, []))) 1 + + (* (λc. case c of (Some(x) → x) (None → c)) Some(s(z))) *) + let case_some = + let c = symbol "c" in + let x = symbol "x" in + App (Abs (c, Case (Var c, [((some, [x]), Var x); ((none, []), Var c)])), + Constr (some, [peano_of_int 1])) + + (* (λc. case c of (Triple(x,y,z) → y)) Triple(1,2,3)) *) + let case_triple = + let c = symbol "c" in + let x = symbol "x" in + let y = symbol "y" in + let z = symbol "z" in + let triple = symbol "triple" in + App (Abs (c, Case (Var c, [((triple, [x;y;z]), Var y)])), + Constr (triple, List.map peano_of_int [1;2;3])) + + (* fix(λf.λc. case c of (s(x) → s(s(f x))) (z → z)) s(s(s(z))) *) + let fix_dup = + let f = symbol "f" in + let c = symbol "c" in + let x = symbol "x" in + App (Fix (f, Abs (c, Case (Var c, + [((s, [x]), peano_add 2 (App (Var f, Var x))); + ((z, []), peano_of_int 0)]))), + peano_of_int 3) + + (* fix(λf.λg.λc. case c of (s(x) → g (f g x)) (z → z)) (λy.s(s(y))) s(s(s(z))) *) + let fix_scale = + let f = symbol "f" in + let g = symbol "g" in + let c = symbol "c" in + let x = symbol "x" in + let y = symbol "y" in + App (App (Fix (f, Abs (g, Abs (c, Case (Var c, + [((s, [x]), App (Var g, (App (App (Var f, Var g), Var x)))); + ((z, []), peano_of_int 0)])))), + Abs (y, peano_add 2 (Var y))), + peano_of_int 3) +end + + +(**************************************************) +(* Untyped lambda calculus with De Bruijn indices *) +(**************************************************) +module DBILambda = struct + type dbi_symbol = int * symbol + type t = Var of dbi_symbol | App of t * t | Abs of symbol * t + | If of t * t * t | True | False + | Constr of t constr | Case of t * (symbol constr * t) list + | Fix of symbol * t + and 'a constr = symbol * 'a list + + let dbi dbis x = (find_idx_exn x dbis, x) + + let show_dbi_symbol (n, x) = show_symbol x + let rec show m = + match m with + | Var x -> show_dbi_symbol x + | App (m1, m2) -> "(" ^ show m1 ^ " " ^ show m2 ^ ")" + | Abs (x, m) -> "(λ" ^ show_symbol x ^ "." ^ show m ^ ")" + | If (m1, m2, m3) -> "if " ^ show m1 + ^ " then " ^ show m2 + ^ " else " ^ show m3 + | True -> "True" | False -> "False" + | Constr (x, ms) -> show_symbol x ^ "(" ^ concat_with ", " show ms ^ ")" + | Case (m, bs) -> "(case " ^ show m ^ " of " + ^ concat_with " " show_branch bs ^ ")" + | Fix (x, m) -> "fix(λ" ^ show_symbol x ^ "." ^ show m ^ ")" + and show_branch ((x, args), m) = + "(" ^ show_symbol x ^ "(" ^ concat_with "," show_symbol args ^ ") → " + ^ show m ^ ")" + let print = print_with show + + let of_lambda = + let rec of_lambda dbis = function + | Lambda.Var x -> let (n, x) = dbi dbis x in Var (n, x) + | Lambda.App (m1, m2) -> App (of_lambda dbis m1, of_lambda dbis m2) + | Lambda.Abs (x, m) -> Abs (x, of_lambda (x :: dbis) m) + | Lambda.If (m1, m2, m3) -> If (of_lambda dbis m1, + of_lambda dbis m2, of_lambda dbis m3) + | Lambda.True -> True | Lambda.False -> False + | Lambda.Constr (x, ms) -> Constr (x, List.map (of_lambda dbis) ms) + | Lambda.Case (m, bs) -> Case (of_lambda dbis m, + List.map (trans_br dbis) bs) + | Lambda.Fix (x, m) -> Fix (x, of_lambda (x :: dbis) m) + and trans_br dbis ((x, args), m) = + let dbis = List.rev args @ dbis in + ((x, args), of_lambda dbis m) in + of_lambda [] +end + + +(*******************) +(* Krivine Machine *) +(*******************) +module KM = struct + open DBILambda + + type st_elm = Clos of DBILambda.t * stack + | IfCont of DBILambda.t * DBILambda.t + | CaseCont of (symbol constr * t) list * stack + | FixClos of symbol * DBILambda.t * stack + and stack = st_elm list + + type state = DBILambda.t * stack * stack + + let reduce m = + let rec reduce (st : state) : DBILambda.t = + match st with + (* Pure lambda calculus *) + | (Var (0, _), s, Clos (m, e') :: e) -> reduce (m, s, e') + | (Var (0, _), s, FixClos (f, m, e') :: e) -> + reduce (m, s, FixClos (f, m, e') :: e') + | (Var (n, x), s, _ :: e) -> reduce (Var (n-1, x), s, e) + | (App (m1, m2), s, e) -> reduce (m1, Clos (m2, e) :: s, e) + | (Abs (_, m), c :: s, e) -> reduce (m, s, c :: e) + (* Conditionals *) + | (If (m1, m2, m3), s, e) -> reduce (m1, IfCont (m2, m3) :: s, e) + | (True, IfCont (m2, m3) :: s, e) -> reduce (m2, s, e) + | (False, IfCont (m2, m3) :: s, e) -> reduce (m3, s, e) + (* Case expressions (+ constructors) *) + | (Case (m, bs), s, e) -> reduce (m, CaseCont (bs, e) :: s, e) + | (Constr (x, ms), CaseCont (((x', args), m) :: bs, e') :: s, e) + when x == x' && List.length ms == List.length args -> + reduce (List.fold_left (fun m x -> Abs (x, m)) m args, + map_rev (fun m -> Clos (m, e)) ms @ s, e') + | (Constr (x, ms), CaseCont (_ :: bs, e') :: s, e) -> + reduce (Constr (x, ms), CaseCont (bs, e') :: s, e) + | (Constr (x, ms), s, e) -> + Constr (x, List.map (fun m -> reduce (m, s, e)) ms) + (* Fixpoints *) + | (Fix (x, m), s, e) -> reduce (m, s, FixClos (x, m, e) :: e) + (* Termination *) + | (m, [], []) -> m + | (_, _, _) -> m in + reduce (m, [], []) +end + + +let do_compile_and_red m = + let dbi_m = DBILambda.of_lambda m in + print_endline ("# Lambda term:\n " ^ DBILambda.show dbi_m); + let red_m = KM.reduce dbi_m in + print_endline ("# Reduced term:\n " ^ DBILambda.show red_m); + print_endline "--------------------------------------------------------------\n" + +let () = + let open Lambda in + List.iter do_compile_and_red [m1; plus; nested_if; constr_test; + case_some; case_triple; fix_dup; fix_scale] diff --git a/code/zam.ml b/code/zam.ml new file mode 100644 index 0000000..07fb85e --- /dev/null +++ b/code/zam.ml @@ -0,0 +1,546 @@ +let print_with f x = print_endline (f x) +let concat_with sep f xs = String.concat sep (List.map f xs) +let split n xs = + let rec split_acc n xs ys = match (n, ys) with + | (0, _) | (_, []) -> (List.rev xs, ys) + | (n, y :: ys) -> split_acc (n-1) (y::xs) ys in + split_acc n [] xs +let find_idx a = + let rec find_acc n = function + | [] -> raise Not_found + | (x :: xs) -> if a == x then n else find_acc (n+1) xs in + find_acc 0 +let rec repeat n x = if n == 0 then [] else x :: repeat (n-1) x +let fold_left1 f = function + | [] -> raise (Invalid_argument "empty string") + | (x::xs) -> List.fold_left f x xs + +let dbg_lev = 5 +let debug lev spaces s = + if dbg_lev >= lev + then print_endline (" -- " ^ String.concat "" (repeat spaces " ") ^ s) + +(* Compile, decompile and reduce errors *) +exception CpErr of string +exception DcErr of string +exception RdErr of string + +module CCLambda = struct + type symbol = string * int + let symbol : string -> symbol = + let id = ref 0 in + let gensym c : symbol = + let newid = !id in + id := !id + 1; + (c, newid) + in + gensym + + type t = Var of symbol | App of t * t | Abs of symbol * t + | Constr of t constr | Case of t * (symbol constr * t) list + | Fix of symbol * symbol list * symbol * t + | Acc of t + and 'a constr = symbol * 'a list + + let show_symbol (s, n) = + if dbg_lev > 2 then s ^ "/" ^ string_of_int n else s + let rec show m = + let show_branch ((x, vs), m) = + "(" ^ show_symbol x ^ "(" ^ concat_with "," show_symbol vs ^ ") → " + ^ show m ^ ")" in + match m with + | Var x -> show_symbol x + | App (m1, m2) -> "(" ^ show m1 ^ " " ^ show m2 ^ ")" + | Abs (x, m) -> "(λ" ^ show_symbol x ^ "." ^ show m ^ ")" + | Constr (x, ms) -> show_symbol x ^ "(" ^ concat_with ", " show ms ^ ")" + | Case (m, bs) -> "(case " ^ show m ^ " of " + ^ concat_with " " show_branch bs ^ ")" + | Fix (f, xs, c, m) -> + "fix_" ^ string_of_int (List.length xs) + ^ "(λ" ^ concat_with ".λ" show_symbol (f::xs@[c]) + ^ ". " ^ show m ^ ")" + | Acc m -> "[" ^ show m ^ "]" + let print = print_with show + + (* Auxiliar term-generating functions *) + let identity s = + let x = symbol s in + Abs (x, Var x) + + let rec appN n f m = if n = 0 then m else appN (n-1) f (App (f, m)) + let apps = fold_left1 (fun m n -> App (m, n)) + + let church_of_int n = + let f = symbol "f" in + let x = symbol "x" in + Abs (f, Abs (x, appN n (Var f) (Var x))) + + let none = symbol "None" + let some = symbol "Some" + let cons = symbol "Cons" + let nil = symbol "Nil" + + (* Peano arithmetic *) + let z = symbol "z" + let s = symbol "s" + + let rec peano_add n x = + if n == 0 then x else peano_add (n-1) (Constr (s, [x])) + + let peano_of_int n = peano_add n (Constr (z, [])) + + (* Examples *) + + (* (λx.λy. (x y)) (λxx.xx) *) + let partial = + let x = symbol "x" in + let y = symbol "y" in + App (Abs (x, Abs (y, App (Var x, Var y))), + identity "xx") + + (* (λm.λn.λf.λx. (m f)((n f) x) *) + let plus = + let m = symbol "m" in + let n = symbol "n" in + let f = symbol "f" in + let x = symbol "x" in + Abs (m, Abs (n, Abs (f, Abs (x, App (App (Var m, Var f), + App (App (Var n, Var f), Var x)))))) + + let _3plus1 = + App (App (plus, church_of_int 3), church_of_int 1) + + (* (λf.λx. f (f x)) (λy.y) (λz.z) *) + let twiceId = + let f = symbol "f" in + let x = symbol "x" in + App (App (Abs (f, Abs (x, App (Var f, App (Var f, Var x)))), + identity "y"), + identity "z") + + (* (λc. case c of (Some(x) → x) (None → c)) Some(s(z))) *) + let case_some = + let c = symbol "c" in + let x = symbol "x" in + App (Abs (c, Case (Var c, [((some, [x]), Var x); ((none, []), Var c)])), + Constr (some, [peano_of_int 1])) + + (* (λc. case c of (Cons(x, xs) → x) (Nil → Nil)) Cons(λx.x, Nil) *) + let case_head = + let c = symbol "c" in + let x = symbol "x" in + let xs = symbol "xs" in + App (Abs (c, Case (Var c, [((cons, [x;xs]), Var x); + ((nil, []), Constr (nil, []))])), + Constr (cons, [identity "m"; Constr (nil, [])])) + + (* fix_0(λf.λc. case c of (s(x) → s(s(f x))) (z → z)) s(s(s(z))) *) + let fix_dup = + let f = symbol "f" in + let c = symbol "c" in + let x = symbol "x" in + App (Fix (f, [], c, Case (Var c, + [((s, [x]), peano_add 2 (App (Var f, Var x))); + ((z, []), peano_of_int 0)])), + peano_of_int 3) + + (* fix_1(λf.λg.λc. case c of (s(x) → g(f x)) (z → z)) (λy.s(s(y))) s(s(s(z))) *) + let fix_scale = + let f = symbol "f" in + let g = symbol "g" in + let c = symbol "c" in + let x = symbol "x" in + let y = symbol "y" in + App (App (Fix (f, [g], c, Case (Var c, + [((s, [x]), App (Var g, (App (Var f, Var x)))); + ((z, []), peano_of_int 0)])), + Abs (y, peano_add 2 (Var y))), + peano_of_int 1) + + (* (λx.x) (λy. ((λz.z) y) (λt.t) *) + let acc_app = + let y = symbol "y" in + App (identity "x", + Abs (y, App (App (identity "z", + Var y), + identity "t"))) + + (* (λc. case c of (Cons(x, xs) → x) (Nil → Nil)) *) + let acc_case = + let c = symbol "c" in + let x = symbol "x" in + let xs = symbol "xs" in + Abs (c, Case (Var c, [((cons, [x;xs]), Var c); + ((nil, []), Constr (nil, []))])) + + (* fix_0(λf.λn. case c of (s(x) → s(s(f x))) (z → z)) *) + let acc_fix = + let f = symbol "f" in + let c = symbol "c" in + let x = symbol "x" in + Fix (f, [], c, Case (Var c, + [((s, [x]), peano_add 2 (App (Var f, Var x))); + ((z, []), peano_of_int 0)])) + +end + +module WeakRed : sig + type instrs + type mval + + val show_instrs : instrs -> string + val show_mval : mval -> string + + val compile : CCLambda.t -> instrs + val decompile : instrs -> CCLambda.t + + val am_reduce : instrs -> mval + val extract : mval -> CCLambda.t + + val reduce : CCLambda.t -> CCLambda.t +end = struct + open CCLambda + + type dbi = symbol * int + type instr = + | ACCESS of dbi + | CLOSURE of instrs + | ACCLOSURE of symbol + | PUSHRETADDR of instrs + | APPLY of int + | GRAB of symbol + | RETURN + | MAKEBLOCK of symbol * int + | SWITCH of (symbol constr * instrs) list + | CLOSUREREC of (symbol * symbol list * symbol) * instrs + | GRABREC of symbol + and instrs = instr list + and accum = + | NoVar of symbol + | NoApp of accum * mval list + | NoCase of accum * instrs * env + | NoFix of accum * instrs * env + and mval = + | Accu of accum + | Cons of mval constr + | Clos of instrs * env + | Ret of instrs * env * int + and env = mval list + and stack = mval list + and state = { + st_c : instrs; + st_e : env; + st_s : stack; + st_n : int; + } + + let show_dbi = function + | (x, i) -> + string_of_int i ^ + if dbg_lev > 2 then " (" ^ show_symbol x ^ ")" else "" + let rec show_instr = function + | ACCESS dbi -> "ACCESS(" ^ show_dbi dbi ^ ")" + | CLOSURE is -> "CLOSURE(" ^ show_instrs is ^ ")" + | ACCLOSURE x -> "ACCLOSURE([" ^ show_symbol x ^ "])" + | PUSHRETADDR is -> "PUSHRETADDR(" ^ show_instrs is ^ ")" + | APPLY i -> "APPLY(" ^ string_of_int i ^ ")" + | GRAB x -> "GRAB(" ^ show_symbol x ^ ")" + | RETURN -> "RETURN" + | MAKEBLOCK (x, n) -> "MAKEBLOCK(#" ^ show_symbol x ^ ", " ^ + string_of_int n ^ ")" + | SWITCH bs -> "SWITCH(" ^ concat_with ", " show_branch bs ^ ")" + | CLOSUREREC (_, is) -> "CLOSUREREC(" ^ show_instrs is ^ ")" + | GRABREC x -> "GRABREC(" ^ show_symbol x ^ ")" + and show_branch (((c, _), _), is) = c ^ " → " ^ show_instrs is + and show_accum = function + | NoVar x -> "{NoVar: " ^ show_symbol x ^ "}" + | NoApp (k, mvs) -> "{NoApp: " ^ show_accum k ^ ", " + ^ concat_with ", " show_mval mvs ^ "}" + | NoCase (k, is, e) -> "{NoCase: " ^ show_accum k ^ ", " + ^ show_instrs is ^ ", " ^ show_env e ^ "}" + | NoFix (k, is, e) -> "{NoFix: " ^ show_accum k ^ ", " + ^ show_instrs is ^ ", " ^ show_env e ^ "}" + and show_mval mval = match mval with + | Accu k -> show_accum k + | Cons ((s, _), mvs) -> + "{#" ^ s ^ if List.length mvs == 0 then "}" + else ": " ^ concat_with ", " show_mval mvs ^ "}" + | Clos (is, e) -> "{Tλ: (" ^ show_instrs is ^ "), " + ^ (if List.length e > 0 && List.hd e == mval + then "{Tλ <fix>}::" ^ show_env (List.tl e) + else show_env e) + ^ "}" + | Ret (is, e, n) -> "{<RET>: (" ^ show_instrs is ^ "), " ^ show_env e ^ ", " + ^ string_of_int n ^ "}" + and show_env e = "[" ^ concat_with ", " show_mval e ^ "]" + and show_instrs is = concat_with "; " show_instr is + + let show_stk stk = "| " ^ concat_with "\n | " show_mval stk + let show_st {st_c; st_e; st_s; st_n} = + "\n/---------------------------------------------------\n" + ^ " C: " ^ show_instrs st_c ^ "\n" + ^ " E: " ^ show_env st_e ^ "\n" + ^ " S: " ^ show_stk st_s ^ "\n" + ^ " N: " ^ string_of_int st_n ^ "\n" + ^ "\\---------------------------------------------------" + + let ret = [RETURN] + + let compile (m : CCLambda.t) : instrs = + let open CCLambda in + + let e = [] in + let rec compile' e (is : instrs) m = + debug 3 3 ("COMPILING: " ^ show m); + debug 3 3 (" IN ENV: " ^ concat_with ", " show_symbol e); + match m with + | Var x -> begin + try ACCESS(x, find_idx x e) :: is + with Not_found -> raise (CpErr ("Var " ^ fst x ^ " not found")) + end + | Abs (x, m) -> CLOSURE(GRAB x :: compile' (x :: e) ret m) :: is + | App (m1, m2) -> let cont = compile' e [APPLY(1)] m1 in + PUSHRETADDR(is) :: compile' e cont m2 + | Constr (x, args) -> let f arg cont = compile' e cont arg in + let cont = [MAKEBLOCK (x, List.length args)] in + List.fold_right f (List.rev args) (cont @ is) + | Case (m, bs) -> + let compile_branch ((c, args), m) = + let dbi' = List.rev args @ e in + ((c, args), compile' dbi' ret m) in + let bs' = List.map compile_branch bs in + PUSHRETADDR(is) :: compile' e [SWITCH(bs')] m + | Fix (f, xs, c, m) -> + let cont = compile' (c :: List.rev xs @ f :: e) ret m in + CLOSUREREC((f, xs, c), + List.map (fun x -> GRAB x) xs @ GRABREC c :: cont) :: is + | Acc (Var x) -> ACCLOSURE x :: is + | Acc _ -> raise (CpErr "Trying to compile non-var accumulator") in + compile' e ret m + + let rec decompile' e s is = + debug 3 3 ("DECOMPILING: " ^ show_instrs is); + debug 3 3 (" IN ENV: " ^ concat_with ", " CCLambda.show e); + debug 3 3 (" IN STK: " ^ concat_with ", " CCLambda.show s); + match is with + | [] -> List.hd s + | [RETURN] -> List.hd s + | (ACCESS (_, i) :: is') -> decompile' e (List.nth e i :: s) is' + | (CLOSURE c_is :: is') -> decompile' e (decompile' e s c_is :: s) is' + | (PUSHRETADDR r_is :: is') -> decompile' e (decompile' e s is' :: s) r_is + | (APPLY i :: is) -> begin + match (i, s) with + | (1, a::b::_) -> App (a, b) + | (n, a::s') -> App (a, decompile' e s' [APPLY (n-1)]) + | _ -> raise (DcErr "Unable to decompile APPLY") + end + | (GRAB x :: is') -> Abs (x, decompile' (Var x :: e) s is') + | (MAKEBLOCK (x, n) :: is') -> let (args, st') = split n s in + decompile' e (Constr (x, args) :: s) is' + | (SWITCH brs :: is') -> begin + let decompile_br ((c, parms), is) = + let parms_m = List.map (fun x -> Var x) parms in + ((c, parms), decompile' (List.rev parms_m @ e) s is) in + match s with + | [] -> Case (Var (symbol "_"), List.map decompile_br brs) + | (a::s') -> Case (a, List.map decompile_br brs) + end + | (CLOSUREREC ((f, xs, c), is') :: is) -> + let m = decompile' (e) s is' in + decompile' e (Fix (f, xs, c, m) :: s) is + | (GRABREC x :: is') -> Abs (x, decompile' (Var x :: e) s is') + | _ -> raise (DcErr "Unable to decompile (unknown instruction)") + let decompile = decompile' [] [] + + let rec extract mv = + debug 3 3 ("EXTRACTING: " ^ show_mval mv); + match mv with + | Clos (is, _) -> decompile is + | Cons (x, mvs) -> Constr (x, List.map extract mvs) + | Accu k -> + let rec extract_accu = function + | (NoVar x) -> Acc (Var x) + | (NoApp (k, mvs)) -> + Acc (apps (extract_accu k :: List.map extract mvs)) + | (NoCase (k, is, e)) -> begin + match decompile' (List.map extract e) [] is with + | Case (m, bs) -> + let accu = extract_accu k in + Acc (Case (accu, bs)) + | _ -> raise (DcErr "Invalid decompilation of CASE accum.") + end + | (NoFix (k, is, e)) -> begin + match decompile' (List.map extract e) [] is with + | Fix (f, xs, c, m) -> + Acc (Fix (f, xs, c, App (m, extract_accu k))) + | _ -> raise (DcErr "Invalid decompilation of fixpt accum.") + end in + extract_accu k + | _ -> raise (DcErr "Unable to extract") + + let am_reduce is = + debug 3 3 ("REDUCING: " ^ show_instrs is); + let rec eval st = + debug 4 4 (show_st st); + let {st_c=c; st_e=e; st_s=s; st_n=n} = st in + match c with + | [] -> raise (RdErr "Empty code section") + | (instr :: c) -> begin + match instr with + | ACCESS ((x, _), i) -> begin + try eval {st with st_c=c; st_s=(List.nth e i :: s)} + with Not_found -> raise (RdErr ("Var " ^ x ^ " not found")) + end + | CLOSURE c' -> eval {st with st_c=c; st_s=(Clos(c', e) :: s)} + | ACCLOSURE x -> eval {st with st_c=c; st_s=(Accu(NoVar x) :: s)} + | PUSHRETADDR c' -> eval {st with st_c=c; st_s=(Ret(c', e, n) :: s)} + | APPLY i -> begin + match s with + | (Clos (c', e') :: s) -> + eval {st_c=c'; st_e=e'; st_s=s; st_n=i} + | (Accu k :: s) -> begin + let (args, s') = split i s in + match s' with + | (Ret (c', e', n') :: s'') -> + eval {st_c=c'; st_e=e'; + st_s=(Accu(NoApp(k,args)))::s''; st_n=n'} + | _ -> raise (RdErr "APPLY over accu with invalid stack") + end + | _ -> raise (RdErr "APPLY over non-closure mval") + end + | GRAB _ -> begin + if n == 0 then + match s with + | (Ret (c', e', n') :: s) -> + let clos = Clos (instr :: c, e) in + eval {st_c=c'; st_e=e'; st_s=clos::s; st_n=n'} + | [] -> Clos (instr :: c, e) + | _ -> raise (RdErr "GRAB (n=0) over non-retval") + else + match s with + | (v :: s) -> eval {st_c=c; st_e=v::e; st_s=s; st_n=n-1} + | _ -> raise (RdErr "GRAB (n>0) over empty stack") + end + | RETURN -> begin + if n == 0 then + match s with + | (v :: Ret (c', e', n') :: s) -> + eval {st_c=c'; st_e=e'; st_s=v::s; st_n=n'} + | [v] -> v + | _ -> raise (RdErr "RETURN over empty stack or non-retval") + else + match s with + | (Clos (c', e') :: s) -> + eval {st_c=c'; st_e=e'; st_s=s; st_n=n} + | _ -> raise (RdErr "RETURN over empty stack or non-retval") + end + | MAKEBLOCK (x, m) -> let (vs, s') = split m s in + eval {st_c=c; st_e=e; + st_s=(Cons (x, vs)::s'); st_n=n} + | SWITCH bs -> begin + match s with + | (Cons (x, vs) :: s) -> + let (_, c') = try List.find (fun ((y, _), _) -> y == x) bs + with Not_found -> + raise (RdErr "SWITCH constr id not found") in + let e' = List.rev vs @ e in + eval {st_c=c'; st_e=e'; st_s=s; st_n=0} + | (Accu k :: s) -> + let accu = Accu (NoCase (k, instr :: c, e)) in + eval {st_c=ret; st_e=e; st_s=accu::s; st_n=0} + | _ -> raise (RdErr "SWITCH over empty stack or non-constr") + end + | CLOSUREREC (_, c') -> let rec v = Clos (c', v::e) in + eval {st with st_c=c; st_s=v::s} + | GRABREC _ -> begin + match (s, n) with + | ([Accu k], 1) -> Accu (NoFix (k, c, e)) + | (Accu k :: s, n) -> + let accu = Accu (NoFix (k, instr :: c, e)) in + eval {st_c=ret; st_e=e; st_s=accu::s; st_n=n-1} + | (Ret (c', e', n') :: s, n) -> + let clos = Clos (instr :: c, e) in + eval {st_c=c'; st_e=e'; st_s=clos::s; st_n=n'} + | (mval :: s, n) -> + eval {st_c=c; st_e=mval::e; st_s=s; st_n=n-1} + | ([], 0) -> Clos (instr :: c, e) + | _ -> raise (RdErr "GRABREC over empty stack or invalid mval") + end + end in + let st = {st_c = is; st_e = []; st_s = []; st_n = 0} in + eval st + + let reduce m = debug 2 1 ("V( " ^ show m ^ " )"); + match m with + | App (m1, m2) -> m |> compile |> am_reduce |> extract + | _ -> m +end + +module StrongRed = struct + open CCLambda + + let rec extract_unique = function + | Var x -> x + | Acc x -> extract_unique x + | _ -> raise (RdErr "Trying to extract invalid value") + + let unique x = symbol (fst x) + + let rec reduce m = + debug 2 0 ("N( " ^ show m ^ " )"); + match m with + | Fix (f, xs, c, m) -> + let xs' = List.map unique xs in + let f' = unique f in + let c' = unique c in + let accs = List.map (fun x -> Acc (Var x)) (f' :: xs' @ [c']) in + (* debug 2 10 (concat_with " # " show accs); *) + let m' = reduce (apps (m :: accs)) in + Fix (f', xs', c', m') + | _ -> readback (WeakRed.reduce m) + and readback m = + debug 2 1 ("R( " ^ show m ^ " )"); + match m with + | Abs (x, m) -> let u = unique x in + Abs (u, reduce (App (Abs (x, m), Acc (Var u)))) + | Constr (x, vs) -> Constr (x, List.map readback vs) + | Acc k -> readback_acc k + | App (Fix (f, xs, c, m), p) -> + App (reduce (Fix (f, xs, c, m)), readback p) + (* | Fix (f, xs, c, m) -> *) + | _ -> raise (RdErr "Readback of invalid value") + and readback_acc m = + debug 2 2 ("R'( " ^ show m ^ " )"); + match m with + | Var x -> Var x + | App (k, v) -> App (readback_acc k, readback v) + | Acc (Var x) -> Var x + | Case (k, bs) -> let x = extract_unique k in + let b = Abs (x, Case (Var x, bs)) in + let rb_branch ((c, xs), m) = + let us = List.map unique xs in + let acc_us = List.map (fun x -> Acc (Var x)) us in + ((c, us), reduce (App (b, Constr (c, acc_us)))) in + Case (readback_acc k, List.map rb_branch bs) + | _ -> raise (RdErr "Readback of invalid accumulator") +end + +let test_weakred m = + print_endline "WEAK REDUCTION TEST"; + print_endline ("Target expression: '" ^ CCLambda.show m ^ "'..."); + + print_string "Compiling... "; + let compiled = WeakRed.compile m in + + print_endline "Reducing..."; + let reduced = WeakRed.am_reduce compiled in + print_endline ("Final value: " ^ CCLambda.show (WeakRed.extract reduced)) + +let test_strongred m = + print_endline "STRONG REDUCTION TEST"; + print_endline ("Target expression: '" ^ CCLambda.show m ^ "'..."); + print_endline ("Final value: " ^ CCLambda.show (StrongRed.reduce m)) + +let () = + let m = CCLambda.fix_scale in + test_strongred m |