{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE NoMonomorphismRestriction  #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE PatternGuards              #-}
{-# LANGUAGE ScopedTypeVariables        #-}

{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

-- | This module defines the representation of Subtyping and WF Constraints,
--   and the code for syntax-directed constraint generation.

module Language.Haskell.Liquid.Constraint.Relational (consAssmRel, consRelTop) where

import           Control.Monad (foldM, forM_)
import           Data.Bifunctor                                 ( Bifunctor(bimap) )
import qualified Data.HashMap.Strict                            as M
import qualified Data.List                                      as L
import           Data.String                                    ( IsString(..) )
import qualified Language.Fixpoint.Types                        as F
import qualified Language.Fixpoint.Types.Visitor                as F
import           Language.Haskell.Liquid.Constraint.Env
import           Language.Haskell.Liquid.Constraint.Fresh
import           Language.Haskell.Liquid.Constraint.Monad
import           Language.Haskell.Liquid.Constraint.Types
import           Liquid.GHC.API                 ( Alt
                                                , AltCon(..)
                                                , Bind(..)
                                                , CoreBind
                                                , CoreBndr
                                                , CoreExpr
                                                , Expr(..)
                                                , Type(..)
                                                , TyVar
                                                , Var(..))
import qualified Liquid.GHC.API                as Ghc
import qualified Language.Haskell.Liquid.GHC.Misc               as GM
import           Language.Haskell.Liquid.GHC.Play               (Subable(sub, subTy))
import qualified Language.Haskell.Liquid.GHC.SpanStack          as Sp
import           Language.Haskell.Liquid.GHC.TypeRep            ()
import           Language.Haskell.Liquid.Misc
import           Language.Haskell.Liquid.Types.Fresh
import           Language.Haskell.Liquid.Types.Literals
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.RefType
import           Language.Haskell.Liquid.Types.Specs
import           Language.Haskell.Liquid.Types.Types hiding (binds)
import           Language.Haskell.Liquid.UX.Config
import           System.Console.CmdArgs.Verbosity               (whenLoud)
import           System.IO.Unsafe                               (unsafePerformIO)

data RelPred
  = RelPred { RelPred -> Var
fun1 :: Var
            , RelPred -> Var
fun2 :: Var
            , RelPred -> [(Symbol, [Symbol])]
args1 :: [(F.Symbol, [F.Symbol])]
            , RelPred -> [(Symbol, [Symbol])]
args2 :: [(F.Symbol, [F.Symbol])]
            , RelPred -> RelExpr
prop :: RelExpr
            } deriving Int -> RelPred -> ShowS
[RelPred] -> ShowS
RelPred -> [Char]
(Int -> RelPred -> ShowS)
-> (RelPred -> [Char]) -> ([RelPred] -> ShowS) -> Show RelPred
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RelPred -> ShowS
showsPrec :: Int -> RelPred -> ShowS
$cshow :: RelPred -> [Char]
show :: RelPred -> [Char]
$cshowList :: [RelPred] -> ShowS
showList :: [RelPred] -> ShowS
Show

type PrEnv = [RelPred]

consAssmRel :: Config -> TargetInfo -> (PrEnv, CGEnv) -> (Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr) -> CG (PrEnv, CGEnv)
consAssmRel :: Config
-> TargetInfo
-> ([RelPred], CGEnv)
-> (Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)
-> CG ([RelPred], CGEnv)
consAssmRel Config
_ TargetInfo
_ ([RelPred]
ψ, CGEnv
γ) (Var
x, Var
y, LocSpecType
t, LocSpecType
s, RelExpr
_, RelExpr
rp) = [Char]
-> Var
-> Var
-> LocSpecType
-> LocSpecType
-> Expr
-> CG ([RelPred], CGEnv)
-> CG ([RelPred], CGEnv)
forall e d t s p a.
(PPrint e, PPrint d, PPrint t, PPrint s, PPrint p) =>
[Char] -> e -> d -> t -> s -> p -> a -> a
traceChk [Char]
"Assm" Var
x Var
y LocSpecType
t LocSpecType
s Expr
p (CG ([RelPred], CGEnv) -> CG ([RelPred], CGEnv))
-> CG ([RelPred], CGEnv) -> CG ([RelPred], CGEnv)
forall a b. (a -> b) -> a -> b
$ do
  [Char] -> CG () -> CG ()
forall a. [Char] -> a -> a
traceWhenLoud ([Char]
"ASSUME " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (Expr, Expr) -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp (RelExpr -> Expr
fromRelExpr RelExpr
p', Expr
p)) (CG () -> CG ()) -> CG () -> CG ()
forall a b. (a -> b) -> a -> b
$ CGEnv -> Var -> SpecType -> CG ()
subUnarySig CGEnv
γ' Var
x SpecType
t'
  CGEnv -> Var -> SpecType -> CG ()
subUnarySig CGEnv
γ' Var
y SpecType
s'
  γ'' <- if SpecType -> Bool
base SpecType
t' Bool -> Bool -> Bool
&& SpecType -> Bool
base SpecType
s'
    then CGEnv
γ' CGEnv -> Expr -> CG CGEnv
`addPred` Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
F.subst
      ([(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
resL, Symbol -> Expr
forall v. v -> ExprV v
F.EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x), (Symbol
resR, Symbol -> Expr
forall v. v -> ExprV v
F.EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
y)])
      (RelExpr -> Expr
fromRelExpr RelExpr
rp)
    else CGEnv -> CG CGEnv
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ'
  return (RelPred x' y' bs cs rp : ψ, γ'')
 where
    p :: Expr
p = RelExpr -> Expr
fromRelExpr RelExpr
rp
    γ' :: CGEnv
γ' = CGEnv
γ CGEnv -> Span -> CGEnv
`setLocation` SrcSpan -> Span
Sp.Span (SourcePos -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (LocSpecType -> SourcePos
forall a. Located a -> SourcePos
F.loc LocSpecType
t))
    (Var
x', Var
y') = Var -> Var -> (Var, Var)
mkRelCopies Var
x Var
y
    t' :: SpecType
t' = LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
t
    s' :: SpecType
s' = LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
s
    ([Symbol]
vs, [SpecType]
ts) = SpecType -> ([Symbol], [SpecType])
vargs SpecType
t'
    ([Symbol]
us, [SpecType]
ss) = SpecType -> ([Symbol], [SpecType])
vargs SpecType
s'
    bs :: [(Symbol, [Symbol])]
bs = [Symbol] -> [[Symbol]] -> [(Symbol, [Symbol])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
vs (([Symbol], [SpecType]) -> [Symbol]
forall a b. (a, b) -> a
fst (([Symbol], [SpecType]) -> [Symbol])
-> (SpecType -> ([Symbol], [SpecType])) -> SpecType -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> ([Symbol], [SpecType])
vargs (SpecType -> [Symbol]) -> [SpecType] -> [[Symbol]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
ts)
    cs :: [(Symbol, [Symbol])]
cs = [Symbol] -> [[Symbol]] -> [(Symbol, [Symbol])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
us (([Symbol], [SpecType]) -> [Symbol]
forall a b. (a, b) -> a
fst (([Symbol], [SpecType]) -> [Symbol])
-> (SpecType -> ([Symbol], [SpecType])) -> SpecType -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> ([Symbol], [SpecType])
vargs (SpecType -> [Symbol]) -> [SpecType] -> [[Symbol]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
ss)
    p' :: RelExpr
p' = (RelExpr -> (Symbol, Symbol) -> RelExpr)
-> RelExpr -> [(Symbol, Symbol)] -> RelExpr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl (\RelExpr
q (Symbol
v, Symbol
u) -> Symbol -> Symbol -> RelExpr -> RelExpr
unapplyRelArgsR Symbol
v Symbol
u RelExpr
q) RelExpr
rp ([Symbol] -> [Symbol] -> [(Symbol, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
vs [Symbol]
us)

consRelTop :: Config -> TargetInfo -> CGEnv -> PrEnv -> (Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr) -> CG ()
consRelTop :: Config
-> TargetInfo
-> CGEnv
-> [RelPred]
-> (Var, Var, LocSpecType, LocSpecType, RelExpr, RelExpr)
-> CG ()
consRelTop Config
_ TargetInfo
ti CGEnv
γ [RelPred]
ψ (Var
x, Var
y, LocSpecType
t, LocSpecType
s, RelExpr
ra, RelExpr
rp) = [Char]
-> CoreBind
-> CoreBind
-> LocSpecType
-> LocSpecType
-> Expr
-> CG ()
-> CG ()
forall e d t s p a.
(PPrint e, PPrint d, PPrint t, PPrint s, PPrint p) =>
[Char] -> e -> d -> t -> s -> p -> a -> a
traceChk [Char]
"Init" CoreBind
e CoreBind
d LocSpecType
t LocSpecType
s Expr
p (CG () -> CG ()) -> CG () -> CG ()
forall a b. (a -> b) -> a -> b
$ do
  CGEnv -> Var -> SpecType -> CG ()
subUnarySig CGEnv
γ' Var
x SpecType
t'
  CGEnv -> Var -> SpecType -> CG ()
subUnarySig CGEnv
γ' Var
y SpecType
s'
  CGEnv
-> [RelPred]
-> CoreBind
-> CoreBind
-> SpecType
-> SpecType
-> RelExpr
-> RelExpr
-> CG ()
consRelCheckBind CGEnv
γ' [RelPred]
ψ CoreBind
e CoreBind
d SpecType
t' SpecType
s' RelExpr
ra RelExpr
rp
  where
    p :: Expr
p = RelExpr -> Expr
fromRelExpr RelExpr
rp
    γ' :: CGEnv
γ' = CGEnv
γ CGEnv -> Span -> CGEnv
`setLocation` SrcSpan -> Span
Sp.Span (SourcePos -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (LocSpecType -> SourcePos
forall a. Located a -> SourcePos
F.loc LocSpecType
t))
    cbs :: [CoreBind]
cbs = TargetSrc -> [CoreBind]
giCbs (TargetSrc -> [CoreBind]) -> TargetSrc -> [CoreBind]
forall a b. (a -> b) -> a -> b
$ TargetInfo -> TargetSrc
giSrc TargetInfo
ti
    e :: CoreBind
e = Var -> [CoreBind] -> CoreBind
lookupBind Var
x [CoreBind]
cbs
    d :: CoreBind
d = Var -> [CoreBind] -> CoreBind
lookupBind Var
y [CoreBind]
cbs
    t' :: SpecType
t' = SpecType -> SpecType
removeAbsRef (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
t
    s' :: SpecType
s' = SpecType -> SpecType
removeAbsRef (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
s

removeAbsRef :: SpecType -> SpecType
removeAbsRef :: SpecType -> SpecType
removeAbsRef (RVar RTyVar
v (MkUReft ReftV Symbol
r PredicateV Symbol
_))
  = SpecType
forall {v} {v} {c}.
Monoid (PredicateV v) =>
RTypeV v c RTyVar (UReftV v (ReftV Symbol))
out
    where
      r' :: UReftV v (ReftV Symbol)
r' = ReftV Symbol -> PredicateV v -> UReftV v (ReftV Symbol)
forall v r. r -> PredicateV v -> UReftV v r
MkUReft ReftV Symbol
r PredicateV v
forall a. Monoid a => a
mempty
      out :: RTypeV v c RTyVar (UReftV v (ReftV Symbol))
out = RTyVar
-> UReftV v (ReftV Symbol)
-> RTypeV v c RTyVar (UReftV v (ReftV Symbol))
forall v c tv r. tv -> r -> RTypeV v c tv r
RVar  RTyVar
v UReftV v (ReftV Symbol)
forall {v}. Monoid (PredicateV v) => UReftV v (ReftV Symbol)
r'
removeAbsRef (RFun  Symbol
b RFInfo
i SpecType
s SpecType
t (MkUReft ReftV Symbol
r PredicateV Symbol
_))
  = SpecType
out
    where
      r' :: UReftV v (ReftV Symbol)
r' = ReftV Symbol -> PredicateV v -> UReftV v (ReftV Symbol)
forall v r. r -> PredicateV v -> UReftV v r
MkUReft ReftV Symbol
r PredicateV v
forall a. Monoid a => a
mempty
      out :: SpecType
out = Symbol -> RFInfo -> SpecType -> SpecType -> RReft -> SpecType
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun  Symbol
b RFInfo
i (SpecType -> SpecType
removeAbsRef SpecType
s) (SpecType -> SpecType
removeAbsRef SpecType
t) RReft
forall {v}. Monoid (PredicateV v) => UReftV v (ReftV Symbol)
r'
removeAbsRef (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
b SpecType
t RReft
r)
  = RTVar RTyVar (RType RTyCon RTyVar ())
-> SpecType -> RReft -> SpecType
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVar RTyVar (RType RTyCon RTyVar ())
b (SpecType -> SpecType
removeAbsRef SpecType
t) RReft
r
removeAbsRef (RAllP PVUV Symbol RTyCon RTyVar
p SpecType
t)
  = SpecType -> SpecType
removeAbsRef (PVUV Symbol RTyCon RTyVar -> SpecType -> SpecType
forgetRAllP PVUV Symbol RTyCon RTyVar
p SpecType
t)
removeAbsRef (RApp  (RTyCon TyCon
c [PVUV Symbol RTyCon RTyVar]
_ TyConInfo
i) [SpecType]
as [RTProp RTyCon RTyVar RReft]
_ (MkUReft ReftV Symbol
r PredicateV Symbol
_))
  = SpecType
out
    where
      c' :: RTyCon
c' = TyCon -> [PVUV Symbol RTyCon RTyVar] -> TyConInfo -> RTyCon
RTyCon TyCon
c [] TyConInfo
i
      as' :: [SpecType]
as' = (SpecType -> SpecType) -> [SpecType] -> [SpecType]
forall a b. (a -> b) -> [a] -> [b]
map SpecType -> SpecType
removeAbsRef [SpecType]
as
      r' :: UReftV v (ReftV Symbol)
r' = ReftV Symbol -> PredicateV v -> UReftV v (ReftV Symbol)
forall v r. r -> PredicateV v -> UReftV v r
MkUReft ReftV Symbol
r PredicateV v
forall a. Monoid a => a
mempty
      out :: SpecType
out = RTyCon
-> [SpecType] -> [RTProp RTyCon RTyVar RReft] -> RReft -> SpecType
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp RTyCon
c' [SpecType]
as' [] RReft
forall {v}. Monoid (PredicateV v) => UReftV v (ReftV Symbol)
r'
removeAbsRef (RAllE Symbol
b SpecType
a SpecType
t)
  = Symbol -> SpecType -> SpecType -> SpecType
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
RAllE Symbol
b (SpecType -> SpecType
removeAbsRef SpecType
a) (SpecType -> SpecType
removeAbsRef SpecType
t)
removeAbsRef (REx   Symbol
b SpecType
a SpecType
t)
  = Symbol -> SpecType -> SpecType -> SpecType
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
REx   Symbol
b (SpecType -> SpecType
removeAbsRef SpecType
a) (SpecType -> SpecType
removeAbsRef SpecType
t)
removeAbsRef (RAppTy SpecType
s SpecType
t RReft
r)
  = SpecType -> SpecType -> RReft -> SpecType
forall v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAppTy (SpecType -> SpecType
removeAbsRef SpecType
s) (SpecType -> SpecType
removeAbsRef SpecType
t) RReft
r
removeAbsRef (RRTy  [(Symbol, SpecType)]
e RReft
r Oblig
o SpecType
t)
  = [(Symbol, SpecType)] -> RReft -> Oblig -> SpecType -> SpecType
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy  [(Symbol, SpecType)]
e RReft
r Oblig
o (SpecType -> SpecType
removeAbsRef SpecType
t)
removeAbsRef SpecType
t
  = SpecType
t

--------------------------------------------------------------
-- Core Checking Rules ---------------------------------------
--------------------------------------------------------------

resL, resR :: F.Symbol
resL :: Symbol
resL = [Char] -> Symbol
forall a. IsString a => [Char] -> a
fromString [Char]
"r1"
resR :: Symbol
resR = [Char] -> Symbol
forall a. IsString a => [Char] -> a
fromString [Char]
"r2"

relSuffixL, relSuffixR :: String
relSuffixL :: [Char]
relSuffixL = [Char]
"l"
relSuffixR :: [Char]
relSuffixR = [Char]
"r"

-- recursion rule
consRelCheckBind :: CGEnv -> PrEnv -> CoreBind -> CoreBind -> SpecType -> SpecType -> RelExpr -> RelExpr -> CG ()
consRelCheckBind :: CGEnv
-> [RelPred]
-> CoreBind
-> CoreBind
-> SpecType
-> SpecType
-> RelExpr
-> RelExpr
-> CG ()
consRelCheckBind CGEnv
γ [RelPred]
ψ b1 :: CoreBind
b1@(NonRec Var
_ CoreExpr
e1) b2 :: CoreBind
b2@(NonRec Var
_ CoreExpr
e2) SpecType
t1 SpecType
t2 RelExpr
ra RelExpr
rp
  | Maybe
  ([Var], [Var], [Symbol], [Symbol], [SpecType], [SpecType], [Expr])
Nothing <- CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> Maybe
     ([Var], [Var], [Symbol], [Symbol], [SpecType], [SpecType], [Expr])
args CoreExpr
e1 CoreExpr
e2 SpecType
t1 SpecType
t2 Expr
p =
  [Char]
-> CoreBind
-> CoreBind
-> SpecType
-> SpecType
-> Expr
-> CG ()
-> CG ()
forall e d t s p a.
(PPrint e, PPrint d, PPrint t, PPrint s, PPrint p) =>
[Char] -> e -> d -> t -> s -> p -> a -> a
traceChk [Char]
"Bind NonRec" CoreBind
b1 CoreBind
b2 SpecType
t1 SpecType
t2 Expr
p (CG () -> CG ()) -> CG () -> CG ()
forall a b. (a -> b) -> a -> b
$ do
    γ' <- CGEnv
γ CGEnv -> Expr -> CG CGEnv
`addPred` Expr
a
    consRelCheck γ' ψ e1 e2 t1 t2 p
  where
    a :: Expr
a = RelExpr -> Expr
fromRelExpr RelExpr
ra
    p :: Expr
p = RelExpr -> Expr
fromRelExpr RelExpr
rp

consRelCheckBind CGEnv
γ [RelPred]
ψ (NonRec Var
x1 CoreExpr
e1) CoreBind
b2 SpecType
t1 SpecType
t2 RelExpr
a RelExpr
p =
  CGEnv
-> [RelPred]
-> CoreBind
-> CoreBind
-> SpecType
-> SpecType
-> RelExpr
-> RelExpr
-> CG ()
consRelCheckBind CGEnv
γ [RelPred]
ψ ([(Var, CoreExpr)] -> CoreBind
forall b. [(b, Expr b)] -> Bind b
Rec [(Var
x1, CoreExpr
e1)]) CoreBind
b2 SpecType
t1 SpecType
t2 RelExpr
a RelExpr
p

consRelCheckBind CGEnv
γ [RelPred]
ψ CoreBind
b1 (NonRec Var
x2 CoreExpr
e2) SpecType
t1 SpecType
t2 RelExpr
a RelExpr
p =
  CGEnv
-> [RelPred]
-> CoreBind
-> CoreBind
-> SpecType
-> SpecType
-> RelExpr
-> RelExpr
-> CG ()
consRelCheckBind CGEnv
γ [RelPred]
ψ CoreBind
b1 ([(Var, CoreExpr)] -> CoreBind
forall b. [(b, Expr b)] -> Bind b
Rec [(Var
x2, CoreExpr
e2)]) SpecType
t1 SpecType
t2 RelExpr
a RelExpr
p

consRelCheckBind CGEnv
γ [RelPred]
ψ b1 :: CoreBind
b1@(Rec [(Var
f1, CoreExpr
e1)]) b2 :: CoreBind
b2@(Rec [(Var
f2, CoreExpr
e2)]) SpecType
t1 SpecType
t2 RelExpr
ra RelExpr
rp
  | Just ([Var]
xs1, [Var]
xs2, [Symbol]
vs1, [Symbol]
vs2, [SpecType]
ts1, [SpecType]
ts2, [Expr]
qs) <- CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> Maybe
     ([Var], [Var], [Symbol], [Symbol], [SpecType], [SpecType], [Expr])
args CoreExpr
e1 CoreExpr
e2 SpecType
t1 SpecType
t2 Expr
p
  = [Char]
-> CoreBind
-> CoreBind
-> SpecType
-> SpecType
-> Expr
-> CG ()
-> CG ()
forall e d t s p a.
(PPrint e, PPrint d, PPrint t, PPrint s, PPrint p) =>
[Char] -> e -> d -> t -> s -> p -> a -> a
traceChk [Char]
"Bind Rec" CoreBind
b1 CoreBind
b2 SpecType
t1 SpecType
t2 Expr
p (CG () -> CG ()) -> CG () -> CG ()
forall a b. (a -> b) -> a -> b
$ do
    [RReft] -> (RReft -> CG ()) -> CG ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (SpecType -> [RReft]
refts SpecType
t1 [RReft] -> [RReft] -> [RReft]
forall a. [a] -> [a] -> [a]
++ SpecType -> [RReft]
refts SpecType
t2) (\RReft
r -> CGEnv -> RReft -> [Char] -> CG ()
entlFunReft CGEnv
γ RReft
r [Char]
"consRelCheckBind Rec")
    let xs' :: [(Var, Var)]
xs' = (Var -> Var -> (Var, Var)) -> [Var] -> [Var] -> [(Var, Var)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Var -> Var -> (Var, Var)
mkRelCopies [Var]
xs1 [Var]
xs2
    let ([Var]
xs1', [Var]
xs2') = [(Var, Var)] -> ([Var], [Var])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Var, Var)]
xs'
    let (CoreExpr
e1'', CoreExpr
e2'') = ((CoreExpr, CoreExpr) -> (Var, Var) -> (CoreExpr, CoreExpr))
-> (CoreExpr, CoreExpr) -> [(Var, Var)] -> (CoreExpr, CoreExpr)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (CoreExpr, CoreExpr) -> (Var, Var) -> (CoreExpr, CoreExpr)
subRel (CoreExpr
e1', CoreExpr
e2') ([Var] -> [Var] -> [(Var, Var)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs1 [Var]
xs2)
    γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"Bind Rec f1", Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
f1', SpecType
t1) CG CGEnv -> (CGEnv -> CG CGEnv) -> CG CGEnv
forall a b.
StateT CGInfo Identity a
-> (a -> StateT CGInfo Identity b) -> StateT CGInfo Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"Bind Rec f2", Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
f2', SpecType
t2))
    γ'' <- foldM (\CGEnv
γγ (Var
x, SpecType
t) -> CGEnv
γγ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"Bind Rec x1", Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x, SpecType
t)) γ' (zip (xs1' ++ xs2') (ts1 ++ ts2))
    let vs2xs =  Subst -> a -> a
forall a. Subable a => Subst -> a -> a
F.subst (Subst -> a -> a) -> Subst -> a -> a
forall a b. (a -> b) -> a -> b
$ [(Symbol, Expr)] -> Subst
F.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 ([Symbol]
vs1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol]
vs2) ([Expr] -> [(Symbol, Expr)]) -> [Expr] -> [(Symbol, Expr)]
forall a b. (a -> b) -> a -> b
$ (Var -> Expr) -> [Var] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol -> Expr
forall v. v -> ExprV v
F.EVar (Symbol -> Expr) -> (Var -> Symbol) -> Var -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol) ([Var]
xs1' [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var]
xs2')
    let (ho, fo) = partitionArgs xs1 xs2 ts1 ts2 qs
    γ''' <- γ'' `addPreds` traceWhenLoud ("PRECONDITION " ++ F.showpp (vs2xs (F.PAnd fo)) ++ "\n" ++
                                          "ASSUMPTION " ++ F.showpp (vs2xs a))
                              map vs2xs [F.PAnd fo, a]
    let p' = RelExpr -> [(Symbol, Symbol)] -> RelExpr
unapp RelExpr
rp ([Symbol] -> [Symbol] -> [(Symbol, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
vs1 [Symbol]
vs2)
    let ψ' = [RelPred]
ho [RelPred] -> [RelPred] -> [RelPred]
forall a. [a] -> [a] -> [a]
++ [RelPred]
ψ
    consRelCheck γ''' ψ' (xbody e1'') (xbody e2'') (vs2xs $ ret t1) (vs2xs $ ret t2) (vs2xs $ concl (fromRelExpr p'))
  where
    a :: Expr
a = RelExpr -> Expr
fromRelExpr RelExpr
ra
    p :: Expr
p = RelExpr -> Expr
fromRelExpr RelExpr
rp
    (Var
f1', Var
f2') = Var -> Var -> (Var, Var)
mkRelCopies Var
f1 Var
f2
    (CoreExpr
e1', CoreExpr
e2') = CoreExpr -> Var -> CoreExpr -> Var -> (CoreExpr, CoreExpr)
subRelCopies CoreExpr
e1 Var
f1 CoreExpr
e2 Var
f2
    unapp :: RelExpr -> [(F.Symbol, F.Symbol)] -> RelExpr
    unapp :: RelExpr -> [(Symbol, Symbol)] -> RelExpr
unapp = (RelExpr -> (Symbol, Symbol) -> RelExpr)
-> RelExpr -> [(Symbol, Symbol)] -> RelExpr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (\RelExpr
p' (Symbol
v1, Symbol
v2) -> Symbol -> Symbol -> RelExpr -> RelExpr
unapplyRelArgsR Symbol
v1 Symbol
v2 RelExpr
p')
    subRel :: (CoreExpr, CoreExpr) -> (Var, Var) -> (CoreExpr, CoreExpr)
subRel (CoreExpr
e1'', CoreExpr
e2'') (Var
x1, Var
x2) = CoreExpr -> Var -> CoreExpr -> Var -> (CoreExpr, CoreExpr)
subRelCopies CoreExpr
e1'' Var
x1 CoreExpr
e2'' Var
x2

consRelCheckBind CGEnv
_ [RelPred]
_ (Rec [(Var
_, CoreExpr
e1)]) (Rec [(Var
_, CoreExpr
e2)]) SpecType
t1 SpecType
t2 RelExpr
_ RelExpr
rp
  = [Char] -> CG ()
forall a. [Char] -> a
F.panic ([Char] -> CG ()) -> [Char] -> CG ()
forall a b. (a -> b) -> a -> b
$ [Char]
"consRelCheckBind Rec: exprs, types, and pred should have same number of args " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++
    Maybe
  ([Var], [Var], [Symbol], [Symbol], [SpecType], [SpecType], [Expr])
-> [Char]
forall a. Show a => a -> [Char]
show (CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> Maybe
     ([Var], [Var], [Symbol], [Symbol], [SpecType], [SpecType], [Expr])
args CoreExpr
e1 CoreExpr
e2 SpecType
t1 SpecType
t2 Expr
p)
    where
      p :: Expr
p = RelExpr -> Expr
fromRelExpr RelExpr
rp

consRelCheckBind CGEnv
_ [RelPred]
_ b1 :: CoreBind
b1@(Rec [(Var, CoreExpr)]
_) b2 :: CoreBind
b2@(Rec [(Var, CoreExpr)]
_) SpecType
_ SpecType
_ RelExpr
_ RelExpr
_
  = [Char] -> CG ()
forall a. [Char] -> a
F.panic ([Char] -> CG ()) -> [Char] -> CG ()
forall a b. (a -> b) -> a -> b
$ [Char]
"consRelCheckBind Rec: multiple binders are not supported " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (CoreBind, CoreBind) -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp (CoreBind
b1, CoreBind
b2)

consRelCheck :: CGEnv -> PrEnv -> CoreExpr -> CoreExpr ->
  SpecType -> SpecType -> F.Expr -> CG ()
consRelCheck :: CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
consRelCheck CGEnv
γ [RelPred]
ψ (Tick CoreTickish
tt CoreExpr
e) CoreExpr
d SpecType
t SpecType
s Expr
p =
  CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
consRelCheck (CGEnv
γ CGEnv -> Span -> CGEnv
`setLocation` CoreTickish -> Span
Sp.Tick CoreTickish
tt) [RelPred]
ψ CoreExpr
e CoreExpr
d SpecType
t SpecType
s Expr
p

consRelCheck CGEnv
γ [RelPred]
ψ CoreExpr
e (Tick CoreTickish
tt CoreExpr
d) SpecType
t SpecType
s Expr
p =
  CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
consRelCheck (CGEnv
γ CGEnv -> Span -> CGEnv
`setLocation` CoreTickish -> Span
Sp.Tick CoreTickish
tt) [RelPred]
ψ CoreExpr
e CoreExpr
d SpecType
t SpecType
s Expr
p

consRelCheck CGEnv
γ [RelPred]
ψ l1 :: CoreExpr
l1@(Lam Var
α1 CoreExpr
e1) CoreExpr
e2 rt1 :: SpecType
rt1@(RAllT RTVar RTyVar (RType RTyCon RTyVar ())
s1 SpecType
t1 RReft
r1) SpecType
t2 Expr
p
  | Var -> Bool
Ghc.isTyVar Var
α1
  = [Char]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
-> CG ()
forall e d t s p a.
(PPrint e, PPrint d, PPrint t, PPrint s, PPrint p) =>
[Char] -> e -> d -> t -> s -> p -> a -> a
traceChk [Char]
"Lam Type L" CoreExpr
l1 CoreExpr
e2 SpecType
rt1 SpecType
t2 Expr
p (CG () -> CG ()) -> CG () -> CG ()
forall a b. (a -> b) -> a -> b
$ do
    CGEnv -> RReft -> [Char] -> CG ()
entlFunReft CGEnv
γ RReft
r1 [Char]
"consRelCheck Lam Type"
    γ'  <- CGEnv
γ CGEnv -> Var -> CG CGEnv
`extendWithTyVar` Var
α1
    consRelCheck γ' ψ e1 e2 (sb (s1, α1) t1) t2 p
  where sb :: (RTVar RTyVar s, Var) -> RType c RTyVar r -> RType c RTyVar r
sb (RTVar RTyVar s
s, Var
α) = (RTyVar, RType c RTyVar r) -> RType c RTyVar r -> RType c RTyVar r
forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
(tv, RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarMeet' (RTVar RTyVar s -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar s
s, Var -> RType c RTyVar r
forall r c. Monoid r => Var -> RType c RTyVar r
rVar Var
α)

consRelCheck CGEnv
γ [RelPred]
ψ CoreExpr
e1 l2 :: CoreExpr
l2@(Lam Var
α2 CoreExpr
e2) SpecType
t1 rt2 :: SpecType
rt2@(RAllT RTVar RTyVar (RType RTyCon RTyVar ())
s2 SpecType
t2 RReft
r2) Expr
p
  | Var -> Bool
Ghc.isTyVar Var
α2
  = [Char]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
-> CG ()
forall e d t s p a.
(PPrint e, PPrint d, PPrint t, PPrint s, PPrint p) =>
[Char] -> e -> d -> t -> s -> p -> a -> a
traceChk [Char]
"Lam Type" CoreExpr
e1 CoreExpr
l2 SpecType
t1 SpecType
rt2 Expr
p (CG () -> CG ()) -> CG () -> CG ()
forall a b. (a -> b) -> a -> b
$ do
    CGEnv -> RReft -> [Char] -> CG ()
entlFunReft CGEnv
γ RReft
r2 [Char]
"consRelCheck Lam Type"
    γ'  <- CGEnv
γ CGEnv -> Var -> CG CGEnv
`extendWithTyVar` Var
α2
    consRelCheck γ' ψ e1 e2 t1 (sb (s2, α2) t2) p
  where sb :: (RTVar RTyVar s, Var) -> RType c RTyVar r -> RType c RTyVar r
sb (RTVar RTyVar s
s, Var
α) = (RTyVar, RType c RTyVar r) -> RType c RTyVar r -> RType c RTyVar r
forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
(tv, RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarMeet' (RTVar RTyVar s -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar s
s, Var -> RType c RTyVar r
forall r c. Monoid r => Var -> RType c RTyVar r
rVar Var
α)

consRelCheck CGEnv
γ [RelPred]
ψ l1 :: CoreExpr
l1@(Lam Var
α1 CoreExpr
e1) l2 :: CoreExpr
l2@(Lam Var
α2 CoreExpr
e2) rt1 :: SpecType
rt1@(RAllT RTVar RTyVar (RType RTyCon RTyVar ())
s1 SpecType
t1 RReft
r1) rt2 :: SpecType
rt2@(RAllT RTVar RTyVar (RType RTyCon RTyVar ())
s2 SpecType
t2 RReft
r2) Expr
p
  | Var -> Bool
Ghc.isTyVar Var
α1 Bool -> Bool -> Bool
&& Var -> Bool
Ghc.isTyVar Var
α2
  = [Char]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
-> CG ()
forall e d t s p a.
(PPrint e, PPrint d, PPrint t, PPrint s, PPrint p) =>
[Char] -> e -> d -> t -> s -> p -> a -> a
traceChk [Char]
"Lam Type" CoreExpr
l1 CoreExpr
l2 SpecType
rt1 SpecType
rt2 Expr
p (CG () -> CG ()) -> CG () -> CG ()
forall a b. (a -> b) -> a -> b
$ do
    CGEnv -> RReft -> RReft -> [Char] -> CG ()
entlFunRefts CGEnv
γ RReft
r1 RReft
r2 [Char]
"consRelCheck Lam Type"
    γ'  <- CGEnv
γ CGEnv -> Var -> CG CGEnv
`extendWithTyVar` Var
α1
    γ'' <- γ' `extendWithTyVar` α2
    consRelCheck γ'' ψ e1 e2 (sb (s1, α1) t1) (sb (s2, α2) t2) p
  where sb :: (RTVar RTyVar s, Var) -> RType c RTyVar r -> RType c RTyVar r
sb (RTVar RTyVar s
s, Var
α) = (RTyVar, RType c RTyVar r) -> RType c RTyVar r -> RType c RTyVar r
forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
(tv, RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarMeet' (RTVar RTyVar s -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar s
s, Var -> RType c RTyVar r
forall r c. Monoid r => Var -> RType c RTyVar r
rVar Var
α)

consRelCheck CGEnv
γ [RelPred]
ψ l1 :: CoreExpr
l1@(Lam Var
x1 CoreExpr
e1) l2 :: CoreExpr
l2@(Lam Var
x2 CoreExpr
e2) rt1 :: SpecType
rt1@(RFun Symbol
v1 RFInfo
_ SpecType
s1 SpecType
t1 RReft
r1) rt2 :: SpecType
rt2@(RFun Symbol
v2 RFInfo
_ SpecType
s2 SpecType
t2 RReft
r2) pr :: Expr
pr@(F.PImp Expr
q Expr
p)
  = [Char]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
-> CG ()
forall e d t s p a.
(PPrint e, PPrint d, PPrint t, PPrint s, PPrint p) =>
[Char] -> e -> d -> t -> s -> p -> a -> a
traceChk [Char]
"Lam Expr" CoreExpr
l1 CoreExpr
l2 SpecType
rt1 SpecType
rt2 Expr
pr (CG () -> CG ()) -> CG () -> CG ()
forall a b. (a -> b) -> a -> b
$ do
    CGEnv -> RReft -> RReft -> [Char] -> CG ()
entlFunRefts CGEnv
γ RReft
r1 RReft
r2 [Char]
"consRelCheck Lam Expr"
    let (Symbol
pvar1, Symbol
pvar2) = (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
evar1, Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
evar2)
    let subst :: a -> a
subst = Subst -> a -> a
forall a. Subable a => Subst -> a -> a
F.subst (Subst -> a -> a) -> Subst -> a -> a
forall a b. (a -> b) -> a -> b
$ [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
v1, Symbol -> Expr
forall v. v -> ExprV v
F.EVar Symbol
pvar1), (Symbol
v2, Symbol -> Expr
forall v. v -> ExprV v
F.EVar Symbol
pvar2)]
    γ'  <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consRelCheck Lam L", Symbol
pvar1, SpecType -> SpecType
forall {a}. Subable a => a -> a
subst SpecType
s1)
    γ'' <- γ' += ("consRelCheck Lam R", pvar2, subst s2)
    let p'    = Symbol -> Symbol -> Expr -> Expr
unapplyRelArgs Symbol
v1 Symbol
v2 Expr
p
    let (ho, fo) = partitionArg x1 x2 s1 s2 q
    γ''' <- γ'' `addPreds` traceWhenLoud ("PRECONDITION " ++ F.showpp (map subst fo)) map subst fo
    consRelCheck γ''' (ho ++ ψ) e1' e2' (subst t1) (subst t2) (subst p')
  where
    (Var
evar1, Var
evar2) = Var -> Var -> (Var, Var)
mkRelCopies Var
x1 Var
x2
    (CoreExpr
e1', CoreExpr
e2')     = CoreExpr -> Var -> CoreExpr -> Var -> (CoreExpr, CoreExpr)
subRelCopies CoreExpr
e1 Var
x1 CoreExpr
e2 Var
x2

consRelCheck CGEnv
γ [RelPred]
ψ l1 :: CoreExpr
l1@(Let (NonRec Var
x1 CoreExpr
d1) CoreExpr
e1) l2 :: CoreExpr
l2@(Let (NonRec Var
x2 CoreExpr
d2) CoreExpr
e2) SpecType
t1 SpecType
t2 Expr
p
  = [Char]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
-> CG ()
forall e d t s p a.
(PPrint e, PPrint d, PPrint t, PPrint s, PPrint p) =>
[Char] -> e -> d -> t -> s -> p -> a -> a
traceChk [Char]
"Let" CoreExpr
l1 CoreExpr
l2 SpecType
t1 SpecType
t2 Expr
p (CG () -> CG ()) -> CG () -> CG ()
forall a b. (a -> b) -> a -> b
$ do
    (s1, s2, _) <- CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
consRelSynth CGEnv
γ [RelPred]
ψ CoreExpr
d1 CoreExpr
d2
    let (evar1, evar2) = mkRelCopies x1 x2
    let (e1', e2')     = subRelCopies e1 x1 e2 x2
    γ'  <- γ += ("consRelCheck Let L", F.symbol evar1, s1)
    γ'' <- γ' += ("consRelCheck Let R", F.symbol evar2, s2)
    consRelCheck γ'' ψ e1' e2' t1 t2 p


consRelCheck CGEnv
γ [RelPred]
ψ l1 :: CoreExpr
l1@(Let (Rec []) CoreExpr
e1) l2 :: CoreExpr
l2@(Let (Rec []) CoreExpr
e2) SpecType
t1 SpecType
t2 Expr
p
  = [Char]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
-> CG ()
forall e d t s p a.
(PPrint e, PPrint d, PPrint t, PPrint s, PPrint p) =>
[Char] -> e -> d -> t -> s -> p -> a -> a
traceChk [Char]
"Let Rec Nil" CoreExpr
l1 CoreExpr
l2 SpecType
t1 SpecType
t2 Expr
p (CG () -> CG ()) -> CG () -> CG ()
forall a b. (a -> b) -> a -> b
$ do
    CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
consRelCheck CGEnv
γ [RelPred]
ψ CoreExpr
e1 CoreExpr
e2 SpecType
t1 SpecType
t2 Expr
p

consRelCheck CGEnv
γ [RelPred]
ψ l1 :: CoreExpr
l1@(Let (Rec ((Var
x1, CoreExpr
d1):[(Var, CoreExpr)]
bs1)) CoreExpr
e1) l2 :: CoreExpr
l2@(Let (Rec ((Var
x2, CoreExpr
d2):[(Var, CoreExpr)]
bs2)) CoreExpr
e2) SpecType
t1 SpecType
t2 Expr
p
  = [Char]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
-> CG ()
forall e d t s p a.
(PPrint e, PPrint d, PPrint t, PPrint s, PPrint p) =>
[Char] -> e -> d -> t -> s -> p -> a -> a
traceChk [Char]
"Let Rec Cons" CoreExpr
l1 CoreExpr
l2 SpecType
t1 SpecType
t2 Expr
p (CG () -> CG ()) -> CG () -> CG ()
forall a b. (a -> b) -> a -> b
$ do
    (s1, s2, _) <- CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
consRelSynth CGEnv
γ [RelPred]
ψ CoreExpr
d1 CoreExpr
d2
    let (evar1, evar2) = mkRelCopies x1 x2
    let (e1', e2')     = subRelCopies e1 x1 e2 x2
    γ'  <- γ += ("consRelCheck Let L", F.symbol evar1, s1)
    γ'' <- γ' += ("consRelCheck Let R", F.symbol evar2, s2)
    consRelCheck γ'' ψ (Let (Rec bs1) e1') (Let (Rec bs2) e2') t1 t2 p

consRelCheck CGEnv
γ [RelPred]
ψ c1 :: CoreExpr
c1@(Case CoreExpr
e1 Var
x1 Type
_ [Alt Var]
alts1) CoreExpr
e2 SpecType
t1 SpecType
t2 Expr
p =
  [Char]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
-> CG ()
forall e d t s p a.
(PPrint e, PPrint d, PPrint t, PPrint s, PPrint p) =>
[Char] -> e -> d -> t -> s -> p -> a -> a
traceChk [Char]
"Case Async L" CoreExpr
c1 CoreExpr
e2 SpecType
t1 SpecType
t2 Expr
p (CG () -> CG ()) -> CG () -> CG ()
forall a b. (a -> b) -> a -> b
$ do
    s1 <- CGEnv -> CoreExpr -> CG SpecType
consUnarySynth CGEnv
γ CoreExpr
e1
    γ' <- γ += ("consRelCheck Case Async L", x1', s1)
    forM_ alts1 $ consRelCheckAltAsyncL γ' ψ t1 t2 p x1' s1 e2
  where
    x1' :: Symbol
x1' = Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Var -> Symbol) -> Var -> Symbol
forall a b. (a -> b) -> a -> b
$ [Char] -> Var -> Var
mkCopyWithSuffix [Char]
relSuffixL Var
x1

consRelCheck CGEnv
γ [RelPred]
ψ CoreExpr
e1 c2 :: CoreExpr
c2@(Case CoreExpr
e2 Var
x2 Type
_ [Alt Var]
alts2) SpecType
t1 SpecType
t2 Expr
p =
  [Char]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
-> CG ()
forall e d t s p a.
(PPrint e, PPrint d, PPrint t, PPrint s, PPrint p) =>
[Char] -> e -> d -> t -> s -> p -> a -> a
traceChk [Char]
"Case Async R" CoreExpr
e1 CoreExpr
c2 SpecType
t1 SpecType
t2 Expr
p (CG () -> CG ()) -> CG () -> CG ()
forall a b. (a -> b) -> a -> b
$ do
    s2 <- CGEnv -> CoreExpr -> CG SpecType
consUnarySynth CGEnv
γ CoreExpr
e2
    γ' <- γ += ("consRelCheck Case Async R", x2', s2)
    forM_ alts2 $ consRelCheckAltAsyncR γ' ψ t1 t2 p e1 x2' s2
  where
    x2' :: Symbol
x2' = Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Var -> Symbol) -> Var -> Symbol
forall a b. (a -> b) -> a -> b
$ [Char] -> Var -> Var
mkCopyWithSuffix [Char]
relSuffixR Var
x2

consRelCheck CGEnv
γ [RelPred]
ψ CoreExpr
e CoreExpr
d SpecType
t1 SpecType
t2 Expr
p =
  [Char]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
-> CG ()
forall e d t s p a.
(PPrint e, PPrint d, PPrint t, PPrint s, PPrint p) =>
[Char] -> e -> d -> t -> s -> p -> a -> a
traceChk [Char]
"Synth" CoreExpr
e CoreExpr
d SpecType
t1 SpecType
t2 Expr
p (CG () -> CG ()) -> CG () -> CG ()
forall a b. (a -> b) -> a -> b
$ do
  (s1, s2, qs) <- CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
consRelSynth CGEnv
γ [RelPred]
ψ CoreExpr
e CoreExpr
d
  let psubst = (Symbol -> Expr) -> c -> c
forall a. Subable a => (Symbol -> Expr) -> a -> a
F.substf (SpecType -> SpecType -> Symbol -> Expr
matchFunArgs SpecType
t1 SpecType
s1) (c -> c) -> (c -> c) -> c -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Expr) -> c -> c
forall a. Subable a => (Symbol -> Expr) -> a -> a
F.substf (SpecType -> SpecType -> Symbol -> Expr
matchFunArgs SpecType
t2 SpecType
s2)
  consRelSub γ s1 s2 (F.PAnd qs) (psubst p)
  addC (SubC γ s1 t1) ("consRelCheck (Synth): s1 = " ++ F.showpp s1 ++ " t1 = " ++ F.showpp t1)
  addC (SubC γ s2 t2) ("consRelCheck (Synth): s2 = " ++ F.showpp s2 ++ " t2 = " ++ F.showpp t2)

consExtAltEnv :: CGEnv -> F.Symbol -> SpecType -> AltCon -> [Var] -> CoreExpr -> String -> CG (CGEnv, CoreExpr)
consExtAltEnv :: CGEnv
-> Symbol
-> SpecType
-> AltCon
-> [Var]
-> CoreExpr
-> [Char]
-> CG (CGEnv, CoreExpr)
consExtAltEnv CGEnv
γ Symbol
x SpecType
s AltCon
c [Var]
bs CoreExpr
e [Char]
suf = do
  ct <- CGEnv -> AltCon -> SpecType -> CG SpecType
ctorTy CGEnv
γ AltCon
c SpecType
s
  unapply γ x s bs (removeAbsRef ct) e suf

consRelCheckAltAsyncL :: CGEnv -> PrEnv -> SpecType -> SpecType -> F.Expr ->
  F.Symbol -> SpecType -> CoreExpr -> Alt CoreBndr -> CG ()
consRelCheckAltAsyncL :: CGEnv
-> [RelPred]
-> SpecType
-> SpecType
-> Expr
-> Symbol
-> SpecType
-> CoreExpr
-> Alt Var
-> CG ()
consRelCheckAltAsyncL CGEnv
γ [RelPred]
ψ SpecType
t1 SpecType
t2 Expr
p Symbol
x1 SpecType
s1 CoreExpr
e2 (Ghc.Alt AltCon
c [Var]
bs1 CoreExpr
e1) = do
  (γ', e1') <- CGEnv
-> Symbol
-> SpecType
-> AltCon
-> [Var]
-> CoreExpr
-> [Char]
-> CG (CGEnv, CoreExpr)
consExtAltEnv CGEnv
γ Symbol
x1 SpecType
s1 AltCon
c [Var]
bs1 CoreExpr
e1 [Char]
relSuffixL
  consRelCheck γ' ψ e1' e2 t1 t2 p

consRelCheckAltAsyncR :: CGEnv -> PrEnv -> SpecType -> SpecType -> F.Expr ->
  CoreExpr -> F.Symbol -> SpecType -> Alt CoreBndr -> CG ()
consRelCheckAltAsyncR :: CGEnv
-> [RelPred]
-> SpecType
-> SpecType
-> Expr
-> CoreExpr
-> Symbol
-> SpecType
-> Alt Var
-> CG ()
consRelCheckAltAsyncR CGEnv
γ [RelPred]
ψ SpecType
t1 SpecType
t2 Expr
p CoreExpr
e1 Symbol
x2 SpecType
s2 (Ghc.Alt AltCon
c [Var]
bs2 CoreExpr
e2) = do
  (γ', e2') <- CGEnv
-> Symbol
-> SpecType
-> AltCon
-> [Var]
-> CoreExpr
-> [Char]
-> CG (CGEnv, CoreExpr)
consExtAltEnv CGEnv
γ Symbol
x2 SpecType
s2 AltCon
c [Var]
bs2 CoreExpr
e2 [Char]
relSuffixR
  consRelCheck γ' ψ e1 e2' t1 t2 p

ctorTy :: CGEnv -> AltCon -> SpecType -> CG SpecType
ctorTy :: CGEnv -> AltCon -> SpecType -> CG SpecType
ctorTy CGEnv
γ (DataAlt DataCon
c) (RApp RTyCon
_ [SpecType]
ts [RTProp RTyCon RTyVar RReft]
_ RReft
_)
  | Just SpecType
ct <- Maybe SpecType
mbct = SpecType -> CG SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshTy (SpecType -> CG SpecType) -> SpecType -> CG SpecType
forall a b. (a -> b) -> a -> b
$ SpecType
ct SpecType -> [SpecType] -> SpecType
`instantiateTys` [SpecType]
ts
  | Maybe SpecType
Nothing <- Maybe SpecType
mbct = [Char] -> CG SpecType
forall a. [Char] -> a
F.panic ([Char] -> CG SpecType) -> [Char] -> CG SpecType
forall a b. (a -> b) -> a -> b
$ [Char]
"ctorTy: data constructor out of scope" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ DataCon -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp DataCon
c
  where mbct :: Maybe SpecType
mbct = CGEnv
γ (?callStack::CallStack) => CGEnv -> Symbol -> Maybe SpecType
CGEnv -> Symbol -> Maybe SpecType
?= Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (DataCon -> Var
Ghc.dataConWorkId DataCon
c)
ctorTy CGEnv
_ (DataAlt DataCon
_) SpecType
t =
  [Char] -> CG SpecType
forall a. [Char] -> a
F.panic ([Char] -> CG SpecType) -> [Char] -> CG SpecType
forall a b. (a -> b) -> a -> b
$ [Char]
"ctorTy: type " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp SpecType
t [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" doesn't have top-level data constructor"
ctorTy CGEnv
_ (LitAlt Literal
c) SpecType
_ = SpecType -> CG SpecType
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (SpecType -> CG SpecType) -> SpecType -> CG SpecType
forall a b. (a -> b) -> a -> b
$ ReftV Symbol -> RReft
forall r v. r -> UReftV v r
uTop (ReftV Symbol -> RReft)
-> RTypeV Symbol RTyCon RTyVar (ReftV Symbol) -> SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Literal -> RTypeV Symbol RTyCon RTyVar (ReftV Symbol)
literalFRefType Literal
c
ctorTy CGEnv
_ AltCon
DEFAULT SpecType
t = SpecType -> CG SpecType
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
t

unapply :: CGEnv -> F.Symbol -> SpecType -> [Var] -> SpecType -> CoreExpr -> String -> CG (CGEnv, CoreExpr)
unapply :: CGEnv
-> Symbol
-> SpecType
-> [Var]
-> SpecType
-> CoreExpr
-> [Char]
-> CG (CGEnv, CoreExpr)
unapply CGEnv
γ Symbol
y SpecType
yt (Var
z : [Var]
zs) (RFun Symbol
x RFInfo
_ SpecType
s SpecType
t RReft
_) CoreExpr
e [Char]
suffix = do
  γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"unapply arg", Symbol
evar, SpecType
s)
  unapply γ' y yt zs (t `F.subst1` (x, F.EVar evar)) e' suffix
  where
    z' :: Var
z' = [Char] -> Var -> Var
mkCopyWithSuffix [Char]
suffix Var
z
    evar :: Symbol
evar = Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
z'
    e' :: CoreExpr
e' = Var -> Var -> CoreExpr -> CoreExpr
subVarAndTy Var
z Var
z' CoreExpr
e
unapply CGEnv
_ Symbol
_ SpecType
_ (Var
_ : [Var]
_) SpecType
t CoreExpr
_ [Char]
_ = [Char] -> CG (CGEnv, CoreExpr)
forall a. [Char] -> a
F.panic ([Char] -> CG (CGEnv, CoreExpr)) -> [Char] -> CG (CGEnv, CoreExpr)
forall a b. (a -> b) -> a -> b
$ [Char]
"can't unapply type " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp SpecType
t
unapply CGEnv
γ Symbol
y SpecType
yt [] SpecType
t CoreExpr
e [Char]
_ = do
  let yt' :: SpecType
yt' = SpecType
t SpecType -> SpecType -> SpecType
forall r. Reftable r => r -> r -> r
`meet` SpecType
yt
  γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"unapply res", Symbol
y, SpecType
yt')
  return $ traceWhenLoud ("SCRUTINEE " ++ F.showpp (y, yt')) (γ', e)

instantiateTys :: SpecType -> [SpecType] -> SpecType
instantiateTys :: SpecType -> [SpecType] -> SpecType
instantiateTys = (SpecType -> SpecType -> SpecType)
-> SpecType -> [SpecType] -> SpecType
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' SpecType -> SpecType -> SpecType
forall {tv} {c} {r}.
(Hashable tv, TyConable c, FreeVar 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 ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())), PPrint tv,
 PPrint c, PPrint r, Reftable r, Reftable (RTProp c tv r),
 Reftable (RTProp c tv ())) =>
RTypeV Symbol c tv r
-> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
go
 where
  go :: RTypeV Symbol c tv r
-> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
go (RAllT RTVar tv (RType c tv ())
α RTypeV Symbol c tv r
tbody r
_) RTypeV Symbol c tv r
t = (tv, RTypeV Symbol c tv r)
-> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
(tv, RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarMeet' (RTVar tv (RType c tv ()) -> tv
forall tv s. RTVar tv s -> tv
ty_var_value RTVar tv (RType c tv ())
α, RTypeV Symbol c tv r
t) RTypeV Symbol c tv r
tbody
  go RTypeV Symbol c tv r
tbody             RTypeV Symbol c tv r
t =
    [Char] -> RTypeV Symbol c tv r
forall a. [Char] -> a
F.panic ([Char] -> RTypeV Symbol c tv r) -> [Char] -> RTypeV Symbol c tv r
forall a b. (a -> b) -> a -> b
$ [Char]
"instantiateTys: non-polymorphic type " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ RTypeV Symbol c tv r -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp RTypeV Symbol c tv r
tbody [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" to instantiate with " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ RTypeV Symbol c tv r -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp RTypeV Symbol c tv r
t

--------------------------------------------------------------
-- Core Synthesis Rules --------------------------------------
--------------------------------------------------------------

consRelSynth :: CGEnv -> PrEnv -> CoreExpr -> CoreExpr -> CG (SpecType, SpecType, [F.Expr])
consRelSynth :: CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
consRelSynth CGEnv
γ [RelPred]
ψ (Tick CoreTickish
tt CoreExpr
e) CoreExpr
d =
  CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
consRelSynth (CGEnv
γ CGEnv -> Span -> CGEnv
`setLocation` CoreTickish -> Span
Sp.Tick CoreTickish
tt) [RelPred]
ψ CoreExpr
e CoreExpr
d

consRelSynth CGEnv
γ [RelPred]
ψ CoreExpr
e (Tick CoreTickish
tt CoreExpr
d) =
  CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
consRelSynth (CGEnv
γ CGEnv -> Span -> CGEnv
`setLocation` CoreTickish -> Span
Sp.Tick CoreTickish
tt) [RelPred]
ψ CoreExpr
e CoreExpr
d

consRelSynth CGEnv
γ [RelPred]
ψ a1 :: CoreExpr
a1@(App CoreExpr
e1 CoreExpr
d1) CoreExpr
e2 | Type Type
t1 <- CoreExpr -> CoreExpr
GM.unTickExpr CoreExpr
d1 =
  [Char]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
-> CG (SpecType, SpecType, [Expr])
forall e d a b c.
(PPrint e, PPrint d, PPrint a, PPrint b, PPrint c) =>
[Char] -> e -> d -> CG (a, b, c) -> CG (a, b, c)
traceSyn [Char]
"App Ty L" CoreExpr
a1 CoreExpr
e2 (CG (SpecType, SpecType, [Expr])
 -> CG (SpecType, SpecType, [Expr]))
-> CG (SpecType, SpecType, [Expr])
-> CG (SpecType, SpecType, [Expr])
forall a b. (a -> b) -> a -> b
$ do
    (ft1', t2, ps) <- CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
consRelSynth CGEnv
γ [RelPred]
ψ CoreExpr
e1 CoreExpr
e2
    let (α1, ft1, _) = unRAllT ft1' "consRelSynth App Ty L"
    t1' <- trueTy (typeclass (getConfig γ)) t1
    return (subsTyVarMeet' (ty_var_value α1, t1') ft1, t2, ps)

consRelSynth CGEnv
γ [RelPred]
ψ CoreExpr
e1 a2 :: CoreExpr
a2@(App CoreExpr
e2 CoreExpr
d2) | Type Type
t2 <- CoreExpr -> CoreExpr
GM.unTickExpr CoreExpr
d2 =
  [Char]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
-> CG (SpecType, SpecType, [Expr])
forall e d a b c.
(PPrint e, PPrint d, PPrint a, PPrint b, PPrint c) =>
[Char] -> e -> d -> CG (a, b, c) -> CG (a, b, c)
traceSyn [Char]
"App Ty R" CoreExpr
e1 CoreExpr
a2 (CG (SpecType, SpecType, [Expr])
 -> CG (SpecType, SpecType, [Expr]))
-> CG (SpecType, SpecType, [Expr])
-> CG (SpecType, SpecType, [Expr])
forall a b. (a -> b) -> a -> b
$ do
    (t1, ft2', ps) <- CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
consRelSynth CGEnv
γ [RelPred]
ψ CoreExpr
e1 CoreExpr
e2
    let (α2, ft2, _) = unRAllT ft2' "consRelSynth App Ty R"
    t2' <- trueTy (typeclass (getConfig γ)) t2
    return (t1, subsTyVarMeet' (ty_var_value α2, t2') ft2, ps)

consRelSynth CGEnv
γ [RelPred]
ψ a1 :: CoreExpr
a1@(App CoreExpr
e1 CoreExpr
d1) a2 :: CoreExpr
a2@(App CoreExpr
e2 CoreExpr
d2) = [Char]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
-> CG (SpecType, SpecType, [Expr])
forall e d a b c.
(PPrint e, PPrint d, PPrint a, PPrint b, PPrint c) =>
[Char] -> e -> d -> CG (a, b, c) -> CG (a, b, c)
traceSyn [Char]
"App Exp Exp" CoreExpr
a1 CoreExpr
a2 (CG (SpecType, SpecType, [Expr])
 -> CG (SpecType, SpecType, [Expr]))
-> CG (SpecType, SpecType, [Expr])
-> CG (SpecType, SpecType, [Expr])
forall a b. (a -> b) -> a -> b
$ do
  (ft1, ft2, fps) <- CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
consRelSynth CGEnv
γ [RelPred]
ψ CoreExpr
e1 CoreExpr
e2
  (t1, t2, ps) <- consRelSynthApp γ ψ ft1 ft2 fps d1 d2
  return (t1, t2, ps)

consRelSynth CGEnv
γ [RelPred]
ψ CoreExpr
e CoreExpr
d = [Char]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
-> CG (SpecType, SpecType, [Expr])
forall e d a b c.
(PPrint e, PPrint d, PPrint a, PPrint b, PPrint c) =>
[Char] -> e -> d -> CG (a, b, c) -> CG (a, b, c)
traceSyn [Char]
"Unary" CoreExpr
e CoreExpr
d (CG (SpecType, SpecType, [Expr])
 -> CG (SpecType, SpecType, [Expr]))
-> CG (SpecType, SpecType, [Expr])
-> CG (SpecType, SpecType, [Expr])
forall a b. (a -> b) -> a -> b
$ do
  t <- CGEnv -> CoreExpr -> CG SpecType
consUnarySynth CGEnv
γ CoreExpr
e CG SpecType -> (SpecType -> CG SpecType) -> CG SpecType
forall a b.
StateT CGInfo Identity a
-> (a -> StateT CGInfo Identity b) -> StateT CGInfo Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SpecType -> CG SpecType
forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshTy
  s <- consUnarySynth γ d >>= refreshTy
  let ps = [RelPred] -> CoreExpr -> CoreExpr -> SpecType -> SpecType -> [Expr]
lookupRelSig [RelPred]
ψ CoreExpr
e CoreExpr
d SpecType
t SpecType
s
  return (t, s, traceWhenLoud ("consRelSynth Unary synthed preds:" ++ F.showpp ps) ps)

lookupRelSig :: PrEnv -> CoreExpr -> CoreExpr -> SpecType -> SpecType -> [F.Expr]
lookupRelSig :: [RelPred] -> CoreExpr -> CoreExpr -> SpecType -> SpecType -> [Expr]
lookupRelSig [RelPred]
ψ (Var Var
x1) (Var Var
x2) SpecType
t1 SpecType
t2 = (RelPred -> [Expr]) -> [RelPred] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap RelPred -> [Expr]
match [RelPred]
ψ
  where
    match :: RelPred -> [F.Expr]
    match :: RelPred -> [Expr]
match (RelPred Var
f1 Var
f2 [(Symbol, [Symbol])]
bs1 [(Symbol, [Symbol])]
bs2 RelExpr
p) | Var
f1 Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
x1, Var
f2 Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
x2 =
        let ([Symbol]
vs1, [SpecType]
ts1') = SpecType -> ([Symbol], [SpecType])
vargs SpecType
t1
            ([Symbol]
vs2, [SpecType]
ts2') = SpecType -> ([Symbol], [SpecType])
vargs SpecType
t2
            vs1' :: [Symbol]
vs1' = (SpecType -> [Symbol]) -> [SpecType] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (([Symbol], [SpecType]) -> [Symbol]
forall a b. (a, b) -> a
fst (([Symbol], [SpecType]) -> [Symbol])
-> (SpecType -> ([Symbol], [SpecType])) -> SpecType -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> ([Symbol], [SpecType])
vargs) [SpecType]
ts1'
            vs2' :: [Symbol]
vs2' = (SpecType -> [Symbol]) -> [SpecType] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (([Symbol], [SpecType]) -> [Symbol]
forall a b. (a, b) -> a
fst (([Symbol], [SpecType]) -> [Symbol])
-> (SpecType -> ([Symbol], [SpecType])) -> SpecType -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> ([Symbol], [SpecType])
vargs) [SpecType]
ts2'
            bs1' :: [Symbol]
bs1' = ((Symbol, [Symbol]) -> [Symbol])
-> [(Symbol, [Symbol])] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Symbol, [Symbol]) -> [Symbol]
forall a b. (a, b) -> b
snd [(Symbol, [Symbol])]
bs1
            bs2' :: [Symbol]
bs2' = ((Symbol, [Symbol]) -> [Symbol])
-> [(Symbol, [Symbol])] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Symbol, [Symbol]) -> [Symbol]
forall a b. (a, b) -> b
snd [(Symbol, [Symbol])]
bs2
            bs2vs :: Subst
bs2vs = [(Symbol, Expr)] -> Subst
F.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 (((Symbol, [Symbol]) -> Symbol) -> [(Symbol, [Symbol])] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, [Symbol]) -> Symbol
forall a b. (a, b) -> a
fst [(Symbol, [Symbol])]
bs1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ ((Symbol, [Symbol]) -> Symbol) -> [(Symbol, [Symbol])] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, [Symbol]) -> Symbol
forall a b. (a, b) -> a
fst [(Symbol, [Symbol])]
bs2 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol]
bs1' [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol]
bs2') ([Expr] -> [(Symbol, Expr)]) -> [Expr] -> [(Symbol, Expr)]
forall a b. (a -> b) -> a -> b
$ (Symbol -> Expr) -> [Symbol] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> Expr
forall v. v -> ExprV v
F.EVar ([Symbol]
vs1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol]
vs2 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol]
vs1' [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol]
vs2')
          in [Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
F.subst Subst
bs2vs (RelExpr -> Expr
fromRelExpr RelExpr
p)]
    match RelPred
