summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/imports.rs6
-rw-r--r--dhall/src/lib.rs2
-rw-r--r--dhall/src/main.rs2
-rw-r--r--dhall/src/normalize.rs10
-rw-r--r--dhall/src/typecheck.rs146
-rw-r--r--dhall/tests/macros.rs2
6 files changed, 84 insertions, 84 deletions
diff --git a/dhall/src/imports.rs b/dhall/src/imports.rs
index 4240b5e..ad0ae0f 100644
--- a/dhall/src/imports.rs
+++ b/dhall/src/imports.rs
@@ -1,11 +1,11 @@
// use dhall_core::{Expr, FilePrefix, Import, ImportLocation, ImportMode, X};
-use dhall_core::{Expr_, StringLike, Import, X};
+use dhall_core::{Expr, StringLike, Import, X};
// use std::path::Path;
// use std::path::PathBuf;
pub fn resolve_imports<Label: StringLike, S: Clone>(
- expr: &Expr_<Label, S, Import>,
-) -> Expr_<Label, S, X> {
+ 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 66d132e..95f7f6f 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -44,7 +44,7 @@ pub fn load_dhall_file<'i, 'a: 'i>(
f: &Path,
source_pool: &'a mut Vec<String>,
_resolve_imports: bool,
-) -> Result<Expr_<String, 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)?;
diff --git a/dhall/src/main.rs b/dhall/src/main.rs
index b571996..23c8108 100644
--- a/dhall/src/main.rs
+++ b/dhall/src/main.rs
@@ -65,7 +65,7 @@ fn main() {
}
};
- let expr: Expr_<String, _, _> = imports::resolve_imports(&expr.take_ownership_of_labels());
+ 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/normalize.rs b/dhall/src/normalize.rs
index 4f07d9a..3b8099a 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -13,8 +13,8 @@ use std::fmt;
/// leave ill-typed sub-expressions unevaluated.
///
pub fn normalize<Label: StringLike, S, T, A>(
- e: &Expr_<Label, S, A>,
-) -> Expr_<Label, T, A>
+ e: &Expr<Label, S, A>,
+) -> Expr<Label, T, A>
where
S: Clone + fmt::Debug,
T: Clone + fmt::Debug,
@@ -22,7 +22,7 @@ where
{
use dhall_core::BinOp::*;
use dhall_core::Builtin::*;
- use dhall_core::Expr_::*;
+ use dhall_core::Expr::*;
match e {
// Matches that don't normalize everything right away
Let(f, _, r, b) => {
@@ -96,7 +96,7 @@ where
// normalize(&dhall!(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!(cons y ys)
@@ -133,7 +133,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!(just y)
});
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 1c15d88..b5bdee8 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -8,9 +8,9 @@ use dhall_core::context::Context;
use dhall_core::core;
use dhall_core::core::Builtin::*;
use dhall_core::core::Const::*;
-use dhall_core::core::Expr_::*;
+use dhall_core::core::Expr::*;
use dhall_core::core::{app, pi};
-use dhall_core::core::{bx, shift, subst, Expr, Expr_, V, X, StringLike};
+use dhall_core::core::{bx, shift, subst, Expr, V, X, StringLike};
use self::TypeMessage::*;
@@ -48,15 +48,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<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<L: StringLike, S, T>(
ctx: &mut Vec<(L, L)>,
- el: &Expr_<L, S, X>,
- er: &Expr_<L, T, X>,
+ el: &Expr<L, S, X>,
+ er: &Expr<L, T, X>,
) -> bool
where
S: Clone + ::std::fmt::Debug,
@@ -146,16 +146,16 @@ where
}
fn op2_type<Label: StringLike + From<String>, S, EF>(
- ctx: &Context<Label, Expr_<Label, S, X>>,
- e: &Expr_<Label, S, X>,
+ 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>>
+ l: &Expr<Label, S, X>,
+ r: &Expr<Label, S, X>,
+) -> Result<Expr<Label, S, X>, TypeError<Label, 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<Label, S>,
{
let tl = normalize(&type_with(ctx, l)?);
match tl {
@@ -179,14 +179,14 @@ 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<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>>
+ 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,
{
use dhall_core::BinOp::*;
- use dhall_core::Expr_;
+ use dhall_core::Expr;
match *e {
Const(c) => axiom(c).map(Const), //.map(Cow::Owned),
Var(V(ref x, n)) => {
@@ -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();
@@ -488,14 +488,14 @@ where
pi("_", app(List, "a"), app(Optional, "a")),
).take_ownership_of_labels()),
Builtin(ListIndexed) => {
- let mut m: BTreeMap<Label, Expr_<Label, _, _>> = BTreeMap::new();
+ 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));
+ 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));
+ 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)),
@@ -509,7 +509,7 @@ where
).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();
@@ -714,8 +714,8 @@ where
/// 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>(
- e: &Expr_<Label, S, X>,
-) -> Result<Expr_<Label, S, X>, TypeError<Label, S>> {
+ 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())
}
@@ -724,83 +724,83 @@ pub fn type_of<Label: StringLike + From<String>, S: Clone + ::std::fmt::Debug>(
#[derive(Debug)]
pub enum TypeMessage<Label: std::hash::Hash + Eq, S> {
UnboundVariable,
- InvalidInputType(Expr_<Label, S, X>),
- InvalidOutputType(Expr_<Label, S, X>),
- NotAFunction(Expr_<Label, S, X>, Expr_<Label, S, X>),
+ InvalidInputType(Expr<Label, S, X>),
+ InvalidOutputType(Expr<Label, S, X>),
+ NotAFunction(Expr<Label, S, X>, Expr<Label, S, X>),
TypeMismatch(
- Expr_<Label, S, X>,
- Expr_<Label, S, X>,
- Expr_<Label, S, X>,
- Expr_<Label, S, X>,
+ Expr<Label, S, X>,
+ Expr<Label, S, X>,
+ Expr<Label, S, X>,
+ Expr<Label, S, X>,
),
- AnnotMismatch(Expr_<Label, S, X>, Expr_<Label, S, X>, Expr_<Label, S, X>),
+ AnnotMismatch(Expr<Label, S, X>, Expr<Label, S, X>, Expr<Label, S, X>),
Untyped,
InvalidListElement(
usize,
- Expr_<Label, S, X>,
- Expr_<Label, S, X>,
- Expr_<Label, S, X>,
+ Expr<Label, S, X>,
+ Expr<Label, S, X>,
+ Expr<Label, S, X>,
),
- InvalidListType(Expr_<Label, S, X>),
+ InvalidListType(Expr<Label, S, X>),
InvalidOptionalElement(
- Expr_<Label, S, X>,
- Expr_<Label, S, X>,
- Expr_<Label, S, X>,
+ Expr<Label, S, X>,
+ Expr<Label, S, X>,
+ Expr<Label, S, X>,
),
InvalidOptionalLiteral(usize),
- InvalidOptionalType(Expr_<Label, S, X>),
- InvalidPredicate(Expr_<Label, S, X>, Expr_<Label, S, X>),
+ InvalidOptionalType(Expr<Label, S, X>),
+ InvalidPredicate(Expr<Label, S, X>, Expr<Label, S, X>),
IfBranchMismatch(
- Expr_<Label, S, X>,
- Expr_<Label, S, X>,
- Expr_<Label, S, X>,
- Expr_<Label, S, X>,
+ Expr<Label, S, X>,
+ Expr<Label, S, X>,
+ Expr<Label, S, X>,
+ Expr<Label, S, X>,
),
IfBranchMustBeTerm(
bool,
- Expr_<Label, S, X>,
- Expr_<Label, S, X>,
- Expr_<Label, S, X>,
+ Expr<Label, S, X>,
+ Expr<Label, S, X>,
+ Expr<Label, S, X>,
),
- InvalidField(Label, Expr_<Label, S, X>),
- InvalidFieldType(Label, Expr_<Label, S, X>),
- InvalidAlternative(Label, Expr_<Label, S, X>),
- InvalidAlternativeType(Label, Expr_<Label, S, X>),
+ 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>),
+ MustCombineARecord(Expr<Label, S, X>, Expr<Label, S, X>),
FieldCollision(Label),
- MustMergeARecord(Expr_<Label, S, X>, Expr_<Label, S, X>),
- MustMergeUnion(Expr_<Label, S, X>, Expr_<Label, S, X>),
+ MustMergeARecord(Expr<Label, S, X>, Expr<Label, S, X>),
+ MustMergeUnion(Expr<Label, S, X>, 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>),
- CantNE(Expr_<Label, S, X>, Expr_<Label, S, X>),
- CantTextAppend(Expr_<Label, S, X>, Expr_<Label, S, X>),
- CantAdd(Expr_<Label, S, X>, Expr_<Label, S, X>),
- CantMultiply(Expr_<Label, S, X>, Expr_<Label, S, X>),
- NoDependentLet(Expr_<Label, S, X>, Expr_<Label, S, X>),
- NoDependentTypes(Expr_<Label, S, X>, Expr_<Label, S, X>),
+ 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>),
+ CantNE(Expr<Label, S, X>, Expr<Label, S, X>),
+ CantTextAppend(Expr<Label, S, X>, Expr<Label, S, X>),
+ CantAdd(Expr<Label, S, X>, Expr<Label, S, X>),
+ CantMultiply(Expr<Label, S, X>, Expr<Label, S, X>),
+ NoDependentLet(Expr<Label, S, X>, Expr<Label, S, X>),
+ NoDependentTypes(Expr<Label, S, X>, Expr<Label, S, X>),
}
/// A structured type error that includes context
#[derive(Debug)]
pub struct TypeError<Label: std::hash::Hash + Eq, S> {
- pub context: Context<Label, Expr_<Label, S, X>>,
- pub current: Expr_<Label, S, X>,
+ pub context: Context<Label, Expr<Label, S, X>>,
+ pub current: Expr<Label, S, X>,
pub type_message: TypeMessage<Label, S>,
}
impl<Label: StringLike, S: Clone> TypeError<Label, S> {
pub fn new(
- context: &Context<Label, Expr_<Label, S, X>>,
- current: &Expr_<Label, S, X>,
+ context: &Context<Label, Expr<Label, S, X>>,
+ current: &Expr<Label, S, X>,
type_message: TypeMessage<Label, S>,
) -> Self {
TypeError {
diff --git a/dhall/tests/macros.rs b/dhall/tests/macros.rs
index 619742e..83510a3 100644
--- a/dhall/tests/macros.rs
+++ b/dhall/tests/macros.rs
@@ -80,7 +80,7 @@ pub enum ExpectedResult {
pub fn read_dhall_file<'i>(
file_path: &str,
mut buffer: &'i mut String,
-) -> Result<Box<Expr_<String, 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();
let expr = parser::parse_expr(&*buffer)?;
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-04 21:44:46 +0000