-- Sergio Antoy and Michael Hanus
-- Wed Apr  6 16:15:41 PDT 2011
-- Shortest itinerary (path in a weighted directed graph)


import List
import SetFunctions
import Quantification

infixl 5 :.

(:.) hours minutes = 60*hours + minutes

data Cities = Portland | Frankfurt | Amsterdam | Hamburg
data Flights = LH469 | NWA92 | LH10 | KL1783

flight
  = (LH469, Portland, Frankfurt,10:.15)
  ? (NWA92, Portland, Amsterdam,10:.00)
  ? (LH10, Frankfurt,Hamburg,1:.00)
  ? (KL1783,Amsterdam,Hamburg, 1:.52)

itinerary orig dest 
   | flight =:= (num,orig,dest,len)
   = [num]
  where num, len free
itinerary orig dest 
   | flight =:= (num1,orig,x,len1)
   & flight =:= (num2,x,dest,len2)
   = [num1,num2]
  where num1, len1, num2, len2, x free

duration [num]
   | flight =:= (num,orig,dest,len)
   = len
   where orig,dest,len free

duration [num1,num2] = duration [num1] + duration [num2]

shortestItin s e 
   | isEmpty (shortestItinThanSet (duration it))
   = it
   where it = itinerary s e
         shortestItinThan itduration
            | duration its < itduration
            = its
            where its = itinerary s e
         shortestItinThanSet d = set1 shortestItinThan d

fastShortestItin s e 
   = minValue shorter (itinerarySet s e)
   where shorter it1 it2 = duration it1 <= duration it2
         itinerarySet s e = set2 itinerary s e

test1 = shortestItin Portland Hamburg
test2 = fastShortestItin Portland Hamburg

solve1 s e 
   | exists r (\it -> 
        notExists (set2 itinerary s e) (\its -> 
           duration its < duration it))
   = r
   where r = itinerary s e

test3 = solve1 Portland Hamburg

solve2 s e 
   | exists r (\it -> 
        forall (set2 itinerary s e) (\its -> 
           duration its >= duration it))
   = r
   where r = itinerary s e

test4 = solve2 Portland Hamburg