git.iko.soy/Idris-dev
on 22b4dc4 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
320 lines 11 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances #-}
4module Idris.AbsSyntax where
6import Core.TT
7import Core.Evaluate
9import Control.Monad.State
10import Data.List
11import Data.Char
13data IOption = IOption { opt_logLevel :: Int }
14 deriving (Show, Eq)
16defaultOpts = IOption 0
18-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
19-- without typechecking).
20-- This will include all the functions and data declarations, plus fixity declarations
21-- and syntax macros.
23data IState = IState { tt_ctxt :: Context,
24 idris_infixes :: [FixDecl],
25 idris_implicits :: Ctxt ([Name], Int), -- implicits, arity
26 idris_log :: String,
27 idris_options :: IOption
28 }
30idrisInit = IState emptyContext [] emptyContext "" defaultOpts
32-- The monad for the main REPL - reading and processing files and updating
33-- global state (hence the IO inner monad).
34type Idris a = StateT IState IO a
36getContext :: Idris Context
37getContext = do i <- get; return (tt_ctxt i)
39setContext :: Context -> Idris ()
40setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
42updateContext :: (Context -> Context) -> Idris ()
43updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
45iputStrLn :: String -> Idris ()
46iputStrLn = lift.putStrLn
48tclift :: Show a => TC a -> Idris a
49tclift tc = case tc of
50 OK v -> return v
51 err -> fail (show err)
53setLogLevel :: Int -> Idris ()
54setLogLevel l = do i <- get
55 let opts = idris_options i
56 let opt' = opts { opt_logLevel = l }
57 put (i { idris_options = opt' } )
59logLevel :: Idris Int
60logLevel = do i <- get
61 return (opt_logLevel (idris_options i))
63logLvl :: Int -> String -> Idris ()
64logLvl l str = do i <- get
65 let lvl = opt_logLevel (idris_options i)
66 when (lvl >= l)
67 $ do lift (putStrLn str)
68 put (i { idris_log = idris_log i ++ str ++ "\n" } )
70iLOG :: String -> Idris ()
71iLOG = logLvl 1
73-- Taken from the library source code - for ghc 6.12/7 compatibility
74liftCatch :: (m (a,s) -> (e -> m (a,s)) -> m (a,s)) ->
75 StateT s m a -> (e -> StateT s m a) -> StateT s m a
76liftCatch catchError m h =
77 StateT $ \s -> runStateT m s `catchError` \e -> runStateT (h e) s
79idrisCatch :: Idris a -> (IOError -> Idris a) -> Idris a
80idrisCatch op handler = liftCatch catch op handler
82-- Commands in the REPL
84data Command = Quit | Help | Eval PTerm
85 | TTShell
86 | NOP
88-- Parsed declarations
90data Fixity = Infixl { prec :: Int }
91 | Infixr { prec :: Int }
92 | InfixN { prec :: Int }
93 deriving Eq
95instance Show Fixity where
96 show (Infixl i) = "infixl " ++ show i
97 show (Infixr i) = "infixr " ++ show i
98 show (InfixN i) = "infix " ++ show i
100data FixDecl = Fix Fixity String
101 deriving (Show, Eq)
103instance Ord FixDecl where
104 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
106data Plicity = Imp | Exp deriving Show
108data PDecl' t = PFix Fixity [String] -- fixity declaration
109 | PTy Name t -- type declaration
110 | PClauses Name [PClause' t] -- pattern clause
111 | PData (PData' t) -- data declaration
112 deriving Functor
114data PClause' t = PClause Name t t
115 deriving Functor
117data PData' t = PDatadecl { d_name :: Name,
118 d_tcon :: t,
119 d_cons :: [(Name, t)] }
120 deriving Functor
122-- Handy to get a free function for applying PTerm -> PTerm functions
123-- across a program, by deriving Functor
125type PDecl = PDecl' PTerm
126type PData = PData' PTerm
127type PClause = PClause' PTerm
128-- High level language terms
130data PTerm = PQuote Raw
131 | PRef Name
132 | PLam Name PTerm PTerm
133 | PPi Plicity Name PTerm PTerm
134 | PApp PTerm [(Name, PTerm)] [PTerm]
135 | PHidden PTerm -- irrelevant or hidden pattern
136 | PSet
137 | Placeholder
139--- Pretty printing declarations and terms
141instance Show PTerm where
142 show tm = showImp False tm
144instance Show PDecl where
145 show (PFix f ops) = show f ++ " " ++ showSep ", " ops
146 show (PTy n ty) = show n ++ " : " ++ show ty
147 show (PClauses n c) = showSep "\n" (map show c)
148 show (PData d) = show d
150instance Show PClause where
151 show c = showCImp False c
153instance Show PData where
154 show d = showDImp False d
156showCImp :: Bool -> PClause -> String
157showCImp impl (PClause n l r) = showImp impl l ++ " = " ++ showImp impl r
159showDImp :: Bool -> PData -> String
160showDImp impl (PDatadecl n ty cons)
161 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
162 ++ showSep "\n\t| "
163 (map (\ (n, t) -> show n ++ " : " ++ showImp impl t) cons)
165showImp :: Bool -> PTerm -> String
166showImp impl tm = se 10 tm where
167 se p (PQuote r) = "![" ++ show r ++ "]"
168 se p (PRef n) = show n
169 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
170 se p (PPi Exp n ty sc)
171 | n `elem` allNamesIn sc = bracket p 2 $
172 "(" ++ show n ++ " : " ++ se 10 ty ++
173 ") -> " ++ se 10 sc
174 | otherwise = bracket p 2 $ se 10 ty ++ " -> " ++ se 10 sc
175 se p (PPi Imp n ty sc)
176 | impl = bracket p 2 $ "{" ++ show n ++ " : " ++ se 10 ty ++
177 "} -> " ++ se 10 sc
178 | otherwise = se 10 sc
179 se p (PApp (PRef f) _ [])
180 | not impl = show f
181 se p (PApp (PRef op@(UN [f:_])) _ [l, r])
182 | not impl && not (isAlpha f)
183 = bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 1 r
184 se p (PApp f imps args)
185 = bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")
186 ++ concatMap seArg args
187 se p (PHidden tm) = "." ++ se 0 tm
188 se p PSet = "Set"
189 se p Placeholder = "_"
191 seArg arg = " " ++ se 0 arg
192 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
194 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
195 | otherwise = str
197allNamesIn :: PTerm -> [Name]
198allNamesIn tm = nub $ ni [] tm
199 where
200 ni env (PRef n)
201 | not (n `elem` env) = [n]
202 ni env (PApp f is es) = ni env f ++ concatMap (ni env) (map snd is) ++
203 concatMap (ni env) es
204 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
205 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
206 ni env (PHidden tm) = ni env tm
207 ni env _ = []
209namesIn :: IState -> PTerm -> [Name]
210namesIn ist tm = nub $ ni [] tm
211 where
212 ni env (PRef n)
213 | not (n `elem` env)
214 = case lookupCtxt n (idris_implicits ist) of
215 Nothing -> [n]
216 _ -> []
217 ni env (PApp f is es) = ni env f ++ concatMap (ni env) (map snd is) ++
218 concatMap (ni env) es
219 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
220 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
221 ni env (PHidden tm) = ni env tm
222 ni env _ = []
224-- For inferring types of things
226inferTy = MN 0 "__Infer"
227inferCon = MN 0 "__infer"
228inferDecl = PDatadecl inferTy
229 PSet
230 [(inferCon, PPi Imp (MN 0 "A") PSet (
231 PPi Exp (MN 0 "a") (PRef (MN 0 "A"))
232 (PRef inferTy)))]
234infTerm t = PApp (PRef inferCon) [(MN 0 "A", Placeholder)] [t]
235infP = P (TCon 0) inferTy (Set 0)
237getInferTerm, getInferType :: Term -> Term
238getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
239getInferTerm (App (App _ _) tm) = tm
240getInferTerm tm = error ("getInferTerm " ++ show tm)
242getInferType (Bind n b sc) = Bind n b $ getInferType sc
243getInferType (App (App _ ty) _) = ty
246-- Dealing with implicit arguments
248-- Add implicit Pi bindings for any names in the term which appear in an
249-- argument position.
251implicitise :: IState -> PTerm -> (PTerm, ([Name], Int))
252implicitise ist tm
253 = let (declimps, a, ns) = execState (imps [] tm) ([], 0, []) in
254 (pibind ns tm, (ns ++ reverse declimps, a))
255 where
256 imps env (PApp f is es)
257 = do (decls, a, ns) <- get
258 let isn = concatMap (namesIn ist) (map snd is)
259 let esn = concatMap (namesIn ist) es
260 put (decls, a, nub (ns ++ ((isn ++ esn) \\ env)))
261 imps env (PPi Imp n ty sc)
262 = do imps env ty
263 (impdecls, a, ns) <- get
264 put (n:impdecls, a+1, ns)
265 imps (n:env) sc
266 imps env (PPi Exp n ty sc)
267 = do imps env ty
268 (impdecls, a, ns) <- get
269 put (impdecls, a+1, ns)
270 imps (n:env) sc
271 imps env (PLam n ty sc)
272 = do imps env ty
273 imps (n:env) sc
274 imps env (PHidden tm) = imps env tm
275 imps env _ = return ()
277 pibind [] sc = sc
278 pibind (n:ns) sc = PPi Imp n Placeholder (pibind ns sc)
280addImpl :: IState -> PTerm -> PTerm
281addImpl ist ptm = ai [] ptm
282 where
283 ai env (PRef f) = aiFn env (PRef f) [] []
284 ai env (PApp (PRef f) is es)
285 = let is' = map (\ (n, tm) -> (n, ai env tm)) is
286 es' = map (ai env) es in
287 aiFn env (PRef f) is' es'
288 ai env (PApp f is es) = let f' = ai env f
289 is' = map (\ (n, tm) -> (n, ai env tm)) is
290 es' = map (ai env) es in
291 aiFn env f' is' es'
292 ai env (PLam n ty sc) = let ty' = ai env ty
293 sc' = ai (n:env) sc in
294 PLam n ty' sc'
295 ai env (PPi p n ty sc) = let ty' = ai env ty
296 sc' = ai (n:env) sc in
297 PPi p n ty' sc'
298 ai env (PHidden tm) = PHidden (ai env tm)
299 ai env tm = tm
301 aiFn env (PRef f) is es | not (f `elem` env)
302 = case lookupCtxt f (idris_implicits ist) of
303 Just (ns, a) -> pApp a (PRef f) (insertImpl ns is) es
304 Nothing -> pApp 1 (PRef f) is es
305 aiFn env f is es = pApp 1 f is es
307 pApp a f [] [] = f
308 pApp a f is es = let rest = drop a es in
309 appRest (PApp f is (take a es)) rest
311 appRest f [] = f
312 appRest f (a : as) = appRest (PApp f [] [a]) as
314 insertImpl [] given = []
315 insertImpl (n:ns) given
316 = case lookup n given of
317 Just val -> (n, val) : insertImpl ns given
318 Nothing -> (n, Placeholder) : insertImpl ns given