term

package
v1.0.0 Latest Latest
Warning

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

 Go to latest Published: Mar 15, 2020 License: MIT Imports: 10 Imported by: 0

Documentation

Overview

Package term contains data types for Dhall terms.

A Term is a data type which represents a Dhall expression. Terms only capture abstract syntax (ie how Terms are built up from each other), not semantics (ie how to evaluate Terms).

Index

Constants

View Source 
const NullOrigin = "null"

NullOrigin is used in Fetchable.Fetch() to indicate no origin.

Variables

This section is empty.

Functions

This section is empty.

Types

type Annot 

type Annot struct {
	Expr       Term
	Annotation Term
}

type App 

type App struct {
	Fn  Term
	Arg Term
}

An App is a Term formed by applying a function to an argument.

func (App) String 

func (app App) String() string

type Assert 

type Assert struct{ Annotation Term }

type Binding 

type Binding struct {
	Variable   string
	Annotation Term // may be nil
	Value      Term
}

type BoolLit 

type BoolLit bool

A BoolLit is a Dhall boolean literal. 

const (
	True  BoolLit = true
	False BoolLit = false
)

Naturally, it is True or False.

type Builtin 

type Builtin string

Builtin is the type of Dhall's builtin constants. 

const (
	Double   Builtin = "Double"
	Text     Builtin = "Text"
	Bool     Builtin = "Bool"
	Natural  Builtin = "Natural"
	Integer  Builtin = "Integer"
	List     Builtin = "List"
	Optional Builtin = "Optional"
	None     Builtin = "None"

	NaturalBuild     Builtin = "Natural/build"
	NaturalFold      Builtin = "Natural/fold"
	NaturalIsZero    Builtin = "Natural/isZero"
	NaturalEven      Builtin = "Natural/even"
	NaturalOdd       Builtin = "Natural/odd"
	NaturalToInteger Builtin = "Natural/toInteger"
	NaturalShow      Builtin = "Natural/show"
	NaturalSubtract  Builtin = "Natural/subtract"

	IntegerClamp    Builtin = "Integer/clamp"
	IntegerNegate   Builtin = "Integer/negate"
	IntegerToDouble Builtin = "Integer/toDouble"
	IntegerShow     Builtin = "Integer/show"

	DoubleShow Builtin = "Double/show"

	TextShow Builtin = "Text/show"

	ListBuild   Builtin = "List/build"
	ListFold    Builtin = "List/fold"
	ListLength  Builtin = "List/length"
	ListHead    Builtin = "List/head"
	ListLast    Builtin = "List/last"
	ListIndexed Builtin = "List/indexed"
	ListReverse Builtin = "List/reverse"

	OptionalBuild Builtin = "Optional/build"
	OptionalFold  Builtin = "Optional/fold"
)

These are the Builtins.

type Chunk 

type Chunk struct {
	Prefix string
	Expr   Term
}

type Chunks 

type Chunks []Chunk

type DoubleLit 

type DoubleLit float64

A DoubleLit is a literal of type Double.

func (DoubleLit) String 

func (d DoubleLit) String() string

type EmptyList 

type EmptyList struct{ Type Term }

An EmptyList is an empty list literal Term of the given type.

type EnvVar 

type EnvVar string

An EnvVar is a Fetchable which represents fetching the value of an environment variable.

func (EnvVar) AsLocation 

func (e EnvVar) AsLocation() Term

AsLocation returns the EnvVar as a Dhall Term. This implements the `env:FOO as Location` Dhall feature.

func (EnvVar) ChainOnto 

func (e EnvVar) ChainOnto(base Fetchable) (Fetchable, error)

ChainOnto returns e.

func (EnvVar) Fetch 

func (e EnvVar) Fetch(origin string) (string, error)

Fetch reads the environment variable. If origin is not NullOrigin, an error is returned, to prevent remote imports from importing environment variables.

func (EnvVar) Origin 

func (EnvVar) Origin() string

