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