diff options
Diffstat (limited to '')
| -rw-r--r-- | dhall/src/imports.rs | 10 | ||||
| -rw-r--r-- | dhall/src/main.rs | 2 | ||||
| -rw-r--r-- | dhall/src/normalize.rs | 6 | ||||
| -rw-r--r-- | dhall/src/typecheck.rs | 136 | ||||
| -rw-r--r-- | dhall/tests/macros.rs | 4 | ||||
| -rw-r--r-- | dhall_core/src/core.rs | 170 | ||||
| -rw-r--r-- | dhall_core/src/parser.rs | 2 | ||||
| -rw-r--r-- | dhall_generator/src/lib.rs | 8 |
8 files changed, 134 insertions, 204 deletions
diff --git a/dhall/src/imports.rs b/dhall/src/imports.rs index 3b8ba6d..007ed47 100644 --- a/dhall/src/imports.rs +++ b/dhall/src/imports.rs @@ -8,9 +8,7 @@ use std::io::Read; use std::path::Path; use std::path::PathBuf; -pub fn panic_imports<S: Clone>( - expr: &Expr<Label, S, Import>, -) -> Expr<Label, S, X> { +pub fn panic_imports<S: Clone>(expr: &Expr<S, Import>) -> Expr<S, X> { let no_import = |i: &Import| -> X { panic!("ahhh import: {:?}", i) }; expr.map_embed(&no_import) } @@ -24,7 +22,7 @@ pub enum ImportRoot { fn resolve_import( import: &Import, root: &ImportRoot, -) -> Result<Expr<Label, X, X>, DhallError> { +) -> Result<Expr<X, X>, DhallError> { use self::ImportRoot::*; use dhall_core::FilePrefix::*; use dhall_core::ImportLocation::*; @@ -71,13 +69,13 @@ impl fmt::Display for DhallError { pub fn load_dhall_file( f: &Path, resolve_imports: bool, -) -> Result<Expr<Label, X, X>, DhallError> { +) -> Result<Expr<X, X>, DhallError> { let mut buffer = String::new(); File::open(f)?.read_to_string(&mut buffer)?; let expr = parser::parse_expr(&*buffer)?; let expr = if resolve_imports { let root = ImportRoot::LocalDir(f.parent().unwrap().to_owned()); - let resolve = |import: &Import| -> Expr<Label, X, X> { + let resolve = |import: &Import| -> Expr<X, X> { resolve_import(import, &root).unwrap() }; let expr = expr.map_embed(&resolve).squash_embed(); diff --git a/dhall/src/main.rs b/dhall/src/main.rs index 349af3d..edc6baf 100644 --- a/dhall/src/main.rs +++ b/dhall/src/main.rs @@ -65,7 +65,7 @@ fn main() { } }; - let expr: Expr<Label, _, _> = imports::panic_imports(&expr); + let expr: Expr<_, _> = imports::panic_imports(&expr); let type_expr = match typecheck::type_of(&expr) { Err(e) => { diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 6344c52..b2ee0f6 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -12,7 +12,7 @@ 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<S, T, A>(e: &Expr<Label, S, A>) -> Expr<Label, T, A> +pub fn normalize<S, T, A>(e: &Expr<S, A>) -> Expr<T, A> where S: Clone + fmt::Debug, T: Clone + fmt::Debug, @@ -93,7 +93,7 @@ where normalize(&dhall_expr!(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_expr!(cons y ys) @@ -130,7 +130,7 @@ 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_expr!(just y) }); diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 0dbb2f9..28982fc 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -29,8 +29,8 @@ fn rule(a: core::Const, b: core::Const) -> Result<core::Const, ()> { } } -fn match_vars<L: Clone + Eq>(vl: &V<L>, vr: &V<L>, ctx: &[(L, L)]) -> bool { - let xxs: Option<(&(L, L), &[(L, L)])> = ctx.split_first(); +fn match_vars(vl: &V, vr: &V, ctx: &[(Label, Label)]) -> bool { + let xxs: Option<(&(Label, Label), &[(Label, Label)])> = ctx.split_first(); match (vl, vr, xxs) { (V(xL, nL), V(xR, nR), None) => xL == xR && nL == nR, (V(xL, 0), V(xR, 0), Some(((xL2, xR2), _))) @@ -46,15 +46,15 @@ fn match_vars<L: Clone + Eq>(vl: &V<L>, vr: &V<L>, ctx: &[(L, L)]) -> bool { } } -fn prop_equal<S, T>(eL0: &Expr<Label, S, X>, eR0: &Expr<Label, T, X>) -> bool +fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool where S: Clone + ::std::fmt::Debug, T: Clone + ::std::fmt::Debug, { fn go<S, T>( ctx: &mut Vec<(Label, Label)>, - el: &Expr<Label, S, X>, - er: &Expr<Label, T, X>, + el: &Expr<S, X>, + er: &Expr<T, X>, ) -> bool where S: Clone + ::std::fmt::Debug, @@ -144,16 +144,16 @@ where } fn op2_type<S, EF>( - ctx: &Context<Label, Expr<Label, S, X>>, - e: &Expr<Label, S, X>, + ctx: &Context<Label, Expr<S, X>>, + e: &Expr<S, X>, t: core::Builtin, ef: EF, - l: &Expr<Label, S, X>, - r: &Expr<Label, S, X>, -) -> Result<Expr<Label, S, X>, TypeError<S>> + l: &Expr<S, X>, + r: &Expr<S, X>, +) -> Result<Expr<S, X>, TypeError<S>> where S: Clone + ::std::fmt::Debug, - EF: FnOnce(Expr<Label, S, X>, Expr<Label, S, X>) -> TypeMessage<S>, + EF: FnOnce(Expr<S, X>, Expr<S, X>) -> TypeMessage<S>, { let tl = normalize(&type_with(ctx, l)?); match tl { @@ -177,9 +177,9 @@ where /// 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, Expr<Label, S, X>>, - e: &Expr<Label, S, X>, -) -> Result<Expr<Label, S, X>, TypeError<S>> + ctx: &Context<Label, Expr<S, X>>, + e: &Expr<S, X>, +) -> Result<Expr<S, X>, TypeError<S>> where S: Clone + ::std::fmt::Debug, { @@ -416,7 +416,7 @@ where } ListLit(ref t, ref xs) => { let mut iter = xs.iter().enumerate(); - let t: Box<Expr<_, _, _>> = match t { + let t: Box<Expr<_, _>> = match t { Some(t) => t.clone(), None => { let (_, first_x) = iter.next().unwrap(); @@ -486,7 +486,7 @@ where pi("_", app(List, "a"), app(Optional, "a")), )), Builtin(ListIndexed) => { - let mut m: BTreeMap<Label, Expr<Label, _, _>> = BTreeMap::new(); + let mut m: BTreeMap<Label, Expr<_, _>> = BTreeMap::new(); m.insert("index".into(), Builtin(Natural)); m.insert("value".into(), Var(V("a".into(), 0))); Ok(pi( @@ -502,7 +502,7 @@ where )), OptionalLit(ref t, ref xs) => { let mut iter = xs.iter(); - let t: Box<Expr<_, _, _>> = match t { + let t: Box<Expr<_, _>> = match t { Some(t) => t.clone(), None => { let first_x = iter.next().unwrap(); @@ -707,8 +707,8 @@ where /// expression must be closed (i.e. no free variables), otherwise type-checking /// will fail. pub fn type_of<S: Clone + ::std::fmt::Debug>( - e: &Expr<Label, S, X>, -) -> Result<Expr<Label, S, X>, TypeError<S>> { + e: &Expr<S, X>, +) -> Result<Expr<S, X>, TypeError<S>> { let ctx = Context::new(); type_with(&ctx, e) //.map(|e| e.into_owned()) } @@ -717,83 +717,59 @@ pub fn type_of<S: Clone + ::std::fmt::Debug>( #[derive(Debug)] pub enum TypeMessage<S> { UnboundVariable, - InvalidInputType(Expr<Label, S, X>), - InvalidOutputType(Expr<Label, S, X>), - NotAFunction(Expr<Label, S, X>, Expr<Label, S, X>), - TypeMismatch( - Expr<Label, S, X>, - Expr<Label, S, X>, - Expr<Label, S, X>, - Expr<Label, S, X>, - ), - AnnotMismatch(Expr<Label, S, X>, Expr<Label, S, X>, Expr<Label, S, X>), + InvalidInputType(Expr<S, X>), + InvalidOutputType(Expr<S, X>), + NotAFunction(Expr<S, X>, Expr<S, X>), + TypeMismatch(Expr<S, X>, Expr<S, X>, Expr<S, X>, Expr<S, X>), + AnnotMismatch(Expr<S, X>, Expr<S, X>, Expr<S, X>), Untyped, - 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>, - ), + InvalidListElement(usize, Expr<S, X>, Expr<S, X>, Expr<S, X>), + InvalidListType(Expr<S, X>), + InvalidOptionalElement(Expr<S, X>, Expr<S, X>, Expr<S, X>), InvalidOptionalLiteral(usize), - InvalidOptionalType(Expr<Label, S, X>), - InvalidPredicate(Expr<Label, S, X>, Expr<Label, S, X>), - IfBranchMismatch( - 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>, - ), - InvalidField(Label, Expr<Label, S, X>), - InvalidFieldType(Label, Expr<Label, S, X>), - InvalidAlternative(Label, Expr<Label, S, X>), - InvalidAlternativeType(Label, Expr<Label, S, X>), + InvalidOptionalType(Expr<S, X>), + InvalidPredicate(Expr<S, X>, Expr<S, X>), + IfBranchMismatch(Expr<S, X>, Expr<S, X>, Expr<S, X>, Expr<S, X>), + IfBranchMustBeTerm(bool, Expr<S, X>, Expr<S, X>, Expr<S, X>), + InvalidField(Label, Expr<S, X>), + InvalidFieldType(Label, Expr<S, X>), + InvalidAlternative(Label, Expr<S, X>), + InvalidAlternativeType(Label, Expr<S, X>), DuplicateAlternative(Label), - MustCombineARecord(Expr<Label, S, X>, Expr<Label, S, X>), + MustCombineARecord(Expr<S, X>, Expr<S, X>), FieldCollision(Label), - MustMergeARecord(Expr<Label, S, X>, Expr<Label, S, X>), - MustMergeUnion(Expr<Label, S, X>, Expr<Label, S, X>), + MustMergeARecord(Expr<S, X>, Expr<S, X>), + MustMergeUnion(Expr<S, X>, Expr<S, X>), UnusedHandler(HashSet<Label>), MissingHandler(HashSet<Label>), - HandlerInputTypeMismatch(Label, Expr<Label, S, X>, Expr<Label, S, X>), - HandlerOutputTypeMismatch(Label, Expr<Label, S, X>, Expr<Label, S, X>), - HandlerNotAFunction(Label, Expr<Label, S, X>), - NotARecord(Label, Expr<Label, S, X>, Expr<Label, S, X>), - MissingField(Label, 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>), + HandlerInputTypeMismatch(Label, Expr<S, X>, Expr<S, X>), + HandlerOutputTypeMismatch(Label, Expr<S, X>, Expr<S, X>), + HandlerNotAFunction(Label, Expr<S, X>), + NotARecord(Label, Expr<S, X>, Expr<S, X>), + MissingField(Label, Expr<S, X>), + CantAnd(Expr<S, X>, Expr<S, X>), + CantOr(Expr<S, X>, Expr<S, X>), + CantEQ(Expr<S, X>, Expr<S, X>), + CantNE(Expr<S, X>, Expr<S, X>), + CantTextAppend(Expr<S, X>, Expr<S, X>), + CantAdd(Expr<S, X>, Expr<S, X>), + CantMultiply(Expr<S, X>, Expr<S, X>), + NoDependentLet(Expr<S, X>, Expr<S, X>), + NoDependentTypes(Expr<S, X>, Expr<S, X>), } /// A structured type error that includes context #[derive(Debug)] pub struct TypeError<S> { - pub context: Context<Label, Expr<Label, S, X>>, - pub current: Expr<Label, S, X>, + pub context: Context<Label, Expr<S, X>>, + pub current: Expr<S, X>, pub type_message: TypeMessage<S>, } impl<S: Clone> TypeError<S> { pub fn new( - context: &Context<Label, Expr<Label, S, X>>, - current: &Expr<Label, S, X>, + context: &Context<Label, Expr<S, X>>, + current: &Expr<S, X>, type_message: TypeMessage<S>, ) -> Self { TypeError { diff --git a/dhall/tests/macros.rs b/dhall/tests/macros.rs index 10c4f5c..9ed48e0 100644 --- a/dhall/tests/macros.rs +++ b/dhall/tests/macros.rs @@ -73,9 +73,7 @@ pub enum ExpectedResult { Failure, } -pub fn read_dhall_file<'i>( - file_path: &str, -) -> Result<Expr<Label, X, X>, DhallError> { +pub fn read_dhall_file<'i>(file_path: &str) -> Result<Expr<X, X>, DhallError> { load_dhall_file(&PathBuf::from(file_path), true) } diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs index 7eaf08e..89fb6b9 100644 --- a/dhall_core/src/core.rs +++ b/dhall_core/src/core.rs @@ -1,7 +1,6 @@ #![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 @@ -139,8 +138,8 @@ impl Label { /// Zero indices are omitted when pretty-printing `Var`s and non-zero indices /// appear as a numeric suffix. /// -#[derive(Debug, Copy, Clone, PartialEq, Eq)] -pub struct V<Label>(pub Label, pub usize); +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct V(pub Label, pub usize); #[derive(Debug, Copy, Clone, PartialEq, Eq)] pub enum BinOp { @@ -172,52 +171,40 @@ pub enum BinOp { /// Syntax tree for expressions #[derive(Debug, Clone, PartialEq)] -pub enum Expr<Label, Note, Embed> { +pub enum Expr<Note, Embed> { /// `Const c ~ c` Const(Const), /// `Var (V x 0) ~ x`<br> /// `Var (V x n) ~ x@n` - Var(V<Label>), + Var(V), /// `Lam x A b ~ λ(x : A) -> b` - Lam( - Label, - Box<Expr<Label, Note, Embed>>, - Box<Expr<Label, Note, Embed>>, - ), + Lam(Label, Box<Expr<Note, Embed>>, Box<Expr<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<Note, Embed>>, Box<Expr<Note, Embed>>), /// `App f A ~ f A` - App(Box<Expr<Label, Note, Embed>>, Box<Expr<Label, Note, Embed>>), + App(Box<Expr<Note, Embed>>, Box<Expr<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( Label, - Option<Box<Expr<Label, Note, Embed>>>, - Box<Expr<Label, Note, Embed>>, - Box<Expr<Label, Note, Embed>>, + Option<Box<Expr<Note, Embed>>>, + Box<Expr<Note, Embed>>, + Box<Expr<Note, Embed>>, ), /// `Annot x t ~ x : t` - Annot(Box<Expr<Label, Note, Embed>>, Box<Expr<Label, Note, Embed>>), + Annot(Box<Expr<Note, Embed>>, Box<Expr<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<Note, Embed>>, Box<Expr<Note, Embed>>), /// `BoolLit b ~ b` BoolLit(bool), /// `BoolIf x y z ~ if x then y else z` BoolIf( - Box<Expr<Label, Note, Embed>>, - Box<Expr<Label, Note, Embed>>, - Box<Expr<Label, Note, Embed>>, + Box<Expr<Note, Embed>>, + Box<Expr<Note, Embed>>, + Box<Expr<Note, Embed>>, ), /// `NaturalLit n ~ +n` NaturalLit(Natural), @@ -228,38 +215,32 @@ 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<Note, Embed>>>, Vec<Expr<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<Note, Embed>>>, Vec<Expr<Note, Embed>>), /// `Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 }` - Record(BTreeMap<Label, Expr<Label, Note, Embed>>), + Record(BTreeMap<Label, Expr<Note, Embed>>), /// `RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 }` - RecordLit(BTreeMap<Label, Expr<Label, Note, Embed>>), + RecordLit(BTreeMap<Label, Expr<Note, Embed>>), /// `Union [(k1, t1), (k2, t2)] ~ < k1 : t1, k2 : t2 >` - Union(BTreeMap<Label, Expr<Label, Note, Embed>>), + Union(BTreeMap<Label, Expr<Note, Embed>>), /// `UnionLit (k1, v1) [(k2, t2), (k3, t3)] ~ < k1 = t1, k2 : t2, k3 : t3 >` UnionLit( Label, - Box<Expr<Label, Note, Embed>>, - BTreeMap<Label, Expr<Label, Note, Embed>>, + Box<Expr<Note, Embed>>, + BTreeMap<Label, Expr<Note, Embed>>, ), /// `Merge x y t ~ merge x y : t` Merge( - Box<Expr<Label, Note, Embed>>, - Box<Expr<Label, Note, Embed>>, - Option<Box<Expr<Label, Note, Embed>>>, + Box<Expr<Note, Embed>>, + Box<Expr<Note, Embed>>, + Option<Box<Expr<Note, Embed>>>, ), /// `Field e x ~ e.x` - Field(Box<Expr<Label, Note, Embed>>, Label), + Field(Box<Expr<Note, Embed>>, Label), /// Annotation on the AST. Unused for now but could hold e.g. file location information - Note(Note, Box<Expr<Label, Note, Embed>>), + Note(Note, Box<Expr<Note, Embed>>), /// Embeds an import or the result of resolving the import Embed(Embed), } @@ -296,49 +277,43 @@ pub enum Builtin { TextShow, } -impl From<Label> for V<Label> { +impl From<Label> for V { fn from(s: Label) -> Self { V(s, 0) } } -impl From<&'static str> for V<Label> { +impl From<&'static str> for V { fn from(s: &'static str) -> Self { V(s.into(), 0) } } -impl<'i, S, A> From<&'i str> for Expr<&'i str, S, A> { - fn from(s: &'i str) -> Self { - Expr::Var(V(s, 0)) - } -} - -impl<S, A> From<&'static str> for Expr<Label, S, A> { +impl<S, A> From<&'static str> for Expr<S, A> { fn from(s: &'static str) -> Self { Expr::Var(V(s.into(), 0)) } } -impl<Label, S, A> From<Builtin> for Expr<Label, S, A> { +impl<S, A> From<Builtin> for Expr<S, A> { fn from(t: Builtin) -> Self { Expr::Builtin(t) } } -impl<S, A> Expr<Label, S, A> { +impl<S, A> Expr<S, A> { pub fn map_shallow<T, B, F1, F2, F3, F4>( &self, map_expr: F1, map_note: F2, map_embed: F3, map_label: F4, - ) -> Expr<Label, T, B> + ) -> Expr<T, B> where A: Clone, T: Clone, S: Clone, - F1: Fn(&Self) -> Expr<Label, T, B>, + F1: Fn(&Self) -> Expr<T, B>, F2: FnOnce(&S) -> T, F3: FnOnce(&A) -> B, F4: Fn(&Label) -> Label, @@ -346,15 +321,13 @@ impl<S, A> Expr<Label, S, A> { map_shallow(self, map_expr, map_note, map_embed, map_label) } - pub fn map_embed<B, F>(&self, map_embed: &F) -> Expr<Label, S, B> + pub fn map_embed<B, F>(&self, map_embed: &F) -> Expr<S, B> where A: Clone, S: Clone, F: Fn(&A) -> B, { - let recurse = |e: &Expr<Label, S, A>| -> Expr<Label, S, B> { - e.map_embed(map_embed) - }; + let recurse = |e: &Expr<S, A>| -> Expr<S, B> { e.map_embed(map_embed) }; self.map_shallow(recurse, |x| x.clone(), map_embed, |x| x.clone()) } @@ -390,8 +363,8 @@ impl<S, A> Expr<Label, S, A> { } } -impl<S: Clone, A: Clone> Expr<Label, S, Expr<Label, S, A>> { - pub fn squash_embed(&self) -> Expr<Label, S, A> { +impl<S: Clone, A: Clone> Expr<S, Expr<S, A>> { + pub fn squash_embed(&self) -> Expr<S, A> { match self { Expr::Embed(e) => e.clone(), e => e.map_shallow( @@ -414,7 +387,7 @@ impl<S: Clone, A: Clone> Expr<Label, S, Expr<Label, S, A>> { // you add a new constructor to the syntax tree without adding a matching // case the corresponding builder. -impl<Label: Display, S, A: Display> Display for Expr<Label, S, A> { +impl<S, A: Display> Display for Expr<S, A> { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { // buildExprA use crate::Expr::*; @@ -430,7 +403,7 @@ impl<Label: Display, S, A: Display> Display for Expr<Label, S, A> { } } -impl<Label: Display, S, A: Display> Expr<Label, S, A> { +impl<S, A: Display> Expr<S, A> { fn fmt_b(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { use crate::Expr::*; match self { @@ -726,7 +699,7 @@ impl Builtin { } } -impl<Label: Display> Display for V<Label> { +impl Display for V { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { let V(ref x, ref n) = *self; x.fmt(f)?; @@ -737,19 +710,19 @@ impl<Label: Display> Display for V<Label> { } } -pub fn pi<S, A, Name, Et, Ev>(var: Name, ty: Et, value: Ev) -> Expr<Label, S, A> +pub fn pi<S, A, Name, Et, Ev>(var: Name, ty: Et, value: Ev) -> Expr<S, A> where Name: Into<Label>, - Et: Into<Expr<Label, S, A>>, - Ev: Into<Expr<Label, S, A>>, + Et: Into<Expr<S, A>>, + Ev: Into<Expr<S, A>>, { Expr::Pi(var.into(), bx(ty.into()), bx(value.into())) } -pub fn app<Label, S, A, Ef, Ex>(f: Ef, x: Ex) -> Expr<Label, S, A> +pub fn app<S, A, Ef, Ex>(f: Ef, x: Ex) -> Expr<S, A> where - Ef: Into<Expr<Label, S, A>>, - Ex: Into<Expr<Label, S, A>>, + Ef: Into<Expr<S, A>>, + Ex: Into<Expr<S, A>>, { Expr::App(bx(f.into()), bx(x.into())) } @@ -783,24 +756,23 @@ fn add_ui(u: usize, i: isize) -> usize { } pub fn map_shallow<S, T, A, B, F1, F2, F3, F4>( - e: &Expr<Label, S, A>, + e: &Expr<S, A>, map: F1, map_note: F2, map_embed: F3, map_label: F4, -) -> Expr<Label, T, B> +) -> Expr<T, B> where A: Clone, S: Clone, T: Clone, - F1: Fn(&Expr<Label, S, A>) -> Expr<Label, T, B>, + F1: Fn(&Expr<S, A>) -> Expr<T, B>, F2: FnOnce(&S) -> T, F3: FnOnce(&A) -> B, F4: Fn(&Label) -> Label, { use crate::Expr::*; - let bxmap = - |x: &Expr<Label, S, A>| -> Box<Expr<Label, T, B>> { bx(map(x)) }; + let bxmap = |x: &Expr<S, A>| -> Box<Expr<T, B>> { bx(map(x)) }; let opt = |x| map_opt_box(x, &map); match *e { Const(k) => Const(k), @@ -959,11 +931,7 @@ 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<S, T, A: Clone>( - d: isize, - v: &V<Label>, - e: &Expr<Label, S, A>, -) -> Expr<Label, T, A> { +pub fn shift<S, T, A: Clone>(d: isize, v: &V, e: &Expr<S, A>) -> Expr<T, A> { use crate::Expr::*; let V(x, n) = v; match e { @@ -1039,15 +1007,12 @@ pub fn shift<S, T, A: Clone>( fn shift_op2<S, T, A, F>( f: F, d: isize, - v: &V<Label>, - a: &Expr<Label, S, A>, - b: &Expr<Label, S, A>, -) -> Expr<Label, T, A> + v: &V, + a: &Expr<S, A>, + b: &Expr<S, A>, +) -> Expr<T, A> where - F: FnOnce( - Box<Expr<Label, T, A>>, - Box<Expr<Label, T, A>>, - ) -> Expr<Label, T, A>, + F: FnOnce(Box<Expr<T, A>>, Box<Expr<T, A>>) -> Expr<T, A>, A: Clone, { map_op2(f, |x| bx(shift(d, v, x)), a, b) @@ -1059,11 +1024,7 @@ where /// subst x C B ~ B[x := C] /// ``` /// -pub fn subst<S, T, A>( - v: &V<Label>, - e: &Expr<Label, S, A>, - b: &Expr<Label, T, A>, -) -> Expr<Label, S, A> +pub fn subst<S, T, A>(v: &V, e: &Expr<S, A>, b: &Expr<T, A>) -> Expr<S, A> where S: Clone, A: Clone, @@ -1150,16 +1111,13 @@ where fn subst_op2<S, T, A, F>( f: F, - v: &V<Label>, - e: &Expr<Label, S, A>, - a: &Expr<Label, T, A>, - b: &Expr<Label, T, A>, -) -> Expr<Label, S, A> + v: &V, + e: &Expr<S, A>, + a: &Expr<T, A>, + b: &Expr<T, A>, +) -> Expr<S, A> where - F: FnOnce( - Box<Expr<Label, S, A>>, - Box<Expr<Label, S, A>>, - ) -> Expr<Label, S, A>, + F: FnOnce(Box<Expr<S, A>>, Box<Expr<S, A>>) -> Expr<S, A>, S: Clone, A: Clone, { diff --git a/dhall_core/src/parser.rs b/dhall_core/src/parser.rs index 7073a93..2fa005a 100644 --- a/dhall_core/src/parser.rs +++ b/dhall_core/src/parser.rs @@ -8,7 +8,7 @@ use dhall_parser::{DhallParser, Rule}; use crate::core; use crate::core::*; -pub type ParsedExpr = Expr<Label, X, Import>; +pub type ParsedExpr = Expr<X, Import>; pub type BoxExpr = Box<ParsedExpr>; pub type ParseError = pest::error::Error<Rule>; diff --git a/dhall_generator/src/lib.rs b/dhall_generator/src/lib.rs index f633544..780b621 100644 --- a/dhall_generator/src/lib.rs +++ b/dhall_generator/src/lib.rs @@ -8,7 +8,7 @@ use quote::quote; #[proc_macro] pub fn dhall_expr(input: proc_macro::TokenStream) -> proc_macro::TokenStream { let input_str = input.to_string(); - let expr: Box<Expr<_, X, Import>> = parser::parse_expr(&input_str).unwrap(); + let expr: Box<Expr<X, Import>> = parser::parse_expr(&input_str).unwrap(); let no_import = |_: &Import| -> X { panic!("Don't use import in dhall!()") }; let expr = expr.map_embed(&no_import); @@ -19,7 +19,7 @@ pub fn dhall_expr(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( - expr: &Expr<Label, X, X>, + expr: &Expr<X, X>, ctx: &Context<Label, ()>, ) -> TokenStream { use dhall_core::Expr::*; @@ -75,7 +75,7 @@ fn dhall_to_tokenstream( // Returns an expression of type Box<Expr<_, _>> fn dhall_to_tokenstream_bx( - expr: &Expr<Label, X, X>, + expr: &Expr<X, X>, ctx: &Context<Label, ()>, ) -> TokenStream { use dhall_core::Expr::*; @@ -93,7 +93,7 @@ fn dhall_to_tokenstream_bx( // TODO: insert appropriate shifts ? let v: TokenStream = s.parse().unwrap(); quote! { { - let x: Box<Expr<_, _, _>> = #v.clone(); + let x: Box<Expr<_, _>> = #v.clone(); x } } } |