{-# LANGUAGE CPP #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ViewPatterns #-}

module Proof.Propositional.TH where

import Control.Arrow (Kleisli (..), second)
import Control.Monad (forM, zipWithM)
import Data.Foldable (asum)
import Data.Functor (void)
import Data.Map (Map)
import qualified Data.Map as M
import Data.Maybe (fromJust)
import Data.Type.Equality ((:~:) (..))
import Language.Haskell.TH (
  DecsQ,
  Lit (CharL, IntegerL),
  Name,
  Q,
  TypeQ,
  isInstance,
  newName,
  ppr,
 )
import Language.Haskell.TH.Desugar (DClause (..), DCon (..), DConFields (..), DCxt, DDec (..), DExp (..), DForallTelescope (..), DInfo (..), DLetDec (DFunD), DPat (DConP, DVarP), DPred, DTyVarBndr (..), DType (..), Overlap (Overlapping), desugar, dsReify, expandType, substTy, sweeten)
import Proof.Propositional.Empty
import Proof.Propositional.Inhabited

#if MIN_VERSION_th_desugar(1,18,0)
import Language.Haskell.TH.Desugar (dLamE, dCaseE)
#else
import Language.Haskell.TH.Desugar (DMatch)
#endif

mkDInstanceD ::
  Maybe Overlap ->
  DCxt ->
  DType ->
  [DDec] ->
  DDec
mkDInstanceD :: Maybe Overlap -> DCxt -> DType -> [DDec] -> DDec
mkDInstanceD Maybe Overlap
ovl DCxt
ctx DType
dtype [DDec]
ddecs = Maybe Overlap
-> Maybe [DTyVarBndrUnit] -> DCxt -> DType -> [DDec] -> DDec
DInstanceD Maybe Overlap
ovl Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing DCxt
ctx DType
dtype [DDec]
ddecs

{- | Macro to automatically derive @'Empty'@ instance for
  concrete (variable-free) types which may contain products.
-}
refute :: TypeQ -> DecsQ
refute :: TypeQ -> DecsQ
refute TypeQ
tps = do
  DType
tp <- DType -> Q DType
forall (q :: * -> *). DsMonad q => DType -> q DType
expandType (DType -> Q DType) -> Q DType -> Q DType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> Q DType
forall th ds (q :: * -> *).
(Desugar th ds, DsMonad q) =>
th -> q ds
forall (q :: * -> *). DsMonad q => Type -> q DType
desugar (Type -> Q DType) -> TypeQ -> Q DType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypeQ
tps
  let Just ([Name]
_, Name
tyName, DCxt
args) = DType -> Maybe ([Name], Name, DCxt)
splitType DType
tp
      mkInst :: DCxt -> [DClause] -> m [Dec]
mkInst DCxt
dxt [DClause]
cls =
        [Dec] -> m [Dec]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Dec] -> m [Dec]) -> [Dec] -> m [Dec]
forall a b. (a -> b) -> a -> b
$
          [DDec] -> [Dec]
forall th ds. Desugar th ds => ds -> th
sweeten
            [ Maybe Overlap -> DCxt -> DType -> [DDec] -> DDec
mkDInstanceD
                (Overlap -> Maybe Overlap
forall a. a -> Maybe a
Just Overlap
Overlapping)
                DCxt
dxt
                (DType -> DType -> DType
DAppT (Name -> DType
DConT ''Empty) ((DType -> DType -> DType) -> DType -> DCxt -> DType
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DType -> DType -> DType
DAppT (Name -> DType
DConT Name
tyName) DCxt
args))
                [DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ Name -> [DClause] -> DLetDec
DFunD 'eliminate [DClause]
cls]
            ]
  if Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''(:~:)
    then do
      let [DType
l, DType
r] = DCxt
args
      Name
v <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_v"
      EqlJudge
dist <- DType -> DType -> Q EqlJudge
compareType DType
l DType
r
      case EqlJudge
dist of
        EqlJudge
NonEqual -> DCxt -> [DClause] -> DecsQ
forall {m :: * -> *}. Monad m => DCxt -> [DClause] -> m [Dec]
mkInst [] [[DPat] -> DExp -> DClause
DClause [] (DExp -> DClause) -> DExp -> DClause
forall a b. (a -> b) -> a -> b
$ [Name] -> DExp -> DExp
dLamE' [Name
v] (DExp -> [DMatch] -> DExp
dCaseE (Name -> DExp
DVarE Name
v) [])]
        EqlJudge
Equal -> String -> DecsQ
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> DecsQ) -> String -> DecsQ
forall a b. (a -> b) -> a -> b
$ String
"Equal: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Type -> Doc
forall a. Ppr a => a -> Doc
ppr (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
l) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ~ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Type -> Doc
forall a. Ppr a => a -> Doc
ppr (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
r)
        EqlJudge
Undecidable ->
          String -> DecsQ
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> DecsQ) -> String -> DecsQ
forall a b. (a -> b) -> a -> b
$
            String
"No enough info to check non-equality: "
              String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Type -> Doc
forall a. Ppr a => a -> Doc
ppr (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
l)
              String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ~ "
              String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Type -> Doc
forall a. Ppr a => a -> Doc
ppr (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
r)
    else do
      (DCxt
dxt, [DCon]
cons) <- DCxt -> DInfo -> Q (DCxt, [DCon])
resolveSubsts DCxt
args (DInfo -> Q (DCxt, [DCon]))
-> (Maybe DInfo -> DInfo) -> Maybe DInfo -> Q (DCxt, [DCon])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe DInfo -> DInfo
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe DInfo -> Q (DCxt, [DCon]))
-> Q (Maybe DInfo) -> Q (DCxt, [DCon])
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Name -> Q (Maybe DInfo)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReify Name
tyName
      Just [DClause]
