{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE UndecidableInstances   #-}
{-# LANGUAGE OverloadedStrings      #-}
{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE TupleSections    #-}
{-# OPTIONS_GHC -Wno-x-partial #-}

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 GHC.Stack

import           Language.Fixpoint.Misc
import           Language.Fixpoint.Types                as F hiding (panic, R, DataDecl, SrcSpan, LocSymbol)
import           Liquid.GHC.API        as Ghc hiding (Expr, showPpr, panic, (<+>))
import           Language.Haskell.Liquid.GHC.Misc
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.Names
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.Types
import           Language.Haskell.Liquid.Types.RefType
-- import           Language.Haskell.Liquid.Types.Variance
-- import           Language.Haskell.Liquid.Types.Bounds
import           Language.Haskell.Liquid.Types.Specs
import           Language.Haskell.Liquid.UX.Tidy


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

mkMSpec' :: [Measure ty DataCon] -> MSpec ty DataCon
mkMSpec' :: forall ty. [Measure ty DataCon] -> MSpec ty DataCon
mkMSpec' [Measure ty DataCon]
ms = HashMap LHName [Def ty DataCon]
-> HashMap (Located LHName) (Measure ty DataCon)
-> HashMap (Located LHName) (Measure ty ())
-> [Measure ty DataCon]
-> MSpec ty DataCon
forall ty ctor.
HashMap LHName [Def ty ctor]
-> HashMap (Located LHName) (Measure ty ctor)
-> HashMap (Located LHName) (Measure ty ())
-> [Measure ty ctor]
-> MSpec ty ctor
MSpec HashMap LHName [Def ty DataCon]
cm HashMap (Located LHName) (Measure ty DataCon)
mm HashMap (Located LHName) (Measure ty ())
forall k v. HashMap k v
M.empty []
  where
    cm :: HashMap LHName [Def ty DataCon]
cm     = (Def ty DataCon -> LHName)
-> [Def ty DataCon] -> HashMap LHName [Def ty DataCon]
forall k a. (Eq k, Hashable k) => (a -> k) -> [a] -> HashMap k [a]
groupMap (Var -> LHName
makeGHCLHNameFromId (Var -> LHName)
-> (Def ty DataCon -> Var) -> Def ty DataCon -> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> Var
dataConWorkId (DataCon -> Var)
-> (Def ty DataCon -> DataCon) -> Def ty DataCon -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Def ty DataCon -> DataCon
forall v ty ctor. DefV v ty ctor -> ctor
ctor) ([Def ty DataCon] -> HashMap LHName [Def ty DataCon])
-> [Def ty DataCon] -> HashMap LHName [Def ty DataCon]
forall a b. (a -> b) -> a -> b
$ (Measure ty DataCon -> [Def ty DataCon])
-> [Measure ty DataCon] -> [Def ty DataCon]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Measure ty DataCon -> [Def ty DataCon]
forall v ty ctor. MeasureV v ty ctor -> [DefV v ty ctor]
msEqns [Measure ty DataCon]
ms
    mm :: HashMap (Located LHName) (Measure ty DataCon)
mm     = [(Located LHName, Measure ty DataCon)]
-> HashMap (Located LHName) (Measure ty DataCon)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Measure ty DataCon -> Located LHName
forall v ty ctor. MeasureV v ty ctor -> Located LHName
msName Measure ty DataCon
m, Measure ty DataCon
m) | Measure ty DataCon
m <- [Measure ty DataCon]
ms ]

-- Note [Duplicate measures and opaque reflection]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--
-- Note that only ms are checked for duplicates! `oms` are the opaque reflections, they are automatically generated
-- so we don't care about duplicates (any two opaque-reflection measures with the same name will refer to the same thing,
-- since their names are fully qualified). Whence the need for a separate field for opaque reflections vs usual measures.
mkMSpec :: [Measure t (F.Located LHName)] -> [Measure t ()] -> [Measure t (F.Located LHName)] -> [Measure t (F.Located LHName)] -> MSpec t (F.Located LHName)
mkMSpec :: forall t.
[Measure t (Located LHName)]
-> [Measure t ()]
-> [Measure t (Located LHName)]
-> [Measure t (Located LHName)]
-> MSpec t (Located LHName)
mkMSpec [Measure t (Located LHName)]
ms [Measure t ()]
cms [Measure t (Located LHName)]
ims [Measure t (Located LHName)]
oms = HashMap LHName [Def t (Located LHName)]
-> HashMap (Located LHName) (Measure t (Located LHName))
-> HashMap (Located LHName) (Measure t ())
-> [Measure t (Located LHName)]
-> MSpec t (Located LHName)
forall ty ctor.
HashMap LHName [Def ty ctor]
-> HashMap (Located LHName) (Measure ty ctor)
-> HashMap (Located LHName) (Measure ty ())
-> [Measure ty ctor]
-> MSpec ty ctor
MSpec HashMap LHName [Def t (Located LHName)]
cm HashMap (Located LHName) (Measure t (Located LHName))
mm HashMap (Located LHName) (Measure t ())
cmm [Measure t (Located LHName)]
ims
  where
    cm :: HashMap LHName [Def t (Located LHName)]
cm     = (Def t (Located LHName) -> LHName)
-> [Def t (Located LHName)]
-> HashMap LHName [Def t (Located LHName)]
forall k a. (Eq k, Hashable k) => (a -> k) -> [a] -> HashMap k [a]
groupMap (Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> (Def t (Located LHName) -> Located LHName)
-> Def t (Located LHName)
-> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Def t (Located LHName) -> Located LHName
forall v ty ctor. DefV v ty ctor -> ctor
ctor) ([Def t (Located LHName)]
 -> HashMap LHName [Def t (Located LHName)])
-> [Def t (Located LHName)]
-> HashMap LHName [Def t (Located LHName)]
forall a b. (a -> b) -> a -> b
$ (Measure t (Located LHName) -> [Def t (Located LHName)])
-> [Measure t (Located LHName)] -> [Def t (Located LHName)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Measure t (Located LHName) -> [Def t (Located LHName)]
forall v ty ctor. MeasureV v ty ctor -> [DefV v ty ctor]
msEqns ([Measure t (Located LHName)]
ms'[Measure t (Located LHName)]
-> [Measure t (Located LHName)] -> [Measure t (Located LHName)]
forall a. [a] -> [a] -> [a]
++[Measure t (Located LHName)]
ims)
    mm :: HashMap (Located LHName) (Measure t (Located LHName))
mm     = [(Located LHName, Measure t (Located LHName))]
-> HashMap (Located LHName) (Measure t (Located LHName))
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Measure t (Located LHName) -> Located LHName
forall v ty ctor. MeasureV v ty ctor -> Located LHName
msName Measure t (Located LHName)
m, Measure t (Located LHName)
m) | Measure t (Located LHName)
m <- [Measure t (Located LHName)]
ms' ]
    cmm :: HashMap (Located LHName) (Measure t ())
cmm    = [(Located LHName, Measure t ())]
-> HashMap (Located LHName) (Measure t ())
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Measure t () -> Located LHName
forall v ty ctor. MeasureV v ty ctor -> Located LHName
msName Measure t ()
m, Measure t ()
m) | Measure t ()
m <- [Measure t ()]
cms ]
    ms' :: [Measure t (Located LHName)]
