006c8f2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #376 from Ralith/simd

006c8f2Edwin Brady13 years ago

README+5−1

compare with master

unifiedsplit

@@ -7,4 +7,8 @@ To install, type 'make'. This will install everything using cabal and

7typecheck the libraries.

9To run the tests, type 'make test' which will execute the test suite, and

10−'make relib', which will typecheck and recompile the standard library.

10+'make relib', which will typecheck and recompile the standard library.

11+

12+Idris has buildtime dependencies on the C libraries llvm-3.3 and libffi. Be sure these are compiled for the same architecture as your Haskell compiler (e.g. 64 bit libraries for 64 bit ghc).

13+

14+Idris has a runtime dependency on libgmp, and on Boehm GC (libgc) when using the LLVM codegen. These are needed for linking into compiled programs, so be sure these are compiled for Idris's default target architecture (usually 64 bit on x86_64 systems).

idris.cabal+2−1

@@ -272,7 +272,8 @@ Executable idris

272 haskeline>=0.7, split, directory,

273 containers, process, transformers, filepath,

274 directory, binary, bytestring, text, pretty,

275− language-java>=0.2.2, libffi, llvm-general>=3.3.0.6 && <3.4

275+ language-java>=0.2.2, libffi, llvm-general==3.3.3.*,

276+ vector, vector-binary-instances

276

277

277 Extensions: MultiParamTypeClasses, FunctionalDependencies,

278 Extensions: MultiParamTypeClasses, FunctionalDependencies,

278 FlexibleInstances, TemplateHaskell

279 FlexibleInstances, TemplateHaskell

src/Core/CaseTree.hs+12−8

@@ -228,17 +228,16 @@ toPat tc tms = evalState (mapM (\x -> toPat' x []) tms) []

228 toPat' (P (TCon t a) n _) args | tc

229 = do args' <- mapM (\x -> toPat' x []) args

230 return $ PCon n t args'

231+ toPat' (Constant (AType (ATInt ITNative))) []

231− toPat' (Constant IType) [] | tc = return $ PCon (UN "Int") 1 []

232+ | tc = return $ PCon (UN "Int") 1 []

232− toPat' (Constant FlType) [] | tc = return $ PCon (UN "Float") 2 []

233+ toPat' (Constant (AType ATFloat)) [] | tc = return $ PCon (UN "Float") 2 []

233 toPat' (Constant ChType) [] | tc = return $ PCon (UN "Char") 3 []

234 toPat' (Constant ChType) [] | tc = return $ PCon (UN "Char") 3 []

234 toPat' (Constant StrType) [] | tc = return $ PCon (UN "String") 4 []

235 toPat' (Constant StrType) [] | tc = return $ PCon (UN "String") 4 []

235 toPat' (Constant PtrType) [] | tc = return $ PCon (UN "Ptr") 5 []

236 toPat' (Constant PtrType) [] | tc = return $ PCon (UN "Ptr") 5 []

237+ toPat' (Constant (AType (ATInt ITBig))) []

236− toPat' (Constant BIType) [] | tc = return $ PCon (UN "Integer") 6 []

238+ | tc = return $ PCon (UN "Integer") 6 []

237− toPat' (Constant B8Type) [] | tc = return $ PCon (UN "Bits8") 7 []

239+ toPat' (Constant (AType (ATInt (ITFixed n)))) []

238− toPat' (Constant B16Type) [] | tc = return $ PCon (UN "Bits16") 8 []

240+ | tc = return $ PCon (UN (fixedN n)) (7 + fromEnum n) [] -- 7-10 inclusive

239− toPat' (Constant B32Type) [] | tc = return $ PCon (UN "Bits32") 9 []

240− toPat' (Constant B64Type) [] | tc = return $ PCon (UN "Bits64") 10 []

241−

242 toPat' (P Bound n _) [] = do ns <- get

241 toPat' (P Bound n _) [] = do ns <- get

243 if n `elem` ns

242 if n `elem` ns

244 then return PAny

243 then return PAny

@@ -248,6 +247,11 @@ toPat tc tms = evalState (mapM (\x -> toPat' x []) tms) []

248 toPat' (Constant x) [] = return $ PConst x

247 toPat' (Constant x) [] = return $ PConst x

249 toPat' _ _ = return PAny

248 toPat' _ _ = return PAny

250

249

250+ fixedN IT8 = "Bits8"

251+ fixedN IT16 = "Bits16"

252+ fixedN IT32 = "Bits32"

253+ fixedN IT64 = "Bits64"

254+

251

255

252data Partition = Cons [Clause]

256data Partition = Cons [Clause]

253 | Vars [Clause]

257 | Vars [Clause]

src/Core/CoreParser.hs+2−1

@@ -36,7 +36,8 @@ idrisDef = haskellDef {

36 "using", "namespace", "class", "instance",

37 "public", "private", "abstract", "implicit",

38 "Int", "Integer", "Float", "Char", "String", "Ptr",

39− "Bits8", "Bits16", "Bits32", "Bits64"]

39+ "Bits8", "Bits16", "Bits32", "Bits64",

40+ "Bits8x16", "Bits16x8", "Bits32x4", "Bits64x2"]

40 }

41 }

42-- | The characters allowed in operator names

43-- | The characters allowed in operator names

src/Core/Evaluate.hs+15−10

@@ -329,11 +329,16 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

329

330 findConst c [] = Nothing

331 findConst c (ConstCase c' v : xs) | c == c' = Just v

332− findConst IType (ConCase n 1 [] v : xs) = Just v

332+ findConst (AType (ATInt ITNative)) (ConCase n 1 [] v : xs) = Just v

333− findConst FlType (ConCase n 2 [] v : xs) = Just v

333+ findConst (AType ATFloat) (ConCase n 2 [] v : xs) = Just v

334 findConst ChType (ConCase n 3 [] v : xs) = Just v

335 findConst StrType (ConCase n 4 [] v : xs) = Just v

336− findConst PtrType (ConCase n 5 [] v : xs) = Just v

336+ findConst PtrType (ConCase n 5 [] v : xs) = Just v

337+ findConst (AType (ATInt ITBig)) (ConCase n 6 [] v : xs) = Just v

338+ findConst (AType (ATInt (ITFixed ity))) (ConCase n tag [] v : xs)

339+ | tag == 7 + fromEnum ity = Just v

340+ findConst (AType (ATInt (ITVec ity count))) (ConCase n tag [] v : xs)

341+ | tag == (fromEnum ity + 1) * 1000 + count = Just v

337 findConst c (_ : xs) = findConst c xs

342 findConst c (_ : xs) = findConst c xs

338

343

339 getValArgs tm = getValArgs' tm []

344 getValArgs tm = getValArgs' tm []

@@ -517,16 +522,16 @@ eval_hnf ctxt statics genv tm = ev [] tm where

517

522

518 findConst c [] = Nothing

523 findConst c [] = Nothing

519 findConst c (ConstCase c' v : xs) | c == c' = Just v

524 findConst c (ConstCase c' v : xs) | c == c' = Just v

520− findConst IType (ConCase n 1 [] v : xs) = Just v

525+ findConst (AType (ATInt ITNative)) (ConCase n 1 [] v : xs) = Just v

521− findConst FlType (ConCase n 2 [] v : xs) = Just v

526+ findConst (AType ATFloat) (ConCase n 2 [] v : xs) = Just v

522 findConst ChType (ConCase n 3 [] v : xs) = Just v

527 findConst ChType (ConCase n 3 [] v : xs) = Just v

523 findConst StrType (ConCase n 4 [] v : xs) = Just v

528 findConst StrType (ConCase n 4 [] v : xs) = Just v

524 findConst PtrType (ConCase n 5 [] v : xs) = Just v

529 findConst PtrType (ConCase n 5 [] v : xs) = Just v

525− findConst BIType (ConCase n 6 [] v : xs) = Just v

530+ findConst (AType (ATInt ITBig)) (ConCase n 6 [] v : xs) = Just v

526− findConst B8Type (ConCase n 7 [] v : xs) = Just v

531+ findConst (AType (ATInt (ITFixed ity))) (ConCase n tag [] v : xs)

527− findConst B16Type (ConCase n 8 [] v : xs) = Just v

532+ | tag == 7 + fromEnum ity = Just v

528− findConst B32Type (ConCase n 9 [] v : xs) = Just v

533+ findConst (AType (ATInt (ITVec ity count))) (ConCase n tag [] v : xs)

529− findConst B64Type (ConCase n 10 [] v : xs) = Just v

534+ | tag == (fromEnum ity + 1) * 1000 + count = Just v

530 findConst c (_ : xs) = findConst c xs

535 findConst c (_ : xs) = findConst c xs

531

536

532 getValArgs (HApp t env args) = (t, env, args)

537 getValArgs (HApp t env args) = (t, env, args)

src/Core/Execute.hs+26−23

@@ -3,9 +3,7 @@ module Core.Execute (execute) where

4import Idris.AbsSyntax

5import Idris.AbsSyntaxTree

6−import IRTS.Lang( IntTy(..)

6+import IRTS.Lang(FType(..))

7− , intTyToConst

8− , FType(..))

10import Idris.Primitives(Prim(..), primitives)

8import Idris.Primitives(Prim(..), primitives)

@@ -387,8 +385,7 @@ chooseAlt _ [] = Nothing

387idrisType :: FType -> ExecVal

385idrisType :: FType -> ExecVal

388idrisType FUnit = EP Ref unitTy EErased

386idrisType FUnit = EP Ref unitTy EErased

389idrisType ft = EConstant (idr ft)

387idrisType ft = EConstant (idr ft)

390− where idr (FInt ty) = intTyToConst ty

388+ where idr (FArith ty) = AType ty

391− idr FDouble = FlType

392 idr FChar = ChType

389 idr FChar = ChType

393 idr FString = StrType

390 idr FString = StrType

394 idr FPtr = PtrType

391 idr FPtr = PtrType

@@ -404,18 +401,24 @@ call (FFun name argTypes retType) args =

404 Just f -> do res <- call' f args retType

401 Just f -> do res <- call' f args retType

405 return . Just . ioWrap $ res

402 return . Just . ioWrap $ res

406 where call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal

403 where call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal

404+ call' (Fun _ h) args (FArith (ATInt ITNative)) = do

407− call' (Fun _ h) args (FInt ITNative) = do res <- execIO $ callFFI h retCInt (prepArgs args)

405+ res <- execIO $ callFFI h retCInt (prepArgs args)

408− return (EConstant (I (fromIntegral res)))

406+ return (EConstant (I (fromIntegral res)))

407+ call' (Fun _ h) args (FArith (ATInt (ITFixed IT8))) = do

409− call' (Fun _ h) args (FInt IT8) = do res <- execIO $ callFFI h retCChar (prepArgs args)

408+ res <- execIO $ callFFI h retCChar (prepArgs args)

410− return (EConstant (B8 (fromIntegral res)))

409+ return (EConstant (B8 (fromIntegral res)))

410+ call' (Fun _ h) args (FArith (ATInt (ITFixed IT16))) = do

411− call' (Fun _ h) args (FInt IT16) = do res <- execIO $ callFFI h retCWchar (prepArgs args)

411+ res <- execIO $ callFFI h retCWchar (prepArgs args)

412− return (EConstant (B16 (fromIntegral res)))

412+ return (EConstant (B16 (fromIntegral res)))

413+ call' (Fun _ h) args (FArith (ATInt (ITFixed IT32))) = do

413− call' (Fun _ h) args (FInt IT32) = do res <- execIO $ callFFI h retCInt (prepArgs args)

414+ res <- execIO $ callFFI h retCInt (prepArgs args)

414− return (EConstant (B32 (fromIntegral res)))

415+ return (EConstant (B32 (fromIntegral res)))

416+ call' (Fun _ h) args (FArith (ATInt (ITFixed IT64))) = do

415− call' (Fun _ h) args (FInt IT64) = do res <- execIO $ callFFI h retCLong (prepArgs args)

417+ res <- execIO $ callFFI h retCLong (prepArgs args)

416− return (EConstant (B64 (fromIntegral res)))

418+ return (EConstant (B64 (fromIntegral res)))

419+ call' (Fun _ h) args (FArith ATFloat) = do

417− call' (Fun _ h) args FDouble = do res <- execIO $ callFFI h retCDouble (prepArgs args)

420+ res <- execIO $ callFFI h retCDouble (prepArgs args)

418− return (EConstant (Fl (realToFrac res)))

421+ return (EConstant (Fl (realToFrac res)))

419 call' (Fun _ h) args FChar = do res <- execIO $ callFFI h retCChar (prepArgs args)

422 call' (Fun _ h) args FChar = do res <- execIO $ callFFI h retCChar (prepArgs args)

420 return (EConstant (Ch (castCCharToChar res)))

423 return (EConstant (Ch (castCCharToChar res)))

421 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)

424 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)

@@ -456,15 +459,15 @@ foreignFromTT t = case (unApplyV t) of

456getFTy :: ExecVal -> Maybe FType

459getFTy :: ExecVal -> Maybe FType

457getFTy (EApp (EP _ (UN "FIntT") _) (EP _ (UN intTy) _)) =

460getFTy (EApp (EP _ (UN "FIntT") _) (EP _ (UN intTy) _)) =

458 case intTy of

461 case intTy of

459− "ITNative" -> Just $ FInt ITNative

462+ "ITNative" -> Just (FArith (ATInt ITNative))

460− "IT8" -> Just $ FInt IT8

463+ "IT8" -> Just (FArith (ATInt (ITFixed IT8)))

461− "IT16" -> Just $ FInt IT16

464+ "IT16" -> Just (FArith (ATInt (ITFixed IT16)))

462− "IT32" -> Just $ FInt IT32

465+ "IT32" -> Just (FArith (ATInt (ITFixed IT32)))

463− "IT64" -> Just $ FInt IT64

466+ "IT64" -> Just (FArith (ATInt (ITFixed IT64)))

464 _ -> Nothing

467 _ -> Nothing

465getFTy (EP _ (UN t) _) =

468getFTy (EP _ (UN t) _) =

466 case t of

469 case t of

467− "FFloat" -> Just FDouble

470+ "FFloat" -> Just (FArith ATFloat)

468 "FChar" -> Just FChar

471 "FChar" -> Just FChar

469 "FString" -> Just FString

472 "FString" -> Just FString

470 "FPtr" -> Just FPtr

473 "FPtr" -> Just FPtr

src/Core/TT.hs+56−18

@@ -25,8 +25,11 @@ import Debug.Trace

25import qualified Data.Map as Map

26import Data.Char

27import Data.List

28+import Data.Vector.Unboxed (Vector)

29+import qualified Data.Vector.Unboxed as V

28import qualified Data.Binary as B

30import qualified Data.Binary as B

29import Data.Binary hiding (get, put)

31import Data.Binary hiding (get, put)

32+import Foreign.Storable (sizeOf)

31import Util.Pretty hiding (Str)

34import Util.Pretty hiding (Str)

@@ -274,12 +277,46 @@ addAlist :: Show a => [(Name, a)] -> Ctxt a -> Ctxt a

274addAlist [] ctxt = ctxt

277addAlist [] ctxt = ctxt

275addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)

278addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)

276

279

277−data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

280+data NativeTy = IT8 | IT16 | IT32 | IT64

281+ deriving (Show, Eq, Ord, Enum)

282+

283+instance Pretty NativeTy where

284+ pretty IT8 = text "Bits8"

285+ pretty IT16 = text "Bits16"

286+ pretty IT32 = text "Bits32"

287+ pretty IT64 = text "Bits64"

288+

289+data IntTy = ITFixed NativeTy | ITNative | ITBig

290+ | ITVec NativeTy Int

291+ deriving (Show, Eq, Ord)

292+

293+data ArithTy = ATInt IntTy | ATFloat -- TODO: Float vectors

294+ deriving (Show, Eq, Ord)

295+

296+instance Pretty ArithTy where

297+ pretty (ATInt ITNative) = text "Int"

298+ pretty (ATInt ITBig) = text "BigInt"

299+ pretty (ATInt (ITFixed n)) = pretty n

300+ pretty (ATInt (ITVec e c)) = pretty e <> text "x" <> (text . show $ c)

301+ pretty ATFloat = text "Float"

302+

303+nativeTyWidth :: NativeTy -> Int

304+nativeTyWidth IT8 = 8

305+nativeTyWidth IT16 = 16

306+nativeTyWidth IT32 = 32

307+nativeTyWidth IT64 = 64

308+

