summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/error/mod.rs17
-rw-r--r--dhall/src/semantics/core/context.rs95
-rw-r--r--dhall/src/semantics/core/value.rs32
-rw-r--r--dhall/src/semantics/core/visitor.rs8
-rw-r--r--dhall/src/semantics/nze/nzexpr.rs411
-rw-r--r--dhall/src/semantics/phase/normalize.rs7
-rw-r--r--dhall/src/semantics/phase/typecheck.rs624
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs5
-rw-r--r--dhall/src/semantics/tck/typecheck.rs30
-rw-r--r--dhall/src/syntax/ast/expr.rs4
10 files changed, 31 insertions, 1202 deletions
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 5330c59..215a7bf 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -3,7 +3,7 @@ use std::io::Error as IOError;
use crate::semantics::core::value::Value;
use crate::semantics::phase::resolve::ImportStack;
use crate::semantics::phase::NormalizedExpr;
-use crate::syntax::{Import, Label, ParseError, Span};
+use crate::syntax::{Import, ParseError};
pub type Result<T> = std::result::Result<T, Error>;
@@ -45,7 +45,7 @@ pub struct TypeError {
/// The specific type error
#[derive(Debug)]
pub(crate) enum TypeMessage {
- UnboundVariable(Span),
+ // UnboundVariable(Span),
InvalidInputType(Value),
InvalidOutputType(Value),
// NotAFunction(Value),
@@ -57,7 +57,7 @@ pub(crate) enum TypeMessage {
// InvalidPredicate(Value),
// IfBranchMismatch(Value, Value),
// IfBranchMustBeTerm(bool, Value),
- InvalidFieldType(Label, Value),
+ // InvalidFieldType(Label, Value),
// NotARecord(Label, Value),
// MustCombineRecord(Value),
// MissingRecordField(Label, Value),
@@ -76,9 +76,9 @@ pub(crate) enum TypeMessage {
// ProjectionMissingEntry,
// ProjectionDuplicateField,
Sort,
- RecordTypeDuplicateField,
+ // RecordTypeDuplicateField,
// RecordTypeMergeRequiresRecordType(Value),
- UnionTypeDuplicateField,
+ // UnionTypeDuplicateField,
// EquivalenceArgumentMustBeTerm(bool, Value),
// EquivalenceTypeMismatch(Value, Value),
// AssertMismatch(Value, Value),
@@ -96,7 +96,7 @@ impl std::fmt::Display for TypeError {
fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
use TypeMessage::*;
let msg = match &self.message {
- UnboundVariable(var) => var.error("Type error: Unbound variable"),
+ // UnboundVariable(var) => var.error("Type error: Unbound variable"),
InvalidInputType(v) => {
v.span().error("Type error: Invalid function input")
}
@@ -171,8 +171,3 @@ impl From<TypeError> for Error {
Error::Typecheck(err)
}
}
-impl From<crate::semantics::nze::nzexpr::TypeError> for Error {
- fn from(_: crate::semantics::nze::nzexpr::TypeError) -> Error {
- Error::Decode(DecodeError::WrongFormatError("type error".to_string()))
- }
-}
diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index 9749c50..8b13789 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -1,96 +1 @@
-use crate::error::TypeError;
-use crate::semantics::core::value::Value;
-use crate::semantics::core::value::ValueKind;
-use crate::semantics::core::var::{AlphaVar, Binder};
-use crate::semantics::nze::NzVar;
-// use crate::semantics::phase::normalize::{NzEnv, NzEnvItem};
-use crate::syntax::{Label, V};
-#[derive(Debug, Clone)]
-enum CtxItem {
- // Variable is bound with given type
- Kept(Value),
- // Variable has been replaced by corresponding value
- Replaced(Value),
-}
-
-#[derive(Debug, Clone)]
-pub(crate) struct TyCtx {
- ctx: Vec<(Binder, CtxItem)>,
-}
-
-impl TyCtx {
- pub fn new() -> Self {
- TyCtx { ctx: Vec::new() }
- }
- fn with_vec(&self, vec: Vec<(Binder, CtxItem)>) -> Self {
- TyCtx { ctx: vec }
- }
- pub fn insert_type(&self, x: &Binder, t: Value) -> Self {
- let mut vec = self.ctx.clone();
- vec.push((x.clone(), CtxItem::Kept(t.under_binder())));
- self.with_vec(vec)
- }
- pub fn insert_value(
- &self,
- x: &Binder,
- e: Value,
- ) -> Result<Self, TypeError> {
- let mut vec = self.ctx.clone();
- vec.push((x.clone(), CtxItem::Replaced(e)));
- Ok(self.with_vec(vec))
- }
- pub fn lookup(&self, var: &V<Label>) -> Option<Value> {
- let mut var = var.clone();
- let mut shift_delta: isize = 0;
- let mut rev_ctx = self.ctx.iter().rev().map(|(b, i)| (b.to_label(), i));
- let found_item = loop {
- if let Some((label, item)) = rev_ctx.next() {
- var = match var.over_binder(&label) {
- Some(newvar) => newvar,
- None => break item,
- };
- if let CtxItem::Kept(_) = item {
- shift_delta += 1;
- }
- } else {
- // Unbound variable
- return None;
- }
- };
- let var_idx = rev_ctx
- .filter(|(_, i)| match i {
- CtxItem::Kept(_) => true,
- CtxItem::Replaced(_) => false,
- })
- .count();
-
- let v = match found_item {
- CtxItem::Kept(t) => Value::from_kind_and_type(
- ValueKind::Var(AlphaVar::default(), NzVar::new(var_idx)),
- t.clone(),
- ),
- CtxItem::Replaced(v) => v.clone()
- // .normalize_whnf(&NzEnv::construct(
- // self.ctx
- // .iter()
- // .filter_map(|(_, i)| match i {
- // CtxItem::Kept(t) => {
- // Some(NzEnvItem::Kept(t.clone()))
- // }
- // CtxItem::Replaced(_) => None,
- // })
- // .collect(),
- // )),
- };
- // Can't fail because delta is positive
- let v = v.shift(shift_delta, &AlphaVar::default()).unwrap();
- return Some(v);
- }
- // pub fn lookup_alpha(&self, var: &AlphaVar) -> Option<Value> {
- // self.lookup(&var.normal)
- // }
- pub fn new_binder(&self, l: &Label) -> Binder {
- Binder::new(l.clone())
- }
-}
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index aa819d2..30c4116 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -68,8 +68,6 @@ pub(crate) enum Closure {
#[derive(Debug, Clone, PartialEq, Eq)]
pub(crate) enum ValueKind<Value> {
/// Closures
- Lam(Binder, Value, Value),
- Pi(Binder, Value, Value),
LamClosure {
binder: Binder,
annot: Value,
@@ -133,13 +131,6 @@ impl Value {
pub(crate) fn from_kind_and_type(v: ValueKind<Value>, t: Value) -> Value {
Value::new(v, Unevaled, t, Span::Artificial)
}
- pub(crate) fn from_kind_and_type_and_span(
- v: ValueKind<Value>,
- t: Value,
- span: Span,
- ) -> Value {
- Value::new(v, Unevaled, t, span)
- }
pub(crate) fn from_kind_and_type_whnf(
v: ValueKind<Value>,
t: Value,
@@ -155,10 +146,6 @@ impl Value {
pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self {
builtin_to_value_env(b, env)
}
- pub(crate) fn with_span(self, span: Span) -> Self {
- self.as_internal_mut().span = span;
- self
- }
pub(crate) fn as_const(&self) -> Option<Const> {
match &*self.as_whnf() {
@@ -238,10 +225,6 @@ impl Value {
pub(crate) fn app(&self, v: Value) -> Value {
let body_t = match &*self.get_type_not_sort().as_whnf() {
- ValueKind::Pi(_, t, e) => {
- v.check_type(t);
- e.subst_shift(&AlphaVar::default(), &v)
- }
ValueKind::PiClosure { annot, closure, .. } => {
v.check_type(annot);
closure.apply(v.clone())
@@ -276,9 +259,6 @@ impl Value {
pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
Some(self.as_internal().shift(delta, var)?.into_value())
}
- pub(crate) fn over_binder(&self) -> Option<Self> {
- self.shift(-1, &AlphaVar::default())
- }
pub(crate) fn under_binder(&self) -> Self {
// Can't fail since delta is positive
self.shift(1, &AlphaVar::default()).unwrap()
@@ -398,10 +378,6 @@ impl Value {
| ValueKind::AppliedBuiltin(..)
| ValueKind::UnionConstructor(..)
| ValueKind::UnionLit(..) => unreachable!(),
- ValueKind::Lam(x, t, e) => {
- ExprKind::Lam(x.to_label(), t, e)
- }
- ValueKind::Pi(x, t, e) => ExprKind::Pi(x.to_label(), t, e),
ValueKind::Const(c) => ExprKind::Const(c),
ValueKind::BoolLit(b) => ExprKind::BoolLit(b),
ValueKind::NaturalLit(n) => ExprKind::NaturalLit(n),
@@ -555,14 +531,6 @@ impl ValueKind<Value> {
ValueKind::NEOptionalLit(th) => {
th.normalize_mut();
}
- ValueKind::Lam(_, t, e) => {
- t.normalize_mut();
- e.normalize_mut();
- }
- ValueKind::Pi(_, t, e) => {
- t.normalize_mut();
- e.normalize_mut();
- }
ValueKind::LamClosure { annot, .. }
| ValueKind::PiClosure { annot, .. } => {
annot.normalize_mut();
diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs
index 61a7d0b..aec66f8 100644
--- a/dhall/src/semantics/core/visitor.rs
+++ b/dhall/src/semantics/core/visitor.rs
@@ -72,14 +72,6 @@ where
{
use ValueKind::*;
Ok(match input {
- Lam(l, t, e) => {
- let (t, e) = v.visit_binder(l, t, e)?;
- Lam(l.clone(), t, e)
- }
- Pi(l, t, e) => {
- let (t, e) = v.visit_binder(l, t, e)?;
- Pi(l.clone(), t, e)
- }
LamClosure {
binder,
annot,
diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs
index 92ba8fd..043840e 100644
--- a/dhall/src/semantics/nze/nzexpr.rs
+++ b/dhall/src/semantics/nze/nzexpr.rs
@@ -1,76 +1,8 @@
-#![allow(dead_code)]
use crate::semantics::core::var::AlphaVar;
-use crate::semantics::phase::typecheck::rc;
-use crate::semantics::phase::{Normalized, NormalizedExpr, ToExprOptions};
-use crate::syntax::{Expr, ExprKind, Label, V};
+use crate::syntax::{Label, V};
-pub(crate) type Type = NzExpr;
-#[derive(Debug, Clone)]
-pub(crate) struct TypeError;
pub(crate) type Binder = Label;
-// An expression with inferred types at every node and resolved variables.
-#[derive(Debug, Clone)]
-pub(crate) struct TyExpr {
- kind: Box<TyExprKind>,
- ty: Option<Type>,
-}
-
-#[derive(Debug, Clone)]
-pub(crate) enum TyExprKind {
- Var(AlphaVar),
- Expr(ExprKind<TyExpr, Normalized>),
-}
-
-#[derive(Debug, Clone)]
-pub(crate) struct NzExpr {
- kind: Box<NzExprKind>,
- ty: Option<Box<Type>>,
-}
-
-#[derive(Debug, Clone)]
-pub(crate) enum NzExprKind {
- Var {
- var: NzVar,
- },
- Lam {
- binder: Binder,
- annot: NzExpr,
- env: NzEnv,
- body: TyExpr,
- },
- Pi {
- binder: Binder,
- annot: NzExpr,
- env: NzEnv,
- body: TyExpr,
- },
- Expr(ExprKind<NzExpr, Normalized>),
- // Unevaled {
- // env: NzEnv,
- // expr: TyExprKind,
- // },
-}
-
-#[derive(Debug, Clone)]
-enum NzEnvItem {
- // Variable is bound with given type
- Kept(Type),
- // Variable has been replaced by corresponding value
- Replaced(NzExpr),
-}
-
-#[derive(Debug, Clone)]
-pub(crate) struct TyEnv {
- names: NameEnv,
- items: NzEnv,
-}
-
-#[derive(Debug, Clone)]
-pub(crate) struct NzEnv {
- items: Vec<NzEnvItem>,
-}
-
#[derive(Debug, Clone)]
pub(crate) struct NameEnv {
names: Vec<Binder>,
@@ -88,54 +20,6 @@ pub(crate) enum NzVar {
/// Fake fresh variable generated for expression equality checking.
Fresh(usize),
}
-// TODO: temporary hopefully
-// impl std::cmp::PartialEq for NzVar {
-// fn eq(&self, _other: &Self) -> bool {
-// true
-// }
-// }
-
-impl TyEnv {
- pub fn new() -> Self {
- TyEnv {
- names: NameEnv::new(),
- items: NzEnv::new(),
- }
- }
- pub fn as_quoteenv(&self) -> QuoteEnv {
- self.names.as_quoteenv()
- }
- pub fn as_nzenv(&self) -> &NzEnv {
- &self.items
- }
- pub fn as_nameenv(&self) -> &NameEnv {
- &self.names
- }
-
- pub fn insert_type(&self, x: &Binder, t: NzExpr) -> Self {
- TyEnv {
- names: self.names.insert(x),
- items: self.items.insert_type(t),
- }
- }
- pub fn insert_value(&self, x: &Binder, e: NzExpr) -> Self {
- TyEnv {
- names: self.names.insert(x),
- items: self.items.insert_value(e),
- }
- }
- pub fn lookup_var(&self, var: &V<Binder>) -> Option<TyExpr> {
- let var = self.names.unlabel_var(var)?;
- let ty = self.lookup_val(&var).get_type().unwrap();
- Some(TyExpr::new(TyExprKind::Var(var), Some(ty)))
- }
- pub fn lookup_val(&self, var: &AlphaVar) -> NzExpr {
- self.items.lookup_val(var)
- }
- pub fn size(&self) -> usize {
- self.names.size()
- }
-}
impl NameEnv {
pub fn new() -> Self {
@@ -163,9 +47,9 @@ impl NameEnv {
pub fn insert_mut(&mut self, x: &Binder) {
self.names.push(x.clone())
}
- pub fn remove_mut(&mut self) {
- self.names.pop();
- }
+ // pub fn remove_mut(&mut self) {
+ // self.names.pop();
+ // }
pub fn unlabel_var(&self, var: &V<Binder>) -> Option<AlphaVar> {
let V(name, idx) = var;
@@ -178,50 +62,17 @@ impl NameEnv {
.nth(*idx)?;
Some(AlphaVar::new(V((), idx)))
}
- pub fn label_var(&self, var: &AlphaVar) -> V<Binder> {
- let name = &self.names[self.names.len() - 1 - var.idx()];
- let idx = self
- .names
- .iter()
- .rev()
- .take(var.idx())
- .filter(|n| *n == name)
- .count();
- V(name.clone(), idx)
- }
- pub fn size(&self) -> usize {
- self.names.len()
- }
-}
-
-impl NzEnv {
- pub fn new() -> Self {
- NzEnv { items: Vec::new() }
- }
-
- pub fn insert_type(&self, t: NzExpr) -> Self {
- let mut env = self.clone();
- env.items.push(NzEnvItem::Kept(t));
- env
- }
- pub fn insert_value(&self, e: NzExpr) -> Self {
- let mut env = self.clone();
- env.items.push(NzEnvItem::Replaced(e));
- env
- }
- pub fn lookup_val(&self, var: &AlphaVar) -> NzExpr {
- // TODO: use VarEnv
- let idx = self.items.len() - 1 - var.idx();
- match &self.items[idx] {
- NzEnvItem::Kept(ty) => NzExpr::new(
- NzExprKind::Var {
- var: NzVar::new(idx),
- },
- Some(ty.clone()),
- ),
- NzEnvItem::Replaced(x) => x.clone(),
- }
- }
+ // pub fn label_var(&self, var: &AlphaVar) -> V<Binder> {
+ // let name = &self.names[self.names.len() - 1 - var.idx()];
+ // let idx = self
+ // .names
+ // .iter()
+ // .rev()
+ // .take(var.idx())
+ // .filter(|n| *n == name)
+ // .count();
+ // V(name.clone(), idx)
+ // }
}
// TODO: rename to VarEnv
@@ -229,9 +80,6 @@ impl QuoteEnv {
pub fn new() -> Self {
QuoteEnv { size: 0 }
}
- pub fn construct(size: usize) -> Self {
- QuoteEnv { size }
- }
pub fn size(&self) -> usize {
self.size
}
@@ -273,232 +121,3 @@ impl NzVar {
}
}
}
-
-impl TyExpr {
- pub fn new(kind: TyExprKind, ty: Option<Type>) -> Self {
- TyExpr {
- kind: Box::new(kind),
- ty,
- }
- }
-
- pub fn kind(&self) -> &TyExprKind {
- self.kind.as_ref()
- }
- pub fn get_type(&self) -> Result<Type, TypeError> {
- match &self.ty {
- Some(t) => Ok(t.clone()),
- None => Err(TypeError),
- }
- }
-
- /// Converts a value back to the corresponding AST expression.
- pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
- if opts.alpha {
- self.to_expr_alpha()
- } else {
- self.to_expr_noalpha(&mut NameEnv::new())
- }
- }
- fn to_expr_noalpha(&self, env: &mut NameEnv) -> NormalizedExpr {
- rc(match self.kind() {
- TyExprKind::Var(var) => ExprKind::Var(env.label_var(var)),
- TyExprKind::Expr(e) => e.map_ref_maybe_binder(|l, tye| {
- if let Some(l) = l {
- env.insert_mut(l);
- }
- let e = tye.to_expr_noalpha(env);
- if let Some(_) = l {
- env.remove_mut();
- }
- e
- }),
- })
- }
- fn to_expr_alpha(&self) -> NormalizedExpr {
- rc(match self.kind() {
- TyExprKind::Var(var) => ExprKind::Var(V("_".into(), var.idx())),
- TyExprKind::Expr(e) => match e.map_ref(TyExpr::to_expr_alpha) {
- ExprKind::Lam(_, t, e) => ExprKind::Lam("_".into(), t, e),
- ExprKind::Pi(_, t, e) => ExprKind::Pi("_".into(), t, e),
- e => e,
- },
- })
- }
-
- pub fn normalize_nf(&self, env: &NzEnv) -> NzExpr {
- let kind = match self.kind() {
- TyExprKind::Var(var) => return env.lookup_val(var),
- TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => {
- NzExprKind::Lam {
- binder: binder.clone(),
- annot: annot.normalize_nf(env),
- env: env.clone(),
- body: body.clone(),
- }
- }
- TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => {
- NzExprKind::Pi {
- binder: binder.clone(),
- annot: annot.normalize_nf(env),
- env: env.clone(),
- body: body.clone(),
- }
- }
- TyExprKind::Expr(e) => {
- let e = e.map_ref(|tye| tye.normalize_nf(env));
- match e {
- ExprKind::App(f, arg) => match f.kind() {
- NzExprKind::Lam { env, body, .. } => {
- return body.normalize_nf(&env.insert_value(arg))
- }
- _ => NzExprKind::Expr(ExprKind::App(f, arg)),
- },
- _ => NzExprKind::Expr(e),
- }
- }
- };
- let ty = self.ty.clone();
- NzExpr::new(kind, ty)
- }
-
- pub fn normalize(&self) -> NzExpr {
- self.normalize_nf(&NzEnv::new())
- }
-}
-
-impl NzExpr {
- pub fn new(kind: NzExprKind, ty: Option<Type>) -> Self {
- NzExpr {
- kind: Box::new(kind),
- ty: ty.map(Box::new),
- }
- }
-
- pub fn kind(&self) -> &NzExprKind {
- self.kind.as_ref()
- }
- pub fn get_type(&self) -> Result<Type, TypeError> {
- match &self.ty {
- Some(t) => Ok(t.as_ref().clone()),
- None => Err(TypeError),
- }
- }
-
- pub fn quote(&self, qenv: QuoteEnv) -> TyExpr {
- let ty = self.ty.as_ref().map(|t| (**t).clone());
- let kind = match self.kind.as_ref() {
- NzExprKind::Var { var } => TyExprKind::Var(qenv.lookup(var)),
- NzExprKind::Lam {
- binder,
- annot,
- env,
- body,
- } => TyExprKind::Expr(ExprKind::Lam(
- binder.clone(),
- annot.quote(qenv),
- body.normalize_nf(&env.insert_type(annot.clone()))
- .quote(qenv.insert()),
- )),
- NzExprKind::Pi {
- binder,
- annot,
- env,
- body,
- } => TyExprKind::Expr(ExprKind::Pi(
- binder.clone(),
- annot.quote(qenv),
- body.normalize_nf(&env.insert_type(annot.clone()))
- .quote(qenv.insert()),
- )),
- NzExprKind::Expr(e) => {
- TyExprKind::Expr(e.map_ref(|nze| nze.quote(qenv)))
- } // NzExprKind::Unevaled { env, expr } => {
- // return TyExpr::new(expr.clone(), ty.clone())
- // .normalize_nf(env)
- // .quote(qenv)
- // }
- };
- TyExpr::new(kind, ty)
- }
- pub fn to_expr(&self) -> NormalizedExpr {
- self.quote(QuoteEnv::new()).to_expr(ToExprOptions {
- alpha: false,
- normalize: false,
- })
- }
-}
-
-/// Type-check an expression and return the expression alongside its type if type-checking
-/// succeeded, or an error if type-checking failed.
-fn type_with(env: &TyEnv, e: Expr<Normalized>) -> Result<TyExpr, TypeError> {
- match e.as_ref() {
- ExprKind::Var(var) => match env.lookup_var(&var) {
- Some(x) => Ok(x),
- None => Err(TypeError),
- },
- ExprKind::Lam(binder, annot, body) => {
- let annot = type_with(env, annot.clone())?;
- let annot_nf = annot.normalize_nf(env.as_nzenv());
- let body = type_with(
- &env.insert_type(&binder, annot_nf.clone()),
- body.clone(),
- )?;
- let ty = NzExpr::new(
- NzExprKind::Pi {
- binder: binder.clone(),
- annot: annot_nf,
- env: env.as_nzenv().clone(),
- body: body.get_type()?.quote(env.as_quoteenv()),
- },
- None, // TODO: function_check
- );
- Ok(TyExpr::new(
- TyExprKind::Expr(ExprKind::Lam(binder.clone(), annot, body)),
- Some(ty),
- ))
- }
- ExprKind::Pi(binder, annot, body) => {
- let annot = type_with(env, annot.clone())?;
- let annot_nf = annot.normalize_nf(env.as_nzenv());
- let body = type_with(
- &env.insert_type(&binder, annot_nf.clone()),
- body.clone(),
- )?;
- Ok(TyExpr::new(
- TyExprKind::Expr(ExprKind::Pi(binder.clone(), annot, body)),
- None, // TODO: function_check
- ))
- }
- ExprKind::App(f, arg) => {
- let f = type_with(env, f.clone())?;
- let arg = type_with(env, arg.clone())?;
- let tf = f.get_type()?;
- let (_expected_arg_ty, body_env, body_ty) = match tf.kind() {
- NzExprKind::Pi {
- annot, env, body, ..
- } => (annot, env, body),
- _ => return Err(TypeError),
- };
- // if arg.get_type()? != *expected_arg_ty {
- // return Err(TypeError);
- // }
-
- let arg_nf = arg.normalize_nf(env.as_nzenv());
- let ty = body_ty.normalize_nf(&body_env.insert_value(arg_nf));
-
- Ok(TyExpr::new(
- TyExprKind::Expr(ExprKind::App(f, arg)),
- Some(ty),
- ))
- }
- e => Ok(TyExpr::new(
- TyExprKind::Expr(e.traverse_ref(|e| type_with(env, e.clone()))?),
- None,
- )),
- }
-}
-
-pub(crate) fn typecheck(e: Expr<Normalized>) -> Result<TyExpr, TypeError> {
- type_with(&TyEnv::new(), e)
-}
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index f4e4099..d40456b 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -1,4 +1,3 @@
-#![allow(dead_code)]
use std::collections::HashMap;
use std::convert::TryInto;
@@ -376,9 +375,6 @@ pub(crate) fn apply_builtin(
pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind<Value> {
let f_borrow = f.as_whnf();
match &*f_borrow {
- ValueKind::Lam(_, _, e) => e
- .subst_shift(&AlphaVar::default(), &a)
- .to_whnf_check_type(ty),
ValueKind::LamClosure { closure, .. } => {
closure.apply(a).to_whnf_check_type(ty)
}
@@ -861,9 +857,6 @@ impl NzEnv {
pub fn new() -> Self {
NzEnv { items: Vec::new() }
}
- pub fn construct(items: Vec<NzEnvItem>) -> Self {
- NzEnv { items }
- }
pub fn to_alpha_tyenv(&self) -> TyEnv {
TyEnv::from_nzenv_alpha(self)
}
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 6de65e8..4392365 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -1,122 +1,10 @@
-use std::borrow::Cow;
-use std::cmp::max;
-use std::collections::HashMap;
-
-use crate::error::{TypeError, TypeMessage};
-use crate::semantics::core::context::TyCtx;
-use crate::semantics::phase::normalize::merge_maps;
use crate::semantics::phase::normalize::NzEnv;
-use crate::semantics::phase::Normalized;
-use crate::semantics::{AlphaVar, Binder, Value, ValueKind};
+use crate::semantics::{Value, ValueKind};
use crate::syntax;
use crate::syntax::{
- Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span,
- UnspannedExpr,
+ Builtin, Const, Expr, ExprKind, Label, Span, UnspannedExpr,
};
-fn tck_pi_type(
- binder: Binder,
- tx: Value,
- te: Value,
-) -> Result<Value, TypeError> {
- use TypeMessage::*;
-
- let ka = match tx.get_type()?.as_const() {
- Some(k) => k,
- _ => return Err(TypeError::new(InvalidInputType(tx))),
- };
-
- let kb = match te.get_type()?.as_const() {
- Some(k) => k,
- _ => return Err(TypeError::new(InvalidOutputType(te.get_type()?))),
- };
-
- let k = function_check(ka, kb);
-
- Ok(Value::from_kind_and_type(
- ValueKind::Pi(binder, tx, te),
- Value::from_const(k),
- ))
-}
-
-fn tck_record_type(
- kts: impl IntoIterator<Item = Result<(Label, Value), TypeError>>,
-) -> Result<Value, TypeError> {
- use std::collections::hash_map::Entry;
- use TypeMessage::*;
- let mut new_kts = HashMap::new();
- // An empty record type has type Type
- let mut k = Const::Type;
- for e in kts {
- let (x, t) = e?;
- // Construct the union of the contained `Const`s
- match t.get_type()?.as_const() {
- Some(k2) => k = max(k, k2),
- None => return Err(TypeError::new(InvalidFieldType(x, t))),
- }
- // Check for duplicated entries
- let entry = new_kts.entry(x);
- match &entry {
- Entry::Occupied(_) => {
- return Err(TypeError::new(RecordTypeDuplicateField))
- }
- Entry::Vacant(_) => entry.or_insert_with(|| t),
- };
- }
-
- Ok(Value::from_kind_and_type(
- ValueKind::RecordType(new_kts),
- Value::from_const(k),
- ))
-}
-
-fn tck_union_type<Iter>(kts: Iter) -> Result<Value, TypeError>
-where
- Iter: IntoIterator<Item = Result<(Label, Option<Value>), TypeError>>,
-{
- use std::collections::hash_map::Entry;
- use TypeMessage::*;
- let mut new_kts = HashMap::new();
- // Check that all types are the same const
- let mut k = None;
- for e in kts {
- let (x, t) = e?;
- if let Some(t) = &t {
- match (k, t.get_type()?.as_const()) {
- (None, Some(k2)) => k = Some(k2),
- (Some(k1), Some(k2)) if k1 == k2 => {}
- _ => {
- return Err(TypeError::new(InvalidFieldType(x, t.clone())))
- }
- }
- }
- let entry = new_kts.entry(x);
- match &entry {
- Entry::Occupied(_) => {
- return Err(TypeError::new(UnionTypeDuplicateField))
- }
- Entry::Vacant(_) => entry.or_insert_with(|| t),
- };
- }
-
- // An empty union type has type Type;
- // an union type with only unary variants also has type Type
- let k = k.unwrap_or(Const::Type);
-
- Ok(Value::from_kind_and_type(
- ValueKind::UnionType(new_kts),
- Value::from_const(k),
- ))
-}
-
-fn function_check(a: Const, b: Const) -> Const {
- if b == Const::Type {
- Const::Type
- } else {
- max(a, b)
- }
-}
-
pub(crate) fn const_to_value(c: Const) -> Value {
let v = ValueKind::Const(c);
match c {
@@ -289,511 +177,3 @@ pub(crate) fn builtin_to_value_env(b: Builtin, env: &NzEnv) -> Value {
.normalize_whnf_noenv(),
)
}
-
-/// Type-check an expression and return the expression alongside its type if type-checking
-/// succeeded, or an error if type-checking failed.
-/// Some normalization is done while typechecking, so the returned expression might be partially
-/// normalized as well.
-fn type_with(ctx: &TyCtx, e: Expr<Normalized>) -> Result<Value, TypeError> {
- use syntax::ExprKind::{Annot, Embed, Lam, Let, Pi, Var};
- let span = e.span();
-
- match e.as_ref() {
- Lam(var, annot, body) => {
- let binder = ctx.new_binder(var);
- let annot = type_with(ctx, annot.clone())?;
- annot.normalize_nf();
- let ctx2 = ctx.insert_type(&binder, annot.clone());
- let body = type_with(&ctx2, body.clone())?;
- let body_type = body.get_type()?;
- Ok(Value::from_kind_and_type(
- ValueKind::Lam(binder.clone(), annot.clone(), body),
- tck_pi_type(binder, annot, body_type)?,
- ))
- }
- Pi(x, ta, tb) => {
- let binder = ctx.new_binder(x);
- let ta = type_with(ctx, ta.clone())?;
- let ctx2 = ctx.insert_type(&binder, ta.clone());
- let tb = type_with(&ctx2, tb.clone())?;
- tck_pi_type(binder, ta, tb)
- }
- Let(x, t, v, e) => {
- let v = if let Some(t) = t {
- t.rewrap(Annot(v.clone(), t.clone()))
- } else {
- v.clone()
- };
-
- let v = type_with(ctx, v)?;
- let binder = ctx.new_binder(x);
- let e =
- type_with(&ctx.insert_value(&binder, v.clone())?, e.clone())?;
- // let e_ty = e.get_type()?;
- // Ok(Value::from_kind_and_type(
- // ValueKind::PartialExpr(ExprKind::Let(x.clone(), None, v, e)),
- // e_ty,
- // ))
- Ok(e)
- }
- Embed(p) => Ok(p.clone().into_value()),
- Var(var) => match ctx.lookup(&var) {
- Some(typed) => Ok(typed.clone()),
- None => Err(TypeError::new(TypeMessage::UnboundVariable(span))),
- },
- e => {
- // Typecheck recursively all subexpressions
- let expr = e.traverse_ref_with_special_handling_of_binders(
- |e| type_with(ctx, e.clone()),
- |_, _| unreachable!(),
- )?;
- type_last_layer(ctx, expr, span)
- }
- }
-}
-
-/// When all sub-expressions have been typed, check the remaining toplevel
-/// layer.
-fn type_last_layer(
- ctx: &TyCtx,
- e: ExprKind<Value, Normalized>,
- span: Span,
-) -> Result<Value, TypeError> {
- use syntax::BinOp::*;
- use syntax::Builtin::*;
- use syntax::Const::Type;
- let mkerr =
- |msg: &str| Err(TypeError::new(TypeMessage::Custom(msg.to_string())));
-
- /// Intermediary return type
- enum Ret {
- /// Returns the contained value as is
- RetWhole(Value),
- /// Returns the input expression `e` with the contained value as its type
- RetTypeOnly(Value),
- }
- use Ret::*;
-
- let ret = match &e {
- ExprKind::Import(_) => unreachable!(
- "There should remain no imports in a resolved expression"
- ),
- ExprKind::Lam(_, _, _)
- | ExprKind::Pi(_, _, _)
- | ExprKind::Let(_, _, _, _)
- | ExprKind::Embed(_)
- | ExprKind::Var(_) => unreachable!(),
- ExprKind::App(f, a) => {
- let tf = f.get_type()?;
- let tf_borrow = tf.as_whnf();
- match &*tf_borrow {
- ValueKind::Pi(_, tx, tb) => {
- if &a.get_type()? != tx {
- return mkerr("TypeMismatch");
- }
-
- let ret = tb.subst_shift(&AlphaVar::default(), a);
- ret.normalize_nf();
- RetTypeOnly(ret)
- }
- ValueKind::PiClosure { closure, .. } => {
- RetTypeOnly(closure.apply(a.clone()))
- }
- _ => return mkerr("NotAFunction"),
- }
- }
- ExprKind::Annot(x, t) => {
- if &x.get_type()? != t {
- return mkerr("AnnotMismatch");
- }
- RetWhole(x.clone())
- }
- ExprKind::Assert(t) => {
- match &*t.as_whnf() {
- ValueKind::Equivalence(x, y) if x == y => {}
- ValueKind::Equivalence(..) => return mkerr("AssertMismatch"),
- _ => return mkerr("AssertMustTakeEquivalence"),
- }
- RetTypeOnly(t.clone())
- }
- ExprKind::BoolIf(x, y, z) => {
- if *x.get_type()?.as_whnf() != ValueKind::from_builtin(Bool) {
- return mkerr("InvalidPredicate");
- }
-
- if y.get_type()?.get_type()?.as_const() != Some(Const::Type) {
- return mkerr("IfBranchMustBeTerm");
- }
-
- if z.get_type()?.get_type()?.as_const() != Some(Const::Type) {
- return mkerr("IfBranchMustBeTerm");
- }
-
- if y.get_type()? != z.get_type()? {
- return mkerr("IfBranchMismatch");
- }
-
- RetTypeOnly(y.get_type()?)
- }
- ExprKind::EmptyListLit(t) => {
- let arg = match &*t.as_whnf() {
- ValueKind::AppliedBuiltin(
- syntax::Builtin::List,
- args,
- _,
- _,
- ) if args.len() == 1 => args[0].clone(),
- _ => return mkerr("InvalidListType"),
- };
- RetWhole(Value::from_kind_and_type(
- ValueKind::EmptyListLit(arg),
- t.clone(),
- ))
- }
- ExprKind::NEListLit(xs) => {
- let mut iter = xs.iter().enumerate();
- let (_, x) = iter.next().unwrap();
- for (_, y) in iter {
- if x.get_type()? != y.get_type()? {
- return mkerr("InvalidListElement");
- }
- }
- let t = x.get_type()?;
- if t.get_type()?.as_const() != Some(Const::Type) {
- return mkerr("InvalidListType");
- }
-
- RetTypeOnly(Value::from_builtin(syntax::Builtin::List).app(t))
- }
- ExprKind::SomeLit(x) => {
- let t = x.get_type()?;
- if t.get_type()?.as_const() != Some(Const::Type) {
- return mkerr("InvalidOptionalType");
- }
-
- RetTypeOnly(Value::from_builtin(syntax::Builtin::Optional).app(t))
- }
- ExprKind::RecordType(kts) => RetWhole(tck_record_type(
- kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
- )?),
- ExprKind::UnionType(kts) => RetWhole(tck_union_type(
- kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
- )?),
- ExprKind::RecordLit(kvs) => RetTypeOnly(tck_record_type(
- kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))),
- )?),
- ExprKind::Field(r, x) => {
- match &*r.get_type()?.as_whnf() {
- ValueKind::RecordType(kts) => match kts.get(&x) {
- Some(tth) => RetTypeOnly(tth.clone()),
- None => return mkerr("MissingRecordField"),
- },
- // TODO: branch here only when r.get_type() is a Const
- _ => {
- match &*r.as_whnf() {
- ValueKind::UnionType(kts) => match kts.get(&x) {
- // Constructor has type T -> < x: T, ... >
- Some(Some(t)) => RetTypeOnly(tck_pi_type(
- ctx.new_binder(x),
- t.clone(),
- r.under_binder(),
- )?),
- Some(None) => RetTypeOnly(r.clone()),
- None => return mkerr("MissingUnionField"),
- },
- _ => return mkerr("NotARecord"),
- }
- } // _ => mkerr("NotARecord"),
- }
- }
- ExprKind::Const(c) => RetWhole(const_to_value(*c)),
- ExprKind::Builtin(b) => RetWhole(builtin_to_value(*b)),
- ExprKind::BoolLit(_) => RetTypeOnly(builtin_to_value(Bool)),
- ExprKind::NaturalLit(_) => RetTypeOnly(builtin_to_value(Natural)),
- ExprKind::IntegerLit(_) => RetTypeOnly(builtin_to_value(Integer)),
- ExprKind::DoubleLit(_) => RetTypeOnly(builtin_to_value(Double)),
- ExprKind::TextLit(interpolated) => {
- let text_type = builtin_to_value(Text);
- for contents in interpolated.iter() {
- use InterpolatedTextContents::Expr;
- if let Expr(x) = contents {
- if x.get_type()? != text_type {
- return mkerr("InvalidTextInterpolation");
- }
- }
- }
- RetTypeOnly(text_type)
- }
- ExprKind::BinOp(RightBiasedRecordMerge, l, r) => {
- let l_type = l.get_type()?;
- let r_type = r.get_type()?;
-
- // Extract the LHS record type
- let l_type_borrow = l_type.as_whnf();
- let kts_x = match &*l_type_borrow {
- ValueKind::RecordType(kts) => kts,
- _ => return mkerr("MustCombineRecord"),
- };
-
- // Extract the RHS record type
- let r_type_borrow = r_type.as_whnf();
- let kts_y = match &*r_type_borrow {
- ValueKind::RecordType(kts) => kts,
- _ => return mkerr("MustCombineRecord"),
- };
-
- // Union the two records, prefering
- // the values found in the RHS.
- let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, _, r_t| {
- Ok(r_t.clone())
- })?;
-
- // Construct the final record type from the union
- RetTypeOnly(tck_record_type(
- kts.into_iter().map(|(x, v)| Ok((x.clone(), v))),
- )?)
- }
- ExprKind::BinOp(RecursiveRecordMerge, l, r) => {
- RetTypeOnly(type_last_layer(
- ctx,
- ExprKind::BinOp(
- RecursiveRecordTypeMerge,
- l.get_type()?,
- r.get_type()?,
- ),
- Span::Artificial,
- )?)
- }
- ExprKind::BinOp(RecursiveRecordTypeMerge, l, r) => {
- // Extract the LHS record type
- let borrow_l = l.as_whnf();
- let kts_x = match &*borrow_l {
- ValueKind::RecordType(kts) => kts,
- _ => return mkerr("RecordTypeMergeRequiresRecordType"),
- };
-
- // Extract the RHS record type
- let borrow_r = r.as_whnf();
- let kts_y = match &*borrow_r {
- ValueKind::RecordType(kts) => kts,
- _ => return mkerr("RecordTypeMergeRequiresRecordType"),
- };
-
- // Ensure that the records combine without a type error
- let kts = merge_maps(
- kts_x,
- kts_y,
- // If the Label exists for both records, then we hit the recursive case.
- |_, l: &Value, r: &Value| {
- type_last_layer(
- ctx,
- ExprKind::BinOp(
- RecursiveRecordTypeMerge,
- l.clone(),
- r.clone(),
- ),
- Span::Artificial,
- )
- },
- )?;
-
- RetWhole(tck_record_type(kts.into_iter().map(Ok))?)
- }
- ExprKind::BinOp(ListAppend, l, r) => {
- match &*l.get_type()?.as_whnf() {
- ValueKind::AppliedBuiltin(List, _, _, _) => {}
- _ => return mkerr("BinOpTypeMismatch"),
- }
-
- if l.get_type()? != r.get_type()? {
- return mkerr("BinOpTypeMismatch");
- }
-
- RetTypeOnly(l.get_type()?)
- }
- ExprKind::BinOp(Equivalence, l, r) => {
- if l.get_type()?.get_type()?.as_const() != Some(Const::Type) {
- return mkerr("EquivalenceArgumentMustBeTerm");
- }
- if r.get_type()?.get_type()?.as_const() != Some(Const::Type) {
- return mkerr("EquivalenceArgumentMustBeTerm");
- }
-
- if l.get_type()? != r.get_type()? {
- return mkerr("EquivalenceTypeMismatch");
- }
-
- RetWhole(Value::from_kind_and_type(
- ValueKind::Equivalence(l.clone(), r.clone()),
- Value::from_const(Type),
- ))
- }
- ExprKind::BinOp(o, l, r) => {
- let t = builtin_to_value(match o {
- BoolAnd => Bool,
- BoolOr => Bool,
- BoolEQ => Bool,
- BoolNE => Bool,
- NaturalPlus => Natural,
- NaturalTimes => Natural,
- TextAppend => Text,
- ListAppend => unreachable!(),
- RightBiasedRecordMerge => unreachable!(),
- RecursiveRecordMerge => unreachable!(),
- RecursiveRecordTypeMerge => unreachable!(),
- ImportAlt => unreachable!("There should remain no import alternatives in a resolved expression"),
- Equivalence => unreachable!(),
- });
-
- if l.get_type()? != t {
- return mkerr("BinOpTypeMismatch");
- }
-
- if r.get_type()? != t {
- return mkerr("BinOpTypeMismatch");
- }
-
- RetTypeOnly(t)
- }
- ExprKind::Merge(record, union, type_annot) => {
- let record_type = record.get_type()?;
- let record_borrow = record_type.as_whnf();
- let handlers = match &*record_borrow {
- ValueKind::RecordType(kts) => kts,
- _ => return mkerr("Merge1ArgMustBeRecord"),
- };
-
- let union_type = union.get_type()?;
- let union_borrow = union_type.as_whnf();
- let variants = match &*union_borrow {
- ValueKind::UnionType(kts) => Cow::Borrowed(kts),
- ValueKind::AppliedBuiltin(
- syntax::Builtin::Optional,
- args,
- _,
- _,
- ) if args.len() == 1 => {
- let ty = &args[0];
- let mut kts = HashMap::new();
- kts.insert("None".into(), None);
- kts.insert("Some".into(), Some(ty.clone()));
- Cow::Owned(kts)
- }
- _ => return mkerr("Merge2ArgMustBeUnionOrOptional"),
- };
-
- let mut inferred_type = None;
- for (x, handler_type) in handlers {
- let handler_return_type =
- match variants.get(x) {
- // Union alternative with type
- Some(Some(variant_type)) => {
- let handler_type_borrow = handler_type.as_whnf();
- let (tx, tb) = match &*handler_type_borrow {
- ValueKind::Pi(_, tx, tb) => (tx, tb),
- _ => return mkerr("NotAFunction"),
- };
-
- if variant_type != tx {
- return mkerr("TypeMismatch");
- }
-
- // Extract `tb` from under the binder. Fails if the variable was used
- // in `tb`.
- match tb.over_binder() {
- Some(x) => x,
- None => return mkerr(
- "MergeHandlerReturnTypeMustNotBeDependent",
- ),
- }
- }
- // Union alternative without type
- Some(None) => handler_type.clone(),
- None => return mkerr("MergeHandlerMissingVariant"),
- };
- match &inferred_type {
- None => inferred_type = Some(handler_return_type),
- Some(t) => {
- if t != &handler_return_type {
- return mkerr("MergeHandlerTypeMismatch");
- }
- }
- }
- }
- for x in variants.keys() {
- if !handlers.contains_key(x) {
- return mkerr("MergeVariantMissingHandler");
- }
- }
-
- match (inferred_type, type_annot.as_ref()) {
- (Some(t1), Some(t2)) => {
- if &t1 != t2 {
- return mkerr("MergeAnnotMismatch");
- }
- RetTypeOnly(t1)
- }
- (Some(t), None) => RetTypeOnly(t),
- (None, Some(t)) => RetTypeOnly(t.clone()),
- (None, None) => return mkerr("MergeEmptyNeedsAnnotation"),
- }
- }
- ExprKind::ToMap(_, _) => unimplemented!("toMap"),
- ExprKind::Projection(record, labels) => {
- let record_type = record.get_type()?;
- let record_type_borrow = record_type.as_whnf();
- let kts = match &*record_type_borrow {
- ValueKind::RecordType(kts) => kts,
- _ => return mkerr("ProjectionMustBeRecord"),
- };
-
- let mut new_kts = HashMap::new();
- for l in labels {
- match kts.get(l) {
- None => return mkerr("ProjectionMissingEntry"),
- Some(t) => {
- use std::collections::hash_map::Entry;
- match new_kts.entry(l.clone()) {
- Entry::Occupied(_) => {
- return mkerr("ProjectionDuplicateField")
- }
- Entry::Vacant(e) => e.insert(t.clone()),
- }
- }
- };
- }
-
- RetTypeOnly(Value::from_kind_and_type(
- ValueKind::RecordType(new_kts),
- record_type.get_type()?,
- ))
- }
- ExprKind::ProjectionByExpr(_, _) => {
- unimplemented!("selection by expression")
- }
- ExprKind::Completion(_, _) => unimplemented!("record completion"),
- };
-
- Ok(match ret {
- RetTypeOnly(typ) => Value::from_kind_and_type_and_span(
- ValueKind::PartialExpr(e),
- typ,
- span,
- ),
- RetWhole(v) => v.with_span(span),
- })
-}
-
-/// `type_of` is the same as `type_with` with an empty context, meaning that the
-/// expression must be closed (i.e. no free variables), otherwise type-checking
-/// will fail.
-pub(crate) fn typecheck(e: Expr<Normalized>) -> Result<Value, TypeError> {
- type_with(&TyCtx::new(), e)
-}
-
-pub(crate) fn typecheck_with(
- expr: Expr<Normalized>,
- ty: Expr<Normalized>,
-) -> Result<Value, TypeError> {
- typecheck(expr.rewrap(ExprKind::Annot(expr.clone(), ty)))
-}
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index e4108ad..abb6fa8 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,4 +1,3 @@
-#![allow(dead_code)]
use crate::error::{TypeError, TypeMessage};
use crate::semantics::core::var::AlphaVar;
use crate::semantics::phase::normalize::{normalize_tyexpr_whnf, NzEnv};
@@ -58,10 +57,6 @@ impl TyExpr {
let mut env = env.iter().collect();
tyexpr_to_expr(self, opts, &mut env)
}
- // TODO: temporary hack
- pub fn to_value(&self) -> Value {
- todo!()
- }
pub fn normalize_whnf(&self, env: &NzEnv) -> Value {
normalize_tyexpr_whnf(self, env)
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index abb36e1..99eb31f 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -1,12 +1,8 @@
-#![allow(dead_code)]
-#![allow(unreachable_code)]
-#![allow(unused_imports)]
use std::borrow::Cow;
use std::cmp::max;
use std::collections::HashMap;
use crate::error::{TypeError, TypeMessage};
-use crate::semantics::core::context::TyCtx;
use crate::semantics::nze::{NameEnv, NzVar, QuoteEnv};
use crate::semantics::phase::normalize::{merge_maps, NzEnv};
use crate::semantics::phase::typecheck::{
@@ -14,12 +10,12 @@ use crate::semantics::phase::typecheck::{
};
use crate::semantics::phase::Normalized;
use crate::semantics::{
- AlphaVar, Binder, Closure, TyExpr, TyExprKind, Type, Value, ValueKind,
+ Binder, Closure, TyExpr, TyExprKind, Type, Value, ValueKind,
};
use crate::syntax;
use crate::syntax::{
BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label,
- Span, UnspannedExpr, V,
+ Span, V,
};
#[derive(Debug, Clone)]
@@ -111,6 +107,8 @@ fn mkerr<T>(x: impl ToString) -> Result<T, TypeError> {
Err(TypeError::new(TypeMessage::Custom(x.to_string())))
}
+/// When all sub-expressions have been typed, check the remaining toplevel
+/// layer.
fn type_one_layer(
env: &TyEnv,
kind: &ExprKind<TyExpr, Normalized>,
@@ -503,20 +501,6 @@ fn type_one_layer(
Some(Some(variant_type)) => {
let handler_type_borrow = handler_type.as_whnf();
match &*handler_type_borrow {
- ValueKind::Pi(_, tx, tb) => {
- if variant_type != tx {
- return mkerr("MergeHandlerTypeMismatch");
- }
-
- // Extract `tb` from under the binder. Fails if the variable was used
- // in `tb`.
- match tb.over_binder() {
- Some(x) => x,
- None => return mkerr(
- "MergeHandlerReturnTypeMustNotBeDependent",
- ),
- }
- }
ValueKind::PiClosure { closure, annot, .. } => {
if variant_type != annot {
// return mkerr("MergeHandlerTypeMismatch");
@@ -609,8 +593,7 @@ fn type_one_layer(
})
}
-/// Type-check an expression and return the expression alongside its type if type-checking
-/// succeeded, or an error if type-checking failed.
+/// `type_with` typechecks an expressio in the provided environment.
pub(crate) fn type_with(
env: &TyEnv,
expr: &Expr<Normalized>,
@@ -689,10 +672,13 @@ pub(crate) fn type_with(
Ok(TyExpr::new(tyekind, ty, expr.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> {
type_with(&TyEnv::new(), e)
}
+/// 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>,
diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index dbe233b..0da617b 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -330,10 +330,6 @@ impl<Label: PartialEq + Clone> V<Label> {
V(y.clone(), *m)
})
}
-
- pub(crate) fn over_binder(&self, x: &Label) -> Option<Self> {
- self.shift(-1, &V(x.clone(), 0))
- }
}
pub fn trivial_result<T>(x: Result<T, !>) -> T {