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

module LinearScan.Vector0 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.Datatypes as Datatypes
import qualified LinearScan.Logic as Logic
import qualified LinearScan.Fintype as Fintype



#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


#ifdef __GLASGOW_HASKELL__
type Any = GHC.Prim.Any
#else
-- HUGS
type Any = ()
#endif

__ :: any
__ = Prelude.error "Logical or arity value used"

type Vec a = Any

vnil :: ()
vnil =
  ()

vsing :: a1 -> (,) a1 ()
vsing x =
  (,) x ()

vcons :: Prelude.Int -> a1 -> (Vec a1) -> (,) a1 Any
vcons n x v =
  (,) x v

fin_contra :: Prelude.Int -> a1
fin_contra _top_assumption_ =
  let {_evar_0_ = \m -> Logic.coq_False_rect} in
  case _top_assumption_ of {
    x -> _evar_0_ x}

fin_rect :: Prelude.Int -> (() -> a1) -> (Prelude.Int -> () -> a1 -> a1) ->
            Prelude.Int -> a1
fin_rect n hz hSn _top_assumption_ =
  let {
   _evar_0_ = \m ->
    let {_evar_0_ = \_ -> hz __} in
    let {
     _evar_0_0 = \m0 iHm -> let {_evar_0_0 = iHm __} in hSn m0 __ _evar_0_0}
    in
    Datatypes.nat_rect _evar_0_ (\m0 iHm _ -> _evar_0_0 m0 iHm) m __}
  in
  case _top_assumption_ of {
    x -> _evar_0_ x}

vec_rect :: a2 -> (Prelude.Int -> a1 -> (Vec a1) -> a2 -> a2) -> Prelude.Int
            -> (Vec a1) -> a2
vec_rect hnil hcons n v =
  let {_evar_0_ = \hnil0 hcons0 v0 -> hnil0} in
  let {
   _evar_0_0 = \n0 iHn hnil0 hcons0 v0 ->
    let {
     _evar_0_0 = \_a_ _b_ ->
      let {_evar_0_0 = iHn hnil0 hcons0 _b_} in hcons0 n0 _a_ _b_ _evar_0_0}
    in
    case v0 of {
     (,) x x0 -> _evar_0_0 x x0}}
  in
  Datatypes.nat_rect (unsafeCoerce _evar_0_) (unsafeCoerce _evar_0_0) n hnil
    hcons v

vecn_rect :: (a1 -> a2) -> (Prelude.Int -> a1 -> ((,) a1 Any) -> a2 -> a2) ->
             Prelude.Int -> ((,) a1 Any) -> a2
vecn_rect hsing hcons n v =
  let {
   _evar_0_ = \hsing0 hcons0 v0 ->
    let {_evar_0_ = \a b -> hsing0 a} in
    case v0 of {
     (,) x x0 -> _evar_0_ x x0}}
  in
  let {
   _evar_0_0 = \n0 iHn hsing0 hcons0 v0 ->
    let {
     _evar_0_0 = \_a_ _b_ ->
      let {_evar_0_0 = iHn hsing0 hcons0 _b_} in hcons0 n0 _a_ _b_ _evar_0_0}
    in
    case v0 of {
     (,) x x0 -> _evar_0_0 x x0}}
  in
  Datatypes.nat_rect (unsafeCoerce _evar_0_) (unsafeCoerce _evar_0_0) n hsing
    hcons v

