ast

package
v0.2.0 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Aug 14, 2024 License: Apache-2.0 Imports: 9 Imported by: 1

Documentation

Overview

Package ast contains abstract syntax tree representations of Mangle code.

Index

Constants

View Source 
const (
	// DescrExtensional is a descriptor for extensional predicates.
	DescrExtensional = "extensional"
	// DescrMode is a descriptor for a supported mode of a predicate.
	DescrMode = "mode"
	// DescrReflects is a descriptor for predicates that test ("reflect") name prefixes
	DescrReflects = "reflects"
	// DescrSynthetic is a descriptor for synthetic declarations.
	DescrSynthetic = "synthetic"
	// DescrPrivate is a descriptor for a predicate with package-private visibility.
	DescrPrivate = "private"
	// DescrDoc is a descriptor containing documentation.
	DescrDoc = "doc"
	// DescrArg is a descriptor containing documentation for an argument.
	DescrArg = "arg"
	// DescrName is a descriptor used internally for naming a declared object.
	DescrName = "name"
	// DescrDesugared is a descriptor used internally to mark desugared declarations.
	DescrDesugared = "desugared"
	// DescrFunDep is a descriptor for a functional dependency.
	DescrFunDep = "fundep"
	// DescrMergePredicate is a descriptor for a merge predicate.
	DescrMergePredicate = "merge"
	// DescrDeferredPredicate is a descriptor for a deferred predicate.
	DescrDeferredPredicate = "deferred"
)
View Source 
const (
	// ArgModeInput indicates an input to the predicate "+"
	ArgModeInput ArgMode = 0b001
	// ArgModeOutput indicates an output to the predicate "-"
	ArgModeOutput = 0b010
	// ArgModeInputOutput indicates that an argument can be either input or output.
	ArgModeInputOutput = 0b100
)
View Source 
const (
	// InputString indicates an argument that is input.
	InputString = "+"
	// OutputString indicates an argument that is output.
	OutputString = "-"
	// InputOutputString indicates an argument that can either be input or output.
	InputOutputString = "?"
)
View Source 
const InternalPredicateSuffix = "__tmp"

InternalPredicateSuffix gets appended to all internal predicate symbol names.

Variables

View Source 
var FalsePredicate = PredicateSym{"false", 0}

FalsePredicate is a predicate symbol to represent an "unconditionally false" proposition.

View Source 
var ListNil = Constant{ListShape, "", 0, nil, nil}

ListNil represents an empty list.

View Source 
var MapNil = Constant{MapShape, "", 0, nil, nil}

MapNil represents an empty map.

View Source 
var StructNil = Constant{StructShape, "", 0, nil, nil}

StructNil represents an empty struct.

View Source 
var TruePredicate = PredicateSym{"true", 0}

TruePredicate is a predicate symbol to represent an "unconditionally true" proposition.

Functions

func AddVars 

func AddVars(term Term, m map[Variable]bool)

AddVars adds all variables from term to map, where term is either variable, constant or atom.

func AddVarsFromClause 

func AddVarsFromClause(clause Clause, m map[Variable]bool)

AddVarsFromClause adds all variables from term to map, where term is either variable, constant or atom.

func Escape added in v0.2.0 

func Escape(str string, isBytes bool) (string, error)

Escape returns a Mangle source representation of a string. In !isBytes mode: - newlines are escaped as \n, tags as \t - other control characters [0x00..0x20] are byte-escaped, - Quote characters " and ' are character-escaped, - UTF8 sequences for code points > 0x80 are unicode-escaped. In isBytes mode: - all characters [0x00..0x20] and [0x80...0xFF] are byte-escaped. - quote characters " and ' are byte-escaped,

func FormatFloat64 

func FormatFloat64(floatNum float64) string

FormatFloat64 turns a float64 constant into a string.

func FormatNumber 

func FormatNumber(num int64) string

FormatNumber turns a number constant into a string.

func SortIndexInto 

func SortIndexInto(keys []*Constant, index []int)

SortIndexInto sorts s and populates the index and hashes slice.

func Unescape added in v0.2.0 

func Unescape(s string, isBytes bool) (string, error)

