X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;ds=sidebyside;f=pres-esop15%2F01.xhtml;h=d74a138f9aa51439db6ede4a8f36c5566ff6e5b1;hb=564cbcc2c27a723d2bdf12cf690a66eb7f36b813;hp=845513e7568c65d663f0afa0221547d9bbcd7236;hpb=606df47f18f6e5e96e43f770d6d2727c736b69fc;p=hacks%2FsimpleWebSlides.git diff --git a/pres-esop15/01.xhtml b/pres-esop15/01.xhtml index 845513e..d74a138 100644 --- a/pres-esop15/01.xhtml +++ b/pres-esop15/01.xhtml @@ -14,8 +14,8 @@ - - + Empty" > + Any" > @@ -189,32 +189,32 @@
- CNRS, PPS, Université Paris-Diderot, Paris, France
- Kangwon National University, Chuncheon, Rep. of Korea
- LRI, Université Paris-Sud, Orsay, France
+ 1 CNRS, PPS, Université Paris-Diderot, Paris, France
+ 2 Kangwon National University, Chuncheon, Rep. of Korea
+ 3 LRI, Université Paris-Sud, Orsay, France
W3C standard language for querying XML - databases/documents
-
+W3C standard to query XML documents
+
declare function get_links($page, $print) {
-
for $i in $page/descendant::a[not(ancestor::b)]
- return print($i)
+ return $print($i)
}
declare function pretty($link) {
typeswitch($link)
- case $l as element(a)
- return switch ($l/@class)
- case "style1"
+ case $l as element(a)
+ return switch ($l/@class)
+ case "style1"
return <a href={$l/@href}><b>{$l/text()}</b></a>
- default return $l
+ default return $l
- default return $link
+ default return $link
}
+
+ let $bold_links := get_links(document("file.xhtml"), $pretty)
- t ::= b | c | t à t | t &rarrow; t | t &lor; t | t &land; t | t ∖ t | ⊤ | ⊥ | α +A set &mathT; of types
+t ::= b | c | t à t | t &rarrow; t | t &lor; t | t &land; t | t ∖ t | ⊤ | ⊥ | αb : ranges over basic types (Int, String, â¦)
-
c : ranges over singleton types (`A, 42, â¦)
+ Type constructors
+ Boolean connectives
α : type variables
- types are interpreted co-inductively (recursive types) and regular + types are interpreted co-inductively: recursive types and regular expression types
- t1 ⡠(Int à t1) &lor; t2 - t2 ⡠(Bool à t2) &lor; (Bool à `nil) - - t1 ⡠[ Int* Bool+ ] - ++t1 ⡠(Int à t1) &lor; t2 + t2 ⡠(Bool à t2) &lor; (Bool à `nil)+t1 ⡠[ Int* Bool+ ]
+
The usual sets &mathV; of values:
+v ::= 1 | ⦠| `Foo | (v, v) | λx.e ++
Sequences are nested pairs (Ã la Lisp):
+[ v1 ⦠vn ] â¡ (v1, (â¦, (vn, `nil))) ++
XML documents are tagged sequences:
<foo>[ v1 ⦠vn ] ⡠(`foo, [ v1 ⦠vn ])+ +
(Sometimes we write [ ] for the variant `nil)
+Everything is built on top of products and variants
+p ::= t | p | p | p & p | (p, p) | x+
(a.k.a. the left-hand side of an arrow in a match ⦠with)
+p ::= t | x | (p, p) | p | p | p & p
t ranges over types
x ranges over capture variables
+ Pair patterns
+ Alternation |, Intersection &
patterns are also co-inductively interpreted (recursive patterns)
v / p : matching a value against a pattern yields a @@ -366,14 +379,14 @@ t ≤ s &Lrarrow; [t] ⊆ [s] | [ _* (x & Int) ] &rarrow; (x, `false) | [ ] &rarrow; (0, `false) -
Sequences are nested pairs: [ v1 ⦠vn ] â¡ (v1, (â¦, (vn, `nil))) -
-XML documents are tagged sequences:
<foo>[ v1 ⦠vn ] ⡠(`foo, [ v1 ⦠vn ])- -
Ususal lisp-like encoding of trees, how to perform navigation - (including upward ?)
-v ::= ⦠| vδ δ ::= &bcirc; | &left;v · δ | &right;v · δ @@ -409,13 +414,13 @@ t ≤ s &Lrarrow; [t] ⊆ [s]Zippers (2/2)
fst (resp. snd) takes the first (resp. second) projection of a pair and update its zipper accordingly:
-v1 ⡠(1, (2, (3, (4, `nil))))&bcirc; - v11 ⡠fst v1 ⡠1&left;(1, (2, (3, (4, `nil))))&bcirc; · &bcirc; - v2 ⡠snd v1 ⡠(2, (3, (4, `nil)))&right;(1, (2, (3, (4, `nil))))&bcirc; · &bcirc; - v3 ⡠snd v2 ⡠(3, (4, `nil))&right;v2 · &right;v1 · &bcirc; +v1 ⡠(1, (2, (3, (4, `nil))))&bcirc; + v11 ⡠fst v1 ⡠1&left;(1, (2, (3, (4, `nil))))&bcirc; · &bcirc; + v2 ⡠snd v1 ⡠(2, (3, (4, `nil)))&right;(1, (2, (3, (4, `nil))))&bcirc; · &bcirc; + v3 ⡠snd v2 ⡠(3, (4, `nil))&right;v2 · &right;v1 · &bcirc;-up pops returns the head of the zipper:
-up v3 ⡠v2 ⡠(2, (3, (4, `nil)))&right;(1, (2, (3, (4, `nil))))&bcirc; · &bcirc; +up returns the head of the zipper:
+up v3 ⡠v2 ⡠(2, (3, (4, `nil)))&right;(1, (2, (3, (4, `nil))))&bcirc; · &bcirc;
t ::= ⦠| tτ τ ::= &bcirc; | &left;t · τ | &right;t · τ | τ &lor; τ | τ ∖ τ | &ztop;-
&bcirc;: singleton type denoting the empty zipper
- &ztop;: the top zipper types
- Zipper types are interpreted co-inductively (regular expressions on
- zippers)
- Int(&left;⊤)* &bcirc;: type of
- integers that are the leftmost descendant of a tree.
- [ [â¦] [â¦] ]]]>&bcirc;: type of
- HTML documents
- [ ⦠]]]>&ztop;: types of links in any context
-
+
&bcirc;: singleton type denoting the empty zipper (root element)
+ &ztop;: the top zipper type
+ Zipper types are interpreted co-inductively
+ Int(&left;⊤)* &bcirc; type of
+ integers that are the leftmost descendant of a tree
+ [ [â¦] [â¦] ]]]>&bcirc; type of
+ HTML documents
+ [ ⦠]]]> &ztop; types of links nested in any context
Since patterns contain types, we can check complex conditions:
-
- p â¡ <a>_ &lor; <_>[ _* p _* ]
+ Has a descendant <a>_:
+ p â¡ <a>_ &lor; <_>[ _* p _* ]
- τ â¡ &bcirc; &lor; &right;⊤ · τ &lor; &left;(⊤∖ <b>_) · τ
-
-
+ Deos not have an ancestor <b>_:
+ τ â¡ &bcirc; &lor; &right;(⊤∖ <b>_) · τ &lor; &left;(⊤∖ <b>_) · τ
match v with
pτ & x &rarrow; â¦
- | _ &rarrow; â¦
-
--We want more, namely return all descendants (ancestor, + | _ &rarrow; ⦠+
We want more, namely return all descendants (ancestors,
children, siblings, â¦) of a node matching a particular condition
Remark: (recursive) patterns already perform a recursive traversal
of the value
-
+
Idea: Piggy back on the traversal and accumulate
nodes in special variables
+v, v' &rleadsto;cons, (v, v')
v, `nil &rleadsto;snoc (v, `nil)
v, (v',v'') &rleadsto;snoc (v', snoc(v,v''))
@@ -495,19 +492,18 @@ nodes in special variables accumulates that node in sequence (in reverse or in-order).
- σ; δ ⊢ v / p &rleadsto; γ, σ' + σ ⊢ v / p &rleadsto; γ, σ'
σ, σ': mapping from accumulators to
- values
+ values. Initially: σ = { Ạ↦ Init(áº) | Ạ∈ p }
v: input value
p: pattern
γ: mapping from capture variables to
values
- δ: current context
Zippers (in values, types, patterns) are orthogonal to the rest of the language
+Zippers (in values, types, patterns) are a conservative extension
We use regular expressions over basic &left;/&right; zippers to encode XPath
- [ [
- []
- []
- [ [] ]
- ]
- ]]]>
-
- self :: t ⡠(Ạ& t | _ )&ztop; - child :: t ⡠<_>[ (Ạ& t | _ )* ]&ztop; - descendant-or-self:: t ⡠X ⡠((Ạ& t | _ ) & <_>[ X * ])&ztop; +Downward XPath axes
+self :: t â¡ (Ạ& t | _ )&ztop; (Init(áº) = [], Op(áº) = snoc) + + child :: t â¡ <_>[ (Ạ& t | _ )* ]&ztop; +
+Example: applying child::<b>_ to the document
+<doc>[ <a>[] <b>[] <c>[] <b>[] ]&bcirc; + <_>[ _ (Ạ& <b>_) _ (Ạ& <b>_)]&ztop; + + áº↦ [ <b>[]&left;⦠&right;⦠&right;⦠&bcirc; <b>[]&left;⦠&right;⦠&right;⦠&right;⦠&right;⦠&bcirc; ] +
+ ++ descendant-or-self:: t ⡠X ⡠((Ạ& t | _ ) & (<_>[ X * ])&ztop; | _ ) + descendant :: t ⡠<_>[ (descendant-or-self::t)* ]&ztop;
- parent :: t â¡ ⊤ (&left;_) · (&right;_)* · (&right; Ạ& t) · (( (&left; _) · &ztop;) &lor; &bcirc; ) - ancestor :: t â¡ ⊤ ((&left;_) · (&right;_)* · (&right; Ạ& t))* · &bcirc; +Binary-tree encoding
+We use regular expressions over basic &left;/&right; zippers to encode upward XPath
+[ [ +
[] + [] + [ [] ] + ] + ]]]> +
+ +
parent :: t â¡ ⊤ (&left;_) · (&right;_)* · (&right; Ạ& t) · (( (&left; _) · &ztop;) &lor; &bcirc; )
+
+ ancestor :: t â¡ ⊤ ( (&left;_) · (&right;_)* · (&right; Ạ& t) )* · &bcirc;
+
+
+
+
+
++ + ⬠⬠⬠⬠+ + parent + + +
Still some problems in the on-going implementation
+Thank you!