diff --git a/core/ast.go b/core/ast.go index 7c863f5..f65a019 100644 --- a/core/ast.go +++ b/core/ast.go @@ -9,7 +9,7 @@ import ( // A Value is a Dhall value in beta-normal form. You can think of // Values as the subset of Dhall which cannot be beta-reduced any -// further. Valid Values include 3, "foo" and 5 + x. +// further. Valid Values include 3, "foo" and λ(x : Natural) → x. // // You create a Value by calling Eval() on a Term. You can convert a // Value back to a Term with Quote(). @@ -17,7 +17,7 @@ type Value interface { isValue() } -// A Universe is a type of types. +// A Universe is a Value representing a type of types. type Universe int // These are the valid Universes. @@ -27,7 +27,8 @@ const ( Sort ) -// Builtin is the type of Dhall's builtin constants. +// A Builtin is a Value representing one of Dhall's non-Callable +// builtin constants. type Builtin string // These are the Builtins. @@ -39,7 +40,7 @@ const ( Integer Builtin = "Integer" ) -// A BoolLit is a Dhall boolean literal. +// A BoolLit is a Value representing a Dhall boolean literal. type BoolLit bool func (BoolLit) isValue() {} @@ -140,13 +141,13 @@ func (listIndexed) isValue() {} func (listReverse) isValue() {} type ( - // OptionalOf is the Value version of `Optional a` + // OptionalOf is a Value representing `Optional a` OptionalOf struct{ Type Value } - // ListOf is the Value version of `List a` + // ListOf is a Value representing `List a` ListOf struct{ Type Value } - // NoneOf is the Value version of `None a` + // NoneOf is a Value representing `None a` NoneOf struct{ Type Value } ) @@ -222,13 +223,13 @@ type ( Fn func(Value) Value } - // A Pi is the value of a Dhall Pi type. Domain is the type - // of the domain, and Range is a go function which returns the - // type of the range, given the value of the domain. + // A Pi is a Value representing a Dhall Pi type. Domain is the + // type of the domain, and Codomain is a go function which returns + // the type of the codomain, given the value of the domain. Pi struct { - Label string - Domain Value - Range func(Value) Value + Label string + Domain Value + Codomain func(Value) Value } // An app is the Value of a Fn applied to an Arg. Note that @@ -256,27 +257,28 @@ func (app) isValue() {} func (oper) isValue() {} // NewPi returns a new pi Value. -func NewPi(label string, d Value, r func(Value) Value) Pi { +func NewPi(label string, domain Value, codomain func(Value) Value) Pi { return Pi{ - Label: label, - Domain: d, - Range: r, + Label: label, + Domain: domain, + Codomain: codomain, } } // NewFnType returns a non-dependent function type Value. -func NewFnType(l string, d Value, r Value) Pi { - return NewPi(l, d, func(Value) Value { return r }) +func NewFnType(label string, domain Value, codomain Value) Pi { + return NewPi(label, domain, func(Value) Value { return codomain }) } type ( - // A NaturalLit is a literal of type Natural. + // A NaturalLit is a literal Value of type Natural. NaturalLit uint // An EmptyList is an empty list literal Value of the given type. EmptyList struct{ Type Value } - // A NonEmptyList is a non-empty list literal Value with the given contents. + // A NonEmptyList is a non-empty list literal Value with the given + // contents. NonEmptyList []Value chunk struct { @@ -288,7 +290,8 @@ type ( Chunks chunks Suffix string } - // A PlainTextLit is a literal of type Text, containing no + + // A PlainTextLit is a literal Value of type Text, containing no // interpolations. PlainTextLit string @@ -298,17 +301,19 @@ type ( F Value } - // A DoubleLit is a literal of type Double. + // A DoubleLit is a literal Value of type Double. DoubleLit float64 - // A IntegerLit is a literal of type Integer. + // A IntegerLit is a literal Value of type Integer. IntegerLit int // Some represents a Value which is present in an Optional type. Some struct{ Val Value } + // A RecordType is a Value representing a Dhall record type. RecordType map[string]Value + // A RecordLit is a Value representing a Dhall record literal. RecordLit map[string]Value toMap struct { @@ -329,6 +334,7 @@ type ( // no projectType because it cannot be in a normal form so cannot // be a Value + // A UnionType is a Value representing a Dhall union type. UnionType map[string]Value merge struct { diff --git a/core/builtins.go b/core/builtins.go index 9b55f91..f79a929 100644 --- a/core/builtins.go +++ b/core/builtins.go @@ -511,6 +511,7 @@ func (rev listReverse) ArgType() Value { return ListOf{rev.typ} } +// These are the builtin Callable Values. var ( NaturalBuild Callable = naturalBuild{} NaturalEven Callable = naturalEven{} diff --git a/core/equivalence.go b/core/equivalence.go index 4777e28..05c2c1f 100644 --- a/core/equivalence.go +++ b/core/equivalence.go @@ -50,8 +50,8 @@ func alphaEquivalentWith(level int, v1 Value, v2 Value) bool { return alphaEquivalentWith(level, v1.Domain, v2.Domain) && alphaEquivalentWith( level+1, - v1.Range(quoteVar{Name: "_", Index: level}), - v2.Range(quoteVar{Name: "_", Index: level}), + v1.Codomain(quoteVar{Name: "_", Index: level}), + v2.Codomain(quoteVar{Name: "_", Index: level}), ) case app: v2, ok := v2.(app) diff --git a/core/eval.go b/core/eval.go index 3030dd2..050a95f 100644 --- a/core/eval.go +++ b/core/eval.go @@ -120,7 +120,7 @@ func evalWith(t term.Term, e env, shouldAlphaNormalize bool) Value { v := Pi{ Label: t.Label, Domain: evalWith(t.Type, e, shouldAlphaNormalize), - Range: func(x Value) Value { + Codomain: func(x Value) Value { newEnv := env{} for k, v := range e { newEnv[k] = v diff --git a/core/quote.go b/core/quote.go index 9dfeefa..e90a87d 100644 --- a/core/quote.go +++ b/core/quote.go @@ -166,7 +166,7 @@ func quoteWith(ctx quoteContext, v Value) term.Term { Body: quoteWith(ctx.extend(v.Label), bodyVal), } case Pi: - bodyVal := v.Range(quoteVar{Name: v.Label, Index: ctx[v.Label]}) + bodyVal := v.Codomain(quoteVar{Name: v.Label, Index: ctx[v.Label]}) return term.Pi{ Label: v.Label, Type: quoteWith(ctx, v.Domain), diff --git a/core/quote_test.go b/core/quote_test.go index ef26e2c..0e0dbc5 100644 --- a/core/quote_test.go +++ b/core/quote_test.go @@ -57,13 +57,13 @@ var _ = DescribeTable("Quote", Body: term.Var{"x", 0}}}, ), Entry(`Natural → Natural`, - Pi{Label: "_", Domain: Natural, Range: func(x Value) Value { + Pi{Label: "_", Domain: Natural, Codomain: func(x Value) Value { return Natural }}, term.Pi{Label: "_", Type: term.Natural, Body: term.Natural}, ), Entry(`∀(a : Type) → List a`, - Pi{Label: "a", Domain: Type, Range: func(x Value) Value { + Pi{Label: "a", Domain: Type, Codomain: func(x Value) Value { return ListOf{x} }}, term.Pi{Label: "a", Type: term.Type, Body: term.App{term.List, term.Var{"a", 0}}}, diff --git a/core/typecheck.go b/core/typecheck.go index 80bd47f..150e03e 100644 --- a/core/typecheck.go +++ b/core/typecheck.go @@ -54,6 +54,8 @@ func functionCheck(input Universe, output Universe) Universe { } } +// TypeOf typechecks a Term, returning the type in normal form. If +// typechecking fails, an error is returned. func TypeOf(t term.Term) (Value, error) { v, err := typeWith(context{}, t) if err != nil { @@ -209,7 +211,7 @@ func typeWith(ctx context, t term.Term) (Value, error) { if !AlphaEquivalent(expectedType, actualType) { return nil, mkTypeError(typeMismatch(Quote(expectedType), Quote(actualType))) } - bodyTypeVal := piType.Range(Eval(t.Arg)) + bodyTypeVal := piType.Codomain(Eval(t.Arg)) return bodyTypeVal, nil case term.Lambda: _, err := typeWith(ctx, t.Type) @@ -225,7 +227,7 @@ func typeWith(ctx context, t term.Term) (Value, error) { if err != nil { return nil, err } - pi.Range = func(x Value) Value { + pi.Codomain = func(x Value) Value { rebound := term.RebindLocal(freshLocal, Quote(bt)) return evalWith(rebound, env{ t.Label: []Value{x}, @@ -649,9 +651,9 @@ func typeWith(ctx context, t term.Term) (Value, error) { return unionType, nil } return Pi{ - Label: t.FieldName, - Domain: alternativeType, - Range: func(Value) Value { return unionType }, + Label: t.FieldName, + Domain: alternativeType, + Codomain: func(Value) Value { return unionType }, }, nil case term.Project: recordTypeVal, err := typeWith(ctx, t.Record) @@ -792,8 +794,8 @@ func typeWith(ctx context, t term.Term) (Value, error) { if !AlphaEquivalent(altType, pi.Domain) { return nil, mkTypeError(handlerInputTypeMismatch(Quote(altType), Quote(pi.Domain))) } - outputType := pi.Range(NaturalLit(1)) - outputType2 := pi.Range(NaturalLit(2)) + outputType := pi.Codomain(NaturalLit(1)) + outputType2 := pi.Codomain(NaturalLit(2)) if !AlphaEquivalent(outputType, outputType2) { // hacky way of detecting output type depending on input return nil, mkTypeError(disallowedHandlerType)