summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/core/context.rs25
-rw-r--r--dhall/src/semantics/core/value.rs8
-rw-r--r--dhall/src/semantics/core/var.rs34
-rw-r--r--dhall/src/semantics/core/visitor.rs8
-rw-r--r--dhall/src/semantics/phase/typecheck.rs27
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),
)?
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 05:13:58 +0000