git.iko.soy/Idris-dev
on 3dfa841 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1618 lines 67 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances, PatternGuards #-}
4module Idris.AbsSyntax(module Idris.AbsSyntax, module Idris.AbsSyntaxTree) where
6import Idris.Core.TT
7import Idris.Core.Evaluate
8import Idris.Core.Elaborate hiding (Tactic(..))
9import Idris.Core.Typecheck
10import Idris.AbsSyntaxTree
11import Idris.Colours
12import Idris.IdeSlave
13import IRTS.CodegenCommon
14import Util.DynamicLinker
16import Paths_idris
18import System.Console.Haskeline
19import System.IO
21import Control.Monad.State
23import Data.List
24import Data.Char
25import Data.Either
26import Data.Maybe
27import Data.Word (Word)
29import Debug.Trace
31import Control.Monad.Error (throwError, catchError)
32import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
34import Util.Pretty
35import Util.System
37getContext :: Idris Context
38getContext = do i <- getIState; return (tt_ctxt i)
40forCodegen :: Codegen -> [(Codegen, a)] -> [a]
41forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']
43getObjectFiles :: Codegen -> Idris [FilePath]
44getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
46addObjectFile :: Codegen -> FilePath -> Idris ()
47addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
49getLibs :: Codegen -> Idris [String]
50getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
52addLib :: Codegen -> String -> Idris ()
53addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
55getFlags :: Codegen -> Idris [String]
56getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
58addFlag :: Codegen -> String -> Idris ()
59addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
61addDyLib :: [String] -> Idris (Either DynamicLib String)
62addDyLib libs = do i <- getIState
63 let ls = idris_dynamic_libs i
64 case mapMaybe (findDyLib ls) libs of
65 x:_ -> return (Left x)
66 [] -> do
67 handle <- lift . lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) $ libs
68 case msum handle of
69 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
70 concat (intersperse "," libs) ++ "\"")
71 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
72 return (Left x)
73 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
74 findDyLib [] l = Nothing
75 findDyLib (lib:libs) l | l == lib_name lib = Just lib
76 | otherwise = findDyLib libs l
79addHdr :: Codegen -> String -> Idris ()
80addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
82addLangExt :: LanguageExt -> Idris ()
83addLangExt TypeProviders = do i <- getIState
84 putIState $ i {
85 idris_language_extensions = TypeProviders : idris_language_extensions i
86 }
87addLangExt ErrorReflection = do i <- getIState
88 putIState $ i {
89 idris_language_extensions = ErrorReflection : idris_language_extensions i
90 }
92addTrans :: (Term, Term) -> Idris ()
93addTrans t = do i <- getIState
94 putIState $ i { idris_transforms = t : idris_transforms i }
96totcheck :: (FC, Name) -> Idris ()
97totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
99defer_totcheck :: (FC, Name) -> Idris ()
100defer_totcheck n
101 = do i <- getIState;
102 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
104clear_totcheck :: Idris ()
105clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
107setFlags :: Name -> [FnOpt] -> Idris ()
108setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
110setAccessibility :: Name -> Accessibility -> Idris ()
111setAccessibility n a
112 = do i <- getIState
113 let ctxt = setAccess n a (tt_ctxt i)
114 putIState $ i { tt_ctxt = ctxt }
116setTotality :: Name -> Totality -> Idris ()
117setTotality n a
118 = do i <- getIState
119 let ctxt = setTotal n a (tt_ctxt i)
120 putIState $ i { tt_ctxt = ctxt }
122getTotality :: Name -> Idris Totality
123getTotality n
124 = do i <- getIState
125 case lookupTotal n (tt_ctxt i) of
126 [t] -> return t
127 _ -> return (Total [])
129-- Get coercions which might return the required type
130getCoercionsTo :: IState -> Type -> [Name]
131getCoercionsTo i ty =
132 let cs = idris_coercions i
133 (fn,_) = unApply (getRetTy ty) in
134 findCoercions fn cs
135 where findCoercions t [] = []
136 findCoercions t (n : ns) =
137 let ps = case lookupTy n (tt_ctxt i) of
138 [ty'] -> case unApply (getRetTy ty') of
139 (t', _) ->
140 if t == t' then [n] else []
141 _ -> [] in
142 ps ++ findCoercions t ns
144addToCG :: Name -> CGInfo -> Idris ()
145addToCG n cg
146 = do i <- getIState
147 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
149-- Trace all the names in a call graph starting at the given name
150getAllNames :: Name -> Idris [Name]
151getAllNames n = allNames [] n
153allNames :: [Name] -> Name -> Idris [Name]
154allNames ns n | n `elem` ns = return []
155allNames ns n = do i <- getIState
156 case lookupCtxtExact n (idris_callgraph i) of
157 [ns'] -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
158 return (nub (n : concat more))
159 _ -> return [n]
161addCoercion :: Name -> Idris ()
162addCoercion n = do i <- getIState
163 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
165addDocStr :: Name -> String -> Idris ()
166addDocStr n doc
167 = do i <- getIState
168 putIState $ i { idris_docstrings = addDef n doc (idris_docstrings i) }
170addNameHint :: Name -> Name -> Idris ()
171addNameHint ty n
172 = do i <- getIState
173 ty' <- case lookupCtxtName ty (idris_implicits i) of
174 [(tyn, _)] -> return tyn
175 [] -> throwError (NoSuchVariable ty)
176 tyns -> throwError (CantResolveAlts (map show (map fst tyns)))
177 let ns' = case lookupCtxt ty' (idris_namehints i) of
178 [ns] -> ns ++ [n]
179 _ -> [n]
180 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
182getNameHints :: IState -> Name -> [Name]
183getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
184getNameHints i n =
185 case lookupCtxt n (idris_namehints i) of
186 [ns] -> ns
187 _ -> []
189addToCalledG :: Name -> [Name] -> Idris ()
190addToCalledG n ns = return () -- TODO
192-- Add a class instance function. Dodgy hack: Put integer instances first in the
193-- list so they are resolved by default.
194-- Dodgy hack 2: put constraint chasers (@@) last
196addInstance :: Bool -> Name -> Name -> Idris ()
197addInstance int n i
198 = do ist <- getIState
199 case lookupCtxt n (idris_classes ist) of
200 [CI a b c d e ins] ->
201 do let cs = addDef n (CI a b c d e (addI i ins)) (idris_classes ist)
202 putIState $ ist { idris_classes = cs }
203 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [i]) (idris_classes ist)
204 putIState $ ist { idris_classes = cs }
205 where addI i ins | int = i : ins
206 | chaser n = ins ++ [i]
207 | otherwise = insI i ins
208 insI i [] = [i]
209 insI i (n : ns) | chaser n = i : n : ns
210 | otherwise = n : insI i ns
212 chaser (UN nm)
213 | ('@':'@':_) <- str nm = True
214 chaser (NS n _) = chaser n
215 chaser _ = False
217addClass :: Name -> ClassInfo -> Idris ()
218addClass n i
219 = do ist <- getIState
220 let i' = case lookupCtxt n (idris_classes ist) of
221 [c] -> c { class_instances = class_instances i }
222 _ -> i
223 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
225addIBC :: IBCWrite -> Idris ()
226addIBC ibc@(IBCDef n)
227 = do i <- getIState
228 when (notDef (ibc_write i)) $
229 putIState $ i { ibc_write = ibc : ibc_write i }
230 where notDef [] = True
231 notDef (IBCDef n': is) | n == n' = False
232 notDef (_ : is) = notDef is
233addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
235clearIBC :: Idris ()
236clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
238resetNameIdx :: Idris ()
239resetNameIdx = do i <- getIState
240 put (i { idris_nameIdx = (0, emptyContext) })
242-- Used to preserve sharing of names
243addNameIdx :: Name -> Idris (Int, Name)
244addNameIdx n = do i <- getIState
245 let (i', x) = addNameIdx' i n
246 return x
248addNameIdx' :: IState -> Name -> (IState, (Int, Name))
249addNameIdx' i n
250 = let idxs = snd (idris_nameIdx i) in
251 case lookupCtxt n idxs of
252 [x] -> (i, x)
253 _ -> let i' = fst (idris_nameIdx i) + 1 in
254 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
256getHdrs :: Codegen -> Idris [String]
257getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
259setErrLine :: Int -> Idris ()
260setErrLine x = do i <- getIState;
261 case (errLine i) of
262 Nothing -> putIState $ i { errLine = Just x }
263 Just _ -> return ()
265clearErr :: Idris ()
266clearErr = do i <- getIState
267 putIState $ i { errLine = Nothing }
269getSO :: Idris (Maybe String)
270getSO = do i <- getIState
271 return (compiled_so i)
273setSO :: Maybe String -> Idris ()
274setSO s = do i <- getIState
275 putIState $ (i { compiled_so = s })
277getIState :: Idris IState
278getIState = get
280putIState :: IState -> Idris ()
281putIState = put
283-- | A version of liftIO that puts errors into the exception type of the Idris monad
284runIO :: IO a -> Idris a
285runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
286-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
288getName :: Idris Int
289getName = do i <- getIState;
290 let idx = idris_name i;
291 putIState $ (i { idris_name = idx + 1 })
292 return idx
294addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
295addInternalApp fp l t
296 = do i <- getIState
297 putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })
299getInternalApp :: FilePath -> Int -> Idris PTerm
300getInternalApp fp l = do i <- getIState
301 case lookup (fp, l) (idris_lineapps i) of
302 Just n' -> return n'
303 Nothing -> return Placeholder
304 -- TODO: What if it's not there?
306-- Pattern definitions are only used for coverage checking, so erase them
307-- when we're done
308clearOrigPats :: Idris ()
309clearOrigPats = do i <- get
310 let ps = idris_patdefs i
311 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
312 put (i { idris_patdefs = ps' })
314-- Erase types from Ps in the context (basically ending up with what's in
315-- the .ibc, which is all we need after all the analysis is done)
316clearPTypes :: Idris ()
317clearPTypes = do i <- get
318 let ctxt = tt_ctxt i
319 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
320 where pErase (CaseOp c t tys orig tot cds)
321 = CaseOp c t tys orig [] (pErase' cds)
322 pErase x = x
323 pErase' (CaseDefs _ (cs, c) _ rs)
324 = let c' = (cs, fmap pEraseType c) in
325 CaseDefs c' c' c' rs
327checkUndefined :: FC -> Name -> Idris ()
328checkUndefined fc n
329 = do i <- getContext
330 case lookupTy n i of
331 (_:_) -> fail $ show fc ++ ":" ++
332 show n ++ " already defined"
333 _ -> return ()
335isUndefined :: FC -> Name -> Idris Bool
336isUndefined fc n
337 = do i <- getContext
338 case lookupTy n i of
339 (_:_) -> return False
340 _ -> return True
342setContext :: Context -> Idris ()
343setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
345updateContext :: (Context -> Context) -> Idris ()
346updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
348addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
349addConstraints fc (v, cs)
350 = do i <- getIState
351 let ctxt = tt_ctxt i
352 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
353 next_tvar = v }
354 let ics = zip cs (repeat fc) ++ idris_constraints i
355 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
357addDeferred = addDeferred' Ref
358addDeferredTyCon = addDeferred' (TCon 0 0)
360addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
361addDeferred' nt ns
362 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns
363 i <- getIState
364 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
365 idris_metavars i }
366 where tidyNames used (Bind (MN i x) b sc)
367 = let n' = uniqueName (UN x) used in
368 Bind n' b $ tidyNames (n':used) sc
369 tidyNames used (Bind n b sc)
370 = let n' = uniqueName n used in
371 Bind n' b $ tidyNames (n':used) sc
372 tidyNames used b = b
374solveDeferred :: Name -> Idris ()
375solveDeferred n = do i <- getIState
376 putIState $ i { idris_metavars =
377 filter (\(n', _) -> n/=n')
378 (idris_metavars i) }
380getUndefined :: Idris [Name]
381getUndefined = do i <- getIState
382 return (map fst (idris_metavars i) \\ primDefs)
384ihPrintResult :: Handle -> String -> Idris ()
385ihPrintResult h s = do i <- getIState
386 case idris_outputmode i of
387 RawOutput -> case s of
388 "" -> return ()
389 s -> runIO $ hPutStrLn h s
390 IdeSlave n ->
391 let good = SexpList [SymbolAtom "ok", toSExp s] in
392 runIO $ hPutStrLn h $ convSExp "return" good n
394ihPrintError :: Handle -> String -> Idris ()
395ihPrintError h s = do i <- getIState
396 case idris_outputmode i of
397 RawOutput -> case s of
398 "" -> return ()
399 s -> runIO $ hPutStrLn h s
400 IdeSlave n ->
401 let good = SexpList [SymbolAtom "error", toSExp s] in
402 runIO . hPutStrLn h $ convSExp "return" good n
404ihputStrLn :: Handle -> String -> Idris ()
405ihputStrLn h s = do i <- getIState
406 case idris_outputmode i of
407 RawOutput -> runIO $ hPutStrLn h s
408 IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n
410iputStrLn = ihputStrLn stdout
411iPrintError = ihPrintError stdout
412iPrintResult = ihPrintResult stdout
413iWarn = ihWarn stdout
415ideslavePutSExp :: SExpable a => String -> a -> Idris ()
416ideslavePutSExp cmd info = do i <- getIState
417 case idris_outputmode i of
418 IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
419 _ -> return ()
421-- this needs some typing magic and more structured output towards emacs
422iputGoal :: String -> Idris ()
423iputGoal s = do i <- getIState
424 case idris_outputmode i of
425 RawOutput -> runIO $ putStrLn s
426 IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" s n
428isetPrompt :: String -> Idris ()
429isetPrompt p = do i <- getIState
430 case idris_outputmode i of
431 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n
433ihWarn :: Handle -> FC -> String -> Idris ()
434ihWarn h fc err = do i <- getIState
435 case idris_outputmode i of
436 RawOutput -> runIO $ hPutStrLn h (show fc ++ ":" ++ err)
437 IdeSlave n -> runIO $ hPutStrLn h $ convSExp "warning" (fc_fname fc, fc_line fc, fc_column fc, err) n
439setLogLevel :: Int -> Idris ()
440setLogLevel l = do i <- getIState
441 let opts = idris_options i
442 let opt' = opts { opt_logLevel = l }
443 putIState $ i { idris_options = opt' }
445setCmdLine :: [Opt] -> Idris ()
446setCmdLine opts = do i <- getIState
447 let iopts = idris_options i
448 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
450getCmdLine :: Idris [Opt]
451getCmdLine = do i <- getIState
452 return (opt_cmdline (idris_options i))
454getDumpDefun :: Idris (Maybe FilePath)
455getDumpDefun = do i <- getIState
456 return $ findC (opt_cmdline (idris_options i))
457 where findC [] = Nothing
458 findC (DumpDefun x : _) = Just x
459 findC (_ : xs) = findC xs
461getDumpCases :: Idris (Maybe FilePath)
462getDumpCases = do i <- getIState
463 return $ findC (opt_cmdline (idris_options i))
464 where findC [] = Nothing
465 findC (DumpCases x : _) = Just x
466 findC (_ : xs) = findC xs
468logLevel :: Idris Int
469logLevel = do i <- getIState
470 return (opt_logLevel (idris_options i))
472setErrContext :: Bool -> Idris ()
473setErrContext t = do i <- getIState
474 let opts = idris_options i
475 let opt' = opts { opt_errContext = t }
476 putIState $ i { idris_options = opt' }
478errContext :: Idris Bool
479errContext = do i <- getIState
480 return (opt_errContext (idris_options i))
482useREPL :: Idris Bool
483useREPL = do i <- getIState
484 return (opt_repl (idris_options i))
486setREPL :: Bool -> Idris ()
487setREPL t = do i <- getIState
488 let opts = idris_options i
489 let opt' = opts { opt_repl = t }
490 putIState $ i { idris_options = opt' }
492setNoBanner :: Bool -> Idris ()
493setNoBanner n = do i <- getIState
494 let opts = idris_options i
495 let opt' = opts {opt_nobanner = n}
496 putIState $ i { idris_options = opt' }
498getNoBanner :: Idris Bool
499getNoBanner = do i <- getIState
500 let opts = idris_options i
501 return (opt_nobanner opts)
503setQuiet :: Bool -> Idris ()
504setQuiet q = do i <- getIState
505 let opts = idris_options i
506 let opt' = opts { opt_quiet = q }
507 putIState $ i { idris_options = opt' }
509getQuiet :: Idris Bool
510getQuiet = do i <- getIState
511 let opts = idris_options i
512 return (opt_quiet opts)
514setCodegen :: Codegen -> Idris ()
515setCodegen t = do i <- getIState
516 let opts = idris_options i
517 let opt' = opts { opt_codegen = t }
518 putIState $ i { idris_options = opt' }
520codegen :: Idris Codegen
521codegen = do i <- getIState
522 return (opt_codegen (idris_options i))
524setOutputTy :: OutputType -> Idris ()
525setOutputTy t = do i <- getIState
526 let opts = idris_options i
527 let opt' = opts { opt_outputTy = t }
528 putIState $ i { idris_options = opt' }
530outputTy :: Idris OutputType
531outputTy = do i <- getIState
532 return $ opt_outputTy $ idris_options i
534setIdeSlave :: Bool -> Idris ()
535setIdeSlave True = do i <- getIState
536 putIState $ i { idris_outputmode = (IdeSlave 0), idris_colourRepl = False }
537setIdeSlave False = return ()
539setTargetTriple :: String -> Idris ()
540setTargetTriple t = do i <- getIState
541 let opts = idris_options i
542 opt' = opts { opt_triple = t }
543 putIState $ i { idris_options = opt' }
545targetTriple :: Idris String
546targetTriple = do i <- getIState
547 return (opt_triple (idris_options i))
549setTargetCPU :: String -> Idris ()
550setTargetCPU t = do i <- getIState
551 let opts = idris_options i
552 opt' = opts { opt_cpu = t }
553 putIState $ i { idris_options = opt' }
555targetCPU :: Idris String
556targetCPU = do i <- getIState
557 return (opt_cpu (idris_options i))
559setOptLevel :: Word -> Idris ()
560setOptLevel t = do i <- getIState
561 let opts = idris_options i
562 opt' = opts { opt_optLevel = t }
563 putIState $ i { idris_options = opt' }
565optLevel :: Idris Word
566optLevel = do i <- getIState
567 return (opt_optLevel (idris_options i))
569verbose :: Idris Bool
570verbose = do i <- getIState
571 return (opt_verbose (idris_options i))
573setVerbose :: Bool -> Idris ()
574setVerbose t = do i <- getIState
575 let opts = idris_options i
576 let opt' = opts { opt_verbose = t }
577 putIState $ i { idris_options = opt' }
579typeInType :: Idris Bool
580typeInType = do i <- getIState
581 return (opt_typeintype (idris_options i))
583setTypeInType :: Bool -> Idris ()
584setTypeInType t = do i <- getIState
585 let opts = idris_options i
586 let opt' = opts { opt_typeintype = t }
587 putIState $ i { idris_options = opt' }
589coverage :: Idris Bool
590coverage = do i <- getIState
591 return (opt_coverage (idris_options i))
593setCoverage :: Bool -> Idris ()
594setCoverage t = do i <- getIState
595 let opts = idris_options i
596 let opt' = opts { opt_coverage = t }
597 putIState $ i { idris_options = opt' }
599setIBCSubDir :: FilePath -> Idris ()
600setIBCSubDir fp = do i <- getIState
601 let opts = idris_options i
602 let opt' = opts { opt_ibcsubdir = fp }
603 putIState $ i { idris_options = opt' }
605valIBCSubDir :: IState -> Idris FilePath
606valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
608addImportDir :: FilePath -> Idris ()
609addImportDir fp = do i <- getIState
610 let opts = idris_options i
611 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
612 putIState $ i { idris_options = opt' }
614setImportDirs :: [FilePath] -> Idris ()
615setImportDirs fps = do i <- getIState
616 let opts = idris_options i
617 let opt' = opts { opt_importdirs = fps }
618 putIState $ i { idris_options = opt' }
620allImportDirs :: Idris [FilePath]
621allImportDirs = do i <- getIState
622 let optdirs = opt_importdirs (idris_options i)
623 return ("." : reverse optdirs)
625colourise :: Idris Bool
626colourise = do i <- getIState
627 return $ idris_colourRepl i
629setColourise :: Bool -> Idris ()
630setColourise b = do i <- getIState
631 putIState $ i { idris_colourRepl = b }
633setOutH :: Handle -> Idris ()
634setOutH h = do i <- getIState
635 putIState $ i { idris_outh = h }
637impShow :: Idris Bool
638impShow = do i <- getIState
639 return (opt_showimp (idris_options i))
641setImpShow :: Bool -> Idris ()
642setImpShow t = do i <- getIState
643 let opts = idris_options i
644 let opt' = opts { opt_showimp = t }
645 putIState $ i { idris_options = opt' }
647setColour :: ColourType -> IdrisColour -> Idris ()
648setColour ct c = do i <- getIState
649 let newTheme = setColour' ct c (idris_colourTheme i)
650 putIState $ i { idris_colourTheme = newTheme }
651 where setColour' KeywordColour c t = t { keywordColour = c }
652 setColour' BoundVarColour c t = t { boundVarColour = c }
653 setColour' ImplicitColour c t = t { implicitColour = c }
654 setColour' FunctionColour c t = t { functionColour = c }
655 setColour' TypeColour c t = t { typeColour = c }
656 setColour' DataColour c t = t { dataColour = c }
657 setColour' PromptColour c t = t { promptColour = c }
659logLvl :: Int -> String -> Idris ()
660logLvl l str = do i <- getIState
661 let lvl = opt_logLevel (idris_options i)
662 when (lvl >= l) $
663 case idris_outputmode i of
664 RawOutput -> do runIO $ putStrLn str
665 IdeSlave n ->
666 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
667 runIO $ putStrLn $ convSExp "log" good n
669cmdOptType :: Opt -> Idris Bool
670cmdOptType x = do i <- getIState
671 return $ x `elem` opt_cmdline (idris_options i)
673iLOG :: String -> Idris ()
674iLOG = logLvl 1
676noErrors :: Idris Bool
677noErrors = do i <- getIState
678 case errLine i of
679 Nothing -> return True
680 _ -> return False
682setTypeCase :: Bool -> Idris ()
683setTypeCase t = do i <- getIState
684 let opts = idris_options i
685 let opt' = opts { opt_typecase = t }
686 putIState $ i { idris_options = opt' }
689-- For inferring types of things
691bi = fileFC "builtin"
693inferTy = sMN 0 "__Infer"
694inferCon = sMN 0 "__infer"
695inferDecl = PDatadecl inferTy
696 PType
697 [("", inferCon, PPi impl (sMN 0 "iType") PType (
698 PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
699 (PRef bi inferTy)), bi)]
700inferOpts = []
702infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
703infP = P (TCon 6 0) inferTy (TType (UVal 0))
705getInferTerm, getInferType :: Term -> Term
706getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
707getInferTerm (App (App _ _) tm) = tm
708getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
710getInferType (Bind n b sc) = Bind n b $ getInferType sc
711getInferType (App (App _ ty) _) = ty
713-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class
715primNames = [unitTy, unitCon,
716 falseTy, pairTy, pairCon,
717 eqTy, eqCon, inferTy, inferCon]
719unitTy = sMN 0 "__Unit"
720unitCon = sMN 0 "__II"
721unitDecl = PDatadecl unitTy PType
722 [("", unitCon, PRef bi unitTy, bi)]
723unitOpts = [DefaultEliminator]
725falseTy = sMN 0 "__False"
726falseDecl = PDatadecl falseTy PType []
727falseOpts = []
729pairTy = sMN 0 "__Pair"
730pairCon = sMN 0 "__MkPair"
731pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
732 [("", pairCon, PPi impl (n "A") PType (
733 PPi impl (n "B") PType (
734 PPi expl (n "a") (PRef bi (n "A")) (
735 PPi expl (n "b") (PRef bi (n "B"))
736 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
737 pexp (PRef bi (n "B"))])))), bi)]
738 where n a = sMN 0 a
739pairOpts = []
741eqTy = sUN "="
742eqCon = sUN "refl"
743eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),
744 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
745 PType)
746 [("", eqCon, PPi impl (n "A") PType (
747 PPi impl (n "x") (PRef bi (n "A"))
748 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
749 pimp (n "B") Placeholder False,
750 pexp (PRef bi (n "x")),
751 pexp (PRef bi (n "x"))])), bi)]
752 where n a = sMN 0 a
753eqOpts = []
755elimName = sUN "__Elim"
756elimMethElimTy = sUN "__elimTy"
757elimMethElim = sUN "elim"
758elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]
759 [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,
760 PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
762-- Defined in builtins.idr
763sigmaTy = sUN "Exists"
764existsCon = sUN "Ex_intro"
766piBind :: [(Name, PTerm)] -> PTerm -> PTerm
767piBind = piBindp expl
769piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
770piBindp p [] t = t
771piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
773-- Dealing with parameters
775expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
776 [Name] -> -- all names
777 [Name] -> -- names with no declaration
778 PTerm -> PTerm
779expandParams dec ps ns infs tm = en tm
780 where
781 -- if we shadow a name (say in a lambda binding) that is used in a call to
782 -- a lifted function, we need access to both names - once in the scope of the
783 -- binding and once to call the lifted functions. So we'll explicitly shadow
784 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
785 -- but we didn't...)
787 mkShadow (UN n) = MN 0 n
788 mkShadow (MN i n) = MN (i+1) n
789 mkShadow (NS x s) = NS (mkShadow x) s
791 en (PLam n t s)
792 | n `elem` (map fst ps ++ ns)
793 = let n' = mkShadow n in
794 PLam n' (en t) (en (shadow n n' s))
795 | otherwise = PLam n (en t) (en s)
796 en (PPi p n t s)
797 | n `elem` (map fst ps ++ ns)
798 = let n' = mkShadow n in
799 PPi p n' (en t) (en (shadow n n' s))
800 | otherwise = PPi p n (en t) (en s)
801 en (PLet n ty v s)
802 | n `elem` (map fst ps ++ ns)
803 = let n' = mkShadow n in
804 PLet n' (en ty) (en v) (en (shadow n n' s))
805 | otherwise = PLet n (en ty) (en v) (en s)
806 -- FIXME: Should only do this in a type signature!
807 en (PDPair f (PRef f' n) t r)
808 | n `elem` (map fst ps ++ ns) && t /= Placeholder
809 = let n' = mkShadow n in
810 PDPair f (PRef f' n') (en t) (en (shadow n n' r))
811 en (PEq f l r) = PEq f (en l) (en r)
812 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
813 en (PTyped l r) = PTyped (en l) (en r)
814 en (PPair f l r) = PPair f (en l) (en r)
815 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
816 en (PAlternative a as) = PAlternative a (map en as)
817 en (PHidden t) = PHidden (en t)
818 en (PUnifyLog t) = PUnifyLog (en t)
819 en (PNoImplicits t) = PNoImplicits (en t)
820 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
821 en (PProof ts) = PProof (map (fmap en) ts)
822 en (PTactics ts) = PTactics (map (fmap en) ts)
824 en (PQuote (Var n))
825 | n `nselem` ns = PQuote (Var (dec n))
826 en (PApp fc (PInferRef fc' n) as)
827 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
828 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
829 en (PApp fc (PRef fc' n) as)
830 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
831 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
832 | n `nselem` ns = PApp fc (PRef fc' (dec n))
833 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
834 en (PAppBind fc (PRef fc' n) as)
835 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
836 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
837 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
838 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
839 en (PRef fc n)
840 | n `elem` infs = PApp fc (PInferRef fc (dec n))
841 (map (pexp . (PRef fc)) (map fst ps))
842 | n `nselem` ns = PApp fc (PRef fc (dec n))
843 (map (pexp . (PRef fc)) (map fst ps))
844 en (PInferRef fc n)
845 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
846 (map (pexp . (PRef fc)) (map fst ps))
847 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
848 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
849 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
850 en t = t
852 nselem x [] = False
853 nselem x (y : xs) | nseq x y = True
854 | otherwise = nselem x xs
856 nseq x y = nsroot x == nsroot y
858expandParamsD :: Bool -> -- True = RHS only
859 IState ->
860 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
861expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)
862 = if n `elem` ns && (not rhsonly)
863 then -- trace (show (n, expandParams dec ps ns ty)) $
864 PTy doc syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
865 else --trace (show (n, expandParams dec ps ns ty)) $
866 PTy doc syn fc o n (expandParams dec ps ns [] ty)
867expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
868 = if n `elem` ns && (not rhsonly)
869 then -- trace (show (n, expandParams dec ps ns ty)) $
870 PPostulate doc syn fc o (dec n) (piBind ps
871 (expandParams dec ps ns [] ty))
872 else --trace (show (n, expandParams dec ps ns ty)) $
873 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
874expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
875 = let n' = if n `elem` ns then dec n else n in
876 PClauses fc opts n' (map expandParamsC cs)
877 where
878 expandParamsC (PClause fc n lhs ws rhs ds)
879 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
880 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
881 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
882 n' = if n `elem` ns then dec n else n
883 -- names bound on the lhs should not be expanded on the rhs
884 ns' = removeBound lhs ns in
885 PClause fc n' lhs'
886 (map (expandParams dec ps'' ns' []) ws)
887 (expandParams dec ps'' ns' [] rhs)
888 (map (expandParamsD True ist dec ps'' ns') ds)
889 expandParamsC (PWith fc n lhs ws wval ds)
890 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
891 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
892 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
893 n' = if n `elem` ns then dec n else n
894 ns' = removeBound lhs ns in
895 PWith fc n' lhs'
896 (map (expandParams dec ps'' ns' []) ws)
897 (expandParams dec ps'' ns' [] wval)
898 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
899 updateps yn nm [] = []
900 updateps yn nm (((a, t), i):as)
901 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
902 | otherwise = (sMN i (show n ++ "_u"), t) : updateps yn nm as
904 removeBound lhs ns = ns \\ nub (bnames lhs)
906 bnames (PRef _ n) = [n]
907 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
908 bnames (PPair _ l r) = bnames l ++ bnames r
909 bnames (PDPair _ l Placeholder r) = bnames l ++ bnames r
910 bnames _ = []
912expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
913 = PData doc syn fc co (expandPData pd)
914 where
915 -- just do the type decl, leave constructors alone (parameters will be
916 -- added implicitly)
917 expandPData (PDatadecl n ty cons)
918 = if n `elem` ns
919 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
920 (map econ cons)
921 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
922 econ (doc, n, t, fc)
923 = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc)
924expandParamsD rhs ist dec ps ns (PParams f params pds)
925 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
926 (map (expandParamsD True ist dec ps ns) pds)
927-- (map (expandParamsD ist dec ps ns) pds)
928expandParamsD rhs ist dec ps ns (PMutual f pds)
929 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
930expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
931 = PClass doc info f
932 (map (expandParams dec ps ns []) cs)
933 n
934 (map (mapsnd (expandParams dec ps ns [])) params)
935 (map (expandParamsD rhs ist dec ps ns) decls)
936expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
937 = PInstance info f
938 (map (expandParams dec ps ns []) cs)
939 n
940 (map (expandParams dec ps ns []) params)
941 (expandParams dec ps ns [] ty)
942 cn
943 (map (expandParamsD rhs ist dec ps ns) decls)
944expandParamsD rhs ist dec ps ns d = d
946mapsnd f (x, t) = (x, f t)
948-- Calculate a priority for a type, for deciding elaboration order
949-- * if it's just a type variable or concrete type, do it early (0)
950-- * if there's only type variables and injective constructors, do it next (1)
951-- * if there's a function type, next (2)
952-- * finally, everything else (3)
954getPriority :: IState -> PTerm -> Int
955getPriority i tm = 1 -- pri tm
956 where
957 pri (PRef _ n) =
958 case lookupP n (tt_ctxt i) of
959 ((P (DCon _ _) _ _):_) -> 1
960 ((P (TCon _ _) _ _):_) -> 1
961 ((P Ref _ _):_) -> 1
962 [] -> 0 -- must be locally bound, if it's not an error...
963 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
964 pri (PTrue _) = 0
965 pri (PFalse _) = 0
966 pri (PRefl _ _) = 1
967 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
968 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
969 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
970 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
971 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
972 pri (PTyped l r) = pri l
973 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
974 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
975 pri (PAlternative a as) = maximum (map pri as)
976 pri (PConstant _) = 0
977 pri Placeholder = 1
978 pri _ = 3
980addStatics :: Name -> Term -> PTerm -> Idris ()
981addStatics n tm ptm =
982 do let (statics, dynamics) = initStatics tm ptm
983 let stnames = nub $ concatMap freeArgNames (map snd statics)
984 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
985 -- also get the arguments which are 'uniquely inferrable' from
986 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
987 let statics' = nub $ map fst statics ++
988 filter (\x -> not (elem x dnames)) stnames
989 let stpos = staticList statics' tm
990 i <- getIState
991 when (not (null statics)) $
992 logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics
993 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
994 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
995 addIBC (IBCStatic n)
996 where
997 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
998 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
999 if pstatic p == Static then ((n, ty) : static, dynamic)
1000 else if (not (searchArg p))
1001 then (static, (n, ty) : dynamic)
1002 else (static, dynamic)
1003 initStatics t pt = ([], [])
1005 freeArgNames (Bind n (Pi ty) sc)
1006 = nub $ freeArgNames ty
1007 freeArgNames tm = let (_, args) = unApply tm in
1008 concatMap freeNames args
1010 -- if a name appears in a type class or tactic implicit index, it doesn't
1011 -- affect its 'uniquely inferrable' from a static status since these are
1012 -- resolved by searching.
1013 searchArg (Constraint _ _ _) = True
1014 searchArg (TacImp _ _ _ _) = True
1015 searchArg _ = False
1017 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
1018 staticList _ _ = []
1020-- Dealing with implicit arguments
1022-- Add constraint bindings from using block
1024addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1025addUsingConstraints syn fc t
1026 = do ist <- get
1027 let ns = namesIn [] ist t
1028 let cs = getConstraints t -- check declared constraints
1029 let addconsts = uconsts \\ cs
1030 -- if all names in the arguments of addconsts appear in ns,
1031 -- add the constraint implicitly
1032 return (doAdd addconsts ns t)
1033 where uconsts = filter uconst (using syn)
1034 uconst (UConstraint _ _) = True
1035 uconst _ = False
1037 doAdd [] _ t = t
1038 -- if all of args in ns, then add it
1039 doAdd (UConstraint c args : cs) ns t
1040 | all (\n -> elem n ns) args
1041 = PPi (Constraint False Dynamic "") (sMN 0 "cu")
1042 (mkConst c args) (doAdd cs ns t)
1043 | otherwise = doAdd cs ns t
1045 mkConst c args = PApp fc (PRef fc c)
1046 (map (\n -> PExp 0 False (PRef fc n) "") args)
1048 getConstraints (PPi (Constraint _ _ _) _ c sc)
1049 = getcapp c ++ getConstraints sc
1050 getConstraints (PPi _ _ c sc) = getConstraints sc
1051 getConstraints _ = []
1053 getcapp (PApp _ (PRef _ c) args)
1054 = do ns <- mapM getName args
1055 return (UConstraint c ns)
1056 getcapp _ = []
1058 getName (PExp _ _ (PRef _ n) _) = return n
1059 getName _ = []
1061-- Add implicit Pi bindings for any names in the term which appear in an
1062-- argument position.
1064-- This has become a right mess already. Better redo it some time...
1066implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
1067implicit syn n ptm = implicit' syn [] n ptm
1069implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1070implicit' syn ignore n ptm
1071 = do i <- getIState
1072 let (tm', impdata) = implicitise syn ignore i ptm
1073-- let (tm'', spos) = findStatics i tm'
1074 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1075 addIBC (IBCImp n)
1076 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1077-- i <- get
1078-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1079 return tm'
1081implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1082implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1083 let (declimps, ns') = execState (imps True [] tm) ([], [])
1084 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1085 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1086 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1087 if null ns
1088 then (tm, reverse declimps)
1089 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1090 where
1091 uvars = map ipair (filter uimplicit (using syn))
1092 pvars = syn_params syn
1094 inUsing n = n `elem` map fst uvars
1096 ipair (UImplicit x y) = (x, y)
1097 uimplicit (UImplicit _ _) = True
1098 uimplicit _ = False
1100 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1101 | otherwise = x : dropAll xs ys
1102 dropAll [] ys = []
1104 imps top env (PApp _ f as)
1105 = do (decls, ns) <- get
1106 let isn = concatMap (namesIn uvars ist) (map getTm as)
1107 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1108 imps top env (PPi (Imp l _ doc _) n ty sc)
1109 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1110 (decls , ns) <- get
1111 put (PImp (getPriority ist ty) True l n Placeholder doc : decls,
1112 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1113 imps True (n:env) sc
1114 imps top env (PPi (Exp l _ doc _) n ty sc)
1115 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1116 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1117 _ -> [])
1118 (decls, ns) <- get -- ignore decls in HO types
1119 put (PExp (getPriority ist ty) l Placeholder doc : decls,
1120 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1121 imps True (n:env) sc
1122 imps top env (PPi (Constraint l _ doc) n ty sc)
1123 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1124 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1125 _ -> [])
1126 (decls, ns) <- get -- ignore decls in HO types
1127 put (PConstraint 10 l Placeholder doc : decls,
1128 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1129 imps True (n:env) sc
1130 imps top env (PPi (TacImp l _ scr doc) n ty sc)
1131 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1132 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1133 _ -> [])
1134 (decls, ns) <- get -- ignore decls in HO types
1135 put (PTacImplicit 10 l n scr Placeholder doc : decls,
1136 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1137 imps True (n:env) sc
1138 imps top env (PEq _ l r)
1139 = do (decls, ns) <- get
1140 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1141 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1142 imps top env (PRewrite _ l r _)
1143 = do (decls, ns) <- get
1144 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1145 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1146 imps top env (PTyped l r)
1147 = imps top env l
1148 imps top env (PPair _ l r)
1149 = do (decls, ns) <- get
1150 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1151 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1152 imps top env (PDPair _ (PRef _ n) t r)
1153 = do (decls, ns) <- get
1154 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1155 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1156 imps top env (PDPair _ l t r)
1157 = do (decls, ns) <- get
1158 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1159 namesIn uvars ist r
1160 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1161 imps top env (PAlternative a as)
1162 = do (decls, ns) <- get
1163 let isn = concatMap (namesIn uvars ist) as
1164 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1165 imps top env (PLam n ty sc)
1166 = do imps False env ty
1167 imps False (n:env) sc
1168 imps top env (PHidden tm) = imps False env tm
1169 imps top env (PUnifyLog tm) = imps False env tm
1170 imps top env (PNoImplicits tm) = imps False env tm
1171 imps top env _ = return ()
1173 pibind using [] sc = sc
1174 pibind using (n:ns) sc
1175 = case lookup n using of
1176 Just ty -> PPi (Imp False Dynamic "" False) n ty (pibind using ns sc)
1177 Nothing -> PPi (Imp False Dynamic "" False) n Placeholder
1178 (pibind using ns sc)
1180-- Add implicit arguments in function calls
1181addImplPat :: IState -> PTerm -> PTerm
1182addImplPat = addImpl' True [] []
1184addImplBound :: IState -> [Name] -> PTerm -> PTerm
1185addImplBound ist ns = addImpl' False ns [] ist
1187addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1188addImplBoundInf ist ns inf = addImpl' False ns inf ist
1190addImpl :: IState -> PTerm -> PTerm
1191addImpl = addImpl' False [] []
1193-- TODO: in patterns, don't add implicits to function names guarded by constructors
1194-- and *not* inside a PHidden
1196addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1197addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm
1198 where
1199 ai env (PRef fc f)
1200 | f `elem` infns = PInferRef fc f
1201 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f []
1202 ai env (PHidden (PRef fc f))
1203 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f []
1204 ai env (PEq fc l r) = let l' = ai env l
1205 r' = ai env r in
1206 PEq fc l' r'
1207 ai env (PRewrite fc l r g) = let l' = ai env l
1208 r' = ai env r
1209 g' = fmap (ai env) g in
1210 PRewrite fc l' r' g'
1211 ai env (PTyped l r) = let l' = ai env l
1212 r' = ai env r in
1213 PTyped l' r'
1214 ai env (PPair fc l r) = let l' = ai env l
1215 r' = ai env r in
1216 PPair fc l' r'
1217 ai env (PDPair fc l t r) = let l' = ai env l
1218 t' = ai env t
1219 r' = ai env r in
1220 PDPair fc l' t' r'
1221 ai env (PAlternative a as) = let as' = map (ai env) as in
1222 PAlternative a as'
1223 ai env (PApp fc (PInferRef _ f) as)
1224 = let as' = map (fmap (ai env)) as in
1225 PApp fc (PInferRef fc f) as'
1226 ai env (PApp fc ftm@(PRef _ f) as)
1227 | f `elem` infns = ai env (PApp fc (PInferRef fc f) as)
1228 | not (f `elem` map fst env)
1229 = let as' = map (fmap (ai env)) as in
1230 handleErr $ aiFn inpat False ist fc f as'
1231 | Just (Just ty) <- lookup f env
1232 = let as' = map (fmap (ai env)) as
1233 arity = getPArity ty in
1234 mkPApp fc arity ftm as'
1235 ai env (PApp fc f as) = let f' = ai env f
1236 as' = map (fmap (ai env)) as in
1237 mkPApp fc 1 f' as'
1238 ai env (PCase fc c os) = let c' = ai env c
1239 os' = map (pmap (ai env)) os in
1240 PCase fc c' os'
1241 ai env (PLam n ty sc) = let ty' = ai env ty
1242 sc' = ai ((n, Just ty):env) sc in
1243 PLam n ty' sc'
1244 ai env (PLet n ty val sc)
1245 = let ty' = ai env ty
1246 val' = ai env val
1247 sc' = ai ((n, Just ty):env) sc in
1248 PLet n ty' val' sc'
1249 ai env (PPi p n ty sc) = let ty' = ai env ty
1250 sc' = ai ((n, Just ty):env) sc in
1251 PPi p n ty' sc'
1252 ai env (PGoal fc r n sc) = let r' = ai env r
1253 sc' = ai ((n, Nothing):env) sc in
1254 PGoal fc r' n sc'
1255 ai env (PHidden tm) = PHidden (ai env tm)
1256 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
1257 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
1258 ai env (PRefl fc tm) = PRefl fc (ai env tm)
1259 ai env (PUnifyLog tm) = PUnifyLog (ai env tm)
1260 ai env (PNoImplicits tm) = PNoImplicits (ai env tm)
1261 ai env tm = tm
1263 handleErr (Left err) = PElabError err
1264 handleErr (Right x) = x
1266-- if in a pattern, and there are no arguments, and there's no possible
1267-- names with zero explicit arguments, don't add implicits.
1269aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
1270aiFn inpat True ist fc f []
1271 = case lookupDef f (tt_ctxt ist) of
1272 [] -> Right $ PPatvar fc f
1273 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1274 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1275 if (not (vname f) || tcname f
1276 || any (conCaf (tt_ctxt ist)) ialts)
1277-- any constructor alts || any allImp ialts))
1278 then aiFn inpat False ist fc f [] -- use it as a constructor
1279 else Right $ PPatvar fc f
1280 where imp (PExp _ _ _ _) = False
1281 imp _ = True
1282-- allImp [] = False
1283 allImp xs = all imp xs
1284 constructor (TyDecl (DCon _ _) _) = True
1285 constructor _ = False
1287 conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
1289 vname (UN n) = True -- non qualified
1290 vname _ = False
1292aiFn inpat expat ist fc f as
1293 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1294aiFn inpat expat ist fc f as
1295 -- This is where namespaces get resolved by adding PAlternative
1296 = do let ns = lookupCtxtName f (idris_implicits ist)
1297 let ns' = filter (\(n, _) -> notHidden n) ns
1298 case ns' of
1299 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1300 [] -> if f `elem` (map fst (idris_metavars ist))
1301 then Right $ PApp fc (PRef fc f) as
1302 else Right $ mkPApp fc (length as) (PRef fc f) as
1303 alts -> Right $
1304 PAlternative True $
1305 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1306 (insertImpl ns as)) alts
1307 where
1308 notHidden n = case getAccessibility n of
1309 Hidden -> False
1310 _ -> True
1312 getAccessibility n
1313 = case lookupDefAcc n False (tt_ctxt ist) of
1314 [(n,t)] -> t
1315 _ -> Public
1318 insertImpl :: [PArg] -> [PArg] -> [PArg]
1319 insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =
1320 PExp p l tm d : insertImpl ps given
1321 insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =
1322 PConstraint p l tm d : insertImpl ps given
1323 insertImpl (PConstraint p l ty d : ps) given =
1324 PConstraint p l (PResolveTC fc) d : insertImpl ps given
1325 insertImpl (PImp p _ l n ty d : ps) given =
1326 case find n given [] of
1327 Just (tm, given') -> PImp p False l n tm "" : insertImpl ps given'
1328 Nothing -> PImp p True l n Placeholder "" : insertImpl ps given
1329 insertImpl (PTacImplicit p l n sc ty d : ps) given =
1330 case find n given [] of
1331 Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'
1332 Nothing -> if inpat
1333 then PTacImplicit p l n sc Placeholder "" : insertImpl ps given
1334 else PTacImplicit p l n sc sc "" : insertImpl ps given
1335 insertImpl expected [] = []
1336 insertImpl _ given = given
1338 find n [] acc = Nothing
1339 find n (PImp _ _ _ n' t _ : gs) acc
1340 | n == n' = Just (t, reverse acc ++ gs)
1341 find n (PTacImplicit _ _ n' _ t _ : gs) acc
1342 | n == n' = Just (t, reverse acc ++ gs)
1343 find n (g : gs) acc = find n gs (g : acc)
1345-- replace non-linear occurrences with _
1346-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1347-- it is hard to get right!
1349stripLinear :: IState -> PTerm -> PTerm
1350stripLinear i tm = evalState (sl tm) [] where
1351 sl :: PTerm -> State [Name] PTerm
1352 sl (PRef fc f)
1353 | (_:_) <- lookupTy f (tt_ctxt i)
1354 = return $ PRef fc f
1355 | otherwise = do ns <- get
1356 if (f `elem` ns)
1357 then return Placeholder
1358 else do put (f : ns)
1359 return (PRef fc f)
1360 sl (PPatvar fc f)
1361 = do ns <- get
1362 if (f `elem` ns)
1363 then return Placeholder
1364 else do put (f : ns)
1365 return (PPatvar fc f)
1366 sl (PApp fc fn args) = do fn' <- sl fn
1367 args' <- mapM slA args
1368 return $ PApp fc fn' args'
1369 where slA (PImp p m l n t d) = do t' <- sl t
1370 return $ PImp p m l n t' d
1371 slA (PExp p l t d) = do t' <- sl t
1372 return $ PExp p l t' d
1373 slA (PConstraint p l t d)
1374 = do t' <- sl t
1375 return $ PConstraint p l t' d
1376 slA (PTacImplicit p l n sc t d)
1377 = do t' <- sl t
1378 return $ PTacImplicit p l n sc t' d
1379 sl x = return x
1381-- Remove functions which aren't applied to anything, which must then
1382-- be resolved by unification. Assume names resolved and alternatives
1383-- filled in (so no ambiguity).
1385stripUnmatchable :: IState -> PTerm -> PTerm
1386stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1387 su :: PTerm -> PTerm
1388 su (PRef fc f)
1389 | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1390 = Placeholder
1391 su (PApp fc fn args)
1392 = PApp fc fn (fmap (fmap su) args)
1393 su (PAlternative b alts)
1394 = let alts' = filter (/= Placeholder) (map su alts) in
1395 if null alts' then Placeholder
1396 else PAlternative b alts'
1397 su (PPair fc l r) = PPair fc (su l) (su r)
1398 su (PDPair fc l t r) = PDPair fc (su l) (su t) (su r)
1399 su t = t
1400stripUnmatchable i tm = tm
1402mkPApp fc a f [] = f
1403mkPApp fc a f as = let rest = drop a as in
1404 appRest fc (PApp fc f (take a as)) rest
1405 where
1406 appRest fc f [] = f
1407 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1409-- Find 'static' argument positions
1410-- (the declared ones, plus any names in argument position in the declared
1411-- statics)
1412-- FIXME: It's possible that this really has to happen after elaboration
1414findStatics :: IState -> PTerm -> (PTerm, [Bool])
1415findStatics ist tm = trace (showImp Nothing True False tm) $
1416 let (ns, ss) = fs tm in
1417 runState (pos ns ss tm) []
1418 where fs (PPi p n t sc)
1419 | Static <- pstatic p
1420 = let (ns, ss) = fs sc in
1421 (namesIn [] ist t : ns, n : ss)
1422 | otherwise = let (ns, ss) = fs sc in
1423 (ns, ss)
1424 fs _ = ([], [])
1426 inOne n ns = length (filter id (map (elem n) ns)) == 1
1428 pos ns ss (PPi p n t sc)
1429 | elem n ss = do sc' <- pos ns ss sc
1430 spos <- get
1431 put (True : spos)
1432 return (PPi (p { pstatic = Static }) n t sc')
1433 | otherwise = do sc' <- pos ns ss sc
1434 spos <- get
1435 put (False : spos)
1436 return (PPi p n t sc')
1437 pos ns ss t = return t
1439-- for 6.12/7 compatibility
1440data EitherErr a b = LeftErr a | RightOK b
1442instance Monad (EitherErr a) where
1443 return = RightOK
1445 (LeftErr e) >>= k = LeftErr e
1446 RightOK v >>= k = k v
1448toEither (LeftErr e) = Left e
1449toEither (RightOK ho) = Right ho
1451-- syntactic match of a against b, returning pair of variables in a
1452-- and what they match. Returns the pair that failed if not a match.
1454matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1455matchClause = matchClause' False
1457matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1458matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1459 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1461 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1462 fullApp x = x
1464 match' x y = match (fullApp x) (fullApp y)
1465 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1466 | fi == txt "fromInteger" && b == txt "builtins",
1467 PConstant (I _) <- getTm x = match (getTm x) x'
1468 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1469 | fi == txt "fromInteger" && b == txt "builtins",
1470 PConstant (I _) <- getTm x = match (getTm x) x'
1471 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1472 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1473 match (PApp _ f args) (PApp _ f' args')
1474 | length args == length args'
1475 = do mf <- match' f f'
1476 ms <- zipWithM matchArg args args'
1477 return (mf ++ concat ms)
1478-- match (PRef _ n) (PRef _ n') | n == n' = return []
1479-- | otherwise = Nothing
1480 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1481 match (PPatvar f n) xr = match (PRef f n) xr
1482 match xr (PPatvar f n) = match xr (PRef f n)
1483 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1484 match (PRef _ n) tm@(PRef _ n')
1485 | n == n' && not names &&
1486 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1487 || tm == Placeholder)
1488 = return [(n, tm)]
1489 | n == n' = return []
1490 match (PRef _ n) tm
1491 | not names && (not (isConName n (tt_ctxt i) ||
1492 isFnName n (tt_ctxt i)) || tm == Placeholder)
1493 = return [(n, tm)]
1494 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1495 mr <- match' r r'
1496 return (ml ++ mr)
1497 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1498 = do ml <- match' l l'
1499 mr <- match' r r'
1500 return (ml ++ mr)
1501 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1502 mr <- match r r'
1503 return (ml ++ mr)
1504 match (PTyped l r) x = match l x
1505 match x (PTyped l r) = match x l
1506 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1507 mr <- match' r r'
1508 return (ml ++ mr)
1509 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1510 mt <- match' t t'
1511 mr <- match' r r'
1512 return (ml ++ mt ++ mr)
1513 match (PAlternative a as) (PAlternative a' as')
1514 = do ms <- zipWithM match' as as'
1515 return (concat ms)
1516 match a@(PAlternative _ as) b
1517 = do let ms = zipWith match' as (repeat b)
1518 case (rights (map toEither ms)) of
1519 (x: _) -> return x
1520 _ -> LeftErr (a, b)
1521 match (PCase _ _ _) _ = return [] -- lifted out
1522 match (PMetavar _) _ = return [] -- modified
1523 match (PInferRef _ _) _ = return [] -- modified
1524 match (PQuote _) _ = return []
1525 match (PProof _) _ = return []
1526 match (PTactics _) _ = return []
1527 match (PRefl _ _) (PRefl _ _) = return []
1528 match (PResolveTC _) (PResolveTC _) = return []
1529 match (PTrue _) (PTrue _) = return []
1530 match (PFalse _) (PFalse _) = return []
1531 match (PReturn _) (PReturn _) = return []
1532 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1533 ms <- match' s s'
1534 return (mt ++ ms)
1535 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1536 ms <- match' s s'
1537 return (mt ++ ms)
1538 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1539 mty <- match' ty ty'
1540 ms <- match' s s'
1541 return (mt ++ mty ++ ms)
1542 match (PHidden x) (PHidden y) = match' x y
1543 match (PUnifyLog x) y = match' x y
1544 match x (PUnifyLog y) = match' x y
1545 match (PNoImplicits x) y = match' x y
1546 match x (PNoImplicits y) = match' x y
1547 match Placeholder _ = return []
1548 match _ Placeholder = return []
1549 match (PResolveTC _) _ = return []
1550 match a b | a == b = return []
1551 | otherwise = LeftErr (a, b)
1553 checkRpts (RightOK ms) = check ms where
1554 check ((n,t):xs)
1555 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1556 then Left (t, t')
1557 else check xs
1558 check (_:xs) = check xs
1559 check [] = Right ms
1560 checkRpts (LeftErr x) = Left x
1562substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1563substMatches ms = substMatchesShadow ms []
1565substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1566substMatchesShadow [] shs t = t
1567substMatchesShadow ((n,tm):ns) shs t
1568 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1570substMatch :: Name -> PTerm -> PTerm -> PTerm
1571substMatch n = substMatchShadow n []
1573substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1574substMatchShadow n shs tm t = sm shs t where
1575 sm xs (PRef _ n') | n == n' = tm
1576 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1577 sm xs (PPi p x t sc)
1578 | x `elem` xs
1579 = let x' = nextName x in
1580 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1581 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1582 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1583 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1584 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1585 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1586 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1587 (fmap (sm xs) tm)
1588 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1589 sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)
1590 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)
1591 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1592 sm xs (PHidden x) = PHidden (sm xs x)
1593 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1594 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1595 sm xs x = x
1597 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1598 fullApp x = x
1600shadow :: Name -> Name -> PTerm -> PTerm
1601shadow n n' t = sm t where
1602 sm (PRef fc x) | n == x = PRef fc n'
1603 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1604 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1605 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1606 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1607 sm (PEq f x y) = PEq f (sm x) (sm y)
1608 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1609 sm (PTyped x y) = PTyped (sm x) (sm y)
1610 sm (PPair f x y) = PPair f (sm x) (sm y)
1611 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1612 sm (PAlternative a as) = PAlternative a (map sm as)
1613 sm (PHidden x) = PHidden (sm x)
1614 sm (PUnifyLog x) = PUnifyLog (sm x)
1615 sm (PNoImplicits x) = PNoImplicits (sm x)
1616 sm x = x