Work on invariants.
This commit is contained in:
Georges Dupéron
parent
6c9a7a95d9
commit
acb444f88f
|
|
@ -1,14 +1,14 @@
|
|||
<!-- Tufts VUE 3.3.0 concept-map (Graph-notes-copy2.vue) 2017-03-19 -->
|
||||
<!-- Tufts VUE 3.3.0 concept-map (Graph-notes-copy2.vue) 2017-03-23 -->
|
||||
<!-- 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: Saved date Sun Mar 19 16:06:34 CET 2017 by georges on platform Linux 4.4.40 in JVM 1.8.0_122-04 -->
|
||||
<!-- 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: 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"?>
|
||||
<LW-MAP xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
|
||||
xsi:noNamespaceSchemaLocation="none" ID="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">
|
||||
<resource referenceCreated="1489935994403" size="216026"
|
||||
<resource referenceCreated="1490230468578" size="216025"
|
||||
spec="/home/georges/phc/racket-packages/phc-graph/Graph-notes-copy2.vue"
|
||||
type="1" xsi:type="URLResource">
|
||||
<title>Graph-notes-copy2.vue</title>
|
||||
|
|
@ -3913,8 +3913,8 @@
|
|||
y="0.0" width="1.4E-45" height="1.4E-45" strokeWidth="0.0" autoSized="false">
|
||||
<URIString>http://vue.tufts.edu/rdf/resource/6dbf6b15c0a80026548592b8d2f3fee2</URIString>
|
||||
</layer>
|
||||
<userZoom>1.0</userZoom>
|
||||
<userOrigin x="-1194.022" y="-194.81644"/>
|
||||
<userZoom>0.75</userZoom>
|
||||
<userOrigin x="-1182.522" y="-189.81644"/>
|
||||
<presentationBackground>#FFFFFF</presentationBackground>
|
||||
<PathwayList currentPathway="0" revealerIndex="-1">
|
||||
<pathway ID="0" label="Chemin sans nom" created="1479309847603"
|
||||
|
|
|
|||
|
|
@ -2,7 +2,7 @@
|
|||
|
||||
(require racket/struct
|
||||
;; TODO: move delay-pure/private/immutable-struct to a separate package
|
||||
delay-pure/private/immutable-struct) ;; for immutable-struct? below.
|
||||
phc-toolkit/untyped/meta-struct) ;; for immutable-struct? below.
|
||||
|
||||
(provide free-id-tree=?
|
||||
free-id-tree-hash-code
|
||||
|
|
@ -31,7 +31,7 @@
|
|||
(cons/c isyntax isyntax)
|
||||
(vectorof isyntax #:immutable #t)
|
||||
(syntax/c isyntax)
|
||||
(and/c immutable-struct?
|
||||
(and/c struct-instance-is-immutable?
|
||||
(λ (v)
|
||||
(andmap isyntax/c (struct->list v)))))))
|
||||
|
||||
|
|
|
|||
|
|
@ -15,12 +15,12 @@
|
|||
|
||||
@section{Introduction}
|
||||
|
||||
The cautious compiler writer will no doubt want to check that the graph used
|
||||
to represent the program verifies some structural properties. For example, the
|
||||
compiled language might not allow cycles between types. Another desirable
|
||||
property is that the @racket[in-method] field of an instruction points back to
|
||||
the method containing it. We will use this second property as a running
|
||||
example in this section.
|
||||
The cautious compiler writer will no doubt want to check that the Abstract
|
||||
Syntax Tree or Graph used to represent the program verifies some structural
|
||||
properties. For example, the compiled language might not allow cycles between
|
||||
types. Another desirable property is that the @racket[in-method] field of the
|
||||
node representing an instruction points back to the method containing it. We
|
||||
will use this second property as a running example in this section.
|
||||
|
||||
@section{Implementation overview : subtyping, variance and phantom types}
|
||||
|
||||
|
|
@ -341,6 +341,12 @@ having an empty union.
|
|||
|
||||
@subsection{Structural (in)equality and (non-)membership invariants}
|
||||
|
||||
@subsubsection{Invariants and their relationships}
|
||||
|
||||
@itemlist[
|
||||
@item{Paths, }
|
||||
]
|
||||
|
||||
@subsubsection{Comparison operator tokens}
|
||||
|
||||
We define some tokens which will be used to identify the operator which
|
||||
|
|
@ -377,17 +383,20 @@ relates two nodes in the graph.
|
|||
(define-type-expander Cycle
|
||||
(syntax-parser
|
||||
[(_ field:id … {~literal ↙} loop1:id … (target:id) loop2:id …)
|
||||
#'(List* (NonTarget ε)
|
||||
(NonTarget 'field) …
|
||||
(Rec R (List* (NonTarget 'loop1) … ;(NonTarget 'loop1) …
|
||||
(Target 'target) ;(NonTarget 'target)
|
||||
(NonTarget 'loop2) … ;(NonTarget 'loop2) …
|
||||
R)))]
|
||||
#'(→ (List* (NonTarget ε)
|
||||
(NonTarget 'field) …
|
||||
(Rec R (List* (NonTarget 'loop1) … ;(NonTarget 'loop1) …
|
||||
(Target 'target) ;(NonTarget 'target)
|
||||
(U (List* (NonTarget 'loop2) … ;(NonTarget 'loop2) …
|
||||
R)
|
||||
Null)))) Void)]
|
||||
[(_ field … target)
|
||||
;; TODO: something special at the end?
|
||||
#'(List (NonTarget ε) (NonTarget 'field) … (Target 'target))]
|
||||
#'(→ (List (NonTarget ε)
|
||||
(NonTarget 'field)
|
||||
…
|
||||
(Target 'target)) Void)]
|
||||
[(_)
|
||||
#'(List (Target ε))]))]
|
||||
#'(→ (List (Target ε)) Void)]))]
|
||||
|
||||
@;{@[
|
||||
|
||||
|
|
@ -431,57 +440,23 @@ Two sorts of paths inside (in)equality constraints:
|
|||
|
||||
@subsection{Putting it all together}
|
||||
|
||||
@chunk[<check-a-stronger-b>
|
||||
(define-syntax (check-a-stronger-than-b stx)
|
||||
(syntax-case stx ()
|
||||
[(_ stronger weaker)
|
||||
(syntax/top-loc stx
|
||||
(begin (check-ann (ann witness-value stronger)
|
||||
weaker)
|
||||
(check-not-tc
|
||||
(ann (ann witness-value weaker) stronger))))]))
|
||||
|
||||
(define-syntax (check-a-same-as-b stx)
|
||||
(syntax-case stx ()
|
||||
[(_ a b)
|
||||
(syntax/top-loc stx
|
||||
(begin
|
||||
(check-ann (ann witness-value a) b)
|
||||
(check-ann (ann witness-value b) a)))]))]
|
||||
|
||||
@chunk[<*>
|
||||
(require (for-syntax phc-toolkit/untyped
|
||||
syntax/parse))
|
||||
|
||||
(provide Invariants ≡)
|
||||
|
||||
;; For testing:
|
||||
(provide Invariants
|
||||
≡
|
||||
inv≡
|
||||
inv≢
|
||||
Or
|
||||
Target
|
||||
NonTarget
|
||||
ε
|
||||
witness-value)
|
||||
|
||||
<witness-value>
|
||||
<grouping-invariants>
|
||||
<cycles>
|
||||
<comparison-operators>
|
||||
<≡>
|
||||
|
||||
(module+ test
|
||||
(require phc-toolkit)
|
||||
<check-a-stronger-b>
|
||||
|
||||
(ann witness-value (Invariants)) ;; No invariants
|
||||
(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))))
|
||||
|
||||
(check-a-stronger-than-b (Invariants (≡ (_)
|
||||
(_ b d a b d ↙ a b (d))))
|
||||
(Invariants (≡ (_)
|
||||
(_ b d ↙ a b (d))))))]
|
||||
<≡>]
|
||||
|
|
|
|||
37
test/invariant-phantom/simple.rkt
Normal file
37
test/invariant-phantom/simple.rkt
Normal file
|
|
@ -0,0 +1,37 @@
|
|||
#lang type-expander
|
||||
|
||||
(require (lib "phc-graph/invariants-phantom.hl.rkt")
|
||||
"util.rkt"
|
||||
phc-toolkit)
|
||||
|
||||
(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))))
|
||||
25
test/invariant-phantom/util.rkt
Normal file
25
test/invariant-phantom/util.rkt
Normal file
|
|
@ -0,0 +1,25 @@
|
|||
#lang type-expander
|
||||
|
||||
(provide check-a-same-as-b
|
||||
check-a-stronger-than-b)
|
||||
|
||||
(require phc-toolkit
|
||||
(lib "phc-graph/invariants-phantom.hl.rkt")
|
||||
(for-syntax phc-toolkit/untyped))
|
||||
|
||||
(define-syntax (check-a-stronger-than-b stx)
|
||||
(syntax-case stx ()
|
||||
[(_ stronger weaker)
|
||||
(syntax/top-loc stx
|
||||
(begin (check-ann (ann witness-value stronger)
|
||||
weaker)
|
||||
(check-not-tc
|
||||
(ann (ann witness-value weaker) stronger))))]))
|
||||
|
||||
(define-syntax (check-a-same-as-b stx)
|
||||
(syntax-case stx ()
|
||||
[(_ a b)
|
||||
(syntax/top-loc stx
|
||||
(begin
|
||||
(check-ann (ann witness-value a) b)
|
||||
(check-ann (ann witness-value b) a)))]))
|
||||
Loading…
Reference in New Issue
Block a user