idris-0.9.17: src/Idris/AbsSyntax.hs
{-# 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.IdeMode hiding (Opt(..))
import IRTS.CodegenCommon
import Util.DynamicLinker
import System.Console.Haskeline
import System.IO
import Control.Applicative
import Control.Monad.State
import Data.List hiding (insert,union)
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 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
getAutoImports :: Idris [FilePath]
getAutoImports = do i <- getIState
return (opt_autoImport (idris_options i))
addAutoImport :: FilePath -> Idris ()
addAutoImport fp = do i <- getIState
let opts = idris_options i
let autoimps = opt_autoImport opts
put (i { idris_options = opts { opt_autoImport =
fp : opt_autoImport opts } } )
addHdr :: Codegen -> String -> Idris ()
addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
addImported :: Bool -> FilePath -> Idris ()
addImported pub f
= do i <- getIState
putIState $ i { idris_imported = nub $ (f, pub) : 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
}
-- Transforms are organised by the function being applied on the lhs of the
-- transform, to make looking up appropriate transforms quicker
addTrans :: Name -> (Term, Term) -> Idris ()
addTrans basefn t
= do i <- getIState
let t' = case lookupCtxtExact basefn (idris_transforms i) of
Just def -> (t : def)
Nothing -> [t]
putIState $ i { idris_transforms = addDef basefn t'
(idris_transforms i) }
addErrRev :: (Term, Term) -> Idris ()
addErrRev t = do i <- getIState
putIState $ i { idris_errRev = t : idris_errRev i }
addErasureUsage :: Name -> Int -> Idris ()
addErasureUsage n i = do ist <- getIState
putIState $ ist { idris_erasureUsed = (n, i) : idris_erasureUsed ist }
addExport :: Name -> Idris ()
addExport n = do ist <- getIState
putIState $ ist { idris_exports = n : idris_exports ist }
addUsedName :: FC -> Name -> Name -> Idris ()
addUsedName fc n arg
= do ist <- getIState
case lookupTyName n (tt_ctxt ist) of
[(n', ty)] -> addUsage n' 0 ty
[] -> throwError (At fc (NoSuchVariable n))
xs -> throwError (At fc (CantResolveAlts (map fst xs)))
where addUsage n i (Bind x _ sc) | x == arg = do addIBC (IBCUsage (n, i))
addErasureUsage n i
| otherwise = addUsage n (i + 1) sc
addUsage _ _ _ = throwError (At fc (Msg ("No such argument name " ++ show arg)))
getErasureUsage :: Idris [(Name, Int)]
getErasureUsage = do ist <- getIState;
return (idris_erasureUsed ist)
getExports :: Idris [Name]
getExports = do ist <- getIState
return (idris_exports ist)
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) }
setFnInfo :: Name -> FnInfo -> Idris ()
setFnInfo n fs = do i <- getIState; putIState $ i { idris_fninfo = addDef n fs (idris_fninfo 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, Nothing) (y, Nothing) (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 DocTerm -> [(Name, Docstring DocTerm)] -> 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 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
_ -> []
-- Issue #1737 in the Issue Tracker.
-- https://github.com/idris-lang/Idris-dev/issues/1737
addToCalledG :: Name -> [Name] -> Idris ()
addToCalledG n ns = return () -- TODO
push_estack :: Name -> Idris ()
push_estack n = do i <- getIState
putIState (i { elab_stack = n : elab_stack i })
pop_estack :: Idris ()
pop_estack = do i <- getIState
putIState (i { elab_stack = ptail (elab_stack i) })
where ptail [] = []
ptail (x : xs) = xs
-- 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 fds] ->
do let cs = addDef n (CI a b c d e (addI i ins) fds) (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
putIState i'
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))
getSymbol :: Name -> Idris Name
getSymbol n = do i <- getIState
case M.lookup n (idris_symbols i) of
Just n' -> return n'
Nothing -> do let sym' = M.insert n n (idris_symbols i)
put (i { idris_symbols = sym' })
return n
getHdrs :: Codegen -> Idris [String]
getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
getImported :: Idris [(FilePath, Bool)]
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
updateIState :: (IState -> IState) -> Idris ()
updateIState f = do i <- getIState
putIState $ f i
withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
withContext ctx name dflt action = do
ist <- getIState
case lookupCtxt name (ctx ist) of
[x] -> action x
_ -> return dflt
withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()
withContext_ ctx name action = withContext ctx name () action
-- | 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"
--
-- Issue #1738 on the issue tracker.
-- https://github.com/idris-lang/Idris-dev/issues/1738
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 lookupTyExact n i of
Just _ -> 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 = nub 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)
-- | Save information about a name that is not yet defined
addDeferred' :: NameType
-> [(Name, (Int, Maybe Name, Type, Bool))]
-- ^ The Name is the name being made into a metavar,
-- the Int is the number of vars that are part of a
-- putative proof context, the Maybe Name is the
-- top-level function containing the new metavariable,
-- the Type is its type, and the Bool is whether :p is
-- allowed
-> Idris ()
addDeferred' nt ns
= do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty 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' is to generate user accessible names in case they are
-- needed in tactic scripts
tidyNames used (Bind (MN i x) b sc)
= let n' = uniqueNameSet (UN x) used in
Bind n' b $ tidyNames (S.insert n' used) sc
tidyNames used (Bind n b sc)
= let n' = uniqueNameSet n used in
Bind n' b $ tidyNames (S.insert 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 }
type1Doc :: Doc OutputAnnotation
type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")
isetPrompt :: String -> Idris ()
isetPrompt p = do i <- getIState
case idris_outputmode i of
IdeMode n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n
-- | Tell clients how much was parsed and loaded
isetLoadedRegion :: Idris ()
isetLoadedRegion = do i <- getIState
let span = idris_parsedSpan i
case span of
Just fc ->
case idris_outputmode i of
IdeMode n h ->
runIO . hPutStrLn h $
convSExp "set-loaded-region" fc n
Nothing -> return ()
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 opts' = opts { opt_errContext = t }
putIState $ i { idris_options = opts' }
errContext :: Idris Bool
errContext = do i <- getIState
return (opt_errContext (idris_options i))
getOptimise :: Idris [Optimisation]
getOptimise = do i <- getIState
return (opt_optimise (idris_options i))
setOptimise :: [Optimisation] -> Idris ()
setOptimise newopts = do i <- getIState
let opts = idris_options i
let opts' = opts { opt_optimise = newopts }
putIState $ i { idris_options = opts' }
addOptimise :: Optimisation -> Idris ()
addOptimise opt = do opts <- getOptimise
setOptimise (nub (opt : opts))
removeOptimise :: Optimisation -> Idris ()
removeOptimise opt = do opts <- getOptimise
setOptimise ((nub opts) \\ [opt])
-- Set appropriate optimisation set for the given level. We only have
-- one optimisation that is configurable at the moment, however!
setOptLevel :: Int -> Idris ()
setOptLevel n | n <= 0 = setOptimise []
setOptLevel 1 = setOptimise []
setOptLevel 2 = setOptimise [PETransform]
setOptLevel n | n >= 3 = setOptimise [PETransform]
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
setIdeMode :: Bool -> Handle -> Idris ()
setIdeMode True h = do i <- getIState
putIState $ i { idris_outputmode = IdeMode 0 h
, idris_colourRepl = False
}
setIdeMode 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))
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 = nub $ 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 }
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 }
setColour' PostulateColour c t = t { postulateColour = 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 h -> do runIO $ hPutStrLn h str
IdeMode n h ->
do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
runIO . hPutStrLn h $ 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 fc n t s)
| n `elem` (map fst ps ++ ns)
= let n' = mkShadow n in
PLam fc n' (en t) (en (shadow n n' s))
| otherwise = PLam fc n (en t) (en s)
en (PPi p n t s)
| n `elem` (map fst ps ++ ns)
= let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
PPi (enTacImp p) n' (en t) (en (shadow n n' s))
| otherwise = PPi (enTacImp p) n (en t) (en s)
en (PLet fc n ty v s)
| n `elem` (map fst ps ++ ns)
= let n' = mkShadow n in
PLet fc n' (en ty) (en v) (en (shadow n n' s))
| otherwise = PLet fc 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 lt rt l r) = PEq f (en lt) (en rt) (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 (PRunTactics fc tm) = PRunTactics fc (en tm)
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
enTacImp (TacImp aos st scr) = TacImp aos st (en scr)
enTacImp other = other
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 pn 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)
pn
(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 _ = []
-- | Expands parameters defined in parameter and where blocks inside of declarations
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 opts cdoc cn cty)
= if tn `elem` ns
then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))
opts cdoc (dec cn) conty
else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)
opts 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 pDocs fds decls)
= PClass doc info f
(map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
n
(map (mapsnd (expandParams dec ps ns [])) params)
pDocs
fds
(map (expandParamsD rhs ist dec ps ns) decls)
expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs n params ty cn decls)
= PInstance doc argDocs info f
(map (\ (n, t) -> (n, expandParams dec ps ns [] t)) 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 (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
ist <- getIState
let paramnames
= nub $ case lookupCtxtExact n (idris_fninfo ist) of
Just p -> getNamesFrom 0 (fn_params p) tm ++
concatMap (getParamNames ist) (map snd statics)
_ -> concatMap (getParamNames ist) (map snd statics)
let stnames = nub $ concatMap freeArgNames (map snd statics)
let dnames = (nub $ concatMap freeArgNames (map snd dynamics))
\\ paramnames
-- also get the arguments which are 'uniquely inferrable' from
-- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
-- or parameters to the type of a static
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 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"
++ showTmImpls ptm ++ "\n"
++ show statics ++ "\n" ++ show dynamics
++ "\n" ++ show paramnames
++ "\n" ++ show stpos
putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
addIBC (IBCStatic n)
where
initStatics (Bind n (Pi _ ty _) sc) (PPi p n' t s)
| n /= n' = let (static, dynamic) = initStatics sc (PPi p n' t s) in
(static, (n, ty) : dynamic)
initStatics (Bind n (Pi _ ty _) sc) (PPi p n' _ 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 = ([], [])
getParamNames ist tm | (P _ n _ , args) <- unApply tm
= case lookupCtxtExact n (idris_datatypes ist) of
Just ti -> getNamePos 0 (param_pos ti) args
Nothing -> []
where getNamePos i ps [] = []
getNamePos i ps (P _ n _ : as)
| i `elem` ps = n : getNamePos (i + 1) ps as
getNamePos i ps (_ : as) = getNamePos (i + 1) ps as
getParamNames ist (Bind t (Pi _ (P _ n _) _) sc)
= n : getParamNames ist sc
getParamNames ist _ = []
getNamesFrom i ps (Bind n (Pi _ _ _) sc)
| i `elem` ps = n : getNamesFrom (i + 1) ps sc
| otherwise = getNamesFrom (i + 1) ps sc
getNamesFrom i ps sc = []
freeArgNames (Bind n (Pi _ ty _) sc)
= nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
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 some bound implicits to the using block if they aren't there already
addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
addToUsing us [] = us
addToUsing us ((n, t) : ns)
| n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
| otherwise = addToUsing us ns
where impName (UImplicit n _) = Just n
impName _ = Nothing
-- 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
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 [] (sMN 0 "carg") (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 bindings from using block, and bind any missing names
addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
addUsingImpls syn n fc t
= do ist <- getIState
let ns = implicitNamesIn (map iname uimpls) ist t
let badnames = filter (\n -> not (implicitable n) &&
n `notElem` (map iname uimpls)) ns
when (not (null badnames)) $
throwError (At fc (Elaborating "type of " n
(NoSuchVariable (head badnames))))
let cs = getArgnames t -- get already bound names
let addimpls = filter (\n -> iname n `notElem` cs) uimpls
-- if all names in the arguments of addconsts appear in ns,
-- add the constraint implicitly
return (bindFree ns (doAdd addimpls ns t))
where uimpls = filter uimpl (using syn)
uimpl (UImplicit _ _) = True
uimpl _ = False
iname (UImplicit n _) = n
iname (UConstraint _ _) = error "Can't happen addUsingImpls"
doAdd [] _ t = t
-- if all of args in ns, then add it
doAdd (UImplicit n ty : cs) ns t
| elem n ns
= PPi (Imp [] Dynamic False Nothing) n ty (doAdd cs ns t)
| otherwise = doAdd cs ns t
-- bind the free names which weren't in the using block
bindFree [] tm = tm
bindFree (n:ns) tm
| elem n (map iname uimpls) = bindFree ns tm
| otherwise
= PPi (Imp [] Dynamic False Nothing) n Placeholder (bindFree ns tm)
getArgnames (PPi _ n c sc)
= n : getArgnames sc
getArgnames _ = []
-- Given the original type and the elaborated type, return the implicitness
-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
getUnboundImplicits i t tm = getImps t (collectImps tm)
where collectImps (PPi p n t sc)
= (n, (p, t)) : collectImps sc
collectImps _ = []
getImps (Bind n (Pi (Just _) _ _) sc) imps = getImps sc imps
getImps (Bind n (Pi _ t _) sc) imps
| Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
where
argInfo n (Imp opt _ _ _) Placeholder
= (True, PImp 0 True opt n Placeholder)
argInfo n (Imp opt _ _ _) t'
= (False, PImp (getPriority i t') True opt n t')
argInfo n (Exp opt _ _) t'
= (InaccessibleArg `elem` opt,
PExp (getPriority i t') opt n t')
argInfo n (Constraint opt _) t'
= (InaccessibleArg `elem` opt,
PConstraint 10 opt n t')
argInfo n (TacImp opt _ scr) t'
= (InaccessibleArg `elem` opt,
PTacImplicit 10 opt n scr t')
getImps (Bind n (Pi _ t _) sc) imps = impBind n t : getImps sc imps
where impBind n t = (True, PImp 1 True [] n Placeholder)
getImps sc tm = []
-- 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...
-- TODO: This is obsoleted by the new way of elaborating types, but there's still
-- a couple of places which use it. Clean them up!
--
-- Issue 1739 in the issue tracker
-- https://github.com/idris-lang/Idris-dev/issues/1739
implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
implicit info syn n ptm = implicit' info syn [] n ptm
implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
implicit' info syn ignore n ptm
= do i <- getIState
let (tm', impdata) = implicitise syn ignore i ptm
defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
-- 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'
where
-- Detect unknown names in default arguments and throw error if found.
defaultArgCheck :: [Name] -> [PArg] -> Idris ()
defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params
notFoundInDefault :: [Name] -> PArg -> Idris [Name]
notFoundInDefault kns (PTacImplicit _ _ n script _)
= do i <- getIState
case notFound kns (namesIn [] i script) of
Nothing -> return (n:kns)
Just name -> throwError (NoSuchVariable name)
notFoundInDefault kns p = return ((pname p):kns)
notFound :: [Name] -> [Name] -> Maybe Name
notFound kns [] = Nothing
notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns -- Known already
notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
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 n 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 n 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 fc 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 (PRunTactics fc 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 Nothing) n ty (pibind using ns sc)
Nothing -> PPi (Imp [] Dynamic False Nothing) 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
-- | Add the implicit arguments to applications in the term
-- [Name] gives the names to always expend, even when under a binder of
-- that name (this is to expand methods with implicit arguments in dependent
-- type classes).
addImpl :: [Name] -> 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] -> [Name] -> IState -> PTerm -> PTerm
addImpl' inpat env infns imp_meths ist ptm
= mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)
where
ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
ai qq env ds (PRef fc f)
| f `elem` infns = PInferRef fc f
| not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq imp_meths ist fc f ds []
ai qq env ds (PHidden (PRef fc f))
| not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq imp_meths ist fc f ds [])
ai qq env ds (PEq fc lt rt l r)
= let lt' = ai qq env ds lt
rt' = ai qq env ds rt
l' = ai qq env ds l
r' = ai qq env ds r in
PEq fc lt' rt' l' r'
ai qq env ds (PRewrite fc l r g)
= let l' = ai qq env ds l
r' = ai qq env ds r
g' = fmap (ai qq env ds) g in
PRewrite fc l' r' g'
ai qq env ds (PTyped l r)
= let l' = ai qq env ds l
r' = ai qq env ds r in
PTyped l' r'
ai qq env ds (PPair fc p l r)
= let l' = ai qq env ds l
r' = ai qq env ds r in
PPair fc p l' r'
ai qq env ds (PDPair fc p l t r)
= let l' = ai qq env ds l
t' = ai qq env ds t
r' = ai qq env ds r in
PDPair fc p l' t' r'
ai qq env ds (PAlternative a as)
= let as' = map (ai qq env ds) as in
PAlternative a as'
ai qq env _ (PDisamb ds' as) = ai qq env ds' as
ai qq env ds (PApp fc (PInferRef _ f) as)
= let as' = map (fmap (ai qq env ds)) as in
PApp fc (PInferRef fc f) as'
ai qq env ds (PApp fc ftm@(PRef _ f) as)
| f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)
| not (f `elem` map fst env)
= let as' = map (fmap (ai qq env ds)) as in
handleErr $ aiFn inpat False qq imp_meths ist fc f ds as'
| Just (Just ty) <- lookup f env =
let as' = map (fmap (ai qq env ds)) as
arity = getPArity ty in
mkPApp fc arity ftm as'
ai qq env ds (PApp fc f as)
= let f' = ai qq env ds f
as' = map (fmap (ai qq env ds)) as in
mkPApp fc 1 f' as'
ai qq env ds (PCase fc c os)
= let c' = ai qq env ds c in
-- leave os alone, because they get lifted into a new pattern match
-- definition which is passed through addImpl again with more scope
-- information
PCase fc c' os
-- If the name in a lambda is a constructor name, do this as a 'case'
-- instead (it is harmless to do so, especially since the lambda will
-- be lifted anyway!)
ai qq env ds (PLam fc n ty sc)
= case lookupDef n (tt_ctxt ist) of
[] -> let ty' = ai qq env ds ty
sc' = ai qq ((n, Just ty):env) ds sc in
PLam fc n ty' sc'
_ -> ai qq env ds (PLam fc (sMN 0 "lamp") ty
(PCase fc (PRef fc (sMN 0 "lamp") )
[(PRef fc n, sc)]))
ai qq env ds (PLet fc n ty val sc)
= case lookupDef n (tt_ctxt ist) of
[] -> let ty' = ai qq env ds ty
val' = ai qq env ds val
sc' = ai qq ((n, Just ty):env) ds sc in
PLet fc n ty' val' sc'
_ -> ai qq env ds (PCase fc val [(PRef fc n, sc)])
ai qq env ds (PPi p n ty sc)
= let ty' = ai qq env ds ty
env' = if n `elem` imp_meths then env
else ((n, Just ty) : env)
sc' = ai qq env' ds sc in
PPi p n ty' sc'
ai qq env ds (PGoal fc r n sc)
= let r' = ai qq env ds r
sc' = ai qq ((n, Nothing):env) ds sc in
PGoal fc r' n sc'
ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)
-- Don't do PProof or PTactics since implicits get added when scope is
-- properly known in ElabTerm.runTac
ai qq env ds (PRefl fc tm) = PRefl fc (ai qq env ds tm)
ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)
ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)
ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)
(fmap (ai True env ds) g)
ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
ai qq env ds (PRunTactics fc tm) = PRunTactics fc (ai False env ds tm)
ai qq 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 -> Bool -> [Name] -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
aiFn inpat True qq imp_meths 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 qq imp_meths 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 || (qq && isTConName n ctxt)) && allImp cia
vname (UN n) = True -- non qualified
vname _ = False
aiFn inpat expat qq imp_meths ist fc f ds as
| f `elem` primNames = Right $ PApp fc (PRef fc f) as
aiFn inpat expat qq imp_meths 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 (isImpName f 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 (isImpName f f'))
(insertImpl ns as)) alts
where
-- if the name is in imp_meths, we should actually refer to the bound
-- name rather than the global one after expanding implicits
isImpName f f' | f `elem` imp_meths = f
| otherwise = f'
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 lookupDefAccExact n False (tt_ctxt ist) of
Just (n,t) -> t
_ -> Public
insertImpl :: [PArg] -> [PArg] -> [PArg]
insertImpl ps as = insImpAcc M.empty ps (filter exp as) (filter (not.exp) as)
exp (PExp _ _ _ _) = True
exp (PConstraint _ _ _ _) = True
exp _ = False
insImpAcc :: M.Map Name PTerm -- accumulated param names & arg terms
-> [PArg] -- parameters
-> [PArg] -- explicit arguments
-> [PArg] -- implicits given
-> [PArg]
insImpAcc pnas (PExp p l n ty : ps) (PExp _ _ _ tm : given) imps =
PExp p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
insImpAcc pnas (PConstraint p l n ty : ps) (PConstraint _ _ _ tm : given) imps =
PConstraint p l n tm : insImpAcc (M.insert n tm pnas) ps given imps
insImpAcc pnas (PConstraint p l n ty : ps) given imps =
let rtc = PResolveTC fc in
PConstraint p l n rtc : insImpAcc (M.insert n rtc pnas) ps given imps
insImpAcc pnas (PImp p _ l n ty : ps) given imps =
case find n imps [] of
Just (tm, imps') ->
PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
Nothing -> let ph = if f `elem` imp_meths then PRef fc n else Placeholder in
PImp p True l n ph :
insImpAcc (M.insert n ph pnas) ps given imps
insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
case find n imps [] of
Just (tm, imps') ->
PTacImplicit p l n sc tm :
insImpAcc (M.insert n tm pnas) ps given imps'
Nothing ->
if inpat
then PTacImplicit p l n sc Placeholder :
insImpAcc (M.insert n Placeholder pnas) ps given imps
else PTacImplicit p l n sc sc :
insImpAcc (M.insert n sc pnas) ps given imps
insImpAcc _ expected [] imps = imps -- so that unused implicits give error
-- TODO: report here, and prune alternatives
-- Issue #1740 in the Issue Tracker
-- https://github.com/idris-lang/Idris-dev/issues/1740
insImpAcc _ _ given imps = given ++ imps
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 _
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 $ PHidden (PRef fc f) -- Placeholder
else do put (f : ns)
return (PRef fc f)
sl (PPatvar fc f)
= do ns <- get
if (f `elem` ns)
then return $ PHidden (PPatvar fc f) -- Placeholder
else do put (f : ns)
return (PPatvar fc f)
-- Assumption is that variables are all the same in each alternative
sl t@(PAlternative b as) = do ns <- get
as' <- slAlts ns as
return (PAlternative b as')
where slAlts ns (a : as) = do put ns
a' <- sl a
as' <- slAlts ns as
return (a' : as')
slAlts ns [] = return []
sl (PPair fc p l r) = do l' <- sl l; r' <- sl r; return (PPair fc p l' r')
sl (PDPair fc p l t r) = do l' <- sl l
t' <- sl t
r' <- sl r
return (PDPair fc p l' t' r')
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 n t) = do t' <- sl t
return $ PExp p l n t'
slA (PConstraint p l n t)
= do t' <- sl t
return $ PConstraint p l n 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 f@(PRef _ fn) args)
-- here we use canBeDConName because the impossible pattern
-- check will not necessarily fully resolve constructor names,
-- and these bare names will otherwise get in the way of
-- impossbility checking.
| canBeDConName fn ctxt
= PApp fc f (fmap (fmap su) args)
su (PApp fc f args)
= PHidden (PApp fc f 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@(PLam fc _ _ _) = PHidden t
su t@(PPi _ _ _ _) = PHidden t
su t@(PEq _ _ _ _ _) = PHidden t
su t = t
ctxt = tt_ctxt i
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 deriving ( Functor )
instance Applicative (EitherErr a) where
pure = return
(<*>) = ap
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 (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)
| RightOK xs <- match x y = return xs -- to collect variables
| otherwise = return [] -- Otherwise hidden things are unmatchable
match (PHidden x) y
| RightOK xs <- match x y = return xs
| otherwise = return []
match x (PHidden y)
| RightOK xs <- match x y = return xs
| otherwise = return []
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 fc x t sc) = PLam fc 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 xt yt x y) = PEq f (sm xs xt) (sm xs yt) (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 fc x t sc) | n /= x = PLam fc x (sm t) (sm sc)
| otherwise = PLam fc x (sm t) sc
sm (PPi p x t sc) | n /= x = PPi p x (sm t) (sm sc)
| otherwise = PPi p x (sm t) sc
sm (PLet fc x t v sc) | n /= x = PLet fc x (sm t) (sm v) (sm sc)
| otherwise = PLet fc x (sm t) (sm v) 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 xt yt x y) = PEq f (sm xt) (sm yt) (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) (S.fromList env) where
inScope :: S.Set Name
inScope = S.fromList $ 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 (S.Set Name) PTerm
mkUniq (PLam fc n ty sc)
= do env <- get
(n', sc') <-
if n `S.member` env
then do let n' = uniqueNameSet (initN n (S.size env))
(S.union env inScope)
return (n', shadow n n' sc)
else return (n, sc)
put (S.insert n' env)
ty' <- mkUniq ty
sc'' <- mkUniq sc'
return $! PLam fc n' ty' sc''
mkUniq (PPi p n ty sc)
= do env <- get
(n', sc') <-
if n `S.member` env
then do let n' = uniqueNameSet (initN n (S.size env))
(S.union env inScope)
return (n', shadow n n' sc)
else return (n, sc)
put (S.insert n' env)
ty' <- mkUniq ty
sc'' <- mkUniq sc'
return $! PPi p n' ty' sc''
mkUniq (PLet fc n ty val sc)
= do env <- get
(n', sc') <-
if n `S.member` env
then do let n' = uniqueNameSet (initN n (S.size env))
(S.union env inScope)
return (n', shadow n n' sc)
else return (n, sc)
put (S.insert n' env)
ty' <- mkUniq ty; val' <- mkUniq val
sc'' <- mkUniq sc'
return $! PLet fc 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 `S.member` env
then do let n' = uniqueNameSet n (S.union env inScope)
return (n', shadow n n' sc)
else return (n, sc)
put (S.insert 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 (PRunTactics fc ts) = liftM (PRunTactics fc ) (mkUniq ts)
mkUniq t = return t