From 37120eec9cd6fddbcab46a42d84598e5afa3b958 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Tue, 11 Apr 2017 22:06:16 +0200 Subject: [PATCH] =?UTF-8?q?Closes=20#62:=20Encoding=20of=20relations=20as?= =?UTF-8?q?=20types=20(=E2=89=A1,=20=E2=88=88,=20=3D=20length,=20<=20lengt?= =?UTF-8?q?h)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- invariants-phantom.hl.rkt | 80 ++++++++++++++++++-------- test/invariant-phantom/simple.rkt | 94 ++++++++++--------------------- 2 files changed, 85 insertions(+), 89 deletions(-) diff --git a/invariants-phantom.hl.rkt b/invariants-phantom.hl.rkt index 43400a9..bc25177 100644 --- a/invariants-phantom.hl.rkt +++ b/invariants-phantom.hl.rkt @@ -423,7 +423,8 @@ making a union of all paths, without factoring out common parts. #:attributes (f τ) (pattern {~rx-id #px"^([^:]+):([^:]+)$" f τ}) (pattern {~rx-id #px"^([^:]+)$" f} #:with ({~optional τ}) #'()) - (pattern {~rx-id #px"^:([^:]+)$" τ} #:with ({~optional f}) #'())) + (pattern {~rx-id #px"^:([^:]+)$" τ} #:with ({~optional f}) #'()) + (pattern {~rx-id #px"^:$"} #:with ({~optional (f τ)}) #'())) (define-syntax-class just-τ #:attributes (τ) (pattern {~rx-id #px"^:([^:]+)$" τ})) @@ -471,9 +472,9 @@ making a union of all paths, without factoring out common parts. #:literals (#%dotted-id #%dot-separator) [(_ {~optional (~or (#%dotted-id fst-τ:just-τ {~seq #%dot-separator fst:f+τ} …) + {~datum :} (~and fst-τ:just-τ - {~parse (fst:f+τ …) #'()}) - {~datum :})} + {~parse (fst:f+τ …) #'()}))} . :sub-elements) #:with R (gensym 'R) (template/top-loc @@ -494,19 +495,51 @@ making a union of all paths, without factoring out common parts. Null)] @chunk[ - ;; TODO: /top-loc everywhere (define-type-expander Invariant (syntax-parser - #:literals (≡ ≢ ∈ ∉ ∋ ∌) - [(_ π₁ … ≡ π₂ …) #`(U (inv≡ (Pairof (Π π₁ …) (Π π₂ …))) - (inv≡ (Pairof (Π π₂ …) (Π π₁ …))))] - [(_ π₁ … ≢ π₂ …) #`(U (inv≢ (Pairof (Π π₁ …) (Π π₂ …))) - (inv≢ (Pairof (Π π₂ …) (Π π₁ …))))] - [(_ π₁ … ∈ π₂ …) #`(inv∈ (Pairof (Π π₁ …) (Π π₂ …)))] - [(_ π₁ … ∋ π₂ …) #`(inv∈ (Pairof (Π π₂ …) (Π π₁ …)))] - [(_ π₁ … ∉ π₂ …) #`(inv≢ (Pairof (Π π₁ …) (Π π₂ … ?)))] - [(_ π₁ … ∌ π₂ …) #`(inv≢ (Pairof (Π π₂ …) (Π π₁ … ?)))] - ))] + #:literals (≡ ≢ ∈ ∉ ∋ ∌ = ≤ ≥ length +) + [(_ π₁ … ≡ π₂ …) #`(U (inv≡ (Π π₁ …) (Π π₂ …)) + (inv≡ (Π π₂ …) (Π π₁ …)))] + [(_ π₁ … ≢ π₂ …) #`(U (inv≢ (Π π₁ …) (Π π₂ …)) + (inv≢ (Π π₂ …) (Π π₁ …)))] + [(_ π₁ … ∈ π₂ …) #`(inv∈ (Π π₁ …) (Π π₂ …))] + [(_ π₁ … ∋ π₂ …) #`(inv∈ (Π π₂ …) (Π π₁ …))] + [(_ π₁ … ∉ π₂ …) + #`(U (inv≢ (Π π₁ …) (Π π₂ … (#%dotted-id #%dot-separator :))) + (inv≢ (Π π₂ … (#%dotted-id #%dot-separator :)) (Π π₁ …)))] + [(_ π₁ … ∌ π₂ …) + #`(U (inv≢ (Π π₂ …) (Π π₁ … (#%dotted-id #%dot-separator :))) + (inv≢ (Π π₁ … (#%dotted-id #%dot-separator :)) (Π π₂ …)))] + ;; TODO: = should use a combination of ≤ and ≥ + [(_ π₁ … + {~and op {~or = ≤ ≥}} + (~or (+ (length π₂ …) n:nat) + {~and (length π₂ …) {~parse n 0}})) + #:with opN (syntax-case #'op (= ≤ ≥) + [= #'=N] + [≤ #'≤N] + [≥ #'≥N]) + #`(→ (invLength (opN n) (Π π₁ …) (Π π₂ …)) Void)]))] + +@CHUNK[<=> + (define-type (P A B) (Promise (Pairof A B))) + (define-type a 'a) + (define-type x 'x) + (define-type ax (U a x)) + (define-type x* (Rec R (P x R))) + (define-type ax* (Rec R (P ax R))) + (define-type-expander =N + (syntax-parser + [(_ 0) #'x*] + [(_ n:nat) #`(P a (=N #,(sub1 (syntax-e #'n))))])) + (define-type-expander ≥N + (syntax-parser + [(_ 0) #'ax*] + [(_ n:nat) #`(P a (≥N #,(sub1 (syntax-e #'n))))])) + (define-type-expander ≤N + (syntax-parser + [(_ 0) #'x*] + [(_ n:nat) #`(P ax (≤N #,(sub1 (syntax-e #'n))))]))] @chunk[ (define-type-expander Invariants @@ -515,7 +548,7 @@ making a union of all paths, without factoring out common parts. #`(→ (U Or (Invariant . inv) …) Void)]))] @chunk[ - (struct AnyField () #:transparent) + (define-type AnyField Symbol);(struct AnyField () #:transparent) (struct AnyType () #:transparent) (define-type ε (Π))] @@ -525,9 +558,10 @@ We define some tokens which will be used to identify the operator which relates two nodes in the graph. @chunk[ - (struct (A) inv≡ ([a : A])) - (struct (A) inv≢ ([a : A])) - (struct (A) inv∈ ([a : A])) + (struct (A B) inv≡ ([a : A] [b : B])) + (struct (A B) inv≢ ([a : A] [b : B])) + (struct (A B) inv∈ ([a : A] [b : B])) + (struct (A B C) invLength ([a : A] [b : B] [c : C])) ;(struct inv∉ ()) ;; Can be expressed in terms of ≢ (module literals typed/racket @@ -541,7 +575,7 @@ relates two nodes in the graph. stx))) ...)) - (define-literals ≡ ≢ ∈ ∉ ∋ ∌)) + (define-literals ≡ ≢ ∈ ∉ ∋ ∌ ≥ ≤)) (require 'literals)] @CHUNK[<≡> @@ -645,12 +679,10 @@ relates two nodes in the graph. (define-syntax-rule (template/top-loc loc e) (quasisyntax/top-loc loc #,(template e)))) - (provide ≡ ≢ ∈ ∉ ∋ ∌) + (provide ≡ ≢ ∈ ∉ ∋ ∌ ≥ ≤) ;; For testing: (provide Invariants - ≡x - ≢x inv≡ inv≢ Or @@ -666,11 +698,9 @@ relates two nodes in the graph. - ; - ; - <≡>] + <=>] diff --git a/test/invariant-phantom/simple.rkt b/test/invariant-phantom/simple.rkt index e12133a..97872b9 100644 --- a/test/invariant-phantom/simple.rkt +++ b/test/invariant-phantom/simple.rkt @@ -22,8 +22,8 @@ (Pairof (Pairof 'c AnyType) R2)) (List (Pairof 'd AnyType) (Pairof 'e AnyType))))))))) -(struct a ()); the node. -(struct b ()); the node. +(struct a AnyType ()); the node type a. +(struct b AnyType ()); the node type b. (check-same-type (Π :a.aa(.b.c)*.d.e) @@ -75,68 +75,7 @@ (check-same-type (Invariant :a(.b.c(.w)*.x.y)*.d.e ≡ :a(.b.c)*.d.e) - (U (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) 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) - (Rec - R3 - (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))))))))))) + (Invariant :a(.b.c(.w)*.x.y)*.d.e ≡ :a(.b.c)*.d.e)) (check-same-type (Invariant :a(.b.c(.w)*.x.y)*.d.e @@ -175,3 +114,30 @@ (check-a-stronger-than-b (Invariants (: ≡ .a.b.c(.d.e)*)) (Invariants (: ≡ .a.b.c.d.e))) + +(check-a-stronger-than-b (Invariants (.l ≥ (+ (length .a.b.c(.d.e)*) 3))) + (Invariants (.l ≥ (+ (length .a.b.c(.d.e)*) 2)))) + +(check-a-stronger-than-b (Invariants (.l ≥ (+ (length .a.b.c(.d.e)*) 1))) + (Invariants (.l ≥ (length .a.b.c(.d.e)*)))) + +(check-a-stronger-than-b (Invariants (.l ≤ (+ (length .a.b.c(.d.e)*) 2))) + (Invariants (.l ≤ (+ (length .a.b.c(.d.e)*) 3)))) + +(check-a-stronger-than-b (Invariants (.l ≤ (length .a.b.c(.d.e)*))) + (Invariants (.l ≤ (+ (length .a.b.c(.d.e)*) 1)))) + +(check-a-stronger-than-b (Invariants (.l = (length .a.b.c(.d.e)*))) + (Invariants (.l ≥ (length .a.b.c(.d.e)*)))) + +(check-a-stronger-than-b (Invariants (.l = (+ (length .a.b.c(.d.e)*) 1))) + (Invariants (.l ≤ (+ (length .a.b.c(.d.e)*) 1)))) + +(check-same-type (Invariants (.l = (length .a.b.c(.d.e)*))) + (Invariants (.l = (+ (length .a.b.c(.d.e)*) 0)))) + +(check-a-stronger-than-b (Invariants (:a.l ≥ (+ (length :a.f.g) 3)) + (:a ≡ :a.f.h) + (:a ∉ :a.f.g)) + (Invariants (:a.l ≥ (+ (length :a.f.g) 2)) + (:a ≢ :a.f.g.x)))