21/07/15

8 files changed, 1035 insertions, 38 deletions

diff --git a/Makefile b/Makefile
index 7faec7d..1ca0edb 100644
--- a/Makefile
+++ b/Makefile
@@ -1,5 +1,5 @@
 all:
-	latexmk -pvc -lualatex tfm.tex
+	latexmk -pvc -lualatex -shell-escape tfm.tex
 
 once:
 	lualatex tfm.tex
diff --git a/bib.bib b/bib.bib
index ed7095e..4c559f3 100644
--- a/bib.bib
+++ b/bib.bib
@@ -197,4 +197,29 @@ simple, portable techniques, such as bytecode interpretation;
 a sophisticated execution model helps counterbalance the
 interpretation overhead.},
   xtopic = {caml}
-}
\ No newline at end of file
+}
+
+@book{PeytonJones87,
+ author = {Peyton Jones, Simon L.},
+ title = {The Implementation of Functional Programming Languages (Prentice-Hall International Series in Computer Science)},
+ year = {1987},
+ isbn = {013453333X},
+ publisher = {Prentice-Hall, Inc.},
+ address = {Upper Saddle River, NJ, USA},
+}
+
+@incollection{Mogensen00,
+year={2000},
+isbn={978-3-540-67102-2},
+booktitle={Perspectives of System Informatics},
+volume={1755},
+series={Lecture Notes in Computer Science},
+editor={Bjøner, Dines and Broy, Manfred and Zamulin, AlexandreV.},
+doi={10.1007/3-540-46562-6_11},
+title={Linear Time Self-Interpretation of the Pure Lambda Calculus},
+url={http://dx.doi.org/10.1007/3-540-46562-6_11},
+publisher={Springer Berlin Heidelberg},
+author={Mogensen, TorbenÆ.},
+pages={128-142},
+language={English}
+}
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
diff --git a/from-copy.sh b/from-copy.sh
index 52427ae..3321f23 100755
--- a/from-copy.sh
+++ b/from-copy.sh
@@ -2,5 +2,5 @@
 
 COPY_D="${HOME}/Copy/univ/master/tfm"
 
-cp -r ${COPY_D}/tfm.pdf ${COPY_D}/*.tex ${COPY_D}/Makefile ${COPY_D}/bib.bib .
+cp -r ${COPY_D}/code ${COPY_D}/tfm.pdf ${COPY_D}/*.tex ${COPY_D}/Makefile ${COPY_D}/bib.bib .
 cp -r ${COPY_D}/front/*.tex front/
diff --git a/tfm.pdf b/tfm.pdf
index 2f76967..550d88a 100644
--- a/tfm.pdf
+++ b/tfm.pdf
diff --git a/tfm.tex b/tfm.tex
index 2f60e2d..946ffa5 100644
--- a/tfm.tex
+++ b/tfm.tex
@@ -1,10 +1,12 @@
 \documentclass[12pt,a4paper,parskip=full]{scrreprt}
-\usepackage{scrhack} % http://tex.stackexchange.com/questions/51867/koma-warning-about-toc
+%\usepackage{scrhack} % http://tex.stackexchange.com/questions/51867/koma-warning-about-toc
 
 \usepackage[top=3.5cm,bottom=3.5cm,left=3cm,right=3cm]{geometry}
 
 % \usepackage[spanish]{babel}
-\usepackage{fontspec} \usepackage{url}
+\usepackage{lmodern}
+\usepackage{fontspec} \setmonofont{DejaVu Sans Mono}
+\usepackage{url}
 \usepackage{graphicx} \usepackage{cite} \usepackage{amsmath}
 \usepackage{mathtools} \usepackage{listings} \usepackage{syntax}
 % \usepackage[compact,small]{titlesec}
@@ -16,7 +18,7 @@
 \usepackage{amssymb} % arrows
 \usepackage{mathpartir} % inference rules
 
-% \usepackage{minted}
+\usepackage{minted}
 
 \usepackage{float}
 \floatstyle{boxed}
@@ -543,23 +545,24 @@ The \textbf{Lambda Calculus} \cite{Church36} is a formal system developed by
 Alonzo Church in the decade of 1930 as part of his research on the foundations
 of mathematics and computation (it was later proven to be equivalent to the
 Turing Machine). In its essence, the Lambda Calculus is a simple term rewriting
-system that represents computation through the application of functions.
+system that represents computation through the \textbf{application of
+  functions}.
 
-Following is the grammar representing Lambda \textbf{terms} ($\mathcal{T}$), or
-well-formed formulas:
+Following is the grammar representing \textbf{lambda terms} ($\mathcal{T}$),
+also called ``well-formed formulas'':
 
 \begin{bnf}[caption=Lambda Calculus, label={lst:lambda}]{}
   $\mathcal{T} ::= x$               variable
     | $(\lambda x . \mathcal{T})$           abstraction
     | $(\mathcal{T}_1 \: \mathcal{T}_2)$           application
-  $x ::= v_1, v_2, v_3, ...$               (infinite variables)
+  $x ::= v_1, v_2, v_3, ...$               (infinite variables available)
 \end{bnf}
 
 Intuitively, the \textbf{abstraction} rule represents function creation: take an
-existing term ($\mathcal{T}$) and parameterize it with an argument ($x$).  The
-variable $x$ \textbf{binds} every instance of the same variable on the body,
-which we say are \textbf{bound} instances. The \textbf{application} represents
-function evaluation ($\mathcal{T}_1$) with an actual argument ($\mathcal{T}_2)$.
+existing term ($\mathcal{T}$) and parameterize it with an argument ($x$). The
+variable $x$ binds every instance of the same variable on the body, which we say
+are \textbf{bound} instances. The \textbf{application} rule represents function
+evaluation ($\mathcal{T}_1$) with an actual argument ($\mathcal{T}_2)$.
 
 Seen as a term rewriting system, the Lambda Calculus has some reduction rules
 that can be applied over terms in order to perform the computation:
@@ -584,13 +587,13 @@ $\beta$-reduced following the rule. The semantics of the rule match with the
 intuition of function application: the result is the body of the function with
 the formal parameter replaced by the actual argument.
 
-The syntax $\mathcal{T}_1[x := \mathcal{T}_2]$ replaces $x$ by $\mathcal{T}_2$
-in the body of $\mathcal{T}_1$, but we have to be careful in its definition,
-because the ``obvious/naïve'' substitution process can lead to unexpected
-results. For example, $(\lambda x . y)[y := x]$ would $\beta$-reduce to
-$(\lambda x . x)$, which is not the expected result: the new $x$ in the body has
-been \textbf{captured} by the argument and the function behavior is now
-different.
+The \textbf{substitution operation} $\mathcal{T}_1[x := \mathcal{T}_2]$ replaces
+$x$ by $\mathcal{T}_2$ in the body of $\mathcal{T}_1$, but we have to be careful
+in its definition, because the ``obvious/naïve'' substitution process can lead
+to unexpected results. For example, $(\lambda x . y)[y := x]$ would
+$\beta$-reduce to $(\lambda x . x)$, which is not the expected result: the new
+$x$ in the body has been \textbf{captured} by the argument and the function
+behavior is now different.
 
 The solution to this problem comes from the intuitive idea that ``the exact
 choice of names for bound variables is not really important''. The functions
@@ -609,7 +612,7 @@ rule is the following:
 So, to correctly apply a $\beta$-reduction, we will do \textbf{capture-avoiding
   substitutions}: if there is the danger of capturing variables during a
 substitution, we will first apply $\alpha$-conversions to change the problematic
-variables by fresh ones. 
+variables by fresh ones.
 
 Another equivalence relation over lambda terms is the one defined by the
 \textbf{eta conversion} ($\eta$-conversion), and follows by the extensional
@@ -625,23 +628,96 @@ equivalence of functions in the calculus:
 In general, we will treat $\alpha$-equivalent and $\eta$-equivalent functions as
 interchangeable.
 
-http://adam.chlipala.net/cpdt/html/Equality.html
 
-\begin{itemize}
-\item Alpha reduction
-\item Beta reduction
-\item ...
-\end{itemize}
+\subsection{Types}
+
+Until now, we have been discussing the \textbf{untyped} Lambda Calculus, where
+there are no restrictions to the kind of terms we can build. Every formula
+resulting from the grammar (\ref{lst:lambda}) is a valid term. There are
+alternative interpretations of the Lambda Calculus, the \textbf{Typed Lambda
+  Calculi}, which give \textbf{typing rules} to construct ``well-typed terms''
+(terms that have a \textbf{type} associated to it). The point is being unable to
+construct terms that ``make no sense'', like the ones that encode logical
+paradoxes or whose evaluation does not finish.
+
+As previously seen, EasyCrypt uses a statically typed expression language that
+in turn is represented internally as a typed Lambda Calculus. (TODO: put in
+context)
 
 
 \subsection{Extensions}
 
-\subsubsection{Case expressions}
+Until there we have seen the ``basic'', or ``pure'' Lambda Calculus, where the
+only data primitive is the function. Being turing complete, it is all that is
+needed to express all the possible computations, but there are extensions that
+make it more suitable to be manipulated by human beings.
+
+One of the most typical is having natural numbers as primitive terms, that is
+way more convenient that representing them as \textbf{church numerals}:
+
+$$0 \Longleftrightarrow (\lambda f . (\lambda x . x))$$
+$$1 \Longleftrightarrow (\lambda f . (\lambda x . (f \: x)))$$
+$$2 \Longleftrightarrow (\lambda f . (\lambda x . (f \: (f \: x))))$$
+$$...$$
+
+As with the natural numbers, any data structure can be encoded in basic Lambda
+Calculus \cite{Mogensen00}, but the representation is complex and the terms can
+rapidly become very difficult to handle. This is why the first major extension
+comes in: \textbf{algebraic data types}.
+
+\subsubsection{Algebraic Data Types}
+
+If we want to be able to extend the Lambda Calculus to encode structured data,
+we will want to have some way to build new data, instead of extending the
+language with every data type we can imagine (naturals, booleans,
+etc.). \textbf{Algebraic data types} (ADT's) offer a powerful way to compose
+existing terms into more complex ones\footnote{Although ADT's are a
+  type-theoretical concept, as we are concerned with the untyped version of the
+  Lambda Calculus, we will be only interested in how it allows us to build new
+  \textbf{terms}, not \textbf{types}. }. The composition can be made in two
+different ways:
+
+\paragraph{Product types}
+
+If we have some terms $T_1, T_2, ..., T_n$, we can produce a new term
+that is the ordered \textit{grouping} of them: $T = (T_1, T_2, ..., T_n)$. The
+resulting structure is often called an \textbf{n-tuple}.
+
+\paragraph{Sum types}
+
+If we have some terms $T_1, T_2, ..., T_n$, we can produce a new term that can
+be \textbf{disjoint union} of them:
+$T = C_1(T_1) \: | \: C_2(T_2) \: | \: ... \: | \: C_n(T_n)$. It consists of a
+series of \textbf{variants}, one for every previous term, each tagged by a
+unique \textbf{constructor} ($C_1-C_n$). A sum type will take the form of one
+(and only one) of the variants, and the constructor is used to in runtime to
+know which of the variants it actually is.
+
+
+
+As a special interesting case, it is often useful not to parameterize a variant
+(sum type) and just have the constructor as one of the values. This can be done
+naturally by parameterizing it over the empty product type $()$, also called
+\textbf{unit}.
+
+While the
 
 \subsubsection{Fixpoints}
 
 
+There's also the problem of recursion: as the lambda
+functions are anonymous, they can't simply refer to themselves. As with the
+church numerals, there are ways to \cite{PeytonJones87}
 
+---
+
+http://adam.chlipala.net/cpdt/html/Equality.html
+
+\begin{itemize}
+\item Alpha reduction
+\item Beta reduction
+\item ...
+\end{itemize}
 
 
 
@@ -651,6 +727,10 @@ http://adam.chlipala.net/cpdt/html/Equality.html
 
 
 
+\section{Normal forms}
+
+
+
 \section{Abstract Machines} %%
 
 (TODO: basic intro, motivation, function application implementations
@@ -683,16 +763,110 @@ http://adam.chlipala.net/cpdt/html/Equality.html
 
 \chapter{KRIVINE MACHINE} %%%%%%%%%%
 
-\cite{Krivine07}
-\cite{Douence07}
-
-
-
-\section{Not compiled} %%
+To begin our study of the implementation of abstract machines, we will start
+with the Krivine Machine. It is a relatively simple and well-known model that
+will help us see the steps that we need to take in order to implement a real
+abstract machine. We will be using the OCaml language from now on (not only in
+this section but also in the next ones).
 
+The Krivine Machine \cite{Krivine07} is an implementation of the weak-head
+call-by-name reduction strategy for pure lambda terms. What that means is that:
 
+\begin{itemize}
+\item The Krivine Machine reduces pure (untyped) terms in the Lambda Calculus
+\item The reduction strategy it implements is call-by-name, reducing first the
+  leftmost outermost term in the formula
+\item It stops reducing whenever the formula is in weak-head normal form, that
+  is:
+  \begin{itemize}
+  \item does not reduce abstractions: $(\lambda x . \mathcal{T})$
+  \item does not reduce applications of non-abstractions: $(x \: \mathcal{T})$
+  \end{itemize}
+\end{itemize}
 
-\section{Compiled} %%
+The first thing we need to have is an encoding of the language we will be
+reducing, in this case the Lambda Calculus. We will define a module,
+\textbf{Lambda}, containing the data structure and basic operations over it:
+
+\begin{code}
+  \begin{minted}[fontsize=\footnotesize]{ocaml}
+type symbol = string * int
+let show_symbol (s, _) = s
+
+module Lambda = struct
+    type t = Var of symbol | App of t * t | Abs of symbol * t
+    let rec show = match m with
+      | Var x -> show_symbol x
+      | App (m1, m2) -> "(" ^ show m1 ^ " " ^ show m2 ^ ")"
+      | Abs (x, m) -> "(λ" ^ show_symbol x ^ "." ^ show m ^ ")"
+end
+  \end{minted}  
+\end{code}
+
+(From now on, the auxiliar (e.g., pretty-printing) functions will be ommited for
+brevity.)
+
+Now we have a representation of the pure Lambda Calculus. As the Krivine Machine
+usually works with expressions in \textbf{de Bruijn} notation\footnote{ The de
+  Bruijn's notation gets rid of variable names by replacing them by the number
+  of ``lambdas'' between it and the lambda that is binding the variable. For
+  example, $(\lambda x . (\lambda y . (x \: y)))$ will be written in de Bruijn
+  notation as $(\lambda . (\lambda . (1 \: 0)))$}, we'll need to write an
+algorithm to do the conversion. To be sure we do not accidentally build terms
+mixing the two notatios, we'll create another module, \textbf{DBILambda}, with a
+different data type to represent them:
+
+\begin{code}
+  \begin{minted}[fontsize=\scriptsize]{ocaml}
+let rec find_idx_exn x = function
+  | [] -> raise Not_found
+  | (y::ys) -> if x = y then 0 else 1 + find_idx_exn x ys
+
+module DBILambda = struct
+    type dbi_symbol = int * symbol
+    type t = Var of dbi_symbol | App of t * t | Abs of symbol * t
+
+    let dbi dbis x = (find_idx_exn x dbis, x)
+
+    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)
+      in of_lambda []
+end
+  \end{minted}  
+\end{code}
+
+The new variables areThe function <<of_lambda>> accepts traditional lambda terms (Lambda.t) and
+returns its representation as a term using de Bruijn notation (DBILambda.t). Now
+we are ready to implement the actual reduction.
+
+The Krivine Machine has a state consisting on the code it is evaluating
+(\textbf{C}), an environmentThe typical description of the Krivine Machine \cite{Douence07} is given by the
+following set of rules:
+
+\begin{center}
+\line(1,0){250}
+\end{center}
+\begin{table}[H]
+\centering
+\begin{tabular}{lllll}
+$(M N, S, E)$ & \rightsquigarrow & $(M, (S,(N,E)), E)$ \\ \\
+$(\lambda M, (S,N), E)$ & \rightsquigarrow & $(M, S, (E,N))$ \\ \\
+$(i+1, S, (E,N))$ & \rightsquigarrow & $(i, S, E)$ \\ \\
+$(0, S, (E_1,(M,E_2)))$ & \rightsquigarrow & $(M, S, E_2)$
+\end{tabular}
+\end{table}
+\begin{center}
+\line(1,0){250}
+\end{center}
+
+\section{With power} %%
+
+
+
+%\section{Compiled} %%
 
 
 
@@ -757,10 +931,12 @@ http://adam.chlipala.net/cpdt/html/Equality.html
 
 \section{Krivine Machine source code} %%
 
+\inputminted[linenos=true,fontsize=\scriptsize]{ocaml}{code/krivine.ml}
 
-
+\newpage
 \section{ZAM source code} %%
 
+%\inputminted[linenos=true,fontsize=\scriptsize]{ocaml}{code/zam.ml}
 
 \pagebreak \bibliography{bib}{} \bibliographystyle{ieeetr}
 
diff --git a/to-copy.sh b/to-copy.sh
index 9c665bf..8352ac2 100755
--- a/to-copy.sh
+++ b/to-copy.sh
@@ -2,5 +2,5 @@
 
 COPY_D="${HOME}/Copy/univ/master/tfm"
 
-cp -r *.tex Makefile bib.bib ${COPY_D}/
+cp -r code *.tex Makefile bib.bib ${COPY_D}/
 cp -r front/*.tex ${COPY_D}/front/