git.iko.soy/Idris-dev
on d3eb486 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1944 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 -- TODO WIP check impdata for unknown vars in default args
1236 defaultArgCheck (eInfoNames info ++ keys (idris_implicits i)) impdata
1237-- let (tm'', spos) = findStatics i tm'
1238 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
1239 addIBC (IBCImp n)
1240 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
1241-- i <- get
1242-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
1243 return tm'
1244 where
1245 -- Detect unknown names in default arguments and throw error if found.
1246 defaultArgCheck :: [Name] -> [PArg] -> Idris ()
1247 defaultArgCheck names params = foldM_ names params unknownInDefault
1249 unknownInDefault :: [Name] -> PArg -> Idris [Name]
1250 unknownInDefault ns (PTacImplicit _ _ n script _)
1251 = case notFound (namesIn script) ns of
1252 Nothing -> return (n:ns)
1253 Just name -> throwError (NoSuchVariable name)
1254 -- TODO See if PConstraint in addition to PExp can reasonably have
1255 -- a name. Until then, 'pname p' worksn't.
1256 unknownInDefault ns p = return (pname p):ns
1258 unknown :: [Name] -> [Name] -> Maybe Name
1259 unknown [] _ = Nothing
1260 unknown (SN (WhereN _ _ _)):as bs = unknown as bs
1261 unknown a:as bs = if elem a bs then unknown as bs else Just a
1263implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1264implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1265 let (declimps, ns') = execState (imps True [] tm) ([], [])
1266 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1267 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1268 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1269 if null ns
1270 then (tm, reverse declimps)
1271 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1272 where
1273 uvars = map ipair (filter uimplicit (using syn))
1274 pvars = syn_params syn
1276 inUsing n = n `elem` map fst uvars
1278 ipair (UImplicit x y) = (x, y)
1279 uimplicit (UImplicit _ _) = True
1280 uimplicit _ = False
1282 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1283 | otherwise = x : dropAll xs ys
1284 dropAll [] ys = []
1286 -- Find names in argument position in a type, suitable for implicit
1287 -- binding
1288 -- Not the function position, but do everything else...
1289 implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args)
1290 implNamesIn uv t = namesIn uv ist t
1292 imps top env (PApp _ f as)
1293 = do (decls, ns) <- get
1294 let isn = concatMap (namesIn uvars ist) (map getTm as)
1295 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1296 imps top env (PPi (Imp l _ _) n ty sc)
1297 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
1298 (decls , ns) <- get
1299 put (PImp (getPriority ist ty) True l n Placeholder : decls,
1300 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1301 imps True (n:env) sc
1302 imps top env (PPi (Exp l _ _) n ty sc)
1303 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1304 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1305 _ -> [])
1306 (decls, ns) <- get -- ignore decls in HO types
1307 put (PExp (getPriority ist ty) l n Placeholder : decls,
1308 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1309 imps True (n:env) sc
1310 imps top env (PPi (Constraint l _) n ty sc)
1311 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1312 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1313 _ -> [])
1314 (decls, ns) <- get -- ignore decls in HO types
1315 put (PConstraint 10 l n Placeholder : decls,
1316 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1317 imps True (n:env) sc
1318 imps top env (PPi (TacImp l _ scr) n ty sc)
1319 = do let isn = nub (implNamesIn uvars ty ++ case sc of
1320 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1321 _ -> [])
1322 (decls, ns) <- get -- ignore decls in HO types
1323 put (PTacImplicit 10 l n scr Placeholder : decls,
1324 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1325 imps True (n:env) sc
1326 imps top env (PEq _ l r)
1327 = do (decls, ns) <- get
1328 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1329 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1330 imps top env (PRewrite _ l r _)
1331 = do (decls, ns) <- get
1332 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1333 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1334 imps top env (PTyped l r)
1335 = imps top env l
1336 imps top env (PPair _ _ l r)
1337 = do (decls, ns) <- get
1338 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1339 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1340 imps top env (PDPair _ _ (PRef _ n) t r)
1341 = do (decls, ns) <- get
1342 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1343 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1344 imps top env (PDPair _ _ l t r)
1345 = do (decls, ns) <- get
1346 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1347 namesIn uvars ist r
1348 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1349 imps top env (PAlternative a as)
1350 = do (decls, ns) <- get
1351 let isn = concatMap (namesIn uvars ist) as
1352 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1353 imps top env (PLam n ty sc)
1354 = do imps False env ty
1355 imps False (n:env) sc
1356 imps top env (PHidden tm) = imps False env tm
1357 imps top env (PUnifyLog tm) = imps False env tm
1358 imps top env (PNoImplicits tm) = imps False env tm
1359 imps top env _ = return ()
1361 pibind using [] sc = sc
1362 pibind using (n:ns) sc
1363 = case lookup n using of
1364 Just ty -> PPi (Imp [] Dynamic False) n ty (pibind using ns sc)
1365 Nothing -> PPi (Imp [] Dynamic False) n Placeholder
1366 (pibind using ns sc)
1368-- Add implicit arguments in function calls
1369addImplPat :: IState -> PTerm -> PTerm
1370addImplPat = addImpl' True [] []
1372addImplBound :: IState -> [Name] -> PTerm -> PTerm
1373addImplBound ist ns = addImpl' False ns [] ist
1375addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1376addImplBoundInf ist ns inf = addImpl' False ns inf ist
1378addImpl :: IState -> PTerm -> PTerm
1379addImpl = addImpl' False [] []
1381-- TODO: in patterns, don't add implicits to function names guarded by constructors
1382-- and *not* inside a PHidden
1384addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1385addImpl' inpat env infns ist ptm
1386 = mkUniqueNames env (ai (zip env (repeat Nothing)) [] ptm)
1387 where
1388 ai env ds (PRef fc f)
1389 | f `elem` infns = PInferRef fc f
1390 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f ds []
1391 ai env ds (PHidden (PRef fc f))
1392 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f ds []
1393 ai env ds (PEq fc l r)
1394 = let l' = ai env ds l
1395 r' = ai env ds r in
1396 PEq fc l' r'
1397 ai env ds (PRewrite fc l r g)
1398 = let l' = ai env ds l
1399 r' = ai env ds r
1400 g' = fmap (ai env ds) g in
1401 PRewrite fc l' r' g'
1402 ai env ds (PTyped l r)
1403 = let l' = ai env ds l
1404 r' = ai env ds r in
1405 PTyped l' r'
1406 ai env ds (PPair fc p l r)
1407 = let l' = ai env ds l
1408 r' = ai env ds r in
1409 PPair fc p l' r'
1410 ai env ds (PDPair fc p l t r)
1411 = let l' = ai env ds l
1412 t' = ai env ds t
1413 r' = ai env ds r in
1414 PDPair fc p l' t' r'
1415 ai env ds (PAlternative a as)
1416 = let as' = map (ai env ds) as in
1417 PAlternative a as'
1418 ai env _ (PDisamb ds' as) = ai env ds' as
1419 ai env ds (PApp fc (PInferRef _ f) as)
1420 = let as' = map (fmap (ai env ds)) as in
1421 PApp fc (PInferRef fc f) as'
1422 ai env ds (PApp fc ftm@(PRef _ f) as)
1423 | f `elem` infns = ai env ds (PApp fc (PInferRef fc f) as)
1424 | not (f `elem` map fst env) -- notelocal
1425 = let as' = map (fmap (ai env ds)) as in
1426 handleErr $ aiFn inpat False ist fc f ds as'
1427 | Just (Just ty) <- lookup f env =
1428 let as' = map (fmap (ai env ds)) as
1429 arity = getPArity ty in
1430 mkPApp fc arity ftm as'
1431 ai env ds (PApp fc f as)
1432 = let f' = ai env ds f
1433 as' = map (fmap (ai env ds)) as in
1434 mkPApp fc 1 f' as'
1435 ai env ds (PCase fc c os)
1436 = let c' = ai env ds c
1437 os' = map (pmap (ai env ds)) os in
1438 PCase fc c' os'
1439 ai env ds (PLam n ty sc)
1440 = let ty' = ai env ds ty
1441 sc' = ai ((n, Just ty):env) ds sc in
1442 PLam n ty' sc'
1443 ai env ds (PLet n ty val sc)
1444 = let ty' = ai env ds ty
1445 val' = ai env ds val
1446 sc' = ai ((n, Just ty):env) ds sc in
1447 PLet n ty' val' sc'
1448 ai env ds (PPi p n ty sc)
1449 = let ty' = ai env ds ty
1450 sc' = ai ((n, Just ty):env) ds sc in
1451 PPi p n ty' sc'
1452 ai env ds (PGoal fc r n sc)
1453 = let r' = ai env ds r
1454 sc' = ai ((n, Nothing):env) ds sc in
1455 PGoal fc r' n sc'
1456 ai env ds (PHidden tm) = PHidden (ai env ds tm)
1457 ai env ds (PProof ts) = PProof (map (fmap (ai env ds)) ts)
1458 ai env ds (PTactics ts) = PTactics (map (fmap (ai env ds)) ts)
1459 ai env ds (PRefl fc tm) = PRefl fc (ai env ds tm)
1460 ai env ds (PUnifyLog tm) = PUnifyLog (ai env ds tm)
1461 ai env ds (PNoImplicits tm) = PNoImplicits (ai env ds tm)
1462 ai env ds tm = tm
1464 handleErr (Left err) = PElabError err
1465 handleErr (Right x) = x
1467-- if in a pattern, and there are no arguments, and there's no possible
1468-- names with zero explicit arguments, don't add implicits.
1470aiFn :: Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1471aiFn inpat True ist fc f ds []
1472 = case lookupDef f (tt_ctxt ist) of
1473 [] -> Right $ PPatvar fc f
1474 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1475 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1476 if (not (vname f) || tcname f
1477 || any (conCaf (tt_ctxt ist)) ialts)
1478-- any constructor alts || any allImp ialts))
1479 then aiFn inpat False ist fc f ds [] -- use it as a constructor
1480 else Right $ PPatvar fc f
1481 where imp (PExp _ _ _ _) = False
1482 imp _ = True
1483-- allImp [] = False
1484 allImp xs = all imp xs
1485 constructor (TyDecl (DCon _ _) _) = True
1486 constructor _ = False
1488 conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
1490 vname (UN n) = True -- non qualified
1491 vname _ = False
1493aiFn inpat expat ist fc f ds as
1494 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1495aiFn inpat expat ist fc f ds as
1496 -- This is where namespaces get resolved by adding PAlternative
1497 = do let ns = lookupCtxtName f (idris_implicits ist)
1498 let nh = filter (\(n, _) -> notHidden n) ns
1499 let ns' = case trimAlts ds nh of
1500 [] -> nh
1501 x -> x
1502 case ns' of
1503 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1504 [] -> if f `elem` (map fst (idris_metavars ist))
1505 then Right $ PApp fc (PRef fc f) as
1506 else Right $ mkPApp fc (length as) (PRef fc f) as
1507 alts -> Right $
1508 PAlternative True $
1509 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1510 (insertImpl ns as)) alts
1511 where
1512 trimAlts [] alts = alts
1513 trimAlts ns alts
1514 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1516 nspace (NS _ s) = s
1517 nspace _ = []
1519 notHidden n = case getAccessibility n of
1520 Hidden -> False
1521 _ -> True
1523 getAccessibility n
1524 = case lookupDefAcc n False (tt_ctxt ist) of
1525 [(n,t)] -> t
1526 _ -> Public
1528 -- TODO WIP substitution into default arg expressions.
1529 -- - An extra accumulator parameter here?
1530 -- - Accumulator of what?
1531 -- - Map of param names and their corresponding arg terms?
1532 -- - Perhaps in an 'inner' function, though?
1533 -- - Though OTOH perhaps this one should become the inner
1534 -- function?
1535 -- - Check for existing call sites of insertImpl.
1536 -- - Well, easy: this is in a where block :-).
1537 insertImpl :: M.Map Name PTerm -- accumulated param names & arg terms
1538 -> [PArg] -- parameters
1539 -> [PArg] -- arguments
1540 -> [PArg]
1541 insertImpl pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) =
1542 PExp p l n tm : insertImpl (M.insert n tm pnas) ps given
1543 insertImpl pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) =
1544 PConstraint p l n tm : insertImpl (M.insert n tm pnas) ps given
1545 insertImpl pnas (PConstraint p l n ty : ps) given =
1546 let rtc = PResolveTC fc in
1547 PConstraint p l n rtc : insertImpl (M.insert n rtc pnas) ps given
1548 insertImpl pnas (PImp p _ l n ty : ps) given =
1549 case find n given [] of
1550 Just (tm, given') ->
1551 PImp p False l n tm : insertImpl (M.insert n tm pnas) ps given'
1552 Nothing ->
1553 PImp p True l n Placeholder :
1554 insertImpl (M.insert n Placeholder pnas) ps given
1555 insertImpl pnas (PTacImplicit p l n sc' ty : ps) given =
1556 let sc = addImpl ist (substMatches (toList pnas) sc') in
1557 case find n given [] of
1558 Just (tm, given') ->
1559 PTacImplicit p l n sc tm :
1560 insertImpl (M.insert n tm pnas) ps given'
1561 Nothing ->
1562 if inpat
1563 then PTacImplicit p l n sc Placeholder :
1564 insertImpl (M.insert n Placeholder pnas) ps given
1565 else PTacImplicit p l n sc sc :
1566 insertImpl (M.insert n sc pnas) ps given
1567 insertImpl expected [] = []
1568 insertImpl _ given = given
1570 find n [] acc = Nothing
1571 find n (PImp _ _ _ n' t : gs) acc
1572 | n == n' = Just (t, reverse acc ++ gs)
1573 find n (PTacImplicit _ _ n' _ t : gs) acc
1574 | n == n' = Just (t, reverse acc ++ gs)
1575 find n (g : gs) acc = find n gs (g : acc)
1577-- replace non-linear occurrences with _
1578-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1579-- it is hard to get right!
1581stripLinear :: IState -> PTerm -> PTerm
1582stripLinear i tm = evalState (sl tm) [] where
1583 sl :: PTerm -> State [Name] PTerm
1584 sl (PRef fc f)
1585 | (_:_) <- lookupTy f (tt_ctxt i)
1586 = return $ PRef fc f
1587 | otherwise = do ns <- get
1588 if (f `elem` ns)
1589 then return Placeholder
1590 else do put (f : ns)
1591 return (PRef fc f)
1592 sl (PPatvar fc f)
1593 = do ns <- get
1594 if (f `elem` ns)
1595 then return Placeholder
1596 else do put (f : ns)
1597 return (PPatvar fc f)
1598 sl t@(PAlternative _ (a : as)) = do sl a
1599 return t
1600 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1601 args' <- mapM slA args
1602 return $ PApp fc fn args'
1603 where slA (PImp p m l n t) = do t' <- sl t
1604 return $ PImp p m l n t'
1605 slA (PExp p l n t) = do t' <- sl t
1606 return $ PExp p l n t'
1607 slA (PConstraint p l n t)
1608 = do t' <- sl t
1609 return $ PConstraint p l n t'
1610 slA (PTacImplicit p l n sc t)
1611 = do t' <- sl t
1612 return $ PTacImplicit p l n sc t'
1613 sl x = return x
1615-- Remove functions which aren't applied to anything, which must then
1616-- be resolved by unification. Assume names resolved and alternatives
1617-- filled in (so no ambiguity).
1619stripUnmatchable :: IState -> PTerm -> PTerm
1620stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1621 su :: PTerm -> PTerm
1622 su (PRef fc f)
1623 | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1624 = Placeholder
1625 su (PApp fc fn args)
1626 = PApp fc fn (fmap (fmap su) args)
1627 su (PAlternative b alts)
1628 = let alts' = filter (/= Placeholder) (map su alts) in
1629 if null alts' then Placeholder
1630 else PAlternative b alts'
1631 su (PPair fc p l r) = PPair fc p (su l) (su r)
1632 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1633 su t = t
1634stripUnmatchable i tm = tm
1636mkPApp fc a f [] = f
1637mkPApp fc a f as = let rest = drop a as in
1638 appRest fc (PApp fc f (take a as)) rest
1639 where
1640 appRest fc f [] = f
1641 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1643-- Find 'static' argument positions
1644-- (the declared ones, plus any names in argument position in the declared
1645-- statics)
1646-- FIXME: It's possible that this really has to happen after elaboration
1648findStatics :: IState -> PTerm -> (PTerm, [Bool])
1649findStatics ist tm = trace (show tm) $
1650 let (ns, ss) = fs tm in
1651 runState (pos ns ss tm) []
1652 where fs (PPi p n t sc)
1653 | Static <- pstatic p
1654 = let (ns, ss) = fs sc in
1655 (namesIn [] ist t : ns, n : ss)
1656 | otherwise = let (ns, ss) = fs sc in
1657 (ns, ss)
1658 fs _ = ([], [])
1660 inOne n ns = length (filter id (map (elem n) ns)) == 1
1662 pos ns ss (PPi p n t sc)
1663 | elem n ss = do sc' <- pos ns ss sc
1664 spos <- get
1665 put (True : spos)
1666 return (PPi (p { pstatic = Static }) n t sc')
1667 | otherwise = do sc' <- pos ns ss sc
1668 spos <- get
1669 put (False : spos)
1670 return (PPi p n t sc')
1671 pos ns ss t = return t
1673-- for 6.12/7 compatibility
1674data EitherErr a b = LeftErr a | RightOK b
1676instance Monad (EitherErr a) where
1677 return = RightOK
1679 (LeftErr e) >>= k = LeftErr e
1680 RightOK v >>= k = k v
1682toEither (LeftErr e) = Left e
1683toEither (RightOK ho) = Right ho
1685-- syntactic match of a against b, returning pair of variables in a
1686-- and what they match. Returns the pair that failed if not a match.
1688matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1689matchClause = matchClause' False
1691matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1692matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1693 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1695 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1696 fullApp x = x
1698 match' x y = match (fullApp x) (fullApp y)
1699 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1700 | fi == txt "fromInteger" && b == txt "builtins",
1701 PConstant (I _) <- getTm x = match (getTm x) x'
1702 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1703 | fi == txt "fromInteger" && b == txt "builtins",
1704 PConstant (I _) <- getTm x = match (getTm x) x'
1705 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1706 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1707 match (PApp _ f args) (PApp _ f' args')
1708 | length args == length args'
1709 = do mf <- match' f f'
1710 ms <- zipWithM matchArg args args'
1711 return (mf ++ concat ms)
1712-- match (PRef _ n) (PRef _ n') | n == n' = return []
1713-- | otherwise = Nothing
1714 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1715 match (PPatvar f n) xr = match (PRef f n) xr
1716 match xr (PPatvar f n) = match xr (PRef f n)
1717 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1718 match (PRef _ n) tm@(PRef _ n')
1719 | n == n' && not names &&
1720 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1721 || tm == Placeholder)
1722 = return [(n, tm)]
1723 | n == n' = return []
1724 match (PRef _ n) tm
1725 | not names && (not (isConName n (tt_ctxt i) ||
1726 isFnName n (tt_ctxt i)) || tm == Placeholder)
1727 = return [(n, tm)]
1728 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1729 mr <- match' r r'
1730 return (ml ++ mr)
1731 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1732 = do ml <- match' l l'
1733 mr <- match' r r'
1734 return (ml ++ mr)
1735 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1736 mr <- match r r'
1737 return (ml ++ mr)
1738 match (PTyped l r) x = match l x
1739 match x (PTyped l r) = match x l
1740 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1741 mr <- match' r r'
1742 return (ml ++ mr)
1743 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1744 mt <- match' t t'
1745 mr <- match' r r'
1746 return (ml ++ mt ++ mr)
1747 match (PAlternative a as) (PAlternative a' as')
1748 = do ms <- zipWithM match' as as'
1749 return (concat ms)
1750 match a@(PAlternative _ as) b
1751 = do let ms = zipWith match' as (repeat b)
1752 case (rights (map toEither ms)) of
1753 (x: _) -> return x
1754 _ -> LeftErr (a, b)
1755 match (PCase _ _ _) _ = return [] -- lifted out
1756 match (PMetavar _) _ = return [] -- modified
1757 match (PInferRef _ _) _ = return [] -- modified
1758 match (PQuote _) _ = return []
1759 match (PProof _) _ = return []
1760 match (PTactics _) _ = return []
1761 match (PRefl _ _) (PRefl _ _) = return []
1762 match (PResolveTC _) (PResolveTC _) = return []
1763 match (PTrue _ _) (PTrue _ _) = return []
1764 match (PFalse _) (PFalse _) = return []
1765 match (PReturn _) (PReturn _) = return []
1766 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1767 ms <- match' s s'
1768 return (mt ++ ms)
1769 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1770 ms <- match' s s'
1771 return (mt ++ ms)
1772 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1773 mty <- match' ty ty'
1774 ms <- match' s s'
1775 return (mt ++ mty ++ ms)
1776 match (PHidden x) (PHidden y) = match' x y
1777 match (PUnifyLog x) y = match' x y
1778 match x (PUnifyLog y) = match' x y
1779 match (PNoImplicits x) y = match' x y
1780 match x (PNoImplicits y) = match' x y
1781 match Placeholder _ = return []
1782 match _ Placeholder = return []
1783 match (PResolveTC _) _ = return []
1784 match a b | a == b = return []
1785 | otherwise = LeftErr (a, b)
1787 checkRpts (RightOK ms) = check ms where
1788 check ((n,t):xs)
1789 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1790 then Left (t, t')
1791 else check xs
1792 check (_:xs) = check xs
1793 check [] = Right ms
1794 checkRpts (LeftErr x) = Left x
1796substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1797substMatches ms = substMatchesShadow ms []
1799substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1800substMatchesShadow [] shs t = t
1801substMatchesShadow ((n,tm):ns) shs t
1802 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1804substMatch :: Name -> PTerm -> PTerm -> PTerm
1805substMatch n = substMatchShadow n []
1807substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1808substMatchShadow n shs tm t = sm shs t where
1809 sm xs (PRef _ n') | n == n' = tm
1810 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1811 sm xs (PPi p x t sc)
1812 | x `elem` xs
1813 = let x' = nextName x in
1814 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1815 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1816 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1817 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1818 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1819 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1820 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1821 (fmap (sm xs) tm)
1822 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1823 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
1824 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
1825 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1826 sm xs (PHidden x) = PHidden (sm xs x)
1827 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1828 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1829 sm xs x = x
1831 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1832 fullApp x = x
1834shadow :: Name -> Name -> PTerm -> PTerm
1835shadow n n' t = sm t where
1836 sm (PRef fc x) | n == x = PRef fc n'
1837 sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)
1838 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1839 sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)
1840 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1841 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1842 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1843 sm (PEq f x y) = PEq f (sm x) (sm y)
1844 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1845 sm (PTyped x y) = PTyped (sm x) (sm y)
1846 sm (PPair f p x y) = PPair f p (sm x) (sm y)
1847 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
1848 sm (PAlternative a as) = PAlternative a (map sm as)
1849 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1850 sm (PProof ts) = PProof (map (fmap sm) ts)
1851 sm (PHidden x) = PHidden (sm x)
1852 sm (PUnifyLog x) = PUnifyLog (sm x)
1853 sm (PNoImplicits x) = PNoImplicits (sm x)
1854 sm x = x
1856-- Rename any binders which are repeated (so that we don't have to mess
1857-- about with shadowing anywhere else).
1859mkUniqueNames :: [Name] -> PTerm -> PTerm
1860mkUniqueNames env tm = evalState (mkUniq tm) env where
1861 inScope = boundNamesIn tm
1863 mkUniqA arg = do t' <- mkUniq (getTm arg)
1864 return (arg { getTm = t' })
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 n (env ++ inScope)
1876 return (n', shadow n n' sc)
1877 else return (n, sc)
1878 put (n' : env)
1879 ty' <- mkUniq ty
1880 sc'' <- mkUniq sc'
1881 return $! PLam n' ty' sc''
1882 mkUniq (PPi p n ty sc)
1883 = do env <- get
1884 (n', sc') <-
1885 if n `elem` env
1886 then do let n' = uniqueName n (env ++ inScope)
1887 return (n', shadow n n' sc)
1888 else return (n, sc)
1889 put (n' : env)
1890 ty' <- mkUniq ty
1891 sc'' <- mkUniq sc'
1892 return $! PPi p n' ty' sc''
1893 mkUniq (PLet n ty val sc)
1894 = do env <- get
1895 (n', sc') <-
1896 if n `elem` env
1897 then do let n' = uniqueName n (env ++ inScope)
1898 return (n', shadow n n' sc)
1899 else return (n, sc)
1900 put (n' : env)
1901 ty' <- mkUniq ty; val' <- mkUniq val
1902 sc'' <- mkUniq sc'
1903 return $! PLet n' ty' val' sc''
1904 mkUniq (PApp fc t args)
1905 = do t' <- mkUniq t
1906 args' <- mapM mkUniqA args
1907 return $! PApp fc t' args'
1908 mkUniq (PAppBind fc t args)
1909 = do t' <- mkUniq t
1910 args' <- mapM mkUniqA args
1911 return $! PAppBind fc t' args'
1912 mkUniq (PCase fc t alts)
1913 = do t' <- mkUniq t
1914 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
1915 return (x', y')) alts
1916 return $! PCase fc t' alts'
1917 mkUniq (PPair fc p l r)
1918 = do l' <- mkUniq l; r' <- mkUniq r
1919 return $! PPair fc p l' r'
1920 mkUniq (PDPair fc p (PRef fc' n) t sc)
1921 | t /= Placeholder
1922 = do env <- get
1923 (n', sc') <- if n `elem` env
1924 then do let n' = uniqueName n (env ++ inScope)
1925 return (n', shadow n n' sc)
1926 else return (n, sc)
1927 put (n' : env)
1928 t' <- mkUniq t
1929 sc'' <- mkUniq sc'
1930 return $! PDPair fc p (PRef fc' n') t' sc''
1931 mkUniq (PDPair fc p l t r)
1932 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
1933 return $! PDPair fc p l' t' r'
1934 mkUniq (PAlternative b as)
1935 = liftM (PAlternative b) (mapM mkUniq as)
1936 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
1937 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
1938 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
1939 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
1940 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
1941 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
1942 mkUniq t = return t