From 6037cb224c5e61828ba41cb3d34438ad03a71403 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 9 Mar 2019 15:46:30 +0100 Subject: Remove the pervasive Label type parameter Closes #1 --- dhall/src/imports.rs | 10 ++-- dhall/src/main.rs | 2 +- dhall/src/normalize.rs | 6 +-- dhall/src/typecheck.rs | 136 ++++++++++++++++++++----------------------------- dhall/tests/macros.rs | 4 +- 5 files changed, 65 insertions(+), 93 deletions(-) (limited to 'dhall') 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( - expr: &Expr, -) -> Expr { +pub fn panic_imports(expr: &Expr) -> Expr { 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, DhallError> { +) -> Result, 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, DhallError> { +) -> Result, 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 { + let resolve = |import: &Import| -> Expr { 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 = 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(e: &Expr) -> Expr +pub fn normalize(e: &Expr) -> Expr 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 { } } -fn match_vars(vl: &V, vr: &V, 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(vl: &V, vr: &V, ctx: &[(L, L)]) -> bool { } } -fn prop_equal(eL0: &Expr, eR0: &Expr) -> bool +fn prop_equal(eL0: &Expr, eR0: &Expr) -> bool where S: Clone + ::std::fmt::Debug, T: Clone + ::std::fmt::Debug, { fn go( ctx: &mut Vec<(Label, Label)>, - el: &Expr, - er: &Expr, + el: &Expr, + er: &Expr, ) -> bool where S: Clone + ::std::fmt::Debug, @@ -144,16 +144,16 @@ where } fn op2_type( - ctx: &Context>, - e: &Expr, + ctx: &Context>, + e: &Expr, t: core::Builtin, ef: EF, - l: &Expr, - r: &Expr, -) -> Result, TypeError> + l: &Expr, + r: &Expr, +) -> Result, TypeError> where S: Clone + ::std::fmt::Debug, - EF: FnOnce(Expr, Expr) -> TypeMessage, + EF: FnOnce(Expr, Expr) -> TypeMessage, { 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( - ctx: &Context>, - e: &Expr, -) -> Result, TypeError> + ctx: &Context>, + e: &Expr, +) -> Result, TypeError> 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> = match t { + let t: Box> = 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> = BTreeMap::new(); + let mut m: BTreeMap> = 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> = match t { + let t: Box> = 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( - e: &Expr, -) -> Result, TypeError> { + e: &Expr, +) -> Result, TypeError> { let ctx = Context::new(); type_with(&ctx, e) //.map(|e| e.into_owned()) } @@ -717,83 +717,59 @@ pub fn type_of( #[derive(Debug)] pub enum TypeMessage { UnboundVariable, - InvalidInputType(Expr), - InvalidOutputType(Expr), - NotAFunction(Expr, Expr), - TypeMismatch( - Expr, - Expr, - Expr, - Expr, - ), - AnnotMismatch(Expr, Expr, Expr), + InvalidInputType(Expr), + InvalidOutputType(Expr), + NotAFunction(Expr, Expr), + TypeMismatch(Expr, Expr, Expr, Expr), + AnnotMismatch(Expr, Expr, Expr), Untyped, - InvalidListElement( - usize, - Expr, - Expr, - Expr, - ), - InvalidListType(Expr), - InvalidOptionalElement( - Expr, - Expr, - Expr, - ), + InvalidListElement(usize, Expr, Expr, Expr), + InvalidListType(Expr), + InvalidOptionalElement(Expr, Expr, Expr), InvalidOptionalLiteral(usize), - InvalidOptionalType(Expr), - InvalidPredicate(Expr, Expr), - IfBranchMismatch( - Expr, - Expr, - Expr, - Expr, - ), - IfBranchMustBeTerm( - bool, - Expr, - Expr, - Expr, - ), - InvalidField(Label, Expr), - InvalidFieldType(Label, Expr), - InvalidAlternative(Label, Expr), - InvalidAlternativeType(Label, Expr), + InvalidOptionalType(Expr), + InvalidPredicate(Expr, Expr), + IfBranchMismatch(Expr, Expr, Expr, Expr), + IfBranchMustBeTerm(bool, Expr, Expr, Expr), + InvalidField(Label, Expr), + InvalidFieldType(Label, Expr), + InvalidAlternative(Label, Expr), + InvalidAlternativeType(Label, Expr), DuplicateAlternative(Label), - MustCombineARecord(Expr, Expr), + MustCombineARecord(Expr, Expr), FieldCollision(Label), - MustMergeARecord(Expr, Expr), - MustMergeUnion(Expr, Expr), + MustMergeARecord(Expr, Expr), + MustMergeUnion(Expr, Expr), UnusedHandler(HashSet