git.iko.soy/Idris-dev
on 86c9dec help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1485 lines 62 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, Type)] -> Idris ()
285addDeferred' nt ns
286 = do mapM_ (\(n, t) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns
287 i <- getIState
288 putIState $ i { idris_metavars = map fst ns ++ idris_metavars i }
289 where tidyNames used (Bind (MN i x) b sc)
290 = let n' = uniqueName (UN x) used in
291 Bind n' b $ tidyNames (n':used) sc
292 tidyNames used (Bind n b sc)
293 = let n' = uniqueName n used in
294 Bind n' b $ tidyNames (n':used) sc
295 tidyNames used b = b
297solveDeferred :: Name -> Idris ()
298solveDeferred n = do i <- getIState
299 putIState $ i { idris_metavars = idris_metavars i \\ [n] }
301ihPrintResult :: Handle -> String -> Idris ()
302ihPrintResult h s = do i <- getIState
303 case idris_outputmode i of
304 RawOutput -> case s of
305 "" -> return ()
306 s -> runIO $ hPutStrLn h s
307 IdeSlave n ->
308 let good = SexpList [SymbolAtom "ok", toSExp s] in
309 runIO $ hPutStrLn h $ convSExp "return" good n
311ihPrintError :: Handle -> String -> Idris ()
312ihPrintError h s = do i <- getIState
313 case idris_outputmode i of
314 RawOutput -> case s of
315 "" -> return ()
316 s -> runIO $ hPutStrLn h s
317 IdeSlave n ->
318 let good = SexpList [SymbolAtom "error", toSExp s] in
319 runIO . hPutStrLn h $ convSExp "return" good n
321ihputStrLn :: Handle -> String -> Idris ()
322ihputStrLn h s = do i <- getIState
323 case idris_outputmode i of
324 RawOutput -> runIO $ hPutStrLn h s
325 IdeSlave n ->
326 case span (/=':') s of
327 (fn, ':':rest) -> case span isDigit rest of
328 ([], ':':msg) -> write
329 ([], msg) -> write
330 (row, ':':rest') ->
331 case span isDigit rest' of
332 ([], msg) -> iWarn (FC fn (read row) 0) msg
333 (col, ':':msg) -> iWarn (FC fn (read row) (read col)) msg
334 _ -> write
335 where write = runIO . hPutStrLn h $ convSExp "write-string" s n
337iputStrLn = ihputStrLn stdout
338iPrintError = ihPrintError stdout
339iPrintResult = ihPrintResult stdout
341ideslavePutSExp :: SExpable a => String -> a -> Idris ()
342ideslavePutSExp cmd info = do i <- getIState
343 case idris_outputmode i of
344 IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
345 _ -> return ()
347-- this needs some typing magic and more structured output towards emacs
348iputGoal :: String -> Idris ()
349iputGoal s = do i <- getIState
350 case idris_outputmode i of
351 RawOutput -> runIO $ putStrLn s
352 IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" s n
354isetPrompt :: String -> Idris ()
355isetPrompt p = do i <- getIState
356 case idris_outputmode i of
357 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n
359iWarn :: FC -> String -> Idris ()
360iWarn fc err = do i <- getIState
361 case idris_outputmode i of
362 RawOutput -> runIO $ putStrLn (show fc ++ ":" ++ err)
363 IdeSlave n -> runIO . putStrLn $ convSExp "warning" (fc_fname fc, fc_line fc, err) n
365setLogLevel :: Int -> Idris ()
366setLogLevel l = do i <- getIState
367 let opts = idris_options i
368 let opt' = opts { opt_logLevel = l }
369 putIState $ i { idris_options = opt' }
371setCmdLine :: [Opt] -> Idris ()
372setCmdLine opts = do i <- getIState
373 let iopts = idris_options i
374 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
376getCmdLine :: Idris [Opt]
377getCmdLine = do i <- getIState
378 return (opt_cmdline (idris_options i))
380getDumpDefun :: Idris (Maybe FilePath)
381getDumpDefun = do i <- getIState
382 return $ findC (opt_cmdline (idris_options i))
383 where findC [] = Nothing
384 findC (DumpDefun x : _) = Just x
385 findC (_ : xs) = findC xs
387getDumpCases :: Idris (Maybe FilePath)
388getDumpCases = do i <- getIState
389 return $ findC (opt_cmdline (idris_options i))
390 where findC [] = Nothing
391 findC (DumpCases x : _) = Just x
392 findC (_ : xs) = findC xs
394logLevel :: Idris Int
395logLevel = do i <- getIState
396 return (opt_logLevel (idris_options i))
398setErrContext :: Bool -> Idris ()
399setErrContext t = do i <- getIState
400 let opts = idris_options i
401 let opt' = opts { opt_errContext = t }
402 putIState $ i { idris_options = opt' }
404errContext :: Idris Bool
405errContext = do i <- getIState
406 return (opt_errContext (idris_options i))
408useREPL :: Idris Bool
409useREPL = do i <- getIState
410 return (opt_repl (idris_options i))
412setREPL :: Bool -> Idris ()
413setREPL t = do i <- getIState
414 let opts = idris_options i
415 let opt' = opts { opt_repl = t }
416 putIState $ i { idris_options = opt' }
418setQuiet :: Bool -> Idris ()
419setQuiet q = do i <- getIState
420 let opts = idris_options i
421 let opt' = opts { opt_quiet = q }
422 putIState $ i { idris_options = opt' }
424getQuiet :: Idris Bool
425getQuiet = do i <- getIState
426 let opts = idris_options i
427 return (opt_quiet opts)
429setCodegen :: Codegen -> Idris ()
430setCodegen t = do i <- getIState
431 let opts = idris_options i
432 let opt' = opts { opt_codegen = t }
433 putIState $ i { idris_options = opt' }
435codegen :: Idris Codegen
436codegen = do i <- getIState
437 return (opt_codegen (idris_options i))
439setOutputTy :: OutputType -> Idris ()
440setOutputTy t = do i <- getIState
441 let opts = idris_options i
442 let opt' = opts { opt_outputTy = t }
443 putIState $ i { idris_options = opt' }
445outputTy :: Idris OutputType
446outputTy = do i <- getIState
447 return $ opt_outputTy $ idris_options i
449setIdeSlave :: Bool -> Idris ()
450setIdeSlave True = do i <- getIState
451 putIState $ i { idris_outputmode = (IdeSlave 0) }
452setIdeSlave False = return ()
454setTargetTriple :: String -> Idris ()
455setTargetTriple t = do i <- getIState
456 let opts = idris_options i
457 opt' = opts { opt_triple = t }
458 putIState $ i { idris_options = opt' }
460targetTriple :: Idris String
461targetTriple = do i <- getIState
462 return (opt_triple (idris_options i))
464setTargetCPU :: String -> Idris ()
465setTargetCPU t = do i <- getIState
466 let opts = idris_options i
467 opt' = opts { opt_cpu = t }
468 putIState $ i { idris_options = opt' }
470targetCPU :: Idris String
471targetCPU = do i <- getIState
472 return (opt_cpu (idris_options i))
474setOptLevel :: Word -> Idris ()
475setOptLevel t = do i <- getIState
476 let opts = idris_options i
477 opt' = opts { opt_optLevel = t }
478 putIState $ i { idris_options = opt' }
480optLevel :: Idris Word
481optLevel = do i <- getIState
482 return (opt_optLevel (idris_options i))
484verbose :: Idris Bool
485verbose = do i <- getIState
486 return (opt_verbose (idris_options i))
488setVerbose :: Bool -> Idris ()
489setVerbose t = do i <- getIState
490 let opts = idris_options i
491 let opt' = opts { opt_verbose = t }
492 putIState $ i { idris_options = opt' }
494typeInType :: Idris Bool
495typeInType = do i <- getIState
496 return (opt_typeintype (idris_options i))
498setTypeInType :: Bool -> Idris ()
499setTypeInType t = do i <- getIState
500 let opts = idris_options i
501 let opt' = opts { opt_typeintype = t }
502 putIState $ i { idris_options = opt' }
504coverage :: Idris Bool
505coverage = do i <- getIState
506 return (opt_coverage (idris_options i))
508setCoverage :: Bool -> Idris ()
509setCoverage t = do i <- getIState
510 let opts = idris_options i
511 let opt' = opts { opt_coverage = t }
512 putIState $ i { idris_options = opt' }
514setIBCSubDir :: FilePath -> Idris ()
515setIBCSubDir fp = do i <- getIState
516 let opts = idris_options i
517 let opt' = opts { opt_ibcsubdir = fp }
518 putIState $ i { idris_options = opt' }
520valIBCSubDir :: IState -> Idris FilePath
521valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
523addImportDir :: FilePath -> Idris ()
524addImportDir fp = do i <- getIState
525 let opts = idris_options i
526 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
527 putIState $ i { idris_options = opt' }
529setImportDirs :: [FilePath] -> Idris ()
530setImportDirs fps = do i <- getIState
531 let opts = idris_options i
532 let opt' = opts { opt_importdirs = fps }
533 putIState $ i { idris_options = opt' }
535allImportDirs :: Idris [FilePath]
536allImportDirs = do i <- getIState
537 let optdirs = opt_importdirs (idris_options i)
538 return ("." : reverse optdirs)
540colourise :: Idris Bool
541colourise = do i <- getIState
542 return $ idris_colourRepl i
544setColourise :: Bool -> Idris ()
545setColourise b = do i <- getIState
546 putIState $ i { idris_colourRepl = b }
548setOutH :: Handle -> Idris ()
549setOutH h = do i <- getIState
550 putIState $ i { idris_outh = h }
552impShow :: Idris Bool
553impShow = do i <- getIState
554 return (opt_showimp (idris_options i))
556setImpShow :: Bool -> Idris ()
557setImpShow t = do i <- getIState
558 let opts = idris_options i
559 let opt' = opts { opt_showimp = t }
560 putIState $ i { idris_options = opt' }
562setColour :: ColourType -> IdrisColour -> Idris ()
563setColour ct c = do i <- getIState
564 let newTheme = setColour' ct c (idris_colourTheme i)
565 putIState $ i { idris_colourTheme = newTheme }
566 where setColour' KeywordColour c t = t { keywordColour = c }
567 setColour' BoundVarColour c t = t { boundVarColour = c }
568 setColour' ImplicitColour c t = t { implicitColour = c }
569 setColour' FunctionColour c t = t { functionColour = c }
570 setColour' TypeColour c t = t { typeColour = c }
571 setColour' DataColour c t = t { dataColour = c }
572 setColour' PromptColour c t = t { promptColour = c }
574logLvl :: Int -> String -> Idris ()
575logLvl l str = do i <- getIState
576 let lvl = opt_logLevel (idris_options i)
577 when (lvl >= l)
578 $ do runIO (putStrLn str)
579 putIState $ i { idris_log = idris_log i ++ str ++ "\n" }
581cmdOptType :: Opt -> Idris Bool
582cmdOptType x = do i <- getIState
583 return $ x `elem` opt_cmdline (idris_options i)
585iLOG :: String -> Idris ()
586iLOG = logLvl 1
588noErrors :: Idris Bool
589noErrors = do i <- getIState
590 case errLine i of
591 Nothing -> return True
592 _ -> return False
594setTypeCase :: Bool -> Idris ()
595setTypeCase t = do i <- getIState
596 let opts = idris_options i
597 let opt' = opts { opt_typecase = t }
598 putIState $ i { idris_options = opt' }
601-- For inferring types of things
603bi = fileFC "builtin"
605inferTy = MN 0 "__Infer"
606inferCon = MN 0 "__infer"
607inferDecl = PDatadecl inferTy
608 PType
609 [("", inferCon, PPi impl (MN 0 "A") PType (
610 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
611 (PRef bi inferTy)), bi)]
613infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder True, pexp t]
614infP = P (TCon 6 0) inferTy (TType (UVal 0))
616getInferTerm, getInferType :: Term -> Term
617getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
618getInferTerm (App (App _ _) tm) = tm
619getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
621getInferType (Bind n b sc) = Bind n b $ getInferType sc
622getInferType (App (App _ ty) _) = ty
624-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
626primNames = [unitTy, unitCon,
627 falseTy, pairTy, pairCon,
628 eqTy, eqCon, inferTy, inferCon]
630unitTy = MN 0 "__Unit"
631unitCon = MN 0 "__II"
632unitDecl = PDatadecl unitTy PType
633 [("", unitCon, PRef bi unitTy, bi)]
635falseTy = MN 0 "__False"
636falseDecl = PDatadecl falseTy PType []
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
649eqTy = UN "="
650eqCon = UN "refl"
651eqDecl = PDatadecl eqTy (piBind [(n "a", PType), (n "b", PType),
652 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
653 PType)
654 [("", eqCon, PPi impl (n "a") PType (
655 PPi impl (n "x") (PRef bi (n "a"))
656 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder False,
657 pimp (n "b") Placeholder False,
658 pexp (PRef bi (n "x")),
659 pexp (PRef bi (n "x"))])), bi)]
660 where n a = MN 0 a
662-- Defined in builtins.idr
663sigmaTy = UN "Exists"
664existsCon = UN "Ex_intro"
666piBind :: [(Name, PTerm)] -> PTerm -> PTerm
667piBind = piBindp expl
669piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
670piBindp p [] t = t
671piBindp p ((n, ty):ns) t = PPi p n ty (piBind ns t)
673-- Dealing with parameters
675expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
676 [Name] -> -- all names
677 [Name] -> -- names with no declaration
678 PTerm -> PTerm
679expandParams dec ps ns infs tm = en tm
680 where
681 -- if we shadow a name (say in a lambda binding) that is used in a call to
682 -- a lifted function, we need access to both names - once in the scope of the
683 -- binding and once to call the lifted functions. So we'll explicitly shadow
684 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
685 -- but we didn't...)
687 mkShadow (UN n) = MN 0 n
688 mkShadow (MN i n) = MN (i+1) n
689 mkShadow (NS x s) = NS (mkShadow x) s
691 en (PLam n t s)
692 | n `elem` (map fst ps ++ ns)
693 = let n' = mkShadow n in
694 PLam n' (en t) (en (shadow n n' s))
695 | otherwise = PLam n (en t) (en s)
696 en (PPi p n t s)
697 | n `elem` (map fst ps ++ ns)
698 = let n' = mkShadow n in
699 PPi p n' (en t) (en (shadow n n' s))
700 | otherwise = PPi p n (en t) (en s)
701 en (PLet n ty v s)
702 | n `elem` (map fst ps ++ ns)
703 = let n' = mkShadow n in
704 PLet n' (en ty) (en v) (en (shadow n n' s))
705 | otherwise = PLet n (en ty) (en v) (en s)
706 -- FIXME: Should only do this in a type signature!
707 en (PDPair f (PRef f' n) t r)
708 | n `elem` (map fst ps ++ ns) && t /= Placeholder
709 = let n' = mkShadow n in
710 PDPair f (PRef f' n') (en t) (en (shadow n n' r))
711 en (PEq f l r) = PEq f (en l) (en r)
712 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
713 en (PTyped l r) = PTyped (en l) (en r)
714 en (PPair f l r) = PPair f (en l) (en r)
715 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
716 en (PAlternative a as) = PAlternative a (map en as)
717 en (PHidden t) = PHidden (en t)
718 en (PUnifyLog t) = PUnifyLog (en t)
719 en (PNoImplicits t) = PNoImplicits (en t)
720 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
721 en (PProof ts) = PProof (map (fmap en) ts)
722 en (PTactics ts) = PTactics (map (fmap en) ts)
724 en (PQuote (Var n))
725 | n `nselem` ns = PQuote (Var (dec n))
726 en (PApp fc (PInferRef fc' n) as)
727 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
728 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
729 en (PApp fc (PRef fc' n) as)
730 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
731 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
732 | n `nselem` ns = PApp fc (PRef fc' (dec n))
733 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
734 en (PAppBind fc (PRef fc' n) as)
735 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
736 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
737 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
738 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
739 en (PRef fc n)
740 | n `elem` infs = PApp fc (PInferRef fc (dec n))
741 (map (pexp . (PRef fc)) (map fst ps))
742 | n `nselem` ns = PApp fc (PRef fc (dec n))
743 (map (pexp . (PRef fc)) (map fst ps))
744 en (PInferRef fc n)
745 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
746 (map (pexp . (PRef fc)) (map fst ps))
747 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
748 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
749 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
750 en t = t
752 nselem x [] = False
753 nselem x (y : xs) | nseq x y = True
754 | otherwise = nselem x xs
756 nseq x y = nsroot x == nsroot y
758expandParamsD :: Bool -> -- True = RHS only
759 IState ->
760 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
761expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)
762 = if n `elem` ns && (not rhsonly)
763 then -- trace (show (n, expandParams dec ps ns ty)) $
764 PTy doc syn fc o (dec n) (piBind ps (expandParams dec ps ns [] ty))
765 else --trace (show (n, expandParams dec ps ns ty)) $
766 PTy doc syn fc o n (expandParams dec ps ns [] ty)
767expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
768 = if n `elem` ns && (not rhsonly)
769 then -- trace (show (n, expandParams dec ps ns ty)) $
770 PPostulate doc syn fc o (dec n) (piBind ps
771 (expandParams dec ps ns [] ty))
772 else --trace (show (n, expandParams dec ps ns ty)) $
773 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
774expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
775 = let n' = if n `elem` ns then dec n else n in
776 PClauses fc opts n' (map expandParamsC cs)
777 where
778 expandParamsC (PClause fc n lhs ws rhs ds)
779 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
780 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
781 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
782 n' = if n `elem` ns then dec n else n
783 -- names bound on the lhs should not be expanded on the rhs
784 ns' = removeBound lhs ns in
785 PClause fc n' lhs'
786 (map (expandParams dec ps'' ns' []) ws)
787 (expandParams dec ps'' ns' [] rhs)
788 (map (expandParamsD True ist dec ps'' ns') ds)
789 expandParamsC (PWith fc n lhs ws wval ds)
790 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
791 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
792 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
793 n' = if n `elem` ns then dec n else n
794 ns' = removeBound lhs ns in
795 PWith fc n' lhs'
796 (map (expandParams dec ps'' ns' []) ws)
797 (expandParams dec ps'' ns' [] wval)
798 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
799 updateps yn nm [] = []
800 updateps yn nm (((a, t), i):as)
801 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
802 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
804 removeBound lhs ns = ns \\ nub (bnames lhs)
806 bnames (PRef _ n) = [n]
807 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
808 bnames (PPair _ l r) = bnames l ++ bnames r
809 bnames (PDPair _ l Placeholder r) = bnames l ++ bnames r
810 bnames _ = []
812expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
813 = PData doc syn fc co (expandPData pd)
814 where
815 -- just do the type decl, leave constructors alone (parameters will be
816 -- added implicitly)
817 expandPData (PDatadecl n ty cons)
818 = if n `elem` ns
819 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
820 (map econ cons)
821 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
822 econ (doc, n, t, fc)
823 = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc)
824expandParamsD rhs ist dec ps ns (PParams f params pds)
825 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
826 (map (expandParamsD True ist dec ps ns) pds)
827-- (map (expandParamsD ist dec ps ns) pds)
828expandParamsD rhs ist dec ps ns (PMutual f pds)
829 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
830expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
831 = PClass doc info f
832 (map (expandParams dec ps ns []) cs)
833 n
834 (map (mapsnd (expandParams dec ps ns [])) params)
835 (map (expandParamsD rhs ist dec ps ns) decls)
836expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
837 = PInstance info f
838 (map (expandParams dec ps ns []) cs)
839 n
840 (map (expandParams dec ps ns []) params)
841 (expandParams dec ps ns [] ty)
842 cn
843 (map (expandParamsD rhs ist dec ps ns) decls)
844expandParamsD rhs ist dec ps ns d = d
846mapsnd f (x, t) = (x, f t)
848-- Calculate a priority for a type, for deciding elaboration order
849-- * if it's just a type variable or concrete type, do it early (0)
850-- * if there's only type variables and injective constructors, do it next (1)
851-- * if there's a function type, next (2)
852-- * finally, everything else (3)
854getPriority :: IState -> PTerm -> Int
855getPriority i tm = 1 -- pri tm
856 where
857 pri (PRef _ n) =
858 case lookupP n (tt_ctxt i) of
859 ((P (DCon _ _) _ _):_) -> 1
860 ((P (TCon _ _) _ _):_) -> 1
861 ((P Ref _ _):_) -> 1
862 [] -> 0 -- must be locally bound, if it's not an error...
863 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
864 pri (PTrue _) = 0
865 pri (PFalse _) = 0
866 pri (PRefl _ _) = 1
867 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
868 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
869 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
870 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
871 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
872 pri (PTyped l r) = pri l
873 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
874 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
875 pri (PAlternative a as) = maximum (map pri as)
876 pri (PConstant _) = 0
877 pri Placeholder = 1
878 pri _ = 3
880addStatics :: Name -> Term -> PTerm -> Idris ()
881addStatics n tm ptm =
882 do let (statics, dynamics) = initStatics tm ptm
883 let stnames = nub $ concatMap freeNames (map snd statics)
884 let dnames = nub $ concatMap freeNames (map snd dynamics)
885 when (not (null statics)) $
886 logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics
887 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
888 let statics' = nub $ map fst statics ++
889 filter (\x -> not (elem x dnames)) stnames
890 let stpos = staticList statics' tm
891 i <- getIState
892 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
893 addIBC (IBCStatic n)
894 where
895 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
896 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
897 if pstatic p == Static then ((n, ty) : static, dynamic)
898 else (static, (n, ty) : dynamic)
899 initStatics t pt = ([], [])
901 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
902 staticList _ _ = []
904-- Dealing with implicit arguments
906-- Add constraint bindings from using block
908addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
909addUsingConstraints syn fc t
910 = do ist <- get
911 let ns = namesIn [] ist t
912 let cs = getConstraints t -- check declared constraints
913 let addconsts = uconsts \\ cs
914 -- if all names in the arguments of addconsts appear in ns,
915 -- add the constraint implicitly
916 return (doAdd addconsts ns t)
917 where uconsts = filter uconst (using syn)
918 uconst (UConstraint _ _) = True
919 uconst _ = False
921 doAdd [] _ t = t
922 -- if all of args in ns, then add it
923 doAdd (UConstraint c args : cs) ns t
924 | all (\n -> elem n ns) args
925 = PPi (Constraint False Dynamic "") (MN 0 "cu")
926 (mkConst c args) (doAdd cs ns t)
927 | otherwise = doAdd cs ns t
929 mkConst c args = PApp fc (PRef fc c)
930 (map (\n -> PExp 0 False (PRef fc n) "") args)
932 getConstraints (PPi (Constraint _ _ _) _ c sc)
933 = getcapp c ++ getConstraints sc
934 getConstraints (PPi _ _ c sc) = getConstraints sc
935 getConstraints _ = []
937 getcapp (PApp _ (PRef _ c) args)
938 = do ns <- mapM getName args
939 return (UConstraint c ns)
940 getcapp _ = []
942 getName (PExp _ _ (PRef _ n) _) = return n
943 getName _ = []
945-- Add implicit Pi bindings for any names in the term which appear in an
946-- argument position.
948-- This has become a right mess already. Better redo it some time...
950implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
951implicit syn n ptm = implicit' syn [] n ptm
953implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
954implicit' syn ignore n ptm
955 = do i <- getIState
956 let (tm', impdata) = implicitise syn ignore i ptm
957-- let (tm'', spos) = findStatics i tm'
958 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
959 addIBC (IBCImp n)
960 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
961-- i <- get
962-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
963 return tm'
965implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
966implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
967 let (declimps, ns') = execState (imps True [] tm) ([], [])
968 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
969 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
970 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
971 if null ns
972 then (tm, reverse declimps)
973 else implicitise syn ignore ist (pibind uvars nsOrder tm)
974 where
975 uvars = map ipair (filter uimplicit (using syn))
976 pvars = syn_params syn
978 inUsing n = n `elem` map fst uvars
980 ipair (UImplicit x y) = (x, y)
981 uimplicit (UImplicit _ _) = True
982 uimplicit _ = False
984 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
985 | otherwise = x : dropAll xs ys
986 dropAll [] ys = []
988 imps top env (PApp _ f as)
989 = do (decls, ns) <- get
990 let isn = concatMap (namesIn uvars ist) (map getTm as)
991 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
992 imps top env (PPi (Imp l _ doc) n ty sc)
993 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
994 (decls , ns) <- get
995 put (PImp (getPriority ist ty) True l n ty doc : decls,
996 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
997 imps True (n:env) sc
998 imps top env (PPi (Exp l _ doc) n ty sc)
999 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1000 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1001 _ -> [])
1002 (decls, ns) <- get -- ignore decls in HO types
1003 put (PExp (getPriority ist ty) l ty doc : decls,
1004 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1005 imps True (n:env) sc
1006 imps top env (PPi (Constraint l _ doc) n ty sc)
1007 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1008 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1009 _ -> [])
1010 (decls, ns) <- get -- ignore decls in HO types
1011 put (PConstraint 10 l ty doc : decls,
1012 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1013 imps True (n:env) sc
1014 imps top env (PPi (TacImp l _ scr doc) n ty sc)
1015 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1016 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1017 _ -> [])
1018 (decls, ns) <- get -- ignore decls in HO types
1019 put (PTacImplicit 10 l n scr ty doc : decls,
1020 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1021 imps True (n:env) sc
1022 imps top env (PEq _ l r)
1023 = do (decls, ns) <- get
1024 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1025 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1026 imps top env (PRewrite _ l r _)
1027 = do (decls, ns) <- get
1028 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1029 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1030 imps top env (PTyped l r)
1031 = imps top env l
1032 imps top env (PPair _ l r)
1033 = do (decls, ns) <- get
1034 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1035 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1036 imps top env (PDPair _ (PRef _ n) t r)
1037 = do (decls, ns) <- get
1038 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1039 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1040 imps top env (PDPair _ l t r)
1041 = do (decls, ns) <- get
1042 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1043 namesIn uvars ist r
1044 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1045 imps top env (PAlternative a as)
1046 = do (decls, ns) <- get
1047 let isn = concatMap (namesIn uvars ist) as
1048 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1049 imps top env (PLam n ty sc)
1050 = do imps False env ty
1051 imps False (n:env) sc
1052 imps top env (PHidden tm) = imps False env tm
1053 imps top env (PUnifyLog tm) = imps False env tm
1054 imps top env (PNoImplicits tm) = imps False env tm
1055 imps top env _ = return ()
1057 pibind using [] sc = sc
1058 pibind using (n:ns) sc
1059 = case lookup n using of
1060 Just ty -> PPi (Imp False Dynamic "") n ty (pibind using ns sc)
1061 Nothing -> PPi (Imp False Dynamic "") n Placeholder
1062 (pibind using ns sc)
1064-- Add implicit arguments in function calls
1065addImplPat :: IState -> PTerm -> PTerm
1066addImplPat = addImpl' True [] []
1068addImplBound :: IState -> [Name] -> PTerm -> PTerm
1069addImplBound ist ns = addImpl' False ns [] ist
1071addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1072addImplBoundInf ist ns inf = addImpl' False ns inf ist
1074addImpl :: IState -> PTerm -> PTerm
1075addImpl = addImpl' False [] []
1077-- TODO: in patterns, don't add implicits to function names guarded by constructors
1078-- and *not* inside a PHidden
1080addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1081addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm
1082 where
1083 ai env (PRef fc f)
1084 | f `elem` infns = PInferRef fc f
1085 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f []
1086 ai env (PHidden (PRef fc f))
1087 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f []
1088 ai env (PEq fc l r) = let l' = ai env l
1089 r' = ai env r in
1090 PEq fc l' r'
1091 ai env (PRewrite fc l r g) = let l' = ai env l
1092 r' = ai env r
1093 g' = fmap (ai env) g in
1094 PRewrite fc l' r' g'
1095 ai env (PTyped l r) = let l' = ai env l
1096 r' = ai env r in
1097 PTyped l' r'
1098 ai env (PPair fc l r) = let l' = ai env l
1099 r' = ai env r in
1100 PPair fc l' r'
1101 ai env (PDPair fc l t r) = let l' = ai env l
1102 t' = ai env t
1103 r' = ai env r in
1104 PDPair fc l' t' r'
1105 ai env (PAlternative a as) = let as' = map (ai env) as in
1106 PAlternative a as'
1107 ai env (PApp fc (PInferRef _ f) as)
1108 = let as' = map (fmap (ai env)) as in
1109 PApp fc (PInferRef fc f) as'
1110 ai env (PApp fc ftm@(PRef _ f) as)
1111 | f `elem` infns = ai env (PApp fc (PInferRef fc f) as)
1112 | not (f `elem` map fst env)
1113 = let as' = map (fmap (ai env)) as in
1114 handleErr $ aiFn inpat False ist fc f as'
1115 | Just (Just ty) <- lookup f env
1116 = let as' = map (fmap (ai env)) as
1117 arity = getPArity ty in
1118 mkPApp fc arity ftm as'
1119 ai env (PApp fc f as) = let f' = ai env f
1120 as' = map (fmap (ai env)) as in
1121 mkPApp fc 1 f' as'
1122 ai env (PCase fc c os) = let c' = ai env c
1123 os' = map (pmap (ai env)) os in
1124 PCase fc c' os'
1125 ai env (PLam n ty sc) = let ty' = ai env ty
1126 sc' = ai ((n, Just ty):env) sc in
1127 PLam n ty' sc'
1128 ai env (PLet n ty val sc)
1129 = let ty' = ai env ty
1130 val' = ai env val
1131 sc' = ai ((n, Just ty):env) sc in
1132 PLet n ty' val' sc'
1133 ai env (PPi p n ty sc) = let ty' = ai env ty
1134 sc' = ai ((n, Just ty):env) sc in
1135 PPi p n ty' sc'
1136 ai env (PGoal fc r n sc) = let r' = ai env r
1137 sc' = ai ((n, Nothing):env) sc in
1138 PGoal fc r' n sc'
1139 ai env (PHidden tm) = PHidden (ai env tm)
1140 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
1141 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
1142 ai env (PRefl fc tm) = PRefl fc (ai env tm)
1143 ai env (PUnifyLog tm) = PUnifyLog (ai env tm)
1144 ai env (PNoImplicits tm) = PNoImplicits (ai env tm)
1145 ai env tm = tm
1147 handleErr (Left err) = PElabError err
1148 handleErr (Right x) = x
1150-- if in a pattern, and there are no arguments, and there's no possible
1151-- names with zero explicit arguments, don't add implicits.
1153aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
1154aiFn inpat True ist fc f []
1155 = case lookupDef f (tt_ctxt ist) of
1156 [] -> Right $ PPatvar fc f
1157 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1158 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1159 if (not (vname f) || tcname f
1160 || any (conCaf (tt_ctxt ist)) ialts)
1161-- any constructor alts || any allImp ialts))
1162 then aiFn inpat False ist fc f [] -- use it as a constructor
1163 else Right $ PPatvar fc f
1164 where imp (PExp _ _ _ _) = False
1165 imp _ = True
1166-- allImp [] = False
1167 allImp xs = all imp xs
1168 constructor (TyDecl (DCon _ _) _) = True
1169 constructor _ = False
1171 conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
1173 vname (UN n) = True -- non qualified
1174 vname _ = False
1176aiFn inpat expat ist fc f as
1177 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1178aiFn inpat expat ist fc f as
1179 -- This is where namespaces get resolved by adding PAlternative
1180 = case lookupCtxtName f (idris_implicits ist) of
1181 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1182 [] -> if f `elem` idris_metavars ist
1183 then Right $ PApp fc (PRef fc f) as
1184 else Right $ mkPApp fc (length as) (PRef fc f) as
1185 alts -> Right $
1186 PAlternative True $
1187 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1188 (insertImpl ns as)) alts
1189 where
1190 insertImpl :: [PArg] -> [PArg] -> [PArg]
1191 insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =
1192 PExp p l tm d : insertImpl ps given
1193 insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =
1194 PConstraint p l tm d : insertImpl ps given
1195 insertImpl (PConstraint p l ty d : ps) given =
1196 PConstraint p l (PResolveTC fc) d : insertImpl ps given
1197 insertImpl (PImp p _ l n ty d : ps) given =
1198 case find n given [] of
1199 Just (tm, given') -> PImp p False l n tm "" : insertImpl ps given'
1200 Nothing -> PImp p True l n Placeholder "" : insertImpl ps given
1201 insertImpl (PTacImplicit p l n sc ty d : ps) given =
1202 case find n given [] of
1203 Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'
1204 Nothing -> if inpat
1205 then PTacImplicit p l n sc Placeholder "" : insertImpl ps given
1206 else PTacImplicit p l n sc sc "" : insertImpl ps given
1207 insertImpl expected [] = []
1208 insertImpl _ given = given
1210 find n [] acc = Nothing
1211 find n (PImp _ _ _ n' t _ : gs) acc
1212 | n == n' = Just (t, reverse acc ++ gs)
1213 find n (PTacImplicit _ _ n' _ t _ : gs) acc
1214 | n == n' = Just (t, reverse acc ++ gs)
1215 find n (g : gs) acc = find n gs (g : acc)
1217-- replace non-linear occurrences with _
1218-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1219-- it is hard to get right!
1221stripLinear :: IState -> PTerm -> PTerm
1222stripLinear i tm = evalState (sl tm) [] where
1223 sl :: PTerm -> State [Name] PTerm
1224 sl (PRef fc f)
1225 | (_:_) <- lookupTy f (tt_ctxt i)
1226 = return $ PRef fc f
1227 | otherwise = do ns <- get
1228 if (f `elem` ns)
1229 then return Placeholder
1230 else do put (f : ns)
1231 return (PRef fc f)
1232 sl (PPatvar fc f)
1233 = do ns <- get
1234 if (f `elem` ns)
1235 then return Placeholder
1236 else do put (f : ns)
1237 return (PPatvar fc f)
1238 sl (PApp fc fn args) = do fn' <- sl fn
1239 args' <- mapM slA args
1240 return $ PApp fc fn' args'
1241 where slA (PImp p m l n t d) = do t' <- sl t
1242 return $ PImp p m l n t' d
1243 slA (PExp p l t d) = do t' <- sl t
1244 return $ PExp p l t' d
1245 slA (PConstraint p l t d)
1246 = do t' <- sl t
1247 return $ PConstraint p l t' d
1248 slA (PTacImplicit p l n sc t d)
1249 = do t' <- sl t
1250 return $ PTacImplicit p l n sc t' d
1251 sl x = return x
1253mkPApp fc a f [] = f
1254mkPApp fc a f as = let rest = drop a as in
1255 appRest fc (PApp fc f (take a as)) rest
1256 where
1257 appRest fc f [] = f
1258 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1260-- Find 'static' argument positions
1261-- (the declared ones, plus any names in argument position in the declared
1262-- statics)
1263-- FIXME: It's possible that this really has to happen after elaboration
1265findStatics :: IState -> PTerm -> (PTerm, [Bool])
1266findStatics ist tm = trace (showImp Nothing True False tm) $
1267 let (ns, ss) = fs tm in
1268 runState (pos ns ss tm) []
1269 where fs (PPi p n t sc)
1270 | Static <- pstatic p
1271 = let (ns, ss) = fs sc in
1272 (namesIn [] ist t : ns, n : ss)
1273 | otherwise = let (ns, ss) = fs sc in
1274 (ns, ss)
1275 fs _ = ([], [])
1277 inOne n ns = length (filter id (map (elem n) ns)) == 1
1279 pos ns ss (PPi p n t sc)
1280 | elem n ss = do sc' <- pos ns ss sc
1281 spos <- get
1282 put (True : spos)
1283 return (PPi (p { pstatic = Static }) n t sc')
1284 | otherwise = do sc' <- pos ns ss sc
1285 spos <- get
1286 put (False : spos)
1287 return (PPi p n t sc')
1288 pos ns ss t = return t
1290-- Debugging/logging stuff
1292dumpDecls :: [PDecl] -> String
1293dumpDecls [] = ""
1294dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
1296dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
1297dumpDecl (PTy _ _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp Nothing True False t
1298dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
1299dumpDecl (PData _ _ _ _ d) = showDImp True d
1300dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
1301dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
1302dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
1303dumpDecl (PClass _ _ _ cs n ps ds)
1304 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
1305dumpDecl (PInstance _ _ cs n _ t _ ds)
1306 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
1307dumpDecl _ = "..."
1308-- dumpDecl (PImport i) = "import " ++ i
1310-- for 6.12/7 compatibility
1311data EitherErr a b = LeftErr a | RightOK b
1313instance Monad (EitherErr a) where
1314 return = RightOK
1316 (LeftErr e) >>= k = LeftErr e
1317 RightOK v >>= k = k v
1319toEither (LeftErr e) = Left e
1320toEither (RightOK ho) = Right ho
1322-- syntactic match of a against b, returning pair of variables in a
1323-- and what they match. Returns the pair that failed if not a match.
1325matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1326matchClause = matchClause' False
1328matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1329matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1330 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1332 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1333 fullApp x = x
1335 match' x y = match (fullApp x) (fullApp y)
1336 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
1337 | PConstant (I _) <- getTm x = match (getTm x) x'
1338 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
1339 | PConstant (I _) <- getTm x = match (getTm x) x'
1340 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
1341 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
1342 match (PApp _ f args) (PApp _ f' args')
1343 | length args == length args'
1344 = do mf <- match' f f'
1345 ms <- zipWithM matchArg args args'
1346 return (mf ++ concat ms)
1347-- match (PRef _ n) (PRef _ n') | n == n' = return []
1348-- | otherwise = Nothing
1349 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1350 match (PPatvar f n) xr = match (PRef f n) xr
1351 match xr (PPatvar f n) = match xr (PRef f n)
1352 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1353 match (PRef _ n) tm@(PRef _ n')
1354 | n == n' && not names &&
1355 (not (isConName n (tt_ctxt i)) || tm == Placeholder)
1356 = return [(n, tm)]
1357 | n == n' = return []
1358 match (PRef _ n) tm
1359 | not names && (not (isConName n (tt_ctxt i)) || tm == Placeholder)
1360 = return [(n, tm)]
1361 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1362 mr <- match' r r'
1363 return (ml ++ mr)
1364 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1365 = do ml <- match' l l'
1366 mr <- match' r r'
1367 return (ml ++ mr)
1368 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1369 mr <- match r r'
1370 return (ml ++ mr)
1371 match (PTyped l r) x = match l x
1372 match x (PTyped l r) = match x l
1373 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1374 mr <- match' r r'
1375 return (ml ++ mr)
1376 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1377 mt <- match' t t'
1378 mr <- match' r r'
1379 return (ml ++ mt ++ mr)
1380 match (PAlternative a as) (PAlternative a' as')
1381 = do ms <- zipWithM match' as as'
1382 return (concat ms)
1383 match a@(PAlternative _ as) b
1384 = do let ms = zipWith match' as (repeat b)
1385 case (rights (map toEither ms)) of
1386 (x: _) -> return x
1387 _ -> LeftErr (a, b)
1388 match (PCase _ _ _) _ = return [] -- lifted out
1389 match (PMetavar _) _ = return [] -- modified
1390 match (PInferRef _ _) _ = return [] -- modified
1391 match (PQuote _) _ = return []
1392 match (PProof _) _ = return []
1393 match (PTactics _) _ = return []
1394 match (PRefl _ _) (PRefl _ _) = return []
1395 match (PResolveTC _) (PResolveTC _) = return []
1396 match (PTrue _) (PTrue _) = return []
1397 match (PFalse _) (PFalse _) = return []
1398 match (PReturn _) (PReturn _) = return []
1399 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1400 ms <- match' s s'
1401 return (mt ++ ms)
1402 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1403 ms <- match' s s'
1404 return (mt ++ ms)
1405 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1406 mty <- match' ty ty'
1407 ms <- match' s s'
1408 return (mt ++ mty ++ ms)
1409 match (PHidden x) (PHidden y) = match' x y
1410 match (PUnifyLog x) y = match' x y
1411 match x (PUnifyLog y) = match' x y
1412 match (PNoImplicits x) y = match' x y
1413 match x (PNoImplicits y) = match' x y
1414 match Placeholder _ = return []
1415 match _ Placeholder = return []
1416 match (PResolveTC _) _ = return []
1417 match a b | a == b = return []
1418 | otherwise = LeftErr (a, b)
1420 checkRpts (RightOK ms) = check ms where
1421 check ((n,t):xs)
1422 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1423 then Left (t, t')
1424 else check xs
1425 check (_:xs) = check xs
1426 check [] = Right ms
1427 checkRpts (LeftErr x) = Left x
1429substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1430substMatches ms = substMatchesShadow ms []
1432substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1433substMatchesShadow [] shs t = t
1434substMatchesShadow ((n,tm):ns) shs t
1435 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1437substMatch :: Name -> PTerm -> PTerm -> PTerm
1438substMatch n = substMatchShadow n []
1440substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1441substMatchShadow n shs tm t = sm shs t where
1442 sm xs (PRef _ n') | n == n' = tm
1443 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1444 sm xs (PPi p x t sc)
1445 | x `elem` xs
1446 = let x' = nextName x in
1447 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1448 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1449 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1450 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1451 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1452 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1453 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1454 (fmap (sm xs) tm)
1455 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1456 sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)
1457 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)
1458 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1459 sm xs (PHidden x) = PHidden (sm xs x)
1460 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1461 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1462 sm xs x = x
1464 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1465 fullApp x = x
1467shadow :: Name -> Name -> PTerm -> PTerm
1468shadow n n' t = sm t where
1469 sm (PRef fc x) | n == x = PRef fc n'
1470 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1471 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1472 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1473 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1474 sm (PEq f x y) = PEq f (sm x) (sm y)
1475 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1476 sm (PTyped x y) = PTyped (sm x) (sm y)
1477 sm (PPair f x y) = PPair f (sm x) (sm y)
1478 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1479 sm (PAlternative a as) = PAlternative a (map sm as)
1480 sm (PHidden x) = PHidden (sm x)
1481 sm (PUnifyLog x) = PUnifyLog (sm x)
1482 sm (PNoImplicits x) = PNoImplicits (sm x)
1483 sm x = x