mirror of
https://github.com/golang/go.git
synced 2025-12-08 06:10:04 +00:00
155 lines
4.1 KiB
Go
155 lines
4.1 KiB
Go
|
|
// Copyright 2025 The Go Authors. All rights reserved.
|
||
|
|
// Use of this source code is governed by a BSD-style
|
||
|
|
// license that can be found in the LICENSE file.
|
||
|
|
|
||
|
|
package unify
|
||
|
|
|
||
|
|
import (
|
||
|
|
"fmt"
|
||
|
|
"iter"
|
||
|
|
"maps"
|
||
|
|
"slices"
|
||
|
|
)
|
||
|
|
|
||
|
|
type Closure struct {
|
||
|
|
val *Value
|
||
|
|
env envSet
|
||
|
|
}
|
||
|
|
|
||
|
|
func NewSum(vs ...*Value) Closure {
|
||
|
|
id := &ident{name: "sum"}
|
||
|
|
return Closure{NewValue(Var{id}), topEnv.bind(id, vs...)}
|
||
|
|
}
|
||
|
|
|
||
|
|
// IsBottom returns whether c consists of no values.
|
||
|
|
func (c Closure) IsBottom() bool {
|
||
|
|
return c.val.Domain == nil
|
||
|
|
}
|
||
|
|
|
||
|
|
// 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 (c Closure) Summands() iter.Seq[*Value] {
|
||
|
|
return func(yield func(*Value) bool) {
|
||
|
|
var rec func(v *Value, env envSet) bool
|
||
|
|
rec = func(v *Value, env envSet) bool {
|
||
|
|
switch d := v.Domain.(type) {
|
||
|
|
case Var:
|
||
|
|
parts := env.partitionBy(d.id)
|
||
|
|
for _, part := range parts {
|
||
|
|
// It may be a sum of sums. Walk into this value.
|
||
|
|
if !rec(part.value, part.env) {
|
||
|
|
return false
|
||
|
|
}
|
||
|
|
}
|
||
|
|
return true
|
||
|
|
default:
|
||
|
|
return yield(v)
|
||
|
|
}
|
||
|
|
}
|
||
|
|
rec(c.val, c.env)
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
// 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}
|
||
|
|
func (c Closure) All() iter.Seq[*Value] {
|
||
|
|
// In order to enumerate all concrete values under all possible variable
|
||
|
|
// bindings, we use a "non-deterministic continuation passing style" to
|
||
|
|
// implement this. We use CPS to traverse the Value tree, threading the
|
||
|
|
// (possibly narrowing) environment through that CPS following an Euler
|
||
|
|
// tour. Where the environment permits multiple choices, we invoke the same
|
||
|
|
// continuation for each choice. Similar to a yield function, the
|
||
|
|
// continuation can return false to stop the non-deterministic walk.
|
||
|
|
return func(yield func(*Value) bool) {
|
||
|
|
c.val.all1(c.env, func(v *Value, e envSet) bool {
|
||
|
|
return yield(v)
|
||
|
|
})
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
func (v *Value) all1(e envSet, cont func(*Value, envSet) bool) bool {
|
||
|
|
switch d := v.Domain.(type) {
|
||
|
|
default:
|
||
|
|
panic(fmt.Sprintf("unknown domain type %T", d))
|
||
|
|
|
||
|
|
case nil:
|
||
|
|
return true
|
||
|
|
|
||
|
|
case Top, String:
|
||
|
|
return cont(v, e)
|
||
|
|
|
||
|
|
case Def:
|
||
|
|
fields := d.keys()
|
||
|
|
// We can reuse this parts slice because we're doing a DFS through the
|
||
|
|
// state space. (Otherwise, we'd have to do some messy threading of an
|
||
|
|
// immutable slice-like value through allElt.)
|
||
|
|
parts := make(map[string]*Value, len(fields))
|
||
|
|
|
||
|
|
// TODO: If there are no Vars or Sums under this Def, then nothing can
|
||
|
|
// change the Value or env, so we could just cont(v, e).
|
||
|
|
var allElt func(elt int, e envSet) bool
|
||
|
|
allElt = func(elt int, e envSet) bool {
|
||
|
|
if elt == len(fields) {
|
||
|
|
// Build a new Def from the concrete parts. Clone parts because
|
||
|
|
// we may reuse it on other non-deterministic branches.
|
||
|
|
nVal := newValueFrom(Def{maps.Clone(parts)}, v)
|
||
|
|
return cont(nVal, e)
|
||
|
|
}
|
||
|
|
|
||
|
|
return d.fields[fields[elt]].all1(e, func(v *Value, e envSet) bool {
|
||
|
|
parts[fields[elt]] = v
|
||
|
|
return allElt(elt+1, e)
|
||
|
|
})
|
||
|
|
}
|
||
|
|
return allElt(0, e)
|
||
|
|
|
||
|
|
case Tuple:
|
||
|
|
// Essentially the same as Def.
|
||
|
|
if d.repeat != nil {
|
||
|
|
// There's nothing we can do with this.
|
||
|
|
return cont(v, e)
|
||
|
|
}
|
||
|
|
parts := make([]*Value, len(d.vs))
|
||
|
|
var allElt func(elt int, e envSet) bool
|
||
|
|
allElt = func(elt int, e envSet) bool {
|
||
|
|
if elt == len(d.vs) {
|
||
|
|
// Build a new tuple from the concrete parts. Clone parts because
|
||
|
|
// we may reuse it on other non-deterministic branches.
|
||
|
|
nVal := newValueFrom(Tuple{vs: slices.Clone(parts)}, v)
|
||
|
|
return cont(nVal, e)
|
||
|
|
}
|
||
|
|
|
||
|
|
return d.vs[elt].all1(e, func(v *Value, e envSet) bool {
|
||
|
|
parts[elt] = v
|
||
|
|
return allElt(elt+1, e)
|
||
|
|
})
|
||
|
|
}
|
||
|
|
return allElt(0, e)
|
||
|
|
|
||
|
|
case Var:
|
||
|
|
// Go each way this variable can be bound.
|
||
|
|
for _, ePart := range e.partitionBy(d.id) {
|
||
|
|
// d.id is no longer bound in this environment partition. We'll may
|
||
|
|
// need it later in the Euler tour, so bind it back to this single
|
||
|
|
// value.
|
||
|
|
env := ePart.env.bind(d.id, ePart.value)
|
||
|
|
if !ePart.value.all1(env, cont) {
|
||
|
|
return false
|
||
|
|
}
|
||
|
|
}
|
||
|
|
return true
|
||
|
|
}
|
||
|
|
}
|