{-# 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.State
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                  hiding (Def,
                                                                 Loc, binds,
                                                                 loc)
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]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [RelPred] -> ShowS
$cshowList :: [RelPred] -> ShowS
show :: RelPred -> [Char]
$cshow :: RelPred -> [Char]
showsPrec :: Int -> RelPred -> ShowS
$cshowsPrec :: Int -> 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) = 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 forall a b. (a -> b) -> a -> b
$ do
  forall a. [Char] -> a -> a
traceWhenLoud ([Char]
"ASSUME " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp (RelExpr -> Expr
fromRelExpr RelExpr
p', Expr
p)) 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'
  CGEnv
γ'' <- if SpecType -> Bool
base SpecType
t' Bool -> Bool -> Bool
&& SpecType -> Bool
base SpecType
s'
    then CGEnv
γ' CGEnv -> Expr -> CG CGEnv
`addPred` forall a. Subable a => Subst -> a -> a
F.subst
      ([(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
resL, Symbol -> Expr
F.EVar forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
F.symbol Var
x), (Symbol
resR, Symbol -> Expr
F.EVar forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
F.symbol Var
y)])
      (RelExpr -> Expr
fromRelExpr RelExpr
rp)
    else forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ'
  forall (m :: * -> *) a. Monad m => a -> m a
return (Var
-> Var
-> [(Symbol, [Symbol])]
-> [(Symbol, [Symbol])]
-> RelExpr
-> RelPred
RelPred Var
x' Var
y' [(Symbol, [Symbol])]
bs [(Symbol, [Symbol])]
cs RelExpr
rp forall a. a -> [a] -> [a]
: [RelPred]
ψ, CGEnv
γ'')
 where
    p :: Expr
p = RelExpr -> Expr
fromRelExpr RelExpr
rp
    γ' :: CGEnv
γ' = CGEnv
γ CGEnv -> Span -> CGEnv
`setLocation` SrcSpan -> Span
Sp.Span (forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (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' = forall a. Located a -> a
val LocSpecType
t
    s' :: SpecType
s' = 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 = forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
vs (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> ([Symbol], [SpecType])
vargs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
ts)
    cs :: [(Symbol, [Symbol])]
cs = forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
us (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> ([Symbol], [SpecType])
vargs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
ss)
    p' :: RelExpr
p' = 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 (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) = 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 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 (forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (forall a. Located a -> SourcePos
F.loc LocSpecType
t))
    cbs :: [CoreBind]
cbs = TargetSrc -> [CoreBind]
giCbs 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 forall a b. (a -> b) -> a -> b
$ forall a. Located a -> a
val LocSpecType
t
    s' :: SpecType
s' = SpecType -> SpecType
removeAbsRef forall a b. (a -> b) -> a -> b
$ forall a. Located a -> a
val LocSpecType
s

removeAbsRef :: SpecType -> SpecType
removeAbsRef :: SpecType -> SpecType
removeAbsRef (RVar RTyVar
v (MkUReft Reft
r Predicate
_))
  = forall {c}. RType c RTyVar RReft
out
    where
      r' :: RReft
r' = forall r. r -> Predicate -> UReft r
MkUReft Reft
r forall a. Monoid a => a
mempty
      out :: RType c RTyVar RReft
out = forall c tv r. tv -> r -> RType c tv r
RVar  RTyVar
v RReft
r'
removeAbsRef (RFun  Symbol
b RFInfo
i SpecType
s SpecType
t (MkUReft Reft
r Predicate
_))
  = SpecType
out
    where
      r' :: RReft
r' = forall r. r -> Predicate -> UReft r
MkUReft Reft
r forall a. Monoid a => a
mempty
      out :: SpecType
out = forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun  Symbol
b RFInfo
i (SpecType -> SpecType
removeAbsRef SpecType
s) (SpecType -> SpecType
removeAbsRef SpecType
t) RReft
r'
removeAbsRef (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
b SpecType
t RReft
r)
  = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVar RTyVar (RType RTyCon RTyVar ())
b (SpecType -> SpecType
removeAbsRef SpecType
t) RReft
r
removeAbsRef (RAllP PVU RTyCon RTyVar
p SpecType
t)
  = SpecType -> SpecType
removeAbsRef (PVU RTyCon RTyVar -> SpecType -> SpecType
forgetRAllP PVU RTyCon RTyVar
p SpecType
t)
removeAbsRef (RApp  (RTyCon TyCon
c [PVU RTyCon RTyVar]
_ TyConInfo
i) [SpecType]
as [RTProp RTyCon RTyVar RReft]
_ (MkUReft Reft
r Predicate
_))
  = SpecType
out
    where
      c' :: RTyCon
c' = TyCon -> [PVU RTyCon RTyVar] -> TyConInfo -> RTyCon
RTyCon TyCon
c [] TyConInfo
i
      as' :: [SpecType]
as' = forall a b. (a -> b) -> [a] -> [b]
map SpecType -> SpecType
removeAbsRef [SpecType]
as
      r' :: RReft
r' = forall r. r -> Predicate -> UReft r
MkUReft Reft
r forall a. Monoid a => a
mempty
      out :: SpecType
out = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c' [SpecType]
as' [] RReft
r'
removeAbsRef (RAllE Symbol
b SpecType
a SpecType
t)
  = forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
b (SpecType -> SpecType
removeAbsRef SpecType
a) (SpecType -> SpecType
removeAbsRef SpecType
t)
removeAbsRef (REx   Symbol
b SpecType
a SpecType
t)
  = forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx   Symbol
b (SpecType -> SpecType
removeAbsRef SpecType
a) (SpecType -> SpecType
removeAbsRef SpecType
t)
removeAbsRef (RAppTy SpecType
s SpecType
t RReft
r)
  = forall c tv r. RType c tv r -> RType c tv r -> r -> RType 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)
  = forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType 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 = forall a. IsString a => [Char] -> a
fromString [Char]
"r1"
resR :: Symbol
resR = 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 =
  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 forall a b. (a -> b) -> a -> b
$ do
    CGEnv
γ' <- CGEnv
γ CGEnv -> Expr -> CG CGEnv
`addPred` Expr
a
    CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
consRelCheck CGEnv
γ' [RelPred]
ψ CoreExpr
e1 CoreExpr
e2 SpecType
t1 SpecType
t2 Expr
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]
ψ (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 (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
  = 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 forall a b. (a -> b) -> a -> b
$ do
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (SpecType -> [RReft]
refts SpecType
t1 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' = 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') = forall a b. [(a, b)] -> ([a], [b])
unzip [(Var, Var)]
xs'
    let (CoreExpr
e1'', CoreExpr
e2'') = 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') (forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
xs1 [Var]
xs2)
    CGEnv
γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"Bind Rec f1", forall a. Symbolic a => a -> Symbol
F.symbol Var
f1', SpecType
t1) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"Bind Rec f2", forall a. Symbolic a => a -> Symbol
F.symbol Var
f2', SpecType
t2))
    CGEnv
γ'' <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\CGEnv
γγ (Var
x, SpecType
t) -> CGEnv
γγ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"Bind Rec x1", forall a. Symbolic a => a -> Symbol
F.symbol Var
x, SpecType
t)) CGEnv
γ' (forall a b. [a] -> [b] -> [(a, b)]
zip ([Var]
xs1' forall a. [a] -> [a] -> [a]
++ [Var]
xs2') ([SpecType]
ts1 forall a. [a] -> [a] -> [a]
++ [SpecType]
ts2))
    let vs2xs :: a -> a
