module Idris.AbsSyntax(module Idris.AbsSyntax, module Idris.AbsSyntaxTree) where
import Idris.Core.TT
import Idris.Core.Evaluate
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Typecheck
import Idris.AbsSyntaxTree
import Idris.Colours
import Idris.IdeSlave
import IRTS.CodegenCommon
import Util.DynamicLinker
import Paths_idris
import System.Console.Haskeline
import System.IO
import Control.Monad.State
import Control.Monad.Error(throwError)
import Data.List
import Data.Char
import qualified Data.Text as T
import Data.Either
import qualified Data.Map as M
import Data.Maybe
import qualified Data.Set as S
import Data.Word (Word)
import Debug.Trace
import Control.Monad.Error (throwError, catchError)
import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
import Util.Pretty
import Util.ScreenSize
import Util.System
getContext :: Idris Context
getContext = do i <- getIState; return (tt_ctxt i)
forCodegen :: Codegen -> [(Codegen, a)] -> [a]
forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']
getObjectFiles :: Codegen -> Idris [FilePath]
getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
addObjectFile :: Codegen -> FilePath -> Idris ()
addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ (tgt, f) : idris_objs i }
getLibs :: Codegen -> Idris [String]
getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)
addLib :: Codegen -> String -> Idris ()
addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ (tgt, f) : idris_libs i }
getFlags :: Codegen -> Idris [String]
getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)
addFlag :: Codegen -> String -> Idris ()
addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f) : idris_cgflags i }
addDyLib :: [String] -> Idris (Either DynamicLib String)
addDyLib libs = do i <- getIState
let ls = idris_dynamic_libs i
case mapMaybe (findDyLib ls) libs of
x:_ -> return (Left x)
[] -> do
handle <- lift . lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) $ libs
case msum handle of
Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
concat (intersperse "," libs) ++ "\"")
Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
return (Left x)
where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
findDyLib [] l = Nothing
findDyLib (lib:libs) l | l == lib_name lib = Just lib
| otherwise = findDyLib libs l
addHdr :: Codegen -> String -> Idris ()
addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
addLangExt :: LanguageExt -> Idris ()
addLangExt TypeProviders = do i <- getIState
putIState $ i {
idris_language_extensions = TypeProviders : idris_language_extensions i
}
addLangExt ErrorReflection = do i <- getIState
putIState $ i {
idris_language_extensions = ErrorReflection : idris_language_extensions i
}
addTrans :: (Term, Term) -> Idris ()
addTrans t = do i <- getIState
putIState $ i { idris_transforms = t : idris_transforms i }
addErrRev :: (Term, Term) -> Idris ()
addErrRev t = do i <- getIState
putIState $ i { idris_errRev = t : idris_errRev i }
totcheck :: (FC, Name) -> Idris ()
totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }
defer_totcheck :: (FC, Name) -> Idris ()
defer_totcheck n
= do i <- getIState;
putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }
clear_totcheck :: Idris ()
clear_totcheck = do i <- getIState; putIState $ i { idris_totcheck = [] }
setFlags :: Name -> [FnOpt] -> Idris ()
setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }
setAccessibility :: Name -> Accessibility -> Idris ()
setAccessibility n a
= do i <- getIState
let ctxt = setAccess n a (tt_ctxt i)
putIState $ i { tt_ctxt = ctxt }
setTotality :: Name -> Totality -> Idris ()
setTotality n a
= do i <- getIState
let ctxt = setTotal n a (tt_ctxt i)
putIState $ i { tt_ctxt = ctxt }
getTotality :: Name -> Idris Totality
getTotality n
= do i <- getIState
case lookupTotal n (tt_ctxt i) of
[t] -> return t
_ -> return (Total [])
getCoercionsTo :: IState -> Type -> [Name]
getCoercionsTo i ty =
let cs = idris_coercions i
(fn,_) = unApply (getRetTy ty) in
findCoercions fn cs
where findCoercions t [] = []
findCoercions t (n : ns) =
let ps = case lookupTy n (tt_ctxt i) of
[ty'] -> case unApply (getRetTy ty') of
(t', _) ->
if t == t' then [n] else []
_ -> [] in
ps ++ findCoercions t ns
addToCG :: Name -> CGInfo -> Idris ()
addToCG n cg
= do i <- getIState
putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()
addFunctionErrorHandlers f arg hs =
do i <- getIState
let oldHandlers = idris_function_errorhandlers i
let newHandlers = flip (addDef f) oldHandlers $
case lookupCtxtExact f oldHandlers of
Nothing -> M.singleton arg (S.fromList hs)
Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers
putIState $ i { idris_function_errorhandlers = newHandlers }
getFunctionErrorHandlers :: Name -> Name -> Idris [Name]
getFunctionErrorHandlers f arg = do i <- getIState
return . maybe [] S.toList $
undefined
getAllNames :: Name -> Idris [Name]
getAllNames n = allNames [] n
allNames :: [Name] -> Name -> Idris [Name]
allNames ns n | n `elem` ns = return []
allNames ns n = do i <- getIState
case lookupCtxtExact n (idris_callgraph i) of
Just ns' -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
return (nub (n : concat more))
_ -> return [n]
addCoercion :: Name -> Idris ()
addCoercion n = do i <- getIState
putIState $ i { idris_coercions = nub $ n : idris_coercions i }
addDocStr :: Name -> String -> Idris ()
addDocStr n doc
= do i <- getIState
putIState $ i { idris_docstrings = addDef n doc (idris_docstrings i) }
addNameHint :: Name -> Name -> Idris ()
addNameHint ty n
= do i <- getIState
ty' <- case lookupCtxtName ty (idris_implicits i) of
[(tyn, _)] -> return tyn
[] -> throwError (NoSuchVariable ty)
tyns -> throwError (CantResolveAlts (map show (map fst tyns)))
let ns' = case lookupCtxt ty' (idris_namehints i) of
[ns] -> ns ++ [n]
_ -> [n]
putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }
getNameHints :: IState -> Name -> [Name]
getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
getNameHints i n =
case lookupCtxt n (idris_namehints i) of
[ns] -> ns
_ -> []
addToCalledG :: Name -> [Name] -> Idris ()
addToCalledG n ns = return ()
addInstance :: Bool -> Name -> Name -> Idris ()
addInstance int n i
= do ist <- getIState
case lookupCtxt n (idris_classes ist) of
[CI a b c d e ins] ->
do let cs = addDef n (CI a b c d e (addI i ins)) (idris_classes ist)
putIState $ ist { idris_classes = cs }
_ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [i]) (idris_classes ist)
putIState $ ist { idris_classes = cs }
where addI i ins | int = i : ins
| chaser n = ins ++ [i]
| otherwise = insI i ins
insI i [] = [i]
insI i (n : ns) | chaser n = i : n : ns
| otherwise = n : insI i ns
chaser (UN nm)
| ('@':'@':_) <- str nm = True
chaser (NS n _) = chaser n
chaser _ = False
addClass :: Name -> ClassInfo -> Idris ()
addClass n i
= do ist <- getIState
let i' = case lookupCtxt n (idris_classes ist) of
[c] -> c { class_instances = class_instances i }
_ -> i
putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
addIBC :: IBCWrite -> Idris ()
addIBC ibc@(IBCDef n)
= do i <- getIState
when (notDef (ibc_write i)) $
putIState $ i { ibc_write = ibc : ibc_write i }
where notDef [] = True
notDef (IBCDef n': is) | n == n' = False
notDef (_ : is) = notDef is
addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }
clearIBC :: Idris ()
clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }
resetNameIdx :: Idris ()
resetNameIdx = do i <- getIState
put (i { idris_nameIdx = (0, emptyContext) })
addNameIdx :: Name -> Idris (Int, Name)
addNameIdx n = do i <- getIState
let (i', x) = addNameIdx' i n
return x
addNameIdx' :: IState -> Name -> (IState, (Int, Name))
addNameIdx' i n
= let idxs = snd (idris_nameIdx i) in
case lookupCtxt n idxs of
[x] -> (i, x)
_ -> let i' = fst (idris_nameIdx i) + 1 in
(i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))
getHdrs :: Codegen -> Idris [String]
getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
setErrLine :: Int -> Idris ()
setErrLine x = do i <- getIState;
case (errLine i) of
Nothing -> putIState $ i { errLine = Just x }
Just _ -> return ()
clearErr :: Idris ()
clearErr = do i <- getIState
putIState $ i { errLine = Nothing }
getSO :: Idris (Maybe String)
getSO = do i <- getIState
return (compiled_so i)
setSO :: Maybe String -> Idris ()
setSO s = do i <- getIState
putIState $ (i { compiled_so = s })
getIState :: Idris IState
getIState = get
putIState :: IState -> Idris ()
putIState = put
runIO :: IO a -> Idris a
runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
getName :: Idris Int
getName = do i <- getIState;
let idx = idris_name i;
putIState $ (i { idris_name = idx + 1 })
return idx
addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
addInternalApp fp l t
= do i <- getIState
putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })
getInternalApp :: FilePath -> Int -> Idris PTerm
getInternalApp fp l = do i <- getIState
case lookup (fp, l) (idris_lineapps i) of
Just n' -> return n'
Nothing -> return Placeholder
clearOrigPats :: Idris ()
clearOrigPats = do i <- get
let ps = idris_patdefs i
let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
put (i { idris_patdefs = ps' })
clearPTypes :: Idris ()
clearPTypes = do i <- get
let ctxt = tt_ctxt i
put (i { tt_ctxt = mapDefCtxt pErase ctxt })
where pErase (CaseOp c t tys orig tot cds)
= CaseOp c t tys orig [] (pErase' cds)
pErase x = x
pErase' (CaseDefs _ (cs, c) _ rs)
= let c' = (cs, fmap pEraseType c) in
CaseDefs c' c' c' rs
checkUndefined :: FC -> Name -> Idris ()
checkUndefined fc n
= do i <- getContext
case lookupTy n i of
(_:_) -> throwError . Msg $ show fc ++ ":" ++
show n ++ " already defined"
_ -> return ()
isUndefined :: FC -> Name -> Idris Bool
isUndefined fc n
= do i <- getContext
case lookupTy n i of
(_:_) -> return False
_ -> return True
setContext :: Context -> Idris ()
setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )
updateContext :: (Context -> Context) -> Idris ()
updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )
addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
addConstraints fc (v, cs)
= do i <- getIState
let ctxt = tt_ctxt i
let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
next_tvar = v }
let ics = zip cs (repeat fc) ++ idris_constraints i
putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
addDeferred = addDeferred' Ref
addDeferredTyCon = addDeferred' (TCon 0 0)
addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
addDeferred' nt ns
= do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns
i <- getIState
putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
idris_metavars i }
where tidyNames used (Bind (MN i x) b sc)
= let n' = uniqueName (UN x) used in
Bind n' b $ tidyNames (n':used) sc
tidyNames used (Bind n b sc)
= let n' = uniqueName n used in
Bind n' b $ tidyNames (n':used) sc
tidyNames used b = b
solveDeferred :: Name -> Idris ()
solveDeferred n = do i <- getIState
putIState $ i { idris_metavars =
filter (\(n', _) -> n/=n')
(idris_metavars i) }
getUndefined :: Idris [Name]
getUndefined = do i <- getIState
return (map fst (idris_metavars i) \\ primDefs)
getWidth :: Idris ConsoleWidth
getWidth = fmap idris_consolewidth getIState
setWidth :: ConsoleWidth -> Idris ()
setWidth w = do ist <- getIState
put ist { idris_consolewidth = w }
renderWidth :: Idris Int
renderWidth = do iw <- getWidth
case iw of
InfinitelyWide -> return 100000000
ColsWide n -> return (max n 1)
AutomaticWidth -> runIO getScreenWidth
iRender :: Doc a -> Idris (SimpleDoc a)
iRender d = do w <- getWidth
case w of
InfinitelyWide -> return $ renderPretty 1.0 1000000000 d
ColsWide n -> return $
if n < 1
then renderPretty 1.0 1000000000 d
else renderPretty 0.8 n d
AutomaticWidth -> do width <- runIO getScreenWidth
return $ renderPretty 0.8 width d
ihPrintResult :: Handle -> String -> Idris ()
ihPrintResult h s = do i <- getIState
case idris_outputmode i of
RawOutput -> case s of
"" -> return ()
s -> runIO $ hPutStrLn h s
IdeSlave n ->
let good = SexpList [SymbolAtom "ok", toSExp s] in
runIO $ hPutStrLn h $ convSExp "return" good n
consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
consoleDisplayAnnotated h output = do ist <- getIState
rendered <- iRender $ output
runIO . hPutStrLn h .
displayDecorated (consoleDecorate ist) $
rendered
ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
ideSlaveReturnAnnotated n h out = do ist <- getIState
(str, spans) <- fmap displaySpans .
iRender .
fmap (fancifyAnnots ist) $
out
let good = [SymbolAtom "ok", toSExp str, toSExp spans]
runIO . hPutStrLn h $ convSExp "return" good n
ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
ihPrintTermWithType h tm ty = do ist <- getIState
let output = tm <+> colon <+> ty
case idris_outputmode ist of
RawOutput -> consoleDisplayAnnotated h output
IdeSlave n -> ideSlaveReturnAnnotated n h output
ihPrintFunTypes :: Handle -> Name -> [(Name, PTerm)] -> Idris ()
ihPrintFunTypes h n [] = ihPrintError h $ "No such variable " ++ show n
ihPrintFunTypes h n overloads = do imp <- impShow
ist <- getIState
let output = vsep (map (uncurry (ppOverload imp)) overloads)
case idris_outputmode ist of
RawOutput -> consoleDisplayAnnotated h output
IdeSlave n -> ideSlaveReturnAnnotated n h output
where fullName n = annotate (AnnName n Nothing Nothing) $ text (show n)
ppOverload imp n tm = fullName n <+> colon <+> align (prettyImp imp tm)
ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()
ihRenderResult h d = do ist <- getIState
case idris_outputmode ist of
RawOutput -> consoleDisplayAnnotated h d
IdeSlave n -> ideSlaveReturnAnnotated n h d
fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
fancifyAnnots ist annot@(AnnName n _ _) =
do let ctxt = tt_ctxt ist
case () of
_ | isDConName n ctxt -> AnnName n (Just DataOutput) Nothing
_ | isFnName n ctxt -> AnnName n (Just FunOutput) Nothing
_ | isTConName n ctxt -> AnnName n (Just TypeOutput) Nothing
_ | otherwise -> annot
fancifyAnnots _ annot = annot
type1Doc :: Doc OutputAnnotation
type1Doc = (annotate AnnConstType $ text "Type 1")
ihPrintError :: Handle -> String -> Idris ()
ihPrintError h s = do i <- getIState
case idris_outputmode i of
RawOutput -> case s of
"" -> return ()
s -> runIO $ hPutStrLn h s
IdeSlave n ->
let good = SexpList [SymbolAtom "error", toSExp s] in
runIO . hPutStrLn h $ convSExp "return" good n
ihputStrLn :: Handle -> String -> Idris ()
ihputStrLn h s = do i <- getIState
case idris_outputmode i of
RawOutput -> runIO $ hPutStrLn h s
IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n
iputStrLn = ihputStrLn stdout
iPrintError = ihPrintError stdout
iPrintResult = ihPrintResult stdout
iWarn = ihWarn stdout
ideslavePutSExp :: SExpable a => String -> a -> Idris ()
ideslavePutSExp cmd info = do i <- getIState
case idris_outputmode i of
IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
_ -> return ()
iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
iputGoal g = do i <- getIState
case idris_outputmode i of
RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)
IdeSlave n -> runIO . putStrLn $
convSExp "write-goal" (displayS (fmap (fancifyAnnots i) g) "") n
isetPrompt :: String -> Idris ()
isetPrompt p = do i <- getIState
case idris_outputmode i of
IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n
ihWarn :: Handle -> FC -> String -> Idris ()
ihWarn h fc err = do i <- getIState
case idris_outputmode i of
RawOutput -> runIO $ hPutStrLn h (show fc ++ ":" ++ err)
IdeSlave n -> runIO $ hPutStrLn h $ convSExp "warning" (fc_fname fc, fc_line fc, fc_column fc, err) n
setLogLevel :: Int -> Idris ()
setLogLevel l = do i <- getIState
let opts = idris_options i
let opt' = opts { opt_logLevel = l }
putIState $ i { idris_options = opt' }
setCmdLine :: [Opt] -> Idris ()
setCmdLine opts = do i <- getIState
let iopts = idris_options i
putIState $ i { idris_options = iopts { opt_cmdline = opts } }
getCmdLine :: Idris [Opt]
getCmdLine = do i <- getIState
return (opt_cmdline (idris_options i))
getDumpDefun :: Idris (Maybe FilePath)
getDumpDefun = do i <- getIState
return $ findC (opt_cmdline (idris_options i))
where findC [] = Nothing
findC (DumpDefun x : _) = Just x
findC (_ : xs) = findC xs
getDumpCases :: Idris (Maybe FilePath)
getDumpCases = do i <- getIState
return $ findC (opt_cmdline (idris_options i))
where findC [] = Nothing
findC (DumpCases x : _) = Just x
findC (_ : xs) = findC xs
logLevel :: Idris Int
logLevel = do i <- getIState
return (opt_logLevel (idris_options i))
setErrContext :: Bool -> Idris ()
setErrContext t = do i <- getIState
let opts = idris_options i
let opt' = opts { opt_errContext = t }
putIState $ i { idris_options = opt' }
errContext :: Idris Bool
errContext = do i <- getIState
return (opt_errContext (idris_options i))
useREPL :: Idris Bool
useREPL = do i <- getIState
return (opt_repl (idris_options i))
setREPL :: Bool -> Idris ()
setREPL t = do i <- getIState
let opts = idris_options i
let opt' = opts { opt_repl = t }
putIState $ i { idris_options = opt' }
showOrigErr :: Idris Bool
showOrigErr = do i <- getIState
return (opt_origerr (idris_options i))
setShowOrigErr :: Bool -> Idris ()
setShowOrigErr b = do i <- getIState
let opts = idris_options i
let opt' = opts { opt_origerr = b }
putIState $ i { idris_options = opt' }
setNoBanner :: Bool -> Idris ()
setNoBanner n = do i <- getIState
let opts = idris_options i
let opt' = opts { opt_nobanner = n }
putIState $ i { idris_options = opt' }
getNoBanner :: Idris Bool
getNoBanner = do i <- getIState
let opts = idris_options i
return (opt_nobanner opts)
setQuiet :: Bool -> Idris ()
setQuiet q = do i <- getIState
let opts = idris_options i
let opt' = opts { opt_quiet = q }
putIState $ i { idris_options = opt' }
getQuiet :: Idris Bool
getQuiet = do i <- getIState
let opts = idris_options i
return (opt_quiet opts)
setCodegen :: Codegen -> Idris ()
setCodegen t = do i <- getIState
let opts = idris_options i
let opt' = opts { opt_codegen = t }
putIState $ i { idris_options = opt' }
codegen :: Idris Codegen
codegen = do i <- getIState
return (opt_codegen (idris_options i))
setOutputTy :: OutputType -> Idris ()
setOutputTy t = do i <- getIState
let opts = idris_options i
let opt' = opts { opt_outputTy = t }
putIState $ i { idris_options = opt' }
outputTy :: Idris OutputType
outputTy = do i <- getIState
return $ opt_outputTy $ idris_options i
setIdeSlave :: Bool -> Idris ()
setIdeSlave True = do i <- getIState
putIState $ i { idris_outputmode = (IdeSlave 0), idris_colourRepl = False }
setIdeSlave False = return ()
setTargetTriple :: String -> Idris ()
setTargetTriple t = do i <- getIState
let opts = idris_options i
opt' = opts { opt_triple = t }
putIState $ i { idris_options = opt' }
targetTriple :: Idris String
targetTriple = do i <- getIState
return (opt_triple (idris_options i))
setTargetCPU :: String -> Idris ()
setTargetCPU t = do i <- getIState
let opts = idris_options i
opt' = opts { opt_cpu = t }
putIState $ i { idris_options = opt' }
targetCPU :: Idris String
targetCPU = do i <- getIState
return (opt_cpu (idris_options i))
setOptLevel :: Word -> Idris ()
setOptLevel t = do i <- getIState
let opts = idris_options i
opt' = opts { opt_optLevel = t }
putIState $ i { idris_options = opt' }
optLevel :: Idris Word
optLevel = do i <- getIState
return (opt_optLevel (idris_options i))
verbose :: Idris Bool
verbose = do i <- getIState
return (opt_verbose (idris_options i))
setVerbose :: Bool -> Idris ()
setVerbose t = do i <- getIState
let opts = idris_options i
let opt' = opts { opt_verbose = t }
putIState $ i { idris_options = opt' }
typeInType :: Idris Bool
typeInType = do i <- getIState
return (opt_typeintype (idris_options i))
setTypeInType :: Bool -> Idris ()
setTypeInType t = do i <- getIState
let opts = idris_options i
let opt' = opts { opt_typeintype = t }
putIState $ i { idris_options = opt' }
coverage :: Idris Bool
coverage = do i <- getIState
return (opt_coverage (idris_options i))
setCoverage :: Bool -> Idris ()
setCoverage t = do i <- getIState
let opts = idris_options i
let opt' = opts { opt_coverage = t }
putIState $ i { idris_options = opt' }
setIBCSubDir :: FilePath -> Idris ()
setIBCSubDir fp = do i <- getIState
let opts = idris_options i
let opt' = opts { opt_ibcsubdir = fp }
putIState $ i { idris_options = opt' }
valIBCSubDir :: IState -> Idris FilePath
valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
addImportDir :: FilePath -> Idris ()
addImportDir fp = do i <- getIState
let opts = idris_options i
let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
putIState $ i { idris_options = opt' }
setImportDirs :: [FilePath] -> Idris ()
setImportDirs fps = do i <- getIState
let opts = idris_options i
let opt' = opts { opt_importdirs = fps }
putIState $ i { idris_options = opt' }
allImportDirs :: Idris [FilePath]
allImportDirs = do i <- getIState
let optdirs = opt_importdirs (idris_options i)
return ("." : reverse optdirs)
colourise :: Idris Bool
colourise = do i <- getIState
return $ idris_colourRepl i
setColourise :: Bool -> Idris ()
setColourise b = do i <- getIState
putIState $ i { idris_colourRepl = b }
setOutH :: Handle -> Idris ()
setOutH h = do i <- getIState
putIState $ i { idris_outh = h }
impShow :: Idris Bool
impShow = do i <- getIState
return (opt_showimp (idris_options i))
setImpShow :: Bool -> Idris ()
setImpShow t = do i <- getIState
let opts = idris_options i
let opt' = opts { opt_showimp = t }
putIState $ i { idris_options = opt' }
setColour :: ColourType -> IdrisColour -> Idris ()
setColour ct c = do i <- getIState
let newTheme = setColour' ct c (idris_colourTheme i)
putIState $ i { idris_colourTheme = newTheme }
where setColour' KeywordColour c t = t { keywordColour = c }
setColour' BoundVarColour c t = t { boundVarColour = c }
setColour' ImplicitColour c t = t { implicitColour = c }
setColour' FunctionColour c t = t { functionColour = c }
setColour' TypeColour c t = t { typeColour = c }
setColour' DataColour c t = t { dataColour = c }
setColour' PromptColour c t = t { promptColour = c }
logLvl :: Int -> String -> Idris ()
logLvl l str = do i <- getIState
let lvl = opt_logLevel (idris_options i)
when (lvl >= l) $
case idris_outputmode i of
RawOutput -> do runIO $ putStrLn str
IdeSlave n ->
do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
runIO $ putStrLn $ convSExp "log" good n
cmdOptType :: Opt -> Idris Bool
cmdOptType x = do i <- getIState
return $ x `elem` opt_cmdline (idris_options i)
iLOG :: String -> Idris ()
iLOG = logLvl 1
noErrors :: Idris Bool
noErrors = do i <- getIState
case errLine i of
Nothing -> return True
_ -> return False
setTypeCase :: Bool -> Idris ()
setTypeCase t = do i <- getIState
let opts = idris_options i
let opt' = opts { opt_typecase = t }
putIState $ i { idris_options = opt' }
expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
[Name] ->
[Name] ->
PTerm -> PTerm
expandParams dec ps ns infs tm = en tm
where
mkShadow (UN n) = MN 0 n
mkShadow (MN i n) = MN (i+1) n
mkShadow (NS x s) = NS (mkShadow x) s
en (PLam n t s)
| n `elem` (map fst ps ++ ns)
= let n' = mkShadow n in
PLam n' (en t) (en (shadow n n' s))
| otherwise = PLam n (en t) (en s)
en (PPi p n t s)
| n `elem` (map fst ps ++ ns)
= let n' = mkShadow n in
PPi p n' (en t) (en (shadow n n' s))
| otherwise = PPi p n (en t) (en s)
en (PLet n ty v s)
| n `elem` (map fst ps ++ ns)
= let n' = mkShadow n in
PLet n' (en ty) (en v) (en (shadow n n' s))
| otherwise = PLet n (en ty) (en v) (en s)
en (PDPair f (PRef f' n) t r)
| n `elem` (map fst ps ++ ns) && t /= Placeholder
= let n' = mkShadow n in
PDPair f (PRef f' n') (en t) (en (shadow n n' r))
en (PEq f l r) = PEq f (en l) (en r)
en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
en (PTyped l r) = PTyped (en l) (en r)
en (PPair f p l r) = PPair f p (en l) (en r)
en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
en (PAlternative a as) = PAlternative a (map en as)
en (PHidden t) = PHidden (en t)
en (PUnifyLog t) = PUnifyLog (en t)
en (PNoImplicits t) = PNoImplicits (en t)
en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
en (PProof ts) = PProof (map (fmap en) ts)
en (PTactics ts) = PTactics (map (fmap en) ts)
en (PQuote (Var n))
| n `nselem` ns = PQuote (Var (dec n))
en (PApp fc (PInferRef fc' n) as)
| n `nselem` ns = PApp fc (PInferRef fc' (dec n))
(map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
en (PApp fc (PRef fc' n) as)
| n `elem` infs = PApp fc (PInferRef fc' (dec n))
(map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
| n `nselem` ns = PApp fc (PRef fc' (dec n))
(map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
en (PAppBind fc (PRef fc' n) as)
| n `elem` infs = PAppBind fc (PInferRef fc' (dec n))
(map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
| n `nselem` ns = PAppBind fc (PRef fc' (dec n))
(map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
en (PRef fc n)
| n `elem` infs = PApp fc (PInferRef fc (dec n))
(map (pexp . (PRef fc)) (map fst ps))
| n `nselem` ns = PApp fc (PRef fc (dec n))
(map (pexp . (PRef fc)) (map fst ps))
en (PInferRef fc n)
| n `nselem` ns = PApp fc (PInferRef fc (dec n))
(map (pexp . (PRef fc)) (map fst ps))
en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
en t = t
nselem x [] = False
nselem x (y : xs) | nseq x y = True
| otherwise = nselem x xs
nseq x y = nsroot x == nsroot y
expandParamsD :: Bool ->
IState ->
(Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)
= if n `elem` ns && (not rhsonly)
then
PTy doc syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
else
PTy doc syn fc o n (expandParams dec ps ns [] ty)
expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
= if n `elem` ns && (not rhsonly)
then
PPostulate doc syn fc o (dec n) (piBind ps
(expandParams dec ps ns [] ty))
else
PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
= let n' = if n `elem` ns then dec n else n in
PClauses fc opts n' (map expandParamsC cs)
where
expandParamsC (PClause fc n lhs ws rhs ds)
= let
ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
n' = if n `elem` ns then dec n else n
ns' = removeBound lhs ns in
PClause fc n' lhs'
(map (expandParams dec ps'' ns' []) ws)
(expandParams dec ps'' ns' [] rhs)
(map (expandParamsD True ist dec ps'' ns') ds)
expandParamsC (PWith fc n lhs ws wval ds)
= let
ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
n' = if n `elem` ns then dec n else n
ns' = removeBound lhs ns in
PWith fc n' lhs'
(map (expandParams dec ps'' ns' []) ws)
(expandParams dec ps'' ns' [] wval)
(map (expandParamsD rhsonly ist dec ps'' ns') ds)
updateps yn nm [] = []
updateps yn nm (((a, t), i):as)
| (a `elem` nm) == yn = (a, t) : updateps yn nm as
| otherwise = (sMN i (show n ++ "_u"), t) : updateps yn nm as
removeBound lhs ns = ns \\ nub (bnames lhs)
bnames (PRef _ n) = [n]
bnames (PApp _ _ args) = concatMap bnames (map getTm args)
bnames (PPair _ _ l r) = bnames l ++ bnames r
bnames (PDPair _ l Placeholder r) = bnames l ++ bnames r
bnames _ = []
expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
= PData doc syn fc co (expandPData pd)
where
expandPData (PDatadecl n ty cons)
= if n `elem` ns
then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
(map econ cons)
else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
econ (doc, n, t, fc, fs)
= (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
expandParamsD rhs ist dec ps ns (PParams f params pds)
= PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
(map (expandParamsD True ist dec ps ns) pds)
expandParamsD rhs ist dec ps ns (PMutual f pds)
= PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
= PClass doc info f
(map (expandParams dec ps ns []) cs)
n
(map (mapsnd (expandParams dec ps ns [])) params)
(map (expandParamsD rhs ist dec ps ns) decls)
expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
= PInstance info f
(map (expandParams dec ps ns []) cs)
n
(map (expandParams dec ps ns []) params)
(expandParams dec ps ns [] ty)
cn
(map (expandParamsD rhs ist dec ps ns) decls)
expandParamsD rhs ist dec ps ns d = d
mapsnd f (x, t) = (x, f t)
getPriority :: IState -> PTerm -> Int
getPriority i tm = 1
where
pri (PRef _ n) =
case lookupP n (tt_ctxt i) of
((P (DCon _ _) _ _):_) -> 1
((P (TCon _ _) _ _):_) -> 1
((P Ref _ _):_) -> 1
[] -> 0
pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
pri (PTrue _ _) = 0
pri (PFalse _) = 0
pri (PRefl _ _) = 1
pri (PEq _ l r) = max 1 (max (pri l) (pri r))
pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
pri (PTyped l r) = pri l
pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))
pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
pri (PAlternative a as) = maximum (map pri as)
pri (PConstant _) = 0
pri Placeholder = 1
pri _ = 3
addStatics :: Name -> Term -> PTerm -> Idris ()
addStatics n tm ptm =
do let (statics, dynamics) = initStatics tm ptm
let stnames = nub $ concatMap freeArgNames (map snd statics)
let dnames = nub $ concatMap freeArgNames (map snd dynamics)
let statics' = nub $ map fst statics ++
filter (\x -> not (elem x dnames)) stnames
let stpos = staticList statics' tm
i <- getIState
when (not (null statics)) $
logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics
++ "\n" ++ show stnames ++ "\n" ++ show dnames
putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
addIBC (IBCStatic n)
where
initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
= let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
if pstatic p == Static then ((n, ty) : static, dynamic)
else if (not (searchArg p))
then (static, (n, ty) : dynamic)
else (static, dynamic)
initStatics t pt = ([], [])
freeArgNames (Bind n (Pi ty) sc)
= nub $ freeArgNames ty
freeArgNames tm = let (_, args) = unApply tm in
concatMap freeNames args
searchArg (Constraint _ _ _) = True
searchArg (TacImp _ _ _ _) = True
searchArg _ = False
staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
staticList _ _ = []
addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
addUsingConstraints syn fc t
= do ist <- get
let ns = namesIn [] ist t
let cs = getConstraints t
let addconsts = uconsts \\ cs
return (doAdd addconsts ns t)
where uconsts = filter uconst (using syn)
uconst (UConstraint _ _) = True
uconst _ = False
doAdd [] _ t = t
doAdd (UConstraint c args : cs) ns t
| all (\n -> elem n ns) args
= PPi (Constraint [] Dynamic "") (sMN 0 "cu")
(mkConst c args) (doAdd cs ns t)
| otherwise = doAdd cs ns t
mkConst c args = PApp fc (PRef fc c)
(map (\n -> PExp 0 [] (PRef fc n) "") args)
getConstraints (PPi (Constraint _ _ _) _ c sc)
= getcapp c ++ getConstraints sc
getConstraints (PPi _ _ c sc) = getConstraints sc
getConstraints _ = []
getcapp (PApp _ (PRef _ c) args)
= do ns <- mapM getName args
return (UConstraint c ns)
getcapp _ = []
getName (PExp _ _ (PRef _ n) _) = return n
getName _ = []
implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
implicit syn n ptm = implicit' syn [] n ptm
implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
implicit' syn ignore n ptm
= do i <- getIState
let (tm', impdata) = implicitise syn ignore i ptm
putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
addIBC (IBCImp n)
logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
return tm'
implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
implicitise syn ignore ist tm =
let (declimps, ns') = execState (imps True [] tm) ([], [])
ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
if null ns
then (tm, reverse declimps)
else implicitise syn ignore ist (pibind uvars nsOrder tm)
where
uvars = map ipair (filter uimplicit (using syn))
pvars = syn_params syn
inUsing n = n `elem` map fst uvars
ipair (UImplicit x y) = (x, y)
uimplicit (UImplicit _ _) = True
uimplicit _ = False
dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
| otherwise = x : dropAll xs ys
dropAll [] ys = []
imps top env (PApp _ f as)
= do (decls, ns) <- get
let isn = concatMap (namesIn uvars ist) (map getTm as)
put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
imps top env (PPi (Imp l _ doc _) n ty sc)
= do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
(decls , ns) <- get
put (PImp (getPriority ist ty) True l n Placeholder doc : decls,
nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
imps True (n:env) sc
imps top env (PPi (Exp l _ doc _) n ty sc)
= do let isn = nub (namesIn uvars ist ty ++ case sc of
(PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
_ -> [])
(decls, ns) <- get
put (PExp (getPriority ist ty) l Placeholder doc : decls,
nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
imps True (n:env) sc
imps top env (PPi (Constraint l _ doc) n ty sc)
= do let isn = nub (namesIn uvars ist ty ++ case sc of
(PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
_ -> [])
(decls, ns) <- get
put (PConstraint 10 l Placeholder doc : decls,
nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
imps True (n:env) sc
imps top env (PPi (TacImp l _ scr doc) n ty sc)
= do let isn = nub (namesIn uvars ist ty ++ case sc of
(PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
_ -> [])
(decls, ns) <- get
put (PTacImplicit 10 l n scr Placeholder doc : decls,
nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
imps True (n:env) sc
imps top env (PEq _ l r)
= do (decls, ns) <- get
let isn = namesIn uvars ist l ++ namesIn uvars ist r
put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
imps top env (PRewrite _ l r _)
= do (decls, ns) <- get
let isn = namesIn uvars ist l ++ namesIn uvars ist r
put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
imps top env (PTyped l r)
= imps top env l
imps top env (PPair _ _ l r)
= do (decls, ns) <- get
let isn = namesIn uvars ist l ++ namesIn uvars ist r
put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
imps top env (PDPair _ (PRef _ n) t r)
= do (decls, ns) <- get
let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
imps top env (PDPair _ l t r)
= do (decls, ns) <- get
let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
namesIn uvars ist r
put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
imps top env (PAlternative a as)
= do (decls, ns) <- get
let isn = concatMap (namesIn uvars ist) as
put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
imps top env (PLam n ty sc)
= do imps False env ty
imps False (n:env) sc
imps top env (PHidden tm) = imps False env tm
imps top env (PUnifyLog tm) = imps False env tm
imps top env (PNoImplicits tm) = imps False env tm
imps top env _ = return ()
pibind using [] sc = sc
pibind using (n:ns) sc
= case lookup n using of
Just ty -> PPi (Imp [] Dynamic "" False) n ty (pibind using ns sc)
Nothing -> PPi (Imp [] Dynamic "" False) n Placeholder
(pibind using ns sc)
addImplPat :: IState -> PTerm -> PTerm
addImplPat = addImpl' True [] []
addImplBound :: IState -> [Name] -> PTerm -> PTerm
addImplBound ist ns = addImpl' False ns [] ist
addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
addImplBoundInf ist ns inf = addImpl' False ns inf ist
addImpl :: IState -> PTerm -> PTerm
addImpl = addImpl' False [] []
addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
addImpl' inpat env infns ist ptm
= mkUniqueNames env (ai (zip env (repeat Nothing)) [] ptm)
where
ai env ds (PRef fc f)
| f `elem` infns = PInferRef fc f
| not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f ds []
ai env ds (PHidden (PRef fc f))
| not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f ds []
ai env ds (PEq fc l r)
= let l' = ai env ds l
r' = ai env ds r in
PEq fc l' r'
ai env ds (PRewrite fc l r g)
= let l' = ai env ds l
r' = ai env ds r
g' = fmap (ai env ds) g in
PRewrite fc l' r' g'
ai env ds (PTyped l r)
= let l' = ai env ds l
r' = ai env ds r in
PTyped l' r'
ai env ds (PPair fc p l r)
= let l' = ai env ds l
r' = ai env ds r in
PPair fc p l' r'
ai env ds (PDPair fc l t r)
= let l' = ai env ds l
t' = ai env ds t
r' = ai env ds r in
PDPair fc l' t' r'
ai env ds (PAlternative a as)
= let as' = map (ai env ds) as in
PAlternative a as'
ai env _ (PDisamb ds' as) = ai env ds' as
ai env ds (PApp fc (PInferRef _ f) as)
= let as' = map (fmap (ai env ds)) as in
PApp fc (PInferRef fc f) as'
ai env ds (PApp fc ftm@(PRef _ f) as)
| f `elem` infns = ai env ds (PApp fc (PInferRef fc f) as)
| not (f `elem` map fst env)
= let as' = map (fmap (ai env ds)) as in
handleErr $ aiFn inpat False ist fc f ds as'
| Just (Just ty) <- lookup f env =
let as' = map (fmap (ai env ds)) as
arity = getPArity ty in
mkPApp fc arity ftm as'
ai env ds (PApp fc f as)
= let f' = ai env ds f
as' = map (fmap (ai env ds)) as in
mkPApp fc 1 f' as'
ai env ds (PCase fc c os)
= let c' = ai env ds c
os' = map (pmap (ai env ds)) os in
PCase fc c' os'
ai env ds (PLam n ty sc)
= let ty' = ai env ds ty
sc' = ai ((n, Just ty):env) ds sc in
PLam n ty' sc'
ai env ds (PLet n ty val sc)
= let ty' = ai env ds ty
val' = ai env ds val
sc' = ai ((n, Just ty):env) ds sc in
PLet n ty' val' sc'
ai env ds (PPi p n ty sc)
= let ty' = ai env ds ty
sc' = ai ((n, Just ty):env) ds sc in
PPi p n ty' sc'
ai env ds (PGoal fc r n sc)
= let r' = ai env ds r
sc' = ai ((n, Nothing):env) ds sc in
PGoal fc r' n sc'
ai env ds (PHidden tm) = PHidden (ai env ds tm)
ai env ds (PProof ts) = PProof (map (fmap (ai env ds)) ts)
ai env ds (PTactics ts) = PTactics (map (fmap (ai env ds)) ts)
ai env ds (PRefl fc tm) = PRefl fc (ai env ds tm)
ai env ds (PUnifyLog tm) = PUnifyLog (ai env ds tm)
ai env ds (PNoImplicits tm) = PNoImplicits (ai env ds tm)
ai env ds tm = tm
handleErr (Left err) = PElabError err
handleErr (Right x) = x
aiFn :: Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
aiFn inpat True ist fc f ds []
= case lookupDef f (tt_ctxt ist) of
[] -> Right $ PPatvar fc f
alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
if (not (vname f) || tcname f
|| any (conCaf (tt_ctxt ist)) ialts)
then aiFn inpat False ist fc f ds []
else Right $ PPatvar fc f
where imp (PExp _ _ _ _) = False
imp _ = True
allImp xs = all imp xs
constructor (TyDecl (DCon _ _) _) = True
constructor _ = False
conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia
vname (UN n) = True
vname _ = False
aiFn inpat expat ist fc f ds as
| f `elem` primNames = Right $ PApp fc (PRef fc f) as
aiFn inpat expat ist fc f ds as
= do let ns = lookupCtxtName f (idris_implicits ist)
let nh = filter (\(n, _) -> notHidden n) ns
let ns' = case trimAlts ds nh of
[] -> nh
x -> x
case ns' of
[(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
[] -> if f `elem` (map fst (idris_metavars ist))
then Right $ PApp fc (PRef fc f) as
else Right $ mkPApp fc (length as) (PRef fc f) as
alts -> Right $
PAlternative True $
map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
(insertImpl ns as)) alts
where
trimAlts [] alts = alts
trimAlts ns alts
= filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
nspace (NS _ s) = s
nspace _ = []
notHidden n = case getAccessibility n of
Hidden -> False
_ -> True
getAccessibility n
= case lookupDefAcc n False (tt_ctxt ist) of
[(n,t)] -> t
_ -> Public
insertImpl :: [PArg] -> [PArg] -> [PArg]
insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =
PExp p l tm d : insertImpl ps given
insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =
PConstraint p l tm d : insertImpl ps given
insertImpl (PConstraint p l ty d : ps) given =
PConstraint p l (PResolveTC fc) d : insertImpl ps given
insertImpl (PImp p _ l n ty d : ps) given =
case find n given [] of
Just (tm, given') -> PImp p False l n tm "" : insertImpl ps given'
Nothing -> PImp p True l n Placeholder "" : insertImpl ps given
insertImpl (PTacImplicit p l n sc' ty d : ps) given =
let sc = addImpl ist sc' in
case find n given [] of
Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'
Nothing -> if inpat
then PTacImplicit p l n sc Placeholder "" : insertImpl ps given
else PTacImplicit p l n sc sc "" : insertImpl ps given
insertImpl expected [] = []
insertImpl _ given = given
find n [] acc = Nothing
find n (PImp _ _ _ n' t _ : gs) acc
| n == n' = Just (t, reverse acc ++ gs)
find n (PTacImplicit _ _ n' _ t _ : gs) acc
| n == n' = Just (t, reverse acc ++ gs)
find n (g : gs) acc = find n gs (g : acc)
stripLinear :: IState -> PTerm -> PTerm
stripLinear i tm = evalState (sl tm) [] where
sl :: PTerm -> State [Name] PTerm
sl (PRef fc f)
| (_:_) <- lookupTy f (tt_ctxt i)
= return $ PRef fc f
| otherwise = do ns <- get
if (f `elem` ns)
then return Placeholder
else do put (f : ns)
return (PRef fc f)
sl (PPatvar fc f)
= do ns <- get
if (f `elem` ns)
then return Placeholder
else do put (f : ns)
return (PPatvar fc f)
sl (PApp fc fn args) = do fn' <- sl fn
args' <- mapM slA args
return $ PApp fc fn' args'
where slA (PImp p m l n t d) = do t' <- sl t
return $ PImp p m l n t' d
slA (PExp p l t d) = do t' <- sl t
return $ PExp p l t' d
slA (PConstraint p l t d)
= do t' <- sl t
return $ PConstraint p l t' d
slA (PTacImplicit p l n sc t d)
= do t' <- sl t
return $ PTacImplicit p l n sc t' d
sl x = return x
stripUnmatchable :: IState -> PTerm -> PTerm
stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
su :: PTerm -> PTerm
su (PRef fc f)
| (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i)
= Placeholder
su (PApp fc fn args)
= PApp fc fn (fmap (fmap su) args)
su (PAlternative b alts)
= let alts' = filter (/= Placeholder) (map su alts) in
if null alts' then Placeholder
else PAlternative b alts'
su (PPair fc p l r) = PPair fc p (su l) (su r)
su (PDPair fc l t r) = PDPair fc (su l) (su t) (su r)
su t = t
stripUnmatchable i tm = tm
mkPApp fc a f [] = f
mkPApp fc a f as = let rest = drop a as in
appRest fc (PApp fc f (take a as)) rest
where
appRest fc f [] = f
appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
findStatics :: IState -> PTerm -> (PTerm, [Bool])
findStatics ist tm = trace (show tm) $
let (ns, ss) = fs tm in
runState (pos ns ss tm) []
where fs (PPi p n t sc)
| Static <- pstatic p
= let (ns, ss) = fs sc in
(namesIn [] ist t : ns, n : ss)
| otherwise = let (ns, ss) = fs sc in
(ns, ss)
fs _ = ([], [])
inOne n ns = length (filter id (map (elem n) ns)) == 1
pos ns ss (PPi p n t sc)
| elem n ss = do sc' <- pos ns ss sc
spos <- get
put (True : spos)
return (PPi (p { pstatic = Static }) n t sc')
| otherwise = do sc' <- pos ns ss sc
spos <- get
put (False : spos)
return (PPi p n t sc')
pos ns ss t = return t
data EitherErr a b = LeftErr a | RightOK b
instance Monad (EitherErr a) where
return = RightOK
(LeftErr e) >>= k = LeftErr e
RightOK v >>= k = k v
toEither (LeftErr e) = Left e
toEither (RightOK ho) = Right ho
matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
matchClause = matchClause' False
matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
fullApp x = x
match' x y = match (fullApp x) (fullApp y)
match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
| fi == txt "fromInteger" && b == txt "builtins",
PConstant (I _) <- getTm x = match (getTm x) x'
match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
| fi == txt "fromInteger" && b == txt "builtins",
PConstant (I _) <- getTm x = match (getTm x) x'
match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
match (PApp _ f args) (PApp _ f' args')
| length args == length args'
= do mf <- match' f f'
ms <- zipWithM matchArg args args'
return (mf ++ concat ms)
match (PRef f n) (PApp _ x []) = match (PRef f n) x
match (PPatvar f n) xr = match (PRef f n) xr
match xr (PPatvar f n) = match xr (PRef f n)
match (PApp _ x []) (PRef f n) = match x (PRef f n)
match (PRef _ n) tm@(PRef _ n')
| n == n' && not names &&
(not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
|| tm == Placeholder)
= return [(n, tm)]
| n == n' = return []
match (PRef _ n) tm
| not names && (not (isConName n (tt_ctxt i) ||
isFnName n (tt_ctxt i)) || tm == Placeholder)
= return [(n, tm)]
match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
mr <- match' r r'
return (ml ++ mr)
match (PRewrite _ l r _) (PRewrite _ l' r' _)
= do ml <- match' l l'
mr <- match' r r'
return (ml ++ mr)
match (PTyped l r) (PTyped l' r') = do ml <- match l l'
mr <- match r r'
return (ml ++ mr)
match (PTyped l r) x = match l x
match x (PTyped l r) = match x l
match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
mr <- match' r r'
return (ml ++ mr)
match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
mt <- match' t t'
mr <- match' r r'
return (ml ++ mt ++ mr)
match (PAlternative a as) (PAlternative a' as')
= do ms <- zipWithM match' as as'
return (concat ms)
match a@(PAlternative _ as) b
= do let ms = zipWith match' as (repeat b)
case (rights (map toEither ms)) of
(x: _) -> return x
_ -> LeftErr (a, b)
match (PCase _ _ _) _ = return []
match (PMetavar _) _ = return []
match (PInferRef _ _) _ = return []
match (PQuote _) _ = return []
match (PProof _) _ = return []
match (PTactics _) _ = return []
match (PRefl _ _) (PRefl _ _) = return []
match (PResolveTC _) (PResolveTC _) = return []
match (PTrue _ _) (PTrue _ _) = return []
match (PFalse _) (PFalse _) = return []
match (PReturn _) (PReturn _) = return []
match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
ms <- match' s s'
return (mt ++ ms)
match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
ms <- match' s s'
return (mt ++ ms)
match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
mty <- match' ty ty'
ms <- match' s s'
return (mt ++ mty ++ ms)
match (PHidden x) (PHidden y) = match' x y
match (PUnifyLog x) y = match' x y
match x (PUnifyLog y) = match' x y
match (PNoImplicits x) y = match' x y
match x (PNoImplicits y) = match' x y
match Placeholder _ = return []
match _ Placeholder = return []
match (PResolveTC _) _ = return []
match a b | a == b = return []
| otherwise = LeftErr (a, b)
checkRpts (RightOK ms) = check ms where
check ((n,t):xs)
| Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
then Left (t, t')
else check xs
check (_:xs) = check xs
check [] = Right ms
checkRpts (LeftErr x) = Left x
substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
substMatches ms = substMatchesShadow ms []
substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
substMatchesShadow [] shs t = t
substMatchesShadow ((n,tm):ns) shs t
= substMatchShadow n shs tm (substMatchesShadow ns shs t)
substMatch :: Name -> PTerm -> PTerm -> PTerm
substMatch n = substMatchShadow n []
substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
substMatchShadow n shs tm t = sm shs t where
sm xs (PRef _ n') | n == n' = tm
sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
sm xs (PPi p x t sc)
| x `elem` xs
= let x' = nextName x in
PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
(sm (x':xs) (substMatch x (PRef emptyFC x') sc))
| otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
(fmap (sm xs) tm)
sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)
sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
sm xs (PHidden x) = PHidden (sm xs x)
sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
sm xs x = x
fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
fullApp x = x
shadow :: Name -> Name -> PTerm -> PTerm
shadow n n' t = sm t where
sm (PRef fc x) | n == x = PRef fc n'
sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)
sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)
sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
sm (PEq f x y) = PEq f (sm x) (sm y)
sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
sm (PTyped x y) = PTyped (sm x) (sm y)
sm (PPair f p x y) = PPair f p (sm x) (sm y)
sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
sm (PAlternative a as) = PAlternative a (map sm as)
sm (PTactics ts) = PTactics (map (fmap sm) ts)
sm (PProof ts) = PProof (map (fmap sm) ts)
sm (PHidden x) = PHidden (sm x)
sm (PUnifyLog x) = PUnifyLog (sm x)
sm (PNoImplicits x) = PNoImplicits (sm x)
sm x = x
mkUniqueNames :: [Name] -> PTerm -> PTerm
mkUniqueNames env tm = evalState (mkUniq tm) env where
inScope = boundNamesIn tm
mkUniqA arg = do t' <- mkUniq (getTm arg)
return (arg { getTm = t' })
mkUniqT tac = return tac
mkUniq :: PTerm -> State [Name] PTerm
mkUniq (PLam n ty sc)
= do env <- get
(n', sc') <-
if n `elem` env
then do let n' = uniqueName n (env ++ inScope)
return (n', shadow n n' sc)
else return (n, sc)
put (n' : env)
ty' <- mkUniq ty
sc'' <- mkUniq sc'
return $! PLam n' ty' sc''
mkUniq (PPi p n ty sc)
= do env <- get
(n', sc') <-
if n `elem` env
then do let n' = uniqueName n (env ++ inScope)
return (n', shadow n n' sc)
else return (n, sc)
put (n' : env)
ty' <- mkUniq ty
sc'' <- mkUniq sc'
return $! PPi p n' ty' sc''
mkUniq (PLet n ty val sc)
= do env <- get
(n', sc') <-
if n `elem` env
then do let n' = uniqueName n (env ++ inScope)
return (n', shadow n n' sc)
else return (n, sc)
put (n' : env)
ty' <- mkUniq ty; val' <- mkUniq val
sc'' <- mkUniq sc'
return $! PLet n' ty' val' sc''
mkUniq (PApp fc t args)
= do t' <- mkUniq t
args' <- mapM mkUniqA args
return $! PApp fc t' args'
mkUniq (PAppBind fc t args)
= do t' <- mkUniq t
args' <- mapM mkUniqA args
return $! PAppBind fc t' args'
mkUniq (PCase fc t alts)
= do t' <- mkUniq t
alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
return (x', y')) alts
return $! PCase fc t' alts'
mkUniq (PPair fc p l r)
= do l' <- mkUniq l; r' <- mkUniq r
return $! PPair fc p l' r'
mkUniq (PDPair fc l t r)
= do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
return $! PDPair fc l' t' r'
mkUniq (PAlternative b as)
= liftM (PAlternative b) (mapM mkUniq as)
mkUniq (PHidden t) = liftM PHidden (mkUniq t)
mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
mkUniq t = return t