diff options
author | Nadrieril | 2021-01-22 19:11:23 +0000 |
---|---|---|
committer | Nadrieril | 2021-01-22 19:11:23 +0000 |
commit | 11ff03a8113580244ced04a8b370ab6192b8e413 (patch) | |
tree | 47782b629686974ffa72a79715be9199997e4062 /dhall/tests | |
parent | 6fd075204e0869a72b0b8f86985ec30f2dcd4a13 (diff) |
doc: document the `dhall` usage test
Diffstat (limited to '')
-rw-r--r-- | dhall/tests/misc.rs | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/dhall/tests/misc.rs b/dhall/tests/misc.rs index 3eecf03..4d80f53 100644 --- a/dhall/tests/misc.rs +++ b/dhall/tests/misc.rs @@ -10,29 +10,41 @@ use dhall::*; fn manual_function_application() { /// Apply a `Natural -> Natural` function to an argument. fn apply_natnat_fn<'cx>(f: &Nir<'cx>, n: u64) -> u64 { + // Convert the number to the internal representation. let n_nir = Nir::from_kind(NirKind::Num(NumKind::Natural(n))); - match f.app(n_nir).kind() { + // Apply `f` to `n`. + let m_nir = f.app(n_nir); + // Convert from the internal representation. + match m_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> { + fn run(cx: Ctxt<'_>) -> Result<(), Error> { + // Parse the type we want into the internal representation. 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); + + // Parse the function `f` itself, and also check its type. + let f = "\\(x: Natural) -> x + 3"; let f = Parsed::parse_str(f)? .skip_resolve(cx)? .typecheck_with(cx, &f_ty.to_hir())? .normalize(cx); + + // Do whatever we want with `f`. for i in 0..5 { let n = apply_natnat_fn(f.as_nir(), i); assert_eq!(n, i + 3); } Ok(()) } + + // The crate uses essentially a global context, created here. Ctxt::with_new(run).unwrap(); } |