cls <- [Maybe DClause] -> Maybe [DClause]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([Maybe DClause] -> Maybe [DClause])
-> Q [Maybe DClause] -> Q (Maybe [DClause])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DCon -> Q (Maybe DClause)) -> [DCon] -> Q [Maybe DClause]
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 DCon -> Q (Maybe DClause)
buildRefuteClause [DCon]
cons
      DCxt -> [DClause] -> DecsQ
forall {m :: * -> *}. Monad m => DCxt -> [DClause] -> m [Dec]
mkInst DCxt
dxt [DClause]
cls

#if !MIN_VERSION_th_desugar(1,18,0)
dCaseE :: DExp -> [DMatch] -> DExp
dCaseE = DCaseE
#endif

dLamE' :: [Name] -> DExp -> DExp
#if MIN_VERSION_th_desugar(1,18,0)
dLamE' :: [Name] -> DExp -> DExp
dLamE' = [DPat] -> DExp -> DExp
dLamE ([DPat] -> DExp -> DExp)
-> ([Name] -> [DPat]) -> [Name] -> DExp -> DExp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> DPat) -> [Name] -> [DPat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DPat
DVarP
#else
dLamE' = DLamE
#endif

{- | Macro to automatically derive @'Inhabited'@ instance for
  concrete (variable-free) types which may contain sums.
-}
prove :: TypeQ -> DecsQ
prove :: TypeQ -> DecsQ
prove TypeQ
tps = do
  DType
tp <- DType -> Q DType
forall (q :: * -> *). DsMonad q => DType -> q DType
expandType (DType -> Q DType) -> Q DType -> Q DType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> Q DType
forall th ds (q :: * -> *).
(Desugar th ds, DsMonad q) =>
th -> q ds
forall (q :: * -> *). DsMonad q => Type -> q DType
desugar (Type -> Q DType) -> TypeQ -> Q DType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypeQ
tps
  let Just ([Name]
_, Name
tyName, DCxt
args) = DType -> Maybe ([Name], Name, DCxt)
splitType DType
tp
      mkInst :: DCxt -> [DClause] -> m [Dec]
mkInst DCxt
dxt [DClause]
cls =
        [Dec] -> m [Dec]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Dec] -> m [Dec]) -> [Dec] -> m [Dec]
forall a b. (a -> b) -> a -> b
$
          [DDec] -> [Dec]
forall th ds. Desugar th ds => ds -> th
sweeten
            [ Maybe Overlap -> DCxt -> DType -> [DDec] -> DDec
mkDInstanceD
                (Overlap -> Maybe Overlap
forall a. a -> Maybe a
Just Overlap
Overlapping)
                DCxt
dxt
                (DType -> DType -> DType
DAppT (Name -> DType
DConT ''Inhabited) ((DType -> DType -> DType) -> DType -> DCxt -> DType
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DType -> DType -> DType
DAppT (Name -> DType
DConT Name
tyName) DCxt
args))
                [DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ Name -> [DClause] -> DLetDec
DFunD 'trivial [DClause]
cls]
            ]
  Bool
isNum <- Name -> [Type] -> Q Bool
isInstance ''Num [DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
tp]

  if
    | Bool
isNum -> DCxt -> [DClause] -> DecsQ
forall {m :: * -> *}. Monad m => DCxt -> [DClause] -> m [Dec]
mkInst [] [[DPat] -> DExp -> DClause
DClause [] (DExp -> DClause) -> DExp -> DClause
forall a b. (a -> b) -> a -> b
$ Lit -> DExp
DLitE (Lit -> DExp) -> Lit -> DExp
forall a b. (a -> b) -> a -> b
$ Integer -> Lit
IntegerL Integer
0]
    | Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Char -> DCxt -> [DClause] -> DecsQ
forall {m :: * -> *}. Monad m => DCxt -> [DClause] -> m [Dec]
mkInst [] [[DPat] -> DExp -> DClause
DClause [] (DExp -> DClause) -> DExp -> DClause
forall a b. (a -> b) -> a -> b
$ Lit -> DExp
DLitE (Lit -> DExp) -> Lit -> DExp
forall a b. (a -> b) -> a -> b
$ Char -> Lit
CharL Char
'\NUL']
    | Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''(:~:) -> do
        let [DType
l, DType
r] = DCxt
args
        EqlJudge
dist <- DType -> DType -> Q EqlJudge
compareType DType
l DType
r
        case EqlJudge
dist of
          EqlJudge
NonEqual -> String -> DecsQ
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> DecsQ) -> String -> DecsQ
forall a b. (a -> b) -> a -> b
$ String
"Equal: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Type -> Doc
forall a. Ppr a => a -> Doc
ppr (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
l) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ~ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Type -> Doc
forall a. Ppr a => a -> Doc
ppr (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
r)
          EqlJudge
Equal -> DCxt -> [DClause] -> DecsQ
forall {m :: * -> *}. Monad m => DCxt -> [DClause] -> m [Dec]
mkInst [] [[DPat] -> DExp -> DClause
DClause [] (DExp -> DClause) -> DExp -> DClause
forall a b. (a -> b) -> a -> b
$ Name -> DExp
DConE 'Refl]
          EqlJudge
Undecidable ->
            String -> DecsQ
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> DecsQ) -> String -> DecsQ
forall a b. (a -> b) -> a -> b
$
              String
