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