diff options
Diffstat (limited to 'dhall')
| -rw-r--r-- | dhall/src/error/mod.rs | 17 | ||||
| -rw-r--r-- | dhall/src/semantics/core/context.rs | 95 | ||||
| -rw-r--r-- | dhall/src/semantics/core/value.rs | 32 | ||||
| -rw-r--r-- | dhall/src/semantics/core/visitor.rs | 8 | ||||
| -rw-r--r-- | dhall/src/semantics/nze/nzexpr.rs | 411 | ||||
| -rw-r--r-- | dhall/src/semantics/phase/normalize.rs | 7 | ||||
| -rw-r--r-- | dhall/src/semantics/phase/typecheck.rs | 624 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/tyexpr.rs | 5 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 30 | ||||
| -rw-r--r-- | dhall/src/syntax/ast/expr.rs | 4 |
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 { |