"No enough info to check non-equality: "
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Type -> Doc
forall a. Ppr a => a -> Doc
ppr (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
l)
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ~ "
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Type -> Doc
forall a. Ppr a => a -> Doc
ppr (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
r)
    | Bool
otherwise -> do
        (DCxt
dxt, [DCon]
cons) <- DCxt -> DInfo -> Q (DCxt, [DCon])
resolveSubsts DCxt
args (DInfo -> Q (DCxt, [DCon]))
-> (Maybe DInfo -> DInfo) -> Maybe DInfo -> Q (DCxt, [DCon])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe DInfo -> DInfo
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe DInfo -> Q (DCxt, [DCon]))
-> Q (Maybe DInfo) -> Q (DCxt, [DCon])
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Name -> Q (Maybe DInfo)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReify Name
tyName
        Just DClause
cls <- [Maybe DClause] -> Maybe DClause
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum ([Maybe DClause] -> Maybe DClause)
-> Q [Maybe DClause] -> Q (Maybe DClause)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DCon -> Q (Maybe DClause)) -> [DCon] -> Q [Maybe DClause]
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 DCon -> Q (Maybe DClause)
buildProveClause [DCon]
cons
        DCxt -> [DClause] -> DecsQ
forall {m :: * -> *}. Monad m => DCxt -> [DClause] -> m [Dec]
mkInst DCxt
dxt [DClause
cls]

buildClause ::
  Name ->
  (DType -> Q b) ->
  (DType -> b -> DExp) ->
  (Name -> [Maybe DExp] -> Maybe DExp) ->
  (Name -> [b] -> [DPat]) ->
  DCon ->
  Q (Maybe DClause)
buildClause :: forall b.
Name
-> (DType -> Q b)
-> (DType -> b -> DExp)
-> (Name -> [Maybe DExp] -> Maybe DExp)
-> (Name -> [b] -> [DPat])
-> DCon
-> Q (Maybe DClause)
buildClause Name
clsName DType -> Q b
genPlaceHolder DType -> b -> DExp
buildFactor Name -> [Maybe DExp] -> Maybe DExp
flattenExps Name -> [b] -> [DPat]
toPats (DCon [DTyVarBndrSpec]
_ DCxt
_ Name
cName DConFields
flds DType
_) = do
  let tys :: DCxt
tys = DConFields -> DCxt
fieldsVars DConFields
flds
  [b]
varDic <- (DType -> Q b) -> DCxt -> Q [b]
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 DType -> Q b
genPlaceHolder DCxt
tys
  (DExp -> DClause) -> Maybe DExp -> Maybe DClause
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([DPat] -> DExp -> DClause
DClause ([DPat] -> DExp -> DClause) -> [DPat] -> DExp -> DClause
forall a b. (a -> b) -> a -> b
$ Name -> [b] -> [DPat]
toPats Name
cName [b]
varDic) (Maybe DExp -> Maybe DClause)
-> ([Maybe DExp] -> Maybe DExp) -> [Maybe DExp] -> Maybe DClause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Maybe DExp] -> Maybe DExp
flattenExps Name
cName ([Maybe DExp] -> Maybe DClause)
-> Q [Maybe DExp] -> Q (Maybe DClause)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DType -> b -> Q (Maybe DExp)) -> DCxt -> [b] -> Q [Maybe DExp]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM DType -> b -> Q (Maybe DExp)
tryProc DCxt
tys [b]
varDic
  where
    tryProc :: DType -> b -> Q (Maybe DExp)
tryProc DType
ty b
name = do
      Bool
isEmpty <- Name -> [Type] -> Q Bool
isInstance Name
clsName ([Type] -> Q Bool) -> (Type -> [Type]) -> Type -> Q Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: []) (Type -> Q Bool) -> Type -> Q Bool
forall a b. (a -> b) -> a -> b
$ DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
ty
      Maybe DExp -> Q (Maybe DExp)
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe DExp -> Q (Maybe DExp)) -> Maybe DExp -> Q (Maybe DExp)
forall a b. (a -> b) -> a -> b
$
        if Bool
isEmpty
          then DExp -> Maybe DExp
forall a. a -> Maybe a
Just (DExp -> Maybe DExp) -> DExp -> Maybe DExp
forall a b. (a -> b) -> a -> b
$ DType -> b -> DExp
buildFactor DType
ty b
name
          else Maybe DExp
forall a. Maybe a
Nothing

buildRefuteClause :: DCon -> Q (Maybe DClause)
buildRefuteClause :: DCon -> Q (Maybe DClause)
buildRefuteClause =
  Name
