{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE UndecidableInstances   #-}
{-# LANGUAGE OverloadedStrings      #-}
{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE TupleSections    #-}

module Language.Haskell.Liquid.Measure (
  -- * Specifications
    Spec (..)
  , MSpec (..)

  -- * Type Aliases
  , BareSpec
  , BareMeasure
  , SpecMeasure

  -- * Constructors
  , mkM, mkMSpec, mkMSpec'
  , dataConTypes
  , defRefType
  , bodyPred
  ) where

import           GHC                                    hiding (Located)
import           Prelude                                hiding (error)
import           Text.PrettyPrint.HughesPJ              hiding ((<>))
-- import           Data.Binary                            as B
-- import           GHC.Generics
import qualified Data.HashMap.Strict                    as M
import qualified Data.List                              as L
import qualified Data.Maybe                             as Mb -- (fromMaybe, isNothing)

import           Language.Fixpoint.Misc
import           Language.Fixpoint.Types                hiding (panic, R, DataDecl, SrcSpan, LocSymbol)
import           Liquid.GHC.API        as Ghc hiding (Expr, showPpr, panic, (<+>))
import           Language.Haskell.Liquid.GHC.Misc
-- import qualified Language.Haskell.Liquid.Misc as Misc
import           Language.Haskell.Liquid.Types.Types    -- hiding (GhcInfo(..), GhcSpec (..))
import           Language.Haskell.Liquid.Types.RefType
-- import           Language.Haskell.Liquid.Types.Variance
-- import           Language.Haskell.Liquid.Types.Bounds
import           Language.Haskell.Liquid.Types.Specs hiding (BareSpec)
import           Language.Haskell.Liquid.UX.Tidy

-- /FIXME/: This needs to be removed once the port to the new API is complete.
type BareSpec = Spec LocBareType LocSymbol

mkM ::  LocSymbol -> ty -> [Def ty bndr] -> MeasureKind -> UnSortedExprs -> Measure ty bndr
mkM :: forall ty bndr.
LocSymbol
-> ty
-> [Def ty bndr]
-> MeasureKind
-> UnSortedExprs
-> Measure ty bndr
mkM LocSymbol
name ty
typ [Def ty bndr]
eqns MeasureKind
kind UnSortedExprs
u
  | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((LocSymbol
name forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty ctor. Def ty ctor -> LocSymbol
measure) [Def ty bndr]
eqns
  = forall ty bndr.
LocSymbol
-> ty
-> [Def ty bndr]
-> MeasureKind
-> UnSortedExprs
-> Measure ty bndr
M LocSymbol
name ty
typ [Def ty bndr]
eqns MeasureKind
kind UnSortedExprs
u
  | Bool
otherwise
  = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ [Char]
"invalid measure definition for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show LocSymbol
name

mkMSpec' :: Symbolic ctor => [Measure ty ctor] -> MSpec ty ctor
mkMSpec' :: forall ctor ty. Symbolic ctor => [Measure ty ctor] -> MSpec ty ctor
mkMSpec' [Measure ty ctor]
ms = forall ty ctor.
HashMap Symbol [Def ty ctor]
-> HashMap LocSymbol (Measure ty ctor)
-> HashMap LocSymbol (Measure ty ())
-> [Measure ty ctor]
-> MSpec ty ctor
MSpec HashMap Symbol [Def ty ctor]
cm HashMap LocSymbol (Measure ty ctor)
mm forall k v. HashMap k v
M.empty []
  where
    cm :: HashMap Symbol [Def ty ctor]
cm     = forall k a. (Eq k, Hashable k) => (a -> k) -> [a] -> HashMap k [a]
groupMap (forall a. Symbolic a => a -> Symbol
symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty ctor. Def ty ctor -> ctor
ctor) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall ty ctor. Measure ty ctor -> [Def ty ctor]
msEqns [Measure ty ctor]
ms
    mm :: HashMap LocSymbol (Measure ty ctor)
mm     = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(forall ty ctor. Measure ty ctor -> LocSymbol
msName Measure ty ctor
m, Measure ty ctor
m) | Measure ty ctor
m <- [Measure ty ctor]
ms ]

mkMSpec :: [Measure t LocSymbol] -> [Measure t ()] -> [Measure t LocSymbol] -> MSpec t LocSymbol
mkMSpec :: forall t.
[Measure t LocSymbol]
-> [Measure t ()] -> [Measure t LocSymbol] -> MSpec t LocSymbol
mkMSpec [Measure t LocSymbol]
ms [Measure t ()]
cms [Measure t LocSymbol]
ims = forall ty ctor.
HashMap Symbol [Def ty ctor]
-> HashMap LocSymbol (Measure ty ctor)
-> HashMap LocSymbol (Measure ty ())
-> [Measure ty ctor]
-> MSpec ty ctor
MSpec HashMap Symbol [Def t LocSymbol]
cm HashMap LocSymbol (Measure t LocSymbol)
mm HashMap LocSymbol (Measure t ())
cmm [Measure t LocSymbol]
ims
  where
    cm :: HashMap Symbol [Def t LocSymbol]
cm     = forall k a. (Eq k, Hashable k) => (a -> k) -> [a] -> HashMap k [a]
groupMap (forall a. Located a -> a
val forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty ctor. Def ty ctor -> ctor
ctor) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall ty ctor. Measure ty ctor -> [Def ty ctor]
msEqns ([Measure t LocSymbol]
ms'forall a. [a] -> [a] -> [a]
++[Measure t LocSymbol]
ims)
    mm :: HashMap LocSymbol (Measure t LocSymbol)
mm     = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(forall ty ctor. Measure ty ctor -> LocSymbol
msName Measure t LocSymbol
m, Measure t LocSymbol
m) | Measure t LocSymbol
m <- [Measure t LocSymbol]
ms' ]
    cmm :: HashMap LocSymbol (Measure t ())
cmm    = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(forall ty ctor. Measure ty ctor -> LocSymbol
msName Measure t ()
m, Measure t ()
m) | Measure t ()
m <- [Measure t ()]
cms ]
    ms' :: [Measure t LocSymbol]
ms'    = forall ty ctor. [Measure ty ctor] -> [Measure ty ctor]
checkDuplicateMeasure [Measure t LocSymbol]
ms


checkDuplicateMeasure :: [Measure ty ctor] -> [Measure ty ctor]
checkDuplicateMeasure :: forall ty ctor. [Measure ty ctor] -> [Measure ty ctor]
checkDuplicateMeasure [Measure ty ctor]
measures
  = case forall k v. HashMap k v -> [(k, v)]
M.toList HashMap LocSymbol [Measure ty ctor]
dups of
      []         -> [Measure ty ctor]
measures
      (LocSymbol
m,[Measure ty ctor]
ms):[(LocSymbol, [Measure ty ctor])]
_   -> forall a. UserError -> a
uError forall a b. (a -> b) -> a -> b
$ forall {a} {a} {t}.
(PPrint a, Loc a) =>
Located a -> [a] -> TError t
mkError LocSymbol
m (forall ty ctor. Measure ty ctor -> LocSymbol
msName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Measure ty ctor]
ms)
    where
      gms :: HashMap LocSymbol [Measure ty ctor]
gms        = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
group [(forall ty ctor. Measure ty ctor -> LocSymbol
msName Measure ty ctor
m , Measure ty ctor
m) | Measure ty ctor
m <- [Measure ty ctor]
measures]
      dups :: HashMap LocSymbol [Measure ty ctor]
dups       = forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
M.filter ((Int
1 forall a. Ord a => a -> a -> Bool
<) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Int
length) HashMap LocSymbol [Measure ty ctor]
gms
      mkError :: Located a -> [a] -> TError t
mkError Located a
m [a]
ms = forall t. SrcSpan -> Doc -> [SrcSpan] -> TError t
ErrDupMeas (forall a. Loc a => a -> SrcSpan
fSrcSpan Located a
m) (forall a. PPrint a => a -> Doc
pprint (forall a. Located a -> a
val Located a
m)) (forall a. Loc a => a -> SrcSpan
fSrcSpan forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
ms)


dataConTypes :: Bool -> MSpec (RRType Reft) DataCon -> ([(Var, RRType Reft)], [(LocSymbol, RRType Reft)])
dataConTypes :: Bool
-> MSpec (RRType Reft) DataCon
-> ([(Var, RRType Reft)], [(LocSymbol, RRType Reft)])
dataConTypes Bool
allowTC  MSpec (RRType Reft) DataCon
s = ([(Var, RRType Reft)]
ctorTys, [(LocSymbol, RRType Reft)]
measTys)
  where
    measTys :: [(LocSymbol, RRType Reft)]
measTys     = [(forall ty ctor. Measure ty ctor -> LocSymbol
msName Measure (RRType Reft) DataCon
m, forall ty ctor. Measure ty ctor -> ty
msSort Measure (RRType Reft) DataCon
m) | Measure (RRType Reft) DataCon
m <- forall k v. HashMap k v -> [v]
M.elems (forall ty ctor.
MSpec ty ctor -> HashMap LocSymbol (Measure ty ctor)
measMap MSpec (RRType Reft) DataCon
s) forall a. [a] -> [a] -> [a]
++ forall ty ctor. MSpec ty ctor -> [Measure ty ctor]
imeas MSpec (RRType Reft) DataCon
s]
    ctorTys :: [(Var, RRType Reft)]
ctorTys     = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Bool -> [Def (RRType Reft) DataCon] -> [(Var, RRType Reft)]
makeDataConType Bool
allowTC) (forall a. PPrint a => [Char] -> a -> a
notracepp [Char]
"HOHOH" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k v. HashMap k v -> [(k, v)]
M.toList (forall ty ctor. MSpec ty ctor -> HashMap Symbol [Def ty ctor]
ctorMap MSpec (RRType Reft) DataCon
s))

