summaryrefslogtreecommitdiff
path: root/dhall/tests
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/tests')
-rw-r--r--dhall/tests/misc.rs38
1 files changed, 38 insertions, 0 deletions
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();
+}