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