library Ontology/GUM/test/GUMFullwithDCC
version 0.3

from Ontology/GUM/GUM get GUM_Spatial_Relations
from Ontology/GUM/OrientationCalculi get DoubleCrossCalculus

spec GUMwithDCC =
	GUM_Spatial_Relations
	and
	DoubleCrossCalculus

then

	%% definition of frames of reference for interpretation
	free type FrameOfReference ::= intrinsic | relative | absolute
	ops
		%% mapping from the spatial modality to a frame of reference to fix the perspective in the interpretation
		referenceOfModality : SpatialModality -> FrameOfReference;
		%% e-connection for mapping GUM spatial modalities to DCC (15) orientations
		modalityToOrientation : SpatialModality -> OrientationDCC

	forall x,y: SpatialModality
		. modalityToOrientation(x) = modalityToOrientation(y)  =>  x = y   %% injective mapping

then

	forall fp: FrontProjection
		. referenceOfModality(fp) = intrinsic  =>
			   modalityToOrientation(fp) = atExit
			\/ modalityToOrientation(fp) = front
			\/ modalityToOrientation(fp) = onCourse
			\/ modalityToOrientation(fp) = left
			\/ modalityToOrientation(fp) = leftFront
			\/ modalityToOrientation(fp) = right
			\/ modalityToOrientation(fp) = rightFront

		. referenceOfModality(fp) = relative  =>
			   modalityToOrientation(fp) = onCourse
			\/ modalityToOrientation(fp) = left
			\/ modalityToOrientation(fp) = leftAtEntry
			\/ modalityToOrientation(fp) = leftBack
			\/ modalityToOrientation(fp) = right
			\/ modalityToOrientation(fp) = rightAtEntry
			\/ modalityToOrientation(fp) = rightBack

	forall bp: BackProjection
		. referenceOfModality(bp) = intrinsic  =>
			   modalityToOrientation(bp) = back
			\/ modalityToOrientation(bp) = leftBack
			\/ modalityToOrientation(bp) = rightBack

		. referenceOfModality(bp) = relative  =>
			   modalityToOrientation(bp) = front
			\/ modalityToOrientation(bp) = leftFront
			\/ modalityToOrientation(bp) = rightFront

	forall lp: LeftProjection
		. referenceOfModality(lp) = intrinsic  =>
			   modalityToOrientation(lp) = left
			\/ modalityToOrientation(lp) = leftAtEntry
			\/ modalityToOrientation(lp) = leftAtExit
			\/ modalityToOrientation(lp) = leftBack
			\/ modalityToOrientation(lp) = leftFront

		. referenceOfModality(lp) = relative  =>
			   modalityToOrientation(lp) = left
			\/ modalityToOrientation(lp) = leftAtEntry
			\/ modalityToOrientation(lp) = leftAtExit
			\/ modalityToOrientation(lp) = leftFront
			\/ modalityToOrientation(lp) = leftBack

	forall rp: RightProjection
		. referenceOfModality(rp) = intrinsic  =>
			   modalityToOrientation(rp) = right
			\/ modalityToOrientation(rp) = rightAtEntry
			\/ modalityToOrientation(rp) = rightAtExit
			\/ modalityToOrientation(rp) = rightFront
			\/ modalityToOrientation(rp) = rightBack

		. referenceOfModality(rp) = relative  =>
			   modalityToOrientation(rp) = right
			\/ modalityToOrientation(rp) = rightAtEntry
			\/ modalityToOrientation(rp) = rightAtExit
			\/ modalityToOrientation(rp) = rightFront
			\/ modalityToOrientation(rp) = rightBack


then
	ops
		%% e-connection for mapping GUM simple things (locatum and relatum) to DCC points
		simpleThingToLocation : SimpleThing -> Location;

	%% define simpleThingToLocation as functional
	forall a: SimpleThing; b,c: Location
		. b = simpleThingToLocation(a) /\ c = simpleThingToLocation(a)  =>  b = c

%% example

	forall lp: LeftProjection
        . modalityToOrientation(lp) = leftFront

	forall gl: GeneralizedLocation; sl: SpatialLocating; lp: LeftProjection; orient: Orientation8; st1, st2, st3: SimpleThing; v, w: Arrow
		. v = simpleThingToLocation(st1) --> simpleThingToLocation(st2) /\ w = simpleThingToLocation(st2) --> simpleThingToLocation(st3) /\ locatum(sl, st3) /\ placement(sl, gl) /\ relatum(gl, st2) /\ hasSpatialModality(gl, lp) /\ modalityToOrientation(lp) = orient /\ not(st1 = st2) /\ not(st1 = st3) /\ not(st2 = st3) =>
			v # w > orient

end


%% example proof

spec GUMwithDCC_example_house_tree =
	GUMwithDCC
then
	ops
		sl              : SpatialLocating;
		house, tree, me : SimpleThing;
		gl              : GeneralizedLocation;
		lp              : LeftProjection;
		u, v, w         : Arrow;

	. not(me = house)
	. not(me = tree)
	. not(house = tree) 
	. locatum(sl, tree)
	. placement(sl, gl)
	. relatum(gl, house)
	. hasSpatialModality(gl, lp)

	. v = simpleThingToLocation(me)    --> simpleThingToLocation(house)
	. w = simpleThingToLocation(house) --> simpleThingToLocation(tree)
	. u = simpleThingToLocation(me)    --> simpleThingToLocation(tree)

then %implies
	. v = simpleThingToLocation(me) --> simpleThingToLocation(house) /\ w = simpleThingToLocation(house) --> simpleThingToLocation(tree) /\ locatum(sl, tree) /\ placement(sl, gl) /\ relatum(gl, house) /\ hasSpatialModality(gl, lp) /\ modalityToOrientation(lp) = leftFront
	. v # w > leftFront
	. (v|w=leftFront /\ v|u=leftFront)
end