text:
open import Prelude
open import Nat
open import dynamics-core
open import contexts
open import lemmas-disjointness

module dom-eq where
  -- main definition: two contexts are domain-equal when they produce (Some
  -- x) on the same indices. note that the context need not map indices to
  -- even the same type of contents; this is just a property about the
  -- domains. the proofs that follow establish that this property is
  -- respected in the appropriate ways by the context maniupulation
  -- operators we use in the other judgements.
  dom-eq : {A B : Set} → A ctx → B ctx → Set
  dom-eq {A} {B} C1 C2 = ((n : Nat) → Σ[ x ∈ A ]( C1 n == Some x) → (Σ[ y ∈ B ](C2 n == Some y)))×
                         ((n : Nat) → Σ[ y ∈ B ]( C2 n == Some y) → (Σ[ x ∈ A ](C1 n == Some x)))

  -- the empty context has the same domain as itself
  dom-∅ : {A B : Set} → dom-eq (λ _ → None {A}) (λ _ → None {B})
  dom-∅ {A} {B} = (λ n x → abort (somenotnone (! (π2 x)))) , (λ n x → abort (somenotnone (! (π2 x))))

  -- the singleton contexts formed with any contents but the same index has
  -- the same domain
  dom-single : {A B : Set} (x : Nat) {a : A} {b : B} → dom-eq (■ (x , a)) (■ (x , b))
  dom-single {A} {B} x {α} {β} = (λ n x₁ → β , (ap1 (λ qq → (■ (qq , β)) n) (! (lem-dom-eq x₁)) · x∈■ _ _)) ,
                             (λ n x₁ → α , (ap1 (λ qq → (■ (qq , α)) n) (! (lem-dom-eq x₁)) · x∈■ _ _))

  -- if two disjoint contexts each share a domain with two others, those
  -- are also disjoint.
  dom-eq-disj : {A B : Set} {Δ1 Δ2 : A ctx} {H1 H2 : B ctx} →
              H1 ## H2 →
              dom-eq Δ1 H1 →
              dom-eq Δ2 H2 →
              Δ1 ## Δ2
  dom-eq-disj {A} {B} {Δ1} {Δ2} {H1} {H2} (d1 , d2) (de1 , de2) (de3 , de4) = guts1 , guts2
    where
      guts1 : (n : Nat) → dom Δ1 n → n # Δ2
      guts1 n dom1 with ctxindirect H2 n
      guts1 n dom1 | Inl x = abort (somenotnone (! (π2 x) · d1 n (de1 n dom1)))
      guts1 n dom1 | Inr x with ctxindirect Δ2 n
      guts1 n dom1 | Inr x₁ | Inl x = abort (somenotnone (! (π2 (de3 n x)) · x₁))
      guts1 n dom1 | Inr x₁ | Inr x = x

      guts2 : (n : Nat) → dom Δ2 n → n # Δ1
      guts2 n dom2 with ctxindirect H1 n
      guts2 n dom2 | Inl x = abort (somenotnone (! (π2 x) · d2 n (de3 n dom2)))
      guts2 n dom2 | Inr x with ctxindirect Δ1 n
      guts2 n dom2 | Inr x₁ | Inl x = abort (somenotnone (! (π2 (de1 n x)) · x₁))
      guts2 n dom2 | Inr x₁ | Inr x = x

  -- if two sets share a domain with disjoint sets, then their union shares
  -- a domain with the union
  dom-union : {A B : Set} {Δ1 Δ2 : A ctx} {H1 H2 : B ctx} →
              H1 ## H2 →
              dom-eq Δ1 H1 →
              dom-eq Δ2 H2 →
              dom-eq (Δ1 ∪ Δ2) (H1 ∪ H2)
  dom-union {A} {B} {Δ1} {Δ2} {H1} {H2} disj (p1 , p2) (p3 , p4) = guts1 , guts2
    where
      guts1 : (n : Nat) →
                 Σ[ x ∈ A ] ((Δ1 ∪ Δ2) n == Some x) →
                 Σ[ y ∈ B ] ((H1 ∪ H2) n == Some y)
      guts1 n (x , eq) with ctxindirect Δ1 n
      guts1 n (x₁ , eq) | Inl x with p1 n x
      ... | q1 , q2 = q1 , x∈∪l H1 H2 n q1 q2
      guts1 n (x₁ , eq) | Inr x with p3 n (_ , lem-dom-union-apt1 {Δ1 = Δ1} {Δ2 = Δ2} x eq)
      ... | q1 , q2 =  q1 , x∈∪r H1 H2 n q1 q2 (π2 disj n (q1 , q2))

      guts2 : (n : Nat) →
                 Σ[ y ∈ B ] ((H1 ∪ H2) n == Some y) →
                 Σ[ x ∈ A ] ((Δ1 ∪ Δ2) n == Some x)
      guts2 n (x , eq) with ctxindirect H1 n
      guts2 n (x₁ , eq) | Inl x with p2 n x
      ... | q1 , q2 = q1 , x∈∪l Δ1 Δ2 n q1 q2
      guts2 n (x₁ , eq) | Inr x with p4 n (_ , lem-dom-union-apt2 {Δ1 = H2} {Δ2 = H1} x (tr (λ qq → qq n == Some x₁) (∪comm H1 H2 disj) eq))
      ... | q1 , q2 with ##-comm (dom-eq-disj disj (p1 , p2) (p3 , p4))
      ... | π3 , π4 = q1 , x∈∪r Δ1 Δ2 n q1 q2 (π3 n (q1 , q2))

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude

-- To enable reasoning about algorithms that concatenate
-- ByteStrings and pass the result to a cryptographic hash
-- function (as LibraBFT does), it is critical to have an
-- injective bitstring concat function ('bs-concat', below).
--
-- To see why, suppose we hash a data structure that contains two
-- fields of type ByteString by passing its fields to a hash
-- function like this:
--
-- > h : String -> String -> Hash
-- > h a b = hash (concat [a , b])
--
-- This function is /NOT/ collision resistant:
--
-- > h "xx" "x" == hash (concat ["xx" , "x"])
-- >            == hash "xxx"
-- >            == hash (concat ["x" , "xx"]) == h "x" "xx"
--
-- We cannot solve the problem simply by using an arbitrary field
-- separator, because an arbitrary ByteString might contain the
-- separator.  For example, if we define:
--
-- > h a b = hash (concat [ a , ";" , b ])
--
-- Then, we still have:
--
-- > h "x;x" "x" == h "x" "x;x"
--
-- Two possible approaches to defining an injective `concat`
-- function are:
--
-- 1) Use some length-prefixed encoding where we know the size of
-- each field. This approach will work in practice but we won't
-- be able to prove its injectivity for arbitrary ByteStrings in
-- Agda: Regardless of how many bytes we reserve for size
-- information, there are some inputs that require more.
--
-- 2) Encoding the arguments' list structure in the result of
-- concat; inverting the concat function then becomes parsing a
-- list of values. This approach is analogous to:
--
-- > concat : List ByteString -> BitString
-- > concat = serialize . toJSON
--
-- We take the second approach.
module LibraBFT.Base.ByteString where

  -- A BitString is a list of bits
  BitString : Set
  BitString = List Bool

  -- A ByteString is a list of bytes
  ByteString : Set
  ByteString = List (Vec Bool 8)

  _≟ByteString_ : (bs1 bs2 : ByteString) → Dec (bs1 ≡ bs2)
  _≟ByteString_ = List-≡-dec (Vec-≡-dec _≟Bool_)

  -- Concatenates ByteString prepending '11' to each byte.
  toBitString-pad' : ByteString → BitString
  toBitString-pad' = concat ∘ List-map (λ v → true ∷ true ∷ Vec-toList v)

  -- Concatenates a ByteString distinguishing an empty list from a non-empty list
  toBitString-pad : ByteString → BitString
  toBitString-pad []       = false ∷ false ∷ []
  toBitString-pad (b ∷ bs) = true  ∷ false ∷ Vec-toList b ++ toBitString-pad' bs

  -- Here's our injective concat function for ByteString
  bs-concat : List ByteString -> BitString
  bs-concat = concat ∘ List-map toBitString-pad

  -----------------------
  -- Injectivity Proof --
  -----------------------

  -- The proof is straightforward once we figure out the core reasoning principle:
  -- Any non-injective cases would be some variation on:
  --
  --         bs-concat ([a] ∷ c) ≡ bs-concat ([b₀ , b₁] ∷ d)
  --
  --    <==> toBitString-pad [a] ++ bs-concat c ≡ toBitString-pad [b₀ , b₁] ++ bs-concat d
  --
  --    <==> 1 1 a₀ ⋯ a₇ ++ bs-concat c ≡ 1 1 b₀₀ ⋯ b₀₇ 1 0 b₁₀ ⋯ b₁₇ ++ bs-concat d
  --
  --         { ++ is injective for same-length prefixes }
  --
  --    <==> aᵢ ≡ b₀ᵢ × bs-concat c ≡ 1 0 b₁₀ ⋯ b₁₇ ++ bs-concat d
  --
  --         { impossible,  bs-concat c is either empty or starts with 11 }
  --
  --    <==> ⊥
  --
  -- The actual Agda is a little more involved; but this covers the intuition.

  -- Appending two lists of the same length is injective.
  ++-len-injective : ∀{a}{A : Set a}(xs₀ ys₀ : List A){xs₁ ys₁ : List A}
               → length xs₀ ≡ length ys₀
               → xs₀ ++ xs₁ ≡ ys₀ ++ ys₁
               → xs₀ ≡ ys₀ × xs₁ ≡ ys₁
  ++-len-injective [] [] len hyp = refl , hyp
  ++-len-injective (x ∷ xs0) (y ∷ ys0) len hyp
    = let x≡y , tails≡ = ∷-injective hyp
          a , b = ++-len-injective xs0 ys0 (suc-injective len) tails≡
       in cong₂ _∷_ x≡y a , b

  Vec-toList-length : ∀{a n}{A : Set a}(x : Vec A n) → length (Vec-toList x) ≡ n
  Vec-toList-length []       = refl
  Vec-toList-length (_ ∷ xs) = cong suc (Vec-toList-length xs)

  Vec-toList-inj : ∀{a n}{A : Set a}{x y : Vec A n}
                 → Vec-toList x ≡ Vec-toList y → x ≡ y
  Vec-toList-inj {x = []}     {[]}     hyp = refl
  Vec-toList-inj {x = x ∷ xs} {y ∷ ys} hyp
    = let x≡y , xs≡ys = ∷-injective hyp
       in cong₂ _∷_ x≡y (Vec-toList-inj xs≡ys)

  -- In general, _++_ is not injective.  However, we can
  -- characterize it universally with a /Prefix/ property.
  data _≺_ {a}{A : Set a} : List A → List A → Set where
    z≺n : ∀{xs}      → [] ≺ xs
    s≺s : ∀{x xs ys} → xs ≺ ys → (x ∷ xs) ≺ (x ∷ ys)

  -- Returns the tail of ys; after dropping the prefix xs.
  ≺-drop : ∀{a}{A : Set a}{xs ys : List A} → xs ≺ ys → List A
  ≺-drop {ys = ys} z≺n = ys
  ≺-drop (s≺s a)       = ≺-drop a

  ++-≺ : ∀{a}{A : Set a}(xs ws : List A){ys zs : List A}
       → xs ++ ys ≡ ws ++ zs
       → Σ (xs ≺ ws) (λ prf → ≺-drop prf ++ zs ≡ ys)
       ⊎ Σ (ws ≺ xs) (λ prf → ≺-drop prf ++ ys ≡ zs)
  ++-≺ [] ys hyp = inj₁ (z≺n , sym hyp)
  ++-≺ (x ∷ xs) [] hyp = inj₂ (z≺n , hyp)
  ++-≺ (x ∷ xs) (y ∷ ys) hyp
    with ∷-injective hyp
  ...| refl , xs≡ys
    with ++-≺ xs ys xs≡ys
  ...| inj₁ (ok , prf) = inj₁ (s≺s ok , prf)
  ...| inj₂ (ok , prf) = inj₂ (s≺s ok , prf)

  ≺-respects-++-len
    : ∀{a}{A : Set a}(xs₀ ys₀ : List A){xs₁ ys₁ : List A}
    → (p : (xs₀ ++ xs₁) ≺ (ys₀ ++ ys₁))
    → length xs₀ ≡ length ys₀
    → xs₀ ≡ ys₀ × Σ (xs₁ ≺ ys₁) (λ p' → ≺-drop p ≡ ≺-drop p')
  ≺-respects-++-len [] [] prf hyp = refl , (prf , refl)
  ≺-respects-++-len (x ∷ xs) (.x ∷ ys) (s≺s prf) hyp
    with ≺-respects-++-len xs ys prf (suc-injective hyp)
  ...| xs≡ys , res , ok = cong (x ∷_) xs≡ys , res , ok

  bs-concat-[]⊎tf : ∀ as {bs} → true ∷ true ∷ bs ≢ bs-concat as
  bs-concat-[]⊎tf ([] ∷ as) ()
  bs-concat-[]⊎tf ((_ ∷ _) ∷ as) ()

  toBitString-pad'-≺
    : ∀{a b}
    → (a≺bbs : toBitString-pad' a ≺ toBitString-pad' b)
    → a ≡ b ⊎ ∃[ tail ] (≺-drop a≺bbs ≡ true ∷ true ∷ tail)
  toBitString-pad'-≺ {[]} {[]} prf     = inj₁ refl
  toBitString-pad'-≺ {[]} {x ∷ bs} z≺n = inj₂ (Vec-toList x ++ toBitString-pad' bs , refl)
  toBitString-pad'-≺ {a ∷ as} {b ∷ bs} (s≺s (s≺s prf))
    with ≺-respects-++-len (Vec-toList a) (Vec-toList b) prf
                           (trans (Vec-toList-length a) (sym (Vec-toList-length b)))
  ...| a≡b , prf' , drop≡
    with toBitString-pad'-≺ {as} {bs} prf'
  ...| inj₁ ok = inj₁ (cong₂ _∷_ (Vec-toList-inj a≡b) ok)
  ...| inj₂ ok = inj₂ (proj₁ ok , trans drop≡ (proj₂ ok))

  toBitString-pad-≺
    : ∀{a b}
    → (a≺bbs : toBitString-pad a ≺ toBitString-pad b)
    → a ≡ b ⊎ ∃[ tail ] (≺-drop a≺bbs ≡ true ∷ true ∷ tail)
  toBitString-pad-≺ {[]}    {[]} prf = inj₁ refl
  toBitString-pad-≺ {a ∷ as} {b ∷ bs} (s≺s (s≺s prf))
    with ≺-respects-++-len (Vec-toList a) (Vec-toList b) prf
                           (trans (Vec-toList-length a) (sym (Vec-toList-length b)))
  ...| a≡b , prf' , drop≡
    with toBitString-pad'-≺ {as} {bs} prf'
  ...| inj₁ ok = inj₁ (cong₂ _∷_ (Vec-toList-inj a≡b) ok)
  ...| inj₂ ok = inj₂ (proj₁ ok , trans drop≡ (proj₂ ok))

  bs-concat-inj : ∀ bs₁ bs₂ → bs-concat bs₁ ≡ bs-concat bs₂ → bs₁ ≡ bs₂
  bs-concat-inj [] [] hyp = refl
  bs-concat-inj ([] ∷ as) [] ()
  bs-concat-inj [] ([] ∷ bs) ()
  bs-concat-inj [] ((_ ∷ _) ∷ bs) ()
  bs-concat-inj ((_ ∷ _) ∷ as) [] ()
  bs-concat-inj (a ∷ as) (b ∷ bs) hyp -- TODO-1: Eliminate catchall warning or explain why we don't.
    with ++-≺ (toBitString-pad a) (toBitString-pad b) hyp
  ...| inj₁ (a≺b , prf)
    with toBitString-pad-≺ a≺b
  ...| inj₁ refl = cong (a ∷_) (bs-concat-inj as bs (proj₂ (++-len-injective (toBitString-pad a) _ refl hyp)))
  ...| inj₂ (tail , aux) rewrite aux = ⊥-elim (bs-concat-[]⊎tf as prf)
  bs-concat-inj (a ∷ as) (b ∷ bs) hyp
     | inj₂ (b≺a , prf)
    with toBitString-pad-≺ b≺a
  ...| inj₁ refl = cong (a ∷_) (bs-concat-inj as bs (proj₂ (++-len-injective (toBitString-pad a) _ refl hyp)))
  ...| inj₂ (tail , aux) rewrite aux  = ⊥-elim (bs-concat-[]⊎tf bs prf)

