From 1741bb9e3fe872b3b841a9f394de69c85f523ba5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 16 Aug 2019 18:34:05 +0200 Subject: No need for generic Context anymore --- dhall/src/core/context.rs | 113 ++++++++++++++++------------------------------ 1 file changed, 38 insertions(+), 75 deletions(-) diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs index 3c07c1c..36542d2 100644 --- a/dhall/src/core/context.rs +++ b/dhall/src/core/context.rs @@ -10,46 +10,46 @@ use crate::error::TypeError; use crate::phase::{Type, Typed}; #[derive(Debug, Clone)] -enum CtxItem { - Kept(AlphaVar, T), - Replaced(Thunk, T), +enum CtxItem { + Kept(AlphaVar, Type), + Replaced(Thunk, Type), } #[derive(Debug, Clone)] -struct Context(Rc)>>); +pub(crate) struct TypecheckContext(Rc>); -#[derive(Debug, Clone)] -pub(crate) struct TypecheckContext(Context); - -impl Context { +impl TypecheckContext { pub fn new() -> Self { - Context(Rc::new(Vec::new())) + TypecheckContext(Rc::new(Vec::new())) } - pub fn insert_kept(&self, x: &Label, t: T) -> Self - where - T: Shift + Clone, - { + pub fn insert_type(&self, x: &Label, t: Type) -> Self { let mut vec = self.0.as_ref().clone(); vec.push((x.clone(), CtxItem::Kept(x.into(), t.under_binder(x)))); - Context(Rc::new(vec)) + TypecheckContext(Rc::new(vec)) } - pub fn insert_replaced(&self, x: &Label, th: Thunk, t: T) -> Self - where - T: Clone, - { + pub fn insert_value(&self, x: &Label, e: Typed) -> Result { let mut vec = self.0.as_ref().clone(); - vec.push((x.clone(), CtxItem::Replaced(th, t))); - Context(Rc::new(vec)) + vec.push(( + x.clone(), + CtxItem::Replaced(e.to_thunk(), e.get_type()?.into_owned()), + )); + Ok(TypecheckContext(Rc::new(vec))) } - pub fn lookup(&self, var: &V