From 6c9a7a95d955d65d40e4bf72a44d57b02a526261 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Mon, 27 Mar 2017 00:39:02 +0200 Subject: [PATCH] =?UTF-8?q?Fixed=20bug=20in=20invariants=20implementation?= =?UTF-8?q?=20(phantom=20type=20Target=20had=20no=20fields,=20and=20theref?= =?UTF-8?q?ore=20its=20polymorphic=20argument=20was=20ignored).=20Used=20m?= =?UTF-8?q?ore=20precise=20tests=20(test=20that=20a=20=E2=8A=8F=20b=20rath?= =?UTF-8?q?er=20than=20a=20=E2=8A=91=20b=20for=20the=20invariant=20types.)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- invariants-phantom.hl.rkt | 42 +++++++++++++++++++++------------------ 1 file changed, 23 insertions(+), 19 deletions(-) diff --git a/invariants-phantom.hl.rkt b/invariants-phantom.hl.rkt index 9c2a84b..49199f6 100644 --- a/invariants-phantom.hl.rkt +++ b/invariants-phantom.hl.rkt @@ -371,8 +371,8 @@ relates two nodes in the graph. @chunk[ (struct ε () #:transparent) - (struct (T) Target () #:transparent) - (struct (T) NonTarget Target ([x : T]) #:transparent) + (struct (T) Target ([x : T]) #:transparent) + (struct (T) NonTarget Target () #:transparent) (define-type-expander Cycle (syntax-parser @@ -432,14 +432,16 @@ Two sorts of paths inside (in)equality constraints: @subsection{Putting it all together} @chunk[ - (define-syntax (check-a-stronger-or-same-b stx) + (define-syntax (check-a-stronger-than-b stx) (syntax-case stx () [(_ stronger weaker) (syntax/top-loc stx - (check-ann (ann witness-value stronger) - weaker))])) + (begin (check-ann (ann witness-value stronger) + weaker) + (check-not-tc + (ann (ann witness-value weaker) stronger))))])) - (define-syntax (check-a-same-b stx) + (define-syntax (check-a-same-as-b stx) (syntax-case stx () [(_ a b) (syntax/top-loc stx @@ -450,6 +452,8 @@ Two sorts of paths inside (in)equality constraints: @chunk[<*> (require (for-syntax phc-toolkit/untyped syntax/parse)) + + (provide Invariants ≡) @@ -464,20 +468,20 @@ Two sorts of paths inside (in)equality constraints: (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-than-b (Invariants (≡ (_ a) (_ a b c))) + (Invariants)) - (check-a-same-b (Invariants (≡ (_ a) (_ a b c))) + (check-a-same-as-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-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-or-same-b (Invariants (≡ (_) - (_ b d a b d ↙ a b (d)))) - (Invariants (≡ (_) - (_ b d ↙ a b (d))))))] + (check-a-stronger-than-b (Invariants (≡ (_) + (_ b d a b d ↙ a b (d)))) + (Invariants (≡ (_) + (_ b d ↙ a b (d))))))]