content: module Agda2Hs.Compile.Term where
  
  import Control.Arrow ( (>>>), (&&&), second )
  import Control.Monad ( zipWithM )
  import Control.Monad.Except
  import Control.Monad.Reader
  
  import Data.Foldable ( toList )
  import Data.Functor ( ($>) )
  import Data.List ( isPrefixOf )
  import Data.Maybe ( fromMaybe, isJust )
  import qualified Data.Text as Text ( unpack )
  import qualified Data.Set as Set ( singleton )
  
  import Agda.Syntax.Common.Pretty ( prettyShow )
  import qualified Agda.Syntax.Common.Pretty as P
  import Agda.Syntax.Common
  import Agda.Syntax.Literal
  import Agda.Syntax.Internal
  
  import Agda.TypeChecking.CheckInternal ( infer )
  import Agda.TypeChecking.Constraints ( noConstraints )
  import Agda.TypeChecking.Conversion ( equalTerm )
  import Agda.TypeChecking.InstanceArguments ( findInstance )
  import Agda.TypeChecking.MetaVars ( newInstanceMeta )
  import Agda.TypeChecking.Monad
  import Agda.TypeChecking.Pretty
  import Agda.TypeChecking.Records ( shouldBeProjectible, isRecordType, recordFieldNames )
  import Agda.TypeChecking.Datatypes ( getConType )
  import Agda.TypeChecking.Reduce ( unfoldDefinitionStep, instantiate, reduce )
  import Agda.TypeChecking.Substitute
  import Agda.TypeChecking.Telescope ( telView, mustBePi, piApplyM, flattenTel )
  import Agda.TypeChecking.ProjectionLike ( reduceProjectionLike )
  
  import Agda.Utils.Lens
  import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
  import Agda.Utils.Maybe
  import Agda.Utils.Monad
  import Agda.Utils.Size
  
  import Agda2Hs.AgdaUtils
  import Agda2Hs.Compile.Name ( compileQName, importInstance )
  
  import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileTelSize )
  import Agda2Hs.Compile.Types
  import Agda2Hs.Compile.Utils
  import Agda2Hs.Compile.Var ( compileDBVar )
  
  import qualified Agda2Hs.Language.Haskell as Hs
  import Agda2Hs.Language.Haskell.Utils
    ( hsName, pp, eApp, hsLambda, hsUnqualName, hsVar )
  
  import {-# SOURCE #-} Agda2Hs.Compile.Function ( compileClause' )
  import qualified Data.List as L
  
  
  -- * Compilation of special definitions
  
  type DefCompileRule = Type -> [Term] -> C (Hs.Exp ())
  
  isSpecialDef :: QName -> Maybe DefCompileRule
  isSpecialDef q = case prettyShow q of
    _ | isExtendedLambdaName q     -> Just (lambdaCase q)
    "Haskell.Prim.if_then_else_"   -> Just ifThenElse
    "Haskell.Prim.case_of_"        -> Just caseOf
    "Haskell.Prim.the"             -> Just expTypeSig
    "Haskell.Extra.Delay.runDelay" -> Just compileErasedApp
    "Agda.Builtin.Word.primWord64FromNat" -> Just primWord64FromNat
    _                              -> Nothing
  
  
  -- | Compile a @\where@ to the equivalent @\case@ expression.
  lambdaCase :: QName -> DefCompileRule
  lambdaCase q ty args = compileLocal $ setCurrentRangeQ q $ do
    Function
      { funClauses = cls
      , funExtLam  = Just ExtLamInfo {extLamModule = mname}
      } <- theDef <$> getConstInfo q
  
    npars <- size <$> lookupSection mname
  
    let (pars, rest) = splitAt npars args
        cs           = applys cls pars
  
    ty' <- piApplyM ty pars
  
    cs <- mapMaybeM (compileClause' mname (Just q) (hsName "(lambdaCase)") ty') cs
  
    case cs of
      -- If there is a single clause and all proper patterns got erased,
      -- we turn the remaining arguments into normal lambdas.
      [Hs.Match _ _ ps (Hs.UnGuardedRhs _ rhs) _]
        | null ps -> return rhs
        | all isVarPat ps -> return $ Hs.Lambda () ps rhs
      _ -> do
        lcase <- hsLCase =<< mapM clauseToAlt cs -- Pattern lambdas cannot have where blocks
        eApp lcase <$> compileArgs ty' rest
        -- undefined -- compileApp lcase (undefined, undefined, rest)
  
    where
      isVarPat :: Hs.Pat () -> Bool
      isVarPat Hs.PVar{} = True
      isVarPat _ = False
  
  -- | Compile @if_then_else_@ to a Haskell @if ... then ... else ... @ expression.
  ifThenElse :: DefCompileRule
  ifThenElse ty args = compileArgs ty args >>= \case
    -- fully applied
    b : t : f : es' -> return $ Hs.If () b t f `eApp` es'
    -- partially applied
    _               -> agda2hsError "if_then_else_ must be fully applied"
  
  
  -- | Compile @case_of_@ to Haskell @\case@ expression.
  caseOf :: DefCompileRule
  caseOf ty args = compileArgs ty args >>= \case
    -- applied to pattern lambda (that we remove, hence decrementLCase)
    e : Hs.LCase _ alts : es' -> decrementLCase $> eApp (Hs.Case () e alts) es'
    -- applied to regular lambda
    e : Hs.Lambda _ (p : ps) b : es' ->
      let lam [] = id
          lam qs = Hs.Lambda () qs
      in return $ eApp (Hs.Case () e [Hs.Alt () p (Hs.UnGuardedRhs () $ lam ps b) Nothing]) es'
    _ -> agda2hsError "case_of_ must be fully applied to a lambda term"
  
  
  -- | Compile @the@ to an explicitly-annotated Haskell expression.
  expTypeSig :: DefCompileRule
  expTypeSig ty args@(_:typ:_:_) = do
      annot    <- compileType typ
      exp:args <- compileArgs ty args
      pure (Hs.ExpTypeSig () exp annot `eApp` args)
  expTypeSig _ _ = agda2hsError "`the` must be fully applied"
  
  primWord64FromNat :: DefCompileRule
  primWord64FromNat ty args = compileArgs ty args >>= \case
    -- literal
    n@Hs.Lit{} : _ -> return n
    -- anything else
    _ -> agda2hsError "primWord64FromNat must be applied to a literal"
  
  
  compileVar :: Int -> Type -> [Term] -> C (Hs.Exp ())
  compileVar i ty es = do
    reportSDoc "agda2hs.compile.term" 15 $ text "Reached variable"
    name <- compileDBVar i
    compileApp (hsVar name) ty es
  
  -- | Compile constructors, defs and vars by
  -- carefully moving projections out of elims and calling compileProj.
  compileSpined
        :: ([Term] -> C (Hs.Exp ()))  -- Compilation continuation
        -> (Elims -> Term)            -- Term begin constructed
        -> Type                       -- Type of term
        -> Elims                      -- Elims the term is applied to
        -> C (Hs.Exp ())
  compileSpined c tm ty [] = c []
  compileSpined c tm ty (e@(Proj o q):es) = do
    let t = tm []
    ty' <- shouldBeProjectible t ty o q
    compileSpined (compileProj q ty t ty') (tm . (e:)) ty' es
  compileSpined c tm ty (e@(Apply (unArg -> x)):es) = do
    (a, b) <- mustBePi ty
    compileSpined (c . (x:)) (tm . (e:)) (absApp b x) es
  compileSpined _ _ _ _ = __IMPOSSIBLE__
  
  -- | Compile a definition.
  compileDef :: QName -> Type -> [Term] -> C (Hs.Exp ())
  compileDef f ty args | Just sem <- isSpecialDef f = do
    reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of special function"
    sem ty args
  
  compileDef f ty args =
    ifM (isTransparentFunction f) (compileErasedApp ty args) $
    ifM (isInlinedFunction f) (compileInlineFunctionApp f ty args) $ do
      reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of regular function:" <+> prettyTCM f
  
      let defMod = qnameModule f
  
      minRecord <- asks minRecordName
      -- TODO: simplify this when Agda exposes where-provenance in 'Internal' syntax
      outerWhereModules <- asks whereModules
  
      (ty', args') <-
  
        -- if the function comes from a where-clause
        -- or is a class-method for the class we are currently defining,
        -- we drop the module parameters
        if defMod `elem` outerWhereModules || Just defMod == minRecord then do
          npars <- size <$> lookupSection defMod
          let (pars, rest) = splitAt npars args
          ty' <- piApplyM ty pars
          pure (ty', rest)
        else pure (ty, args)
  
      reportSDoc "agda2hs.compile.term" 15 $ text "module args" <+> prettyTCM ty'
      reportSDoc "agda2hs.compile.term" 15 $ text "args to def: " <+> prettyTCM args'
  
      hsName <- compileQName f
  
      compileApp (Hs.Var () hsName) ty' args'
  
  
  -- * Compilation of projection(-like) definitions
  
  type ProjCompileRule = Type -> Term -> Type -> [Term] -> C (Hs.Exp ())
  
  
  isSpecialProj :: QName -> Maybe ProjCompileRule
  isSpecialProj q = case prettyShow q of
    "Agda.Builtin.FromNat.Number.fromNat"         -> Just fromNat
    "Haskell.Prim.Enum.Enum.enumFrom"             -> Just mkEnumFrom
    "Haskell.Prim.Enum.Enum.enumFromTo"           -> Just mkEnumFromTo
    "Haskell.Prim.Enum.Enum.enumFromThen"         -> Just mkEnumFromThen
    "Haskell.Prim.Enum.Enum.enumFromThenTo"       -> Just mkEnumFromThenTo
    "Haskell.Prim.Monad.Do.Monad._>>=_"           -> Just monadBind
    "Haskell.Prim.Monad.Do.Monad._>>_"            -> Just monadSeq
    "Agda.Builtin.FromNeg.Negative.fromNeg"       -> Just fromNeg
    "Agda.Builtin.FromString.IsString.fromString" -> Just fromString
    _                                             -> Nothing
  
  
  compileClassFun :: QName -> ProjCompileRule
  compileClassFun q _ w ty args = do
    hf     <- compileQName q
    curMod <- currentModule
    unless (curMod `isLeChildModuleOf` qnameModule q) $ checkInstance w
    eApp (Hs.Var () hf) <$> compileArgs ty args
  
  compileTupleProjection :: QName -> Hs.Boxed -> ProjCompileRule
  compileTupleProjection f b wty w ty args = do
    -- TODO: avoid redoing all of this work each time
    -- by storing the fields of each tuple type somewhere
    when (b == Hs.Unboxed) $ agda2hsError "projecting from unboxed tuples is not allowed"
    reportSDoc "agda2hs.term.proj" 12 $ text "compiling tuple projection"
    (r, pars, def) <- lift $ fromMaybe __IMPOSSIBLE__ <$> isRecordType wty
    let fields = map unDom $ _recFields def
        fieldTypes = flattenTel $ _recTel def `apply` pars
    fname <- compileTupleFields fields fieldTypes >>= \case
      [f1,f2] | f == f1 -> return $ hsName "fst"
              | f == f2 -> return $ hsName "snd"
              | otherwise -> __IMPOSSIBLE__
      fs' -> agda2hsStringError $
        "cannot project from tuple with " ++ show (size fs') ++ " fields"
    cw <- compileTerm wty w
    cargs <- compileArgs ty args
    return $ eApp (Hs.Var () $ Hs.UnQual () fname) (cw:cargs)
  
    where
      compileTupleFields :: [QName] -> [Dom Type] -> C [QName]
      compileTupleFields fs tys = catMaybes <$> zipWithM compileTupleField fs tys
  
      compileTupleField :: QName -> Dom Type -> C (Maybe QName)
      compileTupleField f ty = compileDom ty >>= \case
        DODropped -> return Nothing
        DOTerm -> return (Just f)
        DOType -> agda2hsErrorM $ "illegal type field in tuple record:" <+> prettyTCM f
        DOInstance -> agda2hsErrorM $ "illegal instance field in tuple record:" <+> prettyTCM f
  
  
  -- | Compile a projection(-like) definition
  compileProj
    :: QName  -- ^ Name of the projection
    -> Type   -- ^ Type of the term the projection is being applied to
    -> Term   -- ^ Term the projection is being applied to
    -> Type   -- ^ Return type of the projection
    -> [Term] -- ^ Arguments the projection of the term is applied to
    -> C (Hs.Exp ())
  compileProj q tty t ty args | Just rule <- isSpecialProj q = rule tty t ty args
  compileProj q tty t ty args =
    -- unboxed projection: we drop the projection
    ifM (isJust <$> isUnboxProjection q) (eApp <$> compileTerm tty t <*> compileArgs ty args) $
    -- class projection: we check the instance and drop it
    ifM (isClassFunction q) (compileClassFun q tty t ty args) $
    ifJustM (isTupleProjection q) (\b -> compileTupleProjection q b tty t ty args) $
    do
    -- NOTE(flupe): maybe we want Dom Type for the record arg
      name <- compileQName q
      arg  <- compileTerm tty t
      compileApp (Hs.Var () name `eApp` [arg]) ty args
  
  -- | Utility for translating class methods to special Haskell counterpart.
  -- This runs an instance check.
  specialClassFunction :: ([Hs.Exp ()] -> Hs.Exp ()) -> ProjCompileRule
  specialClassFunction f = specialClassFunctionM (pure . f)
  
  specialClassFunctionM :: ([Hs.Exp ()] -> C (Hs.Exp ())) -> ProjCompileRule
  specialClassFunctionM f _ w ty args = checkInstance w >> (f =<< compileArgs ty args)
  
  specialClassFunction1 :: Hs.Exp () -> (Hs.Exp () -> Hs.Exp ()) -> ProjCompileRule
  specialClassFunction1 v f = specialClassFunction $ \case
    (a : es) -> f a `eApp` es
    []       -> v
  
  specialClassFunction2 :: Hs.Exp () -> (Hs.Exp () -> Hs.Exp () -> Hs.Exp ()) -> ProjCompileRule
  specialClassFunction2 v f = specialClassFunction $ \case
    (a : b : es) -> f a b `eApp` es
    es           -> v `eApp` es
  
  specialClassFunction3 :: Hs.Exp () -> (Hs.Exp () -> Hs.Exp () -> Hs.Exp () -> Hs.Exp ()) -> ProjCompileRule
  specialClassFunction3 v f = specialClassFunction $ \case
    (a : b : c : es) -> f a b c `eApp` es
    es               -> v `eApp` es
  
  -- Note: currently the second (instance) argument {{_ : Constraint n}}
  -- is compiled and then dropped here, ideally it would not be compiled
  -- at all.
  fromNat :: ProjCompileRule
  fromNat = specialClassFunction2 (hsVar "fromIntegral") $ \v _ -> case v of
    n@Hs.Lit{} -> n
    v          -> hsVar "fromIntegral" `eApp` [v]
  
  mkEnumFrom :: ProjCompileRule
  mkEnumFrom = specialClassFunction1 (hsVar "enumFrom") $ Hs.EnumFrom ()
  
  mkEnumFromTo :: ProjCompileRule
  mkEnumFromTo = specialClassFunction2 (hsVar "enumFromTo") $ Hs.EnumFromTo ()
  
  mkEnumFromThen :: ProjCompileRule
  mkEnumFromThen = specialClassFunction2 (hsVar "enumFromThen") $ Hs.EnumFromThen ()
  
  mkEnumFromThenTo :: ProjCompileRule
  mkEnumFromThenTo = specialClassFunction3 (hsVar "enumFromThenTo") $ Hs.EnumFromThenTo ()
  
  -- Same comment as for fromNat
  fromNeg :: ProjCompileRule
  fromNeg = specialClassFunction2 negFromIntegral $ \v _ -> case v of
    n@Hs.Lit{} -> Hs.NegApp () n
    v          -> negFromIntegral `eApp` [v]
    where
      negFromIntegral = hsVar "negate" `o` hsVar "fromIntegral"
      -- TODO: move this to HsUtils
      f `o` g = Hs.InfixApp () f (Hs.QVarOp () $ hsUnqualName "_._") g
  
  -- Same comment as for fromNat
  fromString :: ProjCompileRule
  fromString = specialClassFunction2 (hsVar "fromString") $ \v _ -> case v of
    s@Hs.Lit{} -> s
    v          -> hsVar "fromString" `eApp` [v]
  
  -- | Compile monadic bind operator _>>=_ to Haskell do notation.
  monadBind :: ProjCompileRule
  monadBind = specialClassFunctionM $ \case
    [u, Hs.Lambda _ [p] v] -> pure $ bind' u p v
    [u, Hs.LCase () [Hs.Alt () p (Hs.UnGuardedRhs () v) Nothing]] ->
      decrementLCase >> return (bind' u p v)
    vs -> pure $ hsVar "_>>=_" `eApp` vs
    where
      bind' :: Hs.Exp () -> Hs.Pat () -> Hs.Exp () -> Hs.Exp ()
      bind' u p v =
        let stmt1 = Hs.Generator () p u in
        case v of
          Hs.Do _ stmts -> Hs.Do () (stmt1 : stmts)
          _             -> Hs.Do () [stmt1, Hs.Qualifier () v]
  
  -- | Compile monadic bind operator _>>_ to Haskell do notation.
  monadSeq :: ProjCompileRule-- TElims -> C (Hs.Exp ())
  monadSeq = specialClassFunction $ \case
    (u : v : vs) -> do
      let stmt1 = Hs.Qualifier () u
      case v of
        Hs.Do _ stmts -> Hs.Do () (stmt1 : stmts)
        _             -> Hs.Do () [stmt1, Hs.Qualifier () v]
    vs -> hsVar "_>>_" `eApp` vs
  
  
  -- * Compilation of constructors
  
  type ConCompileRule = Type -> [Term] -> C (Hs.Exp ())
  
  -- | Custom compilation rules for special constructors.
  isSpecialCon :: QName -> Maybe ConCompileRule
  isSpecialCon = prettyShow >>> \case
    "Haskell.Prim.Tuple._,_"          -> Just tupleTerm
    "Haskell.Prim.Tuple._×_×_._,_,_"  -> Just tupleTerm
    "Haskell.Prim.Int.Int.int64"      -> Just int64Term
    "Haskell.Extra.Sigma._,_"         -> Just tupleTerm
    "Haskell.Extra.Erase.Erased"      -> Just erasedTerm
    "Haskell.Extra.Delay.Delay.now"   -> Just compileErasedApp
    "Haskell.Extra.Delay.Delay.later" -> Just compileErasedApp
    _                                 -> Nothing
  
  tupleTerm :: ConCompileRule
  tupleTerm = compileApp' (Hs.Tuple () Hs.Boxed)
  
  erasedTerm :: ConCompileRule
  erasedTerm _ _ = pure (Hs.Tuple () Hs.Boxed [])
  
  int64Term :: ConCompileRule
  int64Term ty args = compileArgs ty args >>= \case
    n@Hs.Lit{} : _ -> return n
    _ -> agda2hsError "int64 must be applied to a literal"
  
  -- | @compileErasedApp@ compiles the application of unboxed constructors
  -- and transparent functions.
  -- Precondition: at most one argument is preserved.
  compileErasedApp :: Type -> [Term] -> C (Hs.Exp ())
  compileErasedApp ty args = do
    reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of transparent function or erased unboxed constructor"
    reportSDoc "agda2hs.compile.term" 12 $ text "Args" <+> prettyTCM args
    reportSDoc "agda2hs.compile.term" 12 $ text "Type" <+> prettyTCM ty
    compileArgs ty args >>= \case
      []  -> return $ hsVar "id"
      [v] -> return v
      _   -> __IMPOSSIBLE__
  
  
  compileCon :: ConHead -> ConInfo -> Type -> [Term] -> C (Hs.Exp ())
  compileCon h i ty args = do
    let c = conName h
    ifJust  (isSpecialCon c)       (\semantics -> semantics ty args) $ do
    ifJustM (isUnboxConstructor c) (\_ -> compileErasedApp ty args)  $ do
    ifJustM (isTupleConstructor c) (\b -> compileTuple ty b args)    $ do
      info <- getConstInfo c
      -- the constructor may be a copy introduced by module application,
      -- therefore we need to find the original constructor
      if defCopy info then
        let Constructor{conSrcCon = ch'} = theDef info in
        compileCon ch' i ty args
      else do
        con <- Hs.Con () <$> compileQName c
        compileApp con ty args
  
  compileTuple :: Type -> Hs.Boxed -> [Term] -> C (Hs.Exp ())
  compileTuple ty b args = do
    tellUnboxedTuples b
    (ty', vs) <- compileArgs' ty args
    TelV tel _ <- telView ty'
    missing <- compileTelSize tel
    let given = size vs
    if -- No arguments: return unit constructor () or (# #)
       | given == 0 && missing == 0 -> return $
           Hs.Con () $ Hs.Special () $ case b of
             Hs.Boxed -> Hs.UnitCon ()
             Hs.Unboxed -> Hs.UnboxedSingleCon ()
       -- All arguments missing: return tuple constructor
       -- e.g. (,) or (#,#)
       | given == 0 -> return $
           Hs.Con () $ Hs.Special () $ Hs.TupleCon () b missing
       -- All arguments given: return tuple
       -- e.g. (v1 , v2) or (# v1 , v2 #)
       | missing == 0 -> return $ Hs.Tuple () b vs
       -- Some arguments given, some missing: return tuple section
       -- e.g. (v1 ,) or (# v1, #)
       | otherwise -> do
           tellExtension $ Hs.TupleSections
           return $ Hs.TupleSection () b $
             map Just vs ++ replicate missing Nothing
  
  
  
  -- * Term compilation
  
  compileTerm :: Type -> Term -> C (Hs.Exp ())
  compileTerm ty v = do
  
    reportSDoc "agda2hs.compile.term" 10  $ text "compiling term:" <+> prettyTCM v
  
    v <- instantiate v
  
    let bad s t = agda2hsErrorM $ vcat
          [ text "cannot compile" <+> text (s ++ ":")
          , nest 2 $ prettyTCM t
          ]
  
    reduceProjectionLike v >>= \case
  
      Def f es -> do
        ty <- defType <$> getConstInfo f
        compileSpined (compileDef f ty) (Def f) ty es
  
      Con ch ci es -> do
        Just ((_, _, _), ty) <- getConType ch ty
        compileSpined (compileCon ch ci ty) (Con ch ci) ty es
  
      Var i es     -> do
        ty <- typeOfBV i
        compileSpined (compileVar i ty) (Var i) ty es
  
      Lit l   -> compileLiteral l
  
      Lam v b -> compileLam ty v b
  
      v@Pi{} -> bad "function type" v
      v@Sort{} -> bad "sort type" v
      v@Level{} -> bad "level term" v
      v@MetaV{} -> bad "unsolved metavariable" v
      v@DontCare{} -> bad "irrelevant term" v
      v@Dummy{} -> bad "dummy term" v
  
  -- | Check whether a domain is usable on the Haskell side.
  --
  -- That is the case if:
  -- * it is usable on the Agda side (i.e neither erased nor irrelevant).
  -- * is not of sort Prop.
  usableDom :: Dom Type -> Bool
  usableDom dom | Prop _ <- getSort dom = False
  usableDom dom = usableModality dom
  
  
  compileLam :: Type -> ArgInfo -> Abs Term -> C (Hs.Exp ())
  compileLam ty argi abs = do
    reportSDoc "agda2hs.compile.term" 50 $ text "Reached lambda"
    (dom, cod) <- mustBePi ty
  
    -- unusable domain, we remove the lambda and compile the body only
    if not (usableDom dom) then
      addContext dom $ compileTerm (absBody cod) (absBody abs)
  
    -- usable domain, user-written lambda is preserved
    else if getOrigin argi == UserWritten then do
  
      when (patternInTeleName `isPrefixOf` absName abs) $ agda2hsError $
        "Record pattern translation not supported. Use a pattern matching lambda instead."
  
      reportSDoc "agda2hs.compile" 17 $ text "compiling regular lambda"
  
      let varName = absName abs
          ctxElt  = (varName,) <$> dom
  
      hsLambda varName <$> addContext ctxElt (compileTerm (absBody cod) (absBody abs))
  
    -- usable domain, generated lambda means we introduce a section
    else do
  
      let varName = absName abs
          ctxElt  = (varName,) <$> dom
  
      addContext ctxElt $ do
        x <- compileDBVar 0
        compileTerm (absBody cod) (absBody abs) <&> \case
          Hs.InfixApp () a op b | a == hsVar x ->
            if pp op == "-" then -- Jesper: no right section for minus, as Haskell parses this as negation!
              Hs.LeftSection () b (Hs.QConOp () $ Hs.UnQual () $ hsName "subtract")
            else
              Hs.RightSection () op b -- System-inserted visible lambdas can only come from sections
          body -> hsLambda x body
  
  
  -- | Compile the application of a function definition marked as inlinable.
  -- The provided arguments will get substituted in the function body, and the missing arguments
  -- will get quantified with lambdas.
  compileInlineFunctionApp :: QName -> Type -> [Term] -> C (Hs.Exp ())
  compileInlineFunctionApp f ty args = do
    reportSDoc "agda2hs.compile.term" 12 $ text "Compiling application of inline function"
  
    def <- getConstInfo f
  
    let ty' = defType def
    let Function{funClauses = cs} = theDef def
    let [Clause{namedClausePats = pats}] = filter (isJust . clauseBody) cs
  
    ty'' <- piApplyM ty args
    -- NOTE(flupe): very flimsy, there has to be a better way
    etaExpand (drop (length args) pats) ty' args >>= compileTerm ty''
  
    where
      -- inline functions can only have transparent constructor patterns and variable patterns
      extractPatName :: DeBruijnPattern -> ArgName
      extractPatName (VarP _ v) = dbPatVarName v
      extractPatName (ConP _ _ args) =
        let arg = namedThing $ unArg $ maybe __IMPOSSIBLE__ fst $ L.uncons $ filter (usableModality `and2M` visible) args
        in extractPatName arg
      extractPatName _ = __IMPOSSIBLE__
  
      extractName :: NamedArg DeBruijnPattern -> ArgName
      extractName (unArg -> np)
        | Just n <- nameOf np = rangedThing (woThing n)
        | otherwise = extractPatName (namedThing np)
  
      etaExpand :: NAPs -> Type -> [Term] -> C Term
      etaExpand [] ty args = do
        r <- liftReduce
              $ locallyReduceDefs (OnlyReduceDefs $ Set.singleton f)
              $ unfoldDefinitionStep (Def f [] `applys` args) f (Apply . defaultArg <$> args)
        case r of
          YesReduction _ t -> pure t
          _ -> agda2hsErrorM $ text "Could not reduce inline function" <+> prettyTCM f
  
      etaExpand (p:ps) ty args = do
        (dom, cod) <- mustBePi ty
        let ai = domInfo dom
        Lam ai . mkAbs (extractName p) <$> etaExpand ps (absBody cod) (raise 1 args ++ [ var 0 ])
  
  
  compileApp :: Hs.Exp () -> Type -> [Term] -> C (Hs.Exp ())
  compileApp = compileApp' . eApp
  
  compileApp' :: ([Hs.Exp ()] -> Hs.Exp ()) -> Type -> [Term] -> C (Hs.Exp ())
  compileApp' acc ty args = acc <$> compileArgs ty args
  
  -- | Compile a list of arguments applied to a function of the given type.
  compileArgs :: Type -> [Term] -> C [Hs.Exp ()]
  compileArgs ty args = snd <$> compileArgs' ty args
  
  compileArgs' :: Type -> [Term] -> C (Type, [Hs.Exp ()])
  compileArgs' ty [] = pure (ty, [])
  compileArgs' ty (x:xs) = do
    (a, b) <- mustBePi ty
    let rest = compileArgs' (absApp b x) xs
    compileDom a >>= \case
      DODropped  -> rest
      DOInstance -> checkInstance x *> rest
      DOType     -> checkValidType x *> rest
      DOTerm     -> second . (:) <$> compileTerm (unDom a) x <*> rest
  
  -- We check that type arguments compile to a valid Haskell type
  -- before dropping them, see issue #357.
  checkValidType :: Term -> C ()
  checkValidType x = noWriteImports (compileType x) *> return ()
  
  clauseToAlt :: Hs.Match () -> C (Hs.Alt ())
  clauseToAlt (Hs.Match _ _ [p] rhs wh) = pure $ Hs.Alt () p rhs wh
  clauseToAlt (Hs.Match _ _ ps _ _)     = agda2hsError "Pattern matching lambdas must take a single argument"
  clauseToAlt Hs.InfixMatch{}           = __IMPOSSIBLE__
  
  compileLiteral :: Literal -> C (Hs.Exp ())
  compileLiteral (LitNat n)    = return $ Hs.intE n
  compileLiteral (LitFloat d)  = return $ Hs.Lit () $ Hs.Frac () (toRational d) (show d)
  compileLiteral (LitWord64 w) = return $ Hs.Lit () $ Hs.PrimWord () (fromIntegral w) (show w)
  compileLiteral (LitChar c)   = return $ Hs.charE c
  compileLiteral (LitString t) = return $ Hs.Lit () $ Hs.String () s s
    where s = Text.unpack t
  compileLiteral l             = agda2hsErrorM $ text "bad term:" <?> prettyTCM (Lit l)
  
  
  checkInstance :: Term -> C ()
  checkInstance u = do
    reportSDoc "agda2hs.checkInstance" 12 $ text "checkInstance" <+> prettyTCM u
    reduce u >>= \case
      Var x es -> do
        unlessM (isInstance <$> domOfBV x) illegalInstance
        checkInstanceElims es
      Def f es -> do
        unlessM (isJust . defInstance <$> getConstInfo f) illegalInstance
        importInstance f
        checkInstanceElims es
    -- We need to compile applications of `fromNat`, `fromNeg`, and
    -- `fromString` where the constraint type is ⊤ or IsTrue .... Ideally
    -- this constraint would be marked as erased but this would involve
    -- changing Agda builtins.
      Con c _ _
        | prettyShow (conName c) == "Agda.Builtin.Unit.tt" ||
          prettyShow (conName c) == "Haskell.Prim.IsTrue.itsTrue" ||
          prettyShow (conName c) == "Haskell.Prim.IsFalse.itsFalse" -> return ()
      _ -> illegalInstance
  
    where
      illegalInstance :: C ()
      illegalInstance = do
        reportSDoc "agda2hs.checkInstance" 15 $ text "illegal instance: " <+> pretty u
        agda2hsErrorM $ text "illegal instance: " <+> prettyTCM u
  
      checkInstanceElims :: Elims -> C ()
      checkInstanceElims = mapM_ checkInstanceElim
  
      checkInstanceElim :: Elim -> C ()
      checkInstanceElim (Apply v) =
        when (isInstance v && usableQuantity v) $
          checkInstance $ unArg v
      checkInstanceElim IApply{} = illegalInstance
      checkInstanceElim (Proj _ f) =
        unlessM (isInstance . defArgInfo <$> getConstInfo f) illegalInstance
  