name matching/overloading de Bruijn weirdness in Cochon

[GoogleCodeExporter]

Following "The Art of the Possible" on the Epilogue I did this:

> data Nat := (zero : Nat) ; (suc : Nat -> Nat) ;

> let plus (m : Nat)(n : Nat) : Nat ;
> <= Nat.Ind m ;
> define plus 'zero n := n ;

Then instead of choosing a sensible name for the first arg I tried this:

> define plus ('suc xf^1) n := 'suc (plus xf^1 n)
I'm sorry, Dave. I'm afraid I can't do that.
Error: relabel: can't match xf^1 with xf^1

This works though:

> = 'suc (plus xf^1 n)
Ta.

And so does choosing a sensible name:

define plus ('suc m) n := 'suc (plus m n) ;

Original issue reported on code.google.com by jmchap...@gmail.com on 2 Sep 2010 at 10:13

[GoogleCodeExporter]

This is a bug in the relabelling code, which is generally broken and needs 
replacement once we figure out how it should really work. At the moment, it 
can't cope with relative or absolute names (those with ^n or _n suffixes).

Original comment by adamgundry on 3 Sep 2010 at 7:43

• Added labels: Priority-Medium, Type-Defect

[GoogleCodeExporter]

I've improved the relabelling code substantially (see issue 23, issue 77 and 
issue 101), but it still doesn't support de Bruijn indices in names because 
they don't really make sense given its current semantics (choose new names for 
all local hypotheses).

Is it okay to mark this issue WontFix, or is there a different semantics we 
should give to relabelling?

Original comment by adamgundry on 13 Sep 2010 at 11:55

• Added labels: Priority-Low
• Removed labels: Priority-Medium

[GoogleCodeExporter]

Is this another instance of that bug:

let case (D : Desc)(v : Mu D)(P : Mu D -> Set)(p : (x : desc D (Mu D)) -> P 
(con x)) : P v ;
<= induction D v ;
refine case D (con x) P p = p x ;

Giving:

I'm sorry, Dave. I'm afraid I can't do that.
Error: relabel: can't match con x with con x

Or it's a brand new bug?

(Writting the following does work:

let case (D : Desc)(v : Mu D)(P : Mu D -> Set)(p : (x : desc D (Mu D)) -> P 
(con x)) : P v ;
<= induction D v ;
= p x ;)

Original comment by pedag...@gmail.com on 20 Sep 2010 at 10:03

[GoogleCodeExporter]

This is an unrelated bug, which I've now fixed by making relabelling work for 
all canonical constructors using canTy. I am closing this issue; feel free to 
reopen it if you *really* want relative names to work on the LHS, or open 
another issue if you encounter other problems with relabelling.

http://www.e-pig.org/darcsweb?r=Pig09;a=commit;h=20100921142333-e29d1-5efb78bf5b
23a0b87d27b9175a7387a1a6e5ae94.gz

Original comment by adamgundry on 21 Sep 2010 at 2:30

• Changed state: WontFix