← Back to branch summary

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

« back to all changes in this revision

Viewing changes to benchmark/monad/MonadPostulates.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:
benchmark/monad/MonadPostulates.agda
1
 
------------------------------------------------------------------------
2
 
------------------------------------------------------------------------
3
 
 
4
 
open import Relation.Binary
5
 
open import Relation.Binary.OrderMorphism
6
 
open import Relation.Binary.PropositionalEquality
7
 
import Relation.Binary.Props.StrictTotalOrder as STOProps
8
 
open import Data.Product
9
 
open import Level
10
 
 
11
 
module MonadPostulates where
12
 
 
13
 
postulate
14
 
  -- Input string positions.
15
 
 
16
 
  Position : Set
17
 
  _<P_ : Rel Position zero
18
 
  posOrdered : IsStrictTotalOrder _≡_ _<P_
19
 
 
20
 
  -- Input strings.
21
 
 
22
 
  Input : Position -> Set
23
 
 
24
 
  -- In order to be able to store results in a memo table (and avoid
25
 
  -- having to lift the table code to Set1) the result types have to
26
 
  -- come from the following universe:
27
 
 
28
 
  Result : Set
29
 
  ⟦_⟧ : Result -> Set
30
 
 
31
 
  -- Memoisation keys. These keys must uniquely identify the
32
 
  -- computation that they are associated with, when paired up with
33
 
  -- the current input string position.
34
 
 
35
 
  Key : let PosPoset = STOProps.poset
36
 
                          (record { Carrier = _ ; _≈_ = _; _<_ = _
37
 
                                  ; isStrictTotalOrder = posOrdered })
38
 
            MonoFun = PosPoset ⇒-Poset PosPoset in
39
 
         MonoFun -> Result -> Set
40
 
  _≈'_ _<_ : Rel (∃₂ Key) zero
41
 
  keyOrdered : IsStrictTotalOrder _≈'_ _<_
42
 
 
43
 
  -- Furthermore the underlying equality needs to be strong enough.
44
 
 
45
 
  funsEqual    : _≈'_ =[ proj₁ ]⇒ _≡_
46
 
  resultsEqual : _≈'_ =[ (\rfk -> proj₁ (proj₂ rfk)) ]⇒ _≡_
47
 
 
48
 
 
49
 
open _⇒-Poset_
50
 
open STOProps (record { Carrier = _ ; _≈_ = _; _<_ = _
51
 
                      ; isStrictTotalOrder = posOrdered })
52
 
 
53
 
import IndexedMap as Map -- renaming (Map to MemoTable)
54
 
open import Category.Monad
55
 
open import Category.Monad.State
56
 
import Data.List as List; open List using (List)
57
 
open import Data.Unit hiding (poset; _≤_)
58
 
open import Function
59
 
open import Data.Maybe hiding (Eq)
60
 
open import Relation.Binary.Product.StrictLex
61
 
open import Relation.Binary.Product.Pointwise
62
 
import Relation.Binary.On as On
63
 
 
64
 
------------------------------------------------------------------------
65
 
 
66
 
MonoFun : Set
67
 
MonoFun = poset ⇒-Poset poset
68
 
 
69
 
------------------------------------------------------------------------
70
 
 
71
 
 
72
 
Index : Set
73
 
Index = Position × MonoFun × Result
74
 
 
75
 
data MemoTableKey : Index -> Set where
76
 
  key : forall {f r} (key : Key f r) pos -> MemoTableKey (pos , f , r)
77
 
 
78
 
 
79
 
Input≤ : Position -> Set
80
 
Input≤ pos = ∃ \pos′ -> pos′ ≤ pos × Input pos′
81
 
 
82
 
 
83
 
Value : Index -> Set
84
 
Value (pos , f , r) = List (⟦ r ⟧ × Input≤ (fun f pos))
85
 
 
86
 
 
87
 
shuffle : ∃ MemoTableKey -> Position × ∃₂ Key
88
 
shuffle ((pos , f , r) , key k .pos) = (pos , f , r , k)
89
 
 
90
 
 
91
 
Eq : Rel (∃ MemoTableKey) _
92
 
Eq = _≡_ ×-Rel _≈'_  on  shuffle
93
 
 
94
 
Lt : Rel (∃ MemoTableKey) _
95
 
Lt = ×-Lex _≡_ _<P_ _<_  on  shuffle
96
 
 
97
 
isOrdered : IsStrictTotalOrder Eq Lt
98
 
isOrdered = On.isStrictTotalOrder shuffle
99
 
              (posOrdered ×-isStrictTotalOrder keyOrdered)
100
 
 
101
 
indicesEqual′ : Eq =[ proj₁ ]⇒ _≡_
102
 
indicesEqual′ {((_ , _ , _) , key _ ._)}
103
 
              {((_ , _ , _) , key _ ._)} (eq₁ , eq₂) =
