From e1a30c6f248c0c17c97598290a0d94993dbb0325 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 10 Apr 2019 19:16:11 +0200
Subject: Add SimpleType and SimpeStaticType. Derive the latter

---
 dhall/src/typecheck.rs | 21 ++++++++++++++++++---
 1 file changed, 18 insertions(+), 3 deletions(-)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 998d3ca..f51f1b6 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -42,7 +42,7 @@ impl Normalized {
         &self.0
     }
     #[inline(always)]
-    fn into_expr(self) -> SubExpr<X, X> {
+    pub(crate) fn into_expr(self) -> SubExpr<X, X> {
         self.0
     }
     #[inline(always)]
@@ -50,7 +50,7 @@ impl Normalized {
         &self.1
     }
     #[inline(always)]
-    fn into_type(self) -> Type {
+    pub(crate) fn into_type(self) -> Type {
         crate::expr::Type(TypeInternal::Expr(Box::new(self)))
     }
     // Expose the outermost constructor
@@ -78,7 +78,7 @@ impl Type {
         }
     }
     #[inline(always)]
-    fn into_normalized(self) -> Result<Normalized, TypeError<X>> {
+    pub(crate) fn into_normalized(self) -> Result<Normalized, TypeError<X>> {
         use TypeInternal::*;
         match self.0 {
             Expr(e) => Ok(*e),
@@ -110,6 +110,21 @@ impl Type {
             Untyped => Untyped,
         })
     }
+
+    #[inline(always)]
+    pub fn const_sort() -> Self {
+        Normalized(rc(ExprF::Const(Const::Sort)), UNTYPE).into_type()
+    }
+    #[inline(always)]
+    pub fn const_kind() -> Self {
+        Normalized(rc(ExprF::Const(Const::Kind)), Type::const_sort())
+            .into_type()
+    }
+    #[inline(always)]
+    pub fn const_type() -> Self {
+        Normalized(rc(ExprF::Const(Const::Type)), Type::const_kind())
+            .into_type()
+    }
 }
 
 const UNTYPE: Type = Type(TypeInternal::Untyped);
-- 
cgit v1.2.3


From 7740ec004c6d7e073358bf2be00b6c0006e4dd06 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 10 Apr 2019 22:32:07 +0200
Subject: Allow providing type for typechecking in API

---
 dhall/src/typecheck.rs | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index f51f1b6..9741e65 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -13,6 +13,11 @@ impl Resolved {
     pub fn typecheck(self) -> Result<Typed, TypeError<X>> {
         type_of(self.0.clone())
     }
+    pub fn typecheck_with(self, ty: &Type) -> Result<Typed, TypeError<X>> {
+        let expr: SubExpr<_, _> = self.0.clone();
+        let ty: SubExpr<_, _> = ty.as_normalized()?.as_expr().clone();
+        type_of(dhall::subexpr!(expr: ty))
+    }
     /// Pretends this expression has been typechecked. Use with care.
     pub fn skip_typecheck(self) -> Typed {
         Typed(self.0, UNTYPE)
-- 
cgit v1.2.3


From 9a060908aae564e7155259a4e12d63be3fb97d9b Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 10 Apr 2019 23:58:12 +0200
Subject: Simplify test harness

---
 dhall/src/typecheck.rs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 9741e65..91846bc 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -726,23 +726,23 @@ mod spec_tests {
 
     macro_rules! tc_success {
         ($name:ident, $path:expr) => {
-            make_spec_test!(TypecheckSuccess, $name, $path);
+            make_spec_test!(Typecheck, Success, $name, $path);
         };
     }
     // macro_rules! tc_failure {
     //     ($name:ident, $path:expr) => {
-    //         make_spec_test!(TypecheckFailure, $name, $path);
+    //         make_spec_test!(Typecheck, Failure, $name, $path);
     //     };
     // }
 
     macro_rules! ti_success {
         ($name:ident, $path:expr) => {
-            make_spec_test!(TypeInferenceSuccess, $name, $path);
+            make_spec_test!(TypeInference, Success, $name, $path);
         };
     }
     // macro_rules! ti_failure {
     //     ($name:ident, $path:expr) => {
-    //         make_spec_test!(TypeInferenceFailure, $name, $path);
+    //         make_spec_test!(TypeInference, Failure, $name, $path);
     //     };
     // }
 
-- 
cgit v1.2.3