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