Unescape returns the Mangle source representation of a string and returns a string.

  • if !isBytes, replaces \x0d \x0a sequences and single \x0d with single \x0a (remove carriage return).
  • replaces '\” '\"' '\\' with corresponding character
  • replaces '\n' '\t ' with whitespace character
  • replaces '\xHH' with byte. Unless `isBytes` is true, checks that result is UTF8 compatible, i.e. in strings only 0x00..0x7F are permitted, in bytestrings anything goes.
  • replaces escapes \u{hhhhh?h?} with UTF8 byte sequences, checks that result is unicode code point.

Types

type ApplyFn 

type ApplyFn struct {
	Function FunctionSym
	Args     []BaseTerm
}

ApplyFn is a function application like "fn:max(X)".

func (ApplyFn) ApplySubst 

func (a ApplyFn) ApplySubst(s Subst) Term

ApplySubst returns the result of applying given substitution to this atom.

func (ApplyFn) ApplySubstBase 

func (a ApplyFn) ApplySubstBase(s Subst) BaseTerm

ApplySubstBase simply returns this constant, for any substitution.

func (ApplyFn) Equals 

func (a ApplyFn) Equals(t Term) bool

Equals checks equality of ApplyFn terms.

func (ApplyFn) Hash 

func (a ApplyFn) Hash() uint64

Hash returns a hash code for this expression.

func (ApplyFn) String 

func (a ApplyFn) String() string

String returns a string representation for this atom.

type ArgMode 

type ArgMode int

ArgMode is an enum specifying whether an argument is input, output, or both.

type Atom 

type Atom struct {
	Predicate PredicateSym
	Args      []BaseTerm
}

Atom represents an atom (a predicate symbol applied to base term arguments). e.g: parent(A, B)

func NewAtom 

func NewAtom(predicateSym string, args ...BaseTerm) Atom

NewAtom is a convenience constructor for Atom.

func NewQuery 

func NewQuery(predicate PredicateSym) Atom

NewQuery is a convenience constructor for constructing a goal atom.

func (Atom) ApplySubst 

func (a Atom) ApplySubst(s Subst) Term

ApplySubst returns the result of applying given substitution to this atom.

func (Atom) Equals 

func (a Atom) Equals(u Term) bool

Equals provides syntactic equality for atoms.

func (Atom) Hash 

func (a Atom) Hash() uint64

Hash returns a hash code for this atom.

func (Atom) IsGround 

func (a Atom) IsGround() bool

IsGround returns true if all arguments are constants.

func (Atom) String 

func (a Atom) String() string

String returns a string representation for this atom.

type BaseTerm 

type BaseTerm interface {
	Term

	Hash() uint64

	// Returns a new base term.
	ApplySubstBase(s Subst) BaseTerm
	// contains filtered or unexported methods
}

BaseTerm represents a subset of terms: constant, variables or ApplyFn. Every BaseTerm will implement Term.

type BoundDecl 

type BoundDecl struct {
	Bounds []BaseTerm
}

BoundDecl is a bound declaration for the arguments of a predicate.

A bound declaration is either a type-expression (a type bound) or a reference to a unary predicate (a predicate bound).

The BaseTerm t represents a set of constants |t| as follows: - |/any| is a type whose elements are all values - |/name| is a type whose elements are name constants - |/number| is a type whose elements are numbers - |/string| is a type whose elements are strings - "$pred" if the model satisfies $pred(X). This is not a type but 

a short way to add an inclusion constraint. Predicate bounds
must not be recursive and resolvable to a type bound t which
can be used for type-checking. This |t| is used as an
upper bound for the elements.

(In the following all subexpression must be type bounds:) - fn:Pair(s, t) if the argument is a pair whose first 

element is in s and whose second element is in t.

- fn:List(t) if the argument is a list - fn:Tuple(s1,...,sN) for N > 2 is a shorthand for type 

fn:Pair(s1, fn:Pair(...fn:Pair(N-1,sN)...))

- fn:Union(s1,...,sN) is the type whose elements are 

included in at least one of types s1, ..., sN.

This list is incomplete in two ways: - There are type expressions that are not permitted in bound declarations, and - extensions may provide further type expressions that are permitted in bound declarations.

func NewBoundDecl 

func NewBoundDecl(bounds ...BaseTerm) BoundDecl

NewBoundDecl returns a new BoundDecl.

type Clause 

type Clause struct {
	Head      Atom
	Premises  []Term
	Transform *Transform
}

Clause represents a clause (a rule of the form "A." or "A :- B1, ..., Bn."). When a clause has a body, the resulting relation can be transformed.

func NewClause 

