Merge pull request #204 from Nadrieril/source-id

3 files changed, 107 insertions, 68 deletions

diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 1fa66f0..fdcc62d 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -1,5 +1,6 @@
 use crate::semantics::{AlphaVar, NameEnv, Nir, NzEnv, NzVar, Type, ValEnv};
 use crate::syntax::Label;
+use crate::Ctxt;
 
 /// Environment for indexing variables.
 #[derive(Debug, Clone, Copy, Default)]
@@ -9,9 +10,10 @@ pub struct VarEnv {
 
 /// Environment for typing expressions.
 #[derive(Debug, Clone)]
-pub struct TyEnv {
+pub struct TyEnv<'cx> {
+    cx: Ctxt<'cx>,
     names: NameEnv,
-    items: ValEnv<Type>,
+    items: ValEnv<'cx, Type<'cx>>,
 }
 
 impl VarEnv {
@@ -38,42 +40,48 @@ impl VarEnv {
     }
 }
 
-impl TyEnv {
-    pub fn new() -> Self {
+impl<'cx> TyEnv<'cx> {
+    pub fn new(cx: Ctxt<'cx>) -> Self {
         TyEnv {
+            cx,
             names: NameEnv::new(),
-            items: ValEnv::new(),
+            items: ValEnv::new(cx),
         }
     }
+    pub fn cx(&self) -> Ctxt<'cx> {
+        self.cx
+    }
     pub fn as_varenv(&self) -> VarEnv {
         self.names.as_varenv()
     }
-    pub fn to_nzenv(&self) -> NzEnv {
+    pub fn to_nzenv(&self) -> NzEnv<'cx> {
         self.items.discard_types()
     }
     pub fn as_nameenv(&self) -> &NameEnv {
         &self.names
     }
 
-    pub fn insert_type(&self, x: &Label, ty: Type) -> Self {
+    pub fn insert_type(&self, x: &Label, ty: Type<'cx>) -> Self {
         TyEnv {
+            cx: self.cx,
             names: self.names.insert(x),
             items: self.items.insert_type(ty),
         }
     }
-    pub fn insert_value(&self, x: &Label, e: Nir, ty: Type) -> Self {
+    pub fn insert_value(&self, x: &Label, e: Nir<'cx>, ty: Type<'cx>) -> Self {
         TyEnv {
+            cx: self.cx,
             names: self.names.insert(x),
             items: self.items.insert_value(e, ty),
         }
     }
-    pub fn lookup(&self, var: AlphaVar) -> Type {
+    pub fn lookup(&self, var: AlphaVar) -> Type<'cx> {
         self.items.lookup_ty(var)
     }
 }
 
-impl<'a> From<&'a TyEnv> for NzEnv {
-    fn from(x: &'a TyEnv) -> Self {
+impl<'a, 'cx> From<&'a TyEnv<'cx>> for NzEnv<'cx> {
+    fn from(x: &'a TyEnv<'cx>) -> Self {
         x.to_nzenv()
     }
 }
diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs
index f34802c..7b04f57 100644
--- a/dhall/src/semantics/tck/tir.rs
+++ b/dhall/src/semantics/tck/tir.rs
@@ -2,6 +2,7 @@ use crate::builtins::Builtin;
 use crate::error::{ErrorBuilder, TypeError};
 use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv};
 use crate::syntax::{Const, Expr, Span};
+use crate::Ctxt;
 
 /// The type of a type. 0 is `Type`, 1 is `Kind`, etc...
 #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)]
@@ -9,17 +10,17 @@ pub struct Universe(u8);
 
 /// An expression representing a type
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub struct Type {
-    val: Nir,
+pub struct Type<'cx> {
+    val: Nir<'cx>,
     univ: Universe,
 }
 
 /// A hir expression plus its inferred type.
 /// Stands for "Typed intermediate representation"
 #[derive(Debug, Clone)]
-pub struct Tir<'hir> {
-    hir: &'hir Hir,
-    ty: Type,
+pub struct Tir<'cx, 'hir> {
+    hir: &'hir Hir<'cx>,
+    ty: Type<'cx>,
 }
 
 impl Universe {
@@ -43,16 +44,16 @@ impl Universe {
     }
 }
 
-impl Type {
-    pub fn new(val: Nir, univ: Universe) -> Self {
+impl<'cx> Type<'cx> {
+    pub fn new(val: Nir<'cx>, univ: Universe) -> Self {
         Type { val, univ }
     }
     /// Creates a new Type and infers its universe by re-typechecking its value.
     /// TODO: ideally avoid this function altogether. Would need to store types in RecordType and
     /// PiClosure.
     pub fn new_infer_universe(
-        env: &TyEnv,
-        val: Nir,
+        env: &TyEnv<'cx>,
+        val: Nir<'cx>,
     ) -> Result<Self, TypeError> {
         let c = val.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const();
         let u = match c {
@@ -67,14 +68,14 @@ impl Type {
     pub fn from_const(c: Const) -> Self {
         Self::new(Nir::from_const(c), c.to_universe().next())
     }
-    pub fn from_builtin(b: Builtin) -> Self {
+    pub fn from_builtin(cx: Ctxt<'cx>, b: Builtin) -> Self {
         use Builtin::*;
         match b {
             Bool | Natural | Integer | Double | Text => {}
             _ => unreachable!("this builtin is not a type: {}", b),
         }
 
-        Self::new(Nir::from_builtin(b), Universe::from_const(Const::Type))
+        Self::new(Nir::from_builtin(cx, b), Universe::from_const(Const::Type))
     }
 
     /// Get the type of this type
@@ -82,60 +83,60 @@ impl Type {
         self.univ
     }
 
-    pub fn to_nir(&self) -> Nir {
+    pub fn to_nir(&self) -> Nir<'cx> {
         self.val.clone()
     }
-    pub fn as_nir(&self) -> &Nir {
+    pub fn as_nir(&self) -> &Nir<'cx> {
         &self.val
     }
-    pub fn into_nir(self) -> Nir {
+    pub fn into_nir(self) -> Nir<'cx> {
         self.val
     }
     pub fn as_const(&self) -> Option<Const> {
         self.val.as_const()
     }
-    pub fn kind(&self) -> &NirKind {
+    pub fn kind(&self) -> &NirKind<'cx> {
         self.val.kind()
     }
 
-    pub fn to_hir(&self, venv: VarEnv) -> Hir {
+    pub fn to_hir(&self, venv: VarEnv) -> Hir<'cx> {
         self.val.to_hir(venv)
     }
-    pub fn to_expr_tyenv(&self, tyenv: &TyEnv) -> Expr {
+    pub fn to_expr_tyenv(&self, tyenv: &TyEnv<'cx>) -> Expr {
         self.val.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
     }
 }
 
-impl<'hir> Tir<'hir> {
-    pub fn from_hir(hir: &'hir Hir, ty: Type) -> Self {
+impl<'cx, 'hir> Tir<'cx, 'hir> {
+    pub fn from_hir(hir: &'hir Hir<'cx>, ty: Type<'cx>) -> Self {
         Tir { hir, ty }
     }
 
     pub fn span(&self) -> Span {
         self.as_hir().span()
     }
-    pub fn ty(&self) -> &Type {
+    pub fn ty(&self) -> &Type<'cx> {
         &self.ty
     }
-    pub fn into_ty(self) -> Type {
+    pub fn into_ty(self) -> Type<'cx> {
         self.ty
     }
 
-    pub fn to_hir(&self) -> Hir {
+    pub fn to_hir(&self) -> Hir<'cx> {
         self.as_hir().clone()
     }
-    pub fn as_hir(&self) -> &Hir {
-        &self.hir
+    pub fn as_hir(&self) -> &'hir Hir<'cx> {
+        self.hir
     }
-    pub fn to_expr_tyenv(&self, env: &TyEnv) -> Expr {
+    pub fn to_expr_tyenv(&self, env: &TyEnv<'cx>) -> Expr {
         self.as_hir().to_expr_tyenv(env)
     }
 
     /// Eval the Tir. 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> {
         self.as_hir().eval(env.into())
     }
-    pub fn ensure_is_type(&self, env: &TyEnv) -> Result<(), TypeError> {
+    pub fn ensure_is_type(&self, env: &TyEnv<'cx>) -> Result<(), TypeError> {
         if self.ty().as_const().is_none() {
             return mkerr(
                 ErrorBuilder::new(format!(
@@ -159,7 +160,10 @@ impl<'hir> Tir<'hir> {
         Ok(())
     }
     /// Evaluate to a Type.
-    pub fn eval_to_type(&self, env: &TyEnv) -> Result<Type, TypeError> {
+    pub fn eval_to_type(
+        &self,
+        env: &TyEnv<'cx>,
+    ) -> Result<Type<'cx>, TypeError> {
         self.ensure_is_type(env)?;
         Ok(Type::new(
             self.eval(env),
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 498bd76..23c2bd2 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -5,6 +5,7 @@ use crate::error::{ErrorBuilder, TypeError, TypeMessage};
 use crate::operations::typecheck_operation;
 use crate::semantics::{Hir, HirKind, Nir, NirKind, Tir, TyEnv, Type};
 use crate::syntax::{Const, ExprKind, InterpolatedTextContents, NumKind, Span};
+use crate::Ctxt;
 
 fn function_check(a: Const, b: Const) -> Const {
     if b == Const::Type {
@@ -28,11 +29,12 @@ pub fn mk_span_err<T, S: ToString>(span: Span, msg: S) -> Result<T, TypeError> {
 
 /// When all sub-expressions have been typed, check the remaining toplevel
 /// layer.
-fn type_one_layer(
-    env: &TyEnv,
-    ekind: ExprKind<Tir<'_>>,
+fn type_one_layer<'cx>(
+    env: &TyEnv<'cx>,
+    ekind: ExprKind<Tir<'cx, '_>>,
     span: Span,
-) -> Result<Type, TypeError> {
+) -> Result<Type<'cx>, TypeError> {
+    let cx = env.cx();
     let span_err = |msg: &str| mk_span_err(span.clone(), msg);
 
     Ok(match ekind {
@@ -50,18 +52,21 @@ fn type_one_layer(
 
         ExprKind::Const(Const::Type) => Type::from_const(Const::Kind),
         ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort),
-        ExprKind::Num(num) => Type::from_builtin(match num {
-            NumKind::Bool(_) => Builtin::Bool,
-            NumKind::Natural(_) => Builtin::Natural,
-            NumKind::Integer(_) => Builtin::Integer,
-            NumKind::Double(_) => Builtin::Double,
-        }),
+        ExprKind::Num(num) => Type::from_builtin(
+            cx,
+            match num {
+                NumKind::Bool(_) => Builtin::Bool,
+                NumKind::Natural(_) => Builtin::Natural,
+                NumKind::Integer(_) => Builtin::Integer,
+                NumKind::Double(_) => Builtin::Double,
+            },
+        ),
         ExprKind::Builtin(b) => {
-            let t_hir = type_of_builtin(b);
-            typecheck(&t_hir)?.eval_to_type(env)?
+            let t_hir = type_of_builtin(cx, b);
+            typecheck(cx, &t_hir)?.eval_to_type(env)?
         }
         ExprKind::TextLit(interpolated) => {
-            let text_type = Type::from_builtin(Builtin::Text);
+            let text_type = Type::from_builtin(cx, Builtin::Text);
             for contents in interpolated.iter() {
                 use InterpolatedTextContents::Expr;
                 if let Expr(x) = contents {
@@ -78,7 +83,7 @@ fn type_one_layer(
             }
 
             let t = x.ty().to_nir();
-            Nir::from_builtin(Builtin::Optional)
+            Nir::from_builtin(cx, Builtin::Optional)
                 .app(t)
                 .to_type(Const::Type)
         }
@@ -103,7 +108,9 @@ fn type_one_layer(
             }
 
             let t = x.ty().to_nir();
-            Nir::from_builtin(Builtin::List).app(t).to_type(Const::Type)
+            Nir::from_builtin(cx, Builtin::List)
+                .app(t)
+                .to_type(Const::Type)
         }
         ExprKind::RecordLit(kvs) => {
             // An empty record type has type Type
@@ -170,14 +177,30 @@ fn type_one_layer(
 /// to compare with.
 // We pass the annotation to avoid duplicating the annot checking logic. I hope one day we can use
 // it to handle the annotations in merge/toMap/etc. uniformly.
-pub fn type_with<'hir>(
-    env: &TyEnv,
-    hir: &'hir Hir,
-    annot: Option<Type>,
-) -> Result<Tir<'hir>, TypeError> {
+pub fn type_with<'cx, 'hir>(
+    env: &TyEnv<'cx>,
+    hir: &'hir Hir<'cx>,
+    annot: Option<Type<'cx>>,
+) -> Result<Tir<'cx, 'hir>, TypeError> {
     let tir = match hir.kind() {
         HirKind::Var(var) => Tir::from_hir(hir, env.lookup(*var)),
-        HirKind::Import(_, ty) => Tir::from_hir(hir, ty.clone()),
+        HirKind::MissingVar(var) => mkerr(
+            ErrorBuilder::new(format!("unbound variable `{}`", var))
+                .span_err(hir.span(), "not found in this scope")
+                .format(),
+        )?,
+        HirKind::Import(import) => {
+            let typed = env.cx()[import].unwrap_result();
+            Tir::from_hir(hir, typed.ty.clone())
+        }
+        HirKind::ImportAlternative(alt, left, right) => {
+            let hir = if env.cx()[alt].unwrap_selected() {
+                left
+            } else {
+                right
+            };
+            return type_with(env, hir, annot);
+        }
         HirKind::Expr(ExprKind::Var(_)) => {
             unreachable!("Hir should contain no unresolved variables")
         }
@@ -267,15 +290,19 @@ pub fn type_with<'hir>(
 
 /// Typecheck an expression and return the expression annotated with its type if type-checking
 /// succeeded, or an error if type-checking failed.
-pub fn typecheck<'hir>(hir: &'hir Hir) -> Result<Tir<'hir>, TypeError> {
-    type_with(&TyEnv::new(), hir, None)
+pub fn typecheck<'cx, 'hir>(
+    cx: Ctxt<'cx>,
+    hir: &'hir Hir<'cx>,
+) -> Result<Tir<'cx, 'hir>, TypeError> {
+    type_with(&TyEnv::new(cx), hir, None)
 }
 
 /// Like `typecheck`, but additionally checks that the expression's type matches the provided type.
-pub fn typecheck_with<'hir>(
-    hir: &'hir Hir,
-    ty: &Hir,
-) -> Result<Tir<'hir>, TypeError> {
-    let ty = typecheck(ty)?.eval_to_type(&TyEnv::new())?;
-    type_with(&TyEnv::new(), hir, Some(ty))
+pub fn typecheck_with<'cx, 'hir>(
+    cx: Ctxt<'cx>,
+    hir: &'hir Hir<'cx>,
+    ty: &Hir<'cx>,
+) -> Result<Tir<'cx, 'hir>, TypeError> {
+    let ty = typecheck(cx, ty)?.eval_to_type(&TyEnv::new(cx))?;
+    type_with(&TyEnv::new(cx), hir, Some(ty))
 }