[ a b , c d e ] parses as [ a (b , c d e)] (instead of [ (a b), (c d e) ])

[GoogleCodeExporter]

I'm writting the following function:

let replace (D : Desc)(X : Set)(Y : Set)(xs : desc D X)
            (hs : box D X (\ _ -> Y) xs) : desc D Y ;
<= induction DescD D ;
refine replace 'idD X Y xs hs = hs ;
refine replace ('constD K) X Y k [] = k ;
refine replace ('sumD E T) X Y [c , d] dd = [ c , replace (T c) X Y d dd ] ;

In the prodD case, I would like to write:

refine replace ('prodD u C D) X Y [c , d] [cc , dd] = [ replace C X Y c cc , 
replace D X Y d dd ];

But I get:

[ProofTrace] Failed to resolve recursive call to replace^1 D X Y xs hs

Leading to the following two, rather surprising, hopes:

Programming: < replace^1 D X Y xs hs : desc D Y >
Goal: :- ((: Set) ((D : Desc)(X : Set)(Y : Set)(xs : desc D X)(hs : box D X (\ 
_ -> Y) xs) -> desc D Y)) == (desc C^1 Y^1)

Strangely enough, I can proceed manually:

refine replace ('prodD u C D) X Y [c , d] [cc , dd] = [ ? , ? ]; 
= (replace C^1 X^1 Y^1 x xh) call;
= (replace D^1 X^1 Y^1 xs hs) call;

Original issue reported on code.google.com by pedag...@gmail.com on 20 Sep 2010 at 11:03

[GoogleCodeExporter]

This a quirk of the syntax, made confusing by the elaborator's ability to make 
sense of anything by inserting enough coercions. I've made this mistake far too 
many times. Recall that [a b] means the nested list of pairs a:b:nil, whereas 
[(a b)] means the list of one element (a applied to b). You need to write

refine replace ('prodD u C D) X Y [c , d] [cc , dd] = [ (replace C X Y c cc) , 
(replace D X Y d dd) ];

but perhaps we should think about changing the syntax.

Original comment by adamgundry on 21 Sep 2010 at 7:35

[GoogleCodeExporter]

After a quick chat, we came to the conclusion that:

In a later incarnation of a parser, we would give a higher precedence to comma, 
hence the term [ a b c , d e f ] will be parsed as [ (a b c) , (d e f) ].

For the time being, nobody feels like playing with the bowels of the parser (it 
smells like haggis, tastes like chicken), so we let this bug open.

Original comment by pedag...@gmail.com on 21 Sep 2010 at 8:38

• Changed title: [ a b , c d e ] parses as [ a (b , c d e)](instead of [ %28a b%29, %28c d e%29 ])