-
Notifications
You must be signed in to change notification settings - Fork 4
/
Step.agda
87 lines (63 loc) · 2.37 KB
/
Step.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
{-# OPTIONS --rewriting #-}
-- Step effect.
open import Algebra.Cost
module Calf.Step (costMonoid : CostMonoid) where
open CostMonoid costMonoid
open import Calf.Prelude
open import Calf.CBPV
open import Calf.Directed
open import Calf.Phase.Core
open import Calf.Phase.Open
open import Relation.Binary.Core using (_⇒_)
open import Relation.Binary.PropositionalEquality
variable
c c' c₁ c₂ : ℂ
ℂ⁺ : tp⁺
ℂ⁺ = meta⁺ ℂ
postulate
step : (X : tp⁻) → ℂ → cmp X → cmp X
step/0 : {e : cmp X} →
step X zero e ≡ e
step/+ : {e : cmp X} →
step X c₁ (step X c₂ e) ≡ step X (c₁ + c₂) e
{-# REWRITE step/0 step/+ #-}
step/ext : (X : tp⁻) (e : cmp X) (c : ℂ) (u : ext) → step X c e ≡ e
-- sadly the above cannot be made an Agda rewrite rule
postulate
bind/step : {e : cmp (F A)} {f : val A → cmp X} →
bind X (step (F A) c e) f ≡ step X c (bind X e f)
{-# REWRITE bind/step #-}
Π/step : {X : val A → tp⁻} {f : cmp (Π A X)} →
step (Π A X) c f ≡ λ a → step (X a) c (f a)
{-# REWRITE Π/step #-}
prod⁻/step : {e : cmp (prod⁻ X Y)} →
step (prod⁻ X Y) c e ≡ (step X c (proj₁ e) , step Y c (proj₂ e))
{-# REWRITE prod⁻/step #-}
unit⁻/step : {e : cmp unit⁻} →
step unit⁻ c e ≡ triv
{-# REWRITE unit⁻/step #-}
Σ⁻/step : {X : val A → tp⁻} {e : cmp (Σ⁻ A X)} →
step (Σ⁻ A X) c e ≡ (proj₁ e , step (X (proj₁ e)) c (proj₂ e))
{-# REWRITE Σ⁻/step #-}
open⁻/step : {X : ext → tp⁻} {e : cmp (open⁻ X)} →
step (open⁻ X) c e ≡ λ u → step (X u) c (e u)
{-# REWRITE open⁻/step #-}
postulate
≤⇒≤⁺ : _≤_ ⇒ _≤⁺_ {ℂ⁺}
step-monoˡ-≤⁻ : (e : cmp X) →
c ≤ c' → step X c e ≤⁻[ X ] step X c' e
step-monoˡ-≤⁻ {X} e c≤c' = ≤⁺-mono (λ c → step X c e) (≤⇒≤⁺ c≤c')
step-monoʳ-≤⁻ : (c : ℂ) {e e' : cmp X} →
_≤⁻_ {X} e e' → _≤⁻_ {X} (step X c e) (step X c e')
step-monoʳ-≤⁻ {X} c = ≤⁻-mono (step X c)
step-mono-≤⁻ : {e e' : cmp X} →
c ≤ c' → e ≤⁻[ X ] e' → step X c e ≤⁻[ X ] step X c' e'
step-mono-≤⁻ {X} {c} {c'} {e} {e'} c≤c' e≤e' =
let open ≤⁻-Reasoning X in
begin
step X c e
≲⟨ step-monoˡ-≤⁻ e c≤c' ⟩
step X c' e
≲⟨ step-monoʳ-≤⁻ c' e≤e' ⟩
step X c' e'
∎