309+{-# DEPRECATED intTyWidth "Non-total function, use nativeTyWidth and appropriate casing" #-}

310+intTyWidth :: IntTy -> Int

311+intTyWidth (ITFixed n) = nativeTyWidth n

312+intTyWidth ITNative = 8 * sizeOf (0 :: Int)

313+intTyWidth ITBig = error "IRTS.Lang.intTyWidth: Big integers have variable width"

279

314

315+data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

280 | B8 Word8 | B16 Word16 | B32 Word32 | B64 Word64

316 | B8 Word8 | B16 Word16 | B32 Word32 | B64 Word64

281− | B8Type | B16Type | B32Type | B64Type

317+ | B8V (Vector Word8) | B16V (Vector Word16)

282−

318+ | B32V (Vector Word32) | B64V (Vector Word64)

319+ | AType ArithTy | ChType | StrType

283 | PtrType | VoidType | Forgot

320 | PtrType | VoidType | Forgot

284 deriving (Eq, Ord)

321 deriving (Eq, Ord)

285{-!

322{-!

@@ -295,18 +332,12 @@ instance Pretty Const where

295 pretty (Fl f) = text . show $ f

332 pretty (Fl f) = text . show $ f

296 pretty (Ch c) = text . show $ c

333 pretty (Ch c) = text . show $ c

297 pretty (Str s) = text s

334 pretty (Str s) = text s

298− pretty IType = text "Int"

335+ pretty (AType a) = pretty a

299− pretty BIType = text "BigInt"

300− pretty FlType = text "Float"

301 pretty ChType = text "Char"

336 pretty ChType = text "Char"

302 pretty StrType = text "String"

337 pretty StrType = text "String"

303 pretty PtrType = text "Ptr"

338 pretty PtrType = text "Ptr"

304 pretty VoidType = text "Void"

339 pretty VoidType = text "Void"

305 pretty Forgot = text "Forgot"

340 pretty Forgot = text "Forgot"

306− pretty B8Type = text "Bits8"

307− pretty B16Type = text "Bits16"

308− pretty B32Type = text "Bits32"

309− pretty B64Type = text "Bits64"

310 pretty (B8 w) = text . show $ w

341 pretty (B8 w) = text . show $ w

311 pretty (B16 w) = text . show $ w

342 pretty (B16 w) = text . show $ w

312 pretty (B32 w) = text . show $ w

343 pretty (B32 w) = text . show $ w

@@ -728,6 +759,11 @@ type WkEnv = WkEnvTT Name

728instance (Eq n, Show n) => Show (TT n) where

759instance (Eq n, Show n) => Show (TT n) where

729 show t = showEnv [] t

760 show t = showEnv [] t

730

761

762+itBitsName IT8 = "Bits8"

763+itBitsName IT16 = "Bits16"

764+itBitsName IT32 = "Bits32"

765+itBitsName IT64 = "Bits64"

766+

731instance Show Const where

767instance Show Const where

732 show (I i) = show i

768 show (I i) = show i

733 show (BI i) = show i ++ "L"

769 show (BI i) = show i ++ "L"

@@ -738,16 +774,18 @@ instance Show Const where

738 show (B16 x) = show x

774 show (B16 x) = show x

739 show (B32 x) = show x

775 show (B32 x) = show x

740 show (B64 x) = show x

776 show (B64 x) = show x

741− show IType = "Int"

777+ show (B8V x) = "<" ++ intercalate "," (map show (V.toList x)) ++ ">"

742− show BIType = "Integer"

778+ show (B16V x) = "<" ++ intercalate "," (map show (V.toList x)) ++ ">"

743− show FlType = "Float"

779+ show (B32V x) = "<" ++ intercalate "," (map show (V.toList x)) ++ ">"

780+ show (B64V x) = "<" ++ intercalate "," (map show (V.toList x)) ++ ">"

781+ show (AType ATFloat) = "Float"

782+ show (AType (ATInt ITBig)) = "Integer"

783+ show (AType (ATInt ITNative)) = "Int"

784+ show (AType (ATInt (ITFixed it))) = itBitsName it

785+ show (AType (ATInt (ITVec it c))) = itBitsName it ++ "x" ++ show c

744 show ChType = "Char"

786 show ChType = "Char"

745 show StrType = "String"

787 show StrType = "String"

746 show PtrType = "Ptr"

788 show PtrType = "Ptr"

747− show B8Type = "Bits8"

748− show B16Type = "Bits16"

749− show B32Type = "Bits32"

750− show B64Type = "Bits64"

751 show VoidType = "Void"

789 show VoidType = "Void"

752

790

753showEnv env t = showEnv' env t False

791showEnv env t = showEnv' env t False

src/Core/Typecheck.hs+12−7

@@ -5,6 +5,7 @@ module Core.Typecheck where

6import Control.Monad.State

7import Debug.Trace

8+import qualified Data.Vector.Unboxed as V (length)

9import Core.TT

10import Core.TT

10import Core.Evaluate

11import Core.Evaluate

@@ -98,15 +99,19 @@ check' holes ctxt env top = chk env top where

98 return (TType (UVar v), TType (UVar (v+1)))

99 return (TType (UVar v), TType (UVar (v+1)))

99 chk env (RConstant Forgot) = return (Erased, Erased)

100 chk env (RConstant Forgot) = return (Erased, Erased)

100 chk env (RConstant c) = return (Constant c, constType c)

101 chk env (RConstant c) = return (Constant c, constType c)

101− where constType (I _) = Constant IType

102+ where constType (I _) = Constant (AType (ATInt ITNative))

102− constType (BI _) = Constant BIType

103+ constType (BI _) = Constant (AType (ATInt ITBig))

103− constType (Fl _) = Constant FlType

104+ constType (Fl _) = Constant (AType ATFloat)

104 constType (Ch _) = Constant ChType

105 constType (Ch _) = Constant ChType

105 constType (Str _) = Constant StrType

106 constType (Str _) = Constant StrType

106− constType (B8 _) = Constant B8Type

107+ constType (B8 _) = Constant (AType (ATInt (ITFixed IT8)))

107− constType (B16 _) = Constant B16Type

108+ constType (B16 _) = Constant (AType (ATInt (ITFixed IT16)))

108− constType (B32 _) = Constant B32Type

109+ constType (B32 _) = Constant (AType (ATInt (ITFixed IT32)))

109− constType (B64 _) = Constant B64Type

110+ constType (B64 _) = Constant (AType (ATInt (ITFixed IT64)))

111+ constType (B8V a) = Constant (AType (ATInt (ITVec IT8 (V.length a))))

112+ constType (B16V a) = Constant (AType (ATInt (ITVec IT16 (V.length a))))

113+ constType (B32V a) = Constant (AType (ATInt (ITVec IT32 (V.length a))))

114+ constType (B64V a) = Constant (AType (ATInt (ITVec IT64 (V.length a))))

110 constType Forgot = Erased

115 constType Forgot = Erased

111 constType _ = TType (UVal 0)

116 constType _ = TType (UVal 0)

112 chk env (RForce t) = do (_, ty) <- chk env t

117 chk env (RForce t) = do (_, ty) <- chk env t

src/IRTS/CodegenC.hs+88−77

@@ -229,39 +229,41 @@ bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); assert(0);

229

230

231

232−c_irts (FInt ITNative) l x = l ++ "MKINT((i_int)(" ++ x ++ "))"

232+c_irts (FArith (ATInt ITNative)) l x = l ++ "MKINT((i_int)(" ++ x ++ "))"

233+c_irts (FArith (ATInt (ITFixed ity))) l x

233−c_irts (FInt ty) l x = l ++ "idris_b" ++ show (intTyWidth ty) ++ "const(vm, " ++ x ++ ")"

234+ = l ++ "idris_b" ++ show (nativeTyWidth ity) ++ "const(vm, " ++ x ++ ")"

234c_irts FChar l x = l ++ "MKINT((i_int)(" ++ x ++ "))"

235c_irts FChar l x = l ++ "MKINT((i_int)(" ++ x ++ "))"

235c_irts FString l x = l ++ "MKSTR(vm, " ++ x ++ ")"

236c_irts FString l x = l ++ "MKSTR(vm, " ++ x ++ ")"

236c_irts FUnit l x = x

237c_irts FUnit l x = x

237c_irts FPtr l x = l ++ "MKPTR(vm, " ++ x ++ ")"

238c_irts FPtr l x = l ++ "MKPTR(vm, " ++ x ++ ")"

238−c_irts FDouble l x = l ++ "MKFLOAT(vm, " ++ x ++ ")"

239+c_irts (FArith ATFloat) l x = l ++ "MKFLOAT(vm, " ++ x ++ ")"

239c_irts FAny l x = l ++ x

240c_irts FAny l x = l ++ x

240

241

241−irts_c (FInt ITNative) x = "GETINT(" ++ x ++ ")"

242+irts_c (FArith (ATInt ITNative)) x = "GETINT(" ++ x ++ ")"

242−irts_c (FInt ty) x = "(" ++ x ++ "->info.bits" ++ show (intTyWidth ty) ++ ")"

243+irts_c (FArith (ATInt (ITFixed ity))) x

244+ = "(" ++ x ++ "->info.bits" ++ show (nativeTyWidth ity) ++ ")"

243irts_c FChar x = "GETINT(" ++ x ++ ")"

245irts_c FChar x = "GETINT(" ++ x ++ ")"

244irts_c FString x = "GETSTR(" ++ x ++ ")"

246irts_c FString x = "GETSTR(" ++ x ++ ")"

245irts_c FUnit x = x

247irts_c FUnit x = x

246irts_c FPtr x = "GETPTR(" ++ x ++ ")"

248irts_c FPtr x = "GETPTR(" ++ x ++ ")"

247−irts_c FDouble x = "GETFLOAT(" ++ x ++ ")"

249+irts_c (FArith ATFloat) x = "GETFLOAT(" ++ x ++ ")"

248irts_c FAny x = x

250irts_c FAny x = x

249

251

250−bitOp v op ty args = v ++ "idris_b" ++ show (intTyWidth ty) ++ op ++ "(vm, " ++ intercalate ", " (map creg args) ++ ")"

252+bitOp v op ty args = v ++ "idris_b" ++ show (nativeTyWidth ty) ++ op ++ "(vm, " ++ intercalate ", " (map creg args) ++ ")"

251

253

252bitCoerce v op input output arg

254bitCoerce v op input output arg

253− = v ++ "idris_b" ++ show (intTyWidth input) ++ op ++ show (intTyWidth output) ++ "(vm, " ++ creg arg ++ ")"

255+ = v ++ "idris_b" ++ show (nativeTyWidth input) ++ op ++ show (nativeTyWidth output) ++ "(vm, " ++ creg arg ++ ")"

254

256

255−signedTy :: IntTy -> String

257+signedTy :: NativeTy -> String

256−signedTy t = "int" ++ show (intTyWidth t) ++ "_t"

258+signedTy t = "int" ++ show (nativeTyWidth t) ++ "_t"

257

259

258−doOp v (LPlus ITNative) [l, r] = v ++ "ADD(" ++ creg l ++ ", " ++ creg r ++ ")"

260+doOp v (LPlus (ATInt ITNative)) [l, r] = v ++ "ADD(" ++ creg l ++ ", " ++ creg r ++ ")"

259−doOp v (LMinus ITNative) [l, r] = v ++ "INTOP(-," ++ creg l ++ ", " ++ creg r ++ ")"

261+doOp v (LMinus (ATInt ITNative)) [l, r] = v ++ "INTOP(-," ++ creg l ++ ", " ++ creg r ++ ")"

260−doOp v (LTimes ITNative) [l, r] = v ++ "MULT(" ++ creg l ++ ", " ++ creg r ++ ")"

262+doOp v (LTimes (ATInt ITNative)) [l, r] = v ++ "MULT(" ++ creg l ++ ", " ++ creg r ++ ")"

261doOp v (LUDiv ITNative) [l, r] = v ++ "UINTOP(/," ++ creg l ++ ", " ++ creg r ++ ")"

263doOp v (LUDiv ITNative) [l, r] = v ++ "UINTOP(/," ++ creg l ++ ", " ++ creg r ++ ")"

262−doOp v (LSDiv ITNative) [l, r] = v ++ "INTOP(/," ++ creg l ++ ", " ++ creg r ++ ")"

264+doOp v (LSDiv (ATInt ITNative)) [l, r] = v ++ "INTOP(/," ++ creg l ++ ", " ++ creg r ++ ")"

263doOp v (LURem ITNative) [l, r] = v ++ "UINTOP(%," ++ creg l ++ ", " ++ creg r ++ ")"

265doOp v (LURem ITNative) [l, r] = v ++ "UINTOP(%," ++ creg l ++ ", " ++ creg r ++ ")"

264−doOp v (LSRem ITNative) [l, r] = v ++ "INTOP(%," ++ creg l ++ ", " ++ creg r ++ ")"

266+doOp v (LSRem (ATInt ITNative)) [l, r] = v ++ "INTOP(%," ++ creg l ++ ", " ++ creg r ++ ")"

265doOp v (LAnd ITNative) [l, r] = v ++ "INTOP(&," ++ creg l ++ ", " ++ creg r ++ ")"

267doOp v (LAnd ITNative) [l, r] = v ++ "INTOP(&," ++ creg l ++ ", " ++ creg r ++ ")"

266doOp v (LOr ITNative) [l, r] = v ++ "INTOP(|," ++ creg l ++ ", " ++ creg r ++ ")"

268doOp v (LOr ITNative) [l, r] = v ++ "INTOP(|," ++ creg l ++ ", " ++ creg r ++ ")"

267doOp v (LXOr ITNative) [l, r] = v ++ "INTOP(^," ++ creg l ++ ", " ++ creg r ++ ")"

269doOp v (LXOr ITNative) [l, r] = v ++ "INTOP(^," ++ creg l ++ ", " ++ creg r ++ ")"

@@ -269,34 +271,34 @@ doOp v (LSHL ITNative) [l, r] = v ++ "INTOP(<<," ++ creg l ++ ", " ++ creg r ++

269doOp v (LLSHR ITNative) [l, r] = v ++ "UINTOP(>>," ++ creg l ++ ", " ++ creg r ++ ")"

271doOp v (LLSHR ITNative) [l, r] = v ++ "UINTOP(>>," ++ creg l ++ ", " ++ creg r ++ ")"

270doOp v (LASHR ITNative) [l, r] = v ++ "INTOP(>>," ++ creg l ++ ", " ++ creg r ++ ")"

272doOp v (LASHR ITNative) [l, r] = v ++ "INTOP(>>," ++ creg l ++ ", " ++ creg r ++ ")"

271doOp v (LCompl ITNative) [x] = v ++ "INTOP(~," ++ creg x ++ ")"

273doOp v (LCompl ITNative) [x] = v ++ "INTOP(~," ++ creg x ++ ")"

272−doOp v (LEq ITNative) [l, r] = v ++ "INTOP(==," ++ creg l ++ ", " ++ creg r ++ ")"

274+doOp v (LEq (ATInt ITNative)) [l, r] = v ++ "INTOP(==," ++ creg l ++ ", " ++ creg r ++ ")"

273−doOp v (LLt ITNative) [l, r] = v ++ "INTOP(<," ++ creg l ++ ", " ++ creg r ++ ")"

275+doOp v (LLt (ATInt ITNative)) [l, r] = v ++ "INTOP(<," ++ creg l ++ ", " ++ creg r ++ ")"

274−doOp v (LLe ITNative) [l, r] = v ++ "INTOP(<=," ++ creg l ++ ", " ++ creg r ++ ")"

276+doOp v (LLe (ATInt ITNative)) [l, r] = v ++ "INTOP(<=," ++ creg l ++ ", " ++ creg r ++ ")"

275−doOp v (LGt ITNative) [l, r] = v ++ "INTOP(>," ++ creg l ++ ", " ++ creg r ++ ")"

277+doOp v (LGt (ATInt ITNative)) [l, r] = v ++ "INTOP(>," ++ creg l ++ ", " ++ creg r ++ ")"

276−doOp v (LGe ITNative) [l, r] = v ++ "INTOP(>=," ++ creg l ++ ", " ++ creg r ++ ")"

278+doOp v (LGe (ATInt ITNative)) [l, r] = v ++ "INTOP(>=," ++ creg l ++ ", " ++ creg r ++ ")"

277−

279+

278−doOp v LFPlus [l, r] = v ++ "FLOATOP(+," ++ creg l ++ ", " ++ creg r ++ ")"

280+doOp v (LPlus ATFloat) [l, r] = v ++ "FLOATOP(+," ++ creg l ++ ", " ++ creg r ++ ")"

279−doOp v LFMinus [l, r] = v ++ "FLOATOP(-," ++ creg l ++ ", " ++ creg r ++ ")"

281+doOp v (LMinus ATFloat) [l, r] = v ++ "FLOATOP(-," ++ creg l ++ ", " ++ creg r ++ ")"

280−doOp v LFTimes [l, r] = v ++ "FLOATOP(*," ++ creg l ++ ", " ++ creg r ++ ")"

282+doOp v (LTimes ATFloat) [l, r] = v ++ "FLOATOP(*," ++ creg l ++ ", " ++ creg r ++ ")"

281−doOp v LFDiv [l, r] = v ++ "FLOATOP(/," ++ creg l ++ ", " ++ creg r ++ ")"

283+doOp v (LSDiv ATFloat) [l, r] = v ++ "FLOATOP(/," ++ creg l ++ ", " ++ creg r ++ ")"

282−doOp v LFEq [l, r] = v ++ "FLOATBOP(==," ++ creg l ++ ", " ++ creg r ++ ")"

284+doOp v (LEq ATFloat) [l, r] = v ++ "FLOATBOP(==," ++ creg l ++ ", " ++ creg r ++ ")"

283−doOp v LFLt [l, r] = v ++ "FLOATBOP(<," ++ creg l ++ ", " ++ creg r ++ ")"

285+doOp v (LLt ATFloat) [l, r] = v ++ "FLOATBOP(<," ++ creg l ++ ", " ++ creg r ++ ")"

284−doOp v LFLe [l, r] = v ++ "FLOATBOP(<=," ++ creg l ++ ", " ++ creg r ++ ")"

286+doOp v (LLe ATFloat) [l, r] = v ++ "FLOATBOP(<=," ++ creg l ++ ", " ++ creg r ++ ")"

285−doOp v LFGt [l, r] = v ++ "FLOATBOP(>," ++ creg l ++ ", " ++ creg r ++ ")"

287+doOp v (LGt ATFloat) [l, r] = v ++ "FLOATBOP(>," ++ creg l ++ ", " ++ creg r ++ ")"

286−doOp v LFGe [l, r] = v ++ "FLOATBOP(>=," ++ creg l ++ ", " ++ creg r ++ ")"

288+doOp v (LGe ATFloat) [l, r] = v ++ "FLOATBOP(>=," ++ creg l ++ ", " ++ creg r ++ ")"

287

289

288doOp v (LIntFloat ITBig) [x] = v ++ "idris_castBigFloat(vm, " ++ creg x ++ ")"

290doOp v (LIntFloat ITBig) [x] = v ++ "idris_castBigFloat(vm, " ++ creg x ++ ")"

289doOp v (LFloatInt ITBig) [x] = v ++ "idris_castFloatBig(vm, " ++ creg x ++ ")"

291doOp v (LFloatInt ITBig) [x] = v ++ "idris_castFloatBig(vm, " ++ creg x ++ ")"

290−doOp v (LPlus ITBig) [l, r] = v ++ "idris_bigPlus(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

292+doOp v (LPlus (ATInt ITBig)) [l, r] = v ++ "idris_bigPlus(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

291−doOp v (LMinus ITBig) [l, r] = v ++ "idris_bigMinus(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

293+doOp v (LMinus (ATInt ITBig)) [l, r] = v ++ "idris_bigMinus(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

292−doOp v (LTimes ITBig) [l, r] = v ++ "idris_bigTimes(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

294+doOp v (LTimes (ATInt ITBig)) [l, r] = v ++ "idris_bigTimes(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

293−doOp v (LSDiv ITBig) [l, r] = v ++ "idris_bigDivide(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

295+doOp v (LSDiv (ATInt ITBig)) [l, r] = v ++ "idris_bigDivide(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

294−doOp v (LSRem ITBig) [l, r] = v ++ "idris_bigMod(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

296+doOp v (LSRem (ATInt ITBig)) [l, r] = v ++ "idris_bigMod(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

295−doOp v (LEq ITBig) [l, r] = v ++ "idris_bigEq(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

297+doOp v (LEq (ATInt ITBig)) [l, r] = v ++ "idris_bigEq(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

296−doOp v (LLt ITBig) [l, r] = v ++ "idris_bigLt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

298+doOp v (LLt (ATInt ITBig)) [l, r] = v ++ "idris_bigLt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

297−doOp v (LLe ITBig) [l, r] = v ++ "idris_bigLe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

299+doOp v (LLe (ATInt ITBig)) [l, r] = v ++ "idris_bigLe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

298−doOp v (LGt ITBig) [l, r] = v ++ "idris_bigGt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

300+doOp v (LGt (ATInt ITBig)) [l, r] = v ++ "idris_bigGt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

299−doOp v (LGe ITBig) [l, r] = v ++ "idris_bigGe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

301+doOp v (LGe (ATInt ITBig)) [l, r] = v ++ "idris_bigGe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

300

302

301doOp v LStrConcat [l,r] = v ++ "idris_concat(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

303doOp v LStrConcat [l,r] = v ++ "idris_concat(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

302doOp v LStrLt [l,r] = v ++ "idris_strlt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

304doOp v LStrLt [l,r] = v ++ "idris_strlt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"

@@ -318,43 +320,52 @@ doOp v LReadStr [x] = v ++ "idris_readStr(vm, GETPTR(" ++ creg x ++ "))"

318doOp _ LPrintNum [x] = "printf(\"%ld\\n\", GETINT(" ++ creg x ++ "))"

320doOp _ LPrintNum [x] = "printf(\"%ld\\n\", GETINT(" ++ creg x ++ "))"

319doOp _ LPrintStr [x] = "fputs(GETSTR(" ++ creg x ++ "), stdout)"

321doOp _ LPrintStr [x] = "fputs(GETSTR(" ++ creg x ++ "), stdout)"

320

322

321−doOp v (LLt ty) [x, y] = bitOp v "Lt" ty [x, y]

323+doOp v (LLt (ATInt (ITFixed ty))) [x, y] = bitOp v "Lt" ty [x, y]

322−doOp v (LLe ty) [x, y] = bitOp v "Lte" ty [x, y]

324+doOp v (LLe (ATInt (ITFixed ty))) [x, y] = bitOp v "Lte" ty [x, y]

323−doOp v (LEq ty) [x, y] = bitOp v "Eq" ty [x, y]

325+doOp v (LEq (ATInt (ITFixed ty))) [x, y] = bitOp v "Eq" ty [x, y]

324−doOp v (LGe ty) [x, y] = bitOp v "Gte" ty [x, y]

326+doOp v (LGe (ATInt (ITFixed ty))) [x, y] = bitOp v "Gte" ty [x, y]

325−doOp v (LGt ty) [x, y] = bitOp v "Gt" ty [x, y]

327+doOp v (LGt (ATInt (ITFixed ty))) [x, y] = bitOp v "Gt" ty [x, y]

326−

328+

327−doOp v (LSHL ty) [x, y] = bitOp v "Shl" ty [x, y]

329+doOp v (LSHL (ITFixed ty)) [x, y] = bitOp v "Shl" ty [x, y]

328−doOp v (LLSHR ty) [x, y] = bitOp v "LShr" ty [x, y]

330+doOp v (LLSHR (ITFixed ty)) [x, y] = bitOp v "LShr" ty [x, y]

329−doOp v (LASHR ty) [x, y] = bitOp v "AShr" ty [x, y]

331+doOp v (LASHR (ITFixed ty)) [x, y] = bitOp v "AShr" ty [x, y]

330−doOp v (LAnd ty) [x, y] = bitOp v "And" ty [x, y]

332+doOp v (LAnd (ITFixed ty)) [x, y] = bitOp v "And" ty [x, y]

331−doOp v (LOr ty) [x, y] = bitOp v "Or" ty [x, y]

333+doOp v (LOr (ITFixed ty)) [x, y] = bitOp v "Or" ty [x, y]

332−doOp v (LXOr ty) [x, y] = bitOp v "Xor" ty [x, y]

334+doOp v (LXOr (ITFixed ty)) [x, y] = bitOp v "Xor" ty [x, y]

333−doOp v (LCompl ty) [x] = bitOp v "Compl" ty [x]

335+doOp v (LCompl (ITFixed ty)) [x] = bitOp v "Compl" ty [x]

334−

336+

335−doOp v (LPlus ty) [x, y] = bitOp v "Plus" ty [x, y]

337+doOp v (LPlus (ATInt (ITFixed ty))) [x, y] = bitOp v "Plus" ty [x, y]

336−doOp v (LMinus ty) [x, y] = bitOp v "Minus" ty [x, y]

338+doOp v (LMinus (ATInt (ITFixed ty))) [x, y] = bitOp v "Minus" ty [x, y]

337−doOp v (LTimes ty) [x, y] = bitOp v "Times" ty [x, y]

339+doOp v (LTimes (ATInt (ITFixed ty))) [x, y] = bitOp v "Times" ty [x, y]

338−doOp v (LUDiv ty) [x, y] = bitOp v "UDiv" ty [x, y]

340+doOp v (LUDiv (ITFixed ty)) [x, y] = bitOp v "UDiv" ty [x, y]

339−doOp v (LSDiv ty) [x, y] = bitOp v "SDiv" ty [x, y]

341+doOp v (LSDiv (ATInt (ITFixed ty))) [x, y] = bitOp v "SDiv" ty [x, y]

340−doOp v (LURem ty) [x, y] = bitOp v "URem" ty [x, y]

342+doOp v (LURem (ITFixed ty)) [x, y] = bitOp v "URem" ty [x, y]

341−doOp v (LSRem ty) [x, y] = bitOp v "SRem" ty [x, y]

343+doOp v (LSRem (ATInt (ITFixed ty))) [x, y] = bitOp v "SRem" ty [x, y]

342−

344+

345+doOp v (LSExt (ITFixed from) ITBig) [x]

343−doOp v (LSExt from ITBig) [x] = v ++ "MKBIGSI(vm, (" ++ signedTy from ++ ")" ++ creg x ++ "->info.bits" ++ show (intTyWidth from) ++ ")"

346+ = v ++ "MKBIGSI(vm, (" ++ signedTy from ++ ")" ++ creg x ++ "->info.bits" ++ show (nativeTyWidth from) ++ ")"

347+doOp v (LSExt ITNative (ITFixed to)) [x]

344−doOp v (LSExt ITNative to) [x] = v ++ "idris_b" ++ show (intTyWidth to) ++ "const(vm, GETINT(" ++ creg x ++ "))"

348+ = v ++ "idris_b" ++ show (nativeTyWidth to) ++ "const(vm, GETINT(" ++ creg x ++ "))"

349+doOp v (LSExt (ITFixed from) ITNative) [x]

345−doOp v (LSExt from ITNative) [x] = v ++ "MKINT((i_int)((" ++ signedTy from ++ ")" ++ creg x ++ "->info.bits" ++ show (intTyWidth from) ++ "))"

350+ = v ++ "MKINT((i_int)((" ++ signedTy from ++ ")" ++ creg x ++ "->info.bits" ++ show (nativeTyWidth from) ++ "))"

346−doOp v (LSExt from to) [x]

351+doOp v (LSExt (ITFixed from) (ITFixed to)) [x]

347− | intTyWidth from < intTyWidth to = bitCoerce v "S" from to x

352+ | nativeTyWidth from < nativeTyWidth to = bitCoerce v "S" from to x

353+doOp v (LZExt ITNative (ITFixed to)) [x]

348−doOp v (LZExt ITNative to) [x] = v ++ "idris_b" ++ show (intTyWidth to) ++ "const(vm, (uintptr_t)GETINT(" ++ creg x ++ ")"

354+ = v ++ "idris_b" ++ show (nativeTyWidth to) ++ "const(vm, (uintptr_t)GETINT(" ++ creg x ++ ")"

355+doOp v (LZExt (ITFixed from) ITNative) [x]

349−doOp v (LZExt from ITNative) [x] = v ++ "MKINT((i_int)" ++ creg x ++ "->info.bits" ++ show (intTyWidth from) ++ ")"

356+ = v ++ "MKINT((i_int)" ++ creg x ++ "->info.bits" ++ show (nativeTyWidth from) ++ ")"

357+doOp v (LZExt (ITFixed from) ITBig) [x]

350−doOp v (LZExt from ITBig) [x] = v ++ "MKBIGUI(vm, " ++ creg x ++ "->info.bits" ++ show (intTyWidth from) ++ ")"

358+ = v ++ "MKBIGUI(vm, " ++ creg x ++ "->info.bits" ++ show (nativeTyWidth from) ++ ")"

351−doOp v (LZExt from to) [x]

359+doOp v (LZExt (ITFixed from) (ITFixed to)) [x]

352− | intTyWidth from < intTyWidth to = bitCoerce v "Z" from to x

360+ | nativeTyWidth from < nativeTyWidth to = bitCoerce v "Z" from to x

361+doOp v (LTrunc ITNative (ITFixed to)) [x]

353−doOp v (LTrunc ITNative to) [x] = v ++ "idris_b" ++ show (intTyWidth to) ++ "const(vm, GETINT(" ++ creg x ++ "))"

362+ = v ++ "idris_b" ++ show (nativeTyWidth to) ++ "const(vm, GETINT(" ++ creg x ++ "))"

363+doOp v (LTrunc (ITFixed from) ITNative) [x]

354−doOp v (LTrunc from ITNative) [x] = v ++ "MKINT((i_int)" ++ creg x ++ "->info.bits" ++ show (intTyWidth from) ++ ")"

364+ = v ++ "MKINT((i_int)" ++ creg x ++ "->info.bits" ++ show (nativeTyWidth from) ++ ")"

365+doOp v (LTrunc ITBig (ITFixed to)) [x]

355−doOp v (LTrunc ITBig to) [x] = v ++ "idris_b" ++ show (intTyWidth to) ++ "const(vm, ISINT(" ++ creg x ++ ") ? GETINT(" ++ creg x ++ ") : mpz_get_ui(GETMPZ(" ++ creg x ++ ")))"

366+ = v ++ "idris_b" ++ show (nativeTyWidth to) ++ "const(vm, ISINT(" ++ creg x ++ ") ? GETINT(" ++ creg x ++ ") : mpz_get_ui(GETMPZ(" ++ creg x ++ ")))"

356−doOp v (LTrunc from to) [x]

367+doOp v (LTrunc (ITFixed from) (ITFixed to)) [x]

357− | intTyWidth from > intTyWidth to = bitCoerce v "T" from to x

368+ | nativeTyWidth from > nativeTyWidth to = bitCoerce v "T" from to x

358

369

359doOp v LFExp [x] = v ++ flUnOp "exp" (creg x)

370doOp v LFExp [x] = v ++ flUnOp "exp" (creg x)

360doOp v LFLog [x] = v ++ flUnOp "log" (creg x)

371doOp v LFLog [x] = v ++ flUnOp "log" (creg x)

src/IRTS/CodegenJava.hs+79−79

@@ -472,17 +472,17 @@ longType :: ClassType

472longType = ClassType [(Ident "Long", [])]

473

474nextIntTy :: IntTy -> IntTy

475−nextIntTy IT8 = IT16

475+nextIntTy (ITFixed IT8) = (ITFixed IT16)

476−nextIntTy IT16 = IT32

476+nextIntTy (ITFixed IT16) = (ITFixed IT32)

477−nextIntTy IT32 = IT64

477+nextIntTy (ITFixed IT32) = (ITFixed IT64)

478−nextIntTy IT64 = IT64

478+nextIntTy (ITFixed IT64) = (ITFixed IT64)

479−nextIntTy ITNative = IT64

479+nextIntTy ITNative = (ITFixed IT64)

480

481intTyToIdent :: IntTy -> Ident

482−intTyToIdent IT8 = Ident "Byte"

482+intTyToIdent (ITFixed IT8) = Ident "Byte"

483−intTyToIdent IT16 = Ident "Short"

483+intTyToIdent (ITFixed IT16) = Ident "Short"

484−intTyToIdent IT32 = Ident "Integer"

484+intTyToIdent (ITFixed IT32) = Ident "Integer"

485−intTyToIdent IT64 = Ident "Long"

485+intTyToIdent (ITFixed IT64) = Ident "Long"

486intTyToIdent ITNative = Ident "Integer"

487intTyToIdent ITBig = Ident "BigInteger"

488

@@ -490,17 +490,17 @@ intTyToClass :: IntTy -> ClassType

490intTyToClass ty = ClassType [(intTyToIdent ty, [])]

491

492intTyToMethod :: IntTy -> String

493−intTyToMethod IT8 = "byteValue"

493+intTyToMethod (ITFixed IT8) = "byteValue"

494−intTyToMethod IT16 = "shortValue"

494+intTyToMethod (ITFixed IT16) = "shortValue"

495−intTyToMethod IT32 = "intValue"

495+intTyToMethod (ITFixed IT32) = "intValue"

496−intTyToMethod IT64 = "longValue"

496+intTyToMethod (ITFixed IT64) = "longValue"

497intTyToMethod ITNative = "intValue"

498

499intTyToPrimTy :: IntTy -> PrimType

500−intTyToPrimTy IT8 = ByteT

500+intTyToPrimTy (ITFixed IT8) = ByteT

501−intTyToPrimTy IT16 = ShortT

501+intTyToPrimTy (ITFixed IT16) = ShortT

502−intTyToPrimTy IT32 = IntT

502+intTyToPrimTy (ITFixed IT32) = IntT

503−intTyToPrimTy IT64 = LongT

503+intTyToPrimTy (ITFixed IT64) = LongT

504intTyToPrimTy ITNative = IntT

505

506bigIntegerType :: ClassType

@@ -995,24 +995,24 @@ mkStringAtIndex var indexExp =

995 <$> mkVarAccess (Just stringType) var

996

997mkForeignType :: FType -> Maybe ClassType

998−mkForeignType (FInt ty) = return (intTyToClass ty)

998+mkForeignType (FArith (ATInt ity)) = return (intTyToClass ity)

999+mkForeignType (FArith ATFloat) = return doubleType

999mkForeignType FChar = return integerType

1000mkForeignType FChar = return integerType

1000mkForeignType FString = return stringType

1001mkForeignType FString = return stringType

1001mkForeignType FPtr = return objectType

1002mkForeignType FPtr = return objectType

1002−mkForeignType FDouble = return doubleType

1003mkForeignType FAny = return objectType

1004mkForeignType FUnit = Nothing

1005

1006mkForeignVarAccess :: FType -> LVar -> CodeGeneration Exp

1007−mkForeignVarAccess (FInt ty) var =

1007+mkForeignVarAccess (FArith (ATInt ty)) var =

1008 (\ var -> MethodInv $ PrimaryMethodCall var

1009 []

1010 (Ident (intTyToMethod ty))

1011 []

1012 )

1013 <$> mkVarAccess (Just $ intTyToClass ty) var

1014−mkForeignVarAccess FChar var = Cast (PrimType CharT) <$> mkForeignVarAccess (FInt IT32) var

1014+mkForeignVarAccess FChar var = Cast (PrimType CharT) <$> mkForeignVarAccess (FArith (ATInt (ITFixed IT32))) var

1015−mkForeignVarAccess FDouble var =

1015+mkForeignVarAccess (FArith ATFloat) var =

1016 (\ var -> MethodInv $ PrimaryMethodCall (var)

1017 []

1018 (Ident "doubleValue")

@@ -1022,13 +1022,13 @@ mkForeignVarAccess FDouble var =

1022mkForeignVarAccess otherType var = mkVarAccess (mkForeignType otherType) var

1023

1024mkFromForeignType :: FType -> Exp -> Exp

1025−mkFromForeignType (FInt ty) from =

1025+mkFromForeignType (FArith (ATInt ty)) from =

1026 MethodInv $ TypeMethodCall (J.Name [intTyToIdent ty])

1027 []

1028 (Ident "valueOf")

1029 [from]

1030−mkFromForeignType FChar from = mkFromForeignType (FInt IT32) from

1030+mkFromForeignType FChar from = mkFromForeignType (FArith (ATInt (ITFixed IT32))) from

1031−mkFromForeignType FDouble from =

1031+mkFromForeignType (FArith ATFloat) from =

1032 MethodInv $ TypeMethodCall (J.Name [Ident "Double"])

1033 []

1034 (Ident "valueOf")

@@ -1269,78 +1269,78 @@ mkExp (SConst (BI x)) =

1269mkExp (SConst (Fl x)) = return $ mkPrimitive "Double" (Double x)

1270mkExp (SConst (Ch x)) = return $ mkPrimitive "Integer" (Char x)

1271mkExp (SConst (Str x)) = return $ Lit $ String x

1272−mkExp (SConst IType) = return $ mkClass integerType

1272+mkExp (SConst (AType (ATInt ITNative))) = return $ mkClass integerType

1273−mkExp (SConst BIType) = return $ mkClass bigIntegerType

1273+mkExp (SConst (AType (ATInt ITBig))) = return $ mkClass bigIntegerType

1274−mkExp (SConst FlType) = return $ mkClass doubleType

1274+mkExp (SConst (AType ATFloat)) = return $ mkClass doubleType

1275mkExp (SConst ChType) = return $ mkClass charType

1276mkExp (SConst StrType) = return $ mkClass stringType

1277mkExp (SConst (B8 x)) = return $ mkPrimitive "Byte" (String (show x))

1278mkExp (SConst (B16 x)) = return $ mkPrimitive "Short" (String (show x))

1279mkExp (SConst (B32 x)) = return $ mkPrimitive "Integer" (Int (toInteger x))

1280mkExp (SConst (B64 x)) = return $ mkPrimitive "Long" (String (show x))

1281−mkExp (SConst (B8Type))= return $ mkClass byteType

1281+mkExp (SConst (AType (ATInt (ITFixed IT8)))) = return $ mkClass byteType

1282−mkExp (SConst (B16Type)) = return $ mkClass shortType

1282+mkExp (SConst (AType (ATInt (ITFixed IT16)))) = return $ mkClass shortType

1283−mkExp (SConst (B32Type)) = return $ mkClass integerType

1283+mkExp (SConst (AType (ATInt (ITFixed IT32)))) = return $ mkClass integerType

1284−mkExp (SConst (B64Type)) = return $ mkClass longType

1284+mkExp (SConst (AType (ATInt (ITFixed IT64)))) = return $ mkClass longType

1285mkExp (SConst (PtrType)) = return $ mkClass objectType

1286mkExp (SConst (VoidType)) = return $ mkClass voidType

1287mkExp (SConst (Forgot)) = return $ mkClass objectType

1288mkExp (SForeign _ fType meth args) = mkForeignInvoke fType meth args

1289−mkExp (SOp (LPlus ITNative) args) = mkExp (SOp (LPlus IT32) args)

1289+mkExp (SOp (LPlus (ATInt ITNative)) args) = mkExp (SOp (LPlus (ATInt (ITFixed IT32))) args)

1290−mkExp (SOp (LMinus ITNative) args) = mkExp (SOp (LMinus IT32) args)

1290+mkExp (SOp (LMinus (ATInt ITNative)) args) = mkExp (SOp (LMinus (ATInt (ITFixed IT32))) args)

1291−mkExp (SOp (LTimes ITNative) args) = mkExp (SOp (LTimes IT32) args)

1291+mkExp (SOp (LTimes (ATInt ITNative)) args) = mkExp (SOp (LTimes (ATInt (ITFixed IT32))) args)

1292−mkExp (SOp (LSDiv ITNative) args) = mkExp (SOp (LSDiv IT32) args)

1292+mkExp (SOp (LSDiv (ATInt ITNative)) args) = mkExp (SOp (LSDiv (ATInt (ITFixed IT32))) args)

1293−mkExp (SOp (LSRem ITNative) args) = mkExp (SOp (LSRem IT32) args)

1293+mkExp (SOp (LSRem (ATInt ITNative)) args) = mkExp (SOp (LSRem (ATInt (ITFixed IT32))) args)

1294−mkExp (SOp (LAnd ITNative) args) = mkExp (SOp (LAnd IT32) args)

1294+mkExp (SOp (LAnd ITNative) args) = mkExp (SOp (LAnd (ITFixed IT32)) args)

1295−mkExp (SOp (LOr ITNative) args) = mkExp (SOp (LOr IT32) args)

1295+mkExp (SOp (LOr ITNative) args) = mkExp (SOp (LOr (ITFixed IT32)) args)

1296−mkExp (SOp (LXOr ITNative) args) = mkExp (SOp (LXOr IT32) args)

1296+mkExp (SOp (LXOr ITNative) args) = mkExp (SOp (LXOr (ITFixed IT32)) args)

1297−mkExp (SOp (LCompl ITNative) args) = mkExp (SOp (LCompl IT32) args)

1297+mkExp (SOp (LCompl ITNative) args) = mkExp (SOp (LCompl (ITFixed IT32)) args)

1298−mkExp (SOp (LSHL ITNative) args) = mkExp (SOp (LSHL IT32) args)

1298+mkExp (SOp (LSHL ITNative) args) = mkExp (SOp (LSHL (ITFixed IT32)) args)

1299−mkExp (SOp (LASHR ITNative) args) = mkExp (SOp (LASHR IT32) args)

1299+mkExp (SOp (LASHR ITNative) args) = mkExp (SOp (LASHR (ITFixed IT32)) args)

1300−mkExp (SOp (LEq ITNative) args) = mkExp (SOp (LEq IT32) args)

1300+mkExp (SOp (LEq (ATInt ITNative)) args) = mkExp (SOp (LEq (ATInt (ITFixed IT32))) args)

1301−mkExp (SOp (LLt ITNative) args) = mkExp (SOp (LLt IT32) args)

1301+mkExp (SOp (LLt (ATInt ITNative)) args) = mkExp (SOp (LLt (ATInt (ITFixed IT32))) args)

1302−mkExp (SOp (LLe ITNative) args) = mkExp (SOp (LLe IT32) args)

1302+mkExp (SOp (LLe (ATInt ITNative)) args) = mkExp (SOp (LLe (ATInt (ITFixed IT32))) args)

1303−mkExp (SOp (LGt ITNative) args) = mkExp (SOp (LGt IT32) args)

1303+mkExp (SOp (LGt (ATInt ITNative)) args) = mkExp (SOp (LGt (ATInt (ITFixed IT32))) args)

1304−mkExp (SOp (LGe ITNative) args) = mkExp (SOp (LGe IT32) args)

1304+mkExp (SOp (LGe (ATInt ITNative)) args) = mkExp (SOp (LGe (ATInt (ITFixed IT32))) args)

1305−mkExp (SOp LFPlus args) = mkBinOpExp doubleType Add args

1305+mkExp (SOp (LPlus ATFloat) args) = mkBinOpExp doubleType Add args

1306−mkExp (SOp LFMinus args) = mkBinOpExp doubleType Sub args

1306+mkExp (SOp (LMinus ATFloat) args) = mkBinOpExp doubleType Sub args

1307−mkExp (SOp LFTimes args) = mkBinOpExp doubleType Mult args

1307+mkExp (SOp (LTimes ATFloat) args) = mkBinOpExp doubleType Mult args

1308−mkExp (SOp LFDiv args) = mkBinOpExp doubleType Div args

1308+mkExp (SOp (LSDiv ATFloat) args) = mkBinOpExp doubleType Div args

1309−mkExp (SOp LFEq args) =

1309+mkExp (SOp (LEq ATFloat) args) =

1310 mkMethodOpChain1 (mkBoolToNumber doubleType) doubleType "equals" args

1311−mkExp (SOp LFLt args) = mkLogicalBinOpExp integerType LThan args

1311+mkExp (SOp (LLt ATFloat) args) = mkLogicalBinOpExp integerType LThan args

1312−mkExp (SOp LFLe args) = mkLogicalBinOpExp integerType LThanE args

1312+mkExp (SOp (LLe ATFloat) args) = mkLogicalBinOpExp integerType LThanE args

1313−mkExp (SOp LFGt args) = mkLogicalBinOpExp integerType GThan args

1313+mkExp (SOp (LGt ATFloat) args) = mkLogicalBinOpExp integerType GThan args

1314−mkExp (SOp LFGe args) = mkLogicalBinOpExp integerType GThanE args

1314+mkExp (SOp (LGe ATFloat) args) = mkLogicalBinOpExp integerType GThanE args

1315−mkExp (SOp (LPlus ITBig) args) = mkMethodOpChain1 id bigIntegerType "add" args

1315+mkExp (SOp (LPlus (ATInt ITBig)) args) = mkMethodOpChain1 id bigIntegerType "add" args

1316−mkExp (SOp (LMinus ITBig) args) = mkMethodOpChain1 id bigIntegerType "subtract" args

1316+mkExp (SOp (LMinus (ATInt ITBig)) args) = mkMethodOpChain1 id bigIntegerType "subtract" args

1317−mkExp (SOp (LTimes ITBig) args) = mkMethodOpChain1 id bigIntegerType "multiply" args

1317+mkExp (SOp (LTimes (ATInt ITBig)) args) = mkMethodOpChain1 id bigIntegerType "multiply" args

1318−mkExp (SOp (LSDiv ITBig) args) = mkMethodOpChain1 id bigIntegerType "divide" args

1318+mkExp (SOp (LSDiv (ATInt ITBig)) args) = mkMethodOpChain1 id bigIntegerType "divide" args

1319−mkExp (SOp (LSRem ITBig) args) = mkMethodOpChain1 id bigIntegerType "mod" args

1319+mkExp (SOp (LSRem (ATInt ITBig)) args) = mkMethodOpChain1 id bigIntegerType "mod" args

1320−mkExp (SOp (LEq ITBig) args) =

1320+mkExp (SOp (LEq (ATInt ITBig)) args) =

1321 mkMethodOpChain1 (mkBoolToNumber bigIntegerType) bigIntegerType "equals" args

1322−mkExp (SOp (LLt ITBig) args) =

1322+mkExp (SOp (LLt (ATInt ITBig)) args) =

1323 mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1324 . mkPartialOrder SLt

1325 )

1326 bigIntegerType

1327 "compareTo"

1328 args

1329−mkExp (SOp (LLe ITBig) args) =

1329+mkExp (SOp (LLe (ATInt ITBig)) args) =

1330 mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1331 . mkPartialOrder SLe

1332 )

1333 bigIntegerType

1334 "compareTo"

1335 args

1336−mkExp (SOp (LGt ITBig) args) =

1336+mkExp (SOp (LGt (ATInt ITBig)) args) =

1337 mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1338 . mkPartialOrder SGt

1339 )

