<commit_before>{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
             TypeSynonymInstances, PatternGuards #-}

module Idris.AbsSyntax(module Idris.AbsSyntax, module Idris.AbsSyntaxTree) where

import Core.TT
import Core.Evaluate
import Core.Elaborate hiding (Tactic(..))
import Core.Typecheck
import Idris.AbsSyntaxTree

import Paths_idris

import System.Console.Haskeline

import Control.Monad.State

import Data.List
import Data.Char
import Data.Either

import Debug.Trace

import Util.Pretty


getContext :: Idris Context
getContext = do i <- get; return (tt_ctxt i)

getObjectFiles :: Idris [FilePath]
getObjectFiles = do i <- get; return (idris_objs i)

addObjectFile :: FilePath -> Idris ()
addObjectFile f = do i <- get; put (i { idris_objs = f : idris_objs i })

getLibs :: Idris [String]
getLibs = do i <- get; return (idris_libs i)

addLib :: String -> Idris ()
addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })

addHdr :: String -> Idris ()
addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })

totcheck :: (FC, Name) -> Idris ()
totcheck n = do i <- get; put (i { idris_totcheck = n : idris_totcheck i })

setFlags :: Name -> [FnOpt] -> Idris ()
setFlags n fs = do i <- get; put (i { idris_flags = addDef n fs (idris_flags i) }) 

setAccessibility :: Name -> Accessibility -> Idris ()
setAccessibility n a 
         = do i <- get
              let ctxt = setAccess n a (tt_ctxt i)
              put (i { tt_ctxt = ctxt })

setTotality :: Name -> Totality -> Idris ()
setTotality n a 
         = do i <- get
              let ctxt = setTotal n a (tt_ctxt i)
              put (i { tt_ctxt = ctxt })

getTotality :: Name -> Idris Totality
getTotality n  
         = do i <- get
              case lookupTotal n (tt_ctxt i) of
                [t] -> return t
                _ -> return (Total [])

addToCG :: Name -> CGInfo -> Idris ()
addToCG n cg = do i <- get
                  put (i { idris_callgraph = addDef n cg (idris_callgraph i) })

addToCalledG :: Name -> [Name] -> Idris ()
addToCalledG n ns = return () -- TODO

-- Add a class instance function. Dodgy hack: Put integer instances first in the
-- list so they are resolved by default.

addInstance :: Bool -> Name -> Name -> Idris ()
addInstance int n i 
    = do ist <- get
         case lookupCtxt Nothing n (idris_classes ist) of
                [CI a b c d ins] ->
                     do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)
                        put (ist { idris_classes = cs })
                _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)
                        put (ist { idris_classes = cs })
  where addI i ins | int = i : ins
                   | otherwise = ins ++ [i]

addClass :: Name -> ClassInfo -> Idris ()
addClass n i 
   = do ist <- get
        let i' = case lookupCtxt Nothing n (idris_classes ist) of
                      [c] -> c { class_instances = class_instances i }
                      _ -> i
        put (ist { idris_classes = addDef n i' (idris_classes ist) }) 

addIBC :: IBCWrite -> Idris ()
addIBC ibc@(IBCDef n) 
           = do i <- get
                when (notDef (ibc_write i)) $
                  put (i { ibc_write = ibc : ibc_write i })
   where notDef [] = True<commit_msg>Type class fix Chase parent class dependencies last (after looking for a directly defined instance)<commit_after>{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
             TypeSynonymInstances, PatternGuards #-}

module Idris.AbsSyntax(module Idris.AbsSyntax, module Idris.AbsSyntaxTree) where

import Core.TT
import Core.Evaluate
import Core.Elaborate hiding (Tactic(..))
import Core.Typecheck
import Idris.AbsSyntaxTree

import Paths_idris

import System.Console.Haskeline

import Control.Monad.State

import Data.List
import Data.Char
import Data.Either

import Debug.Trace

import Util.Pretty


getContext :: Idris Context
getContext = do i <- get; return (tt_ctxt i)

getObjectFiles :: Idris [FilePath]
getObjectFiles = do i <- get; return (idris_objs i)

addObjectFile :: FilePath -> Idris ()
addObjectFile f = do i <- get; put (i { idris_objs = f : idris_objs i })

getLibs :: Idris [String]
getLibs = do i <- get; return (idris_libs i)

addLib :: String -> Idris ()
addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })

addHdr :: String -> Idris ()
addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })

totcheck :: (FC, Name) -> Idris ()
totcheck n = do i <- get; put (i { idris_totcheck = n : idris_totcheck i })

setFlags :: Name -> [FnOpt] -> Idris ()
setFlags n fs = do i <- get; put (i { idris_flags = addDef n fs (idris_flags i) }) 

setAccessibility :: Name -> Accessibility -> Idris ()
setAccessibility n a 
         = do i <- get
              let ctxt = setAccess n a (tt_ctxt i)
              put (i { tt_ctxt = ctxt })

setTotality :: Name -> Totality -> Idris ()
setTotality n a 
         = do i <- get
              let ctxt = setTotal n a (tt_ctxt i)
              put (i { tt_ctxt = ctxt })

getTotality :: Name -> Idris Totality
getTotality n  
         = do i <- get
              case lookupTotal n (tt_ctxt i) of
                [t] -> return t
                _ -> return (Total [])

addToCG :: Name -> CGInfo -> Idris ()
addToCG n cg = do i <- get
                  put (i { idris_callgraph = addDef n cg (idris_callgraph i) })

addToCalledG :: Name -> [Name] -> Idris ()
addToCalledG n ns = return () -- TODO

-- Add a class instance function. Dodgy hack: Put integer instances first in the
-- list so they are resolved by default.
-- Dodgy hack 2: put constraint chasers (@@) last

addInstance :: Bool -> Name -> Name -> Idris ()
addInstance int n i 
    = do ist <- get
         case lookupCtxt Nothing n (idris_classes ist) of
                [CI a b c d ins] ->
                     do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)
                        put (ist { idris_classes = cs })
                _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)
                        put (ist { idris_classes = cs })
  where addI i ins | int = i : ins
                   | chaser n = ins ++ [i]
                   | otherwise = insI i ins
        insI i [] = [i]
        insI i (n : ns) | chaser n = i : n : ns
                        | otherwise = n : insI i ns

        chaser (UN ('@':'@':_)) = True
        chaser (NS n _) = chaser n
        chaser _ = False

addClass :: Name -> ClassInfo -> Idris ()
addClass n i 
   = do ist <- get
        let i' = case lookupCtxt Nothing n (idris_classes ist) of
                      [c] -> c { class_instances = class_instances i }
                      _ -> i
        put (ist { idris_classes = addDef n i' (idris_classes ist) }) 

addIBC :: IBCWrite -> Idris ()
addIBC ibc@(IBCDef n) 
           = do i <- get
                when (notDef (ibc_write i)) $
                  put (i { ibc_write = ibc : ibc_write i })
   where notDef [] = True
{'fraction_non_alphanumeric': 0.11262993022924676, 'fraction_numerical': 0.00042716787697565144, 'mean_word_length': 2.116237799467613, 'pattern_counts': {'":': 0, '<': 33, '<?xml version=': 0, '>': 57, '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': '1840508', 'n_tokens_mistral': 2385, 'n_tokens_neox': 2257, 'n_words': 812}