git.iko.soy/Idris-dev
on master help sign in
Pass export lists to CodegenInfo
4313defEdwin Brady
libs/prelude/IO.idr+13−10
compare with master
unifiedsplit
@@ -21,7 +21,9 @@ abstract WorldRes : Type -> Type
21WorldRes x = x
21WorldRes x = x
22
22
23record FFI : Type where
23record FFI : Type where
24− MkFFI : (ffi_types : Type -> Type) -> (ffi_fn : Type) -> FFI
24+ MkFFI : (ffi_types : Type -> Type) ->
25+ (ffi_fn : Type) ->
26+ (ffi_data : Type) -> FFI
25
27
26abstract
28abstract
27data IO' : (lang : FFI) -> Type -> Type where
29data IO' : (lang : FFI) -> Type -> Type where
@@ -143,7 +145,7 @@ data C_Types : Type -> Type where
143 C_IntT : C_IntTypes i -> C_Types i
145 C_IntT : C_IntTypes i -> C_Types i
144
146
145FFI_C : FFI
147FFI_C : FFI
146−FFI_C = MkFFI C_Types String
148+FFI_C = MkFFI C_Types String String
147
149
148IO : Type -> Type
150IO : Type -> Type
149IO = IO' FFI_C
151IO = IO' FFI_C
@@ -194,7 +196,7 @@ mutual
194%used MkJsFn x
196%used MkJsFn x
195
197
196FFI_JS : FFI
198FFI_JS : FFI
197−FFI_JS = MkFFI JS_Types String
199+FFI_JS = MkFFI JS_Types String String
198
200
199JS_IO : Type -> Type
201JS_IO : Type -> Type
200JS_IO = IO' FFI_JS
202JS_IO = IO' FFI_JS
@@ -205,11 +207,11 @@ JS_IO = IO' FFI_JS
205namespace FFI_Export
207namespace FFI_Export
206-- It's just like Data.List.Elem, but we don't need all the other stuff
208-- It's just like Data.List.Elem, but we don't need all the other stuff
207-- that comes with it, just a proof that a data type is defined.
209-- that comes with it, just a proof that a data type is defined.
208− data DataDefined : Type -> List (Type, String) -> String -> Type where
210+ data DataDefined : Type -> List (Type, s) -> s -> Type where
209 DHere : DataDefined x ((x, t) :: xs) t
211 DHere : DataDefined x ((x, t) :: xs) t
210 DThere : DataDefined x xs t -> DataDefined x (y :: xs) t
212 DThere : DataDefined x xs t -> DataDefined x (y :: xs) t
211
213
212− data FFI_Base : FFI -> List (Type, String) -> Type -> Type where
214+ data FFI_Base : (f : FFI) -> List (Type, ffi_data f) -> Type -> Type where
213 FFI_ExpType : (def : DataDefined t xs n) -> FFI_Base f xs t
215 FFI_ExpType : (def : DataDefined t xs n) -> FFI_Base f xs t
214 FFI_Prim : (prim : ffi_types f t) -> FFI_Base f xs t
216 FFI_Prim : (prim : ffi_types f t) -> FFI_Base f xs t
215
217
@@ -217,19 +219,20 @@ namespace FFI_Export
217 %used FFI_ExpType def
219 %used FFI_ExpType def
218 %used FFI_Prim prim
220 %used FFI_Prim prim
219
221
220− data FFI_Exportable : FFI -> List (Type, String) -> Type -> Type where
222+ data FFI_Exportable : (f : FFI) -> List (Type, ffi_data f) -> Type -> Type where
221 FFI_IO : (b : FFI_Base f xs t) -> FFI_Exportable f xs (IO t)
223 FFI_IO : (b : FFI_Base f xs t) -> FFI_Exportable f xs (IO t)
222− FFI_Fun : (b : FFI_Base f xs s) -> FFI_Exportable f xs t -> FFI_Exportable f xs (s -> t)
224+ FFI_Fun : (b : FFI_Base f xs s) -> (a : FFI_Exportable f xs t) -> FFI_Exportable f xs (s -> t)
223 FFI_Ret : (b : FFI_Base f xs t) -> FFI_Exportable f xs t
225 FFI_Ret : (b : FFI_Base f xs t) -> FFI_Exportable f xs t
224
226
225 %used FFI_IO b
227 %used FFI_IO b
226 %used FFI_Fun b
228 %used FFI_Fun b
229+ %used FFI_Fun a
227 %used FFI_Ret b
230 %used FFI_Ret b
228
231
229− data FFI_Export : FFI -> String -> List (Type, String) -> Type where
232+ data FFI_Export : (f : FFI) -> String -> List (Type, ffi_data f) -> Type where
230− Data : (x : Type) -> (n : String) ->
233+ Data : (x : Type) -> (n : ffi_data f) ->
231 (es : FFI_Export f h ((x, n) :: xs)) -> FFI_Export f h xs
234 (es : FFI_Export f h ((x, n) :: xs)) -> FFI_Export f h xs
232− Fun : (fn : t) -> (n : String) -> {auto prf : FFI_Exportable f xs t} ->
235+ Fun : (fn : t) -> (n : ffi_fn f) -> {auto prf : FFI_Exportable f xs t} ->
233 (es : FFI_Export f h xs) -> FFI_Export f h xs
236 (es : FFI_Export f h xs) -> FFI_Export f h xs
234 End : FFI_Export f h xs
237 End : FFI_Export f h xs
235
238
src/IRTS/Exports.hs+95−1
@@ -1,9 +1,103 @@
1+{-# LANGUAGE PatternGuards #-}
1module IRTS.Exports(findExports) where
2module IRTS.Exports(findExports) where
2
3
3import Idris.AbsSyntax
4import Idris.AbsSyntax
5+import Idris.Core.TT
6+import Idris.Core.CaseTree
7+import Idris.Core.Evaluate
8+import Idris.Error
4import IRTS.Lang
9import IRTS.Lang
5
10
6findExports :: Idris [ExportIFace]
11findExports :: Idris [ExportIFace]
7findExports = do exps <- getExports
12findExports = do exps <- getExports
13+ es <- mapM toIFace exps
14+ logLvl 2 $ "Exporting " ++ show es
8− return []
15+ return es
16+
17+toIFace :: Name -> Idris ExportIFace
18+toIFace n = do i <- getIState
19+ let ctxt = tt_ctxt i
20+ def <- case lookupDefExact n ctxt of
21+ Just (CaseOp _ _ _ _ _ cs)
22+ -> getExpList (snd (cases_compiletime cs))
23+ Nothing -> ifail "Can't happen [toIFace]"
24+ case lookupTyExact n ctxt of
25+ Just ty -> toIFaceTyVal ty def
26+ Nothing -> ifail "Can't happen [toIFace]"
27+ where
28+ getExpList (STerm t) = return t
29+ getExpList _ = ifail "Badly formed export list"
30+
31+toIFaceTyVal :: Type -> Term -> Idris ExportIFace
32+toIFaceTyVal ty tm
33+ | (P _ exp _, [P _ ffi _, Constant (Str hdr), _]) <- unApply ty
34+ = do tm' <- toIFaceVal tm
35+ return $ Export ffi hdr tm'
36+
37+toIFaceVal :: Term -> Idris [Export]
38+toIFaceVal tm
39+ | (P _ end _, _) <- unApply tm,
40+ end == sNS (sUN "End") ["FFI_Export"] = return []
41+ | (P _ fun _, [_,_,_,_,(P _ fn _),extnm,prf,rest]) <- unApply tm,
42+ fun == sNS (sUN "Fun") ["FFI_Export"]
43+ = do rest' <- toIFaceVal rest
44+ return $
45+ ExportFun fn (toFDesc extnm) (toFDescRet prf) (toFDescArgs prf)
46+ : rest'
47+ | (P _ dat _, [_,_,_,_,d,rest]) <- unApply tm,
48+ dat == sNS (sUN "Data") ["FFI_Export"]
49+ = do rest' <- toIFaceVal rest
50+ return $ ExportData (toFDesc d) : rest'
51+ | otherwise = ifail $ "Badly formed export list " ++ show tm
52+
53+toFDesc :: Term -> FDesc
54+toFDesc (Constant (Str str)) = FStr str
55+toFDesc tm
56+ | (P _ n _, []) <- unApply tm = FCon (deNS n)
57+ | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDesc as)
58+toFDesc _ = FUnknown
59+
60+toFDescRet :: Term -> FDesc
61+toFDescRet tm
62+ | (P _ ret _, [_,_,_,b]) <- unApply tm,
63+ ret == sNS (sUN "FFI_Ret") ["FFI_Export"]
64+ = toFDescBase b
65+ | (P _ io _, [_,_,_,b]) <- unApply tm,
66+ io == sNS (sUN "FFI_IO") ["FFI_Export"]
67+ = toFDescBase b
68+ | (P _ fun _, [_,_,_,_,_,t]) <- unApply tm,
69+ fun == sNS (sUN "FFI_Fun") ["FFI_Export"]
70+ = toFDescRet t
71+ | otherwise = error "Badly formed export proof"
72+
73+toFDescBase :: Term -> FDesc
74+toFDescBase tm
75+ | (P _ prim _, [_, _, _, pdesc]) <- unApply tm,
76+ prim == sNS (sUN "FFI_Prim") ["FFI_Export"]
77+ = toFDescPrim pdesc
78+ | (P _ prim _, [_, _, _, ddesc, _]) <- unApply tm,
79+ prim == sNS (sUN "FFI_ExpType") ["FFI_Export"]
80+ = toFDescPrim ddesc
81+ | otherwise = error "Badly formed export type"
82+
83+toFDescArgs :: Term -> [FDesc]
84+toFDescArgs tm
85+ | (P _ io _, [_,_,_,b]) <- unApply tm,
86+ io == sNS (sUN "FFI_IO") ["FFI_Export"]
87+ = [FWorld] -- World, unused but needed explicitly as an argument
88+ | (P _ fun _, [_,_,_,_,b,t]) <- unApply tm,
89+ fun == sNS (sUN "FFI_Fun") ["FFI_Export"]
90+ = toFDescBase b : toFDescArgs t
91+ | otherwise = []
92+
93+toFDescPrim (Constant (Str str)) = FStr str
94+toFDescPrim tm
95+ | (P _ n _, []) <- unApply tm = FCon (deNS n)
96+ | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDescPrim as)
97+toFDescPrim _ = FUnknown
98+
99+deNS (NS n _) = n
100+deNS n = n
101+
102+
9
103
src/IRTS/Lang.hs+2−2
@@ -40,11 +40,11 @@ data LExp = LV LVar
40data FDesc = FCon Name
40data FDesc = FCon Name
41 | FStr String
41 | FStr String
42 | FUnknown
42 | FUnknown
43+ | FWorld
43 | FApp Name [FDesc]
44 | FApp Name [FDesc]
44 deriving (Show, Eq)
45 deriving (Show, Eq)
45
46
46−data Export = ExportData Name -- Idris name
47− FDesc -- Exported function descriptor (usually string)
47+data Export = ExportData FDesc -- Exported data descriptor (usually string)
48 | ExportFun Name -- Idris name
48 | ExportFun Name -- Idris name
49 FDesc -- Exported function descriptor
49 FDesc -- Exported function descriptor
50 FDesc -- Return type descriptor
50 FDesc -- Return type descriptor
src/Idris/Erasure.hs+1−1
@@ -201,7 +201,7 @@ buildDepMap ci used ctx startNames = addPostulates used $
201 [(sUN "run__IO", Result), (sUN "run__IO", Arg 1)]
201 [(sUN "run__IO", Result), (sUN "run__IO", Arg 1)]
202
202
203 -- Explicit usage declarations from a %used pragma
203 -- Explicit usage declarations from a %used pragma
204− , trace (show used) $ map (\(n, i) -> (n, Arg i)) used
204+ , map (\(n, i) -> (n, Arg i)) used
205
205
206 -- MkIO is read by run__IO,
206 -- MkIO is read by run__IO,
207 -- but this cannot be observed in the source code of programs.
207 -- but this cannot be observed in the source code of programs.