← Back to branch summary

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

« back to all changes in this revision

Viewing changes to examples/outdated-and-incorrect/AIM6/Cat/lib/Data/Real/Complete.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/outdated-and-incorrect/AIM6/Cat/lib/Data/Real/Complete.agda
1
 
 
2
 
module Data.Real.Complete where
3
 
 
4
 
import Prelude
5
 
import Data.Real.Gauge
6
 
import Data.Rational
7
 
 
8
 
open Prelude
9
 
open Data.Real.Gauge
10
 
open Data.Rational
11
 
 
12
 
Complete : Set -> Set
13
 
Complete A = Gauge -> A
14
 
 
15
 
unit : {A : Set} -> A -> Complete A
16
 
unit x ε = x
17
 
 
18
 
join : {A : Set} -> Complete (Complete A) -> Complete A
19
 
join f ε = f ε2 ε2
20
 
  where
21
 
    ε2 = ε / fromNat 2
22
 
 
23
 
infixr 10 _==>_
24
 
 
25
 
data _==>_ (A B : Set) : Set where
26
 
  uniformCts : (Gauge -> Gauge) -> (A -> B) -> A ==> B
27
 
 
28
 
modulus : {A B : Set} -> (A ==> B) -> Gauge -> Gauge
29
 
modulus (uniformCts μ _) = μ
30
 
 
31
 
forgetUniformCts : {A B : Set} -> (A ==> B) -> A -> B
32
 
forgetUniformCts (uniformCts _ f) = f
33
 
 
34
 
mapC : {A B : Set} -> (A ==> B) -> Complete A -> Complete B
35
 
mapC (uniformCts μ f) x ε = f (x (μ ε))
36
 
 
37
 
bind : {A B : Set} -> (A ==> Complete B) -> Complete A -> Complete B
38
 
bind f x = join $ mapC f x
39
 
 
40
 
mapC2 : {A B C : Set} -> (A ==> B ==> C) -> Complete A -> Complete B -> Complete C
41
 
mapC2 f x y ε = mapC ≈fx y ε2
42
 
  where
43
 
    ε2  = ε / fromNat 2
44
 
    ≈fx = mapC f x ε2
45
 
 
46
 
_○_ : {A B C : Set} -> (B ==> C) -> (A ==> B) -> A ==> C
47
 
f ○ g = uniformCts μ h
48
 
  where
49
 
    μ = modulus f ∘ modulus g
50
 
    h = forgetUniformCts f ∘ forgetUniformCts g
51
 
 
52
 
constCts : {A B : Set} -> A -> B ==> A
53
 
constCts a = uniformCts (const $ fromNat 1) (const a)
54