diff options
Diffstat (limited to '')
| -rw-r--r-- | dhall/src/lib.rs | 2 | ||||
| -rw-r--r-- | dhall/src/main.rs | 2 | ||||
| -rw-r--r-- | dhall/src/normalize.rs | 53 | ||||
| -rw-r--r-- | dhall/src/typecheck.rs | 126 | ||||
| -rw-r--r-- | dhall/tests/macros.rs | 6 | ||||
| -rw-r--r-- | dhall_core/src/context.rs | 4 | ||||
| -rw-r--r-- | dhall_core/src/core.rs | 269 | ||||
| -rw-r--r-- | dhall_generator/src/lib.rs | 14 |
8 files changed, 298 insertions, 178 deletions
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 4e183b4..6372768 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -43,7 +43,7 @@ impl fmt::Display for DhallError { pub fn load_dhall_file<'i, 'a: 'i>( f: &Path, source_pool: &'a mut Vec<String>, - resolve_imports: bool, + _resolve_imports: bool, ) -> Result<Expr<'i, X, X>, DhallError> { source_pool.push(String::new()); let mut buffer = source_pool.last_mut().unwrap(); diff --git a/dhall/src/main.rs b/dhall/src/main.rs index 493f9be..dbe80a3 100644 --- a/dhall/src/main.rs +++ b/dhall/src/main.rs @@ -89,5 +89,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 246a3c0..d3766d5 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -12,7 +12,9 @@ use std::fmt; /// However, `normalize` will not fail if the expression is ill-typed and will /// leave ill-typed sub-expressions unevaluated. /// -pub fn normalize<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A> +pub fn normalize<Label: StringLike, S, T, A>( + e: &Expr_<Label, S, A>, +) -> Expr_<Label, T, A> where S: Clone + fmt::Debug, T: Clone + fmt::Debug, @@ -24,9 +26,9 @@ where match e { // Matches that don't normalize everything right away Let(f, _, r, 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); + let r2 = shift::<Label, _, S, _>(1, V(f.clone(), 0), r); + let b2 = subst::<Label, _, S, _>(V(f.clone(), 0), &r2, b); + let b3 = shift::<Label, _, T, _>(-1, V(f.clone(), 0), &b2); normalize(&b3) } BoolIf(b, t, f) => match normalize(b) { @@ -36,16 +38,16 @@ where }, Annot(x, _) => normalize(x), Note(_, e) => normalize(e), - App(f, a) => match normalize::<S, T, A>(f) { + App(f, a) => match normalize::<Label, 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 b2 = subst::<S, T, A>(vx0, &a2, &b); - let b3 = shift::<S, T, A>(-1, vx0, &b2); + let a2 = shift::<Label, S, S, A>(1, vx0, a); + let b2 = subst::<Label, S, T, A>(vx0, &a2, &b); + let b3 = shift::<Label, S, T, A>(-1, vx0, &b2); normalize(&b3) } - f2 => match (f2, normalize::<S, T, A>(a)) { + f2 => match (f2, normalize::<Label, S, T, A>(a)) { // fold/build fusion for `List` (App(box Builtin(ListBuild), _), App(box App(box Builtin(ListFold), _), box e2)) | (App(box Builtin(ListFold), _), App(box App(box Builtin(ListBuild), _), box e2)) | @@ -87,13 +89,14 @@ where (Builtin(NaturalOdd), NaturalLit(n)) => BoolLit(n % 2 != 0), (Builtin(NaturalToInteger), NaturalLit(n)) => IntegerLit(n as isize), (Builtin(NaturalShow), NaturalLit(n)) => TextLit(n.to_string()), - (App(box Builtin(ListBuild), a0), k) => { - let k = bx(k); - let a1 = bx(shift(1, V("a", 0), &a0)); - normalize(&dhall!(k (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0))) - } + // TODO: restore when handling variables generically fixed + // (App(box Builtin(ListBuild), a0), k) => { + // let k = bx(k); + // let a1 = bx(shift(1, V("a", 0), &a0)); + // normalize(&dhall!(k (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0))) + // } (App(box App(box App(box App(box Builtin(ListFold), _), box ListLit(_, xs)), _), cons), nil) => { - let e2: Expr<_, _> = xs.into_iter().rev().fold(nil, |y, ys| { + let e2: Expr_<_, _, _> = xs.into_iter().rev().fold(nil, |y, ys| { let y = bx(y); let ys = bx(ys); dhall!(cons y ys) @@ -130,23 +133,29 @@ where ] */ (App(box App(box App(box App(box Builtin(OptionalFold), _), box OptionalLit(_, xs)), _), just), nothing) => { - let e2: Expr<_, _> = xs.into_iter().fold(nothing, |y, _| { + let e2: Expr_<_, _, _> = xs.into_iter().fold(nothing, |y, _| { let y = bx(y); dhall!(just y) }); normalize(&e2) } - (App(box Builtin(OptionalBuild), a0), g) => { - let g = bx(g); - normalize(&dhall!((g (Optional a0)) (λ(x: a0) -> [x] : Optional a0) ([] : Optional a0))) - } + // TODO: restore when handling variables generically fixed + // (App(box Builtin(OptionalBuild), a0), g) => { + // let g = bx(g); + // normalize(&dhall!((g (Optional a0)) (λ(x: a0) -> [x] : Optional a0) ([] : Optional a0))) + // } (f2, a2) => app(f2, a2), }, }, // Normalize everything else before matching e => { - match e.map_shallow(normalize, |_| unreachable!(), |x| x.clone()) { + match e.map_shallow( + normalize, + |_| unreachable!(), + |x| x.clone(), + |x| x.clone(), + ) { BinOp(BoolAnd, box BoolLit(x), box BoolLit(y)) => { BoolLit(x && y) } @@ -180,7 +189,7 @@ where ListLit(t, xs.chain(ys).collect()) } Merge(_x, _y, _t) => unimplemented!(), - Field(box RecordLit(kvs), x) => match kvs.get(x) { + Field(box RecordLit(kvs), x) => match kvs.get(&x) { Some(r) => r.clone(), None => Field(bx(RecordLit(kvs)), x), }, diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 23ab7a6..c2a2ca3 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}; +use dhall_core::core::{bx, shift, subst, Expr, Expr_, V, X}; use self::TypeMessage::*; @@ -155,7 +155,7 @@ fn op2_type<'i, S, EF>( ) -> Result<Expr<'i, S, X>, TypeError<'i, S>> where S: Clone + ::std::fmt::Debug + 'i, - EF: FnOnce(Expr<'i, S, X>, Expr<'i, S, X>) -> TypeMessage<'i, S>, + EF: FnOnce(Expr<'i, S, X>, Expr<'i, S, X>) -> TypeMessage<&'i str, S>, { let tl = normalize(&type_with(ctx, l)?); match tl { @@ -189,7 +189,7 @@ where use dhall_core::Expr_; match *e { Const(c) => axiom(c).map(Const), //.map(Cow::Owned), - Var(V(x, n)) => { + Var(V(ref x, n)) => { ctx.lookup(x, n) .cloned() //.map(Cow::Borrowed) @@ -206,7 +206,7 @@ where Ok(p) } Pi(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, _ => { @@ -253,9 +253,9 @@ where let tA2 = type_with(ctx, a)?; if prop_equal(&tA, &tA2) { let vx0 = V(x, 0); - let a2 = shift::<S, S, X>(1, vx0, a); + let a2 = shift::<&str, S, S, X>(1, vx0, a); let tB2 = subst(vx0, &a2, &tB); - let tB3 = shift::<S, S, X>(-1, vx0, &tB2); + let tB3 = shift::<&str, S, S, X>(-1, vx0, &tB2); Ok(tB3) } else { let nf_A = normalize(&tA); @@ -269,7 +269,7 @@ where } Let(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 @@ -279,7 +279,7 @@ where 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 @@ -426,7 +426,7 @@ where } }; - let s = normalize::<_, S, _>(&type_with(ctx, &t)?); + let s = normalize::<_, _, S, _>(&type_with(ctx, &t)?); match s { Const(Type) => {} _ => return Err(TypeError::new(ctx, e, InvalidListType(*t))), @@ -512,7 +512,7 @@ where } }; - let s = normalize::<_, S, _>(&type_with(ctx, &t)?); + let s = normalize::<_, _, S, _>(&type_with(ctx, &t)?); match s { Const(Type) => {} _ => { @@ -561,7 +561,7 @@ where | 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)?); + let s = normalize::<_, S, S, X>(&type_with(ctx, t)?); match s { Const(Type) => {} _ => { @@ -580,7 +580,7 @@ where .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) => {} _ => { @@ -717,57 +717,71 @@ pub fn type_of<'i, S: Clone + ::std::fmt::Debug + 'i>( /// The specific type error #[derive(Debug)] -pub enum TypeMessage<'i, S> { +pub enum TypeMessage<Label, S> { UnboundVariable, - InvalidInputType(Expr<'i, S, X>), - InvalidOutputType(Expr<'i, S, X>), - NotAFunction(Expr<'i, S, X>, Expr<'i, S, X>), + InvalidInputType(Expr_<Label, S, X>), + InvalidOutputType(Expr_<Label, S, X>), + NotAFunction(Expr_<Label, S, X>, Expr_<Label, S, X>), TypeMismatch( - Expr<'i, S, X>, - Expr<'i, S, X>, - Expr<'i, S, X>, - Expr<'i, S, X>, + Expr_<Label, S, X>, + Expr_<Label, S, X>, + Expr_<Label, S, X>, + Expr_<Label, S, X>, ), - AnnotMismatch(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>), + AnnotMismatch(Expr_<Label, S, X>, Expr_<Label, S, X>, Expr_<Label, S, X>), Untyped, - InvalidListElement(usize, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>), - InvalidListType(Expr<'i, S, X>), - InvalidOptionalElement(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>), + InvalidListElement( + usize, + Expr_<Label, S, X>, + Expr_<Label, S, X>, + Expr_<Label, S, X>, + ), + InvalidListType(Expr_<Label, S, X>), + InvalidOptionalElement( + Expr_<Label, S, X>, + Expr_<Label, S, X>, + Expr_<Label, S, X>, + ), InvalidOptionalLiteral(usize), - InvalidOptionalType(Expr<'i, S, X>), - InvalidPredicate(Expr<'i, S, X>, Expr<'i, S, X>), + InvalidOptionalType(Expr_<Label, S, X>), + InvalidPredicate(Expr_<Label, S, X>, Expr_<Label, S, X>), IfBranchMismatch( - Expr<'i, S, X>, - Expr<'i, S, X>, - Expr<'i, S, X>, - Expr<'i, S, X>, + Expr_<Label, S, X>, + Expr_<Label, S, X>, + Expr_<Label, S, X>, + Expr_<Label, S, X>, + ), + IfBranchMustBeTerm( + bool, + Expr_<Label, S, X>, + Expr_<Label, S, X>, + Expr_<Label, S, X>, ), - IfBranchMustBeTerm(bool, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>), - InvalidField(String, Expr<'i, S, X>), - InvalidFieldType(String, Expr<'i, S, X>), - InvalidAlternative(String, Expr<'i, S, X>), - InvalidAlternativeType(String, Expr<'i, S, X>), + InvalidField(String, Expr_<Label, S, X>), + InvalidFieldType(String, Expr_<Label, S, X>), + InvalidAlternative(String, Expr_<Label, S, X>), + InvalidAlternativeType(String, Expr_<Label, S, X>), DuplicateAlternative(String), - MustCombineARecord(Expr<'i, S, X>, Expr<'i, S, X>), + MustCombineARecord(Expr_<Label, S, X>, Expr_<Label, S, X>), FieldCollision(String), - MustMergeARecord(Expr<'i, S, X>, Expr<'i, S, X>), - MustMergeUnion(Expr<'i, S, X>, Expr<'i, S, X>), + MustMergeARecord(Expr_<Label, S, X>, Expr_<Label, S, X>), + MustMergeUnion(Expr_<Label, S, X>, Expr_<Label, S, X>), UnusedHandler(HashSet<String>), MissingHandler(HashSet<String>), - HandlerInputTypeMismatch(String, Expr<'i, S, X>, Expr<'i, S, X>), - HandlerOutputTypeMismatch(String, Expr<'i, S, X>, Expr<'i, S, X>), - HandlerNotAFunction(String, Expr<'i, S, X>), - NotARecord(String, Expr<'i, S, X>, Expr<'i, S, X>), - MissingField(String, Expr<'i, S, X>), - CantAnd(Expr<'i, S, X>, Expr<'i, S, X>), - CantOr(Expr<'i, S, X>, Expr<'i, S, X>), - CantEQ(Expr<'i, S, X>, Expr<'i, S, X>), - CantNE(Expr<'i, S, X>, Expr<'i, S, X>), - CantTextAppend(Expr<'i, S, X>, Expr<'i, S, X>), - CantAdd(Expr<'i, S, X>, Expr<'i, S, X>), - CantMultiply(Expr<'i, S, X>, Expr<'i, S, X>), - NoDependentLet(Expr<'i, S, X>, Expr<'i, S, X>), - NoDependentTypes(Expr<'i, S, X>, Expr<'i, S, X>), + HandlerInputTypeMismatch(String, Expr_<Label, S, X>, Expr_<Label, S, X>), + HandlerOutputTypeMismatch(String, Expr_<Label, S, X>, Expr_<Label, S, X>), + HandlerNotAFunction(String, Expr_<Label, S, X>), + NotARecord(String, Expr_<Label, S, X>, Expr_<Label, S, X>), + MissingField(String, Expr_<Label, S, X>), + CantAnd(Expr_<Label, S, X>, Expr_<Label, S, X>), + CantOr(Expr_<Label, S, X>, Expr_<Label, S, X>), + CantEQ(Expr_<Label, S, X>, Expr_<Label, S, X>), + CantNE(Expr_<Label, S, X>, Expr_<Label, S, X>), + CantTextAppend(Expr_<Label, S, X>, Expr_<Label, S, X>), + CantAdd(Expr_<Label, S, X>, Expr_<Label, S, X>), + CantMultiply(Expr_<Label, S, X>, Expr_<Label, S, X>), + NoDependentLet(Expr_<Label, S, X>, Expr_<Label, S, X>), + NoDependentTypes(Expr_<Label, S, X>, Expr_<Label, S, X>), } /// A structured type error that includes context @@ -775,14 +789,14 @@ pub enum TypeMessage<'i, S> { pub struct TypeError<'i, S> { pub context: Context<&'i str, Expr<'i, S, X>>, pub current: Expr<'i, S, X>, - pub type_message: TypeMessage<'i, S>, + pub type_message: TypeMessage<&'i str, S>, } impl<'i, S: Clone> TypeError<'i, S> { pub fn new( context: &Context<&'i str, Expr<'i, S, X>>, current: &Expr<'i, S, X>, - type_message: TypeMessage<'i, S>, + type_message: TypeMessage<&'i str, S>, ) -> Self { TypeError { context: context.clone(), @@ -792,7 +806,7 @@ impl<'i, S: Clone> TypeError<'i, S> { } } -impl<'i, S: fmt::Debug> ::std::error::Error for TypeMessage<'i, S> { +impl<'i, S: fmt::Debug> ::std::error::Error for TypeMessage<&'i str, S> { fn description(&self) -> &str { match *self { UnboundVariable => "Unbound variable", @@ -805,7 +819,7 @@ impl<'i, S: fmt::Debug> ::std::error::Error for TypeMessage<'i, S> { } } -impl<'i, S> fmt::Display for TypeMessage<'i, S> { +impl<'i, S> fmt::Display for TypeMessage<&'i str, S> { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { match *self { UnboundVariable => { diff --git a/dhall/tests/macros.rs b/dhall/tests/macros.rs index ef518ed..b27b850 100644 --- a/dhall/tests/macros.rs +++ b/dhall/tests/macros.rs @@ -61,8 +61,8 @@ macro_rules! make_spec_test { } use dhall::*; -use dhall_core::*; use dhall_core::parser::*; +use dhall_core::*; use std::fs::File; use std::io::Read; use std::path::PathBuf; @@ -114,8 +114,8 @@ pub fn run_test(base_path: &str, feature: Feature, expected: ExpectedResult) { let expected = read_dhall_file(&expected_file_path, &mut expected_buffer).unwrap(); assert_eq_!( - normalize::<_, X, _>(&expr), - normalize::<_, X, _>(&expected) + normalize::<_, _, X, _>(&expr), + normalize::<_, _, X, _>(&expected) ); } _ => unimplemented!(), diff --git a/dhall_core/src/context.rs b/dhall_core/src/context.rs index 412d3f0..877843d 100644 --- a/dhall_core/src/context.rs +++ b/dhall_core/src/context.rs @@ -31,8 +31,8 @@ impl<K: Hash + Eq + Clone, T> Context<K, T> { /// lookup k n (insert k v c) = lookup k (n - 1) c -- 1 <= n /// lookup k n (insert j v c) = lookup k n c -- k /= j /// ``` - pub fn lookup<'a>(&'a self, k: K, n: usize) -> Option<&'a T> { - self.0.get(&k).and_then(|v| v.get(v.len() - 1 - n)) + pub fn lookup<'a>(&'a self, k: &K, n: usize) -> Option<&'a T> { + self.0.get(k).and_then(|v| v.get(v.len() - 1 - n)) } pub fn map<U, F: Fn(&T) -> U>(&self, f: F) -> Context<K, U> { diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs index cbf0654..d832a18 100644 --- a/dhall_core/src/core.rs +++ b/dhall_core/src/core.rs @@ -1,6 +1,7 @@ #![allow(non_snake_case)] use std::collections::BTreeMap; use std::fmt::{self, Display}; +use std::hash::Hash; use std::path::PathBuf; /// Constants for a pure type system @@ -144,12 +145,23 @@ pub enum Expr_<Label, Note, Embed> { /// `Var (V x n) ~ x@n` Var(V<Label>), /// `Lam x A b ~ λ(x : A) -> b` - Lam(Label, Box<Expr_<Label, Note, Embed>>, Box<Expr_<Label, Note, Embed>>), + Lam( + Label, + Box<Expr_<Label, Note, Embed>>, + Box<Expr_<Label, Note, Embed>>, + ), /// `Pi "_" A B ~ A -> B` /// `Pi x A B ~ ∀(x : A) -> B` - Pi(Label, Box<Expr_<Label, Note, Embed>>, Box<Expr_<Label, Note, Embed>>), + Pi( + Label, + Box<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( @@ -159,11 +171,18 @@ 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 - BinOp(BinOp, Box<Expr_<Label, Note, Embed>>, Box<Expr_<Label, Note, Embed>>), + BinOp( + BinOp, + Box<Expr_<Label, Note, Embed>>, + Box<Expr_<Label, Note, Embed>>, + ), /// `BoolLit b ~ b` BoolLit(bool), /// `BoolIf x y z ~ if x then y else z` @@ -181,10 +200,16 @@ pub enum Expr_<Label, Note, Embed> { /// `TextLit t ~ t` TextLit(Builder), /// `ListLit t [x, y, z] ~ [x, y, z] : List t` - ListLit(Option<Box<Expr_<Label, Note, Embed>>>, Vec<Expr_<Label, Note, Embed>>), + ListLit( + Option<Box<Expr_<Label, Note, Embed>>>, + Vec<Expr_<Label, Note, Embed>>, + ), /// `OptionalLit t [e] ~ [e] : Optional t` /// `OptionalLit t [] ~ [] : Optional t` - OptionalLit(Option<Box<Expr_<Label, Note, Embed>>>, Vec<Expr_<Label, Note, Embed>>), + OptionalLit( + Option<Box<Expr_<Label, Note, Embed>>>, + Vec<Expr_<Label, Note, Embed>>, + ), /// `Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 }` Record(BTreeMap<Label, Expr_<Label, Note, Embed>>), /// `RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 }` @@ -243,8 +268,26 @@ pub enum Builtin { TextShow, } -impl<'i> From<&'i str> for V<&'i str> { - fn from(s: &'i str) -> Self { +pub trait StringLike: + Display + fmt::Debug + Clone + Copy + Hash + Ord + Eq + Into<String> + Default +{ +} + +impl<T> StringLike for T where + T: Display + + fmt::Debug + + Clone + + Copy + + Hash + + Ord + + Eq + + Into<String> + + Default +{ +} + +impl<Label> From<Label> for V<Label> { + fn from(s: Label) -> Self { V(s, 0) } } @@ -255,39 +298,43 @@ impl<'i, S, A> From<&'i str> for Expr<'i, S, A> { } } -impl<'i, S, A> From<Builtin> for Expr<'i, S, A> { +impl<L, S, A> From<Builtin> for Expr_<L, S, A> { fn from(t: Builtin) -> Self { Expr_::Builtin(t) } } -impl<'i, S, A> Expr<'i, S, A> { - pub fn map_shallow<T, B, F1, F2, F3>( +impl<Label: StringLike, S, A> Expr_<Label, S, A> { + pub fn map_shallow<T, B, Label2, F1, F2, F3, F4>( &self, map_expr: F1, map_note: F2, map_embed: F3, - ) -> Expr<'i, T, B> + map_label: F4, + ) -> Expr_<Label2, T, B> where A: Clone, T: Clone, S: Clone, - F1: Fn(&Self) -> Expr<'i, T, B>, + Label2: StringLike, + F1: Fn(&Self) -> Expr_<Label2, T, B>, F2: FnOnce(&S) -> T, F3: FnOnce(&A) -> B, + F4: Fn(&Label) -> Label2, { - map_shallow(self, map_expr, map_note, map_embed) + map_shallow(self, map_expr, map_note, map_embed, map_label) } - pub fn map_embed<B, F>(&self, map_embed: &F) -> Expr<'i, S, B> + pub fn map_embed<B, F>(&self, map_embed: &F) -> Expr_<Label, S, B> where A: Clone, S: Clone, F: Fn(&A) -> B, { - let recurse = - |e: &Expr<'i, S, A>| -> Expr<'i, S, B> { e.map_embed(map_embed) }; - map_shallow(self, recurse, |x| x.clone(), map_embed) + let recurse = |e: &Expr_<Label, S, A>| -> Expr_<Label, S, B> { + e.map_embed(map_embed) + }; + self.map_shallow(recurse, |x| x.clone(), map_embed, |x| x.clone()) } pub fn bool_lit(&self) -> Option<bool> { @@ -312,6 +359,14 @@ impl<'i, S, A> Expr<'i, S, A> { } } +// impl<'i, S: Clone, A: Clone> Expr_<&'i str, S, A> { +// pub fn to_owned(&self) -> Expr_<String, S, A> { +// let recurse = +// |e: &Expr_<&'i str, S, A>| -> Expr_<String, S, A> { e.to_owned() }; +// self.map_shallow(recurse, |x| x.clone(), |x| x.clone(), |x| x.to_owned()) +// } +// } + // There is a one-to-one correspondence between the formatters in this section // and the grammar in grammar.lalrpop. Each formatter is named after the // corresponding grammar rule and the relationship between formatters exactly matches @@ -322,7 +377,7 @@ impl<'i, S, A> Expr<'i, S, A> { // you add a new constructor to the syntax tree without adding a matching // case the corresponding builder. -impl<'i, S, A: Display> Display for Expr<'i, S, A> { +impl<Label: Display, S, A: Display> Display for Expr_<Label, S, A> { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { // buildExprA use crate::Expr_::*; @@ -338,11 +393,11 @@ impl<'i, S, A: Display> Display for Expr<'i, S, A> { } } -impl<'i, S, A: Display> Expr<'i, S, A> { +impl<Label: Display, S, A: Display> Expr_<Label, S, A> { fn fmt_b(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { use crate::Expr_::*; match self { - &Lam(a, ref b, ref c) => { + &Lam(ref a, ref b, ref c) => { write!(f, "λ({} : ", a)?; b.fmt(f)?; write!(f, ") → ")?; @@ -356,24 +411,25 @@ impl<'i, S, A: Display> Expr<'i, S, A> { write!(f, " else ")?; c.fmt_c(f) } - &Pi("_", ref b, ref c) => { - b.fmt_c(f)?; - write!(f, " → ")?; - c.fmt_b(f) - } - &Pi(a, ref b, ref c) => { + // TODO: wait for decision on label types + // &Pi("_", ref b, ref c) => { + // b.fmt_c(f)?; + // write!(f, " → ")?; + // c.fmt_b(f) + // } + &Pi(ref a, ref b, ref c) => { write!(f, "∀({} : ", a)?; b.fmt(f)?; write!(f, ") → ")?; c.fmt_b(f) } - &Let(a, None, ref c, ref d) => { + &Let(ref a, None, ref c, ref d) => { write!(f, "let {} = ", a)?; c.fmt(f)?; write!(f, ") → ")?; d.fmt_b(f) } - &Let(a, Some(ref b), ref c, ref d) => { + &Let(ref a, Some(ref b), ref c, ref d) => { write!(f, "let {} : ", a)?; b.fmt(f)?; write!(f, " = ")?; @@ -488,7 +544,7 @@ impl<'i, S, A: Display> Expr<'i, S, A> { fn fmt_e(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { use crate::Expr_::*; match self { - &Field(ref a, b) => { + &Field(ref a, ref b) => { a.fmt_e(f)?; write!(f, ".{}", b) } @@ -499,7 +555,7 @@ impl<'i, S, A: Display> Expr<'i, S, A> { fn fmt_f(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { use crate::Expr_::*; - match self { + match &self { &Var(a) => a.fmt(f), &Const(k) => k.fmt(f), &Builtin(v) => v.fmt(f), @@ -521,7 +577,7 @@ impl<'i, S, A: Display> Expr<'i, S, A> { write!(f, "{} = {}", k, v) }), &Union(ref _a) => f.write_str("Union"), - &UnionLit(_a, ref _b, ref _c) => f.write_str("UnionLit"), + &UnionLit(ref _a, ref _b, ref _c) => f.write_str("UnionLit"), &Embed(ref a) => a.fmt(f), &Note(_, ref b) => b.fmt_f(f), a => write!(f, "({})", a), @@ -633,34 +689,34 @@ impl Builtin { } } -impl<'i> Display for V<&'i str> { +impl<Label: Display> Display for V<Label> { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { - let V(x, n) = *self; - f.write_str(x)?; - if n != 0 { + let V(ref x, ref n) = *self; + x.fmt(f)?; + if *n != 0 { write!(f, "@{}", n)?; } Ok(()) } } -pub fn pi<'i, S, A, Name, Et, Ev>( +pub fn pi<Label, S, A, Name, Et, Ev>( var: Name, ty: Et, value: Ev, -) -> Expr<'i, S, A> +) -> Expr_<Label, S, A> where - Name: Into<&'i str>, - Et: Into<Expr<'i, S, A>>, - Ev: Into<Expr<'i, S, A>>, + Name: Into<Label>, + Et: Into<Expr_<Label, S, A>>, + Ev: Into<Expr_<Label, S, A>>, { Expr_::Pi(var.into(), bx(ty.into()), bx(value.into())) } -pub fn app<'i, S, A, Ef, Ex>(f: Ef, x: Ex) -> Expr<'i, S, A> +pub fn app<Label, S, A, Ef, Ex>(f: Ef, x: Ex) -> Expr_<Label, S, A> where - Ef: Into<Expr<'i, S, A>>, - Ex: Into<Expr<'i, S, A>>, + Ef: Into<Expr_<Label, S, A>>, + Ex: Into<Expr_<Label, S, A>>, { Expr_::App(bx(f.into()), bx(x.into())) } @@ -693,30 +749,37 @@ fn add_ui(u: usize, i: isize) -> usize { } } -pub fn map_shallow<'i, S, T, A, B, F1, F2, F3>( - e: &Expr<'i, S, A>, +pub fn map_shallow<Label1, Label2, S, T, A, B, F1, F2, F3, F4>( + e: &Expr_<Label1, S, A>, map: F1, map_note: F2, map_embed: F3, -) -> Expr<'i, T, B> + map_label: F4, +) -> Expr_<Label2, T, B> where A: Clone, S: Clone, T: Clone, - F1: Fn(&Expr<'i, S, A>) -> Expr<'i, T, B>, + Label1: StringLike, + Label2: StringLike, + F1: Fn(&Expr_<Label1, S, A>) -> Expr_<Label2, T, B>, F2: FnOnce(&S) -> T, F3: FnOnce(&A) -> B, + F4: Fn(&Label1) -> Label2, { use crate::Expr_::*; - let bxmap = |x: &Expr<'i, S, A>| -> Box<Expr<'i, T, B>> { bx(map(x)) }; + let bxmap = + |x: &Expr_<Label1, S, A>| -> Box<Expr_<Label2, T, B>> { bx(map(x)) }; let opt = |x| map_opt_box(x, &map); match *e { Const(k) => Const(k), - Var(v) => Var(v), - Lam(x, ref t, ref b) => Lam(x, bxmap(t), bxmap(b)), - Pi(x, ref t, ref b) => Pi(x, bxmap(t), bxmap(b)), + 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)), App(ref f, ref a) => App(bxmap(f), bxmap(a)), - Let(l, ref t, ref a, ref b) => Let(l, opt(t), bxmap(a), bxmap(b)), + Let(ref l, ref t, ref a, ref b) => { + Let(map_label(l), opt(t), bxmap(a), bxmap(b)) + } Annot(ref x, ref t) => Annot(bxmap(x), bxmap(t)), Builtin(v) => Builtin(v), BoolLit(b) => BoolLit(b), @@ -734,27 +797,49 @@ where let es = es.iter().map(&map).collect(); OptionalLit(opt(t), es) } - Record(ref kts) => Record(map_record_value(kts, map)), - RecordLit(ref kvs) => RecordLit(map_record_value(kvs, map)), - Union(ref kts) => Union(map_record_value(kts, map)), - UnionLit(k, ref v, ref kvs) => { - UnionLit(k, bxmap(v), map_record_value(kvs, map)) + Record(ref kts) => { + Record(map_record_value_and_keys(kts, map, map_label)) + } + RecordLit(ref kvs) => { + 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, map, map_label), + ), Merge(ref x, ref y, ref t) => Merge(bxmap(x), bxmap(y), opt(t)), - Field(ref r, x) => Field(bxmap(r), x), + Field(ref r, ref x) => Field(bxmap(r), map_label(x)), Note(ref n, ref e) => Note(map_note(n), bxmap(e)), Embed(ref a) => Embed(map_embed(a)), } } -pub fn map_record_value<'a, I, K, V, U, F>(it: I, mut f: F) -> BTreeMap<K, U> +pub fn map_record_value<'a, I, K, V, U, F>(it: I, f: F) -> BTreeMap<K, U> where I: IntoIterator<Item = (&'a K, &'a V)>, K: Eq + Ord + Copy + 'a, V: 'a, F: FnMut(&V) -> U, { - it.into_iter().map(|(&k, v)| (k, f(v))).collect() + map_record_value_and_keys(it, f, |&x| x) +} + +pub fn map_record_value_and_keys<'a, I, K, L, V, U, F, G>( + it: I, + mut f: F, + mut g: G, +) -> BTreeMap<L, U> +where + I: IntoIterator<Item = (&'a K, &'a V)>, + K: Eq + Ord + 'a, + L: Eq + Ord + 'a, + V: 'a, + F: FnMut(&V) -> U, + G: FnMut(&K) -> L, +{ + it.into_iter().map(|(k, v)| (g(k), f(v))).collect() } pub fn map_opt_box<T, U, F>(x: &Option<Box<T>>, f: F) -> Option<Box<U>> @@ -843,11 +928,16 @@ 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<'i, S, T, A: Clone>( +pub fn shift<Label, S, T, A: Clone>( d: isize, - v: V<&'i str>, - e: &Expr<'i, S, A>, -) -> Expr<'i, T, A> { + v: V<Label>, + e: &Expr_<Label, S, A>, +) -> Expr_<Label, T, A> +where + Label: Copy, + Label: Ord, + Label: PartialEq, +{ use crate::Expr_::*; let V(x, n) = v; match *e { @@ -922,16 +1012,22 @@ pub fn shift<'i, S, T, A: Clone>( } } -fn shift_op2<'i, S, T, A, F>( +fn shift_op2<Label, S, T, A, F>( f: F, d: isize, - v: V<&'i str>, - a: &Expr<'i, S, A>, - b: &Expr<'i, S, A>, -) -> Expr<'i, T, A> + v: V<Label>, + a: &Expr_<Label, S, A>, + b: &Expr_<Label, S, A>, +) -> Expr_<Label, T, A> where - F: FnOnce(Box<Expr<'i, T, A>>, Box<Expr<'i, T, A>>) -> Expr<'i, T, A>, + F: FnOnce( + Box<Expr_<Label, T, A>>, + Box<Expr_<Label, T, A>>, + ) -> Expr_<Label, T, A>, A: Clone, + Label: Copy, + Label: Ord, + Label: PartialEq, { map_op2(f, |x| bx(shift(d, v, x)), a, b) } @@ -942,11 +1038,11 @@ where /// subst x C B ~ B[x := C] /// ``` /// -pub fn subst<'i, S, T, A>( - v: V<&'i str>, - e: &Expr<'i, S, A>, - b: &Expr<'i, T, A>, -) -> Expr<'i, S, A> +pub fn subst<Label: StringLike, S, T, A>( + v: V<Label>, + e: &Expr_<Label, S, A>, + b: &Expr_<Label, T, A>, +) -> Expr_<Label, S, A> where S: Clone, A: Clone, @@ -965,7 +1061,7 @@ where let n2 = if x == y { n + 1 } else { n }; let tB2 = subst(V(x, n2), &shift(1, V(y, 0), e), tB); let tA2 = subst(V(x, n), e, tA); - pi(y, tA2, tB2) + Pi(y, bx(tA2), bx(tB2)) } App(ref f, ref a) => { let f2 = subst(v, e, f); @@ -1028,15 +1124,18 @@ where } } -fn subst_op2<'i, S, T, A, F>( +fn subst_op2<Label: StringLike, S, T, A, F>( f: F, - v: V<&'i str>, - e: &Expr<'i, S, A>, - a: &Expr<'i, T, A>, - b: &Expr<'i, T, A>, -) -> Expr<'i, S, A> + v: V<Label>, + e: &Expr_<Label, S, A>, + a: &Expr_<Label, T, A>, + b: &Expr_<Label, T, A>, +) -> Expr_<Label, S, A> where - F: FnOnce(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>) -> Expr<'i, S, A>, + F: FnOnce( + Box<Expr_<Label, S, A>>, + Box<Expr_<Label, S, A>>, + ) -> Expr_<Label, S, A>, S: Clone, A: Clone, { diff --git a/dhall_generator/src/lib.rs b/dhall_generator/src/lib.rs index 1cc62d0..7f2e295 100644 --- a/dhall_generator/src/lib.rs +++ b/dhall_generator/src/lib.rs @@ -4,8 +4,6 @@ use dhall_core::*; use proc_macro2::Literal; use proc_macro2::TokenStream; use quote::quote; -use std::fmt::Debug; -use std::hash::Hash; #[proc_macro] pub fn dhall(input: proc_macro::TokenStream) -> proc_macro::TokenStream { @@ -20,7 +18,7 @@ pub fn dhall(input: proc_macro::TokenStream) -> proc_macro::TokenStream { // Returns an expression of type Expr<_, _>. Expects input variables // to be of type Box<Expr<_, _>> (future-proof for structural sharing). -fn dhall_to_tokenstream<L: Eq + Hash + Clone + Debug + Into<String>>( +fn dhall_to_tokenstream<L: StringLike>( expr: &Expr_<L, X, X>, ctx: &Context<L, ()>, ) -> TokenStream { @@ -34,7 +32,7 @@ fn dhall_to_tokenstream<L: Eq + Hash + Clone + Debug + Into<String>>( let t = dhall_to_tokenstream_bx(t, ctx); let b = dhall_to_tokenstream_bx(b, &ctx.insert(x.clone(), ())); let x = Literal::string(&x.clone().into()); - quote! { Lam(#x, #t, #b) } + quote! { Lam(#x.to_owned().into(), #t, #b) } } App(f, a) => { let f = dhall_to_tokenstream_bx(f, ctx); @@ -76,18 +74,18 @@ fn dhall_to_tokenstream<L: Eq + Hash + Clone + Debug + Into<String>>( } // Returns an expression of type Box<Expr<_, _>> -fn dhall_to_tokenstream_bx<L: Eq + Hash + Clone + Debug + Into<String>>( +fn dhall_to_tokenstream_bx<L: StringLike>( expr: &Expr_<L, X, X>, ctx: &Context<L, ()>, ) -> TokenStream { use dhall_core::Expr_::*; match expr { Var(V(s, n)) => { - match ctx.lookup(s.clone(), *n) { + match ctx.lookup(&s, *n) { // Non-free variable; interpolates as itself Some(()) => { let s: String = s.clone().into(); - quote! { bx(Var(V(#s, #n))) } + quote! { bx(Var(V(#s.to_owned().into(), #n))) } } // Free variable; interpolates as a rust variable None => { @@ -95,7 +93,7 @@ fn dhall_to_tokenstream_bx<L: Eq + Hash + Clone + Debug + Into<String>>( // TODO: insert appropriate shifts ? let v: TokenStream = s.parse().unwrap(); quote! { { - let x: Box<Expr<_, _>> = #v.clone(); + let x: Box<Expr_<_, _, _>> = #v.clone(); x } } } |