summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/binary.rs145
-rw-r--r--dhall/src/normalize.rs38
-rw-r--r--dhall/src/typecheck.rs26
3 files changed, 107 insertions, 102 deletions
diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs
index cc07431..fbd343b 100644
--- a/dhall/src/binary.rs
+++ b/dhall/src/binary.rs
@@ -2,7 +2,7 @@ use dhall_core::*;
use itertools::*;
use serde_cbor::value::value as cbor;
-type ParsedExpr = Expr<X, Import>;
+type ParsedExpr = Box<Expr<X, Import>>;
#[derive(Debug)]
pub enum DecodeError {
@@ -21,24 +21,24 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
use cbor::Value::*;
use dhall_core::{BinOp, Builtin, Const};
use Expr::*;
- match data {
+ let e = match data {
String(s) => match Builtin::parse(s) {
- Some(b) => Ok(Expr::Builtin(b)),
+ Some(b) => Expr::Builtin(b),
None => match s.as_str() {
- "True" => Ok(BoolLit(true)),
- "False" => Ok(BoolLit(false)),
- "Type" => Ok(Const(Const::Type)),
- "Kind" => Ok(Const(Const::Kind)),
- s => Ok(Var(V(Label::from(s), 0))),
+ "True" => BoolLit(true),
+ "False" => BoolLit(false),
+ "Type" => Const(Const::Type),
+ "Kind" => Const(Const::Kind),
+ s => Var(V(Label::from(s), 0)),
},
},
- U64(n) => Ok(Var(V(Label::from("_"), *n as usize))),
- F64(x) => Ok(DoubleLit(*x)),
- Bool(b) => Ok(BoolLit(*b)),
+ U64(n) => Var(V(Label::from("_"), *n as usize)),
+ F64(x) => DoubleLit(*x),
+ Bool(b) => BoolLit(*b),
Array(vec) => match vec.as_slice() {
[String(l), U64(n)] => {
let l = Label::from(l.as_str());
- Ok(Var(V(l, *n as usize)))
+ Var(V(l, *n as usize))
}
[U64(0), f, args..] => {
let f = cbor_value_to_dhall(&f)?;
@@ -46,33 +46,33 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
.iter()
.map(cbor_value_to_dhall)
.collect::<Result<Vec<_>, _>>()?;
- Ok(App(bx(f), args))
+ App(f, args)
}
[U64(1), x, y] => {
- let x = bx(cbor_value_to_dhall(&x)?);
- let y = bx(cbor_value_to_dhall(&y)?);
- Ok(Lam(Label::from("_"), x, y))
+ let x = cbor_value_to_dhall(&x)?;
+ let y = cbor_value_to_dhall(&y)?;
+ Lam(Label::from("_"), x, y)
}
[U64(1), String(l), x, y] => {
- let x = bx(cbor_value_to_dhall(&x)?);
- let y = bx(cbor_value_to_dhall(&y)?);
+ let x = cbor_value_to_dhall(&x)?;
+ let y = cbor_value_to_dhall(&y)?;
let l = Label::from(l.as_str());
- Ok(Lam(l, x, y))
+ Lam(l, x, y)
}
[U64(2), x, y] => {
- let x = bx(cbor_value_to_dhall(&x)?);
- let y = bx(cbor_value_to_dhall(&y)?);
- Ok(Pi(Label::from("_"), x, y))
+ let x = cbor_value_to_dhall(&x)?;
+ let y = cbor_value_to_dhall(&y)?;
+ Pi(Label::from("_"), x, y)
}
[U64(2), String(l), x, y] => {
- let x = bx(cbor_value_to_dhall(&x)?);
- let y = bx(cbor_value_to_dhall(&y)?);
+ let x = cbor_value_to_dhall(&x)?;
+ let y = cbor_value_to_dhall(&y)?;
let l = Label::from(l.as_str());
- Ok(Pi(l, x, y))
+ Pi(l, x, y)
}
[U64(3), U64(n), x, y] => {
- let x = bx(cbor_value_to_dhall(&x)?);
- let y = bx(cbor_value_to_dhall(&y)?);
+ let x = cbor_value_to_dhall(&x)?;
+ let y = cbor_value_to_dhall(&y)?;
use BinOp::*;
let op = match n {
0 => BoolOr,
@@ -89,77 +89,77 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
11 => ImportAlt,
_ => Err(DecodeError::WrongFormatError)?,
};
- Ok(BinOp(op, x, y))
+ BinOp(op, x, y)
}
[U64(4), t] => {
- let t = bx(cbor_value_to_dhall(&t)?);
- Ok(ListLit(Some(t), vec![]))
+ let t = cbor_value_to_dhall(&t)?;
+ ListLit(Some(t), vec![])
}
[U64(4), Null, rest..] => {
let rest = rest
.iter()
.map(cbor_value_to_dhall)
.collect::<Result<Vec<_>, _>>()?;
- Ok(ListLit(None, rest))
+ ListLit(None, rest)
}
[U64(5), t] => {
- let t = bx(cbor_value_to_dhall(&t)?);
- Ok(OptionalLit(Some(t), None))
+ let t = cbor_value_to_dhall(&t)?;
+ OptionalLit(Some(t), None)
}
[U64(5), Null, x] => {
- let x = bx(cbor_value_to_dhall(&x)?);
- Ok(OptionalLit(None, Some(x)))
+ let x = cbor_value_to_dhall(&x)?;
+ OptionalLit(None, Some(x))
}
[U64(5), t, x] => {
- let x = bx(cbor_value_to_dhall(&x)?);
- let t = bx(cbor_value_to_dhall(&t)?);
- Ok(OptionalLit(Some(t), Some(x)))
+ let x = cbor_value_to_dhall(&x)?;
+ let t = cbor_value_to_dhall(&t)?;
+ OptionalLit(Some(t), Some(x))
}
[U64(6), x, y] => {
- let x = bx(cbor_value_to_dhall(&x)?);
- let y = bx(cbor_value_to_dhall(&y)?);
- Ok(Merge(x, y, None))
+ let x = cbor_value_to_dhall(&x)?;
+ let y = cbor_value_to_dhall(&y)?;
+ Merge(x, y, None)
}
[U64(6), x, y, z] => {
- let x = bx(cbor_value_to_dhall(&x)?);
- let y = bx(cbor_value_to_dhall(&y)?);
- let z = bx(cbor_value_to_dhall(&z)?);
- Ok(Merge(x, y, Some(z)))
+ let x = cbor_value_to_dhall(&x)?;
+ let y = cbor_value_to_dhall(&y)?;
+ let z = cbor_value_to_dhall(&z)?;
+ Merge(x, y, Some(z))
}
[U64(7), Object(map)] => {
let map = cbor_map_to_dhall_map(map)?;
- Ok(Record(map))
+ Record(map)
}
[U64(8), Object(map)] => {
let map = cbor_map_to_dhall_map(map)?;
- Ok(RecordLit(map))
+ RecordLit(map)
}
[U64(9), x, String(l)] => {
- let x = bx(cbor_value_to_dhall(&x)?);
+ let x = cbor_value_to_dhall(&x)?;
let l = Label::from(l.as_str());
- Ok(Field(x, l))
+ Field(x, l)
}
[U64(11), Object(map)] => {
let map = cbor_map_to_dhall_map(map)?;
- Ok(Union(map))
+ Union(map)
}
[U64(12), String(l), x, Object(map)] => {
let map = cbor_map_to_dhall_map(map)?;
- let x = bx(cbor_value_to_dhall(&x)?);
+ let x = cbor_value_to_dhall(&x)?;
let l = Label::from(l.as_str());
- Ok(UnionLit(l, x, map))
+ UnionLit(l, x, map)
}
[U64(14), x, y, z] => {
- let x = bx(cbor_value_to_dhall(&x)?);
- let y = bx(cbor_value_to_dhall(&y)?);
- let z = bx(cbor_value_to_dhall(&z)?);
- Ok(BoolIf(x, y, z))
- }
- [U64(15), U64(x)] => Ok(NaturalLit(*x as Natural)),
- [U64(16), U64(x)] => Ok(IntegerLit(*x as Integer)),
- [U64(16), I64(x)] => Ok(IntegerLit(*x as Integer)),
+ let x = cbor_value_to_dhall(&x)?;
+ let y = cbor_value_to_dhall(&y)?;
+ let z = cbor_value_to_dhall(&z)?;
+ BoolIf(x, y, z)
+ }
+ [U64(15), U64(x)] => NaturalLit(*x as Natural),
+ [U64(16), U64(x)] => IntegerLit(*x as Integer),
+ [U64(16), I64(x)] => IntegerLit(*x as Integer),
[U64(18), String(first), rest..] => {
- Ok(TextLit(InterpolatedText::from((
+ TextLit(InterpolatedText::from((
first.clone(),
rest.iter()
.tuples()
@@ -172,7 +172,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
Ok((x, y))
})
.collect::<Result<_, _>>()?,
- ))))
+ )))
}
[U64(25), bindings..] => {
let mut tuples = bindings.iter().tuples();
@@ -184,9 +184,9 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
};
let t = match t {
Null => None,
- t => Some(bx(cbor_value_to_dhall(&t)?)),
+ t => Some(cbor_value_to_dhall(&t)?),
};
- let v = bx(cbor_value_to_dhall(&v)?);
+ let v = cbor_value_to_dhall(&v)?;
Ok((x, t, v))
})
.collect::<Result<Vec<_>, _>>()?;
@@ -195,19 +195,20 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
.next()
.ok_or(DecodeError::WrongFormatError)?;
let expr = cbor_value_to_dhall(expr)?;
- Ok(bindings
+ return Ok(bindings
.into_iter()
- .fold(expr, |acc, (x, t, v)| Let(x, t, v, bx(acc))))
+ .fold(expr, |acc, (x, t, v)| bx(Let(x, t, v, acc))));
}
[U64(26), x, y] => {
- let x = bx(cbor_value_to_dhall(&x)?);
- let y = bx(cbor_value_to_dhall(&y)?);
- Ok(Annot(x, y))
+ let x = cbor_value_to_dhall(&x)?;
+ let y = cbor_value_to_dhall(&y)?;
+ Annot(x, y)
}
- _ => Err(DecodeError::WrongFormatError),
+ _ => Err(DecodeError::WrongFormatError)?,
},
- _ => Err(DecodeError::WrongFormatError),
- }
+ _ => Err(DecodeError::WrongFormatError)?,
+ };
+ Ok(bx(e))
}
fn cbor_map_to_dhall_map(
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 9105ec4..c49d313 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -44,8 +44,8 @@ where
(Builtin(b), args) => match (
b,
args.iter()
- .map(normalize_whnf)
- .collect::<Vec<_>>()
+ .map(|x| normalize_whnf(&*x))
+ .collect::<Vec<Expr<_, _>>>()
.as_slice(),
) {
(OptionalSome, [a]) => OptionalLit(None, Some(bx(a.clone()))),
@@ -57,10 +57,10 @@ where
(NaturalShow, [NaturalLit(n)]) => TextLit(n.to_string().into()),
(ListLength, [_, ListLit(_, ys)]) => NaturalLit(ys.len()),
(ListHead, [_, ListLit(t, ys)]) => {
- OptionalLit(t.clone(), ys.iter().cloned().map(bx).next())
+ OptionalLit(t.clone(), ys.iter().cloned().next())
}
(ListLast, [_, ListLit(t, ys)]) => {
- OptionalLit(t.clone(), ys.iter().cloned().map(bx).last())
+ OptionalLit(t.clone(), ys.iter().cloned().last())
}
(ListReverse, [_, ListLit(t, ys)]) => {
let xs = ys.iter().rev().cloned().collect();
@@ -72,11 +72,11 @@ where
App(f, args) => match (&**f, args.as_slice()) {
(Builtin(ListFold), [_, x, rest..]) => {
return normalize_whnf(&App(
- bx(x.clone()),
+ x.clone(),
rest.to_vec(),
))
}
- (f, args) => app(f.clone(), args.to_vec()),
+ (_, args) => App(f.clone(), args.to_vec()),
},
g => g.clone(),
};
@@ -93,11 +93,11 @@ where
App(f, args) => match (&**f, args.as_slice()) {
(Builtin(OptionalFold), [_, x, rest..]) => {
return normalize_whnf(&App(
- bx(x.clone()),
+ x.clone(),
rest.to_vec(),
))
}
- (f, args) => app(f.clone(), args.to_vec()),
+ (_, args) => App(f.clone(), args.to_vec()),
},
g => g.clone(),
};
@@ -109,8 +109,8 @@ where
}
(ListFold, [_, ListLit(_, xs), _, cons, nil]) => {
let e2: Expr<_, _> =
- xs.into_iter().rev().fold((*nil).clone(), |acc, x| {
- let x = bx((x).clone());
+ 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)
@@ -122,7 +122,7 @@ where
// normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
// }
(OptionalFold, [_, OptionalLit(_, Some(x)), _, just, _]) => {
- let x = bx((**x).clone());
+ let x = x.clone();
let just = bx(just.clone());
normalize_whnf(&dhall_expr!(just x))
}
@@ -137,11 +137,11 @@ where
match (&**f, args.as_slice()) {
// fold/build fusion
(Builtin(NaturalFold), [x, rest..]) => {
- normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
+ normalize_whnf(&App(x.clone(), rest.to_vec()))
}
- (f, args) => app(
+ (_, args) => app(
Builtin(NaturalBuild),
- vec![app(f.clone(), args.to_vec())],
+ vec![bx(App(f.clone(), args.to_vec()))],
),
}
}
@@ -149,15 +149,17 @@ where
match (&**f, args.as_slice()) {
// fold/build fusion
(Builtin(NaturalBuild), [x, rest..]) => {
- normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
+ normalize_whnf(&App(x.clone(), rest.to_vec()))
}
- (f, args) => app(
+ (_, args) => app(
Builtin(NaturalFold),
- vec![app(f.clone(), args.to_vec())],
+ vec![bx(App(f.clone(), args.to_vec()))],
),
}
}
- (b, args) => App(bx(Builtin(b)), args.to_vec()),
+ (b, args) => {
+ App(bx(Builtin(b)), args.iter().cloned().map(bx).collect())
+ }
},
(f, args) => App(bx(f), args.to_vec()),
},
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 0f87d67..ca0d5af 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -270,7 +270,7 @@ where
Err(TypeError::new(
ctx,
e,
- TypeMismatch((**f).clone(), nf_A, (*a).clone(), nf_A2),
+ TypeMismatch((**f).clone(), nf_A, (**a).clone(), nf_A2),
))
}
}
@@ -436,7 +436,7 @@ where
return Err(TypeError::new(
ctx,
e,
- InvalidListElement(i, nf_t, x.clone(), nf_t2),
+ InvalidListElement(i, nf_t, (**x).clone(), nf_t2),
));
}
}
@@ -529,7 +529,7 @@ where
return Err(TypeError::new(
ctx,
e,
- InvalidFieldType((*k).clone(), (*t).clone()),
+ InvalidFieldType((*k).clone(), (**t).clone()),
));
}
}
@@ -548,11 +548,11 @@ where
return Err(TypeError::new(
ctx,
e,
- InvalidField((*k).clone(), (*v).clone()),
+ InvalidField((*k).clone(), (**v).clone()),
));
}
}
- Ok(((*k).clone(), t))
+ Ok(((*k).clone(), bx(t)))
})
.collect::<Result<_, _>>()?;
Ok(Record(kts))
@@ -641,13 +641,15 @@ where
Field(ref r, ref x) => {
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).clone(), t.clone()),
- )
- }),
+ Record(ref kts) => {
+ kts.get(x).map(|x| &**x).cloned().ok_or_else(|| {
+ TypeError::new(
+ ctx,
+ e,
+ MissingField((*x).clone(), t.clone()),
+ )
+ })
+ }
_ => Err(TypeError::new(
ctx,
e,
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 18:17:17 +0000