vs2xs =  forall a. Subable a => Subst -> a -> a
F.subst forall a b. (a -> b) -> a -> b
$ [(Symbol, Expr)] -> Subst
F.mkSubst forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip ([Symbol]
vs1 forall a. [a] -> [a] -> [a]
++ [Symbol]
vs2) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Symbol -> Expr
F.EVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Symbol
F.symbol) ([Var]
xs1' forall a. [a] -> [a] -> [a]
++ [Var]
xs2')
    let ([RelPred]
ho, [Expr]
fo) = [Var]
-> [Var]
-> [SpecType]
-> [SpecType]
-> [Expr]
-> ([RelPred], [Expr])
partitionArgs [Var]
xs1 [Var]
xs2 [SpecType]
ts1 [SpecType]
ts2 [Expr]
qs
    CGEnv
γ''' <- CGEnv
γ'' CGEnv -> [Expr] -> CG CGEnv
`addPreds` forall a. [Char] -> a -> a
traceWhenLoud ([Char]
"PRECONDITION " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp (forall {a}. Subable a => a -> a
vs2xs ([Expr] -> Expr
F.PAnd [Expr]
fo)) forall a. [a] -> [a] -> [a]
++ [Char]
"\n" forall a. [a] -> [a] -> [a]
++
                                          [Char]
"ASSUMPTION " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp (forall {a}. Subable a => a -> a
vs2xs Expr
a))
                              forall a b. (a -> b) -> [a] -> [b]
map forall {a}. Subable a => a -> a
vs2xs [[Expr] -> Expr
F.PAnd [Expr]
fo, Expr
a]
    let p' :: RelExpr
p' = RelExpr -> [(Symbol, Symbol)] -> RelExpr
unapp RelExpr
rp (forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
vs1 [Symbol]
vs2)
    let ψ' :: [RelPred]
ψ' = [RelPred]
ho forall a. [a] -> [a] -> [a]
++ [RelPred]
ψ
    CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
consRelCheck CGEnv
γ''' [RelPred]
ψ' (CoreExpr -> CoreExpr
xbody CoreExpr
e1'') (CoreExpr -> CoreExpr
xbody CoreExpr
e2'') (forall {a}. Subable a => a -> a
vs2xs forall a b. (a -> b) -> a -> b
$ SpecType -> SpecType
ret SpecType
t1) (forall {a}. Subable a => a -> a
vs2xs forall a b. (a -> b) -> a -> b
$ SpecType -> SpecType
ret SpecType
t2) (forall {a}. Subable a => a -> a
vs2xs forall a b. (a -> b) -> a -> b
$ Expr -> Expr
concl (RelExpr -> Expr
fromRelExpr RelExpr
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 = 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
  = forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"consRelCheckBind Rec: exprs, types, and pred should have same number of args " forall a. [a] -> [a] -> [a]
++
    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
_
  = forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"consRelCheckBind Rec: multiple binders are not supported " forall a. [a] -> [a] -> [a]
++ 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
  = 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 forall a b. (a -> b) -> a -> b
$ do
    CGEnv -> RReft -> [Char] -> CG ()
entlFunReft CGEnv
γ RReft
r1 [Char]
"consRelCheck Lam Type"
    CGEnv
γ'  <- CGEnv
γ CGEnv -> Var -> CG CGEnv
`extendWithTyVar` Var
α1
    CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
consRelCheck CGEnv
γ' [RelPred]
ψ CoreExpr
e1 CoreExpr
e2 (forall {r} {c} {s}.
(Reftable r, TyConable c, FreeVar c RTyVar,
 SubsTy RTyVar (RType c RTyVar ()) c,
 SubsTy RTyVar (RType c RTyVar ()) r,
 SubsTy RTyVar (RType c RTyVar ()) (RType c RTyVar ()),
 SubsTy
   RTyVar (RType c RTyVar ()) (RTVar RTyVar (RType c RTyVar ())),
 SubsTy RTyVar (RType c RTyVar ()) RTyVar) =>
(RTVar RTyVar s, Var) -> RType c RTyVar r -> RType c RTyVar r
sb (RTVar RTyVar (RType RTyCon RTyVar ())
s1, Var
α1) SpecType
t1) SpecType
t2 Expr
p
  where sb :: (RTVar RTyVar s, Var) -> RType c RTyVar r -> RType c RTyVar r
sb (RTVar RTyVar s
s, Var
α) = 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' (forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar s
s, 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
  = 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 forall a b. (a -> b) -> a -> b
$ do
    CGEnv -> RReft -> [Char] -> CG ()
entlFunReft CGEnv
γ RReft
r2 [Char]
"consRelCheck Lam Type"
    CGEnv
γ'  <- CGEnv
γ CGEnv -> Var -> CG CGEnv
`extendWithTyVar` Var
α2
    CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
consRelCheck CGEnv
γ' [RelPred]
ψ CoreExpr
e1 CoreExpr
e2 SpecType
t1 (forall {r} {c} {s}.
(Reftable r, TyConable c, FreeVar c RTyVar,
 SubsTy RTyVar (RType c RTyVar ()) c,
 SubsTy RTyVar (RType c RTyVar ()) r,
 SubsTy RTyVar (RType c RTyVar ()) (RType c RTyVar ()),
 SubsTy
   RTyVar (RType c RTyVar ()) (RTVar RTyVar (RType c RTyVar ())),
 SubsTy RTyVar (RType c RTyVar ()) RTyVar) =>
(RTVar RTyVar s, Var) -> RType c RTyVar r -> RType c RTyVar r
sb (RTVar RTyVar (RType RTyCon RTyVar ())
s2, Var
α2) SpecType
t2) Expr
p
  where sb :: (RTVar RTyVar s, Var) -> RType c RTyVar r -> RType c RTyVar r
sb (RTVar RTyVar s
s, Var
α) = 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' (forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar s
s, 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
  = 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 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
γ CGEnv -> Var -> CG CGEnv
`extendWithTyVar` Var
α1
    CGEnv
γ'' <- CGEnv
γ' CGEnv -> Var -> CG CGEnv
`extendWithTyVar` Var
α2
    CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
consRelCheck CGEnv
γ'' [RelPred]
ψ CoreExpr
e1 CoreExpr
e2 (forall {r} {c} {s}.
(Reftable r, TyConable c, FreeVar c RTyVar,
 SubsTy RTyVar (RType c RTyVar ()) c,
 SubsTy RTyVar (RType c RTyVar ()) r,
 SubsTy RTyVar (RType c RTyVar ()) (RType c RTyVar ()),
 SubsTy
   RTyVar (RType c RTyVar ()) (RTVar RTyVar (RType c RTyVar ())),
 SubsTy RTyVar (RType c RTyVar ()) RTyVar) =>
(RTVar RTyVar s, Var) -> RType c RTyVar r -> RType c RTyVar r
sb (RTVar RTyVar (RType RTyCon RTyVar ())
s1, Var
α1) SpecType
t1) (forall {r} {c} {s}.
(Reftable r, TyConable c, FreeVar c RTyVar,
 SubsTy RTyVar (RType c RTyVar ()) c,
 SubsTy RTyVar (RType c RTyVar ()) r,
 SubsTy RTyVar (RType c RTyVar ()) (RType c RTyVar ()),
 SubsTy
   RTyVar (RType c RTyVar ()) (RTVar RTyVar (RType c RTyVar ())),
 SubsTy RTyVar (RType c RTyVar ()) RTyVar) =>
(RTVar RTyVar s, Var) -> RType c RTyVar r -> RType c RTyVar r
sb (RTVar RTyVar (RType RTyCon RTyVar ())
s2, Var
α2) SpecType
t2) Expr
p
  where sb :: (RTVar RTyVar s, Var) -> RType c RTyVar r -> RType c RTyVar r
sb (RTVar RTyVar s
s, Var
α) = 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' (forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar s
s, 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)
  = 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 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) = (forall a. Symbolic a => a -> Symbol
F.symbol Var
evar1, forall a. Symbolic a => a -> Symbol
F.symbol Var
evar2)
    let subst :: a -> a