makeDataConType :: Bool -> [Def (RRType Reft) DataCon] -> [(Var, RRType Reft)]
makeDataConType :: Bool -> [Def (RRType Reft) DataCon] -> [(Var, RRType Reft)]
makeDataConType Bool
_ []
  = []
makeDataConType Bool
allowTC [Def (RRType Reft) DataCon]
ds | forall a. Maybe a -> Bool
Mb.isNothing (DataCon -> Maybe Var
dataConWrapId_maybe DataCon
dc)
  = forall a. PPrint a => [Char] -> a -> a
notracepp [Char]
_msg [(Var
woId, forall a. PPrint a => [Char] -> a -> a
notracepp [Char]
_msg forall a b. (a -> b) -> a -> b
$ [Char] -> Type -> [RRType Reft] -> RRType Reft
combineDCTypes [Char]
"cdc0" Type
t [RRType Reft]
ts)]
  where
    dc :: DataCon
dc   = forall ty ctor. Def ty ctor -> ctor
ctor (forall a. [a] -> a
head [Def (RRType Reft) DataCon]
ds)
    woId :: Var
woId = DataCon -> Var
dataConWorkId DataCon
dc
    t :: Type
t    = Var -> Type
varType Var
woId
    ts :: [RRType Reft]
ts   = Bool -> Type -> Def (RRType Reft) DataCon -> RRType Reft
defRefType Bool
allowTC Type
t forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Def (RRType Reft) DataCon]
ds
    _msg :: [Char]
