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/builtins.rs | 14 ++----- dhall/src/semantics/hir.rs | 4 +- dhall/src/semantics/nze/env.rs | 3 +- dhall/src/semantics/nze/value.rs | 80 ++++----------------------------------- dhall/src/semantics/tck/tyexpr.rs | 4 +- 5 files changed, 16 insertions(+), 89 deletions(-) diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index b1d12aa..9d4f8a2 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -370,17 +370,9 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { } _ => Ret::DoneAsIs, }, - (ListIndexed, [_, l]) => { - let l_whnf = l.kind(); - match &*l_whnf { + (ListIndexed, [t, l]) => { + match l.kind() { EmptyListLit(_) | NEListLit(_) => { - // Extract the type of the list elements - let t = match &*l_whnf { - EmptyListLit(t) => t.clone(), - NEListLit(xs) => xs[0].get_type_not_sort(), - _ => unreachable!(), - }; - // Construct the returned record type: { index: Natural, value: t } let mut kts = HashMap::new(); kts.insert("index".into(), Value::from_builtin(Natural)); @@ -388,7 +380,7 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { let t = Value::from_kind(RecordType(kts)); // Construct the new list, with added indices - let list = match &*l_whnf { + let list = match l.kind() { EmptyListLit(_) => EmptyListLit(t), NEListLit(xs) => NEListLit( xs.iter() diff --git a/dhall/src/semantics/hir.rs b/dhall/src/semantics/hir.rs index 80d17fb..28b38e3 100644 --- a/dhall/src/semantics/hir.rs +++ b/dhall/src/semantics/hir.rs @@ -79,8 +79,8 @@ impl Hir { } /// Eval a closed Hir fully and recursively (TODO: ish, need to fix under lambdas) pub fn rec_eval_closed_expr(&self) -> Value { - let mut val = self.eval_closed_expr(); - val.normalize_mut(); + let val = self.eval_closed_expr(); + val.normalize(); val } } 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 { diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 48acdb5..5a7b558 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -1,7 +1,7 @@ use std::collections::HashMap; use std::rc::Rc; -use crate::error::{TypeError, TypeMessage}; +use crate::error::TypeError; use crate::semantics::nze::lazy; use crate::semantics::{ apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, @@ -25,8 +25,6 @@ pub(crate) struct Value(Rc); #[derive(Debug)] struct ValueInternal { kind: lazy::Lazy, - /// This is None if and only if `form` is `Sort` (which doesn't have a type) - ty: Option, span: Span, } @@ -103,25 +101,12 @@ pub(crate) enum ValueKind { impl Value { pub(crate) fn const_sort() -> Value { - ValueInternal::from_whnf( - ValueKind::Const(Const::Sort), - None, - Span::Artificial, - ) - .into_value() - } - pub(crate) fn const_kind() -> Value { - Value::from_const(Const::Kind) + Value::from_const(Const::Sort) } /// Construct a Value from a completely unnormalized expression. pub(crate) fn new_thunk(env: &NzEnv, hir: Hir) -> Value { let span = hir.span(); - ValueInternal::from_thunk( - Thunk::new(env, hir), - Some(Value::const_kind()), - span, - ) - .into_value() + ValueInternal::from_thunk(Thunk::new(env, hir), span).into_value() } /// Construct a Value from a partially normalized expression that's not in WHNF. pub(crate) fn from_partial_expr(e: ExprKind) -> Value { @@ -129,33 +114,17 @@ impl Value { let env = NzEnv::new(); ValueInternal::from_thunk( Thunk::from_partial_expr(env, e), - Some(Value::const_kind()), Span::Artificial, ) .into_value() } /// Make a Value from a ValueKind pub(crate) fn from_kind(v: ValueKind) -> Value { - ValueInternal::from_whnf(v, Some(Value::const_kind()), Span::Artificial) - .into_value() + ValueInternal::from_whnf(v, Span::Artificial).into_value() } pub(crate) fn from_const(c: Const) -> Self { let v = ValueKind::Const(c); - match c { - Const::Type => ValueInternal::from_whnf( - v, - Some(Value::from_const(Const::Kind)), - Span::Artificial, - ) - .into_value(), - Const::Kind => ValueInternal::from_whnf( - v, - Some(Value::const_sort()), - Span::Artificial, - ) - .into_value(), - Const::Sort => Value::const_sort(), - } + ValueInternal::from_whnf(v, Span::Artificial).into_value() } pub(crate) fn from_builtin(b: Builtin) -> Self { Self::from_builtin_env(b, &NzEnv::new()) @@ -193,16 +162,6 @@ impl Value { self.to_hir(env.as_varenv()).to_expr_tyenv(env) } - /// Normalizes contents to normal form; faster than `normalize` if - /// no one else shares this. - pub(crate) fn normalize_mut(&mut self) { - match Rc::get_mut(&mut self.0) { - // Mutate directly if sole owner - Some(vint) => vint.normalize_mut(), - // Otherwise mutate through the refcell - None => self.normalize(), - } - } pub(crate) fn normalize(&self) { self.0.normalize() } @@ -214,13 +173,6 @@ impl Value { pub(crate) fn get_type(&self, tyenv: &TyEnv) -> Result { self.to_tyexpr_tyenv(tyenv).get_type() } - /// When we know the value isn't `Sort`, this gets the type directly - pub(crate) fn get_type_not_sort(&self) -> Value { - self.0 - .get_type() - .expect("Internal type error: value is `Sort` but shouldn't be") - .clone() - } pub fn to_hir(&self, venv: VarEnv) -> Hir { let map_uniontype = |kts: &HashMap>| { @@ -340,17 +292,15 @@ impl Value { } impl ValueInternal { - fn from_whnf(k: ValueKind, ty: Option, span: Span) -> Self { + fn from_whnf(k: ValueKind, span: Span) -> Self { ValueInternal { kind: lazy::Lazy::new_completed(k), - ty, span, } } - fn from_thunk(th: Thunk, ty: Option, span: Span) -> Self { + fn from_thunk(th: Thunk, span: Span) -> Self { ValueInternal { kind: lazy::Lazy::new(th), - ty, span, } } @@ -364,17 +314,6 @@ impl ValueInternal { fn normalize(&self) { self.kind().normalize(); } - // TODO: deprecated - fn normalize_mut(&mut self) { - self.normalize(); - } - - fn get_type(&self) -> Result<&Value, TypeError> { - match &self.ty { - Some(t) => Ok(t), - None => Err(TypeError::new(TypeMessage::Sort)), - } - } } impl ValueKind { @@ -616,11 +555,6 @@ impl std::fmt::Debug for Value { } let mut x = fmt.debug_struct(&format!("Value@WHNF")); x.field("kind", kind); - if let Some(ty) = vint.ty.as_ref() { - x.field("type", &ty); - } else { - x.field("type", &None::<()>); - } x.finish() } } diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 29099c5..05fa4b5 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -66,8 +66,8 @@ impl TyExpr { } /// Eval a closed TyExpr fully and recursively; pub fn rec_eval_closed_expr(&self) -> Value { - let mut val = self.eval_closed_expr(); - val.normalize_mut(); + let val = self.eval_closed_expr(); + val.normalize(); val } } -- cgit v1.2.3