git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/src/Idris/ElabDecls.hs
261 lines 10 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 PatternGuards #-}
4module Idris.ElabDecls where
6import Idris.AbsSyntax
7import Idris.ASTUtils
8import Idris.DSL
9import Idris.Error
10import Idris.Delaborate
11import Idris.Imports
12import Idris.ElabTerm
13import Idris.Coverage
14import Idris.DataOpts
15import Idris.Providers
16import Idris.Primitives
17import Idris.Inliner
18import Idris.PartialEval
19import Idris.DeepSeq
20import Idris.Output (iputStrLn, pshow, iWarn)
21import IRTS.Lang
23import Idris.Elab.Utils
24import Idris.Elab.Type
25import Idris.Elab.Clause
26import Idris.Elab.Data
27import Idris.Elab.Record
28import Idris.Elab.Class
29import Idris.Elab.Instance
30import Idris.Elab.Provider
31import Idris.Elab.Transform
32import Idris.Elab.Value
34import Idris.Core.TT
35import Idris.Core.Elaborate hiding (Tactic(..))
36import Idris.Core.Evaluate
37import Idris.Core.Execute
38import Idris.Core.Typecheck
39import Idris.Core.CaseTree
41import Idris.Docstrings hiding (Unchecked)
43import Prelude hiding (id, (.))
44import Control.Category
46import Control.Applicative hiding (Const)
47import Control.DeepSeq
48import Control.Monad
49import Control.Monad.State.Strict as State
50import Data.List
51import Data.Maybe
52import Debug.Trace
54import qualified Data.Map as Map
55import qualified Data.Set as S
56import qualified Data.Text as T
57import Data.Char(isLetter, toLower)
58import Data.List.Split (splitOn)
60import Util.Pretty(pretty, text)
63-- Top level elaborator info, supporting recursive elaboration
64recinfo :: ElabInfo
65recinfo = EInfo [] emptyContext id Nothing Nothing elabDecl'
67-- | Return the elaborated term which calls 'main'
68elabMain :: Idris Term
69elabMain = do (m, _) <- elabVal recinfo ERHS
70 (PApp fc (PRef fc (sUN "run__IO"))
71 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])
72 return m
73 where fc = fileFC "toplevel"
75-- | Elaborate primitives
76elabPrims :: Idris ()
77elabPrims = do mapM_ (elabDecl' EAll recinfo)
78 (map (\(opt, decl, docs, argdocs) -> PData docs argdocs defaultSyntax (fileFC "builtin") opt decl)
79 (zip4
80 [inferOpts, eqOpts]
81 [inferDecl, eqDecl]
82 [emptyDocstring, eqDoc]
83 [[], eqParamDoc]))
84 addNameHint eqTy (sUN "prf")
85 mapM_ elabPrim primitives
86 -- Special case prim__believe_me because it doesn't work on just constants
87 elabBelieveMe
88 -- Finally, syntactic equality
89 elabSynEq
90 where elabPrim :: Prim -> Idris ()
91 elabPrim (Prim n ty i def sc tot)
92 = do updateContext (addOperator n ty i (valuePrim def))
93 setTotality n tot
94 i <- getIState
95 putIState i { idris_scprims = (n, sc) : idris_scprims i }
97 valuePrim :: ([Const] -> Maybe Const) -> [Value] -> Maybe Value
98 valuePrim prim vals = fmap VConstant (mapM getConst vals >>= prim)
100 getConst (VConstant c) = Just c
101 getConst _ = Nothing
104 p_believeMe [_,_,x] = Just x
105 p_believeMe _ = Nothing
106 believeTy = Bind (sUN "a") (Pi Nothing (TType (UVar (-2))) (TType (UVar (-1))))
107 (Bind (sUN "b") (Pi Nothing (TType (UVar (-2))) (TType (UVar (-1))))
108 (Bind (sUN "x") (Pi Nothing (V 1) (TType (UVar (-1)))) (V 1)))
109 elabBelieveMe
110 = do let prim__believe_me = sUN "prim__believe_me"
111 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)
112 setTotality prim__believe_me (Partial NotCovering)
113 i <- getIState
114 putIState i {
115 idris_scprims = (prim__believe_me, (3, LNoOp)) : idris_scprims i
116 }
118 p_synEq [t,_,x,y]
119 | x == y = Just (VApp (VApp vnJust VErased)
120 (VApp (VApp vnRefl t) x))
121 | otherwise = Just (VApp vnNothing VErased)
122 p_synEq args = Nothing
124 nMaybe = P (TCon 0 2) (sNS (sUN "Maybe") ["Maybe", "Prelude"]) Erased
125 vnJust = VP (DCon 1 2 False) (sNS (sUN "Just") ["Maybe", "Prelude"]) VErased
126 vnNothing = VP (DCon 0 1 False) (sNS (sUN "Nothing") ["Maybe", "Prelude"]) VErased
127 vnRefl = VP (DCon 0 2 False) eqCon VErased
129 synEqTy = Bind (sUN "a") (Pi Nothing (TType (UVar (-3))) (TType (UVar (-2))))
130 (Bind (sUN "b") (Pi Nothing (TType (UVar (-3))) (TType (UVar (-2))))
131 (Bind (sUN "x") (Pi Nothing (V 1) (TType (UVar (-2))))
132 (Bind (sUN "y") (Pi Nothing (V 1) (TType (UVar (-2))))
133 (mkApp nMaybe [mkApp (P (TCon 0 4) eqTy Erased)
134 [V 3, V 2, V 1, V 0]]))))
135 elabSynEq
136 = do let synEq = sUN "prim__syntactic_eq"
138 updateContext (addOperator synEq synEqTy 4 p_synEq)
139 setTotality synEq (Total [])
140 i <- getIState
141 putIState i {
142 idris_scprims = (synEq, (4, LNoOp)) : idris_scprims i
143 }
146elabDecls :: ElabInfo -> [PDecl] -> Idris ()
147elabDecls info ds = do mapM_ (elabDecl EAll info) ds
149elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
150elabDecl what info d
151 = let info' = info { rec_elabDecl = elabDecl' } in
152 idrisCatch (withErrorReflection $ elabDecl' what info' d) (setAndReport)
154elabDecl' _ info (PFix _ _ _)
155 = return () -- nothing to elaborate
156elabDecl' _ info (PSyntax _ p)
157 = return () -- nothing to elaborate
158elabDecl' what info (PTy doc argdocs s f o n ty)
159 | what /= EDefns
160 = do iLOG $ "Elaborating type decl " ++ show n ++ show o
161 elabType info s doc argdocs f o n ty
162 return ()
163elabDecl' what info (PPostulate b doc s f o n ty)
164 | what /= EDefns
165 = do iLOG $ "Elaborating postulate " ++ show n ++ show o
166 if b
167 then elabExtern info s doc f o n ty
168 else elabPostulate info s doc f o n ty
169elabDecl' what info (PData doc argDocs s f co d)
170 | what /= ETypes
171 = do iLOG $ "Elaborating " ++ show (d_name d)
172 elabData info s doc argDocs f co d
173 | otherwise
174 = do iLOG $ "Elaborating [type of] " ++ show (d_name d)
175 elabData info s doc argDocs f co (PLaterdecl (d_name d) (d_tcon d))
176elabDecl' what info d@(PClauses f o n ps)
177 | what /= ETypes
178 = do iLOG $ "Elaborating clause " ++ show n
179 i <- getIState -- get the type options too
180 let o' = case lookupCtxt n (idris_flags i) of
181 [fs] -> fs
182 [] -> []
183 elabClauses info f (o ++ o') n ps
184elabDecl' what info (PMutual f ps)
185 = do case ps of
186 [p] -> elabDecl what info p
187 _ -> do mapM_ (elabDecl ETypes info) ps
188 mapM_ (elabDecl EDefns info) ps
189 -- record mutually defined data definitions
190 let datans = concatMap declared (filter isDataDecl ps)
191 mapM_ (setMutData datans) datans
192 iLOG $ "Rechecking for positivity " ++ show datans
193 mapM_ (\x -> do setTotality x Unchecked) datans
194 -- Do totality checking after entire mutual block
195 i <- get
196 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
197 updateContext (simplifyCasedef n $ getErasureInfo i))
198 (map snd (idris_totcheck i))
199 mapM_ buildSCG (idris_totcheck i)
200 mapM_ checkDeclTotality (idris_totcheck i)
201 clear_totcheck
202 where isDataDecl (PData _ _ _ _ _ _) = True
203 isDataDecl _ = False
205 setMutData ns n
206 = do i <- getIState
207 case lookupCtxt n (idris_datatypes i) of
208 [x] -> do let x' = x { mutual_types = ns }
209 putIState $ i { idris_datatypes
210 = addDef n x' (idris_datatypes i) }
211 _ -> return ()
213elabDecl' what info (PParams f ns ps)
214 = do i <- getIState
215 iLOG $ "Expanding params block with " ++ show ns ++ " decls " ++
216 show (concatMap tldeclared ps)
217 let nblock = pblock i
218 mapM_ (elabDecl' what info) nblock
219 where
220 pinfo = let ds = concatMap tldeclared ps
221 newps = params info ++ ns
222 dsParams = map (\n -> (n, map fst newps)) ds
223 newb = addAlist dsParams (inblock info) in
224 info { params = newps,
225 inblock = newb }
226 pblock i = map (expandParamsD False i id ns
227 (concatMap tldeclared ps)) ps
229elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps
230 where
231 ninfo = case namespace info of
232 Nothing -> info { namespace = Just [n] }
233 Just ns -> info { namespace = Just (n:ns) }
234elabDecl' what info (PClass doc s f cs n ps pdocs fds ds)
235 | what /= EDefns
236 = do iLOG $ "Elaborating class " ++ show n
237 elabClass info (s { syn_params = [] }) doc f cs n ps pdocs fds ds
238elabDecl' what info (PInstance doc argDocs s f cs n ps t expn ds)
239 = do iLOG $ "Elaborating instance " ++ show n
240 elabInstance info s doc argDocs what f cs n ps t expn ds
241elabDecl' what info (PRecord doc s f tyn ty opts cdoc cn cty)
242 | what /= ETypes
243 = do iLOG $ "Elaborating record " ++ show tyn
244 elabRecord info s doc f tyn ty opts cdoc cn cty
245 | otherwise
246 = do iLOG $ "Elaborating [type of] " ++ show tyn
247 elabData info s doc [] f [] (PLaterdecl tyn ty)
248elabDecl' _ info (PDSL n dsl)
249 = do i <- getIState
250 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })
251 addIBC (IBCDSL n)
252elabDecl' what info (PDirective i)
253 | what /= EDefns = i
254elabDecl' what info (PProvider doc syn fc provWhat n)
255 | what /= EDefns
256 = do iLOG $ "Elaborating type provider " ++ show n
257 elabProvider doc info syn fc provWhat n
258elabDecl' what info (PTransform fc safety old new)
259 = do elabTransform info fc safety old new
260 return ()
261elabDecl' _ _ _ = return () -- skipped this time