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
130
|
{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
{-# 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
|