_ = []
lookupRelSig [RelPred]
_ CoreExpr
_ CoreExpr
_ SpecType
_ SpecType
_ = []

consRelSynthApp :: CGEnv -> PrEnv -> SpecType -> SpecType ->
  [F.Expr] -> CoreExpr -> CoreExpr -> CG (SpecType, SpecType, [F.Expr])
consRelSynthApp :: CGEnv
-> [RelPred]
-> SpecType
-> SpecType
-> [Expr]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
consRelSynthApp CGEnv
γ [RelPred]
ψ SpecType
ft1 SpecType
ft2 [Expr]
ps CoreExpr
e1 (Tick CoreTickish
_ CoreExpr
e2) =
  CGEnv
-> [RelPred]
-> SpecType
-> SpecType
-> [Expr]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
consRelSynthApp CGEnv
γ [RelPred]
ψ SpecType
ft1 SpecType
ft2 [Expr]
ps CoreExpr
e1 CoreExpr
e2
consRelSynthApp CGEnv
γ [RelPred]
ψ SpecType
ft1 SpecType
ft2 [Expr]
ps (Tick CoreTickish
t1 CoreExpr
e1) CoreExpr
e2 =
  CGEnv
-> [RelPred]
-> SpecType
-> SpecType
-> [Expr]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
consRelSynthApp (CGEnv
γ CGEnv -> Span -> CGEnv
`setLocation` CoreTickish -> Span
Sp.Tick CoreTickish
t1) [RelPred]
ψ SpecType
ft1 SpecType
ft2 [Expr]
ps CoreExpr
e1 CoreExpr
e2

