5e2000e · Idris-dev · git.iko.soy

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE CPP, FlexibleContexts, PatternGuards, TypeSynonymInstances, NamedFieldPuns #-}

8+{-# LANGUAGE CPP, FlexibleContexts, PatternGuards, TypeSynonymInstances, NamedFieldPuns, MultiWayIf #-}

9

10module IRTS.Compiler(compile, generate) where

11

255irTerm :: Name -> Vars -> [Name] -> Term -> Idris LExp

256irTerm top vs env tm@(App _ f a) = do

257 ist <- getIState

258− let (likeNatZ, likeNatS) = getNatLikeCtors ist

259 case unApply tm of

258 case unApply tm of

260 (P _ n _, args)

259 (P _ n _, args)

261 | n `elem` map fst (idris_metavars ist) \\ primDefs

260 | n `elem` map fst (idris_metavars ist) \\ primDefs

396 -> irTerm top vs env (head argsPruned)

395 -> irTerm top vs env (head argsPruned)

397

396

398 -- compile Nat-likes as bigints

397 -- compile Nat-likes as bigints

399− | n `S.member` likeNatZ

398+ | Just LikeZ <- isLikeNat ist n

400 -> irTerm top vs env $ Constant (BI 0)

399 -> irTerm top vs env $ Constant (BI 0)

401

400

402 -- compile Nat-likes as bigints

401 -- compile Nat-likes as bigints

403− | n `S.member` likeNatS

402+ | Just LikeS <- isLikeNat ist n

404 -> irTerm top vs env $

403 -> irTerm top vs env $

405 App Complete (P Ref (sUN "prim__addBigInt") Erased) (Constant $ BI 1)

404 App Complete (P Ref (sUN "prim__addBigInt") Erased) (Constant $ BI 1)

406

405

417 -> return . padLams $ \[vn] -> LApp False (LV n) [LV vn]

416 -> return . padLams $ \[vn] -> LApp False (LV n) [LV vn]

418

417

419 -- compile Nat-likes as bigints

418 -- compile Nat-likes as bigints

420− | n `S.member` likeNatS

419+ | Just LikeS <- isLikeNat ist n

421 -> irTerm top vs env $

420 -> irTerm top vs env $

422 App Complete (P Ref (sUN "prim__addBigInt") Erased) (Constant $ BI 1)

421 App Complete (P Ref (sUN "prim__addBigInt") Erased) (Constant $ BI 1)

423

422

517irTerm top vs env Erased = return LNothing

516irTerm top vs env Erased = return LNothing

518irTerm top vs env Impossible = return LNothing

517irTerm top vs env Impossible = return LNothing

519

518

520−getNatLikeCtors :: IState -> (S.Set Name, S.Set Name)

519+data LikeNat = LikeZ | LikeS

521−getNatLikeCtors ist =

520+

522− ( S.fromList $ map fst natLikeTypes

521+isLikeNat :: IState -> Name -> Maybe LikeNat

523− , S.fromList $ map snd natLikeTypes

522+isLikeNat ist cn

524− )

523+ | Just cTy <- lookupTyExact cn $ tt_ctxt ist

524+ , (P TCon{} tyN _, _) <- unApply $ getRetTy cTy

525+ , Just (z, s) <- natLikeCtors tyN cTy

526+ = if | cn == z -> Just LikeZ

527+ | cn == s -> Just LikeS

528+ | otherwise -> Nothing

525 where

529 where

530+ natLikeCtors :: Name -> Type -> Maybe (Name, Name)

531+ natLikeCtors tyN cTy = case lookupCtxtExact tyN $ idris_datatypes ist of

532+ Just TI{con_names = [z, s]}

533+ | 0 <- getUsedCount z

534+ , looksLikeS tyN s cTy

535+ -> Just (z, s)

536+

537+ Just TI{con_names = [s, z]}

538+ | 0 <- getUsedCount z

539+ , looksLikeS tyN s cTy

540+ -> Just (z, s)

541+

542+ _ -> Nothing

543+

526 getUsedCount :: Name -> Int

544 getUsedCount :: Name -> Int

527 getUsedCount n =

545 getUsedCount n =

528 maybe 0 (length . usedpos)

546 maybe 0 (length . usedpos)

529 $ lookupCtxtExact n

547 $ lookupCtxtExact n

530 $ idris_callgraph ist

548 $ idris_callgraph ist

531

549

532− isRecursive :: Name -> Name -> Bool

550+ looksLikeS :: Name -> Name -> Type -> Bool

533− isRecursive tyN cn

551+ looksLikeS tyN cn cTy

534− | Just (Bind _ Pi{binderTy = P _ argTyN _} _) <- lookupTyExact cn $ tt_ctxt ist

552+ | Just [(i, _)] <- fmap usedpos $ lookupCtxtExact cn $ idris_callgraph ist

535− , argTyN == tyN

553+ , [recTy] <- [recTy | (j, (_n, recTy)) <- zip [0..] (getArgTys cTy), j == i]

554+ , (P TCon{} recTyN _, _) <- unApply recTy

555+ , recTyN == tyN

536 = True

556 = True

537

557

538 | otherwise = False

558 | otherwise = False

539

559

540− natLikeTypes :: [(Name, Name)]

541− natLikeTypes = do

542− (typeName, TI{con_names}) <- toAlist $ idris_datatypes ist

543− case con_names of

544− [z, s]

545− | getUsedCount z == 0

546− , getUsedCount s == 1

547− , isRecursive typeName s

548− -> [(z, s)]

549−

550− [s, z]

551− | getUsedCount z == 0

552− , getUsedCount s == 1

553− , isRecursive typeName s

554− -> [(z, s)]

555−

556− _ -> [] -- not a 2-constructor family

557−

558doForeign :: Vars -> [Name] -> [Term] -> Idris LExp

560doForeign :: Vars -> [Name] -> [Term] -> Idris LExp

559doForeign vs env (ret : fname : world : args)

561doForeign vs env (ret : fname : world : args)

560 = do args' <- mapM splitArg args

562 = do args' <- mapM splitArg args

690irAlt :: Name -> Vars -> LExp -> CaseAlt -> Idris LAlt

692irAlt :: Name -> Vars -> LExp -> CaseAlt -> Idris LAlt

691

693

692-- this leaves out all unused arguments of the constructor

694-- this leaves out all unused arguments of the constructor

693−irAlt top vs _ (ConCase n t args sc) = do

695+irAlt top vs tm (ConCase n t args sc) = do

696+ likeNat <- isLikeNat <$> getIState <*> pure n

694 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)

697 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)

695 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]

698 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]

699+

700+ case likeNat of

701+ -- like S

702+ Just LikeS -> do

703+ sc' <- irSC top vs sc

704+ case usedArgs of

705+ [pv] -> return $ LDefaultCase $ LLet pv

706+ ( LOp

707+ (LMinus (ATInt ITBig))

708+ [ tm

709+ , LConst (BI 1)

710+ ]

711+ )

712+ sc'

713+

714+ _ -> ifail $ "irAlt/LikeS: multiple used args: " ++ show usedArgs

715+

716+ -- like Z

717+ Just LikeZ -> LConstCase (BI 0) <$> irSC top vs sc

718+

719+ -- not like Nat

696− LConCase (-1) n usedArgs <$> irSC top (methodVars `M.union` vs) sc

720+ Nothing -> LConCase (-1) n usedArgs <$> irSC top (methodVars `M.union` vs) sc

697 where

721 where

698 methodVars = case n of

722 methodVars = case n of

699 SN (ImplementationCtorN interfaceName)

723 SN (ImplementationCtorN interfaceName)