Re: Named Views in CASL

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

Till wrote:

> >Nobody has provided me yet with examples of the definition and use of
> >NAMED VIEWS!  I'm almost finished with updating the Summary to v1.0,
> >apart from checking that the previous examples (with Till's suggested
> >modifications) still parse OK.  If I get the examples of named views by
> >sometime on Wednesday (EU time) I may still manage to include them...
> 
> O.K. Here are some examples.

Thanks!  Just in time...  

But my comments here concern the last-minute language design change
proposal that Till included between the examples: I'm afraid that it's
simply too late to make this change, since it would need discussion,
in my opinion.  (Bernd: do you agree?)  There is no time left for such
a discussion before v1.0 is released: I'm putting the final touches to
v1.0 now, and planning to release it as planned on 22 Oct.

> ...
> spec List_Of_List_Of_List_Of_Nat =
>         List[view List_as_Elem[view List_as_Elem[view Nat_as_Elem]]]
> end
> 
> I find this syntax quite wordy. What about
> 
> spec ListOfListOfListOfNat =
>         List[List_as_Elem[List_as_Elem[Nat_as_Elem]]]
> end
> 
> i.e. FIT-VIEW has the same concrete syntax as SPEC-INST,
> where the ambiguity between FIT-VIEW and SPEC-INST is resolved in such 
> a way that both are mapped to SPEC-INST by the parser, and the static
> semantic analysis has to map some SPEC-INSTs to FIT-VIEWs, depending
> on the global environment?

That sounds a bit complicated.  Moreover, I'm worried about the
methodological aspects: removing the "view" keyword above leaves no
clue as to whether a name refers to a SPEC that happens to fit OK
with an empty fitting map, or to a defined VIEW.  It might also hinder
any future extension or revision to allow implicit or default views.

> (This kind of processing appears to be necessary for UNIT-SPEC-NAMEs
> and SYMBs in SYMB-MAPs anyway.)

I've been trying to avoid forcing the static analysis to reconstruct
the abstract syntax:

- For (UNIT-)SPEC-NAME, UNIT-SPEC will now (again) have SPEC-NAME as
an alternative; the semantics has to interpret it as a (constant)
UNIT-TYPE in the case that it refers to an ordinary SPEC, otherwise as
a reference to a defined UNIT-SPEC, according to the global
environment.  I don't think that this requires the static analysis to
replace the SPEC-NAME by a UNIT-TYPE (although this is certainly a
possibility).  Moreover, it's fairly easy to explain what is happening
in the Summary. 

- Similarly, TYPE (used in QUAL-ID) will now have a simple SORT as an
alternative, and the semantics has to interpret it as a (constant)
OP-TYPE or as a (unary) PRED-TYPE (or reject it) depending on the
local environment.  When it isn't obvious from the symbol whether
the ID being qualified is a constant or a predicate, one can indicate
it by inserting the keyword "op" or "pred".

[I am a bit lost here; I hope this will not be a problem for the HO
extensions? (BKB)]

These are just my initial reactions, to explain why I think some
discussion of Till's proposal would be needed.

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

Computer Science Laboratory     mailto:mosses@csl.sri.com
SRI International               phone: +1 (650)  859-2200 ! CHANGED
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
_________________________________________________________