Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Upgrade to Idris 1.3.1. #25

Open
wants to merge 5 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .travis.yml
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ addons:
- hvr-ghc
- mono-nightly
packages:
- ghc-8.0.1
- ghc-8.2.2
- mono-devel
- mono-utils

Expand Down
2 changes: 1 addition & 1 deletion src/IRTS/Cil/FFI.hs
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ module IRTS.Cil.FFI
import qualified Data.HashMap.Strict as HM
import Data.Maybe
import Data.Monoid ((<>))
import Data.Text hiding (map, init, last)
import Data.Text hiding (init, last)

import IRTS.Lang (FDesc(..))
import Idris.Core.TT (Name(..), sUN)
Expand Down
20 changes: 12 additions & 8 deletions src/IRTS/CodegenCil.hs
Original file line number Diff line number Diff line change
Expand Up @@ -184,11 +184,12 @@ originalParameterNamesOf fn@(NS n _) (_, istate) = do

cilExport :: CilCodegenInfo -> Export -> CAF CilExport
cilExport cci (ExportFun fn@(NS n _) desc rt ps) = do
invocation <-
if null ps
then do instruction <- loadCAF fn
pure [instruction]
else pure (loadArgs <> [ app fn ps ])
let invocation
--if null ps
-- then do instruction <- loadCAF fn
-- pure [instruction]
-- else
= if isIO rt then loadArgs <> (loadNothing:[ app' fn ps ]) else loadArgs <> [ app fn ps ]
pure . CilFun $ delegateFunction [MaPublic, MaStatic] retType exportName parameters io invocation
where retType = foreignType rt
exportName = case desc of
Expand All @@ -197,7 +198,7 @@ cilExport cci (ExportFun fn@(NS n _) desc rt ps) = do
parameters = zip paramTypes (maybe paramNames (<> paramNames) (originalParameterNamesOf fn cci))
paramTypes = foreignType <$> ps
loadArgs = zip [0..] paramTypes >>= loadArg
io = isIO rt
io = False --isIO rt

cilExport _ (ExportData (FStr exportedDataType)) = pure . CilType $ publicStruct exportedDataType [ptr] [ctor] []
where ptr = Field [FaAssembly, FaInitOnly] Cil.Object "ptr"
Expand Down Expand Up @@ -555,7 +556,7 @@ cilMethod attrs retType name parameters body = Method attrs retType name paramet
withMaxStack body retType = maxStack (maxStackFor body retType) : body

paramNames :: [String]
paramNames = (("p" <>) . show) <$> [0..]
paramNames = ("p" <>) . show <$> [0..]

-- Exported data types are encoded as structs with a single `ptr` field
loadArg :: (Int, PrimitiveType) -> [Instruction]
Expand Down Expand Up @@ -1247,7 +1248,7 @@ recordType methods constTags = classDef [CaPrivate, CaBeforeFieldInit] className
where className = recordTypeName
allFields = tag : constFields
tag = Field [FaPublic, FaInitOnly] Int32 "tag"
constFields = (Field [FaStatic, FaPublic, FaInitOnly] recordTypeRef . constRecordFieldNameForTag) <$> constTags
constFields = Field [FaStatic, FaPublic, FaInitOnly] recordTypeRef . constRecordFieldNameForTag <$> constTags
allMethods = [cctor, ctor, toString] <> methods
ctor = Constructor [MaPublic] Void [ Param Nothing Int32 "tag" ]
[ ldarg 0
Expand Down Expand Up @@ -1397,5 +1398,8 @@ quoted name = "'" <> (name >>= validChar) <> "'"
app :: Name -> [a] -> Instruction
app n args = call [] Cil.Object "" moduleName (cilName n) (const Cil.Object <$> args)

app' :: Name -> [a] -> Instruction
app' n args = call [] Cil.Object "" moduleName (cilName n) (Cil.Object:(const Cil.Object <$> args))

concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM a b = concat <$> mapM a b
4 changes: 2 additions & 2 deletions stack.yaml
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
resolver: lts-10.0
resolver: lts-11.14

packages:
- location: .
Expand All @@ -8,7 +8,7 @@ packages:
extra-dep: true
- location:
git: https://github.com/idris-lang/Idris-dev.git
commit: cd7e553b6e6d74e3db07f88c8dabeaad968b1d1b
commit: 1510fce9236a088031f7468bf2024b31fe8d1165
extra-dep: true
flags:
idris:
Expand Down
2 changes: 2 additions & 0 deletions test/cases/Enums.idr
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,8 @@ writing
-}
module Main

import Language.Reflection.Utils

import CIL.FFI
import CIL.Elab.Enums

Expand Down
2 changes: 1 addition & 1 deletion test/cases/MaybeAsNullable.idr
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ maybeInt True = Just 42
maybeInt False = Nothing

testMaybeInt : Bool -> CIL_IO ()
testMaybeInt b = printLn (maybeInt b)
testMaybeInt b = putStrLn $ show (maybeInt b)

%inline
invokeTestMaybeInt : Bool -> CIL_IO ()
Expand Down