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