idris-1.2.0: src/Idris/Elab/Utils.hs
{-|
Module : Idris.Elab.Utils
Description : Elaborator utilities.
License : BSD3
Maintainer : The Idris Community.
-}
{-# LANGUAGE FlexibleContexts, PatternGuards #-}
module Idris.Elab.Utils where
import Idris.AbsSyntax
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Core.WHNF
import Idris.Delaborate
import Idris.Docstrings
import Idris.Error
import Idris.Output
import Util.Pretty
import Control.Monad
import Control.Monad.State
import Data.List
import qualified Data.Map as Map
import Data.Maybe
recheckC = recheckC_borrowing False True []
recheckC_borrowing uniq_check addConstrs bs tcns fc mkerr env t
= do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)
ctxt <- getContext
t' <- case safeForget t of
Just ft -> return ft
Nothing -> tclift $ tfail $ mkerr (At fc (IncompleteTerm t))
(tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs tcns ctxt env t' t of
Error e -> tfail (At fc (mkerr e))
OK x -> return x
logElab 6 $ "CONSTRAINTS ADDED: " ++ show (tm, ty, cs)
tit <- typeInType
when (not tit && addConstrs) $
do addConstraints fc cs
mapM_ (\c -> addIBC (IBCConstraint fc c)) (snd cs)
mapM_ (checkDeprecated fc) (allTTNames tm)
mapM_ (checkDeprecated fc) (allTTNames ty)
mapM_ (checkFragile fc) (allTTNames tm)
mapM_ (checkFragile fc) (allTTNames ty)
return (tm, ty)
checkDeprecated :: FC -> Name -> Idris ()
checkDeprecated fc n
= do r <- getDeprecated n
case r of
Nothing -> return ()
Just r -> do iWarn fc $ text "Use of deprecated name " <> annName n
<> case r of
"" -> Util.Pretty.empty
_ -> line <> text r
checkFragile :: FC -> Name -> Idris ()
checkFragile fc n = do
r <- getFragile n
case r of
Nothing -> return ()
Just r -> do
iWarn fc $ text "Use of a fragile construct "
<> annName n
<> case r of
"" -> Util.Pretty.empty
_ -> line <> text r
iderr :: Name -> Err -> Err
iderr _ e = e
checkDef :: ElabInfo -> FC -> (Name -> Err -> Err) -> Bool ->
[(Name, (Int, Maybe Name, Type, [Name]))] ->
Idris [(Name, (Int, Maybe Name, Type, [Name]))]
checkDef info fc mkerr definable ns
= checkAddDef False True info fc mkerr definable ns
checkAddDef :: Bool -> Bool -> ElabInfo -> FC -> (Name -> Err -> Err) -> Bool
-> [(Name, (Int, Maybe Name, Type, [Name]))]
-> Idris [(Name, (Int, Maybe Name, Type, [Name]))]
checkAddDef add toplvl info fc mkerr def [] = return []
checkAddDef add toplvl info fc mkerr definable ((n, (i, top, t, psns)) : ns)
= do ctxt <- getContext
logElab 5 $ "Rechecking deferred name " ++ show (n, t, definable)
(t', _) <- recheckC (constraintNS info) fc (mkerr n) [] t
when add $ do addDeferred [(n, (i, top, t, psns, toplvl, definable))]
addIBC (IBCDef n)
ns' <- checkAddDef add toplvl info fc mkerr definable ns
return ((n, (i, top, t', psns)) : ns')
-- | Get the list of (index, name) of inaccessible arguments from an elaborated
-- type
inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]
inaccessibleImps i (Bind n (Pi _ _ t _) sc) (inacc : ins)
| inacc = (i, n) : inaccessibleImps (i + 1) sc ins
| otherwise = inaccessibleImps (i + 1) sc ins
inaccessibleImps _ _ _ = []
-- | Get the list of (index, name) of inaccessible arguments from the type.
inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]
inaccessibleArgs i (PPi plicity n _ ty t)
| InaccessibleArg `elem` pargopts plicity
= (i,n) : inaccessibleArgs (i+1) t -- an .{erased : Implicit}
| otherwise
= inaccessibleArgs (i+1) t -- a {regular : Implicit}
inaccessibleArgs _ _ = []
elabCaseBlock :: ElabInfo -> FnOpts -> PDecl -> Idris ()
elabCaseBlock info opts d@(PClauses f o n ps)
= do addIBC (IBCDef n)
logElab 5 $ "CASE BLOCK: " ++ show (n, d)
-- propagate totality assertion to the new definitions
let opts' = filter propagatable opts
setFlags n opts'
rec_elabDecl info EAll info (PClauses f opts' n ps )
where
propagatable AssertTotal = True
propagatable Inlinable = True
propagatable _ = False
-- | Check that the result of type checking matches what the programmer wrote
-- (i.e. - if we inferred any arguments that the user provided, make sure
-- they are the same!)
checkInferred :: FC -> PTerm -> PTerm -> Idris ()
checkInferred fc inf user =
do logElab 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n\nFROM\n\n" ++
showTmImpls user
logElab 10 $ "Checking match"
i <- getIState
tclift $ case matchClause' True i user inf of
_ -> return ()
-- Left (x, y) -> tfail $ At fc
-- (Msg $ "The type-checked term and given term do not match: "
-- ++ show x ++ " and " ++ show y)
logElab 10 $ "Checked match"
-- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)
-- | Return whether inferred term is different from given term
-- (as above, but return a Bool)
inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool
inferredDiff fc inf user =
do i <- getIState
logElab 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n" ++
showTmImpls user
tclift $ case matchClause' True i user inf of
Right vs -> return False
Left (x, y) -> return True
-- | Check a PTerm against documentation and ensure that every documented
-- argument actually exists. This must be run _after_ implicits have been
-- found, or it will give spurious errors.
checkDocs :: FC -> [(Name, Docstring a)] -> PTerm -> Idris ()
checkDocs fc args tm = cd (Map.fromList args) tm
where cd as (PPi _ n _ _ sc) = cd (Map.delete n as) sc
cd as _ | Map.null as = return ()
| otherwise = ierror . At fc . Msg $
"There is documentation for argument(s) "
++ (concat . intersperse ", " . map show . Map.keys) as
++ " but they were not found."
decorateid decorate (PTy doc argdocs s f o n nfc t) = PTy doc argdocs s f o (decorate n) nfc t
decorateid decorate (PClauses f o n cs)
= PClauses f o (decorate n) (map dc cs)
where dc (PClause fc n t as w ds) = PClause fc (decorate n) (dappname t) as w ds
dc (PWith fc n t as w pn ds)
= PWith fc (decorate n) (dappname t) as w pn
(map (decorateid decorate) ds)
dappname (PApp fc (PRef fc' hl n) as) = PApp fc (PRef fc' hl (decorate n)) as
dappname t = t
-- if 't' is an interface application, assume its arguments are injective
pbinds :: IState -> Term -> ElabD ()
pbinds i (Bind n (PVar rig t) sc)
= do attack; patbind n rig
env <- get_env
case unApply (normalise (tt_ctxt i) env t) of
(P _ c _, args) -> case lookupCtxt c (idris_interfaces i) of
[] -> return ()
_ -> -- interface, set as injective
mapM_ setinjArg args
_ -> return ()
pbinds i sc
where setinjArg (P _ n _) = setinj n
setinjArg _ = return ()
pbinds i tm = return ()
pbty (Bind n (PVar _ t) sc) tm = Bind n (PVTy t) (pbty sc tm)
pbty _ tm = tm
getPBtys (Bind n (PVar _ t) sc) = (n, t) : getPBtys sc
getPBtys (Bind n (PVTy t) sc) = (n, t) : getPBtys sc
getPBtys _ = []
psolve (Bind n (PVar _ t) sc) = do solve; psolve sc
psolve tm = return ()
pvars ist tm = pv' [] tm
where
pv' env (Bind n (PVar _ t) sc)
= (n, delabWithEnv ist env t) : pv' ((n, t) : env) sc
pv' env _ = []
getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi _ _ t _) sc)
= nub $ getFixedInType i env [] t ++
getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
++ case unApply t of
(P _ n _, _) -> if n `elem` env then [n] else []
_ -> []
getFixedInType i env (_ : is) (Bind n (Pi _ _ t _) sc)
= getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
getFixedInType i env is tm@(App _ f a)
| (P _ tn _, args) <- unApply tm
= case lookupCtxtExact tn (idris_datatypes i) of
Just t -> nub $ paramNames args env (param_pos t) ++
getFixedInType i env is f ++
getFixedInType i env is a
Nothing -> nub $ getFixedInType i env is f ++
getFixedInType i env is a
| otherwise = nub $ getFixedInType i env is f ++
getFixedInType i env is a
getFixedInType i _ _ _ = []
getFlexInType i env ps (Bind n (Pi _ _ t _) sc)
= nub $ (if (not (n `elem` ps)) then getFlexInType i env ps t else []) ++
getFlexInType i (n : env) ps (instantiate (P Bound n t) sc)
getFlexInType i env ps tm@(App _ f a)
| (P nt tn _, args) <- unApply tm, nt /= Bound
= case lookupCtxtExact tn (idris_datatypes i) of
Just t -> nub $ paramNames args env [x | x <- [0..length args],
not (x `elem` param_pos t)]
++ getFlexInType i env ps f ++
getFlexInType i env ps a
Nothing -> let ppos = case lookupCtxtExact tn (idris_fninfo i) of
Just fi -> fn_params fi
Nothing -> []
in nub $ paramNames args env [x | x <- [0..length args],
not (x `elem` ppos)]
++ getFlexInType i env ps f ++
getFlexInType i env ps a
| otherwise = nub $ getFlexInType i env ps f ++
getFlexInType i env ps a
getFlexInType i _ _ _ = []
-- | Treat a name as a parameter if it appears in parameter positions in
-- types, and never in a non-parameter position in a (non-param) argument type.
getParamsInType :: IState -> [Name] -> [PArg] -> Type -> [Name]
getParamsInType i env ps t = let fix = getFixedInType i env ps t
flex = getFlexInType i env fix t in
[x | x <- fix, not (x `elem` flex)]
getTCinj i (Bind n (Pi _ _ t _) sc)
= getTCinj i t ++ getTCinj i (instantiate (P Bound n t) sc)
getTCinj i ap@(App _ f a)
| (P _ n _, args) <- unApply ap,
isTCName n = mapMaybe getInjName args
| otherwise = []
where
isTCName n = case lookupCtxtExact n (idris_interfaces i) of
Just _ -> True
_ -> False
getInjName t | (P _ x _, _) <- unApply t = Just x
| otherwise = Nothing
getTCinj _ _ = []
getTCParamsInType :: IState -> [Name] -> [PArg] -> Type -> [Name]
getTCParamsInType i env ps t = let params = getParamsInType i env ps t
tcs = nub $ getTCinj i t in
filter (flip elem tcs) params
paramNames args env [] = []
paramNames args env (p : ps)
| length args > p = case args!!p of
P _ n _ -> if n `elem` env
then n : paramNames args env ps
else paramNames args env ps
_ -> paramNames args env ps
| otherwise = paramNames args env ps
-- Get all the names with multiplicity '1' used in a partial proof term
getLinearUsed :: Context -> Term -> [Name]
getLinearUsed ctxt tm = execState (getLin [] [] tm) []
where
getLin :: Env -> [(Name, Bool)] -> Term -> State [Name] ()
getLin env us (Bind n b sc)
= do getLinB env us b
let r = getRig b
let lin = case r of
Rig1 -> True
_ -> False
getLin ((n, getRig b, b) : env) ((n, lin) : us) sc
getLin env us (App _ f a) = do getLin env us f; getLin env us a
getLin env us (V i)
| i < length us = if snd (us!!i) then use (fst (us!!1)) else return ()
getLin env us (P _ n _)
| Just u <- lookup n us = if u then use n else return ()
getLin env us _ = return ()
getLinB env us (Let Rig0 t v) = return ()
getLinB env us (Let rig t v) = getLin env us v
getLinB env us (Guess t v) = getLin env us v
getLinB env us (NLet t v) = getLin env us v
getLinB env us b = return ()
use n = do ns <- get; put (n : ns)
getRig :: Binder Term -> RigCount
getRig (Pi rig _ _ _) = rig
getRig (PVar rig _) = rig
getRig (Lam rig _) = rig
getRig (Let rig _ _) = rig
getRig _ = RigW
getUniqueUsed :: Context -> Term -> [Name]
getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []
where
getUniq :: Env -> [(Name, Bool)] -> Term -> State [Name] ()
getUniq env us (Bind n b sc)
= let uniq = case check ctxt env (forgetEnv (map fstEnv env) (binderTy b)) of
OK (_, UType UniqueType) -> True
OK (_, UType NullType) -> True
OK (_, UType AllTypes) -> True
_ -> False in
do getUniqB env us b
getUniq ((n, RigW, b):env) ((n, uniq):us) sc
getUniq env us (App _ f a) = do getUniq env us f; getUniq env us a
getUniq env us (V i)
| i < length us = if snd (us!!i) then use (fst (us!!i)) else return ()
getUniq env us (P _ n _)
| Just u <- lookup n us = if u then use n else return ()
getUniq env us _ = return ()
use n = do ns <- get; put (n : ns)
getUniqB env us (Let rig t v) = getUniq env us v
getUniqB env us (Guess t v) = getUniq env us v
-- getUniqB env us (Pi _ _ t v) = do getUniq env us t; getUniq env us v
getUniqB env us (NLet t v) = getUniq env us v
getUniqB env us b = return () -- getUniq env us (binderTy b)
-- In a functional application, return the names which are used
-- directly in a static position
getStaticNames :: IState -> Term -> [Name]
getStaticNames ist (Bind n (PVar _ _) sc)
= getStaticNames ist (instantiate (P Bound n Erased) sc)
getStaticNames ist tm
| (P _ fn _, args) <- unApply tm
= case lookupCtxtExact fn (idris_statics ist) of
Just stpos -> getStatics args stpos
_ -> []
where
getStatics (P _ n _ : as) (True : ss) = n : getStatics as ss
getStatics (_ : as) (_ : ss) = getStatics as ss
getStatics _ _ = []
getStaticNames _ _ = []
getStatics :: [Name] -> Term -> [Bool]
getStatics ns (Bind n (Pi _ _ _ _) t)
| n `elem` ns = True : getStatics ns t
| otherwise = False : getStatics ns t
getStatics _ _ = []
mkStatic :: [Name] -> PDecl -> PDecl
mkStatic ns (PTy doc argdocs syn fc o n nfc ty)
= PTy doc argdocs syn fc o n nfc (mkStaticTy ns ty)
mkStatic ns t = t
mkStaticTy :: [Name] -> PTerm -> PTerm
mkStaticTy ns (PPi p n fc ty sc)
| n `elem` ns = PPi (p { pstatic = Static }) n fc ty (mkStaticTy ns sc)
| otherwise = PPi p n fc ty (mkStaticTy ns sc)
mkStaticTy ns t = t
-- Check that a name has the minimum required accessibility
checkVisibility :: FC -> Name -> Accessibility -> Accessibility -> Name -> Idris ()
checkVisibility fc n minAcc acc ref
= do nvis <- getFromHideList ref
case nvis of
Nothing -> return ()
Just acc' -> if acc' > minAcc
then tclift $ tfail (At fc
(Msg $ show acc ++ " " ++ show n ++
" can't refer to " ++
show acc' ++ " " ++ show ref))
else return ()
-- | Find the type constructor arguments that are parameters, given a
-- list of constructor types.
--
-- Parameters are names which are unchanged across the structure.
-- They appear at least once in every constructor type, always appear
-- in the same argument position(s), and nothing else ever appears in those
-- argument positions.
findParams :: Name -- ^ the name of the family that we are finding parameters for
-> Type -- ^ the type of the type constructor (normalised already)
-> [Type] -- ^ the declared constructor types
-> [Int]
findParams tyn famty ts =
let allapps = map getDataApp ts
-- do each constructor separately, then merge the results (names
-- may change between constructors)
conParams = map paramPos allapps
in inAll conParams
where
inAll :: [[Int]] -> [Int]
inAll [] = []
inAll (x : xs) = filter (\p -> all (\ps -> p `elem` ps) xs) x
paramPos [] = []
paramPos (args : rest)
= dropNothing $ keepSame (zip [0..] args) rest
dropNothing [] = []
dropNothing ((x, Nothing) : ts) = dropNothing ts
dropNothing ((x, _) : ts) = x : dropNothing ts
keepSame :: [(Int, Maybe Name)] -> [[Maybe Name]] ->
[(Int, Maybe Name)]
keepSame as [] = as
keepSame as (args : rest) = keepSame (update as args) rest
where
update [] _ = []
update _ [] = []
update ((n, Just x) : as) (Just x' : args)
| x == x' = (n, Just x) : update as args
update ((n, _) : as) (_ : args) = (n, Nothing) : update as args
getDataApp :: Type -> [[Maybe Name]]
getDataApp f@(App _ _ _)
| (P _ d _, args) <- unApply f
= if (d == tyn) then [mParam args args] else []
getDataApp (Bind n (Pi _ _ t _) sc)
= getDataApp t ++ getDataApp (instantiate (P Bound n t) sc)
getDataApp _ = []
-- keep the arguments which are single names, which appear
-- in the return type, counting only the first time they appear in
-- the return type as the parameter position
mParam args [] = []
mParam args (P Bound n _ : rest)
| paramIn False n args = Just n : mParam (filter (noN n) args) rest
where paramIn ok n [] = ok
paramIn ok n (P _ t _ : ts)
= paramIn (ok || n == t) n ts
paramIn ok n (t : ts)
| n `elem` freeNames t = False -- not a single name
| otherwise = paramIn ok n ts
-- If the name appears again later, don't count that appearance
-- as a parameter position
noN n (P _ t _) = n /= t
noN n _ = False
mParam args (_ : rest) = Nothing : mParam args rest
-- | Mark a name as detaggable in the global state (should be called
-- for type and constructor names of single-constructor datatypes)
setDetaggable :: Name -> Idris ()
setDetaggable n = do
ist <- getIState
let opt = idris_optimisation ist
case lookupCtxt n opt of
[oi] -> putIState ist { idris_optimisation = addDef n oi { detaggable = True } opt }
_ -> putIState ist { idris_optimisation = addDef n (Optimise [] True []) opt }
displayWarnings :: EState -> Idris ()
displayWarnings est
= mapM_ displayImpWarning (implicit_warnings est)
where
displayImpWarning :: (FC, Name) -> Idris ()
displayImpWarning (fc, n) = do
ist <- getIState
let msg = show (nsroot n)
++ " is bound as an implicit\n"
++ "\tDid you mean to refer to " ++ show n ++ "?"
iWarn fc (pprintErr ist (Msg msg))
propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm
propagateParams i ps t bound tm@(PApp _ (PRef fc hls n) args)
= PApp fc (PRef fc hls n) (addP t args)
where addP (Bind n _ sc) (t : ts)
| Placeholder <- getTm t,
n `elem` ps,
not (n `elem` bound)
= t { getTm = PPatvar NoFC n } : addP sc ts
addP (Bind n _ sc) (t : ts) = t : addP sc ts
addP _ ts = ts
propagateParams i ps t bound (PApp fc ap args)
= PApp fc (propagateParams i ps t bound ap) args
propagateParams i ps t bound (PRef fc hls n)
= case lookupCtxt n (idris_implicits i) of
[is] -> let ps' = filter (isImplicit is) ps in
PApp fc (PRef fc hls n) (map (\x -> pimp x (PRef fc [] x) True) ps')
_ -> PRef fc hls n
where isImplicit [] n = False
isImplicit (PImp _ _ _ x _ : is) n | x == n = True
isImplicit (_ : is) n = isImplicit is n
propagateParams i ps t bound x = x
-- | Gather up all the outer 'PVar's and 'Hole's in an expression and reintroduce
-- them in a canonical order
orderPats :: Term -> Term
orderPats tm = op [] tm
where
op [] (App s f a) = App s f (op [] a) -- for Infer terms
op ps (Bind n (PVar r t) sc) = op ((n, PVar r t) : ps) sc
op ps (Bind n (Hole t) sc) = op ((n, Hole t) : ps) sc
op ps (Bind n (Pi rig i t k) sc) = op ((n, Pi rig i t k) : ps) sc
op ps sc = bindAll (sortP ps) sc
-- Keep explicit Pi in the same order, insert others as necessary,
-- Pi as early as possible, Hole as late as possible
sortP ps = let (exps, imps) = partition isExp ps in
pick (reverse exps) imps
isExp (_, Pi rig Nothing _ _) = True
isExp (_, Pi rig (Just i) _ _) = toplevel_imp i && not (machine_gen i)
isExp _ = False
pick acc [] = acc
pick acc ((n, t) : ps) = pick (insert n t acc) ps
insert n t [] = [(n, t)]
-- if 't' uses any of the names which appear later, insert it later
insert n t rest@((n', t') : ps)
| any (\x -> x `elem` refsIn (binderTy t)) (n' : map fst ps)
= (n', t') : insert n t ps
-- otherwise it's fine where it is (preserve ordering)
| otherwise = (n, t) : rest
-- Make sure all the pattern bindings are as far out as possible
liftPats :: Term -> Term
liftPats tm = let (tm', ps) = runState (getPats tm) [] in
orderPats $ bindPats (reverse ps) tm'
where
bindPats [] tm = tm
bindPats ((n, t):ps) tm
| n `notElem` map fst ps = Bind n (PVar RigW t) (bindPats ps tm)
| otherwise = bindPats ps tm
getPats :: Term -> State [(Name, Type)] Term
getPats (Bind n (PVar _ t) sc) = do ps <- get
put ((n, t) : ps)
getPats sc
getPats (Bind n (Guess t v) sc) = do t' <- getPats t
v' <- getPats v
sc' <- getPats sc
return (Bind n (Guess t' v') sc')
getPats (Bind n (Let rig t v) sc) = do t' <- getPats t
v' <- getPats v
sc' <- getPats sc
return (Bind n (Let rig t' v') sc')
getPats (Bind n (Pi rig i t k) sc) = do t' <- getPats t
k' <- getPats k
sc' <- getPats sc
return (Bind n (Pi rig i t' k') sc')
getPats (Bind n (Lam r t) sc) = do t' <- getPats t
sc' <- getPats sc
return (Bind n (Lam r t') sc')
getPats (Bind n (Hole t) sc) = do t' <- getPats t
sc' <- getPats sc
return (Bind n (Hole t') sc')
getPats (App s f a) = do f' <- getPats f
a' <- getPats a
return (App s f' a')
getPats t = return t
isEmpty :: Context -> Ctxt TypeInfo -> Type -> Bool
isEmpty ctxt tyctxt ty
| (P _ tyname _, args) <- unApply ty,
Just tyinfo <- lookupCtxtExact tyname tyctxt
-- Compare all the constructor types against the type we need
-- If they *all* have an argument position where some constructor
-- clashes with the needed type, then the type we're looking for must
-- be empty
= let neededty = getRetTy ty
contys = mapMaybe getConType (con_names tyinfo) in
all (findClash neededty) contys
where
getConType n = do t <- lookupTyExact n ctxt
return (getRetTy (normalise ctxt [] t))
findClash l r
| (P _ n _, _) <- unApply l,
(P _ n' _, _) <- unApply r,
isConName n ctxt && isConName n' ctxt, n /= n'
= True
findClash (App _ f a) (App _ f' a') = findClash f f' || findClash a a'
findClash l r = False
isEmpty ctxt tyinfo ty = False
hasEmptyPat :: Context -> Ctxt TypeInfo -> Term -> Bool
hasEmptyPat ctxt tyctxt (Bind n (PVar _ ty) sc)
= isEmpty ctxt tyctxt ty || hasEmptyPat ctxt tyctxt sc
hasEmptyPat ctxt tyctxt _ = False
-- Find names which are applied to a function in a Rig1/Rig0 position
-- 'rig' is the multiplicity of the outer argument. When we go under a
-- function application, multiply them (it only needs to be Rig1 if it's
-- a linear argument to a linear argument; it needs to be a Rig0 if it's
-- Rig0 at any level)
findLinear :: RigCount -> IState -> [Name] -> Term -> [(Name, RigCount)]
findLinear rig ist env tm
| (P _ f _, args) <- unApply tm,
f `notElem` env,
Just ty_in <- lookupTyExact f (tt_ctxt ist)
= let ty = whnfArgs (tt_ctxt ist) [] ty_in in
combineRig $ findLinArg ty args
where
findLinArg (Bind n (Pi c _ _ _) sc) (P _ a _ : as)
= (a, rigMult rig c) : findLinArg sc as
findLinArg (Bind n (Pi c _ _ _) sc) (a : as)
= findLinear (rigMult c rig) ist env a ++
findLinArg (whnf (tt_ctxt ist) [] (substV a sc)) as
findLinArg ty (a : as)
= findLinear rig ist env a ++ findLinArg ty as
findLinArg _ [] = []
-- If a name is used multiple times in a pattern, take the least restrictive
-- use of it
combineRig [] = []
combineRig ((n, r) : rs)
= let (rs', rig) = findRestrictive n r [] rs in
(n, rig) : combineRig rs'
findRestrictive n r acc [] = (acc, r)
findRestrictive n r acc ((n', r') : rs)
| n == n' = findRestrictive n (max r r') acc rs
| otherwise = findRestrictive n r ((n', r') : acc) rs
findLinear rig ist env (App _ f a)
= nub $ findLinear rig ist env f ++ findLinear rig ist env a
findLinear rig ist env (Bind n b sc) = findLinear rig ist (n : env) sc
findLinear rig ist _ _ = []
setLinear :: [(Name, RigCount)] -> Term -> Term
setLinear ns (Bind n b@(PVar r t) sc)
| Just r <- lookup n ns = Bind n (PVar r t) (setLinear ns sc)
| otherwise = Bind n b (setLinear ns sc)
setLinear ns tm = tm
linearArg :: Type -> Bool
linearArg (Bind n (Pi Rig1 _ _ _) sc) = True
linearArg (Bind n (Pi _ _ _ _) sc) = linearArg sc
linearArg _ = False
-- Rule out alternatives that don't return the same type as the head of the goal
-- (If there are none left as a result, do nothing)
pruneByType :: Bool -> -- In an impossible clause
Env -> Term -> -- head of the goal
Type -> -- goal
IState -> [PTerm] -> [PTerm]
-- if an alternative has a locally bound name at the head, take it
pruneByType imp env t goalty c as
| Just a <- locallyBound as = [a]
where
locallyBound [] = Nothing
locallyBound (t:ts)
| Just n <- getName t,
n `elem` map fstEnv env = Just t
| otherwise = locallyBound ts
getName (PRef _ _ n) = Just n
getName (PApp _ (PRef _ _ (UN l)) [_, _, arg]) -- ignore Delays
| l == txt "Delay" = getName (getTm arg)
getName (PApp _ f _) = getName f
getName (PHidden t) = getName t
getName _ = Nothing
-- 'n' is the name at the head of the goal type
pruneByType imp env (P _ n _) goalty ist as
-- if the goal type is polymorphic, keep everything
| Nothing <- lookupTyExact n ctxt = as
-- if the goal type is a ?metavariable, keep everything
| Just _ <- lookup n (idris_metavars ist) = as
| otherwise
= let asV = filter (headIs True n) as
as' = filter (headIs False n) as in
case as' of
[] -> asV
_ -> as'
where
ctxt = tt_ctxt ist
-- Get the function at the head of the alternative and see if it's
-- a plausible match against the goal type. Keep if so. Also keep if
-- there is a possible coercion to the goal type.
headIs var f (PRef _ _ f') = typeHead var f f'
headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg])
| l == txt "Delay" = headIs var f (getTm arg)
headIs var f (PApp _ (PRef _ _ f') _) = typeHead var f f'
headIs var f (PApp _ f' _) = headIs var f f'
headIs var f (PPi _ _ _ _ sc) = headIs var f sc
headIs var f (PHidden t) = headIs var f t
headIs var f t = True -- keep if it's not an application
typeHead var f f'
= -- trace ("Trying " ++ show f' ++ " for " ++ show n) $
case lookupTyExact f' ctxt of
Just ty -> case unApply (getRetTy ty) of
(P _ ctyn _, _) | isTConName ctyn ctxt && not (ctyn == f)
-> False
_ -> let ty' = normalise ctxt [] ty in
-- trace ("Trying " ++ show f' ++ " : " ++ show (getRetTy ty') ++ " for " ++ show goalty
-- ++ "\nMATCH: " ++ show (pat, matching (getRetTy ty') goalty)) $
case unApply (getRetTy ty') of
(V _, _) ->
isPlausible ist var env n ty
_ -> matchingTypes imp (getRetTy ty') goalty
|| isCoercion (getRetTy ty') goalty
-- May be useful to keep for debugging purposes for a bit:
-- let res = matching (getRetTy ty') goalty in
-- traceWhen (not res)
-- ("Rejecting " ++ show (getRetTy ty', goalty)) res
_ -> False
matchingTypes True = matchingHead
matchingTypes False = matching
-- If the goal is a constructor, it must match the suggested function type
matching (P _ ctyn _) (P _ n' _)
| isTConName n' ctxt && isTConName ctyn ctxt = ctyn == n'
| otherwise = True
-- Variables match anything
matching (V _) _ = True
matching _ (V _) = True
matching _ (P _ n _) = not (isTConName n ctxt)
matching (P _ n _) _ = not (isTConName n ctxt)
-- Binders are a plausible match, so keep them
matching (Bind n _ sc) _ = True
matching _ (Bind n _ sc) = True
-- If we hit a function name, it's a plausible match
matching apl@(App _ _ _) apr@(App _ _ _)
| (P _ fl _, argsl) <- unApply apl,
(P _ fr _, argsr) <- unApply apr
= fl == fr && and (zipWith matching argsl argsr)
|| (not (isConName fl ctxt && isConName fr ctxt))
-- If the application structures aren't easily comparable, it's a
-- plausible match
matching (App _ f a) (App _ f' a') = True
matching (TType _) (TType _) = True
matching (UType _) (UType _) = True
matching l r = l == r
-- In impossible-case mode, only look at the heads (this is to account for
-- the non type-directed case with 'impossible' - we'd be ruling out
-- too much and wouldn't find the mismatch we're looking for)
matchingHead apl@(App _ _ _) apr@(App _ _ _)
| (P _ fl _, argsl) <- unApply apl,
(P _ fr _, argsr) <- unApply apr,
isConName fl ctxt && isConName fr ctxt
= fl == fr
matchingHead _ _ = True
-- Return whether there is a possible coercion between the return type
-- of an alternative and the goal type
isCoercion rty gty | (P _ r _, _) <- unApply rty
= not (null (getCoercionsBetween r gty))
isCoercion _ _ = False
getCoercionsBetween :: Name -> Type -> [Name]
getCoercionsBetween r goal
= let cs = getCoercionsTo ist goal in
findCoercions r cs
where findCoercions t [] = []
findCoercions t (n : ns) =
let ps = case lookupTy n (tt_ctxt ist) of
[ty'] -> let as = map snd (getArgTys (normalise (tt_ctxt ist) [] ty')) in
[n | any useR as]
_ -> [] in
ps ++ findCoercions t ns
useR ty =
case unApply (getRetTy ty) of
(P _ t _, _) -> t == r
_ -> False
pruneByType _ _ t _ _ as = as
-- Could the name feasibly be the return type?
-- If there is an interface constraint on the return type, and no implementation
-- in the environment or globally for that name, then no
-- Otherwise, yes
-- (FIXME: This isn't complete, but I'm leaving it here and coming back
-- to it later - just returns 'var' for now. EB)
isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool
isPlausible ist var env n ty
= let (hvar, _) = collectConstraints [] [] ty in
case hvar of
Nothing -> True
Just rth -> var -- trace (show (rth, interfaces)) var
where
collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->
(Maybe Name, [(Term, [Name])])
collectConstraints env tcs (Bind n (Pi _ _ ty _) sc)
= let tcs' = case unApply ty of
(P _ c _, _) ->
case lookupCtxtExact c (idris_interfaces ist) of
Just tc -> ((ty, map fst (interface_implementations tc))
: tcs)
Nothing -> tcs
_ -> tcs
in
collectConstraints (n : env) tcs' sc
collectConstraints env tcs t
| (V i, _) <- unApply t = (Just (env !! i), tcs)
| otherwise = (Nothing, tcs)