From 710c794a4411203cc3d668911a869cae0923b954 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Tue, 14 Apr 2015 00:58:53 +0200 Subject: [PATCH] . --- pres-esop15/01.xhtml | 159 +++++---- pres-esop15/rb_tree01.svg | 731 ++++++++++++++++++++++++++++++++++++++ pres-esop15/rb_tree02.svg | 728 +++++++++++++++++++++++++++++++++++++ pres-esop15/rb_tree03.svg | 728 +++++++++++++++++++++++++++++++++++++ pres-esop15/rb_tree04.svg | 728 +++++++++++++++++++++++++++++++++++++ 5 files changed, 3005 insertions(+), 69 deletions(-) create mode 100644 pres-esop15/rb_tree01.svg create mode 100644 pres-esop15/rb_tree02.svg create mode 100644 pres-esop15/rb_tree03.svg create mode 100644 pres-esop15/rb_tree04.svg diff --git a/pres-esop15/01.xhtml b/pres-esop15/01.xhtml index 845513e..6a41862 100644 --- a/pres-esop15/01.xhtml +++ b/pres-esop15/01.xhtml @@ -189,9 +189,9 @@

- 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

@@ -279,7 +279,7 @@ + compact (and efficient) type and value pattern-matching
  • Cons
    - - complex navigation encoded through recursion + - complex navigation encoded through recursion
    - no type inference for functions
    • @@ -290,44 +290,40 @@
    1. Add support for path navigation to &cduce; -

    &cduce;'s type algebra

    -    t ::=  b  |  c  |  t × t  |  t &rarrow; t  |  t &lor; t  |  t  &land; t  |  t ∖ t  |  ⊤  |  ⊥  |  α
+    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+ ]
    
