summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/lib.rs1
-rw-r--r--dhall/src/normalize.rs54
-rw-r--r--dhall/src/typecheck.rs61
-rw-r--r--dhall_core/src/core.rs34
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| {
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 03:32:48 +0000