WIP on #62: Encoding of relations as types (≡, ∈, = length, < length)
This commit is contained in:
Georges Dupéron
parent
540e8a24b7
commit
2ab2701789
|
|
@ -178,9 +178,9 @@ a node with a weaker property is passed.
|
|||
@chunk[<structural-draft>
|
||||
(code:comment "Draft ideas")
|
||||
|
||||
(struct ∈ ())
|
||||
(struct ≡ ())
|
||||
(struct ∉ ())
|
||||
(struct inv∈ ())
|
||||
(struct inv≡ ())
|
||||
(struct inv∉ ())
|
||||
|
||||
;(List Rel From Path1 Path2)
|
||||
(List ≡ ANodeName (List f1 f2) (List))
|
||||
|
|
@ -465,7 +465,7 @@ making a union of all paths, without factoring out common parts.
|
|||
(syntax-parser
|
||||
[(_ :sub-elements after)
|
||||
(template
|
||||
(Rec R
|
||||
(Rec R
|
||||
(U (<~τ (?? (∀ (more) (generate-sub-π sub more))
|
||||
(∀ (more) (List* (Pairof (?? 'f AnyField)
|
||||
(?? τ AnyType))
|
||||
|
|
@ -474,10 +474,10 @@ making a union of all paths, without factoring out common parts.
|
|||
…
|
||||
R)
|
||||
after)))])))
|
||||
(define-for-syntax parse-path
|
||||
(define-type-expander Π
|
||||
(syntax-parser
|
||||
[({~optional (~dot-ish fst-τ:just-τ {~seq |.| fst:f+τ} …)}
|
||||
. :sub-elements)
|
||||
[(_ {~optional (~dot-ish fst-τ:just-τ {~seq |.| fst:f+τ} …)}
|
||||
. :sub-elements)
|
||||
(template (Rec R (U (Pairof Any R)
|
||||
(List* (?? (?@ (Pairof AnyField fst-τ.τ)
|
||||
(Pairof (?? 'fst.f AnyField)
|
||||
|
|
@ -493,6 +493,19 @@ making a union of all paths, without factoring out common parts.
|
|||
…
|
||||
Null)]
|
||||
|
||||
@chunk[<Invariant>
|
||||
(define-type-expander Invariant
|
||||
(syntax-parser
|
||||
#:literals (≡ ≢ ∈ ∉ ∋ ∌)
|
||||
;; For ≡ and ≢, use (U l r) because they are symmetric
|
||||
[(_ π₁ … ≡ π₂ …) #`(inv≡ (U (Π π₁ …) (Π π₂ …)))]
|
||||
[(_ π₁ … ≢ π₂ …) #`(inv≢ (U (Π π₁ …) (Π π₂ …)))]
|
||||
[(_ π₁ … ∈ π₂ …) #`(inv∈ (Pairof (Π π₁ …) (Π π₂ …)))]
|
||||
[(_ π₁ … ∋ π₂ …) #`(inv∈ (Pairof (Π π₂ …) (Π π₁ …)))]
|
||||
[(_ π₁ … ∉ π₂ …) #`(inv≢ (Pairof (Π π₁ …) (Π π₂ … ?)))]
|
||||
[(_ π₁ … ∌ π₂ …) #`(inv≢ (Pairof (Π π₂ …) (Π π₁ … ?)))]
|
||||
))]
|
||||
|
||||
@subsubsection{Comparison operator tokens}
|
||||
|
||||
We define some tokens which will be used to identify the operator which
|
||||
|
|
@ -501,9 +514,22 @@ relates two nodes in the graph.
|
|||
@chunk[<comparison-operators>
|
||||
(struct (A) inv≡ ([a : A]))
|
||||
(struct (A) inv≢ ([a : A]))
|
||||
;(struct inv∈ ()) ;; Can be expressed in terms of ≡
|
||||
(struct (A) inv∈ ([a : A]))
|
||||
;(struct inv∉ ()) ;; Can be expressed in terms of ≢
|
||||
]
|
||||
|
||||
(module literals typed/racket
|
||||
(define-syntax-rule (define-literals name ...)
|
||||
(begin
|
||||
(provide name ...)
|
||||
(define-syntax name
|
||||
(λ (stx)
|
||||
(raise-syntax-error 'name
|
||||
"Can only be used in special contexts"
|
||||
stx)))
|
||||
...))
|
||||
|
||||
(define-literals ≡ ≢ ∈ ∉ ∋ ∌))
|
||||
(require 'literals)]
|
||||
|
||||
@CHUNK[<≡>
|
||||
(define-for-syntax (relation inv)
|
||||
|
|
@ -518,8 +544,8 @@ relates two nodes in the graph.
|
|||
(Pairof (Cycle r-pre-b …)
|
||||
(Cycle post-b …))))]))
|
||||
|
||||
(define-type-expander ≡ (relation #'inv≡))
|
||||
(define-type-expander ≢ (relation #'inv≢))]
|
||||
(define-type-expander ≡x (relation #'inv≡))
|
||||
(define-type-expander ≢x (relation #'inv≢))]
|
||||
|
||||
@chunk[<cycles>
|
||||
(struct ε () #:transparent)
|
||||
|
|
@ -573,21 +599,21 @@ relates two nodes in the graph.
|
|||
@; elements of {a,x} × {b,c}, but we only want three out of these four.
|
||||
|
||||
@;{
|
||||
Two sorts of paths inside (in)equality constraints:
|
||||
Two sorts of paths inside (in)equality constraints:
|
||||
|
||||
@itemlist[
|
||||
@itemlist[
|
||||
@item{those anchored on a node, stating that
|
||||
@$${
|
||||
∀\ \textit{node} : \textit{NodeType},\quad
|
||||
\textit{node}.\textit{path}₁ ≡ \textit{node}.\textit{path}₂}}
|
||||
@$${
|
||||
∀\ \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}}}]
|
||||
}
|
||||
@$${
|
||||
\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}
|
||||
|
||||
|
|
@ -602,9 +628,12 @@ Two sorts of paths inside (in)equality constraints:
|
|||
(for-meta 3 racket/base)
|
||||
"dot-lang.rkt")
|
||||
|
||||
(provide ≡ ≢ ∈ ∉ ∋ ∌)
|
||||
|
||||
;; For testing:
|
||||
(provide Invariants
|
||||
≡
|
||||
≡x
|
||||
≢x
|
||||
inv≡
|
||||
inv≢
|
||||
Or
|
||||
|
|
@ -612,9 +641,10 @@ Two sorts of paths inside (in)equality constraints:
|
|||
NonTarget
|
||||
ε
|
||||
witness-value
|
||||
(for-syntax parse-path)
|
||||
Π
|
||||
AnyType
|
||||
AnyField)
|
||||
AnyField
|
||||
Invariant)
|
||||
|
||||
<parse>
|
||||
|
||||
|
|
@ -622,4 +652,5 @@ Two sorts of paths inside (in)equality constraints:
|
|||
<grouping-invariants>
|
||||
<cycles>
|
||||
<comparison-operators>
|
||||
<Invariant>
|
||||
<≡>]
|
||||
|
|
|
|||
|
|
@ -5,11 +5,6 @@
|
|||
phc-graph/dot-lang
|
||||
phc-toolkit)
|
||||
|
||||
(define-type-expander (Π stx)
|
||||
(syntax-case stx ()
|
||||
[(_ . π)
|
||||
(parse-path #'π)]))
|
||||
|
||||
(check-same-type
|
||||
(Π (λdot a aa) ((λdot b c))* (λdot d e))
|
||||
(Rec
|
||||
|
|
@ -70,23 +65,63 @@
|
|||
(Pairof 'x AnyType)
|
||||
(Pairof (Pairof 'y AnyType) R)))))))))))
|
||||
|
||||
#|
|
||||
;; TODO: test with deeper nesting of ()*
|
||||
|
||||
(check-same-type
|
||||
(Invariant (dot :a) ((λdot b c) ((λdot w)) * (λdot x y))* (λdot d e)
|
||||
≡
|
||||
(dot :a) ((λdot b c))* (λdot d e))
|
||||
(inv≡
|
||||
(U (Rec
|
||||
R
|
||||
(U (Pairof Any R)
|
||||
(Pairof
|
||||
(Pairof AnyField a)
|
||||
(Rec
|
||||
R
|
||||
(U (List (Pairof 'd AnyType) (Pairof 'e AnyType))
|
||||
(Pairof (Pairof 'b AnyType) (Pairof (Pairof 'c AnyType) R)))))))
|
||||
(Rec
|
||||
R
|
||||
(U (Pairof Any R)
|
||||
(Pairof
|
||||
(Pairof AnyField a)
|
||||
(U (List (Pairof 'd AnyType) (Pairof 'e AnyType))
|
||||
(Pairof
|
||||
(Pairof 'b AnyType)
|
||||
(Pairof
|
||||
(Pairof 'c AnyType)
|
||||
(Rec
|
||||
R
|
||||
(U (Pairof (Pairof 'w AnyType) R)
|
||||
(Pairof
|
||||
(Pairof 'x AnyType)
|
||||
(Pairof (Pairof 'y AnyType) R)))))))))))))
|
||||
|
||||
(check-same-type
|
||||
(Invariant (dot :a) ((λdot b c) ((λdot w)) * (λdot x y))* (λdot d e)
|
||||
∈
|
||||
(dot :a) ((λdot b c))* (λdot d e))
|
||||
(Invariant (dot :a) ((λdot b c))* (λdot d e)
|
||||
∋
|
||||
(dot :a) ((λdot b c) ((λdot w)) * (λdot x y))* (λdot d e)))
|
||||
|
||||
|
||||
(check-ann witness-value (Invariants)) ;; No invariants
|
||||
(check-ann witness-value (Invariants (≡ (_ a) (_ a b c))))
|
||||
(check-ann witness-value (Invariants (≡x (_ a) (_ a b c))))
|
||||
|
||||
(check-a-stronger-than-b (Invariants (≡ (_ a) (_ a b c)))
|
||||
(check-a-stronger-than-b (Invariants (≡x (_ a) (_ a b c)))
|
||||
(Invariants))
|
||||
|
||||
(check-a-same-as-b (Invariants (≡ (_ a) (_ a b c)))
|
||||
(Invariants (≡ (_ a b c) (_ a))))
|
||||
(check-a-same-as-b (Invariants (≡x (_ a) (_ a b c)))
|
||||
(Invariants (≡x (_ a b c) (_ a))))
|
||||
|
||||
(check-a-stronger-than-b (Invariants (≡ (_) (_ b c))
|
||||
(≡ (_) (_ b d)))
|
||||
(Invariants (≡ (_) (_ b c))))
|
||||
(check-a-stronger-than-b (Invariants (≡ (_) (_ b d))
|
||||
(≡ (_) (_ b c)))
|
||||
(Invariants (≡ (_) (_ b c))))
|
||||
(check-a-stronger-than-b (Invariants (≡x (_) (_ b c))
|
||||
(≡x (_) (_ b d)))
|
||||
(Invariants (≡x (_) (_ b c))))
|
||||
(check-a-stronger-than-b (Invariants (≡x (_) (_ b d))
|
||||
(≡x (_) (_ b c)))
|
||||
(Invariants (≡x (_) (_ b c))))
|
||||
|
||||
;; ∀ .b.d(.a.b.>d)* of length ≥ 5
|
||||
;; is stronger than
|
||||
|
|
@ -94,46 +129,12 @@
|
|||
;; as the elements of the latter are included in the former, but
|
||||
;; the first element (length = 5) is missing in the latter, so the
|
||||
;; former constrains more paths.
|
||||
(check-a-stronger-than-b (Invariants (≡ (_)
|
||||
(_ b d ↙ a b (d))))
|
||||
(Invariants (≡ (_)
|
||||
(_ b d a b d ↙ a b (d)))))
|
||||
(check-a-stronger-than-b (Invariants (≡x (_)
|
||||
(_ b d ↙ a b (d))))
|
||||
(Invariants (≡x (_)
|
||||
(_ b d a b d ↙ a b (d)))))
|
||||
|
||||
(check-a-stronger-than-b (Invariants (≡ (_)
|
||||
(_ a b c ↙ d (e))))
|
||||
(Invariants (≡ (_)
|
||||
(_ a b c d e))))
|
||||
|#
|
||||
|
||||
|
||||
(check-ann witness-value (Invariants)) ;; No invariants
|
||||
(check-ann witness-value (Invariants (≡ (_ a) (_ a b c))))
|
||||
|
||||
(check-a-stronger-than-b (Invariants (≡ (_ a) (_ a b c)))
|
||||
(Invariants))
|
||||
|
||||
(check-a-same-as-b (Invariants (≡ (_ a) (_ a b c)))
|
||||
(Invariants (≡ (_ a b c) (_ a))))
|
||||
|
||||
(check-a-stronger-than-b (Invariants (≡ (_) (_ b c))
|
||||
(≡ (_) (_ b d)))
|
||||
(Invariants (≡ (_) (_ b c))))
|
||||
(check-a-stronger-than-b (Invariants (≡ (_) (_ b d))
|
||||
(≡ (_) (_ b c)))
|
||||
(Invariants (≡ (_) (_ b c))))
|
||||
|
||||
;; ∀ .b.d(.a.b.>d)* of length ≥ 5
|
||||
;; is stronger than
|
||||
;; ∀ .b.d(.a.b.>d)* of length ≥ 8
|
||||
;; as the elements of the latter are included in the former, but
|
||||
;; the first element (length = 5) is missing in the latter, so the
|
||||
;; former constrains more paths.
|
||||
(check-a-stronger-than-b (Invariants (≡ (_)
|
||||
(_ b d ↙ a b (d))))
|
||||
(Invariants (≡ (_)
|
||||
(_ b d a b d ↙ a b (d)))))
|
||||
|
||||
(check-a-stronger-than-b (Invariants (≡ (_)
|
||||
(_ a b c ↙ d (e))))
|
||||
(Invariants (≡ (_)
|
||||
(_ a b c d e))))
|
||||
(check-a-stronger-than-b (Invariants (≡x (_)
|
||||
(_ a b c ↙ d (e))))
|
||||
(Invariants (≡x (_)
|
||||
(_ a b c d e))))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user