← Back to branch summary

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

« back to all changes in this revision

Viewing changes to examples/Termination/comb.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/Termination/comb.agda
1
 
module comb where
2
 
 
3
 
infixr 50 _⟶_
4
 
 
5
 
data Ty : Set where
6
 
  ι : Ty
7
 
  _⟶_ : Ty -> Ty -> Ty
8
 
 
9
 
data Tm : Ty -> Set where
10
 
  K : {σ τ : Ty} -> Tm (σ ⟶ τ ⟶ σ)
11
 
  S : {σ τ ρ : Ty} -> Tm ((σ ⟶ τ ⟶ ρ) ⟶ (σ ⟶ τ) ⟶ σ ⟶ ρ)
12
 
  _$_ : {σ τ : Ty} -> Tm (σ ⟶ τ) -> Tm σ -> Tm τ
13
 
 
14
 
data Nf : Ty -> Set where
15
 
  Kⁿ : {σ τ : Ty} -> Nf (σ ⟶ τ ⟶ σ)
16
 
  Kⁿ¹ : {σ τ : Ty} -> Nf σ -> Nf (τ ⟶ σ)
17
 
  Sⁿ : {σ τ ρ : Ty} -> Nf ((σ ⟶ τ ⟶ ρ) ⟶ (σ ⟶ τ) ⟶ σ ⟶ ρ)
18
 
  Sⁿ¹ : {σ τ ρ : Ty} -> Nf (σ ⟶ τ ⟶ ρ) -> Nf ((σ ⟶ τ) ⟶ σ ⟶ ρ)
19
 
  Sⁿ² : {σ τ ρ : Ty} -> Nf (σ ⟶ τ ⟶ ρ) -> Nf (σ ⟶ τ) -> Nf (σ ⟶ ρ)
20
 
 
21
 
_$$_ : {σ τ : Ty} -> Nf (σ ⟶ τ) -> Nf σ -> Nf τ
22
 
Kⁿ      $$ x = Kⁿ¹ x
23
 
Kⁿ¹ x   $$ y = x
24
 
Sⁿ      $$ x = Sⁿ¹ x
25
 
Sⁿ¹ x   $$ y = Sⁿ² x y
26
 
Sⁿ² x y $$ z = (x $$ z) $$ (y $$ z)
27
 
 
28
 
nf : {σ : Ty} -> Tm σ -> Nf σ
29
 
nf K = Kⁿ
30
 
nf S = Sⁿ
31
 
nf (t $ u) = nf t $$ nf u
32
 
 
33
 
data _$ⁿ_⇓_ : {σ τ : Ty} -> Nf (σ ⟶ τ) -> Nf σ -> Nf τ -> Set where
34
 
  rKⁿ  : {σ τ : Ty} -> {x : Nf σ} -> Kⁿ {σ} {τ} $ⁿ x ⇓ Kⁿ¹ x
35
 
  rKⁿ¹ : {σ τ : Ty} -> {x : Nf σ} -> {y : Nf τ} -> Kⁿ¹ x $ⁿ y ⇓ x
36
 
  rSⁿ  : {σ τ ρ : Ty} -> {x : Nf (σ ⟶ τ ⟶ ρ)} -> Sⁿ $ⁿ x ⇓ Sⁿ¹ x
37
 
  rSⁿ¹ : {σ τ ρ : Ty} -> {x : Nf (σ ⟶ τ ⟶ ρ)} -> {y : Nf (σ ⟶ τ)} ->
38
 
    Sⁿ¹ x $ⁿ y ⇓ Sⁿ² x y
39
 
  rSⁿ² : {σ τ ρ : Ty} -> {x : Nf (σ ⟶ τ ⟶ ρ)} -> {y : Nf (σ ⟶ τ)} ->
40
 
    {z : Nf σ} -> {u : Nf (τ ⟶ ρ)} -> x $ⁿ z ⇓ u -> {v : Nf τ} ->
