[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: CASL v.1.0: UNIT-SPEC-NAMEs
two messages: from Frederic and from Andrzej (appended) [BKB]
[Note:
> > = Andrzej
> = Peter
]
> > Due to the context-free parsing considerations (I understand), the
> > following clause has disappeared:
> > UNIT-SPEC ::= UNIT-SPEC-NAME
...
> I'm inclined to go with:
>
> > 3. Restore UNIT-SPEC ::= SPEC-NAME
>
> in the abstract syntax - but not in the concrete syntax!
>
> > and and resolve the ambiguity by
> > giving the priority to the parsing
> > SIMPLE-ID qua SPEC-NAME qua UNIT-SPEC
> > over
> > (unit-type () (SIMPLE-ID qua SPEC-NAME qua SPEC))
> > qua UNIT-TYPE qua UNIT-SPEC
> > (This is perhaps standard enough...)
>
> All that is needed, I think, is to indicate which abstract syntax tree
> the parsers should produce, without changing the concrete grammar from
> v1.0-DRAFT.
>
> > Then the semantics will cope correctly with two cases: SPEC-NAME being
> > a SIMPLE-ID bound in the global environment to a UNIT-SPEC, as well as
> > SPEC-NAME being a SIMPLE-ID bound in the global environment to a SPEC.
Yes, maybe I wasn't clear enough. The problem is purely syntactic.
Context-freely we cannot distinguish between the two possibilities,
hence
in the concrete syntax, simply write it is a name. Later, when producing
the abstract syntax tree, check which can of spec that name corresponds
to.
Frederic
------------------------------- message from Andrzej
--------------------
From: Andrzej Tarlecki <tarlecki@mimuw.edu.pl>
Subject: Re: CASL v.1.0: UNIT-SPEC-NAMEs
Dear Peter,
Thanks for the extra time...
On the issue of named unit specifications, it seems that we have
converged on:
PDM> I'm inclined to go with:
AT> 3. Restore UNIT-SPEC ::= SPEC-NAME
PDM> in the abstract syntax - but not in the concrete syntax!
I guess i can swallow this, as long as the parser will return what we
decide below to the abstract syntax level (hence, for the semantics).
AT> and and resolve the ambiguity by
AT> giving the priority to the parsing
AT> SIMPLE-ID qua SPEC-NAME qua UNIT-SPEC
AT> over
AT> (unit-type () (SIMPLE-ID qua SPEC-NAME qua SPEC))
AT> qua UNIT-TYPE qua UNIT-SPEC
AT> (This is perhaps standard enough...)
PDM> All that is needed, I think, is to indicate which abstract syntax
tree
PDM> the parsers should produce, without changing the concrete grammar
from
PDM> v1.0-DRAFT.
AT> Then the semantics will cope correctly with two cases: SPEC-NAME
being
AT> a SIMPLE-ID bound in the global environment to a UNIT-SPEC, as well
as
AT> SPEC-NAME being a SIMPLE-ID bound in the global environment to a
SPEC.
PDM> Right. (We'll need to do something similar regarding the ambiguity
PDM> that I failed to fix in symbol maps, reported by Till earlier on
PDM> Oct 15.)
Once around this topic, i have noticed that no way was introduced in
the concrete syntax for expressing explicit closure of unit types.
I think we all presume that this will be typically achieved by naming
the corresponding unit type in a unit spec definition --- but still,
in the analogous situation for closed (structured) specs, an explicit
operator was provided in the syntax as well. Would this be the only
situation in the language that something that is available in the
abstract syntax cannot be expressed in the concrete syntax? Perhaps
not...
Anyway, I propose to proceed here by analogy with the CLOSED-SPEC, and
allow for a fourth clause for UNIT-SPEC in C.2.3:
UNIT-SPEC ::= closed {GROUP-SPEC * ... * GROUP-SPEC ->
GROUP-SPEC}
This "closure" requires perhaps some more comments in the summary. I
propose to move the clause
CLOSED-UNIT-TYPE ::= closed UNIT-TYPE
from sect. 8.2 to 8.2.1, and add there something like the following
comment (at the end of 8.2.1?):
A unit type may be used as a unit specification in a unit
declaration where unit imports are provided. Then the argument
specifications (and hence the result specification as well) of
the unit type are treated as extensions of the imports. This
dependency is removed when a unit type is closed, either
implicitly in a unit specification definition, or
explicitly, when a closed unit type is written as:
closed { SP_1 * ... * SP_n -> SP}
All my other comments are minor (not that some of the above was
tremendously important...). I'll try to avoid repeating what others
wrote, but I will probably fail...
1. p.xii, l.+6: clsoe -> close
2. p.3/4, sect. 1.1:
Just checking: I understand that the final outcome of the discussion
on overloading between partial and total functions was to stay with
the original restriction that partial and total functions with the same
name cannot have the same profile, right?
If not, then the recent change to allow for this, with the intended
meaning that the operation then has to be total, calls for some
further changes here, to constrain the signature morphisms so that the
total and partial functions with the same profiles are mapped in the
same way. Otherwise the model reducts need not be defined...
3. p.7, l.-11.
"Basic specification *of* the underlying institution" sounds to me a
bit as if we were specifying the institution here.
What about: "Basic specification within the underlying institution..."?
4. p.9, the very end of sect. 2.1.1:
add a space between \textbf{sorts} and s_1 (twice).
5. p.10, l.-14:
...the type is simply written "? s"
(lower case s)
6. p.11, l.+2:
I find this comment rather criptic now: what exactly is t w.r.t. the
operation name (named f earlier)? I guess what is meant is that assoc
for an operation with the name like __t__ introduces the possiblity of
using the associative notation in terms. Would this be clear form the
etxt as it is now?
7. p.11/12, sect. 2.1.2.2:
In operation definitions, is the definitional term allowed to contain
occurrences of variables other than formal parameters?
If not (as I think I would prefer) then this should be mentioned.
If yes, then perhaps it is worth hinting that in the final expansion
this other variables will get universally quantified as well (over
variabled that are there and of course muist have been declared).
Similarly for the definitional formula in predicate definitions
(p.13, sect. 2.1.3.2).
8. p.18, sect.2.3.1, l.-5:
forall V_1,...,V_n:s.F
(colon is missing, i believe).
9. p. 22/23. sect. 2.3.4.1:
Just checking: so, we can have constants and variables with the same
names (even over the same sorts), right? And if both have been
declared then they must be used with qualification? And if another
variable is (locally) declared with the same name and a different
sort, then the variable is hidden, while the constant becomes visible
and usable without qualification (if the sort can be determined)?
Okay...
Aha: I found the abstract syntax a bit strange here. Implicitly, i
presume that SIMPLE-ID qua TERM will be used to parse a constant
without qualification, while the use of a constant with
qualification will have to be parsed as:
(application
(qual-op-name (SIMPLE-IS qua OP-NAME) OP-TYPE) qua
OP-SYMB
terms () ) qua TERM
At least, it should be mentioned that references to constants can also
be qualified (and the empty list of arguments may be omitted then)
when the syntax for qualified op names is introduced (sect.2.3.4.3,
p.23).
10. p.36, the last item.
I wish I was quite sure what the outcome of the discussions around
this topic really was. Has Till provided the final formulation here?
I guess the least that has to be modified here is that the
parenthetical comment must be give a higher priority than the default
identity mapping...
Something like the following perhaps:
...all morphisms from Sigma to Sigma' that extend the given mapping
and are identity on common symbols of Sigma and Sigma' unless this is
in conflict with the given mapping (mapping an operation or predicate
symbol implies mapping the sorts in their profile consistently).
11. p.43, sect. 6.2.1, l.+15:
What exactly is meant here by the "defined specification"? SP? or
instantiations of SN? Or something yet different, which does not occur
here explicitly, but is mentioned only later in the explanation of
the semantics:
{SP"_1 and ...} then {SP_1 and ...} then SP
The last case would be most accurate, i guess. So maybe this comment
should be moved until after this specification was formed here?
12. p.44, l.+17:
A comment here that when SM_i is empty, just SP'_i is written?
13. p.45, definition of FM
Perhaps add in parenthesis some hint that this is explained in more
detail in sect. 6.5?
14. p.45, sect.6.2, the last para:
I did not notice any hint on what models of FA_i might be, so perhaps
a comment in parenthesis:
(these are models of SP'_i reduced by the signature morphism
determined by SM_i)
Then, in the last sentence, it is not so clear the pushout of what and
where is considered. I guess i would add:
...whenever the result signature is not a pushout of the body
and argument signatures.
??
15. p.46, sect.6.3.2.
Now that there are no implicit views, we could be more relaxed about
the exact relationship between the signature of the formal parameter
and the source signature of the view used to instantiate it. A very
open possibility would be to allow here a symbol mapo that would fit
the parameter signature into the source signature of the view. Without
changing the syntax, we could allow here any situation that the empty
symbol map determines a unique signature morphism between them. This
would allow for instance for inclusion of the parameter signature into
the source of the view.
Okay: this was not serious; I do not want to re-start this discussion
again... No suggestion on this from me...
16. p.47/48
Adding to your discussion with Till around here, just a
comment/question: when you wrote about what happens with
SY_i |-> SY'_i in a list with implicit SYMB-KIND, when SY_i is not
qualified, you say that it applies to all operation or predicate
symbols with the same name. I guess this should apply also to sort
symbols with this name, right?
17. p.49, the innocuous sentence "similarly for translation and
reduction."
I guess Michel reported the story as i remember it as well; without
recalling the details, I also recall the conclusion that there
"compositional" extension of symbol maps to compound identifiers takes
place only when the symbol map is used as a fitting morphism.
But i do not think I feel very strongly about this conclusion.
18. p.53, ch.8, l.+3:
How "tentative" the syntax for arch specs is still going to be after
v.1.0 is announced? Do we want to remove this comment?
19. p.55/56: for discussion of closed unit types and unit-spec-names:
see above.
20. p.59: comments on FAU_i
I think it would be more consistent to use a similar syntax as for
argument fittings in instantiations of generic specs.
In particular, write FAU_i as
UT'_i fit SM_i
(why double prime is used now?)
and refer to sect. 6.4 and 6.5 for the interpretation of SM_i.
Finally, I guess we have forgotten to add here any comments that the
argument should fall into the domain of the generic unit. Perhaps, at
the very end:
It is also checked (and the appropriate verification
condition is generated) that the arguments provided do indeed
satisfy the corresponding argument specifications in the unit
specification given for UN.
==============================================================================
This seems to be all...
Are we really that close to finishing up? Thanks, Peter!
Best,
Andrzej