symbols

package
v0.1.0 Latest Latest
Warning

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

 Go to latest Published: Dec 15, 2023 License: Apache-2.0 Imports: 5 Imported by: 0

Documentation

Overview

Package symbols contains symbols for built-in functions and predicates.

Index

Constants

This section is empty.

Variables

View Source 
var (
	// MatchPrefix matches name constants that have a given prefix.
	MatchPrefix = ast.PredicateSym{":match_prefix", 2}

	// StartsWith matches string constants that have a given prefix.
	StartsWith = ast.PredicateSym{":string:starts_with", 2}

	// EndsWith matches string constants that have a given suffix.
	EndsWith = ast.PredicateSym{":string:ends_with", 2}

	// Contains matches string constants that contain the given string.
	Contains = ast.PredicateSym{":string:contains", 2}

	// Lt is the less-than relation on numbers.
	Lt = ast.PredicateSym{":lt", 2}

	// Le is the less-than-or-equal relation on numbers.
	Le = ast.PredicateSym{":le", 2}

	// Gt is the greater-than relation on numbers.
	Gt = ast.PredicateSym{":gt", 2}

	// Ge is the greater-than-or-equal relation on numbers.
	Ge = ast.PredicateSym{":ge", 2}

	// MatchPair mode(+, -, -) matches a pair to its elements.
	MatchPair = ast.PredicateSym{":match_pair", 3}

	// MatchCons mode(+, -, -) matches a list to head and tail.
	MatchCons = ast.PredicateSym{":match_cons", 3}

	// MatchNil matches the empty list.
	MatchNil = ast.PredicateSym{":match_nil", 1}

	// MatchEntry mode(+, +, -) matches an entry in a map.
	MatchEntry = ast.PredicateSym{":match_entry", 3}

	// MatchField mode(+, +, -) matches a field in a struct.
	MatchField = ast.PredicateSym{":match_field", 3}

	// ListMember mode(+, -) either checks membership or binds var to every element.
	ListMember = ast.PredicateSym{":list:member", 2}

	// WithinDistance is a relation on numbers X, Y, Z satisfying |X - Y| < Z.
	WithinDistance = ast.PredicateSym{":within_distance", 3}

	// Div is a family of functions mapping integer division: X,Y1,.. to (X / Y1) / Y2 ... DIV(X) is 1/x.
	Div = ast.FunctionSym{"fn:div", -1}
	// FloatDiv is a family of functions mapping division: X,Y1,.. to (X / Y1) / Y2 ... FloatDiv(X) is 1/x.
	FloatDiv = ast.FunctionSym{"fn:float:div", -1}
	// Mult is a family of functions mapping X,Y1,.. to (X * Y1) * Y2 ... MULT(x) is x.
	Mult = ast.FunctionSym{"fn:mult", -1}
	// Plus is a family of functions mapping X,Y1,.. to (X + Y1) + Y2 ... PLUS(x) is x.
	Plus = ast.FunctionSym{"fn:plus", -1}
	// Minus is a family of functions mapping X,Y1,.. to (X - Y1) - Y2 ...MINUS(x) is -X.
	Minus = ast.FunctionSym{"fn:minus", -1}

	// Collect turns a collection { tuple_1,...tuple_n } into a list [tuple_1, ..., tuple_n].
	Collect = ast.FunctionSym{"fn:collect", -1}
	// CollectDistinct turns a collection { tuple_1,...tuple_n } into a list with distinct elements [tuple_1, ..., tuple_n].
	CollectDistinct = ast.FunctionSym{"fn:collect_distinct", -1}
	// PickAny reduces a set { x_1,...x_n } to a single { x_i },
	PickAny = ast.FunctionSym{"fn:pick_any", 1}
	// Max reduces a set { x_1,...x_n } to { x_i } that is maximal.
	Max = ast.FunctionSym{"fn:max", 1}
	// FloatMax reduces a set of float64 { x_1,...x_n } to { x_i } that is maximal.
	FloatMax = ast.FunctionSym{"fn:float:max", 1}
	// Min reduces a set { x_1,...x_n } to { x_i } that is minimal.
	Min = ast.FunctionSym{"fn:min", 1}
	// FloatMin reduces a set of float64 { x_1,...x_n } to { x_i } that is minimal.
	FloatMin = ast.FunctionSym{"fn:float:min", 1}
	// Sum reduces a set { x_1,...x_n } to { x_1 + ... + x_n }.
	Sum = ast.FunctionSym{"fn:sum", 1}
	// FloatSum reduces a set of float64 { x_1,...x_n } to { x_1 + ... + x_n }.
	FloatSum = ast.FunctionSym{"fn:float:sum", 1}
	// Count reduces a set { x_1,...x_n } to { n }.
	Count = ast.FunctionSym{"fn:count", 0}

	// GroupBy groups all tuples by the values of key variables, e.g. 'group_by(X)'.
	// An empty group_by() treats the whole relation as a group.
	GroupBy = ast.FunctionSym{"fn:group_by", -1}

	// Append appends a element to a list.
	Append = ast.FunctionSym{"fn:list:append", 2}

	// ListGet is a function (List, Number) which returns element at index 'Number'.
	ListGet = ast.FunctionSym{"fn:list:get", 2}

	// ListContains is a function (List, Member) which returns /true if Member is contained in list.
	ListContains = ast.FunctionSym{"fn:list:contains", 2}

	// Len returns length of a list.
	Len = ast.FunctionSym{"fn:list:len", 1}
	// Cons constructs a pair.
	Cons = ast.FunctionSym{"fn:list:cons", 2}
	// Pair constructs a pair.
	Pair = ast.FunctionSym{"fn:pair", 2}
	// MapGet is a function (Map, Key) which returns element at key.
	MapGet = ast.FunctionSym{"fn:map:get", 2}
	// StructGet is a function (Struct, Field) which returns specified field.
	StructGet = ast.FunctionSym{"fn:struct:get", 2}
	// Tuple acts either as identity (one argument), pair (two arguments) or nested pair (more).
	Tuple = ast.FunctionSym{"fn:tuple", -1}
	// Some constructs an element of an option type.
	Some = ast.FunctionSym{"fn:some", 1}
	// List constructs a list.
	List = ast.FunctionSym{"fn:list", -1}
	// Map constructs a map.
	Map = ast.FunctionSym{"fn:map", -1}
	// Struct constructs a struct.
	Struct = ast.FunctionSym{"fn:struct", -1}

	// FunType is a constructor for a function type.
	// fn:Fun(Res, Arg1, ..., ArgN) is Res <= Arg1, ..., ArgN
	FunType = ast.FunctionSym{"fn:Fun", -1}

	// RelType is a constructor for a relation type.
	RelType = ast.FunctionSym{"fn:Rel", -1}

	// NumberToString converts from ast.NumberType to ast.StringType
	NumberToString = ast.FunctionSym{"fn:number:to_string", 1}

	// Float64ToString converts from ast.Float64Type to ast.StringType
	Float64ToString = ast.FunctionSym{"fn:float64:to_string", 1}

	// NameToString converts from ast.NameType to ast.StringType
	NameToString = ast.FunctionSym{"fn:name:to_string", 1}

	// StringConcatenate concatenates the arguments into a single string constant.
	StringConcatenate = ast.FunctionSym{"fn:string:concat", -1}

	// PairType is a constructor for a pair type.
	PairType = ast.FunctionSym{"fn:Pair", 2}
	// TupleType is a type-level function that returns a tuple type out of pair types.
	TupleType = ast.FunctionSym{"fn:Tuple", -1}
	// OptionType is a constructor for an option type.
	// A value of fn:Option(T) is either fn:some(c) for c:T, or fn:none().
	// TODO: Implement runtime representation.
	OptionType = ast.FunctionSym{"fn:Option", 1}
	// ListType is a constructor for a list type.
	ListType = ast.FunctionSym{"fn:List", 1}
	// MapType is a constructor for a map type.
	MapType = ast.FunctionSym{"fn:Map", 2}
	// StructType is a constructor for a struct type.
	StructType = ast.FunctionSym{"fn:Struct", -1}
	// UnionType is a constructor for a union type.
	UnionType = ast.FunctionSym{"fn:Union", -1}

	// Optional may appear inside StructType to indicate optional fields.
	Optional = ast.FunctionSym{"fn:opt", -1}

	// Package is an improper symbol, used to represent package declaration.
	Package = ast.PredicateSym{"Package", 0}
	// Use is an improper symbol, used to represent use declaration.
	Use = ast.PredicateSym{"Use", 0}

	// TypeConstructors is a list of function symbols used in structured type expressions.
	// Each name is mapped to the corresponding type constructor (a function at the level of types).
	TypeConstructors = map[string]ast.FunctionSym{
		UnionType.Symbol:  UnionType,
		ListType.Symbol:   ListType,
		OptionType.Symbol: OptionType,
		PairType.Symbol:   PairType,
		TupleType.Symbol:  TupleType,
		MapType.Symbol:    MapType,
		StructType.Symbol: StructType,
		FunType.Symbol:    FunType,
		RelType.Symbol:    RelType,
	}

	// EmptyType is a type without members.
	// TODO: replace with /bot
	EmptyType = ast.ApplyFn{UnionType, nil}

	// BuiltinRelations maps each builtin predicate to its argument range list
	BuiltinRelations = map[ast.PredicateSym]ast.BaseTerm{
		MatchPrefix: NewRelType(ast.NameBound, ast.NameBound),
		StartsWith:  NewRelType(ast.StringBound, ast.StringBound),
		EndsWith:    NewRelType(ast.StringBound, ast.StringBound),
		Contains:    NewRelType(ast.StringBound, ast.StringBound),

		Lt:       NewRelType(ast.NumberBound, ast.NumberBound),
		Le:       NewRelType(ast.NumberBound, ast.NumberBound),
		MatchNil: NewRelType(NewListType(ast.Variable{"X"})),
		MatchCons: NewRelType(
			NewListType(ast.Variable{"X"}), ast.Variable{"X"}, NewListType(ast.Variable{"X"})),
		MatchPair: NewRelType(
			NewPairType(ast.Variable{"X"}, ast.Variable{"Y"}), ast.Variable{"X"}, ast.Variable{"Y"}),
		MatchEntry: NewRelType(
			NewMapType(ast.AnyBound, ast.AnyBound), ast.AnyBound),
		MatchField: NewRelType(
			ast.AnyBound, ast.NameBound, ast.AnyBound),
		ListMember: NewRelType(ast.Variable{"X"}, NewListType(ast.Variable{"X"})),
	}
)

