<commit_before>{-# LANGUAGE PatternGuards #-}

module Idris.Erasure (performUsageAnalysis) where

import Idris.AbsSyntax
import Idris.Core.CaseTree
import Idris.Core.TT
import Idris.Core.Evaluate
import Idris.Primitives
import Idris.Error

import Debug.Trace
import System.IO.Unsafe

import Control.Arrow
import Control.Applicative
import Control.Monad.State
import Data.Maybe
import Data.List
import qualified Data.Set as S
import qualified Data.IntSet as IS
import qualified Data.Map as M
import qualified Data.IntMap as IM
import Data.Set (Set)
import Data.IntSet (IntSet)
import Data.Map (Map)
import Data.IntMap (IntMap)
import Data.Text (pack)
import qualified Data.Text as T

-- UseMap maps names to the set of used (reachable) argument positions.
type UseMap = Map Name (IntMap (Set Reason))

data Arg = Arg !Int | Result deriving (Eq, Ord)

instance Show Arg where
    show (Arg i) = show i
    show Result  = "*"

type Node = (Name, Arg)
type Deps = Map Cond DepSet
type Reason = (Name, Int)  -- function name, argument index

-- Nodes along with sets of reasons for every one.
type DepSet = Map Node (Set Reason)

-- "Condition" is the conjunction
-- of elementary assumptions along the path from the root.
-- Elementary assumption (f, i) means that "function f uses the argument i".
type Cond = Set Node

-- Every variable draws in certain dependencies.
type Var = DepSet
type Vars = Map Name Var

-- Perform usage analysis, write the relevant information in the internal
-- structures, returning the list of reachable names.
performUsageAnalysis :: Idris [Name]
performUsageAnalysis = do
    ctx <- tt_ctxt <$> getIState

    case lookupCtxt mainName (definitions ctx) of
      [] -> return []  -- no main -> not compiling -> reachability irrelevant
      _  -> do
        ci  <- idris_classes <$> getIState
        cg  <- idris_callgraph <$> getIState
        opt <- idris_optimisation <$> getIState

        -- Build the dependency graph.
        let depMap = buildDepMap ci ctx mainName

        -- Search for reachable nodes in the graph.
        let (residDeps, (reachableNames, minUse)) = minimalUsage depMap
            usage = M.toList minUse

        -- Print some debug info.
        logLvl 3 $ "Reachable names:\n" ++ unlines (map (indent . show) . S.toList $ reachableNames)
        logLvl 4 $ "Minimal usage:\n" ++ fmtUseMap usage
        logLvl 5 $ "Residual deps:\n" ++ unlines (map fmtItem . M.toList $ residDeps)

        -- Check that everything reachable is accessible.
        mapM_ (checkAccessibility opt) usage

        -- Store the usage info in the internal state.
        mapM_ (storeUsage cg) usage

        return $ S.toList reachableNames
  where
    mainName = sNS (sUN "main") ["Main"]
    indent = ("  " ++)

    fmtItem :: (Cond, DepSet) -> String
    fmtItem (cond, deps) = indent $ show (S.toList cond) ++ " -> " ++ show (M.toList deps)

    fmtUseMap :: [(Name, IntMap (Set Reason))] -> String
    fmtUseMap = unlines . map (\(n,is) -> indent $ show n ++ " -> " ++ show (IM.toList is))

    storeUsage :: Ctxt CGInfo -> (Name, IntMap (Set Reason)) -> Idris ()
    storeUsage cg (n, args)
        | [x] <- lookupCtxt n cg
        = addToCG n x{ usedpos = flat }        -- functions

        | otherwise
        = addToCG n (CGInfo [] [] [] [] flat)  -- data ctors
      where
        flat = [(i, S.toList rs) | (i,rs) <- IM.toList args]

    checkAccessibility :: Ctxt OptInfo -> (Name, IntMap (Set Reason)) -> Idris ()
    checkAccessibility opt (n, reachable)
        | [Optimise col nt forc rec inaccessible] <- lookupCtxt n opt<commit_msg>Improve printing of UseMaps.<commit_after>{-# LANGUAGE PatternGuards #-}

module Idris.Erasure (performUsageAnalysis) where

import Idris.AbsSyntax
import Idris.Core.CaseTree
import Idris.Core.TT
import Idris.Core.Evaluate
import Idris.Primitives
import Idris.Error

import Debug.Trace
import System.IO.Unsafe

import Control.Arrow
import Control.Applicative
import Control.Monad.State
import Data.Maybe
import Data.List
import qualified Data.Set as S
import qualified Data.IntSet as IS
import qualified Data.Map as M
import qualified Data.IntMap as IM
import Data.Set (Set)
import Data.IntSet (IntSet)
import Data.Map (Map)
import Data.IntMap (IntMap)
import Data.Text (pack)
import qualified Data.Text as T

-- UseMap maps names to the set of used (reachable) argument positions.
type UseMap = Map Name (IntMap (Set Reason))

data Arg = Arg !Int | Result deriving (Eq, Ord)

instance Show Arg where
    show (Arg i) = show i
    show Result  = "*"

type Node = (Name, Arg)
type Deps = Map Cond DepSet
type Reason = (Name, Int)  -- function name, argument index

-- Nodes along with sets of reasons for every one.
type DepSet = Map Node (Set Reason)

-- "Condition" is the conjunction
-- of elementary assumptions along the path from the root.
-- Elementary assumption (f, i) means that "function f uses the argument i".
type Cond = Set Node

-- Every variable draws in certain dependencies.
type Var = DepSet
type Vars = Map Name Var

-- Perform usage analysis, write the relevant information in the internal
-- structures, returning the list of reachable names.
performUsageAnalysis :: Idris [Name]
performUsageAnalysis = do
    ctx <- tt_ctxt <$> getIState

    case lookupCtxt mainName (definitions ctx) of
      [] -> return []  -- no main -> not compiling -> reachability irrelevant
      _  -> do
        ci  <- idris_classes <$> getIState
        cg  <- idris_callgraph <$> getIState
        opt <- idris_optimisation <$> getIState

        -- Build the dependency graph.
        let depMap = buildDepMap ci ctx mainName

        -- Search for reachable nodes in the graph.
        let (residDeps, (reachableNames, minUse)) = minimalUsage depMap
            usage = M.toList minUse

        -- Print some debug info.
        logLvl 3 $ "Reachable names:\n" ++ unlines (map (indent . show) . S.toList $ reachableNames)
        logLvl 4 $ "Minimal usage:\n" ++ fmtUseMap usage
        logLvl 5 $ "Residual deps:\n" ++ unlines (map fmtItem . M.toList $ residDeps)

        -- Check that everything reachable is accessible.
        mapM_ (checkAccessibility opt) usage

        -- Store the usage info in the internal state.
        mapM_ (storeUsage cg) usage

        return $ S.toList reachableNames
  where
    mainName = sNS (sUN "main") ["Main"]
    indent = ("  " ++)

    fmtItem :: (Cond, DepSet) -> String
    fmtItem (cond, deps) = indent $ show (S.toList cond) ++ " -> " ++ show (M.toList deps)

    fmtUseMap :: [(Name, IntMap (Set Reason))] -> String
    fmtUseMap = unlines . map (\(n,is) -> indent $ show n ++ " -> " ++ fmtIxs is)

    fmtIxs :: IntMap (Set Reason) -> String
    fmtIxs = intercalate ", " . map fmtArg . IM.toList
      where
        fmtArg (i, rs)
            | S.null rs = show i
            | otherwise = show i ++ " from " ++ intercalate ", " (map show $ S.toList rs)

    storeUsage :: Ctxt CGInfo -> (Name, IntMap (Set Reason)) -> Idris ()
    storeUsage cg (n, args)
        | [x] <- lookupCtxt n cg
        = addToCG n x{ usedpos = flat }        -- functions

        | otherwise
        = addToCG n (CGInfo [] [] [] [] flat)  -- data ctors
      where
        flat = [(i, S.toList rs) | (i,rs) <- IM.toList args]

    checkAccessibility :: Ctxt OptInfo -> (Name, IntMap (Set Reason)) -> Idris ()
    checkAccessibility opt (n, reachable)
        | [Optimise col nt forc rec inaccessible] <- lookupCtxt n opt
{'fraction_non_alphanumeric': 0.10530557421087978, 'fraction_numerical': 0.0008059100067159167, 'mean_word_length': 2.7777777777777777, 'pattern_counts': {'":': 0, '<': 25, '<?xml version=': 0, '>': 38, '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': '6846839', 'n_tokens_mistral': 2340, 'n_tokens_neox': 2234, 'n_words': 844}