← Back to branch summary

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

« back to all changes in this revision

Viewing changes to examples/sinatra/Example.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/sinatra/Example.agda
1
 
 
2
 
module Example where
3
 
 
4
 
open import Prelude
5
 
import Typed
6
 
 
7
 
data Data : Set where
8
 
  nat  : Data
9
 
  bool : Data
10
 
 
11
 
Datatype : Data -> List (List Data)
12
 
Datatype nat  = ε ◄ ε ◄ (ε ◄ nat)
13
 
Datatype bool = ε ◄ ε ◄ ε
14
 
 
15
 
data Effect : Set where
16
 
 
17
 
data _⊆_ : Effect -> Effect -> Set where
18
 
  refl⊆  : forall {M} -> M ⊆ M
19
 
 
20
 
Monad : Effect -> Set -> Set
21
 
Monad e A = A
22
 
 
23
 
return : forall {M A} -> A -> Monad M A
24
 
return x = x
25
 
 
26
 
map    : forall {M A B} -> (A -> B) -> Monad M A -> Monad M B
27
 
map f m = f m
28
 
 
29
 
join   : forall {M A} -> Monad M (Monad M A) -> Monad M A
30
 
join m = m
31
 
 
32
 
morph  : forall {M N} -> M ⊆ N -> (A : Set) -> Monad M A -> Monad N A
33
 
morph _ A x = x
34
 
 
35
 
open module TT =
36
 
       Typed Data Datatype
37
 
             Effect _⊆_
38
 
             Monad
39
 
             (\{M A} -> return {M}{A})
40
 
             (\{M A B} -> map {M}{A}{B})
41
 
             (\{M A} -> join {M}{A})
42
 
             morph
43
 
 
44
 
zero : forall {M Γ} -> InV M Γ (TyCon nat)
45
 
zero = con (tl hd) ⟨⟩
46
 
 
47
 
suc : forall {M Γ} -> InV M Γ (TyCon nat) -> InV M Γ (TyCon nat)
48
 
suc n = con hd (⟨⟩ ◃ n)
49
 
 
50
 
true : forall {M Γ} -> InV M Γ (TyCon bool)
51
 
true = con hd ⟨⟩
52
 
 
53
 
false : forall {M Γ} -> InV M Γ (TyCon bool)
54
 
false = con (tl hd) ⟨⟩