summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/typecheck.rs76
1 files changed, 47 insertions, 29 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 78538aa..96c8546 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -374,6 +374,7 @@ fn type_of_builtin<N, E>(b: Builtin) -> Expr<N, E> {
List | Optional => dhall::expr!(
Type -> Type
),
+
NaturalFold => dhall::expr!(
Natural ->
forall (natural: Type) ->
@@ -391,6 +392,14 @@ fn type_of_builtin<N, E>(b: Builtin) -> Expr<N, E> {
NaturalIsZero | NaturalEven | NaturalOdd => dhall::expr!(
Natural -> Bool
),
+ NaturalToInteger => dhall::expr!(Natural -> Integer),
+ NaturalShow => dhall::expr!(Natural -> Text),
+
+ IntegerToDouble => dhall::expr!(Integer -> Double),
+ IntegerShow => dhall::expr!(Integer -> Text),
+ DoubleShow => dhall::expr!(Double -> Text),
+ TextShow => dhall::expr!(Text -> Text),
+
ListBuild => dhall::expr!(
forall (a: Type) ->
(forall (list: Type) ->
@@ -419,6 +428,15 @@ fn type_of_builtin<N, E>(b: Builtin) -> Expr<N, E> {
ListReverse => dhall::expr!(
forall (a: Type) -> List a -> List a
),
+
+ OptionalBuild => dhall::expr!(
+ forall (a: Type) ->
+ (forall (optional: Type) ->
+ forall (just: a -> optional) ->
+ forall (nothing: optional) ->
+ optional) ->
+ Optional a
+ ),
OptionalFold => dhall::expr!(
forall (a: Type) ->
Optional a ->
@@ -427,10 +445,10 @@ fn type_of_builtin<N, E>(b: Builtin) -> Expr<N, E> {
forall (nothing: optional) ->
optional
),
+ // TODO: alpha-equivalence in type-inference tests
OptionalNone => dhall::expr!(
- forall (a: Type) -> Optional a
+ forall (A: Type) -> Optional A
),
- _ => panic!("Unimplemented typecheck case: {:?}", b),
}
}
@@ -1143,12 +1161,12 @@ mod spec_tests {
tc_success!(tc_success_prelude_Bool_or_1, "prelude/Bool/or/1");
tc_success!(tc_success_prelude_Bool_show_0, "prelude/Bool/show/0");
tc_success!(tc_success_prelude_Bool_show_1, "prelude/Bool/show/1");
- // tc_success!(tc_success_prelude_Double_show_0, "prelude/Double/show/0");
- // tc_success!(tc_success_prelude_Double_show_1, "prelude/Double/show/1");
- // tc_success!(tc_success_prelude_Integer_show_0, "prelude/Integer/show/0");
- // tc_success!(tc_success_prelude_Integer_show_1, "prelude/Integer/show/1");
- // tc_success!(tc_success_prelude_Integer_toDouble_0, "prelude/Integer/toDouble/0");
- // tc_success!(tc_success_prelude_Integer_toDouble_1, "prelude/Integer/toDouble/1");
+ tc_success!(tc_success_prelude_Double_show_0, "prelude/Double/show/0");
+ tc_success!(tc_success_prelude_Double_show_1, "prelude/Double/show/1");
+ tc_success!(tc_success_prelude_Integer_show_0, "prelude/Integer/show/0");
+ tc_success!(tc_success_prelude_Integer_show_1, "prelude/Integer/show/1");
+ tc_success!(tc_success_prelude_Integer_toDouble_0, "prelude/Integer/toDouble/0");
+ tc_success!(tc_success_prelude_Integer_toDouble_1, "prelude/Integer/toDouble/1");
tc_success!(tc_success_prelude_List_all_0, "prelude/List/all/0");
tc_success!(tc_success_prelude_List_all_1, "prelude/List/all/1");
tc_success!(tc_success_prelude_List_any_0, "prelude/List/any/0");
@@ -1214,25 +1232,25 @@ mod spec_tests {
tc_success!(tc_success_prelude_Natural_odd_1, "prelude/Natural/odd/1");
tc_success!(tc_success_prelude_Natural_product_0, "prelude/Natural/product/0");
tc_success!(tc_success_prelude_Natural_product_1, "prelude/Natural/product/1");
- // tc_success!(tc_success_prelude_Natural_show_0, "prelude/Natural/show/0");
- // tc_success!(tc_success_prelude_Natural_show_1, "prelude/Natural/show/1");
+ tc_success!(tc_success_prelude_Natural_show_0, "prelude/Natural/show/0");
+ tc_success!(tc_success_prelude_Natural_show_1, "prelude/Natural/show/1");
tc_success!(tc_success_prelude_Natural_sum_0, "prelude/Natural/sum/0");
tc_success!(tc_success_prelude_Natural_sum_1, "prelude/Natural/sum/1");
- // tc_success!(tc_success_prelude_Natural_toDouble_0, "prelude/Natural/toDouble/0");
- // tc_success!(tc_success_prelude_Natural_toDouble_1, "prelude/Natural/toDouble/1");
- // tc_success!(tc_success_prelude_Natural_toInteger_0, "prelude/Natural/toInteger/0");
- // tc_success!(tc_success_prelude_Natural_toInteger_1, "prelude/Natural/toInteger/1");
+ tc_success!(tc_success_prelude_Natural_toDouble_0, "prelude/Natural/toDouble/0");
+ tc_success!(tc_success_prelude_Natural_toDouble_1, "prelude/Natural/toDouble/1");
+ tc_success!(tc_success_prelude_Natural_toInteger_0, "prelude/Natural/toInteger/0");
+ tc_success!(tc_success_prelude_Natural_toInteger_1, "prelude/Natural/toInteger/1");
tc_success!(tc_success_prelude_Optional_all_0, "prelude/Optional/all/0");
tc_success!(tc_success_prelude_Optional_all_1, "prelude/Optional/all/1");
tc_success!(tc_success_prelude_Optional_any_0, "prelude/Optional/any/0");
tc_success!(tc_success_prelude_Optional_any_1, "prelude/Optional/any/1");
- // tc_success!(tc_success_prelude_Optional_build_0, "prelude/Optional/build/0");
- // tc_success!(tc_success_prelude_Optional_build_1, "prelude/Optional/build/1");
+ tc_success!(tc_success_prelude_Optional_build_0, "prelude/Optional/build/0");
+ tc_success!(tc_success_prelude_Optional_build_1, "prelude/Optional/build/1");
tc_success!(tc_success_prelude_Optional_concat_0, "prelude/Optional/concat/0");
tc_success!(tc_success_prelude_Optional_concat_1, "prelude/Optional/concat/1");
tc_success!(tc_success_prelude_Optional_concat_2, "prelude/Optional/concat/2");
- // tc_success!(tc_success_prelude_Optional_filter_0, "prelude/Optional/filter/0");
- // tc_success!(tc_success_prelude_Optional_filter_1, "prelude/Optional/filter/1");
+ tc_success!(tc_success_prelude_Optional_filter_0, "prelude/Optional/filter/0");
+ tc_success!(tc_success_prelude_Optional_filter_1, "prelude/Optional/filter/1");
tc_success!(tc_success_prelude_Optional_fold_0, "prelude/Optional/fold/0");
tc_success!(tc_success_prelude_Optional_fold_1, "prelude/Optional/fold/1");
tc_success!(tc_success_prelude_Optional_head_0, "prelude/Optional/head/0");
@@ -1253,8 +1271,8 @@ mod spec_tests {
tc_success!(tc_success_prelude_Optional_unzip_1, "prelude/Optional/unzip/1");
tc_success!(tc_success_prelude_Text_concat_0, "prelude/Text/concat/0");
tc_success!(tc_success_prelude_Text_concat_1, "prelude/Text/concat/1");
- // tc_success!(tc_success_prelude_Text_concatMap_0, "prelude/Text/concatMap/0");
- // tc_success!(tc_success_prelude_Text_concatMap_1, "prelude/Text/concatMap/1");
+ tc_success!(tc_success_prelude_Text_concatMap_0, "prelude/Text/concatMap/0");
+ tc_success!(tc_success_prelude_Text_concatMap_1, "prelude/Text/concatMap/1");
// tc_success!(tc_success_prelude_Text_concatMapSep_0, "prelude/Text/concatMapSep/0");
// tc_success!(tc_success_prelude_Text_concatMapSep_1, "prelude/Text/concatMapSep/1");
// tc_success!(tc_success_prelude_Text_concatSep_0, "prelude/Text/concatSep/0");
@@ -1355,7 +1373,7 @@ mod spec_tests {
ti_success!(ti_success_unit_Bool, "unit/Bool");
ti_success!(ti_success_unit_Double, "unit/Double");
ti_success!(ti_success_unit_DoubleLiteral, "unit/DoubleLiteral");
- // ti_success!(ti_success_unit_DoubleShow, "unit/DoubleShow");
+ ti_success!(ti_success_unit_DoubleShow, "unit/DoubleShow");
ti_success!(ti_success_unit_False, "unit/False");
ti_success!(ti_success_unit_Function, "unit/Function");
ti_success!(ti_success_unit_FunctionApplication, "unit/FunctionApplication");
@@ -1371,8 +1389,8 @@ mod spec_tests {
ti_success!(ti_success_unit_IfNormalizeArguments, "unit/IfNormalizeArguments");
ti_success!(ti_success_unit_Integer, "unit/Integer");
ti_success!(ti_success_unit_IntegerLiteral, "unit/IntegerLiteral");
- // ti_success!(ti_success_unit_IntegerShow, "unit/IntegerShow");
- // ti_success!(ti_success_unit_IntegerToDouble, "unit/IntegerToDouble");
+ ti_success!(ti_success_unit_IntegerShow, "unit/IntegerShow");
+ ti_success!(ti_success_unit_IntegerToDouble, "unit/IntegerToDouble");
ti_success!(ti_success_unit_Kind, "unit/Kind");
ti_success!(ti_success_unit_Let, "unit/Let");
ti_success!(ti_success_unit_LetNestedTypeSynonym, "unit/LetNestedTypeSynonym");
@@ -1399,11 +1417,11 @@ mod spec_tests {
ti_success!(ti_success_unit_NaturalIsZero, "unit/NaturalIsZero");
ti_success!(ti_success_unit_NaturalLiteral, "unit/NaturalLiteral");
ti_success!(ti_success_unit_NaturalOdd, "unit/NaturalOdd");
- // ti_success!(ti_success_unit_NaturalShow, "unit/NaturalShow");
- // ti_success!(ti_success_unit_NaturalToInteger, "unit/NaturalToInteger");
- // ti_success!(ti_success_unit_None, "unit/None");
+ ti_success!(ti_success_unit_NaturalShow, "unit/NaturalShow");
+ ti_success!(ti_success_unit_NaturalToInteger, "unit/NaturalToInteger");
+ ti_success!(ti_success_unit_None, "unit/None");
ti_success!(ti_success_unit_OldOptionalNone, "unit/OldOptionalNone");
- // ti_success!(ti_success_unit_OldOptionalTrue, "unit/OldOptionalTrue");
+ ti_success!(ti_success_unit_OldOptionalTrue, "unit/OldOptionalTrue");
ti_success!(ti_success_unit_OperatorAnd, "unit/OperatorAnd");
ti_success!(ti_success_unit_OperatorAndNormalizeArguments, "unit/OperatorAndNormalizeArguments");
ti_success!(ti_success_unit_OperatorEqual, "unit/OperatorEqual");
@@ -1421,7 +1439,7 @@ mod spec_tests {
ti_success!(ti_success_unit_OperatorTimes, "unit/OperatorTimes");
ti_success!(ti_success_unit_OperatorTimesNormalizeArguments, "unit/OperatorTimesNormalizeArguments");
ti_success!(ti_success_unit_Optional, "unit/Optional");
- // ti_success!(ti_success_unit_OptionalBuild, "unit/OptionalBuild");
+ ti_success!(ti_success_unit_OptionalBuild, "unit/OptionalBuild");
ti_success!(ti_success_unit_OptionalFold, "unit/OptionalFold");
ti_success!(ti_success_unit_RecordEmpty, "unit/RecordEmpty");
ti_success!(ti_success_unit_RecordOneKind, "unit/RecordOneKind");
@@ -1461,7 +1479,7 @@ mod spec_tests {
ti_success!(ti_success_unit_TextLiteral, "unit/TextLiteral");
ti_success!(ti_success_unit_TextLiteralNormalizeArguments, "unit/TextLiteralNormalizeArguments");
ti_success!(ti_success_unit_TextLiteralWithInterpolation, "unit/TextLiteralWithInterpolation");
- // ti_success!(ti_success_unit_TextShow, "unit/TextShow");
+ ti_success!(ti_success_unit_TextShow, "unit/TextShow");
ti_success!(ti_success_unit_True, "unit/True");
ti_success!(ti_success_unit_Type, "unit/Type");
ti_success!(ti_success_unit_TypeAnnotation, "unit/TypeAnnotation");
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 05:39:05 +0000