diff options
author | Nadrieril | 2020-01-30 18:06:53 +0000 |
---|---|---|
committer | Nadrieril | 2020-01-30 18:06:53 +0000 |
commit | 0749482ad2ab9340fb45a2fe2997d2ea04516d75 (patch) | |
tree | 08e3e0d817ebd031e8b6db98e2fc0bc65b5074b7 /dhall | |
parent | 7062de011eab7954f4bcf78fa1cf970ba91d6a5a (diff) |
Remove type parameter from ValueKind
Diffstat (limited to 'dhall')
-rw-r--r-- | dhall/src/lib.rs | 5 | ||||
-rw-r--r-- | dhall/src/semantics/builtins.rs | 13 | ||||
-rw-r--r-- | dhall/src/semantics/nze/normalize.rs | 11 | ||||
-rw-r--r-- | dhall/src/semantics/nze/value.rs | 27 |
4 files changed, 21 insertions, 35 deletions
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index e9f8aa3..dbf1fc0 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -153,10 +153,7 @@ impl Normalized { pub(crate) fn from_const(c: Const) -> Self { Normalized(Value::from_const(c)) } - pub(crate) fn from_kind_and_type( - v: ValueKind<Value>, - t: Normalized, - ) -> Self { + pub(crate) fn from_kind_and_type(v: ValueKind, t: Normalized) -> Self { Normalized(Value::from_kind_and_type(v, t.into_value())) } pub(crate) fn from_value(th: Value) -> Self { 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)) } } |