{-

  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 = 3  7  0  10  2  []

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