@@ -5,7 +5,7 @@ Description : Coordinates the compilation process.
55License : BSD3
66Maintainer : The Idris Community.
77-}
8−{-# LANGUAGE CPP, FlexibleContexts, PatternGuards, TypeSynonymInstances #-}
8+{-# LANGUAGE CPP, FlexibleContexts, PatternGuards, TypeSynonymInstances, NamedFieldPuns #-}
99
1010module IRTS.Compiler(compile, generate) where
1111
@@ -33,6 +33,7 @@ import Prelude hiding (id, (.))
3333import Control.Category
3434import Control.Monad.State
3535import Data.List
36+import Data.Maybe (maybe)
3637import qualified Data.Map as M
3738import Data.Ord
3839import qualified Data.Set as S
@@ -254,6 +255,7 @@ type Vars = M.Map Name VarInfo
254255irTerm :: Name -> Vars -> [Name] -> Term -> Idris LExp
255256irTerm top vs env tm@(App _ f a) = do
256257 ist <- getIState
258+ let (likeNatZ, likeNatS) = getNatLikeCtors ist
257259 case unApply tm of
258260 (P _ n _, args)
259261 | n `elem` map fst (idris_metavars ist) \\ primDefs
@@ -393,6 +395,15 @@ irTerm top vs env tm@(App _ f a) = do
393395 EQ | isNewtype
394396 -> irTerm top vs env (head argsPruned)
395397
398+ -- compile Nat-likes as bigints
399+ | n `S.member` likeNatZ
400+ -> irTerm top vs env $ Constant (BI 0)
401+
402+ -- compile Nat-likes as bigints
403+ | n `S.member` likeNatS
404+ -> irTerm top vs env $
405+ App Complete (P Ref (sUN "prim__addBigInt") Erased) (Constant $ BI 1)
406+
396407 | otherwise -- not newtype, plain data ctor
397408 -> buildApp (LV n) argsPruned
398409
@@ -405,6 +416,11 @@ irTerm top vs env tm@(App _ f a) = do
405416 | isNewtype -- newtype but the value is not among args yet
406417 -> return . padLams $ \[vn] -> LApp False (LV n) [LV vn]
407418
419+ -- compile Nat-likes as bigints
420+ | n `S.member` likeNatS
421+ -> irTerm top vs env $
422+ App Complete (P Ref (sUN "prim__addBigInt") Erased) (Constant $ BI 1)
423+
408424 -- not a newtype, just apply to a constructor
409425 | otherwise
410426 -> padLams . applyToNames <$> buildApp (LV n) argsPruned
@@ -501,6 +517,34 @@ irTerm top vs env (TType _) = return LNothing
501517irTerm top vs env Erased = return LNothing
502518irTerm top vs env Impossible = return LNothing
503519
520+getNatLikeCtors :: IState -> (S.Set Name, S.Set Name)
521+getNatLikeCtors ist =
522+ ( S.fromList $ map fst natLikeTypes
523+ , S.fromList $ map snd natLikeTypes
524+ )
525+ where
526+ getUsedCount :: Name -> Int
527+ getUsedCount n =
528+ maybe 0 (length . usedpos)
529+ $ lookupCtxtExact n
530+ $ idris_callgraph ist
531+
532+ natLikeTypes :: [(Name, Name)]
533+ natLikeTypes = do
534+ (_typeName, TI{con_names}) <- toAlist $ idris_datatypes ist
535+ case con_names of
536+ [z, s]
537+ | getUsedCount z == 0
538+ , getUsedCount s == 1
539+ -> [(z, s)]
540+
541+ [s, z]
542+ | getUsedCount z == 0
543+ , getUsedCount s == 1
544+ -> [(z, s)]
545+
546+ _ -> [] -- not a 2-constructor family
547+
504548doForeign :: Vars -> [Name] -> [Term] -> Idris LExp
505549doForeign vs env (ret : fname : world : args)
506550 = do args' <- mapM splitArg args