-> (DType -> Q Name)
-> (DType -> Name -> DExp)
-> (Name -> [Maybe DExp] -> Maybe DExp)
-> (Name -> [Name] -> [DPat])
-> DCon
-> Q (Maybe DClause)
forall b.
Name
-> (DType -> Q b)
-> (DType -> b -> DExp)
-> (Name -> [Maybe DExp] -> Maybe DExp)
-> (Name -> [b] -> [DPat])
-> DCon
-> Q (Maybe DClause)
buildClause
    ''Empty
    (Q Name -> DType -> Q Name
forall a b. a -> b -> a
const (Q Name -> DType -> Q Name) -> Q Name -> DType -> Q Name
forall a b. (a -> b) -> a -> b
$ String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x")
    ((Name -> DExp) -> DType -> Name -> DExp
forall a b. a -> b -> a
const ((Name -> DExp) -> DType -> Name -> DExp)
-> (Name -> DExp) -> DType -> Name -> DExp
forall a b. (a -> b) -> a -> b
$ (Name -> DExp
DVarE 'eliminate DExp -> DExp -> DExp
`DAppE`) (DExp -> DExp) -> (Name -> DExp) -> Name -> DExp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> DExp
DVarE)
    (([Maybe DExp] -> Maybe DExp) -> Name -> [Maybe DExp] -> Maybe DExp
forall a b. a -> b -> a
const [Maybe DExp] -> Maybe DExp
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum)
    (\Name
cName [Name]
ps -> [Name -> DCxt -> [DPat] -> DPat
DConP Name
cName [] ([DPat] -> DPat) -> [DPat] -> DPat
forall a b. (a -> b) -> a -> b
$ (Name -> DPat) -> [Name] -> [DPat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DPat
DVarP [Name]
ps])

buildProveClause :: DCon -> Q (Maybe DClause)
buildProveClause :: DCon -> Q (Maybe DClause)
buildProveClause =
  Name
-> (DType -> Q ())
-> (DType -> () -> DExp)
-> (Name -> [Maybe DExp] -> Maybe DExp)
-> (Name -> [()] -> [DPat])
-> DCon
-> Q (Maybe DClause)
forall b.
Name
-> (DType -> Q b)
-> (DType -> b -> DExp)
-> (Name -> [Maybe DExp] -> Maybe DExp)
-> (Name -> [b] -> [DPat])
-> DCon
-> Q (Maybe DClause)
buildClause
    ''Inhabited
    (Q () -> DType -> Q ()
forall a b. a -> b -> a
const (Q () -> DType -> Q ()) -> Q () -> DType -> Q ()
forall a b. (a -> b) -> a -> b
$ () -> Q ()
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
    ((() -> DExp) -> DType -> () -> DExp
forall a b. a -> b -> a
const ((() -> DExp) -> DType -> () -> DExp)
-> (() -> DExp) -> DType -> () -> DExp
forall a b. (a -> b) -> a -> b
$ DExp -> () -> DExp
forall a b. a -> b -> a
const (DExp -> () -> DExp) -> DExp -> () -> DExp
forall a b. (a -> b) -> a -> b
$ Name -> DExp
DVarE 'trivial)
    (\Name
con [Maybe DExp]
args -> (DExp -> DExp -> DExp) -> DExp -> [DExp] -> DExp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DExp -> DExp -> DExp
DAppE (Name -> DExp
DConE Name
con) ([DExp] -> DExp) -> Maybe [DExp] -> Maybe DExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Maybe DExp] -> Maybe [DExp]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [Maybe DExp]
args)
    (([()] -> [DPat]) -> Name -> [()] -> [DPat]
forall a b. a -> b -> a
const (([()] -> [DPat]) -> Name -> [()] -> [DPat])
-> ([()] -> [DPat]) -> Name -> [()] -> [DPat]
forall a b. (a -> b) -> a -> b
$ [DPat] -> [()] -> [DPat]
forall a b. a -> b -> a
const [])

fieldsVars :: DConFields -> [DType]
fieldsVars :: DConFields -> DCxt
fieldsVars (DNormalC Bool
_ [DBangType]
fs) = (DBangType -> DType) -> [DBangType] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map DBangType -> DType
forall a b. (a, b) -> b
snd [DBangType]
fs
fieldsVars (DRecC [DVarBangType]
fs) = (DVarBangType -> DType) -> [DVarBangType] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
_, Bang
_, DType
c) -> DType
c) [DVarBangType]
fs

resolveSubsts :: [DType] -> DInfo -> Q (DCxt, [DCon])
resolveSubsts :: DCxt -> DInfo -> Q (DCxt, [DCon])
resolveSubsts DCxt
args DInfo
info =
  case DInfo
info of
    DTyConI (DDataD DataFlavor
_ DCxt
cxt Name
_ [DTyVarBndrUnit]
tvbs Maybe DType
_ [DCon]
dcons [DDerivClause]
_) Maybe [DDec]
_ -> do
      let dic :: Map Name DType
dic = [(Name, DType)] -> Map Name DType
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Name, DType)] -> Map Name DType)
-> [(Name, DType)] -> Map Name DType
forall a b. (a -> b) -> a -> b
$ [Name] -> DCxt -> [(Name, DType)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((DTyVarBndrUnit -> Name) -> [DTyVarBndrUnit] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrUnit -> Name
forall flag. DTyVarBndr flag -> Name
dtvbToName [DTyVarBndrUnit]
tvbs) DCxt
args
      (DCxt
cxt,) ([DCon] -> (DCxt, [DCon])) -> Q [DCon] -> Q (DCxt, [DCon])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DCon -> Q DCon) -> [DCon] -> Q [DCon]
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 (Map Name DType -> DCon -> Q DCon
substDCon Map Name DType
dic) [DCon]
dcons
    -- (DTyConI (DOpenTypeFamilyD n) _) ->  return []
    -- (DTyConI (DClosedTypeFamilyD _ ddec2) minst) ->  return []
    -- (DTyConI (DDataFamilyD _ ddec2) minst) ->  return []
    -- (DTyConI (DDataInstD _ ddec2 ddec3 ddec4 ddec5 ddec6) minst) ->  return []
    (DTyConI DDec
_ Maybe [DDec]
_) -> String -> Q (DCxt, [DCon])
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Not supported data ty"
    DInfo
_ -> String -> Q (DCxt, [DCon])
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Please pass data-type"

type SubstDic = Map Name DType

