git.iko.soy/Idris-dev
on e90d88a help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1936 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 -- TODO 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)
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 insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
1530 -> [PArg] -- parameters
1531 -> [PArg] -- arguments
1532 -> [PArg]
1533 insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) =
1534 PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given
1535 insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) =
1536 PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given
1537 insImpAcc pnas (PConstraint p l n ty : ps) given =
1538 let rtc = PResolveTC fc in
1539 PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given
1540 insImpAcc pnas (PImp p _ l n ty : ps) given =
1541 case find n given [] of
1542 Just (tm, given') ->
1543 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given'
1544 Nothing ->
1545 PImp p True l n Placeholder :
1546 insImpAcc (M.insert n Placeholder pnas) ps given
1547 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given =
1548 let sc = addImpl ist (substMatches (M.toList pnas) sc') in
1549 case find n given [] of
1550 Just (tm, given') ->
1551 PTacImplicit p l n sc tm :
1552 insImpAcc (M.insert n tm pnas) ps given'
1553 Nothing ->
1554 if inpat
1555 then PTacImplicit p l n sc Placeholder :
1556 insImpAcc (M.insert n Placeholder pnas) ps given
1557 else PTacImplicit p l n sc sc :
1558 insImpAcc (M.insert n sc pnas) ps given
1559 insImpAcc _ expected [] = []
1560 insImpAcc _ _ given = given
1562 find n [] acc = Nothing
1563 find n (PImp _ _ _ n' t : gs) acc
1564 | n == n' = Just (t, reverse acc ++ gs)
1565 find n (PTacImplicit _ _ n' _ t : gs) acc
1566 | n == n' = Just (t, reverse acc ++ gs)
1567 find n (g : gs) acc = find n gs (g : acc)
1569-- replace non-linear occurrences with _
1570-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1571-- it is hard to get right!
1573stripLinear :: IState -> PTerm -> PTerm
1574stripLinear i tm = evalState (sl tm) [] where
1575 sl :: PTerm -> State [Name] PTerm
1576 sl (PRef fc f)
1577 | (_:_) <- lookupTy f (tt_ctxt i)
1578 = return $ PRef fc f
1579 | otherwise = do ns <- get
1580 if (f `elem` ns)
1581 then return Placeholder
1582 else do put (f : ns)
1583 return (PRef fc f)
1584 sl (PPatvar fc f)
1585 = do ns <- get
1586 if (f `elem` ns)
1587 then return Placeholder
1588 else do put (f : ns)
1589 return (PPatvar fc f)
1590 sl t@(PAlternative _ (a : as)) = do sl a
1591 return t
1592 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1593 args' <- mapM slA args
1594 return $ PApp fc fn args'
1595 where slA (PImp p m l n t) = do t' <- sl t
1596 return $ PImp p m l n t'
1597 slA (PExp p l n t) = do t' <- sl t
1598 return $ PExp p l n t'
1599 slA (PConstraint p l n t)
1600 = do t' <- sl t
1601 return $ PConstraint p l n t'
1602 slA (PTacImplicit p l n sc t)
1603 = do t' <- sl t
1604 return $ PTacImplicit p l n sc t'
1605 sl x = return x
1607-- Remove functions which aren't applied to anything, which must then
1608-- be resolved by unification. Assume names resolved and alternatives
1609-- filled in (so no ambiguity).
1611stripUnmatchable :: IState -> PTerm -> PTerm
1612stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1613 su :: PTerm -> PTerm
1614 su (PRef fc f)
1615 | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1616 = Placeholder
1617 su (PApp fc fn args)
1618 = PApp fc fn (fmap (fmap su) args)
1619 su (PAlternative b alts)
1620 = let alts' = filter (/= Placeholder) (map su alts) in
1621 if null alts' then Placeholder
1622 else PAlternative b alts'
1623 su (PPair fc p l r) = PPair fc p (su l) (su r)
1624 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1625 su t = t
1626stripUnmatchable i tm = tm
1628mkPApp fc a f [] = f
1629mkPApp fc a f as = let rest = drop a as in
1630 appRest fc (PApp fc f (take a as)) rest
1631 where
1632 appRest fc f [] = f
1633 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1635-- Find 'static' argument positions
1636-- (the declared ones, plus any names in argument position in the declared
1637-- statics)
1638-- FIXME: It's possible that this really has to happen after elaboration
1640findStatics :: IState -> PTerm -> (PTerm, [Bool])
1641findStatics ist tm = trace (show tm) $
1642 let (ns, ss) = fs tm in
1643 runState (pos ns ss tm) []
1644 where fs (PPi p n t sc)
1645 | Static <- pstatic p
1646 = let (ns, ss) = fs sc in
1647 (namesIn [] ist t : ns, n : ss)
1648 | otherwise = let (ns, ss) = fs sc in
1649 (ns, ss)
1650 fs _ = ([], [])
1652 inOne n ns = length (filter id (map (elem n) ns)) == 1
1654 pos ns ss (PPi p n t sc)
1655 | elem n ss = do sc' <- pos ns ss sc
1656 spos <- get
1657 put (True : spos)
1658 return (PPi (p { pstatic = Static }) n t sc')
1659 | otherwise = do sc' <- pos ns ss sc
1660 spos <- get
1661 put (False : spos)
1662 return (PPi p n t sc')
1663 pos ns ss t = return t
1665-- for 6.12/7 compatibility
1666data EitherErr a b = LeftErr a | RightOK b
1668instance Monad (EitherErr a) where
1669 return = RightOK
1671 (LeftErr e) >>= k = LeftErr e
1672 RightOK v >>= k = k v
1674toEither (LeftErr e) = Left e
1675toEither (RightOK ho) = Right ho
1677-- syntactic match of a against b, returning pair of variables in a
1678-- and what they match. Returns the pair that failed if not a match.
1680matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1681matchClause = matchClause' False
1683matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1684matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1685 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1687 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1688 fullApp x = x
1690 match' x y = match (fullApp x) (fullApp y)
1691 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1692 | fi == txt "fromInteger" && b == txt "builtins",
1693 PConstant (I _) <- getTm x = match (getTm x) x'
1694 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1695 | fi == txt "fromInteger" && b == txt "builtins",
1696 PConstant (I _) <- getTm x = match (getTm x) x'
1697 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1698 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1699 match (PApp _ f args) (PApp _ f' args')
1700 | length args == length args'
1701 = do mf <- match' f f'
1702 ms <- zipWithM matchArg args args'
1703 return (mf ++ concat ms)
1704-- match (PRef _ n) (PRef _ n') | n == n' = return []
1705-- | otherwise = Nothing
1706 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1707 match (PPatvar f n) xr = match (PRef f n) xr
1708 match xr (PPatvar f n) = match xr (PRef f n)
1709 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1710 match (PRef _ n) tm@(PRef _ n')
1711 | n == n' && not names &&
1712 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1713 || tm == Placeholder)
1714 = return [(n, tm)]
1715 | n == n' = return []
1716 match (PRef _ n) tm
1717 | not names && (not (isConName n (tt_ctxt i) ||
1718 isFnName n (tt_ctxt i)) || tm == Placeholder)
1719 = return [(n, tm)]
1720 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1721 mr <- match' r r'
1722 return (ml ++ mr)
1723 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1724 = do ml <- match' l l'
1725 mr <- match' r r'
1726 return (ml ++ mr)
1727 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1728 mr <- match r r'
1729 return (ml ++ mr)
1730 match (PTyped l r) x = match l x
1731 match x (PTyped l r) = match x l
1732 match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
1733 mr <- match' r r'
1734 return (ml ++ mr)
1735 match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'
1736 mt <- match' t t'
1737 mr <- match' r r'
1738 return (ml ++ mt ++ mr)
1739 match (PAlternative a as) (PAlternative a' as')
1740 = do ms <- zipWithM match' as as'
1741 return (concat ms)
1742 match a@(PAlternative _ as) b
1743 = do let ms = zipWith match' as (repeat b)
1744 case (rights (map toEither ms)) of
1745 (x: _) -> return x
1746 _ -> LeftErr (a, b)
1747 match (PCase _ _ _) _ = return [] -- lifted out
1748 match (PMetavar _) _ = return [] -- modified
1749 match (PInferRef _ _) _ = return [] -- modified
1750 match (PQuote _) _ = return []
1751 match (PProof _) _ = return []
1752 match (PTactics _) _ = return []
1753 match (PRefl _ _) (PRefl _ _) = return []
1754 match (PResolveTC _) (PResolveTC _) = return []
1755 match (PTrue _ _) (PTrue _ _) = return []
1756 match (PFalse _) (PFalse _) = return []
1757 match (PReturn _) (PReturn _) = return []
1758 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1759 ms <- match' s s'
1760 return (mt ++ ms)
1761 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1762 ms <- match' s s'
1763 return (mt ++ ms)
1764 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1765 mty <- match' ty ty'
1766 ms <- match' s s'
1767 return (mt ++ mty ++ ms)
1768 match (PHidden x) (PHidden y) = match' x y
1769 match (PUnifyLog x) y = match' x y
1770 match x (PUnifyLog y) = match' x y
1771 match (PNoImplicits x) y = match' x y
1772 match x (PNoImplicits y) = match' x y
1773 match Placeholder _ = return []
1774 match _ Placeholder = return []
1775 match (PResolveTC _) _ = return []
1776 match a b | a == b = return []
1777 | otherwise = LeftErr (a, b)
1779 checkRpts (RightOK ms) = check ms where
1780 check ((n,t):xs)
1781 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1782 then Left (t, t')
1783 else check xs
1784 check (_:xs) = check xs
1785 check [] = Right ms
1786 checkRpts (LeftErr x) = Left x
1788substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1789substMatches ms = substMatchesShadow ms []
1791substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1792substMatchesShadow [] shs t = t
1793substMatchesShadow ((n,tm):ns) shs t
1794 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1796substMatch :: Name -> PTerm -> PTerm -> PTerm
1797substMatch n = substMatchShadow n []
1799substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1800substMatchShadow n shs tm t = sm shs t where
1801 sm xs (PRef _ n') | n == n' = tm
1802 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1803 sm xs (PPi p x t sc)
1804 | x `elem` xs
1805 = let x' = nextName x in
1806 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1807 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1808 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1809 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1810 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1811 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1812 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1813 (fmap (sm xs) tm)
1814 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1815 sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
1816 sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)
1817 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1818 sm xs (PHidden x) = PHidden (sm xs x)
1819 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1820 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1821 sm xs x = x
1823 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1824 fullApp x = x
1826shadow :: Name -> Name -> PTerm -> PTerm
1827shadow n n' t = sm t where
1828 sm (PRef fc x) | n == x = PRef fc n'
1829 sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)
1830 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1831 sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)
1832 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1833 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1834 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1835 sm (PEq f x y) = PEq f (sm x) (sm y)
1836 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1837 sm (PTyped x y) = PTyped (sm x) (sm y)
1838 sm (PPair f p x y) = PPair f p (sm x) (sm y)
1839 sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)
1840 sm (PAlternative a as) = PAlternative a (map sm as)
1841 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1842 sm (PProof ts) = PProof (map (fmap sm) ts)
1843 sm (PHidden x) = PHidden (sm x)
1844 sm (PUnifyLog x) = PUnifyLog (sm x)
1845 sm (PNoImplicits x) = PNoImplicits (sm x)
1846 sm x = x
1848-- Rename any binders which are repeated (so that we don't have to mess
1849-- about with shadowing anywhere else).
1851mkUniqueNames :: [Name] -> PTerm -> PTerm
1852mkUniqueNames env tm = evalState (mkUniq tm) env where
1853 inScope = boundNamesIn tm
1855 mkUniqA arg = do t' <- mkUniq (getTm arg)
1856 return (arg { getTm = t' })
1858 -- FIXME: Probably ought to do this for completeness! It's fine as
1859 -- long as there are no bindings inside tactics though.
1860 mkUniqT tac = return tac
1862 mkUniq :: PTerm -> State [Name] PTerm
1863 mkUniq (PLam n ty sc)
1864 = do env <- get
1865 (n', sc') <-
1866 if n `elem` env
1867 then do let n' = uniqueName n (env ++ inScope)
1868 return (n', shadow n n' sc)
1869 else return (n, sc)
1870 put (n' : env)
1871 ty' <- mkUniq ty
1872 sc'' <- mkUniq sc'
1873 return $! PLam n' ty' sc''
1874 mkUniq (PPi p n ty sc)
1875 = do env <- get
1876 (n', sc') <-
1877 if n `elem` env
1878 then do let n' = uniqueName n (env ++ inScope)
1879 return (n', shadow n n' sc)
1880 else return (n, sc)
1881 put (n' : env)
1882 ty' <- mkUniq ty
1883 sc'' <- mkUniq sc'
1884 return $! PPi p n' ty' sc''
1885 mkUniq (PLet n ty val sc)
1886 = do env <- get
1887 (n', sc') <-
1888 if n `elem` env
1889 then do let n' = uniqueName n (env ++ inScope)
1890 return (n', shadow n n' sc)
1891 else return (n, sc)
1892 put (n' : env)
1893 ty' <- mkUniq ty; val' <- mkUniq val
1894 sc'' <- mkUniq sc'
1895 return $! PLet n' ty' val' sc''
1896 mkUniq (PApp fc t args)
1897 = do t' <- mkUniq t
1898 args' <- mapM mkUniqA args
1899 return $! PApp fc t' args'
1900 mkUniq (PAppBind fc t args)
1901 = do t' <- mkUniq t
1902 args' <- mapM mkUniqA args
1903 return $! PAppBind fc t' args'
1904 mkUniq (PCase fc t alts)
1905 = do t' <- mkUniq t
1906 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
1907 return (x', y')) alts
1908 return $! PCase fc t' alts'
1909 mkUniq (PPair fc p l r)
1910 = do l' <- mkUniq l; r' <- mkUniq r
1911 return $! PPair fc p l' r'
1912 mkUniq (PDPair fc p (PRef fc' n) t sc)
1913 | t /= Placeholder
1914 = do env <- get
1915 (n', sc') <- if n `elem` env
1916 then do let n' = uniqueName n (env ++ inScope)
1917 return (n', shadow n n' sc)
1918 else return (n, sc)
1919 put (n' : env)
1920 t' <- mkUniq t
1921 sc'' <- mkUniq sc'
1922 return $! PDPair fc p (PRef fc' n') t' sc''
1923 mkUniq (PDPair fc p l t r)
1924 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
1925 return $! PDPair fc p l' t' r'
1926 mkUniq (PAlternative b as)
1927 = liftM (PAlternative b) (mapM mkUniq as)
1928 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
1929 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
1930 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
1931 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
1932 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
1933 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
1934 mkUniq t = return t