
   0 | module TyRE.RE
   1 | 
   2 | import Data.List
   3 | import Data.Maybe
   4 | 
   5 | import TyRE.Codes
   6 | import TyRE.Core
   7 | 
   8 | public export
   9 | data RE =
  10 |     Exactly Char -- x
  11 |   | OneOf (List Char) -- [x,y,z]
  12 |   | To Char Char -- [x-y]
  13 |   | Any -- .
  14 |   | Concat RE RE -- AB
  15 |   | Alt RE RE -- A|B
  16 |   | Maybe RE -- A?
  17 |   | Group RE -- `A`
  18 |   | Rep0 RE -- A*
  19 |   | Rep1 RE -- A+
  20 |   | Keep RE
  21 | 
  22 | public export
  23 | Eq RE where
  24 |   (Exactly x) == (Exactly x')                 = x == x'
  25 |   (OneOf xs) == (OneOf ys)                    = xs == ys
  26 |   (x `To` y) == (x' `To` y')                  = (x == x') && (y == y')
  27 |   Any        == Any                           = True
  28 |   (re1 `Concat` re2) == (re1' `Concat` re2')  = (re1 == re1') && (re2 == re2')
  29 |   (Group x) == (Group x')                     = x == x'
  30 |   (Keep x) == (Keep x')                       = x == x'
  31 |   (re1 `Alt` re2) == (re1' `Alt` re2')        = (re1 == re1') && (re2 == re2')
  32 |   (Maybe re) == (Maybe re')                   = re == re'
  33 |   (Rep0 re) == (Rep0 re')                     = re == re'
  34 |   (Rep1 re) == (Rep1 re')                     = re == re'
  35 |   _ == _                                      = False
  36 | 
  37 | public export
  38 | specialChars : String
  39 | specialChars = "[]()\\`-|?+.*!"
  40 | 
  41 | public export
  42 | mapChar : Char -> String
  43 | mapChar c = case (find (\sc => c == sc) (unpack specialChars)) of {Just _ => "\\" ++ (cast c); Nothing => (cast c)}
  44 | 
  45 | public export
  46 | isUnit : RE -> Bool
  47 | isUnit (Exactly x) = True
  48 | isUnit (OneOf xs) = True
  49 | isUnit (To x y) = True
  50 | isUnit Any = True
  51 | isUnit (Concat x y) = False
  52 | isUnit (Alt x y) = False
  53 | isUnit (Maybe x) = False
  54 | isUnit (Group x) = True
  55 | isUnit (Keep x) = False
  56 | isUnit (Rep0 x) = False
  57 | isUnit (Rep1 x) = False
  58 | 
  59 | public export
  60 | isSemiUnit : RE -> Bool
  61 | isSemiUnit (Exactly x) = True
  62 | isSemiUnit (OneOf xs) = True
  63 | isSemiUnit (To x y) = True
  64 | isSemiUnit Any = True
  65 | isSemiUnit (Concat x y) = False
  66 | isSemiUnit (Alt x y) = False
  67 | isSemiUnit (Maybe x) = True
  68 | isSemiUnit (Group x) = True
  69 | isSemiUnit (Keep x) = True
  70 | isSemiUnit (Rep0 x) = True
  71 | isSemiUnit (Rep1 x) = True
  72 | 
  73 | mutual
  74 |   ||| If condintion is satisfied show in parentheses
  75 |   public export
  76 |   pshow : (RE -> Bool) -> RE -> String
  77 |   pshow condition re = if (condition re)
  78 |                 then showAux re
  79 |                 else "(" ++ showAux re ++ ")"
  80 | 
  81 |   public export
  82 |   showAux : RE -> String
  83 |   showAux (Exactly c) = mapChar c
  84 |   showAux (OneOf xs) = "[" ++ (foldl (++) "" (map mapChar xs)) ++ "]"
  85 |   showAux (To x y) = "[" ++ (mapChar x) ++ "-" ++ (mapChar y) ++ "]"
  86 |   showAux Any = "."
  87 |   showAux (Concat x y) = pshow isSemiUnit x ++ showAux y
  88 |   showAux (Alt x y) = pshow isSemiUnit x ++ "|" ++ pshow isSemiUnit y
  89 |   showAux (Maybe x) = pshow isUnit x ++ "?"
  90 |   showAux (Group x) = "`" ++ showAux x ++ "`"
  91 |   showAux (Rep0 x) = pshow isUnit x ++ "*"
  92 |   showAux (Rep1 x) = pshow isUnit x ++ "+"
  93 |   showAux (Keep x) = pshow isSemiUnit x ++ "!"
  94 | 
  95 | public export
  96 | Show RE where
  97 |   show = showAux
  98 | 
  99 | public export
 100 | CodeShapeREKeep : RE -> Code
 101 | CodeShapeREKeep (Exactly _) = UnitC
 102 | CodeShapeREKeep (OneOf _) = CharC
 103 | CodeShapeREKeep (To _ _) = CharC
 104 | CodeShapeREKeep Any = CharC
 105 | CodeShapeREKeep (Concat re1 re2) = PairC (CodeShapeREKeep re1) (CodeShapeREKeep re2)
 106 | CodeShapeREKeep (Alt re1 re2) = EitherC (CodeShapeREKeep re1) (CodeShapeREKeep re2)
 107 | CodeShapeREKeep (Group _) = StringC
 108 | CodeShapeREKeep (Maybe re) = MaybeC (CodeShapeREKeep re)
 109 | CodeShapeREKeep (Rep0 re) = ListC (CodeShapeREKeep re)
 110 | CodeShapeREKeep (Rep1 re) = ListC (CodeShapeREKeep re)
 111 | CodeShapeREKeep (Keep re) = CodeShapeREKeep re
 112 | 
 113 | public export
 114 | CodeShapeRE : RE -> Code
 115 | CodeShapeRE (Exactly _) = IgnoreC
 116 | CodeShapeRE (OneOf _) = IgnoreC
 117 | CodeShapeRE (To _ _) = IgnoreC
 118 | CodeShapeRE Any = IgnoreC
 119 | CodeShapeRE (Concat re1 re2) = PairC (CodeShapeRE re1) (CodeShapeRE re2)
 120 | CodeShapeRE (Alt re1 re2) = EitherC (CodeShapeRE re1) (CodeShapeRE re2)
 121 | CodeShapeRE (Group _) = StringC
 122 | CodeShapeRE (Maybe re) = MaybeC (CodeShapeRE re)
 123 | CodeShapeRE (Rep0 re) = ListC (CodeShapeRE re)
 124 | CodeShapeRE (Rep1 re) = ListC (CodeShapeRE re)
 125 | CodeShapeRE (Keep re) = CodeShapeREKeep re
 126 | 
 127 | public export
 128 | TypeREKeep : RE -> Type
 129 | TypeREKeep = (Sem . SimplifyCode . CodeShapeREKeep)
 130 | 
 131 | public export
 132 | TypeRE : RE -> Type
 133 | TypeRE = (Sem . SimplifyCode . CodeShapeRE)
 134 | 
 135 | export
 136 | pairEq : ((a, x) = (b, y)) -> (a = b, x = y)
 137 | pairEq Refl = (Refl, Refl)
 138 | 
 139 | export
 140 | eitherToMaybeL : Either a () -> Maybe a
 141 | eitherToMaybeL (Left x) = Just x
 142 | eitherToMaybeL (Right _) = Nothing
 143 | 
 144 | export
 145 | eitherToMaybeR : Either () a -> Maybe a
 146 | eitherToMaybeR (Left _) = Nothing
 147 | eitherToMaybeR (Right x) = Just x
 148 | 
 149 | 
 150 | mutual
 151 |   public export
 152 |   altTyREKeep : (re1 : RE) -> (re2 : RE)
 153 |           -> ((SimplifyCode (CodeShapeREKeep re1)) = a)
 154 |           -> ((SimplifyCode (CodeShapeREKeep re2)) = b)
 155 |           -> TyRE $ Either (Sem a) (Sem b)
 156 |   altTyREKeep re1 re2 Refl Refl = compileKeep re1 <|> compileKeep re2
 157 | 
 158 |   public export
 159 |   concatTyREKeep : (re1 : RE) -> (re2 : RE) -> TyRE (TypeREKeep re1, TypeREKeep re2)
 160 |   concatTyREKeep re1 re2 = compileKeep re1 <*> compileKeep re2
 161 | 
 162 |   public export
 163 |   compileKeep                  : (re : RE) -> TyRE $ TypeREKeep re
 164 |   compileKeep (Exactly x)      = match x
 165 |   compileKeep (OneOf xs)       = oneOfCharsList xs
 166 |   compileKeep (To x y)         = range x y
 167 |   compileKeep Any              = any
 168 |   compileKeep (Group re)       = group (compileKeep re)
 169 |   compileKeep (Concat re1 re2) with (SimplifyCode (CodeShapeREKeep re1), SimplifyCode (CodeShapeREKeep re2)) proof p
 170 |     compileKeep (Concat re1 re2) | (CharC, CharC) = concatTyREKeep re1 re2
 171 |     compileKeep (Concat re1 re2) | (CharC, (PairC x y)) = concatTyREKeep re1 re2
 172 |     compileKeep (Concat re1 re2) | (CharC, StringC) = concatTyREKeep re1 re2
 173 |     compileKeep (Concat re1 re2) | (CharC, UnitC) =
 174 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 175 |       $ compileKeep re1 <* (compileKeep re2)
 176 |     compileKeep (Concat re1 re2) | (CharC, (EitherC x y)) = concatTyREKeep re1 re2
 177 |     compileKeep (Concat re1 re2) | (CharC, (MaybeC x)) = concatTyREKeep re1 re2
 178 |     compileKeep (Concat re1 re2) | (CharC, BoolC) = concatTyREKeep re1 re2
 179 |     compileKeep (Concat re1 re2) | (CharC, (ListC z)) = concatTyREKeep re1 re2
 180 |     compileKeep (Concat re1 re2) | (CharC, NatC) = concatTyREKeep re1 re2
 181 |     compileKeep (Concat re1 re2) | (CharC, IgnoreC) = 
 182 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 183 |       $ compileKeep re1 <* (compileKeep re2)
 184 |     compileKeep (Concat re1 re2) | ((PairC x y), CharC) = concatTyREKeep re1 re2
 185 |     compileKeep (Concat re1 re2) | ((PairC x y), (PairC z w)) = concatTyREKeep re1 re2
 186 |     compileKeep (Concat re1 re2) | ((PairC x y), StringC) = concatTyREKeep re1 re2
 187 |     compileKeep (Concat re1 re2) | ((PairC x y), UnitC) =
 188 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 189 |       $ compileKeep re1 <* (compileKeep re2)
 190 |     compileKeep (Concat re1 re2) | ((PairC x y), (EitherC z w)) = concatTyREKeep re1 re2
 191 |     compileKeep (Concat re1 re2) | ((PairC x y), (MaybeC z)) = concatTyREKeep re1 re2
 192 |     compileKeep (Concat re1 re2) | ((PairC x y), BoolC) = concatTyREKeep re1 re2
 193 |     compileKeep (Concat re1 re2) | ((PairC x y), (ListC z)) = concatTyREKeep re1 re2
 194 |     compileKeep (Concat re1 re2) | ((PairC x y), NatC) = concatTyREKeep re1 re2
 195 |     compileKeep (Concat re1 re2) | ((PairC x y), IgnoreC) = 
 196 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 197 |       $ compileKeep re1 <* (compileKeep re2)
 198 |     compileKeep (Concat re1 re2) | (StringC, CharC) = concatTyREKeep re1 re2
 199 |     compileKeep (Concat re1 re2) | (StringC, (PairC x y)) = concatTyREKeep re1 re2
 200 |     compileKeep (Concat re1 re2) | (StringC, StringC) = concatTyREKeep re1 re2
 201 |     compileKeep (Concat re1 re2) | (StringC, UnitC) =
 202 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 203 |       $ compileKeep re1 <* (compileKeep re2)
 204 |     compileKeep (Concat re1 re2) | (StringC, (EitherC x y)) = concatTyREKeep re1 re2
 205 |     compileKeep (Concat re1 re2) | (StringC, (MaybeC x)) = concatTyREKeep re1 re2
 206 |     compileKeep (Concat re1 re2) | (StringC, BoolC) = concatTyREKeep re1 re2
 207 |     compileKeep (Concat re1 re2) | (StringC, (ListC z)) = concatTyREKeep re1 re2
 208 |     compileKeep (Concat re1 re2) | (StringC, NatC) = concatTyREKeep re1 re2
 209 |     compileKeep (Concat re1 re2) | (StringC, IgnoreC) =
 210 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 211 |       $ compileKeep re1 <* (compileKeep re2)
 212 |     compileKeep (Concat re1 re2) | (UnitC, CharC) =
 213 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 214 |       $ compileKeep re1 *> (compileKeep re2)
 215 |     compileKeep (Concat re1 re2) | (UnitC, (PairC x y)) =
 216 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 217 |       $ compileKeep re1 *> (compileKeep re2)
 218 |     compileKeep (Concat re1 re2) | (UnitC, StringC) =
 219 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 220 |       $ compileKeep re1 *> (compileKeep re2)
 221 |     compileKeep (Concat re1 re2) | (UnitC, UnitC) = ignore (concatTyREKeep re1 re2)
 222 |     compileKeep (Concat re1 re2) | (UnitC, (EitherC x y)) =
 223 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 224 |       $ compileKeep re1 *> (compileKeep re2)
 225 |     compileKeep (Concat re1 re2) | (UnitC, (MaybeC x)) =
 226 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 227 |       $ compileKeep re1 *> (compileKeep re2)
 228 |     compileKeep (Concat re1 re2) | (UnitC, BoolC) =
 229 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 230 |       $ compileKeep re1 *> (compileKeep re2)
 231 |     compileKeep (Concat re1 re2) | (UnitC, (ListC z)) =
 232 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 233 |       $ compileKeep re1 *> (compileKeep re2)
 234 |     compileKeep (Concat re1 re2) | (UnitC, NatC) =
 235 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 236 |       $ compileKeep re1 *> (compileKeep re2)
 237 |     compileKeep (Concat re1 re2) | (UnitC, IgnoreC) = ignore (concatTyREKeep re1 re2)
 238 |     compileKeep (Concat re1 re2) | ((EitherC x y), CharC) = concatTyREKeep re1 re2
 239 |     compileKeep (Concat re1 re2) | ((EitherC x y), (PairC z w)) = concatTyREKeep re1 re2
 240 |     compileKeep (Concat re1 re2) | ((EitherC x y), StringC) = concatTyREKeep re1 re2
 241 |     compileKeep (Concat re1 re2) | ((EitherC x y), UnitC) =
 242 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 243 |       $ compileKeep re1 <* (compileKeep re2)
 244 |     compileKeep (Concat re1 re2) | ((EitherC x y), (EitherC z w)) = concatTyREKeep re1 re2
 245 |     compileKeep (Concat re1 re2) | ((EitherC x y), (MaybeC z)) = concatTyREKeep re1 re2
 246 |     compileKeep (Concat re1 re2) | ((EitherC x y), BoolC) = concatTyREKeep re1 re2
 247 |     compileKeep (Concat re1 re2) | ((EitherC x y), (ListC z)) = concatTyREKeep re1 re2
 248 |     compileKeep (Concat re1 re2) | ((EitherC x y), NatC) = concatTyREKeep re1 re2
 249 |     compileKeep (Concat re1 re2) | ((EitherC x y), IgnoreC) =
 250 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 251 |       $ compileKeep re1 <* (compileKeep re2)
 252 |     compileKeep (Concat re1 re2) | ((MaybeC x), CharC) = concatTyREKeep re1 re2
 253 |     compileKeep (Concat re1 re2) | ((MaybeC x), (PairC y z)) = concatTyREKeep re1 re2
 254 |     compileKeep (Concat re1 re2) | ((MaybeC x), StringC) = concatTyREKeep re1 re2
 255 |     compileKeep (Concat re1 re2) | ((MaybeC x), UnitC) =
 256 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 257 |       $ compileKeep re1 <* compileKeep re2
 258 |     compileKeep (Concat re1 re2) | ((MaybeC x), (EitherC y z)) = concatTyREKeep re1 re2
 259 |     compileKeep (Concat re1 re2) | ((MaybeC x), (MaybeC y)) = concatTyREKeep re1 re2
 260 |     compileKeep (Concat re1 re2) | ((MaybeC x), BoolC) = concatTyREKeep re1 re2
 261 |     compileKeep (Concat re1 re2) | ((MaybeC x), (ListC z)) = concatTyREKeep re1 re2
 262 |     compileKeep (Concat re1 re2) | ((MaybeC x), NatC) = concatTyREKeep re1 re2
 263 |     compileKeep (Concat re1 re2) | ((MaybeC x), IgnoreC) = 
 264 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 265 |       $ compileKeep re1 <* compileKeep re2
 266 |     compileKeep (Concat re1 re2) | (BoolC, CharC) = concatTyREKeep re1 re2
 267 |     compileKeep (Concat re1 re2) | (BoolC, (PairC x y)) = concatTyREKeep re1 re2
 268 |     compileKeep (Concat re1 re2) | (BoolC, StringC) = concatTyREKeep re1 re2
 269 |     compileKeep (Concat re1 re2) | (BoolC, UnitC) =
 270 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 271 |       $ compileKeep re1 <* compileKeep re2
 272 |     compileKeep (Concat re1 re2) | (BoolC, (EitherC x y)) = concatTyREKeep re1 re2
 273 |     compileKeep (Concat re1 re2) | (BoolC, (MaybeC x)) = concatTyREKeep re1 re2
 274 |     compileKeep (Concat re1 re2) | (BoolC, BoolC) = concatTyREKeep re1 re2
 275 |     compileKeep (Concat re1 re2) | (BoolC, (ListC z)) = concatTyREKeep re1 re2
 276 |     compileKeep (Concat re1 re2) | (BoolC, NatC) = concatTyREKeep re1 re2
 277 |     compileKeep (Concat re1 re2) | (BoolC, IgnoreC) = 
 278 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 279 |       $ compileKeep re1 <* compileKeep re2
 280 |     compileKeep (Concat re1 re2) | ((ListC z), CharC) = concatTyREKeep re1 re2
 281 |     compileKeep (Concat re1 re2) | ((ListC z), (PairC x y)) = concatTyREKeep re1 re2
 282 |     compileKeep (Concat re1 re2) | ((ListC z), StringC) = concatTyREKeep re1 re2
 283 |     compileKeep (Concat re1 re2) | ((ListC z), UnitC) =
 284 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 285 |       $ compileKeep re1 <* compileKeep re2
 286 |     compileKeep (Concat re1 re2) | ((ListC z), (EitherC x y)) = concatTyREKeep re1 re2
 287 |     compileKeep (Concat re1 re2) | ((ListC z), (MaybeC x)) = concatTyREKeep re1 re2
 288 |     compileKeep (Concat re1 re2) | ((ListC z), BoolC) = concatTyREKeep re1 re2
 289 |     compileKeep (Concat re1 re2) | ((ListC z), (ListC x)) = concatTyREKeep re1 re2
 290 |     compileKeep (Concat re1 re2) | ((ListC z), NatC) = concatTyREKeep re1 re2
 291 |     compileKeep (Concat re1 re2) | ((ListC z), IgnoreC) = 
 292 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 293 |       $ compileKeep re1 <* (compileKeep re2)
 294 |     compileKeep (Concat re1 re2) | (NatC, CharC) = concatTyREKeep re1 re2
 295 |     compileKeep (Concat re1 re2) | (NatC, (PairC x y)) = concatTyREKeep re1 re2
 296 |     compileKeep (Concat re1 re2) | (NatC, StringC) = concatTyREKeep re1 re2
 297 |     compileKeep (Concat re1 re2) | (NatC, UnitC) =
 298 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 299 |       $ compileKeep re1 <* compileKeep re2
 300 |     compileKeep (Concat re1 re2) | (NatC, (EitherC x y)) = concatTyREKeep re1 re2
 301 |     compileKeep (Concat re1 re2) | (NatC, (MaybeC x)) = concatTyREKeep re1 re2
 302 |     compileKeep (Concat re1 re2) | (NatC, BoolC) = concatTyREKeep re1 re2
 303 |     compileKeep (Concat re1 re2) | (NatC, (ListC z)) = concatTyREKeep re1 re2
 304 |     compileKeep (Concat re1 re2) | (NatC, NatC) = concatTyREKeep re1 re2
 305 |     compileKeep (Concat re1 re2) | (NatC, IgnoreC) = 
 306 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 307 |       $ compileKeep re1 <* compileKeep re2
 308 |     compileKeep (Concat re1 re2) | (IgnoreC, CharC) = 
 309 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 310 |       $ compileKeep re1 *> compileKeep re2
 311 |     compileKeep (Concat re1 re2) | (IgnoreC, (PairC x y)) = 
 312 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 313 |       $ compileKeep re1 *> compileKeep re2
 314 |     compileKeep (Concat re1 re2) | (IgnoreC, StringC) = 
 315 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 316 |       $ compileKeep re1 *> compileKeep re2
 317 |     compileKeep (Concat re1 re2) | (IgnoreC, UnitC) = ignore (compileKeep re1 <*> compileKeep re2)
 318 |     compileKeep (Concat re1 re2) | (IgnoreC, (EitherC x y)) = 
 319 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 320 |       $ compileKeep re1 *> compileKeep re2
 321 |     compileKeep (Concat re1 re2) | (IgnoreC, (MaybeC x)) = 
 322 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 323 |       $ compileKeep re1 *> compileKeep re2
 324 |     compileKeep (Concat re1 re2) | (IgnoreC, BoolC) =
 325 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 326 |       $ compileKeep re1 *> compileKeep re2
 327 |     compileKeep (Concat re1 re2) | (IgnoreC, (ListC z)) =
 328 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 329 |       $ compileKeep re1 *> compileKeep re2
 330 |     compileKeep (Concat re1 re2) | (IgnoreC, NatC) =
 331 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 332 |       $ compileKeep re1 *> compileKeep re2
 333 |     compileKeep (Concat re1 re2) | (IgnoreC, IgnoreC) = ignore (compileKeep re1 <*> compileKeep re2)
 334 | 
 335 |   compileKeep (Alt re1 re2) with (SimplifyCode (CodeShapeREKeep re1)) proof p1
 336 |     compileKeep (Alt re1 re2) | sc1 with (SimplifyCode (CodeShapeREKeep re2)) proof p2
 337 |       compileKeep (Alt re1 re2) | CharC | CharC = altTyREKeep re1 re2 p1 p2
 338 |       compileKeep (Alt re1 re2) | CharC | (PairC x y) = altTyREKeep re1 re2 p1 p2
 339 |       compileKeep (Alt re1 re2) | CharC | StringC = altTyREKeep re1 re2 p1 p2
 340 |       compileKeep (Alt re1 re2) | CharC | UnitC = eitherToMaybeL `map` altTyREKeep re1 re2 p1 p2
 341 |       compileKeep (Alt re1 re2) | CharC | (EitherC x y) = altTyREKeep re1 re2 p1 p2
 342 |       compileKeep (Alt re1 re2) | CharC | (MaybeC x) = altTyREKeep re1 re2 p1 p2
 343 |       compileKeep (Alt re1 re2) | CharC | BoolC = altTyREKeep re1 re2 p1 p2
 344 |       compileKeep (Alt re1 re2) | CharC | (ListC x) = altTyREKeep re1 re2 p1 p2
 345 |       compileKeep (Alt re1 re2) | CharC | NatC = altTyREKeep re1 re2 p1 p2
 346 |       compileKeep (Alt re1 re2) | CharC | IgnoreC = eitherToMaybeL `map` altTyREKeep re1 re2 p1 p2
 347 |       compileKeep (Alt re1 re2) | (PairC x y) | CharC = altTyREKeep re1 re2 p1 p2
 348 |       compileKeep (Alt re1 re2) | (PairC x y) | (PairC z w) = altTyREKeep re1 re2 p1 p2
 349 |       compileKeep (Alt re1 re2) | (PairC x y) | StringC = altTyREKeep re1 re2 p1 p2
 350 |       compileKeep (Alt re1 re2) | (PairC x y) | UnitC = eitherToMaybeL `map` altTyREKeep re1 re2 p1 p2
 351 |       compileKeep (Alt re1 re2) | (PairC x y) | (EitherC z w) = altTyREKeep re1 re2 p1 p2
 352 |       compileKeep (Alt re1 re2) | (PairC x y) | (MaybeC z) = altTyREKeep re1 re2 p1 p2
 353 |       compileKeep (Alt re1 re2) | (PairC x y) | BoolC = altTyREKeep re1 re2 p1 p2
 354 |       compileKeep (Alt re1 re2) | (PairC x y) | (ListC z) = altTyREKeep re1 re2 p1 p2
 355 |       compileKeep (Alt re1 re2) | (PairC x y) | NatC = altTyREKeep re1 re2 p1 p2
 356 |       compileKeep (Alt re1 re2) | (PairC x y) | IgnoreC = eitherToMaybeL `map` altTyREKeep re1 re2 p1 p2
 357 |       compileKeep (Alt re1 re2) | StringC | CharC = altTyREKeep re1 re2 p1 p2
 358 |       compileKeep (Alt re1 re2) | StringC | (PairC x y) = altTyREKeep re1 re2 p1 p2
 359 |       compileKeep (Alt re1 re2) | StringC | StringC = altTyREKeep re1 re2 p1 p2
 360 |       compileKeep (Alt re1 re2) | StringC | UnitC = eitherToMaybeL `map` altTyREKeep re1 re2 p1 p2
 361 |       compileKeep (Alt re1 re2) | StringC | (EitherC x y) = altTyREKeep re1 re2 p1 p2
 362 |       compileKeep (Alt re1 re2) | StringC | (MaybeC x) = altTyREKeep re1 re2 p1 p2
 363 |       compileKeep (Alt re1 re2) | StringC | BoolC = altTyREKeep re1 re2 p1 p2
 364 |       compileKeep (Alt re1 re2) | StringC | (ListC x) = altTyREKeep re1 re2 p1 p2
 365 |       compileKeep (Alt re1 re2) | StringC | NatC = altTyREKeep re1 re2 p1 p2
 366 |       compileKeep (Alt re1 re2) | StringC | IgnoreC = eitherToMaybeL `map` altTyREKeep re1 re2 p1 p2
 367 |       compileKeep (Alt re1 re2) | UnitC | CharC = eitherToMaybeR `map` altTyREKeep re1 re2 p1 p2
 368 |       compileKeep (Alt re1 re2) | UnitC | (PairC x y) = eitherToMaybeR `map` altTyREKeep re1 re2 p1 p2
 369 |       compileKeep (Alt re1 re2) | UnitC | StringC = eitherToMaybeR `map` altTyREKeep re1 re2 p1 p2
 370 |       compileKeep (Alt re1 re2) | UnitC | UnitC =
 371 |         let f : Either () () -> Bool
 372 |             f (Left _) = True
 373 |             f (Right _) = False
 374 |         in f `map` altTyREKeep re1 re2 p1 p2
 375 |       compileKeep (Alt re1 re2) | UnitC | (EitherC x y) = eitherToMaybeR `map` altTyREKeep re1 re2 p1 p2
 376 |       compileKeep (Alt re1 re2) | UnitC | (MaybeC x) = eitherToMaybeR `map` altTyREKeep re1 re2 p1 p2
 377 |       compileKeep (Alt re1 re2) | UnitC | BoolC = eitherToMaybeR `map` altTyREKeep re1 re2 p1 p2
 378 |       compileKeep (Alt re1 re2) | UnitC | (ListC x) = eitherToMaybeR `map` altTyREKeep re1 re2 p1 p2
 379 |       compileKeep (Alt re1 re2) | UnitC | NatC = eitherToMaybeR `map` altTyREKeep re1 re2 p1 p2
 380 |       compileKeep (Alt re1 re2) | UnitC | IgnoreC = (isJust . eitherToMaybeL) `map` altTyREKeep re1 re2 p1 p2
 381 |       compileKeep (Alt re1 re2) | (EitherC x y) | CharC = altTyREKeep re1 re2 p1 p2
 382 |       compileKeep (Alt re1 re2) | (EitherC x y) | (PairC z w) = altTyREKeep re1 re2 p1 p2
 383 |       compileKeep (Alt re1 re2) | (EitherC x y) | StringC = altTyREKeep re1 re2 p1 p2
 384 |       compileKeep (Alt re1 re2) | (EitherC x y) | UnitC = eitherToMaybeL `map` altTyREKeep re1 re2 p1 p2
 385 |       compileKeep (Alt re1 re2) | (EitherC x y) | (EitherC z w) = altTyREKeep re1 re2 p1 p2
 386 |       compileKeep (Alt re1 re2) | (EitherC x y) | (MaybeC z) = altTyREKeep re1 re2 p1 p2
 387 |       compileKeep (Alt re1 re2) | (EitherC x y) | BoolC = altTyREKeep re1 re2 p1 p2
 388 |       compileKeep (Alt re1 re2) | (EitherC x y) | (ListC z) = altTyREKeep re1 re2 p1 p2
 389 |       compileKeep (Alt re1 re2) | (EitherC x y) | NatC = altTyREKeep re1 re2 p1 p2
 390 |       compileKeep (Alt re1 re2) | (EitherC x y) | IgnoreC = eitherToMaybeL `map` altTyREKeep re1 re2 p1 p2
 391 |       compileKeep (Alt re1 re2) | (MaybeC x) | CharC = altTyREKeep re1 re2 p1 p2
 392 |       compileKeep (Alt re1 re2) | (MaybeC x) | (PairC y z) = altTyREKeep re1 re2 p1 p2
 393 |       compileKeep (Alt re1 re2) | (MaybeC x) | StringC = altTyREKeep re1 re2 p1 p2
 394 |       compileKeep (Alt re1 re2) | (MaybeC x) | UnitC = eitherToMaybeL `map` altTyREKeep re1 re2 p1 p2
 395 |       compileKeep (Alt re1 re2) | (MaybeC x) | (EitherC y z) = altTyREKeep re1 re2 p1 p2
 396 |       compileKeep (Alt re1 re2) | (MaybeC x) | (MaybeC y) = altTyREKeep re1 re2 p1 p2
 397 |       compileKeep (Alt re1 re2) | (MaybeC x) | BoolC = altTyREKeep re1 re2 p1 p2
 398 |       compileKeep (Alt re1 re2) | (MaybeC x) | (ListC z) = altTyREKeep re1 re2 p1 p2
 399 |       compileKeep (Alt re1 re2) | (MaybeC x) | NatC = altTyREKeep re1 re2 p1 p2
 400 |       compileKeep (Alt re1 re2) | (MaybeC x) | IgnoreC = eitherToMaybeL `map` altTyREKeep re1 re2 p1 p2
 401 |       compileKeep (Alt re1 re2) | BoolC | CharC = altTyREKeep re1 re2 p1 p2
 402 |       compileKeep (Alt re1 re2) | BoolC | (PairC x y) = altTyREKeep re1 re2 p1 p2
 403 |       compileKeep (Alt re1 re2) | BoolC | StringC = altTyREKeep re1 re2 p1 p2
 404 |       compileKeep (Alt re1 re2) | BoolC | UnitC = eitherToMaybeL `map` altTyREKeep re1 re2 p1 p2
 405 |       compileKeep (Alt re1 re2) | BoolC | (EitherC x y) = altTyREKeep re1 re2 p1 p2
 406 |       compileKeep (Alt re1 re2) | BoolC | (MaybeC x) = altTyREKeep re1 re2 p1 p2
 407 |       compileKeep (Alt re1 re2) | BoolC | BoolC = altTyREKeep re1 re2 p1 p2
 408 |       compileKeep (Alt re1 re2) | BoolC | (ListC z) = altTyREKeep re1 re2 p1 p2
 409 |       compileKeep (Alt re1 re2) | BoolC | NatC = altTyREKeep re1 re2 p1 p2
 410 |       compileKeep (Alt re1 re2) | BoolC | IgnoreC = eitherToMaybeL `map` altTyREKeep re1 re2 p1 p2
 411 |       compileKeep (Alt re1 re2) | (ListC z) | CharC = altTyREKeep re1 re2 p1 p2
 412 |       compileKeep (Alt re1 re2) | (ListC z) | (PairC x y) = altTyREKeep re1 re2 p1 p2
 413 |       compileKeep (Alt re1 re2) | (ListC z) | StringC = altTyREKeep re1 re2 p1 p2
 414 |       compileKeep (Alt re1 re2) | (ListC z) | UnitC = eitherToMaybeL `map` altTyREKeep re1 re2 p1 p2
 415 |       compileKeep (Alt re1 re2) | (ListC z) | (EitherC x y) = altTyREKeep re1 re2 p1 p2
 416 |       compileKeep (Alt re1 re2) | (ListC z) | (MaybeC x) = altTyREKeep re1 re2 p1 p2
 417 |       compileKeep (Alt re1 re2) | (ListC z) | BoolC = altTyREKeep re1 re2 p1 p2
 418 |       compileKeep (Alt re1 re2) | (ListC z) | (ListC x) = altTyREKeep re1 re2 p1 p2
 419 |       compileKeep (Alt re1 re2) | (ListC z) | NatC = altTyREKeep re1 re2 p1 p2
 420 |       compileKeep (Alt re1 re2) | (ListC z) | IgnoreC = eitherToMaybeL `map` altTyREKeep re1 re2 p1 p2
 421 |       compileKeep (Alt re1 re2) | NatC | CharC = altTyREKeep re1 re2 p1 p2
 422 |       compileKeep (Alt re1 re2) | NatC | (PairC x y) = altTyREKeep re1 re2 p1 p2
 423 |       compileKeep (Alt re1 re2) | NatC | StringC = altTyREKeep re1 re2 p1 p2
 424 |       compileKeep (Alt re1 re2) | NatC | UnitC = eitherToMaybeL `map` altTyREKeep re1 re2 p1 p2
 425 |       compileKeep (Alt re1 re2) | NatC | (EitherC x y) = altTyREKeep re1 re2 p1 p2
 426 |       compileKeep (Alt re1 re2) | NatC | (MaybeC x) = altTyREKeep re1 re2 p1 p2
 427 |       compileKeep (Alt re1 re2) | NatC | BoolC = altTyREKeep re1 re2 p1 p2
 428 |       compileKeep (Alt re1 re2) | NatC | (ListC z) = altTyREKeep re1 re2 p1 p2
 429 |       compileKeep (Alt re1 re2) | NatC | NatC = altTyREKeep re1 re2 p1 p2
 430 |       compileKeep (Alt re1 re2) | NatC | IgnoreC = eitherToMaybeL `map` altTyREKeep re1 re2 p1 p2
 431 |       compileKeep (Alt re1 re2) | IgnoreC | CharC = eitherToMaybeR `map` altTyREKeep re1 re2 p1 p2
 432 |       compileKeep (Alt re1 re2) | IgnoreC | (PairC x y) = eitherToMaybeR `map` altTyREKeep re1 re2 p1 p2
 433 |       compileKeep (Alt re1 re2) | IgnoreC | StringC = eitherToMaybeR `map` altTyREKeep re1 re2 p1 p2
 434 |       compileKeep (Alt re1 re2) | IgnoreC | UnitC = (isJust . eitherToMaybeR) `map` altTyREKeep re1 re2 p1 p2
 435 |       compileKeep (Alt re1 re2) | IgnoreC | (EitherC x y) = eitherToMaybeR `map` altTyREKeep re1 re2 p1 p2
 436 |       compileKeep (Alt re1 re2) | IgnoreC | (MaybeC x) = eitherToMaybeR `map` altTyREKeep re1 re2 p1 p2
 437 |       compileKeep (Alt re1 re2) | IgnoreC | BoolC = eitherToMaybeR `map` altTyREKeep re1 re2 p1 p2
 438 |       compileKeep (Alt re1 re2) | IgnoreC | (ListC z) = eitherToMaybeR `map` altTyREKeep re1 re2 p1 p2
 439 |       compileKeep (Alt re1 re2) | IgnoreC | NatC = eitherToMaybeR `map` altTyREKeep re1 re2 p1 p2
 440 |       compileKeep (Alt re1 re2) | IgnoreC | IgnoreC = ignore (compileKeep re1 <|> compileKeep re2)
 441 |   compileKeep (Maybe re) with (SimplifyCode (CodeShapeREKeep re)) proof p
 442 |     compileKeep (Maybe re) | CharC = (rewrite p in eitherToMaybeL) `map` compileKeep re <|> Empty
 443 |     compileKeep (Maybe re) | (PairC x y) = (rewrite p in eitherToMaybeL) `map` compileKeep re <|> Empty
 444 |     compileKeep (Maybe re) | StringC = (rewrite p in eitherToMaybeL) `map` compileKeep re <|> Empty
 445 |     compileKeep (Maybe re) | UnitC =
 446 |       let f : Either () () -> Bool
 447 |           f (Left _) = True
 448 |           f (Right _) = False
 449 |       in (rewrite p in f) `map` compileKeep re <|> Empty
 450 |     compileKeep (Maybe re) | (EitherC x y) = (rewrite p in eitherToMaybeL) `map` compileKeep re <|> Empty
 451 |     compileKeep (Maybe re) | (MaybeC x) =
 452 |       let f : Either (Maybe (Sem x)) () -> (Maybe (Sem x))
 453 |           f (Left ms) = ms
 454 |           f (Right _) = Nothing
 455 |       in (rewrite p in f) `map` compileKeep re <|> Empty
 456 |     compileKeep (Maybe re) | BoolC = (rewrite p in eitherToMaybeL) `map` compileKeep re <|> Empty
 457 |     compileKeep (Maybe re) | (ListC z) = (rewrite p in eitherToMaybeL) `map` compileKeep re <|> Empty
 458 |     compileKeep (Maybe re) | NatC = (rewrite p in eitherToMaybeL) `map` compileKeep re <|> Empty
 459 |     compileKeep (Maybe re) | IgnoreC = ignore (option (compileKeep re))
 460 | 
 461 |   compileKeep (Rep0 re) with (SimplifyCode (CodeShapeREKeep re)) proof p
 462 |     compileKeep (Rep0 re) | CharC = replace {p=(TyRE . SnocList . Sem)} p (Rep (compileKeep re))
 463 |     compileKeep (Rep0 re) | (PairC x y) = replace {p=(TyRE . SnocList . Sem)} p (Rep (compileKeep re))
 464 |     compileKeep (Rep0 re) | StringC = replace {p=(TyRE . SnocList . Sem)} p (Rep (compileKeep re))
 465 |     compileKeep (Rep0 re) | UnitC = length `map` Rep (compileKeep re)
 466 |     compileKeep (Rep0 re) | (EitherC x y) = replace {p=(TyRE . SnocList . Sem)} p (Rep (compileKeep re))
 467 |     compileKeep (Rep0 re) | (ListC x) = replace {p=(TyRE . SnocList . Sem)} p (Rep (compileKeep re))
 468 |     compileKeep (Rep0 re) | (MaybeC x) = replace {p=(TyRE . SnocList . Sem)} p (Rep (compileKeep re))
 469 |     compileKeep (Rep0 re) | BoolC = replace {p=(TyRE . SnocList . Sem)} p (Rep (compileKeep re))
 470 |     compileKeep (Rep0 re) | NatC = replace {p=(TyRE . SnocList . Sem)} p (Rep (compileKeep re))
 471 |     compileKeep (Rep0 re) | IgnoreC = ignore (Rep (compileKeep re))
 472 | 
 473 |   compileKeep (Rep1 re) with (SimplifyCode (CodeShapeREKeep re)) proof p
 474 |     compileKeep (Rep1 re) | CharC = 
 475 |       (rewrite p in (\(c,l) => [< c] ++ l)) `map` cre <*> Rep cre where
 476 |         cre : TyRE $ TypeREKeep re
 477 |         cre = compileKeep re
 478 |     compileKeep (Rep1 re) | (PairC x y) =
 479 |       (rewrite p in (\(c,l) => [< c] ++ l)) `map` cre <*> Rep cre where
 480 |         cre : TyRE $ TypeREKeep re
 481 |         cre = compileKeep re
 482 |     compileKeep (Rep1 re) | StringC =
 483 |       (rewrite p in (\(c,l) => [< c] ++ l)) `map` cre <*> Rep cre where
 484 |         cre : TyRE $ TypeREKeep re
 485 |         cre = compileKeep re
 486 |     compileKeep (Rep1 re) | UnitC =
 487 |       (\(_,l) => length l + 1) `map` cre <*> Rep cre where
 488 |         cre : TyRE $ TypeREKeep re
 489 |         cre = compileKeep re
 490 |     compileKeep (Rep1 re) | (EitherC x y) =
 491 |       (rewrite p in (\(c,l) => [< c] ++ l)) `map` cre <*> Rep cre where
 492 |         cre : TyRE $ TypeREKeep re
 493 |         cre = compileKeep re
 494 |     compileKeep (Rep1 re) | (ListC x) =
 495 |       (rewrite p in (\(c,l) => [< c] ++ l)) `map` cre <*> Rep cre where
 496 |         cre : TyRE $ TypeREKeep re
 497 |         cre = compileKeep re
 498 |     compileKeep (Rep1 re) | (MaybeC x) =
 499 |       (rewrite p in (\(c,l) => [< c] ++ l)) `map` cre <*> Rep cre where
 500 |         cre : TyRE $ TypeREKeep re
 501 |         cre = compileKeep re
 502 |     compileKeep (Rep1 re) | BoolC =
 503 |       (rewrite p in (\(c,l) => [< c] ++ l)) `map` cre <*> Rep cre where
 504 |         cre : TyRE $ TypeREKeep re
 505 |         cre = compileKeep re
 506 |     compileKeep (Rep1 re) | NatC =
 507 |       (rewrite p in (\(c,l) => [< c] ++ l)) `map` cre <*> Rep cre where
 508 |         cre : TyRE $ TypeREKeep re
 509 |         cre = compileKeep re
 510 |     compileKeep (Rep1 re) | IgnoreC = ignore (rep1 (compileKeep re))
 511 |   compileKeep (Keep re) = compileKeep re
 512 | 
 513 | mutual
 514 |   public export
 515 |   altTyRE : (re1 : RE) -> (re2 : RE)
 516 |           -> ((SimplifyCode (CodeShapeRE re1)) = a)
 517 |           -> ((SimplifyCode (CodeShapeRE re2)) = b)
 518 |           -> TyRE $ Either (Sem a) (Sem b)
 519 |   altTyRE re1 re2 Refl Refl = compile re1 <|> compile re2
 520 | 
 521 |   public export
 522 |   concatTyRE : (re1 : RE) -> (re2 : RE) -> TyRE (TypeRE re1, TypeRE re2)
 523 |   concatTyRE re1 re2 = compile re1 <*> compile re2
 524 | 
 525 |   public export
 526 |   compile                  : (re : RE) -> TyRE $ TypeRE re
 527 |   compile (Exactly x)      = match x
 528 |   compile (OneOf xs)       = ignore (oneOfCharsList xs)
 529 |   compile (To x y)         = ignore (range x y)
 530 |   compile Any              = ignore any
 531 |   compile (Group re)       = Group $ compile re
 532 |   compile (Concat re1 re2) with (SimplifyCode (CodeShapeRE re1), SimplifyCode (CodeShapeRE re2)) proof p
 533 |     compile (Concat re1 re2) | (CharC, CharC) = concatTyRE re1 re2
 534 |     compile (Concat re1 re2) | (CharC, (PairC x y)) = concatTyRE re1 re2
 535 |     compile (Concat re1 re2) | (CharC, StringC) = concatTyRE re1 re2
 536 |     compile (Concat re1 re2) | (CharC, UnitC) =
 537 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 538 |       $ compile re1 <* (compile re2)
 539 |     compile (Concat re1 re2) | (CharC, (EitherC x y)) = concatTyRE re1 re2
 540 |     compile (Concat re1 re2) | (CharC, (MaybeC x)) = concatTyRE re1 re2
 541 |     compile (Concat re1 re2) | (CharC, BoolC) = concatTyRE re1 re2
 542 |     compile (Concat re1 re2) | (CharC, (ListC z)) = concatTyRE re1 re2
 543 |     compile (Concat re1 re2) | (CharC, NatC) = concatTyRE re1 re2
 544 |     compile (Concat re1 re2) | (CharC, IgnoreC) = 
 545 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 546 |       $ compile re1 <* (compile re2)
 547 |     compile (Concat re1 re2) | ((PairC x y), CharC) = concatTyRE re1 re2
 548 |     compile (Concat re1 re2) | ((PairC x y), (PairC z w)) = concatTyRE re1 re2
 549 |     compile (Concat re1 re2) | ((PairC x y), StringC) = concatTyRE re1 re2
 550 |     compile (Concat re1 re2) | ((PairC x y), UnitC) =
 551 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 552 |       $ compile re1 <* (compile re2)
 553 |     compile (Concat re1 re2) | ((PairC x y), (EitherC z w)) = concatTyRE re1 re2
 554 |     compile (Concat re1 re2) | ((PairC x y), (MaybeC z)) = concatTyRE re1 re2
 555 |     compile (Concat re1 re2) | ((PairC x y), BoolC) = concatTyRE re1 re2
 556 |     compile (Concat re1 re2) | ((PairC x y), (ListC z)) = concatTyRE re1 re2
 557 |     compile (Concat re1 re2) | ((PairC x y), NatC) = concatTyRE re1 re2
 558 |     compile (Concat re1 re2) | ((PairC x y), IgnoreC) = 
 559 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 560 |       $ compile re1 <* (compile re2)
 561 |     compile (Concat re1 re2) | (StringC, CharC) = concatTyRE re1 re2
 562 |     compile (Concat re1 re2) | (StringC, (PairC x y)) = concatTyRE re1 re2
 563 |     compile (Concat re1 re2) | (StringC, StringC) = concatTyRE re1 re2
 564 |     compile (Concat re1 re2) | (StringC, UnitC) =
 565 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 566 |       $ compile re1 <* (compile re2)
 567 |     compile (Concat re1 re2) | (StringC, (EitherC x y)) = concatTyRE re1 re2
 568 |     compile (Concat re1 re2) | (StringC, (MaybeC x)) = concatTyRE re1 re2
 569 |     compile (Concat re1 re2) | (StringC, BoolC) = concatTyRE re1 re2
 570 |     compile (Concat re1 re2) | (StringC, (ListC z)) = concatTyRE re1 re2
 571 |     compile (Concat re1 re2) | (StringC, NatC) = concatTyRE re1 re2
 572 |     compile (Concat re1 re2) | (StringC, IgnoreC) =
 573 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 574 |       $ compile re1 <* (compile re2)
 575 |     compile (Concat re1 re2) | (UnitC, CharC) =
 576 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 577 |       $ compile re1 *> (compile re2)
 578 |     compile (Concat re1 re2) | (UnitC, (PairC x y)) =
 579 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 580 |       $ compile re1 *> (compile re2)
 581 |     compile (Concat re1 re2) | (UnitC, StringC) =
 582 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 583 |       $ compile re1 *> (compile re2)
 584 |     compile (Concat re1 re2) | (UnitC, UnitC) = ignore (concatTyRE re1 re2)
 585 |     compile (Concat re1 re2) | (UnitC, (EitherC x y)) =
 586 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 587 |       $ compile re1 *> (compile re2)
 588 |     compile (Concat re1 re2) | (UnitC, (MaybeC x)) =
 589 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 590 |       $ compile re1 *> (compile re2)
 591 |     compile (Concat re1 re2) | (UnitC, BoolC) =
 592 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 593 |       $ compile re1 *> (compile re2)
 594 |     compile (Concat re1 re2) | (UnitC, (ListC z)) =
 595 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 596 |       $ compile re1 *> (compile re2)
 597 |     compile (Concat re1 re2) | (UnitC, NatC) =
 598 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 599 |       $ compile re1 *> (compile re2)
 600 |     compile (Concat re1 re2) | (UnitC, IgnoreC) = ignore (concatTyRE re1 re2)
 601 |     compile (Concat re1 re2) | ((EitherC x y), CharC) = concatTyRE re1 re2
 602 |     compile (Concat re1 re2) | ((EitherC x y), (PairC z w)) = concatTyRE re1 re2
 603 |     compile (Concat re1 re2) | ((EitherC x y), StringC) = concatTyRE re1 re2
 604 |     compile (Concat re1 re2) | ((EitherC x y), UnitC) =
 605 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 606 |       $ compile re1 <* (compile re2)
 607 |     compile (Concat re1 re2) | ((EitherC x y), (EitherC z w)) = concatTyRE re1 re2
 608 |     compile (Concat re1 re2) | ((EitherC x y), (MaybeC z)) = concatTyRE re1 re2
 609 |     compile (Concat re1 re2) | ((EitherC x y), BoolC) = concatTyRE re1 re2
 610 |     compile (Concat re1 re2) | ((EitherC x y), (ListC z)) = concatTyRE re1 re2
 611 |     compile (Concat re1 re2) | ((EitherC x y), NatC) = concatTyRE re1 re2
 612 |     compile (Concat re1 re2) | ((EitherC x y), IgnoreC) =
 613 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 614 |       $ compile re1 <* (compile re2)
 615 |     compile (Concat re1 re2) | ((MaybeC x), CharC) = concatTyRE re1 re2
 616 |     compile (Concat re1 re2) | ((MaybeC x), (PairC y z)) = concatTyRE re1 re2
 617 |     compile (Concat re1 re2) | ((MaybeC x), StringC) = concatTyRE re1 re2
 618 |     compile (Concat re1 re2) | ((MaybeC x), UnitC) =
 619 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 620 |       $ compile re1 <* compile re2
 621 |     compile (Concat re1 re2) | ((MaybeC x), (EitherC y z)) = concatTyRE re1 re2
 622 |     compile (Concat re1 re2) | ((MaybeC x), (MaybeC y)) = concatTyRE re1 re2
 623 |     compile (Concat re1 re2) | ((MaybeC x), BoolC) = concatTyRE re1 re2
 624 |     compile (Concat re1 re2) | ((MaybeC x), (ListC z)) = concatTyRE re1 re2
 625 |     compile (Concat re1 re2) | ((MaybeC x), NatC) = concatTyRE re1 re2
 626 |     compile (Concat re1 re2) | ((MaybeC x), IgnoreC) = 
 627 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 628 |       $ compile re1 <* compile re2
 629 |     compile (Concat re1 re2) | (BoolC, CharC) = concatTyRE re1 re2
 630 |     compile (Concat re1 re2) | (BoolC, (PairC x y)) = concatTyRE re1 re2
 631 |     compile (Concat re1 re2) | (BoolC, StringC) = concatTyRE re1 re2
 632 |     compile (Concat re1 re2) | (BoolC, UnitC) =
 633 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 634 |       $ compile re1 <* compile re2
 635 |     compile (Concat re1 re2) | (BoolC, (EitherC x y)) = concatTyRE re1 re2
 636 |     compile (Concat re1 re2) | (BoolC, (MaybeC x)) = concatTyRE re1 re2
 637 |     compile (Concat re1 re2) | (BoolC, BoolC) = concatTyRE re1 re2
 638 |     compile (Concat re1 re2) | (BoolC, (ListC z)) = concatTyRE re1 re2
 639 |     compile (Concat re1 re2) | (BoolC, NatC) = concatTyRE re1 re2
 640 |     compile (Concat re1 re2) | (BoolC, IgnoreC) = 
 641 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 642 |       $ compile re1 <* compile re2
 643 |     compile (Concat re1 re2) | ((ListC z), CharC) = concatTyRE re1 re2
 644 |     compile (Concat re1 re2) | ((ListC z), (PairC x y)) = concatTyRE re1 re2
 645 |     compile (Concat re1 re2) | ((ListC z), StringC) = concatTyRE re1 re2
 646 |     compile (Concat re1 re2) | ((ListC z), UnitC) =
 647 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 648 |       $ compile re1 <* compile re2
 649 |     compile (Concat re1 re2) | ((ListC z), (EitherC x y)) = concatTyRE re1 re2
 650 |     compile (Concat re1 re2) | ((ListC z), (MaybeC x)) = concatTyRE re1 re2
 651 |     compile (Concat re1 re2) | ((ListC z), BoolC) = concatTyRE re1 re2
 652 |     compile (Concat re1 re2) | ((ListC z), (ListC x)) = concatTyRE re1 re2
 653 |     compile (Concat re1 re2) | ((ListC z), NatC) = concatTyRE re1 re2
 654 |     compile (Concat re1 re2) | ((ListC z), IgnoreC) = 
 655 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 656 |       $ compile re1 <* (compile re2)
 657 |     compile (Concat re1 re2) | (NatC, CharC) = concatTyRE re1 re2
 658 |     compile (Concat re1 re2) | (NatC, (PairC x y)) = concatTyRE re1 re2
 659 |     compile (Concat re1 re2) | (NatC, StringC) = concatTyRE re1 re2
 660 |     compile (Concat re1 re2) | (NatC, UnitC) =
 661 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 662 |       $ compile re1 <* compile re2
 663 |     compile (Concat re1 re2) | (NatC, (EitherC x y)) = concatTyRE re1 re2
 664 |     compile (Concat re1 re2) | (NatC, (MaybeC x)) = concatTyRE re1 re2
 665 |     compile (Concat re1 re2) | (NatC, BoolC) = concatTyRE re1 re2
 666 |     compile (Concat re1 re2) | (NatC, (ListC z)) = concatTyRE re1 re2
 667 |     compile (Concat re1 re2) | (NatC, NatC) = concatTyRE re1 re2
 668 |     compile (Concat re1 re2) | (NatC, IgnoreC) = 
 669 |       replace {p = (\s => TyRE (Sem s))} (fst $ pairEq p) 
 670 |       $ compile re1 <* compile re2
 671 |     compile (Concat re1 re2) | (IgnoreC, CharC) = 
 672 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 673 |       $ compile re1 *> compile re2
 674 |     compile (Concat re1 re2) | (IgnoreC, (PairC x y)) = 
 675 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 676 |       $ compile re1 *> compile re2
 677 |     compile (Concat re1 re2) | (IgnoreC, StringC) = 
 678 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 679 |       $ compile re1 *> compile re2
 680 |     compile (Concat re1 re2) | (IgnoreC, UnitC) = ignore (compile re1 <*> compile re2)
 681 |     compile (Concat re1 re2) | (IgnoreC, (EitherC x y)) = 
 682 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 683 |       $ compile re1 *> compile re2
 684 |     compile (Concat re1 re2) | (IgnoreC, (MaybeC x)) = 
 685 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 686 |       $ compile re1 *> compile re2
 687 |     compile (Concat re1 re2) | (IgnoreC, BoolC) =
 688 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 689 |       $ compile re1 *> compile re2
 690 |     compile (Concat re1 re2) | (IgnoreC, (ListC z)) =
 691 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 692 |       $ compile re1 *> compile re2
 693 |     compile (Concat re1 re2) | (IgnoreC, NatC) =
 694 |       replace {p = (\s => TyRE (Sem s))} (snd $ pairEq p) 
 695 |       $ compile re1 *> compile re2
 696 |     compile (Concat re1 re2) | (IgnoreC, IgnoreC) = ignore (compile re1 <*> compile re2)
 697 | 
 698 |   compile (Alt re1 re2) with (SimplifyCode (CodeShapeRE re1)) proof p1
 699 |     compile (Alt re1 re2) | sc1 with (SimplifyCode (CodeShapeRE re2)) proof p2
 700 |       compile (Alt re1 re2) | CharC | CharC = altTyRE re1 re2 p1 p2
 701 |       compile (Alt re1 re2) | CharC | (PairC x y) = altTyRE re1 re2 p1 p2
 702 |       compile (Alt re1 re2) | CharC | StringC = altTyRE re1 re2 p1 p2
 703 |       compile (Alt re1 re2) | CharC | UnitC = eitherToMaybeL `map` altTyRE re1 re2 p1 p2
 704 |       compile (Alt re1 re2) | CharC | (EitherC x y) = altTyRE re1 re2 p1 p2
 705 |       compile (Alt re1 re2) | CharC | (MaybeC x) = altTyRE re1 re2 p1 p2
 706 |       compile (Alt re1 re2) | CharC | BoolC = altTyRE re1 re2 p1 p2
 707 |       compile (Alt re1 re2) | CharC | (ListC x) = altTyRE re1 re2 p1 p2
 708 |       compile (Alt re1 re2) | CharC | NatC = altTyRE re1 re2 p1 p2
 709 |       compile (Alt re1 re2) | CharC | IgnoreC = eitherToMaybeL `map` altTyRE re1 re2 p1 p2
 710 |       compile (Alt re1 re2) | (PairC x y) | CharC = altTyRE re1 re2 p1 p2
 711 |       compile (Alt re1 re2) | (PairC x y) | (PairC z w) = altTyRE re1 re2 p1 p2
 712 |       compile (Alt re1 re2) | (PairC x y) | StringC = altTyRE re1 re2 p1 p2
 713 |       compile (Alt re1 re2) | (PairC x y) | UnitC = eitherToMaybeL `map` altTyRE re1 re2 p1 p2
 714 |       compile (Alt re1 re2) | (PairC x y) | (EitherC z w) = altTyRE re1 re2 p1 p2
 715 |       compile (Alt re1 re2) | (PairC x y) | (MaybeC z) = altTyRE re1 re2 p1 p2
 716 |       compile (Alt re1 re2) | (PairC x y) | BoolC = altTyRE re1 re2 p1 p2
 717 |       compile (Alt re1 re2) | (PairC x y) | (ListC z) = altTyRE re1 re2 p1 p2
 718 |       compile (Alt re1 re2) | (PairC x y) | NatC = altTyRE re1 re2 p1 p2
 719 |       compile (Alt re1 re2) | (PairC x y) | IgnoreC = eitherToMaybeL `map` altTyRE re1 re2 p1 p2
 720 |       compile (Alt re1 re2) | StringC | CharC = altTyRE re1 re2 p1 p2
 721 |       compile (Alt re1 re2) | StringC | (PairC x y) = altTyRE re1 re2 p1 p2
 722 |       compile (Alt re1 re2) | StringC | StringC = altTyRE re1 re2 p1 p2
 723 |       compile (Alt re1 re2) | StringC | UnitC = eitherToMaybeL `map` altTyRE re1 re2 p1 p2
 724 |       compile (Alt re1 re2) | StringC | (EitherC x y) = altTyRE re1 re2 p1 p2
 725 |       compile (Alt re1 re2) | StringC | (MaybeC x) = altTyRE re1 re2 p1 p2
 726 |       compile (Alt re1 re2) | StringC | BoolC = altTyRE re1 re2 p1 p2
 727 |       compile (Alt re1 re2) | StringC | (ListC x) = altTyRE re1 re2 p1 p2
 728 |       compile (Alt re1 re2) | StringC | NatC = altTyRE re1 re2 p1 p2
 729 |       compile (Alt re1 re2) | StringC | IgnoreC = eitherToMaybeL `map` altTyRE re1 re2 p1 p2
 730 |       compile (Alt re1 re2) | UnitC | CharC = eitherToMaybeR `map` altTyRE re1 re2 p1 p2
 731 |       compile (Alt re1 re2) | UnitC | (PairC x y) = eitherToMaybeR `map` altTyRE re1 re2 p1 p2
 732 |       compile (Alt re1 re2) | UnitC | StringC = eitherToMaybeR `map` altTyRE re1 re2 p1 p2
 733 |       compile (Alt re1 re2) | UnitC | UnitC =
 734 |         let f : Either () () -> Bool
 735 |             f (Left _) = True
 736 |             f (Right _) = False
 737 |         in f `map` altTyRE re1 re2 p1 p2
 738 |       compile (Alt re1 re2) | UnitC | (EitherC x y) = eitherToMaybeR `map` altTyRE re1 re2 p1 p2
 739 |       compile (Alt re1 re2) | UnitC | (MaybeC x) = eitherToMaybeR `map` altTyRE re1 re2 p1 p2
 740 |       compile (Alt re1 re2) | UnitC | BoolC = eitherToMaybeR `map` altTyRE re1 re2 p1 p2
 741 |       compile (Alt re1 re2) | UnitC | (ListC x) = eitherToMaybeR `map` altTyRE re1 re2 p1 p2
 742 |       compile (Alt re1 re2) | UnitC | NatC = eitherToMaybeR `map` altTyRE re1 re2 p1 p2
 743 |       compile (Alt re1 re2) | UnitC | IgnoreC = (isJust . eitherToMaybeL) `map` altTyRE re1 re2 p1 p2
 744 |       compile (Alt re1 re2) | (EitherC x y) | CharC = altTyRE re1 re2 p1 p2
 745 |       compile (Alt re1 re2) | (EitherC x y) | (PairC z w) = altTyRE re1 re2 p1 p2
 746 |       compile (Alt re1 re2) | (EitherC x y) | StringC = altTyRE re1 re2 p1 p2
 747 |       compile (Alt re1 re2) | (EitherC x y) | UnitC = eitherToMaybeL `map` altTyRE re1 re2 p1 p2
 748 |       compile (Alt re1 re2) | (EitherC x y) | (EitherC z w) = altTyRE re1 re2 p1 p2
 749 |       compile (Alt re1 re2) | (EitherC x y) | (MaybeC z) = altTyRE re1 re2 p1 p2
 750 |       compile (Alt re1 re2) | (EitherC x y) | BoolC = altTyRE re1 re2 p1 p2
 751 |       compile (Alt re1 re2) | (EitherC x y) | (ListC z) = altTyRE re1 re2 p1 p2
 752 |       compile (Alt re1 re2) | (EitherC x y) | NatC = altTyRE re1 re2 p1 p2
 753 |       compile (Alt re1 re2) | (EitherC x y) | IgnoreC = eitherToMaybeL `map` altTyRE re1 re2 p1 p2
 754 |       compile (Alt re1 re2) | (MaybeC x) | CharC = altTyRE re1 re2 p1 p2
 755 |       compile (Alt re1 re2) | (MaybeC x) | (PairC y z) = altTyRE re1 re2 p1 p2
 756 |       compile (Alt re1 re2) | (MaybeC x) | StringC = altTyRE re1 re2 p1 p2
 757 |       compile (Alt re1 re2) | (MaybeC x) | UnitC = eitherToMaybeL `map` altTyRE re1 re2 p1 p2
 758 |       compile (Alt re1 re2) | (MaybeC x) | (EitherC y z) = altTyRE re1 re2 p1 p2
 759 |       compile (Alt re1 re2) | (MaybeC x) | (MaybeC y) = altTyRE re1 re2 p1 p2
 760 |       compile (Alt re1 re2) | (MaybeC x) | BoolC = altTyRE re1 re2 p1 p2
 761 |       compile (Alt re1 re2) | (MaybeC x) | (ListC z) = altTyRE re1 re2 p1 p2
 762 |       compile (Alt re1 re2) | (MaybeC x) | NatC = altTyRE re1 re2 p1 p2
 763 |       compile (Alt re1 re2) | (MaybeC x) | IgnoreC = eitherToMaybeL `map` altTyRE re1 re2 p1 p2
 764 |       compile (Alt re1 re2) | BoolC | CharC = altTyRE re1 re2 p1 p2
 765 |       compile (Alt re1 re2) | BoolC | (PairC x y) = altTyRE re1 re2 p1 p2
 766 |       compile (Alt re1 re2) | BoolC | StringC = altTyRE re1 re2 p1 p2
 767 |       compile (Alt re1 re2) | BoolC | UnitC = eitherToMaybeL `map` altTyRE re1 re2 p1 p2
 768 |       compile (Alt re1 re2) | BoolC | (EitherC x y) = altTyRE re1 re2 p1 p2
 769 |       compile (Alt re1 re2) | BoolC | (MaybeC x) = altTyRE re1 re2 p1 p2
 770 |       compile (Alt re1 re2) | BoolC | BoolC = altTyRE re1 re2 p1 p2
 771 |       compile (Alt re1 re2) | BoolC | (ListC z) = altTyRE re1 re2 p1 p2
 772 |       compile (Alt re1 re2) | BoolC | NatC = altTyRE re1 re2 p1 p2
 773 |       compile (Alt re1 re2) | BoolC | IgnoreC = eitherToMaybeL `map` altTyRE re1 re2 p1 p2
 774 |       compile (Alt re1 re2) | (ListC z) | CharC = altTyRE re1 re2 p1 p2
 775 |       compile (Alt re1 re2) | (ListC z) | (PairC x y) = altTyRE re1 re2 p1 p2
 776 |       compile (Alt re1 re2) | (ListC z) | StringC = altTyRE re1 re2 p1 p2
 777 |       compile (Alt re1 re2) | (ListC z) | UnitC = eitherToMaybeL `map` altTyRE re1 re2 p1 p2
 778 |       compile (Alt re1 re2) | (ListC z) | (EitherC x y) = altTyRE re1 re2 p1 p2
 779 |       compile (Alt re1 re2) | (ListC z) | (MaybeC x) = altTyRE re1 re2 p1 p2
 780 |       compile (Alt re1 re2) | (ListC z) | BoolC = altTyRE re1 re2 p1 p2
 781 |       compile (Alt re1 re2) | (ListC z) | (ListC x) = altTyRE re1 re2 p1 p2
 782 |       compile (Alt re1 re2) | (ListC z) | NatC = altTyRE re1 re2 p1 p2
 783 |       compile (Alt re1 re2) | (ListC z) | IgnoreC = eitherToMaybeL `map` altTyRE re1 re2 p1 p2
 784 |       compile (Alt re1 re2) | NatC | CharC = altTyRE re1 re2 p1 p2
 785 |       compile (Alt re1 re2) | NatC | (PairC x y) = altTyRE re1 re2 p1 p2
 786 |       compile (Alt re1 re2) | NatC | StringC = altTyRE re1 re2 p1 p2
 787 |       compile (Alt re1 re2) | NatC | UnitC = eitherToMaybeL `map` altTyRE re1 re2 p1 p2
 788 |       compile (Alt re1 re2) | NatC | (EitherC x y) = altTyRE re1 re2 p1 p2
 789 |       compile (Alt re1 re2) | NatC | (MaybeC x) = altTyRE re1 re2 p1 p2
 790 |       compile (Alt re1 re2) | NatC | BoolC = altTyRE re1 re2 p1 p2
 791 |       compile (Alt re1 re2) | NatC | (ListC z) = altTyRE re1 re2 p1 p2
 792 |       compile (Alt re1 re2) | NatC | NatC = altTyRE re1 re2 p1 p2
 793 |       compile (Alt re1 re2) | NatC | IgnoreC = eitherToMaybeL `map` altTyRE re1 re2 p1 p2
 794 |       compile (Alt re1 re2) | IgnoreC | CharC = eitherToMaybeR `map` altTyRE re1 re2 p1 p2
 795 |       compile (Alt re1 re2) | IgnoreC | (PairC x y) = eitherToMaybeR `map` altTyRE re1 re2 p1 p2
 796 |       compile (Alt re1 re2) | IgnoreC | StringC = eitherToMaybeR `map` altTyRE re1 re2 p1 p2
 797 |       compile (Alt re1 re2) | IgnoreC | UnitC = (isJust . eitherToMaybeR) `map` altTyRE re1 re2 p1 p2
 798 |       compile (Alt re1 re2) | IgnoreC | (EitherC x y) = eitherToMaybeR `map` altTyRE re1 re2 p1 p2
 799 |       compile (Alt re1 re2) | IgnoreC | (MaybeC x) = eitherToMaybeR `map` altTyRE re1 re2 p1 p2
 800 |       compile (Alt re1 re2) | IgnoreC | BoolC = eitherToMaybeR `map` altTyRE re1 re2 p1 p2
 801 |       compile (Alt re1 re2) | IgnoreC | (ListC z) = eitherToMaybeR `map` altTyRE re1 re2 p1 p2
 802 |       compile (Alt re1 re2) | IgnoreC | NatC = eitherToMaybeR `map` altTyRE re1 re2 p1 p2
 803 |       compile (Alt re1 re2) | IgnoreC | IgnoreC = ignore (compile re1 <|> compile re2)
 804 |   compile (Maybe re) with (SimplifyCode (CodeShapeRE re)) proof p
 805 |     compile (Maybe re) | CharC = (rewrite p in eitherToMaybeL) `map` compile re <|> Empty
 806 |     compile (Maybe re) | (PairC x y) = (rewrite p in eitherToMaybeL) `map` compile re <|> Empty
 807 |     compile (Maybe re) | StringC = (rewrite p in eitherToMaybeL) `map` compile re <|> Empty
 808 |     compile (Maybe re) | UnitC =
 809 |       let f : Either () () -> Bool
 810 |           f (Left _) = True
 811 |           f (Right _) = False
 812 |       in (rewrite p in f) `map` compile re <|> Empty
 813 |     compile (Maybe re) | (EitherC x y) = (rewrite p in eitherToMaybeL) `map` compile re <|> Empty
 814 |     compile (Maybe re) | (MaybeC x) =
 815 |       let f : Either (Maybe (Sem x)) () -> (Maybe (Sem x))
 816 |           f (Left ms) = ms
 817 |           f (Right _) = Nothing
 818 |       in (rewrite p in f) `map` compile re <|> Empty
 819 |     compile (Maybe re) | BoolC = (rewrite p in eitherToMaybeL) `map` compile re <|> Empty
 820 |     compile (Maybe re) | (ListC z) = (rewrite p in eitherToMaybeL) `map` compile re <|> Empty
 821 |     compile (Maybe re) | NatC = (rewrite p in eitherToMaybeL) `map` compile re <|> Empty
 822 |     compile (Maybe re) | IgnoreC = ignore (option (compile re))
 823 | 
 824 |   compile (Rep0 re) with (SimplifyCode (CodeShapeRE re)) proof p
 825 |     compile (Rep0 re) | CharC = replace {p=(TyRE . SnocList . Sem)} p (Rep (compile re))
 826 |     compile (Rep0 re) | (PairC x y) = replace {p=(TyRE . SnocList . Sem)} p (Rep (compile re))
 827 |     compile (Rep0 re) | StringC = replace {p=(TyRE . SnocList . Sem)} p (Rep (compile re))
 828 |     compile (Rep0 re) | UnitC = length `map` Rep (compile re)
 829 |     compile (Rep0 re) | (EitherC x y) = replace {p=(TyRE . SnocList . Sem)} p (Rep (compile re))
 830 |     compile (Rep0 re) | (ListC x) = replace {p=(TyRE . SnocList . Sem)} p (Rep (compile re))
 831 |     compile (Rep0 re) | (MaybeC x) = replace {p=(TyRE . SnocList . Sem)} p (Rep (compile re))
 832 |     compile (Rep0 re) | BoolC = replace {p=(TyRE . SnocList . Sem)} p (Rep (compile re))
 833 |     compile (Rep0 re) | NatC = replace {p=(TyRE . SnocList . Sem)} p (Rep (compile re))
 834 |     compile (Rep0 re) | IgnoreC = ignore (Rep (compile re))
 835 | 
 836 |   compile (Rep1 re) with (SimplifyCode (CodeShapeRE re)) proof p
 837 |     compile (Rep1 re) | CharC =
 838 |       (rewrite p in (\(c,l) => [< c] ++ l)) `map` cre <*> Rep cre where
 839 |         cre : TyRE $ TypeRE re
 840 |         cre = compile re
 841 |     compile (Rep1 re) | (PairC x y) =
 842 |       (rewrite p in (\(c,l) => [< c] ++ l)) `map` cre <*> Rep cre where
 843 |         cre : TyRE $ TypeRE re
 844 |         cre = compile re
 845 |     compile (Rep1 re) | StringC =
 846 |       (rewrite p in (\(c,l) => [< c] ++ l)) `map` cre <*> Rep cre where
 847 |         cre : TyRE $ TypeRE re
 848 |         cre = compile re
 849 |     compile (Rep1 re) | UnitC =
 850 |       (\(_,l) => length l + 1) `map` cre <*> Rep cre where
 851 |         cre : TyRE $ TypeRE re
 852 |         cre = compile re
 853 |     compile (Rep1 re) | (EitherC x y) =
 854 |       (rewrite p in (\(c,l) => [< c] ++ l)) `map` cre <*> Rep cre where
 855 |         cre : TyRE $ TypeRE re
 856 |         cre = compile re
 857 |     compile (Rep1 re) | (ListC x) =
 858 |       (rewrite p in (\(c,l) => [< c] ++ l)) `map` cre <*> Rep cre where
 859 |         cre : TyRE $ TypeRE re
 860 |         cre = compile re
 861 |     compile (Rep1 re) | (MaybeC x) =
 862 |       (rewrite p in (\(c,l) => [< c] ++ l)) `map` cre <*> Rep cre where
 863 |         cre : TyRE $ TypeRE re
 864 |         cre = compile re
 865 |     compile (Rep1 re) | BoolC =
 866 |       (rewrite p in (\(c,l) => [< c] ++ l)) `map` cre <*> Rep cre where
 867 |         cre : TyRE $ TypeRE re
 868 |         cre = compile re
 869 |     compile (Rep1 re) | NatC =
 870 |       (rewrite p in (\(c,l) => [< c] ++ l)) `map` cre <*> Rep cre where
 871 |         cre : TyRE $ TypeRE re
 872 |         cre = compile re
 873 |     compile (Rep1 re) | IgnoreC = ignore (rep1 (compile re))
 874 |   compile (Keep re) = compileKeep re
 875 |