git.iko.soy/Idris-dev
on 083fc70 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
379 lines 13 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
14data IOption = IOption { opt_logLevel :: Int }
15 deriving (Show, Eq)
17defaultOpts = IOption 0
19-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
20-- without typechecking).
21-- This will include all the functions and data declarations, plus fixity declarations
22-- and syntax macros.
24data IState = IState { tt_ctxt :: Context,
25 idris_infixes :: [FixDecl],
26 idris_implicits :: Ctxt [PArg],
27 idris_log :: String,
28 idris_options :: IOption,
29 idris_name :: Int
30 }
32idrisInit = IState emptyContext [] emptyContext "" defaultOpts 0
34-- The monad for the main REPL - reading and processing files and updating
35-- global state (hence the IO inner monad).
36type Idris a = StateT IState IO a
38getContext :: Idris Context
39getContext = do i <- get; return (tt_ctxt i)
41getIState :: Idris IState
42getIState = get
44getName :: Idris Int
45getName = do i <- get;
46 let idx = idris_name i;
47 put (i { idris_name = idx + 1 })
48 return idx
50setContext :: Context -> Idris ()
51setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
53updateContext :: (Context -> Context) -> Idris ()
54updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
56iputStrLn :: String -> Idris ()
57iputStrLn = lift.putStrLn
59setLogLevel :: Int -> Idris ()
60setLogLevel l = do i <- get
61 let opts = idris_options i
62 let opt' = opts { opt_logLevel = l }
63 put (i { idris_options = opt' } )
65logLevel :: Idris Int
66logLevel = do i <- get
67 return (opt_logLevel (idris_options i))
69logLvl :: Int -> String -> Idris ()
70logLvl l str = do i <- get
71 let lvl = opt_logLevel (idris_options i)
72 when (lvl >= l)
73 $ do lift (putStrLn str)
74 put (i { idris_log = idris_log i ++ str ++ "\n" } )
76iLOG :: String -> Idris ()
77iLOG = logLvl 1
79-- Commands in the REPL
81data Command = Quit | Help | Eval PTerm
82 | TTShell
83 | NOP
85-- Parsed declarations
87data Fixity = Infixl { prec :: Int }
88 | Infixr { prec :: Int }
89 | InfixN { prec :: Int }
90 | PrefixN { prec :: Int }
91 deriving Eq
93instance Show Fixity where
94 show (Infixl i) = "infixl " ++ show i
95 show (Infixr i) = "infixr " ++ show i
96 show (InfixN i) = "infix " ++ show i
97 show (PrefixN i) = "prefix " ++ show i
99data FixDecl = Fix Fixity String
100 deriving (Show, Eq)
102instance Ord FixDecl where
103 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
105data Plicity = Imp | Exp deriving Show
107data PDecl' t = PFix Fixity [String] -- fixity declaration
108 | PTy Name t -- type declaration
109 | PClauses Name [PClause' t] -- pattern clause
110 | PData (PData' t) -- data declaration
111 | PParams [(Name, PTerm)] [PDecl' t] -- params block
112 deriving Functor
114data PClause' t = PClause Name t t [PDecl]
115 deriving Functor
117data PData' t = PDatadecl { d_name :: Name,
118 d_tcon :: t,
119 d_cons :: [(Name, t)] }
120 deriving Functor
122-- Handy to get a free function for applying PTerm -> PTerm functions
123-- across a program, by deriving Functor
125type PDecl = PDecl' PTerm
126type PData = PData' PTerm
127type PClause = PClause' PTerm
129-- get all the names declared in a decl
131declared :: PDecl -> [Name]
132declared (PFix _ _) = []
133declared (PTy n t) = [n]
134declared (PClauses n _) = [] -- not a declaration
135declared (PData (PDatadecl n _ ts)) = n : map fst ts
136declared (PParams _ ds) = concatMap declared ds
138-- High level language terms
139--
140data PTerm = PQuote Raw
141 | PRef Name
142 | PLam Name PTerm PTerm
143 | PPi Plicity Name PTerm PTerm
144 | PLet Name PTerm PTerm PTerm -- not implemented yet
145 | PApp PTerm [PArg]
146 | PHidden PTerm -- irrelevant or hidden pattern
147 | PSet
148 | PConstant Const
149 | Placeholder
151data PArg' t = PImp { pname :: Name, getTm :: t }
152 | PExp { getTm :: t }
153 deriving (Show, Functor)
155type PArg = PArg' PTerm
157-- Syntactic sugar info (TODO: namespaces, parameters, modules)
159data SyntaxInfo = Syn { using :: [(Name, PTerm)],
160 syn_params :: [(Name, PTerm)] }
161 deriving Show
163defaultSyntax = Syn [] []
165--- Pretty printing declarations and terms
167instance Show PTerm where
168 show tm = showImp False tm
170instance Show PDecl where
171 show (PFix f ops) = show f ++ " " ++ showSep ", " ops
172 show (PTy n ty) = show n ++ " : " ++ show ty
173 show (PClauses n c) = showSep "\n" (map show c)
174 show (PData d) = show d
176instance Show PClause where
177 show c = showCImp False c
179instance Show PData where
180 show d = showDImp False d
182showCImp :: Bool -> PClause -> String
183showCImp impl (PClause n l r w) = showImp impl l ++ " = " ++ showImp impl r
184 ++ " where " ++ show w
185showDImp :: Bool -> PData -> String
186showDImp impl (PDatadecl n ty cons)
187 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
188 ++ showSep "\n\t| "
189 (map (\ (n, t) -> show n ++ " : " ++ showImp impl t) cons)
191getImps :: [PArg] -> [(Name, PTerm)]
192getImps [] = []
193getImps (PImp n tm : xs) = (n, tm) : getImps xs
194getImps (_ : xs) = getImps xs
196getExps :: [PArg] -> [PTerm]
197getExps [] = []
198getExps (PExp tm : xs) = tm : getExps xs
199getExps (_ : xs) = getExps xs
201getAll :: [PArg] -> [PTerm]
202getAll = map getTm
204showImp :: Bool -> PTerm -> String
205showImp impl tm = se 10 tm where
206 se p (PQuote r) = "![" ++ show r ++ "]"
207 se p (PRef n) = show n
208 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
209 se p (PPi Exp n ty sc)
210 | n `elem` allNamesIn sc = bracket p 2 $
211 "(" ++ show n ++ " : " ++ se 10 ty ++
212 ") -> " ++ se 10 sc
213 | otherwise = bracket p 2 $ se 0 ty ++ " -> " ++ se 10 sc
214 se p (PPi Imp n ty sc)
215 | impl = bracket p 2 $ "{" ++ show n ++ " : " ++ se 10 ty ++
216 "} -> " ++ se 10 sc
217 | otherwise = se 10 sc
218 se p (PApp (PRef f) [])
219 | not impl = show f
220 se p (PApp (PRef op@(UN [f:_])) args)
221 | length (getExps args) == 2 && not impl && not (isAlpha f)
222 = let [l, r] = getExps args in
223 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
224 se p (PApp f as)
225 = let (imps, args) = (getImps as, getExps as) in
226 bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")
227 ++ concatMap seArg args
228 se p (PHidden tm) = "." ++ se 0 tm
229 se p PSet = "Set"
230 se p (PConstant c) = show c
231 se p Placeholder = "_"
233 seArg arg = " " ++ se 0 arg
234 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
236 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
237 | otherwise = str
239allNamesIn :: PTerm -> [Name]
240allNamesIn tm = nub $ ni [] tm
241 where
242 ni env (PRef n)
243 | not (n `elem` env) = [n]
244 ni env (PApp f as) = ni env f ++ concatMap (ni env) (map getTm as)
245 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
246 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
247 ni env (PHidden tm) = ni env tm
248 ni env _ = []
250namesIn :: IState -> PTerm -> [Name]
251namesIn ist tm = nub $ ni [] tm
252 where
253 ni env (PRef n)
254 | not (n `elem` env)
255 = case lookupCtxt n (idris_implicits ist) of
256 Nothing -> [n]
257 _ -> []
258 ni env (PApp f as) = ni env f ++ concatMap (ni env) (map getTm as)
259 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
260 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
261 ni env (PHidden tm) = ni env tm
262 ni env _ = []
264-- For inferring types of things
266inferTy = MN 0 "__Infer"
267inferCon = MN 0 "__infer"
268inferDecl = PDatadecl inferTy
269 PSet
270 [(inferCon, PPi Imp (MN 0 "A") PSet (
271 PPi Exp (MN 0 "a") (PRef (MN 0 "A"))
272 (PRef inferTy)))]
274infTerm t = PApp (PRef inferCon) [PImp (MN 0 "A") Placeholder, PExp t]
275infP = P (TCon 0) inferTy (Set 0)
277getInferTerm, getInferType :: Term -> Term
278getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
279getInferTerm (App (App _ _) tm) = tm
280getInferTerm tm = error ("getInferTerm " ++ show tm)
282getInferType (Bind n b sc) = Bind n b $ getInferType sc
283getInferType (App (App _ ty) _) = ty
285piBind :: [(Name, PTerm)] -> PTerm -> PTerm
286piBind [] t = t
287piBind ((n, ty):ns) t = PPi Exp n ty (piBind ns t)
289-- Dealing with implicit arguments
291-- Add implicit Pi bindings for any names in the term which appear in an
292-- argument position.
294implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
295implicitise syn ist tm
296 = let uvars = using syn
297 pvars = syn_params syn
298 (declimps, ns') = execState (imps True [] tm) ([], [])
299 ns = ns' \\ map fst pvars in
300 if null ns
301 then (tm, reverse declimps)
302 else implicitise syn ist (pibind uvars ns tm)
303 where
304 imps top env (PApp f as)
305 = do (decls, ns) <- get
306 let isn = concatMap (namesIn ist) (map getTm as)
307 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
308 imps top env (PPi Imp n ty sc)
309 = do let isn = namesIn ist ty \\ [n]
310 (decls , ns) <- get
311 put (PImp n ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
312 imps True (n:env) sc
313 imps top env (PPi Exp n ty sc)
314 = do let isn = (namesIn ist ty ++ case sc of
315 (PRef x) -> namesIn ist sc
316 _ -> []) \\ [n]
317 (decls, ns) <- get -- ignore decls in HO types
318 put (PExp ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
319 imps True (n:env) sc
320 imps top env (PLam n ty sc)
321 = do imps False env ty
322 imps False (n:env) sc
323 imps top env (PHidden tm) = imps False env tm
324 imps top env _ = return ()
326 pibind using [] sc = sc
327 pibind using (n:ns) sc = case lookup n using of
328 Just ty -> PPi Imp n ty (pibind using ns sc)
329 Nothing -> PPi Imp n Placeholder (pibind using ns sc)
331-- Add implicit arguments in function calls
333addImpl :: IState -> PTerm -> PTerm
334addImpl ist ptm = ai [] ptm
335 where
336 ai env (PRef f) = aiFn env (PRef f) []
337 ai env (PApp (PRef f) as)
338 = let as' = map (fmap (ai env)) as in
339 aiFn env (PRef f) as'
340 ai env (PApp f as) = let f' = ai env f
341 as' = map (fmap (ai env)) as in
342 aiFn env f' as'
343 ai env (PLam n ty sc) = let ty' = ai env ty
344 sc' = ai (n:env) sc in
345 PLam n ty' sc'
346 ai env (PPi p n ty sc) = let ty' = ai env ty
347 sc' = ai (n:env) sc in
348 PPi p n ty' sc'
349 ai env (PHidden tm) = PHidden (ai env tm)
350 ai env tm = tm
352 aiFn env (PRef f) as | not (f `elem` env)
353 = case lookupCtxt f (idris_implicits ist) of
354 Just ns -> pApp (length ns) (PRef f) (insertImpl ns as)
355 Nothing -> pApp 1 (PRef f) as
356 aiFn env f as = pApp 1 f as
358 pApp a f [] = f
359 pApp a f as = let rest = drop a as in
360 appRest (PApp f (take a as)) rest
362 appRest f [] = f
363 appRest f (a : as) = appRest (PApp f [a]) as
365 insertImpl :: [PArg] -> [PArg] -> [PArg]
366 insertImpl (PExp ty : ps) (PExp tm : given) =
367 PExp tm : insertImpl ps given
368 insertImpl (PImp n ty : ps) given =
369 case find n given [] of
370 Just (tm, given') -> PImp n ty : insertImpl ps given'
371 Nothing -> PImp n Placeholder : insertImpl ps given
372 insertImpl expected [] = []
373 insertImpl [] given = given
375 find n [] acc = Nothing
376 find n (PImp n' t : gs) acc
377 | n == n' = Just (t, reverse acc ++ gs)
378 find n (g : gs) acc = find n gs (g : acc)