Pig: memory allocation failed (and I didn't even try to do any category theory!)

[GoogleCodeExporter]

The below file (renaming for the well-scoped lambda terms) causes the above 
error. It's the last line that pushes it over the edge

data Nat := (zero : Nat) ; (suc : Nat -> Nat) ;
idata Fin : Nat -> Set := (zero : (n : Nat) -> Fin ('suc n)) ; (suc : (n : Nat) 
-> Fin n -> Fin ('suc n)) ;
let wk (m : Nat)(n : Nat)(f : Fin m -> Fin n)(i : Fin ('suc m)) : Fin ('suc n) ;
<= Fin.Ind ('suc m) i ;
define wk m n f ('zero m) := 'zero n ;
define wk m n f ('suc m i) := 'suc n (f i) ;
root ;
idata Lam : Nat -> Set := (var : (n : Nat) -> Fin n -> Lam n) ; (app : (n : 
Nat) -> Lam n -> Lam n -> Lam n) ; (lam : (n : Nat) -> Lam ('suc n) -> Lam n) ;
let ren (m : Nat)(n : Nat)(f : Fin m -> Fin n)(t : Lam m) : Lam n ;
<= Lam.Ind m t ;
define ren m n f ('var m i) := 'var n (f i) ;
define ren m n f ('app m t u) := 'app n (ren m n f t) (ren m n f u) ;
define ren m n f ('lam m t) := 'lam n (ren ('suc m) ('suc n) (wk m n f) t) ;

Original issue reported on code.google.com by jmchap...@gmail.com on 4 Sep 2010 at 8:36

[GoogleCodeExporter]

Original comment by jmchap...@gmail.com on 4 Sep 2010 at 8:36

[GoogleCodeExporter]

There is no less than 3 bugs causing this issue, so far:

http://code.google.com/p/epigram/issues/detail?id=81
http://code.google.com/p/epigram/issues/detail?id=82
http://code.google.com/p/epigram/issues/detail?id=83

Because it is such a wealthy source of bug, I'll wait for the others to be 
solved before signaling this one as "Duplicate".

Hell, you did a good job at spotting a rat nest!

Original comment by pedag...@gmail.com on 6 Sep 2010 at 12:01

[GoogleCodeExporter]

The equivalent Agda code for reference:

module Ren where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

data Fin : Nat -> Set where
  zero : (n : Nat) -> Fin (suc n)
  suc  : (n : Nat) -> Fin n -> Fin (suc n)

wk : (m : Nat)(n : Nat)(f : Fin m -> Fin n)(i : Fin (suc m)) -> Fin (suc n)
wk m n f (zero .m)  = zero n
wk m n f (suc .m i) = suc n (f i)

data Lam : Nat -> Set where
  var : (n : Nat) -> Fin n -> Lam n
  app : (n : Nat) -> Lam n -> Lam n -> Lam n
  lam : (n : Nat) -> Lam (suc n) -> Lam n

ren : (m : Nat)(n : Nat)(f : Fin m -> Fin n)(t : Lam m) -> Lam n
ren m n f (var .m i)   = var n (f i)
ren m n f (app .m t u) = app n (ren m n f t) (ren m n f u)
ren m n f (lam .m t)   = lam n (ren (suc m) (suc n) (wk m n f) t)

Original comment by jmchap...@gmail.com on 6 Sep 2010 at 5:40