...
Run Format

Package unify

import "simd/archsimd/_gen/unify"
Overview
Index
Examples

Overview ▾

Package unify implements unification of structured values.

A Value represents a possibly infinite set of concrete values, where a value is either a string (String), a tuple of values (Tuple), or a string-keyed map of values called a "def" (Def). These sets can be further constrained by variables (Var). A Value combined with bindings of variables is a Closure.

Unify finds a Closure that satisfies two or more other [Closure]s. This can be thought of as intersecting the sets represented by these Closures' values, or as the greatest lower bound/infimum of these Closures. If no such Closure exists, the result of unification is "bottom", or the empty set.

Examples

The regular expression "a*" is the infinite set of strings of zero or more "a"s. "a*" can be unified with "a" or "aa" or "aaa", and the result is just "a", "aa", or "aaa", respectively. However, unifying "a*" with "b" fails because there are no values that satisfy both.

Sums express sets directly. For example, !sum [a, b] is the set consisting of "a" and "b". Unifying this with !sum [b, c] results in just "b". This also makes it easy to demonstrate that unification isn't necessarily a single concrete value. For example, unifying !sum [a, b, c] with !sum [b, c, d] results in two concrete values: "b" and "c".

The special value _ or "top" represents all possible values. Unifying _ with any value x results in x.

Unifying composite values—tuples and defs—unifies their elements.

The value [a*, aa] is an infinite set of tuples. If we unify that with the value [aaa, a*], the only possible value that satisfies both is [aaa, aa]. Likewise, this is the intersection of the sets described by these two values.

Defs are similar to tuples, but they are indexed by strings and don't have a fixed length. For example, {x: a, y: b} is a def with two fields. Any field not mentioned in a def is implicitly top. Thus, unifying this with {y: b, z: c} results in {x: a, y: b, z: c}.

Variables constrain values. For example, the value [$x, $x] represents all tuples whose first and second values are the same, but doesn't otherwise constrain that value. Thus, this set includes [a, a] as well as [[b, c, d], [b, c, d]], but it doesn't include [a, b].

Sums are internally implemented as fresh variables that are simultaneously bound to all values of the sum. That is !sum [a, b] is actually $var (where var is some fresh name), closed under the environment $var=a | $var=b.

Index ▾

Variables
type Closure
    func NewSum(vs ...*Value) Closure
    func Read(r io.Reader, path string, opts ReadOpts) (Closure, error)
    func ReadFile(path string, opts ReadOpts) (Closure, error)
    func Unify(closures ...Closure) (Closure, error)
    func (c Closure) All() iter.Seq[*Value]
    func (c Closure) IsBottom() bool
    func (c Closure) MarshalYAML() (any, error)
    func (c Closure) String() string
    func (c Closure) Summands() iter.Seq[*Value]
    func (c *Closure) UnmarshalYAML(node *yaml.Node) error
type Decoder
type Def
    func (d Def) All() iter.Seq2[string, *Value]
    func (d Def) Exact() bool
    func (d Def) WhyNotExact() string
type DefBuilder
    func (b *DefBuilder) Add(name string, v *Value)
    func (b *DefBuilder) Build() Def
type Domain
type Pos
    func (p Pos) AppendText(b []byte) ([]byte, error)
    func (p Pos) String() string
type ReadOpts
type String
    func NewStringExact(s string) String
    func NewStringRegex(exprs ...string) (String, error)
    func (d String) Exact() bool
    func (d String) WhyNotExact() string
type Top
    func (t Top) Exact() bool
    func (t Top) WhyNotExact() string
type Tuple
    func NewRepeat(gens ...func(envSet) (*Value, envSet)) Tuple
    func NewTuple(vs ...*Value) Tuple
    func (d Tuple) Exact() bool
    func (d Tuple) WhyNotExact() string
type Value
    func NewValue(d Domain) *Value
    func NewValuePos(d Domain, p Pos) *Value
    func (v *Value) Decode(into any) error
    func (v *Value) Exact() bool
    func (v *Value) MarshalYAML() (any, error)
    func (v *Value) Pos() Pos
    func (v *Value) PosString() string
    func (v *Value) Provenance() iter.Seq[*Value]
    func (v *Value) String() string
    func (v *Value) WhyNotExact() string
type Var
    func (d Var) Exact() bool
    func (d Var) WhyNotExact() string

Examples

Closure.All (Def)
Closure.All (Tuple)

Package files

closure.go domain.go dot.go env.go html.go pos.go trace.go unify.go value.go yaml.go

