{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor, TypeSynonymInstances, PatternGuards #-} 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.Docstrings import Idris.IdeSlave hiding (Opt(..)) 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 let importdirs = opt_importdirs (idris_options i) case mapMaybe (findDyLib ls) libs of x:_ -> return (Left x) [] -> do handle <- lift . lift . mapM (\l -> catchIO (tryLoadLib importdirs 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 } addImported :: FilePath -> Idris () addImported f = do i <- getIState putIState $ i { idris_imported = nub $ f : idris_imported 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 []) -- Get coercions which might return the required type 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) } addTyInferred :: Name -> Idris () addTyInferred n = do i <- getIState putIState $ i { idris_tyinfodata = addDef n TIPartial (idris_tyinfodata i) } addTyInfConstraints :: FC -> [(Term, Term)] -> Idris () addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts mapM_ addConstraint ts return () where addConstraint (x, y) = findMVApps x y findMVApps x y = do let (fx, argsx) = unApply x let (fy, argsy) = unApply y if (not (fx == fy)) then do tryAddMV fx y tryAddMV fy x else mapM_ addConstraint (zip argsx argsy) tryAddMV (P _ mv _) y = do ist <- get case lookup mv (idris_metavars ist) of Just _ -> addConstraintRule mv y _ -> return () tryAddMV _ _ = return () addConstraintRule :: Name -> Term -> Idris () addConstraintRule n t = do ist <- get logLvl 1 $ "TI constraint: " ++ show (n, t) case lookupCtxt n (idris_tyinfodata ist) of [TISolution ts] -> do mapM_ (checkConsistent t) ts let ti' = addDef n (TISolution (t : ts)) (idris_tyinfodata ist) put $ ist { idris_tyinfodata = ti' } _ -> do let ti' = addDef n (TISolution [t]) (idris_tyinfodata ist) put $ ist { idris_tyinfodata = ti' } -- Check a solution is consistent with previous solutions -- Meaning: If heads are both data types, they had better be the -- same. checkConsistent :: Term -> Term -> Idris () checkConsistent x y = do let (fx, _) = unApply x let (fy, _) = unApply y case (fx, fy) of (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n) (P (TCon _ _) n _, Constant _) -> errWhen True (Constant _, P (TCon _ _) n' _) -> errWhen True (P (DCon _ _) n _, P (DCon _ _) n' _) -> errWhen (n/=n) _ -> return () where errWhen True = throwError (At fc (CantUnify False x y (Msg "") [] 0)) errWhen False = return () isTyInferred :: Name -> Idris Bool isTyInferred n = do i <- getIState case lookupCtxt n (idris_tyinfodata i) of [TIPartial] -> return True _ -> return False -- | Adds error handlers for a particular function and argument. If names are -- ambiguous, all matching handlers are updated. 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 -- will always be one of those two, thus no extra case putIState $ i { idris_function_errorhandlers = newHandlers } getFunctionErrorHandlers :: Name -> Name -> Idris [Name] getFunctionErrorHandlers f arg = do i <- getIState return . maybe [] S.toList $ undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i) -- Trace all the names in a call graph starting at the given name 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 -> Docstring -> [(Name, Docstring)] -> Idris () addDocStr n doc args = do i <- getIState putIState $ i { idris_docstrings = addDef n (doc, args) (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 () -- TODO -- Add a class instance function. Dodgy hack: Put integer instances first in the -- list so they are resolved by default. -- Dodgy hack 2: put constraint chasers (@@) last 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) }) -- Used to preserve sharing of names 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) getImported :: Idris [FilePath] getImported = do i <- getIState; return (idris_imported i) setErrSpan :: FC -> Idris () setErrSpan x = do i <- getIState; case (errSpan i) of Nothing -> putIState $ i { errSpan = Just x } Just _ -> return () clearErr :: Idris () clearErr = do i <- getIState putIState $ i { errSpan = 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 -- | A version of liftIO that puts errors into the exception type of the Idris monad runIO :: IO a -> Idris a runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return -- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist" getName :: Idris Int getName = do i <- getIState; let idx = idris_name i; putIState $ (i { idris_name = idx + 1 }) return idx -- InternalApp keeps track of the real function application for making case splits from, not the application the -- programmer wrote, which doesn't have the whole context in any case other than top level definitions 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 -- TODO: What if it's not there? -- Pattern definitions are only used for coverage checking, so erase them -- when we're done clearOrigPats :: Idris () clearOrigPats = do i <- get let ps = idris_patdefs i let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps put (i { idris_patdefs = ps' }) -- Erase types from Ps in the context (basically ending up with what's in -- the .ibc, which is all we need after all the analysis is done) 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 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) 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), ibc_write = filter (notMV n) (ibc_write i) } where notMV n (IBCMetavar n') = not (n == n') notMV n _ = True getUndefined :: Idris [Name] getUndefined = do i <- getIState return (map fst (idris_metavars i) \\ primDefs) isMetavarName :: Name -> IState -> Bool isMetavarName n ist = case lookupNames n (tt_ctxt ist) of (t:_) -> isJust $ lookup t (idris_metavars ist) _ -> False 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 type1Doc :: Doc OutputAnnotation type1Doc = (annotate AnnConstType $ text "Type 1") isetPrompt :: String -> Idris () isetPrompt p = do i <- getIState case idris_outputmode i of IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p 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' } setAutoSolve :: Bool -> Idris () setAutoSolve b = do i <- getIState let opts = idris_options i let opt' = opts { opt_autoSolve = 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 errSpan 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' } -- Dealing with parameters expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> -- all names [Name] -> -- names with no declaration PTerm -> PTerm expandParams dec ps ns infs tm = en tm where -- if we shadow a name (say in a lambda binding) that is used in a call to -- a lifted function, we need access to both names - once in the scope of the -- binding and once to call the lifted functions. So we'll explicitly shadow -- it. (Yes, it's a hack. The alternative would be to resolve names earlier -- but we didn't...) 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) -- FIXME: Should only do this in a type signature! en (PDPair f p (PRef f' n) t r) | n `elem` (map fst ps ++ ns) && t /= Placeholder = let n' = mkShadow n in PDPair f p (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 p l t r) = PDPair f p (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 (PDisamb ds t) = PDisamb ds (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 -> -- True = RHS only IState -> (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty) = if n `elem` ns && (not rhsonly) then -- trace (show (n, expandParams dec ps ns ty)) $ PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty)) else --trace (show (n, expandParams dec ps ns ty)) $ PTy doc argdocs 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 -- trace (show (n, expandParams dec ps ns ty)) $ PPostulate doc syn fc o (dec n) (piBind ps (expandParams dec ps ns [] ty)) else --trace (show (n, expandParams dec ps ns ty)) $ 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 True (namesIn ist rhs) (zip ps [0..]) 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 -- names bound on the lhs should not be expanded on the rhs 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 True (namesIn ist wval) (zip ps [0..]) 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 argDocs syn fc co pd) = PData doc argDocs syn fc co (expandPData pd) where -- just do the type decl, leave constructors alone (parameters will be -- added implicitly) 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, argDocs, n, t, fc, fs) = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs) expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty cdoc cn cty) = if tn `elem` ns then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty)) cdoc (dec cn) conty else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty) cdoc (dec cn) conty where conty = piBindp expl ps (expandParams dec ps ns [] cty) 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) -- (map (expandParamsD 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) -- Calculate a priority for a type, for deciding elaboration order -- * if it's just a type variable or concrete type, do it early (0) -- * if there's only type variables and injective constructors, do it next (1) -- * if there's a function type, next (2) -- * finally, everything else (3) getPriority :: IState -> PTerm -> Int getPriority i tm = 1 -- pri tm where pri (PRef _ n) = case lookupP n (tt_ctxt i) of ((P (DCon _ _) _ _):_) -> 1 ((P (TCon _ _) _ _):_) -> 1 ((P Ref _ _):_) -> 1 [] -> 0 -- must be locally bound, if it's not an error... 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) -- also get the arguments which are 'uniquely inferrable' from -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine") 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 -- if a name appears in a type class or tactic implicit index, it doesn't -- affect its 'uniquely inferrable' from a static status since these are -- resolved by searching. searchArg (Constraint _ _) = True searchArg (TacImp _ _ _) = True searchArg _ = False staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc staticList _ _ = [] -- Dealing with implicit arguments -- Add constraint bindings from using block addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm addUsingConstraints syn fc t = do ist <- get let ns = namesIn [] ist t let cs = getConstraints t -- check declared constraints let addconsts = uconsts \\ cs -- if all names in the arguments of addconsts appear in ns, -- add the constraint implicitly return (doAdd addconsts ns t) where uconsts = filter uconst (using syn) uconst (UConstraint _ _) = True uconst _ = False doAdd [] _ t = t -- if all of args in ns, then add it 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 _ = [] -- Add implicit Pi bindings for any names in the term which appear in an -- argument position. -- This has become a right mess already. Better redo it some time... 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 -- let (tm'', spos) = findStatics i tm' putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) } addIBC (IBCImp n) logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata) -- i <- get -- putIState $ i { idris_statics = addDef n spos (idris_statics i) } return tm' implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg]) implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True 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 = [] -- Find names in argument position in a type, suitable for implicit -- binding -- Not the function position, but do everything else... implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv) (map getTm args) implNamesIn uv t = namesIn uv ist t 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 _ _) n ty sc) = do let isn = nub (implNamesIn uvars ty) `dropAll` [n] (decls , ns) <- get put (PImp (getPriority ist ty) True l n Placeholder : decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls))))) imps True (n:env) sc imps top env (PPi (Exp l _ _) n ty sc) = do let isn = nub (implNamesIn uvars ty ++ case sc of (PRef _ x) -> namesIn uvars ist sc `dropAll` [n] _ -> []) (decls, ns) <- get -- ignore decls in HO types put (PExp (getPriority ist ty) l Placeholder : decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls))))) imps True (n:env) sc imps top env (PPi (Constraint l _) n ty sc) = do let isn = nub (implNamesIn uvars ty ++ case sc of (PRef _ x) -> namesIn uvars ist sc `dropAll` [n] _ -> []) (decls, ns) <- get -- ignore decls in HO types put (PConstraint 10 l Placeholder : decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls))))) imps True (n:env) sc imps top env (PPi (TacImp l _ scr) n ty sc) = do let isn = nub (implNamesIn uvars ty ++ case sc of (PRef _ x) -> namesIn uvars ist sc `dropAll` [n] _ -> []) (decls, ns) <- get -- ignore decls in HO types put (PTacImplicit 10 l n scr Placeholder : 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) -- Add implicit arguments in function calls 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 [] [] -- TODO: in patterns, don't add implicits to function names guarded by constructors -- and *not* inside a PHidden 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 p l t r) = let l' = ai env ds l t' = ai env ds t r' = ai env ds r in PDPair fc p 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 -- if in a pattern, and there are no arguments, and there's no possible -- names with zero explicit arguments, don't add implicits. 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 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $ if (not (vname f) || tcname f || any (conCaf (tt_ctxt ist)) ialts) -- any constructor alts || any allImp ialts)) then aiFn inpat False ist fc f ds [] -- use it as a constructor else Right $ PPatvar fc f where imp (PExp _ _ _) = False imp _ = True -- allImp [] = False allImp xs = all imp xs constructor (TyDecl (DCon _ _) _) = True constructor _ = False conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia vname (UN n) = True -- non qualified 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 -- This is where namespaces get resolved by adding PAlternative = 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 : given) = PExp p l tm : insertImpl ps given insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) = PConstraint p l tm : insertImpl ps given insertImpl (PConstraint p l ty : ps) given = PConstraint p l (PResolveTC fc) : insertImpl ps given insertImpl (PImp p _ l n ty : 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 : 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) -- replace non-linear occurrences with _ -- ASSUMPTION: This is called before adding 'alternatives' because otherwise -- it is hard to get right! 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 t@(PAlternative _ (a : as)) = do sl a return t sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var args' <- mapM slA args return $ PApp fc fn args' where slA (PImp p m l n t) = do t' <- sl t return $ PImp p m l n t' slA (PExp p l t) = do t' <- sl t return $ PExp p l t' slA (PConstraint p l t) = do t' <- sl t return $ PConstraint p l t' slA (PTacImplicit p l n sc t) = do t' <- sl t return $ PTacImplicit p l n sc t' sl x = return x -- Remove functions which aren't applied to anything, which must then -- be resolved by unification. Assume names resolved and alternatives -- filled in (so no ambiguity). 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 p l t r) = PDPair fc p (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 -- Find 'static' argument positions -- (the declared ones, plus any names in argument position in the declared -- statics) -- FIXME: It's possible that this really has to happen after elaboration 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 -- for 6.12/7 compatibility 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 -- syntactic match of a against b, returning pair of variables in a -- and what they match. Returns the pair that failed if not a match. 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)] -- if one namespace is missing, drop the other | n == n' || n == dropNS n' || dropNS n == n' = return [] where dropNS (NS n _) = n dropNS n = n 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 [] -- lifted out match (PMetavar _) _ = return [] -- modified match (PInferRef _ _) _ = return [] -- modified 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 p x t y) = PDPair f p (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 p x t y) = PDPair f p (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 -- Rename any binders which are repeated (so that we don't have to mess -- about with shadowing anywhere else). 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' }) -- Initialise the unique name with the environment length (so we're not -- looking for too long...) initN (UN n) l = UN $ txt (str n ++ show l) initN (MN i s) l = MN (i+l) s initN n l = n -- FIXME: Probably ought to do this for completeness! It's fine as -- long as there are no bindings inside tactics though. 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 (initN n (length env)) (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 (initN n (length env)) (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 (initN n (length env)) (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 p (PRef fc' n) t sc) | t /= Placeholder = 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) t' <- mkUniq t sc'' <- mkUniq sc' return $! PDPair fc p (PRef fc' n') t' sc'' mkUniq (PDPair fc p l t r) = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r return $! PDPair fc p 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