git.iko.soy/Idris-dev
on 80a67c5 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1616 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 "->") = [UN "f",UN "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 (MN 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 ('@':'@':_)) = True
213 chaser (NS n _) = chaser n
214 chaser _ = False
216addClass :: Name -> ClassInfo -> Idris ()
217addClass n i
218 = do ist <- getIState
219 let i' = case lookupCtxt n (idris_classes ist) of
220 [c] -> c { class_instances = class_instances i }
221 _ -> i
222 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
224addIBC :: IBCWrite -> Idris ()
225addIBC ibc@(IBCDef n)
226 = do i <- getIState
227 when (notDef (ibc_write i)) $
228 putIState $ i { ibc_write = ibc : ibc_write i }
229 where notDef [] = True
230 notDef (IBCDef n': is) | n == n' = False
231 notDef (_ : is) = notDef is
232addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
234clearIBC :: Idris ()
235clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
237resetNameIdx :: Idris ()
238resetNameIdx = do i <- getIState
239 put (i { idris_nameIdx = (0, emptyContext) })
241-- Used to preserve sharing of names
242addNameIdx :: Name -> Idris (Int, Name)
243addNameIdx n = do i <- getIState
244 let (i', x) = addNameIdx' i n
245 return x
247addNameIdx' :: IState -> Name -> (IState, (Int, Name))
248addNameIdx' i n
249 = let idxs = snd (idris_nameIdx i) in
250 case lookupCtxt n idxs of
251 [x] -> (i, x)
252 _ -> let i' = fst (idris_nameIdx i) + 1 in
253 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
255getHdrs :: Codegen -> Idris [String]
256getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
258setErrLine :: Int -> Idris ()
259setErrLine x = do i <- getIState;
260 case (errLine i) of
261 Nothing -> putIState $ i { errLine = Just x }
262 Just _ -> return ()
264clearErr :: Idris ()
265clearErr = do i <- getIState
266 putIState $ i { errLine = Nothing }
268getSO :: Idris (Maybe String)
269getSO = do i <- getIState
270 return (compiled_so i)
272setSO :: Maybe String -> Idris ()
273setSO s = do i <- getIState
274 putIState $ (i { compiled_so = s })
276getIState :: Idris IState
277getIState = get
279putIState :: IState -> Idris ()
280putIState = put
282-- | A version of liftIO that puts errors into the exception type of the Idris monad
283runIO :: IO a -> Idris a
284runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
285-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
287getName :: Idris Int
288getName = do i <- getIState;
289 let idx = idris_name i;
290 putIState $ (i { idris_name = idx + 1 })
291 return idx
293addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
294addInternalApp fp l t
295 = do i <- getIState
296 putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })
298getInternalApp :: FilePath -> Int -> Idris PTerm
299getInternalApp fp l = do i <- getIState
300 case lookup (fp, l) (idris_lineapps i) of
301 Just n' -> return n'
302 Nothing -> return Placeholder
303 -- TODO: What if it's not there?
305-- Pattern definitions are only used for coverage checking, so erase them
306-- when we're done
307clearOrigPats :: Idris ()
308clearOrigPats = do i <- get
309 let ps = idris_patdefs i
310 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
311 put (i { idris_patdefs = ps' })
313-- Erase types from Ps in the context (basically ending up with what's in
314-- the .ibc, which is all we need after all the analysis is done)
315clearPTypes :: Idris ()
316clearPTypes = do i <- get
317 let ctxt = tt_ctxt i
318 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
319 where pErase (CaseOp c t tys orig tot cds)
320 = CaseOp c t tys orig [] (pErase' cds)
321 pErase x = x
322 pErase' (CaseDefs _ (cs, c) _ rs)
323 = let c' = (cs, fmap pEraseType c) in
324 CaseDefs c' c' c' rs
326checkUndefined :: FC -> Name -> Idris ()
327checkUndefined fc n
328 = do i <- getContext
329 case lookupTy n i of
330 (_:_) -> fail $ show fc ++ ":" ++
331 show n ++ " already defined"
332 _ -> return ()
334isUndefined :: FC -> Name -> Idris Bool
335isUndefined fc n
336 = do i <- getContext
337 case lookupTy n i of
338 (_:_) -> return False
339 _ -> return True
341setContext :: Context -> Idris ()
342setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
344updateContext :: (Context -> Context) -> Idris ()
345updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
347addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
348addConstraints fc (v, cs)
349 = do i <- getIState
350 let ctxt = tt_ctxt i
351 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
352 next_tvar = v }
353 let ics = zip cs (repeat fc) ++ idris_constraints i
354 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
356addDeferred = addDeferred' Ref
357addDeferredTyCon = addDeferred' (TCon 0 0)
359addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
360addDeferred' nt ns
361 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns
362 i <- getIState
363 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
364 idris_metavars i }
365 where tidyNames used (Bind (MN i x) b sc)
366 = let n' = uniqueName (UN x) used in
367 Bind n' b $ tidyNames (n':used) sc
368 tidyNames used (Bind n b sc)
369 = let n' = uniqueName n used in
370 Bind n' b $ tidyNames (n':used) sc
371 tidyNames used b = b
373solveDeferred :: Name -> Idris ()
374solveDeferred n = do i <- getIState
375 putIState $ i { idris_metavars =
376 filter (\(n', _) -> n/=n')
377 (idris_metavars i) }
379getUndefined :: Idris [Name]
380getUndefined = do i <- getIState
381 return (map fst (idris_metavars i) \\ primDefs)
383ihPrintResult :: Handle -> String -> Idris ()
384ihPrintResult h s = do i <- getIState
385 case idris_outputmode i of
386 RawOutput -> case s of
387 "" -> return ()
388 s -> runIO $ hPutStrLn h s
389 IdeSlave n ->
390 let good = SexpList [SymbolAtom "ok", toSExp s] in
391 runIO $ hPutStrLn h $ convSExp "return" good n
393ihPrintError :: Handle -> String -> Idris ()
394ihPrintError h s = do i <- getIState
395 case idris_outputmode i of
396 RawOutput -> case s of
397 "" -> return ()
398 s -> runIO $ hPutStrLn h s
399 IdeSlave n ->
400 let good = SexpList [SymbolAtom "error", toSExp s] in
401 runIO . hPutStrLn h $ convSExp "return" good n
403ihputStrLn :: Handle -> String -> Idris ()
404ihputStrLn h s = do i <- getIState
405 case idris_outputmode i of
406 RawOutput -> runIO $ hPutStrLn h s
407 IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n
409iputStrLn = ihputStrLn stdout
410iPrintError = ihPrintError stdout
411iPrintResult = ihPrintResult stdout
412iWarn = ihWarn stdout
414ideslavePutSExp :: SExpable a => String -> a -> Idris ()
415ideslavePutSExp cmd info = do i <- getIState
416 case idris_outputmode i of
417 IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
418 _ -> return ()
420-- this needs some typing magic and more structured output towards emacs
421iputGoal :: String -> Idris ()
422iputGoal s = do i <- getIState
423 case idris_outputmode i of
424 RawOutput -> runIO $ putStrLn s
425 IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" s n
427isetPrompt :: String -> Idris ()
428isetPrompt p = do i <- getIState
429 case idris_outputmode i of
430 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n
432ihWarn :: Handle -> FC -> String -> Idris ()
433ihWarn h fc err = do i <- getIState
434 case idris_outputmode i of
435 RawOutput -> runIO $ hPutStrLn h (show fc ++ ":" ++ err)
436 IdeSlave n -> runIO $ hPutStrLn h $ convSExp "warning" (fc_fname fc, fc_line fc, fc_column fc, err) n
438setLogLevel :: Int -> Idris ()
439setLogLevel l = do i <- getIState
440 let opts = idris_options i
441 let opt' = opts { opt_logLevel = l }
442 putIState $ i { idris_options = opt' }
444setCmdLine :: [Opt] -> Idris ()
445setCmdLine opts = do i <- getIState
446 let iopts = idris_options i
447 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
449getCmdLine :: Idris [Opt]
450getCmdLine = do i <- getIState
451 return (opt_cmdline (idris_options i))
453getDumpDefun :: Idris (Maybe FilePath)
454getDumpDefun = do i <- getIState
455 return $ findC (opt_cmdline (idris_options i))
456 where findC [] = Nothing
457 findC (DumpDefun x : _) = Just x
458 findC (_ : xs) = findC xs
460getDumpCases :: Idris (Maybe FilePath)
461getDumpCases = do i <- getIState
462 return $ findC (opt_cmdline (idris_options i))
463 where findC [] = Nothing
464 findC (DumpCases x : _) = Just x
465 findC (_ : xs) = findC xs
467logLevel :: Idris Int
468logLevel = do i <- getIState
469 return (opt_logLevel (idris_options i))
471setErrContext :: Bool -> Idris ()
472setErrContext t = do i <- getIState
473 let opts = idris_options i
474 let opt' = opts { opt_errContext = t }
475 putIState $ i { idris_options = opt' }
477errContext :: Idris Bool
478errContext = do i <- getIState
479 return (opt_errContext (idris_options i))
481useREPL :: Idris Bool
482useREPL = do i <- getIState
483 return (opt_repl (idris_options i))
485setREPL :: Bool -> Idris ()
486setREPL t = do i <- getIState
487 let opts = idris_options i
488 let opt' = opts { opt_repl = t }
489 putIState $ i { idris_options = opt' }
491setNoBanner :: Bool -> Idris ()
492setNoBanner n = do i <- getIState
493 let opts = idris_options i
494 let opt' = opts {opt_nobanner = n}
495 putIState $ i { idris_options = opt' }
497getNoBanner :: Idris Bool
498getNoBanner = do i <- getIState
499 let opts = idris_options i
500 return (opt_nobanner opts)
502setQuiet :: Bool -> Idris ()
503setQuiet q = do i <- getIState
504 let opts = idris_options i
505 let opt' = opts { opt_quiet = q }
506 putIState $ i { idris_options = opt' }
508getQuiet :: Idris Bool
509getQuiet = do i <- getIState
510 let opts = idris_options i
511 return (opt_quiet opts)
513setCodegen :: Codegen -> Idris ()
514setCodegen t = do i <- getIState
515 let opts = idris_options i
516 let opt' = opts { opt_codegen = t }
517 putIState $ i { idris_options = opt' }
519codegen :: Idris Codegen
520codegen = do i <- getIState
521 return (opt_codegen (idris_options i))
523setOutputTy :: OutputType -> Idris ()
524setOutputTy t = do i <- getIState
525 let opts = idris_options i
526 let opt' = opts { opt_outputTy = t }
527 putIState $ i { idris_options = opt' }
529outputTy :: Idris OutputType
530outputTy = do i <- getIState
531 return $ opt_outputTy $ idris_options i
533setIdeSlave :: Bool -> Idris ()
534setIdeSlave True = do i <- getIState
535 putIState $ i { idris_outputmode = (IdeSlave 0), idris_colourRepl = False }
536setIdeSlave False = return ()
538setTargetTriple :: String -> Idris ()
539setTargetTriple t = do i <- getIState
540 let opts = idris_options i
541 opt' = opts { opt_triple = t }
542 putIState $ i { idris_options = opt' }
544targetTriple :: Idris String
545targetTriple = do i <- getIState
546 return (opt_triple (idris_options i))
548setTargetCPU :: String -> Idris ()
549setTargetCPU t = do i <- getIState
550 let opts = idris_options i
551 opt' = opts { opt_cpu = t }
552 putIState $ i { idris_options = opt' }
554targetCPU :: Idris String
555targetCPU = do i <- getIState
556 return (opt_cpu (idris_options i))
558setOptLevel :: Word -> Idris ()
559setOptLevel t = do i <- getIState
560 let opts = idris_options i
561 opt' = opts { opt_optLevel = t }
562 putIState $ i { idris_options = opt' }
564optLevel :: Idris Word
565optLevel = do i <- getIState
566 return (opt_optLevel (idris_options i))
568verbose :: Idris Bool
569verbose = do i <- getIState
570 return (opt_verbose (idris_options i))
572setVerbose :: Bool -> Idris ()
573setVerbose t = do i <- getIState
574 let opts = idris_options i
575 let opt' = opts { opt_verbose = t }
576 putIState $ i { idris_options = opt' }
578typeInType :: Idris Bool
579typeInType = do i <- getIState
580 return (opt_typeintype (idris_options i))
582setTypeInType :: Bool -> Idris ()
583setTypeInType t = do i <- getIState
584 let opts = idris_options i
585 let opt' = opts { opt_typeintype = t }
586 putIState $ i { idris_options = opt' }
588coverage :: Idris Bool
589coverage = do i <- getIState
590 return (opt_coverage (idris_options i))
592setCoverage :: Bool -> Idris ()
593setCoverage t = do i <- getIState
594 let opts = idris_options i
595 let opt' = opts { opt_coverage = t }
596 putIState $ i { idris_options = opt' }
598setIBCSubDir :: FilePath -> Idris ()
599setIBCSubDir fp = do i <- getIState
600 let opts = idris_options i
601 let opt' = opts { opt_ibcsubdir = fp }
602 putIState $ i { idris_options = opt' }
604valIBCSubDir :: IState -> Idris FilePath
605valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
607addImportDir :: FilePath -> Idris ()
608addImportDir fp = do i <- getIState
609 let opts = idris_options i
610 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
611 putIState $ i { idris_options = opt' }
613setImportDirs :: [FilePath] -> Idris ()
614setImportDirs fps = do i <- getIState
615 let opts = idris_options i
616 let opt' = opts { opt_importdirs = fps }
617 putIState $ i { idris_options = opt' }
619allImportDirs :: Idris [FilePath]
620allImportDirs = do i <- getIState
621 let optdirs = opt_importdirs (idris_options i)
622 return ("." : reverse optdirs)
624colourise :: Idris Bool
625colourise = do i <- getIState
626 return $ idris_colourRepl i
628setColourise :: Bool -> Idris ()
629setColourise b = do i <- getIState
630 putIState $ i { idris_colourRepl = b }
632setOutH :: Handle -> Idris ()
633setOutH h = do i <- getIState
634 putIState $ i { idris_outh = h }
636impShow :: Idris Bool
637impShow = do i <- getIState
638 return (opt_showimp (idris_options i))
640setImpShow :: Bool -> Idris ()
641setImpShow t = do i <- getIState
642 let opts = idris_options i
643 let opt' = opts { opt_showimp = t }
644 putIState $ i { idris_options = opt' }
646setColour :: ColourType -> IdrisColour -> Idris ()
647setColour ct c = do i <- getIState
648 let newTheme = setColour' ct c (idris_colourTheme i)
649 putIState $ i { idris_colourTheme = newTheme }
650 where setColour' KeywordColour c t = t { keywordColour = c }
651 setColour' BoundVarColour c t = t { boundVarColour = c }
652 setColour' ImplicitColour c t = t { implicitColour = c }
653 setColour' FunctionColour c t = t { functionColour = c }
654 setColour' TypeColour c t = t { typeColour = c }
655 setColour' DataColour c t = t { dataColour = c }
656 setColour' PromptColour c t = t { promptColour = c }
658logLvl :: Int -> String -> Idris ()
659logLvl l str = do i <- getIState
660 let lvl = opt_logLevel (idris_options i)
661 when (lvl >= l) $
662 case idris_outputmode i of
663 RawOutput -> do runIO $ putStrLn str
664 IdeSlave n ->
665 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
666 runIO $ putStrLn $ convSExp "log" good n
668cmdOptType :: Opt -> Idris Bool
669cmdOptType x = do i <- getIState
670 return $ x `elem` opt_cmdline (idris_options i)
672iLOG :: String -> Idris ()
673iLOG = logLvl 1
675noErrors :: Idris Bool
676noErrors = do i <- getIState
677 case errLine i of
678 Nothing -> return True
679 _ -> return False
681setTypeCase :: Bool -> Idris ()
682setTypeCase t = do i <- getIState
683 let opts = idris_options i
684 let opt' = opts { opt_typecase = t }
685 putIState $ i { idris_options = opt' }
688-- For inferring types of things
690bi = fileFC "builtin"
692inferTy = MN 0 "__Infer"
693inferCon = MN 0 "__infer"
694inferDecl = PDatadecl inferTy
695 PType
696 [("", inferCon, PPi impl (MN 0 "iType") PType (
697 PPi expl (MN 0 "ival") (PRef bi (MN 0 "iType"))
698 (PRef bi inferTy)), bi)]
699inferOpts = []
701infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "iType") Placeholder True, pexp t]
702infP = P (TCon 6 0) inferTy (TType (UVal 0))
704getInferTerm, getInferType :: Term -> Term
705getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
706getInferTerm (App (App _ _) tm) = tm
707getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
709getInferType (Bind n b sc) = Bind n b $ getInferType sc
710getInferType (App (App _ ty) _) = ty
712-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class
714primNames = [unitTy, unitCon,
715 falseTy, pairTy, pairCon,
716 eqTy, eqCon, inferTy, inferCon]
718unitTy = MN 0 "__Unit"
719unitCon = MN 0 "__II"
720unitDecl = PDatadecl unitTy PType
721 [("", unitCon, PRef bi unitTy, bi)]
722unitOpts = [DefaultEliminator]
724falseTy = MN 0 "__False"
725falseDecl = PDatadecl falseTy PType []
726falseOpts = []
728pairTy = MN 0 "__Pair"
729pairCon = MN 0 "__MkPair"
730pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
731 [("", pairCon, PPi impl (n "A") PType (
732 PPi impl (n "B") PType (
733 PPi expl (n "a") (PRef bi (n "A")) (
734 PPi expl (n "b") (PRef bi (n "B"))
735 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
736 pexp (PRef bi (n "B"))])))), bi)]
737 where n a = MN 0 a
738pairOpts = []
740eqTy = UN "="
741eqCon = UN "refl"
742eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),
743 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
744 PType)
745 [("", eqCon, PPi impl (n "A") PType (
746 PPi impl (n "x") (PRef bi (n "A"))
747 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
748 pimp (n "B") Placeholder False,
749 pexp (PRef bi (n "x")),
750 pexp (PRef bi (n "x"))])), bi)]
751 where n a = MN 0 a
752eqOpts = []
754elimName = UN "__Elim"
755elimMethElimTy = UN "__elimTy"
756elimMethElim = UN "elim"
757elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(UN "scrutineeType", PType)]
758 [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,
759 PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
761-- Defined in builtins.idr
762sigmaTy = UN "Exists"
763existsCon = UN "Ex_intro"
765piBind :: [(Name, PTerm)] -> PTerm -> PTerm
766piBind = piBindp expl
768piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
769piBindp p [] t = t
770piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
772-- Dealing with parameters
774expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
775 [Name] -> -- all names
776 [Name] -> -- names with no declaration
777 PTerm -> PTerm
778expandParams dec ps ns infs tm = en tm
779 where
780 -- if we shadow a name (say in a lambda binding) that is used in a call to
781 -- a lifted function, we need access to both names - once in the scope of the
782 -- binding and once to call the lifted functions. So we'll explicitly shadow
783 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
784 -- but we didn't...)
786 mkShadow (UN n) = MN 0 n
787 mkShadow (MN i n) = MN (i+1) n
788 mkShadow (NS x s) = NS (mkShadow x) s
790 en (PLam n t s)
791 | n `elem` (map fst ps ++ ns)
792 = let n' = mkShadow n in
793 PLam n' (en t) (en (shadow n n' s))
794 | otherwise = PLam n (en t) (en s)
795 en (PPi p n t s)
796 | n `elem` (map fst ps ++ ns)
797 = let n' = mkShadow n in
798 PPi p n' (en t) (en (shadow n n' s))
799 | otherwise = PPi p n (en t) (en s)
800 en (PLet n ty v s)
801 | n `elem` (map fst ps ++ ns)
802 = let n' = mkShadow n in
803 PLet n' (en ty) (en v) (en (shadow n n' s))
804 | otherwise = PLet n (en ty) (en v) (en s)
805 -- FIXME: Should only do this in a type signature!
806 en (PDPair f (PRef f' n) t r)
807 | n `elem` (map fst ps ++ ns) && t /= Placeholder
808 = let n' = mkShadow n in
809 PDPair f (PRef f' n') (en t) (en (shadow n n' r))
810 en (PEq f l r) = PEq f (en l) (en r)
811 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
812 en (PTyped l r) = PTyped (en l) (en r)
813 en (PPair f l r) = PPair f (en l) (en r)
814 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
815 en (PAlternative a as) = PAlternative a (map en as)
816 en (PHidden t) = PHidden (en t)
817 en (PUnifyLog t) = PUnifyLog (en t)
818 en (PNoImplicits t) = PNoImplicits (en t)
819 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
820 en (PProof ts) = PProof (map (fmap en) ts)
821 en (PTactics ts) = PTactics (map (fmap en) ts)
823 en (PQuote (Var n))
824 | n `nselem` ns = PQuote (Var (dec n))
825 en (PApp fc (PInferRef fc' n) as)
826 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
827 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
828 en (PApp fc (PRef fc' n) as)
829 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
830 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
831 | n `nselem` ns = PApp fc (PRef fc' (dec n))
832 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
833 en (PAppBind fc (PRef fc' n) as)
834 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
835 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
836 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
837 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
838 en (PRef fc n)
839 | n `elem` infs = PApp fc (PInferRef fc (dec n))
840 (map (pexp . (PRef fc)) (map fst ps))
841 | n `nselem` ns = PApp fc (PRef fc (dec n))
842 (map (pexp . (PRef fc)) (map fst ps))
843 en (PInferRef fc n)
844 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
845 (map (pexp . (PRef fc)) (map fst ps))
846 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
847 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
848 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
849 en t = t
851 nselem x [] = False
852 nselem x (y : xs) | nseq x y = True
853 | otherwise = nselem x xs
855 nseq x y = nsroot x == nsroot y
857expandParamsD :: Bool -> -- True = RHS only
858 IState ->
859 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
860expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)
861 = if n `elem` ns && (not rhsonly)
862 then -- trace (show (n, expandParams dec ps ns ty)) $
863 PTy doc syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
864 else --trace (show (n, expandParams dec ps ns ty)) $
865 PTy doc syn fc o n (expandParams dec ps ns [] ty)
866expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
867 = if n `elem` ns && (not rhsonly)
868 then -- trace (show (n, expandParams dec ps ns ty)) $
869 PPostulate doc syn fc o (dec n) (piBind ps
870 (expandParams dec ps ns [] ty))
871 else --trace (show (n, expandParams dec ps ns ty)) $
872 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
873expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
874 = let n' = if n `elem` ns then dec n else n in
875 PClauses fc opts n' (map expandParamsC cs)
876 where
877 expandParamsC (PClause fc n lhs ws rhs ds)
878 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
879 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
880 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
881 n' = if n `elem` ns then dec n else n
882 -- names bound on the lhs should not be expanded on the rhs
883 ns' = removeBound lhs ns in
884 PClause fc n' lhs'
885 (map (expandParams dec ps'' ns' []) ws)
886 (expandParams dec ps'' ns' [] rhs)
887 (map (expandParamsD True ist dec ps'' ns') ds)
888 expandParamsC (PWith fc n lhs ws wval ds)
889 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
890 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
891 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
892 n' = if n `elem` ns then dec n else n
893 ns' = removeBound lhs ns in
894 PWith fc n' lhs'
895 (map (expandParams dec ps'' ns' []) ws)
896 (expandParams dec ps'' ns' [] wval)
897 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
898 updateps yn nm [] = []
899 updateps yn nm (((a, t), i):as)
900 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
901 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
903 removeBound lhs ns = ns \\ nub (bnames lhs)
905 bnames (PRef _ n) = [n]
906 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
907 bnames (PPair _ l r) = bnames l ++ bnames r
908 bnames (PDPair _ l Placeholder r) = bnames l ++ bnames r
909 bnames _ = []
911expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
912 = PData doc syn fc co (expandPData pd)
913 where
914 -- just do the type decl, leave constructors alone (parameters will be
915 -- added implicitly)
916 expandPData (PDatadecl n ty cons)
917 = if n `elem` ns
918 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
919 (map econ cons)
920 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
921 econ (doc, n, t, fc)
922 = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc)
923expandParamsD rhs ist dec ps ns (PParams f params pds)
924 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
925 (map (expandParamsD True ist dec ps ns) pds)
926-- (map (expandParamsD ist dec ps ns) pds)
927expandParamsD rhs ist dec ps ns (PMutual f pds)
928 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
929expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
930 = PClass doc info f
931 (map (expandParams dec ps ns []) cs)
932 n
933 (map (mapsnd (expandParams dec ps ns [])) params)
934 (map (expandParamsD rhs ist dec ps ns) decls)
935expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
936 = PInstance info f
937 (map (expandParams dec ps ns []) cs)
938 n
939 (map (expandParams dec ps ns []) params)
940 (expandParams dec ps ns [] ty)
941 cn
942 (map (expandParamsD rhs ist dec ps ns) decls)
943expandParamsD rhs ist dec ps ns d = d
945mapsnd f (x, t) = (x, f t)
947-- Calculate a priority for a type, for deciding elaboration order
948-- * if it's just a type variable or concrete type, do it early (0)
949-- * if there's only type variables and injective constructors, do it next (1)
950-- * if there's a function type, next (2)
951-- * finally, everything else (3)
953getPriority :: IState -> PTerm -> Int
954getPriority i tm = 1 -- pri tm
955 where
956 pri (PRef _ n) =
957 case lookupP n (tt_ctxt i) of
958 ((P (DCon _ _) _ _):_) -> 1
959 ((P (TCon _ _) _ _):_) -> 1
960 ((P Ref _ _):_) -> 1
961 [] -> 0 -- must be locally bound, if it's not an error...
962 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
963 pri (PTrue _) = 0
964 pri (PFalse _) = 0
965 pri (PRefl _ _) = 1
966 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
967 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
968 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
969 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
970 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
971 pri (PTyped l r) = pri l
972 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
973 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
974 pri (PAlternative a as) = maximum (map pri as)
975 pri (PConstant _) = 0
976 pri Placeholder = 1
977 pri _ = 3
979addStatics :: Name -> Term -> PTerm -> Idris ()
980addStatics n tm ptm =
981 do let (statics, dynamics) = initStatics tm ptm
982 let stnames = nub $ concatMap freeArgNames (map snd statics)
983 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
984 -- also get the arguments which are 'uniquely inferrable' from
985 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
986 let statics' = nub $ map fst statics ++
987 filter (\x -> not (elem x dnames)) stnames
988 let stpos = staticList statics' tm
989 i <- getIState
990 when (not (null statics)) $
991 logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics
992 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
993 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
994 addIBC (IBCStatic n)
995 where
996 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
997 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
998 if pstatic p == Static then ((n, ty) : static, dynamic)
999 else if (not (searchArg p))
1000 then (static, (n, ty) : dynamic)
1001 else (static, dynamic)
1002 initStatics t pt = ([], [])
1004 freeArgNames (Bind n (Pi ty) sc)
1005 = nub $ freeArgNames ty
1006 freeArgNames tm = let (_, args) = unApply tm in
1007 concatMap freeNames args
1009 -- if a name appears in a type class or tactic implicit index, it doesn't
1010 -- affect its 'uniquely inferrable' from a static status since these are
1011 -- resolved by searching.
1012 searchArg (Constraint _ _ _) = True
1013 searchArg (TacImp _ _ _ _) = True
1014 searchArg _ = False
1016 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
1017 staticList _ _ = []
1019-- Dealing with implicit arguments
1021-- Add constraint bindings from using block
1023addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1024addUsingConstraints syn fc t
1025 = do ist <- get
1026 let ns = namesIn [] ist t
1027 let cs = getConstraints t -- check declared constraints
1028 let addconsts = uconsts \\ cs
1029 -- if all names in the arguments of addconsts appear in ns,
1030 -- add the constraint implicitly
1031 return (doAdd addconsts ns t)
1032 where uconsts = filter uconst (using syn)
1033 uconst (UConstraint _ _) = True
1034 uconst _ = False
1036 doAdd [] _ t = t
1037 -- if all of args in ns, then add it
1038 doAdd (UConstraint c args : cs) ns t
1039 | all (\n -> elem n ns) args
1040 = PPi (Constraint False Dynamic "") (MN 0 "cu")
1041 (mkConst c args) (doAdd cs ns t)
1042 | otherwise = doAdd cs ns t
1044 mkConst c args = PApp fc (PRef fc c)
1045 (map (\n -> PExp 0 False (PRef fc n) "") args)
1047 getConstraints (PPi (Constraint _ _ _) _ c sc)
1048 = getcapp c ++ getConstraints sc
1049 getConstraints (PPi _ _ c sc) = getConstraints sc
1050 getConstraints _ = []
1052 getcapp (PApp _ (PRef _ c) args)
1053 = do ns <- mapM getName args
1054 return (UConstraint c ns)
1055 getcapp _ = []
1057 getName (PExp _ _ (PRef _ n) _) = return n
1058 getName _ = []
1060-- Add implicit Pi bindings for any names in the term which appear in an
1061-- argument position.
1063-- This has become a right mess already. Better redo it some time...
1065implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
1066implicit syn n ptm = implicit' syn [] n ptm
1068implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1069implicit' syn ignore n ptm
1070 = do i <- getIState
1071 let (tm', impdata) = implicitise syn ignore i ptm
1072-- let (tm'', spos) = findStatics i tm'
1073 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1074 addIBC (IBCImp n)
1075 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1076-- i <- get
1077-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1078 return tm'
1080implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1081implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1082 let (declimps, ns') = execState (imps True [] tm) ([], [])
1083 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1084 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1085 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1086 if null ns
1087 then (tm, reverse declimps)
1088 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1089 where
1090 uvars = map ipair (filter uimplicit (using syn))
1091 pvars = syn_params syn
1093 inUsing n = n `elem` map fst uvars
1095 ipair (UImplicit x y) = (x, y)
1096 uimplicit (UImplicit _ _) = True
1097 uimplicit _ = False
1099 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1100 | otherwise = x : dropAll xs ys
1101 dropAll [] ys = []
1103 imps top env (PApp _ f as)
1104 = do (decls, ns) <- get
1105 let isn = concatMap (namesIn uvars ist) (map getTm as)
1106 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1107 imps top env (PPi (Imp l _ doc _) n ty sc)
1108 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1109 (decls , ns) <- get
1110 put (PImp (getPriority ist ty) True l n Placeholder doc : decls,
1111 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1112 imps True (n:env) sc
1113 imps top env (PPi (Exp l _ doc _) n ty sc)
1114 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1115 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1116 _ -> [])
1117 (decls, ns) <- get -- ignore decls in HO types
1118 put (PExp (getPriority ist ty) l Placeholder doc : decls,
1119 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1120 imps True (n:env) sc
1121 imps top env (PPi (Constraint l _ doc) n ty sc)
1122 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1123 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1124 _ -> [])
1125 (decls, ns) <- get -- ignore decls in HO types
1126 put (PConstraint 10 l Placeholder doc : decls,
1127 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1128 imps True (n:env) sc
1129 imps top env (PPi (TacImp l _ scr doc) n ty sc)
1130 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1131 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1132 _ -> [])
1133 (decls, ns) <- get -- ignore decls in HO types
1134 put (PTacImplicit 10 l n scr Placeholder doc : decls,
1135 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1136 imps True (n:env) sc
1137 imps top env (PEq _ l r)
1138 = do (decls, ns) <- get
1139 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1140 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1141 imps top env (PRewrite _ l r _)
1142 = do (decls, ns) <- get
1143 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1144 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1145 imps top env (PTyped l r)
1146 = imps top env l
1147 imps top env (PPair _ l r)
1148 = do (decls, ns) <- get
1149 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1150 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1151 imps top env (PDPair _ (PRef _ n) t r)
1152 = do (decls, ns) <- get
1153 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1154 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1155 imps top env (PDPair _ l t r)
1156 = do (decls, ns) <- get
1157 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1158 namesIn uvars ist r
1159 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1160 imps top env (PAlternative a as)
1161 = do (decls, ns) <- get
1162 let isn = concatMap (namesIn uvars ist) as
1163 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1164 imps top env (PLam n ty sc)
1165 = do imps False env ty
1166 imps False (n:env) sc
1167 imps top env (PHidden tm) = imps False env tm
1168 imps top env (PUnifyLog tm) = imps False env tm
1169 imps top env (PNoImplicits tm) = imps False env tm
1170 imps top env _ = return ()
1172 pibind using [] sc = sc
1173 pibind using (n:ns) sc
1174 = case lookup n using of
1175 Just ty -> PPi (Imp False Dynamic "" False) n ty (pibind using ns sc)
1176 Nothing -> PPi (Imp False Dynamic "" False) n Placeholder
1177 (pibind using ns sc)
1179-- Add implicit arguments in function calls
1180addImplPat :: IState -> PTerm -> PTerm
1181addImplPat = addImpl' True [] []
1183addImplBound :: IState -> [Name] -> PTerm -> PTerm
1184addImplBound ist ns = addImpl' False ns [] ist
1186addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1187addImplBoundInf ist ns inf = addImpl' False ns inf ist
1189addImpl :: IState -> PTerm -> PTerm
1190addImpl = addImpl' False [] []
1192-- TODO: in patterns, don't add implicits to function names guarded by constructors
1193-- and *not* inside a PHidden
1195addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1196addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm
1197 where
1198 ai env (PRef fc f)
1199 | f `elem` infns = PInferRef fc f
1200 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f []
1201 ai env (PHidden (PRef fc f))
1202 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f []
1203 ai env (PEq fc l r) = let l' = ai env l
1204 r' = ai env r in
1205 PEq fc l' r'
1206 ai env (PRewrite fc l r g) = let l' = ai env l
1207 r' = ai env r
1208 g' = fmap (ai env) g in
1209 PRewrite fc l' r' g'
1210 ai env (PTyped l r) = let l' = ai env l
1211 r' = ai env r in
1212 PTyped l' r'
1213 ai env (PPair fc l r) = let l' = ai env l
1214 r' = ai env r in
1215 PPair fc l' r'
1216 ai env (PDPair fc l t r) = let l' = ai env l
1217 t' = ai env t
1218 r' = ai env r in
1219 PDPair fc l' t' r'
1220 ai env (PAlternative a as) = let as' = map (ai env) as in
1221 PAlternative a as'
1222 ai env (PApp fc (PInferRef _ f) as)
1223 = let as' = map (fmap (ai env)) as in
1224 PApp fc (PInferRef fc f) as'
1225 ai env (PApp fc ftm@(PRef _ f) as)
1226 | f `elem` infns = ai env (PApp fc (PInferRef fc f) as)
1227 | not (f `elem` map fst env)
1228 = let as' = map (fmap (ai env)) as in
1229 handleErr $ aiFn inpat False ist fc f as'
1230 | Just (Just ty) <- lookup f env
1231 = let as' = map (fmap (ai env)) as
1232 arity = getPArity ty in
1233 mkPApp fc arity ftm as'
1234 ai env (PApp fc f as) = let f' = ai env f
1235 as' = map (fmap (ai env)) as in
1236 mkPApp fc 1 f' as'
1237 ai env (PCase fc c os) = let c' = ai env c
1238 os' = map (pmap (ai env)) os in
1239 PCase fc c' os'
1240 ai env (PLam n ty sc) = let ty' = ai env ty
1241 sc' = ai ((n, Just ty):env) sc in
1242 PLam n ty' sc'
1243 ai env (PLet n ty val sc)
1244 = let ty' = ai env ty
1245 val' = ai env val
1246 sc' = ai ((n, Just ty):env) sc in
1247 PLet n ty' val' sc'
1248 ai env (PPi p n ty sc) = let ty' = ai env ty
1249 sc' = ai ((n, Just ty):env) sc in
1250 PPi p n ty' sc'
1251 ai env (PGoal fc r n sc) = let r' = ai env r
1252 sc' = ai ((n, Nothing):env) sc in
1253 PGoal fc r' n sc'
1254 ai env (PHidden tm) = PHidden (ai env tm)
1255 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
1256 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
1257 ai env (PRefl fc tm) = PRefl fc (ai env tm)
1258 ai env (PUnifyLog tm) = PUnifyLog (ai env tm)
1259 ai env (PNoImplicits tm) = PNoImplicits (ai env tm)
1260 ai env tm = tm
1262 handleErr (Left err) = PElabError err
1263 handleErr (Right x) = x
1265-- if in a pattern, and there are no arguments, and there's no possible
1266-- names with zero explicit arguments, don't add implicits.
1268aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
1269aiFn inpat True ist fc f []
1270 = case lookupDef f (tt_ctxt ist) of
1271 [] -> Right $ PPatvar fc f
1272 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1273 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1274 if (not (vname f) || tcname f
1275 || any (conCaf (tt_ctxt ist)) ialts)
1276-- any constructor alts || any allImp ialts))
1277 then aiFn inpat False ist fc f [] -- use it as a constructor
1278 else Right $ PPatvar fc f
1279 where imp (PExp _ _ _ _) = False
1280 imp _ = True
1281-- allImp [] = False
1282 allImp xs = all imp xs
1283 constructor (TyDecl (DCon _ _) _) = True
1284 constructor _ = False
1286 conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
1288 vname (UN n) = True -- non qualified
1289 vname _ = False
1291aiFn inpat expat ist fc f as
1292 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1293aiFn inpat expat ist fc f as
1294 -- This is where namespaces get resolved by adding PAlternative
1295 = do let ns = lookupCtxtName f (idris_implicits ist)
1296 let ns' = filter (\(n, _) -> notHidden n) ns
1297 case ns' of
1298 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1299 [] -> if f `elem` (map fst (idris_metavars ist))
1300 then Right $ PApp fc (PRef fc f) as
1301 else Right $ mkPApp fc (length as) (PRef fc f) as
1302 alts -> Right $
1303 PAlternative True $
1304 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1305 (insertImpl ns as)) alts
1306 where
1307 notHidden n = case getAccessibility n of
1308 Hidden -> False
1309 _ -> True
1311 getAccessibility n
1312 = case lookupDefAcc n False (tt_ctxt ist) of
1313 [(n,t)] -> t
1314 _ -> Public
1317 insertImpl :: [PArg] -> [PArg] -> [PArg]
1318 insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =
1319 PExp p l tm d : insertImpl ps given
1320 insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =
1321 PConstraint p l tm d : insertImpl ps given
1322 insertImpl (PConstraint p l ty d : ps) given =
1323 PConstraint p l (PResolveTC fc) d : insertImpl ps given
1324 insertImpl (PImp p _ l n ty d : ps) given =
1325 case find n given [] of
1326 Just (tm, given') -> PImp p False l n tm "" : insertImpl ps given'
1327 Nothing -> PImp p True l n Placeholder "" : insertImpl ps given
1328 insertImpl (PTacImplicit p l n sc' ty d : ps) given =
1329 let sc = addImpl ist sc' in
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 "fromInteger") ["builtins"])) [_,_,x]) x'
1466 | PConstant (I _) <- getTm x = match (getTm x) x'
1467 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
1468 | PConstant (I _) <- getTm x = match (getTm x) x'
1469 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
1470 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
1471 match (PApp _ f args) (PApp _ f' args')
1472 | length args == length args'
1473 = do mf <- match' f f'
1474 ms <- zipWithM matchArg args args'
1475 return (mf ++ concat ms)
1476-- match (PRef _ n) (PRef _ n') | n == n' = return []
1477-- | otherwise = Nothing
1478 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1479 match (PPatvar f n) xr = match (PRef f n) xr
1480 match xr (PPatvar f n) = match xr (PRef f n)
1481 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1482 match (PRef _ n) tm@(PRef _ n')
1483 | n == n' && not names &&
1484 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1485 || tm == Placeholder)
1486 = return [(n, tm)]
1487 | n == n' = return []
1488 match (PRef _ n) tm
1489 | not names && (not (isConName n (tt_ctxt i) ||
1490 isFnName n (tt_ctxt i)) || tm == Placeholder)
1491 = return [(n, tm)]
1492 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1493 mr <- match' r r'
1494 return (ml ++ mr)
1495 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1496 = do ml <- match' l l'
1497 mr <- match' r r'
1498 return (ml ++ mr)
1499 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1500 mr <- match r r'
1501 return (ml ++ mr)
1502 match (PTyped l r) x = match l x
1503 match x (PTyped l r) = match x l
1504 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1505 mr <- match' r r'
1506 return (ml ++ mr)
1507 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1508 mt <- match' t t'
1509 mr <- match' r r'
1510 return (ml ++ mt ++ mr)
1511 match (PAlternative a as) (PAlternative a' as')
1512 = do ms <- zipWithM match' as as'
1513 return (concat ms)
1514 match a@(PAlternative _ as) b
1515 = do let ms = zipWith match' as (repeat b)
1516 case (rights (map toEither ms)) of
1517 (x: _) -> return x
1518 _ -> LeftErr (a, b)
1519 match (PCase _ _ _) _ = return [] -- lifted out
1520 match (PMetavar _) _ = return [] -- modified
1521 match (PInferRef _ _) _ = return [] -- modified
1522 match (PQuote _) _ = return []
1523 match (PProof _) _ = return []
1524 match (PTactics _) _ = return []
1525 match (PRefl _ _) (PRefl _ _) = return []
1526 match (PResolveTC _) (PResolveTC _) = return []
1527 match (PTrue _) (PTrue _) = return []
1528 match (PFalse _) (PFalse _) = return []
1529 match (PReturn _) (PReturn _) = return []
1530 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1531 ms <- match' s s'
1532 return (mt ++ ms)
1533 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1534 ms <- match' s s'
1535 return (mt ++ ms)
1536 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1537 mty <- match' ty ty'
1538 ms <- match' s s'
1539 return (mt ++ mty ++ ms)
1540 match (PHidden x) (PHidden y) = match' x y
1541 match (PUnifyLog x) y = match' x y
1542 match x (PUnifyLog y) = match' x y
1543 match (PNoImplicits x) y = match' x y
1544 match x (PNoImplicits y) = match' x y
1545 match Placeholder _ = return []
1546 match _ Placeholder = return []
1547 match (PResolveTC _) _ = return []
1548 match a b | a == b = return []
1549 | otherwise = LeftErr (a, b)
1551 checkRpts (RightOK ms) = check ms where
1552 check ((n,t):xs)
1553 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1554 then Left (t, t')
1555 else check xs
1556 check (_:xs) = check xs
1557 check [] = Right ms
1558 checkRpts (LeftErr x) = Left x
1560substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1561substMatches ms = substMatchesShadow ms []
1563substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1564substMatchesShadow [] shs t = t
1565substMatchesShadow ((n,tm):ns) shs t
1566 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1568substMatch :: Name -> PTerm -> PTerm -> PTerm
1569substMatch n = substMatchShadow n []
1571substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1572substMatchShadow n shs tm t = sm shs t where
1573 sm xs (PRef _ n') | n == n' = tm
1574 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1575 sm xs (PPi p x t sc)
1576 | x `elem` xs
1577 = let x' = nextName x in
1578 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1579 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1580 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1581 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1582 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1583 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1584 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1585 (fmap (sm xs) tm)
1586 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1587 sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)
1588 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)
1589 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1590 sm xs (PHidden x) = PHidden (sm xs x)
1591 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1592 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1593 sm xs x = x
1595 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1596 fullApp x = x
1598shadow :: Name -> Name -> PTerm -> PTerm
1599shadow n n' t = sm t where
1600 sm (PRef fc x) | n == x = PRef fc n'
1601 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1602 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1603 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1604 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1605 sm (PEq f x y) = PEq f (sm x) (sm y)
1606 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1607 sm (PTyped x y) = PTyped (sm x) (sm y)
1608 sm (PPair f x y) = PPair f (sm x) (sm y)
1609 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1610 sm (PAlternative a as) = PAlternative a (map sm as)
1611 sm (PHidden x) = PHidden (sm x)
1612 sm (PUnifyLog x) = PUnifyLog (sm x)
1613 sm (PNoImplicits x) = PNoImplicits (sm x)
1614 sm x = x