From fb1786b4ac5f94f1fa9f0607ec2fb004be0419dd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Mon, 16 Jan 2017 03:11:16 +0100 Subject: [PATCH] More work on the invariants --- .gitignore | 1 + Graph-notes-copy2.vue | 150 ++++++++++++++++++++-------- alpha-equivalence-normal-form.rkt | 79 +++++++++++++++ bench001.rkt | 32 ++++++ flexible-with-utils.hl.rkt | 6 +- flexible-with.hl.rkt | 2 +- graph-info.rkt => graph-info.hl.rkt | 0 invariants-phantom.hl.rkt | 132 ++++++++++++++++++++---- thoughts.rkt | 124 +++++++++++++++++++++++ traversal.hl.rkt | 2 +- 10 files changed, 462 insertions(+), 66 deletions(-) create mode 100644 alpha-equivalence-normal-form.rkt create mode 100644 bench001.rkt rename graph-info.rkt => graph-info.hl.rkt (100%) create mode 100644 thoughts.rkt diff --git a/.gitignore b/.gitignore index 1a59348..33ed4b8 100644 --- a/.gitignore +++ b/.gitignore @@ -4,3 +4,4 @@ .DS_Store compiled/ /doc/ +/.~*.vue \ No newline at end of file diff --git a/Graph-notes-copy2.vue b/Graph-notes-copy2.vue index bb8ee4c..fc34995 100644 --- a/Graph-notes-copy2.vue +++ b/Graph-notes-copy2.vue @@ -1,14 +1,14 @@ - + - + - Graph-notes-copy2.vue @@ -314,9 +314,9 @@ 36 + width="681.0" height="23.0" strokeWidth="1.0" autoSized="true" xsi:type="node"> #F2AE45 #776D6D #000000 @@ -988,7 +988,7 @@ - #C1F780 + #FFFFFF #D0D0D0 #000000 SansSerif-plain-12 @@ -1352,9 +1352,9 @@ 11 241 - + width="184.0" height="23.0" strokeWidth="1.0" autoSized="true" xsi:type="node"> #A6A6A6 #776D6D #000000 @@ -1362,21 +1362,21 @@ http://vue.tufts.edu/rdf/resource/6e0b664b43a6be970d2ffe25608d7f84 - #000000 #404040 SansSerif-plain-11 http://vue.tufts.edu/rdf/resource/6e0b664b43a6be970d2ffe252aafd35e - - + + 11 244 #A6A6A6 #776D6D @@ -1385,22 +1385,22 @@ http://vue.tufts.edu/rdf/resource/6e0b664c43a6be970d2ffe253b42a8fa - #000000 #404040 SansSerif-plain-11 http://vue.tufts.edu/rdf/resource/6e0b664c43a6be970d2ffe25426d76fa - - + + 244 246 #F2AE45 #776D6D @@ -1409,16 +1409,15 @@ http://vue.tufts.edu/rdf/resource/6e12548843a6be970d2ffe259bb5e939 - + #000000 #404040 SansSerif-plain-11 http://vue.tufts.edu/rdf/resource/6e12548843a6be970d2ffe25f25ed174 - - + + 23 252 @@ -1475,7 +1474,7 @@ - #FFFFFF + #C1F780 #D0D0D0 #000000 SansSerif-plain-12 @@ -1699,7 +1698,7 @@ label="Each node has an extra field of the following type: " layerID="1" created="1479317112254" x="-826.86255" y="972.24475" width="339.0" height="107.0" strokeWidth="1.0" autoSized="true" xsi:type="node"> - #F2AE45 + #C1F780 #776D6D #000000 SansSerif-plain-12 @@ -1760,7 +1759,7 @@ label="Use a private struct to prevent forging of the invariants aggregated in a case→ (since it is never executed, any non-terminating λ could otherwise be supplied). " layerID="1" created="1479317202233" x="-960.86255" y="1145.7448" width="531.0" height="77.0" strokeWidth="1.0" autoSized="true" xsi:type="node"> - #F2AE45 + #C1F780 #776D6D #000000 SansSerif-plain-12 @@ -1814,7 +1813,7 @@ label="graph invariants should only define the dummy type used to identify them" layerID="1" created="1479317586757" x="-968.86255" y="1282.7448" width="611.0" height="172.25" strokeWidth="1.0" autoSized="true" xsi:type="node"> - #F2AE45 + #C1F780 #776D6D #000000 SansSerif-plain-12 @@ -1902,7 +1901,7 @@ label="The returned type may contain symbols, to indicate node names and field names, and will contain a reference to a private struct type, so that two invariants with the same name defined in separate won't conflict" layerID="1" created="1479317996531" x="-1558.8625" y="1375.2448" width="543.0" height="53.0" strokeWidth="1.0" autoSized="true" xsi:type="node"> - #F2AE45 + #C1F780 #776D6D #000000 SansSerif-plain-12 @@ -2175,7 +2174,7 @@ 353 #A6A6A6 #776D6D @@ -2184,15 +2183,16 @@ http://vue.tufts.edu/rdf/resource/6f9963d1c0a80026616d9239f16e4b43 - + #404040 #404040 SansSerif-plain-11 http://vue.tufts.edu/rdf/resource/6f9963d1c0a80026616d923937836369 - - + + 353 355 @@ -2345,7 +2345,7 @@ label="What about invariants? * Just copy them over syntactically? * Require that they are re-specified (at least by explicitly copying them by their name)" layerID="1" created="1479346589797" x="788.9707" y="332.74475" width="329.0" height="68.0" strokeWidth="1.0" autoSized="true" xsi:type="node"> - #DD7B11 + #F2AE45 #776D6D #000000 SansSerif-plain-12 @@ -2628,7 +2628,7 @@ #000000 @@ -2636,7 +2636,7 @@ SansSerif-plain-11 http://vue.tufts.edu/rdf/resource/72688d2cc0a8002633539faacb736715 - + 25 42 @@ -3470,7 +3470,7 @@ 512 #FC938D @@ -3708,12 +3708,82 @@ 103 535 + + #E6F7FD + #776D6D + #000000 + SansSerif-plain-12 + http://vue.tufts.edu/rdf/resource/a46d8f60c0a801286acbb58b97c6fd0a + + + + #404040 + #404040 + SansSerif-plain-11 + http://vue.tufts.edu/rdf/resource/a46d8f61c0a801286acbb58b996c697e + + + 393 + 538 + + + #F2AE45 + #776D6D + #000000 + SansSerif-plain-12 + http://vue.tufts.edu/rdf/resource/a46d8f61c0a801286acbb58b2b628a00 + + + + #404040 + #404040 + SansSerif-plain-11 + http://vue.tufts.edu/rdf/resource/a46d8f62c0a801286acbb58b19d6b212 + + + 353 + 540 + + + #F2AE45 + #776D6D + #000000 + SansSerif-plain-12 + http://vue.tufts.edu/rdf/resource/a46d8f62c0a801286acbb58beacd7655 + + + + #404040 + #404040 + SansSerif-plain-11 + http://vue.tufts.edu/rdf/resource/a46d8f62c0a801286acbb58b90bacc82 + + + 540 + 542 + http://vue.tufts.edu/rdf/resource/6dbf6b15c0a80026548592b8d2f3fee2 1.0 - + #FFFFFF (struct InvWeak ()) @@ -336,7 +336,8 @@ having an empty union. (define-type-expander (Invariants stx) (syntax-case stx () [(_ invᵢ …) - #'(→ (U Or (→ invᵢ Void) …) Void)]))] + #'(→ (U Or (→ invᵢ Void) …) Void) + #;#'(→ (→ (∩ invᵢ …) Void) Void)]))] @subsection{Structural (in)equality and (non-)membership invariants} @@ -346,20 +347,87 @@ We define some tokens which will be used to identify the operator which relates two nodes in the graph. @chunk[ - (struct (A B) inv≡ ([a : A] [b : B])) - (struct (A B) inv≢ ([a : A] [b : B])) + (struct (A) inv≡ ([a : A])) + (struct (A) inv≢ ([a : A])) ;(struct inv∈ ()) ;; Can be expressed in terms of ≡ ;(struct inv∉ ()) ;; Can be expressed in terms of ≢ ] -@chunk[<≡> - (define-type-expander (≡ stx) - (syntax-case stx () - [(_ (patha ...) (pathb ...)) - ;; TODO: probably not just List here, have to think. - #'(inv≡ (List 'patha ...) (List 'pathb ...))]))] +@CHUNK[<≡> + (define-for-syntax (relation inv) + (syntax-parser + [(_ (pre-a … {~literal _} post-a …) + (pre-b … {~literal _} post-b …)) + #:with (r-pre-a …) (reverse (syntax->list #'(pre-a …))) + #:with (r-pre-b …) (reverse (syntax->list #'(pre-b …))) + ;; Use U to make it order-independent + #`(#,inv (U (Pairof (Cycle r-pre-a …) + (Cycle post-a …)) + (Pairof (Cycle r-pre-b …) + (Cycle post-b …))))])) -@; TODO: don't forget to include both directions a = b and b = a (or sort the fields?) + (define-type-expander ≡ (relation #'inv≡)) + (define-type-expander ≢ (relation #'inv≢))] + +@chunk[ + (struct ε () #:transparent) + (struct (T) Target () #:transparent) + (struct (T) NonTarget Target ([x : T]) #:transparent) + + (define-type-expander Cycle + (syntax-parser + [(_ field:id … {~literal ↙} loop1:id … (target:id) loop2:id …) + #'(List* (NonTarget ε) + (NonTarget 'field) … + (Rec R (List* (NonTarget 'loop1) … ;(NonTarget 'loop1) … + (Target 'target) ;(NonTarget 'target) + (NonTarget 'loop2) … ;(NonTarget 'loop2) … + R)))] + [(_ field … target) + ;; TODO: something special at the end? + #'(List (NonTarget ε) (NonTarget 'field) … (Target 'target))] + [(_) + #'(List (Target ε))]))] + +@;{@[ + + ;.a.b = .x.y + ;(l1=a ∧ l2=b ∧ r1=x ∧ r2=y) ⇒ eq + ;¬(l1=a ∧ l2=b ∧ r1=x ∧ r2=y) ∨ eq + ;¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=y ∨ eq + + ;.a.c = .x.y + ;(l1=a ∧ l2=c ∧ r1=x ∧ r2=y) ⇒ eq + + ;.a.c = .x.z + ;(l1=a ∧ l2=b ∧ r1=x ∧ r2=z) ⇒ eq + ;¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=z ∨ eq + + + ;.a.b = .x.y ∧ .a.c = .x.z + ;(¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=y ∨ eq) ∧ (¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=z ∨ eq) + ;¬¬(¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=y ∨ eq) ∧ (¬l1=a ∨ ¬l2=b ∨ ¬r1=x ∨ ¬r2=z ∨ eq) + ;¬(l1=a ∧ l2=b ∧ r1=x ∧ r2=y ∧ eq) ∨ (l1=a ∧ l2=b ∧ r1=x ∧ r2=z ∧ ¬eq) + ]} + +@; Problem with ∩: it factors out too much, (∩ '(a . b) '(a . c) '(x . b)) +@; becomes (Pairof (∩ 'a 'x) (∩ 'b 'c)), which is equivalent to have all four +@; elements of {a,x} × {b,c}, but we only want three out of these four. + +Two sorts of paths inside (in)equality constraints: + +@itemlist[ + @item{those anchored on a node, stating that + @$${ + ∀\ \textit{node} : \textit{NodeType},\quad + \textit{node}.\textit{path}₁ ≡ \textit{node}.\textit{path}₂}} + @item{those not anchored on a node, stating that + @$${ + \begin{array}{c} + ∀\ \textit{node}₁ : \textit{NodeType}₁,\quad + ∀\ \textit{node}₂ : \textit{NodeType}₂,\\ + \textit{node}₁.\textit{path}₁ ≡ \textit{node}₂.\textit{path}₂ + \end{array}}}] @subsection{Putting it all together} @@ -369,27 +437,47 @@ relates two nodes in the graph. [(_ stronger weaker) (syntax/top-loc stx (check-ann (ann witness-value stronger) - weaker))]))] + weaker))])) + + (define-syntax (check-a-same-b stx) + (syntax-case stx () + [(_ a b) + (syntax/top-loc stx + (begin + (check-ann (ann witness-value a) b) + (check-ann (ann witness-value b) a)))]))] @chunk[<*> - (require (for-syntax phc-toolkit)) + (require (for-syntax phc-toolkit/untyped + syntax/parse)) + <≡> (module+ test (require phc-toolkit) - - (ann witness-value (Invariants)) ;; No invariants - (ann witness-value (Invariants (≡ (a) (a b c)))) - (check-a-stronger-or-same-b (Invariants (≡ (a) (a b c))) + (ann witness-value (Invariants)) ;; No invariants + (ann witness-value (Invariants (≡ (_ a) (_ a b c)))) + + (check-a-stronger-or-same-b (Invariants (≡ (_ a) (_ a b c))) (Invariants)) - (check-a-stronger-or-same-b (Invariants (≡ (a) (a b c)) (≡ (a) (a b d))) - (Invariants (≡ (a) (a b c)))) - (check-a-stronger-or-same-b (Invariants (≡ (a) (a b d)) (≡ (a) (a b c))) - (Invariants (≡ (a) (a b c)))))] + (check-a-same-b (Invariants (≡ (_ a) (_ a b c))) + (Invariants (≡ (_ a b c) (_ a)))) + + (check-a-stronger-or-same-b (Invariants (≡ (_) (_ b c)) + (≡ (_) (_ b d))) + (Invariants (≡ (_) (_ b c)))) + (check-a-stronger-or-same-b (Invariants (≡ (_) (_ b d)) + (≡ (_) (_ b c))) + (Invariants (≡ (_) (_ b c)))) + + (check-a-stronger-or-same-b (Invariants (≡ (_) + (_ b d a b d ↙ a b (d)))) + (Invariants (≡ (_) + (_ b d ↙ a b (d))))))] diff --git a/thoughts.rkt b/thoughts.rkt new file mode 100644 index 0000000..e265ef2 --- /dev/null +++ b/thoughts.rkt @@ -0,0 +1,124 @@ +#lang type-expander/lang + +#| +Adding fields to the prefix path makes it weaker +Adding fields to the postfix path makes it stronger + +(Expand prefix postfix) +=> (and prefixᵢ postfix) … +Also could be expanded as: +=> (and prefix postfixᵢ) … + +Rewording ((u pre_x pre_x2) pre_a _ post_b (u post_c post_c2) +=> property holds iff + pre1 = a + and (pre2 = x or pre2 = x2) + and post1 = b + and (post2 = c or post2 = c2) +|# + +(define-type (F A) (I (I A))) +(define-type (I A) (→ A Void)) + +(define-type eqA1 (F (Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u1) (G 'u2))) + (List (G 'b) (G 'c))))) + +(define-type eqB1 (F (∩ (Pairof (List* (G 'a1) (∩ (G 'u1) (G 'u2))) + (List (G 'b) (G 'c))) + (Pairof (List* (G 'a2) (∩ (G 'u1) (G 'u2))) + (List (G 'b) (G 'c)))))) + +(define-type eqC1 (F (∩ (Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u1))) + (List (G 'b) (G 'c))) + (Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u2))) + (List (G 'b) (G 'c)))))) + +(define-type weakerD1 (F (∩ (Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u1))) + (List (G 'b) (G 'c)))))) + +(define-type strongerE1 (F (∩ (Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u1) (G 'u2))) + (∩ (List (G 'b) (G 'c)) + (List (G 'b2) (G 'c))))))) + +(define-type strongerF1 (F (∩ (Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u1) (G 'u2))) + (Pairof (G 'b) (∩ (List (G 'c)) + (List (G 'c2)))))))) + +(define-type altF1 (F (∩ (Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u1) (G 'u2))) + (Pairof (G 'b) (List (G 'c)))) + (Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u1) (G 'u2))) + (Pairof (G 'b) (List (G 'c2))))))) + +(ann (ann (λ (x) (void)) eqA1) eqB1) +(ann (ann (λ (x) (void)) eqA1) eqC1) +(ann (ann (λ (x) (void)) eqB1) eqA1) +(ann (ann (λ (x) (void)) eqB1) eqC1) +(ann (ann (λ (x) (void)) eqC1) eqA1) +(ann (ann (λ (x) (void)) eqC1) eqB1) +(ann (ann (λ (x) (void)) eqA1) weakerD1) +(ann (ann (λ (x) (void)) eqB1) weakerD1) +(ann (ann (λ (x) (void)) eqC1) weakerD1) +;(ann (ann (λ (x) (void)) eqA1) strongerD1) ;; rejected, as it should +(ann (ann (λ (x) (void)) strongerE1) eqA1) +;(ann (ann (λ (x) (void)) eqA1) strongerE1) ;; rejected, as it should +(ann (ann (λ (x) (void)) strongerF1) eqA1) +;(ann (ann (λ (x) (void)) eqA1) strongerF1) ;; rejected, as it should +(ann (ann (λ (x) (void)) altF1) eqA1) +;(ann (ann (λ (x) (void)) eqA1) altF1) ;; rejected, as it should +(ann (ann (λ (x) (void)) altF1) strongerF1) +(ann (ann (λ (x) (void)) strongerF1) altF1) + + + + +(let () + (define-type eqA2 (F (case→ (→ (List 'b 'c) 'a1) + (→ (List 'b 'c) 'a2)))) + + (define-type eqB2 (F (case→ (→ (List 'b 'c) + (U 'a1 'a2))))) + + (ann (ann (λ (x) (void)) eqA2) eqB2) + #;(ann (ann (λ (x) (void)) eqB2) eqA2)) + +;(let () +(define-type (G A) (F A)) +(define-type-expander (+ stx) (syntax-case stx () [(_ . rest) #'(∩ . rest)])) +(define-type-expander (* stx) (syntax-case stx () [(_ . rest) #'(U . rest)])) + +(define-type eqA2 (F (+ (* (G 'b) (G 'c) (G 'a1)) + (* (G 'b) (G 'c) (G 'a2))))) + +(define-type eqB2 (F (+ (* (G 'b) (G 'c) (+ (G 'a1) (G 'a2)))))) + +(define-type Weaker2 (F (+ (* (G 'b) (G 'c) (G 'a1))))) + +(ann (ann (λ (x) (void)) eqA2) eqB2) +(ann (ann (λ (x) (void)) eqB2) eqA2) +(ann (ann (λ (x) (void)) eqA2) Weaker2) +(ann (ann (λ (x) (void)) eqB2) Weaker2) +;(ann (ann (λ (x) (void)) Weaker2) eqA2) +;(ann (ann (λ (x) (void)) Weaker2) eqB2) +;) + + + +(let () + (define-type weaker3 + (F (∩ (G (Rec R (List* 'a Any R))) + (G (Rec R (List* Any 'b R)))))) + (define-type stronger3 + (F (∩ (G (List* 'a Any (Rec R (List* 'a Any R)))) + (G (List* Any 'b (Rec R (List* Any 'b R))))))) + + (ann (ann (λ (x) (void)) stronger3) weaker3) + ) + +#| +Put the U ∩ inside the positional list? +What about loops of different sizes => won't work +What about merging all the invariants blindly => won't work, but we can +special-case merging these regexp-like invariants, as long as the merging +doesn't need any info about the regexp itself +(e.g. all are "merge the second elements") +|# \ No newline at end of file diff --git a/traversal.hl.rkt b/traversal.hl.rkt index e30c789..bff6c0e 100644 --- a/traversal.hl.rkt +++ b/traversal.hl.rkt @@ -25,7 +25,7 @@ @title[#:style manual-doc-style #:tag "traversal" #:tag-prefix "phc-graph/traversal"]{Parametric replacement of parts of - data structures, identified by their type} + data structures} @(chunks-toc-prefix '("(lib phc-graph/scribblings/phc-graph-implementation.scrbl)"