Language.Reflection.TT


   0 | module Language.Reflection.TT
   1 | 
   2 | import public Data.List
   3 | import public Data.String
   4 | 
   5 | import Decidable.Equality
   6 | 
   7 | %default total
   8 | ||| namespace, stored in reverse order
   9 | public export
  10 | data Namespace = MkNS (List String)
  11 | 
  12 | export
  13 | isParentOf : (given, candidate : Namespace) -> Bool
  14 | isParentOf (MkNS ms) (MkNS ns) = List.isSuffixOf ms ns
  15 | 
  16 | %name Namespace ns
  17 | ||| module identifier, stored in reverse order
  18 | public export
  19 | data ModuleIdent = MkMI (List String)
  20 | 
  21 | %name ModuleIdent mi
  22 | 
  23 | export
  24 | showSep : String -> List String -> String
  25 | showSep sep [] = ""
  26 | showSep sep [x] = x
  27 | showSep sep (x :: xs) = x ++ sep ++ showSep sep xs
  28 | 
  29 | export
  30 | Show Namespace where
  31 |   show (MkNS ns) = showSep "." (reverse ns)
  32 | 
  33 | ||| 'FilePos' represents the position of
  34 | ||| the source information in the file (or REPL).
  35 | ||| in the form of '(line-no, column-no)'.
  36 | public export
  37 | FilePos : Type
  38 | FilePos = (Int, Int)
  39 | 
  40 | public export
  41 | data VirtualIdent : Type where
  42 |   Interactive : VirtualIdent
  43 | 
  44 | public export
  45 | data OriginDesc : Type where
  46 |   ||| Anything that originates in physical Idris source files is assigned a
  47 |   ||| `PhysicalIdrSrc modIdent`,
  48 |   |||   where `modIdent` is the top-level module identifier of that file.
  49 |   PhysicalIdrSrc : (ident : ModuleIdent) -> OriginDesc
  50 |   ||| Anything parsed from a package file is decorated with `PhysicalPkgSrc fname`,
  51 |   |||   where `fname` is path to the package file.
  52 |   PhysicalPkgSrc : (fname : String) -> OriginDesc
  53 |   Virtual : (ident : VirtualIdent) -> OriginDesc
  54 | 
  55 | %name OriginDesc origin
  56 | 
  57 | ||| A file context is a filename together with starting and ending positions.
  58 | ||| It's often carried by AST nodes that might have been created from a source
  59 | ||| file or by the compiler. That makes it useful to have the notion of
  60 | ||| `EmptyFC` as part of the type.
  61 | public export
  62 | data FC = MkFC        OriginDesc FilePos FilePos
  63 |         | ||| Virtual FCs are FC attached to desugared/generated code. They can help with marking
  64 |           ||| errors, but we shouldn't attach semantic highlighting metadata to them.
  65 |           MkVirtualFC OriginDesc FilePos FilePos
  66 |         | EmptyFC
  67 | 
  68 | %name FC fc
  69 | 
  70 | public export
  71 | emptyFC : FC
  72 | emptyFC = EmptyFC
  73 | 
  74 | ------------------------------------------------------------------------
  75 | ||| A wrapper for a value with a file context.
  76 | public export
  77 | record WithFC (ty : Type) where
  78 |   constructor MkFCVal
  79 |   fc : FC
  80 |   value : ty
  81 | 
  82 | ||| Smart constructor for WithFC that uses EmptyFC as location
  83 | %inline export
  84 | NoFC : a -> WithFC a
  85 | NoFC = MkFCVal EmptyFC
  86 | 
  87 | export
  88 | Functor WithFC where
  89 |   map f = { value $= f}
  90 | 
  91 | export
  92 | Foldable WithFC where
  93 |   foldr f i v = f v.value i
  94 | 
  95 | export
  96 | Traversable WithFC where
  97 |   traverse f (MkFCVal fc val) = map (MkFCVal fc) (f val)
  98 | 
  99 | ||| Locations are not taken into account when comparing reflected trees
 100 | export
 101 | Eq a => Eq (WithFC a) where
 102 |   x == y = x.value == y.value
 103 | 
 104 | ||| Locations are not taken into account when comparing reflected trees
 105 | export
 106 | Ord a => Ord (WithFC a) where
 107 |   compare x y = compare x.value y.value
 108 | 
 109 | public export
 110 | data NameType : Type where
 111 |      Bound   : NameType
 112 |      Func    : NameType
 113 |      DataCon : (tag : Int) -> (arity : Nat) -> NameType
 114 |      TyCon   : (tag : Int) -> (arity : Nat) -> NameType
 115 |                -- TODO: remove type tag, it's is always 0
 116 | 
 117 | %name NameType nty
 118 | 
 119 | public export
 120 | data PrimType
 121 |     = IntType
 122 |     | IntegerType
 123 |     | Int8Type
 124 |     | Int16Type
 125 |     | Int32Type
 126 |     | Int64Type
 127 |     | Bits8Type
 128 |     | Bits16Type
 129 |     | Bits32Type
 130 |     | Bits64Type
 131 |     | StringType
 132 |     | CharType
 133 |     | DoubleType
 134 |     | WorldType
 135 | 
 136 | %name PrimType pty
 137 | 
 138 | public export
 139 | data Constant
 140 |     = I Int
 141 |     | BI Integer
 142 |     | I8 Int8
 143 |     | I16 Int16
 144 |     | I32 Int32
 145 |     | I64 Int64
 146 |     | B8 Bits8
 147 |     | B16 Bits16
 148 |     | B32 Bits32
 149 |     | B64 Bits64
 150 |     | Str String
 151 |     | Ch Char
 152 |     | Db Double
 153 |     | PrT PrimType
 154 |     | WorldVal
 155 | 
 156 | %name Constant c
 157 | 
 158 | export
 159 | Show PrimType where
 160 |   show IntType = "Int"
 161 |   show IntegerType = "Integer"
 162 |   show Int8Type = "Int8"
 163 |   show Int16Type = "Int16"
 164 |   show Int32Type = "Int32"
 165 |   show Int64Type = "Int64"
 166 |   show Bits8Type = "Bits8"
 167 |   show Bits16Type = "Bits16"
 168 |   show Bits32Type = "Bits32"
 169 |   show Bits64Type = "Bits64"
 170 |   show StringType = "String"
 171 |   show CharType = "Char"
 172 |   show DoubleType = "Double"
 173 |   show WorldType = "%World"
 174 | 
 175 | export
 176 | Show Constant where
 177 |   show (I x) = show x
 178 |   show (BI x) = show x
 179 |   show (I8 x) = show x
 180 |   show (I16 x) = show x
 181 |   show (I32 x) = show x
 182 |   show (I64 x) = show x
 183 |   show (B8 x) = show x
 184 |   show (B16 x) = show x
 185 |   show (B32 x) = show x
 186 |   show (B64 x) = show x
 187 |   show (Str x) = show x
 188 |   show (Ch x) = show x
 189 |   show (Db x) = show x
 190 |   show (PrT x) = show x
 191 |   show WorldVal = "%World"
 192 | 
 193 | ||| Any name that a user can assign to
 194 | public export
 195 | data UserName
 196 |   = Basic String -- default name constructor       e.g. map
 197 |   | Field String -- field accessor                 e.g. .fst
 198 |   | Underscore   -- no name                        e.g. _
 199 | 
 200 | %name UserName un
 201 | 
 202 | ||| A name in a Idris program
 203 | public export
 204 | data Name : Type where
 205 |   ||| A qualified name
 206 |   NS : Namespace -> Name -> Name
 207 |   ||| A user defined name
 208 |   UN : UserName -> Name
 209 |   ||| A machine generated name
 210 |   MN : String -> Int -> Name
 211 |   ||| A name with a display string
 212 |   DN : String -> Name -> Name
 213 |   ||| Nested function name
 214 |   Nested : (Int, Int) -> Name -> Name
 215 |   ||| Case block nested in (resolved) name
 216 |   CaseBlock : String -> Int -> Name
 217 |   ||| With block nested in (resolved) name
 218 |   WithBlock : String -> Int -> Name
 219 | 
 220 | %name Name nm
 221 | 
 222 | %nameLit fromName
 223 | 
 224 | public export
 225 | fromName : Name -> Name
 226 | fromName nm = nm
 227 | 
 228 | export
 229 | dropNS : Name -> Name
 230 | dropNS (NS _ n) = dropNS n
 231 | dropNS n = n
 232 | 
 233 | export
 234 | getNS : Name -> Namespace
 235 | getNS (NS ns nm) = ns
 236 | getNS nm = TT.MkNS []
 237 | 
 238 | export
 239 | isOp : Name -> Bool
 240 | isOp nm = case dropNS nm of
 241 |   UN (Basic n) => case strM n of
 242 |     StrCons c _ => not (isAlpha c)
 243 |     _ => False
 244 |   _ => False
 245 | 
 246 | export
 247 | Show UserName where
 248 |   show (Basic n) = n
 249 |   show (Field n) = "." ++ n
 250 |   show Underscore = "_"
 251 | 
 252 | export
 253 | showPrefix : Bool -> Name -> String
 254 | showPrefix b nm@(UN un) = showParens (b && isOp nm) (show un)
 255 | showPrefix b (NS ns n) = show ns ++ "." ++ showPrefix True n
 256 | showPrefix b (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
 257 | showPrefix b (DN str y) = str
 258 | showPrefix b (Nested (outer, idx) inner)
 259 |       = show outer ++ ":" ++ show idx ++ ":" ++ showPrefix False inner
 260 | showPrefix b (CaseBlock outer i) = "case block in " ++ show outer
 261 | showPrefix b (WithBlock outer i) = "with block in " ++ show outer
 262 | 
 263 | export
 264 | Show Name where
 265 |   show = showPrefix False
 266 | 
 267 | public export
 268 | record NameInfo where
 269 |   constructor MkNameInfo
 270 |   nametype : NameType
 271 | 
 272 | ||| A multiplicity
 273 | public export
 274 | data Count : Type where
 275 |   ||| 0 (erased)
 276 |   M0 : Count
 277 |   ||| 1 (linear)
 278 |   M1 : Count
 279 |   ||| ω (unrestricted)
 280 |   MW : Count
 281 | %name Count rig
 282 | 
 283 | export
 284 | enunciate : Count -> String
 285 | enunciate M0 = "runtime irrelevant"
 286 | enunciate M1 = "linear"
 287 | enunciate MW = "unconstrained"
 288 | 
 289 | export
 290 | showCount : Count -> String -> String
 291 | showCount M0 s = "0 \{s}"
 292 | showCount M1 s = "1 \{s}"
 293 | showCount MW s = s
 294 | 
 295 | public export
 296 | data PiInfo t = ImplicitArg | ExplicitArg | AutoImplicit | DefImplicit t
 297 | %name PiInfo pinfo
 298 | 
 299 | public export
 300 | Functor PiInfo where
 301 |   map f ImplicitArg     = ImplicitArg
 302 |   map f ExplicitArg     = ExplicitArg
 303 |   map f AutoImplicit    = AutoImplicit
 304 |   map f $ DefImplicit x = DefImplicit $ f x
 305 | 
 306 | export
 307 | showPiInfo : Show a => {default True wrapExplicit : Bool} -> PiInfo a -> String -> String
 308 | showPiInfo ImplicitArg s = "{\{s}}"
 309 | showPiInfo ExplicitArg s = if wrapExplicit then "(\{s})" else s
 310 | showPiInfo AutoImplicit s = "{auto \{s}}"
 311 | showPiInfo (DefImplicit t) s = "{default \{assert_total $ showPrec App t} \{s}}"
 312 | 
 313 | public export
 314 | data IsVar : Name -> Nat -> List Name -> Type where
 315 |      First : IsVar n Z (n :: ns)
 316 |      Later : IsVar n i ns -> IsVar n (S i) (m :: ns)
 317 | %name IsVar idx
 318 | 
 319 | public export
 320 | data LazyReason = LInf | LLazy | LUnknown
 321 | %name LazyReason lr
 322 | 
 323 | export
 324 | Show LazyReason where
 325 |   show LInf = "Inf"
 326 |   show LLazy = "Lazy"
 327 |   show LUnknown = "Unknown"
 328 | 
 329 | public export
 330 | data TotalReq = Total | CoveringOnly | PartialOK
 331 | %name TotalReq treq
 332 | 
 333 | export
 334 | Show TotalReq where
 335 |   show Total = "total"
 336 |   show CoveringOnly = "covering"
 337 |   show PartialOK = "partial"
 338 | 
 339 | export
 340 | showTotalReq : Maybe TotalReq -> String -> String
 341 | showTotalReq Nothing s = s
 342 | showTotalReq (Just treq) s = unwords [show treq, s]
 343 | 
 344 | public export
 345 | data Visibility = Private | Export | Public
 346 | %name Visibility vis
 347 | 
 348 | export
 349 | Show Visibility where
 350 |   show Private = "private"
 351 |   show Export = "export"
 352 |   show Public = "public export"
 353 | 
 354 | public export
 355 | data BuiltinType = BuiltinNatural | NaturalToInteger | IntegerToNatural
 356 | %name BuiltinType bty
 357 | 
 358 | export
 359 | Show BuiltinType where
 360 |   show BuiltinNatural = "Natural"
 361 |   show NaturalToInteger = "NaturalToInteger"
 362 |   show IntegerToNatural = "IntegerToNatural"
 363 | 
 364 | public export
 365 | Eq TotalReq where
 366 |   Total        == Total        = True
 367 |   CoveringOnly == CoveringOnly = True
 368 |   PartialOK    == PartialOK    = True
 369 |   _ == _ = False
 370 | 
 371 | public export
 372 | Eq Visibility where
 373 |   Private == Private = True
 374 |   Export  == Export  = True
 375 |   Public  == Public  = True
 376 |   _ == _ = False
 377 | 
 378 | public export
 379 | Eq BuiltinType where
 380 |   BuiltinNatural   == BuiltinNatural = True
 381 |   NaturalToInteger == NaturalToInteger = True
 382 |   IntegerToNatural == IntegerToNatural = True
 383 |   _ == _ = False
 384 | 
 385 | 
 386 | public export
 387 | Eq LazyReason where
 388 |   LInf     == LInf     = True
 389 |   LLazy    == LLazy    = True
 390 |   LUnknown == LUnknown = True
 391 |   _ == _ = False
 392 | 
 393 | public export
 394 | Eq Namespace where
 395 |   MkNS ns == MkNS ns' = ns == ns'
 396 | 
 397 | public export
 398 | Eq Count where
 399 |   M0 == M0 = True
 400 |   M1 == M1 = True
 401 |   MW == MW = True
 402 |   _  == _  = False
 403 | 
 404 | public export
 405 | Eq UserName where
 406 |   Basic n    == Basic n'   = n == n'
 407 |   Field n    == Field n'   = n == n'
 408 |   Underscore == Underscore = True
 409 |   _ == _ = False
 410 | 
 411 | public export
 412 | Eq Name where
 413 |   NS ns n        == NS ns' n'       = ns == ns' && n == n'
 414 |   UN n           == UN n'           = n == n'
 415 |   MN n i         == MN n' i'        = n == n' && i == i'
 416 |   DN _ n         == DN _ n'         = n == n'
 417 |   Nested i n     == Nested i' n'    = i == i' && n == n'
 418 |   CaseBlock n i  == CaseBlock n' i' = n == n' && i == i'
 419 |   WithBlock n i  == WithBlock n' i' = n == n' && i == i'
 420 |   _ == _ = False
 421 | 
 422 | public export
 423 | Eq PrimType where
 424 |   IntType     == IntType     = True
 425 |   IntegerType == IntegerType = True
 426 |   Int8Type    == Int8Type    = True
 427 |   Int16Type   == Int16Type   = True
 428 |   Int32Type   == Int32Type   = True
 429 |   Int64Type   == Int64Type   = True
 430 |   Bits8Type   == Bits8Type   = True
 431 |   Bits16Type  == Bits16Type  = True
 432 |   Bits32Type  == Bits32Type  = True
 433 |   Bits64Type  == Bits64Type  = True
 434 |   StringType  == StringType  = True
 435 |   CharType    == CharType    = True
 436 |   DoubleType  == DoubleType  = True
 437 |   WorldType   == WorldType   = True
 438 |   _ == _ = False
 439 | 
 440 | public export
 441 | Eq Constant where
 442 |   I c         == I c'        = c == c'
 443 |   BI c        == BI c'       = c == c'
 444 |   I8 c        == I8 c'       = c == c'
 445 |   I16 c       == I16 c'      = c == c'
 446 |   I32 c       == I32 c'      = c == c'
 447 |   I64 c       == I64 c'      = c == c'
 448 |   B8 c        == B8 c'       = c == c'
 449 |   B16 c       == B16 c'      = c == c'
 450 |   B32 c       == B32 c'      = c == c'
 451 |   B64 c       == B64 c'      = c == c'
 452 |   Str c       == Str c'      = c == c'
 453 |   Ch c        == Ch c'       = c == c'
 454 |   Db c        == Db c'       = c == c'
 455 |   PrT t       == PrT t'      = t == t'
 456 |   WorldVal    == WorldVal    = True
 457 |   _ == _ = False
 458 | 
 459 | public export
 460 | Ord Namespace where
 461 |     compare (MkNS ms) (MkNS ns) = compare ms ns
 462 | 
 463 | public export
 464 | Ord Count where
 465 |   compare M0 M0 = EQ
 466 |   compare M0 _  = LT
 467 |   compare _  M0 = GT
 468 |   compare M1 M1 = EQ
 469 |   compare MW MW = EQ
 470 |   compare MW M1 = GT
 471 |   compare M1 MW = LT
 472 | 
 473 | usernameTag : UserName -> Int
 474 | usernameTag (Basic _)  = 0
 475 | usernameTag (Field _)  = 1
 476 | usernameTag Underscore = 2
 477 | 
 478 | public export
 479 | Ord UserName where
 480 |   compare (Basic x) (Basic y)   = compare x y
 481 |   compare (Field x) (Field y)   = compare x y
 482 |   compare Underscore Underscore = EQ
 483 |   compare x y                   = compare (usernameTag x) (usernameTag y)
 484 | 
 485 | nameTag : Name -> Int
 486 | nameTag (NS _ _)        = 0
 487 | nameTag (UN _)          = 1
 488 | nameTag (MN _ _)        = 2
 489 | nameTag (DN _ _)        = 3
 490 | nameTag (Nested _ _)    = 4
 491 | nameTag (CaseBlock _ _) = 5
 492 | nameTag (WithBlock _ _) = 6
 493 | 
 494 | public export
 495 | Ord Name where
 496 |     compare (NS x y) (NS x' y')
 497 |         = case compare y y' of -- Compare base name first (more likely to differ)
 498 |                EQ => compare x x'
 499 |                -- Because of the terrible way Idris 1 compiles 'case', this
 500 |                -- is actually faster than just having 't => t'...
 501 |                GT => GT
 502 |                LT => LT
 503 |     compare (UN x) (UN y) = compare x y
 504 |     compare (MN x y) (MN x' y')
 505 |         = case compare y y' of
 506 |                EQ => compare x x'
 507 |                GT => GT
 508 |                LT => LT
 509 |     compare (DN _ n) (DN _ n') = compare n n'
 510 |     compare (Nested x y) (Nested x' y')
 511 |         = case compare y y' of
 512 |                EQ => compare x x'
 513 |                GT => GT
 514 |                LT => LT
 515 |     compare (CaseBlock x y) (CaseBlock x' y')
 516 |         = case compare y y' of
 517 |                EQ => compare x x'
 518 |                GT => GT
 519 |                LT => LT
 520 |     compare (WithBlock x y) (WithBlock x' y')
 521 |         = case compare y y' of
 522 |                EQ => compare x x'
 523 |                GT => GT
 524 |                LT => LT
 525 | 
 526 |     compare x y = compare (nameTag x) (nameTag y)
 527 | 
 528 | export Injective MkNS where injective Refl = Refl
 529 | 
 530 | public export
 531 | DecEq Namespace where
 532 |   decEq (MkNS ns) (MkNS ns') = decEqCong (decEq ns ns')
 533 | 
 534 | export Injective Basic where injective Refl = Refl
 535 | export Injective Field where injective Refl = Refl
 536 | 
 537 | public export
 538 | DecEq UserName where
 539 |   decEq (Basic str) (Basic str1) = decEqCong (decEq str str1)
 540 |   decEq (Basic str) (Field str1) = No (\case Refl impossible)
 541 |   decEq (Basic str) Underscore = No (\case Refl impossible)
 542 |   decEq (Field str) (Basic str1) = No (\case Refl impossible)
 543 |   decEq (Field str) (Field str1) = decEqCong (decEq str str1)
 544 |   decEq (Field str) Underscore = No (\case Refl impossible)
 545 |   decEq Underscore (Basic str) = No (\case Refl impossible)
 546 |   decEq Underscore (Field str) = No (\case Refl impossible)
 547 |   decEq Underscore Underscore = Yes Refl
 548 | 
 549 | export Biinjective NS where biinjective Refl = (Refl, Refl)
 550 | export Injective UN where injective Refl = Refl
 551 | export Biinjective MN where biinjective Refl = (Refl, Refl)
 552 | export Biinjective DN where biinjective Refl = (Refl, Refl)
 553 | export Biinjective Nested where biinjective Refl = (Refl, Refl)
 554 | export Biinjective CaseBlock where biinjective Refl = (Refl, Refl)
 555 | export Biinjective WithBlock where biinjective Refl = (Refl, Refl)
 556 | 
 557 | public export
 558 | DecEq Name where
 559 |   decEq (NS ns nm) (NS ns1 nm1) = decEqCong2 (decEq ns ns1) (decEq nm nm1)
 560 |   decEq (NS ns nm) (UN un) =  No (\case Refl impossible)
 561 |   decEq (NS ns nm) (MN str i) = No (\case Refl impossible)
 562 |   decEq (NS ns nm) (DN str nm1) = No (\case Refl impossible)
 563 |   decEq (NS ns nm) (Nested x nm1) = No (\case Refl impossible)
 564 |   decEq (NS ns nm) (CaseBlock str i) = No (\case Refl impossible)
 565 |   decEq (NS ns nm) (WithBlock str i) = No (\case Refl impossible)
 566 |   decEq (UN un) (NS ns nm) = No (\case Refl impossible)
 567 |   decEq (UN un) (UN un1) = decEqCong (decEq un un1)
 568 |   decEq (UN un) (MN str i) = No (\case Refl impossible)
 569 |   decEq (UN un) (DN str nm) = No (\case Refl impossible)
 570 |   decEq (UN un) (Nested x nm) = No (\case Refl impossible)
 571 |   decEq (UN un) (CaseBlock str i) = No (\case Refl impossible)
 572 |   decEq (UN un) (WithBlock str i) = No (\case Refl impossible)
 573 |   decEq (MN str i) (NS ns nm) = No (\case Refl impossible)
 574 |   decEq (MN str i) (UN un) = No (\case Refl impossible)
 575 |   decEq (MN str i) (MN str1 j) = decEqCong2 (decEq str str1) (decEq i j)
 576 |   decEq (MN str i) (DN str1 nm) = No (\case Refl impossible)
 577 |   decEq (MN str i) (Nested x nm) = No (\case Refl impossible)
 578 |   decEq (MN str i) (CaseBlock str1 j) = No (\case Refl impossible)
 579 |   decEq (MN str i) (WithBlock str1 j) = No (\case Refl impossible)
 580 |   decEq (DN str nm) (NS ns nm1) = No (\case Refl impossible)
 581 |   decEq (DN str nm) (UN un) = No (\case Refl impossible)
 582 |   decEq (DN str nm) (MN str1 i) = No (\case Refl impossible)
 583 |   decEq (DN str nm) (DN str1 nm1) = decEqCong2 (decEq str str1) (decEq nm nm1)
 584 |   decEq (DN str nm) (Nested x nm1) = No (\case Refl impossible)
 585 |   decEq (DN str nm) (CaseBlock str1 i) = No (\case Refl impossible)
 586 |   decEq (DN str nm) (WithBlock str1 i) = No (\case Refl impossible)
 587 |   decEq (Nested x nm) (NS ns nm1) = No (\case Refl impossible)
 588 |   decEq (Nested x nm) (UN un) = No (\case Refl impossible)
 589 |   decEq (Nested x nm) (MN str i) = No (\case Refl impossible)
 590 |   decEq (Nested x nm) (DN str nm1) = No (\case Refl impossible)
 591 |   decEq (Nested x nm) (Nested y nm1) = decEqCong2 (decEq x y) (decEq nm nm1)
 592 |   decEq (Nested x nm) (CaseBlock str i) = No (\case Refl impossible)
 593 |   decEq (Nested x nm) (WithBlock str i) = No (\case Refl impossible)
 594 |   decEq (CaseBlock str i) (NS ns nm) = No (\case Refl impossible)
 595 |   decEq (CaseBlock str i) (UN un) = No (\case Refl impossible)
 596 |   decEq (CaseBlock str i) (MN str1 j) = No (\case Refl impossible)
 597 |   decEq (CaseBlock str i) (DN str1 nm) = No (\case Refl impossible)
 598 |   decEq (CaseBlock str i) (Nested x nm) = No (\case Refl impossible)
 599 |   decEq (CaseBlock str i) (CaseBlock str1 j) = decEqCong2 (decEq str str1) (decEq i j)
 600 |   decEq (CaseBlock str i) (WithBlock str1 j) = No (\case Refl impossible)
 601 |   decEq (WithBlock str i) (NS ns nm) = No (\case Refl impossible)
 602 |   decEq (WithBlock str i) (UN un) = No (\case Refl impossible)
 603 |   decEq (WithBlock str i) (MN str1 j) = No (\case Refl impossible)
 604 |   decEq (WithBlock str i) (DN str1 nm) = No (\case Refl impossible)
 605 |   decEq (WithBlock str i) (Nested x nm) = No (\case Refl impossible)
 606 |   decEq (WithBlock str i) (CaseBlock str1 j) = No (\case Refl impossible)
 607 |   decEq (WithBlock str i) (WithBlock str1 j) = decEqCong2 (decEq str str1) (decEq i j)
 608 |