Variables

var Debug struct {
    // UnifyLog, if non-nil, receives a streaming text trace of unification.
    UnifyLog io.Writer

    // HTML, if non-nil, writes an HTML trace of unification to HTML.
    HTML io.Writer
}

type Closure

type Closure struct {
    // contains filtered or unexported fields
}

func NewSum

func NewSum(vs ...*Value) Closure

func Read

func Read(r io.Reader, path string, opts ReadOpts) (Closure, error)

Read reads a Closure in YAML format from r, using path for error messages.

It maps YAML nodes into terminal Values as follows:

- "_" or !top _ is the top value (Top).

- "_|_" or !bottom _ is the bottom value. This is an error during unmarshaling, but can appear in marshaled values.

- "$<name>" or !var <name> is a variable (Var). Everywhere the same name appears within a single unmarshal operation, it is mapped to the same variable. Different unmarshal operations get different variables, even if they have the same string name.

- !regex "x" is a regular expression (String), as is any string that doesn't match "_", "_|_", or "$...". Regular expressions are implicitly anchored at the beginning and end. If the string doesn't contain any meta-characters (that is, it's a "literal" regular expression), then it's treated as an exact string.

- !string "x", or any int, float, bool, or binary value is an exact string (String).

- !regex [x, y, ...] is an intersection of regular expressions (String).

It maps YAML nodes into non-terminal Values as follows:

- Sequence nodes like [x, y, z] are tuples (Tuple).

- !repeat [x] is a repeated tuple (Tuple), which is 0 or more instances of x. There must be exactly one element in the list.

- Mapping nodes like {a: x, b: y} are defs (Def). Any fields not listed are implicitly top.

- !sum [x, y, z] is a sum of its children. This can be thought of as a union of the values x, y, and z, or as a non-deterministic choice between x, y, and z. If a variable appears both inside the sum and outside of it, only the non-deterministic choice view really works. The unifier does not directly implement sums; instead, this is decoded as a fresh variable that's simultaneously bound to x, y, and z.

- !import glob is like a !sum, but its children are read from all files matching the given glob pattern, which is interpreted relative to the current file path. Each file gets its own variable scope.

func ReadFile

func ReadFile(path string, opts ReadOpts) (Closure, error)

ReadFile reads a Closure in YAML format from a file.

The file must consist of a single YAML document.

If opts.FS is not set, this sets it to a FS rooted at path's directory.

See Read for details.

func Unify

func Unify(closures ...Closure) (Closure, error)

Unify computes a Closure that satisfies each input Closure. If no such Closure exists, it returns bottom.

func (Closure) All

func (c Closure) All() iter.Seq[*Value]

All enumerates all possible concrete values of c by substituting variables from the environment.

E.g., enumerating this Value

a: !sum [1, 2]
b: !sum [3, 4]

results in

Example (Def)

Code:

v := mustParse(`
a: !sum [1, 2]
b: !sum [3, 4]
c: 5
`)
printYaml(slices.Collect(v.All()))

Output:

- {a: 1, b: 3, c: 5}
- {a: 1, b: 4, c: 5}
- {a: 2, b: 3, c: 5}
- {a: 2, b: 4, c: 5}

Example (Tuple)

Code:

v := mustParse(`
- !sum [1, 2]
- !sum [3, 4]
`)
printYaml(slices.Collect(v.All()))

Output:

- [1, 3]
- [1, 4]
- [2, 3]
- [2, 4]

func (Closure) IsBottom

func (c Closure) IsBottom() bool

IsBottom returns whether c consists of no values.

func (Closure) MarshalYAML

func (c Closure) MarshalYAML() (any, error)

func (Closure) String

func (c Closure) String() string

func (Closure) Summands

func (c Closure) Summands() iter.Seq[*Value]

Summands returns the top-level Values of c. This assumes the top-level of c was constructed as a sum, and is mostly useful for debugging.

func (*Closure) UnmarshalYAML

func (c *Closure) UnmarshalYAML(node *yaml.Node) error

UnmarshalYAML implements yaml.Unmarshaler.

Since there is no way to pass ReadOpts to this function, it assumes default options.

type Decoder

Decoder can be implemented by types as a custom implementation of [Decode] for that type.

type Decoder interface {
    DecodeUnified(v *Value) error
}

type Def

A Def is a mapping from field names to [Value]s. Any fields not explicitly listed have Value Top.

type Def struct {
    // contains filtered or unexported fields
}

func (Def) All

func (d Def) All() iter.Seq2[string, *Value]

func (Def) Exact

func (d Def) Exact() bool

Exact returns true if all field Values are exact.

func (Def) WhyNotExact

func (d Def) WhyNotExact() string

WhyNotExact returns why the value is not exact

type DefBuilder

A DefBuilder builds a Def one field at a time. The zero value is an empty Def.

type DefBuilder struct {
    // contains filtered or unexported fields
}

func (*DefBuilder) Add

func (b *DefBuilder) Add(name string, v *Value)

func (*DefBuilder) Build

func (b *DefBuilder) Build() Def

Build constructs a Def from the fields added to this builder.

type Domain

A Domain is a non-empty set of values, all of the same kind.

Domain may be a scalar:

Or a composite:

Or top or bottom:

Or a variable:

type Domain interface {
    Exact() bool
    WhyNotExact() string
    // contains filtered or unexported methods
}

type Pos

type Pos struct {
    Path string
    Line int
}

func (Pos) AppendText

func (p Pos) AppendText(b []byte) ([]byte, error)

func (Pos) String

func (p Pos) String() string

type ReadOpts

ReadOpts provides options to Read and related functions. The zero value is the default options.

type ReadOpts struct {
    // FS, if non-nil, is the file system from which to resolve !import file
    // names.
    FS fs.FS
}

type String

A String represents a set of strings. It can represent the intersection of a set of regexps, or a single exact string. In general, the domain of a String is non-empty, but we do not attempt to prove emptiness of a regexp value.

type String struct {
    // contains filtered or unexported fields
}

func NewStringExact

func NewStringExact(s string) String

func NewStringRegex

func NewStringRegex(exprs ...string) (String, error)

func (String) Exact

func (d String) Exact() bool

Exact returns whether this Value is known to consist of a single string.

func (String) WhyNotExact

func (d String) WhyNotExact() string

type Top

Top represents all possible values of all possible types.

type Top struct{}

func (Top) Exact

func (t Top) Exact() bool

func (Top) WhyNotExact

func (t Top) WhyNotExact() string

type Tuple

A Tuple is a sequence of Values in one of two forms: 1. a fixed-length tuple, where each Value can be different or 2. a "repeated tuple", which is a Value repeated 0 or more times.

type Tuple struct {
    // contains filtered or unexported fields
}

func NewRepeat

func NewRepeat(gens ...func(envSet) (*Value, envSet)) Tuple

func NewTuple

func NewTuple(vs ...*Value) Tuple

func (Tuple) Exact

func (d Tuple) Exact() bool

func (Tuple) WhyNotExact

func (d Tuple) WhyNotExact() string

type Value

A Value represents a structured, non-deterministic value consisting of strings, tuples of Values, and string-keyed maps of Values. A non-deterministic Value will also contain variables, which are resolved via an environment as part of a Closure.

For debugging, a Value can also track the source position it was read from in an input file, and its provenance from other Values.

type Value struct {
    Domain Domain
    // contains filtered or unexported fields
}

func NewValue

func NewValue(d Domain) *Value

NewValue returns a new Value with the given domain and no position information.

func NewValuePos

func NewValuePos(d Domain, p Pos) *Value

NewValuePos returns a new Value with the given domain at position p.

func (*Value) Decode

func (v *Value) Decode(into any) error

Decode decodes v into a Go value.

v must be exact, except that it can include Top. into must be a pointer. [Def]s are decoded into structs. [Tuple]s are decoded into slices. [String]s are decoded into strings or ints. Any field can itself be a pointer to one of these types. Top can be decoded into a pointer-typed field and will set the field to nil. Anything else will allocate a value if necessary.

Any type may implement Decoder, in which case its DecodeUnified method will be called instead of using the default decoding scheme.

func (*Value) Exact

func (v *Value) Exact() bool

func (*Value) MarshalYAML

func (v *Value) MarshalYAML() (any, error)

func (*Value) Pos

func (v *Value) Pos() Pos

func (*Value) PosString

func (v *Value) PosString() string

func (*Value) Provenance

func (v *Value) Provenance() iter.Seq[*Value]

Provenance iterates over all of the source Values that have contributed to this Value.

func (*Value) String

func (v *Value) String() string

func (*Value) WhyNotExact

func (v *Value) WhyNotExact() string

type Var

type Var struct {
    // contains filtered or unexported fields
}

func (Var) Exact

func (d Var) Exact() bool

func (Var) WhyNotExact

func (d Var) WhyNotExact() string