summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2020-12-07 17:48:20 +0000
committerNadrieril2020-12-07 19:35:13 +0000
commit7a392b07166c089979e69d4c8a68da3298964c28 (patch)
tree3a861160e7d4b379904dbed891bb684de0ad26bc /dhall
parentf478bc16a3b8414770d84dd87f3e46b869d31750 (diff)
Defer name errors to typechecking
We aren't supposed to inspect anything before alternatives are chosen
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/semantics/nze/normalize.rs1
-rw-r--r--dhall/src/semantics/resolve/hir.rs3
-rw-r--r--dhall/src/semantics/resolve/resolve.rs9
-rw-r--r--dhall/src/semantics/tck/typecheck.rs5
4 files changed, 13 insertions, 5 deletions
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index d545750..0a09a80 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -154,6 +154,7 @@ pub fn normalize_one_layer<'cx>(expr: ExprKind<Nir<'cx>>) -> NirKind<'cx> {
/// Normalize Hir into WHNF
pub fn normalize_hir<'cx>(env: &NzEnv<'cx>, hir: &Hir<'cx>) -> NirKind<'cx> {
match hir.kind() {
+ HirKind::MissingVar(..) => unreachable!("ruled out by typechecking"),
HirKind::Var(var) => env.lookup_val(*var),
HirKind::Import(import) => {
let typed = env.cx()[import].unwrap_result();
diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs
index 3e282b4..05a8550 100644
--- a/dhall/src/semantics/resolve/hir.rs
+++ b/dhall/src/semantics/resolve/hir.rs
@@ -13,6 +13,8 @@ pub struct AlphaVar {
pub enum HirKind<'cx> {
/// A resolved variable (i.e. a DeBruijn index)
Var(AlphaVar),
+ /// 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 by the time we get to typechecking/normalization.
Import(ImportId<'cx>),
// Forbidden ExprKind variants: Var, Import, Completion
@@ -104,6 +106,7 @@ fn hir_to_expr<'cx>(
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::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());
diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs
index 7450825..c4cd518 100644
--- a/dhall/src/semantics/resolve/resolve.rs
+++ b/dhall/src/semantics/resolve/resolve.rs
@@ -377,11 +377,7 @@ fn traverse_resolve_expr<'cx>(
Ok(match expr.kind() {
ExprKind::Var(var) => match name_env.unlabel_var(&var) {
Some(v) => Hir::new(HirKind::Var(v), expr.span()),
- None => mkerr(
- ErrorBuilder::new(format!("unbound variable `{}`", var))
- .span_err(expr.span(), "not found in this scope")
- .format(),
- )?,
+ None => Hir::new(HirKind::MissingVar(var.clone()), expr.span()),
},
ExprKind::Op(OpKind::BinOp(BinOp::ImportAlt, l, r)) => {
match traverse_resolve_expr(name_env, l, f) {
@@ -492,6 +488,8 @@ fn resolve_with_env<'cx>(
Ok(Resolved(resolved))
}
+/// Resolves all imports and names. Returns errors if importing failed. Name errors are deferred to
+/// typechecking.
pub fn resolve<'cx>(
cx: Ctxt<'cx>,
parsed: Parsed,
@@ -499,6 +497,7 @@ pub fn resolve<'cx>(
resolve_with_env(&mut ImportEnv::new(cx), parsed)
}
+/// Resolves names and errors if we find any imports.
pub fn skip_resolve<'cx>(
cx: Ctxt<'cx>,
parsed: Parsed,
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 5a44c9c..e14bcc6 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -184,6 +184,11 @@ pub fn type_with<'cx, 'hir>(
) -> Result<Tir<'cx, 'hir>, TypeError> {
let tir = match hir.kind() {
HirKind::Var(var) => Tir::from_hir(hir, env.lookup(*var)),
+ 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())