dédi' à pierre

main.ml

let () = Printexc.record_backtrace true

type ('l, 'r) either =
  | L of 'l
  | R of 'r

type ('a, 'b) cpl = T of 'a * 'b

module Eq =
struct
  type (_, _) refl = Refl : ('a, 'a) refl

  let symm
    : type m n. (m, n) refl -> (n, m) refl
    = fun Refl -> Refl

  let trans
    : type m n p. (m, n) refl -> (n, p) refl -> (m, p) refl
    = fun Refl Refl -> Refl

  module Lift (T : sig type 'a t end) =
  struct
    let lift
      : type a b. (a, b) refl -> (a T.t, b T.t) refl =
      fun Refl -> Refl
  end

  let cast
    : type a b. (a, b) refl -> a -> b
    = fun Refl x -> x

  let arrow
    : type a b c d. (a, b) refl -> (c, d) refl option -> (a -> c, b -> d) refl option
    = fun Refl -> function
      | Some Refl -> Some Refl
      | None -> None

  let cpl
    : type a b c d. (a, b) refl -> (c, d) refl option -> ((a, c) cpl, (b, d) cpl) refl option
    = fun Refl -> function
      | Some Refl -> Some Refl
      | None -> None

  let star
    : type a b c d. (a, b) refl -> (c, d) refl option -> (a * c, b * d) refl option
    = fun Refl -> function
      | Some Refl -> Some Refl
      | None -> None

  let either
    : type a b c d. (a, b) refl -> (c, d) refl option -> ((a, c) either, (b, d) either) refl option
    = fun Refl -> function
      | Some Refl -> Some Refl
      | None -> None
end

module A =
struct
  type var =
    | Z
    | S of var

  let rec int_of_var = function
    | Z -> 1
    | S n -> 1 + (int_of_var n)

  type typ =
    | Int
    | Bool
    | String
    | Lambda of typ * typ
    | Tuple of typ * typ

  let rec pp_typ ppf = function
    | Int -> Fmt.string ppf "int"
    | Bool -> Fmt.string ppf "bool"
    | String -> Fmt.string ppf "string"
    | Lambda (a, b) -> Fmt.pf ppf "(%a -> %a)" pp_typ a pp_typ b
    | Tuple (a, b) -> Fmt.pf ppf "(%a * %a)" pp_typ a pp_typ b

  type const =
    | Int of int
    | Bool of bool
    | String of string
  and binop =
    | Add | Sub | Mul | Div | Cpl | Eq
  and unop =
    | Fst | Snd | L of typ | R of typ
  and exp =
    | Con of const
    | Var of var
    | Abs of typ * exp
    | App of exp * exp
    | Bin of binop * exp * exp
    | Uno of unop * exp
    | Let of typ * exp * exp
    | Swt of { l : typ
             ; r : typ
             ; t : typ
             ; a : exp
             ; b : exp
             ; s : exp }
    | Rec of typ * typ * exp * exp
    | If  of exp * exp * exp

  let pp_const ppf = function
    | Int n -> Fmt.pf ppf "%d" n
    | Bool b -> Fmt.pf ppf "%b" b
    | String s -> Fmt.pf ppf "%s" s

  let rec pp ppf = function
    | Con c -> Fmt.pf ppf "%a" pp_const c
    | Var n -> Fmt.pf ppf "$%d" (int_of_var n)
    | Abs (t, e) ->
      Fmt.pf ppf "(\\%a %a)" pp_typ t pp e
    | App (f, a) ->
      Fmt.pf ppf "%a %a" pp f pp a
    | Bin (Add, a, b) ->
      Fmt.pf ppf "(%a + %a)" pp a pp b
    | Bin (Sub, a, b) ->
      Fmt.pf ppf "(%a - %a)" pp a pp b
    | Bin (Mul, a, b) ->
      Fmt.pf ppf "(%a * %a)" pp a pp b
    | Bin (Div, a, b) ->
      Fmt.pf ppf "(%a / %a)" pp a pp b
    | Bin (Eq, a, b) ->
      Fmt.pf ppf "(%a = %a)" pp a pp b
    | Bin (Cpl, a, b) ->
      Fmt.pf ppf "(%a, %a)" pp a pp b
    | Uno (Fst, a) ->
      Fmt.pf ppf "(fst %a)" pp a
    | Uno (Snd, a) ->
      Fmt.pf ppf "(snd %a)" pp a
    | Uno (L _, a) ->
      Fmt.pf ppf "(L %a)" pp a
    | Uno (R _, a) ->
      Fmt.pf ppf "(R %a)" pp a
    | Let (t, v, f) ->
      Fmt.pf ppf "let $1 : %a = %a in %a" pp_typ t pp v pp f
    | Swt { l; r; t; a; b; s } ->
      Fmt.pf ppf "(match %a with L $1 : %a -> %a | R $1 : %a -> %a)"
        pp s pp_typ l pp a pp_typ r pp b
    | Rec (t, u, z, s) ->
      Fmt.pf ppf "(\\%a fix z:%a s:%a)" pp_typ t pp z pp s
    | If (t, a, b) ->
      Fmt.pf ppf "(if %a then %a else %a)"
        pp t pp a pp b
end

module B =
struct
  type ('e, 'a) var =
    | Z : ('e * 'a, 'a) var
    | S : ('e, 'a) var -> ('e * 'b, 'a) var

  let rec int_of_var : type e a. (e, a) var -> int = function
    | Z -> 1
    | S n -> 1 + (int_of_var n)

  module V =
  struct
    let o = Z
    let x = ()

    let ( $ ) x () = S x

    (* let v = o$x$x$x$x$x = 5 (church style) *)
  end

  type 'a typ =
    | Int    : int typ
    | Bool   : bool typ
    | String : string typ
    | Lambda : 'a typ * 'b typ -> ('a -> 'b) typ
    | Tuple  : 'a typ * 'b typ -> (('a, 'b) cpl) typ
    | Either : 'a typ * 'b typ -> (('a, 'b) either) typ

  module Type =
  struct
    let int = Int
    let bool = Bool
    let string = String
    let lambda a b = Lambda (a, b)
    let tuple a b = Tuple (a, b)
    let either a b = Either (a, b)

    let ( > ) = lambda
    let ( * ) = tuple
    let ( or ) = either
  end

  type ('l, 'r, 'v) binop =
    | Add : (int, int, int) binop
    | Mul : (int, int, int) binop
    | Sub : (int, int, int) binop
    | Div : (int, int, int) binop
    | Cpl : ('a, 'b, ('a, 'b) cpl) binop
    | Eq  : ('a, 'a, bool) binop

  type ('u, 'v) unop =
    | Fst : (('a, 'b) cpl, 'a) unop
    | Snd : (('a, 'b) cpl, 'b) unop
    | L : ('a, ('a, 'b) either) unop
    | R : ('b, ('a, 'b) either) unop

  type ('e, 'a) exp =
    | Con : 'a -> ('e, 'a) exp
    | Uno : ('a, 'res) unop * ('e, 'a) exp -> ('e, 'res) exp
    | Bin : ('a, 'b, 'res) binop * ('e, 'a) exp * ('e, 'b) exp -> ('e, 'res) exp
    | Var : ('e, 'a) var -> ('e, 'a) exp
    | Abs : 'a typ * ('e * 'a, 'b) exp -> ('e, 'a -> 'b) exp
    | App : ('e, 'a -> 'b) exp * ('e, 'a) exp -> ('e, 'b) exp
    | Let : 'a typ * ('e, 'a -> 'b) exp * ('e, 'a) exp -> ('e, 'b) exp
    | Rec : { z : ('e, 'a) exp
            ; s : ('e * 'a, ('a, 'r) either) exp } -> ('e, 'r) exp
    | Swt : { s : ('e, ('l, 'r) either) exp
            ; a : ('e * 'l, 'l -> 'a) exp
            ; b : ('e * 'r, 'r -> 'a) exp } -> ('e, 'a) exp
    | If  : ('e, bool) exp * ('e, 'a) exp * ('e, 'a) exp -> ('e, 'a) exp

  type 'e env =
    | [] : unit env
    | (::) : 'a typ * 'e env -> ('e * 'a) env

  let rec get
    : type e a. (e, a) var -> e -> a
    = fun v e -> match v, e with
      | Z, (_, x) -> x
      | S n, (r, _) -> get n r

  let rec run
    : type e a. (e, a) exp -> e -> a
    = fun x e -> match x with
      | Con i -> i
      | Uno (L, x) -> L (run x e)
      | Uno (R, x) -> R (run x e)
      | Uno (Fst, x) -> let T (a, _) = run x e in a
      | Uno (Snd, x) -> let T (_, b) = run x e in b
      | Var x -> get x e
      | Abs (_, r) -> (fun v -> run r (e, v))
      | App (f, a) ->
        (run f e) (run a e)
      | Bin (Add, l, r) -> (run l e) + (run r e)
      | Bin (Sub, l, r) -> (run l e) - (run r e)
      | Bin (Mul, l, r) -> (run l e) * (run r e)
      | Bin (Div, l, r) -> (run l e) / (run r e)
      | Bin (Cpl, l, r) -> T (run l e, run r e)
      | Bin (Eq, l, r) -> (run l e) = (run r e)
      | Let (_, f, a) ->
        (run f e) (run a e)
      | Swt { s; a; b; } ->
        (match run s e with
         | L l -> (run a (e, l)) l
         | R r -> (run b (e, r)) r)
      | Rec { z; s; } ->
        let z' = run z e in
        let rec loop a = match run s (e, a) with
          | L a -> loop a
          | R r -> r
        in
        loop z'
      | If (t, a, b) ->
        (match run t e with
         | true -> run a e
         | false -> run b e)

  let int (x:int) = Con x
  let string (x:string) = Con x
  let tuple (a, b) = Bin (Cpl, a, b)
  let lambda t e = Abs (t, e)
  let apply f a = App (f, a)

  let fix ~z ~s = Rec { z; s; }
  let var x = Var x

  let ( = ) a b = Bin (Eq, a, b)
  let ( + ) a b = Bin (Add, a, b)
  let ( * ) a b = Bin (Mul, a, b)
  let ( - ) a b = Bin (Sub, a, b)

  let si t a b = If (t, a, b)

  let left e = Uno (L, e)
  let right e = Uno (R, e)
  let fst e = Uno (Fst, e)
  let snd e = Uno (Snd, e)
end

let option_bind
  : ('a -> 'b option) -> 'a option -> 'b option
  = fun f -> function Some x -> f x | None -> None

let ( >>= )

  : type a b c d.
       (a, b) Eq.refl option
    -> ((a, b) Eq.refl
    -> (c, d) Eq.refl option)
    -> (a -> c, b -> d) Eq.refl option

  = fun x f -> match x with
    | Some (Eq.Refl as x) -> Eq.arrow x (f x)
    | None -> None

let ( >&= )

  : type a b c d.
       (a, b) Eq.refl option
    -> ((a, b) Eq.refl
    -> (c, d) Eq.refl option)
    -> ((a, c) cpl, (b, d) cpl) Eq.refl option

  = fun x f -> match x with
    | Some (Eq.Refl as x) -> Eq.cpl x (f x)
    | None -> None

let ( >*= )

  : type a b c d.
       (a, b) Eq.refl option
    -> ((a, b) Eq.refl
    -> (c, d) Eq.refl option)
    -> (a * c, b * d) Eq.refl option

  = fun x f -> match x with
    | Some (Eq.Refl as x) -> Eq.star x (f x)
    | None -> None

let ( >?= )

  : type a b c d.
       (a, b) Eq.refl option
    -> ((a, b) Eq.refl
    -> (c, d) Eq.refl option)
    -> ((a, c) either, (b, d) either) Eq.refl option

  = fun x f -> match x with
    | Some (Eq.Refl as x) -> Eq.either x (f x)
    | None -> None

let rec eql_typ
  : type a b. a B.typ -> b B.typ -> (a, b) Eq.refl option
  = fun a b -> match a, b with
    | B.Int,            B.Int            -> Some Eq.Refl
    | B.Bool,           B.Bool           -> Some Eq.Refl
    | B.String,         B.String         -> Some Eq.Refl
    | B.Lambda (a, a'), B.Lambda (b, b') -> eql_typ a b >>= fun Eq.Refl -> eql_typ a' b'
    | B.Either (a, a'), B.Either (b, b') -> eql_typ a b >?= fun Eq.Refl -> eql_typ a' b'
    | B.Tuple  (a, a'), B.Tuple  (b, b') -> eql_typ a b >&= fun Eq.Refl -> eql_typ a' b'
    | _, _ -> None

let rec eql_env
  : type a b. a B.env -> b B.env -> (a, b) Eq.refl option
  = fun a b ->
    let open B in match a, b with
    | [], [] -> Some Eq.Refl
    | at :: a, bt :: b ->
      eql_env a b >*= fun Eq.Refl -> eql_typ at bt
    | _ -> None

type wtyp = Wtyp : 'a B.typ -> wtyp

let rec typ
  : A.typ -> wtyp
  = function
    | A.Int -> Wtyp B.Int
    | A.Bool -> Wtyp B.Bool
    | A.String -> Wtyp B.String
    | A.Lambda (a, b) ->
      let Wtyp a = typ a in
      let Wtyp b = typ b in
      Wtyp (B.Lambda (a, b))
    | A.Tuple (a, b) ->
      let Wtyp a = typ a in
      let Wtyp b = typ b in
      Wtyp (B.Tuple (a, b))

type wenv = Wenv : 'a B.env -> wenv

let rec env
  : A.typ list -> wenv
  = function
    | [] -> Wenv B.([])
    | x :: r ->
      let Wtyp x = typ x in
      let Wenv r = env r in
      Wenv B.(x :: r)

type wvar = Wvar : ('e, 'a) B.var * 'e B.env * 'a B.typ -> wvar

let rec var
  : A.var -> A.typ list -> wvar
  = fun v e -> match v, e with
    | A.S x, t :: r ->
      let Wvar (x', r', tr) = var x r in
      let Wtyp t' = typ t in

      Wvar (B.S x', B.(t' :: r'), tr)
    | A.Z, t :: r ->
      let Wtyp t = typ t in
      let Wenv r = env r in

      Wvar (B.Z, B.(t :: r), t)
    | _, _ -> assert false

type wexp = Wexp : ('e, 'a) B.exp * 'e B.env * 'a B.typ -> wexp

type error =
  | EnvMismatch of { g  : wenv
                   ; g' : wenv }
  | TypMismatch of { a  : wtyp
                   ; b  : wtyp }

exception Error of A.exp * A.typ list * error list

let rec exp
  : A.exp -> A.typ list -> wexp
  = fun e g ->
    match e with
    | A.Con (A.Int i) ->
      let Wenv g' = env g in
      Wexp (B.Con i, g', B.Int)
    | A.Con (A.Bool b) ->
      let Wenv g' = env g in
      Wexp (B.Con b, g', B.Bool)
    | A.Con (A.String s) ->
      let Wenv g' = env g in
      Wexp (B.Con s, g', B.String)
    | A.Uno (A.L tr, x) ->
      let Wenv g' = env g in
      let Wtyp tr' = typ tr in
      let Wexp (x', g'', tx') = exp x g in

      (match eql_env g' g'' with
       | Some Eq.Refl ->
         Wexp (B.Uno (B.L, x'), g', B.Either (tx', tr'))
       | _ ->
         raise (Error (e, g, [ EnvMismatch { g = Wenv g'; g' = Wenv g'' } ])))
    | A.Uno (A.R tl, x) ->
      let Wenv g' = env g in
      let Wtyp tl' = typ tl in
      let Wexp (x', g'', tx') = exp x g in

      (match eql_env g' g'' with
       | Some Eq.Refl ->
         Wexp (B.Uno (B.R, x'), g', B.Either (tl', tx'))
       | _ ->
         raise (Error (e, g, [ EnvMismatch { g = Wenv g'; g' = Wenv g'' } ])))
    | A.Uno (A.Fst, x) ->
      let Wenv g' = env g in
      (match exp x g with
       | Wexp (x', g'', B.Tuple (ta', tb')) ->
         (match eql_env g' g'' with
          | Some Eq.Refl ->
            Wexp (B.Uno (B.Fst, x'), g', ta')
          | _ ->
            raise (Error (e, g, [ EnvMismatch { g = Wenv g'; g' = Wenv g'' } ])))
       | _ -> assert false)
    | A.Uno (A.Snd, x) ->
      let Wenv g' = env g in
      (match exp x g with
       | Wexp (x', g'', B.Tuple (ta', tb')) ->
         (match eql_env g' g'' with
          | Some Eq.Refl ->
            Wexp (B.Uno (B.Snd, x'), g', tb')
          | _ ->
            raise (Error (e, g, [ EnvMismatch { g = Wenv g'; g' = Wenv g'' } ])))
       | _ -> assert false)
    | A.Bin (A.Cpl, a, b) ->
      let Wenv g' = env g in
      let Wexp (a', g'', ta') = exp a g in
      let Wexp (b', g''', tb') = exp b g in
      (match eql_env g' g'', eql_env g'' g''' with
       | Some (Eq.Refl as g1), Some (Eq.Refl as g2) ->
         (match Eq.trans g1 g2 with Eq.Refl -> Wexp (B.Bin (B.Cpl, a', b'), g', B.Tuple (ta', tb')))
       | _, _ ->
         raise (Error (e, g, [ EnvMismatch { g = Wenv g'; g' = Wenv g'' }
                             ; EnvMismatch { g = Wenv g''; g' = Wenv g''' } ])))
    | A.Var x ->
      let Wvar (x', g', t') = var x g in
      Wexp (B.Var x', g', t')
    | A.Abs (t, e) ->
      let Wtyp t' = typ t in
      let Wenv g' = env g in
      (let open B in match exp e (t :: g) with
        | Wexp (e', t'' :: g', tr) ->
          (match eql_typ t' t'' with
           | Some Eq.Refl -> Wexp (B.Abs (t', e'), g', B.Lambda (t', tr))
           | None -> raise (Error (e, g, [ TypMismatch { a = Wtyp t'; b = Wtyp t'' } ])))
        | Wexp (_, g'', _) -> raise (Error (e, g, [ EnvMismatch { g = Wenv B.(t' :: g''); g' = Wenv g'' } ])))
    | A.App (f, a) ->
      (match exp f g, exp a g with
       | Wexp (f', g', (B.Lambda (t', u'))),
         Wexp (a', g'', t'') ->
         (match eql_env g' g'', eql_typ t' t'' with
          | Some Eq.Refl, Some Eq.Refl ->
            Wexp (B.App (f', a'), g', u')
          | _, _ -> raise (Error (e, g, [ EnvMismatch { g = Wenv g'; g' = Wenv g'' }
                                        ; TypMismatch { a = Wtyp t'; b = Wtyp t'' } ])))
       | Wexp (_, _, t'), Wexp (_, _, a') ->
         (* XXX(dinosaure): [b] type could be wrong of what the user
            expect. *)
         raise (Error (e, g, [ TypMismatch { a = Wtyp t'; b = Wtyp (B.Lambda (a', t')) } ])))
    | A.Bin ((A.Add | A.Sub | A.Mul | A.Div) as binop, l, r) ->
      let binop = match binop with
        | A.Add -> B.Add
        | A.Sub -> B.Sub
        | A.Mul -> B.Mul
        | A.Div -> B.Div
        | _ -> assert false (* see pattern-matching (polymorphic variant?). *)
      in
      (match exp l g, exp r g with
       | Wexp (l', g', B.Int),
         Wexp (r', g'', B.Int) ->
         (match eql_env g' g'' with
          | Some Eq.Refl -> Wexp (B.Bin (binop, l', r'), g', B.Int)
          | None -> assert false)
       | _, _ -> assert false)
    | A.Let (t, a, b) ->
      (match typ t, exp a g, exp b g with
       | Wtyp t', Wexp (f', g', (B.Lambda (t'', u'))), Wexp (a', g'', t''') ->
         (match eql_typ t' t'' , eql_typ t'' t''', eql_env g' g'' with
          | Some (Eq.Refl as at), Some (Eq.Refl as bt), Some Eq.Refl ->
            (match Eq.trans at bt with Eq.Refl -> Wexp (B.Let (t''', f', a'), g', u'))
          | _, _, _ -> assert false)
       | _ -> assert false)
    | A.If (t, a, b) ->
      (match exp t g, exp a g, exp b g with
       | Wexp (t', g', B.Bool),
         Wexp (a', g'', u'),
         Wexp (b', g''', v') ->
         (match eql_typ u' v', eql_env g' g'', eql_env g'' g''' with
          | Some Eq.Refl, Some (Eq.Refl as ae), Some (Eq.Refl as be) ->
            (match Eq.trans ae be with Eq.Refl -> Wexp (B.If (t', a', b'), g', u'))
          | _ -> assert false)
       | _ -> assert false)
    | A.Bin (A.Eq, a, b) ->
      let Wexp (a', g', ta') = exp a g in
      let Wexp (b', g'', tb') = exp b g in
      (match eql_typ ta' tb', eql_env g' g'' with
       | Some Eq.Refl, Some Eq.Refl -> Wexp (B.Bin (B.Eq, a', b'), g', B.Bool)
       | _, _ -> assert false)
    | A.Swt { l; r; t; a; b; s; } ->
      let Wtyp t' = typ t in
      let Wtyp l' = typ l in
      let Wtyp r' = typ r in
      let Wenv g' = env g in
      let Wexp (s', g'', t'') = exp s g in

      (match eql_typ t'' (B.Either (l', r')) with
       | Some Eq.Refl ->
         (let open B in match exp a (l :: g), exp b (r :: g) with
           | Wexp (a', l'' :: ag'', B.Lambda (l''', ar)),
             Wexp (b', r'' :: bg'', B.Lambda (r''', br)) ->
             (match eql_typ l' l'', eql_typ r' r'',
                    eql_env ag'' g'', eql_env bg'' g'',
                    eql_typ l'' l''', eql_typ r'' r''',
                    eql_typ ar br with
             | Some (Eq.Refl as ta), Some (Eq.Refl as tb),
               Some Eq.Refl, Some Eq.Refl,
               Some (Eq.Refl as ta'), Some (Eq.Refl as tb'),
               Some Eq.Refl ->
               (match Eq.trans ta ta', Eq.trans tb tb' with
                | Eq.Refl, Eq.Refl -> Wexp (B.Swt { s = s'; a = a'; b = b'; }, g'', ar))
             | _ ->
               assert false)
           | _, _ -> assert false)
       | _ -> assert false)
    | A.Rec (t, u, z, s) ->
      let Wenv g' = env g in
      let Wtyp t' = typ t in
      let Wtyp u' = typ u in

      let gz = g in
      let gs = (u :: g) in

      let Wenv gz' = env gz in
      let Wenv gs' = env gs in
      let Wexp (z', gz'', tz') = exp z gz in
      let Wexp (s', gs'', ts') = exp s gs in

      (match eql_env g' gz',
             eql_env B.(tz' :: g') gs' with
      | Some (Eq.Refl as f1), Some (Eq.Refl as e1)->
        (match eql_typ tz' u',
               eql_typ ts' (B.Either (tz', tz')),
               eql_env gz' gz'',
               eql_env gs' gs'' with
        | Some Eq.Refl, Some Eq.Refl, Some (Eq.Refl as f2), Some (Eq.Refl as e2) ->
          (match Eq.trans f1 f2, Eq.trans e1 e2 with
           | Eq.Refl, Eq.Refl -> Wexp (B.Rec { z = z'; s = s'; }, g', u'))
        | _, _, _, _ -> assert false)
      | Some Eq.Refl, None -> assert false
      | None, Some Eq.Refl -> assert false
      | None, None -> assert false)

let run
  : type a. A.exp -> a B.typ -> a
  = fun m t ->
  let open B in match exp m [] with
  | Wexp (m', [], t') ->
    let v = B.run m' () in
    (match eql_typ t t' with Some Eq.Refl -> v | None -> raise (Error (m, [], [ TypMismatch { a = Wtyp t; b = Wtyp t' } ])))
  | Wexp (_, g', _) ->
    raise (Error (m, [], [ EnvMismatch { g = Wenv []; g' = Wenv g' } ]))

let () = assert (run (A.If (A.Con (A.Bool true), A.Con (A.Int 42), A.Con (A.Int 21))) B.Int = 42)

let switch_example =
  A.Swt
    { l = A.String
    ; r = A.Int
    ; t = A.String
    ; a = A.Abs (A.String, A.Var A.Z)
    ; b = A.Abs (A.Int, A.Con (A.String "<int>"))
    ; s = A.Uno (A.L A.Int, A.Con (A.String "Hello World!")) }

let k =
  A.App
    ((A.App
        ((A.Abs (A.Int,
                 A.Abs (A.Int, A.Var A.(S Z)))),
         (A.Con (A.Int 42)))),
     (A.Con (A.Int 21)))

let () = assert (run switch_example B.String = "Hello World!")
let () = assert (run k B.Int = 42)

let fix_example =
  let open B in

  fix
    ~z:(var V.o)
    ~s:(si (int 123 = var V.o)
           (left (var V.o + var V.o))
           (right (var V.o)))

let fact_example =
  let code =
    let rec fact ((k, x) as v) =
      if 0 = (snd v)
      then (fst v, 0)
      else fact ((fun x -> (fst v) x * (snd v)), (snd v) - 1)
    in
    let init x = ((fun x -> 1), x) in

    fun x -> (fst ((fun x -> fact (init x)) x)) 0
  in

  assert (code 5 = 120);

  let open B in

  let main =
    fix
      ~z:(tuple (lambda Type.int (int 1), var V.o))
      ~s:(si (int 0 = (snd (var V.o)))
            (right (tuple (fst (var V.o), int 0)))
            (left  (tuple (lambda Type.int ((apply (fst (var V.(o$x))) (var V.o)) * (snd (var V.(o$x)))),
                           ((snd (var V.o)) - int 1)))))
  in

  lambda Type.int (apply (fst (apply (lambda Type.int main) (var V.o))) (int 0))

let unsafe_fact =
  let open A in

  let t = Tuple (Lambda (Int, Int), Int) in
  let main =
    Rec (Int, t,
         Bin (Cpl, Abs (Int, Con (Int 1)), Var Z),
         If (Bin (Eq, Con (Int 0), Uno (Snd, Var Z)),
             Uno (R t, Bin (Cpl, Uno (Fst, Var Z), Con (Int 0))),
             Uno (L t, Bin (Cpl, Abs (Int, Bin (Mul, App (Uno (Fst, Var (S Z)), Var Z), (Uno (Snd, Var (S Z))))),
                                 Bin (Sub, (Uno (Snd, Var Z)), Con (Int 1))))))
  in

  Abs (Int, App (Uno (Fst, App (Abs (Int, main), Var Z)), Con (Int 0)))

let () = assert (run unsafe_fact B.Type.(int > int) 5 = B.run fact_example () 5)