From db1375eccd1e6943b504cd54ed17eb8f4d19c25f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 6 Feb 2020 17:35:54 +0000 Subject: Remove most reliance on types stored in Value --- dhall/src/semantics/nze/env.rs | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) (limited to 'dhall/src/semantics/nze/env.rs') diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs index 0b22a8b..261e0b6 100644 --- a/dhall/src/semantics/nze/env.rs +++ b/dhall/src/semantics/nze/env.rs @@ -1,4 +1,4 @@ -use crate::semantics::{AlphaVar, Value, ValueKind}; +use crate::semantics::{AlphaVar, Type, Value, ValueKind}; #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub(crate) enum NzVar { @@ -11,9 +11,9 @@ pub(crate) enum NzVar { #[derive(Debug, Clone)] enum NzEnvItem { // Variable is bound with given type - Kept(Value), + Kept(Type), // Variable has been replaced by corresponding value - Replaced(Value), + Replaced(Value, Type), } #[derive(Debug, Clone)] @@ -49,28 +49,31 @@ impl NzEnv { NzEnv { items: Vec::new() } } - pub fn insert_type(&self, t: Value) -> Self { + pub fn insert_type(&self, ty: Type) -> Self { let mut env = self.clone(); - env.items.push(NzEnvItem::Kept(t)); + env.items.push(NzEnvItem::Kept(ty)); env } - pub fn insert_value(&self, e: Value) -> Self { + pub fn insert_value(&self, e: Value, ty: Type) -> Self { let mut env = self.clone(); - env.items.push(NzEnvItem::Replaced(e)); + env.items.push(NzEnvItem::Replaced(e, ty)); env } + pub fn insert_value_noty(&self, e: Value) -> Self { + let ty = e.get_type_not_sort(); + self.insert_value(e, ty) + } pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind { let idx = self.items.len() - 1 - var.idx(); match &self.items[idx] { NzEnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)), - NzEnvItem::Replaced(x) => x.kind().clone(), + NzEnvItem::Replaced(x, _) => x.kind().clone(), } } pub fn lookup_ty(&self, var: &AlphaVar) -> Value { let idx = self.items.len() - 1 - var.idx(); match &self.items[idx] { - NzEnvItem::Kept(ty) => ty.clone(), - NzEnvItem::Replaced(x) => x.get_type().unwrap(), + NzEnvItem::Kept(ty) | NzEnvItem::Replaced(_, ty) => ty.clone(), } } } -- cgit v1.2.3 From ad085a20bc257d03a52708d920cfc65f0e9051e6 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 22:07:03 +0000 Subject: Remove all types from Value --- dhall/src/semantics/nze/env.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'dhall/src/semantics/nze/env.rs') diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs index 261e0b6..ff52343 100644 --- a/dhall/src/semantics/nze/env.rs +++ b/dhall/src/semantics/nze/env.rs @@ -60,7 +60,8 @@ impl NzEnv { env } pub fn insert_value_noty(&self, e: Value) -> Self { - let ty = e.get_type_not_sort(); + // TODO + let ty = Value::const_sort(); self.insert_value(e, ty) } pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind { -- cgit v1.2.3 From 35cc98dc767247f4881866de40c7d8dd82eba8a5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 22:30:32 +0000 Subject: Remove types from NzEnv --- dhall/src/semantics/nze/env.rs | 42 +++++++++++++++++++++++++----------------- 1 file changed, 25 insertions(+), 17 deletions(-) (limited to 'dhall/src/semantics/nze/env.rs') diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs index ff52343..5b036f0 100644 --- a/dhall/src/semantics/nze/env.rs +++ b/dhall/src/semantics/nze/env.rs @@ -1,4 +1,4 @@ -use crate::semantics::{AlphaVar, Type, Value, ValueKind}; +use crate::semantics::{AlphaVar, Value, ValueKind}; #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub(crate) enum NzVar { @@ -9,7 +9,7 @@ pub(crate) enum NzVar { } #[derive(Debug, Clone)] -enum NzEnvItem { +enum EnvItem { // Variable is bound with given type Kept(Type), // Variable has been replaced by corresponding value @@ -17,10 +17,12 @@ enum NzEnvItem { } #[derive(Debug, Clone)] -pub(crate) struct NzEnv { - items: Vec, +pub(crate) struct ValEnv { + items: Vec>, } +pub(crate) type NzEnv = ValEnv<()>; + impl NzVar { pub fn new(idx: usize) -> Self { NzVar::Bound(idx) @@ -44,37 +46,43 @@ impl NzVar { } } -impl NzEnv { +impl ValEnv { pub fn new() -> Self { - NzEnv { items: Vec::new() } + ValEnv { items: Vec::new() } + } + pub fn discard_types(&self) -> ValEnv<()> { + let items = self + .items + .iter() + .map(|i| match i { + EnvItem::Kept(_) => EnvItem::Kept(()), + EnvItem::Replaced(val, _) => EnvItem::Replaced(val.clone(), ()), + }) + .collect(); + ValEnv { items } } pub fn insert_type(&self, ty: Type) -> Self { let mut env = self.clone(); - env.items.push(NzEnvItem::Kept(ty)); + env.items.push(EnvItem::Kept(ty)); env } pub fn insert_value(&self, e: Value, ty: Type) -> Self { let mut env = self.clone(); - env.items.push(NzEnvItem::Replaced(e, ty)); + env.items.push(EnvItem::Replaced(e, ty)); env } - pub fn insert_value_noty(&self, e: Value) -> Self { - // TODO - let ty = Value::const_sort(); - self.insert_value(e, ty) - } pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind { let idx = self.items.len() - 1 - var.idx(); match &self.items[idx] { - NzEnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)), - NzEnvItem::Replaced(x, _) => x.kind().clone(), + EnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)), + EnvItem::Replaced(x, _) => x.kind().clone(), } } - pub fn lookup_ty(&self, var: &AlphaVar) -> Value { + pub fn lookup_ty(&self, var: &AlphaVar) -> Type { let idx = self.items.len() - 1 - var.idx(); match &self.items[idx] { - NzEnvItem::Kept(ty) | NzEnvItem::Replaced(_, ty) => ty.clone(), + EnvItem::Kept(ty) | EnvItem::Replaced(_, ty) => ty.clone(), } } } -- cgit v1.2.3 From c3ed75dc4b354becac0821e4288105dc2a300c4c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 10 Feb 2020 19:14:07 +0000 Subject: Remove need for Embed This was an archaic leftover from copying the Haskell datatypes anyway --- dhall/src/semantics/nze/env.rs | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'dhall/src/semantics/nze/env.rs') diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs index 5b036f0..241af40 100644 --- a/dhall/src/semantics/nze/env.rs +++ b/dhall/src/semantics/nze/env.rs @@ -86,3 +86,9 @@ impl ValEnv { } } } + +impl<'a> From<&'a NzEnv> for NzEnv { + fn from(x: &'a NzEnv) -> Self { + x.clone() + } +} -- cgit v1.2.3 From cd5e172002ce724be7bdd52883e121efa8817f20 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 17 Feb 2020 18:22:06 +0000 Subject: Rename Value to Nir --- dhall/src/semantics/nze/env.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'dhall/src/semantics/nze/env.rs') diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs index 241af40..55050ed 100644 --- a/dhall/src/semantics/nze/env.rs +++ b/dhall/src/semantics/nze/env.rs @@ -1,4 +1,4 @@ -use crate::semantics::{AlphaVar, Value, ValueKind}; +use crate::semantics::{AlphaVar, Nir, NirKind}; #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub(crate) enum NzVar { @@ -13,7 +13,7 @@ enum EnvItem { // Variable is bound with given type Kept(Type), // Variable has been replaced by corresponding value - Replaced(Value, Type), + Replaced(Nir, Type), } #[derive(Debug, Clone)] @@ -67,15 +67,15 @@ impl ValEnv { env.items.push(EnvItem::Kept(ty)); env } - pub fn insert_value(&self, e: Value, ty: Type) -> Self { + pub fn insert_value(&self, e: Nir, ty: Type) -> Self { let mut env = self.clone(); env.items.push(EnvItem::Replaced(e, ty)); env } - pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind { + pub fn lookup_val(&self, var: &AlphaVar) -> NirKind { let idx = self.items.len() - 1 - var.idx(); match &self.items[idx] { - EnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)), + EnvItem::Kept(_) => NirKind::Var(NzVar::new(idx)), EnvItem::Replaced(x, _) => x.kind().clone(), } } -- cgit v1.2.3