<commit_before>{-# LANGUAGE UnicodeSyntax #-}

module Types ( printTypes ) where

------------------------------------------------------------------------------
-- Haskell imports

import qualified Data.HashMap.Strict as HashMap ( toList )

import Data.Int      ( Int32 )
import Data.Function ( on )
import Data.List     ( sortBy )

------------------------------------------------------------------------------
-- Agda library imports

import Agda.Syntax.Abstract.Name
  ( Name(nameBindingSite)
  , QName(qnameName)
  )

import Agda.Syntax.Internal ( Type )

import Agda.TypeChecking.Monad.Base
  ( Definition
  , Definitions
  , defType
  , Interface(iSignature)
  , Signature(sigDefinitions)
  )

import Agda.Syntax.Position
  ( Interval(iStart)
  , Position(posLine)
  , rangeToInterval
  )

------------------------------------------------------------------------------
-- Auxiliary functions

qNameLine ∷ QName → Int32
qNameLine qName =
  case rangeToInterval $ nameBindingSite $ qnameName qName of
    Nothing → error "qNameLine"
    Just i  → posLine $ iStart i

-- We sort the @QName@'s by its position in the Agda module.
myQNameSort ∷ QName → QName → Ordering
myQNameSort = compare `on` qNameLine

myQNameDefinitionSort ∷ (QName, Definition) → (QName, Definition) → Ordering
myQNameDefinitionSort = myQNameSort `on` fst

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

printQNameType ∷ (QName, Definition) → IO ()
printQNameType (qname, def) = do

  let ty ∷ Type
      ty = defType def

  putStrLn $ "Qname: " ++ show qname
  putStrLn $ "Type: "  ++ show ty ++ "\n"

printTypes ∷ Interface → IO ()
printTypes i = do<commit_msg>Cosmetic changes.<commit_after>{-# LANGUAGE UnicodeSyntax #-}

module Types ( printTypes ) where

------------------------------------------------------------------------------
-- Haskell imports

import Data.Function ( on )

import qualified Data.HashMap.Strict as HashMap ( toList )

import Data.Int  ( Int32 )
import Data.List ( sortBy )

------------------------------------------------------------------------------
-- Agda library imports

import Agda.Syntax.Abstract.Name
  ( Name(nameBindingSite)
  , QName(qnameName)
  )

import Agda.Syntax.Internal ( Type )

import Agda.TypeChecking.Monad.Base
  ( Definition
  , Definitions
  , defType
  , Interface(iSignature)
  , Signature(sigDefinitions)
  )

import Agda.Syntax.Position
  ( Interval(iStart)
  , Position(posLine)
  , rangeToInterval
  )

------------------------------------------------------------------------------
-- Auxiliary functions

qNameLine ∷ QName → Int32
qNameLine qName =
  case rangeToInterval $ nameBindingSite $ qnameName qName of
    Nothing → error "qNameLine"
    Just i  → posLine $ iStart i

-- We sort the @QName@'s by its position in the Agda module.
myQNameSort ∷ QName → QName → Ordering
myQNameSort = compare `on` qNameLine

myQNameDefinitionSort ∷ (QName, Definition) → (QName, Definition) → Ordering
myQNameDefinitionSort = myQNameSort `on` fst

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

printQNameType ∷ (QName, Definition) → IO ()
printQNameType (qName, def) = do

  let ty ∷ Type
      ty = defType def

  putStrLn $ "Qname: " ++ show qName
  putStrLn $ "Type: "  ++ show ty ++ "\n"

printTypes ∷ Interface → IO ()
printTypes i = do
{'fraction_non_alphanumeric': 0.26864330637915546, 'fraction_numerical': 0.002395926924228811, 'mean_word_length': 1.7603305785123966, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, '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': '1758015', 'n_tokens_mistral': 992, 'n_tokens_neox': 947, 'n_words': 280}