Documentation
¶
Overview ¶
Copyright Consensys Software Inc.
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.
SPDX-License-Identifier: Apache-2.0
Copyright Consensys Software Inc.
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.
SPDX-License-Identifier: Apache-2.0
Copyright Consensys Software Inc.
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.
SPDX-License-Identifier: Apache-2.0
Copyright Consensys Software Inc.
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.
SPDX-License-Identifier: Apache-2.0
Copyright Consensys Software Inc.
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.
SPDX-License-Identifier: Apache-2.0
Copyright Consensys Software Inc.
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.
SPDX-License-Identifier: Apache-2.0
Index ¶
- Constants
- Variables
- func AsConstantOfExpressions(exprs []Expr, fn func(*big.Int, *big.Int)) *big.Int
- func ListOfExpressions[E Expr](head sexp.SExp, exprs []E) *sexp.List
- type Add
- type AnyType
- type ArrayAccess
- func (e *ArrayAccess) Arity() util.Option[uint]
- func (e *ArrayAccess) AsConstant() *big.Int
- func (e *ArrayAccess) Binding() Binding
- func (e *ArrayAccess) Context() Context
- func (e *ArrayAccess) Dependencies() []Symbol
- func (e *ArrayAccess) IsResolved() bool
- func (e *ArrayAccess) Lisp() sexp.SExp
- func (e *ArrayAccess) Path() *file.Path
- func (e *ArrayAccess) Resolve(binding Binding) bool
- func (e *ArrayAccess) Type() Type
- type ArrayType
- func (p *ArrayType) Element() Type
- func (p *ArrayType) HasUnderlying() bool
- func (p *ArrayType) LeastUpperBound(other Type) Type
- func (p *ArrayType) MaxIndex() uint
- func (p *ArrayType) MinIndex() uint
- func (p *ArrayType) String() string
- func (p *ArrayType) SubtypeOf(other Type) bool
- func (p *ArrayType) Width() uint
- type Binding
- type BoolType
- type Cast
- type Circuit
- type ColumnBinding
- type Concat
- type Connective
- type Constant
- type ConstantBinding
- type Context
- func (p Context) IsConflicted() bool
- func (p Context) IsVoid() bool
- func (p Context) Join(other Context) Context
- func (p Context) LengthMultiplier() uint
- func (p Context) Module() string
- func (p Context) ModuleName() module.Name
- func (p Context) Multiply(factor uint) Context
- func (p Context) String() string
- type Debug
- type Declaration
- type DefAlias
- type DefAliases
- type DefCall
- type DefColumn
- func (e *DefColumn) Arity() util.Option[uint]
- func (e *DefColumn) Binding() Binding
- func (e *DefColumn) DataType() Type
- func (e *DefColumn) InnerBinding() ColumnBinding
- func (e *DefColumn) LengthMultiplier() uint
- func (e *DefColumn) Lisp() sexp.SExp
- func (e *DefColumn) MustProve() bool
- func (e *DefColumn) Name() string
- func (e *DefColumn) Path() *file.Path
- type DefColumns
- type DefComputed
- type DefComputedColumn
- func (p *DefComputedColumn) Defines(symbol Symbol) bool
- func (p *DefComputedColumn) Definitions() iter.Iterator[SymbolDefinition]
- func (p *DefComputedColumn) Dependencies() iter.Iterator[Symbol]
- func (p *DefComputedColumn) Finalise()
- func (p *DefComputedColumn) IsFinalised() bool
- func (p *DefComputedColumn) Lisp() sexp.SExp
- type DefConst
- type DefConstUnit
- type DefConstraint
- func (p *DefConstraint) Defines(symbol Symbol) bool
- func (p *DefConstraint) Definitions() iter.Iterator[SymbolDefinition]
- func (p *DefConstraint) Dependencies() iter.Iterator[Symbol]
- func (p *DefConstraint) Finalise()
- func (p *DefConstraint) IsFinalised() bool
- func (p *DefConstraint) Lisp() sexp.SExp
- type DefFun
- func (p *DefFun) Arity() util.Option[uint]
- func (p *DefFun) Binding() Binding
- func (p *DefFun) Body() Expr
- func (p *DefFun) Defines(symbol Symbol) bool
- func (p *DefFun) Definitions() iter.Iterator[SymbolDefinition]
- func (p *DefFun) Dependencies() iter.Iterator[Symbol]
- func (p *DefFun) Finalise()
- func (p *DefFun) IsFinalised() bool
- func (p *DefFun) IsPure() bool
- func (p *DefFun) Lisp() sexp.SExp
- func (p *DefFun) Name() string
- func (p *DefFun) Parameters() []*DefParameter
- func (p *DefFun) Path() *file.Path
- func (p *DefFun) Return() Type
- type DefInRange
- type DefInterleaved
- func (p *DefInterleaved) Defines(symbol Symbol) bool
- func (p *DefInterleaved) Definitions() iter.Iterator[SymbolDefinition]
- func (p *DefInterleaved) Dependencies() iter.Iterator[Symbol]
- func (p *DefInterleaved) Finalise()
- func (p *DefInterleaved) IsFinalised() bool
- func (p *DefInterleaved) Lisp() sexp.SExp
- type DefLookup
- type DefParameter
- type DefPermutation
- type DefPerspective
- func (p *DefPerspective) Arity() util.Option[uint]
- func (p *DefPerspective) Binding() Binding
- func (p *DefPerspective) Defines(symbol Symbol) bool
- func (p *DefPerspective) Definitions() iter.Iterator[SymbolDefinition]
- func (p *DefPerspective) Dependencies() iter.Iterator[Symbol]
- func (p *DefPerspective) Finalise()
- func (p *DefPerspective) IsFinalised() bool
- func (p *DefPerspective) Lisp() sexp.SExp
- func (p *DefPerspective) Name() string
- func (p *DefPerspective) Path() *file.Path
- type DefProperty
- type DefSorted
- type DefunBinding
- type Equation
- type Exp
- type Expr
- type For
- type FunctionBinding
- type FunctionName
- type FunctionSignature
- type If
- type IntType
- type Invoke
- type Let
- type List
- type LocalVariableBinding
- type Module
- type Mul
- type Name
- func (e *Name[T]) Arity() util.Option[uint]
- func (e *Name[T]) Binding() Binding
- func (e *Name[T]) InnerBinding() T
- func (e *Name[T]) IsResolved() bool
- func (e *Name[T]) Lisp() sexp.SExp
- func (e *Name[T]) Name() string
- func (e *Name[T]) Path() *file.Path
- func (e *Name[T]) Resolve(binding Binding) bool
- type Node
- type Normalise
- type Not
- type PerspectiveBinding
- type PerspectiveName
- type Reduce
- type Shift
- type Sub
- type Symbol
- type SymbolDefinition
- type Type
- type TypedSymbol
- type VariableAccess
- func (e *VariableAccess) Arity() util.Option[uint]
- func (e *VariableAccess) AsConstant() *big.Int
- func (e *VariableAccess) Binding() Binding
- func (e *VariableAccess) Context() Context
- func (e *VariableAccess) Dependencies() []Symbol
- func (e *VariableAccess) IsResolved() bool
- func (e *VariableAccess) Lisp() sexp.SExp
- func (e *VariableAccess) Path() *file.Path
- func (e *VariableAccess) Resolve(binding Binding) bool
- func (e *VariableAccess) Type() Type
Constants ¶
const ( // NOT_COMPUTED signals a column is not a computed column. NOT_COMPUTED = 0 // COMPUTED signals a column is a (non-recursive) computed column. COMPUTED = 1 // COMPUTED_FWD signals a column is a (forward recursive) computed column. // This means its value is computed starting from the first row (hence it // cannot use a forward shift in its declaration). COMPUTED_FWD = 2 // COMPUTED_BWD signals a column is a (backward recursive) computed column. // This means its value is computed starting from the last row (hence it // cannot use a backward shift in its declaration). COMPUTED_BWD = 3 )
const ( // EQUALS indicates an equals (==) relationship EQUALS uint8 = 0 // NOT_EQUALS indicates a not-equals (!=) relationship NOT_EQUALS uint8 = 1 )
Variables ¶
var BOOL_TYPE = &BoolType{}
BOOL_TYPE provides a convenient singleone to use instead of creating a fresh boolean type, etc.
NON_FUNCTION is used to signal a symbol which does not represent a function.
var UINT_TYPE = &IntType{math.INFINITY}
UINT_TYPE represents the infinite integer range. This cannot be translated into a concrete type at the lower level, and therefore can only be used internally (e.g. for type checking).
Functions ¶
func AsConstantOfExpressions ¶
AsConstantOfExpressions attempts to fold one or more expressions across a given operation (e.g. add, subtract, etc) to produce a constant value. If any of the expressions are not themselves constant, then neither is the result.
Types ¶
type Add ¶
type Add struct{ Args []Expr }
Add represents the sum over zero or more expressions.
func (*Add) AsConstant ¶
AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.
func (*Add) Context ¶
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 (*Add) Dependencies ¶
Dependencies needed to signal declaration.
type AnyType ¶
type AnyType struct{}
AnyType represents the top of the type lattice. This is the type into which values of any other type can flow.
func (*AnyType) HasUnderlying ¶
HasUnderlying determines whether or not this type has an underlying representation, or not.
func (*AnyType) LeastUpperBound ¶
LeastUpperBound computes the least upper bound of this type and another. This is smallest type which contains both of the arguments. For example, i32 is the least upper bound of i1 and i32, etc. If no such type exists, then nil is returned.
type ArrayAccess ¶
ArrayAccess represents the a given value taken to a power.
func (*ArrayAccess) Arity ¶
func (e *ArrayAccess) Arity() util.Option[uint]
Arity indicates whether or not this is a function and, if so, what arity (i.e. how many arguments) the function has.
func (*ArrayAccess) AsConstant ¶
func (e *ArrayAccess) AsConstant() *big.Int
AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.
func (*ArrayAccess) Binding ¶
func (e *ArrayAccess) Binding() Binding
Binding gets binding associated with this interface. This will panic if this symbol is not yet resolved.
func (*ArrayAccess) Context ¶
func (e *ArrayAccess) Context() Context
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 (*ArrayAccess) Dependencies ¶
func (e *ArrayAccess) Dependencies() []Symbol
Dependencies needed to signal declaration.
func (*ArrayAccess) IsResolved ¶
func (e *ArrayAccess) IsResolved() bool
IsResolved checks whether this symbol has been resolved already, or not.
func (*ArrayAccess) Lisp ¶
func (e *ArrayAccess) Lisp() sexp.SExp
Lisp converts this schema element into a simple S-Expression, for example so it can be printed.
func (*ArrayAccess) Path ¶
func (e *ArrayAccess) Path() *file.Path
Path returns the given path of this symbol.
func (*ArrayAccess) Resolve ¶
func (e *ArrayAccess) Resolve(binding Binding) bool
Resolve this symbol by associating it with the binding associated with the definition of the symbol to which this refers.
func (*ArrayAccess) Type ¶
func (e *ArrayAccess) Type() Type
Type returns the type associated with this symbol. If the type cannot be determined, then nil is returned.
type ArrayType ¶
type ArrayType struct {
// contains filtered or unexported fields
}
ArrayType represents a statically-sized array of types.
func NewArrayType ¶
NewArrayType constructs a new array type of a given (fixed) size.
func (*ArrayType) HasUnderlying ¶
HasUnderlying determines whether or not this type has an underlying representation, or not.
func (*ArrayType) LeastUpperBound ¶
LeastUpperBound computes the least upper bound of this type and another. This is smallest type which contains both of the arguments. For example, i32 is the least upper bound of i1 and i32, etc. If no such type exists, then nil is returned.
type Binding ¶
type Binding interface {
// Determine whether this binding is finalised or not.
IsFinalised() bool
// Determine whether this binding can be defined recursively or not.
IsRecursive() bool
}
Binding represents an association between a name, as found in a source file, and concrete item (e.g. a column, function, etc).
type BoolType ¶
type BoolType struct {
}
BoolType represents the type of logical conditions, such as equality, logical or, etc.
func (*BoolType) HasUnderlying ¶
HasUnderlying determines whether or not this type has an underlying representation, or not.
func (*BoolType) LeastUpperBound ¶
LeastUpperBound computes the least upper bound of this type and another. This is smallest type which contains both of the arguments. For example, i32 is the least upper bound of i1 and i32, etc. If no such type exists, then nil is returned.
type Cast ¶
type Cast struct {
Arg Expr
Type Type
// Unsafe indicates this is an unsafe cast added explicitly within the
// constraints based on some developer knowledge.
Unsafe bool
}
Cast represents a user-supplied annotation indicating the given expression has the given type. This is only sound upto the user.
func (*Cast) AsConstant ¶
AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.
func (*Cast) Context ¶
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 (*Cast) Dependencies ¶
Dependencies needed to signal declaration.
type Circuit ¶
type Circuit struct {
Modules []Module
Declarations []Declaration
}
Circuit represents the root of the Abstract Syntax Tree. This is also referred to as the "prelude". All modules are contained within the root, and declarations can also be declared here as well.
type ColumnBinding ¶
type ColumnBinding struct {
// Context determines the real (i.e. non-virtual) enclosing module of this
// column, and should always be a prefix of the path. If this column was
// declared in a perspective then it will be the perspective's enclosing
// module. Otherwise, it will exactly match the path's parent.
ColumnContext file.Path
// Absolute Path of column. This determines the name of the column, its
// enclosing module and/or perspective.
Path file.Path
// Column's datatype
DataType Type
// Determines whether this column must be proven (or not).
MustProve bool
// Column's length Multiplier
Multiplier uint
// Determines the kind of this column.
Kind uint8
// Padding value (defaults to 0)
Padding big.Int
// Display modifier
Display string
}
ColumnBinding represents something bound to a given column.
func (*ColumnBinding) AbsolutePath ¶
func (p *ColumnBinding) AbsolutePath() *file.Path
AbsolutePath returns the fully resolved (absolute) path of the column in question.
func (*ColumnBinding) Context ¶
func (p *ColumnBinding) Context() Context
Context returns the of this column. That is, the module in which this colunm was declared and also the length multiplier of that module it requires.
func (*ColumnBinding) Finalise ¶
func (p *ColumnBinding) Finalise(multiplier uint, datatype Type)
Finalise this binding by providing the necessary missing information.
func (*ColumnBinding) IsComputed ¶
func (p *ColumnBinding) IsComputed() bool
IsComputed checks whether this binding is for a computed column (or not).
func (*ColumnBinding) IsFinalised ¶
func (p *ColumnBinding) IsFinalised() bool
IsFinalised checks whether this binding has been finalised yet or not.
func (*ColumnBinding) IsRecursive ¶
func (p *ColumnBinding) IsRecursive() bool
IsRecursive implementation for Binding interface.
type Concat ¶
type Concat struct {
Args []Expr
}
Concat represents a bitwise concatenation of expressions. For example, consider the concatenation (:: X Y) where each variable is 16bits. Then the resulting concatenation is 32bits, and corresponds to (X*65536) + Y. The main purpose of concetenations is to smooth the progress of migrating to a field-agnostic code base. We might imagine that this will be deprecated eventually.
func (*Concat) AsConstant ¶
AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.
func (*Concat) Context ¶
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 (*Concat) Dependencies ¶
Dependencies needed to signal declaration.
type Connective ¶
Connective represents a logical connective, such as logical AND / logical OR.
func (*Connective) AsConstant ¶
func (e *Connective) AsConstant() *big.Int
AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.
func (*Connective) Context ¶
func (e *Connective) Context() Context
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 (*Connective) Dependencies ¶
func (e *Connective) Dependencies() []Symbol
Dependencies needed to signal declaration.
func (*Connective) Lisp ¶
func (e *Connective) Lisp() sexp.SExp
Lisp converts this schema element into a simple S-Expression, for example so it can be printed.
type Constant ¶
Constant represents a constant value within an expression.
func (*Constant) AsConstant ¶
AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.
func (*Constant) Context ¶
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 (*Constant) Dependencies ¶
Dependencies needed to signal declaration.
type ConstantBinding ¶
type ConstantBinding struct {
Path file.Path
// Explicit type for this constant. This maybe nil if no type was given
// and, instead, the type should be inferred from context.
DataType Type
// Constant expression which, when evaluated, produces a constant Value.
Value Expr
// Determines whether this is an "externalised" constant, or not.
// Externalised constants are visible at the HIR level and can have their
// values overridden.
Extern bool
// contains filtered or unexported fields
}
ConstantBinding represents a constant definition
func NewConstantBinding ¶
NewConstantBinding creates a new constant binding (which is initially not finalised).
func (*ConstantBinding) Context ¶
func (p *ConstantBinding) Context() Context
Context returns the of this constant, noting that constants (by definition) do not have a context.
func (*ConstantBinding) IsFinalised ¶
func (p *ConstantBinding) IsFinalised() bool
IsFinalised checks whether this binding has been finalised yet or not.
func (*ConstantBinding) IsRecursive ¶
func (p *ConstantBinding) IsRecursive() bool
IsRecursive implementation for Binding interface.
type Context ¶
type Context struct {
// Identifies the module in which this evaluation context exists. The empty
// module is given by the maximum index (math.MaxUint).
ModuleId string
// Identifies the length multiplier required to complete this context. In
// essence, length multiplies divide up a given module into several disjoint
// "subregions", such than every expression exists only in one of them.
Multiplier uint
}
Context represents the evaluation context in which an expression can be evaluated. Firstly, every expression must have a single enclosing module (i.e. all columns accessed by the expression are in that module); secondly, the length multiplier for all columns accessed by the expression must be the same. Constant expressions are something of an anomily here since they have neither an enclosing module, nor a length modifier. Instead, we consider that constant expressions are evaluated in the empty --- or void --- context. This is something like a bottom type which is contained within all other contexts.
NOTE: Whilst the evaluation context provides a general abstraction, there are a number of restrictions imposed on it in practice which limit its use. These restrictions arise from what is and is not supported by the underlying constraint system (i.e. the prover). Example restrictions imposed include: multipliers must be powers of 2. Likewise, non-normal expressions (i.e those with a multipler > 1) can only be used in a fairly limited number of situtions (e.g. lookups).
func ConflictingContext ¶
func ConflictingContext() Context
ConflictingContext represents the case where multiple different contexts have been joined together. For example, when determining the context of an expression, the conflicting context is returned when no single context can be deteremed. This value is generally considered to indicate an error.
func ContextOfExpressions ¶
ContextOfExpressions returns the context for a set of zero or more expressions. Observe that, if there the expressions have no context (i.e. they are all constants) then the void context is returned. Likewise, if there are expressions with different contexts then the conflicted context will be returned. Otherwise, the one consistent context will be returned.
func NewContext ¶
NewContext returns a context representing the given module with the given length multiplier.
func VoidContext ¶
func VoidContext() Context
VoidContext returns the void (or empty) context. This is the bottom type in the lattice, and is the context contained in all other contexts. It is needed, for example, as the context for constant expressions.
func (Context) IsConflicted ¶
IsConflicted checks whether this context represents the conflicted context. This is the top element in the lattice, and is used to represent the case where e.g. an expression has multiple conflicting contexts.
func (Context) IsVoid ¶
IsVoid checks whether this context is the void context (or not). This is the bottom element in the lattice.
func (Context) Join ¶
Join returns the least upper bound of the two contexts, or false if this does not exist (i.e. the two context's are in conflict).
func (Context) LengthMultiplier ¶
LengthMultiplier returns the length multiplier for this context. Note, however, that this is nonsensical in the case of either the void or the conflicted context. In this cases, this method will panic.
func (Context) Module ¶
Module returns the module for this context. Note, however, that this is nonsensical in the case of either the void or the conflicted context. In this cases, this method will panic.
func (Context) ModuleName ¶
ModuleName returns the name of the module represented by this context. Since context's include length multipliers, this may not match the original (Corset) module name exactly.
type Debug ¶
type Debug struct{ Arg Expr }
Debug is an optional constraint which can be specifically enabled via the debug setting. The intention of debug constraints is that they capture things which are implied by other constraints. The ability to enable them can simply help with debugging, should it arise that they are not actually implied.
func (*Debug) AsConstant ¶
AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.
func (*Debug) Context ¶
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 (*Debug) Dependencies ¶
Dependencies needed to signal declaration.
type Declaration ¶
type Declaration interface {
Node
// Returns the set of symbols being defined this declaration. Observe that
// these may not yet have been finalised.
Definitions() iter.Iterator[SymbolDefinition]
// Return set of columns on which this declaration depends.
Dependencies() iter.Iterator[Symbol]
// Check whether this declaration defines a given symbol. The symbol in
// question needs to have been resolved already for this to make sense.
Defines(Symbol) bool
// Check whether this declaration is finalised already.
IsFinalised() bool
}
Declaration represents a top-level declaration in a Corset source file (e.g. defconstraint, defcolumns, etc).
type DefAlias ¶
type DefAlias struct {
// Name of the alias
Name string
}
DefAlias provides a node on which to hang source information to an alias name.
func NewDefAlias ¶
NewDefAlias constructs a new instance of DefAlias.
type DefAliases ¶
DefAliases represents the declaration of one or more aliases. That is, alternate names for existing symbols.
func NewDefAliases ¶
func NewDefAliases(aliases []*DefAlias, symbols []Symbol) *DefAliases
NewDefAliases constructs a new instance of DefAliases.
func (*DefAliases) Defines ¶
func (p *DefAliases) Defines(symbol Symbol) bool
Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.
func (*DefAliases) Definitions ¶
func (p *DefAliases) Definitions() iter.Iterator[SymbolDefinition]
Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.
func (*DefAliases) Dependencies ¶
func (p *DefAliases) Dependencies() iter.Iterator[Symbol]
Dependencies needed to signal declaration.
func (*DefAliases) IsFinalised ¶
func (p *DefAliases) IsFinalised() bool
IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.
func (*DefAliases) Lisp ¶
func (p *DefAliases) Lisp() sexp.SExp
Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.
type DefCall ¶
type DefCall struct {
// Returns for the call
Returns []Expr
// Function being called
Function string
// Arguments for the call
Arguments []Expr
// Optional source selector
Selector util.Option[Expr]
// contains filtered or unexported fields
}
DefCall captures a function call between a lisp module and an assembly function. A key feature of this is that it triggers trace propagation.
func NewDefCall ¶
NewDefCall creates a new (unfinalised) function call.
func (*DefCall) Defines ¶
Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.
func (*DefCall) Definitions ¶
func (p *DefCall) Definitions() iter.Iterator[SymbolDefinition]
Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.
func (*DefCall) Dependencies ¶
Dependencies needed to signal declaration.
func (*DefCall) Finalise ¶
func (p *DefCall) Finalise()
Finalise this declaration, which means that all source and target expressions have been resolved.
func (*DefCall) IsFinalised ¶
IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.
type DefColumn ¶
type DefColumn struct {
// contains filtered or unexported fields
}
DefColumn packages together those piece relevant to declaring an individual column, such its name and type.
func NewDefColumn ¶
func NewDefColumn(binding ColumnBinding) *DefColumn
NewDefColumn constructs a new (non-computed) column declaration. Such a column is automatically finalised, since all information is provided at the point of creation.
func NewDefComputedColumn ¶
NewDefComputedColumn constructs a new column declaration for a computed column. Such a column cannot be finalised yet, since its type and multiplier remains to be determined, etc.
func (*DefColumn) Arity ¶
Arity indicates whether or not this is a function and, if so, what arity (i.e. how many arguments) the function has.
func (*DefColumn) Binding ¶
Binding returns the allocated binding for this symbol (which may or may not be finalised).
func (*DefColumn) DataType ¶
DataType returns the type of this column. If this column have not yet been finalised, then this will panic.
func (*DefColumn) InnerBinding ¶
func (e *DefColumn) InnerBinding() ColumnBinding
InnerBinding returns the allocated binding for this symbol (which may or may not be finalised).
func (*DefColumn) LengthMultiplier ¶
LengthMultiplier returns the length multiplier of this column (where the height of this column is determined as the product of the enclosing module's height and this length multiplier). If this column have not yet been finalised, then this will panic.
func (*DefColumn) Lisp ¶
Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.
func (*DefColumn) MustProve ¶
MustProve determines whether or not the type of this column must be established by the prover (e.g. a range constraint or similar).
type DefColumns ¶
type DefColumns struct {
Columns []*DefColumn
}
DefColumns captures a set of one or more columns being declared.
func NewDefColumns ¶
func NewDefColumns(columns []*DefColumn) *DefColumns
NewDefColumns constructs a new instance of DefColumns.
func (*DefColumns) Defines ¶
func (p *DefColumns) Defines(symbol Symbol) bool
Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.
func (*DefColumns) Definitions ¶
func (p *DefColumns) Definitions() iter.Iterator[SymbolDefinition]
Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.
func (*DefColumns) Dependencies ¶
func (p *DefColumns) Dependencies() iter.Iterator[Symbol]
Dependencies needed to signal declaration.
func (*DefColumns) IsFinalised ¶
func (p *DefColumns) IsFinalised() bool
IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.
func (*DefColumns) Lisp ¶
func (p *DefColumns) Lisp() sexp.SExp
Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.
type DefComputed ¶
type DefComputed struct {
// Columns being assigned by this computation
Targets []*DefColumn
// Function being invoked to perform computation
Function Symbol
// Source columns as parameters to computation.
Sources []Symbol
// Indicates the declaration has been resolved
Finalised bool
}
DefComputed is an assignment which computes the values for one or more columns based (currently) on a chosen internal function.
func (*DefComputed) Defines ¶
func (p *DefComputed) Defines(symbol Symbol) bool
Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.
func (*DefComputed) Definitions ¶
func (p *DefComputed) Definitions() iter.Iterator[SymbolDefinition]
Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.
func (*DefComputed) Dependencies ¶
func (p *DefComputed) Dependencies() iter.Iterator[Symbol]
Dependencies needed to signal declaration.
func (*DefComputed) Finalise ¶
func (p *DefComputed) Finalise()
Finalise this declaration, which means that all source and target expressions have been resolved.
func (*DefComputed) IsFinalised ¶
func (p *DefComputed) IsFinalised() bool
IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.
func (*DefComputed) Lisp ¶
func (p *DefComputed) Lisp() sexp.SExp
Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.
type DefComputedColumn ¶
type DefComputedColumn struct {
// Column being assigned by this computation.
Target *DefColumn
// The formula to get the target column from the source columns.
Computation Expr
// Indicates the computation has been resolved
Finalised bool
}
DefComputedColumn is an assignment which computes the values for one column based on a chosen internal function.
func (*DefComputedColumn) Defines ¶
func (p *DefComputedColumn) Defines(symbol Symbol) bool
Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.
func (*DefComputedColumn) Definitions ¶
func (p *DefComputedColumn) Definitions() iter.Iterator[SymbolDefinition]
Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.
func (*DefComputedColumn) Dependencies ¶
func (p *DefComputedColumn) Dependencies() iter.Iterator[Symbol]
Dependencies needed to signal declaration.
func (*DefComputedColumn) Finalise ¶
func (p *DefComputedColumn) Finalise()
Finalise this computed column, which means the target binding and the comptuation itself have been finalised.
func (*DefComputedColumn) IsFinalised ¶
func (p *DefComputedColumn) IsFinalised() bool
IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.
func (*DefComputedColumn) Lisp ¶
func (p *DefComputedColumn) Lisp() sexp.SExp
Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.
type DefConst ¶
type DefConst struct {
// List of constant pairs. Observe that every expression in this list must
// be constant (i.e. it cannot refer to column values or call impure
// functions, etc).
Constants []*DefConstUnit
}
DefConst represents the declaration of one of more constant values which can be used within expressions to improve readability.
func (*DefConst) Defines ¶
Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.
func (*DefConst) Definitions ¶
func (p *DefConst) Definitions() iter.Iterator[SymbolDefinition]
Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.
func (*DefConst) Dependencies ¶
Dependencies needed to signal declaration.
func (*DefConst) IsFinalised ¶
IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.
type DefConstUnit ¶
type DefConstUnit struct {
// Binding for this constant.
ConstBinding ConstantBinding
}
DefConstUnit represents the definition of exactly one constant value. As such, this is an instance of SymbolDefinition and provides a binding.
func (*DefConstUnit) Arity ¶
func (e *DefConstUnit) Arity() util.Option[uint]
Arity indicates whether or not this is a function and, if so, what arity (i.e. how many arguments) the function has.
func (*DefConstUnit) Binding ¶
func (e *DefConstUnit) Binding() Binding
Binding returns the allocated binding for this symbol (which may or may not be finalised).
func (*DefConstUnit) Lisp ¶
func (e *DefConstUnit) Lisp() sexp.SExp
Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.
func (*DefConstUnit) Name ¶
func (e *DefConstUnit) Name() string
Name returns the (unqualified) name of this symbol. For example, "X" for a column X defined in a module m1.
func (*DefConstUnit) Path ¶
func (e *DefConstUnit) Path() *file.Path
Path returns the qualified name (i.e. absolute path) of this symbol. For example, "m1.X" for a column X defined in module m1.
type DefConstraint ¶
type DefConstraint struct {
// Unique handle given to this constraint. This is primarily useful for
// debugging (i.e. so we know which constraint failed, etc).
Handle string
// Domain of this constraint which, if empty, indicates a global constraint.
// Otherwise, a given value indicates a single row on which this constraint
// should apply (where negative values are taken from the end, meaning that
// -1 represents the last row of a given module).
Domain util.Option[int]
// A selector which determines for which rows this constraint is active.
// Specifically, when the expression evaluates to a non-zero value then the
// constraint is active; otherwise, its inactive. Nil is permitted to
// indicate no guard is present.
Guard Expr
// Perspective identifies the perspective to which this constraint is
// associated (if any).
Perspective *PerspectiveName
// The constraint itself which (when active) should evaluate to zero for the
// relevant set of rows.
Constraint Expr
// contains filtered or unexported fields
}
DefConstraint represents a vanishing constraint, which is either "local" or "global". A local constraint applies either to the first or last rows, whilst a global constraint applies to all rows. For a constraint to hold, its expression must evaluate to zero for the rows on which it is active. A constraint may also have a "guard" which is an expression that must evaluate to a non-zero value for the constraint to be considered active. The expression for a constraint must have a single context. That is, it can only be applied to columns within the same module (i.e. to ensure they have the same height). Furthermore, within a given module, we require that all columns accessed by the constraint have the same length multiplier.
func NewDefConstraint ¶
func NewDefConstraint(handle string, domain util.Option[int], guard Expr, perspective *PerspectiveName, constraint Expr) *DefConstraint
NewDefConstraint constructs a new (unfinalised) constraint.
func (*DefConstraint) Defines ¶
func (p *DefConstraint) Defines(symbol Symbol) bool
Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.
func (*DefConstraint) Definitions ¶
func (p *DefConstraint) Definitions() iter.Iterator[SymbolDefinition]
Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.
func (*DefConstraint) Dependencies ¶
func (p *DefConstraint) Dependencies() iter.Iterator[Symbol]
Dependencies needed to signal declaration.
func (*DefConstraint) Finalise ¶
func (p *DefConstraint) Finalise()
Finalise this declaration, which means that its guard (if applicable) and body have been resolved.
func (*DefConstraint) IsFinalised ¶
func (p *DefConstraint) IsFinalised() bool
IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.
func (*DefConstraint) Lisp ¶
func (p *DefConstraint) Lisp() sexp.SExp
Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.
type DefFun ¶
type DefFun struct {
// contains filtered or unexported fields
}
DefFun represents defines a (possibly pure) "function" (which, in actuality, is more like a macro). Specifically, whenever an invocation of this function is encountered we can imagine that, in the final constraint set, the body of the function is inlined at the point of the call. A pure function is not permitted to access any columns in scope (i.e. it can only manipulate its parameters). In contrast, an impure function can access those columns defined within its enclosing context.
func NewDefFun ¶
func NewDefFun(name *FunctionName, parameters []*DefParameter, ret Type) *DefFun
NewDefFun constructs a new (unfinalised) function declaration.
func (*DefFun) Arity ¶
Arity indicates whether or not this is a function and, if so, what arity (i.e. how many arguments) the function has.
func (*DefFun) Binding ¶
Binding returns the allocated binding for this symbol (which may or may not be finalised).
func (*DefFun) Defines ¶
Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.
func (*DefFun) Definitions ¶
func (p *DefFun) Definitions() iter.Iterator[SymbolDefinition]
Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.
func (*DefFun) Dependencies ¶
Dependencies needed to signal declaration.
func (*DefFun) IsFinalised ¶
IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.
func (*DefFun) IsPure ¶
IsPure indicates whether or not this is a pure function. That is, a function which is not permitted to access any columns from the enclosing environment (either directly itself, or indirectly via functions it calls).
func (*DefFun) Lisp ¶
Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.
func (*DefFun) Name ¶
Name returns the (unqualified) name of this symbol. For example, "X" for a column X defined in a module m1.
func (*DefFun) Parameters ¶
func (p *DefFun) Parameters() []*DefParameter
Parameters returns information about the parameters defined by this declaration.
type DefInRange ¶
type DefInRange struct {
// The expression whose values are being constrained to within the given
// bound.
Expr Expr
// Bitwidth determines the bitwidth that this range constraint is enforcing.
Bitwidth uint
// contains filtered or unexported fields
}
DefInRange restricts all values for a given expression to be within a range [0..n) for some bound n. Any bound is supported, and the system will choose the best underlying implementation as needed.
func (*DefInRange) Defines ¶
func (p *DefInRange) Defines(symbol Symbol) bool
Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.
func (*DefInRange) Definitions ¶
func (p *DefInRange) Definitions() iter.Iterator[SymbolDefinition]
Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.
func (*DefInRange) Dependencies ¶
func (p *DefInRange) Dependencies() iter.Iterator[Symbol]
Dependencies needed to signal declaration.
func (*DefInRange) Finalise ¶
func (p *DefInRange) Finalise()
Finalise this declaration, meaning that the expression has been resolved.
func (*DefInRange) IsFinalised ¶
func (p *DefInRange) IsFinalised() bool
IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.
func (*DefInRange) Lisp ¶
func (p *DefInRange) Lisp() sexp.SExp
Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.
type DefInterleaved ¶
type DefInterleaved struct {
// The target column being defined
Target *DefColumn
// The source columns used to define the interleaved target column.
Sources []TypedSymbol
// Indicates the declaration has been resolved
Finalised bool
}
DefInterleaved generates a new column by interleaving two or more existing columns. For example, say Z interleaves X and Y (in that order) and we have a trace X=[1,2], Y=[3,4]. Then, the interleaved column Z has the values Z=[1,3,2,4]. All columns must be defined within the same context. Finally, the type of the interleaved column is the widest type of any source columns. For example, consider an interleaving of two columns X and Y with types i16 and i8 respectively. Then, the type of the resulting column is i16 (as this is required to hold an element from any source column).
func (*DefInterleaved) Defines ¶
func (p *DefInterleaved) Defines(symbol Symbol) bool
Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.
func (*DefInterleaved) Definitions ¶
func (p *DefInterleaved) Definitions() iter.Iterator[SymbolDefinition]
Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.
func (*DefInterleaved) Dependencies ¶
func (p *DefInterleaved) Dependencies() iter.Iterator[Symbol]
Dependencies needed to signal declaration.
func (*DefInterleaved) Finalise ¶
func (p *DefInterleaved) Finalise()
Finalise this declaration, which means that all source and target expressions have been resolved.
func (*DefInterleaved) IsFinalised ¶
func (p *DefInterleaved) IsFinalised() bool
IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.
func (*DefInterleaved) Lisp ¶
func (p *DefInterleaved) Lisp() sexp.SExp
Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.
type DefLookup ¶
type DefLookup struct {
// Unique handle given to this constraint. This is primarily useful for
// debugging (i.e. so we know which constraint failed, etc).
Handle string
// Checked determines whether or not "type checking" is enabled for source /
// target pairs.
Checked bool
// Source selector expressions (nil entries mean no selector for corresponding source).
SourceSelectors []Expr
// Source expressions for lookup (i.e. these values must all be contained
// within the targets).
Sources [][]Expr
// Target selector expressions (nil entries mean no selector for corresponding source).
TargetSelectors []Expr
// Target expressions for lookup (i.e. these values must contain all of the
// source values, but may contain more).
Targets [][]Expr
// contains filtered or unexported fields
}
DefLookup represents a lookup constraint between a set N of source expressions and a set of N target expressions. The source expressions must have a single context (i.e. all be in the same module) and likewise for the target expressions (though the source and target contexts can differ). The constraint can be viewed as a "subset constraint". Let the set of "source tuples" be those obtained by evaluating the source expressions over all rows in the source context, and likewise the "target tuples" those for the target expressions in the target context. Then the lookup constraint holds if the set of source tuples is a subset of the target tuples. This does not need to be a strict subset, so the two sets can be identical. Furthermore, these are not treated as multi-sets, hence the number of occurrences of a given tuple is not relevant.
func NewDefLookup ¶
func NewDefLookup(handle string, checked bool, sourceSelectors []Expr, sources [][]Expr, targetSelectors []Expr, targets [][]Expr) *DefLookup
NewDefLookup creates a new (unfinalised) lookup constraint.
func (*DefLookup) Defines ¶
Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.
func (*DefLookup) Definitions ¶
func (p *DefLookup) Definitions() iter.Iterator[SymbolDefinition]
Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.
func (*DefLookup) Dependencies ¶
Dependencies needed to signal declaration.
func (*DefLookup) Finalise ¶
func (p *DefLookup) Finalise()
Finalise this declaration, which means that all source and target expressions have been resolved.
func (*DefLookup) IsFinalised ¶
IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.
type DefParameter ¶
type DefParameter struct {
Binding LocalVariableBinding
}
DefParameter packages together those piece relevant to declaring an individual parameter, such its name and type.
func NewDefParameter ¶
func NewDefParameter(name string, datatype Type) *DefParameter
NewDefParameter constructs a new parameter declaration.
func (*DefParameter) Lisp ¶
func (p *DefParameter) Lisp() sexp.SExp
Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.
type DefPermutation ¶
DefPermutation represents a (lexicographically sorted) permutation of a set of source columns in a given source context, manifested as an assignment to a corresponding set of target columns. The sort direction for each of the source columns can be specified as increasing or decreasing.
func NewDefPermutation ¶
func NewDefPermutation(targets []*DefColumn, sources []Symbol, signs []bool) *DefPermutation
NewDefPermutation constructs a new (unfinalised) sorted permutation assignment.
func (*DefPermutation) Defines ¶
func (p *DefPermutation) Defines(symbol Symbol) bool
Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.
func (*DefPermutation) Definitions ¶
func (p *DefPermutation) Definitions() iter.Iterator[SymbolDefinition]
Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.
func (*DefPermutation) Dependencies ¶
func (p *DefPermutation) Dependencies() iter.Iterator[Symbol]
Dependencies needed to signal declaration.
func (*DefPermutation) IsFinalised ¶
func (p *DefPermutation) IsFinalised() bool
IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.
func (*DefPermutation) Lisp ¶
func (p *DefPermutation) Lisp() sexp.SExp
Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.
type DefPerspective ¶
type DefPerspective struct {
// Selector for the perspective.
Selector Expr
// Columns defined in this perspective.
Columns []*DefColumn
// contains filtered or unexported fields
}
DefPerspective captures the definition of a perspective, its selector and a set of one or more columns being declared within.
func NewDefPerspective ¶
func NewDefPerspective(name *PerspectiveName, selector Expr, columns []*DefColumn) *DefPerspective
NewDefPerspective constructs a new (unfinalised) perspective declaration.
func (*DefPerspective) Arity ¶
func (p *DefPerspective) Arity() util.Option[uint]
Arity indicates whether or not this is a function and, if so, what arity (i.e. how many arguments) the function has.
func (*DefPerspective) Binding ¶
func (p *DefPerspective) Binding() Binding
Binding returns the allocated binding for this symbol (which may or may not be finalised).
func (*DefPerspective) Defines ¶
func (p *DefPerspective) Defines(symbol Symbol) bool
Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.
func (*DefPerspective) Definitions ¶
func (p *DefPerspective) Definitions() iter.Iterator[SymbolDefinition]
Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.
func (*DefPerspective) Dependencies ¶
func (p *DefPerspective) Dependencies() iter.Iterator[Symbol]
Dependencies needed to signal declaration.
func (*DefPerspective) Finalise ¶
func (p *DefPerspective) Finalise()
Finalise this perspective, which indicates the selector expression has been finalised.
func (*DefPerspective) IsFinalised ¶
func (p *DefPerspective) IsFinalised() bool
IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.
func (*DefPerspective) Lisp ¶
func (p *DefPerspective) Lisp() sexp.SExp
Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.
func (*DefPerspective) Name ¶
func (p *DefPerspective) Name() string
Name returns the (unqualified) name of this symbol. For example, "X" for a column X defined in a module m1.
func (*DefPerspective) Path ¶
func (p *DefPerspective) Path() *file.Path
Path returns the qualified name (i.e. absolute path) of this symbol. For example, "m1.X" for a column X defined in module m1.
type DefProperty ¶
type DefProperty struct {
// Unique handle given to this constraint. This is primarily useful for
// debugging (i.e. so we know which constaint failed, etc).
Handle string
// Domain of this property which, if empty, indicates the property applies
// to all rows. Otherwise, a given value indicates a single row on which
// this property should apply (where negative values are taken from the end,
// meaning that -1 represents the last row of a given module).
Domain util.Option[int]
// The assertion itself which (when active) should evaluate to zero for the
// relevant set of rows.
Assertion Expr
// contains filtered or unexported fields
}
DefProperty represents an assertion to be used only for debugging / testing / verification. Unlike vanishing constraints, property assertions do not represent something that the prover can enforce. Rather, they represent properties which are expected to hold for every valid trace. That is, they should be implied by the actual constraints. Thus, whilst the prover cannot enforce such properties, external tools (such as for formal verification) can attempt to ensure they do indeed always hold.
func NewDefProperty ¶
NewDefProperty constructs a new (unfinalised) property assertion.
func (*DefProperty) Defines ¶
func (p *DefProperty) Defines(symbol Symbol) bool
Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.
func (*DefProperty) Definitions ¶
func (p *DefProperty) Definitions() iter.Iterator[SymbolDefinition]
Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.
func (*DefProperty) Dependencies ¶
func (p *DefProperty) Dependencies() iter.Iterator[Symbol]
Dependencies needed to signal declaration.
func (*DefProperty) Finalise ¶
func (p *DefProperty) Finalise()
Finalise this property, meaning that the assertion has been resolved.
func (*DefProperty) IsFinalised ¶
func (p *DefProperty) IsFinalised() bool
IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.
func (*DefProperty) Lisp ¶
func (p *DefProperty) Lisp() sexp.SExp
Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.
type DefSorted ¶
type DefSorted struct {
// Unique handle given to this constraint. This is primarily useful for
// debugging (i.e. so we know which constraint failed, etc).
Handle string
// Optional selector expression which determines when a sorted constraint is active.
Selector util.Option[Expr]
// Source expressions for lookup (i.e. these values must all be contained
// within the targets).
Sources []Expr
// Sorting signs
Signs []bool
// Indicates whether sorting constraint is strict (or not).
Strict bool
// contains filtered or unexported fields
}
DefSorted ensures that a given set of columns are lexicographically sorted. The sort direction for each of the source columns can be specified as increasing or decreasing.
func NewDefSorted ¶
func NewDefSorted(handle string, selector util.Option[Expr], sources []Expr, signs []bool, strict bool) *DefSorted
NewDefSorted constructs a new (unfinalised) sorted constraint which can (optionally) be controlled by a given selector expression, and may be strict or non-strict. Observe that, for strict sorting, a selector is always needed (i.e. because within padding we cannot guarantee strictness).
func (*DefSorted) Defines ¶
Defines checks whether this declaration defines the given symbol. The symbol in question needs to have been resolved already for this to make sense.
func (*DefSorted) Definitions ¶
func (p *DefSorted) Definitions() iter.Iterator[SymbolDefinition]
Definitions returns the set of symbols defined by this declaration. Observe that these may not yet have been finalised.
func (*DefSorted) Dependencies ¶
Dependencies needed to signal declaration.
func (*DefSorted) Finalise ¶
func (p *DefSorted) Finalise()
Finalise this declaration, which means that all source and target expressions have been resolved.
func (*DefSorted) IsFinalised ¶
IsFinalised checks whether this declaration has already been finalised. If so, then we don't need to finalise it again.
type DefunBinding ¶
type DefunBinding struct {
// Flag whether or not is Pure function
Pure bool
// Types of parameters (optional)
ParamTypes []Type
// Type of return (optional)
ReturnType Type
// Body of the function in question.
Body Expr
// contains filtered or unexported fields
}
DefunBinding is a function binding arising from a user-defined function (as opposed, for example, to a function binding arising from an intrinsic).
func NewDefunBinding ¶
func NewDefunBinding(pure bool, paramTypes []Type, returnType Type, forced bool, body Expr) DefunBinding
NewDefunBinding constructs a new function binding.
func (*DefunBinding) Finalise ¶
func (p *DefunBinding) Finalise()
Finalise this binding by providing the necessary missing information.
func (*DefunBinding) IsFinalised ¶
func (p *DefunBinding) IsFinalised() bool
IsFinalised checks whether this binding has been finalised yet or not.
func (*DefunBinding) IsNative ¶
func (p *DefunBinding) IsNative() bool
IsNative checks whether this function binding is native (or not).
func (*DefunBinding) IsPure ¶
func (p *DefunBinding) IsPure() bool
IsPure checks whether this is a defpurefun or not
func (*DefunBinding) IsRecursive ¶
func (p *DefunBinding) IsRecursive() bool
IsRecursive implementation for Binding interface.
func (*DefunBinding) Signature ¶
func (p *DefunBinding) Signature() *FunctionSignature
Signature returns the corresponding function signature for this user-defined function.
type Equation ¶
type Equation struct {
// Indicates equality (true) or non-equality (false).
Kind uint8
// Left-Hand Side
Lhs Expr
// Right-Hand Side
Rhs Expr
}
Equation represents either an equality (e.g. X==Y), a non-equality (X!=Y), or an inequality (X<=Y, X<Y, etc).
func (*Equation) AsConstant ¶
AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.
func (*Equation) Context ¶
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 (*Equation) Dependencies ¶
Dependencies needed to signal declaration.
func (*Equation) LeftHandSide ¶
LeftHandSide returns the left-hand side of this condition.
func (*Equation) Lisp ¶
Lisp converts this schema element into a simple S-Expression, for example so it can be printed.
func (*Equation) RightHandSide ¶
RightHandSide returns the right-hand side of this condition.
type Exp ¶
Exp represents the a given value taken to a power.
func (*Exp) AsConstant ¶
AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.
func (*Exp) Context ¶
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 (*Exp) Dependencies ¶
Dependencies needed to signal declaration.
type Expr ¶
type Expr interface {
Node
// Evaluates this expression as a constant (signed) value. If this
// expression is not constant, then nil is returned.
AsConstant() *big.Int
// 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).
Context() Context
// Return set of columns on which this declaration depends.
Dependencies() []Symbol
}
Expr represents an arbitrary expression over the columns of a given context (or the parameters of an enclosing function). Such expressions are pitched at a higher-level than those of the underlying constraint system. For example, they can contain conditionals (i.e. if expressions) and normalisations, etc. During the lowering process down to the underlying constraints level (AIR), such expressions are "compiled out" using various techniques (such as introducing computed columns where necessary).
func ShallowCopy ¶
ShallowCopy creates a copy of the expression itself, but not those expressions it contains (if any). This is useful in e.g. situations where we want to associate different source file information with a specific expression.
func Substitute ¶
Substitute variables (such as for function parameters) in this expression based on a mapping of said variables to expressions. Furthermore, an (optional) source map is provided which will be updated, such that the freshly created expressions are mapped to their corresponding nodes.
func SubstituteAll ¶
SubstituteAll substitutes all variables found in a given set of expressions.
type For ¶
type For struct {
// Variable binding
Binding LocalVariableBinding
// Start value for Index
Start uint
// Last Value for Index
End uint
// Body of loop
Body Expr
}
For represents a for loop of a statically known range of values
func NewFor ¶
NewFor constructs a new for-expression given a variable name, a static index range and a body.
func (*For) AsConstant ¶
AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.
func (*For) Context ¶
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 (*For) Dependencies ¶
Dependencies needed to signal declaration.
func (*For) Lisp ¶
Lisp converts this schema element into a simple S-Expression, for example so it can be printed.
func (*For) Multiplicity ¶
Multiplicity determines the number of values that evaluating this expression can generate.
type FunctionBinding ¶
type FunctionBinding interface {
Binding
// IsPure checks whether this function binding has side-effects or not.
IsPure() bool
// IsNative checks whether this function binding is native (or not).
IsNative() bool
// Signature returns the function signature for this binding.
Signature() *FunctionSignature
}
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 FunctionName ¶
type FunctionName = Name[*DefunBinding]
FunctionName represents a name used in a position where it can only be resolved as a function.
func NewFunctionName ¶
func NewFunctionName(path file.Path, binding *DefunBinding) *FunctionName
NewFunctionName construct a new column name which is (initially) unresolved.
type FunctionSignature ¶
type FunctionSignature struct {
// contains filtered or unexported fields
}
FunctionSignature embodies a concrete function instance. It is necessary to separate bindings from signatures because, in corset, function overloading is supported. That is, we can have different definitions for a function of the same name and arity. The appropriate definition is then selected for the given parameter types.
func NewFunctionSignature ¶
func NewFunctionSignature(pure bool, parameters []Type, ret Type, body Expr) *FunctionSignature
NewFunctionSignature creates a new function signature with a given set of parameter/return types and a body. The signature can also be identified as that of a pure function, or not.
func (*FunctionSignature) Apply ¶
Apply a set of concreate arguments to this function. This substitutes them through the body of the function producing a single expression.
func (*FunctionSignature) Arity ¶
func (p *FunctionSignature) Arity() uint
Arity returns the number of parameters in this signature.
func (*FunctionSignature) IsPure ¶
func (p *FunctionSignature) IsPure() bool
IsPure checks whether this function binding has side-effects or not.
func (*FunctionSignature) Parameter ¶
func (p *FunctionSignature) Parameter(index uint) Type
Parameter returns the given parameter in this signature.
func (*FunctionSignature) Return ¶
func (p *FunctionSignature) Return() Type
Return the (optional) return type for this signature. If no declared return type is given, then the intention is that it be inferred from the body.
type If ¶
type If struct {
// Elements contained within this list.
Condition Expr
// True branch (optional).
TrueBranch Expr
// False branch (optional).
FalseBranch Expr
}
If returns the (optional) true branch when the condition evaluates to zero, and the (optional false branch otherwise.
func (*If) AsConstant ¶
AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.
func (*If) Context ¶
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 (*If) Dependencies ¶
Dependencies needed to signal declaration.
type IntType ¶
type IntType struct {
// contains filtered or unexported fields
}
IntType represents a set of signed integer values.
func NewIntType ¶
NewIntType constructs a new integer type containing all values between the lower and upper bounds (inclusive).
func (*IntType) HasUnderlying ¶
HasUnderlying determines whether or not this type has an underlying representation, or not.
func (*IntType) LeastUpperBound ¶
LeastUpperBound computes the least upper bound of this type and another. This is smallest type which contains both of the arguments. For example, i32 is the least upper bound of i1 and i32, etc. If no such type exists, then nil is returned.
type Invoke ¶
type Invoke struct {
Name *VariableAccess
Args []Expr
}
Invoke represents an attempt to invoke a given function.
func (*Invoke) AsConstant ¶
AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.
func (*Invoke) Context ¶
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 (*Invoke) Dependencies ¶
Dependencies needed to signal declaration.
type Let ¶
type Let struct {
// The set of variables defined by this expression.
Vars []LocalVariableBinding
// Identifies the assigned expression for each variable defined.
Args []Expr
// Body of the let expression (i.e. where the variables it defines can be
// used).
Body Expr
}
Let is a common expression form used in programming languages, particularly functional languages. It allows us to assign a "variable" to a given expression, such that we can reuse that variable in multiple places rather than repeat the entire expression. Note, however, that such variables are functional in nature --- they cannot, for example, be mutated via assignment, etc.
func (*Let) AsConstant ¶
AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.
func (*Let) Context ¶
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 (*Let) Dependencies ¶
Dependencies needed to signal declaration.
type List ¶
type List struct{ Args []Expr }
List represents a block of zero or more expressions.
func (*List) AsConstant ¶
AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.
func (*List) Context ¶
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 (*List) Dependencies ¶
Dependencies needed to signal declaration.
type LocalVariableBinding ¶
type LocalVariableBinding struct {
// Name the local variable
Name string
// Type to use for this parameter.
DataType Type
// Identifies the variable or column Index (as appropriate).
Index uint
}
LocalVariableBinding represents something bound to a given column.
func NewLocalVariableBinding ¶
func NewLocalVariableBinding(name string, datatype Type) LocalVariableBinding
NewLocalVariableBinding constructs an (unitilalised) variable binding. Being uninitialised means that its index identifier remains unknown.
func (*LocalVariableBinding) Finalise ¶
func (p *LocalVariableBinding) Finalise(index uint)
Finalise this local variable binding by allocating it an identifier.
func (*LocalVariableBinding) IsFinalised ¶
func (p *LocalVariableBinding) IsFinalised() bool
IsFinalised checks whether this binding has been finalised yet or not.
func (*LocalVariableBinding) IsRecursive ¶
func (p *LocalVariableBinding) IsRecursive() bool
IsRecursive implementation for Binding interface.
type Module ¶
type Module struct {
Name string
Declarations []Declaration
}
Module represents a top-level module declaration. This corresponds to a table in the final constraint set.
type Mul ¶
type Mul struct{ Args []Expr }
Mul represents the product over zero or more expressions.
func (*Mul) AsConstant ¶
AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.
func (*Mul) Context ¶
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 (*Mul) Dependencies ¶
Dependencies needed to signal declaration.
type Name ¶
type Name[T Binding] struct { // contains filtered or unexported fields }
Name represents a name within some syntactic item. Essentially this wraps a string and provides a mechanism for it to be associated with source line information.
func NewBoundName ¶
NewBoundName construct a new name which is already unresolved.
func NewUnboundName ¶
NewUnboundName construct a new name which is (initially) unresolved.
func (*Name[T]) Arity ¶
Arity indicates whether or not this is a function and, if so, what arity (i.e. how many arguments) the function has.
func (*Name[T]) Binding ¶
Binding gets binding associated with this interface. This will panic if this symbol is not yet resolved.
func (*Name[T]) InnerBinding ¶
func (e *Name[T]) InnerBinding() T
InnerBinding returns the concrete binding type used within this name.
func (*Name[T]) IsResolved ¶
IsResolved checks whether this symbol has been resolved already, or not.
func (*Name[T]) Lisp ¶
Lisp converts this node into its lisp representation. This is primarily used for debugging purposes.
func (*Name[T]) Name ¶
Name returns the (unqualified) name of this symbol. For example, "X" for a column X defined in a module m1.
type Node ¶
type Node interface {
// Convert this node into its lisp representation. This is primarily used
// for debugging purposes.
Lisp() sexp.SExp
}
Node provides common functionality across all elements of the Abstract Syntax Tree. For example, it ensures every element can converted back into Lisp form for debugging. Furthermore, it provides a reference point for constructing a suitable source map for reporting syntax errors.
type Normalise ¶
type Normalise struct{ Arg Expr }
Normalise reduces the value of an expression to either zero (if it was zero) or one (otherwise).
func (*Normalise) AsConstant ¶
AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.
func (*Normalise) Context ¶
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 (*Normalise) Dependencies ¶
Dependencies needed to signal declaration.
type Not ¶
type Not struct{ Arg Expr }
Not performs a logical negation on its argument.
func (*Not) AsConstant ¶
AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.
func (*Not) Context ¶
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 (*Not) Dependencies ¶
Dependencies needed to signal declaration.
type PerspectiveBinding ¶
type PerspectiveBinding struct {
// Expression which determines when this perspective is enabled.
Selector Expr
// contains filtered or unexported fields
}
PerspectiveBinding contains key information about a perspective, such as its selector expression.
func NewPerspectiveBinding ¶
func NewPerspectiveBinding(selector Expr) *PerspectiveBinding
NewPerspectiveBinding constructs a new binding for a given perspective.
func (*PerspectiveBinding) Finalise ¶
func (p *PerspectiveBinding) Finalise()
Finalise this binding, which indicates the selector expression has been finalised.
func (*PerspectiveBinding) IsFinalised ¶
func (p *PerspectiveBinding) IsFinalised() bool
IsFinalised checks whether this binding has been finalised yet or not.
func (*PerspectiveBinding) IsRecursive ¶
func (p *PerspectiveBinding) IsRecursive() bool
IsRecursive implementation for Binding interface.
type PerspectiveName ¶
type PerspectiveName = Name[*PerspectiveBinding]
PerspectiveName represents a name used in a position where it can only be resolved as a perspective.
func NewPerspectiveName ¶
func NewPerspectiveName(path file.Path, binding *PerspectiveBinding) *PerspectiveName
NewPerspectiveName construct a new column name which is (initially) unresolved.
type Reduce ¶
type Reduce struct {
Name *VariableAccess
Arg Expr
}
Reduce reduces (i.e. folds) a list using a given binary function.
func (*Reduce) AsConstant ¶
AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.
func (*Reduce) Context ¶
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 (*Reduce) Dependencies ¶
Dependencies needed to signal declaration.
type Shift ¶
type Shift struct {
// The expression being shifted
Arg Expr
// The amount it is being shifted by.
Shift Expr
}
Shift represents the result of a given expression shifted by a certain amount. In reality, the shift amount must be statically known. However, it is represented here as an expression to allow for constants and the results of function invocations, etc to be used. In all cases, these must still be eventually translated into constant values however.
func (*Shift) AsConstant ¶
AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.
func (*Shift) Context ¶
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 (*Shift) Dependencies ¶
Dependencies needed to signal declaration.
type Sub ¶
type Sub struct{ Args []Expr }
Sub represents the subtraction over zero or more expressions.
func (*Sub) AsConstant ¶
AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.
func (*Sub) Context ¶
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 (*Sub) Dependencies ¶
Dependencies needed to signal declaration.
type Symbol ¶
type Symbol interface {
Node
// Path returns the given path of this symbol.
Path() *file.Path
// Indicates whether or not this is a function and, if so, what arity (i.e.
// how many arguments) the function has.
Arity() util.Option[uint]
// Checks whether this symbol has been resolved already, or not.
IsResolved() bool
// Get binding associated with this interface. This will panic if this
// symbol is not yet resolved.
Binding() Binding
// Resolve this symbol by associating it with the binding associated with
// the definition of the symbol to which this refers. Observe that
// resolution can fail if we cannot bind the symbol to the given binding
// (e.g. a function binding was provided, but we're expecting a column
// binding).
Resolve(Binding) bool
}
Symbol represents a variable or function access within a declaration. Initially, such the proper interpretation of such accesses is unclear and it is only later when we can distinguish them (e.g. whether its a column access, a constant access, etc).
func DependenciesOfExpressions ¶
DependenciesOfExpressions determines the dependencies for a given set of zero or more expressions.
type SymbolDefinition ¶
type SymbolDefinition interface {
Node
// Name returns the (unqualified) name of this symbol. For example, "X" for
// a column X defined in a module m1.
Name() string
// Path returns the qualified name (i.e. absolute path) of this symbol. For
// example, "m1.X" for a column X defined in module m1.
Path() *file.Path
// Indicates whether or not this is a function and, if so, what arity (i.e.
// how many arguments) the function has.
Arity() util.Option[uint]
// Allocated binding for the symbol which may or may not be finalised.
Binding() Binding
}
SymbolDefinition represents a declaration (or part thereof) which defines a particular symbol. For example, "defcolumns" will define one or more symbols representing columns, etc.
type Type ¶
type Type interface {
// SubtypeOf determines whether or not this type is a subtype of another.
SubtypeOf(Type) bool
// LeastUpperBound computes the least upper bound of this type and another. This
// is smallest type which contains both of the arguments. For example, i32 is
// the least upper bound of i1 and i32, etc. If no such type exists, then nil
// is returned.
LeastUpperBound(Type) 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
// Determines whether or not this type has an underlying representation, or
// not.
HasUnderlying() bool
// Produce a string representation of this type.
String() string
}
Type embodies a richer notion of type found at the Corset level, compared with that found at lower levels (e.g. HIR). below.
ANY_TYPE represents the top of the lattice. That is, any type can flow into any.
func LeastUpperBound ¶
LeastUpperBound computes the Least Upper Bound of two types. This is deliberately coarse-grained and does not, for example, attempt to perform any kind of range analysis for integer types (as this would not make sense).
func LeastUpperBounds ¶
LeastUpperBounds returns, for two arrays, the LUB of each type in each position. Either array can be nil, in which case the other is returned. Otherwise, they must have matching lengths (otherwise this will panic).
func NewUintType ¶
NewUintType constructs a native uint type of the given width which, initially, has no semantic specified.
type TypedSymbol ¶
type TypedSymbol interface {
Symbol
// Type returns the type associated with this symbol. If the type cannot be
// determined, then nil is returned.
Type() Type
}
TypedSymbol is an extended form of symbol which contains additional information about a given column access.
type VariableAccess ¶
type VariableAccess struct {
Name file.Path
FnArity util.Option[uint]
// contains filtered or unexported fields
}
VariableAccess represents reading the value of a given local variable (such as a function parameter).
func NewVariableAccess ¶
NewVariableAccess creates a new variable access with the given (optionally qualified) path that may (or may not) refer to a function, and which has a given initial binding (which can be nil).
func (*VariableAccess) Arity ¶
func (e *VariableAccess) Arity() util.Option[uint]
Arity indicates whether or not this is a function and, if so, what arity (i.e. how many arguments) the function has.
func (*VariableAccess) AsConstant ¶
func (e *VariableAccess) AsConstant() *big.Int
AsConstant attempts to evaluate this expression as a constant (signed) value. If this expression is not constant, then nil is returned.
func (*VariableAccess) Binding ¶
func (e *VariableAccess) Binding() Binding
Binding gets binding associated with this interface. This returns nil if the access has not already been resolved.
func (*VariableAccess) Context ¶
func (e *VariableAccess) Context() Context
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 (*VariableAccess) Dependencies ¶
func (e *VariableAccess) Dependencies() []Symbol
Dependencies needed to signal declaration.
func (*VariableAccess) IsResolved ¶
func (e *VariableAccess) IsResolved() bool
IsResolved checks whether this symbol has been resolved already, or not.
func (*VariableAccess) Lisp ¶
func (e *VariableAccess) Lisp() sexp.SExp
Lisp converts this schema element into a simple S-Expression, for example so it can be printed.a
func (*VariableAccess) Path ¶
func (e *VariableAccess) Path() *file.Path
Path returns the given path of this symbol.
func (*VariableAccess) Resolve ¶
func (e *VariableAccess) Resolve(binding Binding) bool
Resolve this symbol by associating it with the binding associated with the definition of the symbol to which this refers.
func (*VariableAccess) Type ¶
func (e *VariableAccess) Type() Type
Type returns the type associated with this symbol. If the type cannot be determined, then nil is returned.