module Agda.Compiler.Epic.NatDetection where
import Control.Applicative
import Control.Monad
import Control.Monad.State
import Data.Function
import Data.List
import Data.Maybe
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.Utils.Monad (andM)
import Agda.Compiler.Epic.CompileState
import Agda.Compiler.Epic.Interface
import qualified Agda.Utils.HashMap as HM
#include "../../undefined.h"
import Agda.Utils.Impossible
getNatish :: Compile TCM [(ForcedArgs, [QName])]
getNatish = do
sig <- lift (gets (sigDefinitions . stImports))
let defs = HM.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 <- andM $ map 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 HM.! cs
nr = 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 (unDom 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