_msg  = [Char]
"makeDataConType0" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp (Var
woId, Type
t, [RRType Reft]
ts)

makeDataConType Bool
allowTC [Def (RRType Reft) DataCon]
ds
  = [(Var
woId, Bool -> SourcePos -> RRType Reft -> RRType Reft -> RRType Reft
extend Bool
allowTC SourcePos
loci RRType Reft
woRType RRType Reft
wrRType), (Var
wrId, Bool -> SourcePos -> RRType Reft -> RRType Reft -> RRType Reft
extend Bool
allowTC SourcePos
loci RRType Reft
wrRType RRType Reft
woRType)]
  where
    ([Def (RRType Reft) DataCon]
wo, [Def (RRType Reft) DataCon]
wr) = forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition forall {ty} {ctor}. Def ty ctor -> Bool
isWorkerDef [Def (RRType Reft) DataCon]
ds
    dc :: DataCon
dc       = forall ty ctor. Def ty ctor -> ctor
ctor forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
head [Def (RRType Reft) DataCon]
ds
    loci :: SourcePos
loci     = forall a. Located a -> SourcePos
loc forall a b. (a -> b) -> a -> b
$ forall ty ctor. Def ty ctor -> LocSymbol
measure forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
head [Def (RRType Reft) DataCon]
ds
    woId :: Var
