summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/semantics/core/value.rs33
-rw-r--r--dhall/src/semantics/phase/mod.rs2
-rw-r--r--dhall/src/semantics/phase/normalize.rs15
-rw-r--r--dhall/src/semantics/to_expr.rs2
4 files changed, 29 insertions, 23 deletions
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index f06c614..5f244b7 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -30,7 +30,7 @@ pub(crate) struct Value(Rc<RefCell<ValueInternal>>);
#[derive(Debug)]
struct ValueInternal {
form: Form,
- kind: ValueKind,
+ kind: ValueKind<Value>,
/// This is None if and only if `value` is `Sort` (which doesn't have a type)
ty: Option<Value>,
span: Span,
@@ -52,7 +52,7 @@ pub(crate) enum Form {
}
#[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) enum ValueKind {
+pub(crate) enum ValueKind<Value> {
/// Closures
Lam(AlphaLabel, Value, Value),
Pi(AlphaLabel, Value, Value),
@@ -84,7 +84,7 @@ pub(crate) enum ValueKind {
}
impl Value {
- fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value {
+ fn new(kind: ValueKind<Value>, form: Form, ty: Value, span: Span) -> Value {
ValueInternal {
form,
kind,
@@ -102,17 +102,20 @@ impl Value {
}
.into_value()
}
- pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value {
+ pub(crate) fn from_kind_and_type(v: ValueKind<Value>, t: Value) -> Value {
Value::new(v, Unevaled, t, Span::Artificial)
}
pub(crate) fn from_kind_and_type_and_span(
- v: ValueKind,
+ v: ValueKind<Value>,
t: Value,
span: Span,
) -> Value {
Value::new(v, Unevaled, t, span)
}
- pub(crate) fn from_kind_and_type_whnf(v: ValueKind, t: Value) -> Value {
+ pub(crate) fn from_kind_and_type_whnf(
+ v: ValueKind<Value>,
+ t: Value,
+ ) -> Value {
Value::new(v, WHNF, t, Span::Artificial)
}
pub(crate) fn from_const(c: Const) -> Self {
@@ -144,13 +147,13 @@ impl Value {
}
/// WARNING: The returned ValueKind may be entirely unnormalized, in particular it may just be an
/// unevaled PartialExpr. You probably want to use `as_whnf`.
- pub(crate) fn as_kind(&self) -> Ref<ValueKind> {
+ pub(crate) fn as_kind(&self) -> Ref<ValueKind<Value>> {
Ref::map(self.as_internal(), ValueInternal::as_kind)
}
/// This is what you want if you want to pattern-match on the value.
/// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut
/// panics.
- pub(crate) fn as_whnf(&self) -> Ref<ValueKind> {
+ pub(crate) fn as_whnf(&self) -> Ref<ValueKind<Value>> {
self.normalize_whnf();
self.as_kind()
}
@@ -162,11 +165,11 @@ impl Value {
) -> NormalizedExpr {
to_expr::value_to_expr(self, opts)
}
- pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind {
+ pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind<Value> {
self.as_whnf().clone()
}
/// Before discarding type information, check that it matches the expected return type.
- pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind {
+ pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind<Value> {
self.check_type(ty);
self.to_whnf_ignore_type()
}
@@ -241,7 +244,7 @@ impl ValueInternal {
fn into_value(self) -> Value {
Value(Rc::new(RefCell::new(self)))
}
- fn as_kind(&self) -> &ValueKind {
+ fn as_kind(&self) -> &ValueKind<Value> {
&self.kind
}
@@ -297,7 +300,7 @@ impl ValueInternal {
}
}
-impl ValueKind {
+impl ValueKind<Value> {
pub(crate) fn into_value_with_type(self, t: Value) -> Value {
Value::from_kind_and_type(self, t)
}
@@ -380,7 +383,7 @@ impl ValueKind {
}
}
- pub(crate) fn from_builtin(b: Builtin) -> ValueKind {
+ pub(crate) fn from_builtin(b: Builtin) -> ValueKind<Value> {
ValueKind::AppliedBuiltin(b, vec![])
}
}
@@ -402,7 +405,7 @@ impl Shift for ValueInternal {
}
}
-impl Shift for ValueKind {
+impl Shift for ValueKind<Value> {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
Some(match self {
ValueKind::Lam(x, t, e) => ValueKind::Lam(
@@ -495,7 +498,7 @@ impl Subst<Value> for ValueInternal {
}
}
-impl Subst<Value> for ValueKind {
+impl Subst<Value> for ValueKind<Value> {
fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
match self {
ValueKind::AppliedBuiltin(b, args) => {
diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs
index 5332eb3..104a1ba 100644
--- a/dhall/src/semantics/phase/mod.rs
+++ b/dhall/src/semantics/phase/mod.rs
@@ -94,7 +94,7 @@ impl Typed {
pub(crate) fn from_const(c: Const) -> Self {
Typed(Value::from_const(c))
}
- pub(crate) fn from_kind_and_type(v: ValueKind, t: Typed) -> Self {
+ pub(crate) fn from_kind_and_type(v: ValueKind<Value>, t: Typed) -> Self {
Typed(Value::from_kind_and_type(v, t.into_value()))
}
pub(crate) fn from_value(th: Value) -> Self {
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 0c581fe..7b4b37f 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -68,13 +68,13 @@ pub(crate) fn apply_builtin(
b: Builtin,
args: Vec<Value>,
ty: &Value,
-) -> ValueKind {
+) -> ValueKind<Value> {
use syntax::Builtin::*;
use ValueKind::*;
// Small helper enum
enum Ret<'a> {
- ValueKind(ValueKind),
+ ValueKind(ValueKind<Value>),
Value(Value),
// For applications that can return a function, it's important to keep the remaining
// arguments to apply them to the resulting function.
@@ -365,7 +365,7 @@ pub(crate) fn apply_builtin(
}
}
-pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind {
+pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind<Value> {
let f_borrow = f.as_whnf();
match &*f_borrow {
ValueKind::Lam(x, _, e) => {
@@ -456,7 +456,7 @@ where
// Small helper enum to avoid repetition
enum Ret<'a> {
- ValueKind(ValueKind),
+ ValueKind(ValueKind<Value>),
Value(Value),
ValueRef(&'a Value),
Expr(ExprKind<Value, Normalized>),
@@ -589,7 +589,7 @@ fn apply_binop<'a>(
pub(crate) fn normalize_one_layer(
expr: ExprKind<Value, Normalized>,
ty: &Value,
-) -> ValueKind {
+) -> ValueKind<Value> {
use ValueKind::{
AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit,
IntegerLit, NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit,
@@ -779,7 +779,10 @@ pub(crate) fn normalize_one_layer(
}
/// Normalize a ValueKind into WHNF
-pub(crate) fn normalize_whnf(v: ValueKind, ty: &Value) -> ValueKind {
+pub(crate) fn normalize_whnf(
+ v: ValueKind<Value>,
+ ty: &Value,
+) -> ValueKind<Value> {
match v {
ValueKind::AppliedBuiltin(b, args) => apply_builtin(b, args, ty),
ValueKind::PartialExpr(e) => normalize_one_layer(e, ty),
diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs
index b21fb29..9dee7b5 100644
--- a/dhall/src/semantics/to_expr.rs
+++ b/dhall/src/semantics/to_expr.rs
@@ -27,7 +27,7 @@ pub(crate) fn value_to_expr(
/// Converts a value back to the corresponding AST expression.
pub(crate) fn kind_to_expr(
- kind: &ValueKind,
+ kind: &ValueKind<Value>,
opts: ToExprOptions,
) -> NormalizedExpr {
match kind {
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 23:02:47 +0000