summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/semantics/builtins.rs14
-rw-r--r--dhall/src/semantics/hir.rs4
-rw-r--r--dhall/src/semantics/nze/env.rs3
-rw-r--r--dhall/src/semantics/nze/value.rs80
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs4
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<Value>, 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<Value>, 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<ValueInternal>);
#[derive(Debug)]
struct ValueInternal {
kind: lazy::Lazy<Thunk, ValueKind>,
- /// This is None if and only if `form` is `Sort` (which doesn't have a type)
- ty: Option<Value>,
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, Normalized>) -> 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<Value, TypeError> {
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<Label, Option<Value>>| {
@@ -340,17 +292,15 @@ impl Value {
}
impl ValueInternal {
- fn from_whnf(k: ValueKind, ty: Option<Value>, 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<Value>, 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
}
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 17:10:18 +0000