
   0 | module TyRE.Codes
   1 | 
   2 | import Data.SnocList
   3 | 
   4 | %default total
   5 | 
   6 | public export
   7 | data Code =
   8 |     CharC
   9 |     | PairC Code Code
  10 |     | StringC
  11 |     | UnitC
  12 |     | EitherC Code Code
  13 |     | ListC Code
  14 |     | MaybeC Code
  15 |     | BoolC
  16 |     | NatC
  17 |     | IgnoreC
  18 | 
  19 | Eq Code where
  20 |     CharC == CharC                  = True
  21 |     (PairC x z) == (PairC y v)      = (x == y) && (z == v)
  22 |     StringC == StringC              = True
  23 |     UnitC == UnitC                  = True
  24 |     IgnoreC == IgnoreC              = True
  25 |     BoolC == BoolC                  = True
  26 |     (EitherC x z) == (EitherC y v)  = ((x == y) && (z == v))
  27 |     (ListC x) == (ListC y)          = x == y
  28 |     (MaybeC x) == (MaybeC y)        = x == y
  29 |     NatC == NatC                    = True
  30 |     _ == _                          = False
  31 | 
  32 | public export
  33 | Sem : Code -> Type
  34 | Sem CharC         = Char
  35 | Sem (PairC x y)   = (Sem x, Sem y)
  36 | Sem StringC       = String
  37 | Sem UnitC         = ()
  38 | Sem (EitherC x y) = Either (Sem x) (Sem y)
  39 | Sem (ListC x)     = SnocList (Sem x)
  40 | Sem (MaybeC x)    = Maybe (Sem x)
  41 | Sem BoolC         = Bool
  42 | Sem NatC          = Nat
  43 | Sem IgnoreC       = ()
  44 | 
  45 | public export
  46 | SimplifyCode : Code -> Code
  47 | 
  48 | SimplifyCode (ListC x) =
  49 |   case (SimplifyCode x) of
  50 |     IgnoreC => IgnoreC
  51 |     UnitC => NatC
  52 |     e => ListC e
  53 | 
  54 | SimplifyCode (MaybeC x) =
  55 |   let sx = SimplifyCode x
  56 |   in case sx of
  57 |     IgnoreC => IgnoreC
  58 |     UnitC => BoolC
  59 |     (MaybeC y) => sx
  60 |     e => MaybeC sx
  61 | 
  62 | SimplifyCode (PairC x y) =
  63 |   let sx : Code = SimplifyCode x
  64 |       sy : Code = SimplifyCode y
  65 |   in case (sx, sy) of
  66 |     (IgnoreC, x) => x
  67 |     (x, IgnoreC) => x
  68 |     (UnitC, x) => x
  69 |     (x, UnitC) => x
  70 |     _ => PairC sx sy
  71 | 
  72 | SimplifyCode (EitherC x y) =
  73 |   let sx : Code = SimplifyCode x
  74 |       sy : Code = SimplifyCode y
  75 |   in case (sx, sy) of
  76 |     (IgnoreC, UnitC) => BoolC
  77 |     (UnitC, IgnoreC) => BoolC
  78 |     (IgnoreC, IgnoreC) => IgnoreC
  79 |     (IgnoreC, y) => MaybeC y
  80 |     (x, IgnoreC) => MaybeC x
  81 |     (UnitC, UnitC) => BoolC
  82 |     (UnitC, y) => MaybeC y
  83 |     (x, UnitC) => MaybeC x
  84 |     (x,y) => EitherC x y
  85 | 
  86 | SimplifyCode code = code
  87 | 
  88 | public export
  89 | ConvertSimplification : (c : Code) -> Sem c -> Sem (SimplifyCode c)
  90 | ConvertSimplification CharC m   = m
  91 | ConvertSimplification StringC m = m
  92 | ConvertSimplification BoolC m   = m
  93 | ConvertSimplification NatC m    = m
  94 | ConvertSimplification UnitC _   = ()
  95 | ConvertSimplification IgnoreC _   = ()
  96 | 
  97 | ConvertSimplification (MaybeC x) Nothing with (SimplifyCode x)
  98 |   ConvertSimplification (MaybeC x) Nothing | CharC          = Nothing
  99 |   ConvertSimplification (MaybeC x) Nothing | (PairC y z)    = Nothing
 100 |   ConvertSimplification (MaybeC x) Nothing | StringC        = Nothing
 101 |   ConvertSimplification (MaybeC x) Nothing | UnitC          = False
 102 |   ConvertSimplification (MaybeC x) Nothing | (EitherC y z)  = Nothing
 103 |   ConvertSimplification (MaybeC x) Nothing | (ListC y)      = Nothing
 104 |   ConvertSimplification (MaybeC x) Nothing | (MaybeC y)     = Nothing
 105 |   ConvertSimplification (MaybeC x) Nothing | NatC           = Nothing
 106 |   ConvertSimplification (MaybeC x) Nothing | BoolC          = Nothing
 107 |   ConvertSimplification (MaybeC x) Nothing | IgnoreC        = ()
 108 | --
 109 | ConvertSimplification (MaybeC x) (Just y) with (ConvertSimplification x y)
 110 |   ConvertSimplification (MaybeC x) (Just y) | cs with (SimplifyCode x)
 111 |     ConvertSimplification (MaybeC x) (Just y) | cs | UnitC          = True
 112 |     ConvertSimplification (MaybeC x) (Just y) | cs | (MaybeC z)     = cs
 113 |     ConvertSimplification (MaybeC x) (Just y) | cs | CharC          = Just cs
 114 |     ConvertSimplification (MaybeC x) (Just y) | cs | (PairC z w)    = Just cs
 115 |     ConvertSimplification (MaybeC x) (Just y) | cs | StringC        = Just cs
 116 |     ConvertSimplification (MaybeC x) (Just y) | cs | (EitherC z w)  = Just cs
 117 |     ConvertSimplification (MaybeC x) (Just y) | cs | (ListC z)      = Just cs
 118 |     ConvertSimplification (MaybeC x) (Just y) | cs | NatC           = Just cs
 119 |     ConvertSimplification (MaybeC x) (Just y) | cs | BoolC          = Just cs
 120 |     ConvertSimplification (MaybeC x) (Just y) | cs | IgnoreC        = ()
 121 | 
 122 | ConvertSimplification (ListC x) m with (ConvertSimplification x `map` m)
 123 |   ConvertSimplification (ListC x) m | cs with (SimplifyCode x)
 124 |     ConvertSimplification (ListC x) m | cs | CharC          = cs
 125 |     ConvertSimplification (ListC x) m | cs | (PairC y z)    = cs
 126 |     ConvertSimplification (ListC x) m | cs | StringC        = cs
 127 |     ConvertSimplification (ListC x) m | cs | UnitC          = length cs
 128 |     ConvertSimplification (ListC x) m | cs | (EitherC y z)  = cs
 129 |     ConvertSimplification (ListC x) m | cs | (ListC y)      = cs
 130 |     ConvertSimplification (ListC x) m | cs | (MaybeC y)     = cs
 131 |     ConvertSimplification (ListC x) m | cs | BoolC          = cs
 132 |     ConvertSimplification (ListC x) m | cs | NatC           = cs
 133 |     ConvertSimplification (ListC x) m | cs | IgnoreC        = ()
 134 | 
 135 | ConvertSimplification (PairC x y) m with (ConvertSimplification x $ fst m, ConvertSimplification y $ snd m)
 136 |   ConvertSimplification (PairC x y) m | (csx, csy) with (SimplifyCode x)
 137 |     ConvertSimplification (PairC x y) m | (csx, csy) | sx with (SimplifyCode y)
 138 |       ConvertSimplification (PairC x y) m | (csx, csy) | CharC          | CharC         = (csx, csx)
 139 |       ConvertSimplification (PairC x y) m | (csx, csy) | CharC          | (PairC z w)   = (csx, csy)
 140 |       ConvertSimplification (PairC x y) m | (csx, csy) | CharC          | StringC       = (csx, csy)
 141 |       ConvertSimplification (PairC x y) m | (csx, csy) | CharC          | UnitC         = csx
 142 |       ConvertSimplification (PairC x y) m | (csx, csy) | CharC          | (EitherC z w) = (csx, csy)
 143 |       ConvertSimplification (PairC x y) m | (csx, csy) | CharC          | (ListC z)     = (csx, csy)
 144 |       ConvertSimplification (PairC x y) m | (csx, csy) | CharC          | (MaybeC z)    = (csx, csy)
 145 |       ConvertSimplification (PairC x y) m | (csx, csy) | CharC          | BoolC         = (csx, csy)
 146 |       ConvertSimplification (PairC x y) m | (csx, csy) | CharC          | NatC          = (csx, csy)
 147 |       ConvertSimplification (PairC x y) m | (csx, csy) | CharC          | IgnoreC       = csx
 148 | 
 149 |       ConvertSimplification (PairC x y) m | (csx, csy) | (PairC _ _)    | CharC         = (csx, csy)
 150 |       ConvertSimplification (PairC x y) m | (csx, csy) | (PairC _ _)    | (PairC v s)   = (csx, csy)
 151 |       ConvertSimplification (PairC x y) m | (csx, csy) | (PairC _ _)    | StringC       = (csx, csy)
 152 |       ConvertSimplification (PairC x y) m | (csx, csy) | (PairC _ _)    | UnitC         = csx
 153 |       ConvertSimplification (PairC x y) m | (csx, csy) | (PairC _ _)    | (EitherC v s) = (csx, csy)
 154 |       ConvertSimplification (PairC x y) m | (csx, csy) | (PairC _ _)    | (ListC v)     = (csx, csy)
 155 |       ConvertSimplification (PairC x y) m | (csx, csy) | (PairC _ _)    | (MaybeC v)    = (csx, csy)
 156 |       ConvertSimplification (PairC x y) m | (csx, csy) | (PairC _ _)    | BoolC         = (csx, csy)
 157 |       ConvertSimplification (PairC x y) m | (csx, csy) | (PairC _ _)    | NatC          = (csx, csy)
 158 |       ConvertSimplification (PairC x y) m | (csx, csy) | (PairC _ _)    | IgnoreC       = csx
 159 | 
 160 |       ConvertSimplification (PairC x y) m | (csx, csy) | StringC        | CharC         = (csx, csy)
 161 |       ConvertSimplification (PairC x y) m | (csx, csy) | StringC        | (PairC z w)   = (csx, csy)
 162 |       ConvertSimplification (PairC x y) m | (csx, csy) | StringC        | StringC       = (csx, csx)
 163 |       ConvertSimplification (PairC x y) m | (csx, csy) | StringC        | UnitC         = csx
 164 |       ConvertSimplification (PairC x y) m | (csx, csy) | StringC        | (EitherC z w) = (csx, csy)
 165 |       ConvertSimplification (PairC x y) m | (csx, csy) | StringC        | (ListC z)     = (csx, csy)
 166 |       ConvertSimplification (PairC x y) m | (csx, csy) | StringC        | (MaybeC z)    = (csx, csy)
 167 |       ConvertSimplification (PairC x y) m | (csx, csy) | StringC        | BoolC         = (csx, csy)
 168 |       ConvertSimplification (PairC x y) m | (csx, csy) | StringC        | NatC          = (csx, csy)
 169 |       ConvertSimplification (PairC x y) m | (csx, csy) | StringC        | IgnoreC       = csx
 170 | 
 171 |       ConvertSimplification (PairC x y) m | (csx, csy) | UnitC          | CharC         = csy
 172 |       ConvertSimplification (PairC x y) m | (csx, csy) | UnitC          | (PairC z w)   = csy
 173 |       ConvertSimplification (PairC x y) m | (csx, csy) | UnitC          | StringC       = csy
 174 |       ConvertSimplification (PairC x y) m | (csx, csy) | UnitC          | UnitC         = ()
 175 |       ConvertSimplification (PairC x y) m | (csx, csy) | UnitC          | (EitherC z w) = csy
 176 |       ConvertSimplification (PairC x y) m | (csx, csy) | UnitC          | (ListC z)     = csy
 177 |       ConvertSimplification (PairC x y) m | (csx, csy) | UnitC          | (MaybeC z)    = csy
 178 |       ConvertSimplification (PairC x y) m | (csx, csy) | UnitC          | BoolC         = csy
 179 |       ConvertSimplification (PairC x y) m | (csx, csy) | UnitC          | NatC          = csy
 180 |       ConvertSimplification (PairC x y) m | (csx, csy) | UnitC          | IgnoreC       = ()
 181 | 
 182 |       ConvertSimplification (PairC x y) m | (csx, csy) | (EitherC _ _)  | CharC         = (csx, csy)
 183 |       ConvertSimplification (PairC x y) m | (csx, csy) | (EitherC _ _)  | (PairC z w)   = (csx, csy)
 184 |       ConvertSimplification (PairC x y) m | (csx, csy) | (EitherC _ _)  | StringC       = (csx, csy)
 185 |       ConvertSimplification (PairC x y) m | (csx, csy) | (EitherC _ _)  | UnitC         = csx
 186 |       ConvertSimplification (PairC x y) m | (csx, csy) | (EitherC _ _)  | (EitherC z w) = (csx, csy)
 187 |       ConvertSimplification (PairC x y) m | (csx, csy) | (EitherC _ _)  | (ListC z)     = (csx, csy)
 188 |       ConvertSimplification (PairC x y) m | (csx, csy) | (EitherC _ _)  | (MaybeC z)    = (csx, csy)
 189 |       ConvertSimplification (PairC x y) m | (csx, csy) | (EitherC _ _)  | BoolC         = (csx, csy)
 190 |       ConvertSimplification (PairC x y) m | (csx, csy) | (EitherC _ _)  | NatC          = (csx, csy)
 191 |       ConvertSimplification (PairC x y) m | (csx, csy) | (EitherC _ _)  | IgnoreC       = csx
 192 | 
 193 |       ConvertSimplification (PairC x y) m | (csx, csy) | (ListC _)      | CharC         = (csx, csy)
 194 |       ConvertSimplification (PairC x y) m | (csx, csy) | (ListC _)      | (PairC z w)   = (csx, csy)
 195 |       ConvertSimplification (PairC x y) m | (csx, csy) | (ListC _)      | StringC       = (csx, csy)
 196 |       ConvertSimplification (PairC x y) m | (csx, csy) | (ListC _)      | UnitC         = csx
 197 |       ConvertSimplification (PairC x y) m | (csx, csy) | (ListC _)      | (EitherC z w) = (csx, csy)
 198 |       ConvertSimplification (PairC x y) m | (csx, csy) | (ListC _)      | (ListC z)     = (csx, csy)
 199 |       ConvertSimplification (PairC x y) m | (csx, csy) | (ListC _)      | (MaybeC z)    = (csx, csy)
 200 |       ConvertSimplification (PairC x y) m | (csx, csy) | (ListC _)      | BoolC         = (csx, csy)
 201 |       ConvertSimplification (PairC x y) m | (csx, csy) | (ListC _)      | NatC          = (csx, csy)
 202 |       ConvertSimplification (PairC x y) m | (csx, csy) | (ListC _)      | IgnoreC       = csx
 203 | 
 204 |       ConvertSimplification (PairC x y) m | (csx, csy) | (MaybeC _)     | CharC         = (csx, csy)
 205 |       ConvertSimplification (PairC x y) m | (csx, csy) | (MaybeC _)     | (PairC z w)   = (csx, csy)
 206 |       ConvertSimplification (PairC x y) m | (csx, csy) | (MaybeC _)     | StringC       = (csx, csy)
 207 |       ConvertSimplification (PairC x y) m | (csx, csy) | (MaybeC _)     | UnitC         = csx
 208 |       ConvertSimplification (PairC x y) m | (csx, csy) | (MaybeC _)     | (EitherC z w) = (csx, csy)
 209 |       ConvertSimplification (PairC x y) m | (csx, csy) | (MaybeC _)     | (ListC z)     = (csx, csy)
 210 |       ConvertSimplification (PairC x y) m | (csx, csy) | (MaybeC _)     | (MaybeC z)    = (csx, csy)
 211 |       ConvertSimplification (PairC x y) m | (csx, csy) | (MaybeC _)     | BoolC         = (csx, csy)
 212 |       ConvertSimplification (PairC x y) m | (csx, csy) | (MaybeC _)     | NatC          = (csx, csy)
 213 |       ConvertSimplification (PairC x y) m | (csx, csy) | (MaybeC _)     | IgnoreC       = csx
 214 | 
 215 |       ConvertSimplification (PairC x y) m | (csx, csy) | BoolC          | CharC         = (csx, csy)
 216 |       ConvertSimplification (PairC x y) m | (csx, csy) | BoolC          | (PairC z w)   = (csx, csy)
 217 |       ConvertSimplification (PairC x y) m | (csx, csy) | BoolC          | StringC       = (csx, csy)
 218 |       ConvertSimplification (PairC x y) m | (csx, csy) | BoolC          | UnitC         = csx
 219 |       ConvertSimplification (PairC x y) m | (csx, csy) | BoolC          | (EitherC z w) = (csx, csy)
 220 |       ConvertSimplification (PairC x y) m | (csx, csy) | BoolC          | (ListC z)     = (csx, csy)
 221 |       ConvertSimplification (PairC x y) m | (csx, csy) | BoolC          | (MaybeC z)    = (csx, csy)
 222 |       ConvertSimplification (PairC x y) m | (csx, csy) | BoolC          | BoolC         = (csx, csy)
 223 |       ConvertSimplification (PairC x y) m | (csx, csy) | BoolC          | NatC          = (csx, csy)
 224 |       ConvertSimplification (PairC x y) m | (csx, csy) | BoolC          | IgnoreC       = csx
 225 | 
 226 |       ConvertSimplification (PairC x y) m | (csx, csy) | NatC          | CharC         = (csx, csy)
 227 |       ConvertSimplification (PairC x y) m | (csx, csy) | NatC          | (PairC z w)   = (csx, csy)
 228 |       ConvertSimplification (PairC x y) m | (csx, csy) | NatC          | StringC       = (csx, csy)
 229 |       ConvertSimplification (PairC x y) m | (csx, csy) | NatC          | UnitC         = csx
 230 |       ConvertSimplification (PairC x y) m | (csx, csy) | NatC          | (EitherC z w) = (csx, csy)
 231 |       ConvertSimplification (PairC x y) m | (csx, csy) | NatC          | (ListC z)     = (csx, csy)
 232 |       ConvertSimplification (PairC x y) m | (csx, csy) | NatC          | (MaybeC z)    = (csx, csy)
 233 |       ConvertSimplification (PairC x y) m | (csx, csy) | NatC          | BoolC         = (csx, csy)
 234 |       ConvertSimplification (PairC x y) m | (csx, csy) | NatC          | NatC          = (csx, csy)
 235 |       ConvertSimplification (PairC x y) m | (csx, csy) | NatC          | IgnoreC       = csx
 236 | 
 237 |       ConvertSimplification (PairC x y) m | (csx, csy) | IgnoreC       | CharC         = csy
 238 |       ConvertSimplification (PairC x y) m | (csx, csy) | IgnoreC       | (PairC z w)   = csy
 239 |       ConvertSimplification (PairC x y) m | (csx, csy) | IgnoreC       | StringC       = csy
 240 |       ConvertSimplification (PairC x y) m | (csx, csy) | IgnoreC       | UnitC         = ()
 241 |       ConvertSimplification (PairC x y) m | (csx, csy) | IgnoreC       | (EitherC z w) = csy
 242 |       ConvertSimplification (PairC x y) m | (csx, csy) | IgnoreC       | (ListC z)     = csy
 243 |       ConvertSimplification (PairC x y) m | (csx, csy) | IgnoreC       | (MaybeC z)    = csy
 244 |       ConvertSimplification (PairC x y) m | (csx, csy) | IgnoreC       | BoolC         = csy
 245 |       ConvertSimplification (PairC x y) m | (csx, csy) | IgnoreC       | NatC          = csy
 246 |       ConvertSimplification (PairC x y) m | (csx, csy) | IgnoreC       | IgnoreC       = ()
 247 | 
 248 | ConvertSimplification (EitherC x y) (Left m) with (ConvertSimplification x m)
 249 |   ConvertSimplification (EitherC x y) (Left m) | cs with (SimplifyCode x)
 250 |     ConvertSimplification (EitherC x y) (Left m) | cs | sx with (SimplifyCode y)
 251 | 
 252 |       ConvertSimplification (EitherC x y) (Left m) | cs | CharC           | CharC           = Left cs
 253 |       ConvertSimplification (EitherC x y) (Left m) | cs | CharC           | (PairC z w)     = Left cs
 254 |       ConvertSimplification (EitherC x y) (Left m) | cs | CharC           | StringC         = Left cs
 255 |       ConvertSimplification (EitherC x y) (Left m) | cs | CharC           | UnitC           = Just cs
 256 |       ConvertSimplification (EitherC x y) (Left m) | cs | CharC           | (EitherC _ _)   = Left cs
 257 |       ConvertSimplification (EitherC x y) (Left m) | cs | CharC           | (ListC z)       = Left cs
 258 |       ConvertSimplification (EitherC x y) (Left m) | cs | CharC           | (MaybeC z)      = Left cs
 259 |       ConvertSimplification (EitherC x y) (Left m) | cs | CharC           | BoolC           = Left cs
 260 |       ConvertSimplification (EitherC x y) (Left m) | cs | CharC           | NatC            = Left cs
 261 |       ConvertSimplification (EitherC x y) (Left m) | cs | CharC           | IgnoreC         = Just cs
 262 | 
 263 |       ConvertSimplification (EitherC x y) (Left m) | cs | (PairC _ _)     | CharC           = Left cs
 264 |       ConvertSimplification (EitherC x y) (Left m) | cs | (PairC _ _)     | (PairC z w)     = Left cs
 265 |       ConvertSimplification (EitherC x y) (Left m) | cs | (PairC _ _)     | StringC         = Left cs
 266 |       ConvertSimplification (EitherC x y) (Left m) | cs | (PairC _ _)     | UnitC           = Just cs
 267 |       ConvertSimplification (EitherC x y) (Left m) | cs | (PairC _ _)     | (EitherC _ _)   = Left cs
 268 |       ConvertSimplification (EitherC x y) (Left m) | cs | (PairC _ _)     | (ListC z)       = Left cs
 269 |       ConvertSimplification (EitherC x y) (Left m) | cs | (PairC _ _)     | (MaybeC z)      = Left cs
 270 |       ConvertSimplification (EitherC x y) (Left m) | cs | (PairC _ _)     | BoolC           = Left cs
 271 |       ConvertSimplification (EitherC x y) (Left m) | cs | (PairC _ _)     | NatC            = Left cs
 272 |       ConvertSimplification (EitherC x y) (Left m) | cs | (PairC _ _)     | IgnoreC         = Just cs
 273 | 
 274 |       ConvertSimplification (EitherC x y) (Left m) | cs | StringC         | CharC           = Left cs
 275 |       ConvertSimplification (EitherC x y) (Left m) | cs | StringC         | (PairC z w)     = Left cs
 276 |       ConvertSimplification (EitherC x y) (Left m) | cs | StringC         | StringC         = Left cs
 277 |       ConvertSimplification (EitherC x y) (Left m) | cs | StringC         | UnitC           = Just cs
 278 |       ConvertSimplification (EitherC x y) (Left m) | cs | StringC         | (EitherC _ _)   = Left cs
 279 |       ConvertSimplification (EitherC x y) (Left m) | cs | StringC         | (ListC z)       = Left cs
 280 |       ConvertSimplification (EitherC x y) (Left m) | cs | StringC         | (MaybeC z)      = Left cs
 281 |       ConvertSimplification (EitherC x y) (Left m) | cs | StringC         | BoolC           = Left cs
 282 |       ConvertSimplification (EitherC x y) (Left m) | cs | StringC         | NatC            = Left cs
 283 |       ConvertSimplification (EitherC x y) (Left m) | cs | StringC         | IgnoreC         = Just cs
 284 | 
 285 |       ConvertSimplification (EitherC x y) (Left m) | cs | UnitC           | CharC           = Nothing
 286 |       ConvertSimplification (EitherC x y) (Left m) | cs | UnitC           | (PairC z w)     = Nothing
 287 |       ConvertSimplification (EitherC x y) (Left m) | cs | UnitC           | StringC         = Nothing
 288 |       ConvertSimplification (EitherC x y) (Left m) | cs | UnitC           | UnitC           = True
 289 |       ConvertSimplification (EitherC x y) (Left m) | cs | UnitC           | (EitherC _ _)   = Nothing
 290 |       ConvertSimplification (EitherC x y) (Left m) | cs | UnitC           | (ListC z)       = Nothing
 291 |       ConvertSimplification (EitherC x y) (Left m) | cs | UnitC           | (MaybeC z)      = Nothing
 292 |       ConvertSimplification (EitherC x y) (Left m) | cs | UnitC           | BoolC           = Nothing
 293 |       ConvertSimplification (EitherC x y) (Left m) | cs | UnitC           | NatC            = Nothing
 294 |       ConvertSimplification (EitherC x y) (Left m) | cs | UnitC           | IgnoreC         = True
 295 | 
 296 |       ConvertSimplification (EitherC x y) (Left m) | cs | (EitherC _ _)   | CharC           = Left cs
 297 |       ConvertSimplification (EitherC x y) (Left m) | cs | (EitherC _ _)   | (PairC z w)     = Left cs
 298 |       ConvertSimplification (EitherC x y) (Left m) | cs | (EitherC _ _)   | StringC         = Left cs
 299 |       ConvertSimplification (EitherC x y) (Left m) | cs | (EitherC _ _)   | UnitC           = Just cs
 300 |       ConvertSimplification (EitherC x y) (Left m) | cs | (EitherC _ _)   | (EitherC _ _)   = Left cs
 301 |       ConvertSimplification (EitherC x y) (Left m) | cs | (EitherC _ _)   | (ListC z)       = Left cs
 302 |       ConvertSimplification (EitherC x y) (Left m) | cs | (EitherC _ _)   | (MaybeC z)      = Left cs
 303 |       ConvertSimplification (EitherC x y) (Left m) | cs | (EitherC _ _)   | BoolC           = Left cs
 304 |       ConvertSimplification (EitherC x y) (Left m) | cs | (EitherC _ _)   | NatC            = Left cs
 305 |       ConvertSimplification (EitherC x y) (Left m) | cs | (EitherC _ _)   | IgnoreC         = Just cs
 306 | 
 307 |       ConvertSimplification (EitherC x y) (Left m) | cs | (ListC _)       | CharC           = Left cs
 308 |       ConvertSimplification (EitherC x y) (Left m) | cs | (ListC _)       | (PairC z w)     = Left cs
 309 |       ConvertSimplification (EitherC x y) (Left m) | cs | (ListC _)       | StringC         = Left cs
 310 |       ConvertSimplification (EitherC x y) (Left m) | cs | (ListC _)       | UnitC           = Just cs
 311 |       ConvertSimplification (EitherC x y) (Left m) | cs | (ListC _)       | (EitherC _ _)   = Left cs
 312 |       ConvertSimplification (EitherC x y) (Left m) | cs | (ListC _)       | (ListC z)       = Left cs
 313 |       ConvertSimplification (EitherC x y) (Left m) | cs | (ListC _)       | (MaybeC z)      = Left cs
 314 |       ConvertSimplification (EitherC x y) (Left m) | cs | (ListC _)       | BoolC           = Left cs
 315 |       ConvertSimplification (EitherC x y) (Left m) | cs | (ListC _)       | NatC            = Left cs
 316 |       ConvertSimplification (EitherC x y) (Left m) | cs | (ListC _)       | IgnoreC         = Just cs
 317 | 
 318 |       ConvertSimplification (EitherC x y) (Left m) | cs | (MaybeC _)       | CharC           = Left cs
 319 |       ConvertSimplification (EitherC x y) (Left m) | cs | (MaybeC _)       | (PairC z w)     = Left cs
 320 |       ConvertSimplification (EitherC x y) (Left m) | cs | (MaybeC _)       | StringC         = Left cs
 321 |       ConvertSimplification (EitherC x y) (Left m) | cs | (MaybeC _)       | UnitC           = Just cs
 322 |       ConvertSimplification (EitherC x y) (Left m) | cs | (MaybeC _)       | (EitherC _ _)   = Left cs
 323 |       ConvertSimplification (EitherC x y) (Left m) | cs | (MaybeC _)       | (ListC z)       = Left cs
 324 |       ConvertSimplification (EitherC x y) (Left m) | cs | (MaybeC _)       | (MaybeC z)      = Left cs
 325 |       ConvertSimplification (EitherC x y) (Left m) | cs | (MaybeC _)       | BoolC           = Left cs
 326 |       ConvertSimplification (EitherC x y) (Left m) | cs | (MaybeC _)       | NatC            = Left cs
 327 |       ConvertSimplification (EitherC x y) (Left m) | cs | (MaybeC _)       | IgnoreC         = Just cs
 328 | 
 329 |       ConvertSimplification (EitherC x y) (Left m) | cs | BoolC           | CharC           = Left cs
 330 |       ConvertSimplification (EitherC x y) (Left m) | cs | BoolC           | (PairC z w)     = Left cs
 331 |       ConvertSimplification (EitherC x y) (Left m) | cs | BoolC           | StringC         = Left cs
 332 |       ConvertSimplification (EitherC x y) (Left m) | cs | BoolC           | UnitC           = Just cs
 333 |       ConvertSimplification (EitherC x y) (Left m) | cs | BoolC           | (EitherC _ _)   = Left cs
 334 |       ConvertSimplification (EitherC x y) (Left m) | cs | BoolC           | (ListC z)       = Left cs
 335 |       ConvertSimplification (EitherC x y) (Left m) | cs | BoolC           | (MaybeC z)      = Left cs
 336 |       ConvertSimplification (EitherC x y) (Left m) | cs | BoolC           | BoolC           = Left cs
 337 |       ConvertSimplification (EitherC x y) (Left m) | cs | BoolC           | NatC            = Left cs
 338 |       ConvertSimplification (EitherC x y) (Left m) | cs | BoolC           | IgnoreC         = Just cs
 339 | 
 340 |       ConvertSimplification (EitherC x y) (Left m) | cs | NatC            | CharC           = Left cs
 341 |       ConvertSimplification (EitherC x y) (Left m) | cs | NatC            | (PairC z w)     = Left cs
 342 |       ConvertSimplification (EitherC x y) (Left m) | cs | NatC            | StringC         = Left cs
 343 |       ConvertSimplification (EitherC x y) (Left m) | cs | NatC            | UnitC           = Just cs
 344 |       ConvertSimplification (EitherC x y) (Left m) | cs | NatC            | (EitherC _ _)   = Left cs
 345 |       ConvertSimplification (EitherC x y) (Left m) | cs | NatC            | (ListC z)       = Left cs
 346 |       ConvertSimplification (EitherC x y) (Left m) | cs | NatC            | (MaybeC z)      = Left cs
 347 |       ConvertSimplification (EitherC x y) (Left m) | cs | NatC            | BoolC           = Left cs
 348 |       ConvertSimplification (EitherC x y) (Left m) | cs | NatC            | NatC            = Left cs
 349 |       ConvertSimplification (EitherC x y) (Left m) | cs | NatC            | IgnoreC         = Just cs
 350 | 
 351 |       ConvertSimplification (EitherC x y) (Left m) | cs | IgnoreC         | CharC           = Nothing
 352 |       ConvertSimplification (EitherC x y) (Left m) | cs | IgnoreC         | (PairC z w)     = Nothing
 353 |       ConvertSimplification (EitherC x y) (Left m) | cs | IgnoreC         | StringC         = Nothing
 354 |       ConvertSimplification (EitherC x y) (Left m) | cs | IgnoreC         | UnitC           = False
 355 |       ConvertSimplification (EitherC x y) (Left m) | cs | IgnoreC         | (EitherC _ _)   = Nothing
 356 |       ConvertSimplification (EitherC x y) (Left m) | cs | IgnoreC         | (ListC z)       = Nothing
 357 |       ConvertSimplification (EitherC x y) (Left m) | cs | IgnoreC         | (MaybeC z)      = Nothing
 358 |       ConvertSimplification (EitherC x y) (Left m) | cs | IgnoreC         | BoolC           = Nothing
 359 |       ConvertSimplification (EitherC x y) (Left m) | cs | IgnoreC         | NatC            = Nothing
 360 |       ConvertSimplification (EitherC x y) (Left m) | cs | IgnoreC         | IgnoreC         = ()
 361 | 
 362 | ConvertSimplification (EitherC x y) (Right m) with (ConvertSimplification y m)
 363 |   ConvertSimplification (EitherC x y) (Right m) | cs with (SimplifyCode y)
 364 |     ConvertSimplification (EitherC x y) (Right m) | cs | sy with (SimplifyCode x)
 365 | 
 366 |       ConvertSimplification (EitherC x y) (Right m) | cs | CharC           | CharC           = Right cs
 367 |       ConvertSimplification (EitherC x y) (Right m) | cs | CharC           | (PairC z w)     = Right cs
 368 |       ConvertSimplification (EitherC x y) (Right m) | cs | CharC           | StringC         = Right cs
 369 |       ConvertSimplification (EitherC x y) (Right m) | cs | CharC           | UnitC           = Just cs
 370 |       ConvertSimplification (EitherC x y) (Right m) | cs | CharC           | (EitherC _ _)   = Right cs
 371 |       ConvertSimplification (EitherC x y) (Right m) | cs | CharC           | (ListC z)       = Right cs
 372 |       ConvertSimplification (EitherC x y) (Right m) | cs | CharC           | (MaybeC z)      = Right cs
 373 |       ConvertSimplification (EitherC x y) (Right m) | cs | CharC           | BoolC           = Right cs
 374 |       ConvertSimplification (EitherC x y) (Right m) | cs | CharC           | NatC            = Right cs
 375 |       ConvertSimplification (EitherC x y) (Right m) | cs | CharC           | IgnoreC         = Just cs
 376 | 
 377 |       ConvertSimplification (EitherC x y) (Right m) | cs | (PairC _ _)     | CharC           = Right cs
 378 |       ConvertSimplification (EitherC x y) (Right m) | cs | (PairC _ _)     | (PairC z w)     = Right cs
 379 |       ConvertSimplification (EitherC x y) (Right m) | cs | (PairC _ _)     | StringC         = Right cs
 380 |       ConvertSimplification (EitherC x y) (Right m) | cs | (PairC _ _)     | UnitC           = Just cs
 381 |       ConvertSimplification (EitherC x y) (Right m) | cs | (PairC _ _)     | (EitherC _ _)   = Right cs
 382 |       ConvertSimplification (EitherC x y) (Right m) | cs | (PairC _ _)     | (ListC z)       = Right cs
 383 |       ConvertSimplification (EitherC x y) (Right m) | cs | (PairC _ _)     | (MaybeC z)      = Right cs
 384 |       ConvertSimplification (EitherC x y) (Right m) | cs | (PairC _ _)     | BoolC           = Right cs
 385 |       ConvertSimplification (EitherC x y) (Right m) | cs | (PairC _ _)     | NatC            = Right cs
 386 |       ConvertSimplification (EitherC x y) (Right m) | cs | (PairC _ _)     | IgnoreC         = Just cs
 387 | 
 388 |       ConvertSimplification (EitherC x y) (Right m) | cs | StringC         | CharC           = Right cs
 389 |       ConvertSimplification (EitherC x y) (Right m) | cs | StringC         | (PairC z w)     = Right cs
 390 |       ConvertSimplification (EitherC x y) (Right m) | cs | StringC         | StringC         = Right cs
 391 |       ConvertSimplification (EitherC x y) (Right m) | cs | StringC         | UnitC           = Just cs
 392 |       ConvertSimplification (EitherC x y) (Right m) | cs | StringC         | (EitherC _ _)   = Right cs
 393 |       ConvertSimplification (EitherC x y) (Right m) | cs | StringC         | (ListC z)       = Right cs
 394 |       ConvertSimplification (EitherC x y) (Right m) | cs | StringC         | (MaybeC z)      = Right cs
 395 |       ConvertSimplification (EitherC x y) (Right m) | cs | StringC         | BoolC           = Right cs
 396 |       ConvertSimplification (EitherC x y) (Right m) | cs | StringC         | NatC            = Right cs
 397 |       ConvertSimplification (EitherC x y) (Right m) | cs | StringC         | IgnoreC         = Just cs
 398 | 
 399 |       ConvertSimplification (EitherC x y) (Right m) | cs | UnitC           | CharC           = Nothing
 400 |       ConvertSimplification (EitherC x y) (Right m) | cs | UnitC           | (PairC z w)     = Nothing
 401 |       ConvertSimplification (EitherC x y) (Right m) | cs | UnitC           | StringC         = Nothing
 402 |       ConvertSimplification (EitherC x y) (Right m) | cs | UnitC           | UnitC           = False
 403 |       ConvertSimplification (EitherC x y) (Right m) | cs | UnitC           | (EitherC _ _)   = Nothing
 404 |       ConvertSimplification (EitherC x y) (Right m) | cs | UnitC           | (ListC z)       = Nothing
 405 |       ConvertSimplification (EitherC x y) (Right m) | cs | UnitC           | (MaybeC z)      = Nothing
 406 |       ConvertSimplification (EitherC x y) (Right m) | cs | UnitC           | BoolC           = Nothing
 407 |       ConvertSimplification (EitherC x y) (Right m) | cs | UnitC           | NatC            = Nothing
 408 |       ConvertSimplification (EitherC x y) (Right m) | cs | UnitC           | IgnoreC         = True
 409 | 
 410 |       ConvertSimplification (EitherC x y) (Right m) | cs | (EitherC _ _)   | CharC           = Right cs
 411 |       ConvertSimplification (EitherC x y) (Right m) | cs | (EitherC _ _)   | (PairC z w)     = Right cs
 412 |       ConvertSimplification (EitherC x y) (Right m) | cs | (EitherC _ _)   | StringC         = Right cs
 413 |       ConvertSimplification (EitherC x y) (Right m) | cs | (EitherC _ _)   | UnitC           = Just cs
 414 |       ConvertSimplification (EitherC x y) (Right m) | cs | (EitherC _ _)   | (EitherC _ _)   = Right cs
 415 |       ConvertSimplification (EitherC x y) (Right m) | cs | (EitherC _ _)   | (ListC z)       = Right cs
 416 |       ConvertSimplification (EitherC x y) (Right m) | cs | (EitherC _ _)   | (MaybeC z)      = Right cs
 417 |       ConvertSimplification (EitherC x y) (Right m) | cs | (EitherC _ _)   | BoolC           = Right cs
 418 |       ConvertSimplification (EitherC x y) (Right m) | cs | (EitherC _ _)   | NatC            = Right cs
 419 |       ConvertSimplification (EitherC x y) (Right m) | cs | (EitherC _ _)   | IgnoreC         = Just cs
 420 | 
 421 |       ConvertSimplification (EitherC x y) (Right m) | cs | (ListC _)       | CharC           = Right cs
 422 |       ConvertSimplification (EitherC x y) (Right m) | cs | (ListC _)       | (PairC z w)     = Right cs
 423 |       ConvertSimplification (EitherC x y) (Right m) | cs | (ListC _)       | StringC         = Right cs
 424 |       ConvertSimplification (EitherC x y) (Right m) | cs | (ListC _)       | UnitC           = Just cs
 425 |       ConvertSimplification (EitherC x y) (Right m) | cs | (ListC _)       | (EitherC _ _)   = Right cs
 426 |       ConvertSimplification (EitherC x y) (Right m) | cs | (ListC _)       | (ListC z)       = Right cs
 427 |       ConvertSimplification (EitherC x y) (Right m) | cs | (ListC _)       | (MaybeC z)      = Right cs
 428 |       ConvertSimplification (EitherC x y) (Right m) | cs | (ListC _)       | BoolC           = Right cs
 429 |       ConvertSimplification (EitherC x y) (Right m) | cs | (ListC _)       | NatC            = Right cs
 430 |       ConvertSimplification (EitherC x y) (Right m) | cs | (ListC _)       | IgnoreC         = Just cs
 431 | 
 432 |       ConvertSimplification (EitherC x y) (Right m) | cs | (MaybeC _)       | CharC           = Right cs
 433 |       ConvertSimplification (EitherC x y) (Right m) | cs | (MaybeC _)       | (PairC z w)     = Right cs
 434 |       ConvertSimplification (EitherC x y) (Right m) | cs | (MaybeC _)       | StringC         = Right cs
 435 |       ConvertSimplification (EitherC x y) (Right m) | cs | (MaybeC _)       | UnitC           = Just cs
 436 |       ConvertSimplification (EitherC x y) (Right m) | cs | (MaybeC _)       | (EitherC _ _)   = Right cs
 437 |       ConvertSimplification (EitherC x y) (Right m) | cs | (MaybeC _)       | (ListC z)       = Right cs
 438 |       ConvertSimplification (EitherC x y) (Right m) | cs | (MaybeC _)       | (MaybeC z)      = Right cs
 439 |       ConvertSimplification (EitherC x y) (Right m) | cs | (MaybeC _)       | BoolC           = Right cs
 440 |       ConvertSimplification (EitherC x y) (Right m) | cs | (MaybeC _)       | NatC            = Right cs
 441 |       ConvertSimplification (EitherC x y) (Right m) | cs | (MaybeC _)       | IgnoreC         = Just cs
 442 | 
 443 |       ConvertSimplification (EitherC x y) (Right m) | cs | BoolC           | CharC           = Right cs
 444 |       ConvertSimplification (EitherC x y) (Right m) | cs | BoolC           | (PairC z w)     = Right cs
 445 |       ConvertSimplification (EitherC x y) (Right m) | cs | BoolC           | StringC         = Right cs
 446 |       ConvertSimplification (EitherC x y) (Right m) | cs | BoolC           | UnitC           = Just cs
 447 |       ConvertSimplification (EitherC x y) (Right m) | cs | BoolC           | (EitherC _ _)   = Right cs
 448 |       ConvertSimplification (EitherC x y) (Right m) | cs | BoolC           | (ListC z)       = Right cs
 449 |       ConvertSimplification (EitherC x y) (Right m) | cs | BoolC           | (MaybeC z)      = Right cs
 450 |       ConvertSimplification (EitherC x y) (Right m) | cs | BoolC           | BoolC           = Right cs
 451 |       ConvertSimplification (EitherC x y) (Right m) | cs | BoolC           | NatC            = Right cs
 452 |       ConvertSimplification (EitherC x y) (Right m) | cs | BoolC           | IgnoreC         = Just cs
 453 | 
 454 |       ConvertSimplification (EitherC x y) (Right m) | cs | NatC            | CharC           = Right cs
 455 |       ConvertSimplification (EitherC x y) (Right m) | cs | NatC            | (PairC z w)     = Right cs
 456 |       ConvertSimplification (EitherC x y) (Right m) | cs | NatC            | StringC         = Right cs
 457 |       ConvertSimplification (EitherC x y) (Right m) | cs | NatC            | UnitC           = Just cs
 458 |       ConvertSimplification (EitherC x y) (Right m) | cs | NatC            | (EitherC _ _)   = Right cs
 459 |       ConvertSimplification (EitherC x y) (Right m) | cs | NatC            | (ListC z)       = Right cs
 460 |       ConvertSimplification (EitherC x y) (Right m) | cs | NatC            | (MaybeC z)      = Right cs
 461 |       ConvertSimplification (EitherC x y) (Right m) | cs | NatC            | BoolC           = Right cs
 462 |       ConvertSimplification (EitherC x y) (Right m) | cs | NatC            | NatC            = Right cs
 463 |       ConvertSimplification (EitherC x y) (Right m) | cs | NatC            | IgnoreC         = Just cs
 464 | 
 465 |       ConvertSimplification (EitherC x y) (Right m) | cs | IgnoreC         | CharC           = Nothing
 466 |       ConvertSimplification (EitherC x y) (Right m) | cs | IgnoreC         | (PairC z w)     = Nothing
 467 |       ConvertSimplification (EitherC x y) (Right m) | cs | IgnoreC         | StringC         = Nothing
 468 |       ConvertSimplification (EitherC x y) (Right m) | cs | IgnoreC         | UnitC           = False
 469 |       ConvertSimplification (EitherC x y) (Right m) | cs | IgnoreC         | (EitherC _ _)   = Nothing
 470 |       ConvertSimplification (EitherC x y) (Right m) | cs | IgnoreC         | (ListC z)       = Nothing
 471 |       ConvertSimplification (EitherC x y) (Right m) | cs | IgnoreC         | (MaybeC z)      = Nothing
 472 |       ConvertSimplification (EitherC x y) (Right m) | cs | IgnoreC         | BoolC           = Nothing
 473 |       ConvertSimplification (EitherC x y) (Right m) | cs | IgnoreC         | NatC            = Nothing
 474 |       ConvertSimplification (EitherC x y) (Right m) | cs | IgnoreC         | IgnoreC         = ()