subst = forall a. Subable a => Subst -> a -> a
F.subst forall a b. (a -> b) -> a -> b
$ [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
v1, Symbol -> Expr
F.EVar Symbol
pvar1), (Symbol
v2, Symbol -> Expr
F.EVar Symbol
pvar2)]
    CGEnv
γ'  <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consRelCheck Lam L", Symbol
pvar1, forall {a}. Subable a => a -> a
subst SpecType
s1)
    CGEnv
γ'' <- CGEnv
γ' CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consRelCheck Lam R", Symbol
pvar2, forall {a}. Subable a => a -> a
subst SpecType
s2)
    let p' :: Expr
p'    = Symbol -> Symbol -> Expr -> Expr
unapplyRelArgs Symbol
v1 Symbol
v2 Expr
p
    let ([RelPred]
ho, [Expr]
fo) = Var -> Var -> SpecType -> SpecType -> Expr -> ([RelPred], [Expr])
partitionArg Var
x1 Var
x2 SpecType
s1 SpecType
s2 Expr
q
    CGEnv
γ''' <- CGEnv
γ'' CGEnv -> [Expr] -> CG CGEnv
`addPreds` forall a. [Char] -> a -> a
traceWhenLoud ([Char]
"PRECONDITION " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp (forall a b. (a -> b) -> [a] -> [b]
map forall {a}. Subable a => a -> a
subst [Expr]
fo)) forall a b. (a -> b) -> [a] -> [b]
map forall {a}. Subable a => a -> a
subst [Expr]
fo
    CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
consRelCheck CGEnv
γ''' ([RelPred]
ho forall a. [a] -> [a] -> [a]
++ [RelPred]
ψ) CoreExpr
e1' CoreExpr
e2' (forall {a}. Subable a => a -> a
subst SpecType
t1) (forall {a}. Subable a => a -> a
subst SpecType
t2) (forall {a}. Subable a => a -> a
subst Expr
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
  = 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 forall a b. (a -> b) -> a -> b
$ do
    (SpecType
s1, SpecType
s2, [Expr]
_) <- CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
consRelSynth CGEnv
γ [RelPred]
ψ CoreExpr
d1 CoreExpr
d2
    let (Var
evar1, Var
evar2) = Var -> Var -> (Var, Var)
mkRelCopies Var
x1 Var
x2
    let (CoreExpr
e1', CoreExpr
e2')     = CoreExpr -> Var -> CoreExpr -> Var -> (CoreExpr, CoreExpr)
subRelCopies CoreExpr
e1 Var
x1 CoreExpr
e2 Var
x2
    CGEnv
γ'  <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consRelCheck Let L", forall a. Symbolic a => a -> Symbol
F.symbol Var
evar1, SpecType
s1)
    CGEnv
γ'' <- CGEnv
γ' CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consRelCheck Let R", forall a. Symbolic a => a -> Symbol
F.symbol Var
evar2, SpecType
s2)
    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 []) CoreExpr
e1) l2 :: CoreExpr
l2@(Let (Rec []) CoreExpr
e2) SpecType
t1 SpecType
t2 Expr
p
  = 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 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
  = 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 forall a b. (a -> b) -> a -> b
$ do
    (SpecType
s1, SpecType
s2, [Expr]
_) <- CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
consRelSynth CGEnv
γ [RelPred]
ψ CoreExpr
d1 CoreExpr
d2
    let (Var
evar1, Var
evar2) = Var -> Var -> (Var, Var)
mkRelCopies Var
x1 Var
x2
    let (CoreExpr
e1', CoreExpr
e2')     = CoreExpr -> Var -> CoreExpr -> Var -> (CoreExpr, CoreExpr)
subRelCopies CoreExpr
e1 Var
x1 CoreExpr
e2 Var
x2
    CGEnv
γ'  <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consRelCheck Let L", forall a. Symbolic a => a -> Symbol
F.symbol Var
evar1, SpecType
s1)
    CGEnv
γ'' <- CGEnv
γ' CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consRelCheck Let R", forall a. Symbolic a => a -> Symbol
F.symbol Var
evar2, SpecType
s2)
    CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
consRelCheck CGEnv
γ'' [RelPred]
ψ (forall b. Bind b -> Expr b -> Expr b
Let (forall b. [(b, Expr b)] -> Bind b
Rec [(Var, CoreExpr)]
bs1) CoreExpr
e1') (forall b. Bind b -> Expr b -> Expr b
Let (forall b. [(b, Expr b)] -> Bind b
Rec [(Var, CoreExpr)]
bs2) CoreExpr
e2') SpecType
t1 SpecType
t2 Expr
p

consRelCheck CGEnv
γ [RelPred]
ψ c1 :: CoreExpr
c1@(Case CoreExpr
e1 Var
x1 Type
_ [Alt Var]
alts1) CoreExpr
e2 SpecType
t1 SpecType
t2 Expr
p =
  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 forall a b. (a -> b) -> a -> b
$ do
    SpecType
s1 <- CGEnv -> CoreExpr -> CG SpecType
consUnarySynth CGEnv
γ CoreExpr
e1
    CGEnv
γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consRelCheck Case Async L", Symbol
x1', SpecType
s1)
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Alt Var]
alts1 forall a b. (a -> b) -> a -> b
$ 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
  where
    x1' :: Symbol
x1' = forall a. Symbolic a => a -> Symbol
F.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 =
  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 forall a b. (a -> b) -> a -> b
$ do
    SpecType
s2 <- CGEnv -> CoreExpr -> CG SpecType
consUnarySynth CGEnv
γ CoreExpr
e2
    CGEnv
γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consRelCheck Case Async R", Symbol
x2', SpecType
s2)
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Alt Var]
alts2 forall a b. (a -> b) -> a -> b
$ 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
  where
    x2' :: Symbol
x2' = forall a. Symbolic a => a -> Symbol
F.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 =
  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 forall a b. (a -> b) -> a -> b
$ do
  (SpecType
s1, SpecType
s2, [Expr]
qs) <- CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
consRelSynth CGEnv
γ [RelPred]
ψ CoreExpr
e CoreExpr
d
  let psubst :: c -> c
psubst = forall a. Subable a => (Symbol -> Expr) -> a -> a
F.substf (SpecType -> SpecType -> Symbol -> Expr
matchFunArgs SpecType
t1 SpecType
s1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subable a => (Symbol -> Expr) -> a -> a
F.substf (SpecType -> SpecType -> Symbol -> Expr
matchFunArgs SpecType
t2 SpecType
s2)
  CGEnv -> SpecType -> SpecType -> Expr -> Expr -> CG ()
consRelSub CGEnv
γ SpecType
s1 SpecType
s2 ([Expr] -> Expr
F.PAnd [Expr]
qs) (forall {a}. Subable a => a -> a
psubst Expr
p)
  SubC -> [Char] -> CG ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ SpecType
s1 SpecType
t1) ([Char]
"consRelCheck (Synth): s1 = " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp SpecType
s1 forall a. [a] -> [a] -> [a]
++ [Char]
" t1 = " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp SpecType
t1)
  SubC -> [Char] -> CG ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ SpecType
