git.iko.soy/Idris-dev
on 7123e31 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
323 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
48setLogLevel :: Int -> Idris ()
49setLogLevel l = do i <- get
50 let opts = idris_options i
51 let opt' = opts { opt_logLevel = l }
52 put (i { idris_options = opt' } )
54logLevel :: Idris Int
55logLevel = do i <- get
56 return (opt_logLevel (idris_options i))
58logLvl :: Int -> String -> Idris ()
59logLvl l str = do i <- get
60 let lvl = opt_logLevel (idris_options i)
61 when (lvl >= l)
62 $ do lift (putStrLn str)
63 put (i { idris_log = idris_log i ++ str ++ "\n" } )
65iLOG :: String -> Idris ()
66iLOG = logLvl 1
68-- Commands in the REPL
70data Command = Quit | Help | Eval PTerm
71 | TTShell
72 | NOP
74-- Parsed declarations
76data Fixity = Infixl { prec :: Int }
77 | Infixr { prec :: Int }
78 | InfixN { prec :: Int }
79 | PrefixN { prec :: Int }
80 deriving Eq
82instance Show Fixity where
83 show (Infixl i) = "infixl " ++ show i
84 show (Infixr i) = "infixr " ++ show i
85 show (InfixN i) = "infix " ++ show i
86 show (PrefixN i) = "prefix " ++ show i
88data FixDecl = Fix Fixity String
89 deriving (Show, Eq)
91instance Ord FixDecl where
92 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
94data Plicity = Imp | Exp deriving Show
96data PDecl' t = PFix Fixity [String] -- fixity declaration
97 | PTy Name t -- type declaration
98 | PClauses Name [PClause' t] -- pattern clause
99 | PData (PData' t) -- data declaration
100 deriving Functor
102data PClause' t = PClause Name t t
103 deriving Functor
105data PData' t = PDatadecl { d_name :: Name,
106 d_tcon :: t,
107 d_cons :: [(Name, t)] }
108 deriving Functor
110-- Handy to get a free function for applying PTerm -> PTerm functions
111-- across a program, by deriving Functor
113type PDecl = PDecl' PTerm
114type PData = PData' PTerm
115type PClause = PClause' PTerm
116-- High level language terms
118data PTerm = PQuote Raw
119 | PRef Name
120 | PLam Name PTerm PTerm
121 | PPi Plicity Name PTerm PTerm
122 | PLet Name PTerm PTerm PTerm -- not implemented yet
123 | PApp PTerm [(Name, PTerm)] [PTerm]
124 | PHidden PTerm -- irrelevant or hidden pattern
125 | PSet
126 | PConstant Const
127 | Placeholder
129-- Syntactic sugar info (TODO: namespaces, parameters, modules)
131data SyntaxInfo = Syn { using :: [(Name, PTerm)] }
132 deriving Show
134defaultSyntax = Syn []
136--- Pretty printing declarations and terms
138instance Show PTerm where
139 show tm = showImp False tm
141instance Show PDecl where
142 show (PFix f ops) = show f ++ " " ++ showSep ", " ops
143 show (PTy n ty) = show n ++ " : " ++ show ty
144 show (PClauses n c) = showSep "\n" (map show c)
145 show (PData d) = show d
147instance Show PClause where
148 show c = showCImp False c
150instance Show PData where
151 show d = showDImp False d
153showCImp :: Bool -> PClause -> String
154showCImp impl (PClause n l r) = showImp impl l ++ " = " ++ showImp impl r
156showDImp :: Bool -> PData -> String
157showDImp impl (PDatadecl n ty cons)
158 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
159 ++ showSep "\n\t| "
160 (map (\ (n, t) -> show n ++ " : " ++ showImp impl t) cons)
162showImp :: Bool -> PTerm -> String
163showImp impl tm = se 10 tm where
164 se p (PQuote r) = "![" ++ show r ++ "]"
165 se p (PRef n) = show n
166 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
167 se p (PPi Exp n ty sc)
168 | n `elem` allNamesIn sc = bracket p 2 $
169 "(" ++ show n ++ " : " ++ se 10 ty ++
170 ") -> " ++ se 10 sc
171 | otherwise = bracket p 2 $ se 10 ty ++ " -> " ++ se 10 sc
172 se p (PPi Imp n ty sc)
173 | impl = bracket p 2 $ "{" ++ show n ++ " : " ++ se 10 ty ++
174 "} -> " ++ se 10 sc
175 | otherwise = se 10 sc
176 se p (PApp (PRef f) _ [])
177 | not impl = show f
178 se p (PApp (PRef op@(UN [f:_])) _ [l, r])
179 | not impl && not (isAlpha f)
180 = bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
181 se p (PApp f imps args)
182 = bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")
183 ++ concatMap seArg args
184 se p (PHidden tm) = "." ++ se 0 tm
185 se p PSet = "Set"
186 se p (PConstant c) = show c
187 se p Placeholder = "_"
189 seArg arg = " " ++ se 0 arg
190 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
192 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
193 | otherwise = str
195allNamesIn :: PTerm -> [Name]
196allNamesIn tm = nub $ ni [] tm
197 where
198 ni env (PRef n)
199 | not (n `elem` env) = [n]
200 ni env (PApp f is es) = ni env f ++ concatMap (ni env) (map snd is) ++
201 concatMap (ni env) es
202 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
203 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
204 ni env (PHidden tm) = ni env tm
205 ni env _ = []
207namesIn :: IState -> PTerm -> [Name]
208namesIn ist tm = nub $ ni [] tm
209 where
210 ni env (PRef n)
211 | not (n `elem` env)
212 = case lookupCtxt n (idris_implicits ist) of
213 Nothing -> [n]
214 _ -> []
215 ni env (PApp f is es) = ni env f ++ concatMap (ni env) (map snd is) ++
216 concatMap (ni env) es
217 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
218 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
219 ni env (PHidden tm) = ni env tm
220 ni env _ = []
222-- For inferring types of things
224inferTy = MN 0 "__Infer"
225inferCon = MN 0 "__infer"
226inferDecl = PDatadecl inferTy
227 PSet
228 [(inferCon, PPi Imp (MN 0 "A") PSet (
229 PPi Exp (MN 0 "a") (PRef (MN 0 "A"))
230 (PRef inferTy)))]
232infTerm t = PApp (PRef inferCon) [(MN 0 "A", Placeholder)] [t]
233infP = P (TCon 0) inferTy (Set 0)
235getInferTerm, getInferType :: Term -> Term
236getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
237getInferTerm (App (App _ _) tm) = tm
238getInferTerm tm = error ("getInferTerm " ++ show tm)
240getInferType (Bind n b sc) = Bind n b $ getInferType sc
241getInferType (App (App _ ty) _) = ty
244-- Dealing with implicit arguments
246-- Add implicit Pi bindings for any names in the term which appear in an
247-- argument position.
249implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, ([Name], Int))
250implicitise syn ist tm
251 = let uvars = using syn
252 (declimps, a, ns) = execState (imps [] tm) ([], 0, []) in
253 if null ns
254 then (tm, (reverse declimps, a))
255 else implicitise syn ist (pibind uvars ns tm)
256 where
257 imps env (PApp f is es)
258 = do (decls, a, ns) <- get
259 let isn = concatMap (namesIn ist) (map snd is)
260 let esn = concatMap (namesIn ist) es
261 put (decls, a, nub (ns ++ ((isn ++ esn) \\ (env ++ decls))))
262 imps env (PPi Imp n ty sc)
263 = do imps env ty
264 (impdecls, a, ns) <- get
265 put (n:impdecls, a, ns)
266 imps (n:env) sc
267 imps env (PPi Exp n ty sc)
268 = do imps env ty
269 (impdecls, a, ns) <- get
270 put (impdecls, a+1, ns)
271 imps (n:env) sc
272 imps env (PLam n ty sc)
273 = do imps env ty
274 imps (n:env) sc
275 imps env (PHidden tm) = imps env tm
276 imps env _ = return ()
278 pibind using [] sc = sc
279 pibind using (n:ns) sc = case lookup n using of
280 Just ty -> PPi Imp n ty (pibind using ns sc)
281 Nothing -> PPi Imp n Placeholder (pibind using ns sc)
283addImpl :: IState -> PTerm -> PTerm
284addImpl ist ptm = ai [] ptm
285 where
286 ai env (PRef f) = aiFn env (PRef f) [] []
287 ai env (PApp (PRef f) is es)
288 = let is' = map (\ (n, tm) -> (n, ai env tm)) is
289 es' = map (ai env) es in
290 aiFn env (PRef f) is' es'
291 ai env (PApp f is es) = let f' = ai env f
292 is' = map (\ (n, tm) -> (n, ai env tm)) is
293 es' = map (ai env) es in
294 aiFn env f' is' es'
295 ai env (PLam n ty sc) = let ty' = ai env ty
296 sc' = ai (n:env) sc in
297 PLam n ty' sc'
298 ai env (PPi p n ty sc) = let ty' = ai env ty
299 sc' = ai (n:env) sc in
300 PPi p n ty' sc'
301 ai env (PHidden tm) = PHidden (ai env tm)
302 ai env tm = tm
304 aiFn env (PRef f) is es | not (f `elem` env)
305 = case lookupCtxt f (idris_implicits ist) of
306 Just (ns, a) -> pApp a (PRef f) (insertImpl ns is) es
307 Nothing -> pApp 1 (PRef f) is es
308 aiFn env f is es = pApp 1 f is es
310 pApp a f [] [] = f
311 pApp a f is es = let rest = drop a es in
312 appRest (PApp f is (take a es)) rest
314 appRest f [] = f
315 appRest f (a : as) = appRest (PApp f [] [a]) as
317 insertImpl [] given = []
318 insertImpl (n:ns) given
319 = case lookup n given of
320 Just val -> (n, val) : insertImpl ns given
321 Nothing -> (n, Placeholder) : insertImpl ns given