git.iko.soy/Idris-dev
on 10410de help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1553 lines 64 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)]
637inferOpts = []
639infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder True, pexp t]
640infP = P (TCon 6 0) inferTy (TType (UVal 0))
642getInferTerm, getInferType :: Term -> Term
643getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
644getInferTerm (App (App _ _) tm) = tm
645getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
647getInferType (Bind n b sc) = Bind n b $ getInferType sc
648getInferType (App (App _ ty) _) = ty
650-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class
652primNames = [unitTy, unitCon,
653 falseTy, pairTy, pairCon,
654 eqTy, eqCon, inferTy, inferCon]
656unitTy = MN 0 "__Unit"
657unitCon = MN 0 "__II"
658unitDecl = PDatadecl unitTy PType
659 [("", unitCon, PRef bi unitTy, bi)]
660unitOpts = [DefaultEliminator]
662falseTy = MN 0 "__False"
663falseDecl = PDatadecl falseTy PType []
664falseOpts = []
666pairTy = MN 0 "__Pair"
667pairCon = MN 0 "__MkPair"
668pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
669 [("", pairCon, PPi impl (n "A") PType (
670 PPi impl (n "B") PType (
671 PPi expl (n "a") (PRef bi (n "A")) (
672 PPi expl (n "b") (PRef bi (n "B"))
673 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
674 pexp (PRef bi (n "B"))])))), bi)]
675 where n a = MN 0 a
676pairOpts = []
678eqTy = UN "="
679eqCon = UN "refl"
680eqDecl = PDatadecl eqTy (piBind [(n "a", PType), (n "b", PType),
681 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
682 PType)
683 [("", eqCon, PPi impl (n "a") PType (
684 PPi impl (n "x") (PRef bi (n "a"))
685 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder False,
686 pimp (n "b") Placeholder False,
687 pexp (PRef bi (n "x")),
688 pexp (PRef bi (n "x"))])), bi)]
689 where n a = MN 0 a
690eqOpts = []
692elimName = UN "__Elim"
693elimMethElimTy = UN "__elimTy"
694elimMethElim = UN "elim"
695elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(UN "scrutineeType", PType)]
696 [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,
697 PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
699-- Defined in builtins.idr
700sigmaTy = UN "Exists"
701existsCon = UN "Ex_intro"
703piBind :: [(Name, PTerm)] -> PTerm -> PTerm
704piBind = piBindp expl
706piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
707piBindp p [] t = t
708piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
710-- Dealing with parameters
712expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
713 [Name] -> -- all names
714 [Name] -> -- names with no declaration
715 PTerm -> PTerm
716expandParams dec ps ns infs tm = en tm
717 where
718 -- if we shadow a name (say in a lambda binding) that is used in a call to
719 -- a lifted function, we need access to both names - once in the scope of the
720 -- binding and once to call the lifted functions. So we'll explicitly shadow
721 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
722 -- but we didn't...)
724 mkShadow (UN n) = MN 0 n
725 mkShadow (MN i n) = MN (i+1) n
726 mkShadow (NS x s) = NS (mkShadow x) s
728 en (PLam n t s)
729 | n `elem` (map fst ps ++ ns)
730 = let n' = mkShadow n in
731 PLam n' (en t) (en (shadow n n' s))
732 | otherwise = PLam n (en t) (en s)
733 en (PPi p n t s)
734 | n `elem` (map fst ps ++ ns)
735 = let n' = mkShadow n in
736 PPi p n' (en t) (en (shadow n n' s))
737 | otherwise = PPi p n (en t) (en s)
738 en (PLet n ty v s)
739 | n `elem` (map fst ps ++ ns)
740 = let n' = mkShadow n in
741 PLet n' (en ty) (en v) (en (shadow n n' s))
742 | otherwise = PLet n (en ty) (en v) (en s)
743 -- FIXME: Should only do this in a type signature!
744 en (PDPair f (PRef f' n) t r)
745 | n `elem` (map fst ps ++ ns) && t /= Placeholder
746 = let n' = mkShadow n in
747 PDPair f (PRef f' n') (en t) (en (shadow n n' r))
748 en (PEq f l r) = PEq f (en l) (en r)
749 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
750 en (PTyped l r) = PTyped (en l) (en r)
751 en (PPair f l r) = PPair f (en l) (en r)
752 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
753 en (PAlternative a as) = PAlternative a (map en as)
754 en (PHidden t) = PHidden (en t)
755 en (PUnifyLog t) = PUnifyLog (en t)
756 en (PNoImplicits t) = PNoImplicits (en t)
757 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
758 en (PProof ts) = PProof (map (fmap en) ts)
759 en (PTactics ts) = PTactics (map (fmap en) ts)
761 en (PQuote (Var n))
762 | n `nselem` ns = PQuote (Var (dec n))
763 en (PApp fc (PInferRef fc' n) as)
764 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
765 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
766 en (PApp fc (PRef fc' n) as)
767 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
768 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
769 | n `nselem` ns = PApp fc (PRef fc' (dec n))
770 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
771 en (PAppBind fc (PRef fc' n) as)
772 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
773 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
774 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
775 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
776 en (PRef fc n)
777 | n `elem` infs = PApp fc (PInferRef fc (dec n))
778 (map (pexp . (PRef fc)) (map fst ps))
779 | n `nselem` ns = PApp fc (PRef fc (dec n))
780 (map (pexp . (PRef fc)) (map fst ps))
781 en (PInferRef fc n)
782 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
783 (map (pexp . (PRef fc)) (map fst ps))
784 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
785 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
786 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
787 en t = t
789 nselem x [] = False
790 nselem x (y : xs) | nseq x y = True
791 | otherwise = nselem x xs
793 nseq x y = nsroot x == nsroot y
795expandParamsD :: Bool -> -- True = RHS only
796 IState ->
797 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
798expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)
799 = if n `elem` ns && (not rhsonly)
800 then -- trace (show (n, expandParams dec ps ns ty)) $
801 PTy doc syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
802 else --trace (show (n, expandParams dec ps ns ty)) $
803 PTy doc syn fc o n (expandParams dec ps ns [] ty)
804expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
805 = if n `elem` ns && (not rhsonly)
806 then -- trace (show (n, expandParams dec ps ns ty)) $
807 PPostulate doc syn fc o (dec n) (piBind ps
808 (expandParams dec ps ns [] ty))
809 else --trace (show (n, expandParams dec ps ns ty)) $
810 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
811expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
812 = let n' = if n `elem` ns then dec n else n in
813 PClauses fc opts n' (map expandParamsC cs)
814 where
815 expandParamsC (PClause fc n lhs ws rhs ds)
816 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
817 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
818 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
819 n' = if n `elem` ns then dec n else n
820 -- names bound on the lhs should not be expanded on the rhs
821 ns' = removeBound lhs ns in
822 PClause fc n' lhs'
823 (map (expandParams dec ps'' ns' []) ws)
824 (expandParams dec ps'' ns' [] rhs)
825 (map (expandParamsD True ist dec ps'' ns') ds)
826 expandParamsC (PWith fc n lhs ws wval ds)
827 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
828 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
829 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
830 n' = if n `elem` ns then dec n else n
831 ns' = removeBound lhs ns in
832 PWith fc n' lhs'
833 (map (expandParams dec ps'' ns' []) ws)
834 (expandParams dec ps'' ns' [] wval)
835 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
836 updateps yn nm [] = []
837 updateps yn nm (((a, t), i):as)
838 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
839 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
841 removeBound lhs ns = ns \\ nub (bnames lhs)
843 bnames (PRef _ n) = [n]
844 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
845 bnames (PPair _ l r) = bnames l ++ bnames r
846 bnames (PDPair _ l Placeholder r) = bnames l ++ bnames r
847 bnames _ = []
849expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
850 = PData doc syn fc co (expandPData pd)
851 where
852 -- just do the type decl, leave constructors alone (parameters will be
853 -- added implicitly)
854 expandPData (PDatadecl n ty cons)
855 = if n `elem` ns
856 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
857 (map econ cons)
858 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
859 econ (doc, n, t, fc)
860 = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc)
861expandParamsD rhs ist dec ps ns (PParams f params pds)
862 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
863 (map (expandParamsD True ist dec ps ns) pds)
864-- (map (expandParamsD ist dec ps ns) pds)
865expandParamsD rhs ist dec ps ns (PMutual f pds)
866 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
867expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
868 = PClass doc info f
869 (map (expandParams dec ps ns []) cs)
870 n
871 (map (mapsnd (expandParams dec ps ns [])) params)
872 (map (expandParamsD rhs ist dec ps ns) decls)
873expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
874 = PInstance info f
875 (map (expandParams dec ps ns []) cs)
876 n
877 (map (expandParams dec ps ns []) params)
878 (expandParams dec ps ns [] ty)
879 cn
880 (map (expandParamsD rhs ist dec ps ns) decls)
881expandParamsD rhs ist dec ps ns d = d
883mapsnd f (x, t) = (x, f t)
885-- Calculate a priority for a type, for deciding elaboration order
886-- * if it's just a type variable or concrete type, do it early (0)
887-- * if there's only type variables and injective constructors, do it next (1)
888-- * if there's a function type, next (2)
889-- * finally, everything else (3)
891getPriority :: IState -> PTerm -> Int
892getPriority i tm = 1 -- pri tm
893 where
894 pri (PRef _ n) =
895 case lookupP n (tt_ctxt i) of
896 ((P (DCon _ _) _ _):_) -> 1
897 ((P (TCon _ _) _ _):_) -> 1
898 ((P Ref _ _):_) -> 1
899 [] -> 0 -- must be locally bound, if it's not an error...
900 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
901 pri (PTrue _) = 0
902 pri (PFalse _) = 0
903 pri (PRefl _ _) = 1
904 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
905 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
906 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
907 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
908 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
909 pri (PTyped l r) = pri l
910 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
911 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
912 pri (PAlternative a as) = maximum (map pri as)
913 pri (PConstant _) = 0
914 pri Placeholder = 1
915 pri _ = 3
917addStatics :: Name -> Term -> PTerm -> Idris ()
918addStatics n tm ptm =
919 do let (statics, dynamics) = initStatics tm ptm
920 let stnames = nub $ concatMap freeArgNames (map snd statics)
921 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
922 -- also get the arguments which are 'uniquely inferrable' from
923 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
924 let statics' = nub $ map fst statics ++
925 filter (\x -> not (elem x dnames)) stnames
926 let stpos = staticList statics' tm
927 i <- getIState
928 when (not (null statics)) $
929 logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics
930 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
931 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
932 addIBC (IBCStatic n)
933 where
934 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
935 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
936 if pstatic p == Static then ((n, ty) : static, dynamic)
937 else if (not (searchArg p))
938 then (static, (n, ty) : dynamic)
939 else (static, dynamic)
940 initStatics t pt = ([], [])
942 freeArgNames (Bind n (Pi ty) sc)
943 = nub $ freeArgNames ty
944 freeArgNames tm = let (_, args) = unApply tm in
945 concatMap freeNames args
947 -- if a name appears in a type class or tactic implicit index, it doesn't
948 -- affect its 'uniquely inferrable' from a static status since these are
949 -- resolved by searching.
950 searchArg (Constraint _ _ _) = True
951 searchArg (TacImp _ _ _ _) = True
952 searchArg _ = False
954 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
955 staticList _ _ = []
957-- Dealing with implicit arguments
959-- Add constraint bindings from using block
961addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
962addUsingConstraints syn fc t
963 = do ist <- get
964 let ns = namesIn [] ist t
965 let cs = getConstraints t -- check declared constraints
966 let addconsts = uconsts \\ cs
967 -- if all names in the arguments of addconsts appear in ns,
968 -- add the constraint implicitly
969 return (doAdd addconsts ns t)
970 where uconsts = filter uconst (using syn)
971 uconst (UConstraint _ _) = True
972 uconst _ = False
974 doAdd [] _ t = t
975 -- if all of args in ns, then add it
976 doAdd (UConstraint c args : cs) ns t
977 | all (\n -> elem n ns) args
978 = PPi (Constraint False Dynamic "") (MN 0 "cu")
979 (mkConst c args) (doAdd cs ns t)
980 | otherwise = doAdd cs ns t
982 mkConst c args = PApp fc (PRef fc c)
983 (map (\n -> PExp 0 False (PRef fc n) "") args)
985 getConstraints (PPi (Constraint _ _ _) _ c sc)
986 = getcapp c ++ getConstraints sc
987 getConstraints (PPi _ _ c sc) = getConstraints sc
988 getConstraints _ = []
990 getcapp (PApp _ (PRef _ c) args)
991 = do ns <- mapM getName args
992 return (UConstraint c ns)
993 getcapp _ = []
995 getName (PExp _ _ (PRef _ n) _) = return n
996 getName _ = []
998-- Add implicit Pi bindings for any names in the term which appear in an
999-- argument position.
1001-- This has become a right mess already. Better redo it some time...
1003implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
1004implicit syn n ptm = implicit' syn [] n ptm
1006implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1007implicit' syn ignore n ptm
1008 = do i <- getIState
1009 let (tm', impdata) = implicitise syn ignore i ptm
1010-- let (tm'', spos) = findStatics i tm'
1011 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1012 addIBC (IBCImp n)
1013 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1014-- i <- get
1015-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1016 return tm'
1018implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1019implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1020 let (declimps, ns') = execState (imps True [] tm) ([], [])
1021 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1022 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1023 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1024 if null ns
1025 then (tm, reverse declimps)
1026 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1027 where
1028 uvars = map ipair (filter uimplicit (using syn))
1029 pvars = syn_params syn
1031 inUsing n = n `elem` map fst uvars
1033 ipair (UImplicit x y) = (x, y)
1034 uimplicit (UImplicit _ _) = True
1035 uimplicit _ = False
1037 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1038 | otherwise = x : dropAll xs ys
1039 dropAll [] ys = []
1041 imps top env (PApp _ f as)
1042 = do (decls, ns) <- get
1043 let isn = concatMap (namesIn uvars ist) (map getTm as)
1044 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1045 imps top env (PPi (Imp l _ doc _) n ty sc)
1046 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1047 (decls , ns) <- get
1048 put (PImp (getPriority ist ty) True l n ty doc : decls,
1049 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1050 imps True (n:env) sc
1051 imps top env (PPi (Exp l _ doc _) n ty sc)
1052 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1053 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1054 _ -> [])
1055 (decls, ns) <- get -- ignore decls in HO types
1056 put (PExp (getPriority ist ty) l ty doc : decls,
1057 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1058 imps True (n:env) sc
1059 imps top env (PPi (Constraint l _ doc) n ty sc)
1060 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1061 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1062 _ -> [])
1063 (decls, ns) <- get -- ignore decls in HO types
1064 put (PConstraint 10 l ty doc : decls,
1065 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1066 imps True (n:env) sc
1067 imps top env (PPi (TacImp l _ scr doc) n ty sc)
1068 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1069 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1070 _ -> [])
1071 (decls, ns) <- get -- ignore decls in HO types
1072 put (PTacImplicit 10 l n scr ty doc : decls,
1073 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1074 imps True (n:env) sc
1075 imps top env (PEq _ l r)
1076 = do (decls, ns) <- get
1077 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1078 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1079 imps top env (PRewrite _ l r _)
1080 = do (decls, ns) <- get
1081 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1082 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1083 imps top env (PTyped l r)
1084 = imps top env l
1085 imps top env (PPair _ l r)
1086 = do (decls, ns) <- get
1087 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1088 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1089 imps top env (PDPair _ (PRef _ n) t r)
1090 = do (decls, ns) <- get
1091 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1092 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1093 imps top env (PDPair _ l t r)
1094 = do (decls, ns) <- get
1095 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1096 namesIn uvars ist r
1097 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1098 imps top env (PAlternative a as)
1099 = do (decls, ns) <- get
1100 let isn = concatMap (namesIn uvars ist) as
1101 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1102 imps top env (PLam n ty sc)
1103 = do imps False env ty
1104 imps False (n:env) sc
1105 imps top env (PHidden tm) = imps False env tm
1106 imps top env (PUnifyLog tm) = imps False env tm
1107 imps top env (PNoImplicits tm) = imps False env tm
1108 imps top env _ = return ()
1110 pibind using [] sc = sc
1111 pibind using (n:ns) sc
1112 = case lookup n using of
1113 Just ty -> PPi (Imp False Dynamic "" False) n ty (pibind using ns sc)
1114 Nothing -> PPi (Imp False Dynamic "" False) n Placeholder
1115 (pibind using ns sc)
1117-- Add implicit arguments in function calls
1118addImplPat :: IState -> PTerm -> PTerm
1119addImplPat = addImpl' True [] []
1121addImplBound :: IState -> [Name] -> PTerm -> PTerm
1122addImplBound ist ns = addImpl' False ns [] ist
1124addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1125addImplBoundInf ist ns inf = addImpl' False ns inf ist
1127addImpl :: IState -> PTerm -> PTerm
1128addImpl = addImpl' False [] []
1130-- TODO: in patterns, don't add implicits to function names guarded by constructors
1131-- and *not* inside a PHidden
1133addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1134addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm
1135 where
1136 ai env (PRef fc f)
1137 | f `elem` infns = PInferRef fc f
1138 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f []
1139 ai env (PHidden (PRef fc f))
1140 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f []
1141 ai env (PEq fc l r) = let l' = ai env l
1142 r' = ai env r in
1143 PEq fc l' r'
1144 ai env (PRewrite fc l r g) = let l' = ai env l
1145 r' = ai env r
1146 g' = fmap (ai env) g in
1147 PRewrite fc l' r' g'
1148 ai env (PTyped l r) = let l' = ai env l
1149 r' = ai env r in
1150 PTyped l' r'
1151 ai env (PPair fc l r) = let l' = ai env l
1152 r' = ai env r in
1153 PPair fc l' r'
1154 ai env (PDPair fc l t r) = let l' = ai env l
1155 t' = ai env t
1156 r' = ai env r in
1157 PDPair fc l' t' r'
1158 ai env (PAlternative a as) = let as' = map (ai env) as in
1159 PAlternative a as'
1160 ai env (PApp fc (PInferRef _ f) as)
1161 = let as' = map (fmap (ai env)) as in
1162 PApp fc (PInferRef fc f) as'
1163 ai env (PApp fc ftm@(PRef _ f) as)
1164 | f `elem` infns = ai env (PApp fc (PInferRef fc f) as)
1165 | not (f `elem` map fst env)
1166 = let as' = map (fmap (ai env)) as in
1167 handleErr $ aiFn inpat False ist fc f as'
1168 | Just (Just ty) <- lookup f env
1169 = let as' = map (fmap (ai env)) as
1170 arity = getPArity ty in
1171 mkPApp fc arity ftm as'
1172 ai env (PApp fc f as) = let f' = ai env f
1173 as' = map (fmap (ai env)) as in
1174 mkPApp fc 1 f' as'
1175 ai env (PCase fc c os) = let c' = ai env c
1176 os' = map (pmap (ai env)) os in
1177 PCase fc c' os'
1178 ai env (PLam n ty sc) = let ty' = ai env ty
1179 sc' = ai ((n, Just ty):env) sc in
1180 PLam n ty' sc'
1181 ai env (PLet n ty val sc)
1182 = let ty' = ai env ty
1183 val' = ai env val
1184 sc' = ai ((n, Just ty):env) sc in
1185 PLet n ty' val' sc'
1186 ai env (PPi p n ty sc) = let ty' = ai env ty
1187 sc' = ai ((n, Just ty):env) sc in
1188 PPi p n ty' sc'
1189 ai env (PGoal fc r n sc) = let r' = ai env r
1190 sc' = ai ((n, Nothing):env) sc in
1191 PGoal fc r' n sc'
1192 ai env (PHidden tm) = PHidden (ai env tm)
1193 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
1194 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
1195 ai env (PRefl fc tm) = PRefl fc (ai env tm)
1196 ai env (PUnifyLog tm) = PUnifyLog (ai env tm)
1197 ai env (PNoImplicits tm) = PNoImplicits (ai env tm)
1198 ai env tm = tm
1200 handleErr (Left err) = PElabError err
1201 handleErr (Right x) = x
1203-- if in a pattern, and there are no arguments, and there's no possible
1204-- names with zero explicit arguments, don't add implicits.
1206aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
1207aiFn inpat True ist fc f []
1208 = case lookupDef f (tt_ctxt ist) of
1209 [] -> Right $ PPatvar fc f
1210 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1211 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1212 if (not (vname f) || tcname f
1213 || any (conCaf (tt_ctxt ist)) ialts)
1214-- any constructor alts || any allImp ialts))
1215 then aiFn inpat False ist fc f [] -- use it as a constructor
1216 else Right $ PPatvar fc f
1217 where imp (PExp _ _ _ _) = False
1218 imp _ = True
1219-- allImp [] = False
1220 allImp xs = all imp xs
1221 constructor (TyDecl (DCon _ _) _) = True
1222 constructor _ = False
1224 conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
1226 vname (UN n) = True -- non qualified
1227 vname _ = False
1229aiFn inpat expat ist fc f as
1230 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1231aiFn inpat expat ist fc f as
1232 -- This is where namespaces get resolved by adding PAlternative
1233 = do let ns = lookupCtxtName f (idris_implicits ist)
1234 let ns' = filter (\(n, _) -> notHidden n) ns
1235 case ns' of
1236 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1237 [] -> if f `elem` (map fst (idris_metavars ist))
1238 then Right $ PApp fc (PRef fc f) as
1239 else Right $ mkPApp fc (length as) (PRef fc f) as
1240 alts -> Right $
1241 PAlternative True $
1242 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1243 (insertImpl ns as)) alts
1244 where
1245 notHidden n = case getAccessibility n of
1246 Hidden -> False
1247 _ -> True
1249 getAccessibility n
1250 = case lookupDefAcc n False (tt_ctxt ist) of
1251 [(n,t)] -> t
1252 _ -> Public
1255 insertImpl :: [PArg] -> [PArg] -> [PArg]
1256 insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =
1257 PExp p l tm d : insertImpl ps given
1258 insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =
1259 PConstraint p l tm d : insertImpl ps given
1260 insertImpl (PConstraint p l ty d : ps) given =
1261 PConstraint p l (PResolveTC fc) d : insertImpl ps given
1262 insertImpl (PImp p _ l n ty d : ps) given =
1263 case find n given [] of
1264 Just (tm, given') -> PImp p False l n tm "" : insertImpl ps given'
1265 Nothing -> PImp p True l n Placeholder "" : insertImpl ps given
1266 insertImpl (PTacImplicit p l n sc ty d : ps) given =
1267 case find n given [] of
1268 Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'
1269 Nothing -> if inpat
1270 then PTacImplicit p l n sc Placeholder "" : insertImpl ps given
1271 else PTacImplicit p l n sc sc "" : insertImpl ps given
1272 insertImpl expected [] = []
1273 insertImpl _ given = given
1275 find n [] acc = Nothing
1276 find n (PImp _ _ _ n' t _ : gs) acc
1277 | n == n' = Just (t, reverse acc ++ gs)
1278 find n (PTacImplicit _ _ n' _ t _ : gs) acc
1279 | n == n' = Just (t, reverse acc ++ gs)
1280 find n (g : gs) acc = find n gs (g : acc)
1282-- replace non-linear occurrences with _
1283-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1284-- it is hard to get right!
1286stripLinear :: IState -> PTerm -> PTerm
1287stripLinear i tm = evalState (sl tm) [] where
1288 sl :: PTerm -> State [Name] PTerm
1289 sl (PRef fc f)
1290 | (_:_) <- lookupTy f (tt_ctxt i)
1291 = return $ PRef fc f
1292 | otherwise = do ns <- get
1293 if (f `elem` ns)
1294 then return Placeholder
1295 else do put (f : ns)
1296 return (PRef fc f)
1297 sl (PPatvar fc f)
1298 = do ns <- get
1299 if (f `elem` ns)
1300 then return Placeholder
1301 else do put (f : ns)
1302 return (PPatvar fc f)
1303 sl (PApp fc fn args) = do fn' <- sl fn
1304 args' <- mapM slA args
1305 return $ PApp fc fn' args'
1306 where slA (PImp p m l n t d) = do t' <- sl t
1307 return $ PImp p m l n t' d
1308 slA (PExp p l t d) = do t' <- sl t
1309 return $ PExp p l t' d
1310 slA (PConstraint p l t d)
1311 = do t' <- sl t
1312 return $ PConstraint p l t' d
1313 slA (PTacImplicit p l n sc t d)
1314 = do t' <- sl t
1315 return $ PTacImplicit p l n sc t' d
1316 sl x = return x
1318-- Remove functions which aren't applied to anything, which must then
1319-- be resolved by unification. Assume names resolved and alternatives
1320-- filled in (so no ambiguity).
1322stripUnmatchable :: IState -> PTerm -> PTerm
1323stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1324 su :: PTerm -> PTerm
1325 su (PRef fc f)
1326 | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1327 = Placeholder
1328 su (PApp fc fn args)
1329 = PApp fc fn (fmap (fmap su) args)
1330 su (PAlternative b alts)
1331 = let alts' = filter (/= Placeholder) (map su alts) in
1332 if null alts' then Placeholder
1333 else PAlternative b alts'
1334 su (PPair fc l r) = PPair fc (su l) (su r)
1335 su (PDPair fc l t r) = PDPair fc (su l) (su t) (su r)
1336 su t = t
1337stripUnmatchable i tm = tm
1339mkPApp fc a f [] = f
1340mkPApp fc a f as = let rest = drop a as in
1341 appRest fc (PApp fc f (take a as)) rest
1342 where
1343 appRest fc f [] = f
1344 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1346-- Find 'static' argument positions
1347-- (the declared ones, plus any names in argument position in the declared
1348-- statics)
1349-- FIXME: It's possible that this really has to happen after elaboration
1351findStatics :: IState -> PTerm -> (PTerm, [Bool])
1352findStatics ist tm = trace (showImp Nothing True False tm) $
1353 let (ns, ss) = fs tm in
1354 runState (pos ns ss tm) []
1355 where fs (PPi p n t sc)
1356 | Static <- pstatic p
1357 = let (ns, ss) = fs sc in
1358 (namesIn [] ist t : ns, n : ss)
1359 | otherwise = let (ns, ss) = fs sc in
1360 (ns, ss)
1361 fs _ = ([], [])
1363 inOne n ns = length (filter id (map (elem n) ns)) == 1
1365 pos ns ss (PPi p n t sc)
1366 | elem n ss = do sc' <- pos ns ss sc
1367 spos <- get
1368 put (True : spos)
1369 return (PPi (p { pstatic = Static }) n t sc')
1370 | otherwise = do sc' <- pos ns ss sc
1371 spos <- get
1372 put (False : spos)
1373 return (PPi p n t sc')
1374 pos ns ss t = return t
1376-- for 6.12/7 compatibility
1377data EitherErr a b = LeftErr a | RightOK b
1379instance Monad (EitherErr a) where
1380 return = RightOK
1382 (LeftErr e) >>= k = LeftErr e
1383 RightOK v >>= k = k v
1385toEither (LeftErr e) = Left e
1386toEither (RightOK ho) = Right ho
1388-- syntactic match of a against b, returning pair of variables in a
1389-- and what they match. Returns the pair that failed if not a match.
1391matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1392matchClause = matchClause' False
1394matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1395matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1396 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1398 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1399 fullApp x = x
1401 match' x y = match (fullApp x) (fullApp y)
1402 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
1403 | PConstant (I _) <- getTm x = match (getTm x) x'
1404 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
1405 | PConstant (I _) <- getTm x = match (getTm x) x'
1406 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
1407 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
1408 match (PApp _ f args) (PApp _ f' args')
1409 | length args == length args'
1410 = do mf <- match' f f'
1411 ms <- zipWithM matchArg args args'
1412 return (mf ++ concat ms)
1413-- match (PRef _ n) (PRef _ n') | n == n' = return []
1414-- | otherwise = Nothing
1415 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1416 match (PPatvar f n) xr = match (PRef f n) xr
1417 match xr (PPatvar f n) = match xr (PRef f n)
1418 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1419 match (PRef _ n) tm@(PRef _ n')
1420 | n == n' && not names &&
1421 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1422 || tm == Placeholder)
1423 = return [(n, tm)]
1424 | n == n' = return []
1425 match (PRef _ n) tm
1426 | not names && (not (isConName n (tt_ctxt i) ||
1427 isFnName n (tt_ctxt i)) || tm == Placeholder)
1428 = return [(n, tm)]
1429 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1430 mr <- match' r r'
1431 return (ml ++ mr)
1432 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1433 = do ml <- match' l l'
1434 mr <- match' r r'
1435 return (ml ++ mr)
1436 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1437 mr <- match r r'
1438 return (ml ++ mr)
1439 match (PTyped l r) x = match l x
1440 match x (PTyped l r) = match x l
1441 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1442 mr <- match' r r'
1443 return (ml ++ mr)
1444 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1445 mt <- match' t t'
1446 mr <- match' r r'
1447 return (ml ++ mt ++ mr)
1448 match (PAlternative a as) (PAlternative a' as')
1449 = do ms <- zipWithM match' as as'
1450 return (concat ms)
1451 match a@(PAlternative _ as) b
1452 = do let ms = zipWith match' as (repeat b)
1453 case (rights (map toEither ms)) of
1454 (x: _) -> return x
1455 _ -> LeftErr (a, b)
1456 match (PCase _ _ _) _ = return [] -- lifted out
1457 match (PMetavar _) _ = return [] -- modified
1458 match (PInferRef _ _) _ = return [] -- modified
1459 match (PQuote _) _ = return []
1460 match (PProof _) _ = return []
1461 match (PTactics _) _ = return []
1462 match (PRefl _ _) (PRefl _ _) = return []
1463 match (PResolveTC _) (PResolveTC _) = return []
1464 match (PTrue _) (PTrue _) = return []
1465 match (PFalse _) (PFalse _) = return []
1466 match (PReturn _) (PReturn _) = return []
1467 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1468 ms <- match' s s'
1469 return (mt ++ ms)
1470 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1471 ms <- match' s s'
1472 return (mt ++ ms)
1473 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1474 mty <- match' ty ty'
1475 ms <- match' s s'
1476 return (mt ++ mty ++ ms)
1477 match (PHidden x) (PHidden y) = match' x y
1478 match (PUnifyLog x) y = match' x y
1479 match x (PUnifyLog y) = match' x y
1480 match (PNoImplicits x) y = match' x y
1481 match x (PNoImplicits y) = match' x y
1482 match Placeholder _ = return []
1483 match _ Placeholder = return []
1484 match (PResolveTC _) _ = return []
1485 match a b | a == b = return []
1486 | otherwise = LeftErr (a, b)
1488 checkRpts (RightOK ms) = check ms where
1489 check ((n,t):xs)
1490 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1491 then Left (t, t')
1492 else check xs
1493 check (_:xs) = check xs
1494 check [] = Right ms
1495 checkRpts (LeftErr x) = Left x
1497substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1498substMatches ms = substMatchesShadow ms []
1500substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1501substMatchesShadow [] shs t = t
1502substMatchesShadow ((n,tm):ns) shs t
1503 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1505substMatch :: Name -> PTerm -> PTerm -> PTerm
1506substMatch n = substMatchShadow n []
1508substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1509substMatchShadow n shs tm t = sm shs t where
1510 sm xs (PRef _ n') | n == n' = tm
1511 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1512 sm xs (PPi p x t sc)
1513 | x `elem` xs
1514 = let x' = nextName x in
1515 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1516 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1517 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1518 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1519 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1520 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1521 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1522 (fmap (sm xs) tm)
1523 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1524 sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)
1525 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)
1526 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1527 sm xs (PHidden x) = PHidden (sm xs x)
1528 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1529 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1530 sm xs x = x
1532 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1533 fullApp x = x
1535shadow :: Name -> Name -> PTerm -> PTerm
1536shadow n n' t = sm t where
1537 sm (PRef fc x) | n == x = PRef fc n'
1538 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1539 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1540 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1541 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1542 sm (PEq f x y) = PEq f (sm x) (sm y)
1543 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1544 sm (PTyped x y) = PTyped (sm x) (sm y)
1545 sm (PPair f x y) = PPair f (sm x) (sm y)
1546 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1547 sm (PAlternative a as) = PAlternative a (map sm as)
1548 sm (PHidden x) = PHidden (sm x)
1549 sm (PUnifyLog x) = PUnifyLog (sm x)
1550 sm (PNoImplicits x) = PNoImplicits (sm x)
1551 sm x = x