Origin returns NullOrigin, since EnvVars do not have an origin.

func (EnvVar) String 

func (e EnvVar) String() string

type Fetchable 

type Fetchable interface {
	Origin() string
	Fetch(origin string) (string, error)
	ChainOnto(base Fetchable) (Fetchable, error)
	String() string
	AsLocation() Term
}

A Fetchable is the target of a Dhall import: a remote file, local file, environment variable, or the special value `missing`.

Fetch(origin) is the key method on this interface; it fetches the underlying resource, with authority from the given origin.

type Field 

type Field struct {
	Record    Term
	FieldName string
}

type If 

type If struct {
	Cond Term
	T    Term
	F    Term
}

type Import 

type Import struct {
	ImportHashed
	ImportMode
}

An Import is an import Term.

type ImportHashed 

type ImportHashed struct {
	Fetchable
	Hash []byte // stored in multihash form - ie first two bytes are 0x12 0x20
}

ImportHashed is a Fetchable with an optional hash for integrity protection.

type ImportMode 

type ImportMode byte

An ImportMode encodes how an import should be processed once fetched. 

const (
	Code     ImportMode = iota // Import as Dhall code.
	RawText                    // Import as a Text value - `as Text`.
	Location                   // Import as a Location - `as Location`.
)

These are the valid ImportModes.

type IntegerLit 

type IntegerLit int

A IntegerLit is a literal of type Integer.

type Lambda 

type Lambda struct {
	Label string
	Type  Term
	Body  Term
}

A Lambda is a lambda abstraction.

func NewLambda 

func NewLambda(label string, t Term, body Term) Lambda

NewLambda constructs a new lambda Term.

func (Lambda) String 

func (lam Lambda) String() string

type Let 

type Let struct {
	Bindings []Binding
	Body     Term
}

func NewLet 

func NewLet(body Term, bindings ...Binding) Let

NewLet returns a let Term.

type LocalFile 

type LocalFile string

A LocalFile is a Fetchable which represents fetching the content of a local file. It is defined to be one of four classes: here-relative (ie starts with ./), parent-relative (starts with ../), home-relative (starts with ~/), or absolute (starts with /).

func (LocalFile) AsLocation 

func (l LocalFile) AsLocation() Term

AsLocation returns the LocalFile as a Dhall Term. This implements the `./file as Location` Dhall feature.

func (LocalFile) ChainOnto 

func (l LocalFile) ChainOnto(base Fetchable) (Fetchable, error)

ChainOnto chains l onto the base Fetchable, according to the Dhall definition of import chaining: https://github.com/dhall-lang/dhall-lang/blob/master/standard/imports.md#chaining-imports

For here- or parent-relative LocalFiles, they chain onto RemoteFiles using the URL reference resolution algorithm; they chain onto LocalFiles using filesystem path joining; they chain onto Missing or EnvVar by just returning the LocalFile unmodified.

For home-relative or absolute LocalFiles, chaining them onto a RemoteFile is an error; all other cases return the LocalFile unmodified.

func (LocalFile) Fetch 

func (l LocalFile) Fetch(origin string) (string, error)

Fetch reads the local file. If origin is not NullOrigin, an error is returned, to prevent remote imports from importing local files.

func (LocalFile) IsAbs 

func (l LocalFile) IsAbs() bool

IsAbs returns true if the LocalFile is an absolute path.

func (LocalFile) IsRelativeToHome 

func (l LocalFile) IsRelativeToHome() bool

IsRelativeToHome returns true if the LocalFile starts with "~/"

func (LocalFile) IsRelativeToParent 

func (l LocalFile) IsRelativeToParent() bool

IsRelativeToParent returns true if the LocalFile starts with "../"

func (LocalFile) Origin 

func (LocalFile) Origin() string

Origin returns NullOrigin, since LocalFiles do not have an origin.

func (LocalFile) PathComponents 

func (l LocalFile) PathComponents() []string

