diff options
Diffstat (limited to 'dhall/src/semantics/core')
| -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 |
3 files changed, 0 insertions, 135 deletions
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, |