git.iko.soy/Idris-dev
on d25bf25 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1963 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 (PFalse _) = 0
1044 pri (PRefl _ _) = 1
1045 pri (PEq _ _ _ l r) = max 1 (max (pri l) (pri r))
1046 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
1047 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1048 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1049 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1050 pri (PTyped l r) = pri l
1051 pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))
1052 pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1053 pri (PAlternative a as) = maximum (map pri as)
1054 pri (PConstant _) = 0
1055 pri Placeholder = 1
1056 pri _ = 3
1059addStatics :: Name -> Term -> PTerm -> Idris ()
1060addStatics n tm ptm =
1061 do let (statics, dynamics) = initStatics tm ptm
1062 let stnames = nub $ concatMap freeArgNames (map snd statics)
1063 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
1064 -- also get the arguments which are 'uniquely inferrable' from
1065 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1066 let statics' = nub $ map fst statics ++
1067 filter (\x -> not (elem x dnames)) stnames
1068 let stpos = staticList statics' tm
1069 i <- getIState
1070 when (not (null statics)) $
1071 logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ " "
1072 ++ show statics' ++ "\n" ++ show dynamics
1073 ++ "\n" ++ show stpos
1074 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1075 addIBC (IBCStatic n)
1076 where
1077 initStatics (Bind n (Pi ty _) sc) (PPi p n' t s)
1078 | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' t s) in
1079 (static, (n, ty) : dynamic)
1080 initStatics (Bind n (Pi ty _) sc) (PPi p n' _ s)
1081 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1082 if pstatic p == Static then ((n, ty) : static, dynamic)
1083 else if (not (searchArg p))
1084 then (static, (n, ty) : dynamic)
1085 else (static, dynamic)
1086 initStatics t pt = ([], [])
1088 freeArgNames (Bind n (Pi ty _) sc)
1089 = nub $ freeArgNames ty
1090 freeArgNames tm = let (_, args) = unApply tm in
1091 concatMap freeNames args
1093 -- if a name appears in a type class or tactic implicit index, it doesn't
1094 -- affect its 'uniquely inferrable' from a static status since these are
1095 -- resolved by searching.
1096 searchArg (Constraint _ _) = True
1097 searchArg (TacImp _ _ _) = True
1098 searchArg _ = False
1100 staticList sts (Bind n (Pi _ _) sc) = (n `elem` sts) : staticList sts sc
1101 staticList _ _ = []
1103-- Dealing with implicit arguments
1105-- Add some bound implicits to the using block if they aren't there already
1107addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
1108addToUsing us [] = us
1109addToUsing us ((n, t) : ns)
1110 | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
1111 | otherwise = addToUsing us ns
1112 where impName (UImplicit n _) = Just n
1113 impName _ = Nothing
1115-- Add constraint bindings from using block
1117addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1118addUsingConstraints syn fc t
1119 = do ist <- get
1120 let ns = namesIn [] ist t
1121 let cs = getConstraints t -- check declared constraints
1122 let addconsts = uconsts \\ cs
1123 return (doAdd addconsts ns t)
1124 where uconsts = filter uconst (using syn)
1125 uconst (UConstraint _ _) = True
1126 uconst _ = False
1128 doAdd [] _ t = t
1129 -- if all of args in ns, then add it
1130 doAdd (UConstraint c args : cs) ns t
1131 | all (\n -> elem n ns) args
1132 = PPi (Constraint [] Dynamic) (sMN 0 "cu")
1133 (mkConst c args) (doAdd cs ns t)
1134 | otherwise = doAdd cs ns t
1136 mkConst c args = PApp fc (PRef fc c)
1137 (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc n)) args)
1139 getConstraints (PPi (Constraint _ _) _ c sc)
1140 = getcapp c ++ getConstraints sc
1141 getConstraints (PPi _ _ c sc) = getConstraints sc
1142 getConstraints _ = []
1144 getcapp (PApp _ (PRef _ c) args)
1145 = do ns <- mapM getName args
1146 return (UConstraint c ns)
1147 getcapp _ = []
1149 getName (PExp _ _ _ (PRef _ n)) = return n
1150 getName _ = []
1152-- Add implicit bindings from using block, and bind any missing names
1153addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
1154addUsingImpls syn n fc t
1155 = do ist <- getIState
1156 let ns = implicitNamesIn (map iname uimpls) ist t
1157 let badnames = filter (\n -> not (implicitable n) &&
1158 n `notElem` (map iname uimpls)) ns
1159 when (not (null badnames)) $
1160 throwError (At fc (Elaborating "type of " n
1161 (NoSuchVariable (head badnames))))
1162 let cs = getArgnames t -- get already bound names
1163 let addimpls = filter (\n -> iname n `notElem` cs) uimpls
1164 -- if all names in the arguments of addconsts appear in ns,
1165 -- add the constraint implicitly
1166 return (bindFree ns (doAdd addimpls ns t))
1167 where uimpls = filter uimpl (using syn)
1168 uimpl (UImplicit _ _) = True
1169 uimpl _ = False
1171 iname (UImplicit n _) = n
1172 iname (UConstraint _ _) = error "Can't happen addUsingImpls"
1174 doAdd [] _ t = t
1175 -- if all of args in ns, then add it
1176 doAdd (UImplicit n ty : cs) ns t
1177 | elem n ns
1178 = PPi (Imp [] Dynamic False) n ty (doAdd cs ns t)
1179 | otherwise = doAdd cs ns t
1181 -- bind the free names which weren't in the using block
1182 bindFree [] tm = tm
1183 bindFree (n:ns) tm
1184 | elem n (map iname uimpls) = bindFree ns tm
1185 | otherwise
1186 = PPi (Imp [] Dynamic False) n Placeholder (bindFree ns tm)
1188 getArgnames (PPi _ n c sc)
1189 = n : getArgnames sc
1190 getArgnames _ = []
1192-- Given the original type and the elaborated type, return the implicitness
1193-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
1195getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1196getUnboundImplicits i t tm = getImps t (collectImps tm)
1197 where collectImps (PPi p n t sc)
1198 = (n, (p, t)) : collectImps sc
1199 collectImps _ = []
1201 getImps (Bind n (Pi t _) sc) imps
1202 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1203 where
1204 argInfo n (Imp opt _ _) t'
1205 = (True, PImp (getPriority i t') True opt n t')
1206 argInfo n (Exp opt _ _) t'
1207 = (InaccessibleArg `elem` opt,
1208 PExp (getPriority i t') opt n t')
1209 argInfo n (Constraint opt _) t'
1210 = (InaccessibleArg `elem` opt,
1211 PConstraint 10 opt n t')
1212 argInfo n (TacImp opt _ scr) t'
1213 = (InaccessibleArg `elem` opt,
1214 PTacImplicit 10 opt n scr t')
1215 getImps (Bind n (Pi t _) sc) imps = impBind n t : getImps sc imps
1216 where impBind n t = (True, PImp 1 True [] n Placeholder)
1217 getImps sc tm = []
1219-- Add implicit Pi bindings for any names in the term which appear in an
1220-- argument position.
1222-- This has become a right mess already. Better redo it some time...
1223-- TODO: This is obsoleted by the new way of elaborating types, but there's still
1224-- a couple of places which use it. Clean them up!
1225implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1226implicit info syn n ptm = implicit' info syn [] n ptm
1228implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1229implicit' info syn ignore n ptm
1230 = do i <- getIState
1231 let (tm', impdata) = implicitise syn ignore i ptm
1232 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1233-- let (tm'', spos) = findStatics i tm'
1234 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1235 addIBC (IBCImp n)
1236 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1237-- i <- get
1238-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1239 return tm'
1240 where
1241 -- Detect unknown names in default arguments and throw error if found.
1242 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1243 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1245 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1246 notFoundInDefault kns (PTacImplicit _ _ n script _)
1247 = do i <- getIState
1248 case notFound kns (namesIn [] i script) of
1249 Nothing -> return (n:kns)
1250 Just name -> throwError (NoSuchVariable name)
1251 notFoundInDefault kns p = return ((pname p):kns)
1253 notFound :: [Name] -> [Name] -> Maybe Name
1254 notFound kns [] = Nothing
1255 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1256 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1258implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1259implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1260 let (declimps, ns') = execState (imps True [] tm) ([], [])
1261 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1262 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1263 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1264 if null ns
1265 then (tm, reverse declimps)
1266 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1267 where
1268 uvars = map ipair (filter uimplicit (using syn))
1269 pvars = syn_params syn
1271 inUsing n = n `elem` map fst uvars
1273 ipair (UImplicit x y) = (x, y)
1274 uimplicit (UImplicit _ _) = True
1275 uimplicit _ = False
1277 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1278 | otherwise = x : dropAll xs ys
1279 dropAll [] ys = []
1281 -- Find names in argument position in a type, suitable for implicit
1282 -- binding
1283 -- Not the function position, but do everything else...
1284 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1285 implNamesIn uv t = namesIn uv ist t
1287 imps top env (PApp _ f as)
1288 = do (decls, ns) <- get
1289 let isn = concatMap (namesIn uvars ist) (map getTm as)
1290 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1291 imps top env (PPi (Imp l _ _) n ty sc)
1292 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1293 (decls , ns) <- get
1294 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1295 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1296 imps True (n:env) sc
1297 imps top env (PPi (Exp l _ _) n ty sc)
1298 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1299 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1300 _ -> [])
1301 (decls, ns) <- get -- ignore decls in HO types
1302 put (PExp (getPriority ist ty) l n Placeholder : decls,
1303 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1304 imps True (n:env) sc
1305 imps top env (PPi (Constraint l _) n ty sc)
1306 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1307 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1308 _ -> [])
1309 (decls, ns) <- get -- ignore decls in HO types
1310 put (PConstraint 10 l n Placeholder : decls,
1311 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1312 imps True (n:env) sc
1313 imps top env (PPi (TacImp l _ scr) n ty sc)
1314 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1315 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1316 _ -> [])
1317 (decls, ns) <- get -- ignore decls in HO types
1318 put (PTacImplicit 10 l n scr Placeholder : decls,
1319 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1320 imps True (n:env) sc
1321 imps top env (PEq _ _ _ l r)
1322 = do (decls, ns) <- get
1323 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1324 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1325 imps top env (PRewrite _ l r _)
1326 = do (decls, ns) <- get
1327 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1328 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1329 imps top env (PTyped l r)
1330 = imps top env l
1331 imps top env (PPair _ _ l r)
1332 = do (decls, ns) <- get
1333 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1334 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1335 imps top env (PDPair _ _ (PRef _ n) t r)
1336 = do (decls, ns) <- get
1337 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1338 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1339 imps top env (PDPair _ _ l t r)
1340 = do (decls, ns) <- get
1341 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1342 namesIn uvars ist r
1343 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1344 imps top env (PAlternative a as)
1345 = do (decls, ns) <- get
1346 let isn = concatMap (namesIn uvars ist) as
1347 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1348 imps top env (PLam n ty sc)
1349 = do imps False env ty
1350 imps False (n:env) sc
1351 imps top env (PHidden tm) = imps False env tm
1352 imps top env (PUnifyLog tm) = imps False env tm
1353 imps top env (PNoImplicits tm) = imps False env tm
1354 imps top env _ = return ()
1356 pibind using [] sc = sc
1357 pibind using (n:ns) sc
1358 = case lookup n using of
1359 Just ty -> PPi (Imp [] Dynamic False) n ty (pibind using ns sc)
1360 Nothing -> PPi (Imp [] Dynamic False) n Placeholder
1361 (pibind using ns sc)
1363-- Add implicit arguments in function calls
1364addImplPat :: IState -> PTerm -> PTerm
1365addImplPat = addImpl' True [] []
1367addImplBound :: IState -> [Name] -> PTerm -> PTerm
1368addImplBound ist ns = addImpl' False ns [] ist
1370addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1371addImplBoundInf ist ns inf = addImpl' False ns inf ist
1373-- | Add the implicit arguments to applications in the term
1374addImpl :: IState -> PTerm -> PTerm
1375addImpl = addImpl' False [] []
1377-- TODO: in patterns, don't add implicits to function names guarded by constructors
1378-- and *not* inside a PHidden
1380addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1381addImpl' inpat env infns ist ptm
1382 = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)
1383 where
1384 ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
1385 ai qq env ds (PRef fc f)
1386 | f `elem` infns = PInferRef fc f
1387 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []
1388 ai qq env ds (PHidden (PRef fc f))
1389 | not (f `elem` map fst env) = handleErr $ aiFn inpat False qq ist fc f ds []
1390 ai qq env ds (PEq fc lt rt l r)
1391 = let lt' = ai qq env ds lt
1392 rt' = ai qq env ds rt
1393 l' = ai qq env ds l
1394 r' = ai qq env ds r in
1395 PEq fc lt' rt' l' r'
1396 ai qq env ds (PRewrite fc l r g)
1397 = let l' = ai qq env ds l
1398 r' = ai qq env ds r
1399 g' = fmap (ai qq env ds) g in
1400 PRewrite fc l' r' g'
1401 ai qq env ds (PTyped l r)
1402 = let l' = ai qq env ds l
1403 r' = ai qq env ds r in
1404 PTyped l' r'
1405 ai qq env ds (PPair fc p l r)
1406 = let l' = ai qq env ds l
1407 r' = ai qq env ds r in
1408 PPair fc p l' r'
1409 ai qq env ds (PDPair fc p l t r)
1410 = let l' = ai qq env ds l
1411 t' = ai qq env ds t
1412 r' = ai qq env ds r in
1413 PDPair fc p l' t' r'
1414 ai qq env ds (PAlternative a as)
1415 = let as' = map (ai qq env ds) as in
1416 PAlternative a as'
1417 ai qq env _ (PDisamb ds' as) = ai qq env ds' as
1418 ai qq env ds (PApp fc (PInferRef _ f) as)
1419 = let as' = map (fmap (ai qq env ds)) as in
1420 PApp fc (PInferRef fc f) as'
1421 ai qq env ds (PApp fc ftm@(PRef _ f) as)
1422 | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)
1423 | not (f `elem` map fst env)
1424 = let as' = map (fmap (ai qq env ds)) as in
1425 handleErr $ aiFn inpat False qq ist fc f ds as'
1426 | Just (Just ty) <- lookup f env =
1427 let as' = map (fmap (ai qq env ds)) as
1428 arity = getPArity ty in
1429 mkPApp fc arity ftm as'
1430 ai qq env ds (PApp fc f as)
1431 = let f' = ai qq env ds f
1432 as' = map (fmap (ai qq env ds)) as in
1433 mkPApp fc 1 f' as'
1434 ai qq env ds (PCase fc c os)
1435 = let c' = ai qq env ds c in
1436 -- leave os alone, because they get lifted into a new pattern match
1437 -- definition which is passed through addImpl again with more scope
1438 -- information
1439 PCase fc c' os
1440 ai qq env ds (PLam n ty sc)
1441 = let ty' = ai qq env ds ty
1442 sc' = ai qq ((n, Just ty):env) ds sc in
1443 PLam n ty' sc'
1444 ai qq env ds (PLet n ty val sc)
1445 = let ty' = ai qq env ds ty
1446 val' = ai qq env ds val
1447 sc' = ai qq ((n, Just ty):env) ds sc in
1448 PLet n ty' val' sc'
1449 ai qq env ds (PPi p n ty sc)
1450 = let ty' = ai qq env ds ty
1451 sc' = ai qq ((n, Just ty):env) ds sc in
1452 PPi p n ty' sc'
1453 ai qq env ds (PGoal fc r n sc)
1454 = let r' = ai qq env ds r
1455 sc' = ai qq ((n, Nothing):env) ds sc in
1456 PGoal fc r' n sc'
1457 ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)
1458 -- Don't do PProof or PTactics since implicits get added when scope is
1459 -- properly known in ElabTerm.runTac
1460 ai qq env ds (PRefl fc tm) = PRefl fc (ai qq env ds tm)
1461 ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)
1462 ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)
1463 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)
1464 (fmap (ai True env ds) g)
1465 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
1466 ai qq env ds tm = tm
1468 handleErr (Left err) = PElabError err
1469 handleErr (Right x) = x
1471-- if in a pattern, and there are no arguments, and there's no possible
1472-- names with zero explicit arguments, don't add implicits.
1474aiFn :: Bool -> Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1475aiFn inpat True qq ist fc f ds []
1476 = case lookupDef f (tt_ctxt ist) of
1477 [] -> Right $ PPatvar fc f
1478 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1479 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1480 if (not (vname f) || tcname f
1481 || any (conCaf (tt_ctxt ist)) ialts)
1482-- any constructor alts || any allImp ialts))
1483 then aiFn inpat False qq ist fc f ds [] -- use it as a constructor
1484 else Right $ PPatvar fc f
1485 where imp (PExp _ _ _ _) = False
1486 imp _ = True
1487-- allImp [] = False
1488 allImp xs = all imp xs
1489 constructor (TyDecl (DCon _ _ _) _) = True
1490 constructor _ = False
1492 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
1494 vname (UN n) = True -- non qualified
1495 vname _ = False
1497aiFn inpat expat qq ist fc f ds as
1498 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1499aiFn inpat expat qq ist fc f ds as
1500 -- This is where namespaces get resolved by adding PAlternative
1501 = do let ns = lookupCtxtName f (idris_implicits ist)
1502 let nh = filter (\(n, _) -> notHidden n) ns
1503 let ns' = case trimAlts ds nh of
1504 [] -> nh
1505 x -> x
1506 case ns' of
1507 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1508 [] -> if f `elem` (map fst (idris_metavars ist))
1509 then Right $ PApp fc (PRef fc f) as
1510 else Right $ mkPApp fc (length as) (PRef fc f) as
1511 alts -> Right $
1512 PAlternative True $
1513 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1514 (insertImpl ns as)) alts
1515 where
1516 trimAlts [] alts = alts
1517 trimAlts ns alts
1518 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1520 nspace (NS _ s) = s
1521 nspace _ = []
1523 notHidden n = case getAccessibility n of
1524 Hidden -> False
1525 _ -> True
1527 getAccessibility n
1528 = case lookupDefAcc n False (tt_ctxt ist) of
1529 [(n,t)] -> t
1530 _ -> Public
1532 insertImpl :: [PArg] -> [PArg] -> [PArg]
1533 insertImpl ps as = insImpAcc M.empty ps (filter exp as) (filter (not.exp) as)
1535 exp (PExp _ _ _ _) = True
1536 exp (PConstraint _ _ _ _) = True
1537 exp _ = False
1539 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1540 -> [PArg] -- parameters
1541 -> [PArg] -- explicit arguments
1542 -> [PArg] -- implicits given
1543 -> [PArg]
1544 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
1545 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1546 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
1547 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
1548 insImpAcc pnas (PConstraint p l n ty : ps) given imps =
1549 let rtc = PResolveTC fc in
1550 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
1551 insImpAcc pnas (PImp p _ l n ty : ps) given imps =
1552 case find n imps [] of
1553 Just (tm, imps') ->
1554 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
1555 Nothing ->
1556 PImp p True l n Placeholder :
1557 insImpAcc (M.insert n Placeholder pnas) ps given imps
1558 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
1559 let sc = addImpl ist (substMatches (M.toList pnas) sc') in
1560 case find n imps [] of
1561 Just (tm, imps') ->
1562 PTacImplicit p l n sc tm :
1563 insImpAcc (M.insert n tm pnas) ps given imps'
1564 Nothing ->
1565 if inpat
1566 then PTacImplicit p l n sc Placeholder :
1567 insImpAcc (M.insert n Placeholder pnas) ps given imps
1568 else PTacImplicit p l n sc sc :
1569 insImpAcc (M.insert n sc pnas) ps given imps
1570 insImpAcc _ expected [] imps = imps -- so that unused implicits give error
1571 -- TODO: report here, and prune alternatives
1572 insImpAcc _ _ given imps = given ++ imps
1574 find n [] acc = Nothing
1575 find n (PImp _ _ _ n' t : gs) acc
1576 | n == n' = Just (t, reverse acc ++ gs)
1577 find n (PTacImplicit _ _ n' _ t : gs) acc
1578 | n == n' = Just (t, reverse acc ++ gs)
1579 find n (g : gs) acc = find n gs (g : acc)
1581-- replace non-linear occurrences with _
1582-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1583-- it is hard to get right!
1585stripLinear :: IState -> PTerm -> PTerm
1586stripLinear i tm = evalState (sl tm) [] where
1587 sl :: PTerm -> State [Name] PTerm
1588 sl (PRef fc f)
1589 | (_:_) <- lookupTy f (tt_ctxt i)
1590 = return $ PRef fc f
1591 | otherwise = do ns <- get
1592 if (f `elem` ns)
1593 then return Placeholder
1594 else do put (f : ns)
1595 return (PRef fc f)
1596 sl (PPatvar fc f)
1597 = do ns <- get
1598 if (f `elem` ns)
1599 then return Placeholder
1600 else do put (f : ns)
1601 return (PPatvar fc f)
1602 sl t@(PAlternative _ (a : as)) = do sl a
1603 return t
1604 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1605 args' <- mapM slA args
1606 return $ PApp fc fn args'
1607 where slA (PImp p m l n t) = do t' <- sl t
1608 return $ PImp p m l n t'
1609 slA (PExp p l n t) = do t' <- sl t
1610 return $ PExp p l n t'
1611 slA (PConstraint p l n t)
1612 = do t' <- sl t
1613 return $ PConstraint p l n t'
1614 slA (PTacImplicit p l n sc t)
1615 = do t' <- sl t
1616 return $ PTacImplicit p l n sc t'
1617 sl x = return x
1619-- Remove functions which aren't applied to anything, which must then
1620-- be resolved by unification. Assume names resolved and alternatives
1621-- filled in (so no ambiguity).
1623stripUnmatchable :: IState -> PTerm -> PTerm
1624stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1625 su :: PTerm -> PTerm
1626 su (PRef fc f)
1627 | (Bind n (Pi t _) sc :_) <- lookupTy f (tt_ctxt i)
1628 = Placeholder
1629 su (PApp fc fn args)
1630 = PApp fc fn (fmap (fmap su) args)
1631 su (PAlternative b alts)
1632 = let alts' = filter (/= Placeholder) (map su alts) in
1633 if null alts' then Placeholder
1634 else PAlternative b alts'
1635 su (PPair fc p l r) = PPair fc p (su l) (su r)
1636 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1637 su t = t
1638stripUnmatchable i tm = tm
1640mkPApp fc a f [] = f
1641mkPApp fc a f as = let rest = drop a as in
1642 appRest fc (PApp fc f (take a as)) rest
1643 where
1644 appRest fc f [] = f
1645 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1647-- Find 'static' argument positions
1648-- (the declared ones, plus any names in argument position in the declared
1649-- statics)
1650-- FIXME: It's possible that this really has to happen after elaboration
1652findStatics :: IState -> PTerm -> (PTerm, [Bool])
1653findStatics ist tm = trace (show tm) $
1654 let (ns, ss) = fs tm in
1655 runState (pos ns ss tm) []
1656 where fs (PPi p n t sc)
1657 | Static <- pstatic p
1658 = let (ns, ss) = fs sc in
1659 (namesIn [] ist t : ns, n : ss)
1660 | otherwise = let (ns, ss) = fs sc in
1661 (ns, ss)
1662 fs _ = ([], [])
1664 inOne n ns = length (filter id (map (elem n) ns)) == 1
1666 pos ns ss (PPi p n t sc)
1667 | elem n ss = do sc' <- pos ns ss sc
1668 spos <- get
1669 put (True : spos)
1670 return (PPi (p { pstatic = Static }) n t sc')
1671 | otherwise = do sc' <- pos ns ss sc
1672 spos <- get
1673 put (False : spos)
1674 return (PPi p n t sc')
1675 pos ns ss t = return t
1677-- for 6.12/7 compatibility
1678data EitherErr a b = LeftErr a | RightOK b deriving ( Functor )
1680instance Applicative (EitherErr a) where
1681 pure = return
1682 (<*>) = ap
1684instance Monad (EitherErr a) where
1685 return = RightOK
1687 (LeftErr e) >>= k = LeftErr e
1688 RightOK v >>= k = k v
1690toEither (LeftErr e) = Left e
1691toEither (RightOK ho) = Right ho
1693-- syntactic match of a against b, returning pair of variables in a
1694-- and what they match. Returns the pair that failed if not a match.
1696matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1697matchClause = matchClause' False
1699matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1700matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1701 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1703 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1704 fullApp x = x
1706 match' x y = match (fullApp x) (fullApp y)
1707 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1708 | fi == txt "fromInteger" && b == txt "builtins",
1709 PConstant (I _) <- getTm x = match (getTm x) x'
1710 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1711 | fi == txt "fromInteger" && b == txt "builtins",
1712 PConstant (I _) <- getTm x = match (getTm x) x'
1713 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1714 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1715 match (PApp _ f args) (PApp _ f' args')
1716 | length args == length args'
1717 = do mf <- match' f f'
1718 ms <- zipWithM matchArg args args'
1719 return (mf ++ concat ms)
1720 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1721 match (PPatvar f n) xr = match (PRef f n) xr
1722 match xr (PPatvar f n) = match xr (PRef f n)
1723 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1724 match (PRef _ n) tm@(PRef _ n')
1725 | n == n' && not names &&
1726 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1727 || tm == Placeholder)
1728 = return [(n, tm)]
1729 -- if one namespace is missing, drop the other
1730 | n == n' || n == dropNS n' || dropNS n == n' = return []
1731 where dropNS (NS n _) = n
1732 dropNS n = n
1733 match (PRef _ n) tm
1734 | not names && (not (isConName n (tt_ctxt i) ||
1735 isFnName n (tt_ctxt i)) || tm == Placeholder)
1736 = return [(n, tm)]
1737 match (PEq _ _ _ l r) (PEq _ _ _ l' r')
1738 = do ml <- match' l l'
1739 mr <- match' r r'
1740 return (ml ++ mr)
1741 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1742 = do ml <- match' l l'
1743 mr <- match' r r'
1744 return (ml ++ mr)
1745 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1746 mr <- match r r'
1747 return (ml ++ mr)
1748 match (PTyped l r) x = match l x
1749 match x (PTyped l r) = match x l
1750 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1751 mr <- match' r r'
1752 return (ml ++ mr)
1753 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1754 mt <- match' t t'
1755 mr <- match' r r'
1756 return (ml ++ mt ++ mr)
1757 match (PAlternative a as) (PAlternative a' as')
1758 = do ms <- zipWithM match' as as'
1759 return (concat ms)
1760 match a@(PAlternative _ as) b
1761 = do let ms = zipWith match' as (repeat b)
1762 case (rights (map toEither ms)) of
1763 (x: _) -> return x
1764 _ -> LeftErr (a, b)
1765 match (PCase _ _ _) _ = return [] -- lifted out
1766 match (PMetavar _) _ = return [] -- modified
1767 match (PInferRef _ _) _ = return [] -- modified
1768 match (PQuote _) _ = return []
1769 match (PProof _) _ = return []
1770 match (PTactics _) _ = return []
1771 match (PRefl _ _) (PRefl _ _) = return []
1772 match (PResolveTC _) (PResolveTC _) = return []
1773 match (PTrue _ _) (PTrue _ _) = return []
1774 match (PFalse _) (PFalse _) = return []
1775 match (PReturn _) (PReturn _) = return []
1776 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1777 ms <- match' s s'
1778 return (mt ++ ms)
1779 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1780 ms <- match' s s'
1781 return (mt ++ ms)
1782 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1783 mty <- match' ty ty'
1784 ms <- match' s s'
1785 return (mt ++ mty ++ ms)
1786 match (PHidden x) (PHidden y) = match' x y
1787 match (PUnifyLog x) y = match' x y
1788 match x (PUnifyLog y) = match' x y
1789 match (PNoImplicits x) y = match' x y
1790 match x (PNoImplicits y) = match' x y
1791 match Placeholder _ = return []
1792 match _ Placeholder = return []
1793 match (PResolveTC _) _ = return []
1794 match a b | a == b = return []
1795 | otherwise = LeftErr (a, b)
1797 checkRpts (RightOK ms) = check ms where
1798 check ((n,t):xs)
1799 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1800 then Left (t, t')
1801 else check xs
1802 check (_:xs) = check xs
1803 check [] = Right ms
1804 checkRpts (LeftErr x) = Left x
1806substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1807substMatches ms = substMatchesShadow ms []
1809substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1810substMatchesShadow [] shs t = t
1811substMatchesShadow ((n,tm):ns) shs t
1812 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1814substMatch :: Name -> PTerm -> PTerm -> PTerm
1815substMatch n = substMatchShadow n []
1817substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1818substMatchShadow n shs tm t = sm shs t where
1819 sm xs (PRef _ n') | n == n' = tm
1820 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1821 sm xs (PPi p x t sc)
1822 | x `elem` xs
1823 = let x' = nextName x in
1824 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1825 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1826 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1827 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1828 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1829 sm xs (PEq f xt yt x y) = PEq f (sm xs xt) (sm xs yt) (sm xs x) (sm xs y)
1830 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1831 (fmap (sm xs) tm)
1832 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1833 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
1834 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
1835 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1836 sm xs (PHidden x) = PHidden (sm xs x)
1837 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1838 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1839 sm xs x = x
1841 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1842 fullApp x = x
1844shadow :: Name -> Name -> PTerm -> PTerm
1845shadow n n' t = sm t where
1846 sm (PRef fc x) | n == x = PRef fc n'
1847 sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)
1848 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1849 sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)
1850 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1851 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1852 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1853 sm (PEq f xt yt x y) = PEq f (sm xt) (sm yt) (sm x) (sm y)
1854 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1855 sm (PTyped x y) = PTyped (sm x) (sm y)
1856 sm (PPair f p x y) = PPair f p (sm x) (sm y)
1857 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
1858 sm (PAlternative a as) = PAlternative a (map sm as)
1859 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1860 sm (PProof ts) = PProof (map (fmap sm) ts)
1861 sm (PHidden x) = PHidden (sm x)
1862 sm (PUnifyLog x) = PUnifyLog (sm x)
1863 sm (PNoImplicits x) = PNoImplicits (sm x)
1864 sm x = x
1866-- Rename any binders which are repeated (so that we don't have to mess
1867-- about with shadowing anywhere else).
1869mkUniqueNames :: [Name] -> PTerm -> PTerm
1870mkUniqueNames env tm = evalState (mkUniq tm) env where
1871 inScope = boundNamesIn tm
1873 mkUniqA arg = do t' <- mkUniq (getTm arg)
1874 return (arg { getTm = t' })
1876 -- Initialise the unique name with the environment length (so we're not
1877 -- looking for too long...)
1878 initN (UN n) l = UN $ txt (str n ++ show l)
1879 initN (MN i s) l = MN (i+l) s
1880 initN n l = n
1882 -- FIXME: Probably ought to do this for completeness! It's fine as
1883 -- long as there are no bindings inside tactics though.
1884 mkUniqT tac = return tac
1886 mkUniq :: PTerm -> State [Name] PTerm
1887 mkUniq (PLam n ty sc)
1888 = do env <- get
1889 (n', sc') <-
1890 if n `elem` env
1891 then do let n' = uniqueName (initN n (length env))
1892 (env ++ inScope)
1893 return (n', shadow n n' sc)
1894 else return (n, sc)
1895 put (n' : env)
1896 ty' <- mkUniq ty
1897 sc'' <- mkUniq sc'
1898 return $! PLam n' ty' sc''
1899 mkUniq (PPi p n ty sc)
1900 = do env <- get
1901 (n', sc') <-
1902 if n `elem` env
1903 then do let n' = uniqueName (initN n (length env))
1904 (env ++ inScope)
1905 return (n', shadow n n' sc)
1906 else return (n, sc)
1907 put (n' : env)
1908 ty' <- mkUniq ty
1909 sc'' <- mkUniq sc'
1910 return $! PPi p n' ty' sc''
1911 mkUniq (PLet n ty val sc)
1912 = do env <- get
1913 (n', sc') <-
1914 if n `elem` env
1915 then do let n' = uniqueName (initN n (length env))
1916 (env ++ inScope)
1917 return (n', shadow n n' sc)
1918 else return (n, sc)
1919 put (n' : env)
1920 ty' <- mkUniq ty; val' <- mkUniq val
1921 sc'' <- mkUniq sc'
1922 return $! PLet n' ty' val' sc''
1923 mkUniq (PApp fc t args)
1924 = do t' <- mkUniq t
1925 args' <- mapM mkUniqA args
1926 return $! PApp fc t' args'
1927 mkUniq (PAppBind fc t args)
1928 = do t' <- mkUniq t
1929 args' <- mapM mkUniqA args
1930 return $! PAppBind fc t' args'
1931 mkUniq (PCase fc t alts)
1932 = do t' <- mkUniq t
1933 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
1934 return (x', y')) alts
1935 return $! PCase fc t' alts'
1936 mkUniq (PPair fc p l r)
1937 = do l' <- mkUniq l; r' <- mkUniq r
1938 return $! PPair fc p l' r'
1939 mkUniq (PDPair fc p (PRef fc' n) t sc)
1940 | t /= Placeholder
1941 = do env <- get
1942 (n', sc') <- if n `elem` env
1943 then do let n' = uniqueName n (env ++ inScope)
1944 return (n', shadow n n' sc)
1945 else return (n, sc)
1946 put (n' : env)
1947 t' <- mkUniq t
1948 sc'' <- mkUniq sc'
1949 return $! PDPair fc p (PRef fc' n') t' sc''
1950 mkUniq (PDPair fc p l t r)
1951 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
1952 return $! PDPair fc p l' t' r'
1953 mkUniq (PAlternative b as)
1954 = liftM (PAlternative b) (mapM mkUniq as)
1955 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
1956 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
1957 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
1958 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
1959 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
1960 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
1961 mkUniq t = return t