A lib/dhall/typecheck.rb => lib/dhall/typecheck.rb +475 -0
@@ 0,0 1,475 @@
+# frozen_string_literal: true
+
+require "dhall/ast"
+
+module Dhall
+ module TypeChecker
+ def self.for(expr)
+ case expr
+ when Dhall::Variable
+ Variable.new(expr)
+ when Dhall::Bool, Dhall::Natural, Dhall::Text
+ Literal.new(expr)
+ when Dhall::TextLiteral
+ TextLiteral.new(expr)
+ when Dhall::EmptyList
+ EmptyList.new(expr)
+ when Dhall::List
+ List.new(expr)
+ when Dhall::If
+ If.new(expr)
+ when Dhall::Application
+ # TODO
+ Variable.new(Dhall::Variable["Bool"])
+ when Dhall::Operator::And, Dhall::Operator::Or,
+ Dhall::Operator::Equal, Dhall::Operator::NotEqual
+ Operator.new(expr, Dhall::Variable["Bool"])
+ when Dhall::Operator::Plus, Dhall::Operator::Times
+ Operator.new(expr, Dhall::Variable["Natural"])
+ when Dhall::Operator::TextConcatenate
+ Operator.new(expr, Dhall::Variable["Text"])
+ when Dhall::Operator::ListConcatenate
+ OperatorListConcatenate.new(expr)
+ when Dhall::Builtin
+ Builtin.new(expr)
+ else
+ raise TypeError, "Unknown expression: #{expr}"
+ end
+ end
+
+ class Context
+ def initialize(bindings=Hash.new([]))
+ @bindings = bindings.freeze
+ freeze
+ end
+
+ def fetch(var)
+ @bindings[var.name][var.index] ||
+ (raise TypeError, "Free variable: #{var}")
+ end
+
+ def add(name, type)
+ self.class.new(@bindings.merge(
+ name => [type] + @bindings[name]
+ ))
+ end
+ end
+
+ 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(
+ Dhall::Variable["Type"],
+ body: Dhall::Variable["Type"]
+ )
+ }.freeze
+
+ def annotate(context)
+ if @var.name == "Sort"
+ raise TypeError, "Sort has no Type, Kind, or Sort"
+ end
+
+ Dhall::TypeAnnotation.new(
+ value: @var,
+ type: BUILTIN.fetch(@var.name) { context.fetch(@var) }
+ )
+ end
+ end
+
+ class Literal
+ def initialize(lit)
+ @lit = lit
+ @type = Dhall::Variable[lit.class.name.split(/::/).last]
+ end
+
+ def annotate(*)
+ Dhall::TypeAnnotation.new(
+ value: @lit,
+ type: @type
+ )
+ end
+ end
+
+ class TextLiteral
+ def initialize(lit)
+ @lit = lit
+ end
+
+ def annotate(context)
+ chunks = @lit.chunks.map do |c|
+ if c.is_a?(Dhall::Text)
+ c
+ else
+ annotated = TypeChecker.for(c).annotate(context)
+ if annotated.type != Dhall::Variable["Text"]
+ raise TypeError, "Cannot interpolate non-Text: " \
+ "#{annotated.type}"
+ end
+ annotated
+ end
+ end
+
+ Dhall::TypeAnnotation.new(
+ value: @lit.with(chunks: chunks),
+ type: Dhall::Variable["Text"]
+ )
+ end
+ end
+
+ class If
+ def initialize(expr)
+ @expr = expr
+ @predicate = TypeChecker.for(expr.predicate)
+ @then = TypeChecker.for(expr.then)
+ @else = TypeChecker.for(expr.else)
+ end
+
+ def annotate(context)
+ annotated_predicate = @predicate.annotate(context)
+ if annotated_predicate.type != Dhall::Variable["Bool"]
+ raise TypeError, "If must have a predicate of type Bool"
+ end
+
+ annotated_then = @then.annotate(context)
+ then_type_type = TypeChecker.for(annotated_then.type)
+ .annotate(context).type
+ if then_type_type != Dhall::Variable["Type"]
+ raise TypeError, "If branches must have types of type Type"
+ end
+
+ annotated_else = @else.annotate(context)
+ if annotated_then.type == annotated_else.type
+ Dhall::TypeAnnotation.new(
+ value: @expr.with(
+ predicate: annotated_predicate,
+ then: annotated_then,
+ else: annotated_else
+ ),
+ type: annotated_then.type
+ )
+ else
+ raise TypeError, "If branches have mismatched types: " \
+ "#{annotated_then.type}, #{annotated_else.type}"
+ end
+ end
+ end
+
+ class Operator
+ def initialize(expr, type)
+ @expr = expr
+ @lhs = TypeChecker.for(expr.lhs)
+ @rhs = TypeChecker.for(expr.rhs)
+ @type = type
+ end
+
+ def annotate(context)
+ annotated_lhs = @lhs.annotate(context)
+ annotated_rhs = @rhs.annotate(context)
+ types = [annotated_lhs.type, annotated_rhs.type]
+ if types.any? { |t| t != @type }
+ raise TypeError, "Operator arguments not #{@type}: #{types}"
+ end
+
+ Dhall::TypeAnnotation.new(
+ value: @expr.with(lhs: annotated_lhs, rhs: annotated_rhs),
+ type: @type
+ )
+ end
+ end
+
+ class OperatorListConcatenate
+ 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)
+ types = [annotated_lhs.type, annotated_rhs.type]
+ valid_types = types.all? do |t|
+ t.is_a?(Dhall::Application) &&
+ t.function == Dhall::Variable["List"]
+ end
+
+ unless valid_types
+ raise TypeError, "Operator arguments not List: #{types}"
+ end
+
+ unless annotated_lhs.type == annotated_rhs.type
+ raise TypeError, "Operator arguments do not match: #{types}"
+ end
+
+ Dhall::TypeAnnotation.new(
+ value: @expr.with(lhs: annotated_lhs, rhs: annotated_rhs),
+ type: annotated_lhs.type
+ )
+ end
+ end
+
+ class EmptyList
+ 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, "EmptyList element type not of type Type"
+ end
+
+ Dhall::TypeAnnotation.new(
+ value: @expr,
+ type: Dhall::Application.new(
+ function: Dhall::Variable["List"],
+ arguments: [@expr.type]
+ )
+ )
+ end
+ end
+
+ class List
+ def initialize(list)
+ @list = list
+ end
+
+ def annotate(context)
+ alist = @list.map(type: @list.type) do |el|
+ TypeChecker.for(el).annotate(context)
+ end
+ list = alist.with(type: alist.first.value.type)
+
+ if (bad = alist.find { |x| x.type != list.type })
+ raise TypeError, "List #{list.type} with element #{bad}"
+ end
+
+ type_type = TypeChecker.for(list.type).annotate(context).type
+ if type_type != Dhall::Variable["Type"]
+ raise TypeError, "List type no of type Type, was: #{type_type}"
+ end
+
+ Dhall::TypeAnnotation.new(
+ value: list,
+ type: Dhall::Application.new(
+ function: Dhall::Variable["List"],
+ arguments: [list.type]
+ )
+ )
+ end
+ end
+
+ class Builtin
+ def initialize(builtin)
+ @expr = builtin
+ @name = builtin.as_json
+ end
+
+ TYPES = {
+ "Natural/build" => Dhall::Forall.of_arguments(
+ Dhall::Forall.new(
+ var: "natural",
+ type: Dhall::Variable["Type"],
+ body: Dhall::Forall.new(
+ var: "succ",
+ type: Dhall::Forall.of_arguments(
+ Dhall::Variable["natural"],
+ body: Dhall::Variable["natural"]
+ ),
+ body: Dhall::Forall.new(
+ var: "zero",
+ type: Dhall::Variable["natural"],
+ body: Dhall::Variable["natural"]
+ )
+ )
+ ),
+ body: Dhall::Variable["Natural"]
+ ),
+ "Natural/fold" => Dhall::Forall.of_arguments(
+ Dhall::Variable["Natural"],
+ body: Dhall::Forall.new(
+ var: "natural",
+ type: Dhall::Variable["Type"],
+ body: Dhall::Forall.new(
+ var: "succ",
+ type: Dhall::Forall.of_arguments(
+ Dhall::Variable["natural"],
+ body: Dhall::Variable["natural"]
+ ),
+ body: Dhall::Forall.new(
+ var: "zero",
+ type: Dhall::Variable["natural"],
+ body: Dhall::Variable["natural"]
+ )
+ )
+ )
+ ),
+ "Natural/isZero" => Dhall::Forall.of_arguments(
+ Dhall::Variable["Natural"],
+ body: Dhall::Variable["Bool"]
+ ),
+ "Natural/even" => Dhall::Forall.of_arguments(
+ Dhall::Variable["Natural"],
+ body: Dhall::Variable["Bool"]
+ ),
+ "Natural/odd" => Dhall::Forall.of_arguments(
+ Dhall::Variable["Natural"],
+ body: Dhall::Variable["Bool"]
+ ),
+ "Natural/toInteger" => Dhall::Forall.of_arguments(
+ Dhall::Variable["Natural"],
+ body: Dhall::Variable["Integer"]
+ ),
+ "Natural/show" => Dhall::Forall.of_arguments(
+ Dhall::Variable["Natural"],
+ body: Dhall::Variable["Text"]
+ ),
+ "Text/show" => Dhall::Forall.of_arguments(
+ Dhall::Variable["Text"],
+ body: Dhall::Variable["Text"]
+ ),
+ "List/build" => Dhall::Forall.new(
+ var: "a",
+ type: Dhall::Variable["Type"],
+ body: Dhall::Forall.of_arguments(
+ Dhall::Forall.new(
+ var: "list",
+ type: Dhall::Variable["Type"],
+ body: Dhall::Forall.new(
+ var: "cons",
+ type: Dhall::Forall.of_arguments(
+ Dhall::Variable["a"],
+ Dhall::Variable["list"],
+ body: Dhall::Variable["list"]
+ ),
+ body: Dhall::Forall.new(
+ var: "nil",
+ type: Dhall::Variable["list"],
+ body: Dhall::Variable["list"]
+ )
+ )
+ ),
+ body: Dhall::Application.new(
+ function: Dhall::Variable["List"],
+ arguments: [Dhall::Variable["a"]]
+ )
+ )
+ ),
+ "List/fold" => Dhall::Forall.new(
+ var: "a",
+ type: Dhall::Variable["Type"],
+ body: Dhall::Forall.of_arguments(
+ Dhall::Application.new(
+ function: Dhall::Variable["List"],
+ arguments: [Dhall::Variable["a"]]
+ ),
+ body: Dhall::Forall.new(
+ var: "list",
+ type: Dhall::Variable["Type"],
+ body: Dhall::Forall.new(
+ var: "cons",
+ type: Dhall::Forall.of_arguments(
+ Dhall::Variable["a"],
+ Dhall::Variable["list"],
+ body: Dhall::Variable["list"]
+ ),
+ body: Dhall::Forall.new(
+ var: "nil",
+ type: Dhall::Variable["list"],
+ body: Dhall::Variable["list"]
+ )
+ )
+ )
+ )
+ ),
+ "List/length" => Dhall::Forall.new(
+ var: "a",
+ type: Dhall::Variable["Type"],
+ body: Dhall::Forall.of_arguments(
+ Dhall::Application.new(
+ function: Dhall::Variable["List"],
+ arguments: [Dhall::Variable["a"]]
+ ),
+ body: Dhall::Variable["Natural"]
+ )
+ ),
+ "List/head" => Dhall::Forall.new(
+ var: "a",
+ type: Dhall::Variable["Type"],
+ body: Dhall::Forall.of_arguments(
+ Dhall::Application.new(
+ function: Dhall::Variable["List"],
+ arguments: [Dhall::Variable["a"]]
+ ),
+ body: Dhall::Application.new(
+ function: Dhall::Variable["Optional"],
+ arguments: [Dhall::Variable["a"]]
+ )
+ )
+ ),
+ "List/last" => Dhall::Forall.new(
+ var: "a",
+ type: Dhall::Variable["Type"],
+ body: Dhall::Forall.of_arguments(
+ Dhall::Application.new(
+ function: Dhall::Variable["List"],
+ arguments: [Dhall::Variable["a"]]
+ ),
+ body: Dhall::Application.new(
+ function: Dhall::Variable["Optional"],
+ arguments: [Dhall::Variable["a"]]
+ )
+ )
+ ),
+ "List/indexed" => Dhall::Forall.new(
+ var: "a",
+ type: Dhall::Variable["Type"],
+ body: Dhall::Forall.of_arguments(
+ Dhall::Application.new(
+ function: Dhall::Variable["List"],
+ arguments: [Dhall::Variable["a"]]
+ ),
+ body: Dhall::Application.new(
+ function: Dhall::Variable["List"],
+ arguments: [Dhall::RecordType.new(record: {
+ "index" => Dhall::Variable["Natural"],
+ "value" => Dhall::Variable["a"]
+ })]
+ )
+ )
+ ),
+ "List/reverse" => Dhall::Forall.new(
+ var: "a",
+ type: Dhall::Variable["Type"],
+ body: Dhall::Forall.of_arguments(
+ Dhall::Application.new(
+ function: Dhall::Variable["List"],
+ arguments: [Dhall::Variable["a"]]
+ ),
+ body: Dhall::Application.new(
+ function: Dhall::Variable["List"],
+ arguments: [Dhall::Variable["a"]]
+ )
+ )
+ )
+ }.freeze
+
+ def annotate(*)
+ Dhall::TypeAnnotation.new(
+ value: @expr,
+ type: TYPES.fetch(@name) do
+ raise TypeError, "Unknown Builtin #{@name}"
+ end
+ )
+ end
+ end
+ end
+end
A test/test_typechecker.rb => test/test_typechecker.rb +66 -0
@@ 0,0 1,66 @@
+# frozen_string_literal: true
+
+require "minitest/autorun"
+require "pathname"
+
+require "dhall/typecheck"
+require "dhall/binary"
+
+class TestNormalization < 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$/, "")
+
+ define_method("test_#{test}") do
+ assert_equal(
+ Dhall.from_binary((TESTS + "#{test}B.dhallb").binread),
+ Dhall::TypeChecker.for(
+ Dhall.from_binary(path.binread)
+ ).annotate(Dhall::TypeChecker::Context.new).type
+ )
+ end
+ end
+
+ Pathname.glob(TESTS + "failure/**/*.dhallb").each do |path|
+ test = path.relative_path_from(TESTS).to_s.sub(/.dhallb$/, "")
+
+ define_method("test_#{test}") do
+ assert_raises TypeError do
+ expr = Dhall.from_binary(path.binread)
+ Dhall::TypeChecker.for(
+ expr
+ ).annotate(Dhall::TypeChecker::Context.new).type
+ end
+ end
+ end
+
+ def test_variable_in_context
+ context =
+ Dhall::TypeChecker::Context.new
+ .add("x", Dhall::Variable["Type"])
+ .add("x", Dhall::Variable["Kind"])
+
+ assert_equal(
+ Dhall::Variable["Kind"],
+ Dhall::TypeChecker.for(
+ Dhall::Variable["x"]
+ ).annotate(context).type
+ )
+ end
+
+ def test_variable_in_parent_context
+ context =
+ Dhall::TypeChecker::Context.new
+ .add("x", Dhall::Variable["Type"])
+ .add("x", Dhall::Variable["Kind"])
+
+ assert_equal(
+ Dhall::Variable["Type"],
+ Dhall::TypeChecker.for(
+ Dhall::Variable["x", 1]
+ ).annotate(context).type
+ )
+ end
+end
A test/typechecker/failure/IfBranchesNotMatch.dhallb => test/typechecker/failure/IfBranchesNotMatch.dhallb +1 -0
@@ 0,0 1,1 @@
+����`<
\ No newline at end of file
A test/typechecker/failure/IfBranchesNotType.dhallb => test/typechecker/failure/IfBranchesNotType.dhallb +1 -0
@@ 0,0 1,1 @@
+��dTypedType<
\ No newline at end of file
A test/typechecker/failure/IfNotBool.dhallb => test/typechecker/failure/IfNotBool.dhallb +1 -0
@@ 0,0 1,1 @@
+����<
\ No newline at end of file
A test/typechecker/failure/ListLiteralEmptyNoAnnotation.dhallb => test/typechecker/failure/ListLiteralEmptyNoAnnotation.dhallb +1 -0
@@ 0,0 1,1 @@
+��<
\ No newline at end of file
A test/typechecker/failure/ListLiteralEmptyNotType.dhallb => test/typechecker/failure/ListLiteralEmptyNotType.dhallb +1 -0
@@ 0,0 1,1 @@
+�dType<
\ No newline at end of file
A test/typechecker/failure/ListLiteralNotType.dhallb => test/typechecker/failure/ListLiteralNotType.dhallb +1 -0
@@ 0,0 1,1 @@
+��dBool<
\ No newline at end of file
A test/typechecker/failure/ListLiteralTypesNotMatch.dhallb => test/typechecker/failure/ListLiteralTypesNotMatch.dhallb +1 -0
@@ 0,0 1,1 @@
+����<
\ No newline at end of file
A test/typechecker/failure/OperatorAndNotBool.dhallb => test/typechecker/failure/OperatorAndNotBool.dhallb +1 -0
@@ 0,0 1,1 @@
+���<
\ No newline at end of file
A test/typechecker/failure/OperatorEqualNotBool.dhallb => test/typechecker/failure/OperatorEqualNotBool.dhallb +1 -0
@@ 0,0 1,1 @@
+���<
\ No newline at end of file
A test/typechecker/failure/OperatorListConcatenateLhsNotList.dhallb => test/typechecker/failure/OperatorListConcatenateLhsNotList.dhallb +1 -0
@@ 0,0 1,1 @@
+�����<
\ No newline at end of file
A test/typechecker/failure/OperatorListConcatenateListsNotMatch.dhallb => test/typechecker/failure/OperatorListConcatenateListsNotMatch.dhallb +1 -0
@@ 0,0 1,1 @@
+�������<
\ No newline at end of file
A test/typechecker/failure/OperatorListConcatenateRhsNotList.dhallb => test/typechecker/failure/OperatorListConcatenateRhsNotList.dhallb +1 -0
@@ 0,0 1,1 @@
+�����<
\ No newline at end of file
A test/typechecker/failure/OperatorNotEqualNotBool.dhallb => test/typechecker/failure/OperatorNotEqualNotBool.dhallb +1 -0
@@ 0,0 1,1 @@
+���<
\ No newline at end of file
A test/typechecker/failure/OperatorOrNotBool.dhallb => test/typechecker/failure/OperatorOrNotBool.dhallb +0 -0
A test/typechecker/failure/OperatorPlusNotNatural.dhallb => test/typechecker/failure/OperatorPlusNotNatural.dhallb +1 -0
@@ 0,0 1,1 @@
+���<
\ No newline at end of file
A test/typechecker/failure/OperatorTextConcatenateLhsNotText.dhallb => test/typechecker/failure/OperatorTextConcatenateLhsNotText.dhallb +1 -0
@@ 0,0 1,1 @@
+���`<
\ No newline at end of file
A test/typechecker/failure/OperatorTextConcatenateRhsNotText.dhallb => test/typechecker/failure/OperatorTextConcatenateRhsNotText.dhallb +1 -0
@@ 0,0 1,1 @@
+��`�<
\ No newline at end of file
A test/typechecker/failure/OperatorTimesNotNatural.dhallb => test/typechecker/failure/OperatorTimesNotNatural.dhallb +1 -0
@@ 0,0 1,1 @@
+���<
\ No newline at end of file
A test/typechecker/failure/Sort.dhallb => test/typechecker/failure/Sort.dhallb +1 -0
@@ 0,0 1,1 @@
+dSort<
\ No newline at end of file
A test/typechecker/failure/TextLiteralInterpolateNotText.dhallb => test/typechecker/failure/TextLiteralInterpolateNotText.dhallb +1 -0
@@ 0,0 1,1 @@
+�`�`<
\ No newline at end of file
A test/typechecker/failure/VariableFree.dhallb => test/typechecker/failure/VariableFree.dhallb +1 -0
@@ 0,0 1,1 @@
+ax<
\ No newline at end of file
A test/typechecker/success/BoolA.dhallb => test/typechecker/success/BoolA.dhallb +1 -0
@@ 0,0 1,1 @@
+dBool<
\ No newline at end of file
A test/typechecker/success/BoolB.dhallb => test/typechecker/success/BoolB.dhallb +1 -0
@@ 0,0 1,1 @@
+dType<
\ No newline at end of file
A test/typechecker/success/FalseA.dhallb => test/typechecker/success/FalseA.dhallb +1 -0
@@ 0,0 1,1 @@
+�<
\ No newline at end of file
A test/typechecker/success/FalseB.dhallb => test/typechecker/success/FalseB.dhallb +1 -0
@@ 0,0 1,1 @@
+dBool<
\ No newline at end of file
A test/typechecker/success/IfA.dhallb => test/typechecker/success/IfA.dhallb +1 -0
@@ 0,0 1,1 @@
+����<
\ No newline at end of file
A test/typechecker/success/IfB.dhallb => test/typechecker/success/IfB.dhallb +1 -0
@@ 0,0 1,1 @@
+dBool<
\ No newline at end of file
A test/typechecker/success/IfNormalizeArgumentsA.dhallb => test/typechecker/success/IfNormalizeArgumentsA.dhallb +1 -0
@@ 0,0 1,1 @@
+�������������<
\ No newline at end of file
A test/typechecker/success/IfNormalizeArgumentsB.dhallb => test/typechecker/success/IfNormalizeArgumentsB.dhallb +1 -0
@@ 0,0 1,1 @@
+dBool<
\ No newline at end of file
A test/typechecker/success/KindA.dhallb => test/typechecker/success/KindA.dhallb +1 -0
@@ 0,0 1,1 @@
+dKind<
\ No newline at end of file
A test/typechecker/success/KindB.dhallb => test/typechecker/success/KindB.dhallb +1 -0
@@ 0,0 1,1 @@
+dSort<
\ No newline at end of file
A test/typechecker/success/ListA.dhallb => test/typechecker/success/ListA.dhallb +1 -0
@@ 0,0 1,1 @@
+dList<
\ No newline at end of file
A test/typechecker/success/ListB.dhallb => test/typechecker/success/ListB.dhallb +1 -0
@@ 0,0 1,1 @@
+�dTypedType<
\ No newline at end of file
A test/typechecker/success/ListBuildA.dhallb => test/typechecker/success/ListBuildA.dhallb +1 -0
@@ 0,0 1,1 @@
+jList/build<
\ No newline at end of file
A test/typechecker/success/ListBuildB.dhallb => test/typechecker/success/ListBuildB.dhallb +0 -0
A test/typechecker/success/ListFoldA.dhallb => test/typechecker/success/ListFoldA.dhallb +1 -0
@@ 0,0 1,1 @@
+iList/fold<
\ No newline at end of file
A test/typechecker/success/ListFoldB.dhallb => test/typechecker/success/ListFoldB.dhallb +0 -0
A test/typechecker/success/ListHeadA.dhallb => test/typechecker/success/ListHeadA.dhallb +1 -0
@@ 0,0 1,1 @@
+iList/head<
\ No newline at end of file
A test/typechecker/success/ListHeadB.dhallb => test/typechecker/success/ListHeadB.dhallb +0 -0
A test/typechecker/success/ListIndexedA.dhallb => test/typechecker/success/ListIndexedA.dhallb +1 -0
@@ 0,0 1,1 @@
+lList/indexed<
\ No newline at end of file
A test/typechecker/success/ListIndexedB.dhallb => test/typechecker/success/ListIndexedB.dhallb +0 -0
A test/typechecker/success/ListLastA.dhallb => test/typechecker/success/ListLastA.dhallb +1 -0
@@ 0,0 1,1 @@
+iList/last<
\ No newline at end of file
A test/typechecker/success/ListLastB.dhallb => test/typechecker/success/ListLastB.dhallb +0 -0
A test/typechecker/success/ListLengthA.dhallb => test/typechecker/success/ListLengthA.dhallb +1 -0
@@ 0,0 1,1 @@
+kList/length<
\ No newline at end of file
A test/typechecker/success/ListLengthB.dhallb => test/typechecker/success/ListLengthB.dhallb +0 -0
A test/typechecker/success/ListLiteralEmptyA.dhallb => test/typechecker/success/ListLiteralEmptyA.dhallb +1 -0
@@ 0,0 1,1 @@
+�dBool<
\ No newline at end of file
A test/typechecker/success/ListLiteralEmptyB.dhallb => test/typechecker/success/ListLiteralEmptyB.dhallb +0 -0
A test/typechecker/success/ListLiteralNormalizeArgumentsA.dhallb => test/typechecker/success/ListLiteralNormalizeArgumentsA.dhallb +1 -0
@@ 0,0 1,1 @@
+������<
\ No newline at end of file
A test/typechecker/success/ListLiteralNormalizeArgumentsB.dhallb => test/typechecker/success/ListLiteralNormalizeArgumentsB.dhallb +0 -0
A test/typechecker/success/ListLiteralOneA.dhallb => test/typechecker/success/ListLiteralOneA.dhallb +1 -0
@@ 0,0 1,1 @@
+���<
\ No newline at end of file
A test/typechecker/success/ListLiteralOneB.dhallb => test/typechecker/success/ListLiteralOneB.dhallb +0 -0
A test/typechecker/success/ListReverseA.dhallb => test/typechecker/success/ListReverseA.dhallb +1 -0
@@ 0,0 1,1 @@
+lList/reverse<
\ No newline at end of file
A test/typechecker/success/ListReverseB.dhallb => test/typechecker/success/ListReverseB.dhallb +0 -0
A test/typechecker/success/NaturalA.dhallb => test/typechecker/success/NaturalA.dhallb +1 -0
@@ 0,0 1,1 @@
+gNatural<
\ No newline at end of file
A test/typechecker/success/NaturalB.dhallb => test/typechecker/success/NaturalB.dhallb +1 -0
@@ 0,0 1,1 @@
+dType<
\ No newline at end of file
A test/typechecker/success/NaturalBuildA.dhallb => test/typechecker/success/NaturalBuildA.dhallb +1 -0
@@ 0,0 1,1 @@
+mNatural/build<
\ No newline at end of file
A test/typechecker/success/NaturalBuildB.dhallb => test/typechecker/success/NaturalBuildB.dhallb +1 -0
@@ 0,0 1,1 @@
+��gnaturaldType�dsucc�gnaturalgnatural�dzerognaturalgnaturalgNatural<
\ No newline at end of file
A test/typechecker/success/NaturalEvenA.dhallb => test/typechecker/success/NaturalEvenA.dhallb +1 -0
@@ 0,0 1,1 @@
+lNatural/even<
\ No newline at end of file
A test/typechecker/success/NaturalEvenB.dhallb => test/typechecker/success/NaturalEvenB.dhallb +1 -0
@@ 0,0 1,1 @@
+�gNaturaldBool<
\ No newline at end of file
A test/typechecker/success/NaturalFoldA.dhallb => test/typechecker/success/NaturalFoldA.dhallb +1 -0
@@ 0,0 1,1 @@
+lNatural/fold<
\ No newline at end of file
A test/typechecker/success/NaturalFoldB.dhallb => test/typechecker/success/NaturalFoldB.dhallb +1 -0
@@ 0,0 1,1 @@
+�gNatural�gnaturaldType�dsucc�gnaturalgnatural�dzerognaturalgnatural<
\ No newline at end of file
A test/typechecker/success/NaturalIsZeroA.dhallb => test/typechecker/success/NaturalIsZeroA.dhallb +1 -0
@@ 0,0 1,1 @@
+nNatural/isZero<
\ No newline at end of file
A test/typechecker/success/NaturalIsZeroB.dhallb => test/typechecker/success/NaturalIsZeroB.dhallb +1 -0
@@ 0,0 1,1 @@
+�gNaturaldBool<
\ No newline at end of file
A test/typechecker/success/NaturalLiteralA.dhallb => test/typechecker/success/NaturalLiteralA.dhallb +1 -0
@@ 0,0 1,1 @@
+�<
\ No newline at end of file
A test/typechecker/success/NaturalLiteralB.dhallb => test/typechecker/success/NaturalLiteralB.dhallb +1 -0
@@ 0,0 1,1 @@
+gNatural<
\ No newline at end of file
A test/typechecker/success/NaturalOddA.dhallb => test/typechecker/success/NaturalOddA.dhallb +1 -0
@@ 0,0 1,1 @@
+kNatural/odd<
\ No newline at end of file
A test/typechecker/success/NaturalOddB.dhallb => test/typechecker/success/NaturalOddB.dhallb +1 -0
@@ 0,0 1,1 @@
+�gNaturaldBool<
\ No newline at end of file
A test/typechecker/success/NaturalShowA.dhallb => test/typechecker/success/NaturalShowA.dhallb +1 -0
@@ 0,0 1,1 @@
+lNatural/show<
\ No newline at end of file
A test/typechecker/success/NaturalShowB.dhallb => test/typechecker/success/NaturalShowB.dhallb +1 -0
@@ 0,0 1,1 @@
+�gNaturaldText<
\ No newline at end of file
A test/typechecker/success/NaturalToIntegerA.dhallb => test/typechecker/success/NaturalToIntegerA.dhallb +1 -0
@@ 0,0 1,1 @@
+qNatural/toInteger<
\ No newline at end of file
A test/typechecker/success/NaturalToIntegerB.dhallb => test/typechecker/success/NaturalToIntegerB.dhallb +1 -0
@@ 0,0 1,1 @@
+�gNaturalgInteger<
\ No newline at end of file
A test/typechecker/success/OperatorAndA.dhallb => test/typechecker/success/OperatorAndA.dhallb +1 -0
@@ 0,0 1,1 @@
+���<
\ No newline at end of file
A test/typechecker/success/OperatorAndB.dhallb => test/typechecker/success/OperatorAndB.dhallb +1 -0
@@ 0,0 1,1 @@
+dBool<
\ No newline at end of file
A test/typechecker/success/OperatorAndNormalizeArgumentsA.dhallb => test/typechecker/success/OperatorAndNormalizeArgumentsA.dhallb +1 -0
@@ 0,0 1,1 @@
+�����<
\ No newline at end of file
A test/typechecker/success/OperatorAndNormalizeArgumentsB.dhallb => test/typechecker/success/OperatorAndNormalizeArgumentsB.dhallb +1 -0
@@ 0,0 1,1 @@
+dBool<
\ No newline at end of file
A test/typechecker/success/OperatorEqualA.dhallb => test/typechecker/success/OperatorEqualA.dhallb +1 -0
@@ 0,0 1,1 @@
+���<
\ No newline at end of file
A test/typechecker/success/OperatorEqualB.dhallb => test/typechecker/success/OperatorEqualB.dhallb +1 -0
@@ 0,0 1,1 @@
+dBool<
\ No newline at end of file
A test/typechecker/success/OperatorEqualNormalizeArgumentsA.dhallb => test/typechecker/success/OperatorEqualNormalizeArgumentsA.dhallb +1 -0
@@ 0,0 1,1 @@
+�����<
\ No newline at end of file
A test/typechecker/success/OperatorEqualNormalizeArgumentsB.dhallb => test/typechecker/success/OperatorEqualNormalizeArgumentsB.dhallb +1 -0
@@ 0,0 1,1 @@
+dBool<
\ No newline at end of file
A test/typechecker/success/OperatorListConcatenateA.dhallb => test/typechecker/success/OperatorListConcatenateA.dhallb +1 -0
@@ 0,0 1,1 @@
+�������<
\ No newline at end of file
A test/typechecker/success/OperatorListConcatenateB.dhallb => test/typechecker/success/OperatorListConcatenateB.dhallb +0 -0
A test/typechecker/success/OperatorListConcatenateNormalizeArgumentsA.dhallb => test/typechecker/success/OperatorListConcatenateNormalizeArgumentsA.dhallb +1 -0
@@ 0,0 1,1 @@
+����������������<
\ No newline at end of file
A test/typechecker/success/OperatorListConcatenateNormalizeArgumentsB.dhallb => test/typechecker/success/OperatorListConcatenateNormalizeArgumentsB.dhallb +0 -0
A test/typechecker/success/OperatorNotEqualA.dhallb => test/typechecker/success/OperatorNotEqualA.dhallb +1 -0
@@ 0,0 1,1 @@
+���<
\ No newline at end of file
A test/typechecker/success/OperatorNotEqualB.dhallb => test/typechecker/success/OperatorNotEqualB.dhallb +1 -0
@@ 0,0 1,1 @@
+dBool<
\ No newline at end of file
A test/typechecker/success/OperatorNotEqualNormalizeArgumentsA.dhallb => test/typechecker/success/OperatorNotEqualNormalizeArgumentsA.dhallb +1 -0
@@ 0,0 1,1 @@
+�����<
\ No newline at end of file
A test/typechecker/success/OperatorNotEqualNormalizeArgumentsB.dhallb => test/typechecker/success/OperatorNotEqualNormalizeArgumentsB.dhallb +1 -0
@@ 0,0 1,1 @@
+dBool<
\ No newline at end of file
A test/typechecker/success/OperatorOrA.dhallb => test/typechecker/success/OperatorOrA.dhallb +0 -0
A test/typechecker/success/OperatorOrB.dhallb => test/typechecker/success/OperatorOrB.dhallb +1 -0
@@ 0,0 1,1 @@
+dBool<
\ No newline at end of file
A test/typechecker/success/OperatorOrNormalizeArgumentsA.dhallb => test/typechecker/success/OperatorOrNormalizeArgumentsA.dhallb +0 -0
A test/typechecker/success/OperatorOrNormalizeArgumentsB.dhallb => test/typechecker/success/OperatorOrNormalizeArgumentsB.dhallb +1 -0
@@ 0,0 1,1 @@
+dBool<
\ No newline at end of file
A test/typechecker/success/OperatorPlusA.dhallb => test/typechecker/success/OperatorPlusA.dhallb +1 -0
@@ 0,0 1,1 @@
+���<
\ No newline at end of file
A test/typechecker/success/OperatorPlusB.dhallb => test/typechecker/success/OperatorPlusB.dhallb +1 -0
@@ 0,0 1,1 @@
+gNatural<
\ No newline at end of file
A test/typechecker/success/OperatorPlusNormalizeArgumentsA.dhallb => test/typechecker/success/OperatorPlusNormalizeArgumentsA.dhallb +1 -0
@@ 0,0 1,1 @@
+�������<
\ No newline at end of file
A test/typechecker/success/OperatorPlusNormalizeArgumentsB.dhallb => test/typechecker/success/OperatorPlusNormalizeArgumentsB.dhallb +1 -0
@@ 0,0 1,1 @@
+gNatural<
\ No newline at end of file
A test/typechecker/success/OperatorTextConcatenateA.dhallb => test/typechecker/success/OperatorTextConcatenateA.dhallb +1 -0
@@ 0,0 1,1 @@
+��aa�ab<
\ No newline at end of file
A test/typechecker/success/OperatorTextConcatenateB.dhallb => test/typechecker/success/OperatorTextConcatenateB.dhallb +1 -0
@@ 0,0 1,1 @@
+dText<
\ No newline at end of file
A test/typechecker/success/OperatorTextConcatenateNormalizeArgumentsA.dhallb => test/typechecker/success/OperatorTextConcatenateNormalizeArgumentsA.dhallb +1 -0
@@ 0,0 1,1 @@
+���ax�aa��ay�ab<
\ No newline at end of file
A test/typechecker/success/OperatorTextConcatenateNormalizeArgumentsB.dhallb => test/typechecker/success/OperatorTextConcatenateNormalizeArgumentsB.dhallb +1 -0
@@ 0,0 1,1 @@
+dText<
\ No newline at end of file
A test/typechecker/success/OperatorTimesA.dhallb => test/typechecker/success/OperatorTimesA.dhallb +1 -0
@@ 0,0 1,1 @@
+���<
\ No newline at end of file
A test/typechecker/success/OperatorTimesB.dhallb => test/typechecker/success/OperatorTimesB.dhallb +1 -0
@@ 0,0 1,1 @@
+gNatural<
\ No newline at end of file
A test/typechecker/success/OperatorTimesNormalizeArgumentsA.dhallb => test/typechecker/success/OperatorTimesNormalizeArgumentsA.dhallb +1 -0
@@ 0,0 1,1 @@
+�������<
\ No newline at end of file
A test/typechecker/success/OperatorTimesNormalizeArgumentsB.dhallb => test/typechecker/success/OperatorTimesNormalizeArgumentsB.dhallb +1 -0
@@ 0,0 1,1 @@
+gNatural<
\ No newline at end of file
A test/typechecker/success/TextA.dhallb => test/typechecker/success/TextA.dhallb +1 -0
@@ 0,0 1,1 @@
+dText<
\ No newline at end of file
A test/typechecker/success/TextB.dhallb => test/typechecker/success/TextB.dhallb +1 -0
@@ 0,0 1,1 @@
+dType<
\ No newline at end of file
A test/typechecker/success/TextLiteralA.dhallb => test/typechecker/success/TextLiteralA.dhallb +1 -0
@@ 0,0 1,1 @@
+�aa<
\ No newline at end of file
A test/typechecker/success/TextLiteralB.dhallb => test/typechecker/success/TextLiteralB.dhallb +1 -0
@@ 0,0 1,1 @@
+dText<
\ No newline at end of file
A test/typechecker/success/TextLiteralNormalizeArgumentsA.dhallb => test/typechecker/success/TextLiteralNormalizeArgumentsA.dhallb +1 -0
@@ 0,0 1,1 @@
+�aa���aa�ab`<
\ No newline at end of file
A test/typechecker/success/TextLiteralNormalizeArgumentsB.dhallb => test/typechecker/success/TextLiteralNormalizeArgumentsB.dhallb +1 -0
@@ 0,0 1,1 @@
+dText<
\ No newline at end of file
A test/typechecker/success/TextLiteralWithInterpolationA.dhallb => test/typechecker/success/TextLiteralWithInterpolationA.dhallb +1 -0
@@ 0,0 1,1 @@
+�aa�ab`<
\ No newline at end of file
A test/typechecker/success/TextLiteralWithInterpolationB.dhallb => test/typechecker/success/TextLiteralWithInterpolationB.dhallb +1 -0
@@ 0,0 1,1 @@
+dText<
\ No newline at end of file
A test/typechecker/success/TextShowA.dhallb => test/typechecker/success/TextShowA.dhallb +1 -0
@@ 0,0 1,1 @@
+iText/show<
\ No newline at end of file
A test/typechecker/success/TextShowB.dhallb => test/typechecker/success/TextShowB.dhallb +1 -0
@@ 0,0 1,1 @@
+�dTextdText<
\ No newline at end of file
A test/typechecker/success/TrueA.dhallb => test/typechecker/success/TrueA.dhallb +1 -0
@@ 0,0 1,1 @@
+�<
\ No newline at end of file
A test/typechecker/success/TrueB.dhallb => test/typechecker/success/TrueB.dhallb +1 -0
@@ 0,0 1,1 @@
+dBool<
\ No newline at end of file
A test/typechecker/success/TypeA.dhallb => test/typechecker/success/TypeA.dhallb +1 -0
@@ 0,0 1,1 @@
+dType<
\ No newline at end of file
A test/typechecker/success/TypeB.dhallb => test/typechecker/success/TypeB.dhallb +1 -0
@@ 0,0 1,1 @@
+dKind<
\ No newline at end of file