summaryrefslogtreecommitdiff
path: root/dhall/tests
diff options
context:
space:
mode:
authorNadrieril2021-01-22 19:11:23 +0000
committerNadrieril2021-01-22 19:11:23 +0000
commit11ff03a8113580244ced04a8b370ab6192b8e413 (patch)
tree47782b629686974ffa72a79715be9199997e4062 /dhall/tests
parent6fd075204e0869a72b0b8f86985ec30f2dcd4a13 (diff)
doc: document the `dhall` usage test
Diffstat (limited to 'dhall/tests')
-rw-r--r--dhall/tests/misc.rs18
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();
}