git.iko.soy/Idris-dev
on 1b6709f help sign in
Idris-dev/src/Idris/AbsSyntax.hs
238 lines 8.1 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
13data IOption = Logging
14 deriving (Show, Eq)
16-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
17-- without typechecking).
18-- This will include all the functions and data declarations, plus fixity declarations
19-- and syntax macros.
21data IState = IState { tt_ctxt :: Context,
22 idris_infixes :: [FixDecl],
23 idris_implicits :: Ctxt [Name],
24 idris_log :: String,
25 idris_options :: [IOption]
26 }
28idrisInit = IState emptyContext [] emptyContext "" []
30-- The monad for the main REPL - reading and processing files and updating
31-- global state (hence the IO inner monad).
32type Idris a = StateT IState IO a
34iputStrLn :: String -> Idris ()
35iputStrLn = lift.putStrLn
37setOpt :: IOption -> Bool -> Idris ()
38setOpt o True = do i <- get
39 put (i { idris_options = nub (o : idris_options i) })
40setOpt o False = do i <- get
41 put (i { idris_options = idris_options i \\ [o] })
43iLOG :: String -> Idris ()
44iLOG str = do i <- get
45 when (Logging `elem` idris_options i)
46 $ do lift (putStrLn str)
47 put (i { idris_log = idris_log i ++ str ++ "\n" } )
49-- Commands in the REPL
51data Command = Quit | Help | Eval PTerm
52 | TTShell
53 | NOP
55-- Parsed declarations
57data Fixity = Infixl { prec :: Int }
58 | Infixr { prec :: Int }
59 | InfixN { prec :: Int }
60 deriving Eq
62instance Show Fixity where
63 show (Infixl i) = "infixl " ++ show i
64 show (Infixr i) = "infixr " ++ show i
65 show (InfixN i) = "infix " ++ show i
67data FixDecl = Fix Fixity String
68 deriving (Show, Eq)
70instance Ord FixDecl where
71 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
73data Plicity = Imp | Exp deriving Show
75data PDecl' t = PFix Fixity [String] -- fixity declaration
76 | PTy Name t -- type declaration
77 | PClause t t -- pattern clause
78 | PData (PData' t) -- data declaration
79 deriving Functor
81data PData' t = PDatadecl { d_name :: Name,
82 d_tcon :: t,
83 d_cons :: [(Name, t)] }
84 deriving Functor
86-- Handy to get a free function for applying PTerm -> PTerm functions
87-- across a program, by deriving Functor
89type PDecl = PDecl' PTerm
90type PData = PData' PTerm
92-- High level language terms
94data PTerm = PQuote Raw
95 | PRef Name
96 | PLam Name PTerm PTerm
97 | PPi Plicity Name PTerm PTerm
98 | PApp PTerm [(Name, PTerm)] [PTerm]
99 | PHidden PTerm -- irrelevant or hidden pattern
100 | PSet
101 | Placeholder
103instance Show PTerm where
104 show tm = showImp False tm
106instance Show PDecl where
107 show (PFix f ops) = show f ++ " " ++ showSep ", " ops
108 show (PTy n ty) = show n ++ " : " ++ show ty
109 show (PClause l r) = show l ++ " = " ++ show r
110 show (PData d) = show d
112instance Show PData where
113 show d = showDImp False d
115showDImp :: Bool -> PData -> String
116showDImp impl (PDatadecl n ty cons)
117 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
118 ++ showSep "\n\t| "
119 (map (\ (n, t) -> show n ++ " : " ++ showImp impl t) cons)
121showImp :: Bool -> PTerm -> String
122showImp impl tm = se 10 tm where
123 se p (PQuote r) = "![" ++ show r ++ "]"
124 se p (PRef n) = show n
125 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
126 se p (PPi Exp n ty sc)
127 | n `elem` allNamesIn sc = bracket p 2 $
128 "(" ++ show n ++ " : " ++ se 10 ty ++
129 ") -> " ++ se 10 sc
130 | otherwise = bracket p 2 $ se 10 ty ++ " -> " ++ se 10 sc
131 se p (PPi Imp n ty sc)
132 | impl = bracket p 2 $ "{" ++ show n ++ " : " ++ se 10 ty ++
133 "} -> " ++ se 10 sc
134 | otherwise = se 10 sc
135 se p (PApp (PRef op@(UN [f:_])) _ [l, r])
136 | not impl && not (isAlpha f)
137 = bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 1 r
138 se p (PApp f imps args)
139 = bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")
140 ++ concatMap seArg args
141 se p (PHidden tm) = "." ++ se 0 tm
142 se p PSet = "Set"
143 se p Placeholder = "_"
145 seArg arg = " " ++ se 0 arg
146 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
148 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
149 | otherwise = str
151allNamesIn :: PTerm -> [Name]
152allNamesIn tm = nub $ ni [] tm
153 where
154 ni env (PRef n)
155 | not (n `elem` env) = [n]
156 ni env (PApp f is es) = ni env f ++ concatMap (ni env) (map snd is) ++
157 concatMap (ni env) es
158 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
159 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
160 ni env (PHidden tm) = ni env tm
161 ni env _ = []
163namesIn :: IState -> PTerm -> [Name]
164namesIn ist tm = nub $ ni [] tm
165 where
166 ni env (PRef n)
167 | not (n `elem` env)
168 = case lookupCtxt n (idris_implicits ist) of
169 Nothing -> [n]
170 _ -> []
171 ni env (PApp f is es) = ni env f ++ concatMap (ni env) (map snd is) ++
172 concatMap (ni env) es
173 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
174 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
175 ni env (PHidden tm) = ni env tm
176 ni env _ = []
178-- Dealing with implicit arguments
180-- Add implicit Pi bindings for any names in the term which appear in an
181-- argument position.
183implicitise :: IState -> PTerm -> (PTerm, [Name])
184implicitise ist tm
185 = let (declimps, ns) = execState (imps [] tm) ([], []) in
186 (pibind ns tm, ns ++ reverse declimps)
187 where
188 imps env (PApp f is es)
189 = do (decls, ns) <- get
190 let isn = concatMap (namesIn ist) (map snd is)
191 let esn = concatMap (namesIn ist) es
192 put (decls, nub (ns ++ ((isn ++ esn) \\ env)))
193 imps env (PPi Imp n ty sc)
194 = do imps env ty
195 (decls, ns) <- get
196 put (n:decls, ns)
197 imps (n:env) sc
198 imps env (PPi Exp n ty sc)
199 = do imps env ty
200 imps (n:env) sc
201 imps env (PLam n ty sc)
202 = do imps env ty
203 imps (n:env) sc
204 imps env (PHidden tm) = imps env tm
205 imps env _ = return ()
207 pibind [] sc = sc
208 pibind (n:ns) sc = PPi Imp n Placeholder (pibind ns sc)
210addImpl :: IState -> PTerm -> PTerm
211addImpl ist ptm = ai [] ptm
212 where
213 ai env (PApp f is es) = let f' = ai env f
214 is' = map (\ (n, tm) -> (n, ai env tm)) is
215 es' = map (ai env) es in
216 aiFn env f is' es'
217 ai env (PLam n ty sc) = let ty' = ai env ty
218 sc' = ai (n:env) sc in
219 PLam n ty' sc'
220 ai env (PPi p n ty sc) = let ty' = ai env ty
221 sc' = ai (n:env) sc in
222 PPi p n ty' sc'
223 ai env (PHidden tm) = PHidden (ai env tm)
224 ai env tm = tm
226 aiFn env (PRef f) is es | not (f `elem` env)
227 = case lookupCtxt f (idris_implicits ist) of
228 Just ns -> PApp (PRef f) (insertImpl ns is) es
229 Nothing -> PApp (PRef f) is es
230 aiFn env f is es = PApp f is es
232 insertImpl [] given = []
233 insertImpl (n:ns) given
234 = case lookup n given of
235 Just val -> (n, val) : insertImpl ns given
236 Nothing -> (n, Placeholder) : insertImpl ns given