X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;ds=sidebyside;f=pres-esop15%2F01.xhtml;h=d74a138f9aa51439db6ede4a8f36c5566ff6e5b1;hb=564cbcc2c27a723d2bdf12cf690a66eb7f36b813;hp=6a41862198f612ce45c0308b66e0e81d442554a7;hpb=710c794a4411203cc3d668911a869cae0923b954;p=hacks%2FsimpleWebSlides.git diff --git a/pres-esop15/01.xhtml b/pres-esop15/01.xhtml index 6a41862..d74a138 100644 --- a/pres-esop15/01.xhtml +++ b/pres-esop15/01.xhtml @@ -14,8 +14,8 @@ - - + Empty" > + Any" > @@ -196,25 +196,25 @@
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 @@ -340,12 +341,16 @@ t ≤ s &Lrarrow; [t] ⊆ [s]
The usual sets of values: constants, λ-abstractions, pairs, â¦
-Sequences are nested pairs: [ v1 ⦠vn ] â¡ (v1, (â¦, (vn, `nil))) -
+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
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 returns the head of the zipper:
-up v3 ⡠v2 ⡠(2, (3, (4, `nil)))&right;(1, (2, (3, (4, `nil))))&bcirc; · &bcirc; +up v3 ⡠v2 ⡠(2, (3, (4, `nil)))&right;(1, (2, (3, (4, `nil))))&bcirc; · &bcirc;
Since patterns contain types, we can check complex conditions:
-Has a descendant <a>_: - p â¡ <a>_ &lor; <_>[ _* p _* ] +Has a descendant <a>_: + p â¡ <a>_ &lor; <_>[ _* p _* ] Deos not have an ancestor <b>_: - τ â¡ &bcirc; &lor; &right;(⊤∖ <b>_) · τ &lor; &left;(⊤∖ <b>_) · τ - -+ τ â¡ &bcirc; &lor; &right;(⊤∖ <b>_) · τ &lor; &left;(⊤∖ <b>_) · τ
match v with
pτ & x &rarrow; â¦
@@ -480,7 +482,7 @@ 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''))
@@ -490,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; (Init(áº) = [], Op(áº) = snoc) @@ -597,7 +587,7 @@ which is not a type.- descendant-or-self:: t â¡ X â¡ ((Ạ& t | _ ) & <_>[ X * ])&ztop; + descendant-or-self:: t â¡ X â¡ ((Ạ& t | _ ) & (<_>[ X * ])&ztop; | _ ) descendant :: t â¡ <_>[ (descendant-or-self::t)* ]&ztop;@@ -641,6 +631,19 @@ which is not a type. -->
We use regular expressions over basic &left;/&right; zippers to encode upward XPath
+ [ [
+ []
+ []
+ [ [] ]
+ ]
+ ]]]>
+
- ⬠⬠⬠⬠+ ⬠⬠⬠⬠- parent + parent @@ -672,21 +675,26 @@ which is not a type.Other results
Still some problems in the on-going implementation
+Thank you!