diff options
author | Nadrieril | 2020-01-28 21:50:04 +0000 |
---|---|---|
committer | Nadrieril | 2020-01-28 21:50:04 +0000 |
commit | 7683b0d762cf0df489ad4bc006e8db2358e81cf4 (patch) | |
tree | 4131494c3b218f9386c7f3633e3d901cf8f631e9 /dhall/src/semantics/phase | |
parent | 084e81956e99bc759012be7c171f4095c2e59d22 (diff) |
Implement assert & merge and fix more bugs
Diffstat (limited to '')
-rw-r--r-- | dhall/src/semantics/phase/normalize.rs | 20 |
1 files changed, 17 insertions, 3 deletions
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index a11cb75..532dae3 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -855,17 +855,30 @@ pub(crate) enum NzEnvItem { #[derive(Debug, Clone)] pub(crate) struct NzEnv { items: Vec<NzEnvItem>, + vars: QuoteEnv, } impl NzEnv { pub fn new() -> Self { - NzEnv { items: Vec::new() } + NzEnv { + items: Vec::new(), + vars: QuoteEnv::new(), + } } pub fn construct(items: Vec<NzEnvItem>) -> Self { - NzEnv { items } + let vars = QuoteEnv::construct( + items + .iter() + .filter(|i| match i { + NzEnvItem::Kept(_) => true, + NzEnvItem::Replaced(_) => false, + }) + .count(), + ); + NzEnv { items, vars } } pub fn as_quoteenv(&self) -> QuoteEnv { - QuoteEnv::construct(self.items.len()) + self.vars } pub fn to_alpha_tyenv(&self) -> TyEnv { TyEnv::from_nzenv_alpha(self) @@ -874,6 +887,7 @@ impl NzEnv { pub fn insert_type(&self, t: Value) -> Self { let mut env = self.clone(); env.items.push(NzEnvItem::Kept(t)); + env.vars = env.vars.insert(); env } pub fn insert_value(&self, e: Value) -> Self { |