Functions

func CheckAndDesugar 

func CheckAndDesugar(decls map[ast.PredicateSym]ast.Decl) (map[ast.PredicateSym]*ast.Decl, error)

CheckAndDesugar rewrites a complete set of decls so that bound declarations contain only type bounds and unary predicate references are added to inclusion constraints.

func CheckFunTypeExpression 

func CheckFunTypeExpression(ctx map[ast.Variable]ast.BaseTerm, expr ast.ApplyFn) error

CheckFunTypeExpression checks a function type expression.

func CheckSetExpression 

func CheckSetExpression(expr ast.BaseTerm) error

CheckSetExpression returns an error if expr is not a valid type expression. expr is by convention a type expression that talks about sets (no type variables, no function type subexpressions, no reltype).

func CheckTypeExpression 

func CheckTypeExpression(ctx map[ast.Variable]ast.BaseTerm, expr ast.BaseTerm) error

CheckTypeExpression returns an error if expr is not a valid type expression. expr is by convention not a reltype.

func CreateListType 

func CreateListType(bound ast.Constant) ast.ApplyFn

CreateListType applies given type to a list.

func FunTypeArgs 

func FunTypeArgs(tpe ast.BaseTerm) ([]ast.BaseTerm, error)

FunTypeArgs returns function arguments of function type.

