module Agda.Compiler.Epic.NatDetection where
import Control.Applicative
import Control.Monad
import Control.Monad.State
import Data.Function
import Data.List
import qualified Data.Map as M
import Data.Maybe
import Agda.TypeChecking.Monad
import Agda.Syntax.Internal
import Agda.Syntax.Common
import Agda.Compiler.Epic.CompileState hiding (conPars)
getNatish :: MonadTCM m => Compile m [(IrrFilter,[QName])]
getNatish = do
sig <- lift (gets (sigDefinitions . stImports))
let defs = M.toList sig
fmap catMaybes $ forM defs $ \(q, def) ->
case theDef def of
d@(Datatype {}) -> do
case dataCons d of
constrs | length constrs == 2 -> do
z <- zip constrs <$> mapM getIrrFilter constrs
case sortBy (compare `on` nrRel . snd) z of
[(cz,fz), (cs,fs)] -> do
let ts = defType $ sig M.! cs
nr = fromIntegral $ dataPars d
return $ do
guard (nrRel fz == 0)
guard (nrRel fs == 1)
guard (isRec ((fromJust $ elemIndex True fs) + nr) ts q)
return (fs, [cz, cs])
_ -> return Nothing
_ -> return Nothing
_ -> return Nothing
nrRel :: IrrFilter -> Integer
nrRel = sum . map (const 1) . filter id
isRec :: Int -> Type -> QName -> Bool
isRec 0 (El _ t) dat = case t of
Fun arg _ -> argIsDef (unArg arg) dat
Pi arg _ -> argIsDef (unArg arg) dat
_ -> False
isRec n (El _ t) dat = case t of
Pi _ ab -> isRec (n 1) (absBody ab) dat
Fun _ typ -> isRec (n 1) typ dat
_ -> False
argIsDef :: Type -> QName -> Bool
argIsDef (El _ t) dat = case t of
Def q _ -> q == dat
_ -> False