summaryrefslogtreecommitdiff
path: root/dhall/src/typecheck.rs
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/typecheck.rs136
1 files changed, 56 insertions, 80 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 0dbb2f9..28982fc 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -29,8 +29,8 @@ fn rule(a: core::Const, b: core::Const) -> Result<core::Const, ()> {
}
}
-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();
+fn match_vars(vl: &V, vr: &V, ctx: &[(Label, Label)]) -> bool {
+ let xxs: Option<(&(Label, Label), &[(Label, Label)])> = 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), _)))
@@ -46,15 +46,15 @@ fn match_vars<L: Clone + Eq>(vl: &V<L>, vr: &V<L>, ctx: &[(L, L)]) -> bool {
}
}
-fn prop_equal<S, T>(eL0: &Expr<Label, S, X>, eR0: &Expr<Label, T, X>) -> bool
+fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool
where
S: Clone + ::std::fmt::Debug,
T: Clone + ::std::fmt::Debug,
{
fn go<S, T>(
ctx: &mut Vec<(Label, Label)>,
- el: &Expr<Label, S, X>,
- er: &Expr<Label, T, X>,
+ el: &Expr<S, X>,
+ er: &Expr<T, X>,
) -> bool
where
S: Clone + ::std::fmt::Debug,
@@ -144,16 +144,16 @@ where
}
fn op2_type<S, EF>(
- ctx: &Context<Label, Expr<Label, S, X>>,
- e: &Expr<Label, S, X>,
+ ctx: &Context<Label, Expr<S, X>>,
+ e: &Expr<S, X>,
t: core::Builtin,
ef: EF,
- l: &Expr<Label, S, X>,
- r: &Expr<Label, S, X>,
-) -> Result<Expr<Label, S, X>, TypeError<S>>
+ l: &Expr<S, X>,
+ r: &Expr<S, X>,
+) -> Result<Expr<S, X>, TypeError<S>>
where
S: Clone + ::std::fmt::Debug,
- EF: FnOnce(Expr<Label, S, X>, Expr<Label, S, X>) -> TypeMessage<S>,
+ EF: FnOnce(Expr<S, X>, Expr<S, X>) -> TypeMessage<S>,
{
let tl = normalize(&type_with(ctx, l)?);
match tl {
@@ -177,9 +177,9 @@ 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<S>(
- ctx: &Context<Label, Expr<Label, S, X>>,
- e: &Expr<Label, S, X>,
-) -> Result<Expr<Label, S, X>, TypeError<S>>
+ ctx: &Context<Label, Expr<S, X>>,
+ e: &Expr<S, X>,
+) -> Result<Expr<S, X>, TypeError<S>>
where
S: Clone + ::std::fmt::Debug,
{
@@ -416,7 +416,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();
@@ -486,7 +486,7 @@ where
pi("_", app(List, "a"), app(Optional, "a")),
)),
Builtin(ListIndexed) => {
- let mut m: BTreeMap<Label, Expr<Label, _, _>> = BTreeMap::new();
+ let mut m: BTreeMap<Label, Expr<_, _>> = BTreeMap::new();
m.insert("index".into(), Builtin(Natural));
m.insert("value".into(), Var(V("a".into(), 0)));
Ok(pi(
@@ -502,7 +502,7 @@ where
)),
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();
@@ -707,8 +707,8 @@ where
/// expression must be closed (i.e. no free variables), otherwise type-checking
/// will fail.
pub fn type_of<S: Clone + ::std::fmt::Debug>(
- e: &Expr<Label, S, X>,
-) -> Result<Expr<Label, S, X>, TypeError<S>> {
+ e: &Expr<S, X>,
+) -> Result<Expr<S, X>, TypeError<S>> {
let ctx = Context::new();
type_with(&ctx, e) //.map(|e| e.into_owned())
}
@@ -717,83 +717,59 @@ pub fn type_of<S: Clone + ::std::fmt::Debug>(
#[derive(Debug)]
pub enum TypeMessage<S> {
UnboundVariable,
- 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>,
- ),
- AnnotMismatch(Expr<Label, S, X>, Expr<Label, S, X>, Expr<Label, S, X>),
+ InvalidInputType(Expr<S, X>),
+ InvalidOutputType(Expr<S, X>),
+ NotAFunction(Expr<S, X>, Expr<S, X>),
+ TypeMismatch(Expr<S, X>, Expr<S, X>, Expr<S, X>, Expr<S, X>),
+ AnnotMismatch(Expr<S, X>, Expr<S, X>, Expr<S, X>),
Untyped,
- InvalidListElement(
- usize,
- Expr<Label, S, X>,
- Expr<Label, S, X>,
- Expr<Label, S, X>,
- ),
- InvalidListType(Expr<Label, S, X>),
- InvalidOptionalElement(
- Expr<Label, S, X>,
- Expr<Label, S, X>,
- Expr<Label, S, X>,
- ),
+ InvalidListElement(usize, Expr<S, X>, Expr<S, X>, Expr<S, X>),
+ InvalidListType(Expr<S, X>),
+ InvalidOptionalElement(Expr<S, X>, Expr<S, X>, Expr<S, X>),
InvalidOptionalLiteral(usize),
- 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>,
- ),
- IfBranchMustBeTerm(
- bool,
- 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>),
+ InvalidOptionalType(Expr<S, X>),
+ InvalidPredicate(Expr<S, X>, Expr<S, X>),
+ IfBranchMismatch(Expr<S, X>, Expr<S, X>, Expr<S, X>, Expr<S, X>),
+ IfBranchMustBeTerm(bool, Expr<S, X>, Expr<S, X>, Expr<S, X>),
+ InvalidField(Label, Expr<S, X>),
+ InvalidFieldType(Label, Expr<S, X>),
+ InvalidAlternative(Label, Expr<S, X>),
+ InvalidAlternativeType(Label, Expr<S, X>),
DuplicateAlternative(Label),
- MustCombineARecord(Expr<Label, S, X>, Expr<Label, S, X>),
+ MustCombineARecord(Expr<S, X>, Expr<S, X>),
FieldCollision(Label),
- MustMergeARecord(Expr<Label, S, X>, Expr<Label, S, X>),
- MustMergeUnion(Expr<Label, S, X>, Expr<Label, S, X>),
+ MustMergeARecord(Expr<S, X>, Expr<S, X>),
+ MustMergeUnion(Expr<S, X>, Expr<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<S, X>, Expr<S, X>),
+ HandlerOutputTypeMismatch(Label, Expr<S, X>, Expr<S, X>),
+ HandlerNotAFunction(Label, Expr<S, X>),
+ NotARecord(Label, Expr<S, X>, Expr<S, X>),
+ MissingField(Label, Expr<S, X>),
+ CantAnd(Expr<S, X>, Expr<S, X>),
+ CantOr(Expr<S, X>, Expr<S, X>),
+ CantEQ(Expr<S, X>, Expr<S, X>),
+ CantNE(Expr<S, X>, Expr<S, X>),
+ CantTextAppend(Expr<S, X>, Expr<S, X>),
+ CantAdd(Expr<S, X>, Expr<S, X>),
+ CantMultiply(Expr<S, X>, Expr<S, X>),
+ NoDependentLet(Expr<S, X>, Expr<S, X>),
+ NoDependentTypes(Expr<S, X>, Expr<S, X>),
}
/// A structured type error that includes context
#[derive(Debug)]
pub struct TypeError<S> {
- pub context: Context<Label, Expr<Label, S, X>>,
- pub current: Expr<Label, S, X>,
+ pub context: Context<Label, Expr<S, X>>,
+ pub current: Expr<S, X>,
pub type_message: TypeMessage<S>,
}
impl<S: Clone> TypeError<S> {
pub fn new(
- context: &Context<Label, Expr<Label, S, X>>,
- current: &Expr<Label, S, X>,
+ context: &Context<Label, Expr<S, X>>,
+ current: &Expr<S, X>,
type_message: TypeMessage<S>,
) -> Self {
TypeError {
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 22:39:24 +0000