s2 SpecType
t2) ([Char]
"consRelCheck (Synth): s2 = " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp SpecType
s2 forall a. [a] -> [a] -> [a]
++ [Char]
" t2 = " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp SpecType
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
  SpecType
ct <- CGEnv -> AltCon -> SpecType -> CG SpecType
ctorTy CGEnv
γ AltCon
c SpecType
s
  CGEnv
-> Symbol
-> SpecType
-> [Var]
-> SpecType
-> CoreExpr
-> [Char]
-> CG (CGEnv, CoreExpr)
unapply CGEnv
γ Symbol
x SpecType
s [Var]
bs (SpecType -> SpecType
removeAbsRef SpecType
ct) CoreExpr
e [Char]
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
  (CGEnv
γ', CoreExpr
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
  CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
consRelCheck CGEnv
γ' [RelPred]
ψ CoreExpr
e1' CoreExpr
e2 SpecType
t1 SpecType
t2 Expr
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
  (CGEnv
γ', CoreExpr
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
  CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
consRelCheck CGEnv
γ' [RelPred]
ψ CoreExpr
e1 CoreExpr
e2' SpecType
t1 SpecType
t2 Expr
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 = forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshTy forall a b. (a -> b) -> a -> b
$ SpecType
ct SpecType -> [SpecType] -> SpecType
`instantiateTys` [SpecType]
ts
  | Maybe SpecType
Nothing <- Maybe SpecType
mbct = forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"ctorTy: data constructor out of scope" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp DataCon
c
  where mbct :: Maybe SpecType
mbct = CGEnv
γ (?callStack::CallStack) => CGEnv -> Symbol -> Maybe SpecType
?= forall a. Symbolic a => a -> Symbol
F.symbol (DataCon -> Var
Ghc.dataConWorkId DataCon
c)
ctorTy CGEnv
_ (DataAlt DataCon
_) SpecType
t =
  forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"ctorTy: type " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp SpecType
t forall a. [a] -> [a] -> [a]
++ [Char]
" doesn't have top-level data constructor"
ctorTy CGEnv
_ (LitAlt Literal
c) SpecType
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r. r -> UReft r
uTop forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Literal -> RType RTyCon RTyVar Reft
literalFRefType Literal
c
ctorTy CGEnv
_ AltCon
DEFAULT SpecType
t = 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
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"unapply arg", Symbol
evar, SpecType
s)
  CGEnv
-> Symbol
-> SpecType
-> [Var]
-> SpecType
-> CoreExpr
-> [Char]
-> CG (CGEnv, CoreExpr)
unapply CGEnv
γ' Symbol
y SpecType
yt [Var]
zs (SpecType
t forall a. Subable a => a -> (Symbol, Expr) -> a
`F.subst1` (Symbol
x, Symbol -> Expr
F.EVar Symbol
evar)) CoreExpr
e' [Char]
suffix
  where
    z' :: Var
z' = [Char] -> Var -> Var
mkCopyWithSuffix [Char]
suffix Var
z
    evar :: Symbol
evar = 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]
_ = forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"can't unapply type " forall a. [a] -> [a] -> [a]
++ 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 forall r. Reftable r => r -> r -> r
`F.meet` SpecType
yt
  CGEnv
γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"unapply res", Symbol
y, SpecType
yt')
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> a -> a
traceWhenLoud ([Char]
"SCRUTINEE " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp (Symbol
y, SpecType
yt')) (CGEnv
γ', CoreExpr
e)

instantiateTys :: SpecType -> [SpecType] -> SpecType
instantiateTys :: SpecType -> [SpecType] -> SpecType
instantiateTys = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' 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 ())) =>
RType c tv r -> RType c tv r -> RType c tv r
go
 where
  go :: RType c tv r -> RType c tv r -> RType c tv r
go (RAllT RTVar tv (RType c tv ())
α RType c tv r
tbody r
_) RType c tv r
t = 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' (forall tv s. RTVar tv s -> tv
ty_var_value RTVar tv (RType c tv ())
α, RType c tv r
t) RType c tv r
tbody
  go RType c tv r
tbody             RType c tv r
t =
    forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"instantiateTys: non-polymorphic type " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp RType c tv r
tbody forall a. [a] -> [a] -> [a]
++ [Char]
" to instantiate with " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp RType 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 =
  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 forall a b. (a -> b) -> a -> b
$ do
    (SpecType
ft1', SpecType
t2, [Expr]
ps) <- CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
consRelSynth CGEnv
γ [RelPred]
ψ CoreExpr
e1 CoreExpr
e2
    let (RTVar RTyVar (RType RTyCon RTyVar ())
α1, SpecType
ft1, RReft
_) = SpecType
-> [Char]
-> (RTVar RTyVar (RType RTyCon RTyVar ()), SpecType, RReft)
unRAllT SpecType
ft1' [Char]
"consRelSynth App Ty L"
    SpecType
t1' <- Bool -> Type -> CG SpecType
trueTy (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) Type
t1
    forall (m :: * -> *) a. Monad m => a -> m a
return (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' (forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar (RType RTyCon RTyVar ())
α1, SpecType
t1') SpecType
ft1, SpecType
t2, [Expr]
ps)

consRelSynth CGEnv
γ [RelPred]
ψ CoreExpr
e1 a2 :: CoreExpr
a2@(App CoreExpr
e2 CoreExpr
d2) | Type Type
t2 <- CoreExpr -> CoreExpr
GM.unTickExpr CoreExpr
d2 =
  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 forall a b. (a -> b) -> a -> b
$ do
    (SpecType
t1, SpecType
ft2', [Expr]
ps) <- CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
consRelSynth CGEnv
γ [RelPred]
ψ CoreExpr
e1 CoreExpr
e2
    let (RTVar RTyVar (RType RTyCon RTyVar ())
α2, SpecType
ft2, RReft
_) = SpecType
-> [Char]
-> (RTVar RTyVar (RType RTyCon RTyVar ()), SpecType, RReft)
unRAllT SpecType
ft2' [Char]
"consRelSynth App Ty R"
    SpecType
t2' <- Bool -> Type -> CG SpecType
trueTy (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) Type
t2
    forall (m :: * -> *) a. Monad m => a -> m a
return (SpecType
t1, 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' (forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar (RType RTyCon RTyVar ())
α2, SpecType
t2') SpecType
ft2, [Expr]
ps)

consRelSynth CGEnv
γ [RelPred]
ψ a1 :: CoreExpr
a1@(App CoreExpr
e1 CoreExpr
d1) a2 :: CoreExpr
a2@(App CoreExpr
e2 CoreExpr
d2) = 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 forall a b. (a -> b) -> a -> b
$ do
  (SpecType
ft1, SpecType
ft2, [Expr]
fps) <- CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
consRelSynth CGEnv
γ [RelPred]
ψ CoreExpr
e1 CoreExpr
e2
  (SpecType
t1, SpecType
t2, [Expr]
ps) <- CGEnv
-> [RelPred]
-> SpecType
-> SpecType
-> [Expr]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
consRelSynthApp CGEnv
γ [RelPred]
ψ SpecType
ft1 SpecType
ft2 [Expr]
fps CoreExpr
d1 CoreExpr
d2
  forall (m :: * -> *) a. Monad m => a -> m a
return (SpecType
t1, SpecType
t2, [Expr]
ps)

consRelSynth CGEnv
γ [RelPred]
ψ CoreExpr
e CoreExpr
d = 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 forall a b. (a -> b) -> a -> b
$ do
  SpecType
t <- CGEnv -> CoreExpr -> CG SpecType
consUnarySynth CGEnv
γ CoreExpr
e forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshTy
  SpecType
s <- CGEnv -> CoreExpr -> CG SpecType
consUnarySynth CGEnv
γ CoreExpr
d forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *). FreshM m => SpecType -> m SpecType
refreshTy
  let ps :: [Expr]
