git.iko.soy/Idris-dev
on dc4ce0c help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1641 lines 68 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.IdeSlave
13import IRTS.CodegenCommon
14import Util.DynamicLinker
16import Paths_idris
18import System.Console.Haskeline
19import System.IO
21import Control.Monad.State
22import Control.Monad.Error(throwError)
24import Data.List
25import Data.Char
26import qualified Data.Text as T
27import Data.Either
28import Data.Maybe
29import Data.Word (Word)
31import Debug.Trace
33import Control.Monad.Error (throwError, catchError)
34import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
36import Util.Pretty
37import Util.System
39getContext :: Idris Context
40getContext = do i <- getIState; return (tt_ctxt i)
42forCodegen :: Codegen -> [(Codegen, a)] -> [a]
43forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']
45getObjectFiles :: Codegen -> Idris [FilePath]
46getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
48addObjectFile :: Codegen -> FilePath -> Idris ()
49addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
51getLibs :: Codegen -> Idris [String]
52getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
54addLib :: Codegen -> String -> Idris ()
55addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
57getFlags :: Codegen -> Idris [String]
58getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
60addFlag :: Codegen -> String -> Idris ()
61addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
63addDyLib :: [String] -> Idris (Either DynamicLib String)
64addDyLib libs = do i <- getIState
65 let ls = idris_dynamic_libs i
66 case mapMaybe (findDyLib ls) libs of
67 x:_ -> return (Left x)
68 [] -> do
69 handle <- lift . lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) $ libs
70 case msum handle of
71 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
72 concat (intersperse "," libs) ++ "\"")
73 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
74 return (Left x)
75 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
76 findDyLib [] l = Nothing
77 findDyLib (lib:libs) l | l == lib_name lib = Just lib
78 | otherwise = findDyLib libs l
81addHdr :: Codegen -> String -> Idris ()
82addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
84addLangExt :: LanguageExt -> Idris ()
85addLangExt TypeProviders = do i <- getIState
86 putIState $ i {
87 idris_language_extensions = TypeProviders : idris_language_extensions i
88 }
89addLangExt ErrorReflection = do i <- getIState
90 putIState $ i {
91 idris_language_extensions = ErrorReflection : idris_language_extensions i
92 }
94addTrans :: (Term, Term) -> Idris ()
95addTrans t = do i <- getIState
96 putIState $ i { idris_transforms = t : idris_transforms i }
98totcheck :: (FC, Name) -> Idris ()
99totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
101defer_totcheck :: (FC, Name) -> Idris ()
102defer_totcheck n
103 = do i <- getIState;
104 putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
106clear_totcheck :: Idris ()
107clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
109setFlags :: Name -> [FnOpt] -> Idris ()
110setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
112setAccessibility :: Name -> Accessibility -> Idris ()
113setAccessibility n a
114 = do i <- getIState
115 let ctxt = setAccess n a (tt_ctxt i)
116 putIState $ i { tt_ctxt = ctxt }
118setTotality :: Name -> Totality -> Idris ()
119setTotality n a
120 = do i <- getIState
121 let ctxt = setTotal n a (tt_ctxt i)
122 putIState $ i { tt_ctxt = ctxt }
124getTotality :: Name -> Idris Totality
125getTotality n
126 = do i <- getIState
127 case lookupTotal n (tt_ctxt i) of
128 [t] -> return t
129 _ -> return (Total [])
131-- Get coercions which might return the required type
132getCoercionsTo :: IState -> Type -> [Name]
133getCoercionsTo i ty =
134 let cs = idris_coercions i
135 (fn,_) = unApply (getRetTy ty) in
136 findCoercions fn cs
137 where findCoercions t [] = []
138 findCoercions t (n : ns) =
139 let ps = case lookupTy n (tt_ctxt i) of
140 [ty'] -> case unApply (getRetTy ty') of
141 (t', _) ->
142 if t == t' then [n] else []
143 _ -> [] in
144 ps ++ findCoercions t ns
146addToCG :: Name -> CGInfo -> Idris ()
147addToCG n cg
148 = do i <- getIState
149 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
151-- Trace all the names in a call graph starting at the given name
152getAllNames :: Name -> Idris [Name]
153getAllNames n = allNames [] n
155allNames :: [Name] -> Name -> Idris [Name]
156allNames ns n | n `elem` ns = return []
157allNames ns n = do i <- getIState
158 case lookupCtxtExact n (idris_callgraph i) of
159 [ns'] -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
160 return (nub (n : concat more))
161 _ -> return [n]
163addCoercion :: Name -> Idris ()
164addCoercion n = do i <- getIState
165 putIState $ i { idris_coercions = nub $ n : idris_coercions i }
167addDocStr :: Name -> String -> Idris ()
168addDocStr n doc
169 = do i <- getIState
170 putIState $ i { idris_docstrings = addDef n doc (idris_docstrings i) }
172addNameHint :: Name -> Name -> Idris ()
173addNameHint ty n
174 = do i <- getIState
175 ty' <- case lookupCtxtName ty (idris_implicits i) of
176 [(tyn, _)] -> return tyn
177 [] -> throwError (NoSuchVariable ty)
178 tyns -> throwError (CantResolveAlts (map show (map fst tyns)))
179 let ns' = case lookupCtxt ty' (idris_namehints i) of
180 [ns] -> ns ++ [n]
181 _ -> [n]
182 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
184getNameHints :: IState -> Name -> [Name]
185getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
186getNameHints i n =
187 case lookupCtxt n (idris_namehints i) of
188 [ns] -> ns
189 _ -> []
191addToCalledG :: Name -> [Name] -> Idris ()
192addToCalledG n ns = return () -- TODO
194-- Add a class instance function. Dodgy hack: Put integer instances first in the
195-- list so they are resolved by default.
196-- Dodgy hack 2: put constraint chasers (@@) last
198addInstance :: Bool -> Name -> Name -> Idris ()
199addInstance int n i
200 = do ist <- getIState
201 case lookupCtxt n (idris_classes ist) of
202 [CI a b c d e ins] ->
203 do let cs = addDef n (CI a b c d e (addI i ins)) (idris_classes ist)
204 putIState $ ist { idris_classes = cs }
205 _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [i]) (idris_classes ist)
206 putIState $ ist { idris_classes = cs }
207 where addI i ins | int = i : ins
208 | chaser n = ins ++ [i]
209 | otherwise = insI i ins
210 insI i [] = [i]
211 insI i (n : ns) | chaser n = i : n : ns
212 | otherwise = n : insI i ns
214 chaser (UN nm)
215 | ('@':'@':_) <- str nm = True
216 chaser (NS n _) = chaser n
217 chaser _ = False
219addClass :: Name -> ClassInfo -> Idris ()
220addClass n i
221 = do ist <- getIState
222 let i' = case lookupCtxt n (idris_classes ist) of
223 [c] -> c { class_instances = class_instances i }
224 _ -> i
225 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
227addIBC :: IBCWrite -> Idris ()
228addIBC ibc@(IBCDef n)
229 = do i <- getIState
230 when (notDef (ibc_write i)) $
231 putIState $ i { ibc_write = ibc : ibc_write i }
232 where notDef [] = True
233 notDef (IBCDef n': is) | n == n' = False
234 notDef (_ : is) = notDef is
235addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
237clearIBC :: Idris ()
238clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
240resetNameIdx :: Idris ()
241resetNameIdx = do i <- getIState
242 put (i { idris_nameIdx = (0, emptyContext) })
244-- Used to preserve sharing of names
245addNameIdx :: Name -> Idris (Int, Name)
246addNameIdx n = do i <- getIState
247 let (i', x) = addNameIdx' i n
248 return x
250addNameIdx' :: IState -> Name -> (IState, (Int, Name))
251addNameIdx' i n
252 = let idxs = snd (idris_nameIdx i) in
253 case lookupCtxt n idxs of
254 [x] -> (i, x)
255 _ -> let i' = fst (idris_nameIdx i) + 1 in
256 (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
258getHdrs :: Codegen -> Idris [String]
259getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
261setErrLine :: Int -> Idris ()
262setErrLine x = do i <- getIState;
263 case (errLine i) of
264 Nothing -> putIState $ i { errLine = Just x }
265 Just _ -> return ()
267clearErr :: Idris ()
268clearErr = do i <- getIState
269 putIState $ i { errLine = Nothing }
271getSO :: Idris (Maybe String)
272getSO = do i <- getIState
273 return (compiled_so i)
275setSO :: Maybe String -> Idris ()
276setSO s = do i <- getIState
277 putIState $ (i { compiled_so = s })
279getIState :: Idris IState
280getIState = get
282putIState :: IState -> Idris ()
283putIState = put
285-- | A version of liftIO that puts errors into the exception type of the Idris monad
286runIO :: IO a -> Idris a
287runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
288-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
290getName :: Idris Int
291getName = do i <- getIState;
292 let idx = idris_name i;
293 putIState $ (i { idris_name = idx + 1 })
294 return idx
296addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
297addInternalApp fp l t
298 = do i <- getIState
299 putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })
301getInternalApp :: FilePath -> Int -> Idris PTerm
302getInternalApp fp l = do i <- getIState
303 case lookup (fp, l) (idris_lineapps i) of
304 Just n' -> return n'
305 Nothing -> return Placeholder
306 -- TODO: What if it's not there?
308-- Pattern definitions are only used for coverage checking, so erase them
309-- when we're done
310clearOrigPats :: Idris ()
311clearOrigPats = do i <- get
312 let ps = idris_patdefs i
313 let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
314 put (i { idris_patdefs = ps' })
316-- Erase types from Ps in the context (basically ending up with what's in
317-- the .ibc, which is all we need after all the analysis is done)
318clearPTypes :: Idris ()
319clearPTypes = do i <- get
320 let ctxt = tt_ctxt i
321 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
322 where pErase (CaseOp c t tys orig tot cds)
323 = CaseOp c t tys orig [] (pErase' cds)
324 pErase x = x
325 pErase' (CaseDefs _ (cs, c) _ rs)
326 = let c' = (cs, fmap pEraseType c) in
327 CaseDefs c' c' c' rs
329checkUndefined :: FC -> Name -> Idris ()
330checkUndefined fc n
331 = do i <- getContext
332 case lookupTy n i of
333 (_:_) -> throwError . Msg $ show fc ++ ":" ++
334 show n ++ " already defined"
335 _ -> return ()
337isUndefined :: FC -> Name -> Idris Bool
338isUndefined fc n
339 = do i <- getContext
340 case lookupTy n i of
341 (_:_) -> return False
342 _ -> return True
344setContext :: Context -> Idris ()
345setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
347updateContext :: (Context -> Context) -> Idris ()
348updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
350addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
351addConstraints fc (v, cs)
352 = do i <- getIState
353 let ctxt = tt_ctxt i
354 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
355 next_tvar = v }
356 let ics = zip cs (repeat fc) ++ idris_constraints i
357 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
359addDeferred = addDeferred' Ref
360addDeferredTyCon = addDeferred' (TCon 0 0)
362addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
363addDeferred' nt ns
364 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns
365 i <- getIState
366 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
367 idris_metavars i }
368 where tidyNames used (Bind (MN i x) b sc)
369 = let n' = uniqueName (UN x) used in
370 Bind n' b $ tidyNames (n':used) sc
371 tidyNames used (Bind n b sc)
372 = let n' = uniqueName n used in
373 Bind n' b $ tidyNames (n':used) sc
374 tidyNames used b = b
376solveDeferred :: Name -> Idris ()
377solveDeferred n = do i <- getIState
378 putIState $ i { idris_metavars =
379 filter (\(n', _) -> n/=n')
380 (idris_metavars i) }
382getUndefined :: Idris [Name]
383getUndefined = do i <- getIState
384 return (map fst (idris_metavars i) \\ primDefs)
386ihPrintResult :: Handle -> String -> Idris ()
387ihPrintResult h s = do i <- getIState
388 case idris_outputmode i of
389 RawOutput -> case s of
390 "" -> return ()
391 s -> runIO $ hPutStrLn h s
392 IdeSlave n ->
393 let good = SexpList [SymbolAtom "ok", toSExp s] in
394 runIO $ hPutStrLn h $ convSExp "return" good n
396ihPrintError :: Handle -> String -> Idris ()
397ihPrintError h s = do i <- getIState
398 case idris_outputmode i of
399 RawOutput -> case s of
400 "" -> return ()
401 s -> runIO $ hPutStrLn h s
402 IdeSlave n ->
403 let good = SexpList [SymbolAtom "error", toSExp s] in
404 runIO . hPutStrLn h $ convSExp "return" good n
406ihputStrLn :: Handle -> String -> Idris ()
407ihputStrLn h s = do i <- getIState
408 case idris_outputmode i of
409 RawOutput -> runIO $ hPutStrLn h s
410 IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n
412iputStrLn = ihputStrLn stdout
413iPrintError = ihPrintError stdout
414iPrintResult = ihPrintResult stdout
415iWarn = ihWarn stdout
417ideslavePutSExp :: SExpable a => String -> a -> Idris ()
418ideslavePutSExp cmd info = do i <- getIState
419 case idris_outputmode i of
420 IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
421 _ -> return ()
423-- this needs some typing magic and more structured output towards emacs
424iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
425iputGoal g = do i <- getIState
426 case idris_outputmode i of
427 RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)
428 IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" (displayS g "") n
430isetPrompt :: String -> Idris ()
431isetPrompt p = do i <- getIState
432 case idris_outputmode i of
433 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n
435ihWarn :: Handle -> FC -> String -> Idris ()
436ihWarn h fc err = do i <- getIState
437 case idris_outputmode i of
438 RawOutput -> runIO $ hPutStrLn h (show fc ++ ":" ++ err)
439 IdeSlave n -> runIO $ hPutStrLn h $ convSExp "warning" (fc_fname fc, fc_line fc, fc_column fc, err) n
441setLogLevel :: Int -> Idris ()
442setLogLevel l = do i <- getIState
443 let opts = idris_options i
444 let opt' = opts { opt_logLevel = l }
445 putIState $ i { idris_options = opt' }
447setCmdLine :: [Opt] -> Idris ()
448setCmdLine opts = do i <- getIState
449 let iopts = idris_options i
450 putIState $ i { idris_options = iopts { opt_cmdline = opts } }
452getCmdLine :: Idris [Opt]
453getCmdLine = do i <- getIState
454 return (opt_cmdline (idris_options i))
456getDumpDefun :: Idris (Maybe FilePath)
457getDumpDefun = do i <- getIState
458 return $ findC (opt_cmdline (idris_options i))
459 where findC [] = Nothing
460 findC (DumpDefun x : _) = Just x
461 findC (_ : xs) = findC xs
463getDumpCases :: Idris (Maybe FilePath)
464getDumpCases = do i <- getIState
465 return $ findC (opt_cmdline (idris_options i))
466 where findC [] = Nothing
467 findC (DumpCases x : _) = Just x
468 findC (_ : xs) = findC xs
470logLevel :: Idris Int
471logLevel = do i <- getIState
472 return (opt_logLevel (idris_options i))
474setErrContext :: Bool -> Idris ()
475setErrContext t = do i <- getIState
476 let opts = idris_options i
477 let opt' = opts { opt_errContext = t }
478 putIState $ i { idris_options = opt' }
480errContext :: Idris Bool
481errContext = do i <- getIState
482 return (opt_errContext (idris_options i))
484useREPL :: Idris Bool
485useREPL = do i <- getIState
486 return (opt_repl (idris_options i))
488setREPL :: Bool -> Idris ()
489setREPL t = do i <- getIState
490 let opts = idris_options i
491 let opt' = opts { opt_repl = t }
492 putIState $ i { idris_options = opt' }
494setNoBanner :: Bool -> Idris ()
495setNoBanner n = do i <- getIState
496 let opts = idris_options i
497 let opt' = opts {opt_nobanner = n}
498 putIState $ i { idris_options = opt' }
500getNoBanner :: Idris Bool
501getNoBanner = do i <- getIState
502 let opts = idris_options i
503 return (opt_nobanner opts)
505setQuiet :: Bool -> Idris ()
506setQuiet q = do i <- getIState
507 let opts = idris_options i
508 let opt' = opts { opt_quiet = q }
509 putIState $ i { idris_options = opt' }
511getQuiet :: Idris Bool
512getQuiet = do i <- getIState
513 let opts = idris_options i
514 return (opt_quiet opts)
516setCodegen :: Codegen -> Idris ()
517setCodegen t = do i <- getIState
518 let opts = idris_options i
519 let opt' = opts { opt_codegen = t }
520 putIState $ i { idris_options = opt' }
522codegen :: Idris Codegen
523codegen = do i <- getIState
524 return (opt_codegen (idris_options i))
526setOutputTy :: OutputType -> Idris ()
527setOutputTy t = do i <- getIState
528 let opts = idris_options i
529 let opt' = opts { opt_outputTy = t }
530 putIState $ i { idris_options = opt' }
532outputTy :: Idris OutputType
533outputTy = do i <- getIState
534 return $ opt_outputTy $ idris_options i
536setIdeSlave :: Bool -> Idris ()
537setIdeSlave True = do i <- getIState
538 putIState $ i { idris_outputmode = (IdeSlave 0), idris_colourRepl = False }
539setIdeSlave False = return ()
541setTargetTriple :: String -> Idris ()
542setTargetTriple t = do i <- getIState
543 let opts = idris_options i
544 opt' = opts { opt_triple = t }
545 putIState $ i { idris_options = opt' }
547targetTriple :: Idris String
548targetTriple = do i <- getIState
549 return (opt_triple (idris_options i))
551setTargetCPU :: String -> Idris ()
552setTargetCPU t = do i <- getIState
553 let opts = idris_options i
554 opt' = opts { opt_cpu = t }
555 putIState $ i { idris_options = opt' }
557targetCPU :: Idris String
558targetCPU = do i <- getIState
559 return (opt_cpu (idris_options i))
561setOptLevel :: Word -> Idris ()
562setOptLevel t = do i <- getIState
563 let opts = idris_options i
564 opt' = opts { opt_optLevel = t }
565 putIState $ i { idris_options = opt' }
567optLevel :: Idris Word
568optLevel = do i <- getIState
569 return (opt_optLevel (idris_options i))
571verbose :: Idris Bool
572verbose = do i <- getIState
573 return (opt_verbose (idris_options i))
575setVerbose :: Bool -> Idris ()
576setVerbose t = do i <- getIState
577 let opts = idris_options i
578 let opt' = opts { opt_verbose = t }
579 putIState $ i { idris_options = opt' }
581typeInType :: Idris Bool
582typeInType = do i <- getIState
583 return (opt_typeintype (idris_options i))
585setTypeInType :: Bool -> Idris ()
586setTypeInType t = do i <- getIState
587 let opts = idris_options i
588 let opt' = opts { opt_typeintype = t }
589 putIState $ i { idris_options = opt' }
591coverage :: Idris Bool
592coverage = do i <- getIState
593 return (opt_coverage (idris_options i))
595setCoverage :: Bool -> Idris ()
596setCoverage t = do i <- getIState
597 let opts = idris_options i
598 let opt' = opts { opt_coverage = t }
599 putIState $ i { idris_options = opt' }
601setIBCSubDir :: FilePath -> Idris ()
602setIBCSubDir fp = do i <- getIState
603 let opts = idris_options i
604 let opt' = opts { opt_ibcsubdir = fp }
605 putIState $ i { idris_options = opt' }
607valIBCSubDir :: IState -> Idris FilePath
608valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
610addImportDir :: FilePath -> Idris ()
611addImportDir fp = do i <- getIState
612 let opts = idris_options i
613 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
614 putIState $ i { idris_options = opt' }
616setImportDirs :: [FilePath] -> Idris ()
617setImportDirs fps = do i <- getIState
618 let opts = idris_options i
619 let opt' = opts { opt_importdirs = fps }
620 putIState $ i { idris_options = opt' }
622allImportDirs :: Idris [FilePath]
623allImportDirs = do i <- getIState
624 let optdirs = opt_importdirs (idris_options i)
625 return ("." : reverse optdirs)
627colourise :: Idris Bool
628colourise = do i <- getIState
629 return $ idris_colourRepl i
631setColourise :: Bool -> Idris ()
632setColourise b = do i <- getIState
633 putIState $ i { idris_colourRepl = b }
635setOutH :: Handle -> Idris ()
636setOutH h = do i <- getIState
637 putIState $ i { idris_outh = h }
639impShow :: Idris Bool
640impShow = do i <- getIState
641 return (opt_showimp (idris_options i))
643setImpShow :: Bool -> Idris ()
644setImpShow t = do i <- getIState
645 let opts = idris_options i
646 let opt' = opts { opt_showimp = t }
647 putIState $ i { idris_options = opt' }
649setColour :: ColourType -> IdrisColour -> Idris ()
650setColour ct c = do i <- getIState
651 let newTheme = setColour' ct c (idris_colourTheme i)
652 putIState $ i { idris_colourTheme = newTheme }
653 where setColour' KeywordColour c t = t { keywordColour = c }
654 setColour' BoundVarColour c t = t { boundVarColour = c }
655 setColour' ImplicitColour c t = t { implicitColour = c }
656 setColour' FunctionColour c t = t { functionColour = c }
657 setColour' TypeColour c t = t { typeColour = c }
658 setColour' DataColour c t = t { dataColour = c }
659 setColour' PromptColour c t = t { promptColour = c }
661logLvl :: Int -> String -> Idris ()
662logLvl l str = do i <- getIState
663 let lvl = opt_logLevel (idris_options i)
664 when (lvl >= l) $
665 case idris_outputmode i of
666 RawOutput -> do runIO $ putStrLn str
667 IdeSlave n ->
668 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
669 runIO $ putStrLn $ convSExp "log" good n
671cmdOptType :: Opt -> Idris Bool
672cmdOptType x = do i <- getIState
673 return $ x `elem` opt_cmdline (idris_options i)
675iLOG :: String -> Idris ()
676iLOG = logLvl 1
678noErrors :: Idris Bool
679noErrors = do i <- getIState
680 case errLine i of
681 Nothing -> return True
682 _ -> return False
684setTypeCase :: Bool -> Idris ()
685setTypeCase t = do i <- getIState
686 let opts = idris_options i
687 let opt' = opts { opt_typecase = t }
688 putIState $ i { idris_options = opt' }
691-- Dealing with parameters
693expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
694 [Name] -> -- all names
695 [Name] -> -- names with no declaration
696 PTerm -> PTerm
697expandParams dec ps ns infs tm = en tm
698 where
699 -- if we shadow a name (say in a lambda binding) that is used in a call to
700 -- a lifted function, we need access to both names - once in the scope of the
701 -- binding and once to call the lifted functions. So we'll explicitly shadow
702 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
703 -- but we didn't...)
705 mkShadow (UN n) = MN 0 n
706 mkShadow (MN i n) = MN (i+1) n
707 mkShadow (NS x s) = NS (mkShadow x) s
709 en (PLam n t s)
710 | n `elem` (map fst ps ++ ns)
711 = let n' = mkShadow n in
712 PLam n' (en t) (en (shadow n n' s))
713 | otherwise = PLam n (en t) (en s)
714 en (PPi p n t s)
715 | n `elem` (map fst ps ++ ns)
716 = let n' = mkShadow n in
717 PPi p n' (en t) (en (shadow n n' s))
718 | otherwise = PPi p n (en t) (en s)
719 en (PLet n ty v s)
720 | n `elem` (map fst ps ++ ns)
721 = let n' = mkShadow n in
722 PLet n' (en ty) (en v) (en (shadow n n' s))
723 | otherwise = PLet n (en ty) (en v) (en s)
724 -- FIXME: Should only do this in a type signature!
725 en (PDPair f (PRef f' n) t r)
726 | n `elem` (map fst ps ++ ns) && t /= Placeholder
727 = let n' = mkShadow n in
728 PDPair f (PRef f' n') (en t) (en (shadow n n' r))
729 en (PEq f l r) = PEq f (en l) (en r)
730 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
731 en (PTyped l r) = PTyped (en l) (en r)
732 en (PPair f l r) = PPair f (en l) (en r)
733 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
734 en (PAlternative a as) = PAlternative a (map en as)
735 en (PHidden t) = PHidden (en t)
736 en (PUnifyLog t) = PUnifyLog (en t)
737 en (PNoImplicits t) = PNoImplicits (en t)
738 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
739 en (PProof ts) = PProof (map (fmap en) ts)
740 en (PTactics ts) = PTactics (map (fmap en) ts)
742 en (PQuote (Var n))
743 | n `nselem` ns = PQuote (Var (dec n))
744 en (PApp fc (PInferRef fc' n) as)
745 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
746 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
747 en (PApp fc (PRef fc' n) as)
748 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
749 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
750 | n `nselem` ns = PApp fc (PRef fc' (dec n))
751 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
752 en (PAppBind fc (PRef fc' n) as)
753 | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
754 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
755 | n `nselem` ns = PAppBind fc (PRef fc' (dec n))
756 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
757 en (PRef fc n)
758 | n `elem` infs = PApp fc (PInferRef fc (dec n))
759 (map (pexp . (PRef fc)) (map fst ps))
760 | n `nselem` ns = PApp fc (PRef fc (dec n))
761 (map (pexp . (PRef fc)) (map fst ps))
762 en (PInferRef fc n)
763 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
764 (map (pexp . (PRef fc)) (map fst ps))
765 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
766 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
767 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
768 en t = t
770 nselem x [] = False
771 nselem x (y : xs) | nseq x y = True
772 | otherwise = nselem x xs
774 nseq x y = nsroot x == nsroot y
776expandParamsD :: Bool -> -- True = RHS only
777 IState ->
778 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
779expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)
780 = if n `elem` ns && (not rhsonly)
781 then -- trace (show (n, expandParams dec ps ns ty)) $
782 PTy doc syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
783 else --trace (show (n, expandParams dec ps ns ty)) $
784 PTy doc syn fc o n (expandParams dec ps ns [] ty)
785expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
786 = if n `elem` ns && (not rhsonly)
787 then -- trace (show (n, expandParams dec ps ns ty)) $
788 PPostulate doc syn fc o (dec n) (piBind ps
789 (expandParams dec ps ns [] ty))
790 else --trace (show (n, expandParams dec ps ns ty)) $
791 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
792expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
793 = let n' = if n `elem` ns then dec n else n in
794 PClauses fc opts n' (map expandParamsC cs)
795 where
796 expandParamsC (PClause fc n lhs ws rhs ds)
797 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
798 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
799 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
800 n' = if n `elem` ns then dec n else n
801 -- names bound on the lhs should not be expanded on the rhs
802 ns' = removeBound lhs ns in
803 PClause fc n' lhs'
804 (map (expandParams dec ps'' ns' []) ws)
805 (expandParams dec ps'' ns' [] rhs)
806 (map (expandParamsD True ist dec ps'' ns') ds)
807 expandParamsC (PWith fc n lhs ws wval ds)
808 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
809 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
810 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
811 n' = if n `elem` ns then dec n else n
812 ns' = removeBound lhs ns in
813 PWith fc n' lhs'
814 (map (expandParams dec ps'' ns' []) ws)
815 (expandParams dec ps'' ns' [] wval)
816 (map (expandParamsD rhsonly ist dec ps'' ns') ds)
817 updateps yn nm [] = []
818 updateps yn nm (((a, t), i):as)
819 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
820 | otherwise = (sMN i (show n ++ "_u"), t) : updateps yn nm as
822 removeBound lhs ns = ns \\ nub (bnames lhs)
824 bnames (PRef _ n) = [n]
825 bnames (PApp _ _ args) = concatMap bnames (map getTm args)
826 bnames (PPair _ l r) = bnames l ++ bnames r
827 bnames (PDPair _ l Placeholder r) = bnames l ++ bnames r
828 bnames _ = []
830expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
831 = PData doc syn fc co (expandPData pd)
832 where
833 -- just do the type decl, leave constructors alone (parameters will be
834 -- added implicitly)
835 expandPData (PDatadecl n ty cons)
836 = if n `elem` ns
837 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
838 (map econ cons)
839 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
840 econ (doc, n, t, fc, fs)
841 = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
842expandParamsD rhs ist dec ps ns (PParams f params pds)
843 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
844 (map (expandParamsD True ist dec ps ns) pds)
845-- (map (expandParamsD ist dec ps ns) pds)
846expandParamsD rhs ist dec ps ns (PMutual f pds)
847 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
848expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
849 = PClass doc info f
850 (map (expandParams dec ps ns []) cs)
851 n
852 (map (mapsnd (expandParams dec ps ns [])) params)
853 (map (expandParamsD rhs ist dec ps ns) decls)
854expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
855 = PInstance info f
856 (map (expandParams dec ps ns []) cs)
857 n
858 (map (expandParams dec ps ns []) params)
859 (expandParams dec ps ns [] ty)
860 cn
861 (map (expandParamsD rhs ist dec ps ns) decls)
862expandParamsD rhs ist dec ps ns d = d
864mapsnd f (x, t) = (x, f t)
866-- Calculate a priority for a type, for deciding elaboration order
867-- * if it's just a type variable or concrete type, do it early (0)
868-- * if there's only type variables and injective constructors, do it next (1)
869-- * if there's a function type, next (2)
870-- * finally, everything else (3)
872getPriority :: IState -> PTerm -> Int
873getPriority i tm = 1 -- pri tm
874 where
875 pri (PRef _ n) =
876 case lookupP n (tt_ctxt i) of
877 ((P (DCon _ _) _ _):_) -> 1
878 ((P (TCon _ _) _ _):_) -> 1
879 ((P Ref _ _):_) -> 1
880 [] -> 0 -- must be locally bound, if it's not an error...
881 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
882 pri (PTrue _) = 0
883 pri (PFalse _) = 0
884 pri (PRefl _ _) = 1
885 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
886 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
887 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
888 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
889 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
890 pri (PTyped l r) = pri l
891 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
892 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
893 pri (PAlternative a as) = maximum (map pri as)
894 pri (PConstant _) = 0
895 pri Placeholder = 1
896 pri _ = 3
898addStatics :: Name -> Term -> PTerm -> Idris ()
899addStatics n tm ptm =
900 do let (statics, dynamics) = initStatics tm ptm
901 let stnames = nub $ concatMap freeArgNames (map snd statics)
902 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
903 -- also get the arguments which are 'uniquely inferrable' from
904 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
905 let statics' = nub $ map fst statics ++
906 filter (\x -> not (elem x dnames)) stnames
907 let stpos = staticList statics' tm
908 i <- getIState
909 when (not (null statics)) $
910 logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics
911 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
912 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
913 addIBC (IBCStatic n)
914 where
915 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
916 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
917 if pstatic p == Static then ((n, ty) : static, dynamic)
918 else if (not (searchArg p))
919 then (static, (n, ty) : dynamic)
920 else (static, dynamic)
921 initStatics t pt = ([], [])
923 freeArgNames (Bind n (Pi ty) sc)
924 = nub $ freeArgNames ty
925 freeArgNames tm = let (_, args) = unApply tm in
926 concatMap freeNames args
928 -- if a name appears in a type class or tactic implicit index, it doesn't
929 -- affect its 'uniquely inferrable' from a static status since these are
930 -- resolved by searching.
931 searchArg (Constraint _ _ _) = True
932 searchArg (TacImp _ _ _ _) = True
933 searchArg _ = False
935 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
936 staticList _ _ = []
938-- Dealing with implicit arguments
940-- Add constraint bindings from using block
942addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
943addUsingConstraints syn fc t
944 = do ist <- get
945 let ns = namesIn [] ist t
946 let cs = getConstraints t -- check declared constraints
947 let addconsts = uconsts \\ cs
948 -- if all names in the arguments of addconsts appear in ns,
949 -- add the constraint implicitly
950 return (doAdd addconsts ns t)
951 where uconsts = filter uconst (using syn)
952 uconst (UConstraint _ _) = True
953 uconst _ = False
955 doAdd [] _ t = t
956 -- if all of args in ns, then add it
957 doAdd (UConstraint c args : cs) ns t
958 | all (\n -> elem n ns) args
959 = PPi (Constraint False Dynamic "") (sMN 0 "cu")
960 (mkConst c args) (doAdd cs ns t)
961 | otherwise = doAdd cs ns t
963 mkConst c args = PApp fc (PRef fc c)
964 (map (\n -> PExp 0 False (PRef fc n) "") args)
966 getConstraints (PPi (Constraint _ _ _) _ c sc)
967 = getcapp c ++ getConstraints sc
968 getConstraints (PPi _ _ c sc) = getConstraints sc
969 getConstraints _ = []
971 getcapp (PApp _ (PRef _ c) args)
972 = do ns <- mapM getName args
973 return (UConstraint c ns)
974 getcapp _ = []
976 getName (PExp _ _ (PRef _ n) _) = return n
977 getName _ = []
979-- Add implicit Pi bindings for any names in the term which appear in an
980-- argument position.
982-- This has become a right mess already. Better redo it some time...
984implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
985implicit syn n ptm = implicit' syn [] n ptm
987implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
988implicit' syn ignore n ptm
989 = do i <- getIState
990 let (tm', impdata) = implicitise syn ignore i ptm
991-- let (tm'', spos) = findStatics i tm'
992 putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
993 addIBC (IBCImp n)
994 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
995-- i <- get
996-- putIState $ i { idris_statics = addDef n spos (idris_statics i) }
997 return tm'
999implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
1000implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1001 let (declimps, ns') = execState (imps True [] tm) ([], [])
1002 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
1003 ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
1004 nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
1005 if null ns
1006 then (tm, reverse declimps)
1007 else implicitise syn ignore ist (pibind uvars nsOrder tm)
1008 where
1009 uvars = map ipair (filter uimplicit (using syn))
1010 pvars = syn_params syn
1012 inUsing n = n `elem` map fst uvars
1014 ipair (UImplicit x y) = (x, y)
1015 uimplicit (UImplicit _ _) = True
1016 uimplicit _ = False
1018 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
1019 | otherwise = x : dropAll xs ys
1020 dropAll [] ys = []
1022 imps top env (PApp _ f as)
1023 = do (decls, ns) <- get
1024 let isn = concatMap (namesIn uvars ist) (map getTm as)
1025 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1026 imps top env (PPi (Imp l _ doc _) n ty sc)
1027 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
1028 (decls , ns) <- get
1029 put (PImp (getPriority ist ty) True l n Placeholder doc : decls,
1030 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1031 imps True (n:env) sc
1032 imps top env (PPi (Exp l _ doc _) n ty sc)
1033 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1034 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1035 _ -> [])
1036 (decls, ns) <- get -- ignore decls in HO types
1037 put (PExp (getPriority ist ty) l Placeholder doc : decls,
1038 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1039 imps True (n:env) sc
1040 imps top env (PPi (Constraint l _ doc) n ty sc)
1041 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1042 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1043 _ -> [])
1044 (decls, ns) <- get -- ignore decls in HO types
1045 put (PConstraint 10 l Placeholder doc : decls,
1046 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1047 imps True (n:env) sc
1048 imps top env (PPi (TacImp l _ scr doc) n ty sc)
1049 = do let isn = nub (namesIn uvars ist ty ++ case sc of
1050 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
1051 _ -> [])
1052 (decls, ns) <- get -- ignore decls in HO types
1053 put (PTacImplicit 10 l n scr Placeholder doc : decls,
1054 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1055 imps True (n:env) sc
1056 imps top env (PEq _ l r)
1057 = do (decls, ns) <- get
1058 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1059 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1060 imps top env (PRewrite _ l r _)
1061 = do (decls, ns) <- get
1062 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1063 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1064 imps top env (PTyped l r)
1065 = imps top env l
1066 imps top env (PPair _ l r)
1067 = do (decls, ns) <- get
1068 let isn = namesIn uvars ist l ++ namesIn uvars ist r
1069 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1070 imps top env (PDPair _ (PRef _ n) t r)
1071 = do (decls, ns) <- get
1072 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
1073 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1074 imps top env (PDPair _ l t r)
1075 = do (decls, ns) <- get
1076 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1077 namesIn uvars ist r
1078 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
1079 imps top env (PAlternative a as)
1080 = do (decls, ns) <- get
1081 let isn = concatMap (namesIn uvars ist) as
1082 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
1083 imps top env (PLam n ty sc)
1084 = do imps False env ty
1085 imps False (n:env) sc
1086 imps top env (PHidden tm) = imps False env tm
1087 imps top env (PUnifyLog tm) = imps False env tm
1088 imps top env (PNoImplicits tm) = imps False env tm
1089 imps top env _ = return ()
1091 pibind using [] sc = sc
1092 pibind using (n:ns) sc
1093 = case lookup n using of
1094 Just ty -> PPi (Imp False Dynamic "" False) n ty (pibind using ns sc)
1095 Nothing -> PPi (Imp False Dynamic "" False) n Placeholder
1096 (pibind using ns sc)
1098-- Add implicit arguments in function calls
1099addImplPat :: IState -> PTerm -> PTerm
1100addImplPat = addImpl' True [] []
1102addImplBound :: IState -> [Name] -> PTerm -> PTerm
1103addImplBound ist ns = addImpl' False ns [] ist
1105addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
1106addImplBoundInf ist ns inf = addImpl' False ns inf ist
1108addImpl :: IState -> PTerm -> PTerm
1109addImpl = addImpl' False [] []
1111-- TODO: in patterns, don't add implicits to function names guarded by constructors
1112-- and *not* inside a PHidden
1114addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
1115addImpl' inpat env infns ist ptm
1116 = mkUniqueNames env (ai (zip env (repeat Nothing)) [] ptm)
1117 where
1118 ai env ds (PRef fc f)
1119 | f `elem` infns = PInferRef fc f
1120 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f ds []
1121 ai env ds (PHidden (PRef fc f))
1122 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f ds []
1123 ai env ds (PEq fc l r)
1124 = let l' = ai env ds l
1125 r' = ai env ds r in
1126 PEq fc l' r'
1127 ai env ds (PRewrite fc l r g)
1128 = let l' = ai env ds l
1129 r' = ai env ds r
1130 g' = fmap (ai env ds) g in
1131 PRewrite fc l' r' g'
1132 ai env ds (PTyped l r)
1133 = let l' = ai env ds l
1134 r' = ai env ds r in
1135 PTyped l' r'
1136 ai env ds (PPair fc l r)
1137 = let l' = ai env ds l
1138 r' = ai env ds r in
1139 PPair fc l' r'
1140 ai env ds (PDPair fc l t r)
1141 = let l' = ai env ds l
1142 t' = ai env ds t
1143 r' = ai env ds r in
1144 PDPair fc l' t' r'
1145 ai env ds (PAlternative a as)
1146 = let as' = map (ai env ds) as in
1147 PAlternative a as'
1148 ai env _ (PDisamb ds' as) = ai env ds' as
1149 ai env ds (PApp fc (PInferRef _ f) as)
1150 = let as' = map (fmap (ai env ds)) as in
1151 PApp fc (PInferRef fc f) as'
1152 ai env ds (PApp fc ftm@(PRef _ f) as)
1153 | f `elem` infns = ai env ds (PApp fc (PInferRef fc f) as)
1154 | not (f `elem` map fst env)
1155 = let as' = map (fmap (ai env ds)) as in
1156 handleErr $ aiFn inpat False ist fc f ds as'
1157 | Just (Just ty) <- lookup f env =
1158 let as' = map (fmap (ai env ds)) as
1159 arity = getPArity ty in
1160 mkPApp fc arity ftm as'
1161 ai env ds (PApp fc f as)
1162 = let f' = ai env ds f
1163 as' = map (fmap (ai env ds)) as in
1164 mkPApp fc 1 f' as'
1165 ai env ds (PCase fc c os)
1166 = let c' = ai env ds c
1167 os' = map (pmap (ai env ds)) os in
1168 PCase fc c' os'
1169 ai env ds (PLam n ty sc)
1170 = let ty' = ai env ds ty
1171 sc' = ai ((n, Just ty):env) ds sc in
1172 PLam n ty' sc'
1173 ai env ds (PLet n ty val sc)
1174 = let ty' = ai env ds ty
1175 val' = ai env ds val
1176 sc' = ai ((n, Just ty):env) ds sc in
1177 PLet n ty' val' sc'
1178 ai env ds (PPi p n ty sc)
1179 = let ty' = ai env ds ty
1180 sc' = ai ((n, Just ty):env) ds sc in
1181 PPi p n ty' sc'
1182 ai env ds (PGoal fc r n sc)
1183 = let r' = ai env ds r
1184 sc' = ai ((n, Nothing):env) ds sc in
1185 PGoal fc r' n sc'
1186 ai env ds (PHidden tm) = PHidden (ai env ds tm)
1187 ai env ds (PProof ts) = PProof (map (fmap (ai env ds)) ts)
1188 ai env ds (PTactics ts) = PTactics (map (fmap (ai env ds)) ts)
1189 ai env ds (PRefl fc tm) = PRefl fc (ai env ds tm)
1190 ai env ds (PUnifyLog tm) = PUnifyLog (ai env ds tm)
1191 ai env ds (PNoImplicits tm) = PNoImplicits (ai env ds tm)
1192 ai env ds tm = tm
1194 handleErr (Left err) = PElabError err
1195 handleErr (Right x) = x
1197-- if in a pattern, and there are no arguments, and there's no possible
1198-- names with zero explicit arguments, don't add implicits.
1200aiFn :: Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
1201aiFn inpat True ist fc f ds []
1202 = case lookupDef f (tt_ctxt ist) of
1203 [] -> Right $ PPatvar fc f
1204 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
1205 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
1206 if (not (vname f) || tcname f
1207 || any (conCaf (tt_ctxt ist)) ialts)
1208-- any constructor alts || any allImp ialts))
1209 then aiFn inpat False ist fc f ds [] -- use it as a constructor
1210 else Right $ PPatvar fc f
1211 where imp (PExp _ _ _ _) = False
1212 imp _ = True
1213-- allImp [] = False
1214 allImp xs = all imp xs
1215 constructor (TyDecl (DCon _ _) _) = True
1216 constructor _ = False
1218 conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
1220 vname (UN n) = True -- non qualified
1221 vname _ = False
1223aiFn inpat expat ist fc f ds as
1224 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1225aiFn inpat expat ist fc f ds as
1226 -- This is where namespaces get resolved by adding PAlternative
1227 = do let ns = lookupCtxtName f (idris_implicits ist)
1228 let nh = filter (\(n, _) -> notHidden n) ns
1229 let ns' = case trimAlts ds nh of
1230 [] -> nh
1231 x -> x
1232 case ns' of
1233 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1234 [] -> if f `elem` (map fst (idris_metavars ist))
1235 then Right $ PApp fc (PRef fc f) as
1236 else Right $ mkPApp fc (length as) (PRef fc f) as
1237 alts -> Right $
1238 PAlternative True $
1239 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1240 (insertImpl ns as)) alts
1241 where
1242 trimAlts [] alts = alts
1243 trimAlts ns alts
1244 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
1246 nspace (NS _ s) = s
1247 nspace _ = []
1249 notHidden n = case getAccessibility n of
1250 Hidden -> False
1251 _ -> True
1253 getAccessibility n
1254 = case lookupDefAcc n False (tt_ctxt ist) of
1255 [(n,t)] -> t
1256 _ -> Public
1259 insertImpl :: [PArg] -> [PArg] -> [PArg]
1260 insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =
1261 PExp p l tm d : insertImpl ps given
1262 insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =
1263 PConstraint p l tm d : insertImpl ps given
1264 insertImpl (PConstraint p l ty d : ps) given =
1265 PConstraint p l (PResolveTC fc) d : insertImpl ps given
1266 insertImpl (PImp p _ l n ty d : ps) given =
1267 case find n given [] of
1268 Just (tm, given') -> PImp p False l n tm "" : insertImpl ps given'
1269 Nothing -> PImp p True l n Placeholder "" : insertImpl ps given
1270 insertImpl (PTacImplicit p l n sc' ty d : ps) given =
1271 let sc = addImpl ist sc' in
1272 case find n given [] of
1273 Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'
1274 Nothing -> if inpat
1275 then PTacImplicit p l n sc Placeholder "" : insertImpl ps given
1276 else PTacImplicit p l n sc sc "" : insertImpl ps given
1277 insertImpl expected [] = []
1278 insertImpl _ given = given
1280 find n [] acc = Nothing
1281 find n (PImp _ _ _ n' t _ : gs) acc
1282 | n == n' = Just (t, reverse acc ++ gs)
1283 find n (PTacImplicit _ _ n' _ t _ : gs) acc
1284 | n == n' = Just (t, reverse acc ++ gs)
1285 find n (g : gs) acc = find n gs (g : acc)
1287-- replace non-linear occurrences with _
1288-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
1289-- it is hard to get right!
1291stripLinear :: IState -> PTerm -> PTerm
1292stripLinear i tm = evalState (sl tm) [] where
1293 sl :: PTerm -> State [Name] PTerm
1294 sl (PRef fc f)
1295 | (_:_) <- lookupTy f (tt_ctxt i)
1296 = return $ PRef fc f
1297 | otherwise = do ns <- get
1298 if (f `elem` ns)
1299 then return Placeholder
1300 else do put (f : ns)
1301 return (PRef fc f)
1302 sl (PPatvar fc f)
1303 = do ns <- get
1304 if (f `elem` ns)
1305 then return Placeholder
1306 else do put (f : ns)
1307 return (PPatvar fc f)
1308 sl (PApp fc fn args) = do fn' <- sl fn
1309 args' <- mapM slA args
1310 return $ PApp fc fn' args'
1311 where slA (PImp p m l n t d) = do t' <- sl t
1312 return $ PImp p m l n t' d
1313 slA (PExp p l t d) = do t' <- sl t
1314 return $ PExp p l t' d
1315 slA (PConstraint p l t d)
1316 = do t' <- sl t
1317 return $ PConstraint p l t' d
1318 slA (PTacImplicit p l n sc t d)
1319 = do t' <- sl t
1320 return $ PTacImplicit p l n sc t' d
1321 sl x = return x
1323-- Remove functions which aren't applied to anything, which must then
1324-- be resolved by unification. Assume names resolved and alternatives
1325-- filled in (so no ambiguity).
1327stripUnmatchable :: IState -> PTerm -> PTerm
1328stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1329 su :: PTerm -> PTerm
1330 su (PRef fc f)
1331 | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
1332 = Placeholder
1333 su (PApp fc fn args)
1334 = PApp fc fn (fmap (fmap su) args)
1335 su (PAlternative b alts)
1336 = let alts' = filter (/= Placeholder) (map su alts) in
1337 if null alts' then Placeholder
1338 else PAlternative b alts'
1339 su (PPair fc l r) = PPair fc (su l) (su r)
1340 su (PDPair fc l t r) = PDPair fc (su l) (su t) (su r)
1341 su t = t
1342stripUnmatchable i tm = tm
1344mkPApp fc a f [] = f
1345mkPApp fc a f as = let rest = drop a as in
1346 appRest fc (PApp fc f (take a as)) rest
1347 where
1348 appRest fc f [] = f
1349 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
1351-- Find 'static' argument positions
1352-- (the declared ones, plus any names in argument position in the declared
1353-- statics)
1354-- FIXME: It's possible that this really has to happen after elaboration
1356findStatics :: IState -> PTerm -> (PTerm, [Bool])
1357findStatics ist tm = trace (show tm) $
1358 let (ns, ss) = fs tm in
1359 runState (pos ns ss tm) []
1360 where fs (PPi p n t sc)
1361 | Static <- pstatic p
1362 = let (ns, ss) = fs sc in
1363 (namesIn [] ist t : ns, n : ss)
1364 | otherwise = let (ns, ss) = fs sc in
1365 (ns, ss)
1366 fs _ = ([], [])
1368 inOne n ns = length (filter id (map (elem n) ns)) == 1
1370 pos ns ss (PPi p n t sc)
1371 | elem n ss = do sc' <- pos ns ss sc
1372 spos <- get
1373 put (True : spos)
1374 return (PPi (p { pstatic = Static }) n t sc')
1375 | otherwise = do sc' <- pos ns ss sc
1376 spos <- get
1377 put (False : spos)
1378 return (PPi p n t sc')
1379 pos ns ss t = return t
1381-- for 6.12/7 compatibility
1382data EitherErr a b = LeftErr a | RightOK b
1384instance Monad (EitherErr a) where
1385 return = RightOK
1387 (LeftErr e) >>= k = LeftErr e
1388 RightOK v >>= k = k v
1390toEither (LeftErr e) = Left e
1391toEither (RightOK ho) = Right ho
1393-- syntactic match of a against b, returning pair of variables in a
1394-- and what they match. Returns the pair that failed if not a match.
1396matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1397matchClause = matchClause' False
1399matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
1400matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
1401 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
1403 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1404 fullApp x = x
1406 match' x y = match (fullApp x) (fullApp y)
1407 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
1408 | fi == txt "fromInteger" && b == txt "builtins",
1409 PConstant (I _) <- getTm x = match (getTm x) x'
1410 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
1411 | fi == txt "fromInteger" && b == txt "builtins",
1412 PConstant (I _) <- getTm x = match (getTm x) x'
1413 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
1414 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
1415 match (PApp _ f args) (PApp _ f' args')
1416 | length args == length args'
1417 = do mf <- match' f f'
1418 ms <- zipWithM matchArg args args'
1419 return (mf ++ concat ms)
1420-- match (PRef _ n) (PRef _ n') | n == n' = return []
1421-- | otherwise = Nothing
1422 match (PRef f n) (PApp _ x []) = match (PRef f n) x
1423 match (PPatvar f n) xr = match (PRef f n) xr
1424 match xr (PPatvar f n) = match xr (PRef f n)
1425 match (PApp _ x []) (PRef f n) = match x (PRef f n)
1426 match (PRef _ n) tm@(PRef _ n')
1427 | n == n' && not names &&
1428 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
1429 || tm == Placeholder)
1430 = return [(n, tm)]
1431 | n == n' = return []
1432 match (PRef _ n) tm
1433 | not names && (not (isConName n (tt_ctxt i) ||
1434 isFnName n (tt_ctxt i)) || tm == Placeholder)
1435 = return [(n, tm)]
1436 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1437 mr <- match' r r'
1438 return (ml ++ mr)
1439 match (PRewrite _ l r _) (PRewrite _ l' r' _)
1440 = do ml <- match' l l'
1441 mr <- match' r r'
1442 return (ml ++ mr)
1443 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1444 mr <- match r r'
1445 return (ml ++ mr)
1446 match (PTyped l r) x = match l x
1447 match x (PTyped l r) = match x l
1448 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1449 mr <- match' r r'
1450 return (ml ++ mr)
1451 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1452 mt <- match' t t'
1453 mr <- match' r r'
1454 return (ml ++ mt ++ mr)
1455 match (PAlternative a as) (PAlternative a' as')
1456 = do ms <- zipWithM match' as as'
1457 return (concat ms)
1458 match a@(PAlternative _ as) b
1459 = do let ms = zipWith match' as (repeat b)
1460 case (rights (map toEither ms)) of
1461 (x: _) -> return x
1462 _ -> LeftErr (a, b)
1463 match (PCase _ _ _) _ = return [] -- lifted out
1464 match (PMetavar _) _ = return [] -- modified
1465 match (PInferRef _ _) _ = return [] -- modified
1466 match (PQuote _) _ = return []
1467 match (PProof _) _ = return []
1468 match (PTactics _) _ = return []
1469 match (PRefl _ _) (PRefl _ _) = return []
1470 match (PResolveTC _) (PResolveTC _) = return []
1471 match (PTrue _) (PTrue _) = return []
1472 match (PFalse _) (PFalse _) = return []
1473 match (PReturn _) (PReturn _) = return []
1474 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1475 ms <- match' s s'
1476 return (mt ++ ms)
1477 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1478 ms <- match' s s'
1479 return (mt ++ ms)
1480 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1481 mty <- match' ty ty'
1482 ms <- match' s s'
1483 return (mt ++ mty ++ ms)
1484 match (PHidden x) (PHidden y) = match' x y
1485 match (PUnifyLog x) y = match' x y
1486 match x (PUnifyLog y) = match' x y
1487 match (PNoImplicits x) y = match' x y
1488 match x (PNoImplicits y) = match' x y
1489 match Placeholder _ = return []
1490 match _ Placeholder = return []
1491 match (PResolveTC _) _ = return []
1492 match a b | a == b = return []
1493 | otherwise = LeftErr (a, b)
1495 checkRpts (RightOK ms) = check ms where
1496 check ((n,t):xs)
1497 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1498 then Left (t, t')
1499 else check xs
1500 check (_:xs) = check xs
1501 check [] = Right ms
1502 checkRpts (LeftErr x) = Left x
1504substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1505substMatches ms = substMatchesShadow ms []
1507substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1508substMatchesShadow [] shs t = t
1509substMatchesShadow ((n,tm):ns) shs t
1510 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1512substMatch :: Name -> PTerm -> PTerm -> PTerm
1513substMatch n = substMatchShadow n []
1515substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1516substMatchShadow n shs tm t = sm shs t where
1517 sm xs (PRef _ n') | n == n' = tm
1518 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1519 sm xs (PPi p x t sc)
1520 | x `elem` xs
1521 = let x' = nextName x in
1522 PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
1523 (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
1524 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1525 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
1526 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1527 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1528 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
1529 (fmap (sm xs) tm)
1530 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1531 sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)
1532 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)
1533 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1534 sm xs (PHidden x) = PHidden (sm xs x)
1535 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
1536 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
1537 sm xs x = x
1539 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
1540 fullApp x = x
1542shadow :: Name -> Name -> PTerm -> PTerm
1543shadow n n' t = sm t where
1544 sm (PRef fc x) | n == x = PRef fc n'
1545 sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)
1546 sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1547 sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)
1548 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1549 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
1550 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1551 sm (PEq f x y) = PEq f (sm x) (sm y)
1552 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
1553 sm (PTyped x y) = PTyped (sm x) (sm y)
1554 sm (PPair f x y) = PPair f (sm x) (sm y)
1555 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1556 sm (PAlternative a as) = PAlternative a (map sm as)
1557 sm (PTactics ts) = PTactics (map (fmap sm) ts)
1558 sm (PProof ts) = PProof (map (fmap sm) ts)
1559 sm (PHidden x) = PHidden (sm x)
1560 sm (PUnifyLog x) = PUnifyLog (sm x)
1561 sm (PNoImplicits x) = PNoImplicits (sm x)
1562 sm x = x
1564-- Rename any binders which are repeated (so that we don't have to mess
1565-- about with shadowing anywhere else).
1567mkUniqueNames :: [Name] -> PTerm -> PTerm
1568mkUniqueNames env tm = evalState (mkUniq tm) env where
1569 inScope = boundNamesIn tm
1571 mkUniqA arg = do t' <- mkUniq (getTm arg)
1572 return (arg { getTm = t' })
1574 -- FIXME: Probably ought to do this for completeness! It's fine as
1575 -- long as there are no bindings inside tactics though.
1576 mkUniqT tac = return tac
1578 mkUniq :: PTerm -> State [Name] PTerm
1579 mkUniq (PLam n ty sc)
1580 = do env <- get
1581 (n', sc') <-
1582 if n `elem` env
1583 then do let n' = uniqueName n (env ++ inScope)
1584 return (n', shadow n n' sc)
1585 else return (n, sc)
1586 put (n' : env)
1587 ty' <- mkUniq ty
1588 sc'' <- mkUniq sc'
1589 return $! PLam n' ty' sc''
1590 mkUniq (PPi p n ty sc)
1591 = do env <- get
1592 (n', sc') <-
1593 if n `elem` env
1594 then do let n' = uniqueName n (env ++ inScope)
1595 return (n', shadow n n' sc)
1596 else return (n, sc)
1597 put (n' : env)
1598 ty' <- mkUniq ty
1599 sc'' <- mkUniq sc'
1600 return $! PPi p n' ty' sc''
1601 mkUniq (PLet n ty val sc)
1602 = do env <- get
1603 (n', sc') <-
1604 if n `elem` env
1605 then do let n' = uniqueName n (env ++ inScope)
1606 return (n', shadow n n' sc)
1607 else return (n, sc)
1608 put (n' : env)
1609 ty' <- mkUniq ty; val' <- mkUniq val
1610 sc'' <- mkUniq sc'
1611 return $! PLet n' ty' val' sc''
1612 mkUniq (PApp fc t args)
1613 = do t' <- mkUniq t
1614 args' <- mapM mkUniqA args
1615 return $! PApp fc t' args'
1616 mkUniq (PAppBind fc t args)
1617 = do t' <- mkUniq t
1618 args' <- mapM mkUniqA args
1619 return $! PAppBind fc t' args'
1620 mkUniq (PCase fc t alts)
1621 = do t' <- mkUniq t
1622 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
1623 return (x', y')) alts
1624 return $! PCase fc t' alts'
1625 mkUniq (PPair fc l r)
1626 = do l' <- mkUniq l; r' <- mkUniq r
1627 return $! PPair fc l' r'
1628 mkUniq (PDPair fc l t r)
1629 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
1630 return $! PDPair fc l' t' r'
1631 mkUniq (PAlternative b as)
1632 = liftM (PAlternative b) (mapM mkUniq as)
1633 mkUniq (PHidden t) = liftM PHidden (mkUniq t)
1634 mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
1635 mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
1636 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
1637 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
1638 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
1639 mkUniq t = return t