git.iko.soy/Idris-dev
on 2402885 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
471 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 | Expr Name
207 deriving Show
209initDSL = DSL (UN ["io_bind"]) (UN ["io_return"])
211data SyntaxInfo = Syn { using :: [(Name, PTerm)],
212 syn_params :: [(Name, PTerm)],
213 dsl_info :: DSL }
214 deriving Show
216defaultSyntax = Syn [] [] initDSL
218--- Pretty printing declarations and terms
220instance Show PTerm where
221 show tm = showImp False tm
223instance Show PDecl where
224 show (PFix f ops) = show f ++ " " ++ showSep ", " ops
225 show (PTy n ty) = show n ++ " : " ++ show ty
226 show (PClauses n c) = showSep "\n" (map show c)
227 show (PData d) = show d
229instance Show PClause where
230 show c = showCImp False c
232instance Show PData where
233 show d = showDImp False d
235showCImp :: Bool -> PClause -> String
236showCImp impl (PClause n l r w) = showImp impl l ++ " = " ++ showImp impl r
237 ++ " where " ++ show w
238showDImp :: Bool -> PData -> String
239showDImp impl (PDatadecl n ty cons)
240 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
241 ++ showSep "\n\t| "
242 (map (\ (n, t) -> show n ++ " : " ++ showImp impl t) cons)
244getImps :: [PArg] -> [(Name, PTerm)]
245getImps [] = []
246getImps (PImp n tm : xs) = (n, tm) : getImps xs
247getImps (_ : xs) = getImps xs
249getExps :: [PArg] -> [PTerm]
250getExps [] = []
251getExps (PExp tm : xs) = tm : getExps xs
252getExps (_ : xs) = getExps xs
254getAll :: [PArg] -> [PTerm]
255getAll = map getTm
257showImp :: Bool -> PTerm -> String
258showImp impl tm = se 10 tm where
259 se p (PQuote r) = "![" ++ show r ++ "]"
260 se p (PRef n) = show n
261 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
262 se p (PPi Exp n ty sc)
263 | n `elem` allNamesIn sc = bracket p 2 $
264 "(" ++ show n ++ " : " ++ se 10 ty ++
265 ") -> " ++ se 10 sc
266 | otherwise = bracket p 2 $ se 0 ty ++ " -> " ++ se 10 sc
267 se p (PPi Imp n ty sc)
268 | impl = bracket p 2 $ "{" ++ show n ++ " : " ++ se 10 ty ++
269 "} -> " ++ se 10 sc
270 | otherwise = se 10 sc
271 se p (PApp (PRef f) [])
272 | not impl = show f
273 se p (PApp (PRef op@(UN [f:_])) args)
274 | length (getExps args) == 2 && not impl && not (isAlpha f)
275 = let [l, r] = getExps args in
276 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
277 se p (PApp f as)
278 = let (imps, args) = (getImps as, getExps as) in
279 bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")
280 ++ concatMap seArg args
281 se p (PHidden tm) = "." ++ se 0 tm
282 se p PTrue = "()"
283 se p PFalse = "_|_"
284 se p (PPair l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
285 se p PSet = "Set"
286 se p (PConstant c) = show c
287 se p (PMetavar n) = "?" ++ show n
288 se p Placeholder = "_"
290 seArg arg = " " ++ se 0 arg
291 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
293 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
294 | otherwise = str
296allNamesIn :: PTerm -> [Name]
297allNamesIn tm = nub $ ni [] tm
298 where
299 ni env (PRef n)
300 | not (n `elem` env) = [n]
301 ni env (PApp f as) = ni env f ++ concatMap (ni env) (map getTm as)
302 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
303 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
304 ni env (PHidden tm) = ni env tm
305 ni env _ = []
307namesIn :: IState -> PTerm -> [Name]
308namesIn ist tm = nub $ ni [] tm
309 where
310 ni env (PRef n)
311 | not (n `elem` env)
312 = case lookupCtxt n (idris_implicits ist) of
313 Nothing -> [n]
314 _ -> []
315 ni env (PApp f as) = ni env f ++ concatMap (ni env) (map getTm as)
316 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
317 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
318 ni env (PHidden tm) = ni env tm
319 ni env _ = []
321-- For inferring types of things
323inferTy = MN 0 "__Infer"
324inferCon = MN 0 "__infer"
325inferDecl = PDatadecl inferTy
326 PSet
327 [(inferCon, PPi Imp (MN 0 "A") PSet (
328 PPi Exp (MN 0 "a") (PRef (MN 0 "A"))
329 (PRef inferTy)))]
331infTerm t = PApp (PRef inferCon) [PImp (MN 0 "A") Placeholder, PExp t]
332infP = P (TCon 0) inferTy (Set 0)
334getInferTerm, getInferType :: Term -> Term
335getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
336getInferTerm (App (App _ _) tm) = tm
337getInferTerm tm = error ("getInferTerm " ++ show tm)
339getInferType (Bind n b sc) = Bind n b $ getInferType sc
340getInferType (App (App _ ty) _) = ty
342-- Handy primitives: Unit, False, Pair, MkPair, mkForeign
344unitTy = MN 0 "__Unit"
345unitCon = MN 0 "__II"
346unitDecl = PDatadecl unitTy PSet
347 [(unitCon, PRef unitTy)]
349falseTy = MN 0 "__False"
350falseDecl = PDatadecl falseTy PSet []
352pairTy = MN 0 "__Pair"
353pairCon = MN 0 "__MkPair"
354pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
355 [(pairCon, PPi Imp (n "A") PSet (
356 PPi Imp (n "B") PSet (
357 PPi Exp (n "a") (PRef (n "A")) (
358 PPi Exp (n "b") (PRef (n "B"))
359 (PApp (PRef pairTy) [PExp (PRef (n "A")),
360 PExp (PRef (n "B"))])))))]
361 where n a = MN 0 a
363piBind :: [(Name, PTerm)] -> PTerm -> PTerm
364piBind [] t = t
365piBind ((n, ty):ns) t = PPi Exp n ty (piBind ns t)
367-- Dealing with implicit arguments
369-- Add implicit Pi bindings for any names in the term which appear in an
370-- argument position.
372implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
373implicitise syn ist tm
374 = let uvars = using syn
375 pvars = syn_params syn
376 (declimps, ns') = execState (imps True [] tm) ([], [])
377 ns = ns' \\ map fst pvars in
378 if null ns
379 then (tm, reverse declimps)
380 else implicitise syn ist (pibind uvars ns tm)
381 where
382 imps top env (PApp f as)
383 = do (decls, ns) <- get
384 let isn = concatMap (namesIn ist) (map getTm as)
385 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
386 imps top env (PPi Imp n ty sc)
387 = do let isn = namesIn ist ty \\ [n]
388 (decls , ns) <- get
389 put (PImp n ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
390 imps True (n:env) sc
391 imps top env (PPi Exp n ty sc)
392 = do let isn = (namesIn ist ty ++ case sc of
393 (PRef x) -> namesIn ist sc
394 _ -> []) \\ [n]
395 (decls, ns) <- get -- ignore decls in HO types
396 put (PExp ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
397 imps True (n:env) sc
398 imps top env (PLam n ty sc)
399 = do imps False env ty
400 imps False (n:env) sc
401 imps top env (PHidden tm) = imps False env tm
402 imps top env _ = return ()
404 pibind using [] sc = sc
405 pibind using (n:ns) sc = case lookup n using of
406 Just ty -> PPi Imp n ty (pibind using ns sc)
407 Nothing -> PPi Imp n Placeholder (pibind using ns sc)
409-- Add implicit arguments in function calls
411addImpl :: IState -> PTerm -> PTerm
412addImpl ist ptm = ai [] ptm
413 where
414 ai env (PRef f) = aiFn env (PRef f) []
415 ai env (PApp (PRef f) as)
416 = let as' = map (fmap (ai env)) as in
417 aiFn env (PRef f) as'
418 ai env (PApp f as) = let f' = ai env f
419 as' = map (fmap (ai env)) as in
420 aiFn env f' as'
421 ai env (PLam n ty sc) = let ty' = ai env ty
422 sc' = ai (n:env) sc in
423 PLam n ty' sc'
424 ai env (PPi p n ty sc) = let ty' = ai env ty
425 sc' = ai (n:env) sc in
426 PPi p n ty' sc'
427 ai env (PHidden tm) = PHidden (ai env tm)
428 ai env tm = tm
430 aiFn env (PRef f) as | not (f `elem` env)
431 = case lookupCtxt f (idris_implicits ist) of
432 Just ns -> pApp (length ns) (PRef f) (insertImpl ns as)
433 Nothing -> pApp 1 (PRef f) as
434 aiFn env f as = pApp 1 f as
436 pApp a f [] = f
437 pApp a f as = let rest = drop a as in
438 appRest (PApp f (take a as)) rest
440 appRest f [] = f
441 appRest f (a : as) = appRest (PApp f [a]) as
443 insertImpl :: [PArg] -> [PArg] -> [PArg]
444 insertImpl (PExp ty : ps) (PExp tm : given) =
445 PExp tm : insertImpl ps given
446 insertImpl (PImp n ty : ps) given =
447 case find n given [] of
448 Just (tm, given') -> PImp n ty : insertImpl ps given'
449 Nothing -> PImp n Placeholder : insertImpl ps given
450 insertImpl expected [] = []
451 insertImpl [] given = given
453 find n [] acc = Nothing
454 find n (PImp n' t : gs) acc
455 | n == n' = Just (t, reverse acc ++ gs)
456 find n (g : gs) acc = find n gs (g : acc)
458-- Debugging/logging stuff
460dumpDecls :: [PDecl] -> String
461dumpDecls [] = ""
462dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
464dumpDecl (PFix f ops) = show f ++ " " ++ showSep ", " ops
465dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
466dumpDecl (PClauses n cs) = "pat\t" ++ showSep "\n\t" (map (showCImp True) cs)
467dumpDecl (PData d) = showDImp True d
468dumpDecl (PParams ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
469dumpDecl (PSyntax syn) = "syntax " ++ show syn
470-- dumpDecl (PImport i) = "import " ++ i