git.iko.soy/Idris-dev
on c629b60 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1952 lines 81 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances, PatternGuards #-}
4module Idris.AbsSyntax(module Idris.AbsSyntax, module Idris.AbsSyntaxTree) where
6import Idris.Core.TT
7import Idris.Core.Evaluate
8import Idris.Core.Elaborate hiding (Tactic(..))
9import Idris.Core.Typecheck
10import Idris.AbsSyntaxTree
11import Idris.Colours
12import Idris.Docstrings
13import Idris.IdeSlave hiding (Opt(..))
14import IRTS.CodegenCommon
15import Util.DynamicLinker
17import System.Console.Haskeline
18import System.IO
20import Control.Applicative
21import Control.Monad.State
22import Control.Monad.Error(throwError)
24import Data.List
25import Data.Char
26import qualified Data.Text as T
27import Data.Either
28import qualified Data.Map as M
29import Data.Maybe
30import qualified Data.Set as S
31import Data.Word (Word)
33import Debug.Trace
35import Control.Monad.Error (throwError, catchError)
36import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
38import Util.Pretty
39import Util.ScreenSize
40import Util.System
42getContext :: Idris Context
43getContext = do i <- getIState; return (tt_ctxt i)
45forCodegen :: Codegen -> [(Codegen, a)] -> [a]
46forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']
48getObjectFiles :: Codegen -> Idris [FilePath]
49getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
51addObjectFile :: Codegen -> FilePath -> Idris ()
52addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
54getLibs :: Codegen -> Idris [String]
55getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
57addLib :: Codegen -> String -> Idris ()
58addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
60getFlags :: Codegen -> Idris [String]
61getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
63addFlag :: Codegen -> String -> Idris ()
64addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
66addDyLib :: [String] -> Idris (Either DynamicLib String)
67addDyLib libs = do i <- getIState
68 let ls = idris_dynamic_libs i
69 let importdirs = opt_importdirs (idris_options i)
70 case mapMaybe (findDyLib ls) libs of
71 x:_ -> return (Left x)
72 [] -> do
73 handle <- lift . lift .
74 mapM (\l -> catchIO (tryLoadLib importdirs l)
75 (\_ -> return Nothing)) $ libs
76 case msum handle of
77 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
78 concat (intersperse "," libs) ++ "\"")
79 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
80 return (Left x)
81 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
82 findDyLib [] l = Nothing
83 findDyLib (lib:libs) l | l == lib_name lib = Just lib
84 | otherwise = findDyLib libs l
86getAutoImports :: Idris [FilePath]
87getAutoImports = do i <- getIState
88 return (opt_autoImport (idris_options i))
90addAutoImport :: FilePath -> Idris ()
91addAutoImport fp = do i <- getIState
92 let opts = idris_options i
93 let autoimps = opt_autoImport opts
94 put (i { idris_options = opts { opt_autoImport =
95 fp : opt_autoImport opts } } )
97addHdr :: Codegen -> String -> Idris ()
98addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
100addImported :: FilePath -> Idris ()
101addImported f = do i <- getIState
102 putIState $ i { idris_imported = nub $ f : idris_imported i }
104addLangExt :: LanguageExt -> Idris ()
105addLangExt TypeProviders = do i <- getIState
106 putIState $ i {
107 idris_language_extensions = TypeProviders : idris_language_extensions i
108 }
109addLangExt ErrorReflection = do i <- getIState
110 putIState $ i {
111 idris_language_extensions = ErrorReflection : idris_language_extensions i
112 }
114addTrans :: (Term, Term) -> Idris ()
115addTrans t = do i <- getIState
116 putIState $ i { idris_transforms = t : idris_transforms i }
118addErrRev :: (Term, Term) -> Idris ()
119addErrRev t = do i <- getIState
120 putIState $ i { idris_errRev = t : idris_errRev i }
122totcheck :: (FC, Name) -> Idris ()
123totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
125defer_totcheck :: (FC, Name) -> Idris ()
126defer_totcheck n
127 = do i <- getIState;
128 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
130clear_totcheck :: Idris ()
131clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
133setFlags :: Name -> [FnOpt] -> Idris ()
134setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
136setFnInfo :: Name -> FnInfo -> Idris ()
137setFnInfo n fs = do i <- getIState; putIState $ i { idris_fninfo = addDef n fs (idris_fninfo i) }
139setAccessibility :: Name -> Accessibility -> Idris ()
140setAccessibility n a
141 = do i <- getIState
142 let ctxt = setAccess n a (tt_ctxt i)
143 putIState $ i { tt_ctxt = ctxt }
145setTotality :: Name -> Totality -> Idris ()
146setTotality n a
147 = do i <- getIState
148 let ctxt = setTotal n a (tt_ctxt i)
149 putIState $ i { tt_ctxt = ctxt }
151getTotality :: Name -> Idris Totality
152getTotality n
153 = do i <- getIState
154 case lookupTotal n (tt_ctxt i) of
155 [t] -> return t
156 _ -> return (Total [])
158-- Get coercions which might return the required type
159getCoercionsTo :: IState -> Type -> [Name]
160getCoercionsTo i ty =
161 let cs = idris_coercions i
162 (fn,_) = unApply (getRetTy ty) in
163 findCoercions fn cs
164 where findCoercions t [] = []
165 findCoercions t (n : ns) =
166 let ps = case lookupTy n (tt_ctxt i) of
167 [ty'] -> case unApply (getRetTy ty') of
168 (t', _) ->
169 if t == t' then [n] else []
170 _ -> [] in
171 ps ++ findCoercions t ns
173addToCG :: Name -> CGInfo -> Idris ()
174addToCG n cg
175 = do i <- getIState
176 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
178addTyInferred :: Name -> Idris ()
179addTyInferred n
180 = do i <- getIState
181 putIState $ i { idris_tyinfodata =
182 addDef n TIPartial (idris_tyinfodata i) }
184addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()
185addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts
186 mapM_ addConstraint ts
187 return ()
188 where addConstraint (x, y) = findMVApps x y
190 findMVApps x y
191 = do let (fx, argsx) = unApply x
192 let (fy, argsy) = unApply y
193 if (not (fx == fy))
194 then do
195 tryAddMV fx y
196 tryAddMV fy x
197 else mapM_ addConstraint (zip argsx argsy)
199 tryAddMV (P _ mv _) y =
200 do ist <- get
201 case lookup mv (idris_metavars ist) of
202 Just _ -> addConstraintRule mv y
203 _ -> return ()
204 tryAddMV _ _ = return ()
206 addConstraintRule :: Name -> Term -> Idris ()
207 addConstraintRule n t
208 = do ist <- get
209 logLvl 1 $ "TI constraint: " ++ show (n, t)
210 case lookupCtxt n (idris_tyinfodata ist) of
211 [TISolution ts] ->
212 do mapM_ (checkConsistent t) ts
213 let ti' = addDef n (TISolution (t : ts))
214 (idris_tyinfodata ist)
215 put $ ist { idris_tyinfodata = ti' }
216 _ ->
217 do let ti' = addDef n (TISolution [t])
218 (idris_tyinfodata ist)
219 put $ ist { idris_tyinfodata = ti' }
221 -- Check a solution is consistent with previous solutions
222 -- Meaning: If heads are both data types, they had better be the
223 -- same.
224 checkConsistent :: Term -> Term -> Idris ()
225 checkConsistent x y =
226 do let (fx, _) = unApply x
227 let (fy, _) = unApply y
228 case (fx, fy) of
229 (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)
230 (P (TCon _ _) n _, Constant _) -> errWhen True
231 (Constant _, P (TCon _ _) n' _) -> errWhen True
232 (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n)
233 _ -> return ()
235 where errWhen True
236 = throwError (At fc
237 (CantUnify False x y (Msg "") [] 0))
238 errWhen False = return ()
240isTyInferred :: Name -> Idris Bool
241isTyInferred n
242 = do i <- getIState
243 case lookupCtxt n (idris_tyinfodata i) of
244 [TIPartial] -> return True
245 _ -> return False
247-- | Adds error handlers for a particular function and argument. If names are
248-- ambiguous, all matching handlers are updated.
249addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()
250addFunctionErrorHandlers f arg hs =
251 do i <- getIState
252 let oldHandlers = idris_function_errorhandlers i
253 let newHandlers = flip (addDef f) oldHandlers $
254 case lookupCtxtExact f oldHandlers of
255 Nothing -> M.singleton arg (S.fromList hs)
256 Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers
257 -- will always be one of those two, thus no extra case
258 putIState $ i { idris_function_errorhandlers = newHandlers }
260getFunctionErrorHandlers :: Name -> Name -> Idris [Name]
261getFunctionErrorHandlers f arg = do i <- getIState
262 return . maybe [] S.toList $
263 undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)
266-- Trace all the names in a call graph starting at the given name
267getAllNames :: Name -> Idris [Name]
268getAllNames n = allNames [] n
270allNames :: [Name] -> Name -> Idris [Name]
271allNames ns n | n `elem` ns = return []
272allNames ns n = do i <- getIState
273 case lookupCtxtExact n (idris_callgraph i) of
274 Just ns' -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
275 return (nub (n : concat more))
276 _ -> return [n]
278addCoercion :: Name -> Idris ()
279addCoercion n = do i <- getIState
280 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
282addDocStr :: Name -> Docstring -> [(Name, Docstring)] -> Idris ()
283addDocStr n doc args
284 = do i <- getIState
285 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }
287addNameHint :: Name -> Name -> Idris ()
288addNameHint ty n
289 = do i <- getIState
290 ty' <- case lookupCtxtName ty (idris_implicits i) of
291 [(tyn, _)] -> return tyn
292 [] -> throwError (NoSuchVariable ty)
293 tyns -> throwError (CantResolveAlts (map fst tyns))
294 let ns' = case lookupCtxt ty' (idris_namehints i) of
295 [ns] -> ns ++ [n]
296 _ -> [n]
297 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
299getNameHints :: IState -> Name -> [Name]
300getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
301getNameHints i n =
302 case lookupCtxt n (idris_namehints i) of
303 [ns] -> ns
304 _ -> []
306addToCalledG :: Name -> [Name] -> Idris ()
307addToCalledG n ns = return () -- TODO
309-- Add a class instance function. Dodgy hack: Put integer instances first in the
310-- list so they are resolved by default.
311-- Dodgy hack 2: put constraint chasers (@@) last
313addInstance :: Bool -> Name -> Name -> Idris ()
314addInstance int n i
315 = do ist <- getIState
316 case lookupCtxt n (idris_classes ist) of
317 [CI a b c d e ins] ->
318 do let cs = addDef n (CI a b c d e (addI i ins)) (idris_classes ist)
319 putIState $ ist { idris_classes = cs }
320 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [i]) (idris_classes ist)
321 putIState $ ist { idris_classes = cs }
322 where addI i ins | int = i : ins
323 | chaser n = ins ++ [i]
324 | otherwise = insI i ins
325 insI i [] = [i]
326 insI i (n : ns) | chaser n = i : n : ns
327 | otherwise = n : insI i ns
329 chaser (UN nm)
330 | ('@':'@':_) <- str nm = True
331 chaser (NS n _) = chaser n
332 chaser _ = False
334addClass :: Name -> ClassInfo -> Idris ()
335addClass n i
336 = do ist <- getIState
337 let i' = case lookupCtxt n (idris_classes ist) of
338 [c] -> c { class_instances = class_instances i }
339 _ -> i
340 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
342addIBC :: IBCWrite -> Idris ()
343addIBC ibc@(IBCDef n)
344 = do i <- getIState
345 when (notDef (ibc_write i)) $
346 putIState $ i { ibc_write = ibc : ibc_write i }
347 where notDef [] = True
348 notDef (IBCDef n': is) | n == n' = False
349 notDef (_ : is) = notDef is
350addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
352clearIBC :: Idris ()
353clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
355resetNameIdx :: Idris ()
356resetNameIdx = do i <- getIState
357 put (i { idris_nameIdx = (0, emptyContext) })
359-- Used to preserve sharing of names
360addNameIdx :: Name -> Idris (Int, Name)
361addNameIdx n = do i <- getIState
362 let (i', x) = addNameIdx' i n
363 return x
365addNameIdx' :: IState -> Name -> (IState, (Int, Name))
366addNameIdx' i n
367 = let idxs = snd (idris_nameIdx i) in
368 case lookupCtxt n idxs of
369 [x] -> (i, x)
370 _ -> let i' = fst (idris_nameIdx i) + 1 in
371 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
373getHdrs :: Codegen -> Idris [String]
374getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
376getImported :: Idris [FilePath]
377getImported = do i <- getIState; return (idris_imported i)
379setErrSpan :: FC -> Idris ()
380setErrSpan x = do i <- getIState;
381 case (errSpan i) of
382 Nothing -> putIState $ i { errSpan = Just x }
383 Just _ -> return ()
385clearErr :: Idris ()
386clearErr = do i <- getIState
387 putIState $ i { errSpan = Nothing }
389getSO :: Idris (Maybe String)
390getSO = do i <- getIState
391 return (compiled_so i)
393setSO :: Maybe String -> Idris ()
394setSO s = do i <- getIState
395 putIState $ (i { compiled_so = s })
397getIState :: Idris IState
398getIState = get
400putIState :: IState -> Idris ()
401putIState = put
403withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
404withContext ctx name dflt action = do
405 ist <- getIState
406 case lookupCtxt name (ctx ist) of
407 [x] -> action x
408 _ -> return dflt
410withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()
411withContext_ ctx name action = withContext ctx name () action
413-- | A version of liftIO that puts errors into the exception type of the Idris monad
414runIO :: IO a -> Idris a
415runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
416-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
418getName :: Idris Int
419getName = do i <- getIState;
420 let idx = idris_name i;
421 putIState $ (i { idris_name = idx + 1 })
422 return idx
424-- InternalApp keeps track of the real function application for making case splits from, not the application the
425-- programmer wrote, which doesn't have the whole context in any case other than top level definitions
426addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
427addInternalApp fp l t
428 = do i <- getIState
429 putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })
431getInternalApp :: FilePath -> Int -> Idris PTerm
432getInternalApp fp l = do i <- getIState
433 case lookup (fp, l) (idris_lineapps i) of
434 Just n' -> return n'
435 Nothing -> return Placeholder
436 -- TODO: What if it's not there?
438-- Pattern definitions are only used for coverage checking, so erase them
439-- when we're done
440clearOrigPats :: Idris ()
441clearOrigPats = do i <- get
442 let ps = idris_patdefs i
443 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
444 put (i { idris_patdefs = ps' })
446-- Erase types from Ps in the context (basically ending up with what's in
447-- the .ibc, which is all we need after all the analysis is done)
448clearPTypes :: Idris ()
449clearPTypes = do i <- get
450 let ctxt = tt_ctxt i
451 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
452 where pErase (CaseOp c t tys orig tot cds)
453 = CaseOp c t tys orig [] (pErase' cds)
454 pErase x = x
455 pErase' (CaseDefs _ (cs, c) _ rs)
456 = let c' = (cs, fmap pEraseType c) in
457 CaseDefs c' c' c' rs
459checkUndefined :: FC -> Name -> Idris ()
460checkUndefined fc n
461 = do i <- getContext
462 case lookupTy n i of
463 (_:_) -> throwError . Msg $ show fc ++ ":" ++
464 show n ++ " already defined"
465 _ -> return ()
467isUndefined :: FC -> Name -> Idris Bool
468isUndefined fc n
469 = do i <- getContext
470 case lookupTy n i of
471 (_:_) -> return False
472 _ -> return True
474setContext :: Context -> Idris ()
475setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
477updateContext :: (Context -> Context) -> Idris ()
478updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
480addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
481addConstraints fc (v, cs)
482 = do i <- getIState
483 let ctxt = tt_ctxt i
484 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
485 next_tvar = v }
486 let ics = zip cs (repeat fc) ++ idris_constraints i
487 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
489addDeferred = addDeferred' Ref
490addDeferredTyCon = addDeferred' (TCon 0 0)
492addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
493addDeferred' nt ns
494 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns
495 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
496 i <- getIState
497 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
498 idris_metavars i }
499 where
500 -- 'tidyNames' is to generate user accessible names in case they are
501 -- needed in tactic scripts
502 tidyNames used (Bind (MN i x) b sc)
503 = let n' = uniqueName (UN x) used in
504 Bind n' b $ tidyNames (n':used) sc
505 tidyNames used (Bind n b sc)
506 = let n' = uniqueName n used in
507 Bind n' b $ tidyNames (n':used) sc
508 tidyNames used b = b
510solveDeferred :: Name -> Idris ()
511solveDeferred n = do i <- getIState
512 putIState $ i { idris_metavars =
513 filter (\(n', _) -> n/=n')
514 (idris_metavars i),
515 ibc_write =
516 filter (notMV n) (ibc_write i)
517 }
518 where notMV n (IBCMetavar n') = not (n == n')
519 notMV n _ = True
521getUndefined :: Idris [Name]
522getUndefined = do i <- getIState
523 return (map fst (idris_metavars i) \\ primDefs)
525isMetavarName :: Name -> IState -> Bool
526isMetavarName n ist
527 = case lookupNames n (tt_ctxt ist) of
528 (t:_) -> isJust $ lookup t (idris_metavars ist)
529 _ -> False
531getWidth :: Idris ConsoleWidth
532getWidth = fmap idris_consolewidth getIState
534setWidth :: ConsoleWidth -> Idris ()
535setWidth w = do ist <- getIState
536 put ist { idris_consolewidth = w }
538renderWidth :: Idris Int
539renderWidth = do iw <- getWidth
540 case iw of
541 InfinitelyWide -> return 100000000
542 ColsWide n -> return (max n 1)
543 AutomaticWidth -> runIO getScreenWidth
547type1Doc :: Doc OutputAnnotation
548type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
551isetPrompt :: String -> Idris ()
552isetPrompt p = do i <- getIState
553 case idris_outputmode i of
554 IdeSlave n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n
556-- | Tell clients how much was parsed and loaded
557isetLoadedRegion :: Idris ()
558isetLoadedRegion = do i <- getIState
559 let span = idris_parsedSpan i
560 case span of
561 Just fc ->
562 case idris_outputmode i of
563 IdeSlave n h ->
564 runIO . hPutStrLn h $
565 convSExp "set-loaded-region" fc n
566 Nothing -> return ()
568setLogLevel :: Int -> Idris ()
569setLogLevel l = do i <- getIState
570 let opts = idris_options i
571 let opt' = opts { opt_logLevel = l }
572 putIState $ i { idris_options = opt' }
574setCmdLine :: [Opt] -> Idris ()
575setCmdLine opts = do i <- getIState
576 let iopts = idris_options i
577 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
579getCmdLine :: Idris [Opt]
580getCmdLine = do i <- getIState
581 return (opt_cmdline (idris_options i))
583getDumpDefun :: Idris (Maybe FilePath)
584getDumpDefun = do i <- getIState
585 return $ findC (opt_cmdline (idris_options i))
586 where findC [] = Nothing
587 findC (DumpDefun x : _) = Just x
588 findC (_ : xs) = findC xs
590getDumpCases :: Idris (Maybe FilePath)
591getDumpCases = do i <- getIState
592 return $ findC (opt_cmdline (idris_options i))
593 where findC [] = Nothing
594 findC (DumpCases x : _) = Just x
595 findC (_ : xs) = findC xs
597logLevel :: Idris Int
598logLevel = do i <- getIState
599 return (opt_logLevel (idris_options i))
601setErrContext :: Bool -> Idris ()
602setErrContext t = do i <- getIState
603 let opts = idris_options i
604 let opt' = opts { opt_errContext = t }
605 putIState $ i { idris_options = opt' }
607errContext :: Idris Bool
608errContext = do i <- getIState
609 return (opt_errContext (idris_options i))
611useREPL :: Idris Bool
612useREPL = do i <- getIState
613 return (opt_repl (idris_options i))
615setREPL :: Bool -> Idris ()
616setREPL t = do i <- getIState
617 let opts = idris_options i
618 let opt' = opts { opt_repl = t }
619 putIState $ i { idris_options = opt' }
621showOrigErr :: Idris Bool
622showOrigErr = do i <- getIState
623 return (opt_origerr (idris_options i))
625setShowOrigErr :: Bool -> Idris ()
626setShowOrigErr b = do i <- getIState
627 let opts = idris_options i
628 let opt' = opts { opt_origerr = b }
629 putIState $ i { idris_options = opt' }
631setAutoSolve :: Bool -> Idris ()
632setAutoSolve b = do i <- getIState
633 let opts = idris_options i
634 let opt' = opts { opt_autoSolve = b }
635 putIState $ i { idris_options = opt' }
637setNoBanner :: Bool -> Idris ()
638setNoBanner n = do i <- getIState
639 let opts = idris_options i
640 let opt' = opts { opt_nobanner = n }
641 putIState $ i { idris_options = opt' }
643getNoBanner :: Idris Bool
644getNoBanner = do i <- getIState
645 let opts = idris_options i
646 return (opt_nobanner opts)
648setQuiet :: Bool -> Idris ()
649setQuiet q = do i <- getIState
650 let opts = idris_options i
651 let opt' = opts { opt_quiet = q }
652 putIState $ i { idris_options = opt' }
654getQuiet :: Idris Bool
655getQuiet = do i <- getIState
656 let opts = idris_options i
657 return (opt_quiet opts)
659setCodegen :: Codegen -> Idris ()
660setCodegen t = do i <- getIState
661 let opts = idris_options i
662 let opt' = opts { opt_codegen = t }
663 putIState $ i { idris_options = opt' }
665codegen :: Idris Codegen
666codegen = do i <- getIState
667 return (opt_codegen (idris_options i))
669setOutputTy :: OutputType -> Idris ()
670setOutputTy t = do i <- getIState
671 let opts = idris_options i
672 let opt' = opts { opt_outputTy = t }
673 putIState $ i { idris_options = opt' }
675outputTy :: Idris OutputType
676outputTy = do i <- getIState
677 return $ opt_outputTy $ idris_options i
679setIdeSlave :: Bool -> Handle -> Idris ()
680setIdeSlave True h = do i <- getIState
681 putIState $ i { idris_outputmode = (IdeSlave 0 h), idris_colourRepl = False }
682setIdeSlave False _ = return ()
684setTargetTriple :: String -> Idris ()
685setTargetTriple t = do i <- getIState
686 let opts = idris_options i
687 opt' = opts { opt_triple = t }
688 putIState $ i { idris_options = opt' }
690targetTriple :: Idris String
691targetTriple = do i <- getIState
692 return (opt_triple (idris_options i))
694setTargetCPU :: String -> Idris ()
695setTargetCPU t = do i <- getIState
696 let opts = idris_options i
697 opt' = opts { opt_cpu = t }
698 putIState $ i { idris_options = opt' }
700targetCPU :: Idris String
701targetCPU = do i <- getIState
702 return (opt_cpu (idris_options i))
704setOptLevel :: Word -> Idris ()
705setOptLevel t = do i <- getIState
706 let opts = idris_options i
707 opt' = opts { opt_optLevel = t }
708 putIState $ i { idris_options = opt' }
710optLevel :: Idris Word
711optLevel = do i <- getIState
712 return (opt_optLevel (idris_options i))
714verbose :: Idris Bool
715verbose = do i <- getIState
716 return (opt_verbose (idris_options i))
718setVerbose :: Bool -> Idris ()
719setVerbose t = do i <- getIState
720 let opts = idris_options i
721 let opt' = opts { opt_verbose = t }
722 putIState $ i { idris_options = opt' }
724typeInType :: Idris Bool
725typeInType = do i <- getIState
726 return (opt_typeintype (idris_options i))
728setTypeInType :: Bool -> Idris ()
729setTypeInType t = do i <- getIState
730 let opts = idris_options i
731 let opt' = opts { opt_typeintype = t }
732 putIState $ i { idris_options = opt' }
734coverage :: Idris Bool
735coverage = do i <- getIState
736 return (opt_coverage (idris_options i))
738setCoverage :: Bool -> Idris ()
739setCoverage t = do i <- getIState
740 let opts = idris_options i
741 let opt' = opts { opt_coverage = t }
742 putIState $ i { idris_options = opt' }
744setIBCSubDir :: FilePath -> Idris ()
745setIBCSubDir fp = do i <- getIState
746 let opts = idris_options i
747 let opt' = opts { opt_ibcsubdir = fp }
748 putIState $ i { idris_options = opt' }
750valIBCSubDir :: IState -> Idris FilePath
751valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
753addImportDir :: FilePath -> Idris ()
754addImportDir fp = do i <- getIState
755 let opts = idris_options i
756 let opt' = opts { opt_importdirs = nub $ fp : opt_importdirs opts }
757 putIState $ i { idris_options = opt' }
759setImportDirs :: [FilePath] -> Idris ()
760setImportDirs fps = do i <- getIState
761 let opts = idris_options i
762 let opt' = opts { opt_importdirs = fps }
763 putIState $ i { idris_options = opt' }
765allImportDirs :: Idris [FilePath]
766allImportDirs = do i <- getIState
767 let optdirs = opt_importdirs (idris_options i)
768 return ("." : reverse optdirs)
770colourise :: Idris Bool
771colourise = do i <- getIState
772 return $ idris_colourRepl i
774setColourise :: Bool -> Idris ()
775setColourise b = do i <- getIState
776 putIState $ i { idris_colourRepl = b }
778impShow :: Idris Bool
779impShow = do i <- getIState
780 return (opt_showimp (idris_options i))
782setImpShow :: Bool -> Idris ()
783setImpShow t = do i <- getIState
784 let opts = idris_options i
785 let opt' = opts { opt_showimp = t }
786 putIState $ i { idris_options = opt' }
788setColour :: ColourType -> IdrisColour -> Idris ()
789setColour ct c = do i <- getIState
790 let newTheme = setColour' ct c (idris_colourTheme i)
791 putIState $ i { idris_colourTheme = newTheme }
792 where setColour' KeywordColour c t = t { keywordColour = c }
793 setColour' BoundVarColour c t = t { boundVarColour = c }
794 setColour' ImplicitColour c t = t { implicitColour = c }
795 setColour' FunctionColour c t = t { functionColour = c }
796 setColour' TypeColour c t = t { typeColour = c }
797 setColour' DataColour c t = t { dataColour = c }
798 setColour' PromptColour c t = t { promptColour = c }
799 setColour' PostulateColour c t = t { postulateColour = c }
801logLvl :: Int -> String -> Idris ()
802logLvl l str = do i <- getIState
803 let lvl = opt_logLevel (idris_options i)
804 when (lvl >= l) $
805 case idris_outputmode i of
806 RawOutput h -> do runIO $ hPutStrLn h str
807 IdeSlave n h ->
808 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
809 runIO . hPutStrLn h $ convSExp "log" good n
811cmdOptType :: Opt -> Idris Bool
812cmdOptType x = do i <- getIState
813 return $ x `elem` opt_cmdline (idris_options i)
815iLOG :: String -> Idris ()
816iLOG = logLvl 1
818noErrors :: Idris Bool
819noErrors = do i <- getIState
820 case errSpan i of
821 Nothing -> return True
822 _ -> return False
824setTypeCase :: Bool -> Idris ()
825setTypeCase t = do i <- getIState
826 let opts = idris_options i
827 let opt' = opts { opt_typecase = t }
828 putIState $ i { idris_options = opt' }
831-- Dealing with parameters
833expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
834 [Name] -> -- all names
835 [Name] -> -- names with no declaration
836 PTerm -> PTerm
837expandParams dec ps ns infs tm = en tm
838 where
839 -- if we shadow a name (say in a lambda binding) that is used in a call to
840 -- a lifted function, we need access to both names - once in the scope of the
841 -- binding and once to call the lifted functions. So we'll explicitly shadow
842 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
843 -- but we didn't...)
845 mkShadow (UN n) = MN 0 n
846 mkShadow (MN i n) = MN (i+1) n
847 mkShadow (NS x s) = NS (mkShadow x) s
849 en (PLam n t s)
850 | n `elem` (map fst ps ++ ns)
851 = let n' = mkShadow n in
852 PLam n' (en t) (en (shadow n n' s))
853 | otherwise = PLam n (en t) (en s)
854 en (PPi p n t s)
855 | n `elem` (map fst ps ++ ns)
856 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
857 PPi (enTacImp p) n' (en t) (en (shadow n n' s))
858 | otherwise = PPi (enTacImp p) n (en t) (en s)
859 en (PLet n ty v s)
860 | n `elem` (map fst ps ++ ns)
861 = let n' = mkShadow n in
862 PLet n' (en ty) (en v) (en (shadow n n' s))
863 | otherwise = PLet n (en ty) (en v) (en s)
864 -- FIXME: Should only do this in a type signature!
865 en (PDPair f p (PRef f' n) t r)
866 | n `elem` (map fst ps ++ ns) && t /= Placeholder
867 = let n' = mkShadow n in
868 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))
869 en (PEq f lt rt l r) = PEq f (en lt) (en rt) (en l) (en r)
870 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
871 en (PTyped l r) = PTyped (en l) (en r)
872 en (PPair f p l r) = PPair f p (en l) (en r)
873 en (PDPair f p l t r) = PDPair f p (en l) (en t) (en r)
874 en (PAlternative a as) = PAlternative a (map en as)
875 en (PHidden t) = PHidden (en t)
876 en (PUnifyLog t) = PUnifyLog (en t)
877 en (PDisamb ds t) = PDisamb ds (en t)
878 en (PNoImplicits t) = PNoImplicits (en t)
879 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
880 en (PProof ts) = PProof (map (fmap en) ts)
881 en (PTactics ts) = PTactics (map (fmap en) ts)
883 en (PQuote (Var n))
884 | n `nselem` ns = PQuote (Var (dec n))
885 en (PApp fc (PInferRef fc' n) as)
886 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
887 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
888 en (PApp fc (PRef fc' n) as)
889 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
890 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
891 | n `nselem` ns = PApp fc (PRef fc' (dec n))
892 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
893 en (PAppBind fc (PRef fc' n) as)
894 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
895 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
896 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
897 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
898 en (PRef fc n)
899 | n `elem` infs = PApp fc (PInferRef fc (dec n))
900 (map (pexp . (PRef fc)) (map fst ps))
901 | n `nselem` ns = PApp fc (PRef fc (dec n))
902 (map (pexp . (PRef fc)) (map fst ps))
903 en (PInferRef fc n)
904 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
905 (map (pexp . (PRef fc)) (map fst ps))
906 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
907 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
908 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
909 en t = t
911 nselem x [] = False
912 nselem x (y : xs) | nseq x y = True
913 | otherwise = nselem x xs
915 nseq x y = nsroot x == nsroot y
917 enTacImp (TacImp aos st scr) = TacImp aos st (en scr)
918 enTacImp other = other
920expandParamsD :: Bool -> -- True = RHS only
921 IState ->
922 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
923expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty)
924 = if n `elem` ns && (not rhsonly)
925 then -- trace (show (n, expandParams dec ps ns ty)) $
926 PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
927 else --trace (show (n, expandParams dec ps ns ty)) $
928 PTy doc argdocs syn fc o n (expandParams dec ps ns [] ty)
929expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
930 = if n `elem` ns && (not rhsonly)
931 then -- trace (show (n, expandParams dec ps ns ty)) $
932 PPostulate doc syn fc o (dec n) (piBind ps
933 (expandParams dec ps ns [] ty))
934 else --trace (show (n, expandParams dec ps ns ty)) $
935 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
936expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
937 = let n' = if n `elem` ns then dec n else n in
938 PClauses fc opts n' (map expandParamsC cs)
939 where
940 expandParamsC (PClause fc n lhs ws rhs ds)
941 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
942 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
943 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
944 n' = if n `elem` ns then dec n else n
945 -- names bound on the lhs should not be expanded on the rhs
946 ns' = removeBound lhs ns in
947 PClause fc n' lhs'
948 (map (expandParams dec ps'' ns' []) ws)
949 (expandParams dec ps'' ns' [] rhs)
950 (map (expandParamsD True ist dec ps'' ns') ds)
951 expandParamsC (PWith fc n lhs ws wval ds)
952 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
953 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
954 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
955 n' = if n `elem` ns then dec n else n
956 ns' = removeBound lhs ns in
957 PWith fc n' lhs'
958 (map (expandParams dec ps'' ns' []) ws)
959 (expandParams dec ps'' ns' [] wval)
960 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
961 updateps yn nm [] = []
962 updateps yn nm (((a, t), i):as)
963 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
964 | otherwise = (sMN i ('_' : show n ++ "_u"), t) : updateps yn nm as
966 removeBound lhs ns = ns \\ nub (bnames lhs)
968 bnames (PRef _ n) = [n]
969 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
970 bnames (PPair _ _ l r) = bnames l ++ bnames r
971 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r
972 bnames _ = []
974-- | Expands parameters defined in parameter and where blocks inside of declarations
975expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
976 = PData doc argDocs syn fc co (expandPData pd)
977 where
978 -- just do the type decl, leave constructors alone (parameters will be
979 -- added implicitly)
980 expandPData (PDatadecl n ty cons)
981 = if n `elem` ns
982 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
983 (map econ cons)
984 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
985 econ (doc, argDocs, n, t, fc, fs)
986 = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
987expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty opts cdoc cn cty)
988 = if tn `elem` ns
989 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))
990 opts cdoc (dec cn) conty
991 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)
992 opts cdoc (dec cn) conty
993 where conty = piBindp expl ps (expandParams dec ps ns [] cty)
994expandParamsD rhs ist dec ps ns (PParams f params pds)
995 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
996 (map (expandParamsD True ist dec ps ns) pds)
997-- (map (expandParamsD ist dec ps ns) pds)
998expandParamsD rhs ist dec ps ns (PMutual f pds)
999 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
1000expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs decls)
1001 = PClass doc info f
1002 (map (expandParams dec ps ns []) cs)
1004 (map (mapsnd (expandParams dec ps ns [])) params)
1005 pDocs
1006 (map (expandParamsD rhs ist dec ps ns) decls)
1007expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
1008 = PInstance info f
1009 (map (expandParams dec ps ns []) cs)
1011 (map (expandParams dec ps ns []) params)
1012 (expandParams dec ps ns [] ty)
1013 cn
1014 (map (expandParamsD rhs ist dec ps ns) decls)
1015expandParamsD rhs ist dec ps ns d = d
1017mapsnd f (x, t) = (x, f t)
1019-- Calculate a priority for a type, for deciding elaboration order
1020-- * if it's just a type variable or concrete type, do it early (0)
1021-- * if there's only type variables and injective constructors, do it next (1)
1022-- * if there's a function type, next (2)
1023-- * finally, everything else (3)
1025getPriority :: IState -> PTerm -> Int
1026getPriority i tm = 1 -- pri tm
1027 where
1028 pri (PRef _ n) =
1029 case lookupP n (tt_ctxt i) of
1030 ((P (DCon _ _ _) _ _):_) -> 1
1031 ((P (TCon _ _) _ _):_) -> 1
1032 ((P Ref _ _):_) -> 1
1033 [] -> 0 -- must be locally bound, if it's not an error...
1034 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1035 pri (PTrue _ _) = 0
1036 pri (PFalse _) = 0
1037 pri (PRefl _ _) = 1
1038 pri (PEq _ _ _ l r) = max 1 (max (pri l) (pri r))
1039 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
1040 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1041 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1042 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1043 pri (PTyped l r) = pri l
1044 pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))
1045 pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1046 pri (PAlternative a as) = maximum (map pri as)
1047 pri (PConstant _) = 0
1048 pri Placeholder = 1
1049 pri _ = 3
1052addStatics :: Name -> Term -> PTerm -> Idris ()
1053addStatics n tm ptm =
1054 do let (statics, dynamics) = initStatics tm ptm
1055 let stnames = nub $ concatMap freeArgNames (map snd statics)
1056 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
1057 -- also get the arguments which are 'uniquely inferrable' from
1058 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1059 let statics' = nub $ map fst statics ++
1060 filter (\x -> not (elem x dnames)) stnames
1061 let stpos = staticList statics' tm
1062 i <- getIState
1063 when (not (null statics)) $
1064 logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics
1065 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
1066 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1067 addIBC (IBCStatic n)
1068 where
1069 initStatics (Bind n (Pi ty _) sc) (PPi p _ _ s)
1070 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1071 if pstatic p == Static then ((n, ty) : static, dynamic)
1072 else if (not (searchArg p))
1073 then (static, (n, ty) : dynamic)
1074 else (static, dynamic)
1075 initStatics t pt = ([], [])
1077 freeArgNames (Bind n (Pi ty _) sc)
1078 = nub $ freeArgNames ty
1079 freeArgNames tm = let (_, args) = unApply tm in
1080 concatMap freeNames args
1082 -- if a name appears in a type class or tactic implicit index, it doesn't
1083 -- affect its 'uniquely inferrable' from a static status since these are
1084 -- resolved by searching.
1085 searchArg (Constraint _ _) = True
1086 searchArg (TacImp _ _ _) = True
1087 searchArg _ = False
1089 staticList sts (Bind n (Pi _ _) sc) = (n `elem` sts) : staticList sts sc
1090 staticList _ _ = []
1092-- Dealing with implicit arguments
1094-- Add some bound implicits to the using block if they aren't there already
1096addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1097addToUsing us [] = us
1098addToUsing us ((n, t) : ns)
1099 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1100 | otherwise = addToUsing us ns
1101 where impName (UImplicit n _) = Just n
1102 impName _ = Nothing
1104-- Add constraint bindings from using block
1106addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1107addUsingConstraints syn fc t
1108 = do ist <- get
1109 let ns = namesIn [] ist t
1110 let cs = getConstraints t -- check declared constraints
1111 let addconsts = uconsts \\ cs
1112 return (doAdd addconsts ns t)
1113 where uconsts = filter uconst (using syn)
1114 uconst (UConstraint _ _) = True
1115 uconst _ = False
1117 doAdd [] _ t = t
1118 -- if all of args in ns, then add it
1119 doAdd (UConstraint c args : cs) ns t
1120 | all (\n -> elem n ns) args
1121 = PPi (Constraint [] Dynamic) (sMN 0 "cu")
1122 (mkConst c args) (doAdd cs ns t)
1123 | otherwise = doAdd cs ns t
1125 mkConst c args = PApp fc (PRef fc c)
1126 (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc n)) args)
1128 getConstraints (PPi (Constraint _ _) _ c sc)
1129 = getcapp c ++ getConstraints sc
1130 getConstraints (PPi _ _ c sc) = getConstraints sc
1131 getConstraints _ = []
1133 getcapp (PApp _ (PRef _ c) args)
1134 = do ns <- mapM getName args
1135 return (UConstraint c ns)
1136 getcapp _ = []
1138 getName (PExp _ _ _ (PRef _ n)) = return n
1139 getName _ = []
1141-- Add implicit bindings from using block, and bind any missing names
1142addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1143addUsingImpls syn n fc t
1144 = do ist <- getIState
1145 let ns = implicitNamesIn (map iname uimpls) ist t
1146 let badnames = filter (\n -> not (implicitable n) &&
1147 n `notElem` (map iname uimpls)) ns
1148 when (not (null badnames)) $
1149 throwError (At fc (Elaborating "type of " n
1150 (NoSuchVariable (head badnames))))
1151 let cs = getArgnames t -- get already bound names
1152 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1153 -- if all names in the arguments of addconsts appear in ns,
1154 -- add the constraint implicitly
1155 return (bindFree ns (doAdd addimpls ns t))
1156 where uimpls = filter uimpl (using syn)
1157 uimpl (UImplicit _ _) = True
1158 uimpl _ = False
1160 iname (UImplicit n _) = n
1161 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1163 doAdd [] _ t = t
1164 -- if all of args in ns, then add it
1165 doAdd (UImplicit n ty : cs) ns t
1166 | elem n ns
1167 = PPi (Imp [] Dynamic False) n ty (doAdd cs ns t)
1168 | otherwise = doAdd cs ns t
1170 -- bind the free names which weren't in the using block
1171 bindFree [] tm = tm
1172 bindFree (n:ns) tm
1173 | elem n (map iname uimpls) = bindFree ns tm
1174 | otherwise
1175 = PPi (Imp [] Dynamic False) n Placeholder (bindFree ns tm)
1177 getArgnames (PPi _ n c sc)
1178 = n : getArgnames sc
1179 getArgnames _ = []
1181-- Given the original type and the elaborated type, return the implicitness
1182-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1184getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1185getUnboundImplicits i t tm = getImps t (collectImps tm)
1186 where collectImps (PPi p n t sc)
1187 = (n, (p, t)) : collectImps sc
1188 collectImps _ = []
1190 getImps (Bind n (Pi t _) sc) imps
1191 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1192 where
1193 argInfo n (Imp opt _ _) t'
1194 = (True, PImp (getPriority i t') True opt n t')
1195 argInfo n (Exp opt _ _) t'
1196 = (InaccessibleArg `elem` opt,
1197 PExp (getPriority i t') opt n t')
1198 argInfo n (Constraint opt _) t'
1199 = (InaccessibleArg `elem` opt,
1200 PConstraint 10 opt n t')
1201 argInfo n (TacImp opt _ scr) t'
1202 = (InaccessibleArg `elem` opt,
1203 PTacImplicit 10 opt n scr t')
1204 getImps (Bind n (Pi t _) sc) imps = impBind n t : getImps sc imps
1205 where impBind n t = (True, PImp 1 True [] n Placeholder)
1206 getImps sc tm = []
1208-- Add implicit Pi bindings for any names in the term which appear in an
1209-- argument position.
1211-- This has become a right mess already. Better redo it some time...
1212-- TODO: This is obsoleted by the new way of elaborating types, but there's still
1213-- a couple of places which use it. Clean them up!
1214implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1215implicit info syn n ptm = implicit' info syn [] n ptm
1217implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1218implicit' info syn ignore n ptm
1219 = do i <- getIState
1220 let (tm', impdata) = implicitise syn ignore i ptm
1221 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1222-- let (tm'', spos) = findStatics i tm'
1223 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1224 addIBC (IBCImp n)
1225 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1226-- i <- get
1227-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1228 return tm'
1229 where
1230 -- Detect unknown names in default arguments and throw error if found.
1231 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1232 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1234 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1235 notFoundInDefault kns (PTacImplicit _ _ n script _)
1236 = do i <- getIState
1237 case notFound kns (namesIn [] i script) of
1238 Nothing -> return (n:kns)
1239 Just name -> throwError (NoSuchVariable name)
1240 notFoundInDefault kns p = return ((pname p):kns)
1242 notFound :: [Name] -> [Name] -> Maybe Name
1243 notFound kns [] = Nothing
1244 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1245 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1247implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1248implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1249 let (declimps, ns') = execState (imps True [] tm) ([], [])
1250 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1251 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1252 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1253 if null ns
1254 then (tm, reverse declimps)
1255 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1256 where
1257 uvars = map ipair (filter uimplicit (using syn))
1258 pvars = syn_params syn
1260 inUsing n = n `elem` map fst uvars
1262 ipair (UImplicit x y) = (x, y)
1263 uimplicit (UImplicit _ _) = True
1264 uimplicit _ = False
1266 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1267 | otherwise = x : dropAll xs ys
1268 dropAll [] ys = []
1270 -- Find names in argument position in a type, suitable for implicit
1271 -- binding
1272 -- Not the function position, but do everything else...
1273 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1274 implNamesIn uv t = namesIn uv ist t
1276 imps top env (PApp _ f as)
1277 = do (decls, ns) <- get
1278 let isn = concatMap (namesIn uvars ist) (map getTm as)
1279 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1280 imps top env (PPi (Imp l _ _) n ty sc)
1281 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1282 (decls , ns) <- get
1283 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1284 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1285 imps True (n:env) sc
1286 imps top env (PPi (Exp l _ _) n ty sc)
1287 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1288 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1289 _ -> [])
1290 (decls, ns) <- get -- ignore decls in HO types
1291 put (PExp (getPriority ist ty) l n Placeholder : decls,
1292 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1293 imps True (n:env) sc
1294 imps top env (PPi (Constraint l _) n ty sc)
1295 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1296 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1297 _ -> [])
1298 (decls, ns) <- get -- ignore decls in HO types
1299 put (PConstraint 10 l n Placeholder : decls,
1300 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1301 imps True (n:env) sc
1302 imps top env (PPi (TacImp l _ scr) n ty sc)
1303 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1304 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1305 _ -> [])
1306 (decls, ns) <- get -- ignore decls in HO types
1307 put (PTacImplicit 10 l n scr Placeholder : decls,
1308 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1309 imps True (n:env) sc
1310 imps top env (PEq _ _ _ l r)
1311 = do (decls, ns) <- get
1312 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1313 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1314 imps top env (PRewrite _ l r _)
1315 = do (decls, ns) <- get
1316 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1317 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1318 imps top env (PTyped l r)
1319 = imps top env l
1320 imps top env (PPair _ _ l r)
1321 = do (decls, ns) <- get
1322 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1323 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1324 imps top env (PDPair _ _ (PRef _ n) t r)
1325 = do (decls, ns) <- get
1326 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1327 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1328 imps top env (PDPair _ _ l t r)
1329 = do (decls, ns) <- get
1330 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1331 namesIn uvars ist r
1332 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1333 imps top env (PAlternative a as)
1334 = do (decls, ns) <- get
1335 let isn = concatMap (namesIn uvars ist) as
1336 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1337 imps top env (PLam n ty sc)
1338 = do imps False env ty
1339 imps False (n:env) sc
1340 imps top env (PHidden tm) = imps False env tm
1341 imps top env (PUnifyLog tm) = imps False env tm
1342 imps top env (PNoImplicits tm) = imps False env tm
1343 imps top env _ = return ()
1345 pibind using [] sc = sc
1346 pibind using (n:ns) sc
1347 = case lookup n using of
1348 Just ty -> PPi (Imp [] Dynamic False) n ty (pibind using ns sc)
1349 Nothing -> PPi (Imp [] Dynamic False) n Placeholder
1350 (pibind using ns sc)
1352-- Add implicit arguments in function calls
1353addImplPat :: IState -> PTerm -> PTerm
1354addImplPat = addImpl' True [] []
1356addImplBound :: IState -> [Name] -> PTerm -> PTerm
1357addImplBound ist ns = addImpl' False ns [] ist
1359addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1360addImplBoundInf ist ns inf = addImpl' False ns inf ist
1362-- | Add the implicit arguments to applications in the term
1363addImpl :: IState -> PTerm -> PTerm
1364addImpl = addImpl' False [] []
1366-- TODO: in patterns, don't add implicits to function names guarded by constructors
1367-- and *not* inside a PHidden
1369addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1370addImpl' inpat env infns ist ptm
1371 = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)
1372 where
1373 ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1374 ai qq env ds (PRef fc f)
1375 | f `elem` infns = PInferRef fc f
1376 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []
1377 ai qq env ds (PHidden (PRef fc f))
1378 | not (f `elem` map fst env) = handleErr $ aiFn inpat False qq ist fc f ds []
1379 ai qq env ds (PEq fc lt rt l r)
1380 = let lt' = ai qq env ds lt
1381 rt' = ai qq env ds rt
1382 l' = ai qq env ds l
1383 r' = ai qq env ds r in
1384 PEq fc lt' rt' l' r'
1385 ai qq env ds (PRewrite fc l r g)
1386 = let l' = ai qq env ds l
1387 r' = ai qq env ds r
1388 g' = fmap (ai qq env ds) g in
1389 PRewrite fc l' r' g'
1390 ai qq env ds (PTyped l r)
1391 = let l' = ai qq env ds l
1392 r' = ai qq env ds r in
1393 PTyped l' r'
1394 ai qq env ds (PPair fc p l r)
1395 = let l' = ai qq env ds l
1396 r' = ai qq env ds r in
1397 PPair fc p l' r'
1398 ai qq env ds (PDPair fc p l t r)
1399 = let l' = ai qq env ds l
1400 t' = ai qq env ds t
1401 r' = ai qq env ds r in
1402 PDPair fc p l' t' r'
1403 ai qq env ds (PAlternative a as)
1404 = let as' = map (ai qq env ds) as in
1405 PAlternative a as'
1406 ai qq env _ (PDisamb ds' as) = ai qq env ds' as
1407 ai qq env ds (PApp fc (PInferRef _ f) as)
1408 = let as' = map (fmap (ai qq env ds)) as in
1409 PApp fc (PInferRef fc f) as'
1410 ai qq env ds (PApp fc ftm@(PRef _ f) as)
1411 | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)
1412 | not (f `elem` map fst env)
1413 = let as' = map (fmap (ai qq env ds)) as in
1414 handleErr $ aiFn inpat False qq ist fc f ds as'
1415 | Just (Just ty) <- lookup f env =
1416 let as' = map (fmap (ai qq env ds)) as
1417 arity = getPArity ty in
1418 mkPApp fc arity ftm as'
1419 ai qq env ds (PApp fc f as)
1420 = let f' = ai qq env ds f
1421 as' = map (fmap (ai qq env ds)) as in
1422 mkPApp fc 1 f' as'
1423 ai qq env ds (PCase fc c os)
1424 = let c' = ai qq env ds c in
1425 -- leave os alone, because they get lifted into a new pattern match
1426 -- definition which is passed through addImpl again with more scope
1427 -- information
1428 PCase fc c' os
1429 ai qq env ds (PLam n ty sc)
1430 = let ty' = ai qq env ds ty
1431 sc' = ai qq ((n, Just ty):env) ds sc in
1432 PLam n ty' sc'
1433 ai qq env ds (PLet n ty val sc)
1434 = let ty' = ai qq env ds ty
1435 val' = ai qq env ds val
1436 sc' = ai qq ((n, Just ty):env) ds sc in
1437 PLet n ty' val' sc'
1438 ai qq env ds (PPi p n ty sc)
1439 = let ty' = ai qq env ds ty
1440 sc' = ai qq ((n, Just ty):env) ds sc in
1441 PPi p n ty' sc'
1442 ai qq env ds (PGoal fc r n sc)
1443 = let r' = ai qq env ds r
1444 sc' = ai qq ((n, Nothing):env) ds sc in
1445 PGoal fc r' n sc'
1446 ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)
1447 -- Don't do PProof or PTactics since implicits get added when scope is
1448 -- properly known in ElabTerm.runTac
1449 ai qq env ds (PRefl fc tm) = PRefl fc (ai qq env ds tm)
1450 ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)
1451 ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)
1452 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)
1453 (fmap (ai True env ds) g)
1454 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
1455 ai qq env ds tm = tm
1457 handleErr (Left err) = PElabError err
1458 handleErr (Right x) = x
1460-- if in a pattern, and there are no arguments, and there's no possible
1461-- names with zero explicit arguments, don't add implicits.
1463aiFn :: Bool -> Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1464aiFn inpat True qq ist fc f ds []
1465 = case lookupDef f (tt_ctxt ist) of
1466 [] -> Right $ PPatvar fc f
1467 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1468 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1469 if (not (vname f) || tcname f
1470 || any (conCaf (tt_ctxt ist)) ialts)
1471-- any constructor alts || any allImp ialts))
1472 then aiFn inpat False qq ist fc f ds [] -- use it as a constructor
1473 else Right $ PPatvar fc f
1474 where imp (PExp _ _ _ _) = False
1475 imp _ = True
1476-- allImp [] = False
1477 allImp xs = all imp xs
1478 constructor (TyDecl (DCon _ _ _) _) = True
1479 constructor _ = False
1481 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1483 vname (UN n) = True -- non qualified
1484 vname _ = False
1486aiFn inpat expat qq ist fc f ds as
1487 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1488aiFn inpat expat qq ist fc f ds as
1489 -- This is where namespaces get resolved by adding PAlternative
1490 = do let ns = lookupCtxtName f (idris_implicits ist)
1491 let nh = filter (\(n, _) -> notHidden n) ns
1492 let ns' = case trimAlts ds nh of
1493 [] -> nh
1494 x -> x
1495 case ns' of
1496 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1497 [] -> if f `elem` (map fst (idris_metavars ist))
1498 then Right $ PApp fc (PRef fc f) as
1499 else Right $ mkPApp fc (length as) (PRef fc f) as
1500 alts -> Right $
1501 PAlternative True $
1502 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1503 (insertImpl ns as)) alts
1504 where
1505 trimAlts [] alts = alts
1506 trimAlts ns alts
1507 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1509 nspace (NS _ s) = s
1510 nspace _ = []
1512 notHidden n = case getAccessibility n of
1513 Hidden -> False
1514 _ -> True
1516 getAccessibility n
1517 = case lookupDefAcc n False (tt_ctxt ist) of
1518 [(n,t)] -> t
1519 _ -> Public
1521 insertImpl :: [PArg] -> [PArg] -> [PArg]
1522 insertImpl ps as = insImpAcc M.empty ps (filter exp as) (filter (not.exp) as)
1524 exp (PExp _ _ _ _) = True
1525 exp (PConstraint _ _ _ _) = True
1526 exp _ = False
1528 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1529 -> [PArg] -- parameters
1530 -> [PArg] -- explicit arguments
1531 -> [PArg] -- implicits given
1532 -> [PArg]
1533 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
1534 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1535 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
1536 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1537 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
1538 let rtc = PResolveTC fc in
1539 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
1540 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
1541 case find n imps [] of
1542 Just (tm, imps') ->
1543 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1544 Nothing ->
1545 PImp p True l n Placeholder :
1546 insImpAcc (M.insert n Placeholder pnas) ps given imps
1547 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1548 let sc = addImpl ist (substMatches (M.toList pnas) sc') in
1549 case find n imps [] of
1550 Just (tm, imps') ->
1551 PTacImplicit p l n sc tm :
1552 insImpAcc (M.insert n tm pnas) ps given imps'
1553 Nothing ->
1554 if inpat
1555 then PTacImplicit p l n sc Placeholder :
1556 insImpAcc (M.insert n Placeholder pnas) ps given imps
1557 else PTacImplicit p l n sc sc :
1558 insImpAcc (M.insert n sc pnas) ps given imps
1559 insImpAcc _ expected [] imps = imps -- so that unused implicits give error
1560 -- TODO: report here, and prune alternatives
1561 insImpAcc _ _ given imps = given ++ imps
1563 find n [] acc = Nothing
1564 find n (PImp _ _ _ n' t : gs) acc
1565 | n == n' = Just (t, reverse acc ++ gs)
1566 find n (PTacImplicit _ _ n' _ t : gs) acc
1567 | n == n' = Just (t, reverse acc ++ gs)
1568 find n (g : gs) acc = find n gs (g : acc)
1570-- replace non-linear occurrences with _
1571-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1572-- it is hard to get right!
1574stripLinear :: IState -> PTerm -> PTerm
1575stripLinear i tm = evalState (sl tm) [] where
1576 sl :: PTerm -> State [Name] PTerm
1577 sl (PRef fc f)
1578 | (_:_) <- lookupTy f (tt_ctxt i)
1579 = return $ PRef fc f
1580 | otherwise = do ns <- get
1581 if (f `elem` ns)
1582 then return Placeholder
1583 else do put (f : ns)
1584 return (PRef fc f)
1585 sl (PPatvar fc f)
1586 = do ns <- get
1587 if (f `elem` ns)
1588 then return Placeholder
1589 else do put (f : ns)
1590 return (PPatvar fc f)
1591 sl t@(PAlternative _ (a : as)) = do sl a
1592 return t
1593 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1594 args' <- mapM slA args
1595 return $ PApp fc fn args'
1596 where slA (PImp p m l n t) = do t' <- sl t
1597 return $ PImp p m l n t'
1598 slA (PExp p l n t) = do t' <- sl t
1599 return $ PExp p l n t'
1600 slA (PConstraint p l n t)
1601 = do t' <- sl t
1602 return $ PConstraint p l n t'
1603 slA (PTacImplicit p l n sc t)
1604 = do t' <- sl t
1605 return $ PTacImplicit p l n sc t'
1606 sl x = return x
1608-- Remove functions which aren't applied to anything, which must then
1609-- be resolved by unification. Assume names resolved and alternatives
1610-- filled in (so no ambiguity).
1612stripUnmatchable :: IState -> PTerm -> PTerm
1613stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1614 su :: PTerm -> PTerm
1615 su (PRef fc f)
1616 | (Bind n (Pi t _) sc :_) <- lookupTy f (tt_ctxt i)
1617 = Placeholder
1618 su (PApp fc fn args)
1619 = PApp fc fn (fmap (fmap su) args)
1620 su (PAlternative b alts)
1621 = let alts' = filter (/= Placeholder) (map su alts) in
1622 if null alts' then Placeholder
1623 else PAlternative b alts'
1624 su (PPair fc p l r) = PPair fc p (su l) (su r)
1625 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1626 su t = t
1627stripUnmatchable i tm = tm
1629mkPApp fc a f [] = f
1630mkPApp fc a f as = let rest = drop a as in
1631 appRest fc (PApp fc f (take a as)) rest
1632 where
1633 appRest fc f [] = f
1634 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1636-- Find 'static' argument positions
1637-- (the declared ones, plus any names in argument position in the declared
1638-- statics)
1639-- FIXME: It's possible that this really has to happen after elaboration
1641findStatics :: IState -> PTerm -> (PTerm, [Bool])
1642findStatics ist tm = trace (show tm) $
1643 let (ns, ss) = fs tm in
1644 runState (pos ns ss tm) []
1645 where fs (PPi p n t sc)
1646 | Static <- pstatic p
1647 = let (ns, ss) = fs sc in
1648 (namesIn [] ist t : ns, n : ss)
1649 | otherwise = let (ns, ss) = fs sc in
1650 (ns, ss)
1651 fs _ = ([], [])
1653 inOne n ns = length (filter id (map (elem n) ns)) == 1
1655 pos ns ss (PPi p n t sc)
1656 | elem n ss = do sc' <- pos ns ss sc
1657 spos <- get
1658 put (True : spos)
1659 return (PPi (p { pstatic = Static }) n t sc')
1660 | otherwise = do sc' <- pos ns ss sc
1661 spos <- get
1662 put (False : spos)
1663 return (PPi p n t sc')
1664 pos ns ss t = return t
1666-- for 6.12/7 compatibility
1667data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
1669instance Applicative (EitherErr a) where
1670 pure = return
1671 (<*>) = ap
1673instance Monad (EitherErr a) where
1674 return = RightOK
1676 (LeftErr e) >>= k = LeftErr e
1677 RightOK v >>= k = k v
1679toEither (LeftErr e) = Left e
1680toEither (RightOK ho) = Right ho
1682-- syntactic match of a against b, returning pair of variables in a
1683-- and what they match. Returns the pair that failed if not a match.
1685matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1686matchClause = matchClause' False
1688matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1689matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1690 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1692 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1693 fullApp x = x
1695 match' x y = match (fullApp x) (fullApp y)
1696 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1697 | fi == txt "fromInteger" && b == txt "builtins",
1698 PConstant (I _) <- getTm x = match (getTm x) x'
1699 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1700 | fi == txt "fromInteger" && b == txt "builtins",
1701 PConstant (I _) <- getTm x = match (getTm x) x'
1702 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1703 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1704 match (PApp _ f args) (PApp _ f' args')
1705 | length args == length args'
1706 = do mf <- match' f f'
1707 ms <- zipWithM matchArg args args'
1708 return (mf ++ concat ms)
1709 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1710 match (PPatvar f n) xr = match (PRef f n) xr
1711 match xr (PPatvar f n) = match xr (PRef f n)
1712 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1713 match (PRef _ n) tm@(PRef _ n')
1714 | n == n' && not names &&
1715 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1716 || tm == Placeholder)
1717 = return [(n, tm)]
1718 -- if one namespace is missing, drop the other
1719 | n == n' || n == dropNS n' || dropNS n == n' = return []
1720 where dropNS (NS n _) = n
1721 dropNS n = n
1722 match (PRef _ n) tm
1723 | not names && (not (isConName n (tt_ctxt i) ||
1724 isFnName n (tt_ctxt i)) || tm == Placeholder)
1725 = return [(n, tm)]
1726 match (PEq _ _ _ l r) (PEq _ _ _ l' r')
1727 = do ml <- match' l l'
1728 mr <- match' r r'
1729 return (ml ++ mr)
1730 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1731 = do ml <- match' l l'
1732 mr <- match' r r'
1733 return (ml ++ mr)
1734 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1735 mr <- match r r'
1736 return (ml ++ mr)
1737 match (PTyped l r) x = match l x
1738 match x (PTyped l r) = match x l
1739 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1740 mr <- match' r r'
1741 return (ml ++ mr)
1742 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1743 mt <- match' t t'
1744 mr <- match' r r'
1745 return (ml ++ mt ++ mr)
1746 match (PAlternative a as) (PAlternative a' as')
1747 = do ms <- zipWithM match' as as'
1748 return (concat ms)
1749 match a@(PAlternative _ as) b
1750 = do let ms = zipWith match' as (repeat b)
1751 case (rights (map toEither ms)) of
1752 (x: _) -> return x
1753 _ -> LeftErr (a, b)
1754 match (PCase _ _ _) _ = return [] -- lifted out
1755 match (PMetavar _) _ = return [] -- modified
1756 match (PInferRef _ _) _ = return [] -- modified
1757 match (PQuote _) _ = return []
1758 match (PProof _) _ = return []
1759 match (PTactics _) _ = return []
1760 match (PRefl _ _) (PRefl _ _) = return []
1761 match (PResolveTC _) (PResolveTC _) = return []
1762 match (PTrue _ _) (PTrue _ _) = return []
1763 match (PFalse _) (PFalse _) = return []
1764 match (PReturn _) (PReturn _) = return []
1765 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1766 ms <- match' s s'
1767 return (mt ++ ms)
1768 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1769 ms <- match' s s'
1770 return (mt ++ ms)
1771 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1772 mty <- match' ty ty'
1773 ms <- match' s s'
1774 return (mt ++ mty ++ ms)
1775 match (PHidden x) (PHidden y) = match' x y
1776 match (PUnifyLog x) y = match' x y
1777 match x (PUnifyLog y) = match' x y
1778 match (PNoImplicits x) y = match' x y
1779 match x (PNoImplicits y) = match' x y
1780 match Placeholder _ = return []
1781 match _ Placeholder = return []
1782 match (PResolveTC _) _ = return []
1783 match a b | a == b = return []
1784 | otherwise = LeftErr (a, b)
1786 checkRpts (RightOK ms) = check ms where
1787 check ((n,t):xs)
1788 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1789 then Left (t, t')
1790 else check xs
1791 check (_:xs) = check xs
1792 check [] = Right ms
1793 checkRpts (LeftErr x) = Left x
1795substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1796substMatches ms = substMatchesShadow ms []
1798substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1799substMatchesShadow [] shs t = t
1800substMatchesShadow ((n,tm):ns) shs t
1801 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1803substMatch :: Name -> PTerm -> PTerm -> PTerm
1804substMatch n = substMatchShadow n []
1806substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1807substMatchShadow n shs tm t = sm shs t where
1808 sm xs (PRef _ n') | n == n' = tm
1809 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1810 sm xs (PPi p x t sc)
1811 | x `elem` xs
1812 = let x' = nextName x in
1813 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1814 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1815 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1816 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1817 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1818 sm xs (PEq f xt yt x y) = PEq f (sm xs xt) (sm xs yt) (sm xs x) (sm xs y)
1819 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1820 (fmap (sm xs) tm)
1821 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1822 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
1823 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
1824 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1825 sm xs (PHidden x) = PHidden (sm xs x)
1826 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1827 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1828 sm xs x = x
1830 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1831 fullApp x = x
1833shadow :: Name -> Name -> PTerm -> PTerm
1834shadow n n' t = sm t where
1835 sm (PRef fc x) | n == x = PRef fc n'
1836 sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)
1837 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1838 sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)
1839 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1840 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1841 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1842 sm (PEq f xt yt x y) = PEq f (sm xt) (sm yt) (sm x) (sm y)
1843 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1844 sm (PTyped x y) = PTyped (sm x) (sm y)
1845 sm (PPair f p x y) = PPair f p (sm x) (sm y)
1846 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
1847 sm (PAlternative a as) = PAlternative a (map sm as)
1848 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1849 sm (PProof ts) = PProof (map (fmap sm) ts)
1850 sm (PHidden x) = PHidden (sm x)
1851 sm (PUnifyLog x) = PUnifyLog (sm x)
1852 sm (PNoImplicits x) = PNoImplicits (sm x)
1853 sm x = x
1855-- Rename any binders which are repeated (so that we don't have to mess
1856-- about with shadowing anywhere else).
1858mkUniqueNames :: [Name] -> PTerm -> PTerm
1859mkUniqueNames env tm = evalState (mkUniq tm) env where
1860 inScope = boundNamesIn tm
1862 mkUniqA arg = do t' <- mkUniq (getTm arg)
1863 return (arg { getTm = t' })
1865 -- Initialise the unique name with the environment length (so we're not
1866 -- looking for too long...)
1867 initN (UN n) l = UN $ txt (str n ++ show l)
1868 initN (MN i s) l = MN (i+l) s
1869 initN n l = n
1871 -- FIXME: Probably ought to do this for completeness! It's fine as
1872 -- long as there are no bindings inside tactics though.
1873 mkUniqT tac = return tac
1875 mkUniq :: PTerm -> State [Name] PTerm
1876 mkUniq (PLam n ty sc)
1877 = do env <- get
1878 (n', sc') <-
1879 if n `elem` env
1880 then do let n' = uniqueName (initN n (length env))
1881 (env ++ inScope)
1882 return (n', shadow n n' sc)
1883 else return (n, sc)
1884 put (n' : env)
1885 ty' <- mkUniq ty
1886 sc'' <- mkUniq sc'
1887 return $! PLam n' ty' sc''
1888 mkUniq (PPi p n ty sc)
1889 = do env <- get
1890 (n', sc') <-
1891 if n `elem` env
1892 then do let n' = uniqueName (initN n (length env))
1893 (env ++ inScope)
1894 return (n', shadow n n' sc)
1895 else return (n, sc)
1896 put (n' : env)
1897 ty' <- mkUniq ty
1898 sc'' <- mkUniq sc'
1899 return $! PPi p n' ty' sc''
1900 mkUniq (PLet n ty val sc)
1901 = do env <- get
1902 (n', sc') <-
1903 if n `elem` env
1904 then do let n' = uniqueName (initN n (length env))
1905 (env ++ inScope)
1906 return (n', shadow n n' sc)
1907 else return (n, sc)
1908 put (n' : env)
1909 ty' <- mkUniq ty; val' <- mkUniq val
1910 sc'' <- mkUniq sc'
1911 return $! PLet n' ty' val' sc''
1912 mkUniq (PApp fc t args)
1913 = do t' <- mkUniq t
1914 args' <- mapM mkUniqA args
1915 return $! PApp fc t' args'
1916 mkUniq (PAppBind fc t args)
1917 = do t' <- mkUniq t
1918 args' <- mapM mkUniqA args
1919 return $! PAppBind fc t' args'
1920 mkUniq (PCase fc t alts)
1921 = do t' <- mkUniq t
1922 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
1923 return (x', y')) alts
1924 return $! PCase fc t' alts'
1925 mkUniq (PPair fc p l r)
1926 = do l' <- mkUniq l; r' <- mkUniq r
1927 return $! PPair fc p l' r'
1928 mkUniq (PDPair fc p (PRef fc' n) t sc)
1929 | t /= Placeholder
1930 = do env <- get
1931 (n', sc') <- if n `elem` env
1932 then do let n' = uniqueName n (env ++ inScope)
1933 return (n', shadow n n' sc)
1934 else return (n, sc)
1935 put (n' : env)
1936 t' <- mkUniq t
1937 sc'' <- mkUniq sc'
1938 return $! PDPair fc p (PRef fc' n') t' sc''
1939 mkUniq (PDPair fc p l t r)
1940 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
1941 return $! PDPair fc p l' t' r'
1942 mkUniq (PAlternative b as)
1943 = liftM (PAlternative b) (mapM mkUniq as)
1944 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
1945 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
1946 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
1947 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
1948 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
1949 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
1950 mkUniq t = return t