woId     = DataCon -> Var
dataConWorkId DataCon
dc
    wot :: Type
wot      = Var -> Type
varType Var
woId
    wrId :: Var
wrId     = DataCon -> Var
dataConWrapId DataCon
dc
    wrt :: Type
wrt      = Var -> Type
varType Var
wrId
    wots :: [RRType Reft]
wots     = Bool -> Type -> Def (RRType Reft) DataCon -> RRType Reft
defRefType Bool
allowTC Type
wot forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Def (RRType Reft) DataCon]
wo
    wrts :: [RRType Reft]
wrts     = Bool -> Type -> Def (RRType Reft) DataCon -> RRType Reft
defRefType Bool
allowTC Type
wrt forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Def (RRType Reft) DataCon]
wr

    wrRType :: RRType Reft
wrRType  = [Char] -> Type -> [RRType Reft] -> RRType Reft
combineDCTypes [Char]
"cdc1" Type
wrt [RRType Reft]
wrts
    woRType :: RRType Reft
woRType  = [Char] -> Type -> [RRType Reft] -> RRType Reft
combineDCTypes [Char]
"cdc2" Type
wot [RRType Reft]
wots


    isWorkerDef :: Def ty ctor -> Bool
isWorkerDef Def ty ctor
def
      -- types are missing for arguments, so definition came from a logical measure
      -- and it is for the worker datacon
      | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. Maybe a -> Bool
Mb.isNothing (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ty ctor. Def ty ctor -> [(Symbol, Maybe ty)]
binds Def ty ctor
def)
      = Bool
True
      | Bool
otherwise
      = forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall ty ctor. Def ty ctor -> [(Symbol, Maybe ty)]
binds Def ty ctor
def) forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Type -> ([Scaled Type], Type)
splitFunTys forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ Type -> ([Var], Type)
splitForAllTyCoVars Type
wot)


extend :: Bool
       -> SourcePos
       -> RType RTyCon RTyVar Reft
       -> RRType Reft
       -> RType RTyCon RTyVar Reft
extend :: Bool -> SourcePos -> RRType Reft -> RRType Reft -> RRType Reft
extend Bool
allowTC SourcePos
lc RRType Reft
t1' RRType Reft
t2
  | Just Subst
su <- Bool -> SourcePos -> RRType Reft -> RRType Reft -> Maybe Subst
mapArgumens Bool
allowTC SourcePos
lc RRType Reft
t1 RRType Reft
t2
  = RRType Reft
