
    0 | module Idris.Desugar
    1 | 
    2 | import Core.CompileExpr
    3 | import Core.Env
    4 | import Core.Metadata
    5 | import Core.Unify
    6 | 
    7 | import Libraries.Data.List.Extra
    8 | import Libraries.Data.ANameMap
    9 | 
   10 | import Idris.Doc.String
   11 | import Idris.Error
   12 | import Idris.Pretty
   13 | import Idris.REPL.Opts
   14 | import Idris.Syntax
   15 | import Idris.Syntax.Builtin
   16 | 
   17 | import Idris.Elab.Implementation
   18 | import Idris.Elab.Interface
   19 | 
   20 | import Idris.Desugar.Mutual
   21 | 
   22 | import Parser.Support.Escaping
   23 | 
   24 | import TTImp.BindImplicits
   25 | import TTImp.Parser
   26 | import TTImp.ProcessType
   27 | import TTImp.TTImp
   28 | import TTImp.Utils
   29 | 
   30 | import Libraries.Data.IMaybe
   31 | import Libraries.Data.WithDefault
   32 | import Libraries.Utils.Shunting
   33 | 
   34 | import Data.List.Views
   35 | import Data.SortedMap
   36 | import Data.String
   37 | 
   38 | -- Convert high level Idris declarations (PDecl from Idris.Syntax) into
   39 | -- TTImp, recording any high level syntax info on the way (e.g. infix
   40 | -- operators)
   41 | 
   42 | -- Desugaring from high level Idris syntax to TTImp involves:
   43 | 
   44 | -- * Shunting infix operators into function applications according to precedence
   45 | -- * Replacing 'do' notating with applications of (>>=)
   46 | -- * Replacing string interpolation with concatenation by (++)
   47 | -- * Replacing pattern matching binds with 'case'
   48 | -- * Changing tuples to 'Pair/MkPair'
   49 | -- * List notation
   50 | -- * Replacing !-notation
   51 | -- * Dependent pair notation
   52 | -- * Idiom brackets
   53 | 
   54 | %default covering
   55 | 
   56 | public export
   57 | data Side = LHS | AnyExpr
   58 | 
   59 | export
   60 | Eq Side where
   61 |   LHS == LHS = True
   62 |   AnyExpr == AnyExpr = True
   63 |   _ == _ = False
   64 | 
   65 | export
   66 | extendSyn : {auto s : Ref Syn SyntaxInfo} ->
   67 |             {auto c : Ref Ctxt Defs} ->
   68 |             SyntaxInfo -> Core ()
   69 | extendSyn newsyn
   70 |     = do syn <- get Syn
   71 |          log "doc.module" 20 $ unlines
   72 |            [ "Old (" ++ unwords (map show $ saveMod syn) ++ "): "
   73 |               ++ show (modDocstrings syn)
   74 |            , "New (" ++ unwords (map show $ saveMod newsyn) ++ "): "
   75 |               ++ show (modDocstrings newsyn)
   76 |            ]
   77 | 
   78 |          -- Before we merge the two syntax environement, we remove the
   79 |          -- private fixities from the one we are importing.
   80 |          -- We keep the local private fixities since they are visible in the
   81 |          -- current file.
   82 |          let filteredFixities = removePrivate (fixities newsyn)
   83 |          put Syn ({ fixities $= merge filteredFixities,
   84 |                     ifaces $= merge (ifaces newsyn),
   85 |                     modDocstrings $= mergeLeft (modDocstrings newsyn),
   86 |                     modDocexports $= mergeLeft (modDocexports newsyn),
   87 |                     defDocstrings $= merge (defDocstrings newsyn),
   88 |                     bracketholes $= sortedNub . ((bracketholes newsyn) ++) }
   89 |                   syn)
   90 |   where
   91 |     removePrivate : ANameMap FixityInfo -> ANameMap FixityInfo
   92 |     removePrivate = fromList . filter ((/= Private) . vis . snd) . toList
   93 | 
   94 | mkPrec : Fixity -> Nat -> OpPrec
   95 | mkPrec InfixL = AssocL
   96 | mkPrec InfixR = AssocR
   97 | mkPrec Infix  = NonAssoc
   98 | mkPrec Prefix = Prefix
   99 | 
  100 | -- This is used to print the error message for fixities
  101 | [interpName] Interpolation ((OpStr' Name, FixityDeclarationInfo), b) where
  102 |   interpolate ((x, _), _) = show x.toName
  103 | 
  104 | [showWithLoc] Show ((OpStr' Name, FixityDeclarationInfo), b) where
  105 |   show ((x, DeclaredFixity y), _) = show x ++ " at " ++ show y.fc
  106 |   show ((x, UndeclaredFixity), _) = show x
  107 | 
  108 | -- Check that an operator does not have any conflicting fixities in scope.
  109 | -- Each operator can have its fixity defined multiple times across multiple
  110 | -- modules as long as the fixities are consistent. If they aren't, the fixity
  111 | -- can be hidden with %hide, this is handled by `removeFixity`.
  112 | -- Once conflicts are handled we return the operator precedence we found.
  113 | checkConflictingFixities : {auto s : Ref Syn SyntaxInfo} ->
  114 |                            {auto c : Ref Ctxt Defs} ->
  115 |                            (isPrefix : Bool) ->
  116 |                            WithFC (OpStr' Name) -> Core (OpPrec, FixityDeclarationInfo)
  117 | checkConflictingFixities isPrefix opn
  118 |   = do let op = nameRoot opn.val.toName
  119 |        foundFixities <- getFixityInfo op
  120 |        let (pre, inf) = partition ((== Prefix) . fix . snd) foundFixities
  121 |        case (isPrefix, pre, inf) of
  122 |             -- If we do not find any fixity, and it is a backticked operator, then we
  123 |             -- return the default fixity and associativity for backticked operators
  124 |             -- Otherwise, it's an unknown operator.
  125 |             (_, [], []) => case opn.val of
  126 |                               OpSymbols _ => throw (GenericMsg opn.fc "Unknown operator '\{op}'")
  127 |                               Backticked _ =>  pure (NonAssoc 1, UndeclaredFixity) -- Backticks are non associative by default
  128 | 
  129 |             (True, ((fxName, fx) :: _), _) => do
  130 |                 -- in the prefix case, remove conflicts with infix (-)
  131 |                 let extraFixities = pre ++ (filter (\(nm, _) => not $ nameRoot nm == "-") inf)
  132 |                 unless (isCompatible fx extraFixities) $ warnConflict fxName extraFixities
  133 |                 pure (mkPrec fx.fix fx.precedence, DeclaredFixity fx)
  134 |             -- Could not find any prefix operator fixities, there may still be conflicts with
  135 |             -- the infix ones.
  136 |             (True, [] , _) => throw (GenericMsg opn.fc $ "'\{op}' is not a prefix operator")
  137 | 
  138 |             (False, _, ((fxName, fx) :: _)) => do
  139 |                 -- In the infix case, remove conflicts with prefix (-)
  140 |                 let extraFixities = (filter (\(nm, _) => not $ nm == UN (Basic "-")) pre) ++ inf
  141 |                 unless (isCompatible fx extraFixities) $ warnConflict fxName extraFixities
  142 |                 pure (mkPrec fx.fix fx.precedence, DeclaredFixity fx)
  143 |             -- Could not find any infix operator fixities, there may be prefix ones
  144 |             (False, _, []) => throw (GenericMsg opn.fc $ "'\{op}' is not an infix operator")
  145 |   where
  146 |     -- Fixities are compatible with all others of the same name that share the same
  147 |     -- fixity, precedence, and binding information
  148 |     isCompatible :  FixityInfo -> (fixities : List (Name, FixityInfo)) -> Bool
  149 |     isCompatible fx
  150 |       = all (\fx' => fx.fix == fx'.fix
  151 |                   && fx.precedence == fx'.precedence
  152 |                   && fx.bindingInfo == fx'.bindingInfo) . map snd
  153 | 
  154 |     -- Emits a warning using the fixity that we picked and the list of all conflicting fixities
  155 |     warnConflict : (picked : Name) -> (conflicts : List (Name, FixityInfo)) -> Core ()
  156 |     warnConflict fxName all =
  157 |       recordWarning $ GenericWarn opn.fc $ """
  158 |                    operator fixity is ambiguous, we are picking \{show fxName} out of :
  159 |                    \{unlines $ map (\(nm, fx) => " - \{show nm}, precedence level \{show fx.precedence}") $ toList all}
  160 |                    To remove this warning, use `%hide` with the fixity to remove
  161 |                    For example: %hide \{show fxName}
  162 |                    """
  163 | 
  164 | checkConflictingBinding : Ref Ctxt Defs =>
  165 |                           Ref Syn SyntaxInfo =>
  166 |                           WithFC OpStr -> (foundFixity : FixityDeclarationInfo) ->
  167 |                           (usage : OperatorLHSInfo PTerm) -> (rhs : PTerm) -> Core ()
  168 | checkConflictingBinding opName foundFixity use_site rhs
  169 |     = if isCompatible foundFixity use_site
  170 |          then pure ()
  171 |          else throw $ OperatorBindingMismatch
  172 |              {print = byShow} opName.fc foundFixity use_site (opNameToEither opName.val) rhs !candidates
  173 |     where
  174 | 
  175 |       isCompatible : FixityDeclarationInfo -> OperatorLHSInfo PTerm -> Bool
  176 |       isCompatible UndeclaredFixity (NoBinder lhs) = True
  177 |       isCompatible UndeclaredFixity _ = False
  178 |       isCompatible (DeclaredFixity fixInfo) (NoBinder lhs) = fixInfo.bindingInfo == NotBinding
  179 |       isCompatible (DeclaredFixity fixInfo) (BindType name ty) = fixInfo.bindingInfo == Typebind
  180 |       isCompatible (DeclaredFixity fixInfo) (BindExpr name expr) = fixInfo.bindingInfo == Autobind
  181 |       isCompatible (DeclaredFixity fixInfo) (BindExplicitType name type expr)
  182 |           = fixInfo.bindingInfo == Autobind
  183 | 
  184 |       keepCompatibleBinding : BindingModifier -> (Name, GlobalDef) -> Core Bool
  185 |       keepCompatibleBinding compatibleBinder (name, def) = do
  186 |         fixities <- getFixityInfo (nameRoot name)
  187 |         let compatible = any (\(_, fx) => fx.bindingInfo == use_site.getBinder) fixities
  188 |         pure compatible
  189 | 
  190 |       candidates : Core (List String)
  191 |       candidates = do let DeclaredFixity fxInfo = foundFixity
  192 |                         | _ => pure [] -- if there is no declared fixity we can't know what's
  193 |                                        -- supposed to go there.
  194 |                       Just (nm, cs) <- getSimilarNames {keepPredicate = Just (keepCompatibleBinding fxInfo.bindingInfo)} opName.val.toName
  195 |                         | Nothing => pure []
  196 |                       ns <- currentNS <$> get Ctxt
  197 |                       pure (showSimilarNames ns opName.val.toName nm cs)
  198 | 
  199 | checkValidFixity : BindingModifier -> Fixity -> Nat -> Bool
  200 | 
  201 | -- If the fixity declaration is not binding, there are no restrictions
  202 | checkValidFixity NotBinding _ _ = True
  203 | 
  204 | -- If the fixity declaration is not binding, either typebind or autobind
  205 | -- the fixity can only be `infixr` with precedence `0`. We might want
  206 | -- to revisit that in the future, but as of right now we want to be
  207 | -- conservative and avoid abuse.
  208 | -- having multiple precedence levels would mean that if
  209 | -- =@ has higher precedence than -@
  210 | -- the expression (x : a) =@ b -@ (y : List a) =@ List b
  211 | -- would be bracketed as ((x : a) =@ b) -@ (y : List a) =@ List b
  212 | -- instead of (x : a) =@ (b -@ ((y : List a) =@ List b))
  213 | checkValidFixity _ InfixR 0 = True
  214 | 
  215 | -- If it's binding but not infixr precedence 0, raise an error
  216 | checkValidFixity _ _ _ = False
  217 | 
  218 | parameters (side : Side)
  219 |   toTokList : {auto s : Ref Syn SyntaxInfo} ->
  220 |               {auto c : Ref Ctxt Defs} ->
  221 |               PTerm -> Core (List (Tok ((OpStr, FixityDeclarationInfo), Maybe (OperatorLHSInfo PTerm)) PTerm))
  222 |   toTokList (POp fc (MkWithData _ l) opn r)
  223 |       = do (precInfo, fixInfo) <- checkConflictingFixities False opn
  224 |            unless (side == LHS) -- do not check for conflicting fixity on the LHS
  225 |                                 -- This is because we do not parse binders on the lhs
  226 |                                 -- and so, if we check, we will find uses of regular
  227 |                                 -- operator when binding is expected.
  228 |                   (checkConflictingBinding opn fixInfo l r)
  229 |            rtoks <- toTokList r
  230 |            pure (Expr l.getLhs :: Op fc opn.fc ((opn.val, fixInfo), Just l) precInfo :: rtoks)
  231 |   toTokList (PPrefixOp fc opn arg)
  232 |       = do (precInfo, fixInfo) <- checkConflictingFixities True opn
  233 |            rtoks <- toTokList arg
  234 |            pure (Op fc opn.fc ((opn.val, fixInfo), Nothing) precInfo :: rtoks)
  235 |   toTokList t = pure [Expr t]
  236 | 
  237 | record BangData where
  238 |   constructor MkBangData
  239 |   nextName : Int
  240 |   bangNames : List (Name, FC, RawImp)
  241 |   mbNamespace : Maybe Namespace
  242 | 
  243 | initBangs : Maybe Namespace -> BangData
  244 | initBangs = MkBangData 0 []
  245 | 
  246 | addNS : Maybe Namespace -> Name -> Name
  247 | addNS (Just ns) n@(NS {}) = n
  248 | addNS (Just ns) n = NS ns n
  249 | addNS _ n = n
  250 | 
  251 | bindFun : FC -> Maybe Namespace -> RawImp -> RawImp -> RawImp
  252 | bindFun fc ns ma f =
  253 |   let fc = virtualiseFC fc in
  254 |   IApp fc (IApp fc (IVar fc (addNS ns $ UN $ Basic ">>=")) ma) f
  255 | 
  256 | seqFun : FC -> Maybe Namespace -> RawImp -> RawImp -> RawImp
  257 | seqFun fc ns ma mb =
  258 |   let fc = virtualiseFC fc in
  259 |   IApp fc (IApp fc (IVar fc (addNS ns (UN $ Basic ">>"))) ma) mb
  260 | 
  261 | bindBangs : List (Name, FC, RawImp) -> Maybe Namespace -> RawImp -> RawImp
  262 | bindBangs [] ns tm = tm
  263 | bindBangs ((n, fc, btm) :: bs) ns tm
  264 |     = bindBangs bs ns
  265 |     $ bindFun fc ns btm
  266 |     $ ILam EmptyFC top Explicit (Just n) (Implicit fc False) tm
  267 | 
  268 | idiomise : FC -> Maybe Namespace -> Maybe Namespace -> RawImp -> RawImp
  269 | idiomise fc dons mns (IAlternative afc u alts)
  270 |   = IAlternative afc (mapAltType (idiomise afc dons mns) u) (idiomise afc dons mns <$> alts)
  271 | idiomise fc dons mns (IApp afc f a)
  272 |   = let fc  = virtualiseFC fc
  273 |         app = UN $ Basic "<*>"
  274 |         nm  = maybe app (`NS` app) (mns <|> dons)
  275 |      in IApp fc (IApp fc (IVar fc nm) (idiomise afc dons mns f)) a
  276 | idiomise fc dons mns fn
  277 |   = let fc  = virtualiseFC fc
  278 |         pur = UN $ Basic "pure"
  279 |         nm  = maybe pur (`NS` pur) (mns <|> dons)
  280 |      in IApp fc (IVar fc nm) fn
  281 | 
  282 | data Bang : Type where
  283 | 
  284 | mutual
  285 |   desugarB : {auto s : Ref Syn SyntaxInfo} ->
  286 |              {auto b : Ref Bang BangData} ->
  287 |              {auto c : Ref Ctxt Defs} ->
  288 |              {auto m : Ref MD Metadata} ->
  289 |              {auto u : Ref UST UState} ->
  290 |              {auto o : Ref ROpts REPLOpts} ->
  291 |              Side -> List Name -> PTerm -> Core RawImp
  292 |   desugarB side ps (PRef fc x) = do
  293 |     let ns = mbNamespace !(get Bang)
  294 |     let pur = UN $ Basic "pure"
  295 |     case x == pur of -- implicitly add namespace to unqualified occurrences of `pure` in a qualified do-block
  296 |       False => pure $ IVar fc x
  297 |       True => pure $ IVar fc (maybe pur (`NS` pur) ns)
  298 | 
  299 |   -- Desugaring forall n1, n2, n3 . s into
  300 |   -- {0 n1 : ?} -> {0 n2 : ?} -> {0 n3 : ?} -> s
  301 |   desugarB side ps (Forall (MkWithData _ (names, scope)))
  302 |         = desugarForallNames ps (forget names)
  303 |       where
  304 |         desugarForallNames : (ctx : List Name) ->
  305 |                              (names : List (WithFC Name)) -> Core RawImp
  306 |         desugarForallNames ctx [] = desugarB side ctx scope
  307 |         desugarForallNames ctx (x :: xs)
  308 |           = IPi x.fc erased Implicit (Just x.val)
  309 |           <$> desugarB side ps (PImplicit x.fc)
  310 |           <*> desugarForallNames (x.val :: ctx) xs
  311 | 
  312 |   -- Desugaring (n1, n2, n3 : t) -> s into
  313 |   -- (n1 : t) -> (n2 : t) -> (n3 : t) -> s
  314 |   desugarB side ps
  315 |       (NewPi binder@(MkWithData _
  316 |           (MkPBinderScope (MkPBinder info (MkBasicMultiBinder rig names type)) scope)))
  317 |         = desugarMultiBinder ps (forget names)
  318 |       where
  319 |         desugarMultiBinder : (ctx : List Name) -> List (WithFC Name) -> Core RawImp
  320 |         desugarMultiBinder ctx []
  321 |           = desugarB side ctx scope
  322 |         desugarMultiBinder ctx (name :: xs)
  323 |           = let extendedCtx = name.val :: ps
  324 |             in IPi binder.fc rig
  325 |               <$> mapDesugarPiInfo extendedCtx info
  326 |               <*> (pure (Just name.val))
  327 |               <*> desugarB side ps type
  328 |               <*> desugarMultiBinder extendedCtx xs
  329 | 
  330 |   desugarB side ps (PPi fc rig p mn argTy retTy)
  331 |       = let ps' = maybe ps (:: ps) mn in
  332 |             pure $ IPi fc rig !(traverse (desugar side ps') p)
  333 |                               mn !(desugarB side ps argTy)
  334 |                                  !(desugarB side ps' retTy)
  335 |   desugarB side ps (PLam fc rig p pat@(PRef prefFC n@(UN nm)) argTy scope)
  336 |       =  if isPatternVariable nm
  337 |            then do whenJust (isConcreteFC prefFC) $ \nfc
  338 |                      => addSemanticDecorations [(nfc, Bound, Just n)]
  339 |                    pure $ ILam fc rig !(traverse (desugar AnyExpr ps) p)
  340 |                            (Just n) !(desugarB AnyExpr ps argTy)
  341 |                                     !(desugar AnyExpr (n :: ps) scope)
  342 |            else pure $ ILam EmptyFC rig !(traverse (desugar AnyExpr ps) p)
  343 |                    (Just (MN "lamc" 0)) !(desugarB AnyExpr ps argTy) $
  344 |                  ICase fc [] (IVar EmptyFC (MN "lamc" 0)) (Implicit fc False)
  345 |                      [snd !(desugarClause ps True (MkPatClause fc pat scope []))]
  346 |   desugarB side ps (PLam fc rig p (PRef _ n@(MN {})) argTy scope)
  347 |       = pure $ ILam fc rig !(traverse (desugar AnyExpr ps) p)
  348 |                            (Just n) !(desugarB AnyExpr ps argTy)
  349 |                                     !(desugar AnyExpr (n :: ps) scope)
  350 |   desugarB side ps (PLam fc rig p (PImplicit _) argTy scope)
  351 |       = pure $ ILam fc rig !(traverse (desugar AnyExpr ps) p)
  352 |                            Nothing !(desugarB AnyExpr ps argTy)
  353 |                                    !(desugar AnyExpr ps scope)
  354 |   desugarB side ps (PLam fc rig p pat argTy scope)
  355 |       = pure $ ILam EmptyFC rig !(traverse (desugar AnyExpr ps) p)
  356 |                    (Just (MN "lamc" 0)) !(desugarB AnyExpr ps argTy) $
  357 |                  ICase fc [] (IVar EmptyFC (MN "lamc" 0)) (Implicit fc False)
  358 |                      [snd !(desugarClause ps True (MkPatClause fc pat scope []))]
  359 |   desugarB side ps (PLet fc rig (PRef prefFC n) nTy nVal scope [])
  360 |       = do whenJust (isConcreteFC prefFC) $ \nfc =>
  361 |              addSemanticDecorations [(nfc, Bound, Just n)]
  362 |            pure $ ILet fc prefFC rig n !(desugarB side ps nTy) !(desugarB side ps nVal)
  363 |                                        !(desugar side (n :: ps) scope)
  364 |   desugarB side ps (PLet fc rig pat nTy nVal scope alts)
  365 |       = pure $ ICase fc [] !(desugarB side ps nVal) !(desugarB side ps nTy)
  366 |                         !(traverse (map snd . desugarClause ps True)
  367 |                             (MkPatClause fc pat scope [] :: alts))
  368 |   desugarB side ps (PCase fc opts scr cls)
  369 |       = do opts <- traverse (desugarFnOpt ps) opts
  370 |            scr <- desugarB side ps scr
  371 |            let scrty = Implicit (virtualiseFC fc) False
  372 |            cls <- traverse (map snd . desugarClause ps True) cls
  373 |            pure $ ICase fc opts scr scrty cls
  374 |   desugarB side ps (PLocal fc xs scope)
  375 |       = let ps' = definedIn (map val xs) ++ ps in
  376 |             pure $ ILocal fc (concat !(traverse (desugarDecl ps') xs))
  377 |                              !(desugar side ps' scope)
  378 |   desugarB side ps (PApp pfc (PUpdate fc fs) rec)
  379 |       = pure $ IUpdate pfc !(traverse (desugarUpdate side ps) fs)
  380 |                            !(desugarB side ps rec)
  381 |   desugarB side ps (PUpdate fc fs)
  382 |       = desugarB side ps
  383 |       $ let vfc = virtualiseFC fc in
  384 |       PLam vfc top Explicit (PRef vfc (MN "rec" 0)) (PImplicit vfc)
  385 |       $ PApp vfc (PUpdate fc fs) (PRef vfc (MN "rec" 0))
  386 |   desugarB side ps (PApp fc x y)
  387 |       = pure $ IApp fc !(desugarB side ps x) !(desugarB side ps y)
  388 |   desugarB side ps (PAutoApp fc x y)
  389 |       = pure $ IAutoApp fc !(desugarB side ps x) !(desugarB side ps y)
  390 |   desugarB side ps (PWithApp fc x y)
  391 |       = pure $ IWithApp fc !(desugarB side ps x) !(desugarB side ps y)
  392 |   desugarB side ps (PNamedApp fc x argn y)
  393 |       = pure $ INamedApp fc !(desugarB side ps x) argn !(desugarB side ps y)
  394 |   desugarB side ps (PDelayed fc r ty)
  395 |       = pure $ IDelayed fc r !(desugarB side ps ty)
  396 |   desugarB side ps (PDelay fc tm)
  397 |       = pure $ IDelay fc !(desugarB side ps tm)
  398 |   desugarB side ps (PForce fc tm)
  399 |       = pure $ IForce fc !(desugarB side ps tm)
  400 |   desugarB side ps (PEq fc l r)
  401 |       = do l' <- desugarB side ps l
  402 |            r' <- desugarB side ps r
  403 |            pure $ IAlternative fc FirstSuccess
  404 |                      [apply (IVar fc (UN $ Basic "===")) [l', r'],
  405 |                       apply (IVar fc (UN $ Basic "~=~")) [l', r']]
  406 |   desugarB side ps (PBracketed fc e) = desugarB side ps e
  407 |   desugarB side ps (POp fc l op r)
  408 |       = do ts <- toTokList side (POp fc l op r)
  409 |            tree <- parseOps @{interpName} @{showWithLoc} ts
  410 |            unop <- desugarTree side ps (mapFst (\((x, _), y) => (x, y)) tree)
  411 |            desugarB side ps unop
  412 |   desugarB side ps (PPrefixOp fc op arg)
  413 |       = do ts <- toTokList side (PPrefixOp fc op arg)
  414 |            tree <- parseOps @{interpName} @{showWithLoc} ts
  415 |            unop <- desugarTree side ps (mapFst (\((x, _), y) => (x, y)) tree)
  416 |            desugarB side ps unop
  417 |   desugarB side ps (PSectionL fc op arg)
  418 |       = do syn <- get Syn
  419 |            -- It might actually be a prefix argument rather than a section
  420 |            -- so check that first, otherwise desugar as a lambda
  421 |            case lookupName op.val.toName (prefixes syn) of
  422 |                 [] =>
  423 |                     desugarB side ps
  424 |                         (PLam fc top Explicit (PRef fc (MN "arg" 0)) (PImplicit fc)
  425 |                             (POp fc (MkFCVal op.fc (NoBinder (PRef fc (MN "arg" 0)))) op arg))
  426 |                 (prec :: _) => desugarB side ps (PPrefixOp fc op arg)
  427 |   desugarB side ps (PSectionR fc arg op)
  428 |       = desugarB side ps
  429 |           (PLam fc top Explicit (PRef fc (MN "arg" 0)) (PImplicit fc)
  430 |               (POp fc (MkFCVal op.fc $ NoBinder arg) op (PRef fc (MN "arg" 0))))
  431 |   desugarB side ps (PSearch fc depth) = pure $ ISearch fc depth
  432 |   desugarB side ps (PPrimVal fc (BI x))
  433 |       = case !fromIntegerName of
  434 |              Nothing =>
  435 |                 pure $ IAlternative fc (UniqueDefault (IPrimVal fc (BI x)))
  436 |                                 [IPrimVal fc (BI x),
  437 |                                  IPrimVal fc (I (fromInteger x))]
  438 |              Just fi =>
  439 |                let vfc = virtualiseFC fc in
  440 |                pure $ IApp vfc (IVar vfc fi) (IPrimVal fc (BI x))
  441 |   desugarB side ps (PPrimVal fc (Ch x))
  442 |       = case !fromCharName of
  443 |              Nothing =>
  444 |                 pure $ IPrimVal fc (Ch x)
  445 |              Just f =>
  446 |                let vfc = virtualiseFC fc in
  447 |                pure $ IApp vfc (IVar vfc f) (IPrimVal fc (Ch x))
  448 |   desugarB side ps (PPrimVal fc (Db x))
  449 |       = case !fromDoubleName of
  450 |              Nothing =>
  451 |                 pure $ IPrimVal fc (Db x)
  452 |              Just f =>
  453 |                let vfc = virtualiseFC fc in
  454 |                pure $ IApp vfc (IVar vfc f) (IPrimVal fc (Db x))
  455 |   desugarB side ps (PPrimVal fc x) = pure $ IPrimVal fc x
  456 |   desugarB side ps (PQuote fc tm)
  457 |       = do let q = IQuote fc !(desugarB side ps tm)
  458 |            case side of
  459 |                 AnyExpr => pure $ maybeIApp fc !fromTTImpName q
  460 |                 _ => pure q
  461 |   desugarB side ps (PQuoteName fc n)
  462 |       = do let q = IQuoteName fc n
  463 |            case side of
  464 |                 AnyExpr => pure $ maybeIApp fc !fromNameName q
  465 |                 _ => pure q
  466 |   desugarB side ps (PQuoteDecl fc x)
  467 |       = do xs <- traverse (desugarDecl ps) x
  468 |            let dls = IQuoteDecl fc (concat xs)
  469 |            case side of
  470 |                 AnyExpr => pure $ maybeIApp fc !fromDeclsName dls
  471 |                 _ => pure dls
  472 |   desugarB side ps (PUnquote fc tm)
  473 |       = pure $ IUnquote fc !(desugarB side ps tm)
  474 |   desugarB side ps (PRunElab fc tm)
  475 |       = pure $ IRunElab fc True !(desugarB side ps tm)
  476 |   desugarB side ps (PHole fc br holename)
  477 |       = do when br $ update Syn { bracketholes $= ((UN (Basic holename)) ::) }
  478 |            pure $ IHole fc holename
  479 |   desugarB side ps (PType fc) = pure $ IType fc
  480 |   desugarB side ps (PAs fc nameFC vname pattern)
  481 |       = pure $ IAs fc nameFC UseRight vname !(desugarB side ps pattern)
  482 |   desugarB side ps (PDotted fc x)
  483 |       = pure $ IMustUnify fc UserDotted !(desugarB side ps x)
  484 |   desugarB side ps (PImplicit fc) = pure $ Implicit fc True
  485 |   desugarB side ps (PInfer fc)
  486 |     = do when (side == LHS) $
  487 |            throw (GenericMsg fc "? is not a valid pattern")
  488 |          pure $ Implicit fc False
  489 |   desugarB side ps (PMultiline fc hashtag indent lines)
  490 |       = pure $ maybeIApp fc !fromStringName !(expandString side ps fc hashtag !(trimMultiline fc indent lines))
  491 | 
  492 |   -- We only add `fromString` if we are looking at a plain string literal.
  493 |   -- Interpolated string literals don't have a `fromString` call since they
  494 |   -- are always concatenated with other strings and therefore can never use
  495 |   -- another `fromString` implementation that differs from `id`.
  496 |   desugarB side ps (PString fc hashtag [])
  497 |       = pure $ maybeIApp fc !fromStringName (IPrimVal fc (Str ""))
  498 |   desugarB side ps (PString fc hashtag [StrLiteral fc' str])
  499 |       = case unescape hashtag str of
  500 |              Just str => pure $ maybeIApp fc !fromStringName (IPrimVal fc' (Str str))
  501 |              Nothing => throw (GenericMsg fc "Invalid escape sequence: \{show str}")
  502 |   desugarB side ps (PString fc hashtag strs)
  503 |       = expandString side ps fc hashtag strs
  504 | 
  505 |   desugarB side ps (PDoBlock fc ns block)
  506 |       = expandDo side ps fc ns block
  507 |   desugarB side ps (PBang fc term)
  508 |       = do itm <- desugarB side ps term
  509 |            bs <- get Bang
  510 |            let bn = MN "bind" (nextName bs)
  511 |            put Bang ({ nextName $= (+1),
  512 |                        bangNames $= ((bn, fc, itm) ::)
  513 |                      } bs)
  514 |            pure (IVar (virtualiseFC fc) bn)
  515 |   desugarB side ps (PIdiom fc ns term)
  516 |       = do itm <- desugarB side ps term
  517 |            logRaw "desugar.idiom" 10 "Desugaring idiom for" itm
  518 |            let val = idiomise fc (mbNamespace !(get Bang)) ns itm
  519 |            logRaw "desugar.idiom" 10 "Desugared to" val
  520 |            pure val
  521 |   desugarB side ps (PList fc nilFC args)
  522 |       = expandList side ps nilFC args
  523 |   desugarB side ps (PSnocList fc nilFC args)
  524 |       = expandSnocList side ps nilFC args
  525 |   desugarB side ps (PPair fc l r)
  526 |       = do l' <- desugarB side ps l
  527 |            r' <- desugarB side ps r
  528 |            let pval = apply (IVar fc mkpairname) [l', r']
  529 |            pure $ IAlternative fc (UniqueDefault pval)
  530 |                   [apply (IVar fc pairname) [l', r'], pval]
  531 |   desugarB side ps (PDPair fc opFC (PRef nameFC n@(UN _)) (PImplicit _) r)
  532 |       = do r' <- desugarB side ps r
  533 |            let pval = apply (IVar opFC mkdpairname) [IVar nameFC n, r']
  534 |            let vfc = virtualiseFC nameFC
  535 |            whenJust (isConcreteFC nameFC) $ \nfc =>
  536 |              addSemanticDefault (nfc, Bound, Just n)
  537 |            pure $ IAlternative fc (UniqueDefault pval)
  538 |                   [apply (IVar opFC dpairname)
  539 |                       [Implicit vfc False,
  540 |                        ILam nameFC top Explicit (Just n) (Implicit vfc False) r'],
  541 |                    pval]
  542 |   desugarB side ps (PDPair fc opFC (PRef namefc n@(UN _)) ty r)
  543 |       = do ty' <- desugarB side ps ty
  544 |            r' <- desugarB side ps r
  545 |            pure $ apply (IVar opFC dpairname)
  546 |                         [ty', ILam namefc top Explicit (Just n) ty' r']
  547 |   desugarB side ps (PDPair fc opFC l (PImplicit _) r)
  548 |       = do l' <- desugarB side ps l
  549 |            r' <- desugarB side ps r
  550 |            pure $ apply (IVar opFC mkdpairname) [l', r']
  551 |   desugarB side ps (PDPair fc opFC l ty r)
  552 |       = throw (GenericMsg fc "Invalid dependent pair type")
  553 |   desugarB side ps (PUnit fc)
  554 |       = pure $ IAlternative fc (UniqueDefault (IVar fc (UN $ Basic "MkUnit")))
  555 |                [IVar fc (UN $ Basic "Unit"),
  556 |                 IVar fc (UN $ Basic "MkUnit")]
  557 |   desugarB side ps (PIfThenElse fc x t e)
  558 |       = let fc = virtualiseFC fc in
  559 |         pure $ ICase fc [] !(desugarB side ps x) (IVar fc (UN $ Basic "Bool"))
  560 |                    [PatClause fc (IVar fc (UN $ Basic "True")) !(desugar side ps t),
  561 |                     PatClause fc (IVar fc (UN $ Basic "False")) !(desugar side ps e)]
  562 |   desugarB side ps (PComprehension fc ret conds) = do
  563 |         let ns = mbNamespace !(get Bang)
  564 |         desugarB side ps (PDoBlock fc ns (map (guard ns) conds ++ [toPure ns ret]))
  565 |     where
  566 |       guard : Maybe Namespace -> PDo -> PDo
  567 |       guard ns (DoExp fc tm)
  568 |        = DoExp fc (PApp fc (PRef fc (mbApplyNS ns $ UN $ Basic "guard")) tm)
  569 |       guard ns d = d
  570 | 
  571 |       toPure : Maybe Namespace -> PTerm -> PDo
  572 |       toPure ns tm = DoExp fc (PApp fc (PRef fc (mbApplyNS ns $ UN $ Basic "pure")) tm)
  573 |   desugarB side ps (PRewrite fc rule tm)
  574 |       = pure $ IRewrite fc !(desugarB side ps rule) !(desugarB side ps tm)
  575 |   desugarB side ps (PRange fc start next end)
  576 |       = let fc = virtualiseFC fc in
  577 |         desugarB side ps $ case next of
  578 |            Nothing => papply fc (PRef fc (UN $ Basic "rangeFromTo")) [start,end]
  579 |            Just n  => papply fc (PRef fc (UN $ Basic "rangeFromThenTo")) [start, n, end]
  580 |   desugarB side ps (PRangeStream fc start next)
  581 |       = let fc = virtualiseFC fc in
  582 |         desugarB side ps $ case next of
  583 |            Nothing => papply fc (PRef fc (UN $ Basic "rangeFrom")) [start]
  584 |            Just n  => papply fc (PRef fc (UN $ Basic "rangeFromThen")) [start, n]
  585 |   desugarB side ps (PUnifyLog fc lvl tm)
  586 |       = pure $ IUnifyLog fc lvl !(desugarB side ps tm)
  587 |   desugarB side ps (PPostfixApp fc rec projs)
  588 |       = desugarB side ps
  589 |       $ foldl (\x, (fc, proj) => PApp fc (PRef fc proj) x) rec projs
  590 |   desugarB side ps (PPostfixAppPartial fc projs)
  591 |       = do let vfc = virtualiseFC fc
  592 |            let var = PRef vfc (MN "paRoot" 0)
  593 |            desugarB side ps $
  594 |              PLam fc top Explicit var (PImplicit vfc) $
  595 |                foldl (\r, (fc, proj) => PApp fc (PRef fc proj) r) var projs
  596 |   desugarB side ps (PWithUnambigNames fc ns rhs)
  597 |       = IWithUnambigNames fc ns <$> desugarB side ps rhs
  598 | 
  599 |   desugarUpdate : {auto s : Ref Syn SyntaxInfo} ->
  600 |                   {auto b : Ref Bang BangData} ->
  601 |                   {auto c : Ref Ctxt Defs} ->
  602 |                   {auto u : Ref UST UState} ->
  603 |                   {auto m : Ref MD Metadata} ->
  604 |                   {auto o : Ref ROpts REPLOpts} ->
  605 |                   Side -> List Name -> PFieldUpdate -> Core IFieldUpdate
  606 |   desugarUpdate side ps (PSetField p v)
  607 |       = pure (ISetField p !(desugarB side ps v))
  608 |   desugarUpdate side ps (PSetFieldApp p v)
  609 |       = pure (ISetFieldApp p !(desugarB side ps v))
  610 | 
  611 |   expandList : {auto s : Ref Syn SyntaxInfo} ->
  612 |                {auto b : Ref Bang BangData} ->
  613 |                {auto c : Ref Ctxt Defs} ->
  614 |                {auto u : Ref UST UState} ->
  615 |                {auto m : Ref MD Metadata} ->
  616 |                {auto o : Ref ROpts REPLOpts} ->
  617 |                Side -> List Name ->
  618 |                (nilFC : FC) -> List (FC, PTerm) -> Core RawImp
  619 |   expandList side ps nilFC [] = pure (IVar nilFC (UN $ Basic "Nil"))
  620 |   expandList side ps nilFC ((consFC, x) :: xs)
  621 |       = pure $ apply (IVar consFC (UN $ Basic "::"))
  622 |                 [!(desugarB side ps x), !(expandList side ps nilFC xs)]
  623 | 
  624 |   expandSnocList
  625 |              : {auto s : Ref Syn SyntaxInfo} ->
  626 |                {auto b : Ref Bang BangData} ->
  627 |                {auto c : Ref Ctxt Defs} ->
  628 |                {auto u : Ref UST UState} ->
  629 |                {auto m : Ref MD Metadata} ->
  630 |                {auto o : Ref ROpts REPLOpts} ->
  631 |                Side -> List Name -> (nilFC : FC) ->
  632 |                SnocList (FC, PTerm) -> Core RawImp
  633 |   expandSnocList side ps nilFC [<] = pure (IVar nilFC (UN $ Basic "Lin"))
  634 |   expandSnocList side ps nilFC (xs :< (consFC, x))
  635 |       = pure $ apply (IVar consFC (UN $ Basic ":<"))
  636 |                 [!(expandSnocList side ps nilFC xs) , !(desugarB side ps x)]
  637 | 
  638 |   maybeIApp : FC -> Maybe Name -> RawImp -> RawImp
  639 |   maybeIApp fc nm tm
  640 |       = case nm of
  641 |              Nothing => tm
  642 |              Just f =>
  643 |                let fc = virtualiseFC fc in
  644 |                IApp fc (IVar fc f) tm
  645 | 
  646 |   expandString : {auto s : Ref Syn SyntaxInfo} ->
  647 |                  {auto b : Ref Bang BangData} ->
  648 |                  {auto c : Ref Ctxt Defs} ->
  649 |                  {auto m : Ref MD Metadata} ->
  650 |                  {auto u : Ref UST UState} ->
  651 |                  {auto o : Ref ROpts REPLOpts} ->
  652 |                  Side -> List Name -> FC -> Nat -> List PStr -> Core RawImp
  653 |   expandString side ps fc hashtag xs
  654 |     = do xs <- traverse toRawImp (filter notEmpty $ mergeStrLit xs)
  655 |          pure $ case xs of
  656 |            [] => IPrimVal fc (Str "")
  657 |            (_ :: _) =>
  658 |              let vfc = virtualiseFC fc in
  659 |              IApp vfc
  660 |                (INamedApp vfc
  661 |                  (IVar vfc (NS preludeNS $ UN $ Basic "concat"))
  662 |                  (UN $ Basic "t")
  663 |                  (IVar vfc (NS preludeNS $ UN $ Basic "List")))
  664 |                (strInterpolate xs)
  665 |     where
  666 |       toRawImp : PStr -> Core RawImp
  667 |       toRawImp (StrLiteral fc str) =
  668 |         case unescape hashtag str of
  669 |              Just str => pure $ IPrimVal fc (Str str)
  670 |              Nothing => throw (GenericMsg fc "Invalid escape sequence: \{show str}")
  671 |       toRawImp (StrInterp fc tm) = desugarB side ps tm
  672 | 
  673 |       -- merge neighbouring StrLiteral
  674 |       mergeStrLit : List PStr -> List PStr
  675 |       mergeStrLit xs = case List.spanBy isStrLiteral xs of
  676 |         ([], []) => []
  677 |         ([], x::xs) => x :: mergeStrLit xs
  678 |         (lits@(_::_), xs) =>
  679 |           -- TODO: merge all the FCs of the merged literals!
  680 |           let fc  = fst $ head lits in
  681 |           let lit = fastConcat $ snd <$> lits in
  682 |           StrLiteral fc lit :: mergeStrLit xs
  683 | 
  684 |       notEmpty : PStr -> Bool
  685 |       notEmpty (StrLiteral _ str) = str /= ""
  686 |       notEmpty (StrInterp {}) = True
  687 | 
  688 |       strInterpolate : List RawImp -> RawImp
  689 |       strInterpolate []
  690 |         = IVar EmptyFC nilName
  691 |       strInterpolate (x :: xs)
  692 |         = let xFC = virtualiseFC (getFC x) in
  693 |           apply (IVar xFC consName)
  694 |           [ IApp xFC (IVar EmptyFC interpolateName)
  695 |                      x
  696 |           , strInterpolate xs
  697 |           ]
  698 | 
  699 |   trimMultiline : FC -> Nat -> List (List PStr) -> Core (List PStr)
  700 |   trimMultiline fc indent lines
  701 |       = do lines <- trimLast fc lines
  702 |            lines <- traverse (trimLeft indent) lines
  703 |            pure $ concat $ dropLastNL lines
  704 | 
  705 |     where
  706 |       trimLast : FC -> List (List PStr) -> Core (List (List PStr))
  707 |       trimLast fc lines with (snocList lines)
  708 |         trimLast fc [] | Empty = throw $ BadMultiline fc "Expected new line"
  709 |         trimLast _ (initLines `snoc` []) | Snoc [] initLines _ = pure lines
  710 |         trimLast _ (initLines `snoc` [StrLiteral fc str]) | Snoc [(StrLiteral {})] initLines _
  711 |             = if any (not . isSpace) (fastUnpack str)
  712 |                      then throw $ BadMultiline fc "Closing delimiter of multiline strings cannot be preceded by non-whitespace characters"
  713 |                      else pure initLines
  714 |         trimLast _ (initLines `snoc` xs) | Snoc xs initLines _
  715 |             = let fc = fromMaybe fc $ findBy isStrInterp xs in
  716 |                   throw $ BadMultiline fc "Closing delimiter of multiline strings cannot be preceded by non-whitespace characters"
  717 | 
  718 |       trimLeft : Nat -> List PStr -> Core (List PStr)
  719 |       trimLeft indent [] = pure []
  720 |       trimLeft indent [StrLiteral fc str]
  721 |           = let (trimed, rest) = splitAt indent (fastUnpack str) in
  722 |             if any (not . isSpace) trimed
  723 |               then throw $ BadMultiline fc "Line is less indented than the closing delimiter"
  724 |               else let str = if null rest then "\n" else fastPack rest in
  725 |                    pure [StrLiteral fc str]
  726 |       trimLeft indent (StrLiteral fc str :: xs)
  727 |           = let (trimed, rest) = splitAt indent (fastUnpack str) in
  728 |             if any (not . isSpace) trimed || length trimed < indent
  729 |               then throw $ BadMultiline fc "Line is less indented than the closing delimiter"
  730 |              else pure $ (StrLiteral fc (fastPack rest))::xs
  731 |       trimLeft indent xs = throw $ BadMultiline fc "Line is less indented than the closing delimiter"
  732 | 
  733 |       mapLast : (a -> a) -> List a -> List a
  734 |       mapLast f [] = []
  735 |       mapLast f [x] = [f x]
  736 |       mapLast f (x :: xs) = x :: mapLast f xs
  737 | 
  738 |       dropLastNL : List (List PStr) -> List (List PStr)
  739 |       dropLastNL
  740 |           = mapLast $ mapLast $
  741 |               \case StrLiteral fc str => StrLiteral fc (fst $ break isNL str)
  742 |                     other => other
  743 | 
  744 |   expandDo : {auto s : Ref Syn SyntaxInfo} ->
  745 |              {auto c : Ref Ctxt Defs} ->
  746 |              {auto u : Ref UST UState} ->
  747 |              {auto m : Ref MD Metadata} ->
  748 |              {auto o : Ref ROpts REPLOpts} ->
  749 |              Side -> List Name -> FC -> Maybe Namespace -> List PDo -> Core RawImp
  750 |   expandDo side ps fc ns [] = throw (GenericMsg fc "Do block cannot be empty")
  751 |   expandDo side ps _ ns [DoExp fc tm] = desugarDo side ps ns tm
  752 |   expandDo side ps fc ns [e]
  753 |       = throw (GenericMsg (getLoc e)
  754 |                   "Last statement in do block must be an expression")
  755 |   expandDo side ps topfc ns (DoExp fc tm :: rest)
  756 |       = do tm' <- desugarDo side ps ns tm
  757 |            rest' <- expandDo side ps topfc ns rest
  758 |            pure $ seqFun fc ns tm' rest'
  759 |   expandDo side ps topfc ns (DoBind fc nameFC n rig ty tm :: rest)
  760 |       = do tm' <- desugarDo side ps ns tm
  761 |            whenJust (isConcreteFC nameFC) $ \nfc => addSemanticDecorations [(nfc, Bound, Just n)]
  762 |            ty' <- maybe (pure $ Implicit (virtualiseFC fc) False)
  763 |                         (\ty => desugarDo side ps ns ty) ty
  764 |            rest' <- expandDo side ps topfc ns rest
  765 |            pure $ bindFun fc ns tm'
  766 |                 $ ILam nameFC rig Explicit (Just n) ty' rest'
  767 |   expandDo side ps topfc ns (DoBindPat fc pat ty exp alts :: rest)
  768 |       = do pat' <- desugarDo LHS ps ns pat
  769 |            (newps, bpat) <- bindNames False pat'
  770 |            exp' <- desugarDo side ps ns exp
  771 |            alts' <- traverse (map snd . desugarClause ps True) alts
  772 |            let ps' = newps ++ ps
  773 |            let fcOriginal = fc
  774 |            let fc = virtualiseFC fc
  775 |            let patFC = virtualiseFC (getFC bpat)
  776 |            ty' <- maybe (pure $ Implicit fc False)
  777 |                         (\ty => desugarDo side ps ns ty) ty
  778 |            rest' <- expandDo side ps' topfc ns rest
  779 |            pure $ bindFun fc ns exp'
  780 |                 $ ILam EmptyFC top Explicit (Just (MN "_" 0))
  781 |                           ty'
  782 |                           (ICase fc [] (IVar patFC (MN "_" 0))
  783 |                                (Implicit fc False)
  784 |                                (PatClause fcOriginal bpat rest'
  785 |                                   :: alts'))
  786 |   expandDo side ps topfc ns (DoLet fc lhsFC n rig ty tm :: rest)
  787 |       = do b <- newRef Bang (initBangs ns)
  788 |            tm' <- desugarB side ps tm
  789 |            ty' <- desugarDo side ps ns ty
  790 |            rest' <- expandDo side ps topfc ns rest
  791 |            whenJust (isConcreteFC lhsFC) $ \nfc =>
  792 |              addSemanticDecorations [(nfc, Bound, Just n)]
  793 |            let bind = ILet fc lhsFC rig n ty' tm' rest'
  794 |            bd <- get Bang
  795 |            pure $ bindBangs (bangNames bd) ns bind
  796 |   expandDo side ps topfc ns (DoLetPat fc pat ty tm alts :: rest)
  797 |       = do b <- newRef Bang (initBangs ns)
  798 |            pat' <- desugarDo LHS ps ns pat
  799 |            ty' <- desugarDo side ps ns ty
  800 |            (newps, bpat) <- bindNames False pat'
  801 |            tm' <- desugarB side ps tm
  802 |            alts' <- traverse (map snd . desugarClause ps True) alts
  803 |            let ps' = newps ++ ps
  804 |            rest' <- expandDo side ps' topfc ns rest
  805 |            bd <- get Bang
  806 |            let fc = virtualiseFC fc
  807 |            pure $ bindBangs (bangNames bd) ns $
  808 |                     ICase fc [] tm' ty'
  809 |                        (PatClause fc bpat rest'
  810 |                                   :: alts')
  811 |   expandDo side ps topfc ns (DoLetLocal fc decls :: rest)
  812 |       = do decls' <- traverse (desugarDecl ps) decls
  813 |            rest' <- expandDo side ps topfc ns rest
  814 |            pure $ ILocal fc (concat decls') rest'
  815 |   expandDo side ps topfc ns (DoRewrite fc rule :: rest)
  816 |       = do rule' <- desugarDo side ps ns rule
  817 |            rest' <- expandDo side ps topfc ns rest
  818 |            pure $ IRewrite fc rule' rest'
  819 | 
  820 |   -- Replace all operator by function application
  821 |   desugarTree : Side -> List Name -> Tree (OpStr, Maybe $ OperatorLHSInfo PTerm) PTerm ->
  822 |                 Core PTerm
  823 |   desugarTree side ps (Infix loc eqFC (OpSymbols $ UN $ Basic "=", _) l r) -- special case since '=' is special syntax
  824 |       = pure $ PEq eqFC !(desugarTree side ps l) !(desugarTree side ps r)
  825 | 
  826 |   desugarTree side ps (Infix loc _ (OpSymbols $ UN $ Basic "$", _) l r) -- special case since '$' is special syntax
  827 |       = do l' <- desugarTree side ps l
  828 |            r' <- desugarTree side ps r
  829 |            pure (PApp loc l' r')
  830 |   -- normal operators
  831 |   desugarTree side ps (Infix loc opFC (op, Just (NoBinder lhs)) l r)
  832 |       = do l' <- desugarTree side ps l
  833 |            r' <- desugarTree side ps r
  834 |            pure (PApp loc (PApp loc (PRef opFC op.toName) l') r')
  835 |   -- (x : ty) =@ f x ==>> (=@) ty (\x : ty => f x)
  836 |   desugarTree side ps (Infix loc opFC (op, Just (BindType pat lhs)) l r)
  837 |       = do l' <- desugarTree side ps l
  838 |            body <- desugarTree side ps r
  839 |            pure $ PApp loc (PApp loc (PRef opFC op.toName) l')
  840 |                       (PLam loc top Explicit pat l' body)
  841 |   -- (x := exp) =@ f x ==>> (=@) exp (\x : ? => f x)
  842 |   desugarTree side ps (Infix loc opFC (op, Just (BindExpr pat lhs)) l r)
  843 |       = do l' <- desugarTree side ps l
  844 |            body <- desugarTree side ps r
  845 |            pure $ PApp loc (PApp loc (PRef opFC op.toName) l')
  846 |                       (PLam loc top Explicit pat (PInfer opFC) body)
  847 | 
  848 |   -- (x : ty := exp) =@ f x ==>> (=@) exp (\x : ty => f x)
  849 |   desugarTree side ps (Infix loc opFC (op, Just (BindExplicitType pat ty expr)) l r)
  850 |       = do l' <- desugarTree side ps l
  851 |            body <- desugarTree side ps r
  852 |            pure $ PApp loc (PApp loc (PRef opFC op.toName) l')
  853 |                       (PLam loc top Explicit pat ty body)
  854 |   desugarTree side ps (Infix loc opFC (op, Nothing) _ r)
  855 |       = throw $ InternalError "illegal fixity: Parsed as infix but no binding information"
  856 | 
  857 |   -- negation is a special case, since we can't have an operator with
  858 |   -- two meanings otherwise
  859 |   --
  860 |   -- Note: In case of negated signed integer literals, we apply the
  861 |   -- negation directly. Otherwise, the literal might be
  862 |   -- truncated to 0 before being passed on to `negate`.
  863 |   desugarTree side ps (Pre loc opFC (OpSymbols $ UN $ Basic "-", _) $ Leaf $ PPrimVal fc c)
  864 |     = let newFC    = fromMaybe EmptyFC (mergeFC loc fc)
  865 |           continue = desugarTree side ps . Leaf . PPrimVal newFC
  866 |        in case c of
  867 |             I   x => continue $ I (-x)
  868 |             I8  x => continue $ I8 (-x)
  869 |             I16 x => continue $ I16 (-x)
  870 |             I32 x => continue $ I32 (-x)
  871 |             I64 x => continue $ I64 (-x)
  872 |             BI  x => continue $ BI (-x)
  873 | 
  874 |             -- not a signed integer literal. proceed by desugaring
  875 |             -- and applying to `negate`.
  876 |             _     => do arg' <- desugarTree side ps (Leaf $ PPrimVal fc c)
  877 |                         pure (PApp loc (PRef opFC (UN $ Basic "negate")) arg')
  878 | 
  879 |   desugarTree side ps (Pre loc opFC (OpSymbols $ UN $ Basic "-", _) arg)
  880 |     = do arg' <- desugarTree side ps arg
  881 |          pure (PApp loc (PRef opFC (UN $ Basic "negate")) arg')
  882 | 
  883 |   desugarTree side ps (Pre loc opFC (op, _) arg)
  884 |       = do arg' <- desugarTree side ps arg
  885 |            pure (PApp loc (PRef opFC op.toName) arg')
  886 |   desugarTree side ps (Leaf t) = pure t
  887 | 
  888 |   desugarType : {auto s : Ref Syn SyntaxInfo} ->
  889 |                 {auto c : Ref Ctxt Defs} ->
  890 |                 {auto u : Ref UST UState} ->
  891 |                 {auto m : Ref MD Metadata} ->
  892 |                 {auto o : Ref ROpts REPLOpts} ->
  893 |                 List Name -> PTypeDecl -> Core (List ImpTy)
  894 |   desugarType ps pty@(MkWithData _ $ MkPTy names d ty)
  895 |       = flip Core.traverse (forget names) $ \(doc, n) : (String, WithFC Name) =>
  896 |           do addDocString n.val (d ++ doc)
  897 |              syn <- get Syn
  898 |              pure $ Mk [pty.fc, n] !(bindTypeNames pty.fc (usingImpl syn)
  899 |                                                  ps !(desugar AnyExpr ps ty))
  900 | 
  901 |   -- Attempt to get the function name from a function pattern. For example,
  902 |   --   - given the pattern 'f x y', getClauseFn would return 'f'.
  903 |   --   - given the pattern 'x == y', getClausefn would return '=='.
  904 |   getClauseFn : RawImp -> Core Name
  905 |   getClauseFn (IVar _ n) = pure n
  906 |   getClauseFn (IApp _ f _) = getClauseFn f
  907 |   getClauseFn (IWithApp _ f _) = getClauseFn f
  908 |   getClauseFn (IAutoApp _ f _) = getClauseFn f
  909 |   getClauseFn (INamedApp _ f _ _) = getClauseFn f
  910 |   getClauseFn tm = throw $ GenericMsg (getFC tm) "Head term in pattern must be a function name"
  911 | 
  912 |   desugarLHS : {auto s : Ref Syn SyntaxInfo} ->
  913 |                {auto c : Ref Ctxt Defs} ->
  914 |                {auto m : Ref MD Metadata} ->
  915 |                {auto u : Ref UST UState} ->
  916 |                {auto o : Ref ROpts REPLOpts} ->
  917 |                List Name -> (arg : Bool) -> PTerm ->
  918 |                Core (IMaybe (not arg) Name, List Name, RawImp)
  919 |                   -- ^ we only look for the head name of the expression...
  920 |                   --   if we are actually looking at a headed thing!
  921 |   desugarLHS ps arg lhs =
  922 |     do rawlhs <- desugar LHS ps lhs
  923 |        inm <- iunless arg $ getClauseFn rawlhs
  924 |        (bound, blhs) <- bindNames arg rawlhs
  925 |        log "desugar.lhs" 10 "Desugared \{show lhs} to \{show blhs}"
  926 |        iwhenJust inm $ \ nm =>
  927 |          when (nm `elem` bound) $ do
  928 |            let fc = getPTermLoc lhs
  929 |            throw $ GenericMsg fc $ concat $ the (List String)
  930 |              [ "Declaration name ("
  931 |              , show nm
  932 |              , ") shadowed by a pattern variable."
  933 |              ]
  934 | 
  935 |        pure (inm, bound, blhs)
  936 | 
  937 |   desugarWithProblem :
  938 |     {auto s : Ref Syn SyntaxInfo} ->
  939 |     {auto c : Ref Ctxt Defs} ->
  940 |     {auto u : Ref UST UState} ->
  941 |     {auto m : Ref MD Metadata} ->
  942 |     {auto o : Ref ROpts REPLOpts} ->
  943 |     List Name -> PWithProblem ->
  944 |     Core (RigCount, RawImp, Maybe (RigCount, Name))
  945 |   desugarWithProblem ps (MkPWithProblem rig wval mnm)
  946 |     = (rig,,mnm) <$> desugar AnyExpr ps wval
  947 | 
  948 |   desugarClause : {auto s : Ref Syn SyntaxInfo} ->
  949 |                   {auto c : Ref Ctxt Defs} ->
  950 |                   {auto u : Ref UST UState} ->
  951 |                   {auto m : Ref MD Metadata} ->
  952 |                   {auto o : Ref ROpts REPLOpts} ->
  953 |                   List Name -> (arg : Bool) -> PClause ->
  954 |                   Core (IMaybe (not arg) Name, ImpClause)
  955 |   desugarClause ps arg (MkPatClause fc lhs rhs wheres)
  956 |       = do ws <- traverse (desugarDecl ps) wheres
  957 | 
  958 |            (nm, bound, lhs') <- desugarLHS ps arg lhs
  959 | 
  960 |            -- desugar rhs, putting where clauses as local definitions
  961 |            rhs' <- desugar AnyExpr (bound ++ ps) rhs
  962 |            let rhs' = case ws of
  963 |                         [] => rhs'
  964 |                         _ => ILocal fc (concat ws) rhs'
  965 | 
  966 |            pure (nm, PatClause fc lhs' rhs')
  967 | 
  968 |   desugarClause ps arg (MkWithClause fc lhs wps flags cs)
  969 |       = do cs' <- traverse (map snd . desugarClause ps arg) cs
  970 |            (nm, bound, lhs') <- desugarLHS ps arg lhs
  971 |            wps' <- traverseList1 (desugarWithProblem (bound ++ ps)) wps
  972 |            pure (nm, mkWithClause fc lhs' wps' flags cs')
  973 | 
  974 |   desugarClause ps arg (MkImpossible fc lhs)
  975 |       = do (nm, _, lhs') <- desugarLHS ps arg lhs
  976 |            pure (nm, ImpossibleClause fc lhs')
  977 | 
  978 |   desugarData : {auto s : Ref Syn SyntaxInfo} ->
  979 |                 {auto c : Ref Ctxt Defs} ->
  980 |                 {auto u : Ref UST UState} ->
  981 |                 {auto m : Ref MD Metadata} ->
  982 |                 {auto o : Ref ROpts REPLOpts} ->
  983 |                 List Name -> (doc : String) ->
  984 |                 PDataDecl -> Core ImpData
  985 |   desugarData ps doc (MkPData fc n tycon opts datacons)
  986 |       = do addDocString n doc
  987 |            syn <- get Syn
  988 |            mm <- traverse (desugarType ps) datacons
  989 |            pure $ MkImpData fc n
  990 |                    !(flip traverseOpt tycon $ \ tycon => do
  991 |                       tycon <- desugar AnyExpr ps tycon
  992 |                       bindTypeNames fc (usingImpl syn) ps tycon)
  993 |                    opts
  994 |                    (concat mm)
  995 |   desugarData ps doc (MkPLater fc n tycon)
  996 |       = do addDocString n doc
  997 |            syn <- get Syn
  998 |            pure $ MkImpLater fc n !(bindTypeNames fc (usingImpl syn)
  999 |                                                   ps !(desugar AnyExpr ps tycon))
 1000 | 
 1001 |   desugarField : {auto s : Ref Syn SyntaxInfo} ->
 1002 |                  {auto c : Ref Ctxt Defs} ->
 1003 |                  {auto u : Ref UST UState} ->
 1004 |                  {auto m : Ref MD Metadata} ->
 1005 |                  {auto o : Ref ROpts REPLOpts} ->
 1006 |                  List Name -> Namespace -> PField ->
 1007 |                  Core (List IField)
 1008 |   desugarField ps ns field
 1009 |       = flip Core.traverse field.names $ \n : WithFC Name => do
 1010 |            addDocStringNS ns n.val field.doc
 1011 |            addDocStringNS ns (toRF n.val) field.doc
 1012 |            syn <- get Syn
 1013 |            p' <- traverse (desugar AnyExpr ps) field.val.info
 1014 |            ty' <- bindTypeNames field.fc (usingImpl syn) ps !(desugar AnyExpr ps field.val.boundType)
 1015 |            pure (Mk [field.fc, field.rig, n] (MkPiBindData p' ty'))
 1016 | 
 1017 |         where
 1018 |           toRF : Name -> Name
 1019 |           toRF (UN (Basic n)) = UN (Field n)
 1020 |           toRF n = n
 1021 | 
 1022 |   export
 1023 |   desugarFnOpt : {auto s : Ref Syn SyntaxInfo} ->
 1024 |                  {auto c : Ref Ctxt Defs} ->
 1025 |                  {auto u : Ref UST UState} ->
 1026 |                  {auto m : Ref MD Metadata} ->
 1027 |                  {auto o : Ref ROpts REPLOpts} ->
 1028 |                  List Name -> PFnOpt -> Core FnOpt
 1029 |   desugarFnOpt ps (IFnOpt f) = pure f
 1030 |   desugarFnOpt ps (PForeign tms)
 1031 |       = do tms' <- traverse (desugar AnyExpr ps) tms
 1032 |            pure (ForeignFn tms')
 1033 |   desugarFnOpt ps (PForeignExport tms)
 1034 |       = do tms' <- traverse (desugar AnyExpr ps) tms
 1035 |            pure (ForeignExport tms')
 1036 | 
 1037 |   %inline
 1038 |   mapDesugarPiInfo : {auto s : Ref Syn SyntaxInfo} ->
 1039 |                      {auto c : Ref Ctxt Defs} ->
 1040 |                      {auto u : Ref UST UState} ->
 1041 |                      {auto m : Ref MD Metadata} ->
 1042 |                      {auto o : Ref ROpts REPLOpts} ->
 1043 |                      List Name -> PiInfo PTerm -> Core (PiInfo RawImp)
 1044 |   mapDesugarPiInfo ps = PiInfo.traverse (desugar AnyExpr ps)
 1045 | 
 1046 |   displayFixity : Maybe Visibility -> BindingModifier -> Fixity -> Nat -> OpStr -> String
 1047 |   displayFixity Nothing NotBinding fix prec op = "\{show fix} \{show prec} \{show op}"
 1048 |   displayFixity Nothing bind fix prec op = "\{show bind} \{show fix} \{show prec} \{show op}"
 1049 |   displayFixity (Just vis) NotBinding fix prec op = "\{show vis} \{show fix} \{show prec} \{show op}"
 1050 |   displayFixity (Just vis) bind fix prec op = "\{show vis} \{show bind} \{show fix} \{show prec} \{show op}"
 1051 | 
 1052 |   verifyTotalityModifiers : {auto c : Ref Ctxt Defs} ->
 1053 |                             FC -> List FnOpt -> Core ()
 1054 |   verifyTotalityModifiers fc opts =
 1055 |     when (count isTotalityReq opts > 1) $ do
 1056 |       let totalities = sort $ mapMaybe extractTotality opts
 1057 |       let dedupTotalities = dedup totalities
 1058 |       defaultTotality <- getDefaultTotalityOption
 1059 |       throw $ GenericMsgSol fc "Multiple totality modifiers" "Possible solutions" $
 1060 |         catMaybes $
 1061 |           [ checkDuplicates totalities dedupTotalities
 1062 |           , checkCompability dedupTotalities
 1063 |           , checkDefault defaultTotality dedupTotalities
 1064 |           ]
 1065 |     where
 1066 |       showModifiers : Show a => List a -> String
 1067 |       showModifiers = concat . intersperse ", " . map (\s => "`\{show s}`")
 1068 | 
 1069 |       checkCompability : List TotalReq -> Maybe String
 1070 |       checkCompability totalities =
 1071 |         toMaybe (length totalities > 1) $
 1072 |           "Leave only one modifier out of " ++ showModifiers totalities
 1073 | 
 1074 |       checkDuplicates : List TotalReq -> List TotalReq -> Maybe String
 1075 |       checkDuplicates totalities dedupTotalities =
 1076 |         toMaybe (totalities /= dedupTotalities) $ do
 1077 |           let repeated = filter (\x => count (x ==) totalities > 1) dedupTotalities
 1078 |           "Remove duplicates of " ++ showModifiers repeated
 1079 | 
 1080 |       checkDefault : TotalReq -> List TotalReq -> Maybe String
 1081 |       checkDefault def totalities =
 1082 |         toMaybe (def `elem` totalities) $
 1083 |           "Remove modifiers " ++ showModifiers totalities ++
 1084 |           ", resulting in the default totality of " ++ showModifiers [def]
 1085 | 
 1086 |   -- Given a high level declaration, return a list of TTImp declarations
 1087 |   -- which process it, and update any necessary state on the way.
 1088 |   export
 1089 |   desugarDecl : {auto s : Ref Syn SyntaxInfo} ->
 1090 |                 {auto c : Ref Ctxt Defs} ->
 1091 |                 {auto u : Ref UST UState} ->
 1092 |                 {auto m : Ref MD Metadata} ->
 1093 |                 {auto o : Ref ROpts REPLOpts} ->
 1094 |                 List Name -> PDecl -> Core (List ImpDecl)
 1095 |   desugarDecl ps claim@(MkWithData _ (PClaim (MkPClaim rig vis fnopts ty)))
 1096 |       = do opts <- traverse (desugarFnOpt ps) fnopts
 1097 |            verifyTotalityModifiers claim.fc opts
 1098 | 
 1099 |            types <- desugarType ps ty
 1100 |            pure $ flip (map {f = List, b = ImpDecl}) types $ \ty' =>
 1101 |                       IClaim (MkFCVal claim.fc $ MkIClaimData rig vis opts ty')
 1102 | 
 1103 |   desugarDecl ps (MkWithData fc (PDef clauses))
 1104 |   -- The clauses won't necessarily all be from the same function, so split
 1105 |   -- after desugaring, by function name, using collectDefs from RawImp
 1106 |       = do ncs <- traverse (desugarClause ps False) clauses
 1107 |            defs <- traverse (uncurry $ toIDef . fromJust) ncs
 1108 |            pure (collectDefs defs)
 1109 |     where
 1110 |       toIDef : Name -> ImpClause -> Core ImpDecl
 1111 |       toIDef nm (PatClause fc lhs rhs)
 1112 |           = pure $ IDef fc nm [PatClause fc lhs rhs]
 1113 |       toIDef nm (WithClause fc lhs rig rhs prf flags cs)
 1114 |           = pure $ IDef fc nm [WithClause fc lhs rig rhs prf flags cs]
 1115 |       toIDef nm (ImpossibleClause fc lhs)
 1116 |           = pure $ IDef fc nm [ImpossibleClause fc lhs]
 1117 | 
 1118 |   desugarDecl ps dat@(MkWithData _ $ PData doc vis mbtot ddecl)
 1119 |       = pure [IData dat.fc vis mbtot !(desugarData ps doc ddecl)]
 1120 | 
 1121 |   desugarDecl ps pp@(MkWithData _ $ PParameters params pds)
 1122 |       = do
 1123 |            params' <- getArgs params
 1124 |            let paramList = forget params'
 1125 |            let paramNames = map (.name.val) paramList
 1126 |            pds' <- traverse (desugarDecl (ps ++ paramNames)) pds
 1127 |            -- Look for implicitly bindable names in the parameters
 1128 |            pnames <- ifThenElse (not !isUnboundImplicits) (pure [])
 1129 |              $ map concat
 1130 |              $ for (map (boundType . val) paramList)
 1131 |              $ findUniqueBindableNames pp.fc True (ps ++ paramNames) []
 1132 | 
 1133 |            let paramsb = map {f = List1} (map {f = WithData _} (mapType (doBind pnames))) params'
 1134 |            pure [IParameters pp.fc paramsb (concat pds')]
 1135 |       where
 1136 |         getArgs : Either (List1 PlainBinder)
 1137 |                          (List1 PBinder) ->
 1138 |                          Core (List1 (ImpParameter' RawImp))
 1139 |         getArgs (Left params)
 1140 |           = traverseList1 (\ty => do
 1141 |               ty' <- desugar AnyExpr ps ty.val
 1142 |               pure (Mk [top, ty.name] (MkPiBindData Explicit ty'))) params
 1143 |         getArgs (Right params)
 1144 |           = join <$> traverseList1 (\(MkPBinder info (MkBasicMultiBinder rig n ntm)) => do
 1145 |               tm' <- desugar AnyExpr ps ntm
 1146 |               i' <- traverse (desugar AnyExpr ps) info
 1147 |               let allbinders = map (\nn => Mk [rig, nn] (MkPiBindData i' tm')) n
 1148 |               pure allbinders) params
 1149 | 
 1150 |   desugarDecl ps use@(MkWithData _ $ PUsing uimpls uds)
 1151 |       = do syn <- get Syn
 1152 |            let oldu = usingImpl syn
 1153 |            uimpls' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd ntm)
 1154 |                                             btm <- bindTypeNames use.fc oldu ps tm'
 1155 |                                             pure (fst ntm, btm)) uimpls
 1156 |            put Syn ({ usingImpl := uimpls' ++ oldu } syn)
 1157 |            uds' <- traverse (desugarDecl ps) uds
 1158 |            update Syn { usingImpl := oldu }
 1159 |            pure (concat uds')
 1160 |   desugarDecl ps int@(MkWithData _ $ PInterface vis cons_in tn doc params det conname body)
 1161 |       = do addDocString tn doc
 1162 |            let paramNames = concatMap (map val . forget . names) params
 1163 | 
 1164 |            let cons = concatMap expandConstraint cons_in
 1165 |            cons' <- traverse (\ ntm => do tm' <- desugar AnyExpr (ps ++ paramNames)
 1166 |                                                          (snd ntm)
 1167 |                                           pure (fst ntm, tm')) cons
 1168 |            params' : List (WithFC Name, RigCount, RawImp) <-
 1169 |                         map concat $ for params $ \ (MkBasicMultiBinder rig nm tm) =>
 1170 |                            do tm' <- desugar AnyExpr ps tm
 1171 |                               pure $ map (, rig, tm') (forget nm)
 1172 |            -- Look for bindable names in all the constraints and parameters
 1173 |            let mnames = map dropNS (definedIn (map val body))
 1174 |            bnames <- ifThenElse (not !isUnboundImplicits) (pure [])
 1175 |              $ map concat
 1176 |              $ for (map Builtin.snd cons' ++ map (snd . snd) params')
 1177 |              $ findUniqueBindableNames int.fc True (ps ++ mnames ++ paramNames) []
 1178 | 
 1179 |            let paramsb = map (\ (nm, (rig, tm)) =>
 1180 |                                  let tm' = doBind bnames tm in
 1181 |                                  (nm.val, (rig, tm')))
 1182 |                          params'
 1183 |            let consb = map (\ (nm, tm) => (nm, doBind bnames tm)) cons'
 1184 | 
 1185 |            body' <- traverse (desugarDecl (ps ++ mnames ++ paramNames)) body
 1186 |            pure [IPragma int.fc (maybe [tn] (\n => [tn, n.val]) conname)
 1187 |                             (\nest, env =>
 1188 |                               elabInterface int.fc vis env nest consb
 1189 |                                             tn paramsb det conname
 1190 |                                             (concat body'))]
 1191 |     where
 1192 |       -- Turns pairs in the constraints to individual constraints. This
 1193 |       -- is a bit of a hack, but it's necessary to build parent constraint
 1194 |       -- chasing functions correctly
 1195 |       pairToCons : PTerm -> List PTerm
 1196 |       pairToCons (PPair _ l r) = pairToCons l ++ pairToCons r
 1197 |       pairToCons t = [t]
 1198 | 
 1199 |       expandConstraint : (Maybe Name, PTerm) -> List (Maybe Name, PTerm)
 1200 |       expandConstraint (Just n, t) = [(Just n, t)]
 1201 |       expandConstraint (Nothing, p)
 1202 |           = map (\x => (Nothing, x)) (pairToCons p)
 1203 | 
 1204 |   desugarDecl ps impl@(MkWithData _ $ PImplementation vis fnopts pass is cons tn params impln nusing body)
 1205 |       = do opts <- traverse (desugarFnOpt ps) fnopts
 1206 |            verifyTotalityModifiers impl.fc opts
 1207 | 
 1208 |            is' <- for is $ traverse (\ bind =>
 1209 |                      do tm' <- desugar AnyExpr ps bind.boundType
 1210 |                         pi' <- mapDesugarPiInfo ps bind.info
 1211 |                         pure (MkPiBindData pi' tm'))
 1212 |            cons' <- for cons $ \ (n, tm) =>
 1213 |                      do tm' <- desugar AnyExpr ps tm
 1214 |                         pure (n, tm')
 1215 |            params' : List RawImp <- traverse (desugar AnyExpr ps) params
 1216 |            -- Look for bindable names in all the constraints and parameters
 1217 |            bnames <- ifThenElse (not !isUnboundImplicits) (pure [])
 1218 |              $ map concat
 1219 |              $ for (map snd cons' ++ params')
 1220 |              $ findUniqueBindableNames impl.fc True ps []
 1221 | 
 1222 |            let paramsb = map (doBind bnames) params'
 1223 |            let isb = map (map (mapType (doBind bnames))) is'
 1224 |            let consb = map (map (doBind bnames)) cons'
 1225 | 
 1226 |            body' <- maybe (pure Nothing)
 1227 |                           (\b => do b' <- traverse (desugarDecl ps) b
 1228 |                                     pure (Just (concat b'))) body
 1229 |            -- calculate the name of the implementation, if it's not explicitly
 1230 |            -- given.
 1231 |            let impname = maybe (mkImplName impl.fc tn paramsb) id impln
 1232 | 
 1233 |            pure [IPragma impl.fc [impname]
 1234 |                             (\nest, env =>
 1235 |                                elabImplementation impl.fc vis opts pass env nest isb consb
 1236 |                                                   tn paramsb (isNamed impln)
 1237 |                                                   impname nusing
 1238 |                                                   body')]
 1239 |     where
 1240 |       isNamed : Maybe a -> Bool
 1241 |       isNamed Nothing = False
 1242 |       isNamed (Just _) = True
 1243 | 
 1244 |   desugarDecl ps rec@(MkWithData fc $ PRecord doc vis mbtot (MkPRecordLater tn params))
 1245 |       = desugarDecl ps (MkWithData fc $ PData doc vis mbtot (MkPLater rec.fc tn (mkRecType params)))
 1246 |     where
 1247 |       mkRecType : List PBinder -> PTerm
 1248 |       mkRecType [] = PType rec.fc
 1249 |       mkRecType (MkPBinder p (MkBasicMultiBinder c (n ::: []) t) :: ts)
 1250 |         = PPi rec.fc c p (Just n.val) t (mkRecType ts)
 1251 |       mkRecType (MkPBinder p (MkBasicMultiBinder c (n ::: x :: xs) t) :: ts)
 1252 |         = PPi rec.fc c p (Just n.val) t (mkRecType (MkPBinder p (MkBasicMultiBinder c (x ::: xs) t) :: ts))
 1253 |   desugarDecl ps rec@(MkWithData _ $ PRecord doc vis mbtot (MkPRecord tn params opts conname_in fields))
 1254 |       = do addDocString tn doc
 1255 |            params' : List ImpParameter <-
 1256 |               map concat $ for params $ \ (MkPBinder info (MkBasicMultiBinder rig names tm)) =>
 1257 |                  do tm' <- desugar AnyExpr ps tm
 1258 |                     p'  <- mapDesugarPiInfo ps info
 1259 |                     let allBinders = map (\nm => Mk [rig, nm] (MkPiBindData p' tm')) (forget names)
 1260 |                     pure allBinders
 1261 |            let fnames : List Name = concatMap getfname fields
 1262 |            let paramNames : List Name = concatMap (map val . forget . names . bind) params
 1263 | 
 1264 |            -- Look for bindable names in the parameters
 1265 |            let bnames : List (Name, Name) =
 1266 |                 if !isUnboundImplicits
 1267 |                    then concatMap (findBindableNames True (ps ++ fnames ++ paramNames) [])
 1268 |                                   (map (boundType . val) params')
 1269 |                    else []
 1270 | 
 1271 |            let paramsb : List ImpParameter = map (map $ mapType $ doBind bnames) params'
 1272 |            let recName = nameRoot tn
 1273 |            fields' : List (List IField) <- for fields (desugarField (ps ++ fnames ++ paramNames)
 1274 |                                                                     (mkNamespace recName))
 1275 |            let conname : Name = maybe (mkConName tn) val conname_in
 1276 |            whenJust (get "doc" <$> conname_in) (addDocString conname)
 1277 |            pure [IRecord rec.fc (Just recName)
 1278 |                          vis mbtot (Mk [rec.fc] $ MkImpRecord (Mk [NoFC tn] paramsb) (Mk [NoFC conname, opts] (concat fields')))]
 1279 |     where
 1280 |       getfname : PField -> List Name
 1281 |       getfname x = map val x.names
 1282 | 
 1283 |       mkConName : Name -> Name
 1284 |       mkConName (NS ns (UN n))
 1285 |         = let str = displayUserName n in
 1286 |           NS ns (DN str (MN ("__mk" ++ str) 0))
 1287 |       mkConName n = DN (show n) (MN ("__mk" ++ show n) 0)
 1288 | 
 1289 |   desugarDecl ps fx@(MkWithData _ $ PFixity (MkPFixityData vis binding fix prec opNames))
 1290 |       = flip (Core.traverseList1_ {b = Unit}) opNames (\opName : OpStr => do
 1291 |            unless (checkValidFixity binding fix prec)
 1292 |              (throw $ GenericMsgSol fx.fc
 1293 |                  "Invalid fixity, \{binding} operator must be infixr 0." "Possible solutions"
 1294 |                  [ "Make it `infixr 0`: `\{binding} infixr 0 \{show opName}`"
 1295 |                  , "Remove the binding keyword: `\{fix} \{show prec} \{show opName}`"
 1296 |                  ])
 1297 |            when (isDefaulted vis) $
 1298 |              let adjustedExport = displayFixity (Just Export) binding fix prec opName
 1299 |                  adjustedPrivate = displayFixity (Just Private) binding fix prec opName
 1300 |                  originalFixity = displayFixity Nothing binding fix prec opName
 1301 |              in recordWarning $ GenericWarn fx.fc """
 1302 |                Fixity declaration '\{originalFixity}' does not have an export modifier, and
 1303 |                will become private by default in a future version.
 1304 |                To expose it outside of its module, write '\{adjustedExport}'. If you
 1305 |                intend to keep it private, write '\{adjustedPrivate}'.
 1306 |                """
 1307 |            ctx <- get Ctxt
 1308 |            -- We update the context of fixities by adding a namespaced fixity
 1309 |            -- given by the current namespace and its fixity name.
 1310 |            -- This allows fixities to be stored along with the namespace at their
 1311 |            -- declaration site and detect and handle ambiguous fixities
 1312 |            let updatedNS = NS (mkNestedNamespace (Just ctx.currentNS) (show fix))
 1313 |                               (UN $ Basic $ nameRoot opName.toName)
 1314 | 
 1315 |            update Syn
 1316 |              { fixities $=
 1317 |                addName updatedNS
 1318 |                  (MkFixityInfo fx.fc (collapseDefault vis) binding fix prec) })
 1319 |         >> pure []
 1320 |   desugarDecl ps d@(MkWithData _ $ PFail mmsg ds)
 1321 |       = do -- save the state: the content of a failing block should be discarded
 1322 |            ust <- get UST
 1323 |            md <- get MD
 1324 |            opts <- get ROpts
 1325 |            syn <- get Syn
 1326 |            defs <- branch
 1327 |            log "desugar.failing" 20 $ "Desugaring the block:\n" ++ show d.val
 1328 |            -- See whether the desugaring phase fails and return
 1329 |            -- * Right ds                            if the desugaring succeeded
 1330 |            --                                       the error will have to come later in the pipeline
 1331 |            -- * Left Nothing                        if the block correctly failed
 1332 |            -- * Left (Just (FailingWrongError err)) if the block failed with the wrong error
 1333 |            result <- catch
 1334 |              (do -- run the desugarer
 1335 |                  ds <- traverse (desugarDecl ps) ds
 1336 |                  pure (Right (concat ds)))
 1337 |              (\err => do -- no message: any error will do
 1338 |                          let Just msg = mmsg
 1339 |                              | _ => pure (Left Nothing)
 1340 |                          -- otherwise have a look at the displayed message
 1341 |                          log "desugar.failing" 10 $ "Failing block based on \{show msg} failed with \{show err}"
 1342 |                          test <- checkError msg err
 1343 |                          pure $ Left $ do
 1344 |                               -- Unless the error is the expected one
 1345 |                               guard (not test)
 1346 |                               -- We should complain we had the wrong one
 1347 |                               pure (FailingWrongError d.fc msg (err ::: [])))
 1348 |            -- Reset the state
 1349 |            put UST ust
 1350 |            md' <- get MD
 1351 |            put MD ({ semanticHighlighting := semanticHighlighting md'
 1352 |                    , semanticAliases := semanticAliases md'
 1353 |                    , semanticDefaults := semanticDefaults md'
 1354 |                    } md)
 1355 |            put Syn syn
 1356 |            put Ctxt defs
 1357 |            -- either fail or return the block that should fail during the elab phase
 1358 |            case the (Either (Maybe Error) (List ImpDecl)) result of
 1359 |              Right ds => [IFail d.fc mmsg ds] <$ log "desugar.failing" 20 "Success"
 1360 |              Left Nothing => [] <$ log "desugar.failing" 20 "Correctly failed"
 1361 |              Left (Just err) => throw err
 1362 |   desugarDecl ps (MkWithData _ $ PMutual ds)
 1363 |       = do let (tys, defs) = splitMutual ds
 1364 |            mds' <- traverse (desugarDecl ps) (tys ++ defs)
 1365 |            pure (concat mds')
 1366 |   desugarDecl ps n@(MkWithData _ $ PNamespace ns decls)
 1367 |       = withExtendedNS ns $ do
 1368 |            ds <- traverse (desugarDecl ps) decls
 1369 |            pure [INamespace n.fc ns (concat ds)]
 1370 |   desugarDecl ps ts@(MkWithData _ $ PTransform n lhs rhs)
 1371 |       = do (bound, blhs) <- bindNames False !(desugar LHS ps lhs)
 1372 |            rhs' <- desugar AnyExpr (bound ++ ps) rhs
 1373 |            pure [ITransform ts.fc (UN $ Basic n) blhs rhs']
 1374 |   desugarDecl ps el@(MkWithData _ $ PRunElabDecl tm)
 1375 |       = do tm' <- desugar AnyExpr ps tm
 1376 |            pure [IRunElabDecl el.fc tm']
 1377 |   desugarDecl ps dir@(MkWithData _ $ PDirective d)
 1378 |       = let fc = dir.fc in case d of
 1379 |              Hide (HideName n) => pure [IPragma fc [] (\nest, env => hide fc n)]
 1380 |              Hide (HideFixity fx n) => pure [IPragma fc [] (\_, _ => removeFixity fc fx n)]
 1381 |              Unhide n => pure [IPragma fc [] (\nest, env => unhide fc n)]
 1382 |              Logging i => pure [ILog ((\ i => (topics i, verbosity i)) <$> i)]
 1383 |              LazyOn a => pure [IPragma fc [] (\nest, env => lazyActive a)]
 1384 |              UnboundImplicits a => do
 1385 |                setUnboundImplicits a
 1386 |                pure [IPragma fc [] (\nest, env => setUnboundImplicits a)]
 1387 |              PrefixRecordProjections b => do
 1388 |                pure [IPragma fc [] (\nest, env => setPrefixRecordProjections b)]
 1389 |              AmbigDepth n => pure [IPragma fc [] (\nest, env => setAmbigLimit n)]
 1390 |              TotalityDepth n => pure [IPragma fc [] (\next, env => setTotalLimit n)]
 1391 |              AutoImplicitDepth n => pure [IPragma fc [] (\nest, env => setAutoImplicitLimit n)]
 1392 |              NFMetavarThreshold n => pure [IPragma fc [] (\nest, env => setNFThreshold n)]
 1393 |              SearchTimeout n => pure [IPragma fc [] (\nest, env => setSearchTimeout n)]
 1394 |              PairNames ty f s => pure [IPragma fc [] (\nest, env => setPair fc ty f s)]
 1395 |              RewriteName eq rw => pure [IPragma fc [] (\nest, env => setRewrite fc eq rw)]
 1396 |              PrimInteger n => pure [IPragma fc [] (\nest, env => setFromInteger n)]
 1397 |              PrimString n => pure [IPragma fc [] (\nest, env => setFromString n)]
 1398 |              PrimChar n => pure [IPragma fc [] (\nest, env => setFromChar n)]
 1399 |              PrimDouble n => pure [IPragma fc [] (\nest, env => setFromDouble n)]
 1400 |              PrimTTImp n => pure [IPragma fc [] (\nest, env => setFromTTImp n)]
 1401 |              PrimName n => pure [IPragma fc [] (\nest, env => setFromName n)]
 1402 |              PrimDecls n => pure [IPragma fc [] (\nest, env => setFromDecls n)]
 1403 |              CGAction cg dir => pure [IPragma fc [] (\nest, env => addDirective cg dir)]
 1404 |              Names n ns => pure [IPragma fc [] (\nest, env => addNameDirective fc n ns)]
 1405 |              StartExpr tm => pure [IPragma fc [] (\nest, env => throw (InternalError "%start not implemented"))] -- TODO!
 1406 |              Overloadable n => pure [IPragma fc [] (\nest, env => setNameFlag fc n Overloadable)]
 1407 |              Extension e => pure [IPragma fc [] (\nest, env => setExtension e)]
 1408 |              DefaultTotality tot => pure [IPragma fc [] (\_, _ => setDefaultTotalityOption tot)]
 1409 |              ForeignImpl n cs => do
 1410 |                cs' <- traverse (desugar AnyExpr ps) cs
 1411 |                pure [IPragma fc [] (\nest, env => do
 1412 |                       defs <- get Ctxt
 1413 |                       calls <- traverse getFnString cs'
 1414 |                       [(n',_,gdef)] <- lookupCtxtName n (gamma defs)
 1415 |                         | [] => throw (UndefinedName fc n)
 1416 |                         | xs => throw (AmbiguousName fc (map fst xs))
 1417 |                       let ForeignDef arity xs = gdef.definition
 1418 |                         | _ => throw (GenericMsg fc "\{show n} is not a foreign definition")
 1419 | 
 1420 |                       update Ctxt { options->foreignImpl $= (map (n',) calls ++) }
 1421 |                     )]
 1422 |   desugarDecl ps bt@(MkWithData _ $ PBuiltin type name) = pure [IBuiltin bt.fc type name]
 1423 | 
 1424 |   export
 1425 |   desugarDo : {auto s : Ref Syn SyntaxInfo} ->
 1426 |               {auto c : Ref Ctxt Defs} ->
 1427 |               {auto m : Ref MD Metadata} ->
 1428 |               {auto u : Ref UST UState} ->
 1429 |               {auto o : Ref ROpts REPLOpts} ->
 1430 |               Side -> List Name -> Maybe Namespace -> PTerm -> Core RawImp
 1431 |   desugarDo s ps doNamespace tm
 1432 |       = do b <- newRef Bang (initBangs doNamespace)
 1433 |            tm' <- desugarB s ps tm
 1434 |            bd <- get Bang
 1435 |            pure $ bindBangs (bangNames bd) doNamespace tm'
 1436 | 
 1437 |   export
 1438 |   desugar : {auto s : Ref Syn SyntaxInfo} ->
 1439 |             {auto c : Ref Ctxt Defs} ->
 1440 |             {auto m : Ref MD Metadata} ->
 1441 |             {auto u : Ref UST UState} ->
 1442 |             {auto o : Ref ROpts REPLOpts} ->
 1443 |             Side -> List Name -> PTerm -> Core RawImp
 1444 | 
 1445 |   desugar s ps tm = desugarDo s ps Nothing tm
 1446 |