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}