t1 forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthenResult` forall a. Subable a => Subst -> a -> a
subst Subst
su (forall a. a -> Maybe a -> a
Mb.fromMaybe forall a. Monoid a => a
mempty (forall c tv r. RType c tv r -> Maybe r
stripRTypeBase forall a b. (a -> b) -> a -> b
$ forall c tv r. RType c tv r -> RType c tv r
resultTy RRType Reft
t2))
  | Bool
otherwise
  = RRType Reft
t1
  where
    t1 :: RRType Reft
t1 = forall c tv r. OkRT c tv r => RType c tv r -> RType c tv r
noDummySyms RRType Reft
t1'


resultTy :: RType c tv r -> RType c tv r
resultTy :: forall c tv r. RType c tv r -> RType c tv r
resultTy = forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep

strengthenResult :: Reftable r => RType c tv r -> r -> RType c tv r
strengthenResult :: forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
strengthenResult RType c tv r
t r
r = forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep forall a b. (a -> b) -> a -> b
$ RTypeRep c tv r
rep {ty_res :: RType c tv r
ty_res = forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep c tv r
rep forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` r
r}
  where
    rep :: RTypeRep c tv r
rep              = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep RType c tv r
t


noDummySyms :: (OkRT c tv r) => RType c tv r -> RType c tv r
noDummySyms :: forall c tv r. OkRT c tv r => RType c tv r -> RType c tv r
noDummySyms RType c tv r
t
  | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. Symbolic a => a -> Bool
isDummy (forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep c tv r
rep)
  = forall a. Subable a => Subst -> a -> a
subst Subst
su forall a b. (a -> b) -> a -> b
$ forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep forall a b. (a -> b) -> a -> b
$ RTypeRep c tv r
rep{ty_binds :: [Symbol]
ty_binds = [Symbol]
xs'}
  | Bool
otherwise
  = RType c tv r
t
  where
    rep :: RTypeRep c tv r
rep = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep RType c tv r
t
    xs' :: [Symbol]
xs' = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Symbol
_ Int
i -> forall a. Symbolic a => a -> Symbol
symbol ([Char]
"x" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
i)) (forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep c tv r
rep) [(Int
1::Int)..]
    su :: Subst
su  = [(Symbol, Expr)] -> Subst
mkSubst forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep c tv r
rep) (Symbol -> Expr
EVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs')

combineDCTypes :: String -> Type -> [RRType Reft] -> RRType Reft
combineDCTypes :: [Char] -> Type -> [RRType Reft] -> RRType Reft
combineDCTypes [Char]
_msg Type
t [RRType Reft]
ts = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
RType c tv r -> RType c tv r -> RType c tv r
strengthenRefTypeGen (forall r. Monoid r => Type -> RRType r
ofType Type
t) [RRType Reft]
ts

mapArgumens :: Bool -> SourcePos -> RRType Reft -> RRType Reft -> Maybe Subst
mapArgumens :: Bool -> SourcePos -> RRType Reft -> RRType Reft -> Maybe Subst
mapArgumens Bool
allowTC SourcePos
lc RRType Reft
t1 RRType Reft
t2 = forall {t :: * -> *} {t :: * -> *} {a} {a}.
(Foldable t, Foldable t) =>
t a -> t a -> Maybe Subst
go [(Symbol, RRType Reft)]
xts1' [(Symbol, RRType Reft)]
xts2'
  where
    xts1 :: [(Symbol, RRType Reft)]
xts1 = forall a b. [a] -> [b] -> [(a, b)]
zip (forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar Reft
rep1) (forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar Reft
rep1)
    xts2 :: [(Symbol, RRType Reft)]
xts2 = forall a b. [a] -> [b] -> [(a, b)]
zip (forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar Reft
rep2) (forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar Reft
rep2)
    rep1 :: RTypeRep RTyCon RTyVar Reft
rep1 = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep RRType Reft
t1
    rep2 :: RTypeRep RTyCon RTyVar Reft
rep2 = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep RRType Reft
t2

    xts1' :: [(Symbol, RRType Reft)]
xts1' = forall a. (a -> Bool) -> [a] -> [a]
dropWhile forall {c} {a} {t} {t1}. TyConable c => (a, RType c t t1) -> Bool
canDrop [(Symbol, RRType Reft)]
xts1
    xts2' :: [(Symbol, RRType Reft)]
xts2' = forall a. (a -> Bool) -> [a] -> [a]
dropWhile forall {c} {a} {t} {t1}. TyConable c => (a, RType c t t1) -> Bool
canDrop [(Symbol, RRType Reft)]
xts2

    canDrop :: (a, RType c t t1) -> Bool
canDrop (a
_, RType c t t1
t) = if Bool
allowTC then forall c t t1. TyConable c => RType c t t1 -> Bool
isEmbeddedClass RType c t t1
t else forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType RType c t t1
t Bool -> Bool -> Bool
|| forall c t t1. TyConable c => RType c t t1 -> Bool
isEqType RType c t t1
t

    go :: t a -> t a -> Maybe Subst
go t a
xs t a
ys
      | forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
xs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
ys Bool -> Bool -> Bool
&& forall (t :: * -> *). Foldable t => t Bool -> Bool
and (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a. Eq a => a -> a -> Bool
(==) (forall c tv r. RType c tv r -> RType c tv ()
toRSort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RRType Reft)]
xts1') (forall c tv r. RType c tv r -> RType c tv ()
toRSort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RRType Reft)]
xts2'))
      = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [(Symbol, Expr)] -> Subst
