From 8edbeadbd0dc06a75ffb8bf3b0a54a62e3acc5fc Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 27 Dec 2019 14:26:40 +0000 Subject: Parameterize ValueKind by its subnodes --- dhall/src/semantics/core/value.rs | 33 ++++++++++++++++++--------------- dhall/src/semantics/phase/mod.rs | 2 +- dhall/src/semantics/phase/normalize.rs | 15 +++++++++------ dhall/src/semantics/to_expr.rs | 2 +- 4 files changed, 29 insertions(+), 23 deletions(-) (limited to 'dhall') 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>); #[derive(Debug)] struct ValueInternal { form: Form, - kind: ValueKind, + kind: ValueKind, /// This is None if and only if `value` is `Sort` (which doesn't have a type) ty: Option, span: Span, @@ -52,7 +52,7 @@ pub(crate) enum Form { } #[derive(Debug, Clone, PartialEq, Eq)] -pub(crate) enum ValueKind { +pub(crate) enum ValueKind { /// 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, 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, t: Value) -> Value { Value::new(v, Unevaled, t, Span::Artificial) } pub(crate) fn from_kind_and_type_and_span( - v: ValueKind, + v: ValueKind, 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, + 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 { + pub(crate) fn as_kind(&self) -> Ref> { 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 { + pub(crate) fn as_whnf(&self) -> Ref> { 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 { 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 { 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 { &self.kind } @@ -297,7 +300,7 @@ impl ValueInternal { } } -impl ValueKind { +impl ValueKind { 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 { ValueKind::AppliedBuiltin(b, vec![]) } } @@ -402,7 +405,7 @@ impl Shift for ValueInternal { } } -impl Shift for ValueKind { +impl Shift for ValueKind { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(match self { ValueKind::Lam(x, t, e) => ValueKind::Lam( @@ -495,7 +498,7 @@ impl Subst for ValueInternal { } } -impl Subst for ValueKind { +impl Subst for ValueKind { 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, 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, ty: &Value, -) -> ValueKind { +) -> ValueKind { use syntax::Builtin::*; use ValueKind::*; // Small helper enum enum Ret<'a> { - ValueKind(ValueKind), + ValueKind(ValueKind), 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 { 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), ValueRef(&'a Value), Expr(ExprKind), @@ -589,7 +589,7 @@ fn apply_binop<'a>( pub(crate) fn normalize_one_layer( expr: ExprKind, ty: &Value, -) -> ValueKind { +) -> ValueKind { 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, + ty: &Value, +) -> ValueKind { 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, opts: ToExprOptions, ) -> NormalizedExpr { match kind { -- cgit v1.2.3