summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-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
4 files changed, 61 insertions, 85 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 => {
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 13:31:04 +0000