ms'    = [Measure t (Located LHName)] -> [Measure t (Located LHName)]
forall ty ctor. [Measure ty ctor] -> [Measure ty ctor]
checkDuplicateMeasure [Measure t (Located LHName)]
ms [Measure t (Located LHName)]
-> [Measure t (Located LHName)] -> [Measure t (Located LHName)]
forall a. [a] -> [a] -> [a]
++ [Measure t (Located LHName)]
oms


checkDuplicateMeasure :: [Measure ty ctor] -> [Measure ty ctor]
checkDuplicateMeasure :: forall ty ctor. [Measure ty ctor] -> [Measure ty ctor]
checkDuplicateMeasure [Measure ty ctor]
measures
  = case HashMap (Located LHName) [Measure ty ctor]
-> [(Located LHName, [Measure ty ctor])]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap (Located LHName) [Measure ty ctor]
dups of
      []         -> [Measure ty ctor]
measures
      (Located LHName
m,[Measure ty ctor]
ms):[(Located LHName, [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
$ Located LHName -> [Located LHName] -> UserError
forall {a} {a} {t}.
(PPrint a, Loc a) =>
Located a -> [a] -> TError t
mkError Located LHName
m (Measure ty ctor -> Located LHName
forall v ty ctor. MeasureV v ty ctor -> Located LHName
msName (Measure ty ctor -> Located LHName)
-> [Measure ty ctor] -> [Located LHName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Measure ty ctor]
ms)
    where
      gms :: HashMap (Located LHName) [Measure ty ctor]
gms        = [(Located LHName, Measure ty ctor)]
-> HashMap (Located LHName) [Measure ty ctor]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
group [(Measure ty ctor -> Located LHName
forall v ty ctor. MeasureV v ty ctor -> Located LHName
msName Measure ty ctor
m , Measure ty ctor
m) | Measure ty ctor
m <- [Measure ty ctor]
measures]
      dups :: HashMap (Located LHName) [Measure ty ctor]
dups       = ([Measure ty ctor] -> Bool)
-> HashMap (Located LHName) [Measure ty ctor]
-> HashMap (Located LHName) [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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length) HashMap (Located LHName) [Measure ty ctor]
gms
      mkError :: Located a -> [a] -> TError t
mkError 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 :: Bool -> MSpec (RRType Reft) DataCon -> ([(Var, RRType Reft)], [(F.Located LHName, RRType Reft)])
dataConTypes :: Bool
-> MSpec (RRType Reft) DataCon
-> ([(Var, RRType Reft)], [(Located LHName, RRType Reft)])
dataConTypes Bool
allowTC  MSpec (RRType Reft) DataCon
s = ([(Var, RRType Reft)]
ctorTys, [(Located LHName, RRType Reft)]
measTys)
  where
    measTys :: [(Located LHName, RRType Reft)]
measTys     = [(MeasureV Symbol (RRType Reft) DataCon -> Located LHName
forall v ty ctor. MeasureV v ty ctor -> Located LHName
msName MeasureV Symbol (RRType Reft) DataCon
m, MeasureV Symbol (RRType Reft) DataCon -> RRType Reft
forall v ty ctor. MeasureV v ty ctor -> ty
msSort MeasureV Symbol (RRType Reft) DataCon
m) | MeasureV Symbol (RRType Reft) DataCon
m <- HashMap (Located LHName) (MeasureV Symbol (RRType Reft) DataCon)
-> [MeasureV Symbol (RRType Reft) DataCon]
forall k v. HashMap k v -> [v]
M.elems (MSpec (RRType Reft) DataCon
-> HashMap (Located LHName) (MeasureV Symbol (RRType Reft) DataCon)
forall ty ctor.
MSpec ty ctor -> HashMap (Located LHName) (Measure ty ctor)
measMap MSpec (RRType Reft) DataCon
s) [MeasureV Symbol (RRType Reft) DataCon]
-> [MeasureV Symbol (RRType Reft) DataCon]
-> [MeasureV Symbol (RRType Reft) DataCon]
forall a. [a] -> [a] -> [a]
++ MSpec (RRType Reft) DataCon
-> [MeasureV Symbol (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 (Bool -> [Def (RRType Reft) DataCon] -> [(Var, RRType Reft)]
makeDataConType Bool
allowTC) ([Char]
-> [Def (RRType Reft) DataCon] -> [Def (RRType Reft) DataCon]
forall a. PPrint a => [Char] -> a -> a
notracepp [Char]
"HOHOH" ([Def (RRType Reft) DataCon] -> [Def (RRType Reft) DataCon])
-> ((LHName, [Def (RRType Reft) DataCon])
    -> [Def (RRType Reft) DataCon])
-> (LHName, [Def (RRType Reft) DataCon])
-> [Def (RRType Reft) DataCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LHName, [Def (RRType Reft) DataCon])
-> [Def (RRType Reft) DataCon]
forall a b. (a, b) -> b
snd ((LHName, [Def (RRType Reft) DataCon])
 -> [Def (RRType Reft) DataCon])
-> [(LHName, [Def (RRType Reft) DataCon])]
-> [[Def (RRType Reft) DataCon]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap LHName [Def (RRType Reft) DataCon]
-> [(LHName, [Def (RRType Reft) DataCon])]
forall k v. HashMap k v -> [(k, v)]
M.toList (MSpec (RRType Reft) DataCon
-> HashMap LHName [Def (RRType Reft) DataCon]
forall ty ctor. MSpec ty ctor -> HashMap LHName [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 | Maybe Var -> Bool
forall a. Maybe a -> Bool
Mb.isNothing (DataCon -> Maybe Var
dataConWrapId_maybe DataCon
dc)
  = [Char] -> [(Var, RRType Reft)] -> [(Var, RRType Reft)]
forall a. PPrint a => [Char] -> a -> a
notracepp [Char]
_msg [(Var
woId, [Char] -> RRType Reft -> RRType Reft
forall a. PPrint a => [Char] -> a -> a
notracepp [Char]
_msg (RRType Reft -> RRType Reft) -> RRType Reft -> RRType Reft
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   = Def (RRType Reft) DataCon -> DataCon
forall v ty ctor. DefV v ty ctor -> ctor
ctor ([Def (RRType Reft) DataCon] -> Def (RRType Reft) DataCon
forall a. HasCallStack => [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 (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 :: [Char]
_msg  = [Char]
"makeDataConType0" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Var, Type, [RRType Reft]) -> [Char]
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) = (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 {v} {ty} {ctor}. DefV v ty ctor -> Bool
isWorkerDef [Def (RRType Reft) DataCon]
ds
    dc :: DataCon
dc       = Def (RRType Reft) DataCon -> DataCon
forall v ty ctor. DefV v 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. HasCallStack => [a] -> a
head [Def (RRType Reft) DataCon]
ds
    loci :: SourcePos
loci     = Located LHName -> SourcePos
forall a. Located a -> SourcePos
loc (Located LHName -> SourcePos) -> Located LHName -> SourcePos
forall a b. (a -> b) -> a -> b
$ Def (RRType Reft) DataCon -> Located LHName
forall v ty ctor. DefV v ty ctor -> Located LHName
measure (Def (RRType Reft) DataCon -> Located LHName)
-> Def (RRType Reft) DataCon -> Located LHName
forall a b. (a -> b) -> a -> b
$ [Def (RRType Reft) DataCon] -> Def (RRType Reft) DataCon
forall a. HasCallStack => [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 (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     = Bool -> Type -> Def (RRType Reft) DataCon -> RRType Reft
defRefType Bool
allowTC 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  = [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 :: DefV v ty ctor -> Bool
isWorkerDef DefV v 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
<$> DefV v ty ctor -> [(Symbol, Maybe ty)]
forall v ty ctor. DefV v ty ctor -> [(Symbol, Maybe ty)]
binds DefV v ty ctor
def)
      = Bool
True
      | Bool
otherwise
      = [(Symbol, Maybe ty)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (DefV v ty ctor -> [(Symbol, Maybe ty)]
forall v ty ctor. DefV v ty ctor -> [(Symbol, Maybe ty)]
binds DefV v ty ctor
def) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Scaled Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (([Scaled Type], Type) -> [Scaled Type]
forall a b. (a, b) -> a
fst (([Scaled Type], Type) -> [Scaled Type])
-> ([Scaled Type], Type) -> [Scaled Type]
forall a b. (a -> b) -> a -> b
$ Type -> ([Scaled Type], Type)
splitFunTys (Type -> ([Scaled Type], Type)) -> Type -> ([Scaled 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)
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 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 :: forall c tv r. RType c tv r -> RType c tv r
resultTy = RTypeRepV Symbol c tv r -> RTypeV Symbol c tv r
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
ty_res (RTypeRepV Symbol c tv r -> RTypeV Symbol c tv r)
-> (RTypeV Symbol c tv r -> RTypeRepV Symbol c tv r)
-> RTypeV Symbol c tv r
-> RTypeV Symbol c tv r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeV Symbol c tv r -> RTypeRepV Symbol c tv r
forall v c tv r. RTypeV v c tv r -> RTypeRepV v 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 = RTypeRepV Symbol c tv r -> RType c tv r
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
fromRTypeRep (RTypeRepV Symbol c tv r -> RType c tv r)
-> RTypeRepV Symbol c tv r -> RType c tv r
forall a b. (a -> b) -> a -> b
$ RTypeRepV Symbol c tv r
rep {ty_res = ty_res rep `strengthen` r}
  where
    rep :: RTypeRepV Symbol c tv r
rep              = RType c tv r -> RTypeRepV Symbol c tv r
forall v c tv r. RTypeV v c tv r -> RTypeRepV v 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
  | (Symbol -> Bool) -> [Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Symbol -> Bool
forall a. Symbolic a => a -> Bool
isDummy (RTypeRepV Symbol c tv r -> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds RTypeRepV Symbol 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
$ RTypeRepV Symbol c tv r -> RType c tv r
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
fromRTypeRep (RTypeRepV Symbol c tv r -> RType c tv r)
-> RTypeRepV Symbol c tv r -> RType c tv r
forall a b. (a -> b) -> a -> b
$ RTypeRepV Symbol c tv r
rep{ty_binds = xs'}
  | Bool
otherwise
  = RType c tv r
t
  where
    rep :: RTypeRepV Symbol c tv r
rep = RType c tv r -> RTypeRepV Symbol c tv r
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep RType c tv r
t
    xs' :: [Symbol]
xs' = (Symbol -> Int -> Symbol) -> [Symbol] -> [Int] -> [Symbol]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Symbol
_ Int
i -> [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
symbol ([Char]
"x" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i)) (RTypeRepV Symbol c tv r -> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds RTypeRepV Symbol c tv r
rep) [(Int
1::Int)..]
    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 (RTypeRepV Symbol c tv r -> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds RTypeRepV Symbol c tv r
rep) (Symbol -> Expr
forall v. v -> ExprV v
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 :: [Char] -> Type -> [RRType Reft] -> RRType Reft
combineDCTypes [Char]
_msg Type
t [RRType Reft]
ts = (RRType Reft -> RRType Reft -> RRType Reft)
-> RRType Reft -> [RRType Reft] -> RRType Reft
forall b a. (b -> a -> b) -> b -> [a] -> b
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 :: 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 = [(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 (RTypeRepV Symbol RTyCon RTyVar Reft -> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds RTypeRepV Symbol RTyCon RTyVar Reft
rep1) (RTypeRepV Symbol RTyCon RTyVar Reft -> [RRType Reft]
forall v c tv r. RTypeRepV v c tv r -> [RTypeV v c tv r]
ty_args RTypeRepV Symbol RTyCon RTyVar Reft
rep1)
    xts2 :: [(Symbol, RRType Reft)]
xts2 = [Symbol] -> [RRType Reft] -> [(Symbol, RRType Reft)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTypeRepV Symbol RTyCon RTyVar Reft -> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds RTypeRepV Symbol RTyCon RTyVar Reft
rep2) (RTypeRepV Symbol RTyCon RTyVar Reft -> [RRType Reft]
forall v c tv r. RTypeRepV v c tv r -> [RTypeV v c tv r]
ty_args RTypeRepV Symbol RTyCon RTyVar Reft
rep2)
    rep1 :: RTypeRepV Symbol RTyCon RTyVar Reft
rep1 = RRType Reft -> RTypeRepV Symbol RTyCon RTyVar Reft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep RRType Reft
t1
    rep2 :: RTypeRepV Symbol RTyCon RTyVar Reft
rep2 = RRType Reft -> RTypeRepV Symbol RTyCon RTyVar Reft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v 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} {v} {t} {t1}.
TyConable c =>
(a, RTypeV v 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} {v} {t} {t1}.
TyConable c =>
(a, RTypeV v c t t1) -> Bool
canDrop [(Symbol, RRType Reft)]
xts2

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

    go :: t a -> t a -> Maybe Subst
go t a
xs t a
ys
      | t a -> Int
forall a. 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 a. 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 v c tv r. RTypeV v c tv r -> RTypeV v 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 v c tv r. RTypeV v c tv r -> RTypeV v 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
forall v. v -> ExprV v
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 -> [Char] -> Maybe Subst
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> 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) ([Char]
"The types for the wrapper and worker data constructors cannot be merged\n"
          [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RRType Reft -> [Char]
forall a. Show a => a -> [Char]
show RRType Reft
t1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RRType Reft -> [Char]
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 Located LHName
f DataCon
dc Maybe (RRType Reft)
mt [(Symbol, Maybe (RRType Reft))]
xs BodyV Symbol
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)]
-> [PVarV Symbol (RType RTyCon RTyVar ())]
-> [(Symbol, RFInfo, RRType Reft, Reft)]
-> RRType Reft
-> RRType Reft
forall tv v c r.
[(RTVar tv (RTypeV v c tv ()), r)]
-> [PVarV v (RTypeV v c tv ())]
-> [(Symbol, RFInfo, RTypeV v c tv r, r)]
-> RTypeV v c tv r
-> RTypeV v c tv r
mkArrow [(RTVar RTyVar (RType RTyCon RTyVar ()), Reft)]
forall {s}. [(RTVar RTyVar s, Reft)]
as' [] [(Symbol, RFInfo, RRType Reft, Reft)]
xts RRType Reft
t'
  where
    xts :: [(Symbol, RFInfo, RRType Reft, Reft)]
xts             = Bool
-> SrcSpan
-> DataCon
-> [(Symbol, Maybe (RRType Reft))]
-> [Type]
-> [(Symbol, RFInfo, RRType Reft, Reft)]
forall t1 a.
(Monoid t1, PPrint a) =>
Bool
-> SrcSpan
-> a
-> [(Symbol, Maybe (RRType Reft))]
-> [Type]
-> [(Symbol, RFInfo, RRType Reft, t1)]
stitchArgs Bool
allowTC (Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
fSrcSpan Located LHName
f) DataCon
dc [(Symbol, Maybe (RRType Reft))]
xs [Type]
ts
    t' :: RRType Reft
t'              = DataCon
-> Located LHName -> BodyV Symbol -> RRType Reft -> RRType Reft
forall a c tv.
Outputable a =>
a
-> Located LHName
-> BodyV Symbol
-> RType c tv Reft
-> RType c tv Reft
refineWithCtorBody DataCon
dc Located LHName
f BodyV Symbol
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 -> (RTVar RTyVar s, Reft))
-> [RTVar RTyVar s] -> [(RTVar RTyVar s, Reft)]
forall a b. (a -> b) -> [a] -> [b]
map (, Reft
forall a. Monoid a => a
mempty) [RTVar RTyVar s]
forall {s}. [RTVar RTyVar s]
as

splitType :: Type -> ([TyVar],[Type], Type)
splitType :: Type -> ([Var], [Type], Type)
splitType Type
t  = ([Var]
αs, (Scaled Type -> Type) -> [Scaled Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
nTs         = ((Symbol, Maybe (RRType Reft))
-> RRType Reft -> (Symbol, RFInfo, RRType Reft, t1)
forall {d} {a} {c}.
Monoid d =>
(a, Maybe c) -> c -> (a, RFInfo, c, d)
g (Symbol
dummySymbol, Maybe (RRType Reft)
forall a. Maybe a
Nothing) (RRType Reft -> (Symbol, RFInfo, RRType Reft, t1))
-> (Type -> RRType Reft)
-> Type
-> (Symbol, RFInfo, 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, RFInfo, RRType Reft, t1))
-> [Type] -> [(Symbol, RFInfo, RRType Reft, t1)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
pts)
                      [(Symbol, RFInfo, RRType Reft, t1)]
-> [(Symbol, RFInfo, RRType Reft, t1)]
-> [(Symbol, RFInfo, RRType Reft, t1)]
forall a. [a] -> [a] -> [a]
++ ((Symbol, Maybe (RRType Reft))
 -> RRType Reft -> (Symbol, RFInfo, RRType Reft, t1))
-> [(Symbol, Maybe (RRType Reft))]
-> [RRType Reft]
-> [(Symbol, RFInfo, RRType Reft, t1)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Symbol, Maybe (RRType Reft))
-> RRType Reft -> (Symbol, RFInfo, RRType Reft, t1)
forall {d} {a} {c}.
Monoid d =>
(a, Maybe c) -> c -> (a, RFInfo, c, d)
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, RFInfo, 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 -> [Char] -> Bool -> Bool
forall a. PPrint a => [Char] -> a -> a
notracepp ([Char]
"isPredTy: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. PPrint a => a -> [Char]
showpp Type
t) (Bool -> Bool) -> Bool -> Bool
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)        = ((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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, Maybe (RRType Reft))]
xs
      nTs :: Int
nTs              = [Type] -> Int
forall a. [a] -> Int
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, d
forall a. Monoid a => a
mempty)
      g (a
x, Maybe c
_)      c
t  = (a
x, Bool -> RFInfo
classRFInfo Bool
allowTC, c
t, d
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 )(Type -> Bool) -> (RRType r -> Type) -> RRType r -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> RRType r -> Type
forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False (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 :: 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  = 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 :: forall a1 a. PPrint a1 => 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
                   -> F.Located LHName
                   -> Body
                   -> RType c tv Reft
                   -> RType c tv Reft
refineWithCtorBody :: forall a c tv.
Outputable a =>
a
-> Located LHName
-> BodyV Symbol
-> RType c tv Reft
-> RType c tv Reft
refineWithCtorBody a
dc Located LHName
f BodyV Symbol
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 v c tv.
Reftable r =>
RTypeV v c tv r -> r -> RTypeV v 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
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
v, Expr -> BodyV Symbol -> Expr
bodyPred (Expr -> [Expr] -> Expr
forall v. ExprV v -> [ExprV v] -> ExprV v
eApps (Symbol -> Expr
forall v. v -> ExprV v
EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ LHName -> Symbol
lhNameToResolvedSymbol (LHName -> Symbol) -> LHName -> Symbol
forall a b. (a -> b) -> a -> b
$ Located LHName -> LHName
forall a. Located a -> a
val Located LHName
f) [Symbol -> Expr
forall a. Symbolic a => a -> Expr
eVar Symbol
v]) BodyV Symbol
body)
    Maybe Reft
Nothing ->
      Maybe SrcSpan -> [Char] -> RType c tv Reft
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char] -> RType c tv Reft) -> [Char] -> RType c tv Reft
forall a b. (a -> b) -> a -> b
$ [Char]
"measure mismatch " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Located LHName -> [Char]
forall a. PPrint a => a -> [Char]
showpp Located LHName
f [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" on con " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Outputable a => a -> [Char]
showPpr a
dc


bodyPred ::  Expr -> Body -> Expr
bodyPred :: Expr -> BodyV Symbol -> Expr
bodyPred Expr
fv (E Expr
e)    = Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
Eq Expr
fv Expr
e
bodyPred Expr
fv (P Expr
p)    = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
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)