{-

  Agda modules. Crash course.

-}

-- Each Agda file contains a single top-level module with
-- the same name as the file.
module Modules where

-- importing gives you access to modules defined in other files
-- opening lets you use the names from the module unqualified
open import Data.Bool   -- defined in Data/Bool.agda
open import Data.List

-- Parameterized modules are similar to Coq sections.

module Sort {A : Set}(_≤_ : A → A → Bool) where

  insert : A → List A → List A
  insert y [] = y ∷ []
  insert y (x ∷ xs) =
    if y ≤ x then y ∷ x ∷ xs
             else x ∷ insert y xs

  sort : List A → List A
  sort []       = []
  sort (x ∷ xs) = insert x (sort xs)

-- Now let's sort something!

-- This is a wrapper module for Data.Nat from the standard library
-- that defines boolean _≤_ and _≥_.
open import Nat

-- We can instantiate the parameters of a parameterized module
-- (the A parameter is implicit)
open Sort _≤_

-- Now sort : List ℕ → List ℕ

xs =  ∷  ∷  ∷  ∷  ∷ []

test₁ = sort xs

-- using the non-instantiated sort
test₂ = Sort.sort _≥_ xs

-- We might want to give a nicer name to Sort.sort

open Sort using () renaming (sort to sortBy)

test₃ = sortBy _≥_ xs