diff options
author | Nadrieril | 2019-03-08 22:37:32 +0100 |
---|---|---|
committer | Nadrieril | 2019-03-08 22:37:32 +0100 |
commit | 66bed8dbc7249e17a89adcbb19406f4126a434de (patch) | |
tree | 211c309fb3aea301314871899d1286b70eafa05c /dhall | |
parent | 0916eafc12b0ccbbf5b524a273903a0a84f30e74 (diff) |
Finally get rid of all the &'i str
Diffstat (limited to 'dhall')
-rw-r--r-- | dhall/src/imports.rs | 15 | ||||
-rw-r--r-- | dhall/src/lib.rs | 3 | ||||
-rw-r--r-- | dhall/src/main.rs | 2 | ||||
-rw-r--r-- | dhall/src/typecheck.rs | 197 | ||||
-rw-r--r-- | dhall/tests/macros.rs | 5 |
5 files changed, 114 insertions, 108 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<X, Import> { - -// } - -pub fn resolve_imports<'i, S: Clone>( - expr: &Expr<'i, S, Import>, -) -> Expr<'i, S, X> { +pub fn resolve_imports<Label: StringLike, S: Clone>( + expr: &Expr_<Label, S, Import>, +) -> Expr_<Label, S, X> { 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<String>, _resolve_imports: bool, -) -> Result<Expr<'i, X, X>, DhallError> { +) -> Result<Expr_<String, X, X>, 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_<String, _, _> = 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<Label: StringLike, S: Clone>( c: core::Const, -) -> Result<core::Const, TypeError<'i, S>> { +) -> Result<core::Const, TypeError<Label, S>> { 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<core::Const, ()> { } } -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<L: Clone + Eq>(vl: &V<L>, vr: &V<L>, 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<S, T>(eL0: &Expr<S, X>, eR0: &Expr<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, { - 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<L: StringLike, S, T>( + ctx: &mut Vec<(L, L)>, + el: &Expr_<L, S, X>, + er: &Expr_<L, T, X>, ) -> 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::<S, T>(&mut ctx, &normalize(eL0), &normalize(eR0)) + go::<L, S, T>(&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<Label: StringLike + From<String>, S, EF>( + ctx: &Context<Label, Expr_<Label, S, X>>, + e: &Expr_<Label, S, X>, t: core::Builtin, ef: EF, - l: &Expr<'i, S, X>, - r: &Expr<'i, S, X>, -) -> Result<Expr<'i, S, X>, TypeError<'i, S>> + l: &Expr_<Label, S, X>, + r: &Expr_<Label, S, X>, +) -> Result<Expr_<Label, S, X>, TypeError<Label, S>> 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_<Label, S, X>, Expr_<Label, S, X>) -> TypeMessage<Label, S>, { 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<Expr<'i, S, X>, TypeError<'i, S>> +pub fn type_with<Label: StringLike + From<String>, S>( + ctx: &Context<Label, Expr_<Label, S, X>>, + e: &Expr_<Label, S, X>, +) -> Result<Expr_<Label, S, X>, TypeError<Label, S>> 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::<Label, S, S, X>(1, vx0, a); let tB2 = subst(vx0, &a2, &tB); - let tB3 = shift::<&str, S, S, X>(-1, vx0, &tB2); + let tB3 = shift::<Label, S, S, X>(-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<Expr<_, _>> = match t { + let t: Box<Expr_<_, _, _>> = 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<Label, Expr_<Label, _, _>> = BTreeMap::new(); + m.insert("index".to_owned().into(), Builtin(Natural)); + let var: Expr_<Label, _, _> = 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_<Label, _, _> = app(List, Record(m)); + let innerinner2: Expr_<Label, _, _> = app(List, var); + let inner: Expr_<Label, _, _> = 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<Expr<_, _>> = match t { + let t: Box<Expr_<_, _, _>> = 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::<Result<_, _>>()?; 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<Expr<'i, S, X>, TypeError<'i, S>> { +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(); type_with(&ctx, e) //.map(|e| e.into_owned()) } /// The specific type error #[derive(Debug)] -pub enum TypeMessage<Label, S> { +pub enum TypeMessage<Label: std::hash::Hash + Eq, S> { UnboundVariable, InvalidInputType(Expr_<Label, S, X>), InvalidOutputType(Expr_<Label, S, X>), @@ -757,22 +762,22 @@ pub enum TypeMessage<Label, S> { Expr_<Label, S, X>, Expr_<Label, 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), + InvalidField(Label, Expr_<Label, S, X>), + InvalidFieldType(Label, Expr_<Label, S, X>), + InvalidAlternative(Label, Expr_<Label, S, X>), + InvalidAlternativeType(Label, Expr_<Label, S, X>), + DuplicateAlternative(Label), MustCombineARecord(Expr_<Label, S, X>, Expr_<Label, S, X>), - FieldCollision(String), + FieldCollision(Label), 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_<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>), + 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>), @@ -786,17 +791,17 @@ pub enum TypeMessage<Label, S> { /// A structured type error that includes context #[derive(Debug)] -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 str, S>, +pub struct TypeError<Label: std::hash::Hash + Eq, S> { + pub context: Context<Label, Expr_<Label, S, X>>, + pub current: Expr_<Label, S, X>, + pub type_message: TypeMessage<Label, S>, } -impl<'i, S: Clone> TypeError<'i, S> { +impl<Label: StringLike, S: Clone> TypeError<Label, S> { pub fn new( - context: &Context<&'i str, Expr<'i, S, X>>, - current: &Expr<'i, S, X>, - type_message: TypeMessage<&'i str, S>, + context: &Context<Label, Expr_<Label, S, X>>, + current: &Expr_<Label, S, X>, + type_message: TypeMessage<Label, S>, ) -> Self { TypeError { context: context.clone(), @@ -806,7 +811,7 @@ impl<'i, S: Clone> TypeError<'i, S> { } } -impl<'i, S: fmt::Debug> ::std::error::Error for TypeMessage<&'i str, S> { +impl<L: StringLike, S: fmt::Debug> ::std::error::Error for TypeMessage<L, S> { fn description(&self) -> &str { match *self { UnboundVariable => "Unbound variable", @@ -819,7 +824,7 @@ impl<'i, S: fmt::Debug> ::std::error::Error for TypeMessage<&'i str, S> { } } -impl<'i, S> fmt::Display for TypeMessage<&'i str, S> { +impl<L: StringLike, S> fmt::Display for TypeMessage<L, 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 a126d5b..619742e 100644 --- a/dhall/tests/macros.rs +++ b/dhall/tests/macros.rs @@ -80,10 +80,11 @@ pub enum ExpectedResult { pub fn read_dhall_file<'i>( file_path: &str, mut buffer: &'i mut String, -) -> Result<Box<Expr<'i, X, Import>>, ParseError> { +) -> Result<Box<Expr_<String, X, Import>>, ParseError> { let mut file = File::open(&file_path).unwrap(); file.read_to_string(&mut buffer).unwrap(); - parser::parse_expr(&*buffer) + let expr = parser::parse_expr(&*buffer)?; + Ok(Box::new(expr.take_ownership_of_labels())) } pub fn run_test(base_path: &str, feature: Feature, expected: ExpectedResult) { |