summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/tck
diff options
context:
space:
mode:
authorNadrieril2020-02-17 17:58:03 +0000
committerNadrieril2020-02-17 17:58:03 +0000
commit8da4445e6d06cf79d43112042b69c798f86884f3 (patch)
tree4a17a14f3def06a67c30756d49811b00253843e1 /dhall/src/semantics/tck
parent8264df65c21b5ad508c5faf96c4a1f9d732449cc (diff)
Extract resolve-relevant envs together
Diffstat (limited to 'dhall/src/semantics/tck')
-rw-r--r--dhall/src/semantics/tck/env.rs59
1 files changed, 5 insertions, 54 deletions
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 7990059..f290c02 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -1,5 +1,5 @@
-use crate::semantics::{AlphaVar, NzEnv, NzVar, Type, ValEnv, Value};
-use crate::syntax::{Label, V};
+use crate::semantics::{AlphaVar, NameEnv, NzEnv, NzVar, Type, ValEnv, Value};
+use crate::syntax::Label;
/// Environment for indexing variables.
#[derive(Debug, Clone, Copy)]
@@ -7,12 +7,6 @@ pub(crate) struct VarEnv {
size: usize,
}
-/// Environment for resolving names.
-#[derive(Debug, Clone)]
-pub(crate) struct NameEnv {
- names: Vec<Label>,
-}
-
/// Environment for typing expressions.
#[derive(Debug, Clone)]
pub(crate) struct TyEnv {
@@ -24,6 +18,9 @@ impl VarEnv {
pub fn new() -> Self {
VarEnv { size: 0 }
}
+ pub fn from_size(size: usize) -> Self {
+ VarEnv { size }
+ }
pub fn size(&self) -> usize {
self.size
}
@@ -41,52 +38,6 @@ impl VarEnv {
}
}
-impl NameEnv {
- pub fn new() -> Self {
- NameEnv { names: Vec::new() }
- }
- pub fn as_varenv(&self) -> VarEnv {
- VarEnv {
- size: self.names.len(),
- }
- }
-
- pub fn insert(&self, x: &Label) -> Self {
- let mut env = self.clone();
- env.insert_mut(x);
- env
- }
- pub fn insert_mut(&mut self, x: &Label) {
- self.names.push(x.clone())
- }
- pub fn remove_mut(&mut self) {
- self.names.pop();
- }
-
- pub fn unlabel_var(&self, var: &V) -> Option<AlphaVar> {
- let V(name, idx) = var;
- let (idx, _) = self
- .names
- .iter()
- .rev()
- .enumerate()
- .filter(|(_, n)| *n == name)
- .nth(*idx)?;
- Some(AlphaVar::new(idx))
- }
- pub fn label_var(&self, var: &AlphaVar) -> V {
- let name = &self.names[self.names.len() - 1 - var.idx()];
- let idx = self
- .names
- .iter()
- .rev()
- .take(var.idx())
- .filter(|n| *n == name)
- .count();
- V(name.clone(), idx)
- }
-}
-
impl TyEnv {
pub fn new() -> Self {
TyEnv {