<commit_before>{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections, LambdaCase, RecordWildCards,
             OverloadedStrings,
             ScopedTypeVariables,
             FlexibleContexts #-}

module HsToCoq.ConvertHaskell.Declarations.Instances (
  -- * Top-level entry point
  convertClsInstDecls,
  -- * Axiomatizing equivalents
  axiomatizeClsInstDecls,
) where

import Control.Lens

import Data.Semigroup (Semigroup(..), (<>))
import Data.Traversable
import HsToCoq.Util.Traversable
import Data.Maybe
import qualified Data.List.NonEmpty as NE
import Data.Bifunctor
import qualified Data.Text as T

import Control.Monad.State

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

import GHC hiding (Name)
import Bag
import HsToCoq.Util.GHC.Exception
import HsToCoq.Util.GHC.Module

import HsToCoq.Coq.Gallina
import HsToCoq.Coq.FreeVars
import HsToCoq.Coq.Subst
import HsToCoq.Coq.Gallina.Util

import HsToCoq.ConvertHaskell.Monad
import HsToCoq.ConvertHaskell.TypeInfo
import HsToCoq.ConvertHaskell.Definitions
import HsToCoq.ConvertHaskell.Parameters.Edits
import HsToCoq.ConvertHaskell.Type
import HsToCoq.ConvertHaskell.Expr
import HsToCoq.ConvertHaskell.Axiomatize
import HsToCoq.ConvertHaskell.Declarations.Class

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

-- Take the instance head and make it into a valid identifier.
convertInstanceName :: ConversionMonad r m => LHsType GhcRn -> m Qualid
convertInstanceName n = do
    coqType <- convertLType n
    qual <- Qualified . moduleNameText <$> view currentModule
    case skip coqType of
        Left err -> convUnsupported $ "Cannot derive instance name from " ++ show coqType ++ ": " ++ err
        Right name -> return $ qual name
  where
    -- Skip type vaiables and constraints
    skip (Forall _ t)  = skip t
    skip (Arrow _ t)   = skip t
    skip (InScope t _) = skip t
    skip t             = bfToName <$> bfTerm t

    bfToName :: [Qualid] -> T.Text
    bfToName qids | isVanilla = name
                  | otherwise = name <> "__" <> T.pack (show shapeNum)
      where
        tyCons = [ bn | Just bn <- unTyCon <$> qids]
        name = T.intercalate "__" tyCons
        shapeNum = bitsToInt $ map isTyCon qids

        -- A vanilla header is when all tyCons appear before all
        -- type variables. In this case, do not add the shapeNum
        isVanilla = not $ any isTyCon $ dropWhile isTyCon $ qids

        isTyCon = isJust . unTyCon

        unTyCon :: Qualid -> Maybe T.Text
        unTyCon (Qualified _ base)  = Just base
        unTyCon (Bare "bool")       = Just "bool"
        unTyCon (Bare "comparison") = Just "comparison"
        unTyCon (Bare "list")       = Just "list"
        unTyCon (Bare "option")     = Just "option"
        unTyCon (Bare "op_zt__")    = Just "op_zt__"
        unTyCon (Bare "unit")       = Just "unit"
        unTyCon _                   = Nothing

        bitsToInt :: [Bool] -> Integer
        bitsToInt []         = 0
        bitsToInt (True:xs)  = 2*bitsToInt xs + 1
        bitsToInt (False:xs) = 2*bitsToInt xs

    -- Breadth-first traversal listing all variables and type constructors
    bfTerm :: Monad m => Term -> m [Qualid]
    bfTerm = fmap concat . go
      where
        go :: Monad m => Term -> m [[Qualid]]
        go t = do
            (f, args) <- collectArgs t
            subtrees <- mapM go args
            return $ [f] : foldr merge [] subtrees

    merge :: [[a]] -> [[a]] -> [[a]]
    merge xs     []     = xs
    merge []     ys     = ys
    merge (x:xs) (y:ys) = (x ++ y) : merge xs ys

--------------------------------------------------------------------------------
{- Haskell:
      instance Functor ((->) r)
   InstanceInfo
      Name = "Functor__arr_r___"
      Head = "Functor (_(->)_ r)" as a Coq term, with free variable
      Class = "Functor"

   Haskell:
      instance Eq a => Eq [a]
   InstanceInfo
      Name = "Eq_list____"
      Head = "forall `{Eq a}, Eq (list a)"
      Class = "Eq"

-}
data InstanceInfo = InstanceInfo { instanceName       :: !Qualid
                                 , instanceHead       :: !Term
                                 , instanceClass      :: !Qualid
                                 }
                  deriving (Eq, Ord)

convertClsInstDeclInfo :: ConversionMonad r m => ClsInstDecl GhcRn -> m InstanceInfo
convertClsInstDeclInfo ClsInstDecl{..} = do
  instanceName  <- convertInstanceName $ hsib_body cid_poly_ty
  instanceHead  <- convertLHsSigType cid_poly_ty
  instanceClass <- maybe (convUnsupported "strangely-formed instance heads") pure $
                    termHead instanceHead

  pure InstanceInfo{..}

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

unlessSkipped :: ConversionMonad r m => InstanceInfo -> m [Sentence] -> m [Sentence]
unlessSkipped (InstanceInfo{..}) act = do
  view (edits.skipped.contains instanceClass) >>= \case
    True -> pure [ CommentSentence (Comment ("Skipping instance " <> qualidBase instanceName <> " of class " <> qualidBase instanceClass)) ]
    False -> do
      view (edits.skipped.contains instanceName) >>= \case
        True -> pure [ CommentSentence (Comment ("Skipping instance " <> qualidBase instanceName)) ]
        False -> act

convertClsInstDecl :: ConversionMonad r m => ClsInstDecl GhcRn -> m [Sentence]
convertClsInstDecl cid@ClsInstDecl{..} = do
  ii@InstanceInfo{..} <- convertClsInstDeclInfo cid

  let err_handler exn = pure [ translationFailedComment ("instance " <> qualidBase instanceName) exn ]
  unlessSkipped ii $ ghandle err_handler $ do
    cbinds <- fmap catMaybes $ mapM (convertTypedModuleBinding Nothing) $ map unLoc $ bagToList cid_binds
    cdefs <-  forM cbinds $ \case
        ConvertedDefinitionBinding (ConvertedDefinition{..})
            -> return (convDefName, maybe id Fun (NE.nonEmpty (convDefArgs)) $ convDefBody)
        ConvertedPatternBinding{} -> convUnsupported "pattern bindings in instances"

    defaults <-  fromMaybe M.empty <$> lookupDefaultMethods instanceClass
                 -- lookup default methods in the global state, using the
                 -- empty map if the class name is not found
                 -- otherwise gives you a map
                 -- <&> is flip fmap
             <&> filter (\(meth, _) -> isNothing $ lookup meth cdefs) . M.toList

    -- implement the instance part of "skip method"
    skippedMethodsS <- view (edits.skippedMethods)

    let methods = filter (\(m,_) -> (instanceClass,qualidBase m) `S.notMember` skippedMethodsS) (cdefs ++ defaults)

    let (binds, classTy) = decomposeForall instanceHead

    -- decomposeClassTy can fail, so run it in the monad so that
    -- failure will be caugh cause the instance to be skipped
    (className, instTy) <- decomposeClassTy classTy

    topoSortInstance instanceName binds className instTy methods


axiomatizeClsInstDecl :: ConversionMonad r m
                      => ClsInstDecl GhcRn        -- Haskell instance we are converting
                      -> m [Sentence]
axiomatizeClsInstDecl cid@ClsInstDecl{..} = do
  ii@InstanceInfo{..} <- convertClsInstDeclInfo cid
  unlessSkipped ii $ do
      lookupClassDefn instanceClass >>= \case
        Just (ClassDefinition _ _ _ methods) ->
          pure $ [ InstanceSentence $ InstanceDefinition instanceName [] instanceHead []
                                    $ if null methods then Nothing else Just $ ProofAdmitted "" ]
        Nothing ->
          -- convUnsupported ("OOPS! Cannot find information for class " ++ show instanceClass)
          pure []

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

convertClsInstDecls, axiomatizeClsInstDecls :: forall r m. ConversionMonad r m =>
    [ClsInstDecl GhcRn] -> m [Sentence]
convertClsInstDecls = foldTraverse convertClsInstDecl<commit_msg>typo in comments<commit_after>{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections, LambdaCase, RecordWildCards,
             OverloadedStrings,
             ScopedTypeVariables,
             FlexibleContexts #-}

module HsToCoq.ConvertHaskell.Declarations.Instances (
  -- * Top-level entry point
  convertClsInstDecls,
  -- * Axiomatizing equivalents
  axiomatizeClsInstDecls,
) where

import Control.Lens

import Data.Semigroup (Semigroup(..), (<>))
import Data.Traversable
import HsToCoq.Util.Traversable
import Data.Maybe
import qualified Data.List.NonEmpty as NE
import Data.Bifunctor
import qualified Data.Text as T

import Control.Monad.State

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

import GHC hiding (Name)
import Bag
import HsToCoq.Util.GHC.Exception
import HsToCoq.Util.GHC.Module

import HsToCoq.Coq.Gallina
import HsToCoq.Coq.FreeVars
import HsToCoq.Coq.Subst
import HsToCoq.Coq.Gallina.Util

import HsToCoq.ConvertHaskell.Monad
import HsToCoq.ConvertHaskell.TypeInfo
import HsToCoq.ConvertHaskell.Definitions
import HsToCoq.ConvertHaskell.Parameters.Edits
import HsToCoq.ConvertHaskell.Type
import HsToCoq.ConvertHaskell.Expr
import HsToCoq.ConvertHaskell.Axiomatize
import HsToCoq.ConvertHaskell.Declarations.Class

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

-- Take the instance head and make it into a valid identifier.
convertInstanceName :: ConversionMonad r m => LHsType GhcRn -> m Qualid
convertInstanceName n = do
    coqType <- convertLType n
    qual <- Qualified . moduleNameText <$> view currentModule
    case skip coqType of
        Left err -> convUnsupported $ "Cannot derive instance name from " ++ show coqType ++ ": " ++ err
        Right name -> return $ qual name
  where
    -- Skip type vaiables and constraints
    skip (Forall _ t)  = skip t
    skip (Arrow _ t)   = skip t
    skip (InScope t _) = skip t
    skip t             = bfToName <$> bfTerm t

    bfToName :: [Qualid] -> T.Text
    bfToName qids | isVanilla = name
                  | otherwise = name <> "__" <> T.pack (show shapeNum)
      where
        tyCons = [ bn | Just bn <- unTyCon <$> qids]
        name = T.intercalate "__" tyCons
        shapeNum = bitsToInt $ map isTyCon qids

        -- A vanilla header is when all tyCons appear before all
        -- type variables. In this case, do not add the shapeNum
        isVanilla = not $ any isTyCon $ dropWhile isTyCon $ qids

        isTyCon = isJust . unTyCon

        unTyCon :: Qualid -> Maybe T.Text
        unTyCon (Qualified _ base)  = Just base
        unTyCon (Bare "bool")       = Just "bool"
        unTyCon (Bare "comparison") = Just "comparison"
        unTyCon (Bare "list")       = Just "list"
        unTyCon (Bare "option")     = Just "option"
        unTyCon (Bare "op_zt__")    = Just "op_zt__"
        unTyCon (Bare "unit")       = Just "unit"
        unTyCon _                   = Nothing

        bitsToInt :: [Bool] -> Integer
        bitsToInt []         = 0
        bitsToInt (True:xs)  = 2*bitsToInt xs + 1
        bitsToInt (False:xs) = 2*bitsToInt xs

    -- Breadth-first traversal listing all variables and type constructors
    bfTerm :: Monad m => Term -> m [Qualid]
    bfTerm = fmap concat . go
      where
        go :: Monad m => Term -> m [[Qualid]]
        go t = do
            (f, args) <- collectArgs t
            subtrees <- mapM go args
            return $ [f] : foldr merge [] subtrees

    merge :: [[a]] -> [[a]] -> [[a]]
    merge xs     []     = xs
    merge []     ys     = ys
    merge (x:xs) (y:ys) = (x ++ y) : merge xs ys

--------------------------------------------------------------------------------
{- Haskell:
      instance Functor ((->) r)
   InstanceInfo
      Name = "Functor__arr_r___"
      Head = "Functor (_(->)_ r)" as a Coq term, with free variable
      Class = "Functor"

   Haskell:
      instance Eq a => Eq [a]
   InstanceInfo
      Name = "Eq_list____"
      Head = "forall `{Eq a}, Eq (list a)"
      Class = "Eq"

-}
data InstanceInfo = InstanceInfo { instanceName       :: !Qualid
                                 , instanceHead       :: !Term
                                 , instanceClass      :: !Qualid
                                 }
                  deriving (Eq, Ord)

convertClsInstDeclInfo :: ConversionMonad r m => ClsInstDecl GhcRn -> m InstanceInfo
convertClsInstDeclInfo ClsInstDecl{..} = do
  instanceName  <- convertInstanceName $ hsib_body cid_poly_ty
  instanceHead  <- convertLHsSigType cid_poly_ty
  instanceClass <- maybe (convUnsupported "strangely-formed instance heads") pure $
                    termHead instanceHead

  pure InstanceInfo{..}

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

unlessSkipped :: ConversionMonad r m => InstanceInfo -> m [Sentence] -> m [Sentence]
unlessSkipped (InstanceInfo{..}) act = do
  view (edits.skipped.contains instanceClass) >>= \case
    True -> pure [ CommentSentence (Comment ("Skipping instance " <> qualidBase instanceName <> " of class " <> qualidBase instanceClass)) ]
    False -> do
      view (edits.skipped.contains instanceName) >>= \case
        True -> pure [ CommentSentence (Comment ("Skipping instance " <> qualidBase instanceName)) ]
        False -> act

convertClsInstDecl :: ConversionMonad r m => ClsInstDecl GhcRn -> m [Sentence]
convertClsInstDecl cid@ClsInstDecl{..} = do
  ii@InstanceInfo{..} <- convertClsInstDeclInfo cid

  let err_handler exn = pure [ translationFailedComment ("instance " <> qualidBase instanceName) exn ]
  unlessSkipped ii $ ghandle err_handler $ do
    cbinds <- fmap catMaybes $ mapM (convertTypedModuleBinding Nothing) $ map unLoc $ bagToList cid_binds
    cdefs <-  forM cbinds $ \case
        ConvertedDefinitionBinding (ConvertedDefinition{..})
            -> return (convDefName, maybe id Fun (NE.nonEmpty (convDefArgs)) $ convDefBody)
        ConvertedPatternBinding{} -> convUnsupported "pattern bindings in instances"

    defaults <-  fromMaybe M.empty <$> lookupDefaultMethods instanceClass
                 -- lookup default methods in the global state, using the
                 -- empty map if the class name is not found
                 -- otherwise gives you a map
                 -- <&> is flip fmap
             <&> filter (\(meth, _) -> isNothing $ lookup meth cdefs) . M.toList

    -- implement the instance part of "skip method"
    skippedMethodsS <- view (edits.skippedMethods)

    let methods = filter (\(m,_) -> (instanceClass,qualidBase m) `S.notMember` skippedMethodsS) (cdefs ++ defaults)

    let (binds, classTy) = decomposeForall instanceHead

    -- decomposeClassTy can fail, so run it in the monad so that
    -- failure will be caught and cause the instance to be skipped
    (className, instTy) <- decomposeClassTy classTy

    topoSortInstance instanceName binds className instTy methods


axiomatizeClsInstDecl :: ConversionMonad r m
                      => ClsInstDecl GhcRn        -- Haskell instance we are converting
                      -> m [Sentence]
axiomatizeClsInstDecl cid@ClsInstDecl{..} = do
  ii@InstanceInfo{..} <- convertClsInstDeclInfo cid
  unlessSkipped ii $ do
      lookupClassDefn instanceClass >>= \case
        Just (ClassDefinition _ _ _ methods) ->
          pure $ [ InstanceSentence $ InstanceDefinition instanceName [] instanceHead []
                                    $ if null methods then Nothing else Just $ ProofAdmitted "" ]
        Nothing ->
          -- convUnsupported ("OOPS! Cannot find information for class " ++ show instanceClass)
          pure []

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

convertClsInstDecls, axiomatizeClsInstDecls :: forall r m. ConversionMonad r m =>
    [ClsInstDecl GhcRn] -> m [Sentence]
convertClsInstDecls = foldTraverse convertClsInstDecl
{'fraction_non_alphanumeric': 0.13052872394509404, 'fraction_numerical': 0.0005083884087442806, 'mean_word_length': 2.186917780477926, 'pattern_counts': {'":': 2, '<': 61, '<?xml version=': 0, '>': 117, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 8, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5759169', 'n_tokens_mistral': 4760, 'n_tokens_neox': 4579, 'n_words': 1362}