substDCon :: SubstDic -> DCon -> Q DCon
substDCon :: Map Name DType -> DCon -> Q DCon
substDCon Map Name DType
dic (DCon [DTyVarBndrSpec]
forall'd DCxt
cxt Name
conName DConFields
fields DType
mPhantom) =
  [DTyVarBndrSpec] -> DCxt -> Name -> DConFields -> DType -> DCon
DCon [DTyVarBndrSpec]
forall'd DCxt
cxt Name
conName
    (DConFields -> DType -> DCon) -> Q DConFields -> Q (DType -> DCon)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Name DType -> DConFields -> Q DConFields
substFields Map Name DType
dic DConFields
fields
    Q (DType -> DCon) -> Q DType -> Q DCon
forall a b. Q (a -> b) -> Q a -> Q b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map Name DType -> DType -> Q DType
forall (q :: * -> *). Quasi q => Map Name DType -> DType -> q DType
substTy Map Name DType
dic DType
mPhantom

substFields :: SubstDic -> DConFields -> Q DConFields
substFields :: Map Name DType -> DConFields -> Q DConFields
substFields
  Map Name DType
subst
  (DNormalC Bool
fixi [DBangType]
fs) =
    Bool -> [DBangType] -> DConFields
DNormalC Bool
fixi
      ([DBangType] -> DConFields) -> Q [DBangType] -> Q DConFields
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DBangType -> Q DBangType) -> [DBangType] -> Q [DBangType]
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 (Kleisli Q DBangType DBangType -> DBangType -> Q DBangType
forall (m :: * -> *) a b. Kleisli m a b -> a -> m b
runKleisli (Kleisli Q DBangType DBangType -> DBangType -> Q DBangType)
-> Kleisli Q DBangType DBangType -> DBangType -> Q DBangType
forall a b. (a -> b) -> a -> b
$ Kleisli Q DType DType -> Kleisli Q DBangType DBangType
forall b c d. Kleisli Q b c -> Kleisli Q (d, b) (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (Kleisli Q DType DType -> Kleisli Q DBangType DBangType)
-> Kleisli Q DType DType -> Kleisli Q DBangType DBangType
forall a b. (a -> b) -> a -> b
$ (DType -> Q DType) -> Kleisli Q DType DType
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli ((DType -> Q DType) -> Kleisli Q DType DType)
-> (DType -> Q DType) -> Kleisli Q DType DType
forall a b. (a -> b) -> a -> b
$ Map Name DType -> DType -> Q DType
forall (q :: * -> *). Quasi q => Map Name DType -> DType -> q DType
substTy Map Name DType
subst) [DBangType]
fs
substFields Map Name DType
subst (DRecC [DVarBangType]
fs) =
  [DVarBangType] -> DConFields
DRecC ([DVarBangType] -> DConFields) -> Q [DVarBangType] -> Q DConFields
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DVarBangType]
-> (DVarBangType -> Q DVarBangType) -> Q [DVarBangType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [DVarBangType]
fs (\(Name
a, Bang
b, DType
c) -> (Name
a,Bang
b,) (DType -> DVarBangType) -> Q DType -> Q DVarBangType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Name DType -> DType -> Q DType
forall (q :: * -> *). Quasi q => Map Name DType -> DType -> q DType
substTy Map Name DType
subst DType
c)

splitType :: DType -> Maybe ([Name], Name, [DType])
splitType :: DType -> Maybe ([Name], Name, DCxt)
splitType (DConstrainedT DCxt
_ DType
t) = DType -> Maybe ([Name], Name, DCxt)
splitType DType
t
splitType (DForallT (DForallTelescope -> [DTyVarBndrUnit]
unTelescope -> [DTyVarBndrUnit]
vs) DType
t) =
  (\([Name]
a, Name
b, DCxt
c) -> ((DTyVarBndrUnit -> Name) -> [DTyVarBndrUnit] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrUnit -> Name
forall flag. DTyVarBndr flag -> Name
dtvbToName [DTyVarBndrUnit]
vs [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
a, Name
b, DCxt
c)) (([Name], Name, DCxt) -> ([Name], Name, DCxt))
-> Maybe ([Name], Name, DCxt) -> Maybe ([Name], Name, DCxt)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> Maybe ([Name], Name, DCxt)
splitType DType
t
splitType (DAppT DType
t1 DType
t2) = (\([Name]
a, Name
b, DCxt
c) -> ([Name]
a, Name
b, DCxt
c DCxt -> DCxt -> DCxt
forall a. [a] -> [a] -> [a]
++ [DType
t2])) (([Name], Name, DCxt) -> ([Name], Name, DCxt))
-> Maybe ([Name], Name, DCxt) -> Maybe ([Name], Name, DCxt)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> Maybe ([Name], Name, DCxt)
splitType DType
t1
splitType (DSigT DType
t DType
_) = DType -> Maybe ([Name], Name, DCxt)
splitType DType
t
splitType (DVarT Name
_) = Maybe ([Name], Name, DCxt)
forall a. Maybe a
Nothing
splitType (DConT Name
n) = ([Name], Name, DCxt) -> Maybe ([Name], Name, DCxt)
forall a. a -> Maybe a
Just ([], Name
n, [])
splitType DType
DArrowT = ([Name], Name, DCxt) -> Maybe ([Name], Name, DCxt)
forall a. a -> Maybe a
Just ([], ''(->), [])
splitType (DLitT TyLit
_) = Maybe ([Name], Name, DCxt)
forall a. Maybe a
Nothing
splitType DType
DWildCardT = Maybe ([Name], Name, DCxt)
forall a. Maybe a
Nothing
splitType (DAppKindT DType
_ DType
_) = Maybe ([Name], Name, DCxt)
forall a. Maybe a
Nothing

data EqlJudge = NonEqual | Undecidable | Equal
  deriving (ReadPrec [EqlJudge]
ReadPrec EqlJudge
Int -> ReadS EqlJudge
ReadS [EqlJudge]
(Int -> ReadS EqlJudge)
-> ReadS [EqlJudge]
-> ReadPrec EqlJudge
-> ReadPrec [EqlJudge]
-> Read EqlJudge
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS EqlJudge
readsPrec :: Int -> ReadS EqlJudge
$creadList :: ReadS [EqlJudge]
readList :: ReadS [EqlJudge]
$creadPrec :: ReadPrec EqlJudge
readPrec :: ReadPrec EqlJudge
$creadListPrec :: ReadPrec [EqlJudge]
readListPrec :: ReadPrec [EqlJudge]
Read, Int -> EqlJudge -> String -> String
[EqlJudge] -> String -> String
EqlJudge -> String
(Int -> EqlJudge -> String -> String)
-> (EqlJudge -> String)
-> ([EqlJudge] -> String -> String)
-> Show EqlJudge
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> EqlJudge -> String -> String
showsPrec :: Int -> EqlJudge -> String -> String
$cshow :: EqlJudge -> String
show :: EqlJudge -> String
$cshowList :: [EqlJudge] -> String -> String
showList :: [EqlJudge] -> String -> String
Show, EqlJudge -> EqlJudge -> Bool
(EqlJudge -> EqlJudge -> Bool)
-> (EqlJudge -> EqlJudge -> Bool) -> Eq EqlJudge
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: EqlJudge -> EqlJudge -> Bool
== :: EqlJudge -> EqlJudge -> Bool
$c/= :: EqlJudge -> EqlJudge -> Bool
/= :: EqlJudge -> EqlJudge -> Bool
Eq, Eq EqlJudge
Eq EqlJudge =>
(EqlJudge -> EqlJudge -> Ordering)
-> (EqlJudge -> EqlJudge -> Bool)
-> (EqlJudge -> EqlJudge -> Bool)
-> (EqlJudge -> EqlJudge -> Bool)
-> (EqlJudge -> EqlJudge -> Bool)
-> (EqlJudge -> EqlJudge -> EqlJudge)
-> (EqlJudge -> EqlJudge -> EqlJudge)
-> Ord EqlJudge
EqlJudge -> EqlJudge -> Bool
EqlJudge -> EqlJudge -> Ordering
EqlJudge -> EqlJudge -> EqlJudge
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: EqlJudge -> EqlJudge -> Ordering
compare :: EqlJudge -> EqlJudge -> Ordering
$c< :: EqlJudge -> EqlJudge -> Bool
< :: EqlJudge -> EqlJudge -> Bool
$c<= :: EqlJudge -> EqlJudge -> Bool
<= :: EqlJudge -> EqlJudge -> Bool
$c> :: EqlJudge -> EqlJudge -> Bool
> :: EqlJudge -> EqlJudge -> Bool
$c>= :: EqlJudge -> EqlJudge -> Bool
>= :: EqlJudge -> EqlJudge -> Bool
$cmax :: EqlJudge -> EqlJudge -> EqlJudge
max :: EqlJudge -> EqlJudge -> EqlJudge
$cmin :: EqlJudge -> EqlJudge -> EqlJudge
min :: EqlJudge -> EqlJudge -> EqlJudge
Ord)

instance Semigroup EqlJudge where
  EqlJudge
NonEqual <> :: EqlJudge -> EqlJudge -> EqlJudge
<> EqlJudge
_ = EqlJudge
NonEqual
  EqlJudge
Undecidable <> EqlJudge
NonEqual = EqlJudge
NonEqual
  EqlJudge
Undecidable <> EqlJudge
_ = EqlJudge
Undecidable
  EqlJudge
Equal <> EqlJudge
m = EqlJudge
m

instance Monoid EqlJudge where
  mappend :: EqlJudge -> EqlJudge -> EqlJudge
mappend = EqlJudge -> EqlJudge -> EqlJudge
forall a. Semigroup a => a -> a -> a
(<>)
  mempty :: EqlJudge
mempty = EqlJudge
Equal

compareType :: DType -> DType -> Q EqlJudge
compareType :: DType -> DType -> Q EqlJudge
compareType DType
t0 DType
s0 = do
  DType
t <- DType -> Q DType
forall (q :: * -> *). DsMonad q => DType -> q DType
expandType DType
t0
  DType
s <- DType -> Q DType
forall (q :: * -> *). DsMonad q => DType -> q DType
expandType DType
s0
  DType -> DType -> Q EqlJudge
compareType' DType
t DType
s

compareType' :: DType -> DType -> Q EqlJudge
compareType' :: DType -> DType -> Q EqlJudge
compareType' (DSigT DType
t1 DType
t2) (DSigT DType
s1 DType
s2) =
  EqlJudge -> EqlJudge -> EqlJudge
forall a. Semigroup a => a -> a -> a
(<>) (EqlJudge -> EqlJudge -> EqlJudge)
-> Q EqlJudge -> Q (EqlJudge -> EqlJudge)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> DType -> Q EqlJudge
compareType' DType
t1 DType
s1 Q (EqlJudge -> EqlJudge) -> Q EqlJudge -> Q EqlJudge
forall a b. Q (a -> b) -> Q a -> Q b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DType -> DType -> Q EqlJudge
compareType' DType
t2 DType
s2
compareType' (DSigT DType
t DType
_) DType
s =
  DType -> DType -> Q EqlJudge
