diff options
-rw-r--r-- | src/core.rs | 75 | ||||
-rw-r--r-- | src/main.rs | 2 | ||||
-rw-r--r-- | src/typecheck.rs | 34 |
3 files changed, 60 insertions, 51 deletions
diff --git a/src/core.rs b/src/core.rs index 2a0ae1f..5a521b5 100644 --- a/src/core.rs +++ b/src/core.rs @@ -513,6 +513,15 @@ fn add_ui(u: usize, i: isize) -> usize { } } +fn map_record_value<'a, I, K, V, U, F>(it: I, f: F) -> HashMap<K, U> + where I: IntoIterator<Item = (&'a K, &'a V)>, + K: Eq + ::std::hash::Hash + Copy + 'a, + V: 'a, + F: Fn(&V) -> U +{ + it.into_iter().map(|(&k, v)| (k, f(v))).collect() +} + /// `shift` is used by both normalization and type-checking to avoid variable /// capture by shifting variable indices /// @@ -670,11 +679,11 @@ shift d v (OptionalLit a b) = OptionalLit a' b' b' = fmap (shift d v) b */ &Record(ref a) => - Record(a.iter().map(|(&k, val)| (k, shift(d, v, val))).collect()), + Record(map_record_value(a, |val| shift(d, v, val))), &RecordLit(ref a) => - RecordLit(a.iter().map(|(&k, val)| (k, shift(d, v, val))).collect()), + RecordLit(map_record_value(a, |val| shift(d, v, val))), &Union(ref a) => - Union(a.iter().map(|(&k, val)| (k, shift(d, v, val))).collect()), + Union(map_record_value(a, |val| shift(d, v, val))), /* shift d v (UnionLit a b c) = UnionLit a b' c' where @@ -753,8 +762,8 @@ pub fn subst<'i, S, T, A>(v: V<'i>, e: &Expr<'i, S, A>, b: &Expr<'i, T, A>) -> E let b2 = b.iter().map(|be| subst(v, e, be)).collect(); ListLit(bx(a2), b2) } - &Record(ref kts) => Record(kts.iter().map(|(&k, t)| (k, subst(v, e, t))).collect()), - &RecordLit(ref kvs) => Record(kvs.iter().map(|(&k, val)| (k, subst(v, e, val))).collect()), + &Record(ref kts) => Record(map_record_value(kts, |t| subst(v, e, t))), + &RecordLit(ref kvs) => Record(map_record_value(kvs, |val| subst(v, e, val))), &Field(ref a, b) => Field(bx(subst(v, e, a)), b), &Note(_, ref b) => subst(v, e, b), b => panic!("Unimplemented subst case: {:?}", b), @@ -770,7 +779,7 @@ pub fn subst<'i, S, T, A>(v: V<'i>, e: &Expr<'i, S, A>, b: &Expr<'i, T, A>) -> E /// However, `normalize` will not fail if the expression is ill-typed and will /// leave ill-typed sub-expressions unevaluated. /// -pub fn normalize<S, T, A>(e: Expr<S, A>) -> Expr<T, A> +pub fn normalize<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A> where S: Clone + fmt::Debug, T: Clone + fmt::Debug, A: Clone + fmt::Debug, @@ -778,27 +787,27 @@ pub fn normalize<S, T, A>(e: Expr<S, A>) -> Expr<T, A> use BuiltinValue::*; use Expr::*; match e { - Const(k) => Const(k), - Var(v) => Var(v), - Lam(x, tA, b) => { - let tA2 = normalize(*tA); - let b2 = normalize(*b); + &Const(k) => Const(k), + &Var(v) => Var(v), + &Lam(x, ref tA, ref b) => { + let tA2 = normalize(tA); + let b2 = normalize(b); Lam(x, bx(tA2), bx(b2)) } - Pi(x, tA, tB) => { - let tA2 = normalize(*tA); - let tB2 = normalize(*tB); + &Pi(x, ref tA, ref tB) => { + let tA2 = normalize(tA); + let tB2 = normalize(tB); pi(x, tA2, tB2) } - App(f, a) => match normalize::<S, T, A>(*f) { + &App(ref f, ref a) => match normalize::<S, T, A>(f) { Lam(x, _A, b) => { // Beta reduce let vx0 = V(x, 0); - let a2 = shift::<S, S, A>( 1, vx0, &a); + let a2 = shift::<S, S, A>( 1, vx0, a); let b2 = subst::<S, T, A>(vx0, &a2, &b); let b3 = shift::<S, T, A>(-1, vx0, &b2); - normalize(b3) + normalize(&b3) } - f2 => match (f2, normalize::<S, T, A>(*a)) { + f2 => match (f2, normalize::<S, T, A>(a)) { /* -- fold/build fusion for `List` App (App ListBuild _) (App (App ListFold _) e') -> normalize e' @@ -890,31 +899,31 @@ pub fn normalize<S, T, A>(e: Expr<S, A>) -> Expr<T, A> (f2, a2) => app(f2, a2), } }, - Let(f, _, ref r, ref b) => { + &Let(f, _, ref r, ref b) => { let r2 = shift::<_, S, _>( 1, V(f, 0), r); let b2 = subst(V(f, 0), &r2, b); let b3 = shift::<_, T, _>(-1, V(f, 0), &b2); - normalize(b3) + normalize(&b3) } - NaturalLit(n) => NaturalLit(n), - NaturalPlus(x, y) => match (normalize(*x), normalize(*y)) { + &NaturalLit(n) => NaturalLit(n), + &NaturalPlus(ref x, ref y) => match (normalize(x), normalize(y)) { (NaturalLit(xn), NaturalLit(yn)) => NaturalLit(xn + yn), (x2, y2) => NaturalPlus(bx(x2), bx(y2)), }, - IntegerLit(n) => IntegerLit(n), - ListLit(t, es) => { - let t2 = normalize(*t); - let es2 = es.into_iter().map(normalize).collect(); + &IntegerLit(n) => IntegerLit(n), + &ListLit(ref t, ref es) => { + let t2 = normalize(t); + let es2 = es.iter().map(normalize).collect(); ListLit(bx(t2), es2) } - Record(kts) => Record(kts.into_iter().map(|(k, t)| (k, normalize(t))).collect()), - RecordLit(kvs) => Record(kvs.into_iter().map(|(k, v)| (k, normalize(v))).collect()), - BuiltinType(t) => BuiltinType(t), - BuiltinValue(v) => BuiltinValue(v), - Field(r, x) => match normalize(*r) { - RecordLit(kvs) => match kvs.get(x).cloned() { + &Record(ref kts) => Record(map_record_value(kts, normalize)), + &RecordLit(ref kvs) => Record(map_record_value(kvs, normalize)), + &BuiltinType(t) => BuiltinType(t), + &BuiltinValue(v) => BuiltinValue(v), + &Field(ref r, x) => match normalize(r) { + RecordLit(kvs) => match kvs.get(x) { Some(r2) => normalize(r2), - None => Field(bx(RecordLit(kvs.into_iter().map(|(k, v)| (k, normalize(v))).collect())), x), + None => Field(bx(RecordLit(map_record_value(&kvs, normalize))), x), }, r2 => Field(bx(r2), x), }, diff --git a/src/main.rs b/src/main.rs index a4b5408..52a7d9e 100644 --- a/src/main.rs +++ b/src/main.rs @@ -98,7 +98,7 @@ fn main() { }; println!("{}", type_expr); println!(""); - println!("{}", normalize::<_, X, _>(*expr)); + println!("{}", normalize::<_, X, _>(&expr)); /* typeExpr <- case Dhall.TypeCheck.typeOf expr' of Left err -> Control.Exception.throwIO err diff --git a/src/typecheck.rs b/src/typecheck.rs index 6fa9747..ac7e30e 100644 --- a/src/typecheck.rs +++ b/src/typecheck.rs @@ -123,7 +123,7 @@ fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool } } let mut ctx = vec![]; - go::<S, T>(&mut ctx, &normalize(eL0.clone()), &normalize(eR0.clone())) + go::<S, T>(&mut ctx, &normalize(eL0), &normalize(eR0)) } @@ -155,14 +155,14 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>, Ok(p) } &Pi(ref x, ref tA, ref tB) => { - let tA2 = normalize::<S, S, X>(type_with(ctx, tA)?); + let tA2 = normalize::<S, S, X>(&type_with(ctx, tA)?); let kA = match tA2 { Const(k) => k, _ => return Err(TypeError::new(ctx, e, InvalidInputType((**tA).clone()))), }; let ctx2 = ctx.insert(x, (**tA).clone()).map(|e| core::shift(1, V(x, 0), e)); - let tB = normalize(type_with(&ctx2, tB)?); + let tB = normalize(&type_with(&ctx2, tB)?); let kB = match tB { Const(k) => k, _ => return Err(TypeError::new(&ctx2, e, InvalidOutputType(tB))), @@ -174,7 +174,7 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>, } } &App(ref f, ref a) => { - let tf = normalize(type_with(ctx, f)?); + let tf = normalize(&type_with(ctx, f)?); let (x, tA, tB) = match tf { Pi(x, tA, tB) => (x, tA, tB), _ => return Err(TypeError::new(ctx, e, NotAFunction((**f).clone(), tf))), @@ -187,14 +187,14 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>, let tB3 = shift::<S, S, X>(-1, vx0, &tB2); Ok(tB3) } else { - let nf_A = normalize(*tA); - let nf_A2 = normalize(tA2); + let nf_A = normalize(&tA); + let nf_A2 = normalize(&tA2); Err(TypeError::new(ctx, e, 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::<S, S, X>(type_with(ctx, &tR)?); + let ttR = normalize::<S, S, X>(&type_with(ctx, &tR)?); let kR = match ttR { Const(k) => k, // Don't bother to provide a `let`-specific version of this error @@ -204,7 +204,7 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>, let ctx2 = ctx.insert(f, tR.clone()); let tB = type_with(&ctx2, b)?; - let ttB = normalize::<S, S, X>(type_with(ctx, &tB)?); + let ttB = normalize::<S, S, X>(&type_with(ctx, &tB)?); let kB = match ttB { Const(k) => k, // Don't bother to provide a `let`-specific version of this error @@ -217,8 +217,8 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>, } if let &Some(ref t) = mt { - let nf_t = normalize((**t).clone()); - let nf_tR = normalize(tR.clone()); + let nf_t = normalize(t); + let nf_tR = normalize(&tR); if !prop_equal(&nf_tR, &nf_t) { return Err(TypeError::new(ctx, &e, AnnotMismatch((**r).clone(), nf_t, nf_tR))); } @@ -246,13 +246,13 @@ type_with ctx e@(Annot x t ) = do }), &BoolLit(_) => Ok(BuiltinType(Bool)), &BoolAnd(ref l, ref r) => { - let tl = normalize(type_with(ctx, l)?); + let tl = normalize(&type_with(ctx, l)?); match tl { BuiltinType(Bool) => {} _ => return Err(TypeError::new(ctx, e, CantAnd((**l).clone(), tl))), } - let tr = normalize(type_with(ctx, r)?); + let tr = normalize(&type_with(ctx, r)?); match tr { BuiltinType(Bool) => {} _ => return Err(TypeError::new(ctx, e, CantAnd((**r).clone(), tr))), @@ -339,13 +339,13 @@ type_with _ NaturalBuild = do &BuiltinValue(NaturalEven) => Ok(pi("_", Natural, Bool)), &BuiltinValue(NaturalOdd) => Ok(pi("_", Natural, Bool)), &NaturalPlus(ref l, ref r) => { - let tl = normalize(type_with(ctx, l)?); + let tl = normalize(&type_with(ctx, l)?); match tl { BuiltinType(Natural) => {} _ => return Err(TypeError::new(ctx, e, CantAdd((**l).clone(), tl))), } - let tr = normalize(type_with(ctx, r)?); + let tr = normalize(&type_with(ctx, r)?); match tr { BuiltinType(Natural) => {} _ => return Err(TypeError::new(ctx, e, CantAdd((**r).clone(), tr))), @@ -455,7 +455,7 @@ type_with _ OptionalFold = do */ &Record(ref kts) => { for (k, t) in kts { - let s = normalize::<S, S, X>(type_with(ctx, t)?); + let s = normalize::<S, S, X>(&type_with(ctx, t)?); match s { Const(Type) => {} _ => return Err(TypeError::new(ctx, e, InvalidFieldType((*k).to_owned(), (*t).clone()))), @@ -466,7 +466,7 @@ type_with _ OptionalFold = do &RecordLit(ref kvs) => { let kts = kvs.iter().map(|(&k, v)| { let t = type_with(ctx, v)?; - let s = normalize::<S, S, X>(type_with(ctx, &t)?); + let s = normalize::<S, S, X>(&type_with(ctx, &t)?); match s { Const(Type) => {} _ => return Err(TypeError::new(ctx, e, InvalidField((*k).to_owned(), (*v).clone()))), @@ -557,7 +557,7 @@ type_with ctx e@(Merge kvsX kvsY t) = do return t */ &Field(ref r, x) => { - let t = normalize(type_with(ctx, r)?); + let t = normalize(&type_with(ctx, r)?); match &t { &Record(ref kts) => kts.get(x).cloned().ok_or_else(|| TypeError::new(ctx, e, MissingField(x.to_owned(), t.clone()))), |