git.iko.soy/Idris-dev
on 5afcedb help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1561 lines 65 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances, PatternGuards #-}
4module Idris.AbsSyntax(module Idris.AbsSyntax, module Idris.AbsSyntaxTree) where
6import Core.TT
7import Core.Evaluate
8import Core.Elaborate hiding (Tactic(..))
9import Core.Typecheck
10import Idris.AbsSyntaxTree
11import Idris.Colours
12import Idris.IdeSlave
13import IRTS.CodegenCommon
14import Util.DynamicLinker
16import Paths_idris
18import System.Console.Haskeline
19import System.IO
21import Control.Monad.State
23import Data.List
24import Data.Char
25import Data.Either
26import Data.Maybe
27import Data.Word (Word)
29import Debug.Trace
31import Control.Monad.Error (throwError, catchError)
32import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
34import Util.Pretty
35import Util.System
37getContext :: Idris Context
38getContext = do i <- getIState; return (tt_ctxt i)
40forCodegen :: Codegen -> [(Codegen, a)] -> [a]
41forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']
43getObjectFiles :: Codegen -> Idris [FilePath]
44getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
46addObjectFile :: Codegen -> FilePath -> Idris ()
47addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
49getLibs :: Codegen -> Idris [String]
50getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
52addLib :: Codegen -> String -> Idris ()
53addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
55getFlags :: Codegen -> Idris [String]
56getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
58addFlag :: Codegen -> String -> Idris ()
59addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
61addDyLib :: [String] -> Idris (Either DynamicLib String)
62addDyLib libs = do i <- getIState
63 let ls = idris_dynamic_libs i
64 case mapMaybe (findDyLib ls) libs of
65 x:_ -> return (Left x)
66 [] -> do
67 handle <- lift . lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) $ libs
68 case msum handle of
69 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
70 concat (intersperse "," libs) ++ "\"")
71 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
72 return (Left x)
73 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
74 findDyLib [] l = Nothing
75 findDyLib (lib:libs) l | l == lib_name lib = Just lib
76 | otherwise = findDyLib libs l
79addHdr :: Codegen -> String -> Idris ()
80addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
82addLangExt :: LanguageExt -> Idris ()
83addLangExt TypeProviders = do i <- getIState
84 putIState $ i {
85 idris_language_extensions = TypeProviders : idris_language_extensions i
86 }
87addLangExt ErrorReflection = do i <- getIState
88 putIState $ i {
89 idris_language_extensions = ErrorReflection : idris_language_extensions i
90 }
92addTrans :: (Term, Term) -> Idris ()
93addTrans t = do i <- getIState
94 putIState $ i { idris_transforms = t : idris_transforms i }
96totcheck :: (FC, Name) -> Idris ()
97totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
99defer_totcheck :: (FC, Name) -> Idris ()
100defer_totcheck n
101 = do i <- getIState;
102 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
104clear_totcheck :: Idris ()
105clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
107setFlags :: Name -> [FnOpt] -> Idris ()
108setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
110setAccessibility :: Name -> Accessibility -> Idris ()
111setAccessibility n a
112 = do i <- getIState
113 let ctxt = setAccess n a (tt_ctxt i)
114 putIState $ i { tt_ctxt = ctxt }
116setTotality :: Name -> Totality -> Idris ()
117setTotality n a
118 = do i <- getIState
119 let ctxt = setTotal n a (tt_ctxt i)
120 putIState $ i { tt_ctxt = ctxt }
122getTotality :: Name -> Idris Totality
123getTotality n
124 = do i <- getIState
125 case lookupTotal n (tt_ctxt i) of
126 [t] -> return t
127 _ -> return (Total [])
129-- Get coercions which might return the required type
130getCoercionsTo :: IState -> Type -> [Name]
131getCoercionsTo i ty =
132 let cs = idris_coercions i
133 (fn,_) = unApply (getRetTy ty) in
134 findCoercions fn cs
135 where findCoercions t [] = []
136 findCoercions t (n : ns) =
137 let ps = case lookupTy n (tt_ctxt i) of
138 [ty] -> case unApply (getRetTy ty) of
139 (t', _) ->
140 if t == t' then [n] else []
141 _ -> [] in
142 ps ++ findCoercions t ns
144addToCG :: Name -> CGInfo -> Idris ()
145addToCG n cg
146 = do i <- getIState
147 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
149-- Trace all the names in a call graph starting at the given name
150getAllNames :: Name -> Idris [Name]
151getAllNames n = allNames [] n
153allNames :: [Name] -> Name -> Idris [Name]
154allNames ns n | n `elem` ns = return []
155allNames ns n = do i <- getIState
156 case lookupCtxtExact n (idris_callgraph i) of
157 [ns'] -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
158 return (nub (n : concat more))
159 _ -> return [n]
161addCoercion :: Name -> Idris ()
162addCoercion n = do i <- getIState
163 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
165addDocStr :: Name -> String -> Idris ()
166addDocStr n doc
167 = do i <- getIState
168 putIState $ i { idris_docstrings = addDef n doc (idris_docstrings i) }
170addToCalledG :: Name -> [Name] -> Idris ()
171addToCalledG n ns = return () -- TODO
173-- Add a class instance function. Dodgy hack: Put integer instances first in the
174-- list so they are resolved by default.
175-- Dodgy hack 2: put constraint chasers (@@) last
177addInstance :: Bool -> Name -> Name -> Idris ()
178addInstance int n i
179 = do ist <- getIState
180 case lookupCtxt n (idris_classes ist) of
181 [CI a b c d ins] ->
182 do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)
183 putIState $ ist { idris_classes = cs }
184 _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)
185 putIState $ ist { idris_classes = cs }
186 where addI i ins | int = i : ins
187 | chaser n = ins ++ [i]
188 | otherwise = insI i ins
189 insI i [] = [i]
190 insI i (n : ns) | chaser n = i : n : ns
191 | otherwise = n : insI i ns
193 chaser (UN ('@':'@':_)) = True
194 chaser (NS n _) = chaser n
195 chaser _ = False
197addClass :: Name -> ClassInfo -> Idris ()
198addClass n i
199 = do ist <- getIState
200 let i' = case lookupCtxt n (idris_classes ist) of
201 [c] -> c { class_instances = class_instances i }
202 _ -> i
203 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
205addIBC :: IBCWrite -> Idris ()
206addIBC ibc@(IBCDef n)
207 = do i <- getIState
208 when (notDef (ibc_write i)) $
209 putIState $ i { ibc_write = ibc : ibc_write i }
210 where notDef [] = True
211 notDef (IBCDef n': is) | n == n' = False
212 notDef (_ : is) = notDef is
213addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
215clearIBC :: Idris ()
216clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
218getHdrs :: Codegen -> Idris [String]
219getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
221setErrLine :: Int -> Idris ()
222setErrLine x = do i <- getIState;
223 case (errLine i) of
224 Nothing -> putIState $ i { errLine = Just x }
225 Just _ -> return ()
227clearErr :: Idris ()
228clearErr = do i <- getIState
229 putIState $ i { errLine = Nothing }
231getSO :: Idris (Maybe String)
232getSO = do i <- getIState
233 return (compiled_so i)
235setSO :: Maybe String -> Idris ()
236setSO s = do i <- getIState
237 putIState $ (i { compiled_so = s })
239getIState :: Idris IState
240getIState = get
242putIState :: IState -> Idris ()
243putIState = put
245-- | A version of liftIO that puts errors into the exception type of the Idris monad
246runIO :: IO a -> Idris a
247runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
248-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
250getName :: Idris Int
251getName = do i <- getIState;
252 let idx = idris_name i;
253 putIState $ (i { idris_name = idx + 1 })
254 return idx
256addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
257addInternalApp fp l t
258 = do i <- getIState
259 putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })
261getInternalApp :: FilePath -> Int -> Idris PTerm
262getInternalApp fp l = do i <- getIState
263 case lookup (fp, l) (idris_lineapps i) of
264 Just n' -> return n'
265 Nothing -> return Placeholder
266 -- TODO: What if it's not there?
268checkUndefined :: FC -> Name -> Idris ()
269checkUndefined fc n
270 = do i <- getContext
271 case lookupTy n i of
272 (_:_) -> fail $ show fc ++ ":" ++
273 show n ++ " already defined"
274 _ -> return ()
276isUndefined :: FC -> Name -> Idris Bool
277isUndefined fc n
278 = do i <- getContext
279 case lookupTy n i of
280 (_:_) -> return False
281 _ -> return True
283setContext :: Context -> Idris ()
284setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
286updateContext :: (Context -> Context) -> Idris ()
287updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
289addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
290addConstraints fc (v, cs)
291 = do i <- getIState
292 let ctxt = tt_ctxt i
293 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
294 next_tvar = v }
295 let ics = zip cs (repeat fc) ++ idris_constraints i
296 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
298addDeferred = addDeferred' Ref
299addDeferredTyCon = addDeferred' (TCon 0 0)
301addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
302addDeferred' nt ns
303 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns
304 i <- getIState
305 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
306 idris_metavars i }
307 where tidyNames used (Bind (MN i x) b sc)
308 = let n' = uniqueName (UN x) used in
309 Bind n' b $ tidyNames (n':used) sc
310 tidyNames used (Bind n b sc)
311 = let n' = uniqueName n used in
312 Bind n' b $ tidyNames (n':used) sc
313 tidyNames used b = b
315solveDeferred :: Name -> Idris ()
316solveDeferred n = do i <- getIState
317 putIState $ i { idris_metavars =
318 filter (\(n', _) -> n/=n')
319 (idris_metavars i) }
321ihPrintResult :: Handle -> String -> Idris ()
322ihPrintResult h s = do i <- getIState
323 case idris_outputmode i of
324 RawOutput -> case s of
325 "" -> return ()
326 s -> runIO $ hPutStrLn h s
327 IdeSlave n ->
328 let good = SexpList [SymbolAtom "ok", toSExp s] in
329 runIO $ hPutStrLn h $ convSExp "return" good n
331ihPrintError :: Handle -> String -> Idris ()
332ihPrintError h s = do i <- getIState
333 case idris_outputmode i of
334 RawOutput -> case s of
335 "" -> return ()
336 s -> runIO $ hPutStrLn h s
337 IdeSlave n ->
338 let good = SexpList [SymbolAtom "error", toSExp s] in
339 runIO . hPutStrLn h $ convSExp "return" good n
341ihputStrLn :: Handle -> String -> Idris ()
342ihputStrLn h s = do i <- getIState
343 case idris_outputmode i of
344 RawOutput -> runIO $ hPutStrLn h s
345 IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n
347iputStrLn = ihputStrLn stdout
348iPrintError = ihPrintError stdout
349iPrintResult = ihPrintResult stdout
350iWarn = ihWarn stdout
352ideslavePutSExp :: SExpable a => String -> a -> Idris ()
353ideslavePutSExp cmd info = do i <- getIState
354 case idris_outputmode i of
355 IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
356 _ -> return ()
358-- this needs some typing magic and more structured output towards emacs
359iputGoal :: String -> Idris ()
360iputGoal s = do i <- getIState
361 case idris_outputmode i of
362 RawOutput -> runIO $ putStrLn s
363 IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" s n
365isetPrompt :: String -> Idris ()
366isetPrompt p = do i <- getIState
367 case idris_outputmode i of
368 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n
370ihWarn :: Handle -> FC -> String -> Idris ()
371ihWarn h fc err = do i <- getIState
372 case idris_outputmode i of
373 RawOutput -> runIO $ hPutStrLn h (show fc ++ ":" ++ err)
374 IdeSlave n -> runIO $ hPutStrLn h $ convSExp "warning" (fc_fname fc, fc_line fc, err) n
376setLogLevel :: Int -> Idris ()
377setLogLevel l = do i <- getIState
378 let opts = idris_options i
379 let opt' = opts { opt_logLevel = l }
380 putIState $ i { idris_options = opt' }
382setCmdLine :: [Opt] -> Idris ()
383setCmdLine opts = do i <- getIState
384 let iopts = idris_options i
385 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
387getCmdLine :: Idris [Opt]
388getCmdLine = do i <- getIState
389 return (opt_cmdline (idris_options i))
391getDumpDefun :: Idris (Maybe FilePath)
392getDumpDefun = do i <- getIState
393 return $ findC (opt_cmdline (idris_options i))
394 where findC [] = Nothing
395 findC (DumpDefun x : _) = Just x
396 findC (_ : xs) = findC xs
398getDumpCases :: Idris (Maybe FilePath)
399getDumpCases = do i <- getIState
400 return $ findC (opt_cmdline (idris_options i))
401 where findC [] = Nothing
402 findC (DumpCases x : _) = Just x
403 findC (_ : xs) = findC xs
405logLevel :: Idris Int
406logLevel = do i <- getIState
407 return (opt_logLevel (idris_options i))
409setErrContext :: Bool -> Idris ()
410setErrContext t = do i <- getIState
411 let opts = idris_options i
412 let opt' = opts { opt_errContext = t }
413 putIState $ i { idris_options = opt' }
415errContext :: Idris Bool
416errContext = do i <- getIState
417 return (opt_errContext (idris_options i))
419useREPL :: Idris Bool
420useREPL = do i <- getIState
421 return (opt_repl (idris_options i))
423setREPL :: Bool -> Idris ()
424setREPL t = do i <- getIState
425 let opts = idris_options i
426 let opt' = opts { opt_repl = t }
427 putIState $ i { idris_options = opt' }
429setNoBanner :: Bool -> Idris ()
430setNoBanner n = do i <- getIState
431 let opts = idris_options i
432 let opt' = opts {opt_nobanner = n}
433 putIState $ i { idris_options = opt' }
435getNoBanner :: Idris Bool
436getNoBanner = do i <- getIState
437 let opts = idris_options i
438 return (opt_nobanner opts)
440setQuiet :: Bool -> Idris ()
441setQuiet q = do i <- getIState
442 let opts = idris_options i
443 let opt' = opts { opt_quiet = q }
444 putIState $ i { idris_options = opt' }
446getQuiet :: Idris Bool
447getQuiet = do i <- getIState
448 let opts = idris_options i
449 return (opt_quiet opts)
451setCodegen :: Codegen -> Idris ()
452setCodegen t = do i <- getIState
453 let opts = idris_options i
454 let opt' = opts { opt_codegen = t }
455 putIState $ i { idris_options = opt' }
457codegen :: Idris Codegen
458codegen = do i <- getIState
459 return (opt_codegen (idris_options i))
461setOutputTy :: OutputType -> Idris ()
462setOutputTy t = do i <- getIState
463 let opts = idris_options i
464 let opt' = opts { opt_outputTy = t }
465 putIState $ i { idris_options = opt' }
467outputTy :: Idris OutputType
468outputTy = do i <- getIState
469 return $ opt_outputTy $ idris_options i
471setIdeSlave :: Bool -> Idris ()
472setIdeSlave True = do i <- getIState
473 putIState $ i { idris_outputmode = (IdeSlave 0), idris_colourRepl = False }
474setIdeSlave False = return ()
476setTargetTriple :: String -> Idris ()
477setTargetTriple t = do i <- getIState
478 let opts = idris_options i
479 opt' = opts { opt_triple = t }
480 putIState $ i { idris_options = opt' }
482targetTriple :: Idris String
483targetTriple = do i <- getIState
484 return (opt_triple (idris_options i))
486setTargetCPU :: String -> Idris ()
487setTargetCPU t = do i <- getIState
488 let opts = idris_options i
489 opt' = opts { opt_cpu = t }
490 putIState $ i { idris_options = opt' }
492targetCPU :: Idris String
493targetCPU = do i <- getIState
494 return (opt_cpu (idris_options i))
496setOptLevel :: Word -> Idris ()
497setOptLevel t = do i <- getIState
498 let opts = idris_options i
499 opt' = opts { opt_optLevel = t }
500 putIState $ i { idris_options = opt' }
502optLevel :: Idris Word
503optLevel = do i <- getIState
504 return (opt_optLevel (idris_options i))
506verbose :: Idris Bool
507verbose = do i <- getIState
508 return (opt_verbose (idris_options i))
510setVerbose :: Bool -> Idris ()
511setVerbose t = do i <- getIState
512 let opts = idris_options i
513 let opt' = opts { opt_verbose = t }
514 putIState $ i { idris_options = opt' }
516typeInType :: Idris Bool
517typeInType = do i <- getIState
518 return (opt_typeintype (idris_options i))
520setTypeInType :: Bool -> Idris ()
521setTypeInType t = do i <- getIState
522 let opts = idris_options i
523 let opt' = opts { opt_typeintype = t }
524 putIState $ i { idris_options = opt' }
526coverage :: Idris Bool
527coverage = do i <- getIState
528 return (opt_coverage (idris_options i))
530setCoverage :: Bool -> Idris ()
531setCoverage t = do i <- getIState
532 let opts = idris_options i
533 let opt' = opts { opt_coverage = t }
534 putIState $ i { idris_options = opt' }
536setIBCSubDir :: FilePath -> Idris ()
537setIBCSubDir fp = do i <- getIState
538 let opts = idris_options i
539 let opt' = opts { opt_ibcsubdir = fp }
540 putIState $ i { idris_options = opt' }
542valIBCSubDir :: IState -> Idris FilePath
543valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
545addImportDir :: FilePath -> Idris ()
546addImportDir fp = do i <- getIState
547 let opts = idris_options i
548 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
549 putIState $ i { idris_options = opt' }
551setImportDirs :: [FilePath] -> Idris ()
552setImportDirs fps = do i <- getIState
553 let opts = idris_options i
554 let opt' = opts { opt_importdirs = fps }
555 putIState $ i { idris_options = opt' }
557allImportDirs :: Idris [FilePath]
558allImportDirs = do i <- getIState
559 let optdirs = opt_importdirs (idris_options i)
560 return ("." : reverse optdirs)
562colourise :: Idris Bool
563colourise = do i <- getIState
564 return $ idris_colourRepl i
566setColourise :: Bool -> Idris ()
567setColourise b = do i <- getIState
568 putIState $ i { idris_colourRepl = b }
570setOutH :: Handle -> Idris ()
571setOutH h = do i <- getIState
572 putIState $ i { idris_outh = h }
574impShow :: Idris Bool
575impShow = do i <- getIState
576 return (opt_showimp (idris_options i))
578setImpShow :: Bool -> Idris ()
579setImpShow t = do i <- getIState
580 let opts = idris_options i
581 let opt' = opts { opt_showimp = t }
582 putIState $ i { idris_options = opt' }
584setColour :: ColourType -> IdrisColour -> Idris ()
585setColour ct c = do i <- getIState
586 let newTheme = setColour' ct c (idris_colourTheme i)
587 putIState $ i { idris_colourTheme = newTheme }
588 where setColour' KeywordColour c t = t { keywordColour = c }
589 setColour' BoundVarColour c t = t { boundVarColour = c }
590 setColour' ImplicitColour c t = t { implicitColour = c }
591 setColour' FunctionColour c t = t { functionColour = c }
592 setColour' TypeColour c t = t { typeColour = c }
593 setColour' DataColour c t = t { dataColour = c }
594 setColour' PromptColour c t = t { promptColour = c }
596logLvl :: Int -> String -> Idris ()
597logLvl l str = do i <- getIState
598 let lvl = opt_logLevel (idris_options i)
599 when (lvl >= l) $
600 case idris_outputmode i of
601 RawOutput -> do runIO $ putStrLn str
602 IdeSlave n ->
603 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
604 runIO $ putStrLn $ convSExp "log" good n
606cmdOptType :: Opt -> Idris Bool
607cmdOptType x = do i <- getIState
608 return $ x `elem` opt_cmdline (idris_options i)
610iLOG :: String -> Idris ()
611iLOG = logLvl 1
613noErrors :: Idris Bool
614noErrors = do i <- getIState
615 case errLine i of
616 Nothing -> return True
617 _ -> return False
619setTypeCase :: Bool -> Idris ()
620setTypeCase t = do i <- getIState
621 let opts = idris_options i
622 let opt' = opts { opt_typecase = t }
623 putIState $ i { idris_options = opt' }
626-- For inferring types of things
628bi = fileFC "builtin"
630inferTy = MN 0 "__Infer"
631inferCon = MN 0 "__infer"
632inferDecl = PDatadecl inferTy
633 PType
634 [("", inferCon, PPi impl (MN 0 "A") PType (
635 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
636 (PRef bi inferTy)), bi)]
638infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder True, pexp t]
639infP = P (TCon 6 0) inferTy (TType (UVal 0))
641getInferTerm, getInferType :: Term -> Term
642getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
643getInferTerm (App (App _ _) tm) = tm
644getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
646getInferType (Bind n b sc) = Bind n b $ getInferType sc
647getInferType (App (App _ ty) _) = ty
649-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
651primNames = [unitTy, unitCon,
652 falseTy, pairTy, pairCon,
653 eqTy, eqCon, inferTy, inferCon]
655unitTy = MN 0 "__Unit"
656unitCon = MN 0 "__II"
657unitDecl = PDatadecl unitTy PType
658 [("", unitCon, PRef bi unitTy, bi)]
660falseTy = MN 0 "__False"
661falseDecl = PDatadecl falseTy PType []
663pairTy = MN 0 "__Pair"
664pairCon = MN 0 "__MkPair"
665pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
666 [("", pairCon, PPi impl (n "A") PType (
667 PPi impl (n "B") PType (
668 PPi expl (n "a") (PRef bi (n "A")) (
669 PPi expl (n "b") (PRef bi (n "B"))
670 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
671 pexp (PRef bi (n "B"))])))), bi)]
672 where n a = MN 0 a
674eqTy = UN "="
675eqCon = UN "refl"
676eqDecl = PDatadecl eqTy (piBind [(n "a", PType), (n "b", PType),
677 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
678 PType)
679 [("", eqCon, PPi impl (n "a") PType (
680 PPi impl (n "x") (PRef bi (n "a"))
681 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder False,
682 pimp (n "b") Placeholder False,
683 pexp (PRef bi (n "x")),
684 pexp (PRef bi (n "x"))])), bi)]
685 where n a = MN 0 a
687-- Defined in builtins.idr
688sigmaTy = UN "Exists"
689existsCon = UN "Ex_intro"
691piBind :: [(Name, PTerm)] -> PTerm -> PTerm
692piBind = piBindp expl
694piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
695piBindp p [] t = t
696piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
698-- Dealing with parameters
700expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
701 [Name] -> -- all names
702 [Name] -> -- names with no declaration
703 PTerm -> PTerm
704expandParams dec ps ns infs tm = en tm
705 where
706 -- if we shadow a name (say in a lambda binding) that is used in a call to
707 -- a lifted function, we need access to both names - once in the scope of the
708 -- binding and once to call the lifted functions. So we'll explicitly shadow
709 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
710 -- but we didn't...)
712 mkShadow (UN n) = MN 0 n
713 mkShadow (MN i n) = MN (i+1) n
714 mkShadow (NS x s) = NS (mkShadow x) s
716 en (PLam n t s)
717 | n `elem` (map fst ps ++ ns)
718 = let n' = mkShadow n in
719 PLam n' (en t) (en (shadow n n' s))
720 | otherwise = PLam n (en t) (en s)
721 en (PPi p n t s)
722 | n `elem` (map fst ps ++ ns)
723 = let n' = mkShadow n in
724 PPi p n' (en t) (en (shadow n n' s))
725 | otherwise = PPi p n (en t) (en s)
726 en (PLet n ty v s)
727 | n `elem` (map fst ps ++ ns)
728 = let n' = mkShadow n in
729 PLet n' (en ty) (en v) (en (shadow n n' s))
730 | otherwise = PLet n (en ty) (en v) (en s)
731 -- FIXME: Should only do this in a type signature!
732 en (PDPair f (PRef f' n) t r)
733 | n `elem` (map fst ps ++ ns) && t /= Placeholder
734 = let n' = mkShadow n in
735 PDPair f (PRef f' n') (en t) (en (shadow n n' r))
736 en (PEq f l r) = PEq f (en l) (en r)
737 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
738 en (PTyped l r) = PTyped (en l) (en r)
739 en (PPair f l r) = PPair f (en l) (en r)
740 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
741 en (PAlternative a as) = PAlternative a (map en as)
742 en (PHidden t) = PHidden (en t)
743 en (PUnifyLog t) = PUnifyLog (en t)
744 en (PNoImplicits t) = PNoImplicits (en t)
745 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
746 en (PProof ts) = PProof (map (fmap en) ts)
747 en (PTactics ts) = PTactics (map (fmap en) ts)
749 en (PQuote (Var n))
750 | n `nselem` ns = PQuote (Var (dec n))
751 en (PApp fc (PInferRef fc' n) as)
752 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
753 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
754 en (PApp fc (PRef fc' n) as)
755 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
756 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
757 | n `nselem` ns = PApp fc (PRef fc' (dec n))
758 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
759 en (PAppBind fc (PRef fc' n) as)
760 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
761 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
762 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
763 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
764 en (PRef fc n)
765 | n `elem` infs = PApp fc (PInferRef fc (dec n))
766 (map (pexp . (PRef fc)) (map fst ps))
767 | n `nselem` ns = PApp fc (PRef fc (dec n))
768 (map (pexp . (PRef fc)) (map fst ps))
769 en (PInferRef fc n)
770 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
771 (map (pexp . (PRef fc)) (map fst ps))
772 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
773 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
774 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
775 en t = t
777 nselem x [] = False
778 nselem x (y : xs) | nseq x y = True
779 | otherwise = nselem x xs
781 nseq x y = nsroot x == nsroot y
783expandParamsD :: Bool -> -- True = RHS only
784 IState ->
785 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
786expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)
787 = if n `elem` ns && (not rhsonly)
788 then -- trace (show (n, expandParams dec ps ns ty)) $
789 PTy doc syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
790 else --trace (show (n, expandParams dec ps ns ty)) $
791 PTy doc syn fc o n (expandParams dec ps ns [] ty)
792expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
793 = if n `elem` ns && (not rhsonly)
794 then -- trace (show (n, expandParams dec ps ns ty)) $
795 PPostulate doc syn fc o (dec n) (piBind ps
796 (expandParams dec ps ns [] ty))
797 else --trace (show (n, expandParams dec ps ns ty)) $
798 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
799expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
800 = let n' = if n `elem` ns then dec n else n in
801 PClauses fc opts n' (map expandParamsC cs)
802 where
803 expandParamsC (PClause fc n lhs ws rhs ds)
804 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
805 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
806 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
807 n' = if n `elem` ns then dec n else n
808 -- names bound on the lhs should not be expanded on the rhs
809 ns' = removeBound lhs ns in
810 PClause fc n' lhs'
811 (map (expandParams dec ps'' ns' []) ws)
812 (expandParams dec ps'' ns' [] rhs)
813 (map (expandParamsD True ist dec ps'' ns') ds)
814 expandParamsC (PWith fc n lhs ws wval ds)
815 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
816 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
817 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
818 n' = if n `elem` ns then dec n else n
819 ns' = removeBound lhs ns in
820 PWith fc n' lhs'
821 (map (expandParams dec ps'' ns' []) ws)
822 (expandParams dec ps'' ns' [] wval)
823 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
824 updateps yn nm [] = []
825 updateps yn nm (((a, t), i):as)
826 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
827 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
829 removeBound lhs ns = ns \\ nub (bnames lhs)
831 bnames (PRef _ n) = [n]
832 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
833 bnames (PPair _ l r) = bnames l ++ bnames r
834 bnames (PDPair _ l Placeholder r) = bnames l ++ bnames r
835 bnames _ = []
837expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
838 = PData doc syn fc co (expandPData pd)
839 where
840 -- just do the type decl, leave constructors alone (parameters will be
841 -- added implicitly)
842 expandPData (PDatadecl n ty cons)
843 = if n `elem` ns
844 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
845 (map econ cons)
846 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
847 econ (doc, n, t, fc)
848 = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc)
849expandParamsD rhs ist dec ps ns (PParams f params pds)
850 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
851 (map (expandParamsD True ist dec ps ns) pds)
852-- (map (expandParamsD ist dec ps ns) pds)
853expandParamsD rhs ist dec ps ns (PMutual f pds)
854 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
855expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
856 = PClass doc info f
857 (map (expandParams dec ps ns []) cs)
858 n
859 (map (mapsnd (expandParams dec ps ns [])) params)
860 (map (expandParamsD rhs ist dec ps ns) decls)
861expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
862 = PInstance info f
863 (map (expandParams dec ps ns []) cs)
864 n
865 (map (expandParams dec ps ns []) params)
866 (expandParams dec ps ns [] ty)
867 cn
868 (map (expandParamsD rhs ist dec ps ns) decls)
869expandParamsD rhs ist dec ps ns d = d
871mapsnd f (x, t) = (x, f t)
873-- Calculate a priority for a type, for deciding elaboration order
874-- * if it's just a type variable or concrete type, do it early (0)
875-- * if there's only type variables and injective constructors, do it next (1)
876-- * if there's a function type, next (2)
877-- * finally, everything else (3)
879getPriority :: IState -> PTerm -> Int
880getPriority i tm = 1 -- pri tm
881 where
882 pri (PRef _ n) =
883 case lookupP n (tt_ctxt i) of
884 ((P (DCon _ _) _ _):_) -> 1
885 ((P (TCon _ _) _ _):_) -> 1
886 ((P Ref _ _):_) -> 1
887 [] -> 0 -- must be locally bound, if it's not an error...
888 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
889 pri (PTrue _) = 0
890 pri (PFalse _) = 0
891 pri (PRefl _ _) = 1
892 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
893 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
894 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
895 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
896 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
897 pri (PTyped l r) = pri l
898 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
899 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
900 pri (PAlternative a as) = maximum (map pri as)
901 pri (PConstant _) = 0
902 pri Placeholder = 1
903 pri _ = 3
905addStatics :: Name -> Term -> PTerm -> Idris ()
906addStatics n tm ptm =
907 do let (statics, dynamics) = initStatics tm ptm
908 let stnames = nub $ concatMap freeArgNames (map snd statics)
909 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
910 -- also get the arguments which are 'uniquely inferrable' from
911 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
912 let statics' = nub $ map fst statics ++
913 filter (\x -> not (elem x dnames)) stnames
914 let stpos = staticList statics' tm
915 i <- getIState
916 when (not (null statics)) $
917 logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics
918 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
919 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
920 addIBC (IBCStatic n)
921 where
922 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
923 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
924 if pstatic p == Static then ((n, ty) : static, dynamic)
925 else if (not (searchArg p))
926 then (static, (n, ty) : dynamic)
927 else (static, dynamic)
928 initStatics t pt = ([], [])
930 freeArgNames (Bind n (Pi ty) sc)
931 = nub $ freeArgNames ty
932 freeArgNames tm = let (_, args) = unApply tm in
933 concatMap freeNames args
935 -- if a name appears in a type class or tactic implicit index, it doesn't
936 -- affect its 'uniquely inferrable' from a static status since these are
937 -- resolved by searching.
938 searchArg (Constraint _ _ _) = True
939 searchArg (TacImp _ _ _ _) = True
940 searchArg _ = False
942 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
943 staticList _ _ = []
945-- Dealing with implicit arguments
947-- Add constraint bindings from using block
949addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
950addUsingConstraints syn fc t
951 = do ist <- get
952 let ns = namesIn [] ist t
953 let cs = getConstraints t -- check declared constraints
954 let addconsts = uconsts \\ cs
955 -- if all names in the arguments of addconsts appear in ns,
956 -- add the constraint implicitly
957 return (doAdd addconsts ns t)
958 where uconsts = filter uconst (using syn)
959 uconst (UConstraint _ _) = True
960 uconst _ = False
962 doAdd [] _ t = t
963 -- if all of args in ns, then add it
964 doAdd (UConstraint c args : cs) ns t
965 | all (\n -> elem n ns) args
966 = PPi (Constraint False Dynamic "") (MN 0 "cu")
967 (mkConst c args) (doAdd cs ns t)
968 | otherwise = doAdd cs ns t
970 mkConst c args = PApp fc (PRef fc c)
971 (map (\n -> PExp 0 False (PRef fc n) "") args)
973 getConstraints (PPi (Constraint _ _ _) _ c sc)
974 = getcapp c ++ getConstraints sc
975 getConstraints (PPi _ _ c sc) = getConstraints sc
976 getConstraints _ = []
978 getcapp (PApp _ (PRef _ c) args)
979 = do ns <- mapM getName args
980 return (UConstraint c ns)
981 getcapp _ = []
983 getName (PExp _ _ (PRef _ n) _) = return n
984 getName _ = []
986-- Add implicit Pi bindings for any names in the term which appear in an
987-- argument position.
989-- This has become a right mess already. Better redo it some time...
991implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
992implicit syn n ptm = implicit' syn [] n ptm
994implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
995implicit' syn ignore n ptm
996 = do i <- getIState
997 let (tm', impdata) = implicitise syn ignore i ptm
998-- let (tm'', spos) = findStatics i tm'
999 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1000 addIBC (IBCImp n)
1001 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1002-- i <- get
1003-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1004 return tm'
1006implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1007implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1008 let (declimps, ns') = execState (imps True [] tm) ([], [])
1009 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1010 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1011 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1012 if null ns
1013 then (tm, reverse declimps)
1014 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1015 where
1016 uvars = map ipair (filter uimplicit (using syn))
1017 pvars = syn_params syn
1019 inUsing n = n `elem` map fst uvars
1021 ipair (UImplicit x y) = (x, y)
1022 uimplicit (UImplicit _ _) = True
1023 uimplicit _ = False
1025 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1026 | otherwise = x : dropAll xs ys
1027 dropAll [] ys = []
1029 imps top env (PApp _ f as)
1030 = do (decls, ns) <- get
1031 let isn = concatMap (namesIn uvars ist) (map getTm as)
1032 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1033 imps top env (PPi (Imp l _ doc _) n ty sc)
1034 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1035 (decls , ns) <- get
1036 put (PImp (getPriority ist ty) True l n ty doc : decls,
1037 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1038 imps True (n:env) sc
1039 imps top env (PPi (Exp l _ doc _) n ty sc)
1040 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1041 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1042 _ -> [])
1043 (decls, ns) <- get -- ignore decls in HO types
1044 put (PExp (getPriority ist ty) l ty doc : decls,
1045 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1046 imps True (n:env) sc
1047 imps top env (PPi (Constraint l _ doc) n ty sc)
1048 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1049 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1050 _ -> [])
1051 (decls, ns) <- get -- ignore decls in HO types
1052 put (PConstraint 10 l ty doc : decls,
1053 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1054 imps True (n:env) sc
1055 imps top env (PPi (TacImp l _ scr doc) n ty sc)
1056 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1057 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1058 _ -> [])
1059 (decls, ns) <- get -- ignore decls in HO types
1060 put (PTacImplicit 10 l n scr ty doc : decls,
1061 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1062 imps True (n:env) sc
1063 imps top env (PEq _ l r)
1064 = do (decls, ns) <- get
1065 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1066 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1067 imps top env (PRewrite _ l r _)
1068 = do (decls, ns) <- get
1069 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1070 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1071 imps top env (PTyped l r)
1072 = imps top env l
1073 imps top env (PPair _ l r)
1074 = do (decls, ns) <- get
1075 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1076 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1077 imps top env (PDPair _ (PRef _ n) t r)
1078 = do (decls, ns) <- get
1079 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1080 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1081 imps top env (PDPair _ l t r)
1082 = do (decls, ns) <- get
1083 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1084 namesIn uvars ist r
1085 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1086 imps top env (PAlternative a as)
1087 = do (decls, ns) <- get
1088 let isn = concatMap (namesIn uvars ist) as
1089 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1090 imps top env (PLam n ty sc)
1091 = do imps False env ty
1092 imps False (n:env) sc
1093 imps top env (PHidden tm) = imps False env tm
1094 imps top env (PUnifyLog tm) = imps False env tm
1095 imps top env (PNoImplicits tm) = imps False env tm
1096 imps top env _ = return ()
1098 pibind using [] sc = sc
1099 pibind using (n:ns) sc
1100 = case lookup n using of
1101 Just ty -> PPi (Imp False Dynamic "" False) n ty (pibind using ns sc)
1102 Nothing -> PPi (Imp False Dynamic "" False) n Placeholder
1103 (pibind using ns sc)
1105-- Add implicit arguments in function calls
1106addImplPat :: IState -> PTerm -> PTerm
1107addImplPat = addImpl' True [] []
1109addImplBound :: IState -> [Name] -> PTerm -> PTerm
1110addImplBound ist ns = addImpl' False ns [] ist
1112addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1113addImplBoundInf ist ns inf = addImpl' False ns inf ist
1115addImpl :: IState -> PTerm -> PTerm
1116addImpl = addImpl' False [] []
1118-- TODO: in patterns, don't add implicits to function names guarded by constructors
1119-- and *not* inside a PHidden
1121addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1122addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm
1123 where
1124 ai env (PRef fc f)
1125 | f `elem` infns = PInferRef fc f
1126 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f []
1127 ai env (PHidden (PRef fc f))
1128 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f []
1129 ai env (PEq fc l r) = let l' = ai env l
1130 r' = ai env r in
1131 PEq fc l' r'
1132 ai env (PRewrite fc l r g) = let l' = ai env l
1133 r' = ai env r
1134 g' = fmap (ai env) g in
1135 PRewrite fc l' r' g'
1136 ai env (PTyped l r) = let l' = ai env l
1137 r' = ai env r in
1138 PTyped l' r'
1139 ai env (PPair fc l r) = let l' = ai env l
1140 r' = ai env r in
1141 PPair fc l' r'
1142 ai env (PDPair fc l t r) = let l' = ai env l
1143 t' = ai env t
1144 r' = ai env r in
1145 PDPair fc l' t' r'
1146 ai env (PAlternative a as) = let as' = map (ai env) as in
1147 PAlternative a as'
1148 ai env (PApp fc (PInferRef _ f) as)
1149 = let as' = map (fmap (ai env)) as in
1150 PApp fc (PInferRef fc f) as'
1151 ai env (PApp fc ftm@(PRef _ f) as)
1152 | f `elem` infns = ai env (PApp fc (PInferRef fc f) as)
1153 | not (f `elem` map fst env)
1154 = let as' = map (fmap (ai env)) as in
1155 handleErr $ aiFn inpat False ist fc f as'
1156 | Just (Just ty) <- lookup f env
1157 = let as' = map (fmap (ai env)) as
1158 arity = getPArity ty in
1159 mkPApp fc arity ftm as'
1160 ai env (PApp fc f as) = let f' = ai env f
1161 as' = map (fmap (ai env)) as in
1162 mkPApp fc 1 f' as'
1163 ai env (PCase fc c os) = let c' = ai env c
1164 os' = map (pmap (ai env)) os in
1165 PCase fc c' os'
1166 ai env (PLam n ty sc) = let ty' = ai env ty
1167 sc' = ai ((n, Just ty):env) sc in
1168 PLam n ty' sc'
1169 ai env (PLet n ty val sc)
1170 = let ty' = ai env ty
1171 val' = ai env val
1172 sc' = ai ((n, Just ty):env) sc in
1173 PLet n ty' val' sc'
1174 ai env (PPi p n ty sc) = let ty' = ai env ty
1175 sc' = ai ((n, Just ty):env) sc in
1176 PPi p n ty' sc'
1177 ai env (PGoal fc r n sc) = let r' = ai env r
1178 sc' = ai ((n, Nothing):env) sc in
1179 PGoal fc r' n sc'
1180 ai env (PHidden tm) = PHidden (ai env tm)
1181 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
1182 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
1183 ai env (PRefl fc tm) = PRefl fc (ai env tm)
1184 ai env (PUnifyLog tm) = PUnifyLog (ai env tm)
1185 ai env (PNoImplicits tm) = PNoImplicits (ai env tm)
1186 ai env tm = tm
1188 handleErr (Left err) = PElabError err
1189 handleErr (Right x) = x
1191-- if in a pattern, and there are no arguments, and there's no possible
1192-- names with zero explicit arguments, don't add implicits.
1194aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
1195aiFn inpat True ist fc f []
1196 = case lookupDef f (tt_ctxt ist) of
1197 [] -> Right $ PPatvar fc f
1198 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1199 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1200 if (not (vname f) || tcname f
1201 || any (conCaf (tt_ctxt ist)) ialts)
1202-- any constructor alts || any allImp ialts))
1203 then aiFn inpat False ist fc f [] -- use it as a constructor
1204 else Right $ PPatvar fc f
1205 where imp (PExp _ _ _ _) = False
1206 imp _ = True
1207-- allImp [] = False
1208 allImp xs = all imp xs
1209 constructor (TyDecl (DCon _ _) _) = True
1210 constructor _ = False
1212 conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
1214 vname (UN n) = True -- non qualified
1215 vname _ = False
1217aiFn inpat expat ist fc f as
1218 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1219aiFn inpat expat ist fc f as
1220 -- This is where namespaces get resolved by adding PAlternative
1221 = do let ns = lookupCtxtName f (idris_implicits ist)
1222 let ns' = filter (\(n, _) -> notHidden n) ns
1223 case ns' of
1224 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1225 [] -> if f `elem` (map fst (idris_metavars ist))
1226 then Right $ PApp fc (PRef fc f) as
1227 else Right $ mkPApp fc (length as) (PRef fc f) as
1228 alts -> Right $
1229 PAlternative True $
1230 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1231 (insertImpl ns as)) alts
1232 where
1233 notHidden n = case getAccessibility n of
1234 Hidden -> False
1235 _ -> True
1237 getAccessibility n
1238 = case lookupDefAcc n False (tt_ctxt ist) of
1239 [(n,t)] -> t
1240 _ -> Public
1243 insertImpl :: [PArg] -> [PArg] -> [PArg]
1244 insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =
1245 PExp p l tm d : insertImpl ps given
1246 insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =
1247 PConstraint p l tm d : insertImpl ps given
1248 insertImpl (PConstraint p l ty d : ps) given =
1249 PConstraint p l (PResolveTC fc) d : insertImpl ps given
1250 insertImpl (PImp p _ l n ty d : ps) given =
1251 case find n given [] of
1252 Just (tm, given') -> PImp p False l n tm "" : insertImpl ps given'
1253 Nothing -> PImp p True l n Placeholder "" : insertImpl ps given
1254 insertImpl (PTacImplicit p l n sc ty d : ps) given =
1255 case find n given [] of
1256 Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'
1257 Nothing -> if inpat
1258 then PTacImplicit p l n sc Placeholder "" : insertImpl ps given
1259 else PTacImplicit p l n sc sc "" : insertImpl ps given
1260 insertImpl expected [] = []
1261 insertImpl _ given = given
1263 find n [] acc = Nothing
1264 find n (PImp _ _ _ n' t _ : gs) acc
1265 | n == n' = Just (t, reverse acc ++ gs)
1266 find n (PTacImplicit _ _ n' _ t _ : gs) acc
1267 | n == n' = Just (t, reverse acc ++ gs)
1268 find n (g : gs) acc = find n gs (g : acc)
1270-- replace non-linear occurrences with _
1271-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1272-- it is hard to get right!
1274stripLinear :: IState -> PTerm -> PTerm
1275stripLinear i tm = evalState (sl tm) [] where
1276 sl :: PTerm -> State [Name] PTerm
1277 sl (PRef fc f)
1278 | (_:_) <- lookupTy f (tt_ctxt i)
1279 = return $ PRef fc f
1280 | otherwise = do ns <- get
1281 if (f `elem` ns)
1282 then return Placeholder
1283 else do put (f : ns)
1284 return (PRef fc f)
1285 sl (PPatvar fc f)
1286 = do ns <- get
1287 if (f `elem` ns)
1288 then return Placeholder
1289 else do put (f : ns)
1290 return (PPatvar fc f)
1291 sl (PApp fc fn args) = do fn' <- sl fn
1292 args' <- mapM slA args
1293 return $ PApp fc fn' args'
1294 where slA (PImp p m l n t d) = do t' <- sl t
1295 return $ PImp p m l n t' d
1296 slA (PExp p l t d) = do t' <- sl t
1297 return $ PExp p l t' d
1298 slA (PConstraint p l t d)
1299 = do t' <- sl t
1300 return $ PConstraint p l t' d
1301 slA (PTacImplicit p l n sc t d)
1302 = do t' <- sl t
1303 return $ PTacImplicit p l n sc t' d
1304 sl x = return x
1306-- Remove functions which aren't applied to anything, which must then
1307-- be resolved by unification. Assume names resolved and alternatives
1308-- filled in (so no ambiguity).
1310stripUnmatchable :: IState -> PTerm -> PTerm
1311stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1312 su :: PTerm -> PTerm
1313 su (PRef fc f)
1314 | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1315 = Placeholder
1316 su (PApp fc fn args)
1317 = PApp fc fn (fmap (fmap su) args)
1318 su (PAlternative b alts)
1319 = let alts' = filter (/= Placeholder) (map su alts) in
1320 if null alts' then Placeholder
1321 else PAlternative b alts'
1322 su (PPair fc l r) = PPair fc (su l) (su r)
1323 su (PDPair fc l t r) = PDPair fc (su l) (su t) (su r)
1324 su t = t
1325stripUnmatchable i tm = tm
1327mkPApp fc a f [] = f
1328mkPApp fc a f as = let rest = drop a as in
1329 appRest fc (PApp fc f (take a as)) rest
1330 where
1331 appRest fc f [] = f
1332 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1334-- Find 'static' argument positions
1335-- (the declared ones, plus any names in argument position in the declared
1336-- statics)
1337-- FIXME: It's possible that this really has to happen after elaboration
1339findStatics :: IState -> PTerm -> (PTerm, [Bool])
1340findStatics ist tm = trace (showImp Nothing True False tm) $
1341 let (ns, ss) = fs tm in
1342 runState (pos ns ss tm) []
1343 where fs (PPi p n t sc)
1344 | Static <- pstatic p
1345 = let (ns, ss) = fs sc in
1346 (namesIn [] ist t : ns, n : ss)
1347 | otherwise = let (ns, ss) = fs sc in
1348 (ns, ss)
1349 fs _ = ([], [])
1351 inOne n ns = length (filter id (map (elem n) ns)) == 1
1353 pos ns ss (PPi p n t sc)
1354 | elem n ss = do sc' <- pos ns ss sc
1355 spos <- get
1356 put (True : spos)
1357 return (PPi (p { pstatic = Static }) n t sc')
1358 | otherwise = do sc' <- pos ns ss sc
1359 spos <- get
1360 put (False : spos)
1361 return (PPi p n t sc')
1362 pos ns ss t = return t
1364-- Debugging/logging stuff
1366dumpDecls :: [PDecl] -> String
1367dumpDecls [] = ""
1368dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
1370dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
1371dumpDecl (PTy _ _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp Nothing True False t
1372dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
1373dumpDecl (PData _ _ _ _ d) = showDImp True d
1374dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
1375dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
1376dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
1377dumpDecl (PClass _ _ _ cs n ps ds)
1378 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
1379dumpDecl (PInstance _ _ cs n _ t _ ds)
1380 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
1381dumpDecl _ = "..."
1382-- dumpDecl (PImport i) = "import " ++ i
1384-- for 6.12/7 compatibility
1385data EitherErr a b = LeftErr a | RightOK b
1387instance Monad (EitherErr a) where
1388 return = RightOK
1390 (LeftErr e) >>= k = LeftErr e
1391 RightOK v >>= k = k v
1393toEither (LeftErr e) = Left e
1394toEither (RightOK ho) = Right ho
1396-- syntactic match of a against b, returning pair of variables in a
1397-- and what they match. Returns the pair that failed if not a match.
1399matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1400matchClause = matchClause' False
1402matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1403matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1404 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1406 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1407 fullApp x = x
1409 match' x y = match (fullApp x) (fullApp y)
1410 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
1411 | PConstant (I _) <- getTm x = match (getTm x) x'
1412 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
1413 | PConstant (I _) <- getTm x = match (getTm x) x'
1414 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
1415 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
1416 match (PApp _ f args) (PApp _ f' args')
1417 | length args == length args'
1418 = do mf <- match' f f'
1419 ms <- zipWithM matchArg args args'
1420 return (mf ++ concat ms)
1421-- match (PRef _ n) (PRef _ n') | n == n' = return []
1422-- | otherwise = Nothing
1423 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1424 match (PPatvar f n) xr = match (PRef f n) xr
1425 match xr (PPatvar f n) = match xr (PRef f n)
1426 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1427 match (PRef _ n) tm@(PRef _ n')
1428 | n == n' && not names &&
1429 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1430 || tm == Placeholder)
1431 = return [(n, tm)]
1432 | n == n' = return []
1433 match (PRef _ n) tm
1434 | not names && (not (isConName n (tt_ctxt i) ||
1435 isFnName n (tt_ctxt i)) || tm == Placeholder)
1436 = return [(n, tm)]
1437 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1438 mr <- match' r r'
1439 return (ml ++ mr)
1440 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1441 = do ml <- match' l l'
1442 mr <- match' r r'
1443 return (ml ++ mr)
1444 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1445 mr <- match r r'
1446 return (ml ++ mr)
1447 match (PTyped l r) x = match l x
1448 match x (PTyped l r) = match x l
1449 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1450 mr <- match' r r'
1451 return (ml ++ mr)
1452 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1453 mt <- match' t t'
1454 mr <- match' r r'
1455 return (ml ++ mt ++ mr)
1456 match (PAlternative a as) (PAlternative a' as')
1457 = do ms <- zipWithM match' as as'
1458 return (concat ms)
1459 match a@(PAlternative _ as) b
1460 = do let ms = zipWith match' as (repeat b)
1461 case (rights (map toEither ms)) of
1462 (x: _) -> return x
1463 _ -> LeftErr (a, b)
1464 match (PCase _ _ _) _ = return [] -- lifted out
1465 match (PMetavar _) _ = return [] -- modified
1466 match (PInferRef _ _) _ = return [] -- modified
1467 match (PQuote _) _ = return []
1468 match (PProof _) _ = return []
1469 match (PTactics _) _ = return []
1470 match (PRefl _ _) (PRefl _ _) = return []
1471 match (PResolveTC _) (PResolveTC _) = return []
1472 match (PTrue _) (PTrue _) = return []
1473 match (PFalse _) (PFalse _) = return []
1474 match (PReturn _) (PReturn _) = return []
1475 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1476 ms <- match' s s'
1477 return (mt ++ ms)
1478 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1479 ms <- match' s s'
1480 return (mt ++ ms)
1481 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1482 mty <- match' ty ty'
1483 ms <- match' s s'
1484 return (mt ++ mty ++ ms)
1485 match (PHidden x) (PHidden y) = match' x y
1486 match (PUnifyLog x) y = match' x y
1487 match x (PUnifyLog y) = match' x y
1488 match (PNoImplicits x) y = match' x y
1489 match x (PNoImplicits y) = match' x y
1490 match Placeholder _ = return []
1491 match _ Placeholder = return []
1492 match (PResolveTC _) _ = return []
1493 match a b | a == b = return []
1494 | otherwise = LeftErr (a, b)
1496 checkRpts (RightOK ms) = check ms where
1497 check ((n,t):xs)
1498 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1499 then Left (t, t')
1500 else check xs
1501 check (_:xs) = check xs
1502 check [] = Right ms
1503 checkRpts (LeftErr x) = Left x
1505substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1506substMatches ms = substMatchesShadow ms []
1508substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1509substMatchesShadow [] shs t = t
1510substMatchesShadow ((n,tm):ns) shs t
1511 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1513substMatch :: Name -> PTerm -> PTerm -> PTerm
1514substMatch n = substMatchShadow n []
1516substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1517substMatchShadow n shs tm t = sm shs t where
1518 sm xs (PRef _ n') | n == n' = tm
1519 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1520 sm xs (PPi p x t sc)
1521 | x `elem` xs
1522 = let x' = nextName x in
1523 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1524 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1525 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1526 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1527 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1528 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1529 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1530 (fmap (sm xs) tm)
1531 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1532 sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)
1533 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)
1534 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1535 sm xs (PHidden x) = PHidden (sm xs x)
1536 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1537 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1538 sm xs x = x
1540 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1541 fullApp x = x
1543shadow :: Name -> Name -> PTerm -> PTerm
1544shadow n n' t = sm t where
1545 sm (PRef fc x) | n == x = PRef fc n'
1546 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1547 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1548 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1549 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1550 sm (PEq f x y) = PEq f (sm x) (sm y)
1551 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1552 sm (PTyped x y) = PTyped (sm x) (sm y)
1553 sm (PPair f x y) = PPair f (sm x) (sm y)
1554 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1555 sm (PAlternative a as) = PAlternative a (map sm as)
1556 sm (PHidden x) = PHidden (sm x)
1557 sm (PUnifyLog x) = PUnifyLog (sm x)
1558 sm (PNoImplicits x) = PNoImplicits (sm x)
1559 sm x = x