<commit_before>{-# LANGUAGE PatternGuards #-}

module Idris.DataOpts where

-- Forcing, detagging and collapsing

import Idris.AbsSyntax
import Idris.AbsSyntaxTree
import Core.TT

import Control.Applicative
import qualified Data.IntMap.Strict as M
import Data.List
import Data.Maybe
import Debug.Trace

type ForceMap = M.IntMap Forceability

-- Calculate the forceable arguments to a constructor
-- and update the set of optimisations.
forceArgs :: Name -> Name -> Type -> Idris ()
forceArgs typeName n t = do
    ist <- getIState
    let fargs = getForcedArgs ist typeName t
        copt = case lookupCtxt n (idris_optimisation ist) of
          []   -> Optimise False False [] []
          op:_ -> op
        opts = addDef n (copt { forceable = M.toList fargs }) (idris_optimisation ist)
    putIState (ist { idris_optimisation = opts })
    addIBC (IBCOpt n)
    iLOG $ "Forced: " ++ show n ++ " " ++ show fargs ++ "\n   from " ++ show t

getForcedArgs :: IState -> Name -> Type -> ForceMap
getForcedArgs ist typeName t = addCollapsibleArgs 0 t $ forcedInTarget 0 t
  where
    maxUnion = M.unionWith max

    -- Label all occurrences of the variable bound in Pi in the rest of
    -- the term with the number i so that we can recognize them anytime later.
    label i = instantiate $ P Bound (MN i "ctor_arg") Erased<commit_msg>Fix too-new import<commit_after>{-# LANGUAGE PatternGuards #-}

module Idris.DataOpts where

-- Forcing, detagging and collapsing

import Idris.AbsSyntax
import Idris.AbsSyntaxTree
import Core.TT

import Control.Applicative
import qualified Data.IntMap as M
import Data.List
import Data.Maybe
import Debug.Trace

type ForceMap = M.IntMap Forceability

-- Calculate the forceable arguments to a constructor
-- and update the set of optimisations.
forceArgs :: Name -> Name -> Type -> Idris ()
forceArgs typeName n t = do
    ist <- getIState
    let fargs = getForcedArgs ist typeName t
        copt = case lookupCtxt n (idris_optimisation ist) of
          []   -> Optimise False False [] []
          op:_ -> op
        opts = addDef n (copt { forceable = M.toList fargs }) (idris_optimisation ist)
    putIState (ist { idris_optimisation = opts })
    addIBC (IBCOpt n)
    iLOG $ "Forced: " ++ show n ++ " " ++ show fargs ++ "\n   from " ++ show t

getForcedArgs :: IState -> Name -> Type -> ForceMap
getForcedArgs ist typeName t = addCollapsibleArgs 0 t $ forcedInTarget 0 t
  where
    maxUnion = M.unionWith max

    -- Label all occurrences of the variable bound in Pi in the rest of
    -- the term with the number i so that we can recognize them anytime later.
    label i = instantiate $ P Bound (MN i "ctor_arg") Erased
{'fraction_non_alphanumeric': 0.08640120210368145, 'fraction_numerical': 0.0015026296018031556, 'mean_word_length': 3.065648854961832, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 19, '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': '6573917', 'n_tokens_mistral': 834, 'n_tokens_neox': 799, 'n_words': 315}