Re: Revised List of Changes

[Peter Mosses <mosses@csl.sri.com>]

Till wrote:

> Dear friends,
> 
> here are my comments to the revised list of changes.

Thanks to Till for finding the time and energy to go through the
revised list!

> In the section and page numbers, I refer to the summary.
> 
> 2.1.4.1., p.15
> Remove the sentence
> "In a datatype declaration with more than one alternative,
> any selector that is declared as total for some alternative
> must be declared as total selector with the same result
> sort for every other alternative."
> This was decided in Amsterdam, since the Inka and KIV
> people use total selectors (partiality through underspecication).

In fact the citation is the rest of the sentence starting "Some minor
restrictions are imposed:", and was already destined to be replaced.

> 6.1.5, p.40
> after "in Part I)" insert
> "under some minor restrictions"
> (The minor restriction basically is the deleted sentence
> of 2.1.4.1. Perhaps one also could here insert the
> restriction of p.11 (top) of the revised list of changes).

So then it might read:

  Note that the specification written: 

        free types DD1; ... DDn; 

  is parsed as a free datatype of a basic specification--but it
  usually has the same interpretation as the free structured
  specification written:

        free { types DD1; ... DDn; }

  This equivalence holds at least in the framework for basic
  specifications given in Part I, under some minor restrictions: in a
  datatype declaration with more than one alternative, any selector that
  is declared as total for some alternative must be declared as a total
  selector with the same result sort for every other alternative; and
  the sorts and qualified operation symbols declared by the datatype
  declaration must not be already declared in the local environment.

> 6.2.2, p.43
> Replace "the set is a singleton" by "the signature morphism is defined".
> also in Sect. 6.3.1

OK

> 6.2.2, p.44, see p.14 of the revised list of changes:
> When completing the library of basic datatypes,
> Markus came up with an example where it seems to be useful
> to use the local environment within fitting arguments.
> 
> Consider a specification of finite maps as special sets of pairs.
> This would proceed like:
> 
> spec Pair [sorts elem1,elem2] = ...
> end
> 
> spec FiniteMap [sorts source,target] =
> ....
> then
>    FiniteSet[Pair [{} fit elem1 |-> source, elem2 |-> target]
>                  fit elem |-> pair]
> ...
> end
> 
> Thus I would propose not the change the summary here.
> Instead, I propose to allow to abbreviate the above as
>    FiniteSet[Pair [fit elem1 |-> source, elem2 |-> target]
>                  fit elem |-> pair]
> thus omitting the {}.

An objection to the above proposal might be that using `{}' (or
nothing at all) to stand for the entire local environment could be
confusing, especially for non-experts.

As far as I recall, Till's message was the first time that the above
proposal has been made on the cofi-language mailing list (although it
had previously been mentioned to me in private communication), and it
does involve a significant change to (at least) the concrete syntax,
so it may be advisable to leave it for further discussion and a future
version of CASL.

In any case, it seems that the example can be expressed even more
concisely by splitting the parameter specs:

  spec Pair [sort elem1] [sort elem2] =
    free type pair = ...

  spec FiniteMap [sort source] [sort target] =
  ....
  then
     FiniteSet [ Pair [sort source] [sort target]
                 fit elem |-> pair ]

- or is there some problem with that style of specification?

Of course, one would probably also want to use a compound id such as
pair[elem1,elem2]; then the last lines above become:

     FiniteSet [ Pair [sort source] [sort target]
                 fit elem |-> pair[source,target] ]
 
> C.2.2, p. C-5
> Replace
> 
> SOME-IMPORTS ::= given SPEC-NAME ,..., SPEC-NAME
> 
> by
> 
> SOME-IMPORTS ::= given GROUP-SPEC ,..., GROUP-SPEC

OK

> C.5.1, see p.24 of revised list of changes, last para:
> I propose to allow comments of form
> 
> %(  xxx   %)
> 
> where xxx can also be text consisting of several lines.
> This is extremely helpful when commenting out
> parts of specifications. In our practice in Bremen,
> we had to do this several times, and it is very tedious
> to insert a %% at each line.

The original design for the microsyntax of comments, as described in
the obsolete Syntax-Issues document [BCKB+98] and now to be
incorporated in the Summary, was to allow commenting-out by:

  %%<ignore> xxx </ignore>

where each line in xxx has to start with %% - the only effect of the
<ignore> </ignore> is to cause formatters to suppress the display of
the contents of the comment.  Having %% on each line was regarded as
useful for parsing both by programs and by human readers of the input
format.  It was also thought that with modern editors such as Emacs,
the insertion of %% at the beginning of each line in a selected region
was rather easy to do (and certainly would be supported by an Emacs
mode for editing CASL specifications); but maybe doing this with other
editors is indeed "very tedious", which would be a strong argument in
favour of the new proposal.

Since the deadline for discussion of the proposed changes to the
Summary is today, and probably very few readers care to address the
issue of syntax for comments at all, we may as well ask Bernd to
decide straight away about whether commenting-out should be allowed
using <ignore> xxx </ignore>, or %( xxx %), or both.  It will be easy
to change App. C accordingly.  Moreover, like all other details of
App. C, this design decision will still be subject to adjustment due
to any problems that arise in the implementation of parsers and
pretty-printers for CASL.

[BKB: I approve %( xxx %) to be supported by all tools (unless there
is a major objection) while we should decide about the ignore at some
later date as this is really a minor tools issue]

Cheers,

-- Peter
_________________________________________________________
Dr. Peter D. Mosses             International Fellow  (*)

Computer Science Laboratory     mailto:mosses@csl.sri.com
SRI International               phone: +1 (650)  859-2200
333 Ravenswood Avenue           fax:   +1 (650)  859-2844
Menlo Park, CA 94025, USA       http://www.brics.dk/~pdm/

(*) on leave from DAIMI & BRICS, University of Aarhus, DK
    also affiliated to CS Department, Stanford University
_________________________________________________________