ext: agda

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
------------------------------------------------------------------------
-- Information orderings
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --sized-types #-}

open import Prelude hiding (module W)

module Delay-monad.Alternative.Partial-order {a} {A : Type a} where

open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)

open import Bijection equality-with-J using (_↔_)
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional equality-with-paths

open import Delay-monad.Alternative
open import Delay-monad.Alternative.Equivalence
open import Delay-monad.Alternative.Termination
import Delay-monad.Partial-order as PO
import Delay-monad.Termination as T

infix 4 _⊑_

-- Information orderings.

_⊑_ : Delay A → Delay A → Type a
x ⊑ y = ∀ z → x ⇓ z → y ⇓ z

_∥⊑∥_ : Delay A → Delay A → Type a
x ∥⊑∥ y = ∀ z → x ∥⇓∥ z → y ∥⇓∥ z

-- The two ordering relations are logically equivalent (if A is a
-- set).

⊑⇔∥⊑∥ : Is-set A → ∀ x y → x ⊑ y ⇔ x ∥⊑∥ y
⊑⇔∥⊑∥ A-set x y =
  ∀-cong _ λ _ → →-cong _ (⇓⇔∥⇓∥ A-set x) (⇓⇔∥⇓∥ A-set y)

-- The ordering relation _⊑_ is pointwise logically equivalent (via
-- Delay⇔Delay) to the ordering relation defined in
-- Delay-monad.Partial-order.

⊑⇔⊑ : ∀ x y →
      x ⊑ y ⇔ _⇔_.to Delay⇔Delay x PO.⊑ _⇔_.to Delay⇔Delay y
⊑⇔⊑ x y =
  x ⊑ y                                                              ↝⟨ F.id ⟩
  (∀ z → x ⇓ z → y ⇓ z)                                              ↝⟨ ∀-cong _ (λ _ → →-cong _ (⇓⇔⇓ x) (⇓⇔⇓ y)) ⟩
  (∀ z → _⇔_.to Delay⇔Delay x  T.⇓ z → _⇔_.to Delay⇔Delay y  T.⇓ z)  ↝⟨ inverse $ ∀-cong _ (λ _ → →-cong _ (_↔_.logical-equivalence PO.⇓↔⇓)
                                                                                (_↔_.logical-equivalence PO.⇓↔⇓)) ⟩
  (∀ z → _⇔_.to Delay⇔Delay x PO.⇓ z → _⇔_.to Delay⇔Delay y PO.⇓ z)  ↝⟨ inverse PO.⊑⇔⇓→⇓ ⟩□
  _⇔_.to Delay⇔Delay x PO.⊑ _⇔_.to Delay⇔Delay y                     □

⊑⇔⊑′ : ∀ {x y} →
       x PO.⊑ y ⇔ _⇔_.from Delay⇔Delay x ⊑ _⇔_.from Delay⇔Delay y
⊑⇔⊑′ {x} {y} =
  x PO.⊑ y                                                         ↝⟨ PO.⊑⇔⇓→⇓ ⟩
  (∀ z → x PO.⇓ z → y PO.⇓ z)                                      ↝⟨ ∀-cong _ (λ _ → →-cong _ (_↔_.logical-equivalence PO.⇓↔⇓)
                                                                                (_↔_.logical-equivalence PO.⇓↔⇓))  ⟩
  (∀ z → x  T.⇓ z → y  T.⇓ z)                                      ↝⟨ ∀-cong _ (λ _ → →-cong _ ⇓⇔⇓′ ⇓⇔⇓′) ⟩
  (∀ z → _⇔_.from Delay⇔Delay x ⇓ z → _⇔_.from Delay⇔Delay y ⇓ z)  ↝⟨ F.id ⟩□
  _⇔_.from Delay⇔Delay x ⊑ _⇔_.from Delay⇔Delay y                  □

-- The ordering relation _∥⊑∥_ is pointwise propositional.

∥⊑∥-propositional : ∀ x y → Is-proposition (x ∥⊑∥ y)
∥⊑∥-propositional _ _ =
  Π-closure ext 1 λ _ →
  Π-closure ext 1 λ _ →
  truncation-is-proposition

-- The ordering relation _∥⊑∥_ is reflexive.

∥⊑∥-reflexive : ∀ x → x ∥⊑∥ x
∥⊑∥-reflexive _ = λ _ → id

-- The ordering relation _∥⊑∥_ is transitive.

∥⊑∥-transitive : ∀ x y z → x ∥⊑∥ y → y ∥⊑∥ z → x ∥⊑∥ z
∥⊑∥-transitive _ _ _ p q = λ z → q z ∘ p z

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
{-# OPTIONS --universe-polymorphism #-}

open import Categories.Category

module Categories.Object.Initial {o ℓ e} (C : Category o ℓ e) where

open Category C

open import Level

record Initial : Set (o ⊔ ℓ ⊔ e) where
  field
    ⊥ : Obj
    ! : ∀ {A} → (⊥ ⇒ A)
    .!-unique : ∀ {A} → (f : ⊥ ⇒ A) → ! ≡ f

  .!-unique₂ : ∀ {A} → (f g : ⊥ ⇒ A) → f ≡ g
  !-unique₂ f g =
      begin
        f
      ↑⟨ !-unique f ⟩
        !
      ↓⟨ !-unique g ⟩
        g
      ∎
    where
    open HomReasoning

  .⊥-id : (f : ⊥ ⇒ ⊥) → f ≡ id
  ⊥-id f = !-unique₂ f id

import Categories.Morphisms
open Categories.Morphisms C
open Initial

.to-⊥-is-Epi : ∀ {A : Obj} {i : Initial} → (f : A ⇒ ⊥ i) → Epi f
to-⊥-is-Epi {_} {i} f = helper
  where
    helper : ∀ {C : Obj} → (g h : ⊥ i ⇒ C) → g ∘ f ≡ h ∘ f → g ≡ h
    helper g h _ = !-unique₂ i g h

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: copumpkin/categories

max_forks_repo_name: copumpkin/categories


text:
{-# OPTIONS --without-K --prop --rewriting #-}

module Calf.Types.Nat where

open import Calf.Prelude
open import Calf.Metalanguage
open import Data.Nat using (ℕ; zero; suc) public

nat : tp pos
nat = U (meta ℕ)

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Bundles where

open import Cubical.Core.Everything

open import Cubical.Algebra.Base
open import Cubical.Algebra.Structures
open import Cubical.Relation.Binary
open import Cubical.Foundations.Function

open import Cubical.Classes

------------------------------------------------------------------------
-- Bundles with 1 binary operation
------------------------------------------------------------------------

record Magma c : Type (ℓ-suc c) where
  constructor mkmagma
  infix 7 _•_ -- No association - forces parentheses
  field
    Carrier : Type c
    _•_     : Op₂ Carrier
    isMagma : IsMagma Carrier _•_

  open IsMagma isMagma public

instance
  MagmaCoerce : ∀ {c} → Coerce (Magma c)
  MagmaCoerce = record { coerce = Magma.Carrier }

record Semigroup c : Type (ℓ-suc c) where
  constructor mksemigroup
  infixl 7 _•_
  field
    Carrier     : Type c
    _•_         : Op₂ Carrier
    isSemigroup : IsSemigroup Carrier _•_

  open IsSemigroup isSemigroup public

  magma : Magma c
  magma = record { isMagma = isMagma }

instance
  SemigroupCoerce : ∀ {c} → Coerce (Semigroup c)
  SemigroupCoerce = record { coerce = Semigroup.Carrier }

  Semigroup→Magma : ∀ {c} → Cast (Semigroup c) (Magma c)
  Semigroup→Magma = record { cast = Semigroup.magma }

record Band c : Type (ℓ-suc c) where
  constructor mkband
  infixl 7 _•_
  field
    Carrier : Type c
    _•_     : Op₂ Carrier
    isBand  : IsBand Carrier _•_

  open IsBand isBand public

  semigroup : Semigroup c
  semigroup = record { isSemigroup = isSemigroup }

  open Semigroup semigroup public using (magma)

instance
  BandCoerce : ∀ {c} → Coerce (Band c)
  BandCoerce = record { coerce = Band.Carrier }

  Cast-Band→Semigroup : ∀ {c} → Cast (Band c) (Semigroup c)
  Cast-Band→Semigroup = record { cast = Band.semigroup }

  Cast-Band→Magma : ∀ {c} → Cast (Band c) (Magma c)
  Cast-Band→Magma = record { cast = Band.magma }

record CommutativeSemigroup c : Type (ℓ-suc c) where
  constructor mkcommsemigroup
  infixl 7 _•_
  field
    Carrier                 : Type c
    _•_                     : Op₂ Carrier
    isCommutativeSemigroup  : IsCommutativeSemigroup Carrier _•_

  open IsCommutativeSemigroup isCommutativeSemigroup public

  semigroup : Semigroup c
  semigroup = record { isSemigroup = isSemigroup }

  open Semigroup semigroup public using (magma)

instance
  CommSemigroupCoerce : ∀ {c} → Coerce (CommutativeSemigroup c)
  CommSemigroupCoerce = record { coerce = CommutativeSemigroup.Carrier }

  Cast-CommSemigroup→Semigroup : ∀ {c} → Cast (CommutativeSemigroup c) (Semigroup c)
  Cast-CommSemigroup→Semigroup = record { cast = CommutativeSemigroup.semigroup }

  Cast-CommSemigroup→Magma : ∀ {c} → Cast (CommutativeSemigroup c) (Magma c)
  Cast-CommSemigroup→Magma = record { cast = CommutativeSemigroup.magma }

record Semilattice c : Type (ℓ-suc c) where
  constructor mksemilattice
  infixr 7 _•_
  field
    Carrier       : Type c
    _•_           : Op₂ Carrier
    isSemilattice : IsSemilattice Carrier _•_

  open IsSemilattice isSemilattice public

  band : Band c
  band = record { isBand = isBand }

  open Band band public using (magma; semigroup)

instance
  SemilatticeCoerce : ∀ {c} → Coerce (Semilattice c)
  SemilatticeCoerce = record { coerce = Semilattice.Carrier }

record SelectiveMagma c : Type (ℓ-suc c) where
  constructor mkselmagma
  infixl 7 _•_
  field
    Carrier          : Type c
    _•_              : Op₂ Carrier
    isSelectiveMagma : IsSelectiveMagma Carrier _•_

  open IsSelectiveMagma isSelectiveMagma public

  magma : Magma c
  magma = record { isMagma = isMagma }

instance
  SelectiveMagmaCoerce : ∀ {c} → Coerce (SelectiveMagma c)
  SelectiveMagmaCoerce = record { coerce = SelectiveMagma.Carrier }

------------------------------------------------------------------------
-- Bundles with 1 binary operation & 1 element
------------------------------------------------------------------------

record Monoid c : Type (ℓ-suc c) where
  constructor mkmonoid
  infixl 7 _•_
  field
    Carrier  : Type c
    _•_      : Op₂ Carrier
    ε        : Carrier
    isMonoid : IsMonoid Carrier _•_ ε

  open IsMonoid isMonoid public

  semigroup : Semigroup _
  semigroup = record { isSemigroup = isSemigroup }

  open Semigroup semigroup public using (magma)

instance
  MonoidCoerce : ∀ {c} → Coerce (Monoid c)
  MonoidCoerce = record { coerce = Monoid.Carrier }

record CommutativeMonoid c : Type (ℓ-suc c) where
  constructor mkcommmonoid
  infixl 7 _•_
  field
    Carrier             : Type c
    _•_                 : Op₂ Carrier
    ε                   : Carrier
    isCommutativeMonoid : IsCommutativeMonoid Carrier _•_ ε

  open IsCommutativeMonoid isCommutativeMonoid public

  monoid : Monoid _
  monoid = record { isMonoid = isMonoid }

  open Monoid monoid public using (magma; semigroup)

  commutativeSemigroup : CommutativeSemigroup _
  commutativeSemigroup = record { isCommutativeSemigroup = isCommutativeSemigroup }

instance
  CommMonoidCoerce : ∀ {c} → Coerce (CommutativeMonoid c)
  CommMonoidCoerce = record { coerce = CommutativeMonoid.Carrier }

record IdempotentCommutativeMonoid c : Type (ℓ-suc c) where
  constructor mkidemcommmonoid
  infixl 7 _•_
  field
    Carrier                       : Type c
    _•_                           : Op₂ Carrier
    ε                             : Carrier
    isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid Carrier _•_ ε

  open IsIdempotentCommutativeMonoid isIdempotentCommutativeMonoid public

  commutativeMonoid : CommutativeMonoid _
  commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }

  open CommutativeMonoid commutativeMonoid public
    using (magma; semigroup; monoid)

instance
  IdemCommMonoidCoerce : ∀ {c} → Coerce (IdempotentCommutativeMonoid c)
  IdemCommMonoidCoerce = record { coerce = IdempotentCommutativeMonoid.Carrier }

-- Idempotent commutative monoids are also known as bounded lattices.
-- Note that the BoundedLattice necessarily uses the notation inherited
-- from monoids rather than lattices.

BoundedLattice = IdempotentCommutativeMonoid
pattern mkboundedlattice = mkidemcommmonoid

module BoundedLattice {c} (idemCommMonoid : IdempotentCommutativeMonoid c) =
       IdempotentCommutativeMonoid idemCommMonoid

------------------------------------------------------------------------
-- Bundles with 1 binary operation, 1 unary operation & 1 element
------------------------------------------------------------------------

record Group c : Type (ℓ-suc c) where
  constructor mkgroup
  infix  8 _⁻¹
  infixl 7 _•_
  field
    Carrier : Type c
    _•_     : Op₂ Carrier
    ε       : Carrier
    _⁻¹     : Op₁ Carrier
    isGroup : IsGroup Carrier _•_ ε _⁻¹

  open IsGroup isGroup public

  monoid : Monoid _
  monoid = record { isMonoid = isMonoid }

  open Monoid monoid public using (magma; semigroup)

instance
  GroupCoerce : ∀ {c} → Coerce (Group c)
  GroupCoerce = record { coerce = Group.Carrier }

record AbelianGroup c : Type (ℓ-suc c) where
  constructor mkabgroup
  infix  8 -_
  infixl 7 _+_
  field
    Carrier        : Type c
    _+_            : Op₂ Carrier
    ε              : Carrier
    -_             : Op₁ Carrier
    isAbelianGroup : IsAbelianGroup Carrier _+_ ε -_

  open IsAbelianGroup isAbelianGroup public

  group : Group _
  group = record { isGroup = isGroup }

  open Group group public
    using (magma; semigroup; monoid)

  commutativeMonoid : CommutativeMonoid _
  commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }

  open CommutativeMonoid commutativeMonoid public
    using (commutativeSemigroup)

