Support Corset defconstraint

This implements a (fairly minimal) change of syntax to use the corset
style for defining constraints.

pkg/hir/parser.go

@@ -92,14 +92,8 @@ func (p *hirParser) parseDeclaration(s sexp.SExp) error {
 			return p.parseModuleDeclaration(e)
 		} else if e.MatchSymbols(1, "defcolumns") {
 			return p.parseColumnDeclarations(e)
-		} else if e.Len() == 3 && e.MatchSymbols(2, "vanish") {
-			return p.parseVanishingDeclaration(e.Elements, nil)
-		} else if e.Len() == 3 && e.MatchSymbols(2, "vanish:last") {
-			domain := -1
-			return p.parseVanishingDeclaration(e.Elements, &domain)
-		} else if e.Len() == 3 && e.MatchSymbols(2, "vanish:first") {
-			domain := 0
-			return p.parseVanishingDeclaration(e.Elements, &domain)
+		} else if e.Len() == 4 && e.MatchSymbols(2, "defconstraint") {
+			return p.parseConstraintDeclaration(e.Elements)
 		} else if e.Len() == 3 && e.MatchSymbols(2, "assert") {
 			return p.parseAssertionDeclaration(e.Elements)
 		} else if e.Len() == 3 && e.MatchSymbols(1, "permute") {
@@ -111,7 +105,7 @@ func (p *hirParser) parseDeclaration(s sexp.SExp) error {
 		}
 	}
 	// Error
-	return p.translator.SyntaxError(s, "unexpected declaration")
+	return p.translator.SyntaxError(s, "unexpected or malformed declaration")
 }
 
 // Parse a column declaration