PathComponents returns a slice of strings, one for each component of the given path. It excludes any leading ".", ".." or "~".

func (LocalFile) String 

func (l LocalFile) String() string

type LocalVar 

type LocalVar struct {
	Name  string
	Index int
}

A LocalVar is an internal sentinel value used by TypeOf() in the process of typechecking the body of lambdas and pis. Essentially it lets us convert de Bruijn indices (which count how many binders we need to pass from the variable to the correct binder) to de Bruijn levels (which count how many binders we passed before binding this variable)

func (LocalVar) String 

func (v LocalVar) String() string

type Merge 

type Merge struct {
	Handler    Term
	Union      Term
	Annotation Term // optional
}

type Missing 

type Missing struct{}

Missing is a Fetchable which cannot be Fetched.

func (Missing) AsLocation 

func (Missing) AsLocation() Term

AsLocation returns Missing as a Dhall Term. This implements the `missing as Location` feature.

func (Missing) ChainOnto 

func (Missing) ChainOnto(base Fetchable) (Fetchable, error)

ChainOnto returns a Missing.

func (Missing) Fetch 

func (Missing) Fetch(origin string) (string, error)

Fetch always returns an error, because Missing cannot be fetched.

func (Missing) Origin 

func (Missing) Origin() string

Origin returns NullOrigin, since Missing does not have an origin.

func (Missing) String 

func (Missing) String() string

type NaturalLit 

type NaturalLit uint

A NaturalLit is a literal of type Natural.

type NonEmptyList 

type NonEmptyList []Term

A NonEmptyList is a non-empty list literal Term with the given contents.

func NewList 

func NewList(first Term, rest ...Term) NonEmptyList

NewList returns a non-empty list Term from the given Terms.

type Op 

type Op struct {
	OpCode OpCode
	L      Term
	R      Term
}

An Op is two Terms combined by an operator. The OpCode determines the type of operator.

func BoolAnd 

func BoolAnd(l, r Term) Op

BoolAnd takes Terms l and r and returns (l && r).

func BoolOr 

func BoolOr(l, r Term) Op

BoolOr takes Terms l and r and returns (l || r).

func Equivalent 

func Equivalent(l, r Term) Op

Equivalent takes Terms l and r and returns (l ≡ r).

func ListAppend 

func ListAppend(l, r Term) Op

