1 files changed, 55 insertions, 32 deletions

diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs
index 8869915..8baad10 100644
--- a/dhall/src/semantics/resolve/hir.rs
+++ b/dhall/src/semantics/resolve/hir.rs
@@ -1,7 +1,7 @@
 use crate::error::TypeError;
-use crate::semantics::{type_with, NameEnv, Nir, NzEnv, Tir, TyEnv, Type};
+use crate::semantics::{type_with, typecheck, NameEnv, Nir, NzEnv, Tir, TyEnv};
 use crate::syntax::{Expr, ExprKind, Span, V};
-use crate::ToExprOptions;
+use crate::{Ctxt, ImportAlternativeId, ImportId, ToExprOptions};
 
 /// Stores an alpha-normalized variable.
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
@@ -10,19 +10,23 @@ pub struct AlphaVar {
 }
 
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub enum HirKind {
+pub enum HirKind<'cx> {
     /// A resolved variable (i.e. a DeBruijn index)
     Var(AlphaVar),
-    /// Result of resolving an import.
-    Import(Hir, Type),
+    /// A variable that couldn't be resolved. Detected during resolution, but causes an error during typeck.
+    MissingVar(V),
+    /// An import. It must have been resolved after resolution.
+    Import(ImportId<'cx>),
+    /// An import alternative. It must have been decided after resolution.
+    ImportAlternative(ImportAlternativeId<'cx>, Hir<'cx>, Hir<'cx>),
     // Forbidden ExprKind variants: Var, Import, Completion
-    Expr(ExprKind<Hir>),
+    Expr(ExprKind<Hir<'cx>>),
 }
 
 // An expression with resolved variables and imports.
 #[derive(Debug, Clone)]
-pub struct Hir {
-    kind: Box<HirKind>,
+pub struct Hir<'cx> {
+    kind: Box<HirKind<'cx>>,
     span: Span,
 }
 
@@ -35,15 +39,15 @@ impl AlphaVar {
     }
 }
 
-impl Hir {
-    pub fn new(kind: HirKind, span: Span) -> Self {
+impl<'cx> Hir<'cx> {
+    pub fn new(kind: HirKind<'cx>, span: Span) -> Self {
         Hir {
             kind: Box::new(kind),
             span,
         }
     }
 
-    pub fn kind(&self) -> &HirKind {
+    pub fn kind(&self) -> &HirKind<'cx> {
         &*self.kind
     }
     pub fn span(&self) -> Span {
@@ -51,59 +55,78 @@ impl Hir {
     }
 
     /// Converts a closed Hir expr back to the corresponding AST expression.
-    pub fn to_expr(&self, opts: ToExprOptions) -> Expr {
-        hir_to_expr(self, opts, &mut NameEnv::new())
+    pub fn to_expr(&self, cx: Ctxt<'cx>, opts: ToExprOptions) -> Expr {
+        hir_to_expr(cx, self, opts, &mut NameEnv::new())
     }
     /// Converts a closed Hir expr back to the corresponding AST expression.
-    pub fn to_expr_noopts(&self) -> Expr {
+    pub fn to_expr_noopts(&self, cx: Ctxt<'cx>) -> Expr {
         let opts = ToExprOptions { alpha: false };
-        self.to_expr(opts)
+        self.to_expr(cx, opts)
     }
-    pub fn to_expr_alpha(&self) -> Expr {
+    pub fn to_expr_alpha(&self, cx: Ctxt<'cx>) -> Expr {
         let opts = ToExprOptions { alpha: true };
-        self.to_expr(opts)
+        self.to_expr(cx, opts)
     }
-    pub fn to_expr_tyenv(&self, env: &TyEnv) -> Expr {
+    pub fn to_expr_tyenv(&self, env: &TyEnv<'cx>) -> Expr {
         let opts = ToExprOptions { alpha: false };
+        let cx = env.cx();
         let mut env = env.as_nameenv().clone();
-        hir_to_expr(self, opts, &mut env)
+        hir_to_expr(cx, self, opts, &mut env)
     }
 
     /// Typecheck the Hir.
     pub fn typecheck<'hir>(
         &'hir self,
-        env: &TyEnv,
-    ) -> Result<Tir<'hir>, TypeError> {
+        env: &TyEnv<'cx>,
+    ) -> Result<Tir<'cx, 'hir>, TypeError> {
         type_with(env, self, None)
     }
-    pub fn typecheck_noenv<'hir>(&'hir self) -> Result<Tir<'hir>, TypeError> {
-        self.typecheck(&TyEnv::new())
+    pub fn typecheck_noenv<'hir>(
+        &'hir self,
+        cx: Ctxt<'cx>,
+    ) -> Result<Tir<'cx, 'hir>, TypeError> {
+        typecheck(cx, self)
     }
 
     /// Eval the Hir. It will actually get evaluated only as needed on demand.
-    pub fn eval(&self, env: impl Into<NzEnv>) -> Nir {
+    pub fn eval(&self, env: impl Into<NzEnv<'cx>>) -> Nir<'cx> {
         Nir::new_thunk(env.into(), self.clone())
     }
     /// Eval a closed Hir (i.e. without free variables). It will actually get evaluated only as
     /// needed on demand.
-    pub fn eval_closed_expr(&self) -> Nir {
-        self.eval(NzEnv::new())
+    pub fn eval_closed_expr(&self, cx: Ctxt<'cx>) -> Nir<'cx> {
+        self.eval(NzEnv::new(cx))
     }
 }
 
-fn hir_to_expr(hir: &Hir, opts: ToExprOptions, env: &mut NameEnv) -> Expr {
+fn hir_to_expr<'cx>(
+    cx: Ctxt<'cx>,
+    hir: &Hir<'cx>,
+    opts: ToExprOptions,
+    env: &mut NameEnv,
+) -> Expr {
     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::Import(hir, _) => {
-            return hir_to_expr(hir, opts, &mut NameEnv::new())
+        HirKind::MissingVar(v) => ExprKind::Var(v.clone()),
+        HirKind::Import(import) => {
+            let typed = cx[import].unwrap_result();
+            return hir_to_expr(cx, &typed.hir, opts, &mut NameEnv::new());
+        }
+        HirKind::ImportAlternative(alt, left, right) => {
+            let hir = if cx[alt].unwrap_selected() {
+                left
+            } else {
+                right
+            };
+            return hir_to_expr(cx, hir, opts, env);
         }
         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);
+                let e = hir_to_expr(cx, hir, opts, env);
                 if l.is_some() {
                     env.remove_mut();
                 }
@@ -124,9 +147,9 @@ fn hir_to_expr(hir: &Hir, opts: ToExprOptions, env: &mut NameEnv) -> Expr {
     Expr::new(kind, hir.span())
 }
 
-impl std::cmp::PartialEq for Hir {
+impl<'cx> std::cmp::PartialEq for Hir<'cx> {
     fn eq(&self, other: &Self) -> bool {
         self.kind == other.kind
     }
 }
-impl std::cmp::Eq for Hir {}
+impl<'cx> std::cmp::Eq for Hir<'cx> {}