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.

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

Add more ctype extension data structures #23

Merged
merged 13 commits into from
May 17, 2023
16 changes: 16 additions & 0 deletions MANUAL.md
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,22 @@ Parses a type specifier to a ctype in the given environment. The default environ

---

[Function]

**extended-specifier-ctype** *type-specifier* `&optional` *environment* => *ctype*

Parses a type specifier to a ctype in the given environment. Parts of the type-specifier might be using extended types. The default environment is `nil`, representing the current global environment. The environment is used to get information about type macros defined with `deftype`.

---

[Macro]

**define-extended-type** *name* *lambda-list* `&key` *documentation* *simple* *extended* => *name*

Defines an extended type specifier called name. If it is parsed using `specifier-ctype` or some other non-extended parsing facility, the simple forms are used to create a more primitive type specifier. If it is parsed using `extended-type-specifier`, the extended forms are used to create a ctype. Both the simple and extended forms are required.

---

# Relations

## Definitions
Expand Down
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -70,4 +70,4 @@ While ctype implements the Common Lisp type system, some users may be interested

The ext/ directory contains a few example extensions. See the README in that directory for more information.

Extension mechanisms for the type specifier parser have not been solidly defined yet.
Custom ctypes can be represented as type specifiers using `define-extended-type` and accessed using `extended-specifier-ctype` . See the documentation strings for more information.
30 changes: 9 additions & 21 deletions cmember.lisp
charJe marked this conversation as resolved.
Show resolved Hide resolved
charJe marked this conversation as resolved.
Show resolved Hide resolved
Original file line number Diff line number Diff line change
Expand Up @@ -10,54 +10,42 @@
(defmethod subctypep ((ct1 cmember) (ct2 cmember))
(values (subsetp (cmember-members ct1) (cmember-members ct2)) t))

