Skip to content

Commit

Permalink
Fix Declaration Finalisation
Browse files Browse the repository at this point in the history
This fixes some problems with the existing finalisation algorithm.
Firstly, it was sometimes finalising things more than once (which is
wasteful).  Secondly, it was not finalising at a fine-enough granularity
(which caused problems for constant definitions which referred to
themself).  Finally, there were still some gremlins related to binding.
  • Loading branch information
DavePearce committed Dec 13, 2024
1 parent fc77ef4 commit 25e6c0e
Show file tree
Hide file tree
Showing 7 changed files with 270 additions and 41 deletions.
28 changes: 20 additions & 8 deletions pkg/corset/binding.go
Original file line number Diff line number Diff line change
Expand Up @@ -44,9 +44,21 @@ type ColumnBinding struct {
dataType Type
}

// NewColumnBinding constructs a new column binding in a given module.
func NewColumnBinding(module string, computed bool, mustProve bool, multiplier uint, datatype Type) *ColumnBinding {
return &ColumnBinding{math.MaxUint, module, computed, mustProve, multiplier, datatype}
// NewInputColumnBinding constructs a new column binding in a given module.
// This is for the case where all information about the column is already known,
// and will not be inferred from elsewhere.
func NewInputColumnBinding(module string, mustProve bool, multiplier uint, datatype Type) *ColumnBinding {
return &ColumnBinding{math.MaxUint, module, false, mustProve, multiplier, datatype}
}

// NewComputedColumnBinding constructs a new column binding in a given
// module. This is for the case where not all information is yet known about
// the column and, hence, it must be finalised later on. For example, in a
// definterleaved constraint the target column information (e.g. its type) is
// not immediately available and must be determined from those columns from
// which it is constructed.
func NewComputedColumnBinding(module string) *ColumnBinding {
return &ColumnBinding{math.MaxUint, module, true, false, 0, nil}
}

// IsFinalised checks whether this binding has been finalised yet or not.
Expand Down Expand Up @@ -127,15 +139,15 @@ type ParameterBinding struct {
datatype Type
}

// ============================================================================
// FunctionBinding
// ============================================================================

// IsFinalised checks whether this binding has been finalised yet or not.
func (p *ParameterBinding) IsFinalised() bool {
panic("")
panic("should be unreachable?")
}

// ============================================================================
// FunctionBinding
// ============================================================================

// FunctionBinding represents the binding of a function application to its
// physical definition.
type FunctionBinding struct {
Expand Down
189 changes: 188 additions & 1 deletion pkg/corset/ast.go → pkg/corset/declaration.go
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,11 @@ type Declaration interface {
Definitions() util.Iterator[SymbolDefinition]
// Return set of columns on which this declaration depends.
Dependencies() util.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
}

// ============================================================================
Expand Down Expand Up @@ -70,6 +75,20 @@ func (p *DefAliases) Definitions() util.Iterator[SymbolDefinition] {
return util.NewArrayIterator[SymbolDefinition](nil)
}

// 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 (p *DefAliases) Defines(symbol Symbol) bool {
// fine beause defaliases gets special treatement.
return false
}

// IsFinalised checks whether this declaration has already been finalised. If
// so, then we don't need to finalise it again.
func (p *DefAliases) IsFinalised() bool {
// Fine because defaliases doesn't really do anything with its symbols.
return true
}

// Lisp converts this node into its lisp representation. This is primarily used
// for debugging purposes.
//
Expand Down Expand Up @@ -130,6 +149,24 @@ func (p *DefColumns) Definitions() util.Iterator[SymbolDefinition] {
return util.NewCastIterator[*DefColumn, SymbolDefinition](iter)
}

// 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 (p *DefColumns) Defines(symbol Symbol) bool {
for _, sym := range p.Columns {
if &sym.binding == symbol.Binding() {
return true
}
}
//
return false
}

