summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
authorNadrieril2020-01-30 18:06:53 +0000
committerNadrieril2020-01-30 18:06:53 +0000
commit0749482ad2ab9340fb45a2fe2997d2ea04516d75 (patch)
tree08e3e0d817ebd031e8b6db98e2fc0bc65b5074b7 /dhall/src/semantics
parent7062de011eab7954f4bcf78fa1cf970ba91d6a5a (diff)
Remove type parameter from ValueKind
Diffstat (limited to 'dhall/src/semantics')
-rw-r--r--dhall/src/semantics/builtins.rs13
-rw-r--r--dhall/src/semantics/nze/normalize.rs11
-rw-r--r--dhall/src/semantics/nze/value.rs27
3 files changed, 20 insertions, 31 deletions
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index 2211579..6dbe878 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -35,18 +35,13 @@ impl BuiltinClosure<Value> {
}
}
- pub fn apply(
- &self,
- a: Value,
- f_ty: Value,
- ret_ty: &Value,
- ) -> ValueKind<Value> {
+ pub fn apply(&self, a: Value, f_ty: Value, ret_ty: &Value) -> ValueKind {
use std::iter::once;
let args = self.args.iter().cloned().chain(once(a.clone())).collect();
let types = self.types.iter().cloned().chain(once(f_ty)).collect();
apply_builtin(self.b, args, ret_ty, types, self.env.clone())
}
- pub fn ensure_whnf(self, ret_ty: &Value) -> ValueKind<Value> {
+ pub fn ensure_whnf(self, ret_ty: &Value) -> ValueKind {
apply_builtin(self.b, self.args, ret_ty, self.types, self.env)
}
pub fn normalize_mut(&mut self) {
@@ -276,13 +271,13 @@ fn apply_builtin(
ty: &Value,
types: Vec<Value>,
env: NzEnv,
-) -> ValueKind<Value> {
+) -> ValueKind {
use Builtin::*;
use ValueKind::*;
// Small helper enum
enum Ret {
- ValueKind(ValueKind<Value>),
+ ValueKind(ValueKind),
Value(Value),
DoneAsIs,
}
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 6564018..90036e3 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -9,7 +9,7 @@ use crate::syntax::{
};
use crate::Normalized;
-pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind<Value> {
+pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind {
let f_borrow = f.kind();
match &*f_borrow {
ValueKind::LamClosure { closure, .. } => {
@@ -102,7 +102,7 @@ where
// Small helper enum to avoid repetition
enum Ret<'a> {
- ValueKind(ValueKind<Value>),
+ ValueKind(ValueKind),
Value(Value),
ValueRef(&'a Value),
Expr(ExprKind<Value, Normalized>),
@@ -255,7 +255,7 @@ pub(crate) fn normalize_one_layer(
expr: ExprKind<Value, Normalized>,
ty: &Value,
env: &NzEnv,
-) -> ValueKind<Value> {
+) -> ValueKind {
use ValueKind::{
BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit,
NEOptionalLit, NaturalLit, RecordLit, RecordType, TextLit,
@@ -450,10 +450,7 @@ pub(crate) fn normalize_one_layer(
}
/// Normalize a ValueKind into WHNF
-pub(crate) fn normalize_whnf(
- v: ValueKind<Value>,
- ty: &Value,
-) -> ValueKind<Value> {
+pub(crate) fn normalize_whnf(v: ValueKind, ty: &Value) -> ValueKind {
match v {
ValueKind::AppliedBuiltin(closure) => closure.ensure_whnf(ty),
ValueKind::PartialExpr(e) => normalize_one_layer(e, ty, &NzEnv::new()),
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 6ab6fe3..8fad911 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -28,7 +28,7 @@ pub(crate) struct Value(Rc<RefCell<ValueInternal>>);
#[derive(Debug)]
struct ValueInternal {
form: Form,
- kind: ValueKind<Value>,
+ kind: ValueKind,
/// This is None if and only if `value` is `Sort` (which doesn't have a type)
ty: Option<Value>,
span: Span,
@@ -68,7 +68,7 @@ pub(crate) enum Closure {
}
#[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) enum ValueKind<Value> {
+pub(crate) enum ValueKind {
/// Closures
LamClosure {
binder: Binder,
@@ -112,7 +112,7 @@ pub(crate) enum ValueKind<Value> {
}
impl Value {
- fn new(kind: ValueKind<Value>, form: Form, ty: Value, span: Span) -> Value {
+ fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value {
ValueInternal {
form,
kind,
@@ -139,13 +139,10 @@ impl Value {
}
.into_value()
}
- pub(crate) fn from_kind_and_type(v: ValueKind<Value>, t: Value) -> Value {
+ pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value {
Value::new(v, Unevaled, t, Span::Artificial)
}
- pub(crate) fn from_kind_and_type_whnf(
- v: ValueKind<Value>,
- t: Value,
- ) -> Value {
+ pub(crate) fn from_kind_and_type_whnf(v: ValueKind, t: Value) -> Value {
Value::new(v, WHNF, t, Span::Artificial)
}
pub(crate) fn from_const(c: Const) -> Self {
@@ -189,7 +186,7 @@ impl Value {
/// 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 kind(&self) -> Ref<ValueKind<Value>> {
+ pub(crate) fn kind(&self) -> Ref<ValueKind> {
self.normalize_whnf();
Ref::map(self.as_internal(), ValueInternal::as_kind)
}
@@ -202,11 +199,11 @@ impl Value {
self.to_tyexpr_noenv().to_expr(opts)
}
- pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind<Value> {
+ pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind {
self.kind().clone()
}
/// Before discarding type information, check that it matches the expected return type.
- pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind<Value> {
+ pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind {
self.check_type(ty);
self.to_whnf_ignore_type()
}
@@ -397,7 +394,7 @@ impl ValueInternal {
fn into_value(self) -> Value {
Value(Rc::new(RefCell::new(self)))
}
- fn as_kind(&self) -> &ValueKind<Value> {
+ fn as_kind(&self) -> &ValueKind {
&self.kind
}
@@ -442,7 +439,7 @@ impl ValueInternal {
}
}
-impl ValueKind<Value> {
+impl ValueKind {
pub(crate) fn into_value_with_type(self, t: Value) -> Value {
Value::from_kind_and_type(self, t)
}
@@ -513,10 +510,10 @@ impl ValueKind<Value> {
}
}
- pub(crate) fn from_builtin(b: Builtin) -> ValueKind<Value> {
+ pub(crate) fn from_builtin(b: Builtin) -> ValueKind {
ValueKind::from_builtin_env(b, NzEnv::new())
}
- pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> ValueKind<Value> {
+ pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> ValueKind {
ValueKind::AppliedBuiltin(BuiltinClosure::new(b, env))
}
}