git.iko.soy/Idris-dev
on a10e866 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1537 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
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 = [DefaultEliminator]
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 = []
665-- Defined in builtins.idr
666sigmaTy = UN "Exists"
667existsCon = UN "Ex_intro"
669piBind :: [(Name, PTerm)] -> PTerm -> PTerm
670piBind = piBindp expl
672piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
673piBindp p [] t = t
674piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
676-- Dealing with parameters
678expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
679 [Name] -> -- all names
680 [Name] -> -- names with no declaration
681 PTerm -> PTerm
682expandParams dec ps ns infs tm = en tm
683 where
684 -- if we shadow a name (say in a lambda binding) that is used in a call to
685 -- a lifted function, we need access to both names - once in the scope of the
686 -- binding and once to call the lifted functions. So we'll explicitly shadow
687 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
688 -- but we didn't...)
690 mkShadow (UN n) = MN 0 n
691 mkShadow (MN i n) = MN (i+1) n
692 mkShadow (NS x s) = NS (mkShadow x) s
694 en (PLam n t s)
695 | n `elem` (map fst ps ++ ns)
696 = let n' = mkShadow n in
697 PLam n' (en t) (en (shadow n n' s))
698 | otherwise = PLam n (en t) (en s)
699 en (PPi p n t s)
700 | n `elem` (map fst ps ++ ns)
701 = let n' = mkShadow n in
702 PPi p n' (en t) (en (shadow n n' s))
703 | otherwise = PPi p n (en t) (en s)
704 en (PLet n ty v s)
705 | n `elem` (map fst ps ++ ns)
706 = let n' = mkShadow n in
707 PLet n' (en ty) (en v) (en (shadow n n' s))
708 | otherwise = PLet n (en ty) (en v) (en s)
709 -- FIXME: Should only do this in a type signature!
710 en (PDPair f (PRef f' n) t r)
711 | n `elem` (map fst ps ++ ns) && t /= Placeholder
712 = let n' = mkShadow n in
713 PDPair f (PRef f' n') (en t) (en (shadow n n' r))
714 en (PEq f l r) = PEq f (en l) (en r)
715 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
716 en (PTyped l r) = PTyped (en l) (en r)
717 en (PPair f l r) = PPair f (en l) (en r)
718 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
719 en (PAlternative a as) = PAlternative a (map en as)
720 en (PHidden t) = PHidden (en t)
721 en (PUnifyLog t) = PUnifyLog (en t)
722 en (PNoImplicits t) = PNoImplicits (en t)
723 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
724 en (PProof ts) = PProof (map (fmap en) ts)
725 en (PTactics ts) = PTactics (map (fmap en) ts)
727 en (PQuote (Var n))
728 | n `nselem` ns = PQuote (Var (dec n))
729 en (PApp fc (PInferRef fc' n) as)
730 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
731 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
732 en (PApp fc (PRef fc' n) as)
733 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
734 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
735 | n `nselem` ns = PApp fc (PRef fc' (dec n))
736 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
737 en (PAppBind fc (PRef fc' n) as)
738 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
739 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
740 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
741 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
742 en (PRef fc n)
743 | n `elem` infs = PApp fc (PInferRef fc (dec n))
744 (map (pexp . (PRef fc)) (map fst ps))
745 | n `nselem` ns = PApp fc (PRef fc (dec n))
746 (map (pexp . (PRef fc)) (map fst ps))
747 en (PInferRef fc n)
748 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
749 (map (pexp . (PRef fc)) (map fst ps))
750 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
751 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
752 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
753 en t = t
755 nselem x [] = False
756 nselem x (y : xs) | nseq x y = True
757 | otherwise = nselem x xs
759 nseq x y = nsroot x == nsroot y
761expandParamsD :: Bool -> -- True = RHS only
762 IState ->
763 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
764expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)
765 = if n `elem` ns && (not rhsonly)
766 then -- trace (show (n, expandParams dec ps ns ty)) $
767 PTy doc syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
768 else --trace (show (n, expandParams dec ps ns ty)) $
769 PTy doc syn fc o n (expandParams dec ps ns [] ty)
770expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
771 = if n `elem` ns && (not rhsonly)
772 then -- trace (show (n, expandParams dec ps ns ty)) $
773 PPostulate doc syn fc o (dec n) (piBind ps
774 (expandParams dec ps ns [] ty))
775 else --trace (show (n, expandParams dec ps ns ty)) $
776 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
777expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
778 = let n' = if n `elem` ns then dec n else n in
779 PClauses fc opts n' (map expandParamsC cs)
780 where
781 expandParamsC (PClause fc n lhs ws rhs ds)
782 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
783 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
784 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
785 n' = if n `elem` ns then dec n else n
786 -- names bound on the lhs should not be expanded on the rhs
787 ns' = removeBound lhs ns in
788 PClause fc n' lhs'
789 (map (expandParams dec ps'' ns' []) ws)
790 (expandParams dec ps'' ns' [] rhs)
791 (map (expandParamsD True ist dec ps'' ns') ds)
792 expandParamsC (PWith fc n lhs ws wval ds)
793 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
794 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
795 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
796 n' = if n `elem` ns then dec n else n
797 ns' = removeBound lhs ns in
798 PWith fc n' lhs'
799 (map (expandParams dec ps'' ns' []) ws)
800 (expandParams dec ps'' ns' [] wval)
801 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
802 updateps yn nm [] = []
803 updateps yn nm (((a, t), i):as)
804 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
805 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
807 removeBound lhs ns = ns \\ nub (bnames lhs)
809 bnames (PRef _ n) = [n]
810 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
811 bnames (PPair _ l r) = bnames l ++ bnames r
812 bnames (PDPair _ l Placeholder r) = bnames l ++ bnames r
813 bnames _ = []
815expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
816 = PData doc syn fc co (expandPData pd)
817 where
818 -- just do the type decl, leave constructors alone (parameters will be
819 -- added implicitly)
820 expandPData (PDatadecl n ty cons)
821 = if n `elem` ns
822 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
823 (map econ cons)
824 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
825 econ (doc, n, t, fc)
826 = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc)
827expandParamsD rhs ist dec ps ns (PParams f params pds)
828 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
829 (map (expandParamsD True ist dec ps ns) pds)
830-- (map (expandParamsD ist dec ps ns) pds)
831expandParamsD rhs ist dec ps ns (PMutual f pds)
832 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
833expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
834 = PClass doc info f
835 (map (expandParams dec ps ns []) cs)
836 n
837 (map (mapsnd (expandParams dec ps ns [])) params)
838 (map (expandParamsD rhs ist dec ps ns) decls)
839expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
840 = PInstance info f
841 (map (expandParams dec ps ns []) cs)
842 n
843 (map (expandParams dec ps ns []) params)
844 (expandParams dec ps ns [] ty)
845 cn
846 (map (expandParamsD rhs ist dec ps ns) decls)
847expandParamsD rhs ist dec ps ns d = d
849mapsnd f (x, t) = (x, f t)
851-- Calculate a priority for a type, for deciding elaboration order
852-- * if it's just a type variable or concrete type, do it early (0)
853-- * if there's only type variables and injective constructors, do it next (1)
854-- * if there's a function type, next (2)
855-- * finally, everything else (3)
857getPriority :: IState -> PTerm -> Int
858getPriority i tm = 1 -- pri tm
859 where
860 pri (PRef _ n) =
861 case lookupP n (tt_ctxt i) of
862 ((P (DCon _ _) _ _):_) -> 1
863 ((P (TCon _ _) _ _):_) -> 1
864 ((P Ref _ _):_) -> 1
865 [] -> 0 -- must be locally bound, if it's not an error...
866 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
867 pri (PTrue _) = 0
868 pri (PFalse _) = 0
869 pri (PRefl _ _) = 1
870 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
871 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
872 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
873 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
874 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
875 pri (PTyped l r) = pri l
876 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
877 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
878 pri (PAlternative a as) = maximum (map pri as)
879 pri (PConstant _) = 0
880 pri Placeholder = 1
881 pri _ = 3
883addStatics :: Name -> Term -> PTerm -> Idris ()
884addStatics n tm ptm =
885 do let (statics, dynamics) = initStatics tm ptm
886 let stnames = nub $ concatMap freeArgNames (map snd statics)
887 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
888 when (not (null statics)) $
889 logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics
890 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
891 -- also get the arguments which are 'uniquely inferrable' from
892 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
893 let statics' = nub $ map fst statics ++
894 filter (\x -> not (elem x dnames)) stnames
895 let stpos = staticList statics' tm
896 i <- getIState
897 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
898 addIBC (IBCStatic n)
899 where
900 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
901 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
902 if pstatic p == Static then ((n, ty) : static, dynamic)
903 else if (not (searchArg p))
904 then (static, (n, ty) : dynamic)
905 else (static, dynamic)
906 initStatics t pt = ([], [])
908 freeArgNames tm = let (_, args) = unApply tm in
909 concatMap freeNames args
911 -- if a name appears in a type class or tactic implicit index, it doesn't
912 -- affect its 'uniquely inferrable' from a static status since these are
913 -- resolved by searching.
914 searchArg (Constraint _ _ _) = True
915 searchArg (TacImp _ _ _ _) = True
916 searchArg _ = False
918 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
919 staticList _ _ = []
921-- Dealing with implicit arguments
923-- Add constraint bindings from using block
925addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
926addUsingConstraints syn fc t
927 = do ist <- get
928 let ns = namesIn [] ist t
929 let cs = getConstraints t -- check declared constraints
930 let addconsts = uconsts \\ cs
931 -- if all names in the arguments of addconsts appear in ns,
932 -- add the constraint implicitly
933 return (doAdd addconsts ns t)
934 where uconsts = filter uconst (using syn)
935 uconst (UConstraint _ _) = True
936 uconst _ = False
938 doAdd [] _ t = t
939 -- if all of args in ns, then add it
940 doAdd (UConstraint c args : cs) ns t
941 | all (\n -> elem n ns) args
942 = PPi (Constraint False Dynamic "") (MN 0 "cu")
943 (mkConst c args) (doAdd cs ns t)
944 | otherwise = doAdd cs ns t
946 mkConst c args = PApp fc (PRef fc c)
947 (map (\n -> PExp 0 False (PRef fc n) "") args)
949 getConstraints (PPi (Constraint _ _ _) _ c sc)
950 = getcapp c ++ getConstraints sc
951 getConstraints (PPi _ _ c sc) = getConstraints sc
952 getConstraints _ = []
954 getcapp (PApp _ (PRef _ c) args)
955 = do ns <- mapM getName args
956 return (UConstraint c ns)
957 getcapp _ = []
959 getName (PExp _ _ (PRef _ n) _) = return n
960 getName _ = []
962-- Add implicit Pi bindings for any names in the term which appear in an
963-- argument position.
965-- This has become a right mess already. Better redo it some time...
967implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
968implicit syn n ptm = implicit' syn [] n ptm
970implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
971implicit' syn ignore n ptm
972 = do i <- getIState
973 let (tm', impdata) = implicitise syn ignore i ptm
974-- let (tm'', spos) = findStatics i tm'
975 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
976 addIBC (IBCImp n)
977 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
978-- i <- get
979-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
980 return tm'
982implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
983implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
984 let (declimps, ns') = execState (imps True [] tm) ([], [])
985 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
986 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
987 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
988 if null ns
989 then (tm, reverse declimps)
990 else implicitise syn ignore ist (pibind uvars nsOrder tm)
991 where
992 uvars = map ipair (filter uimplicit (using syn))
993 pvars = syn_params syn
995 inUsing n = n `elem` map fst uvars
997 ipair (UImplicit x y) = (x, y)
998 uimplicit (UImplicit _ _) = True
999 uimplicit _ = False
1001 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1002 | otherwise = x : dropAll xs ys
1003 dropAll [] ys = []
1005 imps top env (PApp _ f as)
1006 = do (decls, ns) <- get
1007 let isn = concatMap (namesIn uvars ist) (map getTm as)
1008 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1009 imps top env (PPi (Imp l _ doc _) n ty sc)
1010 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1011 (decls , ns) <- get
1012 put (PImp (getPriority ist ty) True l n ty doc : decls,
1013 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1014 imps True (n:env) sc
1015 imps top env (PPi (Exp l _ doc _) n ty sc)
1016 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1017 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1018 _ -> [])
1019 (decls, ns) <- get -- ignore decls in HO types
1020 put (PExp (getPriority ist ty) l ty doc : decls,
1021 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1022 imps True (n:env) sc
1023 imps top env (PPi (Constraint l _ doc) n ty sc)
1024 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1025 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1026 _ -> [])
1027 (decls, ns) <- get -- ignore decls in HO types
1028 put (PConstraint 10 l ty doc : decls,
1029 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1030 imps True (n:env) sc
1031 imps top env (PPi (TacImp l _ scr doc) n ty sc)
1032 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1033 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1034 _ -> [])
1035 (decls, ns) <- get -- ignore decls in HO types
1036 put (PTacImplicit 10 l n scr ty doc : decls,
1037 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1038 imps True (n:env) sc
1039 imps top env (PEq _ l r)
1040 = do (decls, ns) <- get
1041 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1042 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1043 imps top env (PRewrite _ l r _)
1044 = do (decls, ns) <- get
1045 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1046 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1047 imps top env (PTyped l r)
1048 = imps top env l
1049 imps top env (PPair _ 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 (PDPair _ (PRef _ n) t r)
1054 = do (decls, ns) <- get
1055 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1056 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1057 imps top env (PDPair _ l t r)
1058 = do (decls, ns) <- get
1059 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1060 namesIn uvars ist r
1061 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1062 imps top env (PAlternative a as)
1063 = do (decls, ns) <- get
1064 let isn = concatMap (namesIn uvars ist) as
1065 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1066 imps top env (PLam n ty sc)
1067 = do imps False env ty
1068 imps False (n:env) sc
1069 imps top env (PHidden tm) = imps False env tm
1070 imps top env (PUnifyLog tm) = imps False env tm
1071 imps top env (PNoImplicits tm) = imps False env tm
1072 imps top env _ = return ()
1074 pibind using [] sc = sc
1075 pibind using (n:ns) sc
1076 = case lookup n using of
1077 Just ty -> PPi (Imp False Dynamic "" False) n ty (pibind using ns sc)
1078 Nothing -> PPi (Imp False Dynamic "" False) n Placeholder
1079 (pibind using ns sc)
1081-- Add implicit arguments in function calls
1082addImplPat :: IState -> PTerm -> PTerm
1083addImplPat = addImpl' True [] []
1085addImplBound :: IState -> [Name] -> PTerm -> PTerm
1086addImplBound ist ns = addImpl' False ns [] ist
1088addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1089addImplBoundInf ist ns inf = addImpl' False ns inf ist
1091addImpl :: IState -> PTerm -> PTerm
1092addImpl = addImpl' False [] []
1094-- TODO: in patterns, don't add implicits to function names guarded by constructors
1095-- and *not* inside a PHidden
1097addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1098addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm
1099 where
1100 ai env (PRef fc f)
1101 | f `elem` infns = PInferRef fc f
1102 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f []
1103 ai env (PHidden (PRef fc f))
1104 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f []
1105 ai env (PEq fc l r) = let l' = ai env l
1106 r' = ai env r in
1107 PEq fc l' r'
1108 ai env (PRewrite fc l r g) = let l' = ai env l
1109 r' = ai env r
1110 g' = fmap (ai env) g in
1111 PRewrite fc l' r' g'
1112 ai env (PTyped l r) = let l' = ai env l
1113 r' = ai env r in
1114 PTyped l' r'
1115 ai env (PPair fc l r) = let l' = ai env l
1116 r' = ai env r in
1117 PPair fc l' r'
1118 ai env (PDPair fc l t r) = let l' = ai env l
1119 t' = ai env t
1120 r' = ai env r in
1121 PDPair fc l' t' r'
1122 ai env (PAlternative a as) = let as' = map (ai env) as in
1123 PAlternative a as'
1124 ai env (PApp fc (PInferRef _ f) as)
1125 = let as' = map (fmap (ai env)) as in
1126 PApp fc (PInferRef fc f) as'
1127 ai env (PApp fc ftm@(PRef _ f) as)
1128 | f `elem` infns = ai env (PApp fc (PInferRef fc f) as)
1129 | not (f `elem` map fst env)
1130 = let as' = map (fmap (ai env)) as in
1131 handleErr $ aiFn inpat False ist fc f as'
1132 | Just (Just ty) <- lookup f env
1133 = let as' = map (fmap (ai env)) as
1134 arity = getPArity ty in
1135 mkPApp fc arity ftm as'
1136 ai env (PApp fc f as) = let f' = ai env f
1137 as' = map (fmap (ai env)) as in
1138 mkPApp fc 1 f' as'
1139 ai env (PCase fc c os) = let c' = ai env c
1140 os' = map (pmap (ai env)) os in
1141 PCase fc c' os'
1142 ai env (PLam n ty sc) = let ty' = ai env ty
1143 sc' = ai ((n, Just ty):env) sc in
1144 PLam n ty' sc'
1145 ai env (PLet n ty val sc)
1146 = let ty' = ai env ty
1147 val' = ai env val
1148 sc' = ai ((n, Just ty):env) sc in
1149 PLet n ty' val' sc'
1150 ai env (PPi p n ty sc) = let ty' = ai env ty
1151 sc' = ai ((n, Just ty):env) sc in
1152 PPi p n ty' sc'
1153 ai env (PGoal fc r n sc) = let r' = ai env r
1154 sc' = ai ((n, Nothing):env) sc in
1155 PGoal fc r' n sc'
1156 ai env (PHidden tm) = PHidden (ai env tm)
1157 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
1158 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
1159 ai env (PRefl fc tm) = PRefl fc (ai env tm)
1160 ai env (PUnifyLog tm) = PUnifyLog (ai env tm)
1161 ai env (PNoImplicits tm) = PNoImplicits (ai env tm)
1162 ai env tm = tm
1164 handleErr (Left err) = PElabError err
1165 handleErr (Right x) = x
1167-- if in a pattern, and there are no arguments, and there's no possible
1168-- names with zero explicit arguments, don't add implicits.
1170aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
1171aiFn inpat True ist fc f []
1172 = case lookupDef f (tt_ctxt ist) of
1173 [] -> Right $ PPatvar fc f
1174 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1175 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1176 if (not (vname f) || tcname f
1177 || any (conCaf (tt_ctxt ist)) ialts)
1178-- any constructor alts || any allImp ialts))
1179 then aiFn inpat False ist fc f [] -- use it as a constructor
1180 else Right $ PPatvar fc f
1181 where imp (PExp _ _ _ _) = False
1182 imp _ = True
1183-- allImp [] = False
1184 allImp xs = all imp xs
1185 constructor (TyDecl (DCon _ _) _) = True
1186 constructor _ = False
1188 conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
1190 vname (UN n) = True -- non qualified
1191 vname _ = False
1193aiFn inpat expat ist fc f as
1194 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1195aiFn inpat expat ist fc f as
1196 -- This is where namespaces get resolved by adding PAlternative
1197 = do let ns = lookupCtxtName f (idris_implicits ist)
1198 let ns' = filter (\(n, _) -> notHidden n) ns
1199 case ns' of
1200 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1201 [] -> if f `elem` (map fst (idris_metavars ist))
1202 then Right $ PApp fc (PRef fc f) as
1203 else Right $ mkPApp fc (length as) (PRef fc f) as
1204 alts -> Right $
1205 PAlternative True $
1206 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1207 (insertImpl ns as)) alts
1208 where
1209 notHidden n = case getAccessibility n of
1210 Hidden -> False
1211 _ -> True
1213 getAccessibility n
1214 = case lookupDefAcc n False (tt_ctxt ist) of
1215 [(n,t)] -> t
1216 _ -> Public
1219 insertImpl :: [PArg] -> [PArg] -> [PArg]
1220 insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =
1221 PExp p l tm d : insertImpl ps given
1222 insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =
1223 PConstraint p l tm d : insertImpl ps given
1224 insertImpl (PConstraint p l ty d : ps) given =
1225 PConstraint p l (PResolveTC fc) d : insertImpl ps given
1226 insertImpl (PImp p _ l n ty d : ps) given =
1227 case find n given [] of
1228 Just (tm, given') -> PImp p False l n tm "" : insertImpl ps given'
1229 Nothing -> PImp p True l n Placeholder "" : insertImpl ps given
1230 insertImpl (PTacImplicit p l n sc ty d : ps) given =
1231 case find n given [] of
1232 Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'
1233 Nothing -> if inpat
1234 then PTacImplicit p l n sc Placeholder "" : insertImpl ps given
1235 else PTacImplicit p l n sc sc "" : insertImpl ps given
1236 insertImpl expected [] = []
1237 insertImpl _ given = given
1239 find n [] acc = Nothing
1240 find n (PImp _ _ _ n' t _ : gs) acc
1241 | n == n' = Just (t, reverse acc ++ gs)
1242 find n (PTacImplicit _ _ n' _ t _ : gs) acc
1243 | n == n' = Just (t, reverse acc ++ gs)
1244 find n (g : gs) acc = find n gs (g : acc)
1246-- replace non-linear occurrences with _
1247-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1248-- it is hard to get right!
1250stripLinear :: IState -> PTerm -> PTerm
1251stripLinear i tm = evalState (sl tm) [] where
1252 sl :: PTerm -> State [Name] PTerm
1253 sl (PRef fc f)
1254 | (_:_) <- lookupTy f (tt_ctxt i)
1255 = return $ PRef fc f
1256 | otherwise = do ns <- get
1257 if (f `elem` ns)
1258 then return Placeholder
1259 else do put (f : ns)
1260 return (PRef fc f)
1261 sl (PPatvar fc f)
1262 = do ns <- get
1263 if (f `elem` ns)
1264 then return Placeholder
1265 else do put (f : ns)
1266 return (PPatvar fc f)
1267 sl (PApp fc fn args) = do fn' <- sl fn
1268 args' <- mapM slA args
1269 return $ PApp fc fn' args'
1270 where slA (PImp p m l n t d) = do t' <- sl t
1271 return $ PImp p m l n t' d
1272 slA (PExp p l t d) = do t' <- sl t
1273 return $ PExp p l t' d
1274 slA (PConstraint p l t d)
1275 = do t' <- sl t
1276 return $ PConstraint p l t' d
1277 slA (PTacImplicit p l n sc t d)
1278 = do t' <- sl t
1279 return $ PTacImplicit p l n sc t' d
1280 sl x = return x
1282-- Remove functions which aren't applied to anything, which must then
1283-- be resolved by unification. Assume names resolved and alternatives
1284-- filled in (so no ambiguity).
1286stripUnmatchable :: IState -> PTerm -> PTerm
1287stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1288 su :: PTerm -> PTerm
1289 su (PRef fc f)
1290 | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1291 = Placeholder
1292 su (PApp fc fn args)
1293 = PApp fc fn (fmap (fmap su) args)
1294 su (PAlternative b alts)
1295 = let alts' = filter (/= Placeholder) (map su alts) in
1296 if null alts' then Placeholder
1297 else PAlternative b alts'
1298 su (PPair fc l r) = PPair fc (su l) (su r)
1299 su (PDPair fc l t r) = PDPair fc (su l) (su t) (su r)
1300 su t = t
1301stripUnmatchable i tm = tm
1303mkPApp fc a f [] = f
1304mkPApp fc a f as = let rest = drop a as in
1305 appRest fc (PApp fc f (take a as)) rest
1306 where
1307 appRest fc f [] = f
1308 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1310-- Find 'static' argument positions
1311-- (the declared ones, plus any names in argument position in the declared
1312-- statics)
1313-- FIXME: It's possible that this really has to happen after elaboration
1315findStatics :: IState -> PTerm -> (PTerm, [Bool])
1316findStatics ist tm = trace (showImp Nothing True False tm) $
1317 let (ns, ss) = fs tm in
1318 runState (pos ns ss tm) []
1319 where fs (PPi p n t sc)
1320 | Static <- pstatic p
1321 = let (ns, ss) = fs sc in
1322 (namesIn [] ist t : ns, n : ss)
1323 | otherwise = let (ns, ss) = fs sc in
1324 (ns, ss)
1325 fs _ = ([], [])
1327 inOne n ns = length (filter id (map (elem n) ns)) == 1
1329 pos ns ss (PPi p n t sc)
1330 | elem n ss = do sc' <- pos ns ss sc
1331 spos <- get
1332 put (True : spos)
1333 return (PPi (p { pstatic = Static }) n t sc')
1334 | otherwise = do sc' <- pos ns ss sc
1335 spos <- get
1336 put (False : spos)
1337 return (PPi p n t sc')
1338 pos ns ss t = return t
1340-- Debugging/logging stuff
1342dumpDecls :: [PDecl] -> String
1343dumpDecls [] = ""
1344dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
1346dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
1347dumpDecl (PTy _ _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp Nothing True False t
1348dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
1349dumpDecl (PData _ _ _ _ d) = showDImp True d
1350dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
1351dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
1352dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
1353dumpDecl (PClass _ _ _ cs n ps ds)
1354 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
1355dumpDecl (PInstance _ _ cs n _ t _ ds)
1356 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
1357dumpDecl _ = "..."
1358-- dumpDecl (PImport i) = "import " ++ i
1360-- for 6.12/7 compatibility
1361data EitherErr a b = LeftErr a | RightOK b
1363instance Monad (EitherErr a) where
1364 return = RightOK
1366 (LeftErr e) >>= k = LeftErr e
1367 RightOK v >>= k = k v
1369toEither (LeftErr e) = Left e
1370toEither (RightOK ho) = Right ho
1372-- syntactic match of a against b, returning pair of variables in a
1373-- and what they match. Returns the pair that failed if not a match.
1375matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1376matchClause = matchClause' False
1378matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1379matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1380 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1382 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1383 fullApp x = x
1385 match' x y = match (fullApp x) (fullApp y)
1386 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
1387 | PConstant (I _) <- getTm x = match (getTm x) x'
1388 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
1389 | PConstant (I _) <- getTm x = match (getTm x) x'
1390 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
1391 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
1392 match (PApp _ f args) (PApp _ f' args')
1393 | length args == length args'
1394 = do mf <- match' f f'
1395 ms <- zipWithM matchArg args args'
1396 return (mf ++ concat ms)
1397-- match (PRef _ n) (PRef _ n') | n == n' = return []
1398-- | otherwise = Nothing
1399 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1400 match (PPatvar f n) xr = match (PRef f n) xr
1401 match xr (PPatvar f n) = match xr (PRef f n)
1402 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1403 match (PRef _ n) tm@(PRef _ n')
1404 | n == n' && not names &&
1405 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1406 || tm == Placeholder)
1407 = return [(n, tm)]
1408 | n == n' = return []
1409 match (PRef _ n) tm
1410 | not names && (not (isConName n (tt_ctxt i) ||
1411 isFnName n (tt_ctxt i)) || tm == Placeholder)
1412 = return [(n, tm)]
1413 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1414 mr <- match' r r'
1415 return (ml ++ mr)
1416 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1417 = do ml <- match' l l'
1418 mr <- match' r r'
1419 return (ml ++ mr)
1420 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1421 mr <- match r r'
1422 return (ml ++ mr)
1423 match (PTyped l r) x = match l x
1424 match x (PTyped l r) = match x l
1425 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1426 mr <- match' r r'
1427 return (ml ++ mr)
1428 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1429 mt <- match' t t'
1430 mr <- match' r r'
1431 return (ml ++ mt ++ mr)
1432 match (PAlternative a as) (PAlternative a' as')
1433 = do ms <- zipWithM match' as as'
1434 return (concat ms)
1435 match a@(PAlternative _ as) b
1436 = do let ms = zipWith match' as (repeat b)
1437 case (rights (map toEither ms)) of
1438 (x: _) -> return x
1439 _ -> LeftErr (a, b)
1440 match (PCase _ _ _) _ = return [] -- lifted out
1441 match (PMetavar _) _ = return [] -- modified
1442 match (PInferRef _ _) _ = return [] -- modified
1443 match (PQuote _) _ = return []
1444 match (PProof _) _ = return []
1445 match (PTactics _) _ = return []
1446 match (PRefl _ _) (PRefl _ _) = return []
1447 match (PResolveTC _) (PResolveTC _) = return []
1448 match (PTrue _) (PTrue _) = return []
1449 match (PFalse _) (PFalse _) = return []
1450 match (PReturn _) (PReturn _) = return []
1451 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1452 ms <- match' s s'
1453 return (mt ++ ms)
1454 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1455 ms <- match' s s'
1456 return (mt ++ ms)
1457 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1458 mty <- match' ty ty'
1459 ms <- match' s s'
1460 return (mt ++ mty ++ ms)
1461 match (PHidden x) (PHidden y) = match' x y
1462 match (PUnifyLog x) y = match' x y
1463 match x (PUnifyLog y) = match' x y
1464 match (PNoImplicits x) y = match' x y
1465 match x (PNoImplicits y) = match' x y
1466 match Placeholder _ = return []
1467 match _ Placeholder = return []
1468 match (PResolveTC _) _ = return []
1469 match a b | a == b = return []
1470 | otherwise = LeftErr (a, b)
1472 checkRpts (RightOK ms) = check ms where
1473 check ((n,t):xs)
1474 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1475 then Left (t, t')
1476 else check xs
1477 check (_:xs) = check xs
1478 check [] = Right ms
1479 checkRpts (LeftErr x) = Left x
1481substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1482substMatches ms = substMatchesShadow ms []
1484substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1485substMatchesShadow [] shs t = t
1486substMatchesShadow ((n,tm):ns) shs t
1487 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1489substMatch :: Name -> PTerm -> PTerm -> PTerm
1490substMatch n = substMatchShadow n []
1492substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1493substMatchShadow n shs tm t = sm shs t where
1494 sm xs (PRef _ n') | n == n' = tm
1495 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1496 sm xs (PPi p x t sc)
1497 | x `elem` xs
1498 = let x' = nextName x in
1499 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1500 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1501 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1502 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1503 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1504 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1505 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1506 (fmap (sm xs) tm)
1507 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1508 sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)
1509 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)
1510 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1511 sm xs (PHidden x) = PHidden (sm xs x)
1512 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1513 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1514 sm xs x = x
1516 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1517 fullApp x = x
1519shadow :: Name -> Name -> PTerm -> PTerm
1520shadow n n' t = sm t where
1521 sm (PRef fc x) | n == x = PRef fc n'
1522 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1523 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1524 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1525 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1526 sm (PEq f x y) = PEq f (sm x) (sm y)
1527 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1528 sm (PTyped x y) = PTyped (sm x) (sm y)
1529 sm (PPair f x y) = PPair f (sm x) (sm y)
1530 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1531 sm (PAlternative a as) = PAlternative a (map sm as)
1532 sm (PHidden x) = PHidden (sm x)
1533 sm (PUnifyLog x) = PUnifyLog (sm x)
1534 sm (PNoImplicits x) = PNoImplicits (sm x)
1535 sm x = x