Take Hir for typecheck

7 files changed, 58 insertions, 57 deletions

diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index c2a2f19..2d261f9 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -79,7 +79,7 @@ impl Parsed {
         resolve::resolve(self)
     }
     pub fn skip_resolve(self) -> Result<Resolved, Error> {
-        resolve::skip_resolve_expr(self)
+        Ok(Resolved(resolve::skip_resolve(&self.0)?))
     }
 
     pub fn encode(&self) -> Result<Vec<u8>, EncodeError> {
@@ -94,10 +94,10 @@ impl Parsed {
 
 impl Resolved {
     pub fn typecheck(&self) -> Result<Typed, TypeError> {
-        Ok(Typed(typecheck(&self.to_expr())?))
+        Ok(Typed(typecheck(&self.0)?))
     }
     pub fn typecheck_with(self, ty: &Normalized) -> Result<Typed, TypeError> {
-        Ok(Typed(typecheck_with(&self.to_expr(), ty.to_expr())?))
+        Ok(Typed(typecheck_with(&self.0, ty.to_hir())?))
     }
     /// Converts a value back to the corresponding AST expression.
     pub fn to_expr(&self) -> ResolvedExpr {
@@ -136,6 +136,10 @@ impl Normalized {
             normalize: false,
         })
     }
+    /// Converts a value back to the corresponding Hir expression.
+    pub(crate) fn to_hir(&self) -> Hir {
+        self.0.to_hir_noenv()
+    }
     /// Converts a value back to the corresponding AST expression, alpha-normalizing in the process.
     pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr {
         self.0.to_expr(ToExprOptions {
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index 715e045..b1d12aa 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -1,5 +1,5 @@
 use crate::semantics::{
-    typecheck, Hir, HirKind, NzEnv, Value, ValueKind, VarEnv,
+    skip_resolve, typecheck, Hir, HirKind, NzEnv, Value, ValueKind, VarEnv,
 };
 use crate::syntax::map::DupTreeMap;
 use crate::syntax::Const::Type;
@@ -115,9 +115,9 @@ macro_rules! make_type {
     };
 }
 
-pub(crate) fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
+pub(crate) fn type_of_builtin(b: Builtin) -> Hir {
     use Builtin::*;
-    match b {
+    let expr = match b {
         Bool | Natural | Integer | Double | Text => make_type!(Type),
         List | Optional => make_type!(
             Type -> Type
@@ -200,7 +200,8 @@ pub(crate) fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
         OptionalNone => make_type!(
             forall (A: Type) -> Optional A
         ),
-    }
+    };
+    skip_resolve(&expr).unwrap()
 }
 
 // Ad-hoc macro to help construct closures
@@ -264,7 +265,8 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
         Value(Value),
         DoneAsIs,
     }
-    let make_closure = |e| typecheck(&e).unwrap().eval(&env);
+    let make_closure =
+        |e| typecheck(&skip_resolve(&e).unwrap()).unwrap().eval(&env);
 
     let ret = match (b, args.as_slice()) {
         (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())),
diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs
index a8c0659..ffa16ca 100644
--- a/dhall/src/semantics/mod.rs
+++ b/dhall/src/semantics/mod.rs
@@ -7,4 +7,5 @@ pub mod tck;
 pub(crate) use self::builtins::*;
 pub(crate) use self::hir::*;
 pub(crate) use self::nze::*;
+pub(crate) use self::resolve::*;
 pub(crate) use self::tck::*;
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index a771b91..48acdb5 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -327,9 +327,12 @@ impl Value {
 
         Hir::new(hir, self.0.span.clone())
     }
+    pub fn to_hir_noenv(&self) -> Hir {
+        self.to_hir(VarEnv::new())
+    }
     pub fn to_tyexpr_tyenv(&self, tyenv: &TyEnv) -> TyExpr {
-        let expr = self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv);
-        type_with(tyenv, &expr).unwrap()
+        let hir = self.to_hir(tyenv.as_varenv());
+        type_with(tyenv, &hir).unwrap()
     }
     pub fn to_tyexpr_noenv(&self) -> TyExpr {
         self.to_tyexpr_tyenv(&TyEnv::new())
diff --git a/dhall/src/semantics/resolve.rs b/dhall/src/semantics/resolve.rs
index e12e892..8c9bb05 100644
--- a/dhall/src/semantics/resolve.rs
+++ b/dhall/src/semantics/resolve.rs
@@ -6,7 +6,7 @@ use crate::error::{Error, ImportError};
 use crate::semantics::{mkerr, Hir, HirKind, NameEnv};
 use crate::syntax;
 use crate::syntax::{BinOp, Expr, ExprKind, FilePath, ImportLocation, URL};
-use crate::{Normalized, Parsed, Resolved};
+use crate::{Normalized, Parsed, ParsedExpr, Resolved};
 
 type Import = syntax::Import<Hir>;
 
@@ -162,13 +162,10 @@ pub(crate) fn resolve(parsed: Parsed) -> Result<Resolved, Error> {
     resolve_with_env(&mut ResolveEnv::new(), parsed)
 }
 
-pub(crate) fn skip_resolve_expr(parsed: Parsed) -> Result<Resolved, Error> {
-    let Parsed(expr, _) = parsed;
-    let resolved =
-        traverse_resolve_expr(&mut NameEnv::new(), &expr, &mut |import| {
-            Err(ImportError::UnexpectedImport(import).into())
-        })?;
-    Ok(Resolved(resolved))
+pub(crate) fn skip_resolve(expr: &ParsedExpr) -> Result<Hir, Error> {
+    traverse_resolve_expr(&mut NameEnv::new(), expr, &mut |import| {
+        Err(ImportError::UnexpectedImport(import).into())
+    })
 }
 
 pub trait Canonicalize {
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index af955f4..3b02074 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -21,9 +21,9 @@ pub(crate) struct TyEnv {
 }
 
 impl VarEnv {
-    // pub fn new() -> Self {
-    //     VarEnv { size: 0 }
-    // }
+    pub fn new() -> Self {
+        VarEnv { size: 0 }
+    }
     pub fn size(&self) -> usize {
         self.size
     }
@@ -116,9 +116,7 @@ impl TyEnv {
             items: self.items.insert_value(e, ty),
         }
     }
-    pub fn lookup(&self, var: &V) -> Option<(AlphaVar, Type)> {
-        let var = self.names.unlabel_var(var)?;
-        let ty = self.items.lookup_ty(&var);
-        Some((var, ty))
+    pub fn lookup(&self, var: &AlphaVar) -> Type {
+        self.items.lookup_ty(&var)
     }
 }
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index eb6a58c..ac113cd 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -5,11 +5,11 @@ use std::collections::HashMap;
 use crate::error::{ErrorBuilder, TypeError, TypeMessage};
 use crate::semantics::merge_maps;
 use crate::semantics::{
-    type_of_builtin, Binder, BuiltinClosure, Closure, TyEnv, TyExpr,
-    TyExprKind, Type, Value, ValueKind,
+    type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, TyEnv,
+    TyExpr, TyExprKind, Type, Value, ValueKind,
 };
 use crate::syntax::{
-    BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Span,
+    BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Span,
 };
 use crate::Normalized;
 
@@ -115,8 +115,8 @@ fn type_one_layer(
         ExprKind::Const(Const::Type) => Value::from_const(Const::Kind),
         ExprKind::Const(Const::Kind) => Value::from_const(Const::Sort),
         ExprKind::Builtin(b) => {
-            let t_expr = type_of_builtin(*b);
-            let t_tyexpr = type_with(env, &t_expr)?;
+            let t_hir = type_of_builtin(*b);
+            let t_tyexpr = typecheck(&t_hir)?;
             t_tyexpr.eval(env.as_nzenv())
         }
         ExprKind::BoolLit(_) => Value::from_builtin(Builtin::Bool),
@@ -761,25 +761,16 @@ fn type_one_layer(
 }
 
 /// `type_with` typechecks an expressio in the provided environment.
-pub(crate) fn type_with(
-    env: &TyEnv,
-    expr: &Expr<Normalized>,
-) -> Result<TyExpr, TypeError> {
-    let (tyekind, ty) = match expr.as_ref() {
-        ExprKind::Var(var) => match env.lookup(&var) {
-            Some((v, ty)) => (TyExprKind::Var(v), Some(ty)),
-            None => {
-                return mkerr(
-                    ErrorBuilder::new(format!("unbound variable `{}`", var))
-                        .span_err(expr.span(), "not found in this scope")
-                        .format(),
-                )
-            }
-        },
-        ExprKind::Const(Const::Sort) => {
+pub(crate) fn type_with(env: &TyEnv, hir: &Hir) -> Result<TyExpr, TypeError> {
+    let (tyekind, ty) = match hir.kind() {
+        HirKind::Var(var) => (TyExprKind::Var(*var), Some(env.lookup(&var))),
+        HirKind::Expr(ExprKind::Var(_)) => {
+            unreachable!("Hir should contain no unresolved variables")
+        }
+        HirKind::Expr(ExprKind::Const(Const::Sort)) => {
             (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None)
         }
-        ExprKind::Embed(p) => {
+        HirKind::Expr(ExprKind::Embed(p)) => {
             let val = p.clone().into_value();
             (
                 val.to_tyexpr_noenv().kind().clone(),
@@ -787,7 +778,7 @@ pub(crate) fn type_with(
             )
             // return Ok(p.clone().into_value().to_tyexpr_noenv())
         }
-        ekind => {
+        HirKind::Expr(ekind) => {
             let ekind = match ekind {
                 ExprKind::Lam(binder, annot, body) => {
                     let annot = type_with(env, annot)?;
@@ -805,7 +796,13 @@ pub(crate) fn type_with(
                 }
                 ExprKind::Let(binder, annot, val, body) => {
                     let val = if let Some(t) = annot {
-                        t.rewrap(ExprKind::Annot(val.clone(), t.clone()))
+                        Hir::new(
+                            HirKind::Expr(ExprKind::Annot(
+                                val.clone(),
+                                t.clone(),
+                            )),
+                            t.span(),
+                        )
                     } else {
                         val.clone()
                     };
@@ -818,16 +815,16 @@ pub(crate) fn type_with(
                 }
                 _ => ekind.traverse_ref(|e| type_with(env, e))?,
             };
-            return type_one_layer(env, ekind, expr.span());
+            return type_one_layer(env, ekind, hir.span());
         }
     };
 
-    Ok(TyExpr::new(tyekind, ty, expr.span()))
+    Ok(TyExpr::new(tyekind, ty, hir.span()))
 }
 
 /// Typecheck an expression and return the expression annotated with types if type-checking
 /// succeeded, or an error if type-checking failed.
-pub(crate) fn typecheck(e: &Expr<Normalized>) -> Result<TyExpr, TypeError> {
+pub(crate) fn typecheck(e: &Hir) -> Result<TyExpr, TypeError> {
     let res = type_with(&TyEnv::new(), e)?;
     // Ensure that the inferred type exists (i.e. this is not Sort)
     res.get_type()?;
@@ -835,9 +832,8 @@ pub(crate) fn typecheck(e: &Expr<Normalized>) -> Result<TyExpr, TypeError> {
 }
 
 /// Like `typecheck`, but additionally checks that the expression's type matches the provided type.
-pub(crate) fn typecheck_with(
-    expr: &Expr<Normalized>,
-    ty: Expr<Normalized>,
-) -> Result<TyExpr, TypeError> {
-    typecheck(&expr.rewrap(ExprKind::Annot(expr.clone(), ty)))
+pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result<TyExpr, TypeError> {
+    let hir =
+        Hir::new(HirKind::Expr(ExprKind::Annot(hir.clone(), ty)), hir.span());
+    typecheck(&hir)
 }