summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/binary.rs9
-rw-r--r--dhall/src/main.rs7
-rw-r--r--dhall/src/normalize.rs408
-rw-r--r--dhall/src/typecheck.rs548
-rw-r--r--dhall/tests/common/mod.rs18
-rw-r--r--dhall_core/src/core.rs284
-rw-r--r--dhall_generator/src/lib.rs4
7 files changed, 695 insertions, 583 deletions
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<Expr<X, Import>>;
@@ -22,7 +22,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
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<ParsedExpr, DecodeError> {
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<ParsedExpr, DecodeError> {
_ => 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<Expr<_, _>> = 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<S, A>(e: &Expr<S, A>) -> Expr<S, A>
+pub fn normalize_whnf<S, A>(e: &SubExpr<S, A>) -> SubExpr<S, A>
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::<S, S, A>(1, vx0, a);
- let b2 = subst::<S, S, A>(vx0, &a2, &b);
- let b3 = shift::<S, S, A>(-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::<Vec<Expr<_, _>>>()
- .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::<S, S, A>(1, vx0, a);
+ let b2 = subst::<S, S, A>(vx0, &a2, &b);
+ let b3 = shift::<S, S, A>(-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::<Vec<Rc<Expr<_, _>>>>();
+
+ match (
+ b,
+ args.iter()
+ .map(Rc::as_ref)
+ .collect::<Vec<_>>()
+ .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<Expr<_, _>> = 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<Rc<_>> = t1.as_ref().map(Rc::clone);
+ let t2: Option<Rc<_>> = 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<S, T, A>(e: &Expr<S, A>) -> Expr<T, A>
+pub fn normalize<S, T, A>(e: SubExpr<S, A>) -> SubExpr<T, A>
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<S: Clone>(c: core::Const) -> Result<core::Const, TypeError<S>> {
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<core::Const, ()> {
+fn rule(a: &core::Const, b: &core::Const) -> Result<core::Const, ()> {
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<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool
+fn prop_equal<S, T>(eL0: Rc<Expr<S, X>>, eR0: Rc<Expr<T, X>>) -> bool
where
S: Clone + ::std::fmt::Debug,
T: Clone + ::std::fmt::Debug,
{
fn go<S, T>(
ctx: &mut Vec<(Label, Label)>,
- el: &Expr<S, X>,
- er: &Expr<T, X>,
+ el: Rc<Expr<S, X>>,
+ er: Rc<Expr<T, X>>,
) -> 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::<S, T>(&mut ctx, &normalize(eL0), &normalize(eR0))
+ go::<S, T>(&mut ctx, normalize(eL0), normalize(eR0))
}
fn op2_type<S, EF>(
- ctx: &Context<Label, Expr<S, X>>,
- e: &Expr<S, X>,
+ ctx: &Context<Label, Rc<Expr<S, X>>>,
+ e: Rc<Expr<S, X>>,
t: core::Builtin,
ef: EF,
- l: &Expr<S, X>,
- r: &Expr<S, X>,
+ l: &Rc<Expr<S, X>>,
+ r: &Rc<Expr<S, X>>,
) -> Result<Expr<S, X>, TypeError<S>>
where
S: Clone + ::std::fmt::Debug,
- EF: FnOnce(Expr<S, X>, Expr<S, X>) -> TypeMessage<S>,
+ EF: FnOnce(Rc<Expr<S, X>>, Rc<Expr<S, X>>) -> TypeMessage<S>,
{
- 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<S>(
- ctx: &Context<Label, Expr<S, X>>,
- e: &Expr<S, X>,
-) -> Result<Expr<S, X>, TypeError<S>>
+ ctx: &Context<Label, Rc<Expr<S, X>>>,
+ e: Rc<Expr<S, X>>,
+) -> Result<Rc<Expr<S, X>>, TypeError<S>>
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::<S, S, X>(&type_with(ctx, tA)?);
- let kA = match tA2 {
+ let tA2 = normalize::<S, S, X>(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::<S, S, X>(1, vx0, a);
let tB2 = subst(vx0, &a2, &tB);
let tB3 = shift::<S, S, X>(-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::<S, S, X>(&type_with(ctx, &tR)?);
- let kR = match ttR {
+ let tR = type_with(ctx, r.clone())?;
+ let ttR = normalize::<S, S, X>(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::<S, S, X>(&type_with(ctx, &tB)?);
- let kB = match ttB {
+ let tB = type_with(&ctx2, b.clone())?;
+ let ttB = normalize::<S, S, X>(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<Expr<_, _>> = 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::<S, S, X>(&type_with(ctx, t)?);
- match s {
+ let s = normalize::<S, S, X>(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::<S, S, X>(&type_with(ctx, &t)?);
- match s {
+ let t = type_with(ctx, v.clone())?;
+ let s = normalize::<S, S, X>(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::<Result<_, _>>()?;
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<S: Clone + ::std::fmt::Debug>(
- e: &Expr<S, X>,
-) -> Result<Expr<S, X>, TypeError<S>> {
+ e: Rc<Expr<S, X>>,
+) -> Result<Rc<Expr<S, X>>, TypeError<S>> {
let ctx = Context::new();
type_with(&ctx, e) //.map(|e| e.into_owned())
}
@@ -683,64 +729,74 @@ pub fn type_of<S: Clone + ::std::fmt::Debug>(
#[derive(Debug)]
pub enum TypeMessage<S> {
UnboundVariable,
- InvalidInputType(Expr<S, X>),
- InvalidOutputType(Expr<S, X>),
- NotAFunction(Expr<S, X>, Expr<S, X>),
- TypeMismatch(Expr<S, X>, Expr<S, X>, Expr<S, X>, Expr<S, X>),
- AnnotMismatch(Expr<S, X>, Expr<S, X>, Expr<S, X>),
+ InvalidInputType(Rc<Expr<S, X>>),
+ InvalidOutputType(Rc<Expr<S, X>>),
+ NotAFunction(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+ TypeMismatch(
+ Rc<Expr<S, X>>,
+ Rc<Expr<S, X>>,
+ Rc<Expr<S, X>>,
+ Rc<Expr<S, X>>,
+ ),
+ AnnotMismatch(Rc<Expr<S, X>>, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
Untyped,
- InvalidListElement(usize, Expr<S, X>, Expr<S, X>, Expr<S, X>),
+ InvalidListElement(usize, Rc<Expr<S, X>>, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
InvalidListType(Rc<Expr<S, X>>),
- InvalidOptionalElement(Expr<S, X>, Expr<S, X>, Expr<S, X>),
+ InvalidOptionalElement(Rc<Expr<S, X>>, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
InvalidOptionalLiteral(usize),
InvalidOptionalType(Rc<Expr<S, X>>),
- InvalidPredicate(Expr<S, X>, Expr<S, X>),
- IfBranchMismatch(Expr<S, X>, Expr<S, X>, Expr<S, X>, Expr<S, X>),
- IfBranchMustBeTerm(bool, Expr<S, X>, Expr<S, X>, Expr<S, X>),
- InvalidField(Label, Expr<S, X>),
- InvalidFieldType(Label, Expr<S, X>),
- InvalidAlternative(Label, Expr<S, X>),
- InvalidAlternativeType(Label, Expr<S, X>),
+ InvalidPredicate(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+ IfBranchMismatch(
+ Rc<Expr<S, X>>,
+ Rc<Expr<S, X>>,
+ Rc<Expr<S, X>>,
+ Rc<Expr<S, X>>,
+ ),
+ IfBranchMustBeTerm(bool, Rc<Expr<S, X>>, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+ InvalidField(Label, Rc<Expr<S, X>>),
+ InvalidFieldType(Label, Rc<Expr<S, X>>),
+ InvalidAlternative(Label, Rc<Expr<S, X>>),
+ InvalidAlternativeType(Label, Rc<Expr<S, X>>),
DuplicateAlternative(Label),
- MustCombineARecord(Expr<S, X>, Expr<S, X>),
+ MustCombineARecord(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
FieldCollision(Label),
- MustMergeARecord(Expr<S, X>, Expr<S, X>),
- MustMergeUnion(Expr<S, X>, Expr<S, X>),
+ MustMergeARecord(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+ MustMergeUnion(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
UnusedHandler(HashSet<Label>),
MissingHandler(HashSet<Label>),
- HandlerInputTypeMismatch(Label, Expr<S, X>, Expr<S, X>),
- HandlerOutputTypeMismatch(Label, Expr<S, X>, Expr<S, X>),
- HandlerNotAFunction(Label, Expr<S, X>),
- NotARecord(Label, Expr<S, X>, Expr<S, X>),
- MissingField(Label, Expr<S, X>),
- CantAnd(Expr<S, X>, Expr<S, X>),
- CantOr(Expr<S, X>, Expr<S, X>),
- CantEQ(Expr<S, X>, Expr<S, X>),
- CantNE(Expr<S, X>, Expr<S, X>),
- CantTextAppend(Expr<S, X>, Expr<S, X>),
- CantAdd(Expr<S, X>, Expr<S, X>),
- CantMultiply(Expr<S, X>, Expr<S, X>),
- NoDependentLet(Expr<S, X>, Expr<S, X>),
- NoDependentTypes(Expr<S, X>, Expr<S, X>),
+ HandlerInputTypeMismatch(Label, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+ HandlerOutputTypeMismatch(Label, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+ HandlerNotAFunction(Label, Rc<Expr<S, X>>),
+ NotARecord(Label, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+ MissingField(Label, Rc<Expr<S, X>>),
+ CantAnd(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+ CantOr(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+ CantEQ(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+ CantNE(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+ CantTextAppend(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+ CantAdd(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+ CantMultiply(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+ NoDependentLet(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+ NoDependentTypes(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
}
/// A structured type error that includes context
#[derive(Debug)]
pub struct TypeError<S> {
- pub context: Context<Label, Expr<S, X>>,
- pub current: Expr<S, X>,
+ pub context: Context<Label, Rc<Expr<S, X>>>,
+ pub current: Rc<Expr<S, X>>,
pub type_message: TypeMessage<S>,
}
impl<S: Clone> TypeError<S> {
pub fn new(
- context: &Context<Label, Expr<S, X>>,
- current: &Expr<S, X>,
+ context: &Context<Label, Rc<Expr<S, X>>>,
+ current: Rc<Expr<S, X>>,
type_message: TypeMessage<S>,
) -> Self {
TypeError {
context: context.clone(),
- current: current.clone(),
+ current: current,
type_message,
}
}
diff --git a/dhall/tests/common/mod.rs b/dhall/tests/common/mod.rs
index b60262b..4d64fea 100644
--- a/dhall/tests/common/mod.rs
+++ b/dhall/tests/common/mod.rs
@@ -97,25 +97,25 @@ pub fn run_test(base_path: &str, feature: Feature) {
Normalization => {
let expr_file_path = base_path.clone() + "A.dhall";
let expected_file_path = base_path + "B.dhall";
- let expr = read_dhall_file(&expr_file_path).unwrap();
- let expected = read_dhall_file(&expected_file_path).unwrap();
+ let expr = rc(read_dhall_file(&expr_file_path).unwrap());
+ let expected = rc(read_dhall_file(&expected_file_path).unwrap());
assert_eq_display!(
- normalize::<_, X, _>(&expr),
- normalize::<_, X, _>(&expected)
+ normalize::<_, X, _>(expr),
+ normalize::<_, X, _>(expected)
);
}
TypecheckFailure => {
let file_path = base_path + ".dhall";
- let expr = read_dhall_file(&file_path).unwrap();
- typecheck::type_of(&expr).unwrap_err();
+ let expr = rc(read_dhall_file(&file_path).unwrap());
+ typecheck::type_of(expr).unwrap_err();
}
TypecheckSuccess => {
let expr_file_path = base_path.clone() + "A.dhall";
let expected_file_path = base_path + "B.dhall";
- let expr = read_dhall_file(&expr_file_path).unwrap();
- let expected = read_dhall_file(&expected_file_path).unwrap();
- typecheck::type_of(&Expr::Annot(bx(expr), bx(expected))).unwrap();
+ let expr = rc(read_dhall_file(&expr_file_path).unwrap());
+ let expected = rc(read_dhall_file(&expected_file_path).unwrap());
+ typecheck::type_of(rc(Expr::Annot(expr, expected))).unwrap();
}
}
}
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index f5da1df..eba6a42 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -290,6 +290,8 @@ impl<N: Clone, E: Clone> Add for InterpolatedText<N, E> {
}
}
+pub type SubExpr<Note, Embed> = Rc<Expr<Note, Embed>>;
+
/// Syntax tree for expressions
#[derive(Debug, Clone, PartialEq)]
pub enum Expr<Note, Embed> {
@@ -299,33 +301,33 @@ pub enum Expr<Note, Embed> {
/// `Var (V x n) ~ x@n`
Var(V),
/// `Lam x A b ~ λ(x : A) -> b`
- Lam(Label, Rc<Expr<Note, Embed>>, Rc<Expr<Note, Embed>>),
+ Lam(Label, SubExpr<Note, Embed>, SubExpr<Note, Embed>),
/// `Pi "_" A B ~ A -> B`
/// `Pi x A B ~ ∀(x : A) -> B`
- Pi(Label, Rc<Expr<Note, Embed>>, Rc<Expr<Note, Embed>>),
+ Pi(Label, SubExpr<Note, Embed>, SubExpr<Note, Embed>),
/// `App f A ~ f A`
- App(Rc<Expr<Note, Embed>>, Vec<Rc<Expr<Note, Embed>>>),
+ App(SubExpr<Note, Embed>, Vec<SubExpr<Note, Embed>>),
/// `Let x Nothing r e ~ let x = r in e`
/// `Let x (Just t) r e ~ let x : t = r in e`
Let(
Label,
- Option<Rc<Expr<Note, Embed>>>,
- Rc<Expr<Note, Embed>>,
- Rc<Expr<Note, Embed>>,
+ Option<SubExpr<Note, Embed>>,
+ SubExpr<Note, Embed>,
+ SubExpr<Note, Embed>,
),
/// `Annot x t ~ x : t`
- Annot(Rc<Expr<Note, Embed>>, Rc<Expr<Note, Embed>>),
+ Annot(SubExpr<Note, Embed>, SubExpr<Note, Embed>),
/// Built-in values
Builtin(Builtin),
// Binary operations
- BinOp(BinOp, Rc<Expr<Note, Embed>>, Rc<Expr<Note, Embed>>),
+ BinOp(BinOp, SubExpr<Note, Embed>, SubExpr<Note, Embed>),
/// `BoolLit b ~ b`
BoolLit(bool),
/// `BoolIf x y z ~ if x then y else z`
BoolIf(
- Rc<Expr<Note, Embed>>,
- Rc<Expr<Note, Embed>>,
- Rc<Expr<Note, Embed>>,
+ SubExpr<Note, Embed>,
+ SubExpr<Note, Embed>,
+ SubExpr<Note, Embed>,
),
/// `NaturalLit n ~ +n`
NaturalLit(Natural),
@@ -336,35 +338,32 @@ pub enum Expr<Note, Embed> {
/// `TextLit t ~ t`
TextLit(InterpolatedText<Note, Embed>),
/// `ListLit t [x, y, z] ~ [x, y, z] : List t`
- ListLit(Option<Rc<Expr<Note, Embed>>>, Vec<Rc<Expr<Note, Embed>>>),
+ ListLit(Option<SubExpr<Note, Embed>>, Vec<SubExpr<Note, Embed>>),
/// `OptionalLit t [e] ~ [e] : Optional t`
/// `OptionalLit t [] ~ [] : Optional t`
- OptionalLit(
- Option<Rc<Expr<Note, Embed>>>,
- Option<Rc<Expr<Note, Embed>>>,
- ),
+ OptionalLit(Option<SubExpr<Note, Embed>>, Option<SubExpr<Note, Embed>>),
/// `Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 }`
- Record(BTreeMap<Label, Rc<Expr<Note, Embed>>>),
+ Record(BTreeMap<Label, SubExpr<Note, Embed>>),
/// `RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 }`
- RecordLit(BTreeMap<Label, Rc<Expr<Note, Embed>>>),
+ RecordLit(BTreeMap<Label, SubExpr<Note, Embed>>),
/// `Union [(k1, t1), (k2, t2)] ~ < k1 : t1, k2 : t2 >`
- Union(BTreeMap<Label, Rc<Expr<Note, Embed>>>),
+ Union(BTreeMap<Label, SubExpr<Note, Embed>>),
/// `UnionLit (k1, v1) [(k2, t2), (k3, t3)] ~ < k1 = t1, k2 : t2, k3 : t3 >`
UnionLit(
Label,
- Rc<Expr<Note, Embed>>,
- BTreeMap<Label, Rc<Expr<Note, Embed>>>,
+ SubExpr<Note, Embed>,
+ BTreeMap<Label, SubExpr<Note, Embed>>,
),
/// `Merge x y t ~ merge x y : t`
Merge(
- Rc<Expr<Note, Embed>>,
- Rc<Expr<Note, Embed>>,
- Option<Rc<Expr<Note, Embed>>>,
+ SubExpr<Note, Embed>,
+ SubExpr<Note, Embed>,
+ Option<SubExpr<Note, Embed>>,
),
/// `Field e x ~ e.x`
- Field(Rc<Expr<Note, Embed>>, Label),
+ Field(SubExpr<Note, Embed>, Label),
/// Annotation on the AST. Unused for now but could hold e.g. file location information
- Note(Note, Rc<Expr<Note, Embed>>),
+ Note(Note, SubExpr<Note, Embed>),
/// Embeds an import or the result of resolving the import
Embed(Embed),
}
@@ -444,6 +443,31 @@ impl<S, A> Expr<S, A> {
F3: FnOnce(&A) -> B,
F4: Fn(&Label) -> Label,
{
+ map_shallow(
+ self,
+ |x| rc(map_expr(x.as_ref())),
+ map_note,
+ map_embed,
+ map_label,
+ )
+ }
+
+ pub fn map_shallow_rc<T, B, F1, F2, F3, F4>(
+ &self,
+ map_expr: F1,
+ map_note: F2,
+ map_embed: F3,
+ map_label: F4,
+ ) -> Expr<T, B>
+ where
+ A: Clone,
+ T: Clone,
+ S: Clone,
+ F1: Fn(&SubExpr<S, A>) -> SubExpr<T, B>,
+ F2: FnOnce(&S) -> T,
+ F3: FnOnce(&A) -> B,
+ F4: Fn(&Label) -> Label,
+ {
map_shallow(self, map_expr, map_note, map_embed, map_label)
}
@@ -852,10 +876,7 @@ pub fn app<S, A, Ef>(f: Ef, x: Vec<Rc<Expr<S, A>>>) -> Expr<S, A>
where
Ef: Into<Expr<S, A>>,
{
- Expr::App(
- bx(f.into()),
- x,
- )
+ Expr::App(bx(f.into()), x)
}
pub type Double = f64;
@@ -900,58 +921,55 @@ where
A: Clone,
S: Clone,
T: Clone,
- F1: Fn(&Expr<S, A>) -> Expr<T, B>,
+ F1: Fn(&SubExpr<S, A>) -> SubExpr<T, B>,
F2: FnOnce(&S) -> T,
F3: FnOnce(&A) -> B,
F4: Fn(&Label) -> Label,
{
use crate::Expr::*;
- let bxmap = |x: &Expr<S, A>| -> Rc<Expr<T, B>> { bx(map(x)) };
- let bxbxmap = |x: &Rc<Expr<S, A>>| -> Rc<Expr<T, B>> { bx(map(&**x)) };
- let opt = |x| map_opt_box(x, &map);
+ let map = &map;
+ let opt = |x: &Option<_>| x.as_ref().map(&map);
match *e {
Const(k) => Const(k),
Var(V(ref x, n)) => Var(V(map_label(x), n)),
- Lam(ref x, ref t, ref b) => Lam(map_label(x), bxmap(t), bxmap(b)),
- Pi(ref x, ref t, ref b) => Pi(map_label(x), bxmap(t), bxmap(b)),
+ Lam(ref x, ref t, ref b) => Lam(map_label(x), map(t), map(b)),
+ Pi(ref x, ref t, ref b) => Pi(map_label(x), map(t), map(b)),
App(ref f, ref args) => {
- let args = args.iter().map(bxbxmap).collect();
- App(bxmap(f), args)
+ let args = args.iter().map(map).collect();
+ App(map(f), args)
}
Let(ref l, ref t, ref a, ref b) => {
- Let(map_label(l), opt(t), bxmap(a), bxmap(b))
+ Let(map_label(l), opt(t), map(a), map(b))
}
- Annot(ref x, ref t) => Annot(bxmap(x), bxmap(t)),
+ Annot(ref x, ref t) => Annot(map(x), map(t)),
Builtin(v) => Builtin(v),
BoolLit(b) => BoolLit(b),
- BoolIf(ref b, ref t, ref f) => BoolIf(bxmap(b), bxmap(t), bxmap(f)),
+ BoolIf(ref b, ref t, ref f) => BoolIf(map(b), map(t), map(f)),
NaturalLit(n) => NaturalLit(n),
IntegerLit(n) => IntegerLit(n),
DoubleLit(n) => DoubleLit(n),
- TextLit(ref t) => TextLit(t.map(&bxbxmap)),
- BinOp(o, ref x, ref y) => BinOp(o, bxmap(x), bxmap(y)),
+ TextLit(ref t) => TextLit(t.map(&map)),
+ BinOp(o, ref x, ref y) => BinOp(o, map(x), map(y)),
ListLit(ref t, ref es) => {
- let es = es.iter().map(&bxbxmap).collect();
+ let es = es.iter().map(&map).collect();
ListLit(opt(t), es)
}
OptionalLit(ref t, ref es) => OptionalLit(opt(t), opt(es)),
Record(ref kts) => {
- Record(map_record_value_and_keys(kts, bxbxmap, map_label))
+ Record(map_record_value_and_keys(kts, map, map_label))
}
RecordLit(ref kvs) => {
- RecordLit(map_record_value_and_keys(kvs, bxbxmap, map_label))
- }
- Union(ref kts) => {
- Union(map_record_value_and_keys(kts, bxbxmap, map_label))
+ RecordLit(map_record_value_and_keys(kvs, map, map_label))
}
+ Union(ref kts) => Union(map_record_value_and_keys(kts, map, map_label)),
UnionLit(ref k, ref v, ref kvs) => UnionLit(
map_label(k),
- bxmap(v),
- map_record_value_and_keys(kvs, bxbxmap, map_label),
+ map(v),
+ map_record_value_and_keys(kvs, map, map_label),
),
- Merge(ref x, ref y, ref t) => Merge(bxmap(x), bxmap(y), opt(t)),
- Field(ref r, ref x) => Field(bxmap(r), map_label(x)),
- Note(ref n, ref e) => Note(map_note(n), bxmap(e)),
+ Merge(ref x, ref y, ref t) => Merge(map(x), map(y), opt(t)),
+ Field(ref r, ref x) => Field(map(r), map_label(x)),
+ Note(ref n, ref e) => Note(map_note(n), map(e)),
Embed(ref a) => Embed(map_embed(a)),
}
}
@@ -982,13 +1000,6 @@ where
it.into_iter().map(|(k, v)| (g(k), f(v))).collect()
}
-pub fn map_opt_box<T, U, F>(x: &Option<Rc<T>>, f: F) -> Option<Rc<U>>
-where
- F: FnOnce(&T) -> U,
-{
- x.as_ref().map(|x| x.as_ref()).map(f).map(bx)
-}
-
fn map_op2<T, U, V, F, G>(f: F, g: G, a: T, b: T) -> V
where
F: FnOnce(U, U) -> V,
@@ -1068,10 +1079,14 @@ where
/// descend into a lambda or let expression that binds a variable of the same
/// name in order to avoid shifting the bound variables by mistake.
///
-pub fn shift<S, T, A: Clone>(d: isize, v: &V, e: &Expr<S, A>) -> Expr<T, A> {
+pub fn shift<S, T, A: Clone>(
+ d: isize,
+ v: &V,
+ e: &Rc<Expr<S, A>>,
+) -> Rc<Expr<T, A>> {
use crate::Expr::*;
let V(x, n) = v;
- match e {
+ rc(match e.as_ref() {
Const(a) => Const(*a),
Var(V(x2, n2)) => {
let n3 = if x == x2 && n <= n2 {
@@ -1085,80 +1100,68 @@ pub fn shift<S, T, A: Clone>(d: isize, v: &V, e: &Expr<S, A>) -> Expr<T, A> {
let n2 = if x == x2 { n + 1 } else { *n };
let tA2 = shift(d, v, tA);
let b2 = shift(d, &V(x.clone(), n2), b);
- Lam(x2.clone(), bx(tA2), bx(b2))
+ Lam(x2.clone(), tA2, b2)
}
Pi(x2, tA, tB) => {
let n2 = if x == x2 { n + 1 } else { *n };
let tA2 = shift(d, v, tA);
let tB2 = shift(d, &V(x.clone(), n2), tB);
- Pi(x2.clone(), bx(tA2), bx(tB2))
+ Pi(x2.clone(), tA2, tB2)
}
App(f, args) => {
let f = shift(d, v, f);
- let args = args.iter().map(|a| bx(shift(d, v, a))).collect();
- app(f, args)
+ let args = args.iter().map(|a| shift(d, v, a)).collect();
+ App(f, args)
}
Let(f, mt, r, e) => {
let n2 = if x == f { n + 1 } else { *n };
let e2 = shift(d, &V(x.clone(), n2), e);
- let mt2 = mt.as_ref().map(|t| bx(shift(d, v, t)));
+ let mt2 = mt.as_ref().map(|t| shift(d, v, t));
let r2 = shift(d, v, r);
- Let(f.clone(), mt2, bx(r2), bx(e2))
+ Let(f.clone(), mt2, r2, e2)
}
- Annot(a, b) => shift_op2(Annot, d, v, a, b),
+ Annot(a, b) => map_op2(Annot, |x| shift(d, v, x), a, b),
Builtin(v) => Builtin(*v),
BoolLit(a) => BoolLit(*a),
- BinOp(o, a, b) => shift_op2(|x, y| BinOp(*o, x, y), d, v, a, b),
+ BinOp(o, a, b) => {
+ map_op2(|x, y| BinOp(*o, x, y), |x| shift(d, v, x), a, b)
+ }
BoolIf(a, b, c) => {
- BoolIf(bx(shift(d, v, a)), bx(shift(d, v, b)), bx(shift(d, v, c)))
+ BoolIf(shift(d, v, a), shift(d, v, b), shift(d, v, c))
}
NaturalLit(a) => NaturalLit(*a),
IntegerLit(a) => IntegerLit(*a),
DoubleLit(a) => DoubleLit(*a),
- TextLit(a) => TextLit(a.map(|e| bx(shift(d, v, &*e)))),
+ TextLit(a) => TextLit(a.map(|e| shift(d, v, &*e))),
ListLit(t, es) => ListLit(
- t.as_ref().map(|t| bx(shift(d, v, t))),
- es.iter().map(|e| bx(shift(d, v, e))).collect(),
+ t.as_ref().map(|t| shift(d, v, t)),
+ es.iter().map(|e| shift(d, v, e)).collect(),
),
OptionalLit(t, e) => OptionalLit(
- t.as_ref().map(|t| bx(shift(d, v, t))),
- e.as_ref().map(|t| bx(shift(d, v, t))),
+ t.as_ref().map(|t| shift(d, v, t)),
+ e.as_ref().map(|t| shift(d, v, t)),
),
- Record(a) => Record(map_record_value(a, |val| bx(shift(d, v, &*val)))),
+ Record(a) => Record(map_record_value(a, |val| shift(d, v, &*val))),
RecordLit(a) => {
- RecordLit(map_record_value(a, |val| bx(shift(d, v, &*val))))
+ RecordLit(map_record_value(a, |val| shift(d, v, &*val)))
}
- Union(a) => Union(map_record_value(a, |val| bx(shift(d, v, &*val)))),
+ Union(a) => Union(map_record_value(a, |val| shift(d, v, &*val))),
UnionLit(k, uv, a) => UnionLit(
k.clone(),
- bx(shift(d, v, uv)),
- map_record_value(a, |val| bx(shift(d, v, &*val))),
+ shift(d, v, uv),
+ map_record_value(a, |val| shift(d, v, &*val)),
),
Merge(a, b, c) => Merge(
- bx(shift(d, v, a)),
- bx(shift(d, v, b)),
- c.as_ref().map(|c| bx(shift(d, v, c))),
+ shift(d, v, a),
+ shift(d, v, b),
+ c.as_ref().map(|c| shift(d, v, c)),
),
- Field(a, b) => Field(bx(shift(d, v, a)), b.clone()),
- Note(_, b) => shift(d, v, b),
+ Field(a, b) => Field(shift(d, v, a), b.clone()),
+ Note(_, b) => return shift(d, v, b),
// The Dhall compiler enforces that all embedded values are closed expressions
// and `shift` does nothing to a closed expression
Embed(p) => Embed(p.clone()),
- }
-}
-
-fn shift_op2<S, T, A, F>(
- f: F,
- d: isize,
- v: &V,
- a: &Expr<S, A>,
- b: &Expr<S, A>,
-) -> Expr<T, A>
-where
- F: FnOnce(Rc<Expr<T, A>>, Rc<Expr<T, A>>) -> Expr<T, A>,
- A: Clone,
-{
- map_op2(f, |x| bx(shift(d, v, x)), a, b)
+ })
}
/// Substitute all occurrences of a variable with an expression
@@ -1167,37 +1170,41 @@ where
/// subst x C B ~ B[x := C]
/// ```
///
-pub fn subst<S, T, A>(v: &V, e: &Expr<S, A>, b: &Expr<T, A>) -> Expr<S, A>
+pub fn subst<S, T, A>(
+ v: &V,
+ e: &Rc<Expr<S, A>>,
+ b: &Rc<Expr<T, A>>,
+) -> Rc<Expr<S, A>>
where
S: Clone,
A: Clone,
{
use crate::Expr::*;
let V(x, n) = v;
- match b {
+ rc(match b.as_ref() {
Const(a) => Const(*a),
Lam(y, tA, b) => {
let n2 = if x == y { n + 1 } else { *n };
let b2 =
subst(&V(x.clone(), n2), &shift(1, &V(y.clone(), 0), e), b);
let tA2 = subst(v, e, tA);
- Lam(y.clone(), bx(tA2), bx(b2))
+ Lam(y.clone(), tA2, b2)
}
Pi(y, tA, tB) => {
let n2 = if x == y { n + 1 } else { *n };
let tB2 =
subst(&V(x.clone(), n2), &shift(1, &V(y.clone(), 0), e), tB);
let tA2 = subst(v, e, tA);
- Pi(y.clone(), bx(tA2), bx(tB2))
+ Pi(y.clone(), tA2, tB2)
}
App(f, args) => {
let f2 = subst(v, e, f);
- let args = args.iter().map(|a| bx(subst(v, e, a))).collect();
- app(f2, args)
+ let args = args.iter().map(|a| subst(v, e, a)).collect();
+ App(f2, args)
}
Var(v2) => {
if v == v2 {
- e.clone()
+ return e.clone();
} else {
Var(v2.clone())
}
@@ -1206,63 +1213,50 @@ where
let n2 = if x == f { n + 1 } else { *n };
let b2 =
subst(&V(x.clone(), n2), &shift(1, &V(f.clone(), 0), e), b);
- let mt2 = mt.as_ref().map(|t| bx(subst(v, e, t)));
+ let mt2 = mt.as_ref().map(|t| subst(v, e, t));
let r2 = subst(v, e, r);
- Let(f.clone(), mt2, bx(r2), bx(b2))
+ Let(f.clone(), mt2, r2, b2)
}
- Annot(a, b) => subst_op2(Annot, v, e, a, b),
+ Annot(a, b) => map_op2(Annot, |x| subst(v, e, x), a, b),
Builtin(v) => Builtin(*v),
BoolLit(a) => BoolLit(*a),
- BinOp(o, a, b) => subst_op2(|x, y| BinOp(*o, x, y), v, e, a, b),
+ BinOp(o, a, b) => {
+ map_op2(|x, y| BinOp(*o, x, y), |x| subst(v, e, x), a, b)
+ }
BoolIf(a, b, c) => {
- BoolIf(bx(subst(v, e, a)), bx(subst(v, e, b)), bx(subst(v, e, c)))
+ BoolIf(subst(v, e, a), subst(v, e, b), subst(v, e, c))
}
NaturalLit(a) => NaturalLit(*a),
IntegerLit(a) => IntegerLit(*a),
DoubleLit(a) => DoubleLit(*a),
- TextLit(a) => TextLit(a.map(|b| bx(subst(v, e, &*b)))),
+ TextLit(a) => TextLit(a.map(|b| subst(v, e, &*b))),
ListLit(a, b) => {
- let a2 = a.as_ref().map(|a| bx(subst(v, e, a)));
- let b2 = b.iter().map(|be| bx(subst(v, e, be))).collect();
+ let a2 = a.as_ref().map(|a| subst(v, e, a));
+ let b2 = b.iter().map(|be| subst(v, e, be)).collect();
ListLit(a2, b2)
}
OptionalLit(a, b) => {
- let a2 = a.as_ref().map(|a| bx(subst(v, e, a)));
- let b2 = b.as_ref().map(|a| bx(subst(v, e, a)));
+ let a2 = a.as_ref().map(|a| subst(v, e, a));
+ let b2 = b.as_ref().map(|a| subst(v, e, a));
OptionalLit(a2, b2)
}
- Record(kts) => Record(map_record_value(kts, |t| bx(subst(v, e, &*t)))),
+ Record(kts) => Record(map_record_value(kts, |t| subst(v, e, &*t))),
RecordLit(kvs) => {
- RecordLit(map_record_value(kvs, |val| bx(subst(v, e, &*val))))
+ RecordLit(map_record_value(kvs, |val| subst(v, e, &*val)))
}
- Union(kts) => Union(map_record_value(kts, |t| bx(subst(v, e, &*t)))),
+ Union(kts) => Union(map_record_value(kts, |t| subst(v, e, &*t))),
UnionLit(k, uv, kvs) => UnionLit(
k.clone(),
- bx(subst(v, e, uv)),
- map_record_value(kvs, |val| bx(subst(v, e, &*val))),
+ subst(v, e, uv),
+ map_record_value(kvs, |val| subst(v, e, &*val)),
),
Merge(a, b, c) => Merge(
- bx(subst(v, e, a)),
- bx(subst(v, e, b)),
- c.as_ref().map(|c| bx(subst(v, e, c))),
+ subst(v, e, a),
+ subst(v, e, b),
+ c.as_ref().map(|c| subst(v, e, c)),
),
- Field(a, b) => Field(bx(subst(v, e, a)), b.clone()),
- Note(_, b) => subst(v, e, b),
+ Field(a, b) => Field(subst(v, e, a), b.clone()),
+ Note(_, b) => return subst(v, e, b),
Embed(p) => Embed(p.clone()),
- }
-}
-
-fn subst_op2<S, T, A, F>(
- f: F,
- v: &V,
- e: &Expr<S, A>,
- a: &Expr<T, A>,
- b: &Expr<T, A>,
-) -> Expr<S, A>
-where
- F: FnOnce(Rc<Expr<S, A>>, Rc<Expr<S, A>>) -> Expr<S, A>,
- S: Clone,
- A: Clone,
-{
- map_op2(f, |x| bx(subst(v, e, x)), a, b)
+ })
}
diff --git a/dhall_generator/src/lib.rs b/dhall_generator/src/lib.rs
index 26be4c4..9c0aacf 100644
--- a/dhall_generator/src/lib.rs
+++ b/dhall_generator/src/lib.rs
@@ -13,11 +13,11 @@ pub fn dhall_expr(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
let no_import =
|_: &Import| -> X { panic!("Don't use import in dhall!()") };
let expr = expr.map_embed(&no_import);
- let output = dhall_to_tokenstream(&expr, &Context::new());
+ let output = dhall_to_tokenstream_bx(&expr, &Context::new());
output.into()
}
-// Returns an expression of type Expr<_, _>. Expects input variables
+// Returns an expression of type Expr<_, _>. Expects interpolated variables
// to be of type Rc<Expr<_, _>>.
fn dhall_to_tokenstream(
expr: &Expr<X, X>,
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 20:05:27 +0000