instance
  AbelianGroupCoerce : ∀ {c} → Coerce (AbelianGroup c)
  AbelianGroupCoerce = record { coerce = AbelianGroup.Carrier }

------------------------------------------------------------------------
-- Bundles with 2 binary operations
------------------------------------------------------------------------

record Lattice c : Type (ℓ-suc c) where
  constructor mklattice
  infixr 7 _⋀_
  infixr 6 _⋁_
  field
    Carrier   : Type c
    _⋀_       : Op₂ Carrier
    _⋁_       : Op₂ Carrier
    isLattice : IsLattice Carrier _⋀_ _⋁_

  open IsLattice isLattice public

instance
  LatticeCoerce : ∀ {c} → Coerce (Lattice c)
  LatticeCoerce = record { coerce = Lattice.Carrier }

record DistributiveLattice c : Type (ℓ-suc c) where
  constructor mkdistrlattice
  infixr 7 _⋀_
  infixr 6 _⋁_
  field
    Carrier               : Type c
    _⋀_                   : Op₂ Carrier
    _⋁_                   : Op₂ Carrier
    isDistributiveLattice : IsDistributiveLattice Carrier _⋀_ _⋁_

  open IsDistributiveLattice isDistributiveLattice public

  lattice : Lattice _
  lattice = record { isLattice = isLattice }

instance
  DistrLatticeCoerce : ∀ {c} → Coerce (DistributiveLattice c)
  DistrLatticeCoerce = record { coerce = DistributiveLattice.Carrier }

------------------------------------------------------------------------
-- Bundles with 2 binary operations & 1 element
------------------------------------------------------------------------

record NearSemiring c : Type (ℓ-suc c) where
  constructor mknearsemiring
  infixl 7 _*_
  infixl 6 _+_
  field
    Carrier        : Type c
    _+_            : Op₂ Carrier
    _*_            : Op₂ Carrier
    0#             : Carrier
    isNearSemiring : IsNearSemiring Carrier _+_ _*_ 0#

  open IsNearSemiring isNearSemiring public

  +-monoid : Monoid _
  +-monoid = record { isMonoid = +-isMonoid }

  open Monoid +-monoid public
    using () renaming
    ( magma     to +-magma
    ; semigroup to +-semigroup
    )

  *-semigroup : Semigroup _
  *-semigroup = record { isSemigroup = *-isSemigroup }

  open Semigroup *-semigroup public
    using () renaming
    ( magma to *-magma )

instance
  NearSemiringCoerce : ∀ {c} → Coerce (NearSemiring c)
  NearSemiringCoerce = record { coerce = NearSemiring.Carrier }

record SemiringWithoutOne c : Type (ℓ-suc c) where
  constructor mksemiringwo1
  infixl 7 _*_
  infixl 6 _+_
  field
    Carrier              : Type c
    _+_                  : Op₂ Carrier
    _*_                  : Op₂ Carrier
    0#                   : Carrier
    isSemiringWithoutOne : IsSemiringWithoutOne Carrier _+_ _*_ 0#

  open IsSemiringWithoutOne isSemiringWithoutOne public

  nearSemiring : NearSemiring _
  nearSemiring = record { isNearSemiring = isNearSemiring }

  open NearSemiring nearSemiring public
    using
    ( +-magma; +-semigroup; +-monoid
    ; *-magma; *-semigroup
    )

  +-commutativeMonoid : CommutativeMonoid _
  +-commutativeMonoid = record { isCommutativeMonoid = +-isCommutativeMonoid }

  open CommutativeMonoid +-commutativeMonoid public
    using () renaming (commutativeSemigroup to +-commutativeSemigroup)

instance
  SemiringW1Coerce : ∀ {c} → Coerce (SemiringWithoutOne c)
  SemiringW1Coerce = record { coerce = SemiringWithoutOne.Carrier }

record CommutativeSemiringWithoutOne c : Type (ℓ-suc c) where
  constructor mkcommsemiringwo1
  infixl 7 _*_
  infixl 6 _+_
  field
    Carrier                         : Type c
    _+_                             : Op₂ Carrier
    _*_                             : Op₂ Carrier
    0#                              : Carrier
    isCommutativeSemiringWithoutOne :
      IsCommutativeSemiringWithoutOne Carrier _+_ _*_ 0#

  open IsCommutativeSemiringWithoutOne
         isCommutativeSemiringWithoutOne public

  semiringWithoutOne : SemiringWithoutOne _
  semiringWithoutOne =
    record { isSemiringWithoutOne = isSemiringWithoutOne }

  open SemiringWithoutOne semiringWithoutOne public
    using
    ( +-magma; +-semigroup; +-commutativeSemigroup
    ; *-magma; *-semigroup
    ; +-monoid; +-commutativeMonoid
    ; nearSemiring
    )

instance
  CommSemiringW1Coerce : ∀ {c} → Coerce (CommutativeSemiringWithoutOne c)
  CommSemiringW1Coerce = record { coerce = CommutativeSemiringWithoutOne.Carrier }

------------------------------------------------------------------------
-- Bundles with 2 binary operations & 2 elements
------------------------------------------------------------------------

record SemiringWithoutAnnihilatingZero c : Type (ℓ-suc c) where
  constructor mksemiringwoa0
  infixl 7 _*_
  infixl 6 _+_
  field
    Carrier                           : Type c
    _+_                               : Op₂ Carrier
    _*_                               : Op₂ Carrier
    0#                                : Carrier
    1#                                : Carrier
    isSemiringWithoutAnnihilatingZero :
      IsSemiringWithoutAnnihilatingZero Carrier _+_ _*_ 0# 1#

  open IsSemiringWithoutAnnihilatingZero
         isSemiringWithoutAnnihilatingZero public

  +-commutativeMonoid : CommutativeMonoid _
  +-commutativeMonoid =
    record { isCommutativeMonoid = +-isCommutativeMonoid }

  open CommutativeMonoid +-commutativeMonoid public
    using () renaming
    ( magma                to +-magma
    ; semigroup            to +-semigroup
    ; commutativeSemigroup to +-commutativeSemigroup
    ; monoid               to +-monoid
    )

  *-monoid : Monoid _
  *-monoid = record { isMonoid = *-isMonoid }

  open Monoid *-monoid public
    using ()
    renaming
    ( magma     to *-magma
    ; semigroup to *-semigroup
    )

instance
  SemiringWA0Coerce : ∀ {c} → Coerce (SemiringWithoutAnnihilatingZero c)
  SemiringWA0Coerce = record { coerce = SemiringWithoutAnnihilatingZero.Carrier }

record Semiring c : Type (ℓ-suc c) where
  constructor mksemiring
  infixl 7 _*_
  infixl 6 _+_
  field
    Carrier    : Type c
    _+_        : Op₂ Carrier
    _*_        : Op₂ Carrier
    0#         : Carrier
    1#         : Carrier
    isSemiring : IsSemiring Carrier _+_ _*_ 0# 1#

  open IsSemiring isSemiring public

  semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero _
  semiringWithoutAnnihilatingZero = record
    { isSemiringWithoutAnnihilatingZero =
        isSemiringWithoutAnnihilatingZero
    }

  open SemiringWithoutAnnihilatingZero
         semiringWithoutAnnihilatingZero public
    using
    ( +-magma;  +-semigroup; +-commutativeSemigroup
    ; *-magma;  *-semigroup
    ; +-monoid; +-commutativeMonoid
    ; *-monoid
    )

  semiringWithoutOne : SemiringWithoutOne _
  semiringWithoutOne =
    record { isSemiringWithoutOne = isSemiringWithoutOne }

  open SemiringWithoutOne semiringWithoutOne public
    using (nearSemiring)

instance
  SemiringCoerce : ∀ {c} → Coerce (Semiring c)
  SemiringCoerce = record { coerce = Semiring.Carrier }

record CommutativeSemiring c : Type (ℓ-suc c) where
  constructor mkcommsemiring
  infixl 7 _*_
  infixl 6 _+_
  field
    Carrier               : Type c
    _+_                   : Op₂ Carrier
    _*_                   : Op₂ Carrier
    0#                    : Carrier
    1#                    : Carrier
    isCommutativeSemiring : IsCommutativeSemiring Carrier _+_ _*_ 0# 1#

  open IsCommutativeSemiring isCommutativeSemiring public

  semiring : Semiring _
  semiring = record { isSemiring = isSemiring }

  open Semiring semiring public
    using
    ( +-magma; +-semigroup; +-commutativeSemigroup
    ; *-magma; *-semigroup
    ; +-monoid; +-commutativeMonoid
    ; *-monoid
    ; nearSemiring; semiringWithoutOne
    ; semiringWithoutAnnihilatingZero
    )

  *-commutativeSemigroup : CommutativeSemigroup _
  *-commutativeSemigroup = record
    { isCommutativeSemigroup = *-isCommutativeSemigroup
    }

  *-commutativeMonoid : CommutativeMonoid _
  *-commutativeMonoid = record
    { isCommutativeMonoid = *-isCommutativeMonoid
    }

  commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne _
  commutativeSemiringWithoutOne = record
    { isCommutativeSemiringWithoutOne = isCommutativeSemiringWithoutOne
    }

