From 66bed8dbc7249e17a89adcbb19406f4126a434de Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 8 Mar 2019 22:37:32 +0100 Subject: Finally get rid of all the &'i str --- dhall/src/imports.rs | 15 ++-- dhall/src/lib.rs | 3 +- dhall/src/main.rs | 2 +- dhall/src/typecheck.rs | 197 +++++++++++++++++++++++---------------------- dhall/tests/macros.rs | 5 +- dhall_core/src/core.rs | 20 ++--- dhall_generator/src/lib.rs | 4 +- 7 files changed, 126 insertions(+), 120 deletions(-) diff --git a/dhall/src/imports.rs b/dhall/src/imports.rs index 6d8d670..4240b5e 100644 --- a/dhall/src/imports.rs +++ b/dhall/src/imports.rs @@ -1,12 +1,11 @@ -use dhall_core::{Expr, FilePrefix, Import, ImportLocation, ImportMode, X}; +// use dhall_core::{Expr, FilePrefix, Import, ImportLocation, ImportMode, X}; +use dhall_core::{Expr_, StringLike, Import, X}; +// use std::path::Path; +// use std::path::PathBuf; -// fn resolve_import(import: Import) -> Expr { - -// } - -pub fn resolve_imports<'i, S: Clone>( - expr: &Expr<'i, S, Import>, -) -> Expr<'i, S, X> { +pub fn resolve_imports( + expr: &Expr_, +) -> Expr_ { let no_import = |_: &Import| -> X { panic!("ahhh import") }; expr.map_embed(&no_import) } diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index d7758f1..66d132e 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -44,11 +44,12 @@ pub fn load_dhall_file<'i, 'a: 'i>( f: &Path, source_pool: &'a mut Vec, _resolve_imports: bool, -) -> Result, DhallError> { +) -> Result, DhallError> { source_pool.push(String::new()); let mut buffer = source_pool.last_mut().unwrap(); File::open(f)?.read_to_string(&mut buffer)?; let expr = parser::parse_expr(&*buffer)?; + let expr = expr.take_ownership_of_labels(); let expr = imports::resolve_imports(&expr); Ok(expr) } diff --git a/dhall/src/main.rs b/dhall/src/main.rs index dbe80a3..b571996 100644 --- a/dhall/src/main.rs +++ b/dhall/src/main.rs @@ -65,7 +65,7 @@ fn main() { } }; - let expr = imports::resolve_imports(&expr); + let expr: Expr_ = imports::resolve_imports(&expr.take_ownership_of_labels()); let type_expr = match typecheck::type_of(&expr) { Err(e) => { diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index b7fead3..1c15d88 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -10,13 +10,13 @@ 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, Expr_, V, X}; +use dhall_core::core::{bx, shift, subst, Expr, Expr_, V, X, StringLike}; use self::TypeMessage::*; -fn axiom<'i, S: Clone>( +fn axiom( c: core::Const, -) -> Result> { +) -> Result> { match c { Type => Ok(Kind), Kind => Err(TypeError::new(&Context::new(), &Const(Kind), Untyped)), @@ -31,32 +31,32 @@ fn rule(a: core::Const, b: core::Const) -> Result { } } -fn match_vars(vl: &V<&str>, vr: &V<&str>, ctx: &[(&str, &str)]) -> bool { - let xxs = ctx.get(0).map(|x| (x, ctx.split_at(1).1)); +fn match_vars(vl: &V, vr: &V, ctx: &[(L, L)]) -> bool { + let xxs: Option<(&(L, L), &[(L, L)])> = 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), _))) + (V(xL, nL), V(xR, nR), None) => xL == xR && nL == nR, + (V(xL, 0), V(xR, 0), Some(((xL2, xR2), _))) if xL == xL2 && xR == xR2 => { true } - (&V(xL, nL), &V(xR, nR), Some((&(xL2, xR2), xs))) => { - let nL2 = if xL == xL2 { nL - 1 } else { nL }; - let nR2 = if xR == xR2 { nR - 1 } else { nR }; - match_vars(&V(xL, nL2), &V(xR, nR2), xs) + (V(xL, nL), V(xR, nR), Some(((xL2, xR2), xs))) => { + let nL2 = if xL == xL2 { nL - 1 } else { *nL }; + let nR2 = if xR == xR2 { nR - 1 } else { *nR }; + match_vars(&V(xL.clone(), nL2), &V(xR.clone(), nR2), xs) } } } -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<'i, S, T>( - ctx: &mut Vec<(&'i str, &'i str)>, - el: &'i Expr<'i, S, X>, - er: &'i Expr<'i, T, X>, + fn go( + ctx: &mut Vec<(L, L)>, + el: &Expr_, + er: &Expr_, ) -> bool where S: Clone + ::std::fmt::Debug, @@ -65,12 +65,12 @@ where match (el, er) { (&Const(Type), &Const(Type)) | (&Const(Kind), &Const(Kind)) => true, (&Var(ref vL), &Var(ref vR)) => match_vars(vL, vR, &*ctx), - (&Pi(xL, ref tL, ref bL), &Pi(xR, ref tR, ref bR)) => { + (&Pi(ref xL, ref tL, ref bL), &Pi(ref xR, ref tR, ref bR)) => { //ctx <- State.get let eq1 = go(ctx, tL, tR); if eq1 { //State.put ((xL, xR):ctx) - ctx.push((xL, xR)); + ctx.push((xL.clone(), xR.clone())); let eq2 = go(ctx, bL, bR); //State.put ctx let _ = ctx.pop(); @@ -142,20 +142,20 @@ where } } let mut ctx = vec![]; - go::(&mut ctx, &normalize(eL0), &normalize(eR0)) + go::(&mut ctx, &normalize(eL0), &normalize(eR0)) } -fn op2_type<'i, S, EF>( - ctx: &Context<&'i str, Expr<'i, S, X>>, - e: &Expr<'i, S, X>, +fn op2_type, S, EF>( + ctx: &Context>, + e: &Expr_, t: core::Builtin, ef: EF, - l: &Expr<'i, S, X>, - r: &Expr<'i, S, X>, -) -> Result, TypeError<'i, S>> + l: &Expr_, + r: &Expr_, +) -> Result, TypeError> where - S: Clone + ::std::fmt::Debug + 'i, - EF: FnOnce(Expr<'i, S, X>, Expr<'i, S, X>) -> TypeMessage<&'i str, S>, + S: Clone + ::std::fmt::Debug, + EF: FnOnce(Expr_, Expr_) -> TypeMessage, { let tl = normalize(&type_with(ctx, l)?); match tl { @@ -178,12 +178,12 @@ where /// `type_with` does not necessarily normalize the type since full normalization /// 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<'i, S>( - ctx: &Context<&'i str, Expr<'i, S, X>>, - e: &Expr<'i, S, X>, -) -> Result, TypeError<'i, S>> +pub fn type_with, S>( + ctx: &Context>, + e: &Expr_, +) -> Result, TypeError> where - S: Clone + ::std::fmt::Debug + 'i, + S: Clone + ::std::fmt::Debug, { use dhall_core::BinOp::*; use dhall_core::Expr_; @@ -195,17 +195,17 @@ where //.map(Cow::Borrowed) .ok_or_else(|| TypeError::new(ctx, e, UnboundVariable)) } - Lam(x, ref tA, ref b) => { + Lam(ref x, ref tA, ref b) => { let ctx2 = ctx - .insert(x, (**tA).clone()) - .map(|e| core::shift(1, &V(x, 0), e)); + .insert(x.clone(), (**tA).clone()) + .map(|e| core::shift(1, &V(x.clone(), 0), e)); let tB = type_with(&ctx2, b)?; - let p = Pi(x, tA.clone(), bx(tB)); + let p = Pi(x.clone(), tA.clone(), bx(tB)); let _ = type_with(ctx, &p)?; //Ok(Cow::Owned(p)) Ok(p) } - Pi(x, ref tA, ref tB) => { + Pi(ref x, ref tA, ref tB) => { let tA2 = normalize::<_, S, S, X>(&type_with(ctx, tA)?); let kA = match tA2 { Const(k) => k, @@ -219,8 +219,8 @@ where }; let ctx2 = ctx - .insert(x, (**tA).clone()) - .map(|e| core::shift(1, &V(x, 0), e)); + .insert(x.clone(), (**tA).clone()) + .map(|e| core::shift(1, &V(x.clone(), 0), e)); let tB = normalize(&type_with(&ctx2, tB)?); let kB = match tB { 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::<&str, S, S, X>(1, vx0, a); + let a2 = shift::(1, vx0, a); let tB2 = subst(vx0, &a2, &tB); - let tB3 = shift::<&str, S, S, X>(-1, vx0, &tB2); + let tB3 = shift::(-1, vx0, &tB2); Ok(tB3) } else { let nf_A = normalize(&tA); @@ -267,7 +267,7 @@ where )) } } - Let(f, ref mt, ref r, ref b) => { + 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 kR = match ttR { @@ -277,7 +277,7 @@ where _ => return Err(TypeError::new(ctx, e, InvalidInputType(tR))), }; - let ctx2 = ctx.insert(f, tR.clone()); + let ctx2 = ctx.insert(f.clone(), tR.clone()); let tB = type_with(&ctx2, b)?; let ttB = normalize::<_, S, S, X>(&type_with(ctx, &tB)?); let kB = match ttB { @@ -387,7 +387,7 @@ where pi("zero", "natural", "natural"), ), ), - )), + ).take_ownership_of_labels()), Builtin(NaturalBuild) => Ok(pi( "_", pi( @@ -400,9 +400,9 @@ where ), ), Natural, - )), + ).take_ownership_of_labels()), Builtin(NaturalIsZero) | Builtin(NaturalEven) | Builtin(NaturalOdd) => { - Ok(pi("_", Natural, Bool)) + 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) @@ -418,7 +418,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(); @@ -461,7 +461,7 @@ where ), app(List, "a"), ), - )), + ).take_ownership_of_labels()), Builtin(ListFold) => Ok(pi( "a", Const(Type), @@ -478,33 +478,38 @@ where ), ), ), - )), + ).take_ownership_of_labels()), Builtin(ListLength) => { - Ok(pi("a", Const(Type), pi("_", app(List, "a"), Natural))) + 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()), Builtin(ListIndexed) => { - let mut m = BTreeMap::new(); - m.insert("index", Builtin(Natural)); - m.insert("value", Expr_::from("a")); - Ok(pi( - "a", - Const(Type), - pi("_", app(List, "a"), app(List, Record(m))), + let mut m: BTreeMap> = BTreeMap::new(); + m.insert("index".to_owned().into(), Builtin(Natural)); + let var: Expr_ = Var(V(Label::from("a".to_owned()), 0)); + m.insert("value".to_owned().into(), var.clone()); + let underscore: Label = Label::from("_".to_owned()); + let innerinner: Expr_ = app(List, Record(m)); + let innerinner2: Expr_ = app(List, var); + let inner: Expr_ = Pi(underscore, bx(innerinner2), bx(innerinner)); + Ok(Pi( + Label::from("a".to_owned()), + bx(Const(Type)), + bx(inner), )) } 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> = match t { + let t: Box> = match t { Some(t) => t.clone(), None => { let first_x = iter.next().unwrap(); @@ -553,9 +558,9 @@ where ), ), ), - )), + ).take_ownership_of_labels()), Builtin(List) | Builtin(Optional) => { - Ok(pi("_", Const(Type), Const(Type))) + Ok(pi("_", Const(Type), Const(Type)).take_ownership_of_labels()) } Builtin(Bool) | Builtin(Natural) | Builtin(Integer) | Builtin(Double) | Builtin(Text) => Ok(Const(Type)), @@ -568,7 +573,7 @@ where return Err(TypeError::new( ctx, e, - InvalidFieldType((*k).to_owned(), (*t).clone()), + InvalidFieldType((*k).clone(), (*t).clone()), )); } } @@ -578,7 +583,7 @@ where RecordLit(ref kvs) => { let kts = kvs .iter() - .map(|(&k, v)| { + .map(|(k, v)| { let t = type_with(ctx, v)?; let s = normalize::<_, S, S, X>(&type_with(ctx, &t)?); match s { @@ -587,11 +592,11 @@ where return Err(TypeError::new( ctx, e, - InvalidField((*k).to_owned(), (*v).clone()), + InvalidField((*k).clone(), (*v).clone()), )); } } - Ok((k, t)) + Ok(((*k).clone(), t)) }) .collect::>()?; Ok(Record(kts)) @@ -677,20 +682,20 @@ where mapM_ process (Data.Map.toList ktsY) return t */ - Field(ref r, x) => { + Field(ref r, ref x) => { 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()), + MissingField((*x).clone(), t.clone()), ) }), _ => Err(TypeError::new( ctx, e, - NotARecord(x.to_owned(), (**r).clone(), t.clone()), + NotARecord((*x).clone(), (**r).clone(), t.clone()), )), } } @@ -708,16 +713,16 @@ 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<'i, S: Clone + ::std::fmt::Debug + 'i>( - e: &Expr<'i, S, X>, -) -> Result, TypeError<'i, S>> { +pub fn type_of, S: Clone + ::std::fmt::Debug>( + e: &Expr_, +) -> Result, TypeError> { let ctx = Context::new(); type_with(&ctx, e) //.map(|e| e.into_owned()) } /// The specific type error #[derive(Debug)] -pub enum TypeMessage { +pub enum TypeMessage { UnboundVariable, InvalidInputType(Expr_), InvalidOutputType(Expr_), @@ -757,22 +762,22 @@ pub enum TypeMessage { Expr_, Expr_, ), - InvalidField(String, Expr_), - InvalidFieldType(String, Expr_), - InvalidAlternative(String, Expr_), - InvalidAlternativeType(String, Expr_), - DuplicateAlternative(String), + InvalidField(Label, Expr_), + InvalidFieldType(Label, Expr_), + InvalidAlternative(Label, Expr_), + InvalidAlternativeType(Label, Expr_), + DuplicateAlternative(Label), MustCombineARecord(Expr_, Expr_), - FieldCollision(String), + FieldCollision(Label), MustMergeARecord(Expr_, Expr_), MustMergeUnion(Expr_, Expr_), - UnusedHandler(HashSet), - MissingHandler(HashSet), - HandlerInputTypeMismatch(String, Expr_, Expr_), - HandlerOutputTypeMismatch(String, Expr_, Expr_), - HandlerNotAFunction(String, Expr_), - NotARecord(String, Expr_, Expr_), - MissingField(String, Expr_), + UnusedHandler(HashSet