summaryrefslogtreecommitdiff
path: root/dhall_syntax
diff options
context:
space:
mode:
authorFintanH2019-08-12 22:34:21 +0100
committerFintanH2019-08-12 22:34:21 +0100
commit4a86274878d5ab0ef4f9d8597606226adfd048de (patch)
tree68153eb0e4283740f49042e059402da6eaaf551e /dhall_syntax
parent405bc3d80c0e169ea74dd12422b9504b7383dab3 (diff)
parent7d17d39005531cb77d8eaf32ed7de8938c66f874 (diff)
Merge remote-tracking branch 'origin/master' into fintan/canonicalize
Diffstat (limited to '')
-rw-r--r--dhall_syntax/src/core/expr.rs58
-rw-r--r--dhall_syntax/src/core/import.rs2
-rw-r--r--dhall_syntax/src/core/map.rs95
-rw-r--r--dhall_syntax/src/core/visitor.rs33
-rw-r--r--dhall_syntax/src/parser.rs146
-rw-r--r--dhall_syntax/src/printer.rs27
6 files changed, 254 insertions, 107 deletions
diff --git a/dhall_syntax/src/core/expr.rs b/dhall_syntax/src/core/expr.rs
index da9465d..6522cb1 100644
--- a/dhall_syntax/src/core/expr.rs
+++ b/dhall_syntax/src/core/expr.rs
@@ -1,6 +1,6 @@
use std::rc::Rc;
-use crate::map::DupTreeMap;
+use crate::map::{DupTreeMap, DupTreeSet};
use crate::visitor;
use crate::*;
@@ -44,7 +44,7 @@ impl From<NaiveDouble> for f64 {
}
/// Constants for a pure type system
-#[derive(Debug, Copy, Clone, PartialEq, Eq)]
+#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)]
pub enum Const {
Type,
Kind,
@@ -99,6 +99,8 @@ pub enum BinOp {
BoolEQ,
/// `x != y`
BoolNE,
+ /// x === y
+ Equivalence,
}
/// Built-ins
@@ -119,6 +121,7 @@ pub enum Builtin {
NaturalOdd,
NaturalToInteger,
NaturalShow,
+ NaturalSubtract,
IntegerToDouble,
IntegerShow,
DoubleShow,
@@ -174,6 +177,8 @@ pub enum ExprF<SubExpr, Embed> {
Let(Label, Option<SubExpr>, SubExpr, SubExpr),
/// `x : t`
Annot(SubExpr, SubExpr),
+ /// `assert : t`
+ Assert(SubExpr),
/// Built-in values
Builtin(Builtin),
// Binary operations
@@ -190,14 +195,10 @@ pub enum ExprF<SubExpr, Embed> {
DoubleLit(Double),
/// `"Some ${interpolated} text"`
TextLit(InterpolatedText<SubExpr>),
- /// `[] : List t`
+ /// `[] : t`
EmptyListLit(SubExpr),
/// `[x, y, z]`
NEListLit(Vec<SubExpr>),
- /// Deprecated Optional literal form
- /// `[] : Optional a`
- /// `[x] : Optional a`
- OldOptionalLit(Option<SubExpr>, SubExpr),
/// `Some e`
SomeLit(SubExpr),
/// `{ k1 : t1, k2 : t1 }`
@@ -206,14 +207,12 @@ pub enum ExprF<SubExpr, Embed> {
RecordLit(DupTreeMap<Label, SubExpr>),
/// `< k1 : t1, k2 >`
UnionType(DupTreeMap<Label, Option<SubExpr>>),
- /// `< k1 = t1, k2 : t2, k3 >`
- UnionLit(Label, SubExpr, DupTreeMap<Label, Option<SubExpr>>),
/// `merge x y : t`
Merge(SubExpr, SubExpr, Option<SubExpr>),
/// `e.x`
Field(SubExpr, Label),
/// `e.{ x, y, z }`
- Projection(SubExpr, Vec<Label>),
+ Projection(SubExpr, DupTreeSet<Label>),
/// Embeds an import or the result of resolving the import
Embed(Embed),
}
@@ -311,6 +310,35 @@ impl<N, E> Expr<N, E> {
{
trivial_result(self.traverse_embed(|x| Ok(map_embed(x))))
}
+
+ pub fn traverse_resolve<E2, Err>(
+ &self,
+ visit_embed: impl FnMut(&E) -> Result<E2, Err>,
+ ) -> Result<Expr<N, E2>, Err>
+ where
+ N: Clone,
+ {
+ self.traverse_resolve_with_visitor(&mut visitor::ResolveVisitor(
+ visit_embed,
+ ))
+ }
+
+ pub(crate) fn traverse_resolve_with_visitor<E2, Err, F1>(
+ &self,
+ visitor: &mut visitor::ResolveVisitor<F1>,
+ ) -> Result<Expr<N, E2>, Err>
+ where
+ N: Clone,
+ F1: FnMut(&E) -> Result<E2, Err>,
+ {
+ match self {
+ ExprF::BinOp(BinOp::ImportAlt, l, r) => l
+ .as_ref()
+ .traverse_resolve_with_visitor(visitor)
+ .or(r.as_ref().traverse_resolve_with_visitor(visitor)),
+ _ => self.visit(visitor),
+ }
+ }
}
impl Expr<X, X> {
@@ -387,6 +415,16 @@ impl<N, E> SubExpr<N, E> {
)),
}
}
+
+ pub fn traverse_resolve<E2, Err>(
+ &self,
+ visit_embed: impl FnMut(&E) -> Result<E2, Err>,
+ ) -> Result<SubExpr<N, E2>, Err>
+ where
+ N: Clone,
+ {
+ Ok(self.rewrap(self.as_ref().traverse_resolve(visit_embed)?))
+ }
}
impl SubExpr<X, X> {
diff --git a/dhall_syntax/src/core/import.rs b/dhall_syntax/src/core/import.rs
index ea42dbc..82bb7ff 100644
--- a/dhall_syntax/src/core/import.rs
+++ b/dhall_syntax/src/core/import.rs
@@ -57,6 +57,7 @@ pub struct URL {
pub authority: String,
pub path: File,
pub query: Option<String>,
+ // TODO: implement inline headers
pub headers: Option<Box<ImportHashed>>,
}
@@ -71,6 +72,7 @@ pub enum Scheme {
pub enum ImportMode {
Code,
RawText,
+ Location,
}
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
diff --git a/dhall_syntax/src/core/map.rs b/dhall_syntax/src/core/map.rs
index 63f19cd..6a0ebda 100644
--- a/dhall_syntax/src/core/map.rs
+++ b/dhall_syntax/src/core/map.rs
@@ -1,5 +1,6 @@
/// A sorted map that allows multiple values for each key.
pub use dup_tree_map::DupTreeMap;
+pub use dup_tree_set::DupTreeSet;
mod one_or_more {
use either::Either;
@@ -232,3 +233,97 @@ mod dup_tree_map {
// unsafe impl<K, V> iter::TrustedLen for IntoIter<K, V> {}
}
+
+mod dup_tree_set {
+ use super::DupTreeMap;
+ use std::iter;
+
+ #[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
+ pub struct DupTreeSet<K> {
+ map: DupTreeMap<K, ()>,
+ }
+
+ pub type Iter<'a, K> = iter::Map<
+ super::dup_tree_map::Iter<'a, K, ()>,
+ for<'b> fn((&'b K, &'b ())) -> &'b K,
+ >;
+ pub type IntoIter<K> =
+ iter::Map<super::dup_tree_map::IntoIter<K, ()>, fn((K, ())) -> K>;
+
+ impl<K> DupTreeSet<K> {
+ pub fn new() -> Self
+ where
+ K: Ord,
+ {
+ DupTreeSet {
+ map: DupTreeMap::new(),
+ }
+ }
+
+ pub fn len(&self) -> usize {
+ self.map.len()
+ }
+ pub fn is_empty(&self) -> bool {
+ self.map.is_empty()
+ }
+
+ pub fn iter(&self) -> Iter<'_, K>
+ where
+ K: Ord,
+ {
+ fn foo<'a, K>((k, ()): (&'a K, &'a ())) -> &'a K {
+ k
+ }
+ self.map.iter().map(foo)
+ }
+ }
+
+ impl<K> Default for DupTreeSet<K>
+ where
+ K: Ord,
+ {
+ fn default() -> Self {
+ Self::new()
+ }
+ }
+
+ impl<K> IntoIterator for DupTreeSet<K>
+ where
+ K: Ord + Clone,
+ {
+ type Item = K;
+ type IntoIter = IntoIter<K>;
+
+ fn into_iter(self) -> Self::IntoIter {
+ fn foo<K>((k, ()): (K, ())) -> K {
+ k
+ }
+ self.map.into_iter().map(foo)
+ }
+ }
+
+ impl<'a, K> IntoIterator for &'a DupTreeSet<K>
+ where
+ K: Ord,
+ {
+ type Item = &'a K;
+ type IntoIter = Iter<'a, K>;
+
+ fn into_iter(self) -> Self::IntoIter {
+ self.iter()
+ }
+ }
+
+ impl<K> iter::FromIterator<K> for DupTreeSet<K>
+ where
+ K: Ord,
+ {
+ fn from_iter<T>(iter: T) -> Self
+ where
+ T: IntoIterator<Item = K>,
+ {
+ let map = iter.into_iter().map(|k| (k, ())).collect();
+ DupTreeSet { map }
+ }
+ }
+}
diff --git a/dhall_syntax/src/core/visitor.rs b/dhall_syntax/src/core/visitor.rs
index 99a9c11..18f76d9 100644
--- a/dhall_syntax/src/core/visitor.rs
+++ b/dhall_syntax/src/core/visitor.rs
@@ -137,17 +137,10 @@ where
),
EmptyListLit(t) => EmptyListLit(v.visit_subexpr(t)?),
NEListLit(es) => NEListLit(vec(es, |e| v.visit_subexpr(e))?),
- OldOptionalLit(x, t) => OldOptionalLit(
- opt(x, |e| v.visit_subexpr(e))?,
- v.visit_subexpr(t)?,
- ),
SomeLit(e) => SomeLit(v.visit_subexpr(e)?),
RecordType(kts) => RecordType(dupmap(kts, v)?),
RecordLit(kvs) => RecordLit(dupmap(kvs, v)?),
UnionType(kts) => UnionType(optdupmap(kts, v)?),
- UnionLit(k, x, kts) => {
- UnionLit(k.clone(), v.visit_subexpr(x)?, optdupmap(kts, v)?)
- }
Merge(x, y, t) => Merge(
v.visit_subexpr(x)?,
v.visit_subexpr(y)?,
@@ -155,6 +148,7 @@ where
),
Field(e, l) => Field(v.visit_subexpr(e)?, l.clone()),
Projection(e, ls) => Projection(v.visit_subexpr(e)?, ls.clone()),
+ Assert(e) => Assert(v.visit_subexpr(e)?),
Embed(a) => return v.visit_embed_squash(a),
})
}
@@ -362,6 +356,31 @@ where
}
}
+pub struct ResolveVisitor<F1>(pub F1);
+
+impl<'a, 'b, N, E, E2, Err, F1>
+ ExprFFallibleVisitor<'a, SubExpr<N, E>, SubExpr<N, E2>, E, E2>
+ for &'b mut ResolveVisitor<F1>
+where
+ N: Clone + 'a,
+ F1: FnMut(&E) -> Result<E2, Err>,
+{
+ type Error = Err;
+
+ fn visit_subexpr(
+ &mut self,
+ subexpr: &'a SubExpr<N, E>,
+ ) -> Result<SubExpr<N, E2>, Self::Error> {
+ Ok(subexpr.rewrap(
+ subexpr
+ .as_ref()
+ .traverse_resolve_with_visitor(&mut **self)?,
+ ))
+ }
+ fn visit_embed(self, embed: &'a E) -> Result<E2, Self::Error> {
+ (self.0)(embed)
+ }
+}
pub struct NoteAbsurdVisitor;
impl<'a, 'b, N, E>
diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index 7675622..a2495ee 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -6,7 +6,7 @@ use std::rc::Rc;
use dhall_generated_parser::{DhallParser, Rule};
-use crate::map::DupTreeMap;
+use crate::map::{DupTreeMap, DupTreeSet};
use crate::ExprF::*;
use crate::*;
@@ -80,6 +80,7 @@ impl crate::Builtin {
"Natural/odd" => Some(NaturalOdd),
"Natural/toInteger" => Some(NaturalToInteger),
"Natural/show" => Some(NaturalShow),
+ "Natural/subtract" => Some(NaturalSubtract),
"Integer/toDouble" => Some(IntegerToDouble),
"Integer/show" => Some(IntegerShow),
"Double/show" => Some(DoubleShow),
@@ -318,6 +319,7 @@ fn can_be_shortcutted(rule: Rule) -> bool {
| times_expression
| equal_expression
| not_equal_expression
+ | equivalent_expression
| application_expression
| first_application_expression
| selector_expression
@@ -410,11 +412,50 @@ make_parser! {
"n" => "\n".to_owned(),
"r" => "\r".to_owned(),
"t" => "\t".to_owned(),
+ // "uXXXX" or "u{XXXXX}"
_ => {
- // "uXXXX"
- use std::convert::TryFrom;
- let c = u16::from_str_radix(&s[1..5], 16).unwrap();
- let c = char::try_from(u32::from(c)).unwrap();
+ use std::convert::{TryFrom, TryInto};
+
+ let s = &s[1..];
+ let s = if &s[0..1] == "{" {
+ &s[1..s.len()-1]
+ } else {
+ &s[0..s.len()]
+ };
+
+ if s.len() > 8 {
+ Err(format!("Escape sequences can't have more than 8 chars: \"{}\"", s))?
+ }
+
+ // pad with zeroes
+ let s: String = std::iter::repeat('0')
+ .take(8 - s.len())
+ .chain(s.chars())
+ .collect();
+
+ // `s` has length 8, so `bytes` has length 4
+ let bytes: &[u8] = &hex::decode(s).unwrap();
+ let i = u32::from_be_bytes(bytes.try_into().unwrap());
+ let c = char::try_from(i).unwrap();
+ match i {
+ 0xD800..=0xDFFF => {
+ let c_ecapsed = c.escape_unicode();
+ Err(format!("Escape sequences can't contain surrogate pairs: \"{}\"", c_ecapsed))?
+ },
+ 0x0FFFE..=0x0FFFF | 0x1FFFE..=0x1FFFF |
+ 0x2FFFE..=0x2FFFF | 0x3FFFE..=0x3FFFF |
+ 0x4FFFE..=0x4FFFF | 0x5FFFE..=0x5FFFF |
+ 0x6FFFE..=0x6FFFF | 0x7FFFE..=0x7FFFF |
+ 0x8FFFE..=0x8FFFF | 0x9FFFE..=0x9FFFF |
+ 0xAFFFE..=0xAFFFF | 0xBFFFE..=0xBFFFF |
+ 0xCFFFE..=0xCFFFF | 0xDFFFE..=0xDFFFF |
+ 0xEFFFE..=0xEFFFF | 0xFFFFE..=0xFFFFF |
+ 0x10FFFE..=0x10FFFF => {
+ let c_ecapsed = c.escape_unicode();
+ Err(format!("Escape sequences can't contain non-characters: \"{}\"", c_ecapsed))?
+ },
+ _ => {}
+ }
std::iter::once(c).collect()
}
}
@@ -692,6 +733,7 @@ make_parser! {
));
token_rule!(Text<()>);
+ token_rule!(Location<()>);
rule!(import<ParsedSubExpr> as expression; span; children!(
[import_hashed(location_hashed)] => {
@@ -706,15 +748,28 @@ make_parser! {
location_hashed
}))
},
+ [import_hashed(location_hashed), Location(_)] => {
+ spanned(span, Embed(Import {
+ mode: ImportMode::Location,
+ location_hashed
+ }))
+ },
));
token_rule!(lambda<()>);
token_rule!(forall<()>);
token_rule!(arrow<()>);
token_rule!(merge<()>);
+ token_rule!(assert<()>);
token_rule!(if_<()>);
token_rule!(in_<()>);
+ rule!(empty_list_literal<ParsedSubExpr> as expression; span; children!(
+ [expression(e)] => {
+ spanned(span, EmptyListLit(e))
+ },
+ ));
+
rule!(expression<ParsedSubExpr> as expression; span; children!(
[lambda(()), label(l), expression(typ),
arrow(()), expression(body)] => {
@@ -739,6 +794,9 @@ make_parser! {
[merge(()), expression(x), expression(y), expression(z)] => {
spanned(span, Merge(x, y, Some(z)))
},
+ [assert(()), expression(x)] => {
+ spanned(span, Assert(x))
+ },
[expression(e)] => e,
));
@@ -753,21 +811,6 @@ make_parser! {
token_rule!(List<()>);
token_rule!(Optional<()>);
- rule!(empty_collection<ParsedSubExpr> as expression; span; children!(
- [List(_), expression(t)] => {
- spanned(span, EmptyListLit(t))
- },
- [Optional(_), expression(t)] => {
- spanned(span, OldOptionalLit(None, t))
- },
- ));
-
- rule!(non_empty_optional<ParsedSubExpr> as expression; span; children!(
- [expression(x), Optional(_), expression(t)] => {
- spanned(span, OldOptionalLit(Some(x), t))
- }
- ));
-
rule!(import_alt_expression<ParsedSubExpr> as expression; children!(
[expression(e)] => e,
[expression(first), expression(rest)..] => {
@@ -852,6 +895,13 @@ make_parser! {
rest.fold(first, |acc, e| unspanned(BinOp(o, acc, e)))
},
));
+ rule!(equivalent_expression<ParsedSubExpr> as expression; children!(
+ [expression(e)] => e,
+ [expression(first), expression(rest)..] => {
+ let o = crate::BinOp::Equivalence;
+ rest.fold(first, |acc, e| unspanned(BinOp(o, acc, e)))
+ },
+ ));
rule!(annotated_expression<ParsedSubExpr> as expression; span; children!(
[expression(e)] => e,
@@ -861,6 +911,7 @@ make_parser! {
));
token_rule!(Some_<()>);
+ token_rule!(toMap<()>);
rule!(application_expression<ParsedSubExpr> as expression; children!(
[expression(e)] => e,
@@ -890,13 +941,13 @@ make_parser! {
}
));
- rule!(selector<Either<Label, Vec<Label>>>; children!(
+ rule!(selector<Either<Label, DupTreeSet<Label>>>; children!(
[label(l)] => Either::Left(l),
[labels(ls)] => Either::Right(ls),
[expression(e)] => unimplemented!("selection by expression"), // TODO
));
- rule!(labels<Vec<Label>>; children!(
+ rule!(labels<DupTreeSet<Label>>; children!(
[label(ls)..] => ls.collect(),
));
@@ -953,67 +1004,22 @@ make_parser! {
[label(name), expression(expr)] => (name, expr)
));
- rule!(union_type_or_literal<ParsedSubExpr> as expression; span; children!(
+ rule!(union_type<ParsedSubExpr> as expression; span; children!(
[empty_union_type(_)] => {
spanned(span, UnionType(Default::default()))
},
- [non_empty_union_type_or_literal((Some((l, e)), entries))] => {
- spanned(span, UnionLit(l, e, entries))
- },
- [non_empty_union_type_or_literal((None, entries))] => {
- spanned(span, UnionType(entries))
+ [union_type_entry(entries)..] => {
+ spanned(span, UnionType(entries.collect()))
},
));
token_rule!(empty_union_type<()>);
- rule!(non_empty_union_type_or_literal
- <(Option<(Label, ParsedSubExpr)>,
- DupTreeMap<Label, Option<ParsedSubExpr>>)>;
- children!(
- [label(l), union_literal_variant_value((e, entries))] => {
- (Some((l, e)), entries)
- },
- [label(l), union_type_or_literal_variant_type((e, rest))] => {
- let (x, mut entries) = rest;
- entries.insert(l, e);
- (x, entries)
- },
- ));
-
- rule!(union_literal_variant_value
- <(ParsedSubExpr, DupTreeMap<Label, Option<ParsedSubExpr>>)>;
- children!(
- [expression(e), union_type_entry(entries)..] => {
- (e, entries.collect())
- },
- ));
-
rule!(union_type_entry<(Label, Option<ParsedSubExpr>)>; children!(
[label(name), expression(expr)] => (name, Some(expr)),
[label(name)] => (name, None),
));
- // TODO: unary union variants
- rule!(union_type_or_literal_variant_type
- <(Option<ParsedSubExpr>,
- (Option<(Label, ParsedSubExpr)>,
- DupTreeMap<Label, Option<ParsedSubExpr>>))>;
- children!(
- [expression(e), non_empty_union_type_or_literal(rest)] => {
- (Some(e), rest)
- },
- [expression(e)] => {
- (Some(e), (None, Default::default()))
- },
- [non_empty_union_type_or_literal(rest)] => {
- (None, rest)
- },
- [] => {
- (None, (None, Default::default()))
- },
- ));
-
rule!(non_empty_list_literal<ParsedSubExpr> as expression; span;
children!(
[expression(items)..] => spanned(
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index 8503a1e..5312f23 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -27,17 +27,11 @@ impl<SE: Display + Clone, E: Display> Display for ExprF<SE, E> {
write!(f, " = {} in {}", c, d)?;
}
EmptyListLit(t) => {
- write!(f, "[] : List {}", t)?;
+ write!(f, "[] : {}", t)?;
}
NEListLit(es) => {
fmt_list("[", ", ", "]", es, f, Display::fmt)?;
}
- OldOptionalLit(None, t) => {
- write!(f, "[] : Optional {}", t)?;
- }
- OldOptionalLit(Some(x), t) => {
- write!(f, "[{}] : Optional {}", x, t)?;
- }
SomeLit(e) => {
write!(f, "Some {}", e)?;
}
@@ -50,6 +44,9 @@ impl<SE: Display + Clone, E: Display> Display for ExprF<SE, E> {
Annot(a, b) => {
write!(f, "{} : {}", a, b)?;
}
+ Assert(a) => {
+ write!(f, "assert : {}", a)?;
+ }
ExprF::BinOp(op, a, b) => {
write!(f, "{} {} {}", a, op, b)?;
}
@@ -91,16 +88,6 @@ impl<SE: Display + Clone, E: Display> Display for ExprF<SE, E> {
}
Ok(())
})?,
- UnionLit(a, b, c) => {
- write!(f, "< {} = {}", a, b)?;
- for (k, v) in c {
- write!(f, " | {}", k)?;
- if let Some(v) = v {
- write!(f, ": {}", v)?;
- }
- }
- f.write_str(" >")?
- }
Embed(a) => a.fmt(f)?,
}
Ok(())
@@ -154,7 +141,6 @@ impl<S: Clone, A: Display + Clone> Expr<S, A> {
| Let(_, _, _, _)
| EmptyListLit(_)
| NEListLit(_)
- | OldOptionalLit(_, _)
| SomeLit(_)
| Merge(_, _, _)
| Annot(_, _)
@@ -189,8 +175,6 @@ impl<S: Clone, A: Display + Clone> Expr<S, A> {
a.phase(PrintPhase::BinOp(op)),
b.phase(PrintPhase::BinOp(op)),
),
- EmptyListLit(t) => EmptyListLit(t.phase(Import)),
- OldOptionalLit(x, t) => OldOptionalLit(x, t.phase(Import)),
SomeLit(e) => SomeLit(e.phase(Import)),
ExprF::App(f, a) => ExprF::App(f.phase(Import), a.phase(Import)),
Field(a, b) => Field(a.phase(Primitive), b),
@@ -305,6 +289,7 @@ impl Display for BinOp {
ImportAlt => "?",
RightBiasedRecordMerge => "⫽",
ListAppend => "#",
+ Equivalence => "≡",
})
}
}
@@ -445,6 +430,7 @@ impl Display for Import {
match self.mode {
Code => {}
RawText => write!(f, " as Text")?,
+ Location => write!(f, " as Location")?,
}
Ok(())
}
@@ -469,6 +455,7 @@ impl Display for Builtin {
NaturalOdd => "Natural/odd",
NaturalToInteger => "Natural/toInteger",
NaturalShow => "Natural/show",
+ NaturalSubtract => "Natural/subtract",
IntegerToDouble => "Integer/toDouble",
IntegerShow => "Integer/show",
DoubleShow => "Double/show",