diff options
Diffstat (limited to 'dhall/src')
| -rw-r--r-- | dhall/src/lib.rs | 1 | ||||
| -rw-r--r-- | dhall/src/normalize.rs | 54 | ||||
| -rw-r--r-- | dhall/src/typecheck.rs | 61 |
3 files changed, 91 insertions, 25 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 { |