1340 bigIntegerType

1341 "compareTo"

1342 args

1343−mkExp (SOp (LGe ITBig) args) =

1343+mkExp (SOp (LGe (ATInt ITBig)) args) =

1344 mkMethodOpChain1 ( mkBoolToNumber bigIntegerType

1345 . mkPartialOrder SGe

1346 )

@@ -1397,16 +1397,16 @@ mkExp (SOp LPrintNum [arg]) =

1397mkExp (SOp LPrintStr [arg]) =

1398 mkSystemOutPrint <$> (mkVarAccess (Just stringType) arg)

1399mkExp (SOp LReadStr [arg]) = mkExp (SForeign LANG_C FString "idris_readStr" [(FPtr, arg)])

1400−mkExp (SOp (LLt ty) args) = mkLogicalBinOpExp (intTyToClass ty) LThan args

1400+mkExp (SOp (LLt (ATInt ty)) args) = mkLogicalBinOpExp (intTyToClass ty) LThan args

1401−mkExp (SOp (LLe ty) args) = mkLogicalBinOpExp (intTyToClass ty) LThanE args

1401+mkExp (SOp (LLe (ATInt ty)) args) = mkLogicalBinOpExp (intTyToClass ty) LThanE args

1402−mkExp (SOp (LEq ty) args) =

1402+mkExp (SOp (LEq (ATInt ty)) args) =

1403 mkMethodOpChain1 (mkBoolToNumber (intTyToClass ty)) (intTyToClass ty) "equals" args

1404−mkExp (SOp (LGt ty) args) = mkLogicalBinOpExp (intTyToClass ty) GThan args

1404+mkExp (SOp (LGt (ATInt ty)) args) = mkLogicalBinOpExp (intTyToClass ty) GThan args

1405−mkExp (SOp (LGe ty) args) = mkLogicalBinOpExp (intTyToClass ty) GThanE args

1405+mkExp (SOp (LGe (ATInt ty)) args) = mkLogicalBinOpExp (intTyToClass ty) GThanE args

1406−mkExp (SOp (LPlus ty) args) = mkBinOpExp (intTyToClass ty) Add args

1406+mkExp (SOp (LPlus (ATInt ty)) args) = mkBinOpExp (intTyToClass ty) Add args

1407−mkExp (SOp (LMinus ty) args) = mkBinOpExp (intTyToClass ty) Sub args

1407+mkExp (SOp (LMinus (ATInt ty)) args) = mkBinOpExp (intTyToClass ty) Sub args

1408−mkExp (SOp (LTimes ty) args) = mkBinOpExp (intTyToClass ty) Mult args

1408+mkExp (SOp (LTimes (ATInt ty)) args) = mkBinOpExp (intTyToClass ty) Mult args

1409−mkExp (SOp (LUDiv IT64) (arg:args)) = do

1409+mkExp (SOp (LUDiv (ITFixed IT64)) (arg:args)) = do

1410 (arg:args) <- mapM (mkVarAccess (Just longType)) (arg:args)

1411 return $ foldl (\ exp arg ->

1412 MethodInv $ PrimaryMethodCall

@@ -1436,8 +1436,8 @@ mkExp (SOp (LUDiv ty) args) =

1436 (intTyToClass ty)

1437 Div

1438 args

1439−mkExp (SOp (LSDiv ty) args) = mkBinOpExp (intTyToClass ty) Div args

1439+mkExp (SOp (LSDiv (ATInt ty)) args) = mkBinOpExp (intTyToClass ty) Div args

1440−mkExp (SOp (LURem IT64) (arg:args)) = do

1440+mkExp (SOp (LURem (ITFixed IT64)) (arg:args)) = do

1441 (arg:args) <- mapM (mkVarAccess (Just longType)) (arg:args)

1442 return $ foldl (\ exp arg ->

1443 MethodInv $ PrimaryMethodCall

@@ -1467,7 +1467,7 @@ mkExp (SOp (LURem ty) args) =

1467 (intTyToClass ty)

1468 Rem

1469 args

1470−mkExp (SOp (LSRem ty) args) = mkBinOpExp (intTyToClass ty) Rem args

1470+mkExp (SOp (LSRem (ATInt ty)) args) = mkBinOpExp (intTyToClass ty) Rem args

1471mkExp (SOp (LSHL ty) args) = mkBinOpExp (intTyToClass ty) LShift args

1472mkExp (SOp (LLSHR ty) args) = mkBinOpExp (intTyToClass ty) RRShift args

1473mkExp (SOp (LASHR ty) args) = mkBinOpExp (intTyToClass ty) RShift args

src/IRTS/CodegenJavaScript.hs+29−29

@@ -143,11 +143,11 @@ translateConstant (BI i) = "__IDRRT__.bigInt('" ++ show i ++ "')"

143translateConstant (Fl f) = show f

144translateConstant (Ch c) = show c

145translateConstant (Str s) = show s

146−translateConstant IType = "__IDRRT__.Int"

146+translateConstant (AType (ATInt ITNative)) = "__IDRRT__.Int"

147translateConstant ChType = "__IDRRT__.Char"

148translateConstant StrType = "__IDRRT__.String"

149−translateConstant BIType = "__IDRRT__.Integer"

149+translateConstant (AType (ATInt ITBig)) = "__IDRRT__.Integer"

150−translateConstant FlType = "__IDRRT__.Float"

150+translateConstant (AType ATFloat) = "__IDRRT__.Float"

151translateConstant PtrType = "__IDRRT__.Ptr"

152translateConstant Forgot = "__IDRRT__.Forgot"

153translateConstant c =

@@ -245,44 +245,44 @@ translateExpression (SOp op vars)

245 | (LCompl _) <- op

246 , (arg:_) <- vars = '~' : translateVariableName arg

247

248− | (LPlus ITBig) <- op

248+ | (LPlus (ATInt ITBig)) <- op

249 , (lhs:rhs:_) <- vars = translateBinaryOp ".add(" lhs rhs ++ ")"

250− | (LMinus ITBig) <- op

250+ | (LMinus (ATInt ITBig)) <- op

251 , (lhs:rhs:_) <- vars = translateBinaryOp ".minus(" lhs rhs ++ ")"

252− | (LTimes ITBig) <- op

252+ | (LTimes (ATInt ITBig)) <- op

253 , (lhs:rhs:_) <- vars = translateBinaryOp ".times(" lhs rhs ++ ")"

254− | (LSDiv ITBig) <- op

254+ | (LSDiv (ATInt ITBig)) <- op

255 , (lhs:rhs:_) <- vars = translateBinaryOp ".divide(" lhs rhs ++ ")"

256− | (LSRem ITBig) <- op

256+ | (LSRem (ATInt ITBig)) <- op

257 , (lhs:rhs:_) <- vars = translateBinaryOp ".mod(" lhs rhs ++ ")"

258− | (LEq ITBig) <- op

258+ | (LEq (ATInt ITBig)) <- op

259 , (lhs:rhs:_) <- vars = translateBinaryOp ".equals(" lhs rhs ++ ")"

260− | (LLt ITBig) <- op

260+ | (LLt (ATInt ITBig)) <- op

261 , (lhs:rhs:_) <- vars = translateBinaryOp ".lesser(" lhs rhs ++ ")"

262− | (LLe ITBig) <- op

262+ | (LLe (ATInt ITBig)) <- op

263 , (lhs:rhs:_) <- vars = translateBinaryOp ".lesserOrEquals(" lhs rhs ++ ")"

264− | (LGt ITBig) <- op

264+ | (LGt (ATInt ITBig)) <- op

265 , (lhs:rhs:_) <- vars = translateBinaryOp ".greater(" lhs rhs ++ ")"

266− | (LGe ITBig) <- op

266+ | (LGe (ATInt ITBig)) <- op

267 , (lhs:rhs:_) <- vars = translateBinaryOp ".greaterOrEquals(" lhs rhs ++ ")"

268

269− | LFPlus <- op

269+ | (LPlus ATFloat) <- op

270 , (lhs:rhs:_) <- vars = translateBinaryOp "+" lhs rhs

271− | LFMinus <- op

271+ | (LMinus ATFloat) <- op

272 , (lhs:rhs:_) <- vars = translateBinaryOp "-" lhs rhs

273− | LFTimes <- op

273+ | (LTimes ATFloat) <- op

274 , (lhs:rhs:_) <- vars = translateBinaryOp "*" lhs rhs

275− | LFDiv <- op

275+ | (LSDiv ATFloat) <- op

276 , (lhs:rhs:_) <- vars = translateBinaryOp "/" lhs rhs

277− | LFEq <- op

277+ | (LEq ATFloat) <- op

278 , (lhs:rhs:_) <- vars = translateBinaryOp "==" lhs rhs

279− | LFLt <- op

279+ | (LLt ATFloat) <- op

280 , (lhs:rhs:_) <- vars = translateBinaryOp "<" lhs rhs

281− | LFLe <- op

281+ | (LLe ATFloat) <- op

282 , (lhs:rhs:_) <- vars = translateBinaryOp "<=" lhs rhs

283− | LFGt <- op

283+ | (LGt ATFloat) <- op

284 , (lhs:rhs:_) <- vars = translateBinaryOp ">" lhs rhs

285− | LFGe <- op

285+ | (LGe ATFloat) <- op

286 , (lhs:rhs:_) <- vars = translateBinaryOp ">=" lhs rhs

287

288 | LStrConcat <- op

@@ -470,13 +470,13 @@ translateCase _ (SDefaultCase e) =

470 createIfBlock "true" (translateExpression e)

471

472translateCase var (SConstCase ty e)

473− | ChType <- ty = matchHelper "Char"

473+ | ChType <- ty = matchHelper "Char"

474− | StrType <- ty = matchHelper "String"

474+ | StrType <- ty = matchHelper "String"

475− | IType <- ty = matchHelper "Int"

476− | BIType <- ty = matchHelper "Integer"

477− | FlType <- ty = matchHelper "Float"

478− | PtrType <- ty = matchHelper "Ptr"

475+ | PtrType <- ty = matchHelper "Ptr"

479− | Forgot <- ty = matchHelper "Forgot"

476+ | Forgot <- ty = matchHelper "Forgot"

477+ | (AType ATFloat) <- ty = matchHelper "Float"

478+ | (AType (ATInt ITBig)) <- ty = matchHelper "Integer"

479+ | (AType (ATInt ITNative)) <- ty = matchHelper "Int"

480 where

481 matchHelper tyName = translateTypeMatch var tyName e

482

src/IRTS/CodegenLLVM.hs+200−124

@@ -5,6 +5,7 @@ import IRTS.CodegenCommon

5import IRTS.Lang

6import IRTS.Simplified

7import qualified Core.TT as TT

8+import Core.TT (ArithTy(..), IntTy(..), NativeTy(..), nativeTyWidth)

9import Util.System

10import Util.System

10import Paths_idris

11import Paths_idris

@@ -13,6 +14,9 @@ import LLVM.General.Context

13import LLVM.General.Diagnostic

14import LLVM.General.Diagnostic

14import LLVM.General.AST

15import LLVM.General.AST

15import LLVM.General.AST.AddrSpace

16import LLVM.General.AST.AddrSpace

17+import LLVM.General.Target

18+import LLVM.General.AST.DataLayout

19+import LLVM.General.PassManager

16import qualified LLVM.General.Module as M

20import qualified LLVM.General.Module as M

17import qualified LLVM.General.AST.IntegerPredicate as IPred

21import qualified LLVM.General.AST.IntegerPredicate as IPred

18import qualified LLVM.General.AST.Linkage as L

22import qualified LLVM.General.AST.Linkage as L

@@ -22,16 +26,22 @@ import qualified LLVM.General.AST.Attribute as A

22import qualified LLVM.General.AST.Global as G

26import qualified LLVM.General.AST.Global as G

23import qualified LLVM.General.AST.Constant as C

27import qualified LLVM.General.AST.Constant as C

24import qualified LLVM.General.AST.Float as F

28import qualified LLVM.General.AST.Float as F

29+import qualified LLVM.General.Relocation as R

30+import qualified LLVM.General.CodeModel as CM

31+import qualified LLVM.General.CodeGenOpt as CGO

26import Data.List

33import Data.List

27import Data.Maybe

34import Data.Maybe

28import Data.Word

35import Data.Word

29import Data.Set (Set)

36import Data.Set (Set)

30import qualified Data.Set as S

37import qualified Data.Set as S

38+import qualified Data.Map as M

39+import qualified Data.Vector.Unboxed as V

31import Control.Applicative

40import Control.Applicative

32import Control.Monad.RWS

41import Control.Monad.RWS

33import Control.Monad.Writer

42import Control.Monad.Writer

34import Control.Monad.State

43import Control.Monad.State

44+import Control.Monad.Error

36import qualified System.Info as SI (arch, os)

46import qualified System.Info as SI (arch, os)

37import System.IO

47import System.IO

@@ -41,32 +51,42 @@ import System.Process (rawSystem)

41import System.Exit (ExitCode(..))

51import System.Exit (ExitCode(..))

42import Debug.Trace

52import Debug.Trace

44−data Target = Target { arch :: String, os :: String }

54+data Target = Target { triple :: String, dataLayout :: DataLayout }

46codegenLLVM :: [(TT.Name, SDecl)] ->

56codegenLLVM :: [(TT.Name, SDecl)] ->

57+ String -> -- target triple

58+ String -> -- target CPU

59+ Int -> -- Optimization degree

47 FilePath -> -- output file name

60 FilePath -> -- output file name

48 OutputType ->

61 OutputType ->

49 IO ()

62 IO ()

50−codegenLLVM defs file outty = withContext $ \context -> do

63+codegenLLVM defs triple cpu optimize file outty = withContext $ \context -> do

51− let target = Target { arch = SI.arch, os = SI.os }

64+ initializeAllTargets

65+ (target, _) <- failInIO $ lookupTarget Nothing triple

66+ withTargetOptions $ \options ->

67+ withTargetMachine target triple cpu S.empty options R.Default CM.Default CGO.Default $ \tm ->

68+ do layout <- getTargetMachineDataLayout tm

52− let ast = codegen target (map snd defs)

69+ let ast = codegen (Target triple layout) (map snd defs)

53− result <- M.withModuleFromAST context ast (outputModule file outty)

70+ result <- runErrorT . M.withModuleFromAST context ast $ \m ->

71+ do let opts = defaultCuratedPassSetSpec

72+ { optLevel = Just optimize

73+ , simplifyLibCalls = Just True

74+ , useInlinerWithThreshold = Just 225

75+ }

76+ when (optimize /= 0) $ withPassManager opts $ void . flip runPassManager m

77+ outputModule tm file outty m

54− case result of

78+ case result of

55− Right _ -> return ()

79+ Right _ -> return ()

56− Left msg -> ierror msg

80+ Left msg -> ierror msg

57−

81+

58−itWidth :: IntTy -> Word32

82+failInIO :: ErrorT String IO a -> IO a

59−itWidth ITNative = 32

83+failInIO = either fail return <=< runErrorT

60−itWidth x = fromIntegral $ intTyWidth x

84+

61−

62−outputModule :: FilePath -> OutputType -> M.Module -> IO ()

85+outputModule :: TargetMachine -> FilePath -> OutputType -> M.Module -> IO ()

63−outputModule file Raw m = M.writeBitcodeToFile file m

86+outputModule _ file Raw m = failInIO $ M.writeBitcodeToFile file m

64−outputModule file Object m = withTmpFile $ \bc -> do

87+outputModule tm file Object m = failInIO $ M.writeObjectToFile tm file m

65− outputModule bc Raw m

66− exit <- rawSystem "llc" ["-filetype=obj", "--disable-fp-elim", "-o", file, bc]

67− when (exit /= ExitSuccess) $ ierror "FAILURE: Object generation"

68−outputModule file Executable m = withTmpFile $ \obj -> do

88+outputModule tm file Executable m = withTmpFile $ \obj -> do

69− outputModule obj Object m

89+ outputModule tm obj Object m

70 cc <- getCC

90 cc <- getCC

71 defs <- (</> "llvm" </> "libidris_rts.a") <$> getDataDir

91 defs <- (</> "llvm" </> "libidris_rts.a") <$> getDataDir

72 exit <- rawSystem cc [obj, defs, "-lm", "-lgmp", "-lgc", "-o", file]

92 exit <- rawSystem cc [obj, defs, "-lm", "-lgmp", "-lgc", "-o", file]

@@ -127,10 +147,10 @@ initDefs tgt =

127 }

147 }

128 , rtsFun "intStr" ptrI8 [IntegerType 64]

148 , rtsFun "intStr" ptrI8 [IntegerType 64]

129 [ BasicBlock (UnName 0)

149 [ BasicBlock (UnName 0)

130− [ UnName 1 := simpleCall "GC_malloc_atomic" [ConstantOperand (C.Int (fromInteger $ tgtWordSize tgt) 21)]

150+ [ UnName 1 := simpleCall "GC_malloc_atomic" [ConstantOperand (C.Int (tgtWordSize tgt) 21)]

131 , UnName 2 := simpleCall "snprintf"

151 , UnName 2 := simpleCall "snprintf"

132 [ LocalReference (UnName 1)

152 [ LocalReference (UnName 1)

133− , ConstantOperand (C.Int (fromInteger $ tgtWordSize tgt) 21)

153+ , ConstantOperand (C.Int (tgtWordSize tgt) 21)

134 , ConstantOperand $ C.GetElementPtr True (C.GlobalReference . Name $ "__idris_intFmtStr") [C.Int 32 0, C.Int 32 0]

154 , ConstantOperand $ C.GetElementPtr True (C.GlobalReference . Name $ "__idris_intFmtStr") [C.Int 32 0, C.Int 32 0]

135 , LocalReference (UnName 0)

155 , LocalReference (UnName 0)

136 ]

156 ]

@@ -138,10 +158,12 @@ initDefs tgt =

138 (Do $ Ret (Just (LocalReference (UnName 1))) [])

158 (Do $ Ret (Just (LocalReference (UnName 1))) [])

139 ]

159 ]

140 , exfun "llvm.trap" VoidType [] False

160 , exfun "llvm.trap" VoidType [] False

161+ -- , exfun "llvm.llvm.memcpy.p0i8.p0i8.i32" VoidType [ptrI8, ptrI8, IntegerType 32, IntegerType 32, IntegerType 1] False

162+ -- , exfun "llvm.llvm.memcpy.p0i8.p0i8.i64" VoidType [ptrI8, ptrI8, IntegerType 64, IntegerType 32, IntegerType 1] False

163+ , exfun "memcpy" ptrI8 [ptrI8, ptrI8, intPtr] False

141 , exfun "snprintf" (IntegerType 32) [ptrI8, intPtr, ptrI8] True

164 , exfun "snprintf" (IntegerType 32) [ptrI8, intPtr, ptrI8] True

142 , exfun "strcmp" (IntegerType 32) [ptrI8, ptrI8] False

165 , exfun "strcmp" (IntegerType 32) [ptrI8, ptrI8] False

143 , exfun "strlen" intPtr [ptrI8] False

166 , exfun "strlen" intPtr [ptrI8] False

144− , exfun "memcpy" ptrI8 [ptrI8, ptrI8, intPtr] False

145 , exfun "GC_init" VoidType [] False

167 , exfun "GC_init" VoidType [] False

146 , exfun "GC_malloc" ptrI8 [intPtr] False

168 , exfun "GC_malloc" ptrI8 [intPtr] False

147 , exfun "GC_malloc_atomic" ptrI8 [intPtr] False

169 , exfun "GC_malloc_atomic" ptrI8 [intPtr] False

@@ -169,7 +191,7 @@ initDefs tgt =

169 , GlobalDefinition mainDef

191 , GlobalDefinition mainDef

170 ] ++ map mpzBinFun ["add", "sub", "mul", "fdiv_q", "fdiv_r", "and", "ior", "xor"]

192 ] ++ map mpzBinFun ["add", "sub", "mul", "fdiv_q", "fdiv_r", "and", "ior", "xor"]

171 where

193 where

172− intPtr = IntegerType (fromInteger $ tgtWordSize tgt)

194+ intPtr = IntegerType (tgtWordSize tgt)

173 ptrI8 = PointerType (IntegerType 8) (AddrSpace 0)

195 ptrI8 = PointerType (IntegerType 8) (AddrSpace 0)

174 pmpz = PointerType mpzTy (AddrSpace 0)

196 pmpz = PointerType mpzTy (AddrSpace 0)

175

197

@@ -195,18 +217,24 @@ initDefs tgt =

195 exVar :: String -> Type -> Definition

217 exVar :: String -> Type -> Definition