mkSubst forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(Symbol, RRType Reft)
y (Symbol, RRType Reft)
x -> (forall a b. (a, b) -> a
fst (Symbol, RRType Reft)
x, Symbol -> Expr
EVar forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst (Symbol, RRType Reft)
y)) [(Symbol, RRType Reft)]
xts1' [(Symbol, RRType Reft)]
xts2'
      | Bool
otherwise
      = forall a. Maybe SrcSpan -> [Char] -> a
panic (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ SourcePos -> SrcSpan
sourcePosSrcSpan SourcePos
lc) ([Char]
"The types for the wrapper and worker data constructors cannot be merged\n"
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show RRType Reft
t1 forall a. [a] -> [a] -> [a]
++ [Char]
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show RRType Reft
t2 )

-- should constructors have implicits? probably not
defRefType :: Bool -> Type -> Def (RRType Reft) DataCon -> RRType Reft
defRefType :: Bool -> Type -> Def (RRType Reft) DataCon -> RRType Reft
defRefType Bool
allowTC Type
tdc (Def LocSymbol
f DataCon
dc Maybe (RRType Reft)
mt [(Symbol, Maybe (RRType Reft))]
xs Body
body)
                    = forall tv r c. (Eq tv, Monoid r) => RType c tv r -> RType c tv r
generalize forall a b. (a -> b) -> a -> b
$ forall tv c r.
[(RTVar tv (RType c tv ()), r)]
-> [PVar (RType c tv ())]
-> [(Symbol, RFInfo, RType c tv r, r)]
-> RType c tv r
-> RType c tv r
mkArrow forall {s}. [(RTVar RTyVar s, Reft)]
as' [] [(Symbol, RFInfo, RRType Reft, Reft)]
xts RRType Reft
t'
  where
    xts :: [(Symbol, RFInfo, RRType Reft, Reft)]
xts             = forall t1 a.
(Monoid t1, PPrint a) =>
Bool
-> SrcSpan
-> a
-> [(Symbol, Maybe (RRType Reft))]
-> [Type]
-> [(Symbol, RFInfo, RRType Reft, t1)]
stitchArgs Bool
allowTC (forall a. Loc a => a -> SrcSpan
fSrcSpan LocSymbol
f) DataCon
dc [(Symbol, Maybe (RRType Reft))]
xs [Type]
ts
    t' :: RRType Reft
t'              = forall a c tv.
Outputable a =>
a -> LocSymbol -> Body -> RType c tv Reft -> RType c tv Reft
refineWithCtorBody DataCon
dc LocSymbol
f Body
body RRType Reft
t
    t :: RRType Reft
