Update to standard v17.0.0 (#46)

Author: philandstuff

binary/cbor.go

@@ -50,9 +50,6 @@ var nameToBuiltin = map[string]Term{
 	"List/last":    ListLast,
 	"List/indexed": ListIndexed,
 	"List/reverse": ListReverse,
-
-	"Optional/build": OptionalBuild,
-	"Optional/fold":  OptionalFold,
 }
 
 func unwrapUint(i interface{}) (uint, error) {
@@ -107,7 +104,7 @@ func decode(decodedCbor interface{}) (Term, error) {
 		// _@n
 		return Var{Name: "_", Index: int(val)}, nil
 	case string:
-		// Type, Double, Optional/fold
+		// Type, Double, List/fold
 		if builtin, ok := nameToBuiltin[val]; ok {
 			return builtin, nil
 		}

core/ast.go

@@ -76,16 +76,8 @@ type (
 
 	doubleShow struct{}
 
-	optional      struct{}
-	optionalBuild struct{ typ Value }
-	optionalFold  struct {
-		typ1 Value
-		opt  Value
-		typ2 Value
-		some Value
-		// none Value
-	}
-	none struct{}
+	optional struct{}
+	none     struct{}
 
 	textShow struct{}
 
@@ -124,10 +116,8 @@ func (integerToDouble) isValue() {}
 
 func (doubleShow) isValue() {}
 
-func (optional) isValue()      {}
-func (optionalBuild) isValue() {}
-func (optionalFold) isValue()  {}
-func (none) isValue()          {}
+func (optional) isValue() {}
+func (none) isValue()     {}
 
 func (textShow) isValue() {}
 

core/builtins.go

@@ -193,80 +193,6 @@ func (doubleShow) ArgType() Value { return Double }
 func (optional) Call(x Value) Value { return OptionalOf{x} }
 func (optional) ArgType() Value     { return Type }
 
-func (build optionalBuild) Call(x Value) Value {
-	if build.typ == nil {
-		return optionalBuild{typ: x}
-	}
-	var some Value = lambda{
-		Label:  "a",
-		Domain: build.typ,
-		Fn: func(a Value) Value {
-			return Some{a}
-		},
-	}
-	return apply(x, OptionalOf{build.typ}, some, NoneOf{build.typ})
-}
-
-func (build optionalBuild) ArgType() Value {
-	if build.typ == nil {
-		return Type
-	}
-	return NewPi("optional", Type, func(optional Value) Value {
-		return NewFnType("just", NewFnType("_", build.typ, optional),
-			NewFnType("nothing", optional,
-				optional))
-	})
-}
-
-func (fold optionalFold) Call(x Value) Value {
-	if fold.typ1 == nil {
-		return optionalFold{typ1: x}
-	}
-	if fold.opt == nil {
-		return optionalFold{typ1: fold.typ1, opt: x}
-	}
-	if fold.typ2 == nil {
-		return optionalFold{
-			typ1: fold.typ1,
-			opt:  fold.opt,
-			typ2: x,
-		}
-	}
-	if fold.some == nil {
-		return optionalFold{
-			typ1: fold.typ1,
-			opt:  fold.opt,
-			typ2: fold.typ2,
-			some: x,
-		}
-	}
-	none := x
-	if s, ok := fold.opt.(Some); ok {
-		return apply(fold.some, s.Val)
-	}
-	if _, ok := fold.opt.(NoneOf); ok {
-		return none
-	}
-	return nil
-}
-
-func (fold optionalFold) ArgType() Value {
-	if fold.typ1 == nil {
-		return Type
-	}
-	if fold.opt == nil {
-		return OptionalOf{fold.typ1}
-	}
-	if fold.typ2 == nil {
-		return Type
-	}
-	if fold.some == nil {
-		return NewFnType("_", fold.typ1, fold.typ2)
-	}
-	// none
-	return fold.typ2
-}
-
 func (none) Call(a Value) Value { return NoneOf{a} }
 func (none) ArgType() Value     { return Type }
 
@@ -527,10 +453,8 @@ var (
 	IntegerToDouble  Callable = integerToDouble{}
 	DoubleShow       Callable = doubleShow{}
 
-	Optional      Callable = optional{}
-	OptionalBuild Callable = optionalBuild{}
-	OptionalFold  Callable = optionalFold{}
-	None          Callable = none{}
+	Optional Callable = optional{}
+	None     Callable = none{}
 
 	TextShow Callable = textShow{}
 

core/builtins_test.go

@@ -49,15 +49,6 @@ var _ = DescribeTable("ArgType of builtins", func(src, typ string) {
 	Entry("List/reverse arg 1", `List/reverse`, `Type`),
 	Entry("List/reverse arg 2", `List/reverse Natural`, `List Natural`),
 
-	Entry("Optional/build arg 1", `Optional/build`, `Type`),
-	Entry("Optional/build arg 2", `Optional/build Natural`,
-		`∀(optional : Type) → ∀(just : Natural → optional) → ∀(nothing : optional) → optional`),
-	Entry("Optional/fold arg 1", `Optional/fold`, `Type`),
-	Entry("Optional/fold arg 2", `Optional/fold Natural`, `Optional Natural`),
-	Entry("Optional/fold arg 3", `Optional/fold Natural (Some 2)`, `Type`),
-	Entry("Optional/fold arg 4", `Optional/fold Natural (Some 2) Text`, `Natural → Text`),
-	Entry("Optional/fold arg 5", `Optional/fold Natural (Some 2) Text (λ(x : Natural) → "some")`, `Text`),
-
 	Entry("Integer/show", `Integer/show`, `Integer`),
 	Entry("Integer/toDouble", `Integer/toDouble`, `Integer`),
 	Entry("Integer/negate", `Integer/negate`, `Integer`),

core/equivalence.go

@@ -20,7 +20,7 @@ func alphaEquivalentWith(level int, v1 Value, v2 Value) bool {
 		naturalSubtract, naturalToInteger,
 		integerShow, integerClamp, integerNegate, integerToDouble,
 		doubleShow,
-		optional, optionalBuild, optionalFold, none,
+		optional, none,
 		textShow,
 		list, listBuild, listFold, listHead, listIndexed,
 		listLength, listLast, listReverse,

core/eval.go

@@ -58,10 +58,6 @@ func evalWith(t term.Term, e env) Value {
 			return DoubleShow
 		case term.Optional:
 			return Optional
-		case term.OptionalBuild:
-			return OptionalBuild
-		case term.OptionalFold:
-			return OptionalFold
 		case term.None:
 			return None
 		case term.Text:

core/quote.go

@@ -78,29 +78,6 @@ func quoteWith(ctx quoteContext, shouldAlphaNormalize bool, v Value) term.Term {
 		return term.DoubleShow
 	case optional:
 		return term.Optional
-	case optionalBuild:
-		if v.typ != nil {
-			return term.App{term.OptionalBuild, quoteWith(ctx, shouldAlphaNormalize, v.typ)}
-		}
-		return term.OptionalBuild
-	case optionalFold:
-		var result term.Term = term.OptionalFold
-		if v.typ1 == nil {
-			return result
-		}
-		result = term.App{result, quoteWith(ctx, shouldAlphaNormalize, v.typ1)}
-		if v.opt == nil {
-			return result
-		}
-		result = term.App{result, quoteWith(ctx, shouldAlphaNormalize, v.opt)}
-		if v.typ2 == nil {
-			return result
-		}
-		result = term.App{result, quoteWith(ctx, shouldAlphaNormalize, v.typ2)}
-		if v.some == nil {
-			return result
-		}
-		return term.App{result, quoteWith(ctx, shouldAlphaNormalize, v.some)}
 	case none:
 		return term.None
 	case textShow:

core/typecheck.go

@@ -158,26 +158,6 @@ func typeWith(ctx context, t term.Term) (Value, error) {
 			return NewFnType("_", Natural, NewFnType("_", Natural, Natural)), nil
 		case term.None:
 			return NewPi("A", Type, func(A Value) Value { return OptionalOf{A} }), nil
-		case term.OptionalBuild:
-			return NewPi("a", Type, func(a Value) Value {
-				return NewFnType("_",
-					NewPi("optional", Type, func(optional Value) Value {
-						return NewFnType("just",
-							NewFnType("_", a, optional),
-							NewFnType("nothing", optional, optional))
-					}),
-					OptionalOf{a})
-			}), nil
-		case term.OptionalFold:
-			return NewPi("a", Type, func(a Value) Value {
-				return NewFnType("_",
-					OptionalOf{a},
-					NewPi("optional", Type, func(optional Value) Value {
-						return NewFnType("just",
-							NewFnType("_", a, optional),
-							NewFnType("nothing", optional, optional))
-					}))
-			}), nil
 		case term.TextShow:
 			return NewFnType("_", Text, Text), nil
 		default:

dhall-lang

@@ -24,7 +24,7 @@ handling skipped for brevity):
  dhallBytes, err := ioutil.ReadFile("foo.dhall")
  err = dhall.Unmarshal(dhallBytes, &m)
 
-This version supports Dhall standard 15.0.0, except that it doesn't
+This version supports Dhall standard 17.0.0, except that it doesn't
 support `using` directives.
 */
 package dhall