summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/core/value.rs
diff options
context:
space:
mode:
authorNadrieril2019-12-27 16:05:47 +0000
committerNadrieril2020-01-17 10:06:00 +0000
commit654d752c65f0e221d225ed045a0aee62f223855e (patch)
treeb982c70d01fc32494f0bf1ebcb838ba6cdc8a425 /dhall/src/semantics/core/value.rs
parent8e2da26650e202f9ccb1531fc8a88cfd89e54b6d (diff)
Introduce a notion of binder
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/core/value.rs8
1 files changed, 4 insertions, 4 deletions
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index f7c2fbf..687fcfe 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -4,7 +4,7 @@ use std::rc::Rc;
use crate::error::{TypeError, TypeMessage};
use crate::semantics::core::context::TyCtx;
-use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
+use crate::semantics::core::var::{AlphaVar, Binder, Shift, Subst};
use crate::semantics::phase::normalize::{apply_any, normalize_whnf};
use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value};
use crate::semantics::phase::{Normalized, NormalizedExpr, Typed};
@@ -54,8 +54,8 @@ pub(crate) enum Form {
#[derive(Debug, Clone, PartialEq, Eq)]
pub(crate) enum ValueKind<Value> {
/// Closures
- Lam(AlphaLabel, Value, Value),
- Pi(AlphaLabel, Value, Value),
+ Lam(Binder, Value, Value),
+ Pi(Binder, Value, Value),
// Invariant: in whnf, the evaluation must not be able to progress further.
AppliedBuiltin(Builtin, Vec<Value>),
@@ -393,7 +393,7 @@ impl<V> ValueKind<V> {
pub(crate) fn map_ref_with_special_handling_of_binders<'a, V2>(
&'a self,
mut map_val: impl FnMut(&'a V) -> V2,
- mut map_under_binder: impl FnMut(&'a AlphaLabel, &'a V) -> V2,
+ mut map_under_binder: impl FnMut(&'a Binder, &'a V) -> V2,
) -> ValueKind<V2> {
use crate::semantics::visitor;
use crate::syntax::trivial_result;