ps = [RelPred] -> CoreExpr -> CoreExpr -> SpecType -> SpecType -> [Expr]
lookupRelSig [RelPred]
ψ CoreExpr
e CoreExpr
d SpecType
t SpecType
s
  forall (m :: * -> *) a. Monad m => a -> m a
return (SpecType
t, SpecType
s, forall a. [Char] -> a -> a
traceWhenLoud ([Char]
"consRelSynth Unary synthed preds:" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp [Expr]
ps) [Expr]
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 = 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 forall a. Eq a => a -> a -> Bool
== Var
x1, Var
f2 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' = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> ([Symbol], [SpecType])
vargs) [SpecType]
ts1'
            vs2' :: [Symbol]
vs2' = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> ([Symbol], [SpecType])
vargs) [SpecType]
ts2'
            bs1' :: [Symbol]
bs1' = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a b. (a, b) -> b
snd [(Symbol, [Symbol])]
bs1
            bs2' :: [Symbol]
bs2' = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a b. (a, b) -> b
snd [(Symbol, [Symbol])]
bs2
            bs2vs :: Subst
bs2vs = [(Symbol, Expr)] -> Subst
F.mkSubst forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Symbol, [Symbol])]
bs1 forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Symbol, [Symbol])]
bs2 forall a. [a] -> [a] -> [a]
++ [Symbol]
bs1' forall a. [a] -> [a] -> [a]
++ [Symbol]
bs2') forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Symbol -> Expr
F.EVar ([Symbol]
vs1 forall a. [a] -> [a] -> [a]
++ [Symbol]
vs2 forall a. [a] -> [a] -> [a]
++ [Symbol]
vs1' forall a. [a] -> [a] -> [a]
++ [Symbol]
vs2')
          in [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)
  = 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 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 = forall a. Subable a => Subst -> a -> a
F.subst forall a b. (a -> b) -> a -> b
$ [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
v1, Symbol -> Expr
F.EVar Symbol
resL), (Symbol
v2, Symbol -> Expr
F.EVar Symbol
resR)]
    CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> SpecType
-> SpecType
-> Expr
-> CG ()
consRelCheck CGEnv
γ [RelPred]
ψ CoreExpr
d1 CoreExpr
d2 SpecType
s1 SpecType
s2 (forall {a}. Subable a => a -> a
qsubst Expr
q)
    let subst :: a -> a
subst = forall a. Subable a => Subst -> a -> a
F.subst forall a b. (a -> b) -> a -> b
$ [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
v1, Symbol -> Expr
F.EVar forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
F.symbol Var
x1), (Symbol
v2, Symbol -> Expr
F.EVar forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
F.symbol Var
x2)]
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall {a}. Subable a => a -> a
subst SpecType
t1, forall {a}. Subable a => a -> a
subst SpecType
t2, [(forall {a}. Subable a => a -> a
subst 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)
  = 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 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
    (SpecType
_, SpecType
_, [Expr]
qs) <- CGEnv
-> [RelPred]
-> CoreExpr
-> CoreExpr
-> CG (SpecType, SpecType, [Expr])
consRelSynth CGEnv
γ [RelPred]
ψ CoreExpr
d1 CoreExpr
d2
    let subst :: a -> a
subst =
          forall a. Subable a => Subst -> a -> a
F.subst forall a b. (a -> b) -> a -> b
$ [(Symbol, Expr)] -> Subst
F.mkSubst
            [(Symbol
v1, Symbol -> Expr
F.EVar forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
F.symbol Var
x1), (Symbol
v2, Symbol -> Expr
F.EVar forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
F.symbol Var
x2)]
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall {a}. Subable a => a -> a
subst SpecType
t1, forall {a}. Subable a => a -> a
subst SpecType
t2, forall a b. (a -> b) -> [a] -> [b]
map forall {a}. Subable a => a -> a
subst [Expr]
qs)
consRelSynthApp CGEnv
_ [RelPred]
_ RFun{} RFun{} [Expr]
ps d1 :: CoreExpr
d1@(Var Var
_) d2 :: CoreExpr
d2@(Var Var
_)
  = forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"consRelSynthApp: multiple rel sigs not supported " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp ([Expr]
ps, CoreExpr
d1, CoreExpr
d2)
consRelSynthApp CGEnv
_ [RelPred]
_ RFun{} RFun{} [Expr]
_ CoreExpr
d1 CoreExpr
d2 =
  forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"consRelSynthApp: expected application to variables, got" forall a. [a] -> [a] -> [a]
++ 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 =
  forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"consRelSynthApp: malformed function types or predicate for arguments " forall a. [a] -> [a] -> [a]
++ 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
?= forall a. Symbolic a => a -> Symbol
F.symbol Var
x = SpecType
t
  | Bool
otherwise = forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
msg forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp Var
x forall a. [a] -> [a] -> [a]
++ [Char]
" not in scope " forall a. [a] -> [a] -> [a]
++ 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) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [Char] -> a -> a
traceWhenLoud ([Char]
"SELFIFICATION " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp (Var
x, SpecType -> SpecType
removeAbsRef forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => SpecType -> a -> SpecType
selfify SpecType
t Var
x)) SpecType -> SpecType
removeAbsRef forall a b. (a -> b) -> a -> b
$ 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) =
  forall e a. (PPrint e, PPrint a) => [Char] -> e -> CG a -> CG a
traceUSyn [Char]
"Lit" CoreExpr
e forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SpecType -> SpecType
removeAbsRef forall a b. (a -> b) -> a -> b
$ forall c tv a. RType c tv a -> RType c tv (UReft a)
uRType forall a b. (a -> b) -> a -> b
$ Literal -> RType RTyCon RTyVar Reft
literalFRefType Literal
c
consUnarySynth CGEnv
γ e :: CoreExpr
e@(Let CoreBind
_ CoreExpr
_) =
  forall e a. (PPrint e, PPrint a) => [Char] -> e -> CG a -> CG a
traceUSyn [Char]
"Let" CoreExpr
e forall a b. (a -> b) -> a -> b
$ do
  SpecType
t   <- Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyType (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) KVKind
LetE CoreExpr
e forall a b. (a -> b) -> a -> b
$ CoreExpr -> Type
Ghc.exprType CoreExpr
e
  WfC -> CG ()
addW forall a b. (a -> b) -> a -> b
$ CGEnv -> SpecType -> WfC
WfC CGEnv
γ SpecType
t
  CGEnv -> CoreExpr -> SpecType -> CG ()
consUnaryCheck CGEnv
γ CoreExpr
e SpecType
t
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SpecType -> SpecType
removeAbsRef SpecType
t
consUnarySynth CGEnv
γ e' :: CoreExpr
e'@(App CoreExpr
e CoreExpr
d) =
  forall e a. (PPrint e, PPrint a) => [Char] -> e -> CG a -> CG a
traceUSyn [Char]
"App" CoreExpr
e' forall a b. (a -> b) -> a -> b
$ do
  SpecType
et <- CGEnv -> CoreExpr -> CG SpecType
consUnarySynth CGEnv
γ CoreExpr
e
  CGEnv -> SpecType -> CoreExpr -> CG SpecType
