git.iko.soy/Idris-dev
on 725587f help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1543 lines 64 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] }
99clear_totcheck :: Idris ()
100clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
102setFlags :: Name -> [FnOpt] -> Idris ()
103setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
105setAccessibility :: Name -> Accessibility -> Idris ()
106setAccessibility n a
107 = do i <- getIState
108 let ctxt = setAccess n a (tt_ctxt i)
109 putIState $ i { tt_ctxt = ctxt }
111setTotality :: Name -> Totality -> Idris ()
112setTotality n a
113 = do i <- getIState
114 let ctxt = setTotal n a (tt_ctxt i)
115 putIState $ i { tt_ctxt = ctxt }
117getTotality :: Name -> Idris Totality
118getTotality n
119 = do i <- getIState
120 case lookupTotal n (tt_ctxt i) of
121 [t] -> return t
122 _ -> return (Total [])
124-- Get coercions which might return the required type
125getCoercionsTo :: IState -> Type -> [Name]
126getCoercionsTo i ty =
127 let cs = idris_coercions i
128 (fn,_) = unApply (getRetTy ty) in
129 findCoercions fn cs
130 where findCoercions t [] = []
131 findCoercions t (n : ns) =
132 let ps = case lookupTy n (tt_ctxt i) of
133 [ty] -> case unApply (getRetTy ty) of
134 (t', _) ->
135 if t == t' then [n] else []
136 _ -> [] in
137 ps ++ findCoercions t ns
139addToCG :: Name -> CGInfo -> Idris ()
140addToCG n cg
141 = do i <- getIState
142 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
144addCoercion :: Name -> Idris ()
145addCoercion n = do i <- getIState
146 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
148addDocStr :: Name -> String -> Idris ()
149addDocStr n doc
150 = do i <- getIState
151 putIState $ i { idris_docstrings = addDef n doc (idris_docstrings i) }
153addToCalledG :: Name -> [Name] -> Idris ()
154addToCalledG n ns = return () -- TODO
156-- Add a class instance function. Dodgy hack: Put integer instances first in the
157-- list so they are resolved by default.
158-- Dodgy hack 2: put constraint chasers (@@) last
160addInstance :: Bool -> Name -> Name -> Idris ()
161addInstance int n i
162 = do ist <- getIState
163 case lookupCtxt n (idris_classes ist) of
164 [CI a b c d ins] ->
165 do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)
166 putIState $ ist { idris_classes = cs }
167 _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)
168 putIState $ ist { idris_classes = cs }
169 where addI i ins | int = i : ins
170 | chaser n = ins ++ [i]
171 | otherwise = insI i ins
172 insI i [] = [i]
173 insI i (n : ns) | chaser n = i : n : ns
174 | otherwise = n : insI i ns
176 chaser (UN ('@':'@':_)) = True
177 chaser (NS n _) = chaser n
178 chaser _ = False
180addClass :: Name -> ClassInfo -> Idris ()
181addClass n i
182 = do ist <- getIState
183 let i' = case lookupCtxt n (idris_classes ist) of
184 [c] -> c { class_instances = class_instances i }
185 _ -> i
186 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
188addIBC :: IBCWrite -> Idris ()
189addIBC ibc@(IBCDef n)
190 = do i <- getIState
191 when (notDef (ibc_write i)) $
192 putIState $ i { ibc_write = ibc : ibc_write i }
193 where notDef [] = True
194 notDef (IBCDef n': is) | n == n' = False
195 notDef (_ : is) = notDef is
196addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
198clearIBC :: Idris ()
199clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
201getHdrs :: Codegen -> Idris [String]
202getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
204setErrLine :: Int -> Idris ()
205setErrLine x = do i <- getIState;
206 case (errLine i) of
207 Nothing -> putIState $ i { errLine = Just x }
208 Just _ -> return ()
210clearErr :: Idris ()
211clearErr = do i <- getIState
212 putIState $ i { errLine = Nothing }
214getSO :: Idris (Maybe String)
215getSO = do i <- getIState
216 return (compiled_so i)
218setSO :: Maybe String -> Idris ()
219setSO s = do i <- getIState
220 putIState $ (i { compiled_so = s })
222getIState :: Idris IState
223getIState = get
225putIState :: IState -> Idris ()
226putIState = put
228-- | A version of liftIO that puts errors into the exception type of the Idris monad
229runIO :: IO a -> Idris a
230runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
231-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
233getName :: Idris Int
234getName = do i <- getIState;
235 let idx = idris_name i;
236 putIState $ (i { idris_name = idx + 1 })
237 return idx
239addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
240addInternalApp fp l t
241 = do i <- getIState
242 putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })
244getInternalApp :: FilePath -> Int -> Idris PTerm
245getInternalApp fp l = do i <- getIState
246 case lookup (fp, l) (idris_lineapps i) of
247 Just n' -> return n'
248 Nothing -> return Placeholder
249 -- TODO: What if it's not there?
251checkUndefined :: FC -> Name -> Idris ()
252checkUndefined fc n
253 = do i <- getContext
254 case lookupTy n i of
255 (_:_) -> fail $ show fc ++ ":" ++
256 show n ++ " already defined"
257 _ -> return ()
259isUndefined :: FC -> Name -> Idris Bool
260isUndefined fc n
261 = do i <- getContext
262 case lookupTy n i of
263 (_:_) -> return False
264 _ -> return True
266setContext :: Context -> Idris ()
267setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
269updateContext :: (Context -> Context) -> Idris ()
270updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
272addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
273addConstraints fc (v, cs)
274 = do i <- getIState
275 let ctxt = tt_ctxt i
276 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
277 next_tvar = v }
278 let ics = zip cs (repeat fc) ++ idris_constraints i
279 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
281addDeferred = addDeferred' Ref
282addDeferredTyCon = addDeferred' (TCon 0 0)
284addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
285addDeferred' nt ns
286 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns
287 i <- getIState
288 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
289 idris_metavars i }
290 where tidyNames used (Bind (MN i x) b sc)
291 = let n' = uniqueName (UN x) used in
292 Bind n' b $ tidyNames (n':used) sc
293 tidyNames used (Bind n b sc)
294 = let n' = uniqueName n used in
295 Bind n' b $ tidyNames (n':used) sc
296 tidyNames used b = b
298solveDeferred :: Name -> Idris ()
299solveDeferred n = do i <- getIState
300 putIState $ i { idris_metavars =
301 filter (\(n', _) -> n/=n')
302 (idris_metavars i) }
304ihPrintResult :: Handle -> String -> Idris ()
305ihPrintResult h s = do i <- getIState
306 case idris_outputmode i of
307 RawOutput -> case s of
308 "" -> return ()
309 s -> runIO $ hPutStrLn h s
310 IdeSlave n ->
311 let good = SexpList [SymbolAtom "ok", toSExp s] in
312 runIO $ hPutStrLn h $ convSExp "return" good n
314ihPrintError :: Handle -> String -> Idris ()
315ihPrintError h s = do i <- getIState
316 case idris_outputmode i of
317 RawOutput -> case s of
318 "" -> return ()
319 s -> runIO $ hPutStrLn h s
320 IdeSlave n ->
321 let good = SexpList [SymbolAtom "error", toSExp s] in
322 runIO . hPutStrLn h $ convSExp "return" good n
324ihputStrLn :: Handle -> String -> Idris ()
325ihputStrLn h s = do i <- getIState
326 case idris_outputmode i of
327 RawOutput -> runIO $ hPutStrLn h s
328 IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n
330iputStrLn = ihputStrLn stdout
331iPrintError = ihPrintError stdout
332iPrintResult = ihPrintResult stdout
333iWarn = ihWarn stdout
335ideslavePutSExp :: SExpable a => String -> a -> Idris ()
336ideslavePutSExp cmd info = do i <- getIState
337 case idris_outputmode i of
338 IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
339 _ -> return ()
341-- this needs some typing magic and more structured output towards emacs
342iputGoal :: String -> Idris ()
343iputGoal s = do i <- getIState
344 case idris_outputmode i of
345 RawOutput -> runIO $ putStrLn s
346 IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" s n
348isetPrompt :: String -> Idris ()
349isetPrompt p = do i <- getIState
350 case idris_outputmode i of
351 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n
353ihWarn :: Handle -> FC -> String -> Idris ()
354ihWarn h fc err = do i <- getIState
355 case idris_outputmode i of
356 RawOutput -> runIO $ hPutStrLn h (show fc ++ ":" ++ err)
357 IdeSlave n -> runIO $ hPutStrLn h $ convSExp "warning" (fc_fname fc, fc_line fc, err) n
359setLogLevel :: Int -> Idris ()
360setLogLevel l = do i <- getIState
361 let opts = idris_options i
362 let opt' = opts { opt_logLevel = l }
363 putIState $ i { idris_options = opt' }
365setCmdLine :: [Opt] -> Idris ()
366setCmdLine opts = do i <- getIState
367 let iopts = idris_options i
368 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
370getCmdLine :: Idris [Opt]
371getCmdLine = do i <- getIState
372 return (opt_cmdline (idris_options i))
374getDumpDefun :: Idris (Maybe FilePath)
375getDumpDefun = do i <- getIState
376 return $ findC (opt_cmdline (idris_options i))
377 where findC [] = Nothing
378 findC (DumpDefun x : _) = Just x
379 findC (_ : xs) = findC xs
381getDumpCases :: Idris (Maybe FilePath)
382getDumpCases = do i <- getIState
383 return $ findC (opt_cmdline (idris_options i))
384 where findC [] = Nothing
385 findC (DumpCases x : _) = Just x
386 findC (_ : xs) = findC xs
388logLevel :: Idris Int
389logLevel = do i <- getIState
390 return (opt_logLevel (idris_options i))
392setErrContext :: Bool -> Idris ()
393setErrContext t = do i <- getIState
394 let opts = idris_options i
395 let opt' = opts { opt_errContext = t }
396 putIState $ i { idris_options = opt' }
398errContext :: Idris Bool
399errContext = do i <- getIState
400 return (opt_errContext (idris_options i))
402useREPL :: Idris Bool
403useREPL = do i <- getIState
404 return (opt_repl (idris_options i))
406setREPL :: Bool -> Idris ()
407setREPL t = do i <- getIState
408 let opts = idris_options i
409 let opt' = opts { opt_repl = t }
410 putIState $ i { idris_options = opt' }
412setQuiet :: Bool -> Idris ()
413setQuiet q = do i <- getIState
414 let opts = idris_options i
415 let opt' = opts { opt_quiet = q }
416 putIState $ i { idris_options = opt' }
418getQuiet :: Idris Bool
419getQuiet = do i <- getIState
420 let opts = idris_options i
421 return (opt_quiet opts)
423setCodegen :: Codegen -> Idris ()
424setCodegen t = do i <- getIState
425 let opts = idris_options i
426 let opt' = opts { opt_codegen = t }
427 putIState $ i { idris_options = opt' }
429codegen :: Idris Codegen
430codegen = do i <- getIState
431 return (opt_codegen (idris_options i))
433setOutputTy :: OutputType -> Idris ()
434setOutputTy t = do i <- getIState
435 let opts = idris_options i
436 let opt' = opts { opt_outputTy = t }
437 putIState $ i { idris_options = opt' }
439outputTy :: Idris OutputType
440outputTy = do i <- getIState
441 return $ opt_outputTy $ idris_options i
443setIdeSlave :: Bool -> Idris ()
444setIdeSlave True = do i <- getIState
445 putIState $ i { idris_outputmode = (IdeSlave 0), idris_colourRepl = False }
446setIdeSlave False = return ()
448setTargetTriple :: String -> Idris ()
449setTargetTriple t = do i <- getIState
450 let opts = idris_options i
451 opt' = opts { opt_triple = t }
452 putIState $ i { idris_options = opt' }
454targetTriple :: Idris String
455targetTriple = do i <- getIState
456 return (opt_triple (idris_options i))
458setTargetCPU :: String -> Idris ()
459setTargetCPU t = do i <- getIState
460 let opts = idris_options i
461 opt' = opts { opt_cpu = t }
462 putIState $ i { idris_options = opt' }
464targetCPU :: Idris String
465targetCPU = do i <- getIState
466 return (opt_cpu (idris_options i))
468setOptLevel :: Word -> Idris ()
469setOptLevel t = do i <- getIState
470 let opts = idris_options i
471 opt' = opts { opt_optLevel = t }
472 putIState $ i { idris_options = opt' }
474optLevel :: Idris Word
475optLevel = do i <- getIState
476 return (opt_optLevel (idris_options i))
478verbose :: Idris Bool
479verbose = do i <- getIState
480 return (opt_verbose (idris_options i))
482setVerbose :: Bool -> Idris ()
483setVerbose t = do i <- getIState
484 let opts = idris_options i
485 let opt' = opts { opt_verbose = t }
486 putIState $ i { idris_options = opt' }
488typeInType :: Idris Bool
489typeInType = do i <- getIState
490 return (opt_typeintype (idris_options i))
492setTypeInType :: Bool -> Idris ()
493setTypeInType t = do i <- getIState
494 let opts = idris_options i
495 let opt' = opts { opt_typeintype = t }
496 putIState $ i { idris_options = opt' }
498coverage :: Idris Bool
499coverage = do i <- getIState
500 return (opt_coverage (idris_options i))
502setCoverage :: Bool -> Idris ()
503setCoverage t = do i <- getIState
504 let opts = idris_options i
505 let opt' = opts { opt_coverage = t }
506 putIState $ i { idris_options = opt' }
508setIBCSubDir :: FilePath -> Idris ()
509setIBCSubDir fp = do i <- getIState
510 let opts = idris_options i
511 let opt' = opts { opt_ibcsubdir = fp }
512 putIState $ i { idris_options = opt' }
514valIBCSubDir :: IState -> Idris FilePath
515valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
517addImportDir :: FilePath -> Idris ()
518addImportDir fp = do i <- getIState
519 let opts = idris_options i
520 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
521 putIState $ i { idris_options = opt' }
523setImportDirs :: [FilePath] -> Idris ()
524setImportDirs fps = do i <- getIState
525 let opts = idris_options i
526 let opt' = opts { opt_importdirs = fps }
527 putIState $ i { idris_options = opt' }
529allImportDirs :: Idris [FilePath]
530allImportDirs = do i <- getIState
531 let optdirs = opt_importdirs (idris_options i)
532 return ("." : reverse optdirs)
534colourise :: Idris Bool
535colourise = do i <- getIState
536 return $ idris_colourRepl i
538setColourise :: Bool -> Idris ()
539setColourise b = do i <- getIState
540 putIState $ i { idris_colourRepl = b }
542setOutH :: Handle -> Idris ()
543setOutH h = do i <- getIState
544 putIState $ i { idris_outh = h }
546impShow :: Idris Bool
547impShow = do i <- getIState
548 return (opt_showimp (idris_options i))
550setImpShow :: Bool -> Idris ()
551setImpShow t = do i <- getIState
552 let opts = idris_options i
553 let opt' = opts { opt_showimp = t }
554 putIState $ i { idris_options = opt' }
556setColour :: ColourType -> IdrisColour -> Idris ()
557setColour ct c = do i <- getIState
558 let newTheme = setColour' ct c (idris_colourTheme i)
559 putIState $ i { idris_colourTheme = newTheme }
560 where setColour' KeywordColour c t = t { keywordColour = c }
561 setColour' BoundVarColour c t = t { boundVarColour = c }
562 setColour' ImplicitColour c t = t { implicitColour = c }
563 setColour' FunctionColour c t = t { functionColour = c }
564 setColour' TypeColour c t = t { typeColour = c }
565 setColour' DataColour c t = t { dataColour = c }
566 setColour' PromptColour c t = t { promptColour = c }
568logLvl :: Int -> String -> Idris ()
569logLvl l str = do i <- getIState
570 let lvl = opt_logLevel (idris_options i)
571 when (lvl >= l) $
572 case idris_outputmode i of
573 RawOutput -> do runIO $ putStrLn str
574 IdeSlave n ->
575 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
576 runIO $ putStrLn $ convSExp "log" good n
578cmdOptType :: Opt -> Idris Bool
579cmdOptType x = do i <- getIState
580 return $ x `elem` opt_cmdline (idris_options i)
582iLOG :: String -> Idris ()
583iLOG = logLvl 1
585noErrors :: Idris Bool
586noErrors = do i <- getIState
587 case errLine i of
588 Nothing -> return True
589 _ -> return False
591setTypeCase :: Bool -> Idris ()
592setTypeCase t = do i <- getIState
593 let opts = idris_options i
594 let opt' = opts { opt_typecase = t }
595 putIState $ i { idris_options = opt' }
598-- For inferring types of things
600bi = fileFC "builtin"
602inferTy = MN 0 "__Infer"
603inferCon = MN 0 "__infer"
604inferDecl = PDatadecl inferTy
605 PType
606 [("", inferCon, PPi impl (MN 0 "A") PType (
607 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
608 (PRef bi inferTy)), bi)]
609inferOpts = []
611infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder True, pexp t]
612infP = P (TCon 6 0) inferTy (TType (UVal 0))
614getInferTerm, getInferType :: Term -> Term
615getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
616getInferTerm (App (App _ _) tm) = tm
617getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
619getInferType (Bind n b sc) = Bind n b $ getInferType sc
620getInferType (App (App _ ty) _) = ty
622-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class
624primNames = [unitTy, unitCon,
625 falseTy, pairTy, pairCon,
626 eqTy, eqCon, inferTy, inferCon]
628unitTy = MN 0 "__Unit"
629unitCon = MN 0 "__II"
630unitDecl = PDatadecl unitTy PType
631 [("", unitCon, PRef bi unitTy, bi)]
632unitOpts = [DefaultEliminator]
634falseTy = MN 0 "__False"
635falseDecl = PDatadecl falseTy PType []
636falseOpts = []
638pairTy = MN 0 "__Pair"
639pairCon = MN 0 "__MkPair"
640pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
641 [("", pairCon, PPi impl (n "A") PType (
642 PPi impl (n "B") PType (
643 PPi expl (n "a") (PRef bi (n "A")) (
644 PPi expl (n "b") (PRef bi (n "B"))
645 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
646 pexp (PRef bi (n "B"))])))), bi)]
647 where n a = MN 0 a
648pairOpts = []
650eqTy = UN "="
651eqCon = UN "refl"
652eqDecl = PDatadecl eqTy (piBind [(n "a", PType), (n "b", PType),
653 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
654 PType)
655 [("", eqCon, PPi impl (n "a") PType (
656 PPi impl (n "x") (PRef bi (n "a"))
657 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder False,
658 pimp (n "b") Placeholder False,
659 pexp (PRef bi (n "x")),
660 pexp (PRef bi (n "x"))])), bi)]
661 where n a = MN 0 a
662eqOpts = []
664elimName = UN "__Elim"
665elimMethElimTy = UN "__elimTy"
666elimMethElim = UN "elim"
667elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(UN "scrutineeType", PType)]
668 [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,
669 PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
671-- Defined in builtins.idr
672sigmaTy = UN "Exists"
673existsCon = UN "Ex_intro"
675piBind :: [(Name, PTerm)] -> PTerm -> PTerm
676piBind = piBindp expl
678piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
679piBindp p [] t = t
680piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
682-- Dealing with parameters
684expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
685 [Name] -> -- all names
686 [Name] -> -- names with no declaration
687 PTerm -> PTerm
688expandParams dec ps ns infs tm = en tm
689 where
690 -- if we shadow a name (say in a lambda binding) that is used in a call to
691 -- a lifted function, we need access to both names - once in the scope of the
692 -- binding and once to call the lifted functions. So we'll explicitly shadow
693 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
694 -- but we didn't...)
696 mkShadow (UN n) = MN 0 n
697 mkShadow (MN i n) = MN (i+1) n
698 mkShadow (NS x s) = NS (mkShadow x) s
700 en (PLam n t s)
701 | n `elem` (map fst ps ++ ns)
702 = let n' = mkShadow n in
703 PLam n' (en t) (en (shadow n n' s))
704 | otherwise = PLam n (en t) (en s)
705 en (PPi p n t s)
706 | n `elem` (map fst ps ++ ns)
707 = let n' = mkShadow n in
708 PPi p n' (en t) (en (shadow n n' s))
709 | otherwise = PPi p n (en t) (en s)
710 en (PLet n ty v s)
711 | n `elem` (map fst ps ++ ns)
712 = let n' = mkShadow n in
713 PLet n' (en ty) (en v) (en (shadow n n' s))
714 | otherwise = PLet n (en ty) (en v) (en s)
715 -- FIXME: Should only do this in a type signature!
716 en (PDPair f (PRef f' n) t r)
717 | n `elem` (map fst ps ++ ns) && t /= Placeholder
718 = let n' = mkShadow n in
719 PDPair f (PRef f' n') (en t) (en (shadow n n' r))
720 en (PEq f l r) = PEq f (en l) (en r)
721 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
722 en (PTyped l r) = PTyped (en l) (en r)
723 en (PPair f l r) = PPair f (en l) (en r)
724 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
725 en (PAlternative a as) = PAlternative a (map en as)
726 en (PHidden t) = PHidden (en t)
727 en (PUnifyLog t) = PUnifyLog (en t)
728 en (PNoImplicits t) = PNoImplicits (en t)
729 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
730 en (PProof ts) = PProof (map (fmap en) ts)
731 en (PTactics ts) = PTactics (map (fmap en) ts)
733 en (PQuote (Var n))
734 | n `nselem` ns = PQuote (Var (dec n))
735 en (PApp fc (PInferRef fc' n) as)
736 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
737 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
738 en (PApp fc (PRef fc' n) as)
739 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
740 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
741 | n `nselem` ns = PApp fc (PRef fc' (dec n))
742 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
743 en (PAppBind fc (PRef fc' n) as)
744 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
745 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
746 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
747 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
748 en (PRef fc n)
749 | n `elem` infs = PApp fc (PInferRef fc (dec n))
750 (map (pexp . (PRef fc)) (map fst ps))
751 | n `nselem` ns = PApp fc (PRef fc (dec n))
752 (map (pexp . (PRef fc)) (map fst ps))
753 en (PInferRef fc n)
754 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
755 (map (pexp . (PRef fc)) (map fst ps))
756 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
757 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
758 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
759 en t = t
761 nselem x [] = False
762 nselem x (y : xs) | nseq x y = True
763 | otherwise = nselem x xs
765 nseq x y = nsroot x == nsroot y
767expandParamsD :: Bool -> -- True = RHS only
768 IState ->
769 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
770expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)
771 = if n `elem` ns && (not rhsonly)
772 then -- trace (show (n, expandParams dec ps ns ty)) $
773 PTy doc syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
774 else --trace (show (n, expandParams dec ps ns ty)) $
775 PTy doc syn fc o n (expandParams dec ps ns [] ty)
776expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
777 = if n `elem` ns && (not rhsonly)
778 then -- trace (show (n, expandParams dec ps ns ty)) $
779 PPostulate doc syn fc o (dec n) (piBind ps
780 (expandParams dec ps ns [] ty))
781 else --trace (show (n, expandParams dec ps ns ty)) $
782 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
783expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
784 = let n' = if n `elem` ns then dec n else n in
785 PClauses fc opts n' (map expandParamsC cs)
786 where
787 expandParamsC (PClause fc n lhs ws rhs ds)
788 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
789 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
790 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
791 n' = if n `elem` ns then dec n else n
792 -- names bound on the lhs should not be expanded on the rhs
793 ns' = removeBound lhs ns in
794 PClause fc n' lhs'
795 (map (expandParams dec ps'' ns' []) ws)
796 (expandParams dec ps'' ns' [] rhs)
797 (map (expandParamsD True ist dec ps'' ns') ds)
798 expandParamsC (PWith fc n lhs ws wval ds)
799 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
800 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
801 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
802 n' = if n `elem` ns then dec n else n
803 ns' = removeBound lhs ns in
804 PWith fc n' lhs'
805 (map (expandParams dec ps'' ns' []) ws)
806 (expandParams dec ps'' ns' [] wval)
807 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
808 updateps yn nm [] = []
809 updateps yn nm (((a, t), i):as)
810 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
811 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
813 removeBound lhs ns = ns \\ nub (bnames lhs)
815 bnames (PRef _ n) = [n]
816 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
817 bnames (PPair _ l r) = bnames l ++ bnames r
818 bnames (PDPair _ l Placeholder r) = bnames l ++ bnames r
819 bnames _ = []
821expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
822 = PData doc syn fc co (expandPData pd)
823 where
824 -- just do the type decl, leave constructors alone (parameters will be
825 -- added implicitly)
826 expandPData (PDatadecl n ty cons)
827 = if n `elem` ns
828 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
829 (map econ cons)
830 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
831 econ (doc, n, t, fc)
832 = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc)
833expandParamsD rhs ist dec ps ns (PParams f params pds)
834 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
835 (map (expandParamsD True ist dec ps ns) pds)
836-- (map (expandParamsD ist dec ps ns) pds)
837expandParamsD rhs ist dec ps ns (PMutual f pds)
838 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
839expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
840 = PClass doc info f
841 (map (expandParams dec ps ns []) cs)
842 n
843 (map (mapsnd (expandParams dec ps ns [])) params)
844 (map (expandParamsD rhs ist dec ps ns) decls)
845expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
846 = PInstance info f
847 (map (expandParams dec ps ns []) cs)
848 n
849 (map (expandParams dec ps ns []) params)
850 (expandParams dec ps ns [] ty)
851 cn
852 (map (expandParamsD rhs ist dec ps ns) decls)
853expandParamsD rhs ist dec ps ns d = d
855mapsnd f (x, t) = (x, f t)
857-- Calculate a priority for a type, for deciding elaboration order
858-- * if it's just a type variable or concrete type, do it early (0)
859-- * if there's only type variables and injective constructors, do it next (1)
860-- * if there's a function type, next (2)
861-- * finally, everything else (3)
863getPriority :: IState -> PTerm -> Int
864getPriority i tm = 1 -- pri tm
865 where
866 pri (PRef _ n) =
867 case lookupP n (tt_ctxt i) of
868 ((P (DCon _ _) _ _):_) -> 1
869 ((P (TCon _ _) _ _):_) -> 1
870 ((P Ref _ _):_) -> 1
871 [] -> 0 -- must be locally bound, if it's not an error...
872 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
873 pri (PTrue _) = 0
874 pri (PFalse _) = 0
875 pri (PRefl _ _) = 1
876 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
877 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
878 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
879 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
880 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
881 pri (PTyped l r) = pri l
882 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
883 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
884 pri (PAlternative a as) = maximum (map pri as)
885 pri (PConstant _) = 0
886 pri Placeholder = 1
887 pri _ = 3
889addStatics :: Name -> Term -> PTerm -> Idris ()
890addStatics n tm ptm =
891 do let (statics, dynamics) = initStatics tm ptm
892 let stnames = nub $ concatMap freeArgNames (map snd statics)
893 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
894 when (not (null statics)) $
895 logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics
896 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
897 -- also get the arguments which are 'uniquely inferrable' from
898 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
899 let statics' = nub $ map fst statics ++
900 filter (\x -> not (elem x dnames)) stnames
901 let stpos = staticList statics' tm
902 i <- getIState
903 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
904 addIBC (IBCStatic n)
905 where
906 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
907 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
908 if pstatic p == Static then ((n, ty) : static, dynamic)
909 else if (not (searchArg p))
910 then (static, (n, ty) : dynamic)
911 else (static, dynamic)
912 initStatics t pt = ([], [])
914 freeArgNames tm = let (_, args) = unApply tm in
915 concatMap freeNames args
917 -- if a name appears in a type class or tactic implicit index, it doesn't
918 -- affect its 'uniquely inferrable' from a static status since these are
919 -- resolved by searching.
920 searchArg (Constraint _ _ _) = True
921 searchArg (TacImp _ _ _ _) = True
922 searchArg _ = False
924 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
925 staticList _ _ = []
927-- Dealing with implicit arguments
929-- Add constraint bindings from using block
931addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
932addUsingConstraints syn fc t
933 = do ist <- get
934 let ns = namesIn [] ist t
935 let cs = getConstraints t -- check declared constraints
936 let addconsts = uconsts \\ cs
937 -- if all names in the arguments of addconsts appear in ns,
938 -- add the constraint implicitly
939 return (doAdd addconsts ns t)
940 where uconsts = filter uconst (using syn)
941 uconst (UConstraint _ _) = True
942 uconst _ = False
944 doAdd [] _ t = t
945 -- if all of args in ns, then add it
946 doAdd (UConstraint c args : cs) ns t
947 | all (\n -> elem n ns) args
948 = PPi (Constraint False Dynamic "") (MN 0 "cu")
949 (mkConst c args) (doAdd cs ns t)
950 | otherwise = doAdd cs ns t
952 mkConst c args = PApp fc (PRef fc c)
953 (map (\n -> PExp 0 False (PRef fc n) "") args)
955 getConstraints (PPi (Constraint _ _ _) _ c sc)
956 = getcapp c ++ getConstraints sc
957 getConstraints (PPi _ _ c sc) = getConstraints sc
958 getConstraints _ = []
960 getcapp (PApp _ (PRef _ c) args)
961 = do ns <- mapM getName args
962 return (UConstraint c ns)
963 getcapp _ = []
965 getName (PExp _ _ (PRef _ n) _) = return n
966 getName _ = []
968-- Add implicit Pi bindings for any names in the term which appear in an
969-- argument position.
971-- This has become a right mess already. Better redo it some time...
973implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
974implicit syn n ptm = implicit' syn [] n ptm
976implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
977implicit' syn ignore n ptm
978 = do i <- getIState
979 let (tm', impdata) = implicitise syn ignore i ptm
980-- let (tm'', spos) = findStatics i tm'
981 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
982 addIBC (IBCImp n)
983 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
984-- i <- get
985-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
986 return tm'
988implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
989implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
990 let (declimps, ns') = execState (imps True [] tm) ([], [])
991 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
992 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
993 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
994 if null ns
995 then (tm, reverse declimps)
996 else implicitise syn ignore ist (pibind uvars nsOrder tm)
997 where
998 uvars = map ipair (filter uimplicit (using syn))
999 pvars = syn_params syn
1001 inUsing n = n `elem` map fst uvars
1003 ipair (UImplicit x y) = (x, y)
1004 uimplicit (UImplicit _ _) = True
1005 uimplicit _ = False
1007 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1008 | otherwise = x : dropAll xs ys
1009 dropAll [] ys = []
1011 imps top env (PApp _ f as)
1012 = do (decls, ns) <- get
1013 let isn = concatMap (namesIn uvars ist) (map getTm as)
1014 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1015 imps top env (PPi (Imp l _ doc _) n ty sc)
1016 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1017 (decls , ns) <- get
1018 put (PImp (getPriority ist ty) True l n ty doc : decls,
1019 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1020 imps True (n:env) sc
1021 imps top env (PPi (Exp l _ doc _) n ty sc)
1022 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1023 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1024 _ -> [])
1025 (decls, ns) <- get -- ignore decls in HO types
1026 put (PExp (getPriority ist ty) l ty doc : decls,
1027 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1028 imps True (n:env) sc
1029 imps top env (PPi (Constraint l _ doc) n ty sc)
1030 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1031 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1032 _ -> [])
1033 (decls, ns) <- get -- ignore decls in HO types
1034 put (PConstraint 10 l ty doc : decls,
1035 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1036 imps True (n:env) sc
1037 imps top env (PPi (TacImp l _ scr doc) n ty sc)
1038 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1039 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1040 _ -> [])
1041 (decls, ns) <- get -- ignore decls in HO types
1042 put (PTacImplicit 10 l n scr ty doc : decls,
1043 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1044 imps True (n:env) sc
1045 imps top env (PEq _ l r)
1046 = do (decls, ns) <- get
1047 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1048 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1049 imps top env (PRewrite _ l r _)
1050 = do (decls, ns) <- get
1051 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1052 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1053 imps top env (PTyped l r)
1054 = imps top env l
1055 imps top env (PPair _ l r)
1056 = do (decls, ns) <- get
1057 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1058 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1059 imps top env (PDPair _ (PRef _ n) t r)
1060 = do (decls, ns) <- get
1061 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1062 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1063 imps top env (PDPair _ l t r)
1064 = do (decls, ns) <- get
1065 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1066 namesIn uvars ist r
1067 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1068 imps top env (PAlternative a as)
1069 = do (decls, ns) <- get
1070 let isn = concatMap (namesIn uvars ist) as
1071 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1072 imps top env (PLam n ty sc)
1073 = do imps False env ty
1074 imps False (n:env) sc
1075 imps top env (PHidden tm) = imps False env tm
1076 imps top env (PUnifyLog tm) = imps False env tm
1077 imps top env (PNoImplicits tm) = imps False env tm
1078 imps top env _ = return ()
1080 pibind using [] sc = sc
1081 pibind using (n:ns) sc
1082 = case lookup n using of
1083 Just ty -> PPi (Imp False Dynamic "" False) n ty (pibind using ns sc)
1084 Nothing -> PPi (Imp False Dynamic "" False) n Placeholder
1085 (pibind using ns sc)
1087-- Add implicit arguments in function calls
1088addImplPat :: IState -> PTerm -> PTerm
1089addImplPat = addImpl' True [] []
1091addImplBound :: IState -> [Name] -> PTerm -> PTerm
1092addImplBound ist ns = addImpl' False ns [] ist
1094addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1095addImplBoundInf ist ns inf = addImpl' False ns inf ist
1097addImpl :: IState -> PTerm -> PTerm
1098addImpl = addImpl' False [] []
1100-- TODO: in patterns, don't add implicits to function names guarded by constructors
1101-- and *not* inside a PHidden
1103addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1104addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm
1105 where
1106 ai env (PRef fc f)
1107 | f `elem` infns = PInferRef fc f
1108 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f []
1109 ai env (PHidden (PRef fc f))
1110 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f []
1111 ai env (PEq fc l r) = let l' = ai env l
1112 r' = ai env r in
1113 PEq fc l' r'
1114 ai env (PRewrite fc l r g) = let l' = ai env l
1115 r' = ai env r
1116 g' = fmap (ai env) g in
1117 PRewrite fc l' r' g'
1118 ai env (PTyped l r) = let l' = ai env l
1119 r' = ai env r in
1120 PTyped l' r'
1121 ai env (PPair fc l r) = let l' = ai env l
1122 r' = ai env r in
1123 PPair fc l' r'
1124 ai env (PDPair fc l t r) = let l' = ai env l
1125 t' = ai env t
1126 r' = ai env r in
1127 PDPair fc l' t' r'
1128 ai env (PAlternative a as) = let as' = map (ai env) as in
1129 PAlternative a as'
1130 ai env (PApp fc (PInferRef _ f) as)
1131 = let as' = map (fmap (ai env)) as in
1132 PApp fc (PInferRef fc f) as'
1133 ai env (PApp fc ftm@(PRef _ f) as)
1134 | f `elem` infns = ai env (PApp fc (PInferRef fc f) as)
1135 | not (f `elem` map fst env)
1136 = let as' = map (fmap (ai env)) as in
1137 handleErr $ aiFn inpat False ist fc f as'
1138 | Just (Just ty) <- lookup f env
1139 = let as' = map (fmap (ai env)) as
1140 arity = getPArity ty in
1141 mkPApp fc arity ftm as'
1142 ai env (PApp fc f as) = let f' = ai env f
1143 as' = map (fmap (ai env)) as in
1144 mkPApp fc 1 f' as'
1145 ai env (PCase fc c os) = let c' = ai env c
1146 os' = map (pmap (ai env)) os in
1147 PCase fc c' os'
1148 ai env (PLam n ty sc) = let ty' = ai env ty
1149 sc' = ai ((n, Just ty):env) sc in
1150 PLam n ty' sc'
1151 ai env (PLet n ty val sc)
1152 = let ty' = ai env ty
1153 val' = ai env val
1154 sc' = ai ((n, Just ty):env) sc in
1155 PLet n ty' val' sc'
1156 ai env (PPi p n ty sc) = let ty' = ai env ty
1157 sc' = ai ((n, Just ty):env) sc in
1158 PPi p n ty' sc'
1159 ai env (PGoal fc r n sc) = let r' = ai env r
1160 sc' = ai ((n, Nothing):env) sc in
1161 PGoal fc r' n sc'
1162 ai env (PHidden tm) = PHidden (ai env tm)
1163 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
1164 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
1165 ai env (PRefl fc tm) = PRefl fc (ai env tm)
1166 ai env (PUnifyLog tm) = PUnifyLog (ai env tm)
1167 ai env (PNoImplicits tm) = PNoImplicits (ai env tm)
1168 ai env tm = tm
1170 handleErr (Left err) = PElabError err
1171 handleErr (Right x) = x
1173-- if in a pattern, and there are no arguments, and there's no possible
1174-- names with zero explicit arguments, don't add implicits.
1176aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
1177aiFn inpat True ist fc f []
1178 = case lookupDef f (tt_ctxt ist) of
1179 [] -> Right $ PPatvar fc f
1180 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1181 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1182 if (not (vname f) || tcname f
1183 || any (conCaf (tt_ctxt ist)) ialts)
1184-- any constructor alts || any allImp ialts))
1185 then aiFn inpat False ist fc f [] -- use it as a constructor
1186 else Right $ PPatvar fc f
1187 where imp (PExp _ _ _ _) = False
1188 imp _ = True
1189-- allImp [] = False
1190 allImp xs = all imp xs
1191 constructor (TyDecl (DCon _ _) _) = True
1192 constructor _ = False
1194 conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
1196 vname (UN n) = True -- non qualified
1197 vname _ = False
1199aiFn inpat expat ist fc f as
1200 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1201aiFn inpat expat ist fc f as
1202 -- This is where namespaces get resolved by adding PAlternative
1203 = do let ns = lookupCtxtName f (idris_implicits ist)
1204 let ns' = filter (\(n, _) -> notHidden n) ns
1205 case ns' of
1206 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1207 [] -> if f `elem` (map fst (idris_metavars ist))
1208 then Right $ PApp fc (PRef fc f) as
1209 else Right $ mkPApp fc (length as) (PRef fc f) as
1210 alts -> Right $
1211 PAlternative True $
1212 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1213 (insertImpl ns as)) alts
1214 where
1215 notHidden n = case getAccessibility n of
1216 Hidden -> False
1217 _ -> True
1219 getAccessibility n
1220 = case lookupDefAcc n False (tt_ctxt ist) of
1221 [(n,t)] -> t
1222 _ -> Public
1225 insertImpl :: [PArg] -> [PArg] -> [PArg]
1226 insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =
1227 PExp p l tm d : insertImpl ps given
1228 insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =
1229 PConstraint p l tm d : insertImpl ps given
1230 insertImpl (PConstraint p l ty d : ps) given =
1231 PConstraint p l (PResolveTC fc) d : insertImpl ps given
1232 insertImpl (PImp p _ l n ty d : ps) given =
1233 case find n given [] of
1234 Just (tm, given') -> PImp p False l n tm "" : insertImpl ps given'
1235 Nothing -> PImp p True l n Placeholder "" : insertImpl ps given
1236 insertImpl (PTacImplicit p l n sc ty d : ps) given =
1237 case find n given [] of
1238 Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'
1239 Nothing -> if inpat
1240 then PTacImplicit p l n sc Placeholder "" : insertImpl ps given
1241 else PTacImplicit p l n sc sc "" : insertImpl ps given
1242 insertImpl expected [] = []
1243 insertImpl _ given = given
1245 find n [] acc = Nothing
1246 find n (PImp _ _ _ n' t _ : gs) acc
1247 | n == n' = Just (t, reverse acc ++ gs)
1248 find n (PTacImplicit _ _ n' _ t _ : gs) acc
1249 | n == n' = Just (t, reverse acc ++ gs)
1250 find n (g : gs) acc = find n gs (g : acc)
1252-- replace non-linear occurrences with _
1253-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1254-- it is hard to get right!
1256stripLinear :: IState -> PTerm -> PTerm
1257stripLinear i tm = evalState (sl tm) [] where
1258 sl :: PTerm -> State [Name] PTerm
1259 sl (PRef fc f)
1260 | (_:_) <- lookupTy f (tt_ctxt i)
1261 = return $ PRef fc f
1262 | otherwise = do ns <- get
1263 if (f `elem` ns)
1264 then return Placeholder
1265 else do put (f : ns)
1266 return (PRef fc f)
1267 sl (PPatvar fc f)
1268 = do ns <- get
1269 if (f `elem` ns)
1270 then return Placeholder
1271 else do put (f : ns)
1272 return (PPatvar fc f)
1273 sl (PApp fc fn args) = do fn' <- sl fn
1274 args' <- mapM slA args
1275 return $ PApp fc fn' args'
1276 where slA (PImp p m l n t d) = do t' <- sl t
1277 return $ PImp p m l n t' d
1278 slA (PExp p l t d) = do t' <- sl t
1279 return $ PExp p l t' d
1280 slA (PConstraint p l t d)
1281 = do t' <- sl t
1282 return $ PConstraint p l t' d
1283 slA (PTacImplicit p l n sc t d)
1284 = do t' <- sl t
1285 return $ PTacImplicit p l n sc t' d
1286 sl x = return x
1288-- Remove functions which aren't applied to anything, which must then
1289-- be resolved by unification. Assume names resolved and alternatives
1290-- filled in (so no ambiguity).
1292stripUnmatchable :: IState -> PTerm -> PTerm
1293stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1294 su :: PTerm -> PTerm
1295 su (PRef fc f)
1296 | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1297 = Placeholder
1298 su (PApp fc fn args)
1299 = PApp fc fn (fmap (fmap su) args)
1300 su (PAlternative b alts)
1301 = let alts' = filter (/= Placeholder) (map su alts) in
1302 if null alts' then Placeholder
1303 else PAlternative b alts'
1304 su (PPair fc l r) = PPair fc (su l) (su r)
1305 su (PDPair fc l t r) = PDPair fc (su l) (su t) (su r)
1306 su t = t
1307stripUnmatchable i tm = tm
1309mkPApp fc a f [] = f
1310mkPApp fc a f as = let rest = drop a as in
1311 appRest fc (PApp fc f (take a as)) rest
1312 where
1313 appRest fc f [] = f
1314 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1316-- Find 'static' argument positions
1317-- (the declared ones, plus any names in argument position in the declared
1318-- statics)
1319-- FIXME: It's possible that this really has to happen after elaboration
1321findStatics :: IState -> PTerm -> (PTerm, [Bool])
1322findStatics ist tm = trace (showImp Nothing True False tm) $
1323 let (ns, ss) = fs tm in
1324 runState (pos ns ss tm) []
1325 where fs (PPi p n t sc)
1326 | Static <- pstatic p
1327 = let (ns, ss) = fs sc in
1328 (namesIn [] ist t : ns, n : ss)
1329 | otherwise = let (ns, ss) = fs sc in
1330 (ns, ss)
1331 fs _ = ([], [])
1333 inOne n ns = length (filter id (map (elem n) ns)) == 1
1335 pos ns ss (PPi p n t sc)
1336 | elem n ss = do sc' <- pos ns ss sc
1337 spos <- get
1338 put (True : spos)
1339 return (PPi (p { pstatic = Static }) n t sc')
1340 | otherwise = do sc' <- pos ns ss sc
1341 spos <- get
1342 put (False : spos)
1343 return (PPi p n t sc')
1344 pos ns ss t = return t
1346-- Debugging/logging stuff
1348dumpDecls :: [PDecl] -> String
1349dumpDecls [] = ""
1350dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
1352dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
1353dumpDecl (PTy _ _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp Nothing True False t
1354dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
1355dumpDecl (PData _ _ _ _ d) = showDImp True d
1356dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
1357dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
1358dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
1359dumpDecl (PClass _ _ _ cs n ps ds)
1360 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
1361dumpDecl (PInstance _ _ cs n _ t _ ds)
1362 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
1363dumpDecl _ = "..."
1364-- dumpDecl (PImport i) = "import " ++ i
1366-- for 6.12/7 compatibility
1367data EitherErr a b = LeftErr a | RightOK b
1369instance Monad (EitherErr a) where
1370 return = RightOK
1372 (LeftErr e) >>= k = LeftErr e
1373 RightOK v >>= k = k v
1375toEither (LeftErr e) = Left e
1376toEither (RightOK ho) = Right ho
1378-- syntactic match of a against b, returning pair of variables in a
1379-- and what they match. Returns the pair that failed if not a match.
1381matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1382matchClause = matchClause' False
1384matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1385matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1386 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1388 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1389 fullApp x = x
1391 match' x y = match (fullApp x) (fullApp y)
1392 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
1393 | PConstant (I _) <- getTm x = match (getTm x) x'
1394 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
1395 | PConstant (I _) <- getTm x = match (getTm x) x'
1396 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
1397 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
1398 match (PApp _ f args) (PApp _ f' args')
1399 | length args == length args'
1400 = do mf <- match' f f'
1401 ms <- zipWithM matchArg args args'
1402 return (mf ++ concat ms)
1403-- match (PRef _ n) (PRef _ n') | n == n' = return []
1404-- | otherwise = Nothing
1405 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1406 match (PPatvar f n) xr = match (PRef f n) xr
1407 match xr (PPatvar f n) = match xr (PRef f n)
1408 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1409 match (PRef _ n) tm@(PRef _ n')
1410 | n == n' && not names &&
1411 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1412 || tm == Placeholder)
1413 = return [(n, tm)]
1414 | n == n' = return []
1415 match (PRef _ n) tm
1416 | not names && (not (isConName n (tt_ctxt i) ||
1417 isFnName n (tt_ctxt i)) || tm == Placeholder)
1418 = return [(n, tm)]
1419 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1420 mr <- match' r r'
1421 return (ml ++ mr)
1422 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1423 = do ml <- match' l l'
1424 mr <- match' r r'
1425 return (ml ++ mr)
1426 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1427 mr <- match r r'
1428 return (ml ++ mr)
1429 match (PTyped l r) x = match l x
1430 match x (PTyped l r) = match x l
1431 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1432 mr <- match' r r'
1433 return (ml ++ mr)
1434 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1435 mt <- match' t t'
1436 mr <- match' r r'
1437 return (ml ++ mt ++ mr)
1438 match (PAlternative a as) (PAlternative a' as')
1439 = do ms <- zipWithM match' as as'
1440 return (concat ms)
1441 match a@(PAlternative _ as) b
1442 = do let ms = zipWith match' as (repeat b)
1443 case (rights (map toEither ms)) of
1444 (x: _) -> return x
1445 _ -> LeftErr (a, b)
1446 match (PCase _ _ _) _ = return [] -- lifted out
1447 match (PMetavar _) _ = return [] -- modified
1448 match (PInferRef _ _) _ = return [] -- modified
1449 match (PQuote _) _ = return []
1450 match (PProof _) _ = return []
1451 match (PTactics _) _ = return []
1452 match (PRefl _ _) (PRefl _ _) = return []
1453 match (PResolveTC _) (PResolveTC _) = return []
1454 match (PTrue _) (PTrue _) = return []
1455 match (PFalse _) (PFalse _) = return []
1456 match (PReturn _) (PReturn _) = return []
1457 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1458 ms <- match' s s'
1459 return (mt ++ ms)
1460 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1461 ms <- match' s s'
1462 return (mt ++ ms)
1463 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1464 mty <- match' ty ty'
1465 ms <- match' s s'
1466 return (mt ++ mty ++ ms)
1467 match (PHidden x) (PHidden y) = match' x y
1468 match (PUnifyLog x) y = match' x y
1469 match x (PUnifyLog y) = match' x y
1470 match (PNoImplicits x) y = match' x y
1471 match x (PNoImplicits y) = match' x y
1472 match Placeholder _ = return []
1473 match _ Placeholder = return []
1474 match (PResolveTC _) _ = return []
1475 match a b | a == b = return []
1476 | otherwise = LeftErr (a, b)
1478 checkRpts (RightOK ms) = check ms where
1479 check ((n,t):xs)
1480 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1481 then Left (t, t')
1482 else check xs
1483 check (_:xs) = check xs
1484 check [] = Right ms
1485 checkRpts (LeftErr x) = Left x
1487substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1488substMatches ms = substMatchesShadow ms []
1490substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1491substMatchesShadow [] shs t = t
1492substMatchesShadow ((n,tm):ns) shs t
1493 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1495substMatch :: Name -> PTerm -> PTerm -> PTerm
1496substMatch n = substMatchShadow n []
1498substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1499substMatchShadow n shs tm t = sm shs t where
1500 sm xs (PRef _ n') | n == n' = tm
1501 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1502 sm xs (PPi p x t sc)
1503 | x `elem` xs
1504 = let x' = nextName x in
1505 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1506 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1507 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1508 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1509 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1510 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1511 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1512 (fmap (sm xs) tm)
1513 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1514 sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)
1515 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)
1516 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1517 sm xs (PHidden x) = PHidden (sm xs x)
1518 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1519 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1520 sm xs x = x
1522 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1523 fullApp x = x
1525shadow :: Name -> Name -> PTerm -> PTerm
1526shadow n n' t = sm t where
1527 sm (PRef fc x) | n == x = PRef fc n'
1528 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1529 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1530 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1531 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1532 sm (PEq f x y) = PEq f (sm x) (sm y)
1533 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1534 sm (PTyped x y) = PTyped (sm x) (sm y)
1535 sm (PPair f x y) = PPair f (sm x) (sm y)
1536 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1537 sm (PAlternative a as) = PAlternative a (map sm as)
1538 sm (PHidden x) = PHidden (sm x)
1539 sm (PUnifyLog x) = PUnifyLog (sm x)
1540 sm (PNoImplicits x) = PNoImplicits (sm x)
1541 sm x = x