Commit f392484e authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Add support for enumerated types into the parser and collection. 

VariableParser now deals with enumerated types correctly, and VariableCollection
exposes the enumerated types as appropriately so that further parsing/generating
will work correctly.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@11087 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent e574db0d

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/EnumerationVariableType.java

0 → 100644
+45 −0
Original line number Diff line number Diff line 
/*

 * Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>

 *

 * This program is free software: you can redistribute it and/or modify

 * it under the terms of the GNU General Public License as published by

 * the Free Software Foundation, either version 3 of the License, or

 * (at your option) any later version.

 *

 * This program is distributed in the hope that it will be useful,

 * but WITHOUT ANY WARRANTY; without even the implied warranty of

 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the

 * GNU General Public License for more details.

 *

 * You should have received a copy of the GNU General Public License

 * along with this program.  If not, see <http://www.gnu.org/licenses/>.

 */

package ca.mcmaster.cas.tabularexpressiontoolbox.expression;



import java.util.HashSet;

import java.util.Set;



/**

 *

 * @author matthew

 */

final public class EnumerationVariableType extends VariableType {



    public Set<String> enumerationValues() {

        return m_values;

    }



    @Override

    public boolean canCastToType(VariableType type) {

        return false;

    }



    final Set<String> m_values = new HashSet<String>();



    public static class Marker implements VariableTypeMarker {

        @Override

        public boolean isMarkerFor(VariableType m_type) {

            return m_type instanceof EnumerationVariableType;

        }

    }

}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/VariableCollection.java

+25 −2
Original line number Diff line number Diff line
@@ -16,18 +16,40 @@ 
 */

package ca.mcmaster.cas.tabularexpressiontoolbox.expression;



import java.util.HashMap;

import java.util.Map;

import java.util.Set;



/**

 * @author Matthew Dawson <matthew@mjdsystems.ca>

 */

final public class VariableCollection {