t               = forall a. a -> Maybe a -> a
Mb.fromMaybe (forall r. Monoid r => Type -> RRType r
ofType Type
tr) Maybe (RRType Reft)
mt
    ([Var]
αs, [Type]
ts, Type
tr)    = Type -> ([Var], [Type], Type)
splitType Type
tdc
    as :: [RTVar RTyVar s]
as              = if forall a. Maybe a -> Bool
Mb.isJust Maybe (RRType Reft)
mt then [] else forall tv s. tv -> RTVar tv s
makeRTVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> RTyVar
rTyVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
αs
    as' :: [(RTVar RTyVar s, Reft)]
as'             = forall a b. (a -> b) -> [a] -> [b]
map (, forall a. Monoid a => a
mempty) forall {s}. [RTVar RTyVar s]
as

splitType :: Type -> ([TyVar],[Type], Type)
splitType :: Type -> ([Var], [Type], Type)
splitType Type
t  = ([Var]
αs, forall a b. (a -> b) -> [a] -> [b]
map forall a. Scaled a -> a
irrelevantMult [Scaled Type]
ts, Type
tr)
  where
    ([Var]
αs, Type
tb) = Type -> ([Var], Type)
splitForAllTyCoVars Type
t
    ([Scaled Type]
ts, Type
tr) = Type -> ([Scaled Type], Type)
splitFunTys Type
tb

stitchArgs :: (Monoid t1, PPrint a)
           => Bool
           -> SrcSpan
           -> a
           -> [(Symbol, Maybe (RRType Reft))]
           -> [Type]
           -> [(Symbol, RFInfo, RRType Reft, t1)]
stitchArgs :: forall t1 a.
(Monoid t1, PPrint a) =>
Bool
-> SrcSpan
-> a
-> [(Symbol, Maybe (RRType Reft))]
-> [Type]
-> [(Symbol, RFInfo, RRType Reft, t1)]
stitchArgs Bool
allowTC SrcSpan
sp a
dc [(Symbol, Maybe (RRType Reft))]
allXs [Type]
allTs
  | Int
nXs forall a. Eq a => a -> a -> Bool
== Int
nTs         = (forall {d} {a} {c}.
Monoid d =>
(a, Maybe c) -> c -> (a, RFInfo, c, d)
g (Symbol
dummySymbol, forall a. Maybe a
Nothing) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. Monoid r => Type -> RRType r
ofType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
pts)
                      forall a. [a] -> [a] -> [a]
++ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {d} {a} {c}.
Monoid d =>
(a, Maybe c) -> c -> (a, RFInfo, c, d)
g [(Symbol, Maybe (RRType Reft))]
xs (forall r. Monoid r => Type -> RRType r
ofType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts)
  | Bool
otherwise          = forall a a1 a3 a2.
(PPrint a, PPrint a1, PPrint a3) =>
SrcSpan -> a3 -> a1 -> a -> a2
panicFieldNumMismatch SrcSpan
sp a
dc Int
nXs Int
nTs
    where
      ([Type]
pts, [Type]
ts)        = forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (\Type
t -> forall a. PPrint a => [Char] -> a -> a
notracepp ([Char]
"isPredTy: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp Type
t) forall a b. (a -> b) -> a -> b
$ (if Bool
allowTC then Type -> Bool
isEmbeddedDictType else Type -> Bool
Ghc.isEvVarType ) Type
t) [Type]
allTs
      ([(Symbol, Maybe (RRType Reft))]
_  , [(Symbol, Maybe (RRType Reft))]
xs)        = forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (forall {r}.
(PPrint r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable r,
 Reftable (RTProp RTyCon RTyVar r)) =>
Maybe (RRType r) -> Bool
coArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Symbol, Maybe (RRType Reft))]
allXs
      nXs :: Int
nXs              = forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, Maybe (RRType Reft))]
xs
      nTs :: Int
