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.TypeChecking.Substitute
import Agda.Syntax.Common
import Agda.Compiler.Epic.CompileState
import Agda.Compiler.Epic.Interface
#include "../../undefined.h"
import Agda.Utils.Impossible
getNatish :: Compile TCM [(ForcedArgs, [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 {}) -> isNatish q d
_ -> return Nothing
isNatish :: QName -> Defn -> Compile TCM (Maybe (ForcedArgs, [QName]))
isNatish q d = do
case dataCons d of
constrs | length constrs == 2 -> do
b <- and <$> mapM constrInScope constrs
if b
then do
z <- zip constrs <$> mapM getForcedArgs constrs
case sortBy (compare `on` nrRel . snd) z of
[(cz,fz), (cs,fs)] -> do
sig <- lift (gets (sigDefinitions . stImports))
let ts = defType $ sig M.! cs
nr = fromIntegral $ dataPars d
return $ do
guard (nrRel fz == 0)
guard (nrRel fs == 1)
guard (isRec ((fromMaybe __IMPOSSIBLE__ $ elemIndex NotForced fs) + nr) ts q)
return (fs, [cz, cs])
_ -> return Nothing
else return Nothing
_ -> return Nothing
nrRel :: ForcedArgs -> Integer
nrRel = sum . map (const 1) . filter (== NotForced)
isRec :: Int -> Type -> QName -> Bool
isRec 0 (El _ t) dat = case t of
Pi arg _ -> argIsDef (unArg arg) dat
_ -> False
isRec n (El _ t) dat = case t of
Pi _ ab -> isRec (n 1) (unAbs ab) dat
_ -> False
argIsDef :: Type -> QName -> Bool
argIsDef (El _ t) dat = case t of
Def q _ -> q == dat
_ -> False