module AutoApply
( autoapply
, autoapplyDecs
) where
import Control.Applicative
import Control.Arrow ( (>>>) )
import Control.Monad
import Control.Monad.Logic ( LogicT
, observeManyT
)
import Control.Monad.Trans as T
import Control.Monad.Trans.Except
import Control.Unification
import Control.Unification.IntVar
import Control.Unification.Types
import Data.Foldable
import Data.Functor
import Data.Functor.Fixedpoint
import Data.Maybe
import Data.Traversable
import Language.Haskell.TH
import Language.Haskell.TH.Desugar
import Prelude hiding ( pred )
autoapply
:: [Name]
-> [Name]
-> Name
-> Q Exp
autoapply :: [Name] -> [Name] -> Name -> Q Exp
autoapply [Name]
subsuming [Name]
unifying Name
fun = do
[Given]
unifyingInfos <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Name]
unifying forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (UnificationType -> Name -> DType -> Given
Given UnificationType
Unifying)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name -> Q (Name, DType)
reifyVal
String
"Argument"
[Given]
subsumingInfos <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Name]
subsuming forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (UnificationType -> Name -> DType -> Given
Given UnificationType
Subsuming)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name -> Q (Name, DType)
reifyVal
String
"Argument"
Function
funInfo <- forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> DType -> Function
Function forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Name -> Q (Name, DType)
reifyVal String
"Function" Name
fun
[Given] -> Function -> Q Exp
autoapply1 ([Given]
unifyingInfos forall a. Semigroup a => a -> a -> a
<> [Given]
subsumingInfos) Function
funInfo
autoapplyDecs
:: (String -> String)
-> [Name]
-> [Name]
-> [Name]
-> Q [Dec]
autoapplyDecs :: (String -> String) -> [Name] -> [Name] -> [Name] -> Q [Dec]
autoapplyDecs String -> String
getNewName [Name]
subsuming [Name]
unifying [Name]
funs = do
[Given]
unifyingInfos <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Name]
unifying forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (UnificationType -> Name -> DType -> Given
Given UnificationType
Unifying)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name -> Q (Name, DType)
reifyVal
String
"Argument"
[Given]
subsumingInfos <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Name]
subsuming forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (UnificationType -> Name -> DType -> Given
Given UnificationType
Subsuming)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name -> Q (Name, DType)
reifyVal
String
"Argument"
[Function]
funInfos <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Name]
funs forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> DType -> Function
Function) forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name -> Q (Name, DType)
reifyVal String
"Function"
let mkFun :: Function -> Q Dec
mkFun Function
fun = do
Exp
exp' <- [Given] -> Function -> Q Exp
autoapply1 ([Given]
unifyingInfos forall a. Semigroup a => a -> a -> a
<> [Given]
subsumingInfos) Function
fun
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Name -> [Clause] -> Dec
FunD (String -> Name
mkName forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
getNewName forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
nameBase forall b c a. (b -> c) -> (a -> b) -> a -> c
. Function -> Name
fName forall a b. (a -> b) -> a -> b
$ Function
fun)
[[Pat] -> Body -> [Dec] -> Clause
Clause [] (Exp -> Body
NormalB Exp
exp') []]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Function -> Q Dec
mkFun [Function]
funInfos
data Given = Given
{ Given -> UnificationType
gUnificationType :: UnificationType
, Given -> Name
gName :: Name
, Given -> DType
gType :: DType
}
deriving Int -> Given -> String -> String
[Given] -> String -> String
Given -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Given] -> String -> String
$cshowList :: [Given] -> String -> String
show :: Given -> String
$cshow :: Given -> String
showsPrec :: Int -> Given -> String -> String
$cshowsPrec :: Int -> Given -> String -> String
Show
data UnificationType = Unifying | Subsuming
deriving Int -> UnificationType -> String -> String
[UnificationType] -> String -> String
UnificationType -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [UnificationType] -> String -> String
$cshowList :: [UnificationType] -> String -> String
show :: UnificationType -> String
$cshow :: UnificationType -> String
showsPrec :: Int -> UnificationType -> String -> String
$cshowsPrec :: Int -> UnificationType -> String -> String
Show
data Function = Function
{ Function -> Name
fName :: Name
, Function -> DType
fType :: DType
}
deriving (Int -> Function -> String -> String
[Function] -> String -> String
Function -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Function] -> String -> String
$cshowList :: [Function] -> String -> String
show :: Function -> String
$cshow :: Function -> String
showsPrec :: Int -> Function -> String -> String
$cshowsPrec :: Int -> Function -> String -> String
Show)
autoapply1 :: [Given] -> Function -> Q Exp
autoapply1 :: [Given] -> Function -> Q Exp
autoapply1 [Given]
givens Function
fun = do
let
(forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DTyVarBndrUnit -> Name
varBndrName -> [Name]
cmdVarNames, [DType]
preds, [DType]
args, DType
ret) = DType -> ([DTyVarBndrUnit], [DType], [DType], DType)
unravel (Function -> DType
fType Function
fun)
defaultMaybe :: f a -> f (Maybe a)
defaultMaybe f a
m = (forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
m) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
liftQ :: Q a -> IntBindingT TypeF (LogicT Q) a
liftQ :: forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
T.lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
T.lift
errorToLogic :: ExceptT (UFailure TypeF IntVar) m b -> m b
errorToLogic ExceptT (UFailure TypeF IntVar) m b
go = forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT (UFailure TypeF IntVar) m b
go forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Left (UFailure TypeF IntVar
_ :: UFailure TypeF IntVar) -> forall (f :: * -> *) a. Alternative f => f a
empty
Right b
x -> forall (f :: * -> *) a. Applicative f => a -> f a
pure b
x
quant :: UTerm TypeF IntVar -> IntBindingT TypeF (LogicT Q) ()
quant UTerm TypeF IntVar
t = do
[IntVar]
vs <- forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
UTerm t v -> m [v]
getFreeVars UTerm TypeF IntVar
t
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [IntVar]
vs forall a b. (a -> b) -> a -> b
$ \IntVar
v -> forall (t :: * -> *) v (m :: * -> *).
BindingMonad t v m =>
v -> UTerm t v -> m ()
bindVar IntVar
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Name -> TypeF a
VarF) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (forall (m :: * -> *). Quote m => String -> m Name
newName String
"a")
genProvs :: LogicT Q [ArgProvenance]
genProvs :: LogicT Q [ArgProvenance]
genProvs = forall (m :: * -> *) (t :: * -> *) a.
Monad m =>
IntBindingT t m a -> m a
evalIntBindingT forall a b. (a -> b) -> a -> b
$ do
[(Name, IntVar)]
cmdVars <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ (Name
n, ) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) v (m :: * -> *). BindingMonad t v m => m v
freeVar | Name
n <- [Name]
cmdVarNames ]
[UTerm TypeF IntVar]
instArgs <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse
(forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, IntVar)] -> Fix TypeF -> UTerm TypeF IntVar
instWithVars [(Name, IntVar)]
cmdVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadFail m => DType -> m ([Name], Fix TypeF)
typeDtoF)
[DType]
args
UTerm TypeF IntVar
cmdM <- forall (t :: * -> *) v. v -> UTerm t v
UVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) v (m :: * -> *). BindingMonad t v m => m v
freeVar
UTerm TypeF IntVar
retInst <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, IntVar)] -> Fix TypeF -> UTerm TypeF IntVar
instWithVars [(Name, IntVar)]
cmdVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadFail m => DType -> m ([Name], Fix TypeF)
typeDtoF forall a b. (a -> b) -> a -> b
$ DType
ret
[(UTerm TypeF IntVar,
ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
ArgProvenance)]
instGivens <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Given]
givens forall a b. (a -> b) -> a -> b
$ \g :: Given
g@Given {Name
DType
UnificationType
gType :: DType
gName :: Name
gUnificationType :: UnificationType
gType :: Given -> DType
gName :: Given -> Name
gUnificationType :: Given -> UnificationType
..} -> do
(UTerm TypeF IntVar,
ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
ArgProvenance)
nonApp <- do
UTerm TypeF IntVar
instTy <- forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall (m :: * -> *).
BindingMonad TypeF IntVar m =>
[Name] -> Fix TypeF -> m (UTerm TypeF IntVar)
inst forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadFail m => DType -> m ([Name], Fix TypeF)
typeDtoF forall a b. (a -> b) -> a -> b
$ DType
gType
Name
v <- forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Quote m => String -> m Name
newName String
"g"
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UTerm TypeF IntVar
instTy, forall (f :: * -> *) a. Applicative f => a -> f a
pure (), Name -> Given -> ArgProvenance
BoundPure Name
v Given
g)
Maybe
(UTerm TypeF IntVar,
ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
ArgProvenance)
app <- case DType -> ([Name], DType)
stripForall DType
gType of
([Name]
vars, DAppT DType
m DType
a) ->
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (Name -> [Type] -> Q Bool
isInstance ''Applicative [forall th ds. Desugar th ds => ds -> th
sweeten DType
m]) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Bool
False -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
Bool
True -> do
UTerm TypeF IntVar
m' <- forall (m :: * -> *).
BindingMonad TypeF IntVar m =>
[Name] -> Fix TypeF -> m (UTerm TypeF IntVar)
inst [Name]
vars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadFail m => DType -> m ([Name], Fix TypeF)
typeDtoF forall a b. (a -> b) -> a -> b
$ DType
m
UTerm TypeF IntVar
a' <- forall (m :: * -> *).
BindingMonad TypeF IntVar m =>
[Name] -> Fix TypeF -> m (UTerm TypeF IntVar)
inst [Name]
vars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadFail m => DType -> m ([Name], Fix TypeF)
typeDtoF forall a b. (a -> b) -> a -> b
$ DType
a
Name
v <- forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Quote m => String -> m Name
newName String
"g"
let predicate :: ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) ()
predicate = do
UTerm TypeF IntVar
_ <- forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m),
MonadError e (em m)) =>
UTerm t v -> UTerm t v -> em m (UTerm t v)
unify UTerm TypeF IntVar
m' UTerm TypeF IntVar
cmdM
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (UTerm TypeF IntVar
a', ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) ()
predicate, Name -> Given -> ArgProvenance
Bound Name
v Given
g)
([Name], DType)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(UTerm TypeF IntVar,
ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
ArgProvenance)
nonApp] forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Maybe
(UTerm TypeF IntVar,
ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
ArgProvenance)
app)
[Maybe ArgProvenance]
as <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [UTerm TypeF IntVar]
instArgs forall a b. (a -> b) -> a -> b
$ \UTerm TypeF IntVar
argTy ->
forall {f :: * -> *} {a}. Alternative f => f a -> f (Maybe a)
defaultMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum forall a b. (a -> b) -> a -> b
$ [(UTerm TypeF IntVar,
ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) (),
ArgProvenance)]
instGivens forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(UTerm TypeF IntVar
givenTy, ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) ()
predicate, ArgProvenance
g) -> do
forall {m :: * -> *} {b}.
(Monad m, Alternative m) =>
ExceptT (UFailure TypeF IntVar) m b -> m b
errorToLogic forall a b. (a -> b) -> a -> b
$ do
ExceptT (UFailure TypeF IntVar) (IntBindingT TypeF (LogicT Q)) ()
predicate
UTerm TypeF IntVar
freshGivenTy <- forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m),
MonadError e (em m)) =>
UTerm t v -> em m (UTerm t v)
freshen UTerm TypeF IntVar
givenTy
let u :: UnificationType
u = case ArgProvenance
g of
Bound Name
_ Given {Name
DType
UnificationType
gType :: DType
gName :: Name
gUnificationType :: UnificationType
gType :: Given -> DType
gName :: Given -> Name
gUnificationType :: Given -> UnificationType
..} -> UnificationType
gUnificationType
BoundPure Name
_ Given {Name
DType
UnificationType
gType :: DType
gName :: Name
gUnificationType :: UnificationType
gType :: Given -> DType
gName :: Given -> Name
gUnificationType :: Given -> UnificationType
..} -> UnificationType
gUnificationType
Argument Name
_ DType
_ -> UnificationType
Unifying
case UnificationType
u of
UnificationType
Unifying -> forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m),
MonadError e (em m)) =>
UTerm t v -> UTerm t v -> em m (UTerm t v)
unify UTerm TypeF IntVar
freshGivenTy UTerm TypeF IntVar
argTy
UnificationType
Subsuming -> do
Bool
s <- forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m),
MonadError e (em m)) =>
UTerm t v -> UTerm t v -> em m Bool
subsumes UTerm TypeF IntVar
freshGivenTy UTerm TypeF IntVar
argTy
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
s
forall (f :: * -> *) a. Applicative f => a -> f a
pure ArgProvenance
g
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ArgProvenance -> Bool
isMonadicBind (forall a. [Maybe a] -> [a]
catMaybes [Maybe ArgProvenance]
as)) forall a b. (a -> b) -> a -> b
$ do
UTerm TypeF IntVar
a <- forall (t :: * -> *) v. v -> UTerm t v
UVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) v (m :: * -> *). BindingMonad t v m => m v
freeVar
UTerm TypeF IntVar
ret' <- forall {m :: * -> *} {b}.
(Monad m, Alternative m) =>
ExceptT (UFailure TypeF IntVar) m b -> m b
errorToLogic forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m),
MonadError e (em m)) =>
UTerm t v -> UTerm t v -> em m (UTerm t v)
unify UTerm TypeF IntVar
retInst (forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (forall a. a -> a -> TypeF a
AppF UTerm TypeF IntVar
cmdM UTerm TypeF IntVar
a))
UTerm TypeF IntVar -> IntBindingT TypeF (LogicT Q) ()
quant UTerm TypeF IntVar
ret'
Maybe (Fix TypeF)
retFrozen <- forall (t :: * -> *) v. Traversable t => UTerm t v -> Maybe (Fix t)
freeze forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {m :: * -> *} {b}.
(Monad m, Alternative m) =>
ExceptT (UFailure TypeF IntVar) m b -> m b
errorToLogic (forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m),
MonadError e (em m)) =>
UTerm t v -> em m (UTerm t v)
applyBindings UTerm TypeF IntVar
ret')
case Maybe (Fix TypeF)
retFrozen of
Just (Fix (AppF Fix TypeF
m Fix TypeF
_)) -> do
let typeD :: DType
typeD = Fix TypeF -> DType
typeFtoD Fix TypeF
m
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (Name -> [Type] -> Q Bool
isInstance ''Applicative [forall th ds. Desugar th ds => ds -> th
sweeten DType
typeD]) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Bool
False -> forall (f :: * -> *) a. Alternative f => f a
empty
Bool
True -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Maybe (Fix TypeF)
Nothing ->
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ
forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadFail m => String -> m a
fail
String
"\"impossible\", return type didn't freeze while checking monadic bindings"
Maybe (Fix TypeF)
_ -> forall (f :: * -> *) a. Alternative f => f a
empty
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [DType]
preds forall a b. (a -> b) -> a -> b
$ \DType
pred -> do
UTerm TypeF IntVar
instPred <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, IntVar)] -> Fix TypeF -> UTerm TypeF IntVar
instWithVars [(Name, IntVar)]
cmdVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). MonadFail m => DType -> m ([Name], Fix TypeF)
typeDtoF forall a b. (a -> b) -> a -> b
$ DType
pred
UTerm TypeF IntVar -> IntBindingT TypeF (LogicT Q) ()
quant UTerm TypeF IntVar
instPred
Maybe (Fix TypeF)
instFrozen <- forall (t :: * -> *) v. Traversable t => UTerm t v -> Maybe (Fix t)
freeze forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {m :: * -> *} {b}.
(Monad m, Alternative m) =>
ExceptT (UFailure TypeF IntVar) m b -> m b
errorToLogic (forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m),
MonadError e (em m)) =>
UTerm t v -> em m (UTerm t v)
applyBindings UTerm TypeF IntVar
instPred)
case Maybe (Fix TypeF)
instFrozen of
Just Fix TypeF
f -> do
let (DType
class', [DTypeArg]
predArgs) = DType -> (DType, [DTypeArg])
unfoldDType (Fix TypeF -> DType
typeFtoD Fix TypeF
f)
typeArgs :: [DType]
typeArgs = [ DType
a | DTANormal DType
a <- [DTypeArg]
predArgs ]
Name
className <- case DType
class' of
DConT Name
n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
n
DType
_ -> forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"unfolded predicate didn't begin with a ConT"
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (forall (q :: * -> *). (Quasi q, MonadFail q) => Name -> q Info
reifyWithWarning Name
className) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ClassI Dec
_ [Dec]
_ ->
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (Name -> [Type] -> Q Bool
isInstance Name
className (forall th ds. Desugar th ds => ds -> th
sweeten forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DType]
typeArgs)) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Bool
False -> forall (f :: * -> *) a. Alternative f => f a
empty
Bool
True -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
FamilyI Dec
_ [Dec]
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Info
_ -> forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Predicate name isn't a class or a type family"
Maybe (Fix TypeF)
Nothing ->
forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ
forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadFail m => String -> m a
fail
String
"\"impossible\": predicate didn't freeze while checking predicates"
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for (forall a b. [a] -> [b] -> [(a, b)]
zip [DType]
args [Maybe ArgProvenance]
as) forall a b. (a -> b) -> a -> b
$ \case
(DType
_, Just ArgProvenance
p ) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ArgProvenance
p
(DType
t, Maybe ArgProvenance
Nothing) -> (Name -> DType -> ArgProvenance
`Argument` DType
t) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Q a -> IntBindingT TypeF (LogicT Q) a
liftQ (forall (m :: * -> *). Quote m => String -> m Name
newName String
"a")
[ArgProvenance]
argProvenances <-
forall (m :: * -> *) a. MonadFail m => String -> Maybe a -> m a
note
String
"\"Impossible\" Finding argument provenances failed (unless the function context containts a class with no instances)"
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> Maybe a
listToMaybe
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. Monad m => Int -> LogicT m a -> m [a]
observeManyT Int
1 LogicT Q [ArgProvenance]
genProvs
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Int
length [ArgProvenance]
argProvenances forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [DType]
args) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadFail m => String -> m a
fail
String
"\"Impossible\", incorrect number of argument provenances were found"
let bindGiven :: ArgProvenance -> Maybe Stmt
bindGiven = \case
BoundPure Name
_ Given
_ -> forall a. Maybe a
Nothing
Bound Name
n Given
g -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Pat -> Exp -> Stmt
BindS (Name -> Pat
VarP Name
n) (Name -> Exp
VarE (Given -> Name
gName Given
g))
Argument Name
_ DType
_ -> forall a. Maybe a
Nothing
bs :: [Stmt]
bs = forall a. [Maybe a] -> [a]
catMaybes (ArgProvenance -> Maybe Stmt
bindGiven forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ArgProvenance]
argProvenances)
ret' :: DExp
ret' = DExp -> [DExp] -> DExp
applyDExp
(Name -> DExp
DVarE (Function -> Name
fName Function
fun))
([ArgProvenance]
argProvenances forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
Bound Name
n Given
_ -> Name -> DExp
DVarE Name
n
BoundPure Name
_ (Given UnificationType
_ Name
n DType
_) -> Name -> DExp
DVarE Name
n
Argument Name
n DType
_ -> Name -> DExp
DVarE Name
n
)
DExp
exp' <- forall (q :: * -> *).
DsMonad q =>
Maybe ModName -> [Stmt] -> q DExp
dsDoStmts forall a. Maybe a
Nothing ([Stmt]
bs forall a. Semigroup a => a -> a -> a
<> [Exp -> Stmt
NoBindS (forall th ds. Desugar th ds => ds -> th
sweeten DExp
ret')])
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ [Pat] -> Exp -> Exp
LamE [ Pat -> Type -> Pat
SigP (Name -> Pat
VarP Name
n) (forall th ds. Desugar th ds => ds -> th
sweeten DType
t) | Argument Name
n DType
t <- [ArgProvenance]
argProvenances ]
(forall th ds. Desugar th ds => ds -> th
sweeten DExp
exp')
data ArgProvenance
= Bound Name Given
| BoundPure Name Given
| Argument Name DType
deriving (Int -> ArgProvenance -> String -> String
[ArgProvenance] -> String -> String
ArgProvenance -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [ArgProvenance] -> String -> String
$cshowList :: [ArgProvenance] -> String -> String
show :: ArgProvenance -> String
$cshow :: ArgProvenance -> String
showsPrec :: Int -> ArgProvenance -> String -> String
$cshowsPrec :: Int -> ArgProvenance -> String -> String
Show)
isMonadicBind :: ArgProvenance -> Bool
isMonadicBind :: ArgProvenance -> Bool
isMonadicBind = \case
Bound Name
_ Given
_ -> Bool
True
ArgProvenance
_ -> Bool
False
data TypeF a
= AppF a a
| VarF Name
| ConF Name
| ArrowF
| LitF TyLit
deriving (Int -> TypeF a -> String -> String
forall a. Show a => Int -> TypeF a -> String -> String
forall a. Show a => [TypeF a] -> String -> String
forall a. Show a => TypeF a -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [TypeF a] -> String -> String
$cshowList :: forall a. Show a => [TypeF a] -> String -> String
show :: TypeF a -> String
$cshow :: forall a. Show a => TypeF a -> String
showsPrec :: Int -> TypeF a -> String -> String
$cshowsPrec :: forall a. Show a => Int -> TypeF a -> String -> String
Show, forall a b. a -> TypeF b -> TypeF a
forall a b. (a -> b) -> TypeF a -> TypeF b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> TypeF b -> TypeF a
$c<$ :: forall a b. a -> TypeF b -> TypeF a
fmap :: forall a b. (a -> b) -> TypeF a -> TypeF b
$cfmap :: forall a b. (a -> b) -> TypeF a -> TypeF b
Functor, forall a. Eq a => a -> TypeF a -> Bool
forall a. Num a => TypeF a -> a
forall a. Ord a => TypeF a -> a
forall m. Monoid m => TypeF m -> m
forall a. TypeF a -> Bool
forall a. TypeF a -> Int
forall a. TypeF a -> [a]
forall a. (a -> a -> a) -> TypeF a -> a
forall m a. Monoid m => (a -> m) -> TypeF a -> m
forall b a. (b -> a -> b) -> b -> TypeF a -> b
forall a b. (a -> b -> b) -> b -> TypeF a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => TypeF a -> a
$cproduct :: forall a. Num a => TypeF a -> a
sum :: forall a. Num a => TypeF a -> a
$csum :: forall a. Num a => TypeF a -> a
minimum :: forall a. Ord a => TypeF a -> a
$cminimum :: forall a. Ord a => TypeF a -> a
maximum :: forall a. Ord a => TypeF a -> a
$cmaximum :: forall a. Ord a => TypeF a -> a
elem :: forall a. Eq a => a -> TypeF a -> Bool
$celem :: forall a. Eq a => a -> TypeF a -> Bool
length :: forall a. TypeF a -> Int
$clength :: forall a. TypeF a -> Int
null :: forall a. TypeF a -> Bool
$cnull :: forall a. TypeF a -> Bool
toList :: forall a. TypeF a -> [a]
$ctoList :: forall a. TypeF a -> [a]
foldl1 :: forall a. (a -> a -> a) -> TypeF a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> TypeF a -> a
foldr1 :: forall a. (a -> a -> a) -> TypeF a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> TypeF a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> TypeF a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> TypeF a -> b
foldl :: forall b a. (b -> a -> b) -> b -> TypeF a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> TypeF a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> TypeF a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> TypeF a -> b
foldr :: forall a b. (a -> b -> b) -> b -> TypeF a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> TypeF a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> TypeF a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> TypeF a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> TypeF a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> TypeF a -> m
fold :: forall m. Monoid m => TypeF m -> m
$cfold :: forall m. Monoid m => TypeF m -> m
Foldable, Functor TypeF
Foldable TypeF
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => TypeF (m a) -> m (TypeF a)
forall (f :: * -> *) a. Applicative f => TypeF (f a) -> f (TypeF a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeF a -> m (TypeF b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeF a -> f (TypeF b)
sequence :: forall (m :: * -> *) a. Monad m => TypeF (m a) -> m (TypeF a)
$csequence :: forall (m :: * -> *) a. Monad m => TypeF (m a) -> m (TypeF a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeF a -> m (TypeF b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeF a -> m (TypeF b)
sequenceA :: forall (f :: * -> *) a. Applicative f => TypeF (f a) -> f (TypeF a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => TypeF (f a) -> f (TypeF a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeF a -> f (TypeF b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeF a -> f (TypeF b)
Traversable)
instance Unifiable TypeF where
zipMatch :: forall a. TypeF a -> TypeF a -> Maybe (TypeF (Either a (a, a)))
zipMatch (AppF a
l1 a
r1) (AppF a
l2 a
r2) =
forall a. a -> Maybe a
Just (forall a. a -> a -> TypeF a
AppF (forall a b. b -> Either a b
Right (a
l1, a
l2)) (forall a b. b -> Either a b
Right (a
r1, a
r2)))
zipMatch (VarF Name
n1) (VarF Name
n2) | Name
n1 forall a. Eq a => a -> a -> Bool
== Name
n2 = forall a. a -> Maybe a
Just (forall a. Name -> TypeF a
VarF Name
n1)
zipMatch (ConF Name
n1) (ConF Name
n2) | Name
n1 forall a. Eq a => a -> a -> Bool
== Name
n2 = forall a. a -> Maybe a
Just (forall a. Name -> TypeF a
ConF Name
n1)
zipMatch TypeF a
ArrowF TypeF a
ArrowF = forall a. a -> Maybe a
Just forall a. TypeF a
ArrowF
zipMatch (LitF TyLit
l1) (LitF TyLit
l2) | TyLit
l1 forall a. Eq a => a -> a -> Bool
== TyLit
l2 = forall a. a -> Maybe a
Just (forall a. TyLit -> TypeF a
LitF TyLit
l1)
zipMatch TypeF a
_ TypeF a
_ = forall a. Maybe a
Nothing
typeDtoF :: MonadFail m => DType -> m ([Name], Fix TypeF)
typeDtoF :: forall (m :: * -> *). MonadFail m => DType -> m ([Name], Fix TypeF)
typeDtoF = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse DType -> m (Fix TypeF)
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. DType -> ([Name], DType)
stripForall
where
go :: DType -> m (Fix TypeF)
go = \case
DForallT{} -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"TODO: Higher ranked types"
DConstrainedT{} -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"TODO: Higher ranked types"
DAppT DType
l DType
r -> do
Fix TypeF
l' <- DType -> m (Fix TypeF)
go DType
l
Fix TypeF
r' <- DType -> m (Fix TypeF)
go DType
r
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *). f (Fix f) -> Fix f
Fix (forall a. a -> a -> TypeF a
AppF Fix TypeF
l' Fix TypeF
r')
DAppKindT DType
t DType
_ -> DType -> m (Fix TypeF)
go DType
t
DSigT DType
t DType
_ -> DType -> m (Fix TypeF)
go DType
t
DVarT Name
n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *). f (Fix f) -> Fix f
Fix forall a b. (a -> b) -> a -> b
$ forall a. Name -> TypeF a
VarF Name
n
DConT Name
n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *). f (Fix f) -> Fix f
Fix forall a b. (a -> b) -> a -> b
$ forall a. Name -> TypeF a
ConF Name
n
DType
DArrowT -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *). f (Fix f) -> Fix f
Fix forall a b. (a -> b) -> a -> b
$ forall a. TypeF a
ArrowF
DLitT TyLit
l -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *). f (Fix f) -> Fix f
Fix forall a b. (a -> b) -> a -> b
$ forall a. TyLit -> TypeF a
LitF TyLit
l
DType
DWildCardT -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"TODO: Wildcards"
typeFtoD :: Fix TypeF -> DType
typeFtoD :: Fix TypeF -> DType
typeFtoD = forall (f :: * -> *). Fix f -> f (Fix f)
unFix forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> \case
AppF Fix TypeF
l Fix TypeF
r -> DType -> DType -> DType
DAppT (Fix TypeF -> DType
typeFtoD Fix TypeF
l) (Fix TypeF -> DType
typeFtoD Fix TypeF
r)
VarF Name
n -> Name -> DType
DVarT Name
n
ConF Name
n -> Name -> DType
DConT Name
n
TypeF (Fix TypeF)
ArrowF -> DType
DArrowT
LitF TyLit
l -> TyLit -> DType
DLitT TyLit
l
varBndrName :: DTyVarBndrUnit -> Name
varBndrName :: DTyVarBndrUnit -> Name
varBndrName = \case
DPlainTV Name
n () -> Name
n
DKindedTV Name
n () DType
_ -> Name
n
raiseForalls :: DType -> DType
raiseForalls :: DType -> DType
raiseForalls = DType -> ([DTyVarBndrUnit], [DType], DType)
go forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> \case
([DTyVarBndrUnit]
vs, [DType]
ctx, DType
t) -> DForallTelescope -> DType -> DType
DForallT ([DTyVarBndrUnit] -> DForallTelescope
DForallVis [DTyVarBndrUnit]
vs) forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DType] -> DType -> DType
DConstrainedT [DType]
ctx forall a b. (a -> b) -> a -> b
$ DType
t
where
go :: DType -> ([DTyVarBndrUnit], [DType], DType)
go = \case
DForallT DForallTelescope
vs DType
t -> let ([DTyVarBndrUnit]
vs', [DType]
ctx', DType
t') = DType -> ([DTyVarBndrUnit], [DType], DType)
go DType
t in (DForallTelescope -> [DTyVarBndrUnit]
telescopeBndrs DForallTelescope
vs forall a. Semigroup a => a -> a -> a
<> [DTyVarBndrUnit]
vs', [DType]
ctx', DType
t')
DConstrainedT [DType]
ctx DType
t ->
let ([DTyVarBndrUnit]
vs', [DType]
ctx', DType
t') = DType -> ([DTyVarBndrUnit], [DType], DType)
go DType
t in ([DTyVarBndrUnit]
vs', [DType]
ctx forall a. Semigroup a => a -> a -> a
<> [DType]
ctx', DType
t')
DType
l :~> DType
r -> let ([DTyVarBndrUnit]
vs, [DType]
ctx, DType
r') = DType -> ([DTyVarBndrUnit], [DType], DType)
go DType
r in ([DTyVarBndrUnit]
vs, [DType]
ctx, DType
l DType -> DType -> DType
:~> DType
r')
DType
t -> ([], [], DType
t)
pattern (:~>) :: DType -> DType -> DType
pattern l $b:~> :: DType -> DType -> DType
$m:~> :: forall {r}. DType -> (DType -> DType -> r) -> ((# #) -> r) -> r
:~> r = DArrowT `DAppT` l `DAppT` r
inst
:: BindingMonad TypeF IntVar m
=> [Name]
-> Fix TypeF
-> m (UTerm TypeF IntVar)
inst :: forall (m :: * -> *).
BindingMonad TypeF IntVar m =>
[Name] -> Fix TypeF -> m (UTerm TypeF IntVar)
inst [Name]
ns Fix TypeF
t = do
[(Name, IntVar)]
vs <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ (Name
n, ) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) v (m :: * -> *). BindingMonad t v m => m v
freeVar | Name
n <- [Name]
ns ]
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ [(Name, IntVar)] -> Fix TypeF -> UTerm TypeF IntVar
instWithVars [(Name, IntVar)]
vs Fix TypeF
t
instWithVars :: [(Name, IntVar)] -> Fix TypeF -> UTerm TypeF IntVar
instWithVars :: [(Name, IntVar)] -> Fix TypeF -> UTerm TypeF IntVar
instWithVars [(Name, IntVar)]
vs Fix TypeF
t =
let go :: Fix TypeF -> UTerm TypeF IntVar
go (Fix TypeF (Fix TypeF)
f) = case TypeF (Fix TypeF)
f of
AppF Fix TypeF
l Fix TypeF
r -> forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (forall a. a -> a -> TypeF a
AppF (Fix TypeF -> UTerm TypeF IntVar
go Fix TypeF
l) (Fix TypeF -> UTerm TypeF IntVar
go Fix TypeF
r))
VarF Name
n | Just IntVar
v <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, IntVar)]
vs -> forall (t :: * -> *) v. v -> UTerm t v
UVar IntVar
v
VarF Name
n -> forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (forall a. Name -> TypeF a
VarF Name
n)
ConF Name
n -> forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (forall a. Name -> TypeF a
ConF Name
n)
TypeF (Fix TypeF)
ArrowF -> forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm forall a. TypeF a
ArrowF
LitF TyLit
l -> forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (forall a. TyLit -> TypeF a
LitF TyLit
l)
in Fix TypeF -> UTerm TypeF IntVar
go Fix TypeF
t
reifyVal :: String -> Name -> Q (Name, DType)
reifyVal :: String -> Name -> Q (Name, DType)
reifyVal String
d Name
n = forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReify Name
n forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just (DVarI Name
name DType
ty Maybe Name
_) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name
name, DType
ty)
Maybe DInfo
_ -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
d forall a. Semigroup a => a -> a -> a
<> String
" " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Name
n forall a. Semigroup a => a -> a -> a
<> String
" isn't a value"
stripForall :: DType -> ([Name], DType)
stripForall :: DType -> ([Name], DType)
stripForall = DType -> DType
raiseForalls forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> \case
DForallT DForallTelescope
vs (DConstrainedT [DType]
_ DType
ty) -> (DTyVarBndrUnit -> Name
varBndrName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DForallTelescope -> [DTyVarBndrUnit]
telescopeBndrs DForallTelescope
vs, DType
ty)
DForallT DForallTelescope
vs DType
ty -> (DTyVarBndrUnit -> Name
varBndrName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DForallTelescope -> [DTyVarBndrUnit]
telescopeBndrs DForallTelescope
vs, DType
ty)
DConstrainedT [DType]
_ DType
ty -> ([], DType
ty)
DType
ty -> ([], DType
ty)
telescopeBndrs :: DForallTelescope -> [DTyVarBndrUnit]
telescopeBndrs :: DForallTelescope -> [DTyVarBndrUnit]
telescopeBndrs = \case
DForallVis [DTyVarBndrUnit]
vs -> [DTyVarBndrUnit]
vs
DForallInvis [DTyVarBndrSpec]
vs -> (() forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DTyVarBndrSpec]
vs
unravel :: DType -> ([DTyVarBndrUnit], [DPred], [DType], DType)
unravel :: DType -> ([DTyVarBndrUnit], [DType], [DType], DType)
unravel DType
t =
let (DFunArgs
argList, DType
ret) = DType -> (DFunArgs, DType)
unravelDType DType
t
go :: DFunArgs -> ([DTyVarBndrUnit], [DType], [DType])
go = \case
DFunArgs
DFANil -> ([], [], [])
DFAForalls DForallTelescope
vs DFunArgs
as -> (DForallTelescope -> [DTyVarBndrUnit]
telescopeBndrs DForallTelescope
vs, [], []) forall a. Semigroup a => a -> a -> a
<> DFunArgs -> ([DTyVarBndrUnit], [DType], [DType])
go DFunArgs
as
DFACxt [DType]
preds DFunArgs
as -> ([], [DType]
preds, []) forall a. Semigroup a => a -> a -> a
<> DFunArgs -> ([DTyVarBndrUnit], [DType], [DType])
go DFunArgs
as
DFAAnon DType
a DFunArgs
as -> ([], [], [DType
a]) forall a. Semigroup a => a -> a -> a
<> DFunArgs -> ([DTyVarBndrUnit], [DType], [DType])
go DFunArgs
as
in let ([DTyVarBndrUnit]
vs, [DType]
preds, [DType]
args) = DFunArgs -> ([DTyVarBndrUnit], [DType], [DType])
go DFunArgs
argList in ([DTyVarBndrUnit]
vs, [DType]
preds, [DType]
args, DType
ret)
note :: MonadFail m => String -> Maybe a -> m a
note :: forall (m :: * -> *) a. MonadFail m => String -> Maybe a -> m a
note String
s = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
s) forall (f :: * -> *) a. Applicative f => a -> f a
pure