func FunTypeResult 

func FunTypeResult(tpe ast.BaseTerm) (ast.BaseTerm, error)

FunTypeResult returns result type of function type.

func IsBaseTypeExpression 

func IsBaseTypeExpression(c ast.Constant) bool

IsBaseTypeExpression returns true if c is a base type expression. A name constant is /foo is not a base type expression.

func IsFunTypeExpression 

func IsFunTypeExpression(tpe ast.BaseTerm) bool

IsFunTypeExpression returns true if tpe is a UnionType.

func IsListTypeExpression 

func IsListTypeExpression(tpe ast.BaseTerm) bool

IsListTypeExpression returns true if tpe is a ListType.

func IsMapTypeExpression 

func IsMapTypeExpression(tpe ast.BaseTerm) bool

IsMapTypeExpression returns true if tpe is a MapType.

func IsOptional 

func IsOptional(structElem ast.BaseTerm) bool

IsOptional returns true if an argument of fn:Struct is an optional field.

func IsRelTypeExpression 

func IsRelTypeExpression(tpe ast.BaseTerm) bool

IsRelTypeExpression returns true if tpe is a RelType.

func IsStructTypeExpression 

func IsStructTypeExpression(tpe ast.BaseTerm) bool

IsStructTypeExpression returns true if tpe is a StructType.