func NewClause(head Atom, premises []Term) Clause

NewClause constructs a new clause.

func (Clause) ReplaceWildcards 

func (c Clause) ReplaceWildcards() Clause

ReplaceWildcards returns a new clause where each wildcard is replaced with a fresh variable.

func (Clause) String 

func (c Clause) String() string

type ConstSubstList 

type ConstSubstList []ConstSubstPair

ConstSubstList is a substitution backed by a slice of (variable, constant) pairs.

func (ConstSubstList) Extend 

func (c ConstSubstList) Extend(v Variable, con Constant) ConstSubstList

Extend extends this substitution with a new binding.

func (ConstSubstList) Get 

func (c ConstSubstList) Get(v Variable) BaseTerm

Get implements the Get method from Subst.

type ConstSubstMap 

type ConstSubstMap map[Variable]Constant

ConstSubstMap is a substitution backed by a map from variables to constants.

func (ConstSubstMap) Get 

func (m ConstSubstMap) Get(v Variable) BaseTerm

Get implements the Get method from Subst.

type ConstSubstPair 

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

ConstSubstPair represents a (variable, constant) pair.

type Constant 

type Constant struct {
	// The (runtime) type of this constant.
	Type ConstantType

	// If Type \in {StringType, BytesType}, the data itself.
	// Otherwise, a string representation.
	Symbol string

	// For NumberType, the number value (int64 or the bytes of a float64).
	// For other types it contains a hash code of the value.
	NumValue int64
	// contains filtered or unexported fields
}

Constant represents a constant symbol and other structures (e.g. pair, list map, struct). 

var AnyBound Constant

AnyBound is a type expression that has all values as elements. 

var BotBound Constant

BotBound is a type expression that has no elements. 

var BytesBound Constant

BytesBound is a type expression that has all bytestrings as elements. 

var FalseConstant Constant

FalseConstant is the "/false" name constant. 

var Float64Bound Constant

Float64Bound is a type expression that has all float64s as elements. 

var NameBound Constant

NameBound is a type expression that has all names as elements. 

var NumberBound Constant

NumberBound is a type expression that has all numbers as elements. 

var StringBound Constant

StringBound is a type expression that has all strings as elements. 

var TrueConstant Constant

TrueConstant is the "/true" name constant.

func Bytes added in v0.2.0 

func Bytes(bytes []byte) Constant

Bytes constructs a byte string constant.

func Float64 

func Float64(floatNum float64) Constant

Float64 constructs a constant symbol that contains a float64.

func List 

func List(constants []Constant) Constant

List constructs a list constant. Parts can only be accessed in transforms.

func ListCons 

func ListCons(fst, snd *Constant) Constant

ListCons constructs a list, using pairs. Parts can only be accessed in transforms.

func Map 

func Map(kvMap map[*Constant]*Constant) *Constant

Map constructs a map constant. Parts can only be accessed in transforms.

func MapCons 

func MapCons(key, val, rest *Constant) Constant

MapCons constructs a map, using pairs. Parts can only be accessed in transforms.

func Name 

func Name(symbol string) (Constant, error)

Name constructs a new name constant while checking that constant symbol starts with a '/' and does not contain empty parts.

func Number 

func Number(num int64) Constant

Number constructs a constant symbol that contains a number.

func Pair 

func Pair(fst, snd *Constant) Constant

Pair constructs a pair constant. Parts can only be accessed in transforms.

func String 

func String(str string) Constant

String constructs a string constant.

func Struct 

func Struct(kvMap map[*Constant]*Constant) *Constant

Struct constructs a struct constant. Parts can only be accessed in transforms. labels must be sorted .

func StructCons 

func StructCons(label, val, rest *Constant) Constant

StructCons constructs a struct, using pairs. Parts can only be accessed in transforms.

func (Constant) ApplySubst 

func (c Constant) ApplySubst(s Subst) Term

ApplySubst simply returns this constant, for any substitution.

func (Constant) ApplySubstBase 

func (c Constant) ApplySubstBase(s Subst) BaseTerm

ApplySubstBase simply returns this constant, for any substitution.

func (Constant) ConsValue 

func (c Constant) ConsValue() (Constant, Constant, error)

ConsValue returns the two constants that make up this cons.

func (Constant) Equals 

func (c Constant) Equals(u Term) bool

Equals returns true if u is the same constant.

func (Constant) Float64Value 

