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

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

  -- * Type Aliases
  , BareSpec
  , BareMeasure
  , SpecMeasure

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

import           DataCon
import           GHC                                    hiding (Located)
import           Outputable                             (Outputable)
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           Language.Haskell.Liquid.GHC.API        as Ghc hiding (Expr)
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 :: LocSymbol
-> ty
-> [Def ty bndr]
-> MeasureKind
-> UnSortedExprs
-> Measure ty bndr
mkM LocSymbol
name ty
typ [Def ty bndr]
eqns MeasureKind
kind UnSortedExprs
u
  | (Def ty bndr -> Bool) -> [Def ty bndr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((LocSymbol
name LocSymbol -> LocSymbol -> Bool
forall a. Eq a => a -> a -> Bool
==) (LocSymbol -> Bool)
-> (Def ty bndr -> LocSymbol) -> Def ty bndr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Def ty bndr -> LocSymbol
forall ty ctor. Def ty ctor -> LocSymbol
measure) [Def ty bndr]
eqns
  = LocSymbol
-> ty
-> [Def ty bndr]
-> MeasureKind
-> UnSortedExprs
-> Measure ty bndr
forall ty ctor.
LocSymbol
-> ty
-> [Def ty ctor]
-> MeasureKind
-> UnSortedExprs
-> Measure ty ctor
M LocSymbol
name ty
typ [Def ty bndr]
eqns MeasureKind
kind UnSortedExprs
u
  | Bool
otherwise
  = Maybe SrcSpan -> String -> Measure ty bndr
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (String -> Measure ty bndr) -> String -> Measure ty bndr
forall a b. (a -> b) -> a -> b
$ String
"invalid measure definition for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LocSymbol -> String
forall a. Show a => a -> String
show LocSymbol
name

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


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


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

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

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

    wrRType :: RRType Reft
wrRType  = String -> Type -> [RRType Reft] -> RRType Reft
combineDCTypes String
"cdc1" Type
wrt [RRType Reft]
wrts
    woRType :: RRType Reft
woRType  = String -> Type -> [RRType Reft] -> RRType Reft
combineDCTypes String
"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
      | (Maybe ty -> Bool) -> [Maybe ty] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Maybe ty -> Bool
forall a. Maybe a -> Bool
Mb.isNothing ((Symbol, Maybe ty) -> Maybe ty
forall a b. (a, b) -> b
snd ((Symbol, Maybe ty) -> Maybe ty)
-> [(Symbol, Maybe ty)] -> [Maybe ty]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Def ty ctor -> [(Symbol, Maybe ty)]
forall ty ctor. Def ty ctor -> [(Symbol, Maybe ty)]
binds Def ty ctor
def)
      = Bool
True
      | Bool
otherwise
      = [(Symbol, Maybe ty)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Def ty ctor -> [(Symbol, Maybe ty)]
forall ty ctor. Def ty ctor -> [(Symbol, Maybe ty)]
binds Def ty ctor
def) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (([Type], Type) -> [Type]
forall a b. (a, b) -> a
fst (([Type], Type) -> [Type]) -> ([Type], Type) -> [Type]
forall a b. (a -> b) -> a -> b
$ Type -> ([Type], Type)
splitFunTys (Type -> ([Type], Type)) -> Type -> ([Type], Type)
forall a b. (a -> b) -> a -> b
$ ([Var], Type) -> Type
forall a b. (a, b) -> b
snd (([Var], Type) -> Type) -> ([Var], Type) -> Type
forall a b. (a -> b) -> a -> b
$ Type -> ([Var], Type)
splitForAllTys Type
wot)


extend :: SourcePos
       -> RType RTyCon RTyVar Reft
       -> RRType Reft
       -> RType RTyCon RTyVar Reft
extend :: SourcePos -> RRType Reft -> RRType Reft -> RRType Reft
extend SourcePos
lc RRType Reft
t1' RRType Reft
t2
  | Just Subst
su <- SourcePos -> RRType Reft -> RRType Reft -> Maybe Subst
mapArgumens SourcePos
lc RRType Reft
t1 RRType Reft
t2
  = RRType Reft
t1 RRType Reft -> Reft -> RRType Reft
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthenResult` Subst -> Reft -> Reft
forall a. Subable a => Subst -> a -> a
subst Subst
su (Reft -> Maybe Reft -> Reft
forall a. a -> Maybe a -> a
Mb.fromMaybe Reft
forall a. Monoid a => a
mempty (RRType Reft -> Maybe Reft
forall c tv r. RType c tv r -> Maybe r
stripRTypeBase (RRType Reft -> Maybe Reft) -> RRType Reft -> Maybe Reft
forall a b. (a -> b) -> a -> b
$ RRType Reft -> RRType Reft
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 = RRType Reft -> RRType Reft
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 :: RType c tv r -> RType c tv r
resultTy = RTypeRep c tv r -> RType c tv r
forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res (RTypeRep c tv r -> RType c tv r)
-> (RType c tv r -> RTypeRep c tv r)
-> RType c tv r
-> RType c tv r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType c tv r -> RTypeRep c tv r
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 :: RType c tv r -> r -> RType c tv r
strengthenResult RType c tv r
t r
r = RTypeRep c tv r -> RType c tv r
forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep (RTypeRep c tv r -> RType c tv r)
-> RTypeRep c tv r -> RType c tv r
forall a b. (a -> b) -> a -> b
$ RTypeRep c tv r
rep {ty_res :: RType c tv r
ty_res = RTypeRep c tv r -> RType c tv r
forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep c tv r
rep RType c tv r -> r -> RType c tv r
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              = RType c tv r -> RTypeRep c tv r
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 :: RType c tv r -> RType c tv r
noDummySyms RType c tv r
t
  | (Symbol -> Bool) -> [Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Symbol -> Bool
forall a. Symbolic a => a -> Bool
isDummy (RTypeRep c tv r -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep c tv r
rep)
  = Subst -> RType c tv r -> RType c tv r
forall a. Subable a => Subst -> a -> a
subst Subst
su (RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall a b. (a -> b) -> a -> b
$ RTypeRep c tv r -> RType c tv r
forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep (RTypeRep c tv r -> RType c tv r)
-> RTypeRep c tv r -> RType c tv r
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 = RType c tv r -> RTypeRep c tv r
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep RType c tv r
t
    xs' :: [Symbol]
xs' = (Symbol -> Integer -> Symbol) -> [Symbol] -> [Integer] -> [Symbol]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Symbol
_ Integer
i -> String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i)) (RTypeRep c tv r -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep c tv r
rep) [Integer
1..]
    su :: Subst
su  = [(Symbol, Expr)] -> Subst
mkSubst ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTypeRep c tv r -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep c tv r
rep) (Symbol -> Expr
EVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs')

combineDCTypes :: String -> Type -> [RRType Reft] -> RRType Reft
combineDCTypes :: String -> Type -> [RRType Reft] -> RRType Reft
combineDCTypes String
_msg Type
t [RRType Reft]
ts = (RRType Reft -> RRType Reft -> RRType Reft)
-> RRType Reft -> [RRType Reft] -> RRType Reft
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' RRType Reft -> RRType Reft -> RRType Reft
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 (Type -> RRType Reft
forall r. Monoid r => Type -> RRType r
ofType Type
t) [RRType Reft]
ts

mapArgumens :: SourcePos -> RRType Reft -> RRType Reft -> Maybe Subst
mapArgumens :: SourcePos -> RRType Reft -> RRType Reft -> Maybe Subst
mapArgumens SourcePos
lc RRType Reft
t1 RRType Reft
t2 = [(Symbol, RRType Reft)] -> [(Symbol, RRType Reft)] -> Maybe Subst
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 = [Symbol] -> [RRType Reft] -> [(Symbol, RRType Reft)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTypeRep RTyCon RTyVar Reft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar Reft
rep1) (RTypeRep RTyCon RTyVar Reft -> [RRType Reft]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar Reft
rep1)
    xts2 :: [(Symbol, RRType Reft)]
xts2 = [Symbol] -> [RRType Reft] -> [(Symbol, RRType Reft)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTypeRep RTyCon RTyVar Reft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar Reft
rep2) (RTypeRep RTyCon RTyVar Reft -> [RRType Reft]
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 = RRType Reft -> RTypeRep RTyCon RTyVar Reft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep RRType Reft
t1
    rep2 :: RTypeRep RTyCon RTyVar Reft
rep2 = RRType Reft -> RTypeRep RTyCon RTyVar Reft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep RRType Reft
t2

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

-- should constructors have implicits? probably not
defRefType :: Type -> Def (RRType Reft) DataCon -> RRType Reft
defRefType :: Type -> Def (RRType Reft) DataCon -> RRType Reft
defRefType Type
tdc (Def LocSymbol
f DataCon
dc Maybe (RRType Reft)
mt [(Symbol, Maybe (RRType Reft))]
xs Body
body)
                    = RRType Reft -> RRType Reft
forall tv r c. (Eq tv, Monoid r) => RType c tv r -> RType c tv r
generalize (RRType Reft -> RRType Reft) -> RRType Reft -> RRType Reft
forall a b. (a -> b) -> a -> b
$ [(RTVar RTyVar (RType RTyCon RTyVar ()), Reft)]
-> [PVar (RType RTyCon RTyVar ())]
-> [(Symbol, RRType Reft, Reft)]
-> [(Symbol, RRType Reft, Reft)]
-> RRType Reft
-> RRType Reft
forall tv c r.
[(RTVar tv (RType c tv ()), r)]
-> [PVar (RType c tv ())]
-> [(Symbol, RType c tv r, r)]
-> [(Symbol, RType c tv r, r)]
-> RType c tv r
-> RType c tv r
mkArrow [(RTVar RTyVar (RType RTyCon RTyVar ()), Reft)]
forall s. [(RTVar RTyVar s, Reft)]
as' [] [] [(Symbol, RRType Reft, Reft)]
xts RRType Reft
t'
  where
    xts :: [(Symbol, RRType Reft, Reft)]
xts             = SrcSpan
-> DataCon
-> [(Symbol, Maybe (RRType Reft))]
-> [Type]
-> [(Symbol, RRType Reft, Reft)]
forall t1 a.
(Monoid t1, PPrint a) =>
SrcSpan
-> a
-> [(Symbol, Maybe (RRType Reft))]
-> [Type]
-> [(Symbol, RRType Reft, t1)]
stitchArgs (LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
fSrcSpan LocSymbol
f) DataCon
dc [(Symbol, Maybe (RRType Reft))]
xs [Type]
ts 
    t' :: RRType Reft
t'              = DataCon -> LocSymbol -> Body -> RRType Reft -> RRType Reft
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               = RRType Reft -> Maybe (RRType Reft) -> RRType Reft
forall a. a -> Maybe a -> a
Mb.fromMaybe (Type -> RRType Reft
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 Maybe (RRType Reft) -> Bool
forall a. Maybe a -> Bool
Mb.isJust Maybe (RRType Reft)
mt then [] else RTyVar -> RTVar RTyVar s
forall tv s. tv -> RTVar tv s
makeRTVar (RTyVar -> RTVar RTyVar s)
-> (Var -> RTyVar) -> Var -> RTVar RTyVar s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> RTyVar
rTyVar (Var -> RTVar RTyVar s) -> [Var] -> [RTVar RTyVar s]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
αs
    as' :: [(RTVar RTyVar s, Reft)]
as'             = [RTVar RTyVar s] -> [Reft] -> [(RTVar RTyVar s, Reft)]
forall a b. [a] -> [b] -> [(a, b)]
zip [RTVar RTyVar s]
forall s. [RTVar RTyVar s]
as (Reft -> [Reft]
forall a. a -> [a]
repeat Reft
forall a. Monoid a => a
mempty)

splitType :: Type -> ([TyVar],[Type], Type)
splitType :: Type -> ([Var], [Type], Type)
splitType Type
t  = ([Var]
αs, [Type]
ts, Type
tr)
  where
    ([Var]
αs, Type
tb) = Type -> ([Var], Type)
splitForAllTys Type
t
    ([Type]
ts, Type
tr) = Type -> ([Type], Type)
splitFunTys Type
tb

stitchArgs :: (Monoid t1, PPrint a)
           => SrcSpan
           -> a
           -> [(Symbol, Maybe (RRType Reft))]
           -> [Type]
           -> [(Symbol, RRType Reft, t1)]
stitchArgs :: SrcSpan
-> a
-> [(Symbol, Maybe (RRType Reft))]
-> [Type]
-> [(Symbol, RRType Reft, t1)]
stitchArgs SrcSpan
sp a
dc [(Symbol, Maybe (RRType Reft))]
allXs [Type]
allTs
  | Int
nXs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
nTs         = ((Symbol, Maybe (RRType Reft))
-> RRType Reft -> (Symbol, RRType Reft, t1)
forall c a b. Monoid c => (a, Maybe b) -> b -> (a, b, c)
g (Symbol
dummySymbol, Maybe (RRType Reft)
forall a. Maybe a
Nothing) (RRType Reft -> (Symbol, RRType Reft, t1))
-> (Type -> RRType Reft) -> Type -> (Symbol, RRType Reft, t1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> RRType Reft
forall r. Monoid r => Type -> RRType r
ofType (Type -> (Symbol, RRType Reft, t1))
-> [Type] -> [(Symbol, RRType Reft, t1)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
pts)
                      [(Symbol, RRType Reft, t1)]
-> [(Symbol, RRType Reft, t1)] -> [(Symbol, RRType Reft, t1)]
forall a. [a] -> [a] -> [a]
++ ((Symbol, Maybe (RRType Reft))
 -> RRType Reft -> (Symbol, RRType Reft, t1))
-> [(Symbol, Maybe (RRType Reft))]
-> [RRType Reft]
-> [(Symbol, RRType Reft, t1)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Symbol, Maybe (RRType Reft))
-> RRType Reft -> (Symbol, RRType Reft, t1)
forall c a b. Monoid c => (a, Maybe b) -> b -> (a, b, c)
g [(Symbol, Maybe (RRType Reft))]
xs (Type -> RRType Reft
forall r. Monoid r => Type -> RRType r
ofType (Type -> RRType Reft) -> [Type] -> [RRType Reft]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts)
  | Bool
otherwise          = SrcSpan -> a -> Int -> Int -> [(Symbol, RRType Reft, t1)]
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)        = (Type -> Bool) -> [Type] -> ([Type], [Type])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (\Type
t -> String -> Bool -> Bool
forall a. PPrint a => String -> a -> a
notracepp (String
"isPredTy: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. PPrint a => a -> String
showpp Type
t) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Type -> Bool
Ghc.isEvVarType Type
t) [Type]
allTs
      ([(Symbol, Maybe (RRType Reft))]
_  , [(Symbol, Maybe (RRType Reft))]
xs)        = ((Symbol, Maybe (RRType Reft)) -> Bool)
-> [(Symbol, Maybe (RRType Reft))]
-> ([(Symbol, Maybe (RRType Reft))],
    [(Symbol, Maybe (RRType Reft))])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (Maybe (RRType Reft) -> Bool
forall r.
(PPrint r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable r,
 Reftable (RTProp RTyCon RTyVar r)) =>
Maybe (RRType r) -> Bool
coArg (Maybe (RRType Reft) -> Bool)
-> ((Symbol, Maybe (RRType Reft)) -> Maybe (RRType Reft))
-> (Symbol, Maybe (RRType Reft))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Maybe (RRType Reft)) -> Maybe (RRType Reft)
forall a b. (a, b) -> b
snd) [(Symbol, Maybe (RRType Reft))]
allXs
      nXs :: Int
nXs              = [(Symbol, Maybe (RRType Reft))] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, Maybe (RRType Reft))]
xs
      nTs :: Int
nTs              = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts
      g :: (a, Maybe b) -> b -> (a, b, c)
g (a
x, Just b
t) b
_  = (a
x, b
t, c
forall a. Monoid a => a
mempty)
      g (a
x, Maybe b
_)      b
t  = (a
x, b
t, c
forall a. Monoid a => a
mempty)
      coArg :: Maybe (RRType r) -> Bool
coArg Maybe (RRType r)
Nothing    = Bool
False
      coArg (Just RRType r
t)   = Type -> Bool
Ghc.isEvVarType (Type -> Bool) -> (RRType r -> Type) -> RRType r -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RRType r -> Type
forall r. ToTypeable r => RRType r -> Type
toType (RRType r -> Bool) -> RRType r -> Bool
forall a b. (a -> b) -> a -> b
$ RRType r
t

panicFieldNumMismatch :: (PPrint a, PPrint a1, PPrint a3)
                      => SrcSpan -> a3 -> a1 -> a -> a2
panicFieldNumMismatch :: SrcSpan -> a3 -> a1 -> a -> a2
panicFieldNumMismatch SrcSpan
sp a3
dc a1
nXs a
nTs  = SrcSpan -> a3 -> Doc -> a2
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
<+> a -> Doc
forall a. PPrint a => a -> Doc
pprint a
nTs Doc -> Doc -> Doc
<+> Doc
"fields but given" Doc -> Doc -> Doc
<+> a1 -> Doc
forall a. PPrint a => a -> Doc
pprint a1
nXs

panicDataCon :: PPrint a1 => SrcSpan -> a1 -> Doc -> a
panicDataCon :: SrcSpan -> a1 -> Doc -> a
panicDataCon SrcSpan
sp a1
dc Doc
d
  = Error -> a
forall a. Error -> a
panicError (Error -> a) -> Error -> a
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Doc -> Error
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrDataCon SrcSpan
sp (a1 -> Doc
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 :: a -> LocSymbol -> Body -> RType c tv Reft -> RType c tv Reft
refineWithCtorBody a
dc LocSymbol
f Body
body RType c tv Reft
t =
  case RType c tv Reft -> Maybe Reft
forall c tv r. RType c tv r -> Maybe r
stripRTypeBase RType c tv Reft
t of
    Just (Reft (Symbol
v, Expr
_)) ->
      RType c tv Reft -> Reft -> RType c tv Reft
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
strengthen RType c tv Reft
t (Reft -> RType c tv Reft) -> Reft -> RType c tv Reft
forall a b. (a -> b) -> a -> b
$ (Symbol, Expr) -> Reft
Reft (Symbol
v, Expr -> Body -> Expr
bodyPred (LocSymbol -> [Expr] -> Expr
mkEApp LocSymbol
f [Symbol -> Expr
forall a. Symbolic a => a -> Expr
eVar Symbol
v]) Body
body)
    Maybe Reft
Nothing ->
      Maybe SrcSpan -> String -> RType c tv Reft
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (String -> RType c tv Reft) -> String -> RType c tv Reft
forall a b. (a -> b) -> a -> b
$ String
"measure mismatch " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LocSymbol -> String
forall a. PPrint a => a -> String
showpp LocSymbol
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" on con " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Outputable a => a -> String
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) = Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
subst1 Expr
p (Symbol
v', Expr
fv)