;;; -*- Mode:Lisp; Syntax: Common-Lisp; Package:ONTOLINGUA-USER; Base:10 -*-

;;; Simple Geometry
;;; (c) 1993 Greg Olsen and Thomas Gruber

(in-package "ONTOLINGUA-USER")

(define-theory simple-geometry (quantity-spaces
				3D-tensor-quantities
				standard-dimensions)

"This theory attempts to capture basic geometric concepts used in mechanical
systems modelling.  These concepts include points, frames, position, and
orientation but exclude notions of extent (i.e. the modelling of surfaces or
solid geometry)."
  :issues ("(c) 1993, 1994 Gregory R. Olsen and Thomas R. Gruber"))

(in-theory 'simple-geometry)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; 3D-Length Space
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define-instance 3D-LENGTH-SPACE (quantity-space)
  "The set of points in three-dimensional space."
  :axiom-def (and (quantity-space 3D-LENGTH-SPACE)
		  (=> (and (member ?x1 3D-LENGTH-SPACE)
			   (member ?x2 3D-LENGTH-SPACE))
		      (quantity.dimension (distance ?x1 ?x2)
				 length-dimension))))


(define-class 3D-POINT (?pt)
  "A point in 3D space."
  :iff-def (point-in ?pt 3D-LENGTH-SPACE))


(define-class 3D-FRAME (?f)
  "A frame in 3D space.  A triad of orthonormal basis vectors."
  :iff-def (and (orthonormal-basis ?f)
		(basis.dimension ?f 3)))


(define-function DISTANCE (?p1 ?p2) :-> ?d
  "The distance function specialized to points in 3D space."
  :when (and (3D-POINT ?p1)
	     (3D-POINT ?p2))

  :iff-def (and (scalar-quantity ?d)
		(quantity.dimension ?d length-dimension)
		(= ?d
		   (sqrt (dot (position ?p1 ?p2)
			      (position ?p1 ?p2))))))


(define-function ORIENTATION (?f1 ?f2) :-> ?dircos

  "Function relating frames in space.  Returns a direction cosine
matrix.  An important property of orientation is the ability to
'chain' orientations through multiplication, (orientation ?f1
?f3) = (orientation ?f1 ?f2) * (orientation ?f2 ?f3)."

  :def (and (3D-FRAME ?f1)
	    (3D-FRAME ?f2)
	    (3D-DIRECTION-COSINE ?dircos)
	    (forall ?v
		    (=> (3D-vector-quantity ?v)
			(= (tensor-to-matrix ?v ?f1)
			   (* ?dircos
			      (tensor-to-matrix ?v ?f2)))))
	    (forall ?dyad
		    (=> (3D-dyad ?dyad)
			(= (tensor-to-matrix ?dyad ?f1)
			   (* (inverse ?dircos)
			      (* (tensor-to-matrix ?dyad ?f2)
				 ?dircos))))))
  
  :axiom-def (= (orientation ?f1 ?f3)
		(* (orientation ?f1 ?f2) 
		   (orientation ?f2 ?f3))))


(define-class 3D-DIRECTION-COSINE (?dircos)
  "A direction cosine matrix is an orthogonal three-dimensional matrix."
  :iff-def (and (orthogonal-matrix ?dircos)
		(row-dimension ?dircos 3)))


(define-function SIMPLE-ROTATION (?axis ?angle) :-> ?dircos

  "Shorthand for the commonly used direction cosine matrices that represent
rotations about the three axes in 3D space."

  :iff-def (and (member ?axis (setof 1 2 3))
	    (scalar-quantity ?angle)
            (quantity.dimension ?angle identity-dimension)
	    (3D-DIRECTION-COSINE ?dircos)
	    (=> (= ?axis 1)
		(= ?dircos
		   (matrix-of-rows
		    (matrix-of-columns 1 0 0)
		    (matrix-of-columns 0 (cos ?angle) (- (sin ?angle)))
		    (matrix-of-columns 0 (sin ?angle) (cos ?angle)))))
	    (=> (= ?axis 2)
		(= ?dircos
		   (matrix-of-rows
		    (matrix-of-columns (cos ?angle) 0 (- (sin ?angle)))
		    (matrix-of-columns 0 1 0)
		    (matrix-of-columns (sin ?angle) 0 (cos ?angle)))))
	    (=> (= ?axis 3)
		(= ?dircos
		   (matrix-of-rows
		    (matrix-of-columns (cos ?angle) (- (sin ?angle)) 0)
		    (matrix-of-columns (sin ?angle) (cos ?angle) 0)
		    (matrix-of-columns 0 0 1))))))


(define-function POSITION (?p1 ?p2) :-> ?pos-vec
  "Position is the vector from ?p1 to ?p2."
  :def (and (3D-POINT ?p1)
	    (3D-POINT ?p2)
	    (3D-VECTOR-QUANTITY ?pos-vec))

  :axiom-def (and 
	      (= (position ?p1 ?p3)
		 (+ (position ?p1 ?p2)
		    (position ?p2 ?p3)))
	      (zero-element (position ?p ?p))
	      (= (position ?p1 ?p2)
		 (- (position ?p2 ?p1)))))