From 8264df65c21b5ad508c5faf96c4a1f9d732449cc Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 17 Feb 2020 17:50:22 +0000
Subject: Move hir and resolve into a module

---
 dhall/src/semantics/resolve/hir.rs | 130 +++++++++++++++++++++++++++++++++++++
 1 file changed, 130 insertions(+)
 create mode 100644 dhall/src/semantics/resolve/hir.rs

(limited to 'dhall/src/semantics/resolve/hir.rs')

diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs
new file mode 100644
index 0000000..b5db66f
--- /dev/null
+++ b/dhall/src/semantics/resolve/hir.rs
@@ -0,0 +1,130 @@
+use crate::error::TypeError;
+use crate::semantics::{type_with, NameEnv, NzEnv, TyEnv, TyExpr, Value};
+use crate::syntax::{Expr, ExprKind, Span, V};
+use crate::{NormalizedExpr, ToExprOptions};
+
+/// Stores an alpha-normalized variable.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
+pub struct AlphaVar {
+    idx: usize,
+}
+
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub(crate) enum HirKind {
+    /// A resolved variable (i.e. a DeBruijn index)
+    Var(AlphaVar),
+    // Forbidden ExprKind variants: Var, Import, Completion
+    Expr(ExprKind<Hir>),
+}
+
+// An expression with resolved variables and imports.
+#[derive(Debug, Clone)]
+pub(crate) struct Hir {
+    kind: Box<HirKind>,
+    span: Span,
+}
+
+impl AlphaVar {
+    pub(crate) fn new(idx: usize) -> Self {
+        AlphaVar { idx }
+    }
+    pub(crate) fn idx(&self) -> usize {
+        self.idx
+    }
+}
+
+impl Hir {
+    pub fn new(kind: HirKind, span: Span) -> Self {
+        Hir {
+            kind: Box::new(kind),
+            span,
+        }
+    }
+
+    pub fn kind(&self) -> &HirKind {
+        &*self.kind
+    }
+    pub fn span(&self) -> Span {
+        self.span.clone()
+    }
+
+    /// Converts a HIR expr back to the corresponding AST expression.
+    pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
+        hir_to_expr(self, opts, &mut NameEnv::new())
+    }
+    /// Converts a HIR expr back to the corresponding AST expression.
+    pub fn to_expr_noopts(&self) -> NormalizedExpr {
+        let opts = ToExprOptions {
+            normalize: false,
+            alpha: false,
+        };
+        self.to_expr(opts)
+    }
+    pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
+        let opts = ToExprOptions {
+            normalize: true,
+            alpha: false,
+        };
+        let mut env = env.as_nameenv().clone();
+        hir_to_expr(self, opts, &mut env)
+    }
+
+    /// Typecheck the Hir.
+    pub fn typecheck(&self, env: &TyEnv) -> Result<TyExpr, TypeError> {
+        type_with(env, self, None)
+    }
+
+    /// Eval the Hir. It will actually get evaluated only as needed on demand.
+    pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
+        Value::new_thunk(env.into(), self.clone())
+    }
+}
+
+fn hir_to_expr(
+    hir: &Hir,
+    opts: ToExprOptions,
+    env: &mut NameEnv,
+) -> NormalizedExpr {
+    let kind = match hir.kind() {
+        HirKind::Var(v) if opts.alpha => ExprKind::Var(V("_".into(), v.idx())),
+        HirKind::Var(v) => ExprKind::Var(env.label_var(v)),
+        HirKind::Expr(e) => {
+            let e = e.map_ref_maybe_binder(|l, hir| {
+                if let Some(l) = l {
+                    env.insert_mut(l);
+                }
+                let e = hir_to_expr(hir, opts, env);
+                if let Some(_) = l {
+                    env.remove_mut();
+                }
+                e
+            });
+
+            match e {
+                ExprKind::Lam(_, t, e) if opts.alpha => {
+                    ExprKind::Lam("_".into(), t, e)
+                }
+                ExprKind::Pi(_, t, e) if opts.alpha => {
+                    ExprKind::Pi("_".into(), t, e)
+                }
+                e => e,
+            }
+        }
+    };
+    Expr::new(kind, hir.span())
+}
+
+impl std::cmp::PartialEq for Hir {
+    fn eq(&self, other: &Self) -> bool {
+        self.kind == other.kind
+    }
+}
+impl std::cmp::Eq for Hir {}
+impl std::hash::Hash for Hir {
+    fn hash<H>(&self, state: &mut H)
+    where
+        H: std::hash::Hasher,
+    {
+        self.kind.hash(state)
+    }
+}
-- 
cgit v1.2.3