git.iko.soy/Idris-dev
on bf368ab help sign in
Idris-dev/src/Idris/AbsSyntax.hs
506 lines 17 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] t [PDecl]
144 | PWith Name t [t] t [PDecl]
145 deriving Functor
147data PData' t = PDatadecl { d_name :: Name,
148 d_tcon :: t,
149 d_cons :: [(Name, t, FC)] }
150 deriving Functor
152-- Handy to get a free function for applying PTerm -> PTerm functions
153-- across a program, by deriving Functor
155type PDecl = PDecl' PTerm
156type PData = PData' PTerm
157type PClause = PClause' PTerm
159-- get all the names declared in a decl
161declared :: PDecl -> [Name]
162declared (PFix _ _ _) = []
163declared (PTy _ n t) = [n]
164declared (PClauses _ n _) = [] -- not a declaration
165declared (PData _ (PDatadecl n _ ts)) = n : map fstt ts
166 where fstt (a, _, _) = a
167declared (PParams _ _ ds) = concatMap declared ds
168-- declared (PImport _) = []
170-- High level language terms
171--
172data PTerm = PQuote Raw
173 | PRef FC Name
174 | PLam Name PTerm PTerm
175 | PPi Plicity Name PTerm PTerm
176 | PLet Name PTerm PTerm PTerm -- not implemented yet
177 | PApp FC PTerm [PArg]
178 | PTrue FC
179 | PFalse FC
180 | PPair FC PTerm PTerm
181 | PHidden PTerm -- irrelevant or hidden pattern
182 | PSet
183 | PConstant Const
184 | Placeholder
185 | PDoBlock [PDo]
186 | PReturn FC
187 | PMetavar Name
188 | PElabError String -- error to report on elaboration
190data PDo = DoExp FC PTerm
191 | DoBind FC Name PTerm
192 | DoLet FC Name PTerm
194data PArg' t = PImp { pname :: Name, getTm :: t }
195 | PExp { getTm :: t }
196 deriving (Show, Functor)
198type PArg = PArg' PTerm
200-- Syntactic sugar info (TODO: namespaces, modules)
202data DSL = DSL { dsl_bind :: Name,
203 dsl_return :: Name }
204 deriving Show
206data Syntax = Rule [SSymbol] PTerm
207 deriving Show
209data SSymbol = Keyword Name
210 | Symbol String
211 | Expr Name
212 deriving Show
214initDSL = DSL (UN ["io_bind"]) (UN ["io_return"])
216data SyntaxInfo = Syn { using :: [(Name, PTerm)],
217 syn_params :: [(Name, PTerm)],
218 dsl_info :: DSL }
219 deriving Show
221defaultSyntax = Syn [] [] initDSL
223--- Pretty printing declarations and terms
225instance Show PTerm where
226 show tm = showImp False tm
228instance Show PDecl where
229 show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
230 show (PTy _ n ty) = show n ++ " : " ++ show ty
231 show (PClauses _ n c) = showSep "\n" (map show c)
232 show (PData _ d) = show d
234instance Show PClause where
235 show c = showCImp True c
237instance Show PData where
238 show d = showDImp False d
240showCImp :: Bool -> PClause -> String
241showCImp impl (PClause n l ws r w)
242 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
243 ++ " where " ++ show w
244 where
245 showWs [] = ""
246 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
247showCImp impl (PWith n l ws r w)
248 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
249 ++ " { " ++ show w ++ " } "
250 where
251 showWs [] = ""
252 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
255showDImp :: Bool -> PData -> String
256showDImp impl (PDatadecl n ty cons)
257 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
258 ++ showSep "\n\t| "
259 (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
261getImps :: [PArg] -> [(Name, PTerm)]
262getImps [] = []
263getImps (PImp n tm : xs) = (n, tm) : getImps xs
264getImps (_ : xs) = getImps xs
266getExps :: [PArg] -> [PTerm]
267getExps [] = []
268getExps (PExp tm : xs) = tm : getExps xs
269getExps (_ : xs) = getExps xs
271getAll :: [PArg] -> [PTerm]
272getAll = map getTm
274showImp :: Bool -> PTerm -> String
275showImp impl tm = se 10 tm where
276 se p (PQuote r) = "![" ++ show r ++ "]"
277 se p (PRef _ n) = show n
278 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
279 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
280 " in " ++ se 10 sc
281 se p (PPi Exp n ty sc)
282 | n `elem` allNamesIn sc = bracket p 2 $
283 "(" ++ show n ++ " : " ++ se 10 ty ++
284 ") -> " ++ se 10 sc
285 | otherwise = bracket p 2 $ se 0 ty ++ " -> " ++ se 10 sc
286 se p (PPi Imp n ty sc)
287 | impl = bracket p 2 $ "{" ++ show n ++ " : " ++ se 10 ty ++
288 "} -> " ++ se 10 sc
289 | otherwise = se 10 sc
290 se p (PApp _ (PRef _ f) [])
291 | not impl = show f
292 se p (PApp _ (PRef _ op@(UN [f:_])) args)
293 | length (getExps args) == 2 && not impl && not (isAlpha f)
294 = let [l, r] = getExps args in
295 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
296 se p (PApp _ f as)
297 = let (imps, args) = (getImps as, getExps as) in
298 bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")
299 ++ concatMap seArg args
300 se p (PHidden tm) = "." ++ se 0 tm
301 se p (PTrue _) = "()"
302 se p (PFalse _) = "_|_"
303 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
304 se p PSet = "Set"
305 se p (PConstant c) = show c
306 se p (PMetavar n) = "?" ++ show n
307 se p Placeholder = "_"
309 seArg arg = " " ++ se 0 arg
310 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
312 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
313 | otherwise = str
315allNamesIn :: PTerm -> [Name]
316allNamesIn tm = nub $ ni [] tm
317 where
318 ni env (PRef _ n)
319 | not (n `elem` env) = [n]
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 (PHidden tm) = ni env tm
324 ni env (PPair _ l r) = ni env l ++ ni env r
325 ni env _ = []
327namesIn :: IState -> PTerm -> [Name]
328namesIn ist tm = nub $ ni [] tm
329 where
330 ni env (PRef _ n)
331 | not (n `elem` env)
332 = case lookupCtxt n (idris_implicits ist) of
333 Nothing -> [n]
334 _ -> []
335 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
336 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
337 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
338 ni env (PPair _ l r) = ni env l ++ ni env r
339 ni env (PHidden tm) = ni env tm
340 ni env _ = []
342-- For inferring types of things
344bi = FC "builtin" 0
346inferTy = MN 0 "__Infer"
347inferCon = MN 0 "__infer"
348inferDecl = PDatadecl inferTy
349 PSet
350 [(inferCon, PPi Imp (MN 0 "A") PSet (
351 PPi Exp (MN 0 "a") (PRef bi (MN 0 "A"))
352 (PRef bi inferTy)), bi)]
354infTerm t = PApp bi (PRef bi inferCon) [PImp (MN 0 "A") Placeholder, PExp t]
355infP = P (TCon 0) inferTy (Set 0)
357getInferTerm, getInferType :: Term -> Term
358getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
359getInferTerm (App (App _ _) tm) = tm
360getInferTerm tm = error ("getInferTerm " ++ show tm)
362getInferType (Bind n b sc) = Bind n b $ getInferType sc
363getInferType (App (App _ ty) _) = ty
365-- Handy primitives: Unit, False, Pair, MkPair, mkForeign
368unitTy = MN 0 "__Unit"
369unitCon = MN 0 "__II"
370unitDecl = PDatadecl unitTy PSet
371 [(unitCon, PRef bi unitTy, bi)]
373falseTy = MN 0 "__False"
374falseDecl = PDatadecl falseTy PSet []
376pairTy = UN ["Pair"] -- MN 0 "__Pair"
377pairCon = UN ["MkPair"] -- MN 0 "__MkPair"
378pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
379 [(pairCon, PPi Imp (n "A") PSet (
380 PPi Imp (n "B") PSet (
381 PPi Exp (n "a") (PRef bi (n "A")) (
382 PPi Exp (n "b") (PRef bi (n "B"))
383 (PApp bi (PRef bi pairTy) [PExp (PRef bi (n "A")),
384 PExp (PRef bi (n "B"))])))), bi)]
385 where n a = MN 0 a
387piBind :: [(Name, PTerm)] -> PTerm -> PTerm
388piBind [] t = t
389piBind ((n, ty):ns) t = PPi Exp n ty (piBind ns t)
391-- Dealing with implicit arguments
393-- Add implicit Pi bindings for any names in the term which appear in an
394-- argument position.
396implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
397implicitise syn ist tm
398 = let uvars = using syn
399 pvars = syn_params syn
400 (declimps, ns') = execState (imps True [] tm) ([], [])
401 ns = ns' \\ map fst pvars in
402 if null ns
403 then (tm, reverse declimps)
404 else implicitise syn ist (pibind uvars ns tm)
405 where
406 imps top env (PApp _ f as)
407 = do (decls, ns) <- get
408 let isn = concatMap (namesIn ist) (map getTm as)
409 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
410 imps top env (PPi Imp n ty sc)
411 = do let isn = namesIn ist ty \\ [n]
412 (decls , ns) <- get
413 put (PImp n ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
414 imps True (n:env) sc
415 imps top env (PPi Exp n ty sc)
416 = do let isn = (namesIn ist ty ++ case sc of
417 (PRef _ x) -> namesIn ist sc
418 _ -> []) \\ [n]
419 (decls, ns) <- get -- ignore decls in HO types
420 put (PExp ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
421 imps True (n:env) sc
422 imps top env (PPair _ l r)
423 = do (decls, ns) <- get
424 put (decls, nub (ns ++ namesIn ist l ++ namesIn ist r))
425 imps top env (PLam n ty sc)
426 = do imps False env ty
427 imps False (n:env) sc
428 imps top env (PHidden tm) = imps False env tm
429 imps top env _ = return ()
431 pibind using [] sc = sc
432 pibind using (n:ns) sc = case lookup n using of
433 Just ty -> PPi Imp n ty (pibind using ns sc)
434 Nothing -> PPi Imp n Placeholder (pibind using ns sc)
436-- Add implicit arguments in function calls
438addImpl :: IState -> PTerm -> PTerm
439addImpl ist ptm = ai [] ptm
440 where
441 ai env (PRef fc f) = aiFn fc env (PRef fc f) []
442 ai env (PPair fc l r) = let l' = ai env l
443 r' = ai env r in
444 PPair fc l' r'
445 ai env (PApp fc (PRef _ f) as)
446 = let as' = map (fmap (ai env)) as in
447 aiFn fc env (PRef fc f) as'
448 ai env (PApp fc f as) = let f' = ai env f
449 as' = map (fmap (ai env)) as in
450 aiFn fc env f' as'
451 ai env (PLam n ty sc) = let ty' = ai env ty
452 sc' = ai (n:env) sc in
453 PLam n ty' sc'
454 ai env (PLet n ty val sc)
455 = let ty' = ai env ty
456 val' = ai env val
457 sc' = ai (n:env) sc in
458 PLet n ty' val' sc'
459 ai env (PPi p n ty sc) = let ty' = ai env ty
460 sc' = ai (n:env) sc in
461 PPi p n ty' sc'
462 ai env (PHidden tm) = PHidden (ai env tm)
463 ai env tm = tm
465 aiFn _ env (PRef fc f) as | not (f `elem` env)
466 = case lookupCtxt f (idris_implicits ist) of
467 Just ns -> pApp fc (length ns) (PRef fc f) (insertImpl ns as)
468 Nothing -> pApp fc 1 (PRef fc f) as
469 aiFn fc env f as = pApp fc 1 f as
471 pApp fc a f [] = f
472 pApp fc a f as = let rest = drop a as in
473 appRest fc (PApp fc f (take a as)) rest
475 appRest fc f [] = f
476 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
478 insertImpl :: [PArg] -> [PArg] -> [PArg]
479 insertImpl (PExp ty : ps) (PExp tm : given) =
480 PExp tm : insertImpl ps given
481 insertImpl (PImp n ty : ps) given =
482 case find n given [] of
483 Just (tm, given') -> PImp n tm : insertImpl ps given'
484 Nothing -> PImp n Placeholder : insertImpl ps given
485 insertImpl expected [] = []
486 insertImpl [] given = given
488 find n [] acc = Nothing
489 find n (PImp n' t : gs) acc
490 | n == n' = Just (t, reverse acc ++ gs)
491 find n (g : gs) acc = find n gs (g : acc)
493-- Debugging/logging stuff
495dumpDecls :: [PDecl] -> String
496dumpDecls [] = ""
497dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
499dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
500dumpDecl (PTy _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
501dumpDecl (PClauses _ n cs) = "pat\t" ++ showSep "\n\t" (map (showCImp True) cs)
502dumpDecl (PData _ d) = showDImp True d
503dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
504dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
505-- dumpDecl (PImport i) = "import " ++ i