content: -- Copyright 2022 Google LLC
  --
  -- Use of this source code is governed by a BSD-style
  -- license that can be found in the LICENSE file or at
  -- https://developers.google.com/open-source/licenses/bsd
  
  -- The Dex parser is written in two distinct stages:
  -- - concrete syntax parsing using Megaparsec (in ConcreteSyntax.hs)
  -- - conversion of concrete syntax to abstract syntax (this file).
  --
  -- We separate these two stages to separate concerns: the concrete
  -- syntax deals with grouping (including keywords, primitives, and
  -- operator precedence), and the abstract syntax makes sure that the
  -- resulting grouping structures are actually valid Dex.
  --
  -- As an example of the difference, an input like
  --   4 + * 3
  -- produces a parse error at the concrete syntax stage: `+` and `*`
  -- are both infix operators, so cannot be juxtaposed like that.
  -- On the other hand, an input like
  --   def foo (x + y) = 4
  -- groups just fine, but produces a syntax error at the abstract syntax
  -- stage because `(x + y)` is not a valid pattern for a function argument.
  --
  -- A goal we hope to achieve with this separation is to make the
  -- concrete syntax relatively uniform: something like `:`, which
  -- denotes different bits of abstract syntax in different contexts,
  -- can nonetheless be given a definite operator precedence, and a
  -- reader of Dex should be able to know which substrings of input are
  -- the constitutents of the Dex grammar without having to fully parse
  -- it.
  --
  -- Another goal is more practical: deferring the abstract syntax to a
  -- separate traversal means the meaning of a grouping construct like
  -- `[]` can depend on what follows after it, without requiring the
  -- Megaparsec parser to have unbounded lookahead.  At the
  -- character-by-character level, we just parse "group surrounded by
  -- square brackets", and then the abstract syntax determines whether
  -- to interpret it as a table literal, a table pattern, or a class
  -- constraint, depending on where it appears and what follows.
  --
  -- The separation also turned out to split the code size of the old
  -- parser roughly in half, implying that each of the remaining pieces
  -- is less complex on its own.  This should make adjusting the syntax,
  -- for example to permit grouping parens in more places, that much
  -- easier.
  
  module AbstractSyntax (parseExpr, parseDecl, parseBlock, parseTopDeclRepl) where
  
  import Control.Category ((>>>))
  import Control.Monad (forM, when)
  import Data.Functor
  import Data.Either
  import Data.Maybe (catMaybes)
  import Data.Set qualified as S
  import Data.Text (Text)
  
  import ConcreteSyntax
  import Err
  import Name
  import PPrint
  import Types.Primitives
  import Types.Source
  import qualified Types.OpNames as P
  import Util
  
  -- === Converting concrete syntax to abstract syntax ===
  
  parseExpr :: Fallible m => GroupW -> m (UExpr VoidS)
  parseExpr e = liftSyntaxM $ expr e
  
  parseDecl :: Fallible m => CTopDeclW -> m (UTopDecl VoidS VoidS)
  parseDecl d = liftSyntaxM $ topDecl d
  
  parseBlock :: Fallible m => CSBlock -> m (UBlock VoidS)
  parseBlock b = liftSyntaxM $ block b
  
  liftSyntaxM :: Fallible m => SyntaxM a -> m a
  liftSyntaxM cont = liftExcept cont
  
  parseTopDeclRepl :: Text -> Maybe SourceBlock
  parseTopDeclRepl s = case sbContents b of
    UnParseable True _ -> Nothing
    _ -> case checkSourceBlockParses $ sbContents b of
      Success _ -> Just b
      Failure _ -> Nothing
    where b = mustParseSourceBlock s
  {-# SCC parseTopDeclRepl #-}
  
  checkSourceBlockParses :: SourceBlock' -> SyntaxM ()
  checkSourceBlockParses = \case
    TopDecl (WithSrcs _ _ (CSDecl ann (CExpr e)))-> do
      when (ann /= PlainLet) $ fail "Cannot annotate expressions"
      void $ expr e
    TopDecl d -> void $ topDecl d
    Command _ b -> void $ expr b
    DeclareForeign _ _ ty -> void $ expr ty
    DeclareCustomLinearization _ _ body -> void $ expr body
    Misc _ -> return ()
    UnParseable _ _ -> return ()
  
  -- === Converting concrete syntax to abstract syntax ===
  
  type SyntaxM = Except
  
  topDecl :: CTopDeclW -> SyntaxM (UTopDecl VoidS VoidS)
  topDecl (WithSrcs sid sids topDecl') = case topDecl' of
    CSDecl ann d -> ULocalDecl <$> decl ann (WithSrcs sid sids d)
    CData name tyConParams givens constructors -> do
      tyConParams' <- fromMaybeM tyConParams Empty aExplicitParams
      givens' <- aOptGivens givens
      constructors' <- forM constructors \(v, ps) -> do
        ps' <- fromMaybeM ps Empty \(WithSrcs _ _ ps') ->
          toNest <$> mapM (tyOptBinder Explicit) ps'
        return (v, ps')
      return $ UDataDefDecl
        (UDataDef (withoutSrc name) (givens' >>> tyConParams') $
          map (\(name', cons) -> (withoutSrc name', UDataDefTrail cons)) constructors')
        (fromSourceNameW name)
        (toNest $ map (fromSourceNameW . fst) constructors')
    CStruct name params givens fields defs -> do
      params' <- fromMaybeM params Empty aExplicitParams
      givens' <- aOptGivens givens
      fields' <- forM fields \(v, ty) -> (v,) <$> expr ty
      methods <- forM defs \(ann, d) -> do
        (WithSrc _ methodName, lam) <- aDef d
        return (ann, methodName, Abs (WithSrcB sid (UBindSource "self")) lam)
      return $ UStructDecl (fromSourceNameW name) (UStructDef (withoutSrc name) (givens' >>> params') fields' methods)
    CInterface name params methods -> do
      params' <- aExplicitParams params
      (methodNames, methodTys) <- unzip <$> forM methods \(methodName, ty) -> do
        ty' <- expr ty
        return (fromSourceNameW methodName, ty')
      return $ UInterface params' methodTys (fromSourceNameW name) (toNest methodNames)
    CInstanceDecl def -> aInstanceDef def
  
  decl :: LetAnn -> CSDeclW -> SyntaxM (UDecl VoidS VoidS)
  decl ann (WithSrcs sid _ d) = WithSrcB sid <$> case d of
    CLet binder rhs -> do
      (p, ty) <- patOptAnn binder
      ULet ann p ty <$> asExpr <$> block rhs
    CBind _ _ -> throw sid TopLevelArrowBinder
    CDefDecl def -> do
      (name, lam) <- aDef def
      return $ ULet ann (fromSourceNameW name) Nothing (WithSrcE sid (ULam lam))
    CExpr g -> UExprDecl <$> expr g
    CPass -> return UPass
  
  aInstanceDef :: CInstanceDef -> SyntaxM (UTopDecl VoidS VoidS)
  aInstanceDef (CInstanceDef (WithSrc clNameId clName) args givens methods instNameAndParams) = do
    let clName' = SourceName clNameId clName
    args' <- mapM expr args
    givens' <- aOptGivens givens
    methods' <- catMaybes <$> mapM aMethod methods
    case instNameAndParams of
      Nothing -> return $ UInstance clName' givens' args' methods' NothingB ImplicitApp
      Just (WithSrc sid instName, optParams) -> do
        let instName' = JustB $ WithSrcB sid $ UBindSource instName
        case optParams of
          Just params -> do
            params' <- aExplicitParams params
            return $ UInstance clName' (givens' >>> params') args' methods' instName' ExplicitApp
          Nothing -> return $ UInstance clName' givens' args' methods' instName' ImplicitApp
  
  aDef :: CDef -> SyntaxM (SourceNameW, ULamExpr VoidS)
  aDef (CDef name params optRhs optGivens body) = do
    explicitParams <- explicitBindersOptAnn params
    let rhsDefault = (ExplicitApp, Nothing, Nothing)
    (expl, effs, resultTy) <- fromMaybeM optRhs rhsDefault \(expl, optEffs, resultTy) -> do
      effs <- fromMaybeM optEffs UPure aEffects
      resultTy' <- expr resultTy
      return (expl, Just effs, Just resultTy')
    implicitParams <- aOptGivens optGivens
    let allParams = implicitParams >>> explicitParams
    body' <- block body
    return (name, ULamExpr allParams expl effs resultTy body')
  
  stripParens :: GroupW -> GroupW
  stripParens (WithSrcs _ _ (CParens [g])) = stripParens g
  stripParens g = g
  
  -- === combinators for different sorts of binder lists ===
  
  aOptGivens :: Maybe GivenClause -> SyntaxM (Nest UAnnBinder VoidS VoidS)
  aOptGivens optGivens = fromMaybeM optGivens Empty aGivens
  
  binderList
    :: [GroupW] -> (GroupW -> SyntaxM (Nest UAnnBinder VoidS VoidS))
    -> SyntaxM (Nest UAnnBinder VoidS VoidS)
  binderList gs cont = concatNests <$> forM gs \case
    WithSrcs _ _ (CGivens gs') -> aGivens gs'
    g -> cont g
  
  withTrailingConstraints
    :: GroupW -> (GroupW -> SyntaxM (UAnnBinder VoidS VoidS))
    -> SyntaxM (Nest UAnnBinder VoidS VoidS)
  withTrailingConstraints g cont = case g of
    WithSrcs _ _ (CBin Pipe lhs c) -> do
      Nest (UAnnBinder expl (WithSrcB sid b) ann cs) bs <- withTrailingConstraints lhs cont
      s <- case b of
        UBindSource s -> return s
        UIgnore       -> throw sid CantConstrainAnonBinders
        UBind _ _     -> error "Shouldn't have internal names until renaming pass"
      c' <- expr c
      return $   UnaryNest (UAnnBinder expl (WithSrcB sid b) ann (cs ++ [c']))
             >>> bs
             >>> UnaryNest (asConstraintBinder (mkUVar sid s) c')
    _ -> UnaryNest <$> cont g
    where
      asConstraintBinder :: UExpr VoidS -> UConstraint VoidS -> UAnnBinder VoidS VoidS
      asConstraintBinder v c = do
        let sid = srcPos c
        let t = WithSrcE sid (UApp c [v] [])
        UAnnBinder (Inferred Nothing (Synth Full)) (WithSrcB sid UIgnore) (UAnn t) []
  
  mkUVar :: SrcId -> SourceName -> UExpr VoidS
  mkUVar sid v = WithSrcE sid $ UVar $ SourceName sid v
  
  aGivens :: GivenClause -> SyntaxM (Nest UAnnBinder VoidS VoidS)
  aGivens ((WithSrcs _ _ implicits), optConstraints) = do
    implicits' <- concatNests <$> forM implicits \b -> withTrailingConstraints b implicitArgBinder
    constraints <- fromMaybeM optConstraints Empty (\(WithSrcs _ _ gs) -> toNest <$> mapM synthBinder gs)
    return $ implicits' >>> constraints
  
  synthBinder :: GroupW -> SyntaxM (UAnnBinder VoidS VoidS)
  synthBinder g = tyOptBinder (Inferred Nothing (Synth Full)) g
  
  concatNests :: [Nest b VoidS VoidS] -> Nest b VoidS VoidS
  concatNests [] = Empty
  concatNests (b:bs) = b >>> concatNests bs
  
  implicitArgBinder :: GroupW -> SyntaxM (UAnnBinder VoidS VoidS)
  implicitArgBinder g = do
    UAnnBinder _ b ann cs <- binderOptTy (Inferred Nothing Unify) g
    s <- case b of
      WithSrcB _ (UBindSource s) -> return $ Just s
      _             -> return Nothing
    return $ UAnnBinder (Inferred s Unify) b ann cs
  
  aExplicitParams :: ExplicitParams -> SyntaxM (Nest UAnnBinder VoidS VoidS)
  aExplicitParams (WithSrcs _ _ bs) = binderList bs \b -> withTrailingConstraints b \b' ->
    binderOptTy Explicit b'
  
  aPiBinders :: [GroupW] -> SyntaxM (Nest UAnnBinder VoidS VoidS)
  aPiBinders bs = binderList bs \b ->
    UnaryNest <$> tyOptBinder Explicit b
  
  explicitBindersOptAnn :: ExplicitParams -> SyntaxM (Nest UAnnBinder VoidS VoidS)
  explicitBindersOptAnn (WithSrcs _ _ bs) =
    binderList bs \b -> withTrailingConstraints b \b' -> binderOptTy Explicit b'
  
  -- ===
  
  -- Binder pattern with an optional type annotation
  patOptAnn :: GroupW -> SyntaxM (UPat VoidS VoidS, Maybe (UType VoidS))
  patOptAnn (WithSrcs _ _ (CBin Colon lhs typeAnn)) = (,) <$> pat lhs <*> (Just <$> expr typeAnn)
  patOptAnn (WithSrcs _ _ (CParens [g])) = patOptAnn g
  patOptAnn g = (,Nothing) <$> pat g
  
  uBinder :: GroupW -> SyntaxM (UBinder c VoidS VoidS)
  uBinder (WithSrcs sid _ b) = case b of
    CLeaf (CIdentifier name) -> return $ fromSourceNameW $ WithSrc sid name
    CLeaf CHole -> return $ WithSrcB sid UIgnore
    _ -> throw sid UnexpectedBinder
  
  -- Type annotation with an optional binder pattern
  tyOptPat :: GroupW -> SyntaxM (UAnnBinder VoidS VoidS)
  tyOptPat grpTop@(WithSrcs sid _ grp) = case grp of
    -- Named type
    CBin Colon lhs typeAnn ->
      UAnnBinder Explicit <$> uBinder lhs <*> (UAnn <$> expr typeAnn) <*> pure []
    -- Binder in grouping parens.
    CParens [g] -> tyOptPat g
    -- Anonymous type
    _ -> UAnnBinder Explicit (WithSrcB sid UIgnore) <$> (UAnn <$> expr grpTop) <*> pure []
  
  -- Pattern of a case binder.  This treats bare names specially, in
  -- that they become (nullary) constructors to match rather than names
  -- to bind.
  casePat :: GroupW -> SyntaxM (UPat VoidS VoidS)
  casePat = \case
    WithSrcs src _ (CLeaf (CIdentifier name)) ->
      return $ WithSrcB src $ UPatCon (fromSourceNameW (WithSrc src name)) Empty
    g -> pat g
  
  pat :: GroupW -> SyntaxM (UPat VoidS VoidS)
  pat (WithSrcs sid _ grp) = WithSrcB sid <$> case grp of
    CBin DepComma lhs rhs -> do
      lhs' <- pat lhs
      rhs' <- pat rhs
      return $ UPatDepPair $ PairB lhs' rhs'
    CBrackets gs -> UPatTable . toNest <$> (mapM pat gs)
    -- TODO: use Python-style trailing comma (like `(x,y,)`) for singleton tuples
    CParens gs -> case gs of
      [g] -> do
        WithSrcB _ g' <- casePat g
        return g'
      _   -> UPatProd . toNest <$> mapM pat gs
    CLeaf CHole -> return $ UPatBinder (WithSrcB sid UIgnore)
    CLeaf (CIdentifier name) -> return $ UPatBinder $ fromSourceNameW $ WithSrc sid name
    CJuxtapose True lhs rhs -> do
      case lhs of
        WithSrcs lhsId _ (CJuxtapose True _ _) -> throw lhsId OnlyUnaryWithoutParens
        _ -> return ()
      name <- identifier "pattern constructor name" lhs
      arg <- pat rhs
      return $ UPatCon (fromSourceNameW name) (UnaryNest arg)
    CJuxtapose False lhs rhs -> do
      name <- identifier "pattern constructor name" lhs
      case rhs of
        WithSrcs _ _ (CParens gs) -> do
          gs' <- mapM pat gs
          return $ UPatCon (fromSourceNameW name) (toNest gs')
        _ -> error "unexpected postfix group (should be ruled out at grouping stage)"
    _ -> throw sid IllegalPattern
  
  tyOptBinder :: Explicitness -> GroupW -> SyntaxM (UAnnBinder VoidS VoidS)
  tyOptBinder expl (WithSrcs sid sids grp) = case grp of
    CBin Pipe  _ rhs     -> throw (getSrcId rhs) UnexpectedConstraint
    CBin Colon name ty -> do
      b <- uBinder name
      ann <- UAnn <$> expr ty
      return $ UAnnBinder expl b ann []
    g -> do
      ty <- expr (WithSrcs sid sids g)
      return $ UAnnBinder expl (WithSrcB sid UIgnore) (UAnn ty) []
  
  binderOptTy :: Explicitness -> GroupW -> SyntaxM (UAnnBinder VoidS VoidS)
  binderOptTy expl = \case
    WithSrcs _ _ (CBin Colon name ty) -> do
      b <- uBinder name
      ann <- UAnn <$> expr ty
      return $ UAnnBinder expl b ann []
    g -> do
      b <- uBinder g
      return $ UAnnBinder expl b UNoAnn []
  
  binderReqTy :: Explicitness -> GroupW -> SyntaxM (UAnnBinder VoidS VoidS)
  binderReqTy expl (WithSrcs _ _ (CBin Colon name ty)) = do
    b <- uBinder name
    ann <- UAnn <$> expr ty
    return $ UAnnBinder expl b ann []
  binderReqTy _ g = throw (getSrcId g) ExpectedAnnBinder
  
  argList :: [GroupW] -> SyntaxM ([UExpr VoidS], [UNamedArg VoidS])
  argList gs = partitionEithers <$> mapM singleArg gs
  
  singleArg :: GroupW -> SyntaxM (Either (UExpr VoidS) (UNamedArg VoidS))
  singleArg = \case
    WithSrcs _ _ (CBin CSEqual lhs rhs) -> Right <$>
      ((,) <$> withoutSrc <$> identifier "named argument" lhs <*> expr rhs)
    g -> Left <$> expr g
  
  identifier :: String -> GroupW -> SyntaxM SourceNameW
  identifier ctx (WithSrcs sid _ g) = case g of
    CLeaf (CIdentifier name) -> return $ WithSrc sid name
    _ -> throw sid $ ExpectedIdentifier ctx
  
  aEffects :: WithSrcs ([GroupW], Maybe GroupW) -> SyntaxM (UEffectRow VoidS)
  aEffects (WithSrcs _ _ (effs, optEffTail)) = do
    lhs <- mapM effect effs
    rhs <- forM optEffTail \effTail ->
      fromSourceNameW <$> identifier "effect row remainder variable" effTail
    return $ UEffectRow (S.fromList lhs) rhs
  
  effect :: GroupW -> SyntaxM (UEffect VoidS)
  effect (WithSrcs grpSid _ grp) = case grp of
    CParens [g] -> effect g
    CJuxtapose True (Identifier "Read" ) (WithSrcs sid _ (CLeaf (CIdentifier h))) ->
      return $ URWSEffect Reader $ fromSourceNameW (WithSrc sid h)
    CJuxtapose True (Identifier "Accum") (WithSrcs sid _ (CLeaf (CIdentifier h))) ->
      return $ URWSEffect Writer $ fromSourceNameW (WithSrc sid h)
    CJuxtapose True (Identifier "State") (WithSrcs sid _ (CLeaf (CIdentifier h))) ->
      return $ URWSEffect State $ fromSourceNameW (WithSrc sid h)
    CLeaf (CIdentifier "Except") -> return UExceptionEffect
    CLeaf (CIdentifier "IO"    ) -> return UIOEffect
    _ -> throw grpSid UnexpectedEffectForm
  
  aMethod :: CSDeclW -> SyntaxM (Maybe (UMethodDef VoidS))
  aMethod (WithSrcs _ _ CPass) = return Nothing
  aMethod (WithSrcs sid _ d) = Just . WithSrcE sid <$> case d of
    CDefDecl def -> do
      (WithSrc nameSid name, lam) <- aDef def
      return $ UMethodDef (SourceName nameSid name) lam
    CLet (WithSrcs lhsSid _ (CLeaf (CIdentifier name))) rhs -> do
      rhs' <- ULamExpr Empty ImplicitApp Nothing Nothing <$> block rhs
      return $ UMethodDef (fromSourceNameW (WithSrc lhsSid name)) rhs'
    _ -> throw sid UnexpectedMethodDef
  
  asExpr :: UBlock VoidS -> UExpr VoidS
  asExpr (WithSrcE src b) = case b of
    UBlock Empty e -> e
    _ -> WithSrcE src $ UDo $ WithSrcE src b
  
  block :: CSBlock -> SyntaxM (UBlock VoidS)
  block (ExprBlock g) = WithSrcE (srcPos g) . UBlock Empty <$> expr g
  block (IndentedBlock sid decls) = do
    (decls', result) <- blockDecls decls
    return $ WithSrcE sid $ UBlock decls' result
  
  blockDecls :: [CSDeclW] -> SyntaxM (Nest UDecl VoidS VoidS, UExpr VoidS)
  blockDecls [] = error "shouldn't have empty list of decls"
  blockDecls [WithSrcs sid _ d] = case d of
    CExpr g -> (Empty,) <$> expr g
    _ -> throw sid BlockWithoutFinalExpr
  blockDecls (WithSrcs sid _ (CBind b rhs):ds) = do
    b' <- binderOptTy Explicit b
    rhs' <- asExpr <$> block rhs
    body <- block $ IndentedBlock sid ds -- Not really the right SrcId
    let lam = ULam $ ULamExpr (UnaryNest b') ExplicitApp Nothing Nothing body
    return (Empty, WithSrcE sid $ extendAppRight rhs' (WithSrcE sid lam))
  blockDecls (d:ds) = do
    d' <- decl PlainLet d
    (ds', e) <- blockDecls ds
    return (Nest d' ds', e)
  
  -- === Concrete to abstract syntax of expressions ===
  
  expr :: GroupW -> SyntaxM (UExpr VoidS)
  expr (WithSrcs sid sids grp) = WithSrcE sid <$> case grp of
    CLeaf x -> leaf sid x
    CPrim prim xs     -> UPrim prim <$> mapM expr xs
    CParens [g] -> do
      WithSrcE _ result <- expr g
      return result
    CParens gs -> UPrim UTuple <$> mapM expr gs
    -- Table constructors here.  Other uses of square brackets
    -- should be detected upstream, before calling expr.
    CBrackets gs -> UTabCon <$> mapM expr gs
    CGivens _ -> throw sid UnexpectedGivenClause
    CArrow lhs effs rhs -> do
      case lhs of
        WithSrcs _ _ (CParens gs) -> do
          bs <- aPiBinders gs
          effs' <- fromMaybeM effs UPure aEffects
          resultTy <- expr rhs
          return $ UPi $ UPiExpr bs ExplicitApp effs' resultTy
        WithSrcs lhsSid _ _ -> throw lhsSid ArgsShouldHaveParens
    CDo b -> UDo <$> block b
    CJuxtapose hasSpace lhs rhs -> case hasSpace of
      True -> extendAppRight <$> expr lhs <*> expr rhs
      False -> do
        f <- expr lhs
        case rhs of
          WithSrcs _ _ (CParens args) -> do
            (posArgs, namedArgs) <- argList args
            return $ UApp f posArgs namedArgs
          WithSrcs _ _ (CBrackets args) -> do
            args' <- mapM expr args
            return $ UTabApp f args'
          _ -> error "unexpected postfix group (should be ruled out at grouping stage)"
    CBin op lhs rhs -> case op of
      Dollar -> extendAppRight <$> expr lhs <*> expr rhs
      Pipe   -> extendAppLeft  <$> expr lhs <*> expr rhs
      Dot -> do
        lhs' <- expr lhs
        WithSrcs rhsSid _ rhs' <- return rhs
        name <- case rhs' of
          CLeaf (CIdentifier name) -> return $ FieldName name
          CLeaf (CNat i          ) -> return $ FieldNum $ fromIntegral i
          _ -> throw rhsSid BadField
        return $ UFieldAccess lhs' (WithSrc rhsSid name)
      DoubleColon   -> UTypeAnn <$> (expr lhs) <*> expr rhs
      EvalBinOp (WithSrc opSid s) -> do
        let f = WithSrcE opSid (fromSourceNameW (WithSrc opSid s))
        lhs' <- expr lhs
        rhs' <- expr rhs
        return $ explicitApp f [lhs', rhs']
      DepAmpersand  -> do
        lhs' <- tyOptPat lhs
        UDepPairTy . (UDepPairType ExplicitDepPair lhs') <$> expr rhs
      DepComma      -> UDepPair <$> (expr lhs) <*> expr rhs
      CSEqual       -> throw errSid BadEqualSign
      Colon         -> throw errSid BadColon
      ImplicitArrow -> case lhs of
        WithSrcs _ _ (CParens gs) -> do
          bs <- aPiBinders gs
          resultTy <- expr rhs
          return $ UPi $ UPiExpr bs ImplicitApp UPure resultTy
        WithSrcs lhsSid _ _ -> throw lhsSid ArgsShouldHaveParens
      FatArrow      -> do
        lhs' <- tyOptPat lhs
        UTabPi . (UTabPiExpr lhs') <$> expr rhs
     where
       errSid = case sids of
         [sid'] -> sid'
         _ -> sid
    CPrefix (WithSrc prefixSid name) g -> do
      case name of
        "+" -> (withoutSrc <$> expr g) <&> \case
          UNatLit   i -> UIntLit   (fromIntegral i)
          UIntLit   i -> UIntLit   i
          UFloatLit i -> UFloatLit i
          e -> e
        "-" -> expr g <&> \case
          WithSrcE _ (UNatLit   i) -> UIntLit   (-(fromIntegral i))
          WithSrcE _ (UIntLit   i) -> UIntLit   (-i)
          WithSrcE _ (UFloatLit i) -> UFloatLit (-i)
          e -> unaryApp (mkUVar prefixSid "neg") e
        _ -> throw prefixSid $ BadPrefix $ pprint name
    CLambda params body -> do
      params' <- explicitBindersOptAnn $ WithSrcs sid [] $ map stripParens params
      body' <- block body
      return $ ULam $ ULamExpr params' ExplicitApp Nothing Nothing body'
    CFor kind indices body -> do
      let (dir, trailingUnit) = case kind of
            KFor  -> (Fwd, False)
            KFor_ -> (Fwd, True)
            KRof  -> (Rev, False)
            KRof_ -> (Rev, True)
      -- TODO: Can we fetch the source position from the error context, to feed into `buildFor`?
      e <- buildFor sid dir <$> mapM (binderOptTy Explicit) indices <*> block body
      if trailingUnit
        then return $ UDo $ WithSrcE sid $ UBlock (UnaryNest (WithSrcB sid $ UExprDecl e)) (unitExpr sid)
        else return $ withoutSrc e
    CCase scrut alts -> UCase <$> (expr scrut) <*> mapM alternative alts
      where alternative (match, body) = UAlt <$> casePat match <*> block body
    CIf p c a -> do
      p' <- expr p
      c' <- block c
      a' <- case a of
        Nothing -> return $ WithSrcE sid $ UBlock Empty $ unitExpr sid
        (Just alternative) -> block alternative
      return $ UCase p'
        [ UAlt (WithSrcB sid $ UPatCon (SourceName sid "True")  Empty) c'
        , UAlt (WithSrcB sid $ UPatCon (SourceName sid "False") Empty) a']
    CWith lhs rhs -> do
      ty <- expr lhs
      case rhs of
        WithSrcs _ _ [b] -> do
          b' <- binderReqTy Explicit b
          return $ UDepPairTy $ UDepPairType ImplicitDepPair b' ty
        _ -> error "n-ary dependent pairs not implemented"
  
  leaf :: SrcId -> CLeaf -> SyntaxM (UExpr' VoidS)
  leaf sid = \case
    -- Binders (e.g., in pi types) should not hit this case
    CIdentifier name  -> return $ fromSourceNameW $ WithSrc sid name
    CNat word         -> return $ UNatLit word
    CInt int          -> return $ UIntLit int
    CString str       -> do
      xs <- return $ map (WithSrcE sid . charExpr) str
      let toListVar = mkUVar sid "to_list"
      return $ explicitApp toListVar [WithSrcE sid (UTabCon xs)]
    CChar char        -> return $ charExpr char
    CFloat num        -> return $ UFloatLit num
    CHole             -> return   UHole
  
  charExpr :: Char -> (UExpr' VoidS)
  charExpr c = ULit $ Word8Lit $ fromIntegral $ fromEnum c
  
  unitExpr :: SrcId -> UExpr VoidS
  unitExpr sid = WithSrcE sid $ UPrim (UCon $ P.ProdCon) []
  
  -- === Builders ===
  
  -- TODO Does this generalize?  Swap list for Nest?
  -- TODO: these SrcIds aren't really correct
  buildFor :: SrcId -> Direction -> [UAnnBinder VoidS VoidS] -> UBlock VoidS -> UExpr VoidS
  buildFor sid dir binders body = case binders of
    [] -> error "should have nonempty list of binder"
    [b] -> WithSrcE sid $ UFor dir $ UForExpr b body
    b:bs -> WithSrcE sid $ UFor dir $ UForExpr b $
      WithSrcE sid $ UBlock Empty $ buildFor sid dir bs body
  
  -- === Helpers ===
  
  extendAppRight :: UExpr n -> UExpr n -> UExpr' n
  extendAppRight (WithSrcE _ (UApp f args kwargs)) x = UApp f (args ++ [x]) kwargs
  extendAppRight f x = unaryApp f x
  
  extendAppLeft :: UExpr n -> UExpr n -> UExpr' n
  extendAppLeft x (WithSrcE _ (UApp f args kwargs)) = UApp f (x:args) kwargs
  extendAppLeft x f = unaryApp f x
  
  unaryApp :: UExpr n -> UExpr n -> UExpr' n
  unaryApp f x = UApp f [x] []
  
  explicitApp :: UExpr n -> [UExpr n] -> UExpr' n
  explicitApp f xs = UApp f xs []
  
  toNest :: [a VoidS VoidS] -> Nest a VoidS VoidS
  toNest = foldr Nest Empty
  