func (c Constant) Float64Value() (float64, error)

Float64Value returns the float64 value of this constant, if it is of type float64.

func (Constant) Hash 

func (c Constant) Hash() uint64

Hash returns a hash code for this constant

func (Constant) IsListNil 

func (c Constant) IsListNil() bool

IsListNil returns true if this constant represents the empty list.

func (Constant) IsMapNil 

func (c Constant) IsMapNil() bool

IsMapNil returns true if this constant represents the empty map.

func (Constant) IsStructNil 

func (c Constant) IsStructNil() bool

IsStructNil returns true if this constant represents the empty struct.

func (Constant) ListValues 

func (c Constant) ListValues(cbCons func(Constant) error, cbNil func() error) (error, error)

ListValues provides the constants that make up the list via callback.

func (Constant) MapValues 

func (c Constant) MapValues(cbCons func(Constant, Constant) error, cbNil func() error) (error, error)

MapValues provides the entries of the map via key-value callback.

func (Constant) NameValue 

func (c Constant) NameValue() (string, error)

NameValue returns the name value of this constant, if it is of type name.

func (Constant) NumberValue 

func (c Constant) NumberValue() (int64, error)

NumberValue returns the number(int64) value of this constant, if it is of type number.

func (Constant) PairValue 

func (c Constant) PairValue() (Constant, Constant, error)

PairValue returns the two constants that make up this pair.

func (Constant) String 

func (c Constant) String() string

String returns a string representation of the constant.

func (Constant) StringValue 

func (c Constant) StringValue() (string, error)

StringValue returns the string value of this constant, if it is of type string.

func (Constant) StructValues 

func (c Constant) StructValues(cbCons func(Constant, Constant) error, cbNil func() error) (error, error)

StructValues provides the entries that make up the struct via label-value callback.

type ConstantType 

type ConstantType int

ConstantType describes the primitive type or shape of a constant. 

const (
	// NameType is the type of name constants.
	NameType ConstantType = iota
	// StringType is the type of string constants.
	StringType
	// BytesType is the type of byte strings.
	BytesType
	// NumberType is the type of number (int64) constants.
	NumberType
	// Float64Type is the type of float64 constants.
	Float64Type
	// PairShape indicates that the constant is a pair.
	PairShape
	// ListShape indicates that the constant is a list.
	ListShape
	// MapShape indicates that the constant is a map.
	// Internally, we just represent this as list of ($key, $value) pairs.
	MapShape
	// StructShape indicates that the constant is a struct.
	// Internally, we just represent this as a list of (/field/$name, $value) pairs.
	StructShape
)

type Decl 

type Decl struct {
	// Predicate we are defining, with arguments.
	DeclaredAtom Atom

	// Description atoms for this predicate.
	Descr []Atom

	// Upper bounds (may be empty). Each BoundDecl has a matching arity.
	// For example a foo(X,Y) may have bounds (/string x /string) and
	// (foo x /number), which means that X may be /string or foo(X).
	// The idea is that there are a few special unary predicates describing
	// something that could be considered a "type."
	// The bounds form a union (join) so only one of the needs to hold.
	Bounds []BoundDecl

	// Either nil, or an inclusion constraint that holds.
	Constraints *InclusionConstraint
}

Decl is a declaration.

func NewDecl 

func NewDecl(atom Atom, descrAtoms []Atom, bounds []BoundDecl, constraints *InclusionConstraint) (Decl, error)

NewDecl returns a new Decl.

func NewSyntheticDecl 

func NewSyntheticDecl(declaredAtom Atom) (Decl, error)

NewSyntheticDecl returns a new Decl from an atom. The decl has an empty doc, an explicit mode supporting all arguments as input-output, and is marked as being synthetic.

func NewSyntheticDeclFromSym 

func NewSyntheticDeclFromSym(sym PredicateSym) Decl

NewSyntheticDeclFromSym returns a new Decl from a predicate symbol.

func (Decl) DeferredPredicate added in v0.2.0 

func (d Decl) DeferredPredicate() bool

DeferredPredicate returns true if this predicate has the deferred marker.

func (Decl) Doc 

func (d Decl) Doc() []string

Doc returns the doc strings from the Decl's description atoms.

func (Decl) FunDeps added in v0.2.0 

func (d Decl) FunDeps() []FunDep

FunDeps returns functional dependencies.

func (Decl) IsDesugared 

