
    0 | module Core.Core
    1 | 
    2 | import Core.Context.Context
    3 | import Core.Env
    4 | import public Core.WithData
    5 | 
    6 | import Data.List1
    7 | import Data.SnocList
    8 | import Data.Vect
    9 | 
   10 | import Libraries.Data.List01
   11 | import Libraries.Data.IMaybe
   12 | import Libraries.Text.PrettyPrint.Prettyprinter
   13 | import Libraries.Text.PrettyPrint.Prettyprinter.Util
   14 | import Libraries.Data.Tap
   15 | import Libraries.Data.WithData
   16 | 
   17 | import public Data.IORef
   18 | import System.File
   19 | 
   20 | %hide Libraries.Data.Record.KeyVal.label
   21 | %hide Libraries.Data.Record.LabelledValue.label
   22 | 
   23 | %default covering
   24 | 
   25 | public export
   26 | data TTCErrorMsg
   27 |     = Format String Int Int
   28 |     | EndOfBuffer String
   29 |     | Corrupt String
   30 | 
   31 | public export
   32 | data CaseError = DifferingArgNumbers
   33 |                | DifferingTypes
   34 |                | MatchErased (vars ** (Env Term vars, Term vars))
   35 |                | NotFullyApplied Name
   36 |                | UnknownType
   37 | 
   38 | public export
   39 | data DotReason = NonLinearVar
   40 |                | VarApplied
   41 |                | NotConstructor
   42 |                | ErasedArg
   43 |                | UserDotted
   44 |                | UnknownDot
   45 |                | UnderAppliedCon
   46 | 
   47 | export
   48 | Show DotReason where
   49 |   show NonLinearVar = "Non linear pattern variable"
   50 |   show VarApplied = "Variable applied to arguments"
   51 |   show NotConstructor = "Not a constructor application or primitive"
   52 |   show ErasedArg = "Erased argument"
   53 |   show UserDotted = "User dotted"
   54 |   show UnknownDot = "Unknown reason"
   55 |   show UnderAppliedCon = "Under-applied constructor"
   56 | 
   57 | export
   58 | Pretty ann DotReason where
   59 |   pretty NonLinearVar = reflow "Non linear pattern variable"
   60 |   pretty VarApplied = reflow "Variable applied to arguments"
   61 |   pretty NotConstructor = reflow "Not a constructor application or primitive"
   62 |   pretty ErasedArg = reflow "Erased argument"
   63 |   pretty UserDotted = reflow "User dotted"
   64 |   pretty UnknownDot = reflow "Unknown reason"
   65 |   pretty UnderAppliedCon = reflow "Under-applied constructor"
   66 | 
   67 | public export
   68 | data Warning : Type where
   69 |      ParserWarning : FC -> String -> Warning
   70 |      UnreachableClause : {vars : _} ->
   71 |                          FC -> Env Term vars -> Term vars -> Warning
   72 |      ShadowingGlobalDefs : FC -> List1 (Name, List1 Name) -> Warning
   73 |      ||| Soft-breaking change, make an error later.
   74 |      ||| @ original Originally declared visibility on forward decl
   75 |      ||| @ new      Incompatible new visibility on actual declaration.
   76 |      IncompatibleVisibility : FC -> (original : Visibility) ->
   77 |                               (new : Visibility) -> Name -> Warning
   78 |      ||| First FC is type
   79 |      ||| @ shadowed list of names which are shadowed,
   80 |      |||   where they originally appear
   81 |      |||   and where they are shadowed
   82 |      ShadowingLocalBindings : FC -> (shadowed : List1 (String, FC, FC)) -> Warning
   83 |      ||| A warning about a deprecated definition. Supply an FC and Name to
   84 |      ||| have the documentation for the definition printed with the warning.
   85 |      Deprecated : FC -> String -> Maybe (FC, Name) -> Warning
   86 |      GenericWarn : FC -> String -> Warning
   87 | 
   88 | %name Warning wrn
   89 | 
   90 | -- All possible errors, carrying a location
   91 | public export
   92 | data Error : Type where
   93 |      Fatal : Error -> Error -- flag as unrecoverable (so don't postpone awaiting further info)
   94 |      CantConvert : {vars : _} ->
   95 |                    FC -> Context -> Env Term vars -> Term vars -> Term vars -> Error
   96 |      CantSolveEq : {vars : _} ->
   97 |                    FC -> Context -> Env Term vars -> Term vars -> Term vars -> Error
   98 |      PatternVariableUnifies : {vars : _} ->
   99 |                               FC -> FC -> Env Term vars -> Name -> Term vars -> Error
  100 |      CyclicMeta : {vars : _} ->
  101 |                   FC -> Env Term vars -> Name -> Term vars -> Error
  102 |      WhenUnifying : {vars : _} ->
  103 |                     FC -> Context -> Env Term vars -> Term vars -> Term vars -> Error -> Error
  104 |      ValidCase : {vars : _} ->
  105 |                  FC -> Env Term vars -> Either (Term vars) Error -> Error
  106 | 
  107 |      UndefinedName : FC -> Name -> Error
  108 |      InvisibleName : FC -> Name -> Maybe Namespace -> Error
  109 |      BadTypeConType : FC -> Name -> Error
  110 |      BadDataConType : FC -> Name -> Name -> Error
  111 |      NotCovering : FC -> Name -> Covering -> Error
  112 |      NotTotal : FC -> Name -> PartialReason -> Error
  113 |      ImpossibleCase : Error
  114 |         -- ^ Not a true error.
  115 |         -- Thrown deliberately to signal the coverage checker that a case is impossible
  116 |         -- (e.g. pattern match against an empty type).
  117 |      LinearUsed : FC -> Nat -> Name -> Error
  118 |      LinearMisuse : FC -> Name -> RigCount -> RigCount -> Error
  119 |      BorrowPartial : {vars : _} ->
  120 |                      FC -> Env Term vars -> Term vars -> Term vars -> Error
  121 |      BorrowPartialType : {vars : _} ->
  122 |                          FC -> Env Term vars -> Term vars -> Error
  123 |      AmbiguousName : FC -> List Name -> Error
  124 |      AmbiguousElab : {vars : _} ->
  125 |                      FC -> Env Term vars -> List (Context, Term vars) -> Error
  126 |      AmbiguousSearch : {vars : _} ->
  127 |                        FC -> Env Term vars -> Term vars -> List (Term vars) -> Error
  128 |      AmbiguityTooDeep : FC -> Name -> List Name -> Error
  129 |      AllFailed : List (Maybe Name, Error) -> Error
  130 |      RecordTypeNeeded : {vars : _} ->
  131 |                         FC -> Env Term vars -> Error
  132 |      DuplicatedRecordUpdatePath : FC -> List (List String) -> Error
  133 |      NotRecordField : FC -> String -> Maybe Name -> Error
  134 |      NotRecordType : FC -> Name -> Error
  135 |      IncompatibleFieldUpdate : FC -> List String -> Error
  136 |      InvalidArgs : {vars : _} ->
  137 |                         FC -> Env Term vars -> List Name -> Term vars -> Error
  138 |      TryWithImplicits : {vars : _} ->
  139 |                         FC -> Env Term vars -> List (Name, Term vars) -> Error
  140 |      BadUnboundImplicit : {vars : _} ->
  141 |                           FC -> Env Term vars -> Name -> Term vars -> Error
  142 |      CantSolveGoal : {vars : _} ->
  143 |                      FC -> Context -> Env Term vars -> Term vars ->
  144 |                      Maybe Error -> Error
  145 |      DeterminingArg : {vars : _} ->
  146 |                       FC -> Name -> Int -> Env Term vars -> Term vars -> Error
  147 |      UnsolvedHoles : List (FC, Name) -> Error
  148 |      CantInferArgType : {vars : _} ->
  149 |                         FC -> Env Term vars -> Name -> Name -> Term vars -> Error
  150 |      SolvedNamedHole : {vars : _} ->
  151 |                        FC -> Env Term vars -> Name -> Term vars -> Error
  152 |      VisibilityError : FC -> Visibility -> Name -> Visibility -> Name -> Error
  153 |      NonLinearPattern : FC -> Name -> Error
  154 |      BadPattern : FC -> Name -> Error
  155 |      NoDeclaration : FC -> Name -> Error
  156 |      AlreadyDefined : FC -> Name -> Error
  157 |      NotFunctionType : {vars : _} ->
  158 |                        FC -> Env Term vars -> Term vars -> Error
  159 |      RewriteNoChange : {vars : _} ->
  160 |                        FC -> Env Term vars -> Term vars -> Term vars -> Error
  161 |      NotRewriteRule : {vars : _} ->
  162 |                       FC -> Env Term vars -> Term vars -> Error
  163 |      CaseCompile : FC -> Name -> CaseError -> Error
  164 | 
  165 |      MatchTooSpecific : {vars : _} ->
  166 |                         FC -> Env Term vars -> Term vars -> Error
  167 |      BadDotPattern : {vars : _} ->
  168 |                      FC -> Env Term vars -> DotReason -> Term vars -> Term vars -> Error
  169 |      BadImplicit : FC -> String -> Error
  170 |      BadRunElab : {vars : _} ->
  171 |                   FC -> Env Term vars -> Term vars -> (description : String) -> Error
  172 |      RunElabFail : Error -> Error
  173 |      GenericMsg : FC -> String -> Error
  174 |      GenericMsgSol : FC -> (message : String) ->
  175 |                            (solutionHeader : String) -> (solutions : List String) -> Error
  176 |      OperatorBindingMismatch : {a : Type} -> {print : a -> Doc ()} ->
  177 |          FC -> (expectedFixity : FixityDeclarationInfo) -> (use_site : OperatorLHSInfo a) ->
  178 |          -- left: backticked, right: op symbolds
  179 |          (opName : Either Name Name) -> (rhs : a) -> (candidates : List String) -> Error
  180 |      TTCError : TTCErrorMsg -> Error
  181 |      FileErr : String -> FileError -> Error
  182 |      CantFindPackage : String -> Error
  183 |      LazyImplicitFunction : FC -> Error
  184 |      LazyPatternVar :  FC -> Error
  185 |      LitFail : FC -> Error
  186 |      LexFail : FC -> String -> Error
  187 |      ParseFail : List1 (FC, String) -> Error
  188 |      ModuleNotFound : FC -> ModuleIdent -> Error
  189 |      CyclicImports : List ModuleIdent -> Error
  190 |      ForceNeeded : Error
  191 |      InternalError : String -> Error
  192 |      UserError : String -> Error
  193 |      ||| Contains list of specifiers for which foreign call cannot be resolved
  194 |      NoForeignCC : FC -> List String -> Error
  195 |      BadMultiline : FC -> String -> Error
  196 |      Timeout : String -> Error
  197 |      FailingDidNotFail : FC -> Error
  198 |      FailingWrongError : FC -> String -> List1 Error -> Error
  199 | 
  200 |      InType : FC -> Name -> Error -> Error
  201 |      InCon : WithFC Name -> Error -> Error
  202 |      InLHS : FC -> Name -> Error -> Error
  203 |      InRHS : FC -> Name -> Error -> Error
  204 | 
  205 |      MaybeMisspelling : Error -> List1 String -> Error
  206 |      WarningAsError : Warning -> Error
  207 | 
  208 | %name Error err
  209 | 
  210 | export
  211 | Show TTCErrorMsg where
  212 |   show (Format file ver exp) =
  213 |     let age = if ver < exp then "older" else "newer" in
  214 |         "TTC data is in an " ++ age ++ " format, file: " ++ file ++ ", expected version: " ++ show exp ++ ", actual version: " ++ show ver
  215 |   show (EndOfBuffer when) = "End of buffer when reading " ++ when
  216 |   show (Corrupt ty) = "Corrupt TTC data for " ++ ty
  217 | 
  218 | -- Simplest possible display - higher level languages should unelaborate names
  219 | -- and display annotations appropriately
  220 | 
  221 | export
  222 | Show Warning where
  223 |     show (ParserWarning fc msg) = show fc ++ msg
  224 |     show (UnreachableClause fc _ _) = show fc ++ ":Unreachable clause"
  225 |     show (ShadowingGlobalDefs fc _) = show fc ++ ":Shadowing names"
  226 |     show (IncompatibleVisibility fc _ _ _) = show fc ++ ":Incompatible Visibility"
  227 |     show (ShadowingLocalBindings fc _) = show fc ++ ":Shadowing names"
  228 |     show (Deprecated fc name _) = show fc ++ ":Deprecated " ++ name
  229 |     show (GenericWarn fc msg) = show fc ++ msg
  230 | 
  231 | 
  232 | export
  233 | covering
  234 | Show Error where
  235 |   show (Fatal err) = show err
  236 |   show (CantConvert fc _ env x y)
  237 |       = show fc ++ ":Type mismatch: " ++ show x ++ " and " ++ show y
  238 |   show (CantSolveEq fc _ env x y)
  239 |       = show fc ++ ":" ++ show x ++ " and " ++ show y ++ " are not equal"
  240 |   show (PatternVariableUnifies fc fct env n x)
  241 |       = show fc ++ ":Pattern variable " ++ show n ++ " unifies with " ++ show x
  242 |   show (CyclicMeta fc env n tm)
  243 |       = show fc ++ ":Cycle detected in metavariable solution " ++ show n
  244 |              ++ " = " ++ show tm
  245 |   show (WhenUnifying fc _ _ x y err)
  246 |       = show fc ++ ":When unifying: " ++ show x ++ " and " ++ show y ++ "\n\t" ++ show err
  247 |   show (ValidCase fc _ prob)
  248 |       = show fc ++ ":" ++
  249 |            case prob of
  250 |              Left tm => assert_total (show tm) ++ " is not a valid impossible pattern because it typechecks"
  251 |              Right err => "Not a valid impossible pattern:\n\t" ++ assert_total (show err)
  252 |   show (UndefinedName fc x)
  253 |     = show fc ++ ":Undefined name " ++ show x
  254 |   show (InvisibleName fc x (Just ns))
  255 |        = show fc ++ ":Name " ++ show x ++ " is inaccessible since " ++
  256 |          show ns ++ " is not explicitly imported"
  257 |   show (InvisibleName fc x _) = show fc ++ ":Name " ++ show x ++ " is private"
  258 |   show (BadTypeConType fc n)
  259 |        = show fc ++ ":Return type of " ++ show n ++ " must be Type"
  260 |   show (BadDataConType fc n fam)
  261 |        = show fc ++ ":Return type of " ++ show n ++ " must be in " ++ show fam
  262 |   show (NotCovering fc n cov)
  263 |        = show fc ++ ":" ++ show n ++ " is not covering:\n\t" ++
  264 |             case cov of
  265 |                  IsCovering => "Oh yes it is (Internal error!)"
  266 |                  MissingCases cs => "Missing cases:\n\t" ++
  267 |                                            showSep "\n\t" (map show cs)
  268 |                  NonCoveringCall ns => "Calls non covering function"
  269 |                                            ++ (case ns of
  270 |                                                    [fn] => " " ++ show fn
  271 |                                                    _ => "s: " ++ showSep ", " (map show ns))
  272 | 
  273 |   show (NotTotal fc n r)
  274 |        = show fc ++ ":" ++ show n ++ " is not total"
  275 |   show ImpossibleCase
  276 |        = "Case is impossible (not an error)"
  277 |   show (LinearUsed fc count n)
  278 |       = show fc ++ ":There are " ++ show count ++ " uses of linear name " ++ show n
  279 |   show (LinearMisuse fc n exp ctx)
  280 |       = show fc ++ ":Trying to use " ++ showRig exp ++ " name " ++ show n ++
  281 |                    " in " ++ showRel ctx ++ " context"
  282 |      where
  283 |        showRig : RigCount -> String
  284 |        showRig = elimSemi
  285 |          "irrelevant"
  286 |          "linear"
  287 |          (const "unrestricted")
  288 | 
  289 |        showRel : RigCount -> String
  290 |        showRel = elimSemi
  291 |          "irrelevant"
  292 |          "relevant"
  293 |          (const "non-linear")
  294 |   show (BorrowPartial fc env t arg)
  295 |       = show fc ++ ":" ++ show t ++ " borrows argument " ++ show arg ++
  296 |                    " so must be fully applied"
  297 |   show (BorrowPartialType fc env t)
  298 |       = show fc ++ ":" ++ show t ++ " borrows, so must return a concrete type"
  299 | 
  300 |   show (AmbiguousName fc ns) = show fc ++ ":Ambiguous name " ++ show ns
  301 |   show (AmbiguousElab fc env ts) = show fc ++ ":Ambiguous elaboration " ++ show (map snd ts)
  302 |   show (AmbiguousSearch fc env tgt ts) = show fc ++ ":Ambiguous search " ++ show ts
  303 |   show (AmbiguityTooDeep fc n ns)
  304 |       = show fc ++ ":Ambiguity too deep in " ++ show n ++ " " ++ show ns
  305 |   show (AllFailed ts) = "No successful elaboration: " ++ assert_total (show ts)
  306 |   show (RecordTypeNeeded fc env)
  307 |       = show fc ++ ":Can't infer type of record to update"
  308 |   show (DuplicatedRecordUpdatePath fc ps)
  309 |       = show fc ++ ":Duplicated record update paths: " ++ show ps
  310 |   show (NotRecordField fc fld Nothing)
  311 |       = show fc ++ ":" ++ fld ++ " is not part of a record type"
  312 |   show (NotRecordField fc fld (Just ty))
  313 |       = show fc ++ ":Record type " ++ show ty ++ " has no field " ++ fld
  314 |   show (NotRecordType fc ty)
  315 |       = show fc ++ ":" ++ show ty ++ " is not a record type"
  316 |   show (IncompatibleFieldUpdate fc flds)
  317 |       = show fc ++ ":Field update " ++ showSep "->" flds ++ " not compatible with other updates"
  318 |   show (InvalidArgs fc env ns tm)
  319 |      = show fc ++ ":" ++ show ns ++ " are not valid arguments in " ++ show tm
  320 |   show (TryWithImplicits fc env imps)
  321 |      = show fc ++ ":Need to bind implicits "
  322 |           ++ showSep "," (map (\x => show (fst x) ++ " : " ++ show (snd x)) imps)
  323 |           ++ "\n(The front end should probably have done this for you. Please report!)"
  324 |   show (BadUnboundImplicit fc env n ty)
  325 |       = show fc ++ ":Can't bind name " ++ nameRoot n ++
  326 |                    " with type " ++ show ty
  327 |   show (CantSolveGoal fc gam env g cause)
  328 |       = show fc ++ ":Can't solve goal " ++ assert_total (show g)
  329 |   show (DeterminingArg fc n i env g)
  330 |       = show fc ++ ":Can't solve goal " ++ assert_total (show g) ++
  331 |                 " since argument " ++ show n ++ " can't be inferred"
  332 |   show (UnsolvedHoles hs) = "Unsolved holes " ++ show hs
  333 |   show (CantInferArgType fc env n h ty)
  334 |       = show fc ++ ":Can't infer type for " ++ show n ++
  335 |                    " (got " ++ show ty ++ " with hole " ++ show h ++ ")"
  336 |   show (SolvedNamedHole fc _ h _) = show fc ++ ":Named hole " ++ show h ++ " is solved by unification"
  337 |   show (VisibilityError fc vx x vy y)
  338 |       = show fc ++ ":" ++ show vx ++ " " ++ show x ++ " cannot refer to "
  339 |                        ++ show vy ++ " " ++ show y
  340 |   show (NonLinearPattern fc n) = show fc ++ ":Non linear pattern variable " ++ show n
  341 |   show (BadPattern fc n) = show fc ++ ":Pattern not allowed here: " ++ show n
  342 |   show (NoDeclaration fc x) = show fc ++ ":No type declaration for " ++ show x
  343 |   show (AlreadyDefined fc x) = show fc ++ ":" ++ show x ++ " is already defined"
  344 |   show (NotFunctionType fc env tm) = show fc ++ ":Not a function type: " ++ show tm
  345 |   show (RewriteNoChange fc env rule ty)
  346 |       = show fc ++ ":Rewriting by " ++ show rule ++ " did not change type " ++ show ty
  347 |   show (NotRewriteRule fc env rule)
  348 |       = show fc ++ ":" ++ show rule ++ " is not a rewrite rule type"
  349 |   show (CaseCompile fc n DifferingArgNumbers)
  350 |       = show fc ++ ":Patterns for " ++ show n ++ " have different numbers of arguments"
  351 |   show (CaseCompile fc n DifferingTypes)
  352 |       = show fc ++ ":Patterns for " ++ show n ++ " require matching on different types"
  353 |   show (CaseCompile fc n UnknownType)
  354 |       = show fc ++ ":Can't infer type to match in " ++ show n
  355 |   show (CaseCompile fc n (MatchErased (_ ** (env, tm))))
  356 |       = show fc ++ ":Attempt to match on erased argument " ++ show tm ++
  357 |                    " in " ++ show n
  358 |   show (CaseCompile fc n (NotFullyApplied c))
  359 |       = show fc ++ ":Constructor " ++ show c ++ " is not fully applied"
  360 |   show (MatchTooSpecific fc env tm)
  361 |       = show fc ++ ":Can't match on " ++ show tm ++ " as it is has a polymorphic type"
  362 |   show (BadDotPattern fc env reason x y)
  363 |       = show fc ++ ":Can't match on " ++ show x ++
  364 |            " (" ++ show reason ++ ")" ++
  365 |            " - it elaborates to " ++ show y
  366 |   show (BadImplicit fc str) = show fc ++ ":" ++ str ++ " can't be bound here"
  367 |   show (BadRunElab fc env script desc) = show fc ++ ":Bad elaborator script " ++ show script ++ " (" ++ desc ++ ")"
  368 |   show (RunElabFail e) = "Error during reflection: " ++ show e
  369 |   show (GenericMsg fc str) = show fc ++ ":" ++ str
  370 |   show (GenericMsgSol fc msg solutionHeader sols) = show fc ++ ":" ++ msg ++ " \{solutionHeader}: " ++ show sols
  371 |   show (TTCError msg) = "Error in TTC file: " ++ show msg
  372 |   show (FileErr fname err) = "File error (" ++ fname ++ "): " ++ show err
  373 |   show (CantFindPackage fname) = "Can't find package " ++ fname
  374 |   show (LazyImplicitFunction fc) = "Implicit lazy functions are not yet supported"
  375 |   show (LazyPatternVar fc) = "Defining lazy functions via pattern matching is not yet supported"
  376 |   show (LitFail fc) = show fc ++ ":Can't parse literate"
  377 |   show (LexFail fc err) = show fc ++ ":Lexer error (" ++ show err ++ ")"
  378 |   show (ParseFail errs) = "Parse errors (" ++ show errs ++ ")"
  379 |   show (ModuleNotFound fc ns)
  380 |       = show fc ++ ":" ++ show ns ++ " not found"
  381 |   show (CyclicImports ns)
  382 |       = "Module imports form a cycle: " ++ showSep " -> " (map show ns)
  383 |   show ForceNeeded = "Internal error when resolving implicit laziness"
  384 |   show (InternalError str) = "INTERNAL ERROR: " ++ str
  385 |   show (UserError str) = "Error: " ++ str
  386 |   show (NoForeignCC fc specs) = show fc ++
  387 |        ":The given specifier " ++ show specs ++ " was not accepted by any available backend."
  388 |   show (BadMultiline fc str) = "Invalid multiline string: " ++ str
  389 |   show (Timeout str) = "Timeout in " ++ str
  390 | 
  391 |   show (FailingDidNotFail _) = "Failing block did not fail"
  392 |   show (FailingWrongError fc msg err)
  393 |        = show fc ++ ":Failing block failed with the wrong error:\n" ++
  394 |          "Expected: " ++ msg ++ "\n" ++
  395 |          "but got: " ++ show err
  396 | 
  397 |   show (InType fc n err)
  398 |        = show fc ++ ":When elaborating type of " ++ show n ++ ":\n" ++
  399 |          show err
  400 |   show (InCon n err)
  401 |        = show n.fc ++ ":When elaborating type of constructor " ++ show n.val ++ ":\n" ++
  402 |          show err
  403 |   show (InLHS fc n err)
  404 |        = show fc ++ ":When elaborating left hand side of " ++ show n ++ ":\n" ++
  405 |          show err
  406 |   show (InRHS fc n err)
  407 |        = show fc ++ ":When elaborating right hand side of " ++ show n ++ ":\n" ++
  408 |          show err
  409 | 
  410 |   show (MaybeMisspelling err ns)
  411 |        = show err ++ "\nDid you mean" ++ case ns of
  412 |            (n ::: []) => ": " ++ n ++ "?"
  413 |            _ => " any of: " ++ showSep ", " (map show (forget ns)) ++ "?"
  414 |   show (WarningAsError w) = show w
  415 |   show (OperatorBindingMismatch fc (DeclaredFixity expected) actual opName rhs _)
  416 |        = show fc ++ ": Operator " ++ show opName ++ " is " ++ show expected
  417 |        ++ " but used as a " ++ show actual ++ " operator"
  418 |   show (OperatorBindingMismatch fc UndeclaredFixity actual opName rhs _)
  419 |        = show fc ++ ": Operator " ++ show opName ++ " has no declared fixity"
  420 |        ++ " but used as a " ++ show actual ++ " operator"
  421 | 
  422 | export
  423 | getWarningLoc : Warning -> FC
  424 | getWarningLoc (ParserWarning fc _) = fc
  425 | getWarningLoc (UnreachableClause fc _ _) = fc
  426 | getWarningLoc (ShadowingGlobalDefs fc _) = fc
  427 | getWarningLoc (IncompatibleVisibility loc _ _ _) = loc
  428 | getWarningLoc (ShadowingLocalBindings fc _) = fc
  429 | getWarningLoc (Deprecated fc _ fcAndName) = fromMaybe fc (fst <$> fcAndName)
  430 | getWarningLoc (GenericWarn fc _) = fc
  431 | 
  432 | export
  433 | getErrorLoc : Error -> Maybe FC
  434 | getErrorLoc (Fatal err) = getErrorLoc err
  435 | getErrorLoc (CantConvert loc _ _ _ _) = Just loc
  436 | getErrorLoc (CantSolveEq loc _ _ _ _) = Just loc
  437 | getErrorLoc (PatternVariableUnifies loc _ _ _ _) = Just loc
  438 | getErrorLoc (CyclicMeta loc _ _ _) = Just loc
  439 | getErrorLoc (WhenUnifying loc _ _ _ _ _) = Just loc
  440 | getErrorLoc (ValidCase loc _ _) = Just loc
  441 | getErrorLoc (UndefinedName loc _) = Just loc
  442 | getErrorLoc (InvisibleName loc _ _) = Just loc
  443 | getErrorLoc (BadTypeConType loc _) = Just loc
  444 | getErrorLoc (BadDataConType loc _ _) = Just loc
  445 | getErrorLoc (NotCovering loc _ _) = Just loc
  446 | getErrorLoc (NotTotal loc _ _) = Just loc
  447 | getErrorLoc ImpossibleCase = Nothing
  448 | getErrorLoc (LinearUsed loc _ _) = Just loc
  449 | getErrorLoc (LinearMisuse loc _ _ _) = Just loc
  450 | getErrorLoc (BorrowPartial loc _ _ _) = Just loc
  451 | getErrorLoc (BorrowPartialType loc _ _) = Just loc
  452 | getErrorLoc (AmbiguousName loc _) = Just loc
  453 | getErrorLoc (AmbiguousElab loc _ _) = Just loc
  454 | getErrorLoc (AmbiguousSearch loc _ _ _) = Just loc
  455 | getErrorLoc (AmbiguityTooDeep loc _ _) = Just loc
  456 | getErrorLoc (AllFailed ((_, x) :: _)) = getErrorLoc x
  457 | getErrorLoc (AllFailed []) = Nothing
  458 | getErrorLoc (RecordTypeNeeded loc _) = Just loc
  459 | getErrorLoc (DuplicatedRecordUpdatePath loc _) = Just loc
  460 | getErrorLoc (NotRecordField loc _ _) = Just loc
  461 | getErrorLoc (NotRecordType loc _) = Just loc
  462 | getErrorLoc (IncompatibleFieldUpdate loc _) = Just loc
  463 | getErrorLoc (InvalidArgs loc _ _ _) = Just loc
  464 | getErrorLoc (TryWithImplicits loc _ _) = Just loc
  465 | getErrorLoc (BadUnboundImplicit loc _ _ _) = Just loc
  466 | getErrorLoc (CantSolveGoal loc _ _ _ _) = Just loc
  467 | getErrorLoc (DeterminingArg loc _ _ _ _) = Just loc
  468 | getErrorLoc (UnsolvedHoles ((loc, _) :: _)) = Just loc
  469 | getErrorLoc (UnsolvedHoles []) = Nothing
  470 | getErrorLoc (CantInferArgType loc _ _ _ _) = Just loc
  471 | getErrorLoc (SolvedNamedHole loc _ _ _) = Just loc
  472 | getErrorLoc (VisibilityError loc _ _ _ _) = Just loc
  473 | getErrorLoc (NonLinearPattern loc _) = Just loc
  474 | getErrorLoc (BadPattern loc _) = Just loc
  475 | getErrorLoc (NoDeclaration loc _) = Just loc
  476 | getErrorLoc (AlreadyDefined loc _) = Just loc
  477 | getErrorLoc (NotFunctionType loc _ _) = Just loc
  478 | getErrorLoc (RewriteNoChange loc _ _ _) = Just loc
  479 | getErrorLoc (NotRewriteRule loc _ _) = Just loc
  480 | getErrorLoc (CaseCompile loc _ _) = Just loc
  481 | getErrorLoc (MatchTooSpecific loc _ _) = Just loc
  482 | getErrorLoc (BadDotPattern loc _ _ _ _) = Just loc
  483 | getErrorLoc (BadImplicit loc _) = Just loc
  484 | getErrorLoc (BadRunElab loc _ _ _) = Just loc
  485 | getErrorLoc (RunElabFail e) = getErrorLoc e
  486 | getErrorLoc (GenericMsg loc _) = Just loc
  487 | getErrorLoc (GenericMsgSol loc _ _ _) = Just loc
  488 | getErrorLoc (TTCError _) = Nothing
  489 | getErrorLoc (FileErr _ _) = Nothing
  490 | getErrorLoc (CantFindPackage _) = Nothing
  491 | getErrorLoc (LazyImplicitFunction loc) = Just loc
  492 | getErrorLoc (LazyPatternVar loc) = Just loc
  493 | getErrorLoc (LitFail loc) = Just loc
  494 | getErrorLoc (LexFail loc _) = Just loc
  495 | getErrorLoc (ParseFail ((loc, _) ::: _)) = Just loc
  496 | getErrorLoc (ModuleNotFound loc _) = Just loc
  497 | getErrorLoc (CyclicImports _) = Nothing
  498 | getErrorLoc ForceNeeded = Nothing
  499 | getErrorLoc (InternalError _) = Nothing
  500 | getErrorLoc (UserError _) = Nothing
  501 | getErrorLoc (NoForeignCC loc _) = Just loc
  502 | getErrorLoc (BadMultiline loc _) = Just loc
  503 | getErrorLoc (Timeout _) = Nothing
  504 | getErrorLoc (InType _ _ err) = getErrorLoc err
  505 | getErrorLoc (InCon _ err) = getErrorLoc err
  506 | getErrorLoc (FailingDidNotFail loc) = Just loc
  507 | getErrorLoc (FailingWrongError loc _ _) = Just loc
  508 | getErrorLoc (InLHS _ _ err) = getErrorLoc err
  509 | getErrorLoc (InRHS _ _ err) = getErrorLoc err
  510 | getErrorLoc (MaybeMisspelling err _) = getErrorLoc err
  511 | getErrorLoc (WarningAsError warn) = Just (getWarningLoc warn)
  512 | getErrorLoc (OperatorBindingMismatch loc _ _ _ _ _) = Just loc
  513 | 
  514 | export
  515 | killWarningLoc : Warning -> Warning
  516 | killWarningLoc (ParserWarning fc x) = ParserWarning emptyFC x
  517 | killWarningLoc (UnreachableClause fc x y) = UnreachableClause emptyFC x y
  518 | killWarningLoc (ShadowingGlobalDefs fc xs) = ShadowingGlobalDefs emptyFC xs
  519 | killWarningLoc (IncompatibleVisibility fc x y z) = IncompatibleVisibility emptyFC x y z
  520 | killWarningLoc (ShadowingLocalBindings fc xs) =
  521 |     ShadowingLocalBindings emptyFC $ (\(n, _, _) => (n, emptyFC, emptyFC)) <$> xs
  522 | killWarningLoc (Deprecated fc x y) = Deprecated emptyFC x (map ((emptyFC,) . snd) y)
  523 | killWarningLoc (GenericWarn fc x) = GenericWarn emptyFC x
  524 | 
  525 | export
  526 | killErrorLoc : Error -> Error
  527 | killErrorLoc (Fatal err) = Fatal (killErrorLoc err)
  528 | killErrorLoc (CantConvert fc x y z w) = CantConvert emptyFC x y z w
  529 | killErrorLoc (CantSolveEq fc x y z w) = CantSolveEq emptyFC x y z w
  530 | killErrorLoc (PatternVariableUnifies fc fct x y z) = PatternVariableUnifies emptyFC emptyFC x y z
  531 | killErrorLoc (CyclicMeta fc x y z) = CyclicMeta emptyFC x y z
  532 | killErrorLoc (WhenUnifying fc x y z w err) = WhenUnifying emptyFC x y z w (killErrorLoc err)
  533 | killErrorLoc (ValidCase fc x y) = ValidCase emptyFC x y
  534 | killErrorLoc (UndefinedName fc x) = UndefinedName emptyFC x
  535 | killErrorLoc (InvisibleName fc x y) = InvisibleName emptyFC x y
  536 | killErrorLoc (BadTypeConType fc x) = BadTypeConType emptyFC x
  537 | killErrorLoc (BadDataConType fc x y) = BadDataConType emptyFC x y
  538 | killErrorLoc (NotCovering fc x y) = NotCovering emptyFC x y
  539 | killErrorLoc ImpossibleCase = ImpossibleCase
  540 | killErrorLoc (NotTotal fc x y) = NotTotal emptyFC x y
  541 | killErrorLoc (LinearUsed fc k x) = LinearUsed emptyFC k x
  542 | killErrorLoc (LinearMisuse fc x y z) = LinearMisuse emptyFC x y z
  543 | killErrorLoc (BorrowPartial fc x y z) = BorrowPartial emptyFC x y z
  544 | killErrorLoc (BorrowPartialType fc x y) = BorrowPartialType emptyFC x y
  545 | killErrorLoc (AmbiguousName fc xs) = AmbiguousName emptyFC xs
  546 | killErrorLoc (AmbiguousElab fc x xs) = AmbiguousElab emptyFC x xs
  547 | killErrorLoc (AmbiguousSearch fc x y xs) = AmbiguousSearch emptyFC x y xs
  548 | killErrorLoc (AmbiguityTooDeep fc x xs) = AmbiguityTooDeep emptyFC x xs
  549 | killErrorLoc (AllFailed xs) = AllFailed (map (map killErrorLoc) xs)
  550 | killErrorLoc (RecordTypeNeeded fc x) = RecordTypeNeeded emptyFC x
  551 | killErrorLoc (DuplicatedRecordUpdatePath fc xs) = DuplicatedRecordUpdatePath emptyFC xs
  552 | killErrorLoc (NotRecordField fc x y) = NotRecordField emptyFC x y
  553 | killErrorLoc (NotRecordType fc x) = NotRecordType emptyFC x
  554 | killErrorLoc (IncompatibleFieldUpdate fc xs) = IncompatibleFieldUpdate emptyFC xs
  555 | killErrorLoc (InvalidArgs fc x xs y) = InvalidArgs emptyFC x xs y
  556 | killErrorLoc (TryWithImplicits fc x xs) = TryWithImplicits emptyFC x xs
  557 | killErrorLoc (BadUnboundImplicit fc x y z) = BadUnboundImplicit emptyFC x y z
  558 | killErrorLoc (CantSolveGoal fc x y z w) = CantSolveGoal emptyFC x y z w
  559 | killErrorLoc (DeterminingArg fc x y z w) = DeterminingArg emptyFC x y z w
  560 | killErrorLoc (UnsolvedHoles xs) = UnsolvedHoles xs
  561 | killErrorLoc (CantInferArgType fc x y z w) = CantInferArgType emptyFC x y z w
  562 | killErrorLoc (SolvedNamedHole fc x y z) = SolvedNamedHole emptyFC x y z
  563 | killErrorLoc (VisibilityError fc x y z w) = VisibilityError emptyFC x y z w
  564 | killErrorLoc (NonLinearPattern fc x) = NonLinearPattern emptyFC x
  565 | killErrorLoc (BadPattern fc x) = BadPattern emptyFC x
  566 | killErrorLoc (NoDeclaration fc x) = NoDeclaration emptyFC x
  567 | killErrorLoc (AlreadyDefined fc x) = AlreadyDefined emptyFC x
  568 | killErrorLoc (NotFunctionType fc x y) = NotFunctionType emptyFC x y
  569 | killErrorLoc (RewriteNoChange fc x y z) = RewriteNoChange emptyFC x y z
  570 | killErrorLoc (NotRewriteRule fc x y) = NotRewriteRule emptyFC x y
  571 | killErrorLoc (CaseCompile fc x y) = CaseCompile emptyFC x y
  572 | killErrorLoc (MatchTooSpecific fc x y) = MatchTooSpecific emptyFC x y
  573 | killErrorLoc (BadDotPattern fc x y z w) = BadDotPattern emptyFC x y z w
  574 | killErrorLoc (BadImplicit fc x) = BadImplicit emptyFC x
  575 | killErrorLoc (BadRunElab fc x y description) = BadRunElab emptyFC x y description
  576 | killErrorLoc (RunElabFail e) = RunElabFail $ killErrorLoc e
  577 | killErrorLoc (GenericMsg fc x) = GenericMsg emptyFC x
  578 | killErrorLoc (GenericMsgSol fc x y z) = GenericMsgSol emptyFC x y z
  579 | killErrorLoc (TTCError x) = TTCError x
  580 | killErrorLoc (FileErr x y) = FileErr x y
  581 | killErrorLoc (CantFindPackage x) = CantFindPackage x
  582 | killErrorLoc (LazyImplicitFunction fc) = LazyImplicitFunction emptyFC
  583 | killErrorLoc (LazyPatternVar fc) = LazyPatternVar emptyFC
  584 | killErrorLoc (LitFail fc) = LitFail emptyFC
  585 | killErrorLoc (LexFail fc x) = LexFail emptyFC x
  586 | killErrorLoc (ParseFail xs) = ParseFail $ map ((emptyFC,) . snd) $ xs
  587 | killErrorLoc (ModuleNotFound fc x) = ModuleNotFound emptyFC x
  588 | killErrorLoc (CyclicImports xs) = CyclicImports xs
  589 | killErrorLoc ForceNeeded = ForceNeeded
  590 | killErrorLoc (InternalError x) = InternalError x
  591 | killErrorLoc (UserError x) = UserError x
  592 | killErrorLoc (NoForeignCC fc xs) = NoForeignCC emptyFC xs
  593 | killErrorLoc (BadMultiline fc x) = BadMultiline emptyFC x
  594 | killErrorLoc (Timeout x) = Timeout x
  595 | killErrorLoc (FailingDidNotFail fc) = FailingDidNotFail emptyFC
  596 | killErrorLoc (FailingWrongError fc x errs) = FailingWrongError emptyFC x (map killErrorLoc errs)
  597 | killErrorLoc (InType fc x err) = InType emptyFC x (killErrorLoc err)
  598 | killErrorLoc (InCon x err) = InCon (NoFC x.val) (killErrorLoc err)
  599 | killErrorLoc (InLHS fc x err) = InLHS emptyFC x (killErrorLoc err)
  600 | killErrorLoc (InRHS fc x err) = InRHS emptyFC x (killErrorLoc err)
  601 | killErrorLoc (MaybeMisspelling err xs) = MaybeMisspelling (killErrorLoc err) xs
  602 | killErrorLoc (WarningAsError wrn) = WarningAsError (killWarningLoc wrn)
  603 | killErrorLoc (OperatorBindingMismatch {print} fc expected actual opName rhs candidates)
  604 |              = OperatorBindingMismatch {print} emptyFC expected actual opName rhs candidates
  605 | 
  606 | 
  607 | -- Core is a wrapper around IO that is specialised for efficiency.
  608 | export
  609 | record Core t where
  610 |   constructor MkCore
  611 |   runCore : IO (Either Error t)
  612 | 
  613 | export
  614 | coreRun : Core a ->
  615 |           (Error -> IO b) -> (a -> IO b) -> IO b
  616 | coreRun (MkCore act) err ok
  617 |     = either err ok !act
  618 | 
  619 | export
  620 | coreFail : Error -> Core a
  621 | coreFail e = MkCore (pure (Left e))
  622 | 
  623 | export
  624 | wrapError : (Error -> Error) -> Core a -> Core a
  625 | wrapError fe (MkCore prog) = MkCore $ mapFst fe <$> prog
  626 | 
  627 | -- This would be better if we restrict it to a limited set of IO operations
  628 | export
  629 | %inline
  630 | coreLift : IO a -> Core a
  631 | coreLift op = MkCore (do op' <- op
  632 |                          pure (Right op'))
  633 | 
  634 | {- Monad, Applicative, Traversable are specialised by hand for Core.
  635 | In theory, this shouldn't be necessary, but it turns out that Idris 1 doesn't
  636 | specialise interfaces under 'case' expressions, and this has a significant
  637 | impact on both compile time and run time.
  638 | 
  639 | Of course it would be a good idea to fix this in Idris, but it's not an urgent
  640 | thing on the road to self hosting, and we can make sure this isn't a problem
  641 | in the next version (i.e., in this project...)! -}
  642 | 
  643 | -- Functor (specialised)
  644 | export %inline
  645 | map : (a -> b) -> Core a -> Core b
  646 | map f (MkCore a) = MkCore (map (map f) a)
  647 | 
  648 | export %inline
  649 | (<$>) : (a -> b) -> Core a -> Core b
  650 | (<$>) f (MkCore a) = MkCore (map (map f) a)
  651 | 
  652 | export %inline
  653 | (<$) : b -> Core a -> Core b
  654 | (<$) = (<$>) . const
  655 | 
  656 | export %inline
  657 | ignore : Core a -> Core ()
  658 | ignore = map (\ _ => ())
  659 | 
  660 | -- This would be better if we restrict it to a limited set of IO operations
  661 | export
  662 | %inline
  663 | coreLift_ : IO a -> Core ()
  664 | coreLift_ op = ignore (coreLift op)
  665 | 
  666 | -- Monad (specialised)
  667 | export %inline
  668 | (>>=) : Core a -> (a -> Core b) -> Core b
  669 | (>>=) (MkCore act) f
  670 |     = MkCore (act >>=
  671 |                    \case
  672 |                      Left err => pure $ Left err
  673 |                      Right val => runCore $ f val)
  674 | 
  675 | export %inline
  676 | (>>) : Core () -> Core a -> Core a
  677 | ma >> mb = ma >>= const mb
  678 | 
  679 | -- Flipped bind
  680 | export %inline
  681 | (=<<) : (a -> Core b) -> Core a -> Core b
  682 | (=<<) = flip (>>=)
  683 | 
  684 | -- Kleisli compose
  685 | export %inline
  686 | (>=>) : (a -> Core b) -> (b -> Core c) -> (a -> Core c)
  687 | f >=> g = (g =<<) . f
  688 | 
  689 | -- Flipped kleisli compose
  690 | export %inline
  691 | (<=<) : (b -> Core c) -> (a -> Core b) -> (a -> Core c)
  692 | (<=<) = flip (>=>)
  693 | 
  694 | -- Applicative (specialised)
  695 | export %inline
  696 | pure : a -> Core a
  697 | pure x = MkCore (pure (pure x))
  698 | 
  699 | export
  700 | (<*>) : Core (a -> b) -> Core a -> Core b
  701 | (<*>) (MkCore f) (MkCore a) = MkCore [| f <*> a |]
  702 | 
  703 | export
  704 | (*>) : Core a -> Core b -> Core b
  705 | (*>) (MkCore a) (MkCore b) = MkCore [| a *> b |]
  706 | 
  707 | export
  708 | (<*) : Core a -> Core b -> Core a
  709 | (<*) (MkCore a) (MkCore b) = MkCore [| a <* b |]
  710 | 
  711 | export %inline
  712 | when : Bool -> Lazy (Core ()) -> Core ()
  713 | when True f = f
  714 | when False f = pure ()
  715 | 
  716 | 
  717 | export %inline
  718 | unless : Bool -> Lazy (Core ()) -> Core ()
  719 | unless = when . not
  720 | 
  721 | export
  722 | iwhen : (b : Bool) -> Lazy (Core a) -> Core (IMaybe b a)
  723 | iwhen True f = Just <$> f
  724 | iwhen False _ = pure Nothing
  725 | 
  726 | export
  727 | iunless : (b : Bool) -> Lazy (Core a) -> Core (IMaybe (not b) a)
  728 | iunless b f = iwhen (not b) f
  729 | 
  730 | export %inline
  731 | whenJust : Maybe a -> (a -> Core ()) -> Core ()
  732 | whenJust (Just a) k = k a
  733 | whenJust Nothing k = pure ()
  734 | 
  735 | export
  736 | iwhenJust : IMaybe b a -> (a -> Core ()) -> Core ()
  737 | iwhenJust (Just a) k = k a
  738 | iwhenJust Nothing k = pure ()
  739 | 
  740 | -- Control.Catchable in Idris 1, just copied here (but maybe no need for
  741 | -- it since we'll only have the one instance for Core Error...)
  742 | public export
  743 | interface Catchable m t | m where
  744 |     throw : {0 a : Type} -> t -> m a
  745 |     catch : m a -> (t -> m a) -> m a
  746 | 
  747 |     breakpoint : m a -> m (Either t a)
  748 | 
  749 | export
  750 | Catchable Core Error where
  751 |   catch (MkCore prog) h
  752 |       = MkCore ( do p' <- prog
  753 |                     case p' of
  754 |                          Left e => let MkCore he = h e in he
  755 |                          Right val => pure (Right val))
  756 |   breakpoint (MkCore prog) = MkCore (pure <$> prog)
  757 |   throw = coreFail
  758 | 
  759 | -- Prelude.Monad.foldlM hand specialised for Core
  760 | export
  761 | foldlC : Foldable t => (a -> b -> Core a) -> a -> t b -> Core a
  762 | foldlC fm a0 = foldl (\ma,b => ma >>= flip fm b) (pure a0)
  763 | 
  764 | -- Traversable (specialised)
  765 | traverse' : (a -> Core b) -> List a -> List b -> Core (List b)
  766 | traverse' f [] acc = pure (reverse acc)
  767 | traverse' f (x :: xs) acc
  768 |     = traverse' f xs (!(f x) :: acc)
  769 | 
  770 | %inline
  771 | export
  772 | traverse : (a -> Core b) -> List a -> Core (List b)
  773 | traverse f xs = traverse' f xs []
  774 | 
  775 | namespace SnocList
  776 |   -- Traversable (specialised)
  777 |   traverse' : (a -> Core b) -> SnocList a -> SnocList b -> Core (SnocList b)
  778 |   traverse' f [<] acc = pure acc
  779 |   traverse' f (xs :< x) acc
  780 |       = traverse' f xs (acc :< !(f x))
  781 | 
  782 |   %inline
  783 |   export
  784 |   traverse : (a -> Core b) -> SnocList a -> Core (SnocList b)
  785 |   traverse f xs = traverse' f (reverse xs) [<]
  786 | 
  787 | export
  788 | mapMaybeM : (a -> Core (Maybe b)) -> List a -> Core (List b)
  789 | mapMaybeM f = go [<] where
  790 |   go : SnocList b -> List a -> Core (List b)
  791 |   go acc [] = pure (acc <>> [])
  792 |   go acc (a::as) = do
  793 |     mb <- f a
  794 |     go (maybe id (flip (:<)) mb acc) as
  795 | 
  796 | %inline
  797 | export
  798 | for : List a -> (a -> Core b) -> Core (List b)
  799 | for = flip traverse
  800 | 
  801 | export
  802 | traverseList1 : (a -> Core b) -> List1 a -> Core (List1 b)
  803 | traverseList1 f xxs
  804 |     = let x = head xxs
  805 |           xs = tail xxs in
  806 |           [| f x ::: traverse f xs |]
  807 | 
  808 | export
  809 | traverseSnocList : (a -> Core b) -> SnocList a -> Core (SnocList b)
  810 | traverseSnocList f [<] = pure [<]
  811 | traverseSnocList f (as :< a) = [| traverseSnocList f as :< f a |]
  812 | 
  813 | export
  814 | traverseVect : (a -> Core b) -> Vect n a -> Core (Vect n b)
  815 | traverseVect f [] = pure []
  816 | traverseVect f (x :: xs) = [| f x :: traverseVect f xs |]
  817 | 
  818 | export
  819 | traverseList01 : (a -> Core b) -> List01 ne a -> Core (List01 ne b)
  820 | traverseList01 f [] = pure []
  821 | traverseList01 f (x :: xs) = [| f x :: traverseList01 f xs |]
  822 | 
  823 | %inline
  824 | export
  825 | traverseOpt : (a -> Core b) -> Maybe a -> Core (Maybe b)
  826 | traverseOpt f Nothing = pure Nothing
  827 | traverseOpt f (Just x) = map Just (f x)
  828 | 
  829 | export
  830 | traversePair : (a -> Core b) -> (w, a) -> Core (w, b)
  831 | traversePair f (w, a) = (w,) <$> f a
  832 | 
  833 | namespace List
  834 |   export
  835 |   traverse_ : (a -> Core b) -> List a -> Core ()
  836 |   traverse_ f [] = pure ()
  837 |   traverse_ f (x :: xs)
  838 |       = Core.do ignore (f x)
  839 |                 traverse_ f xs
  840 | 
  841 |   %inline
  842 |   export
  843 |   for_ : List a -> (a -> Core ()) -> Core ()
  844 |   for_ = flip traverse_
  845 | 
  846 |   export
  847 |   sequence : List (Core a) -> Core (List a)
  848 |   sequence [] = pure []
  849 |   sequence (x :: xs) = [| x :: sequence xs |]
  850 | 
  851 | -- TODO put in namespace `List1`
  852 | export
  853 | traverseList1_ : (a -> Core b) -> List1 a -> Core ()
  854 | traverseList1_ f xxs
  855 |     = do let x = head xxs
  856 |          let xs = tail xxs
  857 |          ignore (f x)
  858 |          traverse_ f xs
  859 | 
  860 | namespace SnocList
  861 |   traverse_' : (a -> Core b) -> SnocList a -> Core ()
  862 |   traverse_' f [<] = pure ()
  863 |   traverse_' f (xs :< x)
  864 |       = Core.do _ <- f x
  865 |                 traverse_' f xs
  866 | 
  867 |   export
  868 |   traverse_ : (a -> Core b) -> SnocList a -> Core ()
  869 |   traverse_ f xs = traverse_' f (reverse xs)
  870 | 
  871 | namespace WithData
  872 |   %inline export
  873 |   traverse : (ty -> Core sy) -> WithData fs ty -> Core (WithData fs sy)
  874 |   traverse f (MkWithData extra val) = MkWithData extra <$> f val
  875 | 
  876 | namespace PiInfo
  877 |   export
  878 |   traverse : (a -> Core b) -> PiInfo a -> Core (PiInfo b)
  879 |   traverse f Explicit = pure Explicit
  880 |   traverse f Implicit = pure Implicit
  881 |   traverse f AutoImplicit = pure AutoImplicit
  882 |   traverse f (DefImplicit t) = pure (DefImplicit !(f t))
  883 | 
  884 | namespace PiBindData
  885 |   export
  886 |   traverse : (a -> Core b) -> PiBindData a -> Core (PiBindData b)
  887 |   traverse f (MkPiBindData info boundType) = MkPiBindData <$> traverse f info <*> f boundType
  888 | 
  889 | namespace Binder
  890 |   export
  891 |   traverse : (a -> Core b) -> Binder a -> Core (Binder b)
  892 |   traverse f (Lam fc c p ty) = pure $ Lam fc c !(traverse f p) !(f ty)
  893 |   traverse f (Let fc c val ty) = pure $ Let fc c !(f val) !(f ty)
  894 |   traverse f (Pi fc c p ty) = pure $ Pi fc c !(traverse f p) !(f ty)
  895 |   traverse f (PVar fc c p ty) = pure $ PVar fc c !(traverse f p) !(f ty)
  896 |   traverse f (PLet fc c val ty) = pure $ PLet fc c !(f val) !(f ty)
  897 |   traverse f (PVTy fc c ty) = pure $ PVTy fc c !(f ty)
  898 | 
  899 | export
  900 | mapTermM : ({vars : _} -> Term vars -> Core (Term vars)) ->
  901 |            ({vars : _} -> Term vars -> Core (Term vars))
  902 | mapTermM f = goTerm where
  903 | 
  904 |     goTerm : {vars : _} -> Term vars -> Core (Term vars)
  905 |     goTerm tm@(Local {}) = f tm
  906 |     goTerm tm@(Ref {}) = f tm
  907 |     goTerm (Meta fc n i args) = f =<< Meta fc n i <$> traverse goTerm args
  908 |     goTerm (Bind fc x bd sc) = f =<< Bind fc x <$> traverse goTerm bd <*> goTerm sc
  909 |     goTerm (App fc fn arg) = f =<< App fc <$> goTerm fn <*> goTerm arg
  910 |     goTerm (As fc u as pat) = f =<< As fc u <$> goTerm as <*> goTerm pat
  911 |     goTerm (TDelayed fc la d) = f =<< TDelayed fc la <$> goTerm d
  912 |     goTerm (TDelay fc la ty arg) = f =<< TDelay fc la <$> goTerm ty <*> goTerm arg
  913 |     goTerm (TForce fc la t) = f =<< TForce fc la <$> goTerm t
  914 |     goTerm tm@(PrimVal {}) = f tm
  915 |     goTerm tm@(Erased {}) = f tm
  916 |     goTerm tm@(TType {}) = f tm
  917 | 
  918 | 
  919 | export
  920 | anyM : (a -> Core Bool) -> List a -> Core Bool
  921 | anyM f [] = pure False
  922 | anyM f (x :: xs)
  923 |     = if !(f x)
  924 |          then pure True
  925 |          else anyM f xs
  926 | 
  927 | namespace SnocList
  928 |   anyM' : (a -> Core Bool) -> SnocList a -> Core Bool
  929 |   anyM' f [<] = pure False
  930 |   anyM' f (xs :< x)
  931 |       = if !(f x)
  932 |           then pure True
  933 |           else anyM' f xs
  934 | 
  935 |   export
  936 |   anyM : (a -> Core Bool) -> SnocList a -> Core Bool
  937 |   anyM f xs = anyM' f (reverse xs)
  938 | 
  939 | export
  940 | allM : (a -> Core Bool) -> List a -> Core Bool
  941 | allM f [] = pure True
  942 | allM f (x :: xs)
  943 |     = if !(f x)
  944 |          then allM f xs
  945 |          else pure False
  946 | 
  947 | export
  948 | filterM : (a -> Core Bool) -> List a -> Core (List a)
  949 | filterM p [] = pure []
  950 | filterM p (x :: xs)
  951 |     = if !(p x)
  952 |          then do xs' <- filterM p xs
  953 |                  pure (x :: xs')
  954 |          else filterM p xs
  955 | 
  956 | export
  957 | newRef : (0 x : label) -> t -> Core (Ref x t)
  958 | newRef x val
  959 |     = do ref <- coreLift (newIORef val)
  960 |          pure (MkRef ref)
  961 | 
  962 | export %inline
  963 | get : (0 x : label) -> {auto ref : Ref x a} -> Core a
  964 | get x {ref = MkRef io} = coreLift (readIORef io)
  965 | 
  966 | export %inline
  967 | put : (0 x : label) -> {auto ref : Ref x a} -> a -> Core ()
  968 | put x {ref = MkRef io} val = coreLift (writeIORef io val)
  969 | 
  970 | export %inline
  971 | update : (0 x : label) -> {auto ref : Ref x a} -> (a -> a) -> Core ()
  972 | update x f
  973 |   = do v <- get x
  974 |        put x (f v)
  975 | 
  976 | export
  977 | wrapRef : (0 x : label) -> {auto ref : Ref x a} ->
  978 |           (a -> Core ()) ->
  979 |           Core b ->
  980 |           Core b
  981 | wrapRef x onClose op
  982 |   = do v <- get x
  983 |        o <- catch op $ \err =>
  984 |               do onClose v
  985 |                  put x v
  986 |                  throw err
  987 |        onClose v
  988 |        put x v
  989 |        pure o
  990 | 
  991 | export
  992 | cond : List (Lazy Bool, Lazy a) -> Lazy a -> a
  993 | cond [] def = def
  994 | cond ((x, y) :: xs) def = if x then y else cond xs def
  995 | 
  996 | export
  997 | condC : List (Core Bool, Core a) -> Core a -> Core a
  998 | condC [] def = def
  999 | condC ((x, y) :: xs) def
 1000 |     = if !x then y else condC xs def
 1001 | 
 1002 | export
 1003 | writeFile : (fname : String) -> (content : String) -> Core ()
 1004 | writeFile fname content =
 1005 |   coreLift (writeFile fname content) >>= \case
 1006 |     Right () => pure ()
 1007 |     Left err => throw $ FileErr fname err
 1008 | 
 1009 | export
 1010 | readFile : (fname : String) -> Core String
 1011 | readFile fname =
 1012 |   coreLift (readFile fname) >>= \case
 1013 |     Right content => pure content
 1014 |     Left err => throw $ FileErr fname err
 1015 | 
 1016 | namespace Functor
 1017 | 
 1018 |   export
 1019 |   [CORE] Functor Core where
 1020 |     map = Core.map
 1021 | 
 1022 | namespace Applicative
 1023 | 
 1024 |   export
 1025 |   [CORE] Applicative Core using Functor.CORE where
 1026 |     pure = Core.pure
 1027 |     (<*>) = Core.(<*>)
 1028 | 
 1029 | namespace Monad
 1030 | 
 1031 |   export
 1032 |   [CORE] Monad Core using Applicative.CORE where
 1033 |     (>>=) = Core.(>>=)
 1034 |     join mma = Core.(>>=) mma id
 1035 | 
 1036 | namespace Search
 1037 | 
 1038 |   public export
 1039 |   Search : Type -> Type
 1040 |   Search = Tap Core
 1041 | 
 1042 |   export %hint
 1043 |   functor : Functor Search
 1044 |   functor = (the (forall m. Functor m -> Functor (Tap m)) %search) CORE
 1045 | 
 1046 |   export
 1047 |   traverse : (a -> Core b) -> Search a -> Core (Search b)
 1048 |   traverse = Tap.traverse @{CORE}
 1049 | 
 1050 |   export
 1051 |   filter : (a -> Bool) -> Search a -> Core (Search a)
 1052 |   filter = Tap.filter @{CORE}
 1053 |