suzanne.soy/phc-graph
1
0
Fork 0
Code Issues 24 Pull Requests Actions Packages Projects Releases Wiki Activity

WIP on #62: Encoding of relations as types (≡, ∈, = length, < length) — finished most of the type-level encoding, fixed tests

Browse Source
This commit is contained in:
Georges Dupéron 2017-04-11 14:06:35 +02:00
parent 2ab2701789
commit 839bec824c
4 changed files with 194 additions and 136 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
Graph-notes-copy2.vue
View File

@ -1,14 +1,14 @@
<!-- Tufts VUE 3.3.0 concept-map (Graph-notes-copy2.vue) 2017-03-23 --> <!-- Tufts VUE 3.3.0 concept-map (Graph-notes-copy2.vue) 2017-04-11 -->
<!-- Tufts VUE: http://vue.tufts.edu/ --> <!-- Tufts VUE: http://vue.tufts.edu/ -->
<!-- Do Not Remove: VUE mapping @version(1.1) jar:file:/nix/store/z92y35qgs6g3cvvh0i4f14mg5n47zvvi-vue-3.3.0/share/vue/vue.jar!/tufts/vue/resources/lw_mapping_1_1.xml --> <!-- Do Not Remove: VUE mapping @version(1.1) jar:file:/nix/store/z92y35qgs6g3cvvh0i4f14mg5n47zvvi-vue-3.3.0/share/vue/vue.jar!/tufts/vue/resources/lw_mapping_1_1.xml -->
<!-- Do Not Remove: Saved date Thu Mar 23 01:54:28 CET 2017 by georges on platform Linux 4.4.40 in JVM 1.8.0_122-04 --> <!-- Do Not Remove: Saved date Tue Apr 11 14:04:44 CEST 2017 by georges on platform Linux 4.4.40 in JVM 1.8.0_122-04 -->
<!-- Do Not Remove: Saving version @(#)VUE: built October 8 2015 at 1724 by tomadm on Linux 2.6.32-504.23.4.el6.x86_64 i386 JVM 1.7.0_21-b11(bits=32) --> <!-- Do Not Remove: Saving version @(#)VUE: built October 8 2015 at 1724 by tomadm on Linux 2.6.32-504.23.4.el6.x86_64 i386 JVM 1.7.0_21-b11(bits=32) -->
<?xml version="1.0" encoding="US-ASCII"?> <?xml version="1.0" encoding="US-ASCII"?>
<LW-MAP xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" <LW-MAP xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
xsi:noNamespaceSchemaLocation="none" ID="0" xsi:noNamespaceSchemaLocation="none" ID="0"
label="Graph-notes-copy2.vue" created="1479309847604" x="0.0" label="Graph-notes-copy2.vue" created="1479309847604" x="0.0"
y="0.0" width="1.4E-45" height="1.4E-45" strokeWidth="0.0" autoSized="false"> y="0.0" width="1.4E-45" height="1.4E-45" strokeWidth="0.0" autoSized="false">
<resource referenceCreated="1490230468578" size="216025" <resource referenceCreated="1491912284366" size="216026"
spec="/home/georges/phc/racket-packages/phc-graph/Graph-notes-copy2.vue" spec="/home/georges/phc/racket-packages/phc-graph/Graph-notes-copy2.vue"
type="1" xsi:type="URLResource"> type="1" xsi:type="URLResource">
<title>Graph-notes-copy2.vue</title> <title>Graph-notes-copy2.vue</title>
@ -3914,7 +3914,7 @@
<URIString>http://vue.tufts.edu/rdf/resource/6dbf6b15c0a80026548592b8d2f3fee2</URIString> <URIString>http://vue.tufts.edu/rdf/resource/6dbf6b15c0a80026548592b8d2f3fee2</URIString>
</layer> </layer>
<userZoom>0.75</userZoom> <userZoom>0.75</userZoom>
<userOrigin x="-1182.522" y="-189.81644"/> <userOrigin x="-1182.522" y="-282.81644"/>
<presentationBackground>#FFFFFF</presentationBackground> <presentationBackground>#FFFFFF</presentationBackground>
<PathwayList currentPathway="0" revealerIndex="-1"> <PathwayList currentPathway="0" revealerIndex="-1">
<pathway ID="0" label="Chemin sans nom" created="1479309847603" <pathway ID="0" label="Chemin sans nom" created="1479309847603"

3
info.rkt
View File

@ -16,7 +16,8 @@
"remember" "remember"
"extensible-parser-specifications" "extensible-parser-specifications"
"subtemplate" "subtemplate"
"stxparse-info")) "stxparse-info"
"dotlambda"))
(define build-deps '("scribble-lib" (define build-deps '("scribble-lib"
"racket-doc" "racket-doc"
"remember" "remember"

116
invariants-phantom.hl.rkt
View File

@ -331,8 +331,10 @@ invariants, and therefore use a second nested function type to flip again the
variance direction. We always include the @racket[Or] element in the union, to variance direction. We always include the @racket[Or] element in the union, to
avoid ever having an empty union. avoid ever having an empty union.
@chunk[<Or>
(struct Or ())]
@chunk[<grouping-invariants> @chunk[<grouping-invariants>
(struct Or ())
(define-type-expander (Invariants stx) (define-type-expander (Invariants stx)
(syntax-case stx () (syntax-case stx ()
[(_ invᵢ …) [(_ invᵢ …)
@ -405,25 +407,6 @@ making a union of all paths, without factoring out common parts.
@chunk[<parse> @chunk[<parse>
(begin-for-syntax (begin-for-syntax
(define-syntax-class dot-ish
#:literals (dot λdot)
(pattern ({~and d dot} e …)
#:with full
(add-between (syntax->list #'(e …))
(datum->syntax #'d '|.| #'d #'d)))
(pattern ({~and d λdot} e …)
#:with full
(cons (datum->syntax #'d '|.| #'d #'d)
(add-between (syntax->list #'(e …))
(datum->syntax #'d '|.| #'d #'d)))))
(define-syntax ~dot-ish
(pattern-expander
(λ (stx)
(syntax-case stx ()
[(_ pat …)
#'(~and x:dot-ish
(~parse (pat …) #'x.full))]))))
(define (match-id rx id) (define (match-id rx id)
(let ([m (regexp-match rx (identifier→string id))]) (let ([m (regexp-match rx (identifier→string id))])
(and m (map (λ (%) (datum->syntax id (string->symbol %) id id)) (and m (map (λ (%) (datum->syntax id (string->symbol %) id id))
@ -445,25 +428,34 @@ making a union of all paths, without factoring out common parts.
#:attributes (τ) #:attributes (τ)
(pattern {~rx-id #px"^:([^:]+)$" τ})) (pattern {~rx-id #px"^:([^:]+)$" τ}))
(define-syntax-class π-elements (define-syntax-class π-elements
#:datum-literals (|.|) #:literals (#%dotted-id #%dot-separator)
#:attributes ([f 1] [τ 1]) #:attributes ([f 1] [τ 1])
(pattern (~dot-ish {~seq |.| :f+τ} …))) (pattern (#%dotted-id {~seq #%dot-separator :f+τ} …)))
(define-syntax-class extract-star
#:literals (* #%dotted-id)
(pattern (#%dotted-id {~and st *} . rest)
#:with {extracted-star …} #'{st (#%dotted-id . rest)})
(pattern other
#:with {extracted-star …} #'{other}))
(define-syntax-class sub-elements (define-syntax-class sub-elements
#:literals (*) #:datum-literals (|.|) #:literals (* #%dot-separator)
#:attributes ([f 2] [τ 2] [sub 1]) #:attributes ([f 2] [τ 2] [sub 1])
(pattern (pattern
({~either :π-elements {~seq sub:sub-elements *}} …))))] (:extract-star …)
#:with ({~either :π-elements {~seq sub:sub-elements *}} …)
#| |# #'(extracted-star … …))))]
@chunk[<parse> @chunk[<parse>
(define-type-expander (<~τ stx) (define-type-expander <~τ
(syntax-case stx () (syntax-parser
[(_ τ) #'τ] [(_ τ) #'τ]
[(_ f₀ . more) [(_ f₀ . more)
#'(f₀ (<~τ . more))])) #`(f₀ (<~τ . more))]))
(begin-for-syntax (begin-for-syntax
(define-template-metafunction generate-sub-π (define-template-metafunction generate-sub-π
(syntax-parser (syntax-parser
[(_ :sub-elements after) [(_ :sub-elements after)
#:with R (gensym 'R)
(template (template
(Rec R (Rec R
(U (<~τ (?? (∀ (more) (generate-sub-π sub more)) (U (<~τ (?? (∀ (more) (generate-sub-π sub more))
@ -476,14 +468,22 @@ making a union of all paths, without factoring out common parts.
after)))]))) after)))])))
(define-type-expander Π (define-type-expander Π
(syntax-parser (syntax-parser
[(_ {~optional (~dot-ish fst-τ:just-τ {~seq |.| fst:f+τ} …)} #:literals (#%dotted-id #%dot-separator)
[(_ {~optional (~or (#%dotted-id fst-τ:just-τ
{~seq #%dot-separator fst:f+τ} …)
(~and fst-τ:just-τ
{~parse (fst:f+τ …) #'()})
{~datum :})}
. :sub-elements) . :sub-elements)
(template (Rec R (U (Pairof Any R) #:with R (gensym 'R)
(List* (?? (?@ (Pairof AnyField fst-τ.τ) (template/top-loc
(Pairof (?? 'fst.f AnyField) this-syntax
(?? fst.τ AnyType)) (Rec R (U (Pairof Any R)
…)) (List* (?? (?@ (Pairof AnyField fst-τ.τ)
<π>))))]))] (Pairof (?? 'fst.f AnyField)
(?? fst.τ AnyType))
…))
<π>))))]))]
@chunk[<π> @chunk[<π>
(<~τ (?? (∀ (more) (generate-sub-π sub more)) (<~τ (?? (∀ (more) (generate-sub-π sub more))
@ -494,18 +494,31 @@ making a union of all paths, without factoring out common parts.
Null)] Null)]
@chunk[<Invariant> @chunk[<Invariant>
;; TODO: /top-loc everywhere
(define-type-expander Invariant (define-type-expander Invariant
(syntax-parser (syntax-parser
#:literals (≡ ≢ ∈ ∉ ∋ ∌) #:literals (≡ ≢ ∈ ∉ ∋ ∌)
;; For ≡ and ≢, use (U l r) because they are symmetric [(_ π₁ … ≡ π₂ …) #`(U (inv≡ (Pairof (Π π₁ …) (Π π₂ …)))
[(_ π₁ … ≡ π₂ …) #`(inv≡ (U (Π π₁ …) (Π π₂ …)))] (inv≡ (Pairof (Π π₂ …) (Π π₁ …))))]
[(_ π₁ … ≢ π₂ …) #`(inv≢ (U (Π π₁ …) (Π π₂ …)))] [(_ π₁ … ≢ π₂ …) #`(U (inv≢ (Pairof (Π π₁ …) (Π π₂ …)))
(inv≢ (Pairof (Π π₂ …) (Π π₁ …))))]
[(_ π₁ … ∈ π₂ …) #`(inv∈ (Pairof (Π π₁ …) (Π π₂ …)))] [(_ π₁ … ∈ π₂ …) #`(inv∈ (Pairof (Π π₁ …) (Π π₂ …)))]
[(_ π₁ … ∋ π₂ …) #`(inv∈ (Pairof (Π π₂ …) (Π π₁ …)))] [(_ π₁ … ∋ π₂ …) #`(inv∈ (Pairof (Π π₂ …) (Π π₁ …)))]
[(_ π₁ … ∉ π₂ …) #`(inv≢ (Pairof (Π π₁ …) (Π π₂ … ?)))] [(_ π₁ … ∉ π₂ …) #`(inv≢ (Pairof (Π π₁ …) (Π π₂ … ?)))]
[(_ π₁ … ∌ π₂ …) #`(inv≢ (Pairof (Π π₂ …) (Π π₁ … ?)))] [(_ π₁ … ∌ π₂ …) #`(inv≢ (Pairof (Π π₂ …) (Π π₁ … ?)))]
))] ))]
@chunk[<Invariants>
(define-type-expander Invariants
(syntax-parser
[(_ inv …)
#`(→ (U Or (Invariant . inv) …) Void)]))]
@chunk[<Any*>
(struct AnyField () #:transparent)
(struct AnyType () #:transparent)
(define-type ε (Π))]
@subsubsection{Comparison operator tokens} @subsubsection{Comparison operator tokens}
We define some tokens which will be used to identify the operator which We define some tokens which will be used to identify the operator which
@ -552,9 +565,6 @@ relates two nodes in the graph.
(struct (T) Target ([x : T]) #:transparent) (struct (T) Target ([x : T]) #:transparent)
(struct (T) NonTarget Target () #:transparent) (struct (T) NonTarget Target () #:transparent)
(struct AnyField () #:transparent)
(struct AnyType () #:transparent)
(define-type-expander Cycle (define-type-expander Cycle
(syntax-parser (syntax-parser
[(_ field:id … {~literal ↙} loop1:id … (target:id) loop2:id …) [(_ field:id … {~literal ↙} loop1:id … (target:id) loop2:id …)
@ -617,16 +627,23 @@ relates two nodes in the graph.
@subsection{Putting it all together} @subsection{Putting it all together}
@chunk[<*> @CHUNK[<*>
(require (for-syntax racket/base (require (only-in typed/dotlambda #%dotted-id #%dot-separator)
"dot-lang.rkt"
(for-syntax racket/base
racket/list racket/list
phc-toolkit/untyped phc-toolkit/untyped
syntax/parse syntax/parse
syntax/parse/experimental/template) syntax/parse/experimental/template)
(for-meta 2 racket/base) (for-meta 2 racket/base)
(for-meta 2 phc-toolkit/untyped/aliases) (for-meta 2 phc-toolkit/untyped/aliases)
(for-meta 3 racket/base) (for-meta 3 racket/base))
"dot-lang.rkt")
(begin-for-syntax
(define-syntax-rule (quasisyntax e)
(quasisyntax/top-loc this-syntax e))
(define-syntax-rule (template/top-loc loc e)
(quasisyntax/top-loc loc #,(template e))))
(provide ≡ ≢ ∈ ∉ ∋ ∌) (provide ≡ ≢ ∈ ∉ ∋ ∌)
@ -637,8 +654,8 @@ relates two nodes in the graph.
inv≡ inv≡
inv≢ inv≢
Or Or
Target ;Target
NonTarget ;NonTarget
ε ε
witness-value witness-value
Π Π
@ -649,8 +666,11 @@ relates two nodes in the graph.
<parse> <parse>
<witness-value> <witness-value>
<grouping-invariants> ;<grouping-invariants>
<cycles> ;<cycles>
<Any*>
<comparison-operators> <comparison-operators>
<Invariant> <Invariant>
<Invariants>
<Or>
<≡>] <≡>]

203
test/invariant-phantom/simple.rkt
View File

@ -1,4 +1,5 @@
#lang type-expander #lang typed/dotlambda
(require type-expander)
(require (lib "phc-graph/invariants-phantom.hl.rkt") (require (lib "phc-graph/invariants-phantom.hl.rkt")
"util.rkt" "util.rkt"
@ -6,122 +7,161 @@
phc-toolkit) phc-toolkit)
(check-same-type (check-same-type
(Π (λdot a aa) ((λdot b c))* (λdot d e)) (Π .a.aa(.b.c)*.d.e)
(Rec (Rec
R R1
(U (Pairof Any R) (U (Pairof Any R1)
(Pairof (Pairof
(Pairof 'a AnyType) (Pairof 'a AnyType)
(Pairof (Pairof
(Pairof 'aa AnyType) (Pairof 'aa AnyType)
(Rec (Rec
R R2
(U (Pairof (U (Pairof
(Pairof 'b AnyType) (Pairof 'b AnyType)
(Pairof (Pairof 'c AnyType) R)) (Pairof (Pairof 'c AnyType) R2))
(List (Pairof 'd AnyType) (Pairof 'e AnyType))))))))) (List (Pairof 'd AnyType) (Pairof 'e AnyType)))))))))
(struct a ()); the field.
(struct a ()); the node.
(struct b ()); the node.
(check-same-type (check-same-type
(Π (dot :a aa) ((λdot b c))* (λdot d e)) (Π :a.aa(.b.c)*.d.e)
(Rec (Rec
R R1
(U (Pairof Any R) (U (Pairof Any R1)
(Pairof (Pairof
(Pairof AnyField a) (Pairof AnyField a)
(Pairof (Pairof
(Pairof 'aa AnyType) (Pairof 'aa AnyType)
(Rec (Rec
R R2
(U (List (Pairof 'd AnyType) (Pairof 'e AnyType)) (U (List (Pairof 'd AnyType) (Pairof 'e AnyType))
(Pairof (Pairof 'b AnyType) (Pairof (Pairof 'c AnyType) R))))))))) (Pairof (Pairof 'b AnyType) (Pairof (Pairof 'c AnyType) R2)))))))))
(check-same-type (check-same-type
(Π (dot :a) ((λdot b c))* (λdot d e)) (Π :a(.b.c)*.d.e)
(Rec (Rec
R R1
(U (Pairof Any R) (U (Pairof Any R1)
(Pairof (Pairof
(Pairof AnyField a) (Pairof AnyField a)
(Rec (Rec
R R2
(U (List (Pairof 'd AnyType) (Pairof 'e AnyType)) (U (List (Pairof 'd AnyType) (Pairof 'e AnyType))
(Pairof (Pairof 'b AnyType) (Pairof (Pairof 'c AnyType) R)))))))) (Pairof (Pairof 'b AnyType) (Pairof (Pairof 'c AnyType) R2))))))))
(check-same-type (check-same-type
(Π (dot :a) ((λdot b c) ((λdot w)) * (λdot x y))* (λdot d e)) (Π :a(.b.c(.w)*.x.y)*.d.e)
(Rec (Rec
R R1
(U (Pairof Any R) (U (Pairof Any R1)
(Pairof (Pairof
(Pairof AnyField a) (Pairof AnyField a)
(U (List (Pairof 'd AnyType) (Pairof 'e AnyType)) (Rec
(Pairof R2
(Pairof 'b AnyType) (U (List (Pairof 'd AnyType) (Pairof 'e AnyType))
(Pairof (Pairof
(Pairof 'c AnyType) (Pairof 'b AnyType)
(Rec (Pairof
R (Pairof 'c AnyType)
(U (Pairof (Pairof 'w AnyType) R) (Rec
(Pairof R3
(Pairof 'x AnyType) (U (Pairof (Pairof 'w AnyType) R3)
(Pairof (Pairof 'y AnyType) R))))))))))) (Pairof
(Pairof 'x AnyType)
(Pairof (Pairof 'y AnyType) R2))))))))))))
;; TODO: test with deeper nesting of ()* ;; TODO: test with deeper nesting of ()*
(check-same-type (check-same-type
(Invariant (dot :a) ((λdot b c) ((λdot w)) * (λdot x y))* (λdot d e) (Invariant :a(.b.c(.w)*.x.y)*.d.e ≡ :a(.b.c)*.d.e)
≡ (U (inv≡
(dot :a) ((λdot b c))* (λdot d e)) (Pairof
(inv≡ (Rec
(U (Rec R1
R (U (Pairof Any R1)
(U (Pairof Any R) (Pairof
(Pairof (Pairof AnyField a)
(Pairof AnyField a) (Rec
(Rec R2
R (U (List (Pairof 'd AnyType) (Pairof 'e AnyType))
(U (List (Pairof 'd AnyType) (Pairof 'e AnyType)) (Pairof
(Pairof (Pairof 'b AnyType) (Pairof (Pairof 'c AnyType) R))))))) (Pairof 'b AnyType)
(Rec (Pairof (Pairof 'c AnyType) R2)))))))
R (Rec
(U (Pairof Any R) R1
(Pairof (U (Pairof Any R1)
(Pairof AnyField a) (Pairof
(U (List (Pairof 'd AnyType) (Pairof 'e AnyType)) (Pairof AnyField a)
(Pairof (Rec
(Pairof 'b AnyType) R2
(Pairof (U (List (Pairof 'd AnyType) (Pairof 'e AnyType))
(Pairof 'c AnyType) (Pairof
(Rec (Pairof 'b AnyType)
R (Pairof
(U (Pairof (Pairof 'w AnyType) R) (Pairof 'c AnyType)
(Pairof (Rec
(Pairof 'x AnyType) R3
(Pairof (Pairof 'y AnyType) R))))))))))))) (U (Pairof (Pairof 'w AnyType) R3)
(Pairof
(Pairof 'x AnyType)
(Pairof (Pairof 'y AnyType) R2)))))))))))))
(inv≡
(Pairof
(Rec
R1
(U (Pairof Any R1)
(Pairof
(Pairof AnyField a)
(Rec
R2
(U (List (Pairof 'd AnyType) (Pairof 'e AnyType))
(Pairof
(Pairof 'b AnyType)
(Pairof
(Pairof 'c AnyType)
(Rec
R3
(U (Pairof (Pairof 'w AnyType) R3)
(Pairof
(Pairof 'x AnyType)
(Pairof (Pairof 'y AnyType) R2)))))))))))
(Rec
R1
(U (Pairof Any R1)
(Pairof
(Pairof AnyField a)
(Rec
R2
(U (List (Pairof 'd AnyType) (Pairof 'e AnyType))
(Pairof
(Pairof 'b AnyType)
(Pairof (Pairof 'c AnyType) R2)))))))))))
(check-same-type (check-same-type
(Invariant (dot :a) ((λdot b c) ((λdot w)) * (λdot x y))* (λdot d e) (Invariant :a(.b.c(.w)*.x.y)*.d.e
∈ ∈
(dot :a) ((λdot b c))* (λdot d e)) :a(.b.c)*.d.e)
(Invariant (dot :a) ((λdot b c))* (λdot d e) (Invariant :a(.b.c)*.d.e
∋ ∋
(dot :a) ((λdot b c) ((λdot w)) * (λdot x y))* (λdot d e))) :a(.b.c(.w)*.x.y)*.d.e))
;;;
(check-ann witness-value (Invariants)) ;; No invariants (check-ann witness-value (Invariants)) ;; No invariants
(check-ann witness-value (Invariants (≡x (_ a) (_ a b c)))) (check-ann witness-value (Invariants (:a ≡ :a.b.c)))
(check-a-stronger-than-b (Invariants (≡x (_ a) (_ a b c))) (check-a-stronger-than-b (Invariants (:a ≡ :a.b.c))
(Invariants)) (Invariants))
(check-a-same-as-b (Invariants (:a ≡ :a.b.c))
(check-a-same-as-b (Invariants (≡x (_ a) (_ a b c))) (Invariants (:a.b.c ≡ :a)))
(Invariants (≡x (_ a b c) (_ a)))) (check-a-stronger-than-b (Invariants (: ≡ :b.c)
(: ≡ :b.d))
(check-a-stronger-than-b (Invariants (≡x (_) (_ b c)) (Invariants (: ≡ :b.c)))
(≡x (_) (_ b d))) (check-a-stronger-than-b (Invariants (: ≡ :b.d)
(Invariants (≡x (_) (_ b c)))) (: ≡ :b.c))
(check-a-stronger-than-b (Invariants (≡x (_) (_ b d)) (Invariants (: ≡ :b.c)))
(≡x (_) (_ b c)))
(Invariants (≡x (_) (_ b c))))
;; ∀ .b.d(.a.b.>d)* of length ≥ 5 ;; ∀ .b.d(.a.b.>d)* of length ≥ 5
;; is stronger than ;; is stronger than
@ -129,12 +169,9 @@
;; as the elements of the latter are included in the former, but ;; as the elements of the latter are included in the former, but
;; the first element (length = 5) is missing in the latter, so the ;; the first element (length = 5) is missing in the latter, so the
;; former constrains more paths. ;; former constrains more paths.
(check-a-stronger-than-b (Invariants (≡x (_) (check-a-stronger-than-b (Invariants (: ≡ .b.d(.a.b.d)*))
(_ b d ↙ a b (d)))) (Invariants (: ≡ .b.d.a.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-a-stronger-than-b (Invariants (≡x (_)
(_ a b c ↙ d (e))))
(Invariants (≡x (_)
(_ a b c d e))))