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

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

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

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

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

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

type PrEnv = [RelPred]

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

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

removeAbsRef :: SpecType -> SpecType
removeAbsRef :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
removeAbsRef (RVar RTyVar
v (MkUReft ReftBV Symbol Symbol
r PredicateBV Symbol Symbol
_))
  = RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall {b} {v} {b} {v} {c}.
(Monoid (PredicateBV b v), Eq b) =>
RTypeBV b v c RTyVar (UReftBV b v (ReftBV Symbol Symbol))
out
    where
      r' :: UReftBV b v (ReftBV Symbol Symbol)
r' = ReftBV Symbol Symbol
-> PredicateBV b v -> UReftBV b v (ReftBV Symbol Symbol)
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft ReftBV Symbol Symbol
r PredicateBV b v
forall a. Monoid a => a
mempty
      out :: RTypeBV b v c RTyVar (UReftBV b v (ReftBV Symbol Symbol))
out = RTyVar
-> UReftBV b v (ReftBV Symbol Symbol)
-> RTypeBV b v c RTyVar (UReftBV b v (ReftBV Symbol Symbol))
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar  RTyVar
v UReftBV b v (ReftBV Symbol Symbol)
forall {b} {v}.
(Monoid (PredicateBV b v), Eq b) =>
UReftBV b v (ReftBV Symbol Symbol)
r'
removeAbsRef (RFun  Symbol
b RFInfo
i RTypeBV Symbol Symbol RTyCon RTyVar RReft
s RTypeBV Symbol Symbol RTyCon RTyVar RReft
t (MkUReft ReftBV Symbol Symbol
r PredicateBV Symbol Symbol
_))
  = RTypeBV Symbol Symbol RTyCon RTyVar RReft
out
    where
      r' :: UReftBV b v (ReftBV Symbol Symbol)
r' = ReftBV Symbol Symbol
-> PredicateBV b v -> UReftBV b v (ReftBV Symbol Symbol)
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft ReftBV Symbol Symbol
r PredicateBV b v
forall a. Monoid a => a
mempty
      out :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
out = Symbol
-> RFInfo
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun  Symbol
b RFInfo
i (RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
removeAbsRef RTypeBV Symbol Symbol RTyCon RTyVar RReft
s) (RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
removeAbsRef RTypeBV Symbol Symbol RTyCon RTyVar RReft
t) RReft
forall {b} {v}.
(Monoid (PredicateBV b v), Eq b) =>
UReftBV b v (ReftBV Symbol Symbol)
r'
removeAbsRef (RAllT RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar (NoReftB Symbol))
b RTypeBV Symbol Symbol RTyCon RTyVar RReft
t RReft
r)
  = RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar (NoReftB Symbol))
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar (NoReftB Symbol))
b (RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
removeAbsRef RTypeBV Symbol Symbol RTyCon RTyVar RReft
t) RReft
r
removeAbsRef (RAllP PVUBV Symbol Symbol RTyCon RTyVar
p RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)
  = RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