func (d Decl) IsDesugared() bool

IsDesugared returns true if decl has been desugared.

func (Decl) IsExtensional 

func (d Decl) IsExtensional() bool

IsExtensional returns true if decl is for an extensional predicate.

func (Decl) IsSynthetic 

func (d Decl) IsSynthetic() bool

IsSynthetic returns true if this Decl is synthetic (generated).

func (Decl) MergePredicate added in v0.2.0 

func (d Decl) MergePredicate() ([]int, PredicateSym)

MergePredicate returns the information from the merge predicate descriptor.

A merge predicate is a three-place.

func (Decl) Modes 

func (d Decl) Modes() []Mode

Modes returns the supported modes declared for this predicate. Returns nil if the declaration does not declare modes. This is always interpreted as supporting all modes i.e. "?" ... "?".

func (Decl) PackageID 

func (d Decl) PackageID() string

PackageID returns the package part (dirname).

func (Decl) Reflects 

func (d Decl) Reflects() (Constant, bool)

Reflects returns (true, prefix) if this predicate covers ("reflects") a name prefix type.

func (Decl) Visible 

func (d Decl) Visible() bool

Visible returns whether the predicate should be visible to other packages.

type Eq 

type Eq struct {
	Left  BaseTerm
	Right BaseTerm
}

Eq represents an equality (identity constraint) X = Y or X = c or c = X.

func (Eq) ApplySubst 

func (e Eq) ApplySubst(s Subst) Term

ApplySubst returns the result of applying given substitution to this equality.

func (Eq) Equals 

func (e Eq) Equals(u Term) bool

Equals provides syntactic (structural) equality for Eq(left, right) terms.

func (Eq) String 

func (e Eq) String() string

String returns a string representation for this atom.

type FunDep added in v0.2.0 

type FunDep struct {
	Source []int
	Target []int
}

FunDep represents a functional dependency for the components of this relation.

type FunctionSym 

type FunctionSym struct {
	// Symbol is the name of the function, always with "fn:" prefix.
	Symbol string
	Arity  int
}

FunctionSym represents a function symbol with a given arity.

func (FunctionSym) String 

func (f FunctionSym) String() string

type InclusionConstraint 

type InclusionConstraint struct {
	// All of these must hold.
	Consequences []Atom
	// In addition to Consequences, at least one of these must hold.
	Alternatives [][]Atom
}

InclusionConstraint expresses e.g. that if foo(X, Y) holds, then also bar(X) and baz(Y) and xyz(X,Y) hold. This can be a stronger constraint than bound declarations.

Such an inclusion constraint may be entered by the user like this:

Decl foo(X, Y) 

bound ["even", /number]
bound [/number, "odd"]
inclusion [bar(X), baz(Y), xyz(X,Y)].

In order to account for bound declarations with predicate references, which are also inclusion constraints, declarations are desugared. After desugaring, there is one alternative for each bound declaration, all inclusion constraints appear in Alternatives and Consequences is empty, like so (this is not real syntax:)

Decl foo(X, Y) 

bound [/number, /number]
bound [/number, /number]
inclusion-alternative[ even(X), bar(X), baz(Y), xyz(X,Y)].
inclusion-alternative[ odd(Y), bar(X), baz(Y), xyz(X,Y)].

func NewInclusionConstraint 

func NewInclusionConstraint(consequences []Atom) InclusionConstraint

NewInclusionConstraint returns a new InclusionConstraint.

type Ineq 

type Ineq struct {
	Left  BaseTerm
	Right BaseTerm
}

Ineq represents an inequality (apartness constraint) X != Y or X != c or c != X.

func (Ineq) ApplySubst 

func (e Ineq) ApplySubst(s Subst) Term

ApplySubst returns the result of applying given substitution to this inequality.

func (Ineq) Equals 

func (e Ineq) Equals(u Term) bool

Equals provides syntactic (structural) equality for Ineq(left, right) terms.

func (Ineq) String 

func (e Ineq) String() string

String returns a string representation for this atom.

type Mode 

type Mode []ArgMode

Mode specifies the mode of the predicate. A tuple of argument modes.

func (Mode) Check 

func (m Mode) Check(goal Atom, boundVars map[Variable]bool) error

Check checks a goal against this mode and returns an error if it is incompatible.

type NegAtom 

type NegAtom struct {
	Atom Atom
}

NegAtom represents a negated atom.

func NewNegAtom 

