From 6037cb224c5e61828ba41cb3d34438ad03a71403 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 9 Mar 2019 15:46:30 +0100
Subject: Remove the pervasive Label type parameter

Closes #1
---
 dhall/src/imports.rs   |  10 ++--
 dhall/src/main.rs      |   2 +-
 dhall/src/normalize.rs |   6 +--
 dhall/src/typecheck.rs | 136 ++++++++++++++++++++-----------------------------
 dhall/tests/macros.rs  |   4 +-
 5 files changed, 65 insertions(+), 93 deletions(-)

(limited to 'dhall')

diff --git a/dhall/src/imports.rs b/dhall/src/imports.rs
index 3b8ba6d..007ed47 100644
--- a/dhall/src/imports.rs
+++ b/dhall/src/imports.rs
@@ -8,9 +8,7 @@ use std::io::Read;
 use std::path::Path;
 use std::path::PathBuf;
 
-pub fn panic_imports<S: Clone>(
-    expr: &Expr<Label, S, Import>,
-) -> Expr<Label, S, X> {
+pub fn panic_imports<S: Clone>(expr: &Expr<S, Import>) -> Expr<S, X> {
     let no_import = |i: &Import| -> X { panic!("ahhh import: {:?}", i) };
     expr.map_embed(&no_import)
 }
@@ -24,7 +22,7 @@ pub enum ImportRoot {
 fn resolve_import(
     import: &Import,
     root: &ImportRoot,
-) -> Result<Expr<Label, X, X>, DhallError> {
+) -> Result<Expr<X, X>, DhallError> {
     use self::ImportRoot::*;
     use dhall_core::FilePrefix::*;
     use dhall_core::ImportLocation::*;
@@ -71,13 +69,13 @@ impl fmt::Display for DhallError {
 pub fn load_dhall_file(
     f: &Path,
     resolve_imports: bool,
-) -> Result<Expr<Label, X, X>, DhallError> {
+) -> Result<Expr<X, X>, DhallError> {
     let mut buffer = String::new();
     File::open(f)?.read_to_string(&mut buffer)?;
     let expr = parser::parse_expr(&*buffer)?;
     let expr = if resolve_imports {
         let root = ImportRoot::LocalDir(f.parent().unwrap().to_owned());
-        let resolve = |import: &Import| -> Expr<Label, X, X> {
+        let resolve = |import: &Import| -> Expr<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 349af3d..edc6baf 100644
--- a/dhall/src/main.rs
+++ b/dhall/src/main.rs
@@ -65,7 +65,7 @@ fn main() {
         }
     };
 
-    let expr: Expr<Label, _, _> = imports::panic_imports(&expr);
+    let expr: Expr<_, _> = imports::panic_imports(&expr);
 
     let type_expr = match typecheck::type_of(&expr) {
         Err(e) => {
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 6344c52..b2ee0f6 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -12,7 +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<S, T, A>(e: &Expr<Label, S, A>) -> Expr<Label, T, A>
+pub fn normalize<S, T, A>(e: &Expr<S, A>) -> Expr<T, A>
 where
     S: Clone + fmt::Debug,
     T: Clone + fmt::Debug,
@@ -93,7 +93,7 @@ where
                     normalize(&dhall_expr!(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_expr!(cons y ys)
@@ -130,7 +130,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_expr!(just y)
                     });
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 {
diff --git a/dhall/tests/macros.rs b/dhall/tests/macros.rs
index 10c4f5c..9ed48e0 100644
--- a/dhall/tests/macros.rs
+++ b/dhall/tests/macros.rs
@@ -73,9 +73,7 @@ pub enum ExpectedResult {
     Failure,
 }
 
-pub fn read_dhall_file<'i>(
-    file_path: &str,
-) -> Result<Expr<Label, X, X>, DhallError> {
+pub fn read_dhall_file<'i>(file_path: &str) -> Result<Expr<X, X>, DhallError> {
     load_dhall_file(&PathBuf::from(file_path), true)
 }
 
-- 
cgit v1.2.3