compareType' DType
t DType
s
compareType' DType
t (DSigT DType
s DType
_) =
  DType -> DType -> Q EqlJudge
compareType' DType
t DType
s
compareType' (DVarT Name
t) (DVarT Name
s)
  | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
s = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
  | Bool
otherwise = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
compareType' (DVarT Name
_) DType
_ = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
compareType' DType
_ (DVarT Name
_) = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
compareType' DType
DWildCardT DType
_ = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
compareType' DType
_ DType
DWildCardT = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
compareType' (DConstrainedT DCxt
tCxt DType
t) (DConstrainedT DCxt
sCxt DType
s) = do
  EqlJudge
pd <- DCxt -> DCxt -> Q EqlJudge
compareCxt DCxt
tCxt DCxt
sCxt
  EqlJudge
bd <- DType -> DType -> Q EqlJudge
compareType' DType
t DType
s
  EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (EqlJudge
pd EqlJudge -> EqlJudge -> EqlJudge
forall a. Semigroup a => a -> a -> a
<> EqlJudge
bd)
compareType' DConstrainedT {} DType
_ = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' (DForallT (DForallTelescope -> [DTyVarBndrUnit]
unTelescope -> [DTyVarBndrUnit]
tTvBs) DType
t) (DForallT (DForallTelescope -> [DTyVarBndrUnit]
unTelescope -> [DTyVarBndrUnit]
sTvBs) DType
s)
  | [DTyVarBndrUnit] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DTyVarBndrUnit]
