git.iko.soy/Idris-dev
on be2b9bc help sign in
Idris-dev/src/Idris/AbsSyntax.hs
277 lines 9.3 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 Control.Monad.Trans.State.Lazy(liftCatch)
11import Data.List
12import Data.Char
14data IOption = Logging
15 deriving (Show, Eq)
17-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
18-- without typechecking).
19-- This will include all the functions and data declarations, plus fixity declarations
20-- and syntax macros.
22data IState = IState { tt_ctxt :: Context,
23 idris_infixes :: [FixDecl],
24 idris_implicits :: Ctxt [Name],
25 idris_log :: String,
26 idris_options :: [IOption]
27 }
29idrisInit = IState emptyContext [] emptyContext "" []
31-- The monad for the main REPL - reading and processing files and updating
32-- global state (hence the IO inner monad).
33type Idris a = StateT IState IO a
35getContext :: Idris Context
36getContext = do i <- get; return (tt_ctxt i)
38setContext :: Context -> Idris ()
39setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
41updateContext :: (Context -> Context) -> Idris ()
42updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
44iputStrLn :: String -> Idris ()
45iputStrLn = lift.putStrLn
47tclift :: Show a => TC a -> Idris a
48tclift tc = case tc of
49 OK v -> return v
50 err -> fail (show err)
52setOpt :: IOption -> Bool -> Idris ()
53setOpt o True = do i <- get
54 put (i { idris_options = nub (o : idris_options i) })
55setOpt o False = do i <- get
56 put (i { idris_options = idris_options i \\ [o] })
58iLOG :: String -> Idris ()
59iLOG str = do i <- get
60 when (Logging `elem` idris_options i)
61 $ do lift (putStrLn str)
62 put (i { idris_log = idris_log i ++ str ++ "\n" } )
64idrisCatch :: Idris a -> (IOError -> Idris a) -> Idris a
65idrisCatch op handler = liftCatch catch op handler
67-- Commands in the REPL
69data Command = Quit | Help | Eval PTerm
70 | TTShell
71 | NOP
73-- Parsed declarations
75data Fixity = Infixl { prec :: Int }
76 | Infixr { prec :: Int }
77 | InfixN { prec :: Int }
78 deriving Eq
80instance Show Fixity where
81 show (Infixl i) = "infixl " ++ show i
82 show (Infixr i) = "infixr " ++ show i
83 show (InfixN i) = "infix " ++ show i
85data FixDecl = Fix Fixity String
86 deriving (Show, Eq)
88instance Ord FixDecl where
89 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
91data Plicity = Imp | Exp deriving Show
93data PDecl' t = PFix Fixity [String] -- fixity declaration
94 | PTy Name t -- type declaration
95 | PClauses [PClause' t] -- pattern clause
96 | PData (PData' t) -- data declaration
97 deriving Functor
99data PClause' t = PClause Name t t
100 deriving Functor
102data PData' t = PDatadecl { d_name :: Name,
103 d_tcon :: t,
104 d_cons :: [(Name, t)] }
105 deriving Functor
107-- Handy to get a free function for applying PTerm -> PTerm functions
108-- across a program, by deriving Functor
110type PDecl = PDecl' PTerm
111type PData = PData' PTerm
112type PClause = PClause' PTerm
113-- High level language terms
115data PTerm = PQuote Raw
116 | PRef Name
117 | PLam Name PTerm PTerm
118 | PPi Plicity Name PTerm PTerm
119 | PApp PTerm [(Name, PTerm)] [PTerm]
120 | PHidden PTerm -- irrelevant or hidden pattern
121 | PSet
122 | Placeholder
124--- Pretty printing declarations and terms
126instance Show PTerm where
127 show tm = showImp False tm
129instance Show PDecl where
130 show (PFix f ops) = show f ++ " " ++ showSep ", " ops
131 show (PTy n ty) = show n ++ " : " ++ show ty
132 show (PClauses c) = showSep "\n" (map show c)
133 show (PData d) = show d
135instance Show PClause where
136 show c = showCImp False c
138instance Show PData where
139 show d = showDImp False d
141showCImp :: Bool -> PClause -> String
142showCImp impl (PClause n l r) = showImp impl l ++ " = " ++ showImp impl r
144showDImp :: Bool -> PData -> String
145showDImp impl (PDatadecl n ty cons)
146 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
147 ++ showSep "\n\t| "
148 (map (\ (n, t) -> show n ++ " : " ++ showImp impl t) cons)
150showImp :: Bool -> PTerm -> String
151showImp impl tm = se 10 tm where
152 se p (PQuote r) = "![" ++ show r ++ "]"
153 se p (PRef n) = show n
154 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
155 se p (PPi Exp n ty sc)
156 | n `elem` allNamesIn sc = bracket p 2 $
157 "(" ++ show n ++ " : " ++ se 10 ty ++
158 ") -> " ++ se 10 sc
159 | otherwise = bracket p 2 $ se 10 ty ++ " -> " ++ se 10 sc
160 se p (PPi Imp n ty sc)
161 | impl = bracket p 2 $ "{" ++ show n ++ " : " ++ se 10 ty ++
162 "} -> " ++ se 10 sc
163 | otherwise = se 10 sc
164 se p (PApp (PRef f) _ [])
165 | not impl = show f
166 se p (PApp (PRef op@(UN [f:_])) _ [l, r])
167 | not impl && not (isAlpha f)
168 = bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 1 r
169 se p (PApp f imps args)
170 = bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")
171 ++ concatMap seArg args
172 se p (PHidden tm) = "." ++ se 0 tm
173 se p PSet = "Set"
174 se p Placeholder = "_"
176 seArg arg = " " ++ se 0 arg
177 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
179 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
180 | otherwise = str
182allNamesIn :: PTerm -> [Name]
183allNamesIn tm = nub $ ni [] tm
184 where
185 ni env (PRef n)
186 | not (n `elem` env) = [n]
187 ni env (PApp f is es) = ni env f ++ concatMap (ni env) (map snd is) ++
188 concatMap (ni env) es
189 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
190 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
191 ni env (PHidden tm) = ni env tm
192 ni env _ = []
194namesIn :: IState -> PTerm -> [Name]
195namesIn ist tm = nub $ ni [] tm
196 where
197 ni env (PRef n)
198 | not (n `elem` env)
199 = case lookupCtxt n (idris_implicits ist) of
200 Nothing -> [n]
201 _ -> []
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 _ = []
209-- Dealing with implicit arguments
211-- Add implicit Pi bindings for any names in the term which appear in an
212-- argument position.
214implicitise :: IState -> PTerm -> (PTerm, [Name])
215implicitise ist tm
216 = let (declimps, ns) = execState (imps [] tm) ([], []) in
217 (pibind ns tm, ns ++ reverse declimps)
218 where
219 imps env (PApp f is es)
220 = do (decls, ns) <- get
221 let isn = concatMap (namesIn ist) (map snd is)
222 let esn = concatMap (namesIn ist) es
223 put (decls, nub (ns ++ ((isn ++ esn) \\ env)))
224 imps env (PPi Imp n ty sc)
225 = do imps env ty
226 (decls, ns) <- get
227 put (n:decls, ns)
228 imps (n:env) sc
229 imps env (PPi Exp n ty sc)
230 = do imps env ty
231 imps (n:env) sc
232 imps env (PLam n ty sc)
233 = do imps env ty
234 imps (n:env) sc
235 imps env (PHidden tm) = imps env tm
236 imps env _ = return ()
238 pibind [] sc = sc
239 pibind (n:ns) sc = PPi Imp n Placeholder (pibind ns sc)
241addImpl :: IState -> PTerm -> PTerm
242addImpl ist ptm = ai [] ptm
243 where
244 ai env (PRef f) = aiFn env (PRef f) [] []
245 ai env (PApp (PRef f) is es)
246 = let is' = map (\ (n, tm) -> (n, ai env tm)) is
247 es' = map (ai env) es in
248 aiFn env (PRef f) is' es'
249 ai env (PApp f is es) = let f' = ai env f
250 is' = map (\ (n, tm) -> (n, ai env tm)) is
251 es' = map (ai env) es in
252 aiFn env f' is' es'
253 ai env (PLam n ty sc) = let ty' = ai env ty
254 sc' = ai (n:env) sc in
255 PLam n ty' sc'
256 ai env (PPi p n ty sc) = let ty' = ai env ty
257 sc' = ai (n:env) sc in
258 PPi p n ty' sc'
259 ai env (PHidden tm) = PHidden (ai env tm)
260 ai env tm = tm
262 aiFn env (PRef f) is es | not (f `elem` env)
263 = case lookupCtxt f (idris_implicits ist) of
264 Just ns -> pApp (PRef f) (insertImpl ns is) es
265 Nothing -> pApp (PRef f) is es
266 aiFn env f is es = pApp f is es
268 pApp f [] [] = f
269 pApp f is es = PApp f is es
271 insertImpl [] given = []
272 insertImpl (n:ns) given
273 = case lookup n given of
274 Just val -> (n, val) : insertImpl ns given
275 Nothing -> (n, Placeholder) : insertImpl ns given