Documentation
¶
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 (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) Unmarshal(r io.Reader, opts UnmarshalOpts) error
- func (c *Closure) UnmarshalYAML(node *yaml.Node) error
- type Def
- type Domain
- type Pos
- type String
- type Top
- type Tuple
- type UnmarshalOpts
- type Value
- type Var
Examples ¶
Constants ¶
This section is empty.
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 }
Functions ¶
This section is empty.
Types ¶
type Closure ¶
type Closure struct {
// contains filtered or unexported fields
}
func Unify ¶
Unify computes a Closure that satisfies each input Closure. If no such Closure exists, it returns bottom.
func (Closure) All ¶
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
- {a: 1, b: 3}
- {a: 1, b: 4}
- {a: 2, b: 3}
- {a: 2, b: 4}
Example (Def) ¶
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) ¶
v := mustParse(` - !sum [1, 2] - !sum [3, 4] `) printYaml(slices.Collect(v.All()))
Output: - [1, 3] - [1, 4] - [2, 3] - [2, 4]
func (Closure) MarshalYAML ¶
func (Closure) Summands ¶
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) Unmarshal ¶
func (c *Closure) Unmarshal(r io.Reader, opts UnmarshalOpts) error
Unmarshal is like [UnmarshalYAML], but accepts options and reads from r. If opts.Path is "" and r has a Name() string method, the result of r.Name() is used as the path for all [Value]s read from r.
func (*Closure) UnmarshalYAML ¶
UnmarshalYAML unmarshals a YAML node into a Closure.
This is how UnmarshalYAML maps YAML nodes into terminal Values:
- "_" 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).
This is how UnmarshalYAML maps YAML nodes into non-terminal Values:
- 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.
type Def ¶
type Def struct {
// contains filtered or unexported fields
}
A Def is a mapping from field names to [Value]s. Any fields not explicitly listed have Value Top.
type Domain ¶
type Domain interface {
Exact() bool
// contains filtered or unexported methods
}
A Domain is a non-empty set of values, all of the same kind.
Domain may be a scalar:
- String - Represents string-typed values.
Or a composite:
Def - A mapping from fixed keys to [Domain]s.
Tuple - A fixed-length sequence of [Domain]s or all possible lengths repeating a Domain.
Or top or bottom:
Top - Represents all possible values of all kinds.
nil - Represents no values.
Or a variable:
- Var - A value captured in the environment.
type String ¶
type String struct {
// contains filtered or unexported fields
}
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.
func NewStringExact ¶
func NewStringRegex ¶
type Tuple ¶
type Tuple struct {
// contains filtered or unexported fields
}
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 UnmarshalOpts ¶
type UnmarshalOpts struct {
// Path is the file path to store in the [Pos] of all [Value]s.
Path string
// StringReplacer, if non-nil, is called for each string value to perform
// any application-specific string interpolation.
StringReplacer func(string) string
}
UnmarshalOpts provides options to unmarshaling. The zero value is the default options.
type Value ¶
type Value struct {
Domain Domain
// contains filtered or unexported fields
}
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.
func NewValuePos ¶
NewValuePos returns a new Value with the given domain at position p.
func (*Value) Decode ¶
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.
func (*Value) MarshalYAML ¶
func (*Value) Provenance ¶
Provenance iterates over all of the source Values that have contributed to this Value.
Source Files