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 [])
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' }
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
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 -> 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 ()
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)
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
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
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' }
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 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 ->
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
PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
else
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
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 argDocs syn fc co pd)
= PData doc argDocs 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, 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)
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 = []
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
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
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
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)
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 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
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 : 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)
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
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
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
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' || 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 []
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 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
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' })
initN (UN n) l = UN $ txt (str n ++ show l)
initN (MN i s) l = MN (i+l) s
initN n l = n
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