#|Alan Rector says:

The whole point of this case is something that can be invoked for
the simple cases that don't involve additional restrictions on
the class that reifies the property.  It arose as part of the
notion of a "close to user form" or "intermediate representation"
so as to allow people to say, most of the time, 

"hasSeverity SOME Severe" 
rather than 
"hasFeature SOME (Severity AND (hasValue SOME Severe))".

In those cases where you really do need the reification - as in
your example - the macro is irrelevant - e.g. in this example

hasFeature SOME (Severity AND (hasValue SOME Severe) AND (hasTrend SOME GettingWorse))
|#

(in-package :cl-user)

(defun internal-compound-name (&rest names) ; hack -really should use full names concatenated rather than trailing portion
  "namespace of the last followed by * joined(.)names"
  (let ((take-name-space-from (car (last names))))
    (if (keywordp take-name-space-from)
	(setq take-name-space-from (nth (- (length names) 2) names)))
    (make-uri (format nil "~a#_~{~a~^.~}"
		      (#"replaceAll" (uri-full take-name-space-from) "#.*" "") 
		      (mapcar (lambda(name) (if (keywordp name)
						(string-downcase (string name))
						(#"replaceAll" (uri-full name) "^.*[/#:](?=.)" "")))
			      names)))))

(defun property-property (onproperty propdef &optional domain) ; hack - domain should be looked up
  (let* ((prop-def-name (second propdef))
	(new-prop-def-name (internal-compound-name onproperty prop-def-name)) ; left.stoichiometry
	(reified-property-class-name (internal-compound-name  !reified onproperty))
	(reified-property-slot (internal-compound-name !has.reified onproperty))
	(propdomain (and domain (domain domain))))
    (list
     (class reified-property-class-name :partial)
     (object-property reified-property-slot propdomain (range reified-property-class-name))

;; don't think this is necessary
;;      (equivalent-classes (intersection-of 
;; 			  (restriction reified-property-slot (min-cardinality 1))
;; 			  (restriction onproperty (min-cardinality 1)))
;; 			 (restriction onproperty (min-cardinality 1)))
;     (equivalent-classes (restriction reified-property-slot (some-values-from !owl:Thing))
;			 (restriction onproperty (some-values-from !owl:Thing)))

     (let ((new-propdef (copy-list propdef)))
       (when propdomain 
	 (setq new-propdef (list (car new-propdef) domain (cdr new-propdef))))
       (setf (second new-propdef) new-prop-def-name)
       (list new-propdef
	     (object-property (internal-compound-name onproperty :value) :functional)
	     )))))

(defun individual-with-reified-property (name &rest args &aux propprops)
  (setq args (eval-uri-reader-macro args))
  (let* ((main-ind 
	  (list* :individual name
		 (loop for arg in args
		    for  target = (and (consp arg) (caddr arg))
		    if (and (consp arg) (eq (car arg) :value)
			    (consp (second arg)))
		    collect (list :value (car (second arg)) target) and 
		    do (push  (cdr arg)  propprops)
		    else collect arg
		    ))))
    (if propprops
	(cons (append main-ind
		      (loop for ((prop) target) in propprops collect
			   (value (internal-compound-name :has.reified prop)
				  (internal-compound-name name prop target))))
	      (loop for ((reified-property) target) in propprops 
		 for propprop-values =  (remove-if-not (lambda(p) (eq (caar p) reified-property)) propprops)
		 collect
		 (list* :individual (internal-compound-name name reified-property target)
			(list :type (internal-compound-name !reified reified-property) )
			(value (internal-compound-name reified-property :value) target)
			(loop for ((reified-property proprop value)) in propprop-values
			   collect (value (internal-compound-name reified-property proprop) value)))
		 ))
      main-ind)))

(eval '(advise individual (apply 'individual-with-reified-property (cdr (:do-it))) :when :around :name :reified-property))

(defun restriction-with-reified-property (property axiom)
  (if (consp property)
      (let* ((property (eval-uri-reader-macro property))
	     (restriction (intersection-of  (restriction (car property)  axiom)
					    (restriction (internal-compound-name :has :reified (car property))
							 (some-values-from
							  (intersection-of
							   (restriction (internal-compound-name (car property) (second property)) (eval (third property)))
							   (restriction (internal-compound-name (car property) :value) axiom)
							   ))))))
	restriction)
      (list :restriction property axiom)))

(eval '(advise restriction (apply 'restriction-with-reified-property (cdr (:do-it))) :when :around :name :reified-property))

(defun reified-severity-example ()
  (with-ontology severe-reification ()
      ((value-partition '(!Trend !GettingWorse (!GettingBetter !GettingMuchBetter)))
       (value-partition '(!Degree !Severe !Mild))
       (object-property !hasSeverity)
       (property-property !hasSeverity (object-property !hasTrend))
       (class !probe1 :complete (restriction !hasSeverity (some-values-from !Severe)))
       (class !probe2 :complete 
	      (restriction
	       '(!hasSeverity !hasTrend (some-values-from !GettingBetter))
	       (some-values-from !Severe)))
       (class !probe3 :complete 
	      (restriction '(!hasSeverity !hasTrend (some-values-from !GettingMuchBetter)) 
			   (some-values-from !Severe)))
       (individual !gettingBetter1 (type !GettingBetter))
       (individual !severe1 (type !Severe))
       (individual !probe4 (value '(!hasSeverity !hasTrend !gettingBetter1) !severe1))
       (individual !probe5 (value !hasSeverity !severe1)))
					;  (print-db (descendants !probe2))
					;  (describe !probe2)
    (show-classtree severe-reification :include-instances t)
					;  (princ (abstract-syntax severe-reification))
    (write-rdfxml severe-reification)
					;  (print-db (check severe-reification))
					;  (pprint (multiple-value-list (get-owl-species (kb severe-reification))))
    ))