Make cgen/seq for lists be used more often.
This commit is contained in:
parent
050c1022c9
commit
6d975ea6bb
|
@ -432,6 +432,10 @@
|
||||||
#:when (subtype a b)
|
#:when (subtype a b)
|
||||||
empty]
|
empty]
|
||||||
|
|
||||||
|
;; Lists delegate to sequences
|
||||||
|
[((ListSeq: s-seq) (ListSeq: t-seq))
|
||||||
|
(cgen/seq V X Y s-seq t-seq)]
|
||||||
|
|
||||||
;; refinements are erased to their bound
|
;; refinements are erased to their bound
|
||||||
[((Refinement: S _) T)
|
[((Refinement: S _) T)
|
||||||
(cg S T)]
|
(cg S T)]
|
||||||
|
@ -555,10 +559,6 @@
|
||||||
[((Set: t) (Sequence: (list t*)))
|
[((Set: t) (Sequence: (list t*)))
|
||||||
(cg t t*)]
|
(cg t t*)]
|
||||||
|
|
||||||
;; Lists delegate to sequences
|
|
||||||
[((ListSeq: s-seq) (ListSeq: t-seq))
|
|
||||||
(cgen/seq V X Y s-seq t-seq)]
|
|
||||||
|
|
||||||
;; if we have two mu's, we rename them to have the same variable
|
;; if we have two mu's, we rename them to have the same variable
|
||||||
;; and then compare the bodies
|
;; and then compare the bodies
|
||||||
;; This relies on (B 0) only unifying with itself,
|
;; This relies on (B 0) only unifying with itself,
|
||||||
|
|
Loading…
Reference in New Issue
Block a user