Re: v0.97 local specifications

[Andrzej Tarlecki <tarlecki@mimuw.edu.pl>]

[A related message from Maura Cerioli is appended.  --PDM]

Dear All,

PDM> Andrzej has now proposed to allow also LOCAL-BASIC-ITEMS (App C of v0.95)
PDM> to permit the same sort of thing purely within a BASIC-SPEC, but I've
 (...)
PDM> if you still support the inclusion of LOCAL-BASIC-ITEMS, please say why

Well, I am not quite sure which of my message Peter meant exactly, but
the fragment on locals I found was in my "comments on v.0.96" (Wed,
7 May 1997 18:27:31):

AT> And a related issue: once linear visibility would be restored then
AT> perhaps we could go back to the idea of local declarations (SIG-DECLs)
AT> within basic specs only, rather than locality introduced only at the
AT> level of structured specs?

[Right, that was the one I was referring to.  --PDM]

I think this still holds: I would like linear visibility and local
basic items then (even more to my personal taste would be local
definitions in terms and/or formulae). Without linear visibility,
local decls cause some difficulties, as Don presented.

If non-linear visibility within lists of basic items is there to stay,
then tough...

PDM> - otherwise I'll prepare a minimal Note of Dissent proposing their
PDM> removal.

No protests from me...

Best,

Andrzej
_______________________________________________________________________

  From: cerioli@disi.unige.it (Maura Cerioli)
  Subject: local stuff

Dear all,
this is a sort of follow-up of HB's message (+DS+AT+PDM+myself...+...)
I'm not sure that the part of my message Peter is quoting shows my ideas on
the matter, so I prefer to restate the things from the beginning.

1 *IF*, as in the current version, we have that SPEC is essentially the
  same as BASIC-ITEM*, that is SPEC represents specification fragments,
  then I agree with all the others that the two constructs are redundant
  and that we will be happy with just the one that is causing less problems
  for the semantics.
2 *IF*, as I hope now and as I was convinced we already did in Paris when I
  wrote the message, we will decide to change the language design to have
  that SPEC are self-contained specifications, then, at that moment, we will
  need, or, better, it would be more convenient to have both constructs.

[Watch this space for the announcement of CoFI Language Design Note-of-
Dissent L-3, which gives more details of Maura's hopes on this point ...  
--PDM]

  But in that case, we can also think about having a restricted form of
  local stuff. Indeed, I can easily think of examples where is convenient
  to have signature symbols and axioms local to *axioms*, but I don't have
  an example in mind where it is convenient to have something local to
  a sort declaration, for instance. I have no idea if such restrictions
  could help in defining the semantics, however.
  I have a slight intuition that such a restriction could help in
  "linearizing" a BASIC-ITEM*, first expanding the "derived" constructs,
  like data-type and subsort definitions and such, then extracting all
  the declarations of sorts, function and predicates (whose correctness
  can be decided, because the sorts are all known) to build the environment
  and then process the (iso-decl, susort-decl and) axioms...but I didn't
  think sufficiently on the matter, it's just an intuition.

Best regards
Maura

[Thanks for the prompt responses.  --PDM]