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