
    0 | module Core.Context
    1 | 
    2 | import        Core.Case.CaseTree
    3 | import        Core.CompileExpr
    4 | import public Core.Context.Context
    5 | import public Core.Core
    6 | import        Core.Env
    7 | import        Core.Hash
    8 | import public Core.Name
    9 | import        Core.Options
   10 | import public Core.Options.Log
   11 | import public Core.TT
   12 | 
   13 | import Libraries.Utils.Binary
   14 | import Libraries.Utils.Path
   15 | import Libraries.Utils.Scheme
   16 | import Libraries.Text.PrettyPrint.Prettyprinter
   17 | 
   18 | import Idris.Syntax.Pragmas
   19 | 
   20 | import Data.Either
   21 | import Data.IOArray
   22 | import Data.List1
   23 | import Data.Nat
   24 | import Libraries.Data.IntMap
   25 | import Libraries.Data.NameMap
   26 | import Libraries.Data.NatSet
   27 | import Libraries.Data.StringMap
   28 | import Libraries.Data.UserNameMap
   29 | import Libraries.Data.WithDefault
   30 | import Libraries.Text.Distance.Levenshtein
   31 | 
   32 | import System.Clock
   33 | import System.Directory
   34 | 
   35 | %default covering
   36 | 
   37 | export
   38 | getContent : Context -> Ref Arr (IOArray ContextEntry)
   39 | getContent = content
   40 | 
   41 | export
   42 | namesResolvedAs : Context -> NameMap Name
   43 | namesResolvedAs ctxt = map Resolved ctxt.resolvedAs
   44 | 
   45 | -- Implemented later, once we can convert to and from full names
   46 | -- Defined in Core.TTC
   47 | export
   48 | decode : Context -> Int -> (update : Bool) -> ContextEntry -> Core GlobalDef
   49 | 
   50 | initSize : Int
   51 | initSize = 10000
   52 | 
   53 | Grow : Int
   54 | Grow = initSize
   55 | 
   56 | export
   57 | initCtxtS : Int -> Core Context
   58 | initCtxtS s
   59 |     = do arr <- coreLift $ newArray s
   60 |          aref <- newRef Arr arr
   61 |          pure $ MkContext
   62 |             { firstEntry = 0
   63 |             , nextEntry = 0
   64 |             , resolvedAs = empty
   65 |             , possibles = empty
   66 |             , content = aref
   67 |             , branchDepth = 0
   68 |             , staging = empty
   69 |             , visibleNS = [partialEvalNS]
   70 |             , allPublic = False
   71 |             , inlineOnly = False
   72 |             , hidden = empty
   73 |             , uconstraints = []
   74 |             }
   75 | 
   76 | export
   77 | initCtxt : Core Context
   78 | initCtxt = initCtxtS initSize
   79 | 
   80 | addPossible : Name -> Int ->
   81 |               UserNameMap (List PossibleName) -> UserNameMap (List PossibleName)
   82 | addPossible n i ps
   83 |     = case userNameRoot n of
   84 |            Nothing => ps
   85 |            Just nr =>
   86 |               case lookup nr ps of
   87 |                    Nothing => insert nr [Direct n i] ps
   88 |                    Just nis => insert nr (Direct n i :: nis) ps
   89 | 
   90 | addAlias : Name -> Name -> Int ->
   91 |            UserNameMap (List PossibleName) -> UserNameMap (List PossibleName)
   92 | addAlias alias full i ps
   93 |     = case userNameRoot alias of
   94 |            Nothing => ps
   95 |            Just nr =>
   96 |               case lookup nr ps of
   97 |                    Nothing => insert nr [Alias alias full i] ps
   98 |                    Just nis => insert nr (Alias alias full i :: nis) ps
   99 | 
  100 | export
  101 | newEntry : Name -> Context -> Core (Int, Context)
  102 | newEntry n ctxt
  103 |     = do let idx = nextEntry ctxt
  104 |          let a = content ctxt
  105 |          arr <- get Arr
  106 |          when (idx >= max arr) $
  107 |                  do arr' <- coreLift $ newArrayCopy (max arr + Grow) arr
  108 |                     put Arr arr'
  109 |          pure (idx, { nextEntry := idx + 1,
  110 |                       resolvedAs $= insert n idx,
  111 |                       possibles $= addPossible n idx
  112 |                     } ctxt)
  113 | 
  114 | -- Get the position of the next entry in the context array, growing the
  115 | -- array if it's out of bounds.
  116 | -- Updates the context with the mapping from name to index
  117 | export
  118 | getPosition : Name -> Context -> Core (Int, Context)
  119 | getPosition (Resolved idx) ctxt = pure (idx, ctxt)
  120 | getPosition n ctxt
  121 |     = case lookup n (resolvedAs ctxt) of
  122 |            Just idx =>
  123 |               do pure (idx, ctxt)
  124 |            Nothing => newEntry n ctxt
  125 | 
  126 | newAlias : Name -> Name -> Context -> Core Context
  127 | newAlias alias full ctxt
  128 |     = do (idx, ctxt) <- getPosition full ctxt
  129 |          pure $ { possibles $= addAlias alias full idx } ctxt
  130 | 
  131 | export
  132 | getNameID : Name -> Context -> Maybe Int
  133 | getNameID (Resolved idx) ctxt = Just idx
  134 | getNameID n ctxt = lookup n (resolvedAs ctxt)
  135 | 
  136 | -- Add the name to the context, or update the existing entry if it's already
  137 | -- there.
  138 | -- If we're not at the top level, add it to the staging area
  139 | export
  140 | addCtxt : Name -> GlobalDef -> Context -> Core (Int, Context)
  141 | addCtxt n val ctxt_in
  142 |     = if branchDepth ctxt_in == 0
  143 |          then do (idx, ctxt) <- getPosition n ctxt_in
  144 |                  let a = content ctxt
  145 |                  arr <- get Arr
  146 |                  coreLift_ $ writeArray arr idx (Decoded val)
  147 |                  pure (idx, ctxt)
  148 |          else do (idx, ctxt) <- getPosition n ctxt_in
  149 |                  pure (idx, { staging $= insert idx (Decoded val) } ctxt)
  150 | 
  151 | export
  152 | addEntry : Name -> ContextEntry -> Context -> Core (Int, Context)
  153 | addEntry n entry ctxt_in
  154 |     = if branchDepth ctxt_in == 0
  155 |          then do (idx, ctxt) <- getPosition n ctxt_in
  156 |                  let a = content ctxt
  157 |                  arr <- get Arr
  158 |                  coreLift_ $ writeArray arr idx entry
  159 |                  pure (idx, ctxt)
  160 |          else do (idx, ctxt) <- getPosition n ctxt_in
  161 |                  pure (idx, { staging $= insert idx entry } ctxt)
  162 | 
  163 | returnDef : Bool -> Int -> GlobalDef -> Maybe (Int, GlobalDef)
  164 | returnDef False idx def = Just (idx, def)
  165 | returnDef True idx def
  166 |     = case definition def of
  167 |            PMDef pi _ _ _ _ =>
  168 |                  if alwaysReduce pi
  169 |                     then Just (idx, def)
  170 |                     else Nothing
  171 |            _ => Nothing
  172 | 
  173 | export
  174 | lookupCtxtExactI : Name -> Context -> Core (Maybe (Int, GlobalDef))
  175 | lookupCtxtExactI (Resolved idx) ctxt
  176 |     = case lookup idx (staging ctxt) of
  177 |            Just val =>
  178 |                  pure $ returnDef (inlineOnly ctxt) idx !(decode ctxt idx True val)
  179 |            Nothing =>
  180 |               do arr <- get Arr @{content ctxt}
  181 |                  Just def <- coreLift (readArray arr idx)
  182 |                       | Nothing => pure Nothing
  183 |                  pure $ returnDef (inlineOnly ctxt) idx !(decode ctxt idx True def)
  184 | lookupCtxtExactI n ctxt
  185 |     = do let Just idx = lookup n (resolvedAs ctxt)
  186 |                   | Nothing => pure Nothing
  187 |          lookupCtxtExactI (Resolved idx) ctxt
  188 | 
  189 | export
  190 | lookupCtxtExact : Name -> Context -> Core (Maybe GlobalDef)
  191 | lookupCtxtExact (Resolved idx) ctxt
  192 |     = case lookup idx (staging ctxt) of
  193 |            Just res =>
  194 |                 do def <- decode ctxt idx True res
  195 |                    pure $ map (\(_, def) => def) $
  196 |                      returnDef (inlineOnly ctxt) idx def
  197 |            Nothing =>
  198 |               do arr <- get Arr @{content ctxt}
  199 |                  Just res <- coreLift (readArray arr idx)
  200 |                       | Nothing => pure Nothing
  201 |                  def <- decode ctxt idx True res
  202 |                  pure $ map (\(_, def) => def) $
  203 |                    returnDef (inlineOnly ctxt) idx def
  204 | lookupCtxtExact n ctxt
  205 |     = do Just (i, def) <- lookupCtxtExactI n ctxt
  206 |               | Nothing => pure Nothing
  207 |          pure (Just def)
  208 | 
  209 | export
  210 | lookupContextEntry : Name -> Context -> Core (Maybe (Int, ContextEntry))
  211 | lookupContextEntry (Resolved idx) ctxt
  212 |     = case lookup idx (staging ctxt) of
  213 |            Just res => pure (Just (idx, res))
  214 |            Nothing =>
  215 |               do let a = content ctxt
  216 |                  arr <- get Arr
  217 |                  Just res <- coreLift (readArray arr idx)
  218 |                       | Nothing => pure Nothing
  219 |                  pure (Just (idx, res))
  220 | lookupContextEntry n ctxt
  221 |     = do let Just idx = lookup n (resolvedAs ctxt)
  222 |                   | Nothing => pure Nothing
  223 |          lookupContextEntry (Resolved idx) ctxt
  224 | 
  225 | ||| Check if the given name has been hidden by the `%hide` directive.
  226 | export
  227 | isHidden : Name -> Context -> Bool
  228 | isHidden fulln ctxt = isJust $ lookup fulln (hidden ctxt)
  229 | 
  230 | ||| Look up a possibly hidden name in the context. The first (boolean) argument
  231 | ||| controls whether names hidden by `%hide` are returned too (True=yes, False=no).
  232 | export
  233 | lookupCtxtName' : Bool -> Name -> Context -> Core (List (Name, Int, GlobalDef))
  234 | lookupCtxtName' allowHidden n ctxt
  235 |     = case userNameRoot n of
  236 |            Nothing => do Just (i, res) <- lookupCtxtExactI n ctxt
  237 |                               | Nothing => pure []
  238 |                          pure [(n, i, res)]
  239 |            Just r =>
  240 |               do let Just ps = lookup r (possibles ctxt)
  241 |                       | Nothing => pure []
  242 |                  lookupPossibles [] ps
  243 |   where
  244 | 
  245 |     resn : (Name, Int, GlobalDef) -> Int
  246 |     resn (_, i, _) = i
  247 | 
  248 |     hlookup : Name -> NameMap () -> Maybe ()
  249 |     hlookup fulln hiddens = if allowHidden
  250 |       then Nothing
  251 |       else lookup fulln hiddens
  252 | 
  253 |     lookupPossibles : List (Name, Int, GlobalDef) -> -- accumulator
  254 |                       List PossibleName ->
  255 |                       Core (List (Name, Int, GlobalDef))
  256 |     lookupPossibles acc [] = pure (reverse acc)
  257 |     lookupPossibles acc (Direct fulln i :: ps)
  258 |        = case (hlookup fulln (hidden ctxt)) of
  259 |               Nothing =>
  260 |                 do Just res <- lookupCtxtExact (Resolved i) ctxt
  261 |                         | Nothing => lookupPossibles acc ps
  262 |                    if matches n fulln && not (i `elem` map resn acc)
  263 |                       then lookupPossibles ((fulln, i, res) :: acc) ps
  264 |                       else lookupPossibles acc ps
  265 |               _ => lookupPossibles acc ps
  266 |     lookupPossibles acc (Alias asn fulln i :: ps)
  267 |        = case (hlookup fulln (hidden ctxt)) of
  268 |               Nothing =>
  269 |                 do Just res <- lookupCtxtExact (Resolved i) ctxt
  270 |                         | Nothing => lookupPossibles acc ps
  271 |                    if (matches n asn) && not (i `elem` map resn acc)
  272 |                       then lookupPossibles ((fulln, i, res) :: acc) ps
  273 |                       else lookupPossibles acc ps
  274 |               _ => lookupPossibles acc ps
  275 | 
  276 | ||| Look up a name in the context, ignoring names hidden by `%hide`.
  277 | export
  278 | lookupCtxtName : Name -> Context -> Core (List (Name, Int, GlobalDef))
  279 | lookupCtxtName = lookupCtxtName' False
  280 | 
  281 | ||| Look up a (possible hidden) name in the context.
  282 | export
  283 | lookupHiddenCtxtName : Name -> Context -> Core (List (Name, Int, GlobalDef))
  284 | lookupHiddenCtxtName = lookupCtxtName' True
  285 | 
  286 | hideName : Name -> Context -> Context
  287 | hideName n ctxt = { hidden $= insert n () } ctxt
  288 | 
  289 | unhideName : Name -> Context -> Context
  290 | unhideName n ctxt = { hidden $= delete n } ctxt
  291 | 
  292 | branchCtxt : Context -> Core Context
  293 | branchCtxt ctxt = pure ({ branchDepth $= S } ctxt)
  294 | 
  295 | commitCtxt : Context -> Core Context
  296 | commitCtxt ctxt
  297 |     = case branchDepth ctxt of
  298 |            Z => pure ctxt
  299 |            S Z => -- add all the things from 'staging' to the real array
  300 |                   do let a = content ctxt
  301 |                      arr <- get Arr
  302 |                      coreLift $ commitStaged (toList (staging ctxt)) arr
  303 |                      pure ({ staging := empty,
  304 |                              branchDepth := Z } ctxt)
  305 |            S k => pure ({ branchDepth := k } ctxt)
  306 |   where
  307 |     -- We know the array must be big enough, because it will have been resized
  308 |     -- if necessary in the branch to fit the index we've been given here
  309 |     commitStaged : List (Int, ContextEntry) -> IOArray ContextEntry -> IO ()
  310 |     commitStaged [] arr = pure ()
  311 |     commitStaged ((idx, val) :: rest) arr
  312 |         = do ignore $ writeArray arr idx val
  313 |              commitStaged rest arr
  314 | 
  315 | ||| Produce a new global definition with a lot of default values
  316 | ||| @fc   definition site
  317 | ||| @n    name
  318 | ||| @rig  quantity annotation
  319 | ||| @vars local variables
  320 | ||| @ty   (closed) type
  321 | ||| @vis  Visibility, defaulting to private
  322 | ||| @def  actual definition
  323 | export
  324 | newDef : (fc : FC) -> (n : Name) -> (rig : RigCount) -> (vars : Scope) ->
  325 |          (ty : ClosedTerm) -> (vis : WithDefault Visibility Private) -> (def : Def) -> GlobalDef
  326 | newDef fc n rig vars ty vis def
  327 |     = MkGlobalDef
  328 |         { location = fc
  329 |         , fullname = n
  330 |         , type = ty
  331 |         , eraseArgs = NatSet.empty
  332 |         , safeErase = NatSet.empty
  333 |         , specArgs = NatSet.empty
  334 |         , inferrable = NatSet.empty
  335 |         , multiplicity = rig
  336 |         , localVars = vars
  337 |         , visibility = vis
  338 |         , totality = unchecked
  339 |         , isEscapeHatch = False
  340 |         , flags = []
  341 |         , refersToM = Nothing
  342 |         , refersToRuntimeM = Nothing
  343 |         , invertible = False
  344 |         , noCycles = False
  345 |         , linearChecked = False
  346 |         , definition = def
  347 |         , compexpr = Nothing
  348 |         , namedcompexpr = Nothing
  349 |         , sizeChange = []
  350 |         , schemeExpr = Nothing
  351 |         }
  352 | 
  353 | -- Rewrite rules, applied after type checking, for runtime code only
  354 | -- LHS and RHS must have the same type, but we don't (currently) require that
  355 | -- the result still type checks (which might happen e.g. if transforming to a
  356 | -- faster implementation with different behaviour)
  357 | -- (Q: Do we need the 'Env' here? Usually we end up needing an 'Env' with a
  358 | -- 'NF but we're working with terms rather than values...)
  359 | public export
  360 | data Transform : Type where
  361 |      MkTransform : {vars : _} ->
  362 |                    Name -> -- name for identifying the rule
  363 |                    Env Term vars -> Term vars -> Term vars -> Transform
  364 | 
  365 | ||| Types that are transformed into a faster representation
  366 | ||| during codegen.
  367 | public export
  368 | data BuiltinType : Type where
  369 |     BuiltinNatural : BuiltinType
  370 |     NaturalToInteger : BuiltinType
  371 |     IntegerToNatural : BuiltinType
  372 | 
  373 | export
  374 | Show BuiltinType where
  375 |     show BuiltinNatural = "Natural"
  376 |     show NaturalToInteger = "NaturalToInteger"
  377 |     show IntegerToNatural = "IntegerToNatural"
  378 | 
  379 | export
  380 | getFnName : Transform -> Maybe Name
  381 | getFnName (MkTransform _ _ app _)
  382 |     = case getFn app of
  383 |            Ref _ _ fn => Just fn
  384 |            _ => Nothing
  385 | 
  386 | -- TODO: refactor via a single function
  387 | -- onNames : (Context -> Name -> Core Name) ->
  388 | --           (Context -> a    -> Core a)
  389 | -- ?
  390 | public export
  391 | interface HasNames a where
  392 |   full : Context -> a -> Core a
  393 |   resolved : Context -> a -> Core a
  394 | 
  395 | export
  396 | HasNames Name where
  397 |   full gam (Resolved i)
  398 |       = do Just gdef <- lookupCtxtExact (Resolved i) gam
  399 |                   -- May occasionally happen when working with metadata.
  400 |                   -- It's harmless, so just silently return the resolved name.
  401 |                 | Nothing => pure (Resolved i)
  402 |            pure (fullname gdef)
  403 |   full gam n = pure n
  404 | 
  405 |   resolved gam (Resolved i)
  406 |       = pure (Resolved i)
  407 |   resolved gam n
  408 |       = do let Just i = getNameID n gam
  409 |                     | Nothing => pure n
  410 |            pure (Resolved i)
  411 | 
  412 | export
  413 | HasNames UConstraint where
  414 |   full gam (ULT x y)
  415 |       = do x' <- full gam x; y' <- full gam y
  416 |            pure (ULT x' y')
  417 |   full gam (ULE x y)
  418 |       = do x' <- full gam x; y' <- full gam y
  419 |            pure (ULE x' y')
  420 | 
  421 |   resolved gam (ULT x y)
  422 |       = do x' <- resolved gam x; y' <- resolved gam y
  423 |            pure (ULT x' y')
  424 |   resolved gam (ULE x y)
  425 |       = do x' <- resolved gam x; y' <- resolved gam y
  426 |            pure (ULE x' y')
  427 | 
  428 | export
  429 | HasNames (Term vars) where
  430 |   full gam (Ref fc x (Resolved i))
  431 |       = do Just gdef <- lookupCtxtExact (Resolved i) gam
  432 |                 | Nothing => pure (Ref fc x (Resolved i))
  433 |            pure (Ref fc x (fullname gdef))
  434 |   full gam (Meta fc x i xs)
  435 |       = do xs <- traverse (full gam) xs
  436 |            pure $ case !(lookupCtxtExact (Resolved i) gam) of
  437 |              Nothing => Meta fc x i xs
  438 |              Just gdef => Meta fc (fullname gdef) i xs
  439 |   full gam (Bind fc x b scope)
  440 |       = pure (Bind fc x !(traverse (full gam) b) !(full gam scope))
  441 |   full gam (App fc fn arg)
  442 |       = pure (App fc !(full gam fn) !(full gam arg))
  443 |   full gam (As fc s p tm)
  444 |       = pure (As fc s !(full gam p) !(full gam tm))
  445 |   full gam (TDelayed fc x y)
  446 |       = pure (TDelayed fc x !(full gam y))
  447 |   full gam (TDelay fc x t y)
  448 |       = pure (TDelay fc x !(full gam t) !(full gam y))
  449 |   full gam (TForce fc r y)
  450 |       = pure (TForce fc r !(full gam y))
  451 |   full gam (TType fc (Resolved i))
  452 |       = do Just gdef <- lookupCtxtExact (Resolved i) gam
  453 |                 | Nothing => pure (TType fc (Resolved i))
  454 |            pure (TType fc (fullname gdef))
  455 |   full gam (Erased fc (Dotted t))
  456 |       = pure (Erased fc (Dotted !(full gam t)))
  457 |   full gam tm = pure tm
  458 | 
  459 |   resolved gam (Ref fc x n)
  460 |       = do let Just i = getNameID n gam
  461 |                 | Nothing => pure (Ref fc x n)
  462 |            pure (Ref fc x (Resolved i))
  463 |   resolved gam (Meta fc x y xs)
  464 |       = do xs' <- traverse (resolved gam) xs
  465 |            let Just i = getNameID x gam
  466 |                | Nothing => pure (Meta fc x y xs')
  467 |            pure (Meta fc x i xs')
  468 |   resolved gam (Bind fc x b scope)
  469 |       = pure (Bind fc x !(traverse (resolved gam) b) !(resolved gam scope))
  470 |   resolved gam (App fc fn arg)
  471 |       = pure (App fc !(resolved gam fn) !(resolved gam arg))
  472 |   resolved gam (As fc s p tm)
  473 |       = pure (As fc s !(resolved gam p) !(resolved gam tm))
  474 |   resolved gam (TDelayed fc x y)
  475 |       = pure (TDelayed fc x !(resolved gam y))
  476 |   resolved gam (TDelay fc x t y)
  477 |       = pure (TDelay fc x !(resolved gam t) !(resolved gam y))
  478 |   resolved gam (TForce fc r y)
  479 |       = pure (TForce fc r !(resolved gam y))
  480 |   resolved gam (TType fc n)
  481 |       = do let Just i = getNameID n gam
  482 |                 | Nothing => pure (TType fc n)
  483 |            pure (TType fc (Resolved i))
  484 |   resolved gam (Erased fc (Dotted t))
  485 |       = pure (Erased fc (Dotted !(resolved gam t)))
  486 |   resolved gam tm = pure tm
  487 | 
  488 | export
  489 | HasNames Pat where
  490 |   full gam (PAs fc n p)
  491 |      = [| PAs (pure fc) (full gam n) (full gam p) |]
  492 |   full gam (PCon fc n i ar ps)
  493 |      = [| PCon (pure fc) (full gam n) (pure i) (pure ar) (traverse (full gam) ps) |]
  494 |   full gam (PTyCon fc n ar ps)
  495 |      = [| PTyCon (pure fc) (full gam n) (pure ar) (traverse (full gam) ps) |]
  496 |   full gam p@(PConst {}) = pure p
  497 |   full gam (PArrow fc x p q)
  498 |      = [| PArrow (pure fc) (full gam x) (full gam p) (full gam q) |]
  499 |   full gam (PDelay fc laz p q)
  500 |      = [| PDelay (pure fc) (pure laz) (full gam p) (full gam q) |]
  501 |   full gam (PLoc fc n) = PLoc fc <$> full gam n
  502 |   full gam (PUnmatchable fc t) = PUnmatchable fc <$> full gam t
  503 | 
  504 |   resolved gam (PAs fc n p)
  505 |      = [| PAs (pure fc) (resolved gam n) (resolved gam p) |]
  506 |   resolved gam (PCon fc n i ar ps)
  507 |      = [| PCon (pure fc) (resolved gam n) (pure i) (pure ar) (traverse (resolved gam) ps) |]
  508 |   resolved gam (PTyCon fc n ar ps)
  509 |      = [| PTyCon (pure fc) (resolved gam n) (pure ar) (traverse (resolved gam) ps) |]
  510 |   resolved gam p@(PConst {}) = pure p
  511 |   resolved gam (PArrow fc x p q)
  512 |      = [| PArrow (pure fc) (resolved gam x) (resolved gam p) (resolved gam q) |]
  513 |   resolved gam (PDelay fc laz p q)
  514 |      = [| PDelay (pure fc) (pure laz) (resolved gam p) (resolved gam q) |]
  515 |   resolved gam (PLoc fc n) = PLoc fc <$> resolved gam n
  516 |   resolved gam (PUnmatchable fc t) = PUnmatchable fc <$> resolved gam t
  517 | 
  518 | mutual
  519 |   export
  520 |   HasNames (CaseTree vars) where
  521 |     full gam (Case i v ty alts)
  522 |         = pure $ Case i v !(full gam ty) !(traverse (full gam) alts)
  523 |     full gam (STerm i tm)
  524 |         = pure $ STerm i !(full gam tm)
  525 |     full gam t = pure t
  526 | 
  527 |     resolved gam (Case i v ty alts)
  528 |         = pure $ Case i v !(resolved gam ty) !(traverse (resolved gam) alts)
  529 |     resolved gam (STerm i tm)
  530 |         = pure $ STerm i !(resolved gam tm)
  531 |     resolved gam t = pure t
  532 | 
  533 |   export
  534 |   HasNames (CaseAlt vars) where
  535 |     full gam (ConCase n t args sc)
  536 |         = do sc' <- full gam sc
  537 |              Just gdef <- lookupCtxtExact n gam
  538 |                 | Nothing => pure (ConCase n t args sc')
  539 |              pure $ ConCase (fullname gdef) t args sc'
  540 |     full gam (DelayCase ty arg sc)
  541 |         = pure $ DelayCase ty arg !(full gam sc)
  542 |     full gam (ConstCase c sc)
  543 |         = pure $ ConstCase c !(full gam sc)
  544 |     full gam (DefaultCase sc)
  545 |         = pure $ DefaultCase !(full gam sc)
  546 | 
  547 |     resolved gam (ConCase n t args sc)
  548 |         = do sc' <- resolved gam sc
  549 |              let Just i = getNameID n gam
  550 |                 | Nothing => pure (ConCase n t args sc')
  551 |              pure $ ConCase (Resolved i) t args sc'
  552 |     resolved gam (DelayCase ty arg sc)
  553 |         = pure $ DelayCase ty arg !(resolved gam sc)
  554 |     resolved gam (ConstCase c sc)
  555 |         = pure $ ConstCase c !(resolved gam sc)
  556 |     resolved gam (DefaultCase sc)
  557 |         = pure $ DefaultCase !(resolved gam sc)
  558 | 
  559 | export
  560 | HasNames (Env Term vars) where
  561 |   full gam [] = pure Env.empty
  562 |   full gam (b :: bs)
  563 |       = pure $ !(traverse (full gam) b) :: !(full gam bs)
  564 | 
  565 |   resolved gam [] = pure Env.empty
  566 |   resolved gam (b :: bs)
  567 |       = pure $ !(traverse (resolved gam) b) :: !(resolved gam bs)
  568 | 
  569 | export
  570 | HasNames Clause where
  571 |   full gam (MkClause env lhs rhs)
  572 |      = pure $ MkClause !(full gam env) !(full gam lhs) !(full gam rhs)
  573 | 
  574 |   resolved gam (MkClause env lhs rhs)
  575 |     = [| MkClause (resolved gam env) (resolved gam lhs) (resolved gam rhs) |]
  576 | 
  577 | 
  578 | export
  579 | HasNames Def where
  580 |   full gam (PMDef r args ct rt pats)
  581 |       = pure $ PMDef r args !(full gam ct) !(full gam rt)
  582 |                      !(traverse fullNamesPat pats)
  583 |     where
  584 |       fullNamesPat : (vs ** (Env Term vs, Term vs, Term vs)) ->
  585 |                      Core (vs ** (Env Term vs, Term vs, Term vs))
  586 |       fullNamesPat (_ ** (env, lhs, rhs))
  587 |           = pure $ (_ ** (!(full gam env),
  588 |                           !(full gam lhs), !(full gam rhs)))
  589 |   full gam (TCon a ps ds u ms mcs det)
  590 |       = pure $ TCon a ps ds u !(traverse (full gam) ms)
  591 |                                 !(traverseOpt (traverse (full gam)) mcs) det
  592 |   full gam (BySearch c d def)
  593 |       = pure $ BySearch c d !(full gam def)
  594 |   full gam (Guess tm b cs)
  595 |       = pure $ Guess !(full gam tm) b cs
  596 |   full gam t = pure t
  597 | 
  598 |   resolved gam (PMDef r args ct rt pats)
  599 |       = pure $ PMDef r args !(resolved gam ct) !(resolved gam rt)
  600 |                      !(traverse resolvedNamesPat pats)
  601 |     where
  602 |       resolvedNamesPat : (vs ** (Env Term vs, Term vs, Term vs)) ->
  603 |                          Core (vs ** (Env Term vs, Term vs, Term vs))
  604 |       resolvedNamesPat (_ ** (env, lhs, rhs))
  605 |           = pure $ (_ ** (!(resolved gam env),
  606 |                           !(resolved gam lhs), !(resolved gam rhs)))
  607 |   resolved gam (TCon a ps ds u ms mcs det)
  608 |       = pure $ TCon a ps ds u !(traverse (resolved gam) ms)
  609 |                                 !(traverseOpt (traverse (full gam)) mcs) det
  610 |   resolved gam (BySearch c d def)
  611 |       = pure $ BySearch c d !(resolved gam def)
  612 |   resolved gam (Guess tm b cs)
  613 |       = pure $ Guess !(resolved gam tm) b cs
  614 |   resolved gam t = pure t
  615 | 
  616 | export
  617 | StripNamespace Def where
  618 |   trimNS ns (PMDef i args ct rt pats)
  619 |       = PMDef i args (trimNS ns ct) rt (map trimNSpat pats)
  620 |     where
  621 |       trimNSpat : (vs ** (Env Term vs, Term vs, Term vs)) ->
  622 |                   (vs ** (Env Term vs, Term vs, Term vs))
  623 |       trimNSpat (vs ** (env, lhs, rhs))
  624 |           = (vs ** (env, trimNS ns lhs, trimNS ns rhs))
  625 |   trimNS ns d = d
  626 | 
  627 |   restoreNS ns (PMDef i args ct rt pats)
  628 |       = PMDef i args (restoreNS ns ct) rt (map restoreNSpat pats)
  629 |     where
  630 |       restoreNSpat : (vs ** (Env Term vs, Term vs, Term vs)) ->
  631 |                   (vs ** (Env Term vs, Term vs, Term vs))
  632 |       restoreNSpat (vs ** (env, lhs, rhs))
  633 |           = (vs ** (env, restoreNS ns lhs, restoreNS ns rhs))
  634 |   restoreNS ns d = d
  635 | 
  636 | export
  637 | StripNamespace GlobalDef where
  638 |   trimNS ns def = { definition $= trimNS ns } def
  639 |   restoreNS ns def = { definition $= restoreNS ns } def
  640 | 
  641 | HasNames (NameMap a) where
  642 |   full gam nmap
  643 |       = insertAll empty (toList nmap)
  644 |     where
  645 |       insertAll : NameMap a -> List (Name, a) -> Core (NameMap a)
  646 |       insertAll ms [] = pure ms
  647 |       insertAll ms ((k, v) :: ns)
  648 |           = insertAll (insert !(full gam k) v ms) ns
  649 | 
  650 |   resolved gam nmap
  651 |       = insertAll empty (toList nmap)
  652 |     where
  653 |       insertAll : NameMap a -> List (Name, a) -> Core (NameMap a)
  654 |       insertAll ms [] = pure ms
  655 |       insertAll ms ((k, v) :: ns)
  656 |           = insertAll (insert !(resolved gam k) v ms) ns
  657 | 
  658 | export
  659 | HasNames PartialReason where
  660 |   full gam NotStrictlyPositive = pure NotStrictlyPositive
  661 |   full gam (BadCall ns) = pure $ BadCall !(traverse (full gam) ns)
  662 |   full gam (BadPath init n) = pure $ BadPath !(traverse (traversePair (full gam)) init) !(full gam n)
  663 |   full gam (RecPath loop) = pure $ RecPath !(traverse (traversePair (full gam)) loop)
  664 | 
  665 |   resolved gam NotStrictlyPositive = pure NotStrictlyPositive
  666 |   resolved gam (BadCall ns) = pure $ BadCall !(traverse (resolved gam) ns)
  667 |   resolved gam (BadPath init n) = pure $ BadPath !(traverse (traversePair (resolved gam)) init) !(resolved gam n)
  668 |   resolved gam (RecPath loop) = pure $ RecPath !(traverse (traversePair (resolved gam)) loop)
  669 | 
  670 | export
  671 | HasNames Terminating where
  672 |   full gam (NotTerminating p) = pure $ NotTerminating !(full gam p)
  673 |   full gam t = pure t
  674 | 
  675 |   resolved gam (NotTerminating p) = pure $ NotTerminating !(resolved gam p)
  676 |   resolved gam t = pure t
  677 | 
  678 | export
  679 | HasNames Covering where
  680 |   full gam IsCovering = pure IsCovering
  681 |   full gam (MissingCases ts)
  682 |       = pure $ MissingCases !(traverse (full gam) ts)
  683 |   full gam (NonCoveringCall ns)
  684 |       = pure $ NonCoveringCall !(traverse (full gam) ns)
  685 | 
  686 |   resolved gam IsCovering = pure IsCovering
  687 |   resolved gam (MissingCases ts)
  688 |       = pure $ MissingCases !(traverse (resolved gam) ts)
  689 |   resolved gam (NonCoveringCall ns)
  690 |       = pure $ NonCoveringCall !(traverse (resolved gam) ns)
  691 | 
  692 | export
  693 | HasNames CaseError where
  694 |   full gam DifferingArgNumbers = pure DifferingArgNumbers
  695 |   full gam DifferingTypes = pure DifferingTypes
  696 |   full gam (MatchErased (vs ** (rho, t))) = do
  697 |     rho <- full gam rho
  698 |     t <- full gam t
  699 |     pure (MatchErased (vs ** (rho, t)))
  700 |   full gam (NotFullyApplied n) = NotFullyApplied <$> full gam n
  701 |   full gam UnknownType = pure UnknownType
  702 | 
  703 |   resolved gam DifferingArgNumbers = pure DifferingArgNumbers
  704 |   resolved gam DifferingTypes = pure DifferingTypes
  705 |   resolved gam (MatchErased (vs ** (rho, t))) = do
  706 |     rho <- resolved gam rho
  707 |     t <- resolved gam t
  708 |     pure (MatchErased (vs ** (rho, t)))
  709 |   resolved gam (NotFullyApplied n) = NotFullyApplied <$> resolved gam n
  710 |   resolved gam UnknownType = pure UnknownType
  711 | 
  712 | 
  713 | export
  714 | HasNames Warning where
  715 |   full gam (ParserWarning fc x) = pure (ParserWarning fc x)
  716 |   full gam (UnreachableClause fc rho s) = UnreachableClause fc <$> full gam rho <*> full gam s
  717 |   full gam (ShadowingGlobalDefs fc xs)
  718 |     = ShadowingGlobalDefs fc <$> traverseList1 (traversePair (traverseList1 (full gam))) xs
  719 |   full gam (IncompatibleVisibility fc x y n) = IncompatibleVisibility fc x y <$> full gam n
  720 |   full gam w@(ShadowingLocalBindings {}) = pure w
  721 |   full gam (Deprecated fc x y) = Deprecated fc x <$> traverseOpt (traversePair (full gam)) y
  722 |   full gam (GenericWarn fc x) = pure (GenericWarn fc x)
  723 | 
  724 |   resolved gam (ParserWarning fc x) = pure (ParserWarning fc x)
  725 |   resolved gam (UnreachableClause fc rho s) = UnreachableClause fc <$> resolved gam rho <*> resolved gam s
  726 |   resolved gam (ShadowingGlobalDefs fc xs)
  727 |     = ShadowingGlobalDefs fc <$> traverseList1 (traversePair (traverseList1 (resolved gam))) xs
  728 |   resolved gam (IncompatibleVisibility fc x y n) = IncompatibleVisibility fc x y <$> resolved gam n
  729 |   resolved gam w@(ShadowingLocalBindings {}) = pure w
  730 |   resolved gam (Deprecated fc x y) = Deprecated fc x <$> traverseOpt (traversePair (resolved gam)) y
  731 |   resolved gam (GenericWarn fc x) = pure (GenericWarn fc x)
  732 | 
  733 | export
  734 | HasNames Error where
  735 |   full gam (Fatal err) = Fatal <$> full gam err
  736 |   full _ (CantConvert fc gam rho s t)
  737 |     = CantConvert fc gam <$> full gam rho <*> full gam s <*> full gam t
  738 |   full _ (CantSolveEq fc gam rho s t)
  739 |     = CantSolveEq fc gam <$> full gam rho <*> full gam s <*> full gam t
  740 |   full gam (PatternVariableUnifies fc fct rho n s)
  741 |     = PatternVariableUnifies fc fct <$> full gam rho <*> full gam n <*> full gam s
  742 |   full gam (CyclicMeta fc rho n s)
  743 |     = CyclicMeta fc <$> full gam rho <*> full gam n <*> full gam s
  744 |   full _ (WhenUnifying fc gam rho s t err)
  745 |     = WhenUnifying fc gam <$> full gam rho <*> full gam s <*> full gam t <*> full gam err
  746 |   full gam (ValidCase fc rho x)
  747 |     = ValidCase fc <$> full gam rho <*> either (map Left . full gam) (map Right . full gam) x
  748 |   full gam (UndefinedName fc n) = UndefinedName fc <$> full gam n
  749 |   full gam (InvisibleName fc n mns) = InvisibleName fc <$> full gam n <*> pure mns
  750 |   full gam (BadTypeConType fc n) = BadTypeConType fc <$> full gam n
  751 |   full gam (BadDataConType fc n n') = BadDataConType fc <$> full gam n <*> full gam n'
  752 |   full gam (NotCovering fc n cov) = NotCovering fc <$> full gam n <*> full gam cov
  753 |   full gam (NotTotal fc n pr) = NotTotal fc <$> full gam n <*> full gam pr
  754 |   full gam ImpossibleCase = pure ImpossibleCase
  755 |   full gam (LinearUsed fc k n) = LinearUsed fc k <$> full gam n
  756 |   full gam (LinearMisuse fc n x y) = LinearMisuse fc <$> full gam n <*> pure x <*> pure y
  757 |   full gam (BorrowPartial fc rho s t) = BorrowPartial fc <$> full gam rho <*> full gam s <*> full gam t
  758 |   full gam (BorrowPartialType fc rho s) = BorrowPartialType fc <$> full gam rho <*> full gam s
  759 |   full gam (AmbiguousName fc xs) = AmbiguousName fc <$> traverse (full gam) xs
  760 |   full gam (AmbiguousElab fc rho xs)
  761 |     = AmbiguousElab fc <$> full gam rho <*> traverse (\ (gam, t) => (gam,) <$> full gam t) xs
  762 |   full gam (AmbiguousSearch fc rho s xs)
  763 |     = AmbiguousSearch fc <$> full gam rho <*> full gam s <*> traverse (full gam) xs
  764 |   full gam (AmbiguityTooDeep fc n xs) = AmbiguityTooDeep fc <$> full gam n <*> traverse (full gam) xs
  765 |   full gam (AllFailed xs)
  766 |      = map AllFailed $ for xs $ \ (mn, err) =>
  767 |          (,) <$> traverseOpt (full gam) mn <*> full gam err
  768 |   full gam (RecordTypeNeeded fc rho) = RecordTypeNeeded fc <$> full gam rho
  769 |   full gam (DuplicatedRecordUpdatePath fc xs) = pure (DuplicatedRecordUpdatePath fc xs)
  770 |   full gam (NotRecordField fc x mn) = NotRecordField fc x <$> traverseOpt (full gam) mn
  771 |   full gam (NotRecordType fc n) = NotRecordType fc <$> full gam n
  772 |   full gam (IncompatibleFieldUpdate fc xs) = pure (IncompatibleFieldUpdate fc xs)
  773 |   full gam (InvalidArgs fc rho xs s) = InvalidArgs fc <$> full gam rho <*> traverse (full gam) xs <*> full gam s
  774 |   full gam (TryWithImplicits fc rho xs)
  775 |     = TryWithImplicits fc <$> full gam rho
  776 |        <*> for xs (\ (n, t) => (,) <$> full gam n <*> full gam t)
  777 |   full gam (BadUnboundImplicit fc rho n s) = BadUnboundImplicit fc <$> full gam rho <*> full gam n <*> full gam s
  778 |   full _ (CantSolveGoal fc gam rho s merr)
  779 |     = CantSolveGoal fc gam <$> full gam rho <*> full gam s <*> traverseOpt (full gam) merr
  780 |   full gam (DeterminingArg fc n x rho s)
  781 |     = DeterminingArg fc <$> full gam n <*> pure x <*> full gam rho <*> full gam s
  782 |   full gam (UnsolvedHoles xs) = UnsolvedHoles <$> traverse (traversePair (full gam)) xs
  783 |   full gam (CantInferArgType fc rho n n1 s)
  784 |     = CantInferArgType fc <$> full gam rho <*> full gam n <*> full gam n1 <*> full gam s
  785 |   full gam (SolvedNamedHole fc rho n s) = SolvedNamedHole fc <$> full gam rho <*> full gam n <*> full gam s
  786 |   full gam (VisibilityError fc x n y n1) = VisibilityError fc x <$> full gam n <*> pure y <*> full gam n1
  787 |   full gam (NonLinearPattern fc n) = NonLinearPattern fc <$> full gam  n
  788 |   full gam (BadPattern fc n) = BadPattern fc <$> full gam n
  789 |   full gam (NoDeclaration fc n) = NoDeclaration fc <$> full gam n
  790 |   full gam (AlreadyDefined fc n) = AlreadyDefined fc <$> full gam n
  791 |   full gam (NotFunctionType fc rho s) = NotFunctionType fc <$> full gam rho <*> full gam s
  792 |   full gam (RewriteNoChange fc rho s t) = RewriteNoChange fc <$> full gam rho <*> full gam s <*> full gam t
  793 |   full gam (NotRewriteRule fc rho s) = NotRewriteRule fc <$> full gam rho <*> full gam s
  794 |   full gam (CaseCompile fc n x) = CaseCompile fc <$> full gam n <*> full gam x
  795 |   full gam (MatchTooSpecific fc rho s) = MatchTooSpecific fc <$> full gam rho <*> full gam s
  796 |   full gam (BadDotPattern fc rho x s t)
  797 |     = BadDotPattern fc <$> full gam rho <*> pure x <*> full gam s <*> full gam t
  798 |   full gam (BadImplicit fc x) = pure (BadImplicit fc x)
  799 |   full gam (BadRunElab fc rho s desc) = BadRunElab fc <$> full gam rho <*> full gam s <*> pure desc
  800 |   full gam (RunElabFail e) = RunElabFail <$> full gam e
  801 |   full gam (GenericMsg fc x) = pure (GenericMsg fc x)
  802 |   full gam (GenericMsgSol fc x y z) = pure (GenericMsgSol fc x y z)
  803 |   full gam (TTCError x) = pure (TTCError x)
  804 |   full gam (FileErr x y) = pure (FileErr x y)
  805 |   full gam (CantFindPackage x) = pure (CantFindPackage x)
  806 |   full gam (LazyImplicitFunction fc) = pure (LazyImplicitFunction fc)
  807 |   full gam (LazyPatternVar fc) = pure (LazyPatternVar fc)
  808 |   full gam (LitFail fc) = pure (LitFail fc)
  809 |   full gam (LexFail fc x) = pure (LexFail fc x)
  810 |   full gam (ParseFail xs) = pure (ParseFail xs)
  811 |   full gam (ModuleNotFound fc x) = pure (ModuleNotFound fc x)
  812 |   full gam (CyclicImports xs) = pure (CyclicImports xs)
  813 |   full gam ForceNeeded = pure ForceNeeded
  814 |   full gam (InternalError x) = pure (InternalError x)
  815 |   full gam (UserError x) = pure (UserError x)
  816 |   full gam (NoForeignCC fc xs) = pure (NoForeignCC fc xs)
  817 |   full gam (BadMultiline fc x) = pure (BadMultiline fc x)
  818 |   full gam (Timeout x) = pure (Timeout x)
  819 |   full gam (FailingDidNotFail fc) = pure (FailingDidNotFail fc)
  820 |   full gam (FailingWrongError fc x err) = FailingWrongError fc x <$> traverseList1 (full gam) err
  821 |   full gam (InType fc n err) = InType fc <$> full gam n <*> full gam err
  822 |   full gam (InCon n err) = InCon <$> traverse (full gam) n <*> full gam err
  823 |   full gam (InLHS fc n err) = InLHS fc <$> full gam n <*> full gam err
  824 |   full gam (InRHS fc n err) = InRHS fc <$> full gam n <*> full gam err
  825 |   full gam (MaybeMisspelling err xs) = MaybeMisspelling <$> full gam err <*> pure xs
  826 |   full gam (WarningAsError wrn) = WarningAsError <$> full gam wrn
  827 |   full gam (OperatorBindingMismatch {print} fc expected actual (Left opName) rhs candidates)
  828 |       = OperatorBindingMismatch {print} fc expected actual
  829 |           <$> (Left <$> full gam opName) <*> pure rhs <*> pure candidates
  830 |   full gam (OperatorBindingMismatch {print} fc expected actual (Right opName) rhs candidates)
  831 |       = OperatorBindingMismatch {print} fc expected actual
  832 |           <$> (Right <$> full gam opName) <*> pure rhs <*> pure candidates
  833 | 
  834 |   resolved gam (Fatal err) = Fatal <$> resolved gam err
  835 |   resolved _ (CantConvert fc gam rho s t)
  836 |     = CantConvert fc gam <$> resolved gam rho <*> resolved gam s <*> resolved gam t
  837 |   resolved _ (CantSolveEq fc gam rho s t)
  838 |     = CantSolveEq fc gam <$> resolved gam rho <*> resolved gam s <*> resolved gam t
  839 |   resolved gam (PatternVariableUnifies fc fct rho n s)
  840 |     = PatternVariableUnifies fc fct <$> resolved gam rho <*> resolved gam n <*> resolved gam s
  841 |   resolved gam (CyclicMeta fc rho n s)
  842 |     = CyclicMeta fc <$> resolved gam rho <*> resolved gam n <*> resolved gam s
  843 |   resolved _ (WhenUnifying fc gam rho s t err)
  844 |     = WhenUnifying fc gam <$> resolved gam rho <*> resolved gam s <*> resolved gam t <*> resolved gam err
  845 |   resolved gam (ValidCase fc rho x)
  846 |     = ValidCase fc <$> resolved gam rho <*> either (map Left . resolved gam) (map Right . resolved gam) x
  847 |   resolved gam (UndefinedName fc n) = UndefinedName fc <$> resolved gam n
  848 |   resolved gam (InvisibleName fc n mns) = InvisibleName fc <$> resolved gam n <*> pure mns
  849 |   resolved gam (BadTypeConType fc n) = BadTypeConType fc <$> resolved gam n
  850 |   resolved gam (BadDataConType fc n n') = BadDataConType fc <$> resolved gam n <*> resolved gam n'
  851 |   resolved gam (NotCovering fc n cov) = NotCovering fc <$> resolved gam n <*> resolved gam cov
  852 |   resolved gam (NotTotal fc n pr) = NotTotal fc <$> resolved gam n <*> resolved gam pr
  853 |   resolved gam ImpossibleCase = pure ImpossibleCase
  854 |   resolved gam (LinearUsed fc k n) = LinearUsed fc k <$> resolved gam n
  855 |   resolved gam (LinearMisuse fc n x y) = LinearMisuse fc <$> resolved gam n <*> pure x <*> pure y
  856 |   resolved gam (BorrowPartial fc rho s t) = BorrowPartial fc <$> resolved gam rho <*> resolved gam s <*> resolved gam t
  857 |   resolved gam (BorrowPartialType fc rho s) = BorrowPartialType fc <$> resolved gam rho <*> resolved gam s
  858 |   resolved gam (AmbiguousName fc xs) = AmbiguousName fc <$> traverse (resolved gam) xs
  859 |   resolved gam (AmbiguousElab fc rho xs)
  860 |     = AmbiguousElab fc <$> resolved gam rho <*> traverse (\ (gam, t) => (gam,) <$> resolved gam t) xs
  861 |   resolved gam (AmbiguousSearch fc rho s xs)
  862 |     = AmbiguousSearch fc <$> resolved gam rho <*> resolved gam s <*> traverse (resolved gam) xs
  863 |   resolved gam (AmbiguityTooDeep fc n xs) = AmbiguityTooDeep fc <$> resolved gam n <*> traverse (resolved gam) xs
  864 |   resolved gam (AllFailed xs)
  865 |      = map AllFailed $ for xs $ \ (mn, err) =>
  866 |          (,) <$> traverseOpt (resolved gam) mn <*> resolved gam err
  867 |   resolved gam (RecordTypeNeeded fc rho) = RecordTypeNeeded fc <$> resolved gam rho
  868 |   resolved gam (DuplicatedRecordUpdatePath fc xs) = pure (DuplicatedRecordUpdatePath fc xs)
  869 |   resolved gam (NotRecordField fc x mn) = NotRecordField fc x <$> traverseOpt (resolved gam) mn
  870 |   resolved gam (NotRecordType fc n) = NotRecordType fc <$> resolved gam n
  871 |   resolved gam (IncompatibleFieldUpdate fc xs) = pure (IncompatibleFieldUpdate fc xs)
  872 |   resolved gam (InvalidArgs fc rho xs s) = InvalidArgs fc <$> resolved gam rho <*> traverse (resolved gam) xs <*> resolved gam s
  873 |   resolved gam (TryWithImplicits fc rho xs)
  874 |     = TryWithImplicits fc <$> resolved gam rho
  875 |        <*> for xs (\ (n, t) => (,) <$> resolved gam n <*> resolved gam t)
  876 |   resolved gam (BadUnboundImplicit fc rho n s) = BadUnboundImplicit fc <$> resolved gam rho <*> resolved gam n <*> resolved gam s
  877 |   resolved _ (CantSolveGoal fc gam rho s merr)
  878 |     = CantSolveGoal fc gam <$> resolved gam rho <*> resolved gam s <*> traverseOpt (resolved gam) merr
  879 |   resolved gam (DeterminingArg fc n x rho s)
  880 |     = DeterminingArg fc <$> resolved gam n <*> pure x <*> resolved gam rho <*> resolved gam s
  881 |   resolved gam (UnsolvedHoles xs) = UnsolvedHoles <$> traverse (traversePair (resolved gam)) xs
  882 |   resolved gam (CantInferArgType fc rho n n1 s)
  883 |     = CantInferArgType fc <$> resolved gam rho <*> resolved gam n <*> resolved gam n1 <*> resolved gam s
  884 |   resolved gam (SolvedNamedHole fc rho n s) = SolvedNamedHole fc <$> resolved gam rho <*> resolved gam n <*> resolved gam s
  885 |   resolved gam (VisibilityError fc x n y n1) = VisibilityError fc x <$> resolved gam n <*> pure y <*> resolved gam n1
  886 |   resolved gam (NonLinearPattern fc n) = NonLinearPattern fc <$> resolved gam  n
  887 |   resolved gam (BadPattern fc n) = BadPattern fc <$> resolved gam n
  888 |   resolved gam (NoDeclaration fc n) = NoDeclaration fc <$> resolved gam n
  889 |   resolved gam (AlreadyDefined fc n) = AlreadyDefined fc <$> resolved gam n
  890 |   resolved gam (NotFunctionType fc rho s) = NotFunctionType fc <$> resolved gam rho <*> resolved gam s
  891 |   resolved gam (RewriteNoChange fc rho s t) = RewriteNoChange fc <$> resolved gam rho <*> resolved gam s <*> resolved gam t
  892 |   resolved gam (NotRewriteRule fc rho s) = NotRewriteRule fc <$> resolved gam rho <*> resolved gam s
  893 |   resolved gam (CaseCompile fc n x) = CaseCompile fc <$> resolved gam n <*> resolved gam x
  894 |   resolved gam (MatchTooSpecific fc rho s) = MatchTooSpecific fc <$> resolved gam rho <*> resolved gam s
  895 |   resolved gam (BadDotPattern fc rho x s t)
  896 |     = BadDotPattern fc <$> resolved gam rho <*> pure x <*> resolved gam s <*> resolved gam t
  897 |   resolved gam (BadImplicit fc x) = pure (BadImplicit fc x)
  898 |   resolved gam (BadRunElab fc rho s desc) = BadRunElab fc <$> resolved gam rho <*> resolved gam s <*> pure desc
  899 |   resolved gam (RunElabFail e) = RunElabFail <$> resolved gam e
  900 |   resolved gam (GenericMsg fc x) = pure (GenericMsg fc x)
  901 |   resolved gam (GenericMsgSol fc x y z) = pure (GenericMsgSol fc x y z)
  902 |   resolved gam (TTCError x) = pure (TTCError x)
  903 |   resolved gam (FileErr x y) = pure (FileErr x y)
  904 |   resolved gam (CantFindPackage x) = pure (CantFindPackage x)
  905 |   resolved gam (LazyImplicitFunction fc) = pure (LazyImplicitFunction fc)
  906 |   resolved gam (LazyPatternVar fc) = pure (LazyPatternVar fc)
  907 |   resolved gam (LitFail fc) = pure (LitFail fc)
  908 |   resolved gam (LexFail fc x) = pure (LexFail fc x)
  909 |   resolved gam (ParseFail xs) = pure (ParseFail xs)
  910 |   resolved gam (ModuleNotFound fc x) = pure (ModuleNotFound fc x)
  911 |   resolved gam (CyclicImports xs) = pure (CyclicImports xs)
  912 |   resolved gam ForceNeeded = pure ForceNeeded
  913 |   resolved gam (InternalError x) = pure (InternalError x)
  914 |   resolved gam (UserError x) = pure (UserError x)
  915 |   resolved gam (NoForeignCC fc xs) = pure (NoForeignCC fc xs)
  916 |   resolved gam (BadMultiline fc x) = pure (BadMultiline fc x)
  917 |   resolved gam (Timeout x) = pure (Timeout x)
  918 |   resolved gam (FailingDidNotFail fc) = pure (FailingDidNotFail fc)
  919 |   resolved gam (FailingWrongError fc x err) = FailingWrongError fc x <$> traverseList1 (resolved gam) err
  920 |   resolved gam (InType fc n err) = InType fc <$> resolved gam n <*> resolved gam err
  921 |   resolved gam (InCon n err) = InCon <$> traverse (resolved gam) n <*> resolved gam err
  922 |   resolved gam (InLHS fc n err) = InLHS fc <$> resolved gam n <*> resolved gam err
  923 |   resolved gam (InRHS fc n err) = InRHS fc <$> resolved gam n <*> resolved gam err
  924 |   resolved gam (MaybeMisspelling err xs) = MaybeMisspelling <$> resolved gam err <*> pure xs
  925 |   resolved gam (WarningAsError wrn) = WarningAsError <$> resolved gam wrn
  926 |   resolved gam (OperatorBindingMismatch {print} fc expected actual (Left opName) rhs candidates)
  927 |       = OperatorBindingMismatch {print} fc expected actual
  928 |           <$> (Left <$> resolved gam opName) <*> pure rhs <*> pure candidates
  929 |   resolved gam (OperatorBindingMismatch {print} fc expected actual (Right opName) rhs candidates)
  930 |       = OperatorBindingMismatch {print} fc expected actual
  931 |           <$> (Right <$> resolved gam opName) <*> pure rhs <*> pure candidates
  932 | 
  933 | export
  934 | HasNames Totality where
  935 |   full gam (MkTotality t c) = pure $ MkTotality !(full gam t) !(full gam c)
  936 |   resolved gam (MkTotality t c) = pure $ MkTotality !(resolved gam t) !(resolved gam c)
  937 | 
  938 | export
  939 | HasNames SCCall where
  940 |   full gam sc = pure $ { fnCall := !(full gam (fnCall sc)) } sc
  941 |   resolved gam sc = pure $ { fnCall := !(resolved gam (fnCall sc)) } sc
  942 | 
  943 | export
  944 | HasNames a => HasNames (Maybe a) where
  945 |   full gam Nothing = pure Nothing
  946 |   full gam (Just x) = pure $ Just !(full gam x)
  947 |   resolved gam Nothing = pure Nothing
  948 |   resolved gam (Just x) = pure $ Just !(resolved gam x)
  949 | 
  950 | export
  951 | HasNames GlobalDef where
  952 |   full gam def
  953 |       = do
  954 | --            ts <- full gam (type def)
  955 | --            d <- full gam (definition def)
  956 | --            coreLift $ printLn (fullname def, ts)
  957 | --            coreLift $ printLn (fullname def, d)
  958 |            pure $ { type := !(full gam (type def)),
  959 |                     definition := !(full gam (definition def)),
  960 |                     totality := !(full gam (totality def)),
  961 |                     refersToM := !(full gam (refersToM def)),
  962 |                     refersToRuntimeM := !(full gam (refersToRuntimeM def)),
  963 |                     sizeChange := !(traverse (full gam) (sizeChange def))
  964 |                   } def
  965 |   resolved gam def
  966 |       = pure $ { type := !(resolved gam (type def)),
  967 |                  definition := !(resolved gam (definition def)),
  968 |                  totality := !(resolved gam (totality def)),
  969 |                  refersToM := !(resolved gam (refersToM def)),
  970 |                  refersToRuntimeM := !(resolved gam (refersToRuntimeM def)),
  971 |                  sizeChange := !(traverse (resolved gam) (sizeChange def))
  972 |                } def
  973 | 
  974 | export
  975 | HasNames Transform where
  976 |   full gam (MkTransform n env lhs rhs)
  977 |       = pure $ MkTransform !(full gam n) !(full gam env)
  978 |                            !(full gam lhs) !(full gam rhs)
  979 | 
  980 |   resolved gam (MkTransform n env lhs rhs)
  981 |       = pure $ MkTransform !(resolved gam n) !(resolved gam env)
  982 |                            !(resolved gam lhs) !(resolved gam rhs)
  983 | 
  984 | -- Return all the currently defined names
  985 | export
  986 | allNames : Context -> Core (List Name)
  987 | allNames ctxt = traverse (full ctxt) $ map Resolved [1..nextEntry ctxt - 1]
  988 | 
  989 | public export
  990 | record Defs where
  991 |   constructor MkDefs
  992 |   gamma : Context
  993 |   mutData : List Name -- Currently declared but undefined data types
  994 |   currentNS : Namespace -- namespace for current definitions
  995 |   nestedNS : List Namespace -- other nested namespaces we can look in
  996 |   options : Options
  997 |   toSave : NameMap ()
  998 |   typeHints : NameMap (List (Name, Bool))
  999 |      -- ^ a mapping from type names to hints (and a flag setting whether it's
 1000 |      -- a "direct" hint). Direct hints are searched first (as part of a group)
 1001 |      -- the indirect hints. Indirect hints, in practice, are used to find
 1002 |      -- instances of parent interfaces, and we don't search these until we've
 1003 |      -- tried to find a direct result via a constructor or a top level hint.
 1004 |   autoHints : NameMap Bool
 1005 |      -- ^ global search hints. A mapping from the hint name, to whether it is
 1006 |      -- a "default hint". A default hint is used only if all other attempts
 1007 |      -- to search fail (this flag is really only intended as a mechanism
 1008 |      -- for defaulting of literals)
 1009 |   openHints : NameMap ()
 1010 |      -- ^ currently open global hints; just for the rest of this module (not exported)
 1011 |      -- and prioritised
 1012 |   localHints : NameMap ()
 1013 |      -- ^ Hints defined in the current environment
 1014 |   saveTypeHints : List (Name, Name, Bool)
 1015 |      -- We don't look up anything in here, it's merely for saving out to TTC.
 1016 |      -- We save the hints in the 'GlobalDef' itself for faster lookup.
 1017 |   saveAutoHints : List (Name, Bool)
 1018 |   transforms : NameMap (List Transform)
 1019 |      -- ^ A mapping from names to transformation rules which update applications
 1020 |      -- of that name
 1021 |   saveTransforms : List (Name, Transform)
 1022 |   namedirectives : NameMap (List String)
 1023 |   ifaceHash : Int
 1024 |   importHashes : List (Namespace, Int)
 1025 |      -- ^ interface hashes of imported modules
 1026 |   imported : List (ModuleIdent, Bool, Namespace)
 1027 |      -- ^ imported modules, whether to rexport, as namespace
 1028 |   allImported : List (String, (ModuleIdent, Bool, Namespace))
 1029 |      -- ^ all imported filenames/namespaces, just to avoid loading something
 1030 |      -- twice unnecessarily (this is a record of all the things we've
 1031 |      -- called 'readFromTTC' with, in practice)
 1032 |   cgdirectives : List (CG, String)
 1033 |      -- ^ Code generator directives, which are free form text and thus to
 1034 |      -- be interpreted however the specific code generator requires
 1035 |   toCompileCase : List Name
 1036 |      -- ^ Names which need to be compiled to run time case trees
 1037 |   incData : List (CG, String, List String)
 1038 |      -- ^ What we've compiled incrementally for this module: codegen,
 1039 |      -- object file, any additional CG dependent data (e.g. linker flags)
 1040 |   allIncData : List (CG, List String, List String)
 1041 |      -- ^ Incrementally compiled files for all imports. Only lists CGs for
 1042 |      -- while all modules have associated incremental compile data
 1043 |   toIR : NameMap ()
 1044 |      -- ^ Names which need to be compiled to IR at the end of processing
 1045 |      -- the current module
 1046 |   userHoles : NameMap Bool
 1047 |      -- ^ Metavariables the user still has to fill in. In practice, that's
 1048 |      -- everything with a user accessible name and a definition of Hole.
 1049 |      -- The Bool says whether it was introduced in another module.
 1050 |   peFailures : NameMap ()
 1051 |      -- ^ Partial evaluation names which have failed, so don't bother trying
 1052 |      -- again
 1053 |   timings : StringMap (Bool, Integer)
 1054 |      -- ^ record of timings from logTimeRecord
 1055 |   timer : Maybe (Integer, String)
 1056 |      -- ^ for timing and checking timeouts; the maximum time after which a
 1057 |      -- timeout should be thrown
 1058 |   warnings : List Warning
 1059 |      -- ^ as yet unreported warnings
 1060 |   schemeEvalLoaded : Bool
 1061 |   foreignExports : NameMap (List (String, String))
 1062 |        -- ^ For functions which are callable from a foreign language. This
 1063 |        -- maps names to a pair of the back end and the exported function name
 1064 |   defsStack : SnocList Name -- stack of the definition names being processed
 1065 | 
 1066 | -- Label for context references
 1067 | export
 1068 | data Ctxt : Type where
 1069 | 
 1070 | 
 1071 | export
 1072 | clearDefs : Defs -> Core Defs
 1073 | clearDefs defs
 1074 |     = pure ({ gamma->inlineOnly := True } defs)
 1075 | 
 1076 | export
 1077 | initDefs : Core Defs
 1078 | initDefs
 1079 |     = do gam <- initCtxt
 1080 |          opts <- defaults
 1081 |          pure $ MkDefs
 1082 |            { gamma = gam
 1083 |            , mutData = []
 1084 |            , currentNS = mainNS
 1085 |            , nestedNS = []
 1086 |            , options = opts
 1087 |            , toSave = empty
 1088 |            , typeHints = empty
 1089 |            , autoHints = empty
 1090 |            , openHints = empty
 1091 |            , localHints = empty
 1092 |            , saveTypeHints = []
 1093 |            , saveAutoHints = []
 1094 |            , transforms = empty
 1095 |            , saveTransforms = []
 1096 |            , namedirectives = empty
 1097 |            , ifaceHash = 5381
 1098 |            , importHashes = []
 1099 |            , imported = []
 1100 |            , allImported = []
 1101 |            , cgdirectives = []
 1102 |            , toCompileCase = []
 1103 |            , incData = []
 1104 |            , allIncData = []
 1105 |            , toIR = empty
 1106 |            , userHoles = empty
 1107 |            , peFailures = empty
 1108 |            , timings = empty
 1109 |            , timer = Nothing
 1110 |            , warnings = []
 1111 |            , schemeEvalLoaded = False
 1112 |            , foreignExports = empty
 1113 |            , defsStack = [<]
 1114 |            }
 1115 | 
 1116 | -- Reset the context, except for the options
 1117 | export
 1118 | clearCtxt : {auto c : Ref Ctxt Defs} ->
 1119 |             Core ()
 1120 | clearCtxt
 1121 |     = do defs <- get Ctxt
 1122 |          put Ctxt ({ options := resetElab (options defs),
 1123 |                      timings := timings defs } !initDefs)
 1124 |   where
 1125 |     resetElab : Options -> Options
 1126 |     resetElab opts =
 1127 |       let tot = totalReq (session opts) in
 1128 |       { elabDirectives := { totality := tot } defaultElab } opts
 1129 | 
 1130 | export
 1131 | getFieldNames : Context -> Namespace -> List Name
 1132 | getFieldNames ctxt recNS
 1133 |   = let nms = resolvedAs ctxt in
 1134 |     keys $ flip filterBy nms $ \ n =>
 1135 |       case isRF n of
 1136 |         Nothing => False
 1137 |         Just (ns, field) => ns == recNS
 1138 | 
 1139 | -- Find similar looking names in the context
 1140 | export
 1141 | getSimilarNames : {auto c : Ref Ctxt Defs} ->
 1142 |                   -- Predicate run to customise the behavior of looking for similar names
 1143 |                   -- Sometime we might want to hide names that we know make no sense.
 1144 |                   {default Nothing keepPredicate : Maybe ((Name, GlobalDef) -> Core Bool)} ->
 1145 |                   Name -> Core (Maybe (String, List (Name, Visibility, Nat)))
 1146 | getSimilarNames nm = case show <$> userNameRoot nm of
 1147 |   Nothing => pure Nothing
 1148 |   Just str => if length str <= 1 then pure (Just (str, [])) else
 1149 |     do defs <- get Ctxt
 1150 |        let threshold : Nat := max 1 (assert_total (divNat (length str) 3))
 1151 |        let test : Name -> Core (Maybe (Visibility, Nat)) := \ nm => do
 1152 |                let (Just str') = show <$> userNameRoot nm
 1153 |                    | _ => pure Nothing
 1154 |                dist <- coreLift $ Levenshtein.compute str str'
 1155 |                let True = dist <= threshold
 1156 |                    | False => pure Nothing
 1157 |                Just def <- lookupCtxtExact nm (gamma defs)
 1158 |                    | Nothing => pure Nothing -- should be impossible
 1159 |                let predicate = fromMaybe (\_ => pure True) keepPredicate
 1160 |                True <- predicate (nm, def)
 1161 |                    | False => pure Nothing
 1162 |                pure (Just (collapseDefault $ visibility def, dist))
 1163 |        kept <- NameMap.mapMaybeM @{CORE} test (resolvedAs (gamma defs))
 1164 |        pure $ Just (str, toList kept)
 1165 | 
 1166 | export
 1167 | showSimilarNames : Namespace -> Name -> String ->
 1168 |                    List (Name, Visibility, Nat) -> List String
 1169 | showSimilarNames ns nm str kept
 1170 |   = let (loc, priv) := partitionEithers $ kept <&> \ (nm', vis, n) =>
 1171 |                          let False = fst (splitNS nm') `isParentOf` ns
 1172 |                                | _ => Left (nm', n)
 1173 |                              Private = vis
 1174 |                                | _ => Left (nm', n)
 1175 |                          in Right (nm', n)
 1176 |         sorted      := sortBy (compare `on` snd)
 1177 |         roots1      := mapMaybe (showNames nm str False . fst) (sorted loc)
 1178 |         roots2      := mapMaybe (showNames nm str True  . fst) (sorted priv)
 1179 |     in nub roots1 ++ nub roots2
 1180 | 
 1181 |   where
 1182 | 
 1183 |   showNames : Name -> String -> Bool -> Name -> Maybe String
 1184 |   showNames target str priv nm = do
 1185 |     let adj  = if priv then " (not exported)" else ""
 1186 |     let root = nameRoot nm
 1187 |     let True = str == root
 1188 |       | _ => pure (root ++ adj)
 1189 |     let full = show (pretty nm)
 1190 |     let True = (str == full || show target == full) && not priv
 1191 |       | _ => pure (full ++ adj)
 1192 |     Nothing
 1193 | 
 1194 | 
 1195 | getVisibility : {auto c : Ref Ctxt Defs} ->
 1196 |                 FC -> Name -> Core (WithDefault Visibility Private)
 1197 | getVisibility fc n
 1198 |     = do defs <- get Ctxt
 1199 |          Just def <- lookupCtxtExact n (gamma defs)
 1200 |               | Nothing => throw (UndefinedName fc n)
 1201 |          pure $ visibility def
 1202 | 
 1203 | maybeMisspelling : {auto c : Ref Ctxt Defs} ->
 1204 |                    Error -> Name -> Core a
 1205 | maybeMisspelling err nm = do
 1206 |   ns <- currentNS <$> get Ctxt
 1207 |   Just (str, kept) <- getSimilarNames nm
 1208 |     | Nothing => throw err
 1209 |   let candidates = showSimilarNames ns nm str kept
 1210 |   case candidates of
 1211 |     [] => throw err
 1212 |     (x::xs) => throw (MaybeMisspelling err (x ::: xs))
 1213 | 
 1214 | -- Throw an UndefinedName exception. But try to find similar names first.
 1215 | export
 1216 | undefinedName : {auto c : Ref Ctxt Defs} ->
 1217 |                 FC -> Name -> Core a
 1218 | undefinedName loc nm = maybeMisspelling (UndefinedName loc nm) nm
 1219 | 
 1220 | -- Throw a NoDeclaration exception. But try to find similar names first.
 1221 | export
 1222 | noDeclaration : {auto c : Ref Ctxt Defs} ->
 1223 |                 FC -> Name -> Core a
 1224 | noDeclaration loc nm = maybeMisspelling (NoDeclaration loc nm) nm
 1225 | 
 1226 | export
 1227 | ambiguousName : {auto c : Ref Ctxt Defs} -> FC
 1228 |              -> Name -> List Name
 1229 |              -> Core a
 1230 | ambiguousName fc n ns = do
 1231 |   ns <- filterM (\x => pure $ !(collapseDefault <$> getVisibility fc x) /= Private) ns
 1232 |   case ns of
 1233 |     [] =>         undefinedName fc n
 1234 |     ns => throw $ AmbiguousName fc ns
 1235 | 
 1236 | -- Get the canonical name of something that might have been aliased via
 1237 | -- import as
 1238 | export
 1239 | canonicalName : {auto c : Ref Ctxt Defs} ->
 1240 |                 FC -> Name -> Core Name
 1241 | canonicalName fc n
 1242 |     = do defs <- get Ctxt
 1243 |          case !(lookupCtxtName n (gamma defs)) of
 1244 |               [(n, _, _)] => pure n
 1245 |               ns => ambiguousName fc n (map fst ns)
 1246 | 
 1247 | -- If the name is aliased, get the alias
 1248 | export
 1249 | aliasName : {auto c : Ref Ctxt Defs} ->
 1250 |             Name -> Core Name
 1251 | aliasName fulln
 1252 |     = do defs <- get Ctxt
 1253 |          let Just r = userNameRoot fulln
 1254 |                 | Nothing => pure fulln
 1255 |          let Just ps = lookup r (possibles (gamma defs))
 1256 |                 | Nothing => pure fulln
 1257 |          findAlias ps
 1258 |   where
 1259 |     findAlias : List PossibleName -> Core Name
 1260 |     findAlias [] = pure fulln
 1261 |     findAlias (Alias as full i :: ps)
 1262 |         = if full == fulln
 1263 |              then pure as
 1264 |              else findAlias ps
 1265 |     findAlias (_ :: ps) = findAlias ps
 1266 | 
 1267 | -- Beware: if your hashable thing contains (potentially resolved) names,
 1268 | -- it'll be better to use addHashWithNames to make the hash independent
 1269 | -- of the internal numbering of names.
 1270 | export
 1271 | addHash : {auto c : Ref Ctxt Defs} -> Hashable a => a -> Core ()
 1272 | addHash x = update Ctxt { ifaceHash $= flip hashWithSalt x }
 1273 | 
 1274 | export
 1275 | initHash : {auto c : Ref Ctxt Defs} -> Core ()
 1276 | initHash = update Ctxt { ifaceHash := 5381 }
 1277 | 
 1278 | export
 1279 | addUserHole : {auto c : Ref Ctxt Defs} ->
 1280 |               Bool -> -- defined in another module?
 1281 |               Name -> -- hole name
 1282 |               Core ()
 1283 | addUserHole ext n = update Ctxt { userHoles $= insert n ext }
 1284 | 
 1285 | export
 1286 | clearUserHole : {auto c : Ref Ctxt Defs} -> Name -> Core ()
 1287 | clearUserHole n = update Ctxt { userHoles $= delete n }
 1288 | 
 1289 | export
 1290 | getUserHoles : {auto c : Ref Ctxt Defs} ->
 1291 |                Core (List Name)
 1292 | getUserHoles
 1293 |     = do defs <- get Ctxt
 1294 |          let hs = sort (keys (userHoles defs))
 1295 |          filterM (isHole defs) hs
 1296 |   where
 1297 |     -- If a hole is declared in one file and defined in another, its
 1298 |     -- name won't have been cleared unless we've already looked up its
 1299 |     -- definition (as addDef needs to be called to clear it). So here
 1300 |     -- check that it's really a hole
 1301 |     isHole : Defs -> Name -> Core Bool
 1302 |     isHole defs n
 1303 |         = do Just def <- lookupCtxtExact n (gamma defs)
 1304 |                   | Nothing => pure True
 1305 |              pure $ case definition def of
 1306 |                   None => True
 1307 |                   Hole {} => True
 1308 |                   _ => False
 1309 | 
 1310 | export
 1311 | addDef : {auto c : Ref Ctxt Defs} ->
 1312 |          Name -> GlobalDef -> Core Int
 1313 | addDef n def
 1314 |     = do defs <- get Ctxt
 1315 |          (idx, gam') <- addCtxt n def (gamma defs)
 1316 |          put Ctxt ({ gamma := gam' } defs)
 1317 |          case definition def of
 1318 |               None => pure ()
 1319 |               Hole {} => pure ()
 1320 |               _ => clearUserHole (fullname def)
 1321 |          pure idx
 1322 | 
 1323 | export
 1324 | addContextEntry : {auto c : Ref Ctxt Defs} ->
 1325 |                   Namespace -> Name -> Binary -> Core Int
 1326 | addContextEntry ns n def
 1327 |     = do defs <- get Ctxt
 1328 |          (idx, gam') <- addEntry n (Coded ns def) (gamma defs)
 1329 |          put Ctxt ({ gamma := gam' } defs)
 1330 |          pure idx
 1331 | 
 1332 | export
 1333 | addContextAlias : {auto c : Ref Ctxt Defs} ->
 1334 |                   Name -> Name -> Core ()
 1335 | addContextAlias alias full
 1336 |     = do defs <- get Ctxt
 1337 |          Nothing <- lookupCtxtExact alias (gamma defs)
 1338 |              | _ => pure () -- Don't add the alias if the name exists already
 1339 |          gam' <- newAlias alias full (gamma defs)
 1340 |          put Ctxt ({ gamma := gam' } defs)
 1341 | 
 1342 | export
 1343 | addBuiltin : {arity : _} ->
 1344 |              {auto x : Ref Ctxt Defs} ->
 1345 |              Name -> ClosedTerm -> Totality ->
 1346 |              PrimFn arity -> Core ()
 1347 | addBuiltin n ty tot op
 1348 |    = do ignore $
 1349 |        addDef n $ MkGlobalDef
 1350 |          { location = emptyFC
 1351 |          , fullname = n
 1352 |          , type = ty
 1353 |          , eraseArgs = NatSet.empty
 1354 |          , safeErase = NatSet.empty
 1355 |          , specArgs = NatSet.empty
 1356 |          , inferrable = NatSet.empty
 1357 |          , multiplicity = top
 1358 |          , localVars = Scope.empty
 1359 |          , visibility = specified Public
 1360 |          , totality = tot
 1361 |          , isEscapeHatch = False
 1362 |          , flags = [Inline]
 1363 |          , refersToM = Nothing
 1364 |          , refersToRuntimeM = Nothing
 1365 |          , invertible = False
 1366 |          , noCycles = False
 1367 |          , linearChecked = True
 1368 |          , definition = Builtin op
 1369 |          , compexpr = Nothing
 1370 |          , namedcompexpr = Nothing
 1371 |          , sizeChange = []
 1372 |          , schemeExpr = Nothing
 1373 |          }
 1374 | 
 1375 | export
 1376 | updateDef : {auto c : Ref Ctxt Defs} ->
 1377 |             Name -> (Def -> Maybe Def) -> Core ()
 1378 | updateDef n fdef
 1379 |     = do defs <- get Ctxt
 1380 |          Just gdef <- lookupCtxtExact n (gamma defs)
 1381 |              | Nothing => pure ()
 1382 |          case fdef (definition gdef) of
 1383 |               Nothing => pure ()
 1384 |               Just def' => ignore $ addDef n ({ definition := def',
 1385 |                                                 schemeExpr := Nothing } gdef)
 1386 | 
 1387 | export
 1388 | updateTy : {auto c : Ref Ctxt Defs} ->
 1389 |            Int -> ClosedTerm -> Core ()
 1390 | updateTy i ty
 1391 |     = do defs <- get Ctxt
 1392 |          Just gdef <- lookupCtxtExact (Resolved i) (gamma defs)
 1393 |               | Nothing => pure ()
 1394 |          ignore $ addDef (Resolved i) ({ type := ty } gdef)
 1395 | 
 1396 | export
 1397 | setCompiled : {auto c : Ref Ctxt Defs} ->
 1398 |               Name -> CDef -> Core ()
 1399 | setCompiled n cexp
 1400 |     = do defs <- get Ctxt
 1401 |          Just gdef <- lookupCtxtExact n (gamma defs)
 1402 |               | Nothing => pure ()
 1403 |          ignore $ addDef n ({ compexpr := Just cexp } gdef)
 1404 | 
 1405 | -- Record that the name has been linearity checked so we don't need to do
 1406 | -- it again
 1407 | export
 1408 | setLinearCheck : {auto c : Ref Ctxt Defs} ->
 1409 |                  Int -> Bool -> Core ()
 1410 | setLinearCheck i chk
 1411 |     = do defs <- get Ctxt
 1412 |          Just gdef <- lookupCtxtExact (Resolved i) (gamma defs)
 1413 |               | Nothing => pure ()
 1414 |          ignore $ addDef (Resolved i) ({ linearChecked := chk } gdef)
 1415 | 
 1416 | export
 1417 | setCtxt : {auto c : Ref Ctxt Defs} -> Context -> Core ()
 1418 | setCtxt gam = update Ctxt { gamma := gam }
 1419 | 
 1420 | export
 1421 | resolveName : {auto c : Ref Ctxt Defs} ->
 1422 |             Name -> Core Int
 1423 | resolveName (Resolved idx) = pure idx
 1424 | resolveName n
 1425 |   = do defs <- get Ctxt
 1426 |        (i, gam') <- getPosition n (gamma defs)
 1427 |        setCtxt gam'
 1428 |        pure i
 1429 | 
 1430 | export
 1431 | addName : {auto c : Ref Ctxt Defs} ->
 1432 |           Name -> Core Int
 1433 | addName (Resolved idx) = pure idx
 1434 | addName n
 1435 |   = do defs <- get Ctxt
 1436 |        (i, gam') <- newEntry n (gamma defs)
 1437 |        setCtxt gam'
 1438 |        pure i
 1439 | 
 1440 | -- Call this before trying alternative elaborations, so that updates to the
 1441 | -- context are put in the staging area rather than writing over the mutable
 1442 | -- array of definitions.
 1443 | -- Returns the old context (the one we'll go back to if the branch fails)
 1444 | export
 1445 | branch : {auto c : Ref Ctxt Defs} ->
 1446 |        Core Defs
 1447 | branch
 1448 |   = do ctxt <- get Ctxt
 1449 |        gam' <- branchCtxt (gamma ctxt)
 1450 |        setCtxt gam'
 1451 |        pure ctxt
 1452 | 
 1453 | -- Call this after trying an elaboration to commit any changes to the mutable
 1454 | -- array of definitions once we know they're correct. Only actually commits
 1455 | -- when we're right back at the top level
 1456 | export
 1457 | commit : {auto c : Ref Ctxt Defs} ->
 1458 |        Core ()
 1459 | commit
 1460 |   = do defs <- get Ctxt
 1461 |        gam' <- commitCtxt (gamma defs)
 1462 |        setCtxt gam'
 1463 | 
 1464 | export
 1465 | depth : {auto c : Ref Ctxt Defs} ->
 1466 |       Core Nat
 1467 | depth
 1468 |   = do defs <- get Ctxt
 1469 |        pure (branchDepth (gamma defs))
 1470 | 
 1471 | export
 1472 | dumpStaging : {auto c : Ref Ctxt Defs} ->
 1473 |               Core ()
 1474 | dumpStaging
 1475 |     = do defs <- get Ctxt
 1476 |          coreLift $ putStrLn $ "Staging area: " ++ show (keys (staging (gamma defs)))
 1477 | 
 1478 | -- Explicitly note that the name should be saved when writing out a .ttc
 1479 | export
 1480 | addToSave : {auto c : Ref Ctxt Defs} ->
 1481 |           Name -> Core ()
 1482 | addToSave n_in
 1483 |   = do defs <- get Ctxt
 1484 |        n <- full (gamma defs) n_in
 1485 |        put Ctxt ({ toSave $= insert n (),
 1486 |                    toIR $= insert n ()
 1487 |                  } defs)
 1488 | 
 1489 | -- Specific lookup functions
 1490 | export
 1491 | lookupExactBy : (GlobalDef -> a) -> Name -> Context ->
 1492 |               Core (Maybe a)
 1493 | lookupExactBy fn n gam
 1494 |   = do Just gdef <- lookupCtxtExact n gam
 1495 |             | Nothing => pure Nothing
 1496 |        pure (Just (fn gdef))
 1497 | 
 1498 | export
 1499 | lookupNameBy : (GlobalDef -> a) -> Name -> Context ->
 1500 |              Core (List (Name, Int, a))
 1501 | lookupNameBy fn n gam
 1502 |   = do gdef <- lookupCtxtName n gam
 1503 |        pure (map (\ (n, i, gd) => (n, i, fn gd)) gdef)
 1504 | 
 1505 | export
 1506 | lookupDefExact : Name -> Context -> Core (Maybe Def)
 1507 | lookupDefExact = lookupExactBy definition
 1508 | 
 1509 | export
 1510 | lookupDefName : Name -> Context -> Core (List (Name, Int, Def))
 1511 | lookupDefName = lookupNameBy definition
 1512 | 
 1513 | export
 1514 | lookupTyExact : Name -> Context -> Core (Maybe ClosedTerm)
 1515 | lookupTyExact = lookupExactBy type
 1516 | 
 1517 | export
 1518 | lookupTyName : Name -> Context -> Core (List (Name, Int, ClosedTerm))
 1519 | lookupTyName = lookupNameBy type
 1520 | 
 1521 | export
 1522 | lookupDefTyExact : Name -> Context -> Core (Maybe (Def, ClosedTerm))
 1523 | lookupDefTyExact = lookupExactBy (\g => (definition g, type g))
 1524 | 
 1525 | -- private names are only visible in this namespace if their namespace
 1526 | -- is the current namespace (or an outer one)
 1527 | -- that is: the namespace of 'n' is a parent of nspace
 1528 | export
 1529 | visibleIn : Namespace -> Name -> Visibility -> Bool
 1530 | visibleIn nspace (NS ns n) Private = isParentOf ns nspace
 1531 | -- Public and Export names are always visible
 1532 | visibleIn nspace n _ = True
 1533 | 
 1534 | export
 1535 | visibleInAny : List Namespace -> Name -> Visibility -> Bool
 1536 | visibleInAny nss n vis = any (\ns => visibleIn ns n vis) nss
 1537 | 
 1538 | reducibleIn : Namespace -> Name -> Visibility -> Bool
 1539 | reducibleIn nspace (NS ns (UN n)) Export = isParentOf ns nspace
 1540 | reducibleIn nspace (NS ns (UN n)) Private = isParentOf ns nspace
 1541 | reducibleIn nspace n _ = True
 1542 | 
 1543 | export
 1544 | reducibleInAny : List Namespace -> Name -> Visibility -> Bool
 1545 | reducibleInAny nss n vis = any (\ns => reducibleIn ns n vis) nss
 1546 | 
 1547 | export
 1548 | toFullNames : {auto c : Ref Ctxt Defs} ->
 1549 |               HasNames a => a -> Core a
 1550 | toFullNames t
 1551 |     = do defs <- get Ctxt
 1552 |          full (gamma defs) t
 1553 | 
 1554 | export
 1555 | toResolvedNames : {auto c : Ref Ctxt Defs} ->
 1556 |                   HasNames a => a -> Core a
 1557 | toResolvedNames t
 1558 |     = do defs <- get Ctxt
 1559 |          resolved (gamma defs) t
 1560 | 
 1561 | -- Make the name look nicer for user display
 1562 | export
 1563 | prettyName : {auto c : Ref Ctxt Defs} ->
 1564 |              Name -> Core String
 1565 | prettyName (Nested (i, _) n)
 1566 |     = do i' <- toFullNames (Resolved i)
 1567 |          pure (!(prettyName i') ++ "," ++
 1568 |                !(prettyName n))
 1569 | prettyName (CaseBlock outer idx)
 1570 |     = pure ("case block in " ++ outer)
 1571 | prettyName (WithBlock outer idx)
 1572 |     = pure ("with block in " ++ outer)
 1573 | prettyName (NS ns n) = prettyName n
 1574 | prettyName n = pure (show n)
 1575 | 
 1576 | -- Add a hash of a thing that contains names,
 1577 | -- but convert the internal numbers to full names first.
 1578 | -- This makes the hash not depend on the internal numbering,
 1579 | -- which is unstable.
 1580 | export
 1581 | addHashWithNames : {auto c : Ref Ctxt Defs} ->
 1582 |   Hashable a => HasNames a => a -> Core ()
 1583 | addHashWithNames x = toFullNames x >>= addHash
 1584 | 
 1585 | export
 1586 | setIsEscapeHatch : {auto c : Ref Ctxt Defs} ->
 1587 |   FC -> Name -> Core ()
 1588 | setIsEscapeHatch fc n
 1589 |     = do defs <- get Ctxt
 1590 |          Just def <- lookupCtxtExact n (gamma defs)
 1591 |               | Nothing => undefinedName fc n
 1592 |          ignore $ addDef n ({ isEscapeHatch := True } def)
 1593 | 
 1594 | export
 1595 | setFlag : {auto c : Ref Ctxt Defs} ->
 1596 |         FC -> Name -> DefFlag -> Core ()
 1597 | setFlag fc n fl
 1598 |     = do defs <- get Ctxt
 1599 |          Just def <- lookupCtxtExact n (gamma defs)
 1600 |               | Nothing => undefinedName fc n
 1601 |          let flags' = fl :: filter (/= fl) (flags def)
 1602 |          ignore $ addDef n ({ flags := flags' } def)
 1603 | 
 1604 | export
 1605 | setNameFlag : {auto c : Ref Ctxt Defs} ->
 1606 |               FC -> Name -> DefFlag -> Core ()
 1607 | setNameFlag fc n fl
 1608 |     = do defs <- get Ctxt
 1609 |          [(n', i, def)] <- lookupCtxtName n (gamma defs)
 1610 |               | res => ambiguousName fc n (map fst res)
 1611 |          let flags' = fl :: filter (/= fl) (flags def)
 1612 |          ignore $ addDef (Resolved i) ({ flags := flags' } def)
 1613 | 
 1614 | export
 1615 | unsetFlag : {auto c : Ref Ctxt Defs} ->
 1616 |             FC -> Name -> DefFlag -> Core ()
 1617 | unsetFlag fc n fl
 1618 |     = do defs <- get Ctxt
 1619 |          Just def <- lookupCtxtExact n (gamma defs)
 1620 |               | Nothing => undefinedName fc n
 1621 |          let flags' = filter (/= fl) (flags def)
 1622 |          ignore $ addDef n ({ flags := flags' } def)
 1623 | 
 1624 | export
 1625 | hasFlag : {auto c : Ref Ctxt Defs} ->
 1626 |           FC -> Name -> DefFlag -> Core Bool
 1627 | hasFlag fc n fl
 1628 |     = do defs <- get Ctxt
 1629 |          Just def <- lookupCtxtExact n (gamma defs)
 1630 |               | Nothing => undefinedName fc n
 1631 |          pure (fl `elem` flags def)
 1632 | 
 1633 | export
 1634 | hasSetTotal : {auto c : Ref Ctxt Defs} -> FC -> Name -> Core Bool
 1635 | hasSetTotal fc n
 1636 |     = do defs <- get Ctxt
 1637 |          Just def <- lookupCtxtExact n (gamma defs)
 1638 |              | Nothing => undefinedName fc n
 1639 |          pure $ isJust $ findSetTotal def.flags
 1640 | 
 1641 | export
 1642 | setSizeChange : {auto c : Ref Ctxt Defs} ->
 1643 |                 FC -> Name -> List SCCall -> Core ()
 1644 | setSizeChange loc n sc
 1645 |     = do defs <- get Ctxt
 1646 |          Just def <- lookupCtxtExact n (gamma defs)
 1647 |               | Nothing => undefinedName loc n
 1648 |          ignore $ addDef n ({ sizeChange := sc } def)
 1649 | 
 1650 | export
 1651 | setTotality : {auto c : Ref Ctxt Defs} ->
 1652 |               FC -> Name -> Totality -> Core ()
 1653 | setTotality loc n tot
 1654 |     = do defs <- get Ctxt
 1655 |          Just def <- lookupCtxtExact n (gamma defs)
 1656 |               | Nothing => undefinedName loc n
 1657 |          ignore $ addDef n ({ totality := tot } def)
 1658 | 
 1659 | export
 1660 | setCovering : {auto c : Ref Ctxt Defs} ->
 1661 |               FC -> Name -> Covering -> Core ()
 1662 | setCovering loc n tot
 1663 |     = do defs <- get Ctxt
 1664 |          Just def <- lookupCtxtExact n (gamma defs)
 1665 |               | Nothing => undefinedName loc n
 1666 |          ignore $ addDef n ({ totality->isCovering := tot } def)
 1667 | 
 1668 | export
 1669 | setTerminating : {auto c : Ref Ctxt Defs} ->
 1670 |                  FC -> Name -> Terminating -> Core ()
 1671 | setTerminating loc n tot
 1672 |     = do defs <- get Ctxt
 1673 |          Just def <- lookupCtxtExact n (gamma defs)
 1674 |               | Nothing => undefinedName loc n
 1675 |          ignore $ addDef n ({ totality->isTerminating := tot } def)
 1676 | 
 1677 | export
 1678 | getTotality : {auto c : Ref Ctxt Defs} ->
 1679 |               FC -> Name -> Core Totality
 1680 | getTotality loc n
 1681 |     = do defs <- get Ctxt
 1682 |          Just def <- lookupCtxtExact n (gamma defs)
 1683 |               | Nothing => undefinedName loc n
 1684 |          pure $ totality def
 1685 | 
 1686 | export
 1687 | getSizeChange : {auto c : Ref Ctxt Defs} ->
 1688 |                 FC -> Name -> Core (List SCCall)
 1689 | getSizeChange loc n
 1690 |     = do defs <- get Ctxt
 1691 |          Just def <- lookupCtxtExact n (gamma defs)
 1692 |               | Nothing => undefinedName loc n
 1693 |          pure $ sizeChange def
 1694 | 
 1695 | export
 1696 | setVisibility : {auto c : Ref Ctxt Defs} ->
 1697 |                 FC -> Name -> Visibility -> Core ()
 1698 | setVisibility fc n vis
 1699 |     = do defs <- get Ctxt
 1700 |          Just def <- lookupCtxtExact n (gamma defs)
 1701 |               | Nothing => undefinedName fc n
 1702 |          ignore $ addDef n ({ visibility := specified vis } def)
 1703 | 
 1704 | export
 1705 | withDefStacked : {auto c : Ref Ctxt Defs} ->
 1706 |                  Name -> Core a -> Core a
 1707 | withDefStacked n act
 1708 |     = do defs <- get Ctxt
 1709 |          let ds = defs.defsStack
 1710 |          put Ctxt $ {defsStack $= (:< n)} defs
 1711 |          act <* update Ctxt {defsStack := ds}
 1712 | 
 1713 | public export
 1714 | record SearchData where
 1715 |   constructor MkSearchData
 1716 |   ||| determining argument positions
 1717 |   detArgs : NatSet
 1718 |   ||| Name of functions to use as hints, and whether ambiguity is allowed
 1719 |   |||
 1720 |   ||| In proof search, for every group of names
 1721 |   |||  * If exactly one succeeds, use it
 1722 |   |||  * If more than one succeeds, report an ambiguity error
 1723 |   |||  * If none succeed, move on to the next group
 1724 |   |||
 1725 |   ||| This allows us to prioritise some names (e.g. to declare 'open' hints,
 1726 |   ||| which we might us to open an implementation working as a module, or to
 1727 |   ||| declare a named implementation to be used globally), and to have names
 1728 |   ||| which are only used if all else fails (e.g. as a defaulting mechanism),
 1729 |   ||| while the proof search mechanism doesn't need to know about any of the
 1730 |   ||| details.
 1731 |   hintGroups : List (Bool, List Name)
 1732 | 
 1733 | ||| Get the auto search data for a name.
 1734 | export
 1735 | getSearchData : {auto c : Ref Ctxt Defs} ->
 1736 |                 FC -> (defaults : Bool) -> Name ->
 1737 |                 Core SearchData
 1738 | getSearchData fc defaults target
 1739 |     = do defs <- get Ctxt
 1740 |          Just (TCon _ _ dets u _ _ _) <- lookupDefExact target (gamma defs)
 1741 |               | _ => undefinedName fc target
 1742 |          hs <- case lookup !(toFullNames target) (typeHints defs) of
 1743 |                        Just hs => filterM (\x => notHidden x (gamma defs)) hs
 1744 |                        Nothing => pure []
 1745 |          if defaults
 1746 |             then let defns = map fst !(filterM (\x => pure $ isDefault x
 1747 |                                                  && !(notHidden x (gamma defs)))
 1748 |                                              (toList (autoHints defs))) in
 1749 |                      pure (MkSearchData NatSet.empty [(False, defns)])
 1750 |             else let opens = map fst !(filterM (\x => notHidden x (gamma defs))
 1751 |                                              (toList (openHints defs)))
 1752 |                      autos = map fst !(filterM (\x => pure $ not (isDefault x)
 1753 |                                                  && !(notHidden x (gamma defs)))
 1754 |                                              (toList (autoHints defs)))
 1755 |                      tyhs = map fst (filter direct hs)
 1756 |                      chasers = map fst (filter (not . direct) hs) in
 1757 |                      pure (MkSearchData dets (filter (isCons . snd)
 1758 |                                [(False, opens),
 1759 |                                 (False, autos),
 1760 |                                 (not (uniqueAuto u), tyhs),
 1761 |                                 (True, chasers)]))
 1762 |   where
 1763 |     ||| We don't want hidden (by `%hide`) names to appear in the search.
 1764 |     ||| Lookup has to be done by a full qualified name, not a resolved ID.
 1765 |     notHidden : forall a. (Name, a) -> Context -> Core Bool
 1766 |     notHidden (n, _) ctxt = do
 1767 |       fulln <- toFullNames n
 1768 |       pure $ not (isHidden fulln ctxt)
 1769 | 
 1770 |     isDefault : (Name, Bool) -> Bool
 1771 |     isDefault = snd
 1772 | 
 1773 |     direct : (Name, Bool) -> Bool
 1774 |     direct = snd
 1775 | 
 1776 | export
 1777 | setMutWith : {auto c : Ref Ctxt Defs} ->
 1778 |              FC -> Name -> List Name -> Core ()
 1779 | setMutWith fc tn tns
 1780 |     = do defs <- get Ctxt
 1781 |          Just g <- lookupCtxtExact tn (gamma defs)
 1782 |               | _ => undefinedName fc tn
 1783 |          let TCon a ps dets u _ cons det = definition g
 1784 |               | _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor [setMutWith]"))
 1785 |          updateDef tn (const (Just (TCon a ps dets u tns cons det)))
 1786 | 
 1787 | export
 1788 | addMutData : {auto c : Ref Ctxt Defs} ->
 1789 |              Name -> Core ()
 1790 | addMutData n = update Ctxt { mutData $= (n ::) }
 1791 | 
 1792 | export
 1793 | dropMutData : {auto c : Ref Ctxt Defs} ->
 1794 |               Name -> Core ()
 1795 | dropMutData n = update Ctxt { mutData $= filter (/= n) }
 1796 | 
 1797 | export
 1798 | setDetermining : {auto c : Ref Ctxt Defs} ->
 1799 |                  FC -> Name -> List1 Name -> Core ()
 1800 | setDetermining fc tyn args
 1801 |     = do defs <- get Ctxt
 1802 |          Just g <- lookupCtxtExact tyn (gamma defs)
 1803 |               | _ => undefinedName fc tyn
 1804 |          let TCon a ps _ u cons ms det = definition g
 1805 |               | _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor [setDetermining]"))
 1806 |          apos <- getPos 0 (forget args) (type g)
 1807 |          updateDef tyn (const (Just (TCon a ps apos u cons ms det)))
 1808 |   where
 1809 |     -- Type isn't normalised, but the argument names refer to those given
 1810 |     -- explicitly in the type, so there's no need.
 1811 |     getPos : Nat -> List Name -> Term vs -> Core NatSet
 1812 |     getPos i ns (Bind _ x (Pi {}) sc)
 1813 |         = if x `elem` ns
 1814 |              then do rest <- getPos (1 + i) (filter (/=x) ns) sc
 1815 |                      pure $ insert i rest
 1816 |              else getPos (1 + i) ns sc
 1817 |     getPos _ [] _ = pure NatSet.empty
 1818 |     getPos _ ns ty = throw (GenericMsg fc ("Unknown determining arguments: "
 1819 |                            ++ showSep ", " (map show ns)))
 1820 | 
 1821 | export
 1822 | setDetags : {auto c : Ref Ctxt Defs} ->
 1823 |             FC -> Name -> Maybe NatSet -> Core ()
 1824 | setDetags fc tyn args
 1825 |     = do defs <- get Ctxt
 1826 |          Just g <- lookupCtxtExact tyn (gamma defs)
 1827 |               | _ => undefinedName fc tyn
 1828 |          let TCon a ps det u cons ms _ = definition g
 1829 |               | _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor [setDetermining]"))
 1830 |          updateDef tyn (const (Just (TCon a ps det u cons ms args)))
 1831 | 
 1832 | export
 1833 | setUniqueSearch : {auto c : Ref Ctxt Defs} ->
 1834 |                   FC -> Name -> Bool -> Core ()
 1835 | setUniqueSearch fc tyn u
 1836 |     = do defs <- get Ctxt
 1837 |          Just g <- lookupCtxtExact tyn (gamma defs)
 1838 |               | _ => undefinedName fc tyn
 1839 |          let TCon a ps ds fl cons ms det = definition g
 1840 |               | _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor [setDetermining]"))
 1841 |          let fl' = { uniqueAuto := u } fl
 1842 |          updateDef tyn (const (Just (TCon a ps ds fl' cons ms det)))
 1843 | 
 1844 | export
 1845 | setExternal : {auto c : Ref Ctxt Defs} ->
 1846 |               FC -> Name -> Bool -> Core ()
 1847 | setExternal fc tyn u
 1848 |     = do defs <- get Ctxt
 1849 |          Just g <- lookupCtxtExact tyn (gamma defs)
 1850 |               | _ => undefinedName fc tyn
 1851 |          let TCon a ps ds fl cons ms det = definition g
 1852 |               | _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor [setDetermining]"))
 1853 |          let fl' = { external := u } fl
 1854 |          updateDef tyn (const (Just (TCon a ps ds fl' cons ms det)))
 1855 | 
 1856 | export
 1857 | addHintFor : {auto c : Ref Ctxt Defs} ->
 1858 |              FC -> Name -> Name -> Bool -> Bool -> Core ()
 1859 | addHintFor fc tyn_in hintn_in direct loading
 1860 |     = do defs <- get Ctxt
 1861 |          tyn <- toFullNames tyn_in
 1862 |           -- ^ We have to index by full name because of the order we load -
 1863 |           -- the name may not be resolved yet when we load the hints.
 1864 |           -- Revisit if this turns out to be a bottleneck (it seems unlikely)
 1865 |          hintn <- toResolvedNames hintn_in
 1866 | 
 1867 |          let hs = case lookup tyn (typeHints defs) of
 1868 |                        Just hs => hs
 1869 |                        Nothing => []
 1870 |          if loading
 1871 |             then put Ctxt
 1872 |                      ({ typeHints $= insert tyn ((hintn, direct) :: hs)
 1873 |                       } defs)
 1874 |             else put Ctxt
 1875 |                      ({ typeHints $= insert tyn ((hintn, direct) :: hs),
 1876 |                         saveTypeHints $= ((tyn, hintn, direct) :: )
 1877 |                       } defs)
 1878 | 
 1879 | export
 1880 | addGlobalHint : {auto c : Ref Ctxt Defs} ->
 1881 |                 Name -> Bool -> Core ()
 1882 | addGlobalHint hintn_in isdef
 1883 |     = do hintn <- toResolvedNames hintn_in
 1884 |          update Ctxt { autoHints $= insert hintn isdef,
 1885 |                        saveAutoHints $= ((hintn, isdef) ::) }
 1886 | 
 1887 | export
 1888 | addLocalHint : {auto c : Ref Ctxt Defs} ->
 1889 |                Name -> Core ()
 1890 | addLocalHint hintn_in
 1891 |     = do hintn <- toResolvedNames hintn_in
 1892 |          update Ctxt { localHints $= insert hintn () }
 1893 | 
 1894 | export
 1895 | addOpenHint : {auto c : Ref Ctxt Defs} -> Name -> Core ()
 1896 | addOpenHint hintn_in
 1897 |     = do hintn <- toResolvedNames hintn_in
 1898 |          update Ctxt { openHints $= insert hintn () }
 1899 | 
 1900 | export
 1901 | dropOpenHint : {auto c : Ref Ctxt Defs} -> Name -> Core ()
 1902 | dropOpenHint hintn_in
 1903 |     = do hintn <- toResolvedNames hintn_in
 1904 |          update Ctxt { openHints $= delete hintn }
 1905 | 
 1906 | export
 1907 | setOpenHints : {auto c : Ref Ctxt Defs} -> NameMap () -> Core ()
 1908 | setOpenHints hs = update Ctxt { openHints := hs }
 1909 | 
 1910 | export
 1911 | addTransform : {auto c : Ref Ctxt Defs} ->
 1912 |                FC -> Transform -> Core ()
 1913 | addTransform fc t_in
 1914 |     = do defs <- get Ctxt
 1915 |          let Just fn_in = getFnName t_in
 1916 |              | Nothing =>
 1917 |                   throw (GenericMsg fc "LHS of a transformation must be a function application")
 1918 |          fn <- toResolvedNames fn_in
 1919 |          t <- toResolvedNames t_in
 1920 |          fn_full <- toFullNames fn_in
 1921 |          t_full <- toFullNames t_in
 1922 |          case lookup fn (transforms defs) of
 1923 |               Nothing =>
 1924 |                  put Ctxt ({ transforms $= insert fn [t],
 1925 |                              saveTransforms $= ((fn_full, t_full) ::) } defs)
 1926 |               Just ts =>
 1927 |                  put Ctxt ({ transforms $= insert fn (t :: ts),
 1928 |                              saveTransforms $= ((fn_full, t_full) ::) } defs)
 1929 | 
 1930 | export
 1931 | clearSavedHints : {auto c : Ref Ctxt Defs} -> Core ()
 1932 | clearSavedHints = update Ctxt { saveTypeHints := [], saveAutoHints := [] }
 1933 | 
 1934 | -- Set the default namespace for new definitions
 1935 | export
 1936 | setNS : {auto c : Ref Ctxt Defs} -> Namespace -> Core ()
 1937 | setNS ns = update Ctxt { currentNS := ns }
 1938 | 
 1939 | -- Set the nested namespaces we're allowed to look inside
 1940 | export
 1941 | setNestedNS : {auto c : Ref Ctxt Defs} ->
 1942 |               List Namespace -> Core ()
 1943 | setNestedNS ns = update Ctxt { nestedNS := ns }
 1944 | 
 1945 | -- Get the default namespace for new definitions
 1946 | export
 1947 | getNS : {auto c : Ref Ctxt Defs} ->
 1948 |         Core Namespace
 1949 | getNS
 1950 |     = do defs <- get Ctxt
 1951 |          pure (currentNS defs)
 1952 | 
 1953 | -- Get the nested namespaces we're allowed to look inside
 1954 | export
 1955 | getNestedNS : {auto c : Ref Ctxt Defs} ->
 1956 |               Core (List Namespace)
 1957 | getNestedNS
 1958 |     = do defs <- get Ctxt
 1959 |          pure (nestedNS defs)
 1960 | 
 1961 | -- Add the module name, and namespace, of an imported module
 1962 | -- (i.e. for "import X as Y", it's (X, Y)
 1963 | -- "import public X" is, when rexported, the same as
 1964 | -- "import X as [current namespace]")
 1965 | export
 1966 | addImported : {auto c : Ref Ctxt Defs} ->
 1967 |               (ModuleIdent, Bool, Namespace) -> Core ()
 1968 | addImported mod = update Ctxt { imported $= (mod ::) }
 1969 | 
 1970 | export
 1971 | getImported : {auto c : Ref Ctxt Defs} ->
 1972 |               Core (List (ModuleIdent, Bool, Namespace))
 1973 | getImported
 1974 |     = do defs <- get Ctxt
 1975 |          pure (imported defs)
 1976 | 
 1977 | export
 1978 | addDirective : {auto c : Ref Ctxt Defs} ->
 1979 |                String -> String -> Core ()
 1980 | addDirective c str
 1981 |     = do defs <- get Ctxt
 1982 |          case getCG (options defs) c of
 1983 |               Nothing => -- warn, rather than fail, because the CG may exist
 1984 |                          -- but be unknown to this particular instance
 1985 |                          coreLift $ putStrLn $ "Unknown code generator " ++ c
 1986 |               Just cg => put Ctxt ({ cgdirectives $= ((cg, str) ::) } defs)
 1987 | 
 1988 | export
 1989 | getDirectives : {auto c : Ref Ctxt Defs} ->
 1990 |                 CG -> Core (List String)
 1991 | getDirectives cg
 1992 |     = do defs <- get Ctxt
 1993 |          pure $ defs.options.session.directives ++
 1994 |                  mapMaybe getDir (cgdirectives defs)
 1995 |   where
 1996 |     getDir : (CG, String) -> Maybe String
 1997 |     getDir (x', str) = if cg == x' then Just str else Nothing
 1998 | 
 1999 | -- Add a new nested namespace to the current namespace for new definitions
 2000 | -- e.g. extendNS ["Data"] when namespace is "Prelude.List" leads to
 2001 | -- current namespace of "Prelude.List.Data"
 2002 | -- Inner namespaces go first, for ease of name lookup
 2003 | export
 2004 | extendNS : {auto c : Ref Ctxt Defs} -> Namespace -> Core ()
 2005 | extendNS ns = update Ctxt { currentNS $= (<.> ns) }
 2006 | 
 2007 | export
 2008 | withExtendedNS : {auto c : Ref Ctxt Defs} ->
 2009 |                  Namespace -> Core a -> Core a
 2010 | withExtendedNS ns act
 2011 |     = do defs <- get Ctxt
 2012 |          let cns = currentNS defs
 2013 |          put Ctxt ({ currentNS := cns <.> ns } defs)
 2014 |          ma <- catch (Right <$> act) (pure . Left)
 2015 |          defs <- get Ctxt
 2016 |          put Ctxt ({ currentNS := cns } defs)
 2017 |          case ma of
 2018 |            Left err => throw err
 2019 |            Right a  => pure a
 2020 | 
 2021 | -- Get the name as it would be defined in the current namespace
 2022 | -- i.e. if it doesn't have an explicit namespace already, add it,
 2023 | -- otherwise leave it alone
 2024 | export
 2025 | inCurrentNS : {auto c : Ref Ctxt Defs} ->
 2026 |               Name -> Core Name
 2027 | inCurrentNS (UN n)
 2028 |     = do defs <- get Ctxt
 2029 |          pure (NS (currentNS defs) (UN n))
 2030 | inCurrentNS n@(CaseBlock {})
 2031 |     = do defs <- get Ctxt
 2032 |          pure (NS (currentNS defs) n)
 2033 | inCurrentNS n@(WithBlock {})
 2034 |     = do defs <- get Ctxt
 2035 |          pure (NS (currentNS defs) n)
 2036 | inCurrentNS n@(Nested {})
 2037 |     = do defs <- get Ctxt
 2038 |          pure (NS (currentNS defs) n)
 2039 | inCurrentNS n@(MN {})
 2040 |     = do defs <- get Ctxt
 2041 |          pure (NS (currentNS defs) n)
 2042 | inCurrentNS n@(DN {})
 2043 |     = do defs <- get Ctxt
 2044 |          pure (NS (currentNS defs) n)
 2045 | inCurrentNS n = pure n
 2046 | 
 2047 | export
 2048 | setVisible : {auto c : Ref Ctxt Defs} ->
 2049 |              Namespace -> Core ()
 2050 | setVisible nspace = update Ctxt { gamma->visibleNS $= (nspace ::) }
 2051 | 
 2052 | export
 2053 | getVisible : {auto c : Ref Ctxt Defs} ->
 2054 |              Core (List Namespace)
 2055 | getVisible
 2056 |     = do defs <- get Ctxt
 2057 |          pure (visibleNS (gamma defs))
 2058 | 
 2059 | -- set whether all names should be viewed as public. Be careful with this,
 2060 | -- it's not intended for when checking user code! It's meant for allowing
 2061 | -- easy checking of partially evaluated definitions.
 2062 | export
 2063 | setAllPublic : {auto c : Ref Ctxt Defs} ->
 2064 |                (pub : Bool) -> Core ()
 2065 | setAllPublic pub = update Ctxt { gamma->allPublic := pub }
 2066 | 
 2067 | export
 2068 | isAllPublic : {auto c : Ref Ctxt Defs} ->
 2069 |               Core Bool
 2070 | isAllPublic
 2071 |     = do defs <- get Ctxt
 2072 |          pure (allPublic (gamma defs))
 2073 | 
 2074 | -- Return True if the given namespace is visible in the context (meaning
 2075 | -- the namespace itself, and any namespace it's nested inside)
 2076 | export
 2077 | isVisible : {auto c : Ref Ctxt Defs} ->
 2078 |             Namespace -> Core Bool
 2079 | isVisible nspace
 2080 |     = do defs <- get Ctxt
 2081 |          pure (any visible (allParents (currentNS defs) ++
 2082 |                             nestedNS defs ++
 2083 |                             visibleNS (gamma defs)))
 2084 | 
 2085 |   where
 2086 |     -- Visible if any visible namespace is a parent of the namespace we're
 2087 |     -- asking about
 2088 |     visible : Namespace -> Bool
 2089 |     visible visns = isParentOf visns nspace
 2090 | 
 2091 | -- Get the next entry id in the context (this is for recording where to go
 2092 | -- back to when backtracking in the elaborator)
 2093 | export
 2094 | getNextEntry : {auto c : Ref Ctxt Defs} ->
 2095 |                Core Int
 2096 | getNextEntry
 2097 |     = do defs <- get Ctxt
 2098 |          pure (nextEntry (gamma defs))
 2099 | 
 2100 | export
 2101 | setNextEntry : {auto c : Ref Ctxt Defs} ->
 2102 |                Int -> Core ()
 2103 | setNextEntry i = update Ctxt { gamma->nextEntry := i }
 2104 | 
 2105 | -- Set the 'first entry' index (i.e. the first entry in the current file)
 2106 | -- to the place we currently are in the context
 2107 | export
 2108 | resetFirstEntry : {auto c : Ref Ctxt Defs} ->
 2109 |                   Core ()
 2110 | resetFirstEntry
 2111 |     = do defs <- get Ctxt
 2112 |          put Ctxt ({ gamma->firstEntry := nextEntry (gamma defs) } defs)
 2113 | 
 2114 | export
 2115 | getFullName : {auto c : Ref Ctxt Defs} ->
 2116 |               Name -> Core Name
 2117 | getFullName (Resolved i)
 2118 |     = do defs <- get Ctxt
 2119 |          Just gdef <- lookupCtxtExact (Resolved i) (gamma defs)
 2120 |               | Nothing => pure (Resolved i)
 2121 |          pure (fullname gdef)
 2122 | getFullName n = pure n
 2123 | 
 2124 | -- Getting and setting various options
 2125 | 
 2126 | export
 2127 | getPPrint : {auto c : Ref Ctxt Defs} ->
 2128 |             Core PPrinter
 2129 | getPPrint
 2130 |     = do defs <- get Ctxt
 2131 |          pure (printing (options defs))
 2132 | 
 2133 | export
 2134 | setPPrint : {auto c : Ref Ctxt Defs} -> PPrinter -> Core ()
 2135 | setPPrint ppopts = update Ctxt { options->printing := ppopts }
 2136 | 
 2137 | export
 2138 | updatePPrint : {auto c : Ref Ctxt Defs} -> (PPrinter -> PPrinter) -> Core ()
 2139 | updatePPrint f = update Ctxt { options->printing $= f }
 2140 | 
 2141 | export
 2142 | setCG : {auto c : Ref Ctxt Defs} -> CG -> Core ()
 2143 | setCG cg = update Ctxt { options->session->codegen := cg }
 2144 | 
 2145 | export
 2146 | getDirs : {auto c : Ref Ctxt Defs} -> Core Dirs
 2147 | getDirs
 2148 |     = do defs <- get Ctxt
 2149 |          pure (dirs (options defs))
 2150 | 
 2151 | export
 2152 | addExtraDir : {auto c : Ref Ctxt Defs} -> String -> Core ()
 2153 | addExtraDir dir = update Ctxt { options->dirs->extra_dirs $= ((::) dir) . filter (/= dir) }
 2154 | 
 2155 | export
 2156 | addPackageDir: {auto c : Ref Ctxt Defs} -> String -> Core ()
 2157 | addPackageDir dir = update Ctxt { options->dirs->package_dirs $= ((::) dir) . filter (/= dir) }
 2158 | 
 2159 | export
 2160 | addPackageSearchPath: {auto c : Ref Ctxt Defs} -> String -> Core ()
 2161 | addPackageSearchPath dir =
 2162 |   let newPath = parse dir
 2163 |    in update Ctxt { options->dirs->package_search_paths $= ((::) newPath) . filter (/= newPath) }
 2164 | 
 2165 | export
 2166 | addDataDir : {auto c : Ref Ctxt Defs} -> String -> Core ()
 2167 | addDataDir dir = update Ctxt { options->dirs->data_dirs $= (++ [dir]) }
 2168 | 
 2169 | export
 2170 | addLibDir : {auto c : Ref Ctxt Defs} -> String -> Core ()
 2171 | addLibDir dir = update Ctxt { options->dirs->lib_dirs $= (++ [dir]) }
 2172 | 
 2173 | export
 2174 | setBuildDir : {auto c : Ref Ctxt Defs} -> String -> Core ()
 2175 | setBuildDir dir = update Ctxt { options->dirs->build_dir := dir }
 2176 | 
 2177 | export
 2178 | setDependsDir : {auto c : Ref Ctxt Defs} -> String -> Core ()
 2179 | setDependsDir dir = update Ctxt { options->dirs->depends_dir := dir }
 2180 | 
 2181 | export
 2182 | setOutputDir : {auto c : Ref Ctxt Defs} -> Maybe String -> Core ()
 2183 | setOutputDir dir = update Ctxt { options->dirs->output_dir := dir }
 2184 | 
 2185 | export
 2186 | setSourceDir : {auto c : Ref Ctxt Defs} -> Maybe String -> Core ()
 2187 | setSourceDir mdir = update Ctxt { options->dirs->source_dir := mdir }
 2188 | 
 2189 | export
 2190 | setWorkingDir : {auto c : Ref Ctxt Defs} -> String -> Core ()
 2191 | setWorkingDir dir
 2192 |     = do coreLift_ $ changeDir dir
 2193 |          Just cdir <- coreLift $ currentDir
 2194 |               | Nothing => throw (InternalError "Can't get current directory")
 2195 |          update Ctxt { options->dirs->working_dir := cdir }
 2196 | 
 2197 | export
 2198 | getWorkingDir : Core String
 2199 | getWorkingDir
 2200 |     = do Just d <- coreLift $ currentDir
 2201 |               | Nothing => throw (InternalError "Can't get current directory")
 2202 |          pure d
 2203 | 
 2204 | export
 2205 | setExtraDirs : {auto c : Ref Ctxt Defs} -> List String -> Core ()
 2206 | setExtraDirs dirs = update Ctxt { options->dirs->extra_dirs := dirs }
 2207 | 
 2208 | export
 2209 | setPackageDirs : {auto c : Ref Ctxt Defs} -> List String -> Core ()
 2210 | setPackageDirs dirs = update Ctxt { options->dirs->package_dirs := dirs }
 2211 | 
 2212 | export
 2213 | withCtxt : {auto c : Ref Ctxt Defs} -> Core a -> Core a
 2214 | withCtxt = wrapRef Ctxt resetCtxt
 2215 |   where
 2216 |     resetCtxt : Defs -> Core ()
 2217 |     resetCtxt defs = do let dir = defs.options.dirs.working_dir
 2218 |                         coreLift_ $ changeDir dir
 2219 | 
 2220 | export
 2221 | setPrefix : {auto c : Ref Ctxt Defs} -> String -> Core ()
 2222 | setPrefix dir = update Ctxt { options->dirs->prefix_dir := dir }
 2223 | 
 2224 | export
 2225 | setExtension : {auto c : Ref Ctxt Defs} -> LangExt -> Core ()
 2226 | setExtension e = update Ctxt { options $= setExtension e }
 2227 | 
 2228 | export
 2229 | isExtension : LangExt -> Defs -> Bool
 2230 | isExtension e defs = isExtension e (options defs)
 2231 | 
 2232 | export
 2233 | checkUnambig : {auto c : Ref Ctxt Defs} ->
 2234 |                FC -> Name -> Core Name
 2235 | checkUnambig fc n
 2236 |     = do defs <- get Ctxt
 2237 |          case !(lookupDefName n (gamma defs)) of
 2238 |               [(fulln, i, _)] => pure (Resolved i)
 2239 |               ns => ambiguousName fc n (map fst ns)
 2240 | 
 2241 | export
 2242 | lazyActive : {auto c : Ref Ctxt Defs} -> Bool -> Core ()
 2243 | lazyActive a = update Ctxt { options->elabDirectives->lazyActive := a }
 2244 | 
 2245 | export
 2246 | setUnboundImplicits : {auto c : Ref Ctxt Defs} -> Bool -> Core ()
 2247 | setUnboundImplicits a = update Ctxt { options->elabDirectives->unboundImplicits := a }
 2248 | 
 2249 | export
 2250 | setPrefixRecordProjections : {auto c : Ref Ctxt Defs} -> Bool -> Core ()
 2251 | setPrefixRecordProjections b = update Ctxt { options->elabDirectives->prefixRecordProjections := b }
 2252 | 
 2253 | export
 2254 | setDefaultTotalityOption : {auto c : Ref Ctxt Defs} ->
 2255 |                            TotalReq -> Core ()
 2256 | setDefaultTotalityOption tot = update Ctxt { options->elabDirectives->totality := tot }
 2257 | 
 2258 | export
 2259 | setAmbigLimit : {auto c : Ref Ctxt Defs} ->
 2260 |                 Nat -> Core ()
 2261 | setAmbigLimit max = update Ctxt { options->elabDirectives->ambigLimit := max }
 2262 | 
 2263 | export
 2264 | setTotalLimit : {auto c : Ref Ctxt Defs} ->
 2265 |                 Nat -> Core ()
 2266 | setTotalLimit max = update Ctxt { options->elabDirectives->totalLimit := max }
 2267 | 
 2268 | export
 2269 | setAutoImplicitLimit : {auto c : Ref Ctxt Defs} ->
 2270 |                        Nat -> Core ()
 2271 | setAutoImplicitLimit max = update Ctxt { options->elabDirectives->autoImplicitLimit := max }
 2272 | 
 2273 | export
 2274 | setNFThreshold : {auto c : Ref Ctxt Defs} ->
 2275 |                  Nat -> Core ()
 2276 | setNFThreshold max = update Ctxt { options->elabDirectives->nfThreshold := max }
 2277 | 
 2278 | export
 2279 | setSearchTimeout : {auto c : Ref Ctxt Defs} ->
 2280 |                    Integer -> Core ()
 2281 | setSearchTimeout t = update Ctxt { options->session->searchTimeout := t }
 2282 | 
 2283 | export
 2284 | isLazyActive : {auto c : Ref Ctxt Defs} ->
 2285 |                Core Bool
 2286 | isLazyActive
 2287 |     = do defs <- get Ctxt
 2288 |          pure (lazyActive (elabDirectives (options defs)))
 2289 | 
 2290 | export
 2291 | isUnboundImplicits : {auto c : Ref Ctxt Defs} ->
 2292 |                   Core Bool
 2293 | isUnboundImplicits
 2294 |     = do defs <- get Ctxt
 2295 |          pure (unboundImplicits (elabDirectives (options defs)))
 2296 | 
 2297 | export
 2298 | isPrefixRecordProjections : {auto c : Ref Ctxt Defs} -> Core Bool
 2299 | isPrefixRecordProjections =
 2300 |   prefixRecordProjections . elabDirectives . options <$> get Ctxt
 2301 | 
 2302 | export
 2303 | getDefaultTotalityOption : {auto c : Ref Ctxt Defs} ->
 2304 |                            Core TotalReq
 2305 | getDefaultTotalityOption
 2306 |     = do defs <- get Ctxt
 2307 |          pure (totality (elabDirectives (options defs)))
 2308 | 
 2309 | export
 2310 | getAmbigLimit : {auto c : Ref Ctxt Defs} ->
 2311 |                 Core Nat
 2312 | getAmbigLimit
 2313 |     = do defs <- get Ctxt
 2314 |          pure (ambigLimit (elabDirectives (options defs)))
 2315 | 
 2316 | export
 2317 | getAutoImplicitLimit : {auto c : Ref Ctxt Defs} ->
 2318 |                        Core Nat
 2319 | getAutoImplicitLimit
 2320 |     = do defs <- get Ctxt
 2321 |          pure (autoImplicitLimit (elabDirectives (options defs)))
 2322 | 
 2323 | export
 2324 | addForeignImpl : {auto c : Ref Ctxt Defs} ->
 2325 |           FC -> (fullName : Name) -> (def : String) -> Core ()
 2326 | addForeignImpl fc name def
 2327 |    = do name <- toFullNames name
 2328 |         update Ctxt { options $= addForeignImpl name def }
 2329 | 
 2330 | export
 2331 | setPair : {auto c : Ref Ctxt Defs} ->
 2332 |           FC -> (pairType : Name) -> (fstn : Name) -> (sndn : Name) ->
 2333 |           Core ()
 2334 | setPair fc ty f s
 2335 |     = do ty' <- checkUnambig fc ty
 2336 |          f' <- checkUnambig fc f
 2337 |          s' <- checkUnambig fc s
 2338 |          update Ctxt { options $= setPair ty' f' s' }
 2339 | 
 2340 | export
 2341 | setRewrite : {auto c : Ref Ctxt Defs} ->
 2342 |              FC -> (eq : Name) -> (rwlemma : Name) -> Core ()
 2343 | setRewrite fc eq rw
 2344 |     = do rw' <- checkUnambig fc rw
 2345 |          eq' <- checkUnambig fc eq
 2346 |          update Ctxt { options $= setRewrite eq' rw' }
 2347 | 
 2348 | -- Don't check for ambiguity here; they're all meant to be overloadable
 2349 | export
 2350 | setFromInteger : {auto c : Ref Ctxt Defs} ->
 2351 |                  Name -> Core ()
 2352 | setFromInteger n = update Ctxt { options $= setFromInteger n }
 2353 | 
 2354 | export
 2355 | setFromString : {auto c : Ref Ctxt Defs} ->
 2356 |                 Name -> Core ()
 2357 | setFromString n = update Ctxt { options $= setFromString n }
 2358 | 
 2359 | export
 2360 | setFromChar : {auto c : Ref Ctxt Defs} ->
 2361 |               Name -> Core ()
 2362 | setFromChar n = update Ctxt { options $= setFromChar n }
 2363 | 
 2364 | export
 2365 | setFromDouble : {auto c : Ref Ctxt Defs} ->
 2366 |               Name -> Core ()
 2367 | setFromDouble n = update Ctxt { options $= setFromDouble n }
 2368 | 
 2369 | export
 2370 | setFromTTImp : {auto c : Ref Ctxt Defs} ->
 2371 |                Name -> Core ()
 2372 | setFromTTImp n = update Ctxt { options $= setFromTTImp n }
 2373 | 
 2374 | export
 2375 | setFromName : {auto c : Ref Ctxt Defs} ->
 2376 |               Name -> Core ()
 2377 | setFromName n = update Ctxt { options $= setFromName n }
 2378 | 
 2379 | export
 2380 | setFromDecls : {auto c : Ref Ctxt Defs} ->
 2381 |                Name -> Core ()
 2382 | setFromDecls n = update Ctxt { options $= setFromDecls n }
 2383 | 
 2384 | export
 2385 | addNameDirective : {auto c : Ref Ctxt Defs} ->
 2386 |                    FC -> Name -> List String -> Core ()
 2387 | addNameDirective fc n ns
 2388 |     = do n' <- checkUnambig fc n
 2389 |          update Ctxt { namedirectives $= insert n' ns  }
 2390 | 
 2391 | -- Checking special names from Options
 2392 | 
 2393 | export
 2394 | isPairType : {auto c : Ref Ctxt Defs} ->
 2395 |              Name -> Core Bool
 2396 | isPairType n
 2397 |     = do defs <- get Ctxt
 2398 |          case pairnames (options defs) of
 2399 |               Nothing => pure False
 2400 |               Just l => pure $ !(getFullName n) == !(getFullName (pairType l))
 2401 | 
 2402 | export
 2403 | fstName : {auto c : Ref Ctxt Defs} ->
 2404 |           Core (Maybe Name)
 2405 | fstName
 2406 |     = do defs <- get Ctxt
 2407 |          pure $ maybe Nothing (Just . fstName) (pairnames (options defs))
 2408 | 
 2409 | export
 2410 | sndName : {auto c : Ref Ctxt Defs} ->
 2411 |           Core (Maybe Name)
 2412 | sndName
 2413 |     = do defs <- get Ctxt
 2414 |          pure $ maybe Nothing (Just . sndName) (pairnames (options defs))
 2415 | 
 2416 | export
 2417 | getRewrite :{auto c : Ref Ctxt Defs} ->
 2418 |             Core (Maybe Name)
 2419 | getRewrite
 2420 |     = do defs <- get Ctxt
 2421 |          pure $ maybe Nothing (Just . rewriteName) (rewritenames (options defs))
 2422 | 
 2423 | export
 2424 | isEqualTy : {auto c : Ref Ctxt Defs} ->
 2425 |             Name -> Core Bool
 2426 | isEqualTy n
 2427 |     = do defs <- get Ctxt
 2428 |          case rewritenames (options defs) of
 2429 |               Nothing => pure False
 2430 |               Just r => pure $ !(getFullName n) == !(getFullName (equalType r))
 2431 | 
 2432 | export
 2433 | fromIntegerName : {auto c : Ref Ctxt Defs} ->
 2434 |                   Core (Maybe Name)
 2435 | fromIntegerName
 2436 |     = do defs <- get Ctxt
 2437 |          pure $ fromIntegerName (primnames (options defs))
 2438 | 
 2439 | export
 2440 | fromStringName : {auto c : Ref Ctxt Defs} ->
 2441 |                  Core (Maybe Name)
 2442 | fromStringName
 2443 |     = do defs <- get Ctxt
 2444 |          pure $ fromStringName (primnames (options defs))
 2445 | 
 2446 | export
 2447 | fromCharName : {auto c : Ref Ctxt Defs} ->
 2448 |                Core (Maybe Name)
 2449 | fromCharName
 2450 |     = do defs <- get Ctxt
 2451 |          pure $ fromCharName (primnames (options defs))
 2452 | 
 2453 | export
 2454 | fromDoubleName : {auto c : Ref Ctxt Defs} ->
 2455 |                Core (Maybe Name)
 2456 | fromDoubleName
 2457 |     = do defs <- get Ctxt
 2458 |          pure $ fromDoubleName (primnames (options defs))
 2459 | 
 2460 | export
 2461 | fromTTImpName : {auto c : Ref Ctxt Defs} ->
 2462 |                 Core (Maybe Name)
 2463 | fromTTImpName
 2464 |     = do defs <- get Ctxt
 2465 |          pure $ fromTTImpName (primnames (options defs))
 2466 | 
 2467 | export
 2468 | fromNameName : {auto c : Ref Ctxt Defs} ->
 2469 |                Core (Maybe Name)
 2470 | fromNameName
 2471 |     = do defs <- get Ctxt
 2472 |          pure $ fromNameName (primnames (options defs))
 2473 | 
 2474 | export
 2475 | fromDeclsName : {auto c : Ref Ctxt Defs} ->
 2476 |                 Core (Maybe Name)
 2477 | fromDeclsName
 2478 |     = do defs <- get Ctxt
 2479 |          pure $ fromDeclsName (primnames (options defs))
 2480 | 
 2481 | export
 2482 | getPrimNames : {auto c : Ref Ctxt Defs} -> Core PrimNames
 2483 | getPrimNames = [| MkPrimNs fromIntegerName
 2484 |                            fromStringName
 2485 |                            fromCharName
 2486 |                            fromDoubleName
 2487 |                            fromTTImpName
 2488 |                            fromNameName
 2489 |                            fromDeclsName |]
 2490 | 
 2491 | export
 2492 | getPrimitiveNames : {auto c : Ref Ctxt Defs} -> Core (List Name)
 2493 | getPrimitiveNames = primNamesToList <$> getPrimNames
 2494 | 
 2495 | export
 2496 | isPrimName : List Name -> Name -> Bool
 2497 | isPrimName prims given = let (ns, nm) = splitNS given in go ns nm prims where
 2498 | 
 2499 |   go : Namespace -> Name -> List Name -> Bool
 2500 |   go ns nm [] = False
 2501 |   go ns nm (p :: ps)
 2502 |     = let (ns', nm') = splitNS p in
 2503 |       (nm' == nm && (ns' `isApproximationOf` ns))
 2504 |       || go ns nm ps
 2505 | 
 2506 | export
 2507 | addLogLevel : {auto c : Ref Ctxt Defs} ->
 2508 |               Maybe LogLevel -> Core ()
 2509 | addLogLevel Nothing  = update Ctxt { options->session->logEnabled := False, options->session->logLevel := defaultLogLevel }
 2510 | addLogLevel (Just l) = update Ctxt { options->session->logEnabled := True, options->session->logLevel $= insertLogLevel l }
 2511 | 
 2512 | export
 2513 | setLogLevel : {auto c : Ref Ctxt Defs} ->
 2514 |               LogLevel -> Core ()
 2515 | setLogLevel = addLogLevel . Just
 2516 | 
 2517 | export
 2518 | stopLogging : {auto c : Ref Ctxt Defs} -> Core ()
 2519 | stopLogging = addLogLevel Nothing
 2520 | 
 2521 | export
 2522 | withLogLevel : {auto c : Ref Ctxt Defs} ->
 2523 |                LogLevel -> Core a -> Core a
 2524 | withLogLevel l comp = do
 2525 |   defs <- get Ctxt
 2526 |   let logs = logLevel (session (options defs))
 2527 |   put Ctxt ({ options->session->logLevel := insertLogLevel l logs } defs)
 2528 |   r <- comp
 2529 |   defs <- get Ctxt
 2530 |   put Ctxt ({ options->session->logLevel := logs } defs)
 2531 |   pure r
 2532 | 
 2533 | export
 2534 | setLogTimings : {auto c : Ref Ctxt Defs} -> Nat -> Core ()
 2535 | setLogTimings n = update Ctxt { options->session->logTimings := Just n }
 2536 | 
 2537 | export
 2538 | setDebugElabCheck : {auto c : Ref Ctxt Defs} -> Bool -> Core ()
 2539 | setDebugElabCheck b = update Ctxt { options->session->debugElabCheck := b }
 2540 | 
 2541 | export
 2542 | getSession : {auto c : Ref Ctxt Defs} ->
 2543 |              Core Session
 2544 | getSession
 2545 |     = do defs <- get Ctxt
 2546 |          pure (session (options defs))
 2547 | 
 2548 | export
 2549 | setSession : {auto c : Ref Ctxt Defs} -> Session -> Core ()
 2550 | setSession sopts = update Ctxt { options->session := sopts }
 2551 | 
 2552 | %inline
 2553 | export
 2554 | updateSession : {auto c : Ref Ctxt Defs} ->
 2555 |                 (Session -> Session) -> Core ()
 2556 | updateSession f = setSession (f !getSession)
 2557 | 
 2558 | export
 2559 | recordWarning : {auto c : Ref Ctxt Defs} -> Warning -> Core ()
 2560 | recordWarning w = update Ctxt { warnings $= (w ::) }
 2561 | 
 2562 | export
 2563 | getTime : Core Integer
 2564 | getTime
 2565 |     = do clock <- coreLift (clockTime Monotonic)
 2566 |          pure (seconds clock * nano + nanoseconds clock)
 2567 |   where
 2568 |     nano : Integer
 2569 |     nano = 1000000000
 2570 | 
 2571 | -- A simple timeout mechanism. We can start a timer, clear it, or check
 2572 | -- whether too much time has passed and throw an exception if so
 2573 | 
 2574 | ||| Initialise the timer, setting the time in milliseconds after which a
 2575 | ||| timeout should be thrown.
 2576 | ||| Note: It's important to clear the timer when the operation that might
 2577 | ||| timeout is complete, otherwise something else might throw a timeout
 2578 | ||| error!
 2579 | export
 2580 | startTimer : {auto c : Ref Ctxt Defs} ->
 2581 |              Integer -> String -> Core ()
 2582 | startTimer tmax action
 2583 |     = do t <- getTime
 2584 |          update Ctxt { timer := Just (t + tmax * 1000000, action) }
 2585 | 
 2586 | ||| Clear the timer
 2587 | export
 2588 | clearTimer : {auto c : Ref Ctxt Defs} -> Core ()
 2589 | clearTimer = update Ctxt { timer := Nothing }
 2590 | 
 2591 | ||| If the timer was started more than t milliseconds ago, throw an exception
 2592 | export
 2593 | checkTimer : {auto c : Ref Ctxt Defs} ->
 2594 |              Core ()
 2595 | checkTimer
 2596 |     = do defs <- get Ctxt
 2597 |          let Just (max, action) = timer defs
 2598 |                 | Nothing => pure ()
 2599 |          t <- getTime
 2600 |          if (t > max)
 2601 |             then throw (Timeout action)
 2602 |             else pure ()
 2603 | 
 2604 | -- Update the list of imported incremental compile data, if we're in
 2605 | -- incremental mode for the current CG
 2606 | export
 2607 | addImportedInc : {auto c : Ref Ctxt Defs} ->
 2608 |                  ModuleIdent -> List (CG, String, List String) -> Core ()
 2609 | addImportedInc modNS inc
 2610 |     = do s <- getSession
 2611 |          let cg = s.codegen
 2612 |          defs <- get Ctxt
 2613 |          when (cg `elem` s.incrementalCGs) $
 2614 |            case lookup cg inc of
 2615 |                 Nothing =>
 2616 |                   -- No incremental compile data for current CG, so we can't
 2617 |                   -- compile incrementally
 2618 |                   do recordWarning (GenericWarn emptyFC ("No incremental compile data for " ++ show modNS))
 2619 |                      defs <- get Ctxt
 2620 |                      put Ctxt ({ allIncData $= drop cg } defs)
 2621 |                      -- Tell session that the codegen is no longer incremental
 2622 |                      when (show modNS /= "") $
 2623 |                         updateSession { incrementalCGs $= (delete cg) }
 2624 |                 Just (mods, extra) =>
 2625 |                      put Ctxt ({ allIncData $= addMod cg (mods, extra) }
 2626 |                                       defs)
 2627 |   where
 2628 |     addMod : CG -> (String, List String) ->
 2629 |              List (CG, (List String, List String)) ->
 2630 |              List (CG, (List String, List String))
 2631 |     addMod cg (mod, all) [] = [(cg, ([mod], all))]
 2632 |     addMod cg (mod, all) ((cg', (mods, libs)) :: xs)
 2633 |         = if cg == cg'
 2634 |              then ((cg, (mod :: mods, libs ++ all)) :: xs)
 2635 |              else ((cg', (mods, libs)) :: addMod cg (mod, all) xs)
 2636 | 
 2637 |     drop : CG -> List (CG, a) -> List (CG, a)
 2638 |     drop cg [] = []
 2639 |     drop cg ((x, v) :: xs)
 2640 |         = if cg == x
 2641 |              then xs
 2642 |              else ((x, v) :: drop cg xs)
 2643 | 
 2644 | export
 2645 | setIncData : {auto c : Ref Ctxt Defs} ->
 2646 |              CG -> (String, List String) -> Core ()
 2647 | setIncData cg res = update Ctxt { incData $= ((cg, res) :: )}
 2648 | 
 2649 | -- Set a name as Private that was previously visible (and, if 'everywhere' is
 2650 | -- set, hide in any modules imported by this one)
 2651 | export
 2652 | hide : {auto c : Ref Ctxt Defs} ->
 2653 |        FC -> Name -> Core ()
 2654 | hide fc n
 2655 |     = do defs <- get Ctxt
 2656 |          [(nsn, _)] <- lookupCtxtName n (gamma defs)
 2657 |               | res => ambiguousName fc n (map fst res)
 2658 |          put Ctxt ({ gamma $= hideName nsn } defs)
 2659 | 
 2660 | -- Set a name as Public that was previously hidden
 2661 | -- Note: this is here at the bottom only becuase `recordWarning` is defined just above.
 2662 | export
 2663 | unhide : {auto c : Ref Ctxt Defs} ->
 2664 |        FC -> Name -> Core ()
 2665 | unhide fc n
 2666 |     = do defs <- get Ctxt
 2667 |          [(nsn, _)] <- lookupHiddenCtxtName n (gamma defs)
 2668 |               | res => ambiguousName fc n (map fst res)
 2669 |          put Ctxt ({ gamma $= unhideName nsn } defs)
 2670 |          unless (isHidden nsn (gamma defs)) $ do
 2671 |            recordWarning $ GenericWarn fc $
 2672 |              "Trying to %unhide `" ++ show nsn ++ "`, which was not hidden in the first place"
 2673 |