Skip to content

Commit

Permalink
Godoc gardening (#12)
Browse files Browse the repository at this point in the history
* more godoc gardening

* rename Range to Codomain

Partly because we can't use lowercase `range` for local variables as
it's a go keyword.
  • Loading branch information
philandstuff authored Feb 22, 2020
1 parent 31a594b commit e7f480c
Show file tree
Hide file tree
Showing 7 changed files with 46 additions and 37 deletions.
54 changes: 30 additions & 24 deletions core/ast.go
Original file line number Diff line number Diff line change
Expand Up @@ -9,15 +9,15 @@ 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().
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.
Expand All @@ -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.
Expand All @@ -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() {}
Expand Down Expand Up @@ -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 }
)

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 {
Expand All @@ -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

Expand All @@ -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 {
Expand All @@ -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 {
Expand Down
1 change: 1 addition & 0 deletions core/builtins.go
Original file line number Diff line number Diff line change
Expand Up @@ -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{}
Expand Down
4 changes: 2 additions & 2 deletions core/equivalence.go
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion core/eval.go
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion core/quote.go
Original file line number Diff line number Diff line change
Expand Up @@ -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),
Expand Down
4 changes: 2 additions & 2 deletions core/quote_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -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}}},
Expand Down
16 changes: 9 additions & 7 deletions core/typecheck.go
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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)
Expand All @@ -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},
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down

0 comments on commit e7f480c

Please sign in to comment.