git.iko.soy/Idris-dev
on master help sign in
Extend the Nat hack for Nat-like families.
e16f741Matus Tejiscak
src/IRTS/Compiler.hs+45−1
compare with master
unifiedsplit
@@ -5,7 +5,7 @@ Description : Coordinates the compilation process.
5License : BSD3
5License : BSD3
6Maintainer : The Idris Community.
6Maintainer : The Idris Community.
7-}
7-}
8−{-# LANGUAGE CPP, FlexibleContexts, PatternGuards, TypeSynonymInstances #-}
8+{-# LANGUAGE CPP, FlexibleContexts, PatternGuards, TypeSynonymInstances, NamedFieldPuns #-}
9
9
10module IRTS.Compiler(compile, generate) where
10module IRTS.Compiler(compile, generate) where
11
11
@@ -33,6 +33,7 @@ import Prelude hiding (id, (.))
33import Control.Category
33import Control.Category
34import Control.Monad.State
34import Control.Monad.State
35import Data.List
35import Data.List
36+import Data.Maybe (maybe)
36import qualified Data.Map as M
37import qualified Data.Map as M
37import Data.Ord
38import Data.Ord
38import qualified Data.Set as S
39import qualified Data.Set as S
@@ -254,6 +255,7 @@ type Vars = M.Map Name VarInfo
254irTerm :: Name -> Vars -> [Name] -> Term -> Idris LExp
255irTerm :: Name -> Vars -> [Name] -> Term -> Idris LExp
255irTerm top vs env tm@(App _ f a) = do
256irTerm top vs env tm@(App _ f a) = do
256 ist <- getIState
257 ist <- getIState
258+ let (likeNatZ, likeNatS) = getNatLikeCtors ist
257 case unApply tm of
259 case unApply tm of
258 (P _ n _, args)
260 (P _ n _, args)
259 | n `elem` map fst (idris_metavars ist) \\ primDefs
261 | n `elem` map fst (idris_metavars ist) \\ primDefs
@@ -393,6 +395,15 @@ irTerm top vs env tm@(App _ f a) = do
393 EQ | isNewtype
395 EQ | isNewtype
394 -> irTerm top vs env (head argsPruned)
396 -> irTerm top vs env (head argsPruned)
395
397
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+
396 | otherwise -- not newtype, plain data ctor
407 | otherwise -- not newtype, plain data ctor
397 -> buildApp (LV n) argsPruned
408 -> buildApp (LV n) argsPruned
398
409
@@ -405,6 +416,11 @@ irTerm top vs env tm@(App _ f a) = do
405 | isNewtype -- newtype but the value is not among args yet
416 | isNewtype -- newtype but the value is not among args yet
406 -> return . padLams $ \[vn] -> LApp False (LV n) [LV vn]
417 -> return . padLams $ \[vn] -> LApp False (LV n) [LV vn]
407
418
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+
408 -- not a newtype, just apply to a constructor
424 -- not a newtype, just apply to a constructor
409 | otherwise
425 | otherwise
410 -> padLams . applyToNames <$> buildApp (LV n) argsPruned
426 -> padLams . applyToNames <$> buildApp (LV n) argsPruned
@@ -501,6 +517,34 @@ irTerm top vs env (TType _) = return LNothing
501irTerm top vs env Erased = return LNothing
517irTerm top vs env Erased = return LNothing
502irTerm top vs env Impossible = return LNothing
518irTerm top vs env Impossible = return LNothing
503
519
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+
504doForeign :: Vars -> [Name] -> [Term] -> Idris LExp
548doForeign :: Vars -> [Name] -> [Term] -> Idris LExp
505doForeign vs env (ret : fname : world : args)
549doForeign vs env (ret : fname : world : args)
506 = do args' <- mapM splitArg args
550 = do args' <- mapM splitArg args