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