git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/src/IRTS/Exports.hs
110 lines 3.6 kB history raw
1{-# LANGUAGE PatternGuards #-}
2module IRTS.Exports(findExports, getExpNames) where
4import Idris.AbsSyntax
5import Idris.Core.TT
6import Idris.Core.CaseTree
7import Idris.Core.Evaluate
8import Idris.Error
9import IRTS.Lang
11import Data.Maybe
13findExports :: Idris [ExportIFace]
14findExports = do exps <- getExports
15 es <- mapM toIFace exps
16 logLvl 2 $ "Exporting " ++ show es
17 return es
19getExpNames :: [ExportIFace] -> [Name]
20getExpNames = concatMap expNames
22expNames :: ExportIFace -> [Name]
23expNames (Export _ _ es) = mapMaybe fnames es
24 where fnames (ExportData _) = Nothing
25 fnames (ExportFun n _ _ _) = Just n
27toIFace :: Name -> Idris ExportIFace
28toIFace n = do i <- getIState
29 let ctxt = tt_ctxt i
30 def <- case lookupDefExact n ctxt of
31 Just (CaseOp _ _ _ _ _ cs)
32 -> getExpList (snd (cases_compiletime cs))
33 Nothing -> ifail "Can't happen [toIFace]"
34 case lookupTyExact n ctxt of
35 Just ty -> toIFaceTyVal ty def
36 Nothing -> ifail "Can't happen [toIFace]"
37 where
38 getExpList (STerm t) = return t
39 getExpList _ = ifail "Badly formed export list"
41toIFaceTyVal :: Type -> Term -> Idris ExportIFace
42toIFaceTyVal ty tm
43 | (P _ exp _, [P _ ffi _, Constant (Str hdr), _]) <- unApply ty
44 = do tm' <- toIFaceVal tm
45 return $ Export ffi hdr tm'
47toIFaceVal :: Term -> Idris [Export]
48toIFaceVal tm
49 | (P _ end _, _) <- unApply tm,
50 end == sNS (sUN "End") ["FFI_Export"] = return []
51 | (P _ fun _, [_,_,_,_,(P _ fn _),extnm,prf,rest]) <- unApply tm,
52 fun == sNS (sUN "Fun") ["FFI_Export"]
53 = do rest' <- toIFaceVal rest
54 return $
55 ExportFun fn (toFDesc extnm) (toFDescRet prf) (toFDescArgs prf)
56 : rest'
57 | (P _ dat _, [_,_,_,_,d,rest]) <- unApply tm,
58 dat == sNS (sUN "Data") ["FFI_Export"]
59 = do rest' <- toIFaceVal rest
60 return $ ExportData (toFDesc d) : rest'
61 | otherwise = ifail $ "Badly formed export list " ++ show tm
63toFDesc :: Term -> FDesc
64toFDesc (Constant (Str str)) = FStr str
65toFDesc tm
66 | (P _ n _, []) <- unApply tm = FCon (deNS n)
67 | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDesc as)
68toFDesc _ = FUnknown
70toFDescRet :: Term -> FDesc
71toFDescRet tm
72 | (P _ ret _, [_,_,_,b]) <- unApply tm,
73 ret == sNS (sUN "FFI_Ret") ["FFI_Export"]
74 = toFDescBase b
75 | (P _ io _, [_,_,_,b]) <- unApply tm,
76 io == sNS (sUN "FFI_IO") ["FFI_Export"]
77 = FIO $ toFDescBase b
78 | (P _ fun _, [_,_,_,_,_,t]) <- unApply tm,
79 fun == sNS (sUN "FFI_Fun") ["FFI_Export"]
80 = toFDescRet t
81 | otherwise = error "Badly formed export proof"
83toFDescBase :: Term -> FDesc
84toFDescBase tm
85 | (P _ prim _, [_, _, _, pdesc]) <- unApply tm,
86 prim == sNS (sUN "FFI_Prim") ["FFI_Export"]
87 = toFDescPrim pdesc
88 | (P _ prim _, [_, _, _, ddesc, _]) <- unApply tm,
89 prim == sNS (sUN "FFI_ExpType") ["FFI_Export"]
90 = toFDescPrim ddesc
91 | otherwise = error "Badly formed export type"
93toFDescArgs :: Term -> [FDesc]
94toFDescArgs tm
95 | (P _ fun _, [_,_,_,_,b,t]) <- unApply tm,
96 fun == sNS (sUN "FFI_Fun") ["FFI_Export"]
97 = toFDescBase b : toFDescArgs t
98 | otherwise = []
100toFDescPrim (Constant (Str str)) = FStr str
101toFDescPrim tm
102 | (P _ n _, []) <- unApply tm = FCon (deNS n)
103 | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDescPrim as)
104toFDescPrim _ = FUnknown
106deNS (NS n _) = n
107deNS n = n