-- | This module contains functions for converting Haskell expressions to Coq.
module FreeC.Backend.Coq.Converter.Expr where

import           Control.Monad                    ( (>=>) )
import           Data.Maybe                       ( fromMaybe )

import qualified FreeC.Backend.Coq.Base           as Coq.Base
import           FreeC.Backend.Coq.Converter.Free
import           FreeC.Backend.Coq.Converter.Type
import qualified FreeC.Backend.Coq.Syntax         as Coq
import           FreeC.Environment.LookupOrFail
import qualified FreeC.IR.Syntax                  as IR
import           FreeC.LiftedIR.Converter.Expr
import qualified FreeC.LiftedIR.Syntax            as LIR
import           FreeC.Monad.Converter

-------------------------------------------------------------------------------
-- Expressions                                                               --
-------------------------------------------------------------------------------
-- | Converts a lifted IR expression to a Coq term.
convertLiftedExpr :: LIR.Expr -> Converter Coq.Term
convertLiftedExpr (LIR.Con srcSpan name) = do
  qualid <- lookupIdentOrFail srcSpan IR.ValueScope name
  return $ Coq.Qualid qualid
convertLiftedExpr (LIR.SmartCon srcSpan name) = do
  qualid <- lookupSmartIdentOrFail srcSpan name
  return $ Coq.Qualid qualid
convertLiftedExpr (LIR.Var _ _ _ qualid) = return $ Coq.Qualid qualid
convertLiftedExpr (LIR.App _ func typeArgs effects args freeArgs) = do
  func' : args' <- mapM convertLiftedExpr $ func : args
  typeArgs' <- mapM convertLiftedType typeArgs
  let explicitEffectArgs' = concatMap Coq.Base.selectExplicitArgs effects
      implicitEffectArgs' = concatMap Coq.Base.selectImplicitArgs effects
      implicitTypeArgs'   = concatMap
        (flip Coq.Base.selectTypedImplicitArgs $ length typeArgs) effects
  if freeArgs
    then return
      $ genericApply' func' explicitEffectArgs' implicitEffectArgs' typeArgs'
      implicitTypeArgs' args'
    else return $ Coq.app func' $ explicitEffectArgs' ++ args'
convertLiftedExpr (LIR.If _ cond true false) = do
  cond' <- convertLiftedExpr cond
  true' <- convertLiftedExpr true
  false' <- convertLiftedExpr false
  return $ Coq.If Coq.SymmetricIf cond' Nothing true' false'
convertLiftedExpr (LIR.Case _ expr alts) = do
  expr' <- convertLiftedExpr expr
  alts' <- mapM convertLiftedAlt alts
  return $ Coq.match expr' alts'
convertLiftedExpr (LIR.Undefined _)
  = return $ Coq.Qualid Coq.Base.partialUndefined
convertLiftedExpr (LIR.ErrorExpr _) = return $ Coq.Qualid Coq.Base.partialError
convertLiftedExpr (LIR.Trace _) = return $ Coq.Qualid Coq.Base.trace
convertLiftedExpr (LIR.IntLiteral _ value) = do
  let natValue = Coq.Num $ fromInteger (abs value)
      value'   | value < 0 = Coq.app (Coq.Qualid (Coq.bare "-")) [natValue]
               | otherwise = natValue
  return $ Coq.InScope value' Coq.Base.integerScope
convertLiftedExpr (LIR.StringLiteral _ str) = return
  $ Coq.InScope (Coq.string str) Coq.Base.stringScope
convertLiftedExpr (LIR.Lambda _ args rhs) = do
  let qualids  = map LIR.varPatCoqIdent args
      argTypes = map LIR.varPatType args
  argTypes' <- mapM (mapM convertLiftedType) argTypes
  rhs' <- convertLiftedExpr rhs
  return $ Coq.fun qualids argTypes' rhs'
convertLiftedExpr (LIR.Pure _ arg) = do
  arg' <- convertLiftedExpr arg
  generatePure arg'
convertLiftedExpr (LIR.Bind _ lhs rhs) = do
  lhs' <- convertLiftedExpr lhs
  rhs' <- convertLiftedExpr rhs
  return $ Coq.app (Coq.Qualid Coq.Base.freeBind) [lhs', rhs']
convertLiftedExpr (LIR.Share _ arg argType) = do
  arg' <- convertLiftedExpr arg
  argType' <- mapM convertLiftedType argType
  return
    $ genericApply' (Coq.Qualid Coq.Base.share)
    [Coq.Qualid Coq.Base.strategyArg] []
    [fromMaybe Coq.Base.implicitArg argType'] [Coq.Base.implicitArg] [arg']

-- | Converts a Haskell expression to Coq.
convertExpr :: IR.Expr -> Converter Coq.Term
convertExpr = liftExpr >=> convertLiftedExpr

-------------------------------------------------------------------------------
-- @case@ Expressions                                                        --
-------------------------------------------------------------------------------
-- Converts an alternative of a case expression in the lifted IR to Coq.
convertLiftedAlt :: LIR.Alt -> Converter Coq.Equation
convertLiftedAlt (LIR.Alt _ (LIR.ConPat srcSpan ident) varPats rhs) = do
  qualid <- lookupIdentOrFail srcSpan IR.ValueScope ident
  let varPats' = map (Coq.QualidPat . LIR.varPatCoqIdent) varPats
  rhs' <- convertLiftedExpr rhs
  return $ Coq.equation (Coq.ArgsPat qualid varPats') rhs'