diff options
| -rw-r--r-- | dhall/src/lib.rs | 1 | ||||
| -rw-r--r-- | dhall/src/normalize.rs | 54 | ||||
| -rw-r--r-- | dhall/src/typecheck.rs | 61 | ||||
| -rw-r--r-- | dhall_core/src/core.rs | 34 |
4 files changed, 112 insertions, 38 deletions
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index c85b962..3860890 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -4,6 +4,7 @@ #![feature(label_break_value)] #![feature(non_exhaustive)] #![feature(bind_by_move_pattern_guards)] +#![feature(try_trait)] #![cfg_attr(test, feature(custom_inner_attributes))] #![allow( clippy::type_complexity, diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 7aa8686..c17ed78 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -229,7 +229,21 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF { #[derive(Debug, Clone)] enum EnvItem { Expr(WHNF), - Skip(usize), + Skip(V<Label>), +} + +impl EnvItem { + fn shift0(&self, delta: isize, x: &Label) -> Self { + use EnvItem::*; + match self { + Expr(e) => { + let mut e = e.clone(); + e.shift0(delta, x); + Expr(e) + } + Skip(var) => Skip(var.shift0(delta, x)), + } + } } #[derive(Debug, Clone)] @@ -247,30 +261,36 @@ impl NormalizationContext { fn skip(&self, x: &Label) -> Self { NormalizationContext(Rc::new( self.0 - .map(|l, e| { - use EnvItem::*; - match e { - Expr(e) => { - let mut e = e.clone(); - e.shift0(1, x); - Expr(e) - } - Skip(n) if l == x => Skip(*n + 1), - Skip(n) => Skip(*n), - } - }) - .insert(x.clone(), EnvItem::Skip(0)), + .map(|_, e| e.shift0(1, x)) + .insert(x.clone(), EnvItem::Skip(V(x.clone(), 0))), )) } fn lookup(&self, var: &V<Label>) -> WHNF { let V(x, n) = var; match self.0.lookup(x, *n) { Some(EnvItem::Expr(e)) => e.clone(), - Some(EnvItem::Skip(m)) => { - WHNF::Expr(rc(ExprF::Var(V(x.clone(), *m)))) + Some(EnvItem::Skip(newvar)) => { + WHNF::Expr(rc(ExprF::Var(newvar.clone()))) + } + None => WHNF::Expr(rc(ExprF::Var(var.clone()))), + } + } + fn from_typecheck_ctx(tc_ctx: &crate::typecheck::TypecheckContext) -> Self { + use crate::typecheck::EnvItem::*; + let mut ctx = Context::new(); + for (k, vs) in tc_ctx.0.iter_keys() { + for v in vs.iter().rev() { + let new_item = match v { + Type(var, _) => EnvItem::Skip(var.clone()), + Value(e) => EnvItem::Expr(normalize_whnf( + NormalizationContext::new(), + e.as_expr().embed_absurd(), + )), + }; + ctx = ctx.insert(k.clone(), new_item); } - None => WHNF::Expr(rc(ExprF::Var(V(x.clone(), *n)))), } + NormalizationContext(Rc::new(ctx)) } } diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index a183944..e3ec849 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -3,6 +3,7 @@ use std::borrow::Borrow; use std::borrow::Cow; use std::fmt; use std::marker::PhantomData; +use std::rc::Rc; use crate::expr::*; use crate::traits::DynamicType; @@ -138,18 +139,56 @@ impl<'a> TypeInternal<'a> { } #[derive(Debug, Clone)] -pub(crate) struct TypecheckContext(Context<Label, Type<'static>>); +pub(crate) enum EnvItem { + Type(V<Label>, Type<'static>), + Value(Normalized<'static>), +} + +impl EnvItem { + fn shift0(&self, delta: isize, x: &Label) -> Self { + use EnvItem::*; + match self { + Type(v, e) => Type(v.shift0(delta, x), e.shift0(delta, x)), + Value(e) => Value(e.shift0(delta, x)), + } + } +} + +#[derive(Debug, Clone)] +pub(crate) struct TypecheckContext(pub(crate) Context<Label, EnvItem>); impl TypecheckContext { pub(crate) fn new() -> Self { TypecheckContext(Context::new()) } - pub(crate) fn insert_and_shift(&self, x: &Label, t: Type<'static>) -> Self { - TypecheckContext(self.0.insert(x.clone(), t).map(|_, e| e.shift0(1, x))) + pub(crate) fn insert_type(&self, x: &Label, t: Type<'static>) -> Self { + TypecheckContext( + self.0 + .insert(x.clone(), EnvItem::Type(V(x.clone(), 0), t)) + .map(|_, e| e.shift0(1, x)), + ) + } + pub(crate) fn insert_value( + &self, + x: &Label, + t: Normalized<'static>, + ) -> Self { + TypecheckContext( + self.0 + .insert(x.clone(), EnvItem::Value(t)) + .map(|_, e| e.shift0(1, x)), + ) } - pub(crate) fn lookup(&self, var: &V<Label>) -> Option<&Type<'static>> { + pub(crate) fn lookup( + &self, + var: &V<Label>, + ) -> Option<Cow<'_, Type<'static>>> { let V(x, n) = var; - self.0.lookup(x, *n) + match self.0.lookup(x, *n) { + Some(EnvItem::Type(_, t)) => Some(Cow::Borrowed(&t)), + Some(EnvItem::Value(t)) => Some(t.get_type()?), + None => None, + } } } @@ -416,7 +455,7 @@ fn type_with( let ret = match e.as_ref() { Lam(x, t, b) => { let t = mktype(ctx, t.clone())?; - let ctx2 = ctx.insert_and_shift(x, t.clone()); + let ctx2 = ctx.insert_type(x, t.clone()); let b = type_with(&ctx2, b.clone())?; Ok(RetExpr(Pi( x.clone(), @@ -431,7 +470,7 @@ fn type_with( mkerr(InvalidInputType(ta.into_normalized()?)), ); - let ctx2 = ctx.insert_and_shift(x, ta.clone()); + let ctx2 = ctx.insert_type(x, ta.clone()); let tb = type_with(&ctx2, tb.clone())?; let kB = ensure_is_const!( &tb.get_type()?, @@ -507,7 +546,7 @@ fn type_last_layer( Let(_, _, _, _) => unreachable!(), Embed(_) => unreachable!(), Var(var) => match ctx.lookup(&var) { - Some(e) => Ok(RetType(e.clone())), + Some(e) => Ok(RetType(e.into_owned())), None => Err(mkerr(UnboundVariable)), }, App(f, a) => { @@ -808,6 +847,12 @@ impl TypeError { } } +impl From<TypeError> for std::option::NoneError { + fn from(_: TypeError) -> std::option::NoneError { + std::option::NoneError + } +} + impl ::std::error::Error for TypeMessage<'static> { fn description(&self) -> &str { match *self { diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs index fa6fca4..03974eb 100644 --- a/dhall_core/src/core.rs +++ b/dhall_core/src/core.rs @@ -468,15 +468,24 @@ fn add_ui(u: usize, i: isize) -> usize { } } -/// Applies `shift` to a single var. -/// The first var is the var to shift away from; the second is the variable to shift -fn shift_var(delta: isize, var: &V<Label>, in_expr: &V<Label>) -> V<Label> { - let V(x, n) = var; - let V(y, m) = in_expr; - if x == y && n <= m { - V(y.clone(), add_ui(*m, delta)) - } else { - V(y.clone(), *m) +impl<Label: PartialEq + Clone> V<Label> { + pub fn shift(&self, delta: isize, var: &V<Label>) -> Self { + let V(x, n) = var; + let V(y, m) = self; + if x == y && n <= m { + V(y.clone(), add_ui(*m, delta)) + } else { + V(y.clone(), *m) + } + } + + pub fn shift0(&self, delta: isize, x: &Label) -> Self { + let V(y, m) = self; + if x == y { + V(y.clone(), add_ui(*m, delta)) + } else { + V(y.clone(), *m) + } } } @@ -492,12 +501,11 @@ pub fn shift<N, E>( ) -> SubExpr<N, E> { use crate::ExprF::*; match in_expr.as_ref() { - Var(v) => rc(Var(shift_var(delta, var, v))), + Var(v) => rc(Var(v.shift(delta, var))), _ => in_expr.map_subexprs_with_special_handling_of_binders( |e| shift(delta, var, e), |l: &Label, e| { - let vl = V(l.clone(), 0); - let newvar = shift_var(1, &vl, var); + let newvar = var.shift0(1, l); shift(delta, &newvar, e) }, ), @@ -567,7 +575,7 @@ fn subst_shift_inner<N, E>( let actual_var = V(x.clone(), add_ui(*n, *dn)); match in_expr.as_ref() { Var(v) if v == &actual_var => shift0_multiple(ctx, value), - Var(v) => rc(Var(shift_var(-1, &actual_var, v))), + Var(v) => rc(Var(v.shift(-1, &actual_var))), _ => in_expr.map_subexprs_with_special_handling_of_binders( |e| subst_shift_inner(ctx, var, value, e), |l: &Label, e| { |