Re: [Chicken-hackers] [PATCH] * scrutinizer.scm: Fix renaming issue with 'the'
On 2018-12-10 13:39, felix.winkelm...@bevuta.com wrote:
> Evan, the patches don't apply cleanly. Can you rebase them to the
> current master?
Sure, here's a set that can be applied in order.
megane has asked that the third one be left out until we have a look at
the other patches, which is fine with me so I've omitted it.
Thanks,
Evan
>From 8d9c3675120acb7a6ed9614436b121eaf5e57d09 Mon Sep 17 00:00:00 2001
From: megane
Date: Sun, 2 Dec 2018 18:23:44 +0200
Subject: [PATCH 1/2] Fix renaming issue with typevars
The 'subst' in simplify-type was not checking what it was renaming so
bad things happened as the new test case shows.
* scrutinizer.scm (simplify-type): No need to call subst as the
typevars are renamed during walking (the "(assq t typeenv) =>"
case).
* tests/typematch-tests.scm: Add test
Signed-off-by: Evan Hanson
---
scrutinizer.scm | 9 +
tests/typematch-tests.scm | 3 +++
2 files changed, 4 insertions(+), 8 deletions(-)
diff --git a/scrutinizer.scm b/scrutinizer.scm
index bbc3b5a9..840cda3d 100644
--- a/scrutinizer.scm
+++ b/scrutinizer.scm
@@ -1213,13 +1213,6 @@
(let ((typeenv '()) ; ((VAR1 . NEWVAR1) ...)
(constraints '()) ; ((VAR1 TYPE1) ...)
(used '()))
-(define (subst x)
- (cond ((symbol? x)
- (cond ((assq x typeenv) => cdr)
- (else x)))
- ((pair? x)
- (cons (subst (car x)) (subst (cdr x
- (else x)))
(define (simplify t)
;;(dd "simplify/rec: ~s" t)
(call/cc
@@ -1351,7 +1344,7 @@
(list v (simplify (cadr c)
(else v)
typeenv)
- ,(subst t2
+ ,t2)))
(dd "simplify: ~a -> ~a" t t2)
t2)))
diff --git a/tests/typematch-tests.scm b/tests/typematch-tests.scm
index 97b83289..821ef731 100644
--- a/tests/typematch-tests.scm
+++ b/tests/typematch-tests.scm
@@ -399,6 +399,9 @@
(length a) ; refine (or pair null) with list (= (list-of *))
(infer list a))
+(compiler-typecase (the (list (struct foo) symbol) (the 'a 1))
+ ;; The tv "foo" and "foo" in struct should have no relation
+ ((forall (foo) (list (struct foo) foo)) 'ok))
(assert
(compiler-typecase 1
--
2.11.0
>From f08078dc50b7e5f4bbe23459b2ba6ba3718e9b0d Mon Sep 17 00:00:00 2001
From: megane
Date: Sat, 1 Dec 2018 10:24:16 +0200
Subject: [PATCH 2/2] Fix renaming issue with 'the'
The 'the' macro calls check-and-validate-type which will eventually call
simplify-type on the type. simplify-type renames type variables with
gensym and sets the ##core#real-name property, perhaps because of
prettier messages for the user. Finally the 'the' macro expander uses
the property to undo the renaming.
Fixes #1563.
* scrutinizer.scm (simplify-type): Don't set the ##core#real-name
property for renamed tvs
* tests/typematch-tests.scm: Add test
* tests/scrutiny.expected: Update
Signed-off-by: Evan Hanson
---
scrutinizer.scm | 4 +---
tests/scrutiny.expected | 2 +-
tests/typematch-tests.scm | 3 +++
3 files changed, 5 insertions(+), 4 deletions(-)
diff --git a/scrutinizer.scm b/scrutinizer.scm
index 840cda3d..a8c8b3de 100644
--- a/scrutinizer.scm
+++ b/scrutinizer.scm
@@ -1224,9 +1224,7 @@
(set! typeenv
(append (map (lambda (v)
(let ((v (if (symbol? v) v (first v
- (let ((v* (gensym v)))
- (mark-variable v* '##core#real-name v)
- (cons v v*
+ (cons v (gensym v
typevars)
typeenv))
(set! constraints
diff --git a/tests/scrutiny.expected b/tests/scrutiny.expected
index 665d7008..e445ebbb 100644
--- a/tests/scrutiny.expected
+++ b/tests/scrutiny.expected
@@ -40,7 +40,7 @@ Warning: at toplevel:
(scrutiny-tests.scm:29) in procedure call to `scheme#+', expected argument #2 of type `number' but was given an argument of type `symbol'
Warning: at toplevel:
- assignment of value of type `fixnum' to toplevel variable `scheme#car' does not match declared type `(forall (a) (procedure scheme#car ((pair a *)) a))'
+ assignment of value of type `fixnum' to toplevel variable `scheme#car' does not match declared type `(forall (a335) (procedure scheme#car ((pair a335 *)) a335))'
Warning: at toplevel:
expected a single result in `let' binding of `g19', but received 2 results
diff --git a/tests/typematch-tests.scm b/tests/typematch-tests.scm
index 821ef731..231207f2 100644
--- a/tests/typematch-tests.scm
+++ b/tests/typematch-tests.scm
@@ -403,6 +403,9 @@
;; The tv "foo" and "foo" in struct should have no relation
((forall (foo) (list (struct foo) foo)) 'ok))
+;; Issue #1563
+(compiler-typecase (the (forall (a) a) 1) ((forall (a) (list a)) 'ok))
+
(assert
(compiler-typecase 1
('a #t)))
--
2.11.0
___
Chicken-hackers mailing list
Chicken-hackers@nongnu.org
https://lists.nongnu.org/mailman/listinfo/chicken-hackers
Re: [Chicken-hackers] [PATCH] * scrutinizer.scm: Fix renaming issue with 'the'
Evan Hanson writes: > Hey megane, good find once again. Sign-off attached. > > That's a nice idea regarding tv handling. Some thoughts about that are > inline below. Hey Evan, thanks for taking a look. Sorry, I forgot there was this PS about type variable records in the mail when I asked you to look at this mail. I did not want to bother you with that. This is not a pressing issue :) I commented on the matter more, but feel free to skip that. I am just thinking aloud. > > In the meantime, I think the second patch attacheed to this email would > be good to apply as well. It uses the "real" real name table in a > similar way to what was done before (this should have been the approach > used in the first instance, really), which avoids interfering with macro > handling but still prints the aliases nicely. This avoids a regression > until something more full-on like what you've described can be done. There is a fix to this renaming issue in the patch set I just posted. It is in the last commit (0012). Maybe we can postpone this fix until that patch set gets resolved? > > Cheers, > > Evan > > On 2018-12-02 18:02, megane wrote: >> Personally I feel the best way to handle this would be to remove 'forall >> altogether inside the scrutinizer and use, for example, a record for the >> typevariables inside the types. For example: >> >> (forall (a) (vector a)) would be converted to: >> >> `(vector ,(make-type-variable 'a (generate-new-tv-id) #f)) > > We'd need to include constraints in there somehow, too. True. Like this: (make-type-variable 'a (generate-new-tv-id) #f #f). > > The "forall" representation has the benefit of making it possible to > know what type variables appear in a form without walking it again (once > the type has been constructed) since they can be coalesced onto the > root. I'm not sure how much we take advantage of that currently, so it > might not matter, but there may be a performance cost if we lose that > property. I think the biggest benefit for the forall style is the explicitness. Especially when printing. It shows which symbols are type variables, and what their constraint types are. I think this style has its uses even if the internal representation changes. I think the biggest cost from typeenv comes from the two first tests in 'match1. Here we check all symbols against the typeenv, which is a linear search. If we use records, it's just one test. > > Regardless of the representation used within the scrutiniser, It would > be nice to use the quoted shorthand when printing typevars, now that we > have it. This is handled in the pp patchset I mentioned above. > >> This way we could get rid of the typeenv too. > > How so? Wouldn't we still need to pass the "active" typeenv around to > resolve/match-types/etc. same as today? When using tv records the typeenv would exist implicitly in the records contained in a type. The typeenv is the mapping from tv-name to a list (tv-name false-or-unified-type false-or-constraint). When using tv records the information in this list would exists directly in the tv record. We don't need to look it up from anywhere. So today, we have a type (forall (a b) (procedure (a) b)). From this we extract the typeenv ((a #f #f) (b #f #f)), which we would pass to match-types. With tv records you would convert the type to (procedure (,(make-tv 'a (gen) #f #f)) ,(make-tv 'b (gen) #f #f)), which you can pass to match-types. In match types, instead of checking the typeenv, you just test (tv? t). > >> The unification trail would have to be changed too. Turns out it's >> enough to just push the type-variable record to the trail. When undoing >> the unifications just grab a record from the trail and set the type to >> #f. I'll try to expand this a bit. The trail is used to record unifications. Today, when a unification happens in 'match1, the unified variable's name symbol is added as the head of the 'trail global. To undo unifications, we take a symbol from the trail. Lookup the tv's list , as described above, from a relevant typeenv. Then we set the second element of that list (the false-or-unified-type part) back to #f. When using tv records we just grab a tv record from the trail and set the type field back to #f. ___ Chicken-hackers mailing list Chicken-hackers@nongnu.org https://lists.nongnu.org/mailman/listinfo/chicken-hackers
Re: [Chicken-hackers] [PATCH] * scrutinizer.scm: Fix renaming issue with 'the'
Evan, the patches don't apply cleanly. Can you rebase them to the current master? felix ___ Chicken-hackers mailing list Chicken-hackers@nongnu.org https://lists.nongnu.org/mailman/listinfo/chicken-hackers