@@ -245,9 +239,9 @@ func (p *hirParser) parseSortedPermutationDeclaration(l *sexp.List) error {
 		ctx = ctx.Join(sourceCol.Context())
 		// Sanity check we have a sensible type here.
 		if ctx.IsConflicted() {
-			panic(fmt.Sprintf("source column %s has conflicted evaluation context", sexpSources.Get(i)))
+			return p.translator.SyntaxError(sexpSources.Get(i), "conflicting evaluation context")
 		} else if ctx.IsVoid() {
-			panic(fmt.Sprintf("source column %s has void evaluation context", sexpSources.Get(i)))
+			return p.translator.SyntaxError(sexpSources.Get(i), "empty evaluation context")
 		}
 		// Copy over column name
 		sources[i] = sourceIndex
@@ -356,9 +350,9 @@ func (p *hirParser) parseInterleavingDeclaration(l *sexp.List) error {
 		ctx = ctx.Join(sourceCol.Context())
 		// Sanity check we have a sensible context here.
 		if ctx.IsConflicted() {
-			panic(fmt.Sprintf("source column %s has conflicted evaluation context", sexpSources.Get(i)))
+			return p.translator.SyntaxError(sexpSources.Get(i), "conflicting evaluation context")
 		} else if ctx.IsVoid() {
-			panic(fmt.Sprintf("source column %s has void evaluation context", sexpSources.Get(i)))
+			return p.translator.SyntaxError(sexpSources.Get(i), "empty evaluation context")
 		}
 		// Assign
 		sources[i] = cid
@@ -389,30 +383,93 @@ func (p *hirParser) parseAssertionDeclaration(elements []sexp.SExp) error {
 }
 
 // Parse a vanishing declaration
-func (p *hirParser) parseVanishingDeclaration(elements []sexp.SExp, domain *int) error {
+func (p *hirParser) parseConstraintDeclaration(elements []sexp.SExp) error {
+	//
 	handle := elements[1].AsSymbol().Value
 	// Vanishing constraints do not have global scope, hence qualified column
 	// accesses are not permitted.
 	p.global = false
-	// Translate
-	expr, err := p.translator.Translate(elements[2])
+	attributes, err := p.parseConstraintAttributes(elements[2])
+	// Check for error
+	if err != nil {
+		return err
+	}
+	// Translate expression
+	expr, err := p.translator.Translate(elements[3])
 	if err != nil {
 		return err
 	}
 	// Determine evaluation context of expression.
 	ctx := expr.Context(p.env.schema)
 	// Sanity check we have a sensible context here.
 	if ctx.IsConflicted() {
-		panic(fmt.Sprintf("source column %s has conflicted evaluation context", elements[2]))
+		return p.translator.SyntaxError(elements[3], "conflicting evaluation context")
 	} else if ctx.IsVoid() {
-		panic(fmt.Sprintf("source column %s has void evaluation context", elements[2]))
+		return p.translator.SyntaxError(elements[3], "empty evaluation context")
 	}
 
-	p.env.schema.AddVanishingConstraint(handle, ctx, domain, expr)
+	p.env.schema.AddVanishingConstraint(handle, ctx, attributes, expr)
 
 	return nil
 }
 
+func (p *hirParser) parseConstraintAttributes(attributes sexp.SExp) (domain *int, err error) {
+	var res *int = nil
+	// Check attribute list is a list
+	if attributes.AsList() == nil {
+		return nil, p.translator.SyntaxError(attributes, "expected attribute list")
+	}
+	// Deconstruct as list
+	attrs := attributes.AsList()
+	// Process each attribute in turn
+	for i := 0; i < attrs.Len(); i++ {
+		ith := attrs.Get(i)
+		// Check start of attribute
+		if ith.AsSymbol() == nil {
+			return nil, p.translator.SyntaxError(ith, "malformed attribute")
+		}
+		// Check what we've got
+		switch ith.AsSymbol().Value {
+		case ":domain":
+			i++
+			if res, err = p.parseDomainAttribute(attrs.Get(i)); err != nil {
+				return nil, err
+			}
+		default:
+			return nil, p.translator.SyntaxError(ith, "unknown attribute")
+		}
+	}
+	// Done
+	return res, nil
+}
+
+func (p *hirParser) parseDomainAttribute(attribute sexp.SExp) (domain *int, err error) {
+	if attribute.AsSet() == nil {
+		return nil, p.translator.SyntaxError(attribute, "malformed domain set")
+	}
+	// Sanity check
+	set := attribute.AsSet()
+	// Check all domain elements well-formed.
+	for i := 0; i < set.Len(); i++ {
+		ith := set.Get(i)
+		if ith.AsSymbol() == nil {
+			return nil, p.translator.SyntaxError(ith, "malformed domain")
+		}
+	}
+	// Currently, only support domains of size 1.
+	if set.Len() == 1 {
+		first, err := strconv.Atoi(set.Get(0).AsSymbol().Value)
+		// Check for parse error
+		if err != nil {
+			return nil, p.translator.SyntaxError(set.Get(0), "malformed domain element")
+		}
+		// Done
+		return &first, nil
+	}
+	// Fail
+	return nil, p.translator.SyntaxError(attribute, "multiple values not supported")
+}
+
 func (p *hirParser) parseType(term sexp.SExp) (sc.Type, error) {
 	symbol := term.AsSymbol()
 	if symbol == nil {

pkg/schema/constraint/vanishing.go

@@ -215,18 +215,20 @@ func HoldsLocally[T sc.Testable](k uint, handle string, constraint T, tr tr.Trac
 //
 //nolint:revive
 func (p *VanishingConstraint[T]) Lisp(schema sc.Schema) sexp.SExp {
-	var head string
+	attributes := sexp.EmptyList()
+	// Handle attributes
 	if p.domain == nil {
-		head = "vanish"
+		// Skip
 	} else if *p.domain == 0 {
-		head = "vanish:first"
+		attributes.Append(sexp.NewSymbol(":first"))
 	} else {
-		head = "vanish:last"
+		attributes.Append(sexp.NewSymbol(":last"))
 	}
 	// Construct the list
 	return sexp.NewList([]sexp.SExp{
-		sexp.NewSymbol(head),
+		sexp.NewSymbol("defconstraint"),
 		sexp.NewSymbol(p.handle),
+		attributes,
 		p.constraint.Lisp(schema),
 	})
 }

pkg/sexp/parser.go

@@ -1,6 +1,8 @@
 package sexp
 
-import "unicode"
+import (
+	"unicode"
+)
 
 // Parse a given string into an S-expression, or return an error if the string
 // is malformed.
@@ -83,24 +85,21 @@ func (p *Parser) Parse() (SExp, error) {
 		p.index-- // backup
 		return nil, p.error("unexpected end-of-list")
 	} else if len(token) == 1 && token[0] == '(' {
-		var elements []SExp
-
-		for c := p.Lookahead(0); c == nil || *c != ')'; c = p.Lookahead(0) {
-			// Parse next element
-			element, err := p.Parse()
-			if err != nil {
-				return nil, err
-			} else if element == nil {
-				p.index-- // backup
-				return nil, p.error("unexpected end-of-file")
-			}
-			// Continue around!
-			elements = append(elements, element)
+		elements, err := p.parseSequence(')')
+		// Check for error
+		if err != nil {
+			return nil, err
 		}
-		// Consume right-brace
-		p.Next()
 		// Done
 		term = &List{elements}
+	} else if len(token) == 1 && token[0] == '{' {
+		elements, err := p.parseSequence('}')
+		// Check for error
+		if err != nil {
+			return nil, err
+		}
+		// Done
+		term = &Set{elements}
 	} else {
 		// Must be a symbol
 		term = &Symbol{string(token)}
@@ -121,8 +120,8 @@ func (p *Parser) Next() []rune {
 	}
 	// Check what we have
 	switch p.text[p.index] {
-	case '(', ')':
-		// List begin / end
+	case '(', ')', '{', '}':
+		// List/set begin / end
 		p.index = p.index + 1
 		return p.text[p.index-1 : p.index]
 	}
@@ -160,7 +159,7 @@ func (p *Parser) Lookahead(i int) *rune {
 	// Check what's there
 	if len(p.text) > pos {
 		r := p.text[pos]
-		if r == '(' || r == ')' || r == ';' {
+		if r == '(' || r == ')' || r == '{' || r == '}' || r == ';' {
 			return &r
 		} else if unicode.IsSpace(r) {
 			return p.Lookahead(i + 1)
@@ -176,7 +175,7 @@ func (p *Parser) parseSymbol() []rune {
 
 	for j := p.index; j < i; j++ {
 		c := p.text[j]
-		if c == ')' || c == ' ' || c == '\n' || c == '\t' {
+		if c == ')' || c == '}' || c == ' ' || c == '\n' || c == '\t' {
 			i = j
 			break
 		}
@@ -188,6 +187,27 @@ func (p *Parser) parseSymbol() []rune {
 	return token
 }
 
+func (p *Parser) parseSequence(terminator rune) ([]SExp, error) {
+	var elements []SExp
+
+	for c := p.Lookahead(0); c == nil || *c != terminator; c = p.Lookahead(0) {
+		// Parse next element
+		element, err := p.Parse()
+		if err != nil {
+			return nil, err
+		} else if element == nil {
+			p.index-- // backup
+			return nil, p.error("unexpected end-of-file")
+		}
+		// Continue around!
+		elements = append(elements, element)
+	}
+	// Consume terminator
+	p.Next()
+	//
+	return elements, nil
+}
+
 // Construct a parser error at the current position in the input stream.
 func (p *Parser) error(msg string) *SyntaxError {
 	span := NewSpan(p.index, p.index+1)

pkg/sexp/sexp.go

@@ -11,6 +11,9 @@ type SExp interface {
 	// AsList checks whether this S-Expression is a list and, if
 	// so, returns it.  Otherwise, it returns nil.
 	AsList() *List
+	// AsSet checks whether this S-Expression is a set and, if
+	// so, returns it.  Otherwise, it returns nil.
+	AsSet() *Set
 	// AsSymbol checks whether this S-Expression is a symbol and,
 	// if so, returns it.  Otherwise, it returns nil.
 	AsSymbol() *Symbol
@@ -46,6 +49,9 @@ func NewList(elements []SExp) *List {
 // AsList returns the given list.
 func (l *List) AsList() *List { return l }
 
+// AsSet returns nil for a list.
+func (l *List) AsSet() *Set { return nil }
+
 // AsSymbol returns nil for a list.
 func (l *List) AsSymbol() *Symbol { return nil }
 
@@ -97,6 +103,55 @@ func (l *List) MatchSymbols(n int, symbols ...string) bool {
 	return true
 }
 
+// ===================================================================
+// Set
+// ===================================================================
+
+// Set represents a list of zero or more S-Expressions.
+type Set struct {
+	Elements []SExp
+}
+
+// NOTE: This is used for compile time type checking if the given type
+// satisfies the given interface.
+var _ SExp = (*Set)(nil)
+
+// NewSet creates a new set from a given array of S-Expressions.
+func NewSet(elements []SExp) *Set {
+	return &Set{elements}
+}
+
+// AsList returns nil for a set.
+func (l *Set) AsList() *List { return nil }
+
+// AsSet returns the given set.
+func (l *Set) AsSet() *Set { return l }
+
+// AsSymbol returns nil for a set.
+func (l *Set) AsSymbol() *Symbol { return nil }
+
+// Len gets the number of elements in this set.
+func (l *Set) Len() int { return len(l.Elements) }
+
+// Get the ith element of this set
+func (l *Set) Get(i int) SExp { return l.Elements[i] }
+
+func (l *Set) String(quote bool) string {
+	var s = "{"
+
+	for i := 0; i < len(l.Elements); i++ {
+		if i != 0 {
+			s += " "
+		}
+
+		s += l.Elements[i].String(quote)
+	}
+
+	s += "}"
+
+	return s
+}
+
 // ===================================================================
 // Symbol
 // ===================================================================
@@ -118,6 +173,9 @@ func NewSymbol(value string) *Symbol {
 // AsList returns nil for a symbol.
 func (s *Symbol) AsList() *List { return nil }
 
+// AsSet returns nil for a symbol.
+func (s *Symbol) AsSet() *Set { return nil }
+
 // AsSymbol returns the given symbol
 func (s *Symbol) AsSymbol() *Symbol { return s }