summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/lib.rs1
-rw-r--r--dhall/src/normalize.rs54
-rw-r--r--dhall/src/typecheck.rs61
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 {