git.iko.soy/Idris-dev
on ec87a69 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
483 lines 16 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
14import qualified Epic.Epic as E
16data IOption = IOption { opt_logLevel :: Int }
17 deriving (Show, Eq)
19defaultOpts = IOption 0
21-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
22-- without typechecking).
23-- This will include all the functions and data declarations, plus fixity declarations
24-- and syntax macros.
26data IState = IState { tt_ctxt :: Context,
27 idris_infixes :: [FixDecl],
28 idris_implicits :: Ctxt [PArg],
29 idris_log :: String,
30 idris_options :: IOption,
31 idris_name :: Int,
32 idris_metavars :: [Name],
33 syntax_rules :: [Syntax],
34 imported :: [FilePath],
35 idris_prims :: [(Name, ([E.Name], E.Term))]
36 }
38idrisInit = IState emptyContext [] emptyContext "" defaultOpts 0 [] [] [] []
40-- The monad for the main REPL - reading and processing files and updating
41-- global state (hence the IO inner monad).
42type Idris a = StateT IState IO a
44getContext :: Idris Context
45getContext = do i <- get; return (tt_ctxt i)
47getIState :: Idris IState
48getIState = get
50putIState :: IState -> Idris ()
51putIState = put
53getName :: Idris Int
54getName = do i <- get;
55 let idx = idris_name i;
56 put (i { idris_name = idx + 1 })
57 return idx
59checkUndefined :: FC -> Name -> Idris ()
60checkUndefined fc n
61 = do i <- getContext
62 case lookupCtxt n i of
63 Just _ -> fail $ show fc ++ ":" ++
64 show n ++ " already defined"
65 _ -> return ()
67setContext :: Context -> Idris ()
68setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
70updateContext :: (Context -> Context) -> Idris ()
71updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
73addDeferred :: [(Name, Type)] -> Idris ()
74addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n t)) ns
75 i <- get
76 put (i { idris_metavars = map fst ns ++ idris_metavars i })
78solveDeferred :: Name -> Idris ()
79solveDeferred n = do i <- get
80 put (i { idris_metavars = idris_metavars i \\ [n] })
82iputStrLn :: String -> Idris ()
83iputStrLn = lift.putStrLn
85setLogLevel :: Int -> Idris ()
86setLogLevel l = do i <- get
87 let opts = idris_options i
88 let opt' = opts { opt_logLevel = l }
89 put (i { idris_options = opt' } )
91logLevel :: Idris Int
92logLevel = do i <- get
93 return (opt_logLevel (idris_options i))
95logLvl :: Int -> String -> Idris ()
96logLvl l str = do i <- get
97 let lvl = opt_logLevel (idris_options i)
98 when (lvl >= l)
99 $ do lift (putStrLn str)
100 put (i { idris_log = idris_log i ++ str ++ "\n" } )
102iLOG :: String -> Idris ()
103iLOG = logLvl 1
105-- Commands in the REPL
107data Command = Quit | Help | Eval PTerm
108 | Compile String
109 | Metavars
110 | TTShell
111 | NOP
113-- Parsed declarations
115data Fixity = Infixl { prec :: Int }
116 | Infixr { prec :: Int }
117 | InfixN { prec :: Int }
118 | PrefixN { prec :: Int }
119 deriving Eq
121instance Show Fixity where
122 show (Infixl i) = "infixl " ++ show i
123 show (Infixr i) = "infixr " ++ show i
124 show (InfixN i) = "infix " ++ show i
125 show (PrefixN i) = "prefix " ++ show i
127data FixDecl = Fix Fixity String
128 deriving (Show, Eq)
130instance Ord FixDecl where
131 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
133data Plicity = Imp | Exp deriving Show
135data PDecl' t = PFix FC Fixity [String] -- fixity declaration
136 | PTy FC Name t -- type declaration
137 | PClauses FC Name [PClause' t] -- pattern clause
138 | PData FC (PData' t) -- data declaration
139 | PParams FC [(Name, PTerm)] [PDecl' t] -- params block
140 | PSyntax FC Syntax
141 deriving Functor
143data PClause' t = PClause Name t t [PDecl]
144 deriving Functor
146data PData' t = PDatadecl { d_name :: Name,
147 d_tcon :: t,
148 d_cons :: [(Name, t, FC)] }
149 deriving Functor
151-- Handy to get a free function for applying PTerm -> PTerm functions
152-- across a program, by deriving Functor
154type PDecl = PDecl' PTerm
155type PData = PData' PTerm
156type PClause = PClause' PTerm
158-- get all the names declared in a decl
160declared :: PDecl -> [Name]
161declared (PFix _ _ _) = []
162declared (PTy _ n t) = [n]
163declared (PClauses _ n _) = [] -- not a declaration
164declared (PData _ (PDatadecl n _ ts)) = n : map fstt ts
165 where fstt (a, _, _) = a
166declared (PParams _ _ ds) = concatMap declared ds
167-- declared (PImport _) = []
169-- High level language terms
170--
171data PTerm = PQuote Raw
172 | PRef Name
173 | PLam Name PTerm PTerm
174 | PPi Plicity Name PTerm PTerm
175 | PLet Name PTerm PTerm PTerm -- not implemented yet
176 | PApp PTerm [PArg]
177 | PTrue
178 | PFalse
179 | PPair PTerm PTerm
180 | PHidden PTerm -- irrelevant or hidden pattern
181 | PSet
182 | PConstant Const
183 | Placeholder
184 | PDoBlock [PDo]
185 | PReturn
186 | PMetavar Name
187 | PElabError String -- error to report on elaboration
189data PDo = DoExp PTerm
190 | DoBind Name PTerm
191 | DoLet Name PTerm
193data PArg' t = PImp { pname :: Name, getTm :: t }
194 | PExp { getTm :: t }
195 deriving (Show, Functor)
197type PArg = PArg' PTerm
199-- Syntactic sugar info (TODO: namespaces, modules)
201data DSL = DSL { dsl_bind :: Name,
202 dsl_return :: Name }
203 deriving Show
205data Syntax = Rule [SSymbol] PTerm
206 deriving Show
208data SSymbol = Keyword Name
209 | Symbol String
210 | Expr Name
211 deriving Show
213initDSL = DSL (UN ["io_bind"]) (UN ["io_return"])
215data SyntaxInfo = Syn { using :: [(Name, PTerm)],
216 syn_params :: [(Name, PTerm)],
217 dsl_info :: DSL }
218 deriving Show
220defaultSyntax = Syn [] [] initDSL
222--- Pretty printing declarations and terms
224instance Show PTerm where
225 show tm = showImp False tm
227instance Show PDecl where
228 show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
229 show (PTy _ n ty) = show n ++ " : " ++ show ty
230 show (PClauses _ n c) = showSep "\n" (map show c)
231 show (PData _ d) = show d
233instance Show PClause where
234 show c = showCImp False c
236instance Show PData where
237 show d = showDImp False d
239showCImp :: Bool -> PClause -> String
240showCImp impl (PClause n l r w) = showImp impl l ++ " = " ++ showImp impl r
241 ++ " where " ++ show w
242showDImp :: Bool -> PData -> String
243showDImp impl (PDatadecl n ty cons)
244 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
245 ++ showSep "\n\t| "
246 (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
248getImps :: [PArg] -> [(Name, PTerm)]
249getImps [] = []
250getImps (PImp n tm : xs) = (n, tm) : getImps xs
251getImps (_ : xs) = getImps xs
253getExps :: [PArg] -> [PTerm]
254getExps [] = []
255getExps (PExp tm : xs) = tm : getExps xs
256getExps (_ : xs) = getExps xs
258getAll :: [PArg] -> [PTerm]
259getAll = map getTm
261showImp :: Bool -> PTerm -> String
262showImp impl tm = se 10 tm where
263 se p (PQuote r) = "![" ++ show r ++ "]"
264 se p (PRef n) = show n
265 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
266 se p (PPi Exp n ty sc)
267 | n `elem` allNamesIn sc = bracket p 2 $
268 "(" ++ show n ++ " : " ++ se 10 ty ++
269 ") -> " ++ se 10 sc
270 | otherwise = bracket p 2 $ se 0 ty ++ " -> " ++ se 10 sc
271 se p (PPi Imp n ty sc)
272 | impl = bracket p 2 $ "{" ++ show n ++ " : " ++ se 10 ty ++
273 "} -> " ++ se 10 sc
274 | otherwise = se 10 sc
275 se p (PApp (PRef f) [])
276 | not impl = show f
277 se p (PApp (PRef op@(UN [f:_])) args)
278 | length (getExps args) == 2 && not impl && not (isAlpha f)
279 = let [l, r] = getExps args in
280 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
281 se p (PApp f as)
282 = let (imps, args) = (getImps as, getExps as) in
283 bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")
284 ++ concatMap seArg args
285 se p (PHidden tm) = "." ++ se 0 tm
286 se p PTrue = "()"
287 se p PFalse = "_|_"
288 se p (PPair l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
289 se p PSet = "Set"
290 se p (PConstant c) = show c
291 se p (PMetavar n) = "?" ++ show n
292 se p Placeholder = "_"
294 seArg arg = " " ++ se 0 arg
295 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
297 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
298 | otherwise = str
300allNamesIn :: PTerm -> [Name]
301allNamesIn tm = nub $ ni [] tm
302 where
303 ni env (PRef n)
304 | not (n `elem` env) = [n]
305 ni env (PApp f as) = ni env f ++ concatMap (ni env) (map getTm as)
306 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
307 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
308 ni env (PHidden tm) = ni env tm
309 ni env (PPair l r) = ni env l ++ ni env r
310 ni env _ = []
312namesIn :: IState -> PTerm -> [Name]
313namesIn ist tm = nub $ ni [] tm
314 where
315 ni env (PRef n)
316 | not (n `elem` env)
317 = case lookupCtxt n (idris_implicits ist) of
318 Nothing -> [n]
319 _ -> []
320 ni env (PApp f as) = ni env f ++ concatMap (ni env) (map getTm as)
321 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
322 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
323 ni env (PPair l r) = ni env l ++ ni env r
324 ni env (PHidden tm) = ni env tm
325 ni env _ = []
327-- For inferring types of things
329bi = FC "builtin" 0
331inferTy = MN 0 "__Infer"
332inferCon = MN 0 "__infer"
333inferDecl = PDatadecl inferTy
334 PSet
335 [(inferCon, PPi Imp (MN 0 "A") PSet (
336 PPi Exp (MN 0 "a") (PRef (MN 0 "A"))
337 (PRef inferTy)), bi)]
339infTerm t = PApp (PRef inferCon) [PImp (MN 0 "A") Placeholder, PExp t]
340infP = P (TCon 0) inferTy (Set 0)
342getInferTerm, getInferType :: Term -> Term
343getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
344getInferTerm (App (App _ _) tm) = tm
345getInferTerm tm = error ("getInferTerm " ++ show tm)
347getInferType (Bind n b sc) = Bind n b $ getInferType sc
348getInferType (App (App _ ty) _) = ty
350-- Handy primitives: Unit, False, Pair, MkPair, mkForeign
353unitTy = MN 0 "__Unit"
354unitCon = MN 0 "__II"
355unitDecl = PDatadecl unitTy PSet
356 [(unitCon, PRef unitTy, bi)]
358falseTy = MN 0 "__False"
359falseDecl = PDatadecl falseTy PSet []
361pairTy = UN ["Pair"] -- MN 0 "__Pair"
362pairCon = UN ["MkPair"] -- MN 0 "__MkPair"
363pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
364 [(pairCon, PPi Imp (n "A") PSet (
365 PPi Imp (n "B") PSet (
366 PPi Exp (n "a") (PRef (n "A")) (
367 PPi Exp (n "c") (PRef (n "B"))
368 (PApp (PRef pairTy) [PExp (PRef (n "A")),
369 PExp (PRef (n "B"))])))), bi)]
370 where n a = MN 0 a
372piBind :: [(Name, PTerm)] -> PTerm -> PTerm
373piBind [] t = t
374piBind ((n, ty):ns) t = PPi Exp n ty (piBind ns t)
376-- Dealing with implicit arguments
378-- Add implicit Pi bindings for any names in the term which appear in an
379-- argument position.
381implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
382implicitise syn ist tm
383 = let uvars = using syn
384 pvars = syn_params syn
385 (declimps, ns') = execState (imps True [] tm) ([], [])
386 ns = ns' \\ map fst pvars in
387 if null ns
388 then (tm, reverse declimps)
389 else implicitise syn ist (pibind uvars ns tm)
390 where
391 imps top env (PApp f as)
392 = do (decls, ns) <- get
393 let isn = concatMap (namesIn ist) (map getTm as)
394 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
395 imps top env (PPi Imp n ty sc)
396 = do let isn = namesIn ist ty \\ [n]
397 (decls , ns) <- get
398 put (PImp n ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
399 imps True (n:env) sc
400 imps top env (PPi Exp n ty sc)
401 = do let isn = (namesIn ist ty ++ case sc of
402 (PRef x) -> namesIn ist sc
403 _ -> []) \\ [n]
404 (decls, ns) <- get -- ignore decls in HO types
405 put (PExp ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
406 imps True (n:env) sc
407 imps top env (PPair l r)
408 = do (decls, ns) <- get
409 put (decls, nub (ns ++ namesIn ist l ++ namesIn ist r))
410 imps top env (PLam n ty sc)
411 = do imps False env ty
412 imps False (n:env) sc
413 imps top env (PHidden tm) = imps False env tm
414 imps top env _ = return ()
416 pibind using [] sc = sc
417 pibind using (n:ns) sc = case lookup n using of
418 Just ty -> PPi Imp n ty (pibind using ns sc)
419 Nothing -> PPi Imp n Placeholder (pibind using ns sc)
421-- Add implicit arguments in function calls
423addImpl :: IState -> PTerm -> PTerm
424addImpl ist ptm = ai [] ptm
425 where
426 ai env (PRef f) = aiFn env (PRef f) []
427 ai env (PApp (PRef f) as)
428 = let as' = map (fmap (ai env)) as in
429 aiFn env (PRef f) as'
430 ai env (PApp f as) = let f' = ai env f
431 as' = map (fmap (ai env)) as in
432 aiFn env f' as'
433 ai env (PLam n ty sc) = let ty' = ai env ty
434 sc' = ai (n:env) sc in
435 PLam n ty' sc'
436 ai env (PPi p n ty sc) = let ty' = ai env ty
437 sc' = ai (n:env) sc in
438 PPi p n ty' sc'
439 ai env (PHidden tm) = PHidden (ai env tm)
440 ai env tm = tm
442 aiFn env (PRef f) as | not (f `elem` env)
443 = case lookupCtxt f (idris_implicits ist) of
444 Just ns -> pApp (length ns) (PRef f) (insertImpl ns as)
445 Nothing -> pApp 1 (PRef f) as
446 aiFn env f as = pApp 1 f as
448 pApp a f [] = f
449 pApp a f as = let rest = drop a as in
450 appRest (PApp f (take a as)) rest
452 appRest f [] = f
453 appRest f (a : as) = appRest (PApp f [a]) as
455 insertImpl :: [PArg] -> [PArg] -> [PArg]
456 insertImpl (PExp ty : ps) (PExp tm : given) =
457 PExp tm : insertImpl ps given
458 insertImpl (PImp n ty : ps) given =
459 case find n given [] of
460 Just (tm, given') -> PImp n tm : insertImpl ps given'
461 Nothing -> PImp n Placeholder : insertImpl ps given
462 insertImpl expected [] = []
463 insertImpl [] given = given
465 find n [] acc = Nothing
466 find n (PImp n' t : gs) acc
467 | n == n' = Just (t, reverse acc ++ gs)
468 find n (g : gs) acc = find n gs (g : acc)
470-- Debugging/logging stuff
472dumpDecls :: [PDecl] -> String
473dumpDecls [] = ""
474dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
476dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
477dumpDecl (PTy _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
478dumpDecl (PClauses _ n cs) = "pat\t" ++ showSep "\n\t" (map (showCImp True) cs)
479dumpDecl (PData _ d) = showDImp True d
480dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
481dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
482-- dumpDecl (PImport i) = "import " ++ i