func IsUnionTypeExpression 

func IsUnionTypeExpression(tpe ast.BaseTerm) bool

IsUnionTypeExpression returns true if tpe is a UnionType.

func ListTypeArg 

func ListTypeArg(tpe ast.BaseTerm) (ast.BaseTerm, error)

ListTypeArg returns the type argument of a ListType.

func LowerBound 

func LowerBound(typeExprs []ast.BaseTerm) ast.BaseTerm

LowerBound returns a lower bound of set expressions.

func MapTypeArgs 

func MapTypeArgs(tpe ast.BaseTerm) (ast.BaseTerm, ast.BaseTerm, error)

MapTypeArgs returns the type arguments of a MapType.

func NewFunType 

func NewFunType(res ast.BaseTerm, args ...ast.BaseTerm) ast.ApplyFn

NewFunType returns a new function type. Res <- Arg1, ..., ArgN

func NewListType 

func NewListType(elem ast.BaseTerm) ast.ApplyFn

NewListType returns a new ListType.

func NewMapType 

func NewMapType(keyType, valueType ast.BaseTerm) ast.ApplyFn

NewMapType returns a new MapType.

func NewOpt 

func NewOpt(label, tpe ast.BaseTerm) ast.ApplyFn

NewOpt wraps a label-type pair inside a StructType. fn:optional(/foo, /string)

func NewOptionType 

func NewOptionType(elem ast.BaseTerm) ast.ApplyFn

NewOptionType returns a new ListType.

func NewPairType 

func NewPairType(left, right ast.BaseTerm) ast.ApplyFn

NewPairType returns a new PairType.

func NewRelType 

func NewRelType(args ...ast.BaseTerm) ast.ApplyFn

NewRelType returns a new relation type.

func NewStructType 

func NewStructType(args ...ast.BaseTerm) ast.ApplyFn

NewStructType returns a new StructType.

func NewTupleType 

func NewTupleType(parts ...ast.BaseTerm) ast.ApplyFn

NewTupleType returns a new TupleType.

func NewUnionType 

func NewUnionType(elems ...ast.BaseTerm) ast.ApplyFn

NewUnionType returns a new UnionType.

func RelTypeAlternatives 

func RelTypeAlternatives(relTypeExpr ast.BaseTerm) []ast.BaseTerm

RelTypeAlternatives converts a relation type expression to a list of alternatives relTypes.

func RelTypeArgs 

func RelTypeArgs(tpe ast.BaseTerm) ([]ast.BaseTerm, error)

RelTypeArgs returns type arguments of a RelType.

func RelTypeExprFromDecl 

func RelTypeExprFromDecl(decl ast.Decl) (ast.BaseTerm, error)

RelTypeExprFromDecl converts bounds to relation type expression.

func RelTypeFromAlternatives 

