<commit_before>{-# LANGUAGE TupleSections, LambdaCase, RecordWildCards,
             OverloadedLists, OverloadedStrings,
             FlexibleContexts, RankNTypes, ScopedTypeVariables,
             ViewPatterns, MultiWayIf  #-}

module HsToCoq.ConvertHaskell.Expr (
  -- * Expressions
  convertExpr, convertLExpr,
  -- * Bindings
  convertLocalBinds,
  -- ** Generic
  convertTypedBindings, convertTypedModuleBindings, convertTypedBinding,
  -- * Functions, matches, and guards
  -- ** Functions
  convertFunction,
  -- ** Matches
  convertMatchGroup, convertMatch,
  -- ** `do' blocks and similar
  convertDoBlock, convertListComprehension,
  convertPatternBinding,
  ) where

import Control.Lens

import Data.Bifunctor
import Data.Traversable
import Data.Maybe
import Data.List (intercalate)
import HsToCoq.Util.List hiding (unsnoc)
import Data.List.NonEmpty (nonEmpty, NonEmpty)
import qualified Data.List.NonEmpty as NEL
import qualified HsToCoq.Util.List as NEL ((|>))
import Data.Text (Text)
import qualified Data.Text as T

import Control.Monad.Trans.Maybe
import Control.Monad.Except
import Control.Monad.Writer

import           Data.Map.Strict (Map)
import qualified Data.Set        as S
import qualified Data.Map.Strict as M

import GHC hiding (Name, HsChar, HsString, AsPat)
import qualified GHC
import Bag
import BasicTypes
import HsToCoq.Util.GHC.FastString
import RdrName
import HsToCoq.Util.GHC.Exception

import HsToCoq.Util.GHC
import HsToCoq.Util.GHC.Name hiding (Name)
import HsToCoq.Util.GHC.HsExpr
import HsToCoq.Coq.Gallina as Coq
import HsToCoq.Coq.Gallina.Util
import HsToCoq.Coq.Gallina.Rewrite as Coq
import HsToCoq.Coq.FreeVars

import HsToCoq.ConvertHaskell.Parameters.Edits
import HsToCoq.ConvertHaskell.Monad
import HsToCoq.ConvertHaskell.Variables
import HsToCoq.ConvertHaskell.Definitions
import HsToCoq.ConvertHaskell.Literals
import HsToCoq.ConvertHaskell.Type
import HsToCoq.ConvertHaskell.Pattern
import HsToCoq.ConvertHaskell.Sigs

--------------------------------------------------------------------------------

rewriteExpr :: ConversionMonad m => Term -> m Term
rewriteExpr tm = do
  rws <- use (edits.rewrites)
  return $ Coq.rewrite rws tm

convertExpr :: ConversionMonad m => HsExpr GHC.Name -> m Term
convertExpr hsExpr = convertExpr' hsExpr >>= rewriteExpr

convertExpr' :: ConversionMonad m => HsExpr GHC.Name -> m Term
convertExpr' (HsVar (L _ x)) =
  Qualid <$> var ExprNS x

convertExpr' (HsUnboundVar x) =
  Var <$> freeVar (unboundVarOcc x)

convertExpr' (HsRecFld fld) =
  Qualid <$> recordField fld

convertExpr' (HsOverLabel _) =
  convUnsupported "overloaded labels"

convertExpr' (HsIPVar _) =
  convUnsupported "implicit parameters"

convertExpr' (HsOverLit OverLit{..}) =
  case ol_val of
    HsIntegral   _src int -> App1 "GHC.Num.fromInteger" . Num <$> convertInteger "integer literals" int
    HsFractional fr  -> convertFractional fr
    HsIsString   _src str -> pure $ convertFastString str

convertExpr' (HsLit lit) =
  case lit of
    GHC.HsChar   _ c       -> pure $ HsChar c
    HsCharPrim   _ _       -> convUnsupported "`Char#' literals"
    GHC.HsString _ fs      -> pure $ convertFastString fs
    HsStringPrim _ _       -> convUnsupported "`Addr#' literals"
    HsInt        _ int     -> Num <$> convertInteger "`Integer' literals" int
    HsIntPrim    _ int     -> Num <$> convertInteger "`Integer' literals" int
    HsWordPrim   _ _       -> convUnsupported "`Word#' literals"
    HsInt64Prim  _ _       -> convUnsupported "`Int64#' literals"
    HsWord64Prim _ _       -> convUnsupported "`Word64#' literals"
    HsInteger    _ int _ty -> Num <$> convertInteger "`Integer' literals" int
    HsRat        _ _       -> convUnsupported "`Rational' literals"
    HsFloatPrim  _         -> convUnsupported "`Float#' literals"
    HsDoublePrim _         -> convUnsupported "`Double#' literals"

convertExpr' (HsLam mg) =
  uncurry Fun <$> convertFunction mg

convertExpr' (HsLamCase PlaceHolder mg) =
  uncurry Fun <$> convertFunction mg

convertExpr' (HsApp e1 e2) =
  App1 <$> convertLExpr e1 <*> convertLExpr e2

convertExpr' (HsAppType e1 _) =
  convertLExpr e1
--  convUnsupported "type applications"
--  SCW: just ignore them for now, and let the user figure it out.

convertExpr' (HsAppTypeOut _ _) =
  convUnsupported "`HsAppTypeOut' constructor"

convertExpr' (OpApp el eop _fixity er) =
  case eop of
    L _ (HsVar (L _ hsOp)) -> do
      op <- var ExprNS hsOp
      l  <- convertLExpr el
      r  <- convertLExpr er
      pure $ if
        | qualidIsOp op -> Infix l op r
        | otherwise     -> App2 (Qualid op) l r
    _ ->
      convUnsupported "non-variable infix operators"

convertExpr' (NegApp e1 _) =
  App1 <$> pure "GHC.Num.negate" <*> convertLExpr e1

convertExpr' (HsPar e) =
  Parens <$> convertLExpr e

convertExpr' (SectionL l opE) =
  convert_section (Just l) opE Nothing

convertExpr' (SectionR opE r) =
  convert_section Nothing opE (Just r)

-- TODO: Mark converted unboxed tuples specially?<commit_msg>Make GHC.Num.negate amenable to rewrite rules<commit_after>{-# LANGUAGE TupleSections, LambdaCase, RecordWildCards,
             OverloadedLists, OverloadedStrings,
             FlexibleContexts, RankNTypes, ScopedTypeVariables,
             ViewPatterns, MultiWayIf  #-}

module HsToCoq.ConvertHaskell.Expr (
  -- * Expressions
  convertExpr, convertLExpr,
  -- * Bindings
  convertLocalBinds,
  -- ** Generic
  convertTypedBindings, convertTypedModuleBindings, convertTypedBinding,
  -- * Functions, matches, and guards
  -- ** Functions
  convertFunction,
  -- ** Matches
  convertMatchGroup, convertMatch,
  -- ** `do' blocks and similar
  convertDoBlock, convertListComprehension,
  convertPatternBinding,
  ) where

import Control.Lens

import Data.Bifunctor
import Data.Traversable
import Data.Maybe
import Data.List (intercalate)
import HsToCoq.Util.List hiding (unsnoc)
import Data.List.NonEmpty (nonEmpty, NonEmpty)
import qualified Data.List.NonEmpty as NEL
import qualified HsToCoq.Util.List as NEL ((|>))
import Data.Text (Text)
import qualified Data.Text as T

import Control.Monad.Trans.Maybe
import Control.Monad.Except
import Control.Monad.Writer

import           Data.Map.Strict (Map)
import qualified Data.Set        as S
import qualified Data.Map.Strict as M

import GHC hiding (Name, HsChar, HsString, AsPat)
import qualified GHC
import Bag
import BasicTypes
import HsToCoq.Util.GHC.FastString
import RdrName
import HsToCoq.Util.GHC.Exception

import HsToCoq.Util.GHC
import HsToCoq.Util.GHC.Name hiding (Name)
import HsToCoq.Util.GHC.HsExpr
import HsToCoq.Coq.Gallina as Coq
import HsToCoq.Coq.Gallina.Util
import HsToCoq.Coq.Gallina.Rewrite as Coq
import HsToCoq.Coq.FreeVars

import HsToCoq.ConvertHaskell.Parameters.Edits
import HsToCoq.ConvertHaskell.Monad
import HsToCoq.ConvertHaskell.Variables
import HsToCoq.ConvertHaskell.Definitions
import HsToCoq.ConvertHaskell.Literals
import HsToCoq.ConvertHaskell.Type
import HsToCoq.ConvertHaskell.Pattern
import HsToCoq.ConvertHaskell.Sigs

--------------------------------------------------------------------------------

rewriteExpr :: ConversionMonad m => Term -> m Term
rewriteExpr tm = do
  rws <- use (edits.rewrites)
  return $ Coq.rewrite rws tm

convertExpr :: ConversionMonad m => HsExpr GHC.Name -> m Term
convertExpr hsExpr = convertExpr' hsExpr >>= rewriteExpr

convertExpr' :: ConversionMonad m => HsExpr GHC.Name -> m Term
convertExpr' (HsVar (L _ x)) =
  Qualid <$> var ExprNS x

convertExpr' (HsUnboundVar x) =
  Var <$> freeVar (unboundVarOcc x)

convertExpr' (HsRecFld fld) =
  Qualid <$> recordField fld

convertExpr' (HsOverLabel _) =
  convUnsupported "overloaded labels"

convertExpr' (HsIPVar _) =
  convUnsupported "implicit parameters"

convertExpr' (HsOverLit OverLit{..}) =
  case ol_val of
    HsIntegral   _src int -> App1 "GHC.Num.fromInteger" . Num <$> convertInteger "integer literals" int
    HsFractional fr  -> convertFractional fr
    HsIsString   _src str -> pure $ convertFastString str

convertExpr' (HsLit lit) =
  case lit of
    GHC.HsChar   _ c       -> pure $ HsChar c
    HsCharPrim   _ _       -> convUnsupported "`Char#' literals"
    GHC.HsString _ fs      -> pure $ convertFastString fs
    HsStringPrim _ _       -> convUnsupported "`Addr#' literals"
    HsInt        _ int     -> Num <$> convertInteger "`Integer' literals" int
    HsIntPrim    _ int     -> Num <$> convertInteger "`Integer' literals" int
    HsWordPrim   _ _       -> convUnsupported "`Word#' literals"
    HsInt64Prim  _ _       -> convUnsupported "`Int64#' literals"
    HsWord64Prim _ _       -> convUnsupported "`Word64#' literals"
    HsInteger    _ int _ty -> Num <$> convertInteger "`Integer' literals" int
    HsRat        _ _       -> convUnsupported "`Rational' literals"
    HsFloatPrim  _         -> convUnsupported "`Float#' literals"
    HsDoublePrim _         -> convUnsupported "`Double#' literals"

convertExpr' (HsLam mg) =
  uncurry Fun <$> convertFunction mg

convertExpr' (HsLamCase PlaceHolder mg) =
  uncurry Fun <$> convertFunction mg

convertExpr' (HsApp e1 e2) =
  App1 <$> convertLExpr e1 <*> convertLExpr e2

convertExpr' (HsAppType e1 _) =
  convertLExpr e1
--  convUnsupported "type applications"
--  SCW: just ignore them for now, and let the user figure it out.

convertExpr' (HsAppTypeOut _ _) =
  convUnsupported "`HsAppTypeOut' constructor"

convertExpr' (OpApp el eop _fixity er) =
  case eop of
    L _ (HsVar (L _ hsOp)) -> do
      op <- var ExprNS hsOp
      l  <- convertLExpr el
      r  <- convertLExpr er
      pure $ if
        | qualidIsOp op -> Infix l op r
        | otherwise     -> App2 (Qualid op) l r
    _ ->
      convUnsupported "non-variable infix operators"

convertExpr' (NegApp e1 _) =
  App1 <$> (pure "GHC.Num.negate" >>= rewriteExpr) <*> convertLExpr e1

convertExpr' (HsPar e) =
  Parens <$> convertLExpr e

convertExpr' (SectionL l opE) =
  convert_section (Just l) opE Nothing

convertExpr' (SectionR opE r) =
  convert_section Nothing opE (Just r)

-- TODO: Mark converted unboxed tuples specially?
{'fraction_non_alphanumeric': 0.10741255961844197, 'fraction_numerical': 0.00397456279809221, 'mean_word_length': 3.2939419795221845, 'pattern_counts': {'":': 0, '<': 39, '<?xml version=': 0, '>': 91, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1995775', 'n_tokens_mistral': 3514, 'n_tokens_neox': 3355, 'n_words': 893}