diff options
Diffstat (limited to 'dhall/src/semantics')
-rw-r--r-- | dhall/src/semantics/core/context.rs | 25 | ||||
-rw-r--r-- | dhall/src/semantics/core/value.rs | 8 | ||||
-rw-r--r-- | dhall/src/semantics/core/var.rs | 34 | ||||
-rw-r--r-- | dhall/src/semantics/core/visitor.rs | 8 | ||||
-rw-r--r-- | dhall/src/semantics/phase/typecheck.rs | 27 |
5 files changed, 56 insertions, 46 deletions
diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index ed63b63..3a7930e 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -3,7 +3,7 @@ use std::collections::HashMap; use crate::error::TypeError; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::{AlphaVar, Shift, Subst}; +use crate::semantics::core::var::{AlphaVar, Binder, Shift, Subst}; use crate::syntax::{Label, V}; #[derive(Debug, Clone)] @@ -14,22 +14,26 @@ enum CtxItem { #[derive(Debug, Clone)] pub(crate) struct TyCtx { - ctx: Vec<(Label, CtxItem)>, + ctx: Vec<(Binder, CtxItem)>, } impl TyCtx { pub fn new() -> Self { TyCtx { ctx: Vec::new() } } - fn with_vec(&self, vec: Vec<(Label, CtxItem)>) -> Self { + fn with_vec(&self, vec: Vec<(Binder, CtxItem)>) -> Self { TyCtx { ctx: vec } } - pub fn insert_type(&self, x: &Label, t: Value) -> Self { + pub fn insert_type(&self, x: &Binder, t: Value) -> Self { let mut vec = self.ctx.clone(); vec.push((x.clone(), CtxItem::Kept(x.into(), t.under_binder(x)))); self.with_vec(vec) } - pub fn insert_value(&self, x: &Label, e: Value) -> Result<Self, TypeError> { + 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)) @@ -37,8 +41,9 @@ impl TyCtx { pub fn lookup(&self, var: &V<Label>) -> Option<Value> { let mut var = var.clone(); let mut shift_map: HashMap<Label, _> = HashMap::new(); - for (l, i) in self.ctx.iter().rev() { - match var.over_binder(l) { + for (b, i) in self.ctx.iter().rev() { + let l = b.to_label(); + match var.over_binder(&l) { None => { let i = i.under_multiple_binders(&shift_map); return Some(match i { @@ -51,12 +56,16 @@ impl TyCtx { Some(newvar) => var = newvar, }; if let CtxItem::Kept(_, _) = i { - *shift_map.entry(l.clone()).or_insert(0) += 1; + *shift_map.entry(l).or_insert(0) += 1; } } // Unbound variable None } + pub fn new_binder(&self, l: &Label) -> Binder { + Binder::new(l.clone()) + } + /// Given a var that makes sense in the current context, map the given function in such a way /// that the passed variable always makes sense in the context of the passed item. /// Once we pass the variable definition, the variable doesn't make sense anymore so we just diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index f7c2fbf..687fcfe 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -4,7 +4,7 @@ use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TyCtx; -use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; +use crate::semantics::core::var::{AlphaVar, Binder, Shift, Subst}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; use crate::semantics::phase::{Normalized, NormalizedExpr, Typed}; @@ -54,8 +54,8 @@ pub(crate) enum Form { #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) enum ValueKind<Value> { /// Closures - Lam(AlphaLabel, Value, Value), - Pi(AlphaLabel, Value, Value), + Lam(Binder, Value, Value), + Pi(Binder, Value, Value), // Invariant: in whnf, the evaluation must not be able to progress further. AppliedBuiltin(Builtin, Vec<Value>), @@ -393,7 +393,7 @@ impl<V> ValueKind<V> { pub(crate) fn map_ref_with_special_handling_of_binders<'a, V2>( &'a self, mut map_val: impl FnMut(&'a V) -> V2, - mut map_under_binder: impl FnMut(&'a AlphaLabel, &'a V) -> V2, + mut map_under_binder: impl FnMut(&'a Binder, &'a V) -> V2, ) -> ValueKind<V2> { use crate::semantics::visitor; use crate::syntax::trivial_result; diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs index 017a689..add0500 100644 --- a/dhall/src/semantics/core/var.rs +++ b/dhall/src/semantics/core/var.rs @@ -14,7 +14,9 @@ pub struct AlphaVar { // Exactly like a Label, but equality returns always true. // This is so that ValueKind equality is exactly alpha-equivalence. #[derive(Clone, Eq)] -pub struct AlphaLabel(Label); +pub struct Binder { + name: Label, +} pub(crate) trait Shift: Sized { // Shift an expression to move it around binders without changing the meaning of its free @@ -64,7 +66,10 @@ impl AlphaVar { } } -impl AlphaLabel { +impl Binder { + pub(crate) fn new(name: Label) -> Self { + Binder { name } + } pub(crate) fn to_label_maybe_alpha(&self, alpha: bool) -> Label { if alpha { "_".into() @@ -92,7 +97,7 @@ impl std::cmp::PartialEq for AlphaVar { self.alpha == other.alpha } } -impl std::cmp::PartialEq for AlphaLabel { +impl std::cmp::PartialEq for Binder { fn eq(&self, _other: &Self) -> bool { true } @@ -104,9 +109,9 @@ impl std::fmt::Debug for AlphaVar { } } -impl std::fmt::Debug for AlphaLabel { +impl std::fmt::Debug for Binder { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!(f, "AlphaLabel({})", &self.0) + write!(f, "Binder({})", &self.name) } } @@ -123,26 +128,21 @@ impl<'a> From<&'a Label> for AlphaVar { x.clone().into() } } -impl From<AlphaLabel> for AlphaVar { - fn from(x: AlphaLabel) -> AlphaVar { +impl From<Binder> for AlphaVar { + fn from(x: Binder) -> AlphaVar { let l: Label = x.into(); l.into() } } -impl<'a> From<&'a AlphaLabel> for AlphaVar { - fn from(x: &'a AlphaLabel) -> AlphaVar { +impl<'a> From<&'a Binder> for AlphaVar { + fn from(x: &'a Binder) -> AlphaVar { x.clone().into() } } -impl From<Label> for AlphaLabel { - fn from(x: Label) -> AlphaLabel { - AlphaLabel(x) - } -} -impl From<AlphaLabel> for Label { - fn from(x: AlphaLabel) -> Label { - x.0 +impl From<Binder> for Label { + fn from(x: Binder) -> Label { + x.name } } impl Shift for () { diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs index c7cf79e..2c9ba92 100644 --- a/dhall/src/semantics/core/visitor.rs +++ b/dhall/src/semantics/core/visitor.rs @@ -1,6 +1,6 @@ use std::iter::FromIterator; -use crate::semantics::{AlphaLabel, ValueKind}; +use crate::semantics::{Binder, ValueKind}; use crate::syntax::Label; /// A visitor trait that can be used to traverse `ValueKind`s. We need this pattern so that Rust lets @@ -12,7 +12,7 @@ pub(crate) trait ValueKindVisitor<'a, V1, V2>: Sized { fn visit_val(&mut self, val: &'a V1) -> Result<V2, Self::Error>; fn visit_val_under_binder( mut self, - _label: &'a AlphaLabel, + _label: &'a Binder, val: &'a V1, ) -> Result<V2, Self::Error> { self.visit_val(val) @@ -117,7 +117,7 @@ impl<'a, V1, V2, Err, F1, F2> ValueKindVisitor<'a, V1, V2> where V1: 'a, F1: FnMut(&'a V1) -> Result<V2, Err>, - F2: FnOnce(&'a AlphaLabel, &'a V1) -> Result<V2, Err>, + F2: FnOnce(&'a Binder, &'a V1) -> Result<V2, Err>, { type Error = Err; @@ -126,7 +126,7 @@ where } fn visit_val_under_binder( self, - label: &'a AlphaLabel, + label: &'a Binder, val: &'a V1, ) -> Result<V2, Self::Error> { (self.visit_under_binder)(label, val) diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 2e1cc02..926598d 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -4,11 +4,9 @@ use std::collections::HashMap; use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TyCtx; -use crate::semantics::core::value::Value; -use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::{Shift, Subst}; use crate::semantics::phase::normalize::merge_maps; use crate::semantics::phase::Normalized; +use crate::semantics::{Binder, Shift, Subst, Value, ValueKind}; use crate::syntax; use crate::syntax::{ Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span, @@ -17,12 +15,12 @@ use crate::syntax::{ fn tck_pi_type( ctx: &TyCtx, - x: Label, + binder: Binder, tx: Value, te: Value, ) -> Result<Value, TypeError> { use TypeMessage::*; - let ctx2 = ctx.insert_type(&x, tx.clone()); + let ctx2 = ctx.insert_type(&binder, tx.clone()); let ka = match tx.get_type()?.as_const() { Some(k) => k, @@ -42,7 +40,7 @@ fn tck_pi_type( let k = function_check(ka, kb); Ok(Value::from_kind_and_type( - ValueKind::Pi(x.into(), tx, te), + ValueKind::Pi(binder, tx, te), Value::from_const(k), )) } @@ -307,21 +305,23 @@ fn type_with(ctx: &TyCtx, e: Expr<Normalized>) -> Result<Value, TypeError> { match e.as_ref() { Lam(var, annot, body) => { + let binder = ctx.new_binder(var); let annot = type_with(ctx, annot.clone())?; annot.normalize_nf(); - let ctx2 = ctx.insert_type(var, annot.clone()); + let ctx2 = ctx.insert_type(&binder, annot.clone()); let body = type_with(&ctx2, body.clone())?; let body_type = body.get_type()?; Ok(Value::from_kind_and_type( - ValueKind::Lam(var.clone().into(), annot.clone(), body), - tck_pi_type(ctx, var.clone(), annot, body_type)?, + ValueKind::Lam(binder.clone(), annot.clone(), body), + tck_pi_type(ctx, binder, annot, body_type)?, )) } Pi(x, ta, tb) => { + let binder = ctx.new_binder(x); let ta = type_with(ctx, ta.clone())?; - let ctx2 = ctx.insert_type(x, ta.clone()); + let ctx2 = ctx.insert_type(&binder, ta.clone()); let tb = type_with(&ctx2, tb.clone())?; - tck_pi_type(ctx, x.clone(), ta, tb) + tck_pi_type(ctx, binder, ta, tb) } Let(x, t, v, e) => { let v = if let Some(t) = t { @@ -331,7 +331,8 @@ fn type_with(ctx: &TyCtx, e: Expr<Normalized>) -> Result<Value, TypeError> { }; let v = type_with(ctx, v)?; - type_with(&ctx.insert_value(x, v.clone())?, e.clone()) + let binder = ctx.new_binder(x); + type_with(&ctx.insert_value(&binder, v.clone())?, e.clone()) } Embed(p) => Ok(p.clone().into_typed().into_value()), Var(var) => match ctx.lookup(&var) { @@ -496,7 +497,7 @@ fn type_last_layer( RetTypeOnly( tck_pi_type( ctx, - x.clone(), + ctx.new_binder(x), t.clone(), r.under_binder(x), )? |