ListAppend takes Terms l and r and returns (l # r).

func NaturalPlus 

func NaturalPlus(l, r Term) Op

NaturalPlus takes Terms l and r and returns (l + r).

func NaturalTimes 

func NaturalTimes(l, r Term) Op

NaturalTimes takes Terms l and r and returns (l * r).

func TextAppend 

func TextAppend(l, r Term) Op

TextAppend takes Terms l and r and returns (l ++ r).

func (Op) String 

func (op Op) String() string

type OpCode 

type OpCode int

An OpCode encodes the type of an operator. 

const (
	OrOp  OpCode = iota // a || b
	AndOp               // a && b
	EqOp                // a == b
	NeOp                // a != b

	PlusOp  // a + b
	TimesOp // a * b

	TextAppendOp // a ++ b
	ListAppendOp // a # b

	RecordMergeOp            // a /\ b
	RightBiasedRecordMergeOp // a // b
	RecordTypeMergeOp        // a //\\ b

	ImportAltOp // a ? b
	EquivOp     // a === b
	CompleteOp  // A::b
)

These are the valid OpCodes. Note that the actual integer values have been chosen to match the binary encoding label numbers.

type Pi 

type Pi struct {
	Label string
	Type  Term
	Body  Term
}

A Pi is a function type.

func NewAnonPi 

func NewAnonPi(domain Term, codomain Term) Pi

NewAnonPi returns a pi Term with label "_", typically used for non-dependent function types.

func NewPi 

func NewPi(label string, t Term, body Term) Pi

NewPi constructs a new pi Term.

func (Pi) String 

func (pi Pi) String() string

type Project 

type Project struct {
	Record     Term
	FieldNames []string
}

type ProjectType 

type ProjectType struct {
	Record   Term
	Selector Term
}

type RecordLit 

type RecordLit map[string]Term

type RecordType 

type RecordType map[string]Term

type RemoteFile 

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

A RemoteFile is a Fetchable which represents fetching the content of a remote file (over HTTP or HTTPS).

func NewRemoteFile 

func NewRemoteFile(u *url.URL) RemoteFile

NewRemoteFile constructs a RemoteFile from a *url.URL.

func (RemoteFile) AsLocation 

func (r RemoteFile) AsLocation() Term

AsLocation returns the RemoteFile as a Dhall Term. This implements the `https://example.com/foo/bar as Location` feature.

func (RemoteFile) Authority 

func (r RemoteFile) Authority() string

Authority returns the authority of the URL; that is, the bit between the first "//" and the next "/", which includes optional userinfo, remote host, and optional port number.

func (RemoteFile) ChainOnto 

func (r RemoteFile) ChainOnto(base Fetchable) (Fetchable, error)

ChainOnto returns the RemoteFile unmodified.

func (RemoteFile) Fetch 

func (r RemoteFile) Fetch(origin string) (string, error)

Fetch makes an HTTP request to fetch the RemoteFile. If origin is neither NullOrigin nor the same origin as this RemoteFile, this is considered a cross-origin request and so appropriate CORS checks are made; if these fail, an error is returned with no content.

func (RemoteFile) IsPlainHTTP 

func (r RemoteFile) IsPlainHTTP() bool

IsPlainHTTP returns true if this is an "http://" URL, and false if it an "https://" URL.

func (RemoteFile) Origin 

func (r RemoteFile) Origin() string

Origin returns the scheme and authority of the underlying URL of a RemoteFile. For example, the Origin of "https://example.com/foo/bar" is "https://example.com".

func (RemoteFile) PathComponents 

func (r RemoteFile) PathComponents() []string

PathComponents returns a slice of strings, one for each path component of the given URL.

func (RemoteFile) Query 

func (r RemoteFile) Query() *string

Query returns the query string, or nil if no query string is present.

func (RemoteFile) String 

func (r RemoteFile) String() string

type Some 

type Some struct{ Val Term }

Some represents a Term which is present in an Optional type.

type Term 

type Term interface {
	// contains filtered or unexported methods
}

A Term is an arbitrary Dhall expression. When you parse text into Dhall, you get a value of type Term.

The Term interface is just a marker; there are no interesting methods.

func Apply 

func Apply(fn Term, args ...Term) Term

Apply takes fn and applies it successively to each arg in args.

func RebindLocal 

func RebindLocal(local LocalVar, t Term) Term

RebindLocal takes a Term and finds all instances of a LocalVar and replaces them with the equivalent Var.

func Subst 

func Subst(name string, replacement, t Term) Term

Subst takes a Term and finds all instances of a variable called `name` and replaces them with the replacement.

type TextLit 

type TextLit struct {
	Chunks Chunks
	Suffix string
}

func PlainText 

func PlainText(content string) TextLit

PlainText returns an uninterpolated text literal containing the given string as text.

type ToMap 

type ToMap struct {
	Record Term
	Type   Term // optional
}

type UnionType 

type UnionType map[string]Term

type Universe 

type Universe int

A Universe is a type of types. 

const (
	Type Universe = iota
	Kind
	Sort
)

These are the valid Universes.

func (Universe) String 

func (c Universe) String() string

type Var 

type Var struct {
	Name  string
	Index int
}

A Var is a variable, either bound or free. A free Var is a valid Value; a bound Var is not.

The Index is a de Bruijn index. In an expression such as: 

λ(x : Natural) → λ(x : Natural) → x@1

x@1 refers to the outer bound variable x. x@1 is represented by Var{"x", 1}.

func NewVar 

func NewVar(name string) Var

NewVar returns a new Var.

func (Var) String 

func (v Var) String() string

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.