git.iko.soy/Idris-dev
on 8c19e30 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1476 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
20import Control.Monad.State
22import Data.List
23import Data.Char
24import Data.Either
25import Data.Maybe
26import Data.Word (Word)
28import Debug.Trace
30import Control.Monad.Error (throwError, catchError)
31import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
33import Util.Pretty
34import Util.System
36getContext :: Idris Context
37getContext = do i <- getIState; return (tt_ctxt i)
39forCodegen :: Codegen -> [(Codegen, a)] -> [a]
40forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']
42getObjectFiles :: Codegen -> Idris [FilePath]
43getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
45addObjectFile :: Codegen -> FilePath -> Idris ()
46addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
48getLibs :: Codegen -> Idris [String]
49getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
51addLib :: Codegen -> String -> Idris ()
52addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
54getFlags :: Codegen -> Idris [String]
55getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
57addFlag :: Codegen -> String -> Idris ()
58addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
60addDyLib :: [String] -> Idris (Either DynamicLib String)
61addDyLib libs = do i <- getIState
62 let ls = idris_dynamic_libs i
63 case mapMaybe (findDyLib ls) libs of
64 x:_ -> return (Left x)
65 [] -> do
66 handle <- lift . lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) $ libs
67 case msum handle of
68 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
69 concat (intersperse "," libs) ++ "\"")
70 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
71 return (Left x)
72 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
73 findDyLib [] l = Nothing
74 findDyLib (lib:libs) l | l == lib_name lib = Just lib
75 | otherwise = findDyLib libs l
78addHdr :: Codegen -> String -> Idris ()
79addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
81addLangExt :: LanguageExt -> Idris ()
82addLangExt TypeProviders = do i <- getIState
83 putIState $ i {
84 idris_language_extensions = TypeProviders : idris_language_extensions i
85 }
86addLangExt ErrorReflection = do i <- getIState
87 putIState $ i {
88 idris_language_extensions = ErrorReflection : idris_language_extensions i
89 }
91addTrans :: (Term, Term) -> Idris ()
92addTrans t = do i <- getIState
93 putIState $ i { idris_transforms = t : idris_transforms i }
95totcheck :: (FC, Name) -> Idris ()
96totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
98clear_totcheck :: Idris ()
99clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
101setFlags :: Name -> [FnOpt] -> Idris ()
102setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
104setAccessibility :: Name -> Accessibility -> Idris ()
105setAccessibility n a
106 = do i <- getIState
107 let ctxt = setAccess n a (tt_ctxt i)
108 putIState $ i { tt_ctxt = ctxt }
110setTotality :: Name -> Totality -> Idris ()
111setTotality n a
112 = do i <- getIState
113 let ctxt = setTotal n a (tt_ctxt i)
114 putIState $ i { tt_ctxt = ctxt }
116getTotality :: Name -> Idris Totality
117getTotality n
118 = do i <- getIState
119 case lookupTotal n (tt_ctxt i) of
120 [t] -> return t
121 _ -> return (Total [])
123-- Get coercions which might return the required type
124getCoercionsTo :: IState -> Type -> [Name]
125getCoercionsTo i ty =
126 let cs = idris_coercions i
127 (fn,_) = unApply (getRetTy ty) in
128 findCoercions fn cs
129 where findCoercions t [] = []
130 findCoercions t (n : ns) =
131 let ps = case lookupTy n (tt_ctxt i) of
132 [ty] -> case unApply (getRetTy ty) of
133 (t', _) ->
134 if t == t' then [n] else []
135 _ -> [] in
136 ps ++ findCoercions t ns
138addToCG :: Name -> CGInfo -> Idris ()
139addToCG n cg
140 = do i <- getIState
141 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
143addCoercion :: Name -> Idris ()
144addCoercion n = do i <- getIState
145 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
147addDocStr :: Name -> String -> Idris ()
148addDocStr n doc
149 = do i <- getIState
150 putIState $ i { idris_docstrings = addDef n doc (idris_docstrings i) }
152addToCalledG :: Name -> [Name] -> Idris ()
153addToCalledG n ns = return () -- TODO
155-- Add a class instance function. Dodgy hack: Put integer instances first in the
156-- list so they are resolved by default.
157-- Dodgy hack 2: put constraint chasers (@@) last
159addInstance :: Bool -> Name -> Name -> Idris ()
160addInstance int n i
161 = do ist <- getIState
162 case lookupCtxt n (idris_classes ist) of
163 [CI a b c d ins] ->
164 do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)
165 putIState $ ist { idris_classes = cs }
166 _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)
167 putIState $ ist { idris_classes = cs }
168 where addI i ins | int = i : ins
169 | chaser n = ins ++ [i]
170 | otherwise = insI i ins
171 insI i [] = [i]
172 insI i (n : ns) | chaser n = i : n : ns
173 | otherwise = n : insI i ns
175 chaser (UN ('@':'@':_)) = True
176 chaser (NS n _) = chaser n
177 chaser _ = False
179addClass :: Name -> ClassInfo -> Idris ()
180addClass n i
181 = do ist <- getIState
182 let i' = case lookupCtxt n (idris_classes ist) of
183 [c] -> c { class_instances = class_instances i }
184 _ -> i
185 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
187addIBC :: IBCWrite -> Idris ()
188addIBC ibc@(IBCDef n)
189 = do i <- getIState
190 when (notDef (ibc_write i)) $
191 putIState $ i { ibc_write = ibc : ibc_write i }
192 where notDef [] = True
193 notDef (IBCDef n': is) | n == n' = False
194 notDef (_ : is) = notDef is
195addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
197clearIBC :: Idris ()
198clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
200getHdrs :: Codegen -> Idris [String]
201getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
203setErrLine :: Int -> Idris ()
204setErrLine x = do i <- getIState;
205 case (errLine i) of
206 Nothing -> putIState $ i { errLine = Just x }
207 Just _ -> return ()
209clearErr :: Idris ()
210clearErr = do i <- getIState
211 putIState $ i { errLine = Nothing }
213getSO :: Idris (Maybe String)
214getSO = do i <- getIState
215 return (compiled_so i)
217setSO :: Maybe String -> Idris ()
218setSO s = do i <- getIState
219 putIState $ (i { compiled_so = s })
221getIState :: Idris IState
222getIState = get
224putIState :: IState -> Idris ()
225putIState = put
227-- | A version of liftIO that puts errors into the exception type of the Idris monad
228runIO :: IO a -> Idris a
229runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
230-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
232getName :: Idris Int
233getName = do i <- getIState;
234 let idx = idris_name i;
235 putIState $ (i { idris_name = idx + 1 })
236 return idx
238addInternalName :: FilePath -> Int -> Name -> Int -> Idris ()
239addInternalName fp l n w
240 = do i <- getIState
241 putIState (i { idris_linename = ((fp, l), (n, w)) : idris_linename i })
243getInternalName :: FilePath -> Int -> Name -- ^ default name
244 -> Idris (Name, Int)
245getInternalName fp l n = do i <- getIState
246 case lookup (fp, l) (idris_linename i) of
247 Nothing -> return (n, 0)
248 Just n' -> return n'
250checkUndefined :: FC -> Name -> Idris ()
251checkUndefined fc n
252 = do i <- getContext
253 case lookupTy n i of
254 (_:_) -> fail $ show fc ++ ":" ++
255 show n ++ " already defined"
256 _ -> return ()
258isUndefined :: FC -> Name -> Idris Bool
259isUndefined fc n
260 = do i <- getContext
261 case lookupTy n i of
262 (_:_) -> return False
263 _ -> return True
265setContext :: Context -> Idris ()
266setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
268updateContext :: (Context -> Context) -> Idris ()
269updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
271addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
272addConstraints fc (v, cs)
273 = do i <- getIState
274 let ctxt = tt_ctxt i
275 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
276 next_tvar = v }
277 let ics = zip cs (repeat fc) ++ idris_constraints i
278 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
280addDeferred = addDeferred' Ref
281addDeferredTyCon = addDeferred' (TCon 0 0)
283addDeferred' :: NameType -> [(Name, Type)] -> Idris ()
284addDeferred' nt ns
285 = do mapM_ (\(n, t) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns
286 i <- getIState
287 putIState $ i { idris_metavars = map fst ns ++ idris_metavars i }
288 where tidyNames used (Bind (MN i x) b sc)
289 = let n' = uniqueName (UN x) used in
290 Bind n' b $ tidyNames (n':used) sc
291 tidyNames used (Bind n b sc)
292 = let n' = uniqueName n used in
293 Bind n' b $ tidyNames (n':used) sc
294 tidyNames used b = b
296solveDeferred :: Name -> Idris ()
297solveDeferred n = do i <- getIState
298 putIState $ i { idris_metavars = idris_metavars i \\ [n] }
300iPrintResult :: String -> Idris ()
301iPrintResult s = do i <- getIState
302 case idris_outputmode i of
303 RawOutput -> case s of
304 "" -> return ()
305 s -> runIO $ putStrLn s
306 IdeSlave n ->
307 let good = SexpList [SymbolAtom "ok", toSExp s] in
308 runIO $ putStrLn $ convSExp "return" good n
310iPrintError :: String -> Idris ()
311iPrintError s = do i <- getIState
312 case idris_outputmode i of
313 RawOutput -> case s of
314 "" -> return ()
315 s -> runIO $ putStrLn s
316 IdeSlave n ->
317 let good = SexpList [SymbolAtom "error", toSExp s] in
318 runIO . putStrLn $ convSExp "return" good n
320iputStrLn :: String -> Idris ()
321iputStrLn s = do i <- getIState
322 case idris_outputmode i of
323 RawOutput -> runIO $ putStrLn s
324 IdeSlave n ->
325 case span (/=':') s of
326 (fn, ':':rest) -> case span isDigit rest of
327 ([], ':':msg) -> write
328 ([], msg) -> write
329 (row, ':':rest') ->
330 case span isDigit rest' of
331 ([], msg) -> iWarn (FC fn (read row) 0) msg
332 (col, ':':msg) -> iWarn (FC fn (read row) (read col)) msg
333 _ -> write
334 where write = runIO . putStrLn $ convSExp "write-string" s n
336ideslavePutSExp :: SExpable a => String -> a -> Idris ()
337ideslavePutSExp cmd info = do i <- getIState
338 case idris_outputmode i of
339 IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
340 _ -> return ()
342-- this needs some typing magic and more structured output towards emacs
343iputGoal :: String -> Idris ()
344iputGoal s = do i <- getIState
345 case idris_outputmode i of
346 RawOutput -> runIO $ putStrLn s
347 IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" s n
349isetPrompt :: String -> Idris ()
350isetPrompt p = do i <- getIState
351 case idris_outputmode i of
352 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n
354iWarn :: FC -> String -> Idris ()
355iWarn fc err = do i <- getIState
356 case idris_outputmode i of
357 RawOutput -> runIO $ putStrLn (show fc ++ ":" ++ err)
358 IdeSlave n -> runIO . putStrLn $ convSExp "warning" (fc_fname fc, fc_line fc, err) n
360setLogLevel :: Int -> Idris ()
361setLogLevel l = do i <- getIState
362 let opts = idris_options i
363 let opt' = opts { opt_logLevel = l }
364 putIState $ i { idris_options = opt' }
366setCmdLine :: [Opt] -> Idris ()
367setCmdLine opts = do i <- getIState
368 let iopts = idris_options i
369 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
371getCmdLine :: Idris [Opt]
372getCmdLine = do i <- getIState
373 return (opt_cmdline (idris_options i))
375getDumpDefun :: Idris (Maybe FilePath)
376getDumpDefun = do i <- getIState
377 return $ findC (opt_cmdline (idris_options i))
378 where findC [] = Nothing
379 findC (DumpDefun x : _) = Just x
380 findC (_ : xs) = findC xs
382getDumpCases :: Idris (Maybe FilePath)
383getDumpCases = do i <- getIState
384 return $ findC (opt_cmdline (idris_options i))
385 where findC [] = Nothing
386 findC (DumpCases x : _) = Just x
387 findC (_ : xs) = findC xs
389logLevel :: Idris Int
390logLevel = do i <- getIState
391 return (opt_logLevel (idris_options i))
393setErrContext :: Bool -> Idris ()
394setErrContext t = do i <- getIState
395 let opts = idris_options i
396 let opt' = opts { opt_errContext = t }
397 putIState $ i { idris_options = opt' }
399errContext :: Idris Bool
400errContext = do i <- getIState
401 return (opt_errContext (idris_options i))
403useREPL :: Idris Bool
404useREPL = do i <- getIState
405 return (opt_repl (idris_options i))
407setREPL :: Bool -> Idris ()
408setREPL t = do i <- getIState
409 let opts = idris_options i
410 let opt' = opts { opt_repl = t }
411 putIState $ i { idris_options = opt' }
413setQuiet :: Bool -> Idris ()
414setQuiet q = do i <- getIState
415 let opts = idris_options i
416 let opt' = opts { opt_quiet = q }
417 putIState $ i { idris_options = opt' }
419getQuiet :: Idris Bool
420getQuiet = do i <- getIState
421 let opts = idris_options i
422 return (opt_quiet opts)
424setCodegen :: Codegen -> Idris ()
425setCodegen t = do i <- getIState
426 let opts = idris_options i
427 let opt' = opts { opt_codegen = t }
428 putIState $ i { idris_options = opt' }
430codegen :: Idris Codegen
431codegen = do i <- getIState
432 return (opt_codegen (idris_options i))
434setOutputTy :: OutputType -> Idris ()
435setOutputTy t = do i <- getIState
436 let opts = idris_options i
437 let opt' = opts { opt_outputTy = t }
438 putIState $ i { idris_options = opt' }
440outputTy :: Idris OutputType
441outputTy = do i <- getIState
442 return $ opt_outputTy $ idris_options i
444setIdeSlave :: Bool -> Idris ()
445setIdeSlave True = do i <- getIState
446 putIState $ i { idris_outputmode = (IdeSlave 0) }
447setIdeSlave False = return ()
449setTargetTriple :: String -> Idris ()
450setTargetTriple t = do i <- getIState
451 let opts = idris_options i
452 opt' = opts { opt_triple = t }
453 putIState $ i { idris_options = opt' }
455targetTriple :: Idris String
456targetTriple = do i <- getIState
457 return (opt_triple (idris_options i))
459setTargetCPU :: String -> Idris ()
460setTargetCPU t = do i <- getIState
461 let opts = idris_options i
462 opt' = opts { opt_cpu = t }
463 putIState $ i { idris_options = opt' }
465targetCPU :: Idris String
466targetCPU = do i <- getIState
467 return (opt_cpu (idris_options i))
469setOptLevel :: Word -> Idris ()
470setOptLevel t = do i <- getIState
471 let opts = idris_options i
472 opt' = opts { opt_optLevel = t }
473 putIState $ i { idris_options = opt' }
475optLevel :: Idris Word
476optLevel = do i <- getIState
477 return (opt_optLevel (idris_options i))
479verbose :: Idris Bool
480verbose = do i <- getIState
481 return (opt_verbose (idris_options i))
483setVerbose :: Bool -> Idris ()
484setVerbose t = do i <- getIState
485 let opts = idris_options i
486 let opt' = opts { opt_verbose = t }
487 putIState $ i { idris_options = opt' }
489typeInType :: Idris Bool
490typeInType = do i <- getIState
491 return (opt_typeintype (idris_options i))
493setTypeInType :: Bool -> Idris ()
494setTypeInType t = do i <- getIState
495 let opts = idris_options i
496 let opt' = opts { opt_typeintype = t }
497 putIState $ i { idris_options = opt' }
499coverage :: Idris Bool
500coverage = do i <- getIState
501 return (opt_coverage (idris_options i))
503setCoverage :: Bool -> Idris ()
504setCoverage t = do i <- getIState
505 let opts = idris_options i
506 let opt' = opts { opt_coverage = t }
507 putIState $ i { idris_options = opt' }
509setIBCSubDir :: FilePath -> Idris ()
510setIBCSubDir fp = do i <- getIState
511 let opts = idris_options i
512 let opt' = opts { opt_ibcsubdir = fp }
513 putIState $ i { idris_options = opt' }
515valIBCSubDir :: IState -> Idris FilePath
516valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
518addImportDir :: FilePath -> Idris ()
519addImportDir fp = do i <- getIState
520 let opts = idris_options i
521 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
522 putIState $ i { idris_options = opt' }
524setImportDirs :: [FilePath] -> Idris ()
525setImportDirs fps = do i <- getIState
526 let opts = idris_options i
527 let opt' = opts { opt_importdirs = fps }
528 putIState $ i { idris_options = opt' }
530allImportDirs :: Idris [FilePath]
531allImportDirs = do i <- getIState
532 let optdirs = opt_importdirs (idris_options i)
533 return ("." : reverse optdirs)
535colourise :: Idris Bool
536colourise = do i <- getIState
537 return $ idris_colourRepl i
539setColourise :: Bool -> Idris ()
540setColourise b = do i <- getIState
541 putIState $ i { idris_colourRepl = b }
543impShow :: Idris Bool
544impShow = do i <- getIState
545 return (opt_showimp (idris_options i))
547setImpShow :: Bool -> Idris ()
548setImpShow t = do i <- getIState
549 let opts = idris_options i
550 let opt' = opts { opt_showimp = t }
551 putIState $ i { idris_options = opt' }
553setColour :: ColourType -> IdrisColour -> Idris ()
554setColour ct c = do i <- getIState
555 let newTheme = setColour' ct c (idris_colourTheme i)
556 putIState $ i { idris_colourTheme = newTheme }
557 where setColour' KeywordColour c t = t { keywordColour = c }
558 setColour' BoundVarColour c t = t { boundVarColour = c }
559 setColour' ImplicitColour c t = t { implicitColour = c }
560 setColour' FunctionColour c t = t { functionColour = c }
561 setColour' TypeColour c t = t { typeColour = c }
562 setColour' DataColour c t = t { dataColour = c }
563 setColour' PromptColour c t = t { promptColour = c }
565logLvl :: Int -> String -> Idris ()
566logLvl l str = do i <- getIState
567 let lvl = opt_logLevel (idris_options i)
568 when (lvl >= l)
569 $ do runIO (putStrLn str)
570 putIState $ i { idris_log = idris_log i ++ str ++ "\n" }
572cmdOptType :: Opt -> Idris Bool
573cmdOptType x = do i <- getIState
574 return $ x `elem` opt_cmdline (idris_options i)
576iLOG :: String -> Idris ()
577iLOG = logLvl 1
579noErrors :: Idris Bool
580noErrors = do i <- getIState
581 case errLine i of
582 Nothing -> return True
583 _ -> return False
585setTypeCase :: Bool -> Idris ()
586setTypeCase t = do i <- getIState
587 let opts = idris_options i
588 let opt' = opts { opt_typecase = t }
589 putIState $ i { idris_options = opt' }
592-- For inferring types of things
594bi = fileFC "builtin"
596inferTy = MN 0 "__Infer"
597inferCon = MN 0 "__infer"
598inferDecl = PDatadecl inferTy
599 PType
600 [("", inferCon, PPi impl (MN 0 "A") PType (
601 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
602 (PRef bi inferTy)), bi)]
604infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder True, pexp t]
605infP = P (TCon 6 0) inferTy (TType (UVal 0))
607getInferTerm, getInferType :: Term -> Term
608getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
609getInferTerm (App (App _ _) tm) = tm
610getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
612getInferType (Bind n b sc) = Bind n b $ getInferType sc
613getInferType (App (App _ ty) _) = ty
615-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
617primNames = [unitTy, unitCon,
618 falseTy, pairTy, pairCon,
619 eqTy, eqCon, inferTy, inferCon]
621unitTy = MN 0 "__Unit"
622unitCon = MN 0 "__II"
623unitDecl = PDatadecl unitTy PType
624 [("", unitCon, PRef bi unitTy, bi)]
626falseTy = MN 0 "__False"
627falseDecl = PDatadecl falseTy PType []
629pairTy = MN 0 "__Pair"
630pairCon = MN 0 "__MkPair"
631pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
632 [("", pairCon, PPi impl (n "A") PType (
633 PPi impl (n "B") PType (
634 PPi expl (n "a") (PRef bi (n "A")) (
635 PPi expl (n "b") (PRef bi (n "B"))
636 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
637 pexp (PRef bi (n "B"))])))), bi)]
638 where n a = MN 0 a
640eqTy = UN "="
641eqCon = UN "refl"
642eqDecl = PDatadecl eqTy (piBind [(n "a", PType), (n "b", PType),
643 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
644 PType)
645 [("", eqCon, PPi impl (n "a") PType (
646 PPi impl (n "x") (PRef bi (n "a"))
647 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder False,
648 pimp (n "b") Placeholder False,
649 pexp (PRef bi (n "x")),
650 pexp (PRef bi (n "x"))])), bi)]
651 where n a = MN 0 a
653-- Defined in builtins.idr
654sigmaTy = UN "Exists"
655existsCon = UN "Ex_intro"
657piBind :: [(Name, PTerm)] -> PTerm -> PTerm
658piBind = piBindp expl
660piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
661piBindp p [] t = t
662piBindp p ((n, ty):ns) t = PPi p n ty (piBind ns t)
664-- Dealing with parameters
666expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
667 [Name] -> -- all names
668 [Name] -> -- names with no declaration
669 PTerm -> PTerm
670expandParams dec ps ns infs tm = en tm
671 where
672 -- if we shadow a name (say in a lambda binding) that is used in a call to
673 -- a lifted function, we need access to both names - once in the scope of the
674 -- binding and once to call the lifted functions. So we'll explicitly shadow
675 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
676 -- but we didn't...)
678 mkShadow (UN n) = MN 0 n
679 mkShadow (MN i n) = MN (i+1) n
680 mkShadow (NS x s) = NS (mkShadow x) s
682 en (PLam n t s)
683 | n `elem` (map fst ps ++ ns)
684 = let n' = mkShadow n in
685 PLam n' (en t) (en (shadow n n' s))
686 | otherwise = PLam n (en t) (en s)
687 en (PPi p n t s)
688 | n `elem` (map fst ps ++ ns)
689 = let n' = mkShadow n in
690 PPi p n' (en t) (en (shadow n n' s))
691 | otherwise = PPi p n (en t) (en s)
692 en (PLet n ty v s)
693 | n `elem` (map fst ps ++ ns)
694 = let n' = mkShadow n in
695 PLet n' (en ty) (en v) (en (shadow n n' s))
696 | otherwise = PLet n (en ty) (en v) (en s)
697 -- FIXME: Should only do this in a type signature!
698 en (PDPair f (PRef f' n) t r)
699 | n `elem` (map fst ps ++ ns) && t /= Placeholder
700 = let n' = mkShadow n in
701 PDPair f (PRef f' n') (en t) (en (shadow n n' r))
702 en (PEq f l r) = PEq f (en l) (en r)
703 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
704 en (PTyped l r) = PTyped (en l) (en r)
705 en (PPair f l r) = PPair f (en l) (en r)
706 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
707 en (PAlternative a as) = PAlternative a (map en as)
708 en (PHidden t) = PHidden (en t)
709 en (PUnifyLog t) = PUnifyLog (en t)
710 en (PNoImplicits t) = PNoImplicits (en t)
711 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
712 en (PProof ts) = PProof (map (fmap en) ts)
713 en (PTactics ts) = PTactics (map (fmap en) ts)
715 en (PQuote (Var n))
716 | n `nselem` ns = PQuote (Var (dec n))
717 en (PApp fc (PInferRef fc' n) as)
718 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
719 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
720 en (PApp fc (PRef fc' n) as)
721 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
722 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
723 | n `nselem` ns = PApp fc (PRef fc' (dec n))
724 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
725 en (PAppBind fc (PRef fc' n) as)
726 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
727 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
728 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
729 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
730 en (PRef fc n)
731 | n `elem` infs = PApp fc (PInferRef fc (dec n))
732 (map (pexp . (PRef fc)) (map fst ps))
733 | n `nselem` ns = PApp fc (PRef fc (dec n))
734 (map (pexp . (PRef fc)) (map fst ps))
735 en (PInferRef fc n)
736 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
737 (map (pexp . (PRef fc)) (map fst ps))
738 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
739 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
740 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
741 en t = t
743 nselem x [] = False
744 nselem x (y : xs) | nseq x y = True
745 | otherwise = nselem x xs
747 nseq x y = nsroot x == nsroot y
749expandParamsD :: Bool -> -- True = RHS only
750 IState ->
751 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
752expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)
753 = if n `elem` ns && (not rhsonly)
754 then -- trace (show (n, expandParams dec ps ns ty)) $
755 PTy doc syn fc o (dec n) (piBind ps (expandParams dec ps ns [] ty))
756 else --trace (show (n, expandParams dec ps ns ty)) $
757 PTy doc syn fc o n (expandParams dec ps ns [] ty)
758expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
759 = if n `elem` ns && (not rhsonly)
760 then -- trace (show (n, expandParams dec ps ns ty)) $
761 PPostulate doc syn fc o (dec n) (piBind ps
762 (expandParams dec ps ns [] ty))
763 else --trace (show (n, expandParams dec ps ns ty)) $
764 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
765expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
766 = let n' = if n `elem` ns then dec n else n in
767 PClauses fc opts n' (map expandParamsC cs)
768 where
769 expandParamsC (PClause fc n lhs ws rhs ds)
770 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
771 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
772 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
773 n' = if n `elem` ns then dec n else n
774 -- names bound on the lhs should not be expanded on the rhs
775 ns' = removeBound lhs ns in
776 PClause fc n' lhs'
777 (map (expandParams dec ps'' ns' []) ws)
778 (expandParams dec ps'' ns' [] rhs)
779 (map (expandParamsD True ist dec ps'' ns') ds)
780 expandParamsC (PWith fc n lhs ws wval ds)
781 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
782 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
783 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
784 n' = if n `elem` ns then dec n else n
785 ns' = removeBound lhs ns in
786 PWith fc n' lhs'
787 (map (expandParams dec ps'' ns' []) ws)
788 (expandParams dec ps'' ns' [] wval)
789 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
790 updateps yn nm [] = []
791 updateps yn nm (((a, t), i):as)
792 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
793 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
795 removeBound lhs ns = ns \\ nub (bnames lhs)
797 bnames (PRef _ n) = [n]
798 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
799 bnames (PPair _ l r) = bnames l ++ bnames r
800 bnames (PDPair _ l Placeholder r) = bnames l ++ bnames r
801 bnames _ = []
803expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
804 = PData doc syn fc co (expandPData pd)
805 where
806 -- just do the type decl, leave constructors alone (parameters will be
807 -- added implicitly)
808 expandPData (PDatadecl n ty cons)
809 = if n `elem` ns
810 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
811 (map econ cons)
812 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
813 econ (doc, n, t, fc)
814 = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc)
815expandParamsD rhs ist dec ps ns (PParams f params pds)
816 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
817 (map (expandParamsD True ist dec ps ns) pds)
818-- (map (expandParamsD ist dec ps ns) pds)
819expandParamsD rhs ist dec ps ns (PMutual f pds)
820 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
821expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
822 = PClass doc info f
823 (map (expandParams dec ps ns []) cs)
824 n
825 (map (mapsnd (expandParams dec ps ns [])) params)
826 (map (expandParamsD rhs ist dec ps ns) decls)
827expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
828 = PInstance info f
829 (map (expandParams dec ps ns []) cs)
830 n
831 (map (expandParams dec ps ns []) params)
832 (expandParams dec ps ns [] ty)
833 cn
834 (map (expandParamsD rhs ist dec ps ns) decls)
835expandParamsD rhs ist dec ps ns d = d
837mapsnd f (x, t) = (x, f t)
839-- Calculate a priority for a type, for deciding elaboration order
840-- * if it's just a type variable or concrete type, do it early (0)
841-- * if there's only type variables and injective constructors, do it next (1)
842-- * if there's a function type, next (2)
843-- * finally, everything else (3)
845getPriority :: IState -> PTerm -> Int
846getPriority i tm = 1 -- pri tm
847 where
848 pri (PRef _ n) =
849 case lookupP n (tt_ctxt i) of
850 ((P (DCon _ _) _ _):_) -> 1
851 ((P (TCon _ _) _ _):_) -> 1
852 ((P Ref _ _):_) -> 1
853 [] -> 0 -- must be locally bound, if it's not an error...
854 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
855 pri (PTrue _) = 0
856 pri (PFalse _) = 0
857 pri (PRefl _ _) = 1
858 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
859 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
860 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
861 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
862 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
863 pri (PTyped l r) = pri l
864 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
865 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
866 pri (PAlternative a as) = maximum (map pri as)
867 pri (PConstant _) = 0
868 pri Placeholder = 1
869 pri _ = 3
871addStatics :: Name -> Term -> PTerm -> Idris ()
872addStatics n tm ptm =
873 do let (statics, dynamics) = initStatics tm ptm
874 let stnames = nub $ concatMap freeNames (map snd statics)
875 let dnames = nub $ concatMap freeNames (map snd dynamics)
876 when (not (null statics)) $
877 logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics
878 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
879 let statics' = nub $ map fst statics ++
880 filter (\x -> not (elem x dnames)) stnames
881 let stpos = staticList statics' tm
882 i <- getIState
883 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
884 addIBC (IBCStatic n)
885 where
886 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
887 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
888 if pstatic p == Static then ((n, ty) : static, dynamic)
889 else (static, (n, ty) : dynamic)
890 initStatics t pt = ([], [])
892 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
893 staticList _ _ = []
895-- Dealing with implicit arguments
897-- Add constraint bindings from using block
899addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
900addUsingConstraints syn fc t
901 = do ist <- get
902 let ns = namesIn [] ist t
903 let cs = getConstraints t -- check declared constraints
904 let addconsts = uconsts \\ cs
905 -- if all names in the arguments of addconsts appear in ns,
906 -- add the constraint implicitly
907 return (doAdd addconsts ns t)
908 where uconsts = filter uconst (using syn)
909 uconst (UConstraint _ _) = True
910 uconst _ = False
912 doAdd [] _ t = t
913 -- if all of args in ns, then add it
914 doAdd (UConstraint c args : cs) ns t
915 | all (\n -> elem n ns) args
916 = PPi (Constraint False Dynamic "") (MN 0 "cu")
917 (mkConst c args) (doAdd cs ns t)
918 | otherwise = doAdd cs ns t
920 mkConst c args = PApp fc (PRef fc c)
921 (map (\n -> PExp 0 False (PRef fc n) "") args)
923 getConstraints (PPi (Constraint _ _ _) _ c sc)
924 = getcapp c ++ getConstraints sc
925 getConstraints (PPi _ _ c sc) = getConstraints sc
926 getConstraints _ = []
928 getcapp (PApp _ (PRef _ c) args)
929 = do ns <- mapM getName args
930 return (UConstraint c ns)
931 getcapp _ = []
933 getName (PExp _ _ (PRef _ n) _) = return n
934 getName _ = []
936-- Add implicit Pi bindings for any names in the term which appear in an
937-- argument position.
939-- This has become a right mess already. Better redo it some time...
941implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
942implicit syn n ptm = implicit' syn [] n ptm
944implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
945implicit' syn ignore n ptm
946 = do i <- getIState
947 let (tm', impdata) = implicitise syn ignore i ptm
948-- let (tm'', spos) = findStatics i tm'
949 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
950 addIBC (IBCImp n)
951 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
952-- i <- get
953-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
954 return tm'
956implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
957implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
958 let (declimps, ns') = execState (imps True [] tm) ([], [])
959 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
960 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
961 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
962 if null ns
963 then (tm, reverse declimps)
964 else implicitise syn ignore ist (pibind uvars nsOrder tm)
965 where
966 uvars = map ipair (filter uimplicit (using syn))
967 pvars = syn_params syn
969 inUsing n = n `elem` map fst uvars
971 ipair (UImplicit x y) = (x, y)
972 uimplicit (UImplicit _ _) = True
973 uimplicit _ = False
975 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
976 | otherwise = x : dropAll xs ys
977 dropAll [] ys = []
979 imps top env (PApp _ f as)
980 = do (decls, ns) <- get
981 let isn = concatMap (namesIn uvars ist) (map getTm as)
982 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
983 imps top env (PPi (Imp l _ doc) n ty sc)
984 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
985 (decls , ns) <- get
986 put (PImp (getPriority ist ty) True l n ty doc : decls,
987 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
988 imps True (n:env) sc
989 imps top env (PPi (Exp l _ doc) n ty sc)
990 = do let isn = nub (namesIn uvars ist ty ++ case sc of
991 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
992 _ -> [])
993 (decls, ns) <- get -- ignore decls in HO types
994 put (PExp (getPriority ist ty) l ty doc : decls,
995 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
996 imps True (n:env) sc
997 imps top env (PPi (Constraint l _ doc) n ty sc)
998 = do let isn = nub (namesIn uvars ist ty ++ case sc of
999 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1000 _ -> [])
1001 (decls, ns) <- get -- ignore decls in HO types
1002 put (PConstraint 10 l ty doc : decls,
1003 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1004 imps True (n:env) sc
1005 imps top env (PPi (TacImp l _ scr doc) n ty sc)
1006 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1007 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1008 _ -> [])
1009 (decls, ns) <- get -- ignore decls in HO types
1010 put (PTacImplicit 10 l n scr ty doc : decls,
1011 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1012 imps True (n:env) sc
1013 imps top env (PEq _ l r)
1014 = do (decls, ns) <- get
1015 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1016 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1017 imps top env (PRewrite _ l r _)
1018 = do (decls, ns) <- get
1019 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1020 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1021 imps top env (PTyped l r)
1022 = imps top env l
1023 imps top env (PPair _ l r)
1024 = do (decls, ns) <- get
1025 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1026 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1027 imps top env (PDPair _ (PRef _ n) t r)
1028 = do (decls, ns) <- get
1029 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1030 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1031 imps top env (PDPair _ l t r)
1032 = do (decls, ns) <- get
1033 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1034 namesIn uvars ist r
1035 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1036 imps top env (PAlternative a as)
1037 = do (decls, ns) <- get
1038 let isn = concatMap (namesIn uvars ist) as
1039 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1040 imps top env (PLam n ty sc)
1041 = do imps False env ty
1042 imps False (n:env) sc
1043 imps top env (PHidden tm) = imps False env tm
1044 imps top env (PUnifyLog tm) = imps False env tm
1045 imps top env (PNoImplicits tm) = imps False env tm
1046 imps top env _ = return ()
1048 pibind using [] sc = sc
1049 pibind using (n:ns) sc
1050 = case lookup n using of
1051 Just ty -> PPi (Imp False Dynamic "") n ty (pibind using ns sc)
1052 Nothing -> PPi (Imp False Dynamic "") n Placeholder
1053 (pibind using ns sc)
1055-- Add implicit arguments in function calls
1056addImplPat :: IState -> PTerm -> PTerm
1057addImplPat = addImpl' True [] []
1059addImplBound :: IState -> [Name] -> PTerm -> PTerm
1060addImplBound ist ns = addImpl' False ns [] ist
1062addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1063addImplBoundInf ist ns inf = addImpl' False ns inf ist
1065addImpl :: IState -> PTerm -> PTerm
1066addImpl = addImpl' False [] []
1068-- TODO: in patterns, don't add implicits to function names guarded by constructors
1069-- and *not* inside a PHidden
1071addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1072addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm
1073 where
1074 ai env (PRef fc f)
1075 | f `elem` infns = PInferRef fc f
1076 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f []
1077 ai env (PHidden (PRef fc f))
1078 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f []
1079 ai env (PEq fc l r) = let l' = ai env l
1080 r' = ai env r in
1081 PEq fc l' r'
1082 ai env (PRewrite fc l r g) = let l' = ai env l
1083 r' = ai env r
1084 g' = fmap (ai env) g in
1085 PRewrite fc l' r' g'
1086 ai env (PTyped l r) = let l' = ai env l
1087 r' = ai env r in
1088 PTyped l' r'
1089 ai env (PPair fc l r) = let l' = ai env l
1090 r' = ai env r in
1091 PPair fc l' r'
1092 ai env (PDPair fc l t r) = let l' = ai env l
1093 t' = ai env t
1094 r' = ai env r in
1095 PDPair fc l' t' r'
1096 ai env (PAlternative a as) = let as' = map (ai env) as in
1097 PAlternative a as'
1098 ai env (PApp fc (PInferRef _ f) as)
1099 = let as' = map (fmap (ai env)) as in
1100 PApp fc (PInferRef fc f) as'
1101 ai env (PApp fc ftm@(PRef _ f) as)
1102 | f `elem` infns = ai env (PApp fc (PInferRef fc f) as)
1103 | not (f `elem` map fst env)
1104 = let as' = map (fmap (ai env)) as in
1105 handleErr $ aiFn inpat False ist fc f as'
1106 | Just (Just ty) <- lookup f env
1107 = let as' = map (fmap (ai env)) as
1108 arity = getPArity ty in
1109 mkPApp fc arity ftm as'
1110 ai env (PApp fc f as) = let f' = ai env f
1111 as' = map (fmap (ai env)) as in
1112 mkPApp fc 1 f' as'
1113 ai env (PCase fc c os) = let c' = ai env c
1114 os' = map (pmap (ai env)) os in
1115 PCase fc c' os'
1116 ai env (PLam n ty sc) = let ty' = ai env ty
1117 sc' = ai ((n, Just ty):env) sc in
1118 PLam n ty' sc'
1119 ai env (PLet n ty val sc)
1120 = let ty' = ai env ty
1121 val' = ai env val
1122 sc' = ai ((n, Just ty):env) sc in
1123 PLet n ty' val' sc'
1124 ai env (PPi p n ty sc) = let ty' = ai env ty
1125 sc' = ai ((n, Just ty):env) sc in
1126 PPi p n ty' sc'
1127 ai env (PGoal fc r n sc) = let r' = ai env r
1128 sc' = ai ((n, Nothing):env) sc in
1129 PGoal fc r' n sc'
1130 ai env (PHidden tm) = PHidden (ai env tm)
1131 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
1132 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
1133 ai env (PRefl fc tm) = PRefl fc (ai env tm)
1134 ai env (PUnifyLog tm) = PUnifyLog (ai env tm)
1135 ai env (PNoImplicits tm) = PNoImplicits (ai env tm)
1136 ai env tm = tm
1138 handleErr (Left err) = PElabError err
1139 handleErr (Right x) = x
1141-- if in a pattern, and there are no arguments, and there's no possible
1142-- names with zero explicit arguments, don't add implicits.
1144aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
1145aiFn inpat True ist fc f []
1146 = case lookupDef f (tt_ctxt ist) of
1147 [] -> Right $ PPatvar fc f
1148 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1149 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1150 if (not (vname f) || tcname f
1151 || any (conCaf (tt_ctxt ist)) ialts)
1152-- any constructor alts || any allImp ialts))
1153 then aiFn inpat False ist fc f [] -- use it as a constructor
1154 else Right $ PPatvar fc f
1155 where imp (PExp _ _ _ _) = False
1156 imp _ = True
1157-- allImp [] = False
1158 allImp xs = all imp xs
1159 constructor (TyDecl (DCon _ _) _) = True
1160 constructor _ = False
1162 conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
1164 vname (UN n) = True -- non qualified
1165 vname _ = False
1167aiFn inpat expat ist fc f as
1168 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1169aiFn inpat expat ist fc f as
1170 -- This is where namespaces get resolved by adding PAlternative
1171 = case lookupCtxtName f (idris_implicits ist) of
1172 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1173 [] -> if f `elem` idris_metavars ist
1174 then Right $ PApp fc (PRef fc f) as
1175 else Right $ mkPApp fc (length as) (PRef fc f) as
1176 alts -> Right $
1177 PAlternative True $
1178 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1179 (insertImpl ns as)) alts
1180 where
1181 insertImpl :: [PArg] -> [PArg] -> [PArg]
1182 insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =
1183 PExp p l tm d : insertImpl ps given
1184 insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =
1185 PConstraint p l tm d : insertImpl ps given
1186 insertImpl (PConstraint p l ty d : ps) given =
1187 PConstraint p l (PResolveTC fc) d : insertImpl ps given
1188 insertImpl (PImp p _ l n ty d : ps) given =
1189 case find n given [] of
1190 Just (tm, given') -> PImp p False l n tm "" : insertImpl ps given'
1191 Nothing -> PImp p True l n Placeholder "" : insertImpl ps given
1192 insertImpl (PTacImplicit p l n sc ty d : ps) given =
1193 case find n given [] of
1194 Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'
1195 Nothing -> if inpat
1196 then PTacImplicit p l n sc Placeholder "" : insertImpl ps given
1197 else PTacImplicit p l n sc sc "" : insertImpl ps given
1198 insertImpl expected [] = []
1199 insertImpl _ given = given
1201 find n [] acc = Nothing
1202 find n (PImp _ _ _ n' t _ : gs) acc
1203 | n == n' = Just (t, reverse acc ++ gs)
1204 find n (PTacImplicit _ _ n' _ t _ : gs) acc
1205 | n == n' = Just (t, reverse acc ++ gs)
1206 find n (g : gs) acc = find n gs (g : acc)
1208-- replace non-linear occurrences with _
1209-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1210-- it is hard to get right!
1212stripLinear :: IState -> PTerm -> PTerm
1213stripLinear i tm = evalState (sl tm) [] where
1214 sl :: PTerm -> State [Name] PTerm
1215 sl (PRef fc f)
1216 | (_:_) <- lookupTy f (tt_ctxt i)
1217 = return $ PRef fc f
1218 | otherwise = do ns <- get
1219 if (f `elem` ns)
1220 then return Placeholder
1221 else do put (f : ns)
1222 return (PRef fc f)
1223 sl (PPatvar fc f)
1224 = do ns <- get
1225 if (f `elem` ns)
1226 then return Placeholder
1227 else do put (f : ns)
1228 return (PPatvar fc f)
1229 sl (PApp fc fn args) = do fn' <- sl fn
1230 args' <- mapM slA args
1231 return $ PApp fc fn' args'
1232 where slA (PImp p m l n t d) = do t' <- sl t
1233 return $ PImp p m l n t' d
1234 slA (PExp p l t d) = do t' <- sl t
1235 return $ PExp p l t' d
1236 slA (PConstraint p l t d)
1237 = do t' <- sl t
1238 return $ PConstraint p l t' d
1239 slA (PTacImplicit p l n sc t d)
1240 = do t' <- sl t
1241 return $ PTacImplicit p l n sc t' d
1242 sl x = return x
1244mkPApp fc a f [] = f
1245mkPApp fc a f as = let rest = drop a as in
1246 appRest fc (PApp fc f (take a as)) rest
1247 where
1248 appRest fc f [] = f
1249 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1251-- Find 'static' argument positions
1252-- (the declared ones, plus any names in argument position in the declared
1253-- statics)
1254-- FIXME: It's possible that this really has to happen after elaboration
1256findStatics :: IState -> PTerm -> (PTerm, [Bool])
1257findStatics ist tm = trace (showImp Nothing True False tm) $
1258 let (ns, ss) = fs tm in
1259 runState (pos ns ss tm) []
1260 where fs (PPi p n t sc)
1261 | Static <- pstatic p
1262 = let (ns, ss) = fs sc in
1263 (namesIn [] ist t : ns, n : ss)
1264 | otherwise = let (ns, ss) = fs sc in
1265 (ns, ss)
1266 fs _ = ([], [])
1268 inOne n ns = length (filter id (map (elem n) ns)) == 1
1270 pos ns ss (PPi p n t sc)
1271 | elem n ss = do sc' <- pos ns ss sc
1272 spos <- get
1273 put (True : spos)
1274 return (PPi (p { pstatic = Static }) n t sc')
1275 | otherwise = do sc' <- pos ns ss sc
1276 spos <- get
1277 put (False : spos)
1278 return (PPi p n t sc')
1279 pos ns ss t = return t
1281-- Debugging/logging stuff
1283dumpDecls :: [PDecl] -> String
1284dumpDecls [] = ""
1285dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
1287dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
1288dumpDecl (PTy _ _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp Nothing True False t
1289dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
1290dumpDecl (PData _ _ _ _ d) = showDImp True d
1291dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
1292dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
1293dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
1294dumpDecl (PClass _ _ _ cs n ps ds)
1295 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
1296dumpDecl (PInstance _ _ cs n _ t _ ds)
1297 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
1298dumpDecl _ = "..."
1299-- dumpDecl (PImport i) = "import " ++ i
1301-- for 6.12/7 compatibility
1302data EitherErr a b = LeftErr a | RightOK b
1304instance Monad (EitherErr a) where
1305 return = RightOK
1307 (LeftErr e) >>= k = LeftErr e
1308 RightOK v >>= k = k v
1310toEither (LeftErr e) = Left e
1311toEither (RightOK ho) = Right ho
1313-- syntactic match of a against b, returning pair of variables in a
1314-- and what they match. Returns the pair that failed if not a match.
1316matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1317matchClause = matchClause' False
1319matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1320matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1321 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1323 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1324 fullApp x = x
1326 match' x y = match (fullApp x) (fullApp y)
1327 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
1328 | PConstant (I _) <- getTm x = match (getTm x) x'
1329 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
1330 | PConstant (I _) <- getTm x = match (getTm x) x'
1331 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
1332 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
1333 match (PApp _ f args) (PApp _ f' args')
1334 | length args == length args'
1335 = do mf <- match' f f'
1336 ms <- zipWithM matchArg args args'
1337 return (mf ++ concat ms)
1338-- match (PRef _ n) (PRef _ n') | n == n' = return []
1339-- | otherwise = Nothing
1340 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1341 match (PPatvar f n) xr = match (PRef f n) xr
1342 match xr (PPatvar f n) = match xr (PRef f n)
1343 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1344 match (PRef _ n) tm@(PRef _ n')
1345 | n == n' && not names &&
1346 (not (isConName n (tt_ctxt i)) || tm == Placeholder)
1347 = return [(n, tm)]
1348 | n == n' = return []
1349 match (PRef _ n) tm
1350 | not names && (not (isConName n (tt_ctxt i)) || tm == Placeholder)
1351 = return [(n, tm)]
1352 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1353 mr <- match' r r'
1354 return (ml ++ mr)
1355 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1356 = do ml <- match' l l'
1357 mr <- match' r r'
1358 return (ml ++ mr)
1359 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1360 mr <- match r r'
1361 return (ml ++ mr)
1362 match (PTyped l r) x = match l x
1363 match x (PTyped l r) = match x l
1364 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1365 mr <- match' r r'
1366 return (ml ++ mr)
1367 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1368 mt <- match' t t'
1369 mr <- match' r r'
1370 return (ml ++ mt ++ mr)
1371 match (PAlternative a as) (PAlternative a' as')
1372 = do ms <- zipWithM match' as as'
1373 return (concat ms)
1374 match a@(PAlternative _ as) b
1375 = do let ms = zipWith match' as (repeat b)
1376 case (rights (map toEither ms)) of
1377 (x: _) -> return x
1378 _ -> LeftErr (a, b)
1379 match (PCase _ _ _) _ = return [] -- lifted out
1380 match (PMetavar _) _ = return [] -- modified
1381 match (PInferRef _ _) _ = return [] -- modified
1382 match (PQuote _) _ = return []
1383 match (PProof _) _ = return []
1384 match (PTactics _) _ = return []
1385 match (PRefl _ _) (PRefl _ _) = return []
1386 match (PResolveTC _) (PResolveTC _) = return []
1387 match (PTrue _) (PTrue _) = return []
1388 match (PFalse _) (PFalse _) = return []
1389 match (PReturn _) (PReturn _) = return []
1390 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1391 ms <- match' s s'
1392 return (mt ++ ms)
1393 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1394 ms <- match' s s'
1395 return (mt ++ ms)
1396 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1397 mty <- match' ty ty'
1398 ms <- match' s s'
1399 return (mt ++ mty ++ ms)
1400 match (PHidden x) (PHidden y) = match' x y
1401 match (PUnifyLog x) y = match' x y
1402 match x (PUnifyLog y) = match' x y
1403 match (PNoImplicits x) y = match' x y
1404 match x (PNoImplicits y) = match' x y
1405 match Placeholder _ = return []
1406 match _ Placeholder = return []
1407 match (PResolveTC _) _ = return []
1408 match a b | a == b = return []
1409 | otherwise = LeftErr (a, b)
1411 checkRpts (RightOK ms) = check ms where
1412 check ((n,t):xs)
1413 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1414 then Left (t, t')
1415 else check xs
1416 check (_:xs) = check xs
1417 check [] = Right ms
1418 checkRpts (LeftErr x) = Left x
1420substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1421substMatches ms = substMatchesShadow ms []
1423substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1424substMatchesShadow [] shs t = t
1425substMatchesShadow ((n,tm):ns) shs t
1426 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1428substMatch :: Name -> PTerm -> PTerm -> PTerm
1429substMatch n = substMatchShadow n []
1431substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1432substMatchShadow n shs tm t = sm shs t where
1433 sm xs (PRef _ n') | n == n' = tm
1434 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1435 sm xs (PPi p x t sc)
1436 | x `elem` xs
1437 = let x' = nextName x in
1438 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1439 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1440 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1441 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1442 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1443 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1444 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1445 (fmap (sm xs) tm)
1446 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1447 sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)
1448 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)
1449 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1450 sm xs (PHidden x) = PHidden (sm xs x)
1451 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1452 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1453 sm xs x = x
1455 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1456 fullApp x = x
1458shadow :: Name -> Name -> PTerm -> PTerm
1459shadow n n' t = sm t where
1460 sm (PRef fc x) | n == x = PRef fc n'
1461 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1462 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1463 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1464 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1465 sm (PEq f x y) = PEq f (sm x) (sm y)
1466 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1467 sm (PTyped x y) = PTyped (sm x) (sm y)
1468 sm (PPair f x y) = PPair f (sm x) (sm y)
1469 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1470 sm (PAlternative a as) = PAlternative a (map sm as)
1471 sm (PHidden x) = PHidden (sm x)
1472 sm (PUnifyLog x) = PUnifyLog (sm x)
1473 sm (PNoImplicits x) = PNoImplicits (sm x)
1474 sm x = x