PROBPLUGIN Theory Support Bug for Parameters
Description
Environment
Attachments
Gliffy Diagrams
Activity

Jenkins Build Server February 4, 2014 at 5:55 PM
SUCCESS: Integrated in
ProB_Tests_Gradle #13
PROBPLUGIN-92: Added test cases (plagge: rev 1300)
/public_examples/EventBPrologPackages/Theory/RecOpTypeRefTest.zip
/public_examples/EventBPrologPackages/Theory/RecOpTypeTest.eventb

Jenkins Build Server January 31, 2014 at 1:17 PM
SUCCESS: Integrated in
ProB_Tests_Linux32 #933
PROBPLUGIN-92: Bugfix for recursive operators by introducing a LET similar to direct definitions (plagge: rev 1e9e68f01f1477dc6564767ad0224f5f6b937955)
src/bmachine_eventb.pl
PROBPLUGIN-92: Added test case for recursive operators (plagge: rev 37397539480ae078b256b06662080e35908e9035)src/testcases.pl
PROBPLUGIN-92: Added test cases (plagge: rev 1300)/public_examples/EventBPrologPackages/Theory/RecOpTypeRefTest.zip
/public_examples/EventBPrologPackages/Theory/RecOpTypeTest.eventb

Jenkins Build Server January 31, 2014 at 11:33 AM
SUCCESS: Integrated in
ProB_Tests_Linux64 #7764
PROBPLUGIN-92: Added test case for recursive operators (plagge: rev 37397539480ae078b256b06662080e35908e9035)
src/testcases.pl
PROBPLUGIN-92: Added test cases (plagge: rev 1300)/public_examples/EventBPrologPackages/Theory/RecOpTypeRefTest.zip
/public_examples/EventBPrologPackages/Theory/RecOpTypeTest.eventb

Jenkins Build Server January 31, 2014 at 11:01 AM
SUCCESS: Integrated in
ProB_Tests_Linux64 #7763
PROBPLUGIN-92: Bugfix for recursive operators by introducing a LET similar to direct definitions (plagge: rev 1e9e68f01f1477dc6564767ad0224f5f6b937955)
src/bmachine_eventb.pl

Daniel Plagge January 31, 2014 at 10:36 AM
Now recursive operators are fixed, too.
Details
Details
Assignee

Reporter

Hi,
I encountered what I think is a bug in ProB’s treatment of Theory parameters. I am using the nightly build.
Here is my Context. Note that I use two different Sequences, with different values for the type parameter T.
Here is the translated version. There seem to be two issues:
the parameter T is not typed
the same identifier T is used for both instances of the Sequence data type
When loading in Rodin or Tcl/Tk I get error message (T cannot be found; see below).