diff options
author | Nadrieril | 2019-12-27 14:26:40 +0000 |
---|---|---|
committer | Nadrieril | 2020-01-17 10:06:00 +0000 |
commit | 8edbeadbd0dc06a75ffb8bf3b0a54a62e3acc5fc (patch) | |
tree | a7c6f79d1ad8a81e430cac14ebdf66ad92d188f7 /dhall/src | |
parent | 3603fbf9d321602a2df51e7b3f7a69425bd4d304 (diff) |
Parameterize ValueKind by its subnodes
Diffstat (limited to 'dhall/src')
-rw-r--r-- | dhall/src/semantics/core/value.rs | 33 | ||||
-rw-r--r-- | dhall/src/semantics/phase/mod.rs | 2 | ||||
-rw-r--r-- | dhall/src/semantics/phase/normalize.rs | 15 | ||||
-rw-r--r-- | dhall/src/semantics/to_expr.rs | 2 |
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 { |