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