196 exVar name ty = GlobalDefinition $ globalVariableDefaults { G.name = Name name, G.type' = ty }

218 exVar name ty = GlobalDefinition $ globalVariableDefaults { G.name = Name name, G.type' = ty }

197

219

198− stdinName :: Target -> String

220+isApple :: Target -> Bool

199− stdinName (Target { os = "darwin" }) = "__stdinp"

221+isApple (Target { triple = t }) = isJust . stripPrefix "-apple" $ dropWhile (/= '-') t

222+

223+stdinName, stdoutName, stderrName :: Target -> String

224+stdinName t | isApple t = "__stdinp"

200− stdinName _ = "stdin"

225+stdinName _ = "stdin"

201− stdoutName :: Target -> String

226+stdoutName t | isApple t = "__stdoutp"

202− stdoutName (Target { os = "darwin" }) = "__stdoutp"

203− stdoutName _ = "stdout"

227+stdoutName _ = "stdout"

204− stderrName :: Target -> String

228+stderrName t | isApple t = "__stderrp"

205− stderrName (Target { os = "darwin" }) = "__stderrp"

206− stderrName _ = "stderr"

229+stderrName _ = "stderr"

230+

231+getStdIn, getStdOut, getStdErr :: Codegen Operand

232+getStdIn = ConstantOperand . C.GlobalReference . Name . stdinName <$> asks target

233+getStdOut = ConstantOperand . C.GlobalReference . Name . stdoutName <$> asks target

234+getStdErr = ConstantOperand . C.GlobalReference . Name . stderrName <$> asks target

207

235

208codegen :: Target -> [SDecl] -> Module

236codegen :: Target -> [SDecl] -> Module

209−codegen tgt defs = Module "idris" Nothing Nothing (initDefs tgt ++ globals ++ gendefs)

237+codegen tgt defs = Module "idris" (Just . dataLayout $ tgt) (Just . triple $ tgt) (initDefs tgt ++ globals ++ gendefs)

210 where

238 where

211 (gendefs, _, globals) = runRWS (mapM cgDef defs) tgt 0

239 (gendefs, _, globals) = runRWS (mapM cgDef defs) tgt 0

212

240

@@ -365,13 +393,13 @@ alloc ty = do

365sizeOf :: Type -> Codegen Operand

393sizeOf :: Type -> Codegen Operand

366sizeOf ty = ConstantOperand . C.PtrToInt

394sizeOf ty = ConstantOperand . C.PtrToInt

367 (C.GetElementPtr True (C.Null (PointerType ty (AddrSpace 0))) [C.Int 32 1])

395 (C.GetElementPtr True (C.Null (PointerType ty (AddrSpace 0))) [C.Int 32 1])

368− . IntegerType . fromIntegral <$> getWordSize

396+ . IntegerType <$> getWordSize

369

397

370−tgtWordSize :: Target -> Integer

398+tgtWordSize :: Target -> Word32

371−tgtWordSize (Target { arch = "i386" }) = 32

399+tgtWordSize (Target { dataLayout = DataLayout { pointerLayouts = l } }) =

372−tgtWordSize (Target { arch = "x86_64" }) = 64

400+ fst . fromJust $ M.lookup (AddrSpace 0) l

373

401

374−getWordSize :: Codegen Integer

402+getWordSize :: Codegen Word32

375getWordSize = tgtWordSize <$> asks target

403getWordSize = tgtWordSize <$> asks target

376

404

377cgExpr :: SExp -> Codegen (Maybe Operand)

405cgExpr :: SExp -> Codegen (Maybe Operand)

@@ -556,7 +584,7 @@ cgChainCase :: Operand -> Maybe SExp -> [SAlt] -> Codegen (Maybe Operand)

556cgChainCase caseValPtr defExp alts = do

584cgChainCase caseValPtr defExp alts = do

557 let (caseTy, comparator) =

585 let (caseTy, comparator) =

558 case head alts of

586 case head alts of

559− SConstCase (TT.BI _) _ -> (FInt ITBig, "__gmpz_cmp")

587+ SConstCase (TT.BI _) _ -> (FArith (ATInt ITBig), "__gmpz_cmp")

560 SConstCase (TT.Str _) _ -> (FString, "strcmp")

588 SConstCase (TT.Str _) _ -> (FString, "strcmp")

561 caseVal <- unbox caseTy caseValPtr

589 caseVal <- unbox caseTy caseValPtr

562 defBlockName <- getName "default"

590 defBlockName <- getName "default"

@@ -682,6 +710,11 @@ cgConst' (TT.B8 i) = C.Int 8 (fromIntegral i)

682cgConst' (TT.B16 i) = C.Int 16 (fromIntegral i)

710cgConst' (TT.B16 i) = C.Int 16 (fromIntegral i)

683cgConst' (TT.B32 i) = C.Int 32 (fromIntegral i)

711cgConst' (TT.B32 i) = C.Int 32 (fromIntegral i)

684cgConst' (TT.B64 i) = C.Int 64 (fromIntegral i)

712cgConst' (TT.B64 i) = C.Int 64 (fromIntegral i)

713+cgConst' (TT.B8V v) = C.Vector (map ((C.Int 8) . fromIntegral) . V.toList $ v)

714+cgConst' (TT.B16V v) = C.Vector (map ((C.Int 16) . fromIntegral) . V.toList $ v)

715+cgConst' (TT.B32V v) = C.Vector (map ((C.Int 32) . fromIntegral) . V.toList $ v)

716+cgConst' (TT.B64V v) = C.Vector (map ((C.Int 64) . fromIntegral) . V.toList $ v)

717+

685cgConst' (TT.BI i) = C.Array (IntegerType 8) (map (C.Int 8 . fromIntegral . fromEnum) (show i) ++ [C.Int 8 0])

718cgConst' (TT.BI i) = C.Array (IntegerType 8) (map (C.Int 8 . fromIntegral . fromEnum) (show i) ++ [C.Int 8 0])

686cgConst' (TT.Fl f) = C.Float (F.Double f)

719cgConst' (TT.Fl f) = C.Float (F.Double f)

687cgConst' (TT.Ch c) = C.Int 32 . fromIntegral . fromEnum $ c

720cgConst' (TT.Ch c) = C.Int 32 . fromIntegral . fromEnum $ c

@@ -689,12 +722,16 @@ cgConst' (TT.Str s) = C.Array (IntegerType 8) (map (C.Int 8 . fromIntegral . fro

689cgConst' x = ierror $ "Unsupported constant: " ++ show x

722cgConst' x = ierror $ "Unsupported constant: " ++ show x

690

723

691cgConst :: TT.Const -> Codegen Operand

724cgConst :: TT.Const -> Codegen Operand

692−cgConst c@(TT.I _) = box (FInt ITNative) (ConstantOperand $ cgConst' c)

725+cgConst c@(TT.I _) = box (FArith (ATInt ITNative)) (ConstantOperand $ cgConst' c)

693−cgConst c@(TT.B8 _) = box (FInt IT8) (ConstantOperand $ cgConst' c)

726+cgConst c@(TT.B8 _) = box (FArith (ATInt (ITFixed IT8))) (ConstantOperand $ cgConst' c)

694−cgConst c@(TT.B16 _) = box (FInt IT16) (ConstantOperand $ cgConst' c)

727+cgConst c@(TT.B16 _) = box (FArith (ATInt (ITFixed IT16))) (ConstantOperand $ cgConst' c)

695−cgConst c@(TT.B32 _) = box (FInt IT32) (ConstantOperand $ cgConst' c)

728+cgConst c@(TT.B32 _) = box (FArith (ATInt (ITFixed IT32))) (ConstantOperand $ cgConst' c)

729+cgConst c@(TT.B64 _) = box (FArith (ATInt (ITFixed IT64))) (ConstantOperand $ cgConst' c)

730+cgConst c@(TT.B8V v) = box (FArith (ATInt (ITVec IT8 (V.length v)))) (ConstantOperand $ cgConst' c)

731+cgConst c@(TT.B16V v) = box (FArith (ATInt (ITVec IT16 (V.length v)))) (ConstantOperand $ cgConst' c)

732+cgConst c@(TT.B32V v) = box (FArith (ATInt (ITVec IT32 (V.length v)))) (ConstantOperand $ cgConst' c)

696−cgConst c@(TT.B64 _) = box (FInt IT64) (ConstantOperand $ cgConst' c)

733+cgConst c@(TT.B64V v) = box (FArith (ATInt (ITVec IT64 (V.length v)))) (ConstantOperand $ cgConst' c)

697−cgConst c@(TT.Fl _) = box FDouble (ConstantOperand $ cgConst' c)

734+cgConst c@(TT.Fl _) = box (FArith ATFloat) (ConstantOperand $ cgConst' c)

698cgConst c@(TT.Ch _) = box FChar (ConstantOperand $ cgConst' c)

735cgConst c@(TT.Ch _) = box FChar (ConstantOperand $ cgConst' c)

699cgConst c@(TT.Str s) = do

736cgConst c@(TT.Str s) = do

700 str <- addGlobal' (ArrayType (1 + fromIntegral (length s)) (IntegerType 8)) (cgConst' c)

737 str <- addGlobal' (ArrayType (1 + fromIntegral (length s)) (IntegerType 8)) (cgConst' c)

@@ -706,7 +743,7 @@ cgConst c@(TT.BI i) = do

706 , ConstantOperand $ C.GetElementPtr True str [ C.Int 32 0, C.Int 32 0]

743 , ConstantOperand $ C.GetElementPtr True str [ C.Int 32 0, C.Int 32 0]

707 , ConstantOperand $ C.Int 32 10

744 , ConstantOperand $ C.Int 32 10

708 ]

745 ]

709− box (FInt ITBig) mpz

746+ box (FArith (ATInt ITBig)) mpz

710cgConst x = return $ ConstantOperand nullValue

747cgConst x = return $ ConstantOperand nullValue

711

748

712numDigits :: Integer -> Integer -> Integer

749numDigits :: Integer -> Integer -> Integer

@@ -752,72 +789,82 @@ ffunDecl name rty argtys =

752 }

789 }

753

790

754ftyToTy :: FType -> Type

791ftyToTy :: FType -> Type

755−ftyToTy (FInt ITNative) = IntegerType 32

792+ftyToTy (FArith (ATInt ITNative)) = IntegerType 32

756−ftyToTy (FInt ITBig) = PointerType mpzTy (AddrSpace 0)

793+ftyToTy (FArith (ATInt ITBig)) = PointerType mpzTy (AddrSpace 0)

757−ftyToTy (FInt ty) = IntegerType (itWidth ty)

794+ftyToTy (FArith (ATInt (ITFixed ty))) = IntegerType (fromIntegral $ nativeTyWidth ty)

795+ftyToTy (FArith (ATInt (ITVec e c)))

796+ = VectorType (fromIntegral c) (IntegerType (fromIntegral $ nativeTyWidth e))

758ftyToTy FChar = IntegerType 32

797ftyToTy FChar = IntegerType 32

759ftyToTy FString = PointerType (IntegerType 8) (AddrSpace 0)

798ftyToTy FString = PointerType (IntegerType 8) (AddrSpace 0)

760ftyToTy FUnit = VoidType

799ftyToTy FUnit = VoidType

761ftyToTy FPtr = PointerType (IntegerType 8) (AddrSpace 0)

800ftyToTy FPtr = PointerType (IntegerType 8) (AddrSpace 0)

762−ftyToTy FDouble = FloatingPointType 64 IEEE

801+ftyToTy (FArith ATFloat) = FloatingPointType 64 IEEE

763ftyToTy FAny = valueType

802ftyToTy FAny = valueType

764

803

804+-- Only use when known not to be ITBig

805+itWidth :: IntTy -> Word32

806+itWidth ITNative = 32

807+itWidth (ITFixed x) = fromIntegral $ nativeTyWidth x

808+

765cgOp :: PrimFn -> [Operand] -> Codegen Operand

809cgOp :: PrimFn -> [Operand] -> Codegen Operand

766cgOp (LTrunc ITBig ity) [x] = do

810cgOp (LTrunc ITBig ity) [x] = do

767− nx <- unbox (FInt ITBig) x

811+ nx <- unbox (FArith (ATInt ITBig)) x

768 val <- inst $ simpleCall "mpz_get_ull" [nx]

812 val <- inst $ simpleCall "mpz_get_ull" [nx]

769 v <- case ity of

813 v <- case ity of

770− IT64 -> return val

814+ (ITFixed IT64) -> return val

771− _ -> inst $ Trunc val (IntegerType $ itWidth ity) []

815+ _ -> inst $ Trunc val (ftyToTy (FArith (ATInt ity))) []

772− box (FInt ity) v

816+ box (FArith (ATInt ity)) v

773cgOp (LZExt from ITBig) [x] = do

817cgOp (LZExt from ITBig) [x] = do

774− nx <- unbox (FInt from) x

818+ nx <- unbox (FArith (ATInt from)) x

775 nx' <- case from of

819 nx' <- case from of

776− IT64 -> return nx

820+ (ITFixed IT64) -> return nx

777 _ -> inst $ ZExt nx (IntegerType 64) []

821 _ -> inst $ ZExt nx (IntegerType 64) []

778 mpz <- alloc mpzTy

822 mpz <- alloc mpzTy

779 inst' $ simpleCall "mpz_init_set_ull" [mpz, nx']

823 inst' $ simpleCall "mpz_init_set_ull" [mpz, nx']

780− box (FInt ITBig) mpz

824+ box (FArith (ATInt ITBig)) mpz

781cgOp (LSExt from ITBig) [x] = do

825cgOp (LSExt from ITBig) [x] = do

782− nx <- unbox (FInt from) x

826+ nx <- unbox (FArith (ATInt from)) x

783 nx' <- case from of

827 nx' <- case from of

784− IT64 -> return nx

828+ (ITFixed IT64) -> return nx

785 _ -> inst $ SExt nx (IntegerType 64) []

829 _ -> inst $ SExt nx (IntegerType 64) []

786 mpz <- alloc mpzTy

830 mpz <- alloc mpzTy

787 inst' $ simpleCall "mpz_init_set_sll" [mpz, nx']

831 inst' $ simpleCall "mpz_init_set_sll" [mpz, nx']

788− box (FInt ITBig) mpz

832+ box (FArith (ATInt ITBig)) mpz

789−

833+

790−cgOp (LLt ITBig) [x,y] = mpzCmp IPred.SLT x y

834+cgOp (LLt (ATInt ITBig)) [x,y] = mpzCmp IPred.SLT x y

791−cgOp (LLe ITBig) [x,y] = mpzCmp IPred.SLE x y

835+cgOp (LLe (ATInt ITBig)) [x,y] = mpzCmp IPred.SLE x y

792−cgOp (LEq ITBig) [x,y] = mpzCmp IPred.EQ x y

836+cgOp (LEq (ATInt ITBig)) [x,y] = mpzCmp IPred.EQ x y

793−cgOp (LGe ITBig) [x,y] = mpzCmp IPred.SGE x y

837+cgOp (LGe (ATInt ITBig)) [x,y] = mpzCmp IPred.SGE x y

794−cgOp (LGt ITBig) [x,y] = mpzCmp IPred.SGT x y

838+cgOp (LGt (ATInt ITBig)) [x,y] = mpzCmp IPred.SGT x y

795−cgOp (LPlus ITBig) [x,y] = mpzBin "add" x y

839+cgOp (LPlus (ATInt ITBig)) [x,y] = mpzBin "add" x y

796−cgOp (LMinus ITBig) [x,y] = mpzBin "sub" x y

840+cgOp (LMinus (ATInt ITBig)) [x,y] = mpzBin "sub" x y

797−cgOp (LTimes ITBig) [x,y] = mpzBin "mul" x y

841+cgOp (LTimes (ATInt ITBig)) [x,y] = mpzBin "mul" x y

798−cgOp (LSDiv ITBig) [x,y] = mpzBin "fdiv_q" x y

842+cgOp (LSDiv (ATInt ITBig)) [x,y] = mpzBin "fdiv_q" x y

799−cgOp (LSRem ITBig) [x,y] = mpzBin "fdiv_r" x y

843+cgOp (LSRem (ATInt ITBig)) [x,y] = mpzBin "fdiv_r" x y

800cgOp (LAnd ITBig) [x,y] = mpzBin "and" x y

844cgOp (LAnd ITBig) [x,y] = mpzBin "and" x y

801cgOp (LOr ITBig) [x,y] = mpzBin "ior" x y

845cgOp (LOr ITBig) [x,y] = mpzBin "ior" x y

802cgOp (LXOr ITBig) [x,y] = mpzBin "xor" x y

846cgOp (LXOr ITBig) [x,y] = mpzBin "xor" x y

803cgOp (LCompl ITBig) [x] = mpzUn "com" x

847cgOp (LCompl ITBig) [x] = mpzUn "com" x

804

848

849+cgOp (LTrunc (ITFixed from) (ITFixed to)) [x]

805−cgOp (LTrunc from to) [x] | itWidth from > itWidth to = iCoerce Trunc from to x

850+ | nativeTyWidth from > nativeTyWidth to = iCoerce Trunc from to x

851+cgOp (LZExt (ITFixed from) (ITFixed to)) [x]

806−cgOp (LZExt from to) [x] | itWidth from < itWidth to = iCoerce ZExt from to x

852+ | nativeTyWidth from < nativeTyWidth to = iCoerce ZExt from to x

853+cgOp (LSExt (ITFixed from) (ITFixed to)) [x]

807−cgOp (LSExt from to) [x] | itWidth from < itWidth to = iCoerce SExt from to x

854+ | nativeTyWidth from < nativeTyWidth to = iCoerce SExt from to x

808−

855+

809−cgOp (LLt ity) [x,y] = iCmp ity IPred.SLT x y

856+cgOp (LLt (ATInt ity)) [x,y] = iCmp ity IPred.SLT x y

810−cgOp (LLe ity) [x,y] = iCmp ity IPred.SLE x y

857+cgOp (LLe (ATInt ity)) [x,y] = iCmp ity IPred.SLE x y

811−cgOp (LEq ity) [x,y] = iCmp ity IPred.EQ x y

858+cgOp (LEq (ATInt ity)) [x,y] = iCmp ity IPred.EQ x y

812−cgOp (LGe ity) [x,y] = iCmp ity IPred.SGE x y

859+cgOp (LGe (ATInt ity)) [x,y] = iCmp ity IPred.SGE x y

813−cgOp (LGt ity) [x,y] = iCmp ity IPred.SGT x y

860+cgOp (LGt (ATInt ity)) [x,y] = iCmp ity IPred.SGT x y

814−cgOp (LPlus ity) [x,y] = ibin ity x y (Add False False)

861+cgOp (LPlus (ATInt ity)) [x,y] = ibin ity x y (Add False False)

815−cgOp (LMinus ity) [x,y] = ibin ity x y (Sub False False)

862+cgOp (LMinus (ATInt ity)) [x,y] = ibin ity x y (Sub False False)

816−cgOp (LTimes ity) [x,y] = ibin ity x y (Mul False False)

863+cgOp (LTimes (ATInt ity)) [x,y] = ibin ity x y (Mul False False)

864+cgOp (LSDiv (ATInt ity)) [x,y] = ibin ity x y (SDiv False)

865+cgOp (LSRem (ATInt ity)) [x,y] = ibin ity x y SRem

817cgOp (LUDiv ity) [x,y] = ibin ity x y (UDiv False)

866cgOp (LUDiv ity) [x,y] = ibin ity x y (UDiv False)

818cgOp (LURem ity) [x,y] = ibin ity x y URem

867cgOp (LURem ity) [x,y] = ibin ity x y URem

819−cgOp (LSDiv ity) [x,y] = ibin ity x y (SDiv False)

820−cgOp (LSRem ity) [x,y] = ibin ity x y SRem

821cgOp (LAnd ity) [x,y] = ibin ity x y And

868cgOp (LAnd ity) [x,y] = ibin ity x y And

822cgOp (LOr ity) [x,y] = ibin ity x y Or

869cgOp (LOr ity) [x,y] = ibin ity x y Or

823cgOp (LXOr ity) [x,y] = ibin ity x y Xor

870cgOp (LXOr ity) [x,y] = ibin ity x y Xor

@@ -826,13 +873,36 @@ cgOp (LSHL ity) [x,y] = ibin ity x y (Shl False False)

826cgOp (LLSHR ity) [x,y] = ibin ity x y (LShr False)

873cgOp (LLSHR ity) [x,y] = ibin ity x y (LShr False)

827cgOp (LASHR ity) [x,y] = ibin ity x y (AShr False)

874cgOp (LASHR ity) [x,y] = ibin ity x y (AShr False)

828

875

876+cgOp LNoOp xs = return $ last xs

877+

878+cgOp (LMkVec ety c) xs | c == length xs = do

879+ nxs <- mapM (unbox (FArith (ATInt (ITFixed ety)))) xs

880+ vec <- foldM (\v (e, i) -> inst $ InsertElement v e (ConstantOperand (C.Int 32 i)) [])

881+ (ConstantOperand $ C.Vector (replicate c (C.Undef (IntegerType . fromIntegral $ nativeTyWidth ety))))

882+ (zip nxs [0..])

883+ box (FArith (ATInt (ITVec ety c))) vec

884+

885+cgOp (LIdxVec ety c) [v,i] = do

886+ nv <- unbox (FArith (ATInt (ITVec ety c))) v

887+ ni <- unbox (FArith (ATInt (ITFixed IT32))) i

888+ elt <- inst $ ExtractElement nv ni []

889+ box (FArith (ATInt (ITFixed ety))) elt

890+

891+cgOp (LUpdateVec ety c) [v,i,e] = do

892+ let fty = FArith (ATInt (ITVec ety c))

893+ nv <- unbox fty v

894+ ni <- unbox (FArith (ATInt (ITFixed IT32))) i

895+ ne <- unbox (FArith (ATInt (ITFixed ety))) e

896+ nv' <- inst $ InsertElement nv ne ni []

897+ box fty nv'

898+

829cgOp LStrEq [x,y] = do

899cgOp LStrEq [x,y] = do

830 x' <- unbox FString x

900 x' <- unbox FString x

831 y' <- unbox FString y

901 y' <- unbox FString y

832 cmp <- inst $ simpleCall "strcmp" [x', y']

902 cmp <- inst $ simpleCall "strcmp" [x', y']

833 flag <- inst $ ICmp IPred.EQ cmp (ConstantOperand (C.Int 32 0)) []

903 flag <- inst $ ICmp IPred.EQ cmp (ConstantOperand (C.Int 32 0)) []

834 val <- inst $ ZExt flag (IntegerType 32) []

904 val <- inst $ ZExt flag (IntegerType 32) []

835− box (FInt IT32) val

905+ box (FArith (ATInt (ITFixed IT32))) val

836

906

837cgOp LStrLt [x,y] = do

907cgOp LStrLt [x,y] = do

838 nx <- unbox FString x

908 nx <- unbox FString x

@@ -840,10 +910,10 @@ cgOp LStrLt [x,y] = do

840 cmp <- inst $ simpleCall "strcmp" [nx, ny]

910 cmp <- inst $ simpleCall "strcmp" [nx, ny]

841 flag <- inst $ ICmp IPred.ULT cmp (ConstantOperand (C.Int 32 0)) []

911 flag <- inst $ ICmp IPred.ULT cmp (ConstantOperand (C.Int 32 0)) []

842 val <- inst $ ZExt flag (IntegerType 32) []

912 val <- inst $ ZExt flag (IntegerType 32) []

843− box (FInt IT32) val

913+ box (FArith (ATInt (ITFixed IT32))) val

844

914

845cgOp (LIntStr ITBig) [x] = do

915cgOp (LIntStr ITBig) [x] = do

846− x' <- unbox (FInt ITBig) x

916+ x' <- unbox (FArith (ATInt ITBig)) x

847 ustr <- inst $ simpleCall "__gmpz_get_str"

917 ustr <- inst $ simpleCall "__gmpz_get_str"

848 [ ConstantOperand (C.Null (PointerType (IntegerType 8) (AddrSpace 0)))

918 [ ConstantOperand (C.Null (PointerType (IntegerType 8) (AddrSpace 0)))

849 , ConstantOperand (C.Int 32 10)

919 , ConstantOperand (C.Int 32 10)

@@ -851,7 +921,7 @@ cgOp (LIntStr ITBig) [x] = do

851 ]

921 ]

852 box FString ustr

922 box FString ustr

853cgOp (LIntStr ity) [x] = do

923cgOp (LIntStr ity) [x] = do

854− x' <- unbox (FInt ity) x

924+ x' <- unbox (FArith (ATInt ity)) x

855 x'' <- if itWidth ity < 64

925 x'' <- if itWidth ity < 64

856 then inst $ SExt x' (IntegerType 64) []

926 then inst $ SExt x' (IntegerType 64) []

857 else return x'

927 else return x'

@@ -860,7 +930,7 @@ cgOp (LStrInt ITBig) [s] = do

860 ns <- unbox FString s

930 ns <- unbox FString s

861 mpz <- alloc mpzTy

931 mpz <- alloc mpzTy

862 inst $ simpleCall "__gmpz_init_set_str" [mpz, ns, ConstantOperand $ C.Int 32 10]

932 inst $ simpleCall "__gmpz_init_set_str" [mpz, ns, ConstantOperand $ C.Int 32 10]

863− box (FInt ITBig) mpz

933+ box (FArith (ATInt ITBig)) mpz

864cgOp (LStrInt ity) [s] = do

934cgOp (LStrInt ity) [s] = do

865 ns <- unbox FString s

935 ns <- unbox FString s

866 nx <- inst $ simpleCall "strtoll"

936 nx <- inst $ simpleCall "strtoll"

@@ -869,9 +939,9 @@ cgOp (LStrInt ity) [s] = do

869 , ConstantOperand $ C.Int 32 10

939 , ConstantOperand $ C.Int 32 10

870 ]

940 ]

871 nx' <- case ity of

941 nx' <- case ity of

872− IT64 -> return nx

942+ (ITFixed IT64) -> return nx

873 _ -> inst $ Trunc nx (IntegerType (itWidth ity)) []

943 _ -> inst $ Trunc nx (IntegerType (itWidth ity)) []

874− box (FInt ity) nx'

944+ box (FArith (ATInt ity)) nx'

875

945

876cgOp LStrConcat [x,y] = cgStrCat x y

946cgOp LStrConcat [x,y] = cgStrCat x y

877

947

@@ -890,7 +960,7 @@ cgOp LStrHead [c] = do

890

960

891cgOp LStrIndex [s, i] = do

961cgOp LStrIndex [s, i] = do

892 ns <- unbox FString s

962 ns <- unbox FString s

893− ni <- unbox (FInt IT32) i

963+ ni <- unbox (FArith (ATInt (ITFixed IT32))) i

894 p <- inst $ GetElementPtr True ns [ni] []

964 p <- inst $ GetElementPtr True ns [ni] []

895 c <- inst $ Load False p Nothing 0 []

965 c <- inst $ Load False p Nothing 0 []

896 c' <- inst $ ZExt c (IntegerType 32) []

966 c' <- inst $ ZExt c (IntegerType 32) []

@@ -907,9 +977,9 @@ cgOp LStrLen [s] = do

907 ws <- getWordSize

977 ws <- getWordSize

908 len' <- case ws of

978 len' <- case ws of

909 32 -> return len

979 32 -> return len

910− x | x > 32 -> inst $ Trunc len (IntegerType $ fromInteger x) []

980+ x | x > 32 -> inst $ Trunc len (IntegerType 32) []

911− | x < 32 -> inst $ ZExt len (IntegerType $ fromInteger x) []

981+ | x < 32 -> inst $ ZExt len (IntegerType 32) []

912− box (FInt IT32) len'

982+ box (FArith (ATInt (ITFixed IT32))) len'

913

983

914cgOp LReadStr [p] = do

984cgOp LReadStr [p] = do

915 np <- unbox FPtr p

985 np <- unbox FPtr p

@@ -917,24 +987,26 @@ cgOp LReadStr [p] = do

917 box FString s

987 box FString s

918

988

919cgOp LStdIn [] = do

989cgOp LStdIn [] = do

990+ stdin <- getStdIn

920− ptr <- inst $ Load False (ConstantOperand . C.GlobalReference . Name $ "stdin") Nothing 0 []

991+ ptr <- inst $ Load False stdin Nothing 0 []

921 box FPtr ptr

992 box FPtr ptr

922cgOp LStdOut [] = do

993cgOp LStdOut [] = do

994+ stdout <- getStdOut

923− ptr <- inst $ Load False (ConstantOperand . C.GlobalReference . Name $ "stdout") Nothing 0 []

995+ ptr <- inst $ Load False stdout Nothing 0 []

924 box FPtr ptr

996 box FPtr ptr

925cgOp LStdErr [] = do

997cgOp LStdErr [] = do

998+ stdErr <- getStdErr

926− ptr <- inst $ Load False (ConstantOperand . C.GlobalReference . Name $ "stderr") Nothing 0 []

999+ ptr <- inst $ Load False stdErr Nothing 0 []

927 box FPtr ptr

1000 box FPtr ptr

928

1001

929−

930cgOp prim args = ierror $ "Unimplemented primitive: [" ++ show prim ++ "]("

1002cgOp prim args = ierror $ "Unimplemented primitive: [" ++ show prim ++ "]("

931 ++ intersperse ',' (take (length args) ['a'..]) ++ ")"

1003 ++ intersperse ',' (take (length args) ['a'..]) ++ ")"

932

1004

933−iCoerce :: (Operand -> Type -> InstructionMetadata -> Instruction) -> IntTy -> IntTy -> Operand -> Codegen Operand

1005+iCoerce :: (Operand -> Type -> InstructionMetadata -> Instruction) -> NativeTy -> NativeTy -> Operand -> Codegen Operand

934iCoerce operator from to x = do

1006iCoerce operator from to x = do

935− x' <- unbox (FInt from) x

1007+ x' <- unbox (FArith (ATInt (ITFixed from))) x

936− x'' <- inst $ operator x' (IntegerType $ itWidth to) []

1008+ x'' <- inst $ operator x' (ftyToTy (FArith (ATInt (ITFixed from)))) []

937− box (FInt to) x''

1009+ box (FArith (ATInt (ITFixed to))) x''

938

1010

939cgStrCat :: Operand -> Operand -> Codegen Operand

1011cgStrCat :: Operand -> Operand -> Codegen Operand

940cgStrCat x y = do

1012cgStrCat x y = do

@@ -943,7 +1015,7 @@ cgStrCat x y = do

943 xlen <- inst $ simpleCall "strlen" [x']

1015 xlen <- inst $ simpleCall "strlen" [x']

944 ylen <- inst $ simpleCall "strlen" [y']

1016 ylen <- inst $ simpleCall "strlen" [y']

945 zlen <- inst $ Add False True xlen ylen []

1017 zlen <- inst $ Add False True xlen ylen []

946− ws <- fromIntegral <$> getWordSize

1018+ ws <- getWordSize

947 total <- inst $ Add False True zlen (ConstantOperand (C.Int ws 1)) []

1019 total <- inst $ Add False True zlen (ConstantOperand (C.Int ws 1)) []

948 mem <- allocAtomic total

1020 mem <- allocAtomic total

949 inst $ simpleCall "memcpy" [mem, x', xlen]

1021 inst $ simpleCall "memcpy" [mem, x', xlen]

@@ -960,50 +1032,54 @@ cgStrCat x y = do

960ibin :: IntTy -> Operand -> Operand

1032ibin :: IntTy -> Operand -> Operand

961 -> (Operand -> Operand -> InstructionMetadata -> Instruction) -> Codegen Operand

1033 -> (Operand -> Operand -> InstructionMetadata -> Instruction) -> Codegen Operand

962ibin ity x y instCon = do

1034ibin ity x y instCon = do

963− nx <- unbox (FInt ity) x

1035+ nx <- unbox (FArith (ATInt ity)) x

964− ny <- unbox (FInt ity) y

1036+ ny <- unbox (FArith (ATInt ity)) y

965 nr <- inst $ instCon nx ny []

1037 nr <- inst $ instCon nx ny []

966− box (FInt ity) nr

1038+ box (FArith (ATInt ity)) nr

967

1039

968iun :: IntTy -> Operand -> (Operand -> InstructionMetadata -> Instruction) -> Codegen Operand

1040iun :: IntTy -> Operand -> (Operand -> InstructionMetadata -> Instruction) -> Codegen Operand

969iun ity x instCon = do

1041iun ity x instCon = do

970− nx <- unbox (FInt ity) x

1042+ nx <- unbox (FArith (ATInt ity)) x

971 nr <- inst $ instCon nx []

1043 nr <- inst $ instCon nx []

972− box (FInt ity) nr

1044+ box (FArith (ATInt ity)) nr

973

1045

974iCmp :: IntTy -> IPred.IntegerPredicate -> Operand -> Operand -> Codegen Operand

1046iCmp :: IntTy -> IPred.IntegerPredicate -> Operand -> Operand -> Codegen Operand

975iCmp ity pred x y = do

1047iCmp ity pred x y = do

976− nx <- unbox (FInt ity) x

1048+ nx <- unbox (FArith (ATInt ity)) x

977− ny <- unbox (FInt ity) y

1049+ ny <- unbox (FArith (ATInt ity)) y

978 nr <- inst $ ICmp pred nx ny []

1050 nr <- inst $ ICmp pred nx ny []

979− nr' <- inst $ ZExt nr (IntegerType 32) []

1051+ nr' <- inst $ SExt nr (ftyToTy $ cmpResultTy ity) []

980− box (FInt IT32) nr'

1052+ box (cmpResultTy ity) nr'

1053+

1054+cmpResultTy :: IntTy -> FType

1055+cmpResultTy v@(ITVec _ _) = FArith (ATInt v)

1056+cmpResultTy _ = FArith (ATInt (ITFixed IT32))

981

1057

982mpzBin :: String -> Operand -> Operand -> Codegen Operand

1058mpzBin :: String -> Operand -> Operand -> Codegen Operand

983mpzBin name x y = do

1059mpzBin name x y = do

984− nx <- unbox (FInt ITBig) x

1060+ nx <- unbox (FArith (ATInt ITBig)) x

985− ny <- unbox (FInt ITBig) y

1061+ ny <- unbox (FArith (ATInt ITBig)) y

986 nz <- alloc mpzTy

1062 nz <- alloc mpzTy

987 inst' $ simpleCall "__gmpz_init" [nz]

1063 inst' $ simpleCall "__gmpz_init" [nz]

988 inst' $ simpleCall ("__gmpz_" ++ name) [nz, nx, ny]

1064 inst' $ simpleCall ("__gmpz_" ++ name) [nz, nx, ny]

989− box (FInt ITBig) nz

1065+ box (FArith (ATInt ITBig)) nz

990

1066

991mpzUn :: String -> Operand -> Codegen Operand

1067mpzUn :: String -> Operand -> Codegen Operand

992mpzUn name x = do

1068mpzUn name x = do

993− nx <- unbox (FInt ITBig) x

1069+ nx <- unbox (FArith (ATInt ITBig)) x

994 nz <- alloc mpzTy

1070 nz <- alloc mpzTy

995 inst' $ simpleCall "__gmpz_init" [nz]

1071 inst' $ simpleCall "__gmpz_init" [nz]

996 inst' $ simpleCall ("__gmpz_" ++ name) [nz, nx]

1072 inst' $ simpleCall ("__gmpz_" ++ name) [nz, nx]

997− box (FInt ITBig) nz

1073+ box (FArith (ATInt ITBig)) nz

998

1074

999mpzCmp :: IPred.IntegerPredicate -> Operand -> Operand -> Codegen Operand

1075mpzCmp :: IPred.IntegerPredicate -> Operand -> Operand -> Codegen Operand

1000mpzCmp pred x y = do

1076mpzCmp pred x y = do

1001− nx <- unbox (FInt ITBig) x

1077+ nx <- unbox (FArith (ATInt ITBig)) x

1002− ny <- unbox (FInt ITBig) y

1078+ ny <- unbox (FArith (ATInt ITBig)) y

1003 cmp <- inst $ simpleCall "__gmpz_cmp" [nx, ny]

1079 cmp <- inst $ simpleCall "__gmpz_cmp" [nx, ny]

1004 result <- inst $ ICmp pred cmp (ConstantOperand (C.Int 32 0)) []

1080 result <- inst $ ICmp pred cmp (ConstantOperand (C.Int 32 0)) []

1005 i <- inst $ ZExt result (IntegerType 32) []

1081 i <- inst $ ZExt result (IntegerType 32) []

1006− box (FInt IT32) i

1082+ box (FArith (ATInt (ITFixed IT32))) i

1007

1083

1008simpleCall :: String -> [Operand] -> Instruction

1084simpleCall :: String -> [Operand] -> Instruction

1009simpleCall name args =

1085simpleCall name args =

src/IRTS/Compiler.hs+22−19

@@ -30,8 +30,8 @@ import System.FilePath ((</>), addTrailingPathSeparator)

31import Paths_idris

33−compile :: Target -> FilePath -> Term -> Idris ()

33+compile :: Codegen -> FilePath -> Term -> Idris ()

34−compile target f tm

34+compile codegen f tm

35 = do checkMVs

36 let tmnames = namesUsed (STerm tm)

37 usedIn <- mapM (allNames []) tmnames

@@ -39,9 +39,9 @@ compile target f tm

39 defsIn <- mkDecls tm (concat used)

40 findUnusedArgs (concat used)

41 maindef <- irMain tm

42− objs <- getObjectFiles target

42+ objs <- getObjectFiles codegen

43− libs <- getLibs target

43+ libs <- getLibs codegen

44− hdrs <- getHdrs target

44+ hdrs <- getHdrs codegen

45 let defs = defsIn ++ [(MN 0 "runMain", maindef)]

46 -- iputStrLn $ showSep "\n" (map show defs)

47 let (nexttag, tagged) = addTags 65536 (liftAll defs)

@@ -64,9 +64,12 @@ compile target f tm

64 case dumpDefun of

65 Nothing -> return ()

66 Just f -> liftIO $ writeFile f (dumpDefuns defuns)

67+ triple <- targetTriple

68+ cpu <- targetCPU

69+ optimize <- optLevel

67 iLOG "Building output"

70 iLOG "Building output"

68 case checked of

71 case checked of

69− OK c -> liftIO $ case target of

72+ OK c -> liftIO $ case codegen of

70 ViaC ->

73 ViaC ->

71 codegenC c f outty hdrs

74 codegenC c f outty hdrs

72 (concatMap mkObj objs)

75 (concatMap mkObj objs)

@@ -77,7 +80,7 @@ compile target f tm

77 codegenJavaScript JavaScript c f outty

80 codegenJavaScript JavaScript c f outty

78 ViaNode ->

81 ViaNode ->

79 codegenJavaScript Node c f outty

82 codegenJavaScript Node c f outty

80− ViaLLVM -> codegenLLVM c f outty

83+ ViaLLVM -> codegenLLVM c triple cpu optimize f outty

82 Bytecode -> dumpBC c f

85 Bytecode -> dumpBC c f

83 Error e -> fail $ show e

86 Error e -> fail $ show e

@@ -296,7 +299,7 @@ mkIty' _ = FAny

296-- would be better if these FInt types were evaluated at compile time

299-- would be better if these FInt types were evaluated at compile time

297-- TODO: add %eval directive for such things

300-- TODO: add %eval directive for such things

298

301

299−mkIty "FFloat" = FDouble

302+mkIty "FFloat" = FArith ATFloat

300mkIty "FInt" = mkIntIty "ITNative"

303mkIty "FInt" = mkIntIty "ITNative"

301mkIty "FChar" = mkIntIty "IT8"

304mkIty "FChar" = mkIntIty "IT8"

302mkIty "FShort" = mkIntIty "IT16"

305mkIty "FShort" = mkIntIty "IT16"

@@ -308,11 +311,11 @@ mkIty "FFunction" = FFunction

308mkIty "FFunctionIO" = FFunctionIO

311mkIty "FFunctionIO" = FFunctionIO

309mkIty x = error $ "Unknown type " ++ x

312mkIty x = error $ "Unknown type " ++ x

310

313

311−mkIntIty "ITNative" = FInt ITNative

314+mkIntIty "ITNative" = FArith (ATInt ITNative)

312−mkIntIty "IT8" = FInt IT8

315+mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))

313−mkIntIty "IT16" = FInt IT16

316+mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))

314−mkIntIty "IT32" = FInt IT32

317+mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))

315−mkIntIty "IT64" = FInt IT64

318+mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))

316

319

317zname = NS (UN "O") ["Nat","Prelude"]

320zname = NS (UN "O") ["Nat","Prelude"]

318sname = NS (UN "S") ["Nat","Prelude"]

321sname = NS (UN "S") ["Nat","Prelude"]

@@ -366,15 +369,15 @@ instance ToIR SC where

366 matchable (Str _) = True

369 matchable (Str _) = True

367 matchable _ = False

370 matchable _ = False

368

371

369− matchableTy IType = True

372+ matchableTy (AType (ATInt ITNative)) = True

370− matchableTy BIType = True

373+ matchableTy (AType (ATInt ITBig)) = True

371 matchableTy ChType = True

374 matchableTy ChType = True

372 matchableTy StrType = True

375 matchableTy StrType = True

373

376

374− matchableTy B8Type = True

377+ matchableTy (AType (ATInt (ITFixed IT8))) = True

375− matchableTy B16Type = True

378+ matchableTy (AType (ATInt (ITFixed IT16))) = True

376− matchableTy B32Type = True

379+ matchableTy (AType (ATInt (ITFixed IT32))) = True

377− matchableTy B64Type = True

380+ matchableTy (AType (ATInt (ITFixed IT64))) = True

378

381

379 matchableTy _ = False

382 matchableTy _ = False

380

383

src/IRTS/LParser.hs+32−32

@@ -49,8 +49,8 @@ strlit = PTok.stringLiteral lexer

49chlit = PTok.charLiteral lexer

50lchar = lexeme.char

52−fovm :: Target -> OutputType -> FilePath -> IO ()

52+fovm :: Codegen -> OutputType -> FilePath -> IO ()

53−fovm tgt outty f

53+fovm cgn outty f

54 = do defs <- parseFOVM f

55 let (nexttag, tagged) = addTags 0 (liftAll defs)

56 ctxtIn = addAlist tagged emptyContext

@@ -59,7 +59,7 @@ fovm tgt outty f

59 let checked = checkDefs defuns (toAlist defuns)

60-- print checked

61 case checked of

62− OK c -> case tgt of

62+ OK c -> case cgn of

63 ViaC -> codegenC c "a.out" outty ["math.h"] "" "" TRACE

64 ViaJava -> codegenJava [] c "a.out" [] [] outty

65 Error e -> fail $ show e

@@ -92,39 +92,39 @@ pLDecl = do reserved "data"

93pLExp = buildExpressionParser optable pLExp'

95−optable = [[binary "*" (\x y -> LOp (LTimes ITNative) [x,y]) AssocLeft,

95+optable = [[binary "*" (\x y -> LOp (LTimes (ATInt ITNative)) [x,y]) AssocLeft,

96− binary "/" (\x y -> LOp (LSDiv ITNative) [x,y]) AssocLeft,

96+ binary "/" (\x y -> LOp (LSDiv (ATInt ITNative)) [x,y]) AssocLeft,

97− binary "*." (\x y -> LOp LFTimes [x,y]) AssocLeft,

97+ binary "*." (\x y -> LOp (LTimes ATFloat) [x,y]) AssocLeft,

98− binary "/." (\x y -> LOp LFDiv [x,y]) AssocLeft,

98+ binary "/." (\x y -> LOp (LSDiv ATFloat) [x,y]) AssocLeft,

99− binary "*:" (\x y -> LOp (LTimes ITBig) [x,y]) AssocLeft,

99+ binary "*:" (\x y -> LOp (LTimes (ATInt ITBig)) [x,y]) AssocLeft,

100− binary "/:" (\x y -> LOp (LSDiv ITBig) [x,y]) AssocLeft

100+ binary "/:" (\x y -> LOp (LSDiv (ATInt ITBig)) [x,y]) AssocLeft

101 ],

102 [

103− binary "+" (\x y -> LOp (LPlus ITNative) [x,y]) AssocLeft,

103+ binary "+" (\x y -> LOp (LPlus (ATInt ITNative)) [x,y]) AssocLeft,

104− binary "-" (\x y -> LOp (LMinus ITNative) [x,y]) AssocLeft,

104+ binary "-" (\x y -> LOp (LMinus (ATInt ITNative)) [x,y]) AssocLeft,

105 binary "++" (\x y -> LOp LStrConcat [x,y]) AssocLeft,

106− binary "+." (\x y -> LOp LFPlus [x,y]) AssocLeft,

106+ binary "+." (\x y -> LOp (LPlus ATFloat) [x,y]) AssocLeft,

107− binary "-." (\x y -> LOp LFMinus [x,y]) AssocLeft,

107+ binary "-." (\x y -> LOp (LMinus ATFloat) [x,y]) AssocLeft,

108− binary "+:" (\x y -> LOp (LPlus ITBig) [x,y]) AssocLeft,

108+ binary "+:" (\x y -> LOp (LPlus (ATInt ITBig)) [x,y]) AssocLeft,

109− binary "-:" (\x y -> LOp (LMinus ITBig) [x,y]) AssocLeft

109+ binary "-:" (\x y -> LOp (LMinus (ATInt ITBig)) [x,y]) AssocLeft

110 ],

111 [

112− binary "==" (\x y -> LOp (LEq ITNative) [x, y]) AssocNone,

112+ binary "==" (\x y -> LOp (LEq (ATInt ITNative)) [x, y]) AssocNone,

113− binary "==." (\x y -> LOp LFEq [x, y]) AssocNone,

113+ binary "==." (\x y -> LOp (LEq ATFloat) [x, y]) AssocNone,

114− binary "<" (\x y -> LOp (LLt ITNative) [x, y]) AssocNone,

114+ binary "<" (\x y -> LOp (LLt (ATInt ITNative)) [x, y]) AssocNone,

115− binary "<." (\x y -> LOp LFLt [x, y]) AssocNone,

115+ binary "<." (\x y -> LOp (LLt ATFloat) [x, y]) AssocNone,

116− binary ">" (\x y -> LOp (LGt ITNative) [x, y]) AssocNone,

116+ binary ">" (\x y -> LOp (LGt (ATInt ITNative)) [x, y]) AssocNone,

117− binary ">." (\x y -> LOp LFGt [x, y]) AssocNone,

117+ binary ">." (\x y -> LOp (LGt ATFloat) [x, y]) AssocNone,

118− binary "<=" (\x y -> LOp (LLe ITNative) [x, y]) AssocNone,

118+ binary "<=" (\x y -> LOp (LLe (ATInt ITNative)) [x, y]) AssocNone,

119− binary "<=." (\x y -> LOp LFLe [x, y]) AssocNone,

119+ binary "<=." (\x y -> LOp (LLe ATFloat) [x, y]) AssocNone,

120− binary ">=" (\x y -> LOp (LGe ITNative) [x, y]) AssocNone,

120+ binary ">=" (\x y -> LOp (LGe (ATInt ITNative)) [x, y]) AssocNone,

121− binary ">=." (\x y -> LOp LFGe [x, y]) AssocNone,

121+ binary ">=." (\x y -> LOp (LGe ATFloat) [x, y]) AssocNone,

122

123− binary "==:" (\x y -> LOp (LEq ITBig) [x, y]) AssocNone,

123+ binary "==:" (\x y -> LOp (LEq (ATInt ITBig)) [x, y]) AssocNone,

124− binary "<:" (\x y -> LOp (LLt ITBig) [x, y]) AssocNone,

124+ binary "<:" (\x y -> LOp (LLt (ATInt ITBig)) [x, y]) AssocNone,

125− binary ">:" (\x y -> LOp (LGt ITBig) [x, y]) AssocNone,

125+ binary ">:" (\x y -> LOp (LGt (ATInt ITBig)) [x, y]) AssocNone,

126− binary "<=:" (\x y -> LOp (LLe ITBig) [x, y]) AssocNone,

126+ binary "<=:" (\x y -> LOp (LLe (ATInt ITBig)) [x, y]) AssocNone,

127− binary ">=:" (\x y -> LOp (LGe ITBig) [x, y]) AssocNone

127+ binary ">=:" (\x y -> LOp (LGe (ATInt ITBig)) [x, y]) AssocNone

128 ]]

129

130binary name f assoc = Infix (do reservedOp name; return f) assoc

@@ -164,8 +164,8 @@ pLExp' = try (do lchar '%'; pCast)

164

165pLang = do reserved "C"; return LANG_C

166

167−pType = do reserved "Int"; return (FInt ITNative)

167+pType = do reserved "Int"; return (FArith (ATInt ITNative))

168− <|> do reserved "Float"; return FDouble

168+ <|> do reserved "Float"; return (FArith ATFloat)

169 <|> do reserved "String"; return FString

170 <|> do reserved "Unit"; return FUnit

171 <|> do reserved "Ptr"; return FPtr

src/IRTS/Lang.hs+7−27

@@ -3,7 +3,6 @@ module IRTS.Lang where

3import Core.TT

4import Control.Monad.State hiding(lift)

5import Data.List

6−import Foreign.Storable (sizeOf)

7import Debug.Trace

6import Debug.Trace

9data LVar = Loc Int | Glob Name

8data LVar = Loc Int | Glob Name

@@ -29,33 +28,12 @@ data LExp = LV LVar

29-- Primitive operators. Backends are not *required* to implement all

28-- Primitive operators. Backends are not *required* to implement all

30-- of these, but should report an error if they are unable

29-- of these, but should report an error if they are unable

32−data IntTy = ITNative | IT8 | IT16 | IT32 | IT64 | ITBig

33− deriving (Show, Eq)

34−

35−intTyWidth :: IntTy -> Int

36−intTyWidth IT8 = 8

37−intTyWidth IT16 = 16

38−intTyWidth IT32 = 32

39−intTyWidth IT64 = 64

40−intTyWidth ITNative = 8 * sizeOf (0 :: Int)

41−intTyWidth ITBig = error "IRTS.Lang.intTyWidth: Big integers have variable width"

42−

43−intTyToConst :: IntTy -> Const

44−intTyToConst IT8 = B8Type

45−intTyToConst IT16 = B16Type

46−intTyToConst IT32 = B32Type

47−intTyToConst IT64 = B64Type

48−intTyToConst ITBig = BIType

49−intTyToConst ITNative = IType

50−

51−data PrimFn = LPlus IntTy | LMinus IntTy | LTimes IntTy

31+data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

52− | LUDiv IntTy | LSDiv IntTy | LURem IntTy | LSRem IntTy

32+ | LUDiv IntTy | LSDiv ArithTy | LURem IntTy | LSRem ArithTy

53 | LAnd IntTy | LOr IntTy | LXOr IntTy | LCompl IntTy

33 | LAnd IntTy | LOr IntTy | LXOr IntTy | LCompl IntTy

54 | LSHL IntTy | LLSHR IntTy | LASHR IntTy

34 | LSHL IntTy | LLSHR IntTy | LASHR IntTy

56 | LSExt IntTy IntTy | LZExt IntTy IntTy | LTrunc IntTy IntTy

36 | LSExt IntTy IntTy | LZExt IntTy IntTy | LTrunc IntTy IntTy

57− | LFPlus | LFMinus | LFTimes | LFDiv

59 | LStrConcat | LStrLt | LStrEq | LStrLen

37 | LStrConcat | LStrLt | LStrEq | LStrLen

60 | LIntFloat IntTy | LFloatInt IntTy | LIntStr IntTy | LStrInt IntTy

38 | LIntFloat IntTy | LFloatInt IntTy | LIntStr IntTy | LStrInt IntTy

61 | LFloatStr | LStrFloat | LChInt IntTy | LIntCh IntTy

39 | LFloatStr | LStrFloat | LChInt IntTy | LIntCh IntTy

@@ -64,6 +42,9 @@ data PrimFn = LPlus IntTy | LMinus IntTy | LTimes IntTy

65 | LFSqrt | LFFloor | LFCeil

43 | LFSqrt | LFFloor | LFCeil

45+ -- construction element extraction element insertion

46+ | LMkVec NativeTy Int | LIdxVec NativeTy Int | LUpdateVec NativeTy Int

47+

68 | LStdIn | LStdOut | LStdErr

49 | LStdIn | LStdOut | LStdErr

@@ -79,14 +60,13 @@ data PrimFn = LPlus IntTy | LMinus IntTy | LTimes IntTy

79data FLang = LANG_C

60data FLang = LANG_C

80 deriving (Show, Eq)

61 deriving (Show, Eq)

82−data FType = FInt IntTy

63+data FType = FArith ArithTy

83 | FFunction

64 | FFunction

84 | FFunctionIO

65 | FFunctionIO

85 | FChar

66 | FChar

86 | FString

67 | FString

87 | FUnit

68 | FUnit

88 | FPtr

69 | FPtr

89− | FDouble

90 | FAny

70 | FAny

91 deriving (Show, Eq)

71 deriving (Show, Eq)

src/Idris/AbsSyntax.hs+49−19

@@ -30,19 +30,19 @@ import Util.System

30getContext :: Idris Context

31getContext = do i <- getIState; return (tt_ctxt i)

33−forTarget :: Target -> [(Target, a)] -> [a]

33+forCodegen :: Codegen -> [(Codegen, a)] -> [a]

34−forTarget tgt xs = [x | (tgt', x) <- xs, tgt == tgt']

34+forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']

36−getObjectFiles :: Target -> Idris [FilePath]

36+getObjectFiles :: Codegen -> Idris [FilePath]

37−getObjectFiles tgt = do i <- getIState; return (forTarget tgt $ idris_objs i)

37+getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)

39−addObjectFile :: Target -> FilePath -> Idris ()

39+addObjectFile :: Codegen -> FilePath -> Idris ()

40addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = (tgt, f) : idris_objs i }

42−getLibs :: Target -> Idris [String]

42+getLibs :: Codegen -> Idris [String]

43−getLibs tgt = do i <- getIState; return (forTarget tgt $ idris_libs i)

43+getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)

45−addLib :: Target -> String -> Idris ()

45+addLib :: Codegen -> String -> Idris ()

46addLib tgt f = do i <- getIState; putIState $ i { idris_libs = (tgt, f) : idris_libs i }

48addDyLib :: [String] -> Idris (Either DynamicLib String)

@@ -55,7 +55,7 @@ addDyLib libs = do i <- getIState

55 putIState $ i { idris_dynamic_libs = x:ls }

56 return (Left x)

58−addHdr :: Target -> String -> Idris ()

58+addHdr :: Codegen -> String -> Idris ()

59addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = (tgt, f) : idris_hdrs i }

61addLangExt :: LanguageExt -> Idris ()

@@ -163,8 +163,8 @@ addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }

163clearIBC :: Idris ()

164clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }

165

166−getHdrs :: Target -> Idris [String]

166+getHdrs :: Codegen -> Idris [String]

167−getHdrs tgt = do i <- getIState; return (forTarget tgt $ idris_hdrs i)

167+getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)

168

169setErrLine :: Int -> Idris ()

170setErrLine x = do i <- getIState;

@@ -345,15 +345,15 @@ getQuiet = do i <- getIState

345 let opts = idris_options i

346 return (opt_quiet opts)

347

348−setTarget :: Target -> Idris ()

348+setCodegen :: Codegen -> Idris ()

349−setTarget t = do i <- getIState

349+setCodegen t = do i <- getIState

350− let opts = idris_options i

350+ let opts = idris_options i

351− let opt' = opts { opt_target = t }

351+ let opt' = opts { opt_codegen = t }

352− putIState $ i { idris_options = opt' }

352+ putIState $ i { idris_options = opt' }

353

354−target :: Idris Target

354+codegen :: Idris Codegen

355−target = do i <- getIState

355+codegen = do i <- getIState

356− return (opt_target (idris_options i))

356+ return (opt_codegen (idris_options i))

357

358setOutputTy :: OutputType -> Idris ()

359setOutputTy t = do i <- getIState

@@ -370,6 +370,36 @@ setIdeSlave True = do i <- getIState

370 putIState $ i { idris_outputmode = (IdeSlave 0) }

371setIdeSlave False = return ()

372

373+setTargetTriple :: String -> Idris ()

374+setTargetTriple t = do i <- getIState

375+ let opts = idris_options i

376+ opt' = opts { opt_triple = t }

377+ putIState $ i { idris_options = opt' }

378+

379+targetTriple :: Idris String

380+targetTriple = do i <- getIState

381+ return (opt_triple (idris_options i))

382+

383+setTargetCPU :: String -> Idris ()

384+setTargetCPU t = do i <- getIState

385+ let opts = idris_options i

386+ opt' = opts { opt_cpu = t }

387+ putIState $ i { idris_options = opt' }

388+

389+targetCPU :: Idris String

390+targetCPU = do i <- getIState

391+ return (opt_cpu (idris_options i))

392+

393+setOptLevel :: Int -> Idris ()

394+setOptLevel t = do i <- getIState

395+ let opts = idris_options i

396+ opt' = opts { opt_optLevel = t }

397+ putIState $ i { idris_options = opt' }

398+

399+optLevel :: Idris Int

400+optLevel = do i <- getIState

401+ return (opt_optLevel (idris_options i))

402+

373verbose :: Idris Bool

403verbose :: Idris Bool

374verbose = do i <- getIState

404verbose = do i <- getIState

375 return (opt_verbose (idris_options i))

405 return (opt_verbose (idris_options i))

src/Idris/AbsSyntaxTree.hs+25−16

@@ -33,10 +33,13 @@ data IOption = IOption { opt_logLevel :: Int,

33 opt_repl :: Bool,

34 opt_verbose :: Bool,

35 opt_quiet :: Bool,

36− opt_target :: Target,

36+ opt_codegen :: Codegen,

37 opt_outputTy :: OutputType,

38 opt_ibcsubdir :: FilePath,

39 opt_importdirs :: [FilePath],

40+ opt_triple :: String,

41+ opt_cpu :: String,

42+ opt_optLevel :: Int,

40 opt_cmdline :: [Opt] -- remember whole command line

43 opt_cmdline :: [Opt] -- remember whole command line

41 }

44 }

42 deriving (Show, Eq)

45 deriving (Show, Eq)

@@ -50,10 +53,13 @@ defaultOpts = IOption { opt_logLevel = 0

50 , opt_repl = True

53 , opt_repl = True

51 , opt_verbose = True

54 , opt_verbose = True

52 , opt_quiet = False

55 , opt_quiet = False

53− , opt_target = ViaC

56+ , opt_codegen = ViaC

54 , opt_outputTy = Executable

57 , opt_outputTy = Executable

55 , opt_ibcsubdir = ""

58 , opt_ibcsubdir = ""

56 , opt_importdirs = []

59 , opt_importdirs = []

60+ , opt_triple = ""

61+ , opt_cpu = ""

62+ , opt_optLevel = 2

57 , opt_cmdline = []

63 , opt_cmdline = []

58 }

64 }

@@ -95,9 +101,9 @@ data IState = IState {

95 syntax_keywords :: [String],

101 syntax_keywords :: [String],

96 imported :: [FilePath], -- ^ The imported modules

102 imported :: [FilePath], -- ^ The imported modules

97 idris_scprims :: [(Name, (Int, PrimFn))],

103 idris_scprims :: [(Name, (Int, PrimFn))],

98− idris_objs :: [(Target, FilePath)],

104+ idris_objs :: [(Codegen, FilePath)],

99− idris_libs :: [(Target, String)],

105+ idris_libs :: [(Codegen, String)],

100− idris_hdrs :: [(Target, String)],

106+ idris_hdrs :: [(Codegen, String)],

101 proof_list :: [(Name, [String])],

107 proof_list :: [(Name, [String])],

102 errLine :: Maybe Int,

108 errLine :: Maybe Int,

103 lastParse :: Maybe Name,

109 lastParse :: Maybe Name,

@@ -145,10 +151,10 @@ data IBCWrite = IBCFix FixDecl

145 | IBCSyntax Syntax

151 | IBCSyntax Syntax

146 | IBCKeyword String

152 | IBCKeyword String

147 | IBCImport FilePath

153 | IBCImport FilePath

148− | IBCObj Target FilePath

154+ | IBCObj Codegen FilePath

149− | IBCLib Target String

155+ | IBCLib Codegen String

150 | IBCDyLib String

156 | IBCDyLib String

151− | IBCHeader Target String

157+ | IBCHeader Codegen String

152 | IBCAccess Name Accessibility

158 | IBCAccess Name Accessibility

153 | IBCTotal Name Totality

159 | IBCTotal Name Totality

154 | IBCFlags Name [FnOpt]

160 | IBCFlags Name [FnOpt]

@@ -171,12 +177,12 @@ type Idris = StateT IState IO

171

177

172-- Commands in the REPL

178-- Commands in the REPL

173

179

174−data Target = ViaC

180+data Codegen = ViaC

175− | ViaJava

181+ | ViaJava

176− | ViaNode

182+ | ViaNode

177− | ViaJavaScript

183+ | ViaJavaScript

178− | ViaLLVM

184+ | ViaLLVM

179− | Bytecode

185+ | Bytecode

180 deriving (Show, Eq)

186 deriving (Show, Eq)

181

187

182-- | REPL commands

188-- | REPL commands

@@ -191,7 +197,7 @@ data Command = Quit

191 | ChangeDirectory FilePath

197 | ChangeDirectory FilePath

192 | ModImport String

198 | ModImport String

193 | Edit

199 | Edit

194− | Compile Target String

200+ | Compile Codegen String

195 | Execute

201 | Execute

196 | ExecVal PTerm

202 | ExecVal PTerm

197 | NewCompile String

203 | NewCompile String

@@ -251,10 +257,13 @@ data Opt = Filename String

251 | DumpDefun String

257 | DumpDefun String

252 | DumpCases String

258 | DumpCases String

253 | FOVM String

259 | FOVM String

254− | UseTarget Target

260+ | UseCodegen Codegen

255 | OutputTy OutputType

261 | OutputTy OutputType

256 | Extension LanguageExt

262 | Extension LanguageExt

257 | InterpretScript String

263 | InterpretScript String

264+ | TargetTriple String

265+ | TargetCPU String

266+ | OptLevel Int

258 deriving (Show, Eq)

267 deriving (Show, Eq)

259

268

260-- Parsed declarations

269-- Parsed declarations

src/Idris/ElabDecls.hs+1−1

@@ -1174,7 +1174,7 @@ elabInstance info syn fc cs n ps t expn ds

1174-- mapM_ (elabDecl EAll info) (concat fns)

1175 where

1176 intInst = case ps of

1177− [PConstant IType] -> True

1177+ [PConstant (AType (ATInt ITNative))] -> True

1178 _ -> False

1179

1180 checkNotOverlapping i t n

src/Idris/ElabTerm.hs+15−15

@@ -653,7 +653,7 @@ resolveTC depth fn ist

653

654 needsDefault t num@(P _ (NS (UN "Num") ["Builtins"]) _) [P Bound a _]

655 = do focus a

656− fill (RConstant IType) -- default Int

656+ fill (RConstant (AType (ATInt ITNative))) -- default Int

657 solve

658 return False

659 needsDefault t f as

@@ -1060,15 +1060,15 @@ reifyTTBinderApp reif f [t]

1060reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))

1061

1062reifyTTConst :: Term -> ElabD Const

1063−reifyTTConst (P _ n _) | n == reflm "IType" = return $ IType

1063+reifyTTConst (P _ n _) | n == reflm "IType" = return (AType (ATInt ITNative))

1064−reifyTTConst (P _ n _) | n == reflm "BIType" = return $ BIType

1064+reifyTTConst (P _ n _) | n == reflm "BIType" = return (AType (ATInt ITBig))

1065−reifyTTConst (P _ n _) | n == reflm "FlType" = return $ FlType

1065+reifyTTConst (P _ n _) | n == reflm "FlType" = return (AType ATFloat)

1066reifyTTConst (P _ n _) | n == reflm "ChType" = return $ ChType

1067reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType

1068−reifyTTConst (P _ n _) | n == reflm "B8Type" = return $ B8Type

1068+reifyTTConst (P _ n _) | n == reflm "B8Type" = return (AType (ATInt (ITFixed IT8)))

1069−reifyTTConst (P _ n _) | n == reflm "B16Type" = return $ B16Type

1069+reifyTTConst (P _ n _) | n == reflm "B16Type" = return (AType (ATInt (ITFixed IT16)))

1070−reifyTTConst (P _ n _) | n == reflm "B32Type" = return $ B32Type

1070+reifyTTConst (P _ n _) | n == reflm "B32Type" = return (AType (ATInt (ITFixed IT32)))

1071−reifyTTConst (P _ n _) | n == reflm "B64Type" = return $ B64Type

1071+reifyTTConst (P _ n _) | n == reflm "B64Type" = return (AType (ATInt (ITFixed IT64)))

1072reifyTTConst (P _ n _) | n == reflm "PtrType" = return $ PtrType

1073reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType

1074reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot

@@ -1178,19 +1178,19 @@ reflectConstant c@(BI _) = reflCall "BI" [RConstant c]

1178reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]

1179reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]

1180reflectConstant c@(Str _) = reflCall "Str" [RConstant c]

1181−reflectConstant (IType) = Var (reflm "IType")

1181+reflectConstant (AType (ATInt ITNative)) = Var (reflm "IType")

1182−reflectConstant (BIType) = Var (reflm "BIType")

1182+reflectConstant (AType (ATInt ITBig)) = Var (reflm "BIType")

1183−reflectConstant (FlType) = Var (reflm "FlType")

1183+reflectConstant (AType ATFloat) = Var (reflm "FlType")

1184reflectConstant (ChType) = Var (reflm "ChType")

1185reflectConstant (StrType) = Var (reflm "StrType")

1186reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]

1187reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]

