module CoverageCheck.Prelude where
infixr 5 _∷_
open import Haskell.Prelude public using
( Type; id; _∘_; _$_; flip; case_of_; undefined;
⊤; tt;
Bool; True; False; not; _&&_; _||_; if_then_else_;
Nat; zero; suc; _+_;
List; _++_; map; foldr; foldMap; elem; sum; concat; concatMap; lengthNat; null; iMonadList; reverse; foldl;
String;
_×_; _,_; fst; snd; uncurry;
Maybe; Just; Nothing; maybe;
Either; Left; Right; either;
Semigroup; _<>_;
Functor; DefaultFunctor; fmap;
Applicative; DefaultApplicative; pure; _<*>_; _<*_; _*>_;
Monad; DefaultMonad; _>>=_;
_≡_; refl )
pattern [] = List.[]
pattern _∷_ x xs = List._∷_ x xs
open import Haskell.Prim public using (⊥; the; Level; exFalso)
open import Haskell.Prim.Eq public using (Eq; _==_; _/=_; iEqList; iEqChar; iEqNat)
open import Haskell.Law.Eq public using
(IsLawfulEq; isEquality; eqReflexivity; iLawfulEqList; iLawfulEqChar; iLawfulEqNat)
open import Haskell.Prim.Foldable public using (iFoldableList; Foldable; any)
open import Haskell.Prim.List public using (scanl)
open import Haskell.Prim.Num public using (iNumNat)
open import Haskell.Prim.Ord public using (Ord; OrdFromLessThan; _<_; iOrdList; iOrdChar; iOrdNat)
open import Haskell.Law.Bool public using
(prop-x-||-True; prop-x-||-False; not-involution; not-not)
open import Haskell.Law.Equality public using
(cong; cong₂; subst; subst0; sym; trans)
open import Haskell.Law.List public using (map-++)
open import Haskell.Extra.Erase public using
(Erase; Erased; get; Σ0; ⟨_⟩_; <_>)
Σ0-syntax : (@0 a : Type) (b : @0 a → Type) → Type
Σ0-syntax a b = Σ0 a λ x → b x
syntax Σ0-syntax A (λ x → B) = Σ0[ x ∈ A ] B
infix 2 Σ0-syntax
{-# COMPILE AGDA2HS Σ0-syntax inline #-}
open import Haskell.Extra.Refinement public using
(∃; _⟨_⟩; value; proof; mapRefine)
∃-syntax : (a : Type) (@0 P : a → Type) → Type
∃-syntax a P = ∃ a λ x → P x
syntax ∃-syntax A (λ x → B) = ∃[ x ∈ A ] B
infix 2 ∃-syntax
{-# COMPILE AGDA2HS ∃-syntax inline #-}
open import Haskell.Extra.Sigma public using (Σ; Σ-syntax; _,_; fst; snd)
open import Haskell.Data.Foldable1 public using
( Foldable1; foldMap1 )
open import Haskell.Data.Bifunctor public using
( Bifunctor; bimap; first; second;
BifunctorFromBimap; BifunctorFromFirstSecond;
iBifunctorTuple; iBifunctorEither )
open import Haskell.Data.Bifoldable public using
( Bifoldable; bifoldMap; bifoldr; bifold;
BifoldableFromBifoldMap; BifoldableFromBifoldr;
iBifoldableTuple; iBifoldableEither )
open import Haskell.Data.Bifoldable1 public using
(Bifoldable1; bifoldMap1; bifold1; iBifoldable1Tuple; iBifoldable1Either)
open import CoverageCheck.Extra.Negation public
cong0 : {@0 a : Type} {b : Type} {@0 x y : a} (f : @0 a → b)
→ @0 x ≡ y
→ f x ≡ f y
cong0 f eq = subst0 (λ z → f _ ≡ f z) eq refl
mapListRefine : {a : Type} {@0 p q : a → Type}
→ (@0 f : ∀ {x} → p x → q x)
→ List (∃[ x ∈ a ] p x)
→ List (∃[ x ∈ a ] q x)
mapListRefine f [] = []
mapListRefine f (x ∷ xs) = mapRefine f x ∷ mapListRefine f xs
{-# COMPILE AGDA2HS mapListRefine transparent #-}
open import CoverageCheck.Data.List.Relation as Rel public
hiding ([]; _∷_)
pattern [] = Rel.[]
pattern _∷_ p ps = p Rel.∷ ps
open import CoverageCheck.Data.These public
open import Haskell.Data.List.NonEmpty as NE using (NonEmpty; _<|_)
pattern _∷_ x xs = x NE.:| xs
mapNonEmptyRefine : {a : Type} {@0 p q : a → Type}
→ (@0 f : ∀ {x} → p x → q x)
→ NonEmpty (∃[ x ∈ a ] p x)
→ NonEmpty (∃[ x ∈ a ] q x)
mapNonEmptyRefine f (x ∷ xs) = mapRefine f x ∷ mapListRefine f xs
{-# COMPILE AGDA2HS mapNonEmptyRefine transparent #-}
inits : {a : Type} → List a → List (List a)
inits = map reverse ∘ scanl (flip _∷_) []
inits1 : {a : Type} → List a → List (NonEmpty a)
inits1 [] = []
inits1 (x ∷ xs) = map (x ∷_) (inits xs)
open import CoverageCheck.Extra.Dec public
_≟_ : ∀ {a} {{_ : Eq a}} {{@0 _ : IsLawfulEq a}} → (x y : a) → Dec (x ≡ y)
x ≟ y = (x == y) ⟨ isEquality x y ⟩
{-# COMPILE AGDA2HS _≟_ inline #-}
open import CoverageCheck.Extra.DecP public