git.iko.soy/Idris-dev
on 180e979 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
477 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 :: Name -> Idris ()
60checkUndefined n = do i <- getContext
61 case lookupCtxt n i of
62 Just _ -> fail $ show n ++ " already defined"
63 _ -> return ()
65setContext :: Context -> Idris ()
66setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
68updateContext :: (Context -> Context) -> Idris ()
69updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
71addDeferred :: [(Name, Type)] -> Idris ()
72addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n t)) ns
73 i <- get
74 put (i { idris_metavars = map fst ns ++ idris_metavars i })
76solveDeferred :: Name -> Idris ()
77solveDeferred n = do i <- get
78 put (i { idris_metavars = idris_metavars i \\ [n] })
80iputStrLn :: String -> Idris ()
81iputStrLn = lift.putStrLn
83setLogLevel :: Int -> Idris ()
84setLogLevel l = do i <- get
85 let opts = idris_options i
86 let opt' = opts { opt_logLevel = l }
87 put (i { idris_options = opt' } )
89logLevel :: Idris Int
90logLevel = do i <- get
91 return (opt_logLevel (idris_options i))
93logLvl :: Int -> String -> Idris ()
94logLvl l str = do i <- get
95 let lvl = opt_logLevel (idris_options i)
96 when (lvl >= l)
97 $ do lift (putStrLn str)
98 put (i { idris_log = idris_log i ++ str ++ "\n" } )
100iLOG :: String -> Idris ()
101iLOG = logLvl 1
103-- Commands in the REPL
105data Command = Quit | Help | Eval PTerm
106 | Compile String
107 | Metavars
108 | TTShell
109 | NOP
111-- Parsed declarations
113data Fixity = Infixl { prec :: Int }
114 | Infixr { prec :: Int }
115 | InfixN { prec :: Int }
116 | PrefixN { prec :: Int }
117 deriving Eq
119instance Show Fixity where
120 show (Infixl i) = "infixl " ++ show i
121 show (Infixr i) = "infixr " ++ show i
122 show (InfixN i) = "infix " ++ show i
123 show (PrefixN i) = "prefix " ++ show i
125data FixDecl = Fix Fixity String
126 deriving (Show, Eq)
128instance Ord FixDecl where
129 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
131data Plicity = Imp | Exp deriving Show
133data PDecl' t = PFix Fixity [String] -- fixity declaration
134 | PTy Name t -- type declaration
135 | PClauses Name [PClause' t] -- pattern clause
136 | PData (PData' t) -- data declaration
137 | PParams [(Name, PTerm)] [PDecl' t] -- params block
138 | PSyntax Syntax
139 deriving Functor
141data PClause' t = PClause Name t t [PDecl]
142 deriving Functor
144data PData' t = PDatadecl { d_name :: Name,
145 d_tcon :: t,
146 d_cons :: [(Name, t)] }
147 deriving Functor
149-- Handy to get a free function for applying PTerm -> PTerm functions
150-- across a program, by deriving Functor
152type PDecl = PDecl' PTerm
153type PData = PData' PTerm
154type PClause = PClause' PTerm
156-- get all the names declared in a decl
158declared :: PDecl -> [Name]
159declared (PFix _ _) = []
160declared (PTy n t) = [n]
161declared (PClauses n _) = [] -- not a declaration
162declared (PData (PDatadecl n _ ts)) = n : map fst ts
163declared (PParams _ ds) = concatMap declared ds
164-- declared (PImport _) = []
166-- High level language terms
167--
168data PTerm = PQuote Raw
169 | PRef Name
170 | PLam Name PTerm PTerm
171 | PPi Plicity Name PTerm PTerm
172 | PLet Name PTerm PTerm PTerm -- not implemented yet
173 | PApp PTerm [PArg]
174 | PTrue
175 | PFalse
176 | PPair PTerm PTerm
177 | PHidden PTerm -- irrelevant or hidden pattern
178 | PSet
179 | PConstant Const
180 | Placeholder
181 | PDoBlock [PDo]
182 | PReturn
183 | PMetavar Name
184 | PElabError String -- error to report on elaboration
186data PDo = DoExp PTerm
187 | DoBind Name PTerm
188 | DoLet Name PTerm
190data PArg' t = PImp { pname :: Name, getTm :: t }
191 | PExp { getTm :: t }
192 deriving (Show, Functor)
194type PArg = PArg' PTerm
196-- Syntactic sugar info (TODO: namespaces, modules)
198data DSL = DSL { dsl_bind :: Name,
199 dsl_return :: Name }
200 deriving Show
202data Syntax = Rule [SSymbol] PTerm
203 deriving Show
205data SSymbol = Keyword Name
206 | Symbol String
207 | Expr Name
208 deriving Show
210initDSL = DSL (UN ["io_bind"]) (UN ["io_return"])
212data SyntaxInfo = Syn { using :: [(Name, PTerm)],
213 syn_params :: [(Name, PTerm)],
214 dsl_info :: DSL }
215 deriving Show
217defaultSyntax = Syn [] [] initDSL
219--- Pretty printing declarations and terms
221instance Show PTerm where
222 show tm = showImp False tm
224instance Show PDecl where
225 show (PFix f ops) = show f ++ " " ++ showSep ", " ops
226 show (PTy n ty) = show n ++ " : " ++ show ty
227 show (PClauses n c) = showSep "\n" (map show c)
228 show (PData d) = show d
230instance Show PClause where
231 show c = showCImp False c
233instance Show PData where
234 show d = showDImp False d
236showCImp :: Bool -> PClause -> String
237showCImp impl (PClause n l r w) = showImp impl l ++ " = " ++ showImp impl r
238 ++ " where " ++ show w
239showDImp :: Bool -> PData -> String
240showDImp impl (PDatadecl n ty cons)
241 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
242 ++ showSep "\n\t| "
243 (map (\ (n, t) -> show n ++ " : " ++ showImp impl t) cons)
245getImps :: [PArg] -> [(Name, PTerm)]
246getImps [] = []
247getImps (PImp n tm : xs) = (n, tm) : getImps xs
248getImps (_ : xs) = getImps xs
250getExps :: [PArg] -> [PTerm]
251getExps [] = []
252getExps (PExp tm : xs) = tm : getExps xs
253getExps (_ : xs) = getExps xs
255getAll :: [PArg] -> [PTerm]
256getAll = map getTm
258showImp :: Bool -> PTerm -> String
259showImp impl tm = se 10 tm where
260 se p (PQuote r) = "![" ++ show r ++ "]"
261 se p (PRef n) = show n
262 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
263 se p (PPi Exp n ty sc)
264 | n `elem` allNamesIn sc = bracket p 2 $
265 "(" ++ show n ++ " : " ++ se 10 ty ++
266 ") -> " ++ se 10 sc
267 | otherwise = bracket p 2 $ se 0 ty ++ " -> " ++ se 10 sc
268 se p (PPi Imp n ty sc)
269 | impl = bracket p 2 $ "{" ++ show n ++ " : " ++ se 10 ty ++
270 "} -> " ++ se 10 sc
271 | otherwise = se 10 sc
272 se p (PApp (PRef f) [])
273 | not impl = show f
274 se p (PApp (PRef op@(UN [f:_])) args)
275 | length (getExps args) == 2 && not impl && not (isAlpha f)
276 = let [l, r] = getExps args in
277 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
278 se p (PApp f as)
279 = let (imps, args) = (getImps as, getExps as) in
280 bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")
281 ++ concatMap seArg args
282 se p (PHidden tm) = "." ++ se 0 tm
283 se p PTrue = "()"
284 se p PFalse = "_|_"
285 se p (PPair l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
286 se p PSet = "Set"
287 se p (PConstant c) = show c
288 se p (PMetavar n) = "?" ++ show n
289 se p Placeholder = "_"
291 seArg arg = " " ++ se 0 arg
292 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
294 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
295 | otherwise = str
297allNamesIn :: PTerm -> [Name]
298allNamesIn tm = nub $ ni [] tm
299 where
300 ni env (PRef n)
301 | not (n `elem` env) = [n]
302 ni env (PApp f as) = ni env f ++ concatMap (ni env) (map getTm as)
303 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
304 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
305 ni env (PHidden tm) = ni env tm
306 ni env (PPair l r) = ni env l ++ ni env r
307 ni env _ = []
309namesIn :: IState -> PTerm -> [Name]
310namesIn ist tm = nub $ ni [] tm
311 where
312 ni env (PRef n)
313 | not (n `elem` env)
314 = case lookupCtxt n (idris_implicits ist) of
315 Nothing -> [n]
316 _ -> []
317 ni env (PApp f as) = ni env f ++ concatMap (ni env) (map getTm as)
318 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
319 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
320 ni env (PPair l r) = ni env l ++ ni env r
321 ni env (PHidden tm) = ni env tm
322 ni env _ = []
324-- For inferring types of things
326inferTy = MN 0 "__Infer"
327inferCon = MN 0 "__infer"
328inferDecl = PDatadecl inferTy
329 PSet
330 [(inferCon, PPi Imp (MN 0 "A") PSet (
331 PPi Exp (MN 0 "a") (PRef (MN 0 "A"))
332 (PRef inferTy)))]
334infTerm t = PApp (PRef inferCon) [PImp (MN 0 "A") Placeholder, PExp t]
335infP = P (TCon 0) inferTy (Set 0)
337getInferTerm, getInferType :: Term -> Term
338getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
339getInferTerm (App (App _ _) tm) = tm
340getInferTerm tm = error ("getInferTerm " ++ show tm)
342getInferType (Bind n b sc) = Bind n b $ getInferType sc
343getInferType (App (App _ ty) _) = ty
345-- Handy primitives: Unit, False, Pair, MkPair, mkForeign
347unitTy = MN 0 "__Unit"
348unitCon = MN 0 "__II"
349unitDecl = PDatadecl unitTy PSet
350 [(unitCon, PRef unitTy)]
352falseTy = MN 0 "__False"
353falseDecl = PDatadecl falseTy PSet []
355pairTy = MN 0 "__Pair"
356pairCon = MN 0 "__MkPair"
357pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
358 [(pairCon, PPi Imp (n "A") PSet (
359 PPi Imp (n "B") PSet (
360 PPi Exp (n "a") (PRef (n "A")) (
361 PPi Exp (n "b") (PRef (n "B"))
362 (PApp (PRef pairTy) [PExp (PRef (n "A")),
363 PExp (PRef (n "B"))])))))]
364 where n a = MN 0 a
366piBind :: [(Name, PTerm)] -> PTerm -> PTerm
367piBind [] t = t
368piBind ((n, ty):ns) t = PPi Exp n ty (piBind ns t)
370-- Dealing with implicit arguments
372-- Add implicit Pi bindings for any names in the term which appear in an
373-- argument position.
375implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
376implicitise syn ist tm
377 = let uvars = using syn
378 pvars = syn_params syn
379 (declimps, ns') = execState (imps True [] tm) ([], [])
380 ns = ns' \\ map fst pvars in
381 if null ns
382 then (tm, reverse declimps)
383 else implicitise syn ist (pibind uvars ns tm)
384 where
385 imps top env (PApp f as)
386 = do (decls, ns) <- get
387 let isn = concatMap (namesIn ist) (map getTm as)
388 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
389 imps top env (PPi Imp n ty sc)
390 = do let isn = namesIn ist ty \\ [n]
391 (decls , ns) <- get
392 put (PImp n ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
393 imps True (n:env) sc
394 imps top env (PPi Exp n ty sc)
395 = do let isn = (namesIn ist ty ++ case sc of
396 (PRef x) -> namesIn ist sc
397 _ -> []) \\ [n]
398 (decls, ns) <- get -- ignore decls in HO types
399 put (PExp ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
400 imps True (n:env) sc
401 imps top env (PPair l r)
402 = do (decls, ns) <- get
403 put (decls, nub (ns ++ namesIn ist l ++ namesIn ist r))
404 imps top env (PLam n ty sc)
405 = do imps False env ty
406 imps False (n:env) sc
407 imps top env (PHidden tm) = imps False env tm
408 imps top env _ = return ()
410 pibind using [] sc = sc
411 pibind using (n:ns) sc = case lookup n using of
412 Just ty -> PPi Imp n ty (pibind using ns sc)
413 Nothing -> PPi Imp n Placeholder (pibind using ns sc)
415-- Add implicit arguments in function calls
417addImpl :: IState -> PTerm -> PTerm
418addImpl ist ptm = ai [] ptm
419 where
420 ai env (PRef f) = aiFn env (PRef f) []
421 ai env (PApp (PRef f) as)
422 = let as' = map (fmap (ai env)) as in
423 aiFn env (PRef f) as'
424 ai env (PApp f as) = let f' = ai env f
425 as' = map (fmap (ai env)) as in
426 aiFn env f' as'
427 ai env (PLam n ty sc) = let ty' = ai env ty
428 sc' = ai (n:env) sc in
429 PLam n ty' sc'
430 ai env (PPi p n ty sc) = let ty' = ai env ty
431 sc' = ai (n:env) sc in
432 PPi p n ty' sc'
433 ai env (PHidden tm) = PHidden (ai env tm)
434 ai env tm = tm
436 aiFn env (PRef f) as | not (f `elem` env)
437 = case lookupCtxt f (idris_implicits ist) of
438 Just ns -> pApp (length ns) (PRef f) (insertImpl ns as)
439 Nothing -> pApp 1 (PRef f) as
440 aiFn env f as = pApp 1 f as
442 pApp a f [] = f
443 pApp a f as = let rest = drop a as in
444 appRest (PApp f (take a as)) rest
446 appRest f [] = f
447 appRest f (a : as) = appRest (PApp f [a]) as
449 insertImpl :: [PArg] -> [PArg] -> [PArg]
450 insertImpl (PExp ty : ps) (PExp tm : given) =
451 PExp tm : insertImpl ps given
452 insertImpl (PImp n ty : ps) given =
453 case find n given [] of
454 Just (tm, given') -> PImp n ty : insertImpl ps given'
455 Nothing -> PImp n Placeholder : insertImpl ps given
456 insertImpl expected [] = []
457 insertImpl [] given = given
459 find n [] acc = Nothing
460 find n (PImp n' t : gs) acc
461 | n == n' = Just (t, reverse acc ++ gs)
462 find n (g : gs) acc = find n gs (g : acc)
464-- Debugging/logging stuff
466dumpDecls :: [PDecl] -> String
467dumpDecls [] = ""
468dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
470dumpDecl (PFix f ops) = show f ++ " " ++ showSep ", " ops
471dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
472dumpDecl (PClauses n cs) = "pat\t" ++ showSep "\n\t" (map (showCImp True) cs)
473dumpDecl (PData d) = showDImp True d
474dumpDecl (PParams ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
475dumpDecl (PSyntax syn) = "syntax " ++ show syn
476-- dumpDecl (PImport i) = "import " ++ i