git.iko.soy/Idris-dev
on a611deb help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1594 lines 66 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?
305checkUndefined :: FC -> Name -> Idris ()
306checkUndefined fc n
307 = do i <- getContext
308 case lookupTy n i of
309 (_:_) -> fail $ show fc ++ ":" ++
310 show n ++ " already defined"
311 _ -> return ()
313isUndefined :: FC -> Name -> Idris Bool
314isUndefined fc n
315 = do i <- getContext
316 case lookupTy n i of
317 (_:_) -> return False
318 _ -> return True
320setContext :: Context -> Idris ()
321setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
323updateContext :: (Context -> Context) -> Idris ()
324updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
326addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
327addConstraints fc (v, cs)
328 = do i <- getIState
329 let ctxt = tt_ctxt i
330 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
331 next_tvar = v }
332 let ics = zip cs (repeat fc) ++ idris_constraints i
333 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
335addDeferred = addDeferred' Ref
336addDeferredTyCon = addDeferred' (TCon 0 0)
338addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
339addDeferred' nt ns
340 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns
341 i <- getIState
342 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
343 idris_metavars i }
344 where tidyNames used (Bind (MN i x) b sc)
345 = let n' = uniqueName (UN x) used in
346 Bind n' b $ tidyNames (n':used) sc
347 tidyNames used (Bind n b sc)
348 = let n' = uniqueName n used in
349 Bind n' b $ tidyNames (n':used) sc
350 tidyNames used b = b
352solveDeferred :: Name -> Idris ()
353solveDeferred n = do i <- getIState
354 putIState $ i { idris_metavars =
355 filter (\(n', _) -> n/=n')
356 (idris_metavars i) }
358getUndefined :: Idris [Name]
359getUndefined = do i <- getIState
360 return (map fst (idris_metavars i) \\ primDefs)
362ihPrintResult :: Handle -> String -> Idris ()
363ihPrintResult h s = do i <- getIState
364 case idris_outputmode i of
365 RawOutput -> case s of
366 "" -> return ()
367 s -> runIO $ hPutStrLn h s
368 IdeSlave n ->
369 let good = SexpList [SymbolAtom "ok", toSExp s] in
370 runIO $ hPutStrLn h $ convSExp "return" good n
372ihPrintError :: Handle -> String -> Idris ()
373ihPrintError h s = do i <- getIState
374 case idris_outputmode i of
375 RawOutput -> case s of
376 "" -> return ()
377 s -> runIO $ hPutStrLn h s
378 IdeSlave n ->
379 let good = SexpList [SymbolAtom "error", toSExp s] in
380 runIO . hPutStrLn h $ convSExp "return" good n
382ihputStrLn :: Handle -> String -> Idris ()
383ihputStrLn h s = do i <- getIState
384 case idris_outputmode i of
385 RawOutput -> runIO $ hPutStrLn h s
386 IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n
388iputStrLn = ihputStrLn stdout
389iPrintError = ihPrintError stdout
390iPrintResult = ihPrintResult stdout
391iWarn = ihWarn stdout
393ideslavePutSExp :: SExpable a => String -> a -> Idris ()
394ideslavePutSExp cmd info = do i <- getIState
395 case idris_outputmode i of
396 IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
397 _ -> return ()
399-- this needs some typing magic and more structured output towards emacs
400iputGoal :: String -> Idris ()
401iputGoal s = do i <- getIState
402 case idris_outputmode i of
403 RawOutput -> runIO $ putStrLn s
404 IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" s n
406isetPrompt :: String -> Idris ()
407isetPrompt p = do i <- getIState
408 case idris_outputmode i of
409 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n
411ihWarn :: Handle -> FC -> String -> Idris ()
412ihWarn h fc err = do i <- getIState
413 case idris_outputmode i of
414 RawOutput -> runIO $ hPutStrLn h (show fc ++ ":" ++ err)
415 IdeSlave n -> runIO $ hPutStrLn h $ convSExp "warning" (fc_fname fc, fc_line fc, fc_column fc, err) n
417setLogLevel :: Int -> Idris ()
418setLogLevel l = do i <- getIState
419 let opts = idris_options i
420 let opt' = opts { opt_logLevel = l }
421 putIState $ i { idris_options = opt' }
423setCmdLine :: [Opt] -> Idris ()
424setCmdLine opts = do i <- getIState
425 let iopts = idris_options i
426 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
428getCmdLine :: Idris [Opt]
429getCmdLine = do i <- getIState
430 return (opt_cmdline (idris_options i))
432getDumpDefun :: Idris (Maybe FilePath)
433getDumpDefun = do i <- getIState
434 return $ findC (opt_cmdline (idris_options i))
435 where findC [] = Nothing
436 findC (DumpDefun x : _) = Just x
437 findC (_ : xs) = findC xs
439getDumpCases :: Idris (Maybe FilePath)
440getDumpCases = do i <- getIState
441 return $ findC (opt_cmdline (idris_options i))
442 where findC [] = Nothing
443 findC (DumpCases x : _) = Just x
444 findC (_ : xs) = findC xs
446logLevel :: Idris Int
447logLevel = do i <- getIState
448 return (opt_logLevel (idris_options i))
450setErrContext :: Bool -> Idris ()
451setErrContext t = do i <- getIState
452 let opts = idris_options i
453 let opt' = opts { opt_errContext = t }
454 putIState $ i { idris_options = opt' }
456errContext :: Idris Bool
457errContext = do i <- getIState
458 return (opt_errContext (idris_options i))
460useREPL :: Idris Bool
461useREPL = do i <- getIState
462 return (opt_repl (idris_options i))
464setREPL :: Bool -> Idris ()
465setREPL t = do i <- getIState
466 let opts = idris_options i
467 let opt' = opts { opt_repl = t }
468 putIState $ i { idris_options = opt' }
470setNoBanner :: Bool -> Idris ()
471setNoBanner n = do i <- getIState
472 let opts = idris_options i
473 let opt' = opts {opt_nobanner = n}
474 putIState $ i { idris_options = opt' }
476getNoBanner :: Idris Bool
477getNoBanner = do i <- getIState
478 let opts = idris_options i
479 return (opt_nobanner opts)
481setQuiet :: Bool -> Idris ()
482setQuiet q = do i <- getIState
483 let opts = idris_options i
484 let opt' = opts { opt_quiet = q }
485 putIState $ i { idris_options = opt' }
487getQuiet :: Idris Bool
488getQuiet = do i <- getIState
489 let opts = idris_options i
490 return (opt_quiet opts)
492setCodegen :: Codegen -> Idris ()
493setCodegen t = do i <- getIState
494 let opts = idris_options i
495 let opt' = opts { opt_codegen = t }
496 putIState $ i { idris_options = opt' }
498codegen :: Idris Codegen
499codegen = do i <- getIState
500 return (opt_codegen (idris_options i))
502setOutputTy :: OutputType -> Idris ()
503setOutputTy t = do i <- getIState
504 let opts = idris_options i
505 let opt' = opts { opt_outputTy = t }
506 putIState $ i { idris_options = opt' }
508outputTy :: Idris OutputType
509outputTy = do i <- getIState
510 return $ opt_outputTy $ idris_options i
512setIdeSlave :: Bool -> Idris ()
513setIdeSlave True = do i <- getIState
514 putIState $ i { idris_outputmode = (IdeSlave 0), idris_colourRepl = False }
515setIdeSlave False = return ()
517setTargetTriple :: String -> Idris ()
518setTargetTriple t = do i <- getIState
519 let opts = idris_options i
520 opt' = opts { opt_triple = t }
521 putIState $ i { idris_options = opt' }
523targetTriple :: Idris String
524targetTriple = do i <- getIState
525 return (opt_triple (idris_options i))
527setTargetCPU :: String -> Idris ()
528setTargetCPU t = do i <- getIState
529 let opts = idris_options i
530 opt' = opts { opt_cpu = t }
531 putIState $ i { idris_options = opt' }
533targetCPU :: Idris String
534targetCPU = do i <- getIState
535 return (opt_cpu (idris_options i))
537setOptLevel :: Word -> Idris ()
538setOptLevel t = do i <- getIState
539 let opts = idris_options i
540 opt' = opts { opt_optLevel = t }
541 putIState $ i { idris_options = opt' }
543optLevel :: Idris Word
544optLevel = do i <- getIState
545 return (opt_optLevel (idris_options i))
547verbose :: Idris Bool
548verbose = do i <- getIState
549 return (opt_verbose (idris_options i))
551setVerbose :: Bool -> Idris ()
552setVerbose t = do i <- getIState
553 let opts = idris_options i
554 let opt' = opts { opt_verbose = t }
555 putIState $ i { idris_options = opt' }
557typeInType :: Idris Bool
558typeInType = do i <- getIState
559 return (opt_typeintype (idris_options i))
561setTypeInType :: Bool -> Idris ()
562setTypeInType t = do i <- getIState
563 let opts = idris_options i
564 let opt' = opts { opt_typeintype = t }
565 putIState $ i { idris_options = opt' }
567coverage :: Idris Bool
568coverage = do i <- getIState
569 return (opt_coverage (idris_options i))
571setCoverage :: Bool -> Idris ()
572setCoverage t = do i <- getIState
573 let opts = idris_options i
574 let opt' = opts { opt_coverage = t }
575 putIState $ i { idris_options = opt' }
577setIBCSubDir :: FilePath -> Idris ()
578setIBCSubDir fp = do i <- getIState
579 let opts = idris_options i
580 let opt' = opts { opt_ibcsubdir = fp }
581 putIState $ i { idris_options = opt' }
583valIBCSubDir :: IState -> Idris FilePath
584valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
586addImportDir :: FilePath -> Idris ()
587addImportDir fp = do i <- getIState
588 let opts = idris_options i
589 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
590 putIState $ i { idris_options = opt' }
592setImportDirs :: [FilePath] -> Idris ()
593setImportDirs fps = do i <- getIState
594 let opts = idris_options i
595 let opt' = opts { opt_importdirs = fps }
596 putIState $ i { idris_options = opt' }
598allImportDirs :: Idris [FilePath]
599allImportDirs = do i <- getIState
600 let optdirs = opt_importdirs (idris_options i)
601 return ("." : reverse optdirs)
603colourise :: Idris Bool
604colourise = do i <- getIState
605 return $ idris_colourRepl i
607setColourise :: Bool -> Idris ()
608setColourise b = do i <- getIState
609 putIState $ i { idris_colourRepl = b }
611setOutH :: Handle -> Idris ()
612setOutH h = do i <- getIState
613 putIState $ i { idris_outh = h }
615impShow :: Idris Bool
616impShow = do i <- getIState
617 return (opt_showimp (idris_options i))
619setImpShow :: Bool -> Idris ()
620setImpShow t = do i <- getIState
621 let opts = idris_options i
622 let opt' = opts { opt_showimp = t }
623 putIState $ i { idris_options = opt' }
625setColour :: ColourType -> IdrisColour -> Idris ()
626setColour ct c = do i <- getIState
627 let newTheme = setColour' ct c (idris_colourTheme i)
628 putIState $ i { idris_colourTheme = newTheme }
629 where setColour' KeywordColour c t = t { keywordColour = c }
630 setColour' BoundVarColour c t = t { boundVarColour = c }
631 setColour' ImplicitColour c t = t { implicitColour = c }
632 setColour' FunctionColour c t = t { functionColour = c }
633 setColour' TypeColour c t = t { typeColour = c }
634 setColour' DataColour c t = t { dataColour = c }
635 setColour' PromptColour c t = t { promptColour = c }
637logLvl :: Int -> String -> Idris ()
638logLvl l str = do i <- getIState
639 let lvl = opt_logLevel (idris_options i)
640 when (lvl >= l) $
641 case idris_outputmode i of
642 RawOutput -> do runIO $ putStrLn str
643 IdeSlave n ->
644 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
645 runIO $ putStrLn $ convSExp "log" good n
647cmdOptType :: Opt -> Idris Bool
648cmdOptType x = do i <- getIState
649 return $ x `elem` opt_cmdline (idris_options i)
651iLOG :: String -> Idris ()
652iLOG = logLvl 1
654noErrors :: Idris Bool
655noErrors = do i <- getIState
656 case errLine i of
657 Nothing -> return True
658 _ -> return False
660setTypeCase :: Bool -> Idris ()
661setTypeCase t = do i <- getIState
662 let opts = idris_options i
663 let opt' = opts { opt_typecase = t }
664 putIState $ i { idris_options = opt' }
667-- For inferring types of things
669bi = fileFC "builtin"
671inferTy = MN 0 "__Infer"
672inferCon = MN 0 "__infer"
673inferDecl = PDatadecl inferTy
674 PType
675 [("", inferCon, PPi impl (MN 0 "iType") PType (
676 PPi expl (MN 0 "ival") (PRef bi (MN 0 "iType"))
677 (PRef bi inferTy)), bi)]
678inferOpts = []
680infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "iType") Placeholder True, pexp t]
681infP = P (TCon 6 0) inferTy (TType (UVal 0))
683getInferTerm, getInferType :: Term -> Term
684getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
685getInferTerm (App (App _ _) tm) = tm
686getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
688getInferType (Bind n b sc) = Bind n b $ getInferType sc
689getInferType (App (App _ ty) _) = ty
691-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class
693primNames = [unitTy, unitCon,
694 falseTy, pairTy, pairCon,
695 eqTy, eqCon, inferTy, inferCon]
697unitTy = MN 0 "__Unit"
698unitCon = MN 0 "__II"
699unitDecl = PDatadecl unitTy PType
700 [("", unitCon, PRef bi unitTy, bi)]
701unitOpts = [DefaultEliminator]
703falseTy = MN 0 "__False"
704falseDecl = PDatadecl falseTy PType []
705falseOpts = []
707pairTy = MN 0 "__Pair"
708pairCon = MN 0 "__MkPair"
709pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
710 [("", pairCon, PPi impl (n "A") PType (
711 PPi impl (n "B") PType (
712 PPi expl (n "a") (PRef bi (n "A")) (
713 PPi expl (n "b") (PRef bi (n "B"))
714 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
715 pexp (PRef bi (n "B"))])))), bi)]
716 where n a = MN 0 a
717pairOpts = []
719eqTy = UN "="
720eqCon = UN "refl"
721eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),
722 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
723 PType)
724 [("", eqCon, PPi impl (n "A") PType (
725 PPi impl (n "x") (PRef bi (n "A"))
726 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
727 pimp (n "B") Placeholder False,
728 pexp (PRef bi (n "x")),
729 pexp (PRef bi (n "x"))])), bi)]
730 where n a = MN 0 a
731eqOpts = []
733elimName = UN "__Elim"
734elimMethElimTy = UN "__elimTy"
735elimMethElim = UN "elim"
736elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(UN "scrutineeType", PType)]
737 [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,
738 PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
740-- Defined in builtins.idr
741sigmaTy = UN "Exists"
742existsCon = UN "Ex_intro"
744piBind :: [(Name, PTerm)] -> PTerm -> PTerm
745piBind = piBindp expl
747piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
748piBindp p [] t = t
749piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
751-- Dealing with parameters
753expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
754 [Name] -> -- all names
755 [Name] -> -- names with no declaration
756 PTerm -> PTerm
757expandParams dec ps ns infs tm = en tm
758 where
759 -- if we shadow a name (say in a lambda binding) that is used in a call to
760 -- a lifted function, we need access to both names - once in the scope of the
761 -- binding and once to call the lifted functions. So we'll explicitly shadow
762 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
763 -- but we didn't...)
765 mkShadow (UN n) = MN 0 n
766 mkShadow (MN i n) = MN (i+1) n
767 mkShadow (NS x s) = NS (mkShadow x) s
769 en (PLam n t s)
770 | n `elem` (map fst ps ++ ns)
771 = let n' = mkShadow n in
772 PLam n' (en t) (en (shadow n n' s))
773 | otherwise = PLam n (en t) (en s)
774 en (PPi p n t s)
775 | n `elem` (map fst ps ++ ns)
776 = let n' = mkShadow n in
777 PPi p n' (en t) (en (shadow n n' s))
778 | otherwise = PPi p n (en t) (en s)
779 en (PLet n ty v s)
780 | n `elem` (map fst ps ++ ns)
781 = let n' = mkShadow n in
782 PLet n' (en ty) (en v) (en (shadow n n' s))
783 | otherwise = PLet n (en ty) (en v) (en s)
784 -- FIXME: Should only do this in a type signature!
785 en (PDPair f (PRef f' n) t r)
786 | n `elem` (map fst ps ++ ns) && t /= Placeholder
787 = let n' = mkShadow n in
788 PDPair f (PRef f' n') (en t) (en (shadow n n' r))
789 en (PEq f l r) = PEq f (en l) (en r)
790 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
791 en (PTyped l r) = PTyped (en l) (en r)
792 en (PPair f l r) = PPair f (en l) (en r)
793 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
794 en (PAlternative a as) = PAlternative a (map en as)
795 en (PHidden t) = PHidden (en t)
796 en (PUnifyLog t) = PUnifyLog (en t)
797 en (PNoImplicits t) = PNoImplicits (en t)
798 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
799 en (PProof ts) = PProof (map (fmap en) ts)
800 en (PTactics ts) = PTactics (map (fmap en) ts)
802 en (PQuote (Var n))
803 | n `nselem` ns = PQuote (Var (dec n))
804 en (PApp fc (PInferRef fc' n) as)
805 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
806 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
807 en (PApp fc (PRef fc' n) as)
808 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
809 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
810 | n `nselem` ns = PApp fc (PRef fc' (dec n))
811 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
812 en (PAppBind fc (PRef fc' n) as)
813 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
814 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
815 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
816 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
817 en (PRef fc n)
818 | n `elem` infs = PApp fc (PInferRef fc (dec n))
819 (map (pexp . (PRef fc)) (map fst ps))
820 | n `nselem` ns = PApp fc (PRef fc (dec n))
821 (map (pexp . (PRef fc)) (map fst ps))
822 en (PInferRef fc n)
823 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
824 (map (pexp . (PRef fc)) (map fst ps))
825 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
826 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
827 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
828 en t = t
830 nselem x [] = False
831 nselem x (y : xs) | nseq x y = True
832 | otherwise = nselem x xs
834 nseq x y = nsroot x == nsroot y
836expandParamsD :: Bool -> -- True = RHS only
837 IState ->
838 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
839expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)
840 = if n `elem` ns && (not rhsonly)
841 then -- trace (show (n, expandParams dec ps ns ty)) $
842 PTy doc syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
843 else --trace (show (n, expandParams dec ps ns ty)) $
844 PTy doc syn fc o n (expandParams dec ps ns [] ty)
845expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
846 = if n `elem` ns && (not rhsonly)
847 then -- trace (show (n, expandParams dec ps ns ty)) $
848 PPostulate doc syn fc o (dec n) (piBind ps
849 (expandParams dec ps ns [] ty))
850 else --trace (show (n, expandParams dec ps ns ty)) $
851 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
852expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
853 = let n' = if n `elem` ns then dec n else n in
854 PClauses fc opts n' (map expandParamsC cs)
855 where
856 expandParamsC (PClause fc n lhs ws rhs ds)
857 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
858 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
859 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
860 n' = if n `elem` ns then dec n else n
861 -- names bound on the lhs should not be expanded on the rhs
862 ns' = removeBound lhs ns in
863 PClause fc n' lhs'
864 (map (expandParams dec ps'' ns' []) ws)
865 (expandParams dec ps'' ns' [] rhs)
866 (map (expandParamsD True ist dec ps'' ns') ds)
867 expandParamsC (PWith fc n lhs ws wval ds)
868 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
869 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
870 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
871 n' = if n `elem` ns then dec n else n
872 ns' = removeBound lhs ns in
873 PWith fc n' lhs'
874 (map (expandParams dec ps'' ns' []) ws)
875 (expandParams dec ps'' ns' [] wval)
876 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
877 updateps yn nm [] = []
878 updateps yn nm (((a, t), i):as)
879 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
880 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
882 removeBound lhs ns = ns \\ nub (bnames lhs)
884 bnames (PRef _ n) = [n]
885 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
886 bnames (PPair _ l r) = bnames l ++ bnames r
887 bnames (PDPair _ l Placeholder r) = bnames l ++ bnames r
888 bnames _ = []
890expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
891 = PData doc syn fc co (expandPData pd)
892 where
893 -- just do the type decl, leave constructors alone (parameters will be
894 -- added implicitly)
895 expandPData (PDatadecl n ty cons)
896 = if n `elem` ns
897 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
898 (map econ cons)
899 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
900 econ (doc, n, t, fc)
901 = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc)
902expandParamsD rhs ist dec ps ns (PParams f params pds)
903 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
904 (map (expandParamsD True ist dec ps ns) pds)
905-- (map (expandParamsD ist dec ps ns) pds)
906expandParamsD rhs ist dec ps ns (PMutual f pds)
907 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
908expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
909 = PClass doc info f
910 (map (expandParams dec ps ns []) cs)
911 n
912 (map (mapsnd (expandParams dec ps ns [])) params)
913 (map (expandParamsD rhs ist dec ps ns) decls)
914expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
915 = PInstance info f
916 (map (expandParams dec ps ns []) cs)
917 n
918 (map (expandParams dec ps ns []) params)
919 (expandParams dec ps ns [] ty)
920 cn
921 (map (expandParamsD rhs ist dec ps ns) decls)
922expandParamsD rhs ist dec ps ns d = d
924mapsnd f (x, t) = (x, f t)
926-- Calculate a priority for a type, for deciding elaboration order
927-- * if it's just a type variable or concrete type, do it early (0)
928-- * if there's only type variables and injective constructors, do it next (1)
929-- * if there's a function type, next (2)
930-- * finally, everything else (3)
932getPriority :: IState -> PTerm -> Int
933getPriority i tm = 1 -- pri tm
934 where
935 pri (PRef _ n) =
936 case lookupP n (tt_ctxt i) of
937 ((P (DCon _ _) _ _):_) -> 1
938 ((P (TCon _ _) _ _):_) -> 1
939 ((P Ref _ _):_) -> 1
940 [] -> 0 -- must be locally bound, if it's not an error...
941 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
942 pri (PTrue _) = 0
943 pri (PFalse _) = 0
944 pri (PRefl _ _) = 1
945 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
946 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
947 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
948 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
949 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
950 pri (PTyped l r) = pri l
951 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
952 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
953 pri (PAlternative a as) = maximum (map pri as)
954 pri (PConstant _) = 0
955 pri Placeholder = 1
956 pri _ = 3
958addStatics :: Name -> Term -> PTerm -> Idris ()
959addStatics n tm ptm =
960 do let (statics, dynamics) = initStatics tm ptm
961 let stnames = nub $ concatMap freeArgNames (map snd statics)
962 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
963 -- also get the arguments which are 'uniquely inferrable' from
964 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
965 let statics' = nub $ map fst statics ++
966 filter (\x -> not (elem x dnames)) stnames
967 let stpos = staticList statics' tm
968 i <- getIState
969 when (not (null statics)) $
970 logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics
971 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
972 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
973 addIBC (IBCStatic n)
974 where
975 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
976 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
977 if pstatic p == Static then ((n, ty) : static, dynamic)
978 else if (not (searchArg p))
979 then (static, (n, ty) : dynamic)
980 else (static, dynamic)
981 initStatics t pt = ([], [])
983 freeArgNames (Bind n (Pi ty) sc)
984 = nub $ freeArgNames ty
985 freeArgNames tm = let (_, args) = unApply tm in
986 concatMap freeNames args
988 -- if a name appears in a type class or tactic implicit index, it doesn't
989 -- affect its 'uniquely inferrable' from a static status since these are
990 -- resolved by searching.
991 searchArg (Constraint _ _ _) = True
992 searchArg (TacImp _ _ _ _) = True
993 searchArg _ = False
995 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
996 staticList _ _ = []
998-- Dealing with implicit arguments
1000-- Add constraint bindings from using block
1002addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1003addUsingConstraints syn fc t
1004 = do ist <- get
1005 let ns = namesIn [] ist t
1006 let cs = getConstraints t -- check declared constraints
1007 let addconsts = uconsts \\ cs
1008 -- if all names in the arguments of addconsts appear in ns,
1009 -- add the constraint implicitly
1010 return (doAdd addconsts ns t)
1011 where uconsts = filter uconst (using syn)
1012 uconst (UConstraint _ _) = True
1013 uconst _ = False
1015 doAdd [] _ t = t
1016 -- if all of args in ns, then add it
1017 doAdd (UConstraint c args : cs) ns t
1018 | all (\n -> elem n ns) args
1019 = PPi (Constraint False Dynamic "") (MN 0 "cu")
1020 (mkConst c args) (doAdd cs ns t)
1021 | otherwise = doAdd cs ns t
1023 mkConst c args = PApp fc (PRef fc c)
1024 (map (\n -> PExp 0 False (PRef fc n) "") args)
1026 getConstraints (PPi (Constraint _ _ _) _ c sc)
1027 = getcapp c ++ getConstraints sc
1028 getConstraints (PPi _ _ c sc) = getConstraints sc
1029 getConstraints _ = []
1031 getcapp (PApp _ (PRef _ c) args)
1032 = do ns <- mapM getName args
1033 return (UConstraint c ns)
1034 getcapp _ = []
1036 getName (PExp _ _ (PRef _ n) _) = return n
1037 getName _ = []
1039-- Add implicit Pi bindings for any names in the term which appear in an
1040-- argument position.
1042-- This has become a right mess already. Better redo it some time...
1044implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
1045implicit syn n ptm = implicit' syn [] n ptm
1047implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1048implicit' syn ignore n ptm
1049 = do i <- getIState
1050 let (tm', impdata) = implicitise syn ignore i ptm
1051-- let (tm'', spos) = findStatics i tm'
1052 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1053 addIBC (IBCImp n)
1054 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1055-- i <- get
1056-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1057 return tm'
1059implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1060implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1061 let (declimps, ns') = execState (imps True [] tm) ([], [])
1062 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1063 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1064 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1065 if null ns
1066 then (tm, reverse declimps)
1067 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1068 where
1069 uvars = map ipair (filter uimplicit (using syn))
1070 pvars = syn_params syn
1072 inUsing n = n `elem` map fst uvars
1074 ipair (UImplicit x y) = (x, y)
1075 uimplicit (UImplicit _ _) = True
1076 uimplicit _ = False
1078 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1079 | otherwise = x : dropAll xs ys
1080 dropAll [] ys = []
1082 imps top env (PApp _ f as)
1083 = do (decls, ns) <- get
1084 let isn = concatMap (namesIn uvars ist) (map getTm as)
1085 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1086 imps top env (PPi (Imp l _ doc _) n ty sc)
1087 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1088 (decls , ns) <- get
1089 put (PImp (getPriority ist ty) True l n Placeholder doc : decls,
1090 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1091 imps True (n:env) sc
1092 imps top env (PPi (Exp l _ doc _) n ty sc)
1093 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1094 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1095 _ -> [])
1096 (decls, ns) <- get -- ignore decls in HO types
1097 put (PExp (getPriority ist ty) l Placeholder doc : decls,
1098 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1099 imps True (n:env) sc
1100 imps top env (PPi (Constraint l _ doc) n ty sc)
1101 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1102 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1103 _ -> [])
1104 (decls, ns) <- get -- ignore decls in HO types
1105 put (PConstraint 10 l Placeholder doc : decls,
1106 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1107 imps True (n:env) sc
1108 imps top env (PPi (TacImp l _ scr doc) n ty sc)
1109 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1110 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1111 _ -> [])
1112 (decls, ns) <- get -- ignore decls in HO types
1113 put (PTacImplicit 10 l n scr Placeholder doc : decls,
1114 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1115 imps True (n:env) sc
1116 imps top env (PEq _ l r)
1117 = do (decls, ns) <- get
1118 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1119 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1120 imps top env (PRewrite _ l r _)
1121 = do (decls, ns) <- get
1122 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1123 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1124 imps top env (PTyped l r)
1125 = imps top env l
1126 imps top env (PPair _ l r)
1127 = do (decls, ns) <- get
1128 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1129 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1130 imps top env (PDPair _ (PRef _ n) t r)
1131 = do (decls, ns) <- get
1132 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1133 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1134 imps top env (PDPair _ l t r)
1135 = do (decls, ns) <- get
1136 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1137 namesIn uvars ist r
1138 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1139 imps top env (PAlternative a as)
1140 = do (decls, ns) <- get
1141 let isn = concatMap (namesIn uvars ist) as
1142 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1143 imps top env (PLam n ty sc)
1144 = do imps False env ty
1145 imps False (n:env) sc
1146 imps top env (PHidden tm) = imps False env tm
1147 imps top env (PUnifyLog tm) = imps False env tm
1148 imps top env (PNoImplicits tm) = imps False env tm
1149 imps top env _ = return ()
1151 pibind using [] sc = sc
1152 pibind using (n:ns) sc
1153 = case lookup n using of
1154 Just ty -> PPi (Imp False Dynamic "" False) n ty (pibind using ns sc)
1155 Nothing -> PPi (Imp False Dynamic "" False) n Placeholder
1156 (pibind using ns sc)
1158-- Add implicit arguments in function calls
1159addImplPat :: IState -> PTerm -> PTerm
1160addImplPat = addImpl' True [] []
1162addImplBound :: IState -> [Name] -> PTerm -> PTerm
1163addImplBound ist ns = addImpl' False ns [] ist
1165addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1166addImplBoundInf ist ns inf = addImpl' False ns inf ist
1168addImpl :: IState -> PTerm -> PTerm
1169addImpl = addImpl' False [] []
1171-- TODO: in patterns, don't add implicits to function names guarded by constructors
1172-- and *not* inside a PHidden
1174addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1175addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm
1176 where
1177 ai env (PRef fc f)
1178 | f `elem` infns = PInferRef fc f
1179 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f []
1180 ai env (PHidden (PRef fc f))
1181 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f []
1182 ai env (PEq fc l r) = let l' = ai env l
1183 r' = ai env r in
1184 PEq fc l' r'
1185 ai env (PRewrite fc l r g) = let l' = ai env l
1186 r' = ai env r
1187 g' = fmap (ai env) g in
1188 PRewrite fc l' r' g'
1189 ai env (PTyped l r) = let l' = ai env l
1190 r' = ai env r in
1191 PTyped l' r'
1192 ai env (PPair fc l r) = let l' = ai env l
1193 r' = ai env r in
1194 PPair fc l' r'
1195 ai env (PDPair fc l t r) = let l' = ai env l
1196 t' = ai env t
1197 r' = ai env r in
1198 PDPair fc l' t' r'
1199 ai env (PAlternative a as) = let as' = map (ai env) as in
1200 PAlternative a as'
1201 ai env (PApp fc (PInferRef _ f) as)
1202 = let as' = map (fmap (ai env)) as in
1203 PApp fc (PInferRef fc f) as'
1204 ai env (PApp fc ftm@(PRef _ f) as)
1205 | f `elem` infns = ai env (PApp fc (PInferRef fc f) as)
1206 | not (f `elem` map fst env)
1207 = let as' = map (fmap (ai env)) as in
1208 handleErr $ aiFn inpat False ist fc f as'
1209 | Just (Just ty) <- lookup f env
1210 = let as' = map (fmap (ai env)) as
1211 arity = getPArity ty in
1212 mkPApp fc arity ftm as'
1213 ai env (PApp fc f as) = let f' = ai env f
1214 as' = map (fmap (ai env)) as in
1215 mkPApp fc 1 f' as'
1216 ai env (PCase fc c os) = let c' = ai env c
1217 os' = map (pmap (ai env)) os in
1218 PCase fc c' os'
1219 ai env (PLam n ty sc) = let ty' = ai env ty
1220 sc' = ai ((n, Just ty):env) sc in
1221 PLam n ty' sc'
1222 ai env (PLet n ty val sc)
1223 = let ty' = ai env ty
1224 val' = ai env val
1225 sc' = ai ((n, Just ty):env) sc in
1226 PLet n ty' val' sc'
1227 ai env (PPi p n ty sc) = let ty' = ai env ty
1228 sc' = ai ((n, Just ty):env) sc in
1229 PPi p n ty' sc'
1230 ai env (PGoal fc r n sc) = let r' = ai env r
1231 sc' = ai ((n, Nothing):env) sc in
1232 PGoal fc r' n sc'
1233 ai env (PHidden tm) = PHidden (ai env tm)
1234 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
1235 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
1236 ai env (PRefl fc tm) = PRefl fc (ai env tm)
1237 ai env (PUnifyLog tm) = PUnifyLog (ai env tm)
1238 ai env (PNoImplicits tm) = PNoImplicits (ai env tm)
1239 ai env tm = tm
1241 handleErr (Left err) = PElabError err
1242 handleErr (Right x) = x
1244-- if in a pattern, and there are no arguments, and there's no possible
1245-- names with zero explicit arguments, don't add implicits.
1247aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
1248aiFn inpat True ist fc f []
1249 = case lookupDef f (tt_ctxt ist) of
1250 [] -> Right $ PPatvar fc f
1251 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1252 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1253 if (not (vname f) || tcname f
1254 || any (conCaf (tt_ctxt ist)) ialts)
1255-- any constructor alts || any allImp ialts))
1256 then aiFn inpat False ist fc f [] -- use it as a constructor
1257 else Right $ PPatvar fc f
1258 where imp (PExp _ _ _ _) = False
1259 imp _ = True
1260-- allImp [] = False
1261 allImp xs = all imp xs
1262 constructor (TyDecl (DCon _ _) _) = True
1263 constructor _ = False
1265 conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
1267 vname (UN n) = True -- non qualified
1268 vname _ = False
1270aiFn inpat expat ist fc f as
1271 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1272aiFn inpat expat ist fc f as
1273 -- This is where namespaces get resolved by adding PAlternative
1274 = do let ns = lookupCtxtName f (idris_implicits ist)
1275 let ns' = filter (\(n, _) -> notHidden n) ns
1276 case ns' of
1277 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1278 [] -> if f `elem` (map fst (idris_metavars ist))
1279 then Right $ PApp fc (PRef fc f) as
1280 else Right $ mkPApp fc (length as) (PRef fc f) as
1281 alts -> Right $
1282 PAlternative True $
1283 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1284 (insertImpl ns as)) alts
1285 where
1286 notHidden n = case getAccessibility n of
1287 Hidden -> False
1288 _ -> True
1290 getAccessibility n
1291 = case lookupDefAcc n False (tt_ctxt ist) of
1292 [(n,t)] -> t
1293 _ -> Public
1296 insertImpl :: [PArg] -> [PArg] -> [PArg]
1297 insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =
1298 PExp p l tm d : insertImpl ps given
1299 insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =
1300 PConstraint p l tm d : insertImpl ps given
1301 insertImpl (PConstraint p l ty d : ps) given =
1302 PConstraint p l (PResolveTC fc) d : insertImpl ps given
1303 insertImpl (PImp p _ l n ty d : ps) given =
1304 case find n given [] of
1305 Just (tm, given') -> PImp p False l n tm "" : insertImpl ps given'
1306 Nothing -> PImp p True l n Placeholder "" : insertImpl ps given
1307 insertImpl (PTacImplicit p l n sc ty d : ps) given =
1308 case find n given [] of
1309 Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'
1310 Nothing -> if inpat
1311 then PTacImplicit p l n sc Placeholder "" : insertImpl ps given
1312 else PTacImplicit p l n sc sc "" : insertImpl ps given
1313 insertImpl expected [] = []
1314 insertImpl _ given = given
1316 find n [] acc = Nothing
1317 find n (PImp _ _ _ n' t _ : gs) acc
1318 | n == n' = Just (t, reverse acc ++ gs)
1319 find n (PTacImplicit _ _ n' _ t _ : gs) acc
1320 | n == n' = Just (t, reverse acc ++ gs)
1321 find n (g : gs) acc = find n gs (g : acc)
1323-- replace non-linear occurrences with _
1324-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1325-- it is hard to get right!
1327stripLinear :: IState -> PTerm -> PTerm
1328stripLinear i tm = evalState (sl tm) [] where
1329 sl :: PTerm -> State [Name] PTerm
1330 sl (PRef fc f)
1331 | (_:_) <- lookupTy f (tt_ctxt i)
1332 = return $ PRef fc f
1333 | otherwise = do ns <- get
1334 if (f `elem` ns)
1335 then return Placeholder
1336 else do put (f : ns)
1337 return (PRef fc f)
1338 sl (PPatvar fc f)
1339 = do ns <- get
1340 if (f `elem` ns)
1341 then return Placeholder
1342 else do put (f : ns)
1343 return (PPatvar fc f)
1344 sl (PApp fc fn args) = do fn' <- sl fn
1345 args' <- mapM slA args
1346 return $ PApp fc fn' args'
1347 where slA (PImp p m l n t d) = do t' <- sl t
1348 return $ PImp p m l n t' d
1349 slA (PExp p l t d) = do t' <- sl t
1350 return $ PExp p l t' d
1351 slA (PConstraint p l t d)
1352 = do t' <- sl t
1353 return $ PConstraint p l t' d
1354 slA (PTacImplicit p l n sc t d)
1355 = do t' <- sl t
1356 return $ PTacImplicit p l n sc t' d
1357 sl x = return x
1359-- Remove functions which aren't applied to anything, which must then
1360-- be resolved by unification. Assume names resolved and alternatives
1361-- filled in (so no ambiguity).
1363stripUnmatchable :: IState -> PTerm -> PTerm
1364stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1365 su :: PTerm -> PTerm
1366 su (PRef fc f)
1367 | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1368 = Placeholder
1369 su (PApp fc fn args)
1370 = PApp fc fn (fmap (fmap su) args)
1371 su (PAlternative b alts)
1372 = let alts' = filter (/= Placeholder) (map su alts) in
1373 if null alts' then Placeholder
1374 else PAlternative b alts'
1375 su (PPair fc l r) = PPair fc (su l) (su r)
1376 su (PDPair fc l t r) = PDPair fc (su l) (su t) (su r)
1377 su t = t
1378stripUnmatchable i tm = tm
1380mkPApp fc a f [] = f
1381mkPApp fc a f as = let rest = drop a as in
1382 appRest fc (PApp fc f (take a as)) rest
1383 where
1384 appRest fc f [] = f
1385 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1387-- Find 'static' argument positions
1388-- (the declared ones, plus any names in argument position in the declared
1389-- statics)
1390-- FIXME: It's possible that this really has to happen after elaboration
1392findStatics :: IState -> PTerm -> (PTerm, [Bool])
1393findStatics ist tm = trace (showImp Nothing True False tm) $
1394 let (ns, ss) = fs tm in
1395 runState (pos ns ss tm) []
1396 where fs (PPi p n t sc)
1397 | Static <- pstatic p
1398 = let (ns, ss) = fs sc in
1399 (namesIn [] ist t : ns, n : ss)
1400 | otherwise = let (ns, ss) = fs sc in
1401 (ns, ss)
1402 fs _ = ([], [])
1404 inOne n ns = length (filter id (map (elem n) ns)) == 1
1406 pos ns ss (PPi p n t sc)
1407 | elem n ss = do sc' <- pos ns ss sc
1408 spos <- get
1409 put (True : spos)
1410 return (PPi (p { pstatic = Static }) n t sc')
1411 | otherwise = do sc' <- pos ns ss sc
1412 spos <- get
1413 put (False : spos)
1414 return (PPi p n t sc')
1415 pos ns ss t = return t
1417-- for 6.12/7 compatibility
1418data EitherErr a b = LeftErr a | RightOK b
1420instance Monad (EitherErr a) where
1421 return = RightOK
1423 (LeftErr e) >>= k = LeftErr e
1424 RightOK v >>= k = k v
1426toEither (LeftErr e) = Left e
1427toEither (RightOK ho) = Right ho
1429-- syntactic match of a against b, returning pair of variables in a
1430-- and what they match. Returns the pair that failed if not a match.
1432matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1433matchClause = matchClause' False
1435matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1436matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1437 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1439 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1440 fullApp x = x
1442 match' x y = match (fullApp x) (fullApp y)
1443 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
1444 | PConstant (I _) <- getTm x = match (getTm x) x'
1445 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
1446 | PConstant (I _) <- getTm x = match (getTm x) x'
1447 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
1448 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
1449 match (PApp _ f args) (PApp _ f' args')
1450 | length args == length args'
1451 = do mf <- match' f f'
1452 ms <- zipWithM matchArg args args'
1453 return (mf ++ concat ms)
1454-- match (PRef _ n) (PRef _ n') | n == n' = return []
1455-- | otherwise = Nothing
1456 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1457 match (PPatvar f n) xr = match (PRef f n) xr
1458 match xr (PPatvar f n) = match xr (PRef f n)
1459 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1460 match (PRef _ n) tm@(PRef _ n')
1461 | n == n' && not names &&
1462 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1463 || tm == Placeholder)
1464 = return [(n, tm)]
1465 | n == n' = return []
1466 match (PRef _ n) tm
1467 | not names && (not (isConName n (tt_ctxt i) ||
1468 isFnName n (tt_ctxt i)) || tm == Placeholder)
1469 = return [(n, tm)]
1470 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1471 mr <- match' r r'
1472 return (ml ++ mr)
1473 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1474 = do ml <- match' l l'
1475 mr <- match' r r'
1476 return (ml ++ mr)
1477 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1478 mr <- match r r'
1479 return (ml ++ mr)
1480 match (PTyped l r) x = match l x
1481 match x (PTyped l r) = match x l
1482 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1483 mr <- match' r r'
1484 return (ml ++ mr)
1485 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1486 mt <- match' t t'
1487 mr <- match' r r'
1488 return (ml ++ mt ++ mr)
1489 match (PAlternative a as) (PAlternative a' as')
1490 = do ms <- zipWithM match' as as'
1491 return (concat ms)
1492 match a@(PAlternative _ as) b
1493 = do let ms = zipWith match' as (repeat b)
1494 case (rights (map toEither ms)) of
1495 (x: _) -> return x
1496 _ -> LeftErr (a, b)
1497 match (PCase _ _ _) _ = return [] -- lifted out
1498 match (PMetavar _) _ = return [] -- modified
1499 match (PInferRef _ _) _ = return [] -- modified
1500 match (PQuote _) _ = return []
1501 match (PProof _) _ = return []
1502 match (PTactics _) _ = return []
1503 match (PRefl _ _) (PRefl _ _) = return []
1504 match (PResolveTC _) (PResolveTC _) = return []
1505 match (PTrue _) (PTrue _) = return []
1506 match (PFalse _) (PFalse _) = return []
1507 match (PReturn _) (PReturn _) = return []
1508 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1509 ms <- match' s s'
1510 return (mt ++ ms)
1511 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1512 ms <- match' s s'
1513 return (mt ++ ms)
1514 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1515 mty <- match' ty ty'
1516 ms <- match' s s'
1517 return (mt ++ mty ++ ms)
1518 match (PHidden x) (PHidden y) = match' x y
1519 match (PUnifyLog x) y = match' x y
1520 match x (PUnifyLog y) = match' x y
1521 match (PNoImplicits x) y = match' x y
1522 match x (PNoImplicits y) = match' x y
1523 match Placeholder _ = return []
1524 match _ Placeholder = return []
1525 match (PResolveTC _) _ = return []
1526 match a b | a == b = return []
1527 | otherwise = LeftErr (a, b)
1529 checkRpts (RightOK ms) = check ms where
1530 check ((n,t):xs)
1531 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1532 then Left (t, t')
1533 else check xs
1534 check (_:xs) = check xs
1535 check [] = Right ms
1536 checkRpts (LeftErr x) = Left x
1538substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1539substMatches ms = substMatchesShadow ms []
1541substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1542substMatchesShadow [] shs t = t
1543substMatchesShadow ((n,tm):ns) shs t
1544 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1546substMatch :: Name -> PTerm -> PTerm -> PTerm
1547substMatch n = substMatchShadow n []
1549substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1550substMatchShadow n shs tm t = sm shs t where
1551 sm xs (PRef _ n') | n == n' = tm
1552 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1553 sm xs (PPi p x t sc)
1554 | x `elem` xs
1555 = let x' = nextName x in
1556 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1557 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1558 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1559 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1560 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1561 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1562 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1563 (fmap (sm xs) tm)
1564 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1565 sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)
1566 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)
1567 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1568 sm xs (PHidden x) = PHidden (sm xs x)
1569 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1570 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1571 sm xs x = x
1573 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1574 fullApp x = x
1576shadow :: Name -> Name -> PTerm -> PTerm
1577shadow n n' t = sm t where
1578 sm (PRef fc x) | n == x = PRef fc n'
1579 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1580 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1581 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1582 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1583 sm (PEq f x y) = PEq f (sm x) (sm y)
1584 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1585 sm (PTyped x y) = PTyped (sm x) (sm y)
1586 sm (PPair f x y) = PPair f (sm x) (sm y)
1587 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1588 sm (PAlternative a as) = PAlternative a (map sm as)
1589 sm (PHidden x) = PHidden (sm x)
1590 sm (PUnifyLog x) = PUnifyLog (sm x)
1591 sm (PNoImplicits x) = PNoImplicits (sm x)
1592 sm x = x