104
 
  cong₂ _,_ eq₁ (cong₂ _,_ (funsEqual eq₂) (resultsEqual eq₂))
105
 
 
106
 
open Map isOrdered (\{k₁} {k₂} -> indicesEqual′ {k₁} {k₂}) Value
107
 
 
108
 
{-
109
 
------------------------------------------------------------------------
110
 
 
111
 
 
112
 
 
113
 
module MemoState = RawMonadState (StateMonadState MemoTable)
114
 
 
115
 
 
116
 
module List = RawMonadPlus List.ListMonadPlus
117
 
 
118
 
 
119
 
module IM where
120
 
 
121
 
  Inner : Set -> Set
122
 
  Inner R = State MemoTable (List R)
123
 
 
124
 
  InnerMonadPlus : RawMonadPlus Inner
125
 
  InnerMonadPlus = record
126
 
    { monadZero = record
127
 
      { monad = record
128
 
        { return = \x -> return (List.return x)
129
 
        ; _>>=_  = \m f -> List.concat <$> (List.mapM monad f =<< m)
130
 
        }
131
 
      ; ∅ = return List.∅
132
 
      }
133
 
    ; _∣_ = \m₁ m₂ -> List._∣_ <$> m₁ ⊛ m₂
134
 
    }
135
 
    where
136
 
    open MemoState
137
 
 
138
 
  InnerMonadState : RawMonadState MemoTable Inner
139
 
  InnerMonadState = record
140
 
    { monad = RawMonadPlus.monad InnerMonadPlus
141
 
    ; get   = List.return <$> get
142
 
    ; put   = \s -> List.return <$> put s
143
 
    }
144
 
    where open MemoState
145
 
 
146
 
  open RawMonadPlus  InnerMonadPlus  public
147
 
  open RawMonadState InnerMonadState public
148
 
    using (get; put; modify)
149
 
 
150
 
 
151
 
module PM where
152
 
 
153
 
  P : MonoFun -> Set -> Set
154
 
  P f A = forall {n} -> Input n -> IM.Inner (A × Input≤ (fun f n))
155
 
 
156
 
  -- Memoises the computation, assuming that the key is sufficiently
157
 
  -- unique.
158
 
 
159
 
  memoise : forall {f r} -> Key f r -> P f ⟦ r ⟧ -> P f ⟦ r ⟧
160
 
  memoise k p {pos} xs =
161
 
    let open IM in helper =<< lookup k′ <$> get
162
 
    where
163
 
    i = (pos , _)
164
 
 
165
 
    k′ : MemoTableKey i
166
 
    k′ = key k pos
167
 
 
168
 
    helper : Maybe (Value i) -> State MemoTable (Value i)
169
 
    helper (just ris) = return ris  where open MemoState
170
 
    helper nothing    = p xs                   >>= \ris ->
171
 
                        modify (insert k′ ris) >>
172
 
                        return ris
173
 
      where open MemoState
174
 
 
175
 
  -- Other monadic operations.
176
 
 
177
 
  return : forall {A} -> A -> P idM A
178
 
  return a = \xs -> IM.return (a , _ , refl , xs)
179
 
 
180
 
  _>>=_ : forall {A B f g} -> P f A -> (A -> P g B) -> P (g ∘M f) B
181
 
  _>>=_ {g = g} m₁ m₂ xs =
182
 
    m₁ xs ⟨ IM._>>=_ ⟩ \ays ->
183
 
    let a  = proj₁ ays
184
 
        le = proj₁ $ proj₂ $ proj₂ ays
185
 
        ys = proj₂ $ proj₂ $ proj₂ ays in
186
 
    fix le ⟨ IM._<$>_ ⟩ m₂ a ys
187
 
    where
188
 
    lemma : forall {i j k} -> j ≤ k -> i ≤ fun g j -> i ≤ fun g k
189
 
    lemma j≤k i≤gj = trans i≤gj (monotone g j≤k)
190
 
 
191
 
    fix : forall {A i j} -> i ≤ j ->
192
 
          A × Input≤ (fun g i) ->
193
 
          A × Input≤ (fun g j)
194
 
    fix le = map-× id (map-Σ id (map-× (lemma le) id))
195
 
 
196
 
  ∅ : forall {A} -> P idM A
197
 
  ∅ = const IM.∅
198
 
 
199
 
  _∣_ : forall {A f} -> P f A -> P f A -> P f A
200
 
  m₁ ∣ m₂ = \xs -> IM._∣_ (m₁ xs) (m₂ xs)
201
 
 
202
 
  put : forall {n} -> Input n -> P (constM n) ⊤
203
 
  put xs = \_ -> IM.return (_ , _ , refl , xs)
204
 
 
205
 
  modify : forall {A f} ->
206
 
           (forall {n} -> Input n -> A × Input (fun f n)) ->
207
 
           P f A
208
 
  modify g xs = IM.return (proj₁ gxs , _ , refl , proj₂ gxs)
209
 
    where gxs = g xs
210
 
-}