Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix functional dependency resolution with superclasses #1315

Open
wants to merge 4 commits into
base: main
Choose a base branch
from
Open

Fix functional dependency resolution with superclasses #1315

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
2efe248
fix fundep resolution with superclasses
YarinHeffes Oct 18, 2024
f88d05d
added documentation and removed use of mapcan
YarinHeffes Oct 18, 2024
fb87e95
added test for fundep superclass resolution
YarinHeffes Oct 18, 2024
467687c
replaced apply append with loop append
YarinHeffes Oct 18, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 17 additions & 0 deletions src/typechecker/context-reduction.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -268,11 +268,28 @@ Returns (VALUES deferred-preds retained-preds defaultable-preds)"
:do (setf subs (compose-substitution-lists subs (fundep-entail% env expr-preds pred known-tyvars)))
:finally (return subs)))

(defun expand-pred-into-superclasses (env pred)
stylewarning marked this conversation as resolved.
Show resolved Hide resolved
"This function finds the class in ENV associated with PRED and
recursively appends superclass predicates, with appropriate type
substitutions."
(declare (type environment env)
(type ty-predicate pred)
(values ty-predicate-list &optional))
(let* ((class (lookup-class env (ty-predicate-class pred)))
(subs (mapcan #'match
(ty-predicate-types (ty-class-predicate class))
(ty-predicate-types pred))))
(cons pred (loop :for super-pred :in (ty-class-superclasses class)
:for corrected-super-pred := (apply-substitution subs super-pred)
:append (expand-pred-into-superclasses env corrected-super-pred)))))

(defun fundep-entail% (env expr-preds pred known-tyvars)
(let ((class (lookup-class env (ty-predicate-class pred))))
(unless (ty-class-fundeps class)
(return-from fundep-entail% nil))

(setf expr-preds (mapcan (lambda (p) (expand-pred-into-superclasses env p)) expr-preds))

(let* ((unknown-indices nil)

(known-indices
Expand Down
16 changes: 16 additions & 0 deletions tests/fundep-tests.lisp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -147,3 +147,19 @@
(let ((filled?
(fn (i) (coalton-library/optional:some? (moo-find moo i)))))
(coalton-library/iterator:filter! filled? (coalton-library/iterator:up-to (moo-size moo)))))"))

(deftest fundep-superclass-resolution ()
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

write a few more tests with some more complicated examples

;; See https://github.com/coalton-lang/coalton/issues/1050
(check-coalton-types
"(define-class (RandomAccessBase :f :t (:f -> :t))
(make (UFix -> :t -> :f))
(rab-length (:f -> UFix)))

(define-class (RandomAccessBase :f :t => RandomAccessReadable :f :t (:f -> :t))
(unsafe-set! (:f -> UFix -> :t)))

(declare aref (RandomAccessReadable :f :t => :f -> UFix -> (Optional :t)))
(define (aref storage index)
(if (and (<= 0 index) (< index (rab-length storage)))
(Some (unsafe-set! storage index))
None)))"))
Loading