From 489174a426e6057a68b6edd2e9b4387d09912a25 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 29 Jan 2020 21:56:52 +0000
Subject: Move envs to their own files

---
 dhall/src/semantics/nze/env.rs | 87 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 87 insertions(+)
 create mode 100644 dhall/src/semantics/nze/env.rs

(limited to 'dhall/src/semantics/nze/env.rs')

diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
new file mode 100644
index 0000000..203d99a
--- /dev/null
+++ b/dhall/src/semantics/nze/env.rs
@@ -0,0 +1,87 @@
+use crate::semantics::{AlphaVar, TyEnv, Value, ValueKind};
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub(crate) enum NzVar {
+    /// Reverse-debruijn index: counts number of binders from the bottom of the stack.
+    Bound(usize),
+    /// Fake fresh variable generated for expression equality checking.
+    Fresh(usize),
+}
+
+#[derive(Debug, Clone)]
+pub(crate) enum NzEnvItem {
+    // Variable is bound with given type
+    Kept(Value),
+    // Variable has been replaced by corresponding value
+    Replaced(Value),
+}
+
+#[derive(Debug, Clone)]
+pub(crate) struct NzEnv {
+    items: Vec<NzEnvItem>,
+}
+
+impl NzVar {
+    pub fn new(idx: usize) -> Self {
+        NzVar::Bound(idx)
+    }
+    pub fn fresh() -> Self {
+        use std::sync::atomic::{AtomicUsize, Ordering};
+        // Global counter to ensure uniqueness of the generated id.
+        static FRESH_VAR_COUNTER: AtomicUsize = AtomicUsize::new(0);
+        let id = FRESH_VAR_COUNTER.fetch_add(1, Ordering::SeqCst);
+        NzVar::Fresh(id)
+    }
+    /// Get index of bound variable.
+    /// Panics on a fresh variable.
+    pub fn idx(&self) -> usize {
+        match self {
+            NzVar::Bound(i) => *i,
+            NzVar::Fresh(_) => panic!(
+                "Trying to use a fresh variable outside of equality checking"
+            ),
+        }
+    }
+}
+
+impl NzEnv {
+    pub fn new() -> Self {
+        NzEnv { items: Vec::new() }
+    }
+    pub fn to_alpha_tyenv(&self) -> TyEnv {
+        TyEnv::from_nzenv_alpha(self)
+    }
+
+    pub fn insert_type(&self, t: Value) -> Self {
+        let mut env = self.clone();
+        env.items.push(NzEnvItem::Kept(t));
+        env
+    }
+    pub fn insert_value(&self, e: Value) -> Self {
+        let mut env = self.clone();
+        env.items.push(NzEnvItem::Replaced(e));
+        env
+    }
+    pub fn lookup_val(&self, var: &AlphaVar) -> Value {
+        let idx = self.items.len() - 1 - var.idx();
+        match &self.items[idx] {
+            NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf(
+                ValueKind::Var(var.clone(), NzVar::new(idx)),
+                ty.clone(),
+            ),
+            NzEnvItem::Replaced(x) => x.clone(),
+        }
+    }
+
+    pub fn size(&self) -> usize {
+        self.items.len()
+    }
+}
+
+/// Ignore NzEnv when comparing; useful because we store them in `AppliedBuiltin`.
+impl std::cmp::PartialEq for NzEnv {
+    fn eq(&self, _other: &Self) -> bool {
+        true
+    }
+}
+impl std::cmp::Eq for NzEnv {}
-- 
cgit v1.2.3