git.iko.soy/Idris-dev
on 1203cb9 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1514 lines 63 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.IdeSlave
12import Idris.Colours
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))] -> 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, _)) -> (n, (top, i))) 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 ->
329 case span (/=':') s of
330 (fn, ':':rest) -> case span isDigit rest of
331 ([], ':':msg) -> write
332 ([], msg) -> write
333 (row, ':':rest') ->
334 case span isDigit rest' of
335 ([], msg) -> iWarn (FC fn (read row) 0) msg
336 (col, ':':msg) -> iWarn (FC fn (read row) (read col)) msg
337 _ -> write
338 where write = runIO . hPutStrLn h $ convSExp "write-string" s n
340iputStrLn = ihputStrLn stdout
341iPrintError = ihPrintError stdout
342iPrintResult = ihPrintResult stdout
344ideslavePutSExp :: SExpable a => String -> a -> Idris ()
345ideslavePutSExp cmd info = do i <- getIState
346 case idris_outputmode i of
347 IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
348 _ -> return ()
350-- this needs some typing magic and more structured output towards emacs
351iputGoal :: String -> Idris ()
352iputGoal s = do i <- getIState
353 case idris_outputmode i of
354 RawOutput -> runIO $ putStrLn s
355 IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" s n
357isetPrompt :: String -> Idris ()
358isetPrompt p = do i <- getIState
359 case idris_outputmode i of
360 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n
362iWarn :: FC -> String -> Idris ()
363iWarn fc err = do i <- getIState
364 case idris_outputmode i of
365 RawOutput -> runIO $ putStrLn (show fc ++ ":" ++ err)
366 IdeSlave n -> runIO . putStrLn $ convSExp "warning" (fc_fname fc, fc_line fc, err) n
368setLogLevel :: Int -> Idris ()
369setLogLevel l = do i <- getIState
370 let opts = idris_options i
371 let opt' = opts { opt_logLevel = l }
372 putIState $ i { idris_options = opt' }
374setCmdLine :: [Opt] -> Idris ()
375setCmdLine opts = do i <- getIState
376 let iopts = idris_options i
377 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
379getCmdLine :: Idris [Opt]
380getCmdLine = do i <- getIState
381 return (opt_cmdline (idris_options i))
383getDumpDefun :: Idris (Maybe FilePath)
384getDumpDefun = do i <- getIState
385 return $ findC (opt_cmdline (idris_options i))
386 where findC [] = Nothing
387 findC (DumpDefun x : _) = Just x
388 findC (_ : xs) = findC xs
390getDumpCases :: Idris (Maybe FilePath)
391getDumpCases = do i <- getIState
392 return $ findC (opt_cmdline (idris_options i))
393 where findC [] = Nothing
394 findC (DumpCases x : _) = Just x
395 findC (_ : xs) = findC xs
397logLevel :: Idris Int
398logLevel = do i <- getIState
399 return (opt_logLevel (idris_options i))
401setErrContext :: Bool -> Idris ()
402setErrContext t = do i <- getIState
403 let opts = idris_options i
404 let opt' = opts { opt_errContext = t }
405 putIState $ i { idris_options = opt' }
407errContext :: Idris Bool
408errContext = do i <- getIState
409 return (opt_errContext (idris_options i))
411useREPL :: Idris Bool
412useREPL = do i <- getIState
413 return (opt_repl (idris_options i))
415setREPL :: Bool -> Idris ()
416setREPL t = do i <- getIState
417 let opts = idris_options i
418 let opt' = opts { opt_repl = t }
419 putIState $ i { idris_options = opt' }
421setQuiet :: Bool -> Idris ()
422setQuiet q = do i <- getIState
423 let opts = idris_options i
424 let opt' = opts { opt_quiet = q }
425 putIState $ i { idris_options = opt' }
427getQuiet :: Idris Bool
428getQuiet = do i <- getIState
429 let opts = idris_options i
430 return (opt_quiet opts)
432setCodegen :: Codegen -> Idris ()
433setCodegen t = do i <- getIState
434 let opts = idris_options i
435 let opt' = opts { opt_codegen = t }
436 putIState $ i { idris_options = opt' }
438codegen :: Idris Codegen
439codegen = do i <- getIState
440 return (opt_codegen (idris_options i))
442setOutputTy :: OutputType -> Idris ()
443setOutputTy t = do i <- getIState
444 let opts = idris_options i
445 let opt' = opts { opt_outputTy = t }
446 putIState $ i { idris_options = opt' }
448outputTy :: Idris OutputType
449outputTy = do i <- getIState
450 return $ opt_outputTy $ idris_options i
452setIdeSlave :: Bool -> Idris ()
453setIdeSlave True = do i <- getIState
454 putIState $ i { idris_outputmode = (IdeSlave 0) }
455setIdeSlave False = return ()
457setTargetTriple :: String -> Idris ()
458setTargetTriple t = do i <- getIState
459 let opts = idris_options i
460 opt' = opts { opt_triple = t }
461 putIState $ i { idris_options = opt' }
463targetTriple :: Idris String
464targetTriple = do i <- getIState
465 return (opt_triple (idris_options i))
467setTargetCPU :: String -> Idris ()
468setTargetCPU t = do i <- getIState
469 let opts = idris_options i
470 opt' = opts { opt_cpu = t }
471 putIState $ i { idris_options = opt' }
473targetCPU :: Idris String
474targetCPU = do i <- getIState
475 return (opt_cpu (idris_options i))
477setOptLevel :: Word -> Idris ()
478setOptLevel t = do i <- getIState
479 let opts = idris_options i
480 opt' = opts { opt_optLevel = t }
481 putIState $ i { idris_options = opt' }
483optLevel :: Idris Word
484optLevel = do i <- getIState
485 return (opt_optLevel (idris_options i))
487verbose :: Idris Bool
488verbose = do i <- getIState
489 return (opt_verbose (idris_options i))
491setVerbose :: Bool -> Idris ()
492setVerbose t = do i <- getIState
493 let opts = idris_options i
494 let opt' = opts { opt_verbose = t }
495 putIState $ i { idris_options = opt' }
497typeInType :: Idris Bool
498typeInType = do i <- getIState
499 return (opt_typeintype (idris_options i))
501setTypeInType :: Bool -> Idris ()
502setTypeInType t = do i <- getIState
503 let opts = idris_options i
504 let opt' = opts { opt_typeintype = t }
505 putIState $ i { idris_options = opt' }
507coverage :: Idris Bool
508coverage = do i <- getIState
509 return (opt_coverage (idris_options i))
511setCoverage :: Bool -> Idris ()
512setCoverage t = do i <- getIState
513 let opts = idris_options i
514 let opt' = opts { opt_coverage = t }
515 putIState $ i { idris_options = opt' }
517setIBCSubDir :: FilePath -> Idris ()
518setIBCSubDir fp = do i <- getIState
519 let opts = idris_options i
520 let opt' = opts { opt_ibcsubdir = fp }
521 putIState $ i { idris_options = opt' }
523valIBCSubDir :: IState -> Idris FilePath
524valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
526addImportDir :: FilePath -> Idris ()
527addImportDir fp = do i <- getIState
528 let opts = idris_options i
529 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
530 putIState $ i { idris_options = opt' }
532setImportDirs :: [FilePath] -> Idris ()
533setImportDirs fps = do i <- getIState
534 let opts = idris_options i
535 let opt' = opts { opt_importdirs = fps }
536 putIState $ i { idris_options = opt' }
538allImportDirs :: Idris [FilePath]
539allImportDirs = do i <- getIState
540 let optdirs = opt_importdirs (idris_options i)
541 return ("." : reverse optdirs)
543colourise :: Idris Bool
544colourise = do i <- getIState
545 return $ idris_colourRepl i
547setColourise :: Bool -> Idris ()
548setColourise b = do i <- getIState
549 putIState $ i { idris_colourRepl = b }
551setOutH :: Handle -> Idris ()
552setOutH h = do i <- getIState
553 putIState $ i { idris_outh = h }
555impShow :: Idris Bool
556impShow = do i <- getIState
557 return (opt_showimp (idris_options i))
559setImpShow :: Bool -> Idris ()
560setImpShow t = do i <- getIState
561 let opts = idris_options i
562 let opt' = opts { opt_showimp = t }
563 putIState $ i { idris_options = opt' }
565setColour :: ColourType -> IdrisColour -> Idris ()
566setColour ct c = do i <- getIState
567 let newTheme = setColour' ct c (idris_colourTheme i)
568 putIState $ i { idris_colourTheme = newTheme }
569 where setColour' KeywordColour c t = t { keywordColour = c }
570 setColour' BoundVarColour c t = t { boundVarColour = c }
571 setColour' ImplicitColour c t = t { implicitColour = c }
572 setColour' FunctionColour c t = t { functionColour = c }
573 setColour' TypeColour c t = t { typeColour = c }
574 setColour' DataColour c t = t { dataColour = c }
575 setColour' PromptColour c t = t { promptColour = c }
577logLvl :: Int -> String -> Idris ()
578logLvl l str = do i <- getIState
579 let lvl = opt_logLevel (idris_options i)
580 when (lvl >= l)
581 $ do runIO (putStrLn str)
582 putIState $ i { idris_log = idris_log i ++ str ++ "\n" }
584cmdOptType :: Opt -> Idris Bool
585cmdOptType x = do i <- getIState
586 return $ x `elem` opt_cmdline (idris_options i)
588iLOG :: String -> Idris ()
589iLOG = logLvl 1
591noErrors :: Idris Bool
592noErrors = do i <- getIState
593 case errLine i of
594 Nothing -> return True
595 _ -> return False
597setTypeCase :: Bool -> Idris ()
598setTypeCase t = do i <- getIState
599 let opts = idris_options i
600 let opt' = opts { opt_typecase = t }
601 putIState $ i { idris_options = opt' }
604-- For inferring types of things
606bi = fileFC "builtin"
608inferTy = MN 0 "__Infer"
609inferCon = MN 0 "__infer"
610inferDecl = PDatadecl inferTy
611 PType
612 [("", inferCon, PPi impl (MN 0 "A") PType (
613 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
614 (PRef bi inferTy)), bi)]
616infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder True, pexp t]
617infP = P (TCon 6 0) inferTy (TType (UVal 0))
619getInferTerm, getInferType :: Term -> Term
620getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
621getInferTerm (App (App _ _) tm) = tm
622getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
624getInferType (Bind n b sc) = Bind n b $ getInferType sc
625getInferType (App (App _ ty) _) = ty
627-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
629primNames = [unitTy, unitCon,
630 falseTy, pairTy, pairCon,
631 eqTy, eqCon, inferTy, inferCon]
633unitTy = MN 0 "__Unit"
634unitCon = MN 0 "__II"
635unitDecl = PDatadecl unitTy PType
636 [("", unitCon, PRef bi unitTy, bi)]
638falseTy = MN 0 "__False"
639falseDecl = PDatadecl falseTy PType []
641pairTy = MN 0 "__Pair"
642pairCon = MN 0 "__MkPair"
643pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
644 [("", pairCon, PPi impl (n "A") PType (
645 PPi impl (n "B") PType (
646 PPi expl (n "a") (PRef bi (n "A")) (
647 PPi expl (n "b") (PRef bi (n "B"))
648 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
649 pexp (PRef bi (n "B"))])))), bi)]
650 where n a = MN 0 a
652eqTy = UN "="
653eqCon = UN "refl"
654eqDecl = PDatadecl eqTy (piBind [(n "a", PType), (n "b", PType),
655 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
656 PType)
657 [("", eqCon, PPi impl (n "a") PType (
658 PPi impl (n "x") (PRef bi (n "a"))
659 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder False,
660 pimp (n "b") Placeholder False,
661 pexp (PRef bi (n "x")),
662 pexp (PRef bi (n "x"))])), bi)]
663 where n a = MN 0 a
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
1282mkPApp fc a f [] = f
1283mkPApp fc a f as = let rest = drop a as in
1284 appRest fc (PApp fc f (take a as)) rest
1285 where
1286 appRest fc f [] = f
1287 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1289-- Find 'static' argument positions
1290-- (the declared ones, plus any names in argument position in the declared
1291-- statics)
1292-- FIXME: It's possible that this really has to happen after elaboration
1294findStatics :: IState -> PTerm -> (PTerm, [Bool])
1295findStatics ist tm = trace (showImp Nothing True False tm) $
1296 let (ns, ss) = fs tm in
1297 runState (pos ns ss tm) []
1298 where fs (PPi p n t sc)
1299 | Static <- pstatic p
1300 = let (ns, ss) = fs sc in
1301 (namesIn [] ist t : ns, n : ss)
1302 | otherwise = let (ns, ss) = fs sc in
1303 (ns, ss)
1304 fs _ = ([], [])
1306 inOne n ns = length (filter id (map (elem n) ns)) == 1
1308 pos ns ss (PPi p n t sc)
1309 | elem n ss = do sc' <- pos ns ss sc
1310 spos <- get
1311 put (True : spos)
1312 return (PPi (p { pstatic = Static }) n t sc')
1313 | otherwise = do sc' <- pos ns ss sc
1314 spos <- get
1315 put (False : spos)
1316 return (PPi p n t sc')
1317 pos ns ss t = return t
1319-- Debugging/logging stuff
1321dumpDecls :: [PDecl] -> String
1322dumpDecls [] = ""
1323dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
1325dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
1326dumpDecl (PTy _ _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp Nothing True False t
1327dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
1328dumpDecl (PData _ _ _ _ d) = showDImp True d
1329dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
1330dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
1331dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
1332dumpDecl (PClass _ _ _ cs n ps ds)
1333 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
1334dumpDecl (PInstance _ _ cs n _ t _ ds)
1335 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
1336dumpDecl _ = "..."
1337-- dumpDecl (PImport i) = "import " ++ i
1339-- for 6.12/7 compatibility
1340data EitherErr a b = LeftErr a | RightOK b
1342instance Monad (EitherErr a) where
1343 return = RightOK
1345 (LeftErr e) >>= k = LeftErr e
1346 RightOK v >>= k = k v
1348toEither (LeftErr e) = Left e
1349toEither (RightOK ho) = Right ho
1351-- syntactic match of a against b, returning pair of variables in a
1352-- and what they match. Returns the pair that failed if not a match.
1354matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1355matchClause = matchClause' False
1357matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1358matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1359 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1361 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1362 fullApp x = x
1364 match' x y = match (fullApp x) (fullApp y)
1365 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
1366 | PConstant (I _) <- getTm x = match (getTm x) x'
1367 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
1368 | PConstant (I _) <- getTm x = match (getTm x) x'
1369 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
1370 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
1371 match (PApp _ f args) (PApp _ f' args')
1372 | length args == length args'
1373 = do mf <- match' f f'
1374 ms <- zipWithM matchArg args args'
1375 return (mf ++ concat ms)
1376-- match (PRef _ n) (PRef _ n') | n == n' = return []
1377-- | otherwise = Nothing
1378 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1379 match (PPatvar f n) xr = match (PRef f n) xr
1380 match xr (PPatvar f n) = match xr (PRef f n)
1381 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1382 match (PRef _ n) tm@(PRef _ n')
1383 | n == n' && not names &&
1384 (not (isConName n (tt_ctxt i)) || tm == Placeholder)
1385 = return [(n, tm)]
1386 | n == n' = return []
1387 match (PRef _ n) tm
1388 | not names && (not (isConName n (tt_ctxt i)) || tm == Placeholder)
1389 = return [(n, tm)]
1390 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1391 mr <- match' r r'
1392 return (ml ++ mr)
1393 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1394 = do ml <- match' l l'
1395 mr <- match' r r'
1396 return (ml ++ mr)
1397 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1398 mr <- match r r'
1399 return (ml ++ mr)
1400 match (PTyped l r) x = match l x
1401 match x (PTyped l r) = match x l
1402 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1403 mr <- match' r r'
1404 return (ml ++ mr)
1405 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1406 mt <- match' t t'
1407 mr <- match' r r'
1408 return (ml ++ mt ++ mr)
1409 match (PAlternative a as) (PAlternative a' as')
1410 = do ms <- zipWithM match' as as'
1411 return (concat ms)
1412 match a@(PAlternative _ as) b
1413 = do let ms = zipWith match' as (repeat b)
1414 case (rights (map toEither ms)) of
1415 (x: _) -> return x
1416 _ -> LeftErr (a, b)
1417 match (PCase _ _ _) _ = return [] -- lifted out
1418 match (PMetavar _) _ = return [] -- modified
1419 match (PInferRef _ _) _ = return [] -- modified
1420 match (PQuote _) _ = return []
1421 match (PProof _) _ = return []
1422 match (PTactics _) _ = return []
1423 match (PRefl _ _) (PRefl _ _) = return []
1424 match (PResolveTC _) (PResolveTC _) = return []
1425 match (PTrue _) (PTrue _) = return []
1426 match (PFalse _) (PFalse _) = return []
1427 match (PReturn _) (PReturn _) = return []
1428 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1429 ms <- match' s s'
1430 return (mt ++ ms)
1431 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1432 ms <- match' s s'
1433 return (mt ++ ms)
1434 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1435 mty <- match' ty ty'
1436 ms <- match' s s'
1437 return (mt ++ mty ++ ms)
1438 match (PHidden x) (PHidden y) = match' x y
1439 match (PUnifyLog x) y = match' x y
1440 match x (PUnifyLog y) = match' x y
1441 match (PNoImplicits x) y = match' x y
1442 match x (PNoImplicits y) = match' x y
1443 match Placeholder _ = return []
1444 match _ Placeholder = return []
1445 match (PResolveTC _) _ = return []
1446 match a b | a == b = return []
1447 | otherwise = LeftErr (a, b)
1449 checkRpts (RightOK ms) = check ms where
1450 check ((n,t):xs)
1451 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1452 then Left (t, t')
1453 else check xs
1454 check (_:xs) = check xs
1455 check [] = Right ms
1456 checkRpts (LeftErr x) = Left x
1458substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1459substMatches ms = substMatchesShadow ms []
1461substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1462substMatchesShadow [] shs t = t
1463substMatchesShadow ((n,tm):ns) shs t
1464 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1466substMatch :: Name -> PTerm -> PTerm -> PTerm
1467substMatch n = substMatchShadow n []
1469substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1470substMatchShadow n shs tm t = sm shs t where
1471 sm xs (PRef _ n') | n == n' = tm
1472 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1473 sm xs (PPi p x t sc)
1474 | x `elem` xs
1475 = let x' = nextName x in
1476 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1477 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1478 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1479 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1480 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1481 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1482 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1483 (fmap (sm xs) tm)
1484 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1485 sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)
1486 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)
1487 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1488 sm xs (PHidden x) = PHidden (sm xs x)
1489 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1490 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1491 sm xs x = x
1493 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1494 fullApp x = x
1496shadow :: Name -> Name -> PTerm -> PTerm
1497shadow n n' t = sm t where
1498 sm (PRef fc x) | n == x = PRef fc n'
1499 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1500 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1501 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1502 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1503 sm (PEq f x y) = PEq f (sm x) (sm y)
1504 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1505 sm (PTyped x y) = PTyped (sm x) (sm y)
1506 sm (PPair f x y) = PPair f (sm x) (sm y)
1507 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1508 sm (PAlternative a as) = PAlternative a (map sm as)
1509 sm (PHidden x) = PHidden (sm x)
1510 sm (PUnifyLog x) = PUnifyLog (sm x)
1511 sm (PNoImplicits x) = PNoImplicits (sm x)
1512 sm x = x