+

    Semantic subtyping

    @@ -342,11 +338,23 @@ t ≤ s &Lrarrow; [t] ⊆ [s] [ Int* (Int | Bool*)? ] &land; [ Int+ (Bool+ | Int)* ] ≡ [Int+ Bool*]
    +
    +

    &cduce; data-model

    +

    The usual sets of values: constants, λ-abstractions, pairs, …

    +

    Sequences are nested pairs: [ v1 … vn ] ≡ (v1, (…, (vn, `nil))) +

    +

    XML documents are tagged sequences: 

    <foo>[ v1  … vn ] ≡ (`foo, [ v1  … vn ])
    +

    +

    (Sometimes we write [ ] for the variant `nil)

    +

    &cduce; patterns

    -
        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 @@ -381,24 +389,16 @@ t ≤ s &Lrarrow; [t] ⊆ [s]

    -
    -

    &cduce; data-model

    -

    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 ?)

    -
    +

    Zippers (1/2)

     v ::=  …  |  vδ
  δ ::=  &bcirc;  | &left;v · δ | &right;v · δ
@@ -414,7 +414,7 @@ t ≤ s   &Lrarrow;   [t] ⊆  [s]
     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 returns the head of the zipper: 

        up v3 ≡ v2 ≡ (2, (3, (4, `nil)))&right;(1, (2, (3, (4, `nil))))&bcirc; · &bcirc;
    @@ -424,15 +424,14 @@ t ≤ s &Lrarrow; [t] ⊆ [s] 
     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

    + [ … ]]]>(&right; ⊤) · &ztop; types of links in any context

    @@ -440,31 +439,27 @@ t ≤ s &Lrarrow; [t] ⊆ [s]

    Tree navigation

    Since patterns contain types, we can check complex conditions:

    -
    +
      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
 
    
-
 
 
    
   
    Operators and Accumulators
    
@@ -589,13 +584,21 @@ which is not a type.
    
 
    rb_tree
    
 
    
 
    
-
    Downward axes
    
-  [ [  []  [] [  [] ]   ]  ]]]>&bcirc;
-
-
    -     self :: t ≡    (ẋ & t | _ )&ztop;
-     child :: t ≡  <_>[ (ẋ & t | _ )* ]&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;
 
    
 
 
 
    
-
    Upward axes
    
-  [ [  []  [] [  [] ]   ]  ]]]>&bcirc;
-
-
    -     parent :: t ≡   ⊤ (&left;_) · (&right;_)* · (&right; ẋ & t) · (( (&left; _) · &ztop;)  &lor;  &bcirc; )
-     ancestor :: t ≡   ⊤ ((&left;_) · (&right;_)* · (&right; ẋ & t))* · &bcirc; 
+
    Upward XPath axes
    
+
    
+
+
+
+
+
+
+
         parent :: t ≡   ⊤ (&left;_) · (&right;_)* · (&right; ẋ & t) · (( (&left; _) · &ztop;)  &lor;  &bcirc; )
+                                             
+     ancestor :: t ≡   ⊤ ( (&left;_) · (&right;_)* · (&right; ẋ & t) )* · &bcirc; 
+
+
+
+
+
    
+
    +
+                               ⬆ ⬆     ⬆     ⬆
+
+                                                   parent         
+
+
+
 
    
 
 
    
diff --git a/pres-esop15/rb_tree01.svg b/pres-esop15/rb_tree01.svg
new file mode 100644
index 0000000..897df28
--- /dev/null
+++ b/pres-esop15/rb_tree01.svg
@@ -0,0 +1,731 @@
+
+
+
+
+  
+  
+    
+  
+  
+    
+      
+        image/svg+xml
+        
+        
+      
+    
+  
+  
+    
+    <>
+    
+    (,)
+    
+    
+    <>
+    
+    (,)
+    
+    
+    (,)
+    
+    
+    (,)
+    
+    <>
+    
+    <>
+    
+    <>
+    
+    
+    (,)
+    
+    <>
+    
+    
+    `nil
+    
+    `nil
+    
+    `nil
+    
+    `nil
+    
+    `nil
+    
+    `nil
+    
+    `a
+    `b
+    `c
+    `d
+    `e
+    `f
+    ⏺
+    L
+    L
+    L
+    L
+    L
+    L
+    L
+    L
+    L
+    L
+    L
+    R
+    R
+    R
+    R
+    R
+    R
+    R
+    R
+    R
+    R
+    R
+    
+  
+
diff --git a/pres-esop15/rb_tree02.svg b/pres-esop15/rb_tree02.svg
new file mode 100644
index 0000000..65b8263
--- /dev/null
+++ b/pres-esop15/rb_tree02.svg
@@ -0,0 +1,728 @@
+
+
+
+
+  
+  
+    
+  
+  
+    
+      
+        image/svg+xml
+        
+        
+      
+    
+  
+  
+    
+    <>
+    
+    (,)
+    
+    
+    <>
+    
+    (,)
+    
+    
+    (,)
+    
+    
+    (,)
+    
+    <>
+    
+    <>
+    
+    <>
+    
+    
+    (,)
+    
+    <>
+    
+    
+    `nil
+    
+    `nil
+    
+    `nil
+    
+    `nil
+    
+    `nil
+    
+    `nil
+    
+    `a
+    `b
+    `c
+    `d
+    `e
+    `f
+    ⏺
+    L
+    L
+    L
+    L
+    L
+    L
+    L
+    L
+    L
+    L
+    L
+    R
+    R
+    R
+    R
+    R
+    R
+    R
+    R
+    R
+    R
+    R
+    
+  
+
diff --git a/pres-esop15/rb_tree03.svg b/pres-esop15/rb_tree03.svg
new file mode 100644
index 0000000..0488b5e
--- /dev/null
+++ b/pres-esop15/rb_tree03.svg
@@ -0,0 +1,728 @@
+
+
+
+
+  
+  
+    
+  
+  
+    
+      
+        image/svg+xml
+        
+        
+      
+    
+  
+  
+    
+    <>
+    
+    (,)
+    
+    
+    <>
+    
+    (,)
+    
+    
+    (,)
+    
+    
+    (,)
+    
+    <>
+    
+    <>
+    
+    <>
+    
+    
+    (,)
+    
+    <>
+    
+    
+    `nil
+    
+    `nil
+    
+    `nil
+    
+    `nil
+    
+    `nil
+    
+    `nil
+    
+    `a
+    `b
+    `c
+    `d
+    `e
+    `f
+    ⏺
+    L
+    L
+    L
+    L
+    L
+    L
+    L
+    L
+    L
+    L
+    L
+    R
+    R
+    R
+    R
+    R
+    R
+    R
+    R
+    R
+    R
+    R
+    
+  
+
diff --git a/pres-esop15/rb_tree04.svg b/pres-esop15/rb_tree04.svg
new file mode 100644
index 0000000..97e31ea
--- /dev/null
+++ b/pres-esop15/rb_tree04.svg
@@ -0,0 +1,728 @@
+
+
+
+
+  
+  
+    
+  
+  
+    
+      
+        image/svg+xml
+        
+        
+      
+    
+  
+  
+    
+    <>
+    
+    (,)
+    
+    
+    <>
+    
+    (,)
+    
+    
+    (,)
+    
+    
+    (,)
+    
+    <>
+    
+    <>
+    
+    <>
+    
+    
+    (,)
+    
+    <>
+    
+    
+    `nil
+    
+    `nil
+    
+    `nil
+    
+    `nil
+    
+    `nil
+    
+    `nil
+    
+    `a
+    `b
+    `c
+    `d
+    `e
+    `f
+    ⏺
+    L
+    L
+    L
+    L
+    L
+    L
+    L
+    L
+    L
+    L
+    L
+    R
+    R
+    R
+    R
+    R
+    R
+    R
+    R
+    R
+    R
+    R
+    
+  
+
-- 
2.17.1