{-# LANGUAGE TupleSections, NamedFieldPuns #-}
module Extract where
import Prelude hiding (pi, null)
#if !MIN_VERSION_base(4,8,0)
import Control.Applicative ((<$>), (<*>))
#endif
import Control.Monad.Except (runExceptT)
import Control.Monad.Reader (runReaderT)
import Control.Monad.State (runStateT)
import qualified Data.Traversable as Traversable
import qualified Data.Maybe as Maybe
import Text.PrettyPrint
import Polarity as Pol
import Abstract
import Value
import Eval
import TCM
import TraceError
import Util
traceExtrM :: Monad m => String -> m ()
traceExtrM :: forall (m :: * -> *). Monad m => String -> m ()
traceExtrM String
s = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
runExtract :: Signature -> TypeCheck a -> IO (Either TraceError (a, TCState))
Signature
sig TypeCheck a
k = ExceptT TraceError IO (a, TCState)
-> IO (Either TraceError (a, TCState))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ReaderT TCContext (ExceptT TraceError IO) (a, TCState)
-> TCContext -> ExceptT TraceError IO (a, TCState)
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (TypeCheck a
-> TCState
-> ReaderT TCContext (ExceptT TraceError IO) (a, TCState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT TypeCheck a
k (Signature -> TCState
initWithSig Signature
sig)) TCContext
emptyContext)
type FExpr = Expr
type FDeclaration = Declaration
type FClause = Clause
type FPattern = Pattern
type FConstructor = Constructor
type FTypeSig = TypeSig
type FFun = Fun
type FTelescope = Telescope
type FTVal = TVal
extractDecls :: [EDeclaration] -> TypeCheck [FDeclaration]
[EDeclaration]
ds = [[EDeclaration]] -> [EDeclaration]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[EDeclaration]] -> [EDeclaration])
-> StateT
TCState
(ReaderT TCContext (ExceptT TraceError IO))
[[EDeclaration]]
-> TypeCheck [EDeclaration]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (EDeclaration -> TypeCheck [EDeclaration])
-> [EDeclaration]
-> StateT
TCState
(ReaderT TCContext (ExceptT TraceError IO))
[[EDeclaration]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM EDeclaration -> TypeCheck [EDeclaration]
extractDecl [EDeclaration]
ds
extractDecl :: EDeclaration -> TypeCheck [FDeclaration]
EDeclaration
d =
case EDeclaration
d of
MutualDecl Bool
_ [EDeclaration]
ds -> [EDeclaration] -> TypeCheck [EDeclaration]
extractDecls [EDeclaration]
ds
OverrideDecl{} -> String -> TypeCheck [EDeclaration]
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> TypeCheck [EDeclaration])
-> String -> TypeCheck [EDeclaration]
forall a b. (a -> b) -> a -> b
$ String
"extractDecls internal error: overrides impossible"
MutualFunDecl Bool
_ Co
co [Fun]
funs -> Co -> [Fun] -> TypeCheck [EDeclaration]
extractFuns Co
co [Fun]
funs
FunDecl Co
co Fun
fun -> Co -> Fun -> TypeCheck [EDeclaration]
extractFun Co
co Fun
fun
LetDecl Bool
evl Name
x Telescope
tel (Just FKind
t) FKind
e | Telescope -> Bool
forall a. Null a => a -> Bool
null Telescope
tel -> Bool -> Name -> FKind -> FKind -> TypeCheck [EDeclaration]
extractLet Bool
evl Name
x FKind
t FKind
e
PatternDecl{} -> [EDeclaration] -> TypeCheck [EDeclaration]
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
DataDecl Name
n Sized
_ Co
co [Pol]
_ Telescope
tel FKind
ty [Constructor]
cs [Name]
fields -> Name
-> Co
-> Telescope
-> FKind
-> [Constructor]
-> TypeCheck [EDeclaration]
extractDataDecl Name
n Co
co Telescope
tel FKind
ty [Constructor]
cs
extractFuns :: Co -> [Fun] -> TypeCheck [FDeclaration]
Co
co [Fun]
funs = do
funs <- [[Fun]] -> [Fun]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Fun]] -> [Fun])
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [[Fun]]
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) [Fun]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Fun
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [Fun])
-> [Fun]
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [[Fun]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Fun
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) [Fun]
extractFunTypeSig [Fun]
funs
concat <$> mapM (extractFun co) funs
extractFun :: Co -> Fun -> TypeCheck [FDeclaration]
Co
co (Fun (TypeSig Name
n FKind
t) Name
n' Arity
ar [Clause]
cls) = do
tv <- FKind -> TypeCheck TVal
whnf' FKind
t
cls <- concat <$> mapM (extractClause n tv) cls
return [ FunDecl co $ Fun (TypeSig n t) n' ar cls
]
extractFunTypeSig :: Fun -> TypeCheck [Fun]
(Fun ts :: TySig FKind
ts@(TypeSig Name
n FKind
t) Name
n' Arity
ar [Clause]
cls) = Name
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) [Fun]
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) [Fun]
forall a. Name -> TypeCheck [a] -> TypeCheck [a]
extractIfTerm Name
n (StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) [Fun]
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [Fun])
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) [Fun]
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) [Fun]
forall a b. (a -> b) -> a -> b
$ do
ts@(TypeSig n t) <- TySig FKind -> TypeCheck (TySig FKind)
extractTypeSig TySig FKind
ts
setExtrTyp n' t
return [Fun ts n' ar cls]
extractLet :: Bool -> Name -> Type -> Expr -> TypeCheck [FDeclaration]
Bool
evl Name
n FKind
t FKind
e = Name -> TypeCheck [EDeclaration] -> TypeCheck [EDeclaration]
forall a. Name -> TypeCheck [a] -> TypeCheck [a]
extractIfTerm Name
n (TypeCheck [EDeclaration] -> TypeCheck [EDeclaration])
-> TypeCheck [EDeclaration] -> TypeCheck [EDeclaration]
forall a b. (a -> b) -> a -> b
$ do
TypeSig n t <- TySig FKind -> TypeCheck (TySig FKind)
extractTypeSig (Name -> FKind -> TySig FKind
forall a. Name -> a -> TySig a
TypeSig Name
n FKind
t)
e <- extractCheck e =<< whnf' t
return [LetDecl evl n emptyTel (Just t) e]
extractTypeSig :: TypeSig -> TypeCheck FTypeSig
(TypeSig Name
n FKind
t) = do
t <- TVal -> TypeCheck FKind
extractType (TVal -> TypeCheck FKind) -> TypeCheck TVal -> TypeCheck FKind
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< FKind -> TypeCheck TVal
whnf' FKind
t
setExtrTyp n t
return $ TypeSig n t
extractIfTerm :: Name -> TypeCheck [a] -> TypeCheck [a]
Name
n TypeCheck [a]
cont = do
k <- SigDef -> Kind
symbolKind (SigDef -> Kind)
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Kind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
forall (m :: * -> *). MonadSig m => Name -> m SigDef
lookupSymb Name
n
if k == NoKind || lowerKind k == SortC Tm then cont else return []
extractDataDecl :: Name -> Co -> Telescope -> Type -> [Constructor] -> TypeCheck [FDeclaration]
Name
n Co
co Telescope
tel FKind
ty [Constructor]
cs = do
tel' <- Telescope -> TypeCheck Telescope
extractKindTel Telescope
tel
Just core <- addBinds tel $ extractKind =<< whnf' ty
cs <- mapM (extractConstructor tel) cs
return [DataDecl n NotSized co [] tel' core cs []]
extractConstructor :: Telescope -> Constructor -> TypeCheck FConstructor
Telescope
tel0 (Constructor QName
n ParamPats
pars FKind
t) = do
let tel :: Telescope
tel = Telescope
tel0
t' <- TVal -> TypeCheck FKind
extractType (TVal -> TypeCheck FKind) -> TypeCheck TVal -> TypeCheck FKind
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Env -> FKind -> TypeCheck TVal
whnf Env
forall a. Environ a
emptyEnv (Telescope -> FKind -> FKind
teleToTypeErase Telescope
tel FKind
t)
setExtrTypQ n t'
let (tel',core) = typeToTele' (size tel) t'
return $ Constructor n pars core
extractClause :: Name -> FTVal -> Clause -> TypeCheck [FClause]
Name
f TVal
tv (Clause TeleVal
_ [Pattern]
pl Maybe FKind
Nothing) = [Clause]
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause]
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
extractClause Name
f TVal
tv cl :: Clause
cl@(Clause TeleVal
vtel [Pattern]
pl (Just FKind
rhs)) = do
String
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) ()
forall (m :: * -> *). Monad m => String -> m ()
traceM (String
"extracting clause " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
render (Name -> Clause -> Doc
forall a. Pretty a => a -> Clause -> Doc
prettyClause Name
f Clause
cl)
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n at type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TVal -> String
forall a. Show a => a -> String
show TVal
tv)
[Pattern]
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause]
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause]
forall a. [Pattern] -> TypeCheck a -> TypeCheck a
introPatVars [Pattern]
pl (StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause]
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause])
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause]
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause]
forall a b. (a -> b) -> a -> b
$
TVal
-> [Pattern]
-> ([Pattern]
-> TVal
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause])
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause]
forall a.
TVal
-> [Pattern] -> ([Pattern] -> TVal -> TypeCheck a) -> TypeCheck a
extractPatterns TVal
tv [Pattern]
pl (([Pattern]
-> TVal
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause])
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause])
-> ([Pattern]
-> TVal
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause])
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [Clause]
forall a b. (a -> b) -> a -> b
$ \ [Pattern]
pl TVal
tv -> do
rhs <- FKind -> TVal -> TypeCheck FKind
extractCheck FKind
rhs TVal
tv
return [Clause vtel pl (Just rhs)]
extractPatterns :: FTVal -> [Pattern] ->
([FPattern] -> FTVal -> TypeCheck a) -> TypeCheck a
TVal
tv [] [Pattern] -> TVal -> TypeCheck a
cont = [Pattern] -> TVal -> TypeCheck a
cont [] TVal
tv
extractPatterns TVal
tv (Pattern
p:[Pattern]
ps) [Pattern] -> TVal -> TypeCheck a
cont =
TVal
-> Pattern -> ([Pattern] -> TVal -> TypeCheck a) -> TypeCheck a
forall a.
TVal
-> Pattern -> ([Pattern] -> TVal -> TypeCheck a) -> TypeCheck a
extractPattern TVal
tv Pattern
p (([Pattern] -> TVal -> TypeCheck a) -> TypeCheck a)
-> ([Pattern] -> TVal -> TypeCheck a) -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ \ [Pattern]
pl TVal
tv ->
TVal
-> [Pattern] -> ([Pattern] -> TVal -> TypeCheck a) -> TypeCheck a
forall a.
TVal
-> [Pattern] -> ([Pattern] -> TVal -> TypeCheck a) -> TypeCheck a
extractPatterns TVal
tv [Pattern]
ps (([Pattern] -> TVal -> TypeCheck a) -> TypeCheck a)
-> ([Pattern] -> TVal -> TypeCheck a) -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ \ [Pattern]
ps TVal
tv ->
[Pattern] -> TVal -> TypeCheck a
cont ([Pattern]
pl [Pattern] -> [Pattern] -> [Pattern]
forall a. [a] -> [a] -> [a]
++ [Pattern]
ps) TVal
tv
extractPattern :: FTVal -> Pattern ->
([FPattern] -> FTVal -> TypeCheck a) -> TypeCheck a
TVal
tv Pattern
p [Pattern] -> TVal -> TypeCheck a
cont = do
String
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) ()
forall (m :: * -> *). Monad m => String -> m ()
traceM (String
"extracting pattern " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
render (Pattern -> Doc
forall a. Pretty a => a -> Doc
pretty Pattern
p) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" at type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TVal -> String
forall a. Show a => a -> String
show TVal
tv)
fv <- TVal -> TypeCheck FunView
funView TVal
tv
case fv of
EraseArg TVal
tv -> [Pattern] -> TVal -> TypeCheck a
cont [] TVal
tv
Forall Name
x Domain
dom TVal
fv -> do
xv <- FKind -> TypeCheck TVal
whnf' (Pattern -> FKind
patternToExpr Pattern
p)
bv <- app fv xv
case p of
ErasedP (VarP Name
y) -> Name -> Domain -> TypeCheck a -> TypeCheck a
forall a.
Name
-> Domain
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. MonadCxt m => Name -> Domain -> m a -> m a
setTypeOfName Name
y Domain
dom (TypeCheck a -> TypeCheck a) -> TypeCheck a -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ [Pattern] -> TVal -> TypeCheck a
cont [] TVal
bv
Pattern
_ -> [Pattern] -> TVal -> TypeCheck a
cont [] TVal
bv
Arrow TVal
av TVal
bv -> TVal -> Pattern -> ([Pattern] -> TypeCheck a) -> TypeCheck a
forall a.
TVal -> Pattern -> ([Pattern] -> TypeCheck a) -> TypeCheck a
extractPattern' TVal
av Pattern
p (([Pattern] -> TVal -> TypeCheck a)
-> TVal -> [Pattern] -> TypeCheck a
forall a b c. (a -> b -> c) -> b -> a -> c
flip [Pattern] -> TVal -> TypeCheck a
cont TVal
bv)
extractPattern' :: FTVal -> Pattern ->
([FPattern] -> TypeCheck a) -> TypeCheck a
TVal
av Pattern
p [Pattern] -> TypeCheck a
cont =
case Pattern
p of
VarP Name
y -> Name -> Domain -> TypeCheck a -> TypeCheck a
forall a.
Name
-> Domain
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. MonadCxt m => Name -> Domain -> m a -> m a
setTypeOfName Name
y (TVal -> Domain
forall a. a -> Dom a
defaultDomain TVal
av) (TypeCheck a -> TypeCheck a) -> TypeCheck a -> TypeCheck a
forall a b. (a -> b) -> a -> b
$
[Pattern] -> TypeCheck a
cont [Name -> Pattern
forall e. Name -> Pat e
VarP Name
y]
PairP Pattern
p1 Pattern
p2 -> do
view <- TVal -> TypeCheck ProdView
prodView TVal
av
let (av1, av2) = case view of
Prod TVal
av1 TVal
av2 -> (TVal
av1, TVal
av2)
ProdView
_ -> (TVal
av, TVal
av)
extractPattern' av1 p1 $ \ [Pattern]
ps1 -> do
TVal -> Pattern -> ([Pattern] -> TypeCheck a) -> TypeCheck a
forall a.
TVal -> Pattern -> ([Pattern] -> TypeCheck a) -> TypeCheck a
extractPattern' TVal
av2 Pattern
p2 (([Pattern] -> TypeCheck a) -> TypeCheck a)
-> ([Pattern] -> TypeCheck a) -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ \ [Pattern]
ps2 ->
let ps :: [Pat e] -> [Pat e] -> [Pat e]
ps [] [Pat e]
ps2 = [Pat e]
ps2
ps [Pat e]
ps1 [] = [Pat e]
ps1
ps [Pat e
p1] [Pat e
p2] = [Pat e -> Pat e -> Pat e
forall e. Pat e -> Pat e -> Pat e
PairP Pat e
p1 Pat e
p2]
in [Pattern] -> TypeCheck a
cont ([Pattern] -> TypeCheck a) -> [Pattern] -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ [Pattern] -> [Pattern] -> [Pattern]
forall {e}. [Pat e] -> [Pat e] -> [Pat e]
ps [Pattern]
ps1 [Pattern]
ps2
ConP PatternInfo
pi QName
n [Pattern]
ps -> do
tv <- QName -> TVal -> TypeCheck TVal
extrConType QName
n TVal
av
extractPatterns tv ps $ \ [Pattern]
ps TVal
_ ->
[Pattern] -> TypeCheck a
cont [PatternInfo -> QName -> [Pattern] -> Pattern
forall e. PatternInfo -> QName -> [Pat e] -> Pat e
ConP PatternInfo
pi QName
n [Pattern]
ps]
Pattern
_ -> [Pattern] -> TypeCheck a
cont []
extrConType :: QName -> FTVal -> TypeCheck FTVal
extrConType :: QName -> TVal -> TypeCheck TVal
extrConType QName
c TVal
av = do
ConSig { conPars, extrTyp, dataPars } <- QName
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
forall (m :: * -> *). MonadSig m => QName -> m SigDef
lookupSymbQ QName
c
traceExtrM ("extrConType " ++ show c ++ " has extrTyp = " ++ show extrTyp)
tv <- whnf' extrTyp
numPars <- maybe (return dataPars) (const $ throwErrorMsg $ "NYI: extrConType for pattern parameters") conPars
case numPars of
Int
0 -> TVal -> TypeCheck TVal
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return TVal
tv
Int
_ -> do
case TVal
av of
VApp (VDef (DefId IdKind
DatK QName
d)) [TVal]
vs -> do
DataSig { positivity } <- QName
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
forall (m :: * -> *). MonadSig m => QName -> m SigDef
lookupSymbQ QName
d
traceExtrM ("extrConType " ++ show c ++ "; data type has positivity = " ++ show positivity)
let pars a
0 [pol]
pols [TVal]
vs = []
pars a
n (pol
pol:[pol]
pols) [TVal]
vs | pol -> Bool
forall pol. Polarity pol => pol -> Bool
erased pol
pol = TVal
VIrr TVal -> [TVal] -> [TVal]
forall a. a -> [a] -> [a]
: a -> [pol] -> [TVal] -> [TVal]
pars (a
na -> a -> a
forall a. Num a => a -> a -> a
-a
1) [pol]
pols [TVal]
vs
pars a
n (pol
pol:[pol]
pols) (TVal
v:[TVal]
vs) = TVal
v TVal -> [TVal] -> [TVal]
forall a. a -> [a] -> [a]
: a -> [pol] -> [TVal] -> [TVal]
pars (a
na -> a -> a
forall a. Num a => a -> a -> a
-a
1) [pol]
pols [TVal]
vs
pars a
n [pol]
pols [TVal]
vs = String -> [TVal]
forall a. HasCallStack => String -> a
error (String -> [TVal]) -> String -> [TVal]
forall a b. (a -> b) -> a -> b
$ String
"pars " 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]
++ [pol] -> String
forall a. Show a => a -> String
show [pol]
pols String -> String -> String
forall a. [a] -> [a] -> [a]
++ [TVal] -> String
forall a. Show a => a -> String
show [TVal]
vs
piApps tv $ pars numPars positivity $ vs ++ repeat VIrr
TVal
_ -> TVal -> [TVal] -> TypeCheck TVal
piApps TVal
tv ([TVal] -> TypeCheck TVal) -> [TVal] -> TypeCheck TVal
forall a b. (a -> b) -> a -> b
$ Int -> TVal -> [TVal]
forall a. Int -> a -> [a]
replicate Int
numPars TVal
VIrr
extractInfer :: Expr -> TypeCheck (FExpr, FTVal)
FKind
e = do
case FKind
e of
Var Name
x -> (Name -> FKind
Var Name
x,) (TVal -> (FKind, TVal))
-> (CxtE Domain -> TVal) -> CxtE Domain -> (FKind, TVal)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Domain -> TVal
forall a. Dom a -> a
typ (Domain -> TVal) -> (CxtE Domain -> Domain) -> CxtE Domain -> TVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtE Domain -> Domain
forall a. CxtE a -> a
domain (CxtE Domain -> (FKind, TVal))
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) (CxtE Domain)
-> TypeCheck (FKind, TVal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) (CxtE Domain)
forall (m :: * -> *). MonadCxt m => Name -> m (CxtE Domain)
lookupName1 Name
x
App FKind
f FKind
e0 -> do
let (Bool
er, FKind
e) = FKind -> (Bool, FKind)
isErasedExpr FKind
e0
(f, tv) <- FKind -> TypeCheck (FKind, TVal)
extractInfer FKind
f
fv <- funView tv
case fv of
EraseArg TVal
bv -> (FKind, TVal) -> TypeCheck (FKind, TVal)
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (FKind
f,TVal
bv)
Forall Name
x Domain
dom TVal
fv -> do
e <- FKind -> TVal -> TypeCheck FKind
extractTypeAt FKind
e (Domain -> TVal
forall a. Dom a -> a
typ Domain
dom)
bv <- app fv =<< whnf' e
return $ (App f (erasedExpr e), bv)
Arrow TVal
av TVal
bv -> (FKind, TVal) -> TypeCheck (FKind, TVal)
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (if Bool
er then FKind
f else FKind -> FKind -> FKind
App FKind
f FKind
e, TVal
bv)
FunView
NotFun -> (FKind, TVal) -> TypeCheck (FKind, TVal)
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (if Bool
er then FKind
f else FKind -> FKind
castExpr FKind
f FKind -> FKind -> FKind
`App` FKind
e, TVal
VIrr)
Def DefId
f -> (DefId -> FKind
Def DefId
f,) (TVal -> (FKind, TVal))
-> TypeCheck TVal -> TypeCheck (FKind, TVal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do (FKind -> TypeCheck TVal
whnf' (FKind -> TypeCheck TVal)
-> (SigDef -> FKind) -> SigDef -> TypeCheck TVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigDef -> FKind
extrTyp) (SigDef -> TypeCheck TVal)
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
-> TypeCheck TVal
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
forall (m :: * -> *). MonadSig m => QName -> m SigDef
lookupSymbQ (DefId -> QName
idName DefId
f)
Pair{} -> String -> TypeCheck (FKind, TVal)
forall (m :: * -> *) a. MonadError TraceError m => String -> m a
throwErrorMsg (String -> TypeCheck (FKind, TVal))
-> String -> TypeCheck (FKind, TVal)
forall a b. (a -> b) -> a -> b
$ String
"extractInfer: IMPOSSIBLE: pair " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FKind -> String
forall a. Show a => a -> String
show FKind
e
FKind
_ -> (FKind, TVal) -> TypeCheck (FKind, TVal)
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (FKind
Irr, TVal
VIrr)
extractCheck :: Expr -> FTVal -> TypeCheck (FExpr)
FKind
e TVal
tv = do
case FKind
e of
Lam Dec
dec Name
y FKind
e -> do
fv <- TVal -> TypeCheck FunView
funView TVal
tv
case fv of
EraseArg TVal
bv -> FKind -> TVal -> TypeCheck FKind
extractCheck FKind
e TVal
bv
Forall Name
x Domain
dom TVal
fv ->
Dec -> Name -> FKind -> FKind
Lam (Domain -> Dec
forall a. Dom a -> Dec
decor Domain
dom) Name
y (FKind -> FKind) -> TypeCheck FKind -> TypeCheck FKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
Name
-> Domain -> (Int -> TVal -> TypeCheck FKind) -> TypeCheck FKind
forall a.
Name
-> Domain
-> (Int
-> TVal
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a.
MonadCxt m =>
Name -> Domain -> (Int -> TVal -> m a) -> m a
newWithGen Name
y Domain
dom ((Int -> TVal -> TypeCheck FKind) -> TypeCheck FKind)
-> (Int -> TVal -> TypeCheck FKind) -> TypeCheck FKind
forall a b. (a -> b) -> a -> b
$ \ Int
i TVal
xv ->
FKind -> TVal -> TypeCheck FKind
extractCheck FKind
e (TVal -> TypeCheck FKind) -> TypeCheck TVal -> TypeCheck FKind
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TVal -> TVal -> TypeCheck TVal
app TVal
fv (Int -> TVal
VGen Int
i)
Arrow TVal
av TVal
bv ->
if Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased Dec
dec then FKind -> TVal -> TypeCheck FKind
extractCheck FKind
e TVal
bv
else Dec -> Name -> FKind -> FKind
Lam Dec
dec Name
y (FKind -> FKind) -> TypeCheck FKind -> TypeCheck FKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
Name -> Domain -> TypeCheck FKind -> TypeCheck FKind
forall a.
Name
-> Domain
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. MonadCxt m => Name -> Domain -> m a -> m a
new' Name
y (TVal -> Domain
forall a. a -> Dom a
defaultDomain TVal
av) (TypeCheck FKind -> TypeCheck FKind)
-> TypeCheck FKind -> TypeCheck FKind
forall a b. (a -> b) -> a -> b
$
FKind -> TVal -> TypeCheck FKind
extractCheck FKind
e TVal
bv
FunView
NotFun -> FKind -> FKind
castExpr (FKind -> FKind) -> TypeCheck FKind -> TypeCheck FKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
if Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased Dec
dec then FKind -> TVal -> TypeCheck FKind
extractCheck FKind
e TVal
VIrr
else Dec -> Name -> FKind -> FKind
Lam Dec
dec Name
y (FKind -> FKind) -> TypeCheck FKind -> TypeCheck FKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
Name -> Domain -> TypeCheck FKind -> TypeCheck FKind
forall a.
Name
-> Domain
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. MonadCxt m => Name -> Domain -> m a -> m a
new' Name
y (TVal -> Domain
forall a. a -> Dom a
defaultDomain TVal
VIrr) (TypeCheck FKind -> TypeCheck FKind)
-> TypeCheck FKind -> TypeCheck FKind
forall a b. (a -> b) -> a -> b
$
FKind -> TVal -> TypeCheck FKind
extractCheck FKind
e TVal
VIrr
LLet (TBind Name
x Dom (Maybe FKind)
dom0) Telescope
tel FKind
e1 FKind
e2 | Telescope -> Bool
forall a. Null a => a -> Bool
null Telescope
tel -> do
let dom :: Dom FKind
dom = (Maybe FKind -> FKind) -> Dom (Maybe FKind) -> Dom FKind
forall a b. (a -> b) -> Dom a -> Dom b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe FKind -> FKind
forall a. HasCallStack => Maybe a -> a
Maybe.fromJust Dom (Maybe FKind)
dom0
if Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased (Dom FKind -> Dec
forall a. Dom a -> Dec
decor Dom FKind
dom) then FKind -> TVal -> TypeCheck FKind
extractCheck FKind
e2 TVal
tv else do
vdom <- (FKind -> TypeCheck TVal)
-> Dom FKind
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) Domain
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Dom a -> m (Dom b)
Traversable.mapM FKind -> TypeCheck TVal
whnf' Dom FKind
dom
dom <- Traversable.mapM extractType vdom
vdom <- Traversable.mapM whnf' dom
e1 <- extractCheck e1 (typ vdom)
LLet (TBind x (fmap Just dom)) emptyTel e1 <$> do
new' x vdom $ extractCheck e2 tv
Pair FKind
e1 FKind
e2 -> do
view <- TVal -> TypeCheck ProdView
prodView TVal
tv
let (av1,av2) = case view of
Prod TVal
av1 TVal
av2 -> (TVal
av1, TVal
av2)
ProdView
_ -> (TVal
tv,TVal
tv)
Pair <$> extractCheck e1 av1 <*> extractCheck e2 av2
FKind
_ -> TypeCheck FKind
fallback
where
fallback :: TypeCheck FKind
fallback = do
(e,tv') <- FKind -> TypeCheck (FKind, TVal)
extractInfer FKind
e
insertCast e tv tv'
insertCast :: FExpr -> FTVal -> FTVal -> TypeCheck FExpr
insertCast :: FKind -> TVal -> TVal -> TypeCheck FKind
insertCast FKind
e TVal
tv1 TVal
tv2 = TVal -> TVal -> TypeCheck FKind
forall {m :: * -> *}. Monad m => TVal -> TVal -> m FKind
loop TVal
tv1 TVal
tv2 where
loop :: TVal -> TVal -> m FKind
loop TVal
tv1 TVal
tv2 =
case (TVal
tv1,TVal
tv2) of
(TVal
VIrr,TVal
_) -> FKind -> m FKind
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (FKind -> m FKind) -> FKind -> m FKind
forall a b. (a -> b) -> a -> b
$ FKind -> FKind
castExpr FKind
e
(TVal
_,TVal
VIrr) -> FKind -> m FKind
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (FKind -> m FKind) -> FKind -> m FKind
forall a b. (a -> b) -> a -> b
$ FKind -> FKind
castExpr FKind
e
(TVal, TVal)
_ -> FKind -> m FKind
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return FKind
e
funView :: FTVal -> TypeCheck FunView
funView :: TVal -> TypeCheck FunView
funView TVal
tv =
case TVal
tv of
VQuant PiSigma
Pi Name
x Domain
dom TVal
fv | Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased (Domain -> Dec
forall a. Dom a -> Dec
decor Domain
dom) Bool -> Bool -> Bool
&& Domain -> TVal
forall a. Dom a -> a
typ Domain
dom TVal -> TVal -> Bool
forall a. Eq a => a -> a -> Bool
== TVal
VIrr ->
TVal -> FunView
EraseArg (TVal -> FunView) -> TypeCheck TVal -> TypeCheck FunView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TVal -> TVal -> TypeCheck TVal
app TVal
fv TVal
VIrr
VQuant PiSigma
Pi Name
x Domain
dom TVal
fv | Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased (Domain -> Dec
forall a. Dom a -> Dec
decor Domain
dom) ->
FunView -> TypeCheck FunView
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (FunView -> TypeCheck FunView) -> FunView -> TypeCheck FunView
forall a b. (a -> b) -> a -> b
$ Name -> Domain -> TVal -> FunView
Forall Name
x Domain
dom TVal
fv
VQuant PiSigma
Pi Name
x Domain
dom TVal
fv ->
TVal -> TVal -> FunView
Arrow (Domain -> TVal
forall a. Dom a -> a
typ Domain
dom) (TVal -> FunView) -> TypeCheck TVal -> TypeCheck FunView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TVal -> TVal -> TypeCheck TVal
app TVal
fv TVal
VIrr
TVal
_ -> FunView -> TypeCheck FunView
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return FunView
NotFun
data FunView
= Arrow FTVal FTVal
| Forall Name Domain FTVal
| EraseArg FTVal
| NotFun
prodView :: FTVal -> TypeCheck ProdView
prodView :: TVal -> TypeCheck ProdView
prodView TVal
tv =
case TVal
tv of
VQuant PiSigma
Sigma Name
x Domain
dom TVal
fv -> TVal -> TVal -> ProdView
Prod (Domain -> TVal
forall a. Dom a -> a
typ Domain
dom) (TVal -> ProdView) -> TypeCheck TVal -> TypeCheck ProdView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TVal -> TVal -> TypeCheck TVal
app TVal
fv TVal
VIrr
TVal
_ -> ProdView -> TypeCheck ProdView
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProdView -> TypeCheck ProdView) -> ProdView -> TypeCheck ProdView
forall a b. (a -> b) -> a -> b
$ ProdView
NotProd
data ProdView
= Prod FTVal FTVal
| NotProd
type FKind = Expr
star :: FKind
star :: FKind
star = Sort FKind -> FKind
Sort (Sort FKind -> FKind) -> Sort FKind -> FKind
forall a b. (a -> b) -> a -> b
$ FKind -> Sort FKind
forall a. a -> Sort a
Set FKind
Zero
extractSet :: Sort Val -> Maybe FKind
Sort TVal
s =
case Sort TVal
s of
SortC Class
_ -> Maybe FKind
forall a. Maybe a
Nothing
Set TVal
_ -> FKind -> Maybe FKind
forall a. a -> Maybe a
Just (FKind -> Maybe FKind) -> FKind -> Maybe FKind
forall a b. (a -> b) -> a -> b
$ FKind
star
CoSet TVal
_ -> FKind -> Maybe FKind
forall a. a -> Maybe a
Just (FKind -> Maybe FKind) -> FKind -> Maybe FKind
forall a b. (a -> b) -> a -> b
$ FKind
star
extractKindTel :: Telescope -> TypeCheck FTelescope
(Telescope [TBind]
tel) = [TBind] -> Telescope
Telescope ([TBind] -> Telescope)
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [TBind]
-> TypeCheck Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TBind]
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [TBind]
loop [TBind]
tel where
loop :: [TBind]
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [TBind]
loop [] = [TBind]
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [TBind]
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
loop (TBind Name
x Dom FKind
dom : [TBind]
tel) = do
dom <- (FKind -> TypeCheck TVal)
-> Dom FKind
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) Domain
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Dom a -> m (Dom b)
Traversable.mapM FKind -> TypeCheck TVal
whnf' Dom FKind
dom
dom' <- extractKindDom dom
if erased (decor dom') then
newIrr x $
(TBind x dom' :) <$> loop tel
else newTyVar x (typ dom') $ \ Int
i -> do
x <- Int
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Name
forall (m :: * -> *). MonadCxt m => Int -> m Name
nameOfGen Int
i
(TBind x dom' :) <$> loop tel
extractKindDom :: Domain -> TypeCheck (Dom FKind)
Domain
dom =
Dom FKind -> (FKind -> Dom FKind) -> Maybe FKind -> Dom FKind
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (FKind -> Dom FKind
forall a. a -> Dom a
defaultIrrDom FKind
Irr) FKind -> Dom FKind
forall a. a -> Dom a
defaultDomain (Maybe FKind -> Dom FKind)
-> TypeCheck (Maybe FKind)
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) (Dom FKind)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
if Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased (Domain -> Dec
forall a. Dom a -> Dec
decor Domain
dom) then Maybe FKind -> TypeCheck (Maybe FKind)
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe FKind
forall a. Maybe a
Nothing
else TVal -> TypeCheck (Maybe FKind)
extractKind (Domain -> TVal
forall a. Dom a -> a
typ Domain
dom)
extractKind :: TVal -> TypeCheck (Maybe FKind)
TVal
tv =
case TVal
tv of
VSort Sort TVal
s -> Maybe FKind -> TypeCheck (Maybe FKind)
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe FKind -> TypeCheck (Maybe FKind))
-> Maybe FKind -> TypeCheck (Maybe FKind)
forall a b. (a -> b) -> a -> b
$ Sort TVal -> Maybe FKind
extractSet Sort TVal
s
VMeasured Measure TVal
mu TVal
vb -> TVal -> TypeCheck (Maybe FKind)
extractKind TVal
vb
VGuard Bound TVal
beta TVal
vb -> TVal -> TypeCheck (Maybe FKind)
extractKind TVal
vb
VQuant PiSigma
Pi Name
x Domain
dom TVal
fv -> Name
-> Domain -> TypeCheck (Maybe FKind) -> TypeCheck (Maybe FKind)
forall a.
Name
-> Domain
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. MonadCxt m => Name -> Domain -> m a -> m a
new' Name
x Domain
dom (TypeCheck (Maybe FKind) -> TypeCheck (Maybe FKind))
-> TypeCheck (Maybe FKind) -> TypeCheck (Maybe FKind)
forall a b. (a -> b) -> a -> b
$ do
bv <- TVal -> TVal -> TypeCheck TVal
app TVal
fv TVal
VIrr
mk' <- extractKind bv
case mk' of
Maybe FKind
Nothing -> Maybe FKind -> TypeCheck (Maybe FKind)
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe FKind
forall a. Maybe a
Nothing
Just FKind
k' -> do
dom' <- Domain
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) (Dom FKind)
extractKindDom Domain
dom
let x = String -> Name
fresh String
""
return $ Just $ pi (TBind x dom') k'
TVal
_ -> Maybe FKind -> TypeCheck (Maybe FKind)
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe FKind
forall a. Maybe a
Nothing
type FType = Expr
newTyVar :: Name -> FKind -> (Int -> TypeCheck a) -> TypeCheck a
newTyVar :: forall a. Name -> FKind -> (Int -> TypeCheck a) -> TypeCheck a
newTyVar Name
x FKind
k Int -> TypeCheck a
cont = Name -> Domain -> (Int -> TVal -> TypeCheck a) -> TypeCheck a
forall a.
Name
-> Domain
-> (Int
-> TVal
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a.
MonadCxt m =>
Name -> Domain -> (Int -> TVal -> m a) -> m a
newWithGen Name
x (TVal -> Domain
forall a. a -> Dom a
defaultDomain (Env -> FKind -> TVal
VClos Env
forall a. Environ a
emptyEnv FKind
k)) ((Int -> TVal -> TypeCheck a) -> TypeCheck a)
-> (Int -> TVal -> TypeCheck a) -> TypeCheck a
forall a b. (a -> b) -> a -> b
$
\ Int
i TVal
_ -> Int -> TypeCheck a
cont Int
i
addFKindTel :: FTelescope -> TypeCheck a -> TypeCheck a
addFKindTel :: forall a. Telescope -> TypeCheck a -> TypeCheck a
addFKindTel (Telescope [TBind]
tel) = [TBind] -> TypeCheck a -> TypeCheck a
forall {a}. [TBind] -> TypeCheck a -> TypeCheck a
loop [TBind]
tel where
loop :: [TBind] -> TypeCheck a -> TypeCheck a
loop [] TypeCheck a
cont = TypeCheck a
cont
loop (TBind Name
x Dom FKind
dom : [TBind]
tel) TypeCheck a
cont = Name -> FKind -> (Int -> TypeCheck a) -> TypeCheck a
forall a. Name -> FKind -> (Int -> TypeCheck a) -> TypeCheck a
newTyVar Name
x (Dom FKind -> FKind
forall a. Dom a -> a
typ Dom FKind
dom) ((Int -> TypeCheck a) -> TypeCheck a)
-> (Int -> TypeCheck a) -> TypeCheck a
forall a b. (a -> b) -> a -> b
$ \ Int
_ ->
[TBind] -> TypeCheck a -> TypeCheck a
loop [TBind]
tel TypeCheck a
cont
extractTeleVal :: TeleVal -> TypeCheck FTelescope
= [TBind] -> Telescope
Telescope ([TBind] -> Telescope)
-> (TeleVal
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [TBind])
-> TeleVal
-> TypeCheck Telescope
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> TeleVal
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [TBind]
loop where
loop :: TeleVal
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [TBind]
loop [] = [TBind]
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) [TBind]
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
loop (TBinding TVal
tb : TeleVal
vtel) = do
tb <- (TVal -> TypeCheck FKind)
-> TBinding TVal
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) TBind
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TBinding a -> m (TBinding b)
Traversable.mapM TVal -> TypeCheck FKind
extractType TBinding TVal
tb
addBind tb $ do
(tb :) <$> loop vtel
extractType :: TVal -> TypeCheck FType
= FKind -> TVal -> TypeCheck FKind
extractTypeAt FKind
star
extractTypeAt :: FKind -> TVal -> TypeCheck FType
FKind
k TVal
tv = do
case (TVal
tv,FKind
k) of
(VMeasured Measure TVal
mu TVal
vb, FKind
_) -> FKind -> TVal -> TypeCheck FKind
extractTypeAt FKind
k TVal
vb
(VGuard Bound TVal
beta TVal
vb, FKind
_) -> FKind -> TVal -> TypeCheck FKind
extractTypeAt FKind
k TVal
vb
(VQuant PiSigma
pisig Name
x Domain
dom TVal
fv, FKind
_) | Bool -> Bool
not (Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased (Domain -> Dec
forall a. Dom a -> Dec
decor Domain
dom)) -> do
a <- TVal -> TypeCheck FKind
extractType (Domain -> TVal
forall a. Dom a -> a
typ Domain
dom)
bv <- app fv VIrr
b <- extractType bv
let x = String -> Name
fresh String
""
return $ piSig pisig (TBind x (defaultDomain a)) b
(VQuant PiSigma
Pi Name
x Domain
dom TVal
fv, FKind
_) | Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased (Domain -> Dec
forall a. Dom a -> Dec
decor Domain
dom) -> do
mk <- TVal -> TypeCheck (Maybe FKind)
extractKind (Domain -> TVal
forall a. Dom a -> a
typ Domain
dom)
case mk of
Maybe FKind
Nothing -> do
bv <- TVal -> TVal -> TypeCheck TVal
app TVal
fv TVal
VIrr
b <- extractType bv
let x = String -> Name
fresh String
""
return $ pi (TBind x (defaultIrrDom Irr)) b
Just FKind
k' -> do
Name -> FKind -> (Int -> TypeCheck FKind) -> TypeCheck FKind
forall a. Name -> FKind -> (Int -> TypeCheck a) -> TypeCheck a
newTyVar Name
x FKind
k' ((Int -> TypeCheck FKind) -> TypeCheck FKind)
-> (Int -> TypeCheck FKind) -> TypeCheck FKind
forall a b. (a -> b) -> a -> b
$ \ Int
i -> do
bv <- TVal -> TVal -> TypeCheck TVal
app TVal
fv (TVal -> TypeCheck TVal) -> TVal -> TypeCheck TVal
forall a b. (a -> b) -> a -> b
$ Int -> TVal
VGen Int
i
b <- extractType bv
x <- nameOfGen i
return $ pi (TBind x (defaultIrrDom k')) b
(VApp (VDef (DefId IdKind
DatK QName
n)) [TVal]
vs, FKind
_) -> do
k <- SigDef -> FKind
extrTyp (SigDef -> FKind)
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
-> TypeCheck FKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName
-> StateT
TCState (ReaderT TCContext (ExceptT TraceError IO)) SigDef
forall (m :: * -> *). MonadSig m => QName -> m SigDef
lookupSymbQ QName
n
as <- extractTypes k vs
return $ foldl App (Def (DefId DatK n)) as
(VGen Int
i,FKind
_) -> do
Name -> FKind
Var (Name -> FKind)
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Name
-> TypeCheck FKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Name
forall (m :: * -> *). MonadCxt m => Int -> m Name
nameOfGen Int
i
(VApp (VGen Int
i) [TVal]
vs,FKind
_) -> do
VClos _ k <- (Domain -> TVal
forall a. Dom a -> a
typ (Domain -> TVal)
-> (CxtE (OneOrTwo Domain) -> Domain)
-> CxtE (OneOrTwo Domain)
-> TVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OneOrTwo Domain -> Domain
forall a. OneOrTwo a -> a
fromOne (OneOrTwo Domain -> Domain)
-> (CxtE (OneOrTwo Domain) -> OneOrTwo Domain)
-> CxtE (OneOrTwo Domain)
-> Domain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CxtE (OneOrTwo Domain) -> OneOrTwo Domain
forall a. CxtE a -> a
domain) (CxtE (OneOrTwo Domain) -> TVal)
-> StateT
TCState
(ReaderT TCContext (ExceptT TraceError IO))
(CxtE (OneOrTwo Domain))
-> TypeCheck TVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> StateT
TCState
(ReaderT TCContext (ExceptT TraceError IO))
(CxtE (OneOrTwo Domain))
forall (m :: * -> *).
MonadCxt m =>
Int -> m (CxtE (OneOrTwo Domain))
lookupGen Int
i
as <- extractTypes k vs
x <- nameOfGen i
return $ foldl App (Var x) as
(VLam Name
x Env
env FKind
e, Quant PiSigma
Pi (TBind Name
_ Dom FKind
dom) FKind
k) | Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased (Dom FKind -> Dec
forall a. Dom a -> Dec
decor Dom FKind
dom) -> do
tv <- Env -> FKind -> TypeCheck TVal
whnf (Env -> Name -> TVal -> Env
forall a. Environ a -> Name -> a -> Environ a
update Env
env Name
x TVal
VIrr) FKind
e
extractTypeAt k tv
(VLam Name
x Env
env FKind
e, Quant PiSigma
Pi (TBind Name
_ Dom FKind
dom) FKind
k) -> Name -> FKind -> (Int -> TypeCheck FKind) -> TypeCheck FKind
forall a. Name -> FKind -> (Int -> TypeCheck a) -> TypeCheck a
newTyVar Name
x (Dom FKind -> FKind
forall a. Dom a -> a
typ Dom FKind
dom) ((Int -> TypeCheck FKind) -> TypeCheck FKind)
-> (Int -> TypeCheck FKind) -> TypeCheck FKind
forall a b. (a -> b) -> a -> b
$ \ Int
i -> do
tv <- Env -> FKind -> TypeCheck TVal
whnf (Env -> Name -> TVal -> Env
forall a. Environ a -> Name -> a -> Environ a
update Env
env Name
x (Int -> TVal
VGen Int
i)) FKind
e
x <- nameOfGen i
Lam defaultDec x <$> extractTypeAt k tv
(VLam{},FKind
_) -> String -> TypeCheck FKind
forall a. HasCallStack => String -> a
error (String -> TypeCheck FKind) -> String -> TypeCheck FKind
forall a b. (a -> b) -> a -> b
$ String
"panic! extractTypeAt " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (TVal, FKind) -> String
forall a. Show a => a -> String
show (TVal
tv,FKind
k)
(VSing TVal
_ TVal
tv,FKind
_) -> FKind -> TVal -> TypeCheck FKind
extractTypeAt FKind
k TVal
tv
(VUp TVal
v TVal
_,FKind
_) -> FKind -> TVal -> TypeCheck FKind
extractTypeAt FKind
k TVal
v
(TVal, FKind)
_ -> FKind -> TypeCheck FKind
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return FKind
Irr
extractTypes :: FKind -> [TVal] -> TypeCheck [FType]
FKind
k [TVal]
vs =
case (FKind
k,[TVal]
vs) of
(FKind
_, []) -> [FKind] -> TypeCheck [FKind]
forall a.
a -> StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
(Quant PiSigma
Pi (TBind Name
_ Dom FKind
dom) FKind
k, TVal
v:[TVal]
vs) | Dec -> Bool
forall pol. Polarity pol => pol -> Bool
erased (Dom FKind -> Dec
forall a. Dom a -> Dec
decor Dom FKind
dom) -> FKind -> [TVal] -> TypeCheck [FKind]
extractTypes FKind
k [TVal]
vs
(Quant PiSigma
Pi (TBind Name
_ Dom FKind
dom) FKind
k, TVal
v:[TVal]
vs) -> do
v <- TVal -> TypeCheck TVal
whnfClos TVal
v
a <- extractTypeAt (typ dom) v
as <- extractTypes k vs
return $ a : as
(FKind, [TVal])
_ -> String -> TypeCheck [FKind]
forall a. HasCallStack => String -> a
error (String -> TypeCheck [FKind]) -> String -> TypeCheck [FKind]
forall a b. (a -> b) -> a -> b
$ String
"panic! extractTypes " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FKind -> String
forall a. Show a => a -> String
show FKind
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [TVal] -> String
forall a. Show a => a -> String
show [TVal]
vs