1188reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]

1189reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]

1190−reflectConstant (B8Type) = Var (reflm "B8Type")

1190+reflectConstant (AType (ATInt (ITFixed IT8))) = Var (reflm "B8Type")

1191−reflectConstant (B16Type) = Var (reflm "B16Type")

1191+reflectConstant (AType (ATInt (ITFixed IT16))) = Var (reflm "B16Type")

1192−reflectConstant (B32Type) = Var (reflm "B32Type")

1192+reflectConstant (AType (ATInt (ITFixed IT32))) = Var (reflm "B32Type")

1193−reflectConstant (B64Type) = Var (reflm "B64Type")

1193+reflectConstant (AType (ATInt (ITFixed IT64))) = Var (reflm "B64Type")

1194reflectConstant (PtrType) = Var (reflm "PtrType")

1195reflectConstant (VoidType) = Var (reflm "VoidType")

1196reflectConstant (Forgot) = Var (reflm "Forgot")

src/Idris/IBC.hs+40−23

@@ -11,6 +11,7 @@ import Idris.Imports

11import Idris.Error

13import Data.Binary

14+import Data.Vector.Binary

14import Data.List

15import Data.List

15import Data.ByteString.Lazy as B hiding (length, elem)

16import Data.ByteString.Lazy as B hiding (length, elem)

