summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/imports.rs11
-rw-r--r--dhall/src/main.rs5
-rw-r--r--dhall/src/normalize.rs20
-rw-r--r--dhall/src/typecheck.rs110
-rw-r--r--dhall/tests/macros.rs6
-rw-r--r--dhall_core/src/core.rs119
-rw-r--r--dhall_generator/src/lib.rs16
7 files changed, 109 insertions, 178 deletions
diff --git a/dhall/src/imports.rs b/dhall/src/imports.rs
index d9f0b33..3b8ba6d 100644
--- a/dhall/src/imports.rs
+++ b/dhall/src/imports.rs
@@ -1,5 +1,5 @@
// use dhall_core::{Expr, FilePrefix, Import, ImportLocation, ImportMode, X};
-use dhall_core::{Expr, Import, StringLike, X};
+use dhall_core::{Expr, Import, X};
// use std::path::Path;
use dhall_core::*;
use std::fmt;
@@ -8,7 +8,7 @@ use std::io::Read;
use std::path::Path;
use std::path::PathBuf;
-pub fn panic_imports<Label: StringLike, S: Clone>(
+pub fn panic_imports<S: Clone>(
expr: &Expr<Label, S, Import>,
) -> Expr<Label, S, X> {
let no_import = |i: &Import| -> X { panic!("ahhh import: {:?}", i) };
@@ -24,7 +24,7 @@ pub enum ImportRoot {
fn resolve_import(
import: &Import,
root: &ImportRoot,
-) -> Result<Expr<String, X, X>, DhallError> {
+) -> Result<Expr<Label, X, X>, DhallError> {
use self::ImportRoot::*;
use dhall_core::FilePrefix::*;
use dhall_core::ImportLocation::*;
@@ -71,14 +71,13 @@ impl fmt::Display for DhallError {
pub fn load_dhall_file(
f: &Path,
resolve_imports: bool,
-) -> Result<Expr<String, X, X>, DhallError> {
+) -> Result<Expr<Label, X, X>, DhallError> {
let mut buffer = String::new();
File::open(f)?.read_to_string(&mut buffer)?;
let expr = parser::parse_expr(&*buffer)?;
- let expr = expr.map_label(&|l| String::from(l.clone()));
let expr = if resolve_imports {
let root = ImportRoot::LocalDir(f.parent().unwrap().to_owned());
- let resolve = |import: &Import| -> Expr<String, X, X> {
+ let resolve = |import: &Import| -> Expr<Label, 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 db69a46..349af3d 100644
--- a/dhall/src/main.rs
+++ b/dhall/src/main.rs
@@ -65,8 +65,7 @@ fn main() {
}
};
- let expr: Expr<Label, _, _> =
- imports::panic_imports(&expr);
+ let expr: Expr<Label, _, _> = imports::panic_imports(&expr);
let type_expr = match typecheck::type_of(&expr) {
Err(e) => {
@@ -90,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 16d670f..6344c52 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -12,9 +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<Label: StringLike, S, T, A>(
- e: &Expr<Label, S, A>,
-) -> Expr<Label, T, A>
+pub fn normalize<S, T, A>(e: &Expr<Label, S, A>) -> Expr<Label, T, A>
where
S: Clone + fmt::Debug,
T: Clone + fmt::Debug,
@@ -26,9 +24,9 @@ where
match e {
// Matches that don't normalize everything right away
Let(f, _, r, b) => {
- 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);
+ let r2 = shift::<_, S, _>(1, &V(f.clone(), 0), r);
+ let b2 = subst::<_, S, _>(&V(f.clone(), 0), &r2, b);
+ let b3 = shift::<_, T, _>(-1, &V(f.clone(), 0), &b2);
normalize(&b3)
}
BoolIf(b, t, f) => match normalize(b) {
@@ -38,16 +36,16 @@ where
},
Annot(x, _) => normalize(x),
Note(_, e) => normalize(e),
- App(f, a) => match normalize::<Label, S, T, A>(f) {
+ App(f, a) => match normalize::<S, T, A>(f) {
Lam(x, _A, b) => {
// Beta reduce
let vx0 = &V(x, 0);
- 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);
+ 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);
normalize(&b3)
}
- f2 => match (f2, normalize::<Label, S, T, A>(a)) {
+ f2 => match (f2, normalize::<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)) |
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 6e7775c..0dbb2f9 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -10,13 +10,11 @@ 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, StringLike, V, X};
+use dhall_core::core::{bx, shift, subst, Expr, Label, V, X};
use self::TypeMessage::*;
-fn axiom<Label: StringLike, S: Clone>(
- c: core::Const,
-) -> Result<core::Const, TypeError<Label, S>> {
+fn axiom<S: Clone>(c: core::Const) -> Result<core::Const, TypeError<S>> {
match c {
Type => Ok(Kind),
Kind => Err(TypeError::new(&Context::new(), &Const(Kind), Untyped)),
@@ -48,18 +46,15 @@ fn match_vars<L: Clone + Eq>(vl: &V<L>, vr: &V<L>, ctx: &[(L, L)]) -> bool {
}
}
-fn prop_equal<L: StringLike, S, T>(
- eL0: &Expr<L, S, X>,
- eR0: &Expr<L, T, X>,
-) -> bool
+fn prop_equal<S, T>(eL0: &Expr<Label, S, X>, eR0: &Expr<Label, T, X>) -> bool
where
S: Clone + ::std::fmt::Debug,
T: Clone + ::std::fmt::Debug,
{
- fn go<L: StringLike, S, T>(
- ctx: &mut Vec<(L, L)>,
- el: &Expr<L, S, X>,
- er: &Expr<L, T, X>,
+ fn go<S, T>(
+ ctx: &mut Vec<(Label, Label)>,
+ el: &Expr<Label, S, X>,
+ er: &Expr<Label, T, X>,
) -> bool
where
S: Clone + ::std::fmt::Debug,
@@ -145,20 +140,20 @@ where
}
}
let mut ctx = vec![];
- go::<L, S, T>(&mut ctx, &normalize(eL0), &normalize(eR0))
+ go::<S, T>(&mut ctx, &normalize(eL0), &normalize(eR0))
}
-fn op2_type<Label: StringLike, S, EF>(
+fn op2_type<S, EF>(
ctx: &Context<Label, Expr<Label, S, X>>,
e: &Expr<Label, S, X>,
t: core::Builtin,
ef: EF,
l: &Expr<Label, S, X>,
r: &Expr<Label, S, X>,
-) -> Result<Expr<Label, S, X>, TypeError<Label, S>>
+) -> Result<Expr<Label, S, X>, TypeError<S>>
where
S: Clone + ::std::fmt::Debug,
- EF: FnOnce(Expr<Label, S, X>, Expr<Label, S, X>) -> TypeMessage<Label, S>,
+ EF: FnOnce(Expr<Label, S, X>, Expr<Label, S, X>) -> TypeMessage<S>,
{
let tl = normalize(&type_with(ctx, l)?);
match tl {
@@ -181,10 +176,10 @@ 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<Label: StringLike, S>(
+pub fn type_with<S>(
ctx: &Context<Label, Expr<Label, S, X>>,
e: &Expr<Label, S, X>,
-) -> Result<Expr<Label, S, X>, TypeError<Label, S>>
+) -> Result<Expr<Label, S, X>, TypeError<S>>
where
S: Clone + ::std::fmt::Debug,
{
@@ -209,7 +204,7 @@ where
Ok(p)
}
Pi(ref 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,
_ => {
@@ -256,9 +251,9 @@ where
let tA2 = type_with(ctx, a)?;
if prop_equal(&tA, &tA2) {
let vx0 = &V(x, 0);
- let a2 = shift::<Label, S, S, X>(1, vx0, a);
+ let a2 = shift::<S, S, X>(1, vx0, a);
let tB2 = subst(vx0, &a2, &tB);
- let tB3 = shift::<Label, S, S, X>(-1, vx0, &tB2);
+ let tB3 = shift::<S, S, X>(-1, vx0, &tB2);
Ok(tB3)
} else {
let nf_A = normalize(&tA);
@@ -272,7 +267,7 @@ where
}
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 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
@@ -282,7 +277,7 @@ where
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 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
@@ -390,8 +385,7 @@ where
pi("zero", "natural", "natural"),
),
),
- )
- .take_ownership_of_labels()),
+ )),
Builtin(NaturalBuild) => Ok(pi(
"_",
pi(
@@ -404,14 +398,9 @@ where
),
),
Natural,
- )
- .take_ownership_of_labels()),
+ )),
Builtin(NaturalIsZero) | Builtin(NaturalEven) | Builtin(NaturalOdd) => {
- Ok(Pi(
- "_".to_owned().into(),
- bx(Natural.into()),
- bx(Bool.into()),
- ))
+ Ok(pi("_", Natural, Bool))
}
BinOp(NaturalPlus, ref l, ref r) => {
op2_type(ctx, e, Natural, CantAdd, l, r)
@@ -435,7 +424,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))),
@@ -470,8 +459,7 @@ where
),
app(List, "a"),
),
- )
- .take_ownership_of_labels()),
+ )),
Builtin(ListFold) => Ok(pi(
"a",
Const(Type),
@@ -488,18 +476,15 @@ where
),
),
),
- )
- .take_ownership_of_labels()),
+ )),
Builtin(ListLength) => {
- Ok(pi("a", Const(Type), pi("_", app(List, "a"), Natural))
- .take_ownership_of_labels())
+ Ok(pi("a", Const(Type), pi("_", app(List, "a"), Natural)))
}
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<Label, Expr<Label, _, _>> = BTreeMap::new();
m.insert("index".into(), Builtin(Natural));
@@ -510,12 +495,11 @@ where
pi("_", app(List, Var(V("a".into(), 0))), app(List, Record(m))),
))
}
- Builtin(ListReverse) => {
- Ok(
- pi("a", Const(Type), pi("_", app(List, "a"), app(List, "a")))
- .take_ownership_of_labels(),
- )
- }
+ Builtin(ListReverse) => Ok(pi(
+ "a",
+ Const(Type),
+ pi("_", app(List, "a"), app(List, "a")),
+ )),
OptionalLit(ref t, ref xs) => {
let mut iter = xs.iter();
let t: Box<Expr<_, _, _>> = match t {
@@ -526,7 +510,7 @@ where
}
};
- let s = normalize::<_, _, S, _>(&type_with(ctx, &t)?);
+ let s = normalize::<_, S, _>(&type_with(ctx, &t)?);
match s {
Const(Type) => {}
_ => {
@@ -567,16 +551,15 @@ where
),
),
),
- )
- .take_ownership_of_labels()),
+ )),
Builtin(List) | Builtin(Optional) => {
- Ok(pi("_", Const(Type), Const(Type)).take_ownership_of_labels())
+ Ok(pi("_", Const(Type), Const(Type)))
}
Builtin(Bool) | Builtin(Natural) | Builtin(Integer)
| 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) => {}
_ => {
@@ -595,7 +578,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) => {}
_ => {
@@ -723,19 +706,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<
- Label: StringLike + From<String>,
- S: Clone + ::std::fmt::Debug,
->(
+pub fn type_of<S: Clone + ::std::fmt::Debug>(
e: &Expr<Label, S, X>,
-) -> Result<Expr<Label, S, X>, TypeError<Label, S>> {
+) -> Result<Expr<Label, S, X>, TypeError<S>> {
let ctx = Context::new();
type_with(&ctx, e) //.map(|e| e.into_owned())
}
/// The specific type error
#[derive(Debug)]
-pub enum TypeMessage<Label: std::hash::Hash + Eq, S> {
+pub enum TypeMessage<S> {
UnboundVariable,
InvalidInputType(Expr<Label, S, X>),
InvalidOutputType(Expr<Label, S, X>),
@@ -804,17 +784,17 @@ pub enum TypeMessage<Label: std::hash::Hash + Eq, S> {
/// A structured type error that includes context
#[derive(Debug)]
-pub struct TypeError<Label: std::hash::Hash + Eq, S> {
+pub struct TypeError<S> {
pub context: Context<Label, Expr<Label, S, X>>,
pub current: Expr<Label, S, X>,
- pub type_message: TypeMessage<Label, S>,
+ pub type_message: TypeMessage<S>,
}
-impl<Label: StringLike, S: Clone> TypeError<Label, S> {
+impl<S: Clone> TypeError<S> {
pub fn new(
context: &Context<Label, Expr<Label, S, X>>,
current: &Expr<Label, S, X>,
- type_message: TypeMessage<Label, S>,
+ type_message: TypeMessage<S>,
) -> Self {
TypeError {
context: context.clone(),
@@ -824,7 +804,7 @@ impl<Label: StringLike, S: Clone> TypeError<Label, S> {
}
}
-impl<L: StringLike, S: fmt::Debug> ::std::error::Error for TypeMessage<L, S> {
+impl<S: fmt::Debug> ::std::error::Error for TypeMessage<S> {
fn description(&self) -> &str {
match *self {
UnboundVariable => "Unbound variable",
@@ -837,7 +817,7 @@ impl<L: StringLike, S: fmt::Debug> ::std::error::Error for TypeMessage<L, S> {
}
}
-impl<L: StringLike, S> fmt::Display for TypeMessage<L, S> {
+impl<S> fmt::Display for TypeMessage<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 5175238..10c4f5c 100644
--- a/dhall/tests/macros.rs
+++ b/dhall/tests/macros.rs
@@ -75,7 +75,7 @@ pub enum ExpectedResult {
pub fn read_dhall_file<'i>(
file_path: &str,
-) -> Result<Expr<String, X, X>, DhallError> {
+) -> Result<Expr<Label, X, X>, DhallError> {
load_dhall_file(&PathBuf::from(file_path), true)
}
@@ -104,8 +104,8 @@ pub fn run_test(base_path: &str, feature: Feature, expected: ExpectedResult) {
let expected = read_dhall_file(&expected_file_path).unwrap();
assert_eq_!(
- normalize::<_, _, X, _>(&expr),
- normalize::<_, _, X, _>(&expected)
+ normalize::<_, X, _>(&expr),
+ normalize::<_, X, _>(&expected)
);
}
_ => unimplemented!(),
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index 7bd1318..7eaf08e 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -296,67 +296,52 @@ pub enum Builtin {
TextShow,
}
-pub trait StringLike:
- Display
- + fmt::Debug
- + Clone
- + Hash
- + Ord
- + Eq
- + Into<String>
- + From<String>
- + From<&'static str>
-{
-}
-
-impl<T> StringLike for T where
- T: Display
- + fmt::Debug
- + Clone
- + Hash
- + Ord
- + Eq
- + Into<String>
- + From<String>
- + From<&'static str>
-{
-}
-
-impl<Label> From<Label> for V<Label> {
+impl From<Label> for V<Label> {
fn from(s: Label) -> Self {
V(s, 0)
}
}
+impl From<&'static str> for V<Label> {
+ 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(s.into())
+ Expr::Var(V(s, 0))
}
}
-impl<L, S, A> From<Builtin> for Expr<L, S, A> {
+impl<S, A> From<&'static str> for Expr<Label, 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> {
fn from(t: Builtin) -> Self {
Expr::Builtin(t)
}
}
-impl<Label: StringLike, S, A> Expr<Label, S, A> {
- pub fn map_shallow<T, B, Label2, F1, F2, F3, F4>(
+impl<S, A> Expr<Label, 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<Label2, T, B>
+ ) -> Expr<Label, T, B>
where
A: Clone,
T: Clone,
S: Clone,
- Label2: StringLike,
- F1: Fn(&Self) -> Expr<Label2, T, B>,
+ F1: Fn(&Self) -> Expr<Label, T, B>,
F2: FnOnce(&S) -> T,
F3: FnOnce(&A) -> B,
- F4: Fn(&Label) -> Label2,
+ F4: Fn(&Label) -> Label,
{
map_shallow(self, map_expr, map_note, map_embed, map_label)
}
@@ -373,15 +358,13 @@ impl<Label: StringLike, S, A> Expr<Label, S, A> {
self.map_shallow(recurse, |x| x.clone(), map_embed, |x| x.clone())
}
- pub fn map_label<L2: StringLike, F>(&self, map_label: &F) -> Expr<L2, S, A>
+ pub fn map_label<F>(&self, map_label: &F) -> Self
where
A: Clone,
S: Clone,
- F: Fn(&Label) -> L2,
+ F: Fn(&Label) -> Label,
{
- let recurse = |e: &Expr<Label, S, A>| -> Expr<L2, S, A> {
- e.map_label(map_label)
- };
+ let recurse = |e: &Self| -> Self { e.map_label(map_label) };
self.map_shallow(recurse, |x| x.clone(), |x| x.clone(), map_label)
}
@@ -407,25 +390,8 @@ impl<Label: StringLike, S, A> Expr<Label, S, A> {
}
}
-impl<S: Clone, A: Clone> Expr<&'static str, S, A> {
- pub fn take_ownership_of_labels<L: StringLike>(
- &self,
- ) -> Expr<L, S, A> {
- let recurse = |e: &Expr<&'static str, S, A>| -> Expr<L, S, A> {
- e.take_ownership_of_labels()
- };
- map_shallow(
- self,
- recurse,
- |x| x.clone(),
- |x| x.clone(),
- |x: &&str| -> L { (*x).to_owned().into() },
- )
- }
-}
-
-impl<L: StringLike, S: Clone, A: Clone> Expr<L, S, Expr<L, S, A>> {
- pub fn squash_embed(&self) -> Expr<L, S, A> {
+impl<S: Clone, A: Clone> Expr<Label, S, Expr<Label, S, A>> {
+ pub fn squash_embed(&self) -> Expr<Label, S, A> {
match self {
Expr::Embed(e) => e.clone(),
e => e.map_shallow(
@@ -771,11 +737,7 @@ impl<Label: Display> Display for V<Label> {
}
}
-pub fn pi<Label, 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<Label, S, A>
where
Name: Into<Label>,
Et: Into<Expr<Label, S, A>>,
@@ -820,28 +782,25 @@ fn add_ui(u: usize, i: isize) -> usize {
}
}
-pub fn map_shallow<Label1, Label2, S, T, A, B, F1, F2, F3, F4>(
- e: &Expr<Label1, S, A>,
+pub fn map_shallow<S, T, A, B, F1, F2, F3, F4>(
+ e: &Expr<Label, S, A>,
map: F1,
map_note: F2,
map_embed: F3,
map_label: F4,
-) -> Expr<Label2, T, B>
+) -> Expr<Label, T, B>
where
A: Clone,
S: Clone,
T: Clone,
- Label1:
- Display + fmt::Debug + Clone + Hash + Ord + Eq + Into<String>,
- Label2: StringLike,
- F1: Fn(&Expr<Label1, S, A>) -> Expr<Label2, T, B>,
+ F1: Fn(&Expr<Label, S, A>) -> Expr<Label, T, B>,
F2: FnOnce(&S) -> T,
F3: FnOnce(&A) -> B,
- F4: Fn(&Label1) -> Label2,
+ F4: Fn(&Label) -> Label,
{
use crate::Expr::*;
let bxmap =
- |x: &Expr<Label1, S, A>| -> Box<Expr<Label2, T, B>> { bx(map(x)) };
+ |x: &Expr<Label, S, A>| -> Box<Expr<Label, T, B>> { bx(map(x)) };
let opt = |x| map_opt_box(x, &map);
match *e {
Const(k) => Const(k),
@@ -1000,14 +959,11 @@ 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<Label, S, T, A: Clone>(
+pub fn shift<S, T, A: Clone>(
d: isize,
v: &V<Label>,
e: &Expr<Label, S, A>,
-) -> Expr<Label, T, A>
-where
- Label: StringLike,
-{
+) -> Expr<Label, T, A> {
use crate::Expr::*;
let V(x, n) = v;
match e {
@@ -1080,7 +1036,7 @@ where
}
}
-fn shift_op2<Label, S, T, A, F>(
+fn shift_op2<S, T, A, F>(
f: F,
d: isize,
v: &V<Label>,
@@ -1093,7 +1049,6 @@ where
Box<Expr<Label, T, A>>,
) -> Expr<Label, T, A>,
A: Clone,
- Label: StringLike,
{
map_op2(f, |x| bx(shift(d, v, x)), a, b)
}
@@ -1104,7 +1059,7 @@ where
/// subst x C B ~ B[x := C]
/// ```
///
-pub fn subst<Label: StringLike, S, T, A>(
+pub fn subst<S, T, A>(
v: &V<Label>,
e: &Expr<Label, S, A>,
b: &Expr<Label, T, A>,
@@ -1193,7 +1148,7 @@ where
}
}
-fn subst_op2<Label: StringLike, S, T, A, F>(
+fn subst_op2<S, T, A, F>(
f: F,
v: &V<Label>,
e: &Expr<Label, S, A>,
diff --git a/dhall_generator/src/lib.rs b/dhall_generator/src/lib.rs
index e66ab2c..f633544 100644
--- a/dhall_generator/src/lib.rs
+++ b/dhall_generator/src/lib.rs
@@ -12,15 +12,15 @@ pub fn dhall_expr(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
let no_import =
|_: &Import| -> X { panic!("Don't use import in dhall!()") };
let expr = expr.map_embed(&no_import);
- let output = dhall_to_tokenstream::<Label>(&expr, &Context::new());
+ let output = dhall_to_tokenstream(&expr, &Context::new());
output.into()
}
// 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: StringLike>(
- expr: &Expr<L, X, X>,
- ctx: &Context<L, ()>,
+fn dhall_to_tokenstream(
+ expr: &Expr<Label, X, X>,
+ ctx: &Context<Label, ()>,
) -> TokenStream {
use dhall_core::Expr::*;
match expr {
@@ -31,7 +31,7 @@ fn dhall_to_tokenstream<L: StringLike>(
Lam(x, t, b) => {
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());
+ let x = Literal::string(&String::from(x.clone()));
quote! { Lam(#x.into(), #t, #b) }
}
App(f, a) => {
@@ -74,9 +74,9 @@ fn dhall_to_tokenstream<L: StringLike>(
}
// Returns an expression of type Box<Expr<_, _>>
-fn dhall_to_tokenstream_bx<L: StringLike>(
- expr: &Expr<L, X, X>,
- ctx: &Context<L, ()>,
+fn dhall_to_tokenstream_bx(
+ expr: &Expr<Label, X, X>,
+ ctx: &Context<Label, ()>,
) -> TokenStream {
use dhall_core::Expr::*;
match expr {
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 17:15:34 +0000