diff options
author | Nadrieril | 2021-01-22 19:02:06 +0000 |
---|---|---|
committer | Nadrieril | 2021-01-22 19:02:06 +0000 |
commit | 6fd075204e0869a72b0b8f86985ec30f2dcd4a13 (patch) | |
tree | 30e5b5494380a3f67b4b9acb3d60de8d982589cc /dhall | |
parent | f231bc273c8aac49c32a8cf36535b830b79f6e20 (diff) |
test: try using the `dhall` crate as a user
Diffstat (limited to '')
-rw-r--r-- | dhall/tests/misc.rs | 38 |
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(); +} |