tTvBs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [DTyVarBndrUnit] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DTyVarBndrUnit]
sTvBs = do
      let dic :: Map Name DType
dic = [(Name, DType)] -> Map Name DType
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Name, DType)] -> Map Name DType)
-> [(Name, DType)] -> Map Name DType
forall a b. (a -> b) -> a -> b
$ [Name] -> DCxt -> [(Name, DType)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((DTyVarBndrUnit -> Name) -> [DTyVarBndrUnit] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrUnit -> Name
forall flag. DTyVarBndr flag -> Name
dtvbToName [DTyVarBndrUnit]
sTvBs) ((DTyVarBndrUnit -> DType) -> [DTyVarBndrUnit] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (Name -> DType
DVarT (Name -> DType)
-> (DTyVarBndrUnit -> Name) -> DTyVarBndrUnit -> DType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DTyVarBndrUnit -> Name
forall flag. DTyVarBndr flag -> Name
dtvbToName) [DTyVarBndrUnit]
tTvBs)
      DType
s' <- Map Name DType -> DType -> Q DType
forall (q :: * -> *). Quasi q => Map Name DType -> DType -> q DType
substTy Map Name DType
dic DType
s
      EqlJudge
bd <- DType -> DType -> Q EqlJudge
compareType' DType
t DType
s'
      EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
bd
  | Bool
otherwise = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' DForallT {} DType
_ = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' (DAppT DType
t1 DType
t2) (DAppT DType
s1 DType
s2) =
  EqlJudge -> EqlJudge -> EqlJudge
forall a. Semigroup a => a -> a -> a
(<>) (EqlJudge -> EqlJudge -> EqlJudge)
-> Q EqlJudge -> Q (EqlJudge -> EqlJudge)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> DType -> Q EqlJudge
compareType' DType
t1 DType
s1 Q (EqlJudge -> EqlJudge) -> Q EqlJudge -> Q EqlJudge
forall a b. Q (a -> b) -> Q a -> Q b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DType -> DType -> Q EqlJudge
compareType' DType
t2 DType
s2
compareType' (DConT Name
t) (DConT Name
s)
  | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
s = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
  | Bool
otherwise = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' (DConT Name
_) DType
_ = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' DType
DArrowT DType
DArrowT = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
compareType' DType
DArrowT DType
_ = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' (DLitT TyLit
t) (DLitT TyLit
s)
  | TyLit
t TyLit -> TyLit -> Bool
forall a. Eq a => a -> a -> Bool
== TyLit
s = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
  | Bool
otherwise = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' (DLitT TyLit
_) DType
_ = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' DType
_ DType
_ = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual

compareCxt :: DCxt -> DCxt -> Q EqlJudge
compareCxt :: DCxt -> DCxt -> Q EqlJudge
compareCxt DCxt
l DCxt
r = [EqlJudge] -> EqlJudge
forall a. Monoid a => [a] -> a
mconcat ([EqlJudge] -> EqlJudge) -> Q [EqlJudge] -> Q EqlJudge
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DType -> DType -> Q EqlJudge) -> DCxt -> DCxt -> Q [EqlJudge]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM DType -> DType -> Q EqlJudge
comparePred DCxt
l DCxt
r

comparePred :: DPred -> DPred -> Q EqlJudge
comparePred :: DType -> DType -> Q EqlJudge
comparePred DType
DWildCardT DType
_ = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
comparePred DType
_ DType
DWildCardT = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
comparePred (DVarT Name
l) (DVarT Name
r)
  | Name
l Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
r = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
comparePred (DVarT Name
_) DType
_ = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
comparePred DType
_ (DVarT Name
_) = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
comparePred (DSigT DType
l DType
t) (DSigT DType
r DType
s) =
  EqlJudge -> EqlJudge -> EqlJudge
