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/printer.rs | 51 +++++++++++++++++++++++++++++---------------- 1 file changed, 33 insertions(+), 18 deletions(-) (limited to 'dhall_syntax/src/printer.rs') 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 Display - for ExprF +impl Display for ExprF +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 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, 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 Expr { +impl Expr +where + L: VarLabel, + S: Clone, + A: Display + Clone, +{ fn fmt_phase( &self, f: &mut fmt::Formatter, @@ -179,12 +192,11 @@ impl Expr { // 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 Expr { } } -impl Display - for SubExpr +impl Display for SubExpr +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