16import Control.Monad

17import Control.Monad

@@ -38,10 +39,10 @@ data IBCFile = IBCFile { ver :: Word8,

38 ibc_optimise :: [(Name, OptInfo)],

39 ibc_optimise :: [(Name, OptInfo)],

39 ibc_syntax :: [Syntax],

40 ibc_syntax :: [Syntax],

40 ibc_keywords :: [String],

41 ibc_keywords :: [String],

41− ibc_objs :: [(Target, FilePath)],

42+ ibc_objs :: [(Codegen, FilePath)],

42− ibc_libs :: [(Target, String)],

43+ ibc_libs :: [(Codegen, String)],

43 ibc_dynamic_libs :: [String],

44 ibc_dynamic_libs :: [String],

44− ibc_hdrs :: [(Target, String)],

45+ ibc_hdrs :: [(Codegen, String)],

45 ibc_access :: [(Name, Accessibility)],

46 ibc_access :: [(Name, Accessibility)],

46 ibc_total :: [(Name, Totality)],

47 ibc_total :: [(Name, Totality)],

47 ibc_flags :: [(Name, [FnOpt])],

48 ibc_flags :: [(Name, [FnOpt])],

@@ -243,10 +244,10 @@ pKeywords :: [String] -> Idris ()

243pKeywords k = do i <- getIState

244pKeywords k = do i <- getIState

244 putIState (i { syntax_keywords = k ++ syntax_keywords i })

245 putIState (i { syntax_keywords = k ++ syntax_keywords i })

245

246

246−pObjs :: [(Target, FilePath)] -> Idris ()

247+pObjs :: [(Codegen, FilePath)] -> Idris ()

247pObjs os = mapM_ (uncurry addObjectFile) os

248pObjs os = mapM_ (uncurry addObjectFile) os

248

249

249−pLibs :: [(Target, String)] -> Idris ()

250+pLibs :: [(Codegen, String)] -> Idris ()

250pLibs ls = mapM_ (uncurry addLib) ls

251pLibs ls = mapM_ (uncurry addLib) ls

251

252

252pDyLibs :: [String] -> Idris ()

253pDyLibs :: [String] -> Idris ()

@@ -256,7 +257,7 @@ pDyLibs ls = do res <- mapM (addDyLib . return) ls

256 where checkLoad (Left _) = return ()

257 where checkLoad (Left _) = return ()

257 checkLoad (Right err) = fail err

258 checkLoad (Right err) = fail err

258

259

259−pHdrs :: [(Target, String)] -> Idris ()

260+pHdrs :: [(Codegen, String)] -> Idris ()

260pHdrs hs = mapM_ (uncurry addHdr) hs

261pHdrs hs = mapM_ (uncurry addHdr) hs

261

262

262pDefs :: [(Name, Def)] -> Idris ()

263pDefs :: [(Name, Def)] -> Idris ()

@@ -364,7 +365,7 @@ instance Binary Name where

364 3 -> return NErased

365 3 -> return NErased

365 _ -> error "Corrupted binary data for Name"

366 _ -> error "Corrupted binary data for Name"

366

367

367−

368+

368instance Binary Const where

369instance Binary Const where

369 put x

370 put x

370 = case x of

371 = case x of

@@ -383,17 +384,23 @@ instance Binary Const where

383 B32 x1 -> putWord8 7 >> put x1

384 B32 x1 -> putWord8 7 >> put x1

384 B64 x1 -> putWord8 8 >> put x1

385 B64 x1 -> putWord8 8 >> put x1

385

386

386− IType -> putWord8 9

387+ (AType (ATInt ITNative)) -> putWord8 9

387− BIType -> putWord8 10

388+ (AType (ATInt ITBig)) -> putWord8 10

388− FlType -> putWord8 11

389+ (AType ATFloat) -> putWord8 11

389 ChType -> putWord8 12

390 ChType -> putWord8 12

390 StrType -> putWord8 13

391 StrType -> putWord8 13

391 PtrType -> putWord8 14

392 PtrType -> putWord8 14

392 Forgot -> putWord8 15

393 Forgot -> putWord8 15

393− B8Type -> putWord8 16

394+ (AType (ATInt (ITFixed ity))) -> putWord8 (fromIntegral (16 + fromEnum ity)) -- 16-19 inclusive

394− B16Type -> putWord8 17

395+ (AType (ATInt (ITVec ity count))) -> do

395− B32Type -> putWord8 18

396+ putWord8 20

396− B64Type -> putWord8 19

397+ putWord8 (fromIntegral . fromEnum $ ity)

398+ putWord8 (fromIntegral count)

399+

400+ B8V x1 -> putWord8 21 >> put x1

401+ B16V x1 -> putWord8 22 >> put x1

402+ B32V x1 -> putWord8 23 >> put x1

403+ B64V x1 -> putWord8 24 >> put x1

397 get

404 get

398 = do i <- getWord8

405 = do i <- getWord8

399 case i of

406 case i of

@@ -412,18 +419,28 @@ instance Binary Const where

412 7 -> fmap B32 get

419 7 -> fmap B32 get

413 8 -> fmap B64 get

420 8 -> fmap B64 get

414

421

415− 9 -> return IType

422+ 9 -> return (AType (ATInt ITNative))

416− 10 -> return BIType

423+ 10 -> return (AType (ATInt ITBig))

417− 11 -> return FlType

424+ 11 -> return (AType ATFloat)

418 12 -> return ChType

425 12 -> return ChType

419 13 -> return StrType

426 13 -> return StrType

420 14 -> return PtrType

427 14 -> return PtrType

421 15 -> return Forgot

428 15 -> return Forgot

422

429

423− 16 -> return B8Type

430+ 16 -> return (AType (ATInt (ITFixed IT8)))

424− 17 -> return B16Type

431+ 17 -> return (AType (ATInt (ITFixed IT16)))

425− 18 -> return B32Type

432+ 18 -> return (AType (ATInt (ITFixed IT32)))

426− 19 -> return B64Type

433+ 19 -> return (AType (ATInt (ITFixed IT64)))

434+

435+ 20 -> do

436+ e <- getWord8

437+ c <- getWord8

438+ return (AType (ATInt (ITVec (toEnum . fromIntegral $ e) (fromIntegral c))))

439+

440+ 21 -> fmap B8V get

441+ 22 -> fmap B16V get

442+ 23 -> fmap B32V get

443+ 24 -> fmap B64V get

427

444

428 _ -> error "Corrupted binary data for Const"

445 _ -> error "Corrupted binary data for Const"

429

446

@@ -1678,7 +1695,7 @@ instance Binary SSymbol where

1678 return (Binding x1)

1695 return (Binding x1)

1679 _ -> error "Corrupted binary data for SSymbol"

1696 _ -> error "Corrupted binary data for SSymbol"

1680

1697

1681−instance Binary Target where

1698+instance Binary Codegen where

1682 put x

1699 put x

1683 = case x of

1700 = case x of

1684 ViaC -> putWord8 0

1701 ViaC -> putWord8 0

@@ -1694,5 +1711,5 @@ instance Binary Target where

1694 2 -> return ViaNode

1711 2 -> return ViaNode

1695 3 -> return ViaJavaScript

1712 3 -> return ViaJavaScript

1696 4 -> return Bytecode

1713 4 -> return Bytecode

1697− _ -> error "Corrupted binary data for Target"

1714+ _ -> error "Corrupted binary data for Codegen"

1698

1715

src/Idris/Parser.hs+27−22

@@ -1139,16 +1139,20 @@ pIdiom syn

1139 return (PIdiom fc e)

1140

1141pConstant :: IParser Const

1142−pConstant = do reserved "Integer";return BIType

1142+pConstant = do reserved "Integer";return (AType (ATInt ITBig))

1143− <|> do reserved "Int"; return IType

1143+ <|> do reserved "Int"; return (AType (ATInt ITNative))

1144 <|> do reserved "Char"; return ChType

1145− <|> do reserved "Float"; return FlType

1145+ <|> do reserved "Float"; return (AType ATFloat)

1146 <|> do reserved "String"; return StrType

1147 <|> do reserved "Ptr"; return PtrType

1148− <|> do reserved "Bits8"; return B8Type

1148+ <|> do reserved "Bits8"; return (AType (ATInt (ITFixed IT8)))

1149− <|> do reserved "Bits16"; return B16Type

1149+ <|> do reserved "Bits16"; return (AType (ATInt (ITFixed IT16)))

1150− <|> do reserved "Bits32"; return B32Type

1150+ <|> do reserved "Bits32"; return (AType (ATInt (ITFixed IT32)))

1151− <|> do reserved "Bits64"; return B64Type

1151+ <|> do reserved "Bits64"; return (AType (ATInt (ITFixed IT64)))

1152+ <|> do reserved "Bits8x16"; return (AType (ATInt (ITVec IT8 16)))

1153+ <|> do reserved "Bits16x8"; return (AType (ATInt (ITVec IT16 8)))

1154+ <|> do reserved "Bits32x4"; return (AType (ATInt (ITVec IT32 4)))

1155+ <|> do reserved "Bits64x2"; return (AType (ATInt (ITVec IT64 2)))

1152 <|> try (do f <- float; return $ Fl f)

1156 <|> try (do f <- float; return $ Fl f)

1153 <|> try (do i <- natural; return $ BI i)

1157 <|> try (do i <- natural; return $ BI i)

1154 <|> try (do s <- strlit; return $ Str s)

1158 <|> try (do s <- strlit; return $ Str s)

@@ -1535,25 +1539,26 @@ pWhereblock n syn

1535 closeBlock

1539 closeBlock

1536 return (concat ds, map (\x -> (x, decoration syn x)) dns)

1540 return (concat ds, map (\x -> (x, decoration syn x)) dns)

1537

1541

1538−pTarget :: IParser Target

1542+pCodegen :: IParser Codegen

1539−pTarget = try (do reserved "C"; return ViaC)

1543+pCodegen = try (do reserved "C"; return ViaC)

1540− <|> try (do reserved "Java"; return ViaJava)

1544+ <|> try (do reserved "Java"; return ViaJava)

1541− <|> try (do reserved "JavaScript"; return ViaJavaScript)

1545+ <|> try (do reserved "JavaScript"; return ViaJavaScript)

1542− <|> try (do reserved "Node"; return ViaNode)

1546+ <|> try (do reserved "Node"; return ViaNode)

1547+ <|> try (do reserved "LLVM"; return ViaLLVM)

1543− <|> try (do reserved "Bytecode"; return Bytecode)

1548+ <|> try (do reserved "Bytecode"; return Bytecode)

1544

1549

1545pDirective :: SyntaxInfo -> IParser [PDecl]

1550pDirective :: SyntaxInfo -> IParser [PDecl]

1546−pDirective syn = try (do lchar '%'; reserved "lib"; tgt <- pTarget; lib <- strlit;

1551+pDirective syn = try (do lchar '%'; reserved "lib"; cgn <- pCodegen; lib <- strlit;

1547− return [PDirective (do addLib tgt lib

1552+ return [PDirective (do addLib cgn lib

1548− addIBC (IBCLib tgt lib))])

1553+ addIBC (IBCLib cgn lib))])

1549− <|> try (do lchar '%'; reserved "link"; tgt <- pTarget; obj <- strlit;

1554+ <|> try (do lchar '%'; reserved "link"; cgn <- pCodegen; obj <- strlit;

1550 return [PDirective (do datadir <- liftIO getDataDir

1555 return [PDirective (do datadir <- liftIO getDataDir

1551 o <- liftIO $ findInPath [".", datadir] obj

1556 o <- liftIO $ findInPath [".", datadir] obj

1552− addIBC (IBCObj tgt o)

1557+ addIBC (IBCObj cgn o)

1553− addObjectFile tgt o)])

1558+ addObjectFile cgn o)])

1554− <|> try (do lchar '%'; reserved "include"; tgt <- pTarget; hdr <- strlit;

1559+ <|> try (do lchar '%'; reserved "include"; cgn <- pCodegen; hdr <- strlit;

1555− return [PDirective (do addHdr tgt hdr

1560+ return [PDirective (do addHdr cgn hdr

1556− addIBC (IBCHeader tgt hdr))])

1561+ addIBC (IBCHeader cgn hdr))])

1557 <|> try (do lchar '%'; reserved "hide"; n <- iName []

1562 <|> try (do lchar '%'; reserved "hide"; n <- iName []

1558 return [PDirective (do setAccessibility n Hidden

1563 return [PDirective (do setAccessibility n Hidden

1559 addIBC (IBCAccess n Hidden))])

1564 addIBC (IBCAccess n Hidden))])

src/Idris/Primitives.hs+300−193

@@ -11,6 +11,7 @@ import Core.Evaluate

11import Data.Bits

12import Data.Word

13import Data.Int

14+import qualified Data.Vector.Unboxed as V

15data Prim = Prim { p_name :: Name,

16data Prim = Prim { p_name :: Name,

16 p_type :: Type,

17 p_type :: Type,

@@ -31,130 +32,130 @@ partial = Partial NotCovering

31primitives :: [Prim]

32primitives :: [Prim]

32primitives =

33primitives =

33 -- operators

34 -- operators

34− [Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))

35+ [Prim (UN "prim__eqChar") (ty [ChType, ChType] (AType (ATInt ITNative))) 2 (bcBin (==))

35− (2, LEq ITNative) total,

36+ (2, LEq (ATInt ITNative)) total,

36− Prim (UN "prim__ltChar") (ty [ChType, ChType] IType) 2 (bcBin (<))

37+ Prim (UN "prim__ltChar") (ty [ChType, ChType] (AType (ATInt ITNative))) 2 (bcBin (<))

37− (2, LLt ITNative) total,

38+ (2, LLt (ATInt ITNative)) total,

38− Prim (UN "prim__lteChar") (ty [ChType, ChType] IType) 2 (bcBin (<=))

39+ Prim (UN "prim__lteChar") (ty [ChType, ChType] (AType (ATInt ITNative))) 2 (bcBin (<=))

39− (2, LLe ITNative) total,

40+ (2, LLe (ATInt ITNative)) total,

40− Prim (UN "prim__gtChar") (ty [ChType, ChType] IType) 2 (bcBin (>))

41+ Prim (UN "prim__gtChar") (ty [ChType, ChType] (AType (ATInt ITNative))) 2 (bcBin (>))

41− (2, LGt ITNative) total,

42+ (2, LGt (ATInt ITNative)) total,

42− Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))

43+ Prim (UN "prim__gteChar") (ty [ChType, ChType] (AType (ATInt ITNative))) 2 (bcBin (>=))

43− (2, LGe ITNative) total,

44+ (2, LGe (ATInt ITNative)) total,

44−

45+

45− iCoerce IT8 IT16 "zext" zext LZExt,

46+ iCoerce (ITFixed IT8) (ITFixed IT16) "zext" zext LZExt,

46− iCoerce IT8 IT32 "zext" zext LZExt,

47+ iCoerce (ITFixed IT8) (ITFixed IT32) "zext" zext LZExt,

47− iCoerce IT8 IT64 "zext" zext LZExt,

48+ iCoerce (ITFixed IT8) (ITFixed IT64) "zext" zext LZExt,

48− iCoerce IT8 ITBig "zext" zext LZExt,

49+ iCoerce (ITFixed IT8) ITBig "zext" zext LZExt,

49− iCoerce IT8 ITNative "zext" zext LZExt,

50+ iCoerce (ITFixed IT8) ITNative "zext" zext LZExt,

50− iCoerce IT16 IT32 "zext" zext LZExt,

51+ iCoerce (ITFixed IT16) (ITFixed IT32) "zext" zext LZExt,

51− iCoerce IT16 IT64 "zext" zext LZExt,

52+ iCoerce (ITFixed IT16) (ITFixed IT64) "zext" zext LZExt,

52− iCoerce IT16 ITBig "zext" zext LZExt,

53+ iCoerce (ITFixed IT16) ITBig "zext" zext LZExt,

53− iCoerce IT16 ITNative "zext" zext LZExt,

54+ iCoerce (ITFixed IT16) ITNative "zext" zext LZExt,

54− iCoerce IT32 IT64 "zext" zext LZExt,

55+ iCoerce (ITFixed IT32) (ITFixed IT64) "zext" zext LZExt,

55− iCoerce IT32 ITBig "zext" zext LZExt,

56+ iCoerce (ITFixed IT32) ITBig "zext" zext LZExt,

56− iCoerce IT32 ITNative "zext" zext LZExt,

57+ iCoerce (ITFixed IT32) ITNative "zext" zext LZExt,

57− iCoerce IT64 ITBig "zext" zext LZExt,

58+ iCoerce (ITFixed IT64) ITBig "zext" zext LZExt,

58 iCoerce ITNative ITBig "zext" zext LZExt,

59 iCoerce ITNative ITBig "zext" zext LZExt,

59− iCoerce ITNative IT64 "zext" zext LZExt,

60+ iCoerce ITNative (ITFixed IT64) "zext" zext LZExt,

60− iCoerce ITNative IT32 "zext" zext LZExt,

61+ iCoerce ITNative (ITFixed IT32) "zext" zext LZExt,

61− iCoerce ITNative IT16 "zext" zext LZExt,

62+ iCoerce ITNative (ITFixed IT16) "zext" zext LZExt,

62−

63+

63− iCoerce IT8 IT16 "sext" sext LSExt,

64+ iCoerce (ITFixed IT8) (ITFixed IT16) "sext" sext LSExt,

64− iCoerce IT8 IT32 "sext" sext LSExt,

65+ iCoerce (ITFixed IT8) (ITFixed IT32) "sext" sext LSExt,

65− iCoerce IT8 IT64 "sext" sext LSExt,

66+ iCoerce (ITFixed IT8) (ITFixed IT64) "sext" sext LSExt,

66− iCoerce IT8 ITBig "sext" sext LSExt,

67+ iCoerce (ITFixed IT8) ITBig "sext" sext LSExt,

67− iCoerce IT8 ITNative "sext" sext LSExt,

68+ iCoerce (ITFixed IT8) ITNative "sext" sext LSExt,

68− iCoerce IT16 IT32 "sext" sext LSExt,

69+ iCoerce (ITFixed IT16) (ITFixed IT32) "sext" sext LSExt,

69− iCoerce IT16 IT64 "sext" sext LSExt,

70+ iCoerce (ITFixed IT16) (ITFixed IT64) "sext" sext LSExt,

70− iCoerce IT16 ITBig "sext" sext LSExt,

71+ iCoerce (ITFixed IT16) ITBig "sext" sext LSExt,

71− iCoerce IT16 ITNative "sext" sext LSExt,

72+ iCoerce (ITFixed IT16) ITNative "sext" sext LSExt,

72− iCoerce IT32 IT64 "sext" sext LSExt,

73+ iCoerce (ITFixed IT32) (ITFixed IT64) "sext" sext LSExt,

73− iCoerce IT32 ITBig "sext" sext LSExt,

74+ iCoerce (ITFixed IT32) ITBig "sext" sext LSExt,

74− iCoerce IT32 ITNative "sext" sext LSExt,

75+ iCoerce (ITFixed IT32) ITNative "sext" sext LSExt,

75− iCoerce IT64 ITBig "sext" sext LSExt,

76+ iCoerce (ITFixed IT64) ITBig "sext" sext LSExt,

76 iCoerce ITNative ITBig "sext" sext LSExt,

77 iCoerce ITNative ITBig "sext" sext LSExt,

78 iCoerce ITNative ITBig "sext" sext LSExt,

78− iCoerce ITNative IT64 "sext" sext LSExt,

79+ iCoerce ITNative (ITFixed IT64) "sext" sext LSExt,

79− iCoerce ITNative IT32 "sext" sext LSExt,

80+ iCoerce ITNative (ITFixed IT32) "sext" sext LSExt,

80− iCoerce ITNative IT16 "sext" sext LSExt,

81+ iCoerce ITNative (ITFixed IT16) "sext" sext LSExt,

81−

82+

82− iCoerce IT16 IT8 "trunc" trunc LTrunc,

83+ iCoerce (ITFixed IT16) (ITFixed IT8) "trunc" trunc LTrunc,

83− iCoerce IT32 IT8 "trunc" trunc LTrunc,

84+ iCoerce (ITFixed IT32) (ITFixed IT8) "trunc" trunc LTrunc,

84− iCoerce IT64 IT8 "trunc" trunc LTrunc,

85+ iCoerce (ITFixed IT64) (ITFixed IT8) "trunc" trunc LTrunc,

85− iCoerce ITBig IT8 "trunc" trunc LTrunc,

86+ iCoerce ITBig (ITFixed IT8) "trunc" trunc LTrunc,

86− iCoerce ITNative IT8 "trunc" trunc LTrunc,

87+ iCoerce ITNative (ITFixed IT8) "trunc" trunc LTrunc,

87− iCoerce IT32 IT16 "trunc" trunc LTrunc,

88+ iCoerce (ITFixed IT32) (ITFixed IT16) "trunc" trunc LTrunc,

88− iCoerce IT64 IT16 "trunc" trunc LTrunc,

89+ iCoerce (ITFixed IT64) (ITFixed IT16) "trunc" trunc LTrunc,

89− iCoerce ITBig IT16 "trunc" trunc LTrunc,

90+ iCoerce ITBig (ITFixed IT16) "trunc" trunc LTrunc,

90− iCoerce ITNative IT16 "trunc" trunc LTrunc,

91+ iCoerce ITNative (ITFixed IT16) "trunc" trunc LTrunc,

91− iCoerce IT64 IT32 "trunc" trunc LTrunc,

92+ iCoerce (ITFixed IT64) (ITFixed IT32) "trunc" trunc LTrunc,

92− iCoerce ITBig IT32 "trunc" trunc LTrunc,

93+ iCoerce ITBig (ITFixed IT32) "trunc" trunc LTrunc,

93− iCoerce ITNative IT32 "trunc" trunc LTrunc,

94+ iCoerce ITNative (ITFixed IT32) "trunc" trunc LTrunc,

94− iCoerce ITBig IT64 "trunc" trunc LTrunc,

95+ iCoerce ITBig (ITFixed IT64) "trunc" trunc LTrunc,

95− iCoerce IT16 ITNative "trunc" trunc LTrunc,

96+ iCoerce (ITFixed IT16) ITNative "trunc" trunc LTrunc,

96− iCoerce IT32 ITNative "trunc" trunc LTrunc,

97+ iCoerce (ITFixed IT32) ITNative "trunc" trunc LTrunc,

97− iCoerce IT64 ITNative "trunc" trunc LTrunc,

98+ iCoerce (ITFixed IT64) ITNative "trunc" trunc LTrunc,

98 iCoerce ITBig ITNative "trunc" trunc LTrunc,

99 iCoerce ITBig ITNative "trunc" trunc LTrunc,

99− iCoerce ITNative IT64 "trunc" trunc LTrunc,

100+ iCoerce ITNative (ITFixed IT64) "trunc" trunc LTrunc,

100−

101+

101− Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+))