vec_to_seq :: Prelude.Int -> (Vec a1) -> [] a1
vec_to_seq n v =
  let {_evar_0_ = \v0 -> []} in
  let {
   _evar_0_0 = \n0 v0 ->
    let {_evar_0_0 = \x -> (:) x []} in
    let {_evar_0_1 = \sz x _v_ iHxs -> (:) x iHxs} in
    vecn_rect _evar_0_0 _evar_0_1 n0 v0}
  in
  (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
    (\_ ->
    _evar_0_ v)
    (\x ->
    unsafeCoerce _evar_0_0 x v)
    n

vfoldr_with_index :: Prelude.Int -> (Prelude.Int -> a1 -> a2 -> a2) -> a2 ->
                     (Vec a1) -> a2
vfoldr_with_index n f b v =
  let {_evar_0_ = \_discharged_f_ _discharged_v_ -> b} in
  let {
   _evar_0_0 = \n0 f0 v0 ->
    let {_evar_0_0 = \x -> f0 (Fintype.inord n0 n0) x b} in
    let {
     _evar_0_1 = \sz x xs iHxs ->
      f0 (Fintype.inord n0 ((Prelude.-) n0 ((Prelude.succ) sz))) x iHxs}
    in
    vecn_rect _evar_0_0 _evar_0_1 n0 v0}
  in
  (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
    (\_ ->
    _evar_0_ f v)
    (\x ->
    unsafeCoerce _evar_0_0 x f v)
    n

vfoldl_with_index :: Prelude.Int -> (Prelude.Int -> a2 -> a1 -> a2) -> a2 ->
                     (Vec a1) -> a2
vfoldl_with_index n f b v =
  let {_evar_0_ = \_discharged_f_ _discharged_v_ -> b} in
  let {
   _evar_0_0 = \n0 f0 v0 ->
    let {_evar_0_0 = \x b0 -> f0 (Fintype.inord n0 n0) b0 x} in
    let {
     _evar_0_1 = \sz x xs iHxs b0 ->
      iHxs (f0 (Fintype.inord n0 ((Prelude.-) n0 ((Prelude.succ) sz))) b0 x)}
    in
    vecn_rect _evar_0_0 _evar_0_1 n0 v0 b}
  in
  (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
    (\_ ->
    _evar_0_ f v)
    (\x ->
    unsafeCoerce _evar_0_0 x f v)
    n

vconst :: Prelude.Int -> a1 -> Vec a1
vconst n i =
  let {_evar_0_ = \n0 iHn -> vcons n0 i iHn} in
  Datatypes.nat_rect (unsafeCoerce vnil) (unsafeCoerce _evar_0_) n

vreplace :: Prelude.Int -> (Vec a1) -> Prelude.Int -> a1 -> Vec a1
vreplace n v p i =
  let {_evar_0_ = \v0 p0 -> fin_contra p0} in
  let {
   _evar_0_0 = \n0 v0 p0 ->
    let {_evar_0_0 = \x p1 -> vsing i} in
    let {
     _evar_0_1 = \_n_ x xs iHxs p1 ->
      let {_evar_0_1 = \_ -> vcons ((Prelude.succ) _n_) i xs} in
      let {
       _evar_0_2 = \p2 _the_2nd_wildcard_ ->
        vcons ((Prelude.succ) _n_) x (iHxs ( p2))}
      in
      fin_rect ((Prelude.succ) _n_) _evar_0_1 (\p2 _ _the_2nd_wildcard_ ->
        _evar_0_2 p2 _the_2nd_wildcard_) p1}
    in
    vecn_rect _evar_0_0 (unsafeCoerce _evar_0_1) n0 v0 p0}
  in
  (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
    (\_ ->
    _evar_0_ v p)
    (\x ->
    unsafeCoerce _evar_0_0 x v p)
    n

vnth :: Prelude.Int -> (Vec a1) -> Prelude.Int -> a1
vnth n v p =
  let {_evar_0_ = \v0 p0 -> fin_contra p0} in
  let {
   _evar_0_0 = \n0 v0 p0 ->
    let {_evar_0_0 = \x p1 -> x} in
    let {
     _evar_0_1 = \_n_ x _the_1st_wildcard_ iHxs p1 ->
      let {_evar_0_1 = \_ -> x} in
      let {_evar_0_2 = \p2 _the_2nd_wildcard_ -> iHxs ( p2)} in
      fin_rect ((Prelude.succ) _n_) _evar_0_1 (\p2 _ _the_2nd_wildcard_ ->
        _evar_0_2 p2 _the_2nd_wildcard_) p1}
    in
    vecn_rect _evar_0_0 _evar_0_1 n0 v0 p0}
  in
  (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
    (\_ ->
    _evar_0_ v p)
    (\x ->
    unsafeCoerce _evar_0_0 x v p)
    n

vmodify :: Prelude.Int -> (Vec a1) -> Prelude.Int -> (a1 -> a1) -> Vec a1
vmodify n v p f =
  vreplace n v p (f (vnth n v p))

vshiftin :: Prelude.Int -> (Vec a1) -> a1 -> (,) a1 Any
vshiftin n v i =
  let {_evar_0_ = vsing i} in
  let {_evar_0_0 = \_n_ x _v_ iHxs -> (,) x iHxs} in
  vec_rect (unsafeCoerce _evar_0_) (unsafeCoerce _evar_0_0) n v