← Back to branch summary

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

« back to all changes in this revision

Viewing changes to examples/AIM4/bag/List.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/AIM4/bag/List.agda
1
 
 
2
 
module List where
3
 
 
4
 
  import Prelude
5
 
  import Equiv
6
 
  import Datoid
7
 
  import Nat
8
 
 
9
 
  open Prelude
10
 
  open Equiv
11
 
  open Datoid
12
 
  open Nat
13
 
 
14
 
  data List (a : Set) : Set where
15
 
    nil  : List a
16
 
    _::_ : a -> List a -> List a
17
 
 
18
 
  map : {a b : Set} -> (a -> b) -> List a -> List b
19
 
  map f nil       = nil
20
 
  map f (x :: xs) = f x :: map f xs
21
 
 
22
 
  member : (a : Datoid) -> El a -> List (El a) -> Set
23
 
  member _ x nil       = Absurd
24
 
  member a x (y :: ys) = Either (rel' (datoidEq a) x y) (member a x ys)
25
 
 
26
 
  memberPreservesEq
27
 
    :  {a : Datoid}
28
 
    -> {x y : El a}
29
 
    -> datoidRel a x y
30
 
    -> (zs : List (El a))
31
 
    -> member a x zs
32
 
    -> member a y zs
33
 
  memberPreservesEq     xy nil       abs         = abs
34
 
  memberPreservesEq {a} xy (z :: zs) (left xz)   =
35
 
    left  (dTrans a (dSym a xy) xz)
36
 
  memberPreservesEq {a} xy (z :: zs) (right xzs) =
37
 
    right (memberPreservesEq {a} xy zs xzs)
38
 
 
39
 
  private
40
 
    noCopies' : (a : Datoid) -> (x y : El a) -> Dec (datoidRel a x y) 
41
 
              -> Nat -> Nat
42
 
    noCopies' _ _ _ (left _)  n = suc n
43
 
    noCopies' _ _ _ (right _) n = n
44
 
 
45
 
  noCopies : (a : Datoid) -> El a -> List (El a) -> Nat
46
 
  noCopies a x nil       = zero
47
 
  noCopies a x (y :: ys) =
48
 
    noCopies' a x y (datoidDecRel a x y) (noCopies a x ys)
49
 
 
50
 
  NoDuplicates : (a : Datoid) -> List (El a) -> Set
51
 
  NoDuplicates _ nil      = Unit
52
 
  NoDuplicates a (x :: b) = Pair (Not (member a x b)) (NoDuplicates a b)
53
 
 
54
 
  private
55
 
    delete'
56
 
      : (a : Datoid)
57
 
      -> (x y : El a)
58
 
      -> Dec (datoidRel a x y)
59
 
      -> (ys delXYs : List (El a))
60
 
      -> List (El a)
61
 
    delete' _ _ _ (left _)  ys _      = ys
62
 
    delete' _ _ _ (right _) _  delXYs = delXYs
63
 
 
64
 
  -- Removes first occurrence if any.
65
 
  delete : (a : Datoid) -> El a -> List (El a) -> List (El a)
66
 
  delete a x nil       = nil
67
 
  delete a x (y :: ys) = delete' a x y (datoidDecRel a x y) ys (delete a x ys)
68
 
 
69
 
  private
70
 
    Perm : (a : Datoid) -> (xs ys : List (El a)) -> Set
71
 
    Perm a xs ys = forall z -> datoidRel natDatoid (noCopies a z xs)
72
 
                                                   (noCopies a z ys)
73
 
 
74
 
    refl' : {a : Datoid} -> (xs : List (El a)) -> Perm a xs xs
75
 
    refl' {a} xs = \z -> dRefl natDatoid {noCopies a z xs}
76
 
 
77
 
    sym' :  {a : Datoid} -> (xs ys : List (El a))
78
 
         -> Perm a xs ys -> Perm a ys xs
79
 
    sym' {a} xs ys xy =
80
 
      \z -> dSym natDatoid {noCopies a z xs} {noCopies a z ys} (xy z)
81
 
 
82
 
    trans' : {a : Datoid} -> (xs ys zs : List (El a))
83
 
           -> Perm a xs ys -> Perm a ys zs -> Perm a xs zs
84
 
    trans' {a} xs ys zs xy yz =
85
 
      \z -> dTrans natDatoid
86
 
                   {noCopies a z xs} {noCopies a z ys} {noCopies a z zs}
87
 
                   (xy z) (yz z)
88
 
 
89
 
    postulate
90
 
      dec' : {a : Datoid} -> (xs ys : List (El a))
91
 
             -> Either (Perm a xs ys) (Not (Perm a xs ys))
92
 
 
93
 
  Permutation : (a : Datoid) -> DecidableEquiv (List (El a))
94
 
  Permutation a = decEquiv (equiv (Perm a) (refl' {a}) (sym' {a}) (trans' {a})) (dec (dec' {a}))
95