diff --git a/pkg/corset/environment.go b/pkg/corset/environment.go index e4e37e7..fe59287 100644 --- a/pkg/corset/environment.go +++ b/pkg/corset/environment.go @@ -37,7 +37,7 @@ func NewGlobalEnvironment(scope *GlobalScope) GlobalEnvironment { if binding, ok := b.(*ColumnBinding); ok && !binding.computed { binding.AllocateId(columnId) // Increase the column id - columnId++ + columnId += binding.dataType.Width() } } } @@ -47,7 +47,7 @@ func NewGlobalEnvironment(scope *GlobalScope) GlobalEnvironment { if binding, ok := b.(*ColumnBinding); ok && binding.computed { binding.AllocateId(columnId) // Increase the column id - columnId++ + columnId += binding.dataType.Width() } } } diff --git a/pkg/corset/expression.go b/pkg/corset/expression.go index bf45239..7be4a67 100644 --- a/pkg/corset/expression.go +++ b/pkg/corset/expression.go @@ -87,6 +87,106 @@ func (e *Add) Dependencies() []Symbol { return DependenciesOfExpressions(e.Args) } +// ============================================================================ +// ArrayAccess +// ============================================================================ + +// ArrayAccess represents the a given value taken to a power. +type ArrayAccess struct { + name string + arg Expr + binding Binding +} + +// IsQualified determines whether this symbol is qualfied or not (i.e. has an +// explicitly module specifier). +func (e *ArrayAccess) IsQualified() bool { + return false +} + +// IsFunction indicates whether or not this symbol refers to a function (which +// of course it always does). +func (e *ArrayAccess) IsFunction() bool { + return false +} + +// IsResolved checks whether this symbol has been resolved already, or not. +func (e *ArrayAccess) IsResolved() bool { + return e.binding != nil +} + +// AsConstant attempts to evaluate this expression as a constant (signed) value. +// If this expression is not constant, then nil is returned. +func (e *ArrayAccess) AsConstant() *big.Int { + return nil +} + +// Multiplicity determines the number of values that evaluating this expression +// can generate. +func (e *ArrayAccess) Multiplicity() uint { + return determineMultiplicity([]Expr{e.arg}) +} + +// Module returns the module used to qualify this array access. At this time, +// however, array accesses are always unqualified. +func (e *ArrayAccess) Module() string { + panic("unqualified array access") +} + +// Name returns the (unqualified) name of this symbol +func (e *ArrayAccess) Name() string { + return e.name +} + +// Binding gets binding associated with this interface. This will panic if this +// symbol is not yet resolved. +func (e *ArrayAccess) Binding() Binding { + if e.binding == nil { + panic("variable access is unresolved") + } + // + 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 *ArrayAccess) 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 *ArrayAccess) Lisp() sexp.SExp { + panic("todo") +} + +// Substitute all variables (such as for function parameters) arising in +// this expression. +func (e *ArrayAccess) Substitute(mapping map[uint]Expr) Expr { + return &ArrayAccess{e.name, e.arg.Substitute(mapping), e.binding} +} + +// Resolve this symbol by associating it with the binding associated with +// the definition of the symbol to which this refers. +func (e *ArrayAccess) Resolve(binding Binding) bool { + if binding == nil { + panic("empty binding") + } else if e.binding != nil { + panic("already resolved") + } + // + e.binding = binding + // + return true +} + +// Dependencies needed to signal declaration. +func (e *ArrayAccess) Dependencies() []Symbol { + deps := e.arg.Dependencies() + return append(deps, e) +} + // ============================================================================ // Constants // ============================================================================ diff --git a/pkg/corset/parser.go b/pkg/corset/parser.go index 07fb338..7adb10c 100644 --- a/pkg/corset/parser.go +++ b/pkg/corset/parser.go @@ -146,16 +146,17 @@ func NewParser(srcfile *sexp.SourceFile, srcmap *sexp.SourceMap[sexp.SExp]) *Par // Configure expression translator p.AddSymbolRule(constantParserRule) p.AddSymbolRule(varAccessParserRule) - p.AddRecursiveRule("+", addParserRule) - p.AddRecursiveRule("-", subParserRule) - p.AddRecursiveRule("*", mulParserRule) - p.AddRecursiveRule("~", normParserRule) - p.AddRecursiveRule("^", powParserRule) - p.AddRecursiveRule("begin", beginParserRule) + p.AddRecursiveListRule("+", addParserRule) + p.AddRecursiveListRule("-", subParserRule) + p.AddRecursiveListRule("*", mulParserRule) + p.AddRecursiveListRule("~", normParserRule) + p.AddRecursiveListRule("^", powParserRule) + p.AddRecursiveListRule("begin", beginParserRule) p.AddListRule("for", forParserRule(parser)) - p.AddRecursiveRule("if", ifParserRule) - p.AddRecursiveRule("shift", shiftParserRule) - p.AddDefaultRecursiveRule(invokeParserRule) + p.AddRecursiveListRule("if", ifParserRule) + p.AddRecursiveListRule("shift", shiftParserRule) + p.AddDefaultRecursiveListRule(invokeParserRule) + p.AddDefaultRecursiveArrayRule(arrayAccessParserRule) // return parser } @@ -363,29 +364,55 @@ func (p *Parser) parseColumnDeclarationAttributes(attrs []sexp.SExp) (Type, bool var ( dataType Type = NewFieldType() mustProve bool = false + array uint err *SyntaxError ) - for _, attr := range attrs { - symbol := attr.AsSymbol() + for i := 0; i < len(attrs); i++ { + ith := attrs[i] + symbol := ith.AsSymbol() // Sanity check if symbol == nil { - return nil, false, p.translator.SyntaxError(attr, "unknown column attribute") + return nil, false, p.translator.SyntaxError(ith, "unknown column attribute") } // switch symbol.Value { case ":display", ":opcode": // skip these for now, as they are only relevant to the inspector. + case ":array": + if array, err = p.parseArrayDimension(attrs[i+1]); err != nil { + return nil, false, err + } + // skip dimension + i++ default: - if dataType, mustProve, err = p.parseType(attr); err != nil { + if dataType, mustProve, err = p.parseType(ith); err != nil { return nil, false, err } } } // Done + if array != 0 { + return NewArrayType(dataType, array), mustProve, nil + } + // return dataType, mustProve, nil } +func (p *Parser) parseArrayDimension(s sexp.SExp) (uint, *SyntaxError) { + dim := s.AsArray() + // + if dim == nil || dim.Len() != 1 || dim.Get(0).AsSymbol() == nil { + return 0, p.translator.SyntaxError(s, "invalid array dimension") + } + // + if num, ok := strconv.Atoi(dim.Get(0).AsSymbol().Value); ok == nil && num >= 0 { + return uint(num), nil + } + // + return 0, p.translator.SyntaxError(s, "invalid array dimension") +} + // Parse a constant declaration func (p *Parser) parseDefConst(elements []sexp.SExp) (Declaration, []SyntaxError) { var ( @@ -919,34 +946,26 @@ func forParserRule(p *Parser) sexp.ListRule[Expr] { return func(list *sexp.List) (Expr, []SyntaxError) { var ( errors []SyntaxError - n int = list.Len() - 1 - rangeStr string indexVar *sexp.Symbol ) + // Check we've got the expected number + if list.Len() != 4 { + msg := fmt.Sprintf("expected 3 arguments, found %d", list.Len()) + return nil, p.translator.SyntaxErrors(list, msg) + } // Extract index variable if indexVar = list.Get(1).AsSymbol(); indexVar == nil { err := p.translator.SyntaxError(list.Get(1), "invalid index variable") errors = append(errors, *err) } - // Extract range - for i := 2; i < n; i++ { - if ith := list.Get(i).AsSymbol(); ith != nil { - rangeStr = fmt.Sprintf("%s%s", rangeStr, ith.Value) - } else { - err := p.translator.SyntaxError(list.Get(i), "invalid range component") - errors = append(errors, *err) - } - } // Parse range - start, end, ok := parseForRange(rangeStr) + start, end, errs := parseForRange(p, list.Get(2)) // Error Check - if !ok { - errors = append(errors, *p.translator.SyntaxError(list.Get(2), "malformed index range")) - } + errors = append(errors, errs...) // Parse body - body, errs := p.translator.Translate(list.Get(n)) + body, errs := p.translator.Translate(list.Get(3)) errors = append(errors, errs...) - // + // Error check if len(errors) > 0 { return nil, errors } @@ -957,24 +976,30 @@ func forParserRule(p *Parser) sexp.ListRule[Expr] { } } -func parseForRange(rangeStr string) (uint, uint, bool) { +// Parse a range which, represented as a string is "[s:e]". +func parseForRange(p *Parser, interval sexp.SExp) (uint, uint, []SyntaxError) { var ( start int end int err1 error err2 error ) + // This is a bit dirty. Essentially, we turn the sexp.Array back into a + // string and then parse it from there. + str := interval.String(false) + // Strip out any whitespace (which is permitted) + str = strings.ReplaceAll(str, " ", "") // Check has form "[...]" - if !strings.HasPrefix(rangeStr, "[") || !strings.HasSuffix(rangeStr, "]") { + if !strings.HasPrefix(str, "[") || !strings.HasSuffix(str, "]") { // error - return 0, 0, false + return 0, 0, p.translator.SyntaxErrors(interval, "invalid interval") } // Split out components - splits := strings.Split(rangeStr[1:len(rangeStr)-1], ":") + splits := strings.Split(str[1:len(str)-1], ":") // Error check if len(splits) == 0 || len(splits) > 2 { // error - return 0, 0, false + return 0, 0, p.translator.SyntaxErrors(interval, "invalid interval") } else if len(splits) == 1 { start, err1 = strconv.Atoi(splits[0]) end = start @@ -983,7 +1008,11 @@ func parseForRange(rangeStr string) (uint, uint, bool) { end, err2 = strconv.Atoi(splits[1]) } // - return uint(start), uint(end), err1 == nil && err2 == nil + if err1 != nil || err2 != nil { + return 0, 0, p.translator.SyntaxErrors(interval, "invalid interval") + } + // Success + return uint(start), uint(end), nil } func constantParserRule(symbol string) (Expr, bool, error) { @@ -1016,7 +1045,7 @@ func constantParserRule(symbol string) (Expr, bool, error) { func varAccessParserRule(col string) (Expr, bool, error) { // Sanity check what we have if !unicode.IsLetter(rune(col[0])) { - return nil, false, nil + return nil, false, errors.New("malformed column access") } // Handle qualified accesses (where permitted) // Attempt to split column name into module / column pair. @@ -1030,6 +1059,14 @@ func varAccessParserRule(col string) (Expr, bool, error) { } } +func arrayAccessParserRule(name string, args []Expr) (Expr, error) { + if len(args) != 1 { + return nil, errors.New("malformed array access") + } + // + return &ArrayAccess{name, args[0], nil}, nil +} + func addParserRule(_ string, args []Expr) (Expr, error) { return &Add{args}, nil } diff --git a/pkg/corset/resolver.go b/pkg/corset/resolver.go index 7f68df9..d905cfa 100644 --- a/pkg/corset/resolver.go +++ b/pkg/corset/resolver.go @@ -500,7 +500,9 @@ func (r *resolver) finaliseExpressionsInModule(scope LocalScope, args []Expr) ([ // //nolint:staticcheck func (r *resolver) finaliseExpressionInModule(scope LocalScope, expr Expr) (Type, []SyntaxError) { - if v, ok := expr.(*Constant); ok { + if v, ok := expr.(*ArrayAccess); ok { + return r.finaliseArrayAccessInModule(scope, v) + } else if v, ok := expr.(*Constant); ok { nbits := v.Val.BitLen() return NewUintType(uint(nbits)), nil } else if v, ok := expr.(*Add); ok { @@ -542,7 +544,31 @@ func (r *resolver) finaliseExpressionInModule(scope LocalScope, expr Expr) (Type } else if v, ok := expr.(*VariableAccess); ok { return r.finaliseVariableInModule(scope, v) } else { - return nil, r.srcmap.SyntaxErrors(expr, "unknown expression") + return nil, r.srcmap.SyntaxErrors(expr, "unknown expression encountered during resolution") + } +} + +// Resolve a specific array access contained within some expression which, in +// turn, is contained within some module. +func (r *resolver) finaliseArrayAccessInModule(scope LocalScope, expr *ArrayAccess) (Type, []SyntaxError) { + // Resolve argument + if _, errors := r.finaliseExpressionInModule(scope, expr.arg); errors != nil { + return nil, errors + } + // + if !expr.IsResolved() && !scope.Bind(expr) { + return nil, r.srcmap.SyntaxErrors(expr, "unknown array column") + } else if binding, ok := expr.Binding().(*ColumnBinding); !ok { + 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 } } diff --git a/pkg/corset/translator.go b/pkg/corset/translator.go index 41b2fe2..3aa231b 100644 --- a/pkg/corset/translator.go +++ b/pkg/corset/translator.go @@ -93,22 +93,55 @@ func (t *translator) translateDefColumns(decl *DefColumns, module string) []Synt var errors []SyntaxError // Add each column to schema for _, c := range decl.Columns { - context := t.env.ContextFrom(module, c.LengthMultiplier()) - cid := t.schema.AddDataColumn(context, c.Name(), c.DataType().AsUnderlying()) - // Prove type (if requested) - if c.MustProve() { - bound := c.DataType().AsUnderlying().AsUint().Bound() - t.schema.AddRangeConstraint(c.Name(), context, &hir.ColumnAccess{Column: cid, Shift: 0}, bound) - } - // Sanity check column identifier - if info := t.env.Column(module, c.Name()); info.ColumnId() != cid { - errors = append(errors, *t.srcmap.SyntaxError(c, "invalid column identifier")) - } + errs := t.translateDefColumn(c, module) + errors = append(errors, errs...) } // return errors } +// Translate a "defcolumns" declaration. +func (t *translator) translateDefColumn(decl *DefColumn, module string) []SyntaxError { + // Extract base columnd ID + columnId := t.env.Column(module, decl.Name()).cid + // + if arr_t, ok := decl.DataType().(*ArrayType); ok { + var errors []SyntaxError + // Handle array types + for i := uint(1); i <= arr_t.size; i++ { + name := fmt.Sprintf("%s_%d", decl.name, i) + errs := t.translateRawColumn(decl, module, name, arr_t.element.AsUnderlying(), columnId) + errors = append(errors, errs...) + columnId++ + } + // + return errors + } else { + return t.translateRawColumn(decl, module, decl.name, decl.DataType().AsUnderlying(), columnId) + } +} + +func (t *translator) translateRawColumn(decl *DefColumn, module string, name string, + datatype sc.Type, columnId uint) []SyntaxError { + // + context := t.env.ContextFrom(module, decl.LengthMultiplier()) + cid := t.schema.AddDataColumn(context, name, datatype) + // Prove type (if requested) + if decl.MustProve() { + bound := datatype.AsUint().Bound() + t.schema.AddRangeConstraint(name, context, &hir.ColumnAccess{Column: cid, Shift: 0}, bound) + } + // Sanity check column identifier + if columnId != cid { + msg := fmt.Sprintf("invalid column identifier (expected %d got %d)", columnId, cid) + err := t.srcmap.SyntaxError(decl, msg) + // + return []SyntaxError{*err} + } + // + return nil +} + // Translate all assignment or constraint declarations in the circuit. func (t *translator) translateOtherDeclarations(circuit *Circuit) []SyntaxError { errors := t.translateOtherDeclarationsInModule("", circuit.Declarations) @@ -353,7 +386,9 @@ func (t *translator) translateExpressionsInModule(exprs []Expr, module string) ( // necessary to resolve unqualified names (e.g. for column access, function // invocations, etc). func (t *translator) translateExpressionInModule(expr Expr, module string, shift int) (hir.Expr, []SyntaxError) { - if e, ok := expr.(*Constant); ok { + if e, ok := expr.(*ArrayAccess); ok { + return t.translateArrayAccessInModule(e, shift) + } else if e, ok := expr.(*Constant); ok { var val fr.Element // Initialise field from bigint val.SetBigInt(&e.Val) @@ -375,7 +410,7 @@ func (t *translator) translateExpressionInModule(expr Expr, module string, shift return &hir.IfZero{Condition: args[0], TrueBranch: args[2], FalseBranch: args[1]}, errs } // Should be unreachable - return nil, t.srcmap.SyntaxErrors(expr, "unresolved conditional") + return nil, t.srcmap.SyntaxErrors(expr, "unresolved conditional encountered during translation") } else if e, ok := expr.(*Invoke); ok { return t.translateInvokeInModule(e, module, shift) } else if v, ok := expr.(*List); ok { @@ -395,8 +430,33 @@ func (t *translator) translateExpressionInModule(expr Expr, module string, shift } else if e, ok := expr.(*VariableAccess); ok { return t.translateVariableAccessInModule(e, module, shift) } else { - return nil, t.srcmap.SyntaxErrors(expr, "unknown expression") + return nil, t.srcmap.SyntaxErrors(expr, "unknown expression encountered during translation") + } +} + +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")) + } + // Error check + if len(errors) > 0 { + return nil, errors + } + // Lookup underlying column info + info := t.env.Column(binding.module, expr.Name()) + // Update column id (remember indices start from 1) + columnId := info.cid + uint(index.Uint64()) - 1 + // Done + return &hir.ColumnAccess{Column: columnId, Shift: shift}, nil } func (t *translator) translateExpInModule(expr *Exp, module string, shift int) (hir.Expr, []SyntaxError) { diff --git a/pkg/corset/type.go b/pkg/corset/type.go index 813a294..9a7af8b 100644 --- a/pkg/corset/type.go +++ b/pkg/corset/type.go @@ -29,6 +29,10 @@ type Type interface { // this doesn't exist, then nil is returned. AsUnderlying() sc.Type + // Returns the number of underlying columns represented by this column. For + // example, an array of size n will expand into n underlying columns. + Width() uint + // Produce a string representation of this type. String() string } @@ -108,6 +112,10 @@ func LeastUpperBound(lhs Type, rhs Type) Type { return &NativeType{underlying, l_loobean || r_loobean, l_boolean || r_boolean} } +// ============================================================================ +// NativeType +// ============================================================================ + // NativeType simply wraps one of the types available at the HIR level (and below). type NativeType struct { // The underlying type @@ -156,6 +164,12 @@ func (p *NativeType) WithBooleanSemantics() Type { return &NativeType{p.datatype, false, true} } +// Width returns the number of underlying columns represented by this column. +// For example, an array of size n will expand into n underlying columns. +func (p *NativeType) Width() uint { + return 1 +} + // AsUnderlying attempts to convert this type into an underlying type. If this // is not possible, then nil is returned. func (p *NativeType) AsUnderlying() sc.Type { @@ -171,3 +185,64 @@ func (p *NativeType) String() string { // return p.datatype.String() } + +// ============================================================================ +// ArrayType +// ============================================================================ + +// ArrayType represents a statically-sized array of types. +type ArrayType struct { + // element type + element Type + // array size + size uint +} + +// NewArrayType constructs a new array type of a given (fixed) size. +func NewArrayType(element Type, size uint) *ArrayType { + return &ArrayType{element, size} +} + +// HasLoobeanSemantics indicates whether or not this type supports "loobean" +// semantics or not. If so, this means that 0 is treated as true, with anything +// else being false. +func (p *ArrayType) HasLoobeanSemantics() bool { + return false +} + +// HasBooleanSemantics indicates whether or not this type supports "boolean" +// semantics. If so, this means that 0 is treated as false, with anything else +// being true. +func (p *ArrayType) HasBooleanSemantics() bool { + return false +} + +// WithLoobeanSemantics constructs a variant of this type which employs loobean +// semantics. This will panic if the type has already been given boolean +// semantics. +func (p *ArrayType) WithLoobeanSemantics() Type { + panic("unreachable") +} + +// WithBooleanSemantics constructs a variant of this type which employs boolean +// semantics. This will panic if the type has already been given boolean +// semantics. +func (p *ArrayType) WithBooleanSemantics() Type { + panic("unreachable") +} + +// Width returns the number of underlying columns represented by this column. +// For example, an array of size n will expand into n underlying columns. +func (p *ArrayType) Width() uint { + return p.size +} + +// AsUnderlying attempts to convert this type into an underlying type. If this +// is not possible, then nil is returned. +func (p *ArrayType) AsUnderlying() sc.Type { + return nil +} + +func (p *ArrayType) String() string { + return fmt.Sprintf("(%s)[%d]", p.element.String(), p.size) +} diff --git a/pkg/sexp/parser.go b/pkg/sexp/parser.go index 276455c..3ca2f03 100644 --- a/pkg/sexp/parser.go +++ b/pkg/sexp/parser.go @@ -56,6 +56,12 @@ func (p *Parser) Parse() (SExp, *SyntaxError) { } else if len(token) == 1 && token[0] == ')' { p.index-- // backup return nil, p.error("unexpected end-of-list") + } else if len(token) == 1 && token[0] == '}' { + p.index-- // backup + return nil, p.error("unexpected end-of-set") + } else if len(token) == 1 && token[0] == ']' { + p.index-- // backup + return nil, p.error("unexpected end-of-array") } else if len(token) == 1 && token[0] == '(' { elements, err := p.parseSequence(')') // Check for error @@ -72,6 +78,14 @@ func (p *Parser) Parse() (SExp, *SyntaxError) { } // Done term = &Set{elements} + } else if len(token) == 1 && token[0] == '[' { + elements, err := p.parseSequence(']') + // Check for error + if err != nil { + return nil, err + } + // Done + term = &Array{elements} } else { // Must be a symbol term = &Symbol{string(token)} @@ -92,7 +106,7 @@ func (p *Parser) Next() []rune { } // Check what we have switch p.text[p.index] { - case '(', ')', '{', '}': + case '(', ')', '{', '}', '[', ']': // List/set begin / end p.index = p.index + 1 return p.text[p.index-1 : p.index] @@ -131,7 +145,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 == '{' || r == '}' || r == ';' { + if r == '(' || r == ')' || r == '{' || r == '}' || r == '[' || r == ']' || r == ';' { return &r } else if unicode.IsSpace(r) { return p.Lookahead(i + 1) @@ -147,7 +161,7 @@ func (p *Parser) parseSymbol() []rune { for j := p.index; j < i; j++ { c := p.text[j] - if c == ')' || c == '}' || c == ' ' || c == '\n' || c == '\t' { + if c == ')' || c == '}' || c == ']' || c == ' ' || c == '\n' || c == '\t' { i = j break } diff --git a/pkg/sexp/sexp.go b/pkg/sexp/sexp.go index 0a8f1cd..e264590 100644 --- a/pkg/sexp/sexp.go +++ b/pkg/sexp/sexp.go @@ -14,6 +14,9 @@ type SExp interface { // AsSet checks whether this S-Expression is a set and, if // so, returns it. Otherwise, it returns nil. AsSet() *Set + // AsArray checks whether this S-Expression is an array and, if so, returns + // it. Otherwise, it returns nil. + AsArray() *Array // 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 { return &List{elements} } +// AsArray returns the given array. +func (l *List) AsArray() *Array { return nil } + // AsList returns the given list. func (l *List) AsList() *List { return l } @@ -121,6 +127,9 @@ func NewSet(elements []SExp) *Set { return &Set{elements} } +// AsArray returns the given array. +func (l *Set) AsArray() *Array { return nil } + // AsList returns nil for a set. func (l *Set) AsList() *List { return nil } @@ -170,6 +179,9 @@ func NewSymbol(value string) *Symbol { return &Symbol{value} } +// AsArray returns the given array. +func (s *Symbol) AsArray() *Array { return nil } + // AsList returns nil for a symbol. func (s *Symbol) AsList() *List { return nil } @@ -201,3 +213,55 @@ func (s *Symbol) String(quote bool) string { func isSymbolLetter(r rune) bool { return r != '(' && r != ')' && !unicode.IsSpace(r) } + +// =================================================================== +// Array +// =================================================================== + +// Array represents a list of zero or more S-Expressions. +type Array struct { + Elements []SExp +} + +// NOTE: This is used for compile time type checking if the given type +// satisfies the given interface. +var _ SExp = (*Array)(nil) + +// NewArray creates a new Array from a given array of S-Expressions. +func NewArray(elements []SExp) *Array { + return &Array{elements} +} + +// AsArray returns the given array. +func (a *Array) AsArray() *Array { return a } + +// AsList returns nil for a Array. +func (a *Array) AsList() *List { return nil } + +// AsSet returns the given Array. +func (a *Array) AsSet() *Set { return nil } + +// AsSymbol returns nil for a Array. +func (a *Array) AsSymbol() *Symbol { return nil } + +// Len gets the number of elements in this Array. +func (a *Array) Len() int { return len(a.Elements) } + +// Get the ith element of this Array +func (a *Array) Get(i int) SExp { return a.Elements[i] } + +func (a *Array) String(quote bool) string { + var s = "[" + + for i := 0; i < len(a.Elements); i++ { + if i != 0 { + s += " " + } + + s += a.Elements[i].String(quote) + } + + s += "]" + + return s +} diff --git a/pkg/sexp/translator.go b/pkg/sexp/translator.go index 6a2d5b9..315f3ea 100644 --- a/pkg/sexp/translator.go +++ b/pkg/sexp/translator.go @@ -13,6 +13,11 @@ type SymbolRule[T comparable] func(string) (T, bool, error) // form. type ListRule[T comparable] func(*List) (T, []SyntaxError) +// ArrayRule is an array translator which is responsible converting an array +// with a given sequence of zero or more arguments into an expression type T. +// Observe that the arguments are already translated into the correct form. +type ArrayRule[T comparable] func(*Array) (T, []SyntaxError) + // BinaryRule is a binary translator is a wrapper for translating lists which must // have exactly two symbol arguments. The wrapper takes care of // ensuring sufficient arguments are given, etc. @@ -35,6 +40,10 @@ type Translator[T comparable] struct { lists map[string]ListRule[T] // Fallback rule for generic user-defined lists. list_default ListRule[T] + // Rules for parsing arrays + arrays map[string]ArrayRule[T] + // Fallback rule for generic user-defined arrays. + array_default ArrayRule[T] // Rules for parsing symbols symbols []SymbolRule[T] // Maps S-Expressions to their spans in the original source file. This is @@ -48,12 +57,13 @@ type Translator[T comparable] struct { // NewTranslator constructs a new Translator instance. func NewTranslator[T comparable](srcfile *SourceFile, srcmap *SourceMap[SExp]) *Translator[T] { return &Translator[T]{ - srcfile: srcfile, - lists: make(map[string]ListRule[T]), - list_default: nil, - symbols: make([]SymbolRule[T], 0), - old_srcmap: srcmap, - new_srcmap: NewSourceMap[T](srcmap.srcfile), + srcfile: srcfile, + lists: make(map[string]ListRule[T]), + list_default: nil, + array_default: nil, + symbols: make([]SymbolRule[T], 0), + old_srcmap: srcmap, + new_srcmap: NewSourceMap[T](srcmap.srcfile), } } @@ -82,20 +92,27 @@ func (p *Translator[T]) AddListRule(name string, rule ListRule[T]) { p.lists[name] = rule } -// AddRecursiveRule adds a new list translator to this expression translator. -func (p *Translator[T]) AddRecursiveRule(name string, t RecursiveRule[T]) { +// AddRecursiveListRule adds a new list translator to this expression translator. +func (p *Translator[T]) AddRecursiveListRule(name string, t RecursiveRule[T]) { + // Construct a recursive list translator as a wrapper around a generic list translator. + 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.lists[name] = p.createRecursiveRule(t) + p.list_default = p.createRecursiveListRule(t) } -// AddDefaultRecursiveRule adds a default recursive rule to be applied when no +// AddDefaultRecursiveArrayRule adds a default recursive rule to be applied when no // other recursive rules apply. -func (p *Translator[T]) AddDefaultRecursiveRule(t RecursiveRule[T]) { +func (p *Translator[T]) AddDefaultRecursiveArrayRule(t RecursiveRule[T]) { // Construct a recursive list translator as a wrapper around a generic list translator. - p.list_default = p.createRecursiveRule(t) + p.array_default = p.createRecursiveArrayRule(t) } -func (p *Translator[T]) createRecursiveRule(t RecursiveRule[T]) ListRule[T] { +func (p *Translator[T]) createRecursiveListRule(t RecursiveRule[T]) ListRule[T] { // Construct a recursive list translator as a wrapper around a generic list translator. return func(l *List) (T, []SyntaxError) { var ( @@ -131,6 +148,42 @@ func (p *Translator[T]) createRecursiveRule(t RecursiveRule[T]) ListRule[T] { } } +func (p *Translator[T]) createRecursiveArrayRule(t RecursiveRule[T]) ArrayRule[T] { + // Construct a recursive list translator as a wrapper around a generic list translator. + return func(l *Array) (T, []SyntaxError) { + var ( + empty T + errors []SyntaxError + ) + // Extract the "head" of the list. + if len(l.Elements) == 0 || l.Elements[0].AsSymbol() == nil { + return empty, p.SyntaxErrors(l, "invalid array") + } + // Extract expression name + head := (l.Elements[0].(*Symbol)).Value + // Translate arguments + args := make([]T, len(l.Elements)-1) + // + for i, s := range l.Elements[1:] { + var errs []SyntaxError + args[i], errs = translateSExp(p, s) + errors = append(errors, errs...) + } + // Apply constructor + term, err := t(head, args) + // Check error + if err != nil { + errors = append(errors, *p.SyntaxError(l, err.Error())) + } + // Check for error + if len(errors) == 0 { + return term, nil + } + // Error case + return empty, errors + } +} + // AddBinaryRule . func (p *Translator[T]) AddBinaryRule(name string, t BinaryRule[T]) { var empty T @@ -196,6 +249,8 @@ func translateSExp[T comparable](p *Translator[T], s SExp) (T, []SyntaxError) { switch e := s.(type) { case *List: return translateSExpList[T](p, e) + case *Array: + return translateSExpArray[T](p, e) case *Symbol: for i := 0; i != len(p.symbols); i++ { node, ok, err := (p.symbols[i])(e.Value) @@ -256,6 +311,48 @@ func translateSExpList[T comparable](p *Translator[T], l *List) (T, []SyntaxErro return node, errors } +// Translate an array of S-Expressions into a unary, binary or n-ary +// expression of some kind. This type of expression is determined by +// the first element of the list. The remaining elements are treated +// as arguments which are first recursively translated. +func translateSExpArray[T comparable](p *Translator[T], l *Array) (T, []SyntaxError) { + var ( + empty T + node T + errors []SyntaxError + ) + // Sanity check this list makes sense + if len(l.Elements) == 0 || l.Elements[0].AsSymbol() == nil { + return empty, p.SyntaxErrors(l, "invalid array") + } + // Extract expression name + name := (l.Elements[0].(*Symbol)).Value + // Lookup appropriate translator + t := p.arrays[name] + // Check whether we found one. + if t != nil { + node, errors = (t)(l) + } else if p.list_default != nil { + node, err := (p.array_default)(l) + // Update source mapping + if err == nil { + map2sexp(p, node, l) + } + // Done + return node, err + } else { + // Default fall back + return empty, p.SyntaxErrors(l, "unknown array encountered") + } + // Map source node + if len(errors) == 0 { + // Update source mapping + map2sexp(p, node, l) + } + // Done + return node, errors +} + // Add a mapping from a given item to the S-expression from which it was // generated. This updates the underlying source map to reflect this. func map2sexp[T comparable](p *Translator[T], item T, sexp SExp) { diff --git a/pkg/test/invalid_corset_test.go b/pkg/test/invalid_corset_test.go index 3b10b91..e73d649 100644 --- a/pkg/test/invalid_corset_test.go +++ b/pkg/test/invalid_corset_test.go @@ -494,6 +494,29 @@ func Test_Invalid_For_03(t *testing.T) { CheckInvalid(t, "for_invalid_03") } +// =================================================================== +// Arrays +// =================================================================== +func Test_Invalid_Array_01(t *testing.T) { + CheckInvalid(t, "array_invalid_01") +} + +func Test_Invalid_Array_02(t *testing.T) { + CheckInvalid(t, "array_invalid_02") +} + +func Test_Invalid_Array_03(t *testing.T) { + CheckInvalid(t, "array_invalid_03") +} + +func Test_Invalid_Array_04(t *testing.T) { + CheckInvalid(t, "array_invalid_04") +} + +func Test_Invalid_Array_05(t *testing.T) { + CheckInvalid(t, "array_invalid_05") +} + // =================================================================== // Test Helpers // =================================================================== diff --git a/pkg/test/valid_corset_test.go b/pkg/test/valid_corset_test.go index 53a730b..72f5991 100644 --- a/pkg/test/valid_corset_test.go +++ b/pkg/test/valid_corset_test.go @@ -640,6 +640,23 @@ func Test_For_03(t *testing.T) { Check(t, false, "for_03") } +// =================================================================== +// Arrays +// =================================================================== + +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_03(t *testing.T) { + Check(t, false, "array_03") +} + // =================================================================== // Complex Tests // =================================================================== diff --git a/testdata/array_01.accepts b/testdata/array_01.accepts new file mode 100644 index 0000000..3df73f5 --- /dev/null +++ b/testdata/array_01.accepts @@ -0,0 +1,18 @@ +{ "ARG": [], "BIT_4": [], "BIT_3": [], "BIT_2": [], "BIT_1": [] } +;; +{ "ARG": [0], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [1], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [2], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [3], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [4], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [5], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [6], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [7], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [8], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [9], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [10], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [11], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [12], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [13], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [14], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [15], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } diff --git a/testdata/array_01.lisp b/testdata/array_01.lisp new file mode 100644 index 0000000..9ed97ca --- /dev/null +++ b/testdata/array_01.lisp @@ -0,0 +1,11 @@ +(defcolumns + (BIT :binary@prove :array [4]) + (ARG :i16@loob)) + +(defconstraint bits () + (- ARG + (+ + (* 1 [BIT 1]) + (* 2 [BIT 2]) + (* 4 [BIT 3]) + (* 8 [BIT 4])))) diff --git a/testdata/array_01.rejects b/testdata/array_01.rejects new file mode 100644 index 0000000..ff824cd --- /dev/null +++ b/testdata/array_01.rejects @@ -0,0 +1,256 @@ +;; x=0 +{ "ARG": [0], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [0], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [0], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [0], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [0], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [0], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [0], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [0], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [0], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [0], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [0], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [0], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [0], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [0], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [0], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=1 +{ "ARG": [1], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [1], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [1], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [1], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [1], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [1], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [1], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [1], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [1], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [1], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [1], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [1], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [1], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [1], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [1], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=2 +{ "ARG": [2], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [2], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [2], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [2], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [2], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [2], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [2], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [2], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [2], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [2], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [2], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [2], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [2], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [2], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [2], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=3 +{ "ARG": [3], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [3], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [3], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [3], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [3], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [3], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [3], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [3], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [3], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [3], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [3], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [3], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [3], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [3], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [3], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=4 +{ "ARG": [4], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [4], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [4], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [4], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [4], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [4], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [4], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [4], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [4], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [4], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [4], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [4], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [4], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [4], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [4], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=5 +{ "ARG": [5], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [5], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [5], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [5], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [5], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [5], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [5], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [5], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [5], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [5], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [5], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [5], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [5], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [5], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [5], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=6 +{ "ARG": [6], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [6], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [6], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [6], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [6], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [6], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [6], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [6], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [6], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [6], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [6], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [6], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [6], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [6], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [6], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=7 +{ "ARG": [7], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [7], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [7], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [7], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [7], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [7], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [7], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [7], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [7], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [7], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [7], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [7], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [7], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [7], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [7], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=8 +{ "ARG": [8], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [8], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [8], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [8], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [8], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [8], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [8], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [8], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [8], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [8], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [8], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [8], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [8], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [8], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [8], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=9 +{ "ARG": [9], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [9], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [9], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [9], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [9], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [9], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [9], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [9], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [9], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [9], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [9], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [9], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [9], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [9], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [9], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=10 +{ "ARG": [10], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [10], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [10], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [10], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [10], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [10], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [10], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [10], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [10], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [10], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [10], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [10], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [10], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [10], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [10], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=11 +{ "ARG": [11], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [11], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [11], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [11], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [11], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [11], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [11], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [11], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [11], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [11], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [11], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [11], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [11], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [11], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [11], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=12 +{ "ARG": [12], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [12], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [12], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [12], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [12], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [12], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [12], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [12], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [12], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [12], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [12], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [12], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [12], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [12], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [12], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=13 +{ "ARG": [13], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [13], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [13], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [13], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [13], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [13], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [13], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [13], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [13], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [13], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [13], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [13], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [13], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [13], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [13], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=14 +{ "ARG": [14], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [14], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [14], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [14], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [14], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [14], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [14], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [14], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [14], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [14], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [14], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [14], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [14], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [14], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [14], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=15 +{ "ARG": [15], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [15], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [15], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [15], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [15], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [15], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [15], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [15], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [15], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [15], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [15], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [15], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [15], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [15], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [15], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } diff --git a/testdata/array_02.accepts b/testdata/array_02.accepts new file mode 100644 index 0000000..3df73f5 --- /dev/null +++ b/testdata/array_02.accepts @@ -0,0 +1,18 @@ +{ "ARG": [], "BIT_4": [], "BIT_3": [], "BIT_2": [], "BIT_1": [] } +;; +{ "ARG": [0], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [1], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [2], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [3], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [4], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [5], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [6], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [7], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [8], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [9], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [10], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [11], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [12], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [13], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [14], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [15], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } diff --git a/testdata/array_02.lisp b/testdata/array_02.lisp new file mode 100644 index 0000000..d319048 --- /dev/null +++ b/testdata/array_02.lisp @@ -0,0 +1,8 @@ +(defcolumns + (BIT :binary@prove :array [4]) + (ARG :i16@loob)) + +(defconstraint bits () + (- ARG + (reduce + + (for i [0:3] (* (^ 2 i) [BIT (+ 1 i)]))))) diff --git a/testdata/array_02.rejects b/testdata/array_02.rejects new file mode 100644 index 0000000..ff824cd --- /dev/null +++ b/testdata/array_02.rejects @@ -0,0 +1,256 @@ +;; x=0 +{ "ARG": [0], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [0], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [0], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [0], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [0], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [0], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [0], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [0], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [0], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [0], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [0], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [0], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [0], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [0], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [0], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=1 +{ "ARG": [1], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [1], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [1], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [1], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [1], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [1], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [1], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [1], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [1], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [1], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [1], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [1], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [1], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [1], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [1], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=2 +{ "ARG": [2], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [2], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [2], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [2], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [2], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [2], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [2], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [2], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [2], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [2], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [2], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [2], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [2], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [2], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [2], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=3 +{ "ARG": [3], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [3], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [3], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [3], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [3], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [3], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [3], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [3], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [3], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [3], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [3], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [3], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [3], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [3], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [3], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=4 +{ "ARG": [4], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [4], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [4], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [4], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [4], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [4], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [4], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [4], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [4], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [4], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [4], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [4], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [4], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [4], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [4], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=5 +{ "ARG": [5], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [5], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [5], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [5], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [5], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [5], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [5], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [5], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [5], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [5], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [5], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [5], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [5], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [5], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [5], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=6 +{ "ARG": [6], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [6], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [6], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [6], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [6], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [6], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [6], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [6], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [6], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [6], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [6], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [6], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [6], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [6], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [6], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=7 +{ "ARG": [7], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [7], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [7], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [7], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [7], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [7], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [7], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [7], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [7], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [7], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [7], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [7], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [7], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [7], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [7], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=8 +{ "ARG": [8], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [8], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [8], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [8], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [8], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [8], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [8], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [8], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [8], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [8], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [8], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [8], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [8], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [8], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [8], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=9 +{ "ARG": [9], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [9], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [9], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [9], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [9], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [9], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [9], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [9], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [9], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [9], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [9], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [9], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [9], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [9], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [9], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=10 +{ "ARG": [10], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [10], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [10], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [10], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [10], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [10], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [10], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [10], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [10], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [10], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [10], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [10], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [10], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [10], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [10], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=11 +{ "ARG": [11], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [11], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [11], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [11], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [11], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [11], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [11], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [11], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [11], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [11], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [11], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [11], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [11], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [11], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [11], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=12 +{ "ARG": [12], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [12], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [12], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [12], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [12], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [12], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [12], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [12], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [12], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [12], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [12], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [12], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [12], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [12], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [12], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=13 +{ "ARG": [13], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [13], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [13], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [13], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [13], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [13], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [13], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [13], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [13], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [13], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [13], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [13], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [13], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [13], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [13], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=14 +{ "ARG": [14], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [14], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [14], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [14], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [14], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [14], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [14], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [14], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [14], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [14], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [14], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [14], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [14], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [14], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [14], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +;; x=15 +{ "ARG": [15], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [15], "BIT_4": [0], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [15], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [15], "BIT_4": [0], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [15], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [15], "BIT_4": [0], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [15], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [15], "BIT_4": [0], "BIT_3": [1], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [15], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [15], "BIT_4": [1], "BIT_3": [0], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [15], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [0] } +{ "ARG": [15], "BIT_4": [1], "BIT_3": [0], "BIT_2": [1], "BIT_1": [1] } +{ "ARG": [15], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [0] } +{ "ARG": [15], "BIT_4": [1], "BIT_3": [1], "BIT_2": [0], "BIT_1": [1] } +{ "ARG": [15], "BIT_4": [1], "BIT_3": [1], "BIT_2": [1], "BIT_1": [0] } diff --git a/testdata/array_03.accepts b/testdata/array_03.accepts new file mode 100644 index 0000000..801a8c1 --- /dev/null +++ b/testdata/array_03.accepts @@ -0,0 +1,7 @@ +{"ARR_1": [], "ARR_2": []} +{"ARR_1": [-1], "ARR_2": [1]} +{"ARR_1": [0], "ARR_2": [0]} +{"ARR_1": [1], "ARR_2": [-1]} +{"ARR_1": [0,-1], "ARR_2": [0,1]} +{"ARR_1": [0,0], "ARR_2": [0,0]} +{"ARR_1": [0,1], "ARR_2": [0,-1]} diff --git a/testdata/array_03.lisp b/testdata/array_03.lisp new file mode 100644 index 0000000..4fadec0 --- /dev/null +++ b/testdata/array_03.lisp @@ -0,0 +1,3 @@ +(defcolumns (ARR :@loob :array [2])) +(defconstraint c1 () (+ [ARR 1] [ARR 2])) +(defconstraint c2 () (+ [ARR 2] [ARR 1])) diff --git a/testdata/array_03.rejects b/testdata/array_03.rejects new file mode 100644 index 0000000..0acce1a --- /dev/null +++ b/testdata/array_03.rejects @@ -0,0 +1,6 @@ +{"ARR_1": [1], "ARR_2": [0]} +{"ARR_1": [-1], "ARR_2": [0]} +{"ARR_1": [0], "ARR_2": [1]} +{"ARR_1": [0], "ARR_2": [-1]} +{"ARR_1": [2], "ARR_2": [-1]} +{"ARR_1": [-2], "ARR_2": [1]} diff --git a/testdata/array_invalid_01.lisp b/testdata/array_invalid_01.lisp new file mode 100644 index 0000000..50456c3 --- /dev/null +++ b/testdata/array_invalid_01.lisp @@ -0,0 +1,4 @@ +;;error:4:24-30:not an array column +(defcolumns (BIT :@loob)) + +(defconstraint bits () [BIT 1]) diff --git a/testdata/array_invalid_02.lisp b/testdata/array_invalid_02.lisp new file mode 100644 index 0000000..58137e9 --- /dev/null +++ b/testdata/array_invalid_02.lisp @@ -0,0 +1,4 @@ +;;error:4:24-25:expected loobean constraint (found (𝔽@loob)[4]) +(defcolumns (BIT :@loob :array [4])) + +(defconstraint bits () BIT) diff --git a/testdata/array_invalid_03.lisp b/testdata/array_invalid_03.lisp new file mode 100644 index 0000000..0c04221 --- /dev/null +++ b/testdata/array_invalid_03.lisp @@ -0,0 +1,4 @@ +;;error:4:24-30:expected constant array index +(defcolumns X (BIT :@loob :array [4])) + +(defconstraint bits () [BIT X]) diff --git a/testdata/array_invalid_04.lisp b/testdata/array_invalid_04.lisp new file mode 100644 index 0000000..b2169e5 --- /dev/null +++ b/testdata/array_invalid_04.lisp @@ -0,0 +1,12 @@ +;;error:12:12-18:out-of-bounds array access +(defcolumns + (BIT :binary@prove :array [3]) + (ARG :i16@loob)) + +(defconstraint bits () + (- ARG + (+ + (* 1 [BIT 1]) + (* 2 [BIT 2]) + (* 4 [BIT 3]) + (* 8 [BIT 4])))) diff --git a/testdata/array_invalid_05.lisp b/testdata/array_invalid_05.lisp new file mode 100644 index 0000000..4518bbc --- /dev/null +++ b/testdata/array_invalid_05.lisp @@ -0,0 +1,12 @@ +;;error:12:12-18:out-of-bounds array access +(defcolumns + (BIT :binary@prove :array [4]) + (ARG :i16@loob)) + +(defconstraint bits () + (- ARG + (+ + (* 1 [BIT 0]) + (* 2 [BIT 1]) + (* 4 [BIT 2]) + (* 8 [BIT 3]))))