102+ Prim (UN "prim__addFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType ATFloat)) 2 (fBin (+))

102− (2, LFPlus) total,

103+ (2, LPlus ATFloat) total,

103− Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-))

104+ Prim (UN "prim__subFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType ATFloat)) 2 (fBin (-))

104− (2, LFMinus) total,

105+ (2, LMinus ATFloat) total,

105− Prim (UN "prim__mulFloat") (ty [FlType, FlType] FlType) 2 (fBin (*))

106+ Prim (UN "prim__mulFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType ATFloat)) 2 (fBin (*))

106− (2, LFTimes) total,

107+ (2, LTimes ATFloat) total,

107− Prim (UN "prim__divFloat") (ty [FlType, FlType] FlType) 2 (fBin (/))

108+ Prim (UN "prim__divFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType ATFloat)) 2 (fBin (/))

108− (2, LFDiv) total,

109+ (2, LSDiv ATFloat) total,

109− Prim (UN "prim__eqFloat") (ty [FlType, FlType] IType) 2 (bfBin (==))

110+ Prim (UN "prim__eqFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (==))

110− (2, LFEq) total,

111+ (2, LEq ATFloat) total,

111− Prim (UN "prim__ltFloat") (ty [FlType, FlType] IType) 2 (bfBin (<))

112+ Prim (UN "prim__ltFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (<))

112− (2, LFLt) total,

113+ (2, LLt ATFloat) total,

113− Prim (UN "prim__lteFloat") (ty [FlType, FlType] IType) 2 (bfBin (<=))

114+ Prim (UN "prim__lteFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (<=))

114− (2, LFLe) total,

115+ (2, LLe ATFloat) total,

115− Prim (UN "prim__gtFloat") (ty [FlType, FlType] IType) 2 (bfBin (>))

116+ Prim (UN "prim__gtFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (>))

116− (2, LFGt) total,

117+ (2, LGt ATFloat) total,

117− Prim (UN "prim__gteFloat") (ty [FlType, FlType] IType) 2 (bfBin (>=))

118+ Prim (UN "prim__gteFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType (ATInt ITNative))) 2 (bfBin (>=))

118− (2, LFGe) total,

119+ (2, LGe ATFloat) total,

119 Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))

120 Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))

120 (2, LStrConcat) total,

121 (2, LStrConcat) total,

121− Prim (UN "prim__eqString") (ty [StrType, StrType] IType) 2 (bsBin (==))

122+ Prim (UN "prim__eqString") (ty [StrType, StrType] (AType (ATInt ITNative))) 2 (bsBin (==))

122 (2, LStrEq) total,

123 (2, LStrEq) total,

123− Prim (UN "prim__ltString") (ty [StrType, StrType] IType) 2 (bsBin (<))

124+ Prim (UN "prim__ltString") (ty [StrType, StrType] (AType (ATInt ITNative))) 2 (bsBin (<))

124 (2, LStrLt) total,

125 (2, LStrLt) total,

125− Prim (UN "prim_lenString") (ty [StrType] IType) 1 (p_strLen)

126+ Prim (UN "prim_lenString") (ty [StrType] (AType (ATInt ITNative))) 1 (p_strLen)

126 (1, LStrLen) total,

127 (1, LStrLen) total,

127 -- Conversions

128 -- Conversions

128− Prim (UN "prim__charToInt") (ty [ChType] IType) 1 (c_charToInt)

129+ Prim (UN "prim__charToInt") (ty [ChType] (AType (ATInt ITNative))) 1 (c_charToInt)

129 (1, LChInt ITNative) total,

130 (1, LChInt ITNative) total,

130− Prim (UN "prim__intToChar") (ty [IType] ChType) 1 (c_intToChar)

131+ Prim (UN "prim__intToChar") (ty [(AType (ATInt ITNative))] ChType) 1 (c_intToChar)

131 (1, LIntCh ITNative) total,

132 (1, LIntCh ITNative) total,

132− Prim (UN "prim__strToFloat") (ty [StrType] FlType) 1 (c_strToFloat)

133+ Prim (UN "prim__strToFloat") (ty [StrType] (AType ATFloat)) 1 (c_strToFloat)

133 (1, LStrFloat) total,

134 (1, LStrFloat) total,

134− Prim (UN "prim__floatToStr") (ty [FlType] StrType) 1 (c_floatToStr)

135+ Prim (UN "prim__floatToStr") (ty [(AType ATFloat)] StrType) 1 (c_floatToStr)

135 (1, LFloatStr) total,

136 (1, LFloatStr) total,

136

137

137− Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)

138+ Prim (UN "prim__floatExp") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatExp)

138− (1, LFExp) total,

139+ (1, LFExp) total,

139− Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)

140+ Prim (UN "prim__floatLog") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatLog)

140 (1, LFLog) total,

141 (1, LFLog) total,

141− Prim (UN "prim__floatSin") (ty [FlType] FlType) 1 (p_floatSin)

142+ Prim (UN "prim__floatSin") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatSin)

142 (1, LFSin) total,

143 (1, LFSin) total,

143− Prim (UN "prim__floatCos") (ty [FlType] FlType) 1 (p_floatCos)

144+ Prim (UN "prim__floatCos") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatCos)

144 (1, LFCos) total,

145 (1, LFCos) total,

145− Prim (UN "prim__floatTan") (ty [FlType] FlType) 1 (p_floatTan)

146+ Prim (UN "prim__floatTan") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatTan)

146 (1, LFTan) total,

147 (1, LFTan) total,

147− Prim (UN "prim__floatASin") (ty [FlType] FlType) 1 (p_floatASin)

148+ Prim (UN "prim__floatASin") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatASin)

148 (1, LFASin) total,

149 (1, LFASin) total,

149− Prim (UN "prim__floatACos") (ty [FlType] FlType) 1 (p_floatACos)

150+ Prim (UN "prim__floatACos") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatACos)

150 (1, LFACos) total,

151 (1, LFACos) total,

151− Prim (UN "prim__floatATan") (ty [FlType] FlType) 1 (p_floatATan)

152+ Prim (UN "prim__floatATan") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatATan)

152 (1, LFATan) total,

153 (1, LFATan) total,

153− Prim (UN "prim__floatSqrt") (ty [FlType] FlType) 1 (p_floatSqrt)

154+ Prim (UN "prim__floatSqrt") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatSqrt)

154 (1, LFSqrt) total,

155 (1, LFSqrt) total,

155− Prim (UN "prim__floatFloor") (ty [FlType] FlType) 1 (p_floatFloor)

156+ Prim (UN "prim__floatFloor") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatFloor)

156 (1, LFFloor) total,

157 (1, LFFloor) total,

157− Prim (UN "prim__floatCeil") (ty [FlType] FlType) 1 (p_floatCeil)

158+ Prim (UN "prim__floatCeil") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatCeil)

158 (1, LFCeil) total,

159 (1, LFCeil) total,

159

160

160 Prim (UN "prim__strHead") (ty [StrType] ChType) 1 (p_strHead)

161 Prim (UN "prim__strHead") (ty [StrType] ChType) 1 (p_strHead)

@@ -163,7 +164,7 @@ primitives =

163 (1, LStrTail) partial,

164 (1, LStrTail) partial,

164 Prim (UN "prim__strCons") (ty [ChType, StrType] StrType) 2 (p_strCons)

165 Prim (UN "prim__strCons") (ty [ChType, StrType] StrType) 2 (p_strCons)

165 (2, LStrCons) total,

166 (2, LStrCons) total,

166− Prim (UN "prim__strIndex") (ty [StrType, IType] ChType) 2 (p_strIndex)

167+ Prim (UN "prim__strIndex") (ty [StrType, (AType (ATInt ITNative))] ChType) 2 (p_strIndex)

167 (2, LStrIndex) partial,

168 (2, LStrIndex) partial,

168 Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

169 Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

169 (1, LStrRev) total,

170 (1, LStrRev) total,

@@ -174,22 +175,30 @@ primitives =

174 -- Streams

175 -- Streams

175 Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)

176 Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)

176 (0, LStdIn) partial

177 (0, LStdIn) partial

177− ] ++ concatMap intOps [IT8, IT16, IT32, IT64, ITBig, ITNative]

178+ ] ++ concatMap intOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64, ITBig, ITNative]

179+ ++ concatMap vecOps [ITVec IT8 16, ITVec IT16 8, ITVec IT32 4, ITVec IT64 2]

178

180

179intOps :: IntTy -> [Prim]

181intOps :: IntTy -> [Prim]

180−intOps ity =

182+intOps ity = intCmps ity ++ intArith ity ++ intConv ity

183+

184+intCmps :: IntTy -> [Prim]

185+intCmps ity =

181− [ iCmp ity "lt" (bCmp ity (<)) LLt total

186+ [ iCmp ity "lt" False (bCmp ity (<)) (LLt . ATInt) total

182− , iCmp ity "lte" (bCmp ity (<=)) LLe total

187+ , iCmp ity "lte" False (bCmp ity (<=)) (LLe . ATInt) total

183− , iCmp ity "eq" (bCmp ity (==)) LEq total

188+ , iCmp ity "eq" False (bCmp ity (==)) (LEq . ATInt) total

184− , iCmp ity "gte" (bCmp ity (>=)) LGe total

189+ , iCmp ity "gte" False (bCmp ity (>=)) (LGe . ATInt) total

185− , iCmp ity "gt" (bCmp ity (>)) LGt total

190+ , iCmp ity "gt" False (bCmp ity (>)) (LGt . ATInt) total

191+ ]

192+

193+intArith :: IntTy -> [Prim]

194+intArith ity =

186− , iBinOp ity "add" (bitBin ity (+)) LPlus total

195+ [ iBinOp ity "add" (bitBin ity (+)) (LPlus . ATInt) total

187− , iBinOp ity "sub" (bitBin ity (-)) LMinus total

196+ , iBinOp ity "sub" (bitBin ity (-)) (LMinus . ATInt) total

188− , iBinOp ity "mul" (bitBin ity (*)) LTimes total

197+ , iBinOp ity "mul" (bitBin ity (*)) (LTimes . ATInt) total

189 , iBinOp ity "udiv" (bitBin ity div) LUDiv partial

198 , iBinOp ity "udiv" (bitBin ity div) LUDiv partial

190− , iBinOp ity "sdiv" (bsdiv ity) LSDiv partial

199+ , iBinOp ity "sdiv" (bsdiv ity) (LSDiv . ATInt) partial

191 , iBinOp ity "urem" (bitBin ity rem) LURem partial

200 , iBinOp ity "urem" (bitBin ity rem) LURem partial

192− , iBinOp ity "srem" (bsrem ity) LSRem partial

201+ , iBinOp ity "srem" (bsrem ity) (LSRem . ATInt) partial

193 , iBinOp ity "shl" (bitBin ity (\x y -> shiftL x (fromIntegral y))) LSHL total

202 , iBinOp ity "shl" (bitBin ity (\x y -> shiftL x (fromIntegral y))) LSHL total

194 , iBinOp ity "lshr" (bitBin ity (\x y -> shiftR x (fromIntegral y))) LLSHR total

203 , iBinOp ity "lshr" (bitBin ity (\x y -> shiftR x (fromIntegral y))) LLSHR total

195 , iBinOp ity "ashr" (bashr ity) LASHR total

204 , iBinOp ity "ashr" (bashr ity) LASHR total

@@ -197,52 +206,98 @@ intOps ity =

197 , iBinOp ity "or" (bitBin ity (.|.)) LOr total

206 , iBinOp ity "or" (bitBin ity (.|.)) LOr total

198 , iBinOp ity "xor" (bitBin ity (xor)) LXOr total

207 , iBinOp ity "xor" (bitBin ity (xor)) LXOr total

199 , iUnOp ity "compl" (bUn ity complement) LCompl total

208 , iUnOp ity "compl" (bUn ity complement) LCompl total

209+ ]

210+

211+intConv :: IntTy -> [Prim]

212+intConv ity =

200− , Prim (UN $ "prim__toStr" ++ intTyName ity) (ty [intTyToConst ity] StrType) 1 intToStr

213+ [ Prim (UN $ "prim__toStr" ++ intTyName ity) (ty [AType . ATInt $ ity] StrType) 1 intToStr

201 (1, LIntStr ity) total

214 (1, LIntStr ity) total

202− , Prim (UN $ "prim__fromStr" ++ intTyName ity) (ty [StrType] (intTyToConst ity)) 1 (strToInt ity)

215+ , Prim (UN $ "prim__fromStr" ++ intTyName ity) (ty [StrType] (AType . ATInt $ ity)) 1 (strToInt ity)

203 (1, LStrInt ity) total

216 (1, LStrInt ity) total

204− , Prim (UN $ "prim__toFloat" ++ intTyName ity) (ty [intTyToConst ity] FlType) 1 intToFloat

217+ , Prim (UN $ "prim__toFloat" ++ intTyName ity) (ty [AType . ATInt $ ity] (AType ATFloat)) 1 intToFloat

205 (1, LIntFloat ity) total

218 (1, LIntFloat ity) total

206− , Prim (UN $ "prim__fromFloat" ++ intTyName ity) (ty [FlType] (intTyToConst ity)) 1 (floatToInt ity)

219+ , Prim (UN $ "prim__fromFloat" ++ intTyName ity) (ty [AType ATFloat] (AType . ATInt $ ity)) 1 (floatToInt ity)

207 (1, LFloatInt ity) total

220 (1, LFloatInt ity) total

208 ]

221 ]

209

222

223+vecCmps :: IntTy -> [Prim]

224+vecCmps ity =

225+ [ iCmp ity "lt" True (bCmp ity (<)) (LLt . ATInt) total

226+ , iCmp ity "lte" True (bCmp ity (<=)) (LLe . ATInt) total

227+ , iCmp ity "eq" True (bCmp ity (==)) (LEq . ATInt) total

228+ , iCmp ity "gte" True (bCmp ity (>=)) (LGe . ATInt) total

229+ , iCmp ity "gt" True (bCmp ity (>)) (LGt . ATInt) total

230+ ]

231+

232+vecOps :: IntTy -> [Prim]

233+vecOps ity@(ITVec elem count) =

234+ [ Prim (UN $ "prim__mk" ++ intTyName ity)

235+ (ty (replicate count . AType . ATInt . ITFixed $ elem) (AType . ATInt $ ity))

236+ count (mkVecCon elem count) (count, LMkVec elem count) total

237+ , Prim (UN $ "prim__index" ++ intTyName ity)

238+ (ty [AType . ATInt $ ity, AType (ATInt (ITFixed IT32))] (AType . ATInt . ITFixed $ elem))

239+ 2 (mkVecIndex count) (2, LIdxVec elem count) partial -- TODO: Ensure this reduces

240+ , Prim (UN $ "prim__update" ++ intTyName ity)

241+ (ty [AType . ATInt $ ity, AType (ATInt (ITFixed IT32)), AType . ATInt . ITFixed $ elem]

242+ (AType . ATInt $ ity))

243+ 3 (mkVecUpdate elem count) (3, LUpdateVec elem count) partial -- TODO: Ensure this reduces

244+ ] ++ intArith ity ++ vecCmps ity

245+

246+mkVecCon :: NativeTy -> Int -> [Const] -> Maybe Const

247+mkVecCon ity count args

248+ | length ints == count = Just (mkVec ity count ints)

249+ | otherwise = Nothing

250+ where

251+ ints = getInt args

252+ mkVec :: NativeTy -> Int -> [Integer] -> Const

253+ mkVec IT8 len values = B8V $ V.generate len (fromInteger . (values !!))

254+ mkVec IT16 len values = B16V $ V.generate len (fromInteger . (values !!))

255+ mkVec IT32 len values = B32V $ V.generate len (fromInteger . (values !!))

256+ mkVec IT64 len values = B64V $ V.generate len (fromInteger . (values !!))

257+

258+mkVecIndex count [vec, B32 i] = Just (idxVec vec)

259+ where

260+ idxVec :: Const -> Const

261+ idxVec (B8V v) = B8 $ V.unsafeIndex v (fromIntegral i)

262+ idxVec (B16V v) = B16 $ V.unsafeIndex v (fromIntegral i)

263+ idxVec (B32V v) = B32 $ V.unsafeIndex v (fromIntegral i)

264+ idxVec (B64V v) = B64 $ V.unsafeIndex v (fromIntegral i)

265+mkVecIndex _ _ = Nothing

266+

267+mkVecUpdate ity count [vec, B32 i, newElem] = updateVec vec newElem

268+ where

269+ updateVec :: Const -> Const -> Maybe Const

270+ updateVec (B8V v) (B8 e) = Just . B8V $ V.unsafeUpdate v (V.singleton (fromIntegral i, e))

271+ updateVec (B16V v) (B16 e) = Just . B16V $ V.unsafeUpdate v (V.singleton (fromIntegral i, e))

272+ updateVec (B32V v) (B32 e) = Just . B32V $ V.unsafeUpdate v (V.singleton (fromIntegral i, e))

273+ updateVec (B64V v) (B64 e) = Just . B64V $ V.unsafeUpdate v (V.singleton (fromIntegral i, e))

274+

210intTyName :: IntTy -> String

275intTyName :: IntTy -> String

211intTyName ITNative = "Int"

276intTyName ITNative = "Int"

212intTyName ITBig = "BigInt"

277intTyName ITBig = "BigInt"

213−intTyName sized = "B" ++ show (intTyWidth sized)

278+intTyName (ITFixed sized) = "B" ++ show (nativeTyWidth sized)

214−

279+intTyName (ITVec ity count) = "B" ++ show (nativeTyWidth ity) ++ "x" ++ show count

280+

215−iCmp, iBinOp, iUnOp :: IntTy -> String -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim

281+iCmp :: IntTy -> String -> Bool -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim

282+iCmp ity op self impl irop totality

216−iCmp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) IType) 2 impl (2, irop ity) totality

283+ = Prim (UN $ "prim__" ++ op ++ intTyName ity)

217−iBinOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) (intTyToConst ity)) 2 impl (2, irop ity) totality

284+ (ty (replicate 2 . AType . ATInt $ ity) (AType (ATInt (if self then ity else ITNative))))

218−iUnOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty [intTyToConst ity] (intTyToConst ity)) 1 impl (1, irop ity) totality

285+ 2 impl (2, irop ity) totality

286+

287+iBinOp, iUnOp :: IntTy -> String -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim

288+iBinOp ity op impl irop totality

289+ = Prim (UN $ "prim__" ++ op ++ intTyName ity)

290+ (ty (replicate 2 . AType . ATInt $ ity) (AType . ATInt $ ity))

291+ 2 impl (2, irop ity) totality

292+iUnOp ity op impl irop totality

293+ = Prim (UN $ "prim__" ++ op ++ intTyName ity)

294+ (ty [AType . ATInt $ ity] (AType . ATInt $ ity))

295+ 1 impl (1, irop ity) totality

219

296

220iCoerce :: IntTy -> IntTy -> String -> (IntTy -> IntTy -> [Const] -> Maybe Const) -> (IntTy -> IntTy -> PrimFn) -> Prim

297iCoerce :: IntTy -> IntTy -> String -> (IntTy -> IntTy -> [Const] -> Maybe Const) -> (IntTy -> IntTy -> PrimFn) -> Prim

221iCoerce from to op impl irop =

298iCoerce from to op impl irop =

222 Prim (UN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)

299 Prim (UN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)

223− (ty [intTyToConst from] (intTyToConst to)) 1 (impl from to) (1, irop from to) total

300+ (ty [AType . ATInt $ from] (AType . ATInt $ to)) 1 (impl from to) (1, irop from to) total

224−

225−iUn :: (Int -> Int) -> [Const] -> Maybe Const

226−iUn op [I x] = Just $ I (op x)

227−iUn _ _ = Nothing

228−

229−iBin :: (Int -> Int -> Int) -> [Const] -> Maybe Const

230−iBin op [I x, I y] = Just $ I (op x y)

231−iBin _ _ = Nothing

232−

233−bBin :: (Integer -> Integer -> Integer) -> [Const] -> Maybe Const

234−bBin op [BI x, BI y] = Just $ BI (op x y)

235−bBin _ _ = Nothing

236−

237−bBini :: (Integer -> Integer -> Int) -> [Const] -> Maybe Const

238−bBini op [BI x, BI y] = Just $ I (op x y)

239−bBini _ _ = Nothing

240−

241−biBin :: (Int -> Int -> Bool) -> [Const] -> Maybe Const

242−biBin op = iBin (\x y -> if (op x y) then 1 else 0)

243−

244−bbBin :: (Integer -> Integer -> Bool) -> [Const] -> Maybe Const

245−bbBin op = bBini (\x y -> if (op x y) then 1 else 0)

246

301

247fBin :: (Double -> Double -> Double) -> [Const] -> Maybe Const

302fBin :: (Double -> Double -> Double) -> [Const] -> Maybe Const

248fBin op [Fl x, Fl y] = Just $ Fl (op x y)

303fBin op [Fl x, Fl y] = Just $ Fl (op x y)

@@ -269,81 +324,133 @@ sBin op [Str x, Str y] = Just $ Str (op x y)

269sBin _ _ = Nothing

324sBin _ _ = Nothing

270

325

271bsrem :: IntTy -> [Const] -> Maybe Const

326bsrem :: IntTy -> [Const] -> Maybe Const

272−bsrem IT8 [B8 x, B8 y]

327+bsrem (ITFixed IT8) [B8 x, B8 y]

273 = Just $ B8 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8))

328 = Just $ B8 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8))

274−bsrem IT16 [B16 x, B16 y]

329+bsrem (ITFixed IT16) [B16 x, B16 y]

275 = Just $ B16 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int16))

330 = Just $ B16 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int16))

276−bsrem IT32 [B32 x, B32 y]

331+bsrem (ITFixed IT32) [B32 x, B32 y]

277 = Just $ B32 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int32))

332 = Just $ B32 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int32))

278−bsrem IT64 [B64 x, B64 y]

333+bsrem (ITFixed IT64) [B64 x, B64 y]

279 = Just $ B64 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int64))

334 = Just $ B64 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int64))

280bsrem ITNative [I x, I y] = Just $ I (x `rem` y)

335bsrem ITNative [I x, I y] = Just $ I (x `rem` y)

336+bsrem (ITVec IT8 _) [B8V x, B8V y]

337+ = Just . B8V $

338+ V.zipWith (\n d -> (fromIntegral (fromIntegral n `rem` fromIntegral d :: Int8))) x y

339+bsrem (ITVec IT16 _) [B16V x, B16V y]

340+ = Just . B16V $

341+ V.zipWith (\n d -> (fromIntegral (fromIntegral n `rem` fromIntegral d :: Int16))) x y

342+bsrem (ITVec IT32 _) [B32V x, B32V y]

343+ = Just . B32V $

344+ V.zipWith (\n d -> (fromIntegral (fromIntegral n `rem` fromIntegral d :: Int64))) x y

345+bsrem (ITVec IT64 _) [B64V x, B64V y]

346+ = Just . B64V $

347+ V.zipWith (\n d -> (fromIntegral (fromIntegral n `rem` fromIntegral d :: Int64))) x y

281bsrem _ _ = Nothing

348bsrem _ _ = Nothing

282

349

283bsdiv :: IntTy -> [Const] -> Maybe Const

350bsdiv :: IntTy -> [Const] -> Maybe Const

284−bsdiv IT8 [B8 x, B8 y]

351+bsdiv (ITFixed IT8) [B8 x, B8 y]

285 = Just $ B8 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int8))

352 = Just $ B8 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int8))

286−bsdiv IT16 [B16 x, B16 y]

353+bsdiv (ITFixed IT16) [B16 x, B16 y]

287 = Just $ B16 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int16))

354 = Just $ B16 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int16))

288−bsdiv IT32 [B32 x, B32 y]

355+bsdiv (ITFixed IT32) [B32 x, B32 y]

289 = Just $ B32 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int32))

356 = Just $ B32 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int32))

290−bsdiv IT64 [B64 x, B64 y]

357+bsdiv (ITFixed IT64) [B64 x, B64 y]

291 = Just $ B64 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int64))

358 = Just $ B64 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int64))

292bsdiv ITNative [I x, I y] = Just $ I (x `div` y)

359bsdiv ITNative [I x, I y] = Just $ I (x `div` y)

360+bsdiv (ITVec IT8 _) [B8V x, B8V y]

361+ = Just . B8V $

362+ V.zipWith (\n d -> (fromIntegral (fromIntegral n `div` fromIntegral d :: Int8))) x y

363+bsdiv (ITVec IT16 _) [B16V x, B16V y]

364+ = Just . B16V $

365+ V.zipWith (\n d -> (fromIntegral (fromIntegral n `div` fromIntegral d :: Int16))) x y

366+bsdiv (ITVec IT32 _) [B32V x, B32V y]

367+ = Just . B32V $

368+ V.zipWith (\n d -> (fromIntegral (fromIntegral n `div` fromIntegral d :: Int64))) x y

369+bsdiv (ITVec IT64 _) [B64V x, B64V y]

370+ = Just . B64V $

371+ V.zipWith (\n d -> (fromIntegral (fromIntegral n `div` fromIntegral d :: Int64))) x y

293bsdiv _ _ = Nothing

372bsdiv _ _ = Nothing

294

373

295bashr :: IntTy -> [Const] -> Maybe Const

374bashr :: IntTy -> [Const] -> Maybe Const

296−bashr IT8 [B8 x, B8 y]

375+bashr (ITFixed IT8) [B8 x, B8 y]

297 = Just $ B8 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int8))

376 = Just $ B8 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int8))

298−bashr IT16 [B16 x, B16 y]

377+bashr (ITFixed IT16) [B16 x, B16 y]

299 = Just $ B16 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int16))

378 = Just $ B16 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int16))

300−bashr IT32 [B32 x, B32 y]

