From cb86493012b268ec32ad85a42b54fb1a2adab7b0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 14:20:01 +0000 Subject: s/as_whnf/kind/ --- dhall/src/semantics/builtins.rs | 40 +++++++++++++++++----------------- dhall/src/semantics/core/value.rs | 10 ++++----- dhall/src/semantics/phase/normalize.rs | 26 +++++++++++----------- dhall/src/semantics/tck/typecheck.rs | 32 +++++++++++++-------------- 4 files changed, 53 insertions(+), 55 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index a23591e..a536261 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -290,31 +290,31 @@ fn apply_builtin( let ret = match (b, args.as_slice()) { (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())), - (NaturalIsZero, [n]) => match &*n.as_whnf() { + (NaturalIsZero, [n]) => match &*n.kind() { NaturalLit(n) => Ret::ValueKind(BoolLit(*n == 0)), _ => Ret::DoneAsIs, }, - (NaturalEven, [n]) => match &*n.as_whnf() { + (NaturalEven, [n]) => match &*n.kind() { NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 == 0)), _ => Ret::DoneAsIs, }, - (NaturalOdd, [n]) => match &*n.as_whnf() { + (NaturalOdd, [n]) => match &*n.kind() { NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 != 0)), _ => Ret::DoneAsIs, }, - (NaturalToInteger, [n]) => match &*n.as_whnf() { + (NaturalToInteger, [n]) => match &*n.kind() { NaturalLit(n) => Ret::ValueKind(IntegerLit(*n as isize)), _ => Ret::DoneAsIs, }, (NaturalShow, [n]) => { - match &*n.as_whnf() { + match &*n.kind() { NaturalLit(n) => Ret::ValueKind(TextLit(vec![ InterpolatedTextContents::Text(n.to_string()), ])), _ => Ret::DoneAsIs, } } - (NaturalSubtract, [a, b]) => match (&*a.as_whnf(), &*b.as_whnf()) { + (NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) { (NaturalLit(a), NaturalLit(b)) => { Ret::ValueKind(NaturalLit(if b > a { b - a } else { 0 })) } @@ -323,7 +323,7 @@ fn apply_builtin( _ if a == b => Ret::ValueKind(NaturalLit(0)), _ => Ret::DoneAsIs, }, - (IntegerShow, [n]) => match &*n.as_whnf() { + (IntegerShow, [n]) => match &*n.kind() { IntegerLit(n) => { let s = if *n < 0 { n.to_string() @@ -334,31 +334,31 @@ fn apply_builtin( } _ => Ret::DoneAsIs, }, - (IntegerToDouble, [n]) => match &*n.as_whnf() { + (IntegerToDouble, [n]) => match &*n.kind() { IntegerLit(n) => { Ret::ValueKind(DoubleLit(NaiveDouble::from(*n as f64))) } _ => Ret::DoneAsIs, }, - (IntegerNegate, [n]) => match &*n.as_whnf() { + (IntegerNegate, [n]) => match &*n.kind() { IntegerLit(n) => Ret::ValueKind(IntegerLit(-n)), _ => Ret::DoneAsIs, }, - (IntegerClamp, [n]) => match &*n.as_whnf() { + (IntegerClamp, [n]) => match &*n.kind() { IntegerLit(n) => { Ret::ValueKind(NaturalLit((*n).try_into().unwrap_or(0))) } _ => Ret::DoneAsIs, }, (DoubleShow, [n]) => { - match &*n.as_whnf() { + match &*n.kind() { DoubleLit(n) => Ret::ValueKind(TextLit(vec![ InterpolatedTextContents::Text(n.to_string()), ])), _ => Ret::DoneAsIs, } } - (TextShow, [v]) => match &*v.as_whnf() { + (TextShow, [v]) => match &*v.kind() { TextLit(elts) => { match elts.as_slice() { // Empty string literal. @@ -390,26 +390,26 @@ fn apply_builtin( } _ => Ret::DoneAsIs, }, - (ListLength, [_, l]) => match &*l.as_whnf() { + (ListLength, [_, l]) => match &*l.kind() { EmptyListLit(_) => Ret::ValueKind(NaturalLit(0)), NEListLit(xs) => Ret::ValueKind(NaturalLit(xs.len())), _ => Ret::DoneAsIs, }, - (ListHead, [_, l]) => match &*l.as_whnf() { + (ListHead, [_, l]) => match &*l.kind() { EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())), NEListLit(xs) => { Ret::ValueKind(NEOptionalLit(xs.iter().next().unwrap().clone())) } _ => Ret::DoneAsIs, }, - (ListLast, [_, l]) => match &*l.as_whnf() { + (ListLast, [_, l]) => match &*l.kind() { EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())), NEListLit(xs) => Ret::ValueKind(NEOptionalLit( xs.iter().rev().next().unwrap().clone(), )), _ => Ret::DoneAsIs, }, - (ListReverse, [_, l]) => match &*l.as_whnf() { + (ListReverse, [_, l]) => match &*l.kind() { EmptyListLit(n) => Ret::ValueKind(EmptyListLit(n.clone())), NEListLit(xs) => { Ret::ValueKind(NEListLit(xs.iter().rev().cloned().collect())) @@ -417,7 +417,7 @@ fn apply_builtin( _ => Ret::DoneAsIs, }, (ListIndexed, [_, l]) => { - let l_whnf = l.as_whnf(); + let l_whnf = l.kind(); match &*l_whnf { EmptyListLit(_) | NEListLit(_) => { // Extract the type of the list elements @@ -484,7 +484,7 @@ fn apply_builtin( .app(EmptyListLit(t.clone()).into_value_with_type(list_t)), ) } - (ListFold, [_, l, _, cons, nil]) => match &*l.as_whnf() { + (ListFold, [_, l, _, cons, nil]) => match &*l.kind() { EmptyListLit(_) => Ret::Value(nil.clone()), NEListLit(xs) => { let mut v = nil.clone(); @@ -513,7 +513,7 @@ fn apply_builtin( ), ) } - (OptionalFold, [_, v, _, just, nothing]) => match &*v.as_whnf() { + (OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() { EmptyOptionalLit(_) => Ret::Value(nothing.clone()), NEOptionalLit(x) => Ret::Value(just.app(x.clone())), _ => Ret::DoneAsIs, @@ -530,7 +530,7 @@ fn apply_builtin( ), ), - (NaturalFold, [n, t, succ, zero]) => match &*n.as_whnf() { + (NaturalFold, [n, t, succ, zero]) => match &*n.kind() { NaturalLit(0) => Ret::Value(zero.clone()), NaturalLit(n) => { let fold = Value::from_builtin(NaturalFold) diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index e69d220..02c8013 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -157,7 +157,7 @@ impl Value { } pub(crate) fn as_const(&self) -> Option { - match &*self.as_whnf() { + match &*self.kind() { ValueKind::Const(c) => Some(*c), _ => None, } @@ -180,7 +180,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 as_whnf(&self) -> Ref> { + pub(crate) fn kind(&self) -> Ref> { self.normalize_whnf(); self.as_kind() } @@ -194,7 +194,7 @@ impl Value { self.to_tyexpr_noenv().to_expr(opts) } pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind { - self.as_whnf().clone() + 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 { @@ -233,7 +233,7 @@ impl Value { } pub(crate) fn app(&self, v: Value) -> Value { - let body_t = match &*self.get_type_not_sort().as_whnf() { + let body_t = match &*self.get_type_not_sort().kind() { ValueKind::PiClosure { annot, closure, .. } => { v.check_type(annot); closure.apply(v.clone()) @@ -617,7 +617,7 @@ impl Closure { // TODO: use Rc comparison to shortcut on identical pointers impl std::cmp::PartialEq for Value { fn eq(&self, other: &Self) -> bool { - *self.as_whnf() == *other.as_whnf() + *self.kind() == *other.kind() } } impl std::cmp::Eq for Value {} diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index d7720c7..f36ec4a 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -10,7 +10,7 @@ use crate::syntax::{ }; pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { - let f_borrow = f.as_whnf(); + let f_borrow = f.kind(); match &*f_borrow { ValueKind::LamClosure { closure, .. } => { closure.apply(a).to_whnf_check_type(ty) @@ -47,7 +47,7 @@ pub(crate) fn squash_textlit( match contents { Text(s) => crnt_str.push_str(&s), Expr(e) => { - let e_borrow = e.as_whnf(); + let e_borrow = e.kind(); match &*e_borrow { ValueKind::TextLit(elts2) => { inner(elts2.iter().cloned(), crnt_str, ret) @@ -123,8 +123,8 @@ fn apply_binop<'a>( BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType, TextLit, }; - let x_borrow = x.as_whnf(); - let y_borrow = y.as_whnf(); + let x_borrow = x.kind(); + let y_borrow = y.kind(); Some(match (o, &*x_borrow, &*y_borrow) { (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y), (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x), @@ -206,7 +206,7 @@ fn apply_binop<'a>( Ret::ValueRef(y) } (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let ty_borrow = ty.as_whnf(); + let ty_borrow = ty.kind(); let kts = match &*ty_borrow { RecordType(kts) => kts, _ => unreachable!("Internal type error"), @@ -286,7 +286,7 @@ pub(crate) fn normalize_one_layer( ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)), ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)), ExprKind::EmptyListLit(t) => { - let arg = match &*t.as_whnf() { + let arg = match &*t.kind() { ValueKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, args, @@ -319,13 +319,13 @@ pub(crate) fn normalize_one_layer( } } ExprKind::BoolIf(ref b, ref e1, ref e2) => { - let b_borrow = b.as_whnf(); + let b_borrow = b.kind(); match &*b_borrow { BoolLit(true) => Ret::ValueRef(e1), BoolLit(false) => Ret::ValueRef(e2), _ => { - let e1_borrow = e1.as_whnf(); - let e2_borrow = e2.as_whnf(); + let e1_borrow = e1.kind(); + let e2_borrow = e2.kind(); match (&*e1_borrow, &*e2_borrow) { // Simplify `if b then True else False` (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b), @@ -349,7 +349,7 @@ pub(crate) fn normalize_one_layer( Ret::ValueKind(RecordLit(HashMap::new())) } ExprKind::Projection(ref v, ref ls) => { - let v_borrow = v.as_whnf(); + let v_borrow = v.kind(); match &*v_borrow { RecordLit(kvs) => Ret::ValueKind(RecordLit( ls.iter() @@ -365,7 +365,7 @@ pub(crate) fn normalize_one_layer( } } ExprKind::Field(ref v, ref l) => { - let v_borrow = v.as_whnf(); + let v_borrow = v.kind(); match &*v_borrow { RecordLit(kvs) => match kvs.get(l) { Some(r) => Ret::Value(r.clone()), @@ -391,8 +391,8 @@ pub(crate) fn normalize_one_layer( ExprKind::Completion(_, _) => unimplemented!("record completion"), ExprKind::Merge(ref handlers, ref variant, _) => { - let handlers_borrow = handlers.as_whnf(); - let variant_borrow = variant.as_whnf(); + let handlers_borrow = handlers.kind(); + let variant_borrow = variant.kind(); match (&*handlers_borrow, &*variant_borrow) { (RecordLit(kvs), UnionConstructor(l, _, _)) => match kvs.get(l) { diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index e1a9c11..0c5e779 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -94,7 +94,7 @@ fn type_one_layer( } ExprKind::EmptyListLit(t) => { let t = t.normalize_nf(env.as_nzenv()); - match &*t.as_whnf() { + match &*t.kind() { ValueKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, args, @@ -189,7 +189,7 @@ fn type_one_layer( Value::from_const(k) } ExprKind::Field(scrut, x) => { - match &*scrut.get_type()?.as_whnf() { + match &*scrut.get_type()?.kind() { ValueKind::RecordType(kts) => match kts.get(&x) { Some(tth) => tth.clone(), None => return mkerr("MissingRecordField"), @@ -197,7 +197,7 @@ fn type_one_layer( // TODO: branch here only when scrut.get_type() is a Const _ => { let scrut_nf = scrut.normalize_nf(env.as_nzenv()); - let scrut_nf_borrow = scrut_nf.as_whnf(); + let scrut_nf_borrow = scrut_nf.kind(); match &*scrut_nf_borrow { ValueKind::UnionType(kts) => match kts.get(x) { // Constructor has type T -> < x: T, ... > @@ -244,7 +244,7 @@ fn type_one_layer( } ExprKind::Assert(t) => { let t = t.normalize_whnf(env.as_nzenv()); - match &*t.as_whnf() { + match &*t.kind() { ValueKind::Equivalence(x, y) if x == y => {} ValueKind::Equivalence(..) => return mkerr("AssertMismatch"), _ => return mkerr("AssertMustTakeEquivalence"), @@ -253,7 +253,7 @@ fn type_one_layer( } ExprKind::App(f, arg) => { let tf = f.get_type()?; - let tf_borrow = tf.as_whnf(); + let tf_borrow = tf.kind(); match &*tf_borrow { ValueKind::PiClosure { annot, closure, .. } => { if arg.get_type()? != *annot { @@ -275,9 +275,7 @@ fn type_one_layer( } } ExprKind::BoolIf(x, y, z) => { - if *x.get_type()?.as_whnf() - != ValueKind::from_builtin(Builtin::Bool) - { + if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) { return mkerr("InvalidPredicate"); } if y.get_type()?.get_type()?.as_const() != Some(Const::Type) { @@ -297,14 +295,14 @@ fn type_one_layer( let y_type = y.get_type()?; // Extract the LHS record type - let x_type_borrow = x_type.as_whnf(); + let x_type_borrow = x_type.kind(); let kts_x = match &*x_type_borrow { ValueKind::RecordType(kts) => kts, _ => return mkerr("MustCombineRecord"), }; // Extract the RHS record type - let y_type_borrow = y_type.as_whnf(); + let y_type_borrow = y_type.kind(); let kts_y = match &*y_type_borrow { ValueKind::RecordType(kts) => kts, _ => return mkerr("MustCombineRecord"), @@ -336,8 +334,8 @@ fn type_one_layer( ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => { let x_val = x.normalize_whnf(env.as_nzenv()); let y_val = y.normalize_whnf(env.as_nzenv()); - let x_val_borrow = x_val.as_whnf(); - let y_val_borrow = y_val.as_whnf(); + let x_val_borrow = x_val.kind(); + let y_val_borrow = y_val.kind(); let kts_x = match &*x_val_borrow { ValueKind::RecordType(kts) => kts, _ => return mkerr("RecordTypeMergeRequiresRecordType"), @@ -366,7 +364,7 @@ fn type_one_layer( } ExprKind::BinOp(BinOp::ListAppend, l, r) => { let l_ty = l.get_type()?; - match &*l_ty.as_whnf() { + match &*l_ty.kind() { ValueKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, .. @@ -418,14 +416,14 @@ fn type_one_layer( } ExprKind::Merge(record, union, type_annot) => { let record_type = record.get_type()?; - let record_borrow = record_type.as_whnf(); + let record_borrow = record_type.kind(); let handlers = match &*record_borrow { ValueKind::RecordType(kts) => kts, _ => return mkerr("Merge1ArgMustBeRecord"), }; let union_type = union.get_type()?; - let union_borrow = union_type.as_whnf(); + let union_borrow = union_type.kind(); let variants = match &*union_borrow { ValueKind::UnionType(kts) => Cow::Borrowed(kts), ValueKind::AppliedBuiltin(BuiltinClosure { @@ -447,7 +445,7 @@ fn type_one_layer( let handler_return_type = match variants.get(x) { // Union alternative with type Some(Some(variant_type)) => { - let handler_type_borrow = handler_type.as_whnf(); + let handler_type_borrow = handler_type.kind(); match &*handler_type_borrow { ValueKind::PiClosure { closure, annot, .. } => { if variant_type != annot { @@ -498,7 +496,7 @@ fn type_one_layer( ExprKind::ToMap(_, _) => unimplemented!("toMap"), ExprKind::Projection(record, labels) => { let record_type = record.get_type()?; - let record_type_borrow = record_type.as_whnf(); + let record_type_borrow = record_type.kind(); let kts = match &*record_type_borrow { ValueKind::RecordType(kts) => kts, _ => return mkerr("ProjectionMustBeRecord"), -- cgit v1.2.3