linearscan-0.7.0: LinearScan/Graph.hs

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

module LinearScan.Graph where


import Debug.Trace (trace, traceShow)
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



#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 ([] (Prelude.Maybe Eqtype.Equality__Coq_sort)) ([]
                                                              Eqtype.Equality__Coq_sort) 
 (Eqtype.Equality__Coq_sort -> (,) (Prelude.Maybe Eqtype.Equality__Coq_sort)
 (Prelude.Maybe Eqtype.Equality__Coq_sort))

vertices :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> Graph
            -> [] (Prelude.Maybe Eqtype.Equality__Coq_sort)
vertices a b g =
  case g of {
   Build_Graph vertices0 edges0 edge_f0 -> vertices0}

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

edge_f :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> Graph ->
          Eqtype.Equality__Coq_sort -> (,)
          (Prelude.Maybe Eqtype.Equality__Coq_sort)
          (Prelude.Maybe Eqtype.Equality__Coq_sort)
edge_f a b g =
  case g of {
   Build_Graph vertices0 edges0 edge_f0 -> edge_f0}

emptyGraph :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type ->
              (Eqtype.Equality__Coq_sort -> (,)
              (Prelude.Maybe Eqtype.Equality__Coq_sort)
              (Prelude.Maybe Eqtype.Equality__Coq_sort)) -> Graph
emptyGraph a b f =
  Build_Graph [] [] f

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

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

removeEdge :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type ->
              Eqtype.Equality__Coq_sort -> Graph -> Graph
removeEdge a b x g =
  Build_Graph (vertices a b g)
    (Prelude.filter (\y -> Prelude.not (Eqtype.eq_op b y x)) (edges a b g))
    (edge_f a b g)

connections :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type ->
               (((,) (Prelude.Maybe Eqtype.Equality__Coq_sort)
               (Prelude.Maybe Eqtype.Equality__Coq_sort)) -> Prelude.Maybe
               Eqtype.Equality__Coq_sort) -> (Prelude.Maybe
               Eqtype.Equality__Coq_sort) -> Graph -> []
               Eqtype.Equality__Coq_sort
connections a b f x g =
  Prelude.filter
    ((Prelude..)
      ((Prelude..) (\y ->
        Eqtype.eq_op (Eqtype.option_eqType a) (unsafeCoerce y)
          (unsafeCoerce x)) f) (edge_f a b g)) (edges a b g)

outbound :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type ->
            (Prelude.Maybe Eqtype.Equality__Coq_sort) -> Graph -> []
            Eqtype.Equality__Coq_sort
outbound a b =
  connections a b Prelude.fst

inbound :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type ->
           (Prelude.Maybe Eqtype.Equality__Coq_sort) -> Graph -> []
           Eqtype.Equality__Coq_sort
inbound a b =
  connections a b Prelude.snd

tsort' :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type ->
          Prelude.Int -> ([] Eqtype.Equality__Coq_sort) -> ([]
          (Prelude.Maybe Eqtype.Equality__Coq_sort)) ->
          (Eqtype.Equality__Coq_sort -> [] Eqtype.Equality__Coq_sort) ->
          Graph -> [] Eqtype.Equality__Coq_sort
tsort' a b fuel l roots k g =
  (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
    (\_ ->
    Seq.rev l)
    (\fuel0 ->
    case edges a b g of {
     [] -> Seq.rev l;
     (:) e es ->
      case roots of {
       [] ->
        let {l0 = (:) (Prelude.snd (edge_f a b g e)) []} in
        let {g' = Prelude.foldr (addEdge a b) (removeEdge a b e g) (k e)} in
        case l0 of {
         [] -> [];
         (:) n s ->
          let {outEdges = outbound a b n g'} in
          case Data.List.foldl' (\acc e0 ->
                 case acc of {
                  (,) res g'' -> (,) ((:) e0 res) (removeEdge a b e0 g'')})
                 ((,) [] g') outEdges of {
           (,) res g'' ->
            let {
             outNodes = Prelude.map ((Prelude..) Prelude.snd (edge_f a b g))
                          outEdges}
            in
            let {
             s' = (Prelude.++) s
                    (Prelude.filter
                      ((Prelude..) Seq.nilp (\x -> inbound a b x g''))
                      outNodes)}
            in
            tsort' a b fuel0 ((Prelude.++) l res) s' k g''}};
       (:) n s ->
        let {l0 = (:) n s} in
        case l0 of {
         [] -> [];
         (:) n0 s0 ->
          let {outEdges = outbound a b n0 g} in
          case Data.List.foldl' (\acc e0 ->
                 case acc of {
                  (,) res g'' -> (,) ((:) e0 res) (removeEdge a b e0 g'')})
                 ((,) [] g) outEdges of {
           (,) res g'' ->
            let {
             outNodes = Prelude.map ((Prelude..) Prelude.snd (edge_f a b g))
                          outEdges}
            in
            let {
             s' = (Prelude.++) s0
                    (Prelude.filter
                      ((Prelude..) Seq.nilp (\x -> inbound a b x g''))
                      outNodes)}
            in
            tsort' a b fuel0 ((Prelude.++) l res) s' k g''}}}})
    fuel

topsort :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> Graph ->
           (Eqtype.Equality__Coq_sort -> [] Eqtype.Equality__Coq_sort) -> []
           Eqtype.Equality__Coq_sort
topsort a b g k =
  let {
   noInbound = let {
                xs = Prelude.map ((Prelude..) Prelude.snd (edge_f a b g))
                       (edges a b g)}
               in
               Prelude.filter (\x ->
                 Prelude.not
                   (Ssrbool.in_mem (unsafeCoerce x)
                     (Ssrbool.mem (Seq.seq_predType (Eqtype.option_eqType a))
                       (unsafeCoerce xs)))) (vertices a b g)}
  in
  tsort' a b ((Prelude.succ) (Data.List.length (vertices a b g))) []
    noInbound k g