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} >> ];
signature.asc
Description: Message signed with OpenPGP using GPGMail