consRelSynthApp CGEnv
γ [RelPred]
ψ ft1 :: SpecType
ft1@(RFun Symbol
v1 RFInfo
_ SpecType
s1 SpecType
t1 RReft
r1) ft2 :: SpecType
ft2@(RFun Symbol
v2 RFInfo
_ SpecType
s2 SpecType
t2 RReft
r2) ps :: [Expr]
ps@[F.PImp Expr
q Expr
p] d1 :: CoreExpr
d1@(Var Var
x1) d2 :: CoreExpr
d2@(Var Var
x2)
  = SpecType
-> SpecType
-> [Expr]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
-> CG (SpecType, SpecType, [Expr])
forall e d a b c t.
(PPrint e, PPrint d, PPrint a, PPrint b, PPrint c) =>
e -> d -> a -> b -> c -> t -> t
traceSynApp SpecType
ft1 SpecType
ft2 [Expr]
ps CoreExpr
d1 CoreExpr
d2 (CG (SpecType, SpecType, [Expr])
 -> CG (SpecType, SpecType, [Expr]))
-> CG (SpecType, SpecType, [Expr])
-> CG (SpecType, SpecType, [Expr])
forall a b. (a -> b) -> a -> b
$ do
    CGEnv -> RReft -> RReft -> [Char] -> CG ()