func NewNegAtom(predicateSym string, args ...BaseTerm) NegAtom

NewNegAtom is a convenience constructor for NegAtom.

func (NegAtom) ApplySubst 

func (a NegAtom) ApplySubst(s Subst) Term

ApplySubst returns the result of applying given substitution to this atom.

func (NegAtom) Equals 

func (a NegAtom) Equals(u Term) bool

Equals returns true if u is syntactically (structurally) the same negated atom.

func (NegAtom) IsGround 

func (a NegAtom) IsGround() bool

IsGround returns true if all arguments are constants.

func (NegAtom) String 

func (a NegAtom) String() string

String returns a string representation for this atom.

type PredicateSym 

type PredicateSym struct {
	Symbol string
	Arity  int
}

PredicateSym represents a predicate symbol with a given arity.

func (PredicateSym) IsBuiltin 

func (p PredicateSym) IsBuiltin() bool

IsBuiltin returns true if this predicate symbol is for a built-in predicate.

func (PredicateSym) IsInternalPredicate 

func (p PredicateSym) IsInternalPredicate() bool

IsInternalPredicate returns true if predicate symbol belongs to a generated predicate name.

func (PredicateSym) String 

func (p PredicateSym) String() string

type Subst 

type Subst interface {
	// Returns the term the given variable maps to, or nil if the variable is not in domain.
	Get(Variable) BaseTerm
}

Subst is the interface for substitutions. This interface provides mapping from a variable to BaseTerm.

type SubstMap 

type SubstMap map[Variable]BaseTerm

SubstMap is a substitution backed by a map from variables to constants.

func (SubstMap) Get 

func (m SubstMap) Get(v Variable) BaseTerm

Get implements the Get method from Subst.

type Term 

type Term interface {

	// Returns a string representation.
	String() string

	// Syntactic (or structural) equality.
	// If Equals returns true, terms have the same string representation.
	Equals(Term) bool

	// Returns a new term.
	ApplySubst(s Subst) Term
	// contains filtered or unexported methods
}

Term represents the building blocks of datalog programs, namely constants, variables, atoms, and also negated atoms, equality and inequality.

Some minor differences to formal mathematical logic and prolog-style logic programming: - an Atom in datalog is always a predicate symbol applied to constants or variables ("base terms" - an equality and inequality would be called a "formula" but we do not need a separate interface - Atom and NegatedAtom instances would be called "literals", but again one interface is enough.

Note that constants start with "/" whereas variables start with a capital letter name. This convention gives us a 1:1 mapping between term objects and their string representations, and this is useful because Atom is not a hashable type (use String() to use Term as key in maps).

func ReplaceWildcards 

func ReplaceWildcards(used map[Variable]bool, term Term) Term

ReplaceWildcards returns a new term where each wildcard is replaced with a fresh variables. The used-variables map is modified to keep track of newly added variables.

type Transform 

type Transform struct {
	Statements []TransformStmt
}

Transform represents a transformation of the relation of a clause. e.g. fn:max or fn:group_by

func (Transform) IsLetTransform 

func (t Transform) IsLetTransform() bool

IsLetTransform returns true if transform is a let-transform. The other case is a do-transform which starts with "do fn:group_by()".

func (Transform) String 

func (t Transform) String() string

type TransformStmt 

type TransformStmt struct {
	// The variable to which to assign the result e.g. X in "X = fn:sum(Z)", May be nil.
	Var *Variable
	// An expression that refers to some part of the input relation.
	Fn ApplyFn
}

TransformStmt describes how to transform the relation of a rule.

type Variable 

type Variable struct {
	Symbol string
}

Variable represents a variable by the name.

func FreshVariable 

func FreshVariable(used map[Variable]bool) Variable

FreshVariable returns a variable different from the ones in used.

func (Variable) ApplySubst 

func (v Variable) ApplySubst(s Subst) Term

ApplySubst returns the result of applying the given substitution.

func (Variable) ApplySubstBase 

func (v Variable) ApplySubstBase(s Subst) BaseTerm

ApplySubstBase returns the result of applying the given substitution.

func (Variable) Equals 

func (v Variable) Equals(u Term) bool

Equals provides syntactic equality for variables.

func (Variable) Hash 

func (v Variable) Hash() uint64

Hash returns a hash code.

func (Variable) String 

func (v Variable) String() string

String simply returns the variable's name.

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.