← Back to branch summary

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

« back to all changes in this revision

Viewing changes to examples/AIM5/PolyDep/Homogenous/Base.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/AIM5/PolyDep/Homogenous/Base.agda
1
 
{-# OPTIONS --no-positivity-check --no-termination-check #-}
2
 
module Homogenous.Base where
3
 
 
4
 
import TYPE
5
 
import PolyDepPrelude
6
 
 
7
 
open PolyDepPrelude using
8
 
  ( Absurd
9
 
  ; Unit; unit
10
 
  ; Nat; zero; suc
11
 
  ; List; nil; _::_
12
 
  ; Either; left; right
13
 
  ; Pair; pair)
14
 
 
15
 
 
16
 
Arity : Set
17
 
Arity = Nat
18
 
 
19
 
Sig   : Set
20
 
Sig   = List Arity
21
 
 
22
 
 
23
 
 
24
 
Fa : (n : Arity) -> Set -> Set
25
 
Fa (zero)  X = Unit
26
 
Fa (suc m) X = Pair X (Fa m X)
27
 
 
28
 
 ----------------------------------------------------------------
29
 
Fa1 : (n : Arity) -> {a b : Set} -> (a -> b) -> Fa n a -> Fa n b
30
 
Fa1 (zero)  f (unit)         = unit
31
 
Fa1 (suc m) f (pair fst snd) = pair (f fst) (Fa1 m f snd)
32
 
 
33
 
 
34
 
F : (fi : Sig)(X : Set) -> Set
35
 
F (nil)      X = Absurd
36
 
F (n :: fi') X = Either (Fa n X) (F fi' X)
37
 
 
38
 
F1 : (fi : Sig){a b : Set}(f : a -> b)(x : F fi a) -> F fi b
39
 
F1 (nil)      f ()        -- empty
40
 
F1 (n :: ns)  f (left  t) = left  (Fa1 n f t)
41
 
F1 (n :: ns)  f (right y) = right (F1 ns f y)
42
 
 
43
 
 
44
 
FIHa : (n : Arity){X : Set}(C : X -> Set)(x : Fa n X) -> Set
45
 
FIHa (zero)  C unit           = Unit
46
 
FIHa (suc m) C (pair fst snd) = Pair (C fst) (FIHa m C snd)
47
 
 
48
 
FIH : (fi : Sig){X : Set}(C : X -> Set)(x : F fi X) -> Set
49
 
FIH (nil)      C ()      -- empty
50
 
FIH (n :: ns)  C (left  t) = FIHa n C t
51
 
FIH (n :: ns)  C (right y) = FIH ns C y
52
 
 
53
 
Fmapa : (n : Arity){X : Set}{C : X -> Set}(h : (x : X) -> C x)(u : Fa n X)
54
 
      -> FIHa n C u
55
 
Fmapa (zero)  h (unit)         = unit
56
 
Fmapa (suc m) h (pair fst snd) = pair (h fst) (Fmapa m h snd)
57
 
 
58
 
Fmap : (fi : Sig){X : Set}{C : X -> Set}(h : (x : X) -> C x)(u : F fi X)
59
 
     -> FIH fi C u
60
 
Fmap (nil)      h () -- empty
61
 
Fmap (n :: ns)  h (left  x) = Fmapa n h x
62
 
Fmap (n :: ns)  h (right y) = Fmap ns h y
63
 
 
64
 
 
65
 
data T (fi : Sig) : Set where
66
 
  Intro : F fi (T fi) -> T fi
67
 
 
68
 
It : (fi : Sig){C : Set}(d : F fi C -> C) -> T fi -> C
69
 
It fi d (Intro i) = d (F1 fi (It fi d) i)
70
 
 
71
 
 
72
 
MIt : (fi : Sig){C : Set}(s : {X : Set} -> (X -> C) -> F fi X -> C)
73
 
    -> T fi -> C
74
 
MIt fi s (Intro i) = s (MIt fi s) i
75
 
 
76
 
R : (fi : Sig)
77
 
    {C : T fi -> Set}
78
 
    (d : (y : F fi (T fi)) -> FIH fi C y -> C (Intro y))
79
 
    (x : T fi) -> C x
80
 
R fi d (Intro i) = d i (Fmap fi (R fi d) i)
81
 
 
82
 
 
83
 
FIHs : (fi : Sig) -> (T fi -> Set) -> F fi (T fi) -> Set
84
 
FIHs fi = FIH fi
85
 
 
86
 
 
87
 
out : (fi : Sig) -> T fi -> F fi (T fi)
88
 
out fi = R fi (\y p -> y)
89
 
 
90
 
----------------------------------------------------------------
91
 
 
92
 
FIHaT : (n : Arity)(X : Set)(C : X -> Set1)(x : Fa n X) -> Set1
93
 
FIHaT (zero)  X C (unit)         = TYPE.Unit
94
 
FIHaT (suc m) X C (pair fst snd) = TYPE.Pair (C fst) (FIHaT m X C snd)
95
 
 
96
 
 
97
 
FIHT : (fi : Sig)(X : Set)(C : X -> Set1)(x : F fi X) -> Set1
98
 
FIHT (nil)      X C () -- empty
99
 
FIHT (n :: ns)  X C (left  t) = FIHaT n X C t
100
 
FIHT (n :: ns)  X C (right y) = FIHT ns X C y
101
 
 
102
 
FIHsT : (fi : Sig)(C : T fi -> Set1)(x : F fi (T fi)) -> Set1
103
 
FIHsT fi C x = FIHT fi (T fi) C x
104
 
 
105
 
FmapaT : (n : Arity){X : Set}{C : X -> Set1}(h : (x : X) -> C x)(u : Fa n X)
106
 
  -> FIHaT n X C u
107
 
FmapaT (zero)  h (unit)         = TYPE.unit
108
 
FmapaT (suc m) h (pair fst snd) = TYPE.pair (h fst) (FmapaT m h snd)
109
 
 
110
 
FmapT : (fi : Sig){X : Set}{C : X -> Set1}(h : (x : X) -> C x)(u : F fi X)
111
 
      -> FIHT fi X C u
112
 
FmapT (nil)      h () -- empty
113
 
FmapT (n :: ns)  h (left  x') = FmapaT n h x'
114
 
FmapT (n :: ns)  h (right y)  = FmapT ns h y
115
 
 
116
 
RT : (fi : Sig)
117
 
     {C : T fi -> Set1}
118
 
     (d : (y : F fi (T fi)) -> FIHT fi (T fi) C y -> C (Intro y))
119
 
     (x : T fi) -> C x
120
 
RT fi d (Intro i) = d i (FmapT fi (RT fi d) i)