consUnarySynthApp CGEnv
γ SpecType
et CoreExpr
d
consUnarySynth CGEnv
γ e' :: CoreExpr
e'@(Lam Var
α CoreExpr
e) | Var -> Bool
Ghc.isTyVar Var
α =
                             forall e a. (PPrint e, PPrint a) => [Char] -> e -> CG a -> CG a
traceUSyn [Char]
"LamTyp" CoreExpr
e' forall a b. (a -> b) -> a -> b
$ do
  CGEnv
γ' <- CGEnv
γ CGEnv -> Var -> CG CGEnv
`extendWithTyVar` Var
α
  SpecType
t' <- CGEnv -> CoreExpr -> CG SpecType
consUnarySynth CGEnv
γ' CoreExpr
e
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SpecType -> SpecType
removeAbsRef forall a b. (a -> b) -> a -> b
$ forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT (forall tv s. tv -> RTVar tv s
makeRTVar forall a b. (a -> b) -> a -> b
$ Var -> RTyVar
rTyVar Var
α) SpecType
t' forall a. Monoid a => a
mempty
consUnarySynth CGEnv
γ e :: CoreExpr
e@(Lam Var
x CoreExpr
d)  =
  forall e a. (PPrint e, PPrint a) => [Char] -> e -> CG a -> CG a
traceUSyn [Char]
"Lam" CoreExpr
e 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 forall a b. (a -> b) -> a -> b
$ CoreExpr -> Type
Ghc.exprType CoreExpr
e
  SpecType
s  <- Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyType (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) KVKind
LamE (forall b. Var -> Expr b
Var Var
x) Type
s'
  CGEnv
γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consUnarySynth (Lam)", forall a. Symbolic a => a -> Symbol
F.symbol Var
x, SpecType
s)
  SpecType
t  <- CGEnv -> CoreExpr -> CG SpecType
consUnarySynth CGEnv
γ' CoreExpr
d
  WfC -> CG ()
addW forall a b. (a -> b) -> a -> b
$ CGEnv -> SpecType -> WfC
WfC CGEnv
γ SpecType
s
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SpecType -> SpecType
removeAbsRef forall a b. (a -> b) -> a -> b
$ forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun (forall a. Symbolic a => a -> Symbol
F.symbol Var
x) (Config -> RFInfo
mkRFInfo forall a b. (a -> b) -> a -> b
$ forall t. HasConfig t => t -> Config
getConfig CGEnv
γ) SpecType
s SpecType
t forall a. Monoid a => a
mempty
consUnarySynth CGEnv
γ e :: CoreExpr
e@(Case CoreExpr
_ Var
_ Type
_ [Alt Var]
alts) =
  forall e a. (PPrint e, PPrint a) => [Char] -> e -> CG a -> CG a
traceUSyn [Char]
"Case" CoreExpr
e forall a b. (a -> b) -> a -> b
$ do
  SpecType
t   <- Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyType (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) ([Alt Var] -> KVKind
caseKVKind [Alt Var]
alts) CoreExpr
e forall a b. (a -> b) -> a -> b
$ CoreExpr -> Type
Ghc.exprType CoreExpr
e
  WfC -> CG ()
addW forall a b. (a -> b) -> a -> b
$ CGEnv -> SpecType -> WfC
WfC CGEnv
γ SpecType
t
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SpecType -> SpecType
removeAbsRef SpecType
t
consUnarySynth CGEnv
_ e :: CoreExpr
e@(Cast CoreExpr
_ CoercionR
_) = forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"consUnarySynth is undefined for Cast " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp CoreExpr
e
consUnarySynth CGEnv
_ e :: CoreExpr
e@(Type Type
_) = forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"consUnarySynth is undefined for Type " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp CoreExpr
e
consUnarySynth CGEnv
_ e :: CoreExpr
e@(Coercion CoercionR
_) = forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"consUnarySynth is undefined for Coercion " forall a. [a] -> [a] -> [a]
++ 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 (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 = forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"FunTy was expected but got " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp Type
t forall a. [a] -> [a] -> [a]
++ [Char]
"\t for expression" forall a. [a] -> [a] -> [a]
++ 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' -> forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
v RFInfo
i SpecType
s SpecType
t' RReft
r) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType -> Expr -> Maybe SpecType
selfifyExpr SpecType
t (Expr -> Expr -> Expr
F.EApp Expr
f (Symbol -> Expr
F.EVar Symbol
v))
selfifyExpr SpecType
t Expr
e | SpecType -> Bool
base SpecType
t = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ SpecType
t forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` forall {a}. Expression a => a -> RReft
eq Expr
e
  where eq :: a -> RReft
eq = forall r. r -> UReft r
uTop forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Expression a => a -> Reft
F.exprReft
selfifyExpr SpecType
_ Expr
_ = 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 forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` forall {a}. Symbolic a => a -> RReft
eq a
x
  where eq :: a -> RReft
eq = forall r. r -> UReft r
uTop forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Reft
F.symbolReft forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
F.EVar forall a b. (a -> b) -> a -> b
$ 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
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SpecType
t forall a. Subable a => a -> (Symbol, Expr) -> a
`F.subst1` (Symbol
x, Symbol -> Expr
F.EVar forall a b. (a -> b) -> a -> b
$ 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
    SpecType
s' <- Bool -> Type -> CG SpecType
trueTy (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) Type
s
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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' (forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar (RType RTyCon RTyVar ())
α, SpecType
s') SpecType
t
consUnarySynthApp CGEnv
_ RFun{} CoreExpr
d =
  forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"consUnarySynthApp expected Var as a funciton arg, got " forall a. [a] -> [a] -> [a]
++ 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 =
  forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"consUnarySynthApp malformed function type " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp SpecType
ft forall a. [a] -> [a] -> [a]
++
            [Char]
" for argument " forall a. [a] -> [a] -> [a]
++ 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
  SpecType
s <- CGEnv -> CoreExpr -> CG SpecType
consUnarySynth CGEnv
γ CoreExpr
d
  CGEnv
γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consUnaryCheck Let", forall a. Symbolic a => a -> Symbol
F.symbol Var
x, SpecType
s)
  CGEnv -> CoreExpr -> SpecType -> CG ()
consUnaryCheck CGEnv
γ' CoreExpr
e SpecType
t
consUnaryCheck CGEnv
γ CoreExpr
e SpecType
t = do
  SpecType
s <- CGEnv -> CoreExpr -> CG SpecType
consUnarySynth CGEnv
γ CoreExpr
e
  SubC -> [Char] -> CG ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC CGEnv
γ SpecType
s SpecType
t) ([Char]
"consUnaryCheck (Synth): s = " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp SpecType
s forall a. [a] -> [a] -> [a]
++ [Char]
" t = " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp SpecType
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)
  = 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 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
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consRelSub HOF", forall a. Symbolic a => a -> Symbol
F.symbol Symbol
g1, SpecType
s1)
    CGEnv
γ'' <- CGEnv
γ' CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consRelSub HOF", forall a. Symbolic a => a -> Symbol
F.symbol Symbol
g2, SpecType
s2)
    let psubst :: Expr -> Expr
psubst = Symbol -> Symbol -> Expr -> Expr
unapplyArg Symbol
resL Symbol
g1 forall a. Semigroup a => a -> a -> a
<> Symbol -> Symbol -> Expr -> Expr
unapplyArg Symbol
resR Symbol
g2
    CGEnv -> SpecType -> SpecType -> Expr -> Expr -> CG ()
