double =
  fix (lambda f : Nat -> Nat. lambda n : Nat.
    if iszero n then
      0
    else
      succ (succ (f (pred n))));

/* Basic binary arithmetic */

ZPNat = Rec X. <uu : Unit, x0 : X, x1 : X>;

zpone = <uu = unit> as ZPNat;
zpx0 = lambda n : ZPNat. <x0 = n> as ZPNat;
zpx1 = lambda n : ZPNat. <x1 = n> as ZPNat;
zptwo = zpx0 zpone;
zpthree = zpx1 zpone;

natzp =
  fix (lambda f : ZPNat -> Nat. lambda n : ZPNat.
    case n of
      <uu = u>  ==>  1
    | <x0 = p>  ==>  double (f p)
    | <x1 = p>  ==>  succ (double (f p)));

zpsucc = fix (lambda f : ZPNat -> ZPNat. lambda n : ZPNat.
  case n of
    <uu = u>  ==>  zptwo
  | <x0 = m>  ==>  <x1 = m> as ZPNat
  | <x1 = m>  ==>  <x0 = f m> as ZPNat);

zpdm1 = fix (lambda f : ZPNat -> ZPNat. lambda n : ZPNat.
  case n of
    <uu = u>  ==>  <uu = unit> as ZPNat
  | <x0 = m>  ==>  <x1 = f m> as ZPNat
  | <x1 = m>  ==>  <x1 = zpx0 m> as ZPNat);

zppluscp =
  fix (lambda f : ZPNat -> {p : ZPNat -> ZPNat, c : ZPNat -> ZPNat}.
    lambda n : ZPNat.
      case n of
        <uu = u>   ==>  {p = lambda m : ZPNat.
                               case m of
                                 <x1 = mp>  ==>  <x0 = zpsucc mp> as ZPNat
                               | <x0 = mp>  ==>  <x1 = mp> as ZPNat
                               | <uu = u>   ==>  zptwo,
                         c = lambda m : ZPNat.
                               case m of
                                 <x1 = mp>  ==>  <x1 = zpsucc mp> as ZPNat
                               | <x0 = mp>  ==>  <x0 = zpsucc mp> as ZPNat
                               | <uu = u>   ==>  zpthree}
      | <x0 = np>  ==>  {p = lambda m : ZPNat.
                               case m of
                                 <x1 = mp>  ==>  <x1 = (f np).p mp> as ZPNat
                               | <x0 = mp>  ==>  <x0 = (f np).p mp> as ZPNat
                               | <uu = u>   ==>  <x1 = np> as ZPNat,
                         c = lambda m : ZPNat.
                               case m of
                                 <x1 = mp>  ==>  <x0 = (f np).c mp> as ZPNat
                               | <x0 = mp>  ==>  <x1 = (f np).p mp> as ZPNat
                               | <uu = u>   ==>  <x0 = zpsucc np> as ZPNat}
      | <x1 = np>  ==>  {p = lambda m : ZPNat.
                               case m of
                                 <x1 = mp>  ==>  <x0 = (f np).c mp> as ZPNat
                               | <x0 = mp>  ==>  <x1 = (f np).p mp> as ZPNat
                               | <uu = u>   ==>  <x0 = zpsucc np> as ZPNat,
                         c = lambda m : ZPNat.
                               case m of
                                 <x1 = mp>  ==>  <x1 = (f np).c mp> as ZPNat
                               | <x0 = mp>  ==>  <x0 = (f np).c mp> as ZPNat
                               | <uu = u>   ==>  <x1 = zpsucc np> as ZPNat});

zpplus = lambda n : ZPNat. (zppluscp n).p;

ZNat = <zz : Unit, pp : ZPNat>;

zzero = <zz = unit> as ZNat;
zone = <pp = zpone> as ZNat;
ztwo = <pp = zptwo> as ZNat;
zthree = <pp = zpthree> as ZNat;

ziszero =
  lambda n : ZNat.
    case n of
      <zz = u>  ==>  true
    | <pp = p>  ==>  false;

zsucc =
  lambda n : ZNat.
    case n of
      <zz = u>  ==>  zone
    | <pp = p>  ==>  <pp = zpsucc p> as ZNat;

znat =
  fix (lambda f : Nat -> ZNat. lambda n : Nat.
    if iszero n then
      zzero
    else
      zsucc (f (pred n)));

natz =
  lambda n : ZNat.
    case n of
      <zz = u>  ==>  0
    | <pp = p>  ==>  natzp p;

zplus =
  lambda n : ZNat. lambda m : ZNat.
  case n of
    <zz = u>   ==>  m
  | <pp = np>  ==>  (case m of
                       <zz = u>   ==>  n
                     | <pp = mp>  ==>  <pp = zpplus np mp> as ZNat);

ZInt = <zz : Unit, pp : ZPNat, nn : ZPNat>;

zix0 =
  lambda n : ZInt.
    case n of
      <zz = u>   ==>  <zz = unit> as ZInt
    | <pp = p>   ==>  <pp = <x0 = p> as ZPNat> as ZInt
    | <nn = p>   ==>  <nn = <x0 = p> as ZPNat> as ZInt;

