summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/binary.rs7
-rw-r--r--dhall/src/imports.rs4
-rw-r--r--dhall/src/main.rs3
-rw-r--r--dhall/src/normalize.rs438
-rw-r--r--dhall/src/typecheck.rs117
-rw-r--r--dhall/tests/common/mod.rs2
-rw-r--r--dhall/tests/dhall_type.rs5
7 files changed, 269 insertions, 307 deletions
diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs
index 235a55b..1ba1873 100644
--- a/dhall/src/binary.rs
+++ b/dhall/src/binary.rs
@@ -1,9 +1,8 @@
use dhall_core::*;
use itertools::*;
use serde_cbor::value::value as cbor;
-use std::rc::Rc;
-type ParsedExpr = Rc<Expr<X, Import>>;
+type ParsedExpr = SubExpr<X, Import>;
#[derive(Debug)]
pub enum DecodeError {
@@ -21,10 +20,10 @@ pub fn decode(data: &[u8]) -> Result<ParsedExpr, DecodeError> {
fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
use cbor::Value::*;
use dhall_core::{BinOp, Builtin, Const};
- use Expr::*;
+ use ExprF::*;
Ok(rc(match data {
String(s) => match Builtin::parse(s) {
- Some(b) => Expr::Builtin(b),
+ Some(b) => ExprF::Builtin(b),
None => match s.as_str() {
"True" => BoolLit(true),
"False" => BoolLit(false),
diff --git a/dhall/src/imports.rs b/dhall/src/imports.rs
index 8df4e97..96268ca 100644
--- a/dhall/src/imports.rs
+++ b/dhall/src/imports.rs
@@ -79,9 +79,9 @@ pub fn load_dhall_file(
let resolve = |import: &Import| -> Expr<X, X> {
resolve_import(import, &root).unwrap()
};
- expr.map_embed(&resolve).squash_embed()
+ expr.as_ref().map_embed(&resolve).squash_embed()
} else {
- panic_imports(&expr)
+ panic_imports(expr.as_ref())
};
Ok(expr)
}
diff --git a/dhall/src/main.rs b/dhall/src/main.rs
index 1a2e309..77f558c 100644
--- a/dhall/src/main.rs
+++ b/dhall/src/main.rs
@@ -1,6 +1,5 @@
use std::error::Error;
use std::io::{self, Read};
-use std::rc::Rc;
use term_painter::ToStyle;
use dhall::*;
@@ -66,7 +65,7 @@ fn main() {
}
};
- let expr: Rc<Expr<_, _>> = rc(imports::panic_imports(&expr));
+ let expr: SubExpr<_, _> = rc(imports::panic_imports(expr.as_ref()));
let type_expr = match typecheck::type_of(expr.clone()) {
Err(e) => {
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index d9bd08a..7574c2f 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -2,84 +2,61 @@
use dhall_core::*;
use dhall_generator::dhall_expr;
use std::fmt;
-use std::rc::Rc;
-fn apply_builtin<S, A>(
- b: Builtin,
- mut args: Vec<SubExpr<S, A>>,
-) -> SubExpr<S, A>
+fn apply_builtin<S, A>(b: Builtin, args: &Vec<Expr<S, A>>) -> WhatNext<S, A>
where
- S: fmt::Debug,
- A: fmt::Debug,
+ S: fmt::Debug + Clone,
+ A: fmt::Debug + Clone,
{
use dhall_core::Builtin::*;
- use dhall_core::Expr::*;
- let f = rc(Builtin(b));
- // How many arguments a builtin needs, and which argument
- // should be normalized and pattern-matched
- let (len_consumption, arg_to_eval) = match b {
- OptionalSome => (1, None),
- OptionalNone => (1, None),
- NaturalIsZero => (1, Some(0)),
- NaturalEven => (1, Some(0)),
- NaturalOdd => (1, Some(0)),
- NaturalToInteger => (1, Some(0)),
- NaturalShow => (1, Some(0)),
- ListLength => (2, Some(1)),
- ListHead => (2, Some(1)),
- ListLast => (2, Some(1)),
- ListReverse => (2, Some(1)),
- ListIndexed => (2, Some(1)),
- ListBuild => (2, Some(1)),
- OptionalBuild => (2, Some(1)),
- ListFold => (5, Some(1)),
- OptionalFold => (5, Some(1)),
- NaturalBuild => (1, Some(0)),
- NaturalFold => (4, Some(0)),
- _ => (0, None),
- };
- // Abort if not enough arguments present
- if len_consumption > args.len() {
- return rc(App(f, args));
- }
- // Normalize the important argument
- if let Some(i) = arg_to_eval {
- args[i] = Rc::clone(&normalize_whnf(&args[i]));
- }
- let evaled_arg = arg_to_eval.map(|i| args[i].as_ref());
-
- let ret = match (b, evaled_arg, args.as_slice()) {
- (OptionalSome, _, [x, ..]) => rc(NEOptionalLit(Rc::clone(x))),
- (OptionalNone, _, [t, ..]) => rc(EmptyOptionalLit(Rc::clone(t))),
- (NaturalIsZero, Some(NaturalLit(n)), _) => rc(BoolLit(*n == 0)),
- (NaturalEven, Some(NaturalLit(n)), _) => rc(BoolLit(*n % 2 == 0)),
- (NaturalOdd, Some(NaturalLit(n)), _) => rc(BoolLit(*n % 2 != 0)),
- (NaturalToInteger, Some(NaturalLit(n)), _) => {
- rc(IntegerLit(*n as isize))
+ use dhall_core::ExprF::*;
+ use WhatNext::*;
+ let (ret, rest) = match (b, args.as_slice()) {
+ (OptionalSome, [x, rest..]) => (rc(NEOptionalLit(x.roll())), rest),
+ (OptionalNone, [t, rest..]) => (rc(EmptyOptionalLit(t.roll())), rest),
+ (NaturalIsZero, [NaturalLit(n), rest..]) => {
+ (rc(BoolLit(*n == 0)), rest)
}
- (NaturalShow, Some(NaturalLit(n)), _) => {
- rc(TextLit(n.to_string().into()))
+ (NaturalEven, [NaturalLit(n), rest..]) => {
+ (rc(BoolLit(*n % 2 == 0)), rest)
}
- (ListLength, Some(EmptyListLit(_)), _) => rc(NaturalLit(0)),
- (ListLength, Some(NEListLit(ys)), _) => rc(NaturalLit(ys.len())),
- (ListHead, Some(EmptyListLit(t)), _) => rc(EmptyOptionalLit(t.clone())),
- (ListHead, Some(NEListLit(ys)), _) => {
- rc(NEOptionalLit(ys.first().unwrap().clone()))
+ (NaturalOdd, [NaturalLit(n), rest..]) => {
+ (rc(BoolLit(*n % 2 != 0)), rest)
}
- (ListLast, Some(EmptyListLit(t)), _) => rc(EmptyOptionalLit(t.clone())),
- (ListLast, Some(NEListLit(ys)), _) => {
- rc(NEOptionalLit(ys.last().unwrap().clone()))
+ (NaturalToInteger, [NaturalLit(n), rest..]) => {
+ (rc(IntegerLit(*n as isize)), rest)
}
- (ListReverse, Some(EmptyListLit(t)), _) => rc(EmptyListLit(t.clone())),
- (ListReverse, Some(NEListLit(ys)), _) => {
- let ys = ys.iter().rev().cloned().collect();
- rc(NEListLit(ys))
+ (NaturalShow, [NaturalLit(n), rest..]) => {
+ (rc(TextLit(n.to_string().into())), rest)
+ }
+ (ListLength, [_, EmptyListLit(_), rest..]) => (rc(NaturalLit(0)), rest),
+ (ListLength, [_, NEListLit(ys), rest..]) => {
+ (rc(NaturalLit(ys.len())), rest)
+ }
+ (ListHead, [_, EmptyListLit(t), rest..]) => {
+ (rc(EmptyOptionalLit(t.clone())), rest)
+ }
+ (ListHead, [_, NEListLit(ys), rest..]) => {
+ (rc(NEOptionalLit(ys.first().unwrap().clone())), rest)
}
- (ListIndexed, Some(EmptyListLit(t)), _) => {
- let t = Rc::clone(t);
- dhall_expr!([] : List ({ index : Natural, value : t }))
+ (ListLast, [_, EmptyListLit(t), rest..]) => {
+ (rc(EmptyOptionalLit(t.clone())), rest)
}
- (ListIndexed, Some(NEListLit(xs)), _) => {
+ (ListLast, [_, NEListLit(ys), rest..]) => {
+ (rc(NEOptionalLit(ys.last().unwrap().clone())), rest)
+ }
+ (ListReverse, [_, EmptyListLit(t), rest..]) => {
+ (rc(EmptyListLit(t.clone())), rest)
+ }
+ (ListReverse, [_, NEListLit(ys), rest..]) => {
+ let ys = ys.iter().rev().cloned().collect();
+ (rc(NEListLit(ys)), rest)
+ }
+ (ListIndexed, [_, EmptyListLit(t), rest..]) => (
+ dhall_expr!([] : List ({ index : Natural, value : t })),
+ rest,
+ ),
+ (ListIndexed, [_, NEListLit(xs), rest..]) => {
let xs = xs
.iter()
.cloned()
@@ -89,100 +66,110 @@ where
dhall_expr!({ index = i, value = e })
})
.collect();
- rc(NEListLit(xs))
+ (rc(NEListLit(xs)), rest)
}
- (ListBuild, _, [a0, g, ..]) => {
+ (ListBuild, [a0, g, rest..]) => {
loop {
- if let App(f2, args2) = g.as_ref() {
- if let (Builtin(ListFold), [_, x, rest..]) =
+ if let App(f2, args2) = g {
+ if let (Builtin(ListFold), [_, x, rest_inner..]) =
(f2.as_ref(), args2.as_slice())
{
// fold/build fusion
- break rc(App(x.clone(), rest.to_vec()));
+ break (rc(App(x.clone(), rest_inner.to_vec())), rest);
}
};
- let a0 = Rc::clone(a0);
+ let a0 = a0.roll();
let a1 = shift(1, &V("a".into(), 0), &a0);
- // TODO: use Embed to avoid reevaluating g
- break dhall_expr!(
- g
- (List a0)
- (λ(x : a0) -> λ(xs : List a1) -> [ x ] # xs)
- ([] : List a0)
+ let g = g.roll();
+ break (
+ dhall_expr!(
+ g
+ (List a0)
+ (λ(x : a0) -> λ(xs : List a1) -> [ x ] # xs)
+ ([] : List a0)
+ ),
+ rest,
);
}
}
- (OptionalBuild, _, [a0, g, ..]) => {
+ (OptionalBuild, [a0, g, rest..]) => {
loop {
- if let App(f2, args2) = g.as_ref() {
- if let (Builtin(OptionalFold), [_, x, rest..]) =
+ if let App(f2, args2) = g {
+ if let (Builtin(OptionalFold), [_, x, rest_inner..]) =
(f2.as_ref(), args2.as_slice())
{
// fold/build fusion
- break rc(App(x.clone(), rest.to_vec()));
+ break (rc(App(x.clone(), rest_inner.to_vec())), rest);
}
};
- let a0 = Rc::clone(a0);
- // TODO: use Embed to avoid reevaluating g
- break dhall_expr!(
- g
- (Optional a0)
- (λ(x: a0) -> Some x)
- (None a0)
+ let a0 = a0.roll();
+ let g = g.roll();
+ break (
+ dhall_expr!(
+ g
+ (Optional a0)
+ (λ(x: a0) -> Some x)
+ (None a0)
+ ),
+ rest,
);
}
}
- (ListFold, Some(EmptyListLit(_)), [_, _, _, _, nil, ..]) => {
- Rc::clone(nil)
+ (ListFold, [_, EmptyListLit(_), _, _, nil, rest..]) => {
+ (nil.roll(), rest)
}
- (ListFold, Some(NEListLit(xs)), [_, _, _, cons, nil, ..]) => {
- xs.iter().rev().fold(Rc::clone(nil), |acc, x| {
+ (ListFold, [_, NEListLit(xs), _, cons, nil, rest..]) => (
+ xs.iter().rev().fold(nil.roll(), |acc, x| {
let x = x.clone();
let acc = acc.clone();
- let cons = Rc::clone(cons);
+ let cons = cons.roll();
dhall_expr!(cons x acc)
- })
- }
+ }),
+ rest,
+ ),
// // fold/build fusion
// (ListFold, [_, App(box Builtin(ListBuild), [_, x, rest..]), rest..]) => {
- // normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
+ // normalize_ref(&App(bx(x.clone()), rest.to_vec()))
// }
- (OptionalFold, Some(NEOptionalLit(x)), [_, _, _, just, _, ..]) => {
+ (OptionalFold, [_, NEOptionalLit(x), _, just, _, rest..]) => {
let x = x.clone();
- let just = Rc::clone(just);
- dhall_expr!(just x)
+ let just = just.roll();
+ (dhall_expr!(just x), rest)
+ }
+ (OptionalFold, [_, EmptyOptionalLit(_), _, _, nothing, rest..]) => {
+ (nothing.roll(), rest)
}
- (
- OptionalFold,
- Some(EmptyOptionalLit(_)),
- [_, _, _, _, nothing, ..],
- ) => Rc::clone(nothing),
// // fold/build fusion
// (OptionalFold, [_, App(box Builtin(OptionalBuild), [_, x, rest..]), rest..]) => {
- // normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
+ // normalize_ref(&App(bx(x.clone()), rest.to_vec()))
// }
- (NaturalBuild, _, [g, ..]) => {
+ (NaturalBuild, [g, rest..]) => {
loop {
- if let App(f2, args2) = g.as_ref() {
- if let (Builtin(NaturalFold), [x, rest..]) =
+ if let App(f2, args2) = g {
+ if let (Builtin(NaturalFold), [x, rest_inner..]) =
(f2.as_ref(), args2.as_slice())
{
// fold/build fusion
- break rc(App(x.clone(), rest.to_vec()));
+ break (rc(App(x.clone(), rest_inner.to_vec())), rest);
}
};
- // TODO: use Embed to avoid reevaluating g
- break dhall_expr!(g Natural (λ(x : Natural) -> x + 1) 0);
+ let g = g.roll();
+ break (
+ dhall_expr!(g Natural (λ(x : Natural) -> x + 1) 0),
+ rest,
+ );
}
}
- (NaturalFold, Some(NaturalLit(0)), [_, _, _, zero]) => Rc::clone(zero),
- (NaturalFold, Some(NaturalLit(n)), [_, t, succ, zero]) => {
+ (NaturalFold, [NaturalLit(0), _, _, zero, rest..]) => {
+ (zero.roll(), rest)
+ }
+ (NaturalFold, [NaturalLit(n), t, succ, zero, rest..]) => {
let fold = rc(Builtin(NaturalFold));
let n = rc(NaturalLit(n - 1));
- let t = Rc::clone(t);
- let succ = Rc::clone(succ);
- let zero = Rc::clone(zero);
- dhall_expr!(succ (fold n t succ zero))
+ let t = t.roll();
+ let succ = succ.roll();
+ let zero = zero.roll();
+ (dhall_expr!(succ (fold n t succ zero)), rest)
}
// (NaturalFold, Some(App(f2, args2)), _) => {
// match (f2.as_ref(), args2.as_slice()) {
@@ -193,140 +180,127 @@ where
// _ => return rc(App(f, args)),
// }
// }
- _ => return rc(App(f, args)),
+ _ => return DoneAsIs,
};
// Put the remaining arguments back and eval again. In most cases
// ret will not be of a form that can be applied, so this won't go very deep.
// In lots of cases, there are no remaining args so this cann will just return ret.
- normalize_whnf(&rc(Expr::App(ret, args.split_off(len_consumption))))
+ let rest: Vec<SubExpr<S, A>> = rest.iter().map(ExprF::roll).collect();
+ Continue(ExprF::App(ret, rest))
}
-/// Reduce an expression to its weak head normal form, i.e. normalize
-/// just enough to get the first constructor of the final expression
-/// 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: &SubExpr<S, A>) -> SubExpr<S, A>
+// Small enum to help with being DRY
+enum WhatNext<'a, S, A> {
+ // Recurse on this expression
+ Continue(Expr<S, A>),
+ ContinueSub(SubExpr<S, A>),
+ // The following expression is the normal form
+ Done(Expr<S, A>),
+ DoneRef(&'a Expr<S, A>),
+ DoneRefSub(&'a SubExpr<S, A>),
+ // The current expression is already in normal form
+ DoneAsIs,
+}
+
+pub fn normalize_ref<S, A>(expr: &Expr<S, A>) -> Expr<S, A>
where
- S: fmt::Debug,
- A: fmt::Debug,
+ S: fmt::Debug + Clone,
+ A: fmt::Debug + Clone,
{
use dhall_core::BinOp::*;
- use dhall_core::Expr::*;
- match e.as_ref() {
+ use dhall_core::ExprF::*;
+ // Recursively normalize all subexpressions
+ let expr: ExprF<Expr<S, A>, Label, S, A> =
+ expr.map_ref_simple(|e| normalize_ref(e.as_ref()));
+
+ use WhatNext::*;
+ let what_next = match &expr {
Let(f, _, r, b) => {
let vf0 = &V(f.clone(), 0);
- let r2 = shift(1, vf0, r);
+ let r2 = shift(1, vf0, &r.roll());
// TODO: use a context
- let b2 = subst(vf0, &r2, b);
+ let b2 = subst(vf0, &r2, &b.roll());
// TODO: add tests sensitive to shift errors before
// trying anything
let b3 = shift(-1, vf0, &b2);
- normalize_whnf(&b3)
- }
- Annot(x, _) => normalize_whnf(x),
- Note(_, e) => normalize_whnf(e),
- App(f, args) => {
- let f = normalize_whnf(f);
- match (f.as_ref(), args.as_slice()) {
- (_, []) => f,
- // TODO: use Embed to avoid reevaluating f
- (App(f, args1), args2) => normalize_whnf(&rc(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(&rc(App(b3, rest.to_vec())))
- }
- (Builtin(b), _) => apply_builtin(*b, args.to_vec()),
- _ => rc(App(f, args.to_vec())),
- }
+ ContinueSub(b3)
}
- BoolIf(b, t, f) => {
- let b = normalize_whnf(b);
- match b.as_ref() {
- BoolLit(true) => normalize_whnf(t),
- BoolLit(false) => normalize_whnf(f),
- _ => rc(BoolIf(b, t.clone(), f.clone())),
- }
+ Annot(x, _) => DoneRef(x),
+ Note(_, e) => DoneRef(e),
+ App(f, args) if args.is_empty() => DoneRef(f),
+ App(App(f, args1), args2) => Continue(App(
+ f.clone(),
+ args1
+ .iter()
+ .cloned()
+ .chain(args2.iter().map(ExprF::roll))
+ .collect(),
+ )),
+ App(Builtin(b), args) => apply_builtin(*b, args),
+ App(Lam(x, _, b), args) => {
+ let mut iter = args.iter();
+ // We know args is nonempty
+ let a = iter.next().unwrap();
+ // Beta reduce
+ let vx0 = &V(x.clone(), 0);
+ let a2 = shift(1, vx0, &a.roll());
+ let b2 = subst(vx0, &a2, &b);
+ let b3 = shift(-1, vx0, &b2);
+ Continue(App(b3, iter.map(ExprF::roll).collect()))
}
+ BoolIf(BoolLit(true), t, _) => DoneRef(t),
+ BoolIf(BoolLit(false), _, f) => DoneRef(f),
// TODO: interpolation
// TextLit(t) =>
- BinOp(o, x, y) => {
- let x = normalize_whnf(x);
- let y = normalize_whnf(y);
- rc(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)
- }
- (TextAppend, TextLit(x), TextLit(y)) => TextLit(x + y),
- (ListAppend, EmptyListLit(t), EmptyListLit(_)) => {
- EmptyListLit(Rc::clone(t))
- }
- (ListAppend, EmptyListLit(_), _) => return y,
- (ListAppend, _, EmptyListLit(_)) => return x,
- (ListAppend, NEListLit(xs), NEListLit(ys)) => {
- let xs = xs.into_iter().cloned();
- let ys = ys.into_iter().cloned();
- NEListLit(xs.chain(ys).collect())
- }
- (o, _, _) => BinOp(*o, x, y),
- })
+ BinOp(BoolAnd, BoolLit(x), BoolLit(y)) => Done(BoolLit(*x && *y)),
+ BinOp(BoolOr, BoolLit(x), BoolLit(y)) => Done(BoolLit(*x || *y)),
+ BinOp(BoolEQ, BoolLit(x), BoolLit(y)) => Done(BoolLit(x == y)),
+ BinOp(BoolNE, BoolLit(x), BoolLit(y)) => Done(BoolLit(x != y)),
+ BinOp(NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
+ Done(NaturalLit(x + y))
}
- Merge(x, y, t) => {
- let x = normalize_whnf(x);
- let y = normalize_whnf(y);
- match (x.as_ref(), y.as_ref()) {
- (RecordLit(handlers), UnionLit(k, v, _)) => {
- match handlers.get(&k) {
- Some(h) => {
- normalize_whnf(&rc(App(h.clone(), vec![v.clone()])))
- }
- None => rc(Merge(x, y, t.clone())),
- }
- }
- _ => rc(Merge(x, y, t.clone())),
- }
+ BinOp(NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
+ Done(NaturalLit(x * y))
}
- Field(e, l) => {
- let e = normalize_whnf(e);
- match e.as_ref() {
- RecordLit(kvs) => match kvs.get(&l) {
- Some(r) => normalize_whnf(r),
- None => rc(Field(e, l.clone())),
- },
- _ => rc(Field(e, l.clone())),
- }
+ BinOp(TextAppend, TextLit(x), TextLit(y)) => Done(TextLit(x + y)),
+ BinOp(ListAppend, EmptyListLit(t), EmptyListLit(_)) => {
+ Done(EmptyListLit(SubExpr::clone(t)))
}
- Projection(_, ls) if ls.is_empty() => {
- rc(RecordLit(std::collections::BTreeMap::new()))
+ BinOp(ListAppend, EmptyListLit(_), y) => DoneRef(y),
+ BinOp(ListAppend, x, EmptyListLit(_)) => DoneRef(x),
+ BinOp(ListAppend, NEListLit(xs), NEListLit(ys)) => {
+ let xs = xs.into_iter().cloned();
+ let ys = ys.into_iter().cloned();
+ Done(NEListLit(xs.chain(ys).collect()))
}
- Projection(e, ls) => {
- let e = normalize_whnf(e);
- match e.as_ref() {
- RecordLit(kvs) => rc(RecordLit(
- ls.iter()
- .filter_map(|l| {
- kvs.get(l).map(|x| (l.clone(), x.clone()))
- })
- .collect(),
- )),
- _ => rc(Projection(e, ls.clone())),
+ Merge(RecordLit(handlers), UnionLit(k, v, _), _) => {
+ match handlers.get(&k) {
+ Some(h) => Continue(App(h.clone(), vec![v.clone()])),
+ None => DoneAsIs,
}
}
- _ => Rc::clone(e),
+ Field(RecordLit(kvs), l) => match kvs.get(&l) {
+ Some(r) => DoneRefSub(r),
+ None => DoneAsIs,
+ },
+ Projection(_, ls) if ls.is_empty() => {
+ Done(RecordLit(std::collections::BTreeMap::new()))
+ }
+ Projection(RecordLit(kvs), ls) => Done(RecordLit(
+ ls.iter()
+ .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone())))
+ .collect(),
+ )),
+ _ => DoneAsIs,
+ };
+
+ match what_next {
+ Continue(e) => normalize_ref(&e),
+ ContinueSub(e) => normalize_ref(e.as_ref()),
+ Done(e) => e,
+ DoneRef(e) => e.clone(),
+ DoneRefSub(e) => e.unroll(),
+ DoneAsIs => expr.map_ref_simple(ExprF::roll),
}
}
@@ -341,8 +315,8 @@ where
///
pub fn normalize<S, A>(e: SubExpr<S, A>) -> SubExpr<S, A>
where
- S: fmt::Debug,
- A: fmt::Debug,
+ S: fmt::Debug + Clone,
+ A: fmt::Debug + Clone,
{
- map_subexpr_rc(&normalize_whnf(&e), |x| normalize(Rc::clone(x)))
+ normalize_ref(e.as_ref()).roll()
}
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index f21721d..75e6e1d 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -1,7 +1,6 @@
#![allow(non_snake_case)]
use std::collections::HashSet;
use std::fmt;
-use std::rc::Rc;
use crate::normalize::normalize;
use dhall_core;
@@ -13,7 +12,7 @@ use self::TypeMessage::*;
fn axiom<S>(c: Const) -> Result<Const, TypeError<S>> {
use dhall_core::Const::*;
- use dhall_core::Expr::*;
+ use dhall_core::ExprF::*;
match c {
Type => Ok(Kind),
Kind => Err(TypeError::new(&Context::new(), rc(Const(Kind)), Untyped)),
@@ -29,7 +28,7 @@ fn rule(a: Const, b: Const) -> Result<Const, ()> {
}
}
-fn match_vars(vl: &V, vr: &V, ctx: &[(Label, Label)]) -> bool {
+fn match_vars(vl: &V<Label>, vr: &V<Label>, ctx: &[(Label, Label)]) -> bool {
let mut vl = vl.clone();
let mut vr = vr.clone();
let mut ctx = ctx.to_vec();
@@ -54,7 +53,7 @@ where
S: ::std::fmt::Debug,
T: ::std::fmt::Debug,
{
- use dhall_core::Expr::*;
+ use dhall_core::ExprF::*;
fn go<S, T>(
ctx: &mut Vec<(Label, Label)>,
el: &Expr<S, X>,
@@ -113,7 +112,7 @@ where
go::<S, T>(&mut ctx, eL0, eR0)
}
-fn type_of_builtin<S>(b: Builtin) -> Rc<Expr<S, X>> {
+fn type_of_builtin<S>(b: Builtin) -> SubExpr<S, X> {
use dhall_core::Builtin::*;
match b {
Bool | Natural | Integer | Double | Text => dhall_expr!(Type),
@@ -184,17 +183,16 @@ fn type_of_builtin<S>(b: Builtin) -> Rc<Expr<S, X>> {
/// 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, Rc<Expr<S, X>>>,
- e: Rc<Expr<S, X>>,
-) -> Result<Rc<Expr<S, X>>, TypeError<S>>
+ ctx: &Context<Label, SubExpr<S, X>>,
+ e: SubExpr<S, X>,
+) -> Result<SubExpr<S, X>, TypeError<S>>
where
- S: ::std::fmt::Debug,
+ S: ::std::fmt::Debug + Clone,
{
use dhall_core::BinOp::*;
use dhall_core::Builtin::*;
use dhall_core::Const::*;
- use dhall_core::Expr;
- use dhall_core::Expr::*;
+ use dhall_core::ExprF::*;
let mkerr = |msg: TypeMessage<_>| TypeError::new(ctx, e.clone(), msg);
let ensure_const = |x: &SubExpr<_, _>, msg: TypeMessage<_>| match x.as_ref()
{
@@ -266,7 +264,7 @@ where
return Err(mkerr(NotAFunction(f.clone(), tf)));
}
};
- let tA = normalize(Rc::clone(tA));
+ let tA = normalize(SubExpr::clone(tA));
let tA2 = normalized_type_with(ctx, a.clone())?;
if prop_equal(tA.as_ref(), tA2.as_ref()) {
let vx0 = &V(x.clone(), 0);
@@ -280,9 +278,9 @@ where
}
Let(f, mt, r, b) => {
let r = if let Some(t) = mt {
- rc(Annot(Rc::clone(r), Rc::clone(t)))
+ rc(Annot(SubExpr::clone(r), SubExpr::clone(t)))
} else {
- Rc::clone(r)
+ SubExpr::clone(r)
};
let tR = type_with(ctx, r)?;
@@ -351,7 +349,7 @@ where
EmptyListLit(t) => {
let s = normalized_type_with(ctx, t.clone())?;
ensure_is_type(s, InvalidListType(t.clone()))?;
- let t = normalize(Rc::clone(t));
+ let t = normalize(SubExpr::clone(t));
return Ok(dhall_expr!(List t));
}
NEListLit(xs) => {
@@ -377,7 +375,7 @@ where
return Ok(dhall_expr!(Optional t));
}
NEOptionalLit(x) => {
- let t: Rc<Expr<_, _>> = type_with(ctx, x.clone())?;
+ let t: SubExpr<_, _> = type_with(ctx, x.clone())?;
let s = normalized_type_with(ctx, t.clone())?;
ensure_is_type(s, InvalidOptionalType(t.clone()))?;
let t = normalize(t);
@@ -451,11 +449,11 @@ where
}
pub fn normalized_type_with<S>(
- ctx: &Context<Label, Rc<Expr<S, X>>>,
- e: Rc<Expr<S, X>>,
-) -> Result<Rc<Expr<S, X>>, TypeError<S>>
+ ctx: &Context<Label, SubExpr<S, X>>,
+ e: SubExpr<S, X>,
+) -> Result<SubExpr<S, X>, TypeError<S>>
where
- S: ::std::fmt::Debug,
+ S: ::std::fmt::Debug + Clone,
{
Ok(normalize(type_with(ctx, e)?))
}
@@ -463,9 +461,9 @@ where
/// `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: ::std::fmt::Debug>(
- e: Rc<Expr<S, X>>,
-) -> Result<Rc<Expr<S, X>>, TypeError<S>> {
+pub fn type_of<S: ::std::fmt::Debug + Clone>(
+ e: SubExpr<S, X>,
+) -> Result<SubExpr<S, X>, TypeError<S>> {
let ctx = Context::new();
type_with(&ctx, e) //.map(|e| e.into_owned())
}
@@ -474,63 +472,58 @@ pub fn type_of<S: ::std::fmt::Debug>(
#[derive(Debug)]
pub enum TypeMessage<S> {
UnboundVariable,
- 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>>),
+ InvalidInputType(SubExpr<S, X>),
+ InvalidOutputType(SubExpr<S, X>),
+ NotAFunction(SubExpr<S, X>, SubExpr<S, X>),
+ TypeMismatch(SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
+ AnnotMismatch(SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
Untyped,
- InvalidListElement(usize, Rc<Expr<S, X>>, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
- InvalidListType(Rc<Expr<S, X>>),
- InvalidOptionalElement(Rc<Expr<S, X>>, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+ InvalidListElement(usize, SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
+ InvalidListType(SubExpr<S, X>),
+ InvalidOptionalElement(SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
InvalidOptionalLiteral(usize),
- InvalidOptionalType(Rc<Expr<S, X>>),
- InvalidPredicate(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+ InvalidOptionalType(SubExpr<S, X>),
+ InvalidPredicate(SubExpr<S, X>, SubExpr<S, X>),
IfBranchMismatch(
- Rc<Expr<S, X>>,
- Rc<Expr<S, X>>,
- Rc<Expr<S, X>>,
- Rc<Expr<S, X>>,
+ SubExpr<S, X>,
+ SubExpr<S, X>,
+ SubExpr<S, X>,
+ SubExpr<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>>),
+ IfBranchMustBeTerm(bool, SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
+ InvalidField(Label, SubExpr<S, X>),
+ InvalidFieldType(Label, SubExpr<S, X>),
+ InvalidAlternative(Label, SubExpr<S, X>),
+ InvalidAlternativeType(Label, SubExpr<S, X>),
DuplicateAlternative(Label),
- MustCombineARecord(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+ MustCombineARecord(SubExpr<S, X>, SubExpr<S, X>),
FieldCollision(Label),
- MustMergeARecord(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
- MustMergeUnion(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+ MustMergeARecord(SubExpr<S, X>, SubExpr<S, X>),
+ MustMergeUnion(SubExpr<S, X>, SubExpr<S, X>),
UnusedHandler(HashSet<Label>),
MissingHandler(HashSet<Label>),
- 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>>),
- BinOpTypeMismatch(BinOp, 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>>),
+ HandlerInputTypeMismatch(Label, SubExpr<S, X>, SubExpr<S, X>),
+ HandlerOutputTypeMismatch(Label, SubExpr<S, X>, SubExpr<S, X>),
+ HandlerNotAFunction(Label, SubExpr<S, X>),
+ NotARecord(Label, SubExpr<S, X>, SubExpr<S, X>),
+ MissingField(Label, SubExpr<S, X>),
+ BinOpTypeMismatch(BinOp, SubExpr<S, X>, SubExpr<S, X>),
+ NoDependentLet(SubExpr<S, X>, SubExpr<S, X>),
+ NoDependentTypes(SubExpr<S, X>, SubExpr<S, X>),
}
/// A structured type error that includes context
#[derive(Debug)]
pub struct TypeError<S> {
- pub context: Context<Label, Rc<Expr<S, X>>>,
- pub current: Rc<Expr<S, X>>,
+ pub context: Context<Label, SubExpr<S, X>>,
+ pub current: SubExpr<S, X>,
pub type_message: TypeMessage<S>,
}
impl<S> TypeError<S> {
pub fn new(
- context: &Context<Label, Rc<Expr<S, X>>>,
- current: Rc<Expr<S, X>>,
+ context: &Context<Label, SubExpr<S, X>>,
+ current: SubExpr<S, X>,
type_message: TypeMessage<S>,
) -> Self {
TypeError {
diff --git a/dhall/tests/common/mod.rs b/dhall/tests/common/mod.rs
index 6b893e0..325b80f 100644
--- a/dhall/tests/common/mod.rs
+++ b/dhall/tests/common/mod.rs
@@ -111,7 +111,7 @@ pub fn run_test(base_path: &str, feature: Feature) {
let expected_file_path = base_path + "B.dhall";
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();
+ typecheck::type_of(rc(ExprF::Annot(expr, expected))).unwrap();
}
}
}
diff --git a/dhall/tests/dhall_type.rs b/dhall/tests/dhall_type.rs
index faece20..941e3a4 100644
--- a/dhall/tests/dhall_type.rs
+++ b/dhall/tests/dhall_type.rs
@@ -33,10 +33,7 @@ fn test_dhall_type() {
#[derive(Type)]
#[allow(dead_code)]
struct C<T>(T, Option<String>);
- assert_eq!(
- <C<bool>>::get_type(),
- <(bool, Option<String>)>::get_type()
- );
+ assert_eq!(<C<bool>>::get_type(), <(bool, Option<String>)>::get_type());
#[derive(Type)]
#[allow(dead_code)]
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 16:22:09 +0000