consRelSub CGEnv
γ'' SpecType
t1 SpecType
t2 (Expr -> Expr
psubst Expr
p1) (Expr -> Expr
psubst Expr
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)
  = 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 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
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consRelSub HOF", forall a. Symbolic a => a -> Symbol
F.symbol Symbol
g1, SpecType
s1)
    CGEnv
γ'' <- CGEnv
γ' CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consRelSub HOF", forall a. Symbolic a => a -> Symbol
F.symbol Symbol
g2, SpecType
s2)
    let psubst :: Expr -> Expr
psubst = Symbol -> Symbol -> Expr -> Expr
unapplyArg Symbol
resL Symbol
g1 forall a. Semigroup a => a -> a -> a
<> Symbol -> Symbol -> Expr -> Expr
unapplyArg Symbol
resR Symbol
g2
    CGEnv -> SpecType -> SpecType -> Expr -> Expr -> CG ()
consRelSub CGEnv
γ'' SpecType
t1 SpecType
t2 (Expr -> Expr
psubst Expr
p1) (Expr -> Expr
psubst Expr
p2)
consRelSub CGEnv
γ f1 :: SpecType
f1@(RFun Symbol
x1 RFInfo
_ SpecType
s1 SpecType
e1 RReft
_) SpecType
f2 Expr
p1 Expr
p2 =
  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 forall a b. (a -> b) -> a -> b
$ do
    CGEnv
γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consRelSub RFun L", forall a. Symbolic a => a -> Symbol
F.symbol Symbol
x1, SpecType
s1)
    let psubst :: Expr -> Expr
psubst = Symbol -> Symbol -> Expr -> Expr
unapplyArg Symbol
resL Symbol
x1
    CGEnv -> SpecType -> SpecType -> Expr -> Expr -> CG ()
consRelSub CGEnv
γ' SpecType
e1 SpecType
f2 (Expr -> Expr
psubst Expr
p1) (Expr -> Expr
psubst Expr
p2)
consRelSub CGEnv
γ SpecType
f1 f2 :: SpecType
f2@(RFun Symbol
x2 RFInfo
_ SpecType
s2 SpecType
e2 RReft
_) Expr
p1 Expr
p2 =
  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 forall a b. (a -> b) -> a -> b
$ do
    CGEnv
γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consRelSub RFun R", forall a. Symbolic a => a -> Symbol
F.symbol Symbol
x2, SpecType
s2)
    let psubst :: Expr -> Expr
psubst = Symbol -> Symbol -> Expr -> Expr
unapplyArg Symbol
resR Symbol
x2
    CGEnv -> SpecType -> SpecType -> Expr -> Expr -> CG ()
consRelSub CGEnv
γ' SpecType
f1 SpecType
e2 (Expr -> Expr
psubst Expr
p1) (Expr -> Expr
psubst Expr
p2)
consRelSub CGEnv
γ SpecType
t1 SpecType
t2 Expr
p1 Expr
p2 | forall t t1 t2. RType t t1 t2 -> Bool
isBase SpecType
t1 Bool -> Bool -> Bool
&& forall t t1 t2. RType t t1 t2 -> Bool
isBase SpecType
t2 =
  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 forall a b. (a -> b) -> a -> b
$ do
    Symbol
rl <- forall (m :: * -> *) a. Freshable m a => m a
fresh
    Symbol
rr <- forall (m :: * -> *) a. Freshable m a => m a
fresh
    CGEnv
γ' <- CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consRelSub Base L", Symbol
rl, SpecType
t1)
    CGEnv
γ'' <- CGEnv
γ' CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"consRelSub Base R", Symbol
rr, SpecType
t2)
    let cstr :: Expr
cstr = forall a. Subable a => Subst -> a -> a
F.subst ([(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
resL, Symbol -> Expr
F.EVar Symbol
rl), (Symbol
resR, Symbol -> Expr
F.EVar Symbol
rr)]) forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
F.PImp Expr
p1 Expr
p2
    CGEnv -> Expr -> [Char] -> CG ()
entl CGEnv
γ'' (forall a. [Char] -> a -> a
traceWhenLoud ([Char]
"consRelSub Base cstr " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp Expr
cstr) Expr
cstr) [Char]
"consRelSub Base"
consRelSub CGEnv
_ t1 :: SpecType
t1@(RHole RReft
_) t2 :: SpecType
t2@(RHole RReft
_) Expr
_ Expr
_ = forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"consRelSub is undefined for RHole " forall a. [a] -> [a] -> [a]
++ 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
_ = forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"consRelSub is undefined for RExprArg " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (SpecType
t1, SpecType
t2)
consRelSub CGEnv
_ t1 :: SpecType
t1@REx {} t2 :: SpecType
t2@REx {} Expr
_ Expr
_ = forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"consRelSub is undefined for REx " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (SpecType
t1, SpecType
t2)
consRelSub CGEnv
_ t1 :: SpecType
t1@RAllE {} t2 :: SpecType
t2@RAllE {} Expr
_ Expr
_ = forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"consRelSub is undefined for RAllE " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (SpecType
t1, SpecType
t2)
consRelSub CGEnv
_ t1 :: SpecType
t1@RRTy {} t2 :: SpecType
t2@RRTy {} Expr
_ Expr
_ = forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"consRelSub is undefined for RRTy " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (SpecType
t1, SpecType
t2)
consRelSub CGEnv
_ t1 :: SpecType
t1@RAllP {} t2 :: SpecType
t2@RAllP {} Expr
_ Expr
_ = forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"consRelSub is undefined for RAllP " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (SpecType
t1, SpecType
t2)
consRelSub CGEnv
_ t1 :: SpecType
t1@RAllT {} t2 :: SpecType
t2@RAllT {} Expr
_ Expr
_ = forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"consRelSub is undefined for RAllT " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (SpecType
t1, SpecType
t2)
consRelSub CGEnv
_ SpecType
t1 SpecType
t2 Expr
_ Expr
_ =  forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"consRelSub is undefined for different types " forall a. [a] -> [a] -> [a]
++ 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 = (forall a b. (a -> b) -> [a] -> [b]
map (Var, Var, SpecType, SpecType, Expr) -> RelPred
toRel [(Var, Var, SpecType, SpecType, Expr)]
ho, forall a b. (a -> b) -> [a] -> [b]
map 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) = forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (Expr -> Bool
isFuncPred forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a} {b} {c} {d} {e}. (a, b, c, d, e) -> e
toUnary) (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 = forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
vs1 (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> ([Symbol], [SpecType])
vargs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
ts1')
            in  let bs2 :: [(Symbol, [Symbol])]
bs2 = forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
vs2 (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> ([Symbol], [SpecType])
vargs 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 forall a b. (a -> b) -> a -> b
$ Expr -> RelExpr
ERBasic Expr
q
                    in forall a. [Char] -> a -> a
traceWhenLoud ([Char]
"partitionArgs toRel: " forall a. [a] -> [a] -> [a]
++ 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 = forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
msg forall a. [a] -> [a] -> [a]
++ [Char]
": expected RAllT, got: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp SpecType
t

forgetRAllP :: PVU RTyCon RTyVar -> SpecType -> SpecType
forgetRAllP :: PVU RTyCon RTyVar -> SpecType -> SpecType
forgetRAllP PVU 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,
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
qs forall a. Eq a => a -> a -> Bool
==) [forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
xs1, forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
xs2, forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
vs1, forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
vs2, forall (t :: * -> *) a. Foldable t => t a -> Int
length [SpecType]
ts1, forall (t :: * -> *) a. Foldable t => t a -> Int
length [SpecType]
ts2]
  = 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 = forall a. [Char] -> a -> a
traceWhenLoud ([Char]
"args guard" forall a. [a] -> [a] -> [a]
++ 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)) 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 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 forall a. a -> [a] -> [a]
: SpecType -> [RReft]
refts SpecType
t
refts (RFun Symbol
_ RFInfo
_ SpecType
_ SpecType
t RReft
r) = RReft
r 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
_) = forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (Symbol
v forall a. a -> [a] -> [a]
:) (SpecType
s forall a. a -> [a] -> [a]
:) 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 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", forall a. Symbolic a => a -> Symbol
F.symbol Var
a, forall r. Monoid r => Type -> RRType r
kindToRType forall a b. (a -> b) -> a -> b
$ Var -> Type
Ghc.tyVarKind Var
a)
  | Bool
