on master help sign in
Merge branch 'master' of github.com:idris-lang/Idris-dev
commit9ac4fdc6ad9da5080068c00823b326558b5b9967 authorScott Bonds <scott@ggr.com> dateFri 4 Aug 2017, 08:23 (9 years ago) parentfdc0e3c9d69b47
12 files changed+276−329
Setup.hs+33−18 docs/reference/partial-evaluation.rst+10−10 idris.cabal+10−2 libs/contrib/Text/Lexer.idr+27−17 libs/contrib/Text/Parser.idr+67−26 libs/contrib/Text/PrettyPrint/WL/Characters.idr+2−2 libs/contrib/Text/PrettyPrint/WL/Core.idr+4−4 src/IRTS/CodegenC.hs+116−233 src/IRTS/Compiler.hs+2 src/Idris/Core/Binary.hs+4−2 src/Idris/DeepSeq.hs−14 src/Idris/IBC.hs+1−1
Setup.hs+33−18
@@ -1,11 +1,15 @@
11{-# LANGUAGE CPP #-}
22
3+#if !defined(MIN_VERSION_Cabal)
4+# define MIN_VERSION_Cabal(x,y,z) 0
5+#endif
6+
37import Control.Monad
48import Data.IORef
59import Control.Exception (SomeException, catch)
610
711import Distribution.Simple
8−import Distribution.Simple.BuildPaths (autogenModulesDir)
12+import Distribution.Simple.BuildPaths
913import Distribution.Simple.InstallDirs as I
1014import Distribution.Simple.LocalBuildInfo as L
1115import qualified Distribution.Simple.Setup as S
@@ -56,32 +60,37 @@ windres verbosity = P.runProgramInvocation verbosity . P.simpleProgramInvocation
5660
5761usesGMP :: S.ConfigFlags -> Bool
5862usesGMP flags =
59− case lookup (FlagName "gmp") (S.configConfigurationsFlags flags) of
63+ case lookup (mkFlagName "gmp") (S.configConfigurationsFlags flags) of
6064 Just True -> True
6165 Just False -> False
6266 Nothing -> False
6367
6468execOnly :: S.ConfigFlags -> Bool
6569execOnly flags =
66− case lookup (FlagName "execonly") (S.configConfigurationsFlags flags) of
70+ case lookup (mkFlagName "execonly") (S.configConfigurationsFlags flags) of
6771 Just True -> True
6872 Just False -> False
6973 Nothing -> False
7074
7175isRelease :: S.ConfigFlags -> Bool
7276isRelease flags =
73− case lookup (FlagName "release") (S.configConfigurationsFlags flags) of
77+ case lookup (mkFlagName "release") (S.configConfigurationsFlags flags) of
7478 Just True -> True
7579 Just False -> False
7680 Nothing -> False
7781
7882isFreestanding :: S.ConfigFlags -> Bool
7983isFreestanding flags =
80− case lookup (FlagName "freestanding") (S.configConfigurationsFlags flags) of
84+ case lookup (mkFlagName "freestanding") (S.configConfigurationsFlags flags) of
8185 Just True -> True
8286 Just False -> False
8387 Nothing -> False
8488
89+#if !(MIN_VERSION_Cabal(2,0,0))
90+mkFlagName :: String -> FlagName
91+mkFlagName = FlagName
92+#endif
93+
8594-- -----------------------------------------------------------------------------
8695-- Clean
8796
@@ -151,20 +160,22 @@ generateToolchainModule verbosity srcDir toolDir = do
151160 createDirectoryIfMissingVerbose verbosity True srcDir
152161 rewriteFile toolPath (commonContent ++ toolContent)
153162
154−idrisConfigure _ flags _ local = do
163+idrisConfigure _ flags pkgdesc local = do
155164 configureRTS
156− generateVersionModule verbosity (autogenModulesDir local) (isRelease (configFlags local))
157− if isFreestanding $ configFlags local
158− then do
159− toolDir <- lookupEnv "IDRIS_TOOLCHAIN_DIR"
160− generateToolchainModule verbosity (autogenModulesDir local) toolDir
161− targetDir <- lookupEnv "IDRIS_LIB_DIR"
162− case targetDir of
163− Just d -> generateTargetModule verbosity (autogenModulesDir local) d
164− Nothing -> error $ "Trying to build freestanding without a target directory."
165− ++ " Set it by defining IDRIS_LIB_DIR."
166− else
167− generateToolchainModule verbosity (autogenModulesDir local) Nothing
165+ withLibLBI pkgdesc local $ \_ libcfg -> do
166+ let libAutogenDir = autogenComponentModulesDir local libcfg
167+ generateVersionModule verbosity libAutogenDir (isRelease (configFlags local))
168+ if isFreestanding $ configFlags local
169+ then do
170+ toolDir <- lookupEnv "IDRIS_TOOLCHAIN_DIR"
171+ generateToolchainModule verbosity libAutogenDir toolDir
172+ targetDir <- lookupEnv "IDRIS_LIB_DIR"
173+ case targetDir of
174+ Just d -> generateTargetModule verbosity libAutogenDir d
175+ Nothing -> error $ "Trying to build freestanding without a target directory."
176+ ++ " Set it by defining IDRIS_LIB_DIR."
177+ else
178+ generateToolchainModule verbosity libAutogenDir Nothing
168179 where
169180 verbosity = S.fromFlag $ S.configVerbosity flags
170181 version = pkgVersion . package $ localPkgDescr local
@@ -175,6 +186,10 @@ idrisConfigure _ flags _ local = do
175186 -- the file after configure.
176187 configureRTS = make verbosity ["-C", "rts", "clean"]
177188
189+#if !(MIN_VERSION_Cabal(2,0,0))
190+ autogenComponentModulesDir lbi _ = autogenModulesDir lbi
191+#endif
192+
178193idrisPreSDist args flags = do
179194 let dir = S.fromFlag (S.sDistDirectory flags)
180195 let verb = S.fromFlag (S.sDistVerbosity flags)
docs/reference/partial-evaluation.rst+10−10
@@ -4,15 +4,15 @@ Static Arguments and Partial Evaluation
44
55As of version 0.9.15, Idris has support for *partial evaluation* of
66statically known arguments. This involves creating specialised versions
7−of functions with arguments annotated as ``[static]``.
7+of functions with arguments annotated as ``%static``.
88
99(This is an implementation of the partial evaluator described in `this
1010ICFP 2010
1111paper <http://eb.host.cs.st-andrews.ac.uk/writings/icfp10.pdf>`__.
1212Please refer to this for more precise definitions of what follows.)
1313
14−Partial evaluation is switched on by default. It can be disabled with
15−the ``--no-partial-eval`` flag.
14+Partial evaluation is switched off by default since Idris 1.0. It can
15+be enabled with the ``--partial-eval`` flag.
1616
1717Introductory Example
1818--------------------
@@ -66,18 +66,18 @@ Automatic specialisation of ``pow``
6666~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
6767
6868The trick is to mark the statically known arguments with the
69−``[static]`` flag:
69+``%static`` flag:
7070
7171::
7272
73− my_pow : Nat -> [static] Nat -> Nat
73+ my_pow : Nat -> %static Nat -> Nat
7474 my_pow k Z = 1
7575 my_pow k (S j) = mult k (my_pow k j)
7676
7777When an argument is annotated in this way, Idris will try to create a
7878specialised version whenever it accounts a call with a concrete value
7979(i.e. a constant, constructor form, or globally defined function) in a
80−``[static]`` position. If ``my_pow`` is defined this way, and ``powFn``
80+``%static`` position. If ``my_pow`` is defined this way, and ``powFn``
8181defined as above, we can see the effect by typing ``:printdef powFn`` at
8282the REPL:
8383
@@ -108,7 +108,7 @@ Specialising Type Classes
108108-------------------------
109109
110110Type class dictionaries are very often statically known, so Idris
111−automatically marks any type class constraint as ``[static]`` and builds
111+automatically marks any type class constraint as ``%static`` and builds
112112specialised versions of top level functions where the class is
113113instantiated. For example, given:
114114
@@ -177,7 +177,7 @@ writing ``map`` as follows:
177177
178178::
179179
180− my_map : [static] (a -> b) -> List a -> List b
180+ my_map : %static (a -> b) -> List a -> List b
181181 my_map f [] = []
182182 my_map f (x :: xs) = f x :: my_map f xs
183183
@@ -246,11 +246,11 @@ Then, a function which calculates the factorial of its input:
246246 (App (App eMult (App eFac (Op (-) x (Val 1)))) x))
247247
248248The interpreter's type is written as follows, marking the expression to
249−be evaluated as ``[static]``:
249+be evaluated as ``%static``:
250250
251251::
252252
253− interp : (env : Env gamma) -> [static] (e : Expr gamma t) -> interpTy t
253+ interp : (env : Env gamma) -> %static (e : Expr gamma t) -> interpTy t
254254
255255This means that if we write an Idris program to calculate a factorial by
256256calling ``interp`` on ``eFac``, the resulting definition will be
idris.cabal+10−2
@@ -97,6 +97,14 @@ source-repository head
9797 type: git
9898 location: git://github.com/idris-lang/Idris-dev.git
9999
100+custom-setup
101+ setup-depends:
102+ Cabal >= 1.10 && <2.1,
103+ base >= 4 && <5,
104+ directory,
105+ filepath,
106+ process
107+
100108Flag FFI
101109 Description: Build support for libffi
102110 Default: False
@@ -265,11 +273,11 @@ Library
265273 , ansi-wl-pprint < 0.7
266274 , array >= 0.4.0.1 && < 0.6
267275 , base64-bytestring < 1.1
268− , binary >= 0.7 && < 0.9
276+ , binary >= 0.8.4.1 && < 0.9
269277 , blaze-html >= 0.6.1.3 && < 0.10
270278 , blaze-markup >= 0.5.2.1 && < 0.9
271279 , bytestring < 0.11
272− , cheapskate < 0.1.1
280+ , cheapskate >= 0.1.1 && < 0.2
273281 , code-page >= 0.1 && < 0.2
274282 , containers >= 0.5 && < 0.6
275283 , deepseq < 1.5
libs/contrib/Text/Lexer.idr+27−17
@@ -23,11 +23,11 @@ public export
2323inf : Bool -> Type -> Type
2424inf True t = Inf t
2525inf False t = t
26−
26+
2727||| Sequence two recognisers. If either consumes a character, the sequence
2828||| is guaranteed to consume a character.
2929export %inline
30−(<+>) : {c1 : Bool} ->
30+(<+>) : {c1 : Bool} ->
3131 Recognise c1 -> inf c1 (Recognise c2) -> Recognise (c1 || c2)
3232(<+>) {c1 = False} = SeqEmpty
3333(<+>) {c1 = True} = SeqEat
@@ -59,6 +59,17 @@ export
5959many : Lexer -> Recognise False
6060many l = some l <|> Empty
6161
62+||| Recognise many instances of `l` until an instance of `end` is
63+||| encountered.
64+|||
65+||| Useful for defining comments.
66+export
67+manyTill : (l : Lexer)
68+ -> (end : Lexer) -> Recognise False
69+manyTill l end = end
70+ <|> (l <+> manyTill l end)
71+ <|> Empty
72+
6273||| Recognise any character
6374export
6475any : Lexer
@@ -86,7 +97,7 @@ getString : StrLen -> String
8697getString (MkStrLen str n) = str
8798
8899strIndex : StrLen -> Nat -> Maybe Char
89−strIndex (MkStrLen str len) i
100+strIndex (MkStrLen str len) i
90101 = if i >= len then Nothing
91102 else Just (assert_total (prim__strIndex str (cast i)))
92103
@@ -102,25 +113,25 @@ strTail start (MkStrLen str len)
102113scan : Recognise c -> Nat -> StrLen -> Maybe Nat
103114scan Empty idx str = pure idx
104115scan Fail idx str = Nothing
105−scan (Pred f) idx str
116+scan (Pred f) idx str
106117 = do c <- strIndex str idx
107118 if f c
108119 then Just (idx + 1)
109120 else Nothing
110−scan (SeqEat r1 r2) idx str
121+scan (SeqEat r1 r2) idx str
111122 = do idx' <- scan r1 idx str
112123 -- TODO: Can we prove totality instead by showing idx has increased?
113124 assert_total (scan r2 idx' str)
114−scan (SeqEmpty r1 r2) idx str
125+scan (SeqEmpty r1 r2) idx str
115126 = do idx' <- scan r1 idx str
116127 scan r2 idx' str
117−scan (Alt r1 r2) idx str
128+scan (Alt r1 r2) idx str
118129 = case scan r1 idx str of
119130 Nothing => scan r2 idx str
120131 Just idx => Just idx
121132
122133takeToken : Lexer -> StrLen -> Maybe (String, StrLen)
123−takeToken lex str
134+takeToken lex str
124135 = do i <- scan lex 0 str -- i must be > 0 if successful
125136 pure (substr 0 i (getString str), strTail i str)
126137
@@ -134,7 +145,7 @@ export
134145exact : String -> Lexer
135146exact str with (unpack str)
136147 exact str | [] = Fail -- Not allowed, Lexer has to consume
137− exact str | (x :: xs)
148+ exact str | (x :: xs)
138149 = foldl SeqEmpty (is x) (map is xs)
139150
140151||| Recognise a whitespace character
@@ -185,8 +196,8 @@ record TokenData a where
185196
186197fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String)
187198fspanEnd k p "" = (k, "")
188−fspanEnd k p xxs
189− = assert_total $
199+fspanEnd k p xxs
200+ = assert_total $
190201 let x = prim__strHead xxs
191202 xs = prim__strTail xxs in
192203 if p x then fspanEnd (S k) p xs
@@ -195,14 +206,14 @@ fspanEnd k p xxs
195206-- Faster version of 'span' from the prelude (avoids unpacking)
196207export
197208fspan : (Char -> Bool) -> String -> (String, String)
198−fspan p xs
209+fspan p xs
199210 = let (end, rest) = fspanEnd 0 p xs in
200211 (substr 0 end xs, rest)
201212
202213tokenise : (line : Int) -> (col : Int) ->
203− List (TokenData a) -> TokenMap a ->
214+ List (TokenData a) -> TokenMap a ->
204215 StrLen -> (List (TokenData a), (Int, Int, StrLen))
205−tokenise line col acc tmap str
216+tokenise line col acc tmap str
206217 = case getFirstToken tmap str of
207218 Just (tok, line', col', rest) =>
208219 -- assert total because getFirstToken must consume something
@@ -213,7 +224,7 @@ tokenise line col acc tmap str
213224 countNLs str = List.length (filter (== '\n') str)
214225
215226 getCols : String -> Int -> Int
216− getCols x c
227+ getCols x c
217228 = case fspan (/= '\n') (reverse x) of
218229 (incol, "") => c + cast (length incol)
219230 (incol, _) => cast (length incol)
@@ -223,7 +234,7 @@ tokenise line col acc tmap str
223234 getFirstToken ((lex, fn) :: ts) str
224235 = case takeToken lex str of
225236 Just (tok, rest) => Just (MkToken line col (fn tok),
226− line + cast (countNLs (unpack tok)),
237+ line + cast (countNLs (unpack tok)),
227238 getCols tok col, rest)
228239 Nothing => getFirstToken ts str
229240
@@ -235,4 +246,3 @@ export
235246lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
236247lex tmap str = let (ts, (l, c, str')) = tokenise 0 0 [] tmap (mkStr str) in
237248 (ts, (l, c, getString str'))
238−
libs/contrib/Text/Parser.idr+67−26
@@ -3,7 +3,7 @@ module Text.Parser
33%default total
44
55-- TODO: Add some primitives for helping with error messages.
6−-- e.g. perhaps set a string to state what we're currently trying to
6+-- e.g. perhaps set a string to state what we're currently trying to
77-- parse, or to say what the next expected token is in words
88
99||| Description of a language's grammar. The `tok` parameter is the type
@@ -26,14 +26,14 @@ data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
2626 Grammar tok c1 a -> (a -> Grammar tok c2 b) ->
2727 Grammar tok (c1 || c2) b
2828 Alt : {c1, c2 : Bool} ->
29− Grammar tok c1 ty -> Grammar tok c2 ty ->
29+ Grammar tok c1 ty -> Grammar tok c2 ty ->
3030 Grammar tok (c1 && c2) ty
3131
3232public export
3333inf : Bool -> Type -> Type
3434inf True t = Inf t
3535inf False t = t
36−
36+
3737||| Sequence two grammars. If either consumes some input, the sequence is
3838||| guaranteed to consume some input. If the first one consumes input, the
3939||| second is allowed to be recursive (because it means some input has been
@@ -44,11 +44,11 @@ export %inline
4444 Grammar tok (c1 || c2) b
4545(>>=) {c1 = False} = SeqEmpty
4646(>>=) {c1 = True} = SeqEat
47−
47+
4848||| Give two alternative grammars. If both consume, the combination is
4949||| guaranteed to consume.
5050export
51−(<|>) : Grammar tok c1 ty -> Grammar tok c2 ty ->
51+(<|>) : Grammar tok c1 ty -> Grammar tok c2 ty ->
5252 Grammar tok (c1 && c2) ty
5353(<|>) = Alt
5454
@@ -82,21 +82,21 @@ export
8282eof : Grammar tok False ()
8383eof = EOF
8484
85−||| Commit to an alternative; if the current branch of an alternative
85+||| Commit to an alternative; if the current branch of an alternative
8686||| fails to parse, no more branches will be tried
8787export
8888commit : Grammar tok False ()
8989commit = Commit
9090
9191data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where
92− Failure : {xs : List tok} ->
92+ Failure : {xs : List tok} ->
9393 (committed : Bool) ->
9494 (err : String) -> (rest : List tok) -> ParseResult xs c ty
9595 EmptyRes : (committed : Bool) ->
9696 (val : ty) -> (more : List tok) -> ParseResult more False ty
9797 NonEmptyRes : (committed : Bool) ->
9898 (val : ty) -> (more : List tok) ->
99− ParseResult (x :: xs ++ more) c ty
99+ ParseResult (x :: xs ++ more) c ty
100100
101101weakenRes : {whatever, c : Bool} -> {xs : List tok} ->
102102 ParseResult xs c ty -> ParseResult xs (whatever && c) ty
@@ -105,13 +105,13 @@ weakenRes {whatever=True} (EmptyRes com val xs) = EmptyRes com val xs
105105weakenRes {whatever=False} (EmptyRes com val xs) = EmptyRes com val xs
106106weakenRes (NonEmptyRes com val more) = NonEmptyRes com val more
107107
108−shorter : (more : List tok) -> .(ys : List tok) ->
108+shorter : (more : List tok) -> .(ys : List tok) ->
109109 LTE (S (length more)) (S (length (ys ++ more)))
110110shorter more [] = lteRefl
111111shorter more (x :: xs) = LTESucc (lteSuccLeft (shorter more xs))
112112
113113doParse : {c : Bool} ->
114− (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->
114+ (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->
115115 ParseResult xs c ty
116116doParse com xs act with (sizeAccessible xs)
117117 doParse com xs (Empty val) | sml = EmptyRes com val xs
@@ -120,17 +120,17 @@ doParse com xs act with (sizeAccessible xs)
120120 doParse com xs Commit | sml = EmptyRes True () xs
121121
122122 doParse com [] (Terminal f) | sml = Failure com "End of input" []
123− doParse com (x :: xs) (Terminal f) | sml
123+ doParse com (x :: xs) (Terminal f) | sml
124124 = maybe
125125 (Failure com "Unrecognised token" (x :: xs))
126126 (\a => NonEmptyRes com {xs=[]} a xs)
127127 (f x)
128128 doParse com [] EOF | sml = EmptyRes com () []
129− doParse com (x :: xs) EOF | sml
129+ doParse com (x :: xs) EOF | sml
130130 = Failure com "Expected end of input" (x :: xs)
131131 doParse com [] (NextIs f) | sml = Failure com "End of input" []
132− doParse com (x :: xs) (NextIs f) | sml
133− = if f x
132+ doParse com (x :: xs) (NextIs f) | sml
133+ = if f x
134134 then EmptyRes com x (x :: xs)
135135 else Failure com "Unrecognised token" (x :: xs)
136136 doParse com xs (Alt x y) | sml with (doParse False xs x | sml)
@@ -140,19 +140,19 @@ doParse com xs act with (sizeAccessible xs)
140140 then Failure com msg ts
141141 else weakenRes (doParse False xs y | sml)
142142 -- Successfully parsed the first option, so use the outer commit flag
143− doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)
143+ doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)
144144 = EmptyRes com val xs
145− doParse com (z :: (ys ++ more)) (Alt x y) | sml | (NonEmptyRes _ val more)
145+ doParse com (z :: (ys ++ more)) (Alt x y) | sml | (NonEmptyRes _ val more)
146146 = NonEmptyRes com val more
147147 doParse com xs (SeqEmpty act next) | (Access morerec)
148148 = case doParse com xs act | Access morerec of
149149 Failure com msg ts => Failure com msg ts
150− EmptyRes com val xs =>
150+ EmptyRes com val xs =>
151151 case doParse com xs (next val) | (Access morerec) of
152152 Failure com' msg ts => Failure com' msg ts
153153 EmptyRes com' val xs => EmptyRes com' val xs
154154 NonEmptyRes com' val more => NonEmptyRes com' val more
155− NonEmptyRes {x} {xs=ys} com val more =>
155+ NonEmptyRes {x} {xs=ys} com val more =>
156156 case (doParse com more (next val) | morerec _ (shorter more ys)) of
157157 Failure com' msg ts => Failure com' msg ts
158158 EmptyRes com' val _ => NonEmptyRes com' val more
@@ -160,13 +160,13 @@ doParse com xs act with (sizeAccessible xs)
160160 rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
161161 NonEmptyRes com' val more'
162162 doParse com xs (SeqEat act next) | sml with (doParse com xs act | sml)
163− doParse com xs (SeqEat act next) | sml | Failure com' msg ts
163+ doParse com xs (SeqEat act next) | sml | Failure com' msg ts
164164 = Failure com' msg ts
165− doParse com (x :: (ys ++ more)) (SeqEat act next) | (Access morerec) | (NonEmptyRes com' val more)
165+ doParse com (x :: (ys ++ more)) (SeqEat act next) | (Access morerec) | (NonEmptyRes com' val more)
166166 = case doParse com' more (next val) | morerec _ (shorter more ys) of
167167 Failure com' msg ts => Failure com' msg ts
168168 EmptyRes com' val _ => NonEmptyRes com' val more
169− NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
169+ NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
170170 rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
171171 NonEmptyRes com' val more'
172172 -- This next line is not strictly necessary, but it stops the coverage
@@ -180,7 +180,7 @@ data ParseError tok = Error String (List tok)
180180||| returns a pair of the parse result and the unparsed tokens (the remaining
181181||| input).
182182export
183−parse : (xs : List tok) -> (act : Grammar tok c ty) ->
183+parse : (xs : List tok) -> (act : Grammar tok c ty) ->
184184 Either (ParseError tok) (ty, List tok)
185185parse xs act
186186 = case doParse False xs act of
@@ -190,7 +190,7 @@ parse xs act
190190
191191||| Parse one or more things
192192export
193−some : Grammar tok True a ->
193+some : Grammar tok True a ->
194194 Grammar tok True (List a)
195195some p = do x <- p
196196 (do xs <- some p
@@ -198,14 +198,14 @@ some p = do x <- p
198198
199199||| Parse zero or more things (may match the empty input)
200200export
201−many : Grammar tok True a ->
201+many : Grammar tok True a ->
202202 Grammar tok False (List a)
203203many p = some p
204204 <|> pure []
205205
206206||| Parse one or more things, separated by another thing
207207export
208−sepBy1 : Grammar tok True () -> Grammar tok True a ->
208+sepBy1 : Grammar tok True () -> Grammar tok True a ->
209209 Grammar tok True (List a)
210210sepBy1 sep p = do x <- p
211211 (do sep
@@ -215,7 +215,7 @@ sepBy1 sep p = do x <- p
215215||| Parse zero or more things, separated by another thing. May
216216||| match the empty input.
217217export
218−sepBy : Grammar tok True () -> Grammar tok True a ->
218+sepBy : Grammar tok True () -> Grammar tok True a ->
219219 Grammar tok False (List a)
220220sepBy sep p = sepBy1 sep p <|> pure []
221221
@@ -227,3 +227,44 @@ optional : Grammar tok True a -> (ifNothing : a) ->
227227optional p def = p <|> pure def
228228
229229
230+||| Parse an instance of `p` that is between `left` and `right`.
231+export
232+between : (left : Grammar tok True ())
233+ -> (right : Grammar tok True ())
234+ -> (p : Grammar tok True a)
235+ -> Grammar tok True a
236+between left right contents = do
237+ left
238+ res <- contents
239+ right
240+ pure res
241+
242+||| Parse one or more instances of `p` separated by `s`, returning the
243+||| parsed items and proof the resulting list is non-empty.
244+export
245+sepBy1' : (sep : Grammar tok True ())
246+ -> (p : Grammar tok True a)
247+ -> Grammar tok True (xs : List a ** NonEmpty xs)
248+sepBy1' sep p
249+ = do x <- p
250+ (do sep
251+ xs <- sepBy1 sep p
252+ pure (x :: xs ** IsNonEmpty)) <|> pure ([x] ** IsNonEmpty)
253+
254+||| Parse one or more instances of `p`, returning the parsed items and proof the resulting list is non-empty.
255+export
256+some' : (p : Grammar tok True a)
257+ -> Grammar tok True (xs : List a ** NonEmpty xs)
258+some' p = do
259+ x <- p
260+ (do xs <- some p
261+ pure (x::xs ** IsNonEmpty)) <|> pure ([x] ** IsNonEmpty)
262+
263+
264+||| Optionally parse a thing. If the grammar provides a default use `optional` instead.
265+export
266+maybe : Grammar tok True a
267+ -> Grammar tok False (Maybe a)
268+maybe p =
269+ (do res <- p; pure $ Just res)
270+ <|> pure Nothing
libs/contrib/Text/PrettyPrint/WL/Characters.idr+2−2
@@ -69,8 +69,8 @@ bang = char '!'
6969tick : Doc
7070tick = char '`'
7171
72−tilda : Doc
73−tilda = char '~'
72+tilde : Doc
73+tilde = char '~'
7474
7575hash : Doc
7676hash = char '#'
libs/contrib/Text/PrettyPrint/WL/Core.idr+4−4
@@ -128,10 +128,10 @@ showPrettyDoc : (doc : PrettyDoc) -> String
128128showPrettyDoc doc = showPrettyDocS doc ""
129129 where
130130 showPrettyDocS : (doc : PrettyDoc) -> (acc : String) -> String
131− showPrettyDocS Empty = id
132− showPrettyDocS (Chara c rest) = strCons c . showPrettyDocS rest
133− showPrettyDocS (Text len str rest) = (str ++) . showPrettyDocS rest
134− showPrettyDocS (Line lvl rest) = (('\n' `strCons` indentation lvl) ++) . showPrettyDocS rest
131+ showPrettyDocS Empty acc = acc
132+ showPrettyDocS (Chara c rest) acc = strCons c (showPrettyDocS rest acc)
133+ showPrettyDocS (Text len str rest) acc = str ++ (showPrettyDocS rest acc)
134+ showPrettyDocS (Line lvl rest) acc = (strCons '\n' (indentation lvl)) ++ showPrettyDocS rest acc
135135
136136private
137137fits : (w : Int) -> (x : PrettyDoc) -> Bool
src/IRTS/CodegenC.hs+116−233
@@ -9,7 +9,7 @@ Maintainer : The Idris Community.
99
1010module IRTS.CodegenC (codegenC) where
1111
12−import Idris.AbsSyntax hiding (getBC)
12+import Idris.AbsSyntax
1313import Idris.Core.TT
1414import IRTS.Bytecode
1515import IRTS.CodegenCommon
@@ -21,12 +21,10 @@ import IRTS.System
2121import Util.System
2222
2323import Control.Monad
24−import Control.Monad
25−import Control.Monad.RWS
2624import Data.Bits
2725import Data.Char
28−import Data.List (find, intercalate, nubBy, partition)
29−import qualified Data.Text as T
26+import Data.List (intercalate, nubBy)
27+import Debug.Trace
3028import Numeric
3129import System.Directory
3230import System.Exit
@@ -34,8 +32,6 @@ import System.FilePath ((<.>), (</>))
3432import System.IO
3533import System.Process
3634
37−import Debug.Trace
38−
3935codegenC :: CodeGenerator
4036codegenC ci = do codegenC' (simpleDecls ci)
4137 (outputFile ci)
@@ -70,9 +66,7 @@ codegenC' defs out exec incs objs libs flags exports iface dbg
7066 let bc = map toBC defs
7167 let wrappers = genWrappers bc
7268 let h = concatMap toDecl (map fst bc)
73− let (state, cc) = execRWS (generateSrc bc) 0
74− (CS { fnName = Nothing,
75− level = 1 })
69+ let cc = concatMap (uncurry toC) bc
7670 let hi = concatMap ifaceC (concatMap getExp exports)
7771 d <- getIdrisCRTSDir
7872 mprog <- readFile (d </> "idris_main" <.> "c")
@@ -142,17 +136,12 @@ creg Tmp = "REG1"
142136toDecl :: Name -> String
143137toDecl f = "void " ++ cname f ++ "(VM*, VAL*);\n"
144138
145−generateSrc :: [(Name, [BC])] -> RWS Int String CState ()
146−generateSrc bc = mapM_ toC bc
147−
148−toC :: (Name, [BC]) -> RWS Int String CState ()
149−toC (f, code) = do
150− modify (\s -> s { fnName = Just f })
151− s <- get
152− tell $ "void " ++ cname f ++ "(VM* vm, VAL* oldbase) {\n"
153− tell $ indent (level s) ++ "INITFRAME;\n"
154− bcc code
155− tell $ "}\n\n"
139+toC :: Name -> [BC] -> String
140+toC f code
141+ = -- "/* " ++ show code ++ "*/\n\n" ++
142+ "void " ++ cname f ++ "(VM* vm, VAL* oldbase) {\n" ++
143+ indent 1 ++ "INITFRAME;\n" ++
144+ concatMap (bcc 1) code ++ "}\n\n"
156145
157146showCStr :: String -> String
158147showCStr s = '"' : foldr ((++) . showChar) "\"" s
@@ -188,27 +177,15 @@ showCStr s = '"' : foldr ((++) . showChar) "\"" s
188177 2 -> s
189178 _ -> error $ "Can't happen: String of invalid length " ++ show s
190179
191−data CState = CS {
192− fnName :: Maybe Name,
193− level :: Int
194−}
195−
196−
197−bcc :: [BC] -> RWS Int String CState ()
198−bcc [] = return ()
199−bcc ((ASSIGN l r):xs) = do
200− i <- get
201− tell $ indent (level i) ++ creg l ++ " = " ++ creg r ++ ";\n"
202− bcc xs
203−bcc ((ASSIGNCONST l c):xs) = do
204− i <- get
205− tell $ indent (level i) ++ creg l ++ " = " ++ mkConst c ++ ";\n"
206− bcc xs
180+bcc :: Int -> BC -> String
181+bcc i (ASSIGN l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"
182+bcc i (ASSIGNCONST l c)
183+ = indent i ++ creg l ++ " = " ++ mkConst c ++ ";\n"
207184 where
208185 mkConst (I i) = "MKINT(" ++ show i ++ ")"
209186 mkConst (BI i) | i < (2^30) = "MKINT(" ++ show i ++ ")"
210187 | otherwise = "MKBIGC(vm,\"" ++ show i ++ "\")"
211− mkConst (Fl f) = "MKFLOAT(vm, " ++ show f ++ ")"
188+ mkConst (Fl f) = "MKFLOAT(vm, " ++ (map toUpper $ show f) ++ ")"
212189 mkConst (Ch c) = "MKINT(" ++ show (fromEnum c) ++ ")"
213190 mkConst (Str s) = "MKSTR(vm, " ++ showCStr s ++ ")"
214191 mkConst (B8 x) = "idris_b8const(vm, " ++ show x ++ "U)"
@@ -221,21 +198,16 @@ bcc ((ASSIGNCONST l c):xs) = do
221198 mkConst c | isTypeConst c = "MKINT(42424242)"
222199 mkConst c = error $ "mkConst of (" ++ show c ++ ") not implemented"
223200
224−bcc ((UPDATE l r):xs) = do
225− i <- get
226− tell $ indent (level i) ++ creg l ++ " = " ++ creg r ++ ";\n"
227− bcc xs
228−bcc ((MKCON l loc tag []):xs) | tag < 256 = do
229− i <- get
230− tell $ indent (level i) ++ creg l ++ " = NULL_CON(" ++ show tag ++ ");\n"
231− bcc xs
232−bcc ((MKCON l loc tag args):xs) = do
233− i <- get
234− let tab = indent (level i)
235− tell $ tab ++ alloc loc tag ++
236− tab ++ setArgs 0 args ++ "\n" ++
237− tab ++ creg l ++ " = " ++ creg Tmp ++ ";\n"
238− bcc xs
201+bcc i (UPDATE l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"
202+bcc i (MKCON l loc tag []) | tag < 256
203+ = indent i ++ creg l ++ " = NULL_CON(" ++ show tag ++ ");\n"
204+bcc i (MKCON l loc tag args)
205+ = indent i ++ alloc loc tag ++
206+ indent i ++ setArgs 0 args ++ "\n" ++
207+ indent i ++ creg l ++ " = " ++ creg Tmp ++ ";\n"
208+
209+-- "MKCON(vm, " ++ creg l ++ ", " ++ show tag ++ ", " ++
210+-- show (length args) ++ concatMap showArg args ++ ");\n"
239211 where showArg r = ", " ++ creg r
240212 setArgs i [] = ""
241213 setArgs i (x : xs) = "SETARG(" ++ creg Tmp ++ ", " ++ show i ++ ", " ++ creg x ++
@@ -247,94 +219,52 @@ bcc ((MKCON l loc tag args):xs) = do
247219 = "updateCon(" ++ creg Tmp ++ ", " ++ creg old ++ ", " ++ show tag ++ ", " ++
248220 show (length args) ++ ");\n"
249221
250−bcc ((PROJECT l loc a):xs) = do
251− i <- get
252− tell $ indent (level i) ++ "PROJECT(vm, " ++ creg l ++ ", "
253− ++ show loc ++ ", " ++ show a ++ ");\n"
254− bcc xs
255−bcc ((PROJECTINTO r t idx):xs) = do
256− i <- get
257− tell $ indent (level i) ++ creg r ++ " = GETARG(" ++ creg t
258− ++ ", " ++ show idx ++ ");\n"
259− bcc xs
260−bcc ((CASE True r code def):xs)
261− | length code < 4 = do
262− showCases def code
263− bcc xs
222+bcc i (PROJECT l loc a) = indent i ++ "PROJECT(vm, " ++ creg l ++ ", " ++ show loc ++
223+ ", " ++ show a ++ ");\n"
224+bcc i (PROJECTINTO r t idx)
225+ = indent i ++ creg r ++ " = GETARG(" ++ creg t ++ ", " ++ show idx ++ ");\n"
226+bcc i (CASE True r code def)
227+ | length code < 4 = showCase i def code
264228 where
265− showCode bc = do
266− w <- getBC bc xs
267− i <- get
268− tell $ "{\n" ++ w ++ indent (level i) ++ "}\n"
269−
270− showCases Nothing [(t, c)] = do
271− i <- get
272− tell $ indent (level i)
273− showCode c
274− showCases (Just def) [] = do
275− i <- get
276− tell $ indent (level i)
277− showCode def
278− showCases def ((t, c) : cs) = do
279− i <- get
280− tell $ indent (level i) ++ "if (CTAG(" ++ creg r ++ ") == "
281− ++ show t ++ ") "
282− showCode c
283− tell $ indent (level i) ++ "else\n"
284− showCases def cs
285−
286−bcc ((CASE safe r code def):xs) = do
287− i <- get
288− tell $ indent (level i) ++ "switch(" ++ ctag safe ++ "(" ++ creg r ++ ")) {\n"
289− mapM showCase code
290− showDef def
291− tell $ indent (level i) ++ "}\n"
292− bcc xs
229+ showCode :: Int -> [BC] -> String
230+ showCode i bc = "{\n" ++ concatMap (bcc (i + 1)) bc ++
231+ indent i ++ "}\n"
232+
233+ showCase :: Int -> Maybe [BC] -> [(Int, [BC])] -> String
234+ showCase i Nothing [(t, c)] = indent i ++ showCode i c
235+ showCase i (Just def) [] = indent i ++ showCode i def
236+ showCase i def ((t, c) : cs)
237+ = indent i ++ "if (CTAG(" ++ creg r ++ ") == " ++ show t ++ ") " ++ showCode i c
238+ ++ indent i ++ "else\n" ++ showCase i def cs
239+
240+bcc i (CASE safe r code def)
241+ = indent i ++ "switch(" ++ ctag safe ++ "(" ++ creg r ++ ")) {\n" ++
242+ concatMap (showCase i) code ++
243+ showDef i def ++
244+ indent i ++ "}\n"
293245 where
294246 ctag True = "CTAG"
295247 ctag False = "TAG"
296248
297− showCase (t, bc) = do
298− w <- getBC bc xs
299− is <- get
300− let i = level is
301− tell $ indent i ++ "case " ++ show t ++ ":\n"
302− ++ w ++ indent (i + 1) ++ "break;\n"
303− showDef Nothing = return $ ()
304− showDef (Just c) = do
305− w <- getBC c xs
306− is <- get
307− let i = level is
308− tell $ indent i ++ "default:\n" ++ w ++ indent (i + 1) ++ "break;\n"
309−
310−bcc ((CONSTCASE r code def):xs)
249+ showCase i (t, bc) = indent i ++ "case " ++ show t ++ ":\n"
250+ ++ concatMap (bcc (i+1)) bc ++ indent (i + 1) ++ "break;\n"
251+ showDef i Nothing = ""
252+ showDef i (Just c) = indent i ++ "default:\n"
253+ ++ concatMap (bcc (i+1)) c ++ indent (i + 1) ++ "break;\n"
254+bcc i (CONSTCASE r code def)
311255 | intConsts code
312− = do
313− is <- get
314− let i = level is
315− codes <- mapM getCode code
316− defs <- showDefS def
317− tell $ concatMap (iCase i (creg r)) codes
318− tell $ indent i ++ "{\n" ++ defs ++ indent i ++ "}\n"
319− bcc xs
256+-- = indent i ++ "switch(GETINT(" ++ creg r ++ ")) {\n" ++
257+-- concatMap (showCase i) code ++
258+-- showDef i def ++
259+-- indent i ++ "}\n"
260+ = concatMap (iCase (creg r)) code ++
261+ indent i ++ "{\n" ++ showDefS i def ++ indent i ++ "}\n"
320262 | strConsts code
321− = do
322− is <- get
323− let i = level is
324− codes <- mapM getCode code
325− defs <- showDefS def
326− tell $ concatMap (strCase i ("GETSTR(" ++ creg r ++ ")")) codes
327− ++ indent i ++ "{\n" ++ defs ++ indent i ++ "}\n"
328− bcc xs
263+ = concatMap (strCase ("GETSTR(" ++ creg r ++ ")")) code ++
264+ indent i ++ "{\n" ++ showDefS i def ++ indent i ++ "}\n"
329265 | bigintConsts code
330− = do
331− is <- get
332− let i = level is
333− codes <- mapM getCode code
334− defs <- showDefS def
335− tell $ concatMap (biCase i (creg r)) codes ++
336− indent i ++ "{\n" ++ defs ++ indent i ++ "}\n"
337− bcc xs
266+ = concatMap (biCase (creg r)) code ++
267+ indent i ++ "{\n" ++ showDefS i def ++ indent i ++ "}\n"
338268 | otherwise = error $ "Can't happen: Can't compile const case " ++ show code
339269 where
340270 intConsts ((I _, _ ) : _) = True
@@ -351,119 +281,72 @@ bcc ((CONSTCASE r code def):xs)
351281 strConsts ((Str _, _ ) : _) = True
352282 strConsts _ = False
353283
354− getCode (x, code) = do
355− c <- getBC code xs
356− return (x, c)
357−
358− strCase i sv (s, bc) =
284+ strCase sv (s, bc) =
359285 indent i ++ "if (strcmp(" ++ sv ++ ", " ++ show s ++ ") == 0) {\n" ++
360− bc ++ indent i ++ "} else\n"
361− biCase i bv (BI b, bc) =
286+ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
287+ biCase bv (BI b, bc) =
362288 indent i ++ "if (bigEqConst(" ++ bv ++ ", " ++ show b ++ ")) {\n"
363− ++ bc ++ indent i ++ "} else\n"
364− iCase i v (I b, bc) =
289+ ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
290+ iCase v (I b, bc) =
365291 indent i ++ "if (GETINT(" ++ v ++ ") == " ++ show b ++ ") {\n"
366− ++ bc ++ indent i ++ "} else\n"
367− iCase i v (Ch b, bc) =
292+ ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
293+ iCase v (Ch b, bc) =
368294 indent i ++ "if (GETINT(" ++ v ++ ") == " ++ show (fromEnum b) ++ ") {\n"
369− ++ bc ++ indent i ++ "} else\n"
370− iCase i v (B8 w, bc) =
295+ ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
296+ iCase v (B8 w, bc) =
371297 indent i ++ "if (GETBITS8(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
372− ++ bc ++ indent i ++ "} else\n"
373− iCase i v (B16 w, bc) =
298+ ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
299+ iCase v (B16 w, bc) =
374300 indent i ++ "if (GETBITS16(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
375− ++ bc ++ indent i ++ "} else\n"
376− iCase i v (B32 w, bc) =
301+ ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
302+ iCase v (B32 w, bc) =
377303 indent i ++ "if (GETBITS32(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
378− ++ bc ++ indent i ++ "} else\n"
379− iCase i v (B64 w, bc) =
304+ ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
305+ iCase v (B64 w, bc) =
380306 indent i ++ "if (GETBITS64(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
381− ++ bc ++ indent i ++ "} else\n"
382−
383− showDefS Nothing = return ""
384− showDefS (Just c) = getBC c xs
385−
386−bcc (CALL n:xs) = do
387− i <- get
388− tell $ indent (level i) ++ "CALL(" ++ cname n ++ ");\n"
389− bcc xs
390−bcc (TAILCALL n:xs) = do
391− i <- get
392− tell $ indent (level i) ++ "TAILCALL(" ++ cname n ++ ");\n"
393− bcc xs
394−bcc ((SLIDE n):xs) = do
395− i <- get
396− tell $ indent (level i) ++ "SLIDE(vm, " ++ show n ++ ");\n"
397− bcc xs
398−bcc (REBASE:xs) = do
399− i <- get
400− tell $ indent (level i)++ "REBASE;\n"
401− bcc xs
402−bcc ((RESERVE 0):xs) = bcc xs
403−bcc ((RESERVE n):xs) = do
404− i <- get
405− tell $ indent (level i) ++ "RESERVE(" ++ show n ++ ");\n"
406− bcc xs
407−bcc ((ADDTOP 0):xs) = bcc xs
408−bcc ((ADDTOP n):xs) = do
409− i <- get
410− tell $ indent (level i) ++ "ADDTOP(" ++ show n ++ ");\n"
411− bcc xs
412−bcc ((TOPBASE n):xs) = do
413− i <- get
414− tell $ indent (level i) ++ "TOPBASE(" ++ show n ++ ");\n"
415− bcc xs
416−bcc ((BASETOP n):xs) = do
417− i <- get
418− tell $ indent (level i) ++ "BASETOP(" ++ show n ++ ");\n"
419− bcc xs
420−bcc (STOREOLD:xs) = do
421− i <- get
422− tell $ indent (level i) ++ "STOREOLD;\n"
423− bcc xs
424−bcc ((OP l fn args):xs) = do
425− i <- get
426− tell $ indent (level i) ++ doOp (creg l ++ " = ") fn args ++ ";\n"
427− bcc xs
428−bcc ((FOREIGNCALL l rty (FStr fn@('&':name)) []):xs) = do
429− i <- get
430− tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ") fn ++ ";\n"
431− bcc xs
432−bcc ((FOREIGNCALL l rty (FStr fn) (x:xs)):zs) | fn == "%wrapper"
433− = do
434− i <- get
435− tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ")
307+ ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
308+ showCase i (t, bc) = indent i ++ "case " ++ show t ++ ":\n"
309+ ++ concatMap (bcc (i+1)) bc ++
310+ indent (i + 1) ++ "break;\n"
311+ showDef i Nothing = ""
312+ showDef i (Just c) = indent i ++ "default:\n"
313+ ++ concatMap (bcc (i+1)) c ++
314+ indent (i + 1) ++ "break;\n"
315+ showDefS i Nothing = ""
316+ showDefS i (Just c) = concatMap (bcc (i+1)) c
317+
318+bcc i (CALL n) = indent i ++ "CALL(" ++ cname n ++ ");\n"
319+bcc i (TAILCALL n) = indent i ++ "TAILCALL(" ++ cname n ++ ");\n"
320+bcc i (SLIDE n) = indent i ++ "SLIDE(vm, " ++ show n ++ ");\n"
321+bcc i REBASE = indent i ++ "REBASE;\n"
322+bcc i (RESERVE 0) = ""
323+bcc i (RESERVE n) = indent i ++ "RESERVE(" ++ show n ++ ");\n"
324+bcc i (ADDTOP 0) = ""
325+bcc i (ADDTOP n) = indent i ++ "ADDTOP(" ++ show n ++ ");\n"
326+bcc i (TOPBASE n) = indent i ++ "TOPBASE(" ++ show n ++ ");\n"
327+bcc i (BASETOP n) = indent i ++ "BASETOP(" ++ show n ++ ");\n"
328+bcc i STOREOLD = indent i ++ "STOREOLD;\n"
329+bcc i (OP l fn args) = indent i ++ doOp (creg l ++ " = ") fn args ++ ";\n"
330+bcc i (FOREIGNCALL l rty (FStr fn@('&':name)) [])
331+ = indent i ++
332+ c_irts (toFType rty) (creg l ++ " = ") fn ++ ";\n"
333+bcc i (FOREIGNCALL l rty (FStr fn) (x:xs)) | fn == "%wrapper"
334+ = indent i ++
335+ c_irts (toFType rty) (creg l ++ " = ")
436336 ("_idris_get_wrapper(" ++ creg (snd x) ++ ")") ++ ";\n"
437− bcc zs
438−bcc ((FOREIGNCALL l rty (FStr fn) (x:xs)):zs) | fn == "%dynamic"
439− = do
440− i <- get
441− tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ")
337+bcc i (FOREIGNCALL l rty (FStr fn) (x:xs)) | fn == "%dynamic"
338+ = indent i ++ c_irts (toFType rty) (creg l ++ " = ")
442339 ("(*(" ++ cFnSig "" rty xs ++ ") GETPTR(" ++ creg (snd x) ++ "))" ++
443340 "(" ++ showSep "," (map fcall xs) ++ ")") ++ ";\n"
444− bcc zs
445−bcc ((FOREIGNCALL l rty (FStr fn) args):xs) = do
446− i <- get
447− tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ")
448− (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"
449− bcc xs
450−bcc ((FOREIGNCALL l rty _ args):_) = error "Foreign Function calls cannot be partially applied, without being inlined."
451−bcc ((NULL r):xs) = do
452− i <- get
453− tell $ indent (level i) ++ creg r ++ " = NULL;\n" -- clear, so it'll be GCed
454− bcc xs
455−bcc ((ERROR str):xs) = do
456− i <- get
457− tell $ indent (level i) ++ "fprintf(stderr, "
458− ++ show str ++ "); fprintf(stderr, \"\\n\"); exit(-1);\n"
459− bcc xs
341+bcc i (FOREIGNCALL l rty (FStr fn) args)
342+ = indent i ++
343+ c_irts (toFType rty) (creg l ++ " = ")
344+ (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"
345+bcc i (FOREIGNCALL l rty _ args) = error "Foreign Function calls cannot be partially applied, without being inlined."
346+bcc i (NULL r) = indent i ++ creg r ++ " = NULL;\n" -- clear, so it'll be GCed
347+bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); fprintf(stderr, \"\\n\"); exit(-1);\n"
460348-- bcc i c = error (show c) -- indent i ++ "// not done yet\n"
461349
462−getBC code xs = do
463− i <- get
464− let (a, s, w) = runRWS (bcc code) 0 (i { level = level i + 1 })
465− return w
466−
467350fcall (t, arg) = irts_c (toFType t) (creg arg)
468351-- Deconstruct the Foreign type in the defunctionalised expression and build
469352-- a foreign type description for c_irts and irts_c
src/IRTS/Compiler.hs+2
@@ -63,6 +63,8 @@ compile codegen f mtm = do
6363 Nothing -> []
6464 Just t -> freeNames t
6565
66+ logCodeGen 1 "Running Erasure Analysis"
67+ iReport 3 "Running Erasure Analysis"
6668 reachableNames <- performUsageAnalysis
6769 (rootNames ++ getExpNames exports)
6870 maindef <- case mtm of
src/Idris/Core/Binary.hs+4−2
@@ -16,6 +16,8 @@ import Control.Applicative ((<$>), (<*>))
1616import Control.DeepSeq (($!!))
1717import Control.Monad (liftM2)
1818import Data.Binary
19+import Data.Binary.Get
20+import Data.Binary.Put
1921import qualified Data.Text as T
2022import qualified Data.Text.Encoding as E
2123import Data.Vector.Binary
@@ -400,7 +402,7 @@ instance Binary Const where
400402 BI x1 -> do putWord8 1
401403 put x1
402404 Fl x1 -> do putWord8 2
403− put x1
405+ putDoublele x1
404406 Ch x1 -> do putWord8 3
405407 put x1
406408 Str x1 -> do putWord8 4
@@ -427,7 +429,7 @@ instance Binary Const where
427429 return (I x1)
428430 1 -> do x1 <- get
429431 return (BI x1)
430− 2 -> do x1 <- get
432+ 2 -> do x1 <- getDoublele
431433 return (Fl x1)
432434 3 -> do x1 <- get
433435 return (Ch x1)
src/Idris/DeepSeq.hs−14
@@ -29,20 +29,6 @@ import Control.DeepSeq
2929import Network.Socket (PortNumber)
3030
3131-- These types don't have Generic instances
32−instance NFData CT.Options where
33− rnf (CT.Options x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
34−
35−instance NFData CT.ListType where
36− rnf (CT.Bullet c) = rnf c `seq` ()
37− rnf (CT.Numbered nw i) = rnf nw `seq` rnf i `seq` ()
38−
39−instance NFData CT.CodeAttr where
40− rnf (CT.CodeAttr a b) = rnf a `seq` rnf b `seq` ()
41−
42−instance NFData CT.NumWrapper where
43− rnf CT.PeriodFollowing = ()
44− rnf CT.ParenFollowing = ()
45−
4632instance NFData DynamicLib where
4733 rnf (Lib x _) = rnf x `seq` ()
4834
src/Idris/IBC.hs+1−1
@@ -48,7 +48,7 @@ import System.Directory
4848import System.FilePath
4949
5050ibcVersion :: Word16
51−ibcVersion = 161
51+ibcVersion = 162
5252
5353-- | When IBC is being loaded - we'll load different things (and omit
5454-- different structures/definitions) depending on which phase we're in.