[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] EXPORTING clauses and DATATYPE theories



When I try to typecheck stream_comonad.pvs (see below), I get this
perplexing error:

  "stream_185 occurs in an EXPORTING WITH but is not in a IMPORTING clause"

If I change the EXPORTING clause to use stream_185_adt (and leave the
IMPORTING clause as is), it works fine. I'm generating these
specifications -- it's possible to recognize when a theory name is a
DATATYPE, but I'd rather avoid the bookkeeping if I can.

Have I correctly identified the cause of this error message? IMPORTING
and EXPORTING clauses in the grammar both use TheoryNames, and
IMPORTING clauses don't seem to choke on DATATYPEs in this way.

Thanks for your time,
Nick

=== stream_comonad.pvs ===
stream_comonad : THEORY
EXPORTING ALL WITH stream_185, counit_298, cobind_392, coextend_457,
left_unit_507, right_unit_534, assoc_628 BEGIN
IMPORTING stream_185, counit_298, cobind_392, coextend_457,
left_unit_507, right_unit_534, assoc_628
END stream_comonad

=== stream_185.pvs ===
stream_185[A_176 : TYPE] : DATATYPE BEGIN
scons_226(lookahead_672 : [[nat] -> A_176]) : is_scons_265
END stream_185