| 123456789101112131415161718192021222324252627282930313233 |
- module _ where
- open import Common.Prelude renaming (_∸_ to _-_) -- work-around for #1855
- _<_ : Nat → Nat → Bool
- a < b with b - a
- ... | zero = false
- ... | suc _ = true
- insert : Nat → List Nat → List Nat
- insert x [] = x ∷ []
- insert x (y ∷ xs) = if x < y then x ∷ y ∷ xs else (y ∷ insert x xs)
- sort : List Nat → List Nat
- sort [] = []
- sort (x ∷ xs) = insert x (sort xs)
- downFrom : Nat → List Nat
- downFrom zero = []
- downFrom (suc n) = n ∷ downFrom n
- mapM! : {A : Set} → (A → IO Unit) → List A → IO Unit
- mapM! f [] = return unit
- mapM! f (x ∷ xs) = f x >>= λ _ → mapM! f xs
- main : IO Unit
- main = mapM! printNat (sort (downFrom 1200))
- -- 1000 0.6s
- -- 2000 4.8s
- -- 4000 36.2s
|