    public VariableCollection(Map<String, Variable> variables) {

    public VariableCollection(Map<String, Variable> variables, Set<EnumerationVariableType> enumerationTypes) {

        m_variables = variables;

        if (m_variables != null) {

            for(Map.Entry<String, Variable> var : m_variables.entrySet()) {

                m_variablesAndEnumeratedValues.put(var.getKey(), var.getValue());

            }

        }



        if (enumerationTypes != null) {

            for(EnumerationVariableType enumType : enumerationTypes) {

                for(String enumValue : enumType.enumerationValues()) {

                    if (m_variablesAndEnumeratedValues.containsKey(enumValue)) {

                        new IllegalArgumentException("Enumerated value conflicts with existing variable!");

                    }

                    m_variablesAndEnumeratedValues.put(enumValue, new Variable(enumValue, enumType));

                }

            }

        }

    }



    public VariableCollection(Map<String, Variable> variables) {

        this(variables, null);

    }



    public Map<String, Variable> getVariablesAndEnumeratedValues() {

        return m_variables;

        return m_variablesAndEnumeratedValues;

    }



    public Map<String, Variable> getVariables() {
@@ -35,4 +57,5 @@ final public class VariableCollection { 
    }



    private final Map<String,Variable> m_variables;

    private final Map<String,Variable> m_variablesAndEnumeratedValues = new HashMap<String, Variable>();

}

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/VariableParser.java

+10 −4
Original line number Diff line number Diff line
@@ -5,7 +5,7 @@ 
package ca.mcmaster.cas.tabularexpressiontoolbox.parsers;



import ca.mcmaster.cas.tabularexpressiontoolbox.expression.BooleanVariableType;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Expression;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.EnumerationVariableType;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.FixedPointVariableType;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.RealVariableType;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Variable;
@@ -16,7 +16,9 @@ import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParserParser.Fix 
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParserParser.Real_typeContext;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParserParser.VarContext;

import java.util.HashMap;

import java.util.HashSet;

import java.util.Map;

import java.util.Set;



import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableType;

import org.antlr.v4.runtime.ANTLRInputStream;
@@ -96,6 +98,8 @@ final public class VariableParser { 
            currentType = m_customTypes.get(ctx.UNKNOWN_TYPE().getText());

            if (currentType == null) { // Assume this unknown.  For now, pretend a real is wanted.

                currentType = new RealVariableType();

            } else if (currentType instanceof EnumerationVariableType) {

                m_usedEnumerationTypes.add((EnumerationVariableType)currentType);

            }

        }
@@ -135,8 +139,6 @@ final public class VariableParser { 


        @Override

        public void exitVarlist(@NotNull VariableParserParser.VarlistContext ctx) {

            m_variableCollection = new VariableCollection(m_variables);



            for(Map.Entry<String, limitingExpressionData> limitingExpression : m_variableLimitingExpressions.entrySet()) {

                String subtypeVar = limitingExpression.getValue().variableName;

                String subtypeExpression = limitingExpression.getValue().expression;
@@ -147,14 +149,18 @@ final public class VariableParser { 
                // effectively means the expression can just be emitted into the verification system to limit it.

                m_variables.put(subtypeVar, m_variables.get(limitingExpression.getKey()));



                m_variables.get(limitingExpression.getKey()).type().setSubtypePredicate(PVSSimpleParser.parsePVSCode(m_variableCollection, subtypeExpression));

                VariableCollection variableCollection = new VariableCollection(m_variables, m_usedEnumerationTypes);

                m_variables.get(limitingExpression.getKey()).type().setSubtypePredicate(PVSSimpleParser.parsePVSCode(variableCollection, subtypeExpression));



                // Undo the variables hack, to avoid having unused variables bleed into the verification scripts!

                m_variables.remove(subtypeVar);

            }



            m_variableCollection = new VariableCollection(m_variables, m_usedEnumerationTypes);

        }



        private Map<String, Variable>  m_variables = new HashMap<String, Variable>();

        private Set<EnumerationVariableType> m_usedEnumerationTypes = new HashSet<EnumerationVariableType>();

        public VariableCollection m_variableCollection;



        private Map<String, limitingExpressionData> m_variableLimitingExpressions = new HashMap<String, limitingExpressionData>();

Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/test/VariableCollectionTest.java

0 → 100644
+122 −0
Original line number Diff line number Diff line 
/*

 * Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>

 *

 * This program is free software: you can redistribute it and/or modify

 * it under the terms of the GNU General Public License as published by

 * the Free Software Foundation, either version 3 of the License, or

 * (at your option) any later version.

 *

 * This program is distributed in the hope that it will be useful,

 * but WITHOUT ANY WARRANTY; without even the implied warranty of

 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the

 * GNU General Public License for more details.

 *

 * You should have received a copy of the GNU General Public License

 * along with this program.  If not, see <http://www.gnu.org/licenses/>.

 */

package ca.mcmaster.cas.tabularexpressiontoolbox.expression.test;



import ca.mcmaster.cas.tabularexpressiontoolbox.expression.EnumerationVariableType;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.RealVariableType;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Variable;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableCollection;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableType;



import org.junit.Test;

import org.junit.runner.RunWith;

import org.junit.runners.JUnit4;



import java.util.HashMap;

import java.util.HashSet;

import java.util.Map;

import java.util.Set;



import static org.hamcrest.CoreMatchers.*;

import static org.junit.Assert.assertThat;



/**

 * @author Matthew Dawson <matthew@mjdsystems.ca>

 */

@RunWith(JUnit4.class)

public class VariableCollectionTest {



    private void AssertsForVariablesAreInBothLists(VariableCollection toTest) {

        assertThat(toTest.getVariables().size(), is(1));

        assertThat(toTest.getVariablesAndEnumeratedValues().size(), is(1));



        assertThat(toTest.getVariables().get("a").name(), is("a"));

        assertThat(toTest.getVariables().get("a").type(), is((VariableType)new RealVariableType()));

        assertThat(toTest.getVariables(), is(toTest.getVariablesAndEnumeratedValues()));

    }



    @Test

    public void VariablesAreInBothLists() {

        Map<String, Variable> vars = new HashMap<String, Variable>();

        vars.put("a", new Variable("a", new RealVariableType()));



        AssertsForVariablesAreInBothLists(new VariableCollection(vars));

        AssertsForVariablesAreInBothLists(new VariableCollection(vars, null));

        AssertsForVariablesAreInBothLists(new VariableCollection(vars, new HashSet<EnumerationVariableType>()));

    }



    @Test

    public void EnumeratedValuesAreInOneList() {

        EnumerationVariableType type = new EnumerationVariableType();

        type.enumerationValues().add("e1");

        type.enumerationValues().add("e2");

        type.enumerationValues().add("e3");



        Set<EnumerationVariableType> enums = new HashSet<EnumerationVariableType>();

        enums.add(type);



        VariableCollection vars = new VariableCollection(new HashMap<String, Variable>(), enums);



        assertThat(vars.getVariables().size(), is(0));



        assertThat(vars.getVariablesAndEnumeratedValues().size(), is(3));



        assertThat(vars.getVariablesAndEnumeratedValues().get("e1").name(), is("e1"));

        assertThat(vars.getVariablesAndEnumeratedValues().get("e1").type(), is((VariableType)type));



        assertThat(vars.getVariablesAndEnumeratedValues().get("e2").name(), is("e2"));

        assertThat(vars.getVariablesAndEnumeratedValues().get("e2").type(), is((VariableType)type));



        assertThat(vars.getVariablesAndEnumeratedValues().get("e3").name(), is("e3"));

        assertThat(vars.getVariablesAndEnumeratedValues().get("e3").type(), is((VariableType) type));

    }



    @Test

    public void EnumeratedValuesAndVariablesAreSeparate() {

        EnumerationVariableType type = new EnumerationVariableType();

        type.enumerationValues().add("e1");

        type.enumerationValues().add("e2");

        type.enumerationValues().add("e3");



        Set<EnumerationVariableType> enums = new HashSet<EnumerationVariableType>();

        enums.add(type);



        Map<String, Variable> var = new HashMap<String, Variable>();

        var.put("a", new Variable("a", type));



        VariableCollection vars = new VariableCollection(var, enums);



        assertThat(vars.getVariables().size(), is(1));



        assertThat(vars.getVariables().get("a").name(), is("a"));

        assertThat(vars.getVariables().get("a").type(), is((VariableType)type));



        assertThat(vars.getVariablesAndEnumeratedValues().size(), is(4));



        assertThat(vars.getVariablesAndEnumeratedValues().get("a").name(), is("a"));

        assertThat(vars.getVariablesAndEnumeratedValues().get("a").type(), is((VariableType)type));



        assertThat(vars.getVariablesAndEnumeratedValues().get("e1").name(), is("e1"));

        assertThat(vars.getVariablesAndEnumeratedValues().get("e1").type(), is((VariableType)type));



        assertThat(vars.getVariablesAndEnumeratedValues().get("e2").name(), is("e2"));

        assertThat(vars.getVariablesAndEnumeratedValues().get("e2").type(), is((VariableType)type));



        assertThat(vars.getVariablesAndEnumeratedValues().get("e3").name(), is("e3"));

        assertThat(vars.getVariablesAndEnumeratedValues().get("e3").type(), is((VariableType)type));

    }

}

Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/test/VariableParserTest.java

+22 −0
Original line number Diff line number Diff line
@@ -7,6 +7,7 @@ package ca.mcmaster.cas.tabularexpressiontoolbox.parsers.test; 
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.BooleanVariableType;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.CVC3Generator;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.CheckerGenerator;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.EnumerationVariableType;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.FixedPointVariableType;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.RealVariableType;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Variable;
@@ -171,5 +172,26 @@ public class VariableParserTest { 
        assertThat(vars.get("a").type(), is((VariableType) new RealVariableType()));

    }



    @Test

    public void testEnumerationsAreAvailable() {

        EnumerationVariableType enumType = new EnumerationVariableType();

        enumType.enumerationValues().add("enum1");

        enumType.enumerationValues().add("enum2");



        VariableParser variableParser = new VariableParser();

        variableParser.addCustomType("enumtype", enumType);



        VariableCollection vars = variableParser.parseVariables("a:enumtype");



        assertThat(vars.getVariables().size(), is(1));

        assertThat(vars.getVariablesAndEnumeratedValues().size(), is(3));



        assertThat(vars.getVariables().get("a").type(), is((VariableType)enumType));

        assertThat(vars.getVariablesAndEnumeratedValues().get("a").type(), is((VariableType)enumType));



        assertThat(vars.getVariablesAndEnumeratedValues().get("enum1").type(), is((VariableType)enumType));

        assertThat(vars.getVariablesAndEnumeratedValues().get("enum2").type(), is((VariableType)enumType));

    }



    CheckerGenerator generator = new CVC3Generator();

}