(declaim (inline member-disjointp))
(defun member-disjointp (cmember ctype)
(define-commutative-method disjointp ((cmember cmember) (ctype ctype))
(values
(notany
(lambda (single-member)
(ctypep single-member ctype))
(cmember-members cmember))
(notany (lambda (single-member)
(ctypep single-member ctype))
(cmember-members cmember))
t))

(defmethod disjointp ((cmember cmember) (ctype ctype))
(member-disjointp cmember ctype))

(defmethod disjointp ((ctype ctype) (cmember cmember))
(member-disjointp cmember ctype))

(defmethod conjointp ((ct1 cmember) (ct2 cmember)) (values nil t))

(defmethod cofinitep ((ct cmember)) (values nil t))

(defmethod conjoin/2 ((ct1 cmember) (ct2 cmember))
(apply #'cmember
(intersection (cmember-members ct1) (cmember-members ct2))))
(defun conjoin-cmember (cmember ctype)

(define-commutative-method conjoin/2 ((cmember cmember) (ctype ctype))
;; FIXME: Could save a little consing by checking subctypep first I guess.
(apply #'cmember
(loop for mem in (cmember-members cmember)
when (ctypep mem ctype) collect mem)))
(defmethod conjoin/2 ((ct1 cmember) (ct2 ctype)) (conjoin-cmember ct1 ct2))
(defmethod conjoin/2 ((ct1 ctype) (ct2 cmember)) (conjoin-cmember ct2 ct1))

(defmethod disjoin/2 ((ct1 cmember) (ct2 cmember))
(apply #'cmember (union (cmember-members ct1) (cmember-members ct2))))
(defun disjoin-cmember (cmember ctype)

(define-commutative-method disjoin/2 ((cmember cmember) (ctype ctype))
(let ((non (loop with diff = nil
for mem in (cmember-members cmember)
if (ctypep mem ctype)
do (setf diff t)
else
collect mem
;; If there's no change, give up to avoid recursion
finally (unless diff (return-from disjoin-cmember nil)))))
finally (unless diff (return-from disjoin/2 nil)))))
(if non
(disjunction (apply #'cmember non) ctype)
ctype)))
(defmethod disjoin/2 ((ct1 cmember) (ct2 ctype))
(disjoin-cmember ct1 ct2))
(defmethod disjoin/2 ((ct1 ctype) (ct2 cmember))
(disjoin-cmember ct2 ct1))

(defmethod subtract ((ct1 cmember) (ct2 cmember))
(apply #'cmember
Expand Down
21 changes: 5 additions & 16 deletions conjunction.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -35,34 +35,27 @@
;; this also covers the case of ct2 being top.
(every/tri (lambda (sct) (subctypep ct1 sct)) (junction-ctypes ct2)))

(defmethod disjointp ((ct1 conjunction) (ct2 ctype))
(define-commutative-method disjointp ((ct1 conjunction) (ct2 ctype))
;; if a ^ z = 0 then a ^ b ^ z = 0.
;; doesn't follow the other way, though.
(if (some/tri (lambda (sct) (disjointp sct ct2)) (junction-ctypes ct1))
(values t t)
(values nil nil)))
(defmethod disjointp ((ct1 ctype) (ct2 conjunction))
(if (some/tri (lambda (sct) (disjointp ct1 sct)) (junction-ctypes ct2))
(values t t)
(values nil nil)))
(defmethod conjointp ((ct1 conjunction) (ct2 ctype))

(define-commutative-method conjointp ((ct1 conjunction) (ct2 ctype))
;; (a ^ b) v z = T <=> (a v z) ^ (b v z) = T
(every/tri (lambda (sct) (conjointp sct ct2)) (junction-ctypes ct1)))
(defmethod conjointp ((ct1 ctype) (ct2 conjunction))
(every/tri (lambda (sct) (conjointp ct1 sct)) (junction-ctypes ct2)))

(defmethod negate ((ctype conjunction))
;; de Morgan: ~(a & b) = ~a | ~b
(apply #'disjoin (mapcar #'negate (junction-ctypes ctype))))

(defmethod conjoin/2 ((ct1 conjunction) (ct2 conjunction))
(apply #'conjoin (append (junction-ctypes ct1) (junction-ctypes ct2))))
(defmethod conjoin/2 ((ct1 conjunction) (ct2 ctype))
(define-commutative-method conjoin/2 ((ct1 conjunction) (ct2 ctype))
(apply #'conjoin ct2 (junction-ctypes ct1)))
(defmethod conjoin/2 ((ct1 ctype) (ct2 conjunction))
(apply #'conjoin ct1 (junction-ctypes ct2)))

(defun disjoin-conjunction (conjunction ctype)
(define-commutative-method disjoin/2 ((conjunction conjunction) (ctype ctype))
;; If any disjunction is uninteresting, give up - except that if some
;; of the disjunctions are T, factor those out.
;; (This factoring is important for correctly computing that (or x (not x))
Expand All @@ -84,10 +77,6 @@
(disjunction ctype
(apply #'conjunction uninteresting)))
(t nil)))))
(defmethod disjoin/2 ((ct1 conjunction) (ct2 ctype))
(disjoin-conjunction ct1 ct2))
(defmethod disjoin/2 ((ct1 ctype) (ct2 conjunction))
(disjoin-conjunction ct2 ct1))

(defmethod unparse ((ct conjunction))
(let ((ups (mapcar #'unparse (junction-ctypes ct))))
Expand Down
14 changes: 14 additions & 0 deletions ctype.asd
Original file line number Diff line number Diff line change
Expand Up @@ -57,3 +57,17 @@
"cfunction" "packages"))
(:file "parse"
:depends-on ("generic-functions" "create" "classes" "config" "packages"))))

(asdf:defsystem :ctype/ext
Copy link
Contributor Author

Choose a reason for hiding this comment

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

Perhaps in the future this system could consume the other bundled extensions. Alternatively perhaps you want them to be more granular than this.

:license "BSD"
:depends-on (:ctype :alexandria)
:components
((:module "ext"
:components
((:file "packages")
(:module "data-structures"
:depends-on ("packages")
:components
((:file "list-of")
(:file "array-of")
(:file "hash-table-of")))))))
20 changes: 4 additions & 16 deletions disjunction.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -50,39 +50,27 @@
(values nil t)
(values nil nil)))))

(defmethod disjointp ((ct1 disjunction) (ct2 ctype))
(define-commutative-method disjointp ((ct1 disjunction) (ct2 ctype))
;; (a v b) ^ z = 0 <=> (a ^ z) v (b ^ z) = 0
(every/tri (lambda (sct) (disjointp sct ct2)) (junction-ctypes ct1)))
(defmethod disjointp ((ct1 ctype) (ct2 disjunction))
(every/tri (lambda (sct) (disjointp ct1 sct)) (junction-ctypes ct2)))
(defmethod conjointp ((ct1 disjunction) (ct2 ctype))
(define-commutative-method conjointp ((ct1 disjunction) (ct2 ctype))
(if (some/tri (lambda (sct) (conjointp sct ct2)) (junction-ctypes ct1))
(values t t)
(values nil nil)))
(defmethod conjointp ((ct1 ctype) (ct2 disjunction))
(if (some/tri (lambda (sct) (conjointp ct1 sct)) (junction-ctypes ct2))
(values t t)
(values nil nil)))

(defmethod negate ((ctype disjunction))
(apply #'conjoin (mapcar #'negate (junction-ctypes ctype))))

(defmethod disjoin/2 ((ct1 disjunction) (ct2 disjunction))
(apply #'disjoin (append (junction-ctypes ct1)
(junction-ctypes ct2))))
(defmethod disjoin/2 ((ct1 disjunction) (ct2 ctype))
(define-commutative-method disjoin/2 ((ct1 disjunction) (ct2 ctype))
(apply #'disjoin ct2 (junction-ctypes ct1)))
(defmethod disjoin/2 ((ct1 ctype) (ct2 disjunction))
(apply #'disjoin ct1 (junction-ctypes ct2)))

(defun conjoin-disjunction (disjunction ctype)
(define-commutative-method conjoin/2 ((disjunction disjunction) (ctype ctype))
(apply #'disjoin
(loop for sct in (junction-ctypes disjunction)
collect (conjoin sct ctype))))
(defmethod conjoin/2 ((ct1 disjunction) (ct2 ctype))
(conjoin-disjunction ct1 ct2))
(defmethod conjoin/2 ((ct1 ctype) (ct2 disjunction))
(conjoin-disjunction ct2 ct1))

(defmethod unparse ((ct disjunction))
(let ((ups (mapcar #'unparse (junction-ctypes ct))))
Expand Down
8 changes: 6 additions & 2 deletions ext/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,13 @@ For example, the set of all `evenp` integers is `(ctype.ext.mod:congruence 2 #b0

The type of all integers that are not a multiple of three (i.e. that are 1 mod 3 or 2 mod 3) would be `(congruence 3 #b110)`. This too can be conjoined and disjoined at will, e.g. `(conjoin (congruence 3 #b110) (congruence 2 #b01))` => 2 or 4 mod 6, while `(disjoin (congruence 3 #b110) (congruence 2 #b01))` => 0, 1, 2, 4, or 5 mod 6. The conjunctions and disjunctions of congruences are always either congruences, `integer`, or `nil`.

# Indefinite-length lists
# Homogeneous Data Structures

The `list-of.lisp` file is a self contained implementation of the type of lists of some element type. This type cannot be expressed in the Common Lisp type system but is sometimes desired. In a little more detail, `(list-of x)` can be expressed recursively as being the object `nil` plus all objects of type `(cons x (list-of x))`. This includes circular lists, but not dotted lists.
They can be loaded with the `ctype/ext` ASDF system which has ctype and alexandria as dependencies.

The `list-of` extended type is an implementation of the type of lists of some element type. This type cannot be expressed in the Common Lisp type system but is sometimes desired. In a little more detail, `(list-of x)` can be expressed recursively as being the object `nil` plus all objects of type `(cons x (list-of x))`. This includes circular lists, but not dotted lists.

Types for arrays and hash-tables of some element type(s) have also been defined as `array-of` and `hash-table-of`.

# Type-level functions

Expand Down
Loading