Language.Reflection.TTImp


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