[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[CoFI] CASL v0.99 - rename/require
Dear all,
Translation
-----------
I am dissatisfied with the separation between rename/require. It would be
much better to have just one in which mappings of rename and lists of
require could be mixed, as with other constructs in CASL.
Peter confesses that the only (?) reason this was not done was the lack
of a good keyword covering both.
[A further minor reason was that the mixed lists of single symbols and
symbol maps may be confusing, until one gets used to "|->" having
higher precedence that ",". But we already have that with "reveal".
--PDM]
As a neutral terminology for both rename and require I propose "with" --
it is shorter and the renaming aspect comes in anyway with the special
symbol |-> .
[This proposal involves the following simplification to the abstract
syntax: replace
! RENAMING ::= RENAME | REQUIRE
! RENAME ::= rename SYMB-MAP-ITEMS+
! REQUIRE ::= require SYMB-ITEMS+
by
! RENAMING ::= renaming SYMB-OR-MAP-ITEMS+
and similarly in the concrete syntax, using "with" as the keyword.
Thus one may write e.g.:
NAT with Natural, zero |-> 0, suc |-> succ__, __+__
mixing single symbols and maps, exactly as allowed with "reveal".
I agree with Bernd that "with" - in contrast to "rename" - reads well,
whether or not symbols are merely mentioned or mapped. I don't see
any problems with adopting this proposal in the final v0.99 after
the Lisbon meetings. Comments are welcome! --PDM]
Best regards
Bernd