41
 
    y $ⁿ z ⇓ v -> {w : Nf ρ} -> u $ⁿ v ⇓ w -> Sⁿ² x y $ⁿ z ⇓ w
42
 
 
43
 
data _⇓_ : {σ : Ty} -> Tm σ -> Nf σ -> Set where
44
 
  rK : {σ τ : Ty} -> K {σ} {τ} ⇓ Kⁿ
45
 
  rS : {σ τ ρ : Ty} -> S {σ} {τ} {ρ} ⇓ Sⁿ
46
 
  r$ : {σ τ : Ty} -> {t : Tm (σ ⟶ τ)} -> {f : Nf (σ ⟶ τ)} -> t ⇓ f ->
47
 
    {u : Tm σ} -> {a : Nf σ} -> u ⇓ a -> {v : Nf τ} -> f $ⁿ a ⇓ v  ->
48
 
    t $ u ⇓ v
49
 
 
50
 
data _==_ {A : Set}(a : A) : {B : Set} -> (b : B) -> Set where
51
 
  refl : a == a
52
 
 
53
 
data Σ {A : Set}(B : A -> Set) : Set where
54
 
  sig : (a : A) -> (b : B a) -> Σ B
55
 
 
56
 
σ₀ : {A : Set} -> {B : A -> Set} -> Σ B -> A
57
 
σ₀ (sig x _) = x
58
 
 
59
 
σ₁ : {A : Set} -> {B : A -> Set} -> (s : Σ B) -> B (σ₀ s)
60
 
σ₁ (sig _ y) = y
61
 
 
62
 
 
63
 
_$$⁼_&_ : {σ τ : Ty} -> (f : Nf (σ ⟶ τ)) -> (a : Nf σ) -> {n : Nf τ} ->
64
 
  f $ⁿ a ⇓ n ->     Σ \(n' : Nf τ) -> n' == n
65
 
Kⁿ      $$⁼ x & rKⁿ  = sig (Kⁿ¹ x) refl
66
 
Kⁿ¹ x   $$⁼ y & rKⁿ¹ = sig x refl
67
 
Sⁿ      $$⁼ x & rSⁿ  = sig (Sⁿ¹ x) refl
68
 
Sⁿ¹ x   $$⁼ y & rSⁿ¹ = sig (Sⁿ² x y) refl
69
 
Sⁿ² x y $$⁼ z & (rSⁿ² p q r) with x $$⁼ z & p | y $$⁼ z & q
70
 
Sⁿ² x y $$⁼ z & (rSⁿ² p q r)  |   sig u refl  | sig v refl with u $$⁼ v & r
71
 
Sⁿ² x y $$⁼ z & (rSⁿ² p q r)  |   sig u refl  | sig v refl  |   sig w refl =
72
 
  sig w refl
73
 
 
74
 
nf⁼ : {σ : Ty} -> (t : Tm σ) -> {n : Nf σ} -> t ⇓ n ->
75
 
  Σ \(n' : Nf σ) -> n' == n
76
 
nf⁼ K rK = sig Kⁿ refl
77
 
nf⁼ S rS = sig Sⁿ refl
78
 
nf⁼ (t $ u) (r$ p q r) with nf⁼ t p    | nf⁼ u q
79
 
nf⁼ (t $ u) (r$ p q r)  |   sig f refl | sig a refl with f $$⁼ a & r
80
 
nf⁼ (t $ u) (r$ p q r)  |   sig f refl | sig a refl  |   sig v refl =
81
 
  sig v refl
82
 
 
83
 
proof : {σ : Ty} -> (t : Tm σ) -> Σ \(n : Nf σ) -> t ⇓ n
84
 
proof = {! !}
85
 
 
86
 
nf⇓ :  {σ : Ty} -> Tm σ -> Nf σ
87
 
nf⇓ t = σ₀ (nf⁼ t (σ₁ (proof t)))
88