M lib/dhall/ast.rb => lib/dhall/ast.rb +98 -14
@@ 179,7 179,11 @@ module Dhall
end
def dhall_eq(other)
- reduce(other, super)
+ if other.is_a?(Bool)
+ reduce(other, with(value: self == other))
+ else
+ reduce(other, super)
+ end
end
def as_json
@@ 197,6 201,10 @@ module Dhall
new(name: name, index: index)
end
+ def to_s
+ "#{name}@#{index}"
+ end
+
def as_json
if name == "_"
index
@@ 241,8 249,11 @@ module Dhall
end
class List < Expression
+ include Enumerable
+
include(ValueSemantics.for_attributes do
- elements ArrayOf(Expression)
+ elements Util::ArrayOf.new(Expression, min: 1)
+ type Either(nil, Expression), default: nil
end)
def self.of(*args)
@@ 253,12 264,8 @@ module Dhall
[4, nil, *elements.map(&:as_json)]
end
- def type
- # TODO: inferred element type
- end
-
def map(type: nil, &block)
- with(elements: elements.each_with_index.map(&block))
+ with(elements: elements.each_with_index.map(&block), type: type)
end
def each(&block)
@@ 275,11 282,11 @@ module Dhall
end
def first
- Optional.new(value: elements.first, type: type)
+ Optional.for(elements.first, type: type)
end
def last
- Optional.new(value: elements.last, type: type)
+ Optional.for(elements.last, type: type)
end
def reverse
@@ 297,7 304,7 @@ module Dhall
class EmptyList < List
include(ValueSemantics.for_attributes do
- type Expression
+ type Either(nil, Expression)
end)
def as_json
@@ 343,6 350,18 @@ module Dhall
type Either(nil, Expression), default: nil
end)
+ def self.for(value, type: nil)
+ if value.nil?
+ OptionalNone.new(type: type)
+ else
+ Optional.new(value: value, type: type)
+ end
+ end
+
+ def map(type: nil, &block)
+ with(value: block[value], type: type)
+ end
+
def reduce(_, &block)
block[value]
end
@@ 357,6 376,10 @@ module Dhall
type Expression
end)
+ def map(type: nil)
+ type.nil? ? self : with(type: type)
+ end
+
def reduce(z)
z
end
@@ 384,8 407,22 @@ module Dhall
record Util::HashOf.new(::String, Expression, min: 1)
end)
+ def self.for(types)
+ if types.empty?
+ EmptyRecordType.new
+ else
+ RecordType.new(record: types)
+ end
+ end
+
+ def merge_type(other)
+ return self if other.is_a?(EmptyRecordType)
+
+ with(record: record.merge(other.record))
+ end
+
def deep_merge_type(other)
- return super unless other.is_a?(RecordType)
+ return super unless other.class == RecordType
with(record: Hash[record.merge(other.record) { |_, v1, v2|
v1.deep_merge_type(v2)
@@ 405,9 442,17 @@ module Dhall
end
end
- class EmptyRecordType < Expression
+ class EmptyRecordType < RecordType
include(ValueSemantics.for_attributes {})
+ def record
+ {}
+ end
+
+ def merge_type(other)
+ other
+ end
+
def deep_merge_type(other)
other
end
@@ 448,6 493,10 @@ module Dhall
with(record: Hash[record.merge(other.record).sort])
end
+ def map(&block)
+ with(record: Hash[record.map(&block)])
+ end
+
def ==(other)
other.respond_to?(:record) && record.to_a == other.record.to_a
end
@@ 480,6 529,10 @@ module Dhall
other
end
+ def map
+ self
+ end
+
def as_json
[8, {}]
end
@@ 512,6 565,10 @@ module Dhall
record Expression
end)
+ def selectors
+ []
+ end
+
def as_json
[10, record.as_json]
end
@@ 522,6 579,10 @@ module Dhall
alternatives Util::HashOf.new(::String, Expression)
end)
+ def record
+ alternatives
+ end
+
def ==(other)
other.is_a?(UnionType) && alternatives.to_a == other.alternatives.to_a
end
@@ 530,7 591,11 @@ module Dhall
self == other
end
- def fetch(k)
+ def fetch(k, default=nil)
+ if (default || block_given?) && !alternatives.key?(k)
+ return (default || yield)
+ end
+
remains = with(alternatives: alternatives.dup.tap { |r| r.delete(k) })
Function.new(
var: k,
@@ 540,7 605,7 @@ module Dhall
value: Variable.new(name: k),
alternatives: remains
)
- )
+ ).normalize
end
def as_json
@@ 944,6 1009,25 @@ module Dhall
body Expression
end)
+ def unflatten
+ lets.reverse.reduce(body) do |inside, let|
+ LetBlock.new(lets: [let], body: inside)
+ end
+ end
+
+ def desugar
+ lets.reverse.reduce(body) do |inside, let|
+ Application.new(
+ function: Function.new(
+ var: let.var,
+ type: let.type,
+ body: inside
+ ),
+ arguments: [let.assign]
+ )
+ end
+ end
+
def as_json
[25, *lets.flat_map(&:as_json), body.as_json]
end
M lib/dhall/binary.rb => lib/dhall/binary.rb +3 -3
@@ 70,10 70,10 @@ module Dhall
class List
def self.decode(type, *els)
- if type.nil?
- List.new(elements: els.map(&Dhall.method(:decode)))
+ if els.empty?
+ EmptyList.new(type: type.nil? ? nil : Dhall.decode(type))
else
- EmptyList.new(type: Dhall.decode(type))
+ List.new(elements: els.map(&Dhall.method(:decode)))
end
end
end
M lib/dhall/builtins.rb => lib/dhall/builtins.rb +2 -2
@@ 257,14 257,14 @@ module Dhall
protected
def _call(arg)
- arg.map(type: indexed_type(type)) do |x, idx|
+ arg.map(type: indexed_type(type)) { |x, idx|
Record.new(
record: {
"index" => Natural.new(value: idx),
"value" => x
}
)
- end
+ }.normalize
end
def indexed_type(value_type)
M lib/dhall/normalize.rb => lib/dhall/normalize.rb +13 -14
@@ 236,9 236,15 @@ module Dhall
end
class List
+ def normalize
+ super.with(type: nil)
+ end
end
class EmptyList
+ def normalize
+ super.with(type: type.normalize)
+ end
end
class Optional
@@ 353,21 359,14 @@ module Dhall
desugar.normalize
end
- def desugar
- lets.reverse.reduce(body) do |inside, let|
- Application.new(
- function: Function.new(
- var: let.var,
- type: let.type,
- body: inside
- ),
- arguments: [let.assign]
- )
- end
- end
-
def shift(amount, name, min_index)
- desugar.shift(amount, name, min_index)
+ return unflatten.shift(amount, name, min_index) if lets.length > 1
+ return super unless lets.first.var == name
+
+ with(
+ lets: [let.first.shift(amount, name, min_index)],
+ body: body.shift(amount, name, min_index + 1)
+ )
end
end
M lib/dhall/typecheck.rb => lib/dhall/typecheck.rb +652 -10
@@ 1,6 1,7 @@
# frozen_string_literal: true
require "dhall/ast"
+require "dhall/normalize"
module Dhall
module TypeChecker
@@ 8,7 9,8 @@ module Dhall
case expr
when Dhall::Variable
Variable.new(expr)
- when Dhall::Bool, Dhall::Natural, Dhall::Text
+ when Dhall::Bool, Dhall::Natural, Dhall::Text, Dhall::Integer,
+ Dhall::Double
Literal.new(expr)
when Dhall::TextLiteral
TextLiteral.new(expr)
@@ 16,11 18,14 @@ module Dhall
EmptyList.new(expr)
when Dhall::List
List.new(expr)
+ when Dhall::OptionalNone
+ OptionalNone.new(expr)
+ when Dhall::Optional
+ Optional.new(expr)
when Dhall::If
If.new(expr)
when Dhall::Application
- # TODO
- Variable.new(Dhall::Variable["Bool"])
+ Application.new(expr)
when Dhall::Operator::And, Dhall::Operator::Or,
Dhall::Operator::Equal, Dhall::Operator::NotEqual
Operator.new(expr, Dhall::Variable["Bool"])
@@ 30,6 35,36 @@ module Dhall
Operator.new(expr, Dhall::Variable["Text"])
when Dhall::Operator::ListConcatenate
OperatorListConcatenate.new(expr)
+ when Dhall::Operator::RecursiveRecordMerge
+ OperatorRecursiveRecordMerge.new(expr)
+ when Dhall::Operator::RightBiasedRecordMerge
+ OperatorRightBiasedRecordMerge.new(expr)
+ when Dhall::Operator::RecursiveRecordTypeMerge
+ OperatorRecursiveRecordTypeMerge.new(expr)
+ when Dhall::EmptyRecordType
+ EmptyAnonymousType.new(expr)
+ when Dhall::RecordType, Dhall::UnionType
+ AnonymousType.new(expr)
+ when Dhall::EmptyRecord
+ EmptyRecord.new(expr)
+ when Dhall::Record
+ Record.new(expr)
+ when Dhall::RecordSelection
+ RecordSelection.new(expr)
+ when Dhall::RecordProjection, Dhall::EmptyRecordProjection
+ RecordProjection.new(expr)
+ when Dhall::Union
+ Union.new(expr)
+ when Dhall::Merge
+ Merge.new(expr)
+ when Dhall::Forall
+ Forall.new(expr)
+ when Dhall::Function
+ Function.new(expr)
+ when Dhall::LetBlock
+ LetBlock.new(expr)
+ when Dhall::TypeAnnotation
+ TypeAnnotation.new(expr)
when Dhall::Builtin
Builtin.new(expr)
else
@@ 53,22 88,50 @@ module Dhall
name => [type] + @bindings[name]
))
end
+
+ def shift(amount, name, min_index)
+ self.class.new(@bindings.merge(
+ Hash[@bindings.map { |var, bindings|
+ [var, bindings.map { |b| b.shift(amount, name, min_index) }]
+ }]
+ ))
+ end
end
+ KINDS = [
+ Dhall::Variable["Type"],
+ Dhall::Variable["Kind"],
+ Dhall::Variable["Sort"]
+ ].freeze
+
class Variable
def initialize(var)
@var = var
end
BUILTIN = {
- "Type" => Dhall::Variable["Kind"],
- "Kind" => Dhall::Variable["Sort"],
- "Bool" => Dhall::Variable["Type"],
- "Natural" => Dhall::Variable["Type"],
- "Text" => Dhall::Variable["Type"],
- "List" => Dhall::Forall.of_arguments(
+ "Type" => Dhall::Variable["Kind"],
+ "Kind" => Dhall::Variable["Sort"],
+ "Bool" => Dhall::Variable["Type"],
+ "Natural" => Dhall::Variable["Type"],
+ "Integer" => Dhall::Variable["Type"],
+ "Double" => Dhall::Variable["Type"],
+ "Text" => Dhall::Variable["Type"],
+ "List" => Dhall::Forall.of_arguments(
Dhall::Variable["Type"],
body: Dhall::Variable["Type"]
+ ),
+ "Optional" => Dhall::Forall.of_arguments(
+ Dhall::Variable["Type"],
+ body: Dhall::Variable["Type"]
+ ),
+ "None" => Dhall::Forall.new(
+ var: "A",
+ type: Dhall::Variable["Type"],
+ body: Dhall::Application.new(
+ function: Dhall::Variable["Optional"],
+ arguments: [Dhall::Variable["A"]]
+ )
)
}.freeze
@@ 216,6 279,104 @@ module Dhall
end
end
+ class OperatorRecursiveRecordMerge
+ def initialize(expr)
+ @expr = expr
+ @lhs = TypeChecker.for(expr.lhs)
+ @rhs = TypeChecker.for(expr.rhs)
+ end
+
+ def annotate(context)
+ annotated_lhs = @lhs.annotate(context)
+ annotated_rhs = @rhs.annotate(context)
+
+ type = annotated_lhs.type.deep_merge_type(annotated_rhs.type)
+
+ unless type.is_a?(Dhall::RecordType)
+ raise TypeError, "RecursiveRecordMerge got #{type}"
+ end
+
+ # Annotate to sanity check
+ TypeChecker.for(type).annotate(context)
+
+ Dhall::TypeAnnotation.new(
+ value: @expr.with(lhs: annotated_lhs, rhs: annotated_rhs),
+ type: type
+ )
+ end
+ end
+
+ class OperatorRightBiasedRecordMerge
+ def initialize(expr)
+ @expr = expr
+ @lhs = TypeChecker.for(expr.lhs)
+ @rhs = TypeChecker.for(expr.rhs)
+ end
+
+ def annotate(context)
+ annotated_lhs = @lhs.annotate(context)
+ annotated_rhs = @rhs.annotate(context)
+
+ unless annotated_lhs.type.is_a?(Dhall::RecordType)
+ raise TypeError, "RecursiveRecordMerge got #{annotated_lhs.type}"
+ end
+
+ unless annotated_rhs.type.is_a?(Dhall::RecordType)
+ raise TypeError, "RecursiveRecordMerge got #{annotated_rhs.type}"
+ end
+
+ lkind = TypeChecker.for(annotated_lhs.type).annotate(context).type
+ rkind = TypeChecker.for(annotated_rhs.type).annotate(context).type
+
+ if lkind != rkind
+ raise TypeError, "RecursiveRecordMerge got mixed kinds: " \
+ "#{lkind}, #{rkind}"
+ end
+
+ type = annotated_lhs.type.merge_type(annotated_rhs.type)
+
+ # Annotate to sanity check
+ TypeChecker.for(type).annotate(context)
+
+ Dhall::TypeAnnotation.new(
+ value: @expr.with(lhs: annotated_lhs, rhs: annotated_rhs),
+ type: type
+ )
+ end
+ end
+
+ class OperatorRecursiveRecordTypeMerge
+ def initialize(expr)
+ @expr = expr
+ @lhs = TypeChecker.for(expr.lhs)
+ @rhs = TypeChecker.for(expr.rhs)
+ end
+
+ def annotate(context)
+ annotated_lhs = @lhs.annotate(context)
+ annotated_rhs = @rhs.annotate(context)
+
+ if annotated_lhs.type != annotated_rhs.type
+ raise TypeError, "RecursiveRecordTypeMerge mixed kinds: " \
+ "#{annotated_lhs.type}, #{annotated_rhs.type}"
+ end
+
+ type = @expr.lhs.deep_merge_type(@expr.rhs)
+
+ unless type.is_a?(Dhall::RecordType)
+ raise TypeError, "RecursiveRecordMerge got #{type}"
+ end
+
+ # Annotate to sanity check
+ TypeChecker.for(type).annotate(context)
+
+ Dhall::TypeAnnotation.new(
+ value: @expr,
+ type: annotated_lhs.type
+ )
+ end
+ end
+
class EmptyList
def initialize(expr)
@expr = expr
@@ 267,6 428,423 @@ module Dhall
end
end
+ class OptionalNone
+ def initialize(expr)
+ @expr = expr
+ end
+
+ def annotate(context)
+ type_type = TypeChecker.for(@expr.type).annotate(context).type
+ if type_type != Dhall::Variable["Type"]
+ raise TypeError, "OptionalNone element type not of type Type"
+ end
+
+ Dhall::TypeAnnotation.new(
+ value: @expr,
+ type: Dhall::Application.new(
+ function: Dhall::Variable["Optional"],
+ arguments: [@expr.type]
+ )
+ )
+ end
+ end
+
+ class Optional
+ def initialize(some)
+ @some = some
+ end
+
+ def annotate(context)
+ asome = @some.map(type: @some.type) do |el|
+ TypeChecker.for(el).annotate(context)
+ end
+ some = asome.with(type: asome.value.type)
+
+ type_type = TypeChecker.for(some.type).annotate(context).type
+ if type_type != Dhall::Variable["Type"]
+ raise TypeError, "Some type no of type Type, was: #{type_type}"
+ end
+
+ Dhall::TypeAnnotation.new(
+ value: some,
+ type: Dhall::Application.new(
+ function: Dhall::Variable["Optional"],
+ arguments: [some.type]
+ )
+ )
+ end
+ end
+
+ class EmptyAnonymousType
+ def initialize(expr)
+ @expr = expr
+ end
+
+ def annotate(context)
+ Dhall::TypeAnnotation.new(
+ value: @expr,
+ type: Dhall::Variable["Type"]
+ )
+ end
+ end
+
+ class AnonymousType
+ def initialize(type)
+ @type = type
+ end
+
+ def annotate(context)
+ kinds = @type.record.values.map do |mtype|
+ TypeChecker.for(mtype).annotate(context).type
+ end
+
+ if (bad = kinds.find { |t| !KINDS.include?(t) })
+ raise TypeError, "AnonymousType field kind #{bad} "\
+ "not one of #{KINDS}"
+ end
+
+ if (bad = kinds.find { |t| t != kinds.first })
+ raise TypeError, "AnonymousType field kind #{bad} "\
+ "does not match #{kinds.first}"
+ end
+
+ Dhall::TypeAnnotation.new(
+ value: @type,
+ type: kinds.first || KINDS.first
+ )
+ end
+ end
+
+ class EmptyRecord
+ def initialize(expr)
+ @expr = expr
+ end
+
+ def annotate(context)
+ Dhall::TypeAnnotation.new(
+ value: @expr,
+ type: Dhall::EmptyRecordType.new
+ )
+ end
+ end
+
+ class Record
+ def initialize(record)
+ @record = record
+ end
+
+ def annotate(context)
+ arecord = @record.map do |k, v|
+ [k, TypeChecker.for(v).annotate(context)]
+ end
+
+ type = Dhall::RecordType.for(Hash[
+ arecord.record.map { |k, v| [k, v.type] }
+ ])
+
+ # Annonate to sanity check
+ TypeChecker.for(type).annotate(context)
+
+ Dhall::TypeAnnotation.new(
+ value: arecord,
+ type: type
+ )
+ end
+ end
+
+ class RecordSelection
+ def initialize(selection)
+ @selection = selection
+ @record = selection.record
+ @selector = selection.selector
+ end
+
+ def annotate(context)
+ arecord = TypeChecker.for(@record).annotate(context)
+
+ if arecord.type == Dhall::Variable["Type"]
+ Dhall::TypeAnnotation.new(
+ value: @selection,
+ type: TypeChecker.for(@record.normalize.fetch(@selector) {
+ raise TypeError, "#{@record} has no field #{@selector}"
+ }).annotate(context).type.with(var: @selector)
+ )
+ else
+ fetch_from = if arecord.type.class == Dhall::RecordType
+ arecord.type.record
+ elsif arecord.value.is_a?(Dhall::Record)
+ arecord.value.record
+ else
+ raise TypeError, "RecordSelection on #{arecord.type}"
+ end
+
+ Dhall::TypeAnnotation.new(
+ value: @selection.with(record: arecord),
+ type: fetch_from.fetch(@selector) do
+ raise TypeError, "#{fetch_from} has no field #{@selector}"
+ end
+ )
+ end
+ end
+ end
+
+ class RecordProjection
+ def initialize(projection)
+ @projection = projection
+ @record = projection.record
+ @selectors = projection.selectors
+ end
+
+ def annotate(context)
+ arecord = TypeChecker.for(@record).annotate(context)
+
+ unless arecord.type.class == Dhall::RecordType
+ raise TypeError, "RecordProjection on #{arecord.type}"
+ end
+
+ slice = arecord.type.record.select { |k, _| @selectors.include?(k) }
+ if slice.size != @selectors.length
+ raise TypeError, "#{arecord.type} missing one of: #{@selectors}"
+ end
+
+ Dhall::TypeAnnotation.new(
+ value: @projection.with(record: arecord),
+ type: Dhall::RecordType.for(slice)
+ )
+ end
+ end
+
+ class Union
+ def initialize(union)
+ @union = union
+ @value = TypeChecker.for(union.value)
+ end
+
+ def annotate(context)
+ annotated_value = @value.annotate(context)
+
+ type = Dhall::UnionType.new(
+ alternatives: Hash[@union.alternatives.alternatives.merge(
+ @union.tag => annotated_value.type
+ ).sort]
+ )
+
+ # Annotate to sanity check
+ TypeChecker.for(type).annotate(context)
+
+ Dhall::TypeAnnotation.new(
+ value: @union.with(value: annotated_value),
+ type: type
+ )
+ end
+ end
+
+ class Merge
+ def initialize(merge)
+ @merge = merge
+ @record = TypeChecker.for(merge.record)
+ @union = TypeChecker.for(merge.input)
+ end
+
+ def annotate(context)
+ arecord = @record.annotate(context)
+ aunion = @union.annotate(context)
+
+ unless arecord.type.is_a?(Dhall::RecordType)
+ raise TypeError, "Merge expected Record got: #{arecord.type}"
+ end
+
+ unless aunion.type.is_a?(Dhall::UnionType)
+ raise TypeError, "Merge expected Union got: #{aunion.type}"
+ end
+
+ type = arecord.type.record.reduce(@merge.type) do |type, (k, htype)|
+ unless aunion.type.alternatives.key?(k)
+ raise TypeError, "Merge handler for unknown alternative: #{k}"
+ end
+
+ unless htype.is_a?(Dhall::Forall)
+ raise TypeError, "Merge handlers must all be functions"
+ end
+
+ if type && htype.body != type
+ raise TypeError, "Handler output types must all match"
+ end
+
+ htype.body.shift(-1, htype.var, 0)
+ end
+
+ aunion.type.alternatives.each do |k, atype|
+ unless arecord.type.record.key?(k)
+ raise TypeError, "No merge handler for alternative: #{k}"
+ end
+
+ unless arecord.type.record[k].type == atype
+ raise TypeError, "Handler argument does not match " \
+ "alternative type: #{atype}"
+ end
+ end
+
+ kind = TypeChecker.for(type).annotate(context).type
+ unless kind == Dhall::Variable["Type"]
+ raise TypeError, "Merge must have kind Type"
+ end
+
+ Dhall::TypeAnnotation.new(
+ value: @merge.with(record: arecord, input: aunion),
+ type: type
+ )
+ end
+ end
+
+ class Forall
+ def initialize(expr)
+ @expr = expr
+ @input = TypeChecker.for(expr.type)
+ @output = TypeChecker.for(expr.body)
+ end
+
+ def annotate(context)
+ inkind = @input.annotate(context).type
+ outkind = @output.annotate(
+ context.add(@expr.var, @expr.type).shift(1, @expr.var, 0)
+ ).type
+
+ if !KINDS.include?(inkind) || !KINDS.include?(outkind)
+ raise TypeError, "FunctionType part of this is a term"
+ end
+
+ if KINDS.index(outkind) > KINDS.index(inkind)
+ raise TypeError, "Dependent types are not allowed"
+ end
+
+ type = if outkind == KINDS.first
+ KINDS.first
+ else
+ KINDS[[KINDS.index(outkind), KINDS.index(inkind)].max]
+ end
+
+ Dhall::TypeAnnotation.new(
+ value: @expr,
+ type: type
+ )
+ end
+ end
+
+ class Function
+ def initialize(func)
+ @func = func
+ @output = TypeChecker.for(func.body)
+ end
+
+ def annotate(context)
+ abody = @output.annotate(
+ context.add(@func.var, @func.type).shift(1, @func.var, 0)
+ )
+
+ type = Dhall::Forall.new(
+ var: @func.var,
+ type: @func.type,
+ body: abody.type
+ )
+
+ # Annotate to sanity check
+ TypeChecker.for(type).annotate(context)
+
+ Dhall::TypeAnnotation.new(
+ value: @func.with(body: abody),
+ type: type
+ )
+ end
+ end
+
+ class Application
+ def initialize(app)
+ @app = app
+ @func = TypeChecker.for(app.function)
+ @arg = TypeChecker.for(app.arguments.first)
+ end
+
+ def annotate(context)
+ afunc = @func.annotate(context)
+ aarg = @arg.annotate(context)
+
+ unless afunc.type.is_a?(Dhall::Forall)
+ raise TypeError, "Application LHS is not a function"
+ end
+
+ unless afunc.type.type.normalize == aarg.type.normalize
+ raise TypeError, "Application expected #{afunc.type.type} "\
+ "got #{aarg.type}"
+ end
+
+ type = afunc.type.body.substitute(
+ Dhall::Variable[afunc.type.var],
+ aarg.value.shift(1, afunc.type.var, 0)
+ ).shift(-1, afunc.type.var, 0)
+
+ Dhall::TypeAnnotation.new(
+ value: @app.with(function: afunc, arguments: [aarg]),
+ type: type
+ )
+ end
+ end
+
+ class LetBlock
+ def initialize(letblock)
+ @letblock = letblock.unflatten
+ @let = @letblock.lets.first
+ end
+
+ def annotate(context)
+ aassign = TypeChecker.for(@let.assign).annotate(context)
+
+ if @let.type && @let.type != aassign.type
+ raise TypeError, "Let assignment does not match annotation: " \
+ "#{@let.type}, #{aassign.type}"
+ end
+
+ Dhall::Function.disable_alpha_normalization!
+ nassign = @let.assign.normalize.shift(1, @let.var, 0)
+ Dhall::Function.enable_alpha_normalization!
+
+ abody = TypeChecker.for(@letblock.body.substitute(
+ Dhall::Variable[@let.var],
+ nassign
+ ).shift(-1, @let.var, 0)).annotate(context)
+
+ ablock = @letblock.with(
+ lets: [@let.with(type: aassign.type)],
+ body: Dhall::TypeAnnotation.new(
+ value: @letblock.body,
+ type: abody.type
+ )
+ )
+
+ Dhall::TypeAnnotation.new(
+ value: ablock,
+ type: abody.type
+ )
+ end
+ end
+
+ class TypeAnnotation
+ def initialize(expr)
+ @expr = expr
+ end
+
+ def annotate(context)
+ redo_annotation = TypeChecker.for(@expr.value).annotate(context)
+
+ if redo_annotation.type == @expr.type
+ redo_annotation
+ else
+ raise TypeError, "TypeAnnotation does not match: " \
+ "#{@expr.type}, #{redo_annotation.type}"
+ end
+ end
+ end
+
class Builtin
def initialize(builtin)
@expr = builtin
@@ 459,7 1037,71 @@ module Dhall
arguments: [Dhall::Variable["a"]]
)
)
- )
+ ),
+ "Optional/fold" => Dhall::Forall.new(
+ var: "a",
+ type: Dhall::Variable["Type"],
+ body: Dhall::Forall.of_arguments(
+ Dhall::Application.new(
+ function: Dhall::Variable["Optional"],
+ arguments: [Dhall::Variable["a"]]
+ ),
+ body: Dhall::Forall.new(
+ var: "optional",
+ type: Dhall::Variable["Type"],
+ body: Dhall::Forall.new(
+ var: "just",
+ type: Dhall::Forall.of_arguments(
+ Dhall::Variable["a"],
+ body: Dhall::Variable["optional"]
+ ),
+ body: Dhall::Forall.new(
+ var: "nothing",
+ type: Dhall::Variable["optional"],
+ body: Dhall::Variable["optional"]
+ )
+ )
+ )
+ )
+ ),
+ "Optional/build" => Dhall::Forall.new(
+ var: "a",
+ type: Dhall::Variable["Type"],
+ body: Dhall::Forall.of_arguments(
+ Dhall::Forall.new(
+ var: "optional",
+ type: Dhall::Variable["Type"],
+ body: Dhall::Forall.new(
+ var: "just",
+ type: Dhall::Forall.of_arguments(
+ Dhall::Variable["a"],
+ body: Dhall::Variable["optional"]
+ ),
+ body: Dhall::Forall.new(
+ var: "nothing",
+ type: Dhall::Variable["optional"],
+ body: Dhall::Variable["optional"]
+ )
+ )
+ ),
+ body: Dhall::Application.new(
+ function: Dhall::Variable["Optional"],
+ arguments: [Dhall::Variable["a"]]
+ )
+ )
+ ),
+ "Integer/show" => Dhall::Forall.of_arguments(
+ Dhall::Variable["Integer"],
+ body: Dhall::Variable["Text"]
+ ),
+ "Integer/toDouble" => Dhall::Forall.of_arguments(
+ Dhall::Variable["Integer"],
+ body: Dhall::Variable["Double"]
+ ),
+ "Double/show" => Dhall::Forall.of_arguments(
+ Dhall::Variable["Double"],
+ body: Dhall::Variable["Text"]
+ ),
}.freeze
def annotate(*)
M test/test_typechecker.rb => test/test_typechecker.rb +3 -2
@@ 6,12 6,13 @@ require "pathname"
require "dhall/typecheck"
require "dhall/binary"
-class TestNormalization < Minitest::Test
+class TestTypechecker < Minitest::Test
DIRPATH = Pathname.new(File.dirname(__FILE__))
TESTS = DIRPATH + "typechecker/"
Pathname.glob(TESTS + "success/**/*A.dhallb").each do |path|
test = path.relative_path_from(TESTS).to_s.sub(/A\.dhallb$/, "")
+ next if test =~ /prelude/
define_method("test_#{test}") do
assert_equal(
@@ 31,7 32,7 @@ class TestNormalization < Minitest::Test
expr = Dhall.from_binary(path.binread)
Dhall::TypeChecker.for(
expr
- ).annotate(Dhall::TypeChecker::Context.new).type
+ ).annotate(Dhall::TypeChecker::Context.new)
end
end
end
A test/typechecker/failure/FunctionApplicationArgumentNotMatch.dhallb => test/typechecker/failure/FunctionApplicationArgumentNotMatch.dhallb +0 -0
A test/typechecker/failure/FunctionApplicationIsNotFunction.dhallb => test/typechecker/failure/FunctionApplicationIsNotFunction.dhallb +0 -0
A test/typechecker/failure/FunctionArgumentTypeNotAType.dhallb => test/typechecker/failure/FunctionArgumentTypeNotAType.dhallb +0 -0
A test/typechecker/failure/FunctionDependentType.dhallb => test/typechecker/failure/FunctionDependentType.dhallb +1 -0
@@ 0,0 1,1 @@
+�axdBooldBool<
\ No newline at end of file
A test/typechecker/failure/FunctionDependentType2.dhallb => test/typechecker/failure/FunctionDependentType2.dhallb +1 -0
@@ 0,0 1,1 @@
+�axdBooldType<
\ No newline at end of file
A test/typechecker/failure/FunctionTypeArgumentTypeNotAType.dhallb => test/typechecker/failure/FunctionTypeArgumentTypeNotAType.dhallb +0 -0
A test/typechecker/failure/FunctionTypeKindSort.dhallb => test/typechecker/failure/FunctionTypeKindSort.dhallb +1 -0
@@ 0,0 1,1 @@
+�dKinddSort<
\ No newline at end of file
A test/typechecker/failure/FunctionTypeTypeKind.dhallb => test/typechecker/failure/FunctionTypeTypeKind.dhallb +1 -0
@@ 0,0 1,1 @@
+�dTypedKind<
\ No newline at end of file
A test/typechecker/failure/FunctionTypeTypeSort.dhallb => test/typechecker/failure/FunctionTypeTypeSort.dhallb +1 -0
@@ 0,0 1,1 @@
+�dTypedSort<
\ No newline at end of file
A test/typechecker/failure/LetWithWrongAnnotation.dhallb => test/typechecker/failure/LetWithWrongAnnotation.dhallb +1 -0
@@ 0,0 1,1 @@
+�axgNatural��<
\ No newline at end of file
A test/typechecker/failure/MergeAlternativeHasNoHandler.dhallb => test/typechecker/failure/MergeAlternativeHasNoHandler.dhallb +1 -0
@@ 0,0 1,1 @@
+����ax��<
\ No newline at end of file
A test/typechecker/failure/MergeAnnotationNotType.dhallb => test/typechecker/failure/MergeAnnotationNotType.dhallb +1 -0
@@ 0,0 1,1 @@
+�����dType<
\ No newline at end of file
A test/typechecker/failure/MergeEmptyWithoutAnnotation.dhallb => test/typechecker/failure/MergeEmptyWithoutAnnotation.dhallb +1 -0
@@ 0,0 1,1 @@
+�����<
\ No newline at end of file
A test/typechecker/failure/MergeHandlerNotFunction.dhallb => test/typechecker/failure/MergeHandlerNotFunction.dhallb +1 -0
@@ 0,0 1,1 @@
+���ax��ax��<
\ No newline at end of file
A test/typechecker/failure/MergeHandlerNotInUnion.dhallb => test/typechecker/failure/MergeHandlerNotInUnion.dhallb +0 -0
A test/typechecker/failure/MergeHandlerNotMatchAlternativeType.dhallb => test/typechecker/failure/MergeHandlerNotMatchAlternativeType.dhallb +0 -0
A test/typechecker/failure/MergeHandlersWithDifferentType.dhallb => test/typechecker/failure/MergeHandlersWithDifferentType.dhallb +0 -0
A test/typechecker/failure/MergeLhsNotRecord.dhallb => test/typechecker/failure/MergeLhsNotRecord.dhallb +1 -0
@@ 0,0 1,1 @@
+���ax��<
\ No newline at end of file
A test/typechecker/failure/MergeRhsNotUnion.dhallb => test/typechecker/failure/MergeRhsNotUnion.dhallb +1 -0
@@ 0,0 1,1 @@
+����<
\ No newline at end of file
A test/typechecker/failure/MergeWithWrongAnnotation.dhallb => test/typechecker/failure/MergeWithWrongAnnotation.dhallb +0 -0
A test/typechecker/failure/RecordMixedKinds.dhallb => test/typechecker/failure/RecordMixedKinds.dhallb +1 -0
@@ 0,0 1,1 @@
+��ax��aydBool<
\ No newline at end of file
A test/typechecker/failure/RecordMixedKinds2.dhallb => test/typechecker/failure/RecordMixedKinds2.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdTypeay��<
\ No newline at end of file
A test/typechecker/failure/RecordMixedKinds3.dhallb => test/typechecker/failure/RecordMixedKinds3.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdTypeaydKind<
\ No newline at end of file
A test/typechecker/failure/RecordProjectionEmpty.dhallb => test/typechecker/failure/RecordProjectionEmpty.dhallb +2 -0
@@ 0,0 1,2 @@
+�
+��ax<
\ No newline at end of file
A test/typechecker/failure/RecordProjectionNotPresent.dhallb => test/typechecker/failure/RecordProjectionNotPresent.dhallb +2 -0
@@ 0,0 1,2 @@
+�
+��ay��ax<
\ No newline at end of file
A test/typechecker/failure/RecordProjectionNotRecord.dhallb => test/typechecker/failure/RecordProjectionNotRecord.dhallb +2 -0
@@ 0,0 1,2 @@
+�
+�ax<
\ No newline at end of file
A test/typechecker/failure/RecordSelectionEmpty.dhallb => test/typechecker/failure/RecordSelectionEmpty.dhallb +1 -0
@@ 0,0 1,1 @@
+� ��ax<
\ No newline at end of file
A test/typechecker/failure/RecordSelectionNotPresent.dhallb => test/typechecker/failure/RecordSelectionNotPresent.dhallb +1 -0
@@ 0,0 1,1 @@
+� ��ay��ax<
\ No newline at end of file
A test/typechecker/failure/RecordSelectionNotRecord.dhallb => test/typechecker/failure/RecordSelectionNotRecord.dhallb +1 -0
@@ 0,0 1,1 @@
+� �ax<
\ No newline at end of file
A test/typechecker/failure/RecordTypeMixedKinds.dhallb => test/typechecker/failure/RecordTypeMixedKinds.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdBoolaydType<
\ No newline at end of file
A test/typechecker/failure/RecordTypeMixedKinds2.dhallb => test/typechecker/failure/RecordTypeMixedKinds2.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdKindaydType<
\ No newline at end of file
A test/typechecker/failure/RecordTypeMixedKinds3.dhallb => test/typechecker/failure/RecordTypeMixedKinds3.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdKindaydBool<
\ No newline at end of file
A test/typechecker/failure/RecordTypeValueMember.dhallb => test/typechecker/failure/RecordTypeValueMember.dhallb +1 -0
@@ 0,0 1,1 @@
+��ax�<
\ No newline at end of file
A test/typechecker/failure/RecursiveRecordMergeLhsNotRecord.dhallb => test/typechecker/failure/RecursiveRecordMergeLhsNotRecord.dhallb +1 -0
@@ 0,0 1,1 @@
+����<
\ No newline at end of file
A test/typechecker/failure/RecursiveRecordMergeMixedKinds.dhallb => test/typechecker/failure/RecursiveRecordMergeMixedKinds.dhallb +1 -0
@@ 0,0 1,1 @@
+���ax���aydBool<
\ No newline at end of file
A test/typechecker/failure/RecursiveRecordMergeOverlapping.dhallb => test/typechecker/failure/RecursiveRecordMergeOverlapping.dhallb +1 -0
@@ 0,0 1,1 @@
+���ax���ax�<
\ No newline at end of file
A test/typechecker/failure/RecursiveRecordMergeRhsNotRecord.dhallb => test/typechecker/failure/RecursiveRecordMergeRhsNotRecord.dhallb +1 -0
@@ 0,0 1,1 @@
+����<
\ No newline at end of file
A test/typechecker/failure/RecursiveRecordTypeMergeLhsNotRecordType.dhallb => test/typechecker/failure/RecursiveRecordTypeMergeLhsNotRecordType.dhallb +2 -0
@@ 0,0 1,2 @@
+�
+dBool��<
\ No newline at end of file
A test/typechecker/failure/RecursiveRecordTypeMergeOverlapping.dhallb => test/typechecker/failure/RecursiveRecordTypeMergeOverlapping.dhallb +2 -0
@@ 0,0 1,2 @@
+�
+��axdBool��axgNatural<
\ No newline at end of file
A test/typechecker/failure/RecursiveRecordTypeMergeRhsNotRecordType.dhallb => test/typechecker/failure/RecursiveRecordTypeMergeRhsNotRecordType.dhallb +2 -0
@@ 0,0 1,2 @@
+�
+��dBool<
\ No newline at end of file
A test/typechecker/failure/RightBiasedRecordMergeLhsNotRecord.dhallb => test/typechecker/failure/RightBiasedRecordMergeLhsNotRecord.dhallb +1 -0
@@ 0,0 1,1 @@
+� ���<
\ No newline at end of file
A test/typechecker/failure/RightBiasedRecordMergeMixedKinds.dhallb => test/typechecker/failure/RightBiasedRecordMergeMixedKinds.dhallb +1 -0
@@ 0,0 1,1 @@
+� ��ax����axdBool<
\ No newline at end of file
A test/typechecker/failure/RightBiasedRecordMergeMixedKinds2.dhallb => test/typechecker/failure/RightBiasedRecordMergeMixedKinds2.dhallb +1 -0
@@ 0,0 1,1 @@
+� ��axdBool��axdKind<
\ No newline at end of file
A test/typechecker/failure/RightBiasedRecordMergeMixedKinds3.dhallb => test/typechecker/failure/RightBiasedRecordMergeMixedKinds3.dhallb +1 -0
@@ 0,0 1,1 @@
+� ��ax����axdKind<
\ No newline at end of file
A test/typechecker/failure/RightBiasedRecordMergeRhsNotRecord.dhallb => test/typechecker/failure/RightBiasedRecordMergeRhsNotRecord.dhallb +1 -0
@@ 0,0 1,1 @@
+� ���<
\ No newline at end of file
A test/typechecker/failure/SomeNotType.dhallb => test/typechecker/failure/SomeNotType.dhallb +1 -0
@@ 0,0 1,1 @@
+��dBool<
\ No newline at end of file
A test/typechecker/failure/TypeAnnotationWrong.dhallb => test/typechecker/failure/TypeAnnotationWrong.dhallb +1 -0
@@ 0,0 1,1 @@
+��dBool<
\ No newline at end of file
A test/typechecker/failure/UnionConstructorFieldNotPresent.dhallb => test/typechecker/failure/UnionConstructorFieldNotPresent.dhallb +1 -0
@@ 0,0 1,1 @@
+� ��axdBoolay<
\ No newline at end of file
A test/typechecker/failure/UnionTypeMixedKinds.dhallb => test/typechecker/failure/UnionTypeMixedKinds.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdBoolaydType<
\ No newline at end of file
A test/typechecker/failure/UnionTypeMixedKinds2.dhallb => test/typechecker/failure/UnionTypeMixedKinds2.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdKindaydType<
\ No newline at end of file
A test/typechecker/failure/UnionTypeMixedKinds3.dhallb => test/typechecker/failure/UnionTypeMixedKinds3.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdKindaydBool<
\ No newline at end of file
A test/typechecker/failure/UnionTypeNotType.dhallb => test/typechecker/failure/UnionTypeNotType.dhallb +1 -0
@@ 0,0 1,1 @@
+��ax�<
\ No newline at end of file
A test/typechecker/gen => test/typechecker/gen +10 -0
@@ 0,0 1,10 @@
+#!/bin/sh
+
+cp -r "$(git root)"/dhall-lang/tests/typecheck/success "$(git root)"/test/typechecker/success/standard
+cp -r "$(git root)"/dhall-lang/tests/typecheck/failure "$(git root)"/test/typechecker/failure/standard
+
+cd "$(git root)"/test/typechecker/success/standard
+find . -name '*.dhall' -exec "$(git root)"/test/normalization/dhall-encode '{}' \;
+
+cd "$(git root)"/test/typechecker/failure/standard
+find . -name '*.dhall' -exec "$(git root)"/test/normalization/dhall-encode '{}' \;
A test/typechecker/success/DoubleA.dhallb => test/typechecker/success/DoubleA.dhallb +1 -0
@@ 0,0 1,1 @@
+fDouble<
\ No newline at end of file
A test/typechecker/success/DoubleB.dhallb => test/typechecker/success/DoubleB.dhallb +1 -0
@@ 0,0 1,1 @@
+dType<
\ No newline at end of file
A test/typechecker/success/DoubleLiteralA.dhallb => test/typechecker/success/DoubleLiteralA.dhallb +0 -0
A test/typechecker/success/DoubleLiteralB.dhallb => test/typechecker/success/DoubleLiteralB.dhallb +1 -0
@@ 0,0 1,1 @@
+fDouble<
\ No newline at end of file
A test/typechecker/success/DoubleShowA.dhallb => test/typechecker/success/DoubleShowA.dhallb +1 -0
@@ 0,0 1,1 @@
+kDouble/show<
\ No newline at end of file
A test/typechecker/success/DoubleShowB.dhallb => test/typechecker/success/DoubleShowB.dhallb +1 -0
@@ 0,0 1,1 @@
+�fDoubledText<
\ No newline at end of file
A test/typechecker/success/FunctionA.dhallb => test/typechecker/success/FunctionA.dhallb +0 -0
A test/typechecker/success/FunctionApplicationA.dhallb => test/typechecker/success/FunctionApplicationA.dhallb +0 -0
A test/typechecker/success/FunctionApplicationB.dhallb => test/typechecker/success/FunctionApplicationB.dhallb +1 -0
@@ 0,0 1,1 @@
+dBool<
\ No newline at end of file
A test/typechecker/success/FunctionB.dhallb => test/typechecker/success/FunctionB.dhallb +1 -0
@@ 0,0 1,1 @@
+�dBooldBool<
\ No newline at end of file
A test/typechecker/success/FunctionNamedArgA.dhallb => test/typechecker/success/FunctionNamedArgA.dhallb +1 -0
@@ 0,0 1,1 @@
+�axdBoolax<
\ No newline at end of file
A test/typechecker/success/FunctionNamedArgB.dhallb => test/typechecker/success/FunctionNamedArgB.dhallb +1 -0
@@ 0,0 1,1 @@
+�axdBooldBool<
\ No newline at end of file
A test/typechecker/success/FunctionTypeKindKindA.dhallb => test/typechecker/success/FunctionTypeKindKindA.dhallb +1 -0
@@ 0,0 1,1 @@
+�dKinddKind<
\ No newline at end of file
A test/typechecker/success/FunctionTypeKindKindB.dhallb => test/typechecker/success/FunctionTypeKindKindB.dhallb +1 -0
@@ 0,0 1,1 @@
+dSort<
\ No newline at end of file
A test/typechecker/success/FunctionTypeKindTermA.dhallb => test/typechecker/success/FunctionTypeKindTermA.dhallb +1 -0
@@ 0,0 1,1 @@
+�dKinddBool<
\ No newline at end of file
A test/typechecker/success/FunctionTypeKindTermB.dhallb => test/typechecker/success/FunctionTypeKindTermB.dhallb +1 -0
@@ 0,0 1,1 @@
+dType<
\ No newline at end of file
A test/typechecker/success/FunctionTypeKindTypeA.dhallb => test/typechecker/success/FunctionTypeKindTypeA.dhallb +1 -0
@@ 0,0 1,1 @@
+�dKinddType<
\ No newline at end of file
A test/typechecker/success/FunctionTypeKindTypeB.dhallb => test/typechecker/success/FunctionTypeKindTypeB.dhallb +1 -0
@@ 0,0 1,1 @@
+dSort<
\ No newline at end of file
A test/typechecker/success/FunctionTypeTermTermA.dhallb => test/typechecker/success/FunctionTypeTermTermA.dhallb +1 -0
@@ 0,0 1,1 @@
+�dBooldBool<
\ No newline at end of file
A test/typechecker/success/FunctionTypeTermTermB.dhallb => test/typechecker/success/FunctionTypeTermTermB.dhallb +1 -0
@@ 0,0 1,1 @@
+dType<
\ No newline at end of file
A test/typechecker/success/FunctionTypeTypeTermA.dhallb => test/typechecker/success/FunctionTypeTypeTermA.dhallb +1 -0
@@ 0,0 1,1 @@
+�dTypedBool<
\ No newline at end of file
A test/typechecker/success/FunctionTypeTypeTermB.dhallb => test/typechecker/success/FunctionTypeTypeTermB.dhallb +1 -0
@@ 0,0 1,1 @@
+dType<
\ No newline at end of file
A test/typechecker/success/FunctionTypeTypeTypeA.dhallb => test/typechecker/success/FunctionTypeTypeTypeA.dhallb +1 -0
@@ 0,0 1,1 @@
+�dTypedType<
\ No newline at end of file
A test/typechecker/success/FunctionTypeTypeTypeB.dhallb => test/typechecker/success/FunctionTypeTypeTypeB.dhallb +1 -0
@@ 0,0 1,1 @@
+dKind<
\ No newline at end of file
A test/typechecker/success/FunctionTypeUsingArgumentA.dhallb => test/typechecker/success/FunctionTypeUsingArgumentA.dhallb +0 -0
A test/typechecker/success/FunctionTypeUsingArgumentB.dhallb => test/typechecker/success/FunctionTypeUsingArgumentB.dhallb +1 -0
@@ 0,0 1,1 @@
+dType<
\ No newline at end of file
A test/typechecker/success/IntegerA.dhallb => test/typechecker/success/IntegerA.dhallb +1 -0
@@ 0,0 1,1 @@
+gInteger<
\ No newline at end of file
A test/typechecker/success/IntegerB.dhallb => test/typechecker/success/IntegerB.dhallb +1 -0
@@ 0,0 1,1 @@
+dType<
\ No newline at end of file
A test/typechecker/success/IntegerLiteralA.dhallb => test/typechecker/success/IntegerLiteralA.dhallb +1 -0
@@ 0,0 1,1 @@
+�<
\ No newline at end of file
A test/typechecker/success/IntegerLiteralB.dhallb => test/typechecker/success/IntegerLiteralB.dhallb +1 -0
@@ 0,0 1,1 @@
+gInteger<
\ No newline at end of file
A test/typechecker/success/IntegerShowA.dhallb => test/typechecker/success/IntegerShowA.dhallb +1 -0
@@ 0,0 1,1 @@
+lInteger/show<
\ No newline at end of file
A test/typechecker/success/IntegerShowB.dhallb => test/typechecker/success/IntegerShowB.dhallb +1 -0
@@ 0,0 1,1 @@
+�gIntegerdText<
\ No newline at end of file
A test/typechecker/success/IntegerToDoubleA.dhallb => test/typechecker/success/IntegerToDoubleA.dhallb +1 -0
@@ 0,0 1,1 @@
+pInteger/toDouble<
\ No newline at end of file
A test/typechecker/success/IntegerToDoubleB.dhallb => test/typechecker/success/IntegerToDoubleB.dhallb +1 -0
@@ 0,0 1,1 @@
+�gIntegerfDouble<
\ No newline at end of file
A test/typechecker/success/LetA.dhallb => test/typechecker/success/LetA.dhallb +1 -0
@@ 0,0 1,1 @@
+�ax��ax<
\ No newline at end of file
A test/typechecker/success/LetB.dhallb => test/typechecker/success/LetB.dhallb +1 -0
@@ 0,0 1,1 @@
+dBool<
\ No newline at end of file
A test/typechecker/success/LetNestedTypeSynonymA.dhallb => test/typechecker/success/LetNestedTypeSynonymA.dhallb +1 -0
@@ 0,0 1,1 @@
+�ax�dBoolayax�ay<
\ No newline at end of file
A test/typechecker/success/LetNestedTypeSynonymB.dhallb => test/typechecker/success/LetNestedTypeSynonymB.dhallb +1 -0
@@ 0,0 1,1 @@
+dBool<
\ No newline at end of file
A test/typechecker/success/LetTypeSynonymA.dhallb => test/typechecker/success/LetTypeSynonymA.dhallb +1 -0
@@ 0,0 1,1 @@
+�ax�dBool��ax<
\ No newline at end of file
A test/typechecker/success/LetTypeSynonymB.dhallb => test/typechecker/success/LetTypeSynonymB.dhallb +1 -0
@@ 0,0 1,1 @@
+dBool<
\ No newline at end of file
A test/typechecker/success/LetWithAnnotationA.dhallb => test/typechecker/success/LetWithAnnotationA.dhallb +1 -0
@@ 0,0 1,1 @@
+�axdBool�ax<
\ No newline at end of file
A test/typechecker/success/LetWithAnnotationB.dhallb => test/typechecker/success/LetWithAnnotationB.dhallb +1 -0
@@ 0,0 1,1 @@
+dBool<
\ No newline at end of file
A test/typechecker/success/MergeEmptyUnionA.dhallb => test/typechecker/success/MergeEmptyUnionA.dhallb +1 -0
@@ 0,0 1,1 @@
+�ax�����axdBool<
\ No newline at end of file
A test/typechecker/success/MergeEmptyUnionB.dhallb => test/typechecker/success/MergeEmptyUnionB.dhallb +1 -0
@@ 0,0 1,1 @@
+�ax��dBool<
\ No newline at end of file
A test/typechecker/success/MergeOneA.dhallb => test/typechecker/success/MergeOneA.dhallb +0 -0
A test/typechecker/success/MergeOneB.dhallb => test/typechecker/success/MergeOneB.dhallb +1 -0
@@ 0,0 1,1 @@
+dBool<
\ No newline at end of file
A test/typechecker/success/MergeOneWithAnnotationA.dhallb => test/typechecker/success/MergeOneWithAnnotationA.dhallb +0 -0
A test/typechecker/success/MergeOneWithAnnotationB.dhallb => test/typechecker/success/MergeOneWithAnnotationB.dhallb +1 -0
@@ 0,0 1,1 @@
+dBool<
\ No newline at end of file
A test/typechecker/success/NoneA.dhallb => test/typechecker/success/NoneA.dhallb +1 -0
@@ 0,0 1,1 @@
+dNone<
\ No newline at end of file
A test/typechecker/success/NoneB.dhallb => test/typechecker/success/NoneB.dhallb +0 -0
A test/typechecker/success/OldOptionalNoneA.dhallb => test/typechecker/success/OldOptionalNoneA.dhallb +1 -0
@@ 0,0 1,1 @@
+�dBool<
\ No newline at end of file
A test/typechecker/success/OldOptionalNoneB.dhallb => test/typechecker/success/OldOptionalNoneB.dhallb +0 -0
A test/typechecker/success/OldOptionalTrueA.dhallb => test/typechecker/success/OldOptionalTrueA.dhallb +1 -0
@@ 0,0 1,1 @@
+�dBool�<
\ No newline at end of file
A test/typechecker/success/OldOptionalTrueB.dhallb => test/typechecker/success/OldOptionalTrueB.dhallb +0 -0
A test/typechecker/success/OptionalA.dhallb => test/typechecker/success/OptionalA.dhallb +1 -0
@@ 0,0 1,1 @@
+hOptional<
\ No newline at end of file
A test/typechecker/success/OptionalB.dhallb => test/typechecker/success/OptionalB.dhallb +1 -0
@@ 0,0 1,1 @@
+�dTypedType<
\ No newline at end of file
A test/typechecker/success/OptionalBuildA.dhallb => test/typechecker/success/OptionalBuildA.dhallb +1 -0
@@ 0,0 1,1 @@
+nOptional/build<
\ No newline at end of file
A test/typechecker/success/OptionalBuildB.dhallb => test/typechecker/success/OptionalBuildB.dhallb +0 -0
A test/typechecker/success/OptionalFoldA.dhallb => test/typechecker/success/OptionalFoldA.dhallb +1 -0
@@ 0,0 1,1 @@
+mOptional/fold<
\ No newline at end of file
A test/typechecker/success/OptionalFoldB.dhallb => test/typechecker/success/OptionalFoldB.dhallb +0 -0
A test/typechecker/success/RecordEmptyA.dhallb => test/typechecker/success/RecordEmptyA.dhallb +1 -0
@@ 0,0 1,1 @@
+��<
\ No newline at end of file
A test/typechecker/success/RecordEmptyB.dhallb => test/typechecker/success/RecordEmptyB.dhallb +1 -0
@@ 0,0 1,1 @@
+��<
\ No newline at end of file
A test/typechecker/success/RecordOneKindA.dhallb => test/typechecker/success/RecordOneKindA.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdType<
\ No newline at end of file
A test/typechecker/success/RecordOneKindB.dhallb => test/typechecker/success/RecordOneKindB.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdKind<
\ No newline at end of file
A test/typechecker/success/RecordOneTypeA.dhallb => test/typechecker/success/RecordOneTypeA.dhallb +1 -0
@@ 0,0 1,1 @@
+��ax��<
\ No newline at end of file
A test/typechecker/success/RecordOneTypeB.dhallb => test/typechecker/success/RecordOneTypeB.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdType<
\ No newline at end of file
A test/typechecker/success/RecordOneValueA.dhallb => test/typechecker/success/RecordOneValueA.dhallb +1 -0
@@ 0,0 1,1 @@
+��ax��<
\ No newline at end of file
A test/typechecker/success/RecordOneValueB.dhallb => test/typechecker/success/RecordOneValueB.dhallb +1 -0
@@ 0,0 1,1 @@
+��ax��<
\ No newline at end of file
A test/typechecker/success/RecordProjectionEmptyA.dhallb => test/typechecker/success/RecordProjectionEmptyA.dhallb +2 -0
@@ 0,0 1,2 @@
+�
+��ax��<
\ No newline at end of file
A test/typechecker/success/RecordProjectionEmptyB.dhallb => test/typechecker/success/RecordProjectionEmptyB.dhallb +1 -0
@@ 0,0 1,1 @@
+��<
\ No newline at end of file
A test/typechecker/success/RecordProjectionKindA.dhallb => test/typechecker/success/RecordProjectionKindA.dhallb +2 -0
@@ 0,0 1,2 @@
+�
+��axdTypeaydTypeax<
\ No newline at end of file
A test/typechecker/success/RecordProjectionKindB.dhallb => test/typechecker/success/RecordProjectionKindB.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdKind<
\ No newline at end of file
A test/typechecker/success/RecordProjectionTypeA.dhallb => test/typechecker/success/RecordProjectionTypeA.dhallb +2 -0
@@ 0,0 1,2 @@
+�
+��axdBoolaygNaturalax<
\ No newline at end of file
A test/typechecker/success/RecordProjectionTypeB.dhallb => test/typechecker/success/RecordProjectionTypeB.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdType<
\ No newline at end of file
A test/typechecker/success/RecordProjectionValueA.dhallb => test/typechecker/success/RecordProjectionValueA.dhallb +2 -0
@@ 0,0 1,2 @@
+�
+��ax��ay��ax<
\ No newline at end of file
A test/typechecker/success/RecordProjectionValueB.dhallb => test/typechecker/success/RecordProjectionValueB.dhallb +1 -0
@@ 0,0 1,1 @@
+��ax��<
\ No newline at end of file
A test/typechecker/success/RecordSelectionKindA.dhallb => test/typechecker/success/RecordSelectionKindA.dhallb +1 -0
@@ 0,0 1,1 @@
+� ��axdTypeax<
\ No newline at end of file
A test/typechecker/success/RecordSelectionKindB.dhallb => test/typechecker/success/RecordSelectionKindB.dhallb +1 -0
@@ 0,0 1,1 @@
+dKind<
\ No newline at end of file
A test/typechecker/success/RecordSelectionTypeA.dhallb => test/typechecker/success/RecordSelectionTypeA.dhallb +1 -0
@@ 0,0 1,1 @@
+� ��ax��ax<
\ No newline at end of file
A test/typechecker/success/RecordSelectionTypeB.dhallb => test/typechecker/success/RecordSelectionTypeB.dhallb +1 -0
@@ 0,0 1,1 @@
+dType<
\ No newline at end of file
A test/typechecker/success/RecordSelectionValueA.dhallb => test/typechecker/success/RecordSelectionValueA.dhallb +1 -0
@@ 0,0 1,1 @@
+� ��ax��ax<
\ No newline at end of file
A test/typechecker/success/RecordSelectionValueB.dhallb => test/typechecker/success/RecordSelectionValueB.dhallb +1 -0
@@ 0,0 1,1 @@
+��<
\ No newline at end of file
A test/typechecker/success/RecordTypeA.dhallb => test/typechecker/success/RecordTypeA.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdBool<
\ No newline at end of file
A test/typechecker/success/RecordTypeB.dhallb => test/typechecker/success/RecordTypeB.dhallb +1 -0
@@ 0,0 1,1 @@
+dType<
\ No newline at end of file
A test/typechecker/success/RecordTypeEmptyA.dhallb => test/typechecker/success/RecordTypeEmptyA.dhallb +1 -0
@@ 0,0 1,1 @@
+��<
\ No newline at end of file
A test/typechecker/success/RecordTypeEmptyB.dhallb => test/typechecker/success/RecordTypeEmptyB.dhallb +1 -0
@@ 0,0 1,1 @@
+dType<
\ No newline at end of file
A test/typechecker/success/RecordTypeKindA.dhallb => test/typechecker/success/RecordTypeKindA.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdKind<
\ No newline at end of file
A test/typechecker/success/RecordTypeKindB.dhallb => test/typechecker/success/RecordTypeKindB.dhallb +1 -0
@@ 0,0 1,1 @@
+dSort<
\ No newline at end of file
A test/typechecker/success/RecordTypeTypeA.dhallb => test/typechecker/success/RecordTypeTypeA.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdType<
\ No newline at end of file
A test/typechecker/success/RecordTypeTypeB.dhallb => test/typechecker/success/RecordTypeTypeB.dhallb +1 -0
@@ 0,0 1,1 @@
+dKind<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordMergeLhsEmptyA.dhallb => test/typechecker/success/RecursiveRecordMergeLhsEmptyA.dhallb +1 -0
@@ 0,0 1,1 @@
+�����ax�<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordMergeLhsEmptyB.dhallb => test/typechecker/success/RecursiveRecordMergeLhsEmptyB.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdBool<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordMergeRecursivelyA.dhallb => test/typechecker/success/RecursiveRecordMergeRecursivelyA.dhallb +1 -0
@@ 0,0 1,1 @@
+���ax��aa���ax��ab�<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordMergeRecursivelyB.dhallb => test/typechecker/success/RecursiveRecordMergeRecursivelyB.dhallb +1 -0
@@ 0,0 1,1 @@
+��ax��aadBoolabdBool<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordMergeRecursivelyKindsA.dhallb => test/typechecker/success/RecursiveRecordMergeRecursivelyKindsA.dhallb +1 -0
@@ 0,0 1,1 @@
+���ax��aadType��ax��abdType<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordMergeRecursivelyKindsB.dhallb => test/typechecker/success/RecursiveRecordMergeRecursivelyKindsB.dhallb +1 -0
@@ 0,0 1,1 @@
+��ax��aadKindabdKind<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordMergeRecursivelyTypesA.dhallb => test/typechecker/success/RecursiveRecordMergeRecursivelyTypesA.dhallb +1 -0
@@ 0,0 1,1 @@
+���ax��aadBool��ax��abgNatural<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordMergeRecursivelyTypesB.dhallb => test/typechecker/success/RecursiveRecordMergeRecursivelyTypesB.dhallb +1 -0
@@ 0,0 1,1 @@
+��ax��aadTypeabdType<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordMergeRhsEmptyA.dhallb => test/typechecker/success/RecursiveRecordMergeRhsEmptyA.dhallb +1 -0
@@ 0,0 1,1 @@
+���ax���<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordMergeRhsEmptyB.dhallb => test/typechecker/success/RecursiveRecordMergeRhsEmptyB.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdBool<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordMergeTwoA.dhallb => test/typechecker/success/RecursiveRecordMergeTwoA.dhallb +1 -0
@@ 0,0 1,1 @@
+���ax���ay�<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordMergeTwoB.dhallb => test/typechecker/success/RecursiveRecordMergeTwoB.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdBoolaydBool<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordMergeTwoKindsA.dhallb => test/typechecker/success/RecursiveRecordMergeTwoKindsA.dhallb +1 -0
@@ 0,0 1,1 @@
+���axdType��aydType<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordMergeTwoKindsB.dhallb => test/typechecker/success/RecursiveRecordMergeTwoKindsB.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdKindaydKind<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordMergeTwoTypesA.dhallb => test/typechecker/success/RecursiveRecordMergeTwoTypesA.dhallb +1 -0
@@ 0,0 1,1 @@
+���axdBool��aygNatural<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordMergeTwoTypesB.dhallb => test/typechecker/success/RecursiveRecordMergeTwoTypesB.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdTypeaydType<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordTypeMergeRecursivelyA.dhallb => test/typechecker/success/RecursiveRecordTypeMergeRecursivelyA.dhallb +2 -0
@@ 0,0 1,2 @@
+�
+��ax��aadBool��ay��abdBool<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordTypeMergeRecursivelyB.dhallb => test/typechecker/success/RecursiveRecordTypeMergeRecursivelyB.dhallb +1 -0
@@ 0,0 1,1 @@
+dType<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordTypeMergeRecursivelyKindsA.dhallb => test/typechecker/success/RecursiveRecordTypeMergeRecursivelyKindsA.dhallb +2 -0
@@ 0,0 1,2 @@
+�
+��ax��aadKind��ay��abdKind<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordTypeMergeRecursivelyKindsB.dhallb => test/typechecker/success/RecursiveRecordTypeMergeRecursivelyKindsB.dhallb +1 -0
@@ 0,0 1,1 @@
+dSort<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordTypeMergeRecursivelyTypesA.dhallb => test/typechecker/success/RecursiveRecordTypeMergeRecursivelyTypesA.dhallb +2 -0
@@ 0,0 1,2 @@
+�
+��ax��aadType��ay��abdType<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordTypeMergeRecursivelyTypesB.dhallb => test/typechecker/success/RecursiveRecordTypeMergeRecursivelyTypesB.dhallb +1 -0
@@ 0,0 1,1 @@
+dKind<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordTypeMergeRhsEmptyA.dhallb => test/typechecker/success/RecursiveRecordTypeMergeRhsEmptyA.dhallb +2 -0
@@ 0,0 1,2 @@
+�
+��axdBool��<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordTypeMergeRhsEmptyB.dhallb => test/typechecker/success/RecursiveRecordTypeMergeRhsEmptyB.dhallb +1 -0
@@ 0,0 1,1 @@
+dType<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordTypeMergeTwoA.dhallb => test/typechecker/success/RecursiveRecordTypeMergeTwoA.dhallb +2 -0
@@ 0,0 1,2 @@
+�
+��axdBool��aydBool<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordTypeMergeTwoB.dhallb => test/typechecker/success/RecursiveRecordTypeMergeTwoB.dhallb +1 -0
@@ 0,0 1,1 @@
+dType<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordTypeMergeTwoKindsA.dhallb => test/typechecker/success/RecursiveRecordTypeMergeTwoKindsA.dhallb +2 -0
@@ 0,0 1,2 @@
+�
+��axdKind��aydKind<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordTypeMergeTwoKindsB.dhallb => test/typechecker/success/RecursiveRecordTypeMergeTwoKindsB.dhallb +1 -0
@@ 0,0 1,1 @@
+dSort<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordTypeMergeTwoTypesA.dhallb => test/typechecker/success/RecursiveRecordTypeMergeTwoTypesA.dhallb +2 -0
@@ 0,0 1,2 @@
+�
+��axdType��aydType<
\ No newline at end of file
A test/typechecker/success/RecursiveRecordTypeMergeTwoTypesB.dhallb => test/typechecker/success/RecursiveRecordTypeMergeTwoTypesB.dhallb +1 -0
@@ 0,0 1,1 @@
+dKind<
\ No newline at end of file
A test/typechecker/success/RightBiasedRecordMergeRhsEmptyA.dhallb => test/typechecker/success/RightBiasedRecordMergeRhsEmptyA.dhallb +1 -0
@@ 0,0 1,1 @@
+� ��ax����<
\ No newline at end of file
A test/typechecker/success/RightBiasedRecordMergeRhsEmptyB.dhallb => test/typechecker/success/RightBiasedRecordMergeRhsEmptyB.dhallb +1 -0
@@ 0,0 1,1 @@
+��ax��<
\ No newline at end of file
A test/typechecker/success/RightBiasedRecordMergeTwoA.dhallb => test/typechecker/success/RightBiasedRecordMergeTwoA.dhallb +1 -0
@@ 0,0 1,1 @@
+� ��ax����ax��<
\ No newline at end of file
A test/typechecker/success/RightBiasedRecordMergeTwoB.dhallb => test/typechecker/success/RightBiasedRecordMergeTwoB.dhallb +1 -0
@@ 0,0 1,1 @@
+��ax��<
\ No newline at end of file
A test/typechecker/success/RightBiasedRecordMergeTwoDifferentA.dhallb => test/typechecker/success/RightBiasedRecordMergeTwoDifferentA.dhallb +1 -0
@@ 0,0 1,1 @@
+� ��ax����ax�<
\ No newline at end of file
A test/typechecker/success/RightBiasedRecordMergeTwoDifferentB.dhallb => test/typechecker/success/RightBiasedRecordMergeTwoDifferentB.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdBool<
\ No newline at end of file
A test/typechecker/success/RightBiasedRecordMergeTwoKindsA.dhallb => test/typechecker/success/RightBiasedRecordMergeTwoKindsA.dhallb +1 -0
@@ 0,0 1,1 @@
+� ��axdType��axdType<
\ No newline at end of file
A test/typechecker/success/RightBiasedRecordMergeTwoKindsB.dhallb => test/typechecker/success/RightBiasedRecordMergeTwoKindsB.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdKind<
\ No newline at end of file
A test/typechecker/success/RightBiasedRecordMergeTwoTypesA.dhallb => test/typechecker/success/RightBiasedRecordMergeTwoTypesA.dhallb +1 -0
@@ 0,0 1,1 @@
+� ��axdBool��axgNatural<
\ No newline at end of file
A test/typechecker/success/RightBiasedRecordMergeTwoTypesB.dhallb => test/typechecker/success/RightBiasedRecordMergeTwoTypesB.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdType<
\ No newline at end of file
A test/typechecker/success/SomeTrueA.dhallb => test/typechecker/success/SomeTrueA.dhallb +1 -0
@@ 0,0 1,1 @@
+���<
\ No newline at end of file
A test/typechecker/success/SomeTrueB.dhallb => test/typechecker/success/SomeTrueB.dhallb +0 -0
A test/typechecker/success/TypeAnnotationA.dhallb => test/typechecker/success/TypeAnnotationA.dhallb +1 -0
@@ 0,0 1,1 @@
+��dBool<
\ No newline at end of file
A test/typechecker/success/TypeAnnotationB.dhallb => test/typechecker/success/TypeAnnotationB.dhallb +1 -0
@@ 0,0 1,1 @@
+dBool<
\ No newline at end of file
A test/typechecker/success/UnionConstructorFieldA.dhallb => test/typechecker/success/UnionConstructorFieldA.dhallb +1 -0
@@ 0,0 1,1 @@
+� ��axdBoolax<
\ No newline at end of file
A test/typechecker/success/UnionConstructorFieldB.dhallb => test/typechecker/success/UnionConstructorFieldB.dhallb +1 -0
@@ 0,0 1,1 @@
+�axdBool��axdBool<
\ No newline at end of file
A test/typechecker/success/UnionOneA.dhallb => test/typechecker/success/UnionOneA.dhallb +1 -0
@@ 0,0 1,1 @@
+�ax��<
\ No newline at end of file
A test/typechecker/success/UnionOneB.dhallb => test/typechecker/success/UnionOneB.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdBool<
\ No newline at end of file
A test/typechecker/success/UnionTypeEmptyA.dhallb => test/typechecker/success/UnionTypeEmptyA.dhallb +1 -0
@@ 0,0 1,1 @@
+��<
\ No newline at end of file
A test/typechecker/success/UnionTypeEmptyB.dhallb => test/typechecker/success/UnionTypeEmptyB.dhallb +1 -0
@@ 0,0 1,1 @@
+dType<
\ No newline at end of file
A test/typechecker/success/UnionTypeKindA.dhallb => test/typechecker/success/UnionTypeKindA.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdKind<
\ No newline at end of file
A test/typechecker/success/UnionTypeKindB.dhallb => test/typechecker/success/UnionTypeKindB.dhallb +1 -0
@@ 0,0 1,1 @@
+dSort<
\ No newline at end of file
A test/typechecker/success/UnionTypeOneA.dhallb => test/typechecker/success/UnionTypeOneA.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdBool<
\ No newline at end of file
A test/typechecker/success/UnionTypeOneB.dhallb => test/typechecker/success/UnionTypeOneB.dhallb +1 -0
@@ 0,0 1,1 @@
+dType<
\ No newline at end of file
A test/typechecker/success/UnionTypeTypeA.dhallb => test/typechecker/success/UnionTypeTypeA.dhallb +1 -0
@@ 0,0 1,1 @@
+��axdType<
\ No newline at end of file
A test/typechecker/success/UnionTypeTypeB.dhallb => test/typechecker/success/UnionTypeTypeB.dhallb +1 -0
@@ 0,0 1,1 @@
+dKind<
\ No newline at end of file