From 64d1756678c158c16345574cb1407672f2e28d17 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Mon, 9 Jan 2017 19:44:21 +0100 Subject: [PATCH] =?UTF-8?q?Started=20drafting=20the=20=E2=89=A1=20invarian?= =?UTF-8?q?t=20representation=20as=20a=20type?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- invariants-phantom.hl.rkt | 22 +++++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/invariants-phantom.hl.rkt b/invariants-phantom.hl.rkt index 6e9786b..4589563 100644 --- a/invariants-phantom.hl.rkt +++ b/invariants-phantom.hl.rkt @@ -346,10 +346,20 @@ We define some tokens which will be used to identify the operator which relates two nodes in the graph. @chunk[ - (struct ≡ ()) - (struct ≢ ()) - (struct ∈ ()) - (struct ∉ ())] + (struct (A B) inv≡ ([a : A] [b : B])) + (struct (A B) inv≢ ([a : A] [b : B])) + ;(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 ...))]))] + +@; TODO: don't forget to include both directions a = b and b = a (or sort the fields?) @subsection{Putting it all together} @@ -359,8 +369,10 @@ relates two nodes in the graph. + <≡> (code:comment "Tests:") (ann witness-value (Invariants)) ;; No invariants - + (ann witness-value (Invariants (≡ (a) (a b c)))) ;; No invariants + (void)]