// Copyright (c) K Team. All Rights Reserved.
package org.kframework.parser.outer;

import java.util.List;

import junit.framework.Assert;

import org.junit.Test;
import org.kframework.attributes.Source;
import org.kframework.builtin.Sorts;
import org.kframework.kil.DefinitionItem;
import org.kframework.kil.Module;
import org.kframework.kil.StringSentence;

import static org.kframework.kore.KORE.*;

public class OuterParsingTests {

    @Test
    public void testEmptyRules() {
        String def = "module TEST rule endmodule";

        List<DefinitionItem> defItemList = Outer.parse(Source.apply("generated by OuterParsingTests"), def, null);

        Module mod = (Module) defItemList.get(0);
        StringSentence sen = (StringSentence) mod.getItems().get(0);
        Assert.assertEquals(sen.getContent(), "");
    }

    @Test
    public void testClaimKeyword() throws Exception {
        String def = "module TEST claim X => Y endmodule";

        List<DefinitionItem> defItemList = Outer.parse(Source.apply("generated by OuterParsingTests"), def, null);

        Module mod = (Module) defItemList.get(0);
        StringSentence sen = (StringSentence) mod.getItems().get(0);
        Assert.assertEquals(sen.getContent(), "X => Y");
        Assert.assertEquals(sen.getType(), "claim");
    }

    @Test
    public void testSortParsing() {
        Assert.assertEquals(Sorts.K().toString(), Outer.parseSort(Sorts.K().toString()).toString());
        Assert.assertEquals(Sorts.MInt().toString(), Outer.parseSort(Sorts.MInt().toString()).toString());
        Assert.assertEquals(Sort("X", Sort("6"), Sort("Z")).toString(),
            Outer.parseSort(Sort("X", Sort("6"), Sort("Z")).toString()).toString());
    }
}