forall a. Semigroup a => a -> a -> a
(<>) (EqlJudge -> EqlJudge -> EqlJudge)
-> Q EqlJudge -> Q (EqlJudge -> EqlJudge)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> DType -> Q EqlJudge
compareType' DType
t DType
s Q (EqlJudge -> EqlJudge) -> Q EqlJudge -> Q EqlJudge
forall a b. Q (a -> b) -> Q a -> Q b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DType -> DType -> Q EqlJudge
comparePred DType
l DType
r
comparePred (DSigT DType
l DType
_) DType
r = DType -> DType -> Q EqlJudge
comparePred DType
l DType
r
comparePred DType
l (DSigT DType
r DType
_) = DType -> DType -> Q EqlJudge
comparePred DType
l DType
r
comparePred (DAppT DType
l1 DType
l2) (DAppT DType
r1 DType
r2) = do
  DType
l2' <- DType -> Q DType
forall (q :: * -> *). DsMonad q => DType -> q DType
expandType DType
l2
  DType
r2' <- DType -> Q DType
forall (q :: * -> *). DsMonad q => DType -> q DType
expandType DType
r2
  EqlJudge -> EqlJudge -> EqlJudge
forall a. Semigroup a => a -> a -> a
(<>) (EqlJudge -> EqlJudge -> EqlJudge)
-> Q EqlJudge -> Q (EqlJudge -> EqlJudge)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> DType -> Q EqlJudge
comparePred DType
l1 DType
r1 Q (EqlJudge -> EqlJudge) -> Q EqlJudge -> Q EqlJudge
forall a b. Q (a -> b) -> Q a -> Q b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DType -> DType -> Q EqlJudge
compareType' DType
l2' DType
r2'
comparePred (DAppT DType
_ DType
_) DType
_ = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
comparePred (DConT Name
l) (DConT Name
r)
  | Name
l Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
r = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
  | Bool
otherwise = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
comparePred (DConT Name
_) DType
_ = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
comparePred (DForallT DForallTelescope
_ DType
_) (DForallT DForallTelescope
_ DType
_) = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
comparePred (DForallT {}) DType
_ = EqlJudge -> Q EqlJudge
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
comparePred DType
_ DType
_ = String -> Q EqlJudge
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Kind error: Expecting type-level predicate"

substPred :: SubstDic -> DPred -> Q DPred
substPred :: Map Name DType -> DType -> Q DType
substPred Map Name DType
dic (DAppT DType
p1 DType
p2) = DType -> DType -> DType
DAppT (DType -> DType -> DType) -> Q DType -> Q (DType -> DType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Name DType -> DType -> Q DType
substPred Map Name DType
dic DType
p1 Q (DType -> DType) -> Q DType -> Q DType
forall a b. Q (a -> b) -> Q a -> Q b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (DType -> Q DType
forall (q :: * -> *). DsMonad q => DType -> q DType
expandType (DType -> Q DType) -> Q DType -> Q DType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Map Name DType -> DType -> Q DType
forall (q :: * -> *). Quasi q => Map Name DType -> DType -> q DType
substTy Map Name DType
dic DType
p2)
substPred Map Name DType
dic (DSigT DType
p DType
knd) = DType -> DType -> DType
DSigT (DType -> DType -> DType) -> Q DType -> Q (DType -> DType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Name DType -> DType -> Q DType
substPred Map Name DType
dic DType
p Q (DType -> DType) -> Q DType -> Q DType
forall a b. Q (a -> b) -> Q a -> Q b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (DType -> Q DType
forall (q :: * -> *). DsMonad q => DType -> q DType
expandType (DType -> Q DType) -> Q DType -> Q DType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Map Name DType -> DType -> Q DType
forall (q :: * -> *). Quasi q => Map Name DType -> DType -> q DType
substTy Map Name DType
dic DType
knd)
substPred Map Name DType
dic prd :: DType
prd@(DVarT Name
p)
  | Just (DVarT Name
t) <- Name -> Map Name DType -> Maybe DType
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
p Map Name DType
dic = DType -> Q DType
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> Q DType) -> DType -> Q DType
forall a b. (a -> b) -> a -> b
$ Name -> DType
DVarT Name
t
  | Just (DConT Name
t) <- Name -> Map Name DType -> Maybe DType
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
p Map Name DType
dic = DType -> Q DType
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> Q DType) -> DType -> Q DType
forall a b. (a -> b) -> a -> b
$ Name -> DType
DConT Name
t
  | Bool
otherwise = DType -> Q DType
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return DType
prd
substPred Map Name DType
_ DType
t = DType -> Q DType
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return DType
t

dtvbToName :: DTyVarBndr flag -> Name
dtvbToName :: forall flag. DTyVarBndr flag -> Name
dtvbToName (DPlainTV Name
n flag
_) = Name
n
dtvbToName (DKindedTV Name
n flag
_ DType
_) = Name
n

unTelescope :: DForallTelescope -> [DTyVarBndr ()]
unTelescope :: DForallTelescope -> [DTyVarBndrUnit]
unTelescope (DForallVis [DTyVarBndrUnit]
vis) = (DTyVarBndrUnit -> DTyVarBndrUnit)
-> [DTyVarBndrUnit] -> [DTyVarBndrUnit]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrUnit -> DTyVarBndrUnit
forall (f :: * -> *) a. Functor f => f a -> f ()
void [DTyVarBndrUnit]
vis
unTelescope (DForallInvis [DTyVarBndrSpec]
vis) = (DTyVarBndrSpec -> DTyVarBndrUnit)
-> [DTyVarBndrSpec] -> [DTyVarBndrUnit]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrSpec -> DTyVarBndrUnit
forall (f :: * -> *) a. Functor f => f a -> f ()
void [DTyVarBndrSpec]
vis