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