<commit_before>{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE LambdaCase #-}
module Language.Haskell.Liquid.Synthesize.GHC where

import qualified CoreSyn                       as GHC
import qualified Language.Fixpoint.Types       as F
import           Language.Haskell.Liquid.Types
import           Var
import           TyCoRep
import           CoreSyn
import           IdInfo
import           OccName
import           Unique
import           Name
import           TysPrim
import           Data.Default
import           Data.Maybe                     ( fromMaybe )
import           Language.Haskell.Liquid.GHC.TypeRep
import           Language.Fixpoint.Types
import qualified Data.HashMap.Strict           as M
import           TyCon
import           TysWiredIn

import           Data.List
import           Data.List.Split
import           Debug.Trace

instance Default Type where
    def = TyVarTy alphaTyVar 

mkVar :: Maybe String -> Int -> Type -> Var
mkVar x i t = mkGlobalVar VanillaId name t vanillaIdInfo 
  where 
    name = mkSystemName (mkUnique 'S' i) (mkVarOcc x')
    x'   = fromMaybe (freshName i) x 

freshName :: Int -> String 
freshName i = "lSyn$" ++ show i 

-- | Assuming that the functions are instantiated when this function is called.
goalType ::  Type ->   --  This is the goal type. It is used for basic types.
              Type ->  --   This type comes from the environment.
              Bool     --   True if the 2nd arg produces expression 
                       --   of type equal to 1st argument.
goalType τ (FunTy _ _ t'') 
  | t'' == τ  = True
  | otherwise = goalType τ t''
goalType τ                 t 
  | τ == t    = True
  | otherwise = False

-- Subgoals are function's arguments.
createSubgoals :: Type -> [Type] 
createSubgoals (ForAllTy _ htype) = createSubgoals htype
createSubgoals (FunTy _ t1 t2)      = t1 : createSubgoals t2
createSubgoals t                  = [t]

subgoals :: Type ->               -- Given a function type,
            Maybe (Type, [Type])  -- separate the result type from the input types.
subgoals t = if null gTys then Nothing else Just (resTy, inpTys) 
  where gTys            = createSubgoals t 
        (resTy, inpTys) = (last gTys, take (length gTys - 1) gTys)


-- @withSubgoal@ :: Takes a subgoal type, and 
-- returns all expressions in @ExprMemory@ that have the same type.
withSubgoal :: [(Type, CoreExpr, Int)] -> Type -> [(CoreExpr, Int)]<commit_msg>Support both 8.6.5 and 8.10.1 versions of GHC.<commit_after>{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE CPP #-}
module Language.Haskell.Liquid.Synthesize.GHC where

import qualified CoreSyn                       as GHC
import qualified Language.Fixpoint.Types       as F
import           Language.Haskell.Liquid.Types
import           Var
import           TyCoRep
import           CoreSyn
import           IdInfo
import           OccName
import           Unique
import           Name
import           TysPrim
import           Data.Default
import           Data.Maybe                     ( fromMaybe )
import           Language.Haskell.Liquid.GHC.TypeRep
import           Language.Fixpoint.Types
import qualified Data.HashMap.Strict           as M
import           TyCon
import           TysWiredIn

import           Data.List
import           Data.List.Split
import           Debug.Trace

instance Default Type where
    def = TyVarTy alphaTyVar 

mkVar :: Maybe String -> Int -> Type -> Var
mkVar x i t = mkGlobalVar VanillaId name t vanillaIdInfo 
  where 
    name = mkSystemName (mkUnique 'S' i) (mkVarOcc x')
    x'   = fromMaybe (freshName i) x 

freshName :: Int -> String 
freshName i = "lSyn$" ++ show i 

-- | Assuming that the functions are instantiated when this function is called.
goalType ::  Type ->   --  This is the goal type. It is used for basic types.
              Type ->  --   This type comes from the environment.
              Bool     --   True if the 2nd arg produces expression 
                       --   of type equal to 1st argument.
#if __GLASGOW_HASKELL__ >= 810
goalType τ (FunTy _ _ t'') 
  | t'' == τ  = True
  | otherwise = goalType τ t''
#else
goalType τ (FunTy _ t'') 
  | t'' == τ  = True
  | otherwise = goalType τ t''
#endif
goalType τ                 t 
  | τ == t    = True
  | otherwise = False

-- Subgoals are function's arguments.
createSubgoals :: Type -> [Type] 
createSubgoals (ForAllTy _ htype) = createSubgoals htype
#if __GLASGOW_HASKELL__ >= 810
createSubgoals (FunTy _ t1 t2)      = t1 : createSubgoals t2
#else
createSubgoals (FunTy t1 t2)      = t1 : createSubgoals t2
#endif
createSubgoals t                  = [t]

subgoals :: Type ->               -- Given a function type,
            Maybe (Type, [Type])  -- separate the result type from the input types.
subgoals t = if null gTys then Nothing else Just (resTy, inpTys) 
  where gTys            = createSubgoals t 
        (resTy, inpTys) = (last gTys, take (length gTys - 1) gTys)


-- @withSubgoal@ :: Takes a subgoal type, and 
-- returns all expressions in @ExprMemory@ that have the same type.
withSubgoal :: [(Type, CoreExpr, Int)] -> Type -> [(CoreExpr, Int)]
{'fraction_non_alphanumeric': 0.08354043203976295, 'fraction_numerical': 0.0059262091378321545, 'mean_word_length': 2.0312862108922363, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 25, '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': '6336417', 'n_tokens_mistral': 1656, 'n_tokens_neox': 1547, 'n_words': 546}