From 4c08c603946fa0ac483317d85a71dd1f709eec74 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 17 Mar 2019 22:02:10 +0100 Subject: Use Rc consistently everywhere --- dhall/src/binary.rs | 9 +- dhall/src/main.rs | 7 +- dhall/src/normalize.rs | 408 ++++++++++++++++++++---------------- dhall/src/typecheck.rs | 548 +++++++++++++++++++++++++++---------------------- 4 files changed, 545 insertions(+), 427 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs index 08bdba4..2279a51 100644 --- a/dhall/src/binary.rs +++ b/dhall/src/binary.rs @@ -1,7 +1,7 @@ use dhall_core::*; use itertools::*; -use std::rc::Rc; use serde_cbor::value::value as cbor; +use std::rc::Rc; type ParsedExpr = Rc>; @@ -22,7 +22,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result { use cbor::Value::*; use dhall_core::{BinOp, Builtin, Const}; use Expr::*; - let e = match data { + Ok(rc(match data { String(s) => match Builtin::parse(s) { Some(b) => Expr::Builtin(b), None => match s.as_str() { @@ -198,7 +198,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result { let expr = cbor_value_to_dhall(expr)?; return Ok(bindings .into_iter() - .fold(expr, |acc, (x, t, v)| bx(Let(x, t, v, acc)))); + .fold(expr, |acc, (x, t, v)| rc(Let(x, t, v, acc)))); } [U64(26), x, y] => { let x = cbor_value_to_dhall(&x)?; @@ -208,8 +208,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result { _ => Err(DecodeError::WrongFormatError)?, }, _ => Err(DecodeError::WrongFormatError)?, - }; - Ok(bx(e)) + })) } fn cbor_map_to_dhall_map( diff --git a/dhall/src/main.rs b/dhall/src/main.rs index 3328d99..41953e3 100644 --- a/dhall/src/main.rs +++ b/dhall/src/main.rs @@ -1,5 +1,6 @@ use std::error::Error; use std::io::{self, Read}; +use std::rc::Rc; use term_painter::ToStyle; use dhall::*; @@ -65,9 +66,9 @@ fn main() { } }; - let expr: Expr<_, _> = imports::panic_imports(&expr); + let expr: Rc> = rc(imports::panic_imports(&expr)); - let type_expr = match typecheck::type_of(&expr) { + let type_expr = match typecheck::type_of(expr.clone()) { Err(e) => { let explain = ::std::env::args().any(|s| s == "--explain"); if !explain { @@ -89,5 +90,5 @@ fn main() { println!("{}", type_expr); println!(); - println!("{}", normalize::<_, X, _>(&expr)); + println!("{}", normalize::<_, X, _>(expr)); } diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 40112f1..fccc938 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -9,7 +9,7 @@ use std::rc::Rc; /// Is identical to normalize on primitive types, but not on more complex /// types like functions and records. /// This allows normalization to be lazy. -pub fn normalize_whnf(e: &Expr) -> Expr +pub fn normalize_whnf(e: &SubExpr) -> SubExpr where S: Clone + fmt::Debug, A: Clone + fmt::Debug, @@ -17,158 +17,204 @@ where use dhall_core::BinOp::*; use dhall_core::Builtin::*; use dhall_core::Expr::*; - match e { + rc(match e.as_ref() { Let(f, _, r, b) => { let vf0 = &V(f.clone(), 0); let r2 = shift::<_, S, _>(1, vf0, r); let b2 = subst::<_, S, _>(vf0, &r2, b); let b3 = shift::<_, S, _>(-1, vf0, &b2); - normalize_whnf(&b3) + return normalize_whnf(&b3); } - Annot(x, _) => normalize_whnf(x), - Note(_, e) => normalize_whnf(e), - App(f, args) => match (normalize_whnf(f), args.as_slice()) { - (f, []) => f, - (App(f, args1), args2) => normalize_whnf(&App( - f.clone(), - args1.iter().chain(args2.iter()).cloned().collect(), - )), - (Lam(ref x, _, ref b), [a, rest..]) => { - // Beta reduce - let vx0 = &V(x.clone(), 0); - let a2 = shift::(1, vx0, a); - let b2 = subst::(vx0, &a2, &b); - let b3 = shift::(-1, vx0, &b2); - normalize_whnf(&App(bx(b3), rest.to_vec())) - } - // TODO: this is more normalization than needed - (Builtin(b), args) => match ( - b, - args.iter() - .map(|x| normalize_whnf(&*x)) - .collect::>>() - .as_slice(), - ) { - (OptionalSome, [a]) => OptionalLit(None, Some(bx(a.clone()))), - (OptionalNone, [a]) => OptionalLit(Some(bx(a.clone())), None), - (NaturalIsZero, [NaturalLit(n)]) => BoolLit(*n == 0), - (NaturalEven, [NaturalLit(n)]) => BoolLit(*n % 2 == 0), - (NaturalOdd, [NaturalLit(n)]) => BoolLit(*n % 2 != 0), - (NaturalToInteger, [NaturalLit(n)]) => IntegerLit(*n as isize), - (NaturalShow, [NaturalLit(n)]) => TextLit(n.to_string().into()), - (ListLength, [_, ListLit(_, ys)]) => NaturalLit(ys.len()), - (ListHead, [_, ListLit(t, ys)]) => { - OptionalLit(t.clone(), ys.iter().cloned().next()) - } - (ListLast, [_, ListLit(t, ys)]) => { - OptionalLit(t.clone(), ys.iter().cloned().last()) - } - (ListReverse, [_, ListLit(t, ys)]) => { - let xs = ys.iter().rev().cloned().collect(); - ListLit(t.clone(), xs) + Annot(x, _) => return normalize_whnf(x), + Note(_, e) => return normalize_whnf(e), + App(f, args) => { + let f = normalize_whnf(f); + match (f.as_ref(), args.as_slice()) { + (_, []) => return f, + (App(f, args1), args2) => { + return normalize_whnf(&rc(App( + f.clone(), + args1.iter().chain(args2.iter()).cloned().collect(), + ))) } - (ListBuild, [a0, g]) => { - // fold/build fusion - let g = match g { - App(f, args) => match (&**f, args.as_slice()) { - (Builtin(ListFold), [_, x, rest..]) => { - return normalize_whnf(&App( - x.clone(), - rest.to_vec(), - )) - } - (_, args) => App(f.clone(), args.to_vec()), - }, - g => g.clone(), - }; - let g = bx(g); - let a0 = bx(a0.clone()); - let a1 = bx(shift(1, &V("a".into(), 0), &a0)); - normalize_whnf( - &dhall_expr!(g (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0)), - ) + (Lam(ref x, _, ref b), [a, rest..]) => { + // Beta reduce + let vx0 = &V(x.clone(), 0); + let a2 = shift::(1, vx0, a); + let b2 = subst::(vx0, &a2, &b); + let b3 = shift::(-1, vx0, &b2); + return normalize_whnf(&rc(App(b3, rest.to_vec()))); } - (OptionalBuild, [a0, g]) => { - // fold/build fusion - let g = match g { - App(f, args) => match (&**f, args.as_slice()) { - (Builtin(OptionalFold), [_, x, rest..]) => { - return normalize_whnf(&App( - x.clone(), - rest.to_vec(), - )) + // TODO: this is more normalization than needed + (Builtin(b), args) => { + let args = args + .iter() + .map(|x| normalize_whnf(x)) + .collect::>>>(); + + match ( + b, + args.iter() + .map(Rc::as_ref) + .collect::>() + .as_slice(), + ) { + (OptionalSome, [_]) => { + OptionalLit(None, Some(Rc::clone(&args[0]))) + } + (OptionalNone, [_]) => { + OptionalLit(Some(Rc::clone(&args[0])), None) + } + (NaturalIsZero, [NaturalLit(n)]) => BoolLit(*n == 0), + (NaturalEven, [NaturalLit(n)]) => BoolLit(*n % 2 == 0), + (NaturalOdd, [NaturalLit(n)]) => BoolLit(*n % 2 != 0), + (NaturalToInteger, [NaturalLit(n)]) => { + IntegerLit(*n as isize) + } + (NaturalShow, [NaturalLit(n)]) => { + TextLit(n.to_string().into()) + } + (ListLength, [_, ListLit(_, ys)]) => { + NaturalLit(ys.len()) + } + (ListHead, [_, ListLit(t, ys)]) => { + OptionalLit(t.clone(), ys.iter().cloned().next()) + } + (ListLast, [_, ListLit(t, ys)]) => { + OptionalLit(t.clone(), ys.iter().cloned().last()) + } + (ListReverse, [_, ListLit(t, ys)]) => { + let xs = ys.iter().rev().cloned().collect(); + ListLit(t.clone(), xs) + } + (ListBuild, [_, _]) => { + // fold/build fusion + let g = Rc::clone(&args[1]); + let g = match g.as_ref() { + App(f, args) => { + match (f.as_ref(), args.as_slice()) { + (Builtin(ListFold), [_, x, rest..]) => { + return normalize_whnf(&rc(App( + x.clone(), + rest.to_vec(), + ))) + } + (_, args) => { + rc(App(f.clone(), args.to_vec())) + } + } + } + _ => g, + }; + let a0 = Rc::clone(&args[0]); + let a1 = shift(1, &V("a".into(), 0), &a0); + return normalize_whnf( + &dhall_expr!(g (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0)), + ); + } + (OptionalBuild, [_, _]) => { + // fold/build fusion + let g = Rc::clone(&args[1]); + let g = match g.as_ref() { + App(f, args) => { + match (f.as_ref(), args.as_slice()) { + ( + Builtin(OptionalFold), + [_, x, rest..], + ) => { + return normalize_whnf(&rc(App( + x.clone(), + rest.to_vec(), + ))) + } + (_, args) => { + rc(App(f.clone(), args.to_vec())) + } + } + } + _ => g, + }; + let a0 = Rc::clone(&args[0]); + return normalize_whnf( + &dhall_expr!((g (Optional a0)) (λ(x: a0) -> [x] : Optional a0) ([] : Optional a0)), + ); + } + (ListFold, [_, ListLit(_, xs), _, _, _]) => { + let e2: Rc> = xs.iter().rev().fold( + Rc::clone(&args[4]), + |acc, x| { + let x = x.clone(); + let acc = acc.clone(); + let cons = Rc::clone(&args[3]); + dhall_expr!(cons x acc) + }, + ); + return normalize_whnf(&e2); + } + // // fold/build fusion + // (ListFold, [_, App(box Builtin(ListBuild), [_, x, rest..]), rest..]) => { + // normalize_whnf(&App(bx(x.clone()), rest.to_vec())) + // } + ( + OptionalFold, + [_, OptionalLit(_, Some(x)), _, _, _], + ) => { + let x = x.clone(); + let just = Rc::clone(&args[3]); + return normalize_whnf(&dhall_expr!(just x)); + } + ( + OptionalFold, + [_, OptionalLit(_, None), _, _, nothing], + ) => (*nothing).clone(), + // // fold/build fusion + // (OptionalFold, [_, App(box Builtin(OptionalBuild), [_, x, rest..]), rest..]) => { + // normalize_whnf(&App(bx(x.clone()), rest.to_vec())) + // } + (NaturalBuild, [App(f, args)]) => { + match (f.as_ref(), args.as_slice()) { + // fold/build fusion + (Builtin(NaturalFold), [x, rest..]) => { + return normalize_whnf(&rc(App( + x.clone(), + rest.to_vec(), + ))) + } + (_, args) => app( + Builtin(NaturalBuild), + vec![bx(App(f.clone(), args.to_vec()))], + ), } - (_, args) => App(f.clone(), args.to_vec()), - }, - g => g.clone(), - }; - let g = bx(g); - let a0 = bx(a0.clone()); - normalize_whnf( - &dhall_expr!((g (Optional a0)) (λ(x: a0) -> [x] : Optional a0) ([] : Optional a0)), - ) - } - (ListFold, [_, ListLit(_, xs), _, cons, nil]) => { - let e2: Expr<_, _> = - xs.iter().rev().fold((*nil).clone(), |acc, x| { - let x = (x).clone(); - let acc = bx((acc).clone()); - let cons = bx((cons).clone()); - dhall_expr!(cons x acc) - }); - normalize_whnf(&e2) - } - // // fold/build fusion - // (ListFold, [_, App(box Builtin(ListBuild), [_, x, rest..]), rest..]) => { - // normalize_whnf(&App(bx(x.clone()), rest.to_vec())) - // } - (OptionalFold, [_, OptionalLit(_, Some(x)), _, just, _]) => { - let x = x.clone(); - let just = bx(just.clone()); - normalize_whnf(&dhall_expr!(just x)) - } - (OptionalFold, [_, OptionalLit(_, None), _, _, nothing]) => { - (*nothing).clone() - } - // // fold/build fusion - // (OptionalFold, [_, App(box Builtin(OptionalBuild), [_, x, rest..]), rest..]) => { - // normalize_whnf(&App(bx(x.clone()), rest.to_vec())) - // } - (NaturalBuild, [App(f, args)]) => { - match (&**f, args.as_slice()) { - // fold/build fusion - (Builtin(NaturalFold), [x, rest..]) => { - normalize_whnf(&App(x.clone(), rest.to_vec())) } - (_, args) => app( - Builtin(NaturalBuild), - vec![bx(App(f.clone(), args.to_vec()))], - ), - } - } - (NaturalFold, [App(f, args)]) => { - match (&**f, args.as_slice()) { - // fold/build fusion - (Builtin(NaturalBuild), [x, rest..]) => { - normalize_whnf(&App(x.clone(), rest.to_vec())) + (NaturalFold, [App(f, args)]) => { + match (f.as_ref(), args.as_slice()) { + // fold/build fusion + (Builtin(NaturalBuild), [x, rest..]) => { + return normalize_whnf(&rc(App( + x.clone(), + rest.to_vec(), + ))) + } + (_, args) => app( + Builtin(NaturalFold), + vec![bx(App(f.clone(), args.to_vec()))], + ), + } } - (_, args) => app( - Builtin(NaturalFold), - vec![bx(App(f.clone(), args.to_vec()))], - ), + (b, _) => App(rc(Builtin(*b)), args), } } - (b, args) => { - App(bx(Builtin(b)), args.iter().cloned().map(bx).collect()) - } - }, - (f, args) => App(bx(f), args.to_vec()), - }, - BoolIf(b, t, f) => match normalize_whnf(b) { - BoolLit(true) => normalize_whnf(t), - BoolLit(false) => normalize_whnf(f), - b2 => BoolIf(bx(b2), t.clone(), f.clone()), - }, + (_, args) => App(f, args.to_vec()), + } + } + BoolIf(b, t, f) => { + let b = normalize_whnf(b); + match b.as_ref() { + BoolLit(true) => return normalize_whnf(t), + BoolLit(false) => return normalize_whnf(f), + _ => BoolIf(b, t.clone(), f.clone()), + } + } OptionalLit(t, es) => { if !es.is_none() { OptionalLit(None, es.clone()) @@ -176,36 +222,52 @@ where OptionalLit(t.clone(), es.clone()) } } - BinOp(o, x, y) => match (o, normalize_whnf(&x), normalize_whnf(&y)) { - (BoolAnd, BoolLit(x), BoolLit(y)) => BoolLit(x && y), - (BoolOr, BoolLit(x), BoolLit(y)) => BoolLit(x || y), - (BoolEQ, BoolLit(x), BoolLit(y)) => BoolLit(x == y), - (BoolNE, BoolLit(x), BoolLit(y)) => BoolLit(x != y), - (NaturalPlus, NaturalLit(x), NaturalLit(y)) => NaturalLit(x + y), - (NaturalTimes, NaturalLit(x), NaturalLit(y)) => NaturalLit(x * y), - (TextAppend, TextLit(x), TextLit(y)) => TextLit(x + y), - (ListAppend, ListLit(t1, xs), ListLit(t2, ys)) => { - // Drop type annotation if the result is nonempty - let t = if xs.is_empty() && ys.is_empty() { - t1.or(t2) - } else { - None - }; - let xs = xs.into_iter(); - let ys = ys.into_iter(); - ListLit(t, xs.chain(ys).collect()) + BinOp(o, x, y) => { + let x = normalize_whnf(x); + let y = normalize_whnf(y); + match (o, x.as_ref(), y.as_ref()) { + (BoolAnd, BoolLit(x), BoolLit(y)) => BoolLit(*x && *y), + (BoolOr, BoolLit(x), BoolLit(y)) => BoolLit(*x || *y), + (BoolEQ, BoolLit(x), BoolLit(y)) => BoolLit(x == y), + (BoolNE, BoolLit(x), BoolLit(y)) => BoolLit(x != y), + (NaturalPlus, NaturalLit(x), NaturalLit(y)) => { + NaturalLit(x + y) + } + (NaturalTimes, NaturalLit(x), NaturalLit(y)) => { + NaturalLit(x * y) + } + // TODO: interpolation + (TextAppend, TextLit(x), TextLit(y)) => { + TextLit(x.clone() + y.clone()) + } + (ListAppend, ListLit(t1, xs), ListLit(t2, ys)) => { + let t1: Option> = t1.as_ref().map(Rc::clone); + let t2: Option> = t2.as_ref().map(Rc::clone); + // Drop type annotation if the result is nonempty + let t = if xs.is_empty() && ys.is_empty() { + t1.or(t2) + } else { + None + }; + let xs = xs.into_iter().cloned(); + let ys = ys.into_iter().cloned(); + ListLit(t, xs.chain(ys).collect()) + } + (o, _, _) => BinOp(*o, x, y), + } + } + Field(e, x) => { + let e = normalize_whnf(e); + match (e.as_ref(), x) { + (RecordLit(kvs), x) => match kvs.get(&x) { + Some(r) => return normalize_whnf(r), + None => Field(e, x.clone()), + }, + (_, x) => Field(e, x.clone()), } - (o, x, y) => BinOp(*o, bx(x), bx(y)), - }, - Field(e, x) => match (normalize_whnf(&e), x) { - (RecordLit(kvs), x) => match kvs.get(&x) { - Some(r) => normalize_whnf(r), - None => Field(bx(RecordLit(kvs)), x.clone()), - }, - (e, x) => Field(bx(e), x.clone()), - }, - e => e.clone(), - } + } + _ => return Rc::clone(e), + }) } /// Reduce an expression to its normal form, performing beta reduction @@ -217,16 +279,16 @@ where /// However, `normalize` will not fail if the expression is ill-typed and will /// leave ill-typed sub-expressions unevaluated. /// -pub fn normalize(e: &Expr) -> Expr +pub fn normalize(e: SubExpr) -> SubExpr where S: Clone + fmt::Debug, T: Clone + fmt::Debug, A: Clone + fmt::Debug, { - normalize_whnf(e).map_shallow( - normalize, + rc(normalize_whnf(&e).map_shallow_rc( + |x| normalize(Rc::clone(x)), |_| unreachable!(), |x| x.clone(), |x| x.clone(), - ) + )) } diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index f5670f7..d6195a5 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -4,13 +4,13 @@ use std::collections::HashSet; use std::fmt; use std::rc::Rc; -use crate::normalize; +use crate::normalize::normalize; use dhall_core::context::Context; use dhall_core::core; use dhall_core::core::Builtin::*; use dhall_core::core::Const::*; use dhall_core::core::Expr::*; -use dhall_core::core::{bx, shift, subst, Expr, Label, V, X}; +use dhall_core::core::{bx, rc, shift, subst, Expr, Label, V, X}; use dhall_generator::dhall_expr; use self::TypeMessage::*; @@ -18,11 +18,11 @@ use self::TypeMessage::*; fn axiom(c: core::Const) -> Result> { match c { Type => Ok(Kind), - Kind => Err(TypeError::new(&Context::new(), &Const(Kind), Untyped)), + Kind => Err(TypeError::new(&Context::new(), rc(Const(Kind)), Untyped)), } } -fn rule(a: core::Const, b: core::Const) -> Result { +fn rule(a: &core::Const, b: &core::Const) -> Result { match (a, b) { (Type, Kind) => Err(()), (Kind, Kind) => Ok(Kind), @@ -47,30 +47,30 @@ fn match_vars(vl: &V, vr: &V, ctx: &[(Label, Label)]) -> bool { } } -fn prop_equal(eL0: &Expr, eR0: &Expr) -> bool +fn prop_equal(eL0: Rc>, eR0: Rc>) -> bool where S: Clone + ::std::fmt::Debug, T: Clone + ::std::fmt::Debug, { fn go( ctx: &mut Vec<(Label, Label)>, - el: &Expr, - er: &Expr, + el: Rc>, + er: Rc>, ) -> bool where S: Clone + ::std::fmt::Debug, T: Clone + ::std::fmt::Debug, { - match (el, er) { + match (el.as_ref(), er.as_ref()) { (&Const(Type), &Const(Type)) | (&Const(Kind), &Const(Kind)) => true, - (&Var(ref vL), &Var(ref vR)) => match_vars(vL, vR, &*ctx), + (&Var(ref vL), &Var(ref vR)) => match_vars(vL, vR, ctx), (&Pi(ref xL, ref tL, ref bL), &Pi(ref xR, ref tR, ref bR)) => { //ctx <- State.get - let eq1 = go(ctx, tL, tR); + let eq1 = go(ctx, Rc::clone(tL), Rc::clone(tR)); if eq1 { //State.put ((xL, xR):ctx) ctx.push((xL.clone(), xR.clone())); - let eq2 = go(ctx, bL, bR); + let eq2 = go(ctx, Rc::clone(bL), Rc::clone(bR)); //State.put ctx let _ = ctx.pop(); eq2 @@ -79,8 +79,10 @@ where } } (&App(ref fL, ref aL), &App(ref fR, ref aR)) => { - if go(ctx, fL, fR) { - aL.iter().zip(aR.iter()).all(|(aL, aR)| go(ctx, aL, aR)) + if go(ctx, Rc::clone(fL), Rc::clone(fR)) { + aL.iter() + .zip(aR.iter()) + .all(|(aL, aR)| go(ctx, Rc::clone(aL), Rc::clone(aR))) } else { false } @@ -112,10 +114,9 @@ where } true */ - !ktsL0 - .iter() - .zip(ktsR0.iter()) - .any(|((kL, tL), (kR, tR))| kL != kR || !go(ctx, tL, tR)) + !ktsL0.iter().zip(ktsR0.iter()).any(|((kL, tL), (kR, tR))| { + kL != kR || !go(ctx, Rc::clone(tL), Rc::clone(tR)) + }) } (&Union(ref ktsL0), &Union(ref ktsR0)) => { if ktsL0.len() != ktsR0.len() { @@ -132,40 +133,39 @@ where loop _ _ = return False loop (Data.Map.toList ktsL0) (Data.Map.toList ktsR0) */ - !ktsL0 - .iter() - .zip(ktsR0.iter()) - .any(|((kL, tL), (kR, tR))| kL != kR || !go(ctx, tL, tR)) + !ktsL0.iter().zip(ktsR0.iter()).any(|((kL, tL), (kR, tR))| { + kL != kR || !go(ctx, Rc::clone(tL), Rc::clone(tR)) + }) } (_, _) => false, } } let mut ctx = vec![]; - go::(&mut ctx, &normalize(eL0), &normalize(eR0)) + go::(&mut ctx, normalize(eL0), normalize(eR0)) } fn op2_type( - ctx: &Context>, - e: &Expr, + ctx: &Context>>, + e: Rc>, t: core::Builtin, ef: EF, - l: &Expr, - r: &Expr, + l: &Rc>, + r: &Rc>, ) -> Result, TypeError> where S: Clone + ::std::fmt::Debug, - EF: FnOnce(Expr, Expr) -> TypeMessage, + EF: FnOnce(Rc>, Rc>) -> TypeMessage, { - let tl = normalize(&type_with(ctx, l)?); - match tl { + let tl = normalize(type_with(ctx, l.clone())?); + match *tl { Builtin(lt) if lt == t => {} - _ => return Err(TypeError::new(ctx, e, ef((*l).clone(), tl))), + _ => return Err(TypeError::new(ctx, e, ef(l.clone(), tl))), } - let tr = normalize(&type_with(ctx, r)?); - match tr { + let tr = normalize(type_with(ctx, r.clone())?); + match *tr { Builtin(rt) if rt == t => {} - _ => return Err(TypeError::new(ctx, e, ef((*r).clone(), tr))), + _ => return Err(TypeError::new(ctx, e, ef(r.clone(), tr))), } Ok(Builtin(t)) @@ -178,55 +178,54 @@ where /// is not necessary for just type-checking. If you actually care about the /// returned type then you may want to `normalize` it afterwards. pub fn type_with( - ctx: &Context>, - e: &Expr, -) -> Result, TypeError> + ctx: &Context>>, + e: Rc>, +) -> Result>, TypeError> where S: Clone + ::std::fmt::Debug, { use dhall_core::BinOp::*; use dhall_core::Expr; match *e { - Const(c) => axiom(c).map(Const), //.map(Cow::Owned), + Const(c) => axiom(c).map(Const), Var(V(ref x, n)) => { - ctx.lookup(x, n) + return ctx + .lookup(x, n) .cloned() - //.map(Cow::Borrowed) - .ok_or_else(|| TypeError::new(ctx, e, UnboundVariable)) + .ok_or_else(|| TypeError::new(ctx, e.clone(), UnboundVariable)) } Lam(ref x, ref tA, ref b) => { let ctx2 = ctx - .insert(x.clone(), (**tA).clone()) - .map(|e| core::shift(1, &V(x.clone(), 0), e)); - let tB = type_with(&ctx2, b)?; - let p = Pi(x.clone(), tA.clone(), bx(tB)); - let _ = type_with(ctx, &p)?; - //Ok(Cow::Owned(p)) - Ok(p) + .insert(x.clone(), tA.clone()) + .map(|e| shift(1, &V(x.clone(), 0), e)); + let tB = type_with(&ctx2, b.clone())?; + let p = rc(Pi(x.clone(), tA.clone(), tB)); + let _ = type_with(ctx, p.clone())?; + return Ok(p); } Pi(ref x, ref tA, ref tB) => { - let tA2 = normalize::(&type_with(ctx, tA)?); - let kA = match tA2 { + let tA2 = normalize::(type_with(ctx, tA.clone())?); + let kA = match tA2.as_ref() { Const(k) => k, _ => { return Err(TypeError::new( ctx, - e, - InvalidInputType((**tA).clone()), + e.clone(), + InvalidInputType(tA.clone()), )); } }; let ctx2 = ctx - .insert(x.clone(), (**tA).clone()) - .map(|e| core::shift(1, &V(x.clone(), 0), e)); - let tB = normalize(&type_with(&ctx2, tB)?); - let kB = match tB { + .insert(x.clone(), tA.clone()) + .map(|e| shift(1, &V(x.clone(), 0), e)); + let tB = normalize(type_with(&ctx2, tB.clone())?); + let kB = match tB.as_ref() { Const(k) => k, _ => { return Err(TypeError::new( &ctx2, - e, + e.clone(), InvalidOutputType(tB), )); } @@ -235,184 +234,212 @@ where match rule(kA, kB) { Err(()) => Err(TypeError::new( ctx, - e, - NoDependentTypes((**tA).clone(), tB), + e.clone(), + NoDependentTypes(tA.clone(), tB), )), Ok(k) => Ok(Const(k)), } } App(ref f, ref args) => { let (a, args) = match args.split_last() { - None => return type_with(ctx, f), + None => return type_with(ctx, f.clone()), Some(x) => x, }; let tf = - normalize(&type_with(ctx, &App(f.clone(), args.to_vec()))?); - let (x, tA, tB) = match tf { + normalize(type_with(ctx, rc(App(f.clone(), args.to_vec())))?); + let (x, tA, tB) = match tf.as_ref() { Pi(x, tA, tB) => (x, tA, tB), _ => { return Err(TypeError::new( ctx, - e, - NotAFunction((**f).clone(), tf), + e.clone(), + NotAFunction(f.clone(), tf), )); } }; - let tA2 = type_with(ctx, a)?; - if prop_equal(&tA, &tA2) { - let vx0 = &V(x, 0); + let tA2 = type_with(ctx, a.clone())?; + if prop_equal(tA.clone(), tA2.clone()) { + let vx0 = &V(x.clone(), 0); let a2 = shift::(1, vx0, a); let tB2 = subst(vx0, &a2, &tB); let tB3 = shift::(-1, vx0, &tB2); - Ok(tB3) + return Ok(tB3); } else { - let nf_A = normalize(&tA); - let nf_A2 = normalize(&tA2); + let nf_A = normalize(tA.clone()); + let nf_A2 = normalize(tA2); Err(TypeError::new( ctx, - e, - TypeMismatch((**f).clone(), nf_A, (**a).clone(), nf_A2), + e.clone(), + TypeMismatch(f.clone(), nf_A, a.clone(), nf_A2), )) } } Let(ref f, ref mt, ref r, ref b) => { - let tR = type_with(ctx, r)?; - let ttR = normalize::(&type_with(ctx, &tR)?); - let kR = match ttR { + let tR = type_with(ctx, r.clone())?; + let ttR = normalize::(type_with(ctx, tR.clone())?); + let kR = match ttR.as_ref() { Const(k) => k, // Don't bother to provide a `let`-specific version of this error // message because this should never happen anyway - _ => return Err(TypeError::new(ctx, e, InvalidInputType(tR))), + _ => { + return Err(TypeError::new( + ctx, + e.clone(), + InvalidInputType(tR), + )) + } }; let ctx2 = ctx.insert(f.clone(), tR.clone()); - let tB = type_with(&ctx2, b)?; - let ttB = normalize::(&type_with(ctx, &tB)?); - let kB = match ttB { + let tB = type_with(&ctx2, b.clone())?; + let ttB = normalize::(type_with(ctx, tB.clone())?); + let kB = match ttB.as_ref() { Const(k) => k, // Don't bother to provide a `let`-specific version of this error // message because this should never happen anyway - _ => return Err(TypeError::new(ctx, e, InvalidOutputType(tB))), + _ => { + return Err(TypeError::new( + ctx, + e.clone(), + InvalidOutputType(tB), + )) + } }; if let Err(()) = rule(kR, kB) { - return Err(TypeError::new(ctx, e, NoDependentLet(tR, tB))); + return Err(TypeError::new( + ctx, + e.clone(), + NoDependentLet(tR, tB), + )); } if let Some(ref t) = *mt { - let nf_t = normalize(t); - let nf_tR = normalize(&tR); - if !prop_equal(&nf_tR, &nf_t) { + let nf_t = normalize(t.clone()); + let nf_tR = normalize(tR); + if !prop_equal(nf_tR.clone(), nf_t.clone()) { return Err(TypeError::new( ctx, - e, - AnnotMismatch((**r).clone(), nf_t, nf_tR), + e.clone(), + AnnotMismatch(r.clone(), nf_t, nf_tR), )); } } - Ok(tB) + return Ok(tB); } Annot(ref x, ref t) => { // This is mainly just to check that `t` is not `Kind` - let _ = type_with(ctx, t)?; + let _ = type_with(ctx, t.clone())?; - let t2 = type_with(ctx, x)?; - if prop_equal(t, &t2) { - Ok((**t).clone()) + let t2 = type_with(ctx, x.clone())?; + if prop_equal(t.clone(), t2.clone()) { + return Ok(t.clone()); } else { - let nf_t = normalize(t); - let nf_t2 = normalize(&t2); + let nf_t = normalize(t.clone()); + let nf_t2 = normalize(t2); Err(TypeError::new( ctx, - e, - AnnotMismatch((**x).clone(), nf_t, nf_t2), + e.clone(), + AnnotMismatch(x.clone(), nf_t, nf_t2), )) } } BoolLit(_) => Ok(Builtin(Bool)), - BinOp(BoolAnd, ref l, ref r) => op2_type(ctx, e, Bool, CantAnd, l, r), - BinOp(BoolOr, ref l, ref r) => op2_type(ctx, e, Bool, CantOr, l, r), - BinOp(BoolEQ, ref l, ref r) => op2_type(ctx, e, Bool, CantEQ, l, r), - BinOp(BoolNE, ref l, ref r) => op2_type(ctx, e, Bool, CantNE, l, r), + BinOp(BoolAnd, ref l, ref r) => { + op2_type(ctx, e.clone(), Bool, CantAnd, l, r) + } + BinOp(BoolOr, ref l, ref r) => { + op2_type(ctx, e.clone(), Bool, CantOr, l, r) + } + BinOp(BoolEQ, ref l, ref r) => { + op2_type(ctx, e.clone(), Bool, CantEQ, l, r) + } + BinOp(BoolNE, ref l, ref r) => { + op2_type(ctx, e.clone(), Bool, CantNE, l, r) + } BoolIf(ref x, ref y, ref z) => { - let tx = normalize(&type_with(ctx, x)?); - match tx { + let tx = normalize(type_with(ctx, x.clone())?); + match tx.as_ref() { Builtin(Bool) => {} _ => { return Err(TypeError::new( ctx, - e, - InvalidPredicate((**x).clone(), tx), + e.clone(), + InvalidPredicate(x.clone(), tx), )); } } - let ty = normalize(&type_with(ctx, y)?); - let tty = normalize(&type_with(ctx, &ty)?); - match tty { + let ty = normalize(type_with(ctx, y.clone())?); + let tty = normalize(type_with(ctx, ty.clone())?); + match tty.as_ref() { Const(Type) => {} _ => { return Err(TypeError::new( ctx, - e, - IfBranchMustBeTerm(true, (**y).clone(), ty, tty), + e.clone(), + IfBranchMustBeTerm(true, y.clone(), ty, tty), )); } } - let tz = normalize(&type_with(ctx, z)?); - let ttz = normalize(&type_with(ctx, &tz)?); - match ttz { + let tz = normalize(type_with(ctx, z.clone())?); + let ttz = normalize(type_with(ctx, tz.clone())?); + match ttz.as_ref() { Const(Type) => {} _ => { return Err(TypeError::new( ctx, - e, - IfBranchMustBeTerm(false, (**z).clone(), tz, ttz), + e.clone(), + IfBranchMustBeTerm(false, z.clone(), tz, ttz), )); } } - if !prop_equal(&ty, &tz) { + if !prop_equal(ty.clone(), tz.clone()) { return Err(TypeError::new( ctx, - e, - IfBranchMismatch((**y).clone(), (**z).clone(), ty, tz), + e.clone(), + IfBranchMismatch(y.clone(), z.clone(), ty, tz), )); } - Ok(ty) + return Ok(ty); } NaturalLit(_) => Ok(Builtin(Natural)), - Builtin(NaturalFold) => Ok(dhall_expr!( - Natural -> - forall (natural: Type) -> - forall (succ: natural -> natural) -> - forall (zero: natural) -> - natural - )), - Builtin(NaturalBuild) => Ok(dhall_expr!( - (forall (natural: Type) -> + Builtin(NaturalFold) => { + return Ok(dhall_expr!( + Natural -> + forall (natural: Type) -> forall (succ: natural -> natural) -> forall (zero: natural) -> - natural) -> - Natural - )), + natural + )) + } + Builtin(NaturalBuild) => { + return Ok(dhall_expr!( + (forall (natural: Type) -> + forall (succ: natural -> natural) -> + forall (zero: natural) -> + natural) -> + Natural + )) + } Builtin(NaturalIsZero) | Builtin(NaturalEven) | Builtin(NaturalOdd) => { - Ok(dhall_expr!( + return Ok(dhall_expr!( Natural -> Bool )) } BinOp(NaturalPlus, ref l, ref r) => { - op2_type(ctx, e, Natural, CantAdd, l, r) + op2_type(ctx, e.clone(), Natural, CantAdd, l, r) } BinOp(NaturalTimes, ref l, ref r) => { - op2_type(ctx, e, Natural, CantMultiply, l, r) + op2_type(ctx, e.clone(), Natural, CantMultiply, l, r) } IntegerLit(_) => Ok(Builtin(Integer)), DoubleLit(_) => Ok(Builtin(Double)), TextLit(_) => Ok(Builtin(Text)), BinOp(TextAppend, ref l, ref r) => { - op2_type(ctx, e, Text, CantTextAppend, l, r) + op2_type(ctx, e.clone(), Text, CantTextAppend, l, r) } ListLit(ref t, ref xs) => { let mut iter = xs.iter().enumerate(); @@ -420,117 +447,135 @@ where Some(t) => t.clone(), None => { let (_, first_x) = iter.next().unwrap(); - bx(type_with(ctx, first_x)?) + type_with(ctx, first_x.clone())? } }; - let s = normalize::<_, S, _>(&type_with(ctx, &t)?); - match s { + let s = normalize::<_, S, _>(type_with(ctx, t.clone())?); + match s.as_ref() { Const(Type) => {} - _ => return Err(TypeError::new(ctx, e, InvalidListType(t))), + _ => { + return Err(TypeError::new( + ctx, + e.clone(), + InvalidListType(t), + )) + } } for (i, x) in iter { - let t2 = type_with(ctx, x)?; - if !prop_equal(&t, &t2) { - let nf_t = normalize(&t); - let nf_t2 = normalize(&t2); + let t2 = type_with(ctx, x.clone())?; + if !prop_equal(t.clone(), t2.clone()) { + let nf_t = normalize(t); + let nf_t2 = normalize(t2); return Err(TypeError::new( ctx, - e, - InvalidListElement(i, nf_t, (**x).clone(), nf_t2), + e.clone(), + InvalidListElement(i, nf_t, x.clone(), nf_t2), )); } } - Ok(dhall_expr!(List t)) + return Ok(dhall_expr!(List t)); + } + Builtin(ListBuild) => { + return Ok(dhall_expr!( + forall (a: Type) -> + (forall (list: Type) -> + forall (cons: a -> list -> list) -> + forall (nil: list) -> + list) -> + List a + )) } - Builtin(ListBuild) => Ok(dhall_expr!( - forall (a: Type) -> - (forall (list: Type) -> + Builtin(ListFold) => { + return Ok(dhall_expr!( + forall (a: Type) -> + List a -> + forall (list: Type) -> forall (cons: a -> list -> list) -> forall (nil: list) -> - list) -> - List a - )), - Builtin(ListFold) => Ok(dhall_expr!( - forall (a: Type) -> - List a -> - forall (list: Type) -> - forall (cons: a -> list -> list) -> - forall (nil: list) -> - list - )), + list + )) + } Builtin(ListLength) => { - Ok(dhall_expr!(forall (a: Type) -> List a -> Natural)) + return Ok(dhall_expr!(forall (a: Type) -> List a -> Natural)) } Builtin(ListHead) | Builtin(ListLast) => { - Ok(dhall_expr!(forall (a: Type) -> List a -> Optional a)) - } - Builtin(ListIndexed) => Ok(dhall_expr!( - forall (a: Type) -> - List a -> - List { index: Natural, value: a } - )), - Builtin(ListReverse) => Ok(dhall_expr!( - forall (a: Type) -> List a -> List a - )), + return Ok(dhall_expr!(forall (a: Type) -> List a -> Optional a)) + } + Builtin(ListIndexed) => { + return Ok(dhall_expr!( + forall (a: Type) -> + List a -> + List { index: Natural, value: a } + )) + } + Builtin(ListReverse) => { + return Ok(dhall_expr!( + forall (a: Type) -> List a -> List a + )) + } OptionalLit(ref t, ref xs) => { let mut iter = xs.iter(); let t: Rc> = match t { Some(t) => t.clone(), None => { let x = iter.next().unwrap(); - bx(type_with(ctx, x)?) + type_with(ctx, x.clone())? } }; - let s = normalize::<_, S, _>(&type_with(ctx, &t)?); - match s { + let s = normalize::<_, S, _>(type_with(ctx, t.clone())?); + match s.as_ref() { Const(Type) => {} _ => { return Err(TypeError::new( ctx, - e, + e.clone(), InvalidOptionalType(t), )); } } for x in iter { - let t2 = type_with(ctx, x)?; - if !prop_equal(&t, &t2) { - let nf_t = normalize(&t); - let nf_t2 = normalize(&t2); + let t2 = type_with(ctx, x.clone())?; + if !prop_equal(t.clone(), t2.clone()) { + let nf_t = normalize(t); + let nf_t2 = normalize(t2); return Err(TypeError::new( ctx, - e, - InvalidOptionalElement(nf_t, (**x).clone(), nf_t2), + e.clone(), + InvalidOptionalElement(nf_t, x.clone(), nf_t2), )); } } - Ok(dhall_expr!(Optional t)) - } - Builtin(OptionalFold) => Ok(dhall_expr!( - forall (a: Type) -> - Optional a -> - forall (optional: Type) -> - forall (just: a -> optional) -> - forall (nothing: optional) -> - optional - )), - Builtin(List) | Builtin(Optional) => Ok(dhall_expr!( - Type -> Type - )), + return Ok(dhall_expr!(Optional t)); + } + Builtin(OptionalFold) => { + return Ok(dhall_expr!( + forall (a: Type) -> + Optional a -> + forall (optional: Type) -> + forall (just: a -> optional) -> + forall (nothing: optional) -> + optional + )) + } + Builtin(List) | Builtin(Optional) => { + return Ok(dhall_expr!( + Type -> Type + )) + } Builtin(Bool) | Builtin(Natural) | Builtin(Integer) | Builtin(Double) | Builtin(Text) => Ok(Const(Type)), Record(ref kts) => { for (k, t) in kts { - let s = normalize::(&type_with(ctx, t)?); - match s { + let s = normalize::(type_with(ctx, t.clone())?); + match s.as_ref() { Const(Type) => {} _ => { return Err(TypeError::new( ctx, - e, - InvalidFieldType((*k).clone(), (**t).clone()), + e.clone(), + InvalidFieldType(k.clone(), t.clone()), )); } } @@ -541,19 +586,19 @@ where let kts = kvs .iter() .map(|(k, v)| { - let t = type_with(ctx, v)?; - let s = normalize::(&type_with(ctx, &t)?); - match s { + let t = type_with(ctx, v.clone())?; + let s = normalize::(type_with(ctx, t.clone())?); + match s.as_ref() { Const(Type) => {} _ => { return Err(TypeError::new( ctx, - e, - InvalidField((*k).clone(), (**v).clone()), + e.clone(), + InvalidField(k.clone(), v.clone()), )); } } - Ok(((*k).clone(), bx(t))) + Ok((k.clone(), t)) }) .collect::>()?; Ok(Record(kts)) @@ -640,21 +685,21 @@ where return t */ Field(ref r, ref x) => { - let t = normalize(&type_with(ctx, r)?); - match t { + let t = normalize(type_with(ctx, r.clone())?); + match t.as_ref() { Record(ref kts) => { - kts.get(x).map(|x| &**x).cloned().ok_or_else(|| { + return kts.get(x).cloned().ok_or_else(|| { TypeError::new( ctx, - e, - MissingField((*x).clone(), t.clone()), + e.clone(), + MissingField(x.clone(), t.clone()), ) }) } _ => Err(TypeError::new( ctx, - e, - NotARecord((*x).clone(), (**r).clone(), t.clone()), + e.clone(), + NotARecord(x.clone(), r.clone(), t.clone()), )), } } @@ -667,14 +712,15 @@ where Embed(p) => match p {}, _ => panic!("Unimplemented typecheck case: {:?}", e), } + .map(rc) } /// `typeOf` is the same as `type_with` with an empty context, meaning that the /// expression must be closed (i.e. no free variables), otherwise type-checking /// will fail. pub fn type_of( - e: &Expr, -) -> Result, TypeError> { + e: Rc>, +) -> Result>, TypeError> { let ctx = Context::new(); type_with(&ctx, e) //.map(|e| e.into_owned()) } @@ -683,64 +729,74 @@ pub fn type_of( #[derive(Debug)] pub enum TypeMessage { UnboundVariable, - InvalidInputType(Expr), - InvalidOutputType(Expr), - NotAFunction(Expr, Expr), - TypeMismatch(Expr, Expr, Expr, Expr), - AnnotMismatch(Expr, Expr, Expr), + InvalidInputType(Rc>), + InvalidOutputType(Rc>), + NotAFunction(Rc>, Rc>), + TypeMismatch( + Rc>, + Rc>, + Rc>, + Rc>, + ), + AnnotMismatch(Rc>, Rc>, Rc>), Untyped, - InvalidListElement(usize, Expr, Expr, Expr), + InvalidListElement(usize, Rc>, Rc>, Rc>), InvalidListType(Rc>), - InvalidOptionalElement(Expr, Expr, Expr), + InvalidOptionalElement(Rc>, Rc>, Rc>), InvalidOptionalLiteral(usize), InvalidOptionalType(Rc>), - InvalidPredicate(Expr, Expr), - IfBranchMismatch(Expr, Expr, Expr, Expr), - IfBranchMustBeTerm(bool, Expr, Expr, Expr), - InvalidField(Label, Expr), - InvalidFieldType(Label, Expr), - InvalidAlternative(Label, Expr), - InvalidAlternativeType(Label, Expr), + InvalidPredicate(Rc>, Rc>), + IfBranchMismatch( + Rc>, + Rc>, + Rc>, + Rc>, + ), + IfBranchMustBeTerm(bool, Rc>, Rc>, Rc>), + InvalidField(Label, Rc>), + InvalidFieldType(Label, Rc>), + InvalidAlternative(Label, Rc>), + InvalidAlternativeType(Label, Rc>), DuplicateAlternative(Label), - MustCombineARecord(Expr, Expr), + MustCombineARecord(Rc>, Rc>), FieldCollision(Label), - MustMergeARecord(Expr, Expr), - MustMergeUnion(Expr, Expr), + MustMergeARecord(Rc>, Rc>), + MustMergeUnion(Rc>, Rc>), UnusedHandler(HashSet