1
Vote

PM has problems with EXTENDS of submodules

description

Please consider a module with the following submodules:
------- MODULE inner ------

D(x) == x'

USE DEF D

====

------- MODULE outer -------
EXTENDS inner

LEMMA \A y : (D(y) = y') OBVIOUS 

\* LEMMA \A y : (D(y) = y') BY DEF D 

====
A call to the pm from the toolbox results in a warning about a prover problem(without backtrace). A commandline call results in:
Error: Could not prove or check:
         \A y : D(y) = y'
If I replace the OBVIOUS with BY DEF D, we obtain an error in obligation generation:
 File "errors.ml", line 75, characters 2-8: Assertion failed
Raised at file "errors.ml", line 75, characters 2-15
Called from file "m_gen.ml", line 49, characters 26-62
Called from file "m_gen.ml", line 79, characters 24-36
Called from file "m_gen.ml", line 93, characters 22-34
Called from file "m_gen.ml", line 96, characters 13-33
Called from file "m_gen.ml", line 81, characters 35-48
Called from file "m_gen.ml", line 84, characters 36-48
Called from file "m_gen.ml", line 96, characters 13-33
Called from file "m_elab.ml", line 650, characters 29-51
Called from file "tlapm.ml", line 181, characters 29-68
Called from file "tlapm.ml", line 320, characters 23-43
Called from file "list.ml", line 86, characters 24-34
Called from file "tlapm.ml", line 323, characters 13-40
Called from file "tlapm.ml", line 334, characters 8-33
which seems to be a problem in obligation extraction.

file attachments

comments