0 | module Language.Reflection.TTImp
   1 |
   2 | import public Data.List1
   3 | import Data.Maybe
   4 | import public Language.Reflection.TT
   5 |
   6 |
   7 | %default total
   8 |
   9 | -- Unchecked terms and declarations in the intermediate language
  10 | mutual
  11 |   public export
  12 |   data BindMode = PI Count | PATTERN | COVERAGE | NONE
  13 |   %name BindMode bm
  14 |
  15 |   -- For as patterns matching linear arguments, select which side is
  16 |   -- consumed
  17 |   public export
  18 |   data UseSide = UseLeft | UseRight
  19 |   %name UseSide side
  20 |
  21 |   public export
  22 |   data DotReason = NonLinearVar
  23 |                  | VarApplied
  24 |                  | NotConstructor
  25 |                  | ErasedArg
  26 |                  | UserDotted
  27 |                  | UnknownDot
  28 |                  | UnderAppliedCon
  29 |   %name DotReason dr
  30 |
  31 |   ||| The elaborator representation of an Idris term
  32 |   ||| All of these take a file context `FC` as their first argument
  33 |   public export
  34 |   data TTImp : Type where
  35 |        ||| A variable reference, by name
  36 |        IVar : FC -> Name -> TTImp
  37 |        ||| A function type, of the form `(mult binder : argTy) -> retTy`, with implicitness determined by `info`
  38 |        IPi : FC -> (mult : Count) -> (info : PiInfo TTImp) -> (binder : Maybe Name) ->
  39 |              (argTy : TTImp) -> (retTy : TTImp) -> TTImp
  40 |        ||| A lambda abstraction, of the form`\(mult binder : argTy) => retTy`, with implicitness determined by `info`
  41 |        ILam : FC -> (mult : Count) -> (info : PiInfo TTImp) -> (binder : Maybe Name) ->
  42 |               (argTy : TTImp) -> (lamTy : TTImp) -> TTImp
  43 |        ||| A let binding, of the form `let mult var : nTy = nVal in scope`
  44 |        ILet : FC -> (lhsFC : FC) -> (mult : Count) -> (var : Name) ->
  45 |               (nTy : TTImp) -> (nVal : TTImp) ->
  46 |               (scope : TTImp) -> TTImp
  47 |        ||| A case expression `case val : ty of clauses`
  48 |        ICase : FC -> (opts : List FnOpt) -> (val : TTImp) -> (ty : TTImp) ->
  49 |                (clauses : List Clause) -> TTImp
  50 |        ||| A list of full declarations local to a term
  51 |        ILocal : FC -> (context : List Decl) -> (term : TTImp) -> TTImp
  52 |        ||| An update to a record value, `{ updates } val`
  53 |        IUpdate : FC -> (updates : List IFieldUpdate) -> (val : TTImp) -> TTImp
  54 |
  55 |        ||| A function application, `f x`
  56 |        IApp : FC -> (f : TTImp) -> (x : TTImp) -> TTImp
  57 |        ||| A named function application (for named parameters), e.g, `f {arg=x}`
  58 |        INamedApp : FC -> (f : TTImp) -> (arg : Name) -> (x : TTImp) -> TTImp
  59 |        ||| An explicitly inserted auto implicit, `f @{x}`
  60 |        IAutoApp : FC -> (f : TTImp) -> (x : TTImp) -> TTImp
  61 |        ||| A `with` application `f | e`
  62 |        IWithApp : FC -> (f : TTImp) -> (e : TTImp) -> TTImp
  63 |
  64 |        ||| `%search`
  65 |        ISearch : FC -> (depth : Nat) -> TTImp
  66 |        ||| A list of potential desugarings of an ambiguous expression
  67 |        ||| The success conditions of typechecking is determined by AltType
  68 |        IAlternative : FC -> AltType -> List TTImp -> TTImp
  69 |        ||| A rewrite expression, `rewrite eq in exp`
  70 |        IRewrite : FC -> (eq : TTImp) -> (exp : TTImp) -> TTImp
  71 |
  72 |        ||| Any implicit bindings in the scope should be bound here, using
  73 |        ||| the given binder
  74 |        IBindHere : FC -> BindMode -> TTImp -> TTImp
  75 |        ||| A name which should be implicitly bound
  76 |        IBindVar : FC -> Name -> TTImp
  77 |        ||| An 'as' pattern, valid on the LHS of a clause only, `group@pat`
  78 |        IAs : FC -> (nameFC : FC) -> UseSide -> (group : Name) -> (pat : TTImp) -> TTImp
  79 |        ||| A 'dot' pattern, i.e. one which must be equal to the given value
  80 |        ||| by unification, `.(e)`
  81 |        IMustUnify : FC -> DotReason -> (e : TTImp) -> TTImp
  82 |
  83 |        -- Laziness annotations
  84 |        ||| The delay type, `Delay t`
  85 |        IDelayed : FC -> LazyReason -> TTImp -> TTImp
  86 |        ||| The constructor of `Delay`, `delay t`
  87 |        IDelay : FC -> TTImp -> TTImp
  88 |        ||| `force`
  89 |        IForce : FC -> TTImp -> TTImp
  90 |
  91 |        ||| Quasi-quotation of expression (`( ... ))
  92 |        IQuote : FC -> TTImp -> TTImp
  93 |        ||| Quasi-quotation of a name (`{ ... })
  94 |        IQuoteName : FC -> Name -> TTImp
  95 |        ||| Quasi-quotation of a list of declarations (`[ ... ])
  96 |        IQuoteDecl : FC -> List Decl -> TTImp
  97 |        ||| Unquote of an expression (~e)
  98 |        IUnquote : FC -> TTImp -> TTImp
  99 |        ||| A primitive value, such as an integer or string constant.
 100 |        ||| Also any primitive *type*, apart from `Type` itself
 101 |        IPrimVal : FC -> (c : Constant) -> TTImp
 102 |        ||| The type `Type`
 103 |        IType : FC -> TTImp
 104 |        ||| A named hole
 105 |        IHole : FC -> String -> TTImp
 106 |
 107 |        ||| An implicit value, solved by unification, but which will also be
 108 |        ||| bound (either as a pattern variable or a type variable) if unsolved
 109 |        ||| at the end of elaborator.
 110 |        ||| Note that `Implicit False` is `?`, while `Implicit True` is `_`
 111 |        Implicit : FC -> (bindIfUnsolved : Bool) -> TTImp
 112 |        ||| An explicit disambiguation directive `with names exp`
 113 |        IWithUnambigNames : FC -> (name : List (FC, Name)) -> (exp : TTImp) -> TTImp
 114 |   %name TTImp s, t, u
 115 |
 116 |   ||| A record field update
 117 |   public export
 118 |   data IFieldUpdate : Type where
 119 |        ||| `path := val`
 120 |        ISetField : (path : List String) -> TTImp -> IFieldUpdate
 121 |        ||| `path $= val`
 122 |        ISetFieldApp : (path : List String) -> TTImp -> IFieldUpdate
 123 |
 124 |   %name IFieldUpdate upd
 125 |
 126 |   public export
 127 |   data AltType : Type where
 128 |        FirstSuccess : AltType
 129 |        Unique : AltType
 130 |        UniqueDefault : TTImp -> AltType
 131 |
 132 |   public export
 133 |   data FnOpt : Type where
 134 |        Inline : FnOpt
 135 |        NoInline : FnOpt
 136 |        Deprecate : FnOpt
 137 |        TCInline : FnOpt
 138 |        ||| Flag means the hint is a direct hint, not a function which might
 139 |        ||| find the result (e.g. chasing parent interface dictionaries)
 140 |        Hint : Bool -> FnOpt
 141 |        ||| A hint that is searched if direct hints search failed.
 142 |        ||| `%globalhint` if the argument is `True`, `%defaulthint` if `False`.
 143 |        GlobalHint : Bool -> FnOpt
 144 |        ExternFn : FnOpt
 145 |        ||| Defined externally, takes a list of calling conventions
 146 |        ForeignFn : List TTImp -> FnOpt
 147 |        ||| Mark for export to a foreign language, takes a list of calling conventions
 148 |        ForeignExport : List TTImp -> FnOpt
 149 |        ||| assume safe to cancel arguments in unification
 150 |        Invertible : FnOpt
 151 |        Totality : TotalReq -> FnOpt
 152 |        ||| `%macro`
 153 |        Macro : FnOpt
 154 |        SpecArgs : List Name -> FnOpt
 155 |   ||| A name with an associated type
 156 |   public export
 157 |   data ITy : Type where
 158 |        MkTy : FC -> (n : WithFC Name) -> (ty : TTImp) -> ITy
 159 |
 160 |   %name ITy sig
 161 |
 162 |   public export
 163 |   data DataOpt : Type where
 164 |        ||| Determining arguments
 165 |        SearchBy : List1 Name -> DataOpt
 166 |        ||| Don't generate search hints for constructors
 167 |        NoHints : DataOpt
 168 |        ||| Auto implicit search must check result is unique
 169 |        UniqueSearch : DataOpt
 170 |        ||| Implemented externally
 171 |        External : DataOpt
 172 |        ||| Don't apply newtype optimization
 173 |        NoNewtype : DataOpt
 174 |
 175 |   %name DataOpt dopt
 176 |
 177 |   public export
 178 |   data Data : Type where
 179 |        MkData : FC -> (n : Name) -> (tycon : Maybe TTImp) ->
 180 |                 (opts : List DataOpt) ->
 181 |                 (datacons : List ITy) -> Data
 182 |        MkLater : FC -> (n : Name) -> (tycon : TTImp) -> Data
 183 |
 184 |   %name Data dt
 185 |
 186 |   public export
 187 |   data IField : Type where
 188 |        MkIField : FC -> Count -> PiInfo TTImp -> Name -> TTImp ->
 189 |                   IField
 190 |
 191 |   %name IField fld
 192 |
 193 |   public export
 194 |   data Record : Type where
 195 |        MkRecord : FC -> (n : Name) ->
 196 |                   (params : List (Name, Count, PiInfo TTImp, TTImp)) ->
 197 |                   (opts : List DataOpt) ->
 198 |                   (conName : Name) ->
 199 |                   (fields : List IField) ->
 200 |                   Record
 201 |   %name Record rec
 202 |
 203 |   public export
 204 |   data WithFlag = Syntactic
 205 |   ||| A clause in a function definition
 206 |   public export
 207 |   data Clause : Type where
 208 |        ||| A simple pattern
 209 |        PatClause : FC -> (lhs : TTImp) -> (rhs : TTImp) -> Clause
 210 |        ||| A pattern with views
 211 |        WithClause : FC -> (lhs : TTImp) ->
 212 |                     (rig : Count) -> (wval : TTImp) -> -- with'd expression (& quantity)
 213 |                     (prf : Maybe (Count, Name)) -> -- optional name for the proof (& quantity)
 214 |                     (flags : List WithFlag) ->
 215 |                     List Clause -> Clause
 216 |        ||| An impossible pattern
 217 |        ImpossibleClause : FC -> (lhs : TTImp) -> Clause
 218 |
 219 |   %name Clause cl
 220 |
 221 |   public export
 222 |   data WithDefault : (a : Type) -> (def : a) -> Type where
 223 |        DefaultedValue : WithDefault a def
 224 |        SpecifiedValue : a -> WithDefault a def
 225 |
 226 |   export
 227 |   specified : a -> WithDefault a def
 228 |   specified = SpecifiedValue
 229 |
 230 |   export
 231 |   defaulted : WithDefault a def
 232 |   defaulted = DefaultedValue
 233 |
 234 |   export
 235 |   collapseDefault : {def : a} -> WithDefault a def -> a
 236 |   collapseDefault DefaultedValue     = def
 237 |   collapseDefault (SpecifiedValue a) = a
 238 |
 239 |   export
 240 |   onWithDefault : (defHandler : Lazy b) -> (valHandler : a -> b) ->
 241 |                   WithDefault a def -> b
 242 |   onWithDefault defHandler _ DefaultedValue     = defHandler
 243 |   onWithDefault _ valHandler (SpecifiedValue v) = valHandler v
 244 |
 245 |   public export
 246 |   data IClaimData : Type where
 247 |     MkIClaimData : (rig  : Count) ->
 248 |                    (vis  : Visibility) ->
 249 |                    (opts : List FnOpt) ->
 250 |                    (type : ITy) ->
 251 |                    IClaimData
 252 |   ||| A top-level declaration
 253 |   public export
 254 |   data Decl : Type where
 255 |        ||| A type ascription, `a : b`.
 256 |        ||| Called a claim because of Curry Howard, the statement `x : p` is equivalent to `x` is a proof of `p`.
 257 |        IClaim : (claim : WithFC IClaimData) -> Decl
 258 |        ||| A data type declaration
 259 |        IData : FC -> (vis : WithDefault Visibility Private) -> Maybe TotalReq -> (cons : Data) -> Decl
 260 |        ||| A function body definition
 261 |        IDef : FC -> (f : Name) -> (cls : List Clause) -> Decl
 262 |        ||| A parameters block, e.g. `parameters {0 m : _} {auto _ : Monad m} (level : Nat)
 263 |        IParameters : FC -> (params : List (Name, Count, PiInfo TTImp, TTImp)) ->
 264 |                      (decls : List Decl) -> Decl
 265 |        ||| A record declaration
 266 |        ||| @ ns Nested namespace
 267 |        IRecord : FC ->
 268 |                  (ns : Maybe String) ->
 269 |                  (vis : WithDefault Visibility Private) ->
 270 |                  (totality : Maybe TotalReq) -> (rec : Record) -> Decl
 271 |        ||| A namespace declaration, `namespace ns where decls`
 272 |        INamespace : FC -> Namespace -> (decls : List Decl) -> Decl
 273 |        ||| A transformation rule declaration
 274 |        ITransform : FC -> Name -> TTImp -> TTImp -> Decl
 275 |        ||| A top-level elaborator script run, `%runElab`
 276 |        IRunElabDecl : FC -> TTImp -> Decl
 277 |        ||| A directive for enabling compile-time logging, `%logging "<topic>" <level>`
 278 |        ILog : Maybe (List String, Nat) -> Decl
 279 |        ||| A builtin declaration, `%builtin type name`
 280 |        IBuiltin : FC -> BuiltinType -> Name -> Decl
 281 |
 282 |   %name Decl decl
 283 |
 284 | %TTImpLit fromTTImp
 285 |
 286 | public export
 287 | fromTTImp : TTImp -> TTImp
 288 | fromTTImp s = s
 289 |
 290 | %declsLit fromDecls
 291 |
 292 | public export
 293 | fromDecls : List Decl -> List Decl
 294 | fromDecls decls = decls
 295 |
 296 | public export
 297 | getFC : TTImp -> FC
 298 | getFC (IVar fc _)                = fc
 299 | getFC (IPi fc _ _ _ _ _)         = fc
 300 | getFC (ILam fc _ _ _ _ _)        = fc
 301 | getFC (ILet fc _ _ _ _ _ _)      = fc
 302 | getFC (ICase fc _ _ _ _)         = fc
 303 | getFC (ILocal fc _ _)            = fc
 304 | getFC (IUpdate fc _ _)           = fc
 305 | getFC (IApp fc _ _)              = fc
 306 | getFC (INamedApp fc _ _ _)       = fc
 307 | getFC (IAutoApp fc _ _)          = fc
 308 | getFC (IWithApp fc _ _)          = fc
 309 | getFC (ISearch fc _)             = fc
 310 | getFC (IAlternative fc _ _)      = fc
 311 | getFC (IRewrite fc _ _)          = fc
 312 | getFC (IBindHere fc _ _)         = fc
 313 | getFC (IBindVar fc _)            = fc
 314 | getFC (IAs fc _ _ _ _)           = fc
 315 | getFC (IMustUnify fc _ _)        = fc
 316 | getFC (IDelayed fc _ _)          = fc
 317 | getFC (IDelay fc _)              = fc
 318 | getFC (IForce fc _)              = fc
 319 | getFC (IQuote fc _)              = fc
 320 | getFC (IQuoteName fc _)          = fc
 321 | getFC (IQuoteDecl fc _)          = fc
 322 | getFC (IUnquote fc _)            = fc
 323 | getFC (IPrimVal fc _)            = fc
 324 | getFC (IType fc)                 = fc
 325 | getFC (IHole fc _)               = fc
 326 | getFC (Implicit fc _)            = fc
 327 | getFC (IWithUnambigNames fc _ _) = fc
 328 |
 329 | public export
 330 | mapTopmostFC : (FC -> FC) -> TTImp -> TTImp
 331 | mapTopmostFC fcf $ IVar fc a                = IVar (fcf fc) a
 332 | mapTopmostFC fcf $ IPi fc a b c d e         = IPi (fcf fc) a b c d e
 333 | mapTopmostFC fcf $ ILam fc a b c d e        = ILam (fcf fc) a b c d e
 334 | mapTopmostFC fcf $ ILet fc a b c d e f      = ILet (fcf fc) a b c d e f
 335 | mapTopmostFC fcf $ ICase fc opts a b c      = ICase (fcf fc) opts a b c
 336 | mapTopmostFC fcf $ ILocal fc a b            = ILocal (fcf fc) a b
 337 | mapTopmostFC fcf $ IUpdate fc a b           = IUpdate (fcf fc) a b
 338 | mapTopmostFC fcf $ IApp fc a b              = IApp (fcf fc) a b
 339 | mapTopmostFC fcf $ INamedApp fc a b c       = INamedApp (fcf fc) a b c
 340 | mapTopmostFC fcf $ IAutoApp fc a b          = IAutoApp (fcf fc) a b
 341 | mapTopmostFC fcf $ IWithApp fc a b          = IWithApp (fcf fc) a b
 342 | mapTopmostFC fcf $ ISearch fc a             = ISearch (fcf fc) a
 343 | mapTopmostFC fcf $ IAlternative fc a b      = IAlternative (fcf fc) a b
 344 | mapTopmostFC fcf $ IRewrite fc a b          = IRewrite (fcf fc) a b
 345 | mapTopmostFC fcf $ IBindHere fc a b         = IBindHere (fcf fc) a b
 346 | mapTopmostFC fcf $ IBindVar fc a            = IBindVar (fcf fc) a
 347 | mapTopmostFC fcf $ IAs fc a b c d           = IAs (fcf fc) a b c d
 348 | mapTopmostFC fcf $ IMustUnify fc a b        = IMustUnify (fcf fc) a b
 349 | mapTopmostFC fcf $ IDelayed fc a b          = IDelayed (fcf fc) a b
 350 | mapTopmostFC fcf $ IDelay fc a              = IDelay (fcf fc) a
 351 | mapTopmostFC fcf $ IForce fc a              = IForce (fcf fc) a
 352 | mapTopmostFC fcf $ IQuote fc a              = IQuote (fcf fc) a
 353 | mapTopmostFC fcf $ IQuoteName fc a          = IQuoteName (fcf fc) a
 354 | mapTopmostFC fcf $ IQuoteDecl fc a          = IQuoteDecl (fcf fc) a
 355 | mapTopmostFC fcf $ IUnquote fc a            = IUnquote (fcf fc) a
 356 | mapTopmostFC fcf $ IPrimVal fc a            = IPrimVal (fcf fc) a
 357 | mapTopmostFC fcf $ IType fc                 = IType (fcf fc)
 358 | mapTopmostFC fcf $ IHole fc a               = IHole (fcf fc) a
 359 | mapTopmostFC fcf $ Implicit fc a            = Implicit (fcf fc) a
 360 | mapTopmostFC fcf $ IWithUnambigNames fc a b = IWithUnambigNames (fcf fc) a b
 361 |
 362 | public export
 363 | Eq BindMode where
 364 |   PI c    == PI c'   = c == c'
 365 |   PATTERN == PATTERN = True
 366 |   NONE    == NONE    = True
 367 |   _ == _ = False
 368 |
 369 | public export
 370 | Eq UseSide where
 371 |   UseLeft  == UseLeft  = True
 372 |   UseRight == UseRight = True
 373 |   _ == _ = False
 374 |
 375 | public export
 376 | Eq DotReason where
 377 |   NonLinearVar    == NonLinearVar    = True
 378 |   VarApplied      == VarApplied      = True
 379 |   NotConstructor  == NotConstructor  = True
 380 |   ErasedArg       == ErasedArg       = True
 381 |   UserDotted      == UserDotted      = True
 382 |   UnknownDot      == UnknownDot      = True
 383 |   UnderAppliedCon == UnderAppliedCon = True
 384 |   _ == _ = False
 385 |
 386 | public export
 387 | Eq WithFlag where
 388 |   Syntactic == Syntactic = True
 389 |
 390 | public export
 391 | Eq DataOpt where
 392 |   SearchBy ns == SearchBy ns' = ns == ns'
 393 |   NoHints == NoHints = True
 394 |   UniqueSearch == UniqueSearch = True
 395 |   External == External = True
 396 |   NoNewtype == NoNewtype = True
 397 |   _ == _ = False
 398 |
 399 | public export
 400 | Eq a => Eq (WithDefault a def) where
 401 |   DefaultedValue   == DefaultedValue   = True
 402 |   DefaultedValue   == SpecifiedValue _ = False
 403 |   SpecifiedValue _ == DefaultedValue   = False
 404 |   SpecifiedValue x == SpecifiedValue y = x == y
 405 |
 406 | public export
 407 | Ord a => Ord (WithDefault a def) where
 408 |   compare DefaultedValue   DefaultedValue       = EQ
 409 |   compare DefaultedValue   (SpecifiedValue _)   = LT
 410 |   compare (SpecifiedValue _) DefaultedValue     = GT
 411 |   compare (SpecifiedValue x) (SpecifiedValue y) = compare x y
 412 |
 413 | public export
 414 | {def : a} -> (Show a) => Show (WithDefault a def) where
 415 |   show (SpecifiedValue x) = show x
 416 |   show DefaultedValue     = show def
 417 |
 418 | public export
 419 | Eq a => Eq (PiInfo a) where
 420 |   ImplicitArg   == ImplicitArg = True
 421 |   ExplicitArg   == ExplicitArg = True
 422 |   AutoImplicit  == AutoImplicit = True
 423 |   DefImplicit t == DefImplicit t' = t == t'
 424 |   _ == _ = False
 425 |
 426 | parameters {auto eqTTImp : Eq TTImp}
 427 |   public export
 428 |   Eq Clause where
 429 |     PatClause _ lhs rhs == PatClause _ lhs' rhs' =
 430 |       lhs == lhs' && rhs == rhs'
 431 |     WithClause _ l r w p f cs == WithClause _ l' r' w' p' f' cs' =
 432 |       l == l' && r == r' && w == w' && p == p' && f == f' && (assert_total $ cs == cs')
 433 |     ImpossibleClause _ l == ImpossibleClause _ l' = l == l'
 434 |     _ == _ = False
 435 |
 436 |   public export
 437 |   Eq IFieldUpdate where
 438 |     ISetField p t == ISetField p' t' =
 439 |       p == p' && t == t'
 440 |     ISetFieldApp p t == ISetFieldApp p' t' =
 441 |       p == p' && t == t'
 442 |     _ == _ = False
 443 |
 444 |   public export
 445 |   Eq AltType where
 446 |     FirstSuccess    == FirstSuccess     = True
 447 |     Unique          == Unique           = True
 448 |     UniqueDefault t == UniqueDefault t' = t == t'
 449 |     _ == _ = False
 450 |
 451 |   public export
 452 |   Eq FnOpt where
 453 |     Inline == Inline = True
 454 |     NoInline == NoInline = True
 455 |     Deprecate == Deprecate = True
 456 |     TCInline == TCInline = True
 457 |     Hint b == Hint b' = b == b'
 458 |     GlobalHint b == GlobalHint b' = b == b'
 459 |     ExternFn == ExternFn = True
 460 |     ForeignFn es == ForeignFn es' = es == es'
 461 |     ForeignExport es == ForeignExport es' = es == es'
 462 |     Invertible == Invertible = True
 463 |     Totality tr == Totality tr' = tr == tr'
 464 |     Macro == Macro = True
 465 |     SpecArgs ns == SpecArgs ns' = ns == ns'
 466 |     _ == _ = False
 467 |
 468 |   public export
 469 |   Eq ITy where
 470 |     MkTy _ n ty == MkTy _ n' ty' = n.value == n'.value && ty == ty'
 471 |
 472 |   public export
 473 |   Eq Data where
 474 |     MkData _ n tc os dc == MkData _ n' tc' os' dc' =
 475 |       n == n' && tc == tc' && os == os' && dc == dc'
 476 |     MkLater _ n tc == MkLater _ n' tc' =
 477 |       n == n' && tc == tc'
 478 |     _ == _ = False
 479 |
 480 |   public export
 481 |   Eq IField where
 482 |     MkIField _ c pi n e == MkIField _ c' pi' n' e' =
 483 |       c == c' && pi == pi' && n == n' && e == e'
 484 |
 485 |   public export
 486 |   Eq Record where
 487 |     MkRecord _ n ps opts cn fs == MkRecord _ n' ps' opts' cn' fs' =
 488 |       n == n' && ps == ps' && opts == opts' && cn == cn' && fs == fs'
 489 |
 490 |   public export
 491 |   Eq IClaimData where
 492 |     MkIClaimData c v fos t == MkIClaimData c' v' fos' t' =
 493 |       c == c' && v == v' && fos == fos' && t == t'
 494 |
 495 |   public export
 496 |   Eq Decl where
 497 |     IClaim c == IClaim c' = c.value == c'.value
 498 |     IData _ v t d == IData _ v' t' d' =
 499 |       v == v' && t == t' && d == d'
 500 |     IDef _ n cs == IDef _ n' cs' =
 501 |       n == n' && cs == cs'
 502 |     IParameters _ ps ds == IParameters _ ps' ds' =
 503 |       ps == ps' && (assert_total $ ds == ds')
 504 |     IRecord _ ns v tr r == IRecord _ ns' v' tr' r' =
 505 |       ns == ns' && v == v' && tr == tr' && r == r'
 506 |     INamespace _ ns ds == INamespace _ ns' ds' =
 507 |       ns == ns' && (assert_total $ ds == ds')
 508 |     ITransform _ n f t == ITransform _ n' f' t' =
 509 |       n == n' && f == f' && t == t'
 510 |     IRunElabDecl _ e == IRunElabDecl _ e' = e == e'
 511 |     ILog p == ILog p' = p == p'
 512 |     IBuiltin _ t n == IBuiltin _ t' n' =
 513 |       t == t' && n == n'
 514 |     _ == _ = False
 515 |
 516 | public export
 517 | Eq TTImp where
 518 |   IVar _ v == IVar _ v' = v == v'
 519 |   IPi _ c i n a r == IPi _ c' i' n' a' r' =
 520 |     c == c' && (assert_total $ i == i') && n == n' && a == a' && r == r'
 521 |   ILam _ c i n a r == ILam _ c' i' n' a' r' =
 522 |     c == c' && (assert_total $ i == i') && n == n' && a == a' && r == r'
 523 |   ILet _ _ c n ty val s == ILet _ _ c' n' ty' val' s' =
 524 |     c == c' && n == n' && ty == ty' && val == val' && s == s'
 525 |   ICase _ _ t ty cs == ICase _ _ t' ty' cs'
 526 |     = t == t' && ty == ty' && (assert_total $ cs == cs')
 527 |   ILocal _ ds e == ILocal _ ds' e' =
 528 |     (assert_total $ ds == ds') && e == e'
 529 |   IUpdate _ fs t == IUpdate _ fs' t' =
 530 |     (assert_total $ fs == fs') && t == t'
 531 |
 532 |   IApp _ f x == IApp _ f' x' = f == f' && x == x'
 533 |   INamedApp _ f n x == INamedApp _ f' n' x' =
 534 |     f == f' && n == n' && x == x'
 535 |   IAutoApp _ f x == IAutoApp _ f' x' = f == f' && x == x'
 536 |   IWithApp _ f x == IWithApp _ f' x' = f == f' && x == x'
 537 |
 538 |   ISearch _ n == ISearch _ n' = n == n'
 539 |   IAlternative _ t as == IAlternative _ t' as' =
 540 |     (assert_total $ t == t') && (assert_total $ as == as')
 541 |   IRewrite _ p q == IRewrite _ p' q' =
 542 |     p == p' && q == q'
 543 |
 544 |   IBindHere _ m t == IBindHere _ m' t' =
 545 |     m == m' && t == t'
 546 |   IBindVar _ s == IBindVar _ s' = s == s'
 547 |   IAs _ _ u n t == IAs _ _ u' n' t' =
 548 |     u == u' && n == n' && t == t'
 549 |   IMustUnify _ r t == IMustUnify _ r' t' =
 550 |     r == r' && t == t'
 551 |
 552 |   IDelayed _ r t == IDelayed _ r' t' = r == r' && t == t'
 553 |   IDelay _ t == IDelay _ t' = t == t'
 554 |   IForce _ t == IForce _ t' = t == t'
 555 |
 556 |   IQuote _ tm == IQuote _ tm' = tm == tm'
 557 |   IQuoteName _ n == IQuoteName _ n' = n == n'
 558 |   IQuoteDecl _ ds == IQuoteDecl _ ds' = assert_total $ ds == ds'
 559 |   IUnquote _ tm == IUnquote _ tm' = tm == tm'
 560 |
 561 |   IPrimVal _ c == IPrimVal _ c' = c == c'
 562 |   IType _ == IType _ = True
 563 |   IHole _ s == IHole _ s' = s == s'
 564 |
 565 |   Implicit _ b == Implicit _ b' = b == b'
 566 |   IWithUnambigNames _ ns t == IWithUnambigNames _ ns' t' =
 567 |     map snd ns == map snd ns' && t == t'
 568 |
 569 |   _ == _ = False
 570 |
 571 | public export
 572 | data Mode = InDecl | InCase
 573 |
 574 | mutual
 575 |
 576 |   public export
 577 |   Show IField where
 578 |     show (MkIField fc rig pinfo nm s) =
 579 |       showPiInfo {wrapExplicit=False} pinfo (showCount rig "\{show nm} : \{show s}")
 580 |
 581 |   public export
 582 |   Show Record where
 583 |     show (MkRecord fc n params opts conName fields) -- TODO: print opts
 584 |       = unwords
 585 |       [ "record", show n
 586 |       , unwords (map (\ (nm, rig, pinfo, ty) =>
 587 |                        showPiInfo pinfo (showCount rig "\{show nm} : \{show ty}"))
 588 |                 params)
 589 |       , "where"
 590 |       , "{"
 591 |       , "constructor", show conName, "; "
 592 |       , joinBy "; " (map show fields)
 593 |       , "}"
 594 |       ]
 595 |
 596 |   public export
 597 |   Show Data where
 598 |     show (MkData fc n tycon opts datacons) -- TODO: print opts
 599 |       = unwords
 600 |       [ "data", show n, ":", show tycon, "where"
 601 |       , "{", joinBy "; " (map show datacons), "}"
 602 |       ]
 603 |     show (MkLater fc n tycon) = unwords [ "data", show n, ":", show tycon ]
 604 |
 605 |   public export
 606 |   Show ITy where
 607 |     show (MkTy fc n ty) = "\{show n.value} : \{show ty}"
 608 |
 609 |   Show IClaimData where
 610 |     show (MkIClaimData rig vis xs sig)
 611 |       = unwords [ show vis
 612 |                 , showCount rig (show sig) ]
 613 |
 614 |   public export
 615 |   Show Decl where
 616 |     show (IClaim claim) = show claim.value
 617 |     show (IData fc vis treq dt)
 618 |       = unwords [ show vis
 619 |                 , showTotalReq treq (show dt)
 620 |                 ]
 621 |     show (IDef fc nm xs) = joinBy "; " (map (showClause InDecl) xs)
 622 |     show (IParameters fc params decls)
 623 |       = unwords
 624 |       [ "parameters"
 625 |       , unwords (map (\ (nm, rig, pinfo, ty) =>
 626 |                        showPiInfo pinfo (showCount rig "\{show nm} : \{show ty}"))
 627 |                 params)
 628 |       , "{"
 629 |       , joinBy "; " (assert_total $ map show decls)
 630 |       , "}"
 631 |       ]
 632 |     show (IRecord fc x vis treq rec)
 633 |       = unwords [ show vis, showTotalReq treq (show rec) ]
 634 |     show (INamespace fc ns decls)
 635 |       = unwords
 636 |       [ "namespace", show ns
 637 |       , "{", joinBy "; " (assert_total $ map show decls), "}" ]
 638 |     show (ITransform fc nm s t) = #"%transform "\{show nm}" \{show s} = \{show t}"#
 639 |     show (IRunElabDecl fc s) = "%runElab \{show s}"
 640 |     show (ILog loglvl) = case loglvl of
 641 |       Nothing => "%logging off"
 642 |       Just ([], lvl) => "%logging \{show lvl}"
 643 |       Just (topic, lvl) => "%logging \{joinBy "." topic} \{show lvl}"
 644 |     show (IBuiltin fc bty nm) = "%builtin \{show bty} \{show nm}"
 645 |
 646 |   public export
 647 |   Show IFieldUpdate where
 648 |     show (ISetField path s) = "\{joinBy "->" path} := \{show s}"
 649 |     show (ISetFieldApp path s) = "\{joinBy "->" path} $= \{show s}"
 650 |
 651 |   public export
 652 |   showClause : Mode -> Clause -> String
 653 |   showClause mode (PatClause fc lhs rhs) = "\{show lhs} \{showSep mode} \{show rhs}" where
 654 |     showSep : Mode -> String
 655 |     showSep InDecl = "="
 656 |     showSep InCase = "=>"
 657 |   showClause mode (WithClause fc lhs rig wval prf flags cls) -- TODO print flags
 658 |       = unwords
 659 |       [ show lhs, "with"
 660 |         -- TODO: remove `the` after fix idris-lang/Idris2#3418
 661 |       , showCount rig $ maybe id (the (_ -> _) $ \(rg, nm) => (++ " proof \{showCount rg $ show nm}")) prf
 662 |                       $ showParens True (show wval)
 663 |       , "{", joinBy "; " (assert_total $ map (showClause mode) cls), "}"
 664 |       ]
 665 |   showClause mode (ImpossibleClause fc lhs) = "\{show lhs} impossible"
 666 |
 667 |   collectPis : Count -> PiInfo TTImp -> SnocList Name -> TTImp -> TTImp -> (List Name, TTImp)
 668 |   collectPis rig pinfo xs argTy t@(IPi fc rig' pinfo' x argTy' retTy)
 669 |     = ifThenElse (rig == rig' && pinfo == pinfo' && argTy == argTy')
 670 |          (collectPis rig pinfo (xs :< fromMaybe (UN Underscore) x) argTy retTy)
 671 |          (xs <>> [], t)
 672 |   collectPis rig pinfo xs argTy t = (xs <>> [], t)
 673 |
 674 |   showIApps : TTImp -> List String -> String
 675 |   showIApps (IApp _ f t) ts = showIApps f (assert_total (showPrec App t) :: ts)
 676 |   showIApps (IVar _ nm) [a,b] =
 677 |     if isOp nm then unwords [a, showPrefix False nm, b]
 678 |     else unwords [showPrefix True nm, a, b]
 679 |   showIApps f ts = unwords (show f :: ts)
 680 |
 681 |   public export
 682 |   Show TTImp where
 683 |     showPrec d (IVar fc nm) = showPrefix True nm
 684 |     showPrec d (IPi fc MW ExplicitArg Nothing argTy retTy)
 685 |       = showParens (d > Open) $ "\{showPrec Dollar argTy} -> \{show retTy}"
 686 |     showPrec d (IPi fc MW AutoImplicit Nothing argTy retTy)
 687 |       = showParens (d > Open) $ "\{showPrec Dollar argTy} => \{show retTy}"
 688 |     showPrec d (IPi fc rig pinfo x argTy retTy)
 689 |       = showParens (d > Open) $
 690 |           let (xs, retTy) = collectPis rig pinfo [<fromMaybe (UN Underscore) x] argTy retTy in
 691 |           assert_total (showPiInfo pinfo "\{showCount rig $ joinBy ", " (show <$> xs)} : \{show argTy}")
 692 |           ++ " -> \{assert_total $ show retTy}"
 693 |     showPrec d (ILam fc rig pinfo x argTy lamTy)
 694 |       = showParens (d > Open) $
 695 |           "\\ \{showCount rig $ show (fromMaybe (UN Underscore) x)} => \{show lamTy}"
 696 |     showPrec d (ILet fc lhsFC rig nm nTy nVal scope)
 697 |       = showParens (d > Open) $
 698 |           "let \{showCount rig (show nm)} : \{show nTy} = \{show nVal} in \{show scope}"
 699 |     showPrec d (ICase fc _ s ty xs)
 700 |       = showParens (d > Open) $
 701 |           unwords $ [ "case", show s ] ++ typeFor ty ++ [ "of", "{"
 702 |                     , joinBy "; " (assert_total $ map (showClause InCase) xs)
 703 |                     , "}"
 704 |                     ]
 705 |           where
 706 |             typeFor : TTImp -> List String
 707 |             typeFor $ Implicit _ False = []
 708 |             typeFor ty = [ "{-", ":", show ty, "-}" ]
 709 |     showPrec d (ILocal fc decls s)
 710 |       = showParens (d > Open) $
 711 |           unwords [ "let", joinBy "; " (assert_total $ map show decls)
 712 |                   , "in", show s
 713 |                   ]
 714 |     showPrec d (IUpdate fc upds s)
 715 |       = showParens (d > Open) $
 716 |           unwords [ "{", joinBy ", " $ assert_total (map show upds), "}"
 717 |                   , showPrec App s ]
 718 |     showPrec d (IApp fc f t)
 719 |       = showParens (d >= App) $ assert_total $ showIApps f [showPrec App t]
 720 |     showPrec d (INamedApp fc f nm t)
 721 |       = showParens (d >= App) $ "\{show f} {\{show nm} = \{show t}}"
 722 |     showPrec d (IAutoApp fc f t)
 723 |       = showParens (d >= App) $ "\{show f} @{\{show t}}"
 724 |     showPrec d (IWithApp fc f t)
 725 |       = showParens (d >= App) $ "\{show f} | \{showPrec App t}"
 726 |     showPrec d (ISearch fc depth) = "%search"
 727 |     showPrec d (IAlternative fc x xs) = "<\{show (length xs)} alts>"
 728 |     showPrec d (IRewrite fc s t)
 729 |       = showParens (d > Open) "rewrite \{show s} in \{show t}"
 730 |     showPrec d (IBindHere fc bm s) = showPrec d s
 731 |     showPrec d (IBindVar fc x) = showPrec d x
 732 |     showPrec d (IAs fc nameFC side nm s)
 733 |       = "\{show nm}@\{showPrec App s}"
 734 |     showPrec d (IMustUnify fc dr s) = ".(\{show s})"
 735 |     showPrec d (IDelayed fc LInf s) = showCon d "Inf" $ assert_total $ showArg s
 736 |     showPrec d (IDelayed fc LLazy s) = showCon d "Lazy" $ assert_total $ showArg s
 737 |     showPrec d (IDelayed fc LUnknown s) = "({- unknown lazy -} \{showPrec Open s})"
 738 |     showPrec d (IDelay fc s) = showCon d "Delay" $ assert_total $ showArg s
 739 |     showPrec d (IForce fc s) = showCon d "Force" $ assert_total $ showArg s
 740 |     showPrec d (IQuote fc s) = "`(\{show s})"
 741 |     showPrec d (IQuoteName fc nm) = "`{\{show nm}}"
 742 |     showPrec d (IQuoteDecl fc xs) = "`[\{joinBy "; " (assert_total $ map show xs)}]"
 743 |     showPrec d (IUnquote fc s) = "~(\{show s})"
 744 |     showPrec d (IPrimVal fc c) = show c
 745 |     showPrec d (IType fc) = "Type"
 746 |     showPrec d (IHole fc str) = "?" ++ str
 747 |     showPrec d (Implicit fc b) = ifThenElse b "_" "?"
 748 |     showPrec d (IWithUnambigNames fc ns s) = case ns of
 749 |       [] => show s
 750 |       [(_,x)] => "with \{show x} \{show s}"
 751 |       _   => "with [\{joinBy ", " $ map (show . snd) ns}] \{show s}"
 752 |
 753 | public export
 754 | data Argument a
 755 |   = Arg FC a
 756 |   | NamedArg FC Name a
 757 |   | AutoArg FC a
 758 |
 759 | public export
 760 | isExplicit : Argument a -> Maybe (FC, a)
 761 | isExplicit (Arg fc a) = pure (fc, a)
 762 | isExplicit _ = Nothing
 763 |
 764 | public export
 765 | fromPiInfo : FC -> PiInfo t -> Maybe Name -> a -> Maybe (Argument a)
 766 | fromPiInfo fc ImplicitArg (Just nm) a = pure (NamedArg fc nm a)
 767 | fromPiInfo fc ExplicitArg _ a = pure (Arg fc a)
 768 | fromPiInfo fc AutoImplicit _ a = pure (AutoArg fc a)
 769 | fromPiInfo fc (DefImplicit _) (Just nm) a = pure (NamedArg fc nm a)
 770 | fromPiInfo _ _ _ _ = Nothing
 771 |
 772 | public export
 773 | Functor Argument where
 774 |   map f (Arg fc a) = Arg fc (f a)
 775 |   map f (NamedArg fc nm a) = NamedArg fc nm (f a)
 776 |   map f (AutoArg fc a) = AutoArg fc (f a)
 777 |
 778 | public export
 779 | Foldable Argument where
 780 |   foldr f acc (Arg _ e) = f e acc
 781 |   foldr f acc (NamedArg _ n e) = f e acc
 782 |   foldr f acc (AutoArg _ e) = f e acc
 783 |
 784 | public export
 785 | Traversable Argument where
 786 |   traverse f (Arg fc e) = Arg fc <$> f e
 787 |   traverse f (NamedArg fc n e) = NamedArg fc n <$> f e
 788 |   traverse f (AutoArg fc e) = AutoArg fc <$> f e
 789 |
 790 | public export
 791 | iApp : TTImp -> Argument TTImp -> TTImp
 792 | iApp f (Arg fc t) = IApp fc f t
 793 | iApp f (NamedArg fc nm t) = INamedApp fc f nm t
 794 | iApp f (AutoArg fc t) = IAutoApp fc f t
 795 |
 796 | public export
 797 | unArg : Argument a -> a
 798 | unArg (Arg _ x) = x
 799 | unArg (NamedArg _ _ x) = x
 800 | unArg (AutoArg _ x) = x
 801 |
 802 | ||| We often apply multiple arguments, this makes things simpler
 803 | public export
 804 | apply : TTImp -> List (Argument TTImp) -> TTImp
 805 | apply = foldl iApp
 806 |
 807 | public export
 808 | data IsAppView : (FC, Name) -> SnocList (Argument TTImp) -> TTImp -> Type where
 809 |   AVVar : IsAppView (fc, t) [<] (IVar fc t)
 810 |   AVApp : IsAppView x ts f -> IsAppView x (ts :< Arg fc t) (IApp fc f t)
 811 |   AVNamedApp : IsAppView x ts f -> IsAppView x (ts :< NamedArg fc n t) (INamedApp fc f n t)
 812 |   AVAutoApp : IsAppView x ts f -> IsAppView x (ts :< AutoArg fc t) (IAutoApp fc f a)
 813 |
 814 | public export
 815 | record AppView (t : TTImp) where
 816 |   constructor MkAppView
 817 |   head : (FC, Name)
 818 |   args : SnocList (Argument TTImp)
 819 |   0 isAppView : IsAppView head args t
 820 |
 821 | public export
 822 | appView : (t : TTImp) -> Maybe (AppView t)
 823 | appView (IVar fc f) = Just (MkAppView (fc, f) [<] AVVar)
 824 | appView (IApp fc f t) = do
 825 |   (MkAppView x ts prf) <- appView f
 826 |   pure (MkAppView x (ts :< Arg fc t) (AVApp prf))
 827 | appView (INamedApp fc f n t) = do
 828 |   (MkAppView x ts prf) <- appView f
 829 |   pure (MkAppView x (ts :< NamedArg fc n t) (AVNamedApp prf))
 830 | appView (IAutoApp fc f t) = do
 831 |   (MkAppView x ts prf) <- appView f
 832 |   pure (MkAppView x (ts :< AutoArg fc t) (AVAutoApp prf))
 833 | appView _ = Nothing
 834 |
 835 | parameters (f : TTImp -> TTImp)
 836 |
 837 |   public export
 838 |   mapTTImp : TTImp -> TTImp
 839 |
 840 |   public export
 841 |   mapPiInfo : PiInfo TTImp -> PiInfo TTImp
 842 |   mapPiInfo ImplicitArg = ImplicitArg
 843 |   mapPiInfo ExplicitArg = ExplicitArg
 844 |   mapPiInfo AutoImplicit = AutoImplicit
 845 |   mapPiInfo (DefImplicit t) = DefImplicit (mapTTImp t)
 846 |
 847 |   public export
 848 |   mapClause : Clause -> Clause
 849 |   mapClause (PatClause fc lhs rhs) = PatClause fc (mapTTImp lhs) (mapTTImp rhs)
 850 |   mapClause (WithClause fc lhs rig wval prf flags cls)
 851 |     = WithClause fc (mapTTImp lhs) rig (mapTTImp wval) prf flags (assert_total $ map mapClause cls)
 852 |   mapClause (ImpossibleClause fc lhs) = ImpossibleClause fc (mapTTImp lhs)
 853 |
 854 |   public export
 855 |   mapITy : ITy -> ITy
 856 |   mapITy (MkTy fc n ty) = MkTy fc n (mapTTImp ty)
 857 |
 858 |   public export
 859 |   mapFnOpt : FnOpt -> FnOpt
 860 |   mapFnOpt Inline = Inline
 861 |   mapFnOpt NoInline = NoInline
 862 |   mapFnOpt Deprecate = Deprecate
 863 |   mapFnOpt TCInline = TCInline
 864 |   mapFnOpt (Hint b) = Hint b
 865 |   mapFnOpt (GlobalHint b) = GlobalHint b
 866 |   mapFnOpt ExternFn = ExternFn
 867 |   mapFnOpt (ForeignFn ts) = ForeignFn (map mapTTImp ts)
 868 |   mapFnOpt (ForeignExport ts) = ForeignExport (map mapTTImp ts)
 869 |   mapFnOpt Invertible = Invertible
 870 |   mapFnOpt (Totality treq) = Totality treq
 871 |   mapFnOpt Macro = Macro
 872 |   mapFnOpt (SpecArgs ns) = SpecArgs ns
 873 |
 874 |   public export
 875 |   mapData : Data -> Data
 876 |   mapData (MkData fc n tycon opts datacons)
 877 |     = MkData fc n (map mapTTImp tycon) opts (map mapITy datacons)
 878 |   mapData (MkLater fc n tycon) = MkLater fc n (mapTTImp tycon)
 879 |
 880 |   public export
 881 |   mapIField : IField -> IField
 882 |   mapIField (MkIField fc rig pinfo n t) = MkIField fc rig (mapPiInfo pinfo) n (mapTTImp t)
 883 |
 884 |   public export
 885 |   mapRecord : Record -> Record
 886 |   mapRecord (MkRecord fc n params opts conName fields)
 887 |     = MkRecord fc n (map (map $ map $ bimap mapPiInfo mapTTImp) params) opts conName (map mapIField fields)
 888 |
 889 |   mapIClaimData : IClaimData -> IClaimData
 890 |   mapIClaimData (MkIClaimData rig vis opts ty)
 891 |     = MkIClaimData rig vis (map mapFnOpt opts) (mapITy ty)
 892 |
 893 |   public export
 894 |   mapDecl : Decl -> Decl
 895 |   mapDecl (IClaim claim) = IClaim $ map mapIClaimData claim
 896 |   mapDecl (IData fc vis mtreq dat) = IData fc vis mtreq (mapData dat)
 897 |   mapDecl (IDef fc n cls) = IDef fc n (map mapClause cls)
 898 |   mapDecl (IParameters fc params xs) = IParameters fc params (assert_total $ map mapDecl xs)
 899 |   mapDecl (IRecord fc mstr x y rec) = IRecord fc mstr x y (mapRecord rec)
 900 |   mapDecl (INamespace fc mi xs) = INamespace fc mi (assert_total $ map mapDecl xs)
 901 |   mapDecl (ITransform fc n t u) = ITransform fc n (mapTTImp t) (mapTTImp u)
 902 |   mapDecl (IRunElabDecl fc t) = IRunElabDecl fc (mapTTImp t)
 903 |   mapDecl (ILog x) = ILog x
 904 |   mapDecl (IBuiltin fc x n) = IBuiltin fc x n
 905 |
 906 |   public export
 907 |   mapIFieldUpdate : IFieldUpdate -> IFieldUpdate
 908 |   mapIFieldUpdate (ISetField path t) = ISetField path (mapTTImp t)
 909 |   mapIFieldUpdate (ISetFieldApp path t) = ISetFieldApp path (mapTTImp t)
 910 |
 911 |   public export
 912 |   mapAltType : AltType -> AltType
 913 |   mapAltType FirstSuccess = FirstSuccess
 914 |   mapAltType Unique = Unique
 915 |   mapAltType (UniqueDefault t) = UniqueDefault (mapTTImp t)
 916 |
 917 |   mapTTImp t@(IVar _ _) = f t
 918 |   mapTTImp (IPi fc rig pinfo x argTy retTy)
 919 |     = f $ IPi fc rig (mapPiInfo pinfo) x (mapTTImp argTy) (mapTTImp retTy)
 920 |   mapTTImp (ILam fc rig pinfo x argTy lamTy)
 921 |     = f $ ILam fc rig (mapPiInfo pinfo) x (mapTTImp argTy) (mapTTImp lamTy)
 922 |   mapTTImp (ILet fc lhsFC rig n nTy nVal scope)
 923 |     = f $ ILet fc lhsFC rig n (mapTTImp nTy) (mapTTImp nVal) (mapTTImp scope)
 924 |   mapTTImp (ICase fc opts t ty cls)
 925 |     = f $ ICase fc opts (mapTTImp t) (mapTTImp ty) (assert_total $ map mapClause cls)
 926 |   mapTTImp (ILocal fc xs t)
 927 |     = f $ ILocal fc (assert_total $ map mapDecl xs) (mapTTImp t)
 928 |   mapTTImp (IUpdate fc upds t) = f $ IUpdate fc (assert_total map mapIFieldUpdate upds) (mapTTImp t)
 929 |   mapTTImp (IApp fc t u) = f $ IApp fc (mapTTImp t) (mapTTImp u)
 930 |   mapTTImp (IAutoApp fc t u) = f $ IAutoApp fc (mapTTImp t) (mapTTImp u)
 931 |   mapTTImp (INamedApp fc t n u) = f $ INamedApp fc (mapTTImp t) n (mapTTImp u)
 932 |   mapTTImp (IWithApp fc t u) = f $ IWithApp fc (mapTTImp t) (mapTTImp u)
 933 |   mapTTImp (ISearch fc depth) = f $ ISearch fc depth
 934 |   mapTTImp (IAlternative fc alt ts) = f $ IAlternative fc (mapAltType alt) (assert_total map mapTTImp ts)
 935 |   mapTTImp (IRewrite fc t u) = f $ IRewrite fc (mapTTImp t) (mapTTImp u)
 936 |   mapTTImp (IBindHere fc bm t) = f $ IBindHere fc bm (mapTTImp t)
 937 |   mapTTImp (IBindVar fc str) = f $ IBindVar fc str
 938 |   mapTTImp (IAs fc nameFC side n t) = f $ IAs fc nameFC side n (mapTTImp t)
 939 |   mapTTImp (IMustUnify fc x t) = f $ IMustUnify fc x (mapTTImp t)
 940 |   mapTTImp (IDelayed fc lz t) = f $ IDelayed fc lz (mapTTImp t)
 941 |   mapTTImp (IDelay fc t) = f $ IDelay fc (mapTTImp t)
 942 |   mapTTImp (IForce fc t) = f $ IForce fc (mapTTImp t)
 943 |   mapTTImp (IQuote fc t) = f $ IQuote fc (mapTTImp t)
 944 |   mapTTImp (IQuoteName fc n) = f $ IQuoteName fc n
 945 |   mapTTImp (IQuoteDecl fc xs) = f $ IQuoteDecl fc (assert_total $ map mapDecl xs)
 946 |   mapTTImp (IUnquote fc t) = f $ IUnquote fc (mapTTImp t)
 947 |   mapTTImp (IPrimVal fc c) = f $ IPrimVal fc c
 948 |   mapTTImp (IType fc) = f $ IType fc
 949 |   mapTTImp (IHole fc str) = f $ IHole fc str
 950 |   mapTTImp (Implicit fc bindIfUnsolved) = f $ Implicit fc bindIfUnsolved
 951 |   mapTTImp (IWithUnambigNames fc xs t) = f $ IWithUnambigNames fc xs (mapTTImp t)
 952 |
 953 | parameters {0 m : Type -> Type} {auto apl : Applicative m} (f : (original : TTImp) -> m TTImp -> m TTImp)
 954 |
 955 |   public export
 956 |   mapATTImp' : TTImp -> m TTImp
 957 |
 958 |   public export
 959 |   mapMPiInfo : PiInfo TTImp -> m (PiInfo TTImp)
 960 |   mapMPiInfo ImplicitArg = pure ImplicitArg
 961 |   mapMPiInfo ExplicitArg = pure ExplicitArg
 962 |   mapMPiInfo AutoImplicit = pure AutoImplicit
 963 |   mapMPiInfo (DefImplicit t) = DefImplicit <$> mapATTImp' t
 964 |
 965 |   public export
 966 |   mapMClause : Clause -> m Clause
 967 |   mapMClause (PatClause fc lhs rhs) = PatClause fc <$> mapATTImp' lhs <*> mapATTImp' rhs
 968 |   mapMClause (WithClause fc lhs rig wval prf flags cls)
 969 |     = WithClause fc
 970 |     <$> mapATTImp' lhs
 971 |     <*> pure rig
 972 |     <*> mapATTImp' wval
 973 |     <*> pure prf
 974 |     <*> pure flags
 975 |     <*> assert_total (traverse mapMClause cls)
 976 |   mapMClause (ImpossibleClause fc lhs) = ImpossibleClause fc <$> mapATTImp' lhs
 977 |
 978 |   public export
 979 |   mapMITy : ITy -> m ITy
 980 |   mapMITy (MkTy fc n ty) = MkTy fc n <$> mapATTImp' ty
 981 |
 982 |   public export
 983 |   mapMFnOpt : FnOpt -> m FnOpt
 984 |   mapMFnOpt Inline = pure Inline
 985 |   mapMFnOpt NoInline = pure NoInline
 986 |   mapMFnOpt Deprecate = pure Deprecate
 987 |   mapMFnOpt TCInline = pure TCInline
 988 |   mapMFnOpt (Hint b) = pure (Hint b)
 989 |   mapMFnOpt (GlobalHint b) = pure (GlobalHint b)
 990 |   mapMFnOpt ExternFn = pure ExternFn
 991 |   mapMFnOpt (ForeignFn ts) = ForeignFn <$> traverse mapATTImp' ts
 992 |   mapMFnOpt (ForeignExport ts) = ForeignExport <$> traverse mapATTImp' ts
 993 |   mapMFnOpt Invertible = pure Invertible
 994 |   mapMFnOpt (Totality treq) = pure (Totality treq)
 995 |   mapMFnOpt Macro = pure Macro
 996 |   mapMFnOpt (SpecArgs ns) = pure (SpecArgs ns)
 997 |
 998 |   public export
 999 |   mapMData : Data -> m Data
1000 |   mapMData (MkData fc n tycon opts datacons)
1001 |     = MkData fc n <$> traverse mapATTImp' tycon <*> pure opts <*> traverse mapMITy datacons
1002 |   mapMData (MkLater fc n tycon) = MkLater fc n <$> mapATTImp' tycon
1003 |
1004 |   public export
1005 |   mapMIField : IField -> m IField
1006 |   mapMIField (MkIField fc rig pinfo n t)
1007 |    = MkIField fc rig <$> mapMPiInfo pinfo <*> pure n <*> mapATTImp' t
1008 |
1009 |   public export
1010 |   mapMRecord : Record -> m Record
1011 |   mapMRecord (MkRecord fc n params opts conName fields)
1012 |     = MkRecord fc n
1013 |     <$> traverse (bitraverse pure $ bitraverse pure $ bitraverse mapMPiInfo mapATTImp') params
1014 |     <*> pure opts
1015 |     <*> pure conName
1016 |     <*> traverse mapMIField fields
1017 |
1018 |   mapMIClaimData : IClaimData -> m IClaimData
1019 |   mapMIClaimData (MkIClaimData rig vis opts ty)
1020 |     = MkIClaimData rig vis <$> traverse mapMFnOpt opts <*> mapMITy ty
1021 |
1022 |   public export
1023 |   mapMDecl : Decl -> m Decl
1024 |   mapMDecl (IClaim claim) = IClaim <$> traverse mapMIClaimData claim
1025 |   mapMDecl (IData fc vis mtreq dat) = IData fc vis mtreq <$> mapMData dat
1026 |   mapMDecl (IDef fc n cls) = IDef fc n <$> traverse mapMClause cls
1027 |   mapMDecl (IParameters fc params xs) = IParameters fc params <$> assert_total (traverse mapMDecl xs)
1028 |   mapMDecl (IRecord fc mstr x y rec) = IRecord fc mstr x y <$> mapMRecord rec
1029 |   mapMDecl (INamespace fc mi xs) = INamespace fc mi <$> assert_total (traverse mapMDecl xs)
1030 |   mapMDecl (ITransform fc n t u) = ITransform fc n <$> mapATTImp' t <*> mapATTImp' u
1031 |   mapMDecl (IRunElabDecl fc t) = IRunElabDecl fc <$> mapATTImp' t
1032 |   mapMDecl (ILog x) = pure (ILog x)
1033 |   mapMDecl (IBuiltin fc x n) = pure (IBuiltin fc x n)
1034 |
1035 |   public export
1036 |   mapMIFieldUpdate : IFieldUpdate -> m IFieldUpdate
1037 |   mapMIFieldUpdate (ISetField path t) = ISetField path <$> mapATTImp' t
1038 |   mapMIFieldUpdate (ISetFieldApp path t) = ISetFieldApp path <$> mapATTImp' t
1039 |
1040 |   public export
1041 |   mapMAltType : AltType -> m AltType
1042 |   mapMAltType FirstSuccess = pure FirstSuccess
1043 |   mapMAltType Unique = pure Unique
1044 |   mapMAltType (UniqueDefault t) = UniqueDefault <$> mapATTImp' t
1045 |
1046 |   mapATTImp' t@(IVar _ _) = f t $ pure t
1047 |   mapATTImp' o@(IPi fc rig pinfo x argTy retTy)
1048 |     = f o $ IPi fc rig <$> mapMPiInfo pinfo <*> pure x <*> mapATTImp' argTy <*> mapATTImp' retTy
1049 |   mapATTImp' o@(ILam fc rig pinfo x argTy lamTy)
1050 |     = f o $ ILam fc rig <$> mapMPiInfo pinfo <*> pure x <*> mapATTImp' argTy <*> mapATTImp' lamTy
1051 |   mapATTImp' o@(ILet fc lhsFC rig n nTy nVal scope)
1052 |     = f o $ ILet fc lhsFC rig n <$> mapATTImp' nTy <*> mapATTImp' nVal <*> mapATTImp' scope
1053 |   mapATTImp' o@(ICase fc opts t ty cls)
1054 |     = f o $ ICase fc opts <$> mapATTImp' t <*> mapATTImp' ty <*> assert_total (traverse mapMClause cls)
1055 |   mapATTImp' o@(ILocal fc xs t)
1056 |     = f o $ ILocal fc <$> assert_total (traverse mapMDecl xs) <*> mapATTImp' t
1057 |   mapATTImp' o@(IUpdate fc upds t)
1058 |     = f o $ IUpdate fc <$> assert_total (traverse mapMIFieldUpdate upds) <*> mapATTImp' t
1059 |   mapATTImp' o@(IApp fc t u)
1060 |     = f o $ IApp fc <$> mapATTImp' t <*> mapATTImp' u
1061 |   mapATTImp' o@(IAutoApp fc t u)
1062 |     = f o $ IAutoApp fc <$> mapATTImp' t <*> mapATTImp' u
1063 |   mapATTImp' o@(INamedApp fc t n u)
1064 |     = f o $ INamedApp fc <$> mapATTImp' t <*> pure n <*> mapATTImp' u
1065 |   mapATTImp' o@(IWithApp fc t u) = f o $ IWithApp fc <$> mapATTImp' t <*> mapATTImp' u
1066 |   mapATTImp' o@(ISearch fc depth) = f o $ pure $ ISearch fc depth
1067 |   mapATTImp' o@(IAlternative fc alt ts)
1068 |     = f o $ IAlternative fc <$> mapMAltType alt <*> assert_total (traverse mapATTImp' ts)
1069 |   mapATTImp' o@(IRewrite fc t u) = f o $ IRewrite fc <$> mapATTImp' t <*> mapATTImp' u
1070 |   mapATTImp' o@(IBindHere fc bm t) = f o $ IBindHere fc bm <$> mapATTImp' t
1071 |   mapATTImp' o@(IBindVar fc str) = f o $ pure $ IBindVar fc str
1072 |   mapATTImp' o@(IAs fc nameFC side n t) = f o $ IAs fc nameFC side n <$> mapATTImp' t
1073 |   mapATTImp' o@(IMustUnify fc x t) = f o $ IMustUnify fc x <$> mapATTImp' t
1074 |   mapATTImp' o@(IDelayed fc lz t) = f o $ IDelayed fc lz <$> mapATTImp' t
1075 |   mapATTImp' o@(IDelay fc t) = f o $ IDelay fc <$> mapATTImp' t
1076 |   mapATTImp' o@(IForce fc t) = f o $ IForce fc <$> mapATTImp' t
1077 |   mapATTImp' o@(IQuote fc t) = f o $ IQuote fc <$> mapATTImp' t
1078 |   mapATTImp' o@(IQuoteName fc n) = f o $ pure $ IQuoteName fc n
1079 |   mapATTImp' o@(IQuoteDecl fc xs) = f o $ IQuoteDecl fc <$> assert_total (traverse mapMDecl xs)
1080 |   mapATTImp' o@(IUnquote fc t) = f o $ IUnquote fc <$> mapATTImp' t
1081 |   mapATTImp' o@(IPrimVal fc c) = f o $ pure $ IPrimVal fc c
1082 |   mapATTImp' o@(IType fc) = f o $ pure $ IType fc
1083 |   mapATTImp' o@(IHole fc str) = f o $ pure $ IHole fc str
1084 |   mapATTImp' o@(Implicit fc bindIfUnsolved) = f o $ pure $ Implicit fc bindIfUnsolved
1085 |   mapATTImp' o@(IWithUnambigNames fc xs t) = f o $ IWithUnambigNames fc xs <$> mapATTImp' t
1086 |
1087 | public export %inline
1088 | mapATTImp : Monad m => (m TTImp -> m TTImp) -> TTImp -> m TTImp
1089 | mapATTImp = mapATTImp' . const
1090 |
1091 | public export %inline
1092 | mapMTTImp' : Monad m => ((original, mapped : TTImp) -> m TTImp) -> TTImp -> m TTImp
1093 | mapMTTImp' = mapATTImp' . (=<<) .: apply
1094 |
1095 | public export %inline
1096 | mapMTTImp : Monad m => (TTImp -> m TTImp) -> TTImp -> m TTImp
1097 | mapMTTImp = mapATTImp . (=<<)
1098 |