{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}

module LinearScan.Graph where


import Debug.Trace (trace, traceShow, traceShowId)
import qualified Prelude
import qualified Data.IntMap
import qualified Data.IntSet
import qualified Data.List
import qualified Data.Ord
import qualified Data.Functor.Identity
import qualified Hask.Utils

import qualified LinearScan.Eqtype as Eqtype
import qualified LinearScan.Seq as Seq
import qualified LinearScan.Ssrbool as Ssrbool
import qualified LinearScan.Ssrnat as Ssrnat



#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base as GHC.Base
import qualified GHC.Prim as GHC.Prim
#else
-- HUGS
import qualified LinearScan.IOExts as IOExts
#endif


#ifdef __GLASGOW_HASKELL__
--unsafeCoerce :: a -> b
unsafeCoerce = GHC.Base.unsafeCoerce#
#else
-- HUGS
--unsafeCoerce :: a -> b
unsafeCoerce = IOExts.unsafeCoerce
#endif

data Graph =
   Build_Graph ([] Eqtype.Equality__Coq_sort) ([]
                                              ((,) Eqtype.Equality__Coq_sort
                                              Eqtype.Equality__Coq_sort))

vertices :: Eqtype.Equality__Coq_type -> Graph -> []
            Eqtype.Equality__Coq_sort
vertices a g =
  case g of {
   Build_Graph vertices0 edges0 -> vertices0}

edges :: Eqtype.Equality__Coq_type -> Graph -> []
         ((,) Eqtype.Equality__Coq_sort Eqtype.Equality__Coq_sort)
edges a g =
  case g of {
   Build_Graph vertices0 edges0 -> edges0}

emptyGraph :: Eqtype.Equality__Coq_type -> Graph
emptyGraph a =
  Build_Graph [] []

addVertex :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_sort -> Graph
             -> Graph
addVertex a v g =
  let {vg = vertices a g} in
  Build_Graph
  (case Ssrbool.in_mem v (Ssrbool.mem (Seq.seq_predType a) (unsafeCoerce vg)) of {
    Prelude.True -> vg;
    Prelude.False -> (:) v vg}) (edges a g)

addEdge :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_sort -> Graph ->
           Graph
addEdge a e g =
  let {eg = edges a g} in
  Build_Graph (vertices a g)
  (case Ssrbool.in_mem e
          (Ssrbool.mem (Seq.seq_predType (Eqtype.prod_eqType a a))
            (unsafeCoerce eg)) of {
    Prelude.True -> eg;
    Prelude.False -> (:) (unsafeCoerce e) eg})

removeEdge :: Eqtype.Equality__Coq_type -> ((,) Eqtype.Equality__Coq_sort
              Eqtype.Equality__Coq_sort) -> Graph -> Graph
removeEdge a x g =
  Build_Graph (vertices a g)
    (unsafeCoerce
      (Seq.rem (Eqtype.prod_eqType a a) (unsafeCoerce x)
        (unsafeCoerce (edges a g))))

outbound :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_sort -> Graph
            -> [] ((,) Eqtype.Equality__Coq_sort Eqtype.Equality__Coq_sort)
outbound a x g =
  Prelude.filter (\e -> Eqtype.eq_op a x (Prelude.fst e)) (edges a g)

inbound :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_sort -> Graph ->
           [] ((,) Eqtype.Equality__Coq_sort Eqtype.Equality__Coq_sort)
inbound a x g =
  Prelude.filter (\e -> Eqtype.eq_op a x (Prelude.snd e)) (edges a g)

removeVertex :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_sort ->
                Graph -> Graph
removeVertex a v g =
  Prelude.foldr (removeEdge a) (Build_Graph (Seq.rem a v (vertices a g))
    (edges a g)) ((Prelude.++) (inbound a v g) (outbound a v g))

topsort :: Eqtype.Equality__Coq_type -> (Eqtype.Equality__Coq_sort ->
           Prelude.Bool) -> (Eqtype.Equality__Coq_sort -> Graph -> Graph) ->
           Graph -> [] Eqtype.Equality__Coq_sort
topsort a splittable split g0 =
  let {
   go fuel g =
     (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
       (\_ ->
       vertices a g)
       (\fuel0 ->
       let {
        noInbound = Prelude.filter (\v -> Seq.nilp (inbound a v g))
                      (vertices a g)}
       in
       case noInbound of {
        [] ->
         case vertices a g of {
          [] -> [];
          (:) v vs ->
           case Prelude.filter (\x -> splittable x) ((:) v vs) of {
            [] -> vertices a g;
            (:) x l -> go fuel0 (split x g)}};
        (:) s l ->
         (Prelude.++) noInbound
           (go fuel0 (Prelude.foldr (removeVertex a) g noInbound))})
       fuel}
  in go (Ssrnat.double (Data.List.length (vertices a g0))) g0