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 |                -- TODO: remove type tag, it's is always 0
 112 | 
 113 | %name NameType nty
 114 | 
 115 | public export
 116 | data PrimType
 117 |     = IntType
 118 |     | IntegerType
 119 |     | Int8Type
 120 |     | Int16Type
 121 |     | Int32Type
 122 |     | Int64Type
 123 |     | Bits8Type
 124 |     | Bits16Type
 125 |     | Bits32Type
 126 |     | Bits64Type
 127 |     | StringType
 128 |     | CharType
 129 |     | DoubleType
 130 |     | WorldType
 131 | 
 132 | %name PrimType pty
 133 | 
 134 | public export
 135 | data Constant
 136 |     = I Int
 137 |     | BI Integer
 138 |     | I8 Int8
 139 |     | I16 Int16
 140 |     | I32 Int32
 141 |     | I64 Int64
 142 |     | B8 Bits8
 143 |     | B16 Bits16
 144 |     | B32 Bits32
 145 |     | B64 Bits64
 146 |     | Str String
 147 |     | Ch Char
 148 |     | Db Double
 149 |     | PrT PrimType
 150 |     | WorldVal
 151 | 
 152 | %name Constant c
 153 | 
 154 | export
 155 | Show PrimType where
 156 |   show IntType = "Int"
 157 |   show IntegerType = "Integer"
 158 |   show Int8Type = "Int8"
 159 |   show Int16Type = "Int16"
 160 |   show Int32Type = "Int32"
 161 |   show Int64Type = "Int64"
 162 |   show Bits8Type = "Bits8"
 163 |   show Bits16Type = "Bits16"
 164 |   show Bits32Type = "Bits32"
 165 |   show Bits64Type = "Bits64"
 166 |   show StringType = "String"
 167 |   show CharType = "Char"
 168 |   show DoubleType = "Double"
 169 |   show WorldType = "%World"
 170 | 
 171 | export
 172 | Show Constant where
 173 |   show (I x) = show x
 174 |   show (BI x) = show x
 175 |   show (I8 x) = show x
 176 |   show (I16 x) = show x
 177 |   show (I32 x) = show x
 178 |   show (I64 x) = show x
 179 |   show (B8 x) = show x
 180 |   show (B16 x) = show x
 181 |   show (B32 x) = show x
 182 |   show (B64 x) = show x
 183 |   show (Str x) = show x
 184 |   show (Ch x) = show x
 185 |   show (Db x) = show x
 186 |   show (PrT x) = show x
 187 |   show WorldVal = "%World"
 188 | 
 189 | public export
 190 | data UserName
 191 |   = Basic String -- default name constructor       e.g. map
 192 |   | Field String -- field accessor                 e.g. .fst
 193 |   | Underscore   -- no name                        e.g. _
 194 | 
 195 | %name UserName un
 196 | 
 197 | public export
 198 | data Name = NS Namespace Name -- name in a namespace
 199 |           | UN UserName -- user defined name
 200 |           | MN String Int -- machine generated name
 201 |           | DN String Name -- a name and how to display it
 202 |           | Nested (Int, Int) Name -- nested function name
 203 |           | CaseBlock String Int -- case block nested in (resolved) name
 204 |           | WithBlock String Int -- with block nested in (resolved) name
 205 | 
 206 | %name Name nm
 207 | 
 208 | %nameLit fromName
 209 | 
 210 | public export
 211 | fromName : Name -> Name
 212 | fromName nm = nm
 213 | 
 214 | export
 215 | dropNS : Name -> Name
 216 | dropNS (NS _ n) = dropNS n
 217 | dropNS n = n
 218 | 
 219 | export
 220 | isOp : Name -> Bool
 221 | isOp nm = case dropNS nm of
 222 |   UN (Basic n) => case strM n of
 223 |     StrCons c _ => not (isAlpha c)
 224 |     _ => False
 225 |   _ => False
 226 | 
 227 | export
 228 | Show UserName where
 229 |   show (Basic n) = n
 230 |   show (Field n) = "." ++ n
 231 |   show Underscore = "_"
 232 | 
 233 | export
 234 | showPrefix : Bool -> Name -> String
 235 | showPrefix b nm@(UN un) = showParens (b && isOp nm) (show un)
 236 | showPrefix b (NS ns n) = show ns ++ "." ++ showPrefix True n
 237 | showPrefix b (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
 238 | showPrefix b (DN str y) = str
 239 | showPrefix b (Nested (outer, idx) inner)
 240 |       = show outer ++ ":" ++ show idx ++ ":" ++ showPrefix False inner
 241 | showPrefix b (CaseBlock outer i) = "case block in " ++ show outer
 242 | showPrefix b (WithBlock outer i) = "with block in " ++ show outer
 243 | 
 244 | export
 245 | Show Name where
 246 |   show = showPrefix False
 247 | 
 248 | public export
 249 | record NameInfo where
 250 |   constructor MkNameInfo
 251 |   nametype : NameType
 252 | 
 253 | public export
 254 | data Count = M0 | M1 | MW
 255 | %name Count rig
 256 | 
 257 | export
 258 | enunciate : Count -> String
 259 | enunciate M0 = "runtime irrelevant"
 260 | enunciate M1 = "linear"
 261 | enunciate MW = "unconstrained"
 262 | 
 263 | export
 264 | showCount : Count -> String -> String
 265 | showCount M0 s = "0 \{s}"
 266 | showCount M1 s = "1 \{s}"
 267 | showCount MW s = s
 268 | 
 269 | public export
 270 | data PiInfo t = ImplicitArg | ExplicitArg | AutoImplicit | DefImplicit t
 271 | %name PiInfo pinfo
 272 | 
 273 | public export
 274 | Functor PiInfo where
 275 |   map f ImplicitArg     = ImplicitArg
 276 |   map f ExplicitArg     = ExplicitArg
 277 |   map f AutoImplicit    = AutoImplicit
 278 |   map f $ DefImplicit x = DefImplicit $ f x
 279 | 
 280 | export
 281 | showPiInfo : Show a => {default True wrapExplicit : Bool} -> PiInfo a -> String -> String
 282 | showPiInfo ImplicitArg s = "{\{s}}"
 283 | showPiInfo ExplicitArg s = if wrapExplicit then "(\{s})" else s
 284 | showPiInfo AutoImplicit s = "{auto \{s}}"
 285 | showPiInfo (DefImplicit t) s = "{default \{assert_total $ showPrec App t} \{s}}"
 286 | 
 287 | public export
 288 | data IsVar : Name -> Nat -> List Name -> Type where
 289 |      First : IsVar n Z (n :: ns)
 290 |      Later : IsVar n i ns -> IsVar n (S i) (m :: ns)
 291 | %name IsVar idx
 292 | 
 293 | public export
 294 | data LazyReason = LInf | LLazy | LUnknown
 295 | %name LazyReason lr
 296 | 
 297 | export
 298 | Show LazyReason where
 299 |   show LInf = "Inf"
 300 |   show LLazy = "Lazy"
 301 |   show LUnknown = "Unknown"
 302 | 
 303 | public export
 304 | data TotalReq = Total | CoveringOnly | PartialOK
 305 | %name TotalReq treq
 306 | 
 307 | export
 308 | Show TotalReq where
 309 |   show Total = "total"
 310 |   show CoveringOnly = "covering"
 311 |   show PartialOK = "partial"
 312 | 
 313 | export
 314 | showTotalReq : Maybe TotalReq -> String -> String
 315 | showTotalReq Nothing s = s
 316 | showTotalReq (Just treq) s = unwords [show treq, s]
 317 | 
 318 | public export
 319 | data Visibility = Private | Export | Public
 320 | %name Visibility vis
 321 | 
 322 | export
 323 | Show Visibility where
 324 |   show Private = "private"
 325 |   show Export = "export"
 326 |   show Public = "public export"
 327 | 
 328 | public export
 329 | data BuiltinType = BuiltinNatural | NaturalToInteger | IntegerToNatural
 330 | %name BuiltinType bty
 331 | 
 332 | export
 333 | Show BuiltinType where
 334 |   show BuiltinNatural = "Natural"
 335 |   show NaturalToInteger = "NaturalToInteger"
 336 |   show IntegerToNatural = "IntegerToNatural"
 337 | 
 338 | public export
 339 | Eq TotalReq where
 340 |   Total        == Total        = True
 341 |   CoveringOnly == CoveringOnly = True
 342 |   PartialOK    == PartialOK    = True
 343 |   _ == _ = False
 344 | 
 345 | public export
 346 | Eq Visibility where
 347 |   Private == Private = True
 348 |   Export  == Export  = True
 349 |   Public  == Public  = True
 350 |   _ == _ = False
 351 | 
 352 | public export
 353 | Eq BuiltinType where
 354 |   BuiltinNatural   == BuiltinNatural = True
 355 |   NaturalToInteger == NaturalToInteger = True
 356 |   IntegerToNatural == IntegerToNatural = True
 357 |   _ == _ = False
 358 | 
 359 | 
 360 | public export
 361 | Eq LazyReason where
 362 |   LInf     == LInf     = True
 363 |   LLazy    == LLazy    = True
 364 |   LUnknown == LUnknown = True
 365 |   _ == _ = False
 366 | 
 367 | public export
 368 | Eq Namespace where
 369 |   MkNS ns == MkNS ns' = ns == ns'
 370 | 
 371 | public export
 372 | Eq Count where
 373 |   M0 == M0 = True
 374 |   M1 == M1 = True
 375 |   MW == MW = True
 376 |   _  == _  = False
 377 | 
 378 | public export
 379 | Eq UserName where
 380 |   Basic n    == Basic n'   = n == n'
 381 |   Field n    == Field n'   = n == n'
 382 |   Underscore == Underscore = True
 383 |   _ == _ = False
 384 | 
 385 | public export
 386 | Eq Name where
 387 |   NS ns n        == NS ns' n'       = ns == ns' && n == n'
 388 |   UN n           == UN n'           = n == n'
 389 |   MN n i         == MN n' i'        = n == n' && i == i'
 390 |   DN _ n         == DN _ n'         = n == n'
 391 |   Nested i n     == Nested i' n'    = i == i' && n == n'
 392 |   CaseBlock n i  == CaseBlock n' i' = n == n' && i == i'
 393 |   WithBlock n i  == WithBlock n' i' = n == n' && i == i'
 394 |   _ == _ = False
 395 | 
 396 | public export
 397 | Eq PrimType where
 398 |   IntType     == IntType     = True
 399 |   IntegerType == IntegerType = True
 400 |   Int8Type    == Int8Type    = True
 401 |   Int16Type   == Int16Type   = True
 402 |   Int32Type   == Int32Type   = True
 403 |   Int64Type   == Int64Type   = True
 404 |   Bits8Type   == Bits8Type   = True
 405 |   Bits16Type  == Bits16Type  = True
 406 |   Bits32Type  == Bits32Type  = True
 407 |   Bits64Type  == Bits64Type  = True
 408 |   StringType  == StringType  = True
 409 |   CharType    == CharType    = True
 410 |   DoubleType  == DoubleType  = True
 411 |   WorldType   == WorldType   = True
 412 |   _ == _ = False
 413 | 
 414 | public export
 415 | Eq Constant where
 416 |   I c         == I c'        = c == c'
 417 |   BI c        == BI c'       = c == c'
 418 |   I8 c        == I8 c'       = c == c'
 419 |   I16 c       == I16 c'      = c == c'
 420 |   I32 c       == I32 c'      = c == c'
 421 |   I64 c       == I64 c'      = c == c'
 422 |   B8 c        == B8 c'       = c == c'
 423 |   B16 c       == B16 c'      = c == c'
 424 |   B32 c       == B32 c'      = c == c'
 425 |   B64 c       == B64 c'      = c == c'
 426 |   Str c       == Str c'      = c == c'
 427 |   Ch c        == Ch c'       = c == c'
 428 |   Db c        == Db c'       = c == c'
 429 |   PrT t       == PrT t'      = t == t'
 430 |   WorldVal    == WorldVal    = True
 431 |   _ == _ = False
 432 | 
 433 | public export
 434 | Ord Namespace where
 435 |     compare (MkNS ms) (MkNS ns) = compare ms ns
 436 | 
 437 | public export
 438 | Ord Count where
 439 |   compare M0 M0 = EQ
 440 |   compare M0 _  = LT
 441 |   compare _  M0 = GT
 442 |   compare M1 M1 = EQ
 443 |   compare MW MW = EQ
 444 |   compare MW M1 = GT
 445 |   compare M1 MW = LT
 446 | 
 447 | usernameTag : UserName -> Int
 448 | usernameTag (Basic _)  = 0
 449 | usernameTag (Field _)  = 1
 450 | usernameTag Underscore = 2
 451 | 
 452 | public export
 453 | Ord UserName where
 454 |   compare (Basic x) (Basic y)   = compare x y
 455 |   compare (Field x) (Field y)   = compare x y
 456 |   compare Underscore Underscore = EQ
 457 |   compare x y                   = compare (usernameTag x) (usernameTag y)
 458 | 
 459 | nameTag : Name -> Int
 460 | nameTag (NS _ _)        = 0
 461 | nameTag (UN _)          = 1
 462 | nameTag (MN _ _)        = 2
 463 | nameTag (DN _ _)        = 3
 464 | nameTag (Nested _ _)    = 4
 465 | nameTag (CaseBlock _ _) = 5
 466 | nameTag (WithBlock _ _) = 6
 467 | 
 468 | public export
 469 | Ord Name where
 470 |     compare (NS x y) (NS x' y')
 471 |         = case compare y y' of -- Compare base name first (more likely to differ)
 472 |                EQ => compare x x'
 473 |                -- Because of the terrible way Idris 1 compiles 'case', this
 474 |                -- is actually faster than just having 't => t'...
 475 |                GT => GT
 476 |                LT => LT
 477 |     compare (UN x) (UN y) = compare x y
 478 |     compare (MN x y) (MN x' y')
 479 |         = case compare y y' of
 480 |                EQ => compare x x'
 481 |                GT => GT
 482 |                LT => LT
 483 |     compare (DN _ n) (DN _ n') = compare n n'
 484 |     compare (Nested x y) (Nested x' y')
 485 |         = case compare y y' of
 486 |                EQ => compare x x'
 487 |                GT => GT
 488 |                LT => LT
 489 |     compare (CaseBlock x y) (CaseBlock x' y')
 490 |         = case compare y y' of
 491 |                EQ => compare x x'
 492 |                GT => GT
 493 |                LT => LT
 494 |     compare (WithBlock x y) (WithBlock x' y')
 495 |         = case compare y y' of
 496 |                EQ => compare x x'
 497 |                GT => GT
 498 |                LT => LT
 499 | 
 500 |     compare x y = compare (nameTag x) (nameTag y)
 501 | 
 502 | export Injective MkNS where injective Refl = Refl
 503 | 
 504 | public export
 505 | DecEq Namespace where
 506 |   decEq (MkNS ns) (MkNS ns') = decEqCong (decEq ns ns')
 507 | 
 508 | export Injective Basic where injective Refl = Refl
 509 | export Injective Field where injective Refl = Refl
 510 | 
 511 | public export
 512 | DecEq UserName where
 513 |   decEq (Basic str) (Basic str1) = decEqCong (decEq str str1)
 514 |   decEq (Basic str) (Field str1) = No (\case Refl impossible)
 515 |   decEq (Basic str) Underscore = No (\case Refl impossible)
 516 |   decEq (Field str) (Basic str1) = No (\case Refl impossible)
 517 |   decEq (Field str) (Field str1) = decEqCong (decEq str str1)
 518 |   decEq (Field str) Underscore = No (\case Refl impossible)
 519 |   decEq Underscore (Basic str) = No (\case Refl impossible)
 520 |   decEq Underscore (Field str) = No (\case Refl impossible)
 521 |   decEq Underscore Underscore = Yes Refl
 522 | 
 523 | export Biinjective NS where biinjective Refl = (Refl, Refl)
 524 | export Injective UN where injective Refl = Refl
 525 | export Biinjective MN where biinjective Refl = (Refl, Refl)
 526 | export Biinjective DN where biinjective Refl = (Refl, Refl)
 527 | export Biinjective Nested where biinjective Refl = (Refl, Refl)
 528 | export Biinjective CaseBlock where biinjective Refl = (Refl, Refl)
 529 | export Biinjective WithBlock where biinjective Refl = (Refl, Refl)
 530 | 
 531 | public export
 532 | DecEq Name where
 533 |   decEq (NS ns nm) (NS ns1 nm1) = decEqCong2 (decEq ns ns1) (decEq nm nm1)
 534 |   decEq (NS ns nm) (UN un) =  No (\case Refl impossible)
 535 |   decEq (NS ns nm) (MN str i) = No (\case Refl impossible)
 536 |   decEq (NS ns nm) (DN str nm1) = No (\case Refl impossible)
 537 |   decEq (NS ns nm) (Nested x nm1) = No (\case Refl impossible)
 538 |   decEq (NS ns nm) (CaseBlock str i) = No (\case Refl impossible)
 539 |   decEq (NS ns nm) (WithBlock str i) = No (\case Refl impossible)
 540 |   decEq (UN un) (NS ns nm) = No (\case Refl impossible)
 541 |   decEq (UN un) (UN un1) = decEqCong (decEq un un1)
 542 |   decEq (UN un) (MN str i) = No (\case Refl impossible)
 543 |   decEq (UN un) (DN str nm) = No (\case Refl impossible)
 544 |   decEq (UN un) (Nested x nm) = No (\case Refl impossible)
 545 |   decEq (UN un) (CaseBlock str i) = No (\case Refl impossible)
 546 |   decEq (UN un) (WithBlock str i) = No (\case Refl impossible)
 547 |   decEq (MN str i) (NS ns nm) = No (\case Refl impossible)
 548 |   decEq (MN str i) (UN un) = No (\case Refl impossible)
 549 |   decEq (MN str i) (MN str1 j) = decEqCong2 (decEq str str1) (decEq i j)
 550 |   decEq (MN str i) (DN str1 nm) = No (\case Refl impossible)
 551 |   decEq (MN str i) (Nested x nm) = No (\case Refl impossible)
 552 |   decEq (MN str i) (CaseBlock str1 j) = No (\case Refl impossible)
 553 |   decEq (MN str i) (WithBlock str1 j) = No (\case Refl impossible)
 554 |   decEq (DN str nm) (NS ns nm1) = No (\case Refl impossible)
 555 |   decEq (DN str nm) (UN un) = No (\case Refl impossible)
 556 |   decEq (DN str nm) (MN str1 i) = No (\case Refl impossible)
 557 |   decEq (DN str nm) (DN str1 nm1) = decEqCong2 (decEq str str1) (decEq nm nm1)
 558 |   decEq (DN str nm) (Nested x nm1) = No (\case Refl impossible)
 559 |   decEq (DN str nm) (CaseBlock str1 i) = No (\case Refl impossible)
 560 |   decEq (DN str nm) (WithBlock str1 i) = No (\case Refl impossible)
 561 |   decEq (Nested x nm) (NS ns nm1) = No (\case Refl impossible)
 562 |   decEq (Nested x nm) (UN un) = No (\case Refl impossible)
 563 |   decEq (Nested x nm) (MN str i) = No (\case Refl impossible)
 564 |   decEq (Nested x nm) (DN str nm1) = No (\case Refl impossible)
 565 |   decEq (Nested x nm) (Nested y nm1) = decEqCong2 (decEq x y) (decEq nm nm1)
 566 |   decEq (Nested x nm) (CaseBlock str i) = No (\case Refl impossible)
 567 |   decEq (Nested x nm) (WithBlock str i) = No (\case Refl impossible)
 568 |   decEq (CaseBlock str i) (NS ns nm) = No (\case Refl impossible)
 569 |   decEq (CaseBlock str i) (UN un) = No (\case Refl impossible)
 570 |   decEq (CaseBlock str i) (MN str1 j) = No (\case Refl impossible)
 571 |   decEq (CaseBlock str i) (DN str1 nm) = No (\case Refl impossible)
 572 |   decEq (CaseBlock str i) (Nested x nm) = No (\case Refl impossible)
 573 |   decEq (CaseBlock str i) (CaseBlock str1 j) = decEqCong2 (decEq str str1) (decEq i j)
 574 |   decEq (CaseBlock str i) (WithBlock str1 j) = No (\case Refl impossible)
 575 |   decEq (WithBlock str i) (NS ns nm) = No (\case Refl impossible)
 576 |   decEq (WithBlock str i) (UN un) = No (\case Refl impossible)
 577 |   decEq (WithBlock str i) (MN str1 j) = No (\case Refl impossible)
 578 |   decEq (WithBlock str i) (DN str1 nm) = No (\case Refl impossible)
 579 |   decEq (WithBlock str i) (Nested x nm) = No (\case Refl impossible)
 580 |   decEq (WithBlock str i) (CaseBlock str1 j) = No (\case Refl impossible)
 581 |   decEq (WithBlock str i) (WithBlock str1 j) = decEqCong2 (decEq str str1) (decEq i j)
 582 |