entlFunRefts CGEnv
γ RReft
r1 RReft
r2 [Char]
"consRelSynthApp HO"
    let qsubst :: a -> a
qsubst = Subst -> a -> a
forall a. Subable a => Subst -> a -> a
F.subst (Subst -> a -> a) -> Subst -> a -> a
forall a b. (a -> b) -> a -> b
$ [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
v1, Symbol -> Expr
forall v. v -> ExprV v
F.EVar Symbol
resL), (Symbol
v2, Symbol -> Expr
forall v. v -> ExprV v
F.EVar Symbol
resR)]
    CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
consRelCheck CGEnv
γ [RelPred]
ψ CoreExpr
d1 CoreExpr
d2 SpecType
s1 SpecType
s2 (Expr -> Expr
forall {a}. Subable a => a -> a
qsubst Expr
q)
    let subst :: a -> a
subst = Subst -> a -> a
forall a. Subable a => Subst -> a -> a
F.subst (Subst -> a -> a) -> Subst -> a -> a
forall a b. (a -> b) -> a -> b
$ [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
v1, Symbol -> Expr
forall v. v -> ExprV v
F.EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x1), (Symbol
v2, Symbol -> Expr
forall v. v -> ExprV v
F.EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x2)]
    (SpecType, SpecType, [Expr]) -> CG (SpecType, SpecType, [Expr])
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (SpecType -> SpecType
forall {a}. Subable a => a -> a
subst SpecType
t1, SpecType -> SpecType
forall {a}. Subable a => a -> a
subst SpecType
t2, [(Expr -> Expr
forall {a}. Subable a => a -> a
subst (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol -> Expr -> Expr
unapplyRelArgs Symbol
v1 Symbol
v2) Expr
p])
consRelSynthApp CGEnv
γ [RelPred]
ψ ft1 :: SpecType
ft1@(RFun Symbol
v1 RFInfo
_ SpecType
s1 SpecType
t1 RReft
r1) ft2 :: SpecType
ft2@(RFun Symbol
v2 RFInfo
_ SpecType
s2 SpecType
t2 RReft
r2) ps :: [Expr]
ps@[] d1 :: CoreExpr
d1@(Var Var
x1) d2 :: CoreExpr
d2@(Var Var
x2)
  = SpecType
-> SpecType
-> [Expr]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
-> CG (SpecType, SpecType, [Expr])
forall e d a b c t.
(PPrint e, PPrint d, PPrint a, PPrint b, PPrint c) =>
e -> d -> a -> b -> c -> t -> t
traceSynApp SpecType
ft1 SpecType
ft2 [Expr]
ps CoreExpr
d1 CoreExpr
d2 (CG (SpecType, SpecType, [Expr])
 -> CG (SpecType, SpecType, [Expr]))
-> CG (SpecType, SpecType, [Expr])
-> CG (SpecType, SpecType, [Expr])
forall a b. (a -> b) -> a -> b
$ do
    CGEnv -> RReft -> RReft -> [Char] -> CG ()
entlFunRefts CGEnv
γ RReft
r1 RReft
r2 [Char]
"consRelSynthApp FO"
    CGEnv -> CoreExpr -> SpecType -> CG ()
consUnaryCheck CGEnv
γ CoreExpr
d1 SpecType
s1
    CGEnv -> CoreExpr -> SpecType -> CG ()
consUnaryCheck CGEnv
γ CoreExpr
d2 SpecType
s2
    (_, _, qs) <- CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
consRelSynth CGEnv
γ [RelPred]
ψ CoreExpr
d1 CoreExpr
d2
    let subst =
          Subst -> a -> a
forall a. Subable a => Subst -> a -> a
F.subst (Subst -> a -> a) -> Subst -> a -> a
forall a b. (a -> b) -> a -> b
$ [(Symbol, Expr)] -> Subst
F.mkSubst
            [(Symbol
v1, Symbol -> Expr
forall v. v -> ExprV v
F.EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x1), (Symbol
v2, Symbol -> Expr
forall v. v -> ExprV v
F.EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x2)]
    return (subst t1, subst t2, map subst qs)
consRelSynthApp CGEnv
_ [RelPred]
_ RFun{} RFun{} [Expr]
ps d1 :: CoreExpr
d1@(Var Var
_) d2 :: CoreExpr
d2@(Var Var
_)
  = [Char] -> CG (SpecType, SpecType, [Expr])
forall a. [Char] -> a
F.panic ([Char] -> CG (SpecType, SpecType, [Expr]))
-> [Char] -> CG (SpecType, SpecType, [Expr])
forall a b. (a -> b) -> a -> b
$ [Char]
"consRelSynthApp: multiple rel sigs not supported " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ([Expr], CoreExpr, CoreExpr) -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp ([Expr]
ps, CoreExpr
d1, CoreExpr
d2)
consRelSynthApp CGEnv
_ [RelPred]
_ RFun{} RFun{} [Expr]
_ CoreExpr
d1 CoreExpr
d2 =
  [Char] -> CG (SpecType, SpecType, [Expr])
forall a. [Char] -> a
F.panic ([Char] -> CG (SpecType, SpecType, [Expr]))
-> [Char] -> CG (SpecType, SpecType, [Expr])
forall a b. (a -> b) -> a -> b
$ [Char]
"consRelSynthApp: expected application to variables, got" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (CoreExpr, CoreExpr) -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp (CoreExpr
d1, CoreExpr
d2)
consRelSynthApp CGEnv
_ [RelPred]
_ SpecType
t1 SpecType
t2 [Expr]
p CoreExpr
d1 CoreExpr
d2 =
  [Char] -> CG (SpecType, SpecType, [Expr])
forall a. [Char] -> a
F.panic ([Char] -> CG (SpecType, SpecType, [Expr]))
-> [Char] -> CG (SpecType, SpecType, [Expr])
forall a b. (a -> b) -> a -> b
$ [Char]
"consRelSynthApp: malformed function types or predicate for arguments " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (SpecType, SpecType, [Expr], CoreExpr, CoreExpr) -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp (SpecType
t1, SpecType
t2, [Expr]
p, CoreExpr
d1, CoreExpr
d2)

--------------------------------------------------------------
-- Unary Rules -----------------------------------------------
--------------------------------------------------------------

symbolType :: CGEnv -> Var -> String -> SpecType
symbolType :: CGEnv -> Var -> [Char] -> SpecType
symbolType CGEnv
γ Var
x [Char]
msg
  | Just SpecType
t <- CGEnv
γ (?callStack::CallStack) => CGEnv -> Symbol -> Maybe SpecType
CGEnv -> Symbol -> Maybe SpecType
?= Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x = SpecType
t
  | Bool
otherwise = [Char] -> SpecType
forall a. [Char] -> a
F.panic ([Char] -> SpecType) -> [Char] -> SpecType
forall a b. (a -> b) -> a -> b
$ [Char]
msg [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Var -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp Var
x [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" not in scope " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ CGEnv -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp CGEnv
γ

consUnarySynth :: CGEnv -> CoreExpr -> CG SpecType
consUnarySynth :: CGEnv -> CoreExpr -> CG SpecType
consUnarySynth CGEnv
γ (Tick CoreTickish
t CoreExpr
e) = CGEnv -> CoreExpr -> CG SpecType
consUnarySynth (CGEnv
γ CGEnv -> Span -> CGEnv
`setLocation` CoreTickish -> Span
Sp.Tick CoreTickish
t) CoreExpr
e
consUnarySynth CGEnv
γ (Var Var
x) = SpecType -> CG SpecType
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (SpecType -> CG SpecType) -> SpecType -> CG SpecType
forall a b. (a -> b) -> a -> b
$ [Char] -> (SpecType -> SpecType) -> SpecType -> SpecType
forall a. [Char] -> a -> a
traceWhenLoud ([Char]
"SELFIFICATION " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (Var, SpecType) -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp (Var
x, SpecType -> SpecType
removeAbsRef (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ SpecType -> Var -> SpecType
forall a. Symbolic a => SpecType -> a -> SpecType
selfify SpecType
t Var
x)) SpecType -> SpecType
removeAbsRef (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ SpecType -> Var -> SpecType
forall a. Symbolic a => SpecType -> a -> SpecType
selfify SpecType
t Var
x
  where t :: SpecType
t = CGEnv -> Var -> [Char] -> SpecType
symbolType CGEnv
γ Var
x [Char]
"consUnarySynth (Var)"
consUnarySynth CGEnv
_ e :: CoreExpr
e@(Lit Literal
c) =
  [Char] -> CoreExpr -> CG SpecType -> CG SpecType
forall e a. (PPrint e, PPrint a) => [Char] -> e -> CG a -> CG a
traceUSyn [Char]
"Lit" CoreExpr
e (CG SpecType -> CG SpecType) -> CG SpecType -> CG SpecType
forall a b. (a -> b) -> a -> b
$ do
  SpecType -> CG SpecType
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (SpecType -> CG SpecType) -> SpecType -> CG SpecType
forall a b. (a -> b) -> a -> b
$ SpecType -> SpecType
removeAbsRef (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ RTypeV Symbol RTyCon RTyVar (ReftV Symbol) -> SpecType
forall c tv a. RType c tv a -> RType c tv (UReft a)
uRType (RTypeV Symbol RTyCon RTyVar (ReftV Symbol) -> SpecType)
-> RTypeV Symbol RTyCon RTyVar (ReftV Symbol) -> SpecType
forall a b. (a -> b) -> a -> b
$ Literal -> RTypeV Symbol RTyCon RTyVar (ReftV Symbol)
literalFRefType Literal
c
consUnarySynth CGEnv
γ e :: CoreExpr
e@(Let CoreBind
_ CoreExpr
_) =
  [Char] -> CoreExpr -> CG SpecType -> CG SpecType
forall e a. (PPrint e, PPrint a) => [Char] -> e -> CG a -> CG a
traceUSyn [Char]
"Let" CoreExpr
e (CG SpecType -> CG SpecType) -> CG SpecType -> CG SpecType
forall a b. (a -> b) -> a -> b
$ do
  t   <- Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyType (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) KVKind
LetE CoreExpr
e (Type -> CG SpecType) -> Type -> CG SpecType
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => CoreExpr -> Type
CoreExpr -> Type
Ghc.exprType CoreExpr
e
  addW $ WfC γ t
  consUnaryCheck γ e t
  return $ removeAbsRef t
consUnarySynth CGEnv
γ e' :: CoreExpr
e'@(App CoreExpr
e CoreExpr
d) =
  [Char] -> CoreExpr -> CG SpecType -> CG SpecType
forall e a. (PPrint e, PPrint a) => [Char] -> e -> CG a -> CG a
traceUSyn [Char]
"App" CoreExpr
e' (CG SpecType -> CG SpecType) -> CG SpecType -> CG SpecType
forall a b. (a -> b) -> a -> b
$ do
  et <- CGEnv -> CoreExpr -> CG SpecType
consUnarySynth CGEnv
γ CoreExpr
e
  consUnarySynthApp γ et d
consUnarySynth CGEnv
γ e' :: CoreExpr
e'@(Lam Var
α CoreExpr
e) | Var -> Bool
Ghc.isTyVar Var
α =
                             [Char] -> CoreExpr -> CG SpecType -> CG SpecType
forall e a. (PPrint e, PPrint a) => [Char] -> e -> CG a -> CG a
traceUSyn [Char]
"LamTyp" CoreExpr
e' (CG SpecType -> CG SpecType) -> CG SpecType -> CG SpecType
forall a b. (a -> b) -> a -> b
$ do
  γ' <- CGEnv
γ CGEnv -> Var -> CG CGEnv
`extendWithTyVar` Var
α
  t' <- consUnarySynth γ' e
  return $ removeAbsRef $ RAllT (makeRTVar $ rTyVar α) t' mempty
consUnarySynth CGEnv
γ e :: CoreExpr
e@(Lam Var
x CoreExpr
d)  =
  [Char] -> CoreExpr -> CG SpecType -> CG SpecType
forall e a. (PPrint e, PPrint a) => [Char] -> e -> CG a -> CG a
traceUSyn [Char]
"Lam" CoreExpr
e (CG SpecType -> CG SpecType) -> CG SpecType -> CG SpecType
forall a b. (a -> b) -> a -> b
$ do
  let Ghc.FunTy { ft_arg :: Type -> Type
ft_arg = Type
s' } = CoreExpr -> Type -> Type
checkFun CoreExpr
e (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => CoreExpr -> Type
CoreExpr -> Type
Ghc.exprType CoreExpr
e
  s  <- Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyType (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) KVKind
LamE (Var -> CoreExpr
forall b. Var -> Expr b
Var Var
x) Type
s'
  γ' <- γ += ("consUnarySynth (Lam)", F.symbol x, s)
  t  <- consUnarySynth γ' d
  addW $ WfC γ s
  return $ removeAbsRef $ RFun (F.symbol x) (mkRFInfo $ getConfig γ) s t mempty
consUnarySynth CGEnv
γ e :: CoreExpr
e@(Case CoreExpr
_ Var
_ Type
_ [Alt Var]
alts) =
  [Char] -> CoreExpr -> CG SpecType -> CG SpecType
forall e a. (PPrint e, PPrint a) => [Char] -> e -> CG a -> CG a
traceUSyn [Char]
"Case" CoreExpr
e (CG SpecType -> CG SpecType) -> CG SpecType -> CG SpecType
forall a b. (a -> b) -> a -> b
$ do
  t   <- Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyType (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) ([Alt Var] -> KVKind
caseKVKind [Alt Var]
alts) CoreExpr
e (Type -> CG SpecType) -> Type -> CG SpecType
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => CoreExpr -> Type
CoreExpr -> Type
Ghc.exprType CoreExpr
e
  addW $ WfC γ t
  return $ removeAbsRef t
consUnarySynth CGEnv
_ e :: CoreExpr
e@(Cast CoreExpr
_ CoercionR
_) = [Char] -> CG SpecType
forall a. [Char] -> a
F.panic ([Char] -> CG SpecType) -> [Char] -> CG SpecType
forall a b. (a -> b) -> a -> b
$ [Char]
"consUnarySynth is undefined for Cast " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ CoreExpr -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp CoreExpr
e
consUnarySynth CGEnv
_ e :: CoreExpr
e@(Type Type
_) = [Char] -> CG SpecType
forall a. [Char] -> a
F.panic ([Char] -> CG SpecType) -> [Char] -> CG SpecType
forall a b. (a -> b) -> a -> b
$ [Char]
"consUnarySynth is undefined for Type " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ CoreExpr -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp CoreExpr
e
consUnarySynth CGEnv
_ e :: CoreExpr
e@(Coercion CoercionR
_) = [Char] -> CG SpecType
forall a. [Char] -> a
F.panic ([Char] -> CG SpecType) -> [Char] -> CG SpecType
forall a b. (a -> b) -> a -> b
$ [Char]
"consUnarySynth is undefined for Coercion " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ CoreExpr -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp CoreExpr
e

caseKVKind :: [Alt Var] -> KVKind
caseKVKind :: [Alt Var] -> KVKind
caseKVKind [Ghc.Alt (DataAlt DataCon
_) [Var]
_ (Var Var
_)] = KVKind
ProjectE
caseKVKind [Alt Var]
cs                      = Int -> KVKind
CaseE ([Alt Var] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Alt Var]
cs)

checkFun :: CoreExpr -> Type -> Type
checkFun :: CoreExpr -> Type -> Type
checkFun CoreExpr
_ t :: Type
t@Ghc.FunTy{} = Type
t
checkFun CoreExpr
e Type
t = [Char] -> Type
forall a. [Char] -> a
F.panic ([Char] -> Type) -> [Char] -> Type
forall a b. (a -> b) -> a -> b
$ [Char]
"FunTy was expected but got " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp Type
t [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\t for expression" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ CoreExpr -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp CoreExpr
e

base :: SpecType -> Bool
base :: SpecType -> Bool
base RApp{} = Bool
True
base RVar{} = Bool
True
base SpecType
_      = Bool
False

selfifyExpr :: SpecType -> F.Expr -> Maybe SpecType
selfifyExpr :: SpecType -> Expr -> Maybe SpecType
selfifyExpr (RFun Symbol
v RFInfo
i SpecType
s SpecType
t RReft
r) Expr
f = (\SpecType
t' -> Symbol -> RFInfo -> SpecType -> SpecType -> RReft -> SpecType
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
v RFInfo
i SpecType
s SpecType
t' RReft
r) (SpecType -> SpecType) -> Maybe SpecType -> Maybe SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType -> Expr -> Maybe SpecType
selfifyExpr SpecType
t (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
F.EApp Expr
f (Symbol -> Expr
forall v. v -> ExprV v
F.EVar Symbol
v))
selfifyExpr SpecType
t Expr
e | SpecType -> Bool
base SpecType
t = SpecType -> Maybe SpecType
forall a. a -> Maybe a
Just (SpecType -> Maybe SpecType) -> SpecType -> Maybe SpecType
forall a b. (a -> b) -> a -> b
$ SpecType
t SpecType -> RReft -> SpecType
forall r v c tv.
Reftable r =>
RTypeV v c tv r -> r -> RTypeV v c tv r
`strengthen` Expr -> RReft
forall {a} {v}. Expression a => a -> UReftV v (ReftV Symbol)
eq Expr
e
  where eq :: a -> UReftV v (ReftV Symbol)
eq = ReftV Symbol -> UReftV v (ReftV Symbol)
forall r v. r -> UReftV v r
uTop (ReftV Symbol -> UReftV v (ReftV Symbol))
-> (a -> ReftV Symbol) -> a -> UReftV v (ReftV Symbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ReftV Symbol
forall a. Expression a => a -> ReftV Symbol
F.exprReft
selfifyExpr SpecType
_ Expr
_ = Maybe SpecType
forall a. Maybe a
Nothing

selfify :: F.Symbolic a => SpecType -> a -> SpecType
selfify :: forall a. Symbolic a => SpecType -> a -> SpecType
selfify SpecType
t a
x | SpecType -> Bool
base SpecType
t = SpecType
t SpecType -> RReft -> SpecType
forall r v c tv.
Reftable r =>
RTypeV v c tv r -> r -> RTypeV v c tv r
`strengthen` a -> RReft
forall {a} {v}. Symbolic a => a -> UReftV v (ReftV Symbol)
eq a
x
  where eq :: a -> UReftV v (ReftV Symbol)
eq = ReftV Symbol -> UReftV v (ReftV Symbol)
forall r v. r -> UReftV v r
uTop (ReftV Symbol -> UReftV v (ReftV Symbol))
-> (a -> ReftV Symbol) -> a -> UReftV v (ReftV Symbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> ReftV Symbol
forall a. Symbolic a => a -> ReftV Symbol
F.symbolReft (Symbol -> ReftV Symbol) -> (a -> Symbol) -> a -> ReftV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol
selfify SpecType
t a
e | Just SpecType
t' <- SpecType -> Expr -> Maybe SpecType
selfifyExpr SpecType
t (Symbol -> Expr
forall v. v -> ExprV v
F.EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol a
e) = SpecType
t'
selfify SpecType
t a
_ = SpecType
t

consUnarySynthApp :: CGEnv -> SpecType -> CoreExpr -> CG SpecType
consUnarySynthApp :: CGEnv -> SpecType -> CoreExpr -> CG SpecType
consUnarySynthApp CGEnv
γ SpecType
t (Tick CoreTickish
y CoreExpr
e) = do
  CGEnv -> SpecType -> CoreExpr -> CG SpecType
consUnarySynthApp (CGEnv
γ CGEnv -> Span -> CGEnv
`setLocation` CoreTickish -> Span
Sp.Tick CoreTickish
y) SpecType
t CoreExpr
e
consUnarySynthApp CGEnv
γ (RFun Symbol
x RFInfo
_ SpecType
s SpecType
t RReft
_) d :: CoreExpr
d@(Var Var
y) = do
  CGEnv -> CoreExpr -> SpecType -> CG ()
consUnaryCheck CGEnv
γ CoreExpr
d SpecType
s
  SpecType -> CG SpecType
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (SpecType -> CG SpecType) -> SpecType -> CG SpecType
forall a b. (a -> b) -> a -> b
$ SpecType
t SpecType -> (Symbol, Expr) -> SpecType
forall a. Subable a => a -> (Symbol, Expr) -> a
`F.subst1` (Symbol
x, Symbol -> Expr
forall v. v -> ExprV v
F.EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
y)
consUnarySynthApp CGEnv
γ (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
α SpecType
t RReft
_) (Type Type
s) = do
    s' <- Bool -> Type -> CG SpecType
trueTy (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) Type
s
    return $ subsTyVarMeet' (ty_var_value α, s') t
consUnarySynthApp CGEnv
_ RFun{} CoreExpr
d =
  [Char] -> CG SpecType
forall a. [Char] -> a
F.panic ([Char] -> CG SpecType) -> [Char] -> CG SpecType
forall a b. (a -> b) -> a -> b
$ [Char]
"consUnarySynthApp expected Var as a funciton arg, got " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ CoreExpr -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp CoreExpr
d
consUnarySynthApp CGEnv
γ t :: SpecType
t@(RAllP{}) CoreExpr
e
  = CGEnv -> SpecType -> CoreExpr -> CG SpecType
consUnarySynthApp CGEnv
γ (SpecType -> SpecType
removeAbsRef SpecType
t) CoreExpr
e

consUnarySynthApp CGEnv
_ SpecType
ft CoreExpr
d =
  [Char] -> CG SpecType
forall a. [Char] -> a
F.panic ([Char] -> CG SpecType) -> [Char] -> CG SpecType
forall a b. (a -> b) -> a -> b
$ [Char]
"consUnarySynthApp malformed function type " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp SpecType
ft [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++
            [Char]
" for argument " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ CoreExpr -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp CoreExpr
d

consUnaryCheck :: CGEnv -> CoreExpr -> SpecType -> CG ()
consUnaryCheck :: CGEnv -> CoreExpr -> SpecType -> CG ()
consUnaryCheck CGEnv
γ (Let (NonRec Var
x CoreExpr
d) CoreExpr
e) SpecType
t = do
  s <- CGEnv -> CoreExpr -> CG SpecType
consUnarySynth CGEnv
γ CoreExpr
d
  γ' <- γ += ("consUnaryCheck Let", F.symbol x, s)
  consUnaryCheck γ' e t
consUnaryCheck CGEnv
γ CoreExpr
e SpecType
t = do
  s <- CGEnv -> CoreExpr -> CG SpecType
consUnarySynth CGEnv
γ CoreExpr
e
  addC (SubC γ s t) ("consUnaryCheck (Synth): s = " ++ F.showpp s ++ " t = " ++ F.showpp t)

--------------------------------------------------------------
-- Rel. Predicate Subtyping  ---------------------------------
--------------------------------------------------------------

consRelSub :: CGEnv -> SpecType -> SpecType -> F.Expr -> F.Expr -> CG ()
consRelSub :: CGEnv -> SpecType -> SpecType -> Expr -> Expr -> CG ()
consRelSub CGEnv
γ f1 :: SpecType
f1@(RFun Symbol
g1 RFInfo
_ s1 :: SpecType
s1@RFun{} SpecType
t1 RReft
_) f2 :: SpecType
f2@(RFun Symbol
g2 RFInfo
_ s2 :: SpecType
s2@RFun{} SpecType
t2 RReft
_)
             pr1 :: Expr
pr1@(F.PImp qr1 :: Expr
qr1@F.PImp{} Expr
p1)  pr2 :: Expr
pr2@(F.PImp qr2 :: Expr
qr2@F.PImp{} Expr
p2)
  = [Char] -> SpecType -> SpecType -> Expr -> Expr -> CG () -> CG ()
forall t s p q a.
(PPrint t, PPrint s, PPrint p, PPrint q) =>
[Char] -> t -> s -> p -> q -> a -> a
traceSub [Char]
"hof" SpecType
f1 SpecType
f2 Expr
pr1 Expr
pr2 (CG () -> CG ()) -> CG () -> CG ()
forall a b. (a -> b) -> a -> b
$ do
    CGEnv -> SpecType -> SpecType -> Expr -> Expr -> CG ()
consRelSub CGEnv
γ SpecType
s1 SpecType
s2 Expr
qr2 Expr
qr1
    γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consRelSub HOF", Symbol -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Symbol
g1, SpecType
s1)
    γ'' <- γ' += ("consRelSub HOF", F.symbol g2, s2)
    let psubst Expr
x = Symbol -> Symbol -> Expr -> Expr
unapplyArg Symbol
resL Symbol
g1 Expr
x Expr -> Expr -> Expr
F.&.& Symbol -> Symbol -> Expr -> Expr
unapplyArg Symbol
resR Symbol
g2 Expr
x
    consRelSub γ'' t1 t2 (psubst p1) (psubst p2)
consRelSub CGEnv
γ f1 :: SpecType
f1@(RFun Symbol
g1 RFInfo
_ s1 :: SpecType
s1@RFun{} SpecType
t1 RReft
_) f2 :: SpecType
f2@(RFun Symbol
g2 RFInfo
_ s2 :: SpecType
s2@RFun{} SpecType
t2 RReft
_)
             pr1 :: Expr
pr1@(F.PAnd [F.PImp qr1 :: Expr
qr1@F.PImp{} Expr
p1])            pr2 :: Expr
pr2@(F.PImp qr2 :: Expr
qr2@F.PImp{} Expr
p2)
  = [Char] -> SpecType -> SpecType -> Expr -> Expr -> CG () -> CG ()
forall t s p q a.
(PPrint t, PPrint s, PPrint p, PPrint q) =>
[Char] -> t -> s -> p -> q -> a -> a
traceSub [Char]
"hof" SpecType
f1 SpecType
f2 Expr
pr1 Expr
pr2 (CG () -> CG ()) -> CG () -> CG ()
forall a b. (a -> b) -> a -> b
$ do
    CGEnv -> SpecType -> SpecType -> Expr -> Expr -> CG ()
consRelSub CGEnv
γ SpecType
s1 SpecType
s2 Expr
qr2 Expr
qr1
    γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consRelSub HOF", Symbol -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Symbol
g1, SpecType
s1)
    γ'' <- γ' += ("consRelSub HOF", F.symbol g2, s2)
    let psubst Expr
x = Symbol -> Symbol -> Expr -> Expr
unapplyArg Symbol
resL Symbol
g1 Expr
x Expr -> Expr -> Expr
F.&.& Symbol -> Symbol -> Expr -> Expr
unapplyArg Symbol
resR Symbol
g2 Expr
x
    consRelSub γ'' t1 t2 (psubst p1) (psubst p2)
consRelSub CGEnv
γ f1 :: SpecType
f1@(RFun Symbol
x1 RFInfo
_ SpecType
s1 SpecType
e1 RReft
_) SpecType
f2 Expr
p1 Expr
p2 =
  [Char] -> SpecType -> SpecType -> Expr -> Expr -> CG () -> CG ()
forall t s p q a.
(PPrint t, PPrint s, PPrint p, PPrint q) =>
[Char] -> t -> s -> p -> q -> a -> a
traceSub [Char]
"fun" SpecType
f1 SpecType
f2 Expr
p1 Expr
p2 (CG () -> CG ()) -> CG () -> CG ()
forall a b. (a -> b) -> a -> b
$ do
    γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consRelSub RFun L", Symbol -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Symbol
x1, SpecType
s1)
    let psubst = Symbol -> Symbol -> Expr -> Expr
unapplyArg Symbol
resL Symbol
x1
    consRelSub γ' e1 f2 (psubst p1) (psubst p2)
consRelSub CGEnv
γ SpecType
f1 f2 :: SpecType
f2@(RFun Symbol
x2 RFInfo
_ SpecType
s2 SpecType
e2 RReft
_) Expr
p1 Expr
p2 =
  [Char] -> SpecType -> SpecType -> Expr -> Expr -> CG () -> CG ()
forall t s p q a.
(PPrint t, PPrint s, PPrint p, PPrint q) =>
[Char] -> t -> s -> p -> q -> a -> a
traceSub [Char]
"fun" SpecType
f1 SpecType
f2 Expr
p1 Expr
p2 (CG () -> CG ()) -> CG () -> CG ()
forall a b. (a -> b) -> a -> b
$ do
    γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consRelSub RFun R", Symbol -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Symbol
x2, SpecType
s2)
    let psubst = Symbol -> Symbol -> Expr -> Expr
unapplyArg Symbol
resR Symbol
x2
    consRelSub γ' f1 e2 (psubst p1) (psubst p2)
consRelSub CGEnv
γ SpecType
t1 SpecType
t2 Expr
p1 Expr
p2 | SpecType -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isBase SpecType
t1 Bool -> Bool -> Bool
&& SpecType -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isBase SpecType
t2 =
  [Char] -> SpecType -> SpecType -> Expr -> Expr -> CG () -> CG ()
forall t s p q a.
(PPrint t, PPrint s, PPrint p, PPrint q) =>
[Char] -> t -> s -> p -> q -> a -> a
traceSub [Char]
"base" SpecType
t1 SpecType
t2 Expr
p1 Expr
p2 (CG () -> CG ()) -> CG () -> CG ()
forall a b. (a -> b) -> a -> b
$ do
    rl <- StateT CGInfo Identity Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh
    rr <- fresh
    γ' <- γ += ("consRelSub Base L", rl, t1)
    γ'' <- γ' += ("consRelSub Base R", rr, t2)
    let cstr = Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
F.subst ([(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
resL, Symbol -> Expr
forall v. v -> ExprV v
F.EVar Symbol
rl), (Symbol
resR, Symbol -> Expr
forall v. v -> ExprV v
F.EVar Symbol
rr)]) (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
F.PImp Expr
p1 Expr
p2
    entl γ'' (traceWhenLoud ("consRelSub Base cstr " ++ F.showpp cstr) cstr) "consRelSub Base"
consRelSub CGEnv
_ t1 :: SpecType
t1@(RHole RReft
_) t2 :: SpecType
t2@(RHole RReft
_) Expr
_ Expr
_ = [Char] -> CG ()
forall a. [Char] -> a
F.panic ([Char] -> CG ()) -> [Char] -> CG ()
forall a b. (a -> b) -> a -> b
$ [Char]
"consRelSub is undefined for RHole " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (SpecType, SpecType) -> [Char]
forall a. Show a => a -> [Char]
show (SpecType
t1, SpecType
t2)
consRelSub CGEnv
_ t1 :: SpecType
t1@(RExprArg Located Expr
_) t2 :: SpecType
t2@(RExprArg Located Expr
_) Expr
_ Expr
_ = [Char] -> CG ()
forall a. [Char] -> a
F.panic ([Char] -> CG ()) -> [Char] -> CG ()
forall a b. (a -> b) -> a -> b
$ [Char]
"consRelSub is undefined for RExprArg " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (SpecType, SpecType) -> [Char]
forall a. Show a => a -> [Char]
show (SpecType
t1, SpecType
t2)
consRelSub CGEnv
_ t1 :: SpecType
t1@REx {} t2 :: SpecType
t2@REx {} Expr
_ Expr
_ = [Char] -> CG ()
forall a. [Char] -> a
F.panic ([Char] -> CG ()) -> [Char] -> CG ()
forall a b. (a -> b) -> a -> b
$ [Char]
"consRelSub is undefined for REx " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (SpecType, SpecType) -> [Char]
forall a. Show a => a -> [Char]
show (SpecType
t1, SpecType
t2)
consRelSub CGEnv
_ t1 :: SpecType
t1@RAllE {} t2 :: SpecType
t2@RAllE {} Expr
_ Expr
_ = [Char] -> CG ()
forall a. [Char] -> a
F.panic ([Char] -> CG ()) -> [Char] -> CG ()
forall a b. (a -> b) -> a -> b
$ [Char]
"consRelSub is undefined for RAllE " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (SpecType, SpecType) -> [Char]
forall a. Show a => a -> [Char]
show (SpecType
t1, SpecType
t2)
consRelSub CGEnv
_ t1 :: SpecType
t1@RRTy {} t2 :: SpecType
t2@RRTy {} Expr
_ Expr
_ = [Char] -> CG ()
forall a. [Char] -> a
F.panic ([Char] -> CG ()) -> [Char] -> CG ()
forall a b. (a -> b) -> a -> b
$ [Char]
"consRelSub is undefined for RRTy " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (SpecType, SpecType) -> [Char]
forall a. Show a => a -> [Char]
show (SpecType
t1, SpecType
t2)
consRelSub CGEnv
_ t1 :: SpecType
t1@RAllP {} t2 :: SpecType
t2@RAllP {} Expr
_ Expr
_ = [Char] -> CG ()
forall a. [Char] -> a
F.panic ([Char] -> CG ()) -> [Char] -> CG ()
forall a b. (a -> b) -> a -> b
$ [Char]
"consRelSub is undefined for RAllP " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (SpecType, SpecType) -> [Char]
forall a. Show a => a -> [Char]
show (SpecType
t1, SpecType
t2)
consRelSub CGEnv
_ t1 :: SpecType
t1@RAllT {} t2 :: SpecType
t2@RAllT {} Expr
_ Expr
_ = [Char] -> CG ()
forall a. [Char] -> a
F.panic ([Char] -> CG ()) -> [Char] -> CG ()
forall a b. (a -> b) -> a -> b
$ [Char]
"consRelSub is undefined for RAllT " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (SpecType, SpecType) -> [Char]
forall a. Show a => a -> [Char]
show (SpecType
t1, SpecType
t2)
consRelSub CGEnv
_ SpecType
t1 SpecType
t2 Expr
_ Expr
_ =  [Char] -> CG ()
forall a. [Char] -> a
F.panic ([Char] -> CG ()) -> [Char] -> CG ()
forall a b. (a -> b) -> a -> b
$ [Char]
"consRelSub is undefined for different types " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (SpecType, SpecType) -> [Char]
forall a. Show a => a -> [Char]
show (SpecType
t1, SpecType
t2)

--------------------------------------------------------------
-- Helper Definitions ----------------------------------------
--------------------------------------------------------------

isFuncPred :: F.Expr -> Bool
isFuncPred :: Expr -> Bool
isFuncPred (F.PImp Expr
_ Expr
_) = Bool
True
isFuncPred Expr
_            = Bool
False

partitionArg :: Var -> Var -> SpecType -> SpecType -> F.Expr -> (PrEnv, [F.Expr])
partitionArg :: Var -> Var -> SpecType -> SpecType -> Expr -> ([RelPred], [Expr])
partitionArg Var
x1 Var
x2 SpecType
s1 SpecType
s2 Expr
q = [Var]
-> [Var]
-> [SpecType]
-> [SpecType]
-> [Expr]
-> ([RelPred], [Expr])
partitionArgs [Var
x1] [Var
x2] [SpecType
s1] [SpecType
s2] [Expr
q]

partitionArgs :: [Var] -> [Var] -> [SpecType] -> [SpecType] -> [F.Expr] -> (PrEnv, [F.Expr])
partitionArgs :: [Var]
-> [Var]
-> [SpecType]
-> [SpecType]
-> [Expr]
-> ([RelPred], [Expr])
partitionArgs [Var]
xs1 [Var]
xs2 [SpecType]
ts1 [SpecType]
ts2 [Expr]
qs = (((Var, Var, SpecType, SpecType, Expr) -> RelPred)
-> [(Var, Var, SpecType, SpecType, Expr)] -> [RelPred]
forall a b. (a -> b) -> [a] -> [b]
map (Var, Var, SpecType, SpecType, Expr) -> RelPred
toRel [(Var, Var, SpecType, SpecType, Expr)]
ho, ((Var, Var, SpecType, SpecType, Expr) -> Expr)
-> [(Var, Var, SpecType, SpecType, Expr)] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Var, Var, SpecType, SpecType, Expr) -> Expr
forall {a} {b} {c} {d} {e}. (a, b, c, d, e) -> e
toUnary [(Var, Var, SpecType, SpecType, Expr)]
fo)
 where
  ([(Var, Var, SpecType, SpecType, Expr)]
ho, [(Var, Var, SpecType, SpecType, Expr)]
fo) = ((Var, Var, SpecType, SpecType, Expr) -> Bool)
-> [(Var, Var, SpecType, SpecType, Expr)]
-> ([(Var, Var, SpecType, SpecType, Expr)],
    [(Var, Var, SpecType, SpecType, Expr)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (Expr -> Bool
isFuncPred (Expr -> Bool)
-> ((Var, Var, SpecType, SpecType, Expr) -> Expr)
-> (Var, Var, SpecType, SpecType, Expr)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, Var, SpecType, SpecType, Expr) -> Expr
forall {a} {b} {c} {d} {e}. (a, b, c, d, e) -> e
toUnary) ([Var]
-> [Var]
-> [SpecType]
-> [SpecType]
-> [Expr]
-> [(Var, Var, SpecType, SpecType, Expr)]
forall t t1 t2 t3 t4.
[t] -> [t1] -> [t2] -> [t3] -> [t4] -> [(t, t1, t2, t3, t4)]
zip5 [Var]
xs1 [Var]
xs2 [SpecType]
ts1 [SpecType]
ts2 [Expr]
qs)
  toRel :: (Var, Var, SpecType, SpecType, Expr) -> RelPred
toRel (Var
f1, Var
f2, SpecType
t1, SpecType
t2, Expr
q) =
    let ([Symbol]
vs1, [SpecType]
ts1') = SpecType -> ([Symbol], [SpecType])
vargs SpecType
t1
    in  let ([Symbol]
vs2, [SpecType]
ts2') = SpecType -> ([Symbol], [SpecType])
vargs SpecType
t2
        in  let bs1 :: [(Symbol, [Symbol])]
bs1 = [Symbol] -> [[Symbol]] -> [(Symbol, [Symbol])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
vs1 (([Symbol], [SpecType]) -> [Symbol]
forall a b. (a, b) -> a
fst (([Symbol], [SpecType]) -> [Symbol])
-> (SpecType -> ([Symbol], [SpecType])) -> SpecType -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> ([Symbol], [SpecType])
vargs (SpecType -> [Symbol]) -> [SpecType] -> [[Symbol]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
ts1')
            in  let bs2 :: [(Symbol, [Symbol])]
bs2 = [Symbol] -> [[Symbol]] -> [(Symbol, [Symbol])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
vs2 (([Symbol], [SpecType]) -> [Symbol]
forall a b. (a, b) -> a
fst (([Symbol], [SpecType]) -> [Symbol])
-> (SpecType -> ([Symbol], [SpecType])) -> SpecType -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> ([Symbol], [SpecType])
vargs (SpecType -> [Symbol]) -> [SpecType] -> [[Symbol]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
ts2')
                in  let rp :: RelPred
rp = Var
-> Var
-> [(Symbol, [Symbol])]
-> [(Symbol, [Symbol])]
-> RelExpr
-> RelPred
RelPred Var
f1 Var
f2 [(Symbol, [Symbol])]
bs1 [(Symbol, [Symbol])]
bs2 (RelExpr -> RelPred) -> RelExpr -> RelPred
forall a b. (a -> b) -> a -> b
$ Expr -> RelExpr
forall v. ExprV v -> RelExprV v
ERBasic Expr
q
                    in [Char] -> RelPred -> RelPred
forall a. [Char] -> a -> a
traceWhenLoud ([Char]
"partitionArgs toRel: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (Var, Var, [(Symbol, [Symbol])], [(Symbol, [Symbol])], Expr)
-> [Char]
forall a. PPrint a => a -> [Char]
F.showpp (Var
f1, Var
f2, [(Symbol, [Symbol])]
bs1, [(Symbol, [Symbol])]
bs2, Expr
q)) RelPred
rp
  toUnary :: (a, b, c, d, e) -> e
toUnary (a
_, b
_, c
_, d
_, e
q) = e
q

unRAllT :: SpecType -> String -> (RTVU RTyCon RTyVar, SpecType, RReft)
unRAllT :: SpecType
-> [Char]
-> (RTVar RTyVar (RType RTyCon RTyVar ()), SpecType, RReft)
unRAllT (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
α2 SpecType
ft2 RReft
r2) [Char]
_ = (RTVar RTyVar (RType RTyCon RTyVar ())
α2, SpecType
ft2, RReft
r2)
unRAllT SpecType
t [Char]
msg = [Char] -> (RTVar RTyVar (RType RTyCon RTyVar ()), SpecType, RReft)
forall a. [Char] -> a
F.panic ([Char]
 -> (RTVar RTyVar (RType RTyCon RTyVar ()), SpecType, RReft))
-> [Char]
-> (RTVar RTyVar (RType RTyCon RTyVar ()), SpecType, RReft)
forall a b. (a -> b) -> a -> b
$ [Char]
msg [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": expected RAllT, got: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp SpecType
t

forgetRAllP :: PVU RTyCon RTyVar -> SpecType -> SpecType
forgetRAllP :: PVUV Symbol RTyCon RTyVar -> SpecType -> SpecType
forgetRAllP PVUV Symbol RTyCon RTyVar
_ SpecType
t = SpecType
t

args :: CoreExpr -> CoreExpr -> SpecType -> SpecType -> F.Expr ->
  Maybe ([Var], [Var], [F.Symbol], [F.Symbol], [SpecType], [SpecType], [F.Expr])
args :: CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> Maybe
     ([Var], [Var], [Symbol], [Symbol], [SpecType], [SpecType], [Expr])
args CoreExpr
e1 CoreExpr
e2 SpecType
t1 SpecType
t2 Expr
ps
  | [Var]
xs1 <- CoreExpr -> [Var]
xargs CoreExpr
e1, [Var]
xs2 <- CoreExpr -> [Var]
xargs CoreExpr
e2,
    ([Symbol]
vs1, [SpecType]
ts1) <- SpecType -> ([Symbol], [SpecType])
vargs SpecType
t1, ([Symbol]
vs2, [SpecType]
ts2) <- SpecType -> ([Symbol], [SpecType])
vargs SpecType
t2,
    [Expr]
qs  <- Expr -> [Expr]
prems Expr
ps,
    (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ([Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
qs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==) [[Var] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
xs1, [Var] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
xs2, [Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
vs1, [Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
vs2, [SpecType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SpecType]
ts1, [SpecType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SpecType]
ts2]
  = ([Var], [Var], [Symbol], [Symbol], [SpecType], [SpecType], [Expr])
-> Maybe
     ([Var], [Var], [Symbol], [Symbol], [SpecType], [SpecType], [Expr])
forall a. a -> Maybe a
Just ([Var]
xs1, [Var]
xs2, [Symbol]
vs1, [Symbol]
vs2, [SpecType]
ts1, [SpecType]
ts2, [Expr]
qs)
args CoreExpr
e1 CoreExpr
e2 SpecType
t1 SpecType
t2 Expr
ps = [Char]
-> Maybe
     ([Var], [Var], [Symbol], [Symbol], [SpecType], [SpecType], [Expr])
-> Maybe
     ([Var], [Var], [Symbol], [Symbol], [SpecType], [SpecType], [Expr])
forall a. [Char] -> a -> a
traceWhenLoud ([Char]
"args guard" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ([Var], [Var], ([Symbol], [SpecType]), ([Symbol], [SpecType]),
 [Expr])
-> [Char]
forall a. PPrint a => a -> [Char]
F.showpp (CoreExpr -> [Var]
xargs CoreExpr
e1, CoreExpr -> [Var]
xargs CoreExpr
e2, SpecType -> ([Symbol], [SpecType])
vargs SpecType
t1, SpecType -> ([Symbol], [SpecType])
vargs SpecType
t2, Expr -> [Expr]
prems Expr
ps)) Maybe
  ([Var], [Var], [Symbol], [Symbol], [SpecType], [SpecType], [Expr])
forall a. Maybe a
Nothing

xargs :: CoreExpr -> [Var]
xargs :: CoreExpr -> [Var]
xargs (Tick CoreTickish
_ CoreExpr
e) = CoreExpr -> [Var]
xargs CoreExpr
e
xargs (Lam  Var
x CoreExpr
e) | Var -> Bool
Ghc.isTyVar Var
x = CoreExpr -> [Var]
xargs CoreExpr
e
xargs (Lam  Var
x CoreExpr
e) = Var
x Var -> [Var] -> [Var]
forall a. a -> [a] -> [a]
: CoreExpr -> [Var]
xargs CoreExpr
e
xargs CoreExpr
_          = []

xbody :: CoreExpr -> CoreExpr
xbody :: CoreExpr -> CoreExpr
xbody (Tick CoreTickish
_ CoreExpr
e) = CoreExpr -> CoreExpr
xbody CoreExpr
e
xbody (Lam  Var
_ CoreExpr
e) = CoreExpr -> CoreExpr
xbody CoreExpr
e
xbody CoreExpr
e          = CoreExpr
e

refts :: SpecType -> [RReft]
refts :: SpecType -> [RReft]
refts (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
_ SpecType
t RReft
r ) = RReft
r RReft -> [RReft] -> [RReft]
forall a. a -> [a] -> [a]
: SpecType -> [RReft]
refts SpecType
t
refts (RFun Symbol
_ RFInfo
_ SpecType
_ SpecType
t RReft
r) = RReft
r RReft -> [RReft] -> [RReft]
forall a. a -> [a] -> [a]
: SpecType -> [RReft]
refts SpecType
t
refts SpecType
_              = []

vargs :: SpecType -> ([F.Symbol], [SpecType])
vargs :: SpecType -> ([Symbol], [SpecType])
vargs (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
_ SpecType
t RReft
_ ) = SpecType -> ([Symbol], [SpecType])
vargs SpecType
t
vargs (RFun Symbol
v RFInfo
_ SpecType
s SpecType
t RReft
_) = ([Symbol] -> [Symbol])
-> ([SpecType] -> [SpecType])
-> ([Symbol], [SpecType])
-> ([Symbol], [SpecType])
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (Symbol
v Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:) (SpecType
s SpecType -> [SpecType] -> [SpecType]
forall a. a -> [a] -> [a]
:) (([Symbol], [SpecType]) -> ([Symbol], [SpecType]))
-> ([Symbol], [SpecType]) -> ([Symbol], [SpecType])
forall a b. (a -> b) -> a -> b
$ SpecType -> ([Symbol], [SpecType])
vargs SpecType
t
vargs SpecType
_              = ([], [])

ret :: SpecType -> SpecType
ret :: SpecType -> SpecType
ret (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
_ SpecType
t RReft
_ ) = SpecType -> SpecType
ret SpecType
t
ret (RFun Symbol
_ RFInfo
_ SpecType
_ SpecType
t RReft
_) = SpecType -> SpecType
ret SpecType
t
ret SpecType
t              = SpecType
t

prems :: F.Expr -> [F.Expr]
prems :: Expr -> [Expr]
prems (F.PImp Expr
q Expr
p) = Expr
q Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: Expr -> [Expr]
prems Expr
p
prems Expr
_            = []

concl :: F.Expr -> F.Expr
concl :: Expr -> Expr
concl (F.PImp Expr
_ Expr
p) = Expr -> Expr
concl Expr
p
concl Expr
p            = Expr
p

extendWithTyVar :: CGEnv -> TyVar -> CG CGEnv
extendWithTyVar :: CGEnv -> Var -> CG CGEnv
extendWithTyVar CGEnv
γ Var
a
  | Type -> Bool
isValKind (Var -> Type
Ghc.tyVarKind Var
a)
  = CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"extendWithTyVar", Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
a, Type -> SpecType
forall r. Monoid r => Type -> RRType r
kindToRType (Type -> SpecType) -> Type -> SpecType
forall a b. (a -> b) -> a -> b
$ Var -> Type
Ghc.tyVarKind Var
a)
  | Bool
otherwise
  = CGEnv -> CG CGEnv
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ

matchFunArgs :: SpecType -> SpecType -> F.Symbol -> F.Expr
matchFunArgs :: SpecType -> SpecType -> Symbol -> Expr
matchFunArgs (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
_ SpecType
t1 RReft
_) SpecType
t2 Symbol
x = SpecType -> SpecType -> Symbol -> Expr
matchFunArgs SpecType
t1 SpecType
t2 Symbol
x
matchFunArgs SpecType
t1 (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
_ SpecType
t2 RReft
_) Symbol
x = SpecType -> SpecType -> Symbol -> Expr
matchFunArgs SpecType
t1 SpecType
t2 Symbol
x
matchFunArgs (RFun Symbol
x1 RFInfo
_ SpecType
_ SpecType
t1 RReft
_) (RFun Symbol
x2 RFInfo
_ SpecType
_ SpecType
t2 RReft
_) Symbol
x =
  if Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
x1 then Symbol -> Expr
forall v. v -> ExprV v
F.EVar Symbol
x2 else SpecType -> SpecType -> Symbol -> Expr
matchFunArgs SpecType
t1 SpecType
t2 Symbol
x
matchFunArgs SpecType
t1 SpecType
t2 Symbol
x | SpecType -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isBase SpecType
t1 Bool -> Bool -> Bool
&& SpecType -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isBase SpecType
t2 = Symbol -> Expr
forall v. v -> ExprV v
F.EVar Symbol
x
matchFunArgs SpecType
t1 SpecType
t2 Symbol
_ = [Char] -> Expr
forall a. [Char] -> a
F.panic ([Char] -> Expr) -> [Char] -> Expr
forall a b. (a -> b) -> a -> b
$ [Char]
"matchFunArgs undefined for " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (SpecType, SpecType) -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp (SpecType
t1, SpecType
t2)

entl :: CGEnv -> F.Expr -> String -> CG ()
entl :: CGEnv -> Expr -> [Char] -> CG ()
entl CGEnv
γ Expr
p = SubC -> [Char] -> CG ()
addC (CGEnv -> Oblig -> RReft -> SubC
SubR CGEnv
γ Oblig
OCons (RReft -> SubC) -> RReft -> SubC
forall a b. (a -> b) -> a -> b
$ (Symbol, Expr) -> RReft
uReft (Symbol
F.vv_, Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
F.PIff (Symbol -> Expr
forall v. v -> ExprV v
F.EVar Symbol
F.vv_) Expr
p))

entlFunReft :: CGEnv -> RReft -> String -> CG ()
entlFunReft :: CGEnv -> RReft -> [Char] -> CG ()
entlFunReft CGEnv
γ RReft
r [Char]
msg = do
  CGEnv -> Expr -> [Char] -> CG ()
entl CGEnv
γ (ReftV Symbol -> Expr
forall v. ReftV v -> ExprV v
F.reftPred (ReftV Symbol -> Expr) -> ReftV Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ RReft -> ReftV Symbol
forall v r. UReftV v r -> r
ur_reft RReft
r) ([Char] -> CG ()) -> [Char] -> CG ()
forall a b. (a -> b) -> a -> b
$ [Char]
"entlFunRefts " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
msg

entlFunRefts :: CGEnv -> RReft -> RReft -> String -> CG ()
entlFunRefts :: CGEnv -> RReft -> RReft -> [Char] -> CG ()
entlFunRefts CGEnv
γ RReft
r1 RReft
r2 [Char]
msg = do
  CGEnv -> RReft -> [Char] -> CG ()
entlFunReft CGEnv
γ RReft
r1 ([Char] -> CG ()) -> [Char] -> CG ()
forall a b. (a -> b) -> a -> b
$ [Char]
msg [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" L"
  CGEnv -> RReft -> [Char] -> CG ()
entlFunReft CGEnv
γ RReft
r2 ([Char] -> CG ()) -> [Char] -> CG ()
forall a b. (a -> b) -> a -> b
$ [Char]
msg [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" R"

subRelCopies :: CoreExpr -> Var -> CoreExpr -> Var -> (CoreExpr, CoreExpr)
subRelCopies :: CoreExpr -> Var -> CoreExpr -> Var -> (CoreExpr, CoreExpr)
subRelCopies CoreExpr
e1 Var
x1 CoreExpr
e2 Var
x2 = (Var -> Var -> CoreExpr -> CoreExpr
subVarAndTy Var
x1 Var
evar1 CoreExpr
e1, Var -> Var -> CoreExpr -> CoreExpr
subVarAndTy Var
x2 Var
evar2 CoreExpr
e2)
  where (Var
evar1, Var
evar2) = Var -> Var -> (Var, Var)
mkRelCopies Var
x1 Var
x2

subVarAndTy :: Var -> Var -> CoreExpr -> CoreExpr
subVarAndTy :: Var -> Var -> CoreExpr -> CoreExpr
subVarAndTy Var
x Var
v = HashMap Var Type -> CoreExpr -> CoreExpr
forall a. Subable a => HashMap Var Type -> a -> a
subTy (Var -> Type -> HashMap Var Type
forall k v. Hashable k => k -> v -> HashMap k v
M.singleton Var
x (Type -> HashMap Var Type) -> Type -> HashMap Var Type
forall a b. (a -> b) -> a -> b
$ Var -> Type
TyVarTy Var
v) (CoreExpr -> CoreExpr)
-> (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap Var CoreExpr -> CoreExpr -> CoreExpr
forall a. Subable a => HashMap Var CoreExpr -> a -> a
sub (Var -> CoreExpr -> HashMap Var CoreExpr
forall k v. Hashable k => k -> v -> HashMap k v
M.singleton Var
x (CoreExpr -> HashMap Var CoreExpr)
-> CoreExpr -> HashMap Var CoreExpr
forall a b. (a -> b) -> a -> b
$ Var -> CoreExpr
forall b. Var -> Expr b
Var Var
v)

mkRelCopies :: Var -> Var -> (Var, Var)
mkRelCopies :: Var -> Var -> (Var, Var)
mkRelCopies Var
x1 Var
x2 = ([Char] -> Var -> Var
mkCopyWithSuffix [Char]
relSuffixL Var
x1, [Char] -> Var -> Var
mkCopyWithSuffix [Char]
relSuffixR Var
x2)

mkCopyWithName :: String -> Var -> Var
mkCopyWithName :: [Char] -> Var -> Var
mkCopyWithName [Char]
s Var
v =
  Var -> Name -> Var
Ghc.setVarName Var
v (Name -> Var) -> Name -> Var
forall a b. (a -> b) -> a -> b
$ Unique -> OccName -> Name
Ghc.mkSystemName (Var -> Unique
forall a. Uniquable a => a -> Unique
Ghc.getUnique Var
v) ([Char] -> OccName
Ghc.mkVarOcc [Char]
s)

mkCopyWithSuffix :: String -> Var -> Var
mkCopyWithSuffix :: [Char] -> Var -> Var
mkCopyWithSuffix [Char]
s Var
v = [Char] -> Var -> Var
mkCopyWithName (Var -> [Char]
forall a. NamedThing a => a -> [Char]
Ghc.getOccString Var
v [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
s) Var
v

lookupBind :: Var -> [CoreBind] -> CoreBind
lookupBind :: Var -> [CoreBind] -> CoreBind
lookupBind Var
x [CoreBind]
bs = case Var -> [(Var, CoreBind)] -> Maybe CoreBind
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Var
x ((CoreBind -> [(Var, CoreBind)]) -> [CoreBind] -> [(Var, CoreBind)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CoreBind -> [(Var, CoreBind)]
forall {a}. Bind a -> [(a, Bind a)]
binds [CoreBind]
bs) of
  Maybe CoreBind
Nothing -> [Char] -> CoreBind
forall a. [Char] -> a
F.panic ([Char] -> CoreBind) -> [Char] -> CoreBind
forall a b. (a -> b) -> a -> b
$ [Char]
"Not found definition for " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Var -> [Char]
forall a. Show a => a -> [Char]
show Var
x
  Just CoreBind
e  -> CoreBind
e
 where
  binds :: Bind a -> [(a, Bind a)]
binds b :: Bind a
b@(NonRec a
x' Expr a
_) = [ (a
x', Bind a
b) ]
  binds   (Rec [(a, Expr a)]
bs'    ) = [ (a
x', [(a, Expr a)] -> Bind a
forall b. [(b, Expr b)] -> Bind b
Rec [(a
x',Expr a
e)]) | (a
x',Expr a
e) <- [(a, Expr a)]
bs' ]

subUnarySig :: CGEnv -> Var -> SpecType -> CG ()
subUnarySig :: CGEnv -> Var -> SpecType -> CG ()
subUnarySig CGEnv
γ Var
x SpecType
tRel =
  [(SpecType, SpecType)] -> ((SpecType, SpecType) -> CG ()) -> CG ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(SpecType, SpecType)]
mkargs (((SpecType, SpecType) -> CG ()) -> CG ())
-> ((SpecType, SpecType) -> CG ()) -> CG ()
forall a b. (a -> b) -> a -> b
$ \(SpecType
rt, SpecType
ut) -> SubC -> [Char] -> CG ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ SpecType
ut SpecType
rt) ([Char] -> CG ()) -> [Char] -> CG ()
forall a b. (a -> b) -> a -> b
$ [Char]
"subUnarySig tUn = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp SpecType
ut [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" tRel = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp SpecType
rt
  where
    mkargs :: [(SpecType, SpecType)]
mkargs = [SpecType] -> [SpecType] -> [(SpecType, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip (([Symbol], [SpecType]) -> [SpecType]
forall a b. (a, b) -> b
snd (([Symbol], [SpecType]) -> [SpecType])
-> ([Symbol], [SpecType]) -> [SpecType]
forall a b. (a -> b) -> a -> b
$ SpecType -> ([Symbol], [SpecType])
vargs SpecType
tRel) (([Symbol], [SpecType]) -> [SpecType]
forall a b. (a, b) -> b
snd (([Symbol], [SpecType]) -> [SpecType])
-> ([Symbol], [SpecType]) -> [SpecType]
forall a b. (a -> b) -> a -> b
$ SpecType -> ([Symbol], [SpecType])
vargs SpecType
tUn)
    tUn :: SpecType
tUn = CGEnv -> Var -> [Char] -> SpecType
symbolType CGEnv
γ Var
x ([Char] -> SpecType) -> [Char] -> SpecType
forall a b. (a -> b) -> a -> b
$ [Char]
"subUnarySig " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Var -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp Var
x

addPred :: CGEnv -> F.Expr -> CG CGEnv
addPred :: CGEnv -> Expr -> CG CGEnv
addPred CGEnv
γ Expr
p = CGEnv -> [Expr] -> CG CGEnv
extendWithExprs CGEnv
γ [Expr
p]

addPreds :: CGEnv -> [F.Expr] -> CG CGEnv
addPreds :: CGEnv -> [Expr] -> CG CGEnv
addPreds = CGEnv -> [Expr] -> CG CGEnv
extendWithExprs

extendWithExprs :: CGEnv -> [F.Expr] -> CG CGEnv
extendWithExprs :: CGEnv -> [Expr] -> CG CGEnv
extendWithExprs CGEnv
γ [Expr]
ps = do
  dummy <- StateT CGInfo Identity Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh
  let reft = (Symbol, Expr) -> RReft
uReft (Symbol
F.vv_, [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
F.PAnd [Expr]
ps)
  γ += ("extend with predicate env", dummy, RVar (symbolRTyVar F.dummySymbol) reft)

unapplyArg :: F.Symbol -> F.Symbol -> F.Expr -> F.Expr
unapplyArg :: Symbol -> Symbol -> Expr -> Expr
unapplyArg Symbol
f Symbol
y Expr
e = (Expr -> Expr) -> Expr -> Expr
forall t. Visitable t => (Expr -> Expr) -> t -> t
F.mapExpr Expr -> Expr
sb Expr
e
  where
    sb :: F.Expr -> F.Expr
    sb :: Expr -> Expr
sb (F.EApp (F.EVar Symbol
r) (F.EVar Symbol
x))
      | Symbol
r Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
f Bool -> Bool -> Bool
&& Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
y = Symbol -> Expr
forall v. v -> ExprV v
F.EVar Symbol
r
    sb Expr
e' = Expr
e'

unapplyRelArgs :: F.Symbol -> F.Symbol -> F.Expr -> F.Expr
unapplyRelArgs :: Symbol -> Symbol -> Expr -> Expr
unapplyRelArgs Symbol
x1 Symbol
x2 = Symbol -> Symbol -> Expr -> Expr
unapplyArg Symbol
resL Symbol
x1 (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol -> Expr -> Expr
unapplyArg Symbol
resR Symbol
x2

unapplyRelArgsR :: F.Symbol -> F.Symbol -> RelExpr -> RelExpr
unapplyRelArgsR :: Symbol -> Symbol -> RelExpr -> RelExpr
unapplyRelArgsR Symbol
x1 Symbol
x2 (ERBasic Expr
e) = Expr -> RelExpr
forall v. ExprV v -> RelExprV v
ERBasic (Symbol -> Symbol -> Expr -> Expr
unapplyRelArgs Symbol
x1 Symbol
x2 Expr
e)
unapplyRelArgsR Symbol
x1 Symbol
x2 (ERChecked Expr
e RelExpr
re) = Expr -> RelExpr -> RelExpr
forall v. ExprV v -> RelExprV v -> RelExprV v
ERChecked (Symbol -> Symbol -> Expr -> Expr
unapplyRelArgs Symbol
x1 Symbol
x2 Expr
e) (Symbol -> Symbol -> RelExpr -> RelExpr
unapplyRelArgsR Symbol
x1 Symbol
x2 RelExpr
re)
unapplyRelArgsR Symbol
x1 Symbol
x2 (ERUnChecked Expr
e RelExpr
re) = Expr -> RelExpr -> RelExpr
forall v. ExprV v -> RelExprV v -> RelExprV v
ERUnChecked (Symbol -> Symbol -> Expr -> Expr
unapplyRelArgs Symbol
x1 Symbol
x2 Expr
e) (Symbol -> Symbol -> RelExpr -> RelExpr
unapplyRelArgsR Symbol
x1 Symbol
x2 RelExpr
re)

--------------------------------------------------------------
-- RelExpr & F.Expr ------------------------------------------
--------------------------------------------------------------

fromRelExpr :: RelExpr -> F.Expr
fromRelExpr :: RelExpr -> Expr
fromRelExpr (ERBasic Expr
e) = Expr
e
fromRelExpr (ERChecked Expr
a RelExpr
b) = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
F.PImp Expr
a (RelExpr -> Expr
fromRelExpr RelExpr
b)
fromRelExpr (ERUnChecked Expr
a RelExpr
b) = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
F.PImp Expr
a (RelExpr -> Expr
fromRelExpr RelExpr
b)

--------------------------------------------------------------
-- Debug -----------------------------------------------------
--------------------------------------------------------------


traceSub :: (PPrint t, PPrint s, PPrint p, PPrint q) => String -> t -> s -> p -> q -> a -> a
traceSub :: forall t s p q a.
(PPrint t, PPrint s, PPrint p, PPrint q) =>
[Char] -> t -> s -> p -> q -> a -> a
traceSub [Char]
msg t
t s
s p
p q
q = [Char] -> a -> a
forall a. [Char] -> a -> a
traceWhenLoud ([Char]
msg [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" RelSub\n"
                      [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"t: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp t
t [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n"
                      [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"s: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ s -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp s
s [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n"
                      [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"p: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ p -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp p
p [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n"
                      [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"q: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ q -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp q
q)


traceChk
  :: (PPrint e, PPrint d, PPrint t, PPrint s, PPrint p)
  => String -> e -> d -> t -> s -> p -> a -> a
traceChk :: forall e d t s p a.
(PPrint e, PPrint d, PPrint t, PPrint s, PPrint p) =>
[Char] -> e -> d -> t -> s -> p -> a -> a
traceChk [Char]
expr = [Char] -> e -> d -> t -> s -> p -> a -> a
forall e d t s p a.
(PPrint e, PPrint d, PPrint t, PPrint s, PPrint p) =>
[Char] -> e -> d -> t -> s -> p -> a -> a
trace ([Char]
expr [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" To CHECK")

traceSyn
  :: (PPrint e, PPrint d, PPrint a, PPrint b, PPrint c)
  => String -> e -> d -> CG (a, b, c) -> CG (a, b, c)
traceSyn :: forall e d a b c.
(PPrint e, PPrint d, PPrint a, PPrint b, PPrint c) =>
[Char] -> e -> d -> CG (a, b, c) -> CG (a, b, c)
traceSyn [Char]
expr e
e d
d CG (a, b, c)
cg
  = do
    (a, b, c) <- CG (a, b, c)
cg
    trace (expr ++ " To SYNTH") e d a b c cg

traceSynApp
  :: (PPrint e, PPrint d, PPrint a, PPrint b, PPrint c)
  => e -> d -> a -> b -> c -> t -> t
traceSynApp :: forall e d a b c t.
(PPrint e, PPrint d, PPrint a, PPrint b, PPrint c) =>
e -> d -> a -> b -> c -> t -> t
traceSynApp = [Char] -> e -> d -> a -> b -> c -> t -> t
forall e d t s p a.
(PPrint e, PPrint d, PPrint t, PPrint s, PPrint p) =>
[Char] -> e -> d -> t -> s -> p -> a -> a
trace [Char]
"SYNTH APP TO "

traceUSyn
  :: (PPrint e, PPrint a)
  => String -> e -> CG a -> CG a
traceUSyn :: forall e a. (PPrint e, PPrint a) => [Char] -> e -> CG a -> CG a
traceUSyn [Char]
expr e
e CG a
cg = do
  t <- CG a
cg
  trace (expr ++ " To SYNTH UNARY") e dummy t dummy dummy cg
  where
    dummy :: F.Expr
    dummy :: Expr
dummy = Expr
forall v. ExprV v
F.PTrue

trace
  :: (PPrint e, PPrint d, PPrint t, PPrint s, PPrint p)
  => String -> e -> d -> t -> s -> p -> a -> a
trace :: forall e d t s p a.
(PPrint e, PPrint d, PPrint t, PPrint s, PPrint p) =>
[Char] -> e -> d -> t -> s -> p -> a -> a
trace [Char]
msg e
e d
d t
t s
s p
p = [Char] -> a -> a
forall a. [Char] -> a -> a
traceWhenLoud ([Char]
msg [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
                      [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"e: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ e -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp e
e [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n"
                      [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"d: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ d -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp d
d [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n"
                      [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"t: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp t
t [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n"
                      [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"s: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ s -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp s
s [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n"
                      [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"p: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ p -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp p
p)

traceWhenLoud :: String -> a -> a
traceWhenLoud :: forall a. [Char] -> a -> a
traceWhenLoud [Char]
s a
a = IO a -> a
forall a. IO a -> a
unsafePerformIO (IO a -> a) -> IO a -> a
forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
whenLoud ([Char] -> IO ()
putStrLn [Char]
s) IO () -> IO a -> IO a
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> IO a
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a