001package org.clafer.ast;
002
003import org.clafer.common.Check;
004import org.clafer.common.Util;
005
006/**
007 *
008 * @author jimmy
009 */
010public class AstQuantify implements AstBoolExpr {
011
012    private final Quantifier quantifier;
013    private final AstDecl[] decls;
014    private final AstBoolExpr body;
015
016    public AstQuantify(Quantifier quantifier, AstDecl[] decls, AstBoolExpr body) {
017        this.quantifier = Check.notNull(quantifier);
018        this.decls = Check.noNullsNotEmpty(decls);
019        this.body = Check.notNull(body);
020    }
021
022    public Quantifier getQuantifier() {
023        return quantifier;
024    }
025
026    public AstDecl[] getDecls() {
027        return decls;
028    }
029
030    public AstBoolExpr getBody() {
031        return body;
032    }
033
034    @Override
035    public <A, B> B accept(AstExprVisitor<A, B> visitor, A a) {
036        return visitor.visit(this, a);
037    }
038
039    @Override
040    public String toString() {
041        return quantifier.getSyntax() + " " + Util.commaSeparate(decls) + " | " + body;
042    }
043    
044    
045
046    public static enum Quantifier {
047
048        All("all"),
049        Lone("lone"),
050        None("no"),
051        One("one"),
052        Some("some");
053        private final String syntax;
054
055        private Quantifier(String syntax) {
056            this.syntax = syntax;
057        }
058
059        public String getSyntax() {
060            return syntax;
061        }
062    }
063}