func RelTypeFromAlternatives(alternatives []ast.BaseTerm) ast.BaseTerm

RelTypeFromAlternatives converts list of rel types bounds to union of relation types. It is assumed that each alternatives is a RelType. An empty list of alternatives corresponds to the empty type fn:Union().

func RemoveFromUnionType 

func RemoveFromUnionType(tpeToRemove, unionTpe ast.BaseTerm) (ast.BaseTerm, error)

RemoveFromUnionType given T, removes S from a union type {..., S, ...} if S<:T.

func SetConforms 

func SetConforms(left ast.BaseTerm, right ast.BaseTerm) bool

SetConforms returns true if |- left <: right for set expression.

func StructTypeField 

func StructTypeField(tpe ast.BaseTerm, field ast.Constant) (ast.BaseTerm, error)

StructTypeField returns field type for given field.

func StructTypeOptionaArgs 

func StructTypeOptionaArgs(tpe ast.BaseTerm) ([]ast.BaseTerm, error)

StructTypeOptionaArgs returns type arguments of a StructType.

func StructTypeRequiredArgs 

func StructTypeRequiredArgs(tpe ast.BaseTerm) ([]ast.BaseTerm, error)

StructTypeRequiredArgs returns type arguments of a StructType.

func TypeConforms 

func TypeConforms(ctx map[ast.Variable]ast.BaseTerm, left ast.BaseTerm, right ast.BaseTerm) bool

TypeConforms returns true if ctx |- left <: right. The arguments left and right cannot be RelType or UnionType

func UnionTypeArgs 

func UnionTypeArgs(tpe ast.BaseTerm) ([]ast.BaseTerm, error)

UnionTypeArgs returns type arguments of a UnionType.

func UpperBound 

func UpperBound(typeExprs []ast.BaseTerm) ast.BaseTerm

UpperBound returns upper bound of set expressions.

Types

type NameTrie 

type NameTrie = *NameTrieNode

NameTrie is a trie for looking up name constants. Every node represents a unique part of a name. Note that the trie for {"/foo", "/foo/bar"} is different from {"/foo/bar"}: the former would map a constant "/foo/baz" to the type "/foo", whereas the latter would map it to type "/name". "/foo" appears as a node in both, but only the former treats it as a terminal node.

func NewNameTrie 

func NewNameTrie() NameTrie

NewNameTrie constructs a new NameTrie (representing empty prefix).

func (NameTrie) Add 

func (n NameTrie) Add(parts []string) NameTrie

Add adds a part sequence to this trie.

func (NameTrie) Collect 

func (n NameTrie) Collect(typeExpr ast.BaseTerm)

Collect traverses a type expression and extracts names. Base type expressions are ignored.

func (NameTrie) Contains 

func (n NameTrie) Contains(parts []string) bool

Contains returns true if the part sequence is contained in the trie.

func (NameTrie) LongestPrefix 

func (n NameTrie) LongestPrefix(parts []string) int

LongestPrefix returns index of the last element of longest prefix.

func (NameTrie) PrefixName 

func (n NameTrie) PrefixName(symName string) ast.Constant

PrefixName returns, for a given name constant, the longest prefix contained in the trie.

func (NameTrie) String 

func (n NameTrie) String() string

type NameTrieNode 

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

NameTrieNode is a node in NameTrie.

type TypeHandle 

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

TypeHandle provides functionality related to type expression.

func NewSetHandle 

func NewSetHandle(expr ast.BaseTerm) (TypeHandle, error)

NewSetHandle constructs a TypeHandle for a (simple) monotype.

func NewTypeHandle 

func NewTypeHandle(ctx map[ast.Variable]ast.BaseTerm, expr ast.BaseTerm) (TypeHandle, error)

NewTypeHandle constructs a TypeHandle.

func (TypeHandle) HasType 

func (t TypeHandle) HasType(c ast.Constant) bool

HasType returns true if c has type represented by this TypeHandle.

func (TypeHandle) String 

func (t TypeHandle) String() string

String returns a string represented of this type expression.

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.