From 572dff1240d4e5e0eda910ecee7c68f76e5c490f Mon Sep 17 00:00:00 2001 From: David Pearce Date: Tue, 17 Dec 2024 21:41:11 +1300 Subject: [PATCH] feat: support `reduce` (#445) * Add test cases for reduce * Support reduce operator This adds support for the reduce operator, which performsing folding over binary functions. * Support intrinsics This adds support for intrinsics which are needed for reductions (amongst other things). Specifically, they are required for reductions which operate over built-in operators, such as "+", "-", etc. At this stage, only a few intrinsics have been added and I'm anticipating that more will be required at some point. --- pkg/corset/binding.go | 57 +++++++++--- pkg/corset/declaration.go | 2 +- pkg/corset/expression.go | 155 ++++++++++++++++---------------- pkg/corset/intrinsics.go | 122 +++++++++++++++++++++++++ pkg/corset/parser.go | 96 ++++++++++++++++---- pkg/corset/resolver.go | 60 +++++++++---- pkg/corset/scope.go | 23 +++-- pkg/corset/translator.go | 33 +++++-- pkg/sexp/translator.go | 9 +- pkg/test/invalid_corset_test.go | 24 +++++ pkg/test/valid_corset_test.go | 36 +++++++- testdata/block_04.accepts | 10 +++ testdata/block_04.lisp | 4 + testdata/block_04.rejects | 12 +++ testdata/reduce_01.accepts | 7 ++ testdata/reduce_01.lisp | 3 + testdata/reduce_01.rejects | 6 ++ testdata/reduce_02.accepts | 10 +++ testdata/reduce_02.lisp | 3 + testdata/reduce_02.rejects | 12 +++ testdata/reduce_03.accepts | 11 +++ testdata/reduce_03.lisp | 3 + testdata/reduce_03.rejects | 13 +++ testdata/reduce_04.accepts | 11 +++ testdata/reduce_04.lisp | 10 +++ testdata/reduce_04.rejects | 7 ++ testdata/reduce_05.accepts | 7 ++ testdata/reduce_05.lisp | 3 + testdata/reduce_05.rejects | 6 ++ testdata/reduce_invalid_01.lisp | 2 + testdata/reduce_invalid_02.lisp | 1 + testdata/reduce_invalid_03.lisp | 2 + testdata/reduce_invalid_04.lisp | 3 + testdata/reduce_invalid_05.lisp | 3 + 34 files changed, 616 insertions(+), 150 deletions(-) create mode 100644 pkg/corset/intrinsics.go create mode 100644 testdata/block_04.accepts create mode 100644 testdata/block_04.lisp create mode 100644 testdata/block_04.rejects create mode 100644 testdata/reduce_01.accepts create mode 100644 testdata/reduce_01.lisp create mode 100644 testdata/reduce_01.rejects create mode 100644 testdata/reduce_02.accepts create mode 100644 testdata/reduce_02.lisp create mode 100644 testdata/reduce_02.rejects create mode 100644 testdata/reduce_03.accepts create mode 100644 testdata/reduce_03.lisp create mode 100644 testdata/reduce_03.rejects create mode 100644 testdata/reduce_04.accepts create mode 100644 testdata/reduce_04.lisp create mode 100644 testdata/reduce_04.rejects create mode 100644 testdata/reduce_05.accepts create mode 100644 testdata/reduce_05.lisp create mode 100644 testdata/reduce_05.rejects create mode 100644 testdata/reduce_invalid_01.lisp create mode 100644 testdata/reduce_invalid_02.lisp create mode 100644 testdata/reduce_invalid_03.lisp create mode 100644 testdata/reduce_invalid_04.lisp create mode 100644 testdata/reduce_invalid_05.lisp diff --git a/pkg/corset/binding.go b/pkg/corset/binding.go index dfc07be4..100a3623 100644 --- a/pkg/corset/binding.go +++ b/pkg/corset/binding.go @@ -24,6 +24,26 @@ type Binding interface { IsFinalised() bool } +// FunctionBinding is a special kind of binding which captures the essence of +// something which can be called. For example, this could be a user-defined +// function or an intrinsic. +type FunctionBinding interface { + Binding + // IsPure checks whether this function binding has side-effects or not. + IsPure() bool + // HasArity checks whether this binding supports a given number of + // parameters. For example, intrinsic functions are often nary --- meaning + // they can accept any number of arguments. In contrast, a user-defined + // function may only accept a specific number of arguments, etc. + HasArity(uint) bool + // Apply a set of concreate arguments to this function. This substitutes + // them through the body of the function producing a single expression. + Apply([]Expr) Expr + // Get the declared return type of this function, or nil if no return type + // was declared. + ReturnType() Type +} + // ============================================================================ // ColumnBinding // ============================================================================ @@ -158,12 +178,12 @@ func (p *LocalVariableBinding) Finalise(index uint) { } // ============================================================================ -// FunctionBinding +// DefunBinding // ============================================================================ -// FunctionBinding represents the binding of a function application to its -// physical definition. -type FunctionBinding struct { +// DefunBinding is a function binding arising from a user-defined function (as +// opposed, for example, to a function binding arising from an intrinsic). +type DefunBinding struct { // Flag whether or not is pure function pure bool // Types of parameters (optional) @@ -177,33 +197,42 @@ type FunctionBinding struct { body Expr } -// NewFunctionBinding constructs a new function binding. -func NewFunctionBinding(pure bool, paramTypes []Type, returnType Type, body Expr) FunctionBinding { - return FunctionBinding{pure, paramTypes, returnType, nil, body} +var _ FunctionBinding = &DefunBinding{} + +// NewDefunBinding constructs a new function binding. +func NewDefunBinding(pure bool, paramTypes []Type, returnType Type, body Expr) DefunBinding { + return DefunBinding{pure, paramTypes, returnType, nil, body} } // IsPure checks whether this is a defpurefun or not -func (p *FunctionBinding) IsPure() bool { +func (p *DefunBinding) IsPure() bool { return p.pure } // IsFinalised checks whether this binding has been finalised yet or not. -func (p *FunctionBinding) IsFinalised() bool { +func (p *DefunBinding) IsFinalised() bool { return p.bodyType != nil } -// Arity returns the number of parameters that this function accepts. -func (p *FunctionBinding) Arity() uint { - return uint(len(p.paramTypes)) +// HasArity checks whether this function accepts a given number of arguments (or +// not). +func (p *DefunBinding) HasArity(arity uint) bool { + return arity == uint(len(p.paramTypes)) +} + +// ReturnType gets the declared return type of this function, or nil if no +// return type was declared. +func (p *DefunBinding) ReturnType() Type { + return p.returnType } // Finalise this binding by providing the necessary missing information. -func (p *FunctionBinding) Finalise(bodyType Type) { +func (p *DefunBinding) Finalise(bodyType Type) { p.bodyType = bodyType } // Apply a given set of arguments to this function binding. -func (p *FunctionBinding) Apply(args []Expr) Expr { +func (p *DefunBinding) Apply(args []Expr) Expr { mapping := make(map[uint]Expr) // Setup the mapping for i, e := range args { diff --git a/pkg/corset/declaration.go b/pkg/corset/declaration.go index fca08fd1..5285df6a 100644 --- a/pkg/corset/declaration.go +++ b/pkg/corset/declaration.go @@ -819,7 +819,7 @@ type DefFun struct { // Parameters parameters []*DefParameter // - binding FunctionBinding + binding DefunBinding } // IsFunction is always true for a function definition! diff --git a/pkg/corset/expression.go b/pkg/corset/expression.go index 7be4a679..e1e8115f 100644 --- a/pkg/corset/expression.go +++ b/pkg/corset/expression.go @@ -158,7 +158,10 @@ func (e *ArrayAccess) Context() Context { // Lisp converts this schema element into a simple S-Expression, for example // so it can be printed. func (e *ArrayAccess) Lisp() sexp.SExp { - panic("todo") + return sexp.NewArray([]sexp.SExp{ + sexp.NewSymbol(e.name), + e.arg.Lisp(), + }) } // Substitute all variables (such as for function parameters) arising in @@ -461,65 +464,23 @@ func (e *If) Dependencies() []Symbol { // Invoke represents an attempt to invoke a given function. type Invoke struct { - module *string - name string - args []Expr - binding *FunctionBinding + fn *VariableAccess + args []Expr } // AsConstant attempts to evaluate this expression as a constant (signed) value. // If this expression is not constant, then nil is returned. func (e *Invoke) AsConstant() *big.Int { - if e.binding == nil { + if e.fn.binding == nil { panic("unresolved invocation") + } else if fn_binding, ok := e.fn.binding.(FunctionBinding); ok { + // Unroll body + body := fn_binding.Apply(e.args) + // Attempt to evaluate as constant + return body.AsConstant() } - // Unroll body - body := e.binding.Apply(e.args) - // Attempt to evaluate as constant - return body.AsConstant() -} - -// IsQualified determines whether this symbol is qualfied or not (i.e. has an -// explicitly module specifier). -func (e *Invoke) IsQualified() bool { - return e.module != nil -} - -// IsFunction indicates whether or not this symbol refers to a function (which -// of course it always does). -func (e *Invoke) IsFunction() bool { - return true -} - -// IsResolved checks whether this symbol has been resolved already, or not. -func (e *Invoke) IsResolved() bool { - return e.binding != nil -} - -// Resolve this symbol by associating it with the binding associated with -// the definition of the symbol to which this refers. -func (e *Invoke) Resolve(binding Binding) bool { - if fb, ok := binding.(*FunctionBinding); ok { - e.binding = fb - return true - } - // Problem - return false -} - -// Module returns the optional module qualification. This will panic if this -// invocation is unqualified. -func (e *Invoke) Module() string { - if e.module == nil { - panic("invocation has no module qualifier") - } - - return *e.module -} - -// Name of the function being invoked. -func (e *Invoke) Name() string { - return e.name + // Just fail + return nil } // Args returns the arguments provided by this invocation to the function being @@ -528,24 +489,10 @@ func (e *Invoke) Args() []Expr { return e.args } -// Binding gets binding associated with this interface. This will panic if this -// symbol is not yet resolved. -func (e *Invoke) Binding() Binding { - if e.binding == nil { - panic("invocation not yet resolved") - } - - return e.binding -} - // Context returns the context for this expression. Observe that the // expression must have been resolved for this to be defined (i.e. it may // panic if it has not been resolved yet). func (e *Invoke) Context() Context { - if e.binding == nil { - panic("unresolved expressions encountered whilst resolving context") - } - // TODO: impure functions can have their own context. return ContextOfExpressions(e.args) } @@ -559,20 +506,13 @@ func (e *Invoke) Multiplicity() uint { // Lisp converts this schema element into a simple S-Expression, for example // so it can be printed. func (e *Invoke) Lisp() sexp.SExp { - var fn sexp.SExp - if e.module != nil { - fn = sexp.NewSymbol(fmt.Sprintf("%s.%s", *e.module, e.name)) - } else { - fn = sexp.NewSymbol(e.name) - } - - return ListOfExpressions(fn, e.args) + return ListOfExpressions(e.fn.Lisp(), e.args) } // Substitute all variables (such as for function parameters) arising in // this expression. func (e *Invoke) Substitute(mapping map[uint]Expr) Expr { - return &Invoke{e.module, e.name, SubstituteExpressions(e.args, mapping), e.binding} + return &Invoke{e.fn, SubstituteExpressions(e.args, mapping)} } // Dependencies needed to signal declaration. @@ -580,7 +520,7 @@ func (e *Invoke) Dependencies() []Symbol { deps := DependenciesOfExpressions(e.args) // Include this expression as a symbol (which must be bound to the function // being invoked) - return append(deps, e) + return append(deps, e.fn) } // ============================================================================ @@ -718,6 +658,60 @@ func (e *Normalise) Dependencies() []Symbol { return e.Arg.Dependencies() } +// ============================================================================ +// Reduction +// ============================================================================ + +// Reduce reduces (i.e. folds) a list using a given binary function. +type Reduce struct { + fn *VariableAccess + arg Expr +} + +// AsConstant attempts to evaluate this expression as a constant (signed) value. +// If this expression is not constant, then nil is returned. +func (e *Reduce) AsConstant() *big.Int { + // TODO: potentially we can do better here. + return nil +} + +// Multiplicity determines the number of values that evaluating this expression +// can generate. +func (e *Reduce) Multiplicity() uint { + return 1 +} + +// Context returns the context for this expression. Observe that the +// expression must have been resolved for this to be defined (i.e. it may +// panic if it has not been resolved yet). +func (e *Reduce) Context() Context { + return e.arg.Context() +} + +// Lisp converts this schema element into a simple S-Expression, for example +// so it can be printed. +func (e *Reduce) Lisp() sexp.SExp { + return sexp.NewList([]sexp.SExp{ + sexp.NewSymbol("reduce"), + sexp.NewSymbol(e.fn.name), + e.arg.Lisp()}) +} + +// Substitute all variables (such as for function parameters) arising in +// this expression. +func (e *Reduce) Substitute(mapping map[uint]Expr) Expr { + return &Reduce{ + e.fn, + e.arg.Substitute(mapping), + } +} + +// Dependencies needed to signal declaration. +func (e *Reduce) Dependencies() []Symbol { + deps := e.arg.Dependencies() + return append(deps, e.fn) +} + // ============================================================================ // Subtraction // ============================================================================ @@ -828,6 +822,7 @@ func (e *Shift) Dependencies() []Symbol { type VariableAccess struct { module *string name string + fn bool binding Binding } @@ -850,7 +845,7 @@ func (e *VariableAccess) IsQualified() bool { // IsFunction determines whether this symbol refers to a function (which, of // course, variable accesses never do). func (e *VariableAccess) IsFunction() bool { - return false + return e.fn } // IsResolved checks whether this symbol has been resolved already, or not. @@ -865,6 +860,10 @@ func (e *VariableAccess) Resolve(binding Binding) bool { panic("empty binding") } else if e.binding != nil { panic("already resolved") + } else if _, ok := binding.(FunctionBinding); ok && !e.fn { + return false + } else if _, ok := binding.(FunctionBinding); !ok && e.fn { + return false } // e.binding = binding diff --git a/pkg/corset/intrinsics.go b/pkg/corset/intrinsics.go new file mode 100644 index 00000000..ceeb30db --- /dev/null +++ b/pkg/corset/intrinsics.go @@ -0,0 +1,122 @@ +package corset + +import ( + "fmt" + "math" + + "github.com/consensys/go-corset/pkg/sexp" +) + +// IntrinsicDefinition is a SymbolDefinition for an intrinsic (i.e. built-in) +// operation, such as "+", "-", etc. These are needed for two reasons: firstly, +// so we can alias them; secondly, so they can be used in reductions. +type IntrinsicDefinition struct { + // Name of the intrinsic (e.g. "+") + name string + // Minimum number of arguments this intrinsic can accept. + min_arity uint + // Maximum number of arguments this intrinsic can accept. + max_arity uint + // Construct an instance of this intrinsic for a given arity (i.e. number of + // arguments). + constructor func(uint) Expr +} + +var _ FunctionBinding = &IntrinsicDefinition{} + +// Name returns the name of the intrinsic being defined. +func (p *IntrinsicDefinition) Name() string { + return p.name +} + +// IsPure checks whether this pure (which intrinsics always are). +func (p *IntrinsicDefinition) IsPure() bool { + return true +} + +// IsFunction identifies whether or not the intrinsic being defined is a +// function. At this time, all intrinsics are functions. +func (p *IntrinsicDefinition) IsFunction() bool { + return true +} + +// IsFinalised checks whether this binding has been finalised yet or not. +func (p *IntrinsicDefinition) IsFinalised() bool { + return true +} + +// ReturnType gets the declared return type of this function, or nil if no +// return type was declared. +func (p *IntrinsicDefinition) ReturnType() Type { + return nil +} + +// Binding returns the binding associated with this intrinsic. +func (p *IntrinsicDefinition) Binding() Binding { + return p +} + +// Lisp returns a lisp representation of this intrinsic. +func (p *IntrinsicDefinition) Lisp() sexp.SExp { + panic("unreacahble") +} + +// HasArity checks whether this function accepts a given number of arguments (or +// not). +func (p *IntrinsicDefinition) HasArity(arity uint) bool { + return arity >= p.min_arity && arity <= p.max_arity +} + +// Apply a given set of arguments to this function binding. +func (p *IntrinsicDefinition) Apply(args []Expr) Expr { + // First construct the body + body := p.constructor(uint(len(args))) + // Then, substitute through. + mapping := make(map[uint]Expr) + // Setup the mapping + for i, e := range args { + mapping[uint(i)] = e + } + // Substitute through + return body.Substitute(mapping) +} + +// ============================================================================ +// Intrinsic Definitions +// ============================================================================ + +// INTRINSICS identifies all of the built-in functions used within the corset +// language, such as "+", "-", etc. This is needed for two reasons: firstly, so +// we can alias them; secondly, so they can be used in reductions. +var INTRINSICS []IntrinsicDefinition = []IntrinsicDefinition{ + // Addition + {"+", 1, math.MaxUint, intrinsicAdd}, + // Subtraction + {"-", 1, math.MaxUint, intrinsicSub}, + // Multiplication + {"*", 1, math.MaxUint, intrinsicMul}, +} + +func intrinsicAdd(arity uint) Expr { + return &Add{intrinsicNaryBody(arity)} +} + +func intrinsicSub(arity uint) Expr { + return &Sub{intrinsicNaryBody(arity)} +} + +func intrinsicMul(arity uint) Expr { + return &Mul{intrinsicNaryBody(arity)} +} + +func intrinsicNaryBody(arity uint) []Expr { + args := make([]Expr, arity) + // + for i := uint(0); i != arity; i++ { + name := fmt.Sprintf("x%d", i) + binding := &LocalVariableBinding{name, nil, i} + args[i] = &VariableAccess{nil, name, true, binding} + } + // + return args +} diff --git a/pkg/corset/parser.go b/pkg/corset/parser.go index 7adb10cd..658f99ff 100644 --- a/pkg/corset/parser.go +++ b/pkg/corset/parser.go @@ -153,9 +153,10 @@ func NewParser(srcfile *sexp.SourceFile, srcmap *sexp.SourceMap[sexp.SExp]) *Par p.AddRecursiveListRule("^", powParserRule) p.AddRecursiveListRule("begin", beginParserRule) p.AddListRule("for", forParserRule(parser)) + p.AddListRule("reduce", reduceParserRule(parser)) p.AddRecursiveListRule("if", ifParserRule) p.AddRecursiveListRule("shift", shiftParserRule) - p.AddDefaultRecursiveListRule(invokeParserRule) + p.AddDefaultListRule(invokeParserRule(parser)) p.AddDefaultRecursiveArrayRule(arrayAccessParserRule) // return parser @@ -714,7 +715,7 @@ func (p *Parser) parseDefFun(pure bool, elements []sexp.SExp) (Declaration, []Sy paramTypes[i] = p.Binding.datatype } // Construct binding - binding := NewFunctionBinding(pure, paramTypes, ret, body) + binding := NewDefunBinding(pure, paramTypes, ret, body) // return &DefFun{name, params, binding}, nil } @@ -950,7 +951,7 @@ func forParserRule(p *Parser) sexp.ListRule[Expr] { ) // Check we've got the expected number if list.Len() != 4 { - msg := fmt.Sprintf("expected 3 arguments, found %d", list.Len()) + msg := fmt.Sprintf("expected 3 arguments, found %d", list.Len()-1) return nil, p.translator.SyntaxErrors(list, msg) } // Extract index variable @@ -1015,6 +1016,35 @@ func parseForRange(p *Parser, interval sexp.SExp) (uint, uint, []SyntaxError) { return uint(start), uint(end), nil } +func reduceParserRule(p *Parser) sexp.ListRule[Expr] { + return func(list *sexp.List) (Expr, []SyntaxError) { + var errors []SyntaxError + // Check we've got the expected number + if list.Len() != 3 { + msg := fmt.Sprintf("expected 2 arguments, found %d", list.Len()-1) + return nil, p.translator.SyntaxErrors(list, msg) + } + // function name + name := list.Get(1).AsSymbol() + // + if name == nil { + errors = append(errors, *p.translator.SyntaxError(list.Get(1), "invalid function")) + } + // Parse body + body, errs := p.translator.Translate(list.Get(2)) + errors = append(errors, errs...) + // Error check + if len(errors) > 0 { + return nil, errors + } + // + varaccess := &VariableAccess{nil, name.Value, true, nil} + p.mapSourceNode(name, varaccess) + // + return &Reduce{varaccess, body}, nil + } +} + func constantParserRule(symbol string) (Expr, bool, error) { var ( base int @@ -1051,11 +1081,11 @@ func varAccessParserRule(col string) (Expr, bool, error) { // Attempt to split column name into module / column pair. split := strings.Split(col, ".") if len(split) == 2 { - return &VariableAccess{&split[0], split[1], nil}, true, nil + return &VariableAccess{&split[0], split[1], false, nil}, true, nil } else if len(split) > 2 { return nil, true, errors.New("malformed column access") } else { - return &VariableAccess{nil, col, nil}, true, nil + return &VariableAccess{nil, col, false, nil}, true, nil } } @@ -1089,20 +1119,48 @@ func ifParserRule(_ string, args []Expr) (Expr, error) { return nil, errors.New("incorrect number of arguments") } -func invokeParserRule(name string, args []Expr) (Expr, error) { - // Sanity check what we have - if !unicode.IsLetter(rune(name[0])) { - return nil, nil - } - // Handle qualified accesses (where permitted) - // Attempt to split column name into module / column pair. - split := strings.Split(name, ".") - if len(split) == 2 { - return &Invoke{&split[0], split[1], args, nil}, nil - } else if len(split) > 2 { - return nil, errors.New("malformed function invocation") - } else { - return &Invoke{nil, name, args, nil}, nil +func invokeParserRule(p *Parser) sexp.ListRule[Expr] { + return func(list *sexp.List) (Expr, []SyntaxError) { + var ( + varaccess *VariableAccess + errors []SyntaxError + ) + // + if list.Len() == 0 || list.Get(0).AsSymbol() == nil { + return nil, p.translator.SyntaxErrors(list, "invalid invocation") + } + // Extract function name + name := list.Get(0).AsSymbol().Value + // Sanity check what we have + if !unicode.IsLetter(rune(name[0])) { + errors = append(errors, *p.translator.SyntaxError(list.Get(0), "invalid function name")) + } + // Handle qualified accesses (where permitted) + // Attempt to split column name into module / column pair. + split := strings.Split(name, ".") + if len(split) == 2 { + // + varaccess = &VariableAccess{&split[0], split[1], true, nil} + } else if len(split) > 2 { + return nil, p.translator.SyntaxErrors(list.Get(0), "invalid function name") + } else { + varaccess = &VariableAccess{nil, split[0], true, nil} + } + // Parse arguments + args := make([]Expr, list.Len()-1) + for i := 0; i < len(args); i++ { + var errs []SyntaxError + args[i], errs = p.translator.Translate(list.Get(i + 1)) + errors = append(errors, errs...) + } + // Error check + if len(errors) > 0 { + return nil, errors + } + // + p.mapSourceNode(list.Get(0), varaccess) + // + return &Invoke{varaccess, args}, nil } } diff --git a/pkg/corset/resolver.go b/pkg/corset/resolver.go index d905cfa8..d92d4fb5 100644 --- a/pkg/corset/resolver.go +++ b/pkg/corset/resolver.go @@ -142,7 +142,7 @@ func (r *resolver) initialiseAliasesInModule(scope *ModuleScope, decls []Declara err := r.srcmap.SyntaxError(alias, "symbol already exists") errors = append(errors, *err) } else { - err := r.srcmap.SyntaxError(symbol, "unknown symbol") + err := r.srcmap.SyntaxError(symbol, "unknown symbol encountered during resolution") errors = append(errors, *err) } } @@ -237,7 +237,7 @@ func (r *resolver) declarationDependenciesAreFinalised(scope *ModuleScope, symbol := iter.Next() // Attempt to resolve if !symbol.IsResolved() && !scope.Bind(symbol) { - errors = append(errors, *r.srcmap.SyntaxError(symbol, "unknown symbol")) + errors = append(errors, *r.srcmap.SyntaxError(symbol, "unknown symbol encountered during resolution")) // not finalised yet finalised = false } else { @@ -526,12 +526,14 @@ func (r *resolver) finaliseExpressionInModule(scope LocalScope, expr Expr) (Type return r.finaliseInvokeInModule(scope, v) } else if v, ok := expr.(*List); ok { types, errs := r.finaliseExpressionsInModule(scope, v.Args) - return GreatestLowerBoundAll(types), errs + return LeastUpperBoundAll(types), errs } else if v, ok := expr.(*Mul); ok { types, errs := r.finaliseExpressionsInModule(scope, v.Args) return GreatestLowerBoundAll(types), errs } else if v, ok := expr.(*Normalise); ok { return r.finaliseExpressionInModule(scope, v.Arg) + } else if v, ok := expr.(*Reduce); ok { + return r.finaliseReduceInModule(scope, v) } else if v, ok := expr.(*Shift); ok { purescope := scope.NestedPureScope() arg_types, arg_errs := r.finaliseExpressionInModule(scope, v.Arg) @@ -562,10 +564,6 @@ func (r *resolver) finaliseArrayAccessInModule(scope LocalScope, expr *ArrayAcce return nil, r.srcmap.SyntaxErrors(expr, "unknown array column") } else if arr_t, ok := binding.dataType.(*ArrayType); !ok { return nil, r.srcmap.SyntaxErrors(expr, "expected array column") - } else if c := expr.arg.AsConstant(); c == nil { - return nil, r.srcmap.SyntaxErrors(expr, "expected constant array index") - } else if i := uint(c.Uint64()); i == 0 || i > arr_t.Width() { - return nil, r.srcmap.SyntaxErrors(expr, "array access out-of-bounds") } else { // All good return arr_t.element, nil @@ -605,29 +603,61 @@ func (r *resolver) finaliseInvokeInModule(scope LocalScope, expr *Invoke) (Type, return nil, errors } // Lookup the corresponding function definition. - if !scope.Bind(expr) { + if !expr.fn.IsResolved() && !scope.Bind(expr.fn) { return nil, r.srcmap.SyntaxErrors(expr, "unknown function") - } else if scope.IsPure() && !expr.binding.IsPure() { + } + // Following must be true if we get here. + binding := expr.fn.binding.(FunctionBinding) + + if scope.IsPure() && !binding.IsPure() { return nil, r.srcmap.SyntaxErrors(expr, "not permitted in pure context") - } else if binding := expr.binding; binding.Arity() != uint(len(expr.Args())) { - msg := fmt.Sprintf("incorrect number of arguments (expected %d, found %d)", binding.Arity(), len(expr.Args())) + } else if !binding.HasArity(uint(len(expr.Args()))) { + msg := fmt.Sprintf("incorrect number of arguments (found %d)", len(expr.Args())) return nil, r.srcmap.SyntaxErrors(expr, msg) } // Check whether need to infer return type - if expr.binding.returnType != nil { + if binding.ReturnType() != nil { // no need, it was provided - return expr.binding.returnType, nil + return binding.ReturnType(), nil } // TODO: this is potentially expensive, and it would likely be good if we // could avoid it. Realistically, this is just about determining the right // type information. Potentially, we could adjust the local scope to // provide the required type information. Or we could have a separate pass // which just determines the type. - body := expr.binding.Apply(expr.Args()) + body := binding.Apply(expr.Args()) // Dig out the type return r.finaliseExpressionInModule(scope, body) } +// Resolve a specific invocation contained within some expression which, in +// turn, is contained within some module. Note, qualified accesses are only +// permitted in a global context. +func (r *resolver) finaliseReduceInModule(scope LocalScope, expr *Reduce) (Type, []SyntaxError) { + // Resolve arguments + body_t, errors := r.finaliseExpressionInModule(scope, expr.arg) + // Lookup the corresponding function definition. + if !expr.fn.IsResolved() && !scope.Bind(expr.fn) { + errors = append(errors, *r.srcmap.SyntaxError(expr, "unknown function")) + } else { + // Following must be true if we get here. + binding := expr.fn.binding.(FunctionBinding) + + if scope.IsPure() && !binding.IsPure() { + errors = append(errors, *r.srcmap.SyntaxError(expr, "not permitted in pure context")) + } else if !binding.HasArity(2) { + msg := "incorrect number of arguments (expected 2)" + errors = append(errors, *r.srcmap.SyntaxError(expr, msg)) + } + } + // Error check + if len(errors) > 0 { + return nil, errors + } + // + return body_t, nil +} + // Resolve a specific variable access contained within some expression which, in // turn, is contained within some module. Note, qualified accesses are only // permitted in a global context. @@ -661,7 +691,7 @@ func (r *resolver) finaliseVariableInModule(scope LocalScope, } else if binding, ok := expr.Binding().(*LocalVariableBinding); ok { // Parameter return binding.datatype, nil - } else if _, ok := expr.Binding().(*FunctionBinding); ok { + } else if _, ok := expr.Binding().(FunctionBinding); ok { // Function doesn't makes sense here. return nil, r.srcmap.SyntaxErrors(expr, "refers to a function") } diff --git a/pkg/corset/scope.go b/pkg/corset/scope.go index ebf85c26..a0b92e51 100644 --- a/pkg/corset/scope.go +++ b/pkg/corset/scope.go @@ -47,9 +47,16 @@ func (p *GlobalScope) DeclareModule(module string) { } // Register module mid := uint(len(p.ids)) - scope := ModuleScope{module, mid, make(map[BindingId]uint), make([]Binding, 0), p} - p.modules = append(p.modules, scope) + p.modules = append(p.modules, ModuleScope{ + module, mid, make(map[BindingId]uint), make([]Binding, 0), p, + }) p.ids[module] = mid + // Declare intrinsics (if applicable) + if module == "" { + for _, i := range INTRINSICS { + p.modules[mid].Declare(&i) + } + } } // HasModule checks whether a given module exists, or not. @@ -139,9 +146,9 @@ func (p *ModuleScope) Bind(symbol Symbol) bool { // Attempt to lookup in parent (unless we are the root module, in which // case we have no parent) return p.enclosing.Bind(symbol) - } else { - return false } + // + return false } // Binding returns information about the binding of a particular symbol defined @@ -167,16 +174,16 @@ func (p *ModuleScope) Column(name string) *ColumnBinding { // Declare declares a given binding within this module scope. func (p *ModuleScope) Declare(symbol SymbolDefinition) bool { // construct binding identifier - bid := BindingId{symbol.Name(), symbol.IsFunction()} + id := BindingId{symbol.Name(), symbol.IsFunction()} // Sanity check not already declared - if _, ok := p.ids[bid]; ok { + if _, ok := p.ids[id]; ok { // Cannot redeclare return false } // Done - id := uint(len(p.bindings)) + bid := uint(len(p.bindings)) p.bindings = append(p.bindings, symbol.Binding()) - p.ids[bid] = id + p.ids[id] = bid // return true } diff --git a/pkg/corset/translator.go b/pkg/corset/translator.go index 3aa231b3..1b1dea58 100644 --- a/pkg/corset/translator.go +++ b/pkg/corset/translator.go @@ -422,6 +422,8 @@ func (t *translator) translateExpressionInModule(expr Expr, module string, shift } else if v, ok := expr.(*Normalise); ok { arg, errs := t.translateExpressionInModule(v.Arg, module, shift) return &hir.Normalise{Arg: arg}, errs + } else if v, ok := expr.(*Reduce); ok { + return t.translateReduceInModule(v, module, shift) } else if v, ok := expr.(*Sub); ok { args, errs := t.translateExpressionsInModule(v.Args, module) return &hir.Sub{Args: args}, errs @@ -436,17 +438,20 @@ func (t *translator) translateExpressionInModule(expr Expr, module string, shift func (t *translator) translateArrayAccessInModule(expr *ArrayAccess, shift int) (hir.Expr, []SyntaxError) { var errors []SyntaxError - // Array index should be statically known - index := expr.arg.AsConstant() - if index == nil { - errors = append(errors, *t.srcmap.SyntaxError(expr.arg, "expected constant array index")) - } // Lookup the column binding, ok := expr.Binding().(*ColumnBinding) // Did we find it? if !ok { errors = append(errors, *t.srcmap.SyntaxError(expr.arg, "invalid array index encountered during translation")) } + // Array index should be statically known + index := expr.arg.AsConstant() + // + if index == nil { + errors = append(errors, *t.srcmap.SyntaxError(expr.arg, "expected constant array index")) + } else if i := uint(index.Uint64()); i == 0 || (binding != nil && i > binding.dataType.Width()) { + errors = append(errors, *t.srcmap.SyntaxError(expr.arg, "array index out-of-bounds")) + } // Error check if len(errors) > 0 { return nil, errors @@ -503,7 +508,7 @@ func (t *translator) translateForInModule(expr *For, module string, shift int) ( } func (t *translator) translateInvokeInModule(expr *Invoke, module string, shift int) (hir.Expr, []SyntaxError) { - if binding, ok := expr.Binding().(*FunctionBinding); ok { + if binding, ok := expr.fn.Binding().(FunctionBinding); ok { body := binding.Apply(expr.Args()) return t.translateExpressionInModule(body, module, shift) } @@ -511,6 +516,22 @@ func (t *translator) translateInvokeInModule(expr *Invoke, module string, shift return nil, t.srcmap.SyntaxErrors(expr, "unbound function") } +func (t *translator) translateReduceInModule(expr *Reduce, module string, shift int) (hir.Expr, []SyntaxError) { + if list, ok := expr.arg.(*List); !ok { + return nil, t.srcmap.SyntaxErrors(expr.arg, "expected list") + } else if binding, ok := expr.fn.Binding().(FunctionBinding); !ok { + return nil, t.srcmap.SyntaxErrors(expr.arg, "unbound function") + } else { + reduction := list.Args[0] + // Build reduction + for i := 1; i < len(list.Args); i++ { + reduction = binding.Apply([]Expr{reduction, list.Args[i]}) + } + // Translate reduction + return t.translateExpressionInModule(reduction, module, shift) + } +} + func (t *translator) translateShiftInModule(expr *Shift, module string, shift int) (hir.Expr, []SyntaxError) { constant := expr.Shift.AsConstant() // Determine the shift constant diff --git a/pkg/sexp/translator.go b/pkg/sexp/translator.go index 315f3ea1..4d4ed8a3 100644 --- a/pkg/sexp/translator.go +++ b/pkg/sexp/translator.go @@ -98,11 +98,10 @@ func (p *Translator[T]) AddRecursiveListRule(name string, t RecursiveRule[T]) { p.lists[name] = p.createRecursiveListRule(t) } -// AddDefaultRecursiveListRule adds a default recursive rule to be applied when no -// other recursive rules apply. -func (p *Translator[T]) AddDefaultRecursiveListRule(t RecursiveRule[T]) { - // Construct a recursive list translator as a wrapper around a generic list translator. - p.list_default = p.createRecursiveListRule(t) +// AddDefaultListRule adds a default rule to be applied when no other recursive +// rules apply. +func (p *Translator[T]) AddDefaultListRule(rule ListRule[T]) { + p.list_default = rule } // AddDefaultRecursiveArrayRule adds a default recursive rule to be applied when no diff --git a/pkg/test/invalid_corset_test.go b/pkg/test/invalid_corset_test.go index e73d6496..958ba7f3 100644 --- a/pkg/test/invalid_corset_test.go +++ b/pkg/test/invalid_corset_test.go @@ -517,6 +517,30 @@ func Test_Invalid_Array_05(t *testing.T) { CheckInvalid(t, "array_invalid_05") } +// =================================================================== +// Reduce +// =================================================================== + +func Test_Invalid_Reduce_01(t *testing.T) { + CheckInvalid(t, "reduce_invalid_01") +} + +func Test_Invalid_Reduce_02(t *testing.T) { + CheckInvalid(t, "reduce_invalid_02") +} + +func Test_Invalid_Reduce_03(t *testing.T) { + CheckInvalid(t, "reduce_invalid_03") +} + +func Test_Invalid_Reduce_04(t *testing.T) { + CheckInvalid(t, "reduce_invalid_04") +} + +func Test_Invalid_Reduce_05(t *testing.T) { + CheckInvalid(t, "reduce_invalid_05") +} + // =================================================================== // Test Helpers // =================================================================== diff --git a/pkg/test/valid_corset_test.go b/pkg/test/valid_corset_test.go index 72f5991a..2470252f 100644 --- a/pkg/test/valid_corset_test.go +++ b/pkg/test/valid_corset_test.go @@ -166,6 +166,10 @@ func Test_Block_03(t *testing.T) { Check(t, false, "block_03") } +func Test_Block_04(t *testing.T) { + Check(t, false, "block_04") +} + // =================================================================== // Property Tests // =================================================================== @@ -648,15 +652,39 @@ func Test_Array_01(t *testing.T) { Check(t, false, "array_01") } -/* func Test_Array_02(t *testing.T) { - Check(t, false, "array_02") -} +/* + func Test_Array_02(t *testing.T) { + Check(t, false, "array_02") + } */ - func Test_Array_03(t *testing.T) { Check(t, false, "array_03") } +// =================================================================== +// Reduce +// =================================================================== + +func Test_Reduce_01(t *testing.T) { + Check(t, false, "reduce_01") +} + +func Test_Reduce_02(t *testing.T) { + Check(t, false, "reduce_02") +} + +func Test_Reduce_03(t *testing.T) { + Check(t, false, "reduce_03") +} + +func Test_Reduce_04(t *testing.T) { + Check(t, false, "reduce_04") +} + +func Test_Reduce_05(t *testing.T) { + Check(t, false, "reduce_05") +} + // =================================================================== // Complex Tests // =================================================================== diff --git a/testdata/block_04.accepts b/testdata/block_04.accepts new file mode 100644 index 00000000..6090d1a5 --- /dev/null +++ b/testdata/block_04.accepts @@ -0,0 +1,10 @@ +{"X": [], "Y": []} +{"X": [-2], "Y": [-2]} +{"X": [-1], "Y": [-1]} +{"X": [0], "Y": [0]} +{"X": [1], "Y": [1]} +{"X": [2], "Y": [2]} +{"X": [0,0], "Y": [0,0]} +{"X": [0,1], "Y": [0,1]} +{"X": [1,0], "Y": [1,0]} +{"X": [1,1], "Y": [1,1]} diff --git a/testdata/block_04.lisp b/testdata/block_04.lisp new file mode 100644 index 00000000..94be9c1d --- /dev/null +++ b/testdata/block_04.lisp @@ -0,0 +1,4 @@ +(defcolumns (X :@loob) (Y :@loob)) + +(defconstraint c1 () + (begin (- X Y) (- Y X))) diff --git a/testdata/block_04.rejects b/testdata/block_04.rejects new file mode 100644 index 00000000..b2cf1076 --- /dev/null +++ b/testdata/block_04.rejects @@ -0,0 +1,12 @@ +{"X": [1], "Y": [0]} +{"X": [-1], "Y": [0]} +{"X": [-1], "Y": [1]} +{"X": [0], "Y": [1]} +{"X": [0], "Y": [-1]} +{"X": [2], "Y": [-1]} +{"X": [-2], "Y": [1]} +{"X": [-2], "Y": [2]} +{"X": [0], "Y": [-1]} +{"X": [1], "Y": [-1]} +{"X": [0,-1], "Y": [0,1]} +{"X": [0,1], "Y": [0,-1]} diff --git a/testdata/reduce_01.accepts b/testdata/reduce_01.accepts new file mode 100644 index 00000000..7382df9e --- /dev/null +++ b/testdata/reduce_01.accepts @@ -0,0 +1,7 @@ +{"X": [], "Y": []} +{"X": [-1], "Y": [1]} +{"X": [0], "Y": [0]} +{"X": [1], "Y": [-1]} +{"X": [0,-1], "Y": [0,1]} +{"X": [0,0], "Y": [0,0]} +{"X": [0,1], "Y": [0,-1]} diff --git a/testdata/reduce_01.lisp b/testdata/reduce_01.lisp new file mode 100644 index 00000000..9b6e3011 --- /dev/null +++ b/testdata/reduce_01.lisp @@ -0,0 +1,3 @@ +(defcolumns (X :@loob) (Y :@loob)) +(defconstraint c1 () (reduce + (begin X Y))) +(defconstraint c2 () (reduce + (begin Y X))) diff --git a/testdata/reduce_01.rejects b/testdata/reduce_01.rejects new file mode 100644 index 00000000..cc18fc0e --- /dev/null +++ b/testdata/reduce_01.rejects @@ -0,0 +1,6 @@ +{"X": [1], "Y": [0]} +{"X": [-1], "Y": [0]} +{"X": [0], "Y": [1]} +{"X": [0], "Y": [-1]} +{"X": [2], "Y": [-1]} +{"X": [-2], "Y": [1]} diff --git a/testdata/reduce_02.accepts b/testdata/reduce_02.accepts new file mode 100644 index 00000000..6090d1a5 --- /dev/null +++ b/testdata/reduce_02.accepts @@ -0,0 +1,10 @@ +{"X": [], "Y": []} +{"X": [-2], "Y": [-2]} +{"X": [-1], "Y": [-1]} +{"X": [0], "Y": [0]} +{"X": [1], "Y": [1]} +{"X": [2], "Y": [2]} +{"X": [0,0], "Y": [0,0]} +{"X": [0,1], "Y": [0,1]} +{"X": [1,0], "Y": [1,0]} +{"X": [1,1], "Y": [1,1]} diff --git a/testdata/reduce_02.lisp b/testdata/reduce_02.lisp new file mode 100644 index 00000000..751802ba --- /dev/null +++ b/testdata/reduce_02.lisp @@ -0,0 +1,3 @@ +(defcolumns (X :@loob) (Y :@loob)) +(defconstraint c1 () (reduce - (begin X Y))) +(defconstraint c2 () (reduce - (begin Y X))) diff --git a/testdata/reduce_02.rejects b/testdata/reduce_02.rejects new file mode 100644 index 00000000..b2cf1076 --- /dev/null +++ b/testdata/reduce_02.rejects @@ -0,0 +1,12 @@ +{"X": [1], "Y": [0]} +{"X": [-1], "Y": [0]} +{"X": [-1], "Y": [1]} +{"X": [0], "Y": [1]} +{"X": [0], "Y": [-1]} +{"X": [2], "Y": [-1]} +{"X": [-2], "Y": [1]} +{"X": [-2], "Y": [2]} +{"X": [0], "Y": [-1]} +{"X": [1], "Y": [-1]} +{"X": [0,-1], "Y": [0,1]} +{"X": [0,1], "Y": [0,-1]} diff --git a/testdata/reduce_03.accepts b/testdata/reduce_03.accepts new file mode 100644 index 00000000..b1b5af4a --- /dev/null +++ b/testdata/reduce_03.accepts @@ -0,0 +1,11 @@ +{"X": [], "Y": []} +{"X": [-2], "Y": [0]} +{"X": [0], "Y": [-1]} +{"X": [0], "Y": [0]} +{"X": [0], "Y": [1]} +{"X": [1], "Y": [0]} +{"X": [2], "Y": [0]} +{"X": [0,0], "Y": [0,0]} +{"X": [0,1], "Y": [1,0]} +{"X": [1,0], "Y": [0,0]} +{"X": [1,0], "Y": [0,1]} diff --git a/testdata/reduce_03.lisp b/testdata/reduce_03.lisp new file mode 100644 index 00000000..0071b8f2 --- /dev/null +++ b/testdata/reduce_03.lisp @@ -0,0 +1,3 @@ +(defcolumns (X :@loob) (Y :@loob)) +(defconstraint c1 () (reduce * (begin X Y))) +(defconstraint c2 () (reduce * (begin Y X))) diff --git a/testdata/reduce_03.rejects b/testdata/reduce_03.rejects new file mode 100644 index 00000000..ab021427 --- /dev/null +++ b/testdata/reduce_03.rejects @@ -0,0 +1,13 @@ +{"X": [-1], "Y": [-1]} +{"X": [-1], "Y": [-2]} +{"X": [-1], "Y": [1]} +{"X": [1], "Y": [-1]} +{"X": [1], "Y": [-2]} +{"X": [1], "Y": [1]} +{"X": [2], "Y": [1]} +{"X": [2], "Y": [-1]} +{"X": [3], "Y": [-1]} +{"X": [-2], "Y": [1]} +{"X": [-2], "Y": [2]} +{"X": [-1,-1], "Y": [1,1]} +{"X": [1,1], "Y": [1,-1]} diff --git a/testdata/reduce_04.accepts b/testdata/reduce_04.accepts new file mode 100644 index 00000000..d86446db --- /dev/null +++ b/testdata/reduce_04.accepts @@ -0,0 +1,11 @@ +{"X": [], "Y": []} +{"X": [-4], "Y": [2]} +{"X": [-2], "Y": [1]} +{"X": [0], "Y": [0]} +{"X": [2], "Y": [-1]} +{"X": [4], "Y": [-2]} +{"X": [0,-4], "Y": [0,2]} +{"X": [0,-2], "Y": [0,1]} +{"X": [0,0], "Y": [0,0]} +{"X": [0,2], "Y": [0,-1]} +{"X": [0,4], "Y": [0,-2]} diff --git a/testdata/reduce_04.lisp b/testdata/reduce_04.lisp new file mode 100644 index 00000000..1053625d --- /dev/null +++ b/testdata/reduce_04.lisp @@ -0,0 +1,10 @@ +(defcolumns (X :@loob) (Y :@loob)) + +(defconstraint c1 () (reduce + (begin X (* 2 Y)))) +(defconstraint c2 () (reduce + (begin (* 2 Y) X))) +(defconstraint c3 () (reduce + (begin X Y Y))) +(defconstraint c4 () (reduce + (begin Y X Y))) +(defconstraint c5 () (reduce + (begin Y Y X))) +(defconstraint c6 () (reduce + (begin (* 1 X) Y Y))) +(defconstraint c7 () (reduce + (begin Y (* 1 X) Y))) +(defconstraint c8 () (reduce + (begin Y Y (* 1 X)))) diff --git a/testdata/reduce_04.rejects b/testdata/reduce_04.rejects new file mode 100644 index 00000000..c1000148 --- /dev/null +++ b/testdata/reduce_04.rejects @@ -0,0 +1,7 @@ +{"X": [-2], "Y": [-2]} +{"X": [-2], "Y": [-1]} +{"X": [-2], "Y": [0]} +{"X": [-2], "Y": [2]} +{"X": [-2], "Y": [3]} +{"X": [0,1], "Y": [0,1]} +{"X": [-2,1], "Y": [1,1]} diff --git a/testdata/reduce_05.accepts b/testdata/reduce_05.accepts new file mode 100644 index 00000000..7382df9e --- /dev/null +++ b/testdata/reduce_05.accepts @@ -0,0 +1,7 @@ +{"X": [], "Y": []} +{"X": [-1], "Y": [1]} +{"X": [0], "Y": [0]} +{"X": [1], "Y": [-1]} +{"X": [0,-1], "Y": [0,1]} +{"X": [0,0], "Y": [0,0]} +{"X": [0,1], "Y": [0,-1]} diff --git a/testdata/reduce_05.lisp b/testdata/reduce_05.lisp new file mode 100644 index 00000000..dabbe939 --- /dev/null +++ b/testdata/reduce_05.lisp @@ -0,0 +1,3 @@ +(defcolumns (X :@loob) (Y :@loob)) +(defpurefun (op x y) (+ x y)) +(defconstraint c1 () (reduce op (begin X Y))) diff --git a/testdata/reduce_05.rejects b/testdata/reduce_05.rejects new file mode 100644 index 00000000..cc18fc0e --- /dev/null +++ b/testdata/reduce_05.rejects @@ -0,0 +1,6 @@ +{"X": [1], "Y": [0]} +{"X": [-1], "Y": [0]} +{"X": [0], "Y": [1]} +{"X": [0], "Y": [-1]} +{"X": [2], "Y": [-1]} +{"X": [-2], "Y": [1]} diff --git a/testdata/reduce_invalid_01.lisp b/testdata/reduce_invalid_01.lisp new file mode 100644 index 00000000..56142904 --- /dev/null +++ b/testdata/reduce_invalid_01.lisp @@ -0,0 +1,2 @@ +(defcolumns (X :@loob) (Y :@loob)) +(defconstraint c1 () (reduce + (X Y))) diff --git a/testdata/reduce_invalid_02.lisp b/testdata/reduce_invalid_02.lisp new file mode 100644 index 00000000..7bcbf8e1 --- /dev/null +++ b/testdata/reduce_invalid_02.lisp @@ -0,0 +1 @@ +(defconstraint c1 () (reduce +)) diff --git a/testdata/reduce_invalid_03.lisp b/testdata/reduce_invalid_03.lisp new file mode 100644 index 00000000..850b4246 --- /dev/null +++ b/testdata/reduce_invalid_03.lisp @@ -0,0 +1,2 @@ +(defcolumns X Y) +(defconstraint c1 () (reduce + (begin X Y))) diff --git a/testdata/reduce_invalid_04.lisp b/testdata/reduce_invalid_04.lisp new file mode 100644 index 00000000..8e209510 --- /dev/null +++ b/testdata/reduce_invalid_04.lisp @@ -0,0 +1,3 @@ +(defcolumns (X :@loob) (Y :@loob)) +(defpurefun (op x y z) (+ x y z)) +(defconstraint c1 () (reduce op (begin X Y))) diff --git a/testdata/reduce_invalid_05.lisp b/testdata/reduce_invalid_05.lisp new file mode 100644 index 00000000..0e2deb5a --- /dev/null +++ b/testdata/reduce_invalid_05.lisp @@ -0,0 +1,3 @@ +(defcolumns (X :@loob) (Y :@loob)) +(defpurefun (op x) (+ x 1)) +(defconstraint c1 () (reduce op (begin X Y)))