zix1 =
  lambda n : ZInt.
    case n of
      <zz = u>   ==>  <pp = zpone> as ZInt
    | <pp = p>   ==>  <pp = <x1 = p> as ZPNat> as ZInt
    | <nn = p>   ==>  <nn = <x1 = p> as ZPNat> as ZInt;

zidm2 =
  lambda n : ZPNat.
    case n of
      <uu = u>  ==>  <zz = unit> as ZInt
    | <x0 = p>  ==>  <pp = <x0 = zpdm1 p> as ZPNat> as ZInt
    | <x1 = p>  ==>  <pp = <x0 = <x0 = p> as ZPNat> as ZPNat> as ZInt;

zpminuscp =
  fix (lambda f : ZPNat -> {m : ZPNat -> ZInt, c : ZPNat -> ZInt}.
    lambda n : ZPNat.
      case n of
        <uu = u>   ==>  {m = lambda m : ZPNat.
                               case m of
                                 <x1 = mp>  ==>  <nn = m> as ZInt
                               | <x0 = mp>  ==>  <nn = m> as ZInt
                               | <uu = u>   ==>  <zz = unit> as ZInt,
                         c = lambda m : ZPNat.
                               case m of
                                 <x1 = mp>  ==>  <nn = zpsucc m> as ZInt
                               | <x0 = mp>  ==>  <nn = zpsucc m> as ZInt
                               | <uu = u>   ==>  <nn = zpone> as ZInt}
      | <x0 = np>  ==>  {m = lambda m : ZPNat.
                               case m of
                                 <x1 = mp>  ==>  zix1 ((f np).c mp)
                               | <x0 = mp>  ==>  zix0 ((f np).m mp)
                               | <uu = u>   ==>  <pp = zpdm1 np> as ZInt,
                         c = lambda m : ZPNat.
                               case m of
                                 <x1 = mp>  ==>  zix0 ((f np).c mp)
                               | <x0 = mp>  ==>  zix1 ((f np).c mp)
                               | <uu = u>   ==>  zidm2 np}
      | <x1 = np>  ==>  {m = lambda m : ZPNat.
                               case m of
                                 <x1 = mp>  ==>  zix0 ((f np).m mp)
                               | <x0 = mp>  ==>  zix1 ((f np).m mp)
                               | <uu = u>   ==>  <pp = zpx0 np> as ZInt,
                         c = lambda m : ZPNat.
                               case m of
                                 <x1 = mp>  ==>  zix1 ((f np).c mp)
                               | <x0 = mp>  ==>  zix0 ((f np).m mp)
                               | <uu = u>   ==>  <pp = zpdm1 np> as ZInt});

zpminus = lambda n : ZPNat. (zpminuscp n).m;

zpmask = lambda n : ZNat.
  case n of
    <zz = u>  ==>  <zz = unit> as ZInt
  | <pp = p>  ==>  <pp = p> as ZInt;

znmask = lambda n : ZNat.
  case n of
    <zz = u>  ==>  <zz = unit> as ZInt
  | <pp = p>  ==>  <nn = p> as ZInt;

zminus = lambda n : ZNat. lambda m : ZNat.
  case n of
    <zz = u>   ==>  znmask m
  | <pp = np>  ==>  (case m of
                       <zz = u>   ==>  zpmask n
                     | <pp = mp>  ==>  zpminus np mp);

zdivides =
  lambda m : ZNat.
    fix (lambda f : ZNat -> Bool. lambda n : ZNat. 
      case zminus n m of
        <zz = u>  ==>  true
      | <pp = x>  ==>  f (<pp = x> as ZNat)
      | <nn = y>  ==>  ziszero n);

/* Lists */

NatList = Rec X. <nil : Unit, cons : {hd : Nat, tl : X}>;

nil = <nil = unit> as NatList;

cons =
  lambda h : Nat. lambda t : NatList.
    <cons = {hd = h, tl = t}> as NatList;

/* Streams */

ZNatStream = Rec X. Unit -> {hd : ZNat, tl : X};
ZNatStreamCell = {hd : ZNat, tl : ZNatStream};

/* Stream to list */

take =
  fix (lambda f : Nat -> ZNatStream -> NatList.
    lambda n : Nat. lambda s : ZNatStream.
      if iszero n then
        nil
      else
        let c = s unit in
        cons (natz c.hd) (f (pred n) c.tl));

/* Sieve of Eratosthenes */

nats =
  fix (lambda f : ZNat -> ZNatStream. lambda n : ZNat.
    lambda u : Unit. {hd = n, tl = f (zsucc n)});

filter =
  lambda p : ZNat.
    fix (lambda f : ZNatStream -> ZNatStream. lambda s : ZNatStream.
      lambda u : Unit.
        let c = s unit in
        if zdivides p c.hd then
          f c.tl unit
        else
          {hd = c.hd, tl = f c.tl});

sieve =
  fix (lambda f : ZNatStream -> ZNatStream. lambda s : ZNatStream.
    lambda u : Unit.
      let c = s unit in
      {hd = c.hd, tl = f (filter c.hd c.tl)});

primes = sieve (nats ztwo);

take 25 primes;