// IsFinalised checks whether this declaration has already been finalised. If
// so, then we don't need to finalise it again.
func (p *DefColumns) IsFinalised() bool {
return true
}

// Lisp converts this node into its lisp representation. This is primarily used
// for debugging purposes.
func (p *DefColumns) Lisp() sexp.SExp {
Expand Down Expand Up @@ -258,6 +295,30 @@ func (p *DefConst) Dependencies() util.Iterator[Symbol] {
return util.NewArrayIterator[Symbol](deps)
}

// 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 (p *DefConst) Defines(symbol Symbol) bool {
for _, sym := range p.constants {
if &sym.binding == symbol.Binding() {
return true
}
}
//
return false
}

// IsFinalised checks whether this declaration has already been finalised. If
// so, then we don't need to finalise it again.
func (p *DefConst) IsFinalised() bool {
for _, c := range p.constants {
if !c.binding.IsFinalised() {
return false
}
}
//
return true
}

// Lisp converts this node into its lisp representation. This is primarily used
// for debugging purposes.
func (p *DefConst) Lisp() sexp.SExp {
Expand Down Expand Up @@ -338,6 +399,8 @@ type DefConstraint struct {
// The constraint itself which (when active) should evaluate to zero for the
// relevant set of rows.
Constraint Expr
//
finalised bool
}

// Definitions returns the set of symbols defined by this declaration. Observe
Expand All @@ -359,6 +422,24 @@ func (p *DefConstraint) Dependencies() util.Iterator[Symbol] {
return util.NewArrayIterator[Symbol](append(guard_deps, body_deps...))
}

// 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 (p *DefConstraint) Defines(symbol Symbol) bool {
return false
}

// IsFinalised checks whether this declaration has already been finalised. If
// so, then we don't need to finalise it again.
func (p *DefConstraint) IsFinalised() bool {
return p.finalised
}

// Finalise this declaration, which means that its guard (if applicable) and
// body have been resolved.
func (p *DefConstraint) Finalise() {
p.finalised = true
}

// Lisp converts this node into its lisp representation. This is primarily used
// for debugging purposes.
func (p *DefConstraint) Lisp() sexp.SExp {
Expand Down Expand Up @@ -399,6 +480,8 @@ type DefInRange struct {
// an fr.Element is used here to store the bound simply to make the
// necessary comparison against table data more direct.
Bound fr.Element
// Indicates whether or not the expression has been resolved.
finalised bool
}

// Definitions returns the set of symbols defined by this declaration. Observe
Expand All @@ -412,6 +495,23 @@ func (p *DefInRange) Dependencies() util.Iterator[Symbol] {
return util.NewArrayIterator[Symbol](p.Expr.Dependencies())
}

// 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 (p *DefInRange) Defines(symbol Symbol) bool {
return false
}

// IsFinalised checks whether this declaration has already been finalised. If
// so, then we don't need to finalise it again.
func (p *DefInRange) IsFinalised() bool {
return p.finalised
}

// Finalise this declaration, meaning that the expression has been resolved.
func (p *DefInRange) Finalise() {
p.finalised = true
}

// Lisp converts this node into its lisp representation. This is primarily used
// for debugging purposes.
func (p *DefInRange) Lisp() sexp.SExp {
Expand Down Expand Up @@ -453,6 +553,18 @@ func (p *DefInterleaved) Dependencies() util.Iterator[Symbol] {
return util.NewArrayIterator(p.Sources)
}

// 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 (p *DefInterleaved) Defines(symbol Symbol) bool {
return &p.Target.binding == symbol.Binding()
}

// IsFinalised checks whether this declaration has already been finalised. If
// so, then we don't need to finalise it again.
func (p *DefInterleaved) IsFinalised() bool {
return p.Target.binding.IsFinalised()
}

