{-# LANGUAGE DeriveFunctor, FlexibleContexts, FlexibleInstances,
MultiParamTypeClasses, PatternGuards #-}
module Idris.Core.Typecheck where
import Idris.Core.Evaluate
import Idris.Core.TT
import Control.Monad.State
convertsC :: Context -> Env -> Term -> Term -> StateT UCs TC ()
convertsC ctxt env x y =
do let hs = map fstEnv (filter isHole env)
c1 <- convEq ctxt hs x y
if c1 then return ()
else
do c2 <- convEq ctxt hs (finalise (normalise ctxt env x))
(finalise (normalise ctxt env y))
if c2 then return ()
else lift $ tfail (CantConvert
(finalise (normalise ctxt env x))
(finalise (normalise ctxt env y)) (errEnv env))
converts :: Context -> Env -> Term -> Term -> TC ()
converts ctxt env x y
= let hs = map fstEnv (filter isHole env) in
case convEq' ctxt hs x y of
OK True -> return ()
_ -> case convEq' ctxt hs (finalise (normalise ctxt env x))
(finalise (normalise ctxt env y)) of
OK True -> return ()
_ -> tfail (CantConvert
(finalise (normalise ctxt env x))
(finalise (normalise ctxt env y)) (errEnv env))
isHole (n, _, Hole _) = True
isHole _ = False
errEnv = map (\(x, _, b) -> (x, binderTy b))
isType :: Context -> Env -> Term -> TC ()
isType ctxt env tm = isType' (normalise ctxt env tm)
where isType' tm | isUniverse tm = return ()
| otherwise = fail (showEnv env tm ++ " is not a Type")
convType :: String -> Context -> Env -> Term -> StateT UCs TC ()
convType tcns ctxt env tm =
do (v, cs) <- get
put (v + 1, cs)
case normalise ctxt env tm of
UType _ -> return ()
_ -> convertsC ctxt env tm (TType (UVar tcns v))
recheck :: String -> Context -> Env -> Raw -> Term -> TC (Term, Type, UCs)
recheck = recheck_borrowing False []
recheck_borrowing :: Bool -> [Name] -> String -> Context -> Env -> Raw -> Term ->
TC (Term, Type, UCs)
recheck_borrowing uniq_check bs tcns ctxt env tm orig
= let v = next_tvar ctxt in
case runStateT (check' False tcns ctxt env tm) (v, []) of
Error (IncompleteTerm _) -> Error $ IncompleteTerm orig
Error e -> Error e
OK ((tm, ty), constraints) ->
do when uniq_check $ checkUnique bs ctxt env tm
return (tm, ty, constraints)
check :: Context -> Env -> Raw -> TC (Term, Type)
check ctxt env tm
= evalStateT (check' True [] ctxt env tm) (0, [])
check' :: Bool -> String -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)
check' holes tcns ctxt env top
= do (tm, ty, _) <- chk Rig1 (TType (UVar tcns (-5))) Nothing env top
return (tm, ty)
where
smaller (UType NullType) _ = UType NullType
smaller _ (UType NullType) = UType NullType
smaller (UType u) _ = UType u
smaller _ (UType u) = UType u
smaller x _ = x
astate | holes = MaybeHoles
| otherwise = Complete
chk :: RigCount ->
Type ->
Maybe UExp ->
Env -> Raw -> StateT UCs TC (Term, Type, [Name])
chk rigc u lvl env (Var n)
| Just (i, erig, ty) <- lookupTyEnv n env
= case rigSafe holes erig rigc n of
Nothing -> return (P Bound n ty, ty, used rigc n)
Just msg -> lift $ tfail $ Msg msg
| [P nt n' ty] <- lookupP_all (not holes) True n ctxt
= return (P nt n' ty, ty, [])
| otherwise = do lift $ tfail $ NoSuchVariable n
where rigSafe True _ _ n = Nothing
rigSafe _ Rig1 RigW n = Just ("Trying to use linear name " ++ show n ++ " in non-linear context")
rigSafe _ Rig0 RigW n = Just ("Trying to use irrelevant name " ++ show n ++ " in relevant context")
rigSafe _ Rig0 Rig1 n = Just ("Trying to use irrelevant name " ++ show n ++ " in relevant context")
rigSafe _ _ _ n = Nothing
used Rig0 n = []
used _ n = [n]
chk rigc u lvl env ap@(RApp f RType) | not holes
= do (fv, fty, fns) <- chk rigc u Nothing env f
let fty' = case uniqueBinders (map fstEnv env) (finalise fty) of
ty@(Bind x (Pi _ i s k) t) -> ty
_ -> uniqueBinders (map fstEnv env)
$ case normalise ctxt env fty of
ty@(Bind x (Pi _ i s k) t) -> ty
_ -> normalise ctxt env fty
case fty' of
Bind x (Pi rig i (TType v') k) t ->
do (v, cs) <- get
put (v+1, ULT (UVar tcns v) v' : cs)
let apty = simplify initContext env
(Bind x (Let rig (TType v') (TType (UVar tcns v))) t)
return (App Complete fv (TType (UVar tcns v)), apty, fns)
Bind x (Pi rig i s k) t ->
do (av, aty, _) <- chk rigc u Nothing env RType
convertsC ctxt env aty s
let apty = simplify initContext env
(Bind x (Let rig aty av) t)
return (App astate fv av, apty, fns)
t -> lift $ tfail $ NonFunctionType fv fty
chk rigc u lvl env ap@(RApp f a)
= do (fv, fty, fns) <- chk rigc u Nothing env f
let (rigf, fty') =
case uniqueBinders (map fstEnv env) (finalise fty) of
ty@(Bind x (Pi rig i s k) t) -> (rig, ty)
_ -> case normalise ctxt env fty of
ty@(Bind x (Pi rig i s k) t) ->
(rig, uniqueBinders (map fstEnv env) ty)
_ -> (RigW, uniqueBinders (map fstEnv env)
(normalise ctxt env fty))
(av, aty, ans_in) <- chk (rigMult rigf rigc) u Nothing env a
let ans = case rigf of
Rig0 -> []
_ -> ans_in
case fty' of
Bind x (Pi rig i s k) t ->
do convertsC ctxt env aty s
let apty = simplify initContext env
(Bind x (Let rig aty av) t)
return (App astate fv av, apty, fns ++ ans)
t -> lift $ tfail $ NonFunctionType fv fty
chk rigc u lvl env RType
| holes = return (TType (UVal 0), TType (UVal 0), [])
| otherwise = do (v, cs) <- get
let c = ULT (UVar tcns v) (UVar tcns (v+1))
put (v+2, (c:cs))
return (TType (UVar tcns v), TType (UVar tcns (v+1)), [])
chk rigc u lvl env (RUType un)
| holes = return (UType un, TType (UVal 0), [])
| otherwise = do
return (UType un, TType (UVal 0), [])
chk rigc u lvl env (RConstant Forgot) = return (Erased, Erased, [])
chk rigc u lvl env (RConstant c) = return (Constant c, constType c, [])
where constType (I _) = Constant (AType (ATInt ITNative))
constType (BI _) = Constant (AType (ATInt ITBig))
constType (Fl _) = Constant (AType ATFloat)
constType (Ch _) = Constant (AType (ATInt ITChar))
constType (Str _) = Constant StrType
constType (B8 _) = Constant (AType (ATInt (ITFixed IT8)))
constType (B16 _) = Constant (AType (ATInt (ITFixed IT16)))
constType (B32 _) = Constant (AType (ATInt (ITFixed IT32)))
constType (B64 _) = Constant (AType (ATInt (ITFixed IT64)))
constType TheWorld = Constant WorldType
constType Forgot = Erased
constType _ = TType (UVal 0)
chk rigc u lvl env (RBind n (Pi rig i s k) t)
= do (sv, st, sns) <- chk Rig0 u Nothing (envZero env) s
(v, cs) <- get
(kv, kt, _) <- chk Rig0 u Nothing (envZero env) k
put (v+1, cs)
let maxu = case lvl of
Nothing -> UVar tcns v
Just v' -> v'
(tv, tt, tns) <- chk Rig0 st (Just maxu) ((n, Rig0, Pi Rig0 i sv kv) : envZero env) t
case (normalise ctxt env st, normalise ctxt env tt) of
(TType su, TType tu) -> do
when (not holes) $ do (v, cs) <- get
put (v, ULE su maxu :
ULE tu maxu : cs)
let k' = TType (UVar tcns v) `smaller` st `smaller` kv `smaller` u
return (Bind n (Pi rig i (uniqueBinders (map fstEnv env) sv) k')
(pToV n tv), k', sns ++ tns)
(un, un') ->
let k' = st `smaller` kv `smaller` un `smaller` un' `smaller` u in
return (Bind n (Pi rig i (uniqueBinders (map fstEnv env) sv) k')
(pToV n tv), k', sns ++ tns)
chk rigc_in u lvl env (RBind n b sc)
= do (b', bt', bns) <- checkBinder b
(scv, sct, scns) <- chk rigc (smaller bt' u) Nothing ((n, getCount b, b'):env) sc
checkUsageOK (getCount b) scns
discharge n b' bt' (pToV n scv) (pToV n sct) (bns ++ scns)
where
rigc = case rigc_in of
Rig0 -> Rig0
_ -> Rig1
getCount (Pi rig _ _ _) = rigMult rigc rig
getCount (PVar rig _) = rigMult rigc rig
getCount (Lam rig _) = rigMult rigc rig
getCount (Let rig _ _) = rigMult rigc rig
getCount _ = rigMult rigc RigW
checkUsageOK Rig0 _ = return ()
checkUsageOK RigW _ = return ()
checkUsageOK Rig1 ns
= let used = length (filter (==n) ns) in
if used == 1 then return ()
else lift $ tfail $ Msg $ "There are " ++ (show used) ++
" uses of linear name " ++ show n
checkBinder (Lam rig t)
= do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
convType tcns ctxt env tt
return (Lam rig tv, tt, [])
checkBinder (Let rig t v)
= do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
(vv, vt, vns) <- chk (rigMult rig rigc) u Nothing env v
convertsC ctxt env vt tv
convType tcns ctxt env tt
return (Let rig tv vv, tt, vns)
checkBinder (NLet t v)
= do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
(vv, vt, vns) <- chk rigc u Nothing env v
convertsC ctxt env vt tv
convType tcns ctxt env tt
return (NLet tv vv, tt, vns)
checkBinder (Hole t)
| not holes = lift $ tfail (IncompleteTerm undefined)
| otherwise
= do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
convType tcns ctxt env tt
return (Hole tv, tt, [])
checkBinder (GHole i ns t)
= do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
convType tcns ctxt env tt
return (GHole i ns tv, tt, [])
checkBinder (Guess t v)
| not holes = lift $ tfail (IncompleteTerm undefined)
| otherwise
= do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
(vv, vt, vns) <- chk rigc u Nothing env v
convertsC ctxt env vt tv
convType tcns ctxt env tt
return (Guess tv vv, tt, vns)
checkBinder (PVar rig t)
= do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
convType tcns ctxt env tt
return (PVar rig tv, tt, [])
checkBinder (PVTy t)
= do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
convType tcns ctxt env tt
return (PVTy tv, tt, [])
discharge n (Lam r t) bt scv sct ns
= return (Bind n (Lam r t) scv, Bind n (Pi r Nothing t bt) sct, ns)
discharge n (Pi r i t k) bt scv sct ns
= return (Bind n (Pi r i t k) scv, sct, ns)
discharge n (Let r t v) bt scv sct ns
= return (Bind n (Let r t v) scv, Bind n (Let r t v) sct, ns)
discharge n (NLet t v) bt scv sct ns
= return (Bind n (NLet t v) scv, Bind n (Let RigW t v) sct, ns)
discharge n (Hole t) bt scv sct ns
= return (Bind n (Hole t) scv, sct, ns)
discharge n (GHole i ns t) bt scv sct uns
= return (Bind n (GHole i ns t) scv, sct, uns)
discharge n (Guess t v) bt scv sct ns
= return (Bind n (Guess t v) scv, sct, ns)
discharge n (PVar r t) bt scv sct ns
= return (Bind n (PVar r t) scv, Bind n (PVTy t) sct, ns)
discharge n (PVTy t) bt scv sct ns
= return (Bind n (PVTy t) scv, sct, ns)
data UniqueUse = Never
| Once
| LendOnly
| Many
deriving Eq
checkUnique :: [Name] -> Context -> Env -> Term -> TC ()
checkUnique borrowed ctxt env tm
= evalStateT (chkBinders env (explicitNames tm)) []
where
isVar (P _ _ _) = True
isVar (V _) = True
isVar _ = False
chkBinders :: Env -> Term -> StateT [(Name, (UniqueUse, Universe))] TC ()
chkBinders env (V i) | length env > i = chkName (fstEnv (env!!i))
chkBinders env (P _ n _) = chkName n
chkBinders env (App _ (App _ (P _ (NS (UN lend) [owner]) _) t) a)
| isVar a && owner == txt "Ownership" &&
(lend == txt "lend" || lend == txt "Read")
= do chkBinders env t
st <- get
put (filter (\(n, (ok, _)) -> ok /= LendOnly) st)
chkBinders env a
put st
chkBinders env (App _ f a) = do chkBinders env f; chkBinders env a
chkBinders env (Bind n b t)
= do chkBinderName env n b
st <- get
case b of
Let _ t v -> chkBinders env v
_ -> return ()
chkBinders ((n, Rig0, b) : env) t
chkBinders env t = return ()
chkBinderName :: Env -> Name -> Binder Term ->
StateT [(Name, (UniqueUse, Universe))] TC ()
chkBinderName env n b
= do let rawty = forgetEnv (map fstEnv env) (binderTy b)
(_, kind) <- lift $ check ctxt env rawty
case kind of
UType UniqueType -> do ns <- get
if n `elem` borrowed
then put ((n, (LendOnly, NullType)) : ns)
else put ((n, (Once, UniqueType)) : ns)
UType NullType -> do ns <- get
put ((n, (Many, NullType)) : ns)
UType AllTypes -> do ns <- get
put ((n, (Once, AllTypes)) : ns)
_ -> return ()
chkName n
= do ns <- get
case lookup n ns of
Nothing -> return ()
Just (Many, k) -> return ()
Just (Never, k) -> lift $ tfail (UniqueError k n)
Just (LendOnly, k) -> lift $ tfail (UniqueError k n)
Just (Once, k) -> put ((n, (Never, k)) :
filter (\x -> fst x /= n) ns)