module Agda.Compiler.Agate.Classify where
#include "../../undefined.h"
import Agda.Utils.Impossible
import Agda.Compiler.Agate.TranslateName
import Agda.Compiler.Agate.Common
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Monad
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Abstract.Name
import Data.Map ((!), Map)
import qualified Data.Map as Map
import Control.Monad
import Agda.Utils.Monad
allM :: Monad m => (a -> m Bool) -> [a] -> m Bool
allM f xs = liftM and $ mapM f xs
andM :: Monad m => m Bool -> m Bool -> m Bool
andM x y = ifM x y $ return False
enumTypeFamilies :: Map QName Definition -> TCM [QName]
enumTypeFamilies definitions = fmap concat $ mapM f $ Map.toList definitions
where
f (name,d) = do
let ty = defType d
(_,ty2) <- splitType ty
(El sort term) <- reduce ty2
case term of
Sort _ -> return [name]
_ -> return []
enumCompilableTypeFamilies :: Map QName Definition -> TCM [QName]
enumCompilableTypeFamilies definitions = do
names <- enumTypeFamilies definitions
computeGreatestFixedPoint f names where
f :: [QName] -> QName -> TCM Bool
f names name = do
let d = definitions ! name
let def = theDef d
case def of
Axiom{} -> return False
Primitive{} -> return False
Function{funClauses = []} -> __IMPOSSIBLE__
Function{funClauses = [Clause{ clauseBody = NoBody }]} -> return False
Function{funClauses = [Clause{}]} -> return False
Function{} -> return False
Constructor{} -> return False
Datatype{dataCons = cnames} -> do
ty <- instantiate $ defType d
andM (isCompilableType ty) $
allM ( \cname ->
do let d = definitions ! cname
ty <- instantiate $ defType d
isCompilableType ty ) cnames
Record{} -> return True
where
isCompilableType :: Type -> TCM Bool
isCompilableType (El s tm) = isCompilableTypeFamily tm
isCompilableTypeFamily :: Term -> TCM Bool
isCompilableTypeFamily tm = do
tm <- reduce tm
case tm of
Var n args -> allM (isCompilableTypeFamily . unArg) args
Sort _ -> return True
Lam h abs -> return False
Def c args -> andM (return $ elem c names) $
allM (isCompilableTypeFamily . unArg) args
Pi arg abs -> andM (isCompilableType $ unArg arg) $
underAbstraction_ abs isCompilableType
Fun arg ty -> andM (isCompilableType $ unArg arg) $
isCompilableType ty
Lit lit -> return False
Con c args -> return False
MetaV _ _ -> return __IMPOSSIBLE__
enumOptimizableConstants :: Map QName Definition -> [QName] -> TCM [QName]
enumOptimizableConstants definitions names = do
computeGreatestFixedPoint f names
where
f :: [QName] -> QName -> TCM Bool
f names name = return True
computeGreatestFixedPoint :: ([QName] -> QName -> TCM Bool)-> [QName] -> TCM [QName]
computeGreatestFixedPoint f names = go names True where
go names False = return names
go names True = go2 names names [] False
go2 keptNames [] namesNext changed = go namesNext changed
go2 keptNames (name:names) namesNext changed = do
b <- f keptNames name
case b of
True -> go2 keptNames names (name : namesNext) changed
False -> go2 keptNames names namesNext True
computeLeastFixedPoint :: ([QName] -> QName -> TCM Bool) -> [QName] -> TCM [QName]
computeLeastFixedPoint f names = go names [] True where
go names grantedNames False = return grantedNames
go names grantedNames True = go2 names [] grantedNames False
go2 [] namesNext grantedNames changed =
go namesNext grantedNames changed
go2 (name:names) namesNext grantedNames changed = do
b <- f grantedNames name
case b of
True -> go2 names namesNext (name : grantedNames) True
False -> go2 names (name : namesNext) grantedNames changed