summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/typecheck.rs50
-rw-r--r--dhall_core/src/core.rs53
2 files changed, 65 insertions, 38 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index fa938ef..6e7775c 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -10,7 +10,7 @@ use dhall_core::core::Builtin::*;
use dhall_core::core::Const::*;
use dhall_core::core::Expr::*;
use dhall_core::core::{app, pi};
-use dhall_core::core::{bx, shift, subst, Expr, V, X, StringLike};
+use dhall_core::core::{bx, shift, subst, Expr, StringLike, V, X};
use self::TypeMessage::*;
@@ -48,7 +48,10 @@ fn match_vars<L: Clone + Eq>(vl: &V<L>, vr: &V<L>, ctx: &[(L, L)]) -> bool {
}
}
-fn prop_equal<L: StringLike, S, T>(eL0: &Expr<L, S, X>, eR0: &Expr<L, T, X>) -> bool
+fn prop_equal<L: StringLike, S, T>(
+ eL0: &Expr<L, S, X>,
+ eR0: &Expr<L, T, X>,
+) -> bool
where
S: Clone + ::std::fmt::Debug,
T: Clone + ::std::fmt::Debug,
@@ -387,7 +390,8 @@ where
pi("zero", "natural", "natural"),
),
),
- ).take_ownership_of_labels()),
+ )
+ .take_ownership_of_labels()),
Builtin(NaturalBuild) => Ok(pi(
"_",
pi(
@@ -400,9 +404,14 @@ where
),
),
Natural,
- ).take_ownership_of_labels()),
+ )
+ .take_ownership_of_labels()),
Builtin(NaturalIsZero) | Builtin(NaturalEven) | Builtin(NaturalOdd) => {
- Ok(Pi("_".to_owned().into(), bx(Natural.into()), bx(Bool.into())))
+ Ok(Pi(
+ "_".to_owned().into(),
+ bx(Natural.into()),
+ bx(Bool.into()),
+ ))
}
BinOp(NaturalPlus, ref l, ref r) => {
op2_type(ctx, e, Natural, CantAdd, l, r)
@@ -461,7 +470,8 @@ where
),
app(List, "a"),
),
- ).take_ownership_of_labels()),
+ )
+ .take_ownership_of_labels()),
Builtin(ListFold) => Ok(pi(
"a",
Const(Type),
@@ -478,15 +488,18 @@ where
),
),
),
- ).take_ownership_of_labels()),
+ )
+ .take_ownership_of_labels()),
Builtin(ListLength) => {
- Ok(pi("a", Const(Type), pi("_", app(List, "a"), Natural)).take_ownership_of_labels())
+ Ok(pi("a", Const(Type), pi("_", app(List, "a"), Natural))
+ .take_ownership_of_labels())
}
Builtin(ListHead) | Builtin(ListLast) => Ok(pi(
"a",
Const(Type),
pi("_", app(List, "a"), app(Optional, "a")),
- ).take_ownership_of_labels()),
+ )
+ .take_ownership_of_labels()),
Builtin(ListIndexed) => {
let mut m: BTreeMap<Label, Expr<Label, _, _>> = BTreeMap::new();
m.insert("index".into(), Builtin(Natural));
@@ -497,11 +510,12 @@ where
pi("_", app(List, Var(V("a".into(), 0))), app(List, Record(m))),
))
}
- Builtin(ListReverse) => Ok(pi(
- "a",
- Const(Type),
- pi("_", app(List, "a"), app(List, "a")),
- ).take_ownership_of_labels()),
+ Builtin(ListReverse) => {
+ Ok(
+ pi("a", Const(Type), pi("_", app(List, "a"), app(List, "a")))
+ .take_ownership_of_labels(),
+ )
+ }
OptionalLit(ref t, ref xs) => {
let mut iter = xs.iter();
let t: Box<Expr<_, _, _>> = match t {
@@ -553,7 +567,8 @@ where
),
),
),
- ).take_ownership_of_labels()),
+ )
+ .take_ownership_of_labels()),
Builtin(List) | Builtin(Optional) => {
Ok(pi("_", Const(Type), Const(Type)).take_ownership_of_labels())
}
@@ -708,7 +723,10 @@ 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<Label: StringLike + From<String>, S: Clone + ::std::fmt::Debug>(
+pub fn type_of<
+ Label: StringLike + From<String>,
+ S: Clone + ::std::fmt::Debug,
+>(
e: &Expr<Label, S, X>,
) -> Result<Expr<Label, S, X>, TypeError<Label, S>> {
let ctx = Context::new();
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index 3b98b39..eed9e0c 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -157,10 +157,7 @@ pub enum Expr<Label, Note, Embed> {
Box<Expr<Label, Note, Embed>>,
),
/// `App f A ~ f A`
- App(
- Box<Expr<Label, Note, Embed>>,
- Box<Expr<Label, Note, Embed>>,
- ),
+ App(Box<Expr<Label, Note, Embed>>, Box<Expr<Label, 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(
@@ -170,10 +167,7 @@ pub enum Expr<Label, Note, Embed> {
Box<Expr<Label, Note, Embed>>,
),
/// `Annot x t ~ x : t`
- Annot(
- Box<Expr<Label, Note, Embed>>,
- Box<Expr<Label, Note, Embed>>,
- ),
+ Annot(Box<Expr<Label, Note, Embed>>, Box<Expr<Label, Note, Embed>>),
/// Built-in values
Builtin(Builtin),
// Binary operations
@@ -369,19 +363,32 @@ impl<Label: StringLike, S, A> Expr<Label, S, A> {
}
impl<'i, S: Clone, A: Clone> Expr<&'i str, S, A> {
- pub fn take_ownership_of_labels<L: StringLike + From<String>>(&self) -> Expr<L, S, A> {
- let recurse =
- |e: &Expr<&'i str, S, A>| -> Expr<L, S, A> { e.take_ownership_of_labels() };
- map_shallow(self, recurse, |x| x.clone(), |x| x.clone(), |x: &&str| -> L { (*x).to_owned().into() })
+ pub fn take_ownership_of_labels<L: StringLike + From<String>>(
+ &self,
+ ) -> Expr<L, S, A> {
+ let recurse = |e: &Expr<&'i str, S, A>| -> Expr<L, S, A> {
+ e.take_ownership_of_labels()
+ };
+ map_shallow(
+ self,
+ recurse,
+ |x| x.clone(),
+ |x| x.clone(),
+ |x: &&str| -> L { (*x).to_owned().into() },
+ )
}
}
impl<L: StringLike, S: Clone, A: Clone> Expr<L, S, Expr<L, S, A>> {
- pub fn squash_embed(&self) -> Expr<L, S, A>
- {
+ pub fn squash_embed(&self) -> Expr<L, S, A> {
match self {
Expr::Embed(e) => e.clone(),
- e => e.map_shallow(|e| e.squash_embed(), |x| x.clone(), |_| unreachable!(), |x| x.clone())
+ e => e.map_shallow(
+ |e| e.squash_embed(),
+ |x| x.clone(),
+ |_| unreachable!(),
+ |x| x.clone(),
+ ),
}
}
}
@@ -779,7 +786,8 @@ where
A: Clone,
S: Clone,
T: Clone,
- Label1: Display + fmt::Debug + Clone + Hash + Ord + Eq + Into<String> + Default,
+ Label1:
+ Display + fmt::Debug + Clone + Hash + Ord + Eq + Into<String> + Default,
Label2: StringLike,
F1: Fn(&Expr<Label1, S, A>) -> Expr<Label2, T, B>,
F2: FnOnce(&S) -> T,
@@ -1007,9 +1015,7 @@ where
es.iter().map(|e| shift(d, v, e)).collect(),
),
Record(a) => Record(map_record_value(a, |val| shift(d, v, val))),
- RecordLit(a) => {
- RecordLit(map_record_value(a, |val| shift(d, v, val)))
- }
+ RecordLit(a) => RecordLit(map_record_value(a, |val| shift(d, v, val))),
Union(a) => Union(map_record_value(a, |val| shift(d, v, val))),
UnionLit(k, uv, a) => UnionLit(
k.clone(),
@@ -1068,13 +1074,15 @@ where
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 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))
}
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 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))
}
@@ -1092,7 +1100,8 @@ where
}
Let(f, mt, r, b) => {
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 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 r2 = subst(v, e, r);
Let(f.clone(), mt2, bx(r2), bx(b2))
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 20:06:15 +0000