diff options
author | Nadrieril | 2019-08-19 12:25:09 +0200 |
---|---|---|
committer | Nadrieril | 2019-08-19 12:25:09 +0200 |
commit | 29016b78736dca857e4e7f7c4dc68ed5e30c28bb (patch) | |
tree | 365b46d7b954e2305a9371c996dd6a91e2fe645c /dhall/src/phase | |
parent | e70da4c0e9ee2354d757f19f1712f5b04f7acc99 (diff) |
s/to_valuef/to_whnf/ and avoid cloning ValueFs when possible
Diffstat (limited to 'dhall/src/phase')
-rw-r--r-- | dhall/src/phase/mod.rs | 15 | ||||
-rw-r--r-- | dhall/src/phase/normalize.rs | 94 | ||||
-rw-r--r-- | dhall/src/phase/typecheck.rs | 198 |
3 files changed, 149 insertions, 158 deletions
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs index c18f976..a38e9d3 100644 --- a/dhall/src/phase/mod.rs +++ b/dhall/src/phase/mod.rs @@ -1,4 +1,5 @@ use std::borrow::Cow; +use std::cell::Ref; use std::fmt::Display; use std::path::Path; @@ -111,8 +112,13 @@ impl Typed { Typed::from_const(Const::Type) } - pub(crate) fn to_valuef(&self) -> ValueF { - self.0.to_valuef() + /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut + /// panics. + pub(crate) fn as_whnf(&self) -> Ref<ValueF> { + self.0.as_whnf() + } + pub(crate) fn to_whnf(&self) -> ValueF { + self.0.to_whnf() } pub fn to_expr(&self) -> NormalizedSubExpr { self.0.to_expr() @@ -134,9 +140,6 @@ impl Typed { pub(crate) fn into_typedvalue(self) -> TypedValue { self.0 } - pub(crate) fn to_normalized(&self) -> Normalized { - self.clone().normalize() - } pub(crate) fn as_const(&self) -> Option<Const> { self.0.as_const() } @@ -229,7 +232,7 @@ impl std::hash::Hash for Normalized { impl Eq for Typed {} impl PartialEq for Typed { fn eq(&self, other: &Self) -> bool { - self.to_valuef() == other.to_valuef() + self.0 == other.0 } } diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index 6c65e43..785a75f 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -68,23 +68,23 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { r, EmptyOptionalLit(TypedValue::from_value_simple_type(t.clone())), )), - (NaturalIsZero, [n, r..]) => match &*n.as_valuef() { + (NaturalIsZero, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok((r, BoolLit(*n == 0))), _ => Err(()), }, - (NaturalEven, [n, r..]) => match &*n.as_valuef() { + (NaturalEven, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0))), _ => Err(()), }, - (NaturalOdd, [n, r..]) => match &*n.as_valuef() { + (NaturalOdd, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0))), _ => Err(()), }, - (NaturalToInteger, [n, r..]) => match &*n.as_valuef() { + (NaturalToInteger, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok((r, IntegerLit(*n as isize))), _ => Err(()), }, - (NaturalShow, [n, r..]) => match &*n.as_valuef() { + (NaturalShow, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok(( r, TextLit(vec![InterpolatedTextContents::Text(n.to_string())]), @@ -92,7 +92,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { _ => Err(()), }, (NaturalSubtract, [a, b, r..]) => { - match (&*a.as_valuef(), &*b.as_valuef()) { + match (&*a.as_whnf(), &*b.as_whnf()) { (NaturalLit(a), NaturalLit(b)) => { Ok((r, NaturalLit(if b > a { b - a } else { 0 }))) } @@ -102,7 +102,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { _ => Err(()), } } - (IntegerShow, [n, r..]) => match &*n.as_valuef() { + (IntegerShow, [n, r..]) => match &*n.as_whnf() { IntegerLit(n) => { let s = if *n < 0 { n.to_string() @@ -113,18 +113,18 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { } _ => Err(()), }, - (IntegerToDouble, [n, r..]) => match &*n.as_valuef() { + (IntegerToDouble, [n, r..]) => match &*n.as_whnf() { IntegerLit(n) => Ok((r, DoubleLit(NaiveDouble::from(*n as f64)))), _ => Err(()), }, - (DoubleShow, [n, r..]) => match &*n.as_valuef() { + (DoubleShow, [n, r..]) => match &*n.as_whnf() { DoubleLit(n) => Ok(( r, TextLit(vec![InterpolatedTextContents::Text(n.to_string())]), )), _ => Err(()), }, - (TextShow, [v, r..]) => match &*v.as_valuef() { + (TextShow, [v, r..]) => match &*v.as_whnf() { TextLit(elts) => { match elts.as_slice() { // Empty string literal. @@ -158,33 +158,33 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { } _ => Err(()), }, - (ListLength, [_, l, r..]) => match &*l.as_valuef() { + (ListLength, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(_) => Ok((r, NaturalLit(0))), NEListLit(xs) => Ok((r, NaturalLit(xs.len()))), _ => Err(()), }, - (ListHead, [_, l, r..]) => match &*l.as_valuef() { + (ListHead, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))), NEListLit(xs) => { Ok((r, NEOptionalLit(xs.iter().next().unwrap().clone()))) } _ => Err(()), }, - (ListLast, [_, l, r..]) => match &*l.as_valuef() { + (ListLast, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))), NEListLit(xs) => { Ok((r, NEOptionalLit(xs.iter().rev().next().unwrap().clone()))) } _ => Err(()), }, - (ListReverse, [_, l, r..]) => match &*l.as_valuef() { + (ListReverse, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()))), NEListLit(xs) => { Ok((r, NEListLit(xs.iter().rev().cloned().collect()))) } _ => Err(()), }, - (ListIndexed, [_, l, r..]) => match &*l.as_valuef() { + (ListIndexed, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(t) => { let mut kts = HashMap::new(); kts.insert( @@ -210,11 +210,11 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { } _ => Err(()), }, - (ListBuild, [t, f, r..]) => match &*f.as_valuef() { + (ListBuild, [t, f, r..]) => match &*f.as_whnf() { // fold/build fusion ValueF::AppliedBuiltin(ListFold, args) => { if args.len() >= 2 { - Ok((r, args[1].to_valuef())) + Ok((r, args[1].to_whnf())) } else { // Do we really need to handle this case ? unimplemented!() @@ -237,8 +237,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { )), )), }, - (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_valuef() { - EmptyListLit(_) => Ok((r, nil.to_valuef())), + (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() { + EmptyListLit(_) => Ok((r, nil.to_whnf())), NEListLit(xs) => { let mut v = nil.clone(); for x in xs.iter().rev() { @@ -248,15 +248,15 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { .app_value(v) .into_value(); } - Ok((r, v.to_valuef())) + Ok((r, v.to_whnf())) } _ => Err(()), }, - (OptionalBuild, [t, f, r..]) => match &*f.as_valuef() { + (OptionalBuild, [t, f, r..]) => match &*f.as_whnf() { // fold/build fusion ValueF::AppliedBuiltin(OptionalFold, args) => { if args.len() >= 2 { - Ok((r, args[1].to_valuef())) + Ok((r, args[1].to_whnf())) } else { // Do we really need to handle this case ? unimplemented!() @@ -273,18 +273,16 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { )), )), }, - (OptionalFold, [_, v, _, just, nothing, r..]) => { - match &*v.as_valuef() { - EmptyOptionalLit(_) => Ok((r, nothing.to_valuef())), - NEOptionalLit(x) => Ok((r, just.app_value(x.clone()))), - _ => Err(()), - } - } - (NaturalBuild, [f, r..]) => match &*f.as_valuef() { + (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() { + EmptyOptionalLit(_) => Ok((r, nothing.to_whnf())), + NEOptionalLit(x) => Ok((r, just.app_value(x.clone()))), + _ => Err(()), + }, + (NaturalBuild, [f, r..]) => match &*f.as_whnf() { // fold/build fusion ValueF::AppliedBuiltin(NaturalFold, args) => { if !args.is_empty() { - Ok((r, args[0].to_valuef())) + Ok((r, args[0].to_whnf())) } else { // Do we really need to handle this case ? unimplemented!() @@ -297,8 +295,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { .app_valuef(NaturalLit(0)), )), }, - (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_valuef() { - NaturalLit(0) => Ok((r, zero.to_valuef())), + (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() { + NaturalLit(0) => Ok((r, zero.to_whnf())), NaturalLit(n) => { let fold = ValueF::from_builtin(NaturalFold) .app(NaturalLit(n - 1)) @@ -326,11 +324,11 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { pub(crate) fn apply_any(f: Value, a: Value) -> ValueF { let fallback = |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a)); - let f_borrow = f.as_valuef(); + let f_borrow = f.as_whnf(); match &*f_borrow { ValueF::Lam(x, _, e) => { let val = Typed::from_value_untyped(a); - e.subst_shift(&x.into(), &val).to_valuef() + e.subst_shift(&x.into(), &val).to_whnf() } ValueF::AppliedBuiltin(b, args) => { use std::iter::once; @@ -362,7 +360,7 @@ pub(crate) fn squash_textlit( match contents { Text(s) => crnt_str.push_str(&s), Expr(e) => { - let e_borrow = e.as_valuef(); + let e_borrow = e.as_whnf(); match &*e_borrow { ValueF::TextLit(elts2) => { inner(elts2.iter().cloned(), crnt_str, ret) @@ -520,8 +518,8 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> { BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType, TextLit, }; - let x_borrow = x.as_valuef(); - let y_borrow = y.as_valuef(); + let x_borrow = x.as_whnf(); + let y_borrow = y.as_whnf(); Some(match (o, &*x_borrow, &*y_borrow) { (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y), (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x), @@ -678,7 +676,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { ExprF::SomeLit(e) => Ret::ValueF(NEOptionalLit(e)), ExprF::EmptyListLit(ref t) => { // Check if the type is of the form `List x` - let t_borrow = t.as_valuef(); + let t_borrow = t.as_whnf(); match &*t_borrow { AppliedBuiltin(Builtin::List, args) if args.len() == 1 => { Ret::ValueF(EmptyListLit( @@ -718,13 +716,13 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { } } ExprF::BoolIf(ref b, ref e1, ref e2) => { - let b_borrow = b.as_valuef(); + let b_borrow = b.as_whnf(); match &*b_borrow { BoolLit(true) => Ret::ValueRef(e1), BoolLit(false) => Ret::ValueRef(e2), _ => { - let e1_borrow = e1.as_valuef(); - let e2_borrow = e2.as_valuef(); + let e1_borrow = e1.as_whnf(); + let e2_borrow = e2.as_whnf(); match (&*e1_borrow, &*e2_borrow) { // Simplify `if b then True else False` (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b), @@ -748,7 +746,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { Ret::ValueF(RecordLit(HashMap::new())) } ExprF::Projection(ref v, ref ls) => { - let v_borrow = v.as_valuef(); + let v_borrow = v.as_whnf(); match &*v_borrow { RecordLit(kvs) => Ret::ValueF(RecordLit( ls.iter() @@ -764,7 +762,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { } } ExprF::Field(ref v, ref l) => { - let v_borrow = v.as_valuef(); + let v_borrow = v.as_whnf(); match &*v_borrow { RecordLit(kvs) => match kvs.get(l) { Some(r) => Ret::Value(r.clone()), @@ -784,8 +782,8 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { } ExprF::Merge(ref handlers, ref variant, _) => { - let handlers_borrow = handlers.as_valuef(); - let variant_borrow = variant.as_valuef(); + let handlers_borrow = handlers.as_whnf(); + let variant_borrow = variant.as_whnf(); match (&*handlers_borrow, &*variant_borrow) { (RecordLit(kvs), UnionConstructor(l, _)) => match kvs.get(l) { Some(h) => Ret::Value(h.clone()), @@ -814,8 +812,8 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF { match ret { Ret::ValueF(v) => v, - Ret::Value(th) => th.to_valuef(), - Ret::ValueRef(th) => th.to_valuef(), + Ret::Value(th) => th.as_whnf().clone(), + Ret::ValueRef(th) => th.as_whnf().clone(), Ret::Expr(expr) => ValueF::PartialExpr(expr), } } diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 4154afe..c303ada 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -22,12 +22,7 @@ fn tck_pi_type( let ka = match tx.get_type()?.as_const() { Some(k) => k, - _ => { - return Err(TypeError::new( - ctx, - InvalidInputType(tx.to_normalized()), - )) - } + _ => return Err(TypeError::new(ctx, InvalidInputType(tx))), }; let kb = match te.get_type()?.as_const() { @@ -35,7 +30,7 @@ fn tck_pi_type( _ => { return Err(TypeError::new( &ctx2, - InvalidOutputType(te.get_type()?.to_normalized()), + InvalidOutputType(te.get_type()?.into_owned()), )) } }; @@ -415,18 +410,14 @@ fn type_last_layer( } App(f, a) => { let tf = f.get_type()?; - let (x, tx, tb) = match &tf.to_valuef() { + let (x, tx, tb) = match &*tf.as_whnf() { ValueF::Pi(x, tx, tb) => { (x.clone(), tx.to_type(), tb.to_type()) } _ => return Err(mkerr(NotAFunction(f.clone()))), }; if a.get_type()?.as_ref() != &tx { - return Err(mkerr(TypeMismatch( - f.clone(), - tx.to_normalized(), - a.clone(), - ))); + return Err(mkerr(TypeMismatch(f.clone(), tx, a.clone()))); } Ok(RetTypeOnly(tb.subst_shift(&x.into(), &a))) @@ -434,13 +425,13 @@ fn type_last_layer( Annot(x, t) => { let t = t.to_type(); if &t != x.get_type()?.as_ref() { - return Err(mkerr(AnnotMismatch(x.clone(), t.to_normalized()))); + return Err(mkerr(AnnotMismatch(x.clone(), t))); } Ok(RetTypeOnly(x.get_type()?.into_owned())) } Assert(t) => { - match t.to_valuef() { - ValueF::Equivalence(ref x, ref y) if x == y => {} + match &*t.as_whnf() { + ValueF::Equivalence(x, y) if x == y => {} ValueF::Equivalence(x, y) => { return Err(mkerr(AssertMismatch( x.to_typed(), @@ -472,14 +463,11 @@ fn type_last_layer( } EmptyListLit(t) => { let t = t.to_type(); - match &t.to_valuef() { + match &*t.as_whnf() { ValueF::AppliedBuiltin(dhall_syntax::Builtin::List, args) if args.len() == 1 => {} _ => { - return Err(TypeError::new( - ctx, - InvalidListType(t.to_normalized()), - )) + return Err(TypeError::new(ctx, InvalidListType(t.clone()))) } } Ok(RetTypeOnly(t)) @@ -491,7 +479,7 @@ fn type_last_layer( if x.get_type()? != y.get_type()? { return Err(mkerr(InvalidListElement( i, - x.get_type()?.to_normalized(), + x.get_type()?.into_owned(), y.clone(), ))); } @@ -500,14 +488,14 @@ fn type_last_layer( if t.get_type()?.as_const() != Some(Type) { return Err(TypeError::new( ctx, - InvalidListType(t.to_normalized()), + InvalidListType(t.into_owned()), )); } Ok(RetTypeOnly( Typed::from_value_and_type( ValueF::from_builtin(dhall_syntax::Builtin::List) - .app(t.to_valuef()) + .app_value(t.to_value()) .into_value(), Typed::from_const(Type), ) @@ -517,16 +505,13 @@ fn type_last_layer( SomeLit(x) => { let t = x.get_type()?.into_owned(); if t.get_type()?.as_const() != Some(Type) { - return Err(TypeError::new( - ctx, - InvalidOptionalType(t.to_normalized()), - )); + return Err(TypeError::new(ctx, InvalidOptionalType(t))); } Ok(RetTypeOnly( Typed::from_value_and_type( ValueF::from_builtin(dhall_syntax::Builtin::Optional) - .app(t.to_valuef()) + .app_value(t.to_value()) .into_value(), Typed::from_const(Type).into_type(), ) @@ -551,7 +536,7 @@ fn type_last_layer( .into_type(), )), Field(r, x) => { - match &r.get_type()?.to_valuef() { + match &*r.get_type()?.as_whnf() { ValueF::RecordType(kts) => match kts.get(&x) { Some(tth) => { Ok(RetTypeOnly(tth.to_type())) @@ -561,8 +546,7 @@ fn type_last_layer( }, // TODO: branch here only when r.get_type() is a Const _ => { - let r = r.to_type(); - match &r.to_valuef() { + match &*r.as_whnf() { ValueF::UnionType(kts) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > Some(Some(t)) => { @@ -581,21 +565,21 @@ fn type_last_layer( None => { Err(mkerr(MissingUnionField( x.clone(), - r.to_normalized(), + r.clone(), ))) }, }, _ => { Err(mkerr(NotARecord( x.clone(), - r.to_normalized() + r.clone() ))) }, } } // _ => Err(mkerr(NotARecord( // x, - // r.to_type()?.to_normalized(), + // r.to_type()?, // ))), } } @@ -633,20 +617,22 @@ fn type_last_layer( } // Extract the LHS record type - let kts_x = match l_type.to_valuef() { + let l_type_borrow = l_type.as_whnf(); + let kts_x = match &*l_type_borrow { ValueF::RecordType(kts) => kts, _ => return Err(mkerr(MustCombineRecord(l.clone()))), }; // Extract the RHS record type - let kts_y = match r_type.to_valuef() { + let r_type_borrow = r_type.as_whnf(); + let kts_y = match &*r_type_borrow { ValueF::RecordType(kts) => kts, _ => return Err(mkerr(MustCombineRecord(r.clone()))), }; // Union the two records, prefering // the values found in the RHS. - let kts = merge_maps(&kts_x, &kts_y, |_, r_t| r_t.clone()); + let kts = merge_maps(kts_x, kts_y, |_, r_t| r_t.clone()); // Construct the final record type from the union Ok(RetTypeOnly( @@ -662,8 +648,8 @@ fn type_last_layer( // records of records when merging. fn combine_record_types( ctx: &TypecheckContext, - kts_l: HashMap<Label, TypedValue>, - kts_r: HashMap<Label, TypedValue>, + kts_l: &HashMap<Label, TypedValue>, + kts_r: &HashMap<Label, TypedValue>, ) -> Result<Typed, TypeError> { use crate::phase::normalize::outer_join; @@ -674,7 +660,7 @@ fn type_last_layer( inner_l: &TypedValue, inner_r: &TypedValue| -> Result<Typed, TypeError> { - match (inner_l.to_valuef(), inner_r.to_valuef()) { + match (&*inner_l.as_whnf(), &*inner_r.as_whnf()) { ( ValueF::RecordType(inner_l_kvs), ValueF::RecordType(inner_r_kvs), @@ -690,11 +676,9 @@ fn type_last_layer( let kts: HashMap<Label, Result<Typed, TypeError>> = outer_join( |l| Ok(l.to_type()), |r| Ok(r.to_type()), - |k: &Label, l: &TypedValue, r: &TypedValue| { - combine(k, l, r) - }, - &kts_l, - &kts_r, + combine, + kts_l, + kts_r, ); Ok(tck_record_type( @@ -717,13 +701,15 @@ fn type_last_layer( } // Extract the LHS record type - let kts_x = match l_type.to_valuef() { + let l_type_borrow = l_type.as_whnf(); + let kts_x = match &*l_type_borrow { ValueF::RecordType(kts) => kts, _ => return Err(mkerr(MustCombineRecord(l.clone()))), }; // Extract the RHS record type - let kts_y = match r_type.to_valuef() { + let r_type_borrow = r_type.as_whnf(); + let kts_y = match &*r_type_borrow { ValueF::RecordType(kts) => kts, _ => return Err(mkerr(MustCombineRecord(r.clone()))), }; @@ -735,8 +721,8 @@ fn type_last_layer( // records of records when merging. fn combine_record_types( ctx: &TypecheckContext, - kts_l: HashMap<Label, TypedValue>, - kts_r: HashMap<Label, TypedValue>, + kts_l: &HashMap<Label, TypedValue>, + kts_r: &HashMap<Label, TypedValue>, ) -> Result<Typed, TypeError> { use crate::phase::normalize::intersection_with_key; @@ -747,7 +733,7 @@ fn type_last_layer( kts_l_inner: &TypedValue, kts_r_inner: &TypedValue| -> Result<Typed, TypeError> { - match (kts_l_inner.to_valuef(), kts_r_inner.to_valuef()) { + match (&*kts_l_inner.as_whnf(), &*kts_r_inner.as_whnf()) { ( ValueF::RecordType(kvs_l_inner), ValueF::RecordType(kvs_r_inner), @@ -760,13 +746,7 @@ fn type_last_layer( } }; - let kts = intersection_with_key( - |k: &Label, l: &TypedValue, r: &TypedValue| { - combine(k, l, r) - }, - &kts_l, - &kts_r, - ); + let kts = intersection_with_key(combine, kts_l, kts_r); Ok(tck_record_type( ctx, @@ -776,8 +756,8 @@ fn type_last_layer( }; // Extract the Const of the LHS - let k_l = match l.get_type()?.to_valuef() { - ValueF::Const(k) => k, + let k_l = match l.get_type()?.as_const() { + Some(k) => k, _ => { return Err(mkerr(RecordTypeMergeRequiresRecordType( l.clone(), @@ -786,8 +766,8 @@ fn type_last_layer( }; // Extract the Const of the RHS - let k_r = match r.get_type()?.to_valuef() { - ValueF::Const(k) => k, + let k_r = match r.get_type()?.as_const() { + Some(k) => k, _ => { return Err(mkerr(RecordTypeMergeRequiresRecordType( r.clone(), @@ -808,7 +788,8 @@ fn type_last_layer( }; // Extract the LHS record type - let kts_x = match l.to_valuef() { + let borrow_l = l.as_whnf(); + let kts_x = match &*borrow_l { ValueF::RecordType(kts) => kts, _ => { return Err(mkerr(RecordTypeMergeRequiresRecordType( @@ -818,7 +799,8 @@ fn type_last_layer( }; // Extract the RHS record type - let kts_y = match r.to_valuef() { + let borrow_r = r.as_whnf(); + let kts_y = match &*borrow_r { ValueF::RecordType(kts) => kts, _ => { return Err(mkerr(RecordTypeMergeRequiresRecordType( @@ -833,7 +815,7 @@ fn type_last_layer( .and(Ok(RetTypeOnly(Typed::from_const(k)))) } BinOp(o @ ListAppend, l, r) => { - match l.get_type()?.to_valuef() { + match &*l.get_type()?.as_whnf() { ValueF::AppliedBuiltin(List, _) => {} _ => return Err(mkerr(BinOpTypeMismatch(*o, l.clone()))), } @@ -895,56 +877,63 @@ fn type_last_layer( Ok(RetTypeOnly(t)) } Merge(record, union, type_annot) => { - let handlers = match record.get_type()?.to_valuef() { + let record_type = record.get_type()?; + let record_borrow = record_type.as_whnf(); + let handlers = match &*record_borrow { ValueF::RecordType(kts) => kts, _ => return Err(mkerr(Merge1ArgMustBeRecord(record.clone()))), }; - let variants = match union.get_type()?.to_valuef() { + let union_type = union.get_type()?; + let union_borrow = union_type.as_whnf(); + let variants = match &*union_borrow { ValueF::UnionType(kts) => kts, _ => return Err(mkerr(Merge2ArgMustBeUnion(union.clone()))), }; let mut inferred_type = None; - for (x, handler) in handlers.iter() { - let handler_return_type = match variants.get(x) { - // Union alternative with type - Some(Some(variant_type)) => { - let variant_type = variant_type.to_type(); - let handler_type = handler.to_type(); - let (x, tx, tb) = match &handler_type.to_valuef() { - ValueF::Pi(x, tx, tb) => { - (x.clone(), tx.to_type(), tb.to_type()) + for (x, handler) in handlers { + let handler_return_type = + match variants.get(x) { + // Union alternative with type + Some(Some(variant_type)) => { + let variant_type = variant_type.to_type(); + let handler_type = handler.to_type(); + let (x, tx, tb) = match &*handler_type.as_whnf() { + ValueF::Pi(x, tx, tb) => { + (x.clone(), tx.to_type(), tb.to_type()) + } + _ => { + return Err(mkerr(NotAFunction( + handler_type.clone(), + ))) + } + }; + + if &variant_type != &tx { + return Err(mkerr(TypeMismatch( + handler_type, + tx, + variant_type, + ))); } - _ => return Err(mkerr(NotAFunction(handler_type))), - }; - - if &variant_type != &tx { - return Err(mkerr(TypeMismatch( - handler_type, - tx.to_normalized(), - variant_type, - ))); - } - // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`. - match tb.over_binder(x) { - Some(x) => x, - None => { - return Err(mkerr( + // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`. + match tb.over_binder(x) { + Some(x) => x, + None => return Err(mkerr( MergeHandlerReturnTypeMustNotBeDependent, - )) + )), } } - } - // Union alternative without type - Some(None) => handler.to_type(), - None => { - return Err(mkerr(MergeHandlerMissingVariant( - x.clone(), - ))) - } - }; + // Union alternative without type + Some(None) => handler.to_type(), + None => { + return Err(mkerr(MergeHandlerMissingVariant( + x.clone(), + ))) + } + }; match &inferred_type { None => inferred_type = Some(handler_return_type), Some(t) => { @@ -974,8 +963,9 @@ fn type_last_layer( } } Projection(record, labels) => { - let trecord = record.get_type()?; - let kts = match trecord.to_valuef() { + let record_type = record.get_type()?; + let record_borrow = record_type.as_whnf(); + let kts = match &*record_borrow { ValueF::RecordType(kts) => kts, _ => return Err(mkerr(ProjectionMustBeRecord)), }; @@ -991,7 +981,7 @@ fn type_last_layer( Ok(RetTypeOnly( Typed::from_value_and_type( ValueF::RecordType(new_kts).into_value(), - trecord.get_type()?.into_owned(), + record_type.get_type()?.into_owned(), ) .to_type(), )) |