instance
  CommSemiringCoerce : ∀ {c} → Coerce (CommutativeSemiring c)
  CommSemiringCoerce = record { coerce = CommutativeSemiring.Carrier }

------------------------------------------------------------------------
-- Bundles with 2 binary operations, 1 unary operation & 2 elements
------------------------------------------------------------------------

record Ring c : Type (ℓ-suc c) where
  constructor mkring
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  field
    Carrier : Type c
    _+_     : Op₂ Carrier
    _*_     : Op₂ Carrier
    -_      : Op₁ Carrier
    0#      : Carrier
    1#      : Carrier
    isRing  : IsRing Carrier _+_ _*_ -_ 0# 1#

  open IsRing isRing public

  +-abelianGroup : AbelianGroup _
  +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup }

  semiring : Semiring _
  semiring = record { isSemiring = isSemiring }

  open Semiring semiring public
    using
    ( +-magma; +-semigroup; +-commutativeSemigroup
    ; *-magma; *-semigroup
    ; +-monoid ; +-commutativeMonoid
    ; *-monoid
    ; nearSemiring; semiringWithoutOne
    ; semiringWithoutAnnihilatingZero
    )

  open AbelianGroup +-abelianGroup public
    using () renaming (group to +-group)

instance
  RingCoerce : ∀ {c} → Coerce (Ring c)
  RingCoerce = record { coerce = Ring.Carrier }

record CommutativeRing c : Type (ℓ-suc c) where
  constructor mkcommring
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  field
    Carrier           : Type c
    _+_               : Op₂ Carrier
    _*_               : Op₂ Carrier
    -_                : Op₁ Carrier
    0#                : Carrier
    1#                : Carrier
    isCommutativeRing : IsCommutativeRing Carrier _+_ _*_ -_ 0# 1#

  open IsCommutativeRing isCommutativeRing public

  ring : Ring _
  ring = record { isRing = isRing }

  commutativeSemiring : CommutativeSemiring _
  commutativeSemiring =
    record { isCommutativeSemiring = isCommutativeSemiring }

  open Ring ring public using (+-group; +-abelianGroup)
  open CommutativeSemiring commutativeSemiring public
    using
    ( +-magma; +-semigroup; +-commutativeSemigroup
    ; *-magma; *-semigroup; *-commutativeSemigroup
    ; +-monoid; +-commutativeMonoid
    ; *-monoid; *-commutativeMonoid
    ; nearSemiring; semiringWithoutOne
    ; semiringWithoutAnnihilatingZero; semiring
    ; commutativeSemiringWithoutOne
    )

instance
  CommRingCoerce : ∀ {c} → Coerce (CommutativeRing c)
  CommRingCoerce = record { coerce = CommutativeRing.Carrier }

record BooleanAlgebra c : Type (ℓ-suc c) where
  constructor mkbooleanalgebra
  infix  8 ¬_
  infixr 7 _⋀_
  infixr 6 _⋁_
  field
    Carrier          : Type c
    _⋀_              : Op₂ Carrier
    _⋁_              : Op₂ Carrier
    ¬_               : Op₁ Carrier
    ⊤                : Carrier
    ⊥                : Carrier
    isBooleanAlgebra : IsBooleanAlgebra Carrier _⋀_ _⋁_ ¬_ ⊤ ⊥

  open IsBooleanAlgebra isBooleanAlgebra public

  distributiveLattice : DistributiveLattice _
  distributiveLattice = record { isDistributiveLattice = isDistributiveLattice }

  open DistributiveLattice distributiveLattice public
    using (lattice)

instance
  BooleanCoerce : ∀ {c} → Coerce (BooleanAlgebra c)
  BooleanCoerce = record { coerce = BooleanAlgebra.Carrier }

------------------------------------------------------------------------
-- Bundles with 2 binary operations, 1 unary operation & 2 elements
------------------------------------------------------------------------

record DivisionRing c ℓ : Type (ℓ-suc (ℓ-max c ℓ)) where
  constructor mkdivring
  infix  9 _⁻¹
  infix  8 -_
  infixr 7 _*_
  infixr 6 _+_
  field
    Carrier        : Type c
    Invertible     : Carrier → Type ℓ
    _+_            : Op₂ Carrier
    _*_            : Op₂ Carrier
    0#             : Carrier
    1#             : Carrier
    -_             : Op₁ Carrier
    _⁻¹            : Σ Carrier Invertible → Carrier
    isDivisionRing : IsDivisionRing Carrier Invertible _+_ _*_ -_ _⁻¹ 0# 1#

  open IsDivisionRing isDivisionRing public

  ring : Ring _
  ring = record { isRing = isRing }

  open Ring ring public using (+-group; +-abelianGroup)

instance
  DivisionRingCoerce : ∀ {c ℓ} → Coerce (DivisionRing c ℓ)
  DivisionRingCoerce = record { coerce = DivisionRing.Carrier }

record Field c ℓ : Type (ℓ-suc (ℓ-max c ℓ)) where
  constructor mkfield
  infix  9 _⁻¹
  infix  8 -_
  infixr 7 _*_
  infixr 6 _+_
  field
    Carrier    : Type c
    Invertible : Carrier → Type ℓ
    _+_        : Op₂ Carrier
    _*_        : Op₂ Carrier
    0#         : Carrier
    1#         : Carrier
    -_         : Op₁ Carrier
    _⁻¹        : Σ Carrier Invertible → Carrier
    isField    : IsField Carrier Invertible _+_ _*_ -_ _⁻¹ 0# 1#

  open IsField isField public

  divisionRing : DivisionRing _ _
  divisionRing = record { isDivisionRing = isDivisionRing }

  open DivisionRing divisionRing public using (ring; +-group; +-abelianGroup)

  commutativeRing : CommutativeRing _
  commutativeRing = record { isCommutativeRing = isCommutativeRing }

  open CommutativeRing commutativeRing public
      using
      ( commutativeSemiring
      ; +-magma; +-semigroup; +-commutativeSemigroup
      ; *-magma; *-semigroup; *-commutativeSemigroup
      ; +-monoid; +-commutativeMonoid
      ; *-monoid; *-commutativeMonoid
      ; nearSemiring; semiringWithoutOne
      ; semiringWithoutAnnihilatingZero; semiring
      ; commutativeSemiringWithoutOne
      )

instance
  FieldCoerce : ∀ {c ℓ} → Coerce (Field c ℓ)
  FieldCoerce = record { coerce = Field.Carrier }


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed binary relations
------------------------------------------------------------------------

module Relation.Binary.Indexed where

import Relation.Binary as B

open import Relation.Binary.Indexed.Core public

-- By "instantiating" an indexed setoid one gets an ordinary setoid.

_at_ : ∀ {i s₁ s₂} {I : Set i} → Setoid I s₁ s₂ → I → B.Setoid _ _
S at i = record
  { Carrier       = S.Carrier i
  ; _≈_           = S._≈_
  ; isEquivalence = record
    { refl  = S.refl
    ; sym   = S.sym
    ; trans = S.trans
    }
  } where module S = Setoid S

------------------------------------------------------------------------
-- Simple properties of indexed binary relations

-- Generalised implication.

infixr 4 _=[_]⇒_

_=[_]⇒_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : A → Set b} →
          B.Rel A ℓ₁ → ((x : A) → B x) → Rel B ℓ₂ → Set _
P =[ f ]⇒ Q = ∀ {i j} → P i j → Q (f i) (f j)


text:
module plfa.Naturals where

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)

infixl 6 _+_

-- @practice: exercise `seven` start
_ : 7 ≡ suc (suc (suc (suc (suc (suc (suc zero))))))
_ = refl
-- @practice: exercise `seven` end

_ : 2 + 3 ≡ 5
_ =
  begin
    2 + 3
  ≡⟨⟩
    (suc (suc zero)) + (suc (suc (suc zero)))
  ≡⟨⟩
    suc ((suc zero) + (suc (suc (suc zero))))
  ≡⟨⟩
    suc (suc (zero + (suc (suc (suc zero)))))
  ≡⟨⟩
    suc (suc (suc (suc (suc zero))))
  ≡⟨⟩
    5
  ∎

-- @practice: exercise `+-example` start

_ : 3 + 4 ≡ 7
_ =
  begin
    3 + 4
  ≡⟨⟩
    suc (2 + 4)
  ≡⟨⟩
    suc ( suc ( 1 + 4 ))
  ≡⟨⟩
    suc ( suc ( suc ( 0 + 4 )))
  ≡⟨⟩
    suc ( suc ( suc 4 ))
  ≡⟨⟩
    7
  ∎

-- @practice: exercise `+-example` end

_*_ : ℕ → ℕ → ℕ
zero * ℕ = zero
(suc m) * n = n + ( m * n )

infixl 7 _*_

_ =
  begin
    2 * 3
  ≡⟨⟩
    3 + ( 1 * 3 )
  ≡⟨⟩
    3 + ( 3 + ( 0 * 3 ))
  ≡⟨⟩
    3 + (3 + 0)
  ≡⟨⟩
    6
  ∎

-- @practice: exercise `*-example` start
_ =
  begin
    3 * 4
  ≡⟨⟩
    4 + ( 2 * 4)
  ≡⟨⟩
    4 + ( 4 + (1 * 4))
  ≡⟨⟩
    4 + ( 4 + (4 + (0 * 4)))
  ≡⟨⟩
    4 + (4 + (4 + 0))
  ≡⟨⟩
    12
  ∎
-- @practice: exercise `*-example` end

-- @recommend: exercise `_^_` start
_^_ : ℕ → ℕ → ℕ
m ^ zero = 1
m ^ (suc n) = m * (m ^ n)

infixl 8 _^_

_ : 3 ^ 4 ≡ 81
_ = refl
-- @recommend: exercise `_^_` end

_∸_ : ℕ → ℕ → ℕ
m    ∸ zero = m
zero ∸ n = zero
suc m ∸ suc n = m ∸ n

infixl 6 _∸_

_ =
  begin
    3 ∸ 2
  ≡⟨⟩
    2 ∸ 1
  ≡⟨⟩
    1 ∸ 0
  ≡⟨⟩
    1
  ∎

_ =
  begin
    2 ∸ 3
  ≡⟨⟩
    1 ∸ 2
  ≡⟨⟩
    0 ∸ 1
  ≡⟨⟩
    0
  ∎

-- @recommend: exercise `∸-examples` start
_ =
  begin
    5 ∸ 3
  ≡⟨⟩
    4 ∸ 2
  ≡⟨⟩
    3 ∸ 1
  ≡⟨⟩
    2 ∸ 0
  ≡⟨⟩
    2
  ∎

_ =
  begin
    2 ∸ 5
  ≡⟨⟩
    1 ∸ 4
  ≡⟨⟩
    0 ∸ 3
  ≡⟨⟩
    0
  ∎
-- @recommend: exercise `∸-examples` end

-- infixl 6 _+_ _∸_
-- infixl 7 _⋆_
-- infixl indicates an operator associates to the left
-- infixr indicates an operator associates to the right
-- infix indicates that parentheses are always required

-- C-c + C-l convert `?` to `{}#`
-- C-c + C-f jump to next hole
-- C-c + C-c pattern variables to case
-- C-c + C-, the target type and the context
-- C-c + C-. the target type and the context and the inferred type
-- C-c + C-r recommendation
-- C-c + C-SPA fill up the hole
-- C-c + C-a auto fill up the holes

