Test.java 文件源码

public static void main(String[] args) throws IOException {
    CoqLexer lexer = new CoqLexer(new ANTLRFileStream("../TestProgramC.v"));
    CoqFTParser parser = new CoqFTParser(new CommonTokenStream(lexer));

    //Listener listener = new Listener(parser);
    //parser.addParseListener(listener);
    //CoqParser.ProgContext ctx = parser.prog();
    //System.out.println(ctx.toStringTree(Arrays.asList(CoqParser.ruleNames)));

    Prog prog = parser.parseProg();
    for(Command command : prog) {
        if(command instanceof AssertionAndProof) {
            AssertionAndProof ap = (AssertionAndProof) command;
            System.out.println(ap.getAssertion());
            System.out.println("Proof:");
            for(Tactic tactic : ap.getProof().getTactics()) {
                System.out.println(tactic);
            }
        } else {
            System.out.println(command);
        }
    }
}