← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to examples/Introduction/Modules/Parameterised.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
examples/Introduction/Modules/Parameterised.agda
1
 
 
2
 
 
3
 
module Introduction.Modules.Parameterised where
4
 
 
5
 
 
6
 
data Bool : Set where
7
 
  false : Bool
8
 
  true  : Bool
9
 
 
10
 
data List (A : Set) : Set where
11
 
  nil  : List A
12
 
  _::_ : A -> List A -> List A
13
 
 
14
 
infixr 15 _::_    -- see 'Introduction.Operators' for information on infix
15
 
                  -- declarations
16
 
 
17
 
 
18
 
module Sorting {A : Set}(_<_ : A -> A -> Bool) where
19
 
 
20
 
  insert : A -> List A -> List A
21
 
  insert x  nil      = x :: nil
22
 
  insert x (y :: ys) = ins (x < y)
23
 
    where
24
 
      ins : Bool -> List A      -- local functions can do pattern matching and
25
 
      ins true  = x :: y :: ys  -- be recursive
26
 
      ins false = y :: insert x ys
27
 
 
28
 
  sort : List A -> List A
29
 
  sort  nil      = nil
30
 
  sort (x :: xs) = insert x (sort xs)
31
 
 
32
 
 
33
 
data Nat : Set where
34
 
  zero : Nat
35
 
  suc  : Nat -> Nat
36
 
 
37
 
_<_ : Nat -> Nat -> Bool
38
 
zero  < zero  = false
39
 
zero  < suc _ = true
40
 
suc _ < zero  = false
41
 
suc n < suc m = n < m
42
 
 
43
 
module SortNat = Sorting _<_
44
 
 
45
 
sort' : {A : Set}(_<_ : A -> A -> Bool) -> List A -> List A
46
 
sort' less = Sort'.sort
47
 
  where
48
 
    module Sort' = Sorting less
49
 
 
50
 
open SortNat
51
 
 
52
 
test = sort (suc zero :: zero :: suc (suc zero) :: nil)
53