{-# BUILTIN NATPLUS _+_ #-}
{-# BUILTIN NATTIMES _*_ #-}
{-# BUILTIN NATMINUS _∸_ #-}

-- @stretch: exercise `Bin` start

data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

inc : Bin → Bin
inc (m O) = m I
inc (m I) = (inc m) O
inc ⟨⟩ = ⟨⟩ I

-- inc unit test start

_ =
  begin
    inc (⟨⟩)
  ≡⟨⟩
    ⟨⟩ I
  ∎

_ =
  begin
    inc (⟨⟩ I)
  ≡⟨⟩
    ⟨⟩ I O
  ∎

_ =
  begin
    inc (⟨⟩ I O)
  ≡⟨⟩
    ⟨⟩ I I
  ∎

_ =
  begin
    inc (⟨⟩ I O I I)
  ≡⟨⟩
    (inc (⟨⟩ I O I)) O
  ≡⟨⟩
    ( (inc (⟨⟩ I O)) O ) O
  ≡⟨⟩
    ((⟨⟩ I I) O ) O
  ≡⟨⟩
    ⟨⟩ I I O O
  ∎

-- inc unit test end

to : ℕ → Bin
to zero = ⟨⟩ O
to (suc n) = inc (to n)

from : Bin -> ℕ
from (m O) = 2 * (from m)
from (m I) = 2 * (from m) + 1
from ⟨⟩ = 0

-- from & to unit test start

_ : (to 11) ≡ (⟨⟩ I O I I)
_ = refl

_ : (from (⟨⟩ I O I I)) ≡ 11
_ = refl

_ : (to 0) ≡ (⟨⟩ O)
_ = refl

_ : (to 1) ≡ (⟨⟩ I)
_ = refl

_ : (from (⟨⟩ I)) ≡ 1
_ = refl

_ : (from (⟨⟩ O)) ≡ 0
_ = refl

-- from & to unit test end

-- @stretch: exercise `Bin` end

-- import Data.Nat using (ℕ; zero; suc; _+_; _*_; _^_; _∸_)

max_stars_repo_name: lonelyhentai/workspace

max_issues_repo_name: lonelyhentai/workspace

max_forks_repo_name: lonelyhentai/workspace


text:
{-
  A simple stack language example. Illustrating that one
  wants dependent elimination of inductive families.
-}

module StackLanguage where

open import Lib.Nat
open import Lib.Vec
open import Lib.Id

data Prog (A : Set) : Nat -> Set where
  init : Prog A 0
  push : forall {n} -> A -> Prog A n -> Prog A (suc n)
  pop  : forall {n} -> Prog A (suc n) -> Prog A n

⟦_⟧ : forall {A n} -> Prog A n -> Vec A n
⟦ init     ⟧ = ε
⟦ push x p ⟧ = x ► ⟦ p ⟧
⟦ pop p    ⟧ with ⟦ p ⟧
...             | x ► xs = xs

reify : forall {A n} -> Vec A n -> Prog A n
reify ε        = init
reify (x ► xs) = push x (reify xs)

normalise : forall {A n} -> Prog A n -> Prog A n
normalise p = reify ⟦ p ⟧

_≅_ : forall {A n} -> Prog A n -> Prog A n -> Set
p₁ ≅ p₂ = ⟦ p₁ ⟧ == ⟦ p₂ ⟧

sound : forall {A n} -> (p : Prog A n) -> normalise p ≅ p
sound init       = refl
sound (push x p) = cong (_►_ x) (sound p)
sound (pop p)    with ⟦ p ⟧ | sound p
...           | x ► xs | ih with ⟦ reify xs ⟧
sound (pop p) | x ► xs | refl  | .xs = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K #-}

open import Base
open import Homotopy.Truncation

module Homotopy.Connected {i} where

is-connected : ℕ₋₂ → Set i → Set i
is-connected n A = is-contr (τ n A)

is-connected-is-prop : (n : ℕ₋₂) {A : Set i} → is-prop (is-connected n A)
is-connected-is-prop n = is-contr-is-prop

has-connected-fibers : {A B : Set i} → ℕ₋₂ → (A → B) → Set i
has-connected-fibers n f = ∀ x → is-connected n (hfiber f x)

module _ (n : ℕ₋₂) (A : Set i) where

  private
    τ-to-ττ : τ n A → τ n (τ (S n) A)
    τ-to-ττ = τ-extend-nondep (proj ◯ proj)

    τ-is-truncated-S : is-truncated (S n) (τ n A)
    τ-is-truncated-S = truncated-is-truncated-S n (τ-is-truncated n A)

    ττ-to-τ : τ n (τ (S n) A) → τ n A
    ττ-to-τ = τ-extend-nondep (τ-extend-nondep proj)

    τ-inv-ττ : (x : τ n A) → ττ-to-τ (τ-to-ττ x) ≡ x
    τ-inv-ττ = τ-extend ⦃ λ _ → ≡-is-truncated n (τ-is-truncated n A) ⦄
                 (λ _ → refl)

    ττ-inv-τ : (x : τ n (τ (S n) A)) → τ-to-ττ (ττ-to-τ x) ≡ x
    ττ-inv-τ = τ-extend ⦃ λ _ → ≡-is-truncated n (τ-is-truncated n _) ⦄
                 (τ-extend ⦃ λ _ → truncated-is-truncated-S n
                                     (≡-is-truncated n
                                       (τ-is-truncated n _)) ⦄
                   (λ _ → refl))

  τ-equiv-ττ : τ n A ≃ τ n (τ (S n) A)
  τ-equiv-ττ = (τ-to-ττ , iso-is-eq _ ττ-to-τ ττ-inv-τ τ-inv-ττ)

  ττ-equiv-τ : τ n (τ (S n) A) ≃ τ n A
  ττ-equiv-τ = (ττ-to-τ , iso-is-eq _ τ-to-ττ τ-inv-ττ ττ-inv-τ)

abstract
  contr-is-connected : (n : ℕ₋₂) {A : Set i}
    → (is-contr A → is-connected n A)
  contr-is-connected n (x , p) =
    (proj x , τ-extend ⦃ λ _ → ≡-is-truncated n (τ-is-truncated n _) ⦄
                (λ _ → ap proj (contr-has-all-paths (x , p) _ _)))

  connected-S-is-connected : (n : ℕ₋₂) {A : Set i}
    → (is-connected (S n) A → is-connected n A)
  connected-S-is-connected n p =
    equiv-types-truncated _ (ττ-equiv-τ n _) (contr-is-connected n p)

app-is-inj : ∀ {j} {A : Set i} {B : Set j} {n : ℕ₋₂} {f g : A → B} (x₀ : A)
  → (is-connected n A → is-truncated n B → f x₀ ≡ g x₀ → f ≡ g)
app-is-inj x₀ p q e = equiv-is-inj (τ-extend-equiv _ _ _) _ _
                                   (funext (contr-has-section p (proj x₀) e))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module Structure.Operator.Ring where

import      Lvl
open import Logic
open import Logic.Predicate
open import Logic.Propositional
open import Structure.Setoid
open import Structure.Operator
open import Structure.Operator.Group using (Group ; CommutativeGroup)
open import Structure.Operator.Monoid using (Monoid)
open import Structure.Operator.Properties hiding (distributivityₗ ; distributivityᵣ ; commutativity)
open import Syntax.Function
open import Type

-- TODO: Rg, Rng, Rig

private
  module Impl {ℓ ℓₑ} {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (𝟎 : T) where
    record NonZero (x : T) : Stmt{ℓₑ} where
      constructor intro
      field proof : (x ≢ 𝟎)

-- An algebraic structure over two operators, in which the first one is a commutative group, and the second one is associative and distributes over the first one.
-- Also called: Rg.
record Rng {ℓ ℓₑ} {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_+_  : T → T → T) (_⋅_  : T → T → T) : Stmt{ℓ Lvl.⊔ ℓₑ} where
  constructor intro
  field
    ⦃ [+]-commutative-group ⦄  : CommutativeGroup (_+_)
    ⦃ [⋅]-binary-operator ⦄    : BinaryOperator(_⋅_)
    ⦃ [⋅]-associativity ⦄      : Associativity(_⋅_)
    ⦃ [⋅][+]-distributivityₗ ⦄ : Distributivityₗ(_⋅_)(_+_)
    ⦃ [⋅][+]-distributivityᵣ ⦄ : Distributivityᵣ(_⋅_)(_+_)

  open CommutativeGroup([+]-commutative-group)
    using ()
    renaming(
      group               to [+]-group ;
      commutativity       to [+]-commutativity ;
      monoid              to [+]-monoid ;
      binary-operator     to [+]-binary-operator ;
      associativity       to [+]-associativity ;
      identity-existence  to [+]-identity-existence ;
      identity-existenceₗ to [+]-identity-existenceₗ ;
      identity-existenceᵣ to [+]-identity-existenceᵣ ;
      id                  to 𝟎 ;
      identity            to [+]-identity ;
      identityₗ           to [+]-identityₗ ;
      identityᵣ           to [+]-identityᵣ ;
      inverse-existence   to [+]-inverse-existence ;
      inv                 to −_ ;
      inv-function        to [−]-function ;
      inverse             to [+]-inverse ;
      inverseₗ            to [+]-inverseₗ ;
      inverseᵣ            to [+]-inverseᵣ
    ) public
  open Impl(𝟎) public

  _−_ : T → T → T
  x − y = x + (− y)

  ZeroDivisorₗ : T → Stmt
  ZeroDivisorₗ(a) = ∃(x ↦ (x ≢ 𝟎) ∧ (a ⋅ x ≡ 𝟎))

  ZeroDivisorᵣ : T → Stmt
  ZeroDivisorᵣ(a) = ∃(x ↦ (x ≢ 𝟎) ∧ (x ⋅ a ≡ 𝟎))

  ZeroDivisor : T → Stmt
  ZeroDivisor(a) = ∃(x ↦ (x ≢ 𝟎) ∧ ((a ⋅ x ≡ 𝟎) ∧ (x ⋅ a ≡ 𝟎)))

record RngObject {ℓ ℓₑ} : Stmt{Lvl.𝐒(ℓ Lvl.⊔ ℓₑ)} where
  constructor intro
  field
    {T} : Type{ℓ}
    ⦃ equiv ⦄ : Equiv{ℓₑ}(T)
    _+_ : T → T → T
    _⋅_ : T → T → T
    ⦃ rng ⦄ : Rng(_+_)(_⋅_)
  open Rng(rng) public

record Unity {ℓ ℓₑ} {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_+_  : T → T → T) (_⋅_  : T → T → T) ⦃ rng : Rng(_+_)(_⋅_) ⦄ : Stmt{ℓ Lvl.⊔ ℓₑ} where
  constructor intro
  open Rng(rng)
  field
    ⦃ [⋅]-identity-existence ⦄ : ∃(Identity(_⋅_))

  [⋅]-monoid : Monoid(_⋅_)
  [⋅]-monoid = record{}

  open Monoid([⋅]-monoid)
    using ()
    renaming(
      id                 to 𝟏 ;
      identity           to [⋅]-identity ;
      identityₗ          to [⋅]-identityₗ ;
      identityᵣ          to [⋅]-identityᵣ
    ) public

  DistinctIdentities = NonZero(𝟏)

-- Rng with unity.
-- Also called: Rig.
record Ring {ℓ ℓₑ} {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_+_  : T → T → T) (_⋅_  : T → T → T) : Stmt{ℓ Lvl.⊔ ℓₑ} where
  constructor intro
  field
    ⦃ rng ⦄   : Rng(_+_)(_⋅_)
    ⦃ unity ⦄ : Unity(_+_)(_⋅_)
  open Rng(rng) public
  open Unity(unity) public

record RingObject {ℓ ℓₑ} : Stmt{Lvl.𝐒(ℓ Lvl.⊔ ℓₑ)} where
  constructor intro
  field
    {T} : Type{ℓ}
    ⦃ equiv ⦄ : Equiv{ℓₑ}(T)
    _+_ : T → T → T
    _⋅_ : T → T → T
    ⦃ ring ⦄ : Ring(_+_)(_⋅_)
  open Ring(ring) public

record Division {ℓ ℓₑ} {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_+_  : T → T → T) (_⋅_  : T → T → T) ⦃ rng : Rng(_+_)(_⋅_) ⦄ ⦃ unity : Unity(_+_)(_⋅_) ⦄ : Stmt{ℓ Lvl.⊔ ℓₑ} where
  constructor intro
  open Rng(rng)
  open Unity(unity)
  field
    ⅟ : (x : T) → ⦃ NonZero(x) ⦄ → T
    [⋅]-inverseₗ : ∀{x} → ⦃ non-zero : NonZero(x) ⦄ → (x ⋅ (⅟ x) ≡ 𝟏)
    [⋅]-inverseᵣ : ∀{x} → ⦃ non-zero : NonZero(x) ⦄ → ((⅟ x) ⋅ x ≡ 𝟏)

  _/_ : T → (y : T) → ⦃ NonZero(y) ⦄ → T
  x / y = x ⋅ (⅟ y)

-- Ring with division.
-- Also called: Ring.
record DivisionRing {ℓ ℓₑ} {T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_+_  : T → T → T) (_⋅_  : T → T → T) : Stmt{ℓ Lvl.⊔ ℓₑ} where
  constructor intro
  field
    ⦃ ring ⦄     : Ring(_+_)(_⋅_)
    ⦃ division ⦄ : Division(_+_)(_⋅_)
  open Ring    (ring)     public
  open Division(division) public

record DivisionRingObject {ℓ ℓₑ} : Stmt{Lvl.𝐒(ℓ Lvl.⊔ ℓₑ)} where
  constructor intro
  field
    {T} : Type{ℓ}
    ⦃ equiv ⦄ : Equiv{ℓₑ}(T)
    _+_ : T → T → T
    _⋅_ : T → T → T
    ⦃ divisionRing ⦄ : DivisionRing(_+_)(_⋅_)
  open DivisionRing(divisionRing) public

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
#include <stdlib.h>
#include <stdio.h>
#include <math.h>
#include <gsl/gsl_errno.h>
#include <gsl/gsl_spline.h>

int
main (void)
{
  int i;
  double xi, yi, x[10], y[10];

  printf ("#m=0,S=17\n");

  for (i = 0; i < 10; i++)
    {
      x[i] = i + 0.5 * sin (i);
      y[i] = i + cos (i * i);
      printf ("%g %g\n", x[i], y[i]);
    }

  printf ("#m=1,S=0\n");

  {
    gsl_interp_accel *acc
      = gsl_interp_accel_alloc ();
    gsl_spline *spline
      = gsl_spline_alloc (gsl_interp_cspline, 10);

    gsl_spline_init (spline, x, y, 10);

    for (xi = x[0]; xi < x[9]; xi += 0.01)
      {
        yi = gsl_spline_eval (spline, xi, acc);
        printf ("%g %g\n", xi, yi);
      }
    gsl_spline_free (spline);
    gsl_interp_accel_free (acc);
  }
  return 0;
}

ext: c

max_stars_repo_name: ielomariala/Hex-Game

max_issues_repo_name: Brian-ning/HMNE

max_forks_repo_name: Brian-ning/HMNE


text:
/*
 * Copyright (c) 2009-2020 The University of Tennessee and The University
 *                         of Tennessee Research Foundation.  All rights
 *                         reserved.
 *
 */
#ifndef _TESTSCOMMON_H
#define _TESTSCOMMON_H

/* parsec things */
#include "parsec.h"

/* system and io */
#include <stdlib.h>
#include <stdio.h>
#include <string.h>
/* Plasma and math libs */
#include <math.h>
#include <cblas.h>
#include <lapacke.h>

#include "parsec/profiling.h"
#include "parsec/parsec_internal.h"
#include "parsec/utils/debug.h"
#include "dplasma.h"
#include "dplasmatypes.h"

#include <core_blas.h>
/* timings */
#include "common_timing.h"

#include "flops.h"

/* these are globals in common.c */
extern char *PARSEC_SCHED_NAME[];
extern int unix_timestamp;
extern char cwd[];

/* Update PASTE_CODE_PROGRESS_KERNEL below if you change this list */
enum iparam_t {
  IPARAM_RANK,         /* Rank                              */
  IPARAM_NNODES,       /* Number of nodes                   */
  IPARAM_NCORES,       /* Number of cores                   */
  IPARAM_NGPUS,        /* Number of GPUs                    */
  IPARAM_P,            /* Rows in the process grid          */
  IPARAM_Q,            /* Columns in the process grid       */
  IPARAM_M,            /* Number of rows of the matrix      */
  IPARAM_N,            /* Number of columns of the matrix   */
  IPARAM_K,            /* RHS or K                          */
  IPARAM_LDA,          /* Leading dimension of A            */
  IPARAM_LDB,          /* Leading dimension of B            */
  IPARAM_LDC,          /* Leading dimension of C            */
  IPARAM_IB,           /* Inner-blocking size               */
  IPARAM_NB,           /* Number of columns in a tile       */
  IPARAM_MB,           /* Number of rows in a tile          */
  IPARAM_KQ,           /* Number of columns repetitions in a k-cyclic distribution */
  IPARAM_KP,           /* Number of rows repetititions in a k-cyclic distribution */
  IPARAM_HMB,          /* Small MB for recursive hdags */
  IPARAM_HNB,          /* Small NB for recursive hdags */
  IPARAM_CHECK,        /* Checking activated or not         */
  IPARAM_CHECKINV,     /* Inverse Checking activated or not */
  IPARAM_ASYNC,        /* Bench the asynchronous version    */
  IPARAM_VERBOSE,      /* How much noise do we want?        */
  IPARAM_LOWLVL_TREE,  /* Tree used for reduction inside nodes  (specific to xgeqrf_param) */
  IPARAM_HIGHLVL_TREE, /* Tree used for reduction between nodes (specific to xgeqrf_param) */
  IPARAM_QR_TS_SZE,    /* Size of TS domain                     (specific to xgeqrf_param) */
  IPARAM_QR_HLVL_SZE,  /* Size of the high level tree           (specific to xgeqrf_param) */
  IPARAM_RANDOM_SEED,  /* Seed for the pseudo-random generators */
  IPARAM_MATRIX_INIT,  /* Matrix generator type */
  IPARAM_QR_DOMINO,    /* Enable/disable the domino between the upper and the lower tree (specific to xgeqrf_param) */
  IPARAM_QR_TSRR,      /* Enable/disable the round-robin on TS domain */
  IPARAM_BUT_LEVEL,    /* Butterfly level */
  IPARAM_SCHEDULER,    /* User-selected scheduler */
  IPARAM_SIZEOF
};

#define PARSEC_SCHEDULER_DEFAULT 0
#define PARSEC_SCHEDULER_LFQ 1
#define PARSEC_SCHEDULER_LTQ 2
#define PARSEC_SCHEDULER_AP  3
#define PARSEC_SCHEDULER_LHQ 4
#define PARSEC_SCHEDULER_GD  5
#define PARSEC_SCHEDULER_PBQ 6
#define PARSEC_SCHEDULER_IP  7
#define PARSEC_SCHEDULER_RND 8

void iparam_default_facto(int* iparam);
void iparam_default_solve(int* iparam);
void iparam_default_gemm(int* iparam);
void iparam_default_ibnbmb(int* iparam, int ib, int nb, int mb);

#define PASTE_CODE_IPARAM_LOCALS(iparam)                                \
    int rank  = iparam[IPARAM_RANK];                                    \
    int nodes = iparam[IPARAM_NNODES];                                  \
    int cores = iparam[IPARAM_NCORES];                                  \
    int gpus  = iparam[IPARAM_NGPUS];                                   \
    int P     = iparam[IPARAM_P];                                       \
    int Q     = iparam[IPARAM_Q];                                       \
    int M     = iparam[IPARAM_M];                                       \
    int N     = iparam[IPARAM_N];                                       \
    int K     = iparam[IPARAM_K];                                       \
    int NRHS  = K;                                                      \
    int LDA   = max(M, iparam[IPARAM_LDA]);                             \
    int LDB   = max(N, iparam[IPARAM_LDB]);                             \
    int LDC   = max(K, iparam[IPARAM_LDC]);                             \
    int IB    = iparam[IPARAM_IB];                                      \
    int MB    = iparam[IPARAM_MB];                                      \
    int NB    = iparam[IPARAM_NB];                                      \
    int SMB   = iparam[IPARAM_KP];                                      \
    int SNB   = iparam[IPARAM_KQ];                                      \
    int HMB   = iparam[IPARAM_HMB];                                     \
    int HNB   = iparam[IPARAM_HNB];                                     \
    int MT    = (M%MB==0) ? (M/MB) : (M/MB+1);                          \
    int NT    = (N%NB==0) ? (N/NB) : (N/NB+1);                          \
    int KT    = (K%MB==0) ? (K/MB) : (K/MB+1);                          \
    int check = iparam[IPARAM_CHECK];                                   \
    int check_inv = iparam[IPARAM_CHECKINV];                            \
    int loud  = iparam[IPARAM_VERBOSE];                                 \
    int scheduler = iparam[IPARAM_SCHEDULER];                           \
    int random_seed = iparam[IPARAM_RANDOM_SEED];                       \
    int matrix_init = iparam[IPARAM_MATRIX_INIT];                       \
    int butterfly_level = iparam[IPARAM_BUT_LEVEL];                     \
    int async = iparam[IPARAM_ASYNC];                                   \
    (void)rank;(void)nodes;(void)cores;(void)gpus;(void)P;(void)Q;(void)M;(void)N;(void)K;(void)NRHS; \
    (void)LDA;(void)LDB;(void)LDC;(void)IB;(void)MB;(void)NB;(void)MT;(void)NT;(void)KT; \
    (void)SMB;(void)SNB;(void)HMB;(void)HNB;(void)check;(void)loud;(void)async; \
    (void)scheduler;(void)butterfly_level;(void)check_inv;(void)random_seed;(void)matrix_init;

/* Define a double type which not pass through the precision generation process */
typedef double DagDouble_t;
#define PASTE_CODE_FLOPS( FORMULA, PARAMS ) \
  double gflops = -1.0, flops = FORMULA PARAMS;

#if defined(PRECISION_z) || defined(PRECISION_c)
#define PASTE_CODE_FLOPS_COUNT(FADD,FMUL,PARAMS) \
  double gflops = -1.0, flops = (2. * FADD PARAMS + 6. * FMUL PARAMS);
#else
#define PASTE_CODE_FLOPS_COUNT(FADD,FMUL,PARAMS) \
  double gflops = -1.0, flops = (FADD PARAMS + FMUL PARAMS);
#endif

/*******************************
 * globals values
 *******************************/

#if defined(PARSEC_HAVE_MPI)
extern MPI_Datatype SYNCHRO;
#endif  /* PARSEC_HAVE_MPI */

extern const int side[2];
extern const int uplo[2];
extern const int diag[2];
extern const int trans[3];
extern const int norms[4];
extern const char *sidestr[2];
extern const char *uplostr[2];
extern const char *diagstr[2];
extern const char *transstr[3];
extern const char *normsstr[4];

void print_usage(void);

parsec_context_t *setup_parsec(int argc, char* argv[], int *iparam);
void cleanup_parsec(parsec_context_t* parsec, int *iparam);

/**
 * No macro with the name max or min is acceptable as there is
 * no way to correctly define them without borderline effects.
 */
#undef max
#undef min
static inline int max(int a, int b) { return a > b ? a : b; }
static inline int min(int a, int b) { return a < b ? a : b; }

/* Paste code to allocate a matrix in desc if cond_init is true */
#define PASTE_CODE_ALLOCATE_MATRIX(DC, COND, TYPE, INIT_PARAMS)      \
    TYPE##_t DC;                                                     \
    if(COND) {                                                          \
        TYPE##_init INIT_PARAMS;                                        \
        DC.mat = parsec_data_allocate((size_t)DC.super.nb_local_tiles * \
                                        (size_t)DC.super.bsiz *      \
                                        (size_t)parsec_datadist_getsizeoftype(DC.super.mtype)); \
        parsec_data_collection_set_key((parsec_data_collection_t*)&DC, #DC);          \
    }

#define PASTE_CODE_ENQUEUE_KERNEL(PARSEC, KERNEL, PARAMS)               \
    SYNC_TIME_START();                                                  \
    parsec_taskpool_t* PARSEC_##KERNEL = dplasma_##KERNEL##_New PARAMS;   \
    PARSEC_CHECK_ERROR(parsec_context_add_taskpool(PARSEC, PARSEC_##KERNEL), "parsec_context_add_taskpool");      \
    if( loud > 2 ) SYNC_TIME_PRINT(rank, ( #KERNEL "\tDAG created\n"));

#define PASTE_CODE_PROGRESS_KERNEL(PARSEC, KERNEL)                      \
    SYNC_TIME_START();                                                  \
    PARSEC_CHECK_ERROR(parsec_context_start(PARSEC), "parsec_context_start"); \
    TIME_START();                                                       \
    PARSEC_CHECK_ERROR(parsec_context_wait(PARSEC), "parsec_context_wait"); \
    SYNC_TIME_PRINT(rank, (#KERNEL "\tPxQ= %3d %-3d NB= %4d N= %7d : %14f gflops\n", \
                           P, Q, NB, N,                                 \
                           gflops=(flops/1e9)/sync_time_elapsed));      \
    PROFILING_SAVE_dINFO("TIME_ELAPSED", time_elapsed);                 \
    PROFILING_SAVE_dINFO("SYNC_TIME_ELAPSED", sync_time_elapsed);       \
    PROFILING_SAVE_dINFO("GFLOPS", gflops);                             \
    PROFILING_SAVE_iINFO("PARAM_RANK", iparam[IPARAM_RANK]);            \
    PROFILING_SAVE_iINFO("PARAM_NNODES", iparam[IPARAM_NNODES]);        \
    PROFILING_SAVE_iINFO("PARAM_NCORES", iparam[IPARAM_NCORES]);        \
    PROFILING_SAVE_iINFO("PARAM_NGPUS", iparam[IPARAM_NGPUS]);          \
    PROFILING_SAVE_iINFO("PARAM_P", iparam[IPARAM_P]);                  \
    PROFILING_SAVE_iINFO("PARAM_Q", iparam[IPARAM_Q]);                  \
    PROFILING_SAVE_iINFO("PARAM_M", iparam[IPARAM_M]);                  \
    PROFILING_SAVE_iINFO("PARAM_N", iparam[IPARAM_N]);                  \
    PROFILING_SAVE_iINFO("PARAM_K", iparam[IPARAM_K]);                  \
    PROFILING_SAVE_iINFO("PARAM_LDA", iparam[IPARAM_LDA]);              \
    PROFILING_SAVE_iINFO("PARAM_LDB", iparam[IPARAM_LDB]);              \
    PROFILING_SAVE_iINFO("PARAM_LDC", iparam[IPARAM_LDC]);              \
    PROFILING_SAVE_iINFO("PARAM_IB", iparam[IPARAM_IB]);                \
    PROFILING_SAVE_iINFO("PARAM_NB", iparam[IPARAM_NB]);                \
    PROFILING_SAVE_iINFO("PARAM_MB", iparam[IPARAM_MB]);                \
    PROFILING_SAVE_iINFO("PARAM_KP", iparam[IPARAM_KQ]);                \
    PROFILING_SAVE_iINFO("PARAM_KQ", iparam[IPARAM_KP]);                \
    PROFILING_SAVE_iINFO("PARAM_HNB", iparam[IPARAM_HNB]);              \
    PROFILING_SAVE_iINFO("PARAM_CHECK", iparam[IPARAM_CHECK]);          \
    PROFILING_SAVE_iINFO("PARAM_CHECKINV", iparam[IPARAM_CHECKINV]);    \
    PROFILING_SAVE_iINFO("PARAM_VERBOSE", iparam[IPARAM_VERBOSE]);      \
    PROFILING_SAVE_iINFO("PARAM_LOWLVL_TREE", iparam[IPARAM_LOWLVL_TREE]); \
    PROFILING_SAVE_iINFO("PARAM_HIGHLVL_TREE", iparam[IPARAM_HIGHLVL_TREE]); \
    PROFILING_SAVE_iINFO("PARAM_QR_TS_SZE", iparam[IPARAM_QR_TS_SZE]);  \
    PROFILING_SAVE_iINFO("PARAM_QR_HLVL_SZE", iparam[IPARAM_QR_HLVL_SZE]); \
    PROFILING_SAVE_iINFO("PARAM_QR_DOMINO", iparam[IPARAM_QR_DOMINO]);  \
    PROFILING_SAVE_iINFO("PARAM_QR_TSRR", iparam[IPARAM_QR_TSRR]);      \
    PROFILING_SAVE_iINFO("PARAM_BUT_LEVEL", iparam[IPARAM_BUT_LEVEL]);  \
    PROFILING_SAVE_iINFO("PARAM_SCHEDULER", iparam[IPARAM_SCHEDULER]);  \
    if(loud >= 5 && rank == 0) {                                        \
        printf("<DartMeasurement name=\"performance\" type=\"numeric/double\"\n" \
               "                 encoding=\"none\" compression=\"none\">\n" \
               "%g\n"                                                   \
               "</DartMeasurement>\n",                                  \
               gflops);                                                 \
    }                                                                   \
    (void)gflops;

#endif /* _TESTSCOMMON_H */

ext: h

max_stars_repo_name: therault/dplasma

max_issues_repo_name: therault/dplasma

max_forks_repo_name: therault/dplasma


text:
#pragma once

#include "halley/text/halleystring.h"
#include "halley/utils/utils.h"
#include <gsl/gsl>
#include <array>

namespace Halley {
	class Deserializer;
	class Serializer;

	class UUID {
    public:
        UUID();
        UUID(std::array<Byte, 16> bytes);
        explicit UUID(gsl::span<const gsl::byte> bytes);
		explicit UUID(const Bytes& bytes);
        explicit UUID(const String& str);

        bool operator==(const UUID& other) const;
        bool operator!=(const UUID& other) const;
		bool operator<(const UUID& other) const;

		String toString() const;

        static UUID generate();
        static UUID generateFromUUIDs(const UUID& one, const UUID& two);
    	bool isValid() const;

        gsl::span<const gsl::byte> getBytes() const;
		gsl::span<gsl::byte> getWriteableBytes();
        gsl::span<const uint64_t> getUint64Bytes() const;

    	void serialize(Serializer& s) const;
		void deserialize(Deserializer& s);

    private:
        std::array<uint64_t, 2> bytes;
    };
}

template<>
struct std::hash<Halley::UUID>
{
    std::size_t operator() (const Halley::UUID& uuid) const noexcept
    {
        const auto& bytes = uuid.getUint64Bytes();
        return bytes[0] ^ bytes[1];
    }
};

namespace natvis {
    struct x4lo {
    	uint8_t v: 4;
    	uint8_t _: 4;
    };
    struct x4hi {
	    uint8_t _ : 4;
    	uint8_t v : 4;
    };
    struct x8 {
	    uint8_t _;
    };
	struct x16 {
	    uint16_t _;
    };
    struct x32 {
	    uint32_t _;
    };
	struct x48 {
	    uint32_t b0;
		uint16_t b1;
    };
}

max_stars_repo_name: code-disaster/halley

max_issues_repo_name: code-disaster/halley

max_forks_repo_name: code-disaster/halley


text:
/// @file
///
/// Class to handle Taylor-term fitting to a spectrum
///
/// @copyright (c) 2017 CSIRO
/// Australia Telescope National Facility (ATNF)
/// Commonwealth Scientific and Industrial Research Organisation (CSIRO)
/// PO Box 76, Epping NSW 1710, Australia
/// atnf-enquiries@csiro.au
///
/// This file is part of the ASKAP software distribution.
///
/// The ASKAP software distribution is free software: you can redistribute it
/// and/or modify it under the terms of the GNU General Public License as
/// published by the Free Software Foundation; either version 3 of the License,
/// or (at your option) any later version.
///
/// This program is distributed in the hope that it will be useful,
/// but WITHOUT ANY WARRANTY; without even the implied warranty of
/// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
/// GNU General Public License for more details.
///
/// You should have received a copy of the GNU General Public License
/// along with this program; if not, write to the Free Software
/// Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307 USA
///
/// @author Matthew Whiting <Matthew.Whiting@csiro.au>
///
#ifndef ASKAP_ANALYSISUTILS_FIT_TT_H_
#define ASKAP_ANALYSISUTILS_FIT_TT_H_

#include <gsl/gsl_multifit.h>
#include <gsl/gsl_multifit_nlin.h>
#include <casacore/casa/Arrays/Array.h>

namespace askap {

namespace analysisutilities {

/// Data structure used within the fitting as a way of accessing the
/// various arrays within the GSL functions.
struct data {
    size_t ndata;
    double * xdat;
    double * ydat;
    double * weights;
};

/// @brief Class to perform non-linear fitting to find alpha & beta.
/// @details A non-linear function describing a
/// power-law-with-curvature function is fitted to a spectrum using
/// non-linear Levenberg-Marquardt algorithm. The function is F(nu) =
/// F_0 (nu/nu_0) ^ (alpha + beta * log(nu/nu_0)), where F_0 is the
/// flux at the reference frequency nu_0. It is a weighted fit,
/// taking into account a provided noise array. The number of terms is
/// user-selectable, from 1 (constant flux), 2 (constant flux +
/// spectral index) or 3 (add spectral curvature).
class FitTT {
    public:
        /// Initialise, setting the number of terms that should be fit.
        FitTT(unsigned int nterms);
        virtual ~FitTT() {};

        /// @brief Fit to provided arrays.
        /// @details For spectral-index fitting, x should be the
        /// frequencies divided by the reference frequency, and y should
        /// be the flux values. No weights array is provided, so weights
        /// are implicitly set to 1.  Front end to fit(size_t ndata,
        /// double *xdata, double *ydata, double *weights).
        void fit(casa::Array<float> &x, casa::Array<float> &y);

        /// @brief Fit to provided arrays, with associated weights array.
        /// @details For spectral-index fitting, x should be the
        /// frequencies divided by the reference frequency, y should be
        /// the flux values, and w the weights on the flux values
        /// (ie. noise). Front end to fit(size_t ndata, double *xdata,
        /// double *ydata, double *weights).
        void fit(casa::Array<float> &x, casa::Array<float> &y, casa::Array<float> &w);

        /// @brief Fit to provided arrays - main function that does the fitting.
        /// @details For spectral-index fitting, xdata should be the
        /// frequencies divided by the reference frequency, ydata should be
        /// the flux values, and weights the weights on the flux values
        /// (ie. noise), with ndata the size of the arrays.
        void fit(size_t ndata, double *xdata, double *ydata, double *weights);

        /// @brief Model function, for nterms=1
        static int taylor_f1(const gsl_vector * p, void *data,  gsl_vector * f);
        /// @brief Jacobian function, for nterms=1
        static int taylor_df1(const gsl_vector * p, void *data,  gsl_matrix * J);
        /// @brief Combined model & Jacobian function, for nterms=1
        static int taylor_fdf1(const gsl_vector * x, void *data, gsl_vector * f, gsl_matrix * J);
        /// @brief Model function, for nterms=2
        static int taylor_f2(const gsl_vector * p, void *data,  gsl_vector * f);
        /// @brief Jacobian function, for nterms=2
        static int taylor_df2(const gsl_vector * p, void *data,  gsl_matrix * J);
        /// @brief Combined model & Jacobian function, for nterms=2
        static int taylor_fdf2(const gsl_vector * x, void *data, gsl_vector * f, gsl_matrix * J);
        /// @brief Model function, for nterms=3
        static int taylor_f3(const gsl_vector * p, void *data,  gsl_vector * f);
        /// @brief Jacobian function, for nterms=3
        static int taylor_df3(const gsl_vector * p, void *data,  gsl_matrix * J);
        /// @brief Combined model & Jacobian function, for nterms=3
        static int taylor_fdf3(const gsl_vector * x, void *data, gsl_vector * f, gsl_matrix * J);

        /// @brief Return the fitted value of the flux at the reference pixel
        float fluxZero() {return itsFluxZero;};
        /// @brief Return the fitted value of the spectral index
        float alpha() {return itsAlpha;};
        /// @brief Return the fitted value of the spectral curvature
        float beta() {return itsBeta;};

        /// @brief Return the error on the fitted value of the flux at the reference frequency
        float fluxZeroErr() {return itsFluxZeroErr;};
        /// @brief Return the error on the fitted value of the spectral index
        float alphaErr() {return itsAlphaErr;};
        /// @brief Return the error on the fitted value of the spectral curvature
        float betaErr() {return itsBetaErr;};

    protected:
        /// @brief How many terms to fit?
        unsigned int itsNterms;

        /// @brief Flux at reference frequency
        float itsFluxZero;
        /// @brief Spectral index
        float itsAlpha;
        /// @brief Spectral curvature
        float itsBeta;
        /// @brief Error on flux at reference frequency
        float itsFluxZeroErr;
        /// @brief Error on spectral index
        float itsAlphaErr;
        /// @brief Error on spectral curvature
        float itsBetaErr;

};

}
}
#endif

max_stars_repo_name: steve-ord/askapsoft

max_issues_repo_name: ATNF/askapsoft

max_forks_repo_name: ATNF/askapsoft


text:
/********************************************************
  Stanford Driving Software
  Copyright (c) 2011 Stanford University
  All rights reserved.

  Redistribution and use in source and binary forms, with
  or without modification, are permitted provided that the
  following conditions are met:

* Redistributions of source code must retain the above
  copyright notice, this list of conditions and the
  following disclaimer.
* Redistributions in binary form must reproduce the above
  copyright notice, this list of conditions and the
  following disclaimer in the documentation and/or other
  materials provided with the distribution.
* The names of the contributors may not be used to endorse
  or promote products derived from this software
  without specific prior written permission.

  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND
  CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED
  WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
  WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
  PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT,
  INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
  CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
  PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
  DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
  CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE
  OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
  SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH
  DAMAGE.
 ********************************************************/

#ifndef GSL_SUPPORT_H
#define GSL_SUPPORT_H

#include <gsl/gsl_blas.h>

namespace vlr {

#define matrix_get gsl_matrix_get
#define vector_get gsl_vector_get
#define matrix_set gsl_matrix_set
#define vector_set gsl_vector_set
#define vector_copy gsl_vector_memcpy
#define matrix_copy gsl_matrix_memcpy
#define matrix_set_identity gsl_matrix_set_identity
#define vector_set_zero gsl_vector_set_zero
#define matrix_set_zero gsl_matrix_set_zero
#define vector_scale gsl_vector_scale

gsl_vector *vector_init(int length);
void vector_fill(gsl_vector *v, ...);
void vector_free(gsl_vector *vector);
gsl_matrix *matrix_init(int rows, int cols);
void matrix_fill(gsl_matrix *m, ...);
void matrix_free(gsl_matrix *matrix);
void vector_add(gsl_vector *result, gsl_vector *a, gsl_vector *b);
void vector_add_ip(gsl_vector *a, gsl_vector *b);
void vector_elem_add(gsl_vector *v, int elem, double x);
void vector_subtract(gsl_vector *result, gsl_vector *a,
                                gsl_vector *b);
void vector_subtract_ip(gsl_vector *a, gsl_vector *b);
void matrix_add(gsl_matrix *result, gsl_matrix *a, gsl_matrix *b);
void matrix_add_ip(gsl_matrix *a, gsl_matrix *b);
void matrix_elem_add(gsl_matrix *m, int row, int col, double x);
void matrix_subtract(gsl_matrix *result, gsl_matrix *a,
                                gsl_matrix *b);
void matrix_subtract_ip(gsl_matrix *a, gsl_matrix *b);
void matrix_multiply(gsl_matrix *result, gsl_matrix *a, int a_t,
                     gsl_matrix *b, int b_t);
void matrix_invert(gsl_matrix *inverse, gsl_matrix *m);
void matrix_invert_ip(gsl_matrix *m);
void matrix_vector_multiply(gsl_vector *result, gsl_matrix *a,
                                       gsl_vector *x);
void matrix_linear_transform(gsl_matrix *result, gsl_matrix *m,
                                        gsl_matrix *a);
void matrix_inverse_linear_transform(gsl_matrix *result,
                                                gsl_matrix *m, gsl_matrix *a);
void matrix_scale(gsl_matrix *m, double scale);
void matrix_print(gsl_matrix *m, const char *str);
void vector_print(gsl_vector *v, const char *str);
void matrix_print_signs(gsl_matrix *m, const char *str);
void matrix_to_file(gsl_matrix *m, const char *filename);
void vector_to_file(gsl_vector *v, const char *filename);
double vector_inner_product(gsl_vector *a, gsl_vector *b);
void gaussian_sample(gsl_vector *sample, gsl_vector *mean,
                                gsl_matrix *cov);
double matrix_determinant(gsl_matrix *A);

} // namespace vlr

#endif


text:
/*
**  Matrix Projection,
**   Ref:  Lohmann, Loktyushin, Stelzer, Scheffler (2018) bioRXiv
**
** G.Lohmann, MPI-KYB, Nov 2018
*/

#include <viaio/Vlib.h>
#include <viaio/VImage.h>
#include <viaio/mu.h>
#include <viaio/option.h>

#include <gsl/gsl_matrix.h>
#include <gsl/gsl_vector.h>
#include <gsl/gsl_errno.h>
#include <gsl/gsl_cblas.h>
#include <gsl/gsl_rng.h>
#include <gsl/gsl_randist.h>
#include <gsl/gsl_linalg.h>

#include <stdio.h>
#include <stdlib.h>
#include <math.h>

#ifdef _OPENMP
#include <omp.h>
#endif /*_OPENMP*/

#define SQR(x) ((x) * (x))
#define IMIN(x,y) ((x) < (y) ? (x) : (y))
#define IMAX(x,y) ((x) > (y) ? (x) : (y))

extern double ECMcorrelation(const float *arr1,const float *arr2,size_t nt,int type);
extern void NormVec(float *x,size_t);

void VMatrixProjection(gsl_matrix_float *X,float *ev,int type,int seed)
{
  size_t i,j;
  size_t nvox = X->size1;
  size_t nt = X->size2;
  size_t p = 32;

  fprintf(stderr," VMatrixProjection...\n");

  /* generate random matrix */
  const gsl_rng_type *Tx = gsl_rng_default;
  gsl_rng *rx = gsl_rng_alloc (Tx);
  gsl_rng_set(rx,(unsigned long int)seed);
  gsl_matrix *R = gsl_matrix_calloc(nvox,p);
  for (i=0; i<nvox; i++) {
    for (j=0; j<p; j++) {
      gsl_matrix_set(R,i,j,gsl_ran_ugaussian(rx));
    }
  }

  /* matrix product 1 */
  gsl_matrix *Y = gsl_matrix_calloc(nvox,p);
  size_t progress=0;
  size_t step=4;  /* sparse */
  fprintf(stderr," pass 1:\n");

#pragma omp parallel for shared(progress) schedule(guided) firstprivate(X,Y,R)
  for (i=0; i<nvox; i++) {
    if (i%1000 == 0) fprintf(stderr," %d000  of  %lu\r",(int)(++progress),nvox);

    size_t j=0,k=0;
    double *tmp1 = (double *)VCalloc(nvox,sizeof(double));
    double *tmp2 = NULL;
    double sum=0;
    const float *arr1 = gsl_matrix_float_const_ptr(X,i,0);

    for (j=0; j<nvox; j++) {
      const float *arr2 = gsl_matrix_float_const_ptr(X,j,0);
      tmp1[j] = ECMcorrelation(arr1,arr2,nt,type);
    }

    for (j=0; j<p; j++) {
      tmp2 = gsl_matrix_ptr(R,j,0);
      sum=0;
      for (k=0; k<nvox; k+=step) {
	sum += tmp1[k]*tmp2[k];
      }
      gsl_matrix_set(Y,i,j,sum);
    }
    VFree(tmp1);
  }
  fprintf(stderr,"\n");
  gsl_matrix_free(R);

  /* get orthonormal basis for Y  (SVD) */
  gsl_vector *sv = gsl_vector_calloc(p);
  gsl_vector *work = gsl_vector_calloc(p);
  gsl_matrix *V = gsl_matrix_calloc(p,p);
  gsl_linalg_SV_decomp(Y,V,sv,work);

  /* matrix product 2 */
  fprintf(stderr," pass 2:\n");
  gsl_matrix *D = gsl_matrix_calloc(nvox,p);
  progress=0;

  #pragma omp parallel for shared(progress) schedule(guided) firstprivate(X,Y,D)
  for (i=0; i<nvox; i++) {
    if (i%1000 == 0) fprintf(stderr," %d000  of  %lu\r",(int)(++progress),nvox);

    size_t j=0,k=0;
    double *tmp1 = (double *)VCalloc(nvox,sizeof(double));
    double sum=0;
    const float *arr1 = gsl_matrix_float_const_ptr(X,i,0);

    for (j=0; j<nvox; j++) {
      const float *arr2 = gsl_matrix_float_const_ptr(X,j,0);
      tmp1[j] = ECMcorrelation(arr1,arr2,nt,type);
    }

    for (j=0; j<p; j++) {
      sum=0;
      for (k=0; k<nvox; k+=step) {
	sum += tmp1[k] * gsl_matrix_get(Y,k,j);
      }
      gsl_matrix_set(D,i,j,sum);
    }
    VFree(tmp1);
  }
  fprintf(stderr,"\n");
  gsl_matrix_free(Y);

  /* final SVD */
  gsl_linalg_SV_decomp(D,V,sv,work);

  /* output */
  size_t k=0;
  for (i=0; i<nvox; i++) {
    ev[i] = gsl_matrix_get(D,i,0);
    if (ev[i] < 0) k++;
  }

  /* sign switch if needed */
  if (k > nvox/2) {
    for (i=0; i<nvox; i++) {
      ev[i] = -ev[i];
    }
  }

  /* normalize */
  NormVec(ev,nvox);
  float kx = sqrt((float)(nvox));
  for (i=0; i<nvox; i++)  ev[i] *= kx;
}

max_stars_repo_name: zrajna/lipsia

max_issues_repo_name: zrajna/lipsia

max_forks_repo_name: zrajna/lipsia


text:
/*
 * Copyright (c) 1997-1999 Massachusetts Institute of Technology
 *
 * This program is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 *
 */

/* This file was automatically generated --- DO NOT EDIT */
/* Generated on Sun Nov  7 20:43:52 EST 1999 */

#include <fftw-int.h>
#include <fftw.h>

/* Generated by: ./genfft -magic-alignment-check -magic-twiddle-load-all -magic-variables 4 -magic-loopi -real2hc 1 */

/*
 * This function contains 0 FP additions, 0 FP multiplications,
 * (or, 0 additions, 0 multiplications, 0 fused multiply/add),
 * 1 stack variables, and 2 memory accesses
 */

/*
 * Generator Id's :
 * $Id: exprdag.ml,v 1.41 1999/05/26 15:44:14 fftw Exp $
 * $Id: fft.ml,v 1.43 1999/05/17 19:44:18 fftw Exp $
 * $Id: to_c.ml,v 1.25 1999/10/26 21:41:32 stevenj Exp $
 */

void fftw_real2hc_1(const fftw_real *input, fftw_real *real_output, fftw_real *imag_output, int istride, int real_ostride, int imag_ostride)
{
     fftw_real tmp1;
     ASSERT_ALIGNED_DOUBLE;
     tmp1 = input[0];
     real_output[0] = tmp1;
}

fftw_codelet_desc fftw_real2hc_1_desc =
{
     "fftw_real2hc_1",
     (void (*)()) fftw_real2hc_1,
     1,
     FFTW_FORWARD,
     FFTW_REAL2HC,
     24,
     0,
     (const int *) 0,
};

max_stars_repo_name: albertsgrc/ftdock-opt

max_issues_repo_name: albertsgrc/ftdock-opt

max_forks_repo_name: albertsgrc/ftdock-opt


text:
#ifndef gigp_header

#define gigp_header

#include <gsl/gsl_errno.h>
#include <gsl/gsl_sf_bessel.h>
#include <gsl/gsl_integration.h>
#include <gsl/gsl_multimin.h>
#include <gsl/gsl_rng.h>
#include <gsl/gsl_randist.h>

#define GIGP_GAMMA_ROW 0
#define GIGP_B_ROW 1
#define GIGP_C_ROW 2
#define GIGP_N_ROW 3
#define GIGP_s_ROW 4
#define GIGP_S_ROW 5
#define GIGP_MAXCOUNT_ROW 6
#define GIGP_FIT_ROW 7

struct gigp_param{
        double gamma;
        double b;
        double c;
        double N;
        double s;
        double S;
        double max_count;
        double fit;
};

extern struct gigp_param* fit_exact_gigp(struct gigp_param* gigp_param,double* fx_unique_transcript_count, int len);
extern double gigp_dist (double x, void * p);
extern double sichel_function(const gsl_vector *v, void *params);
extern struct gigp_param* init_gigp_param(void);
extern int copy_gigp_param(struct gigp_param* source, struct gigp_param* target);
extern double give_me_sichel_p0(struct gigp_param* gigp_param ,double* p);

/* housekeeping stuff */
extern struct gigp_param* init_gigp_param(void);
extern int clear_gigp_param(struct gigp_param* tmp);
extern int copy_gigp_param(struct gigp_param* source, struct gigp_param* target);

#endif

max_stars_repo_name: TimoLassmann/SingleCellSim

max_issues_repo_name: TimoLassmann/SingleCellSim

max_forks_repo_name: TimoLassmann/SingleCellSim


text:
#ifndef MATH_FUNCTIONS_H
#define MATH_FUNCTIONS_H

#include "string.h"
#include <math.h>

extern "C" {
#include <cblas.h>
}

void caffe_copy(const int N, const float *X, float *Y);

void caffe_set(const int N, const float alpha, float *X);

void caffe_cpu_gemm(const CBLAS_TRANSPOSE TransA,
	const CBLAS_TRANSPOSE TransB, const int M, const int N, const int K,
	const float alpha, const float* A, const float* B, const float beta,
	float* C);

void caffe_sqr(const int N, const float* a, float* y);

float caffe_cpu_asum(const int n, const float* x);

void caffe_cpu_scale(const int n, const float alpha, const float *x, float* y);

void caffe_cpu_gemv(const CBLAS_TRANSPOSE TransA, const int M,
	const int N, const float alpha, const float* A, const float* x,
	const float beta, float* y);

void caffe_powx(const int n, const float* a, const float b, float* y);

void caffe_div(const int n, const float* a, const float* b, float* y);

void caffe_scal(const int N, const float alpha, float *X);

void caffe_mul(const int n, const float* a, const float* b, float* y);

void caffe_exp(const int n, const float* a, float* y);

#endif


text:
/* min/fsolver.c
 *
 * Copyright (C) 1996, 1997, 1998, 1999, 2000 Brian Gough
 *
 * This program is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or (at
 * your option) any later version.
 *
 * This program is distributed in the hope that it will be useful, but
 * WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program; if not, write to the Free Software
 * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA.
 */

#include <config.h>
#include <stdlib.h>
#include <string.h>
#include <gsl/gsl_errno.h>
#include <gsl/gsl_min.h>

#include "min.h"

static int
compute_f_values (gsl_function * f, double x_minimum, double * f_minimum,
                  double x_lower, double * f_lower,
                  double x_upper, double * f_upper);

static int
compute_f_values (gsl_function * f, double x_minimum, double * f_minimum,
                  double x_lower, double * f_lower,
                  double x_upper, double * f_upper)
{
  SAFE_FUNC_CALL(f, x_lower, f_lower);
  SAFE_FUNC_CALL(f, x_upper, f_upper);
  SAFE_FUNC_CALL(f, x_minimum, f_minimum);

  return GSL_SUCCESS;
}

int
gsl_min_fminimizer_set (gsl_min_fminimizer * s,
                        gsl_function * f,
                        double x_minimum, double x_lower, double x_upper)
{
  int status ;

  double f_minimum, f_lower, f_upper;

  status = compute_f_values (f, x_minimum, &f_minimum,
                             x_lower, &f_lower,
                             x_upper, &f_upper);

  if (status != GSL_SUCCESS)
    {
      return status ;
    }

  status = gsl_min_fminimizer_set_with_values (s, f, x_minimum, f_minimum,
                                               x_lower, f_lower,
                                               x_upper, f_upper);
  return status;
}

gsl_min_fminimizer *
gsl_min_fminimizer_alloc (const gsl_min_fminimizer_type * T)
{
  gsl_min_fminimizer * s =
    (gsl_min_fminimizer *) malloc (sizeof (gsl_min_fminimizer));

  if (s == 0)
    {
      GSL_ERROR_VAL ("failed to allocate space for minimizer struct",
                        GSL_ENOMEM, 0);
    };

  s->state = malloc (T->size);

  if (s->state == 0)
    {
      free (s);         /* exception in constructor, avoid memory leak */

      GSL_ERROR_VAL ("failed to allocate space for minimizer state",
                        GSL_ENOMEM, 0);
    };

  s->type = T ;
  s->function = NULL;

  return s;
}

int
gsl_min_fminimizer_set_with_values (gsl_min_fminimizer * s, gsl_function * f,
                                    double x_minimum, double f_minimum,
                                    double x_lower, double f_lower,
                                    double x_upper, double f_upper)
{
  s->function = f;
  s->x_minimum = x_minimum;
  s->x_lower = x_lower;
  s->x_upper = x_upper;

  if (x_lower > x_upper)
    {
      GSL_ERROR ("invalid interval (lower > upper)", GSL_EINVAL);
    }

  if (x_minimum >= x_upper || x_minimum <= x_lower)
    {
      GSL_ERROR ("x_minimum must lie inside interval (lower < x < upper)",
                 GSL_EINVAL);
    }

  s->f_lower = f_lower;
  s->f_upper = f_upper;
  s->f_minimum = f_minimum;

  if (f_minimum >= f_lower || f_minimum >= f_upper)
    {
      GSL_ERROR ("endpoints do not enclose a minimum", GSL_EINVAL);
    }

  return (s->type->set) (s->state, s->function,
                         x_minimum, f_minimum,
                         x_lower, f_lower,
                         x_upper, f_upper);
}

int
gsl_min_fminimizer_iterate (gsl_min_fminimizer * s)
{
  return (s->type->iterate) (s->state, s->function,
                             &(s->x_minimum), &(s->f_minimum),
                             &(s->x_lower), &(s->f_lower),
                             &(s->x_upper), &(s->f_upper));
}

void
gsl_min_fminimizer_free (gsl_min_fminimizer * s)
{
  free (s->state);
  free (s);
}

const char *
gsl_min_fminimizer_name (const gsl_min_fminimizer * s)
{
  return s->type->name;
}

/* Deprecated, use x_minimum instead */
double
gsl_min_fminimizer_minimum (const gsl_min_fminimizer * s)
{
  return s->x_minimum;
}

double
gsl_min_fminimizer_x_minimum (const gsl_min_fminimizer * s)
{
  return s->x_minimum;
}

double
gsl_min_fminimizer_x_lower (const gsl_min_fminimizer * s)
{
  return s->x_lower;
}

double
gsl_min_fminimizer_x_upper (const gsl_min_fminimizer * s)
{
  return s->x_upper;
}

double
gsl_min_fminimizer_f_minimum (const gsl_min_fminimizer * s)
{
  return s->f_minimum;
}

double
gsl_min_fminimizer_f_lower (const gsl_min_fminimizer * s)
{
  return s->f_lower;
}

double
gsl_min_fminimizer_f_upper (const gsl_min_fminimizer * s)
{
  return s->f_upper;
}

max_stars_repo_name: manggoguy/parsec-modified

max_issues_repo_name: manggoguy/parsec-modified

max_forks_repo_name: manggoguy/parsec-modified