@@ -1,9 +1,103 @@
1+{-# LANGUAGE PatternGuards #-}
12module IRTS.Exports(findExports) where
23
34import Idris.AbsSyntax
5+import Idris.Core.TT
6+import Idris.Core.CaseTree
7+import Idris.Core.Evaluate
8+import Idris.Error
49import IRTS.Lang
510
611findExports :: Idris [ExportIFace]
712findExports = do exps <- getExports
8− return []
13+ es <- mapM toIFace exps
14+ logLvl 2 $ "Exporting " ++ show es
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+
9103