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