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