module Library where

open import Level public renaming (zero to lzero; suc to lsuc)
open import Size  public

open import Data.Bool.Base public using (Bool; true; false; if_then_else_; not; _∧_; _∨_)
open import Data.List.Base public using (List; []; _∷_)
module List = Data.List.Base
open import Data.Maybe public using (Maybe; nothing; just)
open import Data.Nat.Base public using (; zero; suc)
open import Data.Product public using (_×_; _,_; proj₁; proj₂)
open import Data.Sum public using (_⊎_; inj₁; inj₂)
open import Data.Unit public using ()

open import Data.Fin public using (Fin; zero; suc)
open import Data.Vec public using (Vec; []; _∷_)

open import Relation.Nullary public using (Dec; yes; no)
open import Relation.Nullary.Decidable public using (⌊_⌋)
open import Relation.Binary public
open import Relation.Binary.PropositionalEquality public using (_≡_; refl; sym; trans)
import Relation.Binary.EqReasoning
module EqR = Relation.Binary.EqReasoning

open import Data.Bool.Properties public using (isBooleanAlgebra)
open import Algebra public using (IdempotentCommutativeMonoid)
open import Algebra.Structures public using (module IsBooleanAlgebra; module IsDistributiveLattice; module IsLattice)
open IsBooleanAlgebra isBooleanAlgebra public using (∧-cong; ∧-comm; ∧-assoc; ∨-cong; ∨-comm; ∨-assoc; ∨-∧-distribʳ; isDistributiveLattice; isLattice) -- renaming (∨-idempotent to ∨-idem)

open import Algebra.Properties.Lattice (record { isLattice = isLattice }) public using () renaming (∨-idempotent to ∨-idem)

open import Algebra.Properties.DistributiveLattice (record { isDistributiveLattice = isDistributiveLattice }) public
import Algebra.IdempotentCommutativeMonoidSolver
module ICMSolver = Algebra.IdempotentCommutativeMonoidSolver

-- These names are not exported from Algebra.Properties.DistributiveLattice
∨-∧-distribˡ = proj₁ ∨-∧-distrib
∧-∨-distribˡ = proj₁ ∧-∨-distrib
∧-∨-distribʳ = proj₂ ∧-∨-distrib

module Vec where

  open Data.Vec public

  any : ∀{n}  Vec Bool n  Bool
  any = foldr  _  Bool) _∨_ false

  -- Get all indices which map to true.  [ i | v[i] = true ]
  trues : ∀{n}  Vec Bool n  List (Fin n)
  trues v = proj₂ (List.filter proj₁ (toList (zip v (allFin _))))

  ∨-permute : ∀{n}  Vec Bool n  (Fin n  Fin n)  Vec Bool n
  ∨-permute v f = List.foldl setTrue allFalse ( f (trues v))
    allFalse = replicate false
    setTrue = λ v i  v [ i ]≔ true