-- Ontologies of One-way Roads by  Sumit Sen
-- http://ifgi.uni-muenster.de/~sumitsen/sen_Font05.pdf


-- Two way roads
class Link link object | link -> object where 
  from, to::link -> object
  other::Eq object => link -> object -> object
  other link object | object == from link = to link
                    | object == to  link = from link
                    | otherwise = error "not linked"

	
class Path path object where 
  move :: path -> object -> object 


class Named object name | object -> name where
 name :: object -> name

class  LocatedAt object  link where
 location :: object -> link

--Node
type Name = String
data Node = Node Name deriving (Eq, Show)

-- Edge: "A sequence of line segments with nodes at each end"
data Edge = Edge Node Node deriving Show


-- Car
data Car = Car Node deriving (Eq, Show)
type Cars = [Car]

-- a Node is a named object
instance Named Node Name where 
 name (Node n) = n
 
-- an Edge as Link between Nodes
instance Link Edge Node where
 from (Edge node1 node2) = node1
 to (Edge node1 node2) = node2
 

 -- a Car located at a Node
instance LocatedAt Car Node where
 location (Car node) = node


-- Road Element
data RoadElement = RoadElement Edge deriving Show




class (Path path conveyance ) => Conveyance conveyance path object where
 transport :: path -> conveyance -> object -> object


-- RoadElements as Links between Nodes
instance Link RoadElement Node where
 from (RoadElement edge) = from edge
 to (RoadElement edge) = to edge


-- RoadElements as Paths for Cars
instance Path RoadElement Car where
   move (RoadElement edge) (Car node) = Car (other edge node)
   

--  Algebraic specifications usually depend on (automatic) theorem provers for verification of specifications. 
--  For our case however type checking and executablity form the basis of verification of our specifications in Haskell. 
--  This is done by executing test scripts such as
-- As orignal paper
start = Node "start"
end = Node "end"  
theEdge = Edge  start end
theCar = Car start
theRoadElement = RoadElement theEdge
t1 = location (move theRoadElement theCar) == end

-- Some additional tests
-- If start end switched then no linked error
theEdge2 = Edge   start end
theEdge3 = Edge    end start
theCar2 = Car start
theCar3 = Car end
theRoadElement2 = RoadElement theEdge2
theRoadElement3 = RoadElement theEdge3
t2 = location (move theRoadElement2 theCar2) == end
t3 = location (move theRoadElement3 theCar3) == start
-- In prog2 
-- other (Edge (Node "start") (Node "end")) (Node "end")
-- gives start 
--  other (Edge (Node "start") (Node "end")) (Node "start")
-- gives end
-- Which is what we would expect for a two way street.

-- I can get t1, t2 and t3 to give expected results, but I *cannot* get the following to work
-- Thus t1 will be true if spec 1 is used and false if spec2 is used deciding if the road specification is of a one way road.