
   0 | module TTImp.TTImp
   1 | 
   2 | import Core.Context.Log
   3 | import Core.Env
   4 | import Core.Normalise
   5 | import Core.Value
   6 | 
   7 | import public Data.List1
   8 | import Data.SortedSet
   9 | 
  10 | import Libraries.Data.List.SizeOf
  11 | import Libraries.Data.WithDefault
  12 | 
  13 | %default covering
  14 | 
  15 | -- Information about names in nested blocks
  16 | public export
  17 | record NestedNames (vars : Scope) where
  18 |   constructor MkNested
  19 |   -- A map from names to the decorated version of the name, and the new name
  20 |   -- applied to its enclosing environment
  21 |   -- Takes the location and name type, because we don't know them until we
  22 |   -- elaborate the name at the point of use
  23 |   names : List (Name, (Maybe Name,  -- new name if there is one
  24 |                        List (Var vars), -- names used from the environment
  25 |                        FC -> NameType -> Term vars))
  26 | 
  27 | export
  28 | Weaken NestedNames where
  29 |   weakenNs {ns = wkns} s (MkNested ns) = MkNested (map wknName ns)
  30 |     where
  31 |       wknName : (Name, (Maybe Name, List (Var vars), FC -> NameType -> Term vars)) ->
  32 |                 (Name, (Maybe Name, List (Var (wkns ++ vars)), FC -> NameType -> Term (wkns ++ vars)))
  33 |       wknName (n, (mn, vars, rep))
  34 |           = (n, (mn, map (weakenNs s) vars, \fc, nt => weakenNs s (rep fc nt)))
  35 | 
  36 | -- replace nested name with full name
  37 | export
  38 | mapNestedName : NestedNames vars -> Name -> Name
  39 | mapNestedName nest n = case lookup n (names nest) of
  40 |                                (Just (Just n', _)) => n'
  41 |                                _ => n
  42 | 
  43 | -- Unchecked terms, with implicit arguments
  44 | -- This is the raw, elaboratable form.
  45 | -- Higher level expressions (e.g. case, pattern matching let, where blocks,
  46 | -- do notation, etc, should elaborate via this, perhaps in some local
  47 | -- context).
  48 | public export
  49 | data BindMode = PI RigCount | PATTERN | COVERAGE | NONE
  50 | 
  51 | %name BindMode bm
  52 | 
  53 | mutual
  54 | 
  55 |   public export
  56 |   RawImp : Type
  57 |   RawImp = RawImp' Name
  58 | 
  59 |   public export
  60 |   IRawImp : Type
  61 |   IRawImp = RawImp' KindedName
  62 | 
  63 |   public export
  64 |   data RawImp' : Type -> Type where
  65 |        IVar : FC -> nm -> RawImp' nm
  66 |        IPi : FC -> RigCount -> PiInfo (RawImp' nm) -> Maybe Name ->
  67 |              (argTy : RawImp' nm) -> (retTy : RawImp' nm) -> RawImp' nm
  68 |        ILam : FC -> RigCount -> PiInfo (RawImp' nm) -> Maybe Name ->
  69 |               (argTy : RawImp' nm) -> (lamTy : RawImp' nm) -> RawImp' nm
  70 |        ILet : FC -> (lhsFC : FC) -> RigCount -> Name ->
  71 |               (nTy : RawImp' nm) -> (nVal : RawImp' nm) ->
  72 |               (scope : RawImp' nm) -> RawImp' nm
  73 |        ICase : FC -> List (FnOpt' nm) -> RawImp' nm -> (ty : RawImp' nm) ->
  74 |                List (ImpClause' nm) -> RawImp' nm
  75 |        ILocal : FC -> List (ImpDecl' nm) -> RawImp' nm -> RawImp' nm
  76 |        -- Local definitions made elsewhere, but that we're pushing
  77 |        -- into a case branch as nested names.
  78 |        -- An appearance of 'uname' maps to an application of
  79 |        -- 'internalName' to 'args'.
  80 |        ICaseLocal : FC -> (uname : Name) ->
  81 |                     (internalName : Name) ->
  82 |                     (args : List Name) -> RawImp' nm -> RawImp' nm
  83 | 
  84 |        IUpdate : FC -> List (IFieldUpdate' nm) -> RawImp' nm -> RawImp' nm
  85 | 
  86 |        IApp : FC -> RawImp' nm -> RawImp' nm -> RawImp' nm
  87 |        IAutoApp : FC -> RawImp' nm -> RawImp' nm -> RawImp' nm
  88 |        INamedApp : FC -> RawImp' nm -> Name -> RawImp' nm -> RawImp' nm
  89 |        IWithApp : FC -> RawImp' nm -> RawImp' nm -> RawImp' nm
  90 | 
  91 |        ISearch : FC -> (depth : Nat) -> RawImp' nm
  92 |        IAlternative : FC -> AltType' nm -> List (RawImp' nm) -> RawImp' nm
  93 |        IRewrite : FC -> RawImp' nm -> RawImp' nm -> RawImp' nm
  94 |        ICoerced : FC -> RawImp' nm -> RawImp' nm
  95 | 
  96 |        -- Any implicit bindings in the scope should be bound here, using
  97 |        -- the given binder
  98 |        IBindHere : FC -> BindMode -> RawImp' nm -> RawImp' nm
  99 |        -- A name which should be implicitly bound
 100 |        IBindVar : FC -> Name -> RawImp' nm
 101 |        -- An 'as' pattern, valid on the LHS of a clause only
 102 |        IAs : FC -> (nameFC : FC) -> UseSide -> Name -> RawImp' nm -> RawImp' nm
 103 |        -- A 'dot' pattern, i.e. one which must also have the given value
 104 |        -- by unification
 105 |        IMustUnify : FC -> DotReason -> RawImp' nm -> RawImp' nm
 106 | 
 107 |        -- Laziness annotations
 108 |        IDelayed : FC -> LazyReason -> RawImp' nm -> RawImp' nm -- the type
 109 |        IDelay : FC -> RawImp' nm -> RawImp' nm -- delay constructor
 110 |        IForce : FC -> RawImp' nm -> RawImp' nm
 111 | 
 112 |        -- Quasiquoting
 113 |        IQuote : FC -> RawImp' nm -> RawImp' nm
 114 |        IQuoteName : FC -> Name -> RawImp' nm
 115 |        IQuoteDecl : FC -> List (ImpDecl' nm) -> RawImp' nm
 116 |        IUnquote : FC -> RawImp' nm -> RawImp' nm
 117 |        IRunElab : FC -> (requireExtension : Bool) -> RawImp' nm -> RawImp' nm
 118 | 
 119 |        IPrimVal : FC -> (c : Constant) -> RawImp' nm
 120 |        IType : FC -> RawImp' nm
 121 |        IHole : FC -> String -> RawImp' nm
 122 | 
 123 |        IUnifyLog : FC -> LogLevel -> RawImp' nm -> RawImp' nm
 124 |        -- An implicit value, solved by unification, but which will also be
 125 |        -- bound (either as a pattern variable or a type variable) if unsolved
 126 |        -- at the end of elaborator
 127 |        Implicit : FC -> (bindIfUnsolved : Bool) -> RawImp' nm
 128 | 
 129 |        -- with-disambiguation
 130 |        IWithUnambigNames : FC -> List (FC, Name) -> RawImp' nm -> RawImp' nm
 131 | 
 132 |   %name RawImp' t, u
 133 | 
 134 |   public export
 135 |   IFieldUpdate : Type
 136 |   IFieldUpdate = IFieldUpdate' Name
 137 | 
 138 |   public export
 139 |   data IFieldUpdate' : Type -> Type where
 140 |        ISetField : (path : List String) -> RawImp' nm -> IFieldUpdate' nm
 141 |        ISetFieldApp : (path : List String) -> RawImp' nm -> IFieldUpdate' nm
 142 |   %name IFieldUpdate' upd
 143 | 
 144 |   public export
 145 |   AltType : Type
 146 |   AltType = AltType' Name
 147 | 
 148 |   public export
 149 |   data AltType' : Type -> Type where
 150 |        FirstSuccess : AltType' nm
 151 |        Unique : AltType' nm
 152 |        UniqueDefault : RawImp' nm -> AltType' nm
 153 |   %name AltType' alt
 154 | 
 155 |   export
 156 |   covering
 157 |   Show nm => Show (RawImp' nm) where
 158 |       show (IVar fc n) = show n
 159 |       show (IPi fc c p n arg ret)
 160 |          = "(%pi " ++ show c ++ " " ++ show p ++ " " ++
 161 |            showPrec App n ++ " " ++ show arg ++ " " ++ show ret ++ ")"
 162 |       show (ILam fc c p n arg sc)
 163 |          = "(%lam " ++ show c ++ " " ++ show p ++ " " ++
 164 |            showPrec App n ++ " " ++ show arg ++ " " ++ show sc ++ ")"
 165 |       show (ILet fc lhsFC c n ty val sc)
 166 |          = "(%let " ++ show c ++ " " ++ " " ++ show n ++ " " ++ show ty ++
 167 |            " " ++ show val ++ " " ++ show sc ++ ")"
 168 |       show (ICase _ _ scr scrty alts)
 169 |          = "(%case (" ++ show scr ++ " : " ++ show scrty ++ ") " ++ show alts ++ ")"
 170 |       show (ILocal _ def scope)
 171 |          = "(%local (" ++ show def ++ ") " ++ show scope ++ ")"
 172 |       show (ICaseLocal _ uname iname args sc)
 173 |          = "(%caselocal (" ++ show uname ++ " " ++ show iname
 174 |                ++ " " ++ show args ++ ") " ++ show sc ++ ")"
 175 |       show (IUpdate _ flds rec)
 176 |          = "(%record " ++ showSep ", " (map show flds) ++ " " ++ show rec ++ ")"
 177 |       show (IApp fc f a)
 178 |          = "(" ++ show f ++ " " ++ show a ++ ")"
 179 |       show (INamedApp fc f n a)
 180 |          = "(" ++ show f ++ " [" ++ show n ++ " = " ++ show a ++ "])"
 181 |       show (IAutoApp fc f a)
 182 |          = "(" ++ show f ++ " [" ++ show a ++ "])"
 183 |       show (IWithApp fc f a)
 184 |          = "(" ++ show f ++ " | " ++ show a ++ ")"
 185 |       show (ISearch fc d)
 186 |          = "%search"
 187 |       show (IAlternative fc ty alts)
 188 |          = "(|" ++ showSep "," (map show alts) ++ "|)"
 189 |       show (IRewrite _ rule tm)
 190 |          = "(%rewrite (" ++ show rule ++ ") (" ++ show tm ++ "))"
 191 |       show (ICoerced _ tm) = "(%coerced " ++ show tm ++ ")"
 192 | 
 193 |       show (IBindHere fc b sc)
 194 |          = "(%bindhere " ++ show sc ++ ")"
 195 |       show (IBindVar fc n) = "$" ++ show n
 196 |       show (IAs fc _ _ n tm) = show n ++ "@(" ++ show tm ++ ")"
 197 |       show (IMustUnify fc r tm) = ".(" ++ show tm ++ ")"
 198 |       show (IDelayed fc r tm) = "(%delayed " ++ show tm ++ ")"
 199 |       show (IDelay fc tm) = "(%delay " ++ show tm ++ ")"
 200 |       show (IForce fc tm) = "(%force " ++ show tm ++ ")"
 201 |       show (IQuote fc tm) = "(%quote " ++ show tm ++ ")"
 202 |       show (IQuoteName fc tm) = "(%quotename " ++ show tm ++ ")"
 203 |       show (IQuoteDecl fc tm) = "(%quotedecl " ++ show tm ++ ")"
 204 |       show (IUnquote fc tm) = "(%unquote " ++ show tm ++ ")"
 205 |       show (IRunElab fc _ tm) = "(%runelab " ++ show tm ++ ")"
 206 |       show (IPrimVal fc c) = show c
 207 |       show (IHole _ x) = "?" ++ x
 208 |       show (IUnifyLog _ lvl x) = "(%logging " ++ show lvl ++ " " ++ show x ++ ")"
 209 |       show (IType fc) = "%type"
 210 |       show (Implicit fc True) = "_"
 211 |       show (Implicit fc False) = "?"
 212 |       show (IWithUnambigNames fc ns rhs) = "(%with " ++ show ns ++ " " ++ show rhs ++ ")"
 213 | 
 214 |   export
 215 |   covering
 216 |   Show nm => Show (IFieldUpdate' nm) where
 217 |     show (ISetField p val) = showSep "->" p ++ " = " ++ show val
 218 |     show (ISetFieldApp p val) = showSep "->" p ++ " $= " ++ show val
 219 | 
 220 |   public export
 221 |   FnOpt : Type
 222 |   FnOpt = FnOpt' Name
 223 | 
 224 |   public export
 225 |   data FnOpt' : Type -> Type where
 226 |        Unsafe : FnOpt' nm
 227 |        Inline : FnOpt' nm
 228 |        NoInline : FnOpt' nm
 229 |        ||| Mark a function as deprecated.
 230 |        Deprecate : FnOpt' nm
 231 |        TCInline : FnOpt' nm
 232 |        -- Flag means the hint is a direct hint, not a function which might
 233 |        -- find the result (e.g. chasing parent interface dictionaries)
 234 |        Hint : Bool -> FnOpt' nm
 235 |        -- Flag means to use as a default if all else fails
 236 |        GlobalHint : Bool -> FnOpt' nm
 237 |        ExternFn : FnOpt' nm
 238 |        -- Defined externally, list calling conventions
 239 |        ForeignFn : List (RawImp' nm) -> FnOpt' nm
 240 |        -- Mark for export to a foreign language, list calling conventions
 241 |        ForeignExport : List (RawImp' nm) -> FnOpt' nm
 242 |        -- assume safe to cancel arguments in unification
 243 |        Invertible : FnOpt' nm
 244 |        Totality : TotalReq -> FnOpt' nm
 245 |        Macro : FnOpt' nm
 246 |        SpecArgs : List Name -> FnOpt' nm
 247 |   %name FnOpt' fopt
 248 | 
 249 |   public export
 250 |   isTotalityReq : FnOpt' nm -> Bool
 251 |   isTotalityReq (Totality _) = True
 252 |   isTotalityReq _ = False
 253 | 
 254 |   export
 255 |   extractTotality : FnOpt' nm -> Maybe TotalReq
 256 |   extractTotality (Totality t) = Just t
 257 |   extractTotality _ = Nothing
 258 | 
 259 |   export
 260 |   findTotality : List (FnOpt' nm) -> Maybe TotalReq
 261 |   findTotality = foldr (\elem, acc => extractTotality elem <|> acc) empty
 262 | 
 263 |   export
 264 |   covering
 265 |   Show nm => Show (FnOpt' nm) where
 266 |     show Unsafe = "%unsafe"
 267 |     show Inline = "%inline"
 268 |     show NoInline = "%noinline"
 269 |     show Deprecate = "%deprecate"
 270 |     show TCInline = "%tcinline"
 271 |     show (Hint t) = "%hint " ++ show t
 272 |     show (GlobalHint t) = "%globalhint " ++ show t
 273 |     show ExternFn = "%extern"
 274 |     show (ForeignFn cs) = "%foreign " ++ showSep " " (map show cs)
 275 |     show (ForeignExport cs) = "%export " ++ showSep " " (map show cs)
 276 |     show Invertible = "%invertible"
 277 |     show (Totality Total) = "total"
 278 |     show (Totality CoveringOnly) = "covering"
 279 |     show (Totality PartialOK) = "partial"
 280 |     show Macro = "%macro"
 281 |     show (SpecArgs ns) = "%spec " ++ showSep " " (map show ns)
 282 | 
 283 |   export
 284 |   Eq FnOpt where
 285 |     Inline == Inline = True
 286 |     NoInline == NoInline = True
 287 |     Deprecate == Deprecate = True
 288 |     TCInline == TCInline = True
 289 |     (Hint x) == (Hint y) = x == y
 290 |     (GlobalHint x) == (GlobalHint y) = x == y
 291 |     ExternFn == ExternFn = True
 292 |     (ForeignFn xs) == (ForeignFn ys) = True -- xs == ys
 293 |     (ForeignExport xs) == (ForeignExport ys) = True -- xs == ys
 294 |     Invertible == Invertible = True
 295 |     (Totality tot_lhs) == (Totality tot_rhs) = tot_lhs == tot_rhs
 296 |     Macro == Macro = True
 297 |     (SpecArgs ns) == (SpecArgs ns') = ns == ns'
 298 |     _ == _ = False
 299 | 
 300 |   public export
 301 |   ImpTy : Type
 302 |   ImpTy = ImpTy' Name
 303 | 
 304 |   public export
 305 |   ImpTy' : Type -> Type
 306 |   ImpTy' = AddMetadata FC' . AddMetadata TyName' . RawImp'
 307 | 
 308 |   export
 309 |   covering
 310 |   Show nm => Show (ImpTy' nm) where
 311 |     show ty = "(%claim " ++ show ty.tyName.val ++ " " ++ show ty.val ++ ")"
 312 | 
 313 |   public export
 314 |   ImpData : Type
 315 |   ImpData = ImpData' Name
 316 | 
 317 |   public export
 318 |   data ImpData' : Type -> Type where
 319 |        MkImpData : FC -> (n : Name) ->
 320 |                    -- if we have already declared the type using `MkImpLater`,
 321 |                    -- we are allowed to leave the telescope out here.
 322 |                    (tycon : Maybe (RawImp' nm)) ->
 323 |                    (opts : List DataOpt) ->
 324 |                    (datacons : List (ImpTy' nm)) -> ImpData' nm
 325 |        MkImpLater : FC -> (n : Name) -> (tycon : RawImp' nm) -> ImpData' nm
 326 | 
 327 |   %name ImpData' dat
 328 | 
 329 |   export
 330 |   covering
 331 |   Show nm => Show (ImpData' nm) where
 332 |     show (MkImpData fc n (Just tycon) _ cons)
 333 |         = "(%data " ++ show n ++ " " ++ show tycon ++ " " ++ show cons ++ ")"
 334 |     show (MkImpData fc n Nothing _ cons)
 335 |         = "(%data " ++ show n ++ " " ++ show cons ++ ")"
 336 |     show (MkImpLater fc n tycon)
 337 |         = "(%datadecl " ++ show n ++ " " ++ show tycon ++ ")"
 338 | 
 339 |   public export
 340 |   IField : Type
 341 |   IField = IField' Name
 342 | 
 343 |   public export
 344 |   IField' : Type -> Type
 345 |   IField' nm = AddFC $ ImpParameter' (RawImp' nm)
 346 | 
 347 |   public export
 348 |   ImpParameter : Type
 349 |   ImpParameter = ImpParameter' (RawImp' Name)
 350 | 
 351 |   public export
 352 |   ImpParameter' : Type -> Type
 353 |   ImpParameter' nm = WithRig $ WithName $ PiBindData nm
 354 | 
 355 |   -- old datatype for ImpParameter, used for elabreflection compatibility
 356 |   public export
 357 |   OldParameters' : Type -> Type
 358 |   OldParameters' nm = (Name, RigCount, PiInfo (RawImp' nm), RawImp' nm)
 359 | 
 360 |   public export
 361 |   toOldParams : ImpParameter' (RawImp' nm) -> OldParameters' nm
 362 |   toOldParams bind = (bind.name.val, bind.rig, bind.val.info, bind.val.boundType)
 363 | 
 364 |   public export
 365 |   fromOldParams : OldParameters' nm -> ImpParameter' (RawImp' nm)
 366 |   fromOldParams (nm, rig, info,type) = Mk [rig, NoFC nm] (MkPiBindData info type)
 367 | 
 368 |   export
 369 |   Show nm => Show (ImpParameter' nm) where
 370 |     show x = "\{show x.rig}\{show x.name.val} \{show x.val.boundType}"
 371 | 
 372 |   public export 0
 373 |   ImpRecord : Type
 374 |   ImpRecord = AddFC $ ImpRecordData Name
 375 | 
 376 |   public export 0
 377 |   DataHeader : Type -> Type -- the name is the type constructor's name
 378 |   DataHeader nm = WithName $ List (ImpParameter' (RawImp' nm))
 379 | 
 380 |   public export 0
 381 |   RecordBody : Type -> Type -- The name is the data constructor's name
 382 |   RecordBody nm = WithName $ WithOpts $ List (IField' nm)
 383 | 
 384 |   ||| A record is defined by its header containing the name and parameters, and its body
 385 |   ||| containing the constructor name, options, and a list of fields
 386 |   public export
 387 |   record ImpRecordData (nm : Type) where
 388 |     constructor MkImpRecord
 389 |     header : DataHeader nm
 390 |     body : RecordBody nm
 391 | 
 392 |   export
 393 |   covering
 394 |   Show nm => Show (IField' nm) where
 395 |     show f@(MkWithData _ (MkPiBindData Explicit ty)) = show f.name.val ++ " : " ++ show ty
 396 |     show f@(MkWithData _ ty) = "{" ++ show f.name.val ++ " : " ++ show ty.boundType ++ "}"
 397 | 
 398 |   export
 399 |   covering
 400 |   Show nm => Show (ImpRecordData nm) where
 401 |     show (MkImpRecord header body)
 402 |         = "record " ++ show header.name.val ++ " " ++ show header.val ++
 403 |           " " ++ show body.name.val ++ "\n\t" ++
 404 |           showSep "\n\t" (map show body.val) ++ "\n"
 405 | 
 406 |   public export
 407 |   data WithFlag
 408 |          = Syntactic -- abstract syntactically, rather than by value
 409 | 
 410 |   export
 411 |   Eq WithFlag where
 412 |       Syntactic == Syntactic = True
 413 | 
 414 |   public export
 415 |   ImpClause : Type
 416 |   ImpClause = ImpClause' Name
 417 | 
 418 |   public export
 419 |   IImpClause : Type
 420 |   IImpClause = ImpClause' KindedName
 421 | 
 422 |   public export
 423 |   data ImpClause' : Type -> Type where
 424 |        PatClause : FC -> (lhs : RawImp' nm) -> (rhs : RawImp' nm) -> ImpClause' nm
 425 |        WithClause : FC -> (lhs : RawImp' nm) ->
 426 |                     (rig : RigCount) -> (wval : RawImp' nm) -> -- with'd expression (& quantity)
 427 |                     (prf : Maybe (RigCount, Name)) -> -- optional name for the proof
 428 |                     (flags : List WithFlag) ->
 429 |                     List (ImpClause' nm) -> ImpClause' nm
 430 |        ImpossibleClause : FC -> (lhs : RawImp' nm) -> ImpClause' nm
 431 | 
 432 |   %name ImpClause' cl
 433 | 
 434 |   export
 435 |   covering
 436 |   Show nm => Show (ImpClause' nm) where
 437 |     show (PatClause fc lhs rhs)
 438 |        = show lhs ++ " = " ++ show rhs
 439 |     show (WithClause fc lhs rig wval prf flags block)
 440 |        = show lhs
 441 |        ++ " with " ++ showCount rig ++ "(" ++ show wval ++ ")"
 442 |           -- TODO: remove `the` after fix idris-lang/Idris2#3418
 443 |        ++ maybe "" (the (_ -> _) $ \(rg, nm) => " proof " ++ showCount rg ++ show nm) prf
 444 |        ++ "\n\t" ++ show block
 445 |     show (ImpossibleClause fc lhs)
 446 |        = show lhs ++ " impossible"
 447 | 
 448 |   public export
 449 |   ImpDecl : Type
 450 |   ImpDecl = ImpDecl' Name
 451 | 
 452 |   public export
 453 |   record IClaimData (nm : Type) where
 454 |     constructor MkIClaimData
 455 |     rig : RigCount
 456 |     vis : Visibility
 457 |     opts : List (FnOpt' nm)
 458 |     type : ImpTy' nm
 459 | 
 460 |   public export
 461 |   data ImpDecl' : Type -> Type where
 462 |        IClaim : WithFC (IClaimData nm) -> ImpDecl' nm
 463 |        IData : FC -> WithDefault Visibility Private ->
 464 |                Maybe TotalReq -> ImpData' nm -> ImpDecl' nm
 465 |        IDef : FC -> Name -> List (ImpClause' nm) -> ImpDecl' nm
 466 |        IParameters : FC ->
 467 |                      List1 (ImpParameter' (RawImp' nm)) ->
 468 |                      List (ImpDecl' nm) -> ImpDecl' nm
 469 |        IRecord : FC ->
 470 |                  Maybe String -> -- nested namespace
 471 |                  WithDefault Visibility Private ->
 472 |                  Maybe TotalReq ->
 473 |                  AddFC (ImpRecordData nm) -> ImpDecl' nm
 474 |        IFail : FC -> Maybe String -> List (ImpDecl' nm) -> ImpDecl' nm
 475 |        INamespace : FC -> Namespace -> List (ImpDecl' nm) -> ImpDecl' nm
 476 |        ITransform : FC -> Name -> RawImp' nm -> RawImp' nm -> ImpDecl' nm
 477 |        IRunElabDecl : FC -> RawImp' nm -> ImpDecl' nm
 478 |        IPragma : FC -> List Name -> -- pragmas might define names that wouldn't
 479 |                                     -- otherwise be spotted in 'definedInBlock' so they
 480 |                                     -- can be flagged here.
 481 |                  ({vars : _} ->
 482 |                   NestedNames vars -> Env Term vars -> Core ()) ->
 483 |                  ImpDecl' nm
 484 |        ILog : Maybe (List String, Nat) -> ImpDecl' nm
 485 |        IBuiltin : FC -> BuiltinType -> Name -> ImpDecl' nm
 486 | 
 487 |   %name ImpDecl' decl
 488 | 
 489 |   export
 490 |   covering
 491 |   Show nm => Show (ImpDecl' nm) where
 492 |     show (IClaim (MkWithData _ $ MkIClaimData c _ opts ty))
 493 |         = show opts ++ " " ++ show c ++ " " ++ show ty
 494 |     show (IData _ _ _ d) = show d
 495 |     show (IDef _ n cs) = "(%def " ++ show n ++ " " ++ show cs ++ ")"
 496 |     show (IParameters _ ps ds)
 497 |         = "parameters " ++ show ps ++ "\n\t" ++
 498 |           showSep "\n\t" (assert_total $ map show ds)
 499 |     show (IRecord _ _ _ _ d) = show d.val
 500 |     show (IFail _ msg decls)
 501 |         = "fail" ++ maybe "" ((" " ++) . show) msg ++ "\n" ++
 502 |           showSep "\n" (assert_total $ map (("  " ++) . show) decls)
 503 |     show (INamespace _ ns decls)
 504 |         = "namespace " ++ show ns ++
 505 |           showSep "\n" (assert_total $ map show decls)
 506 |     show (ITransform _ n lhs rhs)
 507 |         = "%transform " ++ show n ++ " " ++ show lhs ++ " ==> " ++ show rhs
 508 |     show (IRunElabDecl _ tm)
 509 |         = "%runElab " ++ show tm
 510 |     show (IPragma {}) = "[externally defined pragma]"
 511 |     show (ILog Nothing) = "%logging off"
 512 |     show (ILog (Just (topic, lvl))) = "%logging " ++ case topic of
 513 |       [] => show lvl
 514 |       _  => concat (intersperse "." topic) ++ " " ++ show lvl
 515 |     show (IBuiltin _ type name) = "%builtin " ++ show type ++ " " ++ show name
 516 | 
 517 | 
 518 | export
 519 | mkWithClause : FC -> RawImp' nm -> List1 (RigCount, RawImp' nm, Maybe (RigCount, Name)) ->
 520 |                List WithFlag -> List (ImpClause' nm) -> ImpClause' nm
 521 | mkWithClause fc lhs ((rig, wval, prf) ::: []) flags cls
 522 |   = WithClause fc lhs rig wval prf flags cls
 523 | mkWithClause fc lhs ((rig, wval, prf) ::: wp :: wps) flags cls
 524 |   = let vfc = virtualiseFC fc
 525 |         arg = UN $ Basic "arg"
 526 |      in WithClause fc lhs rig wval prf flags
 527 |           [mkWithClause fc (IApp vfc lhs $ IBindVar vfc arg) (wp ::: wps) flags cls]
 528 | 
 529 | -- Extract the RawImp term from a FieldUpdate.
 530 | export
 531 | getFieldUpdateTerm : IFieldUpdate' nm -> RawImp' nm
 532 | getFieldUpdateTerm (ISetField    _ term) = term
 533 | getFieldUpdateTerm (ISetFieldApp _ term) = term
 534 | 
 535 | 
 536 | export
 537 | getFieldUpdatePath : IFieldUpdate' nm -> List String
 538 | getFieldUpdatePath (ISetField    path _) = path
 539 | getFieldUpdatePath (ISetFieldApp path _) = path
 540 | 
 541 | 
 542 | export
 543 | mapFieldUpdateTerm : (RawImp' nm -> RawImp' nm) -> IFieldUpdate' nm -> IFieldUpdate' nm
 544 | mapFieldUpdateTerm f (ISetField    x term) = ISetField    x (f term)
 545 | mapFieldUpdateTerm f (ISetFieldApp x term) = ISetFieldApp x (f term)
 546 | 
 547 | 
 548 | export
 549 | isIPrimVal : RawImp' nm -> Maybe Constant
 550 | isIPrimVal (IPrimVal _ c) = Just c
 551 | isIPrimVal _ = Nothing
 552 | 
 553 | -- REPL commands for TTImp interaction
 554 | public export
 555 | data ImpREPL : Type where
 556 |      Eval : RawImp -> ImpREPL
 557 |      Check : RawImp -> ImpREPL
 558 |      ProofSearch : Name -> ImpREPL
 559 |      ExprSearch : Name -> ImpREPL
 560 |      GenerateDef : Int -> Name -> ImpREPL
 561 |      Missing : Name -> ImpREPL
 562 |      CheckTotal : Name -> ImpREPL
 563 |      DebugInfo : Name -> ImpREPL
 564 |      Quit : ImpREPL
 565 | 
 566 | export
 567 | mapAltType : (RawImp' nm -> RawImp' nm) -> AltType' nm -> AltType' nm
 568 | mapAltType f (UniqueDefault x) = UniqueDefault (f x)
 569 | mapAltType _ u = u
 570 | 
 571 | export
 572 | lhsInCurrentNS : {auto c : Ref Ctxt Defs} ->
 573 |                  NestedNames vars -> RawImp -> Core RawImp
 574 | lhsInCurrentNS nest (IApp loc f a)
 575 |     = do f' <- lhsInCurrentNS nest f
 576 |          pure (IApp loc f' a)
 577 | lhsInCurrentNS nest (IAutoApp loc f a)
 578 |     = do f' <- lhsInCurrentNS nest f
 579 |          pure (IAutoApp loc f' a)
 580 | lhsInCurrentNS nest (INamedApp loc f n a)
 581 |     = do f' <- lhsInCurrentNS nest f
 582 |          pure (INamedApp loc f' n a)
 583 | lhsInCurrentNS nest (IWithApp loc f a)
 584 |     = do f' <- lhsInCurrentNS nest f
 585 |          pure (IWithApp loc f' a)
 586 | lhsInCurrentNS nest tm@(IVar loc (NS {})) = pure tm -- leave explicit NS alone
 587 | lhsInCurrentNS nest (IVar loc n)
 588 |     = case lookup n (names nest) of
 589 |            Nothing =>
 590 |               do n' <- inCurrentNS n
 591 |                  pure (IVar loc n')
 592 |            -- If it's one of the names in the current nested block, we'll
 593 |            -- be rewriting it during elaboration to be in the scope of the
 594 |            -- parent name.
 595 |            Just _ => pure (IVar loc n)
 596 | lhsInCurrentNS nest tm = pure tm
 597 | 
 598 | export
 599 | findIBinds : RawImp' nm -> List String
 600 | findIBinds (IPi fc rig p mn aty retty)
 601 |     = findIBinds aty ++ findIBinds retty
 602 | findIBinds (ILam fc rig p n aty sc)
 603 |     = findIBinds aty ++ findIBinds sc
 604 | findIBinds (IApp fc fn av)
 605 |     = findIBinds fn ++ findIBinds av
 606 | findIBinds (IAutoApp fc fn av)
 607 |     = findIBinds fn ++ findIBinds av
 608 | findIBinds (INamedApp _ fn _ av)
 609 |     = findIBinds fn ++ findIBinds av
 610 | findIBinds (IWithApp fc fn av)
 611 |     = findIBinds fn ++ findIBinds av
 612 | findIBinds (IAs fc _ _ (UN (Basic n)) pat)
 613 |     = n :: findIBinds pat
 614 | findIBinds (IAs fc _ _ n pat)
 615 |     = findIBinds pat
 616 | findIBinds (IMustUnify fc r pat)
 617 |     = findIBinds pat
 618 | findIBinds (IAlternative fc u alts)
 619 |     = concatMap findIBinds alts
 620 | findIBinds (IDelayed fc _ ty) = findIBinds ty
 621 | findIBinds (IDelay fc tm) = findIBinds tm
 622 | findIBinds (IForce fc tm) = findIBinds tm
 623 | findIBinds (IQuote fc tm) = findIBinds tm
 624 | findIBinds (IUnquote fc tm) = findIBinds tm
 625 | findIBinds (IRunElab fc _ tm) = findIBinds tm
 626 | findIBinds (IBindHere _ _ tm) = findIBinds tm
 627 | findIBinds (IBindVar _ (UN (Basic n))) = [n]
 628 | findIBinds (IUpdate fc updates tm)
 629 |     = findIBinds tm ++ concatMap (findIBinds . getFieldUpdateTerm) updates
 630 | -- We've skipped lambda, case, let and local - rather than guess where the
 631 | -- name should be bound, leave it to the programmer
 632 | findIBinds tm = []
 633 | 
 634 | export
 635 | findImplicits : RawImp' nm -> List String
 636 | findImplicits (IPi fc rig p (Just (UN (Basic mn))) aty retty)
 637 |     = mn :: findImplicits aty ++ findImplicits retty
 638 | findImplicits (IPi fc rig p mn aty retty)
 639 |     = findImplicits aty ++ findImplicits retty
 640 | findImplicits (ILam fc rig p n aty sc)
 641 |     = findImplicits aty ++ findImplicits sc
 642 | findImplicits (IApp fc fn av)
 643 |     = findImplicits fn ++ findImplicits av
 644 | findImplicits (IAutoApp _ fn av)
 645 |     = findImplicits fn ++ findImplicits av
 646 | findImplicits (INamedApp _ fn _ av)
 647 |     = findImplicits fn ++ findImplicits av
 648 | findImplicits (IWithApp fc fn av)
 649 |     = findImplicits fn ++ findImplicits av
 650 | findImplicits (IAs fc _ _ n pat)
 651 |     = findImplicits pat
 652 | findImplicits (IMustUnify fc r pat)
 653 |     = findImplicits pat
 654 | findImplicits (IAlternative fc u alts)
 655 |     = concatMap findImplicits alts
 656 | findImplicits (IDelayed fc _ ty) = findImplicits ty
 657 | findImplicits (IDelay fc tm) = findImplicits tm
 658 | findImplicits (IForce fc tm) = findImplicits tm
 659 | findImplicits (IQuote fc tm) = findImplicits tm
 660 | findImplicits (IUnquote fc tm) = findImplicits tm
 661 | findImplicits (IRunElab fc _ tm) = findImplicits tm
 662 | findImplicits (IBindVar _ (UN (Basic n))) = [n]
 663 | findImplicits (IUpdate fc updates tm)
 664 |     = findImplicits tm ++ concatMap (findImplicits . getFieldUpdateTerm) updates
 665 | findImplicits tm = []
 666 | 
 667 | -- Update the lhs of a clause so that any implicits named in the type are
 668 | -- bound as @-patterns (unless they're already explicitly bound or appear as
 669 | -- IBindVar anywhere else in the pattern) so that they will be available on the
 670 | -- rhs
 671 | export
 672 | implicitsAs : {auto c : Ref Ctxt Defs} ->
 673 |               Int -> Defs ->
 674 |               (vars : List Name) ->
 675 |               RawImp -> Core RawImp
 676 | implicitsAs n defs ns tm
 677 |   = do let implicits = findIBinds tm
 678 |        log "declare.def.lhs.implicits" 30 $ "Found implicits: " ++ show implicits
 679 |        setAs (map Just (ns ++ map (UN . Basic) implicits)) [] tm
 680 |   where
 681 |     -- Takes the function application expression which is the lhs of a clause
 682 |     -- and decomposes it into the underlying function symbol and the variables
 683 |     -- bound by appearing as arguments, and then passes this onto `findImps`.
 684 |     -- More precisely, implicit and explicit arguments are recorded separately,
 685 |     -- into `is` and `es` respectively.
 686 |     setAs : List (Maybe Name) -> List (Maybe Name) -> RawImp -> Core RawImp
 687 |     setAs is es (IApp loc f a)
 688 |         = do f' <- setAs is (Nothing :: es) f
 689 |              pure $ IApp loc f' a
 690 |     setAs is es (IAutoApp loc f a)
 691 |         = do f' <- setAs (Nothing :: is) es f
 692 |              pure $ IAutoApp loc f' a
 693 |     setAs is es (INamedApp loc f n a)
 694 |         = do f' <- setAs (Just n :: is) (Just n :: es) f
 695 |              pure $ INamedApp loc f' n a
 696 |     setAs is es (IWithApp loc f a)
 697 |         = do f' <- setAs is es f
 698 |              pure $ IWithApp loc f' a
 699 |     setAs is es (IVar loc nm)
 700 |         -- #834 Use the (already) resolved name rather than the local one
 701 |         = case !(lookupTyExact (Resolved n) (gamma defs)) of
 702 |             Nothing =>
 703 |                do log "declare.def.lhs.implicits" 30 $
 704 |                     "Could not find variable " ++ show n
 705 |                   pure $ IVar loc nm
 706 |             Just ty =>
 707 |                do ty' <- nf defs Env.empty ty
 708 |                   implicits <- findImps is es ns ty'
 709 |                   log "declare.def.lhs.implicits" 30 $
 710 |                     "\n  In the type of " ++ show n ++ ": " ++ show ty ++
 711 |                     "\n  Using locals: " ++ show ns ++
 712 |                     "\n  Found implicits: " ++ show implicits
 713 |                   pure $ impAs (virtualiseFC loc) implicits (IVar loc nm)
 714 |       where
 715 |         -- If there's an @{c} in the list of given implicits, that's the next
 716 |         -- autoimplicit, so don't rewrite the LHS and update the list of given
 717 |         -- implicits
 718 |         updateNs : Name -> List (Maybe Name) -> Maybe (List (Maybe Name))
 719 |         updateNs n (Nothing :: ns) = Just ns
 720 |         updateNs n (x :: ns)
 721 |             = if Just n == x
 722 |                  then Just ns -- found it
 723 |                  else do ns' <- updateNs n ns
 724 |                          pure (x :: ns')
 725 |         updateNs n [] = Nothing
 726 | 
 727 |         -- Finds the missing implicits which should be added to the lhs of the
 728 |         -- original pattern clause.
 729 |         --
 730 |         -- The first argument, `ns`, specifies which implicit variables alredy
 731 |         -- appear in the lhs, and therefore need not be added.
 732 |         -- The second argument, `es`, specifies which *explicit* variables appear
 733 |         -- in the lhs: this is used to determine when to stop searching for further
 734 |         -- implicits to add.
 735 |         findImps : List (Maybe Name) -> List (Maybe Name) ->
 736 |                    List Name -> ClosedNF ->
 737 |                    Core (List (Name, PiInfo RawImp))
 738 |         -- #834 When we are in a local definition, we have an explicit telescope
 739 |         -- corresponding to the variables bound in the parent function.
 740 |         -- Parameter blocks also introduce additional telescope of implicit, auto,
 741 |         -- and explicit variables. So we first peel off all of the quantifiers
 742 |         -- corresponding to these variables.
 743 |         findImps ns es (_ :: locals) (NBind fc x (Pi {}) sc)
 744 |           = do body <- sc defs (toClosure defaultOpts Env.empty (Erased fc Placeholder))
 745 |                findImps ns es locals body
 746 |                -- ^ TODO? check that name of the pi matches name of local?
 747 |         -- don't add implicits coming after explicits that aren't given
 748 |         findImps ns es [] (NBind fc x (Pi _ _ Explicit _) sc)
 749 |             = do body <- sc defs (toClosure defaultOpts Env.empty (Erased fc Placeholder))
 750 |                  case es of
 751 |                    -- Explicits were skipped, therefore all explicits are given anyway
 752 |                    Just (UN Underscore) :: _ => findImps ns es [] body
 753 |                    -- Explicits weren't skipped, so we need to check
 754 |                    _ => case updateNs x es of
 755 |                           Nothing => pure [] -- explicit wasn't given
 756 |                           Just es' => findImps ns es' [] body
 757 |         -- if the implicit was given, skip it
 758 |         findImps ns es [] (NBind fc x (Pi _ _ AutoImplicit _) sc)
 759 |             = do body <- sc defs (toClosure defaultOpts Env.empty (Erased fc Placeholder))
 760 |                  case updateNs x ns of
 761 |                    Nothing => -- didn't find explicit call
 762 |                       pure $ (x, AutoImplicit) :: !(findImps ns es [] body)
 763 |                    Just ns' => findImps ns' es [] body
 764 |         findImps ns es [] (NBind fc x (Pi _ _ p _) sc)
 765 |             = do body <- sc defs (toClosure defaultOpts Env.empty (Erased fc Placeholder))
 766 |                  if Just x `elem` ns
 767 |                    then findImps ns es [] body
 768 |                    else pure $ (x, forgetDef p) :: !(findImps ns es [] body)
 769 |         findImps _ _ locals _
 770 |           = do log "declare.def.lhs.implicits" 50 $
 771 |                   "Giving up with the following locals left: " ++ show locals
 772 |                pure []
 773 | 
 774 |         impAs : FC -> List (Name, PiInfo RawImp) -> RawImp -> RawImp
 775 |         impAs loc' [] tm = tm
 776 |         impAs loc' ((nm@(UN (Basic _)), AutoImplicit) :: ns) tm
 777 |             = impAs loc' ns $
 778 |                  INamedApp loc' tm nm (IBindVar loc' nm)
 779 | 
 780 |         impAs loc' ((n, Implicit) :: ns) tm
 781 |             = impAs loc' ns $
 782 |                  INamedApp loc' tm n
 783 |                      (IAs loc' EmptyFC UseLeft n (Implicit loc' True))
 784 | 
 785 |         impAs loc' ((n, DefImplicit t) :: ns) tm
 786 |             = impAs loc' ns $
 787 |                  INamedApp loc' tm n
 788 |                      (IAs loc' EmptyFC UseLeft n (Implicit loc' True))
 789 | 
 790 |         impAs loc' (_ :: ns) tm = impAs loc' ns tm
 791 |     setAs is es tm = pure tm
 792 | 
 793 | ||| `definedInBlock` is used to figure out which definitions should
 794 | ||| receive the additional arguments introduced by a Parameters directive
 795 | export
 796 | definedInBlock : Namespace -> -- namespace to resolve names
 797 |                  List ImpDecl -> List Name
 798 | definedInBlock ns decls =
 799 |     Prelude.toList $ foldl (defName ns) empty decls
 800 |   where
 801 |     getName : ImpTy -> Name
 802 |     getName = (.tyName.val)
 803 | 
 804 |     getFieldName : IField -> Name
 805 |     getFieldName f = f.name.val
 806 | 
 807 |     expandNS : Namespace -> Name -> Name
 808 |     expandNS ns n
 809 |        = if ns == emptyNS then n else case n of
 810 |            UN {} => NS ns n
 811 |            MN {} => NS ns n
 812 |            DN {} => NS ns n
 813 |            _ => n
 814 | 
 815 |     defName : Namespace -> SortedSet Name -> ImpDecl -> SortedSet Name
 816 |     defName ns acc (IClaim c) = insert (expandNS ns (getName c.val.type)) acc
 817 |     defName ns acc (IDef _ nm _) = insert (expandNS ns nm) acc
 818 |     defName ns acc (IData _ _ _ (MkImpData _ n _ _ cons))
 819 |         = foldl (flip insert) acc $ expandNS ns n :: map (expandNS ns . getName) cons
 820 |     defName ns acc (IData _ _ _ (MkImpLater _ n _)) = insert (expandNS ns n) acc
 821 |     defName ns acc (IParameters _ _ pds) = foldl (defName ns) acc pds
 822 |     defName ns acc (IFail _ _ nds) = foldl (defName ns) acc nds
 823 |     defName ns acc (INamespace _ n nds) = foldl (defName (ns <.> n)) acc nds
 824 |     defName ns acc (IRecord _ fldns _ _ rec)
 825 |         = foldl (flip insert) acc $ expandNS ns rec.val.body.name.val :: all
 826 |       where
 827 |         fldns' : Namespace
 828 |         fldns' = maybe ns (\ f => ns <.> mkNamespace f) fldns
 829 | 
 830 |         toRF : Name -> Name
 831 |         toRF (UN (Basic n)) = UN (Field n)
 832 |         toRF n = n
 833 | 
 834 |         fnsUN : List Name
 835 |         fnsUN = map getFieldName rec.val.body.val
 836 | 
 837 |         fnsRF : List Name
 838 |         fnsRF = map toRF fnsUN
 839 | 
 840 |         -- Depending on %prefix_record_projections,
 841 |         -- the record may or may not produce prefix projections (fnsUN).
 842 |         --
 843 |         -- However, since definedInBlock is pure, we can't check that flag
 844 |         -- (and it would also be wrong if %prefix_record_projections appears
 845 |         -- inside the parameter block)
 846 |         -- so let's just declare all of them and some may go unused.
 847 |         all : List Name
 848 |         all = expandNS ns rec.val.header.name.val :: map (expandNS fldns') (fnsRF ++ fnsUN)
 849 | 
 850 |     defName ns acc (IPragma _ pns _) = foldl (flip insert) acc $ map (expandNS ns) pns
 851 |     defName _ acc _ = acc
 852 | 
 853 | export
 854 | isIVar : RawImp' nm -> Maybe (FC, nm)
 855 | isIVar (IVar fc v) = Just (fc, v)
 856 | isIVar _ = Nothing
 857 | 
 858 | export
 859 | isIBindVar : RawImp' nm -> Maybe (FC, Name)
 860 | isIBindVar (IBindVar fc v) = Just (fc, v)
 861 | isIBindVar _ = Nothing
 862 | 
 863 | export
 864 | getFC : RawImp' nm -> FC
 865 | getFC (IVar x _) = x
 866 | getFC (IPi x _ _ _ _ _) = x
 867 | getFC (ILam x _ _ _ _ _) = x
 868 | getFC (ILet x _ _ _ _ _ _) = x
 869 | getFC (ICase x _ _ _ _) = x
 870 | getFC (ILocal x _ _) = x
 871 | getFC (ICaseLocal x _ _ _ _) = x
 872 | getFC (IUpdate x _ _) = x
 873 | getFC (IApp x _ _) = x
 874 | getFC (INamedApp x _ _ _) = x
 875 | getFC (IAutoApp x _ _) = x
 876 | getFC (IWithApp x _ _) = x
 877 | getFC (ISearch x _) = x
 878 | getFC (IAlternative x _ _) = x
 879 | getFC (IRewrite x _ _) = x
 880 | getFC (ICoerced x _) = x
 881 | getFC (IPrimVal x _) = x
 882 | getFC (IHole x _) = x
 883 | getFC (IUnifyLog x _ _) = x
 884 | getFC (IType x) = x
 885 | getFC (IBindVar x _) = x
 886 | getFC (IBindHere x _ _) = x
 887 | getFC (IMustUnify x _ _) = x
 888 | getFC (IDelayed x _ _) = x
 889 | getFC (IDelay x _) = x
 890 | getFC (IForce x _) = x
 891 | getFC (IQuote x _) = x
 892 | getFC (IQuoteName x _) = x
 893 | getFC (IQuoteDecl x _) = x
 894 | getFC (IUnquote x _) = x
 895 | getFC (IRunElab x _ _) = x
 896 | getFC (IAs x _ _ _ _) = x
 897 | getFC (Implicit x _) = x
 898 | getFC (IWithUnambigNames x _ _) = x
 899 | 
 900 | namespace ImpDecl
 901 | 
 902 |   public export
 903 |   getFC : ImpDecl' nm -> FC
 904 |   getFC (IClaim c) = c.fc
 905 |   getFC (IData fc _ _ _) = fc
 906 |   getFC (IDef fc _ _) = fc
 907 |   getFC (IParameters fc _ _) = fc
 908 |   getFC (IRecord fc _ _ _ _) = fc
 909 |   getFC (IFail fc _ _) = fc
 910 |   getFC (INamespace fc _ _) = fc
 911 |   getFC (ITransform fc _ _ _) = fc
 912 |   getFC (IRunElabDecl fc _) = fc
 913 |   getFC (IPragma fc _ _) = fc
 914 |   getFC (ILog _) = EmptyFC
 915 |   getFC (IBuiltin fc _ _) = fc
 916 | 
 917 | public export
 918 | data Arg' nm
 919 |    = Explicit FC (RawImp' nm)
 920 |    | Auto     FC (RawImp' nm)
 921 |    | Named    FC Name (RawImp' nm)
 922 | %name Arg' arg
 923 | 
 924 | public export
 925 | Arg : Type
 926 | Arg = Arg' Name
 927 | 
 928 | public export
 929 | IArg : Type
 930 | IArg = Arg' KindedName
 931 | 
 932 | export
 933 | isExplicit : Arg' nm -> Maybe (FC, RawImp' nm)
 934 | isExplicit (Explicit fc t) = Just (fc, t)
 935 | isExplicit _ = Nothing
 936 | 
 937 | export
 938 | unIArg : Arg' nm -> RawImp' nm
 939 | unIArg (Explicit _ t) = t
 940 | unIArg (Auto _ t) = t
 941 | unIArg (Named _ _ t) = t
 942 | 
 943 | export
 944 | covering
 945 | Show nm => Show (Arg' nm) where
 946 |   show (Explicit fc t) = show t
 947 |   show (Auto fc t) = "@{" ++ show t ++ "}"
 948 |   show (Named fc n t) = "{" ++ show n ++ " = " ++ show t ++ "}"
 949 | 
 950 | export
 951 | getFnArgs : RawImp' nm -> List (Arg' nm) -> (RawImp' nm, List (Arg' nm))
 952 | getFnArgs (IApp fc f arg) args = getFnArgs f (Explicit fc arg :: args)
 953 | getFnArgs (INamedApp fc f n arg) args = getFnArgs f (Named fc n arg :: args)
 954 | getFnArgs (IAutoApp fc f arg) args = getFnArgs f (Auto fc arg :: args)
 955 | getFnArgs tm args = (tm, args)
 956 | 
 957 | -- TODO: merge these definitions
 958 | namespace Arg
 959 |   export
 960 |   apply : RawImp' nm -> List (Arg' nm) -> RawImp' nm
 961 |   apply f (Explicit fc a :: args) = apply (IApp fc f a) args
 962 |   apply f (Auto fc a :: args) = apply (IAutoApp fc f a) args
 963 |   apply f (Named fc n a :: args) = apply (INamedApp fc f n a) args
 964 |   apply f [] = f
 965 | 
 966 | export
 967 | apply : RawImp' nm -> List (RawImp' nm) -> RawImp' nm
 968 | apply f [] = f
 969 | apply f (x :: xs) =
 970 |   let fFC = getFC f in
 971 |   apply (IApp (fromMaybe fFC (mergeFC fFC (getFC x))) f x) xs
 972 | 
 973 | export
 974 | gapply : RawImp' nm -> List (Maybe Name, RawImp' nm) -> RawImp' nm
 975 | gapply f [] = f
 976 | gapply f (x :: xs) = gapply (uncurry (app f) x) xs where
 977 | 
 978 |   app : RawImp' nm -> Maybe Name -> RawImp' nm -> RawImp' nm
 979 |   app f Nothing   x = IApp (getFC f) f x
 980 |   app f (Just nm) x = INamedApp (getFC f) f nm x
 981 | 
 982 | 
 983 | export
 984 | getFn : RawImp' nm -> RawImp' nm
 985 | getFn (IApp _ f _) = getFn f
 986 | getFn (IWithApp _ f _) = getFn f
 987 | getFn (INamedApp _ f _ _) = getFn f
 988 | getFn (IAutoApp _ f _) = getFn f
 989 | getFn (IAs _ _ _ _ f) = getFn f
 990 | getFn (IMustUnify _ _ f) = getFn f
 991 | getFn f = f
 992 | 
 993 | -- Log message with a RawImp
 994 | export
 995 | logRaw : {auto c : Ref Ctxt Defs} ->
 996 |          LogTopic -> Nat -> Lazy String -> RawImp -> Core ()
 997 | logRaw s n msg tm = log s n $ msg ++ ": " ++ show tm
 998 |