[Reposting again] Re: [Repost] Instantiating multiple theoriessimultaneously

[Michael Hohmuth <hohmuth@inf.tu-dresden.de>]

[ Again, a repost.  Maybe my original reply was lost again?  Maybe
  nobody read my message text after the quotation? ]


Dear Sam, thank you for your reply.

Sam Owre <owre@csl.sri.com> writes:
> It turns out it isn't a bug, this is part of why theory declarations were
> added to the language.  The right way to do what you want is to change the
> IMPORTING of A to a theory declaration, and map that at the same time you
> map b:
> 
>   A : THEORY
>   BEGIN
>     a : int
>   END A
>   
>   B : THEORY
>   BEGIN
>     Aimp: THEORY = A
>     b : int
>   
>     ab : AXIOM a = b
>   END B
>   
>   Aimplementation : THEORY
>   BEGIN
>     IMPORTING A{{a:=5}}
>   END Aimplementation
>   
>   Bimplementation : THEORY
>   BEGIN
>     IMPORTING B{{Aimp := A{{a:=5}}, b:=5}}
>   END Bimplementation
>
> Note that using IMPORTING B{{Aimp := Aimplementation, b:=5}}
> shoud not be allowed, because Aimplementation is not an instance
> of theory A.  [...]

I see.

The problem with your solution is that it seems like I cannot have an
importable version (with just a shorthand theory name like
"Aimplementation") of the instance of theory A.  Instead, I need to
provide the substitution in every place I wish to use the instance.
This is undesirable from a software-engineering point of view.

Possible solutions would be to allow theory instantiations at the top
level or, as a workaround, to allow 

  Aimplementation_container : THEORY
  BEGIN
    Aimplementation: THEORY = A{{a:=5}}
  END Aimplementation_container
  
  Bimplementation : THEORY
  BEGIN
    IMPORTING B{{Aimp := Aimplementation, b:=5}}
  END Bimplementation

which does not work, possibly because of bug 759
<http://pvs.csl.sri.com/cgi-bin/pvs/pvs-bug?id=759>.

Another (related) problem is that I cannot have chains of
(instantiable) theories, like this:

  A : THEORY
  BEGIN
    % stuff
  END A
  
  B : THEORY
  BEGIN
    Aimp: THEORY = A
    % more stuff
  END B
  
  C : THEORY
  BEGIN
    Bimp: THEORY = B
  END C

When I try this, I get the error message "Found '!id!' when expecting '='"
with the cursor pointing at some random location.  I also tried
    Bimp: THEORY = B{{Aimp := A}}
and various other things, but nothing worked.

Please help!

Kind regards,
Michael
-- 
hohmuth@sax.de, hohmuth@inf.tu-dresden.de
http://www.sax.de/~hohmuth/