otherwise
  = 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 forall a. Eq a => a -> a -> Bool
== Symbol
x1 then Symbol -> Expr
F.EVar Symbol
x2 else SpecType -> SpecType -> Symbol -> Expr
matchFunArgs SpecType
t1 SpecType
t2 Symbol
x
matchFunArgs SpecType
t1 SpecType
t2 Symbol
x | forall t t1 t2. RType t t1 t2 -> Bool
isBase SpecType
t1 Bool -> Bool -> Bool
&& forall t t1 t2. RType t t1 t2 -> Bool
isBase SpecType
t2 = Symbol -> Expr
F.EVar Symbol
x
matchFunArgs SpecType
t1 SpecType
t2 Symbol
_ = forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"matchFunArgs undefined for " forall a. [a] -> [a] -> [a]
++ 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 forall a b. (a -> b) -> a -> b
$ (Symbol, Expr) -> RReft
uReft (Symbol
F.vv_, Expr -> Expr -> Expr
F.PIff (Symbol -> Expr
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
γ (Reft -> Expr
F.reftPred forall a b. (a -> b) -> a -> b
$ forall r. UReft r -> r
ur_reft RReft
r) forall a b. (a -> b) -> a -> b
$ [Char]
"entlFunRefts " 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 forall a b. (a -> b) -> a -> b
$ [Char]
msg forall a. [a] -> [a] -> [a]
++ [Char]
" L"
  CGEnv -> RReft -> [Char] -> CG ()
entlFunReft CGEnv
γ RReft
r2 forall a b. (a -> b) -> a -> b
$ [Char]
msg 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 = forall a. Subable a => HashMap Var Type -> a -> a
subTy (forall k v. Hashable k => k -> v -> HashMap k v
M.singleton Var
x forall a b. (a -> b) -> a -> b
$ Var -> Type
TyVarTy Var
v) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subable a => HashMap Var CoreExpr -> a -> a
sub (forall k v. Hashable k => k -> v -> HashMap k v
M.singleton Var
x forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ Unique -> OccName -> Name
Ghc.mkSystemName (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 (forall a. NamedThing a => a -> [Char]
Ghc.getOccString Var
v forall a. [a] -> [a] -> [a]
++ [Char]
s) Var
v

lookupBind :: Var -> [CoreBind] -> CoreBind
lookupBind :: Var -> [CoreBind] -> CoreBind
lookupBind Var
x [CoreBind]
bs = case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Var
x (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {a}. Bind a -> [(a, Bind a)]
binds [CoreBind]
bs) of
  Maybe CoreBind
Nothing -> forall a. [Char] -> a
F.panic forall a b. (a -> b) -> a -> b
$ [Char]
"Not found definition for " forall a. [a] -> [a] -> [a]
++ 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', 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 =
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(SpecType, SpecType)]
mkargs 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) forall a b. (a -> b) -> a -> b
$ [Char]
"subUnarySig tUn = " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp SpecType
ut forall a. [a] -> [a] -> [a]
++ [Char]
" tRel = " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp SpecType
rt
  where
    mkargs :: [(SpecType, SpecType)]
mkargs = forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ SpecType -> ([Symbol], [SpecType])
vargs SpecType
tRel) (forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ SpecType -> ([Symbol], [SpecType])
vargs SpecType
tUn)
    tUn :: SpecType
tUn = CGEnv -> Var -> [Char] -> SpecType
symbolType CGEnv
γ Var
x forall a b. (a -> b) -> a -> b
$ [Char]
"subUnarySig " forall a. [a] -> [a] -> [a]
++ 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
  Symbol
dummy <- forall (m :: * -> *) a. Freshable m a => m a
fresh
  let reft :: RReft
reft = (Symbol, Expr) -> RReft
uReft (Symbol
F.vv_, [Expr] -> Expr
F.PAnd [Expr]
ps)
  CGEnv
γ CGEnv -> ([Char], Symbol, SpecType) -> CG CGEnv
+= ([Char]
"extend with predicate env", Symbol
dummy, forall c tv r. tv -> r -> RType c tv r
RVar (Symbol -> RTyVar
symbolRTyVar Symbol
F.dummySymbol) RReft
reft)

unapplyArg :: F.Symbol -> F.Symbol -> F.Expr -> F.Expr
unapplyArg :: Symbol -> Symbol -> Expr -> Expr
unapplyArg Symbol
f Symbol
y Expr
e = 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 forall a. Eq a => a -> a -> Bool
== Symbol
f Bool -> Bool -> Bool
&& Symbol
x forall a. Eq a => a -> a -> Bool
== Symbol
y = Symbol -> Expr
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 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
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
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
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
F.PImp Expr
a (RelExpr -> Expr
fromRelExpr RelExpr
b)
fromRelExpr (ERUnChecked Expr
a RelExpr
b) = Expr -> Expr -> Expr
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 = forall a. [Char] -> a -> a
traceWhenLoud ([Char]
msg forall a. [a] -> [a] -> [a]
++ [Char]
" RelSub\n"
                      forall a. [a] -> [a] -> [a]
++ [Char]
"t: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp t
t forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n"
                      forall a. [a] -> [a] -> [a]
++ [Char]
"s: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp s
s forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n"
                      forall a. [a] -> [a] -> [a]
++ [Char]
"p: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp p
p forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n"
                      forall a. [a] -> [a] -> [a]
++ [Char]
"q: " forall a. [a] -> [a] -> [a]
++ 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 = 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 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
a, b
b, c
c) <- CG (a, b, c)
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
trace ([Char]
expr forall a. [a] -> [a] -> [a]
++ [Char]
" To SYNTH") e
e d
d a
a b
b c
c CG (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 = 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
  a
t <- CG a
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
trace ([Char]
expr forall a. [a] -> [a] -> [a]
++ [Char]
" To SYNTH UNARY") e
e Expr
dummy a
t Expr
dummy Expr
dummy CG a
cg
  where dummy :: Expr
dummy = Expr
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 = forall a. [Char] -> a -> a
traceWhenLoud ([Char]
msg forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
                      forall a. [a] -> [a] -> [a]
++ [Char]
"e: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp e
e forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n"
                      forall a. [a] -> [a] -> [a]
++ [Char]
"d: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp d
d forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n"
                      forall a. [a] -> [a] -> [a]
++ [Char]
"t: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp t
t forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n"
                      forall a. [a] -> [a] -> [a]
++ [Char]
"s: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp s
s forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n"
                      forall a. [a] -> [a] -> [a]
++ [Char]
"p: " forall a. [a] -> [a] -> [a]
++ 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 = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
whenLoud ([Char] -> IO ()
putStrLn [Char]
s) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return a
a