379+bashr (ITFixed IT32) [B32 x, B32 y]

301 = Just $ B32 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int32))

380 = Just $ B32 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int32))

302−bashr IT64 [B64 x, B64 y]

381+bashr (ITFixed IT64) [B64 x, B64 y]

303 = Just $ B64 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int64))

382 = Just $ B64 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int64))

304bashr ITNative [I x, I y] = Just $ I (x `shiftR` y)

383bashr ITNative [I x, I y] = Just $ I (x `shiftR` y)

384+bashr (ITVec IT8 _) [B8V x, B8V y]

385+ = Just . B8V $

386+ V.zipWith (\n d -> (fromIntegral (fromIntegral n `shiftR` fromIntegral d :: Int8))) x y

387+bashr (ITVec IT16 _) [B16V x, B16V y]

388+ = Just . B16V $

389+ V.zipWith (\n d -> (fromIntegral (fromIntegral n `shiftR` fromIntegral d :: Int16))) x y

390+bashr (ITVec IT32 _) [B32V x, B32V y]

391+ = Just . B32V $

392+ V.zipWith (\n d -> (fromIntegral (fromIntegral n `shiftR` fromIntegral d :: Int64))) x y

393+bashr (ITVec IT64 _) [B64V x, B64V y]

394+ = Just . B64V $

395+ V.zipWith (\n d -> (fromIntegral (fromIntegral n `shiftR` fromIntegral d :: Int64))) x y

305bashr _ _ = Nothing

396bashr _ _ = Nothing

306

397

307bUn :: IntTy -> (forall a. Bits a => a -> a) -> [Const] -> Maybe Const

398bUn :: IntTy -> (forall a. Bits a => a -> a) -> [Const] -> Maybe Const

308−bUn IT8 op [B8 x] = Just $ B8 (op x)

399+bUn (ITFixed IT8) op [B8 x] = Just $ B8 (op x)

309−bUn IT16 op [B16 x] = Just $ B16 (op x)

400+bUn (ITFixed IT16) op [B16 x] = Just $ B16 (op x)

310−bUn IT32 op [B32 x] = Just $ B32 (op x)

401+bUn (ITFixed IT32) op [B32 x] = Just $ B32 (op x)

311−bUn IT64 op [B64 x] = Just $ B64 (op x)

402+bUn (ITFixed IT64) op [B64 x] = Just $ B64 (op x)

312bUn ITBig op [BI x] = Just $ BI (op x)

403bUn ITBig op [BI x] = Just $ BI (op x)

313bUn ITNative op [I x] = Just $ I (op x)

404bUn ITNative op [I x] = Just $ I (op x)

405+bUn (ITVec IT8 _) op [B8V x] = Just . B8V $ V.map op x

406+bUn (ITVec IT16 _) op [B16V x] = Just . B16V $ V.map op x

407+bUn (ITVec IT32 _) op [B32V x] = Just . B32V $ V.map op x

408+bUn (ITVec IT64 _) op [B64V x] = Just . B64V $ V.map op x

314bUn _ _ _ = Nothing

409bUn _ _ _ = Nothing

315

410

316bitBin :: IntTy -> (forall a. (Bits a, Integral a) => a -> a -> a) -> [Const] -> Maybe Const

411bitBin :: IntTy -> (forall a. (Bits a, Integral a) => a -> a -> a) -> [Const] -> Maybe Const

317−bitBin IT8 op [B8 x, B8 y] = Just $ B8 (op x y)

412+bitBin (ITFixed IT8) op [B8 x, B8 y] = Just $ B8 (op x y)

318−bitBin IT16 op [B16 x, B16 y] = Just $ B16 (op x y)

413+bitBin (ITFixed IT16) op [B16 x, B16 y] = Just $ B16 (op x y)

319−bitBin IT32 op [B32 x, B32 y] = Just $ B32 (op x y)

414+bitBin (ITFixed IT32) op [B32 x, B32 y] = Just $ B32 (op x y)

320−bitBin IT64 op [B64 x, B64 y] = Just $ B64 (op x y)

415+bitBin (ITFixed IT64) op [B64 x, B64 y] = Just $ B64 (op x y)

321bitBin ITBig op [BI x, BI y] = Just $ BI (op x y)

416bitBin ITBig op [BI x, BI y] = Just $ BI (op x y)

322bitBin ITNative op [I x, I y] = Just $ I (op x y)

417bitBin ITNative op [I x, I y] = Just $ I (op x y)

418+bitBin (ITVec IT8 _) op [B8V x, B8V y] = Just . B8V $ V.zipWith op x y

419+bitBin (ITVec IT16 _) op [B16V x, B16V y] = Just . B16V $ V.zipWith op x y

420+bitBin (ITVec IT32 _) op [B32V x, B32V y] = Just . B32V $ V.zipWith op x y

421+bitBin (ITVec IT64 _) op [B64V x, B64V y] = Just . B64V $ V.zipWith op x y

323bitBin _ _ _ = Nothing

422bitBin _ _ _ = Nothing

324

423

325bCmp :: IntTy -> (forall a. Ord a => a -> a -> Bool) -> [Const] -> Maybe Const

424bCmp :: IntTy -> (forall a. Ord a => a -> a -> Bool) -> [Const] -> Maybe Const

326−bCmp IT8 op [B8 x, B8 y] = Just $ I (if (op x y) then 1 else 0)

425+bCmp (ITFixed IT8) op [B8 x, B8 y] = Just $ I (if (op x y) then 1 else 0)

327−bCmp IT16 op [B16 x, B16 y] = Just $ I (if (op x y) then 1 else 0)

426+bCmp (ITFixed IT16) op [B16 x, B16 y] = Just $ I (if (op x y) then 1 else 0)

328−bCmp IT32 op [B32 x, B32 y] = Just $ I (if (op x y) then 1 else 0)

427+bCmp (ITFixed IT32) op [B32 x, B32 y] = Just $ I (if (op x y) then 1 else 0)

329−bCmp IT64 op [B64 x, B64 y] = Just $ I (if (op x y) then 1 else 0)

428+bCmp (ITFixed IT64) op [B64 x, B64 y] = Just $ I (if (op x y) then 1 else 0)

330bCmp ITBig op [BI x, BI y] = Just $ I (if (op x y) then 1 else 0)

429bCmp ITBig op [BI x, BI y] = Just $ I (if (op x y) then 1 else 0)

331bCmp ITNative op [I x, I y] = Just $ I (if (op x y) then 1 else 0)

430bCmp ITNative op [I x, I y] = Just $ I (if (op x y) then 1 else 0)

431+bCmp (ITVec IT8 _) op [B8V x, B8V y]

432+ = Just . B8V . V.map (\b -> if b then -1 else 0) $ V.zipWith op x y

433+bCmp (ITVec IT16 _) op [B16V x, B16V y]

434+ = Just . B16V . V.map (\b -> if b then -1 else 0) $ V.zipWith op x y

435+bCmp (ITVec IT32 _) op [B32V x, B32V y]

436+ = Just . B32V . V.map (\b -> if b then -1 else 0) $ V.zipWith op x y

437+bCmp (ITVec IT64 _) op [B64V x, B64V y]

438+ = Just . B64V . V.map (\b -> if b then -1 else 0) $ V.zipWith op x y

332bCmp _ _ _ = Nothing

439bCmp _ _ _ = Nothing

333

440

334toInt :: Integral a => IntTy -> a -> Const

441toInt :: Integral a => IntTy -> a -> Const

335−toInt IT8 x = B8 (fromIntegral x)

442+toInt (ITFixed IT8) x = B8 (fromIntegral x)

336−toInt IT16 x = B16 (fromIntegral x)

443+toInt (ITFixed IT16) x = B16 (fromIntegral x)

337−toInt IT32 x = B32 (fromIntegral x)

444+toInt (ITFixed IT32) x = B32 (fromIntegral x)

338−toInt IT64 x = B64 (fromIntegral x)

445+toInt (ITFixed IT64) x = B64 (fromIntegral x)

339toInt ITBig x = BI (fromIntegral x)

446toInt ITBig x = BI (fromIntegral x)

340toInt ITNative x = I (fromIntegral x)

447toInt ITNative x = I (fromIntegral x)

341

448

342intToInt :: IntTy -> IntTy -> [Const] -> Maybe Const

449intToInt :: IntTy -> IntTy -> [Const] -> Maybe Const

343−intToInt IT8 out [B8 x] = Just $ toInt out x

450+intToInt (ITFixed IT8) out [B8 x] = Just $ toInt out x

344−intToInt IT16 out [B16 x] = Just $ toInt out x

451+intToInt (ITFixed IT16) out [B16 x] = Just $ toInt out x

345−intToInt IT32 out [B32 x] = Just $ toInt out x

452+intToInt (ITFixed IT32) out [B32 x] = Just $ toInt out x

346−intToInt IT64 out [B64 x] = Just $ toInt out x

453+intToInt (ITFixed IT64) out [B64 x] = Just $ toInt out x

347intToInt ITBig out [BI x] = Just $ toInt out x

454intToInt ITBig out [BI x] = Just $ toInt out x

348intToInt ITNative out [I x] = Just $ toInt out x

455intToInt ITNative out [I x] = Just $ toInt out x

349intToInt _ _ _ = Nothing

456intToInt _ _ _ = Nothing

@@ -356,10 +463,10 @@ zext from to val

356zext _ _ _ = Nothing

463zext _ _ _ = Nothing

357

464

358sext :: IntTy -> IntTy -> [Const] -> Maybe Const

465sext :: IntTy -> IntTy -> [Const] -> Maybe Const

359−sext IT8 out [B8 x] = Just $ toInt out (fromIntegral x :: Int8)

466+sext (ITFixed IT8) out [B8 x] = Just $ toInt out (fromIntegral x :: Int8)

360−sext IT16 out [B16 x] = Just $ toInt out (fromIntegral x :: Int16)

467+sext (ITFixed IT16) out [B16 x] = Just $ toInt out (fromIntegral x :: Int16)

361−sext IT32 out [B32 x] = Just $ toInt out (fromIntegral x :: Int32)

468+sext (ITFixed IT32) out [B32 x] = Just $ toInt out (fromIntegral x :: Int32)

362−sext IT64 out [B64 x] = Just $ toInt out (fromIntegral x :: Int64)

469+sext (ITFixed IT64) out [B64 x] = Just $ toInt out (fromIntegral x :: Int64)

363sext ITBig _ _ = Nothing

470sext ITBig _ _ = Nothing

364sext from to val = intToInt from to val

471sext from to val = intToInt from to val

365

472

@@ -369,19 +476,19 @@ trunc _ ITBig _ = Nothing

369trunc from to val | intTyWidth from > intTyWidth to = intToInt from to val

476trunc from to val | intTyWidth from > intTyWidth to = intToInt from to val

370trunc _ _ _ = Nothing

477trunc _ _ _ = Nothing

371

478

372−getInt :: [Const] -> Maybe Integer

373−getInt [B8 x] = Just . toInteger $ x

374−getInt [B16 x] = Just . toInteger $ x

375−getInt [B32 x] = Just . toInteger $ x

376−getInt [B64 x] = Just . toInteger $ x

377−getInt [I x] = Just . toInteger $ x

378−getInt [BI x] = Just x

379−getInt _ = Nothing

380−

381intToStr :: [Const] -> Maybe Const

479intToStr :: [Const] -> Maybe Const

382−intToStr val | Just i <- getInt val = Just $ Str (show i)

480+intToStr val | [i] <- getInt val = Just $ Str (show i)

383intToStr _ = Nothing

481intToStr _ = Nothing

384

482

483+getInt :: [Const] -> [Integer]

484+getInt (B8 x : xs) = toInteger x : getInt xs

485+getInt (B16 x : xs) = toInteger x : getInt xs

486+getInt (B32 x : xs) = toInteger x : getInt xs

487+getInt (B64 x : xs) = toInteger x : getInt xs

488+getInt (I x : xs) = toInteger x : getInt xs

489+getInt (BI x : xs) = x : getInt xs

490+getInt _ = []

491+

385strToInt :: IntTy -> [Const] -> Maybe Const

492strToInt :: IntTy -> [Const] -> Maybe Const

386strToInt ity [Str x] = case reads x of

493strToInt ity [Str x] = case reads x of

387 [(n,"")] -> Just $ toInt ity (n :: Integer)

494 [(n,"")] -> Just $ toInt ity (n :: Integer)

@@ -389,7 +496,7 @@ strToInt ity [Str x] = case reads x of

389strToInt _ _ = Nothing

496strToInt _ _ = Nothing

390

497

391intToFloat :: [Const] -> Maybe Const

498intToFloat :: [Const] -> Maybe Const

392−intToFloat val | Just i <- getInt val = Just $ Fl (fromIntegral i)

499+intToFloat val | [i] <- getInt val = Just $ Fl (fromIntegral i)

393intToFloat _ = Nothing

500intToFloat _ = Nothing

394

501

395floatToInt :: IntTy -> [Const] -> Maybe Const

502floatToInt :: IntTy -> [Const] -> Maybe Const

src/Idris/REPL.hs+54−21

@@ -39,6 +39,8 @@ import IRTS.CodegenCommon

39-- import RTS.PreC

40-- import RTS.CodegenC

42+import LLVM.General.Target

43+

42import System.Console.Haskeline as H

44import System.Console.Haskeline as H

43import System.FilePath

45import System.FilePath

44import System.Exit

46import System.Exit

@@ -155,8 +157,8 @@ ideslaveProcess fn Execute = do process fn Execute

155 iResult ""

157 iResult ""

156ideslaveProcess fn (NewCompile f) = do process fn (NewCompile f)

158ideslaveProcess fn (NewCompile f) = do process fn (NewCompile f)

157 iResult ""

159 iResult ""

158−ideslaveProcess fn (Compile target f) = do process fn (Compile target f)

160+ideslaveProcess fn (Compile codegen f) = do process fn (Compile codegen f)

159− iResult ""

161+ iResult ""

160ideslaveProcess fn (LogLvl i) = do process fn (LogLvl i)

162ideslaveProcess fn (LogLvl i) = do process fn (LogLvl i)

161 iResult ""

163 iResult ""

162ideslaveProcess fn (Pattelab t) = process fn (Pattelab t)

164ideslaveProcess fn (Pattelab t) = process fn (Pattelab t)

@@ -465,7 +467,7 @@ process fn Execute = do (m, _) <- elabVal toplevel False

465-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))

467-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))

466 (tmpn, tmph) <- liftIO tempfile

468 (tmpn, tmph) <- liftIO tempfile

467 liftIO $ hClose tmph

469 liftIO $ hClose tmph

468− t <- target

470+ t <- codegen

469 compile t tmpn m

471 compile t tmpn m

470 liftIO $ system tmpn

472 liftIO $ system tmpn

471 return ()

473 return ()

@@ -476,11 +478,11 @@ process fn (NewCompile f)

476 [pexp $ PRef fc (NS (UN "main") ["Main"])])

478 [pexp $ PRef fc (NS (UN "main") ["Main"])])

477 compileEpic f m

479 compileEpic f m

478 where fc = FC "main" 0

480 where fc = FC "main" 0

479−process fn (Compile target f)

481+process fn (Compile codegen f)

480 = do (m, _) <- elabVal toplevel False

482 = do (m, _) <- elabVal toplevel False

481 (PApp fc (PRef fc (UN "run__IO"))

483 (PApp fc (PRef fc (UN "run__IO"))

482 [pexp $ PRef fc (NS (UN "main") ["Main"])])

484 [pexp $ PRef fc (NS (UN "main") ["Main"])])

483− compile target f m

485+ compile codegen f m

484 where fc = FC "main" 0

486 where fc = FC "main" 0

485process fn (LogLvl i) = setLogLevel i

487process fn (LogLvl i) = setLogLevel i

486-- Elaborate as if LHS of a pattern (debug command)

488-- Elaborate as if LHS of a pattern (debug command)

@@ -560,14 +562,14 @@ displayHelp = let vstr = showVersion version in

560 l ++ take (c1 - length l) (repeat ' ') ++

562 l ++ take (c1 - length l) (repeat ' ') ++

561 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"

563 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"

562

564

563−parseTarget :: String -> Target

565+parseCodegen :: String -> Codegen

564−parseTarget "C" = ViaC

566+parseCodegen "C" = ViaC

565−parseTarget "Java" = ViaJava

567+parseCodegen "Java" = ViaJava

566−parseTarget "bytecode" = Bytecode

568+parseCodegen "bytecode" = Bytecode

567−parseTarget "javascript" = ViaJavaScript

569+parseCodegen "javascript" = ViaJavaScript

568−parseTarget "node" = ViaNode

570+parseCodegen "node" = ViaNode

569−parseTarget "llvm" = ViaLLVM

571+parseCodegen "llvm" = ViaLLVM

570−parseTarget _ = error "unknown target" -- FIXME: partial function

572+parseCodegen _ = error "unknown codegen" -- FIXME: partial function

571

573

572parseArgs :: [String] -> [Opt]

574parseArgs :: [String] -> [Opt]

573parseArgs [] = []

575parseArgs [] = []

@@ -605,10 +607,17 @@ parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)

605parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)

607parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)

606parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)

608parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)

607parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)

609parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)

608−parseArgs ("--target":n:ns) = UseTarget (parseTarget n) : (parseArgs ns)

610+parseArgs ("--codegen":n:ns) = UseCodegen (parseCodegen n) : (parseArgs ns)

609parseArgs ["--exec"] = InterpretScript "Main.main" : []

611parseArgs ["--exec"] = InterpretScript "Main.main" : []

610parseArgs ("--exec":expr:ns) = InterpretScript expr : parseArgs ns

612parseArgs ("--exec":expr:ns) = InterpretScript expr : parseArgs ns

611parseArgs ("-XTypeProviders":ns) = Extension TypeProviders : (parseArgs ns)

613parseArgs ("-XTypeProviders":ns) = Extension TypeProviders : (parseArgs ns)

614+parseArgs ("-O3":ns) = OptLevel 3 : parseArgs ns

615+parseArgs ("-O2":ns) = OptLevel 2 : parseArgs ns

616+parseArgs ("-O1":ns) = OptLevel 1 : parseArgs ns

617+parseArgs ("-O0":ns) = OptLevel 0 : parseArgs ns

618+parseArgs ("-O":n:ns) = OptLevel (read n) : parseArgs ns

619+parseArgs ("--target":n:ns) = TargetTriple n : parseArgs ns

620+parseArgs ("--cpu":n:ns) = TargetCPU n : parseArgs ns

612parseArgs (n:ns) = Filename n : (parseArgs ns)

621parseArgs (n:ns) = Filename n : (parseArgs ns)

613

622

614helphead =

623helphead =

@@ -637,10 +646,19 @@ idrisMain opts =

637 let bcs = opt getBC opts

646 let bcs = opt getBC opts

638 let vm = opt getFOVM opts

647 let vm = opt getFOVM opts

639 let pkgdirs = opt getPkgDir opts

648 let pkgdirs = opt getPkgDir opts

649+ let optimize = case opt getOptLevel opts of

650+ [] -> 2

651+ xs -> last xs

652+ trpl <- case opt getTriple opts of

653+ [] -> liftIO $ getDefaultTargetTriple

654+ xs -> return (last xs)

655+ tcpu <- case opt getCPU opts of

656+ [] -> liftIO $ getHostCPUName

657+ xs -> return (last xs)

640 let outty = case opt getOutputTy opts of

658 let outty = case opt getOutputTy opts of

641 [] -> Executable

659 [] -> Executable

642 xs -> last xs

660 xs -> last xs

643− let tgt = case opt getTarget opts of

661+ let cgn = case opt getCodegen opts of

644 [] -> ViaC

662 [] -> ViaC

645 xs -> last xs

663 xs -> last xs

646 script <- case opt getExecScript opts of

664 script <- case opt getExecScript opts of

@@ -657,13 +675,16 @@ idrisMain opts =

657 setVerbose runrepl

675 setVerbose runrepl

658 setCmdLine opts

676 setCmdLine opts

659 setOutputTy outty

677 setOutputTy outty

660− setTarget tgt

678+ setCodegen cgn

679+ setTargetTriple trpl

680+ setTargetCPU tcpu

681+ setOptLevel optimize

661 when (Verbose `elem` opts) $ setVerbose True

682 when (Verbose `elem` opts) $ setVerbose True

662 mapM_ makeOption opts

683 mapM_ makeOption opts

663 -- if we have the --fovm flag, drop into the first order VM testing

684 -- if we have the --fovm flag, drop into the first order VM testing

664 case vm of

685 case vm of

665 [] -> return ()

686 [] -> return ()

666− xs -> liftIO $ mapM_ (fovm tgt outty) xs

687+ xs -> liftIO $ mapM_ (fovm cgn outty) xs

667 -- if we have the --bytecode flag, drop into the bytecode assembler

688 -- if we have the --bytecode flag, drop into the bytecode assembler

668 case bcs of

689 case bcs of

669 [] -> return ()

690 [] -> return ()

@@ -684,7 +705,7 @@ idrisMain opts =

684 ok <- noErrors

705 ok <- noErrors

685 when ok $ case output of

706 when ok $ case output of

686 [] -> return ()

707 [] -> return ()

687− (o:_) -> process "" (Compile tgt o)

708+ (o:_) -> process "" (Compile cgn o)

688 when ok $ case newoutput of

709 when ok $ case newoutput of

689 [] -> return ()

710 [] -> return ()

690 (o:_) -> process "" (NewCompile o)

711 (o:_) -> process "" (NewCompile o)

@@ -758,9 +779,9 @@ getPkgClean :: Opt -> Maybe String

758getPkgClean (PkgClean str) = Just str

779getPkgClean (PkgClean str) = Just str

759getPkgClean _ = Nothing

780getPkgClean _ = Nothing

760

781

761−getTarget :: Opt -> Maybe Target

782+getCodegen :: Opt -> Maybe Codegen

762−getTarget (UseTarget x) = Just x

783+getCodegen (UseCodegen x) = Just x

763−getTarget _ = Nothing

784+getCodegen _ = Nothing

764

785

765getExecScript :: Opt -> Maybe String

786getExecScript :: Opt -> Maybe String

766getExecScript (InterpretScript expr) = Just expr

787getExecScript (InterpretScript expr) = Just expr

@@ -774,6 +795,18 @@ getLanguageExt :: Opt -> Maybe LanguageExt

774getLanguageExt (Extension e) = Just e

795getLanguageExt (Extension e) = Just e

775getLanguageExt _ = Nothing

796getLanguageExt _ = Nothing

776

797

798+getTriple :: Opt -> Maybe String

799+getTriple (TargetTriple x) = Just x

800+getTriple _ = Nothing

801+

802+getCPU :: Opt -> Maybe String

803+getCPU (TargetCPU x) = Just x

804+getCPU _ = Nothing

805+

806+getOptLevel :: Opt -> Maybe Int

807+getOptLevel (OptLevel x) = Just x

808+getOptLevel _ = Nothing

809+

777opt :: (Opt -> Maybe a) -> [Opt] -> [a]

810opt :: (Opt -> Maybe a) -> [Opt] -> [a]

778opt = mapMaybe

811opt = mapMaybe

779

812

test/Makefile+49−49

@@ -2,57 +2,57 @@ test:

2 perl ./runtest.pl all

4test_java:

5− perl ./runtest.pl all --target Java

5+ perl ./runtest.pl all --codegen Java

7test_js:

8− @perl ./runtest.pl reg001 --target node

8+ @perl ./runtest.pl reg001 --codegen node

9− @perl ./runtest.pl reg002 --target node

9+ @perl ./runtest.pl reg002 --codegen node

10− @perl ./runtest.pl reg003 --target node

10+ @perl ./runtest.pl reg003 --codegen node

11− @perl ./runtest.pl reg004 --target node

11+ @perl ./runtest.pl reg004 --codegen node

12− @perl ./runtest.pl reg004 --target node

12+ @perl ./runtest.pl reg004 --codegen node

13− @perl ./runtest.pl reg005 --target node

13+ @perl ./runtest.pl reg005 --codegen node

14− @perl ./runtest.pl reg006 --target node

14+ @perl ./runtest.pl reg006 --codegen node

15− @perl ./runtest.pl reg007 --target node

15+ @perl ./runtest.pl reg007 --codegen node

16− @perl ./runtest.pl reg008 --target node

16+ @perl ./runtest.pl reg008 --codegen node

17− @perl ./runtest.pl reg009 --target node

17+ @perl ./runtest.pl reg009 --codegen node

18− @perl ./runtest.pl reg010 --target node

18+ @perl ./runtest.pl reg010 --codegen node

19− @perl ./runtest.pl reg011 --target node

19+ @perl ./runtest.pl reg011 --codegen node

20− @perl ./runtest.pl reg012 --target node

20+ @perl ./runtest.pl reg012 --codegen node

21− @perl ./runtest.pl reg013 --target node

21+ @perl ./runtest.pl reg013 --codegen node

22− @perl ./runtest.pl reg014 --target node

22+ @perl ./runtest.pl reg014 --codegen node

23− @perl ./runtest.pl reg015 --target node

23+ @perl ./runtest.pl reg015 --codegen node

24− @#perl ./runtest.pl reg016 --target node

24+ @#perl ./runtest.pl reg016 --codegen node

25− @perl ./runtest.pl reg017 --target node

25+ @perl ./runtest.pl reg017 --codegen node

26− @perl ./runtest.pl reg018 --target node

26+ @perl ./runtest.pl reg018 --codegen node

27− @perl ./runtest.pl reg019 --target node

27+ @perl ./runtest.pl reg019 --codegen node

28− @perl ./runtest.pl test001 --target node

28+ @perl ./runtest.pl test001 --codegen node

29− @perl ./runtest.pl test002 --target node

29+ @perl ./runtest.pl test002 --codegen node

30− @perl ./runtest.pl test003 --target node

30+ @perl ./runtest.pl test003 --codegen node

31− @#perl ./runtest.pl test004 --target node

31+ @#perl ./runtest.pl test004 --codegen node

32− @perl ./runtest.pl test005 --target node

32+ @perl ./runtest.pl test005 --codegen node

33− @perl ./runtest.pl test006 --target node

33+ @perl ./runtest.pl test006 --codegen node

34− @perl ./runtest.pl test007 --target node

34+ @perl ./runtest.pl test007 --codegen node

35− @perl ./runtest.pl test008 --target node

35+ @perl ./runtest.pl test008 --codegen node

36− @perl ./runtest.pl test009 --target node

36+ @perl ./runtest.pl test009 --codegen node

37− @perl ./runtest.pl test010 --target node

37+ @perl ./runtest.pl test010 --codegen node

38− @perl ./runtest.pl test011 --target node

38+ @perl ./runtest.pl test011 --codegen node

39− @perl ./runtest.pl test012 --target node

39+ @perl ./runtest.pl test012 --codegen node

40− @perl ./runtest.pl test013 --target node

40+ @perl ./runtest.pl test013 --codegen node

41− @#perl ./runtest.pl test014 --target node

41+ @#perl ./runtest.pl test014 --codegen node

42− @perl ./runtest.pl test015 --target node

42+ @perl ./runtest.pl test015 --codegen node

43− @perl ./runtest.pl test016 --target node

43+ @perl ./runtest.pl test016 --codegen node

44− @perl ./runtest.pl test017 --target node

44+ @perl ./runtest.pl test017 --codegen node

45− @#perl ./runtest.pl test018 --target node

45+ @#perl ./runtest.pl test018 --codegen node

46− @perl ./runtest.pl test019 --target node

46+ @perl ./runtest.pl test019 --codegen node

47− @perl ./runtest.pl test020 --target node

47+ @perl ./runtest.pl test020 --codegen node

48− @#perl ./runtest.pl test021 --target node

48+ @#perl ./runtest.pl test021 --codegen node

49− @perl ./runtest.pl test022 --target node

49+ @perl ./runtest.pl test022 --codegen node

50− @perl ./runtest.pl test023 --target node

50+ @perl ./runtest.pl test023 --codegen node

51− @perl ./runtest.pl test024 --target node

51+ @perl ./runtest.pl test024 --codegen node

52− @#perl ./runtest.pl test025 --target node

52+ @#perl ./runtest.pl test025 --codegen node

53− @perl ./runtest.pl test026 --target node

53+ @perl ./runtest.pl test026 --codegen node

54− @perl ./runtest.pl test027 --target node

54+ @perl ./runtest.pl test027 --codegen node

55− @perl ./runtest.pl test028 --target node

55+ @perl ./runtest.pl test028 --codegen node

57update:

58 perl ./runtest.pl all -u