git.iko.soy/Idris-dev
on 7a30f10 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
281 lines 9.5 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 = Logging
14 deriving (Show, Eq)
16-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
17-- without typechecking).
18-- This will include all the functions and data declarations, plus fixity declarations
19-- and syntax macros.
21data IState = IState { tt_ctxt :: Context,
22 idris_infixes :: [FixDecl],
23 idris_implicits :: Ctxt [Name],
24 idris_log :: String,
25 idris_options :: [IOption]
26 }
28idrisInit = IState emptyContext [] emptyContext "" []
30-- The monad for the main REPL - reading and processing files and updating
31-- global state (hence the IO inner monad).
32type Idris a = StateT IState IO a
34getContext :: Idris Context
35getContext = do i <- get; return (tt_ctxt i)
37setContext :: Context -> Idris ()
38setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
40updateContext :: (Context -> Context) -> Idris ()
41updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
43iputStrLn :: String -> Idris ()
44iputStrLn = lift.putStrLn
46tclift :: Show a => TC a -> Idris a
47tclift tc = case tc of
48 OK v -> return v
49 err -> fail (show err)
51setOpt :: IOption -> Bool -> Idris ()
52setOpt o True = do i <- get
53 put (i { idris_options = nub (o : idris_options i) })
54setOpt o False = do i <- get
55 put (i { idris_options = idris_options i \\ [o] })
57iLOG :: String -> Idris ()
58iLOG str = do i <- get
59 when (Logging `elem` idris_options i)
60 $ do lift (putStrLn str)
61 put (i { idris_log = idris_log i ++ str ++ "\n" } )
63liftCatch :: (m (a,s) -> (e -> m (a,s)) -> m (a,s)) ->
64 StateT s m a -> (e -> StateT s m a) -> StateT s m a
65liftCatch catchError m h =
66 StateT $ \s -> runStateT m s `catchError` \e -> runStateT (h e) s
68idrisCatch :: Idris a -> (IOError -> Idris a) -> Idris a
69idrisCatch op handler = liftCatch catch op handler
71-- Commands in the REPL
73data Command = Quit | Help | Eval PTerm
74 | TTShell
75 | NOP
77-- Parsed declarations
79data Fixity = Infixl { prec :: Int }
80 | Infixr { prec :: Int }
81 | InfixN { prec :: Int }
82 deriving Eq
84instance Show Fixity where
85 show (Infixl i) = "infixl " ++ show i
86 show (Infixr i) = "infixr " ++ show i
87 show (InfixN i) = "infix " ++ show i
89data FixDecl = Fix Fixity String
90 deriving (Show, Eq)
92instance Ord FixDecl where
93 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
95data Plicity = Imp | Exp deriving Show
97data PDecl' t = PFix Fixity [String] -- fixity declaration
98 | PTy Name t -- type declaration
99 | PClauses [PClause' t] -- pattern clause
100 | PData (PData' t) -- data declaration
101 deriving Functor
103data PClause' t = PClause Name t t
104 deriving Functor
106data PData' t = PDatadecl { d_name :: Name,
107 d_tcon :: t,
108 d_cons :: [(Name, t)] }
109 deriving Functor
111-- Handy to get a free function for applying PTerm -> PTerm functions
112-- across a program, by deriving Functor
114type PDecl = PDecl' PTerm
115type PData = PData' PTerm
116type PClause = PClause' PTerm
117-- High level language terms
119data PTerm = PQuote Raw
120 | PRef Name
121 | PLam Name PTerm PTerm
122 | PPi Plicity Name PTerm PTerm
123 | PApp PTerm [(Name, PTerm)] [PTerm]
124 | PHidden PTerm -- irrelevant or hidden pattern
125 | PSet
126 | Placeholder
128--- Pretty printing declarations and terms
130instance Show PTerm where
131 show tm = showImp False tm
133instance Show PDecl where
134 show (PFix f ops) = show f ++ " " ++ showSep ", " ops
135 show (PTy n ty) = show n ++ " : " ++ show ty
136 show (PClauses c) = showSep "\n" (map show c)
137 show (PData d) = show d
139instance Show PClause where
140 show c = showCImp False c
142instance Show PData where
143 show d = showDImp False d
145showCImp :: Bool -> PClause -> String
146showCImp impl (PClause n l r) = showImp impl l ++ " = " ++ showImp impl r
148showDImp :: Bool -> PData -> String
149showDImp impl (PDatadecl n ty cons)
150 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
151 ++ showSep "\n\t| "
152 (map (\ (n, t) -> show n ++ " : " ++ showImp impl t) cons)
154showImp :: Bool -> PTerm -> String
155showImp impl tm = se 10 tm where
156 se p (PQuote r) = "![" ++ show r ++ "]"
157 se p (PRef n) = show n
158 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
159 se p (PPi Exp n ty sc)
160 | n `elem` allNamesIn sc = bracket p 2 $
161 "(" ++ show n ++ " : " ++ se 10 ty ++
162 ") -> " ++ se 10 sc
163 | otherwise = bracket p 2 $ se 10 ty ++ " -> " ++ se 10 sc
164 se p (PPi Imp n ty sc)
165 | impl = bracket p 2 $ "{" ++ show n ++ " : " ++ se 10 ty ++
166 "} -> " ++ se 10 sc
167 | otherwise = se 10 sc
168 se p (PApp (PRef f) _ [])
169 | not impl = show f
170 se p (PApp (PRef op@(UN [f:_])) _ [l, r])
171 | not impl && not (isAlpha f)
172 = bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 1 r
173 se p (PApp f imps args)
174 = bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")
175 ++ concatMap seArg args
176 se p (PHidden tm) = "." ++ se 0 tm
177 se p PSet = "Set"
178 se p Placeholder = "_"
180 seArg arg = " " ++ se 0 arg
181 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
183 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
184 | otherwise = str
186allNamesIn :: PTerm -> [Name]
187allNamesIn tm = nub $ ni [] tm
188 where
189 ni env (PRef n)
190 | not (n `elem` env) = [n]
191 ni env (PApp f is es) = ni env f ++ concatMap (ni env) (map snd is) ++
192 concatMap (ni env) es
193 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
194 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
195 ni env (PHidden tm) = ni env tm
196 ni env _ = []
198namesIn :: IState -> PTerm -> [Name]
199namesIn ist tm = nub $ ni [] tm
200 where
201 ni env (PRef n)
202 | not (n `elem` env)
203 = case lookupCtxt n (idris_implicits ist) of
204 Nothing -> [n]
205 _ -> []
206 ni env (PApp f is es) = ni env f ++ concatMap (ni env) (map snd is) ++
207 concatMap (ni env) es
208 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
209 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
210 ni env (PHidden tm) = ni env tm
211 ni env _ = []
213-- Dealing with implicit arguments
215-- Add implicit Pi bindings for any names in the term which appear in an
216-- argument position.
218implicitise :: IState -> PTerm -> (PTerm, [Name])
219implicitise ist tm
220 = let (declimps, ns) = execState (imps [] tm) ([], []) in
221 (pibind ns tm, ns ++ reverse declimps)
222 where
223 imps env (PApp f is es)
224 = do (decls, ns) <- get
225 let isn = concatMap (namesIn ist) (map snd is)
226 let esn = concatMap (namesIn ist) es
227 put (decls, nub (ns ++ ((isn ++ esn) \\ env)))
228 imps env (PPi Imp n ty sc)
229 = do imps env ty
230 (decls, ns) <- get
231 put (n:decls, ns)
232 imps (n:env) sc
233 imps env (PPi Exp n ty sc)
234 = do imps env ty
235 imps (n:env) sc
236 imps env (PLam n ty sc)
237 = do imps env ty
238 imps (n:env) sc
239 imps env (PHidden tm) = imps env tm
240 imps env _ = return ()
242 pibind [] sc = sc
243 pibind (n:ns) sc = PPi Imp n Placeholder (pibind ns sc)
245addImpl :: IState -> PTerm -> PTerm
246addImpl ist ptm = ai [] ptm
247 where
248 ai env (PRef f) = aiFn env (PRef f) [] []
249 ai env (PApp (PRef f) is es)
250 = let is' = map (\ (n, tm) -> (n, ai env tm)) is
251 es' = map (ai env) es in
252 aiFn env (PRef f) is' es'
253 ai env (PApp f is es) = let f' = ai env f
254 is' = map (\ (n, tm) -> (n, ai env tm)) is
255 es' = map (ai env) es in
256 aiFn env f' is' es'
257 ai env (PLam n ty sc) = let ty' = ai env ty
258 sc' = ai (n:env) sc in
259 PLam n ty' sc'
260 ai env (PPi p n ty sc) = let ty' = ai env ty
261 sc' = ai (n:env) sc in
262 PPi p n ty' sc'
263 ai env (PHidden tm) = PHidden (ai env tm)
264 ai env tm = tm
266 aiFn env (PRef f) is es | not (f `elem` env)
267 = case lookupCtxt f (idris_implicits ist) of
268 Just ns -> pApp (PRef f) (insertImpl ns is) es
269 Nothing -> pApp (PRef f) is es
270 aiFn env f is es = pApp f is es
272 pApp f [] [] = f
273 pApp f is es = PApp f is es
275 insertImpl [] given = []
276 insertImpl (n:ns) given
277 = case lookup n given of
278 Just val -> (n, val) : insertImpl ns given
279 Nothing -> (n, Placeholder) : insertImpl ns given