<commit_before>{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE InstanceSigs          #-}

-- | Infrastructure for KURE-based rewrites on CL expressions
   
module Database.DSH.CL.Kure
    (
      -- * The KURE monad
      CompM, TranslateC, RewriteC
      -- * The KURE context
    , CompC
      -- * Congruence combinators
    , tableT, appT, appe1T, appe2T, binopT, lamT, ifT, litT, varT, compT
    , tableR, appR, appe1R, appe2R, binopR, lamR, ifR, litR, varR, compR
    , bindQualT, guardQualT, bindQualR, guardQualR
    , qualsT, qualsR
    ) where
    
       
import           Control.Monad
import           Data.List
import qualified Data.Map as M

import           Language.KURE
       
import           Database.DSH.Common.Data.Op
import           Database.DSH.Common.Data.Val
import           Database.DSH.Common.Data.Type
import           Database.DSH.Common.Data.Expr
import           Database.DSH.CL.Lang
                 

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

-- The rewriting monad. For the moment, we use the regular KURE monad. Should
-- the need arise for e.g. fresh variables, add another monad wrapper.
type CompM = KureM

type TranslateC a b = Translate CompC CompM a b
type RewriteC a     = TranslateC a a

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

-- | The context for KURE-based CL rewrites
data CompC = CompC { cl_bindings :: M.Map Ident Type }

-- | Record a variable binding in the context
bindVar :: Ident -> Type -> CompC -> CompC
bindVar n ty ctx = ctx { cl_bindings = M.insert n ty (cl_bindings ctx) }

-- | If the qualifier represents a generator, bind the variable in the context.
bindQual :: CompC -> Qual -> CompC
bindQual ctx (BindQ n e) = bindVar n (elemT $ typeOf e) ctx
bindQual ctx _           = ctx

--------------------------------------------------------------------------------
-- Congruence combinators for CL expressions

tableT :: Monad m => (Type -> String -> [Column] -> [Key] -> b)
                  -> Translate CompC m Expr b
tableT f = contextfreeT $ \expr -> case expr of
                      Table ty n cs ks -> return $ f ty n cs ks
                      _                -> fail "not a table node"
                      
tableR :: Monad m => Rewrite CompC m Expr
tableR = tableT Table
                                       
appT :: Monad m => Translate CompC m Expr a1
                -> Translate CompC m Expr a2
                -> (Type -> a1 -> a2 -> b)
                -> Translate CompC m Expr b
appT t1 t2 f = translate $ \c expr -> case expr of
                      App ty e1 e2 -> f ty <$> apply t1 c e1 <*> apply t2 c e2
                      _            -> fail "not an application node"
                      
appR :: Monad m => Rewrite CompC m Expr -> Rewrite CompC m Expr -> Rewrite CompC m Expr
appR t1 t2 = appT t1 t2 App
                      
appe1T :: Monad m => Translate CompC m Expr a
                  -> (Type -> Prim1 Type -> a -> b)
                  -> Translate CompC m Expr b
appe1T t f = translate $ \c expr -> case expr of
                      AppE1 ty p e -> f ty p <$> apply t c e                  
                      _            -> fail "not a unary primitive application"
                      <commit_msg>Re-export KURE modules, added simple context query functions.<commit_after>{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE InstanceSigs          #-}

-- | Infrastructure for KURE-based rewrites on CL expressions
   
module Database.DSH.CL.Kure
    ( -- * Re-export relevant KURE modules
      module Language.KURE

      -- * The KURE monad
    , CompM, TranslateC, RewriteC

      -- * The KURE context
    , CompC, freeIn, boundIn

      -- * Congruence combinators
    , tableT, appT, appe1T, appe2T, binopT, lamT, ifT, litT, varT, compT
    , tableR, appR, appe1R, appe2R, binopR, lamR, ifR, litR, varR, compR
    , bindQualT, guardQualT, bindQualR, guardQualR
    , qualsT, qualsR
    ) where
    
       
import           Control.Monad
import           Data.List
import qualified Data.Map as M

import           Language.KURE
       
import           Database.DSH.Common.Data.Op
import           Database.DSH.Common.Data.Val
import           Database.DSH.Common.Data.Type
import           Database.DSH.Common.Data.Expr
import           Database.DSH.CL.Lang
                 

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

-- The rewriting monad. For the moment, we use the regular KURE monad. Should
-- the need arise for e.g. fresh variables, add another monad wrapper.
type CompM = KureM

type TranslateC a b = Translate CompC CompM a b
type RewriteC a     = TranslateC a a

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

-- | The context for KURE-based CL rewrites
data CompC = CompC { cl_bindings :: M.Map Ident Type }

-- | Record a variable binding in the context
bindVar :: Ident -> Type -> CompC -> CompC
bindVar n ty ctx = ctx { cl_bindings = M.insert n ty (cl_bindings ctx) }

-- | If the qualifier represents a generator, bind the variable in the context.
bindQual :: CompC -> Qual -> CompC
bindQual ctx (BindQ n e) = bindVar n (elemT $ typeOf e) ctx
bindQual ctx _           = ctx

boundIn :: Ident -> CompC -> Bool
boundIn n ctx = n `M.member` (cl_bindings ctx)

freeIn :: Ident -> CompC -> Bool
freeIn n ctx = n `M.notMember` (cl_bindings ctx)

--------------------------------------------------------------------------------
-- Congruence combinators for CL expressions

tableT :: Monad m => (Type -> String -> [Column] -> [Key] -> b)
                  -> Translate CompC m Expr b
tableT f = contextfreeT $ \expr -> case expr of
                      Table ty n cs ks -> return $ f ty n cs ks
                      _                -> fail "not a table node"
                      
tableR :: Monad m => Rewrite CompC m Expr
tableR = tableT Table
                                       
appT :: Monad m => Translate CompC m Expr a1
                -> Translate CompC m Expr a2
                -> (Type -> a1 -> a2 -> b)
                -> Translate CompC m Expr b
appT t1 t2 f = translate $ \c expr -> case expr of
                      App ty e1 e2 -> f ty <$> apply t1 c e1 <*> apply t2 c e2
                      _            -> fail "not an application node"
                      
appR :: Monad m => Rewrite CompC m Expr -> Rewrite CompC m Expr -> Rewrite CompC m Expr
appR t1 t2 = appT t1 t2 App
                      
appe1T :: Monad m => Translate CompC m Expr a
                  -> (Type -> Prim1 Type -> a -> b)
                  -> Translate CompC m Expr b
appe1T t f = translate $ \c expr -> case expr of
                      AppE1 ty p e -> f ty p <$> apply t c e                  
                      _            -> fail "not a unary primitive application"
                      
{'fraction_non_alphanumeric': 0.14970575570546865, 'fraction_numerical': 0.006889622506100187, 'mean_word_length': 1.3700680272108843, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 87, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 10, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '643716', 'n_tokens_mistral': 2029, 'n_tokens_neox': 1969, 'n_words': 741}