git.iko.soy/Idris-dev
on aa7262e help sign in
Idris-dev/src/IRTS/Lang.hs
215 lines 9.0 kB history raw
1module IRTS.Lang where
3import Core.TT
4import Control.Monad.State hiding(lift)
5import Data.List
6import Debug.Trace
8data LVar = Loc Int | Glob Name
9 deriving (Show, Eq)
11data LExp = LV LVar
12 | LApp Bool LExp [LExp] -- True = tail call
13 | LLazyApp Name [LExp] -- True = tail call
14 | LLazyExp LExp
15 | LForce LExp -- make sure Exp is evaluted
16 | LLet Name LExp LExp -- name just for pretty printing
17 | LLam [Name] LExp -- lambda, lifted out before compiling
18 | LProj LExp Int -- projection
19 | LCon Int Name [LExp]
20 | LCase LExp [LAlt]
21 | LConst Const
22 | LForeign FLang FType String [(FType, LExp)]
23 | LOp PrimFn [LExp]
24 | LNothing
25 | LError String
26 deriving Eq
28-- Primitive operators. Backends are not *required* to implement all
29-- of these, but should report an error if they are unable
31data PrimFn = LPlus | LMinus | LTimes | LDiv | LMod
32 | LEq | LLt | LLe | LGt | LGe
33 | LFPlus | LFMinus | LFTimes | LFDiv
34 | LFEq | LFLt | LFLe | LFGt | LFGe
35 | LBPlus | LBMinus | LBTimes | LBDiv | LBMod
36 | LBEq | LBLt | LBLe | LBGt | LBGe
37 | LStrConcat | LStrLt | LStrEq | LStrLen
38 | LIntFloat | LFloatInt | LIntStr | LStrInt | LFloatStr | LStrFloat
39 | LIntBig | LBigInt | LStrBig | LBigStr
40 | LPrintNum | LPrintStr | LReadStr
42 | LFExp | LFLog | LFSin | LFCos | LFTan | LFASin | LFACos | LFATan
43 | LFSqrt | LFFloor | LFCeil
45 | LStrHead | LStrTail | LStrCons | LStrIndex | LStrRev
46 | LStdIn | LStdOut | LStdErr
48 | LFork
49 | LPar -- evaluate argument anywhere, possibly on another
50 -- core or another machine. 'id' is a valid implementation
51 | LVMPtr
52 | LNoOp
53 deriving (Show, Eq)
55-- Supported target languages for foreign calls
57data FLang = LANG_C
58 deriving (Show, Eq)
60data FType = FInt | FChar | FString | FUnit | FPtr | FDouble | FAny
61 deriving (Show, Eq)
63data LAlt = LConCase Int Name [Name] LExp
64 | LConstCase Const LExp
65 | LDefaultCase LExp
66 deriving (Show, Eq)
68data LDecl = LFun Name [Name] LExp -- name, arg names, definition, inlinable
69 | LConstructor Name Int Int -- constructor name, tag, arity
70 deriving (Show, Eq)
72type LDefs = Ctxt LDecl
74addTags :: Int -> [(Name, LDecl)] -> (Int, [(Name, LDecl)])
75addTags i ds = tag i ds []
76 where tag i ((n, LConstructor n' (-1) a) : as) acc
77 = tag (i + 1) as ((n, LConstructor n' i a) : acc)
78 tag i ((n, LConstructor n' t a) : as) acc
79 = tag i as ((n, LConstructor n' t a) : acc)
80 tag i (x : as) acc = tag i as (x : acc)
81 tag i [] acc = (i, reverse acc)
83data LiftState = LS Name Int [(Name, LDecl)]
85lname (NS n x) i = NS (lname n i) x
86lname (UN n) i = MN i n
87lname x i = MN i (show x)
89liftAll :: [(Name, LDecl)] -> [(Name, LDecl)]
90liftAll xs = concatMap (\ (x, d) -> lambdaLift x d) xs
92lambdaLift :: Name -> LDecl -> [(Name, LDecl)]
93lambdaLift n (LFun _ args e)
94 = let (e', (LS _ _ decls)) = runState (lift args e) (LS n 0 []) in
95 (n, LFun n args e') : decls
96lambdaLift n x = [(n, x)]
98getNextName :: State LiftState Name
99getNextName = do LS n i ds <- get
100 put (LS n (i + 1) ds)
101 return (lname n i)
103addFn :: Name -> LDecl -> State LiftState ()
104addFn fn d = do LS n i ds <- get
105 put (LS n i ((fn, d) : ds))
107lift :: [Name] -> LExp -> State LiftState LExp
108lift env (LV v) = return (LV v) -- Lifting happens before these can exist...
109lift env (LApp tc (LV (Glob n)) args) = do args' <- mapM (lift env) args
110 return (LApp tc (LV (Glob n)) args')
111lift env (LApp tc f args) = do f' <- lift env f
112 fn <- getNextName
113 addFn fn (LFun fn env f')
114 args' <- mapM (lift env) args
115 return (LApp tc (LV (Glob fn)) (map (LV . Glob) env ++ args'))
116lift env (LLazyApp n args) = do args' <- mapM (lift env) args
117 return (LLazyApp n args')
118lift env (LLazyExp (LConst c)) = return (LConst c)
119lift env (LLazyExp e) = do e' <- lift env e
120 let usedArgs = nub $ usedIn env e'
121 fn <- getNextName
122 addFn fn (LFun fn usedArgs e')
123 return (LLazyApp fn (map (LV . Glob) usedArgs))
124lift env (LForce e) = do e' <- lift env e
125 return (LForce e')
126lift env (LLet n v e) = do v' <- lift env v
127 e' <- lift (env ++ [n]) e
128 return (LLet n v' e')
129lift env (LLam args e) = do e' <- lift (env ++ args) e
130 let usedArgs = nub $ usedIn env e'
131 fn <- getNextName
132 addFn fn (LFun fn (usedArgs ++ args) e')
133 return (LApp False (LV (Glob fn)) (map (LV . Glob) usedArgs))
134lift env (LProj t i) = do t' <- lift env t
135 return (LProj t' i)
136lift env (LCon i n args) = do args' <- mapM (lift env) args
137 return (LCon i n args')
138lift env (LCase e alts) = do alts' <- mapM liftA alts
139 e' <- lift env e
140 return (LCase e' alts')
141 where
142 liftA (LConCase i n args e) = do e' <- lift (env ++ args) e
143 return (LConCase i n args e')
144 liftA (LConstCase c e) = do e' <- lift env e
145 return (LConstCase c e')
146 liftA (LDefaultCase e) = do e' <- lift env e
147 return (LDefaultCase e')
148lift env (LConst c) = return (LConst c)
149lift env (LForeign l t s args) = do args' <- mapM (liftF env) args
150 return (LForeign l t s args')
151 where
152 liftF env (t, e) = do e' <- lift env e
153 return (t, e')
154lift env (LOp f args) = do args' <- mapM (lift env) args
155 return (LOp f args')
156lift env (LError str) = return $ LError str
157lift env LNothing = return $ LNothing
159-- Return variables in list which are used in the expression
161usedArg env n | n `elem` env = [n]
162 | otherwise = []
164usedIn :: [Name] -> LExp -> [Name]
165usedIn env (LV (Glob n)) = usedArg env n
166usedIn env (LApp _ e args) = usedIn env e ++ concatMap (usedIn env) args
167usedIn env (LLazyApp n args) = concatMap (usedIn env) args ++ usedArg env n
168usedIn env (LLazyExp e) = usedIn env e
169usedIn env (LForce e) = usedIn env e
170usedIn env (LLet n v e) = usedIn env v ++ usedIn (env \\ [n]) e
171usedIn env (LLam ns e) = usedIn (env \\ ns) e
172usedIn env (LCon i n args) = concatMap (usedIn env) args
173usedIn env (LProj t i) = usedIn env t
174usedIn env (LCase e alts) = usedIn env e ++ concatMap (usedInA env) alts
175 where usedInA env (LConCase i n ns e) = usedIn env e
176 usedInA env (LConstCase c e) = usedIn env e
177 usedInA env (LDefaultCase e) = usedIn env e
178usedIn env (LForeign _ _ _ args) = concatMap (usedIn env) (map snd args)
179usedIn env (LOp f args) = concatMap (usedIn env) args
180usedIn env _ = []
182instance Show LExp where
183 show e = show' [] e where
184 show' env (LV (Loc i)) = env!!i
185 show' env (LV (Glob n)) = show n
186 show' env (LLazyApp e args) = show e ++ "|(" ++
187 showSep ", " (map (show' env) args) ++")"
188 show' env (LApp _ e args) = show' env e ++ "(" ++
189 showSep ", " (map (show' env) args) ++")"
190 show' env (LLazyExp e) = "%lazy(" ++ show' env e ++ ")"
191 show' env (LForce e) = "%force(" ++ show' env e ++ ")"
192 show' env (LLet n v e) = "let " ++ show n ++ " = " ++ show' env v ++ " in " ++
193 show' (env ++ [show n]) e
194 show' env (LLam args e) = "\\ " ++ showSep "," (map show args) ++ " => " ++
195 show' (env ++ (map show args)) e
196 show' env (LProj t i) = show t ++ "!" ++ show i
197 show' env (LCon i n args) = show n ++ ")" ++ showSep ", " (map (show' env) args) ++ ")"
198 show' env (LCase e alts) = "case " ++ show' env e ++ " of {\n\t" ++
199 showSep "\n\t| " (map (showAlt env) alts)
200 show' env (LConst c) = show c
201 show' env (LForeign lang ty n args)
202 = "foreign " ++ n ++ "(" ++ showSep ", " (map (show' env) (map snd args)) ++ ")"
203 show' env (LOp f args) = show f ++ "(" ++ showSep ", " (map (show' env) args) ++ ")"
204 show' env (LError str) = "error " ++ show str
205 show' env LNothing = "____"
207 showAlt env (LConCase _ n args e)
208 = show n ++ "(" ++ showSep ", " (map show args) ++ ") => "
209 ++ show' env e
210 showAlt env (LConstCase c e) = show c ++ " => " ++ show' env e
211 showAlt env (LDefaultCase e) = "_ => " ++ show' env e