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