From 6fd075204e0869a72b0b8f86985ec30f2dcd4a13 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 22 Jan 2021 19:02:06 +0000
Subject: test: try using the `dhall` crate as a user

---
 dhall/tests/misc.rs | 38 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)
 create mode 100644 dhall/tests/misc.rs

(limited to 'dhall')

diff --git a/dhall/tests/misc.rs b/dhall/tests/misc.rs
new file mode 100644
index 0000000..3eecf03
--- /dev/null
+++ b/dhall/tests/misc.rs
@@ -0,0 +1,38 @@
+use dhall::error::Error;
+use dhall::semantics::*;
+use dhall::syntax::*;
+use dhall::*;
+
+/// Test that showcases someone using the `dhall` crate directly for a simple operation. If
+/// possible try not to break this too much. See
+/// https://github.com/Nadrieril/dhall-rust/issues/208.
+#[test]
+fn manual_function_application() {
+    /// Apply a `Natural -> Natural` function to an argument.
+    fn apply_natnat_fn<'cx>(f: &Nir<'cx>, n: u64) -> u64 {
+        let n_nir = Nir::from_kind(NirKind::Num(NumKind::Natural(n)));
+        match f.app(n_nir).kind() {
+            NirKind::Num(NumKind::Natural(m)) => *m,
+            _ => panic!("`f` was not `Natural -> Natural`"),
+        }
+    }
+    /// Auxiliary function to make `?` work.
+    fn run<'cx>(cx: Ctxt<'cx>) -> Result<(), Error> {
+        let f_ty = "Natural -> Natural";
+        let f = "\\(x: Natural) -> x + 3";
+        let f_ty = Parsed::parse_str(f_ty)?
+            .skip_resolve(cx)?
+            .typecheck(cx)?
+            .normalize(cx);
+        let f = Parsed::parse_str(f)?
+            .skip_resolve(cx)?
+            .typecheck_with(cx, &f_ty.to_hir())?
+            .normalize(cx);
+        for i in 0..5 {
+            let n = apply_natnat_fn(f.as_nir(), i);
+            assert_eq!(n, i + 3);
+        }
+        Ok(())
+    }
+    Ctxt::with_new(run).unwrap();
+}
-- 
cgit v1.2.3