git.iko.soy/Idris-dev
on 5fbca2a help sign in
Idris-dev/src/Idris/AbsSyntax.hs
578 lines 20 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, Eq)
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 | PDPair FC PTerm PTerm
182 | PHidden PTerm -- irrelevant or hidden pattern
183 | PSet
184 | PConstant Const
185 | Placeholder
186 | PDoBlock [PDo]
187 | PReturn FC
188 | PMetavar Name
189 | PElabError String -- error to report on elaboration
190 deriving Eq
192data PDo = DoExp FC PTerm
193 | DoBind FC Name PTerm
194 | DoLet FC Name PTerm
195 deriving Eq
197data PArg' t = PImp { pname :: Name, getTm :: t }
198 | PExp { getTm :: t }
199 deriving (Show, Eq, Functor)
201type PArg = PArg' PTerm
203-- Syntactic sugar info (TODO: namespaces, modules)
205data DSL = DSL { dsl_bind :: Name,
206 dsl_return :: Name }
207 deriving Show
209data Syntax = Rule [SSymbol] PTerm
210 deriving Show
212data SSymbol = Keyword Name
213 | Symbol String
214 | Expr Name
215 deriving Show
217initDSL = DSL (UN ["io_bind"]) (UN ["io_return"])
219data SyntaxInfo = Syn { using :: [(Name, PTerm)],
220 syn_params :: [(Name, PTerm)],
221 no_imp :: [Name],
222 dsl_info :: DSL }
223 deriving Show
225defaultSyntax = Syn [] [] [] initDSL
227--- Pretty printing declarations and terms
229instance Show PTerm where
230 show tm = showImp False tm
232instance Show PDecl where
233 show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
234 show (PTy _ n ty) = show n ++ " : " ++ show ty
235 show (PClauses _ n c) = showSep "\n" (map show c)
236 show (PData _ d) = show d
238instance Show PClause where
239 show c = showCImp True c
241instance Show PData where
242 show d = showDImp False d
244showCImp :: Bool -> PClause -> String
245showCImp impl (PClause n l ws r w)
246 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
247 ++ " where " ++ show w
248 where
249 showWs [] = ""
250 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
251showCImp impl (PWith n l ws r w)
252 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
253 ++ " { " ++ show w ++ " } "
254 where
255 showWs [] = ""
256 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
259showDImp :: Bool -> PData -> String
260showDImp impl (PDatadecl n ty cons)
261 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
262 ++ showSep "\n\t| "
263 (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
265getImps :: [PArg] -> [(Name, PTerm)]
266getImps [] = []
267getImps (PImp n tm : xs) = (n, tm) : getImps xs
268getImps (_ : xs) = getImps xs
270getExps :: [PArg] -> [PTerm]
271getExps [] = []
272getExps (PExp tm : xs) = tm : getExps xs
273getExps (_ : xs) = getExps xs
275getAll :: [PArg] -> [PTerm]
276getAll = map getTm
278showImp :: Bool -> PTerm -> String
279showImp impl tm = se 10 tm where
280 se p (PQuote r) = "![" ++ show r ++ "]"
281 se p (PRef _ n) = show n
282 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
283 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
284 " in " ++ se 10 sc
285 se p (PPi Exp n ty sc)
286 | n `elem` allNamesIn sc = bracket p 2 $
287 "(" ++ show n ++ " : " ++ se 10 ty ++
288 ") -> " ++ se 10 sc
289 | otherwise = bracket p 2 $ se 0 ty ++ " -> " ++ se 10 sc
290 se p (PPi Imp n ty sc)
291 | impl = bracket p 2 $ "{" ++ show n ++ " : " ++ se 10 ty ++
292 "} -> " ++ se 10 sc
293 | otherwise = se 10 sc
294 se p (PApp _ (PRef _ f) [])
295 | not impl = show f
296 se p (PApp _ (PRef _ op@(UN [f:_])) args)
297 | length (getExps args) == 2 && not impl && not (isAlpha f)
298 = let [l, r] = getExps args in
299 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
300 se p (PApp _ f as)
301 = let (imps, args) = (getImps as, getExps as) in
302 bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")
303 ++ concatMap seArg args
304 se p (PHidden tm) = "." ++ se 0 tm
305 se p (PTrue _) = "()"
306 se p (PFalse _) = "_|_"
307 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
308 se p (PDPair _ l r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
309 se p PSet = "Set"
310 se p (PConstant c) = show c
311 se p (PMetavar n) = "?" ++ show n
312 se p Placeholder = "_"
314 seArg arg = " " ++ se 0 arg
315 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
317 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
318 | otherwise = str
320allNamesIn :: PTerm -> [Name]
321allNamesIn tm = nub $ ni [] tm
322 where
323 ni env (PRef _ n)
324 | not (n `elem` env) = [n]
325 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
326 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
327 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
328 ni env (PHidden tm) = ni env tm
329 ni env (PPair _ l r) = ni env l ++ ni env r
330 ni env (PDPair _ l r) = ni env l ++ ni env r
331 ni env _ = []
333namesIn :: IState -> PTerm -> [Name]
334namesIn ist tm = nub $ ni [] tm
335 where
336 ni env (PRef _ n)
337 | not (n `elem` env)
338 = case lookupCtxt n (idris_implicits ist) of
339 Nothing -> [n]
340 _ -> []
341 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
342 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
343 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
344 ni env (PPair _ l r) = ni env l ++ ni env r
345 ni env (PDPair _ l r) = ni env l ++ ni env r
346 ni env (PHidden tm) = ni env tm
347 ni env _ = []
349-- For inferring types of things
351bi = FC "builtin" 0
353inferTy = MN 0 "__Infer"
354inferCon = MN 0 "__infer"
355inferDecl = PDatadecl inferTy
356 PSet
357 [(inferCon, PPi Imp (MN 0 "A") PSet (
358 PPi Exp (MN 0 "a") (PRef bi (MN 0 "A"))
359 (PRef bi inferTy)), bi)]
361infTerm t = PApp bi (PRef bi inferCon) [PImp (MN 0 "A") Placeholder, PExp t]
362infP = P (TCon 0) inferTy (Set 0)
364getInferTerm, getInferType :: Term -> Term
365getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
366getInferTerm (App (App _ _) tm) = tm
367getInferTerm tm = error ("getInferTerm " ++ show tm)
369getInferType (Bind n b sc) = Bind n b $ getInferType sc
370getInferType (App (App _ ty) _) = ty
372-- Handy primitives: Unit, False, Pair, MkPair, mkForeign
375unitTy = MN 0 "__Unit"
376unitCon = MN 0 "__II"
377unitDecl = PDatadecl unitTy PSet
378 [(unitCon, PRef bi unitTy, bi)]
380falseTy = MN 0 "__False"
381falseDecl = PDatadecl falseTy PSet []
383pairTy = MN 0 "__Pair"
384pairCon = MN 0 "__MkPair"
385pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
386 [(pairCon, PPi Imp (n "A") PSet (
387 PPi Imp (n "B") PSet (
388 PPi Exp (n "a") (PRef bi (n "A")) (
389 PPi Exp (n "b") (PRef bi (n "B"))
390 (PApp bi (PRef bi pairTy) [PExp (PRef bi (n "A")),
391 PExp (PRef bi (n "B"))])))), bi)]
392 where n a = MN 0 a
394-- Defined in builtins.idr
395sigmaTy = UN ["Sigma"]
396existsCon = UN ["Exists"]
398piBind :: [(Name, PTerm)] -> PTerm -> PTerm
399piBind [] t = t
400piBind ((n, ty):ns) t = PPi Exp n ty (piBind ns t)
402-- Dealing with implicit arguments
404-- Add implicit Pi bindings for any names in the term which appear in an
405-- argument position.
407implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
408implicitise syn ist tm
409 = let uvars = using syn
410 pvars = syn_params syn
411 (declimps, ns') = execState (imps True [] tm) ([], [])
412 ns = ns' \\ (map fst pvars ++ no_imp syn) in
413 if null ns
414 then (tm, reverse declimps)
415 else implicitise syn ist (pibind uvars ns tm)
416 where
417 imps top env (PApp _ f as)
418 = do (decls, ns) <- get
419 let isn = concatMap (namesIn ist) (map getTm as)
420 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
421 imps top env (PPi Imp n ty sc)
422 = do let isn = namesIn ist ty \\ [n]
423 (decls , ns) <- get
424 put (PImp n ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
425 imps True (n:env) sc
426 imps top env (PPi Exp n ty sc)
427 = do let isn = (namesIn ist ty ++ case sc of
428 (PRef _ x) -> namesIn ist sc
429 _ -> []) \\ [n]
430 (decls, ns) <- get -- ignore decls in HO types
431 put (PExp ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
432 imps True (n:env) sc
433 imps top env (PPair _ l r)
434 = do (decls, ns) <- get
435 let isn = namesIn ist l ++ namesIn ist r
436 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
437 imps top env (PDPair _ (PRef _ n) r)
438 = do (decls, ns) <- get
439 let isn = namesIn ist r \\ [n]
440 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
441 imps top env (PDPair _ l r)
442 = do (decls, ns) <- get
443 let isn = namesIn ist l ++ namesIn ist r
444 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
445 imps top env (PLam n ty sc)
446 = do imps False env ty
447 imps False (n:env) sc
448 imps top env (PHidden tm) = imps False env tm
449 imps top env _ = return ()
451 pibind using [] sc = sc
452 pibind using (n:ns) sc = case lookup n using of
453 Just ty -> PPi Imp n ty (pibind using ns sc)
454 Nothing -> PPi Imp n Placeholder (pibind using ns sc)
456-- Add implicit arguments in function calls
458addImpl :: IState -> PTerm -> PTerm
459addImpl ist ptm = ai [] ptm
460 where
461 ai env (PRef fc f) = aiFn fc env (PRef fc f) []
462 ai env (PPair fc l r) = let l' = ai env l
463 r' = ai env r in
464 PPair fc l' r'
465 ai env (PDPair fc l r) = let l' = ai env l
466 r' = ai env r in
467 PDPair fc l' r'
468 ai env (PApp fc (PRef _ f) as)
469 = let as' = map (fmap (ai env)) as in
470 aiFn fc env (PRef fc f) as'
471 ai env (PApp fc f as) = let f' = ai env f
472 as' = map (fmap (ai env)) as in
473 aiFn fc env f' as'
474 ai env (PLam n ty sc) = let ty' = ai env ty
475 sc' = ai (n:env) sc in
476 PLam n ty' sc'
477 ai env (PLet n ty val sc)
478 = let ty' = ai env ty
479 val' = ai env val
480 sc' = ai (n:env) sc in
481 PLet n ty' val' sc'
482 ai env (PPi p n ty sc) = let ty' = ai env ty
483 sc' = ai (n:env) sc in
484 PPi p n ty' sc'
485 ai env (PHidden tm) = PHidden (ai env tm)
486 ai env tm = tm
488 aiFn _ env (PRef fc f) as | not (f `elem` env)
489 = case lookupCtxt f (idris_implicits ist) of
490 Just ns -> pApp fc (length ns) (PRef fc f) (insertImpl ns as)
491 Nothing -> pApp fc 1 (PRef fc f) as
492 aiFn fc env f as = pApp fc 1 f as
494 pApp fc a f [] = f
495 pApp fc a f as = let rest = drop a as in
496 appRest fc (PApp fc f (take a as)) rest
498 appRest fc f [] = f
499 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
501 insertImpl :: [PArg] -> [PArg] -> [PArg]
502 insertImpl (PExp ty : ps) (PExp tm : given) =
503 PExp tm : insertImpl ps given
504 insertImpl (PImp n ty : ps) given =
505 case find n given [] of
506 Just (tm, given') -> PImp n tm : insertImpl ps given'
507 Nothing -> PImp n Placeholder : insertImpl ps given
508 insertImpl expected [] = []
509 insertImpl [] given = given
511 find n [] acc = Nothing
512 find n (PImp n' t : gs) acc
513 | n == n' = Just (t, reverse acc ++ gs)
514 find n (g : gs) acc = find n gs (g : acc)
516-- Debugging/logging stuff
518dumpDecls :: [PDecl] -> String
519dumpDecls [] = ""
520dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
522dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
523dumpDecl (PTy _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
524dumpDecl (PClauses _ n cs) = "pat\t" ++ showSep "\n\t" (map (showCImp True) cs)
525dumpDecl (PData _ d) = showDImp True d
526dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
527dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
528-- dumpDecl (PImport i) = "import " ++ i
530-- syntactic match of a against b, returning pair of variables in a
531-- and what they match. Returns 'Nothing' if not a match.
533matchClause :: PTerm -> PTerm -> Maybe [(Name, PTerm)]
534matchClause x y = match x y where
535 matchArg x y = match (getTm x) (getTm y)
537 match (PApp _ f args) (PApp _ f' args')
538 | length args == length args'
539 = do mf <- match f f'
540 ms <- zipWithM matchArg args args'
541 return (mf ++ concat ms)
542 match (PRef _ n) (PRef _ n') | n == n' = return []
543 | otherwise = Nothing
544 match (PRef _ n) tm = return [(n, tm)]
545 match (PPair _ l r) (PPair _ l' r') = do ml <- match l l'
546 mr <- match r r'
547 return (ml ++ mr)
548 match (PDPair _ l r) (PDPair _ l' r') = do ml <- match l l'
549 mr <- match r r'
550 return (ml ++ mr)
551 match (PTrue _) (PTrue _) = return []
552 match (PFalse _) (PFalse _) = return []
553 match (PReturn _) (PReturn _) = return []
554 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match t t'
555 ms <- match s s'
556 return (mt ++ ms)
557 match (PLam _ t s) (PLam _ t' s') = do mt <- match t t'
558 ms <- match s s'
559 return (mt ++ ms)
560 match (PHidden x) (PHidden y) = match x y
561 match a b | a == b = return []
562 | otherwise = Nothing
564substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
565substMatches [] t = t
566substMatches ((n,tm):ns) t = substMatch n tm (substMatches ns t)
568substMatch :: Name -> PTerm -> PTerm -> PTerm
569substMatch n tm t = sm t where
570 sm (PRef _ n') | n == n' = tm
571 sm (PLam x t sc) = PLam x (sm t) (sm sc)
572 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
573 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
574 sm (PPair f x y) = PPair f (sm x) (sm y)
575 sm (PDPair f x y) = PDPair f (sm x) (sm y)
576 sm (PHidden x) = PHidden (sm x)
577 sm x = x