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


--One-way road
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
                    | 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)
  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
start = Node "start"
end = Node "end"  
theEdge = Edge  start end
theCar = Car start
theRoadElement = RoadElement theEdge
t1 = location (move theRoadElement theCar) == end



-- In prog1 
--  other (Edge (Node "start") (Node "end")) (Node "start")
-- gives end
-- In  prog1
-- other (Edge (Node "start") (Node "end")) (Node "end")
-- Gives Exception: not linked
-- 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.