git.iko.soy/Idris-dev
on b1419b2 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
398 lines 13 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
12import Debug.Trace
14data IOption = IOption { opt_logLevel :: Int }
15 deriving (Show, Eq)
17defaultOpts = IOption 0
19-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
20-- without typechecking).
21-- This will include all the functions and data declarations, plus fixity declarations
22-- and syntax macros.
24data IState = IState { tt_ctxt :: Context,
25 idris_infixes :: [FixDecl],
26 idris_implicits :: Ctxt [PArg],
27 idris_log :: String,
28 idris_options :: IOption,
29 idris_name :: Int,
30 imported :: [FilePath]
31 }
33idrisInit = IState emptyContext [] emptyContext "" defaultOpts 0 []
35-- The monad for the main REPL - reading and processing files and updating
36-- global state (hence the IO inner monad).
37type Idris a = StateT IState IO a
39getContext :: Idris Context
40getContext = do i <- get; return (tt_ctxt i)
42getIState :: Idris IState
43getIState = get
45putIState :: IState -> Idris ()
46putIState = put
48getName :: Idris Int
49getName = do i <- get;
50 let idx = idris_name i;
51 put (i { idris_name = idx + 1 })
52 return idx
54setContext :: Context -> Idris ()
55setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
57updateContext :: (Context -> Context) -> Idris ()
58updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
60iputStrLn :: String -> Idris ()
61iputStrLn = lift.putStrLn
63setLogLevel :: Int -> Idris ()
64setLogLevel l = do i <- get
65 let opts = idris_options i
66 let opt' = opts { opt_logLevel = l }
67 put (i { idris_options = opt' } )
69logLevel :: Idris Int
70logLevel = do i <- get
71 return (opt_logLevel (idris_options i))
73logLvl :: Int -> String -> Idris ()
74logLvl l str = do i <- get
75 let lvl = opt_logLevel (idris_options i)
76 when (lvl >= l)
77 $ do lift (putStrLn str)
78 put (i { idris_log = idris_log i ++ str ++ "\n" } )
80iLOG :: String -> Idris ()
81iLOG = logLvl 1
83-- Commands in the REPL
85data Command = Quit | Help | Eval PTerm
86 | TTShell
87 | NOP
89-- Parsed declarations
91data Fixity = Infixl { prec :: Int }
92 | Infixr { prec :: Int }
93 | InfixN { prec :: Int }
94 | PrefixN { prec :: Int }
95 deriving Eq
97instance Show Fixity where
98 show (Infixl i) = "infixl " ++ show i
99 show (Infixr i) = "infixr " ++ show i
100 show (InfixN i) = "infix " ++ show i
101 show (PrefixN i) = "prefix " ++ show i
103data FixDecl = Fix Fixity String
104 deriving (Show, Eq)
106instance Ord FixDecl where
107 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
109data Plicity = Imp | Exp deriving Show
111data PDecl' t = PFix Fixity [String] -- fixity declaration
112 | PTy Name t -- type declaration
113 | PClauses Name [PClause' t] -- pattern clause
114 | PData (PData' t) -- data declaration
115 | PParams [(Name, PTerm)] [PDecl' t] -- params block
116 | PImport String
117 deriving Functor
119data PClause' t = PClause Name t t [PDecl]
120 deriving Functor
122data PData' t = PDatadecl { d_name :: Name,
123 d_tcon :: t,
124 d_cons :: [(Name, t)] }
125 deriving Functor
127-- Handy to get a free function for applying PTerm -> PTerm functions
128-- across a program, by deriving Functor
130type PDecl = PDecl' PTerm
131type PData = PData' PTerm
132type PClause = PClause' PTerm
134-- get all the names declared in a decl
136declared :: PDecl -> [Name]
137declared (PFix _ _) = []
138declared (PTy n t) = [n]
139declared (PClauses n _) = [] -- not a declaration
140declared (PData (PDatadecl n _ ts)) = n : map fst ts
141declared (PParams _ ds) = concatMap declared ds
142declared (PImport _) = []
144-- High level language terms
145--
146data PTerm = PQuote Raw
147 | PRef Name
148 | PLam Name PTerm PTerm
149 | PPi Plicity Name PTerm PTerm
150 | PLet Name PTerm PTerm PTerm -- not implemented yet
151 | PApp PTerm [PArg]
152 | PHidden PTerm -- irrelevant or hidden pattern
153 | PSet
154 | PConstant Const
155 | Placeholder
157data PArg' t = PImp { pname :: Name, getTm :: t }
158 | PExp { getTm :: t }
159 deriving (Show, Functor)
161type PArg = PArg' PTerm
163-- Syntactic sugar info (TODO: namespaces, parameters, modules)
165data SyntaxInfo = Syn { using :: [(Name, PTerm)],
166 syn_params :: [(Name, PTerm)] }
167 deriving Show
169defaultSyntax = Syn [] []
171--- Pretty printing declarations and terms
173instance Show PTerm where
174 show tm = showImp False tm
176instance Show PDecl where
177 show (PFix f ops) = show f ++ " " ++ showSep ", " ops
178 show (PTy n ty) = show n ++ " : " ++ show ty
179 show (PClauses n c) = showSep "\n" (map show c)
180 show (PData d) = show d
182instance Show PClause where
183 show c = showCImp False c
185instance Show PData where
186 show d = showDImp False d
188showCImp :: Bool -> PClause -> String
189showCImp impl (PClause n l r w) = showImp impl l ++ " = " ++ showImp impl r
190 ++ " where " ++ show w
191showDImp :: Bool -> PData -> String
192showDImp impl (PDatadecl n ty cons)
193 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
194 ++ showSep "\n\t| "
195 (map (\ (n, t) -> show n ++ " : " ++ showImp impl t) cons)
197getImps :: [PArg] -> [(Name, PTerm)]
198getImps [] = []
199getImps (PImp n tm : xs) = (n, tm) : getImps xs
200getImps (_ : xs) = getImps xs
202getExps :: [PArg] -> [PTerm]
203getExps [] = []
204getExps (PExp tm : xs) = tm : getExps xs
205getExps (_ : xs) = getExps xs
207getAll :: [PArg] -> [PTerm]
208getAll = map getTm
210showImp :: Bool -> PTerm -> String
211showImp impl tm = se 10 tm where
212 se p (PQuote r) = "![" ++ show r ++ "]"
213 se p (PRef n) = show n
214 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
215 se p (PPi Exp n ty sc)
216 | n `elem` allNamesIn sc = bracket p 2 $
217 "(" ++ show n ++ " : " ++ se 10 ty ++
218 ") -> " ++ se 10 sc
219 | otherwise = bracket p 2 $ se 0 ty ++ " -> " ++ se 10 sc
220 se p (PPi Imp n ty sc)
221 | impl = bracket p 2 $ "{" ++ show n ++ " : " ++ se 10 ty ++
222 "} -> " ++ se 10 sc
223 | otherwise = se 10 sc
224 se p (PApp (PRef f) [])
225 | not impl = show f
226 se p (PApp (PRef op@(UN [f:_])) args)
227 | length (getExps args) == 2 && not impl && not (isAlpha f)
228 = let [l, r] = getExps args in
229 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
230 se p (PApp f as)
231 = let (imps, args) = (getImps as, getExps as) in
232 bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")
233 ++ concatMap seArg args
234 se p (PHidden tm) = "." ++ se 0 tm
235 se p PSet = "Set"
236 se p (PConstant c) = show c
237 se p Placeholder = "_"
239 seArg arg = " " ++ se 0 arg
240 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
242 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
243 | otherwise = str
245allNamesIn :: PTerm -> [Name]
246allNamesIn tm = nub $ ni [] tm
247 where
248 ni env (PRef n)
249 | not (n `elem` env) = [n]
250 ni env (PApp f as) = ni env f ++ concatMap (ni env) (map getTm as)
251 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
252 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
253 ni env (PHidden tm) = ni env tm
254 ni env _ = []
256namesIn :: IState -> PTerm -> [Name]
257namesIn ist tm = nub $ ni [] tm
258 where
259 ni env (PRef n)
260 | not (n `elem` env)
261 = case lookupCtxt n (idris_implicits ist) of
262 Nothing -> [n]
263 _ -> []
264 ni env (PApp f as) = ni env f ++ concatMap (ni env) (map getTm as)
265 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
266 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
267 ni env (PHidden tm) = ni env tm
268 ni env _ = []
270-- For inferring types of things
272inferTy = MN 0 "__Infer"
273inferCon = MN 0 "__infer"
274inferDecl = PDatadecl inferTy
275 PSet
276 [(inferCon, PPi Imp (MN 0 "A") PSet (
277 PPi Exp (MN 0 "a") (PRef (MN 0 "A"))
278 (PRef inferTy)))]
280infTerm t = PApp (PRef inferCon) [PImp (MN 0 "A") Placeholder, PExp t]
281infP = P (TCon 0) inferTy (Set 0)
283getInferTerm, getInferType :: Term -> Term
284getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
285getInferTerm (App (App _ _) tm) = tm
286getInferTerm tm = error ("getInferTerm " ++ show tm)
288getInferType (Bind n b sc) = Bind n b $ getInferType sc
289getInferType (App (App _ ty) _) = ty
291piBind :: [(Name, PTerm)] -> PTerm -> PTerm
292piBind [] t = t
293piBind ((n, ty):ns) t = PPi Exp n ty (piBind ns t)
295-- Dealing with implicit arguments
297-- Add implicit Pi bindings for any names in the term which appear in an
298-- argument position.
300implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
301implicitise syn ist tm
302 = let uvars = using syn
303 pvars = syn_params syn
304 (declimps, ns') = execState (imps True [] tm) ([], [])
305 ns = ns' \\ map fst pvars in
306 if null ns
307 then (tm, reverse declimps)
308 else implicitise syn ist (pibind uvars ns tm)
309 where
310 imps top env (PApp f as)
311 = do (decls, ns) <- get
312 let isn = concatMap (namesIn ist) (map getTm as)
313 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
314 imps top env (PPi Imp n ty sc)
315 = do let isn = namesIn ist ty \\ [n]
316 (decls , ns) <- get
317 put (PImp n ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
318 imps True (n:env) sc
319 imps top env (PPi Exp n ty sc)
320 = do let isn = (namesIn ist ty ++ case sc of
321 (PRef x) -> namesIn ist sc
322 _ -> []) \\ [n]
323 (decls, ns) <- get -- ignore decls in HO types
324 put (PExp ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
325 imps True (n:env) sc
326 imps top env (PLam n ty sc)
327 = do imps False env ty
328 imps False (n:env) sc
329 imps top env (PHidden tm) = imps False env tm
330 imps top env _ = return ()
332 pibind using [] sc = sc
333 pibind using (n:ns) sc = case lookup n using of
334 Just ty -> PPi Imp n ty (pibind using ns sc)
335 Nothing -> PPi Imp n Placeholder (pibind using ns sc)
337-- Add implicit arguments in function calls
339addImpl :: IState -> PTerm -> PTerm
340addImpl ist ptm = ai [] ptm
341 where
342 ai env (PRef f) = aiFn env (PRef f) []
343 ai env (PApp (PRef f) as)
344 = let as' = map (fmap (ai env)) as in
345 aiFn env (PRef f) as'
346 ai env (PApp f as) = let f' = ai env f
347 as' = map (fmap (ai env)) as in
348 aiFn env f' as'
349 ai env (PLam n ty sc) = let ty' = ai env ty
350 sc' = ai (n:env) sc in
351 PLam n ty' sc'
352 ai env (PPi p n ty sc) = let ty' = ai env ty
353 sc' = ai (n:env) sc in
354 PPi p n ty' sc'
355 ai env (PHidden tm) = PHidden (ai env tm)
356 ai env tm = tm
358 aiFn env (PRef f) as | not (f `elem` env)
359 = case lookupCtxt f (idris_implicits ist) of
360 Just ns -> pApp (length ns) (PRef f) (insertImpl ns as)
361 Nothing -> pApp 1 (PRef f) as
362 aiFn env f as = pApp 1 f as
364 pApp a f [] = f
365 pApp a f as = let rest = drop a as in
366 appRest (PApp f (take a as)) rest
368 appRest f [] = f
369 appRest f (a : as) = appRest (PApp f [a]) as
371 insertImpl :: [PArg] -> [PArg] -> [PArg]
372 insertImpl (PExp ty : ps) (PExp tm : given) =
373 PExp tm : insertImpl ps given
374 insertImpl (PImp n ty : ps) given =
375 case find n given [] of
376 Just (tm, given') -> PImp n ty : insertImpl ps given'
377 Nothing -> PImp n Placeholder : insertImpl ps given
378 insertImpl expected [] = []
379 insertImpl [] given = given
381 find n [] acc = Nothing
382 find n (PImp n' t : gs) acc
383 | n == n' = Just (t, reverse acc ++ gs)
384 find n (g : gs) acc = find n gs (g : acc)
386-- Debugging/logging stuff
388dumpDecls :: [PDecl] -> String
389dumpDecls [] = ""
390dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
392dumpDecl (PFix f ops) = show f ++ " " ++ showSep ", " ops
393dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
394dumpDecl (PClauses n cs) = "pat\t" ++ showSep "\n\t" (map (showCImp True) cs)
395dumpDecl (PData d) = showDImp True d
396dumpDecl (PParams ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
397dumpDecl (PImport i) = "import " ++ i