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
- type Annot
- type App
- type Assert
- type Binding
- type BoolLit
- type Builtin
- type Chunk
- type Chunks
- type DoubleLit
- type EmptyList
- type EnvVar
- type Fetchable
- type Field
- type If
- type Import
- type ImportHashed
- type ImportMode
- type IntegerLit
- type Lambda
- type Let
- type LocalFile
- func (l LocalFile) AsLocation() Term
- func (l LocalFile) ChainOnto(base Fetchable) (Fetchable, error)
- func (l LocalFile) Fetch(origin string) (string, error)
- func (l LocalFile) IsAbs() bool
- func (l LocalFile) IsRelativeToHome() bool
- func (l LocalFile) IsRelativeToParent() bool
- func (LocalFile) Origin() string
- func (l LocalFile) PathComponents() []string
- func (l LocalFile) String() string
- type LocalVar
- type Merge
- type Missing
- type NaturalLit
- type NonEmptyList
- type Op
- type OpCode
- type Pi
- type Project
- type ProjectType
- type RecordLit
- type RecordType
- type RemoteFile
- func (r RemoteFile) AsLocation() Term
- func (r RemoteFile) Authority() string
- func (r RemoteFile) ChainOnto(base Fetchable) (Fetchable, error)
- func (r RemoteFile) Fetch(origin string) (string, error)
- func (r RemoteFile) IsPlainHTTP() bool
- func (r RemoteFile) Origin() string
- func (r RemoteFile) PathComponents() []string
- func (r RemoteFile) Query() *string
- func (r RemoteFile) String() string
- type Some
- type Term
- type TextLit
- type ToMap
- type UnionType
- type Universe
- type Var
- type With
Constants ¶
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 ¶
func (Annot) MarshalCBOR ¶
MarshalCBOR implements cbor.Marshaler.
type App ¶
An App is a Term formed by applying a function to an argument.
func (App) MarshalCBOR ¶
MarshalCBOR implements cbor.Marshaler.
type Assert ¶
type Assert struct{ Annotation Term }
func (Assert) MarshalCBOR ¶
MarshalCBOR implements cbor.Marshaler.
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" TextReplace Builtin = "Text/replace" 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" )
These are the Builtins.
type EmptyList ¶
type EmptyList struct{ Type Term }
An EmptyList is an empty list literal Term of the given type.
func (EmptyList) MarshalCBOR ¶
MarshalCBOR implements cbor.Marshaler.
type EnvVar ¶
type EnvVar string
An EnvVar is a Fetchable which represents fetching the value of an environment variable.
func (EnvVar) AsLocation ¶
AsLocation returns the EnvVar as a Dhall Term. This implements the `env:FOO as Location` Dhall feature.
func (EnvVar) Fetch ¶
Fetch reads the environment variable. If origin is not NullOrigin, an error is returned, to prevent remote imports from importing environment variables.
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 ¶
func (Field) MarshalCBOR ¶
MarshalCBOR implements cbor.Marshaler.
type If ¶
func (If) MarshalCBOR ¶
MarshalCBOR implements cbor.Marshaler.
type Import ¶
type Import struct { ImportHashed ImportMode }
An Import is an import Term.
func (Import) MarshalCBOR ¶
MarshalCBOR implements cbor.Marshaler.
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.
func (IntegerLit) MarshalCBOR ¶
func (i IntegerLit) MarshalCBOR() ([]byte, error)
MarshalCBOR implements cbor.Marshaler.
type Lambda ¶
A Lambda is a lambda abstraction.
func (Lambda) MarshalCBOR ¶
MarshalCBOR implements cbor.Marshaler.
type Let ¶
func (Let) MarshalCBOR ¶
MarshalCBOR implements cbor.Marshaler.
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 ¶
AsLocation returns the LocalFile as a Dhall Term. This implements the `./file as Location` Dhall feature.
func (LocalFile) ChainOnto ¶
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 ¶
Fetch reads the local file. If origin is not NullOrigin, an error is returned, to prevent remote imports from importing local files.
func (LocalFile) IsRelativeToHome ¶
IsRelativeToHome returns true if the LocalFile starts with "~/"
func (LocalFile) IsRelativeToParent ¶
IsRelativeToParent returns true if the LocalFile starts with "../"
func (LocalFile) PathComponents ¶
PathComponents returns a slice of strings, one for each component of the given path. It excludes any leading ".", ".." or "~".
type LocalVar ¶
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)
type Merge ¶
func (Merge) MarshalCBOR ¶
MarshalCBOR implements cbor.Marshaler.
type Missing ¶
type Missing struct{}
Missing is a Fetchable which cannot be Fetched.
func (Missing) AsLocation ¶
AsLocation returns Missing as a Dhall Term. This implements the `missing as Location` feature.
type NaturalLit ¶
type NaturalLit uint
A NaturalLit is a literal of type Natural.
func (NaturalLit) MarshalCBOR ¶
func (n NaturalLit) MarshalCBOR() ([]byte, error)
MarshalCBOR implements cbor.Marshaler.
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.
func (NonEmptyList) MarshalCBOR ¶
func (l NonEmptyList) MarshalCBOR() ([]byte, error)
MarshalCBOR implements cbor.Marshaler.
type Op ¶
An Op is two Terms combined by an operator. The OpCode determines the type of operator.
func NaturalPlus ¶
NaturalPlus takes Terms l and r and returns (l + r).
func NaturalTimes ¶
NaturalTimes takes Terms l and r and returns (l * r).
func TextAppend ¶
TextAppend takes Terms l and r and returns (l ++ r).
func (Op) MarshalCBOR ¶
MarshalCBOR implements cbor.Marshaler.
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 ¶
A Pi is a function type.
func NewAnonPi ¶
NewAnonPi returns a pi Term with label "_", typically used for non-dependent function types.
func (Pi) MarshalCBOR ¶
MarshalCBOR implements cbor.Marshaler.
type Project ¶
func (Project) MarshalCBOR ¶
MarshalCBOR implements cbor.Marshaler.
type ProjectType ¶
func (ProjectType) MarshalCBOR ¶
func (p ProjectType) MarshalCBOR() ([]byte, error)
MarshalCBOR implements cbor.Marshaler.
type RecordLit ¶
func (RecordLit) MarshalCBOR ¶
MarshalCBOR implements cbor.Marshaler.
type RecordType ¶
func (RecordType) MarshalCBOR ¶
func (r RecordType) MarshalCBOR() ([]byte, error)
MarshalCBOR implements cbor.Marshaler.
func (RecordType) String ¶
func (r RecordType) String() string
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.
func (Some) MarshalCBOR ¶
MarshalCBOR implements cbor.Marshaler.
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 MaybeTransformSubexprs ¶
MaybeTransformSubexprs returns a Term with f() applied to each immediate subexpression. If f() returns an error at any point, MaybeTransformSubexprs returns that error.
func RebindLocal ¶
RebindLocal takes a Term and finds all instances of a LocalVar and replaces them with the equivalent Var.
type TextLit ¶
func PlainText ¶
PlainText returns an uninterpolated text literal containing the given string as text.
func (TextLit) MarshalCBOR ¶
MarshalCBOR implements cbor.Marshaler.
type ToMap ¶
func (ToMap) MarshalCBOR ¶
MarshalCBOR implements cbor.Marshaler.
type UnionType ¶
func (UnionType) MarshalCBOR ¶
MarshalCBOR implements cbor.Marshaler.
type Universe ¶
type Universe int
A Universe is a type of types.
func (Universe) MarshalCBOR ¶
MarshalCBOR implements cbor.Marshaler.
type Var ¶
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 (Var) MarshalCBOR ¶
MarshalCBOR implements cbor.Marshaler.