stop/src/Language/SmallStep.agda at main · runmingl/stop · GitHub

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
open import Prelude

open import Level

{-
  Small-Step Semantics
-}
module Language.SmallStep {ℓ : Level} (monoid : Monoid ℓ) where

open import Language.PCF monoid
open import Language.Substitution monoid

private
  variable
    τ σ : Type

infix 2 _↦_↝_
data _↦_↝_ : · ⊢ τ → · ⊢ τ → Effect → Set ℓ where
  se-suc : {e e' : · ⊢ Nat} {a : Effect} →
      e ↦ e' ↝ a
    ------------------------
    → `suc e ↦ `suc e' ↝ a

  se-case : {e e' : · ⊢ Nat} {e₁ : · ⊢ τ} {e₂ : · # Nat ⊢ τ} {a : Effect} →
      e ↦ e' ↝ a
    ------------------------
    → `case e e₁ e₂ ↦ `case e' e₁ e₂ ↝ a

  se-case-z : {e₁ : · ⊢ τ} {e₂ : · # Nat ⊢ τ} →

    ------------------------
    `case `zero e₁ e₂ ↦ e₁ ↝ 1#

  se-case-s : {v : · ⊢ Nat} {e₁ : · ⊢ τ} {e₂ : · # Nat ⊢ τ} →
      v val
    ------------------------
    → `case (`suc v) e₁ e₂ ↦ e₂ [ v ] ↝ 1#

  se-app : {e₁ e₁' : · ⊢ τ ⇒ σ} {e₂ : · ⊢ τ} {a : Effect} →
      e₁ ↦ e₁' ↝ a
    ------------------------
    → `app e₁ e₂ ↦ `app e₁' e₂ ↝ a

  se-app₁ : {e : · # τ ⇒ σ # τ ⊢ σ} {e₂ e₂' : · ⊢ τ} {a : Effect} →
      e₂ ↦ e₂' ↝ a
    ------------------------
    → `app (`fun e) e₂ ↦ `app (`fun e) e₂' ↝ a

  se-app₂ : {e : · # τ ⇒ σ # τ ⊢ σ} {v : · ⊢ τ} →
      v val
    ------------------------
    → `app (`fun e) v ↦ e [ (`fun e) ][ v ] ↝ 1#

  se-eff : {e : · ⊢ τ} {a : Effect} →

    ------------------------
    `eff a e ↦ e ↝ a

infix 2 _↦*_↝_
data _↦*_↝_ : · ⊢ τ → · ⊢ τ → Effect → Set ℓ where
  ↦*-refl : {e : · ⊢ τ} →

    ------------------------
    e ↦* e ↝ 1#

  ↦*-step : {e e' e'' : · ⊢ τ} {a b : Effect} →
      e ↦ e' ↝ a
    → e' ↦* e'' ↝ b
    ------------------------
    → e ↦* e'' ↝ a ∙ b

↦*-trans : {e e' e'' : · ⊢ τ} {a b : Effect} →
    e ↦* e' ↝ a
  → e' ↦* e'' ↝ b
  ------------------------
  → e ↦* e'' ↝ a ∙ b
↦*-trans {b = b} ↦*-refl step rewrite identityˡ b = step
↦*-trans {b = c} (↦*-step {a = a} {b = b} step₁ step₂) step rewrite assoc a b c =
    ↦*-step step₁ (↦*-trans step₂ step)

compatible : {p : · ⊢ τ → · ⊢ σ}
  → ({e e' : · ⊢ τ} {a : Effect} → e ↦ e' ↝ a → p e ↦ p e' ↝ a)
  → {e e' : · ⊢ τ} {a : Effect} → e ↦* e' ↝ a → p e ↦* p e' ↝ a
compatible alift ↦*-refl       = ↦*-refl
compatible alift (↦*-step x s) = ↦*-step (alift x) (compatible alift s)