removeAbsRef (PVUBV Symbol Symbol RTyCon RTyVar
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forgetRAllP PVUBV Symbol Symbol RTyCon RTyVar
p RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)
removeAbsRef (RApp  (RTyCon TyCon
c [PVUBV Symbol Symbol RTyCon RTyVar]
_ TyConInfo
i) [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
as [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
_ (MkUReft ReftBV Symbol Symbol
r PredicateBV Symbol Symbol
_))
  = RTypeBV Symbol Symbol RTyCon RTyVar RReft
out
    where
      c' :: RTyCon
c' = TyCon -> [PVUBV Symbol Symbol RTyCon RTyVar] -> TyConInfo -> RTyCon
RTyCon TyCon
c [] TyConInfo
i
      as' :: [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
as' = (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
forall a b. (a -> b) -> [a] -> [b]
map RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
removeAbsRef [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
as
      r' :: UReftBV b v (ReftBV Symbol Symbol)
r' = ReftBV Symbol Symbol
-> PredicateBV b v -> UReftBV b v (ReftBV Symbol Symbol)
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft ReftBV Symbol Symbol
r PredicateBV b v
forall a. Monoid a => a
mempty
      out :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
out = RTyCon
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
-> RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
RApp RTyCon
c' [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
as' [] RReft
forall {b} {v}.
(Monoid (PredicateBV b v), Eq b) =>
UReftBV b v (ReftBV Symbol Symbol)
r'
removeAbsRef (RAllE Symbol
b RTypeBV Symbol Symbol RTyCon RTyVar RReft
a RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)
  = Symbol
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllE Symbol
b (RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
removeAbsRef RTypeBV Symbol Symbol RTyCon RTyVar RReft
a) (RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
removeAbsRef RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)
removeAbsRef (REx   Symbol
b RTypeBV Symbol Symbol RTyCon RTyVar RReft
a RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)
  = Symbol
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
REx   Symbol
b (RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
removeAbsRef RTypeBV Symbol Symbol RTyCon RTyVar RReft
a) (RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
removeAbsRef RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)
removeAbsRef (RAppTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
s RTypeBV Symbol Symbol RTyCon RTyVar RReft
t RReft
r)
  = RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
RTypeBV b v c tv r -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAppTy (RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
removeAbsRef RTypeBV Symbol Symbol RTyCon RTyVar RReft
s) (RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
removeAbsRef RTypeBV Symbol Symbol RTyCon RTyVar RReft
t) RReft
r
removeAbsRef (RRTy  [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
e RReft
r Oblig
o RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)
  = [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> RReft
-> Oblig
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r.
[(b, RTypeBV b v c tv r)]
-> r -> Oblig -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RRTy  [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
e RReft
r Oblig
o (RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
removeAbsRef RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)
removeAbsRef RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
  = RTypeBV Symbol Symbol RTyCon RTyVar RReft
t

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

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

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

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

consRelCheckBind CGEnv
γ [RelPred]
ψ (NonRec Var
x1 Expr Var
e1) Bind Var
b2 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2 RelExpr
a RelExpr
p =
  CGEnv
-> [RelPred]
-> Bind Var
-> Bind Var
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RelExpr
-> RelExpr
-> CG ()
consRelCheckBind CGEnv
γ [RelPred]
ψ ([(Var, Expr Var)] -> Bind Var
forall b. [(b, Expr b)] -> Bind b
Rec [(Var
x1, Expr Var
e1)]) Bind Var
b2 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2 RelExpr
a RelExpr
p

consRelCheckBind CGEnv
γ [RelPred]
ψ Bind Var
b1 (NonRec Var
x2 Expr Var
e2) RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2 RelExpr
a RelExpr
p =
  CGEnv
-> [RelPred]
-> Bind Var
-> Bind Var
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RelExpr
-> RelExpr
-> CG ()
consRelCheckBind CGEnv
γ [RelPred]
ψ Bind Var
b1 ([(Var, Expr Var)] -> Bind Var
forall b. [(b, Expr b)] -> Bind b
Rec [(Var
x2, Expr Var
e2)]) RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2 RelExpr
a RelExpr
p

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

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

consRelCheckBind CGEnv
_ [RelPred]
_ b1 :: Bind Var
b1@(Rec [(Var, Expr Var)]
_) b2 :: Bind Var
b2@(Rec [(Var, Expr Var)]
_) RTypeBV Symbol Symbol RTyCon RTyVar RReft
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
_ RelExpr
_ RelExpr
_
  = [Char] -> CG ()
forall a. HasCallStack => [Char] -> a
F.panic ([Char] -> CG ()) -> [Char] -> CG ()
forall a b. (a -> b) -> a -> b
$ [Char]
"consRelCheckBind Rec: multiple binders are not supported " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (Bind Var, Bind Var) -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp (Bind Var
b1, Bind Var
b2)

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

consRelCheck CGEnv
γ [RelPred]
ψ Expr Var
e (Tick CoreTickish
tt Expr Var
d) RTypeBV Symbol Symbol RTyCon RTyVar RReft
t RTypeBV Symbol Symbol RTyCon RTyVar RReft
s ExprBV Symbol Symbol
p =
  CGEnv
-> [RelPred]
-> Expr Var
-> Expr Var
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> ExprBV Symbol Symbol
-> CG ()
consRelCheck (CGEnv
γ CGEnv -> Span -> CGEnv
`setLocation` CoreTickish -> Span
Sp.Tick CoreTickish
tt) [RelPred]
ψ Expr Var
e Expr Var
d RTypeBV Symbol Symbol RTyCon RTyVar RReft
t RTypeBV Symbol Symbol RTyCon RTyVar RReft
s ExprBV Symbol Symbol
p

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

instantiateTys :: SpecType -> [SpecType] -> SpecType
instantiateTys :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
instantiateTys = (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
RTypeBV (ReftBind RReft) Symbol RTyCon RTyVar RReft
-> RTypeBV (ReftBind RReft) Symbol RTyCon RTyVar RReft
-> RTypeBV (ReftBind RReft) Symbol RTyCon RTyVar RReft
forall {c} {tv} {r} {v}.
(FreeVar c tv, TyConable c, IsReft r,
 SubsTy tv (RTypeBV (ReftBind r) v c tv (NoReftB (ReftBind r))) c,
 SubsTy tv (RTypeBV (ReftBind r) v c tv (NoReftB (ReftBind r))) r,
 SubsTy tv (RTypeBV (ReftBind r) v c tv (NoReftB (ReftBind r))) tv,
 SubsTy
   tv
   (RTypeBV (ReftBind r) v c tv (NoReftB (ReftBind r)))
   (RTypeBV (ReftBind r) v c tv (NoReftB (ReftBind r))),
 SubsTy
   tv
   (RTypeBV (ReftBind r) v c tv (NoReftB (ReftBind r)))
   (RTVar tv (RTypeBV (ReftBind r) v c tv (NoReftB (ReftBind r)))),
 PPrint v, PPrint tv, PPrint c, PPrint r, PPrint (ReftBind r),
 PPrint (ReftVar r), Fixpoint v, Fixpoint (ReftBind r),
 Fixpoint (ReftVar r), Ord v, Ord (ReftVar r), Hashable tv) =>
RTypeBV (ReftBind r) v c tv r
-> RTypeBV (ReftBind r) v c tv r -> RTypeBV (ReftBind r) v c tv r
go
 where
  go :: RTypeBV (ReftBind r) v c tv r
-> RTypeBV (ReftBind r) v c tv r -> RTypeBV (ReftBind r) v c tv r
go (RAllT RTVar tv (RTypeBV (ReftBind r) v c tv (NoReftB (ReftBind r)))
α RTypeBV (ReftBind r) v c tv r
tbody r
_) RTypeBV (ReftBind r) v c tv r
t = (tv, RTypeBV (ReftBind r) v c tv r)
-> RTypeBV (ReftBind r) v c tv r -> RTypeBV (ReftBind r) v c tv r
forall tv r c b v.
(Eq tv, Hashable tv, IsReft r, TyConable c, Binder b,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) c,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) r,
 SubsTy
   tv (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv (NoReftB b)),
 FreeVar c tv, SubsTy tv (RTypeBV b v c tv (NoReftB b)) tv,
 SubsTy
   tv
   (RTypeBV b v c tv (NoReftB b))
   (RTVar tv (RTypeBV b v c tv (NoReftB b)))) =>
(tv, RTypeBV b v c tv r)
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
subsTyVarMeet' (RTVar tv (RTypeBV (ReftBind r) v c tv (NoReftB (ReftBind r))) -> tv
forall tv s. RTVar tv s -> tv
ty_var_value RTVar tv (RTypeBV (ReftBind r) v c tv (NoReftB (ReftBind r)))
α, RTypeBV (ReftBind r) v c tv r
t) RTypeBV (ReftBind r) v c tv r
tbody
  go RTypeBV (ReftBind r) v c tv r
tbody             RTypeBV (ReftBind r) v c tv r
t =
    [Char] -> RTypeBV (ReftBind r) v c tv r
forall a. HasCallStack => [Char] -> a
F.panic ([Char] -> RTypeBV (ReftBind r) v c tv r)
-> [Char] -> RTypeBV (ReftBind r) v c tv r
forall a b. (a -> b) -> a -> b
$ [Char]
"instantiateTys: non-polymorphic type " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ RTypeBV (ReftBind r) v c tv r -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp RTypeBV (ReftBind r) v c tv r
tbody [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" to instantiate with " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ RTypeBV (ReftBind r) v c tv r -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp RTypeBV (ReftBind r) v c tv r
t

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

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

consRelSynth CGEnv
γ [RelPred]
ψ Expr Var
e (Tick CoreTickish
tt Expr Var
d) =
  CGEnv
-> [RelPred]
-> Expr Var
-> Expr Var
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
consRelSynth (CGEnv
γ CGEnv -> Span -> CGEnv
`setLocation` CoreTickish -> Span
Sp.Tick CoreTickish
tt) [RelPred]
ψ Expr Var
e Expr Var
d

consRelSynth CGEnv
γ [RelPred]
ψ a1 :: Expr Var
a1@(App Expr Var
e1 Expr Var
d1) Expr Var
e2 | Type Type
t1 <- Expr Var -> Expr Var
GM.unTickExpr Expr Var
d1 =
  [Char]
-> Expr Var
-> Expr Var
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
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" Expr Var
a1 Expr Var
e2 (CG
   (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
    RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
 -> CG
      (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
       RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol]))
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
forall a b. (a -> b) -> a -> b
$ do
    (ft1', t2, ps) <- CGEnv
-> [RelPred]
-> Expr Var
-> Expr Var
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
consRelSynth CGEnv
γ [RelPred]
ψ Expr Var
e1 Expr Var
e2
    let (α1, ft1, _) = unRAllT ft1' "consRelSynth App Ty L"
    t1' <- trueTy (typeclass (getConfig γ)) t1
    return (subsTyVarMeet' (ty_var_value α1, t1') ft1, t2, ps)

consRelSynth CGEnv
γ [RelPred]
ψ Expr Var
e1 a2 :: Expr Var
a2@(App Expr Var
e2 Expr Var
d2) | Type Type
t2 <- Expr Var -> Expr Var
GM.unTickExpr Expr Var
d2 =
  [Char]
-> Expr Var
-> Expr Var
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
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" Expr Var
e1 Expr Var
a2 (CG
   (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
    RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
 -> CG
      (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
       RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol]))
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
forall a b. (a -> b) -> a -> b
$ do
    (t1, ft2', ps) <- CGEnv
-> [RelPred]
-> Expr Var
-> Expr Var
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
consRelSynth CGEnv
γ [RelPred]
ψ Expr Var
e1 Expr Var
e2
    let (α2, ft2, _) = unRAllT ft2' "consRelSynth App Ty R"
    t2' <- trueTy (typeclass (getConfig γ)) t2
    return (t1, subsTyVarMeet' (ty_var_value α2, t2') ft2, ps)

consRelSynth CGEnv
γ [RelPred]
ψ a1 :: Expr Var
a1@(App Expr Var
e1 Expr Var
d1) a2 :: Expr Var
a2@(App Expr Var
e2 Expr Var
d2) = [Char]
-> Expr Var
-> Expr Var
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
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" Expr Var
a1 Expr Var
a2 (CG
   (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
    RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
 -> CG
      (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
       RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol]))
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
forall a b. (a -> b) -> a -> b
$ do
  (ft1, ft2, fps) <- CGEnv
-> [RelPred]
-> Expr Var
-> Expr Var
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
consRelSynth CGEnv
γ [RelPred]
ψ Expr Var
e1 Expr Var
e2
  (t1, t2, ps) <- consRelSynthApp γ ψ ft1 ft2 fps d1 d2
  return (t1, t2, ps)

consRelSynth CGEnv
γ [RelPred]
ψ Expr Var
e Expr Var
d = [Char]
-> Expr Var
-> Expr Var
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
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" Expr Var
e Expr Var
d (CG
   (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
    RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
 -> CG
      (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
       RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol]))
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
-> CG
     (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft, [ExprBV Symbol Symbol])
forall a b. (a -> b) -> a -> b
$ do
  t <- CGEnv -> Expr Var -> CG (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
consUnarySynth CGEnv
γ Expr Var
e CG (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft
    -> CG (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> CG (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall a b.
StateT CGInfo Identity a
-> (a -> StateT CGInfo Identity b) -> StateT CGInfo Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> CG (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall (m :: * -> *).
FreshM m =>
RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> m (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
refreshTy
  s <- consUnarySynth γ d >>= refreshTy
  let ps = [RelPred]
-> Expr Var
-> Expr Var
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> [ExprBV Symbol Symbol]
lookupRelSig [RelPred]
ψ Expr Var
e Expr Var
d RTypeBV Symbol Symbol RTyCon RTyVar RReft
t RTypeBV Symbol Symbol RTyCon RTyVar RReft
s
  return (t, s, traceWhenLoud ("consRelSynth Unary synthed preds:" ++ F.showpp ps) ps)

lookupRelSig :: PrEnv -> CoreExpr -> CoreExpr -> SpecType -> SpecType -> [F.Expr]
lookupRelSig :: [RelPred]
-> Expr Var
-> Expr Var
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> [ExprBV Symbol Symbol]
lookupRelSig [RelPred]
ψ (Var Var
x1) (Var Var
x2) RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2 = (RelPred -> [ExprBV Symbol Symbol])
-> [RelPred] -> [ExprBV Symbol Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap RelPred -> [ExprBV Symbol Symbol]
match [RelPred]
ψ
  where
    match :: RelPred -> [F.Expr]
    match :: RelPred -> [ExprBV Symbol Symbol]
match (RelPred Var
f1 Var
f2 [(Symbol, [Symbol])]
bs1 [(Symbol, [Symbol])]
bs2 RelExpr
p) | Var
f1 Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
x1, Var
f2 Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
x2 =
        let ([Symbol]
vs1, [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts1') = RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> ([Symbol], [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
vargs RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1
            ([Symbol]
vs2, [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts2') = RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> ([Symbol], [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
vargs RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2
            vs1' :: [Symbol]
vs1' = (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Symbol])
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (([Symbol], [RTypeBV Symbol Symbol RTyCon RTyVar RReft]) -> [Symbol]
forall a b. (a, b) -> a
fst (([Symbol], [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
 -> [Symbol])
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft
    -> ([Symbol], [RTypeBV Symbol Symbol RTyCon RTyVar RReft]))
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> ([Symbol], [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
vargs) [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts1'
            vs2' :: [Symbol]
vs2' = (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Symbol])
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (([Symbol], [RTypeBV Symbol Symbol RTyCon RTyVar RReft]) -> [Symbol]
forall a b. (a, b) -> a
fst (([Symbol], [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
 -> [Symbol])
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft
    -> ([Symbol], [RTypeBV Symbol Symbol RTyCon RTyVar RReft]))
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> ([Symbol], [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
vargs) [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts2'
            bs1' :: [Symbol]
bs1' = ((Symbol, [Symbol]) -> [Symbol])
-> [(Symbol, [Symbol])] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Symbol, [Symbol]) -> [Symbol]
forall a b. (a, b) -> b
snd [(Symbol, [Symbol])]
bs1
            bs2' :: [Symbol]
bs2' = ((Symbol, [Symbol]) -> [Symbol])
-> [(Symbol, [Symbol])] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Symbol, [Symbol]) -> [Symbol]
forall a b. (a, b) -> b
snd [(Symbol, [Symbol])]
bs2
            bs2vs :: SubstV Symbol
bs2vs = [(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
F.mkSubst ([(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol)
-> [(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol
forall a b. (a -> b) -> a -> b
$ [Symbol]
-> [ExprBV Symbol Symbol] -> [(Symbol, ExprBV Symbol Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((Symbol, [Symbol]) -> Symbol) -> [(Symbol, [Symbol])] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, [Symbol]) -> Symbol
forall a b. (a, b) -> a
fst [(Symbol, [Symbol])]
bs1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ ((Symbol, [Symbol]) -> Symbol) -> [(Symbol, [Symbol])] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, [Symbol]) -> Symbol
forall a b. (a, b) -> a
fst [(Symbol, [Symbol])]
bs2 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol]
bs1' [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol]
bs2') ([ExprBV Symbol Symbol] -> [(Symbol, ExprBV Symbol Symbol)])
-> [ExprBV Symbol Symbol] -> [(Symbol, ExprBV Symbol Symbol)]
forall a b. (a -> b) -> a -> b
$ (Symbol -> ExprBV Symbol Symbol)
-> [Symbol] -> [ExprBV Symbol Symbol]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar ([Symbol]
vs1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol]
vs2 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol]
vs1' [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol]
vs2')
          in [SubstV (Variable (ExprBV Symbol Symbol))
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
F.subst SubstV Symbol
SubstV (Variable (ExprBV Symbol Symbol))
bs2vs (RelExpr -> ExprBV Symbol Symbol
fromRelExpr RelExpr
p)]
    match RelPred
_ = []
lookupRelSig [RelPred]
_ Expr Var
_ Expr Var
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
_ = []

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

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

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

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

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

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

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

base :: SpecType -> Bool
base :: RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Bool
base RApp{} = Bool
True
base RVar{} = Bool
True
base RTypeBV Symbol Symbol RTyCon RTyVar RReft
_      = Bool
False

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

selfify :: F.Symbolic a => SpecType -> a -> SpecType
selfify :: forall a.
Symbolic a =>
RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> a -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
selfify RTypeBV Symbol Symbol RTyCon RTyVar RReft
t a
x | RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Bool
base RTypeBV Symbol Symbol RTyCon RTyVar RReft
t = RTypeBV Symbol Symbol RTyCon RTyVar RReft
t RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RReft -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall r b v c tv.
Meet r =>
RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
`strengthen` a -> RReft
forall {a} {v}.
Symbolic a =>
a -> UReftBV Symbol v (ReftBV Symbol Symbol)
eq a
x
  where eq :: a -> UReftBV Symbol v (ReftBV Symbol Symbol)
eq = ReftBV Symbol Symbol -> UReftBV Symbol v (ReftBV Symbol Symbol)
forall r v. r -> UReftV v r
uTop (ReftBV Symbol Symbol -> UReftBV Symbol v (ReftBV Symbol Symbol))
-> (a -> ReftBV Symbol Symbol)
-> a
-> UReftBV Symbol v (ReftBV Symbol Symbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> ReftBV Symbol Symbol
forall a. Symbolic a => a -> ReftBV Symbol Symbol
F.symbolReft (Symbol -> ReftBV Symbol Symbol)
-> (a -> Symbol) -> a -> ReftBV Symbol Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol
selfify RTypeBV Symbol Symbol RTyCon RTyVar RReft
t a
e | Just RTypeBV Symbol Symbol RTyCon RTyVar RReft
t' <- RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> ExprBV Symbol Symbol
-> Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
selfifyExpr RTypeBV Symbol Symbol RTyCon RTyVar RReft
t (Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar (Symbol -> ExprBV Symbol Symbol) -> Symbol -> ExprBV Symbol Symbol
forall a b. (a -> b) -> a -> b
$ a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol a
e) = RTypeBV Symbol Symbol RTyCon RTyVar RReft
t'
selfify RTypeBV Symbol Symbol RTyCon RTyVar RReft
t a
_ = RTypeBV Symbol Symbol RTyCon RTyVar RReft
t

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

consUnarySynthApp CGEnv
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
ft Expr Var
d =
  [Char] -> CG (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall a. HasCallStack => [Char] -> a
F.panic ([Char] -> CG (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> [Char] -> CG (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall a b. (a -> b) -> a -> b
$ [Char]
"consUnarySynthApp malformed function type " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp RTypeBV Symbol Symbol RTyCon RTyVar RReft
ft [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++
            [Char]
" for argument " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr Var -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp Expr Var
d

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

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

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

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

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

partitionArg :: Var -> Var -> SpecType -> SpecType -> F.Expr -> (PrEnv, [F.Expr])
partitionArg :: Var
-> Var
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> ExprBV Symbol Symbol
-> ([RelPred], [ExprBV Symbol Symbol])
partitionArg Var
x1 Var
x2 RTypeBV Symbol Symbol RTyCon RTyVar RReft
s1 RTypeBV Symbol Symbol RTyCon RTyVar RReft
s2 ExprBV Symbol Symbol
q = [Var]
-> [Var]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [ExprBV Symbol Symbol]
-> ([RelPred], [ExprBV Symbol Symbol])
partitionArgs [Var
x1] [Var
x2] [RTypeBV Symbol Symbol RTyCon RTyVar RReft
s1] [RTypeBV Symbol Symbol RTyCon RTyVar RReft
s2] [ExprBV Symbol Symbol
q]

partitionArgs :: [Var] -> [Var] -> [SpecType] -> [SpecType] -> [F.Expr] -> (PrEnv, [F.Expr])
partitionArgs :: [Var]
-> [Var]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [ExprBV Symbol Symbol]
-> ([RelPred], [ExprBV Symbol Symbol])
partitionArgs [Var]
xs1 [Var]
xs2 [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts1 [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts2 [ExprBV Symbol Symbol]
qs = (((Var, Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
  RTypeBV Symbol Symbol RTyCon RTyVar RReft, ExprBV Symbol Symbol)
 -> RelPred)
-> [(Var, Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
     RTypeBV Symbol Symbol RTyCon RTyVar RReft, ExprBV Symbol Symbol)]
-> [RelPred]
forall a b. (a -> b) -> [a] -> [b]
map (Var, Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
 RTypeBV Symbol Symbol RTyCon RTyVar RReft, ExprBV Symbol Symbol)
-> RelPred
toRel [(Var, Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
  RTypeBV Symbol Symbol RTyCon RTyVar RReft, ExprBV Symbol Symbol)]
ho, ((Var, Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
  RTypeBV Symbol Symbol RTyCon RTyVar RReft, ExprBV Symbol Symbol)
 -> ExprBV Symbol Symbol)
-> [(Var, Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
     RTypeBV Symbol Symbol RTyCon RTyVar RReft, ExprBV Symbol Symbol)]
-> [ExprBV Symbol Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Var, Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
 RTypeBV Symbol Symbol RTyCon RTyVar RReft, ExprBV Symbol Symbol)
-> ExprBV Symbol Symbol
forall {a} {b} {c} {d} {e}. (a, b, c, d, e) -> e
toUnary [(Var, Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
  RTypeBV Symbol Symbol RTyCon RTyVar RReft, ExprBV Symbol Symbol)]
fo)
 where
  ([(Var, Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
  RTypeBV Symbol Symbol RTyCon RTyVar RReft, ExprBV Symbol Symbol)]
ho, [(Var, Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
  RTypeBV Symbol Symbol RTyCon RTyVar RReft, ExprBV Symbol Symbol)]
fo) = ((Var, Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
  RTypeBV Symbol Symbol RTyCon RTyVar RReft, ExprBV Symbol Symbol)
 -> Bool)
-> [(Var, Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
     RTypeBV Symbol Symbol RTyCon RTyVar RReft, ExprBV Symbol Symbol)]
-> ([(Var, Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft, ExprBV Symbol Symbol)],
    [(Var, Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
      RTypeBV Symbol Symbol RTyCon RTyVar RReft, ExprBV Symbol Symbol)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (ExprBV Symbol Symbol -> Bool
isFuncPred (ExprBV Symbol Symbol -> Bool)
-> ((Var, Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
     RTypeBV Symbol Symbol RTyCon RTyVar RReft, ExprBV Symbol Symbol)
    -> ExprBV Symbol Symbol)
-> (Var, Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
    RTypeBV Symbol Symbol RTyCon RTyVar RReft, ExprBV Symbol Symbol)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
 RTypeBV Symbol Symbol RTyCon RTyVar RReft, ExprBV Symbol Symbol)
-> ExprBV Symbol Symbol
forall {a} {b} {c} {d} {e}. (a, b, c, d, e) -> e
toUnary) ([Var]
-> [Var]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [ExprBV Symbol Symbol]
-> [(Var, Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
     RTypeBV Symbol Symbol RTyCon RTyVar RReft, ExprBV Symbol Symbol)]
forall t t1 t2 t3 t4.
[t] -> [t1] -> [t2] -> [t3] -> [t4] -> [(t, t1, t2, t3, t4)]
zip5 [Var]
xs1 [Var]
xs2 [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts1 [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts2 [ExprBV Symbol Symbol]
qs)
  toRel :: (Var, Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft,
 RTypeBV Symbol Symbol RTyCon RTyVar RReft, ExprBV Symbol Symbol)
-> RelPred
toRel (Var
f1, Var
f2, RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1, RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2, ExprBV Symbol Symbol
q) =
    let ([Symbol]
vs1, [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts1') = RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> ([Symbol], [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
vargs RTypeBV Symbol Symbol RTyCon RTyVar RReft
t1
    in  let ([Symbol]
vs2, [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts2') = RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> ([Symbol], [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
vargs RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2
        in  let bs1 :: [(Symbol, [Symbol])]
bs1 = [Symbol] -> [[Symbol]] -> [(Symbol, [Symbol])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
vs1 (([Symbol], [RTypeBV Symbol Symbol RTyCon RTyVar RReft]) -> [Symbol]
forall a b. (a, b) -> a
fst (([Symbol], [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
 -> [Symbol])
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft
    -> ([Symbol], [RTypeBV Symbol Symbol RTyCon RTyVar RReft]))
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> ([Symbol], [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
vargs (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Symbol])
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft] -> [[Symbol]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts1')
            in  let bs2 :: [(Symbol, [Symbol])]
bs2 = [Symbol] -> [[Symbol]] -> [(Symbol, [Symbol])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
vs2 (([Symbol], [RTypeBV Symbol Symbol RTyCon RTyVar RReft]) -> [Symbol]
forall a b. (a, b) -> a
fst (([Symbol], [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
 -> [Symbol])
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft
    -> ([Symbol], [RTypeBV Symbol Symbol RTyCon RTyVar RReft]))
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> ([Symbol], [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
vargs (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Symbol])
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft] -> [[Symbol]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts2')
                in  let rp :: RelPred
rp = Var
-> Var
-> [(Symbol, [Symbol])]
-> [(Symbol, [Symbol])]
-> RelExpr
-> RelPred
RelPred Var
f1 Var
f2 [(Symbol, [Symbol])]
bs1 [(Symbol, [Symbol])]
bs2 (RelExpr -> RelPred) -> RelExpr -> RelPred
forall a b. (a -> b) -> a -> b
$ ExprBV Symbol Symbol -> RelExpr
forall v. ExprV v -> RelExprV v
ERBasic ExprBV Symbol Symbol
q
                    in [Char] -> RelPred -> RelPred
forall a. [Char] -> a -> a
traceWhenLoud ([Char]
"partitionArgs toRel: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (Var, Var, [(Symbol, [Symbol])], [(Symbol, [Symbol])],
 ExprBV Symbol Symbol)
-> [Char]
forall a. PPrint a => a -> [Char]
F.showpp (Var
f1, Var
f2, [(Symbol, [Symbol])]
bs1, [(Symbol, [Symbol])]
bs2, ExprBV Symbol Symbol
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 :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> [Char]
-> (RTVar
      RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar (NoReftB Symbol)),
    RTypeBV Symbol Symbol RTyCon RTyVar RReft, RReft)
unRAllT (RAllT RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar (NoReftB Symbol))
α2 RTypeBV Symbol Symbol RTyCon RTyVar RReft
ft2 RReft
r2) [Char]
_ = (RTVar RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar (NoReftB Symbol))
α2, RTypeBV Symbol Symbol RTyCon RTyVar RReft
ft2, RReft
r2)
unRAllT RTypeBV Symbol Symbol RTyCon RTyVar RReft
t [Char]
msg = [Char]
-> (RTVar
      RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar (NoReftB Symbol)),
    RTypeBV Symbol Symbol RTyCon RTyVar RReft, RReft)
forall a. HasCallStack => [Char] -> a
F.panic ([Char]
 -> (RTVar
       RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar (NoReftB Symbol)),
     RTypeBV Symbol Symbol RTyCon RTyVar RReft, RReft))
-> [Char]
-> (RTVar
      RTyVar (RTypeBV Symbol Symbol RTyCon RTyVar (NoReftB Symbol)),
    RTypeBV Symbol Symbol RTyCon RTyVar RReft, RReft)
forall a b. (a -> b) -> a -> b
$ [Char]
msg [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
": expected RAllT, got: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp RTypeBV Symbol Symbol RTyCon RTyVar RReft
t

forgetRAllP :: PVU RTyCon RTyVar -> SpecType -> SpecType
forgetRAllP :: PVUBV Symbol Symbol RTyCon RTyVar
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forgetRAllP PVUBV Symbol Symbol RTyCon RTyVar
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t = RTypeBV Symbol Symbol RTyCon RTyVar RReft
t

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

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

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

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

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

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

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

concl :: F.Expr -> F.Expr
concl :: ExprBV Symbol Symbol -> ExprBV Symbol Symbol
concl (F.PImp ExprBV Symbol Symbol
_ ExprBV Symbol Symbol
p) = ExprBV Symbol Symbol -> ExprBV Symbol Symbol
concl ExprBV Symbol Symbol
p
concl ExprBV Symbol Symbol
p            = ExprBV Symbol Symbol
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, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CG CGEnv
+= ([Char]
"extendWithTyVar", Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
a, Type -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall r. IsReft r => Type -> RRType r
kindToRType (Type -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> Type -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ Var -> Type
Ghc.tyVarKind Var
a)
  | Bool
otherwise
  = CGEnv -> CG CGEnv
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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


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

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

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

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

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

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