From 4c159640e5ee77ffa48b85a5bffa56350cf933ef Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 4 May 2019 17:59:05 +0200
Subject: Make SubExpr generic in the variable labels type

---
 dhall_syntax/src/core.rs    | 207 ++++++++++++++++++++++++--------------------
 dhall_syntax/src/parser.rs  |  24 +++--
 dhall_syntax/src/printer.rs |  44 ++++++----
 dhall_syntax/src/visitor.rs | 130 ++++++++++++++--------------
 4 files changed, 218 insertions(+), 187 deletions(-)

(limited to 'dhall_syntax')

diff --git a/dhall_syntax/src/core.rs b/dhall_syntax/src/core.rs
index a186d19..c8a2425 100644
--- a/dhall_syntax/src/core.rs
+++ b/dhall_syntax/src/core.rs
@@ -60,19 +60,7 @@ pub enum Const {
 /// The `Int` field is a DeBruijn index.
 /// See dhall-lang/standard/semantics.md for details
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub struct V<Label>(pub Label, pub usize);
-
-// This is only for the specific `Label` type, not generic
-impl From<Label> for V<Label> {
-    fn from(x: Label) -> V<Label> {
-        V(x, 0)
-    }
-}
-impl<'a> From<&'a Label> for V<Label> {
-    fn from(x: &'a Label) -> V<Label> {
-        V(x.clone(), 0)
-    }
-}
+pub struct Var<Label>(pub Label, pub usize);
 
 // Definition order must match precedence order for
 // pretty-printing to work correctly
@@ -137,44 +125,52 @@ pub enum Builtin {
     TextShow,
 }
 
-pub type ParsedExpr = SubExpr<X, Import>;
-pub type ResolvedExpr = SubExpr<X, X>;
+pub type ParsedExpr = SubExpr<Label, X, Import>;
+pub type ResolvedExpr = SubExpr<Label, X, X>;
 pub type DhallExpr = ResolvedExpr;
 
 // Each node carries an annotation. In practice it's either X (no annotation) or a Span.
 #[derive(Debug)]
-pub struct SubExpr<Note, Embed>(Rc<(Expr<Note, Embed>, Option<Note>)>);
+pub struct SubExpr<VarLabel, Note, Embed>(
+    Rc<(Expr<VarLabel, Note, Embed>, Option<Note>)>,
+);
 
-impl<Note, Embed: PartialEq> std::cmp::PartialEq for SubExpr<Note, Embed> {
+impl<VarLabel: PartialEq, Note, Embed: PartialEq> std::cmp::PartialEq
+    for SubExpr<VarLabel, Note, Embed>
+{
     fn eq(&self, other: &Self) -> bool {
         self.0.as_ref().0 == other.0.as_ref().0
     }
 }
 
-impl<Note, Embed: Eq> std::cmp::Eq for SubExpr<Note, Embed> {}
+impl<VarLabel: Eq, Note, Embed: Eq> std::cmp::Eq
+    for SubExpr<VarLabel, Note, Embed>
+{
+}
 
-pub type Expr<Note, Embed> = ExprF<SubExpr<Note, Embed>, Label, Embed>;
+pub type Expr<VarLabel, Note, Embed> =
+    ExprF<SubExpr<VarLabel, Note, Embed>, VarLabel, Embed>;
 
 /// Syntax tree for expressions
 // Having the recursion out of the enum definition enables writing
 // much more generic code and improves pattern-matching behind
 // smart pointers.
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub enum ExprF<SubExpr, Label, Embed> {
+pub enum ExprF<SubExpr, VarLabel, Embed> {
     Const(Const),
     ///  `x`
     ///  `x@n`
-    Var(V<Label>),
+    Var(Var<VarLabel>),
     ///  `λ(x : A) -> b`
-    Lam(Label, SubExpr, SubExpr),
+    Lam(VarLabel, SubExpr, SubExpr),
     ///  `A -> B`
     ///  `∀(x : A) -> B`
-    Pi(Label, SubExpr, SubExpr),
+    Pi(VarLabel, SubExpr, SubExpr),
     ///  `f a`
     App(SubExpr, SubExpr),
     ///  `let x     = r in e`
     ///  `let x : t = r in e`
-    Let(Label, Option<SubExpr>, SubExpr, SubExpr),
+    Let(VarLabel, Option<SubExpr>, SubExpr, SubExpr),
     ///  `x : t`
     Annot(SubExpr, SubExpr),
     /// Built-in values
@@ -235,11 +231,7 @@ impl<SE, L, E> ExprF<SE, L, E> {
         visit_under_binder: impl FnOnce(&'a L, &'a SE) -> Result<SE2, Err>,
         visit_embed: impl FnOnce(&'a E) -> Result<E2, Err>,
         visit_label: impl FnMut(&'a L) -> Result<L2, Err>,
-    ) -> Result<ExprF<SE2, L2, E2>, Err>
-    where
-        L: Ord,
-        L2: Ord,
-    {
+    ) -> Result<ExprF<SE2, L2, E2>, Err> {
         self.visit(visitor::TraverseRefWithBindersVisitor {
             visit_subexpr,
             visit_under_binder,
@@ -253,11 +245,7 @@ impl<SE, L, E> ExprF<SE, L, E> {
         visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>,
         visit_embed: impl FnOnce(&'a E) -> Result<E2, Err>,
         visit_label: impl FnMut(&'a L) -> Result<L2, Err>,
-    ) -> Result<ExprF<SE2, L2, E2>, Err>
-    where
-        L: Ord,
-        L2: Ord,
-    {
+    ) -> Result<ExprF<SE2, L2, E2>, Err> {
         self.visit(visitor::TraverseRefVisitor {
             visit_subexpr,
             visit_embed,
@@ -271,11 +259,7 @@ impl<SE, L, E> ExprF<SE, L, E> {
         mut map_under_binder: impl FnMut(&'a L, &'a SE) -> SE2,
         map_embed: impl FnOnce(&'a E) -> E2,
         mut map_label: impl FnMut(&'a L) -> L2,
-    ) -> ExprF<SE2, L2, E2>
-    where
-        L: Ord,
-        L2: Ord,
-    {
+    ) -> ExprF<SE2, L2, E2> {
         trivial_result(self.traverse_ref_with_special_handling_of_binders(
             |x| Ok(map_subexpr(x)),
             |l, x| Ok(map_under_binder(l, x)),
@@ -289,11 +273,7 @@ impl<SE, L, E> ExprF<SE, L, E> {
         mut map_subexpr: impl FnMut(&'a SE) -> SE2,
         map_embed: impl FnOnce(&'a E) -> E2,
         mut map_label: impl FnMut(&'a L) -> L2,
-    ) -> ExprF<SE2, L2, E2>
-    where
-        L: Ord,
-        L2: Ord,
-    {
+    ) -> ExprF<SE2, L2, E2> {
         trivial_result(self.traverse_ref(
             |x| Ok(map_subexpr(x)),
             |x| Ok(map_embed(x)),
@@ -306,7 +286,7 @@ impl<SE, L, E> ExprF<SE, L, E> {
         visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>,
     ) -> Result<ExprF<SE2, L, E>, Err>
     where
-        L: Ord + Clone,
+        L: Clone,
         E: Clone,
     {
         self.traverse_ref(
@@ -321,26 +301,31 @@ impl<SE, L, E> ExprF<SE, L, E> {
         map_subexpr: impl Fn(&'a SE) -> SE2,
     ) -> ExprF<SE2, L, E>
     where
-        L: Ord + Clone,
+        L: Clone,
         E: Clone,
     {
         self.map_ref(map_subexpr, E::clone, L::clone)
     }
 }
 
-impl<N, E> Expr<N, E> {
+impl<L, N, E> Expr<L, N, E> {
     fn traverse_embed<E2, Err>(
         &self,
         visit_embed: impl FnMut(&E) -> Result<E2, Err>,
-    ) -> Result<Expr<N, E2>, Err>
+    ) -> Result<Expr<L, N, E2>, Err>
     where
+        L: Clone,
         N: Clone,
     {
         self.visit(&mut visitor::TraverseEmbedVisitor(visit_embed))
     }
 
-    fn map_embed<E2>(&self, mut map_embed: impl FnMut(&E) -> E2) -> Expr<N, E2>
+    fn map_embed<E2>(
+        &self,
+        mut map_embed: impl FnMut(&E) -> E2,
+    ) -> Expr<L, N, E2>
     where
+        L: Clone,
         N: Clone,
     {
         trivial_result(self.traverse_embed(|x| Ok(map_embed(x))))
@@ -348,52 +333,52 @@ impl<N, E> Expr<N, E> {
 
     pub fn squash_embed<E2>(
         &self,
-        f: impl FnMut(&E) -> SubExpr<N, E2>,
-    ) -> SubExpr<N, E2>
+        f: impl FnMut(&E) -> SubExpr<L, N, E2>,
+    ) -> SubExpr<L, N, E2>
     where
+        L: Clone,
         N: Clone,
     {
         trivial_result(self.visit(&mut visitor::SquashEmbedVisitor(f)))
     }
 }
 
-impl<E: Clone> Expr<X, E> {
-    pub fn note_absurd<N>(&self) -> Expr<N, E> {
+impl<L: Clone, E: Clone> Expr<L, X, E> {
+    pub fn note_absurd<N>(&self) -> Expr<L, N, E> {
         self.visit(&mut visitor::NoteAbsurdVisitor)
     }
 }
 
-impl<N: Clone> Expr<N, X> {
-    pub fn embed_absurd<E>(&self) -> Expr<N, E> {
+impl<L: Clone, N: Clone> Expr<L, N, X> {
+    pub fn embed_absurd<E>(&self) -> Expr<L, N, E> {
         self.visit(&mut visitor::EmbedAbsurdVisitor)
     }
 }
 
-impl<N, E> SubExpr<N, E> {
-    pub fn as_ref(&self) -> &Expr<N, E> {
+impl<V, N, E> SubExpr<V, N, E> {
+    pub fn as_ref(&self) -> &Expr<V, N, E> {
         &self.0.as_ref().0
     }
 
-    pub fn new(x: Expr<N, E>, n: N) -> Self {
+    pub fn new(x: Expr<V, N, E>, n: N) -> Self {
         SubExpr(Rc::new((x, Some(n))))
     }
 
-    pub fn from_expr_no_note(x: Expr<N, E>) -> Self {
+    pub fn from_expr_no_note(x: Expr<V, N, E>) -> Self {
         SubExpr(Rc::new((x, None)))
     }
 
-    pub fn unnote(&self) -> SubExpr<X, E>
+    pub fn unnote(&self) -> SubExpr<V, X, E>
     where
+        V: Clone,
         E: Clone,
     {
         SubExpr::from_expr_no_note(
             self.as_ref().visit(&mut visitor::UnNoteVisitor),
         )
     }
-}
 
-impl<N: Clone, E> SubExpr<N, E> {
-    pub fn rewrap<E2>(&self, x: Expr<N, E2>) -> SubExpr<N, E2>
+    pub fn rewrap<E2>(&self, x: Expr<V, N, E2>) -> SubExpr<V, N, E2>
     where
         N: Clone,
     {
@@ -403,8 +388,9 @@ impl<N: Clone, E> SubExpr<N, E> {
     pub fn traverse_embed<E2, Err>(
         &self,
         visit_embed: impl FnMut(&E) -> Result<E2, Err>,
-    ) -> Result<SubExpr<N, E2>, Err>
+    ) -> Result<SubExpr<V, N, E2>, Err>
     where
+        V: Clone,
         N: Clone,
     {
         Ok(self.rewrap(self.as_ref().traverse_embed(visit_embed)?))
@@ -413,8 +399,9 @@ impl<N: Clone, E> SubExpr<N, E> {
     pub fn map_embed<E2>(
         &self,
         map_embed: impl FnMut(&E) -> E2,
-    ) -> SubExpr<N, E2>
+    ) -> SubExpr<V, N, E2>
     where
+        V: Clone,
         N: Clone,
     {
         self.rewrap(self.as_ref().map_embed(map_embed))
@@ -423,8 +410,12 @@ impl<N: Clone, E> SubExpr<N, E> {
     pub fn map_subexprs_with_special_handling_of_binders<'a>(
         &'a self,
         map_expr: impl FnMut(&'a Self) -> Self,
-        map_under_binder: impl FnMut(&'a Label, &'a Self) -> Self,
-    ) -> Self {
+        map_under_binder: impl FnMut(&'a V, &'a Self) -> Self,
+    ) -> Self
+    where
+        V: Clone,
+        N: Clone,
+    {
         match self.as_ref() {
             ExprF::Embed(_) => SubExpr::clone(self),
             // This calls ExprF::map_ref
@@ -432,7 +423,7 @@ impl<N: Clone, E> SubExpr<N, E> {
                 map_expr,
                 map_under_binder,
                 |_| unreachable!(),
-                Label::clone,
+                V::clone,
             )),
         }
     }
@@ -441,26 +432,34 @@ impl<N: Clone, E> SubExpr<N, E> {
     /// capture by shifting variable indices
     /// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift
     /// for details
-    pub fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+    pub fn shift(&self, delta: isize, var: &Var<V>) -> Self
+    where
+        V: Clone + PartialEq,
+        N: Clone,
+    {
         match self.as_ref() {
             ExprF::Var(v) => self.rewrap(ExprF::Var(v.shift(delta, var))),
             _ => self.map_subexprs_with_special_handling_of_binders(
                 |e| e.shift(delta, var),
-                |x: &Label, e| e.shift(delta, &var.shift(1, &x.into())),
+                |x: &V, e| e.shift(delta, &var.shift(1, &Var::new(x.clone()))),
             ),
         }
     }
 
-    pub fn subst_shift(&self, var: &V<Label>, val: &Self) -> Self {
+    pub fn subst_shift(&self, var: &Var<V>, val: &Self) -> Self
+    where
+        V: Clone + PartialEq,
+        N: Clone,
+    {
         match self.as_ref() {
             ExprF::Var(v) if v == var => val.clone(),
             ExprF::Var(v) => self.rewrap(ExprF::Var(v.shift(-1, var))),
             _ => self.map_subexprs_with_special_handling_of_binders(
                 |e| e.subst_shift(var, val),
-                |x: &Label, e| {
+                |x: &V, e| {
                     e.subst_shift(
-                        &var.shift(1, &x.into()),
-                        &val.shift(1, &x.into()),
+                        &var.shift(1, &Var::new(x.clone())),
+                        &val.shift(1, &Var::new(x.clone())),
                     )
                 },
             ),
@@ -468,26 +467,26 @@ impl<N: Clone, E> SubExpr<N, E> {
     }
 }
 
-impl<N: Clone> SubExpr<N, X> {
-    pub fn embed_absurd<T>(&self) -> SubExpr<N, T> {
+impl<L: Clone, N: Clone> SubExpr<L, N, X> {
+    pub fn embed_absurd<T>(&self) -> SubExpr<L, N, T> {
         self.rewrap(self.as_ref().embed_absurd())
     }
 }
 
-impl<E: Clone> SubExpr<X, E> {
-    pub fn note_absurd<N>(&self) -> SubExpr<N, E> {
+impl<L: Clone, E: Clone> SubExpr<L, X, E> {
+    pub fn note_absurd<N>(&self) -> SubExpr<L, N, E> {
         SubExpr::from_expr_no_note(self.as_ref().note_absurd())
     }
 }
 
-impl<N, E> Clone for SubExpr<N, E> {
+impl<L, N, E> Clone for SubExpr<L, N, E> {
     fn clone(&self) -> Self {
         SubExpr(Rc::clone(&self.0))
     }
 }
 
 // Should probably rename this
-pub fn rc<E>(x: Expr<X, E>) -> SubExpr<X, E> {
+pub fn rc<L, E>(x: Expr<L, X, E>) -> SubExpr<L, X, E> {
     SubExpr::from_expr_no_note(x)
 }
 
@@ -501,18 +500,35 @@ fn add_ui(u: usize, i: isize) -> usize {
     }
 }
 
-impl<Label: PartialEq + Clone> V<Label> {
-    pub fn shift(&self, delta: isize, var: &V<Label>) -> Self {
-        let V(x, n) = var;
-        let V(y, m) = self;
+impl<L> Var<L> {
+    fn new(x: L) -> Self {
+        Var(x, 0)
+    }
+}
+impl<L: PartialEq + Clone> Var<L> {
+    pub fn shift(&self, delta: isize, var: &Var<L>) -> Self {
+        let Var(x, n) = var;
+        let Var(y, m) = self;
         if x == y && n <= m {
-            V(y.clone(), add_ui(*m, delta))
+            Var(y.clone(), add_ui(*m, delta))
         } else {
-            V(y.clone(), *m)
+            Var(y.clone(), *m)
         }
     }
 }
 
+// This is only for the specific `Label` type, not generic
+impl From<Label> for Var<Label> {
+    fn from(x: Label) -> Var<Label> {
+        Var(x, 0)
+    }
+}
+impl<'a> From<&'a Label> for Var<Label> {
+    fn from(x: &'a Label) -> Var<Label> {
+        Var(x.clone(), 0)
+    }
+}
+
 /// `shift` is used by both normalization and type-checking to avoid variable
 /// capture by shifting variable indices
 /// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift
@@ -520,9 +536,9 @@ impl<Label: PartialEq + Clone> V<Label> {
 ///
 pub fn shift<N, E>(
     delta: isize,
-    var: &V<Label>,
-    in_expr: &SubExpr<N, E>,
-) -> SubExpr<N, E>
+    var: &Var<Label>,
+    in_expr: &SubExpr<Label, N, E>,
+) -> SubExpr<Label, N, E>
 where
     N: Clone,
 {
@@ -531,8 +547,8 @@ where
 
 pub fn shift0_multiple<N, E>(
     deltas: &HashMap<Label, isize>,
-    in_expr: &SubExpr<N, E>,
-) -> SubExpr<N, E>
+    in_expr: &SubExpr<Label, N, E>,
+) -> SubExpr<Label, N, E>
 where
     N: Clone,
 {
@@ -542,16 +558,15 @@ where
 fn shift0_multiple_inner<N, E>(
     ctx: &Context<Label, ()>,
     deltas: &HashMap<Label, isize>,
-    in_expr: &SubExpr<N, E>,
-) -> SubExpr<N, E>
+    in_expr: &SubExpr<Label, N, E>,
+) -> SubExpr<Label, N, E>
 where
     N: Clone,
 {
-    use crate::ExprF::*;
     match in_expr.as_ref() {
-        Var(V(y, m)) if ctx.lookup(y, *m).is_none() => {
+        ExprF::Var(Var(y, m)) if ctx.lookup(y, *m).is_none() => {
             let delta = deltas.get(y).unwrap_or(&0);
-            in_expr.rewrap(Var(V(y.clone(), add_ui(*m, *delta))))
+            in_expr.rewrap(ExprF::Var(Var(y.clone(), add_ui(*m, *delta))))
         }
         _ => in_expr.map_subexprs_with_special_handling_of_binders(
             |e| shift0_multiple_inner(ctx, deltas, e),
diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index 83ccc1e..bdef553 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -8,7 +8,13 @@ use std::rc::Rc;
 
 use dhall_generated_parser::{DhallParser, Rule};
 
-use crate::ExprF::*;
+use crate::ExprF::{
+    Annot, App, BinOp, BoolIf, BoolLit, Builtin, Const, DoubleLit, Embed,
+    EmptyListLit, Field, IntegerLit, Lam, Let, Merge, NEListLit, NaturalLit,
+    OldOptionalLit, Pi, Projection, RecordLit, RecordType, SomeLit, TextLit,
+    UnionLit, UnionType,
+};
+
 use crate::*;
 
 // This file consumes the parse tree generated by pest and turns it into
@@ -16,10 +22,10 @@ use crate::*;
 // their own crate because they are quite general and useful. For now they
 // are here and hopefully you can figure out how they work.
 
-type ParsedExpr = Expr<Span, Import>;
-type ParsedSubExpr = SubExpr<Span, Import>;
-type ParsedText = InterpolatedText<SubExpr<Span, Import>>;
-type ParsedTextContents = InterpolatedTextContents<SubExpr<Span, Import>>;
+type ParsedExpr = Expr<Label, Span, Import>;
+type ParsedSubExpr = SubExpr<Label, Span, Import>;
+type ParsedText = InterpolatedText<ParsedSubExpr>;
+type ParsedTextContents = InterpolatedTextContents<ParsedSubExpr>;
 
 pub type ParseError = pest::error::Error<Rule>;
 
@@ -504,17 +510,17 @@ make_parser! {
 
     rule!(identifier<ParsedSubExpr> as expression; span; children!(
         [variable(v)] => {
-            spanned(span, Var(v))
+            spanned(span, ExprF::Var(v))
         },
         [builtin(e)] => e,
     ));
 
-    rule!(variable<V<Label>>; children!(
+    rule!(variable<Var<Label>>; children!(
         [label(l), natural_literal(idx)] => {
-            V(l, idx)
+            Var(l, idx)
         },
         [label(l)] => {
-            V(l, 0)
+            Var(l, 0)
         },
     ));
 
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index e3b180b..9cc1b46 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -3,7 +3,9 @@ use itertools::Itertools;
 use std::fmt::{self, Display};
 
 /// Generic instance that delegates to subexpressions
-impl<SE: Display + Clone, E: Display> Display for ExprF<SE, Label, E> {
+impl<SE: Display + Clone, L: Display + Clone, E: Display> Display
+    for ExprF<SE, L, E>
+{
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         use crate::ExprF::*;
         match self {
@@ -13,9 +15,10 @@ impl<SE: Display + Clone, E: Display> Display for ExprF<SE, Label, E> {
             BoolIf(a, b, c) => {
                 write!(f, "if {} then {} else {}", a, b, c)?;
             }
-            Pi(a, b, c) if &String::from(a) == "_" => {
-                write!(f, "{} → {}", b, c)?;
-            }
+            // TODO: arrow type
+            // Pi(a, b, c) if &String::from(a) == "_" => {
+            //     write!(f, "{} → {}", b, c)?;
+            // }
             Pi(a, b, c) => {
                 write!(f, "∀({} : {}) → {}", a, b, c)?;
             }
@@ -124,21 +127,25 @@ enum PrintPhase {
 // Wraps an Expr with a phase, so that phase selsction can be done
 // separate from the actual printing
 #[derive(Clone)]
-struct PhasedExpr<'a, S, A>(&'a SubExpr<S, A>, PrintPhase);
+struct PhasedExpr<'a, L, S, A>(&'a SubExpr<L, S, A>, PrintPhase);
 
-impl<'a, S: Clone, A: Display + Clone> Display for PhasedExpr<'a, S, A> {
+impl<'a, L: Display + Clone, S: Clone, A: Display + Clone> Display
+    for PhasedExpr<'a, L, S, A>
+{
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         self.0.as_ref().fmt_phase(f, self.1)
     }
 }
 
-impl<'a, S: Clone, A: Display + Clone> PhasedExpr<'a, S, A> {
-    fn phase(self, phase: PrintPhase) -> PhasedExpr<'a, S, A> {
+impl<'a, L: Display + Clone, S: Clone, A: Display + Clone>
+    PhasedExpr<'a, L, S, A>
+{
+    fn phase(self, phase: PrintPhase) -> PhasedExpr<'a, L, S, A> {
         PhasedExpr(self.0, phase)
     }
 }
 
-impl<S: Clone, A: Display + Clone> Expr<S, A> {
+impl<L: Display + Clone, S: Clone, A: Display + Clone> Expr<L, S, A> {
     fn fmt_phase(
         &self,
         f: &mut fmt::Formatter,
@@ -172,11 +179,12 @@ impl<S: Clone, A: Display + Clone> Expr<S, A> {
         // Annotate subexpressions with the appropriate phase, defaulting to Base
         let phased_self = match self.map_ref_simple(|e| PhasedExpr(e, Base)) {
             Pi(a, b, c) => {
-                if &String::from(&a) == "_" {
-                    Pi(a, b.phase(Operator), c)
-                } else {
-                    Pi(a, b, c)
-                }
+                // TODO: arrow type
+                // if &String::from(&a) == "_" {
+                //     Pi(a, b.phase(Operator), c)
+                // } else {
+                Pi(a, b, c)
+                // }
             }
             Merge(a, b, c) => Merge(
                 a.phase(Import),
@@ -212,7 +220,9 @@ impl<S: Clone, A: Display + Clone> Expr<S, A> {
     }
 }
 
-impl<S: Clone, A: Display + Clone> Display for SubExpr<S, A> {
+impl<L: Display + Clone, S: Clone, A: Display + Clone> Display
+    for SubExpr<L, S, A>
+{
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         self.as_ref().fmt_phase(f, PrintPhase::Base)
     }
@@ -474,9 +484,9 @@ impl Display for Scheme {
     }
 }
 
-impl<Label: Display> Display for V<Label> {
+impl<Label: Display> Display for Var<Label> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
-        let V(x, n) = self;
+        let Var(x, n) = self;
         x.fmt(f)?;
         if *n != 0 {
             write!(f, "@{}", n)?;
diff --git a/dhall_syntax/src/visitor.rs b/dhall_syntax/src/visitor.rs
index 7fdf217..a8e5a8c 100644
--- a/dhall_syntax/src/visitor.rs
+++ b/dhall_syntax/src/visitor.rs
@@ -48,8 +48,6 @@ pub trait ExprFVeryGenericVisitor<'a, Ret, SE1, L1, E1>: Sized {
 impl<'a, T, Ret, SE1, L1, E1>
     GenericVisitor<&'a ExprF<SE1, L1, E1>, Result<Ret, T::Error>> for T
 where
-    L1: Ord,
-    T::L2: Ord,
     T: ExprFVeryGenericVisitor<'a, Ret, SE1, L1, E1>,
 {
     fn visit(self, input: &'a ExprF<SE1, L1, E1>) -> Result<Ret, T::Error> {
@@ -69,31 +67,27 @@ where
             })
         }
         fn btmap<'a, V, Ret, SE, L, E>(
-            x: &'a BTreeMap<L, SE>,
+            x: &'a BTreeMap<Label, SE>,
             mut v: V,
-        ) -> Result<BTreeMap<V::L2, V::SE2>, V::Error>
+        ) -> Result<BTreeMap<Label, V::SE2>, V::Error>
         where
-            L: Ord,
-            V::L2: Ord,
             V: ExprFVeryGenericVisitor<'a, Ret, SE, L, E>,
         {
             x.iter()
-                .map(|(k, x)| Ok((v.visit_label(k)?, v.visit_subexpr(x)?)))
+                .map(|(k, x)| Ok((k.clone(), v.visit_subexpr(x)?)))
                 .collect()
         }
         fn btoptmap<'a, V, Ret, SE, L, E>(
-            x: &'a BTreeMap<L, Option<SE>>,
+            x: &'a BTreeMap<Label, Option<SE>>,
             mut v: V,
-        ) -> Result<BTreeMap<V::L2, Option<V::SE2>>, V::Error>
+        ) -> Result<BTreeMap<Label, Option<V::SE2>>, V::Error>
         where
-            L: Ord,
-            V::L2: Ord,
             V: ExprFVeryGenericVisitor<'a, Ret, SE, L, E>,
         {
             x.iter()
                 .map(|(k, x)| {
                     Ok((
-                        v.visit_label(k)?,
+                        k.clone(),
                         match x {
                             Some(x) => Some(v.visit_subexpr(x)?),
                             None => None,
@@ -104,9 +98,14 @@ where
         }
 
         let mut v = self;
-        use crate::ExprF::*;
+        use crate::ExprF::{
+            Annot, App, BinOp, BoolIf, BoolLit, Builtin, Const, DoubleLit,
+            Embed, EmptyListLit, Field, IntegerLit, Lam, Let, Merge, NEListLit,
+            NaturalLit, OldOptionalLit, Pi, Projection, RecordLit, RecordType,
+            SomeLit, TextLit, UnionLit, UnionType,
+        };
         T::visit_resulting_exprf(match input {
-            Var(V(l, n)) => Var(V(v.visit_label(l)?, *n)),
+            ExprF::Var(Var(l, n)) => ExprF::Var(Var(v.visit_label(l)?, *n)),
             Lam(l, t, e) => {
                 let t = v.visit_subexpr(t)?;
                 let (l, e) = v.visit_binder(l, e)?;
@@ -150,20 +149,16 @@ where
             RecordType(kts) => RecordType(btmap(kts, v)?),
             RecordLit(kvs) => RecordLit(btmap(kvs, v)?),
             UnionType(kts) => UnionType(btoptmap(kts, v)?),
-            UnionLit(k, x, kts) => UnionLit(
-                v.visit_label(k)?,
-                v.visit_subexpr(x)?,
-                btoptmap(kts, v)?,
-            ),
+            UnionLit(l, x, kts) => {
+                UnionLit(l.clone(), v.visit_subexpr(x)?, btoptmap(kts, v)?)
+            }
             Merge(x, y, t) => Merge(
                 v.visit_subexpr(x)?,
                 v.visit_subexpr(y)?,
                 opt(t, |e| v.visit_subexpr(e))?,
             ),
-            Field(e, l) => Field(v.visit_subexpr(e)?, v.visit_label(l)?),
-            Projection(e, ls) => {
-                Projection(v.visit_subexpr(e)?, vec(ls, |l| v.visit_label(l))?)
-            }
+            Field(e, l) => Field(v.visit_subexpr(e)?, l.clone()),
+            Projection(e, ls) => Projection(v.visit_subexpr(e)?, ls.clone()),
             Embed(a) => return v.visit_embed_squash(a),
         })
     }
@@ -314,8 +309,6 @@ where
 impl<'a, T, SE1, SE2, L1, L2, E1, E2>
     GenericVisitor<&'a ExprF<SE1, L1, E1>, ExprF<SE2, L2, E2>> for T
 where
-    L1: Ord,
-    L2: Ord,
     T: ExprFInFallibleVisitor<'a, SE1, SE2, L1, L2, E1, E2>,
 {
     fn visit(self, input: &'a ExprF<SE1, L1, E1>) -> ExprF<SE2, L2, E2> {
@@ -337,8 +330,6 @@ where
     SE: 'a,
     L: 'a,
     E: 'a,
-    L: Ord,
-    L2: Ord,
     F1: FnMut(&'a SE) -> Result<SE2, Err>,
     F2: FnOnce(&'a L, &'a SE) -> Result<SE2, Err>,
     F4: FnOnce(&'a E) -> Result<E2, Err>,
@@ -377,8 +368,6 @@ where
     SE: 'a,
     L: 'a,
     E: 'a,
-    L: Ord,
-    L2: Ord,
     F1: FnMut(&'a SE) -> Result<SE2, Err>,
     F3: FnOnce(&'a E) -> Result<E2, Err>,
     F4: FnMut(&'a L) -> Result<L2, Err>,
@@ -398,10 +387,11 @@ where
 
 pub struct TraverseEmbedVisitor<F1>(pub F1);
 
-impl<'a, 'b, N, E, E2, Err, F1>
-    ExprFFallibleVisitor<'a, SubExpr<N, E>, SubExpr<N, E2>, Label, Label, E, E2>
+impl<'a, 'b, L, N, E, E2, Err, F1>
+    ExprFFallibleVisitor<'a, SubExpr<L, N, E>, SubExpr<L, N, E2>, L, L, E, E2>
     for &'b mut TraverseEmbedVisitor<F1>
 where
+    L: Clone + 'a,
     N: Clone + 'a,
     F1: FnMut(&E) -> Result<E2, Err>,
 {
@@ -409,50 +399,48 @@ where
 
     fn visit_subexpr(
         &mut self,
-        subexpr: &'a SubExpr<N, E>,
-    ) -> Result<SubExpr<N, E2>, Self::Error> {
+        subexpr: &'a SubExpr<L, N, E>,
+    ) -> Result<SubExpr<L, N, E2>, Self::Error> {
         Ok(subexpr.rewrap(subexpr.as_ref().visit(&mut **self)?))
     }
     fn visit_embed(self, embed: &'a E) -> Result<E2, Self::Error> {
         (self.0)(embed)
     }
-    fn visit_label(&mut self, label: &'a Label) -> Result<Label, Self::Error> {
-        Ok(Label::clone(label))
+    fn visit_label(&mut self, label: &'a L) -> Result<L, Self::Error> {
+        Ok(L::clone(label))
     }
 }
 
 pub struct SquashEmbedVisitor<F1>(pub F1);
 
-impl<'a, 'b, N, E1, E2, F1>
-    ExprFVeryGenericVisitor<'a, SubExpr<N, E2>, SubExpr<N, E1>, Label, E1>
+impl<'a, 'b, L, N, E1, E2, F1>
+    ExprFVeryGenericVisitor<'a, SubExpr<L, N, E2>, SubExpr<L, N, E1>, L, E1>
     for &'b mut SquashEmbedVisitor<F1>
 where
+    L: Clone + 'a,
     N: Clone + 'a,
-    F1: FnMut(&E1) -> SubExpr<N, E2>,
+    F1: FnMut(&E1) -> SubExpr<L, N, E2>,
 {
     type Error = X;
-    type SE2 = SubExpr<N, E2>;
-    type L2 = Label;
+    type SE2 = SubExpr<L, N, E2>;
+    type L2 = L;
     type E2 = E2;
 
     fn visit_subexpr(
         &mut self,
-        subexpr: &'a SubExpr<N, E1>,
+        subexpr: &'a SubExpr<L, N, E1>,
     ) -> Result<Self::SE2, Self::Error> {
         Ok(subexpr.as_ref().visit(&mut **self)?)
     }
 
-    fn visit_label(
-        &mut self,
-        label: &'a Label,
-    ) -> Result<Self::L2, Self::Error> {
-        Ok(Label::clone(label))
+    fn visit_label(&mut self, label: &'a L) -> Result<Self::L2, Self::Error> {
+        Ok(L::clone(label))
     }
 
     fn visit_binder(
         mut self,
-        label: &'a Label,
-        subexpr: &'a SubExpr<N, E1>,
+        label: &'a L,
+        subexpr: &'a SubExpr<L, N, E1>,
     ) -> Result<(Self::L2, Self::SE2), Self::Error> {
         Ok((self.visit_label(label)?, self.visit_subexpr(subexpr)?))
     }
@@ -460,7 +448,7 @@ where
     fn visit_embed_squash(
         self,
         embed: &'a E1,
-    ) -> Result<SubExpr<N, E2>, Self::Error> {
+    ) -> Result<SubExpr<L, N, E2>, Self::Error> {
         Ok((self.0)(embed))
     }
 
@@ -468,7 +456,7 @@ where
     // Useful to change the result type, and/or avoid some loss of info
     fn visit_resulting_exprf(
         result: ExprF<Self::SE2, Self::L2, Self::E2>,
-    ) -> Result<SubExpr<N, E2>, Self::Error> {
+    ) -> Result<SubExpr<L, N, E2>, Self::Error> {
         // TODO: don't lose note
         Ok(SubExpr::from_expr_no_note(result))
     }
@@ -476,57 +464,69 @@ where
 
 pub struct UnNoteVisitor;
 
-impl<'a, 'b, N, E>
-    ExprFInFallibleVisitor<'a, SubExpr<N, E>, SubExpr<X, E>, Label, Label, E, E>
+impl<'a, 'b, L, N, E>
+    ExprFInFallibleVisitor<'a, SubExpr<L, N, E>, SubExpr<L, X, E>, L, L, E, E>
     for &'b mut UnNoteVisitor
 where
+    L: Clone + 'a,
     E: Clone + 'a,
 {
-    fn visit_subexpr(&mut self, subexpr: &'a SubExpr<N, E>) -> SubExpr<X, E> {
+    fn visit_subexpr(
+        &mut self,
+        subexpr: &'a SubExpr<L, N, E>,
+    ) -> SubExpr<L, X, E> {
         SubExpr::from_expr_no_note(subexpr.as_ref().visit(&mut **self))
     }
     fn visit_embed(self, embed: &'a E) -> E {
         E::clone(embed)
     }
-    fn visit_label(&mut self, label: &'a Label) -> Label {
-        Label::clone(label)
+    fn visit_label(&mut self, label: &'a L) -> L {
+        L::clone(label)
     }
 }
 
 pub struct NoteAbsurdVisitor;
 
-impl<'a, 'b, N, E>
-    ExprFInFallibleVisitor<'a, SubExpr<X, E>, SubExpr<N, E>, Label, Label, E, E>
+impl<'a, 'b, L, N, E>
+    ExprFInFallibleVisitor<'a, SubExpr<L, X, E>, SubExpr<L, N, E>, L, L, E, E>
     for &'b mut NoteAbsurdVisitor
 where
+    L: Clone + 'a,
     E: Clone + 'a,
 {
-    fn visit_subexpr(&mut self, subexpr: &'a SubExpr<X, E>) -> SubExpr<N, E> {
+    fn visit_subexpr(
+        &mut self,
+        subexpr: &'a SubExpr<L, X, E>,
+    ) -> SubExpr<L, N, E> {
         SubExpr::from_expr_no_note(subexpr.as_ref().visit(&mut **self))
     }
     fn visit_embed(self, embed: &'a E) -> E {
         E::clone(embed)
     }
-    fn visit_label(&mut self, label: &'a Label) -> Label {
-        Label::clone(label)
+    fn visit_label(&mut self, label: &'a L) -> L {
+        L::clone(label)
     }
 }
 
 pub struct EmbedAbsurdVisitor;
 
-impl<'a, 'b, N, E>
-    ExprFInFallibleVisitor<'a, SubExpr<N, X>, SubExpr<N, E>, Label, Label, X, E>
+impl<'a, 'b, L, N, E>
+    ExprFInFallibleVisitor<'a, SubExpr<L, N, X>, SubExpr<L, N, E>, L, L, X, E>
     for &'b mut EmbedAbsurdVisitor
 where
+    L: Clone + 'a,
     N: Clone + 'a,
 {
-    fn visit_subexpr(&mut self, subexpr: &'a SubExpr<N, X>) -> SubExpr<N, E> {
+    fn visit_subexpr(
+        &mut self,
+        subexpr: &'a SubExpr<L, N, X>,
+    ) -> SubExpr<L, N, E> {
         subexpr.rewrap(subexpr.as_ref().visit(&mut **self))
     }
     fn visit_embed(self, embed: &'a X) -> E {
         match *embed {}
     }
-    fn visit_label(&mut self, label: &'a Label) -> Label {
-        Label::clone(label)
+    fn visit_label(&mut self, label: &'a L) -> L {
+        L::clone(label)
     }
 }
-- 
cgit v1.2.3


From 153cf8dab3b80aba30ac3adfd44e4be251494ea2 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 4 May 2019 18:37:15 +0200
Subject: Recover arrow type detection

---
 dhall_syntax/src/core.rs    | 15 ++++++++++++-
 dhall_syntax/src/printer.rs | 51 +++++++++++++++++++++++++++++----------------
 2 files changed, 47 insertions(+), 19 deletions(-)

(limited to 'dhall_syntax')

diff --git a/dhall_syntax/src/core.rs b/dhall_syntax/src/core.rs
index c8a2425..389f037 100644
--- a/dhall_syntax/src/core.rs
+++ b/dhall_syntax/src/core.rs
@@ -60,7 +60,7 @@ pub enum Const {
 /// The `Int` field is a DeBruijn index.
 /// See dhall-lang/standard/semantics.md for details
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub struct Var<Label>(pub Label, pub usize);
+pub struct Var<VarLabel>(pub VarLabel, pub usize);
 
 // Definition order must match precedence order for
 // pretty-printing to work correctly
@@ -529,6 +529,19 @@ impl<'a> From<&'a Label> for Var<Label> {
     }
 }
 
+/// Trait for things that capture a label used for variables.
+/// Allows normalization to be generic in whether to alpha-normalize or not.
+pub trait VarLabel: std::fmt::Display + Clone {
+    /// Is `self` the default variable (i.e. "_") ?
+    fn is_underscore_var(&self) -> bool;
+}
+
+impl VarLabel for Label {
+    fn is_underscore_var(&self) -> bool {
+        &String::from(self) == "_"
+    }
+}
+
 /// `shift` is used by both normalization and type-checking to avoid variable
 /// capture by shifting variable indices
 /// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index 9cc1b46..6ebd537 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -3,8 +3,11 @@ use itertools::Itertools;
 use std::fmt::{self, Display};
 
 /// Generic instance that delegates to subexpressions
-impl<SE: Display + Clone, L: Display + Clone, E: Display> Display
-    for ExprF<SE, L, E>
+impl<SE, L, E> Display for ExprF<SE, L, E>
+where
+    SE: Display + Clone,
+    L: VarLabel,
+    E: Display,
 {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         use crate::ExprF::*;
@@ -15,10 +18,9 @@ impl<SE: Display + Clone, L: Display + Clone, E: Display> Display
             BoolIf(a, b, c) => {
                 write!(f, "if {} then {} else {}", a, b, c)?;
             }
-            // TODO: arrow type
-            // Pi(a, b, c) if &String::from(a) == "_" => {
-            //     write!(f, "{} → {}", b, c)?;
-            // }
+            Pi(a, b, c) if a.is_underscore_var() => {
+                write!(f, "{} → {}", b, c)?;
+            }
             Pi(a, b, c) => {
                 write!(f, "∀({} : {}) → {}", a, b, c)?;
             }
@@ -129,23 +131,34 @@ enum PrintPhase {
 #[derive(Clone)]
 struct PhasedExpr<'a, L, S, A>(&'a SubExpr<L, S, A>, PrintPhase);
 
-impl<'a, L: Display + Clone, S: Clone, A: Display + Clone> Display
-    for PhasedExpr<'a, L, S, A>
+impl<'a, L, S, A> Display for PhasedExpr<'a, L, S, A>
+where
+    L: VarLabel,
+    S: Clone,
+    A: Display + Clone,
 {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         self.0.as_ref().fmt_phase(f, self.1)
     }
 }
 
-impl<'a, L: Display + Clone, S: Clone, A: Display + Clone>
-    PhasedExpr<'a, L, S, A>
+impl<'a, L, S, A> PhasedExpr<'a, L, S, A>
+where
+    L: VarLabel,
+    S: Clone,
+    A: Display + Clone,
 {
     fn phase(self, phase: PrintPhase) -> PhasedExpr<'a, L, S, A> {
         PhasedExpr(self.0, phase)
     }
 }
 
-impl<L: Display + Clone, S: Clone, A: Display + Clone> Expr<L, S, A> {
+impl<L, S, A> Expr<L, S, A>
+where
+    L: VarLabel,
+    S: Clone,
+    A: Display + Clone,
+{
     fn fmt_phase(
         &self,
         f: &mut fmt::Formatter,
@@ -179,12 +192,11 @@ impl<L: Display + Clone, S: Clone, A: Display + Clone> Expr<L, S, A> {
         // Annotate subexpressions with the appropriate phase, defaulting to Base
         let phased_self = match self.map_ref_simple(|e| PhasedExpr(e, Base)) {
             Pi(a, b, c) => {
-                // TODO: arrow type
-                // if &String::from(&a) == "_" {
-                //     Pi(a, b.phase(Operator), c)
-                // } else {
+                if a.is_underscore_var() {
+                    Pi(a, b.phase(Operator), c)
+                } else {
                 Pi(a, b, c)
-                // }
+                }
             }
             Merge(a, b, c) => Merge(
                 a.phase(Import),
@@ -220,8 +232,11 @@ impl<L: Display + Clone, S: Clone, A: Display + Clone> Expr<L, S, A> {
     }
 }
 
-impl<L: Display + Clone, S: Clone, A: Display + Clone> Display
-    for SubExpr<L, S, A>
+impl<L, S, A> Display for SubExpr<L, S, A>
+where
+    L: VarLabel,
+    S: Clone,
+    A: Display + Clone,
 {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         self.as_ref().fmt_phase(f, PrintPhase::Base)
-- 
cgit v1.2.3


From 6ad7a2000bf32b96be731cd51da5b841976dae12 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 4 May 2019 18:41:21 +0200
Subject: Revert "Recover arrow type detection"

This reverts commit 153cf8dab3b80aba30ac3adfd44e4be251494ea2.
---
 dhall_syntax/src/core.rs    | 15 +------------
 dhall_syntax/src/printer.rs | 51 ++++++++++++++++-----------------------------
 2 files changed, 19 insertions(+), 47 deletions(-)

(limited to 'dhall_syntax')

diff --git a/dhall_syntax/src/core.rs b/dhall_syntax/src/core.rs
index 389f037..c8a2425 100644
--- a/dhall_syntax/src/core.rs
+++ b/dhall_syntax/src/core.rs
@@ -60,7 +60,7 @@ pub enum Const {
 /// The `Int` field is a DeBruijn index.
 /// See dhall-lang/standard/semantics.md for details
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub struct Var<VarLabel>(pub VarLabel, pub usize);
+pub struct Var<Label>(pub Label, pub usize);
 
 // Definition order must match precedence order for
 // pretty-printing to work correctly
@@ -529,19 +529,6 @@ impl<'a> From<&'a Label> for Var<Label> {
     }
 }
 
-/// Trait for things that capture a label used for variables.
-/// Allows normalization to be generic in whether to alpha-normalize or not.
-pub trait VarLabel: std::fmt::Display + Clone {
-    /// Is `self` the default variable (i.e. "_") ?
-    fn is_underscore_var(&self) -> bool;
-}
-
-impl VarLabel for Label {
-    fn is_underscore_var(&self) -> bool {
-        &String::from(self) == "_"
-    }
-}
-
 /// `shift` is used by both normalization and type-checking to avoid variable
 /// capture by shifting variable indices
 /// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index 6ebd537..9cc1b46 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -3,11 +3,8 @@ use itertools::Itertools;
 use std::fmt::{self, Display};
 
 /// Generic instance that delegates to subexpressions
-impl<SE, L, E> Display for ExprF<SE, L, E>
-where
-    SE: Display + Clone,
-    L: VarLabel,
-    E: Display,
+impl<SE: Display + Clone, L: Display + Clone, E: Display> Display
+    for ExprF<SE, L, E>
 {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         use crate::ExprF::*;
@@ -18,9 +15,10 @@ where
             BoolIf(a, b, c) => {
                 write!(f, "if {} then {} else {}", a, b, c)?;
             }
-            Pi(a, b, c) if a.is_underscore_var() => {
-                write!(f, "{} → {}", b, c)?;
-            }
+            // TODO: arrow type
+            // Pi(a, b, c) if &String::from(a) == "_" => {
+            //     write!(f, "{} → {}", b, c)?;
+            // }
             Pi(a, b, c) => {
                 write!(f, "∀({} : {}) → {}", a, b, c)?;
             }
@@ -131,34 +129,23 @@ enum PrintPhase {
 #[derive(Clone)]
 struct PhasedExpr<'a, L, S, A>(&'a SubExpr<L, S, A>, PrintPhase);
 
-impl<'a, L, S, A> Display for PhasedExpr<'a, L, S, A>
-where
-    L: VarLabel,
-    S: Clone,
-    A: Display + Clone,
+impl<'a, L: Display + Clone, S: Clone, A: Display + Clone> Display
+    for PhasedExpr<'a, L, S, A>
 {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         self.0.as_ref().fmt_phase(f, self.1)
     }
 }
 
-impl<'a, L, S, A> PhasedExpr<'a, L, S, A>
-where
-    L: VarLabel,
-    S: Clone,
-    A: Display + Clone,
+impl<'a, L: Display + Clone, S: Clone, A: Display + Clone>
+    PhasedExpr<'a, L, S, A>
 {
     fn phase(self, phase: PrintPhase) -> PhasedExpr<'a, L, S, A> {
         PhasedExpr(self.0, phase)
     }
 }
 
-impl<L, S, A> Expr<L, S, A>
-where
-    L: VarLabel,
-    S: Clone,
-    A: Display + Clone,
-{
+impl<L: Display + Clone, S: Clone, A: Display + Clone> Expr<L, S, A> {
     fn fmt_phase(
         &self,
         f: &mut fmt::Formatter,
@@ -192,11 +179,12 @@ where
         // Annotate subexpressions with the appropriate phase, defaulting to Base
         let phased_self = match self.map_ref_simple(|e| PhasedExpr(e, Base)) {
             Pi(a, b, c) => {
-                if a.is_underscore_var() {
-                    Pi(a, b.phase(Operator), c)
-                } else {
+                // TODO: arrow type
+                // if &String::from(&a) == "_" {
+                //     Pi(a, b.phase(Operator), c)
+                // } else {
                 Pi(a, b, c)
-                }
+                // }
             }
             Merge(a, b, c) => Merge(
                 a.phase(Import),
@@ -232,11 +220,8 @@ where
     }
 }
 
-impl<L, S, A> Display for SubExpr<L, S, A>
-where
-    L: VarLabel,
-    S: Clone,
-    A: Display + Clone,
+impl<L: Display + Clone, S: Clone, A: Display + Clone> Display
+    for SubExpr<L, S, A>
 {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         self.as_ref().fmt_phase(f, PrintPhase::Base)
-- 
cgit v1.2.3


From ab100be616932dab22a5309df86107b66e93db37 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 4 May 2019 18:41:22 +0200
Subject: Revert "Make SubExpr generic in the variable labels type"

This reverts commit 4c159640e5ee77ffa48b85a5bffa56350cf933ef.
---
 dhall_syntax/src/core.rs    | 207 ++++++++++++++++++++------------------------
 dhall_syntax/src/parser.rs  |  24 ++---
 dhall_syntax/src/printer.rs |  44 ++++------
 dhall_syntax/src/visitor.rs | 130 ++++++++++++++--------------
 4 files changed, 187 insertions(+), 218 deletions(-)

(limited to 'dhall_syntax')

diff --git a/dhall_syntax/src/core.rs b/dhall_syntax/src/core.rs
index c8a2425..a186d19 100644
--- a/dhall_syntax/src/core.rs
+++ b/dhall_syntax/src/core.rs
@@ -60,7 +60,19 @@ pub enum Const {
 /// The `Int` field is a DeBruijn index.
 /// See dhall-lang/standard/semantics.md for details
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub struct Var<Label>(pub Label, pub usize);
+pub struct V<Label>(pub Label, pub usize);
+
+// This is only for the specific `Label` type, not generic
+impl From<Label> for V<Label> {
+    fn from(x: Label) -> V<Label> {
+        V(x, 0)
+    }
+}
+impl<'a> From<&'a Label> for V<Label> {
+    fn from(x: &'a Label) -> V<Label> {
+        V(x.clone(), 0)
+    }
+}
 
 // Definition order must match precedence order for
 // pretty-printing to work correctly
@@ -125,52 +137,44 @@ pub enum Builtin {
     TextShow,
 }
 
-pub type ParsedExpr = SubExpr<Label, X, Import>;
-pub type ResolvedExpr = SubExpr<Label, X, X>;
+pub type ParsedExpr = SubExpr<X, Import>;
+pub type ResolvedExpr = SubExpr<X, X>;
 pub type DhallExpr = ResolvedExpr;
 
 // Each node carries an annotation. In practice it's either X (no annotation) or a Span.
 #[derive(Debug)]
-pub struct SubExpr<VarLabel, Note, Embed>(
-    Rc<(Expr<VarLabel, Note, Embed>, Option<Note>)>,
-);
+pub struct SubExpr<Note, Embed>(Rc<(Expr<Note, Embed>, Option<Note>)>);
 
-impl<VarLabel: PartialEq, Note, Embed: PartialEq> std::cmp::PartialEq
-    for SubExpr<VarLabel, Note, Embed>
-{
+impl<Note, Embed: PartialEq> std::cmp::PartialEq for SubExpr<Note, Embed> {
     fn eq(&self, other: &Self) -> bool {
         self.0.as_ref().0 == other.0.as_ref().0
     }
 }
 
-impl<VarLabel: Eq, Note, Embed: Eq> std::cmp::Eq
-    for SubExpr<VarLabel, Note, Embed>
-{
-}
+impl<Note, Embed: Eq> std::cmp::Eq for SubExpr<Note, Embed> {}
 
-pub type Expr<VarLabel, Note, Embed> =
-    ExprF<SubExpr<VarLabel, Note, Embed>, VarLabel, Embed>;
+pub type Expr<Note, Embed> = ExprF<SubExpr<Note, Embed>, Label, Embed>;
 
 /// Syntax tree for expressions
 // Having the recursion out of the enum definition enables writing
 // much more generic code and improves pattern-matching behind
 // smart pointers.
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub enum ExprF<SubExpr, VarLabel, Embed> {
+pub enum ExprF<SubExpr, Label, Embed> {
     Const(Const),
     ///  `x`
     ///  `x@n`
-    Var(Var<VarLabel>),
+    Var(V<Label>),
     ///  `λ(x : A) -> b`
-    Lam(VarLabel, SubExpr, SubExpr),
+    Lam(Label, SubExpr, SubExpr),
     ///  `A -> B`
     ///  `∀(x : A) -> B`
-    Pi(VarLabel, SubExpr, SubExpr),
+    Pi(Label, SubExpr, SubExpr),
     ///  `f a`
     App(SubExpr, SubExpr),
     ///  `let x     = r in e`
     ///  `let x : t = r in e`
-    Let(VarLabel, Option<SubExpr>, SubExpr, SubExpr),
+    Let(Label, Option<SubExpr>, SubExpr, SubExpr),
     ///  `x : t`
     Annot(SubExpr, SubExpr),
     /// Built-in values
@@ -231,7 +235,11 @@ impl<SE, L, E> ExprF<SE, L, E> {
         visit_under_binder: impl FnOnce(&'a L, &'a SE) -> Result<SE2, Err>,
         visit_embed: impl FnOnce(&'a E) -> Result<E2, Err>,
         visit_label: impl FnMut(&'a L) -> Result<L2, Err>,
-    ) -> Result<ExprF<SE2, L2, E2>, Err> {
+    ) -> Result<ExprF<SE2, L2, E2>, Err>
+    where
+        L: Ord,
+        L2: Ord,
+    {
         self.visit(visitor::TraverseRefWithBindersVisitor {
             visit_subexpr,
             visit_under_binder,
@@ -245,7 +253,11 @@ impl<SE, L, E> ExprF<SE, L, E> {
         visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>,
         visit_embed: impl FnOnce(&'a E) -> Result<E2, Err>,
         visit_label: impl FnMut(&'a L) -> Result<L2, Err>,
-    ) -> Result<ExprF<SE2, L2, E2>, Err> {
+    ) -> Result<ExprF<SE2, L2, E2>, Err>
+    where
+        L: Ord,
+        L2: Ord,
+    {
         self.visit(visitor::TraverseRefVisitor {
             visit_subexpr,
             visit_embed,
@@ -259,7 +271,11 @@ impl<SE, L, E> ExprF<SE, L, E> {
         mut map_under_binder: impl FnMut(&'a L, &'a SE) -> SE2,
         map_embed: impl FnOnce(&'a E) -> E2,
         mut map_label: impl FnMut(&'a L) -> L2,
-    ) -> ExprF<SE2, L2, E2> {
+    ) -> ExprF<SE2, L2, E2>
+    where
+        L: Ord,
+        L2: Ord,
+    {
         trivial_result(self.traverse_ref_with_special_handling_of_binders(
             |x| Ok(map_subexpr(x)),
             |l, x| Ok(map_under_binder(l, x)),
@@ -273,7 +289,11 @@ impl<SE, L, E> ExprF<SE, L, E> {
         mut map_subexpr: impl FnMut(&'a SE) -> SE2,
         map_embed: impl FnOnce(&'a E) -> E2,
         mut map_label: impl FnMut(&'a L) -> L2,
-    ) -> ExprF<SE2, L2, E2> {
+    ) -> ExprF<SE2, L2, E2>
+    where
+        L: Ord,
+        L2: Ord,
+    {
         trivial_result(self.traverse_ref(
             |x| Ok(map_subexpr(x)),
             |x| Ok(map_embed(x)),
@@ -286,7 +306,7 @@ impl<SE, L, E> ExprF<SE, L, E> {
         visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>,
     ) -> Result<ExprF<SE2, L, E>, Err>
     where
-        L: Clone,
+        L: Ord + Clone,
         E: Clone,
     {
         self.traverse_ref(
@@ -301,31 +321,26 @@ impl<SE, L, E> ExprF<SE, L, E> {
         map_subexpr: impl Fn(&'a SE) -> SE2,
     ) -> ExprF<SE2, L, E>
     where
-        L: Clone,
+        L: Ord + Clone,
         E: Clone,
     {
         self.map_ref(map_subexpr, E::clone, L::clone)
     }
 }
 
-impl<L, N, E> Expr<L, N, E> {
+impl<N, E> Expr<N, E> {
     fn traverse_embed<E2, Err>(
         &self,
         visit_embed: impl FnMut(&E) -> Result<E2, Err>,
-    ) -> Result<Expr<L, N, E2>, Err>
+    ) -> Result<Expr<N, E2>, Err>
     where
-        L: Clone,
         N: Clone,
     {
         self.visit(&mut visitor::TraverseEmbedVisitor(visit_embed))
     }
 
-    fn map_embed<E2>(
-        &self,
-        mut map_embed: impl FnMut(&E) -> E2,
-    ) -> Expr<L, N, E2>
+    fn map_embed<E2>(&self, mut map_embed: impl FnMut(&E) -> E2) -> Expr<N, E2>
     where
-        L: Clone,
         N: Clone,
     {
         trivial_result(self.traverse_embed(|x| Ok(map_embed(x))))
@@ -333,52 +348,52 @@ impl<L, N, E> Expr<L, N, E> {
 
     pub fn squash_embed<E2>(
         &self,
-        f: impl FnMut(&E) -> SubExpr<L, N, E2>,
-    ) -> SubExpr<L, N, E2>
+        f: impl FnMut(&E) -> SubExpr<N, E2>,
+    ) -> SubExpr<N, E2>
     where
-        L: Clone,
         N: Clone,
     {
         trivial_result(self.visit(&mut visitor::SquashEmbedVisitor(f)))
     }
 }
 
-impl<L: Clone, E: Clone> Expr<L, X, E> {
-    pub fn note_absurd<N>(&self) -> Expr<L, N, E> {
+impl<E: Clone> Expr<X, E> {
+    pub fn note_absurd<N>(&self) -> Expr<N, E> {
         self.visit(&mut visitor::NoteAbsurdVisitor)
     }
 }
 
-impl<L: Clone, N: Clone> Expr<L, N, X> {
-    pub fn embed_absurd<E>(&self) -> Expr<L, N, E> {
+impl<N: Clone> Expr<N, X> {
+    pub fn embed_absurd<E>(&self) -> Expr<N, E> {
         self.visit(&mut visitor::EmbedAbsurdVisitor)
     }
 }
 
-impl<V, N, E> SubExpr<V, N, E> {
-    pub fn as_ref(&self) -> &Expr<V, N, E> {
+impl<N, E> SubExpr<N, E> {
+    pub fn as_ref(&self) -> &Expr<N, E> {
         &self.0.as_ref().0
     }
 
-    pub fn new(x: Expr<V, N, E>, n: N) -> Self {
+    pub fn new(x: Expr<N, E>, n: N) -> Self {
         SubExpr(Rc::new((x, Some(n))))
     }
 
-    pub fn from_expr_no_note(x: Expr<V, N, E>) -> Self {
+    pub fn from_expr_no_note(x: Expr<N, E>) -> Self {
         SubExpr(Rc::new((x, None)))
     }
 
-    pub fn unnote(&self) -> SubExpr<V, X, E>
+    pub fn unnote(&self) -> SubExpr<X, E>
     where
-        V: Clone,
         E: Clone,
     {
         SubExpr::from_expr_no_note(
             self.as_ref().visit(&mut visitor::UnNoteVisitor),
         )
     }
+}
 
-    pub fn rewrap<E2>(&self, x: Expr<V, N, E2>) -> SubExpr<V, N, E2>
+impl<N: Clone, E> SubExpr<N, E> {
+    pub fn rewrap<E2>(&self, x: Expr<N, E2>) -> SubExpr<N, E2>
     where
         N: Clone,
     {
@@ -388,9 +403,8 @@ impl<V, N, E> SubExpr<V, N, E> {
     pub fn traverse_embed<E2, Err>(
         &self,
         visit_embed: impl FnMut(&E) -> Result<E2, Err>,
-    ) -> Result<SubExpr<V, N, E2>, Err>
+    ) -> Result<SubExpr<N, E2>, Err>
     where
-        V: Clone,
         N: Clone,
     {
         Ok(self.rewrap(self.as_ref().traverse_embed(visit_embed)?))
@@ -399,9 +413,8 @@ impl<V, N, E> SubExpr<V, N, E> {
     pub fn map_embed<E2>(
         &self,
         map_embed: impl FnMut(&E) -> E2,
-    ) -> SubExpr<V, N, E2>
+    ) -> SubExpr<N, E2>
     where
-        V: Clone,
         N: Clone,
     {
         self.rewrap(self.as_ref().map_embed(map_embed))
@@ -410,12 +423,8 @@ impl<V, N, E> SubExpr<V, N, E> {
     pub fn map_subexprs_with_special_handling_of_binders<'a>(
         &'a self,
         map_expr: impl FnMut(&'a Self) -> Self,
-        map_under_binder: impl FnMut(&'a V, &'a Self) -> Self,
-    ) -> Self
-    where
-        V: Clone,
-        N: Clone,
-    {
+        map_under_binder: impl FnMut(&'a Label, &'a Self) -> Self,
+    ) -> Self {
         match self.as_ref() {
             ExprF::Embed(_) => SubExpr::clone(self),
             // This calls ExprF::map_ref
@@ -423,7 +432,7 @@ impl<V, N, E> SubExpr<V, N, E> {
                 map_expr,
                 map_under_binder,
                 |_| unreachable!(),
-                V::clone,
+                Label::clone,
             )),
         }
     }
@@ -432,34 +441,26 @@ impl<V, N, E> SubExpr<V, N, E> {
     /// capture by shifting variable indices
     /// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift
     /// for details
-    pub fn shift(&self, delta: isize, var: &Var<V>) -> Self
-    where
-        V: Clone + PartialEq,
-        N: Clone,
-    {
+    pub fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         match self.as_ref() {
             ExprF::Var(v) => self.rewrap(ExprF::Var(v.shift(delta, var))),
             _ => self.map_subexprs_with_special_handling_of_binders(
                 |e| e.shift(delta, var),
-                |x: &V, e| e.shift(delta, &var.shift(1, &Var::new(x.clone()))),
+                |x: &Label, e| e.shift(delta, &var.shift(1, &x.into())),
             ),
         }
     }
 
-    pub fn subst_shift(&self, var: &Var<V>, val: &Self) -> Self
-    where
-        V: Clone + PartialEq,
-        N: Clone,
-    {
+    pub fn subst_shift(&self, var: &V<Label>, val: &Self) -> Self {
         match self.as_ref() {
             ExprF::Var(v) if v == var => val.clone(),
             ExprF::Var(v) => self.rewrap(ExprF::Var(v.shift(-1, var))),
             _ => self.map_subexprs_with_special_handling_of_binders(
                 |e| e.subst_shift(var, val),
-                |x: &V, e| {
+                |x: &Label, e| {
                     e.subst_shift(
-                        &var.shift(1, &Var::new(x.clone())),
-                        &val.shift(1, &Var::new(x.clone())),
+                        &var.shift(1, &x.into()),
+                        &val.shift(1, &x.into()),
                     )
                 },
             ),
@@ -467,26 +468,26 @@ impl<V, N, E> SubExpr<V, N, E> {
     }
 }
 
-impl<L: Clone, N: Clone> SubExpr<L, N, X> {
-    pub fn embed_absurd<T>(&self) -> SubExpr<L, N, T> {
+impl<N: Clone> SubExpr<N, X> {
+    pub fn embed_absurd<T>(&self) -> SubExpr<N, T> {
         self.rewrap(self.as_ref().embed_absurd())
     }
 }
 
-impl<L: Clone, E: Clone> SubExpr<L, X, E> {
-    pub fn note_absurd<N>(&self) -> SubExpr<L, N, E> {
+impl<E: Clone> SubExpr<X, E> {
+    pub fn note_absurd<N>(&self) -> SubExpr<N, E> {
         SubExpr::from_expr_no_note(self.as_ref().note_absurd())
     }
 }
 
-impl<L, N, E> Clone for SubExpr<L, N, E> {
+impl<N, E> Clone for SubExpr<N, E> {
     fn clone(&self) -> Self {
         SubExpr(Rc::clone(&self.0))
     }
 }
 
 // Should probably rename this
-pub fn rc<L, E>(x: Expr<L, X, E>) -> SubExpr<L, X, E> {
+pub fn rc<E>(x: Expr<X, E>) -> SubExpr<X, E> {
     SubExpr::from_expr_no_note(x)
 }
 
@@ -500,35 +501,18 @@ fn add_ui(u: usize, i: isize) -> usize {
     }
 }
 
-impl<L> Var<L> {
-    fn new(x: L) -> Self {
-        Var(x, 0)
-    }
-}
-impl<L: PartialEq + Clone> Var<L> {
-    pub fn shift(&self, delta: isize, var: &Var<L>) -> Self {
-        let Var(x, n) = var;
-        let Var(y, m) = self;
+impl<Label: PartialEq + Clone> V<Label> {
+    pub fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        let V(x, n) = var;
+        let V(y, m) = self;
         if x == y && n <= m {
-            Var(y.clone(), add_ui(*m, delta))
+            V(y.clone(), add_ui(*m, delta))
         } else {
-            Var(y.clone(), *m)
+            V(y.clone(), *m)
         }
     }
 }
 
-// This is only for the specific `Label` type, not generic
-impl From<Label> for Var<Label> {
-    fn from(x: Label) -> Var<Label> {
-        Var(x, 0)
-    }
-}
-impl<'a> From<&'a Label> for Var<Label> {
-    fn from(x: &'a Label) -> Var<Label> {
-        Var(x.clone(), 0)
-    }
-}
-
 /// `shift` is used by both normalization and type-checking to avoid variable
 /// capture by shifting variable indices
 /// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift
@@ -536,9 +520,9 @@ impl<'a> From<&'a Label> for Var<Label> {
 ///
 pub fn shift<N, E>(
     delta: isize,
-    var: &Var<Label>,
-    in_expr: &SubExpr<Label, N, E>,
-) -> SubExpr<Label, N, E>
+    var: &V<Label>,
+    in_expr: &SubExpr<N, E>,
+) -> SubExpr<N, E>
 where
     N: Clone,
 {
@@ -547,8 +531,8 @@ where
 
 pub fn shift0_multiple<N, E>(
     deltas: &HashMap<Label, isize>,
-    in_expr: &SubExpr<Label, N, E>,
-) -> SubExpr<Label, N, E>
+    in_expr: &SubExpr<N, E>,
+) -> SubExpr<N, E>
 where
     N: Clone,
 {
@@ -558,15 +542,16 @@ where
 fn shift0_multiple_inner<N, E>(
     ctx: &Context<Label, ()>,
     deltas: &HashMap<Label, isize>,
-    in_expr: &SubExpr<Label, N, E>,
-) -> SubExpr<Label, N, E>
+    in_expr: &SubExpr<N, E>,
+) -> SubExpr<N, E>
 where
     N: Clone,
 {
+    use crate::ExprF::*;
     match in_expr.as_ref() {
-        ExprF::Var(Var(y, m)) if ctx.lookup(y, *m).is_none() => {
+        Var(V(y, m)) if ctx.lookup(y, *m).is_none() => {
             let delta = deltas.get(y).unwrap_or(&0);
-            in_expr.rewrap(ExprF::Var(Var(y.clone(), add_ui(*m, *delta))))
+            in_expr.rewrap(Var(V(y.clone(), add_ui(*m, *delta))))
         }
         _ => in_expr.map_subexprs_with_special_handling_of_binders(
             |e| shift0_multiple_inner(ctx, deltas, e),
diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index bdef553..83ccc1e 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -8,13 +8,7 @@ use std::rc::Rc;
 
 use dhall_generated_parser::{DhallParser, Rule};
 
-use crate::ExprF::{
-    Annot, App, BinOp, BoolIf, BoolLit, Builtin, Const, DoubleLit, Embed,
-    EmptyListLit, Field, IntegerLit, Lam, Let, Merge, NEListLit, NaturalLit,
-    OldOptionalLit, Pi, Projection, RecordLit, RecordType, SomeLit, TextLit,
-    UnionLit, UnionType,
-};
-
+use crate::ExprF::*;
 use crate::*;
 
 // This file consumes the parse tree generated by pest and turns it into
@@ -22,10 +16,10 @@ use crate::*;
 // their own crate because they are quite general and useful. For now they
 // are here and hopefully you can figure out how they work.
 
-type ParsedExpr = Expr<Label, Span, Import>;
-type ParsedSubExpr = SubExpr<Label, Span, Import>;
-type ParsedText = InterpolatedText<ParsedSubExpr>;
-type ParsedTextContents = InterpolatedTextContents<ParsedSubExpr>;
+type ParsedExpr = Expr<Span, Import>;
+type ParsedSubExpr = SubExpr<Span, Import>;
+type ParsedText = InterpolatedText<SubExpr<Span, Import>>;
+type ParsedTextContents = InterpolatedTextContents<SubExpr<Span, Import>>;
 
 pub type ParseError = pest::error::Error<Rule>;
 
@@ -510,17 +504,17 @@ make_parser! {
 
     rule!(identifier<ParsedSubExpr> as expression; span; children!(
         [variable(v)] => {
-            spanned(span, ExprF::Var(v))
+            spanned(span, Var(v))
         },
         [builtin(e)] => e,
     ));
 
-    rule!(variable<Var<Label>>; children!(
+    rule!(variable<V<Label>>; children!(
         [label(l), natural_literal(idx)] => {
-            Var(l, idx)
+            V(l, idx)
         },
         [label(l)] => {
-            Var(l, 0)
+            V(l, 0)
         },
     ));
 
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index 9cc1b46..e3b180b 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -3,9 +3,7 @@ use itertools::Itertools;
 use std::fmt::{self, Display};
 
 /// Generic instance that delegates to subexpressions
-impl<SE: Display + Clone, L: Display + Clone, E: Display> Display
-    for ExprF<SE, L, E>
-{
+impl<SE: Display + Clone, E: Display> Display for ExprF<SE, Label, E> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         use crate::ExprF::*;
         match self {
@@ -15,10 +13,9 @@ impl<SE: Display + Clone, L: Display + Clone, E: Display> Display
             BoolIf(a, b, c) => {
                 write!(f, "if {} then {} else {}", a, b, c)?;
             }
-            // TODO: arrow type
-            // Pi(a, b, c) if &String::from(a) == "_" => {
-            //     write!(f, "{} → {}", b, c)?;
-            // }
+            Pi(a, b, c) if &String::from(a) == "_" => {
+                write!(f, "{} → {}", b, c)?;
+            }
             Pi(a, b, c) => {
                 write!(f, "∀({} : {}) → {}", a, b, c)?;
             }
@@ -127,25 +124,21 @@ enum PrintPhase {
 // Wraps an Expr with a phase, so that phase selsction can be done
 // separate from the actual printing
 #[derive(Clone)]
-struct PhasedExpr<'a, L, S, A>(&'a SubExpr<L, S, A>, PrintPhase);
+struct PhasedExpr<'a, S, A>(&'a SubExpr<S, A>, PrintPhase);
 
-impl<'a, L: Display + Clone, S: Clone, A: Display + Clone> Display
-    for PhasedExpr<'a, L, S, A>
-{
+impl<'a, S: Clone, A: Display + Clone> Display for PhasedExpr<'a, S, A> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         self.0.as_ref().fmt_phase(f, self.1)
     }
 }
 
-impl<'a, L: Display + Clone, S: Clone, A: Display + Clone>
-    PhasedExpr<'a, L, S, A>
-{
-    fn phase(self, phase: PrintPhase) -> PhasedExpr<'a, L, S, A> {
+impl<'a, S: Clone, A: Display + Clone> PhasedExpr<'a, S, A> {
+    fn phase(self, phase: PrintPhase) -> PhasedExpr<'a, S, A> {
         PhasedExpr(self.0, phase)
     }
 }
 
-impl<L: Display + Clone, S: Clone, A: Display + Clone> Expr<L, S, A> {
+impl<S: Clone, A: Display + Clone> Expr<S, A> {
     fn fmt_phase(
         &self,
         f: &mut fmt::Formatter,
@@ -179,12 +172,11 @@ impl<L: Display + Clone, S: Clone, A: Display + Clone> Expr<L, S, A> {
         // Annotate subexpressions with the appropriate phase, defaulting to Base
         let phased_self = match self.map_ref_simple(|e| PhasedExpr(e, Base)) {
             Pi(a, b, c) => {
-                // TODO: arrow type
-                // if &String::from(&a) == "_" {
-                //     Pi(a, b.phase(Operator), c)
-                // } else {
-                Pi(a, b, c)
-                // }
+                if &String::from(&a) == "_" {
+                    Pi(a, b.phase(Operator), c)
+                } else {
+                    Pi(a, b, c)
+                }
             }
             Merge(a, b, c) => Merge(
                 a.phase(Import),
@@ -220,9 +212,7 @@ impl<L: Display + Clone, S: Clone, A: Display + Clone> Expr<L, S, A> {
     }
 }
 
-impl<L: Display + Clone, S: Clone, A: Display + Clone> Display
-    for SubExpr<L, S, A>
-{
+impl<S: Clone, A: Display + Clone> Display for SubExpr<S, A> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         self.as_ref().fmt_phase(f, PrintPhase::Base)
     }
@@ -484,9 +474,9 @@ impl Display for Scheme {
     }
 }
 
-impl<Label: Display> Display for Var<Label> {
+impl<Label: Display> Display for V<Label> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
-        let Var(x, n) = self;
+        let V(x, n) = self;
         x.fmt(f)?;
         if *n != 0 {
             write!(f, "@{}", n)?;
diff --git a/dhall_syntax/src/visitor.rs b/dhall_syntax/src/visitor.rs
index a8e5a8c..7fdf217 100644
--- a/dhall_syntax/src/visitor.rs
+++ b/dhall_syntax/src/visitor.rs
@@ -48,6 +48,8 @@ pub trait ExprFVeryGenericVisitor<'a, Ret, SE1, L1, E1>: Sized {
 impl<'a, T, Ret, SE1, L1, E1>
     GenericVisitor<&'a ExprF<SE1, L1, E1>, Result<Ret, T::Error>> for T
 where
+    L1: Ord,
+    T::L2: Ord,
     T: ExprFVeryGenericVisitor<'a, Ret, SE1, L1, E1>,
 {
     fn visit(self, input: &'a ExprF<SE1, L1, E1>) -> Result<Ret, T::Error> {
@@ -67,27 +69,31 @@ where
             })
         }
         fn btmap<'a, V, Ret, SE, L, E>(
-            x: &'a BTreeMap<Label, SE>,
+            x: &'a BTreeMap<L, SE>,
             mut v: V,
-        ) -> Result<BTreeMap<Label, V::SE2>, V::Error>
+        ) -> Result<BTreeMap<V::L2, V::SE2>, V::Error>
         where
+            L: Ord,
+            V::L2: Ord,
             V: ExprFVeryGenericVisitor<'a, Ret, SE, L, E>,
         {
             x.iter()
-                .map(|(k, x)| Ok((k.clone(), v.visit_subexpr(x)?)))
+                .map(|(k, x)| Ok((v.visit_label(k)?, v.visit_subexpr(x)?)))
                 .collect()
         }
         fn btoptmap<'a, V, Ret, SE, L, E>(
-            x: &'a BTreeMap<Label, Option<SE>>,
+            x: &'a BTreeMap<L, Option<SE>>,
             mut v: V,
-        ) -> Result<BTreeMap<Label, Option<V::SE2>>, V::Error>
+        ) -> Result<BTreeMap<V::L2, Option<V::SE2>>, V::Error>
         where
+            L: Ord,
+            V::L2: Ord,
             V: ExprFVeryGenericVisitor<'a, Ret, SE, L, E>,
         {
             x.iter()
                 .map(|(k, x)| {
                     Ok((
-                        k.clone(),
+                        v.visit_label(k)?,
                         match x {
                             Some(x) => Some(v.visit_subexpr(x)?),
                             None => None,
@@ -98,14 +104,9 @@ where
         }
 
         let mut v = self;
-        use crate::ExprF::{
-            Annot, App, BinOp, BoolIf, BoolLit, Builtin, Const, DoubleLit,
-            Embed, EmptyListLit, Field, IntegerLit, Lam, Let, Merge, NEListLit,
-            NaturalLit, OldOptionalLit, Pi, Projection, RecordLit, RecordType,
-            SomeLit, TextLit, UnionLit, UnionType,
-        };
+        use crate::ExprF::*;
         T::visit_resulting_exprf(match input {
-            ExprF::Var(Var(l, n)) => ExprF::Var(Var(v.visit_label(l)?, *n)),
+            Var(V(l, n)) => Var(V(v.visit_label(l)?, *n)),
             Lam(l, t, e) => {
                 let t = v.visit_subexpr(t)?;
                 let (l, e) = v.visit_binder(l, e)?;
@@ -149,16 +150,20 @@ where
             RecordType(kts) => RecordType(btmap(kts, v)?),
             RecordLit(kvs) => RecordLit(btmap(kvs, v)?),
             UnionType(kts) => UnionType(btoptmap(kts, v)?),
-            UnionLit(l, x, kts) => {
-                UnionLit(l.clone(), v.visit_subexpr(x)?, btoptmap(kts, v)?)
-            }
+            UnionLit(k, x, kts) => UnionLit(
+                v.visit_label(k)?,
+                v.visit_subexpr(x)?,
+                btoptmap(kts, v)?,
+            ),
             Merge(x, y, t) => Merge(
                 v.visit_subexpr(x)?,
                 v.visit_subexpr(y)?,
                 opt(t, |e| v.visit_subexpr(e))?,
             ),
-            Field(e, l) => Field(v.visit_subexpr(e)?, l.clone()),
-            Projection(e, ls) => Projection(v.visit_subexpr(e)?, ls.clone()),
+            Field(e, l) => Field(v.visit_subexpr(e)?, v.visit_label(l)?),
+            Projection(e, ls) => {
+                Projection(v.visit_subexpr(e)?, vec(ls, |l| v.visit_label(l))?)
+            }
             Embed(a) => return v.visit_embed_squash(a),
         })
     }
@@ -309,6 +314,8 @@ where
 impl<'a, T, SE1, SE2, L1, L2, E1, E2>
     GenericVisitor<&'a ExprF<SE1, L1, E1>, ExprF<SE2, L2, E2>> for T
 where
+    L1: Ord,
+    L2: Ord,
     T: ExprFInFallibleVisitor<'a, SE1, SE2, L1, L2, E1, E2>,
 {
     fn visit(self, input: &'a ExprF<SE1, L1, E1>) -> ExprF<SE2, L2, E2> {
@@ -330,6 +337,8 @@ where
     SE: 'a,
     L: 'a,
     E: 'a,
+    L: Ord,
+    L2: Ord,
     F1: FnMut(&'a SE) -> Result<SE2, Err>,
     F2: FnOnce(&'a L, &'a SE) -> Result<SE2, Err>,
     F4: FnOnce(&'a E) -> Result<E2, Err>,
@@ -368,6 +377,8 @@ where
     SE: 'a,
     L: 'a,
     E: 'a,
+    L: Ord,
+    L2: Ord,
     F1: FnMut(&'a SE) -> Result<SE2, Err>,
     F3: FnOnce(&'a E) -> Result<E2, Err>,
     F4: FnMut(&'a L) -> Result<L2, Err>,
@@ -387,11 +398,10 @@ where
 
 pub struct TraverseEmbedVisitor<F1>(pub F1);
 
-impl<'a, 'b, L, N, E, E2, Err, F1>
-    ExprFFallibleVisitor<'a, SubExpr<L, N, E>, SubExpr<L, N, E2>, L, L, E, E2>
+impl<'a, 'b, N, E, E2, Err, F1>
+    ExprFFallibleVisitor<'a, SubExpr<N, E>, SubExpr<N, E2>, Label, Label, E, E2>
     for &'b mut TraverseEmbedVisitor<F1>
 where
-    L: Clone + 'a,
     N: Clone + 'a,
     F1: FnMut(&E) -> Result<E2, Err>,
 {
@@ -399,48 +409,50 @@ where
 
     fn visit_subexpr(
         &mut self,
-        subexpr: &'a SubExpr<L, N, E>,
-    ) -> Result<SubExpr<L, N, E2>, Self::Error> {
+        subexpr: &'a SubExpr<N, E>,
+    ) -> Result<SubExpr<N, E2>, Self::Error> {
         Ok(subexpr.rewrap(subexpr.as_ref().visit(&mut **self)?))
     }
     fn visit_embed(self, embed: &'a E) -> Result<E2, Self::Error> {
         (self.0)(embed)
     }
-    fn visit_label(&mut self, label: &'a L) -> Result<L, Self::Error> {
-        Ok(L::clone(label))
+    fn visit_label(&mut self, label: &'a Label) -> Result<Label, Self::Error> {
+        Ok(Label::clone(label))
     }
 }
 
 pub struct SquashEmbedVisitor<F1>(pub F1);
 
-impl<'a, 'b, L, N, E1, E2, F1>
-    ExprFVeryGenericVisitor<'a, SubExpr<L, N, E2>, SubExpr<L, N, E1>, L, E1>
+impl<'a, 'b, N, E1, E2, F1>
+    ExprFVeryGenericVisitor<'a, SubExpr<N, E2>, SubExpr<N, E1>, Label, E1>
     for &'b mut SquashEmbedVisitor<F1>
 where
-    L: Clone + 'a,
     N: Clone + 'a,
-    F1: FnMut(&E1) -> SubExpr<L, N, E2>,
+    F1: FnMut(&E1) -> SubExpr<N, E2>,
 {
     type Error = X;
-    type SE2 = SubExpr<L, N, E2>;
-    type L2 = L;
+    type SE2 = SubExpr<N, E2>;
+    type L2 = Label;
     type E2 = E2;
 
     fn visit_subexpr(
         &mut self,
-        subexpr: &'a SubExpr<L, N, E1>,
+        subexpr: &'a SubExpr<N, E1>,
     ) -> Result<Self::SE2, Self::Error> {
         Ok(subexpr.as_ref().visit(&mut **self)?)
     }
 
-    fn visit_label(&mut self, label: &'a L) -> Result<Self::L2, Self::Error> {
-        Ok(L::clone(label))
+    fn visit_label(
+        &mut self,
+        label: &'a Label,
+    ) -> Result<Self::L2, Self::Error> {
+        Ok(Label::clone(label))
     }
 
     fn visit_binder(
         mut self,
-        label: &'a L,
-        subexpr: &'a SubExpr<L, N, E1>,
+        label: &'a Label,
+        subexpr: &'a SubExpr<N, E1>,
     ) -> Result<(Self::L2, Self::SE2), Self::Error> {
         Ok((self.visit_label(label)?, self.visit_subexpr(subexpr)?))
     }
@@ -448,7 +460,7 @@ where
     fn visit_embed_squash(
         self,
         embed: &'a E1,
-    ) -> Result<SubExpr<L, N, E2>, Self::Error> {
+    ) -> Result<SubExpr<N, E2>, Self::Error> {
         Ok((self.0)(embed))
     }
 
@@ -456,7 +468,7 @@ where
     // Useful to change the result type, and/or avoid some loss of info
     fn visit_resulting_exprf(
         result: ExprF<Self::SE2, Self::L2, Self::E2>,
-    ) -> Result<SubExpr<L, N, E2>, Self::Error> {
+    ) -> Result<SubExpr<N, E2>, Self::Error> {
         // TODO: don't lose note
         Ok(SubExpr::from_expr_no_note(result))
     }
@@ -464,69 +476,57 @@ where
 
 pub struct UnNoteVisitor;
 
-impl<'a, 'b, L, N, E>
-    ExprFInFallibleVisitor<'a, SubExpr<L, N, E>, SubExpr<L, X, E>, L, L, E, E>
+impl<'a, 'b, N, E>
+    ExprFInFallibleVisitor<'a, SubExpr<N, E>, SubExpr<X, E>, Label, Label, E, E>
     for &'b mut UnNoteVisitor
 where
-    L: Clone + 'a,
     E: Clone + 'a,
 {
-    fn visit_subexpr(
-        &mut self,
-        subexpr: &'a SubExpr<L, N, E>,
-    ) -> SubExpr<L, X, E> {
+    fn visit_subexpr(&mut self, subexpr: &'a SubExpr<N, E>) -> SubExpr<X, E> {
         SubExpr::from_expr_no_note(subexpr.as_ref().visit(&mut **self))
     }
     fn visit_embed(self, embed: &'a E) -> E {
         E::clone(embed)
     }
-    fn visit_label(&mut self, label: &'a L) -> L {
-        L::clone(label)
+    fn visit_label(&mut self, label: &'a Label) -> Label {
+        Label::clone(label)
     }
 }
 
 pub struct NoteAbsurdVisitor;
 
-impl<'a, 'b, L, N, E>
-    ExprFInFallibleVisitor<'a, SubExpr<L, X, E>, SubExpr<L, N, E>, L, L, E, E>
+impl<'a, 'b, N, E>
+    ExprFInFallibleVisitor<'a, SubExpr<X, E>, SubExpr<N, E>, Label, Label, E, E>
     for &'b mut NoteAbsurdVisitor
 where
-    L: Clone + 'a,
     E: Clone + 'a,
 {
-    fn visit_subexpr(
-        &mut self,
-        subexpr: &'a SubExpr<L, X, E>,
-    ) -> SubExpr<L, N, E> {
+    fn visit_subexpr(&mut self, subexpr: &'a SubExpr<X, E>) -> SubExpr<N, E> {
         SubExpr::from_expr_no_note(subexpr.as_ref().visit(&mut **self))
     }
     fn visit_embed(self, embed: &'a E) -> E {
         E::clone(embed)
     }
-    fn visit_label(&mut self, label: &'a L) -> L {
-        L::clone(label)
+    fn visit_label(&mut self, label: &'a Label) -> Label {
+        Label::clone(label)
     }
 }
 
 pub struct EmbedAbsurdVisitor;
 
-impl<'a, 'b, L, N, E>
-    ExprFInFallibleVisitor<'a, SubExpr<L, N, X>, SubExpr<L, N, E>, L, L, X, E>
+impl<'a, 'b, N, E>
+    ExprFInFallibleVisitor<'a, SubExpr<N, X>, SubExpr<N, E>, Label, Label, X, E>
     for &'b mut EmbedAbsurdVisitor
 where
-    L: Clone + 'a,
     N: Clone + 'a,
 {
-    fn visit_subexpr(
-        &mut self,
-        subexpr: &'a SubExpr<L, N, X>,
-    ) -> SubExpr<L, N, E> {
+    fn visit_subexpr(&mut self, subexpr: &'a SubExpr<N, X>) -> SubExpr<N, E> {
         subexpr.rewrap(subexpr.as_ref().visit(&mut **self))
     }
     fn visit_embed(self, embed: &'a X) -> E {
         match *embed {}
     }
-    fn visit_label(&mut self, label: &'a L) -> L {
-        L::clone(label)
+    fn visit_label(&mut self, label: &'a Label) -> Label {
+        Label::clone(label)
     }
 }
-- 
cgit v1.2.3


From 6792d3da32d11b5303b00d1cc667f6f946d8bf33 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 4 May 2019 19:51:26 +0200
Subject: We actually don't need SubExpr::shift anymore

---
 dhall_syntax/src/core.rs | 81 ------------------------------------------------
 1 file changed, 81 deletions(-)

(limited to 'dhall_syntax')

diff --git a/dhall_syntax/src/core.rs b/dhall_syntax/src/core.rs
index a186d19..7cdda64 100644
--- a/dhall_syntax/src/core.rs
+++ b/dhall_syntax/src/core.rs
@@ -1,9 +1,7 @@
 #![allow(non_snake_case)]
 use std::collections::BTreeMap;
-use std::collections::HashMap;
 use std::rc::Rc;
 
-use crate::context::Context;
 use crate::visitor;
 use crate::*;
 
@@ -436,36 +434,6 @@ impl<N: Clone, E> SubExpr<N, E> {
             )),
         }
     }
-
-    /// `shift` is used by both normalization and type-checking to avoid variable
-    /// capture by shifting variable indices
-    /// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift
-    /// for details
-    pub fn shift(&self, delta: isize, var: &V<Label>) -> Self {
-        match self.as_ref() {
-            ExprF::Var(v) => self.rewrap(ExprF::Var(v.shift(delta, var))),
-            _ => self.map_subexprs_with_special_handling_of_binders(
-                |e| e.shift(delta, var),
-                |x: &Label, e| e.shift(delta, &var.shift(1, &x.into())),
-            ),
-        }
-    }
-
-    pub fn subst_shift(&self, var: &V<Label>, val: &Self) -> Self {
-        match self.as_ref() {
-            ExprF::Var(v) if v == var => val.clone(),
-            ExprF::Var(v) => self.rewrap(ExprF::Var(v.shift(-1, var))),
-            _ => self.map_subexprs_with_special_handling_of_binders(
-                |e| e.subst_shift(var, val),
-                |x: &Label, e| {
-                    e.subst_shift(
-                        &var.shift(1, &x.into()),
-                        &val.shift(1, &x.into()),
-                    )
-                },
-            ),
-        }
-    }
 }
 
 impl<N: Clone> SubExpr<N, X> {
@@ -512,52 +480,3 @@ impl<Label: PartialEq + Clone> V<Label> {
         }
     }
 }
-
-/// `shift` is used by both normalization and type-checking to avoid variable
-/// capture by shifting variable indices
-/// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift
-/// for details
-///
-pub fn shift<N, E>(
-    delta: isize,
-    var: &V<Label>,
-    in_expr: &SubExpr<N, E>,
-) -> SubExpr<N, E>
-where
-    N: Clone,
-{
-    in_expr.shift(delta, var)
-}
-
-pub fn shift0_multiple<N, E>(
-    deltas: &HashMap<Label, isize>,
-    in_expr: &SubExpr<N, E>,
-) -> SubExpr<N, E>
-where
-    N: Clone,
-{
-    shift0_multiple_inner(&Context::new(), deltas, in_expr)
-}
-
-fn shift0_multiple_inner<N, E>(
-    ctx: &Context<Label, ()>,
-    deltas: &HashMap<Label, isize>,
-    in_expr: &SubExpr<N, E>,
-) -> SubExpr<N, E>
-where
-    N: Clone,
-{
-    use crate::ExprF::*;
-    match in_expr.as_ref() {
-        Var(V(y, m)) if ctx.lookup(y, *m).is_none() => {
-            let delta = deltas.get(y).unwrap_or(&0);
-            in_expr.rewrap(Var(V(y.clone(), add_ui(*m, *delta))))
-        }
-        _ => in_expr.map_subexprs_with_special_handling_of_binders(
-            |e| shift0_multiple_inner(ctx, deltas, e),
-            |x: &Label, e| {
-                shift0_multiple_inner(&ctx.insert(x.clone(), ()), deltas, e)
-            },
-        ),
-    }
-}
-- 
cgit v1.2.3