git.iko.soy/Idris-dev
on 7ea4422 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
443 lines 15 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 imported :: [FilePath],
33 idris_prims :: [(Name, ([E.Name], E.Term))]
34 }
36idrisInit = IState emptyContext [] emptyContext "" defaultOpts 0 [] []
38-- The monad for the main REPL - reading and processing files and updating
39-- global state (hence the IO inner monad).
40type Idris a = StateT IState IO a
42getContext :: Idris Context
43getContext = do i <- get; return (tt_ctxt i)
45getIState :: Idris IState
46getIState = get
48putIState :: IState -> Idris ()
49putIState = put
51getName :: Idris Int
52getName = do i <- get;
53 let idx = idris_name i;
54 put (i { idris_name = idx + 1 })
55 return idx
57setContext :: Context -> Idris ()
58setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
60updateContext :: (Context -> Context) -> Idris ()
61updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
63iputStrLn :: String -> Idris ()
64iputStrLn = lift.putStrLn
66setLogLevel :: Int -> Idris ()
67setLogLevel l = do i <- get
68 let opts = idris_options i
69 let opt' = opts { opt_logLevel = l }
70 put (i { idris_options = opt' } )
72logLevel :: Idris Int
73logLevel = do i <- get
74 return (opt_logLevel (idris_options i))
76logLvl :: Int -> String -> Idris ()
77logLvl l str = do i <- get
78 let lvl = opt_logLevel (idris_options i)
79 when (lvl >= l)
80 $ do lift (putStrLn str)
81 put (i { idris_log = idris_log i ++ str ++ "\n" } )
83iLOG :: String -> Idris ()
84iLOG = logLvl 1
86-- Commands in the REPL
88data Command = Quit | Help | Eval PTerm
89 | Compile String
90 | TTShell
91 | NOP
93-- Parsed declarations
95data Fixity = Infixl { prec :: Int }
96 | Infixr { prec :: Int }
97 | InfixN { prec :: Int }
98 | PrefixN { prec :: Int }
99 deriving Eq
101instance Show Fixity where
102 show (Infixl i) = "infixl " ++ show i
103 show (Infixr i) = "infixr " ++ show i
104 show (InfixN i) = "infix " ++ show i
105 show (PrefixN i) = "prefix " ++ show i
107data FixDecl = Fix Fixity String
108 deriving (Show, Eq)
110instance Ord FixDecl where
111 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
113data Plicity = Imp | Exp deriving Show
115data PDecl' t = PFix Fixity [String] -- fixity declaration
116 | PTy Name t -- type declaration
117 | PClauses Name [PClause' t] -- pattern clause
118 | PData (PData' t) -- data declaration
119 | PParams [(Name, PTerm)] [PDecl' t] -- params block
120 | PImport String
121 deriving Functor
123data PClause' t = PClause Name t t [PDecl]
124 deriving Functor
126data PData' t = PDatadecl { d_name :: Name,
127 d_tcon :: t,
128 d_cons :: [(Name, t)] }
129 deriving Functor
131-- Handy to get a free function for applying PTerm -> PTerm functions
132-- across a program, by deriving Functor
134type PDecl = PDecl' PTerm
135type PData = PData' PTerm
136type PClause = PClause' PTerm
138-- get all the names declared in a decl
140declared :: PDecl -> [Name]
141declared (PFix _ _) = []
142declared (PTy n t) = [n]
143declared (PClauses n _) = [] -- not a declaration
144declared (PData (PDatadecl n _ ts)) = n : map fst ts
145declared (PParams _ ds) = concatMap declared ds
146declared (PImport _) = []
148-- High level language terms
149--
150data PTerm = PQuote Raw
151 | PRef Name
152 | PLam Name PTerm PTerm
153 | PPi Plicity Name PTerm PTerm
154 | PLet Name PTerm PTerm PTerm -- not implemented yet
155 | PApp PTerm [PArg]
156 | PTrue
157 | PFalse
158 | PPair PTerm PTerm
159 | PHidden PTerm -- irrelevant or hidden pattern
160 | PSet
161 | PConstant Const
162 | Placeholder
163 | PDoBlock [PDo]
164 | PReturn
165 | PElabError String -- error to report on elaboration
167data PDo = DoExp PTerm
168 | DoBind Name PTerm
169 | DoLet Name PTerm
171data PArg' t = PImp { pname :: Name, getTm :: t }
172 | PExp { getTm :: t }
173 deriving (Show, Functor)
175type PArg = PArg' PTerm
177-- Syntactic sugar info (TODO: namespaces, modules)
179data DSL = DSL { dsl_bind :: Name,
180 dsl_return :: Name }
181 deriving Show
183initDSL = DSL (UN ["io_bind"]) (UN ["io_return"])
185data SyntaxInfo = Syn { using :: [(Name, PTerm)],
186 syn_params :: [(Name, PTerm)],
187 dsl_info :: DSL }
188 deriving Show
190defaultSyntax = Syn [] [] initDSL
192--- Pretty printing declarations and terms
194instance Show PTerm where
195 show tm = showImp False tm
197instance Show PDecl where
198 show (PFix f ops) = show f ++ " " ++ showSep ", " ops
199 show (PTy n ty) = show n ++ " : " ++ show ty
200 show (PClauses n c) = showSep "\n" (map show c)
201 show (PData d) = show d
203instance Show PClause where
204 show c = showCImp False c
206instance Show PData where
207 show d = showDImp False d
209showCImp :: Bool -> PClause -> String
210showCImp impl (PClause n l r w) = showImp impl l ++ " = " ++ showImp impl r
211 ++ " where " ++ show w
212showDImp :: Bool -> PData -> String
213showDImp impl (PDatadecl n ty cons)
214 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
215 ++ showSep "\n\t| "
216 (map (\ (n, t) -> show n ++ " : " ++ showImp impl t) cons)
218getImps :: [PArg] -> [(Name, PTerm)]
219getImps [] = []
220getImps (PImp n tm : xs) = (n, tm) : getImps xs
221getImps (_ : xs) = getImps xs
223getExps :: [PArg] -> [PTerm]
224getExps [] = []
225getExps (PExp tm : xs) = tm : getExps xs
226getExps (_ : xs) = getExps xs
228getAll :: [PArg] -> [PTerm]
229getAll = map getTm
231showImp :: Bool -> PTerm -> String
232showImp impl tm = se 10 tm where
233 se p (PQuote r) = "![" ++ show r ++ "]"
234 se p (PRef n) = show n
235 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
236 se p (PPi Exp n ty sc)
237 | n `elem` allNamesIn sc = bracket p 2 $
238 "(" ++ show n ++ " : " ++ se 10 ty ++
239 ") -> " ++ se 10 sc
240 | otherwise = bracket p 2 $ se 0 ty ++ " -> " ++ se 10 sc
241 se p (PPi Imp n ty sc)
242 | impl = bracket p 2 $ "{" ++ show n ++ " : " ++ se 10 ty ++
243 "} -> " ++ se 10 sc
244 | otherwise = se 10 sc
245 se p (PApp (PRef f) [])
246 | not impl = show f
247 se p (PApp (PRef op@(UN [f:_])) args)
248 | length (getExps args) == 2 && not impl && not (isAlpha f)
249 = let [l, r] = getExps args in
250 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
251 se p (PApp f as)
252 = let (imps, args) = (getImps as, getExps as) in
253 bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")
254 ++ concatMap seArg args
255 se p (PHidden tm) = "." ++ se 0 tm
256 se p PTrue = "()"
257 se p PFalse = "_|_"
258 se p (PPair l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
259 se p PSet = "Set"
260 se p (PConstant c) = show c
261 se p Placeholder = "_"
263 seArg arg = " " ++ se 0 arg
264 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
266 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
267 | otherwise = str
269allNamesIn :: PTerm -> [Name]
270allNamesIn tm = nub $ ni [] tm
271 where
272 ni env (PRef n)
273 | not (n `elem` env) = [n]
274 ni env (PApp f as) = ni env f ++ concatMap (ni env) (map getTm as)
275 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
276 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
277 ni env (PHidden tm) = ni env tm
278 ni env _ = []
280namesIn :: IState -> PTerm -> [Name]
281namesIn ist tm = nub $ ni [] tm
282 where
283 ni env (PRef n)
284 | not (n `elem` env)
285 = case lookupCtxt n (idris_implicits ist) of
286 Nothing -> [n]
287 _ -> []
288 ni env (PApp f as) = ni env f ++ concatMap (ni env) (map getTm as)
289 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
290 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
291 ni env (PHidden tm) = ni env tm
292 ni env _ = []
294-- For inferring types of things
296inferTy = MN 0 "__Infer"
297inferCon = MN 0 "__infer"
298inferDecl = PDatadecl inferTy
299 PSet
300 [(inferCon, PPi Imp (MN 0 "A") PSet (
301 PPi Exp (MN 0 "a") (PRef (MN 0 "A"))
302 (PRef inferTy)))]
304infTerm t = PApp (PRef inferCon) [PImp (MN 0 "A") Placeholder, PExp t]
305infP = P (TCon 0) inferTy (Set 0)
307getInferTerm, getInferType :: Term -> Term
308getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
309getInferTerm (App (App _ _) tm) = tm
310getInferTerm tm = error ("getInferTerm " ++ show tm)
312getInferType (Bind n b sc) = Bind n b $ getInferType sc
313getInferType (App (App _ ty) _) = ty
315-- Handy primitives: Unit, False, Pair, MkPair
317unitTy = MN 0 "__Unit"
318unitCon = MN 0 "__II"
319unitDecl = PDatadecl unitTy PSet
320 [(unitCon, PRef unitTy)]
322falseTy = MN 0 "__False"
323falseDecl = PDatadecl falseTy PSet []
325pairTy = MN 0 "__Pair"
326pairCon = MN 0 "__MkPair"
327pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)
328 [(pairCon, PPi Imp (n "A") PSet (
329 PPi Imp (n "B") PSet (
330 PPi Exp (n "a") (PRef (n "A")) (
331 PPi Exp (n "b") (PRef (n "B"))
332 (PApp (PRef pairTy) [PExp (PRef (n "A")),
333 PExp (PRef (n "B"))])))))]
334 where n a = MN 0 a
336piBind :: [(Name, PTerm)] -> PTerm -> PTerm
337piBind [] t = t
338piBind ((n, ty):ns) t = PPi Exp n ty (piBind ns t)
340-- Dealing with implicit arguments
342-- Add implicit Pi bindings for any names in the term which appear in an
343-- argument position.
345implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
346implicitise syn ist tm
347 = let uvars = using syn
348 pvars = syn_params syn
349 (declimps, ns') = execState (imps True [] tm) ([], [])
350 ns = ns' \\ map fst pvars in
351 if null ns
352 then (tm, reverse declimps)
353 else implicitise syn ist (pibind uvars ns tm)
354 where
355 imps top env (PApp f as)
356 = do (decls, ns) <- get
357 let isn = concatMap (namesIn ist) (map getTm as)
358 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
359 imps top env (PPi Imp n ty sc)
360 = do let isn = namesIn ist ty \\ [n]
361 (decls , ns) <- get
362 put (PImp n ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
363 imps True (n:env) sc
364 imps top env (PPi Exp n ty sc)
365 = do let isn = (namesIn ist ty ++ case sc of
366 (PRef x) -> namesIn ist sc
367 _ -> []) \\ [n]
368 (decls, ns) <- get -- ignore decls in HO types
369 put (PExp ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
370 imps True (n:env) sc
371 imps top env (PLam n ty sc)
372 = do imps False env ty
373 imps False (n:env) sc
374 imps top env (PHidden tm) = imps False env tm
375 imps top env _ = return ()
377 pibind using [] sc = sc
378 pibind using (n:ns) sc = case lookup n using of
379 Just ty -> PPi Imp n ty (pibind using ns sc)
380 Nothing -> PPi Imp n Placeholder (pibind using ns sc)
382-- Add implicit arguments in function calls
384addImpl :: IState -> PTerm -> PTerm
385addImpl ist ptm = ai [] ptm
386 where
387 ai env (PRef f) = aiFn env (PRef f) []
388 ai env (PApp (PRef f) as)
389 = let as' = map (fmap (ai env)) as in
390 aiFn env (PRef f) as'
391 ai env (PApp f as) = let f' = ai env f
392 as' = map (fmap (ai env)) as in
393 aiFn env f' as'
394 ai env (PLam n ty sc) = let ty' = ai env ty
395 sc' = ai (n:env) sc in
396 PLam n ty' sc'
397 ai env (PPi p n ty sc) = let ty' = ai env ty
398 sc' = ai (n:env) sc in
399 PPi p n ty' sc'
400 ai env (PHidden tm) = PHidden (ai env tm)
401 ai env tm = tm
403 aiFn env (PRef f) as | not (f `elem` env)
404 = case lookupCtxt f (idris_implicits ist) of
405 Just ns -> pApp (length ns) (PRef f) (insertImpl ns as)
406 Nothing -> pApp 1 (PRef f) as
407 aiFn env f as = pApp 1 f as
409 pApp a f [] = f
410 pApp a f as = let rest = drop a as in
411 appRest (PApp f (take a as)) rest
413 appRest f [] = f
414 appRest f (a : as) = appRest (PApp f [a]) as
416 insertImpl :: [PArg] -> [PArg] -> [PArg]
417 insertImpl (PExp ty : ps) (PExp tm : given) =
418 PExp tm : insertImpl ps given
419 insertImpl (PImp n ty : ps) given =
420 case find n given [] of
421 Just (tm, given') -> PImp n ty : insertImpl ps given'
422 Nothing -> PImp n Placeholder : insertImpl ps given
423 insertImpl expected [] = []
424 insertImpl [] given = given
426 find n [] acc = Nothing
427 find n (PImp n' t : gs) acc
428 | n == n' = Just (t, reverse acc ++ gs)
429 find n (g : gs) acc = find n gs (g : acc)
431-- Debugging/logging stuff
433dumpDecls :: [PDecl] -> String
434dumpDecls [] = ""
435dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
437dumpDecl (PFix f ops) = show f ++ " " ++ showSep ", " ops
438dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
439dumpDecl (PClauses n cs) = "pat\t" ++ showSep "\n\t" (map (showCImp True) cs)
440dumpDecl (PData d) = showDImp True d
441dumpDecl (PParams ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
442dumpDecl (PImport i) = "import " ++ i