Glad to hear the explanation helped! As for the highlighting, I did that after I wrote up the email. I like to reread things I write make sure they are sensible. I found it a bit difficult to parse in plain back text so I went through and added a bit a color to emphasize the different parts.
-Rich Robbert van Dalen wrote: > Rich, > > That’s a great write-up, it really all makes sense now! > I learned a great deal more about avail’s grammatical restrictions and parse > rejections. > > I also really like the way you use syntax highlighting. > Do you use a tool for that .. or have you done this manually? > > cheers, > Robbert. > > >> On 24 Feb 2015, at 05:59, Richard Arriaga <[email protected]> wrote: >> >> Robbert, >> The second one failed to compile due to a lack of a grammatical >> restriction. There are two primitives defined for n-ary tuple replacement: >> • "_[_]→_" >> • "_«[_]»→_" >> The first one represents a simple tuple. The second is the definition for a >> tuple path that takes two or more indices (nested at least 2 levels deep). >> In the module Foundation.avail/Late Restrictions.avail, there is a >> grammatical restriction for "_«[_]»→_" that prevents "_[_]" from being in >> the first argument. I had neglected to introduce that same grammatical >> restriction for "_[_]→_" , thus making ( t[1] ) [3] → 7 a valid statement. >> That of course collides with the intended parsing using the method, >> "_«[_]»→_". By introducing the grammatical restriction forbidding "_[_]" >> as the first argument for "_[_]→_" , I have removed the ambiguity. >> >> Though I'm sure you could puzzle that bit out. As to why the first one >> parsed and the second one didn't is simply magic...or at least that was my >> first conjecture as everything I knew about Avail up until now told me that >> shouldn't be the case. The *actual* reason for the first method parsing and >> not the second lies in the semantic restriction of the method "Require:_=_" . >> >> Semantic restriction "Require:_=_" is >> [ >> actual : any's type, >> expected : any's type >> | >> If actual ∩ expected = ⊥ then >> [ >> Reject parse, expected: >> format "a predicate that could ever be true (because \ >> \|(“①”) doesn't intersect (“②”)." >> with actual, expected >> ]; >> ⊤ >> ]; >> >> The result of the parsed statement >> 1) ( t[1] ) [3] → 7 is the tuple <1,2,7>. >> >> The result of the parsed statement >> 2) t[1][3] → 7 is the nested tuple <<1,2,7>,<14,5,6>>. >> >> The "Require:_=_" statement in your method requires the result of n to be >> equal to the tuple, <<1,2,7>,<14,5,6>>. If you push both resulting tuples >> through the semantic restriction for "Require:_=_", this is what you get: >> >> 1) <1,2,7>'s type ∩ <<1,2,7>,<14,5,6>>'s type = ⊥ >> By the semantic restriction this parsing is always rejected as the result of >> the type intersection is bottom. The parse is rejected by the primitive, >> "Reject parse,expected:_". (the primitive is in >> Foundation.avail/Bootstrap.avail/Fallible Primitives.avail) >> >> 2) <<1,2,7>,<14,5,6>>'s type ∩ <<1,2,7>,<14,5,6>>'s type ≠ ⊥ >> In this case, the semantic restriction does not reject the parse, making >> this parse the only valid remaining parsing. >> >> "Reject parse,expected:_" rejects a parse and throws an error only if there >> are no remaining parses syntactically accepted by the compiler. If there >> still remain parses syntactically accepted by the compiler, then no error is >> thrown. As the semantic restriction for "Require:_=_" called "Reject >> parse,expected:_" on ( t[1] ) [3] → 7 but not on t[1][3] → 7, it allowed for >> only one remaining viable parsing. Thus the semantic restriction for >> "Require:_=_" disambiguated the parsing of t[1][3] → 7. >> >> -Rich >> >> >> Robbert van Dalen wrote: >>> Method "testpath" is [ >>> t : <<natural number…|3>…|> := <<1,2,3>,<4,5,6>>; >>> n ::= t[1][3] → 7; >>> Require: <<1,2,7>,<4,5,6>> = n; >>> {n,t} >>> ]; >>> >>> {<<1, 2, 7>, <4, 5, 6>>, <<1, 2, 3>, <4, 5, 6>>} >>> >>> But without the Require, it doesn’t compile?? >>> >>> Method "testpath" is [ >>> t : <<natural number…|3>…|> := <<1,2,3>,<4,5,6>>; >>> n ::= t[1][3] → 7; >>> {n,t} >>> ]; >
