git.iko.soy/Idris-dev
on c78fb14 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1945 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 Paths_idris
19import System.Console.Haskeline
20import System.IO
22import Control.Monad.State
23import Control.Monad.Error(throwError)
25import Data.List
26import Data.Char
27import qualified Data.Text as T
28import Data.Either
29import qualified Data.Map as M
30import Data.Maybe
31import qualified Data.Set as S
32import Data.Word (Word)
34import Debug.Trace
36import Control.Monad.Error (throwError, catchError)
37import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
39import Util.Pretty
40import Util.ScreenSize
41import Util.System
43getContext :: Idris Context
44getContext = do i <- getIState; return (tt_ctxt i)
46forCodegen :: Codegen -> [(Codegen, a)] -> [a]
47forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']
49getObjectFiles :: Codegen -> Idris [FilePath]
50getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
52addObjectFile :: Codegen -> FilePath -> Idris ()
53addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
55getLibs :: Codegen -> Idris [String]
56getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
58addLib :: Codegen -> String -> Idris ()
59addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
61getFlags :: Codegen -> Idris [String]
62getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
64addFlag :: Codegen -> String -> Idris ()
65addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
67addDyLib :: [String] -> Idris (Either DynamicLib String)
68addDyLib libs = do i <- getIState
69 let ls = idris_dynamic_libs i
70 let importdirs = opt_importdirs (idris_options i)
71 case mapMaybe (findDyLib ls) libs of
72 x:_ -> return (Left x)
73 [] -> do
74 handle <- lift . lift .
75 mapM (\l -> catchIO (tryLoadLib importdirs l)
76 (\_ -> return Nothing)) $ libs
77 case msum handle of
78 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
79 concat (intersperse "," libs) ++ "\"")
80 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
81 return (Left x)
82 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
83 findDyLib [] l = Nothing
84 findDyLib (lib:libs) l | l == lib_name lib = Just lib
85 | otherwise = findDyLib libs l
88addHdr :: Codegen -> String -> Idris ()
89addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
91addLangExt :: LanguageExt -> Idris ()
92addLangExt TypeProviders = do i <- getIState
93 putIState $ i {
94 idris_language_extensions = TypeProviders : idris_language_extensions i
95 }
96addLangExt ErrorReflection = do i <- getIState
97 putIState $ i {
98 idris_language_extensions = ErrorReflection : idris_language_extensions i
99 }
101addTrans :: (Term, Term) -> Idris ()
102addTrans t = do i <- getIState
103 putIState $ i { idris_transforms = t : idris_transforms i }
105addErrRev :: (Term, Term) -> Idris ()
106addErrRev t = do i <- getIState
107 putIState $ i { idris_errRev = t : idris_errRev i }
109totcheck :: (FC, Name) -> Idris ()
110totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
112defer_totcheck :: (FC, Name) -> Idris ()
113defer_totcheck n
114 = do i <- getIState;
115 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
117clear_totcheck :: Idris ()
118clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
120setFlags :: Name -> [FnOpt] -> Idris ()
121setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
123setAccessibility :: Name -> Accessibility -> Idris ()
124setAccessibility n a
125 = do i <- getIState
126 let ctxt = setAccess n a (tt_ctxt i)
127 putIState $ i { tt_ctxt = ctxt }
129setTotality :: Name -> Totality -> Idris ()
130setTotality n a
131 = do i <- getIState
132 let ctxt = setTotal n a (tt_ctxt i)
133 putIState $ i { tt_ctxt = ctxt }
135getTotality :: Name -> Idris Totality
136getTotality n
137 = do i <- getIState
138 case lookupTotal n (tt_ctxt i) of
139 [t] -> return t
140 _ -> return (Total [])
142-- Get coercions which might return the required type
143getCoercionsTo :: IState -> Type -> [Name]
144getCoercionsTo i ty =
145 let cs = idris_coercions i
146 (fn,_) = unApply (getRetTy ty) in
147 findCoercions fn cs
148 where findCoercions t [] = []
149 findCoercions t (n : ns) =
150 let ps = case lookupTy n (tt_ctxt i) of
151 [ty'] -> case unApply (getRetTy ty') of
152 (t', _) ->
153 if t == t' then [n] else []
154 _ -> [] in
155 ps ++ findCoercions t ns
157addToCG :: Name -> CGInfo -> Idris ()
158addToCG n cg
159 = do i <- getIState
160 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
162addTyInferred :: Name -> Idris ()
163addTyInferred n
164 = do i <- getIState
165 putIState $ i { idris_tyinfodata =
166 addDef n TIPartial (idris_tyinfodata i) }
168addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()
169addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts
170 mapM_ addConstraint ts
171 return ()
172 where addConstraint (x, y) = findMVApps x y
174 findMVApps x y
175 = do let (fx, argsx) = unApply x
176 let (fy, argsy) = unApply y
177 if (not (fx == fy))
178 then do
179 tryAddMV fx y
180 tryAddMV fy x
181 else mapM_ addConstraint (zip argsx argsy)
183 tryAddMV (P _ mv _) y =
184 do ist <- get
185 case lookup mv (idris_metavars ist) of
186 Just _ -> addConstraintRule mv y
187 _ -> return ()
188 tryAddMV _ _ = return ()
190 addConstraintRule :: Name -> Term -> Idris ()
191 addConstraintRule n t
192 = do ist <- get
193 logLvl 1 $ "TI constraint: " ++ show (n, t)
194 case lookupCtxt n (idris_tyinfodata ist) of
195 [TISolution ts] ->
196 do mapM_ (checkConsistent t) ts
197 let ti' = addDef n (TISolution (t : ts))
198 (idris_tyinfodata ist)
199 put $ ist { idris_tyinfodata = ti' }
200 _ ->
201 do let ti' = addDef n (TISolution [t])
202 (idris_tyinfodata ist)
203 put $ ist { idris_tyinfodata = ti' }
205 -- Check a solution is consistent with previous solutions
206 -- Meaning: If heads are both data types, they had better be the
207 -- same.
208 checkConsistent :: Term -> Term -> Idris ()
209 checkConsistent x y =
210 do let (fx, _) = unApply x
211 let (fy, _) = unApply y
212 case (fx, fy) of
213 (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)
214 (P (TCon _ _) n _, Constant _) -> errWhen True
215 (Constant _, P (TCon _ _) n' _) -> errWhen True
216 (P (DCon _ _) n _, P (DCon _ _) n' _) -> errWhen (n/=n)
217 _ -> return ()
219 where errWhen True
220 = throwError (At fc
221 (CantUnify False x y (Msg "") [] 0))
222 errWhen False = return ()
224isTyInferred :: Name -> Idris Bool
225isTyInferred n
226 = do i <- getIState
227 case lookupCtxt n (idris_tyinfodata i) of
228 [TIPartial] -> return True
229 _ -> return False
231-- | Adds error handlers for a particular function and argument. If names are
232-- ambiguous, all matching handlers are updated.
233addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()
234addFunctionErrorHandlers f arg hs =
235 do i <- getIState
236 let oldHandlers = idris_function_errorhandlers i
237 let newHandlers = flip (addDef f) oldHandlers $
238 case lookupCtxtExact f oldHandlers of
239 Nothing -> M.singleton arg (S.fromList hs)
240 Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers
241 -- will always be one of those two, thus no extra case
242 putIState $ i { idris_function_errorhandlers = newHandlers }
244getFunctionErrorHandlers :: Name -> Name -> Idris [Name]
245getFunctionErrorHandlers f arg = do i <- getIState
246 return . maybe [] S.toList $
247 undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)
250-- Trace all the names in a call graph starting at the given name
251getAllNames :: Name -> Idris [Name]
252getAllNames n = allNames [] n
254allNames :: [Name] -> Name -> Idris [Name]
255allNames ns n | n `elem` ns = return []
256allNames ns n = do i <- getIState
257 case lookupCtxtExact n (idris_callgraph i) of
258 Just ns' -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
259 return (nub (n : concat more))
260 _ -> return [n]
262addCoercion :: Name -> Idris ()
263addCoercion n = do i <- getIState
264 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
266addDocStr :: Name -> Docstring -> [(Name, Docstring)] -> Idris ()
267addDocStr n doc args
268 = do i <- getIState
269 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }
271addNameHint :: Name -> Name -> Idris ()
272addNameHint ty n
273 = do i <- getIState
274 ty' <- case lookupCtxtName ty (idris_implicits i) of
275 [(tyn, _)] -> return tyn
276 [] -> throwError (NoSuchVariable ty)
277 tyns -> throwError (CantResolveAlts (map show (map fst tyns)))
278 let ns' = case lookupCtxt ty' (idris_namehints i) of
279 [ns] -> ns ++ [n]
280 _ -> [n]
281 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
283getNameHints :: IState -> Name -> [Name]
284getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
285getNameHints i n =
286 case lookupCtxt n (idris_namehints i) of
287 [ns] -> ns
288 _ -> []
290addToCalledG :: Name -> [Name] -> Idris ()
291addToCalledG n ns = return () -- TODO
293-- Add a class instance function. Dodgy hack: Put integer instances first in the
294-- list so they are resolved by default.
295-- Dodgy hack 2: put constraint chasers (@@) last
297addInstance :: Bool -> Name -> Name -> Idris ()
298addInstance int n i
299 = do ist <- getIState
300 case lookupCtxt n (idris_classes ist) of
301 [CI a b c d e ins] ->
302 do let cs = addDef n (CI a b c d e (addI i ins)) (idris_classes ist)
303 putIState $ ist { idris_classes = cs }
304 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [i]) (idris_classes ist)
305 putIState $ ist { idris_classes = cs }
306 where addI i ins | int = i : ins
307 | chaser n = ins ++ [i]
308 | otherwise = insI i ins
309 insI i [] = [i]
310 insI i (n : ns) | chaser n = i : n : ns
311 | otherwise = n : insI i ns
313 chaser (UN nm)
314 | ('@':'@':_) <- str nm = True
315 chaser (NS n _) = chaser n
316 chaser _ = False
318addClass :: Name -> ClassInfo -> Idris ()
319addClass n i
320 = do ist <- getIState
321 let i' = case lookupCtxt n (idris_classes ist) of
322 [c] -> c { class_instances = class_instances i }
323 _ -> i
324 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
326addIBC :: IBCWrite -> Idris ()
327addIBC ibc@(IBCDef n)
328 = do i <- getIState
329 when (notDef (ibc_write i)) $
330 putIState $ i { ibc_write = ibc : ibc_write i }
331 where notDef [] = True
332 notDef (IBCDef n': is) | n == n' = False
333 notDef (_ : is) = notDef is
334addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
336clearIBC :: Idris ()
337clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
339resetNameIdx :: Idris ()
340resetNameIdx = do i <- getIState
341 put (i { idris_nameIdx = (0, emptyContext) })
343-- Used to preserve sharing of names
344addNameIdx :: Name -> Idris (Int, Name)
345addNameIdx n = do i <- getIState
346 let (i', x) = addNameIdx' i n
347 return x
349addNameIdx' :: IState -> Name -> (IState, (Int, Name))
350addNameIdx' i n
351 = let idxs = snd (idris_nameIdx i) in
352 case lookupCtxt n idxs of
353 [x] -> (i, x)
354 _ -> let i' = fst (idris_nameIdx i) + 1 in
355 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
357getHdrs :: Codegen -> Idris [String]
358getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
360setErrSpan :: FC -> Idris ()
361setErrSpan x = do i <- getIState;
362 case (errSpan i) of
363 Nothing -> putIState $ i { errSpan = Just x }
364 Just _ -> return ()
366clearErr :: Idris ()
367clearErr = do i <- getIState
368 putIState $ i { errSpan = Nothing }
370getSO :: Idris (Maybe String)
371getSO = do i <- getIState
372 return (compiled_so i)
374setSO :: Maybe String -> Idris ()
375setSO s = do i <- getIState
376 putIState $ (i { compiled_so = s })
378getIState :: Idris IState
379getIState = get
381putIState :: IState -> Idris ()
382putIState = put
384-- | A version of liftIO that puts errors into the exception type of the Idris monad
385runIO :: IO a -> Idris a
386runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
387-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
389getName :: Idris Int
390getName = do i <- getIState;
391 let idx = idris_name i;
392 putIState $ (i { idris_name = idx + 1 })
393 return idx
395-- InternalApp keeps track of the real function application for making case splits from, not the application the
396-- programmer wrote, which doesn't have the whole context in any case other than top level definitions
397addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
398addInternalApp fp l t
399 = do i <- getIState
400 putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })
402getInternalApp :: FilePath -> Int -> Idris PTerm
403getInternalApp fp l = do i <- getIState
404 case lookup (fp, l) (idris_lineapps i) of
405 Just n' -> return n'
406 Nothing -> return Placeholder
407 -- TODO: What if it's not there?
409-- Pattern definitions are only used for coverage checking, so erase them
410-- when we're done
411clearOrigPats :: Idris ()
412clearOrigPats = do i <- get
413 let ps = idris_patdefs i
414 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
415 put (i { idris_patdefs = ps' })
417-- Erase types from Ps in the context (basically ending up with what's in
418-- the .ibc, which is all we need after all the analysis is done)
419clearPTypes :: Idris ()
420clearPTypes = do i <- get
421 let ctxt = tt_ctxt i
422 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
423 where pErase (CaseOp c t tys orig tot cds)
424 = CaseOp c t tys orig [] (pErase' cds)
425 pErase x = x
426 pErase' (CaseDefs _ (cs, c) _ rs)
427 = let c' = (cs, fmap pEraseType c) in
428 CaseDefs c' c' c' rs
430checkUndefined :: FC -> Name -> Idris ()
431checkUndefined fc n
432 = do i <- getContext
433 case lookupTy n i of
434 (_:_) -> throwError . Msg $ show fc ++ ":" ++
435 show n ++ " already defined"
436 _ -> return ()
438isUndefined :: FC -> Name -> Idris Bool
439isUndefined fc n
440 = do i <- getContext
441 case lookupTy n i of
442 (_:_) -> return False
443 _ -> return True
445setContext :: Context -> Idris ()
446setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
448updateContext :: (Context -> Context) -> Idris ()
449updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
451addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
452addConstraints fc (v, cs)
453 = do i <- getIState
454 let ctxt = tt_ctxt i
455 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
456 next_tvar = v }
457 let ics = zip cs (repeat fc) ++ idris_constraints i
458 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
460addDeferred = addDeferred' Ref
461addDeferredTyCon = addDeferred' (TCon 0 0)
463addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
464addDeferred' nt ns
465 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns
466 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
467 i <- getIState
468 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
469 idris_metavars i }
470 where tidyNames used (Bind (MN i x) b sc)
471 = let n' = uniqueName (UN x) used in
472 Bind n' b $ tidyNames (n':used) sc
473 tidyNames used (Bind n b sc)
474 = let n' = uniqueName n used in
475 Bind n' b $ tidyNames (n':used) sc
476 tidyNames used b = b
478solveDeferred :: Name -> Idris ()
479solveDeferred n = do i <- getIState
480 putIState $ i { idris_metavars =
481 filter (\(n', _) -> n/=n')
482 (idris_metavars i),
483 ibc_write =
484 filter (notMV n) (ibc_write i)
485 }
486 where notMV n (IBCMetavar n') = not (n == n')
487 notMV n _ = True
489getUndefined :: Idris [Name]
490getUndefined = do i <- getIState
491 return (map fst (idris_metavars i) \\ primDefs)
493getWidth :: Idris ConsoleWidth
494getWidth = fmap idris_consolewidth getIState
496setWidth :: ConsoleWidth -> Idris ()
497setWidth w = do ist <- getIState
498 put ist { idris_consolewidth = w }
500renderWidth :: Idris Int
501renderWidth = do iw <- getWidth
502 case iw of
503 InfinitelyWide -> return 100000000
504 ColsWide n -> return (max n 1)
505 AutomaticWidth -> runIO getScreenWidth
508iRender :: Doc a -> Idris (SimpleDoc a)
509iRender d = do w <- getWidth
510 ist <- getIState
511 let ideSlave = case idris_outputmode ist of
512 IdeSlave _ -> True
513 _ -> False
514 case w of
515 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d
516 ColsWide n -> return $
517 if n < 1
518 then renderPretty 1.0 1000000000 d
519 else renderPretty 0.8 n d
520 AutomaticWidth | ideSlave -> return $ renderPretty 1.0 1000000000 d
521 | otherwise -> do width <- runIO getScreenWidth
522 return $ renderPretty 0.8 width d
524ihPrintResult :: Handle -> String -> Idris ()
525ihPrintResult h s = do i <- getIState
526 case idris_outputmode i of
527 RawOutput -> case s of
528 "" -> return ()
529 s -> runIO $ hPutStrLn h s
530 IdeSlave n ->
531 let good = SexpList [SymbolAtom "ok", toSExp s] in
532 runIO $ hPutStrLn h $ convSExp "return" good n
534-- | Write a pretty-printed term to the console with semantic coloring
535consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
536consoleDisplayAnnotated h output = do ist <- getIState
537 rendered <- iRender $ output
538 runIO . hPutStrLn h .
539 displayDecorated (consoleDecorate ist) $
540 rendered
543-- | Write pretty-printed output to IDESlave with semantic annotations
544ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
545ideSlaveReturnAnnotated n h out = do ist <- getIState
546 (str, spans) <- fmap displaySpans .
547 iRender .
548 fmap (fancifyAnnots ist) $
549 out
550 let good = [SymbolAtom "ok", toSExp str, toSExp spans]
551 runIO . hPutStrLn h $ convSExp "return" good n
553ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
554ihPrintTermWithType h tm ty = do ist <- getIState
555 let output = tm <+> colon <+> ty
556 case idris_outputmode ist of
557 RawOutput -> consoleDisplayAnnotated h output
558 IdeSlave n -> ideSlaveReturnAnnotated n h output
560-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name
561ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()
562ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n
563ihPrintFunTypes h bnd n overloads = do imp <- impShow
564 ist <- getIState
565 let output = vsep (map (uncurry (ppOverload imp)) overloads)
566 case idris_outputmode ist of
567 RawOutput -> consoleDisplayAnnotated h output
568 IdeSlave n -> ideSlaveReturnAnnotated n h output
569 where fullName n = prettyName True bnd n
570 ppOverload imp n tm = fullName n <+> colon <+> align (pprintPTerm imp bnd [] tm)
572ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()
573ihRenderResult h d = do ist <- getIState
574 case idris_outputmode ist of
575 RawOutput -> consoleDisplayAnnotated h d
576 IdeSlave n -> ideSlaveReturnAnnotated n h d
578fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
579fancifyAnnots ist annot@(AnnName n _ _) =
580 do let ctxt = tt_ctxt ist
581 case () of
582 _ | isDConName n ctxt -> AnnName n (Just DataOutput) Nothing
583 _ | isFnName n ctxt -> AnnName n (Just FunOutput) Nothing
584 _ | isTConName n ctxt -> AnnName n (Just TypeOutput) Nothing
585 _ | otherwise -> annot
586fancifyAnnots _ annot = annot
588type1Doc :: Doc OutputAnnotation
589type1Doc = (annotate AnnConstType $ text "Type 1")
591-- | Show an error with semantic highlighting
592ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()
593ihRenderError h e = do ist <- getIState
594 case idris_outputmode ist of
595 RawOutput -> consoleDisplayAnnotated h e
596 IdeSlave n -> do
597 (str, spans) <- fmap displaySpans .
598 iRender .
599 fmap (fancifyAnnots ist) $
600 e
601 let good = [SymbolAtom "error", toSExp str, toSExp spans]
602 runIO . hPutStrLn h $ convSExp "return" good n
604ihPrintError :: Handle -> String -> Idris ()
605ihPrintError h s = do i <- getIState
606 case idris_outputmode i of
607 RawOutput -> case s of
608 "" -> return ()
609 s -> runIO $ hPutStrLn h s
610 IdeSlave n ->
611 let good = SexpList [SymbolAtom "error", toSExp s] in
612 runIO . hPutStrLn h $ convSExp "return" good n
614ihputStrLn :: Handle -> String -> Idris ()
615ihputStrLn h s = do i <- getIState
616 case idris_outputmode i of
617 RawOutput -> runIO $ hPutStrLn h s
618 IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n
620iputStrLn = ihputStrLn stdout
621iPrintError = ihPrintError stdout
622iPrintResult = ihPrintResult stdout
623iWarn = ihWarn stdout
625ideslavePutSExp :: SExpable a => String -> a -> Idris ()
626ideslavePutSExp cmd info = do i <- getIState
627 case idris_outputmode i of
628 IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
629 _ -> return ()
631-- this needs some typing magic and more structured output towards emacs
632iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
633iputGoal g = do i <- getIState
634 case idris_outputmode i of
635 RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)
636 IdeSlave n -> runIO . putStrLn $
637 convSExp "write-goal" (displayS (fmap (fancifyAnnots i) g) "") n
639isetPrompt :: String -> Idris ()
640isetPrompt p = do i <- getIState
641 case idris_outputmode i of
642 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n
644ihWarn :: Handle -> FC -> Doc OutputAnnotation -> Idris ()
645ihWarn h fc err = do i <- getIState
646 case idris_outputmode i of
647 RawOutput ->
648 do err' <- iRender . fmap (fancifyAnnots i) $
649 text (show fc) <> colon <//> err
650 runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'
651 IdeSlave n ->
652 do err' <- iRender . fmap (fancifyAnnots i) $ err
653 let (str, spans) = displaySpans err'
654 runIO . hPutStrLn h $
655 convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n
657setLogLevel :: Int -> Idris ()
658setLogLevel l = do i <- getIState
659 let opts = idris_options i
660 let opt' = opts { opt_logLevel = l }
661 putIState $ i { idris_options = opt' }
663setCmdLine :: [Opt] -> Idris ()
664setCmdLine opts = do i <- getIState
665 let iopts = idris_options i
666 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
668getCmdLine :: Idris [Opt]
669getCmdLine = do i <- getIState
670 return (opt_cmdline (idris_options i))
672getDumpDefun :: Idris (Maybe FilePath)
673getDumpDefun = do i <- getIState
674 return $ findC (opt_cmdline (idris_options i))
675 where findC [] = Nothing
676 findC (DumpDefun x : _) = Just x
677 findC (_ : xs) = findC xs
679getDumpCases :: Idris (Maybe FilePath)
680getDumpCases = do i <- getIState
681 return $ findC (opt_cmdline (idris_options i))
682 where findC [] = Nothing
683 findC (DumpCases x : _) = Just x
684 findC (_ : xs) = findC xs
686logLevel :: Idris Int
687logLevel = do i <- getIState
688 return (opt_logLevel (idris_options i))
690setErrContext :: Bool -> Idris ()
691setErrContext t = do i <- getIState
692 let opts = idris_options i
693 let opt' = opts { opt_errContext = t }
694 putIState $ i { idris_options = opt' }
696errContext :: Idris Bool
697errContext = do i <- getIState
698 return (opt_errContext (idris_options i))
700useREPL :: Idris Bool
701useREPL = do i <- getIState
702 return (opt_repl (idris_options i))
704setREPL :: Bool -> Idris ()
705setREPL t = do i <- getIState
706 let opts = idris_options i
707 let opt' = opts { opt_repl = t }
708 putIState $ i { idris_options = opt' }
710showOrigErr :: Idris Bool
711showOrigErr = do i <- getIState
712 return (opt_origerr (idris_options i))
714setShowOrigErr :: Bool -> Idris ()
715setShowOrigErr b = do i <- getIState
716 let opts = idris_options i
717 let opt' = opts { opt_origerr = b }
718 putIState $ i { idris_options = opt' }
720setAutoSolve :: Bool -> Idris ()
721setAutoSolve b = do i <- getIState
722 let opts = idris_options i
723 let opt' = opts { opt_autoSolve = b }
724 putIState $ i { idris_options = opt' }
726setNoBanner :: Bool -> Idris ()
727setNoBanner n = do i <- getIState
728 let opts = idris_options i
729 let opt' = opts { opt_nobanner = n }
730 putIState $ i { idris_options = opt' }
732getNoBanner :: Idris Bool
733getNoBanner = do i <- getIState
734 let opts = idris_options i
735 return (opt_nobanner opts)
737setQuiet :: Bool -> Idris ()
738setQuiet q = do i <- getIState
739 let opts = idris_options i
740 let opt' = opts { opt_quiet = q }
741 putIState $ i { idris_options = opt' }
743getQuiet :: Idris Bool
744getQuiet = do i <- getIState
745 let opts = idris_options i
746 return (opt_quiet opts)
748setCodegen :: Codegen -> Idris ()
749setCodegen t = do i <- getIState
750 let opts = idris_options i
751 let opt' = opts { opt_codegen = t }
752 putIState $ i { idris_options = opt' }
754codegen :: Idris Codegen
755codegen = do i <- getIState
756 return (opt_codegen (idris_options i))
758setOutputTy :: OutputType -> Idris ()
759setOutputTy t = do i <- getIState
760 let opts = idris_options i
761 let opt' = opts { opt_outputTy = t }
762 putIState $ i { idris_options = opt' }
764outputTy :: Idris OutputType
765outputTy = do i <- getIState
766 return $ opt_outputTy $ idris_options i
768setIdeSlave :: Bool -> Idris ()
769setIdeSlave True = do i <- getIState
770 putIState $ i { idris_outputmode = (IdeSlave 0), idris_colourRepl = False }
771setIdeSlave False = return ()
773setTargetTriple :: String -> Idris ()
774setTargetTriple t = do i <- getIState
775 let opts = idris_options i
776 opt' = opts { opt_triple = t }
777 putIState $ i { idris_options = opt' }
779targetTriple :: Idris String
780targetTriple = do i <- getIState
781 return (opt_triple (idris_options i))
783setTargetCPU :: String -> Idris ()
784setTargetCPU t = do i <- getIState
785 let opts = idris_options i
786 opt' = opts { opt_cpu = t }
787 putIState $ i { idris_options = opt' }
789targetCPU :: Idris String
790targetCPU = do i <- getIState
791 return (opt_cpu (idris_options i))
793setOptLevel :: Word -> Idris ()
794setOptLevel t = do i <- getIState
795 let opts = idris_options i
796 opt' = opts { opt_optLevel = t }
797 putIState $ i { idris_options = opt' }
799optLevel :: Idris Word
800optLevel = do i <- getIState
801 return (opt_optLevel (idris_options i))
803verbose :: Idris Bool
804verbose = do i <- getIState
805 return (opt_verbose (idris_options i))
807setVerbose :: Bool -> Idris ()
808setVerbose t = do i <- getIState
809 let opts = idris_options i
810 let opt' = opts { opt_verbose = t }
811 putIState $ i { idris_options = opt' }
813typeInType :: Idris Bool
814typeInType = do i <- getIState
815 return (opt_typeintype (idris_options i))
817setTypeInType :: Bool -> Idris ()
818setTypeInType t = do i <- getIState
819 let opts = idris_options i
820 let opt' = opts { opt_typeintype = t }
821 putIState $ i { idris_options = opt' }
823coverage :: Idris Bool
824coverage = do i <- getIState
825 return (opt_coverage (idris_options i))
827setCoverage :: Bool -> Idris ()
828setCoverage t = do i <- getIState
829 let opts = idris_options i
830 let opt' = opts { opt_coverage = t }
831 putIState $ i { idris_options = opt' }
833setIBCSubDir :: FilePath -> Idris ()
834setIBCSubDir fp = do i <- getIState
835 let opts = idris_options i
836 let opt' = opts { opt_ibcsubdir = fp }
837 putIState $ i { idris_options = opt' }
839valIBCSubDir :: IState -> Idris FilePath
840valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
842addImportDir :: FilePath -> Idris ()
843addImportDir fp = do i <- getIState
844 let opts = idris_options i
845 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
846 putIState $ i { idris_options = opt' }
848setImportDirs :: [FilePath] -> Idris ()
849setImportDirs fps = do i <- getIState
850 let opts = idris_options i
851 let opt' = opts { opt_importdirs = fps }
852 putIState $ i { idris_options = opt' }
854allImportDirs :: Idris [FilePath]
855allImportDirs = do i <- getIState
856 let optdirs = opt_importdirs (idris_options i)
857 return ("." : reverse optdirs)
859colourise :: Idris Bool
860colourise = do i <- getIState
861 return $ idris_colourRepl i
863setColourise :: Bool -> Idris ()
864setColourise b = do i <- getIState
865 putIState $ i { idris_colourRepl = b }
867setOutH :: Handle -> Idris ()
868setOutH h = do i <- getIState
869 putIState $ i { idris_outh = h }
871impShow :: Idris Bool
872impShow = do i <- getIState
873 return (opt_showimp (idris_options i))
875setImpShow :: Bool -> Idris ()
876setImpShow t = do i <- getIState
877 let opts = idris_options i
878 let opt' = opts { opt_showimp = t }
879 putIState $ i { idris_options = opt' }
881setColour :: ColourType -> IdrisColour -> Idris ()
882setColour ct c = do i <- getIState
883 let newTheme = setColour' ct c (idris_colourTheme i)
884 putIState $ i { idris_colourTheme = newTheme }
885 where setColour' KeywordColour c t = t { keywordColour = c }
886 setColour' BoundVarColour c t = t { boundVarColour = c }
887 setColour' ImplicitColour c t = t { implicitColour = c }
888 setColour' FunctionColour c t = t { functionColour = c }
889 setColour' TypeColour c t = t { typeColour = c }
890 setColour' DataColour c t = t { dataColour = c }
891 setColour' PromptColour c t = t { promptColour = c }
893logLvl :: Int -> String -> Idris ()
894logLvl l str = do i <- getIState
895 let lvl = opt_logLevel (idris_options i)
896 when (lvl >= l) $
897 case idris_outputmode i of
898 RawOutput -> do runIO $ putStrLn str
899 IdeSlave n ->
900 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
901 runIO $ putStrLn $ convSExp "log" good n
903cmdOptType :: Opt -> Idris Bool
904cmdOptType x = do i <- getIState
905 return $ x `elem` opt_cmdline (idris_options i)
907iLOG :: String -> Idris ()
908iLOG = logLvl 1
910noErrors :: Idris Bool
911noErrors = do i <- getIState
912 case errSpan i of
913 Nothing -> return True
914 _ -> return False
916setTypeCase :: Bool -> Idris ()
917setTypeCase t = do i <- getIState
918 let opts = idris_options i
919 let opt' = opts { opt_typecase = t }
920 putIState $ i { idris_options = opt' }
923-- Dealing with parameters
925expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
926 [Name] -> -- all names
927 [Name] -> -- names with no declaration
928 PTerm -> PTerm
929expandParams dec ps ns infs tm = en tm
930 where
931 -- if we shadow a name (say in a lambda binding) that is used in a call to
932 -- a lifted function, we need access to both names - once in the scope of the
933 -- binding and once to call the lifted functions. So we'll explicitly shadow
934 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
935 -- but we didn't...)
937 mkShadow (UN n) = MN 0 n
938 mkShadow (MN i n) = MN (i+1) n
939 mkShadow (NS x s) = NS (mkShadow x) s
941 en (PLam n t s)
942 | n `elem` (map fst ps ++ ns)
943 = let n' = mkShadow n in
944 PLam n' (en t) (en (shadow n n' s))
945 | otherwise = PLam n (en t) (en s)
946 en (PPi p n t s)
947 | n `elem` (map fst ps ++ ns)
948 = let n' = mkShadow n in -- FIXME THINK SHADOWING TacImp?
949 PPi (enTacImp p) n' (en t) (en (shadow n n' s))
950 | otherwise = PPi (enTacImp p) n (en t) (en s)
951 en (PLet n ty v s)
952 | n `elem` (map fst ps ++ ns)
953 = let n' = mkShadow n in
954 PLet n' (en ty) (en v) (en (shadow n n' s))
955 | otherwise = PLet n (en ty) (en v) (en s)
956 -- FIXME: Should only do this in a type signature!
957 en (PDPair f p (PRef f' n) t r)
958 | n `elem` (map fst ps ++ ns) && t /= Placeholder
959 = let n' = mkShadow n in
960 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))
961 en (PEq f l r) = PEq f (en l) (en r)
962 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
963 en (PTyped l r) = PTyped (en l) (en r)
964 en (PPair f p l r) = PPair f p (en l) (en r)
965 en (PDPair f p l t r) = PDPair f p (en l) (en t) (en r)
966 en (PAlternative a as) = PAlternative a (map en as)
967 en (PHidden t) = PHidden (en t)
968 en (PUnifyLog t) = PUnifyLog (en t)
969 en (PDisamb ds t) = PDisamb ds (en t)
970 en (PNoImplicits t) = PNoImplicits (en t)
971 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
972 en (PProof ts) = PProof (map (fmap en) ts)
973 en (PTactics ts) = PTactics (map (fmap en) ts)
975 en (PQuote (Var n))
976 | n `nselem` ns = PQuote (Var (dec n))
977 en (PApp fc (PInferRef fc' n) as)
978 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
979 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
980 en (PApp fc (PRef fc' n) as)
981 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
982 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
983 | n `nselem` ns = PApp fc (PRef fc' (dec n))
984 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
985 en (PAppBind fc (PRef fc' n) as)
986 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
987 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
988 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
989 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
990 en (PRef fc n)
991 | n `elem` infs = PApp fc (PInferRef fc (dec n))
992 (map (pexp . (PRef fc)) (map fst ps))
993 | n `nselem` ns = PApp fc (PRef fc (dec n))
994 (map (pexp . (PRef fc)) (map fst ps))
995 en (PInferRef fc n)
996 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
997 (map (pexp . (PRef fc)) (map fst ps))
998 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
999 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
1000 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
1001 en t = t
1003 nselem x [] = False
1004 nselem x (y : xs) | nseq x y = True
1005 | otherwise = nselem x xs
1007 nseq x y = nsroot x == nsroot y
1009 enTacImp (TacImp aos st scr) = TacImp aos st (en scr)
1010 enTacImp other = other
1012expandParamsD :: Bool -> -- True = RHS only
1013 IState ->
1014 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
1015expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty)
1016 = if n `elem` ns && (not rhsonly)
1017 then -- trace (show (n, expandParams dec ps ns ty)) $
1018 PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
1019 else --trace (show (n, expandParams dec ps ns ty)) $
1020 PTy doc argdocs syn fc o n (expandParams dec ps ns [] ty)
1021expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
1022 = if n `elem` ns && (not rhsonly)
1023 then -- trace (show (n, expandParams dec ps ns ty)) $
1024 PPostulate doc syn fc o (dec n) (piBind ps
1025 (expandParams dec ps ns [] ty))
1026 else --trace (show (n, expandParams dec ps ns ty)) $
1027 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
1028expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
1029 = let n' = if n `elem` ns then dec n else n in
1030 PClauses fc opts n' (map expandParamsC cs)
1031 where
1032 expandParamsC (PClause fc n lhs ws rhs ds)
1033 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
1034 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1035 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1036 n' = if n `elem` ns then dec n else n
1037 -- names bound on the lhs should not be expanded on the rhs
1038 ns' = removeBound lhs ns in
1039 PClause fc n' lhs'
1040 (map (expandParams dec ps'' ns' []) ws)
1041 (expandParams dec ps'' ns' [] rhs)
1042 (map (expandParamsD True ist dec ps'' ns') ds)
1043 expandParamsC (PWith fc n lhs ws wval ds)
1044 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
1045 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
1046 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
1047 n' = if n `elem` ns then dec n else n
1048 ns' = removeBound lhs ns in
1049 PWith fc n' lhs'
1050 (map (expandParams dec ps'' ns' []) ws)
1051 (expandParams dec ps'' ns' [] wval)
1052 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
1053 updateps yn nm [] = []
1054 updateps yn nm (((a, t), i):as)
1055 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
1056 | otherwise = (sMN i (show n ++ "_u"), t) : updateps yn nm as
1058 removeBound lhs ns = ns \\ nub (bnames lhs)
1060 bnames (PRef _ n) = [n]
1061 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
1062 bnames (PPair _ _ l r) = bnames l ++ bnames r
1063 bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r
1064 bnames _ = []
1066expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
1067 = PData doc argDocs syn fc co (expandPData pd)
1068 where
1069 -- just do the type decl, leave constructors alone (parameters will be
1070 -- added implicitly)
1071 expandPData (PDatadecl n ty cons)
1072 = if n `elem` ns
1073 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
1074 (map econ cons)
1075 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
1076 econ (doc, argDocs, n, t, fc, fs)
1077 = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
1078expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty cdoc cn cty)
1079 = if tn `elem` ns
1080 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))
1081 cdoc (dec cn) conty
1082 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)
1083 cdoc (dec cn) conty
1084 where conty = piBindp expl ps (expandParams dec ps ns [] cty)
1085expandParamsD rhs ist dec ps ns (PParams f params pds)
1086 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1087 (map (expandParamsD True ist dec ps ns) pds)
1088-- (map (expandParamsD ist dec ps ns) pds)
1089expandParamsD rhs ist dec ps ns (PMutual f pds)
1090 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
1091expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
1092 = PClass doc info f
1093 (map (expandParams dec ps ns []) cs)
1095 (map (mapsnd (expandParams dec ps ns [])) params)
1096 (map (expandParamsD rhs ist dec ps ns) decls)
1097expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
1098 = PInstance info f
1099 (map (expandParams dec ps ns []) cs)
1101 (map (expandParams dec ps ns []) params)
1102 (expandParams dec ps ns [] ty)
1103 cn
1104 (map (expandParamsD rhs ist dec ps ns) decls)
1105expandParamsD rhs ist dec ps ns d = d
1107mapsnd f (x, t) = (x, f t)
1109-- Calculate a priority for a type, for deciding elaboration order
1110-- * if it's just a type variable or concrete type, do it early (0)
1111-- * if there's only type variables and injective constructors, do it next (1)
1112-- * if there's a function type, next (2)
1113-- * finally, everything else (3)
1115getPriority :: IState -> PTerm -> Int
1116getPriority i tm = 1 -- pri tm
1117 where
1118 pri (PRef _ n) =
1119 case lookupP n (tt_ctxt i) of
1120 ((P (DCon _ _) _ _):_) -> 1
1121 ((P (TCon _ _) _ _):_) -> 1
1122 ((P Ref _ _):_) -> 1
1123 [] -> 0 -- must be locally bound, if it's not an error...
1124 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
1125 pri (PTrue _ _) = 0
1126 pri (PFalse _) = 0
1127 pri (PRefl _ _) = 1
1128 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
1129 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
1130 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1131 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
1132 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
1133 pri (PTyped l r) = pri l
1134 pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))
1135 pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
1136 pri (PAlternative a as) = maximum (map pri as)
1137 pri (PConstant _) = 0
1138 pri Placeholder = 1
1139 pri _ = 3
1142addStatics :: Name -> Term -> PTerm -> Idris ()
1143addStatics n tm ptm =
1144 do let (statics, dynamics) = initStatics tm ptm
1145 let stnames = nub $ concatMap freeArgNames (map snd statics)
1146 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
1147 -- also get the arguments which are 'uniquely inferrable' from
1148 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1149 let statics' = nub $ map fst statics ++
1150 filter (\x -> not (elem x dnames)) stnames
1151 let stpos = staticList statics' tm
1152 i <- getIState
1153 when (not (null statics)) $
1154 logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics
1155 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
1156 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
1157 addIBC (IBCStatic n)
1158 where
1159 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
1160 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
1161 if pstatic p == Static then ((n, ty) : static, dynamic)
1162 else if (not (searchArg p))
1163 then (static, (n, ty) : dynamic)
1164 else (static, dynamic)
1165 initStatics t pt = ([], [])
1167 freeArgNames (Bind n (Pi ty) sc)
1168 = nub $ freeArgNames ty
1169 freeArgNames tm = let (_, args) = unApply tm in
1170 concatMap freeNames args
1172 -- if a name appears in a type class or tactic implicit index, it doesn't
1173 -- affect its 'uniquely inferrable' from a static status since these are
1174 -- resolved by searching.
1175 searchArg (Constraint _ _) = True
1176 searchArg (TacImp _ _ _) = True
1177 searchArg _ = False
1179 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
1180 staticList _ _ = []
1182-- Dealing with implicit arguments
1184-- Add constraint bindings from using block
1186addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
1187addUsingConstraints syn fc t
1188 = do ist <- get
1189 let ns = namesIn [] ist t
1190 let cs = getConstraints t -- check declared constraints
1191 let addconsts = uconsts \\ cs
1192 -- if all names in the arguments of addconsts appear in ns,
1193 -- add the constraint implicitly
1194 return (doAdd addconsts ns t)
1195 where uconsts = filter uconst (using syn)
1196 uconst (UConstraint _ _) = True
1197 uconst _ = False
1199 doAdd [] _ t = t
1200 -- if all of args in ns, then add it
1201 doAdd (UConstraint c args : cs) ns t
1202 | all (\n -> elem n ns) args
1203 = PPi (Constraint [] Dynamic) (sMN 0 "cu")
1204 (mkConst c args) (doAdd cs ns t)
1205 | otherwise = doAdd cs ns t
1207 mkConst c args = PApp fc (PRef fc c)
1208 (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc n)) args)
1210 getConstraints (PPi (Constraint _ _) _ c sc)
1211 = getcapp c ++ getConstraints sc
1212 getConstraints (PPi _ _ c sc) = getConstraints sc
1213 getConstraints _ = []
1215 getcapp (PApp _ (PRef _ c) args)
1216 = do ns <- mapM getName args
1217 return (UConstraint c ns)
1218 getcapp _ = []
1220 getName (PExp _ _ _ (PRef _ n)) = return n
1221 getName _ = []
1223-- Add implicit Pi bindings for any names in the term which appear in an
1224-- argument position.
1226-- This has become a right mess already. Better redo it some time...
1228implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
1229implicit info syn n ptm = implicit' info syn [] n ptm
1231implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
1232implicit' info syn ignore n ptm
1233 = do i <- getIState
1234 let (tm', impdata) = implicitise syn ignore i ptm
1235 defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
1236-- let (tm'', spos) = findStatics i tm'
1237 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1238 addIBC (IBCImp n)
1239 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1240-- i <- get
1241-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1242 return tm'
1243 where
1244 -- Detect unknown names in default arguments and throw error if found.
1245 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1246 defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
1248 notFoundInDefault :: [Name] -> PArg -> Idris [Name]
1249 notFoundInDefault kns (PTacImplicit _ _ n script _)
1250 = do i <- getIState
1251 case notFound kns (namesIn [] i script) of
1252 Nothing -> return (n:kns)
1253 Just name -> throwError (NoSuchVariable name)
1254 notFoundInDefault kns p = return ((pname p):kns)
1256 notFound :: [Name] -> [Name] -> Maybe Name
1257 notFound kns [] = Nothing
1258 notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
1259 notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
1261implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1262implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1263 let (declimps, ns') = execState (imps True [] tm) ([], [])
1264 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1265 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1266 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1267 if null ns
1268 then (tm, reverse declimps)
1269 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1270 where
1271 uvars = map ipair (filter uimplicit (using syn))
1272 pvars = syn_params syn
1274 inUsing n = n `elem` map fst uvars
1276 ipair (UImplicit x y) = (x, y)
1277 uimplicit (UImplicit _ _) = True
1278 uimplicit _ = False
1280 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1281 | otherwise = x : dropAll xs ys
1282 dropAll [] ys = []
1284 -- Find names in argument position in a type, suitable for implicit
1285 -- binding
1286 -- Not the function position, but do everything else...
1287 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1288 implNamesIn uv t = namesIn uv ist t
1290 imps top env (PApp _ f as)
1291 = do (decls, ns) <- get
1292 let isn = concatMap (namesIn uvars ist) (map getTm as)
1293 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1294 imps top env (PPi (Imp l _ _) n ty sc)
1295 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1296 (decls , ns) <- get
1297 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1298 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1299 imps True (n:env) sc
1300 imps top env (PPi (Exp l _ _) n ty sc)
1301 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1302 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1303 _ -> [])
1304 (decls, ns) <- get -- ignore decls in HO types
1305 put (PExp (getPriority ist ty) 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 (Constraint 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 (PConstraint 10 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 (TacImp l _ scr) 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 (PTacImplicit 10 l n scr Placeholder : decls,
1322 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1323 imps True (n:env) sc
1324 imps top env (PEq _ l r)
1325 = do (decls, ns) <- get
1326 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1327 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1328 imps top env (PRewrite _ l r _)
1329 = do (decls, ns) <- get
1330 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1331 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1332 imps top env (PTyped l r)
1333 = imps top env l
1334 imps top env (PPair _ _ l r)
1335 = do (decls, ns) <- get
1336 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1337 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1338 imps top env (PDPair _ _ (PRef _ n) t r)
1339 = do (decls, ns) <- get
1340 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1341 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1342 imps top env (PDPair _ _ l t r)
1343 = do (decls, ns) <- get
1344 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1345 namesIn uvars ist r
1346 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1347 imps top env (PAlternative a as)
1348 = do (decls, ns) <- get
1349 let isn = concatMap (namesIn uvars ist) as
1350 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1351 imps top env (PLam n ty sc)
1352 = do imps False env ty
1353 imps False (n:env) sc
1354 imps top env (PHidden tm) = imps False env tm
1355 imps top env (PUnifyLog tm) = imps False env tm
1356 imps top env (PNoImplicits tm) = imps False env tm
1357 imps top env _ = return ()
1359 pibind using [] sc = sc
1360 pibind using (n:ns) sc
1361 = case lookup n using of
1362 Just ty -> PPi (Imp [] Dynamic False) n ty (pibind using ns sc)
1363 Nothing -> PPi (Imp [] Dynamic False) n Placeholder
1364 (pibind using ns sc)
1366-- Add implicit arguments in function calls
1367addImplPat :: IState -> PTerm -> PTerm
1368addImplPat = addImpl' True [] []
1370addImplBound :: IState -> [Name] -> PTerm -> PTerm
1371addImplBound ist ns = addImpl' False ns [] ist
1373addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1374addImplBoundInf ist ns inf = addImpl' False ns inf ist
1376addImpl :: IState -> PTerm -> PTerm
1377addImpl = addImpl' False [] []
1379-- TODO: in patterns, don't add implicits to function names guarded by constructors
1380-- and *not* inside a PHidden
1382addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1383addImpl' inpat env infns ist ptm
1384 = mkUniqueNames env (ai (zip env (repeat Nothing)) [] ptm)
1385 where
1386 ai env ds (PRef fc f)
1387 | f `elem` infns = PInferRef fc f
1388 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f ds []
1389 ai env ds (PHidden (PRef fc f))
1390 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f ds []
1391 ai env ds (PEq fc l r)
1392 = let l' = ai env ds l
1393 r' = ai env ds r in
1394 PEq fc l' r'
1395 ai env ds (PRewrite fc l r g)
1396 = let l' = ai env ds l
1397 r' = ai env ds r
1398 g' = fmap (ai env ds) g in
1399 PRewrite fc l' r' g'
1400 ai env ds (PTyped l r)
1401 = let l' = ai env ds l
1402 r' = ai env ds r in
1403 PTyped l' r'
1404 ai env ds (PPair fc p l r)
1405 = let l' = ai env ds l
1406 r' = ai env ds r in
1407 PPair fc p l' r'
1408 ai env ds (PDPair fc p l t r)
1409 = let l' = ai env ds l
1410 t' = ai env ds t
1411 r' = ai env ds r in
1412 PDPair fc p l' t' r'
1413 ai env ds (PAlternative a as)
1414 = let as' = map (ai env ds) as in
1415 PAlternative a as'
1416 ai env _ (PDisamb ds' as) = ai env ds' as
1417 ai env ds (PApp fc (PInferRef _ f) as)
1418 = let as' = map (fmap (ai env ds)) as in
1419 PApp fc (PInferRef fc f) as'
1420 ai env ds (PApp fc ftm@(PRef _ f) as)
1421 | f `elem` infns = ai env ds (PApp fc (PInferRef fc f) as)
1422 | not (f `elem` map fst env) -- notelocal
1423 = let as' = map (fmap (ai env ds)) as in
1424 handleErr $ aiFn inpat False ist fc f ds as'
1425 | Just (Just ty) <- lookup f env =
1426 let as' = map (fmap (ai env ds)) as
1427 arity = getPArity ty in
1428 mkPApp fc arity ftm as'
1429 ai env ds (PApp fc f as)
1430 = let f' = ai env ds f
1431 as' = map (fmap (ai env ds)) as in
1432 mkPApp fc 1 f' as'
1433 ai env ds (PCase fc c os)
1434 = let c' = ai env ds c
1435 os' = map (pmap (ai env ds)) os in
1436 PCase fc c' os'
1437 ai env ds (PLam n ty sc)
1438 = let ty' = ai env ds ty
1439 sc' = ai ((n, Just ty):env) ds sc in
1440 PLam n ty' sc'
1441 ai env ds (PLet n ty val sc)
1442 = let ty' = ai env ds ty
1443 val' = ai env ds val
1444 sc' = ai ((n, Just ty):env) ds sc in
1445 PLet n ty' val' sc'
1446 ai env ds (PPi p n ty sc)
1447 = let ty' = ai env ds ty
1448 sc' = ai ((n, Just ty):env) ds sc in
1449 PPi p n ty' sc'
1450 ai env ds (PGoal fc r n sc)
1451 = let r' = ai env ds r
1452 sc' = ai ((n, Nothing):env) ds sc in
1453 PGoal fc r' n sc'
1454 ai env ds (PHidden tm) = PHidden (ai env ds tm)
1455 ai env ds (PProof ts) = PProof (map (fmap (ai env ds)) ts)
1456 ai env ds (PTactics ts) = PTactics (map (fmap (ai env ds)) ts)
1457 ai env ds (PRefl fc tm) = PRefl fc (ai env ds tm)
1458 ai env ds (PUnifyLog tm) = PUnifyLog (ai env ds tm)
1459 ai env ds (PNoImplicits tm) = PNoImplicits (ai env ds tm)
1460 ai env ds tm = tm
1462 handleErr (Left err) = PElabError err
1463 handleErr (Right x) = x
1465-- if in a pattern, and there are no arguments, and there's no possible
1466-- names with zero explicit arguments, don't add implicits.
1468aiFn :: Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1469aiFn inpat True ist fc f ds []
1470 = case lookupDef f (tt_ctxt ist) of
1471 [] -> Right $ PPatvar fc f
1472 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1473 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1474 if (not (vname f) || tcname f
1475 || any (conCaf (tt_ctxt ist)) ialts)
1476-- any constructor alts || any allImp ialts))
1477 then aiFn inpat False ist fc f ds [] -- use it as a constructor
1478 else Right $ PPatvar fc f
1479 where imp (PExp _ _ _ _) = False
1480 imp _ = True
1481-- allImp [] = False
1482 allImp xs = all imp xs
1483 constructor (TyDecl (DCon _ _) _) = True
1484 constructor _ = False
1486 conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
1488 vname (UN n) = True -- non qualified
1489 vname _ = False
1491aiFn inpat expat ist fc f ds as
1492 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1493aiFn inpat expat ist fc f ds as
1494 -- This is where namespaces get resolved by adding PAlternative
1495 = do let ns = lookupCtxtName f (idris_implicits ist)
1496 let nh = filter (\(n, _) -> notHidden n) ns
1497 let ns' = case trimAlts ds nh of
1498 [] -> nh
1499 x -> x
1500 case ns' of
1501 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1502 [] -> if f `elem` (map fst (idris_metavars ist))
1503 then Right $ PApp fc (PRef fc f) as
1504 else Right $ mkPApp fc (length as) (PRef fc f) as
1505 alts -> Right $
1506 PAlternative True $
1507 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1508 (insertImpl ns as)) alts
1509 where
1510 trimAlts [] alts = alts
1511 trimAlts ns alts
1512 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1514 nspace (NS _ s) = s
1515 nspace _ = []
1517 notHidden n = case getAccessibility n of
1518 Hidden -> False
1519 _ -> True
1521 getAccessibility n
1522 = case lookupDefAcc n False (tt_ctxt ist) of
1523 [(n,t)] -> t
1524 _ -> Public
1526 insertImpl :: [PArg] -> [PArg] -> [PArg]
1527 insertImpl ps as = insImpAcc M.empty ps as
1529 -- TODO WIP substitution into default arg expressions.
1530 -- - An extra accumulator parameter here?
1531 -- - Accumulator of what?
1532 -- - Map of param names and their corresponding arg terms?
1533 -- - Perhaps in an 'inner' function, though?
1534 -- - Though OTOH perhaps this one should become the inner
1535 -- function?
1536 -- - Check for existing call sites of insertImpl.
1537 -- - Well, easy: this is in a where block :-).
1538 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1539 -> [PArg] -- parameters
1540 -> [PArg] -- arguments
1541 -> [PArg]
1542 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) =
1543 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given
1544 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) =
1545 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given
1546 insImpAcc pnas (PConstraint p l n ty : ps) given =
1547 let rtc = PResolveTC fc in
1548 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given
1549 insImpAcc pnas (PImp p _ l n ty : ps) given =
1550 case find n given [] of
1551 Just (tm, given') ->
1552 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given'
1553 Nothing ->
1554 PImp p True l n Placeholder :
1555 insImpAcc (M.insert n Placeholder pnas) ps given
1556 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given =
1557 let sc = addImpl ist (substMatches (M.toList pnas) sc') in
1558 case find n given [] of
1559 Just (tm, given') ->
1560 PTacImplicit p l n sc tm :
1561 insImpAcc (M.insert n tm pnas) ps given'
1562 Nothing ->
1563 if inpat
1564 then PTacImplicit p l n sc Placeholder :
1565 insImpAcc (M.insert n Placeholder pnas) ps given
1566 else PTacImplicit p l n sc sc :
1567 insImpAcc (M.insert n sc pnas) ps given
1568 insImpAcc _ expected [] = []
1569 insImpAcc _ _ given = given
1571 find n [] acc = Nothing
1572 find n (PImp _ _ _ n' t : gs) acc
1573 | n == n' = Just (t, reverse acc ++ gs)
1574 find n (PTacImplicit _ _ n' _ t : gs) acc
1575 | n == n' = Just (t, reverse acc ++ gs)
1576 find n (g : gs) acc = find n gs (g : acc)
1578-- replace non-linear occurrences with _
1579-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1580-- it is hard to get right!
1582stripLinear :: IState -> PTerm -> PTerm
1583stripLinear i tm = evalState (sl tm) [] where
1584 sl :: PTerm -> State [Name] PTerm
1585 sl (PRef fc f)
1586 | (_:_) <- lookupTy f (tt_ctxt i)
1587 = return $ PRef fc f
1588 | otherwise = do ns <- get
1589 if (f `elem` ns)
1590 then return Placeholder
1591 else do put (f : ns)
1592 return (PRef fc f)
1593 sl (PPatvar fc f)
1594 = do ns <- get
1595 if (f `elem` ns)
1596 then return Placeholder
1597 else do put (f : ns)
1598 return (PPatvar fc f)
1599 sl t@(PAlternative _ (a : as)) = do sl a
1600 return t
1601 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1602 args' <- mapM slA args
1603 return $ PApp fc fn args'
1604 where slA (PImp p m l n t) = do t' <- sl t
1605 return $ PImp p m l n t'
1606 slA (PExp p l n t) = do t' <- sl t
1607 return $ PExp p l n t'
1608 slA (PConstraint p l n t)
1609 = do t' <- sl t
1610 return $ PConstraint p l n t'
1611 slA (PTacImplicit p l n sc t)
1612 = do t' <- sl t
1613 return $ PTacImplicit p l n sc t'
1614 sl x = return x
1616-- Remove functions which aren't applied to anything, which must then
1617-- be resolved by unification. Assume names resolved and alternatives
1618-- filled in (so no ambiguity).
1620stripUnmatchable :: IState -> PTerm -> PTerm
1621stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1622 su :: PTerm -> PTerm
1623 su (PRef fc f)
1624 | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1625 = Placeholder
1626 su (PApp fc fn args)
1627 = PApp fc fn (fmap (fmap su) args)
1628 su (PAlternative b alts)
1629 = let alts' = filter (/= Placeholder) (map su alts) in
1630 if null alts' then Placeholder
1631 else PAlternative b alts'
1632 su (PPair fc p l r) = PPair fc p (su l) (su r)
1633 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1634 su t = t
1635stripUnmatchable i tm = tm
1637mkPApp fc a f [] = f
1638mkPApp fc a f as = let rest = drop a as in
1639 appRest fc (PApp fc f (take a as)) rest
1640 where
1641 appRest fc f [] = f
1642 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1644-- Find 'static' argument positions
1645-- (the declared ones, plus any names in argument position in the declared
1646-- statics)
1647-- FIXME: It's possible that this really has to happen after elaboration
1649findStatics :: IState -> PTerm -> (PTerm, [Bool])
1650findStatics ist tm = trace (show tm) $
1651 let (ns, ss) = fs tm in
1652 runState (pos ns ss tm) []
1653 where fs (PPi p n t sc)
1654 | Static <- pstatic p
1655 = let (ns, ss) = fs sc in
1656 (namesIn [] ist t : ns, n : ss)
1657 | otherwise = let (ns, ss) = fs sc in
1658 (ns, ss)
1659 fs _ = ([], [])
1661 inOne n ns = length (filter id (map (elem n) ns)) == 1
1663 pos ns ss (PPi p n t sc)
1664 | elem n ss = do sc' <- pos ns ss sc
1665 spos <- get
1666 put (True : spos)
1667 return (PPi (p { pstatic = Static }) n t sc')
1668 | otherwise = do sc' <- pos ns ss sc
1669 spos <- get
1670 put (False : spos)
1671 return (PPi p n t sc')
1672 pos ns ss t = return t
1674-- for 6.12/7 compatibility
1675data EitherErr a b = LeftErr a | RightOK b
1677instance Monad (EitherErr a) where
1678 return = RightOK
1680 (LeftErr e) >>= k = LeftErr e
1681 RightOK v >>= k = k v
1683toEither (LeftErr e) = Left e
1684toEither (RightOK ho) = Right ho
1686-- syntactic match of a against b, returning pair of variables in a
1687-- and what they match. Returns the pair that failed if not a match.
1689matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1690matchClause = matchClause' False
1692matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1693matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1694 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1696 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1697 fullApp x = x
1699 match' x y = match (fullApp x) (fullApp y)
1700 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1701 | fi == txt "fromInteger" && b == txt "builtins",
1702 PConstant (I _) <- getTm x = match (getTm x) x'
1703 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1704 | fi == txt "fromInteger" && b == txt "builtins",
1705 PConstant (I _) <- getTm x = match (getTm x) x'
1706 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1707 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1708 match (PApp _ f args) (PApp _ f' args')
1709 | length args == length args'
1710 = do mf <- match' f f'
1711 ms <- zipWithM matchArg args args'
1712 return (mf ++ concat ms)
1713-- match (PRef _ n) (PRef _ n') | n == n' = return []
1714-- | otherwise = Nothing
1715 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1716 match (PPatvar f n) xr = match (PRef f n) xr
1717 match xr (PPatvar f n) = match xr (PRef f n)
1718 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1719 match (PRef _ n) tm@(PRef _ n')
1720 | n == n' && not names &&
1721 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1722 || tm == Placeholder)
1723 = return [(n, tm)]
1724 | n == n' = return []
1725 match (PRef _ n) tm
1726 | not names && (not (isConName n (tt_ctxt i) ||
1727 isFnName n (tt_ctxt i)) || tm == Placeholder)
1728 = return [(n, tm)]
1729 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1730 mr <- match' r r'
1731 return (ml ++ mr)
1732 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1733 = do ml <- match' l l'
1734 mr <- match' r r'
1735 return (ml ++ mr)
1736 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1737 mr <- match r r'
1738 return (ml ++ mr)
1739 match (PTyped l r) x = match l x
1740 match x (PTyped l r) = match x l
1741 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1742 mr <- match' r r'
1743 return (ml ++ mr)
1744 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1745 mt <- match' t t'
1746 mr <- match' r r'
1747 return (ml ++ mt ++ mr)
1748 match (PAlternative a as) (PAlternative a' as')
1749 = do ms <- zipWithM match' as as'
1750 return (concat ms)
1751 match a@(PAlternative _ as) b
1752 = do let ms = zipWith match' as (repeat b)
1753 case (rights (map toEither ms)) of
1754 (x: _) -> return x
1755 _ -> LeftErr (a, b)
1756 match (PCase _ _ _) _ = return [] -- lifted out
1757 match (PMetavar _) _ = return [] -- modified
1758 match (PInferRef _ _) _ = return [] -- modified
1759 match (PQuote _) _ = return []
1760 match (PProof _) _ = return []
1761 match (PTactics _) _ = return []
1762 match (PRefl _ _) (PRefl _ _) = return []
1763 match (PResolveTC _) (PResolveTC _) = return []
1764 match (PTrue _ _) (PTrue _ _) = return []
1765 match (PFalse _) (PFalse _) = return []
1766 match (PReturn _) (PReturn _) = return []
1767 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1768 ms <- match' s s'
1769 return (mt ++ ms)
1770 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1771 ms <- match' s s'
1772 return (mt ++ ms)
1773 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1774 mty <- match' ty ty'
1775 ms <- match' s s'
1776 return (mt ++ mty ++ ms)
1777 match (PHidden x) (PHidden y) = match' x y
1778 match (PUnifyLog x) y = match' x y
1779 match x (PUnifyLog y) = match' x y
1780 match (PNoImplicits x) y = match' x y
1781 match x (PNoImplicits y) = match' x y
1782 match Placeholder _ = return []
1783 match _ Placeholder = return []
1784 match (PResolveTC _) _ = return []
1785 match a b | a == b = return []
1786 | otherwise = LeftErr (a, b)
1788 checkRpts (RightOK ms) = check ms where
1789 check ((n,t):xs)
1790 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1791 then Left (t, t')
1792 else check xs
1793 check (_:xs) = check xs
1794 check [] = Right ms
1795 checkRpts (LeftErr x) = Left x
1797substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1798substMatches ms = substMatchesShadow ms []
1800substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1801substMatchesShadow [] shs t = t
1802substMatchesShadow ((n,tm):ns) shs t
1803 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1805substMatch :: Name -> PTerm -> PTerm -> PTerm
1806substMatch n = substMatchShadow n []
1808substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1809substMatchShadow n shs tm t = sm shs t where
1810 sm xs (PRef _ n') | n == n' = tm
1811 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1812 sm xs (PPi p x t sc)
1813 | x `elem` xs
1814 = let x' = nextName x in
1815 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1816 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1817 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1818 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1819 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1820 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1821 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1822 (fmap (sm xs) tm)
1823 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1824 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
1825 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
1826 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1827 sm xs (PHidden x) = PHidden (sm xs x)
1828 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1829 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1830 sm xs x = x
1832 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1833 fullApp x = x
1835shadow :: Name -> Name -> PTerm -> PTerm
1836shadow n n' t = sm t where
1837 sm (PRef fc x) | n == x = PRef fc n'
1838 sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)
1839 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1840 sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)
1841 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1842 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1843 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1844 sm (PEq f x y) = PEq f (sm x) (sm y)
1845 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1846 sm (PTyped x y) = PTyped (sm x) (sm y)
1847 sm (PPair f p x y) = PPair f p (sm x) (sm y)
1848 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
1849 sm (PAlternative a as) = PAlternative a (map sm as)
1850 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1851 sm (PProof ts) = PProof (map (fmap sm) ts)
1852 sm (PHidden x) = PHidden (sm x)
1853 sm (PUnifyLog x) = PUnifyLog (sm x)
1854 sm (PNoImplicits x) = PNoImplicits (sm x)
1855 sm x = x
1857-- Rename any binders which are repeated (so that we don't have to mess
1858-- about with shadowing anywhere else).
1860mkUniqueNames :: [Name] -> PTerm -> PTerm
1861mkUniqueNames env tm = evalState (mkUniq tm) env where
1862 inScope = boundNamesIn tm
1864 mkUniqA arg = do t' <- mkUniq (getTm arg)
1865 return (arg { getTm = t' })
1867 -- FIXME: Probably ought to do this for completeness! It's fine as
1868 -- long as there are no bindings inside tactics though.
1869 mkUniqT tac = return tac
1871 mkUniq :: PTerm -> State [Name] PTerm
1872 mkUniq (PLam n ty sc)
1873 = do env <- get
1874 (n', sc') <-
1875 if n `elem` env
1876 then do let n' = uniqueName n (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 n (env ++ inScope)
1888 return (n', shadow n n' sc)
1889 else return (n, sc)
1890 put (n' : env)
1891 ty' <- mkUniq ty
1892 sc'' <- mkUniq sc'
1893 return $! PPi p n' ty' sc''
1894 mkUniq (PLet n ty val sc)
1895 = do env <- get
1896 (n', sc') <-
1897 if n `elem` env
1898 then do let n' = uniqueName n (env ++ inScope)
1899 return (n', shadow n n' sc)
1900 else return (n, sc)
1901 put (n' : env)
1902 ty' <- mkUniq ty; val' <- mkUniq val
1903 sc'' <- mkUniq sc'
1904 return $! PLet n' ty' val' sc''
1905 mkUniq (PApp fc t args)
1906 = do t' <- mkUniq t
1907 args' <- mapM mkUniqA args
1908 return $! PApp fc t' args'
1909 mkUniq (PAppBind fc t args)
1910 = do t' <- mkUniq t
1911 args' <- mapM mkUniqA args
1912 return $! PAppBind fc t' args'
1913 mkUniq (PCase fc t alts)
1914 = do t' <- mkUniq t
1915 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
1916 return (x', y')) alts
1917 return $! PCase fc t' alts'
1918 mkUniq (PPair fc p l r)
1919 = do l' <- mkUniq l; r' <- mkUniq r
1920 return $! PPair fc p l' r'
1921 mkUniq (PDPair fc p (PRef fc' n) t sc)
1922 | t /= Placeholder
1923 = do env <- get
1924 (n', sc') <- if n `elem` env
1925 then do let n' = uniqueName n (env ++ inScope)
1926 return (n', shadow n n' sc)
1927 else return (n, sc)
1928 put (n' : env)
1929 t' <- mkUniq t
1930 sc'' <- mkUniq sc'
1931 return $! PDPair fc p (PRef fc' n') t' sc''
1932 mkUniq (PDPair fc p l t r)
1933 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
1934 return $! PDPair fc p l' t' r'
1935 mkUniq (PAlternative b as)
1936 = liftM (PAlternative b) (mapM mkUniq as)
1937 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
1938 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
1939 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
1940 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
1941 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
1942 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
1943 mkUniq t = return t