Impressum patch-4.lisp

(defun get-current-imported-theories (id)
  (let* ((idstr (string id))
  (idlen (length idstr)))
    (when *current-context*
      (let ((theories nil))
 (map-lhash #'(lambda (x y)
         (declare (ignore y))
         (if (eq (id x) id)
      (push x theories)
      (when (and (library-rectype-theory? x)
          (let ((len (length (string (id x)))))
     (and (< idlen len)
          (string= id (id x) :end2 idlen))))
        (let ((adt (get-theory* id (lib-ref x))))
          (assert adt () "Should have found adt")
          (pushnew adt theories :test #'eq)))))
     (current-using-hash))
 theories))))

;(defun get-current-imported-theories (id)
;  (let* ((idstr (string id))
;  (idlen (length idstr)))
;    (when *current-context*
;      (let ((theories nil))
; (map-lhash #'(lambda (x y)
;        (declare (ignore y))
;        (if (eq (id x) id)
;    (push x theories)
;    (when (and (library-rectype-theory? x)
;       (let ((len (length (string (id x)))))
; (and (< idlen len)
;      (string= id (id x) :end2 idlen))))
;      (let* ((lib (libref-to-libid (lib-ref x)))
;     (adt (get-theory* id lib)))
;        (assert adt () "Should have found adt")
;        (pushnew adt theories :test #'eq)))))
;    (current-using-hash))
; theories))))

(defun get-adt-slot-value (te)
  ;; te must be a type-name
  (or (let ((dt (get-theory (id te))))
 (and (recursive-type? dt) dt))
      (find-if #'(lambda (d)
     (and (typep d 'recursive-type)
   (eq (id d) (id te))))
 (all-decls (module (declaration te))))
      (let ((enumtype (find-if #'(lambda (d)
       (and (typep d 'type-eq-decl)
     (eq (id d) (id te))
     (typep (type-expr d) 'recursive-type)))
   (all-decls (module (declaration te))))))
 (when enumtype
   (type-expr enumtype)))
      (let* ((adt-id (makesym "~a_adt" (id te)))
      (adt (get-theory adt-id))
      (dt (if adt
       (if (lib-ref adt)
    (get-theory* (id te)
          (libref-to-libid (lib-ref adt)))
    (break "get-adt-slot-value: no lib-ref"))
       (break "get-adt-slot-value: no adt"))))
 (and (recursive-type? dt) dt))
      (break "Can't restore")))