// Lisp converts this node into its lisp representation. This is primarily used
// for debugging purposes.
func (p *DefInterleaved) Lisp() sexp.SExp {
Expand Down Expand Up @@ -495,6 +607,8 @@ type DefLookup struct {
// Target expressions for lookup (i.e. these values must contain all of the
// source values, but may contain more).
Targets []Expr
// Indicates whether or not target and source expressions have been resolved.
finalised bool
}

// Definitions returns the set of symbols defined by this declaration. Observe
Expand All @@ -511,6 +625,24 @@ func (p *DefLookup) Dependencies() util.Iterator[Symbol] {
return util.NewArrayIterator(append(sourceDeps, targetDeps...))
}

// 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 (p *DefLookup) Defines(symbol Symbol) bool {
return false
}

// IsFinalised checks whether this declaration has already been finalised. If
// so, then we don't need to finalise it again.
func (p *DefLookup) IsFinalised() bool {
return p.finalised
}

// Finalise this declaration, which means that all source and target expressions
// have been resolved.
func (p *DefLookup) Finalise() {
p.finalised = true
}

// Lisp converts this node into its lisp representation. This is primarily used
// for debugging purposes.
func (p *DefLookup) Lisp() sexp.SExp {
Expand Down Expand Up @@ -559,6 +691,30 @@ func (p *DefPermutation) Dependencies() util.Iterator[Symbol] {
return util.NewArrayIterator(p.Sources)
}

// 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 (p *DefPermutation) Defines(symbol Symbol) bool {
for _, col := range p.Targets {
if &col.binding == symbol.Binding() {
return true
}
}
// Done
return false
}

// IsFinalised checks whether this declaration has already been finalised. If
// so, then we don't need to finalise it again.
func (p *DefPermutation) IsFinalised() bool {
for _, col := range p.Targets {
if !col.binding.IsFinalised() {
return false
}
}
// Done
return true
}

// Lisp converts this node into its lisp representation. This is primarily used
// for debugging purposes.
func (p *DefPermutation) Lisp() sexp.SExp {
Expand Down Expand Up @@ -606,6 +762,8 @@ type DefProperty struct {
// The assertion itself which (when active) should evaluate to zero for the
// relevant set of rows.
Assertion Expr
// Indicates whether or not the assertion has been resolved.
finalised bool
}

// Definitions returns the set of symbols defined by this declaration. Observe that
Expand All @@ -619,6 +777,23 @@ func (p *DefProperty) Dependencies() util.Iterator[Symbol] {
return util.NewArrayIterator(p.Assertion.Dependencies())
}

// 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 (p *DefProperty) Defines(symbol Symbol) bool {
return false
}

// IsFinalised checks whether this declaration has already been finalised. If
// so, then we don't need to finalise it again.
func (p *DefProperty) IsFinalised() bool {
return p.finalised
}

// Finalise this property, meaning that the assertion has been resolved.
func (p *DefProperty) Finalise() {
p.finalised = true
}

// Lisp converts this node into its lisp representation. This is primarily used
// for debugging purposes.
func (p *DefProperty) Lisp() sexp.SExp {
Expand Down Expand Up @@ -703,6 +878,18 @@ func (p *DefFun) Dependencies() util.Iterator[Symbol] {
return util.NewArrayIterator(ndeps)
}

// 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 (p *DefFun) Defines(symbol Symbol) bool {
return &p.binding == symbol.Binding()
}

// IsFinalised checks whether this declaration has already been finalised. If
// so, then we don't need to finalise it again.
func (p *DefFun) IsFinalised() bool {
return p.binding.IsFinalised()
}

// Lisp converts this node into its lisp representation. This is primarily used
// for debugging purposes.
func (p *DefFun) Lisp() sexp.SExp {
Expand Down Expand Up @@ -737,5 +924,5 @@ type DefParameter struct {
// Lisp converts this node into its lisp representation. This is primarily used
// for debugging purposes.
func (p *DefParameter) Lisp() sexp.SExp {
panic("got here")
return sexp.NewSymbol(p.Name)
}
File renamed without changes.
Loading

0 comments on commit 25e6c0e

Please sign in to comment.