Export Theory Operator WD conditions from Rodin

[leuschel]

Currently the .eventb export only contains the WD conditions of the body of an operator (at least for direct definitions). We should also export the user-defined WD conditions.

[leuschel]

This probably also holds for the ProB2 access to Rodin.

ProB1 for Rodin has this piece of code in Theories.java:

        Predicate wdCondition = opDef.getWDCondition(ff, te);
        printPredicate(prologOutput, wdCondition);

We should probably call INewOperatorDefinition.java : IOperatorWDCondition[] getOperatorWDConditions() throws RodinDBException; and convert this to a predicate (using the type environment?) and conjoin this with the current result.

[leuschel]

TheoryWDTest.zip Here is a small example where the WD condition for the operators are not visible in the exported .eventb file.

[leuschel]

package(load_event_b_project([],[event_b_context(none,'TestTheoryWD',[extends(none,[]),constants(none,[identifier(none,x)]),abstract_constants(none,[]),axioms(none,[member(rodinpos('TestTheoryWD',axm1,'_AcGdQFFVEe6_b6OkGjYNHg'),identifier(none,x),natural_set(none)),equal(rodinpos('TestTheoryWD',axm2,'_AcHrYFFVEe6_b6OkGjYNHg'),identifier(none,x),typeof(none,extended_expr(none,mu,[set_extension(none,[integer(none,1)])],[]),integer_set(none)))]),theorems(none,[equal(rodinpos('TestTheoryWD',thm1,'_AcHrYVFVEe6_b6OkGjYNHg'),identifier(none,x),integer(none,1)),equal(rodinpos('TestTheoryWD',thm2,'_6CIbwFFaEe6OgPVmDV3zSA'),typeof(none,extended_expr(none,assert_non_empty,[set_extension(none,[integer(none,1),integer(none,2),integer(none,3)])],[]),pow_subset(none,integer_set(none))),interval(none,integer(none,1),integer(none,3)))]),sets(none,[])])],[exporter_version(3),po('TestTheoryWD','Well-definedness of Axiom',[axiom(axm2)],true),po('TestTheoryWD','Theorem',[axiom(thm1)],false),po('TestTheoryWD','Well-definedness of Theorem',[axiom(thm2)],true),po('TestTheoryWD','Theorem',[axiom(thm2)],false),theory(theory_name('TheoryWDTest','SimpleWDTheory'),[],['T'],[],[
operator(mu,[argument(set,pow_subset(none,identifier(none,'T')))],conjunct(none,[member(none,boolean_true(none),domain(none,cartesian_product(none,set_extension(none,[boolean_true(none)]),identifier(none,set)))),member(none,cartesian_product(none,set_extension(none,[boolean_true(none)]),identifier(none,set)),partial_function(none,bool_set(none),identifier(none,'T')))]),[function(none,cartesian_product(none,set_extension(none,[boolean_true(none)]),identifier(none,set)),[boolean_true(none)])],[]),
operator(assert_non_empty,[argument(set,pow_subset(none,identifier(none,'T')))],truth(none),[identifier(none,set)],[])],[],[])],_Error)).