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
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
{-# LANGUAGE UnicodeSyntax #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
module T5329 where
data PZero
data PSucc p
data Peano n where
PZero ∷ Peano PZero
PSucc ∷ IsPeano p ⇒ Peano p → Peano (PSucc p)
class IsPeano n where
peano ∷ Peano n
instance IsPeano PZero where
peano = PZero
instance IsPeano p ⇒ IsPeano (PSucc p) where
peano = PSucc peano
class (n ~ PSucc (PPred n)) ⇒ PHasPred n where
type PPred n
instance PHasPred (PSucc p) where
type PPred (PSucc p) = p
pPred ∷ Peano (PSucc p) → Peano p
pPred (PSucc p) = p
infixl 6 :+:
class (IsPeano n, IsPeano m, IsPeano (n :+: m), (n :+: m) ~ (m :+: n))
⇒ PAdd n m where
type n :+: m
instance PAdd PZero PZero where
type PZero :+: PZero = PZero
instance IsPeano p ⇒ PAdd PZero (PSucc p) where
type PZero :+: (PSucc p) = PSucc p
instance IsPeano p ⇒ PAdd (PSucc p) PZero where
type (PSucc p) :+: PZero = PSucc p
instance (IsPeano n, IsPeano m, PAdd n m) ⇒ PAdd (PSucc n) (PSucc m) where
type (PSucc n) :+: (PSucc m) = PSucc (PSucc (n :+: m))
data PAddResult n m r where
PAddResult ∷ (PAdd n m, PAdd m n, (n :+: m) ~ r)
⇒ PAddResult n m r
pAddLeftZero ∷ ∀ n . IsPeano n ⇒ PAddResult PZero n n
pAddLeftZero = case peano ∷ Peano n of
PZero → PAddResult
PSucc _ → PAddResult
pAddRightZero ∷ ∀ n . IsPeano n ⇒ PAddResult n PZero n
pAddRightZero = case peano ∷ Peano n of
PZero → PAddResult
PSucc _ → PAddResult
data PAddSucc n m where
PAddSucc ∷ (PAdd n m, PAdd m n,
PAdd (PSucc n) m, PAdd m (PSucc n),
PAdd n (PSucc m), PAdd (PSucc m) n,
(PSucc n :+: m) ~ PSucc (n :+: m),
(n :+: PSucc m) ~ PSucc (n :+: m))
⇒ PAddSucc n m
pAddSucc ∷ ∀ n m . (IsPeano n, IsPeano m) ⇒ PAddSucc n m
pAddSucc = case (peano ∷ Peano n, peano ∷ Peano m) of
(PZero, PZero) → PAddSucc
(PZero, PSucc _) → case pAddLeftZero ∷ PAddResult n (PPred m) (PPred m) of
PAddResult → PAddSucc
(PSucc _, PZero) → case pAddRightZero ∷ PAddResult (PPred n) m (PPred n) of
PAddResult → PAddSucc
(PSucc _, PSucc _) → case pAddSucc ∷ PAddSucc (PPred n) (PPred m) of
PAddSucc → PAddSucc
data PAdd2 n m where
PAdd2 ∷ (PAdd n m, PAdd m n) ⇒ PAdd2 n m
pAdd2 ∷ ∀ n m . (IsPeano n, IsPeano m) ⇒ PAdd2 n m
pAdd2 = case (peano ∷ Peano n, peano ∷ Peano m) of
(PZero, PZero) → PAdd2
(PZero, PSucc _) → PAdd2
(PSucc _, PZero) → PAdd2
(PSucc _, PSucc _) → case pAdd2 ∷ PAdd2 (PPred n) (PPred m) of
PAdd2 → PAdd2
data PAdd3 n m k where
PAdd3 ∷ (PAdd n m, PAdd m k, PAdd m n, PAdd k m, PAdd n k, PAdd k n,
PAdd (n :+: m) k, PAdd k (m :+: n),
PAdd n (m :+: k), PAdd (m :+: k) n,
PAdd (n :+: k) m, PAdd m (n :+: k),
((n :+: m) :+: k) ~ (n :+: (m :+: k)),
(m :+: (n :+: k)) ~ ((m :+: n) :+: k))
⇒ PAdd3 n m k
pAdd3 ∷ ∀ n m k . (IsPeano n, IsPeano m, IsPeano k) ⇒ PAdd3 n m k
pAdd3 = case (peano ∷ Peano n, peano ∷ Peano m, peano ∷ Peano k) of
(PZero, PZero, PZero) → PAdd3
(PZero, PZero, PSucc _) → PAdd3
(PZero, PSucc _, PZero) → PAdd3
(PSucc _, PZero, PZero) → PAdd3
(PZero, PSucc _, PSucc _) →
case pAdd2 ∷ PAdd2 (PPred m) (PPred k) of
PAdd2 → PAdd3
(PSucc _, PZero, PSucc _) →
case pAdd2 ∷ PAdd2 (PPred n) (PPred k) of
PAdd2 → PAdd3
(PSucc _, PSucc _, PZero) →
case pAdd2 ∷ PAdd2 (PPred n) (PPred m) of
PAdd2 → PAdd3
(PSucc _, PSucc _, PSucc _) →
case pAdd3 ∷ PAdd3 (PPred n) (PPred m) (PPred k) of
PAdd3 → case pAddSucc ∷ PAddSucc (PPred n :+: PPred m) (PPred k) of
PAddSucc → case pAddSucc ∷ PAddSucc (PPred n :+: PPred k) (PPred m) of
PAddSucc → case pAddSucc ∷ PAddSucc (PPred m :+: PPred k) (PPred n) of
PAddSucc → PAdd3
|