nTs              = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts
      g :: (a, Maybe c) -> c -> (a, RFInfo, c, d)
g (a
x, Just c
t) c
_  = (a
x, Bool -> RFInfo
classRFInfo Bool
allowTC, c
t, forall a. Monoid a => a
mempty)
      g (a
x, Maybe c
_)      c
t  = (a
x, Bool -> RFInfo
classRFInfo Bool
allowTC, c
t, forall a. Monoid a => a
mempty)
      coArg :: Maybe (RRType r) -> Bool
coArg Maybe (RRType r)
Nothing    = Bool
False
      coArg (Just RRType r
t)   = (if Bool
allowTC then Type -> Bool
isEmbeddedDictType else Type -> Bool
Ghc.isEvVarType )forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False forall a b. (a -> b) -> a -> b
$ RRType r
t

panicFieldNumMismatch :: (PPrint a, PPrint a1, PPrint a3)
                      => SrcSpan -> a3 -> a1 -> a -> a2
panicFieldNumMismatch :: forall a a1 a3 a2.
(PPrint a, PPrint a1, PPrint a3) =>
SrcSpan -> a3 -> a1 -> a -> a2
panicFieldNumMismatch SrcSpan
sp a3
dc a1
nXs a
nTs  = forall a1 a. PPrint a1 => SrcSpan -> a1 -> Doc -> a
panicDataCon SrcSpan
sp a3
dc Doc
msg
  where
    msg :: Doc
msg = Doc
"Requires" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint a
nTs Doc -> Doc -> Doc
<+> Doc
"fields but given" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint a1
nXs

panicDataCon :: PPrint a1 => SrcSpan -> a1 -> Doc -> a
panicDataCon :: forall a1 a. PPrint a1 => SrcSpan -> a1 -> Doc -> a
panicDataCon SrcSpan
sp a1
dc Doc
d
  = forall a. Error -> a
panicError forall a b. (a -> b) -> a -> b
$ forall t. SrcSpan -> Doc -> Doc -> TError t
ErrDataCon SrcSpan
sp (forall a. PPrint a => a -> Doc
pprint a1
dc) Doc
d

refineWithCtorBody :: Outputable a
                   => a
                   -> LocSymbol
                   -> Body
                   -> RType c tv Reft
                   -> RType c tv Reft
refineWithCtorBody :: forall a c tv.
Outputable a =>
a -> LocSymbol -> Body -> RType c tv Reft -> RType c tv Reft
refineWithCtorBody a
dc LocSymbol
f Body
body RType c tv Reft
t =
  case forall c tv r. RType c tv r -> Maybe r
stripRTypeBase RType c tv Reft
t of
    Just (Reft (Symbol
v, Expr
_)) ->
      forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
strengthen RType c tv Reft
t forall a b. (a -> b) -> a -> b
$ (Symbol, Expr) -> Reft
Reft (Symbol
v, Expr -> Body -> Expr
bodyPred (LocSymbol -> [Expr] -> Expr
mkEApp LocSymbol
f [forall a. Symbolic a => a -> Expr
eVar Symbol
v]) Body
body)
    Maybe Reft
Nothing ->
      forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ [Char]
"measure mismatch " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp LocSymbol
f forall a. [a] -> [a] -> [a]
++ [Char]
" on con " forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
showPpr a
dc


bodyPred ::  Expr -> Body -> Expr
bodyPred :: Expr -> Body -> Expr
bodyPred Expr
fv (E Expr
e)    = Brel -> Expr -> Expr -> Expr
PAtom Brel
Eq Expr
fv Expr
e
bodyPred Expr
fv (P Expr
p)    = Expr -> Expr -> Expr
PIff  Expr
fv Expr
p
bodyPred Expr
fv (R Symbol
v' Expr
p) = forall a. Subable a => a -> (Symbol, Expr) -> a
subst1 Expr
p (Symbol
v', Expr
fv)