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. > Thank you. Pushed. felix ___ 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'
Peter Bex writes: > On Mon, Dec 10, 2018 at 09:24:57PM +0200, megane wrote: >> > On 2018-12-02 18:02, megane wrote: [...] >> >> 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. > > I have only been following this with half an eye, so I apologize if I'm > being a complete idiot, but wouldn't it be more in line with the style > of CHICKEN core to use a gensym for the type variable and attach a plist > to it to hold the type variable information? > > The gensym itself would act both as a unique identifier and as the > variable itself; when printing the type you'd only need to strip the > syntax info and voila, you have a readable type. I guess that could work. Doesn't strip-syntax ultimately use ##core#real-name, which was the core issue with #1563? I think the current system is completely fine for the current scrutinizer features, however. If you want to daydream about new features for scrutinizer then I think the record version is more beneficial. If you allow a tv to unify with another tv then having fast way to deal with tvs becomes important. This leads to tvs living longer and thus there being more of them. Currently you'd be hard pressed to find a file that takes more than 10ms to scrutinize. If you allow this unification you need to rename the variables anyway when printing to user. If get two type variables, whose original names were "a", from different routes you want to print them with different names if they really are different tvs. I have allowed this tv-tv unification in my local branch so I'm not completely talking out of my ass. This is all daydreaming, though. There's more useful targets for improvements in the scrutinizer. ___ 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'
On Mon, Dec 10, 2018 at 09:24:57PM +0200, megane wrote: > > 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). [...] > 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. I have only been following this with half an eye, so I apologize if I'm being a complete idiot, but wouldn't it be more in line with the style of CHICKEN core to use a gensym for the type variable and attach a plist to it to hold the type variable information? The gensym itself would act both as a unique identifier and as the variable itself; when printing the type you'd only need to strip the syntax info and voila, you have a readable type. Cheers, Peter signature.asc Description: PGP signature ___ 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'
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
Re: [Chicken-hackers] [PATCH] * scrutinizer.scm: Fix renaming issue with 'the'
Hey megane, good find once again. Sign-off attached.
That's a nice idea regarding tv handling. Some thoughts about that are
inline below.
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.
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.
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.
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 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?
> 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.
>
> If you have Norvig's book Paradigms of Artificial Intelligence
> Programming, there's a short explanation of this in chapter 11.6
> "Destructive Unification".
I'll have to go read PAIP before I ask any more questions. :)
Evan
>From 3b5a2237b71955638f25371005d7cbd2c4a35865 Mon Sep 17 00:00:00 2001
From: megane
Date: Sat, 1 Dec 2018 10:24:16 +0200
Subject: [PATCH 1/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
>From 7e0e92083192ff75bdda28882e428bdece32d448 Mon Sep 17 00:00:00 2001
From: Evan Hanson
Date: Mon, 10 Dec 2018 18:27:12 +1300
Subject: [PATCH 2/2] Restore typevar (un)renaming via real name table
Use the real name table to register type variables aliases as they're
assigned, and to subsequently unalias them when they are displayed to
the
