From 654d752c65f0e221d225ed045a0aee62f223855e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 27 Dec 2019 16:05:47 +0000 Subject: Introduce a notion of binder --- dhall/src/semantics/core/context.rs | 25 +++++++++++++++++-------- dhall/src/semantics/core/value.rs | 8 ++++---- dhall/src/semantics/core/var.rs | 34 +++++++++++++++++----------------- dhall/src/semantics/core/visitor.rs | 8 ++++---- dhall/src/semantics/phase/typecheck.rs | 27 ++++++++++++++------------- 5 files changed, 56 insertions(+), 46 deletions(-) (limited to 'dhall/src') 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 { + pub fn insert_value( + &self, + x: &Binder, + e: Value, + ) -> Result { 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