module LinearScan.Lib 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 LinearScan.Utils

import qualified LinearScan.Specif as Specif
import qualified LinearScan.Eqtype as Eqtype


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

option_choose :: (Prelude.Maybe a1) -> (Prelude.Maybe a1) -> Prelude.Maybe a1
option_choose x y =
  case x of {
   Prelude.Just a -> x;
   Prelude.Nothing -> y}

olast :: ([] a1) -> Prelude.Maybe a1
olast l =
  let {
   go res xs =
     case xs of {
      [] -> res;
      (:) x xs0 -> go (Prelude.Just x) xs0}}
  in go Prelude.Nothing l

maybeLookup :: Eqtype.Equality__Coq_type -> ([]
               ((,) Eqtype.Equality__Coq_sort a1)) ->
               Eqtype.Equality__Coq_sort -> Prelude.Maybe a1
maybeLookup a v x =
  case v of {
   [] -> Prelude.Nothing;
   (:) p xs ->
    case p of {
     (,) k v0 ->
      case Eqtype.eq_op a k x of {
       Prelude.True -> Prelude.Just v0;
       Prelude.False -> maybeLookup a xs x}}}

lebf :: (a1 -> Prelude.Int) -> a1 -> a1 -> Prelude.Bool
lebf f n m =
  (Prelude.<=) (f n) (f m)

type Coq_oddnum = Prelude.Int

odd1 :: Prelude.Int
odd1 =
  (Prelude.succ) 0

forFold :: a2 -> ([] a1) -> (a2 -> a1 -> a2) -> a2
forFold b v f =
  Data.List.foldl' f b v

forFoldr :: a2 -> ([] a1) -> (a1 -> a2 -> a2) -> a2
forFoldr b v f =
  Prelude.foldr f b v

catMaybes :: ([] (Prelude.Maybe a1)) -> [] a1
catMaybes l =
  forFoldr [] l (\mx rest ->
    case mx of {
     Prelude.Just x -> (:) x rest;
     Prelude.Nothing -> rest})

span :: (a1 -> Prelude.Bool) -> ([] a1) -> (,) ([] a1) ([] a1)
span p l =
  case l of {
   [] -> (,) [] [];
   (:) x xs ->
    case p x of {
     Prelude.True ->
      case span p xs of {
       (,) ys zs -> (,) ((:) x ys) zs};
     Prelude.False -> (,) [] l}}

partition :: (a1 -> Prelude.Bool) -> ([] a1) -> (,) ([] a1) ([] a1)
partition p =
  Prelude.foldr (\x acc ->
    case p x of {
     Prelude.True -> (,) ((:) x (Prelude.fst acc)) (Prelude.snd acc);
     Prelude.False -> (,) (Prelude.fst acc) ((:) x (Prelude.snd acc))}) ((,)
    [] [])

insert :: (a1 -> a1 -> Prelude.Bool) -> a1 -> ([] a1) -> [] a1
insert p z l =
  case l of {
   [] -> (:) z [];
   (:) x xs ->
    case p x z of {
     Prelude.True -> (:) x (insert p z xs);
     Prelude.False -> (:) z ((:) x xs)}}

sortBy :: (a1 -> a1 -> Prelude.Bool) -> ([] a1) -> [] a1
sortBy p l =
  case l of {
   [] -> [];
   (:) x xs -> insert p x (sortBy p xs)}

dep_foldl_inv :: (a1 -> Eqtype.Equality__Coq_type) -> a1 -> ([]
                 Eqtype.Equality__Coq_sort) -> Prelude.Int -> (a1 -> []
                 Eqtype.Equality__Coq_sort) -> (a1 -> a1 -> () ->
                 Eqtype.Equality__Coq_sort -> Eqtype.Equality__Coq_sort) ->
                 (a1 -> () -> Eqtype.Equality__Coq_sort -> ([]
                 Eqtype.Equality__Coq_sort) -> () -> Specif.Coq_sig2 
                 a1) -> a1
dep_foldl_inv e b v n q f f0 =
  let {filtered_var = (,) v n} in
  case filtered_var of {
   (,) l n0 ->
    case l of {
     [] -> b;
     (:) y ys ->
      (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
        (\_ ->
        b)
        (\n' ->
        let {filtered_var0 = f0 b __ y ys __} in
        let {ys' = Prelude.map (f b filtered_var0 __) ys} in
        dep_foldl_inv e filtered_var0 ys' n' q f f0)
        n0}}

dep_foldl_invE :: (a2 -> Eqtype.Equality__Coq_type) -> a2 -> ([]
                  Eqtype.Equality__Coq_sort) -> Prelude.Int -> (a2 -> []
                  Eqtype.Equality__Coq_sort) -> (a2 -> a2 -> () ->
                  Eqtype.Equality__Coq_sort -> Eqtype.Equality__Coq_sort) ->
                  (a2 -> () -> Eqtype.Equality__Coq_sort -> ([]
                  Eqtype.Equality__Coq_sort) -> () -> Prelude.Either 
                  a1 (Specif.Coq_sig2 a2)) -> Prelude.Either a1 a2
dep_foldl_invE e b v n q f f0 =
  let {filtered_var = (,) v n} in
  case filtered_var of {
   (,) l n0 ->
    case l of {
     [] -> Prelude.Right b;
     (:) y ys ->
      (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
        (\_ -> Prelude.Right
        b)
        (\n' ->
        let {filtered_var0 = f0 b __ y ys __} in
        case filtered_var0 of {
         Prelude.Left err -> Prelude.Left err;
         Prelude.Right s ->
          let {ys' = Prelude.map (f b s __) ys} in
          dep_foldl_invE e s ys' n' q f f0})
        n0}}